- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] g(A) -> A [2] g(B) -> A [3] g(B) -> B [4] g(C) -> A [5] g(C) -> B [6] g(C) -> C [7] foldf(x,nil) -> x [8] foldf(x,cons(y,z)) -> f(foldf(x,z),y) [9] f(t,x) -> f'(t,g(x)) [10] f'(triple(a,b,c),C) -> triple(a,b,cons(C,c)) [11] f'(triple(a,b,c),B) -> f(triple(a,b,c),A) [12] f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b)) [13] f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { g(A) >= A ; g(B) >= A ; g(B) >= B ; g(C) >= A ; g(C) >= B ; g(C) >= C ; foldf(x,nil) >= x ; foldf(x,cons(y,z)) >= f(foldf(x,z),y) ; f(t,x) >= f'(t,g(x)) ; f'(triple(a,b,c),A) >= f''(foldf(triple(cons(A,a),nil,c),b)) ; f'(triple(a,b,c),B) >= f(triple(a,b,c),A) ; f'(triple(a,b,c),C) >= triple(a,b,cons(C,c)) ; f''(triple(a,b,c)) >= foldf(triple(a,b,nil),c) ; Marked_f''(triple(a,b,c)) >= Marked_foldf(triple(a,b,nil),c) ; Marked_foldf(x,cons(y,z)) >= Marked_foldf(x,z) ; Marked_foldf(x,cons(y,z)) >= Marked_f(foldf(x,z),y) ; Marked_f'(triple(a,b,c),A) >= Marked_f''(foldf(triple(cons(A,a),nil,c),b)) ; Marked_f'(triple(a,b,c),A) >= Marked_foldf(triple(cons(A,a),nil,c),b) ; Marked_f'(triple(a,b,c),B) >= Marked_f(triple(a,b,c),A) ; Marked_f(t,x) >= Marked_f'(t,g(x)) ; } + Disjunctions:{ { Marked_f''(triple(a,b,c)) > Marked_foldf(triple(a,b,nil),c) ; } { Marked_foldf(x,cons(y,z)) > Marked_foldf(x,z) ; } { Marked_foldf(x,cons(y,z)) > Marked_f(foldf(x,z),y) ; } { Marked_f'(triple(a,b,c),A) > Marked_f''(foldf(triple(cons(A,a),nil,c),b)) ; } { Marked_f'(triple(a,b,c),A) > Marked_foldf(triple(cons(A,a),nil,c),b) ; } { Marked_f'(triple(a,b,c),B) > Marked_f(triple(a,b,c),A) ; } { Marked_f(t,x) > Marked_f'(t,g(x)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: g(A) >= A constraint: g(B) >= A constraint: g(B) >= B constraint: g(C) >= A constraint: g(C) >= B constraint: g(C) >= C constraint: foldf(x,nil) >= x constraint: foldf(x,cons(y,z)) >= f(foldf(x,z),y) constraint: f(t,x) >= f'(t,g(x)) constraint: f'(triple(a,b,c),A) >= f''(foldf(triple(cons(A,a),nil,c),b)) constraint: f'(triple(a,b,c),B) >= f(triple(a,b,c),A) constraint: f'(triple(a,b,c),C) >= triple(a,b,cons(C,c)) constraint: f''(triple(a,b,c)) >= foldf(triple(a,b,nil),c) constraint: Marked_f''(triple(a,b,c)) >= Marked_foldf(triple(a,b,nil),c) constraint: Marked_foldf(x,cons(y,z)) >= Marked_foldf(x,z) constraint: Marked_foldf(x,cons(y,z)) >= Marked_f(foldf(x,z),y) constraint: Marked_f'(triple(a,b,c),A) >= Marked_f''(foldf(triple(cons(A,a), nil,c),b)) constraint: Marked_f'(triple(a,b,c),A) >= Marked_foldf(triple(cons(A,a),nil,c), b) constraint: Marked_f'(triple(a,b,c),B) >= Marked_f(triple(a,b,c),A) constraint: Marked_f(t,x) >= Marked_f'(t,g(x)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { g(A) >= A ; g(B) >= A ; g(B) >= B ; g(C) >= A ; g(C) >= B ; g(C) >= C ; foldf(x,nil) >= x ; foldf(x,cons(y,z)) >= f(foldf(x,z),y) ; f(t,x) >= f'(t,g(x)) ; f'(triple(a,b,c),A) >= f''(foldf(triple(cons(A,a),nil,c),b)) ; f'(triple(a,b,c),B) >= f(triple(a,b,c),A) ; f'(triple(a,b,c),C) >= triple(a,b,cons(C,c)) ; f''(triple(a,b,c)) >= foldf(triple(a,b,nil),c) ; Marked_f''(triple(a,b,c)) >= Marked_foldf(triple(a,b,nil),c) ; Marked_foldf(x,cons(y,z)) >= Marked_foldf(x,z) ; Marked_foldf(x,cons(y,z)) >= Marked_f(foldf(x,z),y) ; Marked_f'(triple(a,b,c),A) >= Marked_f''(foldf(triple(cons(A,a),nil,c),b)) ; Marked_f'(triple(a,b,c),A) >= Marked_foldf(triple(cons(A,a),nil,c),b) ; Marked_f(t,x) >= Marked_f'(t,g(x)) ; } + Disjunctions:{ { Marked_f''(triple(a,b,c)) > Marked_foldf(triple(a,b,nil),c) ; } { Marked_foldf(x,cons(y,z)) > Marked_foldf(x,z) ; } { Marked_foldf(x,cons(y,z)) > Marked_f(foldf(x,z),y) ; } { Marked_f'(triple(a,b,c),A) > Marked_f''(foldf(triple(cons(A,a),nil,c),b)) ; } { Marked_f'(triple(a,b,c),A) > Marked_foldf(triple(cons(A,a),nil,c),b) ; } { Marked_f(t,x) > Marked_f'(t,g(x)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: g(A) >= A constraint: g(B) >= A constraint: g(B) >= B constraint: g(C) >= A constraint: g(C) >= B constraint: g(C) >= C constraint: foldf(x,nil) >= x constraint: foldf(x,cons(y,z)) >= f(foldf(x,z),y) constraint: f(t,x) >= f'(t,g(x)) constraint: f'(triple(a,b,c),A) >= f''(foldf(triple(cons(A,a),nil,c),b)) constraint: f'(triple(a,b,c),B) >= f(triple(a,b,c),A) constraint: f'(triple(a,b,c),C) >= triple(a,b,cons(C,c)) constraint: f''(triple(a,b,c)) >= foldf(triple(a,b,nil),c) constraint: Marked_f''(triple(a,b,c)) >= Marked_foldf(triple(a,b,nil),c) constraint: Marked_foldf(x,cons(y,z)) >= Marked_foldf(x,z) constraint: Marked_foldf(x,cons(y,z)) >= Marked_f(foldf(x,z),y) constraint: Marked_f'(triple(a,b,c),A) >= Marked_f''(foldf(triple(cons(A,a), nil,c),b)) constraint: Marked_f'(triple(a,b,c),A) >= Marked_foldf(triple(cons(A,a),nil,c), b) constraint: Marked_f(t,x) >= Marked_f'(t,g(x)) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] g(A) -> A [2] g(B) -> A [3] g(B) -> B [4] g(C) -> A [5] g(C) -> B [6] g(C) -> C [7] foldf(x,nil) -> x [8] foldf(x,cons(y,z)) -> f(foldf(x,z),y) [9] f(t,x) -> f'(t,g(x)) [10] f'(triple(a,b,c),C) -> triple(a,b,cons(C,c)) [11] f'(triple(a,b,c),B) -> f(triple(a,b,c),A) [12] f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b)) [13] f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ A ] () = 0; [ f' ] (X0,X1) = 2*X1 + 1*X0; [ foldf ] (X0,X1) = 1*X1 + 1*X0; [ Marked_foldf ] (X0,X1) = 2*X1 + 2*X0; [ B ] () = 2; [ f'' ] (X0) = 1*X0; [ f ] (X0,X1) = 2*X1 + 1*X0; [ Marked_f ] (X0,X1) = 1*X1 + 2*X0; [ g ] (X0) = 1*X0; [ triple ] (X0,X1,X2) = 1*X2 + 2*X1; [ nil ] () = 0; [ Marked_f' ] (X0,X1) = 1*X1 + 2*X0; [ C ] () = 2; [ Marked_f'' ] (X0) = 2*X0; [ cons ] (X0,X1) = 1*X1 + 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ A ] () = 0; [ f' ] (X0,X1) = 1*X0 + 2; [ foldf ] (X0,X1) = 1*X1 + 1*X0; [ Marked_foldf ] (X0,X1) = 2*X1 + 2*X0; [ B ] () = 0; [ f'' ] (X0) = 1*X0; [ f ] (X0,X1) = 1*X0 + 2; [ Marked_f ] (X0,X1) = 2*X0; [ g ] (X0) = 0; [ triple ] (X0,X1,X2) = 1*X2 + 2*X1; [ nil ] () = 0; [ Marked_f' ] (X0,X1) = 2*X0; [ C ] () = 0; [ Marked_f'' ] (X0) = 2*X0; [ cons ] (X0,X1) = 1*X1 + 2; removing [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} ]} ]} Cime worked for 0.280801 seconds (real time) Cime Exit Status: 0