Problem HirokawaMiddeldorp 04 t000

Tool Bounds

Execution Time35.295246ms
Answer
MAYBE
InputHirokawaMiddeldorp 04 t000

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  c(x, c(y, z)) -> c(+(x, y), z)
     , c(0(), x) -> x
     , +(c(x, y), z) -> c(x, +(y, z))
     , +(x, c(y, z)) -> c(y, +(x, z))
     , +(9(), 9()) -> c(1(), 8())
     , +(9(), 8()) -> c(1(), 7())
     , +(9(), 7()) -> c(1(), 6())
     , +(9(), 6()) -> c(1(), 5())
     , +(9(), 5()) -> c(1(), 4())
     , +(9(), 4()) -> c(1(), 3())
     , +(9(), 3()) -> c(1(), 2())
     , +(9(), 2()) -> c(1(), 1())
     , +(9(), 1()) -> c(1(), 0())
     , +(9(), 0()) -> 9()
     , +(8(), 9()) -> c(1(), 7())
     , +(8(), 8()) -> c(1(), 6())
     , +(8(), 7()) -> c(1(), 5())
     , +(8(), 6()) -> c(1(), 4())
     , +(8(), 5()) -> c(1(), 3())
     , +(8(), 4()) -> c(1(), 2())
     , +(8(), 3()) -> c(1(), 1())
     , +(8(), 2()) -> c(1(), 0())
     , +(8(), 1()) -> 9()
     , +(8(), 0()) -> 8()
     , +(7(), 9()) -> c(1(), 6())
     , +(7(), 8()) -> c(1(), 5())
     , +(7(), 7()) -> c(1(), 4())
     , +(7(), 6()) -> c(1(), 3())
     , +(7(), 5()) -> c(1(), 2())
     , +(7(), 4()) -> c(1(), 1())
     , +(7(), 3()) -> c(1(), 0())
     , +(7(), 2()) -> 9()
     , +(7(), 1()) -> 8()
     , +(7(), 0()) -> 7()
     , +(6(), 9()) -> c(1(), 5())
     , +(6(), 8()) -> c(1(), 4())
     , +(6(), 7()) -> c(1(), 3())
     , +(6(), 6()) -> c(1(), 2())
     , +(6(), 5()) -> c(1(), 1())
     , +(6(), 4()) -> c(1(), 0())
     , +(6(), 3()) -> 9()
     , +(6(), 2()) -> 8()
     , +(6(), 1()) -> 7()
     , +(6(), 0()) -> 6()
     , +(5(), 9()) -> c(1(), 4())
     , +(5(), 8()) -> c(1(), 3())
     , +(5(), 7()) -> c(1(), 2())
     , +(5(), 6()) -> c(1(), 1())
     , +(5(), 5()) -> c(1(), 0())
     , +(5(), 4()) -> 9()
     , +(5(), 3()) -> 8()
     , +(5(), 2()) -> 7()
     , +(5(), 1()) -> 6()
     , +(5(), 0()) -> 5()
     , +(4(), 9()) -> c(1(), 3())
     , +(4(), 8()) -> c(1(), 2())
     , +(4(), 7()) -> c(1(), 1())
     , +(4(), 6()) -> c(1(), 0())
     , +(4(), 5()) -> 9()
     , +(4(), 4()) -> 8()
     , +(4(), 3()) -> 7()
     , +(4(), 2()) -> 6()
     , +(4(), 1()) -> 5()
     , +(4(), 0()) -> 4()
     , +(3(), 9()) -> c(1(), 2())
     , +(3(), 8()) -> c(1(), 1())
     , +(3(), 7()) -> c(1(), 0())
     , +(3(), 6()) -> 9()
     , +(3(), 5()) -> 8()
     , +(3(), 4()) -> 7()
     , +(3(), 3()) -> 6()
     , +(3(), 2()) -> 5()
     , +(3(), 1()) -> 4()
     , +(3(), 0()) -> 3()
     , +(2(), 9()) -> c(1(), 1())
     , +(2(), 8()) -> c(1(), 0())
     , +(2(), 7()) -> 9()
     , +(2(), 6()) -> 8()
     , +(2(), 5()) -> 7()
     , +(2(), 4()) -> 6()
     , +(2(), 3()) -> 5()
     , +(2(), 2()) -> 4()
     , +(2(), 1()) -> 3()
     , +(2(), 0()) -> 2()
     , +(1(), 9()) -> c(1(), 0())
     , +(1(), 8()) -> 9()
     , +(1(), 7()) -> 8()
     , +(1(), 6()) -> 7()
     , +(1(), 5()) -> 6()
     , +(1(), 4()) -> 5()
     , +(1(), 3()) -> 4()
     , +(1(), 2()) -> 3()
     , +(1(), 1()) -> 2()
     , +(1(), 0()) -> 1()
     , +(0(), 9()) -> 9()
     , +(0(), 8()) -> 8()
     , +(0(), 7()) -> 7()
     , +(0(), 6()) -> 6()
     , +(0(), 5()) -> 5()
     , +(0(), 4()) -> 4()
     , +(0(), 3()) -> 3()
     , +(0(), 2()) -> 2()
     , +(0(), 1()) -> 1()
     , +(0(), 0()) -> 0()}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  None of the processors succeeded.
  

