MAYBE
0.08/0.19	MAYBE
0.08/0.19	
0.08/0.19	Problem:
0.08/0.19	 car(cons(x,l)) -> x
0.08/0.19	 cddr(nil()) -> nil()
0.08/0.19	 cddr(cons(x,nil())) -> nil()
0.08/0.19	 cddr(cons(x,cons(y,l))) -> l
0.08/0.19	 cadr(cons(x,cons(y,l))) -> y
0.08/0.19	 isZero(0()) -> true()
0.08/0.19	 isZero(s(x)) -> false()
0.08/0.19	 plus(x,y) -> ifplus(isZero(x),x,y)
0.08/0.19	 ifplus(true(),x,y) -> y
0.08/0.19	 ifplus(false(),x,y) -> s(plus(p(x),y))
0.08/0.19	 times(x,y) -> iftimes(isZero(x),x,y)
0.08/0.19	 iftimes(true(),x,y) -> 0()
0.08/0.19	 iftimes(false(),x,y) -> plus(y,times(p(x),y))
0.08/0.19	 p(s(x)) -> x
0.08/0.19	 p(0()) -> 0()
0.08/0.19	 shorter(nil(),y) -> true()
0.08/0.19	 shorter(cons(x,l),0()) -> false()
0.08/0.19	 shorter(cons(x,l),s(y)) -> shorter(l,y)
0.08/0.19	 prod(l) -> if(shorter(l,0()),shorter(l,s(0())),l)
0.08/0.19	 if(true(),b,l) -> s(0())
0.08/0.19	 if(false(),b,l) -> if2(b,l)
0.08/0.19	 if2(true(),l) -> car(l)
0.08/0.19	 if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))
0.08/0.19	
0.08/0.19	Proof:
0.08/0.19	 Open
0.08/0.19	EOF