- : 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] foldB(t,0) -> t [8] foldB(t,s(n)) -> f(foldB(t,n),B) [9] foldC(t,0) -> t [10] foldC(t,s(n)) -> f(foldC(t,n),C) [11] f(t,x) -> f'(t,g(x)) [12] f'(triple(a,b,c),C) -> triple(a,b,s(c)) [13] f'(triple(a,b,c),B) -> f(triple(a,b,c),A) [14] f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) [15] f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) [16] fold(t,x,0) -> t [17] fold(t,x,s(n)) -> f(fold(t,x,n),x) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 2 components: { --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_fold -> 3 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 ; foldB(t,0) >= t ; foldB(t,s(n)) >= f(foldB(t,n),B) ; f(t,x) >= f'(t,g(x)) ; foldC(t,0) >= t ; foldC(t,s(n)) >= f(foldC(t,n),C) ; f'(triple(a,b,c),A) >= f''(foldB(triple(s(a),0,c),b)) ; f'(triple(a,b,c),B) >= f(triple(a,b,c),A) ; f'(triple(a,b,c),C) >= triple(a,b,s(c)) ; f''(triple(a,b,c)) >= foldC(triple(a,b,0),c) ; fold(t,x,0) >= t ; fold(t,x,s(n)) >= f(fold(t,x,n),x) ; Marked_f(t,x) >= Marked_f'(t,g(x)) ; Marked_f''(triple(a,b,c)) >= Marked_foldC(triple(a,b,0),c) ; Marked_foldC(t,s(n)) >= Marked_f(foldC(t,n),C) ; Marked_foldC(t,s(n)) >= Marked_foldC(t,n) ; Marked_f'(triple(a,b,c),A) >= Marked_f''(foldB(triple(s(a),0,c),b)) ; Marked_f'(triple(a,b,c),A) >= Marked_foldB(triple(s(a),0,c),b) ; Marked_f'(triple(a,b,c),B) >= Marked_f(triple(a,b,c),A) ; Marked_foldB(t,s(n)) >= Marked_f(foldB(t,n),B) ; Marked_foldB(t,s(n)) >= Marked_foldB(t,n) ; } + Disjunctions:{ { Marked_f(t,x) > Marked_f'(t,g(x)) ; } { Marked_f''(triple(a,b,c)) > Marked_foldC(triple(a,b,0),c) ; } { Marked_foldC(t,s(n)) > Marked_f(foldC(t,n),C) ; } { Marked_foldC(t,s(n)) > Marked_foldC(t,n) ; } { Marked_f'(triple(a,b,c),A) > Marked_f''(foldB(triple(s(a),0,c),b)) ; } { Marked_f'(triple(a,b,c),A) > Marked_foldB(triple(s(a),0,c),b) ; } { Marked_f'(triple(a,b,c),B) > Marked_f(triple(a,b,c),A) ; } { Marked_foldB(t,s(n)) > Marked_f(foldB(t,n),B) ; } { Marked_foldB(t,s(n)) > Marked_foldB(t,n) ; } } === 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: foldB(t,0) >= t constraint: foldB(t,s(n)) >= f(foldB(t,n),B) constraint: f(t,x) >= f'(t,g(x)) constraint: foldC(t,0) >= t constraint: foldC(t,s(n)) >= f(foldC(t,n),C) constraint: f'(triple(a,b,c),A) >= f''(foldB(triple(s(a),0,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,s(c)) constraint: f''(triple(a,b,c)) >= foldC(triple(a,b,0),c) constraint: fold(t,x,0) >= t constraint: fold(t,x,s(n)) >= f(fold(t,x,n),x) constraint: Marked_f(t,x) >= Marked_f'(t,g(x)) constraint: Marked_f''(triple(a,b,c)) >= Marked_foldC(triple(a,b,0),c) constraint: Marked_foldC(t,s(n)) >= Marked_f(foldC(t,n),C) constraint: Marked_foldC(t,s(n)) >= Marked_foldC(t,n) constraint: Marked_f'(triple(a,b,c),A) >= Marked_f''(foldB(triple(s(a),0,c),b)) constraint: Marked_f'(triple(a,b,c),A) >= Marked_foldB(triple(s(a),0,c),b) constraint: Marked_f'(triple(a,b,c),B) >= Marked_f(triple(a,b,c),A) constraint: Marked_foldB(t,s(n)) >= Marked_f(foldB(t,n),B) constraint: Marked_foldB(t,s(n)) >= Marked_foldB(t,n) APPLY CRITERIA (Graph splitting) Found 0 components: 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 ; foldB(t,0) >= t ; foldB(t,s(n)) >= f(foldB(t,n),B) ; f(t,x) >= f'(t,g(x)) ; foldC(t,0) >= t ; foldC(t,s(n)) >= f(foldC(t,n),C) ; f'(triple(a,b,c),A) >= f''(foldB(triple(s(a),0,c),b)) ; f'(triple(a,b,c),B) >= f(triple(a,b,c),A) ; f'(triple(a,b,c),C) >= triple(a,b,s(c)) ; f''(triple(a,b,c)) >= foldC(triple(a,b,0),c) ; fold(t,x,0) >= t ; fold(t,x,s(n)) >= f(fold(t,x,n),x) ; Marked_f(t,x) >= Marked_f'(t,g(x)) ; Marked_f''(triple(a,b,c)) >= Marked_foldC(triple(a,b,0),c) ; Marked_foldC(t,s(n)) >= Marked_f(foldC(t,n),C) ; Marked_foldC(t,s(n)) >= Marked_foldC(t,n) ; Marked_f'(triple(a,b,c),A) >= Marked_f''(foldB(triple(s(a),0,c),b)) ; Marked_f'(triple(a,b,c),B) >= Marked_f(triple(a,b,c),A) ; } + Disjunctions:{ { Marked_f(t,x) > Marked_f'(t,g(x)) ; } { Marked_f''(triple(a,b,c)) > Marked_foldC(triple(a,b,0),c) ; } { Marked_foldC(t,s(n)) > Marked_f(foldC(t,n),C) ; } { Marked_foldC(t,s(n)) > Marked_foldC(t,n) ; } { Marked_f'(triple(a,b,c),A) > Marked_f''(foldB(triple(s(a),0,c),b)) ; } { Marked_f'(triple(a,b,c),B) > Marked_f(triple(a,b,c),A) ; } } === 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: foldB(t,0) >= t constraint: foldB(t,s(n)) >= f(foldB(t,n),B) constraint: f(t,x) >= f'(t,g(x)) constraint: foldC(t,0) >= t constraint: foldC(t,s(n)) >= f(foldC(t,n),C) constraint: f'(triple(a,b,c),A) >= f''(foldB(triple(s(a),0,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,s(c)) constraint: f''(triple(a,b,c)) >= foldC(triple(a,b,0),c) constraint: fold(t,x,0) >= t constraint: fold(t,x,s(n)) >= f(fold(t,x,n),x) constraint: Marked_f(t,x) >= Marked_f'(t,g(x)) constraint: Marked_f''(triple(a,b,c)) >= Marked_foldC(triple(a,b,0),c) constraint: Marked_foldC(t,s(n)) >= Marked_f(foldC(t,n),C) constraint: Marked_foldC(t,s(n)) >= Marked_foldC(t,n) constraint: Marked_f'(triple(a,b,c),A) >= Marked_f''(foldB(triple(s(a),0,c),b)) constraint: Marked_f'(triple(a,b,c),B) >= Marked_f(triple(a,b,c),A) 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 ; foldB(t,0) >= t ; foldB(t,s(n)) >= f(foldB(t,n),B) ; f(t,x) >= f'(t,g(x)) ; foldC(t,0) >= t ; foldC(t,s(n)) >= f(foldC(t,n),C) ; f'(triple(a,b,c),A) >= f''(foldB(triple(s(a),0,c),b)) ; f'(triple(a,b,c),B) >= f(triple(a,b,c),A) ; f'(triple(a,b,c),C) >= triple(a,b,s(c)) ; f''(triple(a,b,c)) >= foldC(triple(a,b,0),c) ; fold(t,x,0) >= t ; fold(t,x,s(n)) >= f(fold(t,x,n),x) ; Marked_f(t,x) >= Marked_f'(t,g(x)) ; Marked_f'(triple(a,b,c),B) >= Marked_f(triple(a,b,c),A) ; } + Disjunctions:{ { Marked_f(t,x) > Marked_f'(t,g(x)) ; } { Marked_f'(triple(a,b,c),B) > Marked_f(triple(a,b,c),A) ; } } === 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: foldB(t,0) >= t constraint: foldB(t,s(n)) >= f(foldB(t,n),B) constraint: f(t,x) >= f'(t,g(x)) constraint: foldC(t,0) >= t constraint: foldC(t,s(n)) >= f(foldC(t,n),C) constraint: f'(triple(a,b,c),A) >= f''(foldB(triple(s(a),0,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,s(c)) constraint: f''(triple(a,b,c)) >= foldC(triple(a,b,0),c) constraint: fold(t,x,0) >= t constraint: fold(t,x,s(n)) >= f(fold(t,x,n),x) constraint: Marked_f(t,x) >= Marked_f'(t,g(x)) constraint: Marked_f'(triple(a,b,c),B) >= Marked_f(triple(a,b,c),A) 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] foldB(t,0) -> t [8] foldB(t,s(n)) -> f(foldB(t,n),B) [9] foldC(t,0) -> t [10] foldC(t,s(n)) -> f(foldC(t,n),C) [11] f(t,x) -> f'(t,g(x)) [12] f'(triple(a,b,c),C) -> triple(a,b,s(c)) [13] f'(triple(a,b,c),B) -> f(triple(a,b,c),A) [14] f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) [15] f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) [16] fold(t,x,0) -> t [17] fold(t,x,s(n)) -> f(fold(t,x,n),x) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ A ] () = 0; [ Marked_foldC ] (X0,X1) = 1*X0 + 2; [ foldC ] (X0,X1) = 1*X0; [ foldB ] (X0,X1) = 2*X0; [ fold ] (X0,X1,X2) = 1*X2 + 3*X1 + 3*X0; [ B ] () = 0; [ Marked_foldB ] (X0,X1) = 1*X1 + 2*X0 + 2; [ triple ] (X0,X1,X2) = 1*X1; [ f ] (X0,X1) = 1*X0; [ Marked_f ] (X0,X1) = 1*X0 + 2; [ g ] (X0) = 0; [ Marked_f' ] (X0,X1) = 1*X0 + 2; [ f' ] (X0,X1) = 1*X0; [ 0 ] () = 0; [ C ] () = 0; [ f'' ] (X0) = 1*X0; [ s ] (X0) = 2*X0 + 2; [ Marked_f'' ] (X0) = 2*X0 + 2; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ A ] () = 0; [ Marked_foldC ] (X0,X1) = 1*X1 + 1*X0; [ foldC ] (X0,X1) = 1*X1 + 1*X0; [ foldB ] (X0,X1) = 1*X1 + 1*X0; [ fold ] (X0,X1,X2) = 1*X2 + 3*X1 + 3*X0; [ B ] () = 0; [ triple ] (X0,X1,X2) = 1*X2 + 2*X1; [ f ] (X0,X1) = 1*X0 + 1; [ Marked_f ] (X0,X1) = 1*X0; [ g ] (X0) = 0; [ Marked_f' ] (X0,X1) = 1*X0; [ f' ] (X0,X1) = 1*X0 + 1; [ 0 ] () = 0; [ C ] () = 0; [ f'' ] (X0) = 1*X0; [ s ] (X0) = 1*X0 + 1; [ Marked_f'' ] (X0) = 1*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ A ] () = 0; [ foldC ] (X0,X1) = 2*X0; [ foldB ] (X0,X1) = 2*X1 + 1*X0 + 2; [ fold ] (X0,X1,X2) = 2*X2 + 3*X1 + 3*X0 + 2; [ B ] () = 2; [ triple ] (X0,X1,X2) = 0; [ f ] (X0,X1) = 0; [ Marked_f ] (X0,X1) = 2*X1 + 2; [ g ] (X0) = 2*X0; [ Marked_f' ] (X0,X1) = 1*X1 + 2; [ f' ] (X0,X1) = 0; [ 0 ] () = 0; [ C ] () = 2; [ f'' ] (X0) = 0; [ s ] (X0) = 2; removing [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} ]} ]} ]} ]} Cime worked for 0.389357 seconds (real time) Cime Exit Status: 0