Arrrr..

Tool CDI

Execution Time60.223633ms
Answer
TIMEOUT
InputHirokawaMiddeldorp 04 t000

stdout:

TIMEOUT

Statistics:
Number of monomials: 12812
Last formula building started for bound 3
Last SAT solving started for bound 3

Tool EDA

Execution Time60.120335ms
Answer
TIMEOUT
InputHirokawaMiddeldorp 04 t000

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  c(x, c(y, z)) -> c(+(x, y), z)
     , c(0(), x) -> x
     , +(c(x, y), z) -> c(x, +(y, z))
     , +(x, c(y, z)) -> c(y, +(x, z))
     , +(9(), 9()) -> c(1(), 8())
     , +(9(), 8()) -> c(1(), 7())
     , +(9(), 7()) -> c(1(), 6())
     , +(9(), 6()) -> c(1(), 5())
     , +(9(), 5()) -> c(1(), 4())
     , +(9(), 4()) -> c(1(), 3())
     , +(9(), 3()) -> c(1(), 2())
     , +(9(), 2()) -> c(1(), 1())
     , +(9(), 1()) -> c(1(), 0())
     , +(9(), 0()) -> 9()
     , +(8(), 9()) -> c(1(), 7())
     , +(8(), 8()) -> c(1(), 6())
     , +(8(), 7()) -> c(1(), 5())
     , +(8(), 6()) -> c(1(), 4())
     , +(8(), 5()) -> c(1(), 3())
     , +(8(), 4()) -> c(1(), 2())
     , +(8(), 3()) -> c(1(), 1())
     , +(8(), 2()) -> c(1(), 0())
     , +(8(), 1()) -> 9()
     , +(8(), 0()) -> 8()
     , +(7(), 9()) -> c(1(), 6())
     , +(7(), 8()) -> c(1(), 5())
     , +(7(), 7()) -> c(1(), 4())
     , +(7(), 6()) -> c(1(), 3())
     , +(7(), 5()) -> c(1(), 2())
     , +(7(), 4()) -> c(1(), 1())
     , +(7(), 3()) -> c(1(), 0())
     , +(7(), 2()) -> 9()
     , +(7(), 1()) -> 8()
     , +(7(), 0()) -> 7()
     , +(6(), 9()) -> c(1(), 5())
     , +(6(), 8()) -> c(1(), 4())
     , +(6(), 7()) -> c(1(), 3())
     , +(6(), 6()) -> c(1(), 2())
     , +(6(), 5()) -> c(1(), 1())
     , +(6(), 4()) -> c(1(), 0())
     , +(6(), 3()) -> 9()
     , +(6(), 2()) -> 8()
     , +(6(), 1()) -> 7()
     , +(6(), 0()) -> 6()
     , +(5(), 9()) -> c(1(), 4())
     , +(5(), 8()) -> c(1(), 3())
     , +(5(), 7()) -> c(1(), 2())
     , +(5(), 6()) -> c(1(), 1())
     , +(5(), 5()) -> c(1(), 0())
     , +(5(), 4()) -> 9()
     , +(5(), 3()) -> 8()
     , +(5(), 2()) -> 7()
     , +(5(), 1()) -> 6()
     , +(5(), 0()) -> 5()
     , +(4(), 9()) -> c(1(), 3())
     , +(4(), 8()) -> c(1(), 2())
     , +(4(), 7()) -> c(1(), 1())
     , +(4(), 6()) -> c(1(), 0())
     , +(4(), 5()) -> 9()
     , +(4(), 4()) -> 8()
     , +(4(), 3()) -> 7()
     , +(4(), 2()) -> 6()
     , +(4(), 1()) -> 5()
     , +(4(), 0()) -> 4()
     , +(3(), 9()) -> c(1(), 2())
     , +(3(), 8()) -> c(1(), 1())
     , +(3(), 7()) -> c(1(), 0())
     , +(3(), 6()) -> 9()
     , +(3(), 5()) -> 8()
     , +(3(), 4()) -> 7()
     , +(3(), 3()) -> 6()
     , +(3(), 2()) -> 5()
     , +(3(), 1()) -> 4()
     , +(3(), 0()) -> 3()
     , +(2(), 9()) -> c(1(), 1())
     , +(2(), 8()) -> c(1(), 0())
     , +(2(), 7()) -> 9()
     , +(2(), 6()) -> 8()
     , +(2(), 5()) -> 7()
     , +(2(), 4()) -> 6()
     , +(2(), 3()) -> 5()
     , +(2(), 2()) -> 4()
     , +(2(), 1()) -> 3()
     , +(2(), 0()) -> 2()
     , +(1(), 9()) -> c(1(), 0())
     , +(1(), 8()) -> 9()
     , +(1(), 7()) -> 8()
     , +(1(), 6()) -> 7()
     , +(1(), 5()) -> 6()
     , +(1(), 4()) -> 5()
     , +(1(), 3()) -> 4()
     , +(1(), 2()) -> 3()
     , +(1(), 1()) -> 2()
     , +(1(), 0()) -> 1()
     , +(0(), 9()) -> 9()
     , +(0(), 8()) -> 8()
     , +(0(), 7()) -> 7()
     , +(0(), 6()) -> 6()
     , +(0(), 5()) -> 5()
     , +(0(), 4()) -> 4()
     , +(0(), 3()) -> 3()
     , +(0(), 2()) -> 2()
     , +(0(), 1()) -> 1()
     , +(0(), 0()) -> 0()}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool IDA

