%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN622-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 : n032.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:08 EDT 2024 % Result : Unsatisfiable 0.47s 0.57s % Output : CNFRefutation 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : SYN622-1 : TPTP v8.2.0. Released v2.5.0. % 0.02/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Sun Jun 23 18:42:53 EDT 2024 % 0.08/0.28 % CPUTime : % 0.13/0.45 start to proof:theBenchmark % 0.47/0.57 %------------------------------------------- % 0.47/0.57 % File :CSE---1.7 % 0.47/0.57 % Problem :theBenchmark % 0.47/0.57 % Transform :cnf % 0.47/0.57 % Format :tptp:raw % 0.47/0.57 % Command :java -jar mcs_scs.jar %d %s % 0.47/0.57 % 0.47/0.57 % Result :Theorem 0.080000s % 0.47/0.57 % Output :CNFRefutation 0.080000s % 0.47/0.57 %------------------------------------------- % 0.47/0.57 %-------------------------------------------------------------------------- % 0.47/0.57 % File : SYN622-1 : TPTP v8.2.0. Released v2.5.0. % 0.47/0.57 % Domain : Syntactic % 0.47/0.57 % Problem : Harrison problem 4012 % 0.47/0.57 % Version : Especial. % 0.47/0.57 % English : % 0.47/0.57 % 0.47/0.57 % Refs : [Har01] Email to G. Sutcliffe % 0.47/0.57 % Source : [Har01] % 0.47/0.57 % Names : % 0.47/0.57 % 0.47/0.57 % Status : Unsatisfiable % 0.47/0.57 % Rating : 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.12 v5.4.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.14 v4.1.0, 0.00 v2.5.0 % 0.47/0.57 % Syntax : Number of clauses : 34 ( 12 unt; 1 nHn; 26 RR) % 0.47/0.57 % Number of literals : 74 ( 0 equ; 41 neg) % 0.47/0.57 % Maximal clause size : 4 ( 2 avg) % 0.47/0.57 % Maximal term depth : 4 ( 1 avg) % 0.47/0.57 % Number of predicates : 9 ( 9 usr; 0 prp; 1-2 aty) % 0.47/0.57 % Number of functors : 18 ( 18 usr; 6 con; 0-2 aty) % 0.47/0.57 % Number of variables : 72 ( 1 sgn) % 0.47/0.57 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.47/0.57 % 0.47/0.57 % Comments : % 0.47/0.57 %-------------------------------------------------------------------------- % 0.47/0.57 cnf(p11_1,negated_conjecture, % 0.47/0.57 p11(X0,X0) ). % 0.47/0.57 % 0.47/0.57 cnf(p9_2,negated_conjecture, % 0.47/0.57 p9(X60,X60) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_3,negated_conjecture, % 0.47/0.57 p8(X36,X36) ). % 0.47/0.57 % 0.47/0.57 cnf(p3_4,negated_conjecture, % 0.47/0.57 p3(X25,X25) ). % 0.47/0.57 % 0.47/0.57 cnf(p2_5,negated_conjecture, % 0.47/0.57 p2(X9,X9) ). % 0.47/0.57 % 0.47/0.57 cnf(p3_6,negated_conjecture, % 0.47/0.57 p3(f4(c23),c24) ). % 0.47/0.57 % 0.47/0.57 cnf(p19_7,negated_conjecture, % 0.47/0.57 p19(f5(f6(f7(c25))),c24) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_8,negated_conjecture, % 0.47/0.57 p8(f16(X50,f17(X51,X50)),X51) ). % 0.47/0.57 % 0.47/0.57 cnf(p21_9,negated_conjecture, % 0.47/0.57 ( p21(X17) % 0.47/0.57 | ~ p21(X18) % 0.47/0.57 | ~ p11(X18,X17) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p11_10,negated_conjecture, % 0.47/0.57 ( p11(f13(X3),f13(X4)) % 0.47/0.57 | ~ p2(X3,X4) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p9_11,negated_conjecture, % 0.47/0.57 ( p9(f15(X65),f15(X66)) % 0.47/0.57 | ~ p3(X65,X66) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p9_12,negated_conjecture, % 0.47/0.57 ( p9(f10(X63),f10(X64)) % 0.47/0.57 | ~ p8(X63,X64) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_13,negated_conjecture, % 0.47/0.57 ( p8(f14(X44),f14(X45)) % 0.47/0.57 | ~ p9(X44,X45) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p3_14,negated_conjecture, % 0.47/0.57 ( p3(f7(X34),f7(X35)) % 0.47/0.57 | ~ p3(X34,X35) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p3_15,negated_conjecture, % 0.47/0.57 ( p3(f6(X32),f6(X33)) % 0.47/0.57 | ~ p3(X32,X33) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p3_16,negated_conjecture, % 0.47/0.57 ( p3(f5(X30),f5(X31)) % 0.47/0.57 | ~ p3(X30,X31) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p3_17,negated_conjecture, % 0.47/0.57 ( p3(f4(X28),f4(X29)) % 0.47/0.57 | ~ p2(X28,X29) ) ). % 0.47/0.57 % 0.47/0.57 cnf(not_p8_18,negated_conjecture, % 0.47/0.57 ~ p8(f12(f13(c26),c27),f14(f15(f5(c25)))) ). % 0.47/0.57 % 0.47/0.57 cnf(p11_19,negated_conjecture, % 0.47/0.57 ( p11(X1,X2) % 0.47/0.57 | ~ p11(X0,X1) % 0.47/0.57 | ~ p11(X0,X2) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p9_20,negated_conjecture, % 0.47/0.57 ( p9(X61,X62) % 0.47/0.57 | ~ p9(X60,X61) % 0.47/0.57 | ~ p9(X60,X62) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_21,negated_conjecture, % 0.47/0.57 ( p8(X37,X38) % 0.47/0.57 | ~ p8(X36,X37) % 0.47/0.57 | ~ p8(X36,X38) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p3_22,negated_conjecture, % 0.47/0.57 ( p3(X26,X27) % 0.47/0.57 | ~ p3(X25,X26) % 0.47/0.57 | ~ p3(X25,X27) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p2_23,negated_conjecture, % 0.47/0.57 ( p2(X10,X11) % 0.47/0.57 | ~ p2(X9,X10) % 0.47/0.57 | ~ p2(X9,X11) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_24,negated_conjecture, % 0.47/0.57 p8(f12(f13(c23),X43),f12(f13(c26),f16(c27,X43))) ). % 0.47/0.57 % 0.47/0.57 cnf(p20_25,negated_conjecture, % 0.47/0.57 p20(f10(f12(f13(c26),c27)),f10(f12(f13(c26),X16))) ). % 0.47/0.57 % 0.47/0.57 cnf(not_p8_26,negated_conjecture, % 0.47/0.57 ~ p8(f12(f13(c23),f17(c28,c27)),f12(f13(c26),c28)) ). % 0.47/0.57 % 0.47/0.57 cnf(p19_27,negated_conjecture, % 0.47/0.57 ( p19(X5,X6) % 0.47/0.57 | ~ p3(X7,X5) % 0.47/0.57 | ~ p3(X8,X6) % 0.47/0.57 | ~ p19(X7,X8) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p22_28,negated_conjecture, % 0.47/0.57 ( p22(X21,X22) % 0.47/0.57 | ~ p3(X23,X21) % 0.47/0.57 | ~ p3(X24,X22) % 0.47/0.57 | ~ p22(X23,X24) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p20_29,negated_conjecture, % 0.47/0.57 ( p20(X12,X13) % 0.47/0.57 | ~ p9(X14,X12) % 0.47/0.57 | ~ p9(X15,X13) % 0.47/0.57 | ~ p20(X14,X15) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_30,negated_conjecture, % 0.47/0.57 ( p8(f18(X56,X57),f18(X58,X59)) % 0.47/0.57 | ~ p2(X57,X59) % 0.47/0.57 | ~ p3(X56,X58) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_31,negated_conjecture, % 0.47/0.57 ( p8(f12(X39,X40),f12(X41,X42)) % 0.47/0.57 | ~ p11(X39,X41) % 0.47/0.57 | ~ p8(X40,X42) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_32,negated_conjecture, % 0.47/0.57 ( p8(f16(X46,X47),f16(X48,X49)) % 0.47/0.57 | ~ p8(X46,X48) % 0.47/0.57 | ~ p8(X47,X49) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p8_33,negated_conjecture, % 0.47/0.57 ( p8(f17(X52,X53),f17(X54,X55)) % 0.47/0.57 | ~ p8(X52,X54) % 0.47/0.57 | ~ p8(X53,X55) ) ). % 0.47/0.57 % 0.47/0.57 cnf(p21_34,negated_conjecture, % 0.47/0.57 ( p21(f13(X19)) % 0.47/0.57 | p8(f12(f13(X19),f18(X20,X19)),f14(f15(f5(c25)))) % 0.47/0.57 | ~ p22(X20,c24) % 0.47/0.57 | ~ p3(f4(X19),X20) ) ). % 0.47/0.57 % 0.47/0.57 %-------------------------------------------------------------------------- % 0.47/0.57 %------------------------------------------- % 0.47/0.57 % Proof found % 0.47/0.57 % SZS status Theorem for theBenchmark % 0.47/0.57 % SZS output start Proof % 0.47/0.57 %ClaNum:34(EqnAxiom:0) % 0.47/0.58 %VarNum:146(SingletonVarNum:72) % 0.47/0.58 %MaxLitNum:4 % 0.47/0.58 %MaxfuncDepth:3 % 0.47/0.58 %SharedTerms:24 % 0.47/0.58 %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 % 0.47/0.58 %singleGoalClaCount:12 % 0.47/0.58 [6]P4(f2(a1),a3) % 0.47/0.58 [12]~P3(f8(f7(a1),f5(a12,a10)),f8(f7(a9),a12)) % 0.47/0.58 [7]P6(f18(f17(f16(a4))),a3) % 0.47/0.58 [11]~P3(f8(f7(a9),a10),f14(f13(f18(a4)))) % 0.47/0.58 [1]P1(x11,x11) % 0.47/0.58 [2]P2(x21,x21) % 0.47/0.58 [3]P3(x31,x31) % 0.47/0.58 [4]P4(x41,x41) % 0.47/0.58 [5]P5(x51,x51) % 0.47/0.58 [9]P3(f8(f7(a1),x91),f8(f7(a9),f6(a10,x91))) % 0.47/0.58 [10]P7(f11(f8(f7(a9),a10)),f11(f8(f7(a9),x101))) % 0.47/0.58 [8]P3(f6(x81,f5(x82,x81)),x82) % 0.47/0.58 [14]~P5(x141,x142)+P1(f7(x141),f7(x142)) % 0.47/0.58 [15]~P4(x151,x152)+P2(f13(x151),f13(x152)) % 0.47/0.58 [16]~P3(x161,x162)+P2(f11(x161),f11(x162)) % 0.47/0.58 [17]~P2(x171,x172)+P3(f14(x171),f14(x172)) % 0.47/0.58 [18]~P5(x181,x182)+P4(f2(x181),f2(x182)) % 0.47/0.58 [19]~P4(x191,x192)+P4(f16(x191),f16(x192)) % 0.47/0.58 [20]~P4(x201,x202)+P4(f17(x201),f17(x202)) % 0.47/0.58 [21]~P4(x211,x212)+P4(f18(x211),f18(x212)) % 0.47/0.58 [13]~P1(x132,x131)+P8(x131)+~P8(x132) % 0.47/0.58 [22]~P1(x223,x221)+P1(x221,x222)+~P1(x223,x222) % 0.47/0.58 [23]~P2(x233,x231)+P2(x231,x232)+~P2(x233,x232) % 0.47/0.58 [24]~P3(x243,x241)+P3(x241,x242)+~P3(x243,x242) % 0.47/0.58 [25]~P4(x253,x251)+P4(x251,x252)+~P4(x253,x252) % 0.47/0.58 [26]~P5(x263,x261)+P5(x261,x262)+~P5(x263,x262) % 0.47/0.58 [30]~P3(x302,x304)+~P3(x301,x303)+P3(f5(x301,x302),f5(x303,x304)) % 0.47/0.58 [31]~P3(x312,x314)+~P3(x311,x313)+P3(f6(x311,x312),f6(x313,x314)) % 0.47/0.58 [32]~P1(x321,x323)+~P3(x322,x324)+P3(f8(x321,x322),f8(x323,x324)) % 0.47/0.58 [33]~P4(x331,x333)+~P5(x332,x334)+P3(f15(x331,x332),f15(x333,x334)) % 0.47/0.58 [34]~P9(x342,a3)+~P4(f2(x341),x342)+P8(f7(x341))+P3(f8(f7(x341),f15(x342,x341)),f14(f13(f18(a4)))) % 0.47/0.58 [27]~P6(x274,x273)+P6(x271,x272)+~P4(x273,x272)+~P4(x274,x271) % 0.47/0.58 [28]~P7(x284,x283)+P7(x281,x282)+~P2(x283,x282)+~P2(x284,x281) % 0.47/0.58 [29]~P9(x294,x293)+P9(x291,x292)+~P4(x293,x292)+~P4(x294,x291) % 0.47/0.58 %EqnAxiom % 0.47/0.58 % 0.47/0.58 %------------------------------------------- % 0.47/0.58 cnf(43,plain, % 0.47/0.58 (P3(f8(f7(a9),f6(a10,x431)),f8(f7(a1),x431))), % 0.47/0.58 inference(scs_inference,[],[9,3,6,4,25,24])). % 0.47/0.58 cnf(126,plain, % 0.47/0.58 (~P3(f8(f7(a9),a12),f8(f7(a1),f5(a12,a10)))), % 0.47/0.58 inference(scs_inference,[],[12,3,24])). % 0.47/0.58 cnf(138,plain, % 0.47/0.58 ($false), % 0.47/0.58 inference(scs_inference,[],[1,43,126,8,24,32]), % 0.47/0.58 ['proof']). % 0.47/0.58 % SZS output end Proof % 0.47/0.58 % Total time :0.080000s %------------------------------------------------------------------------------