%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN652-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 : n024.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 58.61s 58.65s % Output : CNFRefutation 58.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN652-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 : n024.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:36:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 58.56/58.62 %------------------------------------------- % 58.56/58.62 % File :CSE---1.7 % 58.56/58.62 % Problem :theBenchmark % 58.56/58.62 % Transform :cnf % 58.56/58.62 % Format :tptp:raw % 58.56/58.62 % Command :java -jar mcs_scs.jar %d %s % 58.56/58.62 % 58.56/58.62 % Result :Theorem 58.010000s % 58.56/58.62 % Output :CNFRefutation 58.010000s % 58.56/58.62 %------------------------------------------- % 58.61/58.64 %-------------------------------------------------------------------------- % 58.61/58.64 % File : SYN652-1 : TPTP v8.2.0. Released v2.5.0. % 58.61/58.64 % Domain : Syntactic % 58.61/58.64 % Problem : Harrison problem 4447 % 58.61/58.64 % Version : Especial. % 58.61/58.64 % English : % 58.61/58.64 % 58.61/58.64 % Refs : [Har01] Email to G. Sutcliffe % 58.61/58.64 % Source : [Har01] % 58.61/58.64 % Names : % 58.61/58.64 % 58.61/58.64 % Status : Unsatisfiable % 58.61/58.64 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.15 v5.2.0, 0.00 v2.5.0 % 58.61/58.64 % Syntax : Number of clauses : 47 ( 20 unt; 0 nHn; 30 RR) % 58.61/58.64 % Number of literals : 101 ( 0 equ; 55 neg) % 58.61/58.64 % Maximal clause size : 4 ( 2 avg) % 58.61/58.64 % Maximal term depth : 5 ( 1 avg) % 58.61/58.64 % Number of predicates : 16 ( 16 usr; 0 prp; 2-2 aty) % 58.61/58.64 % Number of functors : 21 ( 21 usr; 11 con; 0-2 aty) % 58.61/58.64 % Number of variables : 111 ( 0 sgn) % 58.61/58.64 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.61/58.64 % 58.61/58.64 % Comments : % 58.61/58.64 %-------------------------------------------------------------------------- % 58.61/58.64 cnf(p11_1,negated_conjecture, % 58.61/58.64 p11(X0,X0) ). % 58.61/58.64 % 58.61/58.64 cnf(p9_2,negated_conjecture, % 58.61/58.64 p9(X93,X93) ). % 58.61/58.64 % 58.61/58.64 cnf(p7_3,negated_conjecture, % 58.61/58.64 p7(X86,X86) ). % 58.61/58.64 % 58.61/58.64 cnf(p6_4,negated_conjecture, % 58.61/58.64 p6(X75,X75) ). % 58.61/58.64 % 58.61/58.64 cnf(p4_5,negated_conjecture, % 58.61/58.64 p4(X53,X53) ). % 58.61/58.64 % 58.61/58.64 cnf(p3_6,negated_conjecture, % 58.61/58.64 p3(X50,X50) ). % 58.61/58.64 % 58.61/58.64 cnf(p25_7,negated_conjecture, % 58.61/58.64 p25(X43,X43) ). % 58.61/58.64 % 58.61/58.64 cnf(p23_8,negated_conjecture, % 58.61/58.64 p23(X40,X40) ). % 58.61/58.64 % 58.61/58.64 cnf(p21_9,negated_conjecture, % 58.61/58.64 p21(X33,X33) ). % 58.61/58.64 % 58.61/58.64 cnf(p2_10,negated_conjecture, % 58.61/58.64 p2(X30,X30) ). % 58.61/58.64 % 58.61/58.64 cnf(p19_11,negated_conjecture, % 58.61/58.64 p19(X23,X23) ). % 58.61/58.64 % 58.61/58.64 cnf(p18_12,negated_conjecture, % 58.61/58.64 p18(X16,X16) ). % 58.61/58.64 % 58.61/58.64 cnf(p16_13,negated_conjecture, % 58.61/58.64 p16(X13,X13) ). % 58.61/58.64 % 58.61/58.64 cnf(p14_14,negated_conjecture, % 58.61/58.64 p14(X6,X6) ). % 58.61/58.64 % 58.61/58.64 cnf(p12_15,negated_conjecture, % 58.61/58.64 p12(X3,X3) ). % 58.61/58.64 % 58.61/58.64 cnf(p4_16,negated_conjecture, % 58.61/58.64 p4(c34,f5(c35,c32)) ). % 58.61/58.64 % 58.61/58.64 cnf(p27_17,negated_conjecture, % 58.61/58.64 p27(f8(f10(c28,f13(c29,c30)),c32),c33) ). % 58.61/58.64 % 58.61/58.64 cnf(not_p4_18,negated_conjecture, % 58.61/58.64 ~ p4(f5(c31,c33),f15(f17(c36,c31),c34)) ). % 58.61/58.64 % 58.61/58.64 cnf(p11_19,negated_conjecture, % 58.61/58.64 ( p11(X1,X2) % 58.61/58.64 | ~ p11(X0,X1) % 58.61/58.64 | ~ p11(X0,X2) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p9_20,negated_conjecture, % 58.61/58.64 ( p9(X94,X95) % 58.61/58.64 | ~ p9(X93,X94) % 58.61/58.64 | ~ p9(X93,X95) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p7_21,negated_conjecture, % 58.61/58.64 ( p7(X87,X88) % 58.61/58.64 | ~ p7(X86,X87) % 58.61/58.64 | ~ p7(X86,X88) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p6_22,negated_conjecture, % 58.61/58.64 ( p6(X76,X77) % 58.61/58.64 | ~ p6(X75,X76) % 58.61/58.64 | ~ p6(X75,X77) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p4_23,negated_conjecture, % 58.61/58.64 ( p4(X54,X55) % 58.61/58.64 | ~ p4(X53,X54) % 58.61/58.64 | ~ p4(X53,X55) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p3_24,negated_conjecture, % 58.61/58.64 ( p3(X51,X52) % 58.61/58.64 | ~ p3(X50,X51) % 58.61/58.64 | ~ p3(X50,X52) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p25_25,negated_conjecture, % 58.61/58.64 ( p25(X44,X45) % 58.61/58.64 | ~ p25(X43,X44) % 58.61/58.64 | ~ p25(X43,X45) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p23_26,negated_conjecture, % 58.61/58.64 ( p23(X41,X42) % 58.61/58.64 | ~ p23(X40,X41) % 58.61/58.64 | ~ p23(X40,X42) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p21_27,negated_conjecture, % 58.61/58.64 ( p21(X34,X35) % 58.61/58.64 | ~ p21(X33,X34) % 58.61/58.64 | ~ p21(X33,X35) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p2_28,negated_conjecture, % 58.61/58.64 ( p2(X31,X32) % 58.61/58.64 | ~ p2(X30,X31) % 58.61/58.64 | ~ p2(X30,X32) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p19_29,negated_conjecture, % 58.61/58.64 ( p19(X24,X25) % 58.61/58.64 | ~ p19(X23,X24) % 58.61/58.64 | ~ p19(X23,X25) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p18_30,negated_conjecture, % 58.61/58.64 ( p18(X17,X18) % 58.61/58.64 | ~ p18(X16,X17) % 58.61/58.64 | ~ p18(X16,X18) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p16_31,negated_conjecture, % 58.61/58.64 ( p16(X14,X15) % 58.61/58.64 | ~ p16(X13,X14) % 58.61/58.64 | ~ p16(X13,X15) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p14_32,negated_conjecture, % 58.61/58.64 ( p14(X7,X8) % 58.61/58.64 | ~ p14(X6,X7) % 58.61/58.64 | ~ p14(X6,X8) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p12_33,negated_conjecture, % 58.61/58.64 ( p12(X4,X5) % 58.61/58.64 | ~ p12(X3,X4) % 58.61/58.64 | ~ p12(X3,X5) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p4_34,negated_conjecture, % 58.61/58.64 p4(f15(f17(c36,X60),f5(c35,X61)),f5(X60,X61)) ). % 58.61/58.64 % 58.61/58.64 cnf(p27_35,negated_conjecture, % 58.61/58.64 ( p27(X46,X47) % 58.61/58.64 | ~ p3(X49,X47) % 58.61/58.64 | ~ p7(X48,X46) % 58.61/58.64 | ~ p27(X48,X49) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p7_36,negated_conjecture, % 58.61/58.64 ( p7(f8(X89,X90),f8(X91,X92)) % 58.61/58.64 | ~ p3(X90,X92) % 58.61/58.64 | ~ p6(X89,X91) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p14_37,negated_conjecture, % 58.61/58.64 ( p14(f17(X9,X10),f17(X11,X12)) % 58.61/58.64 | ~ p16(X9,X11) % 58.61/58.64 | ~ p2(X10,X12) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p18_38,negated_conjecture, % 58.61/58.64 ( p18(f26(X19,X20),f26(X21,X22)) % 58.61/58.64 | ~ p25(X19,X21) % 58.61/58.64 | ~ p3(X20,X22) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p19_39,negated_conjecture, % 58.61/58.64 ( p19(f22(X26,X27),f22(X28,X29)) % 58.61/58.64 | ~ p19(X27,X29) % 58.61/58.64 | ~ p21(X26,X28) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p21_40,negated_conjecture, % 58.61/58.64 ( p21(f24(X36,X37),f24(X38,X39)) % 58.61/58.64 | ~ p14(X37,X39) % 58.61/58.64 | ~ p23(X36,X38) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p4_41,negated_conjecture, % 58.61/58.64 ( p4(f15(X56,X57),f15(X58,X59)) % 58.61/58.64 | ~ p14(X56,X58) % 58.61/58.64 | ~ p4(X57,X59) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p4_42,negated_conjecture, % 58.61/58.64 ( p4(f20(X65,X66),f20(X67,X68)) % 58.61/58.64 | ~ p18(X65,X67) % 58.61/58.64 | ~ p19(X66,X68) ) ). % 58.61/58.64 % 58.61/58.64 cnf(p4_43,negated_conjecture, % 58.61/58.64 ( p4(f5(X69,X70),f5(X71,X72)) % 58.61/58.64 | ~ p2(X69,X71) % 58.61/58.64 | ~ p3(X70,X72) ) ). % 58.61/58.65 % 58.61/58.65 cnf(p6_44,negated_conjecture, % 58.61/58.65 ( p6(f10(X78,X79),f10(X80,X81)) % 58.61/58.65 | ~ p6(X79,X81) % 58.61/58.65 | ~ p9(X78,X80) ) ). % 58.61/58.65 % 58.61/58.65 cnf(p6_45,negated_conjecture, % 58.61/58.65 ( p6(f13(X82,X83),f13(X84,X85)) % 58.61/58.65 | ~ p11(X82,X84) % 58.61/58.65 | ~ p12(X83,X85) ) ). % 58.61/58.65 % 58.61/58.65 cnf(p4_46,negated_conjecture, % 58.61/58.65 ( p4(f5(c31,X73),f5(c31,X74)) % 58.61/58.65 | ~ p27(f8(f10(c28,f13(c29,c30)),X73),X74) ) ). % 58.61/58.65 % 58.61/58.65 cnf(p4_47,negated_conjecture, % 58.61/58.65 p4(f15(f17(c36,X62),f20(f26(c37,X63),X64)),f20(f26(c37,X63),f22(f24(c38,f17(c36,X62)),X64))) ). % 58.61/58.65 % 58.61/58.65 %-------------------------------------------------------------------------- % 58.61/58.65 %------------------------------------------- % 58.61/58.65 % Proof found % 58.61/58.65 % SZS status Theorem for theBenchmark % 58.61/58.65 % SZS output start Proof % 58.64/58.65 %ClaNum:47(EqnAxiom:0) % 58.64/58.65 %VarNum:222(SingletonVarNum:111) % 58.64/58.65 %MaxLitNum:4 % 58.64/58.65 %MaxfuncDepth:4 % 58.64/58.65 %SharedTerms:21 % 58.64/58.65 %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 % 58.64/58.65 %singleGoalClaCount:20 % 58.64/58.65 [16]P5(a1,f9(a8,a2)) % 58.64/58.65 [20]~P5(f9(a6,a7),f12(f11(a10,a6),a1)) % 58.64/58.65 [18]P16(f21(f14(a3,f13(a4,a5)),a2),a7) % 58.64/58.65 [1]P1(x11,x11) % 58.64/58.65 [2]P2(x21,x21) % 58.64/58.65 [3]P3(x31,x31) % 58.64/58.65 [4]P4(x41,x41) % 58.64/58.65 [5]P5(x51,x51) % 58.64/58.65 [6]P6(x61,x61) % 58.64/58.65 [7]P7(x71,x71) % 58.64/58.65 [8]P8(x81,x81) % 58.64/58.65 [9]P9(x91,x91) % 58.64/58.65 [10]P10(x101,x101) % 58.64/58.65 [11]P11(x111,x111) % 58.64/58.65 [12]P12(x121,x121) % 58.64/58.65 [13]P13(x131,x131) % 58.64/58.65 [14]P14(x141,x141) % 58.64/58.65 [15]P15(x151,x151) % 58.64/58.65 [17]P5(f12(f11(a10,x171),f9(a8,x172)),f9(x171,x172)) % 58.64/58.65 [19]P5(f12(f11(a10,x191),f18(f17(a15,x192),x193)),f18(f17(a15,x192),f20(f19(a16,f11(a10,x191)),x193))) % 58.64/58.65 [47]P5(f9(a6,x471),f9(a6,x472))+~P16(f21(f14(a3,f13(a4,a5)),x471),x472) % 58.64/58.65 [21]~P1(x213,x211)+P1(x211,x212)+~P1(x213,x212) % 58.64/58.65 [22]~P2(x223,x221)+P2(x221,x222)+~P2(x223,x222) % 58.64/58.65 [23]~P3(x233,x231)+P3(x231,x232)+~P3(x233,x232) % 58.64/58.65 [24]~P4(x243,x241)+P4(x241,x242)+~P4(x243,x242) % 58.64/58.65 [25]~P5(x253,x251)+P5(x251,x252)+~P5(x253,x252) % 58.64/58.65 [26]~P6(x263,x261)+P6(x261,x262)+~P6(x263,x262) % 58.64/58.65 [27]~P7(x273,x271)+P7(x271,x272)+~P7(x273,x272) % 58.64/58.65 [28]~P8(x283,x281)+P8(x281,x282)+~P8(x283,x282) % 58.64/58.65 [29]~P9(x293,x291)+P9(x291,x292)+~P9(x293,x292) % 58.64/58.65 [30]~P10(x303,x301)+P10(x301,x302)+~P10(x303,x302) % 58.64/58.65 [31]~P11(x313,x311)+P11(x311,x312)+~P11(x313,x312) % 58.64/58.65 [32]~P12(x323,x321)+P12(x321,x322)+~P12(x323,x322) % 58.64/58.65 [33]~P13(x333,x331)+P13(x331,x332)+~P13(x333,x332) % 58.64/58.65 [34]~P14(x343,x341)+P14(x341,x342)+~P14(x343,x342) % 58.64/58.65 [35]~P15(x353,x351)+P15(x351,x352)+~P15(x353,x352) % 58.64/58.65 [37]~P4(x371,x373)+~P6(x372,x374)+P3(f21(x371,x372),f21(x373,x374)) % 58.64/58.65 [38]~P1(x381,x383)+~P15(x382,x384)+P4(f13(x381,x382),f13(x383,x384)) % 58.64/58.65 [39]~P2(x391,x393)+~P4(x392,x394)+P4(f14(x391,x392),f14(x393,x394)) % 58.64/58.65 [40]~P6(x402,x404)+~P10(x401,x403)+P5(f9(x401,x402),f9(x403,x404)) % 58.64/58.65 [41]~P5(x412,x414)+~P14(x411,x413)+P5(f12(x411,x412),f12(x413,x414)) % 58.64/58.65 [42]~P11(x422,x424)+~P12(x421,x423)+P5(f18(x421,x422),f18(x423,x424)) % 58.64/58.65 [43]~P8(x431,x433)+~P14(x432,x434)+P9(f19(x431,x432),f19(x433,x434)) % 58.64/58.65 [44]~P9(x441,x443)+~P11(x442,x444)+P11(f20(x441,x442),f20(x443,x444)) % 58.64/58.65 [45]~P6(x452,x454)+~P7(x451,x453)+P12(f17(x451,x452),f17(x453,x454)) % 58.64/58.65 [46]~P10(x462,x464)+~P13(x461,x463)+P14(f11(x461,x462),f11(x463,x464)) % 58.64/58.65 [36]~P16(x363,x364)+P16(x361,x362)+~P3(x363,x361)+~P6(x364,x362) % 58.64/58.65 %EqnAxiom % 58.64/58.65 % 58.64/58.65 %------------------------------------------- % 58.64/58.66 cnf(48,plain, % 58.64/58.66 (P5(f9(a6,a2),f9(a6,a7))), % 58.64/58.66 inference(scs_inference,[],[18,47])). % 58.64/58.66 cnf(58,plain, % 58.64/58.66 (P5(f9(a8,a2),a1)), % 58.64/58.66 inference(scs_inference,[],[16,5,25])). % 58.64/58.66 cnf(68,plain, % 58.64/58.66 (P5(f12(x681,f9(a8,a2)),f12(x681,a1))), % 58.64/58.66 inference(scs_inference,[],[14,58,34,41])). % 58.64/58.66 cnf(104,plain, % 58.64/58.66 (~P5(f9(a6,a2),f12(f11(a10,a6),a1))), % 58.64/58.66 inference(scs_inference,[],[20,48,25])). % 58.64/58.66 cnf(115,plain, % 58.64/58.66 ($false), % 58.64/58.66 inference(scs_inference,[],[104,68,17,25]), % 58.64/58.66 ['proof']). % 58.64/58.66 % SZS output end Proof % 58.64/58.66 % Total time :58.010000s %------------------------------------------------------------------------------