%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN635-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 : n028.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:10 EDT 2024 % Result : Unsatisfiable 0.87s 1.00s % Output : CNFRefutation 0.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN635-1 : TPTP v8.2.0. Released v2.5.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.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 23:19:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 0.87/0.99 %------------------------------------------- % 0.87/0.99 % File :CSE---1.7 % 0.87/0.99 % Problem :theBenchmark % 0.87/0.99 % Transform :cnf % 0.87/0.99 % Format :tptp:raw % 0.87/0.99 % Command :java -jar mcs_scs.jar %d %s % 0.87/0.99 % 0.87/0.99 % Result :Theorem 0.390000s % 0.87/0.99 % Output :CNFRefutation 0.390000s % 0.87/0.99 %------------------------------------------- % 0.87/0.99 %-------------------------------------------------------------------------- % 0.87/0.99 % File : SYN635-1 : TPTP v8.2.0. Released v2.5.0. % 0.87/0.99 % Domain : Syntactic % 0.87/0.99 % Problem : Harrison problem 4218 % 0.87/0.99 % Version : Especial. % 0.87/0.99 % English : % 0.87/0.99 % 0.87/0.99 % Refs : [Har01] Email to G. Sutcliffe % 0.87/0.99 % Source : [Har01] % 0.87/0.99 % Names : % 0.87/0.99 % 0.87/0.99 % Status : Unsatisfiable % 0.87/0.99 % 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.14 v6.2.0, 0.11 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.29 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0 % 0.87/0.99 % Syntax : Number of clauses : 40 ( 9 unt; 8 nHn; 29 RR) % 0.87/0.99 % Number of literals : 102 ( 0 equ; 52 neg) % 0.87/0.99 % Maximal clause size : 4 ( 2 avg) % 0.87/0.99 % Maximal term depth : 4 ( 1 avg) % 0.87/0.99 % Number of predicates : 8 ( 8 usr; 0 prp; 2-2 aty) % 0.87/0.99 % Number of functors : 23 ( 23 usr; 10 con; 0-3 aty) % 0.87/0.99 % Number of variables : 113 ( 2 sgn) % 0.87/0.99 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.87/0.99 % 0.87/0.99 % Comments : % 0.87/0.99 %-------------------------------------------------------------------------- % 0.87/0.99 cnf(p10_1,negated_conjecture, % 0.87/0.99 p10(X0,X0) ). % 0.87/0.99 % 0.87/0.99 cnf(p9_2,negated_conjecture, % 0.87/0.99 p9(X92,X92) ). % 0.87/0.99 % 0.87/0.99 cnf(p5_3,negated_conjecture, % 0.87/0.99 p5(X85,X85) ). % 0.87/0.99 % 0.87/0.99 cnf(p3_4,negated_conjecture, % 0.87/0.99 p3(X75,X75) ). % 0.87/0.99 % 0.87/0.99 cnf(p2_5,negated_conjecture, % 0.87/0.99 p2(X58,X58) ). % 0.87/0.99 % 0.87/0.99 cnf(p14_6,negated_conjecture, % 0.87/0.99 p14(X51,X51) ). % 0.87/0.99 % 0.87/0.99 cnf(not_p3_7,negated_conjecture, % 0.87/0.99 ~ p3(c23,f8(c24)) ). % 0.87/0.99 % 0.87/0.99 cnf(p3_8,negated_conjecture, % 0.87/0.99 p3(f4(f6(X80,f7(X81,X82))),X81) ). % 0.87/0.99 % 0.87/0.99 cnf(p3_9,negated_conjecture, % 0.87/0.99 ( p3(f8(X83),f8(X84)) % 0.87/0.99 | ~ p3(X83,X84) ) ). % 0.87/0.99 % 0.87/0.99 cnf(p10_10,negated_conjecture, % 0.87/0.99 ( p10(f12(X21),f12(X22)) % 0.87/0.99 | ~ p10(X21,X22) ) ). % 0.87/0.99 % 0.87/0.99 cnf(p14_11,negated_conjecture, % 0.87/0.99 ( p14(f15(X54),f15(X55)) % 0.87/0.99 | ~ p2(X54,X55) ) ). % 0.87/0.99 % 0.87/0.99 cnf(p14_12,negated_conjecture, % 0.87/0.99 ( p14(f16(X56),f16(X57)) % 0.87/0.99 | ~ p2(X56,X57) ) ). % 0.87/0.99 % 0.87/0.99 cnf(p3_13,negated_conjecture, % 0.87/0.99 ( p3(f4(X78),f4(X79)) % 0.87/0.99 | ~ p2(X78,X79) ) ). % 0.87/0.99 % 0.87/0.99 cnf(p10_14,negated_conjecture, % 0.87/0.99 ( p10(X1,X2) % 0.87/0.99 | ~ p10(X0,X1) % 0.87/0.99 | ~ p10(X0,X2) ) ). % 0.87/0.99 % 0.87/0.99 cnf(p9_15,negated_conjecture, % 0.87/0.99 ( p9(X93,X94) % 0.87/0.99 | ~ p9(X92,X93) % 0.87/0.99 | ~ p9(X92,X94) ) ). % 0.87/0.99 % 0.87/1.00 cnf(p5_16,negated_conjecture, % 0.87/1.00 ( p5(X86,X87) % 0.87/1.00 | ~ p5(X85,X86) % 0.87/1.00 | ~ p5(X85,X87) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_17,negated_conjecture, % 0.87/1.00 ( p3(X76,X77) % 0.87/1.00 | ~ p3(X75,X76) % 0.87/1.00 | ~ p3(X75,X77) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p2_18,negated_conjecture, % 0.87/1.00 ( p2(X59,X60) % 0.87/1.00 | ~ p2(X58,X59) % 0.87/1.00 | ~ p2(X58,X60) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p14_19,negated_conjecture, % 0.87/1.00 ( p14(X52,X53) % 0.87/1.00 | ~ p14(X51,X52) % 0.87/1.00 | ~ p14(X51,X53) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p22_20,negated_conjecture, % 0.87/1.00 ( p22(X71,X72) % 0.87/1.00 | ~ p14(X74,X72) % 0.87/1.00 | ~ p22(X73,X74) % 0.87/1.00 | ~ p10(X73,X71) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p21_21,negated_conjecture, % 0.87/1.00 ( p21(X65,X66) % 0.87/1.00 | ~ p10(X68,X66) % 0.87/1.00 | ~ p21(X67,X68) % 0.87/1.00 | ~ p10(X67,X65) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p10_22,negated_conjecture, % 0.87/1.00 ( p10(f13(X23,X24),f13(X25,X26)) % 0.87/1.00 | ~ p10(X23,X25) % 0.87/1.00 | ~ p10(X24,X26) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p5_23,negated_conjecture, % 0.87/1.00 ( p5(f7(X88,X89),f7(X90,X91)) % 0.87/1.00 | ~ p3(X88,X90) % 0.87/1.00 | ~ p3(X89,X91) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p2_24,negated_conjecture, % 0.87/1.00 ( p2(f6(X61,X62),f6(X63,X64)) % 0.87/1.00 | ~ p3(X61,X63) % 0.87/1.00 | ~ p5(X62,X64) ) ). % 0.87/1.00 % 0.87/1.00 cnf(not_p10_25,negated_conjecture, % 0.87/1.00 ~ p10(f11(f6(c25,f7(c23,c26)),c27,c28),f11(f6(c25,f7(c23,c26)),c27,c29)) ). % 0.87/1.00 % 0.87/1.00 cnf(p21_26,negated_conjecture, % 0.87/1.00 ( p21(f12(f13(c28,c29)),f12(f13(c28,X70))) % 0.87/1.00 | ~ p22(X70,f16(f6(c25,f7(c23,c26)))) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p21_27,negated_conjecture, % 0.87/1.00 ( p21(f12(f13(c28,c29)),f12(f13(c28,X69))) % 0.87/1.00 | ~ p22(X69,f15(f6(c25,f7(c23,c26)))) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p10_28,negated_conjecture, % 0.87/1.00 ( p10(f11(X3,X4,X5),f11(X6,X7,X8)) % 0.87/1.00 | ~ p2(X3,X6) % 0.87/1.00 | ~ p9(X4,X7) % 0.87/1.00 | ~ p10(X5,X8) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p10_29,negated_conjecture, % 0.87/1.00 ( p10(f20(X45,X46,X47),f20(X48,X49,X50)) % 0.87/1.00 | ~ p10(X47,X50) % 0.87/1.00 | ~ p2(X45,X48) % 0.87/1.00 | ~ p10(X46,X49) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p10_30,negated_conjecture, % 0.87/1.00 ( p10(f19(X39,X40,X41),f19(X42,X43,X44)) % 0.87/1.00 | ~ p10(X41,X44) % 0.87/1.00 | ~ p2(X39,X42) % 0.87/1.00 | ~ p10(X40,X43) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p10_31,negated_conjecture, % 0.87/1.00 ( p10(f18(X33,X34,X35),f18(X36,X37,X38)) % 0.87/1.00 | ~ p10(X35,X38) % 0.87/1.00 | ~ p2(X33,X36) % 0.87/1.00 | ~ p10(X34,X37) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p10_32,negated_conjecture, % 0.87/1.00 ( p10(f17(X27,X28,X29),f17(X30,X31,X32)) % 0.87/1.00 | ~ p10(X29,X32) % 0.87/1.00 | ~ p2(X27,X30) % 0.87/1.00 | ~ p10(X28,X31) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_33,negated_conjecture, % 0.87/1.00 ( p3(f4(X9),f8(c24)) % 0.87/1.00 | p22(f17(X9,X10,X11),f16(X9)) % 0.87/1.00 | p10(f11(X9,c30,X10),f11(X9,c30,X11)) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_34,negated_conjecture, % 0.87/1.00 ( p3(f4(X18),f8(c24)) % 0.87/1.00 | p22(f20(X18,X19,X20),f15(X18)) % 0.87/1.00 | p10(f11(X18,c32,X19),f11(X18,c32,X20)) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_35,negated_conjecture, % 0.87/1.00 ( p3(f4(X15),f8(c24)) % 0.87/1.00 | p22(f19(X15,X16,X17),f16(X15)) % 0.87/1.00 | p10(f11(X15,c27,X16),f11(X15,c27,X17)) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_36,negated_conjecture, % 0.87/1.00 ( p3(f4(X12),f8(c24)) % 0.87/1.00 | p22(f18(X12,X13,X14),f16(X12)) % 0.87/1.00 | p10(f11(X12,c31,X13),f11(X12,c31,X14)) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_37,negated_conjecture, % 0.87/1.00 ( p3(f4(X18),f8(c24)) % 0.87/1.00 | p10(f11(X18,c32,X19),f11(X18,c32,X20)) % 0.87/1.00 | ~ p21(f12(f13(X19,X20)),f12(f13(X19,f20(X18,X19,X20)))) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_38,negated_conjecture, % 0.87/1.00 ( p3(f4(X9),f8(c24)) % 0.87/1.00 | p10(f11(X9,c30,X10),f11(X9,c30,X11)) % 0.87/1.00 | ~ p21(f12(f13(X10,X11)),f12(f13(X10,f17(X9,X10,X11)))) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_39,negated_conjecture, % 0.87/1.00 ( p3(f4(X12),f8(c24)) % 0.87/1.00 | p10(f11(X12,c31,X13),f11(X12,c31,X14)) % 0.87/1.00 | ~ p21(f12(f13(X13,X14)),f12(f13(X13,f18(X12,X13,X14)))) ) ). % 0.87/1.00 % 0.87/1.00 cnf(p3_40,negated_conjecture, % 0.87/1.00 ( p3(f4(X15),f8(c24)) % 0.87/1.00 | p10(f11(X15,c27,X16),f11(X15,c27,X17)) % 0.87/1.00 | ~ p21(f12(f13(X16,X17)),f12(f13(X16,f19(X15,X16,X17)))) ) ). % 0.87/1.00 % 0.87/1.00 %-------------------------------------------------------------------------- % 0.87/1.00 %------------------------------------------- % 0.87/1.00 % Proof found % 0.87/1.00 % SZS status Theorem for theBenchmark % 0.87/1.00 % SZS output start Proof % 0.87/1.00 %ClaNum:40(EqnAxiom:0) % 0.87/1.00 %VarNum:256(SingletonVarNum:113) % 0.87/1.00 %MaxLitNum:4 % 0.87/1.00 %MaxfuncDepth:3 % 0.87/1.00 %SharedTerms:21 % 0.87/1.00 %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 % 0.87/1.00 %singleGoalClaCount:9 % 0.87/1.00 [8]~P4(a4,f23(a5)) % 0.87/1.00 [9]~P1(f10(f2(a6,f1(a4,a7)),a8,a9),f10(f2(a6,f1(a4,a7)),a8,a11)) % 0.87/1.00 [1]P1(x11,x11) % 0.87/1.00 [2]P2(x21,x21) % 0.87/1.00 [3]P3(x31,x31) % 0.87/1.00 [4]P4(x41,x41) % 0.87/1.00 [5]P5(x51,x51) % 0.87/1.00 [6]P6(x61,x61) % 0.87/1.00 [7]P4(f3(f2(x71,f1(x72,x73))),x72) % 0.87/1.00 [31]P8(f15(f17(a9,a11)),f15(f17(a9,x311)))+~P7(x311,f16(f2(a6,f1(a4,a7)))) % 0.87/1.00 [32]P8(f15(f17(a9,a11)),f15(f17(a9,x321)))+~P7(x321,f18(f2(a6,f1(a4,a7)))) % 0.87/1.00 [10]~P1(x101,x102)+P1(f15(x101),f15(x102)) % 0.87/1.00 [11]~P4(x111,x112)+P4(f23(x111),f23(x112)) % 0.87/1.00 [12]~P5(x121,x122)+P4(f3(x121),f3(x122)) % 0.87/1.00 [13]~P5(x131,x132)+P6(f16(x131),f16(x132)) % 0.87/1.00 [14]~P5(x141,x142)+P6(f18(x141),f18(x142)) % 0.87/1.00 [15]~P1(x153,x151)+P1(x151,x152)+~P1(x153,x152) % 0.87/1.00 [16]~P2(x163,x161)+P2(x161,x162)+~P2(x163,x162) % 0.87/1.00 [17]~P3(x173,x171)+P3(x171,x172)+~P3(x173,x172) % 0.87/1.00 [18]~P4(x183,x181)+P4(x181,x182)+~P4(x183,x182) % 0.87/1.00 [19]~P5(x193,x191)+P5(x191,x192)+~P5(x193,x192) % 0.87/1.00 [20]~P6(x203,x201)+P6(x201,x202)+~P6(x203,x202) % 0.87/1.00 [33]P7(f19(x331,x332,x333),f16(x331))+P1(f10(x331,a12,x332),f10(x331,a12,x333))+P4(f3(x331),f23(a5)) % 0.87/1.00 [34]P7(f20(x341,x342,x343),f18(x341))+P1(f10(x341,a8,x342),f10(x341,a8,x343))+P4(f3(x341),f23(a5)) % 0.87/1.00 [35]P7(f21(x351,x352,x353),f18(x351))+P1(f10(x351,a13,x352),f10(x351,a13,x353))+P4(f3(x351),f23(a5)) % 0.87/1.00 [36]P7(f22(x361,x362,x363),f18(x361))+P1(f10(x361,a14,x362),f10(x361,a14,x363))+P4(f3(x361),f23(a5)) % 0.87/1.00 [37]P1(f10(x371,a8,x372),f10(x371,a8,x373))+P4(f3(x371),f23(a5))+~P8(f15(f17(x372,x373)),f15(f17(x372,f20(x371,x372,x373)))) % 0.87/1.00 [38]P1(f10(x381,a14,x382),f10(x381,a14,x383))+P4(f3(x381),f23(a5))+~P8(f15(f17(x382,x383)),f15(f17(x382,f22(x381,x382,x383)))) % 0.87/1.00 [39]P1(f10(x391,a12,x392),f10(x391,a12,x393))+P4(f3(x391),f23(a5))+~P8(f15(f17(x392,x393)),f15(f17(x392,f19(x391,x392,x393)))) % 0.87/1.00 [40]P1(f10(x401,a13,x402),f10(x401,a13,x403))+P4(f3(x401),f23(a5))+~P8(f15(f17(x402,x403)),f15(f17(x402,f21(x401,x402,x403)))) % 0.87/1.00 [23]~P1(x232,x234)+~P1(x231,x233)+P1(f17(x231,x232),f17(x233,x234)) % 0.87/1.00 [24]~P4(x242,x244)+~P4(x241,x243)+P3(f1(x241,x242),f1(x243,x244)) % 0.87/1.00 [25]~P3(x252,x254)+~P4(x251,x253)+P5(f2(x251,x252),f2(x253,x254)) % 0.87/1.00 [21]~P7(x213,x214)+P7(x211,x212)+~P1(x213,x211)+~P6(x214,x212) % 0.87/1.00 [22]~P8(x223,x224)+P8(x221,x222)+~P1(x223,x221)+~P1(x224,x222) % 0.87/1.00 [26]~P1(x263,x266)+~P2(x262,x265)+~P5(x261,x264)+P1(f10(x261,x262,x263),f10(x264,x265,x266)) % 0.87/1.00 [27]~P1(x273,x276)+~P1(x272,x275)+~P5(x271,x274)+P1(f19(x271,x272,x273),f19(x274,x275,x276)) % 0.87/1.00 [28]~P1(x283,x286)+~P1(x282,x285)+~P5(x281,x284)+P1(f20(x281,x282,x283),f20(x284,x285,x286)) % 0.87/1.00 [29]~P1(x293,x296)+~P1(x292,x295)+~P5(x291,x294)+P1(f21(x291,x292,x293),f21(x294,x295,x296)) % 0.87/1.00 [30]~P1(x303,x306)+~P1(x302,x305)+~P5(x301,x304)+P1(f22(x301,x302,x303),f22(x304,x305,x306)) % 0.87/1.00 %EqnAxiom % 0.87/1.00 % 0.87/1.00 %------------------------------------------- % 0.87/1.00 cnf(60,plain, % 0.87/1.00 (P4(f3(f2(a6,f1(a4,a7))),f23(a5))+~P7(f20(f2(a6,f1(a4,a7)),a9,a11),f18(f2(a6,f1(a4,a7))))), % 0.87/1.00 inference(scs_inference,[],[9,32,37])). % 0.87/1.00 cnf(134,plain, % 0.87/1.00 (P4(f3(f2(a6,f1(a4,a7))),f23(a5))), % 0.87/1.00 inference(scs_inference,[],[9,60,34])). % 0.87/1.00 cnf(139,plain, % 0.87/1.00 (P4(f23(a5),a4)), % 0.87/1.00 inference(scs_inference,[],[134,7,18])). % 0.87/1.00 cnf(150,plain, % 0.87/1.00 ($false), % 0.87/1.00 inference(scs_inference,[],[139,8,4,18]), % 0.87/1.00 ['proof']). % 0.87/1.00 % SZS output end Proof % 0.87/1.00 % Total time :0.390000s %------------------------------------------------------------------------------