%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN569-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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 6.69s 6.76s % Output : CNFRefutation 6.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN569-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.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:58:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.45/0.56 start to proof:theBenchmark % 6.69/6.75 %------------------------------------------- % 6.69/6.75 % File :CSE---1.7 % 6.69/6.75 % Problem :theBenchmark % 6.69/6.75 % Transform :cnf % 6.69/6.75 % Format :tptp:raw % 6.69/6.75 % Command :java -jar mcs_scs.jar %d %s % 6.69/6.75 % 6.69/6.75 % Result :Theorem 6.140000s % 6.69/6.75 % Output :CNFRefutation 6.140000s % 6.69/6.75 %------------------------------------------- % 6.69/6.75 %-------------------------------------------------------------------------- % 6.69/6.75 % File : SYN569-1 : TPTP v8.2.0. Released v2.5.0. % 6.69/6.75 % Domain : Syntactic % 6.69/6.75 % Problem : Harrison problem 3088 % 6.69/6.75 % Version : Especial. % 6.69/6.75 % English : % 6.69/6.75 % 6.69/6.75 % Refs : [Har01] Email to G. Sutcliffe % 6.69/6.75 % Source : [Har01] % 6.69/6.75 % Names : % 6.69/6.75 % 6.69/6.75 % Status : Unsatisfiable % 6.69/6.75 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v2.5.0 % 6.69/6.75 % Syntax : Number of clauses : 20 ( 7 unt; 0 nHn; 18 RR) % 6.69/6.75 % Number of literals : 48 ( 0 equ; 29 neg) % 6.69/6.75 % Maximal clause size : 5 ( 2 avg) % 6.69/6.75 % Maximal term depth : 3 ( 1 avg) % 6.69/6.75 % Number of predicates : 5 ( 5 usr; 0 prp; 2-3 aty) % 6.69/6.75 % Number of functors : 9 ( 9 usr; 5 con; 0-2 aty) % 6.69/6.75 % Number of variables : 44 ( 0 sgn) % 6.69/6.75 % SPC : CNF_UNS_RFO_NEQ_HRN % 6.69/6.75 % 6.69/6.75 % Comments : % 6.69/6.75 %-------------------------------------------------------------------------- % 6.69/6.75 cnf(p2_1,negated_conjecture, % 6.69/6.75 p2(X6,X6) ). % 6.69/6.75 % 6.69/6.75 cnf(p6_2,negated_conjecture, % 6.69/6.75 p6(X27,X27) ). % 6.69/6.75 % 6.69/6.75 cnf(p8_3,negated_conjecture, % 6.69/6.75 p8(c14,c12) ). % 6.69/6.75 % 6.69/6.75 cnf(p8_4,negated_conjecture, % 6.69/6.75 p8(c11,c12) ). % 6.69/6.75 % 6.69/6.75 cnf(p8_5,negated_conjecture, % 6.69/6.75 p8(c11,c14) ). % 6.69/6.75 % 6.69/6.75 cnf(p9_6,negated_conjecture, % 6.69/6.75 p9(c13,c15,c14) ). % 6.69/6.75 % 6.69/6.75 cnf(p10_7,negated_conjecture, % 6.69/6.75 ( p10(X4,X5) % 6.69/6.75 | ~ p8(X4,X5) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p2_8,negated_conjecture, % 6.69/6.75 ( p2(f3(X13),f3(X14)) % 6.69/6.75 | ~ p2(X13,X14) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p6_9,negated_conjecture, % 6.69/6.75 ( p6(X28,X29) % 6.69/6.75 | ~ p6(X27,X28) % 6.69/6.75 | ~ p6(X27,X29) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p2_10,negated_conjecture, % 6.69/6.75 ( p2(X7,X8) % 6.69/6.75 | ~ p2(X6,X7) % 6.69/6.75 | ~ p2(X6,X8) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p2_11,negated_conjecture, % 6.69/6.75 ( p2(X9,X10) % 6.69/6.75 | ~ p9(X11,X9,X12) % 6.69/6.75 | ~ p9(X11,X10,X12) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p9_12,negated_conjecture, % 6.69/6.75 ( p9(c13,f3(X40),X40) % 6.69/6.75 | ~ p10(X40,c12) % 6.69/6.75 | ~ p10(c11,X40) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p10_13,negated_conjecture, % 6.69/6.75 ( p10(X0,X1) % 6.69/6.75 | ~ p2(X2,X0) % 6.69/6.75 | ~ p2(X3,X1) % 6.69/6.75 | ~ p10(X2,X3) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p8_14,negated_conjecture, % 6.69/6.75 ( p8(X30,X31) % 6.69/6.75 | ~ p2(X33,X31) % 6.69/6.75 | ~ p8(X32,X33) % 6.69/6.75 | ~ p2(X32,X30) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p2_15,negated_conjecture, % 6.69/6.75 p2(f5(f7(c13,c12),f7(c13,c11)),f4(f5(c12,c11),c15)) ). % 6.69/6.75 % 6.69/6.75 cnf(p2_16,negated_conjecture, % 6.69/6.75 ( p2(f4(X15,X16),f4(X17,X18)) % 6.69/6.75 | ~ p2(X15,X17) % 6.69/6.75 | ~ p2(X16,X18) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p2_17,negated_conjecture, % 6.69/6.75 ( p2(f7(X23,X24),f7(X25,X26)) % 6.69/6.75 | ~ p2(X24,X26) % 6.69/6.75 | ~ p6(X23,X25) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p2_18,negated_conjecture, % 6.69/6.75 ( p2(f5(X19,X20),f5(X21,X22)) % 6.69/6.75 | ~ p2(X19,X21) % 6.69/6.75 | ~ p2(X20,X22) ) ). % 6.69/6.75 % 6.69/6.75 cnf(p9_19,negated_conjecture, % 6.69/6.75 ( p9(X34,X35,X36) % 6.69/6.75 | ~ p2(X37,X35) % 6.69/6.75 | ~ p2(X38,X36) % 6.69/6.75 | ~ p6(X39,X34) % 6.69/6.75 | ~ p9(X39,X37,X38) ) ). % 6.69/6.75 % 6.69/6.75 cnf(not_p8_20,negated_conjecture, % 6.69/6.75 ( ~ p8(X41,c12) % 6.69/6.76 | ~ p8(c11,X41) % 6.69/6.76 | ~ p2(f5(f7(c13,c12),f7(c13,c11)),f4(f5(c12,c11),f3(X41))) ) ). % 6.69/6.76 % 6.69/6.76 %-------------------------------------------------------------------------- % 6.69/6.76 %------------------------------------------- % 6.69/6.76 % Proof found % 6.69/6.76 % SZS status Theorem for theBenchmark % 6.69/6.76 % SZS output start Proof % 6.69/6.76 %ClaNum:20(EqnAxiom:0) % 6.69/6.76 %VarNum:91(SingletonVarNum:44) % 6.69/6.76 %MaxLitNum:5 % 6.69/6.76 %MaxfuncDepth:2 % 6.69/6.76 %SharedTerms:15 % 6.69/6.76 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 % 6.69/6.76 %singleGoalClaCount:7 % 6.69/6.76 [1]P1(a1,a2) % 6.69/6.76 [2]P1(a3,a1) % 6.69/6.76 [3]P1(a3,a2) % 6.69/6.76 [6]P5(a4,a5,a1) % 6.69/6.76 [7]P2(f7(f6(a4,a2),f6(a4,a3)),f8(f7(a2,a3),a5)) % 6.69/6.76 [4]P2(x41,x41) % 6.69/6.76 [5]P4(x51,x51) % 6.69/6.76 [8]~P1(x81,x82)+P3(x81,x82) % 6.69/6.76 [9]~P2(x91,x92)+P2(f9(x91),f9(x92)) % 6.69/6.76 [14]~P3(x141,a2)+~P3(a3,x141)+P5(a4,f9(x141),x141) % 6.69/6.76 [20]~P1(a3,x201)+~P1(x201,a2)+~P2(f7(f6(a4,a2),f6(a4,a3)),f8(f7(a2,a3),f9(x201))) % 6.69/6.76 [10]~P2(x103,x101)+P2(x101,x102)+~P2(x103,x102) % 6.69/6.76 [11]~P4(x113,x111)+P4(x111,x112)+~P4(x113,x112) % 6.69/6.76 [18]~P5(x183,x181,x184)+P2(x181,x182)+~P5(x183,x182,x184) % 6.69/6.76 [15]~P2(x152,x154)+~P4(x151,x153)+P2(f6(x151,x152),f6(x153,x154)) % 6.69/6.76 [16]~P2(x162,x164)+~P2(x161,x163)+P2(f7(x161,x162),f7(x163,x164)) % 6.69/6.76 [17]~P2(x172,x174)+~P2(x171,x173)+P2(f8(x171,x172),f8(x173,x174)) % 6.69/6.76 [12]~P1(x123,x124)+P1(x121,x122)+~P2(x123,x121)+~P2(x124,x122) % 6.69/6.76 [13]~P3(x134,x133)+P3(x131,x132)+~P2(x133,x132)+~P2(x134,x131) % 6.69/6.76 [19]~P5(x196,x195,x194)+P5(x191,x192,x193)+~P2(x194,x193)+~P2(x195,x192)+~P4(x196,x191) % 6.69/6.76 %EqnAxiom % 6.69/6.76 % 6.69/6.76 %------------------------------------------- % 6.69/6.76 cnf(24,plain, % 6.69/6.76 (P2(f8(f7(a2,a3),a5),f7(f6(a4,a2),f6(a4,a3)))), % 6.69/6.76 inference(scs_inference,[],[7,4,10])). % 6.69/6.76 cnf(109,plain, % 6.69/6.76 (~P3(a3,a1)+P5(a4,f9(a1),a1)), % 6.69/6.76 inference(scs_inference,[],[1,8,14])). % 6.69/6.76 cnf(151,plain, % 6.69/6.76 (P5(a4,f9(a1),a1)), % 6.69/6.76 inference(scs_inference,[],[2,8,109])). % 6.69/6.76 cnf(856,plain, % 6.69/6.76 (~P2(a2,x8561)+P1(a1,x8561)), % 6.69/6.76 inference(scs_inference,[],[1,4,12])). % 6.69/6.76 cnf(1030,plain, % 6.69/6.76 (~P2(f7(f6(a4,a2),f6(a4,a3)),f8(f7(a2,a3),f9(a1)))), % 6.69/6.76 inference(scs_inference,[],[4,2,856,20])). % 6.69/6.76 cnf(1031,plain, % 6.69/6.76 (~P2(f8(f7(a2,a3),f9(a1)),f7(f6(a4,a2),f6(a4,a3)))), % 6.69/6.76 inference(scs_inference,[],[1030,4,10])). % 6.69/6.76 cnf(1040,plain, % 6.69/6.76 ($false), % 6.69/6.76 inference(scs_inference,[],[24,151,1031,4,6,10,17,18]), % 6.69/6.76 ['proof']). % 6.69/6.76 % SZS output end Proof % 6.69/6.76 % Total time :6.140000s %------------------------------------------------------------------------------