0.00/0.32	YES
0.00/0.32	Proof: 
0.00/0.32	To show the infeasibility of the given CoCo INF problem, 
0.00/0.32	we transform the problem into a word problem by the split-if encoding (Claessen and Smallbone, 2018).
0.00/0.32	It suffices to show that the follwing ES does not entail true__ = false__ .
0.00/0.32	ES:
0.00/0.32	pin(a) = pout(b)
0.00/0.32	pin(b) = pout(c)
0.00/0.32	tc(x) = x
0.00/0.32	f1(pout(z),x,y) = tc(x)
0.00/0.32	f2(tc(z),x,y) = f1(pin(x),x,y)
0.00/0.32	f2(y,x,y) = y
0.00/0.32	f3(pout(z)) = true__
0.00/0.32	f4(tc(z),x1) = f3(pin(x1))
0.00/0.32	f4(x2,x1) = false__
0.00/0.32	f5(false__) = false__
0.00/0.32	f5(true__) = true__
0.00/0.32	
0.00/0.32	The ES admits the following equivalent ground-complete ordered rewrite system:
0.00/0.32	LPO with precedence: tc > f4 > f5 > f1 > f2 > c > b > pin > a > pout > true__ > f3 > false__ > z
0.00/0.32	ES:
0.00/0.32	f4(x201,x112) -> false__
0.00/0.32	f3(pin(x12)) -> false__
0.00/0.32	pout(b) -> pin(a)
0.00/0.32	pout(c) -> pin(b)
0.00/0.32	tc(x) -> x
0.00/0.32	f1(pout(z),x,y) -> x
0.00/0.32	f1(pin(x),x,y) -> f2(z,x,y)
0.00/0.32	f2(y,x,y) -> y
0.00/0.32	f3(pout(z)) -> true__
0.00/0.32	f5(false__) -> false__
0.00/0.32	f5(true__) -> true__
0.00/0.32	
0.00/0.32	Since true__ and false__ are not joinable,
0.00/0.32	the original problem is infeasible.
0.00/0.33	EOF