%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN592-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 : n026.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:03 EDT 2024 % Result : Unsatisfiable 121.26s 121.37s % Output : CNFRefutation 121.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN592-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n026.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 23:52:54 EDT 2024 % 0.11/0.33 % CPUTime : % 0.52/0.56 start to proof:theBenchmark % 121.18/121.35 %------------------------------------------- % 121.18/121.35 % File :CSE---1.7 % 121.18/121.35 % Problem :theBenchmark % 121.18/121.35 % Transform :cnf % 121.18/121.35 % Format :tptp:raw % 121.18/121.35 % Command :java -jar mcs_scs.jar %d %s % 121.18/121.35 % 121.18/121.35 % Result :Theorem 120.620000s % 121.18/121.35 % Output :CNFRefutation 120.620000s % 121.18/121.35 %------------------------------------------- % 121.26/121.37 %-------------------------------------------------------------------------- % 121.26/121.37 % File : SYN592-1 : TPTP v8.2.0. Released v2.5.0. % 121.26/121.37 % Domain : Syntactic % 121.26/121.37 % Problem : Harrison problem 3584 % 121.26/121.37 % Version : Especial. % 121.26/121.37 % English : % 121.26/121.37 % 121.26/121.37 % Refs : [Har01] Email to G. Sutcliffe % 121.26/121.37 % Source : [Har01] % 121.26/121.37 % Names : % 121.26/121.37 % 121.26/121.37 % Status : Unsatisfiable % 121.26/121.37 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v5.2.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.00 v2.5.0 % 121.26/121.37 % Syntax : Number of clauses : 27 ( 13 unt; 1 nHn; 23 RR) % 121.26/121.37 % Number of literals : 54 ( 0 equ; 29 neg) % 121.26/121.37 % Maximal clause size : 4 ( 2 avg) % 121.26/121.37 % Maximal term depth : 3 ( 1 avg) % 121.26/121.37 % Number of predicates : 8 ( 8 usr; 0 prp; 1-2 aty) % 121.26/121.37 % Number of functors : 9 ( 9 usr; 6 con; 0-2 aty) % 121.26/121.37 % Number of variables : 40 ( 1 sgn) % 121.26/121.37 % SPC : CNF_UNS_RFO_NEQ_NHN % 121.26/121.37 % 121.26/121.37 % Comments : % 121.26/121.37 %-------------------------------------------------------------------------- % 121.26/121.37 cnf(c14_is_p9_1,negated_conjecture, % 121.26/121.37 p9(c14) ). % 121.26/121.37 % 121.26/121.37 cnf(c13_is_p8_2,negated_conjecture, % 121.26/121.37 p8(c13) ). % 121.26/121.37 % 121.26/121.37 cnf(p7_3,negated_conjecture, % 121.26/121.37 p7(X30,X30) ). % 121.26/121.37 % 121.26/121.37 cnf(p2_4,negated_conjecture, % 121.26/121.37 p2(X15,X15) ). % 121.26/121.37 % 121.26/121.37 cnf(p3_5,negated_conjecture, % 121.26/121.37 p3(X23,X23) ). % 121.26/121.37 % 121.26/121.37 cnf(p10_6,negated_conjecture, % 121.26/121.37 p10(c14,X4) ). % 121.26/121.37 % 121.26/121.37 cnf(p10_7,negated_conjecture, % 121.26/121.37 p10(c13,c15) ). % 121.26/121.37 % 121.26/121.37 cnf(p10_8,negated_conjecture, % 121.26/121.37 p10(c13,c17) ). % 121.26/121.37 % 121.26/121.37 cnf(p10_9,negated_conjecture, % 121.26/121.37 p10(c13,c16) ). % 121.26/121.37 % 121.26/121.37 cnf(not_p2_10,negated_conjecture, % 121.26/121.37 ~ p2(c17,c15) ). % 121.26/121.37 % 121.26/121.37 cnf(p12_11,negated_conjecture, % 121.26/121.37 p12(c14,f4(c18,c17)) ). % 121.26/121.37 % 121.26/121.37 cnf(not_p11_12,negated_conjecture, % 121.26/121.37 ~ p11(c13,f4(c17,f5(c18))) ). % 121.26/121.37 % 121.26/121.37 cnf(not_p11_13,negated_conjecture, % 121.26/121.37 ~ p11(c13,f4(f5(c18),c17)) ). % 121.26/121.37 % 121.26/121.37 cnf(p8_14,negated_conjecture, % 121.26/121.37 ( p8(X33) % 121.26/121.37 | ~ p8(X34) % 121.26/121.37 | ~ p7(X34,X33) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p9_15,negated_conjecture, % 121.26/121.37 ( p9(X35) % 121.26/121.37 | ~ p9(X36) % 121.26/121.37 | ~ p7(X36,X35) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p11_16,negated_conjecture, % 121.26/121.37 ( p11(c14,f4(c15,X10)) % 121.26/121.37 | ~ p10(c13,X10) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p2_17,negated_conjecture, % 121.26/121.37 ( p2(f5(X18),f5(X19)) % 121.26/121.37 | ~ p2(X18,X19) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p2_18,negated_conjecture, % 121.26/121.37 ( p2(f6(X21),f6(X22)) % 121.26/121.37 | ~ p2(X21,X22) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p7_19,negated_conjecture, % 121.26/121.37 ( p7(X31,X32) % 121.26/121.37 | ~ p7(X30,X31) % 121.26/121.37 | ~ p7(X30,X32) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p2_20,negated_conjecture, % 121.26/121.37 ( p2(X16,X17) % 121.26/121.37 | ~ p2(X15,X16) % 121.26/121.37 | ~ p2(X15,X17) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p3_21,negated_conjecture, % 121.26/121.37 ( p3(X24,X25) % 121.26/121.37 | ~ p3(X23,X24) % 121.26/121.37 | ~ p3(X23,X25) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p2_22,negated_conjecture, % 121.26/121.37 ( p2(f6(X20),f5(X20)) % 121.26/121.37 | ~ p12(c14,f4(X20,c17)) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p10_23,negated_conjecture, % 121.26/121.37 ( p10(X0,X1) % 121.26/121.37 | ~ p2(X3,X1) % 121.26/121.37 | ~ p7(X2,X0) % 121.26/121.37 | ~ p10(X2,X3) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p12_24,negated_conjecture, % 121.26/121.37 ( p12(X11,X12) % 121.26/121.37 | ~ p3(X14,X12) % 121.26/121.37 | ~ p7(X13,X11) % 121.26/121.37 | ~ p12(X13,X14) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p11_25,negated_conjecture, % 121.26/121.37 ( p11(X5,X6) % 121.26/121.37 | ~ p3(X8,X6) % 121.26/121.37 | ~ p7(X7,X5) % 121.26/121.37 | ~ p11(X7,X8) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p3_26,negated_conjecture, % 121.26/121.37 ( p3(f4(X26,X27),f4(X28,X29)) % 121.26/121.37 | ~ p2(X26,X28) % 121.26/121.37 | ~ p2(X27,X29) ) ). % 121.26/121.37 % 121.26/121.37 cnf(p11_27,negated_conjecture, % 121.26/121.37 ( p11(c13,f4(c17,f6(X9))) % 121.26/121.37 | p11(c13,f4(f6(X9),c17)) % 121.26/121.37 | ~ p12(c14,f4(X9,c17)) ) ). % 121.26/121.37 % 121.26/121.37 %-------------------------------------------------------------------------- % 121.26/121.37 %------------------------------------------- % 121.26/121.37 % Proof found % 121.26/121.37 % SZS status Theorem for theBenchmark % 121.26/121.37 % SZS output start Proof % 121.29/121.39 %ClaNum:27(EqnAxiom:0) % 121.29/121.39 %VarNum:81(SingletonVarNum:40) % 121.29/121.39 %MaxLitNum:4 % 121.29/121.39 %MaxfuncDepth:2 % 121.29/121.39 %SharedTerms:19 % 121.29/121.39 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 % 121.29/121.39 %singleGoalClaCount:13 % 121.29/121.39 [1]P1(a1) % 121.29/121.39 [2]P2(a2) % 121.29/121.39 [3]P3(a2,a3) % 121.29/121.39 [4]P3(a2,a4) % 121.29/121.39 [5]P3(a2,a5) % 121.29/121.39 [11]~P5(a4,a3) % 121.29/121.39 [10]P6(a1,f7(a6,a4)) % 121.29/121.39 [12]~P7(a2,f7(a4,f8(a6))) % 121.29/121.39 [13]~P7(a2,f7(f8(a6),a4)) % 121.29/121.39 [6]P3(a1,x61) % 121.29/121.39 [7]P4(x71,x71) % 121.29/121.39 [8]P5(x81,x81) % 121.29/121.39 [9]P8(x91,x91) % 121.29/121.39 [18]~P3(a2,x181)+P7(a1,f7(a3,x181)) % 121.29/121.39 [25]P5(f9(x251),f8(x251))+~P6(a1,f7(x251,a4)) % 121.29/121.39 [16]~P5(x161,x162)+P5(f8(x161),f8(x162)) % 121.29/121.39 [17]~P5(x171,x172)+P5(f9(x171),f9(x172)) % 121.29/121.39 [27]~P6(a1,f7(x271,a4))+P7(a2,f7(a4,f9(x271)))+P7(a2,f7(f9(x271),a4)) % 121.29/121.39 [14]~P4(x142,x141)+P1(x141)+~P1(x142) % 121.29/121.39 [15]~P4(x152,x151)+P2(x151)+~P2(x152) % 121.29/121.39 [19]~P4(x193,x191)+P4(x191,x192)+~P4(x193,x192) % 121.29/121.39 [20]~P5(x203,x201)+P5(x201,x202)+~P5(x203,x202) % 121.29/121.39 [21]~P8(x213,x211)+P8(x211,x212)+~P8(x213,x212) % 121.29/121.39 [26]~P5(x262,x264)+~P5(x261,x263)+P8(f7(x261,x262),f7(x263,x264)) % 121.29/121.39 [22]~P3(x223,x224)+P3(x221,x222)+~P4(x223,x221)+~P5(x224,x222) % 121.29/121.39 [23]~P6(x233,x234)+P6(x231,x232)+~P4(x233,x231)+~P8(x234,x232) % 121.29/121.39 [24]~P7(x243,x244)+P7(x241,x242)+~P4(x243,x241)+~P8(x244,x242) % 121.29/121.39 %EqnAxiom % 121.29/121.39 % 121.29/121.39 %------------------------------------------- % 121.29/121.41 cnf(28,plain, % 121.29/121.41 (P5(f9(a6),f8(a6))), % 121.29/121.41 inference(scs_inference,[],[10,25])). % 121.29/121.41 cnf(167,plain, % 121.29/121.41 (P7(a2,f7(f9(a6),a4))+P7(a2,f7(a4,f9(a6)))), % 121.29/121.41 inference(scs_inference,[],[3,10,18,27])). % 121.29/121.41 cnf(175,plain, % 121.29/121.41 (~P8(f7(f9(a6),a4),f7(f8(a6),a4))+P7(a2,f7(a4,f9(a6)))), % 121.29/121.41 inference(scs_inference,[],[7,13,167,24])). % 121.29/121.41 cnf(789,plain, % 121.29/121.41 (~P8(f7(a4,f9(a6)),f7(a4,f8(a6)))+~P8(f7(f9(a6),a4),f7(f8(a6),a4))), % 121.29/121.41 inference(scs_inference,[],[12,7,175,24])). % 121.29/121.41 cnf(825,plain, % 121.29/121.41 (~P8(f7(f9(a6),a4),f7(f8(a6),a4))), % 121.29/121.41 inference(scs_inference,[],[28,8,789,26])). % 121.29/121.41 cnf(826,plain, % 121.29/121.41 ($false), % 121.29/121.41 inference(scs_inference,[],[28,8,825,26]), % 121.29/121.41 ['proof']). % 121.29/121.41 % SZS output end Proof % 121.29/121.41 % Total time :120.620000s %------------------------------------------------------------------------------