Problem Strategy outermost added 08 ExIntrod Zan97 Z

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 ExIntrod Zan97 Z

stdout:

MAYBE

Problem:
 fact(X) -> if(zero(X),n__s(0()),n__prod(X,fact(p(X))))
 add(0(),X) -> X
 add(s(X),Y) -> s(add(X,Y))
 prod(0(),X) -> 0()
 prod(s(X),Y) -> add(Y,prod(X,Y))
 if(true(),X,Y) -> activate(X)
 if(false(),X,Y) -> activate(Y)
 zero(0()) -> true()
 zero(s(X)) -> false()
 p(s(X)) -> X
 s(X) -> n__s(X)
 prod(X1,X2) -> n__prod(X1,X2)
 activate(n__s(X)) -> s(X)
 activate(n__prod(X1,X2)) -> prod(X1,X2)
 activate(X) -> X

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 ExIntrod Zan97 Z

stdout:

MAYBE
 Warning when parsing problem:
                             
                               Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputStrategy outermost added 08 ExIntrod Zan97 Z

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  fact(X) -> if(zero(X), n__s(0()), n__prod(X, fact(p(X))))
     , add(0(), X) -> X
     , add(s(X), Y) -> s(add(X, Y))
     , prod(0(), X) -> 0()
     , prod(s(X), Y) -> add(Y, prod(X, Y))
     , if(true(), X, Y) -> activate(X)
     , if(false(), X, Y) -> activate(Y)
     , zero(0()) -> true()
     , zero(s(X)) -> false()
     , p(s(X)) -> X
     , s(X) -> n__s(X)
     , prod(X1, X2) -> n__prod(X1, X2)
     , activate(n__s(X)) -> s(X)
     , activate(n__prod(X1, X2)) -> prod(X1, X2)
     , activate(X) -> X}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 ExIntrod Zan97 Z

stdout:

MAYBE
 Warning when parsing problem:
                             
                               Unsupported strategy 'OUTERMOST'

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputStrategy outermost added 08 ExIntrod Zan97 Z

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  fact(X) -> if(zero(X), n__s(0()), n__prod(X, fact(p(X))))
     , add(0(), X) -> X
     , add(s(X), Y) -> s(add(X, Y))
     , prod(0(), X) -> 0()
     , prod(s(X), Y) -> add(Y, prod(X, Y))
     , if(true(), X, Y) -> activate(X)
     , if(false(), X, Y) -> activate(Y)
     , zero(0()) -> true()
     , zero(s(X)) -> false()
     , p(s(X)) -> X
     , s(X) -> n__s(X)
     , prod(X1, X2) -> n__prod(X1, X2)
     , activate(n__s(X)) -> s(X)
     , activate(n__prod(X1, X2)) -> prod(X1, X2)
     , activate(X) -> X}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds