%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN620-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 : n028.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:07 EDT 2024 % Result : Unsatisfiable 59.78s 59.86s % Output : CNFRefutation 59.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN620-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.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 22:14:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 59.78/59.85 %------------------------------------------- % 59.78/59.85 % File :CSE---1.7 % 59.78/59.85 % Problem :theBenchmark % 59.78/59.85 % Transform :cnf % 59.78/59.85 % Format :tptp:raw % 59.78/59.85 % Command :java -jar mcs_scs.jar %d %s % 59.78/59.85 % 59.78/59.85 % Result :Theorem 59.230000s % 59.78/59.85 % Output :CNFRefutation 59.230000s % 59.78/59.85 %------------------------------------------- % 59.78/59.86 %-------------------------------------------------------------------------- % 59.78/59.86 % File : SYN620-1 : TPTP v8.2.0. Released v2.5.0. % 59.78/59.86 % Domain : Syntactic % 59.78/59.86 % Problem : Harrison problem 3996 % 59.78/59.86 % Version : Especial. % 59.78/59.86 % English : % 59.78/59.86 % 59.78/59.86 % Refs : [Har01] Email to G. Sutcliffe % 59.78/59.86 % Source : [Har01] % 59.78/59.86 % Names : % 59.78/59.86 % 59.78/59.86 % Status : Unsatisfiable % 59.78/59.86 % Rating : 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v5.5.0, 0.25 v5.4.0, 0.20 v5.3.0, 0.10 v5.2.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 59.78/59.86 % Syntax : Number of clauses : 34 ( 13 unt; 1 nHn; 27 RR) % 59.78/59.86 % Number of literals : 72 ( 0 equ; 41 neg) % 59.78/59.86 % Maximal clause size : 4 ( 2 avg) % 59.78/59.86 % Maximal term depth : 6 ( 2 avg) % 59.78/59.86 % Number of predicates : 9 ( 9 usr; 0 prp; 1-2 aty) % 59.78/59.86 % Number of functors : 17 ( 17 usr; 6 con; 0-2 aty) % 59.78/59.86 % Number of variables : 66 ( 1 sgn) % 59.78/59.86 % SPC : CNF_UNS_RFO_NEQ_NHN % 59.78/59.86 % 59.78/59.86 % Comments : % 59.78/59.86 %-------------------------------------------------------------------------- % 59.78/59.86 cnf(p10_1,negated_conjecture, % 59.78/59.86 p10(X0,X0) ). % 59.78/59.86 % 59.78/59.86 cnf(p5_2,negated_conjecture, % 59.78/59.86 p5(X56,X56) ). % 59.78/59.86 % 59.78/59.86 cnf(p3_3,negated_conjecture, % 59.78/59.86 p3(X45,X45) ). % 59.78/59.86 % 59.78/59.86 cnf(p2_4,negated_conjecture, % 59.78/59.86 p2(X33,X33) ). % 59.78/59.86 % 59.78/59.86 cnf(p11_5,negated_conjecture, % 59.78/59.86 p11(X20,X20) ). % 59.78/59.86 % 59.78/59.86 cnf(f6_is_not_p18_6,negated_conjecture, % 59.78/59.86 ~ p18(f6(c24)) ). % 59.78/59.86 % 59.78/59.86 cnf(f6_is_not_p18_7,negated_conjecture, % 59.78/59.86 ~ p18(f6(c22)) ). % 59.78/59.86 % 59.78/59.86 cnf(p3_8,negated_conjecture, % 59.78/59.86 p3(f4(c22),c23) ). % 59.78/59.86 % 59.78/59.86 cnf(p19_9,negated_conjecture, % 59.78/59.86 p19(f7(f8(f9(c25))),c23) ). % 59.78/59.86 % 59.78/59.86 cnf(p18_10,negated_conjecture, % 59.78/59.86 ( p18(X27) % 59.78/59.86 | ~ p18(X28) % 59.78/59.86 | ~ p5(X28,X27) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p10_11,negated_conjecture, % 59.78/59.86 ( p10(f14(X10),f14(X11)) % 59.78/59.86 | ~ p11(X10,X11) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p5_12,negated_conjecture, % 59.78/59.86 ( p5(f6(X59),f6(X60)) % 59.78/59.86 | ~ p2(X59,X60) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p3_13,negated_conjecture, % 59.78/59.86 ( p3(f9(X54),f9(X55)) % 59.78/59.86 | ~ p3(X54,X55) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p3_14,negated_conjecture, % 59.78/59.86 ( p3(f8(X52),f8(X53)) % 59.78/59.86 | ~ p3(X52,X53) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p3_15,negated_conjecture, % 59.78/59.86 ( p3(f7(X50),f7(X51)) % 59.78/59.86 | ~ p3(X50,X51) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p3_16,negated_conjecture, % 59.78/59.86 ( p3(f4(X48),f4(X49)) % 59.78/59.86 | ~ p2(X48,X49) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p11_17,negated_conjecture, % 59.78/59.86 ( p11(f15(X25),f15(X26)) % 59.78/59.86 | ~ p3(X25,X26) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p11_18,negated_conjecture, % 59.78/59.86 ( p11(f12(X23),f12(X24)) % 59.78/59.86 | ~ p10(X23,X24) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p10_19,negated_conjecture, % 59.78/59.86 ( p10(X1,X2) % 59.78/59.86 | ~ p10(X0,X1) % 59.78/59.86 | ~ p10(X0,X2) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p5_20,negated_conjecture, % 59.78/59.86 ( p5(X57,X58) % 59.78/59.86 | ~ p5(X56,X57) % 59.78/59.86 | ~ p5(X56,X58) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p3_21,negated_conjecture, % 59.78/59.86 ( p3(X46,X47) % 59.78/59.86 | ~ p3(X45,X46) % 59.78/59.86 | ~ p3(X45,X47) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p2_22,negated_conjecture, % 59.78/59.86 ( p2(X34,X35) % 59.78/59.86 | ~ p2(X33,X34) % 59.78/59.86 | ~ p2(X33,X35) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p11_23,negated_conjecture, % 59.78/59.86 ( p11(X21,X22) % 59.78/59.86 | ~ p11(X20,X21) % 59.78/59.86 | ~ p11(X20,X22) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p10_24,negated_conjecture, % 59.78/59.86 p10(f13(f6(c22),X9),f13(f6(c24),f16(c26,X9))) ). % 59.78/59.86 % 59.78/59.86 cnf(not_p10_25,negated_conjecture, % 59.78/59.86 ~ p10(f13(f6(c22),f14(f15(f7(c25)))),f14(f15(f7(c25)))) ). % 59.78/59.86 % 59.78/59.86 cnf(p21_26,negated_conjecture, % 59.78/59.86 ( p21(X41,X42) % 59.78/59.86 | ~ p3(X43,X41) % 59.78/59.86 | ~ p3(X44,X42) % 59.78/59.86 | ~ p21(X43,X44) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p19_27,negated_conjecture, % 59.78/59.86 ( p19(X29,X30) % 59.78/59.86 | ~ p3(X31,X29) % 59.78/59.86 | ~ p3(X32,X30) % 59.78/59.86 | ~ p19(X31,X32) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p20_28,negated_conjecture, % 59.78/59.86 ( p20(X36,X37) % 59.78/59.86 | ~ p11(X39,X37) % 59.78/59.86 | ~ p20(X38,X39) % 59.78/59.86 | ~ p11(X38,X36) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p10_29,negated_conjecture, % 59.78/59.86 ( p10(f13(X3,X4),f13(X5,X6)) % 59.78/59.86 | ~ p10(X4,X6) % 59.78/59.86 | ~ p5(X3,X5) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p10_30,negated_conjecture, % 59.78/59.86 ( p10(f17(X16,X17),f17(X18,X19)) % 59.78/59.86 | ~ p2(X17,X19) % 59.78/59.86 | ~ p3(X16,X18) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p10_31,negated_conjecture, % 59.78/59.86 ( p10(f16(X12,X13),f16(X14,X15)) % 59.78/59.86 | ~ p10(X12,X14) % 59.78/59.86 | ~ p10(X13,X15) ) ). % 59.78/59.86 % 59.78/59.86 cnf(p20_32,negated_conjecture, % 59.78/59.86 p20(f12(f13(f6(c22),f14(f15(f7(c25))))),f12(f13(f6(c24),X40))) ). % 59.78/59.86 % 59.78/59.86 cnf(not_p20_33,negated_conjecture, % 59.78/59.86 ~ p20(f12(f13(f6(c22),f14(f15(f7(c25))))),f12(f13(f6(c22),c27))) ). % 59.78/59.86 % 59.78/59.86 cnf(p18_34,negated_conjecture, % 59.78/59.86 ( p18(f6(X7)) % 59.78/59.86 | p10(f13(f6(X7),f17(X8,X7)),f14(f15(f7(c25)))) % 59.78/59.86 | ~ p21(X8,c23) % 59.78/59.86 | ~ p3(f4(X7),X8) ) ). % 59.78/59.86 % 59.78/59.86 %-------------------------------------------------------------------------- % 59.78/59.86 %------------------------------------------- % 59.78/59.86 % Proof found % 59.78/59.86 % SZS status Theorem for theBenchmark % 59.78/59.87 % SZS output start Proof % 59.78/59.87 %ClaNum:34(EqnAxiom:0) % 59.78/59.87 %VarNum:134(SingletonVarNum:66) % 59.78/59.87 %MaxLitNum:4 % 59.78/59.87 %MaxfuncDepth:5 % 59.78/59.87 %SharedTerms:25 % 59.78/59.87 %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 % 59.78/59.87 %singleGoalClaCount:13 % 59.78/59.87 [6]P3(f2(a1),a3) % 59.78/59.87 [10]~P7(f17(a5)) % 59.78/59.87 [11]~P7(f17(a1)) % 59.78/59.87 [7]P6(f16(f15(f14(a4))),a3) % 59.78/59.87 [12]~P1(f6(f17(a1),f12(f11(f16(a4)))),f12(f11(f16(a4)))) % 59.78/59.87 [13]~P8(f8(f6(f17(a1),f12(f11(f16(a4))))),f8(f6(f17(a1),a9))) % 59.78/59.87 [1]P1(x11,x11) % 59.78/59.87 [2]P2(x21,x21) % 59.78/59.87 [3]P3(x31,x31) % 59.78/59.87 [4]P4(x41,x41) % 59.78/59.87 [5]P5(x51,x51) % 59.78/59.87 [8]P1(f6(f17(a1),x81),f6(f17(a5),f10(a7,x81))) % 59.78/59.87 [9]P8(f8(f6(f17(a1),f12(f11(f16(a4))))),f8(f6(f17(a5),x91))) % 59.78/59.87 [15]~P5(x151,x152)+P1(f12(x151),f12(x152)) % 59.78/59.87 [16]~P4(x161,x162)+P2(f17(x161),f17(x162)) % 59.78/59.87 [17]~P4(x171,x172)+P3(f2(x171),f2(x172)) % 59.78/59.87 [18]~P3(x181,x182)+P3(f14(x181),f14(x182)) % 59.78/59.87 [19]~P3(x191,x192)+P3(f15(x191),f15(x192)) % 59.78/59.87 [20]~P3(x201,x202)+P3(f16(x201),f16(x202)) % 59.78/59.87 [21]~P3(x211,x212)+P5(f11(x211),f11(x212)) % 59.78/59.87 [22]~P1(x221,x222)+P5(f8(x221),f8(x222)) % 59.78/59.87 [14]~P2(x142,x141)+P7(x141)+~P7(x142) % 59.78/59.87 [23]~P1(x233,x231)+P1(x231,x232)+~P1(x233,x232) % 59.78/59.87 [24]~P2(x243,x241)+P2(x241,x242)+~P2(x243,x242) % 59.78/59.87 [25]~P3(x253,x251)+P3(x251,x252)+~P3(x253,x252) % 59.78/59.87 [26]~P4(x263,x261)+P4(x261,x262)+~P4(x263,x262) % 59.78/59.87 [27]~P5(x273,x271)+P5(x271,x272)+~P5(x273,x272) % 59.78/59.87 [31]~P1(x312,x314)+~P2(x311,x313)+P1(f6(x311,x312),f6(x313,x314)) % 59.78/59.87 [32]~P1(x322,x324)+~P1(x321,x323)+P1(f10(x321,x322),f10(x323,x324)) % 59.78/59.87 [33]~P3(x331,x333)+~P4(x332,x334)+P1(f13(x331,x332),f13(x333,x334)) % 59.78/59.87 [34]~P9(x342,a3)+~P3(f2(x341),x342)+P7(f17(x341))+P1(f6(f17(x341),f13(x342,x341)),f12(f11(f16(a4)))) % 59.78/59.87 [28]~P6(x284,x283)+P6(x281,x282)+~P3(x283,x282)+~P3(x284,x281) % 59.78/59.87 [29]~P9(x294,x293)+P9(x291,x292)+~P3(x293,x292)+~P3(x294,x291) % 59.78/59.87 [30]~P8(x303,x304)+P8(x301,x302)+~P5(x303,x301)+~P5(x304,x302) % 59.78/59.87 %EqnAxiom % 59.78/59.87 % 59.78/59.87 %------------------------------------------- % 59.78/59.87 cnf(38,plain, % 59.78/59.87 (P3(a3,f2(a1))), % 59.78/59.88 inference(scs_inference,[],[6,3,25])). % 59.78/59.88 cnf(73,plain, % 59.78/59.88 (P1(f6(f17(a5),f10(a7,x731)),f6(f17(a1),x731))), % 59.78/59.88 inference(scs_inference,[],[8,1,23])). % 59.78/59.88 cnf(78,plain, % 59.78/59.88 (P1(f12(f11(a3)),f12(f11(f2(a1))))), % 59.78/59.88 inference(scs_inference,[],[38,15,21])). % 59.78/59.88 cnf(80,plain, % 59.78/59.88 (P3(f14(f15(a3)),f14(f15(f2(a1))))), % 59.78/59.88 inference(scs_inference,[],[38,18,19])). % 59.78/59.88 cnf(85,plain, % 59.78/59.88 (P3(f16(f14(a3)),f16(f14(f2(a1))))), % 59.78/59.88 inference(scs_inference,[],[38,20,18])). % 59.78/59.88 cnf(102,plain, % 59.78/59.88 (P1(f12(f11(f2(a1))),f12(f11(a3)))), % 59.78/59.88 inference(scs_inference,[],[78,1,23])). % 59.78/59.88 cnf(106,plain, % 59.78/59.88 (P3(f14(f15(f2(a1))),f14(f15(a3)))), % 59.78/59.88 inference(scs_inference,[],[80,3,25])). % 59.78/59.88 cnf(120,plain, % 59.78/59.88 (P3(f16(f14(f2(a1))),f16(f14(a3)))), % 59.78/59.88 inference(scs_inference,[],[85,3,25])). % 59.78/59.88 cnf(232,plain, % 59.78/59.88 (P3(f16(f15(f2(a1))),f16(f15(a3)))), % 59.78/59.88 inference(scs_inference,[],[6,19,20])). % 59.78/59.88 cnf(237,plain, % 59.78/59.88 (P3(f15(f16(a3)),f15(f16(f2(a1))))), % 59.78/59.88 inference(scs_inference,[],[38,19,20])). % 59.78/59.88 cnf(254,plain, % 59.78/59.88 (P3(f14(f16(a3)),f14(f16(f2(a1))))), % 59.78/59.88 inference(scs_inference,[],[38,20,18])). % 59.78/59.88 cnf(259,plain, % 59.78/59.88 (P3(f16(f14(f14(f15(f2(a1))))),f16(f14(f14(f15(a3)))))), % 59.78/59.88 inference(scs_inference,[],[106,20,18])). % 59.78/59.88 cnf(264,plain, % 59.78/59.88 (P1(f13(f16(a3),x2641),f13(f16(f2(a1)),x2641))), % 59.78/59.88 inference(scs_inference,[],[38,4,20,33])). % 59.78/59.88 cnf(329,plain, % 59.78/59.88 (P3(f14(f16(f2(a1))),f14(f16(a3)))), % 59.78/59.88 inference(scs_inference,[],[254,3,25])). % 59.78/59.88 cnf(454,plain, % 59.78/59.88 (P5(f11(f16(f16(f15(f2(a1))))),f11(f16(f16(f15(a3)))))), % 59.78/59.88 inference(scs_inference,[],[232,20,21])). % 59.78/59.88 cnf(795,plain, % 59.78/59.88 (P1(f6(f17(x7951),f13(f16(a3),x7952)),f6(f17(x7951),f13(f16(f2(a1)),x7952)))), % 59.78/59.88 inference(scs_inference,[],[264,4,31,16])). % 59.78/59.88 cnf(835,plain, % 59.78/59.88 (P1(f6(x8351,f13(f2(a1),x8352)),f6(x8351,f13(a3,x8352)))), % 59.78/59.88 inference(scs_inference,[],[4,6,2,33,31])). % 59.78/59.88 cnf(2383,plain, % 59.78/59.88 (~P5(f8(f6(f17(a5),x23831)),f8(f6(f17(a1),a9)))), % 59.78/59.88 inference(scs_inference,[],[102,12,9,13,259,454,73,5,4,15,18,19,20,21,22,32,33,23,29,30])). % 59.78/59.88 cnf(2686,plain, % 59.78/59.88 (P3(f14(f16(f14(f2(a1)))),f14(f16(f14(a3))))), % 59.78/59.88 inference(scs_inference,[],[795,120,329,22,20,19,18])). % 59.78/59.88 cnf(2745,plain, % 59.78/59.88 (P5(f11(f14(f16(f2(a1)))),f11(f14(f16(a3))))), % 59.78/59.88 inference(scs_inference,[],[2686,835,329,237,22,20,19,18,21])). % 59.78/59.88 cnf(2755,plain, % 59.78/59.88 ($false), % 59.78/59.88 inference(scs_inference,[],[2745,2383,73,15,22]), % 59.78/59.88 ['proof']). % 59.78/59.88 % SZS output end Proof % 59.78/59.88 % Total time :59.230000s %------------------------------------------------------------------------------