%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN576-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 : 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:00 EDT 2024 % Result : Unsatisfiable 5.99s 6.09s % Output : CNFRefutation 5.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SYN576-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 18:32:53 EDT 2024 % 0.13/0.34 % CPUTime : % 0.55/0.58 start to proof:theBenchmark % 5.99/6.08 %------------------------------------------- % 5.99/6.08 % File :CSE---1.7 % 5.99/6.08 % Problem :theBenchmark % 5.99/6.08 % Transform :cnf % 5.99/6.08 % Format :tptp:raw % 5.99/6.08 % Command :java -jar mcs_scs.jar %d %s % 5.99/6.08 % 5.99/6.08 % Result :Theorem 5.460000s % 5.99/6.08 % Output :CNFRefutation 5.460000s % 5.99/6.08 %------------------------------------------- % 5.99/6.09 %-------------------------------------------------------------------------- % 5.99/6.09 % File : SYN576-1 : TPTP v8.2.0. Released v2.5.0. % 5.99/6.09 % Domain : Syntactic % 5.99/6.09 % Problem : Harrison problem 3280 % 5.99/6.09 % Version : Especial. % 5.99/6.09 % English : % 5.99/6.09 % 5.99/6.09 % Refs : [Har01] Email to G. Sutcliffe % 5.99/6.09 % Source : [Har01] % 5.99/6.09 % Names : % 5.99/6.09 % 5.99/6.09 % Status : Unsatisfiable % 5.99/6.09 % Rating : 0.17 v8.2.0, 0.00 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.29 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 5.99/6.09 % Syntax : Number of clauses : 22 ( 8 unt; 1 nHn; 16 RR) % 5.99/6.09 % Number of literals : 52 ( 0 equ; 30 neg) % 5.99/6.09 % Maximal clause size : 4 ( 2 avg) % 5.99/6.09 % Maximal term depth : 4 ( 1 avg) % 5.99/6.09 % Number of predicates : 6 ( 6 usr; 0 prp; 2-2 aty) % 5.99/6.09 % Number of functors : 9 ( 9 usr; 4 con; 0-3 aty) % 5.99/6.09 % Number of variables : 52 ( 0 sgn) % 5.99/6.09 % SPC : CNF_UNS_RFO_NEQ_NHN % 5.99/6.09 % 5.99/6.09 % Comments : % 5.99/6.09 %-------------------------------------------------------------------------- % 5.99/6.09 cnf(p8_1,negated_conjecture, % 5.99/6.09 p8(X42,X42) ). % 5.99/6.09 % 5.99/6.09 cnf(p2_2,negated_conjecture, % 5.99/6.09 p2(X13,X13) ). % 5.99/6.09 % 5.99/6.09 cnf(p4_3,negated_conjecture, % 5.99/6.09 p4(X34,X34) ). % 5.99/6.09 % 5.99/6.09 cnf(p5_4,negated_conjecture, % 5.99/6.09 p5(X37,X37) ). % 5.99/6.09 % 5.99/6.09 cnf(p12_5,negated_conjecture, % 5.99/6.09 p12(c15,f6(c13)) ). % 5.99/6.09 % 5.99/6.09 cnf(p12_6,negated_conjecture, % 5.99/6.09 p12(c16,f6(c13)) ). % 5.99/6.09 % 5.99/6.09 cnf(p11_7,negated_conjecture, % 5.99/6.09 ( p11(X4,X5) % 5.99/6.09 | p11(X5,X4) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p2_8,negated_conjecture, % 5.99/6.09 p2(f3(X22,X23),f3(X23,X22)) ). % 5.99/6.09 % 5.99/6.09 cnf(p5_9,negated_conjecture, % 5.99/6.09 ( p5(f6(X40),f6(X41)) % 5.99/6.09 | ~ p4(X40,X41) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p2_10,negated_conjecture, % 5.99/6.09 ( p2(f10(X16),f10(X17)) % 5.99/6.09 | ~ p2(X16,X17) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p8_11,negated_conjecture, % 5.99/6.09 ( p8(X43,X44) % 5.99/6.09 | ~ p8(X42,X43) % 5.99/6.09 | ~ p8(X42,X44) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p2_12,negated_conjecture, % 5.99/6.09 ( p2(X14,X15) % 5.99/6.09 | ~ p2(X13,X14) % 5.99/6.09 | ~ p2(X13,X15) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p4_13,negated_conjecture, % 5.99/6.09 ( p4(X35,X36) % 5.99/6.09 | ~ p4(X34,X35) % 5.99/6.09 | ~ p4(X34,X36) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p5_14,negated_conjecture, % 5.99/6.09 ( p5(X38,X39) % 5.99/6.09 | ~ p5(X37,X38) % 5.99/6.09 | ~ p5(X37,X39) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p11_15,negated_conjecture, % 5.99/6.09 ( p11(X0,X1) % 5.99/6.09 | ~ p2(X2,X0) % 5.99/6.09 | ~ p2(X3,X1) % 5.99/6.09 | ~ p11(X2,X3) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p12_16,negated_conjecture, % 5.99/6.09 ( p12(X6,X7) % 5.99/6.09 | ~ p2(X8,X6) % 5.99/6.09 | ~ p5(X9,X7) % 5.99/6.09 | ~ p12(X8,X9) ) ). % 5.99/6.09 % 5.99/6.09 cnf(not_p12_17,negated_conjecture, % 5.99/6.09 ~ p12(f7(f9(c13,c14,f3(c15,c16)),f3(c15,c16)),f6(c13)) ). % 5.99/6.09 % 5.99/6.09 cnf(p2_18,negated_conjecture, % 5.99/6.09 ( p2(f3(X18,X19),f3(X20,X21)) % 5.99/6.09 | ~ p2(X18,X20) % 5.99/6.09 | ~ p2(X19,X21) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p2_19,negated_conjecture, % 5.99/6.09 ( p2(f7(X24,X25),f7(X26,X27)) % 5.99/6.09 | ~ p2(X24,X26) % 5.99/6.09 | ~ p2(X25,X27) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p2_20,negated_conjecture, % 5.99/6.09 ( p2(f9(X28,X29,X30),f9(X31,X32,X33)) % 5.99/6.09 | ~ p4(X28,X31) % 5.99/6.09 | ~ p8(X29,X32) % 5.99/6.09 | ~ p2(X30,X33) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p12_21,negated_conjecture, % 5.99/6.09 ( p12(f7(f9(X10,c14,f3(X11,X12)),X12),f6(X10)) % 5.99/6.09 | ~ p12(X12,f6(X10)) % 5.99/6.09 | ~ p12(X11,f6(X10)) % 5.99/6.09 | ~ p11(f10(X11),f10(X12)) ) ). % 5.99/6.09 % 5.99/6.09 cnf(p12_22,negated_conjecture, % 5.99/6.09 ( p12(f7(f9(X10,c14,f3(X11,X12)),f3(X11,X12)),f6(X10)) % 5.99/6.09 | ~ p12(X12,f6(X10)) % 5.99/6.09 | ~ p12(X11,f6(X10)) % 5.99/6.09 | ~ p11(f10(X11),f10(X12)) ) ). % 5.99/6.09 % 5.99/6.09 %-------------------------------------------------------------------------- % 5.99/6.09 %------------------------------------------- % 5.99/6.09 % Proof found % 5.99/6.09 % SZS status Theorem for theBenchmark % 5.99/6.09 % SZS output start Proof % 5.99/6.09 %ClaNum:22(EqnAxiom:0) % 5.99/6.09 %VarNum:115(SingletonVarNum:52) % 5.99/6.09 %MaxLitNum:4 % 5.99/6.09 %MaxfuncDepth:3 % 5.99/6.09 %SharedTerms:11 % 5.99/6.09 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 % 5.99/6.09 %singleGoalClaCount:8 % 5.99/6.09 [5]P3(a1,f4(a2)) % 5.99/6.09 [6]P3(a5,f4(a2)) % 5.99/6.09 [8]~P3(f9(f8(a2,a3,f6(a1,a5)),f6(a1,a5)),f4(a2)) % 5.99/6.09 [1]P1(x11,x11) % 5.99/6.09 [2]P2(x21,x21) % 5.99/6.09 [3]P5(x31,x31) % 5.99/6.09 [4]P6(x41,x41) % 5.99/6.09 [7]P2(f6(x71,x72),f6(x72,x71)) % 5.99/6.09 [9]P4(x92,x91)+P4(x91,x92) % 5.99/6.09 [10]~P2(x101,x102)+P2(f7(x101),f7(x102)) % 5.99/6.09 [11]~P5(x111,x112)+P6(f4(x111),f4(x112)) % 5.99/6.09 [12]~P1(x123,x121)+P1(x121,x122)+~P1(x123,x122) % 5.99/6.09 [13]~P2(x133,x131)+P2(x131,x132)+~P2(x133,x132) % 5.99/6.09 [14]~P5(x143,x141)+P5(x141,x142)+~P5(x143,x142) % 5.99/6.09 [15]~P6(x153,x151)+P6(x151,x152)+~P6(x153,x152) % 5.99/6.09 [18]~P2(x182,x184)+~P2(x181,x183)+P2(f6(x181,x182),f6(x183,x184)) % 5.99/6.09 [19]~P2(x192,x194)+~P2(x191,x193)+P2(f9(x191,x192),f9(x193,x194)) % 5.99/6.09 [22]~P3(x223,f4(x221))+~P3(x222,f4(x221))+~P4(f7(x222),f7(x223))+P3(f9(f8(x221,a3,f6(x222,x223)),f6(x222,x223)),f4(x221)) % 5.99/6.09 [21]~P3(x213,f4(x211))+~P3(x212,f4(x211))+~P4(f7(x212),f7(x213))+P3(f9(f8(x211,a3,f6(x212,x213)),x213),f4(x211)) % 5.99/6.09 [16]~P3(x163,x164)+P3(x161,x162)+~P2(x163,x161)+~P6(x164,x162) % 5.99/6.09 [17]~P4(x174,x173)+P4(x171,x172)+~P2(x173,x172)+~P2(x174,x171) % 5.99/6.09 [20]~P1(x202,x205)+~P2(x203,x206)+~P5(x201,x204)+P2(f8(x201,x202,x203),f8(x204,x205,x206)) % 5.99/6.09 %EqnAxiom % 5.99/6.09 % 5.99/6.09 %------------------------------------------- % 5.99/6.09 cnf(25,plain, % 5.99/6.09 (P4(f7(a5),f7(a1))), % 5.99/6.09 inference(scs_inference,[],[5,6,8,22,9])). % 5.99/6.09 cnf(36,plain, % 5.99/6.09 (P2(f8(x361,x362,f6(x363,x364)),f8(x361,x362,f6(x364,x363)))), % 5.99/6.09 inference(scs_inference,[],[1,7,3,12,20])). % 5.99/6.09 cnf(41,plain, % 5.99/6.09 (~P2(f7(a5),x411)+P4(x411,f7(a1))), % 5.99/6.09 inference(scs_inference,[],[25,2,17])). % 5.99/6.10 cnf(57,plain, % 5.99/6.10 (P3(f9(f8(a2,a3,f6(a5,a1)),f6(a5,a1)),f4(a2))), % 5.99/6.10 inference(scs_inference,[],[2,5,6,41,22])). % 5.99/6.10 cnf(116,plain, % 5.99/6.10 ($false), % 5.99/6.10 inference(scs_inference,[],[36,57,7,8,4,16,19]), % 5.99/6.10 ['proof']). % 5.99/6.10 % SZS output end Proof % 5.99/6.10 % Total time :5.460000s %------------------------------------------------------------------------------