Problem CiME 04 ternary-hard

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 ternary-hard

stdout:

MAYBE

Problem:
 0(#()) -> #()
 +(#(),x) -> x
 +(x,#()) -> x
 +(0(x),0(y)) -> 0(+(x,y))
 +(0(x),1(y)) -> 1(+(x,y))
 +(1(x),0(y)) -> 1(+(x,y))
 +(0(x),j(y)) -> j(+(x,y))
 +(j(x),0(y)) -> j(+(x,y))
 +(1(x),1(y)) -> j(+(+(x,y),1(#())))
 +(j(x),j(y)) -> 1(+(+(x,y),j(#())))
 +(1(x),j(y)) -> 0(+(x,y))
 +(j(x),1(y)) -> 0(+(x,y))
 +(+(x,y),z) -> +(x,+(y,z))
 opp(#()) -> #()
 opp(0(x)) -> 0(opp(x))
 opp(1(x)) -> j(opp(x))
 opp(j(x)) -> 1(opp(x))
 -(x,y) -> +(x,opp(y))
 *(#(),x) -> #()
 *(0(x),y) -> 0(*(x,y))
 *(1(x),y) -> +(0(*(x,y)),y)
 *(j(x),y) -> -(0(*(x,y)),y)
 *(*(x,y),z) -> *(x,*(y,z))
 *(+(x,y),z) -> +(*(x,z),*(y,z))
 *(x,+(y,z)) -> +(*(x,y),*(x,z))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 ternary-hard

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputCiME 04 ternary-hard

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  0(#()) -> #()
     , +(#(), x) -> x
     , +(x, #()) -> x
     , +(0(x), 0(y)) -> 0(+(x, y))
     , +(0(x), 1(y)) -> 1(+(x, y))
     , +(1(x), 0(y)) -> 1(+(x, y))
     , +(0(x), j(y)) -> j(+(x, y))
     , +(j(x), 0(y)) -> j(+(x, y))
     , +(1(x), 1(y)) -> j(+(+(x, y), 1(#())))
     , +(j(x), j(y)) -> 1(+(+(x, y), j(#())))
     , +(1(x), j(y)) -> 0(+(x, y))
     , +(j(x), 1(y)) -> 0(+(x, y))
     , +(+(x, y), z) -> +(x, +(y, z))
     , opp(#()) -> #()
     , opp(0(x)) -> 0(opp(x))
     , opp(1(x)) -> j(opp(x))
     , opp(j(x)) -> 1(opp(x))
     , -(x, y) -> +(x, opp(y))
     , *(#(), x) -> #()
     , *(0(x), y) -> 0(*(x, y))
     , *(1(x), y) -> +(0(*(x, y)), y)
     , *(j(x), y) -> -(0(*(x, y)), y)
     , *(*(x, y), z) -> *(x, *(y, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, +(y, z)) -> +(*(x, y), *(x, z))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 ternary-hard

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputCiME 04 ternary-hard

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  0(#()) -> #()
     , +(#(), x) -> x
     , +(x, #()) -> x
     , +(0(x), 0(y)) -> 0(+(x, y))
     , +(0(x), 1(y)) -> 1(+(x, y))
     , +(1(x), 0(y)) -> 1(+(x, y))
     , +(0(x), j(y)) -> j(+(x, y))
     , +(j(x), 0(y)) -> j(+(x, y))
     , +(1(x), 1(y)) -> j(+(+(x, y), 1(#())))
     , +(j(x), j(y)) -> 1(+(+(x, y), j(#())))
     , +(1(x), j(y)) -> 0(+(x, y))
     , +(j(x), 1(y)) -> 0(+(x, y))
     , +(+(x, y), z) -> +(x, +(y, z))
     , opp(#()) -> #()
     , opp(0(x)) -> 0(opp(x))
     , opp(1(x)) -> j(opp(x))
     , opp(j(x)) -> 1(opp(x))
     , -(x, y) -> +(x, opp(y))
     , *(#(), x) -> #()
     , *(0(x), y) -> 0(*(x, y))
     , *(1(x), y) -> +(0(*(x, y)), y)
     , *(j(x), y) -> -(0(*(x, y)), y)
     , *(*(x, y), z) -> *(x, *(y, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, +(y, z)) -> +(*(x, y), *(x, z))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds