- : unit = ()
h : heuristic = <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:
<Marked_c(x,c(y,z)) , Marked_c(+(x,y),z)>
<Marked_c(x,c(y,z)) , Marked_+(x,y)>
<Marked_+(1,9) , Marked_c(1,0)>
<Marked_+(2,8) , Marked_c(1,0)>
<Marked_+(2,9) , Marked_c(1,1)>
<Marked_+(3,7) , Marked_c(1,0)>
<Marked_+(3,8) , Marked_c(1,1)>
<Marked_+(3,9) , Marked_c(1,2)>
<Marked_+(4,6) , Marked_c(1,0)>
<Marked_+(4,7) , Marked_c(1,1)>
<Marked_+(4,8) , Marked_c(1,2)>
<Marked_+(4,9) , Marked_c(1,3)>
<Marked_+(5,5) , Marked_c(1,0)>
<Marked_+(5,6) , Marked_c(1,1)>
<Marked_+(5,7) , Marked_c(1,2)>
<Marked_+(5,8) , Marked_c(1,3)>
<Marked_+(5,9) , Marked_c(1,4)>
<Marked_+(6,4) , Marked_c(1,0)>
<Marked_+(6,5) , Marked_c(1,1)>
<Marked_+(6,6) , Marked_c(1,2)>
<Marked_+(6,7) , Marked_c(1,3)>
<Marked_+(6,8) , Marked_c(1,4)>
<Marked_+(6,9) , Marked_c(1,5)>
<Marked_+(7,3) , Marked_c(1,0)>
<Marked_+(7,4) , Marked_c(1,1)>
<Marked_+(7,5) , Marked_c(1,2)>
<Marked_+(7,6) , Marked_c(1,3)>
<Marked_+(7,7) , Marked_c(1,4)>
<Marked_+(7,8) , Marked_c(1,5)>
<Marked_+(7,9) , Marked_c(1,6)>
<Marked_+(8,2) , Marked_c(1,0)>
<Marked_+(8,3) , Marked_c(1,1)>
<Marked_+(8,4) , Marked_c(1,2)>
<Marked_+(8,5) , Marked_c(1,3)>
<Marked_+(8,6) , Marked_c(1,4)>
<Marked_+(8,7) , Marked_c(1,5)>
<Marked_+(8,8) , Marked_c(1,6)>
<Marked_+(8,9) , Marked_c(1,7)>
<Marked_+(9,1) , Marked_c(1,0)>
<Marked_+(9,2) , Marked_c(1,1)>
<Marked_+(9,3) , Marked_c(1,2)>
<Marked_+(9,4) , Marked_c(1,3)>
<Marked_+(9,5) , Marked_c(1,4)>
<Marked_+(9,6) , Marked_c(1,5)>
<Marked_+(9,7) , Marked_c(1,6)>
<Marked_+(9,8) , Marked_c(1,7)>
<Marked_+(9,9) , Marked_c(1,8)>
<Marked_+(x,c(y,z)) , Marked_c(y,+(x,z))>
<Marked_+(x,c(y,z)) , Marked_+(x,z)>
<Marked_+(c(x,y),z) , Marked_c(x,+(y,z))>
<Marked_+(c(x,y),z) , Marked_+(y,z)>
<Marked_*(2,5) , Marked_c(1,0)>
<Marked_*(2,6) , Marked_c(1,2)>
<Marked_*(2,7) , Marked_c(1,4)>
<Marked_*(2,8) , Marked_c(1,6)>
<Marked_*(2,9) , Marked_c(1,8)>
<Marked_*(3,4) , Marked_c(1,2)>
<Marked_*(3,5) , Marked_c(1,5)>
<Marked_*(3,6) , Marked_c(1,8)>
<Marked_*(3,7) , Marked_c(2,1)>
<Marked_*(3,8) , Marked_c(2,4)>
<Marked_*(3,9) , Marked_c(2,7)>
<Marked_*(4,3) , Marked_c(1,2)>
<Marked_*(4,4) , Marked_c(1,6)>
<Marked_*(4,5) , Marked_c(2,0)>
<Marked_*(4,6) , Marked_c(2,4)>
<Marked_*(4,7) , Marked_c(2,8)>
<Marked_*(4,8) , Marked_c(3,2)>
<Marked_*(4,9) , Marked_c(3,6)>
<Marked_*(5,2) , Marked_c(1,0)>
<Marked_*(5,3) , Marked_c(1,5)>
<Marked_*(5,4) , Marked_c(2,0)>
<Marked_*(5,5) , Marked_c(2,5)>
<Marked_*(5,6) , Marked_c(3,0)>
<Marked_*(5,7) , Marked_c(3,5)>
<Marked_*(5,8) , Marked_c(4,0)>
<Marked_*(5,9) , Marked_c(4,5)>
<Marked_*(6,2) , Marked_c(1,2)>
<Marked_*(6,3) , Marked_c(1,8)>
<Marked_*(6,4) , Marked_c(2,4)>
<Marked_*(6,5) , Marked_c(3,0)>
<Marked_*(6,6) , Marked_c(3,6)>
<Marked_*(6,7) , Marked_c(4,2)>
<Marked_*(6,8) , Marked_c(4,8)>
<Marked_*(6,9) , Marked_c(5,4)>
<Marked_*(7,2) , Marked_c(1,4)>
<Marked_*(7,3) , Marked_c(2,1)>
<Marked_*(7,4) , Marked_c(2,8)>
<Marked_*(7,5) , Marked_c(3,5)>
<Marked_*(7,6) , Marked_c(4,2)>
<Marked_*(7,7) , Marked_c(4,9)>
<Marked_*(7,8) , Marked_c(5,6)>
<Marked_*(7,9) , Marked_c(6,3)>
<Marked_*(8,2) , Marked_c(1,8)>
<Marked_*(8,3) , Marked_c(2,4)>
<Marked_*(8,4) , Marked_c(3,2)>
<Marked_*(8,5) , Marked_c(4,0)>
<Marked_*(8,6) , Marked_c(4,8)>
<Marked_*(8,7) , Marked_c(5,6)>
<Marked_*(8,8) , Marked_c(6,4)>
<Marked_*(8,9) , Marked_c(7,2)>
<Marked_*(9,2) , Marked_c(1,8)>
<Marked_*(9,3) , Marked_c(2,7)>
<Marked_*(9,4) , Marked_c(3,6)>
<Marked_*(9,5) , Marked_c(4,5)>
<Marked_*(9,6) , Marked_c(5,4)>
<Marked_*(9,7) , Marked_c(6,3)>
<Marked_*(9,8) , Marked_c(7,2)>
<Marked_*(9,9) , Marked_c(8,1)>
<Marked_*(x,c(y,z)) , Marked_c( *(x,y), *(x,z))>
<Marked_*(x,c(y,z)) , Marked_*(x,y)>
<Marked_*(x,c(y,z)) , Marked_*(x,z)>
<Marked_*(c(x,y),z) , Marked_c( *(x,z), *(y,z))>
<Marked_*(c(x,y),z) , Marked_*(x,z)>
<Marked_*(c(x,y),z) , Marked_*(y,z)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 2 components:

{  <Marked_*(c(x,y),z) , Marked_*(y,z)> 
      --> <Marked_*(c(x,y),z) , Marked_*(y,z)>
  <Marked_*(c(x,y),z) , Marked_*(y,z)> --> <Marked_*(c(x,y),z) , Marked_*(x,z)>
  <Marked_*(c(x,y),z) , Marked_*(y,z)> --> <Marked_*(x,c(y,z)) , Marked_*(x,z)>
  <Marked_*(c(x,y),z) , Marked_*(y,z)> --> <Marked_*(x,c(y,z)) , Marked_*(x,y)>
  <Marked_*(c(x,y),z) , Marked_*(x,z)> --> <Marked_*(c(x,y),z) , Marked_*(y,z)>
  <Marked_*(c(x,y),z) , Marked_*(x,z)> --> <Marked_*(c(x,y),z) , Marked_*(x,z)>
  <Marked_*(c(x,y),z) , Marked_*(x,z)> --> <Marked_*(x,c(y,z)) , Marked_*(x,z)>
  <Marked_*(c(x,y),z) , Marked_*(x,z)> --> <Marked_*(x,c(y,z)) , Marked_*(x,y)>
  <Marked_*(x,c(y,z)) , Marked_*(x,z)> --> <Marked_*(c(x,y),z) , Marked_*(y,z)>
  <Marked_*(x,c(y,z)) , Marked_*(x,z)> --> <Marked_*(c(x,y),z) , Marked_*(x,z)>
  <Marked_*(x,c(y,z)) , Marked_*(x,z)> --> <Marked_*(x,c(y,z)) , Marked_*(x,z)>
  <Marked_*(x,c(y,z)) , Marked_*(x,z)> --> <Marked_*(x,c(y,z)) , Marked_*(x,y)>
  <Marked_*(x,c(y,z)) , Marked_*(x,y)> --> <Marked_*(c(x,y),z) , Marked_*(y,z)>
  <Marked_*(x,c(y,z)) , Marked_*(x,y)> --> <Marked_*(c(x,y),z) , Marked_*(x,z)>
  <Marked_*(x,c(y,z)) , Marked_*(x,y)> --> <Marked_*(x,c(y,z)) , Marked_*(x,z)>
  <Marked_*(x,c(y,z)) , Marked_*(x,y)> --> <Marked_*(x,c(y,z)) , Marked_*(x,y)>
}

{  <Marked_+(c(x,y),z) , Marked_+(y,z)> 
      --> <Marked_+(c(x,y),z) , Marked_+(y,z)>
  <Marked_+(c(x,y),z) , Marked_+(y,z)> 
     --> <Marked_+(c(x,y),z) , Marked_c(x,+(y,z))>
  <Marked_+(c(x,y),z) , Marked_+(y,z)> --> <Marked_+(x,c(y,z)) , Marked_+(x,z)>
  <Marked_+(c(x,y),z) , Marked_+(y,z)> 
     --> <Marked_+(x,c(y,z)) , Marked_c(y,+(x,z))>
  <Marked_+(c(x,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,c(y,z)) , Marked_c(+(x,y),z)>
  <Marked_+(x,c(y,z)) , Marked_+(x,z)> --> <Marked_+(c(x,y),z) , Marked_+(y,z)>
  <Marked_+(x,c(y,z)) , Marked_+(x,z)> 
     --> <Marked_+(c(x,y),z) , Marked_c(x,+(y,z))>
  <Marked_+(x,c(y,z)) , Marked_+(x,z)> --> <Marked_+(x,c(y,z)) , Marked_+(x,z)>
  <Marked_+(x,c(y,z)) , Marked_+(x,z)> 
     --> <Marked_+(x,c(y,z)) , Marked_c(y,+(x,z))>
  <Marked_+(x,c(y,z)) , Marked_c(y,+(x,z))> 
     --> <Marked_c(x,c(y,z)) , Marked_+(x,y)>
  <Marked_+(x,c(y,z)) , Marked_c(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_+(y,z)>
  <Marked_c(x,c(y,z)) , Marked_+(x,y)> 
     --> <Marked_+(c(x,y),z) , Marked_c(x,+(y,z))>
  <Marked_c(x,c(y,z)) , Marked_+(x,y)> --> <Marked_+(x,c(y,z)) , Marked_+(x,z)>
  <Marked_c(x,c(y,z)) , Marked_+(x,y)> 
     --> <Marked_+(x,c(y,z)) , Marked_c(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,c(y,z)) , Marked_c(+(x,y),z)> 
     --> <Marked_c(x,c(y,z)) , Marked_c(+(x,y),z)>
}
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,y),z) >= Marked_*(x,z) ;
  Marked_*(c(x,y),z) >= Marked_*(y,z) ;
  Marked_*(x,c(y,z)) >= Marked_*(x,y) ;
  Marked_*(x,c(y,z)) >= Marked_*(x,z) ;
 }
 + Disjunctions:{ 
{
  Marked_*(c(x,y),z) > Marked_*(x,z) ;
 }
{
  Marked_*(c(x,y),z) > Marked_*(y,z) ;
 }
{
  Marked_*(x,c(y,z)) > Marked_*(x,y) ;
 }
{
  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 : 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,y),z) >= Marked_*(x,z)
constraint: Marked_*(c(x,y),z) >= Marked_*(y,z)
constraint: Marked_*(x,c(y,z)) >= Marked_*(x,y)
constraint: Marked_*(x,c(y,z)) >= Marked_*(x,z)
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 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:
     <Marked_c(x,c(y,z)) , Marked_c(+(x,y),z)>
