- : unit = ()
h : heuristic = <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:
<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_c(x,c(y,z)) , Marked_c(+(x,y),z)>
<Marked_c(x,c(y,z)) , Marked_+(x,y)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <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)>
  <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)>
}
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:

{  <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:
{
  +(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:
     <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_c(x,c(y,z)) , Marked_c(+(x,y),z)>
<Marked_c(x,c(y,z)) , Marked_+(x,y)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <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_c(x,c(y,z)) , Marked_c(+(x,y),z)>
<Marked_c(x,c(y,z)) , Marked_+(x,y)>
 ,
 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 <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_c(x,c(y,z)),Marked_+(x,y)>
 [ {
      
     DP termination of:
     <Marked_c(x,c(y,z)) , Marked_c(+(x,y),z)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_c(x,c(y,z)) , Marked_c(+(x,y),z)>
 ,
 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