%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : SYN088-1.010 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n023.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:49 EDT 2022 % Result : Unsatisfiable 1.97s 2.09s % Output : Proof 1.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SYN088-1.010 : TPTP v8.1.0. Released v1.0.0. % 0.10/0.12 % Command : moca.sh %s % 0.11/0.33 % Computer : n023.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 08:50:24 EDT 2022 % 0.11/0.33 % CPUTime : % 1.97/2.09 % SZS status Unsatisfiable % 1.97/2.09 % SZS output start Proof % 1.97/2.09 The input problem is unsatisfiable because % 1.97/2.09 % 1.97/2.09 [1] the following set of Horn clauses is unsatisfiable: % 1.97/2.09 % 1.97/2.09 p(a, a, a, a, a, a, a, a, a, a) ==> \bottom % 1.97/2.09 q_1(X_1) & q_2(X_2) & q_3(X_3) & q_4(X_4) & q_5(X_5) & q_6(X_6) & q_7(X_7) & q_8(X_8) & q_9(X_9) & q_10(X_10) ==> p(X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 q_1(a) % 1.97/2.09 q_1(b) % 1.97/2.09 q_2(a) % 1.97/2.09 q_2(b) % 1.97/2.09 q_3(a) % 1.97/2.09 q_3(b) % 1.97/2.09 q_4(a) % 1.97/2.09 q_4(b) % 1.97/2.09 q_5(a) % 1.97/2.09 q_5(b) % 1.97/2.09 q_6(a) % 1.97/2.09 q_6(b) % 1.97/2.09 q_7(a) % 1.97/2.09 q_7(b) % 1.97/2.09 q_8(a) % 1.97/2.09 q_8(b) % 1.97/2.09 q_9(a) % 1.97/2.09 q_9(b) % 1.97/2.09 q_10(a) % 1.97/2.09 q_10(b) % 1.97/2.09 % 1.97/2.09 This holds because % 1.97/2.09 % 1.97/2.09 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 1.97/2.09 % 1.97/2.09 E: % 1.97/2.09 f1(p(a, a, a, a, a, a, a, a, a, a)) = true__ % 1.97/2.09 f1(true__) = false__ % 1.97/2.09 f10(true__, X_8, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_9, X_10) = f9(q_8(X_8), X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_8, X_9, X_10) % 1.97/2.09 f11(q_10(X_10), X_9, X_8, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_10) = true__ % 1.97/2.09 f11(true__, X_9, X_8, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_10) = f10(q_9(X_9), X_8, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_9, X_10) % 1.97/2.09 f2(true__, X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) = p(X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f3(true__, X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) = f2(q_1(X_1), X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f4(true__, X_2, X_1, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) = f3(q_2(X_2), X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f5(true__, X_3, X_2, X_1, X_4, X_5, X_6, X_7, X_8, X_9, X_10) = f4(q_3(X_3), X_2, X_1, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f6(true__, X_4, X_3, X_2, X_1, X_5, X_6, X_7, X_8, X_9, X_10) = f5(q_4(X_4), X_3, X_2, X_1, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f7(true__, X_5, X_4, X_3, X_2, X_1, X_6, X_7, X_8, X_9, X_10) = f6(q_5(X_5), X_4, X_3, X_2, X_1, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f8(true__, X_6, X_5, X_4, X_3, X_2, X_1, X_7, X_8, X_9, X_10) = f7(q_6(X_6), X_5, X_4, X_3, X_2, X_1, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f9(true__, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_8, X_9, X_10) = f8(q_7(X_7), X_6, X_5, X_4, X_3, X_2, X_1, X_7, X_8, X_9, X_10) % 1.97/2.09 q_1(a) = true__ % 1.97/2.09 q_1(b) = true__ % 1.97/2.09 q_10(a) = true__ % 1.97/2.09 q_10(b) = true__ % 1.97/2.09 q_2(a) = true__ % 1.97/2.09 q_2(b) = true__ % 1.97/2.09 q_3(a) = true__ % 1.97/2.09 q_3(b) = true__ % 1.97/2.09 q_4(a) = true__ % 1.97/2.09 q_4(b) = true__ % 1.97/2.09 q_5(a) = true__ % 1.97/2.09 q_5(b) = true__ % 1.97/2.09 q_6(a) = true__ % 1.97/2.09 q_6(b) = true__ % 1.97/2.09 q_7(a) = true__ % 1.97/2.09 q_7(b) = true__ % 1.97/2.09 q_8(a) = true__ % 1.97/2.09 q_8(b) = true__ % 1.97/2.09 q_9(a) = true__ % 1.97/2.09 q_9(b) = true__ % 1.97/2.09 G: % 1.97/2.09 true__ = false__ % 1.97/2.09 % 1.97/2.09 This holds because % 1.97/2.09 % 1.97/2.09 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 1.97/2.09 % 1.97/2.09 % 1.97/2.09 f1(f6(true__, a, a, a, a, a, a, a, a, a, a)) -> true__ % 1.97/2.09 f1(f8(true__, a, a, a, a, a, a, a, a, a, a)) -> true__ % 1.97/2.09 f1(p(a, a, a, a, a, a, a, a, a, a)) -> true__ % 1.97/2.09 f1(true__) -> false__ % 1.97/2.09 f10(q_9(X_9), X_8, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_9, X_10) -> f11(true__, X_9, X_8, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_10) % 1.97/2.09 f10(true__, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, a, Y9) -> f11(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f10(true__, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, b, Y9) -> f11(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f11(q_10(X_10), X_9, X_8, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_10) -> true__ % 1.97/2.09 f11(true__, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, a) -> true__ % 1.97/2.09 f11(true__, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, b) -> true__ % 1.97/2.09 f2(q_1(X_1), X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) -> f3(true__, X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f2(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) -> f3(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f2(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) -> f3(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f3(q_2(X_2), X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) -> f4(true__, X_2, X_1, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f3(true__, Y1, a, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) -> f4(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f3(true__, Y1, b, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) -> f4(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f4(q_3(X_3), X_2, X_1, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) -> f5(true__, X_3, X_2, X_1, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f4(true__, Y1, Y2, a, Y3, Y4, Y5, Y6, Y7, Y8, Y9) -> f5(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f4(true__, Y1, Y2, b, Y3, Y4, Y5, Y6, Y7, Y8, Y9) -> f5(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f5(q_4(X_4), X_3, X_2, X_1, X_4, X_5, X_6, X_7, X_8, X_9, X_10) -> f6(true__, X_4, X_3, X_2, X_1, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f5(true__, Y1, Y2, Y3, a, Y4, Y5, Y6, Y7, Y8, Y9) -> f6(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f5(true__, Y1, Y2, Y3, b, Y4, Y5, Y6, Y7, Y8, Y9) -> f6(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f6(q_5(X_5), X_4, X_3, X_2, X_1, X_5, X_6, X_7, X_8, X_9, X_10) -> f7(true__, X_5, X_4, X_3, X_2, X_1, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 f6(true__, Y1, Y2, Y3, Y4, a, Y5, Y6, Y7, Y8, Y9) -> f7(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f6(true__, Y1, Y2, Y3, Y4, b, Y5, Y6, Y7, Y8, Y9) -> f7(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f7(q_6(X_6), X_5, X_4, X_3, X_2, X_1, X_6, X_7, X_8, X_9, X_10) -> f8(true__, X_6, X_5, X_4, X_3, X_2, X_1, X_7, X_8, X_9, X_10) % 1.97/2.09 f7(true__, Y1, Y2, Y3, Y4, Y5, a, Y6, Y7, Y8, Y9) -> f8(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f7(true__, Y1, Y2, Y3, Y4, Y5, b, Y6, Y7, Y8, Y9) -> f8(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f8(q_7(X_7), X_6, X_5, X_4, X_3, X_2, X_1, X_7, X_8, X_9, X_10) -> f9(true__, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_8, X_9, X_10) % 1.97/2.09 f8(true__, Y1, Y2, Y3, Y4, Y5, Y6, a, Y7, Y8, Y9) -> f9(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f8(true__, Y1, Y2, Y3, Y4, Y5, Y6, b, Y7, Y8, Y9) -> f9(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f9(q_8(X_8), X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_8, X_9, X_10) -> f10(true__, X_8, X_7, X_6, X_5, X_4, X_3, X_2, X_1, X_9, X_10) % 1.97/2.09 f9(true__, Y1, Y2, Y3, Y4, Y5, Y6, Y7, a, Y8, Y9) -> f10(true__, a, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 f9(true__, Y1, Y2, Y3, Y4, Y5, Y6, Y7, b, Y8, Y9) -> f10(true__, b, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9) % 1.97/2.09 false__ -> true__ % 1.97/2.09 p(X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) -> f2(true__, X_1, X_2, X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_10) % 1.97/2.09 q_1(a) -> true__ % 1.97/2.09 q_1(b) -> true__ % 1.97/2.09 q_10(a) -> true__ % 1.97/2.09 q_10(b) -> true__ % 1.97/2.09 q_2(a) -> true__ % 1.97/2.09 q_2(b) -> true__ % 1.97/2.09 q_3(a) -> true__ % 1.97/2.09 q_3(b) -> true__ % 1.97/2.09 q_4(a) -> true__ % 1.97/2.09 q_4(b) -> true__ % 1.97/2.09 q_5(a) -> true__ % 1.97/2.09 q_5(b) -> true__ % 1.97/2.09 q_6(a) -> true__ % 1.97/2.09 q_6(b) -> true__ % 1.97/2.09 q_7(a) -> true__ % 1.97/2.09 q_7(b) -> true__ % 1.97/2.09 q_8(a) -> true__ % 1.97/2.09 q_8(b) -> true__ % 1.97/2.09 q_9(a) -> true__ % 1.97/2.09 q_9(b) -> true__ % 1.97/2.09 with the LPO induced by % 1.97/2.09 b > q_10 > p > f2 > f3 > f4 > f5 > f6 > f7 > f8 > f9 > f10 > f11 > q_9 > f1 > q_8 > q_7 > q_6 > q_5 > q_4 > q_3 > q_2 > q_1 > a > false__ > true__ % 1.97/2.09 % 1.97/2.09 % SZS output end Proof % 1.97/2.09 %------------------------------------------------------------------------------