Problem Transformed CSR 04 Ex49 GM04 FR

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex49 GM04 FR

stdout:

MAYBE

Problem:
minus(n__0(),Y) -> 0()
minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
geq(X,n__0()) -> true()
geq(n__0(),n__s(Y)) -> false()
geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
div(0(),n__s(Y)) -> 0()
div(s(X),n__s(Y)) ->
if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
if(true(),X,Y) -> activate(X)
if(false(),X,Y) -> activate(Y)
0() -> n__0()
s(X) -> n__s(X)
div(X1,X2) -> n__div(X1,X2)
minus(X1,X2) -> n__minus(X1,X2)
activate(n__0()) -> 0()
activate(n__s(X)) -> s(activate(X))
activate(n__div(X1,X2)) -> div(activate(X1),X2)
activate(n__minus(X1,X2)) -> minus(X1,X2)
activate(X) -> X

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex49 GM04 FR

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex49 GM04 FR

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  minus(n__0(), Y) -> 0()
     , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
     , geq(X, n__0()) -> true()
     , geq(n__0(), n__s(Y)) -> false()
     , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
     , div(0(), n__s(Y)) -> 0()
     , div(s(X), n__s(Y)) ->
       if(geq(X, activate(Y)),
          n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
          n__0())
     , if(true(), X, Y) -> activate(X)
     , if(false(), X, Y) -> activate(Y)
     , 0() -> n__0()
     , s(X) -> n__s(X)
     , div(X1, X2) -> n__div(X1, X2)
     , minus(X1, X2) -> n__minus(X1, X2)
     , activate(n__0()) -> 0()
     , activate(n__s(X)) -> s(activate(X))
     , activate(n__div(X1, X2)) -> div(activate(X1), X2)
     , activate(n__minus(X1, X2)) -> minus(X1, X2)
     , activate(X) -> X}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex49 GM04 FR

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex49 GM04 FR

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  minus(n__0(), Y) -> 0()
     , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
     , geq(X, n__0()) -> true()
     , geq(n__0(), n__s(Y)) -> false()
     , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
     , div(0(), n__s(Y)) -> 0()
     , div(s(X), n__s(Y)) ->
       if(geq(X, activate(Y)),
          n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
          n__0())
     , if(true(), X, Y) -> activate(X)
     , if(false(), X, Y) -> activate(Y)
     , 0() -> n__0()
     , s(X) -> n__s(X)
     , div(X1, X2) -> n__div(X1, X2)
     , minus(X1, X2) -> n__minus(X1, X2)
     , activate(n__0()) -> 0()
     , activate(n__s(X)) -> s(activate(X))
     , activate(n__div(X1, X2)) -> div(activate(X1), X2)
     , activate(n__minus(X1, X2)) -> minus(X1, X2)
     , activate(X) -> X}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds