- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] t(N) -> cs(r(q(N)),nt(ns(N))) [2] q(0) -> 0 [3] q(s(X)) -> s(p(q(X),d(X))) [4] d(0) -> 0 [5] d(s(X)) -> s(s(d(X))) [6] p(0,X) -> X [7] p(X,0) -> X [8] p(s(X),s(Y)) -> s(s(p(X,Y))) [9] f(0,X) -> nil [10] f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) [11] t(X) -> nt(X) [12] s(X) -> ns(X) [13] f(X1,X2) -> nf(X1,X2) [14] a(nt(X)) -> t(a(X)) [15] a(ns(X)) -> s(a(X)) [16] a(nf(X1,X2)) -> f(a(X1),a(X2)) [17] a(X) -> X Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 4 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> } { --> } { --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { q(0) >= 0 ; q(s(X)) >= s(p(q(X),d(X))) ; t(N) >= cs(r(q(N)),nt(ns(N))) ; t(X) >= nt(X) ; s(X) >= ns(X) ; p(0,X) >= X ; p(s(X),s(Y)) >= s(s(p(X,Y))) ; p(X,0) >= X ; d(0) >= 0 ; d(s(X)) >= s(s(d(X))) ; f(0,X) >= nil ; f(s(X),cs(Y,Z)) >= cs(Y,nf(X,a(Z))) ; f(X1,X2) >= nf(X1,X2) ; a(nt(X)) >= t(a(X)) ; a(ns(X)) >= s(a(X)) ; a(nf(X1,X2)) >= f(a(X1),a(X2)) ; a(X) >= X ; Marked_a(nt(X)) >= Marked_a(X) ; Marked_a(ns(X)) >= Marked_a(X) ; Marked_a(nf(X1,X2)) >= Marked_a(X1) ; Marked_a(nf(X1,X2)) >= Marked_a(X2) ; Marked_a(nf(X1,X2)) >= Marked_f(a(X1),a(X2)) ; Marked_f(s(X),cs(Y,Z)) >= Marked_a(Z) ; } + Disjunctions:{ { Marked_a(nt(X)) > Marked_a(X) ; } { Marked_a(ns(X)) > Marked_a(X) ; } { Marked_a(nf(X1,X2)) > Marked_a(X1) ; } { Marked_a(nf(X1,X2)) > Marked_a(X2) ; } { Marked_a(nf(X1,X2)) > Marked_f(a(X1),a(X2)) ; } { Marked_f(s(X),cs(Y,Z)) > Marked_a(Z) ; } } === 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: q(0) >= 0 constraint: q(s(X)) >= s(p(q(X),d(X))) constraint: t(N) >= cs(r(q(N)),nt(ns(N))) constraint: t(X) >= nt(X) constraint: s(X) >= ns(X) constraint: p(0,X) >= X constraint: p(s(X),s(Y)) >= s(s(p(X,Y))) constraint: p(X,0) >= X constraint: d(0) >= 0 constraint: d(s(X)) >= s(s(d(X))) constraint: f(0,X) >= nil constraint: f(s(X),cs(Y,Z)) >= cs(Y,nf(X,a(Z))) constraint: f(X1,X2) >= nf(X1,X2) constraint: a(nt(X)) >= t(a(X)) constraint: a(ns(X)) >= s(a(X)) constraint: a(nf(X1,X2)) >= f(a(X1),a(X2)) constraint: a(X) >= X constraint: Marked_a(nt(X)) >= Marked_a(X) constraint: Marked_a(ns(X)) >= Marked_a(X) constraint: Marked_a(nf(X1,X2)) >= Marked_a(X1) constraint: Marked_a(nf(X1,X2)) >= Marked_a(X2) constraint: Marked_a(nf(X1,X2)) >= Marked_f(a(X1),a(X2)) constraint: Marked_f(s(X),cs(Y,Z)) >= Marked_a(Z) APPLY CRITERIA (Subterm criterion) ST: Marked_q -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_p -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_d -> 1 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { q(0) >= 0 ; q(s(X)) >= s(p(q(X),d(X))) ; t(N) >= cs(r(q(N)),nt(ns(N))) ; t(X) >= nt(X) ; s(X) >= ns(X) ; p(0,X) >= X ; p(s(X),s(Y)) >= s(s(p(X,Y))) ; p(X,0) >= X ; d(0) >= 0 ; d(s(X)) >= s(s(d(X))) ; f(0,X) >= nil ; f(s(X),cs(Y,Z)) >= cs(Y,nf(X,a(Z))) ; f(X1,X2) >= nf(X1,X2) ; a(nt(X)) >= t(a(X)) ; a(ns(X)) >= s(a(X)) ; a(nf(X1,X2)) >= f(a(X1),a(X2)) ; a(X) >= X ; Marked_a(ns(X)) >= Marked_a(X) ; Marked_a(nf(X1,X2)) >= Marked_a(X1) ; Marked_a(nf(X1,X2)) >= Marked_a(X2) ; Marked_a(nf(X1,X2)) >= Marked_f(a(X1),a(X2)) ; Marked_f(s(X),cs(Y,Z)) >= Marked_a(Z) ; } + Disjunctions:{ { Marked_a(ns(X)) > Marked_a(X) ; } { Marked_a(nf(X1,X2)) > Marked_a(X1) ; } { Marked_a(nf(X1,X2)) > Marked_a(X2) ; } { Marked_a(nf(X1,X2)) > Marked_f(a(X1),a(X2)) ; } { Marked_f(s(X),cs(Y,Z)) > Marked_a(Z) ; } } === 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: q(0) >= 0 constraint: q(s(X)) >= s(p(q(X),d(X))) constraint: t(N) >= cs(r(q(N)),nt(ns(N))) constraint: t(X) >= nt(X) constraint: s(X) >= ns(X) constraint: p(0,X) >= X constraint: p(s(X),s(Y)) >= s(s(p(X,Y))) constraint: p(X,0) >= X constraint: d(0) >= 0 constraint: d(s(X)) >= s(s(d(X))) constraint: f(0,X) >= nil constraint: f(s(X),cs(Y,Z)) >= cs(Y,nf(X,a(Z))) constraint: f(X1,X2) >= nf(X1,X2) constraint: a(nt(X)) >= t(a(X)) constraint: a(ns(X)) >= s(a(X)) constraint: a(nf(X1,X2)) >= f(a(X1),a(X2)) constraint: a(X) >= X constraint: Marked_a(ns(X)) >= Marked_a(X) constraint: Marked_a(nf(X1,X2)) >= Marked_a(X1) constraint: Marked_a(nf(X1,X2)) >= Marked_a(X2) constraint: Marked_a(nf(X1,X2)) >= Marked_f(a(X1),a(X2)) constraint: Marked_f(s(X),cs(Y,Z)) >= Marked_a(Z) APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Subterm criterion) ST: Marked_a -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] t(N) -> cs(r(q(N)),nt(ns(N))) [2] q(0) -> 0 [3] q(s(X)) -> s(p(q(X),d(X))) [4] d(0) -> 0 [5] d(s(X)) -> s(s(d(X))) [6] p(0,X) -> X [7] p(X,0) -> X [8] p(s(X),s(Y)) -> s(s(p(X,Y))) [9] f(0,X) -> nil [10] f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) [11] t(X) -> nt(X) [12] s(X) -> ns(X) [13] f(X1,X2) -> nf(X1,X2) [14] a(nt(X)) -> t(a(X)) [15] a(ns(X)) -> s(a(X)) [16] a(nf(X1,X2)) -> f(a(X1),a(X2)) [17] a(X) -> X , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ cs ] (X0,X1) = 1*X1; [ p ] (X0,X1) = 2*X1 + 2*X0; [ ns ] (X0) = 1*X0; [ nf ] (X0,X1) = 1*X1 + 1*X0; [ q ] (X0) = 0; [ nil ] () = 0; [ 0 ] () = 0; [ Marked_a ] (X0) = 2*X0; [ r ] (X0) = 0; [ d ] (X0) = 0; [ t ] (X0) = 1*X0 + 2; [ a ] (X0) = 1*X0; [ nt ] (X0) = 1*X0 + 2; [ f ] (X0,X1) = 1*X1 + 1*X0; [ s ] (X0) = 1*X0; [ Marked_f ] (X0,X1) = 2*X1; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ cs ] (X0,X1) = 1*X1; [ p ] (X0,X1) = 1*X1 + 1*X0; [ ns ] (X0) = 1*X0; [ nf ] (X0,X1) = 1*X1 + 2*X0 + 2; [ q ] (X0) = 0; [ nil ] () = 2; [ 0 ] () = 0; [ Marked_a ] (X0) = 2*X0; [ r ] (X0) = 0; [ d ] (X0) = 0; [ t ] (X0) = 0; [ a ] (X0) = 1*X0; [ nt ] (X0) = 0; [ f ] (X0,X1) = 1*X1 + 2*X0 + 2; [ s ] (X0) = 1*X0; [ Marked_f ] (X0,X1) = 2*X1 + 2*X0 + 2; removing < Marked_a(nf(X1,X2)),Marked_a(X1)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 0.192558 seconds (real time) Cime Exit Status: 0