- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] from(X) -> cons(X,n__from(s(X))) [2] 2ndspos(0,Z) -> rnil [3] 2ndspos(s(N),cons(X,n__cons(Y,Z))) -> rcons(posrecip(activate(Y)),2ndsneg(N,activate(Z))) [4] 2ndsneg(0,Z) -> rnil [5] 2ndsneg(s(N),cons(X,n__cons(Y,Z))) -> rcons(negrecip(activate(Y)),2ndspos(N,activate(Z))) [6] pi(X) -> 2ndspos(X,from(0)) [7] plus(0,Y) -> Y [8] plus(s(X),Y) -> s(plus(X,Y)) [9] times(0,Y) -> 0 [10] times(s(X),Y) -> plus(Y,times(X,Y)) [11] square(X) -> times(X,X) [12] from(X) -> n__from(X) [13] cons(X1,X2) -> n__cons(X1,X2) [14] activate(n__from(X)) -> from(X) [15] activate(n__cons(X1,X2)) -> cons(X1,X2) [16] activate(X) -> X Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 3 components: { --> --> } { --> } { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; from(X) >= cons(X,n__from(s(X))) ; from(X) >= n__from(X) ; 2ndspos(s(N),cons(X,n__cons(Y,Z))) >= rcons(posrecip(activate(Y)), 2ndsneg(N,activate(Z))) ; 2ndspos(0,Z) >= rnil ; activate(n__from(X)) >= from(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(X) >= X ; 2ndsneg(s(N),cons(X,n__cons(Y,Z))) >= rcons(negrecip(activate(Y)), 2ndspos(N,activate(Z))) ; 2ndsneg(0,Z) >= rnil ; pi(X) >= 2ndspos(X,from(0)) ; plus(s(X),Y) >= s(plus(X,Y)) ; plus(0,Y) >= Y ; times(s(X),Y) >= plus(Y,times(X,Y)) ; times(0,Y) >= 0 ; square(X) >= times(X,X) ; Marked_2ndspos(s(N),cons(X,n__cons(Y,Z))) >= Marked_2ndsneg(N,activate(Z)) ; Marked_2ndsneg(s(N),cons(X,n__cons(Y,Z))) >= Marked_2ndspos(N,activate(Z)) ; } + Disjunctions:{ { Marked_2ndspos(s(N),cons(X,n__cons(Y,Z))) > Marked_2ndsneg(N,activate(Z)) ; } { Marked_2ndsneg(s(N),cons(X,n__cons(Y,Z))) > Marked_2ndspos(N,activate(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: cons(X1,X2) >= n__cons(X1,X2) constraint: from(X) >= cons(X,n__from(s(X))) constraint: from(X) >= n__from(X) constraint: 2ndspos(s(N),cons(X,n__cons(Y,Z))) >= rcons(posrecip(activate(Y)), 2ndsneg(N,activate(Z))) constraint: 2ndspos(0,Z) >= rnil constraint: activate(n__from(X)) >= from(X) constraint: activate(n__cons(X1,X2)) >= cons(X1,X2) constraint: activate(X) >= X constraint: 2ndsneg(s(N),cons(X,n__cons(Y,Z))) >= rcons(negrecip(activate(Y)), 2ndspos(N,activate(Z))) constraint: 2ndsneg(0,Z) >= rnil constraint: pi(X) >= 2ndspos(X,from(0)) constraint: plus(s(X),Y) >= s(plus(X,Y)) constraint: plus(0,Y) >= Y constraint: times(s(X),Y) >= plus(Y,times(X,Y)) constraint: times(0,Y) >= 0 constraint: square(X) >= times(X,X) constraint: Marked_2ndspos(s(N),cons(X,n__cons(Y,Z))) >= Marked_2ndsneg( N,activate(Z)) constraint: Marked_2ndsneg(s(N),cons(X,n__cons(Y,Z))) >= Marked_2ndspos( N,activate(Z)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; from(X) >= cons(X,n__from(s(X))) ; from(X) >= n__from(X) ; 2ndspos(s(N),cons(X,n__cons(Y,Z))) >= rcons(posrecip(activate(Y)), 2ndsneg(N,activate(Z))) ; 2ndspos(0,Z) >= rnil ; activate(n__from(X)) >= from(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(X) >= X ; 2ndsneg(s(N),cons(X,n__cons(Y,Z))) >= rcons(negrecip(activate(Y)), 2ndspos(N,activate(Z))) ; 2ndsneg(0,Z) >= rnil ; pi(X) >= 2ndspos(X,from(0)) ; plus(s(X),Y) >= s(plus(X,Y)) ; plus(0,Y) >= Y ; times(s(X),Y) >= plus(Y,times(X,Y)) ; times(0,Y) >= 0 ; square(X) >= times(X,X) ; Marked_times(s(X),Y) >= Marked_times(X,Y) ; } + Disjunctions:{ { Marked_times(s(X),Y) > Marked_times(X,Y) ; } } === 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: cons(X1,X2) >= n__cons(X1,X2) constraint: from(X) >= cons(X,n__from(s(X))) constraint: from(X) >= n__from(X) constraint: 2ndspos(s(N),cons(X,n__cons(Y,Z))) >= rcons(posrecip(activate(Y)), 2ndsneg(N,activate(Z))) constraint: 2ndspos(0,Z) >= rnil constraint: activate(n__from(X)) >= from(X) constraint: activate(n__cons(X1,X2)) >= cons(X1,X2) constraint: activate(X) >= X constraint: 2ndsneg(s(N),cons(X,n__cons(Y,Z))) >= rcons(negrecip(activate(Y)), 2ndspos(N,activate(Z))) constraint: 2ndsneg(0,Z) >= rnil constraint: pi(X) >= 2ndspos(X,from(0)) constraint: plus(s(X),Y) >= s(plus(X,Y)) constraint: plus(0,Y) >= Y constraint: times(s(X),Y) >= plus(Y,times(X,Y)) constraint: times(0,Y) >= 0 constraint: square(X) >= times(X,X) constraint: Marked_times(s(X),Y) >= Marked_times(X,Y) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; from(X) >= cons(X,n__from(s(X))) ; from(X) >= n__from(X) ; 2ndspos(s(N),cons(X,n__cons(Y,Z))) >= rcons(posrecip(activate(Y)), 2ndsneg(N,activate(Z))) ; 2ndspos(0,Z) >= rnil ; activate(n__from(X)) >= from(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(X) >= X ; 2ndsneg(s(N),cons(X,n__cons(Y,Z))) >= rcons(negrecip(activate(Y)), 2ndspos(N,activate(Z))) ; 2ndsneg(0,Z) >= rnil ; pi(X) >= 2ndspos(X,from(0)) ; plus(s(X),Y) >= s(plus(X,Y)) ; plus(0,Y) >= Y ; times(s(X),Y) >= plus(Y,times(X,Y)) ; times(0,Y) >= 0 ; square(X) >= times(X,X) ; Marked_plus(s(X),Y) >= Marked_plus(X,Y) ; } + Disjunctions:{ { Marked_plus(s(X),Y) > Marked_plus(X,Y) ; } } === 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: cons(X1,X2) >= n__cons(X1,X2) constraint: from(X) >= cons(X,n__from(s(X))) constraint: from(X) >= n__from(X) constraint: 2ndspos(s(N),cons(X,n__cons(Y,Z))) >= rcons(posrecip(activate(Y)), 2ndsneg(N,activate(Z))) constraint: 2ndspos(0,Z) >= rnil constraint: activate(n__from(X)) >= from(X) constraint: activate(n__cons(X1,X2)) >= cons(X1,X2) constraint: activate(X) >= X constraint: 2ndsneg(s(N),cons(X,n__cons(Y,Z))) >= rcons(negrecip(activate(Y)), 2ndspos(N,activate(Z))) constraint: 2ndsneg(0,Z) >= rnil constraint: pi(X) >= 2ndspos(X,from(0)) constraint: plus(s(X),Y) >= s(plus(X,Y)) constraint: plus(0,Y) >= Y constraint: times(s(X),Y) >= plus(Y,times(X,Y)) constraint: times(0,Y) >= 0 constraint: square(X) >= times(X,X) constraint: Marked_plus(s(X),Y) >= Marked_plus(X,Y) 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] from(X) -> cons(X,n__from(s(X))) [2] 2ndspos(0,Z) -> rnil [3] 2ndspos(s(N),cons(X,n__cons(Y,Z))) -> rcons(posrecip(activate(Y)),2ndsneg(N,activate(Z))) [4] 2ndsneg(0,Z) -> rnil [5] 2ndsneg(s(N),cons(X,n__cons(Y,Z))) -> rcons(negrecip(activate(Y)),2ndspos(N,activate(Z))) [6] pi(X) -> 2ndspos(X,from(0)) [7] plus(0,Y) -> Y [8] plus(s(X),Y) -> s(plus(X,Y)) [9] times(0,Y) -> 0 [10] times(s(X),Y) -> plus(Y,times(X,Y)) [11] square(X) -> times(X,X) [12] from(X) -> n__from(X) [13] cons(X1,X2) -> n__cons(X1,X2) [14] activate(n__from(X)) -> from(X) [15] activate(n__cons(X1,X2)) -> cons(X1,X2) [16] activate(X) -> X , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ cons ] (X0,X1) = 1 + 2*X1 + 0; [ square ] (X0) = 1*X0 + 0; [ posrecip ] (X0) = 0; [ Marked_2ndspos ] (X0,X1) = 2*X1 + 0; [ rnil ] () = 0; [ negrecip ] (X0) = 0; [ s ] (X0) = 0; [ 2ndsneg ] (X0,X1) = 0; [ 0 ] () = 0; [ plus ] (X0,X1) = 1*X1 + 0; [ n__from ] (X0) = 1 + 0; [ activate ] (X0) = 3*X0 + 0; [ Marked_2ndsneg ] (X0,X1) = 2*X1 + 0; [ 2ndspos ] (X0,X1) = 2 + 0; [ pi ] (X0) = 3 + 1*X0 + 0; [ from ] (X0) = 3 + 0; [ n__cons ] (X0,X1) = 1 + 2*X1 + 0; [ rcons ] (X0,X1) = 0; [ times ] (X0,X1) = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: RPO with AFS = AFS: and precedence: prec (All symbols are Lex.): { cons < from ; cons < 2ndspos ; cons < activate ; cons < 2ndsneg ; cons > n__cons ; cons < pi ; n__from < from ; n__from < 2ndspos ; n__from < activate ; n__from < 2ndsneg ; n__from < pi ; s < from ; s < 2ndspos ; s < activate ; s < 2ndsneg ; s < pi ; s < plus ; s < times ; s < square ; from > cons ; from > n__from ; from > s ; from < 2ndspos ; from < activate ; from < 2ndsneg ; from > n__cons ; from < pi ; rnil < 2ndspos ; rnil < 2ndsneg ; rnil < pi ; 2ndspos > cons ; 2ndspos > n__from ; 2ndspos > s ; 2ndspos > from ; 2ndspos > rnil ; 2ndspos > rcons ; 2ndspos > posrecip ; 2ndspos > activate ; 2ndspos = 2ndsneg ; 2ndspos > n__cons ; 2ndspos > negrecip ; 2ndspos < pi ; 0 < pi ; rcons < 2ndspos ; rcons < 2ndsneg ; rcons < pi ; posrecip < 2ndspos ; posrecip < 2ndsneg ; posrecip < pi ; activate > cons ; activate > n__from ; activate > s ; activate > from ; activate < 2ndspos ; activate < 2ndsneg ; activate > n__cons ; activate < pi ; 2ndsneg > cons ; 2ndsneg > n__from ; 2ndsneg > s ; 2ndsneg > from ; 2ndsneg > rnil ; 2ndsneg = 2ndspos ; 2ndsneg > rcons ; 2ndsneg > posrecip ; 2ndsneg > activate ; 2ndsneg > n__cons ; 2ndsneg > negrecip ; 2ndsneg < pi ; n__cons < cons ; n__cons < from ; n__cons < 2ndspos ; n__cons < activate ; n__cons < 2ndsneg ; n__cons < pi ; negrecip < 2ndspos ; negrecip < 2ndsneg ; negrecip < pi ; pi > cons ; pi > n__from ; pi > s ; pi > from ; pi > rnil ; pi > 2ndspos ; pi > 0 ; pi > rcons ; pi > posrecip ; pi > activate ; pi > 2ndsneg ; pi > n__cons ; pi > negrecip ; plus > s ; plus < times ; plus < square ; times > s ; times > plus ; times < square ; square > s ; square > plus ; square > times ; } ]} { DP termination of: , CRITERION: ORD [ Solution found: RPO with AFS = AFS: and precedence: prec (All symbols are Lex.): { cons < from ; cons < 2ndspos ; cons < activate ; cons < 2ndsneg ; cons > n__cons ; cons < pi ; n__from < from ; n__from < 2ndspos ; n__from < activate ; n__from < 2ndsneg ; n__from < pi ; s < from ; s < 2ndspos ; s < activate ; s < 2ndsneg ; s < pi ; s < plus ; s < times ; s < square ; from > cons ; from > n__from ; from > s ; from < 2ndspos ; from < activate ; from < 2ndsneg ; from > n__cons ; from < pi ; rnil < 2ndspos ; rnil < 2ndsneg ; rnil < pi ; 2ndspos > cons ; 2ndspos > n__from ; 2ndspos > s ; 2ndspos > from ; 2ndspos > rnil ; 2ndspos > rcons ; 2ndspos > posrecip ; 2ndspos > activate ; 2ndspos = 2ndsneg ; 2ndspos > n__cons ; 2ndspos > negrecip ; 2ndspos < pi ; 0 < pi ; rcons < 2ndspos ; rcons < 2ndsneg ; rcons < pi ; posrecip < 2ndspos ; posrecip < 2ndsneg ; posrecip < pi ; activate > cons ; activate > n__from ; activate > s ; activate > from ; activate < 2ndspos ; activate < 2ndsneg ; activate > n__cons ; activate < pi ; 2ndsneg > cons ; 2ndsneg > n__from ; 2ndsneg > s ; 2ndsneg > from ; 2ndsneg > rnil ; 2ndsneg = 2ndspos ; 2ndsneg > rcons ; 2ndsneg > posrecip ; 2ndsneg > activate ; 2ndsneg > n__cons ; 2ndsneg > negrecip ; 2ndsneg < pi ; n__cons < cons ; n__cons < from ; n__cons < 2ndspos ; n__cons < activate ; n__cons < 2ndsneg ; n__cons < pi ; negrecip < 2ndspos ; negrecip < 2ndsneg ; negrecip < pi ; pi > cons ; pi > n__from ; pi > s ; pi > from ; pi > rnil ; pi > 2ndspos ; pi > 0 ; pi > rcons ; pi > posrecip ; pi > activate ; pi > 2ndsneg ; pi > n__cons ; pi > negrecip ; plus > s ; plus < times ; plus < square ; times > s ; times > plus ; times < square ; square > s ; square > plus ; square > times ; } ]} ]} ]} Cime worked for 0.294887 seconds (real time) Cime Exit Status: 0