Tool CaT
stdout:
MAYBE
Problem:
0(#()) -> #()
+(x,#()) -> x
+(#(),x) -> x
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#())))
+(x,+(y,z)) -> +(+(x,y),z)
-(x,#()) -> x
-(#(),x) -> #()
-(0(x),0(y)) -> 0(-(x,y))
-(0(x),1(y)) -> 1(-(-(x,y),1(#())))
-(1(x),0(y)) -> 1(-(x,y))
-(1(x),1(y)) -> 0(-(x,y))
not(false()) -> true()
not(true()) -> false()
and(x,true()) -> x
and(x,false()) -> false()
if(true(),x,y) -> x
if(false(),x,y) -> y
ge(0(x),0(y)) -> ge(x,y)
ge(0(x),1(y)) -> not(ge(y,x))
ge(1(x),0(y)) -> ge(x,y)
ge(1(x),1(y)) -> ge(x,y)
ge(x,#()) -> true()
ge(#(),1(x)) -> false()
ge(#(),0(x)) -> ge(#(),x)
val(l(x)) -> x
val(n(x,y,z)) -> x
min(l(x)) -> x
min(n(x,y,z)) -> min(y)
max(l(x)) -> x
max(n(x,y,z)) -> max(z)
bs(l(x)) -> true()
bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
size(l(x)) -> 1(#())
size(n(x,y,z)) -> +(+(size(x),size(y)),1(#()))
wb(l(x)) -> true()
wb(n(x,y,z)) ->
and(if(ge(size(y),size(z)),ge(1(#()),-(size(y),size(z))),ge(1(#()),-(size(z),size(y)))),
and(wb(y),wb(z)))
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:
{ 0(#()) -> #()
, +(x, #()) -> x
, +(#(), x) -> x
, +(0(x), 0(y)) -> 0(+(x, y))
, +(0(x), 1(y)) -> 1(+(x, y))
, +(1(x), 0(y)) -> 1(+(x, y))
, +(1(x), 1(y)) -> 0(+(+(x, y), 1(#())))
, +(x, +(y, z)) -> +(+(x, y), z)
, -(x, #()) -> x
, -(#(), x) -> #()
, -(0(x), 0(y)) -> 0(-(x, y))
, -(0(x), 1(y)) -> 1(-(-(x, y), 1(#())))
, -(1(x), 0(y)) -> 1(-(x, y))
, -(1(x), 1(y)) -> 0(-(x, y))
, not(false()) -> true()
, not(true()) -> false()
, and(x, true()) -> x
, and(x, false()) -> false()
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, ge(0(x), 0(y)) -> ge(x, y)
, ge(0(x), 1(y)) -> not(ge(y, x))
, ge(1(x), 0(y)) -> ge(x, y)
, ge(1(x), 1(y)) -> ge(x, y)
, ge(x, #()) -> true()
, ge(#(), 1(x)) -> false()
, ge(#(), 0(x)) -> ge(#(), x)
, val(l(x)) -> x
, val(n(x, y, z)) -> x
, min(l(x)) -> x
, min(n(x, y, z)) -> min(y)
, max(l(x)) -> x
, max(n(x, y, z)) -> max(z)
, bs(l(x)) -> true()
, bs(n(x, y, z)) ->
and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))
, size(l(x)) -> 1(#())
, size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#()))
, wb(l(x)) -> true()
, wb(n(x, y, z)) ->
and(if(ge(size(y), size(z)),
ge(1(#()), -(size(y), size(z))),
ge(1(#()), -(size(z), size(y)))),
and(wb(y), wb(z)))}
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:
{ 0(#()) -> #()
, +(x, #()) -> x
, +(#(), x) -> x
, +(0(x), 0(y)) -> 0(+(x, y))
, +(0(x), 1(y)) -> 1(+(x, y))
, +(1(x), 0(y)) -> 1(+(x, y))
, +(1(x), 1(y)) -> 0(+(+(x, y), 1(#())))
, +(x, +(y, z)) -> +(+(x, y), z)
, -(x, #()) -> x
, -(#(), x) -> #()
, -(0(x), 0(y)) -> 0(-(x, y))
, -(0(x), 1(y)) -> 1(-(-(x, y), 1(#())))
, -(1(x), 0(y)) -> 1(-(x, y))
, -(1(x), 1(y)) -> 0(-(x, y))
, not(false()) -> true()
, not(true()) -> false()
, and(x, true()) -> x
, and(x, false()) -> false()
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, ge(0(x), 0(y)) -> ge(x, y)
, ge(0(x), 1(y)) -> not(ge(y, x))
, ge(1(x), 0(y)) -> ge(x, y)
, ge(1(x), 1(y)) -> ge(x, y)
, ge(x, #()) -> true()
, ge(#(), 1(x)) -> false()
, ge(#(), 0(x)) -> ge(#(), x)
, val(l(x)) -> x
, val(n(x, y, z)) -> x
, min(l(x)) -> x
, min(n(x, y, z)) -> min(y)
, max(l(x)) -> x
, max(n(x, y, z)) -> max(z)
, bs(l(x)) -> true()
, bs(n(x, y, z)) ->
and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))
, size(l(x)) -> 1(#())
, size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#()))
, wb(l(x)) -> true()
, wb(n(x, y, z)) ->
and(if(ge(size(y), size(z)),
ge(1(#()), -(size(y), size(z))),
ge(1(#()), -(size(z), size(y)))),
and(wb(y), wb(z)))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds