%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN600-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 : n001.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:04 EDT 2024 % Result : Unsatisfiable 3.58s 3.70s % Output : CNFRefutation 3.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SYN600-1 : TPTP v8.2.0. Released v2.5.0. % 0.11/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.34 % Computer : n001.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Sun Jun 23 19:45:54 EDT 2024 % 0.20/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 3.58/3.69 %------------------------------------------- % 3.58/3.69 % File :CSE---1.7 % 3.58/3.69 % Problem :theBenchmark % 3.58/3.69 % Transform :cnf % 3.58/3.69 % Format :tptp:raw % 3.58/3.69 % Command :java -jar mcs_scs.jar %d %s % 3.58/3.69 % 3.58/3.69 % Result :Theorem 3.080000s % 3.58/3.69 % Output :CNFRefutation 3.080000s % 3.58/3.69 %------------------------------------------- % 3.58/3.70 %-------------------------------------------------------------------------- % 3.58/3.70 % File : SYN600-1 : TPTP v8.2.0. Released v2.5.0. % 3.58/3.70 % Domain : Syntactic % 3.58/3.70 % Problem : Harrison problem 3759 % 3.58/3.70 % Version : Especial. % 3.58/3.70 % English : % 3.58/3.70 % 3.58/3.70 % Refs : [Har01] Email to G. Sutcliffe % 3.58/3.70 % Source : [Har01] % 3.58/3.70 % Names : % 3.58/3.70 % 3.58/3.70 % Status : Unsatisfiable % 3.58/3.70 % Rating : 0.27 v8.2.0, 0.43 v8.1.0, 0.50 v6.1.0, 0.57 v6.0.0, 0.44 v5.5.0, 0.62 v5.4.0, 0.50 v5.3.0, 0.60 v5.2.0, 0.54 v5.1.0, 0.50 v5.0.0, 0.40 v4.1.0, 0.47 v4.0.1, 0.57 v3.4.0, 0.40 v3.3.0, 0.33 v2.7.0, 0.38 v2.6.0, 0.33 v2.5.0 % 3.58/3.70 % Syntax : Number of clauses : 29 ( 8 unt; 0 nHn; 25 RR) % 3.58/3.70 % Number of literals : 64 ( 0 equ; 36 neg) % 3.58/3.70 % Maximal clause size : 4 ( 2 avg) % 3.58/3.70 % Maximal term depth : 12 ( 3 avg) % 3.58/3.70 % Number of predicates : 7 ( 7 usr; 0 prp; 1-2 aty) % 3.58/3.70 % Number of functors : 14 ( 14 usr; 3 con; 0-2 aty) % 3.58/3.70 % Number of variables : 58 ( 0 sgn) % 3.58/3.70 % SPC : CNF_UNS_RFO_NEQ_HRN % 3.58/3.70 % 3.58/3.70 % Comments : % 3.58/3.70 %-------------------------------------------------------------------------- % 3.58/3.70 cnf(c21_is_p19_1,negated_conjecture, % 3.58/3.70 p19(c21) ). % 3.58/3.70 % 3.58/3.70 cnf(c22_is_p19_2,negated_conjecture, % 3.58/3.70 p19(c22) ). % 3.58/3.70 % 3.58/3.70 cnf(p2_3,negated_conjecture, % 3.58/3.70 p2(X11,X11) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_4,negated_conjecture, % 3.58/3.70 p7(X32,X32) ). % 3.58/3.70 % 3.58/3.70 cnf(p5_5,negated_conjecture, % 3.58/3.70 p5(X29,X29) ). % 3.58/3.70 % 3.58/3.70 cnf(p3_6,negated_conjecture, % 3.58/3.70 p3(X16,X16) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_7,negated_conjecture, % 3.58/3.70 p7(f16(c21),f16(c22)) ). % 3.58/3.70 % 3.58/3.70 cnf(not_p3_8,negated_conjecture, % 3.58/3.70 ~ p3(f4(f6(c21)),f4(f6(c22))) ). % 3.58/3.70 % 3.58/3.70 cnf(p19_9,negated_conjecture, % 3.58/3.70 ( p19(X9) % 3.58/3.70 | ~ p19(X10) % 3.58/3.70 | ~ p5(X10,X9) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_10,negated_conjecture, % 3.58/3.70 ( p7(f16(X43),f16(X44)) % 3.58/3.70 | ~ p5(X43,X44) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p2_11,negated_conjecture, % 3.58/3.70 ( p2(f6(X14),f6(X15)) % 3.58/3.70 | ~ p5(X14,X15) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p3_12,negated_conjecture, % 3.58/3.70 ( p3(f11(X19),f11(X20)) % 3.58/3.70 | ~ p3(X19,X20) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p3_13,negated_conjecture, % 3.58/3.70 ( p3(f12(X21),f12(X22)) % 3.58/3.70 | ~ p3(X21,X22) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p3_14,negated_conjecture, % 3.58/3.70 ( p3(f14(X23),f14(X24)) % 3.58/3.70 | ~ p3(X23,X24) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p3_15,negated_conjecture, % 3.58/3.70 ( p3(f4(X25),f4(X26)) % 3.58/3.70 | ~ p2(X25,X26) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_16,negated_conjecture, % 3.58/3.70 ( p7(f13(X39),f13(X40)) % 3.58/3.70 | ~ p3(X39,X40) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_17,negated_conjecture, % 3.58/3.70 ( p7(f15(X41),f15(X42)) % 3.58/3.70 | ~ p7(X41,X42) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p2_18,negated_conjecture, % 3.58/3.70 ( p2(X12,X13) % 3.58/3.70 | ~ p2(X11,X12) % 3.58/3.70 | ~ p2(X11,X13) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_19,negated_conjecture, % 3.58/3.70 ( p7(X33,X34) % 3.58/3.70 | ~ p7(X32,X33) % 3.58/3.70 | ~ p7(X32,X34) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p5_20,negated_conjecture, % 3.58/3.70 ( p5(X30,X31) % 3.58/3.70 | ~ p5(X29,X30) % 3.58/3.70 | ~ p5(X29,X31) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p3_21,negated_conjecture, % 3.58/3.70 ( p3(X17,X18) % 3.58/3.70 | ~ p3(X16,X17) % 3.58/3.70 | ~ p3(X16,X18) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p17_22,negated_conjecture, % 3.58/3.70 ( p17(X0,X1) % 3.58/3.70 | ~ p7(X2,X0) % 3.58/3.70 | ~ p7(X3,X1) % 3.58/3.70 | ~ p17(X2,X3) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p18_23,negated_conjecture, % 3.58/3.70 ( p18(X5,X6) % 3.58/3.70 | ~ p7(X7,X5) % 3.58/3.70 | ~ p7(X8,X6) % 3.58/3.70 | ~ p18(X7,X8) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_24,negated_conjecture, % 3.58/3.70 ( p7(f9(X49,X50),f9(X51,X52)) % 3.58/3.70 | ~ p7(X50,X52) % 3.58/3.70 | ~ p7(X49,X51) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_25,negated_conjecture, % 3.58/3.70 ( p7(f10(X35,X36),f10(X37,X38)) % 3.58/3.70 | ~ p3(X36,X38) % 3.58/3.70 | ~ p7(X35,X37) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p7_26,negated_conjecture, % 3.58/3.70 ( p7(f8(X45,X46),f8(X47,X48)) % 3.58/3.70 | ~ p7(X45,X47) % 3.58/3.70 | ~ p7(X46,X48) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p18_27,negated_conjecture, % 3.58/3.70 ( p18(f9(f10(f13(f11(f14(f12(c20)))),f4(f6(X4))),f10(f13(f11(f14(f12(c20)))),f11(f12(f12(f12(f12(f12(f12(f12(c20)))))))))),f15(f16(X4))) % 3.58/3.70 | ~ p19(X4) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p17_28,negated_conjecture, % 3.58/3.70 ( p17(f15(f16(X4)),f8(f13(f11(f14(f12(c20)))),f9(f10(f13(f11(f14(f12(c20)))),f4(f6(X4))),f10(f13(f11(f14(f12(c20)))),f11(f12(f12(f12(f12(f12(f12(f12(c20)))))))))))) % 3.58/3.70 | ~ p19(X4) ) ). % 3.58/3.70 % 3.58/3.70 cnf(p3_29,negated_conjecture, % 3.58/3.70 ( p3(f4(f6(X27)),X28) % 3.58/3.70 | ~ p19(X27) % 3.58/3.70 | ~ p18(f9(f10(f13(f11(f14(f12(c20)))),X28),f10(f13(f11(f14(f12(c20)))),f11(f12(f12(f12(f12(f12(f12(f12(c20)))))))))),f15(f16(X27))) % 3.58/3.70 | ~ p17(f15(f16(X27)),f8(f13(f11(f14(f12(c20)))),f9(f10(f13(f11(f14(f12(c20)))),X28),f10(f13(f11(f14(f12(c20)))),f11(f12(f12(f12(f12(f12(f12(f12(c20)))))))))))) ) ). % 3.58/3.70 % 3.58/3.70 %-------------------------------------------------------------------------- % 3.58/3.70 %------------------------------------------- % 3.58/3.70 % Proof found % 3.58/3.70 % SZS status Theorem for theBenchmark % 3.58/3.70 % SZS output start Proof % 3.58/3.70 %ClaNum:29(EqnAxiom:0) % 3.58/3.70 %VarNum:121(SingletonVarNum:58) % 3.58/3.70 %MaxLitNum:4 % 3.58/3.70 %MaxfuncDepth:11 % 3.58/3.70 %SharedTerms:24 % 3.58/3.70 %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 % 3.58/3.70 %singleGoalClaCount:8 % 3.58/3.70 [1]P1(a1) % 3.58/3.70 [2]P1(a3) % 3.58/3.70 [7]P5(f4(a1),f4(a3)) % 3.58/3.70 [8]~P7(f12(f11(a1)),f12(f11(a3))) % 3.58/3.70 [3]P4(x31,x31) % 3.58/3.70 [4]P5(x41,x41) % 3.58/3.70 [5]P6(x51,x51) % 3.58/3.70 [6]P7(x61,x61) % 3.58/3.70 [27]~P1(x271)+P3(f13(f7(f5(f6(f10(f8(a2)))),f12(f11(x271))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))),f9(f4(x271))) % 3.58/3.70 [28]~P1(x281)+P2(f9(f4(x281)),f14(f5(f6(f10(f8(a2)))),f13(f7(f5(f6(f10(f8(a2)))),f12(f11(x281))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))))) % 3.58/3.70 [10]~P6(x101,x102)+P4(f11(x101),f11(x102)) % 3.58/3.70 [11]~P6(x111,x112)+P5(f4(x111),f4(x112)) % 3.58/3.70 [12]~P7(x121,x122)+P5(f5(x121),f5(x122)) % 3.58/3.70 [13]~P5(x131,x132)+P5(f9(x131),f9(x132)) % 3.58/3.70 [14]~P4(x141,x142)+P7(f12(x141),f12(x142)) % 3.58/3.70 [15]~P7(x151,x152)+P7(f6(x151),f6(x152)) % 3.58/3.70 [16]~P7(x161,x162)+P7(f8(x161),f8(x162)) % 3.58/3.71 [17]~P7(x171,x172)+P7(f10(x171),f10(x172)) % 3.58/3.71 [9]~P6(x92,x91)+P1(x91)+~P1(x92) % 3.58/3.71 [18]~P4(x183,x181)+P4(x181,x182)+~P4(x183,x182) % 3.58/3.71 [19]~P5(x193,x191)+P5(x191,x192)+~P5(x193,x192) % 3.58/3.71 [20]~P6(x203,x201)+P6(x201,x202)+~P6(x203,x202) % 3.58/3.71 [21]~P7(x213,x211)+P7(x211,x212)+~P7(x213,x212) % 3.58/3.71 [24]~P5(x242,x244)+~P5(x241,x243)+P5(f13(x241,x242),f13(x243,x244)) % 3.58/3.71 [25]~P5(x251,x253)+~P7(x252,x254)+P5(f7(x251,x252),f7(x253,x254)) % 3.58/3.71 [26]~P5(x262,x264)+~P5(x261,x263)+P5(f14(x261,x262),f14(x263,x264)) % 3.58/3.71 [29]~P1(x291)+P7(f12(f11(x291)),x292)+~P3(f13(f7(f5(f6(f10(f8(a2)))),x292),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))),f9(f4(x291)))+~P2(f9(f4(x291)),f14(f5(f6(f10(f8(a2)))),f13(f7(f5(f6(f10(f8(a2)))),x292),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))))) % 3.58/3.71 [22]~P2(x224,x223)+P2(x221,x222)+~P5(x223,x222)+~P5(x224,x221) % 3.58/3.71 [23]~P3(x234,x233)+P3(x231,x232)+~P5(x233,x232)+~P5(x234,x231) % 3.58/3.71 %EqnAxiom % 3.58/3.71 % 3.58/3.71 %------------------------------------------- % 3.58/3.71 cnf(131,plain, % 3.58/3.71 (P3(f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))),f9(f4(a1)))), % 3.58/3.71 inference(scs_inference,[],[1,5,27,9])). % 3.58/3.71 cnf(132,plain, % 3.58/3.71 (P2(f9(f4(a1)),f14(f5(f6(f10(f8(a2)))),f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2))))))))))))), % 3.58/3.71 inference(scs_inference,[],[1,5,28,9])). % 3.58/3.71 cnf(133,plain, % 3.58/3.71 (~P3(f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))),f9(f4(a3)))+~P2(f9(f4(a3)),f14(f5(f6(f10(f8(a2)))),f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2))))))))))))), % 3.58/3.71 inference(scs_inference,[],[6,8,2,21,29])). % 3.58/3.71 cnf(207,plain, % 3.58/3.71 (~P5(f9(f4(a1)),x2071)+P2(x2071,f14(f5(f6(f10(f8(a2)))),f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2))))))))))))), % 3.58/3.71 inference(scs_inference,[],[132,4,22])). % 3.58/3.71 cnf(265,plain, % 3.58/3.71 (P2(f9(f4(a3)),f14(f5(f6(f10(f8(a2)))),f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2))))))))))))), % 3.58/3.71 inference(scs_inference,[],[7,13,207])). % 3.58/3.71 cnf(266,plain, % 3.58/3.71 (~P3(f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))),f9(f4(a3)))), % 3.58/3.71 inference(scs_inference,[],[265,133])). % 3.58/3.71 cnf(484,plain, % 3.58/3.71 (~P5(x4841,f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))))+~P3(x4841,f9(f4(a3)))), % 3.58/3.71 inference(scs_inference,[],[266,4,23])). % 3.58/3.71 cnf(492,plain, % 3.58/3.71 (~P5(x4921,f7(f5(f6(f10(f8(a2)))),f12(f11(a1))))+~P3(f13(x4921,f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))),f9(f4(a3)))), % 3.58/3.71 inference(scs_inference,[],[4,484,24])). % 3.58/3.71 cnf(493,plain, % 3.58/3.71 (~P5(f9(f4(a1)),f9(f4(a3)))+~P5(f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))),f13(f7(f5(f6(f10(f8(a2)))),f12(f11(a1))),f7(f5(f6(f10(f8(a2)))),f6(f8(f8(f8(f8(f8(f8(f8(a2)))))))))))), % 3.58/3.71 inference(scs_inference,[],[4,131,492,23])). % 3.58/3.71 cnf(494,plain, % 3.58/3.71 (~P5(f9(f4(a1)),f9(f4(a3)))), % 3.58/3.71 inference(scs_inference,[],[4,493])). % 3.58/3.71 cnf(496,plain, % 3.58/3.71 ($false), % 3.58/3.71 inference(scs_inference,[],[494,7,13]), % 3.58/3.71 ['proof']). % 3.58/3.71 % SZS output end Proof % 3.58/3.71 % Total time :3.080000s %------------------------------------------------------------------------------