Problem AProVE 07 kabasci03

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAProVE 07 kabasci03

stdout:

MAYBE

Problem:
 h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w))))))
 h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w)))
 h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x)))))
 t(t(x)) -> t(c(t(x),x))
 t(x) -> x
 t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x)))))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 07 kabasci03

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 07 kabasci03

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  h(c(x, y), c(s(z), z), t(w)) ->
       h(z, c(y, x), t(t(c(x, c(y, t(w))))))
     , h(x, c(y, z), t(w)) -> h(c(s(y), x), z, t(c(t(w), w)))
     , h(c(s(x), c(s(0()), y)), z, t(x)) ->
       h(y, c(s(0()), c(x, z)), t(t(c(x, s(x)))))
     , t(t(x)) -> t(c(t(x), x))
     , t(x) -> x
     , t(x) -> c(0(), c(0(), c(0(), c(0(), c(0(), x)))))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 07 kabasci03

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 07 kabasci03

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  h(c(x, y), c(s(z), z), t(w)) ->
       h(z, c(y, x), t(t(c(x, c(y, t(w))))))
     , h(x, c(y, z), t(w)) -> h(c(s(y), x), z, t(c(t(w), w)))
     , h(c(s(x), c(s(0()), y)), z, t(x)) ->
       h(y, c(s(0()), c(x, z)), t(t(c(x, s(x)))))
     , t(t(x)) -> t(c(t(x), x))
     , t(x) -> x
     , t(x) -> c(0(), c(0(), c(0(), c(0(), c(0(), x)))))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds