%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : SYN095-1.002 : TPTP v8.1.0. Bugfixed v1.2.1. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n012.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 : Thu Jul 21 09:13:51 EDT 2022 % Result : Unsatisfiable 1.78s 1.93s % Output : Proof 1.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SYN095-1.002 : TPTP v8.1.0. Bugfixed v1.2.1. % 0.11/0.12 % Command : moca.sh %s % 0.11/0.33 % Computer : n012.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Tue Jul 12 05:38:57 EDT 2022 % 0.11/0.33 % CPUTime : % 1.78/1.93 % SZS status Unsatisfiable % 1.78/1.93 % SZS output start Proof % 1.78/1.93 The input problem is unsatisfiable because % 1.78/1.93 % 1.78/1.93 [1] the following set of Horn clauses is unsatisfiable: % 1.78/1.93 % 1.78/1.93 p_1_2(X) ==> \bottom % 1.78/1.93 p_2_2(X) & p_1_1(X) ==> p_1_2(X) % 1.78/1.93 q_2_2(X) & q_1_1(X) ==> p_1_2(X) % 1.78/1.93 p_2_2(X) & q_1_1(X) ==> q_1_2(X) % 1.78/1.93 q_2_2(X) & p_1_1(X) ==> q_1_2(X) % 1.78/1.93 p_1_2(X) ==> p_1_1(X) % 1.78/1.93 q_1_2(X) ==> q_1_1(X) % 1.78/1.93 p_1_2(X) ==> p_2_2(X) % 1.78/1.93 q_1_2(X) ==> q_2_2(X) % 1.78/1.93 p_1_1(a) % 1.78/1.93 q_1_1(a) % 1.78/1.93 p_2_2(a) % 1.78/1.93 q_2_2(a) % 1.78/1.93 % 1.78/1.93 This holds because % 1.78/1.93 % 1.78/1.93 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 1.78/1.93 % 1.78/1.93 E: % 1.78/1.93 f1(p_1_2(X)) = true__ % 1.78/1.93 f1(true__) = false__ % 1.78/1.93 f10(p_1_2(X), X) = true__ % 1.78/1.93 f10(true__, X) = p_1_1(X) % 1.78/1.93 f11(q_1_2(X), X) = true__ % 1.78/1.93 f11(true__, X) = q_1_1(X) % 1.78/1.93 f12(p_1_2(X), X) = true__ % 1.78/1.93 f12(true__, X) = p_2_2(X) % 1.78/1.93 f13(q_1_2(X), X) = true__ % 1.78/1.93 f13(true__, X) = q_2_2(X) % 1.78/1.93 f2(true__, X) = p_1_2(X) % 1.78/1.93 f3(p_1_1(X), X) = true__ % 1.78/1.93 f3(true__, X) = f2(p_2_2(X), X) % 1.78/1.93 f4(true__, X) = p_1_2(X) % 1.78/1.93 f5(q_1_1(X), X) = true__ % 1.78/1.93 f5(true__, X) = f4(q_2_2(X), X) % 1.78/1.93 f6(true__, X) = q_1_2(X) % 1.78/1.93 f7(q_1_1(X), X) = true__ % 1.78/1.93 f7(true__, X) = f6(p_2_2(X), X) % 1.78/1.93 f8(true__, X) = q_1_2(X) % 1.78/1.93 f9(p_1_1(X), X) = true__ % 1.78/1.93 f9(true__, X) = f8(q_2_2(X), X) % 1.78/1.93 p_1_1(a) = true__ % 1.78/1.93 p_2_2(a) = true__ % 1.78/1.93 q_1_1(a) = true__ % 1.78/1.93 q_2_2(a) = true__ % 1.78/1.93 G: % 1.78/1.93 true__ = false__ % 1.78/1.93 % 1.78/1.93 This holds because % 1.78/1.93 % 1.78/1.93 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 1.78/1.93 % 1.78/1.93 % 1.78/1.93 f1(f2(true__, Y0)) -> true__ % 1.78/1.93 f1(p_1_2(X)) -> true__ % 1.78/1.93 f1(true__) -> false__ % 1.78/1.93 f10(f2(true__, Y0), Y0) -> true__ % 1.78/1.93 f10(p_1_2(X), X) -> true__ % 1.78/1.93 f10(true__, a) -> true__ % 1.78/1.93 f11(f6(true__, Y0), Y0) -> true__ % 1.78/1.93 f11(q_1_2(X), X) -> true__ % 1.78/1.93 f11(true__, X) -> q_1_1(X) % 1.78/1.93 f12(f2(true__, Y0), Y0) -> true__ % 1.78/1.93 f12(p_1_2(X), X) -> true__ % 1.78/1.93 f12(true__, a) -> true__ % 1.78/1.93 f13(f6(true__, Y0), Y0) -> true__ % 1.78/1.93 f13(q_1_2(X), X) -> true__ % 1.78/1.93 f13(true__, a) -> true__ % 1.78/1.93 f2(f12(true__, a), a) -> true__ % 1.78/1.93 f2(true__, a) -> true__ % 1.78/1.93 f3(f10(true__, Y0), Y0) -> true__ % 1.78/1.93 f3(p_1_1(X), X) -> true__ % 1.78/1.93 f3(true__, X) -> f2(p_2_2(X), X) % 1.78/1.93 f4(f13(true__, a), a) -> true__ % 1.78/1.93 f4(true__, X) -> p_1_2(X) % 1.78/1.93 f5(q_1_1(X), X) -> true__ % 1.78/1.93 f5(true__, X) -> f4(q_2_2(X), X) % 1.78/1.93 f6(f12(true__, a), a) -> true__ % 1.78/1.93 f6(true__, a) -> true__ % 1.78/1.93 f7(q_1_1(X), X) -> true__ % 1.78/1.93 f7(true__, X) -> f6(p_2_2(X), X) % 1.78/1.93 f8(f13(true__, a), a) -> true__ % 1.78/1.93 f8(true__, X) -> q_1_2(X) % 1.78/1.93 f9(f10(true__, Y0), Y0) -> true__ % 1.78/1.93 f9(p_1_1(X), X) -> true__ % 1.78/1.93 f9(true__, X) -> f8(q_2_2(X), X) % 1.78/1.93 false__ -> true__ % 1.78/1.93 p_1_1(X) -> f10(true__, X) % 1.78/1.93 p_1_1(a) -> true__ % 1.78/1.93 p_1_2(X) -> f2(true__, X) % 1.78/1.93 p_2_2(X) -> f12(true__, X) % 1.78/1.93 p_2_2(a) -> true__ % 1.78/1.93 q_1_1(a) -> true__ % 1.78/1.93 q_1_2(X) -> f6(true__, X) % 1.78/1.93 q_2_2(X) -> f13(true__, X) % 1.78/1.93 q_2_2(a) -> true__ % 1.78/1.93 with the LPO induced by % 1.78/1.93 a > f9 > p_1_1 > f10 > f5 > q_2_2 > f13 > f7 > f3 > f4 > p_1_2 > f2 > p_2_2 > f12 > f11 > f8 > q_1_2 > f6 > q_1_1 > f1 > false__ > true__ % 1.78/1.93 % 1.78/1.93 % SZS output end Proof % 1.78/1.93 %------------------------------------------------------------------------------