%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN604-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:05 EDT 2024 % Result : Unsatisfiable 0.50s 0.65s % Output : CNFRefutation 0.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN604-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.31 % Computer : n024.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.31 % CPULimit : 300 % 0.12/0.31 % WCLimit : 300 % 0.12/0.31 % DateTime : Sun Jun 23 22:48:09 EDT 2024 % 0.16/0.31 % CPUTime : % 0.48/0.54 start to proof:theBenchmark % 0.50/0.64 %------------------------------------------- % 0.50/0.64 % File :CSE---1.7 % 0.50/0.64 % Problem :theBenchmark % 0.50/0.64 % Transform :cnf % 0.50/0.64 % Format :tptp:raw % 0.50/0.64 % Command :java -jar mcs_scs.jar %d %s % 0.50/0.64 % 0.50/0.64 % Result :Theorem 0.070000s % 0.50/0.64 % Output :CNFRefutation 0.070000s % 0.50/0.64 %------------------------------------------- % 0.50/0.64 %-------------------------------------------------------------------------- % 0.50/0.64 % File : SYN604-1 : TPTP v8.2.0. Released v2.5.0. % 0.50/0.64 % Domain : Syntactic % 0.50/0.64 % Problem : Harrison problem 3820 % 0.50/0.64 % Version : Especial. % 0.50/0.64 % English : % 0.50/0.64 % 0.50/0.64 % Refs : [Har01] Email to G. Sutcliffe % 0.50/0.64 % Source : [Har01] % 0.50/0.64 % Names : % 0.50/0.64 % 0.50/0.64 % Status : Unsatisfiable % 0.50/0.64 % Rating : 0.00 v8.1.0, 0.14 v7.5.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.18 v5.0.0, 0.29 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.29 v3.4.0, 0.25 v3.3.0, 0.33 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 0.50/0.64 % Syntax : Number of clauses : 30 ( 11 unt; 1 nHn; 20 RR) % 0.50/0.64 % Number of literals : 61 ( 0 equ; 31 neg) % 0.50/0.64 % Maximal clause size : 4 ( 2 avg) % 0.50/0.64 % Maximal term depth : 6 ( 1 avg) % 0.50/0.64 % Number of predicates : 7 ( 7 usr; 0 prp; 2-2 aty) % 0.50/0.64 % Number of functors : 15 ( 15 usr; 7 con; 0-2 aty) % 0.50/0.64 % Number of variables : 60 ( 2 sgn) % 0.50/0.64 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.50/0.64 % 0.50/0.64 % Comments : % 0.50/0.64 %-------------------------------------------------------------------------- % 0.50/0.64 cnf(p14_1,negated_conjecture, % 0.50/0.64 p14(X0,X0) ). % 0.50/0.64 % 0.50/0.64 cnf(p9_2,negated_conjecture, % 0.50/0.64 p9(X49,X49) ). % 0.50/0.64 % 0.50/0.64 cnf(p5_3,negated_conjecture, % 0.50/0.64 p5(X42,X42) ). % 0.50/0.64 % 0.50/0.64 cnf(p3_4,negated_conjecture, % 0.50/0.64 p3(X31,X31) ). % 0.50/0.64 % 0.50/0.64 cnf(p2_5,negated_conjecture, % 0.50/0.64 p2(X20,X20) ). % 0.50/0.64 % 0.50/0.64 cnf(p15_6,negated_conjecture, % 0.50/0.64 p15(c17,c18) ). % 0.50/0.64 % 0.50/0.64 cnf(p3_7,negated_conjecture, % 0.50/0.64 p3(f4(f8(X41)),f12(X41)) ). % 0.50/0.64 % 0.50/0.64 cnf(p3_8,negated_conjecture, % 0.50/0.64 p3(f12(f10(X38)),f10(X38)) ). % 0.50/0.64 % 0.50/0.64 cnf(p16_9,negated_conjecture, % 0.50/0.64 p16(f10(f11(c21)),f12(X16)) ). % 0.50/0.64 % 0.50/0.64 cnf(p16_10,negated_conjecture, % 0.50/0.64 ( p16(X14,X15) % 0.50/0.64 | p16(X15,f12(X14)) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p9_11,negated_conjecture, % 0.50/0.64 ( p9(f11(X52),f11(X53)) % 0.50/0.64 | ~ p9(X52,X53) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p2_12,negated_conjecture, % 0.50/0.64 ( p2(f13(X23),f13(X24)) % 0.50/0.64 | ~ p2(X23,X24) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p2_13,negated_conjecture, % 0.50/0.64 ( p2(f8(X29),f8(X30)) % 0.50/0.64 | ~ p3(X29,X30) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p3_14,negated_conjecture, % 0.50/0.64 ( p3(f10(X34),f10(X35)) % 0.50/0.64 | ~ p9(X34,X35) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p3_15,negated_conjecture, % 0.50/0.64 ( p3(f12(X36),f12(X37)) % 0.50/0.64 | ~ p3(X36,X37) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p3_16,negated_conjecture, % 0.50/0.64 ( p3(f4(X39),f4(X40)) % 0.50/0.64 | ~ p2(X39,X40) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p16_17,negated_conjecture, % 0.50/0.64 p16(f4(f6(c18,c22)),f4(f6(c18,X17))) ). % 0.50/0.64 % 0.50/0.64 cnf(p14_18,negated_conjecture, % 0.50/0.64 ( p14(X1,X2) % 0.50/0.64 | ~ p14(X0,X1) % 0.50/0.64 | ~ p14(X0,X2) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p9_19,negated_conjecture, % 0.50/0.64 ( p9(X50,X51) % 0.50/0.64 | ~ p9(X49,X50) % 0.50/0.64 | ~ p9(X49,X51) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p5_20,negated_conjecture, % 0.50/0.64 ( p5(X43,X44) % 0.50/0.64 | ~ p5(X42,X43) % 0.50/0.64 | ~ p5(X42,X44) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p3_21,negated_conjecture, % 0.50/0.64 ( p3(X32,X33) % 0.50/0.64 | ~ p3(X31,X32) % 0.50/0.64 | ~ p3(X31,X33) ) ). % 0.50/0.64 % 0.50/0.64 cnf(p2_22,negated_conjecture, % 0.50/0.64 ( p2(X21,X22) % 0.50/0.65 | ~ p2(X20,X21) % 0.50/0.65 | ~ p2(X20,X22) ) ). % 0.50/0.65 % 0.50/0.65 cnf(p16_23,negated_conjecture, % 0.50/0.65 ( p16(X11,X12) % 0.50/0.65 | ~ p16(X11,X13) % 0.50/0.65 | ~ p16(X13,X12) ) ). % 0.50/0.65 % 0.50/0.65 cnf(p15_24,negated_conjecture, % 0.50/0.65 ( p15(X3,X4) % 0.50/0.65 | ~ p15(X5,X6) % 0.50/0.65 | ~ p5(X6,X4) % 0.50/0.65 | ~ p14(X5,X3) ) ). % 0.50/0.65 % 0.50/0.65 cnf(p16_25,negated_conjecture, % 0.50/0.65 ( p16(X7,X8) % 0.50/0.65 | ~ p3(X9,X7) % 0.50/0.65 | ~ p3(X10,X8) % 0.50/0.65 | ~ p16(X9,X10) ) ). % 0.50/0.65 % 0.50/0.65 cnf(p5_26,negated_conjecture, % 0.50/0.65 ( p5(f7(X45,X46),f7(X47,X48)) % 0.50/0.65 | ~ p2(X45,X47) % 0.50/0.65 | ~ p5(X46,X48) ) ). % 0.50/0.65 % 0.50/0.65 cnf(p2_27,negated_conjecture, % 0.50/0.65 ( p2(f6(X25,X26),f6(X27,X28)) % 0.50/0.65 | ~ p2(X26,X28) % 0.50/0.65 | ~ p5(X25,X27) ) ). % 0.50/0.65 % 0.50/0.65 cnf(not_p16_28,negated_conjecture, % 0.50/0.65 ~ p16(f4(f6(f7(c20,c18),X54)),f4(f6(f7(c20,c18),f13(X54)))) ). % 0.50/0.65 % 0.50/0.65 cnf(p16_29,negated_conjecture, % 0.50/0.65 ( p16(f4(f6(f7(c20,c18),c23)),f4(f6(f7(c20,c18),X18))) % 0.50/0.65 | ~ p16(f4(X18),f12(c19)) ) ). % 0.50/0.65 % 0.50/0.65 cnf(p16_30,negated_conjecture, % 0.50/0.65 ( p16(f4(f6(f7(c20,c18),f8(f10(f11(c21))))),f4(f6(f7(c20,c18),X19))) % 0.50/0.65 | ~ p16(c19,f4(X19)) ) ). % 0.50/0.65 % 0.50/0.65 %-------------------------------------------------------------------------- % 0.50/0.65 %------------------------------------------- % 0.50/0.65 % Proof found % 0.50/0.65 % SZS status Theorem for theBenchmark % 0.50/0.65 % SZS output start Proof % 0.50/0.65 %ClaNum:30(EqnAxiom:0) % 0.50/0.65 %VarNum:118(SingletonVarNum:60) % 0.50/0.65 %MaxLitNum:4 % 0.50/0.65 %MaxfuncDepth:5 % 0.50/0.65 %SharedTerms:19 % 0.50/0.65 %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 % 0.50/0.65 %singleGoalClaCount:11 % 0.50/0.65 [1]P1(a1,a2) % 0.50/0.65 [2]P2(x21,x21) % 0.50/0.65 [3]P3(x31,x31) % 0.50/0.65 [4]P4(x41,x41) % 0.50/0.65 [5]P5(x51,x51) % 0.50/0.65 [6]P6(x61,x61) % 0.50/0.65 [7]P7(f7(f6(a3)),f10(x71)) % 0.50/0.65 [8]P5(f12(f11(x81)),f10(x81)) % 0.50/0.65 [9]P5(f10(f7(x91)),f7(x91)) % 0.50/0.65 [10]P7(f12(f14(a2,a8)),f12(f14(a2,x101))) % 0.50/0.65 [11]~P7(f12(f14(f15(a4,a2),x111)),f12(f14(f15(a4,a2),f13(x111)))) % 0.50/0.65 [29]~P7(f12(x291),f10(a5))+P7(f12(f14(f15(a4,a2),a9)),f12(f14(f15(a4,a2),x291))) % 0.50/0.65 [30]~P7(a5,f12(x301))+P7(f12(f14(f15(a4,a2),f11(f7(f6(a3))))),f12(f14(f15(a4,a2),x301))) % 0.50/0.65 [12]P7(x121,x122)+P7(x122,f10(x121)) % 0.50/0.65 [13]~P3(x131,x132)+P3(f6(x131),f6(x132)) % 0.50/0.65 [14]~P6(x141,x142)+P5(f12(x141),f12(x142)) % 0.50/0.65 [15]~P5(x151,x152)+P5(f10(x151),f10(x152)) % 0.50/0.65 [16]~P3(x161,x162)+P5(f7(x161),f7(x162)) % 0.50/0.65 [17]~P5(x171,x172)+P6(f11(x171),f11(x172)) % 0.50/0.65 [18]~P6(x181,x182)+P6(f13(x181),f13(x182)) % 0.50/0.65 [19]~P2(x193,x191)+P2(x191,x192)+~P2(x193,x192) % 0.50/0.65 [20]~P3(x203,x201)+P3(x201,x202)+~P3(x203,x202) % 0.50/0.65 [21]~P4(x213,x211)+P4(x211,x212)+~P4(x213,x212) % 0.50/0.65 [22]~P5(x223,x221)+P5(x221,x222)+~P5(x223,x222) % 0.50/0.65 [23]~P6(x233,x231)+P6(x231,x232)+~P6(x233,x232) % 0.50/0.65 [24]~P7(x241,x243)+P7(x241,x242)+~P7(x243,x242) % 0.50/0.65 [27]~P4(x272,x274)+~P6(x271,x273)+P4(f15(x271,x272),f15(x273,x274)) % 0.50/0.65 [28]~P4(x281,x283)+~P6(x282,x284)+P6(f14(x281,x282),f14(x283,x284)) % 0.50/0.65 [25]~P1(x253,x254)+P1(x251,x252)+~P2(x253,x251)+~P4(x254,x252) % 0.50/0.65 [26]~P7(x264,x263)+P7(x261,x262)+~P5(x263,x262)+~P5(x264,x261) % 0.50/0.65 %EqnAxiom % 0.50/0.65 % 0.50/0.65 %------------------------------------------- % 0.50/0.65 cnf(37,plain, % 0.50/0.65 (P7(a5,f12(f13(a9)))), % 0.50/0.65 inference(scs_inference,[],[7,11,29,24,12])). % 0.50/0.65 cnf(41,plain, % 0.50/0.65 (P5(f7(x411),f10(f7(x411)))), % 0.50/0.65 inference(scs_inference,[],[9,5,22])). % 0.50/0.65 cnf(49,plain, % 0.50/0.65 (P7(f10(f7(f6(a3))),f10(x491))), % 0.50/0.65 inference(scs_inference,[],[41,5,7,26])). % 0.50/0.65 cnf(53,plain, % 0.50/0.65 (P7(f7(f6(a3)),f7(f6(a3)))), % 0.50/0.65 inference(scs_inference,[],[49,9,26])). % 0.50/0.65 cnf(57,plain, % 0.50/0.65 (P7(f10(f7(f6(a3))),f7(f6(a3)))), % 0.50/0.65 inference(scs_inference,[],[53,41,5,26])). % 0.50/0.65 cnf(61,plain, % 0.50/0.65 (P5(f12(f11(f7(x611))),f12(f11(f10(f7(x611)))))), % 0.50/0.65 inference(scs_inference,[],[41,14,17])). % 0.50/0.65 cnf(62,plain, % 0.50/0.65 (P5(f12(f11(f10(f7(x621)))),f12(f11(f7(x621))))), % 0.50/0.65 inference(scs_inference,[],[61,5,22])). % 0.50/0.65 cnf(70,plain, % 0.50/0.65 (~P7(f12(f11(f10(f7(x701)))),x702)+P7(f12(f11(f7(x701))),x702)), % 0.50/0.65 inference(scs_inference,[],[62,5,26])). % 0.50/0.65 cnf(81,plain, % 0.50/0.65 (P5(f10(x811),f12(f11(x811)))), % 0.50/0.65 inference(scs_inference,[],[8,5,22])). % 0.50/0.65 cnf(84,plain, % 0.50/0.65 (P7(f12(f11(f7(f6(a3)))),f12(f11(f7(f6(a3)))))), % 0.50/0.65 inference(scs_inference,[],[8,49,5,22,26])). % 0.50/0.65 cnf(88,plain, % 0.50/0.65 (P7(f10(f7(f6(a3))),f12(f11(f7(f6(a3)))))), % 0.50/0.65 inference(scs_inference,[],[8,84,5,26])). % 0.50/0.65 cnf(93,plain, % 0.50/0.65 (P7(f12(f11(f7(f6(a3)))),f10(f7(f6(a3))))), % 0.50/0.65 inference(scs_inference,[],[8,88,81,26])). % 0.50/0.65 cnf(100,plain, % 0.50/0.65 (~P5(a5,x1001)+P7(x1001,f12(f13(a9)))), % 0.50/0.65 inference(scs_inference,[],[37,93,57,5,24,26])). % 0.50/0.65 cnf(103,plain, % 0.50/0.65 (P7(f12(f14(f15(a4,a2),f11(f7(f6(a3))))),f12(f14(f15(a4,a2),f13(a9))))), % 0.50/0.65 inference(scs_inference,[],[5,100,30])). % 0.50/0.65 cnf(111,plain, % 0.50/0.65 (~P7(f12(f11(f10(f7(f6(a3))))),f10(a5))), % 0.50/0.65 inference(scs_inference,[],[103,11,24,29,12,70])). % 0.50/0.65 cnf(156,plain, % 0.50/0.65 (P7(f12(f11(f10(f7(f6(a3))))),f7(f6(a3)))), % 0.50/0.65 inference(scs_inference,[],[9,61,93,26])). % 0.50/0.65 cnf(161,plain, % 0.50/0.65 ($false), % 0.50/0.65 inference(scs_inference,[],[111,156,7,24]), % 0.50/0.65 ['proof']). % 0.50/0.65 % SZS output end Proof % 0.50/0.65 % Total time :0.070000s %------------------------------------------------------------------------------