%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN613-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:06 EDT 2024 % Result : Unsatisfiable 1.20s 1.32s % Output : CNFRefutation 1.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN613-1 : TPTP v8.2.0. Released v2.5.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 23:28:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.43/0.58 start to proof:theBenchmark % 1.20/1.31 %------------------------------------------- % 1.20/1.31 % File :CSE---1.7 % 1.20/1.31 % Problem :theBenchmark % 1.20/1.31 % Transform :cnf % 1.20/1.31 % Format :tptp:raw % 1.20/1.31 % Command :java -jar mcs_scs.jar %d %s % 1.20/1.31 % 1.20/1.31 % Result :Theorem 0.690000s % 1.20/1.31 % Output :CNFRefutation 0.690000s % 1.20/1.31 %------------------------------------------- % 1.20/1.31 %-------------------------------------------------------------------------- % 1.20/1.31 % File : SYN613-1 : TPTP v8.2.0. Released v2.5.0. % 1.20/1.31 % Domain : Syntactic % 1.20/1.31 % Problem : Harrison problem 3862 % 1.20/1.31 % Version : Especial. % 1.20/1.31 % English : % 1.20/1.31 % 1.20/1.31 % Refs : [Har01] Email to G. Sutcliffe % 1.20/1.31 % Source : [Har01] % 1.20/1.31 % Names : % 1.20/1.31 % 1.20/1.31 % Status : Unsatisfiable % 1.20/1.32 % Rating : 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v2.5.0 % 1.20/1.32 % Syntax : Number of clauses : 31 ( 10 unt; 1 nHn; 25 RR) % 1.20/1.32 % Number of literals : 70 ( 0 equ; 39 neg) % 1.20/1.32 % Maximal clause size : 5 ( 2 avg) % 1.20/1.32 % Maximal term depth : 5 ( 1 avg) % 1.20/1.32 % Number of predicates : 8 ( 8 usr; 0 prp; 2-3 aty) % 1.20/1.32 % Number of functors : 16 ( 16 usr; 7 con; 0-2 aty) % 1.20/1.32 % Number of variables : 62 ( 0 sgn) % 1.20/1.32 % SPC : CNF_UNS_RFO_NEQ_NHN % 1.20/1.32 % 1.20/1.32 % Comments : % 1.20/1.32 %-------------------------------------------------------------------------- % 1.20/1.32 cnf(p11_1,negated_conjecture, % 1.20/1.32 p11(X0,X0) ). % 1.20/1.32 % 1.20/1.32 cnf(p6_2,negated_conjecture, % 1.20/1.32 p6(X48,X48) ). % 1.20/1.32 % 1.20/1.32 cnf(p5_3,negated_conjecture, % 1.20/1.32 p5(X41,X41) ). % 1.20/1.32 % 1.20/1.32 cnf(p3_4,negated_conjecture, % 1.20/1.32 p3(X36,X36) ). % 1.20/1.32 % 1.20/1.32 cnf(p2_5,negated_conjecture, % 1.20/1.32 p2(X29,X29) ). % 1.20/1.32 % 1.20/1.32 cnf(p16_6,negated_conjecture, % 1.20/1.32 p16(X14,X14) ). % 1.20/1.32 % 1.20/1.32 cnf(p11_7,negated_conjecture, % 1.20/1.32 p11(c23,f12(f9(c21))) ). % 1.20/1.32 % 1.20/1.32 cnf(p11_8,negated_conjecture, % 1.20/1.32 p11(c24,f12(f9(c21))) ). % 1.20/1.32 % 1.20/1.32 cnf(p5_9,negated_conjecture, % 1.20/1.32 ( p5(f9(X46),f9(X47)) % 1.20/1.32 | ~ p5(X46,X47) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p11_10,negated_conjecture, % 1.20/1.32 ( p11(f12(X3),f12(X4)) % 1.20/1.32 | ~ p5(X3,X4) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p11_11,negated_conjecture, % 1.20/1.32 ( p11(f13(X5),f13(X6)) % 1.20/1.32 | ~ p11(X5,X6) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p11_12,negated_conjecture, % 1.20/1.32 ( p11(f15(X11),f15(X12)) % 1.20/1.32 | ~ p11(X11,X12) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p3_13,negated_conjecture, % 1.20/1.32 ( p3(f4(X39),f4(X40)) % 1.20/1.32 | ~ p2(X39,X40) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p5_14,negated_conjecture, % 1.20/1.32 ( p5(f10(X44),f10(X45)) % 1.20/1.32 | ~ p2(X44,X45) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p11_15,negated_conjecture, % 1.20/1.32 ( p11(X1,X2) % 1.20/1.32 | ~ p11(X0,X1) % 1.20/1.32 | ~ p11(X0,X2) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p6_16,negated_conjecture, % 1.20/1.32 ( p6(X49,X50) % 1.20/1.32 | ~ p6(X48,X49) % 1.20/1.32 | ~ p6(X48,X50) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p5_17,negated_conjecture, % 1.20/1.32 ( p5(X42,X43) % 1.20/1.32 | ~ p5(X41,X42) % 1.20/1.32 | ~ p5(X41,X43) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p3_18,negated_conjecture, % 1.20/1.32 ( p3(X37,X38) % 1.20/1.32 | ~ p3(X36,X37) % 1.20/1.32 | ~ p3(X36,X38) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p2_19,negated_conjecture, % 1.20/1.32 ( p2(X30,X31) % 1.20/1.32 | ~ p2(X29,X30) % 1.20/1.32 | ~ p2(X29,X31) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p16_20,negated_conjecture, % 1.20/1.32 ( p16(X15,X16) % 1.20/1.32 | ~ p16(X14,X15) % 1.20/1.32 | ~ p16(X14,X16) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p17_21,negated_conjecture, % 1.20/1.32 p17(c19,f4(f7(f10(c20),f8(f9(c21),c22))),c24) ). % 1.20/1.32 % 1.20/1.32 cnf(not_p17_22,negated_conjecture, % 1.20/1.32 ~ p17(c19,f4(f7(f10(c20),f8(f9(c21),c22))),c23) ). % 1.20/1.32 % 1.20/1.32 cnf(p18_23,negated_conjecture, % 1.20/1.32 ( p18(X23,X24) % 1.20/1.32 | ~ p11(X26,X24) % 1.20/1.32 | ~ p18(X25,X26) % 1.20/1.32 | ~ p11(X25,X23) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p11_24,negated_conjecture, % 1.20/1.32 ( p11(f14(X7,X8),f14(X9,X10)) % 1.20/1.32 | ~ p11(X7,X9) % 1.20/1.32 | ~ p11(X8,X10) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p6_25,negated_conjecture, % 1.20/1.32 ( p6(f8(X51,X52),f8(X53,X54)) % 1.20/1.32 | ~ p5(X51,X53) % 1.20/1.32 | ~ p5(X52,X54) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p2_26,negated_conjecture, % 1.20/1.32 ( p2(f7(X32,X33),f7(X34,X35)) % 1.20/1.32 | ~ p5(X32,X34) % 1.20/1.32 | ~ p6(X33,X35) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p18_27,negated_conjecture, % 1.20/1.32 ( p18(f13(f14(X28,c25)),f13(f14(c23,c25))) % 1.20/1.32 | ~ p11(X28,f12(f9(c21))) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p18_28,negated_conjecture, % 1.20/1.32 ( p18(f13(f14(X27,c25)),f13(f14(c24,c25))) % 1.20/1.32 | ~ p11(X27,f12(f9(c21))) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p17_29,negated_conjecture, % 1.20/1.32 ( p17(X17,X18,X19) % 1.20/1.32 | ~ p3(X22,X18) % 1.20/1.32 | ~ p16(X21,X17) % 1.20/1.32 | ~ p11(X20,X19) % 1.20/1.32 | ~ p17(X21,X22,X20) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p17_30,negated_conjecture, % 1.20/1.32 ( p17(c19,f4(c20),c23) % 1.20/1.32 | p11(f15(X13),f12(f9(c21))) % 1.20/1.32 | ~ p11(X13,f12(f9(c21))) % 1.20/1.32 | ~ p17(c19,f4(c20),X13) ) ). % 1.20/1.32 % 1.20/1.32 cnf(p17_31,negated_conjecture, % 1.20/1.32 ( p17(c19,f4(c20),c23) % 1.20/1.32 | ~ p11(X13,f12(f9(c21))) % 1.20/1.32 | ~ p17(c19,f4(c20),X13) % 1.20/1.32 | ~ p18(f13(f14(f15(X13),c25)),f13(f14(X13,c25))) ) ). % 1.20/1.32 % 1.20/1.32 %-------------------------------------------------------------------------- % 1.20/1.32 %------------------------------------------- % 1.20/1.32 % Proof found % 1.20/1.32 % SZS status Theorem for theBenchmark % 1.20/1.32 % SZS output start Proof % 1.20/1.32 %ClaNum:31(EqnAxiom:0) % 1.20/1.32 %VarNum:127(SingletonVarNum:62) % 1.20/1.32 %MaxLitNum:5 % 1.20/1.32 %MaxfuncDepth:4 % 1.20/1.32 %SharedTerms:23 % 1.20/1.32 %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 % 1.20/1.32 %singleGoalClaCount:10 % 1.20/1.32 [7]P1(a1,f7(f6(a2))) % 1.20/1.32 [8]P1(a8,f7(f6(a2))) % 1.20/1.32 [9]P7(a3,f13(f12(f9(a4),f11(f6(a2),a5))),a8) % 1.20/1.32 [10]~P7(a3,f13(f12(f9(a4),f11(f6(a2),a5))),a1) % 1.20/1.32 [1]P1(x11,x11) % 1.20/1.32 [2]P2(x21,x21) % 1.20/1.32 [3]P3(x31,x31) % 1.20/1.32 [4]P4(x41,x41) % 1.20/1.32 [5]P5(x51,x51) % 1.20/1.32 [6]P6(x61,x61) % 1.20/1.32 [27]~P1(x271,f7(f6(a2)))+P8(f14(f16(x271,a10)),f14(f16(a1,a10))) % 1.20/1.32 [28]~P1(x281,f7(f6(a2)))+P8(f14(f16(x281,a10)),f14(f16(a8,a10))) % 1.20/1.32 [11]~P3(x111,x112)+P1(f7(x111),f7(x112)) % 1.20/1.32 [12]~P1(x121,x122)+P1(f14(x121),f14(x122)) % 1.20/1.32 [13]~P1(x131,x132)+P1(f15(x131),f15(x132)) % 1.20/1.32 [14]~P3(x141,x142)+P3(f6(x141),f6(x142)) % 1.20/1.32 [15]~P5(x151,x152)+P3(f9(x151),f9(x152)) % 1.20/1.32 [16]~P5(x161,x162)+P4(f13(x161),f13(x162)) % 1.20/1.32 [17]~P1(x173,x171)+P1(x171,x172)+~P1(x173,x172) % 1.20/1.32 [18]~P2(x183,x181)+P2(x181,x182)+~P2(x183,x182) % 1.20/1.32 [19]~P3(x193,x191)+P3(x191,x192)+~P3(x193,x192) % 1.20/1.32 [20]~P4(x203,x201)+P4(x201,x202)+~P4(x203,x202) % 1.20/1.32 [21]~P5(x213,x211)+P5(x211,x212)+~P5(x213,x212) % 1.20/1.32 [22]~P6(x223,x221)+P6(x221,x222)+~P6(x223,x222) % 1.20/1.32 [24]~P1(x242,x244)+~P1(x241,x243)+P1(f16(x241,x242),f16(x243,x244)) % 1.20/1.32 [25]~P3(x252,x254)+~P3(x251,x253)+P2(f11(x251,x252),f11(x253,x254)) % 1.20/1.32 [26]~P2(x262,x264)+~P3(x261,x263)+P5(f12(x261,x262),f12(x263,x264)) % 1.20/1.32 [30]~P7(a3,f13(a4),x301)+~P1(x301,f7(f6(a2)))+P1(f15(x301),f7(f6(a2)))+P7(a3,f13(a4),a1) % 1.20/1.32 [31]P7(a3,f13(a4),a1)+~P7(a3,f13(a4),x311)+~P1(x311,f7(f6(a2)))+~P8(f14(f16(f15(x311),a10)),f14(f16(x311,a10))) % 1.20/1.32 [23]~P8(x233,x234)+P8(x231,x232)+~P1(x233,x231)+~P1(x234,x232) % 1.20/1.32 [29]~P7(x296,x295,x294)+P7(x291,x292,x293)+~P1(x294,x293)+~P4(x295,x292)+~P6(x296,x291) % 1.20/1.32 %EqnAxiom % 1.20/1.32 % 1.20/1.32 %------------------------------------------- % 1.20/1.32 cnf(32,plain, % 1.20/1.32 (P7(a3,f13(f12(f9(a4),f11(f6(a2),a5))),f7(f6(a2)))), % 1.20/1.32 inference(scs_inference,[],[4,6,8,9,29])). % 1.20/1.32 cnf(1455,plain, % 1.20/1.32 ($false), % 1.20/1.32 inference(scs_inference,[],[7,1,10,32,4,6,17,29]), % 1.20/1.32 ['proof']). % 1.20/1.32 % SZS output end Proof % 1.20/1.32 % Total time :0.690000s %------------------------------------------------------------------------------