%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : COL027-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Fri Jul 15 00:36:56 EDT 2022 % Result : Unsatisfiable 20.23s 20.37s % Output : Proof 20.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : COL027-1 : TPTP v8.1.0. Released v1.0.0. % 0.07/0.12 % Command : moca.sh %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue May 31 15:53:13 EDT 2022 % 0.12/0.33 % CPUTime : % 20.23/20.37 % SZS status Unsatisfiable % 20.23/20.37 % SZS output start Proof % 20.23/20.37 The input problem is unsatisfiable because % 20.23/20.37 % 20.23/20.37 [1] the following set of Horn clauses is unsatisfiable: % 20.23/20.37 % 20.23/20.37 apply(apply(apply(b, X), Y), Z) = apply(X, apply(Y, Z)) % 20.23/20.37 apply(apply(apply(h, X), Y), Z) = apply(apply(apply(X, Y), Z), Y) % 20.23/20.37 Y = apply(combinator, Y) ==> \bottom % 20.23/20.37 % 20.23/20.37 This holds because % 20.23/20.37 % 20.23/20.37 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 20.23/20.37 % 20.23/20.37 E: % 20.23/20.37 apply(apply(apply(b, X), Y), Z) = apply(X, apply(Y, Z)) % 20.23/20.37 apply(apply(apply(h, X), Y), Z) = apply(apply(apply(X, Y), Z), Y) % 20.23/20.37 f1(Y, Y) = true__ % 20.23/20.37 f1(apply(combinator, Y), Y) = false__ % 20.23/20.37 G: % 20.23/20.37 true__ = false__ % 20.23/20.37 % 20.23/20.37 This holds because % 20.23/20.37 % 20.23/20.37 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 20.23/20.37 % 20.23/20.37 apply(X0, apply(apply(Y1, Y2), Y1)) = apply(apply(apply(h, apply(b, apply(b, X0))), Y1), Y2) % 20.23/20.37 apply(Y0, apply(X0, apply(X1, Y0))) = apply(apply(apply(h, b), Y0), apply(apply(b, X0), X1)) % 20.23/20.37 apply(Y0, apply(X0, apply(Y0, X0))) = apply(apply(apply(h, b), Y0), apply(apply(h, b), X0)) % 20.23/20.37 apply(Y1, apply(Y2, Y1)) = apply(apply(apply(h, b), Y1), Y2) % 20.23/20.37 apply(Y2, apply(b, Y2)) = apply(apply(apply(h, h), b), Y2) % 20.23/20.37 apply(apply(X0, apply(Y1, Y2)), Y1) = apply(apply(apply(h, apply(b, X0)), Y1), Y2) % 20.23/20.37 apply(apply(X0, apply(Y1, apply(b, X0))), Y1) = apply(apply(apply(h, h), apply(b, X0)), Y1) % 20.23/20.37 apply(apply(Y1, apply(Y2, Y1)), Y1) = apply(apply(apply(h, apply(h, b)), Y1), Y2) % 20.23/20.37 apply(apply(apply(Y1, Y2), Y1), Y2) = apply(apply(apply(h, h), Y1), Y2) % 20.23/20.37 apply(apply(apply(Y1, h), Y1), h) = apply(apply(apply(h, h), h), Y1) % 20.23/20.37 apply(apply(apply(apply(apply(h, h), h), b), Y1), Y2) = apply(apply(h, apply(Y1, Y2)), Y1) % 20.23/20.37 apply(apply(apply(apply(h, apply(h, b)), b), X1), Y2) = apply(apply(X1, b), apply(b, Y2)) % 20.23/20.37 apply(apply(apply(apply(h, apply(h, h)), b), h), Y2) = apply(apply(h, apply(b, Y2)), b) % 20.23/20.37 apply(apply(apply(apply(h, apply(h, h)), h), b), Y1) = apply(apply(h, apply(h, Y1)), h) % 20.23/20.37 apply(apply(apply(apply(h, h), apply(b, h)), b), Y2) = apply(h, apply(apply(b, Y2), b)) % 20.23/20.37 apply(apply(apply(h, X), Y), Z) = apply(apply(apply(X, Y), Z), Y) % 20.23/20.37 apply(apply(apply(h, apply(apply(h, h), h)), b), Y0) = apply(apply(h, apply(Y0, b)), Y0) % 20.23/20.37 apply(apply(apply(h, apply(h, apply(h, b))), b), Y0) = apply(apply(Y0, b), apply(b, b)) % 20.23/20.37 apply(apply(apply(h, apply(h, h)), Y1), Y2) = apply(apply(apply(h, apply(Y1, Y2)), Y1), Y2) % 20.23/20.37 apply(apply(apply(h, apply(h, h)), Y1), h) = apply(apply(apply(h, apply(Y1, h)), Y1), h) % 20.23/20.37 apply(apply(X0, apply(h, apply(b, X0))), h) -> apply(apply(apply(h, h), h), apply(b, X0)) % 20.23/20.37 apply(apply(Y1, apply(apply(h, b), Y1)), Y1) -> apply(apply(apply(h, h), apply(h, b)), Y1) % 20.23/20.37 apply(apply(Y2, apply(b, Y2)), b) -> apply(apply(apply(h, apply(h, h)), b), Y2) % 20.23/20.37 apply(apply(apply(apply(X0, Y1), Y2), Y1), Y1) -> apply(apply(apply(h, apply(h, X0)), Y1), Y2) % 20.23/20.37 apply(apply(apply(apply(apply(h, b), b), X1), Y1), Y2) -> apply(apply(X1, b), apply(Y1, Y2)) % 20.23/20.37 apply(apply(apply(apply(h, X0), Y2), Y1), Y1) -> apply(apply(apply(h, apply(X0, Y2)), Y1), Y2) % 20.23/20.37 apply(apply(apply(apply(h, apply(b, b)), Y1), X2), Y2) -> apply(apply(Y1, X2), apply(Y1, Y2)) % 20.23/20.37 apply(apply(apply(apply(h, apply(h, h)), b), b), Y2) -> apply(apply(b, b), apply(b, Y2)) % 20.23/20.37 apply(apply(apply(b, X), Y), Z) -> apply(X, apply(Y, Z)) % 20.23/20.37 apply(h, apply(b, h)) -> apply(apply(apply(h, h), h), b) % 20.23/20.37 f1(Y, Y) -> true__ % 20.23/20.37 f1(apply(apply(apply(h, apply(b, apply(b, combinator))), X1), X2), apply(apply(X1, X2), X1)) -> false__ % 20.23/20.37 f1(apply(apply(apply(h, b), combinator), X1), apply(X1, combinator)) -> false__ % 20.23/20.37 f1(apply(apply(apply(h, b), combinator), apply(apply(b, X0), X1)), apply(X0, apply(X1, combinator))) -> false__ % 20.23/20.37 f1(apply(apply(apply(h, b), combinator), apply(apply(h, b), X0)), apply(X0, apply(combinator, X0))) -> false__ % 20.23/20.37 f1(apply(combinator, Y), Y) -> false__ % 20.23/20.37 false__ -> true__ % 20.23/20.37 with the LPO induced by % 20.23/20.37 b > apply > h > combinator > f1 > false__ > true__ % 20.23/20.37 % 20.23/20.37 % SZS output end Proof % 20.23/20.37 %------------------------------------------------------------------------------