0.79/0.99	YES
0.79/0.99	Proof: 
0.79/0.99	To show the infeasibility of the given CoCo INF problem, 
0.79/0.99	we transform the problem into a word problem by the split-if encoding (Claessen and Smallbone, 2018).
0.79/0.99	It suffices to show that the follwing ES does not entail true__ = false__ .
0.79/0.99	ES:
0.79/0.99	f1(c(a(b())), x, y) = f(c(x), c(c(y)))
0.79/0.99	f1(c(f(x, y)), x, y) = a(a(x))
0.79/0.99	f2(c(a(a(b()))), x, y) = f(c(c(c(x))), y)
0.79/0.99	f2(c(f(c(x), c(c(y)))), x, y) = a(y)
0.79/0.99	h(b()) = b()
0.79/0.99	f3(b(), x) = h(a(a(x)))
0.79/0.99	f3(h(x), x) = a(b())
0.79/0.99	f4(c(a(b()))) = true__()
0.79/0.99	f5(c(a(a(b()))), x1, y) = f4(c(f(c(c(x1)), y)))
0.79/0.99	f5(c(f(c(x1), c(c(c(c(y)))))), x1, y) = false__()
0.79/0.99	f6(false__()) = false__()
0.79/0.99	f6(true__()) = true__()
0.79/0.99	The ES admits the following equivalent ground-complete ordered rewrite system:
0.79/0.99	LPO with precedence: f5 > f2 > f1 > f > h > a > f3 > true__ > c > f4 > f6 > b > false__
0.79/0.99	ES:
0.79/0.99	f5(c(f(c(X3), c(c(c(c(X1)))))), X3, X1) -> false__()
0.79/0.99	f2(c(f(c(X2), c(c(X3)))), X2, X3) -> a(X3)
0.79/0.99	f1(c(f(X0, X1)), X0, X1) -> a(a(X0))
0.79/0.99	h(b()) -> b()
0.79/0.99	h(a(a(X0))) -> f3(b(), X0)
0.79/0.99	f3(h(X0), X0) -> f3(b(), b())
0.79/0.99	f5(c(a(f3(b(), b()))), X2, X1) -> f4(c(f(c(c(X2)), X1)))
0.79/0.99	f6(false__()) -> false__()
0.79/0.99	f6(true__()) -> true__()
0.79/0.99	a(b()) -> f3(b(), b())
0.79/0.99	f5(c(a(f3(b(), b()))), X2, c(c(X4))) -> f4(c(f(c(c(X2)), c(c(X4)))))
0.79/0.99	f3(f3(b(), b()), a(f3(b(), b()))) -> f3(b(), b())
0.79/0.99	f4(c(f3(b(), b()))) -> true__()
0.79/0.99	h(a(f3(b(), b()))) -> f3(b(), b())
0.79/0.99	f3(f3(b(), X1), a(a(X1))) -> f3(b(), b())
0.79/0.99	f1(c(f3(b(), b())), X0, X1) -> f(c(X0), c(c(X1)))
0.79/0.99	f2(c(a(f3(b(), b()))), X0, X1) -> f(c(c(c(X0))), X1)
0.79/0.99	
0.79/0.99	Since true__ and false__ are not joinable,
0.79/0.99	the original problem is infeasible.
0.79/0.99	EOF