%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN565-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 : 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:05:59 EDT 2024 % Result : Unsatisfiable 116.93s 117.08s % Output : CNFRefutation 116.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN565-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/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 20:33:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 116.87/117.06 %------------------------------------------- % 116.87/117.06 % File :CSE---1.7 % 116.87/117.06 % Problem :theBenchmark % 116.87/117.06 % Transform :cnf % 116.87/117.06 % Format :tptp:raw % 116.87/117.06 % Command :java -jar mcs_scs.jar %d %s % 116.87/117.06 % 116.87/117.06 % Result :Theorem 116.290000s % 116.87/117.06 % Output :CNFRefutation 116.290000s % 116.87/117.06 %------------------------------------------- % 116.93/117.08 %-------------------------------------------------------------------------- % 116.93/117.08 % File : SYN565-1 : TPTP v8.2.0. Released v2.5.0. % 116.93/117.08 % Domain : Syntactic % 116.93/117.08 % Problem : Harrison problem 2889 % 116.93/117.08 % Version : Especial. % 116.93/117.08 % English : % 116.93/117.08 % 116.93/117.08 % Refs : [Har01] Email to G. Sutcliffe % 116.93/117.08 % Source : [Har01] % 116.93/117.08 % Names : % 116.93/117.08 % 116.93/117.08 % Status : Unsatisfiable % 116.93/117.08 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.00 v5.4.0, 0.11 v5.3.0, 0.25 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.00 v2.5.0 % 116.93/117.08 % Syntax : Number of clauses : 18 ( 7 unt; 0 nHn; 12 RR) % 116.93/117.08 % Number of literals : 37 ( 0 equ; 20 neg) % 116.93/117.08 % Maximal clause size : 4 ( 2 avg) % 116.93/117.08 % Maximal term depth : 4 ( 1 avg) % 116.93/117.08 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty) % 116.93/117.08 % Number of functors : 8 ( 8 usr; 2 con; 0-2 aty) % 116.93/117.08 % Number of variables : 45 ( 0 sgn) % 116.93/117.08 % SPC : CNF_UNS_RFO_NEQ_HRN % 116.93/117.08 % 116.93/117.08 % Comments : % 116.93/117.08 %-------------------------------------------------------------------------- % 116.93/117.08 cnf(p2_1,negated_conjecture, % 116.93/117.08 p2(X9,X9) ). % 116.93/117.08 % 116.93/117.08 cnf(p4_2,negated_conjecture, % 116.93/117.08 p4(X23,X23) ). % 116.93/117.08 % 116.93/117.08 cnf(p2_3,negated_conjecture, % 116.93/117.08 p2(f5(f7(X18)),f5(X18)) ). % 116.93/117.08 % 116.93/117.08 cnf(p4_4,negated_conjecture, % 116.93/117.08 p4(f8(X38,X39),f6(X38,f7(X39))) ). % 116.93/117.08 % 116.93/117.08 cnf(p4_5,negated_conjecture, % 116.93/117.08 p4(f7(f8(X32,X33)),f8(X33,X32)) ). % 116.93/117.08 % 116.93/117.08 cnf(p2_6,negated_conjecture, % 116.93/117.08 ( p2(f5(X16),f5(X17)) % 116.93/117.08 | ~ p4(X16,X17) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p4_7,negated_conjecture, % 116.93/117.08 ( p4(f7(X30),f7(X31)) % 116.93/117.08 | ~ p4(X30,X31) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p2_8,negated_conjecture, % 116.93/117.08 ( p2(X10,X11) % 116.93/117.08 | ~ p2(X9,X10) % 116.93/117.08 | ~ p2(X9,X11) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p4_9,negated_conjecture, % 116.93/117.08 ( p4(X24,X25) % 116.93/117.08 | ~ p4(X23,X24) % 116.93/117.08 | ~ p4(X23,X25) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p10_10,negated_conjecture, % 116.93/117.08 p10(f5(X7),f3(f5(f6(X7,X8)),f5(X8))) ). % 116.93/117.08 % 116.93/117.08 cnf(not_p10_11,negated_conjecture, % 116.93/117.08 ~ p10(f9(f5(c11),f5(c12)),f5(f8(c12,c11))) ). % 116.93/117.08 % 116.93/117.08 cnf(p10_12,negated_conjecture, % 116.93/117.08 ( p10(X4,f3(X5,X6)) % 116.93/117.08 | ~ p10(f9(X4,X6),X5) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p10_13,negated_conjecture, % 116.93/117.08 ( p10(f9(X4,X6),X5) % 116.93/117.08 | ~ p10(X4,f3(X5,X6)) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p10_14,negated_conjecture, % 116.93/117.08 ( p10(X0,X1) % 116.93/117.08 | ~ p2(X2,X0) % 116.93/117.08 | ~ p2(X3,X1) % 116.93/117.08 | ~ p10(X2,X3) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p4_15,negated_conjecture, % 116.93/117.08 ( p4(f8(X34,X35),f8(X36,X37)) % 116.93/117.08 | ~ p4(X34,X36) % 116.93/117.08 | ~ p4(X35,X37) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p2_16,negated_conjecture, % 116.93/117.08 ( p2(f3(X12,X13),f3(X14,X15)) % 116.93/117.08 | ~ p2(X12,X14) % 116.93/117.08 | ~ p2(X13,X15) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p2_17,negated_conjecture, % 116.93/117.08 ( p2(f9(X19,X20),f9(X21,X22)) % 116.93/117.08 | ~ p2(X19,X21) % 116.93/117.08 | ~ p2(X20,X22) ) ). % 116.93/117.08 % 116.93/117.08 cnf(p4_18,negated_conjecture, % 116.93/117.08 ( p4(f6(X26,X27),f6(X28,X29)) % 116.93/117.08 | ~ p4(X26,X28) % 116.93/117.08 | ~ p4(X27,X29) ) ). % 116.93/117.08 % 116.93/117.08 %-------------------------------------------------------------------------- % 116.93/117.08 %------------------------------------------- % 116.93/117.08 % Proof found % 116.93/117.08 % SZS status Theorem for theBenchmark % 116.93/117.08 % SZS output start Proof % 116.93/117.10 %ClaNum:18(EqnAxiom:0) % 116.93/117.10 %VarNum:90(SingletonVarNum:45) % 116.93/117.10 %MaxLitNum:4 % 116.93/117.10 %MaxfuncDepth:2 % 116.93/117.10 %SharedTerms:8 % 116.93/117.10 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 % 116.93/117.10 %singleGoalClaCount:7 % 116.93/117.10 [7]~P2(f8(f2(a4),f2(a5)),f2(f7(a5,a4))) % 116.93/117.10 [1]P1(x11,x11) % 116.93/117.10 [2]P3(x21,x21) % 116.93/117.10 [3]P1(f2(f1(x31)),f2(x31)) % 116.93/117.10 [4]P3(f7(x41,x42),f6(x41,f1(x42))) % 116.93/117.10 [5]P3(f1(f7(x51,x52)),f7(x52,x51)) % 116.93/117.10 [6]P2(f2(x61),f3(f2(f6(x61,x62)),f2(x62))) % 116.93/117.10 [8]~P3(x81,x82)+P1(f2(x81),f2(x82)) % 116.93/117.10 [9]~P3(x91,x92)+P3(f1(x91),f1(x92)) % 116.93/117.10 [13]~P2(f8(x131,x133),x132)+P2(x131,f3(x132,x133)) % 116.93/117.10 [14]~P2(x141,f3(x143,x142))+P2(f8(x141,x142),x143) % 116.93/117.10 [10]~P1(x103,x101)+P1(x101,x102)+~P1(x103,x102) % 116.93/117.10 [11]~P3(x113,x111)+P3(x111,x112)+~P3(x113,x112) % 116.93/117.10 [15]~P1(x152,x154)+~P1(x151,x153)+P1(f3(x151,x152),f3(x153,x154)) % 116.93/117.10 [16]~P1(x162,x164)+~P1(x161,x163)+P1(f8(x161,x162),f8(x163,x164)) % 116.93/117.10 [17]~P3(x172,x174)+~P3(x171,x173)+P3(f7(x171,x172),f7(x173,x174)) % 116.93/117.10 [18]~P3(x182,x184)+~P3(x181,x183)+P3(f6(x181,x182),f6(x183,x184)) % 116.93/117.10 [12]~P2(x124,x123)+P2(x121,x122)+~P1(x123,x122)+~P1(x124,x121) % 116.93/117.10 %EqnAxiom % 116.93/117.10 % 116.93/117.10 %------------------------------------------- % 116.93/117.12 cnf(19,plain, % 116.93/117.12 (~P2(f2(a4),f3(f2(f7(a5,a4)),f2(a5)))), % 116.93/117.12 inference(scs_inference,[],[7,14])). % 116.93/117.12 cnf(23,plain, % 116.93/117.12 (P3(f6(x231,f1(x232)),f7(x231,x232))), % 116.93/117.12 inference(scs_inference,[],[4,2,11])). % 116.93/117.12 cnf(28,plain, % 116.93/117.12 (P1(f2(f1(f6(x281,f1(x282)))),f2(f1(f7(x281,x282))))), % 116.93/117.12 inference(scs_inference,[],[23,8,9])). % 116.93/117.12 cnf(29,plain, % 116.93/117.12 (P1(f2(x291),f2(f1(x291)))), % 116.93/117.12 inference(scs_inference,[],[3,1,10])). % 116.93/117.12 cnf(34,plain, % 116.93/117.12 (~P2(f8(f2(f1(a4)),f2(a5)),f2(f7(a5,a4)))), % 116.93/117.12 inference(scs_inference,[],[1,3,19,13,12])). % 116.93/117.12 cnf(35,plain, % 116.93/117.12 (~P2(f2(f1(a4)),f3(f2(f7(a5,a4)),f2(a5)))), % 116.93/117.12 inference(scs_inference,[],[34,14])). % 116.93/117.12 cnf(37,plain, % 116.93/117.12 (P2(f2(f1(x371)),f3(f2(f6(x371,x372)),f2(x372)))), % 116.93/117.12 inference(scs_inference,[],[1,29,6,12])). % 116.93/117.12 cnf(43,plain, % 116.93/117.12 (P3(f7(x431,x432),f1(f7(x432,x431)))), % 116.93/117.12 inference(scs_inference,[],[5,2,11])). % 116.93/117.12 cnf(55,plain, % 116.93/117.12 (~P2(f8(f2(a4),f2(a5)),f2(f1(f7(a5,a4))))), % 116.93/117.12 inference(scs_inference,[],[19,3,1,13,12])). % 116.93/117.12 cnf(58,plain, % 116.93/117.12 (~P1(f8(f2(f1(x581)),f2(x582)),x583)+P2(x583,f2(f6(x581,x582)))), % 116.93/117.12 inference(scs_inference,[],[37,1,14,12])). % 116.93/117.12 cnf(60,plain, % 116.93/117.12 (P2(f8(f2(f1(x601)),f2(x602)),f2(f6(x601,x602)))), % 116.93/117.12 inference(scs_inference,[],[1,58,10])). % 116.93/117.12 cnf(61,plain, % 116.93/117.12 (P1(f8(f2(x611),f2(f1(x611))),f8(f2(x611),f2(x611)))), % 116.93/117.12 inference(scs_inference,[],[3,16,10])). % 116.93/117.12 cnf(68,plain, % 116.93/117.12 (P3(f7(f6(x681,f1(x682)),f7(x681,x682)),f7(f7(x681,x682),f7(x681,x682)))), % 116.93/117.12 inference(scs_inference,[],[23,17,11])). % 116.93/117.12 cnf(71,plain, % 116.93/117.12 (P3(f6(f6(x711,f1(x712)),f7(x711,x712)),f6(f7(x711,x712),f7(x711,x712)))), % 116.93/117.12 inference(scs_inference,[],[23,18,11])). % 116.93/117.12 cnf(73,plain, % 116.93/117.12 (P3(f7(f7(x731,x732),f7(x731,x732)),f7(f6(x731,f1(x732)),f7(x731,x732)))), % 116.93/117.12 inference(scs_inference,[],[68,2,11])). % 116.93/117.12 cnf(88,plain, % 116.93/117.12 (~P1(x881,f8(f2(f1(a4)),f2(a5)))+~P2(x881,f2(f7(a5,a4)))), % 116.93/117.12 inference(scs_inference,[],[35,1,13,12])). % 116.93/117.12 cnf(91,plain, % 116.93/117.12 (~P2(f8(f2(f1(a4)),f2(f1(a5))),f2(f7(a5,a4)))), % 116.93/117.12 inference(scs_inference,[],[1,3,16,88])). % 116.93/117.12 cnf(101,plain, % 116.93/117.12 (P2(f8(f2(f1(x1011)),f2(x1012)),f2(f1(f6(x1011,x1012))))), % 116.93/117.12 inference(scs_inference,[],[37,29,1,14,12])). % 116.93/117.12 cnf(109,plain, % 116.93/117.12 (~P2(f2(f1(f1(a4))),f3(f2(f7(a5,a4)),f2(a5)))), % 116.93/117.12 inference(scs_inference,[],[34,1,3,14,12])). % 116.93/117.12 cnf(143,plain, % 116.93/117.12 (P3(f6(f1(f7(x1431,x1432)),f7(x1432,x1431)),f6(f7(x1432,x1431),f7(x1432,x1431)))), % 116.93/117.12 inference(scs_inference,[],[5,18,11])). % 116.93/117.12 cnf(144,plain, % 116.93/117.12 (P3(f6(f7(x1441,x1442),f7(x1441,x1442)),f6(f1(f7(x1442,x1441)),f7(x1441,x1442)))), % 116.93/117.12 inference(scs_inference,[],[143,2,11])). % 116.93/117.12 cnf(162,plain, % 116.93/117.12 (~P1(f2(f6(x1621,x1622)),f2(f7(a5,a4)))+~P1(f8(f2(f1(x1621)),f2(x1622)),f8(f2(a4),f2(a5)))), % 116.93/117.12 inference(scs_inference,[],[7,60,12])). % 116.93/117.12 cnf(220,plain, % 116.93/117.12 (~P1(f8(f2(f1(x2201)),f2(x2202)),f8(f2(a4),f2(a5)))+~P1(f2(f7(a5,a4)),f2(f6(x2201,x2202)))), % 116.93/117.12 inference(scs_inference,[],[1,162,10])). % 116.93/117.12 cnf(223,plain, % 116.93/117.12 (~P1(f8(f2(a4),f2(a5)),f8(f2(f1(x2231)),f2(x2232)))+~P1(f2(f6(x2231,x2232)),f2(f7(a5,a4)))), % 116.93/117.12 inference(scs_inference,[],[1,162,10])). % 116.93/117.12 cnf(260,plain, % 116.93/117.12 (P2(f2(f6(f7(x2601,x2602),f7(x2601,x2602))),f3(f2(f6(f6(f6(x2601,f1(x2602)),f7(x2601,x2602)),x2603)),f2(x2603)))), % 116.93/117.12 inference(scs_inference,[],[71,6,1,8,12])). % 116.93/117.12 cnf(271,plain, % 116.93/117.12 (~P1(f2(f1(x2711)),f2(a4))+~P1(f2(f7(a5,a4)),f2(f6(x2711,f1(a5))))), % 116.93/117.12 inference(scs_inference,[],[3,220,16])). % 116.93/117.12 cnf(290,plain, % 116.93/117.12 (P2(f2(f6(f1(f7(x2901,x2902)),f7(x2902,x2901))),f3(f2(f6(f6(f7(x2902,x2901),f7(x2902,x2901)),x2903)),f2(x2903)))), % 116.93/117.12 inference(scs_inference,[],[144,6,1,8,12])). % 116.93/117.12 cnf(291,plain, % 116.93/117.12 (P2(f8(f2(f1(x2911)),f2(f1(x2912))),f2(f7(x2911,x2912)))), % 116.93/117.12 inference(scs_inference,[],[23,60,1,8,12])). % 116.93/117.12 cnf(335,plain, % 116.93/117.12 (P1(f8(f2(f1(x3351)),f2(x3351)),f8(f2(f1(x3351)),f2(f1(x3351))))), % 116.93/117.12 inference(scs_inference,[],[29,16,10])). % 116.93/117.12 cnf(355,plain, % 116.93/117.12 (~P1(f2(a4),f2(f1(x3551)))+~P1(f2(f6(x3551,f1(a5))),f2(f7(a5,a4)))), % 116.93/117.12 inference(scs_inference,[],[29,223,16])). % 116.93/117.12 cnf(1292,plain, % 116.93/117.12 (P2(f2(f6(f7(x12921,x12922),f7(x12921,x12922))),f3(f2(f6(f6(f1(f7(x12922,x12921)),f7(x12921,x12922)),x12923)),f2(x12923)))), % 116.93/117.12 inference(scs_inference,[],[143,6,1,8,12])). % 116.93/117.12 cnf(1299,plain, % 116.93/117.12 (~P1(f2(f7(a5,a4)),f2(f6(a4,f1(a5))))), % 116.93/117.12 inference(scs_inference,[],[3,271])). % 116.93/117.12 cnf(1305,plain, % 116.93/117.12 (~P2(f8(f2(f1(f1(a4))),f2(a5)),f2(f7(a5,a4)))), % 116.93/117.12 inference(scs_inference,[],[109,29,3,271,355,13])). % 116.93/117.12 cnf(1348,plain, % 116.93/117.12 (P1(f3(f2(x13481),f2(x13481)),f3(f2(f1(x13481)),f2(f1(x13481))))), % 116.93/117.12 inference(scs_inference,[],[1299,91,73,29,8,14,17,15])). % 116.93/117.12 cnf(1354,plain, % 116.93/117.12 (P2(f8(f2(f1(x13541)),f2(f1(x13541))),f2(f1(f7(x13541,f1(x13541)))))), % 116.93/117.12 inference(scs_inference,[],[61,1299,91,101,28,73,29,8,14,17,15,16,18,12])). % 116.93/117.12 cnf(1409,plain, % 116.93/117.12 (~P1(f8(f2(f1(a5)),f2(f1(a4))),f8(f2(f1(f1(a4))),f2(a5)))), % 116.93/117.12 inference(scs_inference,[],[1305,1348,291,43,1,15,17,16,18,12])). % 116.93/117.12 cnf(1481,plain, % 116.93/117.12 (P2(f8(f2(f1(x14811)),f2(f1(x14811))),f2(f6(x14811,x14811)))), % 116.93/117.12 inference(scs_inference,[],[4,335,260,14,8,58])). % 116.93/117.12 cnf(1508,plain, % 116.93/117.12 (~P1(f8(f2(f1(a4)),f2(f1(a5))),f8(f2(a4),f2(a5)))), % 116.93/117.12 inference(scs_inference,[],[1,43,55,291,1409,1354,290,14,8,13,9,10,12])). % 116.93/117.12 cnf(1522,plain, % 116.93/117.12 (~P1(f2(f1(a4)),f2(a4))), % 116.93/117.12 inference(scs_inference,[],[3,71,1508,1481,1292,13,14,9,8,16])). % 116.93/117.12 cnf(1533,plain, % 116.93/117.12 ($false), % 116.93/117.12 inference(scs_inference,[],[1522,3]), % 116.93/117.12 ['proof']). % 116.93/117.12 % SZS output end Proof % 116.93/117.12 % Total time :116.290000s %------------------------------------------------------------------------------