MAYBE
237.69/60.28	MAYBE
237.69/60.28	
237.69/60.28	Problem:
237.69/60.28	 p(0(x1)) -> 0(s(s(p(x1))))
237.69/60.28	 p(s(x1)) -> x1
237.69/60.28	 p(p(s(x1))) -> p(x1)
237.69/60.28	 f(s(x1)) -> p(s(g(p(s(s(x1))))))
237.69/60.28	 g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
237.69/60.28	 j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
237.69/60.28	 half(0(x1)) -> 0(s(s(half(p(s(p(s(x1))))))))
237.69/60.28	 half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
237.69/60.28	 rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(x1)))))))))
237.69/60.28	
237.69/60.28	Proof:
237.69/60.28	 Open
237.69/60.28	EOF