%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN572-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 : n020.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:00 EDT 2024 % Result : Unsatisfiable 83.36s 83.42s % Output : CNFRefutation 83.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN572-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 : n020.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 23:01:08 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 83.36/83.40 %------------------------------------------- % 83.36/83.40 % File :CSE---1.7 % 83.36/83.40 % Problem :theBenchmark % 83.36/83.40 % Transform :cnf % 83.36/83.40 % Format :tptp:raw % 83.36/83.40 % Command :java -jar mcs_scs.jar %d %s % 83.36/83.40 % 83.36/83.40 % Result :Theorem 82.790000s % 83.36/83.40 % Output :CNFRefutation 82.790000s % 83.36/83.40 %------------------------------------------- % 83.36/83.41 %-------------------------------------------------------------------------- % 83.36/83.42 % File : SYN572-1 : TPTP v8.2.0. Released v2.5.0. % 83.36/83.42 % Domain : Syntactic % 83.36/83.42 % Problem : Harrison problem 3112 % 83.36/83.42 % Version : Especial. % 83.36/83.42 % English : % 83.36/83.42 % 83.36/83.42 % Refs : [Har01] Email to G. Sutcliffe % 83.36/83.42 % Source : [Har01] % 83.36/83.42 % Names : % 83.36/83.42 % 83.36/83.42 % Status : Unsatisfiable % 83.36/83.42 % Rating : 0.09 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.2.0, 0.17 v6.1.0, 0.21 v6.0.0, 0.33 v5.5.0, 0.25 v5.4.0, 0.33 v5.3.0, 0.45 v5.2.0, 0.23 v5.1.0, 0.25 v5.0.0, 0.33 v4.0.1, 0.29 v4.0.0, 0.14 v3.4.0, 0.20 v3.3.0, 0.00 v2.7.0, 0.25 v2.6.0, 0.67 v2.5.0 % 83.36/83.42 % Syntax : Number of clauses : 20 ( 9 unt; 0 nHn; 12 RR) % 83.36/83.42 % Number of literals : 38 ( 0 equ; 19 neg) % 83.36/83.42 % Maximal clause size : 4 ( 1 avg) % 83.36/83.42 % Maximal term depth : 5 ( 1 avg) % 83.36/83.42 % Number of predicates : 4 ( 4 usr; 0 prp; 2-2 aty) % 83.36/83.42 % Number of functors : 10 ( 10 usr; 3 con; 0-2 aty) % 83.36/83.42 % Number of variables : 42 ( 0 sgn) % 83.36/83.42 % SPC : CNF_UNS_RFO_NEQ_HRN % 83.36/83.42 % 83.36/83.42 % Comments : % 83.36/83.42 %-------------------------------------------------------------------------- % 83.36/83.42 cnf(p2_1,negated_conjecture, % 83.36/83.42 p2(X6,X6) ). % 83.36/83.42 % 83.36/83.42 cnf(p6_2,negated_conjecture, % 83.36/83.42 p6(X34,X34) ). % 83.36/83.42 % 83.36/83.42 cnf(p4_3,negated_conjecture, % 83.36/83.42 p4(X22,X22) ). % 83.36/83.42 % 83.36/83.42 cnf(p4_4,negated_conjecture, % 83.36/83.42 p4(f10(f9(X27)),f10(X27)) ). % 83.36/83.42 % 83.36/83.42 cnf(p2_5,negated_conjecture, % 83.36/83.42 p2(f3(X13,f5(f7(f8(c13)))),X13) ). % 83.36/83.42 % 83.36/83.42 cnf(p6_6,negated_conjecture, % 83.36/83.42 ( p6(f8(X37),f8(X38)) % 83.36/83.42 | ~ p6(X37,X38) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p2_7,negated_conjecture, % 83.36/83.42 ( p2(f5(X18),f5(X19)) % 83.36/83.42 | ~ p4(X18,X19) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p2_8,negated_conjecture, % 83.36/83.42 ( p2(f9(X20),f9(X21)) % 83.36/83.42 | ~ p2(X20,X21) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p4_9,negated_conjecture, % 83.36/83.42 ( p4(f10(X25),f10(X26)) % 83.36/83.42 | ~ p2(X25,X26) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p4_10,negated_conjecture, % 83.36/83.42 ( p4(f7(X32),f7(X33)) % 83.36/83.42 | ~ p6(X32,X33) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p2_11,negated_conjecture, % 83.36/83.42 p2(f3(X14,f9(X14)),f5(f7(f8(c13)))) ). % 83.36/83.42 % 83.36/83.42 cnf(p2_12,negated_conjecture, % 83.36/83.42 ( p2(X7,X8) % 83.36/83.42 | ~ p2(X6,X7) % 83.36/83.42 | ~ p2(X6,X8) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p6_13,negated_conjecture, % 83.36/83.42 ( p6(X35,X36) % 83.36/83.42 | ~ p6(X34,X35) % 83.36/83.42 | ~ p6(X34,X36) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p4_14,negated_conjecture, % 83.36/83.42 ( p4(X23,X24) % 83.36/83.42 | ~ p4(X22,X23) % 83.36/83.42 | ~ p4(X22,X24) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p12_15,negated_conjecture, % 83.36/83.42 p12(f10(f3(X4,X5)),f11(f10(X4),f10(X5))) ). % 83.36/83.42 % 83.36/83.42 cnf(not_p12_16,negated_conjecture, % 83.36/83.42 ~ p12(f10(c14),f11(f10(f3(c14,c15)),f10(c15))) ). % 83.36/83.42 % 83.36/83.42 cnf(p2_17,negated_conjecture, % 83.36/83.42 p2(f3(X15,f3(X16,X17)),f3(f3(X15,X16),X17)) ). % 83.36/83.42 % 83.36/83.42 cnf(p12_18,negated_conjecture, % 83.36/83.42 ( p12(X0,X1) % 83.36/83.42 | ~ p4(X2,X0) % 83.36/83.42 | ~ p4(X3,X1) % 83.36/83.42 | ~ p12(X2,X3) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p4_19,negated_conjecture, % 83.36/83.42 ( p4(f11(X28,X29),f11(X30,X31)) % 83.36/83.42 | ~ p4(X28,X30) % 83.36/83.42 | ~ p4(X29,X31) ) ). % 83.36/83.42 % 83.36/83.42 cnf(p2_20,negated_conjecture, % 83.36/83.42 ( p2(f3(X9,X10),f3(X11,X12)) % 83.36/83.42 | ~ p2(X9,X11) % 83.36/83.42 | ~ p2(X10,X12) ) ). % 83.36/83.42 % 83.36/83.42 %-------------------------------------------------------------------------- % 83.36/83.42 %------------------------------------------- % 83.36/83.42 % Proof found % 83.36/83.42 % SZS status Theorem for theBenchmark % 83.36/83.42 % SZS output start Proof % 83.36/83.43 %ClaNum:20(EqnAxiom:0) % 83.36/83.43 %VarNum:84(SingletonVarNum:42) % 83.36/83.43 %MaxLitNum:4 % 83.36/83.43 %MaxfuncDepth:4 % 83.36/83.43 %SharedTerms:12 % 83.36/83.43 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 % 83.36/83.43 %singleGoalClaCount:9 % 83.36/83.43 [9]~P2(f2(a4),f7(f2(f6(a4,a5)),f2(a5))) % 83.36/83.43 [1]P1(x11,x11) % 83.36/83.43 [2]P3(x21,x21) % 83.36/83.43 [3]P4(x31,x31) % 83.36/83.43 [4]P4(f2(f1(x41)),f2(x41)) % 83.36/83.43 [5]P1(f6(x51,f1(x51)),f10(f9(f8(a3)))) % 83.36/83.43 [6]P1(f6(x61,f10(f9(f8(a3)))),x61) % 83.36/83.43 [7]P2(f2(f6(x71,x72)),f7(f2(x71),f2(x72))) % 83.36/83.43 [8]P1(f6(x81,f6(x82,x83)),f6(f6(x81,x82),x83)) % 83.36/83.43 [10]~P1(x101,x102)+P1(f1(x101),f1(x102)) % 83.36/83.43 [11]~P4(x111,x112)+P1(f10(x111),f10(x112)) % 83.36/83.43 [12]~P3(x121,x122)+P3(f8(x121),f8(x122)) % 83.36/83.43 [13]~P1(x131,x132)+P4(f2(x131),f2(x132)) % 83.36/83.43 [14]~P3(x141,x142)+P4(f9(x141),f9(x142)) % 83.36/83.43 [15]~P1(x153,x151)+P1(x151,x152)+~P1(x153,x152) % 83.36/83.43 [16]~P3(x163,x161)+P3(x161,x162)+~P3(x163,x162) % 83.36/83.43 [17]~P4(x173,x171)+P4(x171,x172)+~P4(x173,x172) % 83.36/83.43 [19]~P1(x192,x194)+~P1(x191,x193)+P1(f6(x191,x192),f6(x193,x194)) % 83.36/83.43 [20]~P4(x202,x204)+~P4(x201,x203)+P4(f7(x201,x202),f7(x203,x204)) % 83.36/83.43 [18]~P2(x184,x183)+P2(x181,x182)+~P4(x183,x182)+~P4(x184,x181) % 83.36/83.43 %EqnAxiom % 83.36/83.43 % 83.36/83.43 %------------------------------------------- % 83.36/83.44 cnf(23,plain, % 83.36/83.44 (P4(f2(x231),f2(f1(x231)))), % 83.36/83.44 inference(scs_inference,[],[4,3,17])). % 83.36/83.44 cnf(43,plain, % 83.36/83.44 (P1(f10(f9(f8(a3))),f6(x431,f1(x431)))), % 83.36/83.44 inference(scs_inference,[],[5,1,15])). % 83.36/83.44 cnf(47,plain, % 83.36/83.44 (P1(x471,f6(x471,f10(f9(f8(a3)))))), % 83.36/83.44 inference(scs_inference,[],[6,1,15])). % 83.36/83.44 cnf(50,plain, % 83.36/83.44 (P1(f6(f6(x501,x502),x503),f6(x501,f6(x502,x503)))), % 83.36/83.44 inference(scs_inference,[],[8,1,15])). % 83.36/83.45 cnf(1998,plain, % 83.36/83.45 (P4(f2(f6(f6(x19981,x19982),x19983)),f2(f6(x19981,f6(x19982,x19983))))), % 83.36/83.45 inference(scs_inference,[],[50,4,11,10,13])). % 83.36/83.45 cnf(2022,plain, % 83.36/83.45 (P4(f2(f6(x20221,f6(x20222,x20223))),f2(f6(f6(x20221,x20222),x20223)))), % 83.36/83.45 inference(scs_inference,[],[8,10,13])). % 83.36/83.45 cnf(2057,plain, % 83.36/83.45 (~P4(x20571,f7(f2(f6(a4,a5)),f2(a5)))+~P2(f2(a4),x20571)), % 83.36/83.45 inference(scs_inference,[],[3,9,18])). % 83.36/83.45 cnf(2067,plain, % 83.36/83.45 (P4(f7(f2(f1(x20671)),x20672),f7(f2(x20671),x20672))), % 83.36/83.45 inference(scs_inference,[],[4,3,20])). % 83.36/83.45 cnf(2069,plain, % 83.36/83.45 (~P2(f2(a4),f7(f2(f1(f6(a4,a5))),f2(a5)))), % 83.36/83.45 inference(scs_inference,[],[4,3,20,2057])). % 83.36/83.45 cnf(2076,plain, % 83.36/83.45 (P4(f7(x20761,f2(f1(x20762))),f7(x20761,f2(x20762)))), % 83.36/83.45 inference(scs_inference,[],[4,2067,3,11,20])). % 83.36/83.45 cnf(2085,plain, % 83.36/83.45 (~P2(f2(f1(a4)),f7(f2(f1(f6(a4,a5))),f2(f1(a5))))), % 83.36/83.45 inference(scs_inference,[],[4,2076,2069,11,18])). % 83.36/83.45 cnf(2106,plain, % 83.36/83.45 (~P2(f2(a4),f7(f2(f6(a4,a5)),f2(f1(a5))))), % 83.36/83.45 inference(scs_inference,[],[4,2085,2076,3,18,2057])). % 83.36/83.45 cnf(2109,plain, % 83.36/83.45 (~P2(f2(f1(a4)),f7(f2(f6(a4,a5)),f2(f1(f1(a5)))))), % 83.36/83.45 inference(scs_inference,[],[4,2106,2076,18])). % 83.36/83.45 cnf(2137,plain, % 83.36/83.45 (P1(f6(f6(x21371,f1(x21371)),x21372),f6(f10(f9(f8(a3))),x21372))), % 83.36/83.45 inference(scs_inference,[],[5,1,19])). % 83.36/83.45 cnf(2146,plain, % 83.36/83.45 (~P2(f2(f1(a4)),f7(f2(f1(f6(a4,a5))),f2(f1(f1(a5)))))), % 83.36/83.45 inference(scs_inference,[],[2109,2137,2067,6,3,15,18])). % 83.36/83.45 cnf(2185,plain, % 83.36/83.45 (P4(f7(f2(x21851),x21852),f7(f2(f1(x21851)),x21852))), % 83.36/83.45 inference(scs_inference,[],[23,3,20])). % 83.36/83.45 cnf(2192,plain, % 83.36/83.45 (P4(f7(x21921,f2(x21922)),f7(x21921,f2(f1(x21922))))), % 83.36/83.45 inference(scs_inference,[],[23,3,20])). % 83.36/83.45 cnf(2221,plain, % 83.36/83.45 (~P2(f2(a4),f7(f2(f6(a4,a5)),f2(f1(f1(a5)))))), % 83.36/83.45 inference(scs_inference,[],[23,2146,2185,18])). % 83.36/83.45 cnf(2258,plain, % 83.36/83.45 (P1(f6(x22581,f10(f9(f8(a3)))),f6(x22581,f6(x22582,f1(x22582))))), % 83.36/83.45 inference(scs_inference,[],[43,1,19])). % 83.36/83.45 cnf(2269,plain, % 83.36/83.45 (P1(f6(f6(f6(x22691,x22692),x22693),x22694),f6(f6(x22691,f6(x22692,x22693)),x22694))), % 83.36/83.45 inference(scs_inference,[],[50,1,19])). % 83.36/83.45 cnf(2271,plain, % 83.36/83.45 (P1(f6(x22711,f6(x22712,x22713)),f6(f6(f6(x22711,x22712),x22713),f10(f9(f8(a3)))))), % 83.36/83.45 inference(scs_inference,[],[50,47,1,19,15])). % 83.36/83.45 cnf(2440,plain, % 83.36/83.45 (P1(x24401,f6(x24401,f6(x24402,f1(x24402))))), % 83.36/83.45 inference(scs_inference,[],[2258,6,15])). % 83.36/83.45 cnf(2445,plain, % 83.36/83.45 (P4(f2(x24451),f2(f6(x24451,f6(x24452,f1(x24452)))))), % 83.36/83.45 inference(scs_inference,[],[2258,6,15,10,13])). % 83.36/83.45 cnf(2448,plain, % 83.36/83.45 (P4(f2(f6(x24481,f6(x24482,f1(x24482)))),f2(x24481))), % 83.36/83.45 inference(scs_inference,[],[2445,3,17])). % 83.36/83.45 cnf(2451,plain, % 83.36/83.45 (P1(f6(x24511,f6(x24512,f1(x24512))),x24511)), % 83.36/83.45 inference(scs_inference,[],[2258,2445,6,3,17,15])). % 83.36/83.45 cnf(2457,plain, % 83.36/83.45 (P1(x24571,f6(f6(x24571,f6(x24572,f1(x24572))),f6(x24573,f1(x24573))))), % 83.36/83.45 inference(scs_inference,[],[2440,2451,15])). % 83.36/83.45 cnf(2460,plain, % 83.36/83.45 (~P2(f2(f6(a4,f6(x24601,f1(x24601)))),f7(f2(f6(a4,a5)),f2(f1(a5))))), % 83.36/83.45 inference(scs_inference,[],[2440,2451,2448,2221,2192,15,18])). % 83.36/83.45 cnf(2469,plain, % 83.36/83.45 (P1(f6(f6(f6(x24691,f6(x24692,f1(x24692))),f6(x24693,f1(x24693))),f6(x24694,f1(x24694))),x24691)), % 83.36/83.45 inference(scs_inference,[],[2457,2451,15])). % 83.36/83.45 cnf(2473,plain, % 83.36/83.45 (P1(x24731,f6(f6(f6(x24731,x24732),f1(x24732)),f10(f9(f8(a3)))))), % 83.36/83.45 inference(scs_inference,[],[2271,2451,15])). % 83.36/83.45 cnf(2503,plain, % 83.36/83.45 (~P2(f2(f6(f6(a4,x25031),f1(x25031))),f7(f2(f6(a4,a5)),f2(a5)))), % 83.36/83.45 inference(scs_inference,[],[2269,2460,2469,1998,2192,15,18])). % 83.36/83.45 cnf(2515,plain, % 83.36/83.45 (~P2(f2(f6(f6(f6(a4,x25151),f1(x25151)),f6(x25152,f1(x25152)))),f7(f2(f6(a4,a5)),f2(a5)))), % 83.36/83.45 inference(scs_inference,[],[2269,2503,2448,2440,3,15,18])). % 83.36/83.45 cnf(2523,plain, % 83.36/83.45 (~P2(f2(f6(f6(a4,x25231),f1(x25231))),f7(f2(f1(f6(a4,a5))),f2(a5)))), % 83.36/83.45 inference(scs_inference,[],[2269,2515,2445,2451,2067,15,18])). % 83.36/83.45 cnf(2570,plain, % 83.36/83.45 (~P2(f2(f6(a4,f6(x25701,f1(x25701)))),f7(f2(f6(a4,a5)),f2(a5)))), % 83.36/83.45 inference(scs_inference,[],[2523,2022,2185,18])). % 83.36/83.45 cnf(2607,plain, % 83.36/83.45 ($false), % 83.36/83.45 inference(scs_inference,[],[2473,2570,1998,2440,7,2076,15,18]), % 83.36/83.45 ['proof']). % 83.45/83.45 % SZS output end Proof % 83.45/83.45 % Total time :82.790000s %------------------------------------------------------------------------------