- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N))) [2] a__sqr(0) -> 0 [3] a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)),a__dbl(mark(X)))) [4] a__dbl(0) -> 0 [5] a__dbl(s(X)) -> s(s(a__dbl(mark(X)))) [6] a__add(0,X) -> mark(X) [7] a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) [8] a__first(0,X) -> nil [9] a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) [10] a__half(0) -> 0 [11] a__half(s(0)) -> 0 [12] a__half(s(s(X))) -> s(a__half(mark(X))) [13] a__half(dbl(X)) -> mark(X) [14] mark(terms(X)) -> a__terms(mark(X)) [15] mark(sqr(X)) -> a__sqr(mark(X)) [16] mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) [17] mark(dbl(X)) -> a__dbl(mark(X)) [18] mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) [19] mark(half(X)) -> a__half(mark(X)) [20] mark(cons(X1,X2)) -> cons(mark(X1),X2) [21] mark(recip(X)) -> recip(mark(X)) [22] mark(s(X)) -> s(mark(X)) [23] mark(0) -> 0 [24] mark(nil) -> nil [25] a__terms(X) -> terms(X) [26] a__sqr(X) -> sqr(X) [27] a__add(X1,X2) -> add(X1,X2) [28] a__dbl(X) -> dbl(X) [29] a__first(X1,X2) -> first(X1,X2) [30] a__half(X) -> half(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__sqr(s(X)) >= s(a__add(a__sqr(mark(X)),a__dbl(mark(X)))) ; a__sqr(0) >= 0 ; a__sqr(X) >= sqr(X) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(recip(X)) >= recip(mark(X)) ; mark(terms(X)) >= a__terms(mark(X)) ; mark(s(X)) >= s(mark(X)) ; mark(0) >= 0 ; mark(nil) >= nil ; mark(first(X1,X2)) >= a__first(mark(X1),mark(X2)) ; mark(dbl(X)) >= a__dbl(mark(X)) ; mark(sqr(X)) >= a__sqr(mark(X)) ; mark(add(X1,X2)) >= a__add(mark(X1),mark(X2)) ; mark(half(X)) >= a__half(mark(X)) ; a__terms(N) >= cons(recip(a__sqr(mark(N))),terms(s(N))) ; a__terms(X) >= terms(X) ; a__add(s(X),Y) >= s(a__add(mark(X),mark(Y))) ; a__add(0,X) >= mark(X) ; a__add(X1,X2) >= add(X1,X2) ; a__dbl(s(X)) >= s(s(a__dbl(mark(X)))) ; a__dbl(0) >= 0 ; a__dbl(X) >= dbl(X) ; a__first(s(X),cons(Y,Z)) >= cons(mark(Y),first(X,Z)) ; a__first(0,X) >= nil ; a__first(X1,X2) >= first(X1,X2) ; a__half(s(s(X))) >= s(a__half(mark(X))) ; a__half(s(0)) >= 0 ; a__half(0) >= 0 ; a__half(dbl(X)) >= mark(X) ; a__half(X) >= half(X) ; Marked_a__half(s(s(X))) >= Marked_a__half(mark(X)) ; Marked_a__half(s(s(X))) >= Marked_mark(X) ; Marked_a__half(dbl(X)) >= Marked_mark(X) ; Marked_a__first(s(X),cons(Y,Z)) >= Marked_mark(Y) ; Marked_a__dbl(s(X)) >= Marked_a__dbl(mark(X)) ; Marked_a__dbl(s(X)) >= Marked_mark(X) ; Marked_a__add(s(X),Y) >= Marked_a__add(mark(X),mark(Y)) ; Marked_a__add(s(X),Y) >= Marked_mark(X) ; Marked_a__add(s(X),Y) >= Marked_mark(Y) ; Marked_a__add(0,X) >= Marked_mark(X) ; Marked_a__sqr(s(X)) >= Marked_a__dbl(mark(X)) ; Marked_a__sqr(s(X)) >= Marked_a__add(a__sqr(mark(X)),a__dbl(mark(X))) ; Marked_a__sqr(s(X)) >= Marked_a__sqr(mark(X)) ; Marked_a__sqr(s(X)) >= Marked_mark(X) ; Marked_a__terms(N) >= Marked_a__sqr(mark(N)) ; Marked_a__terms(N) >= Marked_mark(N) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(recip(X)) >= Marked_mark(X) ; Marked_mark(terms(X)) >= Marked_a__terms(mark(X)) ; Marked_mark(terms(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(first(X1,X2)) >= Marked_a__first(mark(X1),mark(X2)) ; Marked_mark(first(X1,X2)) >= Marked_mark(X1) ; Marked_mark(first(X1,X2)) >= Marked_mark(X2) ; Marked_mark(dbl(X)) >= Marked_a__dbl(mark(X)) ; Marked_mark(dbl(X)) >= Marked_mark(X) ; Marked_mark(sqr(X)) >= Marked_a__sqr(mark(X)) ; Marked_mark(sqr(X)) >= Marked_mark(X) ; Marked_mark(add(X1,X2)) >= Marked_a__add(mark(X1),mark(X2)) ; Marked_mark(add(X1,X2)) >= Marked_mark(X1) ; Marked_mark(add(X1,X2)) >= Marked_mark(X2) ; Marked_mark(half(X)) >= Marked_a__half(mark(X)) ; Marked_mark(half(X)) >= Marked_mark(X) ; } + Disjunctions:{ { Marked_a__half(s(s(X))) > Marked_a__half(mark(X)) ; } { Marked_a__half(s(s(X))) > Marked_mark(X) ; } { Marked_a__half(dbl(X)) > Marked_mark(X) ; } { Marked_a__first(s(X),cons(Y,Z)) > Marked_mark(Y) ; } { Marked_a__dbl(s(X)) > Marked_a__dbl(mark(X)) ; } { Marked_a__dbl(s(X)) > Marked_mark(X) ; } { Marked_a__add(s(X),Y) > Marked_a__add(mark(X),mark(Y)) ; } { Marked_a__add(s(X),Y) > Marked_mark(X) ; } { Marked_a__add(s(X),Y) > Marked_mark(Y) ; } { Marked_a__add(0,X) > Marked_mark(X) ; } { Marked_a__sqr(s(X)) > Marked_a__dbl(mark(X)) ; } { Marked_a__sqr(s(X)) > Marked_a__add(a__sqr(mark(X)),a__dbl(mark(X))) ; } { Marked_a__sqr(s(X)) > Marked_a__sqr(mark(X)) ; } { Marked_a__sqr(s(X)) > Marked_mark(X) ; } { Marked_a__terms(N) > Marked_a__sqr(mark(N)) ; } { Marked_a__terms(N) > Marked_mark(N) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(recip(X)) > Marked_mark(X) ; } { Marked_mark(terms(X)) > Marked_a__terms(mark(X)) ; } { Marked_mark(terms(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(first(X1,X2)) > Marked_a__first(mark(X1),mark(X2)) ; } { Marked_mark(first(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(first(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(dbl(X)) > Marked_a__dbl(mark(X)) ; } { Marked_mark(dbl(X)) > Marked_mark(X) ; } { Marked_mark(sqr(X)) > Marked_a__sqr(mark(X)) ; } { Marked_mark(sqr(X)) > Marked_mark(X) ; } { Marked_mark(add(X1,X2)) > Marked_a__add(mark(X1),mark(X2)) ; } { Marked_mark(add(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(add(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(half(X)) > Marked_a__half(mark(X)) ; } { Marked_mark(half(X)) > Marked_mark(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 === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === STOPING TIMER virtual === constraint: a__sqr(s(X)) >= s(a__add(a__sqr(mark(X)),a__dbl(mark(X)))) constraint: a__sqr(0) >= 0 constraint: a__sqr(X) >= sqr(X) constraint: mark(cons(X1,X2)) >= cons(mark(X1),X2) constraint: mark(recip(X)) >= recip(mark(X)) constraint: mark(terms(X)) >= a__terms(mark(X)) constraint: mark(s(X)) >= s(mark(X)) constraint: mark(0) >= 0 constraint: mark(nil) >= nil constraint: mark(first(X1,X2)) >= a__first(mark(X1),mark(X2)) constraint: mark(dbl(X)) >= a__dbl(mark(X)) constraint: mark(sqr(X)) >= a__sqr(mark(X)) constraint: mark(add(X1,X2)) >= a__add(mark(X1),mark(X2)) constraint: mark(half(X)) >= a__half(mark(X)) constraint: a__terms(N) >= cons(recip(a__sqr(mark(N))),terms(s(N))) constraint: a__terms(X) >= terms(X) constraint: a__add(s(X),Y) >= s(a__add(mark(X),mark(Y))) constraint: a__add(0,X) >= mark(X) constraint: a__add(X1,X2) >= add(X1,X2) constraint: a__dbl(s(X)) >= s(s(a__dbl(mark(X)))) constraint: a__dbl(0) >= 0 constraint: a__dbl(X) >= dbl(X) constraint: a__first(s(X),cons(Y,Z)) >= cons(mark(Y),first(X,Z)) constraint: a__first(0,X) >= nil constraint: a__first(X1,X2) >= first(X1,X2) constraint: a__half(s(s(X))) >= s(a__half(mark(X))) constraint: a__half(s(0)) >= 0 constraint: a__half(0) >= 0 constraint: a__half(dbl(X)) >= mark(X) constraint: a__half(X) >= half(X) constraint: Marked_a__half(s(s(X))) >= Marked_a__half(mark(X)) constraint: Marked_a__half(s(s(X))) >= Marked_mark(X) constraint: Marked_a__half(dbl(X)) >= Marked_mark(X) constraint: Marked_a__first(s(X),cons(Y,Z)) >= Marked_mark(Y) constraint: Marked_a__dbl(s(X)) >= Marked_a__dbl(mark(X)) constraint: Marked_a__dbl(s(X)) >= Marked_mark(X) constraint: Marked_a__add(s(X),Y) >= Marked_a__add(mark(X),mark(Y)) constraint: Marked_a__add(s(X),Y) >= Marked_mark(X) constraint: Marked_a__add(s(X),Y) >= Marked_mark(Y) constraint: Marked_a__add(0,X) >= Marked_mark(X) constraint: Marked_a__sqr(s(X)) >= Marked_a__dbl(mark(X)) constraint: Marked_a__sqr(s(X)) >= Marked_a__add(a__sqr(mark(X)), a__dbl(mark(X))) constraint: Marked_a__sqr(s(X)) >= Marked_a__sqr(mark(X)) constraint: Marked_a__sqr(s(X)) >= Marked_mark(X) constraint: Marked_a__terms(N) >= Marked_a__sqr(mark(N)) constraint: Marked_a__terms(N) >= Marked_mark(N) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(recip(X)) >= Marked_mark(X) constraint: Marked_mark(terms(X)) >= Marked_a__terms(mark(X)) constraint: Marked_mark(terms(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(first(X1,X2)) >= Marked_a__first(mark(X1),mark(X2)) constraint: Marked_mark(first(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(first(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(dbl(X)) >= Marked_a__dbl(mark(X)) constraint: Marked_mark(dbl(X)) >= Marked_mark(X) constraint: Marked_mark(sqr(X)) >= Marked_a__sqr(mark(X)) constraint: Marked_mark(sqr(X)) >= Marked_mark(X) constraint: Marked_mark(add(X1,X2)) >= Marked_a__add(mark(X1),mark(X2)) constraint: Marked_mark(add(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(add(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(half(X)) >= Marked_a__half(mark(X)) constraint: Marked_mark(half(X)) >= Marked_mark(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__sqr(s(X)) >= s(a__add(a__sqr(mark(X)),a__dbl(mark(X)))) ; a__sqr(0) >= 0 ; a__sqr(X) >= sqr(X) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(recip(X)) >= recip(mark(X)) ; mark(terms(X)) >= a__terms(mark(X)) ; mark(s(X)) >= s(mark(X)) ; mark(0) >= 0 ; mark(nil) >= nil ; mark(first(X1,X2)) >= a__first(mark(X1),mark(X2)) ; mark(dbl(X)) >= a__dbl(mark(X)) ; mark(sqr(X)) >= a__sqr(mark(X)) ; mark(add(X1,X2)) >= a__add(mark(X1),mark(X2)) ; mark(half(X)) >= a__half(mark(X)) ; a__terms(N) >= cons(recip(a__sqr(mark(N))),terms(s(N))) ; a__terms(X) >= terms(X) ; a__add(s(X),Y) >= s(a__add(mark(X),mark(Y))) ; a__add(0,X) >= mark(X) ; a__add(X1,X2) >= add(X1,X2) ; a__dbl(s(X)) >= s(s(a__dbl(mark(X)))) ; a__dbl(0) >= 0 ; a__dbl(X) >= dbl(X) ; a__first(s(X),cons(Y,Z)) >= cons(mark(Y),first(X,Z)) ; a__first(0,X) >= nil ; a__first(X1,X2) >= first(X1,X2) ; a__half(s(s(X))) >= s(a__half(mark(X))) ; a__half(s(0)) >= 0 ; a__half(0) >= 0 ; a__half(dbl(X)) >= mark(X) ; a__half(X) >= half(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } } === 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: a__sqr(s(X)) >= s(a__add(a__sqr(mark(X)),a__dbl(mark(X)))) constraint: a__sqr(0) >= 0 constraint: a__sqr(X) >= sqr(X) constraint: mark(cons(X1,X2)) >= cons(mark(X1),X2) constraint: mark(recip(X)) >= recip(mark(X)) constraint: mark(terms(X)) >= a__terms(mark(X)) constraint: mark(s(X)) >= s(mark(X)) constraint: mark(0) >= 0 constraint: mark(nil) >= nil constraint: mark(first(X1,X2)) >= a__first(mark(X1),mark(X2)) constraint: mark(dbl(X)) >= a__dbl(mark(X)) constraint: mark(sqr(X)) >= a__sqr(mark(X)) constraint: mark(add(X1,X2)) >= a__add(mark(X1),mark(X2)) constraint: mark(half(X)) >= a__half(mark(X)) constraint: a__terms(N) >= cons(recip(a__sqr(mark(N))),terms(s(N))) constraint: a__terms(X) >= terms(X) constraint: a__add(s(X),Y) >= s(a__add(mark(X),mark(Y))) constraint: a__add(0,X) >= mark(X) constraint: a__add(X1,X2) >= add(X1,X2) constraint: a__dbl(s(X)) >= s(s(a__dbl(mark(X)))) constraint: a__dbl(0) >= 0 constraint: a__dbl(X) >= dbl(X) constraint: a__first(s(X),cons(Y,Z)) >= cons(mark(Y),first(X,Z)) constraint: a__first(0,X) >= nil constraint: a__first(X1,X2) >= first(X1,X2) constraint: a__half(s(s(X))) >= s(a__half(mark(X))) constraint: a__half(s(0)) >= 0 constraint: a__half(0) >= 0 constraint: a__half(dbl(X)) >= mark(X) constraint: a__half(X) >= half(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N))) [2] a__sqr(0) -> 0 [3] a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)),a__dbl(mark(X)))) [4] a__dbl(0) -> 0 [5] a__dbl(s(X)) -> s(s(a__dbl(mark(X)))) [6] a__add(0,X) -> mark(X) [7] a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) [8] a__first(0,X) -> nil [9] a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) [10] a__half(0) -> 0 [11] a__half(s(0)) -> 0 [12] a__half(s(s(X))) -> s(a__half(mark(X))) [13] a__half(dbl(X)) -> mark(X) [14] mark(terms(X)) -> a__terms(mark(X)) [15] mark(sqr(X)) -> a__sqr(mark(X)) [16] mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) [17] mark(dbl(X)) -> a__dbl(mark(X)) [18] mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) [19] mark(half(X)) -> a__half(mark(X)) [20] mark(cons(X1,X2)) -> cons(mark(X1),X2) [21] mark(recip(X)) -> recip(mark(X)) [22] mark(s(X)) -> s(mark(X)) [23] mark(0) -> 0 [24] mark(nil) -> nil [25] a__terms(X) -> terms(X) [26] a__sqr(X) -> sqr(X) [27] a__add(X1,X2) -> add(X1,X2) [28] a__dbl(X) -> dbl(X) [29] a__first(X1,X2) -> first(X1,X2) [30] a__half(X) -> half(X) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using RPO with AFS = AFS: cons -> 0Marked_mark -> 0mark -> 0 and precedence: prec (All symbols are Lex.): { recip < terms ; recip < a__terms ; a__sqr < terms ; a__sqr > s ; a__sqr < a__terms ; a__sqr > a__add ; a__sqr > a__dbl ; a__sqr > dbl ; a__sqr = sqr ; a__sqr > add ; a__sqr > Marked_a__dbl ; a__sqr > Marked_a__add ; a__sqr = Marked_a__sqr ; a__sqr < Marked_a__terms ; terms > recip ; terms > a__sqr ; terms > s ; terms = a__terms ; terms > a__add ; terms > a__dbl ; terms > dbl ; terms > sqr ; terms > add ; terms > Marked_a__dbl ; terms > Marked_a__add ; terms > Marked_a__sqr ; terms > Marked_a__terms ; s < a__sqr ; s < terms ; s < a__terms ; s < a__add ; s < a__dbl ; s < a__half ; s < dbl ; s < sqr ; s < add ; s < half ; s < Marked_a__sqr ; s < Marked_a__terms ; a__terms > recip ; a__terms > a__sqr ; a__terms = terms ; a__terms > s ; a__terms > a__add ; a__terms > a__dbl ; a__terms > dbl ; a__terms > sqr ; a__terms > add ; a__terms > Marked_a__dbl ; a__terms > Marked_a__add ; a__terms > Marked_a__sqr ; a__terms > Marked_a__terms ; a__add < a__sqr ; a__add < terms ; a__add > s ; a__add < a__terms ; a__add < sqr ; a__add = add ; a__add > Marked_a__add ; a__add < Marked_a__sqr ; a__add < Marked_a__terms ; a__dbl < a__sqr ; a__dbl < terms ; a__dbl > s ; a__dbl < a__terms ; a__dbl = dbl ; a__dbl < sqr ; a__dbl > Marked_a__dbl ; a__dbl < Marked_a__sqr ; a__dbl < Marked_a__terms ; nil < a__first ; nil < first ; a__first > nil ; a__first = first ; a__first > Marked_a__first ; first > nil ; first = a__first ; first > Marked_a__first ; a__half > s ; a__half = half ; a__half > Marked_a__half ; dbl < a__sqr ; dbl < terms ; dbl > s ; dbl < a__terms ; dbl = a__dbl ; dbl < sqr ; dbl > Marked_a__dbl ; dbl < Marked_a__sqr ; dbl < Marked_a__terms ; sqr = a__sqr ; sqr < terms ; sqr > s ; sqr < a__terms ; sqr > a__add ; sqr > a__dbl ; sqr > dbl ; sqr > add ; sqr > Marked_a__dbl ; sqr > Marked_a__add ; sqr = Marked_a__sqr ; sqr < Marked_a__terms ; add < a__sqr ; add < terms ; add > s ; add < a__terms ; add = a__add ; add < sqr ; add > Marked_a__add ; add < Marked_a__sqr ; add < Marked_a__terms ; half > s ; half = a__half ; half > Marked_a__half ; Marked_a__half < a__half ; Marked_a__half < half ; Marked_a__first < a__first ; Marked_a__first < first ; Marked_a__dbl < a__sqr ; Marked_a__dbl < terms ; Marked_a__dbl < a__terms ; Marked_a__dbl < a__dbl ; Marked_a__dbl < dbl ; Marked_a__dbl < sqr ; Marked_a__dbl < Marked_a__sqr ; Marked_a__dbl < Marked_a__terms ; Marked_a__add < a__sqr ; Marked_a__add < terms ; Marked_a__add < a__terms ; Marked_a__add < a__add ; Marked_a__add < sqr ; Marked_a__add < add ; Marked_a__add < Marked_a__sqr ; Marked_a__add < Marked_a__terms ; Marked_a__sqr = a__sqr ; Marked_a__sqr < terms ; Marked_a__sqr > s ; Marked_a__sqr < a__terms ; Marked_a__sqr > a__add ; Marked_a__sqr > a__dbl ; Marked_a__sqr > dbl ; Marked_a__sqr = sqr ; Marked_a__sqr > add ; Marked_a__sqr > Marked_a__dbl ; Marked_a__sqr > Marked_a__add ; Marked_a__sqr < Marked_a__terms ; Marked_a__terms > a__sqr ; Marked_a__terms < terms ; Marked_a__terms > s ; Marked_a__terms < a__terms ; Marked_a__terms > a__add ; Marked_a__terms > a__dbl ; Marked_a__terms > dbl ; Marked_a__terms > sqr ; Marked_a__terms > add ; Marked_a__terms > Marked_a__dbl ; Marked_a__terms > Marked_a__add ; Marked_a__terms > Marked_a__sqr ; } removing < Marked_a__add(s(X),Y),Marked_mark(X)>< Marked_a__first(s(X),cons(Y,Z)),Marked_mark(Y)>< Marked_mark(add(X1,X2)),Marked_mark(X2)>< Marked_mark(dbl(X)),Marked_mark(X)>< Marked_mark(first(X1,X2)),Marked_mark(X1)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ cons ] (X0,X1) = 1 + 2*X0 + 0; [ add ] (X0,X1) = 1*X1 + 0; [ a__add ] (X0,X1) = 1*X1 + 0; [ Marked_mark ] (X0) = 3*X0 + 0; [ terms ] (X0) = 1 + 0; [ first ] (X0,X1) = 1*X1 + 0; [ a__sqr ] (X0) = 0; [ nil ] () = 0; [ a__terms ] (X0) = 1 + 0; [ dbl ] (X0) = 1*X0 + 0; [ recip ] (X0) = 0; [ half ] (X0) = 1*X0 + 0; [ a__dbl ] (X0) = 1*X0 + 0; [ s ] (X0) = 0; [ a__half ] (X0) = 1*X0 + 0; [ mark ] (X0) = 1*X0 + 0; [ a__first ] (X0,X1) = 1*X1 + 0; [ 0 ] () = 0; [ sqr ] (X0) = 0; ]} ]} ]} ]} ]} Cime worked for 19.017318 seconds (real time) Cime Exit Status: 0