MAYBE
0.08/0.19	MAYBE
0.18/0.20	
0.18/0.20	Problem:
0.18/0.20	 0(#()) -> #()
0.18/0.20	 +(#(),x) -> x
0.18/0.20	 +(x,#()) -> x
0.18/0.20	 +(0(x),0(y)) -> 0(+(x,y))
0.18/0.20	 +(0(x),1(y)) -> 1(+(x,y))
0.18/0.20	 +(1(x),0(y)) -> 1(+(x,y))
0.18/0.20	 +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
0.18/0.20	 +(+(x,y),z) -> +(x,+(y,z))
0.18/0.20	 -(#(),x) -> #()
0.18/0.20	 -(x,#()) -> x
0.18/0.20	 -(0(x),0(y)) -> 0(-(x,y))
0.18/0.20	 -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
0.18/0.20	 -(1(x),0(y)) -> 1(-(x,y))
0.18/0.20	 -(1(x),1(y)) -> 0(-(x,y))
0.18/0.20	 not(true()) -> false()
0.18/0.20	 not(false()) -> true()
0.18/0.20	 if(true(),x,y) -> x
0.18/0.20	 if(false(),x,y) -> y
0.18/0.20	 ge(0(x),0(y)) -> ge(x,y)
0.18/0.20	 ge(0(x),1(y)) -> not(ge(y,x))
0.18/0.20	 ge(1(x),0(y)) -> ge(x,y)
0.18/0.20	 ge(1(x),1(y)) -> ge(x,y)
0.18/0.20	 ge(x,#()) -> true()
0.18/0.20	 ge(#(),0(x)) -> ge(#(),x)
0.18/0.20	 ge(#(),1(x)) -> false()
0.18/0.20	 log(x) -> -(log'(x),1(#()))
0.18/0.20	 log'(#()) -> #()
0.18/0.20	 log'(1(x)) -> +(log'(x),1(#()))
0.18/0.20	 log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
0.18/0.20	
0.18/0.20	Proof:
0.18/0.20	 Open
0.18/0.20	EOF