- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] a__from(X) -> cons(mark(X),from(s(X))) [2] a__2ndspos(0,Z) -> rnil [3] a__2ndspos(s(N),cons(X,Z)) -> a__2ndspos(s(mark(N)),cons2(X,mark(Z))) [4] a__2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z))) [5] a__2ndsneg(0,Z) -> rnil [6] a__2ndsneg(s(N),cons(X,Z)) -> a__2ndsneg(s(mark(N)),cons2(X,mark(Z))) [7] a__2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z))) [8] a__pi(X) -> a__2ndspos(mark(X),a__from(0)) [9] a__plus(0,Y) -> mark(Y) [10] a__plus(s(X),Y) -> s(a__plus(mark(X),mark(Y))) [11] a__times(0,Y) -> 0 [12] a__times(s(X),Y) -> a__plus(mark(Y),a__times(mark(X),mark(Y))) [13] a__square(X) -> a__times(mark(X),mark(X)) [14] mark(from(X)) -> a__from(mark(X)) [15] mark(2ndspos(X1,X2)) -> a__2ndspos(mark(X1),mark(X2)) [16] mark(2ndsneg(X1,X2)) -> a__2ndsneg(mark(X1),mark(X2)) [17] mark(pi(X)) -> a__pi(mark(X)) [18] mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) [19] mark(times(X1,X2)) -> a__times(mark(X1),mark(X2)) [20] mark(square(X)) -> a__square(mark(X)) [21] mark(0) -> 0 [22] mark(s(X)) -> s(mark(X)) [23] mark(posrecip(X)) -> posrecip(mark(X)) [24] mark(negrecip(X)) -> negrecip(mark(X)) [25] mark(nil) -> nil [26] mark(cons(X1,X2)) -> cons(mark(X1),X2) [27] mark(cons2(X1,X2)) -> cons2(X1,mark(X2)) [28] mark(rnil) -> rnil [29] mark(rcons(X1,X2)) -> rcons(mark(X1),mark(X2)) [30] a__from(X) -> from(X) [31] a__2ndspos(X1,X2) -> 2ndspos(X1,X2) [32] a__2ndsneg(X1,X2) -> 2ndsneg(X1,X2) [33] a__pi(X) -> pi(X) [34] a__plus(X1,X2) -> plus(X1,X2) [35] a__times(X1,X2) -> times(X1,X2) [36] a__square(X) -> square(X) 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: { mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(from(X)) >= a__from(mark(X)) ; mark(s(X)) >= s(mark(X)) ; mark(rnil) >= rnil ; mark(0) >= 0 ; mark(cons2(X1,X2)) >= cons2(X1,mark(X2)) ; mark(rcons(X1,X2)) >= rcons(mark(X1),mark(X2)) ; mark(posrecip(X)) >= posrecip(mark(X)) ; mark(negrecip(X)) >= negrecip(mark(X)) ; mark(2ndspos(X1,X2)) >= a__2ndspos(mark(X1),mark(X2)) ; mark(2ndsneg(X1,X2)) >= a__2ndsneg(mark(X1),mark(X2)) ; mark(pi(X)) >= a__pi(mark(X)) ; mark(plus(X1,X2)) >= a__plus(mark(X1),mark(X2)) ; mark(times(X1,X2)) >= a__times(mark(X1),mark(X2)) ; mark(square(X)) >= a__square(mark(X)) ; mark(nil) >= nil ; a__from(X) >= cons(mark(X),from(s(X))) ; a__from(X) >= from(X) ; a__2ndspos(s(N),cons(X,Z)) >= a__2ndspos(s(mark(N)),cons2(X,mark(Z))) ; a__2ndspos(s(N),cons2(X,cons(Y,Z))) >= rcons(posrecip(mark(Y)), a__2ndsneg(mark(N),mark(Z))) ; a__2ndspos(0,Z) >= rnil ; a__2ndspos(X1,X2) >= 2ndspos(X1,X2) ; a__2ndsneg(s(N),cons(X,Z)) >= a__2ndsneg(s(mark(N)),cons2(X,mark(Z))) ; a__2ndsneg(s(N),cons2(X,cons(Y,Z))) >= rcons(negrecip(mark(Y)), a__2ndspos(mark(N),mark(Z))) ; a__2ndsneg(0,Z) >= rnil ; a__2ndsneg(X1,X2) >= 2ndsneg(X1,X2) ; a__pi(X) >= a__2ndspos(mark(X),a__from(0)) ; a__pi(X) >= pi(X) ; a__plus(s(X),Y) >= s(a__plus(mark(X),mark(Y))) ; a__plus(0,Y) >= mark(Y) ; a__plus(X1,X2) >= plus(X1,X2) ; a__times(s(X),Y) >= a__plus(mark(Y),a__times(mark(X),mark(Y))) ; a__times(0,Y) >= 0 ; a__times(X1,X2) >= times(X1,X2) ; a__square(X) >= a__times(mark(X),mark(X)) ; a__square(X) >= square(X) ; Marked_a__square(X) >= Marked_a__times(mark(X),mark(X)) ; Marked_a__square(X) >= Marked_mark(X) ; Marked_a__times(s(X),Y) >= Marked_a__times(mark(X),mark(Y)) ; Marked_a__times(s(X),Y) >= Marked_a__plus(mark(Y),a__times(mark(X),mark(Y))) ; Marked_a__times(s(X),Y) >= Marked_mark(X) ; Marked_a__times(s(X),Y) >= Marked_mark(Y) ; Marked_a__plus(s(X),Y) >= Marked_a__plus(mark(X),mark(Y)) ; Marked_a__plus(s(X),Y) >= Marked_mark(X) ; Marked_a__plus(s(X),Y) >= Marked_mark(Y) ; Marked_a__plus(0,Y) >= Marked_mark(Y) ; Marked_a__pi(X) >= Marked_a__2ndspos(mark(X),a__from(0)) ; Marked_a__pi(X) >= Marked_a__from(0) ; Marked_a__pi(X) >= Marked_mark(X) ; Marked_a__2ndsneg(s(N),cons(X,Z)) >= Marked_a__2ndsneg(s(mark(N)), cons2(X,mark(Z))) ; Marked_a__2ndsneg(s(N),cons(X,Z)) >= Marked_mark(N) ; Marked_a__2ndsneg(s(N),cons(X,Z)) >= Marked_mark(Z) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) >= Marked_a__2ndspos(mark(N), mark(Z)) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) >= Marked_mark(N) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) >= Marked_mark(Y) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) >= Marked_mark(Z) ; Marked_a__2ndspos(s(N),cons(X,Z)) >= Marked_a__2ndspos(s(mark(N)), cons2(X,mark(Z))) ; Marked_a__2ndspos(s(N),cons(X,Z)) >= Marked_mark(N) ; Marked_a__2ndspos(s(N),cons(X,Z)) >= Marked_mark(Z) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) >= Marked_a__2ndsneg(mark(N), mark(Z)) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) >= Marked_mark(N) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) >= Marked_mark(Y) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) >= Marked_mark(Z) ; Marked_a__from(X) >= Marked_mark(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(from(X)) >= Marked_a__from(mark(X)) ; Marked_mark(from(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(cons2(X1,X2)) >= Marked_mark(X2) ; Marked_mark(rcons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(rcons(X1,X2)) >= Marked_mark(X2) ; Marked_mark(posrecip(X)) >= Marked_mark(X) ; Marked_mark(negrecip(X)) >= Marked_mark(X) ; Marked_mark(2ndspos(X1,X2)) >= Marked_a__2ndspos(mark(X1),mark(X2)) ; Marked_mark(2ndspos(X1,X2)) >= Marked_mark(X1) ; Marked_mark(2ndspos(X1,X2)) >= Marked_mark(X2) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_a__2ndsneg(mark(X1),mark(X2)) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_mark(X1) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_mark(X2) ; Marked_mark(pi(X)) >= Marked_a__pi(mark(X)) ; Marked_mark(pi(X)) >= Marked_mark(X) ; Marked_mark(plus(X1,X2)) >= Marked_a__plus(mark(X1),mark(X2)) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X1) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X2) ; Marked_mark(times(X1,X2)) >= Marked_a__times(mark(X1),mark(X2)) ; Marked_mark(times(X1,X2)) >= Marked_mark(X1) ; Marked_mark(times(X1,X2)) >= Marked_mark(X2) ; Marked_mark(square(X)) >= Marked_a__square(mark(X)) ; Marked_mark(square(X)) >= Marked_mark(X) ; } + Disjunctions:{ { Marked_a__square(X) > Marked_a__times(mark(X),mark(X)) ; } { Marked_a__square(X) > Marked_mark(X) ; } { Marked_a__times(s(X),Y) > Marked_a__times(mark(X),mark(Y)) ; } { Marked_a__times(s(X),Y) > Marked_a__plus(mark(Y),a__times(mark(X),mark(Y))) ; } { Marked_a__times(s(X),Y) > Marked_mark(X) ; } { Marked_a__times(s(X),Y) > Marked_mark(Y) ; } { Marked_a__plus(s(X),Y) > Marked_a__plus(mark(X),mark(Y)) ; } { Marked_a__plus(s(X),Y) > Marked_mark(X) ; } { Marked_a__plus(s(X),Y) > Marked_mark(Y) ; } { Marked_a__plus(0,Y) > Marked_mark(Y) ; } { Marked_a__pi(X) > Marked_a__2ndspos(mark(X),a__from(0)) ; } { Marked_a__pi(X) > Marked_a__from(0) ; } { Marked_a__pi(X) > Marked_mark(X) ; } { Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_a__2ndsneg(s(mark(N)), cons2(X,mark(Z))) ; } { Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_mark(N) ; } { Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_mark(Z) ; } { Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_a__2ndspos(mark(N), mark(Z)) ; } { Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(N) ; } { Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Y) ; } { Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Z) ; } { Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_a__2ndspos(s(mark(N)), cons2(X,mark(Z))) ; } { Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_mark(N) ; } { Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_mark(Z) ; } { Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_a__2ndsneg(mark(N), mark(Z)) ; } { Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(N) ; } { Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Y) ; } { Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Z) ; } { Marked_a__from(X) > Marked_mark(X) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(from(X)) > Marked_a__from(mark(X)) ; } { Marked_mark(from(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(cons2(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(rcons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(rcons(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(posrecip(X)) > Marked_mark(X) ; } { Marked_mark(negrecip(X)) > Marked_mark(X) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_a__2ndspos(mark(X1),mark(X2)) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(2ndsneg(X1,X2)) > Marked_a__2ndsneg(mark(X1),mark(X2)) ; } { Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(pi(X)) > Marked_a__pi(mark(X)) ; } { Marked_mark(pi(X)) > Marked_mark(X) ; } { Marked_mark(plus(X1,X2)) > Marked_a__plus(mark(X1),mark(X2)) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(times(X1,X2)) > Marked_a__times(mark(X1),mark(X2)) ; } { Marked_mark(times(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(times(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(square(X)) > Marked_a__square(mark(X)) ; } { Marked_mark(square(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 === Time out for these parameters. === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (Simple graph) Found the following constraints: { mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(from(X)) >= a__from(mark(X)) ; mark(s(X)) >= s(mark(X)) ; mark(rnil) >= rnil ; mark(0) >= 0 ; mark(cons2(X1,X2)) >= cons2(X1,mark(X2)) ; mark(rcons(X1,X2)) >= rcons(mark(X1),mark(X2)) ; mark(posrecip(X)) >= posrecip(mark(X)) ; mark(negrecip(X)) >= negrecip(mark(X)) ; mark(2ndspos(X1,X2)) >= a__2ndspos(mark(X1),mark(X2)) ; mark(2ndsneg(X1,X2)) >= a__2ndsneg(mark(X1),mark(X2)) ; mark(pi(X)) >= a__pi(mark(X)) ; mark(plus(X1,X2)) >= a__plus(mark(X1),mark(X2)) ; mark(times(X1,X2)) >= a__times(mark(X1),mark(X2)) ; mark(square(X)) >= a__square(mark(X)) ; mark(nil) >= nil ; a__from(X) >= cons(mark(X),from(s(X))) ; a__from(X) >= from(X) ; a__2ndspos(s(N),cons(X,Z)) >= a__2ndspos(s(mark(N)),cons2(X,mark(Z))) ; a__2ndspos(s(N),cons2(X,cons(Y,Z))) >= rcons(posrecip(mark(Y)), a__2ndsneg(mark(N),mark(Z))) ; a__2ndspos(0,Z) >= rnil ; a__2ndspos(X1,X2) >= 2ndspos(X1,X2) ; a__2ndsneg(s(N),cons(X,Z)) >= a__2ndsneg(s(mark(N)),cons2(X,mark(Z))) ; a__2ndsneg(s(N),cons2(X,cons(Y,Z))) >= rcons(negrecip(mark(Y)), a__2ndspos(mark(N),mark(Z))) ; a__2ndsneg(0,Z) >= rnil ; a__2ndsneg(X1,X2) >= 2ndsneg(X1,X2) ; a__pi(X) >= a__2ndspos(mark(X),a__from(0)) ; a__pi(X) >= pi(X) ; a__plus(s(X),Y) >= s(a__plus(mark(X),mark(Y))) ; a__plus(0,Y) >= mark(Y) ; a__plus(X1,X2) >= plus(X1,X2) ; a__times(s(X),Y) >= a__plus(mark(Y),a__times(mark(X),mark(Y))) ; a__times(0,Y) >= 0 ; a__times(X1,X2) >= times(X1,X2) ; a__square(X) >= a__times(mark(X),mark(X)) ; a__square(X) >= square(X) ; Marked_a__square(X) >= Marked_a__times(mark(X),mark(X)) ; Marked_a__square(X) > Marked_mark(X) ; Marked_a__times(s(X),Y) > Marked_a__times(mark(X),mark(Y)) ; Marked_a__times(s(X),Y) >= Marked_a__plus(mark(Y),a__times(mark(X),mark(Y))) ; Marked_a__times(s(X),Y) > Marked_mark(X) ; Marked_a__times(s(X),Y) > Marked_mark(Y) ; Marked_a__plus(s(X),Y) > Marked_a__plus(mark(X),mark(Y)) ; Marked_a__plus(s(X),Y) > Marked_mark(X) ; Marked_a__plus(s(X),Y) > Marked_mark(Y) ; Marked_a__plus(0,Y) > Marked_mark(Y) ; Marked_a__pi(X) >= Marked_a__2ndspos(mark(X),a__from(0)) ; Marked_a__pi(X) >= Marked_a__from(0) ; Marked_a__pi(X) > Marked_mark(X) ; Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_a__2ndsneg(s(mark(N)), cons2(X,mark(Z))) ; Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_mark(N) ; Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_mark(Z) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_a__2ndspos(mark(N), mark(Z)) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(N) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Y) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Z) ; Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_a__2ndspos(s(mark(N)), cons2(X,mark(Z))) ; Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_mark(N) ; Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_mark(Z) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_a__2ndsneg(mark(N), mark(Z)) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(N) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Y) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Z) ; Marked_a__from(X) > Marked_mark(X) ; Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; Marked_mark(from(X)) > Marked_a__from(mark(X)) ; Marked_mark(from(X)) > Marked_mark(X) ; Marked_mark(s(X)) > Marked_mark(X) ; Marked_mark(cons2(X1,X2)) > Marked_mark(X2) ; Marked_mark(rcons(X1,X2)) > Marked_mark(X1) ; Marked_mark(rcons(X1,X2)) > Marked_mark(X2) ; Marked_mark(posrecip(X)) > Marked_mark(X) ; Marked_mark(negrecip(X)) > Marked_mark(X) ; Marked_mark(2ndspos(X1,X2)) >= Marked_a__2ndspos(mark(X1),mark(X2)) ; Marked_mark(2ndspos(X1,X2)) > Marked_mark(X1) ; Marked_mark(2ndspos(X1,X2)) > Marked_mark(X2) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_a__2ndsneg(mark(X1),mark(X2)) ; Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X1) ; Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X2) ; Marked_mark(pi(X)) >= Marked_a__pi(mark(X)) ; Marked_mark(pi(X)) > Marked_mark(X) ; Marked_mark(plus(X1,X2)) >= Marked_a__plus(mark(X1),mark(X2)) ; Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; Marked_mark(times(X1,X2)) >= Marked_a__times(mark(X1),mark(X2)) ; Marked_mark(times(X1,X2)) > Marked_mark(X1) ; Marked_mark(times(X1,X2)) > Marked_mark(X2) ; Marked_mark(square(X)) >= Marked_a__square(mark(X)) ; Marked_mark(square(X)) > Marked_mark(X) ; } APPLY CRITERIA (SOLVE_ORD) Trying to solve the following constraints: { mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(from(X)) >= a__from(mark(X)) ; mark(s(X)) >= s(mark(X)) ; mark(rnil) >= rnil ; mark(0) >= 0 ; mark(cons2(X1,X2)) >= cons2(X1,mark(X2)) ; mark(rcons(X1,X2)) >= rcons(mark(X1),mark(X2)) ; mark(posrecip(X)) >= posrecip(mark(X)) ; mark(negrecip(X)) >= negrecip(mark(X)) ; mark(2ndspos(X1,X2)) >= a__2ndspos(mark(X1),mark(X2)) ; mark(2ndsneg(X1,X2)) >= a__2ndsneg(mark(X1),mark(X2)) ; mark(pi(X)) >= a__pi(mark(X)) ; mark(plus(X1,X2)) >= a__plus(mark(X1),mark(X2)) ; mark(times(X1,X2)) >= a__times(mark(X1),mark(X2)) ; mark(square(X)) >= a__square(mark(X)) ; mark(nil) >= nil ; a__from(X) >= cons(mark(X),from(s(X))) ; a__from(X) >= from(X) ; a__2ndspos(s(N),cons(X,Z)) >= a__2ndspos(s(mark(N)),cons2(X,mark(Z))) ; a__2ndspos(s(N),cons2(X,cons(Y,Z))) >= rcons(posrecip(mark(Y)), a__2ndsneg(mark(N),mark(Z))) ; a__2ndspos(0,Z) >= rnil ; a__2ndspos(X1,X2) >= 2ndspos(X1,X2) ; a__2ndsneg(s(N),cons(X,Z)) >= a__2ndsneg(s(mark(N)),cons2(X,mark(Z))) ; a__2ndsneg(s(N),cons2(X,cons(Y,Z))) >= rcons(negrecip(mark(Y)), a__2ndspos(mark(N),mark(Z))) ; a__2ndsneg(0,Z) >= rnil ; a__2ndsneg(X1,X2) >= 2ndsneg(X1,X2) ; a__pi(X) >= a__2ndspos(mark(X),a__from(0)) ; a__pi(X) >= pi(X) ; a__plus(s(X),Y) >= s(a__plus(mark(X),mark(Y))) ; a__plus(0,Y) >= mark(Y) ; a__plus(X1,X2) >= plus(X1,X2) ; a__times(s(X),Y) >= a__plus(mark(Y),a__times(mark(X),mark(Y))) ; a__times(0,Y) >= 0 ; a__times(X1,X2) >= times(X1,X2) ; a__square(X) >= a__times(mark(X),mark(X)) ; a__square(X) >= square(X) ; Marked_a__square(X) >= Marked_a__times(mark(X),mark(X)) ; Marked_a__square(X) > Marked_mark(X) ; Marked_a__times(s(X),Y) > Marked_a__times(mark(X),mark(Y)) ; Marked_a__times(s(X),Y) >= Marked_a__plus(mark(Y),a__times(mark(X),mark(Y))) ; Marked_a__times(s(X),Y) > Marked_mark(X) ; Marked_a__times(s(X),Y) > Marked_mark(Y) ; Marked_a__plus(s(X),Y) > Marked_a__plus(mark(X),mark(Y)) ; Marked_a__plus(s(X),Y) > Marked_mark(X) ; Marked_a__plus(s(X),Y) > Marked_mark(Y) ; Marked_a__plus(0,Y) > Marked_mark(Y) ; Marked_a__pi(X) >= Marked_a__2ndspos(mark(X),a__from(0)) ; Marked_a__pi(X) >= Marked_a__from(0) ; Marked_a__pi(X) > Marked_mark(X) ; Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_a__2ndsneg(s(mark(N)), cons2(X,mark(Z))) ; Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_mark(N) ; Marked_a__2ndsneg(s(N),cons(X,Z)) > Marked_mark(Z) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_a__2ndspos(mark(N), mark(Z)) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(N) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Y) ; Marked_a__2ndsneg(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Z) ; Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_a__2ndspos(s(mark(N)), cons2(X,mark(Z))) ; Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_mark(N) ; Marked_a__2ndspos(s(N),cons(X,Z)) > Marked_mark(Z) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_a__2ndsneg(mark(N), mark(Z)) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(N) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Y) ; Marked_a__2ndspos(s(N),cons2(X,cons(Y,Z))) > Marked_mark(Z) ; Marked_a__from(X) > Marked_mark(X) ; Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; Marked_mark(from(X)) > Marked_a__from(mark(X)) ; Marked_mark(from(X)) > Marked_mark(X) ; Marked_mark(s(X)) > Marked_mark(X) ; Marked_mark(cons2(X1,X2)) > Marked_mark(X2) ; Marked_mark(rcons(X1,X2)) > Marked_mark(X1) ; Marked_mark(rcons(X1,X2)) > Marked_mark(X2) ; Marked_mark(posrecip(X)) > Marked_mark(X) ; Marked_mark(negrecip(X)) > Marked_mark(X) ; Marked_mark(2ndspos(X1,X2)) >= Marked_a__2ndspos(mark(X1),mark(X2)) ; Marked_mark(2ndspos(X1,X2)) > Marked_mark(X1) ; Marked_mark(2ndspos(X1,X2)) > Marked_mark(X2) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_a__2ndsneg(mark(X1),mark(X2)) ; Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X1) ; Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X2) ; Marked_mark(pi(X)) >= Marked_a__pi(mark(X)) ; Marked_mark(pi(X)) > Marked_mark(X) ; Marked_mark(plus(X1,X2)) >= Marked_a__plus(mark(X1),mark(X2)) ; Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; Marked_mark(times(X1,X2)) >= Marked_a__times(mark(X1),mark(X2)) ; Marked_mark(times(X1,X2)) > Marked_mark(X1) ; Marked_mark(times(X1,X2)) > Marked_mark(X2) ; Marked_mark(square(X)) >= Marked_a__square(mark(X)) ; Marked_mark(square(X)) > Marked_mark(X) ; } + Disjunctions:{ } === 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 === Time out for these parameters. === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 66.869362 seconds (real time) Cime Exit Status: 0