Problem CiME 04 maude2

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 maude2

stdout:

MAYBE

Problem:
 p(s(N)) -> N
 +(N,0()) -> N
 +(s(N),s(M)) -> s(s(+(N,M)))
 *(N,0()) -> 0()
 *(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
 gt(0(),M) -> False()
 gt(NzN,0()) -> u_4(is_NzNat(NzN))
 u_4(True()) -> True()
 is_NzNat(0()) -> False()
 is_NzNat(s(N)) -> True()
 gt(s(N),s(M)) -> gt(N,M)
 lt(N,M) -> gt(M,N)
 d(0(),N) -> N
 d(s(N),s(M)) -> d(N,M)
 quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
 u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
 u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
 quot(NzM,NzM) -> u_01(is_NzNat(NzM))
 u_01(True()) -> s(0())
 quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
 u_21(True(),NzM,N) -> u_2(gt(NzM,N))
 u_2(True()) -> 0()
 gcd(0(),N) -> 0()
 gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
 u_02(True(),NzM) -> NzM
 gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
 u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
 u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 maude2

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputCiME 04 maude2

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  p(s(N)) -> N
     , +(N, 0()) -> N
     , +(s(N), s(M)) -> s(s(+(N, M)))
     , *(N, 0()) -> 0()
     , *(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
     , gt(0(), M) -> False()
     , gt(NzN, 0()) -> u_4(is_NzNat(NzN))
     , u_4(True()) -> True()
     , is_NzNat(0()) -> False()
     , is_NzNat(s(N)) -> True()
     , gt(s(N), s(M)) -> gt(N, M)
     , lt(N, M) -> gt(M, N)
     , d(0(), N) -> N
     , d(s(N), s(M)) -> d(N, M)
     , quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM)
     , u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM)
     , u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM))
     , quot(NzM, NzM) -> u_01(is_NzNat(NzM))
     , u_01(True()) -> s(0())
     , quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N)
     , u_21(True(), NzM, N) -> u_2(gt(NzM, N))
     , u_2(True()) -> 0()
     , gcd(0(), N) -> 0()
     , gcd(NzM, NzM) -> u_02(is_NzNat(NzM), NzM)
     , u_02(True(), NzM) -> NzM
     , gcd(NzN, NzM) -> u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
     , u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM)
     , u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 maude2

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputCiME 04 maude2

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  p(s(N)) -> N
     , +(N, 0()) -> N
     , +(s(N), s(M)) -> s(s(+(N, M)))
     , *(N, 0()) -> 0()
     , *(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
     , gt(0(), M) -> False()
     , gt(NzN, 0()) -> u_4(is_NzNat(NzN))
     , u_4(True()) -> True()
     , is_NzNat(0()) -> False()
     , is_NzNat(s(N)) -> True()
     , gt(s(N), s(M)) -> gt(N, M)
     , lt(N, M) -> gt(M, N)
     , d(0(), N) -> N
     , d(s(N), s(M)) -> d(N, M)
     , quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM)
     , u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM)
     , u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM))
     , quot(NzM, NzM) -> u_01(is_NzNat(NzM))
     , u_01(True()) -> s(0())
     , quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N)
     , u_21(True(), NzM, N) -> u_2(gt(NzM, N))
     , u_2(True()) -> 0()
     , gcd(0(), N) -> 0()
     , gcd(NzM, NzM) -> u_02(is_NzNat(NzM), NzM)
     , u_02(True(), NzM) -> NzM
     , gcd(NzN, NzM) -> u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
     , u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM)
     , u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds