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