2.22/1.18	NO
2.22/1.18	proof: 
2.22/1.18	  Conditions are not infeasible.
2.22/1.18	  There are some non-trivial conditions.
2.22/1.18	  Call external tool:
2.22/1.18	./nonreach.sh
2.22/1.18	Variables:
2.22/1.18	x
2.22/1.18	Input:
2.22/1.18	  s(p(x)) -> x
2.22/1.18	  p(s(x)) -> x
2.22/1.18	  pos(0) -> false
2.22/1.18	  pos(s(0)) -> true
2.22/1.18	  pos(s(x)) -> true <= pos(x) = true
2.22/1.18	  pos(p(x)) -> false <= pos(x) = false
2.22/1.18	
2.22/1.18	Condition: pos(p(x)) = true
2.22/1.18	By external nonreachability tool.
2.22/1.18	NO
2.22/1.18	FEASIBLE with
2.22/1.18	{x/s(s(0()))}
2.22/1.19	EOF