MAYBE
222.98/58.74	MAYBE
222.98/58.74	
222.98/58.74	Problem:
222.98/58.74	 thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
222.98/58.74	 thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
222.98/58.74	 half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
222.98/58.74	 half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
222.98/58.74	 half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
222.98/58.74	 sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
222.98/58.74	 sixtimes(s(x1)) ->
222.98/58.74	 p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
222.98/58.74	 p(p(s(x1))) -> p(x1)
222.98/58.74	 p(s(x1)) -> x1
222.98/58.74	 p(0(x1)) -> 0(s(s(s(s(x1)))))
222.98/58.74	 0(x1) -> x1
222.98/58.74	
222.98/58.74	Proof:
222.98/58.74	 Open
222.98/58.74	EOF