- : 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,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) [4] active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) [5] active(2ndsneg(0,Z)) -> mark(rnil) [6] active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) [7] active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) [8] active(pi(X)) -> mark(2ndspos(X,from(0))) [9] active(plus(0,Y)) -> mark(Y) [10] active(plus(s(X),Y)) -> mark(s(plus(X,Y))) [11] active(times(0,Y)) -> mark(0) [12] active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) [13] active(square(X)) -> mark(times(X,X)) [14] mark(from(X)) -> active(from(mark(X))) [15] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [16] mark(s(X)) -> active(s(mark(X))) [17] mark(2ndspos(X1,X2)) -> active(2ndspos(mark(X1),mark(X2))) [18] mark(0) -> active(0) [19] mark(rnil) -> active(rnil) [20] mark(cons2(X1,X2)) -> active(cons2(X1,mark(X2))) [21] mark(rcons(X1,X2)) -> active(rcons(mark(X1),mark(X2))) [22] mark(posrecip(X)) -> active(posrecip(mark(X))) [23] mark(2ndsneg(X1,X2)) -> active(2ndsneg(mark(X1),mark(X2))) [24] mark(negrecip(X)) -> active(negrecip(mark(X))) [25] mark(pi(X)) -> active(pi(mark(X))) [26] mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) [27] mark(times(X1,X2)) -> active(times(mark(X1),mark(X2))) [28] mark(square(X)) -> active(square(mark(X))) [29] from(mark(X)) -> from(X) [30] from(active(X)) -> from(X) [31] cons(mark(X1),X2) -> cons(X1,X2) [32] cons(X1,mark(X2)) -> cons(X1,X2) [33] cons(active(X1),X2) -> cons(X1,X2) [34] cons(X1,active(X2)) -> cons(X1,X2) [35] s(mark(X)) -> s(X) [36] s(active(X)) -> s(X) [37] 2ndspos(mark(X1),X2) -> 2ndspos(X1,X2) [38] 2ndspos(X1,mark(X2)) -> 2ndspos(X1,X2) [39] 2ndspos(active(X1),X2) -> 2ndspos(X1,X2) [40] 2ndspos(X1,active(X2)) -> 2ndspos(X1,X2) [41] cons2(mark(X1),X2) -> cons2(X1,X2) [42] cons2(X1,mark(X2)) -> cons2(X1,X2) [43] cons2(active(X1),X2) -> cons2(X1,X2) [44] cons2(X1,active(X2)) -> cons2(X1,X2) [45] rcons(mark(X1),X2) -> rcons(X1,X2) [46] rcons(X1,mark(X2)) -> rcons(X1,X2) [47] rcons(active(X1),X2) -> rcons(X1,X2) [48] rcons(X1,active(X2)) -> rcons(X1,X2) [49] posrecip(mark(X)) -> posrecip(X) [50] posrecip(active(X)) -> posrecip(X) [51] 2ndsneg(mark(X1),X2) -> 2ndsneg(X1,X2) [52] 2ndsneg(X1,mark(X2)) -> 2ndsneg(X1,X2) [53] 2ndsneg(active(X1),X2) -> 2ndsneg(X1,X2) [54] 2ndsneg(X1,active(X2)) -> 2ndsneg(X1,X2) [55] negrecip(mark(X)) -> negrecip(X) [56] negrecip(active(X)) -> negrecip(X) [57] pi(mark(X)) -> pi(X) [58] pi(active(X)) -> pi(X) [59] plus(mark(X1),X2) -> plus(X1,X2) [60] plus(X1,mark(X2)) -> plus(X1,X2) [61] plus(active(X1),X2) -> plus(X1,X2) [62] plus(X1,active(X2)) -> plus(X1,X2) [63] times(mark(X1),X2) -> times(X1,X2) [64] times(X1,mark(X2)) -> times(X1,X2) [65] times(active(X1),X2) -> times(X1,X2) [66] times(X1,active(X2)) -> times(X1,X2) [67] square(mark(X)) -> square(X) [68] square(active(X)) -> square(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 14 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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) ; 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) ; active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) ; active(2ndsneg(s(N),cons2(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) ; cons2(mark(X1),X2) >= cons2(X1,X2) ; cons2(active(X1),X2) >= cons2(X1,X2) ; cons2(X1,mark(X2)) >= cons2(X1,X2) ; cons2(X1,active(X2)) >= cons2(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(cons2(X1,X2)) >= Marked_mark(X2) ; Marked_mark(cons2(X1,X2)) >= Marked_active(cons2(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,Z))) >= Marked_mark(2ndspos(s(N), cons2(X,Z))) ; Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,Z))) >= Marked_mark(2ndsneg(s(N), cons2(X,Z))) ; Marked_active(2ndsneg(s(N),cons2(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(cons2(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(cons2(X1,X2)) > Marked_active(cons2(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,Z))) > Marked_mark(2ndspos(s(N),cons2(X,Z))) ; } { Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; } { Marked_active(2ndsneg(s(N),cons(X,Z))) > Marked_mark(2ndsneg(s(N),cons2(X,Z))) ; } { Marked_active(2ndsneg(s(N),cons2(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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) constraint: active(2ndspos(s(N),cons2(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,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) constraint: active(2ndsneg(s(N),cons2(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: cons2(mark(X1),X2) >= cons2(X1,X2) constraint: cons2(active(X1),X2) >= cons2(X1,X2) constraint: cons2(X1,mark(X2)) >= cons2(X1,X2) constraint: cons2(X1,active(X2)) >= cons2(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(cons2(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(cons2(X1,X2)) >= Marked_active(cons2(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,Z))) >= Marked_mark(2ndspos( s(N), cons2(X,Z))) constraint: Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= Marked_mark( rcons( posrecip( Y), 2ndsneg(N,Z))) constraint: Marked_active(2ndsneg(s(N),cons(X,Z))) >= Marked_mark(2ndsneg( s(N), cons2(X,Z))) constraint: Marked_active(2ndsneg(s(N),cons2(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_cons2 -> 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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) ; 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) ; active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) ; active(2ndsneg(s(N),cons2(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) ; cons2(mark(X1),X2) >= cons2(X1,X2) ; cons2(active(X1),X2) >= cons2(X1,X2) ; cons2(X1,mark(X2)) >= cons2(X1,X2) ; cons2(X1,active(X2)) >= cons2(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(cons2(X1,X2)) >= Marked_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,Z))) >= Marked_mark(2ndspos(s(N), cons2(X,Z))) ; Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,Z))) >= Marked_mark(2ndsneg(s(N), cons2(X,Z))) ; Marked_active(2ndsneg(s(N),cons2(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(cons2(X1,X2)) > Marked_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,Z))) > Marked_mark(2ndspos(s(N),cons2(X,Z))) ; } { Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; } { Marked_active(2ndsneg(s(N),cons(X,Z))) > Marked_mark(2ndsneg(s(N),cons2(X,Z))) ; } { Marked_active(2ndsneg(s(N),cons2(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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) constraint: active(2ndspos(s(N),cons2(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,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) constraint: active(2ndsneg(s(N),cons2(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: cons2(mark(X1),X2) >= cons2(X1,X2) constraint: cons2(active(X1),X2) >= cons2(X1,X2) constraint: cons2(X1,mark(X2)) >= cons2(X1,X2) constraint: cons2(X1,active(X2)) >= cons2(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(cons2(X1,X2)) >= Marked_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,Z))) >= Marked_mark(2ndspos( s(N), cons2(X,Z))) constraint: Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= Marked_mark( rcons( posrecip( Y), 2ndsneg(N,Z))) constraint: Marked_active(2ndsneg(s(N),cons(X,Z))) >= Marked_mark(2ndsneg( s(N), cons2(X,Z))) constraint: Marked_active(2ndsneg(s(N),cons2(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 (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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) ; 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) ; active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) ; active(2ndsneg(s(N),cons2(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) ; cons2(mark(X1),X2) >= cons2(X1,X2) ; cons2(active(X1),X2) >= cons2(X1,X2) ; cons2(X1,mark(X2)) >= cons2(X1,X2) ; cons2(X1,active(X2)) >= cons2(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(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(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(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,Z))) >= Marked_mark(2ndspos(s(N), cons2(X,Z))) ; Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,Z))) >= Marked_mark(2ndsneg(s(N), cons2(X,Z))) ; Marked_active(2ndsneg(s(N),cons2(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(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(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(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,Z))) > Marked_mark(2ndspos(s(N),cons2(X,Z))) ; } { Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; } { Marked_active(2ndsneg(s(N),cons(X,Z))) > Marked_mark(2ndsneg(s(N),cons2(X,Z))) ; } { Marked_active(2ndsneg(s(N),cons2(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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) constraint: active(2ndspos(s(N),cons2(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,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) constraint: active(2ndsneg(s(N),cons2(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: cons2(mark(X1),X2) >= cons2(X1,X2) constraint: cons2(active(X1),X2) >= cons2(X1,X2) constraint: cons2(X1,mark(X2)) >= cons2(X1,X2) constraint: cons2(X1,active(X2)) >= cons2(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(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(cons2(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(rcons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(rcons(X1,X2)) >= Marked_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,Z))) >= Marked_mark(2ndspos( s(N), cons2(X,Z))) constraint: Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= Marked_mark( rcons( posrecip( Y), 2ndsneg(N,Z))) constraint: Marked_active(2ndsneg(s(N),cons(X,Z))) >= Marked_mark(2ndsneg( s(N), cons2(X,Z))) constraint: Marked_active(2ndsneg(s(N),cons2(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 (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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) ; 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) ; active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) ; active(2ndsneg(s(N),cons2(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) ; cons2(mark(X1),X2) >= cons2(X1,X2) ; cons2(active(X1),X2) >= cons2(X1,X2) ; cons2(X1,mark(X2)) >= cons2(X1,X2) ; cons2(X1,active(X2)) >= cons2(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(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(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,Z))) >= Marked_mark(2ndspos(s(N), cons2(X,Z))) ; Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,Z))) >= Marked_mark(2ndsneg(s(N), cons2(X,Z))) ; Marked_active(2ndsneg(s(N),cons2(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(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(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,Z))) > Marked_mark(2ndspos(s(N),cons2(X,Z))) ; } { Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; } { Marked_active(2ndsneg(s(N),cons(X,Z))) > Marked_mark(2ndsneg(s(N),cons2(X,Z))) ; } { Marked_active(2ndsneg(s(N),cons2(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 : 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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) ; 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) ; active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) ; active(2ndsneg(s(N),cons2(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) ; cons2(mark(X1),X2) >= cons2(X1,X2) ; cons2(active(X1),X2) >= cons2(X1,X2) ; cons2(X1,mark(X2)) >= cons2(X1,X2) ; cons2(X1,active(X2)) >= cons2(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(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(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,Z))) > Marked_mark(2ndspos(s(N),cons2(X,Z))) ; Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,Z))) > Marked_mark(2ndsneg(s(N),cons2(X,Z))) ; Marked_active(2ndsneg(s(N),cons2(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(cons2(X1,X2)) >= active(cons2(X1,mark(X2))) ; 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,Z))) >= mark(2ndspos(s(N),cons2(X,Z))) ; active(2ndspos(s(N),cons2(X,cons(Y,Z)))) >= mark(rcons(posrecip(Y), 2ndsneg(N,Z))) ; active(2ndspos(0,Z)) >= mark(rnil) ; active(2ndsneg(s(N),cons(X,Z))) >= mark(2ndsneg(s(N),cons2(X,Z))) ; active(2ndsneg(s(N),cons2(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) ; cons2(mark(X1),X2) >= cons2(X1,X2) ; cons2(active(X1),X2) >= cons2(X1,X2) ; cons2(X1,mark(X2)) >= cons2(X1,X2) ; cons2(X1,active(X2)) >= cons2(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(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(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,Z))) > Marked_mark(2ndspos(s(N),cons2(X,Z))) ; Marked_active(2ndspos(s(N),cons2(X,cons(Y,Z)))) > Marked_mark(rcons( posrecip( Y), 2ndsneg(N,Z))) ; Marked_active(2ndsneg(s(N),cons(X,Z))) > Marked_mark(2ndsneg(s(N),cons2(X,Z))) ; Marked_active(2ndsneg(s(N),cons2(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.(1249 bt (923) [1048]) === 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 virtual === === STOPING TIMER real === Global timeout: 300.000000