MAYBE
210.24/59.86	MAYBE
210.24/59.86	
210.24/59.86	Problem:
210.24/59.86	 twoto(0(x1)) -> p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1))))))))))))))))
210.24/59.86	 twoto(s(x1)) ->
210.24/59.86	 p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))
210.24/59.86	 twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1)))))))))))))
210.24/59.86	 twice(s(x1)) -> s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1)))))))))))))))))))
210.24/59.86	 p(p(s(x1))) -> p(x1)
210.24/59.86	 p(s(x1)) -> x1
210.24/59.86	 p(0(x1)) -> 0(s(s(s(s(p(s(x1)))))))
210.24/59.86	 0(x1) -> x1
210.24/59.86	
210.24/59.86	Proof:
210.24/59.86	 Open
210.24/59.86	EOF