- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] c(0,x) -> x [2] c(x,c(y,z)) -> c(+(x,y),z) [3] +(0,0) -> 0 [4] +(0,1) -> 1 [5] +(0,2) -> 2 [6] +(0,3) -> 3 [7] +(0,4) -> 4 [8] +(0,5) -> 5 [9] +(0,6) -> 6 [10] +(0,7) -> 7 [11] +(0,8) -> 8 [12] +(0,9) -> 9 [13] +(1,0) -> 1 [14] +(1,1) -> 2 [15] +(1,2) -> 3 [16] +(1,3) -> 4 [17] +(1,4) -> 5 [18] +(1,5) -> 6 [19] +(1,6) -> 7 [20] +(1,7) -> 8 [21] +(1,8) -> 9 [22] +(1,9) -> c(1,0) [23] +(2,0) -> 2 [24] +(2,1) -> 3 [25] +(2,2) -> 4 [26] +(2,3) -> 5 [27] +(2,4) -> 6 [28] +(2,5) -> 7 [29] +(2,6) -> 8 [30] +(2,7) -> 9 [31] +(2,8) -> c(1,0) [32] +(2,9) -> c(1,1) [33] +(3,0) -> 3 [34] +(3,1) -> 4 [35] +(3,2) -> 5 [36] +(3,3) -> 6 [37] +(3,4) -> 7 [38] +(3,5) -> 8 [39] +(3,6) -> 9 [40] +(3,7) -> c(1,0) [41] +(3,8) -> c(1,1) [42] +(3,9) -> c(1,2) [43] +(4,0) -> 4 [44] +(4,1) -> 5 [45] +(4,2) -> 6 [46] +(4,3) -> 7 [47] +(4,4) -> 8 [48] +(4,5) -> 9 [49] +(4,6) -> c(1,0) [50] +(4,7) -> c(1,1) [51] +(4,8) -> c(1,2) [52] +(4,9) -> c(1,3) [53] +(5,0) -> 5 [54] +(5,1) -> 6 [55] +(5,2) -> 7 [56] +(5,3) -> 8 [57] +(5,4) -> 9 [58] +(5,5) -> c(1,0) [59] +(5,6) -> c(1,1) [60] +(5,7) -> c(1,2) [61] +(5,8) -> c(1,3) [62] +(5,9) -> c(1,4) [63] +(6,0) -> 6 [64] +(6,1) -> 7 [65] +(6,2) -> 8 [66] +(6,3) -> 9 [67] +(6,4) -> c(1,0) [68] +(6,5) -> c(1,1) [69] +(6,6) -> c(1,2) [70] +(6,7) -> c(1,3) [71] +(6,8) -> c(1,4) [72] +(6,9) -> c(1,5) [73] +(7,0) -> 7 [74] +(7,1) -> 8 [75] +(7,2) -> 9 [76] +(7,3) -> c(1,0) [77] +(7,4) -> c(1,1) [78] +(7,5) -> c(1,2) [79] +(7,6) -> c(1,3) [80] +(7,7) -> c(1,4) [81] +(7,8) -> c(1,5) [82] +(7,9) -> c(1,6) [83] +(8,0) -> 8 [84] +(8,1) -> 9 [85] +(8,2) -> c(1,0) [86] +(8,3) -> c(1,1) [87] +(8,4) -> c(1,2) [88] +(8,5) -> c(1,3) [89] +(8,6) -> c(1,4) [90] +(8,7) -> c(1,5) [91] +(8,8) -> c(1,6) [92] +(8,9) -> c(1,7) [93] +(9,0) -> 9 [94] +(9,1) -> c(1,0) [95] +(9,2) -> c(1,1) [96] +(9,3) -> c(1,2) [97] +(9,4) -> c(1,3) [98] +(9,5) -> c(1,4) [99] +(9,6) -> c(1,5) [100] +(9,7) -> c(1,6) [101] +(9,8) -> c(1,7) [102] +(9,9) -> c(1,8) [103] +(x,c(y,z)) -> c(y,+(x,z)) [104] +(c(x,y),z) -> c(x,+(y,z)) [105] *(0,0) -> 0 [106] *(0,1) -> 0 [107] *(0,2) -> 0 [108] *(0,3) -> 0 [109] *(0,4) -> 0 [110] *(0,5) -> 0 [111] *(0,6) -> 0 [112] *(0,7) -> 0 [113] *(0,8) -> 0 [114] *(0,9) -> 0 [115] *(1,0) -> 0 [116] *(1,1) -> 1 [117] *(1,2) -> 2 [118] *(1,3) -> 3 [119] *(1,4) -> 4 [120] *(1,5) -> 5 [121] *(1,6) -> 6 [122] *(1,7) -> 7 [123] *(1,8) -> 8 [124] *(1,9) -> 9 [125] *(2,0) -> 0 [126] *(2,1) -> 2 [127] *(2,2) -> 4 [128] *(2,3) -> 6 [129] *(2,4) -> 8 [130] *(2,5) -> c(1,0) [131] *(2,6) -> c(1,2) [132] *(2,7) -> c(1,4) [133] *(2,8) -> c(1,6) [134] *(2,9) -> c(1,8) [135] *(3,0) -> 0 [136] *(3,1) -> 3 [137] *(3,2) -> 6 [138] *(3,3) -> 9 [139] *(3,4) -> c(1,2) [140] *(3,5) -> c(1,5) [141] *(3,6) -> c(1,8) [142] *(3,7) -> c(2,1) [143] *(3,8) -> c(2,4) [144] *(3,9) -> c(2,7) [145] *(4,0) -> 0 [146] *(4,1) -> 4 [147] *(4,2) -> 8 [148] *(4,3) -> c(1,2) [149] *(4,4) -> c(1,6) [150] *(4,5) -> c(2,0) [151] *(4,6) -> c(2,4) [152] *(4,7) -> c(2,8) [153] *(4,8) -> c(3,2) [154] *(4,9) -> c(3,6) [155] *(5,0) -> 0 [156] *(5,1) -> 5 [157] *(5,2) -> c(1,0) [158] *(5,3) -> c(1,5) [159] *(5,4) -> c(2,0) [160] *(5,5) -> c(2,5) [161] *(5,6) -> c(3,0) [162] *(5,7) -> c(3,5) [163] *(5,8) -> c(4,0) [164] *(5,9) -> c(4,5) [165] *(6,0) -> 0 [166] *(6,1) -> 6 [167] *(6,2) -> c(1,2) [168] *(6,3) -> c(1,8) [169] *(6,4) -> c(2,4) [170] *(6,5) -> c(3,0) [171] *(6,6) -> c(3,6) [172] *(6,7) -> c(4,2) [173] *(6,8) -> c(4,8) [174] *(6,9) -> c(5,4) [175] *(7,0) -> 0 [176] *(7,1) -> 7 [177] *(7,2) -> c(1,4) [178] *(7,3) -> c(2,1) [179] *(7,4) -> c(2,8) [180] *(7,5) -> c(3,5) [181] *(7,6) -> c(4,2) [182] *(7,7) -> c(4,9) [183] *(7,8) -> c(5,6) [184] *(7,9) -> c(6,3) [185] *(8,0) -> 0 [186] *(8,1) -> 8 [187] *(8,2) -> c(1,8) [188] *(8,3) -> c(2,4) [189] *(8,4) -> c(3,2) [190] *(8,5) -> c(4,0) [191] *(8,6) -> c(4,8) [192] *(8,7) -> c(5,6) [193] *(8,8) -> c(6,4) [194] *(8,9) -> c(7,2) [195] *(9,0) -> 0 [196] *(9,1) -> 9 [197] *(9,2) -> c(1,8) [198] *(9,3) -> c(2,7) [199] *(9,4) -> c(3,6) [200] *(9,5) -> c(4,5) [201] *(9,6) -> c(5,4) [202] *(9,7) -> c(6,3) [203] *(9,8) -> c(7,2) [204] *(9,9) -> c(8,1) [205] *(x,c(y,z)) -> c( *(x,y), *(x,z)) [206] *(c(x,y),z) -> c( *(x,z), *(y,z)) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 2 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_* -> 2 APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { c(0,x) >= x ; c(x,c(y,z)) >= c(+(x,y),z) ; +(c(x,y),z) >= c(x,+(y,z)) ; +(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) ; +(x,c(y,z)) >= c(y,+(x,z)) ; *(c(x,y),z) >= c( *(x,z), *(y,z)) ; *(0,0) >= 0 ; *(0,1) >= 0 ; *(0,2) >= 0 ; *(0,3) >= 0 ; *(0,4) >= 0 ; *(0,5) >= 0 ; *(0,6) >= 0 ; *(0,7) >= 0 ; *(0,8) >= 0 ; *(0,9) >= 0 ; *(1,0) >= 0 ; *(1,1) >= 1 ; *(1,2) >= 2 ; *(1,3) >= 3 ; *(1,4) >= 4 ; *(1,5) >= 5 ; *(1,6) >= 6 ; *(1,7) >= 7 ; *(1,8) >= 8 ; *(1,9) >= 9 ; *(2,0) >= 0 ; *(2,1) >= 2 ; *(2,2) >= 4 ; *(2,3) >= 6 ; *(2,4) >= 8 ; *(2,5) >= c(1,0) ; *(2,6) >= c(1,2) ; *(2,7) >= c(1,4) ; *(2,8) >= c(1,6) ; *(2,9) >= c(1,8) ; *(3,0) >= 0 ; *(3,1) >= 3 ; *(3,2) >= 6 ; *(3,3) >= 9 ; *(3,4) >= c(1,2) ; *(3,5) >= c(1,5) ; *(3,6) >= c(1,8) ; *(3,7) >= c(2,1) ; *(3,8) >= c(2,4) ; *(3,9) >= c(2,7) ; *(4,0) >= 0 ; *(4,1) >= 4 ; *(4,2) >= 8 ; *(4,3) >= c(1,2) ; *(4,4) >= c(1,6) ; *(4,5) >= c(2,0) ; *(4,6) >= c(2,4) ; *(4,7) >= c(2,8) ; *(4,8) >= c(3,2) ; *(4,9) >= c(3,6) ; *(5,0) >= 0 ; *(5,1) >= 5 ; *(5,2) >= c(1,0) ; *(5,3) >= c(1,5) ; *(5,4) >= c(2,0) ; *(5,5) >= c(2,5) ; *(5,6) >= c(3,0) ; *(5,7) >= c(3,5) ; *(5,8) >= c(4,0) ; *(5,9) >= c(4,5) ; *(6,0) >= 0 ; *(6,1) >= 6 ; *(6,2) >= c(1,2) ; *(6,3) >= c(1,8) ; *(6,4) >= c(2,4) ; *(6,5) >= c(3,0) ; *(6,6) >= c(3,6) ; *(6,7) >= c(4,2) ; *(6,8) >= c(4,8) ; *(6,9) >= c(5,4) ; *(7,0) >= 0 ; *(7,1) >= 7 ; *(7,2) >= c(1,4) ; *(7,3) >= c(2,1) ; *(7,4) >= c(2,8) ; *(7,5) >= c(3,5) ; *(7,6) >= c(4,2) ; *(7,7) >= c(4,9) ; *(7,8) >= c(5,6) ; *(7,9) >= c(6,3) ; *(8,0) >= 0 ; *(8,1) >= 8 ; *(8,2) >= c(1,8) ; *(8,3) >= c(2,4) ; *(8,4) >= c(3,2) ; *(8,5) >= c(4,0) ; *(8,6) >= c(4,8) ; *(8,7) >= c(5,6) ; *(8,8) >= c(6,4) ; *(8,9) >= c(7,2) ; *(9,0) >= 0 ; *(9,1) >= 9 ; *(9,2) >= c(1,8) ; *(9,3) >= c(2,7) ; *(9,4) >= c(3,6) ; *(9,5) >= c(4,5) ; *(9,6) >= c(5,4) ; *(9,7) >= c(6,3) ; *(9,8) >= c(7,2) ; *(9,9) >= c(8,1) ; *(x,c(y,z)) >= c( *(x,y), *(x,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 === 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 : 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: c(0,x) >= x constraint: c(x,c(y,z)) >= c(+(x,y),z) constraint: +(c(x,y),z) >= c(x,+(y,z)) 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: +(x,c(y,z)) >= c(y,+(x,z)) constraint: *(c(x,y),z) >= c( *(x,z), *(y,z)) constraint: *(0,0) >= 0 constraint: *(0,1) >= 0 constraint: *(0,2) >= 0 constraint: *(0,3) >= 0 constraint: *(0,4) >= 0 constraint: *(0,5) >= 0 constraint: *(0,6) >= 0 constraint: *(0,7) >= 0 constraint: *(0,8) >= 0 constraint: *(0,9) >= 0 constraint: *(1,0) >= 0 constraint: *(1,1) >= 1 constraint: *(1,2) >= 2 constraint: *(1,3) >= 3 constraint: *(1,4) >= 4 constraint: *(1,5) >= 5 constraint: *(1,6) >= 6 constraint: *(1,7) >= 7 constraint: *(1,8) >= 8 constraint: *(1,9) >= 9 constraint: *(2,0) >= 0 constraint: *(2,1) >= 2 constraint: *(2,2) >= 4 constraint: *(2,3) >= 6 constraint: *(2,4) >= 8 constraint: *(2,5) >= c(1,0) constraint: *(2,6) >= c(1,2) constraint: *(2,7) >= c(1,4) constraint: *(2,8) >= c(1,6) constraint: *(2,9) >= c(1,8) constraint: *(3,0) >= 0 constraint: *(3,1) >= 3 constraint: *(3,2) >= 6 constraint: *(3,3) >= 9 constraint: *(3,4) >= c(1,2) constraint: *(3,5) >= c(1,5) constraint: *(3,6) >= c(1,8) constraint: *(3,7) >= c(2,1) constraint: *(3,8) >= c(2,4) constraint: *(3,9) >= c(2,7) constraint: *(4,0) >= 0 constraint: *(4,1) >= 4 constraint: *(4,2) >= 8 constraint: *(4,3) >= c(1,2) constraint: *(4,4) >= c(1,6) constraint: *(4,5) >= c(2,0) constraint: *(4,6) >= c(2,4) constraint: *(4,7) >= c(2,8) constraint: *(4,8) >= c(3,2) constraint: *(4,9) >= c(3,6) constraint: *(5,0) >= 0 constraint: *(5,1) >= 5 constraint: *(5,2) >= c(1,0) constraint: *(5,3) >= c(1,5) constraint: *(5,4) >= c(2,0) constraint: *(5,5) >= c(2,5) constraint: *(5,6) >= c(3,0) constraint: *(5,7) >= c(3,5) constraint: *(5,8) >= c(4,0) constraint: *(5,9) >= c(4,5) constraint: *(6,0) >= 0 constraint: *(6,1) >= 6 constraint: *(6,2) >= c(1,2) constraint: *(6,3) >= c(1,8) constraint: *(6,4) >= c(2,4) constraint: *(6,5) >= c(3,0) constraint: *(6,6) >= c(3,6) constraint: *(6,7) >= c(4,2) constraint: *(6,8) >= c(4,8) constraint: *(6,9) >= c(5,4) constraint: *(7,0) >= 0 constraint: *(7,1) >= 7 constraint: *(7,2) >= c(1,4) constraint: *(7,3) >= c(2,1) constraint: *(7,4) >= c(2,8) constraint: *(7,5) >= c(3,5) constraint: *(7,6) >= c(4,2) constraint: *(7,7) >= c(4,9) constraint: *(7,8) >= c(5,6) constraint: *(7,9) >= c(6,3) constraint: *(8,0) >= 0 constraint: *(8,1) >= 8 constraint: *(8,2) >= c(1,8) constraint: *(8,3) >= c(2,4) constraint: *(8,4) >= c(3,2) constraint: *(8,5) >= c(4,0) constraint: *(8,6) >= c(4,8) constraint: *(8,7) >= c(5,6) constraint: *(8,8) >= c(6,4) constraint: *(8,9) >= c(7,2) constraint: *(9,0) >= 0 constraint: *(9,1) >= 9 constraint: *(9,2) >= c(1,8) constraint: *(9,3) >= c(2,7) constraint: *(9,4) >= c(3,6) constraint: *(9,5) >= c(4,5) constraint: *(9,6) >= c(5,4) constraint: *(9,7) >= c(6,3) constraint: *(9,8) >= c(7,2) constraint: *(9,9) >= c(8,1) constraint: *(x,c(y,z)) >= c( *(x,y), *(x,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 (Subterm criterion) ST: Marked_* -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] c(0,x) -> x [2] c(x,c(y,z)) -> c(+(x,y),z) [3] +(0,0) -> 0 [4] +(0,1) -> 1 [5] +(0,2) -> 2 [6] +(0,3) -> 3 [7] +(0,4) -> 4 [8] +(0,5) -> 5 [9] +(0,6) -> 6 [10] +(0,7) -> 7 [11] +(0,8) -> 8 [12] +(0,9) -> 9 [13] +(1,0) -> 1 [14] +(1,1) -> 2 [15] +(1,2) -> 3 [16] +(1,3) -> 4 [17] +(1,4) -> 5 [18] +(1,5) -> 6 [19] +(1,6) -> 7 [20] +(1,7) -> 8 [21] +(1,8) -> 9 [22] +(1,9) -> c(1,0) [23] +(2,0) -> 2 [24] +(2,1) -> 3 [25] +(2,2) -> 4 [26] +(2,3) -> 5 [27] +(2,4) -> 6 [28] +(2,5) -> 7 [29] +(2,6) -> 8 [30] +(2,7) -> 9 [31] +(2,8) -> c(1,0) [32] +(2,9) -> c(1,1) [33] +(3,0) -> 3 [34] +(3,1) -> 4 [35] +(3,2) -> 5 [36] +(3,3) -> 6 [37] +(3,4) -> 7 [38] +(3,5) -> 8 [39] +(3,6) -> 9 [40] +(3,7) -> c(1,0) [41] +(3,8) -> c(1,1) [42] +(3,9) -> c(1,2) [43] +(4,0) -> 4 [44] +(4,1) -> 5 [45] +(4,2) -> 6 [46] +(4,3) -> 7 [47] +(4,4) -> 8 [48] +(4,5) -> 9 [49] +(4,6) -> c(1,0) [50] +(4,7) -> c(1,1) [51] +(4,8) -> c(1,2) [52] +(4,9) -> c(1,3) [53] +(5,0) -> 5 [54] +(5,1) -> 6 [55] +(5,2) -> 7 [56] +(5,3) -> 8 [57] +(5,4) -> 9 [58] +(5,5) -> c(1,0) [59] +(5,6) -> c(1,1) [60] +(5,7) -> c(1,2) [61] +(5,8) -> c(1,3) [62] +(5,9) -> c(1,4) [63] +(6,0) -> 6 [64] +(6,1) -> 7 [65] +(6,2) -> 8 [66] +(6,3) -> 9 [67] +(6,4) -> c(1,0) [68] +(6,5) -> c(1,1) [69] +(6,6) -> c(1,2) [70] +(6,7) -> c(1,3) [71] +(6,8) -> c(1,4) [72] +(6,9) -> c(1,5) [73] +(7,0) -> 7 [74] +(7,1) -> 8 [75] +(7,2) -> 9 [76] +(7,3) -> c(1,0) [77] +(7,4) -> c(1,1) [78] +(7,5) -> c(1,2) [79] +(7,6) -> c(1,3) [80] +(7,7) -> c(1,4) [81] +(7,8) -> c(1,5) [82] +(7,9) -> c(1,6) [83] +(8,0) -> 8 [84] +(8,1) -> 9 [85] +(8,2) -> c(1,0) [86] +(8,3) -> c(1,1) [87] +(8,4) -> c(1,2) [88] +(8,5) -> c(1,3) [89] +(8,6) -> c(1,4) [90] +(8,7) -> c(1,5) [91] +(8,8) -> c(1,6) [92] +(8,9) -> c(1,7) [93] +(9,0) -> 9 [94] +(9,1) -> c(1,0) [95] +(9,2) -> c(1,1) [96] +(9,3) -> c(1,2) [97] +(9,4) -> c(1,3) [98] +(9,5) -> c(1,4) [99] +(9,6) -> c(1,5) [100] +(9,7) -> c(1,6) [101] +(9,8) -> c(1,7) [102] +(9,9) -> c(1,8) [103] +(x,c(y,z)) -> c(y,+(x,z)) [104] +(c(x,y),z) -> c(x,+(y,z)) [105] *(0,0) -> 0 [106] *(0,1) -> 0 [107] *(0,2) -> 0 [108] *(0,3) -> 0 [109] *(0,4) -> 0 [110] *(0,5) -> 0 [111] *(0,6) -> 0 [112] *(0,7) -> 0 [113] *(0,8) -> 0 [114] *(0,9) -> 0 [115] *(1,0) -> 0 [116] *(1,1) -> 1 [117] *(1,2) -> 2 [118] *(1,3) -> 3 [119] *(1,4) -> 4 [120] *(1,5) -> 5 [121] *(1,6) -> 6 [122] *(1,7) -> 7 [123] *(1,8) -> 8 [124] *(1,9) -> 9 [125] *(2,0) -> 0 [126] *(2,1) -> 2 [127] *(2,2) -> 4 [128] *(2,3) -> 6 [129] *(2,4) -> 8 [130] *(2,5) -> c(1,0) [131] *(2,6) -> c(1,2) [132] *(2,7) -> c(1,4) [133] *(2,8) -> c(1,6) [134] *(2,9) -> c(1,8) [135] *(3,0) -> 0 [136] *(3,1) -> 3 [137] *(3,2) -> 6 [138] *(3,3) -> 9 [139] *(3,4) -> c(1,2) [140] *(3,5) -> c(1,5) [141] *(3,6) -> c(1,8) [142] *(3,7) -> c(2,1) [143] *(3,8) -> c(2,4) [144] *(3,9) -> c(2,7) [145] *(4,0) -> 0 [146] *(4,1) -> 4 [147] *(4,2) -> 8 [148] *(4,3) -> c(1,2) [149] *(4,4) -> c(1,6) [150] *(4,5) -> c(2,0) [151] *(4,6) -> c(2,4) [152] *(4,7) -> c(2,8) [153] *(4,8) -> c(3,2) [154] *(4,9) -> c(3,6) [155] *(5,0) -> 0 [156] *(5,1) -> 5 [157] *(5,2) -> c(1,0) [158] *(5,3) -> c(1,5) [159] *(5,4) -> c(2,0) [160] *(5,5) -> c(2,5) [161] *(5,6) -> c(3,0) [162] *(5,7) -> c(3,5) [163] *(5,8) -> c(4,0) [164] *(5,9) -> c(4,5) [165] *(6,0) -> 0 [166] *(6,1) -> 6 [167] *(6,2) -> c(1,2) [168] *(6,3) -> c(1,8) [169] *(6,4) -> c(2,4) [170] *(6,5) -> c(3,0) [171] *(6,6) -> c(3,6) [172] *(6,7) -> c(4,2) [173] *(6,8) -> c(4,8) [174] *(6,9) -> c(5,4) [175] *(7,0) -> 0 [176] *(7,1) -> 7 [177] *(7,2) -> c(1,4) [178] *(7,3) -> c(2,1) [179] *(7,4) -> c(2,8) [180] *(7,5) -> c(3,5) [181] *(7,6) -> c(4,2) [182] *(7,7) -> c(4,9) [183] *(7,8) -> c(5,6) [184] *(7,9) -> c(6,3) [185] *(8,0) -> 0 [186] *(8,1) -> 8 [187] *(8,2) -> c(1,8) [188] *(8,3) -> c(2,4) [189] *(8,4) -> c(3,2) [190] *(8,5) -> c(4,0) [191] *(8,6) -> c(4,8) [192] *(8,7) -> c(5,6) [193] *(8,8) -> c(6,4) [194] *(8,9) -> c(7,2) [195] *(9,0) -> 0 [196] *(9,1) -> 9 [197] *(9,2) -> c(1,8) [198] *(9,3) -> c(2,7) [199] *(9,4) -> c(3,6) [200] *(9,5) -> c(4,5) [201] *(9,6) -> c(5,4) [202] *(9,7) -> c(6,3) [203] *(9,8) -> c(7,2) [204] *(9,9) -> c(8,1) [205] *(x,c(y,z)) -> c( *(x,y), *(x,z)) [206] *(c(x,y),z) -> c( *(x,z), *(y,z)) , 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 [ ]} ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ c ] (X0,X1) = 1*X1 + 1*X0 + 1; [ 6 ] () = 2; [ 2 ] () = 1; [ * ] (X0,X1) = 2*X1*X0 + 1*X1 + 1*X0; [ + ] (X0,X1) = 1*X1 + 1*X0; [ 8 ] () = 2; [ 4 ] () = 2; [ Marked_c ] (X0,X1) = 1*X1 + 1*X0; [ 0 ] () = 1; [ 7 ] () = 2; [ 3 ] () = 1; [ 1 ] () = 1; [ 9 ] () = 2; [ 5 ] () = 2; [ Marked_+ ] (X0,X1) = 1*X1 + 1*X0 + 1; removing [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 2.037725 seconds (real time) Cime Exit Status: 0