%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN638-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 : n023.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:11 EDT 2024 % Result : Unsatisfiable 58.56s 58.61s % Output : CNFRefutation 58.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN638-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.36 % Computer : n023.cluster.edu % 0.12/0.36 % Model : x86_64 x86_64 % 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.36 % Memory : 8042.1875MB % 0.12/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Sun Jun 23 22:10:39 EDT 2024 % 0.12/0.37 % CPUTime : % 0.61/0.65 start to proof:theBenchmark % 58.56/58.59 %------------------------------------------- % 58.56/58.59 % File :CSE---1.7 % 58.56/58.59 % Problem :theBenchmark % 58.56/58.59 % Transform :cnf % 58.56/58.59 % Format :tptp:raw % 58.56/58.59 % Command :java -jar mcs_scs.jar %d %s % 58.56/58.59 % 58.56/58.59 % Result :Theorem 57.900000s % 58.56/58.59 % Output :CNFRefutation 57.900000s % 58.56/58.59 %------------------------------------------- % 58.56/58.60 %-------------------------------------------------------------------------- % 58.56/58.60 % File : SYN638-1 : TPTP v8.2.0. Released v2.5.0. % 58.56/58.60 % Domain : Syntactic % 58.56/58.60 % Problem : Harrison problem 4262 % 58.56/58.60 % Version : Especial. % 58.56/58.60 % English : % 58.56/58.60 % 58.56/58.60 % Refs : [Har01] Email to G. Sutcliffe % 58.56/58.60 % Source : [Har01] % 58.56/58.60 % Names : % 58.56/58.60 % 58.56/58.60 % Status : Unsatisfiable % 58.56/58.60 % Rating : 0.00 v8.1.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.06 v5.3.0, 0.15 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.14 v3.7.0, 0.00 v2.6.0, 0.17 v2.5.0 % 58.56/58.60 % Syntax : Number of clauses : 41 ( 14 unt; 0 nHn; 34 RR) % 58.56/58.60 % Number of literals : 93 ( 0 equ; 55 neg) % 58.56/58.60 % Maximal clause size : 4 ( 2 avg) % 58.56/58.60 % Maximal term depth : 7 ( 2 avg) % 58.56/58.60 % Number of predicates : 11 ( 11 usr; 0 prp; 2-2 aty) % 58.56/58.60 % Number of functors : 18 ( 18 usr; 6 con; 0-3 aty) % 58.56/58.60 % Number of variables : 83 ( 0 sgn) % 58.56/58.60 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.56/58.60 % 58.56/58.60 % Comments : % 58.56/58.60 %-------------------------------------------------------------------------- % 58.56/58.60 cnf(p18_1,negated_conjecture, % 58.56/58.60 p18(X0,X0) ). % 58.56/58.60 % 58.56/58.60 cnf(p7_2,negated_conjecture, % 58.56/58.60 p7(X67,X67) ). % 58.56/58.60 % 58.56/58.60 cnf(p6_3,negated_conjecture, % 58.56/58.60 p6(X52,X52) ). % 58.56/58.60 % 58.56/58.60 cnf(p4_4,negated_conjecture, % 58.56/58.60 p4(X36,X36) ). % 58.56/58.60 % 58.56/58.60 cnf(p3_5,negated_conjecture, % 58.56/58.60 p3(X33,X33) ). % 58.56/58.60 % 58.56/58.60 cnf(p2_6,negated_conjecture, % 58.56/58.60 p2(X5,X5) ). % 58.56/58.60 % 58.56/58.60 cnf(p20_7,negated_conjecture, % 58.56/58.60 p20(f12(c25),c28) ). % 58.56/58.60 % 58.56/58.60 cnf(not_p6_8,negated_conjecture, % 58.56/58.60 ~ p6(f10(c25),f13(c30)) ). % 58.56/58.60 % 58.56/58.60 cnf(p21_9,negated_conjecture, % 58.56/58.60 p21(f13(f14(f15(c30))),f10(c25)) ). % 58.56/58.60 % 58.56/58.60 cnf(p6_10,negated_conjecture, % 58.56/58.61 ( p6(f15(X65),f15(X66)) % 58.56/58.61 | ~ p6(X65,X66) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p18_11,negated_conjecture, % 58.56/58.61 ( p18(f19(X3),f19(X4)) % 58.56/58.61 | ~ p2(X3,X4) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p4_12,negated_conjecture, % 58.56/58.61 ( p4(f16(X39),f16(X40)) % 58.56/58.61 | ~ p4(X39,X40) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p6_13,negated_conjecture, % 58.56/58.61 ( p6(f10(X55),f10(X56)) % 58.56/58.61 | ~ p2(X55,X56) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p6_14,negated_conjecture, % 58.56/58.61 ( p6(f11(X57),f11(X58)) % 58.56/58.61 | ~ p2(X57,X58) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p6_15,negated_conjecture, % 58.56/58.61 ( p6(f12(X59),f12(X60)) % 58.56/58.61 | ~ p2(X59,X60) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p6_16,negated_conjecture, % 58.56/58.61 ( p6(f13(X61),f13(X62)) % 58.56/58.61 | ~ p6(X61,X62) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p6_17,negated_conjecture, % 58.56/58.61 ( p6(f14(X63),f14(X64)) % 58.56/58.61 | ~ p6(X63,X64) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p22_18,negated_conjecture, % 58.56/58.61 p22(f5(c25,c26,c29),f5(c25,c26,c27)) ). % 58.56/58.61 % 58.56/58.61 cnf(p18_19,negated_conjecture, % 58.56/58.61 ( p18(X1,X2) % 58.56/58.61 | ~ p18(X0,X1) % 58.56/58.61 | ~ p18(X0,X2) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p7_20,negated_conjecture, % 58.56/58.61 ( p7(X68,X69) % 58.56/58.61 | ~ p7(X67,X68) % 58.56/58.61 | ~ p7(X67,X69) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p6_21,negated_conjecture, % 58.56/58.61 ( p6(X53,X54) % 58.56/58.61 | ~ p6(X52,X53) % 58.56/58.61 | ~ p6(X52,X54) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p4_22,negated_conjecture, % 58.56/58.61 ( p4(X37,X38) % 58.56/58.61 | ~ p4(X36,X37) % 58.56/58.61 | ~ p4(X36,X38) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p3_23,negated_conjecture, % 58.56/58.61 ( p3(X34,X35) % 58.56/58.61 | ~ p3(X33,X34) % 58.56/58.61 | ~ p3(X33,X35) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p2_24,negated_conjecture, % 58.56/58.61 ( p2(X6,X7) % 58.56/58.61 | ~ p2(X5,X6) % 58.56/58.61 | ~ p2(X5,X7) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p24_25,negated_conjecture, % 58.56/58.61 ( p24(X29,X30) % 58.56/58.61 | ~ p24(X32,X31) % 58.56/58.61 | ~ p4(X32,X29) % 58.56/58.61 | ~ p18(X31,X30) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p20_26,negated_conjecture, % 58.56/58.61 ( p20(X12,X13) % 58.56/58.61 | ~ p6(X14,X12) % 58.56/58.61 | ~ p6(X15,X13) % 58.56/58.61 | ~ p20(X14,X15) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p21_27,negated_conjecture, % 58.56/58.61 ( p21(X16,X17) % 58.56/58.61 | ~ p6(X18,X16) % 58.56/58.61 | ~ p6(X19,X17) % 58.56/58.61 | ~ p21(X18,X19) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p22_28,negated_conjecture, % 58.56/58.61 ( p22(X20,X21) % 58.56/58.61 | ~ p4(X22,X20) % 58.56/58.61 | ~ p4(X23,X21) % 58.56/58.61 | ~ p22(X22,X23) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p23_29,negated_conjecture, % 58.56/58.61 ( p23(X24,X25) % 58.56/58.61 | ~ p4(X26,X24) % 58.56/58.61 | ~ p4(X27,X25) % 58.56/58.61 | ~ p23(X26,X27) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p2_30,negated_conjecture, % 58.56/58.61 ( p2(f8(X8,X9),f8(X10,X11)) % 58.56/58.61 | ~ p6(X8,X10) % 58.56/58.61 | ~ p7(X9,X11) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p7_31,negated_conjecture, % 58.56/58.61 ( p7(f9(X70,X71),f9(X72,X73)) % 58.56/58.61 | ~ p6(X70,X72) % 58.56/58.61 | ~ p6(X71,X73) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p4_32,negated_conjecture, % 58.56/58.61 ( p4(f17(X41,X42),f17(X43,X44)) % 58.56/58.61 | ~ p4(X41,X43) % 58.56/58.61 | ~ p4(X42,X44) ) ). % 58.56/58.61 % 58.56/58.61 cnf(not_p4_33,negated_conjecture, % 58.56/58.61 ~ p4(f5(c25,c26,c27),f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27)) ). % 58.56/58.61 % 58.56/58.61 cnf(p23_34,negated_conjecture, % 58.56/58.61 ( p23(X28,c27) % 58.56/58.61 | ~ p23(X28,c29) % 58.56/58.61 | ~ p24(X28,f19(f8(f11(c25),f9(f10(c25),c28)))) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p23_35,negated_conjecture, % 58.56/58.61 ( p23(X28,c29) % 58.56/58.61 | ~ p23(X28,c27) % 58.56/58.61 | ~ p24(X28,f19(f8(f11(c25),f9(f10(c25),c28)))) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p23_36,negated_conjecture, % 58.56/58.61 ( p23(c27,X28) % 58.56/58.61 | ~ p23(c29,X28) % 58.56/58.61 | ~ p24(X28,f19(f8(f11(c25),f9(f10(c25),c28)))) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p23_37,negated_conjecture, % 58.56/58.61 ( p23(c29,X28) % 58.56/58.61 | ~ p23(c27,X28) % 58.56/58.61 | ~ p24(X28,f19(f8(f11(c25),f9(f10(c25),c28)))) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p4_38,negated_conjecture, % 58.56/58.61 ( p4(f5(X45,X46,X47),f5(X48,X49,X50)) % 58.56/58.61 | ~ p3(X46,X49) % 58.56/58.61 | ~ p4(X47,X50) % 58.56/58.61 | ~ p2(X45,X48) ) ). % 58.56/58.61 % 58.56/58.61 cnf(p4_39,negated_conjecture, % 58.56/58.61 p4(f5(f8(f11(c25),f9(f10(c25),c28)),X51,c27),f5(f8(f11(c25),f9(f10(c25),c28)),X51,c29)) ). % 58.56/58.61 % 58.56/58.61 cnf(p22_40,negated_conjecture, % 58.56/58.61 p22(f16(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27))),f16(f17(c27,f5(c25,c26,c27)))) ). % 58.56/58.61 % 58.56/58.61 cnf(not_p22_41,negated_conjecture, % 58.56/58.61 ~ p22(f16(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29))),f16(f17(c27,f5(c25,c26,c27)))) ). % 58.56/58.61 % 58.56/58.61 %-------------------------------------------------------------------------- % 58.56/58.61 %------------------------------------------- % 58.56/58.61 % Proof found % 58.56/58.61 % SZS status Theorem for theBenchmark % 58.56/58.61 % SZS output start Proof % 58.56/58.61 %ClaNum:41(EqnAxiom:0) % 58.56/58.61 %VarNum:170(SingletonVarNum:83) % 58.56/58.61 %MaxLitNum:4 % 58.56/58.61 %MaxfuncDepth:6 % 58.56/58.61 %SharedTerms:33 % 58.56/58.61 %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 % 58.56/58.61 %singleGoalClaCount:14 % 58.56/58.61 [7]P7(f2(a1),a3) % 58.56/58.61 [9]P9(f13(a1,a4,a7),f13(a1,a4,a5)) % 58.56/58.61 [12]~P3(f8(a1),f12(a6)) % 58.56/58.61 [8]P8(f12(f11(f10(a6))),f8(a1)) % 58.56/58.61 [13]~P4(f13(a1,a4,a5),f13(f18(f9(a1),f17(f8(a1),a3)),a4,a5)) % 58.56/58.61 [11]P9(f15(f14(a5,f13(f18(f9(a1),f17(f8(a1),a3)),a4,a5))),f15(f14(a5,f13(a1,a4,a5)))) % 58.56/58.61 [14]~P9(f15(f14(a5,f13(f18(f9(a1),f17(f8(a1),a3)),a4,a7))),f15(f14(a5,f13(a1,a4,a5)))) % 58.56/58.61 [1]P1(x11,x11) % 58.56/58.61 [2]P2(x21,x21) % 58.56/58.61 [3]P3(x31,x31) % 58.56/58.61 [4]P4(x41,x41) % 58.56/58.61 [5]P5(x51,x51) % 58.56/58.61 [6]P6(x61,x61) % 58.56/58.61 [10]P4(f13(f18(f9(a1),f17(f8(a1),a3)),x101,a5),f13(f18(f9(a1),f17(f8(a1),a3)),x101,a7)) % 58.56/58.61 [15]~P6(x151,x152)+P1(f16(x151),f16(x152)) % 58.56/58.61 [16]~P6(x161,x162)+P3(f2(x161),f2(x162)) % 58.56/58.61 [17]~P6(x171,x172)+P3(f8(x171),f8(x172)) % 58.56/58.61 [18]~P3(x181,x182)+P3(f12(x181),f12(x182)) % 58.56/58.61 [19]~P3(x191,x192)+P3(f10(x191),f10(x192)) % 58.56/58.61 [20]~P3(x201,x202)+P3(f11(x201),f11(x202)) % 58.56/58.61 [21]~P6(x211,x212)+P3(f9(x211),f9(x212)) % 58.56/58.61 [22]~P4(x221,x222)+P4(f15(x221),f15(x222)) % 58.56/58.61 [38]~P11(x381,a5)+P11(x381,a7)+~P10(x381,f16(f18(f9(a1),f17(f8(a1),a3)))) % 58.56/58.61 [39]~P11(x391,a7)+P11(x391,a5)+~P10(x391,f16(f18(f9(a1),f17(f8(a1),a3)))) % 58.56/58.61 [40]~P11(a5,x401)+P11(a7,x401)+~P10(x401,f16(f18(f9(a1),f17(f8(a1),a3)))) % 58.56/58.61 [41]~P11(a7,x411)+P11(a5,x411)+~P10(x411,f16(f18(f9(a1),f17(f8(a1),a3)))) % 58.56/58.61 [23]~P1(x233,x231)+P1(x231,x232)+~P1(x233,x232) % 58.56/58.61 [24]~P2(x243,x241)+P2(x241,x242)+~P2(x243,x242) % 58.56/58.61 [25]~P3(x253,x251)+P3(x251,x252)+~P3(x253,x252) % 58.56/58.61 [26]~P4(x263,x261)+P4(x261,x262)+~P4(x263,x262) % 58.56/58.61 [27]~P5(x273,x271)+P5(x271,x272)+~P5(x273,x272) % 58.56/58.61 [28]~P6(x283,x281)+P6(x281,x282)+~P6(x283,x282) % 58.56/58.61 [34]~P3(x342,x344)+~P3(x341,x343)+P2(f17(x341,x342),f17(x343,x344)) % 58.56/58.61 [35]~P4(x352,x354)+~P4(x351,x353)+P4(f14(x351,x352),f14(x353,x354)) % 58.56/58.61 [36]~P2(x362,x364)+~P3(x361,x363)+P6(f18(x361,x362),f18(x363,x364)) % 58.56/58.61 [29]~P7(x294,x293)+P7(x291,x292)+~P3(x293,x292)+~P3(x294,x291) % 58.56/58.61 [30]~P8(x304,x303)+P8(x301,x302)+~P3(x303,x302)+~P3(x304,x301) % 58.56/58.61 [31]~P9(x314,x313)+P9(x311,x312)+~P4(x313,x312)+~P4(x314,x311) % 58.56/58.61 [32]~P10(x324,x323)+P10(x321,x322)+~P1(x323,x322)+~P4(x324,x321) % 58.56/58.61 [33]~P11(x334,x333)+P11(x331,x332)+~P4(x333,x332)+~P4(x334,x331) % 58.56/58.61 [37]~P4(x373,x376)+~P5(x372,x375)+~P6(x371,x374)+P4(f13(x371,x372,x373),f13(x374,x375,x376)) % 58.56/58.61 %EqnAxiom % 58.56/58.61 % 58.56/58.61 %------------------------------------------- % 58.56/58.62 cnf(253,plain, % 58.56/58.62 (P4(x2531,x2531)), % 58.56/58.62 inference(rename_variables,[],[4])). % 58.56/58.62 cnf(257,plain, % 58.56/58.62 ($false), % 58.56/58.62 inference(scs_inference,[],[10,4,253,11,14,31,22,35]), % 58.56/58.62 ['proof']). % 58.56/58.62 % SZS output end Proof % 58.56/58.62 % Total time :57.900000s %------------------------------------------------------------------------------