%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN645-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 : n027.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:12 EDT 2024 % Result : Unsatisfiable 2.31s 2.43s % Output : CNFRefutation 2.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYN645-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n027.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 21:17:09 EDT 2024 % 0.11/0.33 % CPUTime : % 0.18/0.56 start to proof:theBenchmark % 2.31/2.41 %------------------------------------------- % 2.31/2.41 % File :CSE---1.7 % 2.31/2.41 % Problem :theBenchmark % 2.31/2.41 % Transform :cnf % 2.31/2.41 % Format :tptp:raw % 2.31/2.41 % Command :java -jar mcs_scs.jar %d %s % 2.31/2.41 % 2.31/2.41 % Result :Theorem 1.790000s % 2.31/2.41 % Output :CNFRefutation 1.790000s % 2.31/2.41 %------------------------------------------- % 2.31/2.42 %-------------------------------------------------------------------------- % 2.31/2.42 % File : SYN645-1 : TPTP v8.2.0. Released v2.5.0. % 2.31/2.42 % Domain : Syntactic % 2.31/2.42 % Problem : Harrison problem 4319 % 2.31/2.42 % Version : Especial. % 2.31/2.42 % English : % 2.31/2.42 % 2.31/2.42 % Refs : [Har01] Email to G. Sutcliffe % 2.31/2.42 % Source : [Har01] % 2.31/2.42 % Names : % 2.31/2.42 % 2.31/2.42 % Status : Unsatisfiable % 2.31/2.42 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.38 v6.3.0, 0.14 v6.2.0, 0.22 v6.1.0, 0.29 v5.5.0, 0.38 v5.4.0, 0.40 v5.2.0, 0.30 v5.1.0, 0.36 v5.0.0, 0.29 v4.1.0, 0.25 v4.0.1, 0.20 v4.0.0, 0.29 v3.4.0, 0.75 v3.3.0, 0.67 v3.2.0, 0.33 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0 % 2.31/2.42 % Syntax : Number of clauses : 42 ( 11 unt; 3 nHn; 31 RR) % 2.31/2.42 % Number of literals : 111 ( 0 equ; 67 neg) % 2.31/2.42 % Maximal clause size : 6 ( 2 avg) % 2.31/2.42 % Maximal term depth : 6 ( 2 avg) % 2.31/2.42 % Number of predicates : 10 ( 10 usr; 0 prp; 1-2 aty) % 2.31/2.42 % Number of functors : 21 ( 21 usr; 7 con; 0-5 aty) % 2.31/2.42 % Number of variables : 123 ( 1 sgn) % 2.31/2.42 % SPC : CNF_UNS_RFO_NEQ_NHN % 2.31/2.42 % 2.31/2.42 % Comments : % 2.31/2.42 %-------------------------------------------------------------------------- % 2.31/2.42 cnf(p12_1,negated_conjecture, % 2.31/2.42 p12(X0,X0) ). % 2.31/2.42 % 2.31/2.42 cnf(p9_2,negated_conjecture, % 2.31/2.42 p9(X82,X82) ). % 2.31/2.42 % 2.31/2.42 cnf(p7_3,negated_conjecture, % 2.31/2.42 p7(X77,X77) ). % 2.31/2.42 % 2.31/2.42 cnf(p6_4,negated_conjecture, % 2.31/2.42 p6(X70,X70) ). % 2.31/2.42 % 2.31/2.42 cnf(p2_5,negated_conjecture, % 2.31/2.42 p2(X43,X43) ). % 2.31/2.42 % 2.31/2.42 cnf(p15_6,negated_conjecture, % 2.31/2.42 p15(X40,X40) ). % 2.31/2.42 % 2.31/2.42 cnf(p22_7,negated_conjecture, % 2.31/2.42 p22(f3(f4(f5(c26))),c27) ). % 2.31/2.42 % 2.31/2.42 cnf(p24_8,negated_conjecture, % 2.31/2.42 ( p24(X64) % 2.31/2.42 | ~ p24(X65) % 2.31/2.42 | ~ p2(X65,X64) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p23_9,negated_conjecture, % 2.31/2.42 p23(c28,f8(f10(c29,f11(c27,c30)))) ). % 2.31/2.42 % 2.31/2.42 cnf(p7_10,negated_conjecture, % 2.31/2.42 ( p7(f8(X80),f8(X81)) % 2.31/2.42 | ~ p6(X80,X81) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p12_11,negated_conjecture, % 2.31/2.42 ( p12(f13(X8),f13(X9)) % 2.31/2.42 | ~ p12(X8,X9) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p12_12,negated_conjecture, % 2.31/2.42 ( p12(f19(X24),f19(X25)) % 2.31/2.42 | ~ p2(X24,X25) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p2_13,negated_conjecture, % 2.31/2.42 ( p2(f3(X50),f3(X51)) % 2.31/2.42 | ~ p2(X50,X51) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p2_14,negated_conjecture, % 2.31/2.42 ( p2(f4(X52),f4(X53)) % 2.31/2.42 | ~ p2(X52,X53) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p2_15,negated_conjecture, % 2.31/2.42 ( p2(f5(X54),f5(X55)) % 2.31/2.42 | ~ p2(X54,X55) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p12_16,negated_conjecture, % 2.31/2.42 ( p12(X1,X2) % 2.31/2.42 | ~ p12(X0,X1) % 2.31/2.42 | ~ p12(X0,X2) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p9_17,negated_conjecture, % 2.31/2.42 ( p9(X83,X84) % 2.31/2.42 | ~ p9(X82,X83) % 2.31/2.42 | ~ p9(X82,X84) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p7_18,negated_conjecture, % 2.31/2.42 ( p7(X78,X79) % 2.31/2.42 | ~ p7(X77,X78) % 2.31/2.42 | ~ p7(X77,X79) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p6_19,negated_conjecture, % 2.31/2.42 ( p6(X71,X72) % 2.31/2.42 | ~ p6(X70,X71) % 2.31/2.42 | ~ p6(X70,X72) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p2_20,negated_conjecture, % 2.31/2.42 ( p2(X44,X45) % 2.31/2.42 | ~ p2(X43,X44) % 2.31/2.42 | ~ p2(X43,X45) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p15_21,negated_conjecture, % 2.31/2.42 ( p15(X41,X42) % 2.31/2.42 | ~ p15(X40,X41) % 2.31/2.42 | ~ p15(X40,X42) ) ). % 2.31/2.42 % 2.31/2.42 cnf(not_p12_22,negated_conjecture, % 2.31/2.42 ~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) ). % 2.31/2.42 % 2.31/2.42 cnf(p25_23,negated_conjecture, % 2.31/2.42 ( p25(X66,X67) % 2.31/2.42 | ~ p12(X69,X67) % 2.31/2.42 | ~ p25(X68,X69) % 2.31/2.42 | ~ p12(X68,X66) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p22_24,negated_conjecture, % 2.31/2.42 ( p22(X56,X57) % 2.31/2.42 | ~ p2(X59,X57) % 2.31/2.42 | ~ p22(X58,X59) % 2.31/2.42 | ~ p2(X58,X56) ) ). % 2.31/2.42 % 2.31/2.42 cnf(p23_25,negated_conjecture, % 2.31/2.43 ( p23(X60,X61) % 2.31/2.43 | ~ p23(X62,X63) % 2.31/2.43 | ~ p7(X63,X61) % 2.31/2.43 | ~ p12(X62,X60) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_26,negated_conjecture, % 2.31/2.43 ( p12(f14(X10,X11),f14(X12,X13)) % 2.31/2.43 | ~ p12(X10,X12) % 2.31/2.43 | ~ p12(X11,X13) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p9_27,negated_conjecture, % 2.31/2.43 ( p9(f11(X85,X86),f11(X87,X88)) % 2.31/2.43 | ~ p2(X85,X87) % 2.31/2.43 | ~ p2(X86,X88) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p6_28,negated_conjecture, % 2.31/2.43 ( p6(f10(X73,X74),f10(X75,X76)) % 2.31/2.43 | ~ p2(X73,X75) % 2.31/2.43 | ~ p9(X74,X76) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p2_29,negated_conjecture, % 2.31/2.43 ( p2(f17(X46,X47),f17(X48,X49)) % 2.31/2.43 | ~ p12(X47,X49) % 2.31/2.43 | ~ p6(X46,X48) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_30,negated_conjecture, % 2.31/2.43 ( p12(f20(X26,X27),f20(X28,X29)) % 2.31/2.43 | ~ p12(X27,X29) % 2.31/2.43 | ~ p6(X26,X28) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_31,negated_conjecture, % 2.31/2.43 ( p12(f18(X20,X21),f18(X22,X23)) % 2.31/2.43 | ~ p12(X20,X22) % 2.31/2.43 | ~ p12(X21,X23) ) ). % 2.31/2.43 % 2.31/2.43 cnf(f17_is_not_p24_32,negated_conjecture, % 2.31/2.43 ~ p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_33,negated_conjecture, % 2.31/2.43 p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_34,negated_conjecture, % 2.31/2.43 ( p12(f16(X14,X15,X16),f16(X17,X18,X19)) % 2.31/2.43 | ~ p15(X15,X18) % 2.31/2.43 | ~ p6(X14,X17) % 2.31/2.43 | ~ p12(X16,X19) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p23_35,negated_conjecture, % 2.31/2.43 ( p23(f16(f10(X4,f11(X5,X6)),c32,X7),f8(f10(X4,f11(X5,X6)))) % 2.31/2.43 | ~ p22(f3(f4(f5(c26))),X5) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_36,negated_conjecture, % 2.31/2.43 ( p12(f21(X30,X31,X32,X33,X34),f21(X35,X36,X37,X38,X39)) % 2.31/2.43 | ~ p2(X31,X36) % 2.31/2.43 | ~ p2(X32,X37) % 2.31/2.43 | ~ p12(X33,X38) % 2.31/2.43 | ~ p12(X34,X39) % 2.31/2.43 | ~ p2(X30,X35) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p25_37,negated_conjecture, % 2.31/2.43 ( p25(f13(f14(X7,f16(f10(X4,f11(X5,X6)),c32,X7))),f13(f14(X7,X3))) % 2.31/2.43 | ~ p22(f3(f4(f5(c26))),X5) % 2.31/2.43 | ~ p23(X3,f8(f10(X4,f11(X5,X6)))) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p25_38,negated_conjecture, % 2.31/2.43 ( p25(f13(f14(X7,f16(f10(X4,f11(X5,X6)),c32,X7))),f18(f20(f10(X4,f11(X5,X6)),X7),f19(f3(f4(f5(c26)))))) % 2.31/2.43 | ~ p22(f3(f4(f5(c26))),X5) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_39,negated_conjecture, % 2.31/2.43 ( p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) % 2.31/2.43 | p23(f21(X4,X5,X6,X7,X3),f8(f10(X4,f11(X5,X6)))) % 2.31/2.43 | ~ p22(f3(f4(f5(c26))),X5) % 2.31/2.43 | ~ p24(f17(f10(X4,f11(X5,X6)),X3)) % 2.31/2.43 | ~ p23(X3,f8(f10(X4,f11(X5,X6)))) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_40,negated_conjecture, % 2.31/2.43 ( p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) % 2.31/2.43 | ~ p22(f3(f4(f5(c26))),X5) % 2.31/2.43 | ~ p24(f17(f10(X4,f11(X5,X6)),X3)) % 2.31/2.43 | ~ p23(X3,f8(f10(X4,f11(X5,X6)))) % 2.31/2.43 | ~ p25(f13(f14(X7,X3)),f13(f14(X7,f21(X4,X5,X6,X7,X3)))) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_41,negated_conjecture, % 2.31/2.43 ( p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) % 2.31/2.43 | p23(f21(X4,X5,X6,X7,X3),f8(f10(X4,f11(X5,X6)))) % 2.31/2.43 | p24(f17(f10(X4,f11(X5,X6)),f16(f10(X4,f11(X5,X6)),c32,X7))) % 2.31/2.43 | ~ p22(f3(f4(f5(c26))),X5) % 2.31/2.43 | ~ p23(X3,f8(f10(X4,f11(X5,X6)))) ) ). % 2.31/2.43 % 2.31/2.43 cnf(p12_42,negated_conjecture, % 2.31/2.43 ( p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) % 2.31/2.43 | p24(f17(f10(X4,f11(X5,X6)),f16(f10(X4,f11(X5,X6)),c32,X7))) % 2.31/2.43 | ~ p22(f3(f4(f5(c26))),X5) % 2.31/2.43 | ~ p23(X3,f8(f10(X4,f11(X5,X6)))) % 2.31/2.43 | ~ p25(f13(f14(X7,X3)),f13(f14(X7,f21(X4,X5,X6,X7,X3)))) ) ). % 2.31/2.43 % 2.31/2.43 %-------------------------------------------------------------------------- % 2.31/2.43 %------------------------------------------- % 2.31/2.43 % Proof found % 2.31/2.43 % SZS status Theorem for theBenchmark % 2.31/2.43 % SZS output start Proof % 2.31/2.43 %ClaNum:42(EqnAxiom:0) % 2.31/2.43 %VarNum:304(SingletonVarNum:123) % 2.31/2.43 %MaxLitNum:6 % 2.31/2.43 %MaxfuncDepth:5 % 2.31/2.43 %SharedTerms:25 % 2.31/2.43 %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 33 34 35 36 37 38 39 40 41 42 % 2.31/2.43 %singleGoalClaCount:11 % 2.31/2.43 [7]P7(f4(f3(f2(a1))),a5) % 2.31/2.43 [8]P8(a6,f21(f10(a7,f9(a5,a8)))) % 2.31/2.43 [10]~P1(a6,f15(f10(a7,f9(a5,a8)),a12,a11)) % 2.31/2.43 [11]~P9(f16(f10(a7,f9(a5,a8)),f15(f10(a7,f9(a5,a8)),a12,a11))) % 2.31/2.43 [9]P1(f14(f13(a11,a6)),f14(f13(a11,f15(f10(a7,f9(a5,a8)),a12,a11)))) % 2.31/2.43 [1]P1(x11,x11) % 2.31/2.43 [2]P2(x21,x21) % 2.31/2.43 [3]P3(x31,x31) % 2.31/2.43 [4]P4(x41,x41) % 2.31/2.43 [5]P5(x51,x51) % 2.31/2.43 [6]P6(x61,x61) % 2.31/2.43 [13]~P1(x131,x132)+P1(f14(x131),f14(x132)) % 2.31/2.43 [14]~P5(x141,x142)+P1(f17(x141),f17(x142)) % 2.31/2.43 [15]~P4(x151,x152)+P3(f21(x151),f21(x152)) % 2.31/2.43 [16]~P5(x161,x162)+P5(f2(x161),f2(x162)) % 2.31/2.43 [17]~P5(x171,x172)+P5(f3(x171),f3(x172)) % 2.31/2.43 [18]~P5(x181,x182)+P5(f4(x181),f4(x182)) % 2.31/2.43 [35]~P7(f4(f3(f2(a1))),x352)+P8(f15(f10(x351,f9(x352,x353)),a12,x354),f21(f10(x351,f9(x352,x353)))) % 2.31/2.43 [37]~P7(f4(f3(f2(a1))),x373)+P10(f14(f13(x371,f15(f10(x372,f9(x373,x374)),a12,x371))),f18(f19(f10(x372,f9(x373,x374)),x371),f17(f4(f3(f2(a1)))))) % 2.31/2.43 [12]~P5(x122,x121)+P9(x121)+~P9(x122) % 2.31/2.43 [19]~P1(x193,x191)+P1(x191,x192)+~P1(x193,x192) % 2.31/2.43 [20]~P2(x203,x201)+P2(x201,x202)+~P2(x203,x202) % 2.31/2.43 [21]~P3(x213,x211)+P3(x211,x212)+~P3(x213,x212) % 2.31/2.43 [22]~P4(x223,x221)+P4(x221,x222)+~P4(x223,x222) % 2.31/2.43 [23]~P5(x233,x231)+P5(x231,x232)+~P5(x233,x232) % 2.31/2.43 [24]~P6(x243,x241)+P6(x241,x242)+~P6(x243,x242) % 2.31/2.43 [28]~P1(x282,x284)+~P1(x281,x283)+P1(f13(x281,x282),f13(x283,x284)) % 2.31/2.43 [29]~P1(x292,x294)+~P4(x291,x293)+P1(f19(x291,x292),f19(x293,x294)) % 2.31/2.43 [30]~P1(x302,x304)+~P1(x301,x303)+P1(f18(x301,x302),f18(x303,x304)) % 2.31/2.43 [31]~P5(x312,x314)+~P5(x311,x313)+P2(f9(x311,x312),f9(x313,x314)) % 2.31/2.43 [32]~P2(x322,x324)+~P5(x321,x323)+P4(f10(x321,x322),f10(x323,x324)) % 2.31/2.43 [33]~P1(x332,x334)+~P4(x331,x333)+P5(f16(x331,x332),f16(x333,x334)) % 2.31/2.43 [36]~P8(x365,f21(f10(x362,f9(x363,x364))))+~P7(f4(f3(f2(a1))),x363)+P10(f14(f13(x361,f15(f10(x362,f9(x363,x364)),a12,x361))),f14(f13(x361,x365))) % 2.31/2.43 [25]~P7(x253,x254)+P7(x251,x252)+~P5(x253,x251)+~P5(x254,x252) % 2.31/2.43 [26]~P8(x263,x264)+P8(x261,x262)+~P1(x263,x261)+~P3(x264,x262) % 2.31/2.43 [27]~P10(x273,x274)+P10(x271,x272)+~P1(x273,x271)+~P1(x274,x272) % 2.31/2.43 [34]~P1(x343,x346)+~P4(x341,x344)+~P6(x342,x345)+P1(f15(x341,x342,x343),f15(x344,x345,x346)) % 2.31/2.43 [38]P8(f20(x382,x383,x384,x385,x381),f21(f10(x382,f9(x383,x384))))+~P8(x381,f21(f10(x382,f9(x383,x384))))+~P7(f4(f3(f2(a1))),x383)+P1(x381,f15(f10(x382,f9(x383,x384)),a12,x385))+~P9(f16(f10(x382,f9(x383,x384)),x381)) % 2.31/2.43 [41]~P10(f14(f13(x415,x411)),f14(f13(x415,f20(x412,x413,x414,x415,x411))))+~P8(x411,f21(f10(x412,f9(x413,x414))))+~P7(f4(f3(f2(a1))),x413)+P1(x411,f15(f10(x412,f9(x413,x414)),a12,x415))+~P9(f16(f10(x412,f9(x413,x414)),x411)) % 2.31/2.43 [39]P8(f20(x392,x393,x394,x395,x391),f21(f10(x392,f9(x393,x394))))+~P8(x391,f21(f10(x392,f9(x393,x394))))+~P7(f4(f3(f2(a1))),x393)+P1(x391,f15(f10(x392,f9(x393,x394)),a12,x395))+P9(f16(f10(x392,f9(x393,x394)),f15(f10(x392,f9(x393,x394)),a12,x395))) % 2.31/2.43 [42]~P10(f14(f13(x425,x421)),f14(f13(x425,f20(x422,x423,x424,x425,x421))))+~P8(x421,f21(f10(x422,f9(x423,x424))))+~P7(f4(f3(f2(a1))),x423)+P1(x421,f15(f10(x422,f9(x423,x424)),a12,x425))+P9(f16(f10(x422,f9(x423,x424)),f15(f10(x422,f9(x423,x424)),a12,x425))) % 2.31/2.43 [40]~P1(x405,x4010)+~P1(x404,x409)+~P5(x403,x408)+~P5(x402,x407)+~P5(x401,x406)+P1(f20(x401,x402,x403,x404,x405),f20(x406,x407,x408,x409,x4010)) % 2.31/2.43 %EqnAxiom % 2.31/2.43 % 2.31/2.43 %------------------------------------------- % 2.31/2.43 cnf(43,plain, % 2.31/2.43 (P8(f20(a7,a5,a8,a11,a6),f21(f10(a7,f9(a5,a8))))), % 2.31/2.43 inference(scs_inference,[],[7,8,10,11,39])). % 2.31/2.43 cnf(45,plain, % 2.31/2.43 (~P10(f14(f13(a11,a6)),f14(f13(a11,f20(a7,a5,a8,a11,a6))))), % 2.31/2.43 inference(scs_inference,[],[7,8,10,11,39,42])). % 2.31/2.43 cnf(63,plain, % 2.31/2.43 (P1(f14(f13(a11,f15(f10(a7,f9(a5,a8)),a12,a11))),f14(f13(a11,a6)))), % 2.31/2.43 inference(scs_inference,[],[9,1,19])). % 2.31/2.43 cnf(329,plain, % 2.31/2.43 (~P5(a5,a5)+P10(f14(f13(x3291,f15(f10(a7,f9(a5,a8)),a12,x3291))),f14(f13(x3291,f20(a7,a5,a8,a11,a6))))), % 2.31/2.43 inference(scs_inference,[],[43,5,7,36,25])). % 2.31/2.43 cnf(330,plain, % 2.31/2.43 (P10(f14(f13(x3301,f15(f10(a7,f9(a5,a8)),a12,x3301))),f14(f13(x3301,f20(a7,a5,a8,a11,a6))))), % 2.31/2.43 inference(scs_inference,[],[5,329])). % 2.31/2.43 cnf(333,plain, % 2.31/2.43 ($false), % 2.31/2.43 inference(scs_inference,[],[1,63,330,45,27]), % 2.31/2.43 ['proof']). % 2.31/2.43 % SZS output end Proof % 2.31/2.43 % Total time :1.790000s %------------------------------------------------------------------------------