- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] .(1,x) -> x [2] .(x,1) -> x [3] .(i(x),x) -> 1 [4] .(x,i(x)) -> 1 [5] i(1) -> 1 [6] i(i(x)) -> x [7] .(i(y),.(y,z)) -> z [8] .(y,.(i(y),z)) -> z [9] .(.(x,y),z) -> .(x,.(y,z)) [10] i(.(x,y)) -> .(i(y),i(x)) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 2 components: { --> --> --> --> } { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_i -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_. -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] .(1,x) -> x [2] .(x,1) -> x [3] .(i(x),x) -> 1 [4] .(x,i(x)) -> 1 [5] i(1) -> 1 [6] i(i(x)) -> x [7] .(i(y),.(y,z)) -> z [8] .(y,.(i(y),z)) -> z [9] .(.(x,y),z) -> .(x,.(y,z)) [10] i(.(x,y)) -> .(i(y),i(x)) , CRITERION: MDP [ { 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 0.007337 seconds (real time) Cime Exit Status: 0