- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(primes) -> mark(sieve(from(s(s(0))))) [2] active(from(X)) -> mark(cons(X,from(s(X)))) [3] active(head(cons(X,Y))) -> mark(X) [4] active(tail(cons(X,Y))) -> mark(Y) [5] active(if(true,X,Y)) -> mark(X) [6] active(if(false,X,Y)) -> mark(Y) [7] active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) [8] active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) [9] mark(primes) -> active(primes) [10] mark(sieve(X)) -> active(sieve(mark(X))) [11] mark(from(X)) -> active(from(mark(X))) [12] mark(s(X)) -> active(s(mark(X))) [13] mark(0) -> active(0) [14] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [15] mark(head(X)) -> active(head(mark(X))) [16] mark(tail(X)) -> active(tail(mark(X))) [17] mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3)) [18] mark(true) -> active(true) [19] mark(false) -> active(false) [20] mark(filter(X1,X2)) -> active(filter(mark(X1),mark(X2))) [21] mark(divides(X1,X2)) -> active(divides(mark(X1),mark(X2))) [22] sieve(mark(X)) -> sieve(X) [23] sieve(active(X)) -> sieve(X) [24] from(mark(X)) -> from(X) [25] from(active(X)) -> from(X) [26] s(mark(X)) -> s(X) [27] s(active(X)) -> s(X) [28] cons(mark(X1),X2) -> cons(X1,X2) [29] cons(X1,mark(X2)) -> cons(X1,X2) [30] cons(active(X1),X2) -> cons(X1,X2) [31] cons(X1,active(X2)) -> cons(X1,X2) [32] head(mark(X)) -> head(X) [33] head(active(X)) -> head(X) [34] tail(mark(X)) -> tail(X) [35] tail(active(X)) -> tail(X) [36] if(mark(X1),X2,X3) -> if(X1,X2,X3) [37] if(X1,mark(X2),X3) -> if(X1,X2,X3) [38] if(X1,X2,mark(X3)) -> if(X1,X2,X3) [39] if(active(X1),X2,X3) -> if(X1,X2,X3) [40] if(X1,active(X2),X3) -> if(X1,X2,X3) [41] if(X1,X2,active(X3)) -> if(X1,X2,X3) [42] filter(mark(X1),X2) -> filter(X1,X2) [43] filter(X1,mark(X2)) -> filter(X1,X2) [44] filter(active(X1),X2) -> filter(X1,X2) [45] filter(X1,active(X2)) -> filter(X1,X2) [46] divides(mark(X1),X2) -> divides(X1,X2) [47] divides(X1,mark(X2)) -> divides(X1,X2) [48] divides(active(X1),X2) -> divides(X1,X2) [49] divides(X1,active(X2)) -> divides(X1,X2) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 10 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(sieve(X)) >= active(sieve(mark(X))) ; mark(from(X)) >= active(from(mark(X))) ; mark(s(X)) >= active(s(mark(X))) ; mark(0) >= active(0) ; mark(primes) >= active(primes) ; mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(head(X)) >= active(head(mark(X))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; mark(true) >= active(true) ; mark(false) >= active(false) ; mark(divides(X1,X2)) >= active(divides(mark(X1),mark(X2))) ; mark(filter(X1,X2)) >= active(filter(mark(X1),mark(X2))) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; from(mark(X)) >= from(X) ; from(active(X)) >= from(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; active(sieve(cons(X,Y))) >= mark(cons(X,filter(X,sieve(Y)))) ; active(from(X)) >= mark(cons(X,from(s(X)))) ; active(primes) >= mark(sieve(from(s(s(0))))) ; active(head(cons(X,Y))) >= mark(X) ; active(tail(cons(X,Y))) >= mark(Y) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; active(filter(s(s(X)),cons(Y,Z))) >= mark(if(divides(s(s(X)),Y), filter(s(s(X)),Z), cons(Y,filter(X,sieve(Y))))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; head(mark(X)) >= head(X) ; head(active(X)) >= head(X) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; 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) ; divides(mark(X1),X2) >= divides(X1,X2) ; divides(active(X1),X2) >= divides(X1,X2) ; divides(X1,mark(X2)) >= divides(X1,X2) ; divides(X1,active(X2)) >= divides(X1,X2) ; filter(mark(X1),X2) >= filter(X1,X2) ; filter(active(X1),X2) >= filter(X1,X2) ; filter(X1,mark(X2)) >= filter(X1,X2) ; filter(X1,active(X2)) >= filter(X1,X2) ; Marked_mark(sieve(X)) >= Marked_mark(X) ; Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) ; Marked_mark(from(X)) >= Marked_mark(X) ; Marked_mark(from(X)) >= Marked_active(from(mark(X))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(primes) >= Marked_active(primes) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(head(X)) >= Marked_mark(X) ; Marked_mark(head(X)) >= Marked_active(head(mark(X))) ; Marked_mark(tail(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) ; Marked_mark(if(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(if(X1,X2,X3)) >= Marked_active(if(mark(X1),X2,X3)) ; Marked_mark(divides(X1,X2)) >= Marked_mark(X1) ; Marked_mark(divides(X1,X2)) >= Marked_mark(X2) ; Marked_mark(divides(X1,X2)) >= Marked_active(divides(mark(X1),mark(X2))) ; Marked_mark(filter(X1,X2)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2)) >= Marked_mark(X2) ; Marked_mark(filter(X1,X2)) >= Marked_active(filter(mark(X1),mark(X2))) ; Marked_active(sieve(cons(X,Y))) >= Marked_mark(cons(X,filter(X,sieve(Y)))) ; Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) ; Marked_active(primes) >= Marked_mark(sieve(from(s(s(0))))) ; Marked_active(head(cons(X,Y))) >= Marked_mark(X) ; Marked_active(tail(cons(X,Y))) >= Marked_mark(Y) ; Marked_active(if(true,X,Y)) >= Marked_mark(X) ; Marked_active(if(false,X,Y)) >= Marked_mark(Y) ; Marked_active(filter(s(s(X)),cons(Y,Z))) >= Marked_mark(if(divides(s(s(X)),Y), filter(s(s(X)),Z), cons(Y, filter(X,sieve(Y))))) ; } + Disjunctions:{ { Marked_mark(sieve(X)) > Marked_mark(X) ; } { Marked_mark(sieve(X)) > Marked_active(sieve(mark(X))) ; } { Marked_mark(from(X)) > Marked_mark(X) ; } { Marked_mark(from(X)) > Marked_active(from(mark(X))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(primes) > Marked_active(primes) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(head(X)) > Marked_mark(X) ; } { Marked_mark(head(X)) > Marked_active(head(mark(X))) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_active(tail(mark(X))) ; } { Marked_mark(if(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(if(X1,X2,X3)) > Marked_active(if(mark(X1),X2,X3)) ; } { Marked_mark(divides(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(divides(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(divides(X1,X2)) > Marked_active(divides(mark(X1),mark(X2))) ; } { Marked_mark(filter(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(filter(X1,X2)) > Marked_active(filter(mark(X1),mark(X2))) ; } { Marked_active(sieve(cons(X,Y))) > Marked_mark(cons(X,filter(X,sieve(Y)))) ; } { Marked_active(from(X)) > Marked_mark(cons(X,from(s(X)))) ; } { Marked_active(primes) > Marked_mark(sieve(from(s(s(0))))) ; } { Marked_active(head(cons(X,Y))) > Marked_mark(X) ; } { Marked_active(tail(cons(X,Y))) > Marked_mark(Y) ; } { Marked_active(if(true,X,Y)) > Marked_mark(X) ; } { Marked_active(if(false,X,Y)) > Marked_mark(Y) ; } { Marked_active(filter(s(s(X)),cons(Y,Z))) > Marked_mark(if(divides(s(s(X)),Y), filter(s(s(X)),Z), cons(Y, filter(X,sieve(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(sieve(X)) >= active(sieve(mark(X))) constraint: mark(from(X)) >= active(from(mark(X))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(0) >= active(0) constraint: mark(primes) >= active(primes) constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(head(X)) >= active(head(mark(X))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) constraint: mark(true) >= active(true) constraint: mark(false) >= active(false) constraint: mark(divides(X1,X2)) >= active(divides(mark(X1),mark(X2))) constraint: mark(filter(X1,X2)) >= active(filter(mark(X1),mark(X2))) constraint: sieve(mark(X)) >= sieve(X) constraint: sieve(active(X)) >= sieve(X) constraint: from(mark(X)) >= from(X) constraint: from(active(X)) >= from(X) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: active(sieve(cons(X,Y))) >= mark(cons(X,filter(X,sieve(Y)))) constraint: active(from(X)) >= mark(cons(X,from(s(X)))) constraint: active(primes) >= mark(sieve(from(s(s(0))))) constraint: active(head(cons(X,Y))) >= mark(X) constraint: active(tail(cons(X,Y))) >= mark(Y) constraint: active(if(true,X,Y)) >= mark(X) constraint: active(if(false,X,Y)) >= mark(Y) constraint: active(filter(s(s(X)),cons(Y,Z))) >= mark(if(divides(s(s(X)),Y), filter(s(s(X)),Z), cons(Y, filter(X,sieve(Y))))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: head(mark(X)) >= head(X) constraint: head(active(X)) >= head(X) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) 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: divides(mark(X1),X2) >= divides(X1,X2) constraint: divides(active(X1),X2) >= divides(X1,X2) constraint: divides(X1,mark(X2)) >= divides(X1,X2) constraint: divides(X1,active(X2)) >= divides(X1,X2) constraint: filter(mark(X1),X2) >= filter(X1,X2) constraint: filter(active(X1),X2) >= filter(X1,X2) constraint: filter(X1,mark(X2)) >= filter(X1,X2) constraint: filter(X1,active(X2)) >= filter(X1,X2) constraint: Marked_mark(sieve(X)) >= Marked_mark(X) constraint: Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) constraint: Marked_mark(from(X)) >= Marked_mark(X) constraint: Marked_mark(from(X)) >= Marked_active(from(mark(X))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(primes) >= Marked_active(primes) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(head(X)) >= Marked_mark(X) constraint: Marked_mark(head(X)) >= Marked_active(head(mark(X))) constraint: Marked_mark(tail(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) 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_mark(divides(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(divides(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(divides(X1,X2)) >= Marked_active(divides(mark(X1), mark(X2))) constraint: Marked_mark(filter(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(filter(X1,X2)) >= Marked_active(filter(mark(X1), mark(X2))) constraint: Marked_active(sieve(cons(X,Y))) >= Marked_mark(cons(X, filter(X,sieve(Y)))) constraint: Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) constraint: Marked_active(primes) >= Marked_mark(sieve(from(s(s(0))))) constraint: Marked_active(head(cons(X,Y))) >= Marked_mark(X) constraint: Marked_active(tail(cons(X,Y))) >= Marked_mark(Y) constraint: Marked_active(if(true,X,Y)) >= Marked_mark(X) constraint: Marked_active(if(false,X,Y)) >= Marked_mark(Y) constraint: Marked_active(filter(s(s(X)),cons(Y,Z))) >= Marked_mark(if( divides( s( s(X)), Y), filter( s( s(X)), Z), cons( Y, filter( X, sieve(Y))))) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(sieve(X)) >= active(sieve(mark(X))) ; mark(from(X)) >= active(from(mark(X))) ; mark(s(X)) >= active(s(mark(X))) ; mark(0) >= active(0) ; mark(primes) >= active(primes) ; mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(head(X)) >= active(head(mark(X))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(if(X1,X2,X3)) >= active(if(mark(X1),X2,X3)) ; mark(true) >= active(true) ; mark(false) >= active(false) ; mark(divides(X1,X2)) >= active(divides(mark(X1),mark(X2))) ; mark(filter(X1,X2)) >= active(filter(mark(X1),mark(X2))) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; from(mark(X)) >= from(X) ; from(active(X)) >= from(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; active(sieve(cons(X,Y))) >= mark(cons(X,filter(X,sieve(Y)))) ; active(from(X)) >= mark(cons(X,from(s(X)))) ; active(primes) >= mark(sieve(from(s(s(0))))) ; active(head(cons(X,Y))) >= mark(X) ; active(tail(cons(X,Y))) >= mark(Y) ; active(if(true,X,Y)) >= mark(X) ; active(if(false,X,Y)) >= mark(Y) ; active(filter(s(s(X)),cons(Y,Z))) >= mark(if(divides(s(s(X)),Y), filter(s(s(X)),Z), cons(Y,filter(X,sieve(Y))))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; head(mark(X)) >= head(X) ; head(active(X)) >= head(X) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; 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) ; divides(mark(X1),X2) >= divides(X1,X2) ; divides(active(X1),X2) >= divides(X1,X2) ; divides(X1,mark(X2)) >= divides(X1,X2) ; divides(X1,active(X2)) >= divides(X1,X2) ; filter(mark(X1),X2) >= filter(X1,X2) ; filter(active(X1),X2) >= filter(X1,X2) ; filter(X1,mark(X2)) >= filter(X1,X2) ; filter(X1,active(X2)) >= filter(X1,X2) ; Marked_sieve(mark(X)) >= Marked_sieve(X) ; Marked_sieve(active(X)) >= Marked_sieve(X) ; } + Disjunctions:{ { Marked_sieve(mark(X)) > Marked_sieve(X) ; } { Marked_sieve(active(X)) > Marked_sieve(X) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat timeout reached === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 82.738406 seconds (real time) Cime Exit Status: 0