Tool CaT
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:
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
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 secondsTool RC1
stdout:
MAYBE
Tool RC2
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