%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN621-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 : n019.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:08 EDT 2024 % Result : Unsatisfiable 58.54s 58.66s % Output : CNFRefutation 58.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN621-1 : TPTP v8.2.0. Released v2.5.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n019.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:38:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 58.54/58.65 %------------------------------------------- % 58.54/58.65 % File :CSE---1.7 % 58.54/58.65 % Problem :theBenchmark % 58.54/58.65 % Transform :cnf % 58.54/58.65 % Format :tptp:raw % 58.54/58.65 % Command :java -jar mcs_scs.jar %d %s % 58.54/58.65 % 58.54/58.65 % Result :Theorem 58.030000s % 58.54/58.65 % Output :CNFRefutation 58.030000s % 58.54/58.65 %------------------------------------------- % 58.54/58.65 %-------------------------------------------------------------------------- % 58.54/58.66 % File : SYN621-1 : TPTP v8.2.0. Released v2.5.0. % 58.54/58.66 % Domain : Syntactic % 58.54/58.66 % Problem : Harrison problem 3998 % 58.54/58.66 % Version : Especial. % 58.54/58.66 % English : % 58.54/58.66 % 58.54/58.66 % Refs : [Har01] Email to G. Sutcliffe % 58.54/58.66 % Source : [Har01] % 58.54/58.66 % Names : % 58.54/58.66 % 58.54/58.66 % Status : Unsatisfiable % 58.54/58.66 % Rating : 0.00 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.07 v4.1.0, 0.12 v4.0.1, 0.00 v2.5.0 % 58.54/58.66 % Syntax : Number of clauses : 34 ( 8 unt; 3 nHn; 25 RR) % 58.54/58.66 % Number of literals : 82 ( 0 equ; 47 neg) % 58.54/58.66 % Maximal clause size : 5 ( 2 avg) % 58.54/58.66 % Maximal term depth : 6 ( 1 avg) % 58.54/58.66 % Number of predicates : 8 ( 8 usr; 0 prp; 2-2 aty) % 58.54/58.66 % Number of functors : 19 ( 19 usr; 6 con; 0-4 aty) % 58.54/58.66 % Number of variables : 95 ( 1 sgn) % 58.54/58.66 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.54/58.66 % 58.54/58.66 % Comments : % 58.54/58.66 %-------------------------------------------------------------------------- % 58.54/58.66 cnf(p10_1,negated_conjecture, % 58.54/58.66 p10(X0,X0) ). % 58.54/58.66 % 58.54/58.66 cnf(p8_2,negated_conjecture, % 58.54/58.66 p8(X78,X78) ). % 58.54/58.66 % 58.54/58.66 cnf(p7_3,negated_conjecture, % 58.54/58.66 p7(X71,X71) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_4,negated_conjecture, % 58.54/58.66 p4(X38,X38) ). % 58.54/58.66 % 58.54/58.66 cnf(p2_5,negated_conjecture, % 58.54/58.66 p2(X12,X12) ). % 58.54/58.66 % 58.54/58.66 cnf(p13_6,negated_conjecture, % 58.54/58.66 p13(X7,X7) ). % 58.54/58.66 % 58.54/58.66 cnf(not_p2_7,negated_conjecture, % 58.54/58.66 ~ p2(c23,f3(c24)) ). % 58.54/58.66 % 58.54/58.66 cnf(p13_8,negated_conjecture, % 58.54/58.66 ( p13(f14(X10),f14(X11)) % 58.54/58.66 | ~ p7(X10,X11) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_9,negated_conjecture, % 58.54/58.66 ( p4(f5(X59),f5(X60)) % 58.54/58.66 | ~ p4(X59,X60) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_10,negated_conjecture, % 58.54/58.66 ( p4(f16(X45),f16(X46)) % 58.54/58.66 | ~ p2(X45,X46) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p2_11,negated_conjecture, % 58.54/58.66 ( p2(f3(X24),f3(X25)) % 58.54/58.66 | ~ p2(X24,X25) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p2_12,negated_conjecture, % 58.54/58.66 ( p2(f18(X22),f18(X23)) % 58.54/58.66 | ~ p2(X22,X23) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p2_13,negated_conjecture, % 58.54/58.66 ( p2(f17(X20),f17(X21)) % 58.54/58.66 | ~ p2(X20,X21) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p10_14,negated_conjecture, % 58.54/58.66 ( p10(X1,X2) % 58.54/58.66 | ~ p10(X0,X1) % 58.54/58.66 | ~ p10(X0,X2) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p8_15,negated_conjecture, % 58.54/58.66 ( p8(X79,X80) % 58.54/58.66 | ~ p8(X78,X79) % 58.54/58.66 | ~ p8(X78,X80) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p7_16,negated_conjecture, % 58.54/58.66 ( p7(X72,X73) % 58.54/58.66 | ~ p7(X71,X72) % 58.54/58.66 | ~ p7(X71,X73) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_17,negated_conjecture, % 58.54/58.66 ( p4(X39,X40) % 58.54/58.66 | ~ p4(X38,X39) % 58.54/58.66 | ~ p4(X38,X40) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p21_18,negated_conjecture, % 58.54/58.66 ( p21(X30,X31) % 58.54/58.66 | ~ p21(X30,X32) % 58.54/58.66 | ~ p21(X32,X31) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p2_19,negated_conjecture, % 58.54/58.66 ( p2(X13,X14) % 58.54/58.66 | ~ p2(X12,X13) % 58.54/58.66 | ~ p2(X12,X14) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p13_20,negated_conjecture, % 58.54/58.66 ( p13(X8,X9) % 58.54/58.66 | ~ p13(X7,X8) % 58.54/58.66 | ~ p13(X7,X9) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p21_21,negated_conjecture, % 58.54/58.66 ( p21(X26,X27) % 58.54/58.66 | ~ p4(X28,X26) % 58.54/58.66 | ~ p4(X29,X27) % 58.54/58.66 | ~ p21(X28,X29) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p22_22,negated_conjecture, % 58.54/58.66 ( p22(X34,X35) % 58.54/58.66 | ~ p22(X37,X36) % 58.54/58.66 | ~ p4(X37,X34) % 58.54/58.66 | ~ p13(X36,X35) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p7_23,negated_conjecture, % 58.54/58.66 ( p7(f11(X74,X75),f11(X76,X77)) % 58.54/58.66 | ~ p10(X75,X77) % 58.54/58.66 | ~ p2(X74,X76) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p10_24,negated_conjecture, % 58.54/58.66 ( p10(f12(X3,X4),f12(X5,X6)) % 58.54/58.66 | ~ p2(X3,X5) % 58.54/58.66 | ~ p2(X4,X6) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_25,negated_conjecture, % 58.54/58.66 ( p4(f15(X41,X42),f15(X43,X44)) % 58.54/58.66 | ~ p4(X41,X43) % 58.54/58.66 | ~ p4(X42,X44) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_26,negated_conjecture, % 58.54/58.66 ( p4(f19(X47,X48),f19(X49,X50)) % 58.54/58.66 | ~ p4(X48,X50) % 58.54/58.66 | ~ p7(X47,X49) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_27,negated_conjecture, % 58.54/58.66 ( p4(f6(X61,X62),f6(X63,X64)) % 58.54/58.66 | ~ p4(X61,X63) % 58.54/58.66 | ~ p4(X62,X64) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p2_28,negated_conjecture, % 58.54/58.66 ( p2(X15,f3(c24)) % 58.54/58.66 | p22(f20(X17,X15,X18,X16),f14(f11(X17,f12(X15,X18)))) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_29,negated_conjecture, % 58.54/58.66 ( p4(f9(X65,X66,X67),f9(X68,X69,X70)) % 58.54/58.66 | ~ p7(X65,X68) % 58.54/58.66 | ~ p8(X66,X69) % 58.54/58.66 | ~ p4(X67,X70) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p4_30,negated_conjecture, % 58.54/58.66 ( p4(f20(X51,X52,X53,X54),f20(X55,X56,X57,X58)) % 58.54/58.66 | ~ p2(X53,X57) % 58.54/58.66 | ~ p4(X54,X58) % 58.54/58.66 | ~ p2(X51,X55) % 58.54/58.66 | ~ p2(X52,X56) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p21_31,negated_conjecture, % 58.54/58.66 ( p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f5(f6(c27,X33))) % 58.54/58.66 | ~ p22(X33,f14(f11(c25,f12(c23,c26)))) ) ). % 58.54/58.66 % 58.54/58.66 cnf(not_p21_32,negated_conjecture, % 58.54/58.66 ~ p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f15(f19(f11(c25,f12(c23,c26)),c27),f16(f3(f17(f18(c24)))))) ). % 58.54/58.66 % 58.54/58.66 cnf(p2_33,negated_conjecture, % 58.54/58.66 ( p2(X15,f3(c24)) % 58.54/58.66 | p21(f5(f6(X16,f20(X17,X15,X18,X16))),f5(f6(X16,X19))) % 58.54/58.66 | ~ p22(X19,f14(f11(X17,f12(X15,X18)))) ) ). % 58.54/58.66 % 58.54/58.66 cnf(p2_34,negated_conjecture, % 58.54/58.66 ( p2(X15,f3(c24)) % 58.54/58.66 | p21(f5(f6(X16,f20(X17,X15,X18,X16))),f15(f19(f11(X17,f12(X15,X18)),X16),f16(f3(f17(f18(c24)))))) ) ). % 58.54/58.66 % 58.54/58.66 %-------------------------------------------------------------------------- % 58.54/58.66 %------------------------------------------- % 58.54/58.66 % Proof found % 58.54/58.66 % SZS status Theorem for theBenchmark % 58.54/58.66 % SZS output start Proof % 58.54/58.66 %ClaNum:34(EqnAxiom:0) % 58.54/58.66 %VarNum:194(SingletonVarNum:95) % 58.54/58.66 %MaxLitNum:5 % 58.54/58.66 %MaxfuncDepth:5 % 58.54/58.66 %SharedTerms:21 % 58.54/58.66 %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 % 58.54/58.66 %singleGoalClaCount:8 % 58.54/58.66 [7]~P5(a1,f3(a2)) % 58.54/58.66 [8]~P7(f19(f18(a4,f17(f8(a5,f7(a1,a6)),a9,a4))),f14(f10(f8(a5,f7(a1,a6)),a4),f13(f3(f12(f11(a2)))))) % 58.54/58.66 [1]P1(x11,x11) % 58.54/58.66 [2]P2(x21,x21) % 58.54/58.66 [3]P3(x31,x31) % 58.54/58.66 [4]P4(x41,x41) % 58.54/58.66 [5]P5(x51,x51) % 58.54/58.66 [6]P6(x61,x61) % 58.54/58.66 [32]~P8(x321,f15(f8(a5,f7(a1,a6))))+P7(f19(f18(a4,f17(f8(a5,f7(a1,a6)),a9,a4))),f19(f18(a4,x321))) % 58.54/58.66 [9]~P4(x91,x92)+P4(f19(x91),f19(x92)) % 58.54/58.66 [10]~P5(x101,x102)+P4(f13(x101),f13(x102)) % 58.54/58.66 [11]~P5(x111,x112)+P5(f3(x111),f3(x112)) % 58.54/58.66 [12]~P5(x121,x122)+P5(f11(x121),f11(x122)) % 58.54/58.66 [13]~P5(x131,x132)+P5(f12(x131),f12(x132)) % 58.54/58.66 [14]~P3(x141,x142)+P6(f15(x141),f15(x142)) % 58.54/58.66 [30]P5(x301,f3(a2))+P8(f16(x302,x301,x303,x304),f15(f8(x302,f7(x301,x303)))) % 58.54/58.66 [34]P5(x341,f3(a2))+P7(f19(f18(x342,f16(x343,x341,x344,x342))),f14(f10(f8(x343,f7(x341,x344)),x342),f13(f3(f12(f11(a2)))))) % 58.54/58.66 [15]~P1(x153,x151)+P1(x151,x152)+~P1(x153,x152) % 58.54/58.66 [16]~P2(x163,x161)+P2(x161,x162)+~P2(x163,x162) % 58.54/58.66 [17]~P3(x173,x171)+P3(x171,x172)+~P3(x173,x172) % 58.54/58.66 [18]~P4(x183,x181)+P4(x181,x182)+~P4(x183,x182) % 58.54/58.66 [19]~P5(x193,x191)+P5(x191,x192)+~P5(x193,x192) % 58.54/58.66 [20]~P6(x203,x201)+P6(x201,x202)+~P6(x203,x202) % 58.54/58.66 [21]~P7(x211,x213)+P7(x211,x212)+~P7(x213,x212) % 58.54/58.66 [24]~P5(x242,x244)+~P5(x241,x243)+P1(f7(x241,x242),f7(x243,x244)) % 58.54/58.66 [25]~P1(x252,x254)+~P5(x251,x253)+P3(f8(x251,x252),f8(x253,x254)) % 58.54/58.66 [26]~P4(x262,x264)+~P4(x261,x263)+P4(f14(x261,x262),f14(x263,x264)) % 58.54/58.66 [27]~P3(x271,x273)+~P4(x272,x274)+P4(f10(x271,x272),f10(x273,x274)) % 58.54/58.66 [28]~P4(x282,x284)+~P4(x281,x283)+P4(f18(x281,x282),f18(x283,x284)) % 58.54/58.66 [33]P5(x331,f3(a2))+~P8(x335,f15(f8(x333,f7(x331,x334))))+P7(f19(f18(x332,f16(x333,x331,x334,x332))),f19(f18(x332,x335))) % 58.54/58.66 [22]~P7(x224,x223)+P7(x221,x222)+~P4(x223,x222)+~P4(x224,x221) % 58.54/58.66 [23]~P8(x233,x234)+P8(x231,x232)+~P4(x233,x231)+~P6(x234,x232) % 58.54/58.66 [29]~P2(x292,x295)+~P3(x291,x294)+~P4(x293,x296)+P4(f17(x291,x292,x293),f17(x294,x295,x296)) % 58.54/58.66 [31]~P4(x314,x318)+~P5(x313,x317)+~P5(x312,x316)+~P5(x311,x315)+P4(f16(x311,x312,x313,x314),f16(x315,x316,x317,x318)) % 58.54/58.66 %EqnAxiom % 58.54/58.66 % 58.54/58.66 %------------------------------------------- % 58.54/58.67 cnf(49,plain, % 58.54/58.67 (P7(f19(f18(a4,f17(f8(a5,f7(a1,a6)),a9,a4))),f19(f18(a4,f16(a5,a1,a6,x491))))), % 58.54/58.67 inference(scs_inference,[],[7,32,30])). % 58.54/58.67 cnf(53,plain, % 58.54/58.67 (P1(f7(x531,x532),f7(x531,f3(a2)))+P7(f19(f18(x533,f16(x534,x532,x535,x533))),f14(f10(f8(x534,f7(x532,x535)),x533),f13(f3(f12(f11(a2))))))), % 58.54/58.67 inference(scs_inference,[],[5,34,24])). % 58.54/58.67 cnf(55,plain, % 58.54/58.67 (P1(f7(x551,a1),f7(x551,f3(a2)))), % 58.54/58.67 inference(scs_inference,[],[49,8,53,21])). % 58.54/58.67 cnf(57,plain, % 58.54/58.67 (P1(f7(x571,f3(a2)),f7(x571,a1))), % 58.54/58.67 inference(scs_inference,[],[55,1,15])). % 58.54/58.67 cnf(136,plain, % 58.54/58.67 (P3(f8(f12(x1361),f7(x1362,f3(a2))),f8(f12(x1361),f7(x1362,a1)))), % 58.54/58.67 inference(scs_inference,[],[5,57,13,25])). % 58.54/58.67 cnf(2606,plain, % 58.54/58.67 ($false), % 58.54/58.67 inference(scs_inference,[],[8,49,55,7,136,4,5,14,34,30,25,27,28,21]), % 58.54/58.67 ['proof']). % 58.54/58.67 % SZS output end Proof % 58.54/58.67 % Total time :58.030000s %------------------------------------------------------------------------------