%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : MSC015-1.005 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n020.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 : Sun Jul 17 22:54:55 EDT 2022 % Result : Unsatisfiable 4.02s 4.06s % Output : Proof 4.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : MSC015-1.005 : TPTP v8.1.0. Released v3.5.0. % 0.11/0.12 % Command : moca.sh %s % 0.12/0.33 % Computer : n020.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 : Fri Jul 1 16:10:30 EDT 2022 % 0.12/0.33 % CPUTime : % 4.02/4.06 % SZS status Unsatisfiable % 4.02/4.06 % SZS output start Proof % 4.02/4.06 The input problem is unsatisfiable because % 4.02/4.06 % 4.02/4.06 [1] the following set of Horn clauses is unsatisfiable: % 4.02/4.06 % 4.02/4.06 p(s0, s0, s0, s0, s0) % 4.02/4.06 p(X0, X1, X2, X3, s0) ==> p(X0, X1, X2, X3, s1) % 4.02/4.06 p(X0, X1, X2, s0, s1) ==> p(X0, X1, X2, s1, s0) % 4.02/4.06 p(X0, X1, s0, s1, s1) ==> p(X0, X1, s1, s0, s0) % 4.02/4.06 p(X0, s0, s1, s1, s1) ==> p(X0, s1, s0, s0, s0) % 4.02/4.06 p(s0, s1, s1, s1, s1) ==> p(s1, s0, s0, s0, s0) % 4.02/4.06 p(s1, s1, s1, s1, s1) ==> \bottom % 4.02/4.06 % 4.02/4.06 This holds because % 4.02/4.06 % 4.02/4.06 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 4.02/4.06 % 4.02/4.06 E: % 4.02/4.06 f1(p(X0, X1, X2, X3, s0), X0, X1, X2, X3) = true__ % 4.02/4.06 f1(true__, X0, X1, X2, X3) = p(X0, X1, X2, X3, s1) % 4.02/4.06 f2(p(X0, X1, X2, s0, s1), X0, X1, X2) = true__ % 4.02/4.06 f2(true__, X0, X1, X2) = p(X0, X1, X2, s1, s0) % 4.02/4.06 f3(p(X0, X1, s0, s1, s1), X0, X1) = true__ % 4.02/4.06 f3(true__, X0, X1) = p(X0, X1, s1, s0, s0) % 4.02/4.06 f4(p(X0, s0, s1, s1, s1), X0) = true__ % 4.02/4.06 f4(true__, X0) = p(X0, s1, s0, s0, s0) % 4.02/4.06 f5(p(s0, s1, s1, s1, s1)) = true__ % 4.02/4.06 f5(true__) = p(s1, s0, s0, s0, s0) % 4.02/4.06 f6(p(s1, s1, s1, s1, s1)) = true__ % 4.02/4.06 f6(true__) = false__ % 4.02/4.06 p(s0, s0, s0, s0, s0) = true__ % 4.02/4.06 G: % 4.02/4.06 true__ = false__ % 4.02/4.06 % 4.02/4.06 This holds because % 4.02/4.06 % 4.02/4.06 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 4.02/4.06 % 4.02/4.06 % 4.02/4.06 f1(f2(true__, Y0, Y1, Y2), Y0, Y1, Y2, s1) -> true__ % 4.02/4.06 f1(f3(true__, Y0, Y1), Y0, Y1, s1, s0) -> true__ % 4.02/4.06 f1(f4(true__, Y0), Y0, s1, s0, s0) -> true__ % 4.02/4.06 f1(f5(true__), s1, s0, s0, s0) -> true__ % 4.02/4.06 f1(p(X0, X1, X2, X3, s0), X0, X1, X2, X3) -> true__ % 4.02/4.06 f1(true__, X0, X1, X2, X3) -> p(X0, X1, X2, X3, s1) % 4.02/4.06 f2(p(X0, X1, X2, s0, s1), X0, X1, X2) -> true__ % 4.02/4.06 f2(true__, s0, s0, s0) -> true__ % 4.02/4.06 f2(true__, s0, s0, s1) -> true__ % 4.02/4.06 f2(true__, s0, s1, s0) -> true__ % 4.02/4.06 f2(true__, s0, s1, s1) -> true__ % 4.02/4.06 f2(true__, s1, s0, s0) -> true__ % 4.02/4.06 f2(true__, s1, s0, s1) -> true__ % 4.02/4.06 f2(true__, s1, s1, s0) -> true__ % 4.02/4.06 f2(true__, s1, s1, s1) -> true__ % 4.02/4.06 f3(p(X0, X1, s0, s1, s1), X0, X1) -> true__ % 4.02/4.06 f3(true__, s0, s0) -> true__ % 4.02/4.06 f3(true__, s0, s1) -> true__ % 4.02/4.06 f3(true__, s1, s0) -> true__ % 4.02/4.06 f3(true__, s1, s1) -> true__ % 4.02/4.06 f4(p(X0, s0, s1, s1, s1), X0) -> true__ % 4.02/4.07 f4(true__, s0) -> true__ % 4.02/4.07 f4(true__, s1) -> true__ % 4.02/4.07 f5(p(s0, s1, s1, s1, s1)) -> true__ % 4.02/4.07 f5(true__) -> true__ % 4.02/4.07 f6(p(s1, s1, s1, s1, s1)) -> true__ % 4.02/4.07 f6(true__) -> false__ % 4.02/4.07 false__ -> true__ % 4.02/4.07 p(X0, X1, X2, s1, s0) -> f2(true__, X0, X1, X2) % 4.02/4.07 p(X0, X1, s1, s0, s0) -> f3(true__, X0, X1) % 4.02/4.07 p(X0, s1, s0, s0, s0) -> f4(true__, X0) % 4.02/4.07 p(s0, s0, s0, s0, s0) -> true__ % 4.02/4.07 p(s0, s0, s0, s0, s1) -> true__ % 4.02/4.07 p(s0, s0, s0, s1, s1) -> true__ % 4.02/4.07 p(s0, s0, s1, s0, s1) -> true__ % 4.02/4.07 p(s0, s0, s1, s1, s1) -> true__ % 4.02/4.07 p(s0, s1, s0, s0, s1) -> true__ % 4.02/4.07 p(s0, s1, s0, s1, s1) -> true__ % 4.02/4.07 p(s0, s1, s1, s0, s1) -> true__ % 4.02/4.07 p(s0, s1, s1, s1, s1) -> true__ % 4.02/4.07 p(s1, s0, s0, s0, s0) -> f5(true__) % 4.02/4.07 p(s1, s0, s0, s0, s1) -> true__ % 4.02/4.07 p(s1, s0, s0, s1, s1) -> true__ % 4.02/4.07 p(s1, s0, s1, s0, s1) -> true__ % 4.02/4.07 p(s1, s0, s1, s1, s1) -> true__ % 4.02/4.07 p(s1, s1, s0, s0, s1) -> true__ % 4.02/4.07 p(s1, s1, s0, s1, s1) -> true__ % 4.02/4.07 p(s1, s1, s1, s0, s1) -> true__ % 4.02/4.07 p(s1, s1, s1, s1, s1) -> true__ % 4.02/4.07 with the LPO induced by % 4.02/4.07 f6 > f1 > p > f5 > f2 > f3 > f4 > s1 > s0 > false__ > true__ % 4.02/4.07 % 4.02/4.07 % SZS output end Proof % 4.02/4.07 %------------------------------------------------------------------------------