Tool CaT
stdout:
MAYBE
Problem:
app(nil(),k) -> k
app(l,nil()) -> l
app(cons(x,l),k) -> cons(x,app(l,k))
sum(cons(x,nil())) -> cons(x,nil())
sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
plus(zero(),y) -> y
plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
id(x) -> x
if(true(),x,y) -> x
if(false(),x,y) -> y
not(x) -> if(x,false(),true())
gt(s(x),zero()) -> true()
gt(zero(),y) -> false()
gt(s(x),s(y)) -> gt(x,y)
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:
{ app(nil(), k) -> k
, app(l, nil()) -> l
, app(cons(x, l), k) -> cons(x, app(l, k))
, sum(cons(x, nil())) -> cons(x, nil())
, sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
, sum(app(l, cons(x, cons(y, k)))) ->
sum(app(l, sum(cons(x, cons(y, k)))))
, plus(s(x), s(y)) ->
s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
, plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
, plus(zero(), y) -> y
, plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
, id(x) -> x
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, not(x) -> if(x, false(), true())
, gt(s(x), zero()) -> true()
, gt(zero(), y) -> false()
, gt(s(x), s(y)) -> gt(x, y)}
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:
{ app(nil(), k) -> k
, app(l, nil()) -> l
, app(cons(x, l), k) -> cons(x, app(l, k))
, sum(cons(x, nil())) -> cons(x, nil())
, sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
, sum(app(l, cons(x, cons(y, k)))) ->
sum(app(l, sum(cons(x, cons(y, k)))))
, plus(s(x), s(y)) ->
s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
, plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x))
, plus(zero(), y) -> y
, plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y))))
, id(x) -> x
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, not(x) -> if(x, false(), true())
, gt(s(x), zero()) -> true()
, gt(zero(), y) -> false()
, gt(s(x), s(y)) -> gt(x, y)}
Proof Output:
Computation stopped due to timeout after 60.0 seconds