%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN651-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 : n027.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:13 EDT 2024 % Result : Unsatisfiable 1.25s 1.33s % Output : CNFRefutation 1.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYN651-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n027.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sun Jun 23 22:04:09 EDT 2024 % 0.18/0.32 % CPUTime : % 0.50/0.55 start to proof:theBenchmark % 1.25/1.32 %------------------------------------------- % 1.25/1.32 % File :CSE---1.7 % 1.25/1.32 % Problem :theBenchmark % 1.25/1.32 % Transform :cnf % 1.25/1.32 % Format :tptp:raw % 1.25/1.32 % Command :java -jar mcs_scs.jar %d %s % 1.25/1.32 % 1.25/1.32 % Result :Theorem 0.720000s % 1.25/1.32 % Output :CNFRefutation 0.720000s % 1.25/1.32 %------------------------------------------- % 1.25/1.32 %-------------------------------------------------------------------------- % 1.25/1.32 % File : SYN651-1 : TPTP v8.2.0. Released v2.5.0. % 1.25/1.32 % Domain : Syntactic % 1.25/1.32 % Problem : Harrison problem 4423 % 1.25/1.32 % Version : Especial. % 1.25/1.32 % English : % 1.25/1.32 % 1.25/1.32 % Refs : [Har01] Email to G. Sutcliffe % 1.25/1.32 % Source : [Har01] % 1.25/1.32 % Names : % 1.25/1.32 % 1.25/1.32 % Status : Unsatisfiable % 1.25/1.32 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.05 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v2.5.0 % 1.25/1.32 % Syntax : Number of clauses : 45 ( 15 unt; 0 nHn; 32 RR) % 1.25/1.32 % Number of literals : 100 ( 0 equ; 56 neg) % 1.25/1.32 % Maximal clause size : 4 ( 2 avg) % 1.25/1.32 % Maximal term depth : 6 ( 1 avg) % 1.25/1.32 % Number of predicates : 13 ( 13 usr; 0 prp; 2-2 aty) % 1.25/1.32 % Number of functors : 20 ( 20 usr; 11 con; 0-2 aty) % 1.25/1.32 % Number of variables : 114 ( 2 sgn) % 1.25/1.32 % SPC : CNF_UNS_RFO_NEQ_HRN % 1.25/1.32 % 1.25/1.32 % Comments : % 1.25/1.32 %-------------------------------------------------------------------------- % 1.25/1.32 cnf(p11_1,negated_conjecture, % 1.25/1.32 p11(X0,X0) ). % 1.25/1.32 % 1.25/1.32 cnf(p9_2,negated_conjecture, % 1.25/1.32 p9(X80,X80) ). % 1.25/1.32 % 1.25/1.32 cnf(p8_3,negated_conjecture, % 1.25/1.32 p8(X77,X77) ). % 1.25/1.32 % 1.25/1.32 cnf(p6_4,negated_conjecture, % 1.25/1.32 p6(X70,X70) ). % 1.25/1.32 % 1.25/1.32 cnf(p4_5,negated_conjecture, % 1.25/1.32 p4(X63,X63) ). % 1.25/1.32 % 1.25/1.32 cnf(p3_6,negated_conjecture, % 1.25/1.32 p3(X56,X56) ). % 1.25/1.32 % 1.25/1.32 cnf(p21_7,negated_conjecture, % 1.25/1.32 p21(X38,X38) ). % 1.25/1.32 % 1.25/1.32 cnf(p2_8,negated_conjecture, % 1.25/1.32 p2(X31,X31) ). % 1.25/1.32 % 1.25/1.32 cnf(p19_9,negated_conjecture, % 1.25/1.32 p19(X28,X28) ). % 1.25/1.32 % 1.25/1.32 cnf(p17_10,negated_conjecture, % 1.25/1.32 p17(X21,X21) ). % 1.25/1.32 % 1.25/1.32 cnf(p15_11,negated_conjecture, % 1.25/1.32 p15(X14,X14) ). % 1.25/1.32 % 1.25/1.32 cnf(p13_12,negated_conjecture, % 1.25/1.32 p13(X3,X3) ). % 1.25/1.32 % 1.25/1.32 cnf(p23_13,negated_conjecture, % 1.25/1.32 p23(f5(c27,c28),c30) ). % 1.25/1.32 % 1.25/1.32 cnf(p11_14,negated_conjecture, % 1.25/1.32 ( p11(X1,X2) % 1.25/1.32 | ~ p11(X0,X1) % 1.25/1.32 | ~ p11(X0,X2) ) ). % 1.25/1.32 % 1.25/1.32 cnf(p9_15,negated_conjecture, % 1.25/1.32 ( p9(X81,X82) % 1.25/1.32 | ~ p9(X80,X81) % 1.25/1.32 | ~ p9(X80,X82) ) ). % 1.25/1.32 % 1.25/1.32 cnf(p8_16,negated_conjecture, % 1.25/1.32 ( p8(X78,X79) % 1.25/1.32 | ~ p8(X77,X78) % 1.25/1.33 | ~ p8(X77,X79) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p6_17,negated_conjecture, % 1.25/1.33 ( p6(X71,X72) % 1.25/1.33 | ~ p6(X70,X71) % 1.25/1.33 | ~ p6(X70,X72) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p4_18,negated_conjecture, % 1.25/1.33 ( p4(X64,X65) % 1.25/1.33 | ~ p4(X63,X64) % 1.25/1.33 | ~ p4(X63,X65) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p3_19,negated_conjecture, % 1.25/1.33 ( p3(X57,X58) % 1.25/1.33 | ~ p3(X56,X57) % 1.25/1.33 | ~ p3(X56,X58) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p21_20,negated_conjecture, % 1.25/1.33 ( p21(X39,X40) % 1.25/1.33 | ~ p21(X38,X39) % 1.25/1.33 | ~ p21(X38,X40) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p2_21,negated_conjecture, % 1.25/1.33 ( p2(X32,X33) % 1.25/1.33 | ~ p2(X31,X32) % 1.25/1.33 | ~ p2(X31,X33) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p19_22,negated_conjecture, % 1.25/1.33 ( p19(X29,X30) % 1.25/1.33 | ~ p19(X28,X29) % 1.25/1.33 | ~ p19(X28,X30) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p17_23,negated_conjecture, % 1.25/1.33 ( p17(X22,X23) % 1.25/1.33 | ~ p17(X21,X22) % 1.25/1.33 | ~ p17(X21,X23) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p15_24,negated_conjecture, % 1.25/1.33 ( p15(X15,X16) % 1.25/1.33 | ~ p15(X14,X15) % 1.25/1.33 | ~ p15(X14,X16) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p13_25,negated_conjecture, % 1.25/1.33 ( p13(X4,X5) % 1.25/1.33 | ~ p13(X3,X4) % 1.25/1.33 | ~ p13(X3,X5) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_26,negated_conjecture, % 1.25/1.33 p23(f5(f7(f10(c24,f12(c25,c26)),c27),c30),c29) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_27,negated_conjecture, % 1.25/1.33 ( p23(X41,X42) % 1.25/1.33 | ~ p3(X44,X42) % 1.25/1.33 | ~ p4(X43,X41) % 1.25/1.33 | ~ p23(X43,X44) ) ). % 1.25/1.33 % 1.25/1.33 cnf(not_p23_28,negated_conjecture, % 1.25/1.33 ~ p23(f5(f7(f10(c24,f12(c25,f12(c25,c26))),c27),c28),c29) ). % 1.25/1.33 % 1.25/1.33 cnf(p13_29,negated_conjecture, % 1.25/1.33 ( p13(f16(X6,X7),f16(X8,X9)) % 1.25/1.33 | ~ p15(X6,X8) % 1.25/1.33 | ~ p2(X7,X9) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p9_30,negated_conjecture, % 1.25/1.33 ( p9(f12(X83,X84),f12(X85,X86)) % 1.25/1.33 | ~ p11(X83,X85) % 1.25/1.33 | ~ p9(X84,X86) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p6_31,negated_conjecture, % 1.25/1.33 ( p6(f10(X73,X74),f10(X75,X76)) % 1.25/1.33 | ~ p8(X73,X75) % 1.25/1.33 | ~ p9(X74,X76) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p4_32,negated_conjecture, % 1.25/1.33 ( p4(f5(X66,X67),f5(X68,X69)) % 1.25/1.33 | ~ p2(X66,X68) % 1.25/1.33 | ~ p3(X67,X69) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p3_33,negated_conjecture, % 1.25/1.33 ( p3(f14(X59,X60),f14(X61,X62)) % 1.25/1.33 | ~ p13(X59,X61) % 1.25/1.33 | ~ p3(X60,X62) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p2_34,negated_conjecture, % 1.25/1.33 ( p2(f7(X34,X35),f7(X36,X37)) % 1.25/1.33 | ~ p2(X35,X37) % 1.25/1.33 | ~ p6(X34,X36) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p17_35,negated_conjecture, % 1.25/1.33 ( p17(f20(X24,X25),f20(X26,X27)) % 1.25/1.33 | ~ p19(X24,X26) % 1.25/1.33 | ~ p9(X25,X27) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p15_36,negated_conjecture, % 1.25/1.33 ( p15(f18(X17,X18),f18(X19,X20)) % 1.25/1.33 | ~ p17(X17,X19) % 1.25/1.33 | ~ p3(X18,X20) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p13_37,negated_conjecture, % 1.25/1.33 ( p13(f22(X10,X11),f22(X12,X13)) % 1.25/1.33 | ~ p21(X10,X12) % 1.25/1.33 | ~ p3(X11,X13) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p3_38,negated_conjecture, % 1.25/1.33 ( p3(X54,X55) % 1.25/1.33 | ~ p23(f5(f7(f10(c24,f12(c32,c33)),X53),X54),X55) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_39,negated_conjecture, % 1.25/1.33 ( p23(f5(f7(f10(c24,f12(c32,c33)),X53),X54),X55) % 1.25/1.33 | ~ p3(X54,X55) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_40,negated_conjecture, % 1.25/1.33 ( p23(f5(c27,X49),f14(f22(c34,X50),X49)) % 1.25/1.33 | ~ p23(f5(f7(f10(c24,f12(c25,c26)),c27),X49),X50) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_41,negated_conjecture, % 1.25/1.33 ( p23(f5(X45,f14(f16(f18(f20(c31,X46),X47),X45),X48)),X48) % 1.25/1.33 | ~ p23(f5(f7(f10(c24,f12(c25,X46)),X45),X47),X48) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_42,negated_conjecture, % 1.25/1.33 ( p23(f5(f7(f10(c24,c26),c27),f14(f22(c34,X50),X49)),X50) % 1.25/1.33 | ~ p23(f5(f7(f10(c24,f12(c25,c26)),c27),X49),X50) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_43,negated_conjecture, % 1.25/1.33 ( p23(f5(f7(f10(c24,f12(c25,X46)),X45),X47),X48) % 1.25/1.33 | ~ p23(f5(X45,X51),X48) % 1.25/1.33 | ~ p23(f5(f7(f10(c24,X46),X45),X47),X51) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_44,negated_conjecture, % 1.25/1.33 ( p23(f5(f7(f10(c24,f12(c25,c26)),c27),X49),X50) % 1.25/1.33 | ~ p23(f5(c27,X49),X52) % 1.25/1.33 | ~ p23(f5(f7(f10(c24,c26),c27),X52),X50) ) ). % 1.25/1.33 % 1.25/1.33 cnf(p23_45,negated_conjecture, % 1.25/1.33 ( p23(f5(f7(f10(c24,X46),X45),X47),f14(f16(f18(f20(c31,X46),X47),X45),X48)) % 1.25/1.33 | ~ p23(f5(f7(f10(c24,f12(c25,X46)),X45),X47),X48) ) ). % 1.25/1.33 % 1.25/1.33 %-------------------------------------------------------------------------- % 1.25/1.33 %------------------------------------------- % 1.25/1.33 % Proof found % 1.25/1.33 % SZS status Theorem for theBenchmark % 1.25/1.33 % SZS output start Proof % 1.25/1.33 %ClaNum:45(EqnAxiom:0) % 1.25/1.33 %VarNum:234(SingletonVarNum:114) % 1.25/1.33 %MaxLitNum:4 % 1.25/1.33 %MaxfuncDepth:5 % 1.25/1.33 %SharedTerms:27 % 1.25/1.33 %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 45 % 1.25/1.33 %singleGoalClaCount:15 % 1.25/1.33 [13]P13(f6(a1,a5),a7) % 1.25/1.33 [14]P13(f6(f20(f10(a2,f9(a3,a4)),a1),a7),a8) % 1.25/1.33 [15]~P13(f6(f20(f10(a2,f9(a3,f9(a3,a4))),a1),a5),a8) % 1.25/1.33 [1]P1(x11,x11) % 1.25/1.33 [2]P2(x21,x21) % 1.25/1.33 [3]P3(x31,x31) % 1.25/1.33 [4]P4(x41,x41) % 1.25/1.33 [5]P5(x51,x51) % 1.25/1.33 [6]P6(x61,x61) % 1.25/1.33 [7]P7(x71,x71) % 1.25/1.33 [8]P8(x81,x81) % 1.25/1.33 [9]P9(x91,x91) % 1.25/1.33 [10]P10(x101,x101) % 1.25/1.33 [11]P11(x111,x111) % 1.25/1.33 [12]P12(x121,x121) % 1.25/1.33 [40]P13(f6(a1,x401),f15(f19(a14,x402),x401))+~P13(f6(f20(f10(a2,f9(a3,a4)),a1),x401),x402) % 1.25/1.33 [43]P13(f6(f20(f10(a2,a4),a1),f15(f19(a14,x431),x432)),x431)+~P13(f6(f20(f10(a2,f9(a3,a4)),a1),x432),x431) % 1.25/1.33 [38]~P6(x382,x383)+P13(f6(f20(f10(a2,f9(a11,a13)),x381),x382),x383) % 1.25/1.33 [39]P6(x391,x392)+~P13(f6(f20(f10(a2,f9(a11,a13)),x393),x391),x392) % 1.25/1.33 [44]~P13(f6(f20(f10(a2,f9(a3,x441)),x442),x443),x444)+P13(f6(f20(f10(a2,x441),x442),x443),f15(f18(f17(f16(a12,x441),x443),x442),x444)) % 1.25/1.33 [45]~P13(f6(f20(f10(a2,f9(a3,x452)),x451),x453),x454)+P13(f6(x451,f15(f18(f17(f16(a12,x452),x453),x451),x454)),x454) % 1.25/1.33 [16]~P1(x163,x161)+P1(x161,x162)+~P1(x163,x162) % 1.25/1.33 [17]~P2(x173,x171)+P2(x171,x172)+~P2(x173,x172) % 1.25/1.33 [18]~P3(x183,x181)+P3(x181,x182)+~P3(x183,x182) % 1.25/1.33 [19]~P4(x193,x191)+P4(x191,x192)+~P4(x193,x192) % 1.25/1.33 [20]~P5(x203,x201)+P5(x201,x202)+~P5(x203,x202) % 1.25/1.33 [21]~P6(x213,x211)+P6(x211,x212)+~P6(x213,x212) % 1.25/1.33 [22]~P7(x223,x221)+P7(x221,x222)+~P7(x223,x222) % 1.25/1.33 [23]~P8(x233,x231)+P8(x231,x232)+~P8(x233,x232) % 1.25/1.33 [24]~P9(x243,x241)+P9(x241,x242)+~P9(x243,x242) % 1.25/1.33 [25]~P10(x253,x251)+P10(x251,x252)+~P10(x253,x252) % 1.25/1.33 [26]~P11(x263,x261)+P11(x261,x262)+~P11(x263,x262) % 1.25/1.33 [27]~P12(x273,x271)+P12(x271,x272)+~P12(x273,x272) % 1.25/1.33 [41]~P13(f6(a1,x411),x413)+~P13(f6(f20(f10(a2,a4),a1),x413),x412)+P13(f6(f20(f10(a2,f9(a3,a4)),a1),x411),x412) % 1.25/1.33 [29]~P1(x291,x293)+~P2(x292,x294)+P2(f9(x291,x292),f9(x293,x294)) % 1.25/1.33 [30]~P2(x302,x304)+~P3(x301,x303)+P4(f10(x301,x302),f10(x303,x304)) % 1.25/1.33 [31]~P6(x312,x314)+~P8(x311,x313)+P5(f6(x311,x312),f6(x313,x314)) % 1.25/1.33 [32]~P6(x322,x324)+~P12(x321,x323)+P6(f15(x321,x322),f15(x323,x324)) % 1.25/1.33 [33]~P4(x331,x333)+~P8(x332,x334)+P8(f20(x331,x332),f20(x333,x334)) % 1.25/1.33 [34]~P2(x342,x344)+~P9(x341,x343)+P10(f16(x341,x342),f16(x343,x344)) % 1.25/1.33 [35]~P6(x352,x354)+~P10(x351,x353)+P11(f17(x351,x352),f17(x353,x354)) % 1.25/1.33 [36]~P8(x362,x364)+~P11(x361,x363)+P12(f18(x361,x362),f18(x363,x364)) % 1.25/1.33 [37]~P6(x372,x374)+~P7(x371,x373)+P12(f19(x371,x372),f19(x373,x374)) % 1.25/1.33 [42]~P13(f6(x422,x425),x424)+~P13(f6(f20(f10(a2,x421),x422),x423),x425)+P13(f6(f20(f10(a2,f9(a3,x421)),x422),x423),x424) % 1.25/1.33 [28]~P13(x283,x284)+P13(x281,x282)+~P5(x283,x281)+~P6(x284,x282) % 1.25/1.33 %EqnAxiom % 1.25/1.33 % 1.25/1.33 %------------------------------------------- % 1.25/1.33 cnf(46,plain, % 1.25/1.33 (P13(f6(a1,a7),f15(f19(a14,a8),a7))), % 1.25/1.33 inference(scs_inference,[],[14,40])). % 1.25/1.33 cnf(48,plain, % 1.25/1.33 (P13(f6(f20(f10(a2,a4),a1),f15(f19(a14,a8),a7)),a8)), % 1.25/1.33 inference(scs_inference,[],[14,40,43])). % 1.25/1.33 cnf(55,plain, % 1.25/1.33 (P13(f6(a1,f15(f18(f17(f16(a12,a4),a7),a1),a8)),a8)), % 1.25/1.33 inference(scs_inference,[],[48,46,45,41])). % 1.25/1.33 cnf(89,plain, % 1.25/1.33 (P13(f6(f20(f10(a2,a4),a1),a7),f15(f18(f17(f16(a12,a4),a7),a1),a8))), % 1.25/1.33 inference(scs_inference,[],[48,46,44,41])). % 1.25/1.33 cnf(210,plain, % 1.25/1.33 (~P13(f6(a1,f15(f18(f17(f16(a12,a4),a7),a1),a8)),a8)+P13(f6(f20(f10(a2,f9(a3,f9(a3,a4))),a1),a5),a8)), % 1.25/1.33 inference(scs_inference,[],[15,55,89,13,42,41])). % 1.25/1.33 cnf(211,plain, % 1.25/1.33 ($false), % 1.25/1.33 inference(scs_inference,[],[55,15,210]), % 1.25/1.33 ['proof']). % 1.25/1.33 % SZS output end Proof % 1.25/1.33 % Total time :0.720000s %------------------------------------------------------------------------------