- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] __(__(X,Y),Z) -> __(X,__(Y,Z)) [2] __(X,nil) -> X [3] __(nil,X) -> X [4] and(tt,X) -> activate(X) [5] isNePal(__(I,__(P,I))) -> tt [6] 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: { __(__(X,Y),Z) >= __(X,__(Y,Z)) ; __(nil,X) >= X ; __(X,nil) >= X ; activate(X) >= X ; and(tt,X) >= activate(X) ; isNePal(__(I,__(P,I))) >= tt ; Marked___(__(X,Y),Z) >= Marked___(X,__(Y,Z)) ; Marked___(__(X,Y),Z) >= Marked___(Y,Z) ; } + Disjunctions:{ { Marked___(__(X,Y),Z) > Marked___(X,__(Y,Z)) ; } { Marked___(__(X,Y),Z) > Marked___(Y,Z) ; } } === 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: __(__(X,Y),Z) >= __(X,__(Y,Z)) constraint: __(nil,X) >= X constraint: __(X,nil) >= X constraint: activate(X) >= X constraint: and(tt,X) >= activate(X) constraint: isNePal(__(I,__(P,I))) >= tt constraint: Marked___(__(X,Y),Z) >= Marked___(X,__(Y,Z)) constraint: Marked___(__(X,Y),Z) >= Marked___(Y,Z) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] __(__(X,Y),Z) -> __(X,__(Y,Z)) [2] __(X,nil) -> X [3] __(nil,X) -> X [4] and(tt,X) -> activate(X) [5] isNePal(__(I,__(P,I))) -> tt [6] activate(X) -> X , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ __ ] (X0,X1) = 3 + 3*X0 + 1*X1 + 0; [ tt ] () = 0; [ activate ] (X0) = 3 + 3*X0 + 0; [ nil ] () = 3 + 0; [ Marked___ ] (X0,X1) = 2*X0 + 0; [ isNePal ] (X0) = 3 + 3*X0 + 0; [ and ] (X0,X1) = 3 + 3*X0 + 3*X1 + 0; ]} ]} ]} Cime worked for 0.021700 seconds (real time) Cime Exit Status: 0