Problem Secret 07 TRS aprove10

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Secret 07 TRS aprove10

stdout:

MAYBE

Problem:
lessElements(l,t) -> lessE(l,t,0())
lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
if(true(),b,l,t,n) -> l
if(false(),true(),l,t,n) -> t
if(false(),false(),l,t,n) -> lessE(l,t,s(n))
length(nil()) -> 0()
length(cons(n,l)) -> s(length(l))
toList(leaf()) -> nil()
toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
append(nil(),l2) -> l2
append(cons(n,l1),l2) -> cons(n,append(l1,l2))
le(s(n),0()) -> false()
le(0(),m) -> true()
le(s(n),s(m)) -> le(n,m)
a() -> c()
a() -> d()

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 07 TRS aprove10

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 07 TRS aprove10

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  lessElements(l, t) -> lessE(l, t, 0())
     , lessE(l, t, n) ->
       if(le(length(l), n), le(length(toList(t)), n), l, t, n)
     , if(true(), b, l, t, n) -> l
     , if(false(), true(), l, t, n) -> t
     , if(false(), false(), l, t, n) -> lessE(l, t, s(n))
     , length(nil()) -> 0()
     , length(cons(n, l)) -> s(length(l))
     , toList(leaf()) -> nil()
     , toList(node(t1, n, t2)) ->
       append(toList(t1), cons(n, toList(t2)))
     , append(nil(), l2) -> l2
     , append(cons(n, l1), l2) -> cons(n, append(l1, l2))
     , le(s(n), 0()) -> false()
     , le(0(), m) -> true()
     , le(s(n), s(m)) -> le(n, m)
     , a() -> c()
     , a() -> d()}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 07 TRS aprove10

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 07 TRS aprove10

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  lessElements(l, t) -> lessE(l, t, 0())
     , lessE(l, t, n) ->
       if(le(length(l), n), le(length(toList(t)), n), l, t, n)
     , if(true(), b, l, t, n) -> l
     , if(false(), true(), l, t, n) -> t
     , if(false(), false(), l, t, n) -> lessE(l, t, s(n))
     , length(nil()) -> 0()
     , length(cons(n, l)) -> s(length(l))
     , toList(leaf()) -> nil()
     , toList(node(t1, n, t2)) ->
       append(toList(t1), cons(n, toList(t2)))
     , append(nil(), l2) -> l2
     , append(cons(n, l1), l2) -> cons(n, append(l1, l2))
     , le(s(n), 0()) -> false()
     , le(0(), m) -> true()
     , le(s(n), s(m)) -> le(n, m)
     , a() -> c()
     , a() -> d()}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds