%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN658-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 : 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:14 EDT 2024 % Result : Unsatisfiable 30.78s 30.84s % Output : CNFRefutation 30.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN658-1 : TPTP v8.2.0. Released v2.5.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/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.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sun Jun 23 23:55:09 EDT 2024 % 0.11/0.33 % CPUTime : % 0.18/0.56 start to proof:theBenchmark % 30.68/30.82 %------------------------------------------- % 30.68/30.82 % File :CSE---1.7 % 30.68/30.82 % Problem :theBenchmark % 30.68/30.82 % Transform :cnf % 30.68/30.82 % Format :tptp:raw % 30.68/30.82 % Command :java -jar mcs_scs.jar %d %s % 30.68/30.82 % 30.68/30.82 % Result :Theorem 30.220000s % 30.68/30.82 % Output :CNFRefutation 30.220000s % 30.68/30.82 %------------------------------------------- % 30.78/30.83 %-------------------------------------------------------------------------- % 30.78/30.83 % File : SYN658-1 : TPTP v8.2.0. Released v2.5.0. % 30.78/30.83 % Domain : Syntactic % 30.78/30.83 % Problem : Harrison problem 4501 % 30.78/30.83 % Version : Especial. % 30.78/30.83 % English : % 30.78/30.83 % 30.78/30.83 % Refs : [Har01] Email to G. Sutcliffe % 30.78/30.83 % Source : [Har01] % 30.78/30.83 % Names : % 30.78/30.83 % 30.78/30.83 % Status : Unsatisfiable % 30.78/30.83 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.25 v6.3.0, 0.29 v6.2.0, 0.22 v6.1.0, 0.14 v5.5.0, 0.38 v5.4.0, 0.40 v5.2.0, 0.30 v5.1.0, 0.27 v5.0.0, 0.43 v4.1.0, 0.25 v4.0.1, 0.40 v4.0.0, 0.43 v3.4.0, 0.25 v3.3.0, 0.33 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 30.78/30.83 % Syntax : Number of clauses : 50 ( 20 unt; 3 nHn; 42 RR) % 30.78/30.83 % Number of literals : 108 ( 0 equ; 57 neg) % 30.78/30.83 % Maximal clause size : 4 ( 2 avg) % 30.78/30.83 % Maximal term depth : 7 ( 1 avg) % 30.78/30.83 % Number of predicates : 10 ( 10 usr; 0 prp; 2-2 aty) % 30.78/30.83 % Number of functors : 25 ( 25 usr; 10 con; 0-3 aty) % 30.78/30.83 % Number of variables : 102 ( 2 sgn) % 30.78/30.83 % SPC : CNF_UNS_RFO_NEQ_NHN % 30.78/30.83 % 30.78/30.83 % Comments : % 30.78/30.83 %-------------------------------------------------------------------------- % 30.78/30.83 cnf(p17_1,negated_conjecture, % 30.78/30.83 p17(X0,X0) ). % 30.78/30.83 % 30.78/30.83 cnf(p7_2,negated_conjecture, % 30.78/30.83 p7(X85,X85) ). % 30.78/30.83 % 30.78/30.83 cnf(p6_3,negated_conjecture, % 30.78/30.83 p6(X71,X71) ). % 30.78/30.83 % 30.78/30.83 cnf(p4_4,negated_conjecture, % 30.78/30.83 p4(X36,X36) ). % 30.78/30.83 % 30.78/30.83 cnf(p3_5,negated_conjecture, % 30.78/30.83 p3(X33,X33) ). % 30.78/30.83 % 30.78/30.83 cnf(p2_6,negated_conjecture, % 30.78/30.83 p2(X5,X5) ). % 30.78/30.83 % 30.78/30.83 cnf(p24_7,negated_conjecture, % 30.78/30.83 p24(c32,c31) ). % 30.78/30.83 % 30.78/30.83 cnf(p26_8,negated_conjecture, % 30.78/30.83 p26(c32,c31) ). % 30.78/30.83 % 30.78/30.83 cnf(p26_9,negated_conjecture, % 30.78/30.83 p26(c31,c35) ). % 30.78/30.83 % 30.78/30.83 cnf(p24_10,negated_conjecture, % 30.78/30.83 p24(c32,c34) ). % 30.78/30.83 % 30.78/30.83 cnf(not_p6_11,negated_conjecture, % 30.78/30.83 ~ p6(c28,f10(c33)) ). % 30.78/30.83 % 30.78/30.83 cnf(p23_12,negated_conjecture, % 30.78/30.83 p23(f10(f11(f12(c33))),c28) ). % 30.78/30.83 % 30.78/30.83 cnf(p25_13,negated_conjecture, % 30.78/30.83 p25(c35,f18(f8(c27,f9(c28,c29)))) ). % 30.78/30.83 % 30.78/30.83 cnf(p25_14,negated_conjecture, % 30.78/30.83 p25(c32,f18(f8(c27,f9(c28,c29)))) ). % 30.78/30.83 % 30.78/30.83 cnf(p6_15,negated_conjecture, % 30.78/30.83 p6(f21(f8(X82,f9(X83,X84))),X83) ). % 30.78/30.83 % 30.78/30.83 cnf(p17_16,negated_conjecture, % 30.78/30.83 ( p17(f18(X3),f18(X4)) % 30.78/30.83 | ~ p2(X3,X4) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p6_17,negated_conjecture, % 30.78/30.83 ( p6(f21(X80),f21(X81)) % 30.78/30.83 | ~ p2(X80,X81) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p6_18,negated_conjecture, % 30.78/30.83 ( p6(f12(X78),f12(X79)) % 30.78/30.83 | ~ p6(X78,X79) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p6_19,negated_conjecture, % 30.78/30.83 ( p6(f11(X76),f11(X77)) % 30.78/30.83 | ~ p6(X76,X77) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p6_20,negated_conjecture, % 30.78/30.83 ( p6(f10(X74),f10(X75)) % 30.78/30.83 | ~ p6(X74,X75) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p4_21,negated_conjecture, % 30.78/30.83 ( p4(f19(X53),f19(X54)) % 30.78/30.83 | ~ p4(X53,X54) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p4_22,negated_conjecture, % 30.78/30.83 ( p4(f15(X47),f15(X48)) % 30.78/30.83 | ~ p6(X47,X48) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p17_23,negated_conjecture, % 30.78/30.83 ( p17(X1,X2) % 30.78/30.83 | ~ p17(X0,X1) % 30.78/30.83 | ~ p17(X0,X2) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p7_24,negated_conjecture, % 30.78/30.83 ( p7(X86,X87) % 30.78/30.83 | ~ p7(X85,X86) % 30.78/30.83 | ~ p7(X85,X87) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p6_25,negated_conjecture, % 30.78/30.83 ( p6(X72,X73) % 30.78/30.83 | ~ p6(X71,X72) % 30.78/30.83 | ~ p6(X71,X73) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p4_26,negated_conjecture, % 30.78/30.83 ( p4(X37,X38) % 30.78/30.83 | ~ p4(X36,X37) % 30.78/30.83 | ~ p4(X36,X38) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p3_27,negated_conjecture, % 30.78/30.83 ( p3(X34,X35) % 30.78/30.83 | ~ p3(X33,X34) % 30.78/30.83 | ~ p3(X33,X35) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p2_28,negated_conjecture, % 30.78/30.83 ( p2(X6,X7) % 30.78/30.83 | ~ p2(X5,X6) % 30.78/30.83 | ~ p2(X5,X7) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p4_29,negated_conjecture, % 30.78/30.83 p4(f5(f8(c27,f9(c28,c29)),c30,c31),c32) ). % 30.78/30.83 % 30.78/30.83 cnf(p4_30,negated_conjecture, % 30.78/30.83 p4(c35,f13(c32,f16(f8(c27,f9(c28,c29)),c31))) ). % 30.78/30.83 % 30.78/30.83 cnf(p23_31,negated_conjecture, % 30.78/30.83 ( p23(X12,X13) % 30.78/30.83 | ~ p6(X14,X12) % 30.78/30.83 | ~ p6(X15,X13) % 30.78/30.83 | ~ p23(X14,X15) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p26_32,negated_conjecture, % 30.78/30.83 ( p26(X28,X29) % 30.78/30.83 | ~ p4(X30,X28) % 30.78/30.83 | ~ p4(X31,X29) % 30.78/30.83 | ~ p26(X30,X31) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p25_33,negated_conjecture, % 30.78/30.83 ( p25(X21,X22) % 30.78/30.83 | ~ p25(X24,X23) % 30.78/30.83 | ~ p4(X24,X21) % 30.78/30.83 | ~ p17(X23,X22) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p24_34,negated_conjecture, % 30.78/30.83 ( p24(X16,X17) % 30.78/30.83 | ~ p4(X18,X16) % 30.78/30.83 | ~ p4(X19,X17) % 30.78/30.83 | ~ p24(X18,X19) ) ). % 30.78/30.83 % 30.78/30.83 cnf(p2_35,negated_conjecture, % 30.78/30.83 ( p2(f8(X8,X9),f8(X10,X11)) % 30.78/30.83 | ~ p6(X8,X10) % 30.78/30.84 | ~ p7(X9,X11) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p7_36,negated_conjecture, % 30.78/30.84 ( p7(f9(X88,X89),f9(X90,X91)) % 30.78/30.84 | ~ p6(X88,X90) % 30.78/30.84 | ~ p6(X89,X91) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p4_37,negated_conjecture, % 30.78/30.84 ( p4(f20(X55,X56),f20(X57,X58)) % 30.78/30.84 | ~ p4(X55,X57) % 30.78/30.84 | ~ p4(X56,X58) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p4_38,negated_conjecture, % 30.78/30.84 ( p4(f16(X49,X50),f16(X51,X52)) % 30.78/30.84 | ~ p2(X49,X51) % 30.78/30.84 | ~ p4(X50,X52) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p4_39,negated_conjecture, % 30.78/30.84 ( p4(f14(X43,X44),f14(X45,X46)) % 30.78/30.84 | ~ p4(X43,X45) % 30.78/30.84 | ~ p4(X44,X46) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p4_40,negated_conjecture, % 30.78/30.84 ( p4(f13(X39,X40),f13(X41,X42)) % 30.78/30.84 | ~ p4(X39,X41) % 30.78/30.84 | ~ p4(X40,X42) ) ). % 30.78/30.84 % 30.78/30.84 cnf(not_p24_41,negated_conjecture, % 30.78/30.84 ( ~ p24(X92,c35) % 30.78/30.84 | ~ p24(c32,X92) % 30.78/30.84 | ~ p25(X92,f18(f8(c27,f9(c28,c29)))) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p4_42,negated_conjecture, % 30.78/30.84 p4(f16(f8(c27,f9(c28,c29)),c34),f16(f8(c27,f9(c28,c29)),c31)) ). % 30.78/30.84 % 30.78/30.84 cnf(p24_43,negated_conjecture, % 30.78/30.84 p24(c34,f13(c32,f14(f16(f8(c27,f9(c28,c29)),c31),f15(f10(f11(f12(c33))))))) ). % 30.78/30.84 % 30.78/30.84 cnf(not_p4_44,negated_conjecture, % 30.78/30.84 ~ p4(f5(f8(c27,f9(c28,c29)),c36,c31),f5(f8(c27,f9(c28,c29)),c36,c34)) ). % 30.78/30.84 % 30.78/30.84 cnf(p24_45,negated_conjecture, % 30.78/30.84 ( p24(f19(f20(c34,c31)),f19(f20(c34,X20))) % 30.78/30.84 | ~ p25(X20,f18(f8(c27,f9(c28,c29)))) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p4_46,negated_conjecture, % 30.78/30.84 ( p4(f5(X65,X66,X67),f5(X68,X69,X70)) % 30.78/30.84 | ~ p3(X66,X69) % 30.78/30.84 | ~ p4(X67,X70) % 30.78/30.84 | ~ p2(X65,X68) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p4_47,negated_conjecture, % 30.78/30.84 ( p4(f22(X59,X60,X61),f22(X62,X63,X64)) % 30.78/30.84 | ~ p4(X60,X63) % 30.78/30.84 | ~ p4(X61,X64) % 30.78/30.84 | ~ p2(X59,X62) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p6_48,negated_conjecture, % 30.78/30.84 ( p6(f21(X25),f10(c33)) % 30.78/30.84 | p25(f22(X25,X26,X27),f18(X25)) % 30.78/30.84 | p4(f5(X25,c36,X26),f5(X25,c36,X27)) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p6_49,negated_conjecture, % 30.78/30.84 ( p6(f21(X25),f10(c33)) % 30.78/30.84 | p4(f5(X25,c36,X26),f5(X25,c36,X27)) % 30.78/30.84 | ~ p24(f19(f20(X26,X27)),f19(f20(X26,f22(X25,X26,X27)))) ) ). % 30.78/30.84 % 30.78/30.84 cnf(p26_50,negated_conjecture, % 30.78/30.84 ( p26(f19(f20(c31,c32)),f19(f20(c31,X32))) % 30.78/30.84 | p26(f19(f20(c31,c35)),f19(f20(c31,X32))) % 30.78/30.84 | ~ p25(X32,f18(f8(c27,f9(c28,c29)))) ) ). % 30.78/30.84 % 30.78/30.84 %-------------------------------------------------------------------------- % 30.78/30.84 %------------------------------------------- % 30.78/30.84 % Proof found % 30.78/30.84 % SZS status Theorem for theBenchmark % 30.78/30.84 % SZS output start Proof % 30.78/30.84 %ClaNum:50(EqnAxiom:0) % 30.78/30.84 %VarNum:212(SingletonVarNum:102) % 30.78/30.84 %MaxLitNum:4 % 30.78/30.84 %MaxfuncDepth:6 % 30.78/30.84 %SharedTerms:45 % 30.78/30.84 %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 % 30.78/30.84 %singleGoalClaCount:20 % 30.78/30.84 [1]P1(a1,a2) % 30.78/30.84 [2]P1(a1,a7) % 30.78/30.84 [3]P5(a1,a2) % 30.78/30.84 [4]P5(a2,a9) % 30.78/30.84 [19]~P8(a3,f12(a8)) % 30.78/30.84 [11]P4(f12(f11(f10(a8))),a3) % 30.78/30.84 [12]P6(a1,f16(f15(a4,f14(a3,a5)))) % 30.78/30.84 [13]P6(a9,f16(f15(a4,f14(a3,a5)))) % 30.78/30.84 [15]P9(f24(f15(a4,f14(a3,a5)),a6,a2),a1) % 30.78/30.84 [16]P9(f17(f15(a4,f14(a3,a5)),a7),f17(f15(a4,f14(a3,a5)),a2)) % 30.78/30.84 [20]~P9(f24(f15(a4,f14(a3,a5)),a13,a2),f24(f15(a4,f14(a3,a5)),a13,a7)) % 30.78/30.84 [17]P9(a9,f18(a1,f17(f15(a4,f14(a3,a5)),a2))) % 30.78/30.84 [18]P1(a7,f18(a1,f20(f17(f15(a4,f14(a3,a5)),a2),f19(f12(f11(f10(a8))))))) % 30.78/30.84 [5]P2(x51,x51) % 30.78/30.84 [6]P7(x61,x61) % 30.78/30.84 [7]P8(x71,x71) % 30.78/30.84 [8]P9(x81,x81) % 30.78/30.84 [9]P10(x91,x91) % 30.78/30.84 [10]P3(x101,x101) % 30.78/30.84 [14]P8(f21(f15(x141,f14(x142,x143))),x142) % 30.78/30.84 [47]P1(f22(f23(a7,a2)),f22(f23(a7,x471)))+~P6(x471,f16(f15(a4,f14(a3,a5)))) % 30.78/30.84 [21]~P3(x211,x212)+P2(f16(x211),f16(x212)) % 30.78/30.84 [22]~P8(x221,x222)+P8(f12(x221),f12(x222)) % 30.78/30.84 [23]~P8(x231,x232)+P8(f10(x231),f10(x232)) % 30.78/30.84 [24]~P8(x241,x242)+P8(f11(x241),f11(x242)) % 30.78/30.84 [25]~P3(x251,x252)+P8(f21(x251),f21(x252)) % 30.78/30.84 [26]~P9(x261,x262)+P9(f22(x261),f22(x262)) % 30.78/30.84 [27]~P8(x271,x272)+P9(f19(x271),f19(x272)) % 30.78/30.84 [44]~P1(a1,x441)+~P1(x441,a9)+~P6(x441,f16(f15(a4,f14(a3,a5)))) % 30.78/30.84 [49]P5(f22(f23(a2,a1)),f22(f23(a2,x491)))+P5(f22(f23(a2,a9)),f22(f23(a2,x491)))+~P6(x491,f16(f15(a4,f14(a3,a5)))) % 30.78/30.84 [28]~P2(x283,x281)+P2(x281,x282)+~P2(x283,x282) % 30.78/30.84 [29]~P7(x293,x291)+P7(x291,x292)+~P7(x293,x292) % 30.78/30.84 [30]~P8(x303,x301)+P8(x301,x302)+~P8(x303,x302) % 30.78/30.84 [31]~P9(x313,x311)+P9(x311,x312)+~P9(x313,x312) % 30.78/30.84 [32]~P10(x323,x321)+P10(x321,x322)+~P10(x323,x322) % 30.78/30.84 [33]~P3(x333,x331)+P3(x331,x332)+~P3(x333,x332) % 30.78/30.84 [48]P6(f25(x481,x482,x483),f16(x481))+P9(f24(x481,a13,x482),f24(x481,a13,x483))+P8(f21(x481),f12(a8)) % 30.78/30.84 [50]P9(f24(x501,a13,x502),f24(x501,a13,x503))+P8(f21(x501),f12(a8))+~P1(f22(f23(x502,x503)),f22(f23(x502,f25(x501,x502,x503)))) % 30.78/30.84 [38]~P8(x382,x384)+~P8(x381,x383)+P7(f14(x381,x382),f14(x383,x384)) % 30.78/30.84 [39]~P9(x392,x394)+~P3(x391,x393)+P9(f17(x391,x392),f17(x393,x394)) % 30.78/30.84 [40]~P9(x402,x404)+~P9(x401,x403)+P9(f18(x401,x402),f18(x403,x404)) % 30.78/30.84 [41]~P9(x412,x414)+~P9(x411,x413)+P9(f23(x411,x412),f23(x413,x414)) % 30.78/30.84 [42]~P9(x422,x424)+~P9(x421,x423)+P9(f20(x421,x422),f20(x423,x424)) % 30.78/30.84 [43]~P7(x432,x434)+~P8(x431,x433)+P3(f15(x431,x432),f15(x433,x434)) % 30.78/30.84 [34]~P1(x344,x343)+P1(x341,x342)+~P9(x343,x342)+~P9(x344,x341) % 30.78/30.84 [35]~P5(x354,x353)+P5(x351,x352)+~P9(x353,x352)+~P9(x354,x351) % 30.78/30.84 [36]~P4(x364,x363)+P4(x361,x362)+~P8(x363,x362)+~P8(x364,x361) % 30.78/30.84 [37]~P6(x374,x373)+P6(x371,x372)+~P2(x373,x372)+~P9(x374,x371) % 30.78/30.84 [45]~P9(x453,x456)+~P10(x452,x455)+~P3(x451,x454)+P9(f24(x451,x452,x453),f24(x454,x455,x456)) % 30.78/30.84 [46]~P9(x463,x466)+~P9(x462,x465)+~P3(x461,x464)+P9(f25(x461,x462,x463),f25(x464,x465,x466)) % 30.78/30.84 %EqnAxiom % 30.78/30.84 % 30.78/30.84 %------------------------------------------- % 30.78/30.84 cnf(70,plain, % 30.78/30.84 (P8(x701,f21(f15(x702,f14(x701,x703))))), % 30.78/30.84 inference(scs_inference,[],[14,13,7,47,30])). % 30.78/30.84 cnf(88,plain, % 30.78/30.84 (P8(f21(f15(x881,f14(f21(f15(x882,f14(x883,x884))),x885))),x883)), % 30.78/30.84 inference(scs_inference,[],[70,14,30])). % 30.78/30.84 cnf(336,plain, % 30.78/30.84 (~P9(f24(f15(a4,f14(a3,a5)),a13,a7),f24(f15(a4,f14(a3,a5)),a13,a2))), % 30.78/30.84 inference(scs_inference,[],[20,8,31])). % 30.78/30.84 cnf(399,plain, % 30.78/30.84 (P9(f24(x3991,x3992,f24(x3993,a13,x3994)),f24(x3991,x3992,f24(x3993,a13,x3995)))+P8(f21(x3993),f12(a8))+~P1(f22(f23(x3994,x3995)),f22(f23(x3994,f25(x3993,x3994,x3995))))), % 30.78/30.84 inference(scs_inference,[],[9,10,50,45])). % 30.78/30.84 cnf(401,plain, % 30.78/30.84 (P9(f24(x4011,x4012,f24(x4013,a13,a7)),f24(x4011,x4012,f24(x4013,a13,a2)))+P8(f21(x4013),f12(a8))+~P6(f25(x4013,a7,a2),f16(f15(a4,f14(a3,a5))))), % 30.78/30.84 inference(scs_inference,[],[399,47])). % 30.78/30.84 cnf(551,plain, % 30.78/30.84 (P8(f10(f21(f15(a4,f14(a3,a5)))),f10(f12(a8)))+~P1(f22(f23(a7,a2)),f22(f23(a7,f25(f15(a4,f14(a3,a5)),a7,a2))))), % 30.78/30.84 inference(scs_inference,[],[336,23,50])). % 30.78/30.84 cnf(552,plain, % 30.78/30.84 (P8(f10(f21(f15(a4,f14(a3,a5)))),f10(f12(a8)))+~P6(f25(f15(a4,f14(a3,a5)),a7,a2),f16(f15(a4,f14(a3,a5))))), % 30.78/30.84 inference(scs_inference,[],[551,47])). % 30.78/30.84 cnf(712,plain, % 30.78/30.84 (P8(f11(f21(f15(a4,f14(a3,a5)))),f11(f12(a8)))+~P1(f22(f23(a7,a2)),f22(f23(a7,f25(f15(a4,f14(a3,a5)),a7,a2))))), % 30.78/30.84 inference(scs_inference,[],[336,24,50])). % 30.78/30.84 cnf(713,plain, % 30.78/30.84 (P8(f11(f21(f15(a4,f14(a3,a5)))),f11(f12(a8)))+~P6(f25(f15(a4,f14(a3,a5)),a7,a2),f16(f15(a4,f14(a3,a5))))), % 30.78/30.84 inference(scs_inference,[],[712,47])). % 30.78/30.84 cnf(714,plain, % 30.78/30.84 (~P6(f25(f15(a4,f14(a3,a5)),a7,a2),f16(f15(a4,f14(a3,a5))))+P3(f15(f11(f21(f15(a4,f14(a3,a5)))),x7141),f15(f11(f12(a8)),x7141))), % 30.78/30.84 inference(scs_inference,[],[6,713,43])). % 30.78/30.84 cnf(854,plain, % 30.78/30.84 (P9(f19(f21(f15(a4,f14(a3,a5)))),f19(f12(a8)))+~P1(f22(f23(a7,a2)),f22(f23(a7,f25(f15(a4,f14(a3,a5)),a7,a2))))), % 30.78/30.84 inference(scs_inference,[],[336,27,50])). % 30.78/30.84 cnf(855,plain, % 30.78/30.84 (P9(f19(f21(f15(a4,f14(a3,a5)))),f19(f12(a8)))+~P6(f25(f15(a4,f14(a3,a5)),a7,a2),f16(f15(a4,f14(a3,a5))))), % 30.78/30.84 inference(scs_inference,[],[854,47])). % 30.78/30.84 cnf(1147,plain, % 30.78/30.84 (~P8(f12(a8),a3)), % 30.78/30.84 inference(scs_inference,[],[7,19,30])). % 30.78/30.84 cnf(1150,plain, % 30.78/30.84 (~P8(f21(f15(x11501,f14(f21(f15(x11502,f14(a3,x11503))),x11504))),f12(a8))), % 30.78/30.84 inference(scs_inference,[],[88,1147,30])). % 30.78/30.84 cnf(1154,plain, % 30.78/30.84 (~P8(f12(a8),f21(f15(x11541,f14(f21(f15(x11542,f14(a3,x11543))),x11544))))), % 30.78/30.84 inference(scs_inference,[],[1150,7,30])). % 30.78/30.84 cnf(1158,plain, % 30.78/30.84 (~P8(f21(f15(x11581,f14(a3,x11582))),f12(a8))), % 30.78/30.84 inference(scs_inference,[],[70,1154,30])). % 30.78/30.84 cnf(1161,plain, % 30.78/30.84 (P6(f25(f15(a4,f14(a3,a5)),a7,a2),f16(f15(a4,f14(a3,a5))))), % 30.78/30.84 inference(scs_inference,[],[70,336,1154,30,48])). % 30.78/30.84 cnf(1170,plain, % 30.78/30.84 (P1(f22(f23(a7,a2)),f22(f23(a7,f25(f15(a4,f14(a3,a5)),a7,a2))))), % 30.78/30.84 inference(scs_inference,[],[70,336,1154,30,48,399,401,552,713,855,47])). % 30.78/30.84 cnf(1180,plain, % 30.78/30.84 (P3(f15(f11(f21(f15(a4,f14(a3,a5)))),x11801),f15(f11(f12(a8)),x11801))), % 30.78/30.84 inference(scs_inference,[],[1161,714])). % 30.78/30.84 cnf(1186,plain, % 30.78/30.84 ($false), % 30.78/30.84 inference(scs_inference,[],[336,1170,1180,1158,10,33,50]), % 30.78/30.84 ['proof']). % 30.78/30.84 % SZS output end Proof % 30.78/30.84 % Total time :30.220000s %------------------------------------------------------------------------------