%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN564-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 : n022.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.24s 116.70s % Output : CNFRefutation 116.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : SYN564-1 : TPTP v8.2.0. Released v2.5.0. % 0.09/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.36 % Computer : n022.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Sun Jun 23 20:47:54 EDT 2024 % 0.13/0.36 % CPUTime : % 0.22/0.59 start to proof:theBenchmark % 116.24/116.66 %------------------------------------------- % 116.24/116.66 % File :CSE---1.7 % 116.24/116.66 % Problem :theBenchmark % 116.24/116.66 % Transform :cnf % 116.24/116.66 % Format :tptp:raw % 116.24/116.66 % Command :java -jar mcs_scs.jar %d %s % 116.24/116.66 % 116.24/116.66 % Result :Theorem 115.630000s % 116.24/116.66 % Output :CNFRefutation 115.630000s % 116.24/116.66 %------------------------------------------- % 116.24/116.69 %-------------------------------------------------------------------------- % 116.24/116.69 % File : SYN564-1 : TPTP v8.2.0. Released v2.5.0. % 116.24/116.69 % Domain : Syntactic % 116.24/116.69 % Problem : Harrison problem 2888 % 116.24/116.69 % Version : Especial. % 116.24/116.69 % English : % 116.24/116.69 % 116.24/116.69 % Refs : [Har01] Email to G. Sutcliffe % 116.24/116.69 % Source : [Har01] % 116.24/116.69 % Names : % 116.24/116.69 % 116.24/116.69 % Status : Unsatisfiable % 116.24/116.69 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.11 v5.3.0, 0.25 v5.2.0, 0.00 v2.5.0 % 116.24/116.69 % Syntax : Number of clauses : 18 ( 7 unt; 0 nHn; 12 RR) % 116.24/116.70 % Number of literals : 37 ( 0 equ; 20 neg) % 116.24/116.70 % Maximal clause size : 4 ( 2 avg) % 116.24/116.70 % Maximal term depth : 4 ( 1 avg) % 116.24/116.70 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty) % 116.24/116.70 % Number of functors : 8 ( 8 usr; 2 con; 0-2 aty) % 116.24/116.70 % Number of variables : 45 ( 0 sgn) % 116.24/116.70 % SPC : CNF_UNS_RFO_NEQ_HRN % 116.24/116.70 % 116.24/116.70 % Comments : % 116.24/116.70 %-------------------------------------------------------------------------- % 116.24/116.70 cnf(p2_1,negated_conjecture, % 116.24/116.70 p2(X9,X9) ). % 116.24/116.70 % 116.24/116.70 cnf(p4_2,negated_conjecture, % 116.24/116.70 p4(X23,X23) ). % 116.24/116.70 % 116.24/116.70 cnf(p2_3,negated_conjecture, % 116.24/116.70 p2(f5(f7(X18)),f5(X18)) ). % 116.24/116.70 % 116.24/116.70 cnf(p4_4,negated_conjecture, % 116.24/116.70 p4(f8(X38,X39),f6(X38,f7(X39))) ). % 116.24/116.70 % 116.24/116.70 cnf(p4_5,negated_conjecture, % 116.24/116.70 p4(f7(f8(X32,X33)),f8(X33,X32)) ). % 116.24/116.70 % 116.24/116.70 cnf(p2_6,negated_conjecture, % 116.24/116.70 ( p2(f5(X16),f5(X17)) % 116.24/116.70 | ~ p4(X16,X17) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p4_7,negated_conjecture, % 116.24/116.70 ( p4(f7(X30),f7(X31)) % 116.24/116.70 | ~ p4(X30,X31) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p2_8,negated_conjecture, % 116.24/116.70 ( p2(X10,X11) % 116.24/116.70 | ~ p2(X9,X10) % 116.24/116.70 | ~ p2(X9,X11) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p4_9,negated_conjecture, % 116.24/116.70 ( p4(X24,X25) % 116.24/116.70 | ~ p4(X23,X24) % 116.24/116.70 | ~ p4(X23,X25) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p10_10,negated_conjecture, % 116.24/116.70 p10(f5(X7),f3(f5(f6(X7,X8)),f5(X8))) ). % 116.24/116.70 % 116.24/116.70 cnf(not_p10_11,negated_conjecture, % 116.24/116.70 ~ p10(f9(f5(c11),f5(c12)),f5(f8(c11,c12))) ). % 116.24/116.70 % 116.24/116.70 cnf(p10_12,negated_conjecture, % 116.24/116.70 ( p10(X4,f3(X5,X6)) % 116.24/116.70 | ~ p10(f9(X4,X6),X5) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p10_13,negated_conjecture, % 116.24/116.70 ( p10(f9(X4,X6),X5) % 116.24/116.70 | ~ p10(X4,f3(X5,X6)) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p10_14,negated_conjecture, % 116.24/116.70 ( p10(X0,X1) % 116.24/116.70 | ~ p2(X2,X0) % 116.24/116.70 | ~ p2(X3,X1) % 116.24/116.70 | ~ p10(X2,X3) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p4_15,negated_conjecture, % 116.24/116.70 ( p4(f8(X34,X35),f8(X36,X37)) % 116.24/116.70 | ~ p4(X34,X36) % 116.24/116.70 | ~ p4(X35,X37) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p2_16,negated_conjecture, % 116.24/116.70 ( p2(f3(X12,X13),f3(X14,X15)) % 116.24/116.70 | ~ p2(X12,X14) % 116.24/116.70 | ~ p2(X13,X15) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p2_17,negated_conjecture, % 116.24/116.70 ( p2(f9(X19,X20),f9(X21,X22)) % 116.24/116.70 | ~ p2(X19,X21) % 116.24/116.70 | ~ p2(X20,X22) ) ). % 116.24/116.70 % 116.24/116.70 cnf(p4_18,negated_conjecture, % 116.24/116.70 ( p4(f6(X26,X27),f6(X28,X29)) % 116.24/116.70 | ~ p4(X26,X28) % 116.24/116.70 | ~ p4(X27,X29) ) ). % 116.24/116.70 % 116.24/116.70 %-------------------------------------------------------------------------- % 116.24/116.70 %------------------------------------------- % 116.24/116.70 % Proof found % 116.24/116.70 % SZS status Theorem for theBenchmark % 116.24/116.70 % SZS output start Proof % 116.32/116.72 %ClaNum:18(EqnAxiom:0) % 116.32/116.72 %VarNum:90(SingletonVarNum:45) % 116.32/116.72 %MaxLitNum:4 % 116.32/116.72 %MaxfuncDepth:2 % 116.32/116.72 %SharedTerms:8 % 116.32/116.72 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 % 116.32/116.72 %singleGoalClaCount:7 % 116.32/116.72 [7]~P2(f8(f2(a4),f2(a5)),f2(f7(a4,a5))) % 116.32/116.72 [1]P1(x11,x11) % 116.32/116.72 [2]P3(x21,x21) % 116.32/116.72 [3]P1(f2(f1(x31)),f2(x31)) % 116.32/116.72 [4]P3(f7(x41,x42),f6(x41,f1(x42))) % 116.32/116.72 [5]P3(f1(f7(x51,x52)),f7(x52,x51)) % 116.32/116.72 [6]P2(f2(x61),f3(f2(f6(x61,x62)),f2(x62))) % 116.32/116.72 [8]~P3(x81,x82)+P1(f2(x81),f2(x82)) % 116.32/116.72 [9]~P3(x91,x92)+P3(f1(x91),f1(x92)) % 116.32/116.72 [13]~P2(f8(x131,x133),x132)+P2(x131,f3(x132,x133)) % 116.32/116.72 [14]~P2(x141,f3(x143,x142))+P2(f8(x141,x142),x143) % 116.32/116.72 [10]~P1(x103,x101)+P1(x101,x102)+~P1(x103,x102) % 116.32/116.72 [11]~P3(x113,x111)+P3(x111,x112)+~P3(x113,x112) % 116.32/116.72 [15]~P1(x152,x154)+~P1(x151,x153)+P1(f3(x151,x152),f3(x153,x154)) % 116.32/116.72 [16]~P1(x162,x164)+~P1(x161,x163)+P1(f8(x161,x162),f8(x163,x164)) % 116.32/116.72 [17]~P3(x172,x174)+~P3(x171,x173)+P3(f7(x171,x172),f7(x173,x174)) % 116.32/116.72 [18]~P3(x182,x184)+~P3(x181,x183)+P3(f6(x181,x182),f6(x183,x184)) % 116.32/116.72 [12]~P2(x124,x123)+P2(x121,x122)+~P1(x123,x122)+~P1(x124,x121) % 116.32/116.72 %EqnAxiom % 116.32/116.72 % 116.32/116.72 %------------------------------------------- % 116.32/116.75 cnf(19,plain, % 116.32/116.75 (~P2(f2(a4),f3(f2(f7(a4,a5)),f2(a5)))), % 116.32/116.75 inference(scs_inference,[],[7,14])). % 116.32/116.75 cnf(23,plain, % 116.32/116.75 (P3(f6(x231,f1(x232)),f7(x231,x232))), % 116.32/116.75 inference(scs_inference,[],[4,2,11])). % 116.32/116.75 cnf(29,plain, % 116.32/116.75 (P1(f2(x291),f2(f1(x291)))), % 116.32/116.75 inference(scs_inference,[],[3,1,10])). % 116.32/116.75 cnf(34,plain, % 116.32/116.75 (~P2(f8(f2(f1(a4)),f2(a5)),f2(f7(a4,a5)))), % 116.32/116.75 inference(scs_inference,[],[1,3,19,13,12])). % 116.32/116.75 cnf(35,plain, % 116.32/116.75 (~P2(f2(f1(a4)),f3(f2(f7(a4,a5)),f2(a5)))), % 116.32/116.75 inference(scs_inference,[],[34,14])). % 116.32/116.75 cnf(37,plain, % 116.32/116.75 (P2(f2(f1(x371)),f3(f2(f6(x371,x372)),f2(x372)))), % 116.32/116.75 inference(scs_inference,[],[1,29,6,12])). % 116.32/116.75 cnf(56,plain, % 116.32/116.75 (~P1(x561,f8(f2(a4),f2(a5)))+~P2(x561,f2(f7(a4,a5)))), % 116.32/116.75 inference(scs_inference,[],[19,1,13,12])). % 116.32/116.75 cnf(58,plain, % 116.32/116.75 (~P1(f8(f2(f1(x581)),f2(x582)),x583)+P2(x583,f2(f6(x581,x582)))), % 116.32/116.75 inference(scs_inference,[],[37,1,14,12])). % 116.32/116.75 cnf(60,plain, % 116.32/116.75 (P2(f8(f2(f1(x601)),f2(x602)),f2(f6(x601,x602)))), % 116.32/116.75 inference(scs_inference,[],[1,58,10])). % 116.32/116.75 cnf(63,plain, % 116.32/116.75 (~P2(f8(f2(a4),f2(f1(a5))),f2(f7(a4,a5)))), % 116.32/116.75 inference(scs_inference,[],[1,3,16,56])). % 116.32/116.75 cnf(162,plain, % 116.32/116.75 (~P1(f2(f6(x1621,x1622)),f2(f7(a4,a5)))+~P1(f8(f2(f1(x1621)),f2(x1622)),f8(f2(a4),f2(a5)))), % 116.32/116.75 inference(scs_inference,[],[7,60,12])). % 116.32/116.75 cnf(213,plain, % 116.32/116.75 (~P1(f8(f2(f1(x2131)),f2(x2132)),f8(f2(a4),f2(a5)))+~P1(f2(f7(a4,a5)),f2(f6(x2131,x2132)))), % 116.32/116.75 inference(scs_inference,[],[1,162,10])). % 116.32/116.75 cnf(236,plain, % 116.32/116.75 (~P1(f2(f1(x2361)),f2(a4))+~P1(f2(f7(a4,a5)),f2(f6(x2361,f1(a5))))), % 116.32/116.75 inference(scs_inference,[],[3,213,16])). % 116.32/116.75 cnf(261,plain, % 116.32/116.75 (~P2(f8(f2(f1(a4)),f2(a5)),f2(f6(a4,f1(a5))))), % 116.32/116.75 inference(scs_inference,[],[23,34,1,8,12])). % 116.32/116.75 cnf(276,plain, % 116.32/116.75 (P2(f8(f2(x2761),f2(x2762)),f2(f6(x2761,x2762)))), % 116.32/116.75 inference(scs_inference,[],[6,14])). % 116.32/116.75 cnf(282,plain, % 116.32/116.75 (~P1(f8(f2(x2821),f2(x2822)),x2823)+P2(x2823,f2(f6(x2821,x2822)))), % 116.32/116.75 inference(scs_inference,[],[276,1,12])). % 116.32/116.75 cnf(316,plain, % 116.32/116.75 (~P1(f3(f2(f6(f1(a4),x3161)),f2(x3161)),f3(f2(f7(a4,a5)),f2(a5)))), % 116.32/116.75 inference(scs_inference,[],[276,19,3,13,12])). % 116.32/116.75 cnf(317,plain, % 116.32/116.75 (~P1(f2(f1(x3171)),f2(a4))+~P1(f2(f6(x3171,f1(a5))),f2(f7(a4,a5)))), % 116.32/116.75 inference(scs_inference,[],[3,162,16])). % 116.32/116.75 cnf(338,plain, % 116.32/116.75 (~P1(f2(f6(f1(a4),a5)),f2(f7(a4,a5)))), % 116.32/116.75 inference(scs_inference,[],[35,276,1,13,12])). % 116.32/116.75 cnf(373,plain, % 116.32/116.75 (~P1(f8(f2(a4),f2(f1(a5))),f8(f2(a4),f2(a5)))), % 116.32/116.75 inference(scs_inference,[],[23,276,7,8,12])). % 116.32/116.75 cnf(2021,plain, % 116.32/116.75 (P1(f2(f1(x20211)),f2(x20211))), % 116.32/116.75 inference(rename_variables,[],[3])). % 116.32/116.75 cnf(2024,plain, % 116.32/116.75 (P1(f2(f1(x20241)),f2(x20241))), % 116.32/116.75 inference(rename_variables,[],[3])). % 116.32/116.75 cnf(2034,plain, % 116.32/116.75 (P1(f2(f1(x20341)),f2(x20341))), % 116.32/116.75 inference(rename_variables,[],[3])). % 116.32/116.75 cnf(2036,plain, % 116.32/116.75 ($false), % 116.32/116.75 inference(scs_inference,[],[63,338,373,261,316,3,2021,2024,2034,1,236,317,282,14,8,15,16]), % 116.32/116.75 ['proof']). % 116.32/116.75 % SZS output end Proof % 116.32/116.75 % Total time :115.630000s %------------------------------------------------------------------------------