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