- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) [2] active(sqr(0)) -> mark(0) [3] active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) [4] active(dbl(0)) -> mark(0) [5] active(dbl(s(X))) -> mark(s(s(dbl(X)))) [6] active(add(0,X)) -> mark(X) [7] active(add(s(X),Y)) -> mark(s(add(X,Y))) [8] active(first(0,X)) -> mark(nil) [9] active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) [10] active(terms(X)) -> terms(active(X)) [11] active(cons(X1,X2)) -> cons(active(X1),X2) [12] active(recip(X)) -> recip(active(X)) [13] active(sqr(X)) -> sqr(active(X)) [14] active(s(X)) -> s(active(X)) [15] active(add(X1,X2)) -> add(active(X1),X2) [16] active(add(X1,X2)) -> add(X1,active(X2)) [17] active(dbl(X)) -> dbl(active(X)) [18] active(first(X1,X2)) -> first(active(X1),X2) [19] active(first(X1,X2)) -> first(X1,active(X2)) [20] terms(mark(X)) -> mark(terms(X)) [21] cons(mark(X1),X2) -> mark(cons(X1,X2)) [22] recip(mark(X)) -> mark(recip(X)) [23] sqr(mark(X)) -> mark(sqr(X)) [24] s(mark(X)) -> mark(s(X)) [25] add(mark(X1),X2) -> mark(add(X1,X2)) [26] add(X1,mark(X2)) -> mark(add(X1,X2)) [27] dbl(mark(X)) -> mark(dbl(X)) [28] first(mark(X1),X2) -> mark(first(X1,X2)) [29] first(X1,mark(X2)) -> mark(first(X1,X2)) [30] proper(terms(X)) -> terms(proper(X)) [31] proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) [32] proper(recip(X)) -> recip(proper(X)) [33] proper(sqr(X)) -> sqr(proper(X)) [34] proper(s(X)) -> s(proper(X)) [35] proper(0) -> ok(0) [36] proper(add(X1,X2)) -> add(proper(X1),proper(X2)) [37] proper(dbl(X)) -> dbl(proper(X)) [38] proper(first(X1,X2)) -> first(proper(X1),proper(X2)) [39] proper(nil) -> ok(nil) [40] terms(ok(X)) -> ok(terms(X)) [41] cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) [42] recip(ok(X)) -> ok(recip(X)) [43] sqr(ok(X)) -> ok(sqr(X)) [44] s(ok(X)) -> ok(s(X)) [45] add(ok(X1),ok(X2)) -> ok(add(X1,X2)) [46] dbl(ok(X)) -> ok(dbl(X)) [47] first(ok(X1),ok(X2)) -> ok(first(X1,X2)) [48] top(mark(X)) -> top(proper(X)) [49] top(ok(X)) -> top(active(X)) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 11 components: { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_top(mark(X)) >= Marked_top(proper(X)) ; Marked_top(ok(X)) >= Marked_top(active(X)) ; } + Disjunctions:{ { Marked_top(mark(X)) > Marked_top(proper(X)) ; } { Marked_top(ok(X)) > Marked_top(active(X)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_top(mark(X)) >= Marked_top(proper(X)) constraint: Marked_top(ok(X)) >= Marked_top(active(X)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_proper(cons(X1,X2)) >= Marked_proper(X1) ; Marked_proper(cons(X1,X2)) >= Marked_proper(X2) ; Marked_proper(recip(X)) >= Marked_proper(X) ; Marked_proper(sqr(X)) >= Marked_proper(X) ; Marked_proper(terms(X)) >= Marked_proper(X) ; Marked_proper(s(X)) >= Marked_proper(X) ; Marked_proper(add(X1,X2)) >= Marked_proper(X1) ; Marked_proper(add(X1,X2)) >= Marked_proper(X2) ; Marked_proper(dbl(X)) >= Marked_proper(X) ; Marked_proper(first(X1,X2)) >= Marked_proper(X1) ; Marked_proper(first(X1,X2)) >= Marked_proper(X2) ; } + Disjunctions:{ { Marked_proper(cons(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(cons(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(recip(X)) > Marked_proper(X) ; } { Marked_proper(sqr(X)) > Marked_proper(X) ; } { Marked_proper(terms(X)) > Marked_proper(X) ; } { Marked_proper(s(X)) > Marked_proper(X) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(dbl(X)) > Marked_proper(X) ; } { Marked_proper(first(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(first(X1,X2)) > Marked_proper(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_proper(cons(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(cons(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(recip(X)) >= Marked_proper(X) constraint: Marked_proper(sqr(X)) >= Marked_proper(X) constraint: Marked_proper(terms(X)) >= Marked_proper(X) constraint: Marked_proper(s(X)) >= Marked_proper(X) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(dbl(X)) >= Marked_proper(X) constraint: Marked_proper(first(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(first(X1,X2)) >= Marked_proper(X2) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_active(cons(X1,X2)) >= Marked_active(X1) ; Marked_active(recip(X)) >= Marked_active(X) ; Marked_active(sqr(X)) >= Marked_active(X) ; Marked_active(terms(X)) >= Marked_active(X) ; Marked_active(s(X)) >= Marked_active(X) ; Marked_active(add(X1,X2)) >= Marked_active(X1) ; Marked_active(add(X1,X2)) >= Marked_active(X2) ; Marked_active(dbl(X)) >= Marked_active(X) ; Marked_active(first(X1,X2)) >= Marked_active(X1) ; Marked_active(first(X1,X2)) >= Marked_active(X2) ; } + Disjunctions:{ { Marked_active(cons(X1,X2)) > Marked_active(X1) ; } { Marked_active(recip(X)) > Marked_active(X) ; } { Marked_active(sqr(X)) > Marked_active(X) ; } { Marked_active(terms(X)) > Marked_active(X) ; } { Marked_active(s(X)) > Marked_active(X) ; } { Marked_active(add(X1,X2)) > Marked_active(X1) ; } { Marked_active(add(X1,X2)) > Marked_active(X2) ; } { Marked_active(dbl(X)) > Marked_active(X) ; } { Marked_active(first(X1,X2)) > Marked_active(X1) ; } { Marked_active(first(X1,X2)) > Marked_active(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_active(cons(X1,X2)) >= Marked_active(X1) constraint: Marked_active(recip(X)) >= Marked_active(X) constraint: Marked_active(sqr(X)) >= Marked_active(X) constraint: Marked_active(terms(X)) >= Marked_active(X) constraint: Marked_active(s(X)) >= Marked_active(X) constraint: Marked_active(add(X1,X2)) >= Marked_active(X1) constraint: Marked_active(add(X1,X2)) >= Marked_active(X2) constraint: Marked_active(dbl(X)) >= Marked_active(X) constraint: Marked_active(first(X1,X2)) >= Marked_active(X1) constraint: Marked_active(first(X1,X2)) >= Marked_active(X2) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_terms(mark(X)) >= Marked_terms(X) ; Marked_terms(ok(X)) >= Marked_terms(X) ; } + Disjunctions:{ { Marked_terms(mark(X)) > Marked_terms(X) ; } { Marked_terms(ok(X)) > Marked_terms(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_terms(mark(X)) >= Marked_terms(X) constraint: Marked_terms(ok(X)) >= Marked_terms(X) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_cons(mark(X1),X2) >= Marked_cons(X1,X2) ; Marked_cons(ok(X1),ok(X2)) >= Marked_cons(X1,X2) ; } + Disjunctions:{ { Marked_cons(mark(X1),X2) > Marked_cons(X1,X2) ; } { Marked_cons(ok(X1),ok(X2)) > Marked_cons(X1,X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_cons(mark(X1),X2) >= Marked_cons(X1,X2) constraint: Marked_cons(ok(X1),ok(X2)) >= Marked_cons(X1,X2) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_recip(mark(X)) >= Marked_recip(X) ; Marked_recip(ok(X)) >= Marked_recip(X) ; } + Disjunctions:{ { Marked_recip(mark(X)) > Marked_recip(X) ; } { Marked_recip(ok(X)) > Marked_recip(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_recip(mark(X)) >= Marked_recip(X) constraint: Marked_recip(ok(X)) >= Marked_recip(X) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_sqr(mark(X)) >= Marked_sqr(X) ; Marked_sqr(ok(X)) >= Marked_sqr(X) ; } + Disjunctions:{ { Marked_sqr(mark(X)) > Marked_sqr(X) ; } { Marked_sqr(ok(X)) > Marked_sqr(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_sqr(mark(X)) >= Marked_sqr(X) constraint: Marked_sqr(ok(X)) >= Marked_sqr(X) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_s(mark(X)) >= Marked_s(X) ; Marked_s(ok(X)) >= Marked_s(X) ; } + Disjunctions:{ { Marked_s(mark(X)) > Marked_s(X) ; } { Marked_s(ok(X)) > Marked_s(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_s(mark(X)) >= Marked_s(X) constraint: Marked_s(ok(X)) >= Marked_s(X) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_add(mark(X1),X2) >= Marked_add(X1,X2) ; Marked_add(ok(X1),ok(X2)) >= Marked_add(X1,X2) ; Marked_add(X1,mark(X2)) >= Marked_add(X1,X2) ; } + Disjunctions:{ { Marked_add(mark(X1),X2) > Marked_add(X1,X2) ; } { Marked_add(ok(X1),ok(X2)) > Marked_add(X1,X2) ; } { Marked_add(X1,mark(X2)) > Marked_add(X1,X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_add(mark(X1),X2) >= Marked_add(X1,X2) constraint: Marked_add(ok(X1),ok(X2)) >= Marked_add(X1,X2) constraint: Marked_add(X1,mark(X2)) >= Marked_add(X1,X2) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_dbl(mark(X)) >= Marked_dbl(X) ; Marked_dbl(ok(X)) >= Marked_dbl(X) ; } + Disjunctions:{ { Marked_dbl(mark(X)) > Marked_dbl(X) ; } { Marked_dbl(ok(X)) > Marked_dbl(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_dbl(mark(X)) >= Marked_dbl(X) constraint: Marked_dbl(ok(X)) >= Marked_dbl(X) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_first(mark(X1),X2) >= Marked_first(X1,X2) ; Marked_first(ok(X1),ok(X2)) >= Marked_first(X1,X2) ; Marked_first(X1,mark(X2)) >= Marked_first(X1,X2) ; } + Disjunctions:{ { Marked_first(mark(X1),X2) > Marked_first(X1,X2) ; } { Marked_first(ok(X1),ok(X2)) > Marked_first(X1,X2) ; } { Marked_first(X1,mark(X2)) > Marked_first(X1,X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_first(mark(X1),X2) >= Marked_first(X1,X2) constraint: Marked_first(ok(X1),ok(X2)) >= Marked_first(X1,X2) constraint: Marked_first(X1,mark(X2)) >= Marked_first(X1,X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_top(ok(X)) >= Marked_top(active(X)) ; } + Disjunctions:{ { Marked_top(ok(X)) > Marked_top(active(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_top(ok(X)) >= Marked_top(active(X)) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_proper(cons(X1,X2)) >= Marked_proper(X1) ; Marked_proper(cons(X1,X2)) >= Marked_proper(X2) ; Marked_proper(recip(X)) >= Marked_proper(X) ; Marked_proper(terms(X)) >= Marked_proper(X) ; Marked_proper(s(X)) >= Marked_proper(X) ; Marked_proper(add(X1,X2)) >= Marked_proper(X1) ; Marked_proper(add(X1,X2)) >= Marked_proper(X2) ; Marked_proper(dbl(X)) >= Marked_proper(X) ; Marked_proper(first(X1,X2)) >= Marked_proper(X1) ; Marked_proper(first(X1,X2)) >= Marked_proper(X2) ; } + Disjunctions:{ { Marked_proper(cons(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(cons(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(recip(X)) > Marked_proper(X) ; } { Marked_proper(terms(X)) > Marked_proper(X) ; } { Marked_proper(s(X)) > Marked_proper(X) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(dbl(X)) > Marked_proper(X) ; } { Marked_proper(first(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(first(X1,X2)) > Marked_proper(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_proper(cons(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(cons(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(recip(X)) >= Marked_proper(X) constraint: Marked_proper(terms(X)) >= Marked_proper(X) constraint: Marked_proper(s(X)) >= Marked_proper(X) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(dbl(X)) >= Marked_proper(X) constraint: Marked_proper(first(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(first(X1,X2)) >= Marked_proper(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_proper(cons(X1,X2)) >= Marked_proper(X1) ; Marked_proper(cons(X1,X2)) >= Marked_proper(X2) ; Marked_proper(recip(X)) >= Marked_proper(X) ; Marked_proper(terms(X)) >= Marked_proper(X) ; Marked_proper(s(X)) >= Marked_proper(X) ; Marked_proper(add(X1,X2)) >= Marked_proper(X1) ; Marked_proper(add(X1,X2)) >= Marked_proper(X2) ; Marked_proper(dbl(X)) >= Marked_proper(X) ; } + Disjunctions:{ { Marked_proper(cons(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(cons(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(recip(X)) > Marked_proper(X) ; } { Marked_proper(terms(X)) > Marked_proper(X) ; } { Marked_proper(s(X)) > Marked_proper(X) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(dbl(X)) > Marked_proper(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_proper(cons(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(cons(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(recip(X)) >= Marked_proper(X) constraint: Marked_proper(terms(X)) >= Marked_proper(X) constraint: Marked_proper(s(X)) >= Marked_proper(X) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(dbl(X)) >= Marked_proper(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_proper(cons(X1,X2)) >= Marked_proper(X1) ; Marked_proper(cons(X1,X2)) >= Marked_proper(X2) ; Marked_proper(recip(X)) >= Marked_proper(X) ; Marked_proper(s(X)) >= Marked_proper(X) ; Marked_proper(add(X1,X2)) >= Marked_proper(X1) ; Marked_proper(add(X1,X2)) >= Marked_proper(X2) ; Marked_proper(dbl(X)) >= Marked_proper(X) ; } + Disjunctions:{ { Marked_proper(cons(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(cons(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(recip(X)) > Marked_proper(X) ; } { Marked_proper(s(X)) > Marked_proper(X) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(dbl(X)) > Marked_proper(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_proper(cons(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(cons(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(recip(X)) >= Marked_proper(X) constraint: Marked_proper(s(X)) >= Marked_proper(X) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(dbl(X)) >= Marked_proper(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_proper(recip(X)) >= Marked_proper(X) ; Marked_proper(s(X)) >= Marked_proper(X) ; Marked_proper(add(X1,X2)) >= Marked_proper(X1) ; Marked_proper(add(X1,X2)) >= Marked_proper(X2) ; Marked_proper(dbl(X)) >= Marked_proper(X) ; } + Disjunctions:{ { Marked_proper(recip(X)) > Marked_proper(X) ; } { Marked_proper(s(X)) > Marked_proper(X) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(dbl(X)) > Marked_proper(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_proper(recip(X)) >= Marked_proper(X) constraint: Marked_proper(s(X)) >= Marked_proper(X) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(dbl(X)) >= Marked_proper(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_proper(recip(X)) >= Marked_proper(X) ; Marked_proper(add(X1,X2)) >= Marked_proper(X1) ; Marked_proper(add(X1,X2)) >= Marked_proper(X2) ; Marked_proper(dbl(X)) >= Marked_proper(X) ; } + Disjunctions:{ { Marked_proper(recip(X)) > Marked_proper(X) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(dbl(X)) > Marked_proper(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_proper(recip(X)) >= Marked_proper(X) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(dbl(X)) >= Marked_proper(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_proper(add(X1,X2)) >= Marked_proper(X1) ; Marked_proper(add(X1,X2)) >= Marked_proper(X2) ; Marked_proper(dbl(X)) >= Marked_proper(X) ; } + Disjunctions:{ { Marked_proper(add(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X2) ; } { Marked_proper(dbl(X)) > Marked_proper(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X2) constraint: Marked_proper(dbl(X)) >= Marked_proper(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_proper(add(X1,X2)) >= Marked_proper(X1) ; Marked_proper(add(X1,X2)) >= Marked_proper(X2) ; } + Disjunctions:{ { Marked_proper(add(X1,X2)) > Marked_proper(X1) ; } { Marked_proper(add(X1,X2)) > Marked_proper(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X1) constraint: Marked_proper(add(X1,X2)) >= Marked_proper(X2) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_active(cons(X1,X2)) >= Marked_active(X1) ; Marked_active(sqr(X)) >= Marked_active(X) ; Marked_active(terms(X)) >= Marked_active(X) ; Marked_active(s(X)) >= Marked_active(X) ; Marked_active(add(X1,X2)) >= Marked_active(X1) ; Marked_active(add(X1,X2)) >= Marked_active(X2) ; Marked_active(dbl(X)) >= Marked_active(X) ; Marked_active(first(X1,X2)) >= Marked_active(X1) ; Marked_active(first(X1,X2)) >= Marked_active(X2) ; } + Disjunctions:{ { Marked_active(cons(X1,X2)) > Marked_active(X1) ; } { Marked_active(sqr(X)) > Marked_active(X) ; } { Marked_active(terms(X)) > Marked_active(X) ; } { Marked_active(s(X)) > Marked_active(X) ; } { Marked_active(add(X1,X2)) > Marked_active(X1) ; } { Marked_active(add(X1,X2)) > Marked_active(X2) ; } { Marked_active(dbl(X)) > Marked_active(X) ; } { Marked_active(first(X1,X2)) > Marked_active(X1) ; } { Marked_active(first(X1,X2)) > Marked_active(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_active(cons(X1,X2)) >= Marked_active(X1) constraint: Marked_active(sqr(X)) >= Marked_active(X) constraint: Marked_active(terms(X)) >= Marked_active(X) constraint: Marked_active(s(X)) >= Marked_active(X) constraint: Marked_active(add(X1,X2)) >= Marked_active(X1) constraint: Marked_active(add(X1,X2)) >= Marked_active(X2) constraint: Marked_active(dbl(X)) >= Marked_active(X) constraint: Marked_active(first(X1,X2)) >= Marked_active(X1) constraint: Marked_active(first(X1,X2)) >= Marked_active(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_active(sqr(X)) >= Marked_active(X) ; Marked_active(terms(X)) >= Marked_active(X) ; Marked_active(s(X)) >= Marked_active(X) ; Marked_active(add(X1,X2)) >= Marked_active(X1) ; Marked_active(add(X1,X2)) >= Marked_active(X2) ; Marked_active(dbl(X)) >= Marked_active(X) ; Marked_active(first(X1,X2)) >= Marked_active(X1) ; Marked_active(first(X1,X2)) >= Marked_active(X2) ; } + Disjunctions:{ { Marked_active(sqr(X)) > Marked_active(X) ; } { Marked_active(terms(X)) > Marked_active(X) ; } { Marked_active(s(X)) > Marked_active(X) ; } { Marked_active(add(X1,X2)) > Marked_active(X1) ; } { Marked_active(add(X1,X2)) > Marked_active(X2) ; } { Marked_active(dbl(X)) > Marked_active(X) ; } { Marked_active(first(X1,X2)) > Marked_active(X1) ; } { Marked_active(first(X1,X2)) > Marked_active(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_active(sqr(X)) >= Marked_active(X) constraint: Marked_active(terms(X)) >= Marked_active(X) constraint: Marked_active(s(X)) >= Marked_active(X) constraint: Marked_active(add(X1,X2)) >= Marked_active(X1) constraint: Marked_active(add(X1,X2)) >= Marked_active(X2) constraint: Marked_active(dbl(X)) >= Marked_active(X) constraint: Marked_active(first(X1,X2)) >= Marked_active(X1) constraint: Marked_active(first(X1,X2)) >= Marked_active(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_active(sqr(X)) >= Marked_active(X) ; Marked_active(terms(X)) >= Marked_active(X) ; Marked_active(add(X1,X2)) >= Marked_active(X1) ; Marked_active(add(X1,X2)) >= Marked_active(X2) ; Marked_active(dbl(X)) >= Marked_active(X) ; Marked_active(first(X1,X2)) >= Marked_active(X1) ; Marked_active(first(X1,X2)) >= Marked_active(X2) ; } + Disjunctions:{ { Marked_active(sqr(X)) > Marked_active(X) ; } { Marked_active(terms(X)) > Marked_active(X) ; } { Marked_active(add(X1,X2)) > Marked_active(X1) ; } { Marked_active(add(X1,X2)) > Marked_active(X2) ; } { Marked_active(dbl(X)) > Marked_active(X) ; } { Marked_active(first(X1,X2)) > Marked_active(X1) ; } { Marked_active(first(X1,X2)) > Marked_active(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_active(sqr(X)) >= Marked_active(X) constraint: Marked_active(terms(X)) >= Marked_active(X) constraint: Marked_active(add(X1,X2)) >= Marked_active(X1) constraint: Marked_active(add(X1,X2)) >= Marked_active(X2) constraint: Marked_active(dbl(X)) >= Marked_active(X) constraint: Marked_active(first(X1,X2)) >= Marked_active(X1) constraint: Marked_active(first(X1,X2)) >= Marked_active(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_active(sqr(X)) >= Marked_active(X) ; Marked_active(terms(X)) >= Marked_active(X) ; Marked_active(add(X1,X2)) >= Marked_active(X1) ; Marked_active(add(X1,X2)) >= Marked_active(X2) ; Marked_active(dbl(X)) >= Marked_active(X) ; } + Disjunctions:{ { Marked_active(sqr(X)) > Marked_active(X) ; } { Marked_active(terms(X)) > Marked_active(X) ; } { Marked_active(add(X1,X2)) > Marked_active(X1) ; } { Marked_active(add(X1,X2)) > Marked_active(X2) ; } { Marked_active(dbl(X)) > Marked_active(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_active(sqr(X)) >= Marked_active(X) constraint: Marked_active(terms(X)) >= Marked_active(X) constraint: Marked_active(add(X1,X2)) >= Marked_active(X1) constraint: Marked_active(add(X1,X2)) >= Marked_active(X2) constraint: Marked_active(dbl(X)) >= Marked_active(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_active(sqr(X)) >= Marked_active(X) ; Marked_active(terms(X)) >= Marked_active(X) ; Marked_active(add(X1,X2)) >= Marked_active(X1) ; Marked_active(add(X1,X2)) >= Marked_active(X2) ; } + Disjunctions:{ { Marked_active(sqr(X)) > Marked_active(X) ; } { Marked_active(terms(X)) > Marked_active(X) ; } { Marked_active(add(X1,X2)) > Marked_active(X1) ; } { Marked_active(add(X1,X2)) > Marked_active(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_active(sqr(X)) >= Marked_active(X) constraint: Marked_active(terms(X)) >= Marked_active(X) constraint: Marked_active(add(X1,X2)) >= Marked_active(X1) constraint: Marked_active(add(X1,X2)) >= Marked_active(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_active(sqr(X)) >= Marked_active(X) ; Marked_active(add(X1,X2)) >= Marked_active(X1) ; Marked_active(add(X1,X2)) >= Marked_active(X2) ; } + Disjunctions:{ { Marked_active(sqr(X)) > Marked_active(X) ; } { Marked_active(add(X1,X2)) > Marked_active(X1) ; } { Marked_active(add(X1,X2)) > Marked_active(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_active(sqr(X)) >= Marked_active(X) constraint: Marked_active(add(X1,X2)) >= Marked_active(X1) constraint: Marked_active(add(X1,X2)) >= Marked_active(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_active(sqr(X)) >= Marked_active(X) ; } + Disjunctions:{ { Marked_active(sqr(X)) > Marked_active(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_active(sqr(X)) >= Marked_active(X) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_terms(mark(X)) >= Marked_terms(X) ; } + Disjunctions:{ { Marked_terms(mark(X)) > Marked_terms(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_terms(mark(X)) >= Marked_terms(X) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_cons(mark(X1),X2) >= Marked_cons(X1,X2) ; } + Disjunctions:{ { Marked_cons(mark(X1),X2) > Marked_cons(X1,X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_cons(mark(X1),X2) >= Marked_cons(X1,X2) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_recip(mark(X)) >= Marked_recip(X) ; } + Disjunctions:{ { Marked_recip(mark(X)) > Marked_recip(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_recip(mark(X)) >= Marked_recip(X) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_sqr(mark(X)) >= Marked_sqr(X) ; } + Disjunctions:{ { Marked_sqr(mark(X)) > Marked_sqr(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_sqr(mark(X)) >= Marked_sqr(X) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_s(ok(X)) >= Marked_s(X) ; } + Disjunctions:{ { Marked_s(ok(X)) > Marked_s(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_s(ok(X)) >= Marked_s(X) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_add(mark(X1),X2) >= Marked_add(X1,X2) ; Marked_add(X1,mark(X2)) >= Marked_add(X1,X2) ; } + Disjunctions:{ { Marked_add(mark(X1),X2) > Marked_add(X1,X2) ; } { Marked_add(X1,mark(X2)) > Marked_add(X1,X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_add(mark(X1),X2) >= Marked_add(X1,X2) constraint: Marked_add(X1,mark(X2)) >= Marked_add(X1,X2) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_dbl(mark(X)) >= Marked_dbl(X) ; } + Disjunctions:{ { Marked_dbl(mark(X)) > Marked_dbl(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: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_dbl(mark(X)) >= Marked_dbl(X) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(mark(X1),X2) >= mark(cons(X1,X2)) ; cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) ; recip(mark(X)) >= mark(recip(X)) ; recip(ok(X)) >= ok(recip(X)) ; sqr(mark(X)) >= mark(sqr(X)) ; sqr(ok(X)) >= ok(sqr(X)) ; terms(mark(X)) >= mark(terms(X)) ; terms(ok(X)) >= ok(terms(X)) ; s(mark(X)) >= mark(s(X)) ; s(ok(X)) >= ok(s(X)) ; active(cons(X1,X2)) >= cons(active(X1),X2) ; active(recip(X)) >= recip(active(X)) ; active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) ; active(sqr(0)) >= mark(0) ; active(sqr(X)) >= sqr(active(X)) ; active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) ; active(terms(X)) >= terms(active(X)) ; active(s(X)) >= s(active(X)) ; active(add(s(X),Y)) >= mark(s(add(X,Y))) ; active(add(0,X)) >= mark(X) ; active(add(X1,X2)) >= add(active(X1),X2) ; active(add(X1,X2)) >= add(X1,active(X2)) ; active(dbl(s(X))) >= mark(s(s(dbl(X)))) ; active(dbl(0)) >= mark(0) ; active(dbl(X)) >= dbl(active(X)) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,X)) >= mark(nil) ; active(first(X1,X2)) >= first(active(X1),X2) ; active(first(X1,X2)) >= first(X1,active(X2)) ; add(mark(X1),X2) >= mark(add(X1,X2)) ; add(ok(X1),ok(X2)) >= ok(add(X1,X2)) ; add(X1,mark(X2)) >= mark(add(X1,X2)) ; dbl(mark(X)) >= mark(dbl(X)) ; dbl(ok(X)) >= ok(dbl(X)) ; first(mark(X1),X2) >= mark(first(X1,X2)) ; first(ok(X1),ok(X2)) >= ok(first(X1,X2)) ; first(X1,mark(X2)) >= mark(first(X1,X2)) ; proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) ; proper(recip(X)) >= recip(proper(X)) ; proper(sqr(X)) >= sqr(proper(X)) ; proper(terms(X)) >= terms(proper(X)) ; proper(s(X)) >= s(proper(X)) ; proper(0) >= ok(0) ; proper(add(X1,X2)) >= add(proper(X1),proper(X2)) ; proper(dbl(X)) >= dbl(proper(X)) ; proper(nil) >= ok(nil) ; proper(first(X1,X2)) >= first(proper(X1),proper(X2)) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_first(mark(X1),X2) >= Marked_first(X1,X2) ; Marked_first(X1,mark(X2)) >= Marked_first(X1,X2) ; } + Disjunctions:{ { Marked_first(mark(X1),X2) > Marked_first(X1,X2) ; } { Marked_first(X1,mark(X2)) > Marked_first(X1,X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(mark(X1),X2) >= mark(cons(X1,X2)) constraint: cons(ok(X1),ok(X2)) >= ok(cons(X1,X2)) constraint: recip(mark(X)) >= mark(recip(X)) constraint: recip(ok(X)) >= ok(recip(X)) constraint: sqr(mark(X)) >= mark(sqr(X)) constraint: sqr(ok(X)) >= ok(sqr(X)) constraint: terms(mark(X)) >= mark(terms(X)) constraint: terms(ok(X)) >= ok(terms(X)) constraint: s(mark(X)) >= mark(s(X)) constraint: s(ok(X)) >= ok(s(X)) constraint: active(cons(X1,X2)) >= cons(active(X1),X2) constraint: active(recip(X)) >= recip(active(X)) constraint: active(sqr(s(X))) >= mark(s(add(sqr(X),dbl(X)))) constraint: active(sqr(0)) >= mark(0) constraint: active(sqr(X)) >= sqr(active(X)) constraint: active(terms(N)) >= mark(cons(recip(sqr(N)),terms(s(N)))) constraint: active(terms(X)) >= terms(active(X)) constraint: active(s(X)) >= s(active(X)) constraint: active(add(s(X),Y)) >= mark(s(add(X,Y))) constraint: active(add(0,X)) >= mark(X) constraint: active(add(X1,X2)) >= add(active(X1),X2) constraint: active(add(X1,X2)) >= add(X1,active(X2)) constraint: active(dbl(s(X))) >= mark(s(s(dbl(X)))) constraint: active(dbl(0)) >= mark(0) constraint: active(dbl(X)) >= dbl(active(X)) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,X)) >= mark(nil) constraint: active(first(X1,X2)) >= first(active(X1),X2) constraint: active(first(X1,X2)) >= first(X1,active(X2)) constraint: add(mark(X1),X2) >= mark(add(X1,X2)) constraint: add(ok(X1),ok(X2)) >= ok(add(X1,X2)) constraint: add(X1,mark(X2)) >= mark(add(X1,X2)) constraint: dbl(mark(X)) >= mark(dbl(X)) constraint: dbl(ok(X)) >= ok(dbl(X)) constraint: first(mark(X1),X2) >= mark(first(X1,X2)) constraint: first(ok(X1),ok(X2)) >= ok(first(X1,X2)) constraint: first(X1,mark(X2)) >= mark(first(X1,X2)) constraint: proper(cons(X1,X2)) >= cons(proper(X1),proper(X2)) constraint: proper(recip(X)) >= recip(proper(X)) constraint: proper(sqr(X)) >= sqr(proper(X)) constraint: proper(terms(X)) >= terms(proper(X)) constraint: proper(s(X)) >= s(proper(X)) constraint: proper(0) >= ok(0) constraint: proper(add(X1,X2)) >= add(proper(X1),proper(X2)) constraint: proper(dbl(X)) >= dbl(proper(X)) constraint: proper(nil) >= ok(nil) constraint: proper(first(X1,X2)) >= first(proper(X1),proper(X2)) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_first(mark(X1),X2) >= Marked_first(X1,X2) constraint: Marked_first(X1,mark(X2)) >= Marked_first(X1,X2) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) [2] active(sqr(0)) -> mark(0) [3] active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) [4] active(dbl(0)) -> mark(0) [5] active(dbl(s(X))) -> mark(s(s(dbl(X)))) [6] active(add(0,X)) -> mark(X) [7] active(add(s(X),Y)) -> mark(s(add(X,Y))) [8] active(first(0,X)) -> mark(nil) [9] active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) [10] active(terms(X)) -> terms(active(X)) [11] active(cons(X1,X2)) -> cons(active(X1),X2) [12] active(recip(X)) -> recip(active(X)) [13] active(sqr(X)) -> sqr(active(X)) [14] active(s(X)) -> s(active(X)) [15] active(add(X1,X2)) -> add(active(X1),X2) [16] active(add(X1,X2)) -> add(X1,active(X2)) [17] active(dbl(X)) -> dbl(active(X)) [18] active(first(X1,X2)) -> first(active(X1),X2) [19] active(first(X1,X2)) -> first(X1,active(X2)) [20] terms(mark(X)) -> mark(terms(X)) [21] cons(mark(X1),X2) -> mark(cons(X1,X2)) [22] recip(mark(X)) -> mark(recip(X)) [23] sqr(mark(X)) -> mark(sqr(X)) [24] s(mark(X)) -> mark(s(X)) [25] add(mark(X1),X2) -> mark(add(X1,X2)) [26] add(X1,mark(X2)) -> mark(add(X1,X2)) [27] dbl(mark(X)) -> mark(dbl(X)) [28] first(mark(X1),X2) -> mark(first(X1,X2)) [29] first(X1,mark(X2)) -> mark(first(X1,X2)) [30] proper(terms(X)) -> terms(proper(X)) [31] proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) [32] proper(recip(X)) -> recip(proper(X)) [33] proper(sqr(X)) -> sqr(proper(X)) [34] proper(s(X)) -> s(proper(X)) [35] proper(0) -> ok(0) [36] proper(add(X1,X2)) -> add(proper(X1),proper(X2)) [37] proper(dbl(X)) -> dbl(proper(X)) [38] proper(first(X1,X2)) -> first(proper(X1),proper(X2)) [39] proper(nil) -> ok(nil) [40] terms(ok(X)) -> ok(terms(X)) [41] cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) [42] recip(ok(X)) -> ok(recip(X)) [43] sqr(ok(X)) -> ok(sqr(X)) [44] s(ok(X)) -> ok(s(X)) [45] add(ok(X1),ok(X2)) -> ok(add(X1,X2)) [46] dbl(ok(X)) -> ok(dbl(X)) [47] first(ok(X1),ok(X2)) -> ok(first(X1,X2)) [48] top(mark(X)) -> top(proper(X)) [49] top(ok(X)) -> top(active(X)) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using RPO with AFS = AFS: proper -> 0active -> 0cons -> 0ok -> 0 and precedence: prec (All symbols are Lex.): { mark < recip ; mark < sqr ; mark < terms ; mark < s ; mark < add ; mark < dbl ; mark < first ; recip > mark ; recip < terms ; sqr > mark ; sqr < terms ; sqr > s ; sqr > add ; sqr > dbl ; terms > mark ; terms > recip ; terms > sqr ; terms > s ; terms > add ; terms > dbl ; s > mark ; s < sqr ; s < terms ; s < add ; s < dbl ; add > mark ; add < sqr ; add < terms ; add > s ; dbl > mark ; dbl < sqr ; dbl < terms ; dbl > s ; nil < first ; first > mark ; first > nil ; } removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X1 + 0; [ terms ] (X0) = 2*X0 + 0; [ proper ] (X0) = 3*X0 + 0; [ recip ] (X0) = 2*X0 + 0; [ nil ] () = 3 + 0; [ active ] (X0) = 1*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2 + 2*X0 + 0; [ dbl ] (X0) = 3*X0 + 0; [ s ] (X0) = 2*X0 + 0; [ ok ] (X0) = 3 + 2*X0 + 0; [ sqr ] (X0) = 3*X0 + 0; [ first ] (X0,X1) = 3*X1 + 0; [ 0 ] () = 3 + 0; [ Marked_top ] (X0) = 2*X0 + 0; ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 2*X0; [ recip ] (X0) = 2*X0; [ nil ] () = 2; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X1 + 1*X0; [ Marked_proper ] (X0) = 3*X0; [ dbl ] (X0) = 2*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 0; [ sqr ] (X0) = 1*X0 + 1; [ first ] (X0,X1) = 2*X1 + 2*X0; [ 0 ] () = 3; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 2*X0; [ nil ] () = 0; [ active ] (X0) = 1*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X1 + 2*X0; [ Marked_proper ] (X0) = 3*X0; [ dbl ] (X0) = 2*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 0; [ sqr ] (X0) = 0; [ first ] (X0,X1) = 1*X1 + 1*X0 + 1; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 2*X0 + 2; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 1*X0; [ nil ] () = 0; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X1 + 2*X0; [ Marked_proper ] (X0) = 3*X0; [ dbl ] (X0) = 3*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 0; [ sqr ] (X0) = 0; [ first ] (X0,X1) = 1*X1 + 3*X0; [ 0 ] () = 1; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 0; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 1*X0; [ nil ] () = 0; [ active ] (X0) = 1*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X1 + 1*X0 + 2; [ Marked_proper ] (X0) = 3*X0; [ dbl ] (X0) = 1*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 0; [ sqr ] (X0) = 0; [ first ] (X0,X1) = 3*X0; [ 0 ] () = 2; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X1 + 1*X0; [ terms ] (X0) = 1; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 2*X0; [ nil ] () = 2; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2; [ Marked_proper ] (X0) = 3*X0; [ dbl ] (X0) = 2*X0; [ s ] (X0) = 1*X0 + 1; [ ok ] (X0) = 0; [ sqr ] (X0) = 1; [ first ] (X0,X1) = 0; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X1 + 1*X0; [ terms ] (X0) = 0; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 2*X0 + 1; [ nil ] () = 0; [ active ] (X0) = 1*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0; [ Marked_proper ] (X0) = 3*X0; [ dbl ] (X0) = 1*X0; [ s ] (X0) = 1; [ ok ] (X0) = 0; [ sqr ] (X0) = 3*X0 + 1; [ first ] (X0,X1) = 2*X1 + 1; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 3*X0; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 0; [ nil ] () = 0; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0; [ Marked_proper ] (X0) = 3*X0; [ dbl ] (X0) = 1*X0 + 1; [ s ] (X0) = 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 0; [ first ] (X0,X1) = 3*X1; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 1 + 2*X0 + 2*X1 + 0; [ terms ] (X0) = 0; [ proper ] (X0) = 1*X0 + 0; [ recip ] (X0) = 0; [ nil ] () = 0; [ active ] (X0) = 1*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 0; [ Marked_proper ] (X0) = 3*X0 + 0; [ dbl ] (X0) = 0; [ s ] (X0) = 2 + 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 1 + 0; [ first ] (X0,X1) = 1*X0 + 0; [ 0 ] () = 0; ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ Marked_active ] (X0) = 3*X0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 2*X0; [ proper ] (X0) = 2*X0; [ recip ] (X0) = 1*X0 + 1; [ nil ] () = 0; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 3*X1 + 1*X0; [ dbl ] (X0) = 2*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 0; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 2*X1 + 2*X0; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ Marked_active ] (X0) = 3*X0; [ add ] (X0,X1) = 2*X1 + 1*X0; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 0; [ nil ] () = 0; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 3*X1 + 1*X0 + 2; [ dbl ] (X0) = 2*X0; [ s ] (X0) = 1*X0; [ ok ] (X0) = 0; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 2*X1 + 2*X0; [ 0 ] () = 1; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ Marked_active ] (X0) = 3*X0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 0; [ nil ] () = 0; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0; [ dbl ] (X0) = 2*X0; [ s ] (X0) = 2*X0 + 1; [ ok ] (X0) = 0; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 2*X1 + 2*X0; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ Marked_active ] (X0) = 3*X0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 1*X0; [ nil ] () = 2; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 1*X0; [ dbl ] (X0) = 1*X0; [ s ] (X0) = 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 1*X1 + 1*X0 + 2; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ Marked_active ] (X0) = 3*X0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 0; [ nil ] () = 0; [ active ] (X0) = 1*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 0; [ dbl ] (X0) = 1*X0 + 1; [ s ] (X0) = 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 1*X0; [ first ] (X0,X1) = 3*X0 + 2; [ 0 ] () = 3; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ Marked_active ] (X0) = 3*X0; [ add ] (X0,X1) = 2*X1 + 2*X0; [ terms ] (X0) = 2*X0 + 1; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 2; [ nil ] () = 0; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 1*X1; [ dbl ] (X0) = 0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 0; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 0; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ Marked_active ] (X0) = 3*X0; [ add ] (X0,X1) = 2*X1 + 1*X0 + 1; [ terms ] (X0) = 2; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 0; [ nil ] () = 0; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0; [ dbl ] (X0) = 0; [ s ] (X0) = 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 1*X0; [ first ] (X0,X1) = 3*X1 + 2; [ 0 ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 0; [ Marked_active ] (X0) = 3*X0 + 0; [ add ] (X0,X1) = 1 + 3*X0 + 3*X1 + 0; [ terms ] (X0) = 3 + 0; [ proper ] (X0) = 2*X0 + 0; [ recip ] (X0) = 2 + 0; [ nil ] () = 1 + 0; [ active ] (X0) = 2*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 3*X0 + 0; [ dbl ] (X0) = 2 + 3*X0 + 0; [ s ] (X0) = 2*X0 + 0; [ ok ] (X0) = 1*X0 + 0; [ sqr ] (X0) = 2 + 2*X0 + 0; [ first ] (X0,X1) = 1 + 1*X0 + 2*X1 + 0; [ 0 ] () = 0; ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ add ] (X0,X1) = 2*X1; [ terms ] (X0) = 2*X0; [ proper ] (X0) = 3*X0; [ recip ] (X0) = 1*X0; [ nil ] () = 1; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 1*X1; [ dbl ] (X0) = 2*X0; [ Marked_terms ] (X0) = 3*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 2*X0 + 1; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 1*X1 + 3*X0; [ 0 ] () = 2; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 1*X0 + 0; [ add ] (X0,X1) = 1*X0 + 1*X1 + 0; [ terms ] (X0) = 1 + 3*X0 + 0; [ proper ] (X0) = 2*X0 + 0; [ recip ] (X0) = 1*X0 + 0; [ nil ] () = 1 + 0; [ active ] (X0) = 2*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0 + 0; [ dbl ] (X0) = 2 + 3*X0 + 0; [ Marked_terms ] (X0) = 3*X0 + 0; [ s ] (X0) = 3 + 2*X0 + 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 3*X0 + 0; [ first ] (X0,X1) = 2*X0 + 1*X1 + 0; [ 0 ] () = 1 + 0; ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ add ] (X0,X1) = 2*X0; [ Marked_cons ] (X0,X1) = 1*X1; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 3*X0; [ recip ] (X0) = 1*X0; [ nil ] () = 2; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 3*X1; [ dbl ] (X0) = 3*X0 + 1; [ s ] (X0) = 3*X0 + 1; [ ok ] (X0) = 2*X0 + 1; [ sqr ] (X0) = 1*X0; [ first ] (X0,X1) = 2*X1; [ 0 ] () = 3; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 1*X0 + 0; [ add ] (X0,X1) = 1*X0 + 1*X1 + 0; [ Marked_cons ] (X0,X1) = 3*X0 + 0; [ terms ] (X0) = 2 + 2*X0 + 0; [ proper ] (X0) = 1*X0 + 0; [ recip ] (X0) = 2*X0 + 0; [ nil ] () = 0; [ active ] (X0) = 3*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0 + 0; [ dbl ] (X0) = 2*X0 + 0; [ s ] (X0) = 1 + 2*X0 + 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 1*X0 + 0; [ first ] (X0,X1) = 1*X0 + 2*X1 + 0; [ 0 ] () = 2 + 0; ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ add ] (X0,X1) = 2*X1; [ terms ] (X0) = 2*X0; [ proper ] (X0) = 3*X0; [ recip ] (X0) = 1*X0; [ nil ] () = 2; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0; [ dbl ] (X0) = 1*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 2*X0 + 1; [ sqr ] (X0) = 1*X0; [ first ] (X0,X1) = 3*X1 + 3*X0 + 3; [ 0 ] () = 2; [ Marked_recip ] (X0) = 3*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 1*X0 + 0; [ add ] (X0,X1) = 1*X0 + 1*X1 + 0; [ terms ] (X0) = 3 + 2*X0 + 0; [ proper ] (X0) = 1*X0 + 0; [ recip ] (X0) = 1*X0 + 0; [ nil ] () = 2 + 0; [ active ] (X0) = 3*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0 + 1*X1 + 0; [ dbl ] (X0) = 2*X0 + 0; [ s ] (X0) = 2 + 2*X0 + 0; [ ok ] (X0) = 2 + 0; [ sqr ] (X0) = 1*X0 + 0; [ first ] (X0,X1) = 2 + 2*X0 + 1*X1 + 0; [ 0 ] () = 3 + 0; [ Marked_recip ] (X0) = 3*X0 + 0; ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ add ] (X0,X1) = 1*X1; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 3*X0; [ recip ] (X0) = 1*X0; [ nil ] () = 1; [ active ] (X0) = 1*X0; [ Marked_sqr ] (X0) = 3*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 1*X1; [ dbl ] (X0) = 1*X0; [ s ] (X0) = 1*X0; [ ok ] (X0) = 2*X0 + 1; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 2*X0; [ 0 ] () = 2; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 1*X0 + 0; [ add ] (X0,X1) = 1*X0 + 1*X1 + 0; [ terms ] (X0) = 3 + 2*X0 + 0; [ proper ] (X0) = 2*X0 + 0; [ recip ] (X0) = 1*X0 + 0; [ nil ] () = 1 + 0; [ active ] (X0) = 3*X0 + 0; [ Marked_sqr ] (X0) = 3*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2 + 2*X0 + 1*X1 + 0; [ dbl ] (X0) = 2*X0 + 0; [ s ] (X0) = 1 + 2*X0 + 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 1*X0 + 0; [ first ] (X0,X1) = 3*X0 + 3*X1 + 0; [ 0 ] () = 1 + 0; ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0 + 1; [ add ] (X0,X1) = 1*X1 + 2*X0; [ terms ] (X0) = 3*X0 + 2; [ proper ] (X0) = 1*X0; [ recip ] (X0) = 2*X0; [ nil ] () = 3; [ active ] (X0) = 3*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0 + 1; [ dbl ] (X0) = 1*X0; [ s ] (X0) = 1*X0 + 2; [ Marked_s ] (X0) = 3*X0; [ ok ] (X0) = 1*X0; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 2*X1 + 2*X0; [ 0 ] () = 2; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 0; [ add ] (X0,X1) = 2 + 2*X0 + 0; [ terms ] (X0) = 1 + 2*X0 + 0; [ proper ] (X0) = 3*X0 + 0; [ recip ] (X0) = 1*X0 + 0; [ nil ] () = 3 + 0; [ active ] (X0) = 2*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2 + 3*X0 + 0; [ dbl ] (X0) = 2*X0 + 0; [ s ] (X0) = 1 + 2*X0 + 0; [ Marked_s ] (X0) = 3*X0 + 0; [ ok ] (X0) = 2 + 2*X0 + 0; [ sqr ] (X0) = 1*X0 + 0; [ first ] (X0,X1) = 2 + 2*X1 + 0; [ 0 ] () = 2 + 0; ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ add ] (X0,X1) = 1*X1; [ terms ] (X0) = 1*X0; [ Marked_add ] (X0,X1) = 2*X0; [ proper ] (X0) = 3*X0; [ recip ] (X0) = 1*X0; [ nil ] () = 2; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2*X0; [ dbl ] (X0) = 2*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 1*X0 + 2; [ sqr ] (X0) = 1*X0; [ first ] (X0,X1) = 2*X1 + 1*X0; [ 0 ] () = 3; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 1 + 1*X0 + 0; [ add ] (X0,X1) = 1*X0 + 2*X1 + 0; [ terms ] (X0) = 3 + 2*X0 + 0; [ Marked_add ] (X0,X1) = 3*X0 + 3*X1 + 0; [ proper ] (X0) = 1*X0 + 0; [ recip ] (X0) = 1*X0 + 0; [ nil ] () = 0; [ active ] (X0) = 3*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 1*X0 + 0; [ dbl ] (X0) = 1 + 3*X0 + 0; [ s ] (X0) = 2 + 2*X0 + 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 3*X0 + 0; [ first ] (X0,X1) = 2*X0 + 1*X1 + 0; [ 0 ] () = 3 + 0; ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ add ] (X0,X1) = 2*X1; [ terms ] (X0) = 2*X0; [ proper ] (X0) = 3*X0; [ recip ] (X0) = 3*X0 + 1; [ nil ] () = 1; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 1*X1; [ dbl ] (X0) = 1*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 2*X0 + 1; [ sqr ] (X0) = 1*X0; [ Marked_dbl ] (X0) = 3*X0; [ first ] (X0,X1) = 1*X0; [ 0 ] () = 1; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 1*X0 + 0; [ add ] (X0,X1) = 1*X0 + 1*X1 + 0; [ terms ] (X0) = 2 + 3*X0 + 0; [ proper ] (X0) = 2*X0 + 0; [ recip ] (X0) = 2*X0 + 0; [ nil ] () = 2 + 0; [ active ] (X0) = 2*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2 + 1*X0 + 0; [ dbl ] (X0) = 2*X0 + 0; [ s ] (X0) = 2 + 2*X0 + 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 2*X0 + 0; [ Marked_dbl ] (X0) = 3*X0 + 0; [ first ] (X0,X1) = 3*X0 + 1*X1 + 0; [ 0 ] () = 1 + 0; ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ add ] (X0,X1) = 2*X1; [ terms ] (X0) = 1*X0; [ proper ] (X0) = 3*X0; [ recip ] (X0) = 2*X0; [ Marked_first ] (X0,X1) = 1*X1 + 3*X0; [ nil ] () = 2; [ active ] (X0) = 2*X0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 1*X1; [ dbl ] (X0) = 2*X0; [ s ] (X0) = 2*X0; [ ok ] (X0) = 2*X0 + 2; [ sqr ] (X0) = 2*X0; [ first ] (X0,X1) = 3*X0 + 2; [ 0 ] () = 2; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 1*X0 + 0; [ add ] (X0,X1) = 1*X0 + 2*X1 + 0; [ terms ] (X0) = 3 + 3*X0 + 0; [ proper ] (X0) = 1*X0 + 0; [ recip ] (X0) = 3*X0 + 0; [ Marked_first ] (X0,X1) = 3*X0 + 3*X1 + 0; [ nil ] () = 0; [ active ] (X0) = 3*X0 + 0; [ top ] (X0) = 0; [ cons ] (X0,X1) = 2 + 3*X0 + 0; [ dbl ] (X0) = 2 + 1*X0 + 0; [ s ] (X0) = 3 + 1*X0 + 0; [ ok ] (X0) = 0; [ sqr ] (X0) = 1*X0 + 0; [ first ] (X0,X1) = 2*X0 + 1*X1 + 0; [ 0 ] () = 1 + 0; ]} ]} ]} ]} ]} Cime worked for 7.658313 seconds (real time) Cime Exit Status: 0