MAYBE

Problem:
 +(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,+(y,z))
 c(0(),x) -> x
 c(x,c(y,z)) -> c(+(x,y),z)

Proof:
 RT Transformation Processor:
  strict:
   +(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,+(y,z))
   c(0(),x) -> x
   c(x,c(y,z)) -> c(+(x,y),z)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [c](x0, x1) = x0 + x1 + 24,
    
    [9] = 25,
    
    [8] = 25,
    
    [7] = 12,
    
    [6] = 11,
    
    [5] = 22,
    
    [4] = 2,
    
    [3] = 17,
    
    [2] = 24,
    
    [1] = 8,
    
    [+](x0, x1) = x0 + x1 + 8,
    
    [0] = 2
   orientation:
    +(0(),0()) = 12 >= 2 = 0()
    
    +(0(),1()) = 18 >= 8 = 1()
    
    +(0(),2()) = 34 >= 24 = 2()
    
    +(0(),3()) = 27 >= 17 = 3()
    
    +(0(),4()) = 12 >= 2 = 4()
    
    +(0(),5()) = 32 >= 22 = 5()
    
    +(0(),6()) = 21 >= 11 = 6()
    
    +(0(),7()) = 22 >= 12 = 7()
    
    +(0(),8()) = 35 >= 25 = 8()
    
    +(0(),9()) = 35 >= 25 = 9()
    
    +(1(),0()) = 18 >= 8 = 1()
    
    +(1(),1()) = 24 >= 24 = 2()
    
    +(1(),2()) = 40 >= 17 = 3()
    
    +(1(),3()) = 33 >= 2 = 4()
    
    +(1(),4()) = 18 >= 22 = 5()
    
    +(1(),5()) = 38 >= 11 = 6()
    
    +(1(),6()) = 27 >= 12 = 7()
    
    +(1(),7()) = 28 >= 25 = 8()
    
    +(1(),8()) = 41 >= 25 = 9()
    
    +(1(),9()) = 41 >= 34 = c(1(),0())
    
    +(2(),0()) = 34 >= 24 = 2()
    
    +(2(),1()) = 40 >= 17 = 3()
    
    +(2(),2()) = 56 >= 2 = 4()
    
    +(2(),3()) = 49 >= 22 = 5()
    
    +(2(),4()) = 34 >= 11 = 6()
    
    +(2(),5()) = 54 >= 12 = 7()
    
    +(2(),6()) = 43 >= 25 = 8()
    
    +(2(),7()) = 44 >= 25 = 9()
    
    +(2(),8()) = 57 >= 34 = c(1(),0())
    
    +(2(),9()) = 57 >= 40 = c(1(),1())
    
    +(3(),0()) = 27 >= 17 = 3()
    
    +(3(),1()) = 33 >= 2 = 4()
    
    +(3(),2()) = 49 >= 22 = 5()
    
    +(3(),3()) = 42 >= 11 = 6()
    
    +(3(),4()) = 27 >= 12 = 7()
    
    +(3(),5()) = 47 >= 25 = 8()
    
    +(3(),6()) = 36 >= 25 = 9()
    
    +(3(),7()) = 37 >= 34 = c(1(),0())
    
    +(3(),8()) = 50 >= 40 = c(1(),1())
    
    +(3(),9()) = 50 >= 56 = c(1(),2())
    
    +(4(),0()) = 12 >= 2 = 4()
    
    +(4(),1()) = 18 >= 22 = 5()
    
    +(4(),2()) = 34 >= 11 = 6()
    
    +(4(),3()) = 27 >= 12 = 7()
    
    +(4(),4()) = 12 >= 25 = 8()
    
    +(4(),5()) = 32 >= 25 = 9()
    
    +(4(),6()) = 21 >= 34 = c(1(),0())
    
    +(4(),7()) = 22 >= 40 = c(1(),1())
    
    +(4(),8()) = 35 >= 56 = c(1(),2())
    
    +(4(),9()) = 35 >= 49 = c(1(),3())
    
    +(5(),0()) = 32 >= 22 = 5()
    
    +(5(),1()) = 38 >= 11 = 6()
    
    +(5(),2()) = 54 >= 12 = 7()
    
    +(5(),3()) = 47 >= 25 = 8()
    
    +(5(),4()) = 32 >= 25 = 9()
    
    +(5(),5()) = 52 >= 34 = c(1(),0())
    
    +(5(),6()) = 41 >= 40 = c(1(),1())
    
    +(5(),7()) = 42 >= 56 = c(1(),2())
    
    +(5(),8()) = 55 >= 49 = c(1(),3())
    
    +(5(),9()) = 55 >= 34 = c(1(),4())
    
    +(6(),0()) = 21 >= 11 = 6()
    
    +(6(),1()) = 27 >= 12 = 7()
    
    +(6(),2()) = 43 >= 25 = 8()
    
    +(6(),3()) = 36 >= 25 = 9()
    
    +(6(),4()) = 21 >= 34 = c(1(),0())
    
    +(6(),5()) = 41 >= 40 = c(1(),1())
    
    +(6(),6()) = 30 >= 56 = c(1(),2())
    
    +(6(),7()) = 31 >= 49 = c(1(),3())
    
    +(6(),8()) = 44 >= 34 = c(1(),4())
    
    +(6(),9()) = 44 >= 54 = c(1(),5())
    
    +(7(),0()) = 22 >= 12 = 7()
    
    +(7(),1()) = 28 >= 25 = 8()
    
    +(7(),2()) = 44 >= 25 = 9()
    
    +(7(),3()) = 37 >= 34 = c(1(),0())
    
    +(7(),4()) = 22 >= 40 = c(1(),1())
    
    +(7(),5()) = 42 >= 56 = c(1(),2())
    
    +(7(),6()) = 31 >= 49 = c(1(),3())
    
    +(7(),7()) = 32 >= 34 = c(1(),4())
    
    +(7(),8()) = 45 >= 54 = c(1(),5())
    
    +(7(),9()) = 45 >= 43 = c(1(),6())
    
    +(8(),0()) = 35 >= 25 = 8()
    
    +(8(),1()) = 41 >= 25 = 9()
    
    +(8(),2()) = 57 >= 34 = c(1(),0())
    
    +(8(),3()) = 50 >= 40 = c(1(),1())
    
    +(8(),4()) = 35 >= 56 = c(1(),2())
    
    +(8(),5()) = 55 >= 49 = c(1(),3())
    
    +(8(),6()) = 44 >= 34 = c(1(),4())
    
    +(8(),7()) = 45 >= 54 = c(1(),5())
    
    +(8(),8()) = 58 >= 43 = c(1(),6())
    
    +(8(),9()) = 58 >= 44 = c(1(),7())
    
    +(9(),0()) = 35 >= 25 = 9()
    
    +(9(),1()) = 41 >= 34 = c(1(),0())
    
    +(9(),2()) = 57 >= 40 = c(1(),1())
    
    +(9(),3()) = 50 >= 56 = c(1(),2())
    
    +(9(),4()) = 35 >= 49 = c(1(),3())
    
    +(9(),5()) = 55 >= 34 = c(1(),4())
    
    +(9(),6()) = 44 >= 54 = c(1(),5())
    
    +(9(),7()) = 45 >= 43 = c(1(),6())
    
    +(9(),8()) = 58 >= 44 = c(1(),7())
    
    +(9(),9()) = 58 >= 57 = c(1(),8())
    
    +(x,c(y,z)) = x + y + z + 32 >= x + y + z + 32 = c(y,+(x,z))
    
    +(c(x,y),z) = x + y + z + 32 >= x + y + z + 32 = c(x,+(y,z))
    
    c(0(),x) = x + 26 >= x = x
    
    c(x,c(y,z)) = x + y + z + 48 >= x + y + z + 32 = c(+(x,y),z)
   problem:
    strict:
     +(1(),1()) -> 2()
     +(1(),4()) -> 5()
     +(3(),9()) -> c(1(),2())
     +(4(),1()) -> 5()
     +(4(),4()) -> 8()
     +(4(),6()) -> c(1(),0())
     +(4(),7()) -> c(1(),1())
     +(4(),8()) -> c(1(),2())
     +(4(),9()) -> c(1(),3())
     +(5(),7()) -> c(1(),2())
     +(6(),4()) -> c(1(),0())
     +(6(),6()) -> c(1(),2())
     +(6(),7()) -> c(1(),3())
     +(6(),9()) -> c(1(),5())
     +(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())
     +(8(),4()) -> c(1(),2())
     +(8(),7()) -> c(1(),5())
     +(9(),3()) -> c(1(),2())
     +(9(),4()) -> c(1(),3())
     +(9(),6()) -> c(1(),5())
     +(x,c(y,z)) -> c(y,+(x,z))
     +(c(x,y),z) -> c(x,+(y,z))
    weak:
     +(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(),2()) -> 3()
     +(1(),3()) -> 4()
     +(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())
     +(4(),0()) -> 4()
     +(4(),2()) -> 6()
     +(4(),3()) -> 7()
     +(4(),5()) -> 9()
     +(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(),8()) -> c(1(),3())
     +(5(),9()) -> c(1(),4())
     +(6(),0()) -> 6()
     +(6(),1()) -> 7()
     +(6(),2()) -> 8()
     +(6(),3()) -> 9()
     +(6(),5()) -> c(1(),1())
     +(6(),8()) -> c(1(),4())
     +(7(),0()) -> 7()
     +(7(),1()) -> 8()
     +(7(),2()) -> 9()
     +(7(),3()) -> c(1(),0())
     +(7(),9()) -> c(1(),6())
     +(8(),0()) -> 8()
     +(8(),1()) -> 9()
     +(8(),2()) -> c(1(),0())
     +(8(),3()) -> c(1(),1())
     +(8(),5()) -> c(1(),3())
     +(8(),6()) -> c(1(),4())
     +(8(),8()) -> c(1(),6())
     +(8(),9()) -> c(1(),7())
     +(9(),0()) -> 9()
     +(9(),1()) -> c(1(),0())
     +(9(),2()) -> c(1(),1())
     +(9(),5()) -> c(1(),4())
     +(9(),7()) -> c(1(),6())
     +(9(),8()) -> c(1(),7())
     +(9(),9()) -> c(1(),8())
     c(0(),x) -> x
     c(x,c(y,z)) -> c(+(x,y),z)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [c](x0, x1) = x0 + x1,
     
     [9] = 5,
     
     [8] = 6,
     
     [7] = 4,
     
     [6] = 7,
     
     [5] = 5,
     
     [4] = 1,
     
     [3] = 6,
     
     [2] = 16,
     
     [1] = 2,
     
     [+](x0, x1) = x0 + x1,
     
     [0] = 0
    orientation:
     +(1(),1()) = 4 >= 16 = 2()
     
     +(1(),4()) = 3 >= 5 = 5()
     
     +(3(),9()) = 11 >= 18 = c(1(),2())
     
     +(4(),1()) = 3 >= 5 = 5()
     
     +(4(),4()) = 2 >= 6 = 8()
     
     +(4(),6()) = 8 >= 2 = c(1(),0())
     
     +(4(),7()) = 5 >= 4 = c(1(),1())
     
     +(4(),8()) = 7 >= 18 = c(1(),2())
     
     +(4(),9()) = 6 >= 8 = c(1(),3())
     
     +(5(),7()) = 9 >= 18 = c(1(),2())
     
     +(6(),4()) = 8 >= 2 = c(1(),0())
     
     +(6(),6()) = 14 >= 18 = c(1(),2())
     
     +(6(),7()) = 11 >= 8 = c(1(),3())
     
     +(6(),9()) = 12 >= 7 = c(1(),5())
     
     +(7(),4()) = 5 >= 4 = c(1(),1())
     
     +(7(),5()) = 9 >= 18 = c(1(),2())
     
     +(7(),6()) = 11 >= 8 = c(1(),3())
     
     +(7(),7()) = 8 >= 3 = c(1(),4())
     
     +(7(),8()) = 10 >= 7 = c(1(),5())
     
     +(8(),4()) = 7 >= 18 = c(1(),2())
     
     +(8(),7()) = 10 >= 7 = c(1(),5())
     
     +(9(),3()) = 11 >= 18 = c(1(),2())
     
     +(9(),4()) = 6 >= 8 = c(1(),3())
     
     +(9(),6()) = 12 >= 7 = c(1(),5())
     
     +(x,c(y,z)) = x + y + z >= x + y + z = c(y,+(x,z))
     
     +(c(x,y),z) = x + y + z >= x + y + z = c(x,+(y,z))
     
     +(0(),0()) = 0 >= 0 = 0()
     
     +(0(),1()) = 2 >= 2 = 1()
     
     +(0(),2()) = 16 >= 16 = 2()
     
     +(0(),3()) = 6 >= 6 = 3()
     
     +(0(),4()) = 1 >= 1 = 4()
     
     +(0(),5()) = 5 >= 5 = 5()
     
     +(0(),6()) = 7 >= 7 = 6()
     
     +(0(),7()) = 4 >= 4 = 7()
     
     +(0(),8()) = 6 >= 6 = 8()
     
     +(0(),9()) = 5 >= 5 = 9()
     
     +(1(),0()) = 2 >= 2 = 1()
     
     +(1(),2()) = 18 >= 6 = 3()
     
     +(1(),3()) = 8 >= 1 = 4()
     
     +(1(),5()) = 7 >= 7 = 6()
     
     +(1(),6()) = 9 >= 4 = 7()
     
     +(1(),7()) = 6 >= 6 = 8()
     
     +(1(),8()) = 8 >= 5 = 9()
     
     +(1(),9()) = 7 >= 2 = c(1(),0())
     
     +(2(),0()) = 16 >= 16 = 2()
     
     +(2(),1()) = 18 >= 6 = 3()
     
     +(2(),2()) = 32 >= 1 = 4()
     
     +(2(),3()) = 22 >= 5 = 5()
     
     +(2(),4()) = 17 >= 7 = 6()
     
     +(2(),5()) = 21 >= 4 = 7()
     
     +(2(),6()) = 23 >= 6 = 8()
     
     +(2(),7()) = 20 >= 5 = 9()
     
     +(2(),8()) = 22 >= 2 = c(1(),0())
     
     +(2(),9()) = 21 >= 4 = c(1(),1())
     
     +(3(),0()) = 6 >= 6 = 3()
     
     +(3(),1()) = 8 >= 1 = 4()
     
     +(3(),2()) = 22 >= 5 = 5()
     
     +(3(),3()) = 12 >= 7 = 6()
     
     +(3(),4()) = 7 >= 4 = 7()
     
     +(3(),5()) = 11 >= 6 = 8()
     
     +(3(),6()) = 13 >= 5 = 9()
     
     +(3(),7()) = 10 >= 2 = c(1(),0())
     
     +(3(),8()) = 12 >= 4 = c(1(),1())
     
     +(4(),0()) = 1 >= 1 = 4()
     
     +(4(),2()) = 17 >= 7 = 6()
     
     +(4(),3()) = 7 >= 4 = 7()
     
     +(4(),5()) = 6 >= 5 = 9()
     
     +(5(),0()) = 5 >= 5 = 5()
     
     +(5(),1()) = 7 >= 7 = 6()
     
     +(5(),2()) = 21 >= 4 = 7()
     
     +(5(),3()) = 11 >= 6 = 8()
     
     +(5(),4()) = 6 >= 5 = 9()
     
     +(5(),5()) = 10 >= 2 = c(1(),0())
     
     +(5(),6()) = 12 >= 4 = c(1(),1())
     
     +(5(),8()) = 11 >= 8 = c(1(),3())
     
     +(5(),9()) = 10 >= 3 = c(1(),4())
     
     +(6(),0()) = 7 >= 7 = 6()
     
     +(6(),1()) = 9 >= 4 = 7()
     
     +(6(),2()) = 23 >= 6 = 8()
     
     +(6(),3()) = 13 >= 5 = 9()
     
     +(6(),5()) = 12 >= 4 = c(1(),1())
     
     +(6(),8()) = 13 >= 3 = c(1(),4())
     
     +(7(),0()) = 4 >= 4 = 7()
     
     +(7(),1()) = 6 >= 6 = 8()
     
     +(7(),2()) = 20 >= 5 = 9()
     
     +(7(),3()) = 10 >= 2 = c(1(),0())
     
     +(7(),9()) = 9 >= 9 = c(1(),6())
     
     +(8(),0()) = 6 >= 6 = 8()
     
     +(8(),1()) = 8 >= 5 = 9()
     
     +(8(),2()) = 22 >= 2 = c(1(),0())
     
     +(8(),3()) = 12 >= 4 = c(1(),1())
     
     +(8(),5()) = 11 >= 8 = c(1(),3())
     
     +(8(),6()) = 13 >= 3 = c(1(),4())
     
     +(8(),8()) = 12 >= 9 = c(1(),6())
     
     +(8(),9()) = 11 >= 6 = c(1(),7())
     
     +(9(),0()) = 5 >= 5 = 9()
     
     +(9(),1()) = 7 >= 2 = c(1(),0())
     
     +(9(),2()) = 21 >= 4 = c(1(),1())
     
     +(9(),5()) = 10 >= 3 = c(1(),4())
     
     +(9(),7()) = 9 >= 9 = c(1(),6())
     
     +(9(),8()) = 11 >= 6 = c(1(),7())
     
     +(9(),9()) = 10 >= 8 = c(1(),8())
     
     c(0(),x) = x >= x = x
     
     c(x,c(y,z)) = x + y + z >= x + y + z = c(+(x,y),z)
    problem:
     strict:
      +(1(),1()) -> 2()
      +(1(),4()) -> 5()
      +(3(),9()) -> c(1(),2())
      +(4(),1()) -> 5()
      +(4(),4()) -> 8()
      +(4(),8()) -> c(1(),2())
      +(4(),9()) -> c(1(),3())
      +(5(),7()) -> c(1(),2())
      +(6(),6()) -> c(1(),2())
      +(7(),5()) -> c(1(),2())
      +(8(),4()) -> c(1(),2())
      +(9(),3()) -> c(1(),2())
      +(9(),4()) -> c(1(),3())
      +(x,c(y,z)) -> c(y,+(x,z))
      +(c(x,y),z) -> c(x,+(y,z))
     weak:
      +(4(),6()) -> c(1(),0())
      +(4(),7()) -> c(1(),1())
      +(6(),4()) -> c(1(),0())
      +(6(),7()) -> c(1(),3())
      +(6(),9()) -> c(1(),5())
      +(7(),4()) -> c(1(),1())
      +(7(),6()) -> c(1(),3())
      +(7(),7()) -> c(1(),4())
      +(7(),8()) -> c(1(),5())
      +(8(),7()) -> c(1(),5())
      +(9(),6()) -> c(1(),5())
      +(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(),2()) -> 3()
      +(1(),3()) -> 4()
      +(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())
      +(4(),0()) -> 4()
      +(4(),2()) -> 6()
      +(4(),3()) -> 7()
      +(4(),5()) -> 9()
      +(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(),8()) -> c(1(),3())
      +(5(),9()) -> c(1(),4())
      +(6(),0()) -> 6()
      +(6(),1()) -> 7()
      +(6(),2()) -> 8()
      +(6(),3()) -> 9()
      +(6(),5()) -> c(1(),1())
      +(6(),8()) -> c(1(),4())
      +(7(),0()) -> 7()
      +(7(),1()) -> 8()
      +(7(),2()) -> 9()
      +(7(),3()) -> c(1(),0())
      +(7(),9()) -> c(1(),6())
      +(8(),0()) -> 8()
      +(8(),1()) -> 9()
      +(8(),2()) -> c(1(),0())
      +(8(),3()) -> c(1(),1())
      +(8(),5()) -> c(1(),3())
      +(8(),6()) -> c(1(),4())
      +(8(),8()) -> c(1(),6())
      +(8(),9()) -> c(1(),7())
      +(9(),0()) -> 9()
      +(9(),1()) -> c(1(),0())
      +(9(),2()) -> c(1(),1())
      +(9(),5()) -> c(1(),4())
      +(9(),7()) -> c(1(),6())
      +(9(),8()) -> c(1(),7())
      +(9(),9()) -> c(1(),8())
      c(0(),x) -> x
      c(x,c(y,z)) -> c(+(x,y),z)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [c](x0, x1) = x0 + x1 + 24,
      
      [9] = 19,
      
      [8] = 8,
      
      [7] = 3,
      
      [6] = 12,
      
      [5] = 4,
      
      [4] = 0,
      
      [3] = 10,
      
      [2] = 2,
      
      [1] = 1,
      
      [+](x0, x1) = x0 + x1 + 24,
      
      [0] = 7
     orientation:
      +(1(),1()) = 26 >= 2 = 2()
      
      +(1(),4()) = 25 >= 4 = 5()
      
      +(3(),9()) = 53 >= 27 = c(1(),2())
      
      +(4(),1()) = 25 >= 4 = 5()
      
      +(4(),4()) = 24 >= 8 = 8()
      
      +(4(),8()) = 32 >= 27 = c(1(),2())
      
      +(4(),9()) = 43 >= 35 = c(1(),3())
      
      +(5(),7()) = 31 >= 27 = c(1(),2())
      
      +(6(),6()) = 48 >= 27 = c(1(),2())
      
      +(7(),5()) = 31 >= 27 = c(1(),2())
      
      +(8(),4()) = 32 >= 27 = c(1(),2())
      
      +(9(),3()) = 53 >= 27 = c(1(),2())
      
      +(9(),4()) = 43 >= 35 = c(1(),3())
      
      +(x,c(y,z)) = x + y + z + 48 >= x + y + z + 48 = c(y,+(x,z))
      
      +(c(x,y),z) = x + y + z + 48 >= x + y + z + 48 = c(x,+(y,z))
      
      +(4(),6()) = 36 >= 32 = c(1(),0())
      
      +(4(),7()) = 27 >= 26 = c(1(),1())
      
      +(6(),4()) = 36 >= 32 = c(1(),0())
      
      +(6(),7()) = 39 >= 35 = c(1(),3())
      
      +(6(),9()) = 55 >= 29 = c(1(),5())
      
      +(7(),4()) = 27 >= 26 = c(1(),1())
      
      +(7(),6()) = 39 >= 35 = c(1(),3())
      
      +(7(),7()) = 30 >= 25 = c(1(),4())
      
      +(7(),8()) = 35 >= 29 = c(1(),5())
      
      +(8(),7()) = 35 >= 29 = c(1(),5())
      
      +(9(),6()) = 55 >= 29 = c(1(),5())
      
      +(0(),0()) = 38 >= 7 = 0()
      
      +(0(),1()) = 32 >= 1 = 1()
      
      +(0(),2()) = 33 >= 2 = 2()
      
      +(0(),3()) = 41 >= 10 = 3()
      
      +(0(),4()) = 31 >= 0 = 4()
      
      +(0(),5()) = 35 >= 4 = 5()
      
      +(0(),6()) = 43 >= 12 = 6()
      
      +(0(),7()) = 34 >= 3 = 7()
      
      +(0(),8()) = 39 >= 8 = 8()
      
      +(0(),9()) = 50 >= 19 = 9()
      
      +(1(),0()) = 32 >= 1 = 1()
      
      +(1(),2()) = 27 >= 10 = 3()
      
      +(1(),3()) = 35 >= 0 = 4()
      
      +(1(),5()) = 29 >= 12 = 6()
      
      +(1(),6()) = 37 >= 3 = 7()
      
      +(1(),7()) = 28 >= 8 = 8()
      
      +(1(),8()) = 33 >= 19 = 9()
      
      +(1(),9()) = 44 >= 32 = c(1(),0())
      
      +(2(),0()) = 33 >= 2 = 2()
      
      +(2(),1()) = 27 >= 10 = 3()
      
      +(2(),2()) = 28 >= 0 = 4()
      
      +(2(),3()) = 36 >= 4 = 5()
      
      +(2(),4()) = 26 >= 12 = 6()
      
      +(2(),5()) = 30 >= 3 = 7()
      
      +(2(),6()) = 38 >= 8 = 8()
      
      +(2(),7()) = 29 >= 19 = 9()
      
      +(2(),8()) = 34 >= 32 = c(1(),0())
      
      +(2(),9()) = 45 >= 26 = c(1(),1())
      
      +(3(),0()) = 41 >= 10 = 3()
      
      +(3(),1()) = 35 >= 0 = 4()
      
      +(3(),2()) = 36 >= 4 = 5()
      
      +(3(),3()) = 44 >= 12 = 6()
      
      +(3(),4()) = 34 >= 3 = 7()
      
      +(3(),5()) = 38 >= 8 = 8()
      
      +(3(),6()) = 46 >= 19 = 9()
      
      +(3(),7()) = 37 >= 32 = c(1(),0())
      
      +(3(),8()) = 42 >= 26 = c(1(),1())
      
      +(4(),0()) = 31 >= 0 = 4()
      
      +(4(),2()) = 26 >= 12 = 6()
      
      +(4(),3()) = 34 >= 3 = 7()
      
      +(4(),5()) = 28 >= 19 = 9()
      
      +(5(),0()) = 35 >= 4 = 5()
      
      +(5(),1()) = 29 >= 12 = 6()
      
      +(5(),2()) = 30 >= 3 = 7()
      
      +(5(),3()) = 38 >= 8 = 8()
      
      +(5(),4()) = 28 >= 19 = 9()
      
      +(5(),5()) = 32 >= 32 = c(1(),0())
      
      +(5(),6()) = 40 >= 26 = c(1(),1())
      
      +(5(),8()) = 36 >= 35 = c(1(),3())
      
      +(5(),9()) = 47 >= 25 = c(1(),4())
      
      +(6(),0()) = 43 >= 12 = 6()
      
      +(6(),1()) = 37 >= 3 = 7()
      
      +(6(),2()) = 38 >= 8 = 8()
      
      +(6(),3()) = 46 >= 19 = 9()
      
      +(6(),5()) = 40 >= 26 = c(1(),1())
      
      +(6(),8()) = 44 >= 25 = c(1(),4())
      
      +(7(),0()) = 34 >= 3 = 7()
      
      +(7(),1()) = 28 >= 8 = 8()
      
      +(7(),2()) = 29 >= 19 = 9()
      
      +(7(),3()) = 37 >= 32 = c(1(),0())
      
      +(7(),9()) = 46 >= 37 = c(1(),6())
      
      +(8(),0()) = 39 >= 8 = 8()
      
      +(8(),1()) = 33 >= 19 = 9()
      
      +(8(),2()) = 34 >= 32 = c(1(),0())
      
      +(8(),3()) = 42 >= 26 = c(1(),1())
      
      +(8(),5()) = 36 >= 35 = c(1(),3())
      
      +(8(),6()) = 44 >= 25 = c(1(),4())
      
      +(8(),8()) = 40 >= 37 = c(1(),6())
      
      +(8(),9()) = 51 >= 28 = c(1(),7())
      
      +(9(),0()) = 50 >= 19 = 9()
      
      +(9(),1()) = 44 >= 32 = c(1(),0())
      
      +(9(),2()) = 45 >= 26 = c(1(),1())
      
      +(9(),5()) = 47 >= 25 = c(1(),4())
      
      +(9(),7()) = 46 >= 37 = c(1(),6())
      
      +(9(),8()) = 51 >= 28 = c(1(),7())
      
      +(9(),9()) = 62 >= 33 = c(1(),8())
      
      c(0(),x) = x + 31 >= x = x
      
      c(x,c(y,z)) = x + y + z + 48 >= x + y + z + 48 = c(+(x,y),z)
     problem:
      strict:
       +(x,c(y,z)) -> c(y,+(x,z))
       +(c(x,y),z) -> c(x,+(y,z))
      weak:
       +(1(),1()) -> 2()
       +(1(),4()) -> 5()
       +(3(),9()) -> c(1(),2())
       +(4(),1()) -> 5()
       +(4(),4()) -> 8()
       +(4(),8()) -> c(1(),2())
       +(4(),9()) -> c(1(),3())
       +(5(),7()) -> c(1(),2())
       +(6(),6()) -> c(1(),2())
       +(7(),5()) -> c(1(),2())
       +(8(),4()) -> c(1(),2())
       +(9(),3()) -> c(1(),2())
       +(9(),4()) -> c(1(),3())
       +(4(),6()) -> c(1(),0())
       +(4(),7()) -> c(1(),1())
       +(6(),4()) -> c(1(),0())
       +(6(),7()) -> c(1(),3())
       +(6(),9()) -> c(1(),5())
       +(7(),4()) -> c(1(),1())
       +(7(),6()) -> c(1(),3())
       +(7(),7()) -> c(1(),4())
       +(7(),8()) -> c(1(),5())
       +(8(),7()) -> c(1(),5())
       +(9(),6()) -> c(1(),5())
       +(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(),2()) -> 3()
       +(1(),3()) -> 4()
       +(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())
       +(4(),0()) -> 4()
       +(4(),2()) -> 6()
       +(4(),3()) -> 7()
       +(4(),5()) -> 9()
       +(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(),8()) -> c(1(),3())
       +(5(),9()) -> c(1(),4())
       +(6(),0()) -> 6()
       +(6(),1()) -> 7()
       +(6(),2()) -> 8()
       +(6(),3()) -> 9()
       +(6(),5()) -> c(1(),1())
       +(6(),8()) -> c(1(),4())
       +(7(),0()) -> 7()
       +(7(),1()) -> 8()
       +(7(),2()) -> 9()
       +(7(),3()) -> c(1(),0())
       +(7(),9()) -> c(1(),6())
       +(8(),0()) -> 8()
       +(8(),1()) -> 9()
       +(8(),2()) -> c(1(),0())
       +(8(),3()) -> c(1(),1())
       +(8(),5()) -> c(1(),3())
       +(8(),6()) -> c(1(),4())
       +(8(),8()) -> c(1(),6())
       +(8(),9()) -> c(1(),7())
       +(9(),0()) -> 9()
       +(9(),1()) -> c(1(),0())
       +(9(),2()) -> c(1(),1())
       +(9(),5()) -> c(1(),4())
       +(9(),7()) -> c(1(),6())
       +(9(),8()) -> c(1(),7())
       +(9(),9()) -> c(1(),8())
       c(0(),x) -> x
       c(x,c(y,z)) -> c(+(x,y),z)
     Open