%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN631-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:09 EDT 2024 % Result : Unsatisfiable 118.08s 118.17s % Output : CNFRefutation 118.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN631-1 : TPTP v8.2.0. Released v2.5.0. % 0.10/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 19:50:24 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 118.08/118.13 %------------------------------------------- % 118.08/118.13 % File :CSE---1.7 % 118.08/118.13 % Problem :theBenchmark % 118.08/118.13 % Transform :cnf % 118.08/118.13 % Format :tptp:raw % 118.08/118.13 % Command :java -jar mcs_scs.jar %d %s % 118.08/118.13 % 118.08/118.13 % Result :Theorem 117.490000s % 118.08/118.13 % Output :CNFRefutation 117.490000s % 118.08/118.13 %------------------------------------------- % 118.08/118.16 %-------------------------------------------------------------------------- % 118.08/118.16 % File : SYN631-1 : TPTP v8.2.0. Released v2.5.0. % 118.08/118.16 % Domain : Syntactic % 118.08/118.16 % Problem : Harrison problem 4139 % 118.08/118.16 % Version : Especial. % 118.08/118.16 % English : % 118.08/118.16 % 118.08/118.16 % Refs : [Har01] Email to G. Sutcliffe % 118.08/118.16 % Source : [Har01] % 118.08/118.16 % Names : % 118.08/118.16 % 118.08/118.16 % Status : Unsatisfiable % 118.08/118.16 % Rating : 0.27 v8.2.0, 0.29 v8.1.0, 0.25 v7.4.0, 0.33 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.50 v6.0.0, 0.44 v5.5.0, 0.50 v5.3.0, 0.55 v5.2.0, 0.38 v5.1.0, 0.50 v5.0.0, 0.40 v4.1.0, 0.53 v4.0.1, 0.29 v3.4.0, 0.40 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.50 v2.6.0, 0.67 v2.5.0 % 118.08/118.16 % Syntax : Number of clauses : 38 ( 13 unt; 0 nHn; 28 RR) % 118.08/118.16 % Number of literals : 84 ( 0 equ; 47 neg) % 118.08/118.16 % Maximal clause size : 4 ( 2 avg) % 118.08/118.16 % Maximal term depth : 3 ( 1 avg) % 118.08/118.16 % Number of predicates : 11 ( 11 usr; 0 prp; 2-2 aty) % 118.08/118.16 % Number of functors : 17 ( 17 usr; 6 con; 0-3 aty) % 118.08/118.16 % Number of variables : 90 ( 2 sgn) % 118.08/118.16 % SPC : CNF_UNS_RFO_NEQ_HRN % 118.08/118.16 % 118.08/118.16 % Comments : % 118.08/118.16 %-------------------------------------------------------------------------- % 118.08/118.16 cnf(p10_1,negated_conjecture, % 118.08/118.16 p10(X0,X0) ). % 118.08/118.16 % 118.08/118.17 cnf(p9_2,negated_conjecture, % 118.08/118.17 p9(X74,X74) ). % 118.08/118.17 % 118.08/118.17 cnf(p7_3,negated_conjecture, % 118.08/118.17 p7(X65,X65) ). % 118.08/118.17 % 118.08/118.17 cnf(p6_4,negated_conjecture, % 118.08/118.17 p6(X62,X62) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_5,negated_conjecture, % 118.08/118.17 p5(X37,X37) ). % 118.08/118.17 % 118.08/118.17 cnf(p3_6,negated_conjecture, % 118.08/118.17 p3(X32,X32) ). % 118.08/118.17 % 118.08/118.17 cnf(p2_7,negated_conjecture, % 118.08/118.17 p2(X12,X12) ). % 118.08/118.17 % 118.08/118.17 cnf(p12_8,negated_conjecture, % 118.08/118.17 p12(X5,X5) ). % 118.08/118.17 % 118.08/118.17 cnf(p22_9,negated_conjecture, % 118.08/118.17 p22(c25,c28) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_10,negated_conjecture, % 118.08/118.17 p5(f17(f18(X48,X49)),X48) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_11,negated_conjecture, % 118.08/118.17 p5(f16(f18(X44,X45)),X45) ). % 118.08/118.17 % 118.08/118.17 cnf(p23_12,negated_conjecture, % 118.08/118.17 p23(f13(c27,f14(c28)),f11(f15(c24))) ). % 118.08/118.17 % 118.08/118.17 cnf(not_p23_13,negated_conjecture, % 118.08/118.17 ~ p23(f13(f16(c27),f14(c28)),f11(c24)) ). % 118.08/118.17 % 118.08/118.17 cnf(p9_14,negated_conjecture, % 118.08/118.17 ( p9(f15(X77),f15(X78)) % 118.08/118.17 | ~ p9(X77,X78) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p10_15,negated_conjecture, % 118.08/118.17 ( p10(f11(X3),f11(X4)) % 118.08/118.17 | ~ p9(X3,X4) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p3_16,negated_conjecture, % 118.08/118.17 ( p3(f4(X35),f4(X36)) % 118.08/118.17 | ~ p2(X35,X36) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_17,negated_conjecture, % 118.08/118.17 ( p5(f14(X40),f14(X41)) % 118.08/118.17 | ~ p6(X40,X41) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_18,negated_conjecture, % 118.08/118.17 ( p5(f16(X42),f16(X43)) % 118.08/118.17 | ~ p5(X42,X43) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_19,negated_conjecture, % 118.08/118.17 ( p5(f17(X46),f17(X47)) % 118.08/118.17 | ~ p5(X46,X47) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_20,negated_conjecture, % 118.08/118.17 ( p5(f20(X60),f20(X61)) % 118.08/118.17 | ~ p5(X60,X61) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p10_21,negated_conjecture, % 118.08/118.17 ( p10(X1,X2) % 118.08/118.17 | ~ p10(X0,X1) % 118.08/118.17 | ~ p10(X0,X2) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p9_22,negated_conjecture, % 118.08/118.17 ( p9(X75,X76) % 118.08/118.17 | ~ p9(X74,X75) % 118.08/118.17 | ~ p9(X74,X76) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p7_23,negated_conjecture, % 118.08/118.17 ( p7(X66,X67) % 118.08/118.17 | ~ p7(X65,X66) % 118.08/118.17 | ~ p7(X65,X67) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p6_24,negated_conjecture, % 118.08/118.17 ( p6(X63,X64) % 118.08/118.17 | ~ p6(X62,X63) % 118.08/118.17 | ~ p6(X62,X64) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_25,negated_conjecture, % 118.08/118.17 ( p5(X38,X39) % 118.08/118.17 | ~ p5(X37,X38) % 118.08/118.17 | ~ p5(X37,X39) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p3_26,negated_conjecture, % 118.08/118.17 ( p3(X33,X34) % 118.08/118.17 | ~ p3(X32,X33) % 118.08/118.17 | ~ p3(X32,X34) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p2_27,negated_conjecture, % 118.08/118.17 ( p2(X13,X14) % 118.08/118.17 | ~ p2(X12,X13) % 118.08/118.17 | ~ p2(X12,X14) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p12_28,negated_conjecture, % 118.08/118.17 ( p12(X6,X7) % 118.08/118.17 | ~ p12(X5,X6) % 118.08/118.17 | ~ p12(X5,X7) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p23_29,negated_conjecture, % 118.08/118.17 ( p23(X25,X26) % 118.08/118.17 | ~ p12(X28,X25) % 118.08/118.17 | ~ p23(X28,X27) % 118.08/118.17 | ~ p10(X27,X26) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p21_30,negated_conjecture, % 118.08/118.17 ( p21(X15,X16) % 118.08/118.17 | ~ p3(X18,X16) % 118.08/118.17 | ~ p7(X17,X15) % 118.08/118.17 | ~ p21(X17,X18) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p22_31,negated_conjecture, % 118.08/118.17 ( p22(X21,X22) % 118.08/118.17 | ~ p3(X23,X21) % 118.08/118.17 | ~ p6(X24,X22) % 118.08/118.17 | ~ p22(X23,X24) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p12_32,negated_conjecture, % 118.08/118.17 ( p12(f13(X8,X9),f13(X10,X11)) % 118.08/118.17 | ~ p5(X8,X10) % 118.08/118.17 | ~ p5(X9,X11) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_33,negated_conjecture, % 118.08/118.17 ( p5(f18(X50,X51),f18(X52,X53)) % 118.08/118.17 | ~ p5(X50,X52) % 118.08/118.17 | ~ p5(X51,X53) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_34,negated_conjecture, % 118.08/118.17 ( p5(X30,f18(f20(c29),f19(X29,X30,X31))) % 118.08/118.17 | ~ p23(f13(X30,X31),f11(f15(X29))) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p23_35,negated_conjecture, % 118.08/118.17 ( p23(f13(f19(X29,X30,X31),X31),f11(X29)) % 118.08/118.17 | ~ p23(f13(X30,X31),f11(f15(X29))) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p21_36,negated_conjecture, % 118.08/118.17 ( p21(f8(c26,X19,X20),f4(c26)) % 118.08/118.17 | ~ p22(c25,X20) % 118.08/118.17 | ~ p23(f13(X19,f14(X20)),f11(c24)) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p7_37,negated_conjecture, % 118.08/118.17 ( p7(f8(X68,X69,X70),f8(X71,X72,X73)) % 118.08/118.17 | ~ p5(X69,X72) % 118.08/118.17 | ~ p6(X70,X73) % 118.08/118.17 | ~ p2(X68,X71) ) ). % 118.08/118.17 % 118.08/118.17 cnf(p5_38,negated_conjecture, % 118.08/118.17 ( p5(f19(X54,X55,X56),f19(X57,X58,X59)) % 118.08/118.17 | ~ p5(X56,X59) % 118.08/118.17 | ~ p9(X54,X57) % 118.08/118.17 | ~ p5(X55,X58) ) ). % 118.08/118.17 % 118.08/118.17 %-------------------------------------------------------------------------- % 118.08/118.17 %------------------------------------------- % 118.08/118.17 % Proof found % 118.08/118.17 % SZS status Theorem for theBenchmark % 118.08/118.17 % SZS output start Proof % 118.17/118.20 %ClaNum:38(EqnAxiom:0) % 118.17/118.20 %VarNum:182(SingletonVarNum:90) % 118.17/118.20 %MaxLitNum:4 % 118.17/118.20 %MaxfuncDepth:2 % 118.17/118.20 %SharedTerms:18 % 118.17/118.20 %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 28 29 30 31 32 33 34 35 36 37 38 % 118.17/118.20 %singleGoalClaCount:13 % 118.17/118.20 [1]P1(a1,a3) % 118.17/118.20 [10]P11(f7(a4,f6(a3)),f8(f10(a2))) % 118.17/118.20 [13]~P11(f7(f13(a4),f6(a3)),f8(a2)) % 118.17/118.20 [2]P2(x21,x21) % 118.17/118.20 [3]P6(x31,x31) % 118.17/118.20 [4]P7(x41,x41) % 118.17/118.20 [5]P8(x51,x51) % 118.17/118.20 [6]P9(x61,x61) % 118.17/118.20 [7]P10(x71,x71) % 118.17/118.20 [8]P3(x81,x81) % 118.17/118.20 [9]P4(x91,x91) % 118.17/118.20 [11]P9(f12(f11(x111,x112)),x111) % 118.17/118.20 [12]P9(f13(f11(x121,x122)),x122) % 118.17/118.20 [14]~P6(x141,x142)+P2(f8(x141),f8(x142)) % 118.17/118.20 [15]~P6(x151,x152)+P6(f10(x151),f10(x152)) % 118.17/118.20 [16]~P9(x161,x162)+P9(f12(x161),f12(x162)) % 118.17/118.20 [17]~P9(x171,x172)+P9(f13(x171),f13(x172)) % 118.17/118.20 [18]~P8(x181,x182)+P9(f6(x181),f6(x182)) % 118.17/118.20 [19]~P9(x191,x192)+P9(f14(x191),f14(x192)) % 118.17/118.20 [20]~P3(x201,x202)+P10(f16(x201),f16(x202)) % 118.17/118.20 [37]~P11(f7(x372,x373),f8(f10(x371)))+P11(f7(f15(x371,x372,x373),x373),f8(x371)) % 118.17/118.20 [38]~P11(f7(x381,x383),f8(f10(x382)))+P9(x381,f11(f14(a9),f15(x382,x381,x383))) % 118.17/118.20 [34]~P1(a1,x342)+P5(f17(a5,x341,x342),f16(a5))+~P11(f7(x341,f6(x342)),f8(a2)) % 118.17/118.20 [21]~P2(x213,x211)+P2(x211,x212)+~P2(x213,x212) % 118.17/118.20 [22]~P6(x223,x221)+P6(x221,x222)+~P6(x223,x222) % 118.17/118.20 [23]~P7(x233,x231)+P7(x231,x232)+~P7(x233,x232) % 118.17/118.20 [24]~P8(x243,x241)+P8(x241,x242)+~P8(x243,x242) % 118.17/118.20 [25]~P9(x253,x251)+P9(x251,x252)+~P9(x253,x252) % 118.17/118.20 [26]~P10(x263,x261)+P10(x261,x262)+~P10(x263,x262) % 118.17/118.20 [27]~P3(x273,x271)+P3(x271,x272)+~P3(x273,x272) % 118.17/118.20 [28]~P4(x283,x281)+P4(x281,x282)+~P4(x283,x282) % 118.17/118.20 [32]~P9(x322,x324)+~P9(x321,x323)+P9(f11(x321,x322),f11(x323,x324)) % 118.17/118.20 [33]~P9(x332,x334)+~P9(x331,x333)+P4(f7(x331,x332),f7(x333,x334)) % 118.17/118.20 [29]~P1(x294,x293)+P1(x291,x292)+~P8(x293,x292)+~P10(x294,x291) % 118.17/118.20 [30]~P11(x304,x303)+P11(x301,x302)+~P2(x303,x302)+~P4(x304,x301) % 118.17/118.20 [31]~P5(x313,x314)+P5(x311,x312)+~P7(x313,x311)+~P10(x314,x312) % 118.17/118.20 [35]~P8(x353,x356)+~P9(x352,x355)+~P3(x351,x354)+P7(f17(x351,x352,x353),f17(x354,x355,x356)) % 118.17/118.20 [36]~P6(x361,x364)+~P9(x363,x366)+~P9(x362,x365)+P9(f15(x361,x362,x363),f15(x364,x365,x366)) % 118.17/118.20 %EqnAxiom % 118.17/118.20 % 118.20/118.20 %------------------------------------------- % 118.22/118.24 cnf(46,plain, % 118.22/118.24 (P9(x461,f12(f11(x461,x462)))), % 118.22/118.24 inference(scs_inference,[],[11,6,25])). % 118.22/118.24 cnf(50,plain, % 118.22/118.24 (P9(x501,f13(f11(x502,x501)))), % 118.22/118.24 inference(scs_inference,[],[12,6,25])). % 118.22/118.24 cnf(250,plain, % 118.22/118.24 (P9(f11(f14(a9),f15(a2,a4,f6(a3))),a4)), % 118.22/118.24 inference(scs_inference,[],[6,10,25,38])). % 118.22/118.24 cnf(354,plain, % 118.22/118.24 (P11(f7(f15(a2,a4,f6(a3)),f6(a3)),f8(a2))), % 118.22/118.24 inference(scs_inference,[],[10,9,2,37,30])). % 118.22/118.24 cnf(474,plain, % 118.22/118.24 (~P9(f15(a2,a4,f6(a3)),f13(a4))), % 118.22/118.24 inference(scs_inference,[],[354,2,6,13,30,33])). % 118.22/118.24 cnf(786,plain, % 118.22/118.24 (P4(f7(x7861,x7862),f7(f13(f11(x7863,x7861)),x7862))), % 118.22/118.24 inference(scs_inference,[],[6,50,32,33])). % 118.22/118.24 cnf(798,plain, % 118.22/118.24 (P9(f15(x7981,x7982,x7983),f15(x7981,x7982,f12(f11(x7983,x7984))))), % 118.22/118.24 inference(scs_inference,[],[6,786,46,10,2,3,32,33,30,36])). % 118.22/118.24 cnf(810,plain, % 118.22/118.24 (P9(f11(x8101,f12(f11(x8102,x8103))),f11(x8101,x8102))), % 118.22/118.24 inference(scs_inference,[],[6,11,32])). % 118.22/118.24 cnf(1768,plain, % 118.22/118.24 (P9(f13(f11(f14(a9),f15(a2,a4,f6(a3)))),f13(a4))), % 118.22/118.24 inference(scs_inference,[],[250,16,19,17])). % 118.22/118.24 cnf(1921,plain, % 118.22/118.24 ($false), % 118.22/118.24 inference(scs_inference,[],[12,810,798,474,1768,16,19,17,33,25]), % 118.22/118.24 ['proof']). % 118.22/118.25 % SZS output end Proof % 118.22/118.25 % Total time :117.490000s %------------------------------------------------------------------------------