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(true()) -> false()
not(false()) -> true()
if(true(),x,y) -> x
if(false(),x,y) -> y
eq(#(),#()) -> true()
eq(#(),1(y)) -> false()
eq(1(x),#()) -> false()
eq(#(),0(y)) -> eq(#(),y)
eq(0(x),#()) -> eq(x,#())
eq(1(x),1(y)) -> eq(x,y)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(0(x),0(y)) -> eq(x,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(#(),0(x)) -> ge(#(),x)
ge(#(),1(x)) -> false()
log(x) -> -(log'(x),1(#()))
log'(#()) -> #()
log'(1(x)) -> +(log'(x),1(#()))
log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
*(#(),x) -> #()
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
*(*(x,y),z) -> *(x,*(y,z))
*(x,+(y,z)) -> +(*(x,y),*(x,z))
app(nil(),l) -> l
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
sum(nil()) -> 0(#())
sum(cons(x,l)) -> +(x,sum(l))
sum(app(l1,l2)) -> +(sum(l1),sum(l2))
prod(nil()) -> 1(#())
prod(cons(x,l)) -> *(x,prod(l))
prod(app(l1,l2)) -> *(prod(l1),prod(l2))
mem(x,nil()) -> false()
mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
inter(x,nil()) -> nil()
inter(nil(),x) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifinter(false(),x,l1,l2) -> inter(l1,l2)
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(true()) -> false()
, not(false()) -> true()
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(#(), #()) -> true()
, eq(#(), 1(y)) -> false()
, eq(1(x), #()) -> false()
, eq(#(), 0(y)) -> eq(#(), y)
, eq(0(x), #()) -> eq(x, #())
, eq(1(x), 1(y)) -> eq(x, y)
, eq(0(x), 1(y)) -> false()
, eq(1(x), 0(y)) -> false()
, eq(0(x), 0(y)) -> eq(x, 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(#(), 0(x)) -> ge(#(), x)
, ge(#(), 1(x)) -> false()
, log(x) -> -(log'(x), 1(#()))
, log'(#()) -> #()
, log'(1(x)) -> +(log'(x), 1(#()))
, log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #())
, *(#(), x) -> #()
, *(0(x), y) -> 0(*(x, y))
, *(1(x), y) -> +(0(*(x, y)), y)
, *(*(x, y), z) -> *(x, *(y, z))
, *(x, +(y, z)) -> +(*(x, y), *(x, z))
, app(nil(), l) -> l
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, sum(nil()) -> 0(#())
, sum(cons(x, l)) -> +(x, sum(l))
, sum(app(l1, l2)) -> +(sum(l1), sum(l2))
, prod(nil()) -> 1(#())
, prod(cons(x, l)) -> *(x, prod(l))
, prod(app(l1, l2)) -> *(prod(l1), prod(l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l))
, inter(x, nil()) -> nil()
, inter(nil(), x) -> nil()
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2)}
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(true()) -> false()
, not(false()) -> true()
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(#(), #()) -> true()
, eq(#(), 1(y)) -> false()
, eq(1(x), #()) -> false()
, eq(#(), 0(y)) -> eq(#(), y)
, eq(0(x), #()) -> eq(x, #())
, eq(1(x), 1(y)) -> eq(x, y)
, eq(0(x), 1(y)) -> false()
, eq(1(x), 0(y)) -> false()
, eq(0(x), 0(y)) -> eq(x, 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(#(), 0(x)) -> ge(#(), x)
, ge(#(), 1(x)) -> false()
, log(x) -> -(log'(x), 1(#()))
, log'(#()) -> #()
, log'(1(x)) -> +(log'(x), 1(#()))
, log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #())
, *(#(), x) -> #()
, *(0(x), y) -> 0(*(x, y))
, *(1(x), y) -> +(0(*(x, y)), y)
, *(*(x, y), z) -> *(x, *(y, z))
, *(x, +(y, z)) -> +(*(x, y), *(x, z))
, app(nil(), l) -> l
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, sum(nil()) -> 0(#())
, sum(cons(x, l)) -> +(x, sum(l))
, sum(app(l1, l2)) -> +(sum(l1), sum(l2))
, prod(nil()) -> 1(#())
, prod(cons(x, l)) -> *(x, prod(l))
, prod(app(l1, l2)) -> *(prod(l1), prod(l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l))
, inter(x, nil()) -> nil()
, inter(nil(), x) -> nil()
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2)}
Proof Output:
Computation stopped due to timeout after 60.0 seconds