- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] filter(cons(X,Y),0,M) -> cons(0,n__filter(activate(Y),M,M)) [2] filter(cons(X,Y),s(N),M) -> cons(X,n__filter(activate(Y),N,M)) [3] sieve(cons(0,Y)) -> cons(0,n__sieve(activate(Y))) [4] sieve(cons(s(N),Y)) -> cons(s(N),n__sieve(n__filter(activate(Y),N,N))) [5] nats(N) -> cons(N,n__nats(n__s(N))) [6] zprimes -> sieve(nats(s(s(0)))) [7] filter(X1,X2,X3) -> n__filter(X1,X2,X3) [8] sieve(X) -> n__sieve(X) [9] nats(X) -> n__nats(X) [10] s(X) -> n__s(X) [11] activate(n__filter(X1,X2,X3)) -> filter(activate(X1),activate(X2),activate(X3)) [12] activate(n__sieve(X)) -> sieve(activate(X)) [13] activate(n__nats(X)) -> nats(activate(X)) [14] activate(n__s(X)) -> s(activate(X)) [15] activate(X) -> X Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { activate(n__filter(X1,X2,X3)) >= filter(activate(X1),activate(X2), activate(X3)) ; activate(n__sieve(X)) >= sieve(activate(X)) ; activate(n__nats(X)) >= nats(activate(X)) ; activate(n__s(X)) >= s(activate(X)) ; activate(X) >= X ; filter(cons(X,Y),0,M) >= cons(0,n__filter(activate(Y),M,M)) ; filter(cons(X,Y),s(N),M) >= cons(X,n__filter(activate(Y),N,M)) ; filter(X1,X2,X3) >= n__filter(X1,X2,X3) ; s(X) >= n__s(X) ; sieve(cons(0,Y)) >= cons(0,n__sieve(activate(Y))) ; sieve(cons(s(N),Y)) >= cons(s(N),n__sieve(n__filter(activate(Y),N,N))) ; sieve(X) >= n__sieve(X) ; nats(X) >= n__nats(X) ; nats(N) >= cons(N,n__nats(n__s(N))) ; zprimes >= sieve(nats(s(s(0)))) ; Marked_activate(n__filter(X1,X2,X3)) >= Marked_activate(X1) ; Marked_activate(n__filter(X1,X2,X3)) >= Marked_activate(X2) ; Marked_activate(n__filter(X1,X2,X3)) >= Marked_activate(X3) ; Marked_activate(n__filter(X1,X2,X3)) >= Marked_filter(activate(X1), activate(X2),activate(X3)) ; Marked_activate(n__sieve(X)) >= Marked_activate(X) ; Marked_activate(n__sieve(X)) >= Marked_sieve(activate(X)) ; Marked_activate(n__nats(X)) >= Marked_activate(X) ; Marked_activate(n__s(X)) >= Marked_activate(X) ; Marked_sieve(cons(0,Y)) >= Marked_activate(Y) ; Marked_sieve(cons(s(N),Y)) >= Marked_activate(Y) ; Marked_filter(cons(X,Y),0,M) >= Marked_activate(Y) ; Marked_filter(cons(X,Y),s(N),M) >= Marked_activate(Y) ; } + Disjunctions:{ { Marked_activate(n__filter(X1,X2,X3)) > Marked_activate(X1) ; } { Marked_activate(n__filter(X1,X2,X3)) > Marked_activate(X2) ; } { Marked_activate(n__filter(X1,X2,X3)) > Marked_activate(X3) ; } { Marked_activate(n__filter(X1,X2,X3)) > Marked_filter(activate(X1), activate(X2),activate(X3)) ; } { Marked_activate(n__sieve(X)) > Marked_activate(X) ; } { Marked_activate(n__sieve(X)) > Marked_sieve(activate(X)) ; } { Marked_activate(n__nats(X)) > Marked_activate(X) ; } { Marked_activate(n__s(X)) > Marked_activate(X) ; } { Marked_sieve(cons(0,Y)) > Marked_activate(Y) ; } { Marked_sieve(cons(s(N),Y)) > Marked_activate(Y) ; } { Marked_filter(cons(X,Y),0,M) > Marked_activate(Y) ; } { Marked_filter(cons(X,Y),s(N),M) > Marked_activate(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 === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 6.041982 seconds (real time) Cime Exit Status: 0