Execution Time29.759945ms
Answer
MAYBE
InputHirokawaMiddeldorp 04 t000

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  c(x, c(y, z)) -> c(+(x, y), z)
     , c(0(), x) -> x
     , +(c(x, y), z) -> c(x, +(y, z))
     , +(x, c(y, z)) -> c(y, +(x, z))
     , +(9(), 9()) -> c(1(), 8())
     , +(9(), 8()) -> c(1(), 7())
     , +(9(), 7()) -> c(1(), 6())
     , +(9(), 6()) -> c(1(), 5())
     , +(9(), 5()) -> c(1(), 4())
     , +(9(), 4()) -> c(1(), 3())
     , +(9(), 3()) -> c(1(), 2())
     , +(9(), 2()) -> c(1(), 1())
     , +(9(), 1()) -> c(1(), 0())
     , +(9(), 0()) -> 9()
     , +(8(), 9()) -> c(1(), 7())
     , +(8(), 8()) -> c(1(), 6())
     , +(8(), 7()) -> c(1(), 5())
     , +(8(), 6()) -> c(1(), 4())
     , +(8(), 5()) -> c(1(), 3())
     , +(8(), 4()) -> c(1(), 2())
     , +(8(), 3()) -> c(1(), 1())
     , +(8(), 2()) -> c(1(), 0())
     , +(8(), 1()) -> 9()
     , +(8(), 0()) -> 8()
     , +(7(), 9()) -> c(1(), 6())
     , +(7(), 8()) -> c(1(), 5())
     , +(7(), 7()) -> c(1(), 4())
     , +(7(), 6()) -> c(1(), 3())
     , +(7(), 5()) -> c(1(), 2())
     , +(7(), 4()) -> c(1(), 1())
     , +(7(), 3()) -> c(1(), 0())
     , +(7(), 2()) -> 9()
     , +(7(), 1()) -> 8()
     , +(7(), 0()) -> 7()
     , +(6(), 9()) -> c(1(), 5())
     , +(6(), 8()) -> c(1(), 4())
     , +(6(), 7()) -> c(1(), 3())
     , +(6(), 6()) -> c(1(), 2())
     , +(6(), 5()) -> c(1(), 1())
     , +(6(), 4()) -> c(1(), 0())
     , +(6(), 3()) -> 9()
     , +(6(), 2()) -> 8()
     , +(6(), 1()) -> 7()
     , +(6(), 0()) -> 6()
     , +(5(), 9()) -> c(1(), 4())
     , +(5(), 8()) -> c(1(), 3())
     , +(5(), 7()) -> c(1(), 2())
     , +(5(), 6()) -> c(1(), 1())
     , +(5(), 5()) -> c(1(), 0())
     , +(5(), 4()) -> 9()
     , +(5(), 3()) -> 8()
     , +(5(), 2()) -> 7()
     , +(5(), 1()) -> 6()
     , +(5(), 0()) -> 5()
     , +(4(), 9()) -> c(1(), 3())
     , +(4(), 8()) -> c(1(), 2())
     , +(4(), 7()) -> c(1(), 1())
     , +(4(), 6()) -> c(1(), 0())
     , +(4(), 5()) -> 9()
     , +(4(), 4()) -> 8()
     , +(4(), 3()) -> 7()
     , +(4(), 2()) -> 6()
     , +(4(), 1()) -> 5()
     , +(4(), 0()) -> 4()
     , +(3(), 9()) -> c(1(), 2())
     , +(3(), 8()) -> c(1(), 1())
     , +(3(), 7()) -> c(1(), 0())
     , +(3(), 6()) -> 9()
     , +(3(), 5()) -> 8()
     , +(3(), 4()) -> 7()
     , +(3(), 3()) -> 6()
     , +(3(), 2()) -> 5()
     , +(3(), 1()) -> 4()
     , +(3(), 0()) -> 3()
     , +(2(), 9()) -> c(1(), 1())
     , +(2(), 8()) -> c(1(), 0())
     , +(2(), 7()) -> 9()
     , +(2(), 6()) -> 8()
     , +(2(), 5()) -> 7()
     , +(2(), 4()) -> 6()
     , +(2(), 3()) -> 5()
     , +(2(), 2()) -> 4()
     , +(2(), 1()) -> 3()
     , +(2(), 0()) -> 2()
     , +(1(), 9()) -> c(1(), 0())
     , +(1(), 8()) -> 9()
     , +(1(), 7()) -> 8()
     , +(1(), 6()) -> 7()
     , +(1(), 5()) -> 6()
     , +(1(), 4()) -> 5()
     , +(1(), 3()) -> 4()
     , +(1(), 2()) -> 3()
     , +(1(), 1()) -> 2()
     , +(1(), 0()) -> 1()
     , +(0(), 9()) -> 9()
     , +(0(), 8()) -> 8()
     , +(0(), 7()) -> 7()
     , +(0(), 6()) -> 6()
     , +(0(), 5()) -> 5()
     , +(0(), 4()) -> 4()
     , +(0(), 3()) -> 3()
     , +(0(), 2()) -> 2()
     , +(0(), 1()) -> 1()
     , +(0(), 0()) -> 0()}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible
    
    2) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible
    
    3) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible
    
    4) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible
    
    5) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible
    
    6) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    