<Marked_c(x,c(y,z)) , Marked_+(x,y)>
<Marked_+(1,9) , Marked_c(1,0)>
<Marked_+(2,8) , Marked_c(1,0)>
<Marked_+(2,9) , Marked_c(1,1)>
<Marked_+(3,7) , Marked_c(1,0)>
<Marked_+(3,8) , Marked_c(1,1)>
<Marked_+(3,9) , Marked_c(1,2)>
<Marked_+(4,6) , Marked_c(1,0)>
<Marked_+(4,7) , Marked_c(1,1)>
<Marked_+(4,8) , Marked_c(1,2)>
<Marked_+(4,9) , Marked_c(1,3)>
<Marked_+(5,5) , Marked_c(1,0)>
<Marked_+(5,6) , Marked_c(1,1)>
<Marked_+(5,7) , Marked_c(1,2)>
<Marked_+(5,8) , Marked_c(1,3)>
<Marked_+(5,9) , Marked_c(1,4)>
<Marked_+(6,4) , Marked_c(1,0)>
<Marked_+(6,5) , Marked_c(1,1)>
<Marked_+(6,6) , Marked_c(1,2)>
<Marked_+(6,7) , Marked_c(1,3)>
<Marked_+(6,8) , Marked_c(1,4)>
<Marked_+(6,9) , Marked_c(1,5)>
<Marked_+(7,3) , Marked_c(1,0)>
<Marked_+(7,4) , Marked_c(1,1)>
<Marked_+(7,5) , Marked_c(1,2)>
<Marked_+(7,6) , Marked_c(1,3)>
<Marked_+(7,7) , Marked_c(1,4)>
<Marked_+(7,8) , Marked_c(1,5)>
<Marked_+(7,9) , Marked_c(1,6)>
<Marked_+(8,2) , Marked_c(1,0)>
<Marked_+(8,3) , Marked_c(1,1)>
<Marked_+(8,4) , Marked_c(1,2)>
<Marked_+(8,5) , Marked_c(1,3)>
<Marked_+(8,6) , Marked_c(1,4)>
<Marked_+(8,7) , Marked_c(1,5)>
<Marked_+(8,8) , Marked_c(1,6)>
<Marked_+(8,9) , Marked_c(1,7)>
<Marked_+(9,1) , Marked_c(1,0)>
<Marked_+(9,2) , Marked_c(1,1)>
<Marked_+(9,3) , Marked_c(1,2)>
<Marked_+(9,4) , Marked_c(1,3)>
<Marked_+(9,5) , Marked_c(1,4)>
<Marked_+(9,6) , Marked_c(1,5)>
<Marked_+(9,7) , Marked_c(1,6)>
<Marked_+(9,8) , Marked_c(1,7)>
<Marked_+(9,9) , Marked_c(1,8)>
<Marked_+(x,c(y,z)) , Marked_c(y,+(x,z))>
<Marked_+(x,c(y,z)) , Marked_+(x,z)>
<Marked_+(c(x,y),z) , Marked_c(x,+(y,z))>
<Marked_+(c(x,y),z) , Marked_+(y,z)>
<Marked_*(2,5) , Marked_c(1,0)>
<Marked_*(2,6) , Marked_c(1,2)>
<Marked_*(2,7) , Marked_c(1,4)>
<Marked_*(2,8) , Marked_c(1,6)>
<Marked_*(2,9) , Marked_c(1,8)>
<Marked_*(3,4) , Marked_c(1,2)>
<Marked_*(3,5) , Marked_c(1,5)>
<Marked_*(3,6) , Marked_c(1,8)>
<Marked_*(3,7) , Marked_c(2,1)>
<Marked_*(3,8) , Marked_c(2,4)>
<Marked_*(3,9) , Marked_c(2,7)>
<Marked_*(4,3) , Marked_c(1,2)>
<Marked_*(4,4) , Marked_c(1,6)>
<Marked_*(4,5) , Marked_c(2,0)>
<Marked_*(4,6) , Marked_c(2,4)>
<Marked_*(4,7) , Marked_c(2,8)>
<Marked_*(4,8) , Marked_c(3,2)>
<Marked_*(4,9) , Marked_c(3,6)>
<Marked_*(5,2) , Marked_c(1,0)>
<Marked_*(5,3) , Marked_c(1,5)>
<Marked_*(5,4) , Marked_c(2,0)>
<Marked_*(5,5) , Marked_c(2,5)>
<Marked_*(5,6) , Marked_c(3,0)>
<Marked_*(5,7) , Marked_c(3,5)>
<Marked_*(5,8) , Marked_c(4,0)>
<Marked_*(5,9) , Marked_c(4,5)>
<Marked_*(6,2) , Marked_c(1,2)>
<Marked_*(6,3) , Marked_c(1,8)>
<Marked_*(6,4) , Marked_c(2,4)>
<Marked_*(6,5) , Marked_c(3,0)>
<Marked_*(6,6) , Marked_c(3,6)>
<Marked_*(6,7) , Marked_c(4,2)>
<Marked_*(6,8) , Marked_c(4,8)>
<Marked_*(6,9) , Marked_c(5,4)>
<Marked_*(7,2) , Marked_c(1,4)>
<Marked_*(7,3) , Marked_c(2,1)>
<Marked_*(7,4) , Marked_c(2,8)>
<Marked_*(7,5) , Marked_c(3,5)>
<Marked_*(7,6) , Marked_c(4,2)>
<Marked_*(7,7) , Marked_c(4,9)>
<Marked_*(7,8) , Marked_c(5,6)>
<Marked_*(7,9) , Marked_c(6,3)>
<Marked_*(8,2) , Marked_c(1,8)>
<Marked_*(8,3) , Marked_c(2,4)>
<Marked_*(8,4) , Marked_c(3,2)>
<Marked_*(8,5) , Marked_c(4,0)>
<Marked_*(8,6) , Marked_c(4,8)>
<Marked_*(8,7) , Marked_c(5,6)>
<Marked_*(8,8) , Marked_c(6,4)>
<Marked_*(8,9) , Marked_c(7,2)>
<Marked_*(9,2) , Marked_c(1,8)>
<Marked_*(9,3) , Marked_c(2,7)>
<Marked_*(9,4) , Marked_c(3,6)>
<Marked_*(9,5) , Marked_c(4,5)>
<Marked_*(9,6) , Marked_c(5,4)>
<Marked_*(9,7) , Marked_c(6,3)>
<Marked_*(9,8) , Marked_c(7,2)>
<Marked_*(9,9) , Marked_c(8,1)>
<Marked_*(x,c(y,z)) , Marked_c( *(x,y), *(x,z))>
<Marked_*(x,c(y,z)) , Marked_*(x,y)>
<Marked_*(x,c(y,z)) , Marked_*(x,z)>
<Marked_*(c(x,y),z) , Marked_c( *(x,z), *(y,z))>
<Marked_*(c(x,y),z) , Marked_*(x,z)>
<Marked_*(c(x,y),z) , Marked_*(y,z)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_*(x,c(y,z)) , Marked_*(x,y)>
<Marked_*(x,c(y,z)) , Marked_*(x,z)>
<Marked_*(c(x,y),z) , Marked_*(x,z)>
<Marked_*(c(x,y),z) , Marked_*(y,z)>
 ,
 CRITERION: ORD
 [ 
     Solution found:
     polynomial interpretation = 
      [ c ] (X0,X1) = 2 + 1*X0 + 1*X1 + 0; 
 [ 6 ] () = 1 + 0; 
 [ 2 ] () = 1 + 0; 
 [ * ] (X0,X1) = 2*X0 + 2*X1 + 2*X1*X0 + 0; 
 [ + ] (X0,X1) = 2 + 1*X0 + 1*X1 + 0; 
 [ 8 ] () = 1 + 0; 
 [ 4 ] () = 2 + 0; 
 [ 0 ] () = 1 + 0; 
 [ 7 ] () = 1 + 0; 
 [ 3 ] () = 1 + 0; 
 [ Marked_* ] (X0,X1) = 2*X0 + 2*X1 + 2*X1*X0 + 0; 
 [ 1 ] () = 0; 
 [ 9 ] () = 1 + 0; 
 [ 5 ] () = 2 + 0; 
 ]} 
{
 
DP termination of:
<Marked_c(x,c(y,z)) , Marked_c(+(x,y),z)>
<Marked_c(x,c(y,z)) , Marked_+(x,y)>
<Marked_+(x,c(y,z)) , Marked_c(y,+(x,z))>
<Marked_+(x,c(y,z)) , Marked_+(x,z)>
<Marked_+(c(x,y),z) , Marked_c(x,+(y,z))>
<Marked_+(c(x,y),z) , Marked_+(y,z)>
 ,
 CRITERION: ORD
 [ 
     Solution found:
     polynomial interpretation = 
      [ c ] (X0,X1) = 2 + 2*X0 + 1*X1 + 0; 
 [ 6 ] () = 2 + 0; 
 [ 2 ] () = 1 + 0; 
 [ * ] (X0,X1) = 1*X0 + 1*X1 + 2*X1*X0 + 0; 
 [ + ] (X0,X1) = 1 + 1*X0 + 1*X1 + 0; 
 [ 8 ] () = 2 + 0; 
 [ 4 ] () = 1 + 0; 
 [ Marked_c ] (X0,X1) = 1 + 2*X0 + 2*X1 + 0; 
 [ 0 ] () = 0; 
 [ 7 ] () = 2 + 0; 
 [ 3 ] () = 1 + 0; 
 [ 1 ] () = 0; 
 [ 9 ] () = 2 + 0; 
 [ 5 ] () = 2 + 0; 
 [ Marked_+ ] (X0,X1) = 2*X0 + 2*X1 + 0; 
 ]} 
 ]} 
 ]} 

Cime worked for 4.116819 seconds (real time)
Cime Exit Status: 0