%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN657-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:13 EDT 2024 % Result : Unsatisfiable 8.09s 8.17s % Output : CNFRefutation 8.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYN657-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.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 21:58:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.55 start to proof:theBenchmark % 8.09/8.16 %------------------------------------------- % 8.09/8.16 % File :CSE---1.7 % 8.09/8.16 % Problem :theBenchmark % 8.09/8.16 % Transform :cnf % 8.09/8.16 % Format :tptp:raw % 8.09/8.16 % Command :java -jar mcs_scs.jar %d %s % 8.09/8.16 % 8.09/8.16 % Result :Theorem 7.560000s % 8.09/8.16 % Output :CNFRefutation 7.560000s % 8.09/8.16 %------------------------------------------- % 8.09/8.16 %-------------------------------------------------------------------------- % 8.09/8.16 % File : SYN657-1 : TPTP v8.2.0. Released v2.5.0. % 8.09/8.16 % Domain : Syntactic % 8.09/8.16 % Problem : Harrison problem 4500 % 8.09/8.16 % Version : Especial. % 8.09/8.16 % English : % 8.09/8.16 % 8.09/8.16 % Refs : [Har01] Email to G. Sutcliffe % 8.09/8.16 % Source : [Har01] % 8.09/8.16 % Names : % 8.09/8.16 % 8.09/8.16 % Status : Unsatisfiable % 8.09/8.16 % Rating : 0.08 v8.2.0, 0.14 v8.1.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.25 v5.4.0, 0.40 v5.2.0, 0.20 v5.1.0, 0.18 v5.0.0, 0.36 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 % 8.09/8.16 % Syntax : Number of clauses : 50 ( 20 unt; 3 nHn; 42 RR) % 8.09/8.16 % Number of literals : 108 ( 0 equ; 57 neg) % 8.09/8.16 % Maximal clause size : 4 ( 2 avg) % 8.09/8.16 % Maximal term depth : 7 ( 1 avg) % 8.09/8.16 % Number of predicates : 10 ( 10 usr; 0 prp; 2-2 aty) % 8.09/8.16 % Number of functors : 25 ( 25 usr; 10 con; 0-3 aty) % 8.09/8.16 % Number of variables : 102 ( 2 sgn) % 8.09/8.16 % SPC : CNF_UNS_RFO_NEQ_NHN % 8.09/8.16 % 8.09/8.16 % Comments : % 8.09/8.16 %-------------------------------------------------------------------------- % 8.09/8.16 cnf(p17_1,negated_conjecture, % 8.09/8.16 p17(X0,X0) ). % 8.09/8.16 % 8.09/8.16 cnf(p7_2,negated_conjecture, % 8.09/8.16 p7(X85,X85) ). % 8.09/8.16 % 8.09/8.16 cnf(p6_3,negated_conjecture, % 8.09/8.17 p6(X71,X71) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_4,negated_conjecture, % 8.09/8.17 p4(X36,X36) ). % 8.09/8.17 % 8.09/8.17 cnf(p3_5,negated_conjecture, % 8.09/8.17 p3(X33,X33) ). % 8.09/8.17 % 8.09/8.17 cnf(p2_6,negated_conjecture, % 8.09/8.17 p2(X5,X5) ). % 8.09/8.17 % 8.09/8.17 cnf(p24_7,negated_conjecture, % 8.09/8.17 p24(c32,c31) ). % 8.09/8.17 % 8.09/8.17 cnf(p26_8,negated_conjecture, % 8.09/8.17 p26(c32,c31) ). % 8.09/8.17 % 8.09/8.17 cnf(p26_9,negated_conjecture, % 8.09/8.17 p26(c31,c35) ). % 8.09/8.17 % 8.09/8.17 cnf(p24_10,negated_conjecture, % 8.09/8.17 p24(c32,c34) ). % 8.09/8.17 % 8.09/8.17 cnf(not_p6_11,negated_conjecture, % 8.09/8.17 ~ p6(c28,f10(c33)) ). % 8.09/8.17 % 8.09/8.17 cnf(p23_12,negated_conjecture, % 8.09/8.17 p23(f10(f11(f12(c33))),c28) ). % 8.09/8.17 % 8.09/8.17 cnf(p25_13,negated_conjecture, % 8.09/8.17 p25(c35,f18(f8(c27,f9(c28,c29)))) ). % 8.09/8.17 % 8.09/8.17 cnf(p25_14,negated_conjecture, % 8.09/8.17 p25(c32,f18(f8(c27,f9(c28,c29)))) ). % 8.09/8.17 % 8.09/8.17 cnf(p6_15,negated_conjecture, % 8.09/8.17 p6(f21(f8(X82,f9(X83,X84))),X83) ). % 8.09/8.17 % 8.09/8.17 cnf(p17_16,negated_conjecture, % 8.09/8.17 ( p17(f18(X3),f18(X4)) % 8.09/8.17 | ~ p2(X3,X4) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p6_17,negated_conjecture, % 8.09/8.17 ( p6(f21(X80),f21(X81)) % 8.09/8.17 | ~ p2(X80,X81) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p6_18,negated_conjecture, % 8.09/8.17 ( p6(f12(X78),f12(X79)) % 8.09/8.17 | ~ p6(X78,X79) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p6_19,negated_conjecture, % 8.09/8.17 ( p6(f11(X76),f11(X77)) % 8.09/8.17 | ~ p6(X76,X77) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p6_20,negated_conjecture, % 8.09/8.17 ( p6(f10(X74),f10(X75)) % 8.09/8.17 | ~ p6(X74,X75) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_21,negated_conjecture, % 8.09/8.17 ( p4(f19(X53),f19(X54)) % 8.09/8.17 | ~ p4(X53,X54) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_22,negated_conjecture, % 8.09/8.17 ( p4(f15(X47),f15(X48)) % 8.09/8.17 | ~ p6(X47,X48) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p17_23,negated_conjecture, % 8.09/8.17 ( p17(X1,X2) % 8.09/8.17 | ~ p17(X0,X1) % 8.09/8.17 | ~ p17(X0,X2) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p7_24,negated_conjecture, % 8.09/8.17 ( p7(X86,X87) % 8.09/8.17 | ~ p7(X85,X86) % 8.09/8.17 | ~ p7(X85,X87) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p6_25,negated_conjecture, % 8.09/8.17 ( p6(X72,X73) % 8.09/8.17 | ~ p6(X71,X72) % 8.09/8.17 | ~ p6(X71,X73) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_26,negated_conjecture, % 8.09/8.17 ( p4(X37,X38) % 8.09/8.17 | ~ p4(X36,X37) % 8.09/8.17 | ~ p4(X36,X38) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p3_27,negated_conjecture, % 8.09/8.17 ( p3(X34,X35) % 8.09/8.17 | ~ p3(X33,X34) % 8.09/8.17 | ~ p3(X33,X35) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p2_28,negated_conjecture, % 8.09/8.17 ( p2(X6,X7) % 8.09/8.17 | ~ p2(X5,X6) % 8.09/8.17 | ~ p2(X5,X7) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_29,negated_conjecture, % 8.09/8.17 p4(f5(f8(c27,f9(c28,c29)),c30,c31),c32) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_30,negated_conjecture, % 8.09/8.17 p4(c35,f13(c32,f16(f8(c27,f9(c28,c29)),c31))) ). % 8.09/8.17 % 8.09/8.17 cnf(p23_31,negated_conjecture, % 8.09/8.17 ( p23(X12,X13) % 8.09/8.17 | ~ p6(X14,X12) % 8.09/8.17 | ~ p6(X15,X13) % 8.09/8.17 | ~ p23(X14,X15) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p26_32,negated_conjecture, % 8.09/8.17 ( p26(X28,X29) % 8.09/8.17 | ~ p4(X30,X28) % 8.09/8.17 | ~ p4(X31,X29) % 8.09/8.17 | ~ p26(X30,X31) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p25_33,negated_conjecture, % 8.09/8.17 ( p25(X21,X22) % 8.09/8.17 | ~ p25(X24,X23) % 8.09/8.17 | ~ p4(X24,X21) % 8.09/8.17 | ~ p17(X23,X22) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p24_34,negated_conjecture, % 8.09/8.17 ( p24(X16,X17) % 8.09/8.17 | ~ p4(X18,X16) % 8.09/8.17 | ~ p4(X19,X17) % 8.09/8.17 | ~ p24(X18,X19) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p2_35,negated_conjecture, % 8.09/8.17 ( p2(f8(X8,X9),f8(X10,X11)) % 8.09/8.17 | ~ p6(X8,X10) % 8.09/8.17 | ~ p7(X9,X11) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p7_36,negated_conjecture, % 8.09/8.17 ( p7(f9(X88,X89),f9(X90,X91)) % 8.09/8.17 | ~ p6(X88,X90) % 8.09/8.17 | ~ p6(X89,X91) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_37,negated_conjecture, % 8.09/8.17 ( p4(f20(X55,X56),f20(X57,X58)) % 8.09/8.17 | ~ p4(X55,X57) % 8.09/8.17 | ~ p4(X56,X58) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_38,negated_conjecture, % 8.09/8.17 ( p4(f16(X49,X50),f16(X51,X52)) % 8.09/8.17 | ~ p2(X49,X51) % 8.09/8.17 | ~ p4(X50,X52) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_39,negated_conjecture, % 8.09/8.17 ( p4(f14(X43,X44),f14(X45,X46)) % 8.09/8.17 | ~ p4(X43,X45) % 8.09/8.17 | ~ p4(X44,X46) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_40,negated_conjecture, % 8.09/8.17 ( p4(f13(X39,X40),f13(X41,X42)) % 8.09/8.17 | ~ p4(X39,X41) % 8.09/8.17 | ~ p4(X40,X42) ) ). % 8.09/8.17 % 8.09/8.17 cnf(not_p24_41,negated_conjecture, % 8.09/8.17 ( ~ p24(X92,c35) % 8.09/8.17 | ~ p24(c32,X92) % 8.09/8.17 | ~ p25(X92,f18(f8(c27,f9(c28,c29)))) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_42,negated_conjecture, % 8.09/8.17 p4(f16(f8(c27,f9(c28,c29)),c34),f16(f8(c27,f9(c28,c29)),c31)) ). % 8.09/8.17 % 8.09/8.17 cnf(p24_43,negated_conjecture, % 8.09/8.17 p24(c34,f13(c32,f14(f16(f8(c27,f9(c28,c29)),c31),f15(f10(f11(f12(c33))))))) ). % 8.09/8.17 % 8.09/8.17 cnf(not_p4_44,negated_conjecture, % 8.09/8.17 ~ p4(f5(f8(c27,f9(c28,c29)),c36,c31),f5(f8(c27,f9(c28,c29)),c36,c34)) ). % 8.09/8.17 % 8.09/8.17 cnf(p24_45,negated_conjecture, % 8.09/8.17 ( p24(f19(f20(c31,c34)),f19(f20(c31,X20))) % 8.09/8.17 | ~ p25(X20,f18(f8(c27,f9(c28,c29)))) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_46,negated_conjecture, % 8.09/8.17 ( p4(f5(X65,X66,X67),f5(X68,X69,X70)) % 8.09/8.17 | ~ p3(X66,X69) % 8.09/8.17 | ~ p4(X67,X70) % 8.09/8.17 | ~ p2(X65,X68) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p4_47,negated_conjecture, % 8.09/8.17 ( p4(f22(X59,X60,X61),f22(X62,X63,X64)) % 8.09/8.17 | ~ p4(X60,X63) % 8.09/8.17 | ~ p4(X61,X64) % 8.09/8.17 | ~ p2(X59,X62) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p6_48,negated_conjecture, % 8.09/8.17 ( p6(f21(X25),f10(c33)) % 8.09/8.17 | p25(f22(X25,X26,X27),f18(X25)) % 8.09/8.17 | p4(f5(X25,c36,X26),f5(X25,c36,X27)) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p6_49,negated_conjecture, % 8.09/8.17 ( p6(f21(X25),f10(c33)) % 8.09/8.17 | p4(f5(X25,c36,X26),f5(X25,c36,X27)) % 8.09/8.17 | ~ p24(f19(f20(X26,X27)),f19(f20(X26,f22(X25,X26,X27)))) ) ). % 8.09/8.17 % 8.09/8.17 cnf(p26_50,negated_conjecture, % 8.09/8.17 ( p26(f19(f20(c31,c32)),f19(f20(c31,X32))) % 8.09/8.17 | p26(f19(f20(c31,c35)),f19(f20(c31,X32))) % 8.09/8.17 | ~ p25(X32,f18(f8(c27,f9(c28,c29)))) ) ). % 8.09/8.17 % 8.09/8.17 %-------------------------------------------------------------------------- % 8.09/8.17 %------------------------------------------- % 8.09/8.17 % Proof found % 8.09/8.17 % SZS status Theorem for theBenchmark % 8.09/8.17 % SZS output start Proof % 8.09/8.17 %ClaNum:50(EqnAxiom:0) % 8.09/8.17 %VarNum:212(SingletonVarNum:102) % 8.09/8.17 %MaxLitNum:4 % 8.09/8.17 %MaxfuncDepth:6 % 8.09/8.17 %SharedTerms:45 % 8.09/8.17 %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 % 8.09/8.17 %singleGoalClaCount:20 % 8.09/8.17 [1]P1(a1,a2) % 8.09/8.17 [2]P1(a1,a7) % 8.09/8.17 [3]P5(a1,a2) % 8.09/8.17 [4]P5(a2,a9) % 8.09/8.17 [19]~P8(a3,f12(a8)) % 8.09/8.17 [11]P4(f12(f11(f10(a8))),a3) % 8.09/8.17 [12]P6(a1,f16(f15(a4,f14(a3,a5)))) % 8.09/8.17 [13]P6(a9,f16(f15(a4,f14(a3,a5)))) % 8.09/8.17 [15]P9(f24(f15(a4,f14(a3,a5)),a6,a2),a1) % 8.09/8.17 [16]P9(f17(f15(a4,f14(a3,a5)),a7),f17(f15(a4,f14(a3,a5)),a2)) % 8.09/8.17 [20]~P9(f24(f15(a4,f14(a3,a5)),a13,a2),f24(f15(a4,f14(a3,a5)),a13,a7)) % 8.09/8.17 [17]P9(a9,f18(a1,f17(f15(a4,f14(a3,a5)),a2))) % 8.09/8.17 [18]P1(a7,f18(a1,f20(f17(f15(a4,f14(a3,a5)),a2),f19(f12(f11(f10(a8))))))) % 8.09/8.17 [5]P2(x51,x51) % 8.09/8.17 [6]P7(x61,x61) % 8.09/8.17 [7]P8(x71,x71) % 8.09/8.17 [8]P9(x81,x81) % 8.09/8.17 [9]P10(x91,x91) % 8.09/8.17 [10]P3(x101,x101) % 8.09/8.17 [14]P8(f21(f15(x141,f14(x142,x143))),x142) % 8.09/8.17 [47]P1(f22(f23(a2,a7)),f22(f23(a2,x471)))+~P6(x471,f16(f15(a4,f14(a3,a5)))) % 8.09/8.17 [21]~P3(x211,x212)+P2(f16(x211),f16(x212)) % 8.09/8.17 [22]~P8(x221,x222)+P8(f12(x221),f12(x222)) % 8.09/8.17 [23]~P8(x231,x232)+P8(f10(x231),f10(x232)) % 8.09/8.17 [24]~P8(x241,x242)+P8(f11(x241),f11(x242)) % 8.09/8.17 [25]~P3(x251,x252)+P8(f21(x251),f21(x252)) % 8.09/8.17 [26]~P9(x261,x262)+P9(f22(x261),f22(x262)) % 8.09/8.17 [27]~P8(x271,x272)+P9(f19(x271),f19(x272)) % 8.09/8.18 [44]~P1(a1,x441)+~P1(x441,a9)+~P6(x441,f16(f15(a4,f14(a3,a5)))) % 8.09/8.18 [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)))) % 8.09/8.18 [28]~P2(x283,x281)+P2(x281,x282)+~P2(x283,x282) % 8.09/8.18 [29]~P7(x293,x291)+P7(x291,x292)+~P7(x293,x292) % 8.09/8.18 [30]~P8(x303,x301)+P8(x301,x302)+~P8(x303,x302) % 8.09/8.18 [31]~P9(x313,x311)+P9(x311,x312)+~P9(x313,x312) % 8.09/8.18 [32]~P10(x323,x321)+P10(x321,x322)+~P10(x323,x322) % 8.09/8.18 [33]~P3(x333,x331)+P3(x331,x332)+~P3(x333,x332) % 8.09/8.18 [48]P6(f25(x481,x482,x483),f16(x481))+P9(f24(x481,a13,x482),f24(x481,a13,x483))+P8(f21(x481),f12(a8)) % 8.09/8.18 [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)))) % 8.09/8.18 [38]~P8(x382,x384)+~P8(x381,x383)+P7(f14(x381,x382),f14(x383,x384)) % 8.09/8.18 [39]~P9(x392,x394)+~P3(x391,x393)+P9(f17(x391,x392),f17(x393,x394)) % 8.09/8.18 [40]~P9(x402,x404)+~P9(x401,x403)+P9(f18(x401,x402),f18(x403,x404)) % 8.09/8.18 [41]~P9(x412,x414)+~P9(x411,x413)+P9(f23(x411,x412),f23(x413,x414)) % 8.09/8.18 [42]~P9(x422,x424)+~P9(x421,x423)+P9(f20(x421,x422),f20(x423,x424)) % 8.09/8.18 [43]~P7(x432,x434)+~P8(x431,x433)+P3(f15(x431,x432),f15(x433,x434)) % 8.09/8.18 [34]~P1(x344,x343)+P1(x341,x342)+~P9(x343,x342)+~P9(x344,x341) % 8.09/8.18 [35]~P5(x354,x353)+P5(x351,x352)+~P9(x353,x352)+~P9(x354,x351) % 8.09/8.18 [36]~P4(x364,x363)+P4(x361,x362)+~P8(x363,x362)+~P8(x364,x361) % 8.09/8.18 [37]~P6(x374,x373)+P6(x371,x372)+~P2(x373,x372)+~P9(x374,x371) % 8.09/8.18 [45]~P9(x453,x456)+~P10(x452,x455)+~P3(x451,x454)+P9(f24(x451,x452,x453),f24(x454,x455,x456)) % 8.09/8.18 [46]~P9(x463,x466)+~P9(x462,x465)+~P3(x461,x464)+P9(f25(x461,x462,x463),f25(x464,x465,x466)) % 8.09/8.18 %EqnAxiom % 8.09/8.18 % 8.09/8.18 %------------------------------------------- % 8.09/8.18 cnf(70,plain, % 8.09/8.18 (P8(x701,f21(f15(x702,f14(x701,x703))))), % 8.09/8.18 inference(scs_inference,[],[14,13,7,47,30])). % 8.09/8.18 cnf(88,plain, % 8.09/8.18 (P8(f21(f15(x881,f14(f21(f15(x882,f14(x883,x884))),x885))),x883)), % 8.09/8.18 inference(scs_inference,[],[70,14,30])). % 8.09/8.18 cnf(399,plain, % 8.09/8.18 (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))))), % 8.09/8.18 inference(scs_inference,[],[9,10,50,45])). % 8.09/8.18 cnf(918,plain, % 8.09/8.18 (~P8(f12(a8),a3)), % 8.09/8.18 inference(scs_inference,[],[7,19,30])). % 8.09/8.18 cnf(921,plain, % 8.09/8.18 (~P8(f21(f15(x9211,f14(f21(f15(x9212,f14(a3,x9213))),x9214))),f12(a8))), % 8.09/8.18 inference(scs_inference,[],[88,918,30])). % 8.09/8.18 cnf(925,plain, % 8.09/8.18 (~P8(f12(a8),f21(f15(x9251,f14(f21(f15(x9252,f14(a3,x9253))),x9254))))), % 8.09/8.18 inference(scs_inference,[],[921,7,30])). % 8.09/8.18 cnf(929,plain, % 8.09/8.18 (~P8(f21(f15(x9291,f14(a3,x9292))),f12(a8))), % 8.09/8.18 inference(scs_inference,[],[70,925,30])). % 8.09/8.18 cnf(947,plain, % 8.09/8.18 (~P1(f22(f23(x9471,x9472)),f22(f23(x9471,f25(f15(x9473,f14(a3,x9474)),x9471,x9472))))+P9(f24(x9475,x9476,f24(f15(x9473,f14(a3,x9474)),a13,x9471)),f24(x9475,x9476,f24(f15(x9473,f14(a3,x9474)),a13,x9472)))), % 8.09/8.18 inference(scs_inference,[],[929,7,30,399])). % 8.09/8.18 cnf(971,plain, % 8.09/8.18 (P9(f24(x9711,x9712,f24(f15(x9713,f14(a3,x9714)),a13,a2)),f24(x9711,x9712,f24(f15(x9713,f14(a3,x9714)),a13,a7)))+~P6(f25(f15(x9713,f14(a3,x9714)),a2,a7),f16(f15(a4,f14(a3,a5))))), % 8.09/8.18 inference(scs_inference,[],[947,47])). % 8.09/8.18 cnf(1020,plain, % 8.09/8.18 (~P8(f21(f15(x10201,f14(a3,x10202))),f12(a8))), % 8.09/8.18 inference(rename_variables,[],[929])). % 8.09/8.18 cnf(1026,plain, % 8.09/8.18 ($false), % 8.09/8.18 inference(scs_inference,[],[20,929,1020,48,971,47,50]), % 8.09/8.18 ['proof']). % 8.09/8.18 % SZS output end Proof % 8.09/8.18 % Total time :7.560000s %------------------------------------------------------------------------------