- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(minus(0,Y)) -> mark(0) [2] active(minus(s(X),s(Y))) -> mark(minus(X,Y)) [3] active(geq(X,0)) -> mark(true) [4] active(geq(0,s(Y))) -> mark(false) [5] active(geq(s(X),s(Y))) -> mark(geq(X,Y)) [6] active(div(0,s(Y))) -> mark(0) [7] active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) [8] active(if(true,X,Y)) -> mark(X) [9] active(if(false,X,Y)) -> mark(Y) [10] mark(minus(X1,X2)) -> active(minus(X1,X2)) [11] mark(0) -> active(0) [12] mark(s(X)) -> active(s(mark(X))) [13] mark(geq(X1,X2)) -> active(geq(X1,X2)) [14] mark(true) -> active(true) [15] mark(false) -> active(false) [16] mark(div(X1,X2)) -> active(div(mark(X1),X2)) [17] mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3)) [18] minus(mark(X1),X2) -> minus(X1,X2) [19] minus(X1,mark(X2)) -> minus(X1,X2) [20] minus(active(X1),X2) -> minus(X1,X2) [21] minus(X1,active(X2)) -> minus(X1,X2) [22] s(mark(X)) -> s(X) [23] s(active(X)) -> s(X) [24] geq(mark(X1),X2) -> geq(X1,X2) [25] geq(X1,mark(X2)) -> geq(X1,X2) [26] geq(active(X1),X2) -> geq(X1,X2) [27] geq(X1,active(X2)) -> geq(X1,X2) [28] div(mark(X1),X2) -> div(X1,X2) [29] div(X1,mark(X2)) -> div(X1,X2) [30] div(active(X1),X2) -> div(X1,X2) [31] div(X1,active(X2)) -> div(X1,X2) [32] if(mark(X1),X2,X3) -> if(X1,X2,X3) [33] if(X1,mark(X2),X3) -> if(X1,X2,X3) [34] if(X1,X2,mark(X3)) -> if(X1,X2,X3) [35] if(active(X1),X2,X3) -> if(X1,X2,X3) [36] if(X1,active(X2),X3) -> if(X1,X2,X3) [37] if(X1,X2,active(X3)) -> if(X1,X2,X3) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 6 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) ; Marked_mark(div(X1,X2)) >= Marked_mark(X1) ; Marked_mark(div(X1,X2)) >= Marked_active(div(mark(X1),X2)) ; Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) ; Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) ; Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) ; Marked_active(div(s(X),s(Y))) >= Marked_mark(if(geq(X,Y), s(div(minus(X,Y),s(Y))), 0)) ; Marked_active(if(true,X,Y)) >= Marked_mark(X) ; Marked_active(if(false,X,Y)) >= Marked_mark(Y) ; } + Disjunctions:{ { Marked_mark(minus(X1,X2)) > Marked_active(minus(X1,X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(geq(X1,X2)) > Marked_active(geq(X1,X2)) ; } { Marked_mark(div(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(div(X1,X2)) > Marked_active(div(mark(X1),X2)) ; } { Marked_mark(if(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(if(X1,X2,X3)) > Marked_active(if(mark(X1),X2,X3)) ; } { Marked_active(minus(s(X),s(Y))) > Marked_mark(minus(X,Y)) ; } { Marked_active(geq(s(X),s(Y))) > Marked_mark(geq(X,Y)) ; } { Marked_active(div(s(X),s(Y))) > Marked_mark(if(geq(X,Y), s(div(minus(X,Y),s(Y))), 0)) ; } { Marked_active(if(true,X,Y)) > Marked_mark(X) ; } { Marked_active(if(false,X,Y)) > Marked_mark(Y) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) constraint: Marked_mark(div(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(div(X1,X2)) >= Marked_active(div(mark(X1),X2)) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) constraint: Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) constraint: Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) constraint: Marked_active(div(s(X),s(Y))) >= Marked_mark(if(geq(X,Y), s(div(minus(X,Y), s(Y))),0)) constraint: Marked_active(if(true,X,Y)) >= Marked_mark(X) constraint: Marked_active(if(false,X,Y)) >= Marked_mark(Y) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_minus(mark(X1),X2) >= Marked_minus(X1,X2) ; Marked_minus(active(X1),X2) >= Marked_minus(X1,X2) ; Marked_minus(X1,mark(X2)) >= Marked_minus(X1,X2) ; Marked_minus(X1,active(X2)) >= Marked_minus(X1,X2) ; } + Disjunctions:{ { Marked_minus(mark(X1),X2) > Marked_minus(X1,X2) ; } { Marked_minus(active(X1),X2) > Marked_minus(X1,X2) ; } { Marked_minus(X1,mark(X2)) > Marked_minus(X1,X2) ; } { Marked_minus(X1,active(X2)) > Marked_minus(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: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_minus(mark(X1),X2) >= Marked_minus(X1,X2) constraint: Marked_minus(active(X1),X2) >= Marked_minus(X1,X2) constraint: Marked_minus(X1,mark(X2)) >= Marked_minus(X1,X2) constraint: Marked_minus(X1,active(X2)) >= Marked_minus(X1,X2) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_s(mark(X)) >= Marked_s(X) ; Marked_s(active(X)) >= Marked_s(X) ; } + Disjunctions:{ { Marked_s(mark(X)) > Marked_s(X) ; } { Marked_s(active(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: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_s(mark(X)) >= Marked_s(X) constraint: Marked_s(active(X)) >= Marked_s(X) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_geq(mark(X1),X2) >= Marked_geq(X1,X2) ; Marked_geq(active(X1),X2) >= Marked_geq(X1,X2) ; Marked_geq(X1,mark(X2)) >= Marked_geq(X1,X2) ; Marked_geq(X1,active(X2)) >= Marked_geq(X1,X2) ; } + Disjunctions:{ { Marked_geq(mark(X1),X2) > Marked_geq(X1,X2) ; } { Marked_geq(active(X1),X2) > Marked_geq(X1,X2) ; } { Marked_geq(X1,mark(X2)) > Marked_geq(X1,X2) ; } { Marked_geq(X1,active(X2)) > Marked_geq(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: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_geq(mark(X1),X2) >= Marked_geq(X1,X2) constraint: Marked_geq(active(X1),X2) >= Marked_geq(X1,X2) constraint: Marked_geq(X1,mark(X2)) >= Marked_geq(X1,X2) constraint: Marked_geq(X1,active(X2)) >= Marked_geq(X1,X2) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_div(mark(X1),X2) >= Marked_div(X1,X2) ; Marked_div(active(X1),X2) >= Marked_div(X1,X2) ; Marked_div(X1,mark(X2)) >= Marked_div(X1,X2) ; Marked_div(X1,active(X2)) >= Marked_div(X1,X2) ; } + Disjunctions:{ { Marked_div(mark(X1),X2) > Marked_div(X1,X2) ; } { Marked_div(active(X1),X2) > Marked_div(X1,X2) ; } { Marked_div(X1,mark(X2)) > Marked_div(X1,X2) ; } { Marked_div(X1,active(X2)) > Marked_div(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: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_div(mark(X1),X2) >= Marked_div(X1,X2) constraint: Marked_div(active(X1),X2) >= Marked_div(X1,X2) constraint: Marked_div(X1,mark(X2)) >= Marked_div(X1,X2) constraint: Marked_div(X1,active(X2)) >= Marked_div(X1,X2) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_if(mark(X1),X2,X3) >= Marked_if(X1,X2,X3) ; Marked_if(active(X1),X2,X3) >= Marked_if(X1,X2,X3) ; Marked_if(X1,mark(X2),X3) >= Marked_if(X1,X2,X3) ; Marked_if(X1,active(X2),X3) >= Marked_if(X1,X2,X3) ; Marked_if(X1,X2,mark(X3)) >= Marked_if(X1,X2,X3) ; Marked_if(X1,X2,active(X3)) >= Marked_if(X1,X2,X3) ; } + Disjunctions:{ { Marked_if(mark(X1),X2,X3) > Marked_if(X1,X2,X3) ; } { Marked_if(active(X1),X2,X3) > Marked_if(X1,X2,X3) ; } { Marked_if(X1,mark(X2),X3) > Marked_if(X1,X2,X3) ; } { Marked_if(X1,active(X2),X3) > Marked_if(X1,X2,X3) ; } { Marked_if(X1,X2,mark(X3)) > Marked_if(X1,X2,X3) ; } { Marked_if(X1,X2,active(X3)) > Marked_if(X1,X2,X3) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_if(mark(X1),X2,X3) >= Marked_if(X1,X2,X3) constraint: Marked_if(active(X1),X2,X3) >= Marked_if(X1,X2,X3) constraint: Marked_if(X1,mark(X2),X3) >= Marked_if(X1,X2,X3) constraint: Marked_if(X1,active(X2),X3) >= Marked_if(X1,X2,X3) constraint: Marked_if(X1,X2,mark(X3)) >= Marked_if(X1,X2,X3) constraint: Marked_if(X1,X2,active(X3)) >= Marked_if(X1,X2,X3) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) ; Marked_mark(div(X1,X2)) >= Marked_mark(X1) ; Marked_mark(div(X1,X2)) >= Marked_active(div(mark(X1),X2)) ; Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) ; Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) ; Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) ; Marked_active(div(s(X),s(Y))) >= Marked_mark(if(geq(X,Y), s(div(minus(X,Y),s(Y))), 0)) ; Marked_active(if(true,X,Y)) >= Marked_mark(X) ; Marked_active(if(false,X,Y)) >= Marked_mark(Y) ; } + Disjunctions:{ { Marked_mark(minus(X1,X2)) > Marked_active(minus(X1,X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(geq(X1,X2)) > Marked_active(geq(X1,X2)) ; } { Marked_mark(div(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(div(X1,X2)) > Marked_active(div(mark(X1),X2)) ; } { Marked_mark(if(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(if(X1,X2,X3)) > Marked_active(if(mark(X1),X2,X3)) ; } { Marked_active(minus(s(X),s(Y))) > Marked_mark(minus(X,Y)) ; } { Marked_active(geq(s(X),s(Y))) > Marked_mark(geq(X,Y)) ; } { Marked_active(div(s(X),s(Y))) > Marked_mark(if(geq(X,Y), s(div(minus(X,Y),s(Y))), 0)) ; } { Marked_active(if(true,X,Y)) > Marked_mark(X) ; } { Marked_active(if(false,X,Y)) > Marked_mark(Y) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) constraint: Marked_mark(div(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(div(X1,X2)) >= Marked_active(div(mark(X1),X2)) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) constraint: Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) constraint: Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) constraint: Marked_active(div(s(X),s(Y))) >= Marked_mark(if(geq(X,Y), s(div(minus(X,Y), s(Y))),0)) constraint: Marked_active(if(true,X,Y)) >= Marked_mark(X) constraint: Marked_active(if(false,X,Y)) >= Marked_mark(Y) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) ; Marked_mark(div(X1,X2)) >= Marked_active(div(mark(X1),X2)) ; Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) ; Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) ; Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) ; Marked_active(div(s(X),s(Y))) >= Marked_mark(if(geq(X,Y), s(div(minus(X,Y),s(Y))), 0)) ; Marked_active(if(true,X,Y)) >= Marked_mark(X) ; Marked_active(if(false,X,Y)) >= Marked_mark(Y) ; } + Disjunctions:{ { Marked_mark(minus(X1,X2)) > Marked_active(minus(X1,X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(geq(X1,X2)) > Marked_active(geq(X1,X2)) ; } { Marked_mark(div(X1,X2)) > Marked_active(div(mark(X1),X2)) ; } { Marked_mark(if(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(if(X1,X2,X3)) > Marked_active(if(mark(X1),X2,X3)) ; } { Marked_active(minus(s(X),s(Y))) > Marked_mark(minus(X,Y)) ; } { Marked_active(geq(s(X),s(Y))) > Marked_mark(geq(X,Y)) ; } { Marked_active(div(s(X),s(Y))) > Marked_mark(if(geq(X,Y), s(div(minus(X,Y),s(Y))), 0)) ; } { Marked_active(if(true,X,Y)) > Marked_mark(X) ; } { Marked_active(if(false,X,Y)) > Marked_mark(Y) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) constraint: Marked_mark(div(X1,X2)) >= Marked_active(div(mark(X1),X2)) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) constraint: Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) constraint: Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) constraint: Marked_active(div(s(X),s(Y))) >= Marked_mark(if(geq(X,Y), s(div(minus(X,Y), s(Y))),0)) constraint: Marked_active(if(true,X,Y)) >= Marked_mark(X) constraint: Marked_active(if(false,X,Y)) >= Marked_mark(Y) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) ; Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) ; Marked_mark(div(X1,X2)) >= Marked_active(div(mark(X1),X2)) ; Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) ; Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) ; Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) ; Marked_active(div(s(X),s(Y))) >= Marked_mark(if(geq(X,Y), s(div(minus(X,Y),s(Y))), 0)) ; Marked_active(if(true,X,Y)) >= Marked_mark(X) ; Marked_active(if(false,X,Y)) >= Marked_mark(Y) ; } + Disjunctions:{ { Marked_mark(minus(X1,X2)) > Marked_active(minus(X1,X2)) ; } { Marked_mark(geq(X1,X2)) > Marked_active(geq(X1,X2)) ; } { Marked_mark(div(X1,X2)) > Marked_active(div(mark(X1),X2)) ; } { Marked_mark(if(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(if(X1,X2,X3)) > Marked_active(if(mark(X1),X2,X3)) ; } { Marked_active(minus(s(X),s(Y))) > Marked_mark(minus(X,Y)) ; } { Marked_active(geq(s(X),s(Y))) > Marked_mark(geq(X,Y)) ; } { Marked_active(div(s(X),s(Y))) > Marked_mark(if(geq(X,Y), s(div(minus(X,Y),s(Y))), 0)) ; } { Marked_active(if(true,X,Y)) > Marked_mark(X) ; } { Marked_active(if(false,X,Y)) > Marked_mark(Y) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) constraint: Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) constraint: Marked_mark(div(X1,X2)) >= Marked_active(div(mark(X1),X2)) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) constraint: Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) constraint: Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) constraint: Marked_active(div(s(X),s(Y))) >= Marked_mark(if(geq(X,Y), s(div(minus(X,Y), s(Y))),0)) constraint: Marked_active(if(true,X,Y)) >= Marked_mark(X) constraint: Marked_active(if(false,X,Y)) >= Marked_mark(Y) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) ; Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) ; Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) ; Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) ; Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) ; Marked_active(if(true,X,Y)) >= Marked_mark(X) ; Marked_active(if(false,X,Y)) >= Marked_mark(Y) ; } + Disjunctions:{ { Marked_mark(minus(X1,X2)) > Marked_active(minus(X1,X2)) ; } { Marked_mark(geq(X1,X2)) > Marked_active(geq(X1,X2)) ; } { Marked_mark(if(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(if(X1,X2,X3)) > Marked_active(if(mark(X1),X2,X3)) ; } { Marked_active(minus(s(X),s(Y))) > Marked_mark(minus(X,Y)) ; } { Marked_active(geq(s(X),s(Y))) > Marked_mark(geq(X,Y)) ; } { Marked_active(if(true,X,Y)) > Marked_mark(X) ; } { Marked_active(if(false,X,Y)) > Marked_mark(Y) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) constraint: Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) constraint: Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) constraint: Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) constraint: Marked_active(if(true,X,Y)) >= Marked_mark(X) constraint: Marked_active(if(false,X,Y)) >= Marked_mark(Y) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) ; Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) ; Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) ; Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) ; } + Disjunctions:{ { Marked_mark(minus(X1,X2)) > Marked_active(minus(X1,X2)) ; } { Marked_mark(geq(X1,X2)) > Marked_active(geq(X1,X2)) ; } { Marked_active(minus(s(X),s(Y))) > Marked_mark(minus(X,Y)) ; } { Marked_active(geq(s(X),s(Y))) > Marked_mark(geq(X,Y)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) constraint: Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) constraint: Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) constraint: Marked_active(geq(s(X),s(Y))) >= Marked_mark(geq(X,Y)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) ; Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) ; Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) ; } + Disjunctions:{ { Marked_mark(minus(X1,X2)) > Marked_active(minus(X1,X2)) ; } { Marked_mark(geq(X1,X2)) > Marked_active(geq(X1,X2)) ; } { Marked_active(minus(s(X),s(Y))) > Marked_mark(minus(X,Y)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) constraint: Marked_mark(geq(X1,X2)) >= Marked_active(geq(X1,X2)) constraint: Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) ; Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) ; } + Disjunctions:{ { Marked_mark(minus(X1,X2)) > Marked_active(minus(X1,X2)) ; } { Marked_active(minus(s(X),s(Y))) > Marked_mark(minus(X,Y)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_mark(minus(X1,X2)) >= Marked_active(minus(X1,X2)) constraint: Marked_active(minus(s(X),s(Y))) >= Marked_mark(minus(X,Y)) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(0) >= active(0) ; mark(minus(X1,X2)) >= active(minus(X1,X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(true) >= active(true) ; mark(geq(X1,X2)) >= active(geq(X1,X2)) ; mark(false) >= active(false) ; mark(div(X1,X2)) >= active(div(mark(X1),X2)) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; active(minus(0,Y)) >= mark(0) ; active(minus(s(X),s(Y))) >= mark(minus(X,Y)) ; active(geq(0,s(Y))) >= mark(false) ; active(geq(s(X),s(Y))) >= mark(geq(X,Y)) ; active(geq(X,0)) >= mark(true) ; active(div(0,s(Y))) >= mark(0) ; active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; minus(mark(X1),X2) >= minus(X1,X2) ; minus(active(X1),X2) >= minus(X1,X2) ; minus(X1,mark(X2)) >= minus(X1,X2) ; minus(X1,active(X2)) >= minus(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; geq(mark(X1),X2) >= geq(X1,X2) ; geq(active(X1),X2) >= geq(X1,X2) ; geq(X1,mark(X2)) >= geq(X1,X2) ; geq(X1,active(X2)) >= geq(X1,X2) ; div(mark(X1),X2) >= div(X1,X2) ; div(active(X1),X2) >= div(X1,X2) ; div(X1,mark(X2)) >= div(X1,X2) ; div(X1,active(X2)) >= div(X1,X2) ; if(mark(X1),X2,X3) >= if(X1,X2,X3) ; if(active(X1),X2,X3) >= if(X1,X2,X3) ; if(X1,mark(X2),X3) >= if(X1,X2,X3) ; if(X1,active(X2),X3) >= if(X1,X2,X3) ; if(X1,X2,mark(X3)) >= if(X1,X2,X3) ; if(X1,X2,active(X3)) >= if(X1,X2,X3) ; Marked_minus(X1,mark(X2)) >= Marked_minus(X1,X2) ; Marked_minus(X1,active(X2)) >= Marked_minus(X1,X2) ; } + Disjunctions:{ { Marked_minus(X1,mark(X2)) > Marked_minus(X1,X2) ; } { Marked_minus(X1,active(X2)) > Marked_minus(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: mark(0) >= active(0) constraint: mark(minus(X1,X2)) >= active(minus(X1,X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(true) >= active(true) constraint: mark(geq(X1,X2)) >= active(geq(X1,X2)) constraint: mark(false) >= active(false) constraint: mark(div(X1,X2)) >= active(div(mark(X1),X2)) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: active(minus(0,Y)) >= mark(0) constraint: active(minus(s(X),s(Y))) >= mark(minus(X,Y)) constraint: active(geq(0,s(Y))) >= mark(false) constraint: active(geq(s(X),s(Y))) >= mark(geq(X,Y)) constraint: active(geq(X,0)) >= mark(true) constraint: active(div(0,s(Y))) >= mark(0) constraint: active(div(s(X),s(Y))) >= mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))), 0)) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: minus(mark(X1),X2) >= minus(X1,X2) constraint: minus(active(X1),X2) >= minus(X1,X2) constraint: minus(X1,mark(X2)) >= minus(X1,X2) constraint: minus(X1,active(X2)) >= minus(X1,X2) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: geq(mark(X1),X2) >= geq(X1,X2) constraint: geq(active(X1),X2) >= geq(X1,X2) constraint: geq(X1,mark(X2)) >= geq(X1,X2) constraint: geq(X1,active(X2)) >= geq(X1,X2) constraint: div(mark(X1),X2) >= div(X1,X2) constraint: div(active(X1),X2) >= div(X1,X2) constraint: div(X1,mark(X2)) >= div(X1,X2) constraint: div(X1,active(X2)) >= div(X1,X2) constraint: if(mark(X1),X2,X3) >= if(X1,X2,X3) constraint: if(active(X1),X2,X3) >= if(X1,X2,X3) constraint: if(X1,mark(X2),X3) >= if(X1,X2,X3) constraint: if(X1,active(X2),X3) >= if(X1,X2,X3) constraint: if(X1,X2,mark(X3)) >= if(X1,X2,X3) constraint: if(X1,X2,active(X3)) >= if(X1,X2,X3) constraint: Marked_minus(X1,mark(X2)) >= Marked_minus(X1,X2) constraint: Marked_minus(X1,active(X2)) >= Marked_minus(X1,X2) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] active(minus(0,Y)) -> mark(0) [2] active(minus(s(X),s(Y))) -> mark(minus(X,Y)) [3] active(geq(X,0)) -> mark(true) [4] active(geq(0,s(Y))) -> mark(false) [5] active(geq(s(X),s(Y))) -> mark(geq(X,Y)) [6] active(div(0,s(Y))) -> mark(0) [7] active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)) [8] active(if(true,X,Y)) -> mark(X) [9] active(if(false,X,Y)) -> mark(Y) [10] mark(minus(X1,X2)) -> active(minus(X1,X2)) [11] mark(0) -> active(0) [12] mark(s(X)) -> active(s(mark(X))) [13] mark(geq(X1,X2)) -> active(geq(X1,X2)) [14] mark(true) -> active(true) [15] mark(false) -> active(false) [16] mark(div(X1,X2)) -> active(div(mark(X1),X2)) [17] mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3)) [18] minus(mark(X1),X2) -> minus(X1,X2) [19] minus(X1,mark(X2)) -> minus(X1,X2) [20] minus(active(X1),X2) -> minus(X1,X2) [21] minus(X1,active(X2)) -> minus(X1,X2) [22] s(mark(X)) -> s(X) [23] s(active(X)) -> s(X) [24] geq(mark(X1),X2) -> geq(X1,X2) [25] geq(X1,mark(X2)) -> geq(X1,X2) [26] geq(active(X1),X2) -> geq(X1,X2) [27] geq(X1,active(X2)) -> geq(X1,X2) [28] div(mark(X1),X2) -> div(X1,X2) [29] div(X1,mark(X2)) -> div(X1,X2) [30] div(active(X1),X2) -> div(X1,X2) [31] div(X1,active(X2)) -> div(X1,X2) [32] if(mark(X1),X2,X3) -> if(X1,X2,X3) [33] if(X1,mark(X2),X3) -> if(X1,X2,X3) [34] if(X1,X2,mark(X3)) -> if(X1,X2,X3) [35] if(active(X1),X2,X3) -> if(X1,X2,X3) [36] if(X1,active(X2),X3) -> if(X1,X2,X3) [37] if(X1,X2,active(X3)) -> if(X1,X2,X3) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ Marked_active ] (X0) = 1*X0; [ div ] (X0,X1) = 1; [ s ] (X0) = 0; [ active ] (X0) = 0; [ geq ] (X0,X1) = 1; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 1; [ true ] () = 0; [ minus ] (X0,X1) = 1; [ false ] () = 0; [ Marked_mark ] (X0) = 1; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ Marked_active ] (X0) = 2*X0; [ div ] (X0,X1) = 2*X0 + 1; [ s ] (X0) = 1*X0; [ active ] (X0) = 1*X0; [ geq ] (X0,X1) = 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 1*X2 + 1*X1 + 2*X0; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; [ Marked_mark ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ Marked_active ] (X0) = 2*X0; [ div ] (X0,X1) = 3*X1 + 1*X0; [ s ] (X0) = 1*X0 + 2; [ active ] (X0) = 1*X0; [ geq ] (X0,X1) = 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 2*X2 + 1*X1 + 2*X0; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; [ Marked_mark ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 2*X0; [ Marked_active ] (X0) = 1*X0; [ div ] (X0,X1) = 1; [ s ] (X0) = 0; [ active ] (X0) = 1*X0; [ geq ] (X0,X1) = 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; [ Marked_mark ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 2*X0; [ Marked_active ] (X0) = 1*X0; [ div ] (X0,X1) = 2*X1 + 3*X0 + 3; [ s ] (X0) = 2; [ active ] (X0) = 1*X0; [ geq ] (X0,X1) = 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 3*X2 + 2*X1 + 2*X0 + 2; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; [ Marked_mark ] (X0) = 2*X0; removing < Marked_mark(if(X1,X2,X3)),Marked_mark(X1)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ Marked_active ] (X0) = 2*X0; [ div ] (X0,X1) = 2*X0; [ s ] (X0) = 1*X0 + 1; [ active ] (X0) = 1*X0; [ geq ] (X0,X1) = 1*X1 + 1*X0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 2*X2 + 2*X1; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; [ Marked_mark ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ Marked_active ] (X0) = 0; [ div ] (X0,X1) = 0; [ s ] (X0) = 0; [ active ] (X0) = 0; [ geq ] (X0,X1) = 1; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 0; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; [ Marked_mark ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 1*X0 + 0; [ Marked_active ] (X0) = 2*X0 + 0; [ div ] (X0,X1) = 2 + 3*X0 + 0; [ s ] (X0) = 2 + 2*X0 + 0; [ active ] (X0) = 1*X0 + 0; [ geq ] (X0,X1) = 1 + 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 2*X0 + 1*X1 + 2*X2 + 0; [ true ] () = 1 + 0; [ minus ] (X0,X1) = 1*X0 + 0; [ false ] () = 0; [ Marked_mark ] (X0) = 1 + 3*X0 + 0; ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0 + 1; [ div ] (X0,X1) = 0; [ s ] (X0) = 0; [ active ] (X0) = 1*X0 + 1; [ geq ] (X0,X1) = 1; [ Marked_minus ] (X0,X1) = 2*X0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 2*X2 + 2*X1; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 2*X0 + 0; [ div ] (X0,X1) = 0; [ s ] (X0) = 0; [ active ] (X0) = 2 + 2*X0 + 0; [ geq ] (X0,X1) = 3 + 0; [ Marked_minus ] (X0,X1) = 3*X1 + 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 2*X1 + 2*X2 + 0; [ true ] () = 2 + 0; [ minus ] (X0,X1) = 1 + 0; [ false ] () = 2 + 0; ]} ]} ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 3*X0 + 0; [ div ] (X0,X1) = 2 + 3*X1 + 0; [ s ] (X0) = 3 + 0; [ active ] (X0) = 2 + 3*X0 + 0; [ geq ] (X0,X1) = 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 3*X1 + 3*X2 + 0; [ true ] () = 0; [ Marked_s ] (X0) = 3*X0 + 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 1 + 2*X0 + 0; [ div ] (X0,X1) = 0; [ s ] (X0) = 0; [ Marked_geq ] (X0,X1) = 3*X0 + 3*X1 + 0; [ active ] (X0) = 1 + 2*X0 + 0; [ geq ] (X0,X1) = 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 2*X1 + 2*X2 + 0; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 1 + 2*X0 + 0; [ div ] (X0,X1) = 0; [ s ] (X0) = 0; [ active ] (X0) = 1 + 2*X0 + 0; [ geq ] (X0,X1) = 1 + 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 1*X1 + 1*X2 + 0; [ true ] () = 0; [ minus ] (X0,X1) = 0; [ Marked_div ] (X0,X1) = 3*X0 + 3*X1 + 0; [ false ] () = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 1 + 1*X0 + 0; [ div ] (X0,X1) = 3*X1 + 0; [ s ] (X0) = 3 + 0; [ active ] (X0) = 1 + 1*X0 + 0; [ Marked_if ] (X0,X1,X2) = 3*X0 + 3*X1 + 3*X2 + 0; [ geq ] (X0,X1) = 1 + 0; [ 0 ] () = 0; [ if ] (X0,X1,X2) = 2*X1 + 2*X2 + 0; [ true ] () = 0; [ minus ] (X0,X1) = 1 + 0; [ false ] () = 0; ]} ]} ]} Cime worked for 2.699453 seconds (real time) Cime Exit Status: 0