- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(filter(cons(X,Y),0,M)) -> mark(cons(0,filter(Y,M,M))) [2] active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M))) [3] active(sieve(cons(0,Y))) -> mark(cons(0,sieve(Y))) [4] active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N)))) [5] active(nats(N)) -> mark(cons(N,nats(s(N)))) [6] active(zprimes) -> mark(sieve(nats(s(s(0))))) [7] mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3))) [8] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [9] mark(0) -> active(0) [10] mark(s(X)) -> active(s(mark(X))) [11] mark(sieve(X)) -> active(sieve(mark(X))) [12] mark(nats(X)) -> active(nats(mark(X))) [13] mark(zprimes) -> active(zprimes) [14] filter(mark(X1),X2,X3) -> filter(X1,X2,X3) [15] filter(X1,mark(X2),X3) -> filter(X1,X2,X3) [16] filter(X1,X2,mark(X3)) -> filter(X1,X2,X3) [17] filter(active(X1),X2,X3) -> filter(X1,X2,X3) [18] filter(X1,active(X2),X3) -> filter(X1,X2,X3) [19] filter(X1,X2,active(X3)) -> filter(X1,X2,X3) [20] cons(mark(X1),X2) -> cons(X1,X2) [21] cons(X1,mark(X2)) -> cons(X1,X2) [22] cons(active(X1),X2) -> cons(X1,X2) [23] cons(X1,active(X2)) -> cons(X1,X2) [24] s(mark(X)) -> s(X) [25] s(active(X)) -> s(X) [26] sieve(mark(X)) -> sieve(X) [27] sieve(active(X)) -> sieve(X) [28] nats(mark(X)) -> nats(X) [29] nats(active(X)) -> nats(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 6 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) ; mark(s(X)) >= active(s(mark(X))) ; mark(sieve(X)) >= active(sieve(mark(X))) ; mark(nats(X)) >= active(nats(mark(X))) ; mark(zprimes) >= active(zprimes) ; 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) ; filter(mark(X1),X2,X3) >= filter(X1,X2,X3) ; filter(active(X1),X2,X3) >= filter(X1,X2,X3) ; filter(X1,mark(X2),X3) >= filter(X1,X2,X3) ; filter(X1,active(X2),X3) >= filter(X1,X2,X3) ; filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) ; filter(X1,X2,active(X3)) >= filter(X1,X2,X3) ; active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) ; active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) ; active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) ; active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) ; active(nats(N)) >= mark(cons(N,nats(s(N)))) ; active(zprimes) >= mark(sieve(nats(s(s(0))))) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; nats(mark(X)) >= nats(X) ; nats(active(X)) >= nats(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) ; Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(sieve(X)) >= Marked_mark(X) ; Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) ; Marked_mark(nats(X)) >= Marked_mark(X) ; Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) ; Marked_mark(zprimes) >= Marked_active(zprimes) ; Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons(0,filter(Y,M,M))) ; Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons(X,filter(Y,N,M))) ; Marked_active(sieve(cons(0,Y))) >= Marked_mark(cons(0,sieve(Y))) ; Marked_active(sieve(cons(s(N),Y))) >= Marked_mark(cons(s(N), sieve(filter(Y,N,N)))) ; Marked_active(nats(N)) >= Marked_mark(cons(N,nats(s(N)))) ; Marked_active(zprimes) >= Marked_mark(sieve(nats(s(s(0))))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X2) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X3) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(sieve(X)) > Marked_mark(X) ; } { Marked_mark(sieve(X)) > Marked_active(sieve(mark(X))) ; } { Marked_mark(nats(X)) > Marked_mark(X) ; } { Marked_mark(nats(X)) > Marked_active(nats(mark(X))) ; } { Marked_mark(zprimes) > Marked_active(zprimes) ; } { Marked_active(filter(cons(X,Y),0,M)) > Marked_mark(cons(0,filter(Y,M,M))) ; } { Marked_active(filter(cons(X,Y),s(N),M)) > Marked_mark(cons(X,filter(Y,N,M))) ; } { Marked_active(sieve(cons(0,Y))) > Marked_mark(cons(0,sieve(Y))) ; } { Marked_active(sieve(cons(s(N),Y))) > Marked_mark(cons(s(N), sieve(filter(Y,N,N)))) ; } { Marked_active(nats(N)) > Marked_mark(cons(N,nats(s(N)))) ; } { Marked_active(zprimes) > Marked_mark(sieve(nats(s(s(0))))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(sieve(X)) >= active(sieve(mark(X))) constraint: mark(nats(X)) >= active(nats(mark(X))) constraint: mark(zprimes) >= active(zprimes) 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: filter(mark(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(active(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(X1,mark(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,active(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) constraint: filter(X1,X2,active(X3)) >= filter(X1,X2,X3) constraint: active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) constraint: active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) constraint: active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) constraint: active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) constraint: active(nats(N)) >= mark(cons(N,nats(s(N)))) constraint: active(zprimes) >= mark(sieve(nats(s(s(0))))) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: sieve(mark(X)) >= sieve(X) constraint: sieve(active(X)) >= sieve(X) constraint: nats(mark(X)) >= nats(X) constraint: nats(active(X)) >= nats(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1), mark(X2), mark(X3))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(sieve(X)) >= Marked_mark(X) constraint: Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) constraint: Marked_mark(nats(X)) >= Marked_mark(X) constraint: Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) constraint: Marked_mark(zprimes) >= Marked_active(zprimes) constraint: Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons( 0, filter(Y,M,M))) constraint: Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons( X, filter( Y, N, M))) constraint: Marked_active(sieve(cons(0,Y))) >= Marked_mark(cons(0,sieve(Y))) constraint: Marked_active(sieve(cons(s(N),Y))) >= Marked_mark(cons(s(N), sieve( filter( Y,N, N)))) constraint: Marked_active(nats(N)) >= Marked_mark(cons(N,nats(s(N)))) constraint: Marked_active(zprimes) >= Marked_mark(sieve(nats(s(s(0))))) APPLY CRITERIA (Subterm criterion) ST: Marked_filter -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_cons -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_s -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_sieve -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_nats -> 1 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) ; mark(s(X)) >= active(s(mark(X))) ; mark(sieve(X)) >= active(sieve(mark(X))) ; mark(nats(X)) >= active(nats(mark(X))) ; mark(zprimes) >= active(zprimes) ; 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) ; filter(mark(X1),X2,X3) >= filter(X1,X2,X3) ; filter(active(X1),X2,X3) >= filter(X1,X2,X3) ; filter(X1,mark(X2),X3) >= filter(X1,X2,X3) ; filter(X1,active(X2),X3) >= filter(X1,X2,X3) ; filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) ; filter(X1,X2,active(X3)) >= filter(X1,X2,X3) ; active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) ; active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) ; active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) ; active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) ; active(nats(N)) >= mark(cons(N,nats(s(N)))) ; active(zprimes) >= mark(sieve(nats(s(s(0))))) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; nats(mark(X)) >= nats(X) ; nats(active(X)) >= nats(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) ; Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(sieve(X)) >= Marked_mark(X) ; Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) ; Marked_mark(nats(X)) >= Marked_mark(X) ; Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) ; Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons(0,filter(Y,M,M))) ; Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons(X,filter(Y,N,M))) ; Marked_active(sieve(cons(0,Y))) >= Marked_mark(cons(0,sieve(Y))) ; Marked_active(sieve(cons(s(N),Y))) >= Marked_mark(cons(s(N), sieve(filter(Y,N,N)))) ; Marked_active(nats(N)) >= Marked_mark(cons(N,nats(s(N)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X2) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X3) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(sieve(X)) > Marked_mark(X) ; } { Marked_mark(sieve(X)) > Marked_active(sieve(mark(X))) ; } { Marked_mark(nats(X)) > Marked_mark(X) ; } { Marked_mark(nats(X)) > Marked_active(nats(mark(X))) ; } { Marked_active(filter(cons(X,Y),0,M)) > Marked_mark(cons(0,filter(Y,M,M))) ; } { Marked_active(filter(cons(X,Y),s(N),M)) > Marked_mark(cons(X,filter(Y,N,M))) ; } { Marked_active(sieve(cons(0,Y))) > Marked_mark(cons(0,sieve(Y))) ; } { Marked_active(sieve(cons(s(N),Y))) > Marked_mark(cons(s(N), sieve(filter(Y,N,N)))) ; } { Marked_active(nats(N)) > Marked_mark(cons(N,nats(s(N)))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(sieve(X)) >= active(sieve(mark(X))) constraint: mark(nats(X)) >= active(nats(mark(X))) constraint: mark(zprimes) >= active(zprimes) 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: filter(mark(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(active(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(X1,mark(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,active(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) constraint: filter(X1,X2,active(X3)) >= filter(X1,X2,X3) constraint: active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) constraint: active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) constraint: active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) constraint: active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) constraint: active(nats(N)) >= mark(cons(N,nats(s(N)))) constraint: active(zprimes) >= mark(sieve(nats(s(s(0))))) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: sieve(mark(X)) >= sieve(X) constraint: sieve(active(X)) >= sieve(X) constraint: nats(mark(X)) >= nats(X) constraint: nats(active(X)) >= nats(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1), mark(X2), mark(X3))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(sieve(X)) >= Marked_mark(X) constraint: Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) constraint: Marked_mark(nats(X)) >= Marked_mark(X) constraint: Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) constraint: Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons( 0, filter(Y,M,M))) constraint: Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons( X, filter( Y, N, M))) constraint: Marked_active(sieve(cons(0,Y))) >= Marked_mark(cons(0,sieve(Y))) constraint: Marked_active(sieve(cons(s(N),Y))) >= Marked_mark(cons(s(N), sieve( filter( Y,N, N)))) constraint: Marked_active(nats(N)) >= Marked_mark(cons(N,nats(s(N)))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) ; mark(s(X)) >= active(s(mark(X))) ; mark(sieve(X)) >= active(sieve(mark(X))) ; mark(nats(X)) >= active(nats(mark(X))) ; mark(zprimes) >= active(zprimes) ; 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) ; filter(mark(X1),X2,X3) >= filter(X1,X2,X3) ; filter(active(X1),X2,X3) >= filter(X1,X2,X3) ; filter(X1,mark(X2),X3) >= filter(X1,X2,X3) ; filter(X1,active(X2),X3) >= filter(X1,X2,X3) ; filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) ; filter(X1,X2,active(X3)) >= filter(X1,X2,X3) ; active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) ; active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) ; active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) ; active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) ; active(nats(N)) >= mark(cons(N,nats(s(N)))) ; active(zprimes) >= mark(sieve(nats(s(s(0))))) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; nats(mark(X)) >= nats(X) ; nats(active(X)) >= nats(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) ; Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(sieve(X)) >= Marked_mark(X) ; Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) ; Marked_mark(nats(X)) >= Marked_mark(X) ; Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) ; Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons(0,filter(Y,M,M))) ; Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons(X,filter(Y,N,M))) ; Marked_active(sieve(cons(0,Y))) >= Marked_mark(cons(0,sieve(Y))) ; Marked_active(sieve(cons(s(N),Y))) >= Marked_mark(cons(s(N), sieve(filter(Y,N,N)))) ; Marked_active(nats(N)) >= Marked_mark(cons(N,nats(s(N)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X2) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X3) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(sieve(X)) > Marked_mark(X) ; } { Marked_mark(sieve(X)) > Marked_active(sieve(mark(X))) ; } { Marked_mark(nats(X)) > Marked_mark(X) ; } { Marked_mark(nats(X)) > Marked_active(nats(mark(X))) ; } { Marked_active(filter(cons(X,Y),0,M)) > Marked_mark(cons(0,filter(Y,M,M))) ; } { Marked_active(filter(cons(X,Y),s(N),M)) > Marked_mark(cons(X,filter(Y,N,M))) ; } { Marked_active(sieve(cons(0,Y))) > Marked_mark(cons(0,sieve(Y))) ; } { Marked_active(sieve(cons(s(N),Y))) > Marked_mark(cons(s(N), sieve(filter(Y,N,N)))) ; } { Marked_active(nats(N)) > Marked_mark(cons(N,nats(s(N)))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(sieve(X)) >= active(sieve(mark(X))) constraint: mark(nats(X)) >= active(nats(mark(X))) constraint: mark(zprimes) >= active(zprimes) 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: filter(mark(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(active(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(X1,mark(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,active(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) constraint: filter(X1,X2,active(X3)) >= filter(X1,X2,X3) constraint: active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) constraint: active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) constraint: active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) constraint: active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) constraint: active(nats(N)) >= mark(cons(N,nats(s(N)))) constraint: active(zprimes) >= mark(sieve(nats(s(s(0))))) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: sieve(mark(X)) >= sieve(X) constraint: sieve(active(X)) >= sieve(X) constraint: nats(mark(X)) >= nats(X) constraint: nats(active(X)) >= nats(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1), mark(X2), mark(X3))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(sieve(X)) >= Marked_mark(X) constraint: Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) constraint: Marked_mark(nats(X)) >= Marked_mark(X) constraint: Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) constraint: Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons( 0, filter(Y,M,M))) constraint: Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons( X, filter( Y, N, M))) constraint: Marked_active(sieve(cons(0,Y))) >= Marked_mark(cons(0,sieve(Y))) constraint: Marked_active(sieve(cons(s(N),Y))) >= Marked_mark(cons(s(N), sieve( filter( Y,N, N)))) constraint: Marked_active(nats(N)) >= Marked_mark(cons(N,nats(s(N)))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) ; mark(s(X)) >= active(s(mark(X))) ; mark(sieve(X)) >= active(sieve(mark(X))) ; mark(nats(X)) >= active(nats(mark(X))) ; mark(zprimes) >= active(zprimes) ; 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) ; filter(mark(X1),X2,X3) >= filter(X1,X2,X3) ; filter(active(X1),X2,X3) >= filter(X1,X2,X3) ; filter(X1,mark(X2),X3) >= filter(X1,X2,X3) ; filter(X1,active(X2),X3) >= filter(X1,X2,X3) ; filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) ; filter(X1,X2,active(X3)) >= filter(X1,X2,X3) ; active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) ; active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) ; active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) ; active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) ; active(nats(N)) >= mark(cons(N,nats(s(N)))) ; active(zprimes) >= mark(sieve(nats(s(s(0))))) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; nats(mark(X)) >= nats(X) ; nats(active(X)) >= nats(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) ; Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(sieve(X)) >= Marked_mark(X) ; Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) ; Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) ; Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons(0,filter(Y,M,M))) ; Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons(X,filter(Y,N,M))) ; Marked_active(sieve(cons(0,Y))) >= Marked_mark(cons(0,sieve(Y))) ; Marked_active(sieve(cons(s(N),Y))) >= Marked_mark(cons(s(N), sieve(filter(Y,N,N)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X2) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X3) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(sieve(X)) > Marked_mark(X) ; } { Marked_mark(sieve(X)) > Marked_active(sieve(mark(X))) ; } { Marked_mark(nats(X)) > Marked_active(nats(mark(X))) ; } { Marked_active(filter(cons(X,Y),0,M)) > Marked_mark(cons(0,filter(Y,M,M))) ; } { Marked_active(filter(cons(X,Y),s(N),M)) > Marked_mark(cons(X,filter(Y,N,M))) ; } { Marked_active(sieve(cons(0,Y))) > Marked_mark(cons(0,sieve(Y))) ; } { Marked_active(sieve(cons(s(N),Y))) > Marked_mark(cons(s(N), sieve(filter(Y,N,N)))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(sieve(X)) >= active(sieve(mark(X))) constraint: mark(nats(X)) >= active(nats(mark(X))) constraint: mark(zprimes) >= active(zprimes) 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: filter(mark(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(active(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(X1,mark(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,active(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) constraint: filter(X1,X2,active(X3)) >= filter(X1,X2,X3) constraint: active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) constraint: active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) constraint: active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) constraint: active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) constraint: active(nats(N)) >= mark(cons(N,nats(s(N)))) constraint: active(zprimes) >= mark(sieve(nats(s(s(0))))) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: sieve(mark(X)) >= sieve(X) constraint: sieve(active(X)) >= sieve(X) constraint: nats(mark(X)) >= nats(X) constraint: nats(active(X)) >= nats(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1), mark(X2), mark(X3))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(sieve(X)) >= Marked_mark(X) constraint: Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) constraint: Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) constraint: Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons( 0, filter(Y,M,M))) constraint: Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons( X, filter( Y, N, M))) constraint: Marked_active(sieve(cons(0,Y))) >= Marked_mark(cons(0,sieve(Y))) constraint: Marked_active(sieve(cons(s(N),Y))) >= Marked_mark(cons(s(N), sieve( filter( Y,N, N)))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) ; mark(s(X)) >= active(s(mark(X))) ; mark(sieve(X)) >= active(sieve(mark(X))) ; mark(nats(X)) >= active(nats(mark(X))) ; mark(zprimes) >= active(zprimes) ; 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) ; filter(mark(X1),X2,X3) >= filter(X1,X2,X3) ; filter(active(X1),X2,X3) >= filter(X1,X2,X3) ; filter(X1,mark(X2),X3) >= filter(X1,X2,X3) ; filter(X1,active(X2),X3) >= filter(X1,X2,X3) ; filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) ; filter(X1,X2,active(X3)) >= filter(X1,X2,X3) ; active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) ; active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) ; active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) ; active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) ; active(nats(N)) >= mark(cons(N,nats(s(N)))) ; active(zprimes) >= mark(sieve(nats(s(s(0))))) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; nats(mark(X)) >= nats(X) ; nats(active(X)) >= nats(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) ; Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) ; Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) ; Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons(0,filter(Y,M,M))) ; Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons(X,filter(Y,N,M))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X2) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X3) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(sieve(X)) > Marked_active(sieve(mark(X))) ; } { Marked_mark(nats(X)) > Marked_active(nats(mark(X))) ; } { Marked_active(filter(cons(X,Y),0,M)) > Marked_mark(cons(0,filter(Y,M,M))) ; } { Marked_active(filter(cons(X,Y),s(N),M)) > Marked_mark(cons(X,filter(Y,N,M))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(sieve(X)) >= active(sieve(mark(X))) constraint: mark(nats(X)) >= active(nats(mark(X))) constraint: mark(zprimes) >= active(zprimes) 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: filter(mark(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(active(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(X1,mark(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,active(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) constraint: filter(X1,X2,active(X3)) >= filter(X1,X2,X3) constraint: active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) constraint: active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) constraint: active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) constraint: active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) constraint: active(nats(N)) >= mark(cons(N,nats(s(N)))) constraint: active(zprimes) >= mark(sieve(nats(s(s(0))))) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: sieve(mark(X)) >= sieve(X) constraint: sieve(active(X)) >= sieve(X) constraint: nats(mark(X)) >= nats(X) constraint: nats(active(X)) >= nats(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1), mark(X2), mark(X3))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(sieve(X)) >= Marked_active(sieve(mark(X))) constraint: Marked_mark(nats(X)) >= Marked_active(nats(mark(X))) constraint: Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons( 0, filter(Y,M,M))) constraint: Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons( X, filter( Y, N, M))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) ; mark(s(X)) >= active(s(mark(X))) ; mark(sieve(X)) >= active(sieve(mark(X))) ; mark(nats(X)) >= active(nats(mark(X))) ; mark(zprimes) >= active(zprimes) ; 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) ; filter(mark(X1),X2,X3) >= filter(X1,X2,X3) ; filter(active(X1),X2,X3) >= filter(X1,X2,X3) ; filter(X1,mark(X2),X3) >= filter(X1,X2,X3) ; filter(X1,active(X2),X3) >= filter(X1,X2,X3) ; filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) ; filter(X1,X2,active(X3)) >= filter(X1,X2,X3) ; active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) ; active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) ; active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) ; active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) ; active(nats(N)) >= mark(cons(N,nats(s(N)))) ; active(zprimes) >= mark(sieve(nats(s(s(0))))) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; nats(mark(X)) >= nats(X) ; nats(active(X)) >= nats(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) ; Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons(0,filter(Y,M,M))) ; Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons(X,filter(Y,N,M))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X2) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X3) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_active(filter(cons(X,Y),0,M)) > Marked_mark(cons(0,filter(Y,M,M))) ; } { Marked_active(filter(cons(X,Y),s(N),M)) > Marked_mark(cons(X,filter(Y,N,M))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(sieve(X)) >= active(sieve(mark(X))) constraint: mark(nats(X)) >= active(nats(mark(X))) constraint: mark(zprimes) >= active(zprimes) 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: filter(mark(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(active(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(X1,mark(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,active(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) constraint: filter(X1,X2,active(X3)) >= filter(X1,X2,X3) constraint: active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) constraint: active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) constraint: active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) constraint: active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) constraint: active(nats(N)) >= mark(cons(N,nats(s(N)))) constraint: active(zprimes) >= mark(sieve(nats(s(s(0))))) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: sieve(mark(X)) >= sieve(X) constraint: sieve(active(X)) >= sieve(X) constraint: nats(mark(X)) >= nats(X) constraint: nats(active(X)) >= nats(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1), mark(X2), mark(X3))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_active(filter(cons(X,Y),0,M)) >= Marked_mark(cons( 0, filter(Y,M,M))) constraint: Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons( X, filter( Y, N, M))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) ; mark(s(X)) >= active(s(mark(X))) ; mark(sieve(X)) >= active(sieve(mark(X))) ; mark(nats(X)) >= active(nats(mark(X))) ; mark(zprimes) >= active(zprimes) ; 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) ; filter(mark(X1),X2,X3) >= filter(X1,X2,X3) ; filter(active(X1),X2,X3) >= filter(X1,X2,X3) ; filter(X1,mark(X2),X3) >= filter(X1,X2,X3) ; filter(X1,active(X2),X3) >= filter(X1,X2,X3) ; filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) ; filter(X1,X2,active(X3)) >= filter(X1,X2,X3) ; active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) ; active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) ; active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) ; active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) ; active(nats(N)) >= mark(cons(N,nats(s(N)))) ; active(zprimes) >= mark(sieve(nats(s(s(0))))) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; sieve(mark(X)) >= sieve(X) ; sieve(active(X)) >= sieve(X) ; nats(mark(X)) >= nats(X) ; nats(active(X)) >= nats(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) ; Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) ; Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons(X,filter(Y,N,M))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X2) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_mark(X3) ; } { Marked_mark(filter(X1,X2,X3)) > Marked_active(filter(mark(X1),mark(X2), mark(X3))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_active(filter(cons(X,Y),s(N),M)) > Marked_mark(cons(X,filter(Y,N,M))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(filter(X1,X2,X3)) >= active(filter(mark(X1),mark(X2),mark(X3))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(sieve(X)) >= active(sieve(mark(X))) constraint: mark(nats(X)) >= active(nats(mark(X))) constraint: mark(zprimes) >= active(zprimes) 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: filter(mark(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(active(X1),X2,X3) >= filter(X1,X2,X3) constraint: filter(X1,mark(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,active(X2),X3) >= filter(X1,X2,X3) constraint: filter(X1,X2,mark(X3)) >= filter(X1,X2,X3) constraint: filter(X1,X2,active(X3)) >= filter(X1,X2,X3) constraint: active(filter(cons(X,Y),0,M)) >= mark(cons(0,filter(Y,M,M))) constraint: active(filter(cons(X,Y),s(N),M)) >= mark(cons(X,filter(Y,N,M))) constraint: active(sieve(cons(0,Y))) >= mark(cons(0,sieve(Y))) constraint: active(sieve(cons(s(N),Y))) >= mark(cons(s(N),sieve(filter(Y,N,N)))) constraint: active(nats(N)) >= mark(cons(N,nats(s(N)))) constraint: active(zprimes) >= mark(sieve(nats(s(s(0))))) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: sieve(mark(X)) >= sieve(X) constraint: sieve(active(X)) >= sieve(X) constraint: nats(mark(X)) >= nats(X) constraint: nats(active(X)) >= nats(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X2) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_mark(X3) constraint: Marked_mark(filter(X1,X2,X3)) >= Marked_active(filter(mark(X1), mark(X2), mark(X3))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_active(filter(cons(X,Y),s(N),M)) >= Marked_mark(cons( X, filter( Y, N, M))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_mark -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_filter -> 2 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_filter -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_cons -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] active(filter(cons(X,Y),0,M)) -> mark(cons(0,filter(Y,M,M))) [2] active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M))) [3] active(sieve(cons(0,Y))) -> mark(cons(0,sieve(Y))) [4] active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N)))) [5] active(nats(N)) -> mark(cons(N,nats(s(N)))) [6] active(zprimes) -> mark(sieve(nats(s(s(0))))) [7] mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3))) [8] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [9] mark(0) -> active(0) [10] mark(s(X)) -> active(s(mark(X))) [11] mark(sieve(X)) -> active(sieve(mark(X))) [12] mark(nats(X)) -> active(nats(mark(X))) [13] mark(zprimes) -> active(zprimes) [14] filter(mark(X1),X2,X3) -> filter(X1,X2,X3) [15] filter(X1,mark(X2),X3) -> filter(X1,X2,X3) [16] filter(X1,X2,mark(X3)) -> filter(X1,X2,X3) [17] filter(active(X1),X2,X3) -> filter(X1,X2,X3) [18] filter(X1,active(X2),X3) -> filter(X1,X2,X3) [19] filter(X1,X2,active(X3)) -> filter(X1,X2,X3) [20] cons(mark(X1),X2) -> cons(X1,X2) [21] cons(X1,mark(X2)) -> cons(X1,X2) [22] cons(active(X1),X2) -> cons(X1,X2) [23] cons(X1,active(X2)) -> cons(X1,X2) [24] s(mark(X)) -> s(X) [25] s(active(X)) -> s(X) [26] sieve(mark(X)) -> sieve(X) [27] sieve(active(X)) -> sieve(X) [28] nats(mark(X)) -> nats(X) [29] nats(active(X)) -> nats(X) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ zprimes ] () = 1; [ active ] (X0) = 1*X0; [ 0 ] () = 0; [ sieve ] (X0) = 2*X0; [ Marked_mark ] (X0) = 2*X0; [ cons ] (X0,X1) = 2*X0; [ s ] (X0) = 2*X0; [ filter ] (X0,X1,X2) = 1*X2 + 1*X1 + 2*X0; [ nats ] (X0) = 2*X0; [ Marked_active ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ zprimes ] () = 0; [ active ] (X0) = 0; [ 0 ] () = 0; [ sieve ] (X0) = 1; [ Marked_mark ] (X0) = 2; [ cons ] (X0,X1) = 0; [ s ] (X0) = 0; [ filter ] (X0,X1,X2) = 1; [ nats ] (X0) = 1; [ Marked_active ] (X0) = 2*X0; removing < Marked_mark(s(X)),Marked_active(s(mark(X)))> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ zprimes ] () = 2; [ active ] (X0) = 1*X0; [ 0 ] () = 0; [ sieve ] (X0) = 2*X0; [ Marked_mark ] (X0) = 2*X0; [ cons ] (X0,X1) = 2*X0; [ s ] (X0) = 1*X0; [ filter ] (X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; [ nats ] (X0) = 2*X0 + 1; [ Marked_active ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ zprimes ] () = 1; [ active ] (X0) = 1*X0; [ 0 ] () = 0; [ sieve ] (X0) = 2*X0 + 1; [ Marked_mark ] (X0) = 2*X0; [ cons ] (X0,X1) = 2*X0; [ s ] (X0) = 2*X0; [ filter ] (X0,X1,X2) = 1*X2 + 1*X1 + 2*X0; [ nats ] (X0) = 2*X0; [ Marked_active ] (X0) = 2*X0; removing < Marked_active(sieve(cons(s(N),Y))),Marked_mark(cons(s(N),sieve(filter(Y,N,N))))>< Marked_mark(sieve(X)),Marked_mark(X)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 0; [ zprimes ] () = 0; [ active ] (X0) = 0; [ 0 ] () = 0; [ sieve ] (X0) = 0; [ Marked_mark ] (X0) = 1; [ cons ] (X0,X1) = 0; [ s ] (X0) = 0; [ filter ] (X0,X1,X2) = 1; [ nats ] (X0) = 0; [ Marked_active ] (X0) = 1*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ zprimes ] () = 2; [ active ] (X0) = 1*X0; [ 0 ] () = 2; [ sieve ] (X0) = 1*X0; [ Marked_mark ] (X0) = 2*X0 + 3; [ cons ] (X0,X1) = 1*X0; [ s ] (X0) = 1*X0; [ filter ] (X0,X1,X2) = 1*X2 + 2*X1 + 2*X0; [ nats ] (X0) = 1*X0; [ Marked_active ] (X0) = 2*X0 + 3; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0; [ zprimes ] () = 2; [ active ] (X0) = 1*X0; [ 0 ] () = 0; [ sieve ] (X0) = 1*X0; [ Marked_mark ] (X0) = 2*X0; [ cons ] (X0,X1) = 1*X0 + 2; [ s ] (X0) = 1*X0; [ filter ] (X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; [ nats ] (X0) = 1*X0 + 2; [ Marked_active ] (X0) = 2*X0; removing < Marked_mark(cons(X1,X2)),Marked_mark(X1)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 2.111223 seconds (real time) Cime Exit Status: 0