Problem Secret 05 TRS cime2

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 TRS cime2

stdout:

MAYBE

Problem:
circ(cons(a,s),t) -> cons(msubst(a,t),circ(s,t))
circ(cons(lift(),s),cons(a,t)) -> cons(a,circ(s,t))
circ(cons(lift(),s),cons(lift(),t)) -> cons(lift(),circ(s,t))
circ(circ(s,t),u) -> circ(s,circ(t,u))
circ(s,id()) -> s
circ(id(),s) -> s
circ(cons(lift(),s),circ(cons(lift(),t),u)) -> circ(cons(lift(),circ(s,t)),u)
subst(a,id()) -> a
msubst(a,id()) -> a
msubst(msubst(a,s),t) -> msubst(a,circ(s,t))

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 TRS cime2

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 05 TRS cime2

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t))
     , circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t))
     , circ(cons(lift(), s), cons(lift(), t)) ->
       cons(lift(), circ(s, t))
     , circ(circ(s, t), u) -> circ(s, circ(t, u))
     , circ(s, id()) -> s
     , circ(id(), s) -> s
     , circ(cons(lift(), s), circ(cons(lift(), t), u)) ->
       circ(cons(lift(), circ(s, t)), u)
     , subst(a, id()) -> a
     , msubst(a, id()) -> a
     , msubst(msubst(a, s), t) -> msubst(a, circ(s, t))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 TRS cime2

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 05 TRS cime2

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t))
     , circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t))
     , circ(cons(lift(), s), cons(lift(), t)) ->
       cons(lift(), circ(s, t))
     , circ(circ(s, t), u) -> circ(s, circ(t, u))
     , circ(s, id()) -> s
     , circ(id(), s) -> s
     , circ(cons(lift(), s), circ(cons(lift(), t), u)) ->
       circ(cons(lift(), circ(s, t)), u)
     , subst(a, id()) -> a
     , msubst(a, id()) -> a
     , msubst(msubst(a, s), t) -> msubst(a, circ(s, t))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds