%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN659-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:14 EDT 2024 % Result : Unsatisfiable 58.72s 58.74s % Output : CNFRefutation 58.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN659-1 : TPTP v8.2.0. Released v2.5.0. % 0.11/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 22:25:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.54 start to proof:theBenchmark % 58.72/58.73 %------------------------------------------- % 58.72/58.73 % File :CSE---1.7 % 58.72/58.73 % Problem :theBenchmark % 58.72/58.73 % Transform :cnf % 58.72/58.73 % Format :tptp:raw % 58.72/58.73 % Command :java -jar mcs_scs.jar %d %s % 58.72/58.73 % 58.72/58.73 % Result :Theorem 58.140000s % 58.72/58.73 % Output :CNFRefutation 58.140000s % 58.72/58.73 %------------------------------------------- % 58.72/58.74 %-------------------------------------------------------------------------- % 58.72/58.74 % File : SYN659-1 : TPTP v8.2.0. Released v2.5.0. % 58.72/58.74 % Domain : Syntactic % 58.72/58.74 % Problem : Harrison problem 4504 % 58.72/58.74 % Version : Especial. % 58.72/58.74 % English : % 58.72/58.74 % 58.72/58.74 % Refs : [Har01] Email to G. Sutcliffe % 58.72/58.74 % Source : [Har01] % 58.72/58.74 % Names : % 58.72/58.74 % 58.72/58.74 % Status : Unsatisfiable % 58.72/58.74 % Rating : 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.2.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.00 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.00 v2.6.0, 0.33 v2.5.0 % 58.72/58.74 % Syntax : Number of clauses : 51 ( 22 unt; 2 nHn; 41 RR) % 58.72/58.74 % Number of literals : 107 ( 0 equ; 56 neg) % 58.72/58.74 % Maximal clause size : 5 ( 2 avg) % 58.72/58.74 % Maximal term depth : 4 ( 1 avg) % 58.72/58.74 % Number of predicates : 14 ( 14 usr; 0 prp; 1-3 aty) % 58.72/58.74 % Number of functors : 26 ( 26 usr; 15 con; 0-2 aty) % 58.72/58.74 % Number of variables : 105 ( 5 sgn) % 58.72/58.74 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.72/58.74 % 58.72/58.74 % Comments : % 58.72/58.74 %-------------------------------------------------------------------------- % 58.72/58.74 cnf(c27_is_p22_1,negated_conjecture, % 58.72/58.74 p22(c27) ). % 58.72/58.74 % 58.72/58.74 cnf(p10_2,negated_conjecture, % 58.72/58.74 p10(X0,X0) ). % 58.72/58.74 % 58.72/58.74 cnf(p7_3,negated_conjecture, % 58.72/58.74 p7(X87,X87) ). % 58.72/58.74 % 58.72/58.74 cnf(p6_4,negated_conjecture, % 58.72/58.74 p6(X84,X84) ). % 58.72/58.74 % 58.72/58.74 cnf(p3_5,negated_conjecture, % 58.72/58.74 p3(X79,X79) ). % 58.72/58.74 % 58.72/58.74 cnf(p20_6,negated_conjecture, % 58.72/58.74 p20(X51,X51) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_7,negated_conjecture, % 58.72/58.74 p2(X32,X32) ). % 58.72/58.74 % 58.72/58.74 cnf(p19_8,negated_conjecture, % 58.72/58.74 p19(X29,X29) ). % 58.72/58.74 % 58.72/58.74 cnf(p14_9,negated_conjecture, % 58.72/58.74 p14(X20,X20) ). % 58.72/58.74 % 58.72/58.74 cnf(p12_10,negated_conjecture, % 58.72/58.74 p12(X13,X13) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_11,negated_conjecture, % 58.72/58.74 p2(c41,c38) ). % 58.72/58.74 % 58.72/58.74 cnf(p10_12,negated_conjecture, % 58.72/58.74 p10(f16(c31),c32) ). % 58.72/58.74 % 58.72/58.74 cnf(p7_13,negated_conjecture, % 58.72/58.74 p7(f8(c28),c29) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_14,negated_conjecture, % 58.72/58.74 p2(f17(c36),c38) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_15,negated_conjecture, % 58.72/58.74 p2(f17(c31),c33) ). % 58.72/58.74 % 58.72/58.74 cnf(p10_16,negated_conjecture, % 58.72/58.74 p10(f16(c36),c37) ). % 58.72/58.74 % 58.72/58.74 cnf(not_p14_17,negated_conjecture, % 58.72/58.74 ~ p14(f18(c34),c35) ). % 58.72/58.74 % 58.72/58.74 cnf(p23_18,negated_conjecture, % 58.72/58.74 p23(c27,f4(f5(X66)),f4(X66)) ). % 58.72/58.74 % 58.72/58.74 cnf(p22_19,negated_conjecture, % 58.72/58.74 ( p22(X58) % 58.72/58.74 | ~ p22(X59) % 58.72/58.74 | ~ p19(X59,X58) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p10_20,negated_conjecture, % 58.72/58.74 ( p10(f16(X11),f16(X12)) % 58.72/58.74 | ~ p12(X11,X12) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p7_21,negated_conjecture, % 58.72/58.74 ( p7(f8(X90),f8(X91)) % 58.72/58.74 | ~ p6(X90,X91) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p3_22,negated_conjecture, % 58.72/58.74 ( p3(f4(X82),f4(X83)) % 58.72/58.74 | ~ p2(X82,X83) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_23,negated_conjecture, % 58.72/58.74 ( p2(f9(X49),f9(X50)) % 58.72/58.74 | ~ p2(X49,X50) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_24,negated_conjecture, % 58.72/58.74 ( p2(f5(X47),f5(X48)) % 58.72/58.74 | ~ p2(X47,X48) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_25,negated_conjecture, % 58.72/58.74 ( p2(f17(X45),f17(X46)) % 58.72/58.74 | ~ p12(X45,X46) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p14_26,negated_conjecture, % 58.72/58.74 ( p14(f18(X27),f18(X28)) % 58.72/58.74 | ~ p14(X27,X28) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p24_27,negated_conjecture, % 58.72/58.74 p24(f15(c29,f13(c40,c41)),f13(c32,c33)) ). % 58.72/58.74 % 58.72/58.74 cnf(p24_28,negated_conjecture, % 58.72/58.74 p24(f15(c29,f13(c37,c38)),f13(c32,c33)) ). % 58.72/58.74 % 58.72/58.74 cnf(p12_29,negated_conjecture, % 58.72/58.74 p12(f13(f16(c39),f17(c39)),f13(c40,c41)) ). % 58.72/58.74 % 58.72/58.74 cnf(p10_30,negated_conjecture, % 58.72/58.74 ( p10(X1,X2) % 58.72/58.74 | ~ p10(X0,X1) % 58.72/58.74 | ~ p10(X0,X2) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p7_31,negated_conjecture, % 58.72/58.74 ( p7(X88,X89) % 58.72/58.74 | ~ p7(X87,X88) % 58.72/58.74 | ~ p7(X87,X89) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p6_32,negated_conjecture, % 58.72/58.74 ( p6(X85,X86) % 58.72/58.74 | ~ p6(X84,X85) % 58.72/58.74 | ~ p6(X84,X86) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p3_33,negated_conjecture, % 58.72/58.74 ( p3(X80,X81) % 58.72/58.74 | ~ p3(X79,X80) % 58.72/58.74 | ~ p3(X79,X81) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p20_34,negated_conjecture, % 58.72/58.74 ( p20(X52,X53) % 58.72/58.74 | ~ p20(X51,X52) % 58.72/58.74 | ~ p20(X51,X53) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_35,negated_conjecture, % 58.72/58.74 ( p2(X33,X34) % 58.72/58.74 | ~ p2(X32,X33) % 58.72/58.74 | ~ p2(X32,X34) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p19_36,negated_conjecture, % 58.72/58.74 ( p19(X30,X31) % 58.72/58.74 | ~ p19(X29,X30) % 58.72/58.74 | ~ p19(X29,X31) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p14_37,negated_conjecture, % 58.72/58.74 ( p14(X21,X22) % 58.72/58.74 | ~ p14(X20,X21) % 58.72/58.74 | ~ p14(X20,X22) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p12_38,negated_conjecture, % 58.72/58.74 ( p12(X14,X15) % 58.72/58.74 | ~ p12(X13,X14) % 58.72/58.74 | ~ p12(X13,X15) ) ). % 58.72/58.74 % 58.72/58.74 cnf(not_p24_39,negated_conjecture, % 58.72/58.74 ~ p24(f15(c29,f13(f16(c39),f17(c39))),f13(c32,c33)) ). % 58.72/58.74 % 58.72/58.74 cnf(p26_40,negated_conjecture, % 58.72/58.74 ( p26(X75,X76) % 58.72/58.74 | ~ p2(X78,X76) % 58.72/58.74 | ~ p26(X77,X78) % 58.72/58.74 | ~ p2(X77,X75) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p24_41,negated_conjecture, % 58.72/58.74 ( p24(X67,X68) % 58.72/58.74 | ~ p14(X70,X67) % 58.72/58.74 | ~ p24(X70,X69) % 58.72/58.74 | ~ p12(X69,X68) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p25_42,negated_conjecture, % 58.72/58.74 ( p25(X71,X72) % 58.72/58.74 | ~ p20(X74,X71) % 58.72/58.74 | ~ p25(X74,X73) % 58.72/58.74 | ~ p10(X73,X72) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p20_43,negated_conjecture, % 58.72/58.74 ( p20(f21(X54,X55),f21(X56,X57)) % 58.72/58.74 | ~ p10(X55,X57) % 58.72/58.74 | ~ p19(X54,X56) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p12_44,negated_conjecture, % 58.72/58.74 ( p12(f13(X16,X17),f13(X18,X19)) % 58.72/58.74 | ~ p10(X16,X18) % 58.72/58.74 | ~ p2(X17,X19) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p14_45,negated_conjecture, % 58.72/58.74 ( p14(f15(X23,X24),f15(X25,X26)) % 58.72/58.74 | ~ p12(X24,X26) % 58.72/58.74 | ~ p7(X23,X25) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_46,negated_conjecture, % 58.72/58.74 ( p2(f11(X41,X42),f11(X43,X44)) % 58.72/58.74 | ~ p10(X42,X44) % 58.72/58.74 | ~ p3(X41,X43) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p10_47,negated_conjecture, % 58.72/58.74 ( p10(X7,X8) % 58.72/58.74 | p25(f21(c27,X7),X8) % 58.72/58.74 | ~ p24(f15(c29,f13(X7,X9)),f13(X8,X10)) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p23_48,negated_conjecture, % 58.72/58.74 ( p23(X60,X61,X62) % 58.72/58.74 | ~ p3(X65,X62) % 58.72/58.74 | ~ p3(X64,X61) % 58.72/58.74 | ~ p19(X63,X60) % 58.72/58.74 | ~ p23(X63,X64,X65) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p10_49,negated_conjecture, % 58.72/58.74 ( p10(X3,X4) % 58.72/58.74 | ~ p2(f11(f4(X5),X3),f9(c30)) % 58.72/58.74 | ~ p24(f15(c29,f13(X3,X5)),f13(X4,X6)) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p2_50,negated_conjecture, % 58.72/58.74 ( p2(X35,X36) % 58.72/58.74 | ~ p24(f15(c29,f13(X37,X35)),f13(X38,X39)) % 58.72/58.74 | ~ p24(f15(c29,f13(X40,X36)),f13(X38,X39)) ) ). % 58.72/58.74 % 58.72/58.74 cnf(p25_51,negated_conjecture, % 58.72/58.74 ( p25(f21(c27,X7),X8) % 58.72/58.74 | p26(f11(f4(X9),X8),f11(f4(X10),X8)) % 58.72/58.74 | ~ p24(f15(c29,f13(X7,X9)),f13(X8,X10)) ) ). % 58.72/58.74 % 58.72/58.74 %-------------------------------------------------------------------------- % 58.72/58.74 %------------------------------------------- % 58.72/58.74 % Proof found % 58.72/58.74 % SZS status Theorem for theBenchmark % 58.72/58.74 % SZS output start Proof % 58.72/58.75 %ClaNum:51(EqnAxiom:0) % 58.72/58.75 %VarNum:210(SingletonVarNum:105) % 58.72/58.75 %MaxLitNum:5 % 58.72/58.75 %MaxfuncDepth:3 % 58.72/58.75 %SharedTerms:43 % 58.72/58.75 %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 % 58.72/58.75 %singleGoalClaCount:22 % 58.72/58.75 [1]P1(a1) % 58.72/58.75 [2]P2(a2,a3) % 58.72/58.75 [12]P3(f16(a4),a8) % 58.72/58.75 [13]P3(f16(a9),a13) % 58.72/58.75 [14]P8(f20(a5),a6) % 58.72/58.75 [15]P2(f21(a4),a10) % 58.72/58.75 [16]P2(f21(a9),a3) % 58.72/58.75 [21]~P5(f24(a11),a12) % 58.72/58.75 [17]P6(f17(f16(a14),f21(a14)),f17(a15,a2)) % 58.72/58.75 [19]P12(f19(a6,f17(a13,a3)),f17(a8,a10)) % 58.72/58.75 [20]P12(f19(a6,f17(a15,a2)),f17(a8,a10)) % 58.72/58.75 [22]~P12(f19(a6,f17(f16(a14),f21(a14))),f17(a8,a10)) % 58.72/58.75 [3]P3(x31,x31) % 58.72/58.75 [4]P8(x41,x41) % 58.72/58.75 [5]P9(x51,x51) % 58.72/58.75 [6]P10(x61,x61) % 58.72/58.75 [7]P7(x71,x71) % 58.72/58.75 [8]P2(x81,x81) % 58.72/58.75 [9]P4(x91,x91) % 58.72/58.75 [10]P5(x101,x101) % 58.72/58.75 [11]P6(x111,x111) % 58.72/58.75 [18]P11(a1,f23(f22(x181)),f23(x181)) % 58.72/58.75 [24]~P6(x241,x242)+P3(f16(x241),f16(x242)) % 58.72/58.75 [25]~P9(x251,x252)+P8(f20(x251),f20(x252)) % 58.72/58.75 [26]~P2(x261,x262)+P10(f23(x261),f23(x262)) % 58.72/58.75 [27]~P6(x271,x272)+P2(f21(x271),f21(x272)) % 58.72/58.75 [28]~P2(x281,x282)+P2(f22(x281),f22(x282)) % 58.72/58.75 [29]~P2(x291,x292)+P2(f26(x291),f26(x292)) % 58.72/58.75 [30]~P5(x301,x302)+P5(f24(x301),f24(x302)) % 58.72/58.75 [23]~P4(x232,x231)+P1(x231)+~P1(x232) % 58.72/58.75 [31]~P3(x313,x311)+P3(x311,x312)+~P3(x313,x312) % 58.72/58.75 [32]~P8(x323,x321)+P8(x321,x322)+~P8(x323,x322) % 58.72/58.75 [33]~P9(x333,x331)+P9(x331,x332)+~P9(x333,x332) % 58.72/58.75 [34]~P10(x343,x341)+P10(x341,x342)+~P10(x343,x342) % 58.72/58.75 [35]~P7(x353,x351)+P7(x351,x352)+~P7(x353,x352) % 58.72/58.75 [36]~P2(x363,x361)+P2(x361,x362)+~P2(x363,x362) % 58.72/58.75 [37]~P4(x373,x371)+P4(x371,x372)+~P4(x373,x372) % 58.72/58.75 [38]~P5(x383,x381)+P5(x381,x382)+~P5(x383,x382) % 58.72/58.75 [39]~P6(x393,x391)+P6(x391,x392)+~P6(x393,x392) % 58.72/58.75 [43]~P3(x432,x434)+~P4(x431,x433)+P7(f25(x431,x432),f25(x433,x434)) % 58.72/58.75 [44]~P3(x442,x444)+~P10(x441,x443)+P2(f18(x441,x442),f18(x443,x444)) % 58.72/58.75 [45]~P8(x451,x453)+~P6(x452,x454)+P5(f19(x451,x452),f19(x453,x454)) % 58.72/58.75 [46]~P3(x461,x463)+~P2(x462,x464)+P6(f17(x461,x462),f17(x463,x464)) % 58.72/58.75 [48]P3(x481,x482)+P14(f25(a1,x481),x482)+~P12(f19(a6,f17(x481,x483)),f17(x482,x484)) % 58.72/58.75 [49]P3(x491,x492)+~P12(f19(a6,f17(x491,x493)),f17(x492,x494))+~P2(f18(f23(x493),x491),f26(a7)) % 58.72/58.75 [50]P14(f25(a1,x501),x502)+P13(f18(f23(x503),x502),f18(f23(x504),x502))+~P12(f19(a6,f17(x501,x503)),f17(x502,x504)) % 58.72/58.75 [51]P2(x511,x512)+~P12(f19(a6,f17(x513,x512)),f17(x514,x515))+~P12(f19(a6,f17(x516,x511)),f17(x514,x515)) % 58.72/58.75 [40]~P12(x403,x404)+P12(x401,x402)+~P5(x403,x401)+~P6(x404,x402) % 58.72/58.75 [41]~P13(x413,x414)+P13(x411,x412)+~P2(x413,x411)+~P2(x414,x412) % 58.72/58.75 [42]~P14(x424,x423)+P14(x421,x422)+~P3(x423,x422)+~P7(x424,x421) % 58.72/58.75 [47]~P11(x476,x474,x475)+P11(x471,x472,x473)+~P10(x474,x472)+~P10(x475,x473)+~P4(x476,x471) % 58.72/58.75 %EqnAxiom % 58.72/58.75 % 58.72/58.75 %------------------------------------------- % 58.72/58.76 cnf(166,plain, % 58.72/58.76 (P2(a10,f21(a4))), % 58.72/58.76 inference(scs_inference,[],[15,8,36])). % 58.72/58.76 cnf(2304,plain, % 58.72/58.76 (P5(f19(f20(a5),f17(f16(a14),f21(a14))),f19(a6,f17(a15,a2)))), % 58.72/58.76 inference(scs_inference,[],[2,14,17,24,26,27,28,29,45])). % 58.72/58.76 cnf(2306,plain, % 58.72/58.76 (P6(f17(f16(a4),a2),f17(a8,a3))), % 58.72/58.76 inference(scs_inference,[],[2,14,17,12,24,26,27,28,29,45,46])). % 58.72/58.76 cnf(2340,plain, % 58.72/58.76 (P2(f22(a10),f22(f21(a4)))), % 58.72/58.76 inference(scs_inference,[],[166,28])). % 58.72/58.76 cnf(2348,plain, % 58.72/58.76 (~P5(f19(a6,f17(a15,a2)),f19(a6,f17(f16(a14),f21(a14))))), % 58.72/58.76 inference(scs_inference,[],[2306,22,4,166,15,11,20,28,26,29,45,40])). % 58.72/58.76 cnf(2364,plain, % 58.72/58.76 ($false), % 58.72/58.76 inference(scs_inference,[],[2340,2348,2304,14,11,28,26,29,45,38]), % 58.72/58.76 ['proof']). % 58.72/58.77 % SZS output end Proof % 58.72/58.77 % Total time :58.140000s %------------------------------------------------------------------------------