%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN609-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:06 EDT 2024 % Result : Unsatisfiable 116.76s 116.85s % Output : CNFRefutation 116.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SYN609-1 : TPTP v8.2.0. Released v2.5.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 23:29:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 116.76/116.84 %------------------------------------------- % 116.76/116.84 % File :CSE---1.7 % 116.76/116.84 % Problem :theBenchmark % 116.76/116.84 % Transform :cnf % 116.76/116.84 % Format :tptp:raw % 116.76/116.84 % Command :java -jar mcs_scs.jar %d %s % 116.76/116.84 % 116.76/116.84 % Result :Theorem 116.200000s % 116.76/116.84 % Output :CNFRefutation 116.200000s % 116.76/116.84 %------------------------------------------- % 116.76/116.85 %-------------------------------------------------------------------------- % 116.76/116.85 % File : SYN609-1 : TPTP v8.2.0. Released v2.5.0. % 116.76/116.85 % Domain : Syntactic % 116.76/116.85 % Problem : Harrison problem 3829 % 116.76/116.85 % Version : Especial. % 116.76/116.85 % English : % 116.76/116.85 % 116.76/116.85 % Refs : [Har01] Email to G. Sutcliffe % 116.76/116.85 % Source : [Har01] % 116.76/116.85 % Names : % 116.76/116.85 % 116.76/116.85 % Status : Unsatisfiable % 116.76/116.85 % Rating : 0.00 v7.5.0, 0.33 v7.4.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.00 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.38 v5.4.0, 0.40 v5.2.0, 0.30 v5.1.0, 0.27 v5.0.0, 0.43 v4.1.0, 0.25 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.50 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0 % 116.76/116.85 % Syntax : Number of clauses : 30 ( 12 unt; 1 nHn; 27 RR) % 116.76/116.85 % Number of literals : 62 ( 0 equ; 34 neg) % 116.76/116.85 % Maximal clause size : 4 ( 2 avg) % 116.76/116.85 % Maximal term depth : 8 ( 2 avg) % 116.76/116.85 % Number of predicates : 6 ( 6 usr; 0 prp; 1-2 aty) % 116.76/116.85 % Number of functors : 15 ( 15 usr; 4 con; 0-2 aty) % 116.76/116.85 % Number of variables : 54 ( 1 sgn) % 116.76/116.85 % SPC : CNF_UNS_RFO_NEQ_NHN % 116.76/116.85 % 116.76/116.85 % Comments : % 116.76/116.85 %-------------------------------------------------------------------------- % 116.76/116.85 cnf(c21_is_not_p16_1,negated_conjecture, % 116.76/116.85 ~ p16(c21) ). % 116.76/116.85 % 116.76/116.85 cnf(p2_2,negated_conjecture, % 116.76/116.85 p2(X11,X11) ). % 116.76/116.85 % 116.76/116.85 cnf(p5_3,negated_conjecture, % 116.76/116.85 p5(X43,X43) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_4,negated_conjecture, % 116.76/116.85 p3(X18,X18) ). % 116.76/116.85 % 116.76/116.85 cnf(not_p5_5,negated_conjecture, % 116.76/116.85 ~ p5(c21,f7(c20)) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_6,negated_conjecture, % 116.76/116.85 p3(f12(c22,c21),c22) ). % 116.76/116.85 % 116.76/116.85 cnf(not_p3_7,negated_conjecture, % 116.76/116.85 ~ p3(c19,f4(f6(f7(c20)))) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_8,negated_conjecture, % 116.76/116.85 p3(f12(f15(c22),c21),f15(c22)) ). % 116.76/116.85 % 116.76/116.85 cnf(p16_9,negated_conjecture, % 116.76/116.85 ( p16(X0) % 116.76/116.85 | ~ p16(X1) % 116.76/116.85 | ~ p5(X1,X0) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p5_10,negated_conjecture, % 116.76/116.85 ( p5(f8(X48),f8(X49)) % 116.76/116.85 | ~ p5(X48,X49) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p2_11,negated_conjecture, % 116.76/116.85 ( p2(f6(X14),f6(X15)) % 116.76/116.85 | ~ p5(X14,X15) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p2_12,negated_conjecture, % 116.76/116.85 ( p2(f9(X16),f9(X17)) % 116.76/116.85 | ~ p3(X16,X17) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_13,negated_conjecture, % 116.76/116.85 ( p3(f13(X33),f13(X34)) % 116.76/116.85 | ~ p5(X33,X34) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_14,negated_conjecture, % 116.76/116.85 ( p3(f15(X39),f15(X40)) % 116.76/116.85 | ~ p3(X39,X40) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_15,negated_conjecture, % 116.76/116.85 ( p3(f4(X41),f4(X42)) % 116.76/116.85 | ~ p2(X41,X42) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p5_16,negated_conjecture, % 116.76/116.85 ( p5(f7(X46),f7(X47)) % 116.76/116.85 | ~ p5(X46,X47) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p2_17,negated_conjecture, % 116.76/116.85 ( p2(X12,X13) % 116.76/116.85 | ~ p2(X11,X12) % 116.76/116.85 | ~ p2(X11,X13) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p5_18,negated_conjecture, % 116.76/116.85 ( p5(X44,X45) % 116.76/116.85 | ~ p5(X43,X44) % 116.76/116.85 | ~ p5(X43,X45) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_19,negated_conjecture, % 116.76/116.85 ( p3(X19,X20) % 116.76/116.85 | ~ p3(X18,X19) % 116.76/116.85 | ~ p3(X18,X20) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p17_20,negated_conjecture, % 116.76/116.85 ( p17(X2,X3) % 116.76/116.85 | ~ p2(X4,X2) % 116.76/116.85 | ~ p2(X5,X3) % 116.76/116.85 | ~ p17(X4,X5) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p18_21,negated_conjecture, % 116.76/116.85 ( p18(X7,X8) % 116.76/116.85 | ~ p5(X9,X7) % 116.76/116.85 | ~ p5(X10,X8) % 116.76/116.85 | ~ p18(X9,X10) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_22,negated_conjecture, % 116.76/116.85 p3(f12(f4(f6(f7(f8(c20)))),c21),f4(f6(f7(f8(c20))))) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_23,negated_conjecture, % 116.76/116.85 ( p3(f14(X35,X36),f14(X37,X38)) % 116.76/116.85 | ~ p3(X35,X37) % 116.76/116.85 | ~ p3(X36,X38) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_24,negated_conjecture, % 116.76/116.85 ( p3(f10(X21,X22),f10(X23,X24)) % 116.76/116.85 | ~ p3(X21,X23) % 116.76/116.85 | ~ p3(X22,X24) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_25,negated_conjecture, % 116.76/116.85 ( p3(f11(X25,X26),f11(X27,X28)) % 116.76/116.85 | ~ p3(X25,X27) % 116.76/116.85 | ~ p3(X26,X28) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_26,negated_conjecture, % 116.76/116.85 ( p3(f12(X29,X30),f12(X31,X32)) % 116.76/116.85 | ~ p3(X29,X31) % 116.76/116.85 | ~ p5(X30,X32) ) ). % 116.76/116.85 % 116.76/116.85 cnf(p3_27,negated_conjecture, % 116.76/116.85 p3(f12(f15(f4(f6(f7(f8(c20))))),c21),f15(f4(f6(f7(f8(c20)))))) ). % 116.76/116.85 % 116.76/116.85 cnf(not_p17_28,negated_conjecture, % 116.76/116.85 ~ p17(f9(f10(f14(f4(f9(c19)),c19),f12(X50,c21))),f6(f7(f8(c20)))) ). % 116.76/116.85 % 116.76/116.85 cnf(p17_29,negated_conjecture, % 116.76/116.85 p17(f9(f10(f14(f4(f9(c19)),c19),f15(f4(f6(f7(f8(c20))))))),f6(f7(f8(c20)))) ). % 116.76/116.85 % 116.76/116.85 cnf(p5_30,negated_conjecture, % 116.76/116.85 ( p5(X6,f7(c20)) % 116.76/116.85 | p3(c19,f4(f6(f7(c20)))) % 116.76/116.85 | p17(f9(f10(f4(f6(f7(f8(c20)))),f11(c19,f12(f13(X6),X6)))),f6(f7(f8(c20)))) % 116.76/116.85 | ~ p18(X6,c21) ) ). % 116.76/116.85 % 116.76/116.85 %-------------------------------------------------------------------------- % 116.76/116.85 %------------------------------------------- % 116.76/116.85 % Proof found % 116.76/116.85 % SZS status Theorem for theBenchmark % 116.76/116.85 % SZS output start Proof % 116.76/116.86 %ClaNum:30(EqnAxiom:0) % 116.76/116.86 %VarNum:109(SingletonVarNum:54) % 116.76/116.86 %MaxLitNum:4 % 116.76/116.86 %MaxfuncDepth:7 % 116.76/116.86 %SharedTerms:31 % 116.76/116.86 %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 % 116.76/116.86 %singleGoalClaCount:12 % 116.76/116.86 [9]~P3(a2) % 116.76/116.86 [4]P6(f5(a1,a2),a1) % 116.76/116.86 [10]~P5(a2,f12(a3)) % 116.76/116.86 [5]P6(f5(f8(a1),a2),f8(a1)) % 116.76/116.86 [11]~P6(a4,f14(f13(f12(a3)))) % 116.76/116.86 [6]P6(f5(f14(f13(f12(f11(a3)))),a2),f14(f13(f12(f11(a3))))) % 116.76/116.86 [7]P6(f5(f8(f14(f13(f12(f11(a3))))),a2),f8(f14(f13(f12(f11(a3)))))) % 116.76/116.86 [8]P2(f15(f6(f9(f14(f15(a4)),a4),f8(f14(f13(f12(f11(a3))))))),f13(f12(f11(a3)))) % 116.76/116.86 [1]P1(x11,x11) % 116.76/116.86 [2]P5(x21,x21) % 116.76/116.86 [3]P6(x31,x31) % 116.76/116.86 [12]~P2(f15(f6(f9(f14(f15(a4)),a4),f5(x121,a2))),f13(f12(f11(a3)))) % 116.76/116.86 [14]~P5(x141,x142)+P1(f13(x141),f13(x142)) % 116.76/116.86 [15]~P6(x151,x152)+P1(f15(x151),f15(x152)) % 116.76/116.86 [16]~P5(x161,x162)+P5(f12(x161),f12(x162)) % 116.76/116.86 [17]~P5(x171,x172)+P5(f11(x171),f11(x172)) % 116.76/116.86 [18]~P1(x181,x182)+P6(f14(x181),f14(x182)) % 116.76/116.86 [19]~P6(x191,x192)+P6(f8(x191),f8(x192)) % 116.76/116.86 [20]~P5(x201,x202)+P6(f10(x201),f10(x202)) % 116.76/116.86 [13]~P5(x132,x131)+P3(x131)+~P3(x132) % 116.76/116.86 [21]~P1(x213,x211)+P1(x211,x212)+~P1(x213,x212) % 116.76/116.86 [22]~P5(x223,x221)+P5(x221,x222)+~P5(x223,x222) % 116.76/116.86 [23]~P6(x233,x231)+P6(x231,x232)+~P6(x233,x232) % 116.76/116.86 [26]~P5(x262,x264)+~P6(x261,x263)+P6(f5(x261,x262),f5(x263,x264)) % 116.76/116.86 [27]~P6(x272,x274)+~P6(x271,x273)+P6(f9(x271,x272),f9(x273,x274)) % 116.76/116.86 [28]~P6(x282,x284)+~P6(x281,x283)+P6(f6(x281,x282),f6(x283,x284)) % 116.76/116.86 [29]~P6(x292,x294)+~P6(x291,x293)+P6(f7(x291,x292),f7(x293,x294)) % 116.76/116.86 [30]~P4(x301,a2)+P5(x301,f12(a3))+P6(a4,f14(f13(f12(a3))))+P2(f15(f6(f14(f13(f12(f11(a3)))),f7(a4,f5(f10(x301),x301)))),f13(f12(f11(a3)))) % 116.76/116.86 [24]~P2(x244,x243)+P2(x241,x242)+~P1(x243,x242)+~P1(x244,x241) % 116.76/116.86 [25]~P4(x254,x253)+P4(x251,x252)+~P5(x253,x252)+~P5(x254,x251) % 116.76/116.86 %EqnAxiom % 116.76/116.86 % 116.76/116.86 %------------------------------------------- % 116.76/116.87 cnf(39,plain, % 116.76/116.87 (P6(a1,f5(a1,a2))), % 116.76/116.87 inference(scs_inference,[],[4,3,23])). % 116.76/116.87 cnf(47,plain, % 116.76/116.87 (P6(f8(a1),f5(f8(a1),a2))), % 116.76/116.87 inference(scs_inference,[],[5,3,23])). % 116.76/116.87 cnf(55,plain, % 116.76/116.87 (P6(f8(f14(f13(f12(f11(a3))))),f5(f8(f14(f13(f12(f11(a3))))),a2))), % 116.76/116.87 inference(scs_inference,[],[7,3,23])). % 116.76/116.87 cnf(59,plain, % 116.76/116.87 (P6(f5(a1,f12(x591)),f5(f5(a1,a2),f12(x591)))), % 116.76/116.87 inference(scs_inference,[],[39,2,26,16])). % 116.76/116.87 cnf(62,plain, % 116.76/116.87 (P6(f7(f8(f8(a1)),f8(f8(a1))),f7(f8(f5(f8(a1),a2)),f8(f5(f8(a1),a2))))), % 116.76/116.87 inference(scs_inference,[],[47,29,19])). % 116.76/116.87 cnf(132,plain, % 116.76/116.87 (P1(f15(f9(f5(a1,f12(x1321)),f5(a1,f12(x1321)))),f15(f9(f5(f5(a1,a2),f12(x1321)),f5(f5(a1,a2),f12(x1321)))))), % 116.76/116.87 inference(scs_inference,[],[59,15,27])). % 116.76/116.87 cnf(142,plain, % 116.76/116.87 (P1(f15(f7(f5(a1,f12(x1421)),f5(a1,f12(x1421)))),f15(f7(f5(f5(a1,a2),f12(x1421)),f5(f5(a1,a2),f12(x1421)))))), % 116.76/116.87 inference(scs_inference,[],[59,15,29])). % 116.76/116.87 cnf(170,plain, % 116.76/116.87 (P1(f15(f9(f5(f5(a1,a2),f12(x1701)),f5(f5(a1,a2),f12(x1701)))),f15(f9(f5(a1,f12(x1701)),f5(a1,f12(x1701)))))), % 116.76/116.87 inference(scs_inference,[],[132,1,21])). % 116.76/116.87 cnf(182,plain, % 116.76/116.87 (P1(f15(f7(f5(f5(a1,a2),f12(x1821)),f5(f5(a1,a2),f12(x1821)))),f15(f7(f5(a1,f12(x1821)),f5(a1,f12(x1821)))))), % 116.76/116.87 inference(scs_inference,[],[142,1,21])). % 116.76/116.87 cnf(193,plain, % 116.76/116.87 (P6(f14(f15(f5(a1,a2))),f14(f15(a1)))), % 116.76/116.87 inference(scs_inference,[],[4,15,18])). % 116.76/116.87 cnf(418,plain, % 116.76/116.87 (P6(f8(f5(f5(a1,f12(x4181)),x4182)),f8(f5(f5(f5(a1,a2),f12(x4181)),x4182)))), % 116.76/116.87 inference(scs_inference,[],[2,59,19,26])). % 116.76/116.87 cnf(749,plain, % 116.76/116.87 (P6(f9(f7(f8(f8(a1)),f8(f8(a1))),f7(f8(f8(a1)),f8(f8(a1)))),f9(f7(f8(f5(f8(a1),a2)),f8(f5(f8(a1),a2))),f7(f8(f5(f8(a1),a2)),f8(f5(f8(a1),a2)))))), % 116.76/116.87 inference(scs_inference,[],[418,62,182,2,15,18,19,26,27])). % 116.76/116.87 cnf(771,plain, % 116.76/116.87 (~P1(f15(f6(f9(f14(f15(a4)),a4),f8(f14(f13(f12(f11(a3))))))),f15(f6(f9(f14(f15(a4)),a4),f5(x7711,a2))))), % 116.76/116.87 inference(scs_inference,[],[1,749,8,170,193,12,2,15,19,18,26,28,27,29,24])). % 116.76/116.87 cnf(3281,plain, % 116.76/116.87 ($false), % 116.76/116.87 inference(scs_inference,[],[3,55,771,15,28]), % 116.76/116.87 ['proof']). % 116.76/116.88 % SZS output end Proof % 116.89/116.88 % Total time :116.200000s %------------------------------------------------------------------------------