MAYBE
0.08/0.19	MAYBE
0.08/0.19	
0.08/0.19	Problem:
0.08/0.19	 times(x,y) -> sum(generate(x,y))
0.08/0.19	 generate(x,y) -> gen(x,y,0())
0.08/0.19	 gen(x,y,z) -> if(ge(z,x),x,y,z)
0.08/0.19	 if(true(),x,y,z) -> nil()
0.08/0.19	 if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
0.08/0.19	 sum(xs) -> sum2(xs,0())
0.08/0.19	 sum2(xs,y) -> ifsum(isNil(xs),isZero(head(xs)),xs,y)
0.08/0.19	 ifsum(true(),b,xs,y) -> y
0.08/0.19	 ifsum(false(),b,xs,y) -> ifsum2(b,xs,y)
0.08/0.19	 ifsum2(true(),xs,y) -> sum2(tail(xs),y)
0.08/0.19	 ifsum2(false(),xs,y) -> sum2(cons(p(head(xs)),tail(xs)),s(y))
0.08/0.19	 isNil(nil()) -> true()
0.08/0.19	 isNil(cons(x,xs)) -> false()
0.08/0.19	 tail(nil()) -> nil()
0.08/0.19	 tail(cons(x,xs)) -> xs
0.08/0.19	 head(cons(x,xs)) -> x
0.08/0.19	 head(nil()) -> error()
0.08/0.19	 isZero(0()) -> true()
0.08/0.19	 isZero(s(0())) -> false()
0.08/0.19	 isZero(s(s(x))) -> isZero(s(x))
0.08/0.19	 p(0()) -> s(s(0()))
0.08/0.19	 p(s(0())) -> 0()
0.08/0.19	 p(s(s(x))) -> s(p(s(x)))
0.08/0.19	 ge(x,0()) -> true()
0.08/0.19	 ge(0(),s(y)) -> false()
0.08/0.19	 ge(s(x),s(y)) -> ge(x,y)
0.08/0.19	 a() -> c()
0.08/0.19	 a() -> d()
0.08/0.19	
0.08/0.19	Proof:
0.08/0.19	 Open
0.08/0.19	EOF