0.00/0.03	YES
0.00/0.03	
0.00/0.03	proof:
0.00/0.03	The input problem is infeasible because
0.00/0.03	
0.00/0.03	[1] the following set of Horn clauses is satisfiable:
0.00/0.03	
0.00/0.03		x = a ==> f(x) = a
0.00/0.03		x = b ==> f(x) = b
0.00/0.03		x = a & x = b ==> true__ = false__
0.00/0.03		true__ = false__ ==> \bottom
0.00/0.03	
0.00/0.03	This holds because
0.00/0.03	
0.00/0.03	[2] the following E does not entail the following G (Claessen-Smallbone's transformation (2018)):
0.00/0.03	
0.00/0.03	E:
0.00/0.03		f(a) = a
0.00/0.03		f(b) = b
0.00/0.03		f1(a) = true__
0.00/0.03		f1(b) = false__
0.00/0.03		f2(false__) = true__
0.00/0.03		f2(true__) = false__
0.00/0.03	G:
0.00/0.03		true__ = false__
0.00/0.03	
0.00/0.03	This holds because
0.00/0.03	
0.00/0.03	[3] the following ground-complete ordered TRS entails E but does not entail G:
0.00/0.03	
0.00/0.03		f(a) -> a
0.00/0.03		f(b) -> b
0.00/0.03		f1(a) -> true__
0.00/0.03		f1(b) -> false__
0.00/0.03		f2(false__) -> true__
0.00/0.03		f2(true__) -> false__
0.00/0.03	with the LPO induced by
0.00/0.03		f2 > f1 > b > a > f > false__ > true__
0.00/0.03	
0.00/0.04	EOF