%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN616-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %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 : 300s % DateTime : Mon Jun 24 19:06:07 EDT 2024 % Result : Unsatisfiable 120.71s 120.79s % Output : CNFRefutation 120.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SYN616-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.34 % Computer : n023.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Sun Jun 23 20:32:09 EDT 2024 % 0.14/0.35 % CPUTime : % 0.49/0.58 start to proof:theBenchmark % 120.71/120.78 %------------------------------------------- % 120.71/120.78 % File :CSE---1.7 % 120.71/120.78 % Problem :theBenchmark % 120.71/120.78 % Transform :cnf % 120.71/120.78 % Format :tptp:raw % 120.71/120.78 % Command :java -jar mcs_scs.jar %d %s % 120.71/120.78 % 120.71/120.78 % Result :Theorem 120.120000s % 120.71/120.78 % Output :CNFRefutation 120.120000s % 120.71/120.78 %------------------------------------------- % 120.71/120.79 %-------------------------------------------------------------------------- % 120.71/120.79 % File : SYN616-1 : TPTP v8.2.0. Released v2.5.0. % 120.71/120.79 % Domain : Syntactic % 120.71/120.79 % Problem : Harrison problem 3901 % 120.71/120.79 % Version : Especial. % 120.71/120.79 % English : % 120.71/120.79 % 120.71/120.79 % Refs : [Har01] Email to G. Sutcliffe % 120.71/120.79 % Source : [Har01] % 120.71/120.79 % Names : % 120.71/120.79 % 120.71/120.79 % Status : Unsatisfiable % 120.71/120.79 % Rating : 0.27 v8.2.0, 0.14 v8.1.0, 0.25 v7.4.0, 0.33 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.29 v6.0.0, 0.56 v5.5.0, 0.50 v5.3.0, 0.60 v5.2.0, 0.46 v5.1.0, 0.44 v5.0.0, 0.40 v4.1.0, 0.47 v4.0.1, 0.43 v3.7.0, 0.29 v3.4.0, 0.20 v3.3.0, 0.00 v2.7.0, 0.25 v2.6.0, 0.33 v2.5.0 % 120.71/120.79 % Syntax : Number of clauses : 32 ( 13 unt; 0 nHn; 28 RR) % 120.71/120.79 % Number of literals : 73 ( 0 equ; 43 neg) % 120.71/120.79 % Maximal clause size : 5 ( 2 avg) % 120.71/120.79 % Maximal term depth : 6 ( 1 avg) % 120.71/120.79 % Number of predicates : 10 ( 10 usr; 0 prp; 1-3 aty) % 120.71/120.79 % Number of functors : 17 ( 17 usr; 9 con; 0-3 aty) % 120.71/120.79 % Number of variables : 67 ( 0 sgn) % 120.71/120.79 % SPC : CNF_UNS_RFO_NEQ_HRN % 120.71/120.79 % 120.71/120.79 % Comments : % 120.71/120.79 %-------------------------------------------------------------------------- % 120.71/120.79 cnf(c28_is_p17_1,negated_conjecture, % 120.71/120.79 p17(c28) ). % 120.71/120.79 % 120.71/120.79 cnf(p10_2,negated_conjecture, % 120.71/120.79 p10(X0,X0) ). % 120.71/120.79 % 120.71/120.79 cnf(p9_3,negated_conjecture, % 120.71/120.79 p9(X60,X60) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_4,negated_conjecture, % 120.71/120.79 p2(X31,X31) ). % 120.71/120.79 % 120.71/120.79 cnf(p18_5,negated_conjecture, % 120.71/120.79 p18(X24,X24) ). % 120.71/120.79 % 120.71/120.79 cnf(p19_6,negated_conjecture, % 120.71/120.79 p19(c26,c27) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_7,negated_conjecture, % 120.71/120.79 p2(c25,c28) ). % 120.71/120.79 % 120.71/120.79 cnf(not_p15_8,negated_conjecture, % 120.71/120.79 ~ p15(c25,c27) ). % 120.71/120.79 % 120.71/120.79 cnf(p13_9,negated_conjecture, % 120.71/120.79 p13(f3(f4(f5(c20))),c21) ). % 120.71/120.79 % 120.71/120.79 cnf(p17_10,negated_conjecture, % 120.71/120.79 ( p17(X22) % 120.71/120.79 | ~ p17(X23) % 120.71/120.79 | ~ p2(X23,X22) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_11,negated_conjecture, % 120.71/120.79 ( p2(f6(X50),f6(X51)) % 120.71/120.79 | ~ p2(X50,X51) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_12,negated_conjecture, % 120.71/120.79 ( p2(f3(X44),f3(X45)) % 120.71/120.79 | ~ p2(X44,X45) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_13,negated_conjecture, % 120.71/120.79 ( p2(f4(X46),f4(X47)) % 120.71/120.79 | ~ p2(X46,X47) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_14,negated_conjecture, % 120.71/120.79 ( p2(f5(X48),f5(X49)) % 120.71/120.79 | ~ p2(X48,X49) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p10_15,negated_conjecture, % 120.71/120.79 ( p10(X1,X2) % 120.71/120.79 | ~ p10(X0,X1) % 120.71/120.79 | ~ p10(X0,X2) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p9_16,negated_conjecture, % 120.71/120.79 ( p9(X61,X62) % 120.71/120.79 | ~ p9(X60,X61) % 120.71/120.79 | ~ p9(X60,X62) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_17,negated_conjecture, % 120.71/120.79 ( p2(X32,X33) % 120.71/120.79 | ~ p2(X31,X32) % 120.71/120.79 | ~ p2(X31,X33) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p18_18,negated_conjecture, % 120.71/120.79 ( p18(X25,X26) % 120.71/120.79 | ~ p18(X24,X25) % 120.71/120.79 | ~ p18(X24,X26) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_19,negated_conjecture, % 120.71/120.79 p2(f11(c23,c24,f3(f5(c20))),f8(c21,f3(f5(c20)))) ). % 120.71/120.79 % 120.71/120.79 cnf(p15_20,negated_conjecture, % 120.71/120.79 ( p15(X17,c24) % 120.71/120.79 | ~ p17(X17) % 120.71/120.79 | ~ p16(X17,f8(c21,f3(f5(c20)))) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p13_21,negated_conjecture, % 120.71/120.79 ( p13(X3,X4) % 120.71/120.79 | ~ p2(X5,X3) % 120.71/120.79 | ~ p2(X6,X4) % 120.71/120.79 | ~ p13(X5,X6) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p19_22,negated_conjecture, % 120.71/120.79 ( p19(X27,X28) % 120.71/120.79 | ~ p18(X30,X27) % 120.71/120.79 | ~ p19(X30,X29) % 120.71/120.79 | ~ p10(X29,X28) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p16_23,negated_conjecture, % 120.71/120.79 ( p16(X18,X19) % 120.71/120.79 | ~ p2(X20,X18) % 120.71/120.79 | ~ p2(X21,X19) % 120.71/120.79 | ~ p16(X20,X21) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p15_24,negated_conjecture, % 120.71/120.79 ( p15(X13,X14) % 120.71/120.79 | ~ p15(X16,X15) % 120.71/120.79 | ~ p2(X16,X13) % 120.71/120.79 | ~ p10(X15,X14) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p14_25,negated_conjecture, % 120.71/120.79 p14(f7(c22,f8(c21,f3(f5(c20)))),f3(f5(c20)),f6(c21)) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_26,negated_conjecture, % 120.71/120.79 ( p2(f8(X56,X57),f8(X58,X59)) % 120.71/120.79 | ~ p2(X56,X58) % 120.71/120.79 | ~ p2(X57,X59) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_27,negated_conjecture, % 120.71/120.79 ( p2(f12(X40,X41),f12(X42,X43)) % 120.71/120.79 | ~ p2(X40,X42) % 120.71/120.79 | ~ p2(X41,X43) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_28,negated_conjecture, % 120.71/120.79 ( p2(f7(X52,X53),f7(X54,X55)) % 120.71/120.79 | ~ p2(X53,X55) % 120.71/120.79 | ~ p2(X52,X54) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p14_29,negated_conjecture, % 120.71/120.79 p14(f7(c22,f12(f8(c21,f3(f5(c20))),c25)),f3(f5(c20)),f6(c21)) ). % 120.71/120.79 % 120.71/120.79 cnf(not_p14_30,negated_conjecture, % 120.71/120.79 ~ p14(f7(c22,f12(f8(c21,f3(f5(c20))),c28)),f3(f5(c20)),f6(c21)) ). % 120.71/120.79 % 120.71/120.79 cnf(p14_31,negated_conjecture, % 120.71/120.79 ( p14(X7,X8,X9) % 120.71/120.79 | ~ p2(X12,X9) % 120.71/120.79 | ~ p2(X11,X8) % 120.71/120.79 | ~ p2(X10,X7) % 120.71/120.79 | ~ p14(X10,X11,X12) ) ). % 120.71/120.79 % 120.71/120.79 cnf(p2_32,negated_conjecture, % 120.71/120.79 ( p2(f11(X34,X35,X36),f11(X37,X38,X39)) % 120.71/120.79 | ~ p2(X36,X39) % 120.71/120.79 | ~ p9(X34,X37) % 120.71/120.79 | ~ p10(X35,X38) ) ). % 120.71/120.79 % 120.71/120.79 %-------------------------------------------------------------------------- % 120.71/120.79 %------------------------------------------- % 120.71/120.79 % Proof found % 120.71/120.79 % SZS status Theorem for theBenchmark % 120.71/120.79 % SZS output start Proof % 120.71/120.80 %ClaNum:32(EqnAxiom:0) % 120.71/120.80 %VarNum:135(SingletonVarNum:67) % 120.71/120.80 %MaxLitNum:5 % 120.71/120.80 %MaxfuncDepth:5 % 120.71/120.80 %SharedTerms:30 % 120.71/120.80 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 % 120.71/120.80 %singleGoalClaCount:13 % 120.71/120.80 [1]P1(a1) % 120.71/120.80 [2]P7(a2,a1) % 120.71/120.80 [3]P8(a8,a9) % 120.71/120.80 [12]~P5(a2,a9) % 120.71/120.80 [8]P3(f12(f11(f10(a3))),a4) % 120.71/120.80 [9]P7(f13(a5,a7,f12(f10(a3))),f15(a4,f12(f10(a3)))) % 120.71/120.80 [10]P4(f16(a6,f15(a4,f12(f10(a3)))),f12(f10(a3)),f17(a4)) % 120.71/120.80 [11]P4(f16(a6,f14(f15(a4,f12(f10(a3))),a2)),f12(f10(a3)),f17(a4)) % 120.71/120.80 [13]~P4(f16(a6,f14(f15(a4,f12(f10(a3))),a1)),f12(f10(a3)),f17(a4)) % 120.71/120.80 [4]P2(x41,x41) % 120.71/120.80 [5]P10(x51,x51) % 120.71/120.80 [6]P7(x61,x61) % 120.71/120.80 [7]P9(x71,x71) % 120.71/120.80 [15]~P7(x151,x152)+P7(f10(x151),f10(x152)) % 120.71/120.80 [16]~P7(x161,x162)+P7(f11(x161),f11(x162)) % 120.71/120.80 [17]~P7(x171,x172)+P7(f12(x171),f12(x172)) % 120.71/120.80 [18]~P7(x181,x182)+P7(f17(x181),f17(x182)) % 120.71/120.80 [30]~P1(x301)+P5(x301,a7)+~P6(x301,f15(a4,f12(f10(a3)))) % 120.71/120.80 [14]~P7(x142,x141)+P1(x141)+~P1(x142) % 120.71/120.80 [19]~P2(x193,x191)+P2(x191,x192)+~P2(x193,x192) % 120.71/120.80 [20]~P10(x203,x201)+P10(x201,x202)+~P10(x203,x202) % 120.71/120.80 [21]~P7(x213,x211)+P7(x211,x212)+~P7(x213,x212) % 120.71/120.80 [22]~P9(x223,x221)+P9(x221,x222)+~P9(x223,x222) % 120.71/120.80 [27]~P7(x272,x274)+~P7(x271,x273)+P7(f15(x271,x272),f15(x273,x274)) % 120.71/120.80 [28]~P7(x282,x284)+~P7(x281,x283)+P7(f16(x281,x282),f16(x283,x284)) % 120.71/120.80 [29]~P7(x292,x294)+~P7(x291,x293)+P7(f14(x291,x292),f14(x293,x294)) % 120.71/120.80 [23]~P8(x234,x233)+P8(x231,x232)+~P2(x233,x232)+~P9(x234,x231) % 120.71/120.80 [24]~P5(x244,x243)+P5(x241,x242)+~P2(x243,x242)+~P7(x244,x241) % 120.71/120.80 [25]~P3(x254,x253)+P3(x251,x252)+~P7(x253,x252)+~P7(x254,x251) % 120.71/120.80 [26]~P6(x264,x263)+P6(x261,x262)+~P7(x263,x262)+~P7(x264,x261) % 120.71/120.80 [32]~P2(x322,x325)+~P10(x321,x324)+~P7(x323,x326)+P7(f13(x321,x322,x323),f13(x324,x325,x326)) % 120.71/120.80 [31]~P4(x314,x315,x316)+P4(x311,x312,x313)+~P7(x314,x311)+~P7(x315,x312)+~P7(x316,x313) % 120.71/120.80 %EqnAxiom % 120.71/120.80 % 120.71/120.80 %------------------------------------------- % 120.82/120.81 cnf(36,plain, % 120.82/120.81 (P7(a1,a2)), % 120.82/120.81 inference(scs_inference,[],[2,6,21])). % 120.82/120.81 cnf(132,plain, % 120.82/120.81 (P7(f10(f11(a1)),f10(f11(a2)))), % 120.82/120.81 inference(scs_inference,[],[36,15,16])). % 120.82/120.81 cnf(139,plain, % 120.82/120.81 (P7(f12(f17(a1)),f12(f17(a2)))), % 120.82/120.81 inference(scs_inference,[],[36,17,18])). % 120.82/120.81 cnf(153,plain, % 120.82/120.81 (P7(f10(f11(a2)),f10(f11(a1)))), % 120.82/120.81 inference(scs_inference,[],[132,6,21])). % 120.82/120.81 cnf(183,plain, % 120.82/120.81 (P7(f12(f17(a2)),f12(f17(a1)))), % 120.82/120.81 inference(scs_inference,[],[139,6,21])). % 120.82/120.81 cnf(324,plain, % 120.82/120.81 (P7(f13(x3241,x3242,a1),f13(x3241,x3242,a2))), % 120.82/120.81 inference(scs_inference,[],[4,5,36,19,32])). % 120.82/120.81 cnf(336,plain, % 120.82/120.81 (P7(f13(x3361,x3362,a2),f13(x3361,x3362,a1))), % 120.82/120.81 inference(scs_inference,[],[324,6,21])). % 120.82/120.81 cnf(746,plain, % 120.82/120.81 (P7(f10(f12(a1)),f10(f12(a2)))), % 120.82/120.81 inference(scs_inference,[],[36,15,17])). % 120.82/120.81 cnf(753,plain, % 120.82/120.81 (P7(f11(f10(a1)),f11(f10(a2)))), % 120.82/120.81 inference(scs_inference,[],[36,15,16])). % 120.82/120.81 cnf(760,plain, % 120.82/120.81 (P7(f10(f17(a1)),f10(f17(a2)))), % 120.82/120.81 inference(scs_inference,[],[36,15,18])). % 120.82/120.81 cnf(767,plain, % 120.82/120.81 (P7(f17(f10(a1)),f17(f10(a2)))), % 120.82/120.81 inference(scs_inference,[],[36,15,18])). % 120.82/120.81 cnf(823,plain, % 120.82/120.81 (P7(f10(f12(a2)),f10(f12(a1)))), % 120.82/120.81 inference(scs_inference,[],[746,6,21])). % 120.82/120.81 cnf(843,plain, % 120.82/120.81 (P7(f11(f10(a2)),f11(f10(a1)))), % 120.82/120.81 inference(scs_inference,[],[753,6,21])). % 120.82/120.81 cnf(863,plain, % 120.82/120.81 (P7(f10(f17(a2)),f10(f17(a1)))), % 120.82/120.81 inference(scs_inference,[],[760,6,21])). % 120.82/120.81 cnf(883,plain, % 120.82/120.81 (P7(f17(f10(a2)),f17(f10(a1)))), % 120.82/120.81 inference(scs_inference,[],[767,6,21])). % 120.82/120.81 cnf(1762,plain, % 120.82/120.81 (P7(f15(f10(a1),f10(a1)),f15(f10(a2),f10(a2)))), % 120.82/120.81 inference(scs_inference,[],[36,15,27])). % 120.82/120.81 cnf(1769,plain, % 120.82/120.81 (P7(f10(f15(a1,a1)),f10(f15(a2,a2)))), % 120.82/120.81 inference(scs_inference,[],[36,15,27])). % 120.82/120.81 cnf(1845,plain, % 120.82/120.81 (P7(f15(f10(a2),f10(a2)),f15(f10(a1),f10(a1)))), % 120.82/120.81 inference(scs_inference,[],[1762,6,21])). % 120.82/120.81 cnf(1870,plain, % 120.82/120.81 (P7(f10(f15(a2,a2)),f10(f15(a1,a1)))), % 120.82/120.81 inference(scs_inference,[],[1769,6,21])). % 120.82/120.81 cnf(2830,plain, % 120.82/120.81 (P7(f16(f10(a1),f10(a1)),f16(f10(a2),f10(a2)))), % 120.82/120.81 inference(scs_inference,[],[36,15,28])). % 120.82/120.81 cnf(2936,plain, % 120.82/120.81 (P7(f16(f10(a2),f10(a2)),f16(f10(a1),f10(a1)))), % 120.82/120.81 inference(scs_inference,[],[2830,6,21])). % 120.82/120.81 cnf(3467,plain, % 120.82/120.81 (P7(f14(f16(f10(a1),f10(a1)),f16(f10(a1),f10(a1))),f14(f16(f10(a2),f10(a2)),f16(f10(a2),f10(a2))))), % 120.82/120.81 inference(scs_inference,[],[2830,18,16,15,17,27,29])). % 120.82/120.81 cnf(3567,plain, % 120.82/120.81 (P7(f15(f10(f15(a1,a1)),f10(f15(a1,a1))),f15(f10(f15(a2,a2)),f10(f15(a2,a2))))), % 120.82/120.81 inference(scs_inference,[],[3467,1769,15,17,16,18,29,27])). % 120.82/120.81 cnf(3602,plain, % 120.82/120.81 (P7(f15(f17(f10(a1)),f17(f10(a1))),f15(f17(f10(a2)),f17(f10(a2))))), % 120.82/120.81 inference(scs_inference,[],[3567,767,16,17,18,15,29,27])). % 120.82/120.81 cnf(3636,plain, % 120.82/120.81 (P7(f14(f16(f10(a2),f10(a2)),f16(f10(a2),f10(a2))),f14(f16(f10(a1),f10(a1)),f16(f10(a1),f10(a1))))), % 120.82/120.81 inference(scs_inference,[],[3602,2936,18,15,16,17,29])). % 120.82/120.81 cnf(3654,plain, % 120.82/120.81 (P7(f15(f13(x36541,x36542,a2),f13(x36541,x36542,a2)),f15(f13(x36541,x36542,a1),f13(x36541,x36542,a1)))), % 120.82/120.81 inference(scs_inference,[],[3636,336,17,18,15,16,27])). % 120.82/120.81 cnf(3670,plain, % 120.82/120.81 (P7(f14(f15(f13(x36701,x36702,a2),f13(x36701,x36702,a2)),f15(f13(x36701,x36702,a2),f13(x36701,x36702,a2))),f14(f15(f13(x36701,x36702,a1),f13(x36701,x36702,a1)),f15(f13(x36701,x36702,a1),f13(x36701,x36702,a1))))), % 120.82/120.81 inference(scs_inference,[],[3654,16,17,18,15,29])). % 120.82/120.81 cnf(3974,plain, % 120.82/120.81 (P7(f15(f11(f10(a1)),f11(f10(a1))),f15(f11(f10(a2)),f11(f10(a2))))), % 120.82/120.81 inference(scs_inference,[],[3670,753,18,15,17,16,29,27])). % 120.82/120.81 cnf(4007,plain, % 120.82/120.81 (P7(f14(f10(f17(a1)),f10(f17(a1))),f14(f10(f17(a2)),f10(f17(a2))))), % 120.82/120.81 inference(scs_inference,[],[3974,760,18,15,17,16,29])). % 120.82/120.81 cnf(4025,plain, % 120.82/120.81 (P7(f15(f10(f12(a1)),f10(f12(a1))),f15(f10(f12(a2)),f10(f12(a2))))), % 120.82/120.81 inference(scs_inference,[],[4007,746,18,15,16,17,27])). % 120.82/120.81 cnf(4045,plain, % 120.82/120.81 (P7(f15(f10(f15(a2,a2)),f10(f15(a2,a2))),f15(f10(f15(a1,a1)),f10(f15(a1,a1))))), % 120.82/120.81 inference(scs_inference,[],[4025,1870,18,15,17,16,29,27])). % 120.82/120.81 cnf(4080,plain, % 120.82/120.81 (P7(f15(f15(f10(a1),f10(a1)),f15(f10(a1),f10(a1))),f15(f15(f10(a2),f10(a2)),f15(f10(a2),f10(a2))))), % 120.82/120.81 inference(scs_inference,[],[4045,1762,18,15,17,16,29,27])). % 120.82/120.81 cnf(4114,plain, % 120.82/120.81 (P7(f14(f10(f17(a2)),f10(f17(a2))),f14(f10(f17(a1)),f10(f17(a1))))), % 120.82/120.81 inference(scs_inference,[],[4080,863,18,15,17,16,29])). % 120.82/120.81 cnf(4133,plain, % 120.82/120.81 (P7(f15(f10(f12(a2)),f10(f12(a2))),f15(f10(f12(a1)),f10(f12(a1))))), % 120.82/120.81 inference(scs_inference,[],[4114,823,18,15,16,17,27])). % 120.82/120.81 cnf(4153,plain, % 120.82/120.81 (P7(f15(f17(f10(a2)),f17(f10(a2))),f15(f17(f10(a1)),f17(f10(a1))))), % 120.82/120.81 inference(scs_inference,[],[4133,883,18,15,17,16,29,27])). % 120.82/120.81 cnf(4191,plain, % 120.82/120.81 (P7(f16(f11(f10(a2)),f11(f10(a2))),f16(f11(f10(a1)),f11(f10(a1))))), % 120.82/120.81 inference(scs_inference,[],[4153,843,18,15,17,16,29,27,28])). % 120.82/120.81 cnf(4240,plain, % 120.82/120.81 (P7(f14(f13(x42401,x42402,a1),f13(x42401,x42402,a1)),f14(f13(x42401,x42402,a2),f13(x42401,x42402,a2)))), % 120.82/120.81 inference(scs_inference,[],[4191,324,15,18,17,16,29])). % 120.82/120.81 cnf(4242,plain, % 120.82/120.81 (P7(f15(f13(x42421,x42422,a1),f13(x42421,x42422,a1)),f15(f13(x42421,x42422,a2),f13(x42421,x42422,a2)))), % 120.82/120.81 inference(scs_inference,[],[4191,324,15,18,17,16,29,27])). % 120.82/120.81 cnf(4260,plain, % 120.82/120.81 (P7(f14(f14(f13(x42601,x42602,a1),f13(x42601,x42602,a1)),f14(f13(x42601,x42602,a1),f13(x42601,x42602,a1))),f14(f14(f13(x42601,x42602,a2),f13(x42601,x42602,a2)),f14(f13(x42601,x42602,a2),f13(x42601,x42602,a2))))), % 120.82/120.81 inference(scs_inference,[],[4240,18,15,17,16,29])). % 120.82/120.81 cnf(4368,plain, % 120.82/120.81 (P7(f14(f15(f13(x43681,x43682,a1),f13(x43681,x43682,a1)),f15(f13(x43681,x43682,a1),f13(x43681,x43682,a1))),f14(f15(f13(x43681,x43682,a2),f13(x43681,x43682,a2)),f15(f13(x43681,x43682,a2),f13(x43681,x43682,a2))))), % 120.82/120.81 inference(scs_inference,[],[4260,4242,18,15,16,17,27,29])). % 120.82/120.81 cnf(4405,plain, % 120.82/120.81 (P7(f15(f12(f17(a1)),f12(f17(a1))),f15(f12(f17(a2)),f12(f17(a2))))), % 120.82/120.81 inference(scs_inference,[],[4368,139,18,15,16,17,27])). % 120.82/120.81 cnf(4426,plain, % 120.82/120.81 (P7(f15(f15(f10(a2),f10(a2)),f15(f10(a2),f10(a2))),f15(f15(f10(a1),f10(a1)),f15(f10(a1),f10(a1))))), % 120.82/120.81 inference(scs_inference,[],[4405,1845,18,15,16,17,29,27])). % 120.82/120.81 cnf(4458,plain, % 120.82/120.81 (P7(f14(f10(f11(a1)),f10(f11(a1))),f14(f10(f11(a2)),f10(f11(a2))))), % 120.82/120.81 inference(scs_inference,[],[4426,132,18,15,16,17,29])). % 120.82/120.81 cnf(4474,plain, % 120.82/120.81 (P7(f15(f10(f11(a2)),f10(f11(a2))),f15(f10(f11(a1)),f10(f11(a1))))), % 120.82/120.81 inference(scs_inference,[],[4458,153,18,15,16,17,27])). % 120.82/120.81 cnf(4493,plain, % 120.82/120.81 (P7(f15(f12(f17(a2)),f12(f17(a2))),f15(f12(f17(a1)),f12(f17(a1))))), % 120.82/120.81 inference(scs_inference,[],[4474,183,18,15,16,17,27])). % 120.82/120.81 cnf(4511,plain, % 120.82/120.81 (P7(f15(a1,a1),f15(a2,a2))), % 120.82/120.81 inference(scs_inference,[],[4493,36,18,15,16,17,27])). % 120.82/120.81 cnf(4513,plain, % 120.82/120.81 (P7(f14(a1,a1),f14(a2,a2))), % 120.82/120.81 inference(scs_inference,[],[4493,36,18,15,16,17,27,29])). % 120.82/120.81 cnf(4515,plain, % 120.82/120.81 (P7(f16(a1,a1),f16(a2,a2))), % 120.82/120.81 inference(scs_inference,[],[4493,36,18,15,16,17,27,29,28])). % 120.82/120.81 cnf(4523,plain, % 120.82/120.81 (P7(f17(f15(a1,a1)),f17(f15(a2,a2)))), % 120.82/120.81 inference(scs_inference,[],[4511,18])). % 120.82/120.81 cnf(4525,plain, % 120.82/120.81 (P7(f10(f14(a1,a1)),f10(f14(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4511,4513,18,15])). % 120.82/120.82 cnf(4529,plain, % 120.82/120.82 (P7(f12(f15(a1,a1)),f12(f15(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4511,4513,18,15,16,17])). % 120.82/120.82 cnf(4531,plain, % 120.82/120.82 (P7(f15(f15(a1,a1),f15(a1,a1)),f15(f15(a2,a2),f15(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4511,4513,18,15,16,17,27])). % 120.82/120.82 cnf(4533,plain, % 120.82/120.82 (P7(f14(f15(a1,a1),f15(a1,a1)),f14(f15(a2,a2),f15(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4511,4513,18,15,16,17,27,29])). % 120.82/120.82 cnf(4537,plain, % 120.82/120.82 (P7(f13(x45371,x45372,f15(a1,a1)),f13(x45371,x45372,f15(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4511,4513,5,4,18,15,16,17,27,29,28,32])). % 120.82/120.82 cnf(4541,plain, % 120.82/120.82 (P7(f17(f16(a1,a1)),f17(f16(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4515,18])). % 120.82/120.82 cnf(4543,plain, % 120.82/120.82 (P7(f10(f16(a1,a1)),f10(f16(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4515,18,15])). % 120.82/120.82 cnf(4547,plain, % 120.82/120.82 (P7(f12(f16(a1,a1)),f12(f16(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4515,18,15,16,17])). % 120.82/120.82 cnf(4549,plain, % 120.82/120.82 (P7(f15(f16(a1,a1),f16(a1,a1)),f15(f16(a2,a2),f16(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[4515,18,15,16,17,27])). % 120.82/120.82 cnf(4584,plain, % 120.82/120.82 (P7(f15(f17(f16(a1,a1)),f17(f16(a1,a1))),f15(f17(f16(a2,a2)),f17(f16(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4541,18,15,16,17,27])). % 120.82/120.82 cnf(4691,plain, % 120.82/120.82 (P7(f14(f10(f16(a1,a1)),f10(f16(a1,a1))),f14(f10(f16(a2,a2)),f10(f16(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4584,4543,18,15,16,17,27,29])). % 120.82/120.82 cnf(4722,plain, % 120.82/120.82 (P7(f15(f12(f16(a1,a1)),f12(f16(a1,a1))),f15(f12(f16(a2,a2)),f12(f16(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4691,4547,18,15,16,17,27])). % 120.82/120.82 cnf(4742,plain, % 120.82/120.82 (P7(f14(f15(f16(a1,a1),f16(a1,a1)),f15(f16(a1,a1),f16(a1,a1))),f14(f15(f16(a2,a2),f16(a2,a2)),f15(f16(a2,a2),f16(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4722,4549,15,18,16,17,27,29])). % 120.82/120.82 cnf(4886,plain, % 120.82/120.82 (P7(f15(f13(x48861,x48862,f15(a1,a1)),f13(x48861,x48862,f15(a1,a1))),f15(f13(x48861,x48862,f15(a2,a2)),f13(x48861,x48862,f15(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4742,4537,18,15,17,16,27])). % 120.82/120.82 cnf(4904,plain, % 120.82/120.82 (P7(f14(f17(f15(a1,a1)),f17(f15(a1,a1))),f14(f17(f15(a2,a2)),f17(f15(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4886,4523,18,15,17,16,27,29])). % 120.82/120.82 cnf(4938,plain, % 120.82/120.82 (P7(f15(f12(f15(a1,a1)),f12(f15(a1,a1))),f15(f12(f15(a2,a2)),f12(f15(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4904,4529,18,15,17,16,27])). % 120.82/120.82 cnf(4956,plain, % 120.82/120.82 (P7(f15(f15(f15(a1,a1),f15(a1,a1)),f15(f15(a1,a1),f15(a1,a1))),f15(f15(f15(a2,a2),f15(a2,a2)),f15(f15(a2,a2),f15(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4938,4531,18,15,17,16,27])). % 120.82/120.82 cnf(4976,plain, % 120.82/120.82 (P7(f14(f14(f15(a1,a1),f15(a1,a1)),f14(f15(a1,a1),f15(a1,a1))),f14(f14(f15(a2,a2),f15(a2,a2)),f14(f15(a2,a2),f15(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4956,4533,18,15,17,16,27,29])). % 120.82/120.82 cnf(5011,plain, % 120.82/120.82 (P7(f15(f10(f14(a1,a1)),f10(f14(a1,a1))),f15(f10(f14(a2,a2)),f10(f14(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[4976,4525,18,15,17,16,27])). % 120.82/120.82 cnf(5029,plain, % 120.82/120.82 (P7(f15(f14(a1,a1),f14(a1,a1)),f15(f14(a2,a2),f14(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[5011,4513,18,15,17,16,27])). % 120.82/120.82 cnf(5031,plain, % 120.82/120.82 (P7(f14(f14(a1,a1),f14(a1,a1)),f14(f14(a2,a2),f14(a2,a2)))), % 120.82/120.82 inference(scs_inference,[],[5011,4513,18,15,17,16,27,29])). % 120.82/120.82 cnf(5047,plain, % 120.82/120.82 (P7(f15(f15(f14(a1,a1),f14(a1,a1)),f15(f14(a1,a1),f14(a1,a1))),f15(f15(f14(a2,a2),f14(a2,a2)),f15(f14(a2,a2),f14(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[5029,18,15,17,16,27])). % 120.82/120.82 cnf(5154,plain, % 120.82/120.82 (P7(f15(f14(f14(a1,a1),f14(a1,a1)),f14(f14(a1,a1),f14(a1,a1))),f15(f14(f14(a2,a2),f14(a2,a2)),f14(f14(a2,a2),f14(a2,a2))))), % 120.82/120.82 inference(scs_inference,[],[5047,5031,18,15,17,16,27])). % 120.82/120.82 cnf(5186,plain, % 120.82/120.82 (P7(f15(a2,a2),f15(a1,a1))), % 120.82/120.82 inference(scs_inference,[],[5154,2,18,15,17,16,27])). % 120.82/120.82 cnf(5188,plain, % 120.82/120.82 (P7(f14(a2,a2),f14(a1,a1))), % 120.82/120.82 inference(scs_inference,[],[5154,2,18,15,17,16,27,29])). % 120.82/120.82 cnf(5190,plain, % 120.82/120.82 (P7(f16(a2,a2),f16(a1,a1))), % 120.82/120.82 inference(scs_inference,[],[5154,2,18,15,17,16,27,29,28])). % 120.82/120.82 cnf(5198,plain, % 120.82/120.82 (P7(f17(f15(a2,a2)),f17(f15(a1,a1)))), % 120.82/120.82 inference(scs_inference,[],[5186,18])). % 120.82/120.82 cnf(5200,plain, % 120.82/120.82 (P7(f10(f14(a2,a2)),f10(f14(a1,a1)))), % 120.82/120.82 inference(scs_inference,[],[5186,5188,18,15])). % 120.82/120.82 cnf(5202,plain, % 120.82/120.82 (P7(f12(f15(a2,a2)),f12(f15(a1,a1)))), % 120.82/120.82 inference(scs_inference,[],[5186,5188,18,15,17])). % 120.82/120.82 cnf(5210,plain, % 120.82/120.82 (P7(f16(f15(a2,a2),f15(a2,a2)),f16(f15(a1,a1),f15(a1,a1)))), % 120.82/120.82 inference(scs_inference,[],[5186,5188,18,15,17,16,27,29,28])). % 120.82/120.82 cnf(5224,plain, % 120.82/120.82 (P7(f15(f16(a2,a2),f16(a2,a2)),f15(f16(a1,a1),f16(a1,a1)))), % 120.82/120.82 inference(scs_inference,[],[5190,18,15,17,16,27])). % 120.82/120.82 cnf(5370,plain, % 120.82/120.82 (P7(f11(a2),f11(a1))), % 120.82/120.82 inference(scs_inference,[],[2,16])). % 120.82/120.82 cnf(5372,plain, % 120.82/120.82 (P7(f17(a2),f17(a1))), % 120.82/120.82 inference(scs_inference,[],[2,16,18])). % 120.82/120.82 cnf(5376,plain, % 120.82/120.82 (P7(f12(a2),f12(a1))), % 120.82/120.82 inference(scs_inference,[],[2,16,18,15,17])). % 120.82/120.82 cnf(5388,plain, % 120.82/120.82 (P7(f11(f11(a2)),f11(f11(a1)))), % 120.82/120.82 inference(scs_inference,[],[5370,16])). % 120.82/120.82 cnf(5417,plain, % 120.82/120.82 (P7(f15(f11(f11(a2)),f11(f11(a2))),f15(f11(f11(a1)),f11(f11(a1))))), % 120.82/120.82 inference(scs_inference,[],[5388,16,18,15,17,29,28,27])). % 120.82/120.82 cnf(5783,plain, % 120.82/120.82 (P7(f16(f12(a2),f12(a2)),f16(f12(a1),f12(a1)))), % 120.82/120.82 inference(scs_inference,[],[5417,5376,15,17,16,18,28])). % 120.82/120.82 cnf(5800,plain, % 120.82/120.82 (P7(f16(f16(f12(a2),f12(a2)),f16(f12(a2),f12(a2))),f16(f16(f12(a1),f12(a1)),f16(f12(a1),f12(a1))))), % 120.82/120.82 inference(scs_inference,[],[5783,15,17,16,18,28])). % 120.82/120.82 cnf(6092,plain, % 120.82/120.82 (P7(f14(f17(a2),f17(a2)),f14(f17(a1),f17(a1)))), % 120.82/120.82 inference(scs_inference,[],[5800,5372,18,15,17,16,29])). % 120.82/120.82 cnf(6094,plain, % 120.82/120.82 (P7(f16(f17(a2),f17(a2)),f16(f17(a1),f17(a1)))), % 120.82/120.82 inference(scs_inference,[],[5800,5372,18,15,17,16,29,28])). % 120.82/120.82 cnf(6096,plain, % 120.82/120.82 (P7(f15(f17(a2),f17(a2)),f15(f17(a1),f17(a1)))), % 120.82/120.82 inference(scs_inference,[],[5800,5372,18,15,17,16,29,28,27])). % 120.82/120.82 cnf(6108,plain, % 120.82/120.82 (P7(f14(f14(f17(a2),f17(a2)),f14(f17(a2),f17(a2))),f14(f14(f17(a1),f17(a1)),f14(f17(a1),f17(a1))))), % 120.82/120.82 inference(scs_inference,[],[6092,18,15,17,16,29])). % 120.82/120.82 cnf(6195,plain, % 120.82/120.82 (P7(f15(f16(f17(a2),f17(a2)),f16(f17(a2),f17(a2))),f15(f16(f17(a1),f17(a1)),f16(f17(a1),f17(a1))))), % 120.82/120.82 inference(scs_inference,[],[6108,6094,18,15,17,16,29,28,27])). % 120.82/120.82 cnf(6209,plain, % 120.82/120.82 (P7(f15(f15(f17(a2),f17(a2)),f15(f17(a2),f17(a2))),f15(f15(f17(a1),f17(a1)),f15(f17(a1),f17(a1))))), % 120.82/120.82 inference(scs_inference,[],[6195,6096,18,15,17,16,29,28,27])). % 120.82/120.82 cnf(6219,plain, % 120.82/120.82 (P7(f14(f16(f15(a2,a2),f15(a2,a2)),f16(f15(a2,a2),f15(a2,a2))),f14(f16(f15(a1,a1),f15(a1,a1)),f16(f15(a1,a1),f15(a1,a1))))), % 120.82/120.82 inference(scs_inference,[],[6209,5210,18,15,17,16,29])). % 120.82/120.82 cnf(6237,plain, % 120.82/120.82 (P7(f16(f15(f16(a2,a2),f16(a2,a2)),f15(f16(a2,a2),f16(a2,a2))),f16(f15(f16(a1,a1),f16(a1,a1)),f15(f16(a1,a1),f16(a1,a1))))), % 120.82/120.82 inference(scs_inference,[],[6219,5224,18,15,17,16,29,28])). % 120.82/120.82 cnf(6286,plain, % 120.82/120.82 (P7(f14(f17(f15(a2,a2)),f17(f15(a2,a2))),f14(f17(f15(a1,a1)),f17(f15(a1,a1))))), % 120.82/120.82 inference(scs_inference,[],[6237,5198,18,15,17,16,29])). % 120.82/120.82 cnf(6306,plain, % 120.82/120.82 (P7(f16(f12(f15(a2,a2)),f12(f15(a2,a2))),f16(f12(f15(a1,a1)),f12(f15(a1,a1))))), % 120.82/120.82 inference(scs_inference,[],[6286,5202,18,15,17,16,29,28])). % 120.82/120.82 cnf(6347,plain, % 120.82/120.82 (~P7(f17(a4),f17(a4))+~P7(f16(a6,f14(f15(a4,f12(f10(a3))),a2)),f16(a6,f14(f15(a4,f12(f10(a3))),a1)))), % 120.82/120.82 inference(scs_inference,[],[6306,11,5200,13,5,6,4,18,15,17,16,29,28,27,32,31])). % 120.82/120.82 cnf(6357,plain, % 120.82/120.82 (~P7(f16(a6,f14(f15(a4,f12(f10(a3))),a2)),f16(a6,f14(f15(a4,f12(f10(a3))),a1)))), % 120.82/120.82 inference(scs_inference,[],[6,6347])). % 120.82/120.82 cnf(6371,plain, % 120.82/120.82 (P7(x63711,x63711)), % 120.82/120.82 inference(rename_variables,[],[6])). % 120.82/120.82 cnf(6373,plain, % 120.82/120.82 ($false), % 120.82/120.82 inference(scs_inference,[],[6,6371,2,6357,28,29]), % 120.82/120.82 ['proof']). % 120.82/120.82 % SZS output end Proof % 120.82/120.82 % Total time :120.120000s %------------------------------------------------------------------------------