- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] +(0,0) -> 0 [2] +(0,1) -> 1 [3] +(0,2) -> 2 [4] +(0,3) -> 3 [5] +(0,4) -> 4 [6] +(0,5) -> 5 [7] +(0,6) -> 6 [8] +(0,7) -> 7 [9] +(0,8) -> 8 [10] +(0,9) -> 9 [11] +(1,0) -> 1 [12] +(1,1) -> 2 [13] +(1,2) -> 3 [14] +(1,3) -> 4 [15] +(1,4) -> 5 [16] +(1,5) -> 6 [17] +(1,6) -> 7 [18] +(1,7) -> 8 [19] +(1,8) -> 9 [20] +(1,9) -> c(1,0) [21] +(2,0) -> 2 [22] +(2,1) -> 3 [23] +(2,2) -> 4 [24] +(2,3) -> 5 [25] +(2,4) -> 6 [26] +(2,5) -> 7 [27] +(2,6) -> 8 [28] +(2,7) -> 9 [29] +(2,8) -> c(1,0) [30] +(2,9) -> c(1,1) [31] +(3,0) -> 3 [32] +(3,1) -> 4 [33] +(3,2) -> 5 [34] +(3,3) -> 6 [35] +(3,4) -> 7 [36] +(3,5) -> 8 [37] +(3,6) -> 9 [38] +(3,7) -> c(1,0) [39] +(3,8) -> c(1,1) [40] +(3,9) -> c(1,2) [41] +(4,0) -> 4 [42] +(4,1) -> 5 [43] +(4,2) -> 6 [44] +(4,3) -> 7 [45] +(4,4) -> 8 [46] +(4,5) -> 9 [47] +(4,6) -> c(1,0) [48] +(4,7) -> c(1,1) [49] +(4,8) -> c(1,2) [50] +(4,9) -> c(1,3) [51] +(5,0) -> 5 [52] +(5,1) -> 6 [53] +(5,2) -> 7 [54] +(5,3) -> 8 [55] +(5,4) -> 9 [56] +(5,5) -> c(1,0) [57] +(5,6) -> c(1,1) [58] +(5,7) -> c(1,2) [59] +(5,8) -> c(1,3) [60] +(5,9) -> c(1,4) [61] +(6,0) -> 6 [62] +(6,1) -> 7 [63] +(6,2) -> 8 [64] +(6,3) -> 9 [65] +(6,4) -> c(1,0) [66] +(6,5) -> c(1,1) [67] +(6,6) -> c(1,2) [68] +(6,7) -> c(1,3) [69] +(6,8) -> c(1,4) [70] +(6,9) -> c(1,5) [71] +(7,0) -> 7 [72] +(7,1) -> 8 [73] +(7,2) -> 9 [74] +(7,3) -> c(1,0) [75] +(7,4) -> c(1,1) [76] +(7,5) -> c(1,2) [77] +(7,6) -> c(1,3) [78] +(7,7) -> c(1,4) [79] +(7,8) -> c(1,5) [80] +(7,9) -> c(1,6) [81] +(8,0) -> 8 [82] +(8,1) -> 9 [83] +(8,2) -> c(1,0) [84] +(8,3) -> c(1,1) [85] +(8,4) -> c(1,2) [86] +(8,5) -> c(1,3) [87] +(8,6) -> c(1,4) [88] +(8,7) -> c(1,5) [89] +(8,8) -> c(1,6) [90] +(8,9) -> c(1,7) [91] +(9,0) -> 9 [92] +(9,1) -> c(1,0) [93] +(9,2) -> c(1,1) [94] +(9,3) -> c(1,2) [95] +(9,4) -> c(1,3) [96] +(9,5) -> c(1,4) [97] +(9,6) -> c(1,5) [98] +(9,7) -> c(1,6) [99] +(9,8) -> c(1,7) [100] +(9,9) -> c(1,8) [101] +(x,c(y,z)) -> c(y,+(x,z)) [102] +(c(x,y),z) -> c(x,+(y,z)) [103] c(0,x) -> x [104] c(x,c(y,z)) -> c(+(x,y),z) 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: { +(0,0) >= 0 ; +(0,1) >= 1 ; +(0,2) >= 2 ; +(0,3) >= 3 ; +(0,4) >= 4 ; +(0,5) >= 5 ; +(0,6) >= 6 ; +(0,7) >= 7 ; +(0,8) >= 8 ; +(0,9) >= 9 ; +(1,0) >= 1 ; +(1,1) >= 2 ; +(1,2) >= 3 ; +(1,3) >= 4 ; +(1,4) >= 5 ; +(1,5) >= 6 ; +(1,6) >= 7 ; +(1,7) >= 8 ; +(1,8) >= 9 ; +(1,9) >= c(1,0) ; +(2,0) >= 2 ; +(2,1) >= 3 ; +(2,2) >= 4 ; +(2,3) >= 5 ; +(2,4) >= 6 ; +(2,5) >= 7 ; +(2,6) >= 8 ; +(2,7) >= 9 ; +(2,8) >= c(1,0) ; +(2,9) >= c(1,1) ; +(3,0) >= 3 ; +(3,1) >= 4 ; +(3,2) >= 5 ; +(3,3) >= 6 ; +(3,4) >= 7 ; +(3,5) >= 8 ; +(3,6) >= 9 ; +(3,7) >= c(1,0) ; +(3,8) >= c(1,1) ; +(3,9) >= c(1,2) ; +(4,0) >= 4 ; +(4,1) >= 5 ; +(4,2) >= 6 ; +(4,3) >= 7 ; +(4,4) >= 8 ; +(4,5) >= 9 ; +(4,6) >= c(1,0) ; +(4,7) >= c(1,1) ; +(4,8) >= c(1,2) ; +(4,9) >= c(1,3) ; +(5,0) >= 5 ; +(5,1) >= 6 ; +(5,2) >= 7 ; +(5,3) >= 8 ; +(5,4) >= 9 ; +(5,5) >= c(1,0) ; +(5,6) >= c(1,1) ; +(5,7) >= c(1,2) ; +(5,8) >= c(1,3) ; +(5,9) >= c(1,4) ; +(6,0) >= 6 ; +(6,1) >= 7 ; +(6,2) >= 8 ; +(6,3) >= 9 ; +(6,4) >= c(1,0) ; +(6,5) >= c(1,1) ; +(6,6) >= c(1,2) ; +(6,7) >= c(1,3) ; +(6,8) >= c(1,4) ; +(6,9) >= c(1,5) ; +(7,0) >= 7 ; +(7,1) >= 8 ; +(7,2) >= 9 ; +(7,3) >= c(1,0) ; +(7,4) >= c(1,1) ; +(7,5) >= c(1,2) ; +(7,6) >= c(1,3) ; +(7,7) >= c(1,4) ; +(7,8) >= c(1,5) ; +(7,9) >= c(1,6) ; +(8,0) >= 8 ; +(8,1) >= 9 ; +(8,2) >= c(1,0) ; +(8,3) >= c(1,1) ; +(8,4) >= c(1,2) ; +(8,5) >= c(1,3) ; +(8,6) >= c(1,4) ; +(8,7) >= c(1,5) ; +(8,8) >= c(1,6) ; +(8,9) >= c(1,7) ; +(9,0) >= 9 ; +(9,1) >= c(1,0) ; +(9,2) >= c(1,1) ; +(9,3) >= c(1,2) ; +(9,4) >= c(1,3) ; +(9,5) >= c(1,4) ; +(9,6) >= c(1,5) ; +(9,7) >= c(1,6) ; +(9,8) >= c(1,7) ; +(9,9) >= c(1,8) ; +(c(x,y),z) >= c(x,+(y,z)) ; +(x,c(y,z)) >= c(y,+(x,z)) ; c(0,x) >= x ; c(x,c(y,z)) >= c(+(x,y),z) ; Marked_c(x,c(y,z)) >= Marked_c(+(x,y),z) ; Marked_c(x,c(y,z)) >= Marked_+(x,y) ; Marked_+(c(x,y),z) >= Marked_c(x,+(y,z)) ; Marked_+(c(x,y),z) >= Marked_+(y,z) ; Marked_+(x,c(y,z)) >= Marked_c(y,+(x,z)) ; Marked_+(x,c(y,z)) >= Marked_+(x,z) ; } + Disjunctions:{ { Marked_c(x,c(y,z)) > Marked_c(+(x,y),z) ; } { Marked_c(x,c(y,z)) > Marked_+(x,y) ; } { Marked_+(c(x,y),z) > Marked_c(x,+(y,z)) ; } { Marked_+(c(x,y),z) > Marked_+(y,z) ; } { Marked_+(x,c(y,z)) > Marked_c(y,+(x,z)) ; } { Marked_+(x,c(y,z)) > Marked_+(x,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: +(0,0) >= 0 constraint: +(0,1) >= 1 constraint: +(0,2) >= 2 constraint: +(0,3) >= 3 constraint: +(0,4) >= 4 constraint: +(0,5) >= 5 constraint: +(0,6) >= 6 constraint: +(0,7) >= 7 constraint: +(0,8) >= 8 constraint: +(0,9) >= 9 constraint: +(1,0) >= 1 constraint: +(1,1) >= 2 constraint: +(1,2) >= 3 constraint: +(1,3) >= 4 constraint: +(1,4) >= 5 constraint: +(1,5) >= 6 constraint: +(1,6) >= 7 constraint: +(1,7) >= 8 constraint: +(1,8) >= 9 constraint: +(1,9) >= c(1,0) constraint: +(2,0) >= 2 constraint: +(2,1) >= 3 constraint: +(2,2) >= 4 constraint: +(2,3) >= 5 constraint: +(2,4) >= 6 constraint: +(2,5) >= 7 constraint: +(2,6) >= 8 constraint: +(2,7) >= 9 constraint: +(2,8) >= c(1,0) constraint: +(2,9) >= c(1,1) constraint: +(3,0) >= 3 constraint: +(3,1) >= 4 constraint: +(3,2) >= 5 constraint: +(3,3) >= 6 constraint: +(3,4) >= 7 constraint: +(3,5) >= 8 constraint: +(3,6) >= 9 constraint: +(3,7) >= c(1,0) constraint: +(3,8) >= c(1,1) constraint: +(3,9) >= c(1,2) constraint: +(4,0) >= 4 constraint: +(4,1) >= 5 constraint: +(4,2) >= 6 constraint: +(4,3) >= 7 constraint: +(4,4) >= 8 constraint: +(4,5) >= 9 constraint: +(4,6) >= c(1,0) constraint: +(4,7) >= c(1,1) constraint: +(4,8) >= c(1,2) constraint: +(4,9) >= c(1,3) constraint: +(5,0) >= 5 constraint: +(5,1) >= 6 constraint: +(5,2) >= 7 constraint: +(5,3) >= 8 constraint: +(5,4) >= 9 constraint: +(5,5) >= c(1,0) constraint: +(5,6) >= c(1,1) constraint: +(5,7) >= c(1,2) constraint: +(5,8) >= c(1,3) constraint: +(5,9) >= c(1,4) constraint: +(6,0) >= 6 constraint: +(6,1) >= 7 constraint: +(6,2) >= 8 constraint: +(6,3) >= 9 constraint: +(6,4) >= c(1,0) constraint: +(6,5) >= c(1,1) constraint: +(6,6) >= c(1,2) constraint: +(6,7) >= c(1,3) constraint: +(6,8) >= c(1,4) constraint: +(6,9) >= c(1,5) constraint: +(7,0) >= 7 constraint: +(7,1) >= 8 constraint: +(7,2) >= 9 constraint: +(7,3) >= c(1,0) constraint: +(7,4) >= c(1,1) constraint: +(7,5) >= c(1,2) constraint: +(7,6) >= c(1,3) constraint: +(7,7) >= c(1,4) constraint: +(7,8) >= c(1,5) constraint: +(7,9) >= c(1,6) constraint: +(8,0) >= 8 constraint: +(8,1) >= 9 constraint: +(8,2) >= c(1,0) constraint: +(8,3) >= c(1,1) constraint: +(8,4) >= c(1,2) constraint: +(8,5) >= c(1,3) constraint: +(8,6) >= c(1,4) constraint: +(8,7) >= c(1,5) constraint: +(8,8) >= c(1,6) constraint: +(8,9) >= c(1,7) constraint: +(9,0) >= 9 constraint: +(9,1) >= c(1,0) constraint: +(9,2) >= c(1,1) constraint: +(9,3) >= c(1,2) constraint: +(9,4) >= c(1,3) constraint: +(9,5) >= c(1,4) constraint: +(9,6) >= c(1,5) constraint: +(9,7) >= c(1,6) constraint: +(9,8) >= c(1,7) constraint: +(9,9) >= c(1,8) constraint: +(c(x,y),z) >= c(x,+(y,z)) constraint: +(x,c(y,z)) >= c(y,+(x,z)) constraint: c(0,x) >= x constraint: c(x,c(y,z)) >= c(+(x,y),z) constraint: Marked_c(x,c(y,z)) >= Marked_c(+(x,y),z) constraint: Marked_c(x,c(y,z)) >= Marked_+(x,y) constraint: Marked_+(c(x,y),z) >= Marked_c(x,+(y,z)) constraint: Marked_+(c(x,y),z) >= Marked_+(y,z) constraint: Marked_+(x,c(y,z)) >= Marked_c(y,+(x,z)) constraint: Marked_+(x,c(y,z)) >= Marked_+(x,z) APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { +(0,0) >= 0 ; +(0,1) >= 1 ; +(0,2) >= 2 ; +(0,3) >= 3 ; +(0,4) >= 4 ; +(0,5) >= 5 ; +(0,6) >= 6 ; +(0,7) >= 7 ; +(0,8) >= 8 ; +(0,9) >= 9 ; +(1,0) >= 1 ; +(1,1) >= 2 ; +(1,2) >= 3 ; +(1,3) >= 4 ; +(1,4) >= 5 ; +(1,5) >= 6 ; +(1,6) >= 7 ; +(1,7) >= 8 ; +(1,8) >= 9 ; +(1,9) >= c(1,0) ; +(2,0) >= 2 ; +(2,1) >= 3 ; +(2,2) >= 4 ; +(2,3) >= 5 ; +(2,4) >= 6 ; +(2,5) >= 7 ; +(2,6) >= 8 ; +(2,7) >= 9 ; +(2,8) >= c(1,0) ; +(2,9) >= c(1,1) ; +(3,0) >= 3 ; +(3,1) >= 4 ; +(3,2) >= 5 ; +(3,3) >= 6 ; +(3,4) >= 7 ; +(3,5) >= 8 ; +(3,6) >= 9 ; +(3,7) >= c(1,0) ; +(3,8) >= c(1,1) ; +(3,9) >= c(1,2) ; +(4,0) >= 4 ; +(4,1) >= 5 ; +(4,2) >= 6 ; +(4,3) >= 7 ; +(4,4) >= 8 ; +(4,5) >= 9 ; +(4,6) >= c(1,0) ; +(4,7) >= c(1,1) ; +(4,8) >= c(1,2) ; +(4,9) >= c(1,3) ; +(5,0) >= 5 ; +(5,1) >= 6 ; +(5,2) >= 7 ; +(5,3) >= 8 ; +(5,4) >= 9 ; +(5,5) >= c(1,0) ; +(5,6) >= c(1,1) ; +(5,7) >= c(1,2) ; +(5,8) >= c(1,3) ; +(5,9) >= c(1,4) ; +(6,0) >= 6 ; +(6,1) >= 7 ; +(6,2) >= 8 ; +(6,3) >= 9 ; +(6,4) >= c(1,0) ; +(6,5) >= c(1,1) ; +(6,6) >= c(1,2) ; +(6,7) >= c(1,3) ; +(6,8) >= c(1,4) ; +(6,9) >= c(1,5) ; +(7,0) >= 7 ; +(7,1) >= 8 ; +(7,2) >= 9 ; +(7,3) >= c(1,0) ; +(7,4) >= c(1,1) ; +(7,5) >= c(1,2) ; +(7,6) >= c(1,3) ; +(7,7) >= c(1,4) ; +(7,8) >= c(1,5) ; +(7,9) >= c(1,6) ; +(8,0) >= 8 ; +(8,1) >= 9 ; +(8,2) >= c(1,0) ; +(8,3) >= c(1,1) ; +(8,4) >= c(1,2) ; +(8,5) >= c(1,3) ; +(8,6) >= c(1,4) ; +(8,7) >= c(1,5) ; +(8,8) >= c(1,6) ; +(8,9) >= c(1,7) ; +(9,0) >= 9 ; +(9,1) >= c(1,0) ; +(9,2) >= c(1,1) ; +(9,3) >= c(1,2) ; +(9,4) >= c(1,3) ; +(9,5) >= c(1,4) ; +(9,6) >= c(1,5) ; +(9,7) >= c(1,6) ; +(9,8) >= c(1,7) ; +(9,9) >= c(1,8) ; +(c(x,y),z) >= c(x,+(y,z)) ; +(x,c(y,z)) >= c(y,+(x,z)) ; c(0,x) >= x ; c(x,c(y,z)) >= c(+(x,y),z) ; Marked_c(x,c(y,z)) >= Marked_c(+(x,y),z) ; } + Disjunctions:{ { Marked_c(x,c(y,z)) > Marked_c(+(x,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: +(0,0) >= 0 constraint: +(0,1) >= 1 constraint: +(0,2) >= 2 constraint: +(0,3) >= 3 constraint: +(0,4) >= 4 constraint: +(0,5) >= 5 constraint: +(0,6) >= 6 constraint: +(0,7) >= 7 constraint: +(0,8) >= 8 constraint: +(0,9) >= 9 constraint: +(1,0) >= 1 constraint: +(1,1) >= 2 constraint: +(1,2) >= 3 constraint: +(1,3) >= 4 constraint: +(1,4) >= 5 constraint: +(1,5) >= 6 constraint: +(1,6) >= 7 constraint: +(1,7) >= 8 constraint: +(1,8) >= 9 constraint: +(1,9) >= c(1,0) constraint: +(2,0) >= 2 constraint: +(2,1) >= 3 constraint: +(2,2) >= 4 constraint: +(2,3) >= 5 constraint: +(2,4) >= 6 constraint: +(2,5) >= 7 constraint: +(2,6) >= 8 constraint: +(2,7) >= 9 constraint: +(2,8) >= c(1,0) constraint: +(2,9) >= c(1,1) constraint: +(3,0) >= 3 constraint: +(3,1) >= 4 constraint: +(3,2) >= 5 constraint: +(3,3) >= 6 constraint: +(3,4) >= 7 constraint: +(3,5) >= 8 constraint: +(3,6) >= 9 constraint: +(3,7) >= c(1,0) constraint: +(3,8) >= c(1,1) constraint: +(3,9) >= c(1,2) constraint: +(4,0) >= 4 constraint: +(4,1) >= 5 constraint: +(4,2) >= 6 constraint: +(4,3) >= 7 constraint: +(4,4) >= 8 constraint: +(4,5) >= 9 constraint: +(4,6) >= c(1,0) constraint: +(4,7) >= c(1,1) constraint: +(4,8) >= c(1,2) constraint: +(4,9) >= c(1,3) constraint: +(5,0) >= 5 constraint: +(5,1) >= 6 constraint: +(5,2) >= 7 constraint: +(5,3) >= 8 constraint: +(5,4) >= 9 constraint: +(5,5) >= c(1,0) constraint: +(5,6) >= c(1,1) constraint: +(5,7) >= c(1,2) constraint: +(5,8) >= c(1,3) constraint: +(5,9) >= c(1,4) constraint: +(6,0) >= 6 constraint: +(6,1) >= 7 constraint: +(6,2) >= 8 constraint: +(6,3) >= 9 constraint: +(6,4) >= c(1,0) constraint: +(6,5) >= c(1,1) constraint: +(6,6) >= c(1,2) constraint: +(6,7) >= c(1,3) constraint: +(6,8) >= c(1,4) constraint: +(6,9) >= c(1,5) constraint: +(7,0) >= 7 constraint: +(7,1) >= 8 constraint: +(7,2) >= 9 constraint: +(7,3) >= c(1,0) constraint: +(7,4) >= c(1,1) constraint: +(7,5) >= c(1,2) constraint: +(7,6) >= c(1,3) constraint: +(7,7) >= c(1,4) constraint: +(7,8) >= c(1,5) constraint: +(7,9) >= c(1,6) constraint: +(8,0) >= 8 constraint: +(8,1) >= 9 constraint: +(8,2) >= c(1,0) constraint: +(8,3) >= c(1,1) constraint: +(8,4) >= c(1,2) constraint: +(8,5) >= c(1,3) constraint: +(8,6) >= c(1,4) constraint: +(8,7) >= c(1,5) constraint: +(8,8) >= c(1,6) constraint: +(8,9) >= c(1,7) constraint: +(9,0) >= 9 constraint: +(9,1) >= c(1,0) constraint: +(9,2) >= c(1,1) constraint: +(9,3) >= c(1,2) constraint: +(9,4) >= c(1,3) constraint: +(9,5) >= c(1,4) constraint: +(9,6) >= c(1,5) constraint: +(9,7) >= c(1,6) constraint: +(9,8) >= c(1,7) constraint: +(9,9) >= c(1,8) constraint: +(c(x,y),z) >= c(x,+(y,z)) constraint: +(x,c(y,z)) >= c(y,+(x,z)) constraint: c(0,x) >= x constraint: c(x,c(y,z)) >= c(+(x,y),z) constraint: Marked_c(x,c(y,z)) >= Marked_c(+(x,y),z) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] +(0,0) -> 0 [2] +(0,1) -> 1 [3] +(0,2) -> 2 [4] +(0,3) -> 3 [5] +(0,4) -> 4 [6] +(0,5) -> 5 [7] +(0,6) -> 6 [8] +(0,7) -> 7 [9] +(0,8) -> 8 [10] +(0,9) -> 9 [11] +(1,0) -> 1 [12] +(1,1) -> 2 [13] +(1,2) -> 3 [14] +(1,3) -> 4 [15] +(1,4) -> 5 [16] +(1,5) -> 6 [17] +(1,6) -> 7 [18] +(1,7) -> 8 [19] +(1,8) -> 9 [20] +(1,9) -> c(1,0) [21] +(2,0) -> 2 [22] +(2,1) -> 3 [23] +(2,2) -> 4 [24] +(2,3) -> 5 [25] +(2,4) -> 6 [26] +(2,5) -> 7 [27] +(2,6) -> 8 [28] +(2,7) -> 9 [29] +(2,8) -> c(1,0) [30] +(2,9) -> c(1,1) [31] +(3,0) -> 3 [32] +(3,1) -> 4 [33] +(3,2) -> 5 [34] +(3,3) -> 6 [35] +(3,4) -> 7 [36] +(3,5) -> 8 [37] +(3,6) -> 9 [38] +(3,7) -> c(1,0) [39] +(3,8) -> c(1,1) [40] +(3,9) -> c(1,2) [41] +(4,0) -> 4 [42] +(4,1) -> 5 [43] +(4,2) -> 6 [44] +(4,3) -> 7 [45] +(4,4) -> 8 [46] +(4,5) -> 9 [47] +(4,6) -> c(1,0) [48] +(4,7) -> c(1,1) [49] +(4,8) -> c(1,2) [50] +(4,9) -> c(1,3) [51] +(5,0) -> 5 [52] +(5,1) -> 6 [53] +(5,2) -> 7 [54] +(5,3) -> 8 [55] +(5,4) -> 9 [56] +(5,5) -> c(1,0) [57] +(5,6) -> c(1,1) [58] +(5,7) -> c(1,2) [59] +(5,8) -> c(1,3) [60] +(5,9) -> c(1,4) [61] +(6,0) -> 6 [62] +(6,1) -> 7 [63] +(6,2) -> 8 [64] +(6,3) -> 9 [65] +(6,4) -> c(1,0) [66] +(6,5) -> c(1,1) [67] +(6,6) -> c(1,2) [68] +(6,7) -> c(1,3) [69] +(6,8) -> c(1,4) [70] +(6,9) -> c(1,5) [71] +(7,0) -> 7 [72] +(7,1) -> 8 [73] +(7,2) -> 9 [74] +(7,3) -> c(1,0) [75] +(7,4) -> c(1,1) [76] +(7,5) -> c(1,2) [77] +(7,6) -> c(1,3) [78] +(7,7) -> c(1,4) [79] +(7,8) -> c(1,5) [80] +(7,9) -> c(1,6) [81] +(8,0) -> 8 [82] +(8,1) -> 9 [83] +(8,2) -> c(1,0) [84] +(8,3) -> c(1,1) [85] +(8,4) -> c(1,2) [86] +(8,5) -> c(1,3) [87] +(8,6) -> c(1,4) [88] +(8,7) -> c(1,5) [89] +(8,8) -> c(1,6) [90] +(8,9) -> c(1,7) [91] +(9,0) -> 9 [92] +(9,1) -> c(1,0) [93] +(9,2) -> c(1,1) [94] +(9,3) -> c(1,2) [95] +(9,4) -> c(1,3) [96] +(9,5) -> c(1,4) [97] +(9,6) -> c(1,5) [98] +(9,7) -> c(1,6) [99] +(9,8) -> c(1,7) [100] +(9,9) -> c(1,8) [101] +(x,c(y,z)) -> c(y,+(x,z)) [102] +(c(x,y),z) -> c(x,+(y,z)) [103] c(0,x) -> x [104] c(x,c(y,z)) -> c(+(x,y),z) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ 0 ] () = 0; [ 7 ] () = 2; [ 3 ] () = 1; [ Marked_c ] (X0,X1) = 1*X1 + 3*X0 + 3; [ 1 ] () = 0; [ 9 ] () = 2; [ 5 ] () = 1; [ + ] (X0,X1) = 1*X1 + 1*X0 + 1; [ 8 ] () = 2; [ 4 ] () = 1; [ Marked_+ ] (X0,X1) = 1*X1 + 3*X0 + 3; [ 2 ] () = 0; [ c ] (X0,X1) = 1*X1 + 3*X0 + 3; [ 6 ] () = 2; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ 0 ] () = 0; [ 7 ] () = 0; [ 3 ] () = 0; [ Marked_c ] (X0,X1) = 3*X1 + 0; [ 1 ] () = 0; [ 9 ] () = 0; [ 5 ] () = 0; [ + ] (X0,X1) = 2 + 1*X0 + 2*X1 + 0; [ 8 ] () = 0; [ 4 ] () = 0; [ 2 ] () = 0; [ c ] (X0,X1) = 2 + 1*X1 + 0; [ 6 ] () = 0; ]} ]} ]} ]} ]} Cime worked for 0.649950 seconds (real time) Cime Exit Status: 0