%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN672-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 : n020.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 0.54s 0.90s % Output : CNFRefutation 0.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN672-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n020.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 21:57:23 EDT 2024 % 0.11/0.33 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 0.54/0.89 %------------------------------------------- % 0.54/0.89 % File :CSE---1.7 % 0.54/0.89 % Problem :theBenchmark % 0.54/0.89 % Transform :cnf % 0.54/0.89 % Format :tptp:raw % 0.54/0.89 % Command :java -jar mcs_scs.jar %d %s % 0.54/0.89 % 0.54/0.89 % Result :Theorem 0.280000s % 0.54/0.89 % Output :CNFRefutation 0.280000s % 0.54/0.89 %------------------------------------------- % 0.54/0.89 %-------------------------------------------------------------------------- % 0.54/0.89 % File : SYN672-1 : TPTP v8.2.0. Released v2.5.0. % 0.54/0.89 % Domain : Syntactic % 0.54/0.89 % Problem : Harrison problem 4541 % 0.54/0.89 % Version : Especial. % 0.54/0.89 % English : % 0.54/0.89 % 0.54/0.89 % Refs : [Har01] Email to G. Sutcliffe % 0.54/0.89 % Source : [Har01] % 0.54/0.89 % Names : % 0.54/0.89 % 0.54/0.89 % Status : Unsatisfiable % 0.54/0.89 % Rating : 0.00 v5.2.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.07 v4.1.0, 0.00 v2.5.0 % 0.54/0.89 % Syntax : Number of clauses : 54 ( 22 unt; 1 nHn; 35 RR) % 0.54/0.89 % Number of literals : 119 ( 0 equ; 66 neg) % 0.54/0.89 % Maximal clause size : 4 ( 2 avg) % 0.54/0.89 % Maximal term depth : 5 ( 1 avg) % 0.54/0.89 % Number of predicates : 19 ( 19 usr; 0 prp; 2-2 aty) % 0.54/0.89 % Number of functors : 22 ( 22 usr; 11 con; 0-2 aty) % 0.54/0.89 % Number of variables : 129 ( 0 sgn) % 0.54/0.89 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.54/0.89 % 0.54/0.89 % Comments : % 0.54/0.89 %-------------------------------------------------------------------------- % 0.54/0.89 cnf(p11_1,negated_conjecture, % 0.54/0.89 p11(X0,X0) ). % 0.54/0.89 % 0.54/0.89 cnf(p9_2,negated_conjecture, % 0.54/0.89 p9(X105,X105) ). % 0.54/0.89 % 0.54/0.89 cnf(p8_3,negated_conjecture, % 0.54/0.89 p8(X98,X98) ). % 0.54/0.89 % 0.54/0.89 cnf(p6_4,negated_conjecture, % 0.54/0.89 p6(X95,X95) ). % 0.54/0.89 % 0.54/0.89 cnf(p5_5,negated_conjecture, % 0.54/0.89 p5(X92,X92) ). % 0.54/0.89 % 0.54/0.89 cnf(p3_6,negated_conjecture, % 0.54/0.89 p3(X62,X62) ). % 0.54/0.89 % 0.54/0.89 cnf(p28_7,negated_conjecture, % 0.54/0.89 p28(X57,X57) ). % 0.54/0.89 % 0.54/0.89 cnf(p26_8,negated_conjecture, % 0.54/0.89 p26(X54,X54) ). % 0.54/0.89 % 0.54/0.89 cnf(p24_9,negated_conjecture, % 0.54/0.89 p24(X47,X47) ). % 0.54/0.89 % 0.54/0.89 cnf(p22_10,negated_conjecture, % 0.54/0.89 p22(X40,X40) ). % 0.54/0.89 % 0.54/0.89 cnf(p21_11,negated_conjecture, % 0.54/0.89 p21(X33,X33) ). % 0.54/0.89 % 0.54/0.89 cnf(p2_12,negated_conjecture, % 0.54/0.90 p2(X26,X26) ). % 0.54/0.90 % 0.54/0.90 cnf(p19_13,negated_conjecture, % 0.54/0.90 p19(X19,X19) ). % 0.54/0.90 % 0.54/0.90 cnf(p18_14,negated_conjecture, % 0.54/0.90 p18(X16,X16) ). % 0.54/0.90 % 0.54/0.90 cnf(p16_15,negated_conjecture, % 0.54/0.90 p16(X9,X9) ). % 0.54/0.90 % 0.54/0.90 cnf(p15_16,negated_conjecture, % 0.54/0.90 p15(X6,X6) ). % 0.54/0.90 % 0.54/0.90 cnf(p13_17,negated_conjecture, % 0.54/0.90 p13(X3,X3) ). % 0.54/0.90 % 0.54/0.90 cnf(not_p3_18,negated_conjecture, % 0.54/0.90 ~ p3(c40,f14(c38,c39)) ). % 0.54/0.90 % 0.54/0.90 cnf(p31_19,negated_conjecture, % 0.54/0.90 p31(f20(c36,c39),f17(c37,c40)) ). % 0.54/0.90 % 0.54/0.90 cnf(p11_20,negated_conjecture, % 0.54/0.90 ( p11(X1,X2) % 0.54/0.90 | ~ p11(X0,X1) % 0.54/0.90 | ~ p11(X0,X2) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p9_21,negated_conjecture, % 0.54/0.90 ( p9(X106,X107) % 0.54/0.90 | ~ p9(X105,X106) % 0.54/0.90 | ~ p9(X105,X107) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p8_22,negated_conjecture, % 0.54/0.90 ( p8(X99,X100) % 0.54/0.90 | ~ p8(X98,X99) % 0.54/0.90 | ~ p8(X98,X100) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p6_23,negated_conjecture, % 0.54/0.90 ( p6(X96,X97) % 0.54/0.90 | ~ p6(X95,X96) % 0.54/0.90 | ~ p6(X95,X97) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p5_24,negated_conjecture, % 0.54/0.90 ( p5(X93,X94) % 0.54/0.90 | ~ p5(X92,X93) % 0.54/0.90 | ~ p5(X92,X94) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p3_25,negated_conjecture, % 0.54/0.90 ( p3(X63,X64) % 0.54/0.90 | ~ p3(X62,X63) % 0.54/0.90 | ~ p3(X62,X64) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p28_26,negated_conjecture, % 0.54/0.90 ( p28(X58,X59) % 0.54/0.90 | ~ p28(X57,X58) % 0.54/0.90 | ~ p28(X57,X59) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p26_27,negated_conjecture, % 0.54/0.90 ( p26(X55,X56) % 0.54/0.90 | ~ p26(X54,X55) % 0.54/0.90 | ~ p26(X54,X56) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p24_28,negated_conjecture, % 0.54/0.90 ( p24(X48,X49) % 0.54/0.90 | ~ p24(X47,X48) % 0.54/0.90 | ~ p24(X47,X49) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p22_29,negated_conjecture, % 0.54/0.90 ( p22(X41,X42) % 0.54/0.90 | ~ p22(X40,X41) % 0.54/0.90 | ~ p22(X40,X42) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p21_30,negated_conjecture, % 0.54/0.90 ( p21(X34,X35) % 0.54/0.90 | ~ p21(X33,X34) % 0.54/0.90 | ~ p21(X33,X35) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p2_31,negated_conjecture, % 0.54/0.90 ( p2(X27,X28) % 0.54/0.90 | ~ p2(X26,X27) % 0.54/0.90 | ~ p2(X26,X28) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p19_32,negated_conjecture, % 0.54/0.90 ( p19(X20,X21) % 0.54/0.90 | ~ p19(X19,X20) % 0.54/0.90 | ~ p19(X19,X21) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p18_33,negated_conjecture, % 0.54/0.90 ( p18(X17,X18) % 0.54/0.90 | ~ p18(X16,X17) % 0.54/0.90 | ~ p18(X16,X18) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p16_34,negated_conjecture, % 0.54/0.90 ( p16(X10,X11) % 0.54/0.90 | ~ p16(X9,X10) % 0.54/0.90 | ~ p16(X9,X11) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p15_35,negated_conjecture, % 0.54/0.90 ( p15(X7,X8) % 0.54/0.90 | ~ p15(X6,X7) % 0.54/0.90 | ~ p15(X6,X8) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p13_36,negated_conjecture, % 0.54/0.90 ( p13(X4,X5) % 0.54/0.90 | ~ p13(X3,X4) % 0.54/0.90 | ~ p13(X3,X5) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p3_37,negated_conjecture, % 0.54/0.90 p3(f4(f7(c34,X77),f14(c38,X78)),f14(X77,X78)) ). % 0.54/0.90 % 0.54/0.90 cnf(p31_38,negated_conjecture, % 0.54/0.90 ( p31(X88,X89) % 0.54/0.90 | ~ p19(X91,X88) % 0.54/0.90 | ~ p31(X91,X90) % 0.54/0.90 | ~ p16(X90,X89) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p30_39,negated_conjecture, % 0.54/0.90 ( p30(X82,X83) % 0.54/0.90 | ~ p30(X85,X84) % 0.54/0.90 | ~ p9(X85,X82) % 0.54/0.90 | ~ p3(X84,X83) ) ). % 0.54/0.90 % 0.54/0.90 cnf(not_p30_40,negated_conjecture, % 0.54/0.90 ~ p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)) ). % 0.54/0.90 % 0.54/0.90 cnf(p16_41,negated_conjecture, % 0.54/0.90 ( p16(f17(X12,X13),f17(X14,X15)) % 0.54/0.90 | ~ p15(X12,X14) % 0.54/0.90 | ~ p3(X13,X15) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p9_42,negated_conjecture, % 0.54/0.90 ( p9(f10(X108,X109),f10(X110,X111)) % 0.54/0.90 | ~ p3(X109,X111) % 0.54/0.90 | ~ p8(X108,X110) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p8_43,negated_conjecture, % 0.54/0.90 ( p8(f12(X101,X102),f12(X103,X104)) % 0.54/0.90 | ~ p11(X101,X103) % 0.54/0.90 | ~ p8(X102,X104) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p3_44,negated_conjecture, % 0.54/0.90 ( p3(f4(X73,X74),f4(X75,X76)) % 0.54/0.90 | ~ p2(X73,X75) % 0.54/0.90 | ~ p3(X74,X76) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p3_45,negated_conjecture, % 0.54/0.90 ( p3(f23(X69,X70),f23(X71,X72)) % 0.54/0.90 | ~ p21(X69,X71) % 0.54/0.90 | ~ p22(X70,X72) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p3_46,negated_conjecture, % 0.54/0.90 ( p3(f14(X65,X66),f14(X67,X68)) % 0.54/0.90 | ~ p13(X66,X68) % 0.54/0.90 | ~ p6(X65,X67) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p24_47,negated_conjecture, % 0.54/0.90 ( p24(f27(X50,X51),f27(X52,X53)) % 0.54/0.90 | ~ p2(X51,X53) % 0.54/0.90 | ~ p26(X50,X52) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p22_48,negated_conjecture, % 0.54/0.90 ( p22(f25(X43,X44),f25(X45,X46)) % 0.54/0.90 | ~ p22(X44,X46) % 0.54/0.90 | ~ p24(X43,X45) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p21_49,negated_conjecture, % 0.54/0.90 ( p21(f29(X36,X37),f29(X38,X39)) % 0.54/0.90 | ~ p13(X37,X39) % 0.54/0.90 | ~ p28(X36,X38) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p2_50,negated_conjecture, % 0.54/0.90 ( p2(f7(X29,X30),f7(X31,X32)) % 0.54/0.90 | ~ p5(X29,X31) % 0.54/0.90 | ~ p6(X30,X32) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p19_51,negated_conjecture, % 0.54/0.90 ( p19(f20(X22,X23),f20(X24,X25)) % 0.54/0.90 | ~ p13(X23,X25) % 0.54/0.90 | ~ p18(X22,X24) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p3_52,negated_conjecture, % 0.54/0.90 p3(f4(f7(c34,X79),f23(f29(c41,X80),X81)),f23(f29(c41,X80),f25(f27(c42,f7(c34,X79)),X81))) ). % 0.54/0.90 % 0.54/0.90 cnf(p3_53,negated_conjecture, % 0.54/0.90 ( p3(X60,f14(c38,X61)) % 0.54/0.90 | p30(f10(f12(c32,c33),f14(c38,X61)),X60) % 0.54/0.90 | ~ p31(f20(c36,X61),f17(c37,X60)) ) ). % 0.54/0.90 % 0.54/0.90 cnf(p30_54,negated_conjecture, % 0.54/0.90 ( p30(f10(f12(c32,c33),f4(f7(c34,c35),X86)),f4(f7(c34,c35),X87)) % 0.54/0.90 | ~ p30(f10(f12(c32,c33),X86),X87) ) ). % 0.54/0.90 % 0.54/0.90 %-------------------------------------------------------------------------- % 0.54/0.90 %------------------------------------------- % 0.54/0.90 % Proof found % 0.54/0.90 % SZS status Theorem for theBenchmark % 0.54/0.90 % SZS output start Proof % 0.54/0.90 %ClaNum:54(EqnAxiom:0) % 0.54/0.90 %VarNum:260(SingletonVarNum:129) % 0.54/0.90 %MaxLitNum:4 % 0.54/0.90 %MaxfuncDepth:4 % 0.54/0.90 %SharedTerms:22 % 0.54/0.90 %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 % 0.54/0.90 %singleGoalClaCount:22 % 0.54/0.90 [18]P18(f9(a1,a6),f11(a7,a10)) % 0.54/0.90 [21]~P6(a10,f12(a8,a6)) % 0.54/0.90 [22]~P19(f16(f15(a3,a4),f12(a5,a6)),f18(f17(a2,a5),a10)) % 0.54/0.90 [1]P1(x11,x11) % 0.54/0.90 [2]P2(x21,x21) % 0.54/0.90 [3]P3(x31,x31) % 0.54/0.90 [4]P4(x41,x41) % 0.54/0.90 [5]P5(x51,x51) % 0.54/0.90 [6]P6(x61,x61) % 0.54/0.90 [7]P7(x71,x71) % 0.54/0.90 [8]P8(x81,x81) % 0.54/0.90 [9]P9(x91,x91) % 0.54/0.90 [10]P10(x101,x101) % 0.54/0.90 [11]P11(x111,x111) % 0.54/0.90 [12]P12(x121,x121) % 0.54/0.90 [13]P13(x131,x131) % 0.54/0.90 [14]P14(x141,x141) % 0.54/0.90 [15]P15(x151,x151) % 0.54/0.90 [16]P16(x161,x161) % 0.54/0.90 [17]P17(x171,x171) % 0.54/0.90 [19]P6(f18(f17(a2,x191),f12(a8,x192)),f12(x191,x192)) % 0.54/0.90 [20]P6(f18(f17(a2,x201),f20(f19(a13,x202),x203)),f20(f19(a13,x202),f22(f21(a14,f17(a2,x201)),x203))) % 0.54/0.90 [54]~P19(f16(f15(a3,a4),x541),x542)+P19(f16(f15(a3,a4),f18(f17(a2,a5),x541)),f18(f17(a2,a5),x542)) % 0.54/0.90 [53]P6(x531,f12(a8,x532))+~P18(f9(a1,x532),f11(a7,x531))+P19(f16(f15(a3,a4),f12(a8,x532)),x531) % 0.54/0.90 [23]~P1(x233,x231)+P1(x231,x232)+~P1(x233,x232) % 0.54/0.90 [24]~P2(x243,x241)+P2(x241,x242)+~P2(x243,x242) % 0.54/0.90 [25]~P3(x253,x251)+P3(x251,x252)+~P3(x253,x252) % 0.54/0.90 [26]~P4(x263,x261)+P4(x261,x262)+~P4(x263,x262) % 0.54/0.90 [27]~P5(x273,x271)+P5(x271,x272)+~P5(x273,x272) % 0.54/0.90 [28]~P6(x283,x281)+P6(x281,x282)+~P6(x283,x282) % 0.54/0.90 [29]~P7(x293,x291)+P7(x291,x292)+~P7(x293,x292) % 0.54/0.90 [30]~P8(x303,x301)+P8(x301,x302)+~P8(x303,x302) % 0.54/0.90 [31]~P9(x313,x311)+P9(x311,x312)+~P9(x313,x312) % 0.54/0.90 [32]~P10(x323,x321)+P10(x321,x322)+~P10(x323,x322) % 0.54/0.90 [33]~P11(x333,x331)+P11(x331,x332)+~P11(x333,x332) % 0.54/0.90 [34]~P12(x343,x341)+P12(x341,x342)+~P12(x343,x342) % 0.54/0.90 [35]~P13(x353,x351)+P13(x351,x352)+~P13(x353,x352) % 0.54/0.90 [36]~P14(x363,x361)+P14(x361,x362)+~P14(x363,x362) % 0.54/0.90 [37]~P15(x373,x371)+P15(x371,x372)+~P15(x373,x372) % 0.54/0.90 [38]~P16(x383,x381)+P16(x381,x382)+~P16(x383,x382) % 0.54/0.90 [39]~P17(x393,x391)+P17(x391,x392)+~P17(x393,x392) % 0.54/0.90 [42]~P3(x421,x423)+~P6(x422,x424)+P2(f16(x421,x422),f16(x423,x424)) % 0.54/0.90 [43]~P1(x431,x433)+~P3(x432,x434)+P3(f15(x431,x432),f15(x433,x434)) % 0.54/0.90 [44]~P4(x441,x443)+~P17(x442,x444)+P6(f12(x441,x442),f12(x443,x444)) % 0.54/0.90 [45]~P6(x452,x454)+~P12(x451,x453)+P6(f18(x451,x452),f18(x453,x454)) % 0.54/0.90 [46]~P10(x462,x464)+~P11(x461,x463)+P6(f20(x461,x462),f20(x463,x464)) % 0.54/0.90 [47]~P8(x471,x473)+~P12(x472,x474)+P9(f21(x471,x472),f21(x473,x474)) % 0.54/0.90 [48]~P9(x481,x483)+~P10(x482,x484)+P10(f22(x481,x482),f22(x483,x484)) % 0.54/0.90 [49]~P7(x491,x493)+~P17(x492,x494)+P11(f19(x491,x492),f19(x493,x494)) % 0.54/0.90 [50]~P4(x502,x504)+~P5(x501,x503)+P12(f17(x501,x502),f17(x503,x504)) % 0.54/0.90 [51]~P14(x511,x513)+~P17(x512,x514)+P13(f9(x511,x512),f9(x513,x514)) % 0.54/0.90 [52]~P6(x522,x524)+~P16(x521,x523)+P15(f11(x521,x522),f11(x523,x524)) % 0.54/0.90 [40]~P18(x403,x404)+P18(x401,x402)+~P13(x403,x401)+~P15(x404,x402) % 0.54/0.90 [41]~P19(x413,x414)+P19(x411,x412)+~P2(x413,x411)+~P6(x414,x412) % 0.54/0.90 %EqnAxiom % 0.54/0.90 % 0.54/0.90 %------------------------------------------- % 0.54/0.90 cnf(55,plain, % 0.54/0.90 (P19(f16(f15(a3,a4),f18(f17(a2,a5),f12(a8,a6))),f18(f17(a2,a5),a10))), % 0.54/0.91 inference(scs_inference,[],[18,21,54,53])). % 0.54/0.91 cnf(57,plain, % 0.54/0.91 (P6(f12(x571,x572),f18(f17(a2,x571),f12(a8,x572)))), % 0.54/0.91 inference(scs_inference,[],[19,6,28])). % 0.54/0.91 cnf(106,plain, % 0.54/0.91 (P2(f16(f15(x1061,x1062),f12(x1063,x1064)),f16(f15(x1061,x1062),f18(f17(a2,x1063),f12(a8,x1064))))), % 0.54/0.91 inference(scs_inference,[],[1,3,57,43,42])). % 0.54/0.91 cnf(107,plain, % 0.54/0.91 (P2(f16(f15(x1071,x1072),f18(f17(a2,x1073),f12(a8,x1074))),f16(f15(x1071,x1072),f12(x1073,x1074)))), % 0.54/0.91 inference(scs_inference,[],[106,2,24])). % 0.54/0.91 cnf(247,plain, % 0.54/0.91 ($false), % 0.54/0.91 inference(scs_inference,[],[6,107,55,22,41]), % 0.54/0.91 ['proof']). % 0.54/0.91 % SZS output end Proof % 0.54/0.91 % Total time :0.280000s %------------------------------------------------------------------------------