- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(from(X)) -> mark(cons(X,from(s(X)))) [2] active(2ndspos(0,Z)) -> mark(rnil) [3] active(2ndspos(s(N),cons(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) [4] active(2ndsneg(0,Z)) -> mark(rnil) [5] active(2ndsneg(s(N),cons(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) [6] active(pi(X)) -> mark(2ndspos(X,from(0))) [7] active(plus(0,Y)) -> mark(Y) [8] active(plus(s(X),Y)) -> mark(s(plus(X,Y))) [9] active(times(0,Y)) -> mark(0) [10] active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) [11] active(square(X)) -> mark(times(X,X)) [12] mark(from(X)) -> active(from(mark(X))) [13] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [14] mark(s(X)) -> active(s(mark(X))) [15] mark(2ndspos(X1,X2)) -> active(2ndspos(mark(X1),mark(X2))) [16] mark(0) -> active(0) [17] mark(rnil) -> active(rnil) [18] mark(rcons(X1,X2)) -> active(rcons(mark(X1),mark(X2))) [19] mark(posrecip(X)) -> active(posrecip(mark(X))) [20] mark(2ndsneg(X1,X2)) -> active(2ndsneg(mark(X1),mark(X2))) [21] mark(negrecip(X)) -> active(negrecip(mark(X))) [22] mark(pi(X)) -> active(pi(mark(X))) [23] mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) [24] mark(times(X1,X2)) -> active(times(mark(X1),mark(X2))) [25] mark(square(X)) -> active(square(mark(X))) [26] from(mark(X)) -> from(X) [27] from(active(X)) -> from(X) [28] cons(mark(X1),X2) -> cons(X1,X2) [29] cons(X1,mark(X2)) -> cons(X1,X2) [30] cons(active(X1),X2) -> cons(X1,X2) [31] cons(X1,active(X2)) -> cons(X1,X2) [32] s(mark(X)) -> s(X) [33] s(active(X)) -> s(X) [34] 2ndspos(mark(X1),X2) -> 2ndspos(X1,X2) [35] 2ndspos(X1,mark(X2)) -> 2ndspos(X1,X2) [36] 2ndspos(active(X1),X2) -> 2ndspos(X1,X2) [37] 2ndspos(X1,active(X2)) -> 2ndspos(X1,X2) [38] rcons(mark(X1),X2) -> rcons(X1,X2) [39] rcons(X1,mark(X2)) -> rcons(X1,X2) [40] rcons(active(X1),X2) -> rcons(X1,X2) [41] rcons(X1,active(X2)) -> rcons(X1,X2) [42] posrecip(mark(X)) -> posrecip(X) [43] posrecip(active(X)) -> posrecip(X) [44] 2ndsneg(mark(X1),X2) -> 2ndsneg(X1,X2) [45] 2ndsneg(X1,mark(X2)) -> 2ndsneg(X1,X2) [46] 2ndsneg(active(X1),X2) -> 2ndsneg(X1,X2) [47] 2ndsneg(X1,active(X2)) -> 2ndsneg(X1,X2) [48] negrecip(mark(X)) -> negrecip(X) [49] negrecip(active(X)) -> negrecip(X) [50] pi(mark(X)) -> pi(X) [51] pi(active(X)) -> pi(X) [52] plus(mark(X1),X2) -> plus(X1,X2) [53] plus(X1,mark(X2)) -> plus(X1,X2) [54] plus(active(X1),X2) -> plus(X1,X2) [55] plus(X1,active(X2)) -> plus(X1,X2) [56] times(mark(X1),X2) -> times(X1,X2) [57] times(X1,mark(X2)) -> times(X1,X2) [58] times(active(X1),X2) -> times(X1,X2) [59] times(X1,active(X2)) -> times(X1,X2) [60] square(mark(X)) -> square(X) [61] square(active(X)) -> square(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 13 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(from(X)) >= active(from(mark(X))) ; mark(s(X)) >= active(s(mark(X))) ; mark(rnil) >= active(rnil) ; mark(2ndspos(X1,X2)) >= active(2ndspos(mark(X1),mark(X2))) ; mark(0) >= active(0) ; mark(rcons(X1,X2)) >= active(rcons(mark(X1),mark(X2))) ; mark(posrecip(X)) >= active(posrecip(mark(X))) ; mark(2ndsneg(X1,X2)) >= active(2ndsneg(mark(X1),mark(X2))) ; mark(negrecip(X)) >= active(negrecip(mark(X))) ; mark(pi(X)) >= active(pi(mark(X))) ; mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) ; mark(times(X1,X2)) >= active(times(mark(X1),mark(X2))) ; mark(square(X)) >= active(square(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; from(mark(X)) >= from(X) ; from(active(X)) >= from(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; active(from(X)) >= mark(cons(X,from(s(X)))) ; active(2ndspos(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(negrecip(Y), 2ndspos(N,Z))) ; active(2ndsneg(0,Z)) >= mark(rnil) ; active(pi(X)) >= mark(2ndspos(X,from(0))) ; active(plus(s(X),Y)) >= mark(s(plus(X,Y))) ; active(plus(0,Y)) >= mark(Y) ; active(times(s(X),Y)) >= mark(plus(Y,times(X,Y))) ; active(times(0,Y)) >= mark(0) ; active(square(X)) >= mark(times(X,X)) ; 2ndspos(mark(X1),X2) >= 2ndspos(X1,X2) ; 2ndspos(active(X1),X2) >= 2ndspos(X1,X2) ; 2ndspos(X1,mark(X2)) >= 2ndspos(X1,X2) ; 2ndspos(X1,active(X2)) >= 2ndspos(X1,X2) ; rcons(mark(X1),X2) >= rcons(X1,X2) ; rcons(active(X1),X2) >= rcons(X1,X2) ; rcons(X1,mark(X2)) >= rcons(X1,X2) ; rcons(X1,active(X2)) >= rcons(X1,X2) ; posrecip(mark(X)) >= posrecip(X) ; posrecip(active(X)) >= posrecip(X) ; 2ndsneg(mark(X1),X2) >= 2ndsneg(X1,X2) ; 2ndsneg(active(X1),X2) >= 2ndsneg(X1,X2) ; 2ndsneg(X1,mark(X2)) >= 2ndsneg(X1,X2) ; 2ndsneg(X1,active(X2)) >= 2ndsneg(X1,X2) ; negrecip(mark(X)) >= negrecip(X) ; negrecip(active(X)) >= negrecip(X) ; pi(mark(X)) >= pi(X) ; pi(active(X)) >= pi(X) ; plus(mark(X1),X2) >= plus(X1,X2) ; plus(active(X1),X2) >= plus(X1,X2) ; plus(X1,mark(X2)) >= plus(X1,X2) ; plus(X1,active(X2)) >= plus(X1,X2) ; times(mark(X1),X2) >= times(X1,X2) ; times(active(X1),X2) >= times(X1,X2) ; times(X1,mark(X2)) >= times(X1,X2) ; times(X1,active(X2)) >= times(X1,X2) ; square(mark(X)) >= square(X) ; square(active(X)) >= square(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(from(X)) >= Marked_mark(X) ; Marked_mark(from(X)) >= Marked_active(from(mark(X))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(2ndspos(X1,X2)) >= Marked_mark(X1) ; Marked_mark(2ndspos(X1,X2)) >= Marked_mark(X2) ; Marked_mark(2ndspos(X1,X2)) >= Marked_active(2ndspos(mark(X1),mark(X2))) ; Marked_mark(rcons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(rcons(X1,X2)) >= Marked_mark(X2) ; Marked_mark(rcons(X1,X2)) >= Marked_active(rcons(mark(X1),mark(X2))) ; Marked_mark(posrecip(X)) >= Marked_mark(X) ; Marked_mark(posrecip(X)) >= Marked_active(posrecip(mark(X))) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_mark(X1) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_mark(X2) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_active(2ndsneg(mark(X1),mark(X2))) ; Marked_mark(negrecip(X)) >= Marked_mark(X) ; Marked_mark(negrecip(X)) >= Marked_active(negrecip(mark(X))) ; Marked_mark(pi(X)) >= Marked_mark(X) ; Marked_mark(pi(X)) >= Marked_active(pi(mark(X))) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X1) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X2) ; Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) ; Marked_mark(times(X1,X2)) >= Marked_mark(X1) ; Marked_mark(times(X1,X2)) >= Marked_mark(X2) ; Marked_mark(times(X1,X2)) >= Marked_active(times(mark(X1),mark(X2))) ; Marked_mark(square(X)) >= Marked_mark(X) ; Marked_mark(square(X)) >= Marked_active(square(mark(X))) ; Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) ; Marked_active(2ndspos(s(N),cons(X,cons(Y,Z)))) >= Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,cons(Y,Z)))) >= Marked_mark(rcons( negrecip( Y), 2ndspos(N,Z))) ; Marked_active(pi(X)) >= Marked_mark(2ndspos(X,from(0))) ; Marked_active(plus(s(X),Y)) >= Marked_mark(s(plus(X,Y))) ; Marked_active(plus(0,Y)) >= Marked_mark(Y) ; Marked_active(times(s(X),Y)) >= Marked_mark(plus(Y,times(X,Y))) ; Marked_active(square(X)) >= Marked_mark(times(X,X)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(from(X)) > Marked_mark(X) ; } { Marked_mark(from(X)) > Marked_active(from(mark(X))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_active(2ndspos(mark(X1),mark(X2))) ; } { Marked_mark(rcons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(rcons(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(rcons(X1,X2)) > Marked_active(rcons(mark(X1),mark(X2))) ; } { Marked_mark(posrecip(X)) > Marked_mark(X) ; } { Marked_mark(posrecip(X)) > Marked_active(posrecip(mark(X))) ; } { Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(2ndsneg(X1,X2)) > Marked_active(2ndsneg(mark(X1),mark(X2))) ; } { Marked_mark(negrecip(X)) > Marked_mark(X) ; } { Marked_mark(negrecip(X)) > Marked_active(negrecip(mark(X))) ; } { Marked_mark(pi(X)) > Marked_mark(X) ; } { Marked_mark(pi(X)) > Marked_active(pi(mark(X))) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(plus(X1,X2)) > Marked_active(plus(mark(X1),mark(X2))) ; } { Marked_mark(times(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(times(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(times(X1,X2)) > Marked_active(times(mark(X1),mark(X2))) ; } { Marked_mark(square(X)) > Marked_mark(X) ; } { Marked_mark(square(X)) > Marked_active(square(mark(X))) ; } { Marked_active(from(X)) > Marked_mark(cons(X,from(s(X)))) ; } { Marked_active(2ndspos(s(N),cons(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; } { Marked_active(2ndsneg(s(N),cons(X,cons(Y,Z)))) > Marked_mark(rcons( negrecip( Y), 2ndspos(N,Z))) ; } { Marked_active(pi(X)) > Marked_mark(2ndspos(X,from(0))) ; } { Marked_active(plus(s(X),Y)) > Marked_mark(s(plus(X,Y))) ; } { Marked_active(plus(0,Y)) > Marked_mark(Y) ; } { Marked_active(times(s(X),Y)) > Marked_mark(plus(Y,times(X,Y))) ; } { Marked_active(square(X)) > Marked_mark(times(X,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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(from(X)) >= active(from(mark(X))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(rnil) >= active(rnil) constraint: mark(2ndspos(X1,X2)) >= active(2ndspos(mark(X1),mark(X2))) constraint: mark(0) >= active(0) constraint: mark(rcons(X1,X2)) >= active(rcons(mark(X1),mark(X2))) constraint: mark(posrecip(X)) >= active(posrecip(mark(X))) constraint: mark(2ndsneg(X1,X2)) >= active(2ndsneg(mark(X1),mark(X2))) constraint: mark(negrecip(X)) >= active(negrecip(mark(X))) constraint: mark(pi(X)) >= active(pi(mark(X))) constraint: mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) constraint: mark(times(X1,X2)) >= active(times(mark(X1),mark(X2))) constraint: mark(square(X)) >= active(square(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: from(mark(X)) >= from(X) constraint: from(active(X)) >= from(X) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: active(from(X)) >= mark(cons(X,from(s(X)))) constraint: active(2ndspos(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) constraint: active(2ndspos(0,Z)) >= mark(rnil) constraint: active(2ndsneg(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(negrecip(Y), 2ndspos(N,Z))) constraint: active(2ndsneg(0,Z)) >= mark(rnil) constraint: active(pi(X)) >= mark(2ndspos(X,from(0))) constraint: active(plus(s(X),Y)) >= mark(s(plus(X,Y))) constraint: active(plus(0,Y)) >= mark(Y) constraint: active(times(s(X),Y)) >= mark(plus(Y,times(X,Y))) constraint: active(times(0,Y)) >= mark(0) constraint: active(square(X)) >= mark(times(X,X)) constraint: 2ndspos(mark(X1),X2) >= 2ndspos(X1,X2) constraint: 2ndspos(active(X1),X2) >= 2ndspos(X1,X2) constraint: 2ndspos(X1,mark(X2)) >= 2ndspos(X1,X2) constraint: 2ndspos(X1,active(X2)) >= 2ndspos(X1,X2) constraint: rcons(mark(X1),X2) >= rcons(X1,X2) constraint: rcons(active(X1),X2) >= rcons(X1,X2) constraint: rcons(X1,mark(X2)) >= rcons(X1,X2) constraint: rcons(X1,active(X2)) >= rcons(X1,X2) constraint: posrecip(mark(X)) >= posrecip(X) constraint: posrecip(active(X)) >= posrecip(X) constraint: 2ndsneg(mark(X1),X2) >= 2ndsneg(X1,X2) constraint: 2ndsneg(active(X1),X2) >= 2ndsneg(X1,X2) constraint: 2ndsneg(X1,mark(X2)) >= 2ndsneg(X1,X2) constraint: 2ndsneg(X1,active(X2)) >= 2ndsneg(X1,X2) constraint: negrecip(mark(X)) >= negrecip(X) constraint: negrecip(active(X)) >= negrecip(X) constraint: pi(mark(X)) >= pi(X) constraint: pi(active(X)) >= pi(X) constraint: plus(mark(X1),X2) >= plus(X1,X2) constraint: plus(active(X1),X2) >= plus(X1,X2) constraint: plus(X1,mark(X2)) >= plus(X1,X2) constraint: plus(X1,active(X2)) >= plus(X1,X2) constraint: times(mark(X1),X2) >= times(X1,X2) constraint: times(active(X1),X2) >= times(X1,X2) constraint: times(X1,mark(X2)) >= times(X1,X2) constraint: times(X1,active(X2)) >= times(X1,X2) constraint: square(mark(X)) >= square(X) constraint: square(active(X)) >= square(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(from(X)) >= Marked_mark(X) constraint: Marked_mark(from(X)) >= Marked_active(from(mark(X))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(2ndspos(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(2ndspos(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(2ndspos(X1,X2)) >= Marked_active(2ndspos(mark(X1), mark(X2))) constraint: Marked_mark(rcons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(rcons(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(rcons(X1,X2)) >= Marked_active(rcons(mark(X1),mark(X2))) constraint: Marked_mark(posrecip(X)) >= Marked_mark(X) constraint: Marked_mark(posrecip(X)) >= Marked_active(posrecip(mark(X))) constraint: Marked_mark(2ndsneg(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(2ndsneg(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(2ndsneg(X1,X2)) >= Marked_active(2ndsneg(mark(X1), mark(X2))) constraint: Marked_mark(negrecip(X)) >= Marked_mark(X) constraint: Marked_mark(negrecip(X)) >= Marked_active(negrecip(mark(X))) constraint: Marked_mark(pi(X)) >= Marked_mark(X) constraint: Marked_mark(pi(X)) >= Marked_active(pi(mark(X))) constraint: Marked_mark(plus(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(plus(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) constraint: Marked_mark(times(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(times(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(times(X1,X2)) >= Marked_active(times(mark(X1),mark(X2))) constraint: Marked_mark(square(X)) >= Marked_mark(X) constraint: Marked_mark(square(X)) >= Marked_active(square(mark(X))) constraint: Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) constraint: Marked_active(2ndspos(s(N),cons(X,cons(Y,Z)))) >= Marked_mark( rcons( posrecip( Y), 2ndsneg(N,Z))) constraint: Marked_active(2ndsneg(s(N),cons(X,cons(Y,Z)))) >= Marked_mark( rcons( negrecip( Y), 2ndspos(N,Z))) constraint: Marked_active(pi(X)) >= Marked_mark(2ndspos(X,from(0))) constraint: Marked_active(plus(s(X),Y)) >= Marked_mark(s(plus(X,Y))) constraint: Marked_active(plus(0,Y)) >= Marked_mark(Y) constraint: Marked_active(times(s(X),Y)) >= Marked_mark(plus(Y,times(X,Y))) constraint: Marked_active(square(X)) >= Marked_mark(times(X,X)) APPLY CRITERIA (Subterm criterion) ST: Marked_from -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_cons -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_s -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_2ndspos -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_rcons -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_posrecip -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_2ndsneg -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_negrecip -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_pi -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_plus -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_times -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_square -> 1 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)) >= active(cons(mark(X1),X2)) ; mark(from(X)) >= active(from(mark(X))) ; mark(s(X)) >= active(s(mark(X))) ; mark(rnil) >= active(rnil) ; mark(2ndspos(X1,X2)) >= active(2ndspos(mark(X1),mark(X2))) ; mark(0) >= active(0) ; mark(rcons(X1,X2)) >= active(rcons(mark(X1),mark(X2))) ; mark(posrecip(X)) >= active(posrecip(mark(X))) ; mark(2ndsneg(X1,X2)) >= active(2ndsneg(mark(X1),mark(X2))) ; mark(negrecip(X)) >= active(negrecip(mark(X))) ; mark(pi(X)) >= active(pi(mark(X))) ; mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) ; mark(times(X1,X2)) >= active(times(mark(X1),mark(X2))) ; mark(square(X)) >= active(square(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; from(mark(X)) >= from(X) ; from(active(X)) >= from(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; active(from(X)) >= mark(cons(X,from(s(X)))) ; active(2ndspos(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(negrecip(Y), 2ndspos(N,Z))) ; active(2ndsneg(0,Z)) >= mark(rnil) ; active(pi(X)) >= mark(2ndspos(X,from(0))) ; active(plus(s(X),Y)) >= mark(s(plus(X,Y))) ; active(plus(0,Y)) >= mark(Y) ; active(times(s(X),Y)) >= mark(plus(Y,times(X,Y))) ; active(times(0,Y)) >= mark(0) ; active(square(X)) >= mark(times(X,X)) ; 2ndspos(mark(X1),X2) >= 2ndspos(X1,X2) ; 2ndspos(active(X1),X2) >= 2ndspos(X1,X2) ; 2ndspos(X1,mark(X2)) >= 2ndspos(X1,X2) ; 2ndspos(X1,active(X2)) >= 2ndspos(X1,X2) ; rcons(mark(X1),X2) >= rcons(X1,X2) ; rcons(active(X1),X2) >= rcons(X1,X2) ; rcons(X1,mark(X2)) >= rcons(X1,X2) ; rcons(X1,active(X2)) >= rcons(X1,X2) ; posrecip(mark(X)) >= posrecip(X) ; posrecip(active(X)) >= posrecip(X) ; 2ndsneg(mark(X1),X2) >= 2ndsneg(X1,X2) ; 2ndsneg(active(X1),X2) >= 2ndsneg(X1,X2) ; 2ndsneg(X1,mark(X2)) >= 2ndsneg(X1,X2) ; 2ndsneg(X1,active(X2)) >= 2ndsneg(X1,X2) ; negrecip(mark(X)) >= negrecip(X) ; negrecip(active(X)) >= negrecip(X) ; pi(mark(X)) >= pi(X) ; pi(active(X)) >= pi(X) ; plus(mark(X1),X2) >= plus(X1,X2) ; plus(active(X1),X2) >= plus(X1,X2) ; plus(X1,mark(X2)) >= plus(X1,X2) ; plus(X1,active(X2)) >= plus(X1,X2) ; times(mark(X1),X2) >= times(X1,X2) ; times(active(X1),X2) >= times(X1,X2) ; times(X1,mark(X2)) >= times(X1,X2) ; times(X1,active(X2)) >= times(X1,X2) ; square(mark(X)) >= square(X) ; square(active(X)) >= square(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(from(X)) >= Marked_mark(X) ; Marked_mark(from(X)) >= Marked_active(from(mark(X))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(2ndspos(X1,X2)) >= Marked_mark(X1) ; Marked_mark(2ndspos(X1,X2)) >= Marked_mark(X2) ; Marked_mark(2ndspos(X1,X2)) >= Marked_active(2ndspos(mark(X1),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(2ndsneg(X1,X2)) >= Marked_mark(X1) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_mark(X2) ; Marked_mark(2ndsneg(X1,X2)) >= Marked_active(2ndsneg(mark(X1),mark(X2))) ; Marked_mark(negrecip(X)) >= Marked_mark(X) ; Marked_mark(pi(X)) >= Marked_mark(X) ; Marked_mark(pi(X)) >= Marked_active(pi(mark(X))) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X1) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X2) ; Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) ; Marked_mark(times(X1,X2)) >= Marked_mark(X1) ; Marked_mark(times(X1,X2)) >= Marked_mark(X2) ; Marked_mark(times(X1,X2)) >= Marked_active(times(mark(X1),mark(X2))) ; Marked_mark(square(X)) >= Marked_mark(X) ; Marked_mark(square(X)) >= Marked_active(square(mark(X))) ; Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) ; Marked_active(2ndspos(s(N),cons(X,cons(Y,Z)))) >= Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,cons(Y,Z)))) >= Marked_mark(rcons( negrecip( Y), 2ndspos(N,Z))) ; Marked_active(pi(X)) >= Marked_mark(2ndspos(X,from(0))) ; Marked_active(plus(s(X),Y)) >= Marked_mark(s(plus(X,Y))) ; Marked_active(plus(0,Y)) >= Marked_mark(Y) ; Marked_active(times(s(X),Y)) >= Marked_mark(plus(Y,times(X,Y))) ; Marked_active(square(X)) >= Marked_mark(times(X,X)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(from(X)) > Marked_mark(X) ; } { Marked_mark(from(X)) > Marked_active(from(mark(X))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(2ndspos(X1,X2)) > Marked_active(2ndspos(mark(X1),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(2ndsneg(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(2ndsneg(X1,X2)) > Marked_active(2ndsneg(mark(X1),mark(X2))) ; } { Marked_mark(negrecip(X)) > Marked_mark(X) ; } { Marked_mark(pi(X)) > Marked_mark(X) ; } { Marked_mark(pi(X)) > Marked_active(pi(mark(X))) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(plus(X1,X2)) > Marked_active(plus(mark(X1),mark(X2))) ; } { Marked_mark(times(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(times(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(times(X1,X2)) > Marked_active(times(mark(X1),mark(X2))) ; } { Marked_mark(square(X)) > Marked_mark(X) ; } { Marked_mark(square(X)) > Marked_active(square(mark(X))) ; } { Marked_active(from(X)) > Marked_mark(cons(X,from(s(X)))) ; } { Marked_active(2ndspos(s(N),cons(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; } { Marked_active(2ndsneg(s(N),cons(X,cons(Y,Z)))) > Marked_mark(rcons( negrecip( Y), 2ndspos(N,Z))) ; } { Marked_active(pi(X)) > Marked_mark(2ndspos(X,from(0))) ; } { Marked_active(plus(s(X),Y)) > Marked_mark(s(plus(X,Y))) ; } { Marked_active(plus(0,Y)) > Marked_mark(Y) ; } { Marked_active(times(s(X),Y)) > Marked_mark(plus(Y,times(X,Y))) ; } { Marked_active(square(X)) > Marked_mark(times(X,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 === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === 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)) >= active(cons(mark(X1),X2)) ; mark(from(X)) >= active(from(mark(X))) ; mark(s(X)) >= active(s(mark(X))) ; mark(rnil) >= active(rnil) ; mark(2ndspos(X1,X2)) >= active(2ndspos(mark(X1),mark(X2))) ; mark(0) >= active(0) ; mark(rcons(X1,X2)) >= active(rcons(mark(X1),mark(X2))) ; mark(posrecip(X)) >= active(posrecip(mark(X))) ; mark(2ndsneg(X1,X2)) >= active(2ndsneg(mark(X1),mark(X2))) ; mark(negrecip(X)) >= active(negrecip(mark(X))) ; mark(pi(X)) >= active(pi(mark(X))) ; mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) ; mark(times(X1,X2)) >= active(times(mark(X1),mark(X2))) ; mark(square(X)) >= active(square(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; from(mark(X)) >= from(X) ; from(active(X)) >= from(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; active(from(X)) >= mark(cons(X,from(s(X)))) ; active(2ndspos(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(negrecip(Y), 2ndspos(N,Z))) ; active(2ndsneg(0,Z)) >= mark(rnil) ; active(pi(X)) >= mark(2ndspos(X,from(0))) ; active(plus(s(X),Y)) >= mark(s(plus(X,Y))) ; active(plus(0,Y)) >= mark(Y) ; active(times(s(X),Y)) >= mark(plus(Y,times(X,Y))) ; active(times(0,Y)) >= mark(0) ; active(square(X)) >= mark(times(X,X)) ; 2ndspos(mark(X1),X2) >= 2ndspos(X1,X2) ; 2ndspos(active(X1),X2) >= 2ndspos(X1,X2) ; 2ndspos(X1,mark(X2)) >= 2ndspos(X1,X2) ; 2ndspos(X1,active(X2)) >= 2ndspos(X1,X2) ; rcons(mark(X1),X2) >= rcons(X1,X2) ; rcons(active(X1),X2) >= rcons(X1,X2) ; rcons(X1,mark(X2)) >= rcons(X1,X2) ; rcons(X1,active(X2)) >= rcons(X1,X2) ; posrecip(mark(X)) >= posrecip(X) ; posrecip(active(X)) >= posrecip(X) ; 2ndsneg(mark(X1),X2) >= 2ndsneg(X1,X2) ; 2ndsneg(active(X1),X2) >= 2ndsneg(X1,X2) ; 2ndsneg(X1,mark(X2)) >= 2ndsneg(X1,X2) ; 2ndsneg(X1,active(X2)) >= 2ndsneg(X1,X2) ; negrecip(mark(X)) >= negrecip(X) ; negrecip(active(X)) >= negrecip(X) ; pi(mark(X)) >= pi(X) ; pi(active(X)) >= pi(X) ; plus(mark(X1),X2) >= plus(X1,X2) ; plus(active(X1),X2) >= plus(X1,X2) ; plus(X1,mark(X2)) >= plus(X1,X2) ; plus(X1,active(X2)) >= plus(X1,X2) ; times(mark(X1),X2) >= times(X1,X2) ; times(active(X1),X2) >= times(X1,X2) ; times(X1,mark(X2)) >= times(X1,X2) ; times(X1,active(X2)) >= times(X1,X2) ; square(mark(X)) >= square(X) ; square(active(X)) >= square(X) ; Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; Marked_mark(from(X)) > Marked_mark(X) ; Marked_mark(from(X)) > Marked_active(from(mark(X))) ; Marked_mark(s(X)) > Marked_mark(X) ; Marked_mark(2ndspos(X1,X2)) > Marked_mark(X1) ; Marked_mark(2ndspos(X1,X2)) > Marked_mark(X2) ; Marked_mark(2ndspos(X1,X2)) > Marked_active(2ndspos(mark(X1),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(2ndsneg(X1,X2)) > Marked_mark(X1) ; Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X2) ; Marked_mark(2ndsneg(X1,X2)) > Marked_active(2ndsneg(mark(X1),mark(X2))) ; Marked_mark(negrecip(X)) > Marked_mark(X) ; Marked_mark(pi(X)) > Marked_mark(X) ; Marked_mark(pi(X)) > Marked_active(pi(mark(X))) ; Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; Marked_mark(plus(X1,X2)) > Marked_active(plus(mark(X1),mark(X2))) ; Marked_mark(times(X1,X2)) > Marked_mark(X1) ; Marked_mark(times(X1,X2)) > Marked_mark(X2) ; Marked_mark(times(X1,X2)) > Marked_active(times(mark(X1),mark(X2))) ; Marked_mark(square(X)) > Marked_mark(X) ; Marked_mark(square(X)) >= Marked_active(square(mark(X))) ; Marked_active(from(X)) > Marked_mark(cons(X,from(s(X)))) ; Marked_active(2ndspos(s(N),cons(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,cons(Y,Z)))) > Marked_mark(rcons( negrecip( Y), 2ndspos(N,Z))) ; Marked_active(pi(X)) > Marked_mark(2ndspos(X,from(0))) ; Marked_active(plus(s(X),Y)) > Marked_mark(s(plus(X,Y))) ; Marked_active(plus(0,Y)) > Marked_mark(Y) ; Marked_active(times(s(X),Y)) > Marked_mark(plus(Y,times(X,Y))) ; Marked_active(square(X)) > Marked_mark(times(X,X)) ; } APPLY CRITERIA (SOLVE_ORD) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(from(X)) >= active(from(mark(X))) ; mark(s(X)) >= active(s(mark(X))) ; mark(rnil) >= active(rnil) ; mark(2ndspos(X1,X2)) >= active(2ndspos(mark(X1),mark(X2))) ; mark(0) >= active(0) ; mark(rcons(X1,X2)) >= active(rcons(mark(X1),mark(X2))) ; mark(posrecip(X)) >= active(posrecip(mark(X))) ; mark(2ndsneg(X1,X2)) >= active(2ndsneg(mark(X1),mark(X2))) ; mark(negrecip(X)) >= active(negrecip(mark(X))) ; mark(pi(X)) >= active(pi(mark(X))) ; mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) ; mark(times(X1,X2)) >= active(times(mark(X1),mark(X2))) ; mark(square(X)) >= active(square(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; from(mark(X)) >= from(X) ; from(active(X)) >= from(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; active(from(X)) >= mark(cons(X,from(s(X)))) ; active(2ndspos(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,cons(Y,Z)))) >= mark(rcons(negrecip(Y), 2ndspos(N,Z))) ; active(2ndsneg(0,Z)) >= mark(rnil) ; active(pi(X)) >= mark(2ndspos(X,from(0))) ; active(plus(s(X),Y)) >= mark(s(plus(X,Y))) ; active(plus(0,Y)) >= mark(Y) ; active(times(s(X),Y)) >= mark(plus(Y,times(X,Y))) ; active(times(0,Y)) >= mark(0) ; active(square(X)) >= mark(times(X,X)) ; 2ndspos(mark(X1),X2) >= 2ndspos(X1,X2) ; 2ndspos(active(X1),X2) >= 2ndspos(X1,X2) ; 2ndspos(X1,mark(X2)) >= 2ndspos(X1,X2) ; 2ndspos(X1,active(X2)) >= 2ndspos(X1,X2) ; rcons(mark(X1),X2) >= rcons(X1,X2) ; rcons(active(X1),X2) >= rcons(X1,X2) ; rcons(X1,mark(X2)) >= rcons(X1,X2) ; rcons(X1,active(X2)) >= rcons(X1,X2) ; posrecip(mark(X)) >= posrecip(X) ; posrecip(active(X)) >= posrecip(X) ; 2ndsneg(mark(X1),X2) >= 2ndsneg(X1,X2) ; 2ndsneg(active(X1),X2) >= 2ndsneg(X1,X2) ; 2ndsneg(X1,mark(X2)) >= 2ndsneg(X1,X2) ; 2ndsneg(X1,active(X2)) >= 2ndsneg(X1,X2) ; negrecip(mark(X)) >= negrecip(X) ; negrecip(active(X)) >= negrecip(X) ; pi(mark(X)) >= pi(X) ; pi(active(X)) >= pi(X) ; plus(mark(X1),X2) >= plus(X1,X2) ; plus(active(X1),X2) >= plus(X1,X2) ; plus(X1,mark(X2)) >= plus(X1,X2) ; plus(X1,active(X2)) >= plus(X1,X2) ; times(mark(X1),X2) >= times(X1,X2) ; times(active(X1),X2) >= times(X1,X2) ; times(X1,mark(X2)) >= times(X1,X2) ; times(X1,active(X2)) >= times(X1,X2) ; square(mark(X)) >= square(X) ; square(active(X)) >= square(X) ; Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; Marked_mark(from(X)) > Marked_mark(X) ; Marked_mark(from(X)) > Marked_active(from(mark(X))) ; Marked_mark(s(X)) > Marked_mark(X) ; Marked_mark(2ndspos(X1,X2)) > Marked_mark(X1) ; Marked_mark(2ndspos(X1,X2)) > Marked_mark(X2) ; Marked_mark(2ndspos(X1,X2)) > Marked_active(2ndspos(mark(X1),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(2ndsneg(X1,X2)) > Marked_mark(X1) ; Marked_mark(2ndsneg(X1,X2)) > Marked_mark(X2) ; Marked_mark(2ndsneg(X1,X2)) > Marked_active(2ndsneg(mark(X1),mark(X2))) ; Marked_mark(negrecip(X)) > Marked_mark(X) ; Marked_mark(pi(X)) > Marked_mark(X) ; Marked_mark(pi(X)) > Marked_active(pi(mark(X))) ; Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; Marked_mark(plus(X1,X2)) > Marked_active(plus(mark(X1),mark(X2))) ; Marked_mark(times(X1,X2)) > Marked_mark(X1) ; Marked_mark(times(X1,X2)) > Marked_mark(X2) ; Marked_mark(times(X1,X2)) > Marked_active(times(mark(X1),mark(X2))) ; Marked_mark(square(X)) > Marked_mark(X) ; Marked_mark(square(X)) >= Marked_active(square(mark(X))) ; Marked_active(from(X)) > Marked_mark(cons(X,from(s(X)))) ; Marked_active(2ndspos(s(N),cons(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,cons(Y,Z)))) > Marked_mark(rcons( negrecip( Y), 2ndspos(N,Z))) ; Marked_active(pi(X)) > Marked_mark(2ndspos(X,from(0))) ; Marked_active(plus(s(X),Y)) > Marked_mark(s(plus(X,Y))) ; Marked_active(plus(0,Y)) > Marked_mark(Y) ; Marked_active(times(s(X),Y)) > Marked_mark(plus(Y,times(X,Y))) ; Marked_active(square(X)) > Marked_mark(times(X,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 === No solution found for these parameters.(338 bt (249) [302]) === 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) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_cons -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_2ndspos -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_rcons -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_2ndsneg -> 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 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_plus -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_times -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: NOT SOLVED No proof found Cime worked for 88.915823 seconds (real time) Cime Exit Status: 0