%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN628-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 : n017.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 116.90s 116.89s % Output : CNFRefutation 116.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN628-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n017.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 21:58:24 EDT 2024 % 0.13/0.33 % CPUTime : % 0.47/0.60 start to proof:theBenchmark % 116.90/116.87 %------------------------------------------- % 116.90/116.87 % File :CSE---1.7 % 116.90/116.87 % Problem :theBenchmark % 116.90/116.87 % Transform :cnf % 116.90/116.87 % Format :tptp:raw % 116.90/116.87 % Command :java -jar mcs_scs.jar %d %s % 116.90/116.87 % 116.90/116.87 % Result :Theorem 116.230000s % 116.90/116.87 % Output :CNFRefutation 116.230000s % 116.90/116.87 %------------------------------------------- % 116.90/116.88 %-------------------------------------------------------------------------- % 116.90/116.88 % File : SYN628-1 : TPTP v8.2.0. Released v2.5.0. % 116.90/116.88 % Domain : Syntactic % 116.90/116.88 % Problem : Harrison problem 4091 % 116.90/116.88 % Version : Especial. % 116.90/116.88 % English : % 116.90/116.88 % 116.90/116.88 % Refs : [Har01] Email to G. Sutcliffe % 116.90/116.88 % Source : [Har01] % 116.90/116.88 % Names : % 116.90/116.88 % 116.90/116.88 % Status : Unsatisfiable % 116.90/116.88 % Rating : 0.18 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.1.0, 0.29 v6.0.0, 0.44 v5.5.0, 0.38 v5.4.0, 0.39 v5.3.0, 0.45 v5.2.0, 0.38 v5.0.0, 0.33 v4.1.0, 0.40 v4.0.1, 0.57 v4.0.0, 0.43 v3.7.0, 0.29 v3.4.0, 0.20 v3.3.0, 0.00 v3.2.0, 0.33 v3.1.0, 0.00 v2.7.0, 0.25 v2.6.0, 0.33 v2.5.0 % 116.90/116.88 % Syntax : Number of clauses : 36 ( 15 unt; 0 nHn; 31 RR) % 116.90/116.88 % Number of literals : 75 ( 0 equ; 41 neg) % 116.90/116.88 % Maximal clause size : 4 ( 2 avg) % 116.90/116.88 % Maximal term depth : 6 ( 1 avg) % 116.90/116.88 % Number of predicates : 8 ( 8 usr; 0 prp; 2-2 aty) % 116.90/116.88 % Number of functors : 20 ( 20 usr; 8 con; 0-2 aty) % 116.90/116.88 % Number of variables : 69 ( 0 sgn) % 116.90/116.88 % SPC : CNF_UNS_RFO_NEQ_HRN % 116.90/116.88 % 116.90/116.88 % Comments : % 116.90/116.88 %-------------------------------------------------------------------------- % 116.90/116.88 cnf(p2_1,negated_conjecture, % 116.90/116.88 p2(X4,X4) ). % 116.90/116.88 % 116.90/116.88 cnf(p9_2,negated_conjecture, % 116.90/116.88 p9(X40,X40) ). % 116.90/116.88 % 116.90/116.88 cnf(p6_3,negated_conjecture, % 116.90/116.88 p6(X33,X33) ). % 116.90/116.88 % 116.90/116.88 cnf(p5_4,negated_conjecture, % 116.90/116.88 p5(X24,X24) ). % 116.90/116.88 % 116.90/116.88 cnf(p3_5,negated_conjecture, % 116.90/116.88 p3(X19,X19) ). % 116.90/116.88 % 116.90/116.88 cnf(p9_6,negated_conjecture, % 116.90/116.88 p9(c28,c22) ). % 116.90/116.88 % 116.90/116.88 cnf(p20_7,negated_conjecture, % 116.90/116.88 p20(c22,c28) ). % 116.90/116.88 % 116.90/116.88 cnf(p20_8,negated_conjecture, % 116.90/116.88 p20(c28,c26) ). % 116.90/116.88 % 116.90/116.88 cnf(p21_9,negated_conjecture, % 116.90/116.88 p21(c27,c22) ). % 116.90/116.88 % 116.90/116.88 cnf(p19_10,negated_conjecture, % 116.90/116.89 p19(c22,f4(f7(c23,f8(c24,c25)))) ). % 116.90/116.89 % 116.90/116.89 cnf(p19_11,negated_conjecture, % 116.90/116.89 p19(c27,f4(f7(c23,f8(c24,c25)))) ). % 116.90/116.89 % 116.90/116.89 cnf(p19_12,negated_conjecture, % 116.90/116.89 p19(c26,f4(f7(c23,f8(c24,c25)))) ). % 116.90/116.89 % 116.90/116.89 cnf(p9_13,negated_conjecture, % 116.90/116.89 ( p9(f16(X53),f16(X54)) % 116.90/116.89 | ~ p9(X53,X54) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p3_14,negated_conjecture, % 116.90/116.89 ( p3(f4(X22),f4(X23)) % 116.90/116.89 | ~ p2(X22,X23) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p5_15,negated_conjecture, % 116.90/116.89 ( p5(f12(X27),f12(X28)) % 116.90/116.89 | ~ p5(X27,X28) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p5_16,negated_conjecture, % 116.90/116.89 ( p5(f13(X29),f13(X30)) % 116.90/116.89 | ~ p5(X29,X30) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p5_17,negated_conjecture, % 116.90/116.89 ( p5(f14(X31),f14(X32)) % 116.90/116.89 | ~ p5(X31,X32) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p9_18,negated_conjecture, % 116.90/116.89 ( p9(f11(X47),f11(X48)) % 116.90/116.89 | ~ p5(X47,X48) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p2_19,negated_conjecture, % 116.90/116.89 ( p2(X5,X6) % 116.90/116.89 | ~ p2(X4,X5) % 116.90/116.89 | ~ p2(X4,X6) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p9_20,negated_conjecture, % 116.90/116.89 ( p9(X41,X42) % 116.90/116.89 | ~ p9(X40,X41) % 116.90/116.89 | ~ p9(X40,X42) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p6_21,negated_conjecture, % 116.90/116.89 ( p6(X34,X35) % 116.90/116.89 | ~ p6(X33,X34) % 116.90/116.89 | ~ p6(X33,X35) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p5_22,negated_conjecture, % 116.90/116.89 ( p5(X25,X26) % 116.90/116.89 | ~ p5(X24,X25) % 116.90/116.89 | ~ p5(X24,X26) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p3_23,negated_conjecture, % 116.90/116.89 ( p3(X20,X21) % 116.90/116.89 | ~ p3(X19,X20) % 116.90/116.89 | ~ p3(X19,X21) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p19_24,negated_conjecture, % 116.90/116.89 ( p19(X0,X1) % 116.90/116.89 | ~ p3(X3,X1) % 116.90/116.89 | ~ p9(X2,X0) % 116.90/116.89 | ~ p19(X2,X3) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p21_25,negated_conjecture, % 116.90/116.89 ( p21(X15,X16) % 116.90/116.89 | ~ p9(X17,X15) % 116.90/116.89 | ~ p9(X18,X16) % 116.90/116.89 | ~ p21(X17,X18) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p20_26,negated_conjecture, % 116.90/116.89 ( p20(X11,X12) % 116.90/116.89 | ~ p9(X13,X11) % 116.90/116.89 | ~ p9(X14,X12) % 116.90/116.89 | ~ p20(X13,X14) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p2_27,negated_conjecture, % 116.90/116.89 ( p2(f7(X7,X8),f7(X9,X10)) % 116.90/116.89 | ~ p5(X7,X9) % 116.90/116.89 | ~ p6(X8,X10) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p9_28,negated_conjecture, % 116.90/116.89 ( p9(f18(X59,X60),f18(X61,X62)) % 116.90/116.89 | ~ p9(X59,X61) % 116.90/116.89 | ~ p9(X60,X62) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p9_29,negated_conjecture, % 116.90/116.89 ( p9(f17(X55,X56),f17(X57,X58)) % 116.90/116.89 | ~ p9(X55,X57) % 116.90/116.89 | ~ p9(X56,X58) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p9_30,negated_conjecture, % 116.90/116.89 ( p9(f15(X49,X50),f15(X51,X52)) % 116.90/116.89 | ~ p2(X49,X51) % 116.90/116.89 | ~ p9(X50,X52) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p9_31,negated_conjecture, % 116.90/116.89 ( p9(f10(X43,X44),f10(X45,X46)) % 116.90/116.89 | ~ p9(X43,X45) % 116.90/116.89 | ~ p9(X44,X46) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p6_32,negated_conjecture, % 116.90/116.89 ( p6(f8(X36,X37),f8(X38,X39)) % 116.90/116.89 | ~ p5(X36,X38) % 116.90/116.89 | ~ p5(X37,X39) ) ). % 116.90/116.89 % 116.90/116.89 cnf(not_p21_33,negated_conjecture, % 116.90/116.89 ( ~ p21(X63,c26) % 116.90/116.89 | ~ p21(c22,X63) % 116.90/116.89 | ~ p19(X63,f4(f7(c23,f8(c24,c25)))) ) ). % 116.90/116.89 % 116.90/116.89 cnf(p20_34,negated_conjecture, % 116.90/116.89 p20(f16(f17(c28,c27)),f10(f15(f7(c23,f8(c24,c25)),c28),f11(f12(f13(f14(c29)))))) ). % 116.90/116.89 % 116.90/116.89 cnf(not_p20_35,negated_conjecture, % 116.90/116.89 ~ p20(f16(f17(c22,c27)),f10(f15(f7(c23,f8(c24,c25)),c22),f11(f12(f13(f14(c29)))))) ). % 116.90/116.89 % 116.90/116.89 cnf(p20_36,negated_conjecture, % 116.90/116.89 p20(f15(f7(c23,f8(c24,c25)),c28),f18(f11(f12(f13(f14(c29)))),f15(f7(c23,f8(c24,c25)),c22))) ). % 116.90/116.89 % 116.90/116.89 %-------------------------------------------------------------------------- % 116.90/116.89 %------------------------------------------- % 116.90/116.89 % Proof found % 116.90/116.89 % SZS status Theorem for theBenchmark % 116.90/116.89 % SZS output start Proof % 116.90/116.89 %ClaNum:36(EqnAxiom:0) % 116.90/116.89 %VarNum:139(SingletonVarNum:69) % 116.90/116.89 %MaxLitNum:4 % 116.90/116.89 %MaxfuncDepth:5 % 116.90/116.89 %SharedTerms:34 % 116.90/116.89 %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 % 116.90/116.89 %singleGoalClaCount:15 % 116.90/116.89 [1]P1(a1,a2) % 116.90/116.89 [2]P2(a1,a3) % 116.90/116.89 [3]P2(a2,a1) % 116.90/116.89 [4]P5(a7,a2) % 116.90/116.89 [10]P4(a2,f10(f9(a4,f8(a5,a6)))) % 116.90/116.89 [11]P4(a3,f10(f9(a4,f8(a5,a6)))) % 116.90/116.89 [12]P4(a7,f10(f9(a4,f8(a5,a6)))) % 116.90/116.89 [14]P2(f13(f9(a4,f8(a5,a6)),a1),f20(f18(f17(f16(f15(a14)))),f13(f9(a4,f8(a5,a6)),a2))) % 116.90/116.89 [13]P2(f12(f11(a1,a7)),f19(f13(f9(a4,f8(a5,a6)),a1),f18(f17(f16(f15(a14)))))) % 116.90/116.89 [15]~P2(f12(f11(a2,a7)),f19(f13(f9(a4,f8(a5,a6)),a2),f18(f17(f16(f15(a14)))))) % 116.90/116.89 [5]P3(x51,x51) % 116.90/116.89 [6]P1(x61,x61) % 116.90/116.89 [7]P6(x71,x71) % 116.90/116.89 [8]P7(x81,x81) % 116.90/116.89 [9]P8(x91,x91) % 116.90/116.89 [16]~P1(x161,x162)+P1(f12(x161),f12(x162)) % 116.90/116.89 [17]~P7(x171,x172)+P1(f18(x171),f18(x172)) % 116.90/116.89 [18]~P7(x181,x182)+P7(f17(x181),f17(x182)) % 116.90/116.89 [19]~P7(x191,x192)+P7(f16(x191),f16(x192)) % 116.90/116.89 [20]~P7(x201,x202)+P7(f15(x201),f15(x202)) % 116.90/116.89 [21]~P3(x211,x212)+P8(f10(x211),f10(x212)) % 116.90/116.89 [36]~P5(a2,x361)+~P5(x361,a3)+~P4(x361,f10(f9(a4,f8(a5,a6)))) % 116.90/116.89 [22]~P3(x223,x221)+P3(x221,x222)+~P3(x223,x222) % 116.90/116.89 [23]~P1(x233,x231)+P1(x231,x232)+~P1(x233,x232) % 116.90/116.89 [24]~P6(x243,x241)+P6(x241,x242)+~P6(x243,x242) % 116.90/116.89 [25]~P7(x253,x251)+P7(x251,x252)+~P7(x253,x252) % 116.90/116.89 [26]~P8(x263,x261)+P8(x261,x262)+~P8(x263,x262) % 116.90/116.89 [30]~P6(x302,x304)+~P7(x301,x303)+P3(f9(x301,x302),f9(x303,x304)) % 116.90/116.89 [31]~P1(x312,x314)+~P1(x311,x313)+P1(f20(x311,x312),f20(x313,x314)) % 116.90/116.89 [32]~P1(x322,x324)+~P1(x321,x323)+P1(f11(x321,x322),f11(x323,x324)) % 116.90/116.89 [33]~P3(x331,x333)+~P1(x332,x334)+P1(f13(x331,x332),f13(x333,x334)) % 116.90/116.89 [34]~P1(x342,x344)+~P1(x341,x343)+P1(f19(x341,x342),f19(x343,x344)) % 116.90/116.89 [35]~P7(x352,x354)+~P7(x351,x353)+P6(f8(x351,x352),f8(x353,x354)) % 116.90/116.89 [27]~P2(x274,x273)+P2(x271,x272)+~P1(x273,x272)+~P1(x274,x271) % 116.90/116.89 [28]~P5(x284,x283)+P5(x281,x282)+~P1(x283,x282)+~P1(x284,x281) % 116.90/116.89 [29]~P4(x293,x294)+P4(x291,x292)+~P1(x293,x291)+~P8(x294,x292) % 116.90/116.89 %EqnAxiom % 116.90/116.89 % 116.90/116.89 %------------------------------------------- % 116.90/116.91 cnf(153,plain, % 116.90/116.91 (P1(f13(x1531,a1),f13(x1531,a2))), % 116.90/116.91 inference(scs_inference,[],[5,1,22,33])). % 116.90/116.91 cnf(2188,plain, % 116.90/116.91 (P1(f12(a1),f12(a2))), % 116.90/116.91 inference(scs_inference,[],[1,16])). % 116.90/116.91 cnf(2190,plain, % 116.90/116.91 (P1(f20(a1,a1),f20(a2,a2))), % 116.90/116.91 inference(scs_inference,[],[1,16,31])). % 116.90/116.91 cnf(2192,plain, % 116.90/116.91 (P1(f11(a1,a1),f11(a2,a2))), % 116.90/116.91 inference(scs_inference,[],[1,16,31,32])). % 116.90/116.91 cnf(2202,plain, % 116.90/116.91 (P1(f19(f11(a1,a1),f11(a1,a1)),f19(f11(a2,a2),f11(a2,a2)))), % 116.90/116.91 inference(scs_inference,[],[2192,2188,16,34])). % 116.90/116.91 cnf(2208,plain, % 116.90/116.91 (~P1(x22081,f19(f13(f9(a4,f8(a5,a6)),a2),f18(f17(f16(f15(a14))))))+~P2(f12(f11(a2,a7)),x22081)), % 116.90/116.91 inference(scs_inference,[],[2192,2190,2188,15,6,16,34,31,32,27])). % 116.90/116.91 cnf(2211,plain, % 116.90/116.91 (~P2(f12(f11(a2,a7)),f19(f13(f9(a4,f8(a5,a6)),a1),f18(f17(f16(f15(a14))))))), % 116.90/116.91 inference(scs_inference,[],[153,6,2208,34])). % 116.90/116.91 cnf(2233,plain, % 116.90/116.91 (~P1(f12(f11(a1,a7)),f12(f11(a2,a7)))), % 116.90/116.91 inference(scs_inference,[],[2202,2211,13,6,16,34,31,32,27])). % 116.90/116.91 cnf(4502,plain, % 116.90/116.91 ($false), % 116.90/116.91 inference(scs_inference,[],[1,6,2233,16,32]), % 116.90/116.91 ['proof']). % 116.90/116.91 % SZS output end Proof % 116.90/116.91 % Total time :116.230000s %------------------------------------------------------------------------------