MAYBE
96.27/29.75	MAYBE
96.27/29.75	
96.27/29.75	Problem:
96.27/29.75	 p(0(x1)) -> 0(s(s(p(x1))))
96.27/29.75	 p(s(x1)) -> x1
96.27/29.75	 p(p(s(x1))) -> p(x1)
96.27/29.75	 f(s(x1)) -> g(s(x1))
96.27/29.75	 g(x1) -> i(s(half(x1)))
96.27/29.75	 i(x1) -> f(p(x1))
96.27/29.75	 half(0(x1)) -> 0(s(s(half(x1))))
96.27/29.75	 half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
96.27/29.75	 0(x1) -> x1
96.27/29.75	 rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
96.27/29.75	
96.27/29.75	Proof:
96.27/29.75	 Open
96.27/29.75	EOF