MAYBE
MAYBE
TRS:
 {
  c(x, c(y, z)) -> c(+(x, y), z),
      c(0(), x) -> x,
  +(x, c(y, z)) -> c(y, +(x, 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(*(x, 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())
 }
 DUP: We consider a duplicating system.
  Trs:
   {
    c(x, c(y, z)) -> c(+(x, y), z),
        c(0(), x) -> x,
    +(x, c(y, z)) -> c(y, +(x, 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(*(x, 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())
   }
  Fail