%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN649-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 : 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:12 EDT 2024 % Result : Unsatisfiable 58.55s 58.62s % Output : CNFRefutation 58.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYN649-1 : TPTP v8.2.0. Released v2.5.0. % 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.30 % Computer : n021.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Sun Jun 23 20:48:53 EDT 2024 % 0.11/0.30 % CPUTime : % 0.46/0.55 start to proof:theBenchmark % 58.55/58.60 %------------------------------------------- % 58.55/58.60 % File :CSE---1.7 % 58.55/58.60 % Problem :theBenchmark % 58.55/58.60 % Transform :cnf % 58.55/58.60 % Format :tptp:raw % 58.55/58.60 % Command :java -jar mcs_scs.jar %d %s % 58.55/58.60 % 58.55/58.60 % Result :Theorem 58.000000s % 58.55/58.60 % Output :CNFRefutation 58.000000s % 58.55/58.60 %------------------------------------------- % 58.55/58.61 %-------------------------------------------------------------------------- % 58.55/58.61 % File : SYN649-1 : TPTP v8.2.0. Released v2.5.0. % 58.55/58.61 % Domain : Syntactic % 58.55/58.61 % Problem : Harrison problem 4403 % 58.55/58.61 % Version : Especial. % 58.55/58.61 % English : % 58.55/58.61 % 58.55/58.61 % Refs : [Har01] Email to G. Sutcliffe % 58.55/58.61 % Source : [Har01] % 58.55/58.61 % Names : % 58.55/58.61 % 58.55/58.61 % Status : Unsatisfiable % 58.55/58.61 % Rating : 0.09 v8.2.0, 0.14 v8.1.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.25 v6.2.0, 0.33 v6.1.0, 0.14 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.17 v5.3.0, 0.20 v5.2.0, 0.23 v5.1.0, 0.19 v5.0.0, 0.20 v4.1.0, 0.13 v4.0.1, 0.14 v3.4.0, 0.20 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0 % 58.55/58.61 % Syntax : Number of clauses : 44 ( 13 unt; 0 nHn; 31 RR) % 58.55/58.61 % Number of literals : 100 ( 0 equ; 57 neg) % 58.55/58.61 % Maximal clause size : 4 ( 2 avg) % 58.55/58.61 % Maximal term depth : 6 ( 1 avg) % 58.55/58.61 % Number of predicates : 13 ( 13 usr; 0 prp; 2-2 aty) % 58.55/58.61 % Number of functors : 19 ( 19 usr; 10 con; 0-2 aty) % 58.55/58.61 % Number of variables : 115 ( 2 sgn) % 58.55/58.61 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.55/58.61 % 58.55/58.61 % Comments : % 58.55/58.61 %-------------------------------------------------------------------------- % 58.55/58.61 cnf(p11_1,negated_conjecture, % 58.55/58.61 p11(X0,X0) ). % 58.55/58.61 % 58.55/58.61 cnf(p9_2,negated_conjecture, % 58.55/58.61 p9(X80,X80) ). % 58.55/58.61 % 58.55/58.61 cnf(p8_3,negated_conjecture, % 58.55/58.61 p8(X77,X77) ). % 58.55/58.61 % 58.55/58.61 cnf(p6_4,negated_conjecture, % 58.55/58.61 p6(X70,X70) ). % 58.55/58.61 % 58.55/58.61 cnf(p4_5,negated_conjecture, % 58.55/58.61 p4(X63,X63) ). % 58.55/58.61 % 58.55/58.61 cnf(p3_6,negated_conjecture, % 58.55/58.61 p3(X56,X56) ). % 58.55/58.61 % 58.55/58.61 cnf(p21_7,negated_conjecture, % 58.55/58.61 p21(X38,X38) ). % 58.55/58.61 % 58.55/58.61 cnf(p2_8,negated_conjecture, % 58.55/58.61 p2(X31,X31) ). % 58.55/58.61 % 58.55/58.61 cnf(p19_9,negated_conjecture, % 58.55/58.61 p19(X28,X28) ). % 58.55/58.61 % 58.55/58.61 cnf(p17_10,negated_conjecture, % 58.55/58.61 p17(X21,X21) ). % 58.55/58.61 % 58.55/58.61 cnf(p15_11,negated_conjecture, % 58.55/58.61 p15(X14,X14) ). % 58.55/58.61 % 58.55/58.61 cnf(p13_12,negated_conjecture, % 58.55/58.61 p13(X3,X3) ). % 58.55/58.61 % 58.55/58.61 cnf(p11_13,negated_conjecture, % 58.55/58.61 ( p11(X1,X2) % 58.55/58.61 | ~ p11(X0,X1) % 58.55/58.61 | ~ p11(X0,X2) ) ). % 58.55/58.61 % 58.55/58.61 cnf(p9_14,negated_conjecture, % 58.55/58.61 ( p9(X81,X82) % 58.55/58.61 | ~ p9(X80,X81) % 58.55/58.61 | ~ p9(X80,X82) ) ). % 58.55/58.61 % 58.55/58.61 cnf(p8_15,negated_conjecture, % 58.55/58.61 ( p8(X78,X79) % 58.55/58.61 | ~ p8(X77,X78) % 58.55/58.61 | ~ p8(X77,X79) ) ). % 58.55/58.61 % 58.55/58.61 cnf(p6_16,negated_conjecture, % 58.55/58.61 ( p6(X71,X72) % 58.55/58.61 | ~ p6(X70,X71) % 58.55/58.61 | ~ p6(X70,X72) ) ). % 58.55/58.61 % 58.55/58.61 cnf(p4_17,negated_conjecture, % 58.55/58.61 ( p4(X64,X65) % 58.55/58.61 | ~ p4(X63,X64) % 58.55/58.61 | ~ p4(X63,X65) ) ). % 58.55/58.61 % 58.55/58.61 cnf(p3_18,negated_conjecture, % 58.55/58.61 ( p3(X57,X58) % 58.55/58.61 | ~ p3(X56,X57) % 58.55/58.61 | ~ p3(X56,X58) ) ). % 58.55/58.61 % 58.55/58.61 cnf(p21_19,negated_conjecture, % 58.55/58.61 ( p21(X39,X40) % 58.55/58.61 | ~ p21(X38,X39) % 58.55/58.61 | ~ p21(X38,X40) ) ). % 58.55/58.61 % 58.55/58.61 cnf(p2_20,negated_conjecture, % 58.55/58.61 ( p2(X32,X33) % 58.55/58.61 | ~ p2(X31,X32) % 58.55/58.62 | ~ p2(X31,X33) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p19_21,negated_conjecture, % 58.55/58.62 ( p19(X29,X30) % 58.55/58.62 | ~ p19(X28,X29) % 58.55/58.62 | ~ p19(X28,X30) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p17_22,negated_conjecture, % 58.55/58.62 ( p17(X22,X23) % 58.55/58.62 | ~ p17(X21,X22) % 58.55/58.62 | ~ p17(X21,X23) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p15_23,negated_conjecture, % 58.55/58.62 ( p15(X15,X16) % 58.55/58.62 | ~ p15(X14,X15) % 58.55/58.62 | ~ p15(X14,X16) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p13_24,negated_conjecture, % 58.55/58.62 ( p13(X4,X5) % 58.55/58.62 | ~ p13(X3,X4) % 58.55/58.62 | ~ p13(X3,X5) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_25,negated_conjecture, % 58.55/58.62 ( p23(X41,X42) % 58.55/58.62 | ~ p3(X44,X42) % 58.55/58.62 | ~ p4(X43,X41) % 58.55/58.62 | ~ p23(X43,X44) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_26,negated_conjecture, % 58.55/58.62 p23(f5(f7(f10(c26,f12(c27,f12(c27,c28))),c24),c25),c29) ). % 58.55/58.62 % 58.55/58.62 cnf(p9_27,negated_conjecture, % 58.55/58.62 ( p9(f12(X83,X84),f12(X85,X86)) % 58.55/58.62 | ~ p11(X83,X85) % 58.55/58.62 | ~ p9(X84,X86) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p13_28,negated_conjecture, % 58.55/58.62 ( p13(f16(X6,X7),f16(X8,X9)) % 58.55/58.62 | ~ p15(X6,X8) % 58.55/58.62 | ~ p2(X7,X9) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p13_29,negated_conjecture, % 58.55/58.62 ( p13(f22(X10,X11),f22(X12,X13)) % 58.55/58.62 | ~ p21(X10,X12) % 58.55/58.62 | ~ p3(X11,X13) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p15_30,negated_conjecture, % 58.55/58.62 ( p15(f18(X17,X18),f18(X19,X20)) % 58.55/58.62 | ~ p17(X17,X19) % 58.55/58.62 | ~ p3(X18,X20) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p17_31,negated_conjecture, % 58.55/58.62 ( p17(f20(X24,X25),f20(X26,X27)) % 58.55/58.62 | ~ p19(X24,X26) % 58.55/58.62 | ~ p9(X25,X27) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p2_32,negated_conjecture, % 58.55/58.62 ( p2(f7(X34,X35),f7(X36,X37)) % 58.55/58.62 | ~ p2(X35,X37) % 58.55/58.62 | ~ p6(X34,X36) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p3_33,negated_conjecture, % 58.55/58.62 ( p3(f14(X59,X60),f14(X61,X62)) % 58.55/58.62 | ~ p13(X59,X61) % 58.55/58.62 | ~ p3(X60,X62) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p4_34,negated_conjecture, % 58.55/58.62 ( p4(f5(X66,X67),f5(X68,X69)) % 58.55/58.62 | ~ p2(X66,X68) % 58.55/58.62 | ~ p3(X67,X69) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p6_35,negated_conjecture, % 58.55/58.62 ( p6(f10(X73,X74),f10(X75,X76)) % 58.55/58.62 | ~ p8(X73,X75) % 58.55/58.62 | ~ p9(X74,X76) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p3_36,negated_conjecture, % 58.55/58.62 ( p3(X54,X55) % 58.55/58.62 | ~ p23(f5(f7(f10(c26,f12(c31,c32)),X53),X54),X55) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_37,negated_conjecture, % 58.55/58.62 ( p23(f5(f7(f10(c26,f12(c31,c32)),X53),X54),X55) % 58.55/58.62 | ~ p3(X54,X55) ) ). % 58.55/58.62 % 58.55/58.62 cnf(not_p23_38,negated_conjecture, % 58.55/58.62 ( ~ p23(f5(c24,c25),X87) % 58.55/58.62 | ~ p23(f5(f7(f10(c26,f12(c27,c28)),c24),X87),c29) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_39,negated_conjecture, % 58.55/58.62 ( p23(f5(c24,X49),f14(f22(c33,X50),X49)) % 58.55/58.62 | ~ p23(f5(f7(f10(c26,f12(c27,c28)),c24),X49),X50) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_40,negated_conjecture, % 58.55/58.62 ( p23(f5(X45,f14(f16(f18(f20(c30,X46),X47),X45),X48)),X48) % 58.55/58.62 | ~ p23(f5(f7(f10(c26,f12(c27,X46)),X45),X47),X48) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_41,negated_conjecture, % 58.55/58.62 ( p23(f5(f7(f10(c26,c28),c24),f14(f22(c33,X50),X49)),X50) % 58.55/58.62 | ~ p23(f5(f7(f10(c26,f12(c27,c28)),c24),X49),X50) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_42,negated_conjecture, % 58.55/58.62 ( p23(f5(f7(f10(c26,f12(c27,X46)),X45),X47),X48) % 58.55/58.62 | ~ p23(f5(X45,X51),X48) % 58.55/58.62 | ~ p23(f5(f7(f10(c26,X46),X45),X47),X51) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_43,negated_conjecture, % 58.55/58.62 ( p23(f5(f7(f10(c26,f12(c27,c28)),c24),X49),X50) % 58.55/58.62 | ~ p23(f5(c24,X49),X52) % 58.55/58.62 | ~ p23(f5(f7(f10(c26,c28),c24),X52),X50) ) ). % 58.55/58.62 % 58.55/58.62 cnf(p23_44,negated_conjecture, % 58.55/58.62 ( p23(f5(f7(f10(c26,X46),X45),X47),f14(f16(f18(f20(c30,X46),X47),X45),X48)) % 58.55/58.62 | ~ p23(f5(f7(f10(c26,f12(c27,X46)),X45),X47),X48) ) ). % 58.55/58.62 % 58.55/58.62 %-------------------------------------------------------------------------- % 58.55/58.62 %------------------------------------------- % 58.55/58.62 % Proof found % 58.55/58.62 % SZS status Theorem for theBenchmark % 58.55/58.62 % SZS output start Proof % 58.55/58.62 %ClaNum:44(EqnAxiom:0) % 58.55/58.62 %VarNum:236(SingletonVarNum:115) % 58.55/58.62 %MaxLitNum:4 % 58.55/58.62 %MaxfuncDepth:5 % 58.55/58.62 %SharedTerms:23 % 58.55/58.62 %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 39 40 41 42 43 44 % 58.55/58.62 %singleGoalClaCount:13 % 58.55/58.62 [13]P13(f14(f13(f7(a1,f6(a4,f6(a4,a5))),a2),a3),a8) % 58.55/58.62 [1]P1(x11,x11) % 58.55/58.62 [2]P2(x21,x21) % 58.55/58.62 [3]P3(x31,x31) % 58.55/58.62 [4]P4(x41,x41) % 58.55/58.62 [5]P5(x51,x51) % 58.55/58.62 [6]P6(x61,x61) % 58.55/58.62 [7]P7(x71,x71) % 58.55/58.62 [8]P8(x81,x81) % 58.55/58.62 [9]P9(x91,x91) % 58.55/58.62 [10]P10(x101,x101) % 58.55/58.62 [11]P11(x111,x111) % 58.55/58.62 [12]P12(x121,x121) % 58.55/58.62 [38]~P13(f14(a2,a3),x381)+~P13(f14(f13(f7(a1,f6(a4,a5)),a2),x381),a8) % 58.55/58.62 [39]P13(f14(a2,x391),f15(f19(a12,x392),x391))+~P13(f14(f13(f7(a1,f6(a4,a5)),a2),x391),x392) % 58.55/58.62 [42]P13(f14(f13(f7(a1,a5),a2),f15(f19(a12,x421),x422)),x421)+~P13(f14(f13(f7(a1,f6(a4,a5)),a2),x422),x421) % 58.55/58.62 [36]~P6(x362,x363)+P13(f14(f13(f7(a1,f6(a9,a11)),x361),x362),x363) % 58.55/58.62 [37]P6(x371,x372)+~P13(f14(f13(f7(a1,f6(a9,a11)),x373),x371),x372) % 58.55/58.62 [43]~P13(f14(f13(f7(a1,f6(a4,x431)),x432),x433),x434)+P13(f14(f13(f7(a1,x431),x432),x433),f15(f18(f17(f16(a10,x431),x433),x432),x434)) % 58.55/58.62 [44]~P13(f14(f13(f7(a1,f6(a4,x442)),x441),x443),x444)+P13(f14(x441,f15(f18(f17(f16(a10,x442),x443),x441),x444)),x444) % 58.55/58.62 [14]~P1(x143,x141)+P1(x141,x142)+~P1(x143,x142) % 58.55/58.62 [15]~P2(x153,x151)+P2(x151,x152)+~P2(x153,x152) % 58.55/58.62 [16]~P3(x163,x161)+P3(x161,x162)+~P3(x163,x162) % 58.55/58.62 [17]~P4(x173,x171)+P4(x171,x172)+~P4(x173,x172) % 58.55/58.62 [18]~P5(x183,x181)+P5(x181,x182)+~P5(x183,x182) % 58.55/58.62 [19]~P6(x193,x191)+P6(x191,x192)+~P6(x193,x192) % 58.55/58.62 [20]~P7(x203,x201)+P7(x201,x202)+~P7(x203,x202) % 58.55/58.62 [21]~P8(x213,x211)+P8(x211,x212)+~P8(x213,x212) % 58.55/58.62 [22]~P9(x223,x221)+P9(x221,x222)+~P9(x223,x222) % 58.55/58.62 [23]~P10(x233,x231)+P10(x231,x232)+~P10(x233,x232) % 58.55/58.62 [24]~P11(x243,x241)+P11(x241,x242)+~P11(x243,x242) % 58.55/58.62 [25]~P12(x253,x251)+P12(x251,x252)+~P12(x253,x252) % 58.55/58.62 [40]~P13(f14(a2,x401),x403)+~P13(f14(f13(f7(a1,a5),a2),x403),x402)+P13(f14(f13(f7(a1,f6(a4,a5)),a2),x401),x402) % 58.55/58.62 [27]~P1(x271,x273)+~P2(x272,x274)+P2(f6(x271,x272),f6(x273,x274)) % 58.55/58.62 [28]~P2(x282,x284)+~P3(x281,x283)+P4(f7(x281,x282),f7(x283,x284)) % 58.55/58.62 [29]~P6(x292,x294)+~P8(x291,x293)+P5(f14(x291,x292),f14(x293,x294)) % 58.55/58.62 [30]~P6(x302,x304)+~P12(x301,x303)+P6(f15(x301,x302),f15(x303,x304)) % 58.55/58.62 [31]~P4(x311,x313)+~P8(x312,x314)+P8(f13(x311,x312),f13(x313,x314)) % 58.55/58.62 [32]~P2(x322,x324)+~P9(x321,x323)+P10(f16(x321,x322),f16(x323,x324)) % 58.55/58.62 [33]~P6(x332,x334)+~P10(x331,x333)+P11(f17(x331,x332),f17(x333,x334)) % 58.55/58.62 [34]~P8(x342,x344)+~P11(x341,x343)+P12(f18(x341,x342),f18(x343,x344)) % 58.55/58.62 [35]~P6(x352,x354)+~P7(x351,x353)+P12(f19(x351,x352),f19(x353,x354)) % 58.55/58.62 [41]~P13(f14(x412,x415),x414)+~P13(f14(f13(f7(a1,x411),x412),x413),x415)+P13(f14(f13(f7(a1,f6(a4,x411)),x412),x413),x414) % 58.55/58.62 [26]~P13(x263,x264)+P13(x261,x262)+~P5(x263,x261)+~P6(x264,x262) % 58.55/58.62 %EqnAxiom % 58.55/58.62 % 58.55/58.62 %------------------------------------------- % 58.55/58.62 cnf(45,plain, % 58.55/58.62 (P13(f14(f13(f7(a1,f6(a9,a11)),x451),x452),x452)), % 58.55/58.62 inference(scs_inference,[],[6,36,19])). % 58.55/58.62 cnf(46,plain, % 58.55/58.62 (~P13(f14(f13(f7(a1,f6(a4,a5)),a2),a3),x461)+~P13(f14(f13(f7(a1,f6(a4,a5)),a2),f15(f19(a12,x461),a3)),a8)), % 58.55/58.62 inference(scs_inference,[],[38,39])). % 58.55/58.62 cnf(54,plain, % 58.55/58.62 (P13(f14(f13(f7(a1,f6(a4,f6(a9,a11))),f13(f7(a1,f6(a9,a11)),x541)),x542),x542)), % 58.55/58.62 inference(scs_inference,[],[6,45,36,41])). % 58.55/58.62 cnf(75,plain, % 58.55/58.62 (~P13(f14(a2,x751),x752)+P13(f14(f13(f7(a1,f6(a4,a5)),a2),f15(f19(a12,x751),x753)),x752)+~P13(f14(f13(f7(a1,f6(a4,a5)),a2),x753),x751)), % 58.55/58.62 inference(scs_inference,[],[42,41])). % 58.55/58.62 cnf(76,plain, % 58.55/58.62 (~P13(f14(a2,x761),a8)+~P13(f14(f13(f7(a1,f6(a4,a5)),a2),a3),x761)), % 58.55/58.62 inference(scs_inference,[],[75,46])). % 58.55/58.62 cnf(187,plain, % 58.55/58.62 ($false), % 58.55/58.62 inference(scs_inference,[],[54,13,45,44,43,41,76]), % 58.55/58.62 ['proof']). % 58.55/58.62 % SZS output end Proof % 58.55/58.62 % Total time :58.000000s %------------------------------------------------------------------------------