Tool CaT
stdout:
MAYBE
Problem:
sort(l) -> st(0(),l)
st(n,l) -> cond1(member(n,l),n,l)
cond1(true(),n,l) -> cons(n,st(s(n),l))
cond1(false(),n,l) -> cond2(gt(n,max(l)),n,l)
cond2(true(),n,l) -> nil()
cond2(false(),n,l) -> st(s(n),l)
member(n,nil()) -> false()
member(n,cons(m,l)) -> or(equal(n,m),member(n,l))
or(x,true()) -> true()
or(x,false()) -> x
equal(0(),0()) -> true()
equal(s(x),0()) -> false()
equal(0(),s(y)) -> false()
equal(s(x),s(y)) -> equal(x,y)
gt(0(),v) -> false()
gt(s(u),0()) -> true()
gt(s(u),s(v)) -> gt(u,v)
max(nil()) -> 0()
max(cons(u,l)) -> if(gt(u,max(l)),u,max(l))
if(true(),u,v) -> u
if(false(),u,v) -> v
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:
{ sort(l) -> st(0(), l)
, st(n, l) -> cond1(member(n, l), n, l)
, cond1(true(), n, l) -> cons(n, st(s(n), l))
, cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
, cond2(true(), n, l) -> nil()
, cond2(false(), n, l) -> st(s(n), l)
, member(n, nil()) -> false()
, member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
, or(x, true()) -> true()
, or(x, false()) -> x
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)
, gt(0(), v) -> false()
, gt(s(u), 0()) -> true()
, gt(s(u), s(v)) -> gt(u, v)
, max(nil()) -> 0()
, max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
, if(true(), u, v) -> u
, if(false(), u, v) -> v}
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:
{ sort(l) -> st(0(), l)
, st(n, l) -> cond1(member(n, l), n, l)
, cond1(true(), n, l) -> cons(n, st(s(n), l))
, cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
, cond2(true(), n, l) -> nil()
, cond2(false(), n, l) -> st(s(n), l)
, member(n, nil()) -> false()
, member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
, or(x, true()) -> true()
, or(x, false()) -> x
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)
, gt(0(), v) -> false()
, gt(s(u), 0()) -> true()
, gt(s(u), s(v)) -> gt(u, v)
, max(nil()) -> 0()
, max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
, if(true(), u, v) -> u
, if(false(), u, v) -> v}
Proof Output:
Computation stopped due to timeout after 60.0 seconds