Arrrr..

Tool TRI

Execution Time23.575012ms
Answer
MAYBE
InputHirokawaMiddeldorp 04 t000

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  c(x, c(y, z)) -> c(+(x, y), z)
     , c(0(), x) -> x
     , +(c(x, y), z) -> c(x, +(y, z))
     , +(x, c(y, z)) -> c(y, +(x, z))
     , +(9(), 9()) -> c(1(), 8())
     , +(9(), 8()) -> c(1(), 7())
     , +(9(), 7()) -> c(1(), 6())
     , +(9(), 6()) -> c(1(), 5())
     , +(9(), 5()) -> c(1(), 4())
     , +(9(), 4()) -> c(1(), 3())
     , +(9(), 3()) -> c(1(), 2())
     , +(9(), 2()) -> c(1(), 1())
     , +(9(), 1()) -> c(1(), 0())
     , +(9(), 0()) -> 9()
     , +(8(), 9()) -> c(1(), 7())
     , +(8(), 8()) -> c(1(), 6())
     , +(8(), 7()) -> c(1(), 5())
     , +(8(), 6()) -> c(1(), 4())
     , +(8(), 5()) -> c(1(), 3())
     , +(8(), 4()) -> c(1(), 2())
     , +(8(), 3()) -> c(1(), 1())
     , +(8(), 2()) -> c(1(), 0())
     , +(8(), 1()) -> 9()
     , +(8(), 0()) -> 8()
     , +(7(), 9()) -> c(1(), 6())
     , +(7(), 8()) -> c(1(), 5())
     , +(7(), 7()) -> c(1(), 4())
     , +(7(), 6()) -> c(1(), 3())
     , +(7(), 5()) -> c(1(), 2())
     , +(7(), 4()) -> c(1(), 1())
     , +(7(), 3()) -> c(1(), 0())
     , +(7(), 2()) -> 9()
     , +(7(), 1()) -> 8()
     , +(7(), 0()) -> 7()
     , +(6(), 9()) -> c(1(), 5())
     , +(6(), 8()) -> c(1(), 4())
     , +(6(), 7()) -> c(1(), 3())
     , +(6(), 6()) -> c(1(), 2())
     , +(6(), 5()) -> c(1(), 1())
     , +(6(), 4()) -> c(1(), 0())
     , +(6(), 3()) -> 9()
     , +(6(), 2()) -> 8()
     , +(6(), 1()) -> 7()
     , +(6(), 0()) -> 6()
     , +(5(), 9()) -> c(1(), 4())
     , +(5(), 8()) -> c(1(), 3())
     , +(5(), 7()) -> c(1(), 2())
     , +(5(), 6()) -> c(1(), 1())
     , +(5(), 5()) -> c(1(), 0())
     , +(5(), 4()) -> 9()
     , +(5(), 3()) -> 8()
     , +(5(), 2()) -> 7()
     , +(5(), 1()) -> 6()
     , +(5(), 0()) -> 5()
     , +(4(), 9()) -> c(1(), 3())
     , +(4(), 8()) -> c(1(), 2())
     , +(4(), 7()) -> c(1(), 1())
     , +(4(), 6()) -> c(1(), 0())
     , +(4(), 5()) -> 9()
     , +(4(), 4()) -> 8()
     , +(4(), 3()) -> 7()
     , +(4(), 2()) -> 6()
     , +(4(), 1()) -> 5()
     , +(4(), 0()) -> 4()
     , +(3(), 9()) -> c(1(), 2())
     , +(3(), 8()) -> c(1(), 1())
     , +(3(), 7()) -> c(1(), 0())
     , +(3(), 6()) -> 9()
     , +(3(), 5()) -> 8()
     , +(3(), 4()) -> 7()
     , +(3(), 3()) -> 6()
     , +(3(), 2()) -> 5()
     , +(3(), 1()) -> 4()
     , +(3(), 0()) -> 3()
     , +(2(), 9()) -> c(1(), 1())
     , +(2(), 8()) -> c(1(), 0())
     , +(2(), 7()) -> 9()
     , +(2(), 6()) -> 8()
     , +(2(), 5()) -> 7()
     , +(2(), 4()) -> 6()
     , +(2(), 3()) -> 5()
     , +(2(), 2()) -> 4()
     , +(2(), 1()) -> 3()
     , +(2(), 0()) -> 2()
     , +(1(), 9()) -> c(1(), 0())
     , +(1(), 8()) -> 9()
     , +(1(), 7()) -> 8()
     , +(1(), 6()) -> 7()
     , +(1(), 5()) -> 6()
     , +(1(), 4()) -> 5()
     , +(1(), 3()) -> 4()
     , +(1(), 2()) -> 3()
     , +(1(), 1()) -> 2()
     , +(1(), 0()) -> 1()
     , +(0(), 9()) -> 9()
     , +(0(), 8()) -> 8()
     , +(0(), 7()) -> 7()
     , +(0(), 6()) -> 6()
     , +(0(), 5()) -> 5()
     , +(0(), 4()) -> 4()
     , +(0(), 3()) -> 3()
     , +(0(), 2()) -> 2()
     , +(0(), 1()) -> 1()
     , +(0(), 0()) -> 0()}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'matrix-interpretation of dimension 5' failed due to the following reason:
         The input cannot be shown compatible
    
    2) 'matrix-interpretation of dimension 4' failed due to the following reason:
         The input cannot be shown compatible
    
    3) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible
    
    4) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible
    
    5) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    

Arrrr..

Tool TRI2

Execution Time2.143338ms
Answer
MAYBE
InputHirokawaMiddeldorp 04 t000

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  c(x, c(y, z)) -> c(+(x, y), z)
     , c(0(), x) -> x
     , +(c(x, y), z) -> c(x, +(y, z))
     , +(x, c(y, z)) -> c(y, +(x, z))
     , +(9(), 9()) -> c(1(), 8())
     , +(9(), 8()) -> c(1(), 7())
     , +(9(), 7()) -> c(1(), 6())
     , +(9(), 6()) -> c(1(), 5())
     , +(9(), 5()) -> c(1(), 4())
     , +(9(), 4()) -> c(1(), 3())
     , +(9(), 3()) -> c(1(), 2())
     , +(9(), 2()) -> c(1(), 1())
     , +(9(), 1()) -> c(1(), 0())
     , +(9(), 0()) -> 9()
     , +(8(), 9()) -> c(1(), 7())
     , +(8(), 8()) -> c(1(), 6())
     , +(8(), 7()) -> c(1(), 5())
     , +(8(), 6()) -> c(1(), 4())
     , +(8(), 5()) -> c(1(), 3())
     , +(8(), 4()) -> c(1(), 2())
     , +(8(), 3()) -> c(1(), 1())
     , +(8(), 2()) -> c(1(), 0())
     , +(8(), 1()) -> 9()
     , +(8(), 0()) -> 8()
     , +(7(), 9()) -> c(1(), 6())
     , +(7(), 8()) -> c(1(), 5())
     , +(7(), 7()) -> c(1(), 4())
     , +(7(), 6()) -> c(1(), 3())
     , +(7(), 5()) -> c(1(), 2())
     , +(7(), 4()) -> c(1(), 1())
     , +(7(), 3()) -> c(1(), 0())
     , +(7(), 2()) -> 9()
     , +(7(), 1()) -> 8()
     , +(7(), 0()) -> 7()
     , +(6(), 9()) -> c(1(), 5())
     , +(6(), 8()) -> c(1(), 4())
     , +(6(), 7()) -> c(1(), 3())
     , +(6(), 6()) -> c(1(), 2())
     , +(6(), 5()) -> c(1(), 1())
     , +(6(), 4()) -> c(1(), 0())
     , +(6(), 3()) -> 9()
     , +(6(), 2()) -> 8()
     , +(6(), 1()) -> 7()
     , +(6(), 0()) -> 6()
     , +(5(), 9()) -> c(1(), 4())
     , +(5(), 8()) -> c(1(), 3())
     , +(5(), 7()) -> c(1(), 2())
     , +(5(), 6()) -> c(1(), 1())
     , +(5(), 5()) -> c(1(), 0())
     , +(5(), 4()) -> 9()
     , +(5(), 3()) -> 8()
     , +(5(), 2()) -> 7()
     , +(5(), 1()) -> 6()
     , +(5(), 0()) -> 5()
     , +(4(), 9()) -> c(1(), 3())
     , +(4(), 8()) -> c(1(), 2())
     , +(4(), 7()) -> c(1(), 1())
     , +(4(), 6()) -> c(1(), 0())
     , +(4(), 5()) -> 9()
     , +(4(), 4()) -> 8()
     , +(4(), 3()) -> 7()
     , +(4(), 2()) -> 6()
     , +(4(), 1()) -> 5()
     , +(4(), 0()) -> 4()
     , +(3(), 9()) -> c(1(), 2())
     , +(3(), 8()) -> c(1(), 1())
     , +(3(), 7()) -> c(1(), 0())
     , +(3(), 6()) -> 9()
     , +(3(), 5()) -> 8()
     , +(3(), 4()) -> 7()
     , +(3(), 3()) -> 6()
     , +(3(), 2()) -> 5()
     , +(3(), 1()) -> 4()
     , +(3(), 0()) -> 3()
     , +(2(), 9()) -> c(1(), 1())
     , +(2(), 8()) -> c(1(), 0())
     , +(2(), 7()) -> 9()
     , +(2(), 6()) -> 8()
     , +(2(), 5()) -> 7()
     , +(2(), 4()) -> 6()
     , +(2(), 3()) -> 5()
     , +(2(), 2()) -> 4()
     , +(2(), 1()) -> 3()
     , +(2(), 0()) -> 2()
     , +(1(), 9()) -> c(1(), 0())
     , +(1(), 8()) -> 9()
     , +(1(), 7()) -> 8()
     , +(1(), 6()) -> 7()
     , +(1(), 5()) -> 6()
     , +(1(), 4()) -> 5()
     , +(1(), 3()) -> 4()
     , +(1(), 2()) -> 3()
     , +(1(), 1()) -> 2()
     , +(1(), 0()) -> 1()
     , +(0(), 9()) -> 9()
     , +(0(), 8()) -> 8()
     , +(0(), 7()) -> 7()
     , +(0(), 6()) -> 6()
     , +(0(), 5()) -> 5()
     , +(0(), 4()) -> 4()
     , +(0(), 3()) -> 3()
     , +(0(), 2()) -> 2()
     , +(0(), 1()) -> 1()
     , +(0(), 0()) -> 0()}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..