%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN626-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 : n019.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 0.60s 0.64s % Output : CNFRefutation 0.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN626-1 : TPTP v8.2.0. Released v2.5.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n019.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 20:12:24 EDT 2024 % 0.13/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 0.60/0.64 %------------------------------------------- % 0.60/0.64 % File :CSE---1.7 % 0.60/0.64 % Problem :theBenchmark % 0.60/0.64 % Transform :cnf % 0.60/0.64 % Format :tptp:raw % 0.60/0.64 % Command :java -jar mcs_scs.jar %d %s % 0.60/0.64 % 0.60/0.64 % Result :Theorem 0.030000s % 0.60/0.64 % Output :CNFRefutation 0.030000s % 0.60/0.64 %------------------------------------------- % 0.60/0.64 %-------------------------------------------------------------------------- % 0.60/0.64 % File : SYN626-1 : TPTP v8.2.0. Released v2.5.0. % 0.60/0.64 % Domain : Syntactic % 0.60/0.64 % Problem : Harrison problem 4045 % 0.60/0.64 % Version : Especial. % 0.60/0.64 % English : % 0.60/0.64 % 0.60/0.64 % Refs : [Har01] Email to G. Sutcliffe % 0.60/0.64 % Source : [Har01] % 0.60/0.64 % Names : % 0.60/0.64 % 0.60/0.64 % Status : Unsatisfiable % 0.60/0.64 % Rating : 0.00 v2.5.0 % 0.60/0.64 % Syntax : Number of clauses : 35 ( 10 unt; 1 nHn; 29 RR) % 0.60/0.64 % Number of literals : 85 ( 0 equ; 49 neg) % 0.60/0.64 % Maximal clause size : 4 ( 2 avg) % 0.60/0.64 % Maximal term depth : 6 ( 1 avg) % 0.60/0.64 % Number of predicates : 11 ( 11 usr; 0 prp; 2-2 aty) % 0.60/0.64 % Number of functors : 12 ( 12 usr; 5 con; 0-2 aty) % 0.60/0.64 % Number of variables : 77 ( 0 sgn) % 0.60/0.64 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.60/0.64 % 0.60/0.64 % Comments : % 0.60/0.64 %-------------------------------------------------------------------------- % 0.60/0.64 cnf(p11_1,negated_conjecture, % 0.60/0.64 p11(X0,X0) ). % 0.60/0.64 % 0.60/0.64 cnf(p7_2,negated_conjecture, % 0.60/0.64 p7(X54,X54) ). % 0.60/0.64 % 0.60/0.64 cnf(p6_3,negated_conjecture, % 0.60/0.64 p6(X47,X47) ). % 0.60/0.64 % 0.60/0.64 cnf(p3_4,negated_conjecture, % 0.60/0.64 p3(X38,X38) ). % 0.60/0.64 % 0.60/0.64 cnf(p2_5,negated_conjecture, % 0.60/0.64 p2(X33,X33) ). % 0.60/0.64 % 0.60/0.64 cnf(p11_6,negated_conjecture, % 0.60/0.64 p11(f13(f12(X5)),X5) ). % 0.60/0.64 % 0.60/0.64 cnf(p14_7,negated_conjecture, % 0.60/0.64 p14(f4(f5(c20)),f4(c21)) ). % 0.60/0.64 % 0.60/0.64 cnf(p16_8,negated_conjecture, % 0.60/0.64 ( p16(X14,X15) % 0.60/0.64 | ~ p15(X14,X15) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p15_9,negated_conjecture, % 0.60/0.64 p15(c22,f8(f5(c20),f9(c23,c24))) ). % 0.60/0.64 % 0.60/0.64 cnf(p16_10,negated_conjecture, % 0.60/0.64 ( p16(c22,X20) % 0.60/0.64 | ~ p7(f12(f13(X20)),X20) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p11_11,negated_conjecture, % 0.60/0.64 ( p11(f13(X3),f13(X4)) % 0.60/0.64 | ~ p7(X3,X4) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p7_12,negated_conjecture, % 0.60/0.64 ( p7(f12(X57),f12(X58)) % 0.60/0.64 | ~ p11(X57,X58) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p3_13,negated_conjecture, % 0.60/0.64 ( p3(f4(X45),f4(X46)) % 0.60/0.64 | ~ p2(X45,X46) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p2_14,negated_conjecture, % 0.60/0.64 ( p2(f5(X36),f5(X37)) % 0.60/0.64 | ~ p2(X36,X37) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p7_15,negated_conjecture, % 0.60/0.64 ( p7(f12(f13(X20)),X20) % 0.60/0.64 | ~ p16(c22,X20) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p11_16,negated_conjecture, % 0.60/0.64 ( p11(X1,X2) % 0.60/0.64 | ~ p11(X0,X1) % 0.60/0.64 | ~ p11(X0,X2) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p7_17,negated_conjecture, % 0.60/0.64 ( p7(X55,X56) % 0.60/0.64 | ~ p7(X54,X55) % 0.60/0.64 | ~ p7(X54,X56) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p6_18,negated_conjecture, % 0.60/0.64 ( p6(X48,X49) % 0.60/0.64 | ~ p6(X47,X48) % 0.60/0.64 | ~ p6(X47,X49) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p3_19,negated_conjecture, % 0.60/0.64 ( p3(X39,X40) % 0.60/0.64 | ~ p3(X38,X39) % 0.60/0.64 | ~ p3(X38,X40) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p2_20,negated_conjecture, % 0.60/0.64 ( p2(X34,X35) % 0.60/0.64 | ~ p2(X33,X34) % 0.60/0.64 | ~ p2(X33,X35) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p15_21,negated_conjecture, % 0.60/0.64 ( p15(X14,X15) % 0.60/0.64 | ~ p16(X14,X15) % 0.60/0.64 | ~ p19(X14,X15) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p15_22,negated_conjecture, % 0.60/0.64 ( p15(X14,X15) % 0.60/0.64 | ~ p16(X14,X15) % 0.60/0.64 | ~ p18(X14,X15) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p15_23,negated_conjecture, % 0.60/0.64 ( p15(X14,X15) % 0.60/0.64 | ~ p16(X14,X15) % 0.60/0.64 | ~ p17(X14,X15) ) ). % 0.60/0.64 % 0.60/0.64 cnf(not_p15_24,negated_conjecture, % 0.60/0.64 ~ p15(c22,f12(f13(f8(f5(c20),f9(c23,c24))))) ). % 0.60/0.64 % 0.60/0.64 cnf(p17_25,negated_conjecture, % 0.60/0.64 ( p17(X14,X15) % 0.60/0.64 | p18(X14,X15) % 0.60/0.64 | p19(X14,X15) % 0.60/0.64 | ~ p15(X14,X15) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p14_26,negated_conjecture, % 0.60/0.64 ( p14(X6,X7) % 0.60/0.64 | ~ p3(X8,X6) % 0.60/0.64 | ~ p3(X9,X7) % 0.60/0.64 | ~ p14(X8,X9) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p19_27,negated_conjecture, % 0.60/0.64 ( p19(X29,X30) % 0.60/0.64 | ~ p6(X31,X29) % 0.60/0.64 | ~ p7(X32,X30) % 0.60/0.64 | ~ p19(X31,X32) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p18_28,negated_conjecture, % 0.60/0.64 ( p18(X25,X26) % 0.60/0.64 | ~ p6(X27,X25) % 0.60/0.64 | ~ p7(X28,X26) % 0.60/0.64 | ~ p18(X27,X28) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p17_29,negated_conjecture, % 0.60/0.64 ( p17(X21,X22) % 0.60/0.64 | ~ p6(X23,X21) % 0.60/0.64 | ~ p7(X24,X22) % 0.60/0.64 | ~ p17(X23,X24) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p16_30,negated_conjecture, % 0.60/0.64 ( p16(X16,X17) % 0.60/0.64 | ~ p6(X18,X16) % 0.60/0.64 | ~ p7(X19,X17) % 0.60/0.64 | ~ p16(X18,X19) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p15_31,negated_conjecture, % 0.60/0.64 ( p15(X10,X11) % 0.60/0.64 | ~ p6(X12,X10) % 0.60/0.64 | ~ p7(X13,X11) % 0.60/0.64 | ~ p15(X12,X13) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p3_32,negated_conjecture, % 0.60/0.64 p3(f10(c22,f12(f13(f8(f5(c20),f9(c23,c24))))),f4(c21)) ). % 0.60/0.64 % 0.60/0.64 cnf(p7_33,negated_conjecture, % 0.60/0.64 ( p7(f8(X59,X60),f8(X61,X62)) % 0.60/0.64 | ~ p2(X59,X61) % 0.60/0.64 | ~ p6(X60,X62) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p3_34,negated_conjecture, % 0.60/0.64 ( p3(f10(X41,X42),f10(X43,X44)) % 0.60/0.64 | ~ p6(X41,X43) % 0.60/0.64 | ~ p7(X42,X44) ) ). % 0.60/0.64 % 0.60/0.64 cnf(p6_35,negated_conjecture, % 0.60/0.64 ( p6(f9(X50,X51),f9(X52,X53)) % 0.60/0.64 | ~ p2(X51,X53) % 0.60/0.64 | ~ p2(X50,X52) ) ). % 0.60/0.64 % 0.60/0.64 %-------------------------------------------------------------------------- % 0.60/0.64 %------------------------------------------- % 0.60/0.64 % Proof found % 0.60/0.64 % SZS status Theorem for theBenchmark % 0.60/0.64 % SZS output start Proof % 0.60/0.64 %ClaNum:35(EqnAxiom:0) % 0.60/0.64 %VarNum:166(SingletonVarNum:77) % 0.60/0.64 %MaxLitNum:4 % 0.60/0.64 %MaxfuncDepth:5 % 0.60/0.64 %SharedTerms:17 % 0.60/0.64 %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 % 0.60/0.64 %singleGoalClaCount:10 % 0.60/0.64 [6]P6(f3(f2(a1)),f3(a4)) % 0.60/0.64 [8]P7(a6,f12(f2(a1),f11(a7,a8))) % 0.60/0.64 [10]~P7(a6,f5(f10(f12(f2(a1),f11(a7,a8))))) % 0.60/0.64 [9]P4(f9(a6,f5(f10(f12(f2(a1),f11(a7,a8))))),f3(a4)) % 0.60/0.64 [1]P1(x11,x11) % 0.60/0.64 [2]P2(x21,x21) % 0.60/0.64 [3]P3(x31,x31) % 0.60/0.64 [4]P4(x41,x41) % 0.60/0.64 [5]P5(x51,x51) % 0.60/0.64 [7]P1(f10(f5(x71)),x71) % 0.60/0.64 [16]~P8(a6,x161)+P2(f5(f10(x161)),x161) % 0.60/0.64 [25]P8(a6,x251)+~P2(f5(f10(x251)),x251) % 0.60/0.64 [11]~P7(x111,x112)+P8(x111,x112) % 0.60/0.64 [12]~P2(x121,x122)+P1(f10(x121),f10(x122)) % 0.60/0.64 [13]~P1(x131,x132)+P2(f5(x131),f5(x132)) % 0.60/0.64 [14]~P5(x141,x142)+P4(f3(x141),f3(x142)) % 0.60/0.64 [15]~P5(x151,x152)+P5(f2(x151),f2(x152)) % 0.60/0.64 [22]~P8(x221,x222)+~P9(x221,x222)+P7(x221,x222) % 0.60/0.64 [23]~P8(x231,x232)+~P10(x231,x232)+P7(x231,x232) % 0.60/0.64 [24]~P8(x241,x242)+~P11(x241,x242)+P7(x241,x242) % 0.60/0.64 [17]~P1(x173,x171)+P1(x171,x172)+~P1(x173,x172) % 0.60/0.64 [18]~P2(x183,x181)+P2(x181,x182)+~P2(x183,x182) % 0.60/0.64 [19]~P3(x193,x191)+P3(x191,x192)+~P3(x193,x192) % 0.60/0.64 [20]~P4(x203,x201)+P4(x201,x202)+~P4(x203,x202) % 0.60/0.64 [21]~P5(x213,x211)+P5(x211,x212)+~P5(x213,x212) % 0.60/0.64 [33]~P3(x332,x334)+~P5(x331,x333)+P2(f12(x331,x332),f12(x333,x334)) % 0.60/0.64 [34]~P5(x342,x344)+~P5(x341,x343)+P3(f11(x341,x342),f11(x343,x344)) % 0.60/0.64 [35]~P2(x352,x354)+~P3(x351,x353)+P4(f9(x351,x352),f9(x353,x354)) % 0.60/0.64 [26]P10(x261,x262)+P11(x261,x262)+~P7(x261,x262)+P9(x261,x262) % 0.60/0.65 [27]~P6(x274,x273)+P6(x271,x272)+~P4(x273,x272)+~P4(x274,x271) % 0.60/0.65 [28]~P8(x284,x283)+P8(x281,x282)+~P2(x283,x282)+~P3(x284,x281) % 0.60/0.65 [29]~P7(x294,x293)+P7(x291,x292)+~P2(x293,x292)+~P3(x294,x291) % 0.60/0.65 [30]~P9(x304,x303)+P9(x301,x302)+~P2(x303,x302)+~P3(x304,x301) % 0.60/0.65 [31]~P10(x314,x313)+P10(x311,x312)+~P2(x313,x312)+~P3(x314,x311) % 0.60/0.65 [32]~P11(x324,x323)+P11(x321,x322)+~P2(x323,x322)+~P3(x324,x321) % 0.60/0.65 %EqnAxiom % 0.60/0.65 % 0.60/0.65 %------------------------------------------- % 0.60/0.65 cnf(63,plain, % 0.60/0.65 (P2(f5(f10(f12(f2(a1),f11(a7,a8)))),f12(f2(a1),f11(a7,a8)))), % 0.60/0.65 inference(scs_inference,[],[8,11,16])). % 0.60/0.65 cnf(76,plain, % 0.60/0.65 (P2(f12(f2(a1),f11(a7,a8)),f5(f10(f12(f2(a1),f11(a7,a8)))))), % 0.60/0.65 inference(scs_inference,[],[63,2,18])). % 0.60/0.65 cnf(79,plain, % 0.60/0.65 ($false), % 0.60/0.65 inference(scs_inference,[],[3,76,10,8,29]), % 0.60/0.65 ['proof']). % 0.60/0.65 % SZS output end Proof % 0.60/0.65 % Total time :0.030000s %------------------------------------------------------------------------------