%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN585-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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:02 EDT 2024 % Result : Unsatisfiable 58.92s 58.99s % Output : CNFRefutation 59.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SYN585-1 : TPTP v8.2.0. Released v2.5.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n018.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Sun Jun 23 19:54:08 EDT 2024 % 0.14/0.36 % CPUTime : % 0.54/0.61 start to proof:theBenchmark % 58.92/58.97 %------------------------------------------- % 58.92/58.97 % File :CSE---1.7 % 58.92/58.97 % Problem :theBenchmark % 58.92/58.97 % Transform :cnf % 58.92/58.97 % Format :tptp:raw % 58.92/58.97 % Command :java -jar mcs_scs.jar %d %s % 58.92/58.97 % 58.92/58.97 % Result :Theorem 58.310000s % 58.92/58.97 % Output :CNFRefutation 58.310000s % 58.92/58.97 %------------------------------------------- % 58.92/58.98 %-------------------------------------------------------------------------- % 58.92/58.98 % File : SYN585-1 : TPTP v8.2.0. Released v2.5.0. % 58.92/58.98 % Domain : Syntactic % 58.92/58.98 % Problem : Harrison problem 3538 % 58.92/58.98 % Version : Especial. % 58.92/58.98 % English : % 58.92/58.98 % 58.92/58.98 % Refs : [Har01] Email to G. Sutcliffe % 58.92/58.98 % Source : [Har01] % 58.92/58.98 % Names : % 58.92/58.98 % 58.92/58.98 % Status : Unsatisfiable % 58.92/58.98 % Rating : 0.00 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.14 v4.1.0, 0.12 v4.0.1, 0.00 v2.5.0 % 58.92/58.98 % Syntax : Number of clauses : 26 ( 12 unt; 2 nHn; 22 RR) % 58.92/58.98 % Number of literals : 53 ( 0 equ; 29 neg) % 58.92/58.98 % Maximal clause size : 4 ( 2 avg) % 58.92/58.98 % Maximal term depth : 3 ( 1 avg) % 58.92/58.99 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty) % 58.92/58.99 % Number of functors : 14 ( 14 usr; 7 con; 0-2 aty) % 58.92/58.99 % Number of variables : 49 ( 1 sgn) % 58.92/58.99 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.92/58.99 % 58.92/58.99 % Comments : % 58.92/58.99 %-------------------------------------------------------------------------- % 58.92/58.99 cnf(p2_1,negated_conjecture, % 58.92/58.99 p2(X18,X18) ). % 58.92/58.99 % 58.92/58.99 cnf(p11_2,negated_conjecture, % 58.92/58.99 p11(X8,X8) ). % 58.92/58.99 % 58.92/58.99 cnf(p10_3,negated_conjecture, % 58.92/58.99 p10(c14,c15) ). % 58.92/58.99 % 58.92/58.99 cnf(p10_4,negated_conjecture, % 58.92/58.99 p10(c17,c14) ). % 58.92/58.99 % 58.92/58.99 cnf(not_p2_5,negated_conjecture, % 58.92/58.99 ~ p2(c14,f3(c13)) ). % 58.92/58.99 % 58.92/58.99 cnf(not_p2_6,negated_conjecture, % 58.92/58.99 ~ p2(c12,f3(c13)) ). % 58.92/58.99 % 58.92/58.99 cnf(p11_7,negated_conjecture, % 58.92/58.99 p11(c18,f9(c12,c14)) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_8,negated_conjecture, % 58.92/58.99 p2(f6(c15,c14),c17) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_9,negated_conjecture, % 58.92/58.99 p2(f5(c15,c14),c16) ). % 58.92/58.99 % 58.92/58.99 cnf(not_p2_10,negated_conjecture, % 58.92/58.99 ~ p2(c12,f3(f4(c13))) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_11,negated_conjecture, % 58.92/58.99 p2(f7(f8(c16,c14),c17),c15) ). % 58.92/58.99 % 58.92/58.99 cnf(not_p11_12,negated_conjecture, % 58.92/58.99 ~ p11(c18,f9(c12,f8(c16,c14))) ). % 58.92/58.99 % 58.92/58.99 cnf(p11_13,negated_conjecture, % 58.92/58.99 ( p11(X9,f8(X10,X11)) % 58.92/58.99 | ~ p11(X9,X11) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_14,negated_conjecture, % 58.92/58.99 ( p2(f4(X23),f4(X24)) % 58.92/58.99 | ~ p2(X23,X24) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_15,negated_conjecture, % 58.92/58.99 ( p2(f3(X21),f3(X22)) % 58.92/58.99 | ~ p2(X21,X22) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p11_16,negated_conjecture, % 58.92/58.99 ( p11(X12,X13) % 58.92/58.99 | ~ p11(X12,X14) % 58.92/58.99 | ~ p11(X14,X13) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_17,negated_conjecture, % 58.92/58.99 ( p2(X19,X20) % 58.92/58.99 | ~ p2(X18,X19) % 58.92/58.99 | ~ p2(X18,X20) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p10_18,negated_conjecture, % 58.92/58.99 ( p10(X0,X1) % 58.92/58.99 | ~ p2(X2,X0) % 58.92/58.99 | ~ p2(X3,X1) % 58.92/58.99 | ~ p10(X2,X3) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p11_19,negated_conjecture, % 58.92/58.99 ( p11(X4,X5) % 58.92/58.99 | ~ p2(X6,X4) % 58.92/58.99 | ~ p2(X7,X5) % 58.92/58.99 | ~ p11(X6,X7) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_20,negated_conjecture, % 58.92/58.99 ( p2(f9(X41,X42),f9(X43,X44)) % 58.92/58.99 | ~ p2(X41,X43) % 58.92/58.99 | ~ p2(X42,X44) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_21,negated_conjecture, % 58.92/58.99 ( p2(f5(X25,X26),f5(X27,X28)) % 58.92/58.99 | ~ p2(X25,X27) % 58.92/58.99 | ~ p2(X26,X28) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_22,negated_conjecture, % 58.92/58.99 ( p2(f6(X29,X30),f6(X31,X32)) % 58.92/58.99 | ~ p2(X30,X32) % 58.92/58.99 | ~ p2(X29,X31) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_23,negated_conjecture, % 58.92/58.99 ( p2(f7(X33,X34),f7(X35,X36)) % 58.92/58.99 | ~ p2(X33,X35) % 58.92/58.99 | ~ p2(X34,X36) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_24,negated_conjecture, % 58.92/58.99 ( p2(f8(X37,X38),f8(X39,X40)) % 58.92/58.99 | ~ p2(X37,X39) % 58.92/58.99 | ~ p2(X38,X40) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p11_25,negated_conjecture, % 58.92/58.99 ( p11(X15,X16) % 58.92/58.99 | p2(X17,f3(c13)) % 58.92/58.99 | ~ p11(f9(X17,X15),f9(X17,X16)) ) ). % 58.92/58.99 % 58.92/58.99 cnf(p2_26,negated_conjecture, % 58.92/58.99 ( p2(X17,f3(c13)) % 58.92/58.99 | p11(f9(X17,X15),f9(X17,X16)) % 58.92/58.99 | ~ p11(X15,X16) ) ). % 58.92/58.99 % 58.92/58.99 %-------------------------------------------------------------------------- % 58.92/58.99 %------------------------------------------- % 58.92/58.99 % Proof found % 58.92/58.99 % SZS status Theorem for theBenchmark % 58.92/58.99 % SZS output start Proof % 58.92/58.99 %ClaNum:26(EqnAxiom:0) % 58.92/58.99 %VarNum:99(SingletonVarNum:49) % 58.92/58.99 %MaxLitNum:4 % 58.92/58.99 %MaxfuncDepth:2 % 58.92/58.99 %SharedTerms:26 % 58.92/58.99 %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 % 58.92/58.99 %singleGoalClaCount:12 % 58.92/58.99 [1]P1(a1,a4) % 58.92/58.99 [2]P1(a5,a1) % 58.92/58.99 [5]P3(a7,f8(a2,a1)) % 58.92/58.99 [6]P2(f9(a4,a1),a5) % 58.92/58.99 [7]P2(f10(a4,a1),a6) % 58.92/58.99 [9]~P2(a1,f11(a3)) % 58.92/58.99 [10]~P2(a2,f11(a3)) % 58.92/58.99 [8]P2(f14(f13(a6,a1),a5),a4) % 58.92/58.99 [11]~P2(a2,f11(f12(a3))) % 58.92/58.99 [12]~P3(a7,f8(a2,f13(a6,a1))) % 58.92/58.99 [3]P2(x31,x31) % 58.92/58.99 [4]P3(x41,x41) % 58.92/58.99 [13]~P2(x131,x132)+P2(f11(x131),f11(x132)) % 58.92/58.99 [14]~P2(x141,x142)+P2(f12(x141),f12(x142)) % 58.92/58.99 [17]~P3(x171,x173)+P3(x171,f13(x172,x173)) % 58.92/58.99 [15]~P2(x153,x151)+P2(x151,x152)+~P2(x153,x152) % 58.92/58.99 [16]~P3(x161,x163)+P3(x161,x162)+~P3(x163,x162) % 58.92/58.99 [20]~P3(x202,x203)+P3(f8(x201,x202),f8(x201,x203))+P2(x201,f11(a3)) % 58.92/58.99 [26]P3(x261,x262)+~P3(f8(x263,x261),f8(x263,x262))+P2(x263,f11(a3)) % 58.92/58.99 [21]~P2(x212,x214)+~P2(x211,x213)+P2(f8(x211,x212),f8(x213,x214)) % 58.92/58.99 [22]~P2(x222,x224)+~P2(x221,x223)+P2(f9(x221,x222),f9(x223,x224)) % 58.92/58.99 [23]~P2(x232,x234)+~P2(x231,x233)+P2(f10(x231,x232),f10(x233,x234)) % 58.92/58.99 [24]~P2(x242,x244)+~P2(x241,x243)+P2(f13(x241,x242),f13(x243,x244)) % 58.92/58.99 [25]~P2(x252,x254)+~P2(x251,x253)+P2(f14(x251,x252),f14(x253,x254)) % 58.92/58.99 [18]~P3(x184,x183)+P3(x181,x182)+~P2(x183,x182)+~P2(x184,x181) % 58.92/58.99 [19]~P1(x194,x193)+P1(x191,x192)+~P2(x193,x192)+~P2(x194,x191) % 58.92/58.99 %EqnAxiom % 58.92/58.99 % 58.92/58.99 %------------------------------------------- % 59.00/59.00 cnf(40,plain, % 59.00/59.00 (P2(a5,f9(a4,a1))), % 59.00/59.00 inference(scs_inference,[],[6,3,15])). % 59.00/59.00 cnf(41,plain, % 59.00/59.00 (P2(x411,x411)), % 59.00/59.00 inference(rename_variables,[],[3])). % 59.00/59.00 cnf(43,plain, % 59.00/59.00 (P3(a5,f9(a4,a1))), % 59.00/59.00 inference(scs_inference,[],[6,3,41,4,15,18])). % 59.00/59.00 cnf(55,plain, % 59.00/59.00 (P2(a6,f10(a4,a1))), % 59.00/59.00 inference(scs_inference,[],[7,3,15])). % 59.00/59.00 cnf(56,plain, % 59.00/59.00 (P2(x561,x561)), % 59.00/59.00 inference(rename_variables,[],[3])). % 59.00/59.00 cnf(58,plain, % 59.00/59.00 (P3(a6,f10(a4,a1))), % 59.00/59.00 inference(scs_inference,[],[7,3,56,4,15,18])). % 59.00/59.00 cnf(69,plain, % 59.00/59.00 (P2(a4,f14(f13(a6,a1),a5))), % 59.00/59.00 inference(scs_inference,[],[8,3,15])). % 59.00/59.00 cnf(70,plain, % 59.00/59.00 (P2(x701,x701)), % 59.00/59.00 inference(rename_variables,[],[3])). % 59.00/59.00 cnf(72,plain, % 59.00/59.00 (P3(a4,f14(f13(a6,a1),a5))), % 59.00/59.00 inference(scs_inference,[],[8,3,70,4,15,18])). % 59.00/59.00 cnf(109,plain, % 59.00/59.00 (P3(f9(a4,a1),a5)), % 59.00/59.00 inference(scs_inference,[],[40,43,6,18])). % 59.00/59.00 cnf(114,plain, % 59.00/59.00 (P3(f10(a4,a1),a6)), % 59.00/59.00 inference(scs_inference,[],[55,58,7,18])). % 59.00/59.00 cnf(117,plain, % 59.00/59.00 (P3(f14(f13(a6,a1),a5),a4)), % 59.00/59.00 inference(scs_inference,[],[69,72,8,18])). % 59.00/59.00 cnf(158,plain, % 59.00/59.00 (P3(a5,f13(x1581,a5))), % 59.00/59.00 inference(scs_inference,[],[109,43,17,16])). % 59.00/59.00 cnf(159,plain, % 59.00/59.00 (P3(f9(a4,a1),f13(x1591,a5))), % 59.00/59.00 inference(scs_inference,[],[109,158,16])). % 59.00/59.00 cnf(164,plain, % 59.00/59.00 (P3(f8(a1,f9(a4,a1)),f8(a1,a5))), % 59.00/59.00 inference(scs_inference,[],[109,9,20])). % 59.00/59.00 cnf(207,plain, % 59.00/59.00 (~P2(f8(a1,f9(a4,a1)),x2071)+P3(x2071,f8(a1,a5))), % 59.00/59.00 inference(scs_inference,[],[164,3,18])). % 59.00/59.00 cnf(525,plain, % 59.00/59.00 (~P2(a1,x5251)+P3(f8(x5251,f9(a4,a1)),f8(a1,a5))), % 59.00/59.00 inference(scs_inference,[],[3,207,21])). % 59.00/59.00 cnf(665,plain, % 59.00/59.00 (~P2(a5,a1)+P3(f8(f9(a4,a1),f9(a4,a1)),f8(a1,a5))), % 59.00/59.00 inference(scs_inference,[],[40,525,15])). % 59.00/59.00 cnf(666,plain, % 59.00/59.00 (~P2(a5,a1)+P3(f8(f9(a4,a1),f9(a4,a1)),f13(x6661,f8(a1,a5)))), % 59.00/59.00 inference(scs_inference,[],[665,17])). % 59.00/59.01 cnf(1144,plain, % 59.00/59.01 (~P2(f8(f9(a4,a1),f9(a4,a1)),x11441)+P3(x11441,f13(x11442,f8(a1,a5)))+~P2(a5,a1)), % 59.00/59.01 inference(scs_inference,[],[3,666,18])). % 59.00/59.01 cnf(1145,plain, % 59.00/59.01 (~P2(f9(a4,a1),a1)+P3(f8(f9(a4,a1),f9(a4,a1)),f13(x11451,f8(a1,a5)))), % 59.00/59.01 inference(scs_inference,[],[3,6,1144,15])). % 59.00/59.01 cnf(1707,plain, % 59.00/59.01 (~P2(f8(f9(a4,a1),f9(a4,a1)),x17071)+P3(x17071,f13(x17072,f8(a1,a5)))+~P2(f9(a4,a1),a1)), % 59.00/59.01 inference(scs_inference,[],[3,1145,18])). % 59.00/59.01 cnf(2085,plain, % 59.00/59.01 (P2(f13(a6,a6),f13(f10(a4,a1),f10(a4,a1)))), % 59.00/59.01 inference(scs_inference,[],[159,55,17,13,14,21,22,23,24])). % 59.00/59.01 cnf(2110,plain, % 59.00/59.01 (P3(x21101,f13(x21102,x21101))), % 59.00/59.01 inference(scs_inference,[],[4,17])). % 59.00/59.01 cnf(2120,plain, % 59.00/59.01 (P2(f8(f9(a4,a1),f9(a4,a1)),f8(a5,a5))), % 59.00/59.01 inference(scs_inference,[],[4,6,17,14,13,23,25,21])). % 59.00/59.01 cnf(2162,plain, % 59.00/59.01 (P3(f10(a4,a1),f13(x21621,a6))), % 59.00/59.01 inference(scs_inference,[],[114,17])). % 59.00/59.01 cnf(2179,plain, % 59.00/59.01 (~P3(f8(a2,a1),f8(a2,f13(a6,a1)))), % 59.00/59.01 inference(scs_inference,[],[2162,2085,2120,5,117,12,7,17,18,1707,16])). % 59.00/59.01 cnf(2184,plain, % 59.00/59.01 ($false), % 59.00/59.01 inference(scs_inference,[],[2179,2110,58,10,17,20]), % 59.00/59.01 ['proof']). % 59.00/59.01 % SZS output end Proof % 59.00/59.01 % Total time :58.310000s %------------------------------------------------------------------------------