%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN590-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 : n032.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 118.33s 118.41s % Output : CNFRefutation 118.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SYN590-1 : TPTP v8.2.0. Released v2.5.0. % 0.00/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.27 % Computer : n032.cluster.edu % 0.07/0.27 % Model : x86_64 x86_64 % 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.27 % Memory : 8042.1875MB % 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.27 % CPULimit : 300 % 0.07/0.27 % WCLimit : 300 % 0.07/0.27 % DateTime : Sun Jun 23 19:59:38 EDT 2024 % 0.07/0.27 % CPUTime : % 0.12/0.45 start to proof:theBenchmark % 118.24/118.40 %------------------------------------------- % 118.24/118.40 % File :CSE---1.7 % 118.24/118.40 % Problem :theBenchmark % 118.24/118.40 % Transform :cnf % 118.24/118.40 % Format :tptp:raw % 118.24/118.40 % Command :java -jar mcs_scs.jar %d %s % 118.24/118.40 % 118.24/118.40 % Result :Theorem 117.890000s % 118.24/118.40 % Output :CNFRefutation 117.890000s % 118.24/118.40 %------------------------------------------- % 118.33/118.41 %-------------------------------------------------------------------------- % 118.33/118.41 % File : SYN590-1 : TPTP v8.2.0. Released v2.5.0. % 118.33/118.41 % Domain : Syntactic % 118.33/118.41 % Problem : Harrison problem 3582 % 118.33/118.41 % Version : Especial. % 118.33/118.41 % English : % 118.33/118.41 % 118.33/118.41 % Refs : [Har01] Email to G. Sutcliffe % 118.33/118.41 % Source : [Har01] % 118.33/118.41 % Names : % 118.33/118.41 % 118.33/118.41 % Status : Unsatisfiable % 118.33/118.41 % Rating : 0.00 v5.3.0, 0.05 v5.2.0, 0.00 v2.5.0 % 118.33/118.41 % Syntax : Number of clauses : 27 ( 8 unt; 0 nHn; 24 RR) % 118.33/118.41 % Number of literals : 55 ( 0 equ; 29 neg) % 118.33/118.41 % Maximal clause size : 4 ( 2 avg) % 118.33/118.41 % Maximal term depth : 3 ( 1 avg) % 118.33/118.41 % Number of predicates : 6 ( 6 usr; 0 prp; 1-2 aty) % 118.33/118.41 % Number of functors : 11 ( 11 usr; 6 con; 0-1 aty) % 118.33/118.41 % Number of variables : 43 ( 0 sgn) % 118.33/118.41 % SPC : CNF_UNS_RFO_NEQ_HRN % 118.33/118.41 % 118.33/118.41 % Comments : % 118.33/118.41 %-------------------------------------------------------------------------- % 118.33/118.41 cnf(c14_is_p11_1,negated_conjecture, % 118.33/118.41 p11(c14) ). % 118.33/118.41 % 118.33/118.41 cnf(c17_is_p11_2,negated_conjecture, % 118.33/118.41 p11(c17) ). % 118.33/118.41 % 118.33/118.41 cnf(c16_is_p11_3,negated_conjecture, % 118.33/118.41 p11(c16) ). % 118.33/118.41 % 118.33/118.41 cnf(p5_4,negated_conjecture, % 118.33/118.41 p5(X27,X27) ). % 118.33/118.41 % 118.33/118.41 cnf(p2_5,negated_conjecture, % 118.33/118.41 p2(X14,X14) ). % 118.33/118.41 % 118.33/118.41 cnf(p3_6,negated_conjecture, % 118.33/118.41 p3(X19,X19) ). % 118.33/118.41 % 118.33/118.41 cnf(p3_7,negated_conjecture, % 118.33/118.41 p3(f4(c17),f6(c18)) ). % 118.33/118.41 % 118.33/118.41 cnf(p3_8,negated_conjecture, % 118.33/118.41 p3(f4(c16),f6(c15)) ). % 118.33/118.41 % 118.33/118.41 cnf(p11_9,negated_conjecture, % 118.33/118.41 ( p11(f9(X4)) % 118.33/118.41 | ~ p11(X4) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p11_10,negated_conjecture, % 118.33/118.41 ( p11(X8) % 118.33/118.41 | ~ p11(X9) % 118.33/118.41 | ~ p2(X9,X8) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p12_11,negated_conjecture, % 118.33/118.41 ( p12(X5,X6) % 118.33/118.41 | ~ p10(f6(X5),f6(X6)) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p5_12,negated_conjecture, % 118.33/118.41 ( p5(f8(X32),f8(X33)) % 118.33/118.41 | ~ p2(X32,X33) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p10_13,negated_conjecture, % 118.33/118.41 ( p10(f6(X5),f6(X6)) % 118.33/118.41 | ~ p12(X5,X6) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p2_14,negated_conjecture, % 118.33/118.41 ( p2(f9(X17),f9(X18)) % 118.33/118.41 | ~ p2(X17,X18) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p3_15,negated_conjecture, % 118.33/118.41 ( p3(f4(X22),f4(X23)) % 118.33/118.41 | ~ p2(X22,X23) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p3_16,negated_conjecture, % 118.33/118.41 ( p3(f6(X25),f6(X26)) % 118.33/118.41 | ~ p5(X25,X26) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p5_17,negated_conjecture, % 118.33/118.41 ( p5(f7(X30),f7(X31)) % 118.33/118.41 | ~ p5(X30,X31) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p3_18,negated_conjecture, % 118.33/118.41 ( p3(f4(X24),f6(f8(X24))) % 118.33/118.41 | ~ p11(X24) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p10_19,negated_conjecture, % 118.33/118.41 ( p10(f4(f9(X4)),f4(X4)) % 118.33/118.41 | ~ p11(X4) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p10_20,negated_conjecture, % 118.33/118.41 ( p10(f6(f7(c13)),f4(X7)) % 118.33/118.41 | ~ p11(X7) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p10_21,negated_conjecture, % 118.33/118.41 ( p10(f6(f7(c13)),f4(X4)) % 118.33/118.41 | ~ p11(X4) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p5_22,negated_conjecture, % 118.33/118.41 ( p5(X28,X29) % 118.33/118.41 | ~ p5(X27,X28) % 118.33/118.41 | ~ p5(X27,X29) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p2_23,negated_conjecture, % 118.33/118.41 ( p2(X15,X16) % 118.33/118.41 | ~ p2(X14,X15) % 118.33/118.41 | ~ p2(X14,X16) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p3_24,negated_conjecture, % 118.33/118.41 ( p3(X20,X21) % 118.33/118.41 | ~ p3(X19,X20) % 118.33/118.41 | ~ p3(X19,X21) ) ). % 118.33/118.41 % 118.33/118.41 cnf(not_p11_25,negated_conjecture, % 118.33/118.41 ( ~ p11(X34) % 118.33/118.41 | ~ p12(X35,c15) % 118.33/118.41 | ~ p3(f4(X34),f6(X35)) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p10_26,negated_conjecture, % 118.33/118.41 ( p10(X0,X1) % 118.33/118.41 | ~ p3(X2,X0) % 118.33/118.41 | ~ p3(X3,X1) % 118.33/118.41 | ~ p10(X2,X3) ) ). % 118.33/118.41 % 118.33/118.41 cnf(p12_27,negated_conjecture, % 118.33/118.41 ( p12(X10,X11) % 118.33/118.41 | ~ p5(X12,X10) % 118.33/118.41 | ~ p5(X13,X11) % 118.33/118.41 | ~ p12(X12,X13) ) ). % 118.33/118.41 % 118.33/118.41 %-------------------------------------------------------------------------- % 118.33/118.41 %------------------------------------------- % 118.33/118.41 % Proof found % 118.33/118.41 % SZS status Theorem for theBenchmark % 118.33/118.41 % SZS output start Proof % 118.33/118.41 %ClaNum:27(EqnAxiom:0) % 118.33/118.41 %VarNum:86(SingletonVarNum:42) % 118.33/118.41 %MaxLitNum:4 % 118.33/118.41 %MaxfuncDepth:2 % 118.33/118.41 %SharedTerms:17 % 118.33/118.42 %goalClause: 1 2 3 4 5 6 7 8 9 10 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 % 118.33/118.42 %singleGoalClaCount:8 % 118.33/118.42 [1]P1(a1) % 118.33/118.42 [2]P1(a3) % 118.33/118.42 [3]P1(a4) % 118.33/118.42 [7]P6(f6(a3),f8(a7)) % 118.33/118.42 [8]P6(f6(a4),f8(a5)) % 118.33/118.42 [4]P3(x41,x41) % 118.33/118.42 [5]P4(x51,x51) % 118.33/118.42 [6]P6(x61,x61) % 118.33/118.42 [9]~P1(x91)+P1(f9(x91)) % 118.33/118.42 [12]~P1(x121)+P2(f8(f10(a2)),f6(x121)) % 118.33/118.42 [13]~P1(x131)+P6(f6(x131),f8(f11(x131))) % 118.33/118.42 [14]~P1(x141)+P2(f6(f9(x141)),f6(x141)) % 118.33/118.42 [15]~P4(x151,x152)+P3(f11(x151),f11(x152)) % 118.33/118.42 [16]~P3(x161,x162)+P3(f10(x161),f10(x162)) % 118.33/118.42 [17]~P4(x171,x172)+P4(f9(x171),f9(x172)) % 118.33/118.42 [18]~P4(x181,x182)+P6(f6(x181),f6(x182)) % 118.33/118.42 [19]~P3(x191,x192)+P6(f8(x191),f8(x192)) % 118.33/118.42 [20]~P5(x201,x202)+P2(f8(x201),f8(x202)) % 118.33/118.42 [21]P5(x211,x212)+~P2(f8(x211),f8(x212)) % 118.33/118.42 [10]~P4(x102,x101)+P1(x101)+~P1(x102) % 118.33/118.42 [25]~P1(x251)+~P6(f6(x251),f8(x252))+~P5(x252,a5) % 118.33/118.42 [22]~P3(x223,x221)+P3(x221,x222)+~P3(x223,x222) % 118.33/118.42 [23]~P4(x233,x231)+P4(x231,x232)+~P4(x233,x232) % 118.33/118.42 [24]~P6(x243,x241)+P6(x241,x242)+~P6(x243,x242) % 118.33/118.42 [26]~P5(x264,x263)+P5(x261,x262)+~P3(x263,x262)+~P3(x264,x261) % 118.33/118.42 [27]~P2(x274,x273)+P2(x271,x272)+~P6(x273,x272)+~P6(x274,x271) % 118.33/118.42 %EqnAxiom % 118.33/118.42 % 118.33/118.42 %------------------------------------------- % 118.33/118.43 cnf(46,plain, % 118.33/118.43 (P1(f9(a3))), % 118.33/118.43 inference(scs_inference,[],[2,5,9,10])). % 118.33/118.43 cnf(58,plain, % 118.33/118.43 (P6(f8(a5),f6(a4))), % 118.33/118.43 inference(scs_inference,[],[8,6,24])). % 118.33/118.43 cnf(86,plain, % 118.33/118.43 (P1(f9(a1))), % 118.33/118.43 inference(scs_inference,[],[1,5,9,10])). % 118.33/118.43 cnf(98,plain, % 118.33/118.43 (P6(f6(a1),f8(f11(a1)))), % 118.33/118.43 inference(scs_inference,[],[1,5,13,10])). % 118.33/118.43 cnf(111,plain, % 118.33/118.43 (P6(x1111,x1111)), % 118.33/118.43 inference(rename_variables,[],[6])). % 118.33/118.43 cnf(113,plain, % 118.33/118.43 (~P2(f6(a1),x1131)+P2(f8(f11(a1)),x1131)), % 118.33/118.43 inference(scs_inference,[],[98,6,111,24,27])). % 118.33/118.43 cnf(163,plain, % 118.33/118.43 (~P5(f11(a4),a5)), % 118.33/118.43 inference(scs_inference,[],[3,13,25])). % 118.33/118.43 cnf(166,plain, % 118.33/118.43 (~P2(f8(f11(a1)),f8(a5))), % 118.33/118.43 inference(scs_inference,[],[98,1,21,25])). % 118.33/118.43 cnf(756,plain, % 118.33/118.43 (~P5(x7561,a5)+~P6(f6(f9(a1)),f8(x7561))), % 118.33/118.43 inference(scs_inference,[],[1,9,25])). % 118.33/118.43 cnf(760,plain, % 118.33/118.43 (~P6(f6(f9(a1)),f8(x7601))+~P2(f8(x7601),f8(a5))), % 118.33/118.43 inference(scs_inference,[],[756,21])). % 118.33/118.43 cnf(762,plain, % 118.33/118.43 (P1(f9(a4))), % 118.33/118.43 inference(scs_inference,[],[3,5,9,10])). % 118.33/118.43 cnf(763,plain, % 118.33/118.43 (P2(f8(f10(a2)),f6(a4))), % 118.33/118.43 inference(scs_inference,[],[3,5,10,12])). % 118.33/118.43 cnf(769,plain, % 118.33/118.43 (P5(f10(a2),a5)), % 118.33/118.43 inference(scs_inference,[],[763,6,8,27,760,21])). % 118.33/118.43 cnf(2153,plain, % 118.33/118.43 (P1(f9(f9(a3)))), % 118.33/118.43 inference(scs_inference,[],[46,9])). % 118.33/118.43 cnf(2161,plain, % 118.33/118.43 (~P2(f8(f11(a4)),f8(a5))), % 118.33/118.43 inference(scs_inference,[],[2,46,163,9,13,14,12,21])). % 118.33/118.43 cnf(2163,plain, % 118.33/118.43 (~P2(f8(f11(a1)),f6(a4))), % 118.33/118.43 inference(scs_inference,[],[2,46,166,163,8,6,9,13,14,12,21,27])). % 118.33/118.43 cnf(2168,plain, % 118.33/118.43 (P2(f6(f9(a4)),f6(a4))), % 118.33/118.43 inference(scs_inference,[],[762,3,9,14])). % 118.33/118.43 cnf(2170,plain, % 118.33/118.43 (P6(f6(a4),f8(f11(a4)))), % 118.33/118.43 inference(scs_inference,[],[762,3,9,14,13])). % 118.33/118.43 cnf(2174,plain, % 118.33/118.43 (~P2(f8(f11(a4)),f6(a4))), % 118.33/118.43 inference(scs_inference,[],[2163,2161,762,3,8,6,9,14,13,113,27])). % 118.33/118.43 cnf(2180,plain, % 118.33/118.43 (P1(f9(f9(a1)))), % 118.33/118.43 inference(scs_inference,[],[86,9])). % 118.33/118.43 cnf(2193,plain, % 118.33/118.43 (P6(f8(f11(a4)),f6(a4))), % 118.33/118.43 inference(scs_inference,[],[2170,6,24])). % 118.33/118.43 cnf(2217,plain, % 118.33/118.43 (~P2(f6(a4),f8(f11(a4)))), % 118.33/118.43 inference(scs_inference,[],[2174,2193,2170,27])). % 118.33/118.43 cnf(2224,plain, % 118.33/118.43 (~P2(f8(a5),f8(f11(a4)))), % 118.33/118.43 inference(scs_inference,[],[6,2217,58,27])). % 118.33/118.43 cnf(3009,plain, % 118.33/118.43 (P1(f9(f9(f9(a3))))), % 118.33/118.43 inference(scs_inference,[],[2153,12,13,14,9])). % 118.33/118.43 cnf(3011,plain, % 118.33/118.43 (~P6(f6(f9(f9(a3))),f8(f10(a2)))), % 118.33/118.43 inference(scs_inference,[],[2153,769,12,13,14,9,25])). % 118.33/118.43 cnf(3032,plain, % 118.33/118.43 (P6(f6(f9(a4)),f8(f11(f9(a4))))), % 118.33/118.43 inference(scs_inference,[],[2180,762,12,13])). % 118.33/118.43 cnf(3051,plain, % 118.33/118.43 (P2(f8(f11(f9(a4))),f6(a4))), % 118.33/118.43 inference(scs_inference,[],[2168,3009,3032,46,769,6,14,12,9,25,27])). % 118.33/118.43 cnf(3113,plain, % 118.33/118.43 (~P5(f11(f9(a4)),a5)), % 118.33/118.43 inference(scs_inference,[],[6,762,2224,3032,3011,20,24,25])). % 118.33/118.43 cnf(3303,plain, % 118.33/118.43 ($false), % 118.33/118.43 inference(scs_inference,[],[8,6,3051,3113,27,21]), % 118.33/118.43 ['proof']). % 118.33/118.43 % SZS output end Proof % 118.33/118.43 % Total time :117.890000s %------------------------------------------------------------------------------