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