MAYBE
176.43/56.46	MAYBE
176.43/56.46	
176.43/56.46	Problem:
176.43/56.46	 q(0(x1)) -> p(p(s(s(0(s(s(s(s(x1)))))))))
176.43/56.46	 q(s(x1)) -> p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
176.43/56.46	 r(0(x1)) -> p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
176.43/56.46	 r(s(x1)) -> p(s(p(s(s(q(p(s(p(s(x1))))))))))
176.43/56.46	 p(p(s(x1))) -> p(x1)
176.43/56.46	 p(s(x1)) -> x1
176.43/56.46	 p(0(x1)) -> 0(s(s(s(x1))))
176.43/56.46	
176.43/56.46	Proof:
176.43/56.46	 Open
176.43/56.48	EOF