%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN673-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n021.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:16 EDT 2024 % Result : Unsatisfiable 58.60s 58.66s % Output : CNFRefutation 58.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SYN673-1 : TPTP v8.2.0. Released v2.5.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n021.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 20:45:38 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 58.60/58.64 %------------------------------------------- % 58.60/58.64 % File :CSE---1.7 % 58.60/58.64 % Problem :theBenchmark % 58.60/58.64 % Transform :cnf % 58.60/58.64 % Format :tptp:raw % 58.60/58.64 % Command :java -jar mcs_scs.jar %d %s % 58.60/58.64 % 58.60/58.64 % Result :Theorem 58.020000s % 58.60/58.64 % Output :CNFRefutation 58.020000s % 58.60/58.64 %------------------------------------------- % 58.60/58.65 %-------------------------------------------------------------------------- % 58.60/58.65 % File : SYN673-1 : TPTP v8.2.0. Released v2.5.0. % 58.60/58.65 % Domain : Syntactic % 58.60/58.65 % Problem : Harrison problem 4552 % 58.60/58.65 % Version : Especial. % 58.60/58.65 % English : % 58.60/58.65 % 58.60/58.65 % Refs : [Har01] Email to G. Sutcliffe % 58.60/58.65 % Source : [Har01] % 58.60/58.65 % Names : % 58.60/58.65 % 58.60/58.65 % Status : Unsatisfiable % 58.60/58.65 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.0.0, 0.12 v6.3.0, 0.00 v6.0.0, 0.14 v5.5.0, 0.12 v5.4.0, 0.30 v5.3.0, 0.20 v5.2.0, 0.30 v5.1.0, 0.27 v5.0.0, 0.36 v4.1.0, 0.12 v4.0.1, 0.00 v2.7.0, 0.38 v2.6.0, 0.33 v2.5.0 % 58.60/58.65 % Syntax : Number of clauses : 55 ( 19 unt; 1 nHn; 39 RR) % 58.60/58.65 % Number of literals : 125 ( 0 equ; 70 neg) % 58.60/58.65 % Maximal clause size : 4 ( 2 avg) % 58.60/58.65 % Maximal term depth : 5 ( 1 avg) % 58.60/58.65 % Number of predicates : 18 ( 18 usr; 0 prp; 2-2 aty) % 58.60/58.65 % Number of functors : 24 ( 24 usr; 14 con; 0-2 aty) % 58.60/58.65 % Number of variables : 124 ( 0 sgn) % 58.60/58.65 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.60/58.65 % 58.60/58.65 % Comments : % 58.60/58.65 %-------------------------------------------------------------------------- % 58.60/58.65 cnf(p10_1,negated_conjecture, % 58.60/58.65 p10(X0,X0) ). % 58.60/58.65 % 58.60/58.65 cnf(p9_2,negated_conjecture, % 58.60/58.65 p9(X102,X102) ). % 58.60/58.65 % 58.60/58.65 cnf(p7_3,negated_conjecture, % 58.60/58.65 p7(X99,X99) ). % 58.60/58.65 % 58.60/58.65 cnf(p6_4,negated_conjecture, % 58.60/58.65 p6(X96,X96) ). % 58.60/58.65 % 58.60/58.65 cnf(p4_5,negated_conjecture, % 58.60/58.65 p4(X81,X81) ). % 58.60/58.65 % 58.60/58.65 cnf(p3_6,negated_conjecture, % 58.60/58.65 p3(X74,X74) ). % 58.60/58.65 % 58.60/58.65 cnf(p25_7,negated_conjecture, % 58.60/58.65 p25(X52,X52) ). % 58.60/58.65 % 58.60/58.65 cnf(p23_8,negated_conjecture, % 58.60/58.65 p23(X49,X49) ). % 58.60/58.65 % 58.60/58.65 cnf(p20_9,negated_conjecture, % 58.60/58.65 p20(X42,X42) ). % 58.60/58.65 % 58.60/58.65 cnf(p2_10,negated_conjecture, % 58.60/58.65 p2(X39,X39) ). % 58.60/58.65 % 58.60/58.65 cnf(p18_11,negated_conjecture, % 58.60/58.65 p18(X36,X36) ). % 58.60/58.65 % 58.60/58.65 cnf(p16_12,negated_conjecture, % 58.60/58.65 p16(X29,X29) ). % 58.60/58.65 % 58.60/58.65 cnf(p15_13,negated_conjecture, % 58.60/58.65 p15(X26,X26) ). % 58.60/58.65 % 58.60/58.65 cnf(p13_14,negated_conjecture, % 58.60/58.65 p13(X19,X19) ). % 58.60/58.65 % 58.60/58.65 cnf(p11_15,negated_conjecture, % 58.60/58.65 p11(X12,X12) ). % 58.60/58.65 % 58.60/58.65 cnf(p10_16,negated_conjecture, % 58.60/58.65 p10(f14(f19(c35,X7),c41),X7) ). % 58.60/58.65 % 58.60/58.65 cnf(not_p29_17,negated_conjecture, % 58.60/58.65 ~ p29(f5(c33,f8(c34,c30)),c38) ). % 58.60/58.65 % 58.60/58.65 cnf(p29_18,negated_conjecture, % 58.60/58.65 ( p29(X60,X59) % 58.60/58.65 | ~ p27(f12(c32,X59),X60) ) ). % 58.60/58.65 % 58.60/58.65 cnf(p27_19,negated_conjecture, % 58.60/58.65 ( p27(f12(c32,X59),X60) % 58.60/58.65 | ~ p29(X60,X59) ) ). % 58.60/58.65 % 58.60/58.65 cnf(p28_20,negated_conjecture, % 58.60/58.65 ( p28(f21(c30,X68),c31) % 58.60/58.65 | ~ p16(X68,c40) ) ). % 58.60/58.65 % 58.60/58.65 cnf(p27_21,negated_conjecture, % 58.60/58.65 p27(f12(c32,c37),f5(c33,f8(c34,c30))) ). % 58.60/58.65 % 58.60/58.65 cnf(p10_22,negated_conjecture, % 58.60/58.65 ( p10(X1,X2) % 58.60/58.65 | ~ p10(X0,X1) % 58.60/58.65 | ~ p10(X0,X2) ) ). % 58.60/58.65 % 58.60/58.65 cnf(p9_23,negated_conjecture, % 58.60/58.65 ( p9(X103,X104) % 58.60/58.65 | ~ p9(X102,X103) % 58.60/58.65 | ~ p9(X102,X104) ) ). % 58.60/58.65 % 58.60/58.65 cnf(p7_24,negated_conjecture, % 58.60/58.65 ( p7(X100,X101) % 58.60/58.65 | ~ p7(X99,X100) % 58.60/58.66 | ~ p7(X99,X101) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p6_25,negated_conjecture, % 58.60/58.66 ( p6(X97,X98) % 58.60/58.66 | ~ p6(X96,X97) % 58.60/58.66 | ~ p6(X96,X98) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p4_26,negated_conjecture, % 58.60/58.66 ( p4(X82,X83) % 58.60/58.66 | ~ p4(X81,X82) % 58.60/58.66 | ~ p4(X81,X83) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p3_27,negated_conjecture, % 58.60/58.66 ( p3(X75,X76) % 58.60/58.66 | ~ p3(X74,X75) % 58.60/58.66 | ~ p3(X74,X76) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p25_28,negated_conjecture, % 58.60/58.66 ( p25(X53,X54) % 58.60/58.66 | ~ p25(X52,X53) % 58.60/58.66 | ~ p25(X52,X54) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p23_29,negated_conjecture, % 58.60/58.66 ( p23(X50,X51) % 58.60/58.66 | ~ p23(X49,X50) % 58.60/58.66 | ~ p23(X49,X51) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p20_30,negated_conjecture, % 58.60/58.66 ( p20(X43,X44) % 58.60/58.66 | ~ p20(X42,X43) % 58.60/58.66 | ~ p20(X42,X44) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p2_31,negated_conjecture, % 58.60/58.66 ( p2(X40,X41) % 58.60/58.66 | ~ p2(X39,X40) % 58.60/58.66 | ~ p2(X39,X41) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p18_32,negated_conjecture, % 58.60/58.66 ( p18(X37,X38) % 58.60/58.66 | ~ p18(X36,X37) % 58.60/58.66 | ~ p18(X36,X38) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p16_33,negated_conjecture, % 58.60/58.66 ( p16(X30,X31) % 58.60/58.66 | ~ p16(X29,X30) % 58.60/58.66 | ~ p16(X29,X31) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p15_34,negated_conjecture, % 58.60/58.66 ( p15(X27,X28) % 58.60/58.66 | ~ p15(X26,X27) % 58.60/58.66 | ~ p15(X26,X28) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p13_35,negated_conjecture, % 58.60/58.66 ( p13(X20,X21) % 58.60/58.66 | ~ p13(X19,X20) % 58.60/58.66 | ~ p13(X19,X21) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p11_36,negated_conjecture, % 58.60/58.66 ( p11(X13,X14) % 58.60/58.66 | ~ p11(X12,X13) % 58.60/58.66 | ~ p11(X12,X14) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p28_37,negated_conjecture, % 58.60/58.66 ( p28(f21(c30,X68),c31) % 58.60/58.66 | ~ p29(f24(c42,X68),c39) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p29_38,negated_conjecture, % 58.60/58.66 ( p29(X69,X70) % 58.60/58.66 | ~ p29(X72,X71) % 58.60/58.66 | ~ p4(X72,X69) % 58.60/58.66 | ~ p10(X71,X70) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p27_39,negated_conjecture, % 58.60/58.66 ( p27(X55,X56) % 58.60/58.66 | ~ p27(X57,X58) % 58.60/58.66 | ~ p4(X58,X56) % 58.60/58.66 | ~ p11(X57,X55) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p28_40,negated_conjecture, % 58.60/58.66 ( p28(X64,X65) % 58.60/58.66 | ~ p20(X67,X64) % 58.60/58.66 | ~ p28(X67,X66) % 58.60/58.66 | ~ p16(X66,X65) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p10_41,negated_conjecture, % 58.60/58.66 p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))) ). % 58.60/58.66 % 58.60/58.66 cnf(p4_42,negated_conjecture, % 58.60/58.66 ( p4(f5(X92,X93),f5(X94,X95)) % 58.60/58.66 | ~ p2(X92,X94) % 58.60/58.66 | ~ p3(X93,X95) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p10_43,negated_conjecture, % 58.60/58.66 ( p10(f14(X3,X4),f14(X5,X6)) % 58.60/58.66 | ~ p10(X4,X6) % 58.60/58.66 | ~ p13(X3,X5) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p10_44,negated_conjecture, % 58.60/58.66 ( p10(f17(X8,X9),f17(X10,X11)) % 58.60/58.66 | ~ p15(X8,X10) % 58.60/58.66 | ~ p16(X9,X11) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p11_45,negated_conjecture, % 58.60/58.66 ( p11(f12(X15,X16),f12(X17,X18)) % 58.60/58.66 | ~ p10(X16,X18) % 58.60/58.66 | ~ p9(X15,X17) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p13_46,negated_conjecture, % 58.60/58.66 ( p13(f19(X22,X23),f19(X24,X25)) % 58.60/58.66 | ~ p10(X23,X25) % 58.60/58.66 | ~ p18(X22,X24) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p16_47,negated_conjecture, % 58.60/58.66 ( p16(f26(X32,X33),f26(X34,X35)) % 58.60/58.66 | ~ p10(X33,X35) % 58.60/58.66 | ~ p25(X32,X34) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p20_48,negated_conjecture, % 58.60/58.66 ( p20(f21(X45,X46),f21(X47,X48)) % 58.60/58.66 | ~ p16(X46,X48) % 58.60/58.66 | ~ p7(X45,X47) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p3_49,negated_conjecture, % 58.60/58.66 ( p3(f8(X77,X78),f8(X79,X80)) % 58.60/58.66 | ~ p6(X77,X79) % 58.60/58.66 | ~ p7(X78,X80) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p4_50,negated_conjecture, % 58.60/58.66 ( p4(f22(X84,X85),f22(X86,X87)) % 58.60/58.66 | ~ p10(X85,X87) % 58.60/58.66 | ~ p3(X84,X86) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p4_51,negated_conjecture, % 58.60/58.66 ( p4(f24(X88,X89),f24(X90,X91)) % 58.60/58.66 | ~ p16(X89,X91) % 58.60/58.66 | ~ p23(X88,X90) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p29_52,negated_conjecture, % 58.60/58.66 ( p29(f24(c42,f26(c43,X73)),c39) % 58.60/58.66 | p29(f5(c33,f8(c34,c30)),X73) % 58.60/58.66 | ~ p10(X73,f14(f19(c35,c37),c39)) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p29_53,negated_conjecture, % 58.60/58.66 ( p29(f5(c33,f8(c34,c30)),X73) % 58.60/58.66 | ~ p10(X73,f14(f19(c35,c37),c39)) % 58.60/58.66 | ~ p28(f21(c30,f26(c43,X73)),c31) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p27_54,negated_conjecture, % 58.60/58.66 ( p27(f12(c32,f14(f19(c35,X63),f17(c36,c31))),f5(c33,f8(c34,c30))) % 58.60/58.66 | ~ p29(f22(f8(c34,c30),X63),c37) ) ). % 58.60/58.66 % 58.60/58.66 cnf(p27_55,negated_conjecture, % 58.60/58.66 ( p27(f12(c32,f14(f19(c35,X61),f17(c36,X62))),f5(c33,f8(c34,c30))) % 58.60/58.66 | ~ p28(f21(c30,X62),c31) % 58.60/58.66 | ~ p27(f12(c32,X61),f5(c33,f8(c34,c30))) ) ). % 58.60/58.66 % 58.60/58.66 %-------------------------------------------------------------------------- % 58.60/58.66 %------------------------------------------- % 58.60/58.66 % Proof found % 58.60/58.66 % SZS status Theorem for theBenchmark % 58.60/58.66 % SZS output start Proof % 58.60/58.66 %ClaNum:55(EqnAxiom:0) % 58.60/58.66 %VarNum:250(SingletonVarNum:124) % 58.60/58.66 %MaxLitNum:4 % 58.60/58.66 %MaxfuncDepth:3 % 58.60/58.66 %SharedTerms:26 % 58.60/58.66 %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 43 44 45 46 47 48 49 50 51 52 53 54 55 % 58.60/58.66 %singleGoalClaCount:19 % 58.60/58.66 [17]P16(f15(a2,a9),f20(a5,f19(a6,a3))) % 58.60/58.66 [18]P1(a11,f14(f7(a1,f14(f7(a1,a9),a12)),f18(a10,a13))) % 58.60/58.66 [19]~P17(f20(a5,f19(a6,a3)),a11) % 58.60/58.66 [1]P1(x11,x11) % 58.60/58.66 [2]P2(x21,x21) % 58.60/58.66 [3]P3(x31,x31) % 58.60/58.66 [4]P4(x41,x41) % 58.60/58.66 [5]P5(x51,x51) % 58.60/58.66 [6]P6(x61,x61) % 58.60/58.66 [7]P7(x71,x71) % 58.60/58.66 [8]P8(x81,x81) % 58.60/58.66 [9]P9(x91,x91) % 58.60/58.66 [10]P10(x101,x101) % 58.60/58.66 [11]P11(x111,x111) % 58.60/58.66 [12]P12(x121,x121) % 58.60/58.66 [13]P13(x131,x131) % 58.60/58.66 [14]P14(x141,x141) % 58.60/58.66 [15]P15(x151,x151) % 58.60/58.66 [16]P1(f14(f7(a1,x161),a8),x161) % 58.60/58.66 [20]~P12(x201,a13)+P18(f21(a3,x201),a4) % 58.60/58.66 [41]~P17(f22(a16,x411),a12)+P18(f21(a3,x411),a4) % 58.60/58.66 [54]~P17(f23(f19(a6,a3),x541),a9)+P16(f15(a2,f14(f7(a1,x541),f18(a10,a4))),f20(a5,f19(a6,a3))) % 58.60/58.66 [36]~P17(x362,x361)+P16(f15(a2,x361),x362) % 58.60/58.66 [37]P17(x371,x372)+~P16(f15(a2,x372),x371) % 58.60/58.66 [52]P17(f20(a5,f19(a6,a3)),x521)+~P1(x521,f14(f7(a1,a9),a12))+P17(f22(a16,f24(a17,x521)),a12) % 58.60/58.66 [53]P17(f20(a5,f19(a6,a3)),x531)+~P1(x531,f14(f7(a1,a9),a12))+~P18(f21(a3,f24(a17,x531)),a4) % 58.60/58.66 [55]~P18(f21(a3,x552),a4)+~P16(f15(a2,x551),f20(a5,f19(a6,a3)))+P16(f15(a2,f14(f7(a1,x551),f18(a10,x552))),f20(a5,f19(a6,a3))) % 58.60/58.66 [21]~P1(x213,x211)+P1(x211,x212)+~P1(x213,x212) % 58.60/58.66 [22]~P2(x223,x221)+P2(x221,x222)+~P2(x223,x222) % 58.60/58.66 [23]~P3(x233,x231)+P3(x231,x232)+~P3(x233,x232) % 58.60/58.66 [24]~P4(x243,x241)+P4(x241,x242)+~P4(x243,x242) % 58.60/58.66 [25]~P5(x253,x251)+P5(x251,x252)+~P5(x253,x252) % 58.60/58.66 [26]~P6(x263,x261)+P6(x261,x262)+~P6(x263,x262) % 58.60/58.66 [27]~P7(x273,x271)+P7(x271,x272)+~P7(x273,x272) % 58.60/58.66 [28]~P8(x283,x281)+P8(x281,x282)+~P8(x283,x282) % 58.60/58.66 [29]~P9(x293,x291)+P9(x291,x292)+~P9(x293,x292) % 58.60/58.66 [30]~P10(x303,x301)+P10(x301,x302)+~P10(x303,x302) % 58.60/58.66 [31]~P11(x313,x311)+P11(x311,x312)+~P11(x313,x312) % 58.60/58.66 [32]~P12(x323,x321)+P12(x321,x322)+~P12(x323,x322) % 58.60/58.66 [33]~P13(x333,x331)+P13(x331,x332)+~P13(x333,x332) % 58.60/58.66 [34]~P14(x343,x341)+P14(x341,x342)+~P14(x343,x342) % 58.60/58.66 [35]~P15(x353,x351)+P15(x351,x352)+~P15(x353,x352) % 58.60/58.66 [42]~P1(x422,x424)+~P14(x421,x423)+P1(f14(x421,x422),f14(x423,x424)) % 58.60/58.66 [43]~P12(x432,x434)+~P13(x431,x433)+P1(f18(x431,x432),f18(x433,x434)) % 58.60/58.66 [44]~P6(x442,x444)+~P10(x441,x443)+P5(f20(x441,x442),f20(x443,x444)) % 58.60/58.66 [45]~P8(x451,x453)+~P12(x452,x454)+P5(f22(x451,x452),f22(x453,x454)) % 58.60/58.66 [46]~P1(x462,x464)+~P6(x461,x463)+P5(f23(x461,x462),f23(x463,x464)) % 58.60/58.66 [47]~P3(x472,x474)+~P4(x471,x473)+P6(f19(x471,x472),f19(x473,x474)) % 58.60/58.66 [48]~P3(x481,x483)+~P12(x482,x484)+P9(f21(x481,x482),f21(x483,x484)) % 58.60/58.66 [49]~P1(x492,x494)+~P7(x491,x493)+P12(f24(x491,x492),f24(x493,x494)) % 58.60/58.66 [50]~P1(x502,x504)+~P11(x501,x503)+P14(f7(x501,x502),f7(x503,x504)) % 58.60/58.66 [51]~P1(x512,x514)+~P2(x511,x513)+P15(f15(x511,x512),f15(x513,x514)) % 58.60/58.66 [38]~P17(x384,x383)+P17(x381,x382)+~P1(x383,x382)+~P5(x384,x381) % 58.60/58.66 [39]~P16(x394,x393)+P16(x391,x392)+~P5(x393,x392)+~P15(x394,x391) % 58.60/58.66 [40]~P18(x403,x404)+P18(x401,x402)+~P9(x403,x401)+~P12(x404,x402) % 58.60/58.66 %EqnAxiom % 58.60/58.66 % 58.60/58.66 %------------------------------------------- % 58.60/58.66 cnf(66,plain, % 58.60/58.66 (P18(f21(a3,a13),a4)), % 58.60/58.66 inference(scs_inference,[],[12,20,32])). % 58.60/58.66 cnf(68,plain, % 58.60/58.66 (P17(f20(a5,f19(a6,a3)),f14(f7(a1,a9),a12))+~P17(f22(a16,f24(a17,f14(f7(a1,a9),a12))),a12)), % 58.60/58.66 inference(scs_inference,[],[1,41,53])). % 58.60/58.66 cnf(104,plain, % 58.60/58.66 (P1(f14(f7(a1,f14(f7(a1,a9),a12)),f18(a10,a13)),a11)), % 58.60/58.66 inference(scs_inference,[],[18,1,21])). % 58.60/58.66 cnf(153,plain, % 58.60/58.66 (~P17(f20(a5,f19(a6,a3)),f14(f7(a1,f14(f7(a1,a9),a12)),f18(a10,a13)))), % 58.60/58.66 inference(scs_inference,[],[5,104,19,38])). % 58.60/58.66 cnf(178,plain, % 58.60/58.66 (P16(f15(a2,f14(f7(a1,a9),a12)),f20(a5,f19(a6,a3)))+P17(f22(a16,f24(a17,f14(f7(a1,a9),a12))),a12)), % 58.60/58.66 inference(scs_inference,[],[1,52,36])). % 58.60/58.66 cnf(198,plain, % 58.60/58.66 (~P16(f15(a2,f14(f7(a1,a9),a12)),f20(a5,f19(a6,a3)))), % 58.60/58.66 inference(scs_inference,[],[153,66,37,55])). % 58.60/58.66 cnf(199,plain, % 58.60/58.66 (P17(f22(a16,f24(a17,f14(f7(a1,a9),a12))),a12)), % 58.60/58.66 inference(scs_inference,[],[198,178])). % 58.60/58.66 cnf(201,plain, % 58.60/58.66 (~P17(f20(a5,f19(a6,a3)),f14(f7(a1,a9),a12))), % 58.60/58.66 inference(scs_inference,[],[198,36])). % 58.60/58.66 cnf(203,plain, % 58.60/58.66 (~P17(f22(a16,f24(a17,f14(f7(a1,a9),a12))),a12)), % 58.60/58.66 inference(scs_inference,[],[201,68])). % 58.60/58.66 cnf(1232,plain, % 58.60/58.66 ($false), % 58.60/58.66 inference(scs_inference,[],[199,203]), % 58.60/58.66 ['proof']). % 58.60/58.66 % SZS output end Proof % 58.60/58.66 % Total time :58.020000s %------------------------------------------------------------------------------