%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN619-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 : n027.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:07 EDT 2024 % Result : Unsatisfiable 59.08s 59.19s % Output : CNFRefutation 59.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN619-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n027.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 23:36:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 59.08/59.18 %------------------------------------------- % 59.08/59.18 % File :CSE---1.7 % 59.08/59.18 % Problem :theBenchmark % 59.08/59.18 % Transform :cnf % 59.08/59.18 % Format :tptp:raw % 59.08/59.18 % Command :java -jar mcs_scs.jar %d %s % 59.08/59.18 % 59.08/59.18 % Result :Theorem 58.580000s % 59.08/59.18 % Output :CNFRefutation 58.580000s % 59.08/59.18 %------------------------------------------- % 59.08/59.19 %-------------------------------------------------------------------------- % 59.08/59.19 % File : SYN619-1 : TPTP v8.2.0. Released v2.5.0. % 59.08/59.19 % Domain : Syntactic % 59.08/59.19 % Problem : Harrison problem 3992 % 59.08/59.19 % Version : Especial. % 59.08/59.19 % English : % 59.08/59.19 % 59.08/59.19 % Refs : [Har01] Email to G. Sutcliffe % 59.08/59.19 % Source : [Har01] % 59.08/59.19 % Names : % 59.08/59.19 % 59.08/59.19 % Status : Unsatisfiable % 59.08/59.19 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v2.5.0 % 59.08/59.19 % Syntax : Number of clauses : 34 ( 8 unt; 4 nHn; 28 RR) % 59.08/59.19 % Number of literals : 78 ( 0 equ; 42 neg) % 59.08/59.19 % Maximal clause size : 4 ( 2 avg) % 59.08/59.19 % Maximal term depth : 5 ( 1 avg) % 59.08/59.19 % Number of predicates : 7 ( 7 usr; 0 prp; 2-2 aty) % 59.08/59.19 % Number of functors : 17 ( 17 usr; 7 con; 0-2 aty) % 59.08/59.19 % Number of variables : 76 ( 5 sgn) % 59.08/59.19 % SPC : CNF_UNS_RFO_NEQ_NHN % 59.08/59.19 % 59.08/59.19 % Comments : % 59.08/59.19 %-------------------------------------------------------------------------- % 59.08/59.19 cnf(p10_1,negated_conjecture, % 59.08/59.19 p10(X0,X0) ). % 59.08/59.19 % 59.08/59.19 cnf(p8_2,negated_conjecture, % 59.08/59.19 p8(X51,X51) ). % 59.08/59.19 % 59.08/59.19 cnf(p5_3,negated_conjecture, % 59.08/59.19 p5(X46,X46) ). % 59.08/59.19 % 59.08/59.19 cnf(p4_4,negated_conjecture, % 59.08/59.19 p4(X39,X39) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_5,negated_conjecture, % 59.08/59.19 p2(X18,X18) ). % 59.08/59.19 % 59.08/59.19 cnf(p17_6,negated_conjecture, % 59.08/59.19 p17(X9,X9) ). % 59.08/59.19 % 59.08/59.19 cnf(p18_7,negated_conjecture, % 59.08/59.19 p18(c24,f6(c25)) ). % 59.08/59.19 % 59.08/59.19 cnf(not_p18_8,negated_conjecture, % 59.08/59.19 ~ p18(c24,f6(f7(c22,c23))) ). % 59.08/59.19 % 59.08/59.19 cnf(p17_9,negated_conjecture, % 59.08/59.19 ( p17(X10,X11) % 59.08/59.19 | ~ p17(f3(X10),X11) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p5_10,negated_conjecture, % 59.08/59.19 ( p5(f6(X49),f6(X50)) % 59.08/59.19 | ~ p4(X49,X50) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p10_11,negated_conjecture, % 59.08/59.19 ( p10(f12(X3),f12(X4)) % 59.08/59.19 | ~ p4(X3,X4) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_12,negated_conjecture, % 59.08/59.19 ( p2(f11(X25),f11(X26)) % 59.08/59.19 | ~ p10(X25,X26) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_13,negated_conjecture, % 59.08/59.19 ( p2(f14(X31),f14(X32)) % 59.08/59.19 | ~ p8(X31,X32) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_14,negated_conjecture, % 59.08/59.19 ( p2(f15(X33),f15(X34)) % 59.08/59.19 | ~ p8(X33,X34) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_15,negated_conjecture, % 59.08/59.19 ( p2(f16(X35),f16(X36)) % 59.08/59.19 | ~ p8(X35,X36) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_16,negated_conjecture, % 59.08/59.19 ( p2(f3(X37),f3(X38)) % 59.08/59.19 | ~ p2(X37,X38) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p10_17,negated_conjecture, % 59.08/59.19 ( p10(X1,X2) % 59.08/59.19 | ~ p10(X0,X1) % 59.08/59.19 | ~ p10(X0,X2) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p8_18,negated_conjecture, % 59.08/59.19 ( p8(X52,X53) % 59.08/59.19 | ~ p8(X51,X52) % 59.08/59.19 | ~ p8(X51,X53) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p5_19,negated_conjecture, % 59.08/59.19 ( p5(X47,X48) % 59.08/59.19 | ~ p5(X46,X47) % 59.08/59.19 | ~ p5(X46,X48) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p4_20,negated_conjecture, % 59.08/59.19 ( p4(X40,X41) % 59.08/59.19 | ~ p4(X39,X40) % 59.08/59.19 | ~ p4(X39,X41) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_21,negated_conjecture, % 59.08/59.19 ( p2(X19,X20) % 59.08/59.19 | ~ p2(X18,X19) % 59.08/59.19 | ~ p2(X18,X20) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_22,negated_conjecture, % 59.08/59.19 ( p2(X23,X24) % 59.08/59.19 | ~ p2(f13(X21,X23),f13(X22,X24)) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_23,negated_conjecture, % 59.08/59.19 ( p2(X21,X22) % 59.08/59.19 | ~ p2(f13(X21,X23),f13(X22,X24)) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p18_24,negated_conjecture, % 59.08/59.19 ( p18(X12,f6(c19)) % 59.08/59.19 | p2(f14(X12),c20) % 59.08/59.19 | ~ p18(X12,f6(c25)) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p17_25,negated_conjecture, % 59.08/59.19 ( p17(X5,X6) % 59.08/59.19 | ~ p2(X7,X5) % 59.08/59.19 | ~ p2(X8,X6) % 59.08/59.19 | ~ p17(X7,X8) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p18_26,negated_conjecture, % 59.08/59.19 ( p18(X13,X14) % 59.08/59.19 | ~ p5(X16,X14) % 59.08/59.19 | ~ p8(X15,X13) % 59.08/59.19 | ~ p18(X15,X16) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p18_27,negated_conjecture, % 59.08/59.19 ( p18(X12,f6(c19)) % 59.08/59.19 | p17(f3(c21),f15(X12)) % 59.08/59.19 | ~ p18(X12,f6(c25)) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p8_28,negated_conjecture, % 59.08/59.19 ( p8(f9(X54,X55),f9(X56,X57)) % 59.08/59.19 | ~ p2(X55,X57) % 59.08/59.19 | ~ p2(X54,X56) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_29,negated_conjecture, % 59.08/59.19 ( p2(f13(X27,X28),f13(X29,X30)) % 59.08/59.19 | ~ p2(X27,X29) % 59.08/59.19 | ~ p2(X28,X30) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p2_30,negated_conjecture, % 59.08/59.19 ( p2(f13(X21,X23),f13(X22,X24)) % 59.08/59.19 | ~ p2(X21,X22) % 59.08/59.19 | ~ p2(X23,X24) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p4_31,negated_conjecture, % 59.08/59.19 ( p4(f7(X42,X43),f7(X44,X45)) % 59.08/59.19 | ~ p2(X42,X44) % 59.08/59.19 | ~ p4(X43,X45) ) ). % 59.08/59.19 % 59.08/59.19 cnf(not_p2_32,negated_conjecture, % 59.08/59.19 ( ~ p2(X59,c20) % 59.08/59.19 | ~ p17(c21,X58) % 59.08/59.19 | ~ p8(c24,f9(f13(X59,X58),X60)) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p18_33,negated_conjecture, % 59.08/59.19 ( p18(X12,f6(c19)) % 59.08/59.19 | p8(X12,f9(f13(f14(X12),f15(X12)),f16(X12))) % 59.08/59.19 | ~ p18(X12,f6(c25)) ) ). % 59.08/59.19 % 59.08/59.19 cnf(p18_34,negated_conjecture, % 59.08/59.19 ( p18(X17,f6(f7(c22,c23))) % 59.08/59.19 | p8(X17,f9(f13(c20,c21),f11(f12(f7(c22,c23))))) % 59.08/59.19 | ~ p18(X17,f6(c19)) ) ). % 59.08/59.19 % 59.08/59.19 %-------------------------------------------------------------------------- % 59.08/59.19 %------------------------------------------- % 59.08/59.19 % Proof found % 59.08/59.19 % SZS status Theorem for theBenchmark % 59.08/59.19 % SZS output start Proof % 59.08/59.19 %ClaNum:34(EqnAxiom:0) % 59.08/59.19 %VarNum:146(SingletonVarNum:72) % 59.08/59.19 %MaxLitNum:4 % 59.08/59.19 %MaxfuncDepth:4 % 59.08/59.20 %SharedTerms:18 % 59.08/59.20 %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 29 30 31 32 33 34 % 59.08/59.20 %singleGoalClaCount:8 % 59.08/59.20 [7]P7(a1,f8(a7)) % 59.08/59.20 [8]~P7(a1,f8(f16(a2,a6))) % 59.08/59.20 [1]P1(x11,x11) % 59.08/59.20 [2]P2(x21,x21) % 59.08/59.20 [3]P3(x31,x31) % 59.08/59.20 [4]P4(x41,x41) % 59.08/59.20 [5]P5(x51,x51) % 59.08/59.20 [6]P6(x61,x61) % 59.08/59.20 [9]P6(x91,x92)+~P6(f9(x91),x92) % 59.08/59.20 [10]~P4(x101,x102)+P1(f10(x101),f10(x102)) % 59.08/59.20 [11]~P4(x111,x112)+P3(f8(x111),f8(x112)) % 59.08/59.20 [12]~P5(x121,x122)+P5(f9(x121),f9(x122)) % 59.08/59.20 [13]~P1(x131,x132)+P5(f11(x131),f11(x132)) % 59.08/59.20 [14]~P2(x141,x142)+P5(f12(x141),f12(x142)) % 59.08/59.20 [15]~P2(x151,x152)+P5(f14(x151),f14(x152)) % 59.08/59.20 [16]~P2(x161,x162)+P5(f15(x161),f15(x162)) % 59.08/59.20 [30]P5(x301,x302)+~P5(f13(x303,x301),f13(x304,x302)) % 59.08/59.20 [31]P5(x311,x312)+~P5(f13(x311,x313),f13(x312,x314)) % 59.08/59.20 [22]~P7(x221,f8(a7))+P7(x221,f8(a3))+P5(f12(x221),a4) % 59.08/59.20 [23]P6(f9(a5),f14(x231))+~P7(x231,f8(a7))+P7(x231,f8(a3)) % 59.08/59.20 [33]~P7(x331,f8(a7))+P7(x331,f8(a3))+P2(x331,f17(f13(f12(x331),f14(x331)),f15(x331))) % 59.08/59.20 [34]~P7(x341,f8(a3))+P7(x341,f8(f16(a2,a6)))+P2(x341,f17(f13(a4,a5),f11(f10(f16(a2,a6))))) % 59.08/59.20 [17]~P1(x173,x171)+P1(x171,x172)+~P1(x173,x172) % 59.08/59.20 [18]~P2(x183,x181)+P2(x181,x182)+~P2(x183,x182) % 59.08/59.20 [19]~P3(x193,x191)+P3(x191,x192)+~P3(x193,x192) % 59.08/59.20 [20]~P4(x203,x201)+P4(x201,x202)+~P4(x203,x202) % 59.08/59.20 [21]~P5(x213,x211)+P5(x211,x212)+~P5(x213,x212) % 59.08/59.20 [32]~P5(x321,a4)+~P6(a5,x322)+~P2(a1,f17(f13(x321,x322),x323)) % 59.08/59.20 [26]~P5(x262,x264)+~P5(x261,x263)+P2(f17(x261,x262),f17(x263,x264)) % 59.08/59.20 [27]~P4(x272,x274)+~P5(x271,x273)+P4(f16(x271,x272),f16(x273,x274)) % 59.08/59.20 [29]~P5(x292,x294)+~P5(x291,x293)+P5(f13(x291,x292),f13(x293,x294)) % 59.08/59.20 [24]~P6(x244,x243)+P6(x241,x242)+~P5(x243,x242)+~P5(x244,x241) % 59.08/59.20 [25]~P7(x253,x254)+P7(x251,x252)+~P2(x253,x251)+~P3(x254,x252) % 59.08/59.20 %EqnAxiom % 59.08/59.20 % 59.08/59.20 %------------------------------------------- % 59.19/59.20 cnf(35,plain, % 59.19/59.20 (P6(x351,f9(x351))), % 59.19/59.20 inference(scs_inference,[],[6,9])). % 59.19/59.20 cnf(38,plain, % 59.19/59.20 (P7(a1,f8(a3))+P6(f9(a5),f14(a1))), % 59.19/59.20 inference(scs_inference,[],[6,7,9,23])). % 59.19/59.20 cnf(49,plain, % 59.19/59.20 (P5(f12(a1),f12(f17(f13(f12(a1),f14(a1)),f15(a1))))+P7(a1,f8(a3))), % 59.19/59.20 inference(scs_inference,[],[7,14,33])). % 59.19/59.20 cnf(51,plain, % 59.19/59.20 (P5(f15(a1),f15(f17(f13(f12(a1),f14(a1)),f15(a1))))+P7(a1,f8(a3))), % 59.19/59.20 inference(scs_inference,[],[7,16,33])). % 59.19/59.20 cnf(52,plain, % 59.19/59.20 (P6(f9(a5),f14(a1))+P2(a1,f17(f13(a4,a5),f11(f10(f16(a2,a6)))))), % 59.19/59.20 inference(scs_inference,[],[8,38,34])). % 59.19/59.20 cnf(55,plain, % 59.19/59.20 (P5(f12(a1),f12(f17(f13(f12(a1),f14(a1)),f15(a1))))+P2(a1,f17(f13(a4,a5),f11(f10(f16(a2,a6)))))), % 59.19/59.20 inference(scs_inference,[],[8,49,34])). % 59.19/59.20 cnf(56,plain, % 59.19/59.20 (P5(f15(a1),f15(f17(f13(f12(a1),f14(a1)),f15(a1))))+P2(a1,f17(f13(a4,a5),f11(f10(f16(a2,a6)))))), % 59.19/59.20 inference(scs_inference,[],[8,51,34])). % 59.19/59.20 cnf(57,plain, % 59.19/59.20 (P6(a5,f14(a1))+P2(a1,f17(f13(a4,a5),f11(f10(f16(a2,a6)))))), % 59.19/59.20 inference(scs_inference,[],[52,9])). % 59.19/59.20 cnf(58,plain, % 59.19/59.20 (P6(a5,f14(a1))), % 59.19/59.20 inference(scs_inference,[],[5,6,57,32])). % 59.19/59.20 cnf(59,plain, % 59.19/59.20 (P5(f12(a1),f12(f17(f13(f12(a1),f14(a1)),f15(a1))))), % 59.19/59.20 inference(scs_inference,[],[5,6,55,32])). % 59.19/59.20 cnf(60,plain, % 59.19/59.20 (P5(f12(f17(f13(f12(a1),f14(a1)),f15(a1))),f12(a1))), % 59.19/59.20 inference(scs_inference,[],[59,5,21])). % 59.19/59.20 cnf(63,plain, % 59.19/59.20 (P5(f15(a1),f15(f17(f13(f12(a1),f14(a1)),f15(a1))))), % 59.19/59.20 inference(scs_inference,[],[5,6,56,32])). % 59.19/59.20 cnf(64,plain, % 59.19/59.20 (P2(f17(f13(f12(a1),f14(a1)),f15(a1)),a1)+P7(a1,f8(a3))), % 59.19/59.20 inference(scs_inference,[],[2,7,18,33])). % 59.19/59.20 cnf(69,plain, % 59.19/59.20 (P2(f17(f13(f12(a1),f14(a1)),f15(a1)),a1)+P2(a1,f17(f13(a4,a5),f11(f10(f16(a2,a6)))))), % 59.19/59.20 inference(scs_inference,[],[8,64,34])). % 59.19/59.20 cnf(70,plain, % 59.19/59.20 (P5(f15(f17(f13(f12(a1),f14(a1)),f15(a1))),f15(a1))), % 59.19/59.20 inference(scs_inference,[],[63,5,21])). % 59.19/59.20 cnf(77,plain, % 59.19/59.20 (P2(f17(f13(f12(a1),f14(a1)),f15(a1)),a1)), % 59.19/59.20 inference(scs_inference,[],[5,6,69,32])). % 59.19/59.20 cnf(78,plain, % 59.19/59.20 (P2(a1,f17(f13(f12(a1),f14(a1)),f15(a1)))), % 59.19/59.20 inference(scs_inference,[],[77,2,18])). % 59.19/59.20 cnf(81,plain, % 59.19/59.20 (~P5(f12(a1),a4)), % 59.19/59.20 inference(scs_inference,[],[77,58,2,18,32])). % 59.19/59.20 cnf(90,plain, % 59.19/59.20 (P7(a1,f8(a3))), % 59.19/59.20 inference(scs_inference,[],[6,70,77,58,7,5,2,3,8,18,32,25,24,22])). % 59.19/59.20 cnf(140,plain, % 59.19/59.20 (~P5(a4,f12(a1))), % 59.19/59.20 inference(scs_inference,[],[81,5,21])). % 59.19/59.20 cnf(143,plain, % 59.19/59.20 (~P5(f12(f17(f13(f12(a1),f14(a1)),f15(a1))),a4)), % 59.19/59.20 inference(scs_inference,[],[140,60,21])). % 59.19/59.20 cnf(167,plain, % 59.19/59.20 (~P5(a4,f12(f17(f13(f12(a1),f14(a1)),f15(a1))))), % 59.19/59.20 inference(scs_inference,[],[143,5,21])). % 59.19/59.20 cnf(191,plain, % 59.19/59.20 (P5(f9(f14(a1)),f9(f14(f17(f13(f12(a1),f14(a1)),f15(a1)))))), % 59.19/59.20 inference(scs_inference,[],[78,15,12])). % 59.19/59.20 cnf(299,plain, % 59.19/59.20 (~P5(f13(f13(x2991,f12(a1)),x2992),f13(f13(x2993,a4),x2994))), % 59.19/59.20 inference(scs_inference,[],[81,30,31])). % 59.19/59.20 cnf(300,plain, % 59.19/59.20 (~P5(f13(x3001,f12(a1)),f13(x3002,a4))), % 59.19/59.20 inference(scs_inference,[],[70,299,29])). % 59.19/59.20 cnf(1898,plain, % 59.19/59.20 (~P5(f9(x18981),x18982)+P6(x18981,x18982)), % 59.19/59.20 inference(scs_inference,[],[5,35,24])). % 59.19/59.20 cnf(2006,plain, % 59.19/59.20 (P2(a1,f17(f13(a4,a5),f11(f10(f16(a2,a6)))))), % 59.19/59.20 inference(scs_inference,[],[191,167,300,90,8,78,70,1898,12,15,30,31,34])). % 59.19/59.20 cnf(2055,plain, % 59.19/59.20 ($false), % 59.19/59.20 inference(scs_inference,[],[6,2006,5,32]), % 59.19/59.20 ['proof']). % 59.19/59.21 % SZS output end Proof % 59.19/59.21 % Total time :58.580000s %------------------------------------------------------------------------------