Problem CiME 04 lse

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	CiME 04 lse

stdout:

MAYBE

Problem:
Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
Term_sub(Term_var(x),Id()) -> Term_var(x)
Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
Sum_sub(xi,Id()) -> Sum_term_var(xi)
Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
Concat(Id(),s) -> s

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	CiME 04 lse

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	CiME 04 lse

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
     , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
     , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
     , Frozen(m, Sum_term_var(xi), n, s) ->
       Case(Term_sub(m, s), xi, Term_sub(n, s))
     , Term_sub(Term_app(m, n), s) ->
       Term_app(Term_sub(m, s), Term_sub(n, s))
     , Term_sub(Term_pair(m, n), s) ->
       Term_pair(Term_sub(m, s), Term_sub(n, s))
     , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
     , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
     , Term_sub(Term_var(x), Id()) -> Term_var(x)
     , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
     , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
       Term_sub(Term_var(x), s)
     , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
       Term_sub(Term_var(x), s)
     , Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
     , Sum_sub(xi, Id()) -> Sum_term_var(xi)
     , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
     , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
     , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
     , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
     , Concat(Cons_usual(x, m, s), t) ->
       Cons_usual(x, Term_sub(m, t), Concat(s, t))
     , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
     , Concat(Id(), s) -> s}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	CiME 04 lse

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	CiME 04 lse

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
     , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
     , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
     , Frozen(m, Sum_term_var(xi), n, s) ->
       Case(Term_sub(m, s), xi, Term_sub(n, s))
     , Term_sub(Term_app(m, n), s) ->
       Term_app(Term_sub(m, s), Term_sub(n, s))
     , Term_sub(Term_pair(m, n), s) ->
       Term_pair(Term_sub(m, s), Term_sub(n, s))
     , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
     , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
     , Term_sub(Term_var(x), Id()) -> Term_var(x)
     , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
     , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
       Term_sub(Term_var(x), s)
     , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
       Term_sub(Term_var(x), s)
     , Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
     , Sum_sub(xi, Id()) -> Sum_term_var(xi)
     , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
     , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
     , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
     , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
     , Concat(Cons_usual(x, m, s), t) ->
       Cons_usual(x, Term_sub(m, t), Concat(s, t))
     , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
     , Concat(Id(), s) -> s}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds