Problem Secret 05 TRS aprove2

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 TRS aprove2

stdout:

MAYBE

Problem:
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
div(x,y) -> ify(ge(y,s(0())),x,y)
ify(false(),x,y) -> divByZeroError()
ify(true(),x,y) -> if(ge(x,y),x,y)
if(false(),x,y) -> 0()
if(true(),x,y) -> s(div(minus(x,y),y))

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 TRS aprove2

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 05 TRS aprove2

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  ge(x, 0()) -> true()
     , ge(0(), s(x)) -> false()
     , ge(s(x), s(y)) -> ge(x, y)
     , minus(x, 0()) -> x
     , minus(s(x), s(y)) -> minus(x, y)
     , div(x, y) -> ify(ge(y, s(0())), x, y)
     , ify(false(), x, y) -> divByZeroError()
     , ify(true(), x, y) -> if(ge(x, y), x, y)
     , if(false(), x, y) -> 0()
     , if(true(), x, y) -> s(div(minus(x, y), y))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 TRS aprove2

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 05 TRS aprove2

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  ge(x, 0()) -> true()
     , ge(0(), s(x)) -> false()
     , ge(s(x), s(y)) -> ge(x, y)
     , minus(x, 0()) -> x
     , minus(s(x), s(y)) -> minus(x, y)
     , div(x, y) -> ify(ge(y, s(0())), x, y)
     , ify(false(), x, y) -> divByZeroError()
     , ify(true(), x, y) -> if(ge(x, y), x, y)
     , if(false(), x, y) -> 0()
     , if(true(), x, y) -> s(div(minus(x, y), y))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds