%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN648-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 : n025.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:12 EDT 2024 % Result : Unsatisfiable 58.60s 58.68s % Output : CNFRefutation 58.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : SYN648-1 : TPTP v8.2.0. Released v2.5.0. % 0.09/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.35 % Computer : n025.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Sun Jun 23 23:33:39 EDT 2024 % 0.14/0.35 % CPUTime : % 0.55/0.59 start to proof:theBenchmark % 58.60/58.66 %------------------------------------------- % 58.60/58.66 % File :CSE---1.7 % 58.60/58.66 % Problem :theBenchmark % 58.60/58.66 % Transform :cnf % 58.60/58.66 % Format :tptp:raw % 58.60/58.66 % Command :java -jar mcs_scs.jar %d %s % 58.60/58.66 % 58.60/58.66 % Result :Theorem 58.010000s % 58.60/58.66 % Output :CNFRefutation 58.010000s % 58.60/58.66 %------------------------------------------- % 58.60/58.67 %-------------------------------------------------------------------------- % 58.60/58.67 % File : SYN648-1 : TPTP v8.2.0. Released v2.5.0. % 58.60/58.67 % Domain : Syntactic % 58.60/58.67 % Problem : Harrison problem 4401 % 58.60/58.67 % Version : Especial. % 58.60/58.67 % English : % 58.60/58.67 % 58.60/58.67 % Refs : [Har01] Email to G. Sutcliffe % 58.60/58.67 % Source : [Har01] % 58.60/58.67 % Names : % 58.60/58.67 % 58.60/58.67 % Status : Unsatisfiable % 58.60/58.67 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.12 v5.4.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.21 v4.1.0, 0.12 v4.0.1, 0.00 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.2.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.12 v2.6.0, 0.00 v2.5.0 % 58.60/58.67 % Syntax : Number of clauses : 44 ( 16 unt; 1 nHn; 31 RR) % 58.60/58.67 % Number of literals : 107 ( 0 equ; 63 neg) % 58.60/58.67 % Maximal clause size : 6 ( 2 avg) % 58.60/58.67 % Maximal term depth : 6 ( 1 avg) % 58.60/58.67 % Number of predicates : 15 ( 15 usr; 0 prp; 2-2 aty) % 58.60/58.67 % Number of functors : 18 ( 18 usr; 8 con; 0-2 aty) % 58.60/58.67 % Number of variables : 110 ( 0 sgn) % 58.60/58.67 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.60/58.67 % 58.60/58.67 % Comments : % 58.60/58.67 %-------------------------------------------------------------------------- % 58.60/58.67 cnf(p10_1,negated_conjecture, % 58.60/58.67 p10(X0,X0) ). % 58.60/58.67 % 58.60/58.67 cnf(p8_2,negated_conjecture, % 58.60/58.67 p8(X86,X86) ). % 58.60/58.67 % 58.60/58.67 cnf(p7_3,negated_conjecture, % 58.60/58.67 p7(X79,X79) ). % 58.60/58.67 % 58.60/58.67 cnf(p5_4,negated_conjecture, % 58.60/58.67 p5(X76,X76) ). % 58.60/58.67 % 58.60/58.67 cnf(p3_5,negated_conjecture, % 58.60/58.67 p3(X65,X65) ). % 58.60/58.67 % 58.60/58.67 cnf(p25_6,negated_conjecture, % 58.60/58.67 p25(X58,X58) ). % 58.60/58.67 % 58.60/58.67 cnf(p22_7,negated_conjecture, % 58.60/58.67 p22(X45,X45) ). % 58.60/58.67 % 58.60/58.67 cnf(p20_8,negated_conjecture, % 58.60/58.67 p20(X38,X38) ). % 58.60/58.67 % 58.60/58.67 cnf(p2_9,negated_conjecture, % 58.60/58.67 p2(X31,X31) ). % 58.60/58.67 % 58.60/58.67 cnf(p18_10,negated_conjecture, % 58.60/58.67 p18(X24,X24) ). % 58.60/58.67 % 58.60/58.67 cnf(p16_11,negated_conjecture, % 58.60/58.67 p16(X17,X17) ). % 58.60/58.67 % 58.60/58.67 cnf(p14_12,negated_conjecture, % 58.60/58.67 p14(X14,X14) ). % 58.60/58.67 % 58.60/58.67 cnf(p12_13,negated_conjecture, % 58.60/58.67 p12(X7,X7) ). % 58.60/58.67 % 58.60/58.67 cnf(p2_14,negated_conjecture, % 58.60/58.67 p2(c27,c30) ). % 58.60/58.67 % 58.60/58.67 cnf(p26_15,negated_conjecture, % 58.60/58.67 p26(c31,c30) ). % 58.60/58.67 % 58.60/58.67 cnf(not_p24_16,negated_conjecture, % 58.60/58.67 ~ p24(f4(c27,c28),c29) ). % 58.60/58.67 % 58.60/58.67 cnf(p10_17,negated_conjecture, % 58.60/58.67 ( p10(X1,X2) % 58.60/58.67 | ~ p10(X0,X1) % 58.60/58.67 | ~ p10(X0,X2) ) ). % 58.60/58.67 % 58.60/58.67 cnf(p8_18,negated_conjecture, % 58.60/58.67 ( p8(X87,X88) % 58.60/58.67 | ~ p8(X86,X87) % 58.60/58.67 | ~ p8(X86,X88) ) ). % 58.60/58.67 % 58.60/58.67 cnf(p7_19,negated_conjecture, % 58.60/58.67 ( p7(X80,X81) % 58.60/58.67 | ~ p7(X79,X80) % 58.60/58.67 | ~ p7(X79,X81) ) ). % 58.60/58.67 % 58.60/58.67 cnf(p5_20,negated_conjecture, % 58.60/58.67 ( p5(X77,X78) % 58.60/58.67 | ~ p5(X76,X77) % 58.60/58.67 | ~ p5(X76,X78) ) ). % 58.60/58.67 % 58.60/58.67 cnf(p3_21,negated_conjecture, % 58.60/58.67 ( p3(X66,X67) % 58.60/58.67 | ~ p3(X65,X66) % 58.60/58.67 | ~ p3(X65,X67) ) ). % 58.60/58.67 % 58.60/58.67 cnf(p25_22,negated_conjecture, % 58.60/58.67 ( p25(X59,X60) % 58.60/58.67 | ~ p25(X58,X59) % 58.60/58.67 | ~ p25(X58,X60) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p22_23,negated_conjecture, % 58.60/58.68 ( p22(X46,X47) % 58.60/58.68 | ~ p22(X45,X46) % 58.60/58.68 | ~ p22(X45,X47) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p20_24,negated_conjecture, % 58.60/58.68 ( p20(X39,X40) % 58.60/58.68 | ~ p20(X38,X39) % 58.60/58.68 | ~ p20(X38,X40) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p2_25,negated_conjecture, % 58.60/58.68 ( p2(X32,X33) % 58.60/58.68 | ~ p2(X31,X32) % 58.60/58.68 | ~ p2(X31,X33) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p18_26,negated_conjecture, % 58.60/58.68 ( p18(X25,X26) % 58.60/58.68 | ~ p18(X24,X25) % 58.60/58.68 | ~ p18(X24,X26) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p16_27,negated_conjecture, % 58.60/58.68 ( p16(X18,X19) % 58.60/58.68 | ~ p16(X17,X18) % 58.60/58.68 | ~ p16(X17,X19) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p14_28,negated_conjecture, % 58.60/58.68 ( p14(X15,X16) % 58.60/58.68 | ~ p14(X14,X15) % 58.60/58.68 | ~ p14(X14,X16) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p12_29,negated_conjecture, % 58.60/58.68 ( p12(X8,X9) % 58.60/58.68 | ~ p12(X7,X8) % 58.60/58.68 | ~ p12(X7,X9) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p24_30,negated_conjecture, % 58.60/58.68 ( p24(f4(c30,X56),X57) % 58.60/58.68 | ~ p24(f4(f6(c32,c30),X56),X57) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p24_31,negated_conjecture, % 58.60/58.68 ( p24(X48,X49) % 58.60/58.68 | ~ p3(X50,X48) % 58.60/58.68 | ~ p8(X51,X49) % 58.60/58.68 | ~ p24(X50,X51) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p26_32,negated_conjecture, % 58.60/58.68 ( p26(X61,X62) % 58.60/58.68 | ~ p25(X64,X61) % 58.60/58.68 | ~ p26(X64,X63) % 58.60/58.68 | ~ p2(X63,X62) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p8_33,negated_conjecture, % 58.60/58.68 ( p8(f9(X89,X90),f9(X91,X92)) % 58.60/58.68 | ~ p2(X90,X92) % 58.60/58.68 | ~ p7(X89,X91) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p10_34,negated_conjecture, % 58.60/58.68 ( p10(f13(X3,X4),f13(X5,X6)) % 58.60/58.68 | ~ p12(X3,X5) % 58.60/58.68 | ~ p3(X4,X6) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p12_35,negated_conjecture, % 58.60/58.68 ( p12(f15(X10,X11),f15(X12,X13)) % 58.60/58.68 | ~ p14(X10,X12) % 58.60/58.68 | ~ p3(X11,X13) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p16_36,negated_conjecture, % 58.60/58.68 ( p16(f19(X20,X21),f19(X22,X23)) % 58.60/58.68 | ~ p18(X20,X22) % 58.60/58.68 | ~ p2(X21,X23) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p18_37,negated_conjecture, % 58.60/58.68 ( p18(f21(X27,X28),f21(X29,X30)) % 58.60/58.68 | ~ p20(X27,X29) % 58.60/58.68 | ~ p3(X28,X30) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p2_38,negated_conjecture, % 58.60/58.68 ( p2(f6(X34,X35),f6(X36,X37)) % 58.60/58.68 | ~ p2(X35,X37) % 58.60/58.68 | ~ p5(X34,X36) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p20_39,negated_conjecture, % 58.60/58.68 ( p20(f23(X41,X42),f23(X43,X44)) % 58.60/58.68 | ~ p22(X41,X43) % 58.60/58.68 | ~ p3(X42,X44) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p3_40,negated_conjecture, % 58.60/58.68 ( p3(f17(X68,X69),f17(X70,X71)) % 58.60/58.68 | ~ p16(X68,X70) % 58.60/58.68 | ~ p2(X69,X71) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p3_41,negated_conjecture, % 58.60/58.68 ( p3(f4(X72,X73),f4(X74,X75)) % 58.60/58.68 | ~ p2(X72,X74) % 58.60/58.68 | ~ p3(X73,X75) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p7_42,negated_conjecture, % 58.60/58.68 ( p7(f11(X82,X83),f11(X84,X85)) % 58.60/58.68 | ~ p10(X82,X84) % 58.60/58.68 | ~ p2(X83,X85) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p24_43,negated_conjecture, % 58.60/58.68 ( p24(X52,c29) % 58.60/58.68 | ~ p3(X52,X54) % 58.60/58.68 | ~ p2(X55,X53) % 58.60/58.68 | ~ p26(c31,X53) % 58.60/58.68 | ~ p3(X54,f4(X55,c28)) % 58.60/58.68 | ~ p24(f4(X53,f17(f19(f21(f23(c33,X52),X54),X55),X53)),f9(f11(f13(f15(c34,X52),X54),X55),X53)) ) ). % 58.60/58.68 % 58.60/58.68 cnf(p24_44,negated_conjecture, % 58.60/58.68 ( p24(X52,c29) % 58.60/58.68 | p24(f4(f6(c32,X53),f17(f19(f21(f23(c33,X52),X54),X55),X53)),f9(f11(f13(f15(c34,X52),X54),X55),X53)) % 58.60/58.68 | ~ p3(X52,X54) % 58.60/58.68 | ~ p2(X55,X53) % 58.60/58.68 | ~ p26(c31,X53) % 58.60/58.68 | ~ p3(X54,f4(X55,c28)) ) ). % 58.60/58.68 % 58.60/58.68 %-------------------------------------------------------------------------- % 58.60/58.68 %------------------------------------------- % 58.60/58.68 % Proof found % 58.60/58.68 % SZS status Theorem for theBenchmark % 58.60/58.68 % SZS output start Proof % 58.60/58.68 %ClaNum:44(EqnAxiom:0) % 58.60/58.68 %VarNum:238(SingletonVarNum:110) % 58.60/58.68 %MaxLitNum:6 % 58.60/58.68 %MaxfuncDepth:5 % 58.60/58.68 %SharedTerms:13 % 58.60/58.68 %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 % 58.60/58.68 %singleGoalClaCount:16 % 58.60/58.68 [1]P1(a1,a2) % 58.60/58.68 [2]P7(a5,a2) % 58.60/58.68 [16]~P11(f6(a1,a3),a4) % 58.60/58.68 [3]P2(x31,x31) % 58.60/58.68 [4]P12(x41,x41) % 58.60/58.68 [5]P13(x51,x51) % 58.60/58.68 [6]P14(x61,x61) % 58.60/58.68 [7]P15(x71,x71) % 58.60/58.68 [8]P8(x81,x81) % 58.60/58.68 [9]P9(x91,x91) % 58.60/58.68 [10]P10(x101,x101) % 58.60/58.68 [11]P1(x111,x111) % 58.60/58.68 [12]P3(x121,x121) % 58.60/58.68 [13]P4(x131,x131) % 58.60/58.68 [14]P5(x141,x141) % 58.60/58.68 [15]P6(x151,x151) % 58.60/58.68 [42]P11(f6(a2,x421),x422)+~P11(f6(f18(a9,a2),x421),x422) % 58.60/58.68 [17]~P2(x173,x171)+P2(x171,x172)+~P2(x173,x172) % 58.60/58.68 [18]~P12(x183,x181)+P12(x181,x182)+~P12(x183,x182) % 58.60/58.68 [19]~P13(x193,x191)+P13(x191,x192)+~P13(x193,x192) % 58.60/58.68 [20]~P14(x203,x201)+P14(x201,x202)+~P14(x203,x202) % 58.60/58.68 [21]~P15(x213,x211)+P15(x211,x212)+~P15(x213,x212) % 58.60/58.68 [22]~P8(x223,x221)+P8(x221,x222)+~P8(x223,x222) % 58.60/58.68 [23]~P9(x233,x231)+P9(x231,x232)+~P9(x233,x232) % 58.60/58.68 [24]~P10(x243,x241)+P10(x241,x242)+~P10(x243,x242) % 58.60/58.68 [25]~P1(x253,x251)+P1(x251,x252)+~P1(x253,x252) % 58.60/58.68 [26]~P3(x263,x261)+P3(x261,x262)+~P3(x263,x262) % 58.60/58.68 [27]~P4(x273,x271)+P4(x271,x272)+~P4(x273,x272) % 58.60/58.68 [28]~P5(x283,x281)+P5(x281,x282)+~P5(x283,x282) % 58.60/58.68 [29]~P6(x293,x291)+P6(x291,x292)+~P6(x293,x292) % 58.60/58.68 [32]~P15(x322,x324)+~P6(x321,x323)+P2(f7(x321,x322),f7(x323,x324)) % 58.60/58.68 [33]~P13(x331,x333)+~P1(x332,x334)+P12(f17(x331,x332),f17(x333,x334)) % 58.60/58.68 [34]~P2(x341,x343)+~P1(x342,x344)+P13(f8(x341,x342),f8(x343,x344)) % 58.60/58.68 [35]~P15(x352,x354)+~P1(x351,x353)+P15(f6(x351,x352),f6(x353,x354)) % 58.60/58.68 [36]~P1(x362,x364)+~P4(x361,x363)+P15(f12(x361,x362),f12(x363,x364)) % 58.60/58.68 [37]~P15(x372,x374)+~P9(x371,x373)+P10(f14(x371,x372),f14(x373,x374)) % 58.60/58.68 [38]~P14(x381,x383)+~P1(x382,x384)+P1(f18(x381,x382),f18(x383,x384)) % 58.60/58.68 [39]~P15(x392,x394)+~P10(x391,x393)+P3(f15(x391,x392),f15(x393,x394)) % 58.60/58.68 [40]~P1(x402,x404)+~P3(x401,x403)+P4(f16(x401,x402),f16(x403,x404)) % 58.60/58.68 [41]~P15(x412,x414)+~P5(x411,x413)+P6(f13(x411,x412),f13(x413,x414)) % 58.60/58.68 [30]~P7(x303,x304)+P7(x301,x302)+~P8(x303,x301)+~P1(x304,x302) % 58.60/58.68 [31]~P11(x314,x313)+P11(x311,x312)+~P12(x313,x312)+~P15(x314,x311) % 58.60/58.68 [43]~P15(x431,x433)+~P1(x434,x432)+~P7(a5,x432)+P11(x431,a4)+~P15(x433,f6(x434,a3))+P11(f6(f18(a9,x432),f12(f16(f15(f14(a10,x431),x433),x434),x432)),f17(f8(f7(f13(a11,x431),x433),x434),x432)) % 58.60/58.68 [44]~P15(x441,x442)+~P1(x443,x444)+~P7(a5,x444)+P11(x441,a4)+~P15(x442,f6(x443,a3))+~P11(f6(x444,f12(f16(f15(f14(a10,x441),x442),x443),x444)),f17(f8(f7(f13(a11,x441),x442),x443),x444)) % 58.60/58.68 %EqnAxiom % 58.60/58.68 % 58.60/58.68 %------------------------------------------- % 58.60/58.69 cnf(52,plain, % 58.60/58.69 (P13(f8(x521,a1),f8(x521,a2))), % 58.60/58.69 inference(scs_inference,[],[3,1,17,34])). % 58.60/58.69 cnf(53,plain, % 58.60/58.69 (P13(f8(x531,a2),f8(x531,a1))), % 58.60/58.69 inference(scs_inference,[],[52,5,19])). % 58.60/58.69 cnf(57,plain, % 58.60/58.69 (P15(f6(a1,x571),f6(a2,x571))), % 58.60/58.69 inference(scs_inference,[],[7,1,21,35])). % 58.60/58.69 cnf(58,plain, % 58.60/58.69 (P15(f6(a2,x581),f6(a1,x581))), % 58.60/58.69 inference(scs_inference,[],[57,7,21])). % 58.60/58.69 cnf(64,plain, % 58.60/58.69 (~P11(f6(a2,a3),a4)), % 58.60/58.69 inference(scs_inference,[],[58,4,16,31])). % 58.60/58.69 cnf(373,plain, % 58.60/58.69 (P12(f17(f8(x3731,a2),a2),f17(f8(x3731,a1),a2))), % 58.60/58.69 inference(scs_inference,[],[1,53,25,33])). % 58.60/58.69 cnf(374,plain, % 58.60/58.69 (~P11(f6(a1,x3741),f17(f8(x3742,a2),a2))+P11(f6(a2,x3741),f17(f8(x3742,a1),a2))), % 58.60/58.69 inference(scs_inference,[],[57,373,31])). % 58.60/58.69 cnf(379,plain, % 58.60/58.69 (~P11(f6(a1,f12(f16(f15(f14(a10,f6(a2,a3)),f6(a2,a3)),a1),a2)),f17(f8(f7(f13(a11,f6(a2,a3)),f6(a2,a3)),a2),a2))), % 58.60/58.69 inference(scs_inference,[],[58,2,64,7,1,374,44])). % 58.60/58.69 cnf(423,plain, % 58.60/58.69 (P12(f17(f8(x4231,a1),a2),f17(f8(x4231,a2),a2))), % 58.60/58.69 inference(scs_inference,[],[373,4,18])). % 58.60/58.69 cnf(486,plain, % 58.60/58.69 (~P11(f6(a2,x4861),f17(f8(x4862,a1),a2))+P11(f6(a1,x4861),f17(f8(x4862,a2),a2))), % 58.60/58.69 inference(scs_inference,[],[58,423,31])). % 58.60/58.69 cnf(492,plain, % 58.60/58.69 (P11(f6(a1,x4921),f17(f8(x4922,a2),a2))+~P11(f6(f18(a9,a2),x4921),f17(f8(x4922,a1),a2))), % 58.60/58.69 inference(scs_inference,[],[486,42])). % 58.60/58.69 cnf(498,plain, % 58.60/58.69 (P11(f6(a1,f12(f16(f15(f14(a10,f6(a2,a3)),f6(a2,a3)),a1),a2)),f17(f8(f7(f13(a11,f6(a2,a3)),f6(a2,a3)),a2),a2))), % 58.60/58.69 inference(scs_inference,[],[58,2,64,7,1,492,43])). % 58.60/58.69 cnf(2658,plain, % 58.60/58.69 ($false), % 58.60/58.70 inference(scs_inference,[],[498,379]), % 58.60/58.70 ['proof']). % 58.60/58.70 % SZS output end Proof % 58.60/58.70 % Total time :58.010000s %------------------------------------------------------------------------------