%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN627-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 : n018.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 60.17s 60.22s % Output : CNFRefutation 60.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN627-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n018.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sun Jun 23 22:05:24 EDT 2024 % 0.13/0.33 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 60.17/60.20 %------------------------------------------- % 60.17/60.20 % File :CSE---1.7 % 60.17/60.20 % Problem :theBenchmark % 60.17/60.20 % Transform :cnf % 60.17/60.20 % Format :tptp:raw % 60.17/60.20 % Command :java -jar mcs_scs.jar %d %s % 60.17/60.20 % 60.17/60.20 % Result :Theorem 59.570000s % 60.17/60.20 % Output :CNFRefutation 59.570000s % 60.17/60.20 %------------------------------------------- % 60.17/60.21 %-------------------------------------------------------------------------- % 60.17/60.21 % File : SYN627-1 : TPTP v8.2.0. Released v2.5.0. % 60.17/60.21 % Domain : Syntactic % 60.17/60.21 % Problem : Harrison problem 4072 % 60.17/60.21 % Version : Especial. % 60.17/60.21 % English : % 60.17/60.21 % 60.17/60.21 % Refs : [Har01] Email to G. Sutcliffe % 60.17/60.21 % Source : [Har01] % 60.17/60.21 % Names : % 60.17/60.21 % 60.17/60.21 % Status : Unsatisfiable % 60.17/60.21 % Rating : 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v2.5.0 % 60.17/60.21 % Syntax : Number of clauses : 36 ( 10 unt; 1 nHn; 29 RR) % 60.17/60.21 % Number of literals : 88 ( 0 equ; 52 neg) % 60.17/60.21 % Maximal clause size : 7 ( 2 avg) % 60.17/60.21 % Maximal term depth : 4 ( 1 avg) % 60.17/60.21 % Number of predicates : 8 ( 8 usr; 0 prp; 2-5 aty) % 60.17/60.21 % Number of functors : 16 ( 16 usr; 9 con; 0-5 aty) % 60.17/60.21 % Number of variables : 97 ( 5 sgn) % 60.17/60.21 % SPC : CNF_UNS_RFO_NEQ_NHN % 60.17/60.21 % 60.17/60.21 % Comments : % 60.17/60.21 %-------------------------------------------------------------------------- % 60.17/60.21 cnf(p10_1,negated_conjecture, % 60.17/60.21 p10(X0,X0) ). % 60.17/60.21 % 60.17/60.21 cnf(p8_2,negated_conjecture, % 60.17/60.21 p8(X70,X70) ). % 60.17/60.21 % 60.17/60.21 cnf(p6_3,negated_conjecture, % 60.17/60.21 p6(X67,X67) ). % 60.17/60.21 % 60.17/60.21 cnf(p5_4,negated_conjecture, % 60.17/60.21 p5(X64,X64) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_5,negated_conjecture, % 60.17/60.21 p3(X40,X40) ). % 60.17/60.21 % 60.17/60.21 cnf(p2_6,negated_conjecture, % 60.17/60.21 p2(X33,X33) ). % 60.17/60.21 % 60.17/60.21 cnf(p15_7,negated_conjecture, % 60.17/60.21 p15(c18,c19) ). % 60.17/60.21 % 60.17/60.21 cnf(not_p3_8,negated_conjecture, % 60.17/60.21 ~ p3(c23,c24) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_9,negated_conjecture, % 60.17/60.21 p3(c23,f4(f7(c17,c18),c21)) ). % 60.17/60.21 % 60.17/60.21 cnf(p16_10,negated_conjecture, % 60.17/60.21 p16(c17,c20,f9(c19,c18),c21,c22) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_11,negated_conjecture, % 60.17/60.21 ( p3(f14(X55),f14(X56)) % 60.17/60.21 | ~ p6(X55,X56) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p10_12,negated_conjecture, % 60.17/60.21 ( p10(f12(X7),f12(X8)) % 60.17/60.21 | ~ p10(X7,X8) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_13,negated_conjecture, % 60.17/60.21 ( p3(f13(X53),f13(X54)) % 60.17/60.21 | ~ p6(X53,X54) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p10_14,negated_conjecture, % 60.17/60.21 ( p10(X1,X2) % 60.17/60.21 | ~ p10(X0,X1) % 60.17/60.21 | ~ p10(X0,X2) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p8_15,negated_conjecture, % 60.17/60.21 ( p8(X71,X72) % 60.17/60.21 | ~ p8(X70,X71) % 60.17/60.21 | ~ p8(X70,X72) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p6_16,negated_conjecture, % 60.17/60.21 ( p6(X68,X69) % 60.17/60.21 | ~ p6(X67,X68) % 60.17/60.21 | ~ p6(X67,X69) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p5_17,negated_conjecture, % 60.17/60.21 ( p5(X65,X66) % 60.17/60.21 | ~ p5(X64,X65) % 60.17/60.21 | ~ p5(X64,X66) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_18,negated_conjecture, % 60.17/60.21 ( p3(X41,X42) % 60.17/60.21 | ~ p3(X40,X41) % 60.17/60.21 | ~ p3(X40,X42) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p2_19,negated_conjecture, % 60.17/60.21 ( p2(X34,X35) % 60.17/60.21 | ~ p2(X33,X34) % 60.17/60.21 | ~ p2(X33,X35) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_20,negated_conjecture, % 60.17/60.21 ( p3(c24,f4(f7(c17,X32),f14(X32))) % 60.17/60.21 | ~ p15(X32,c19) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_21,negated_conjecture, % 60.17/60.21 ( p3(c23,f4(f7(c17,X31),f13(X31))) % 60.17/60.21 | ~ p15(X31,c19) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p16_22,negated_conjecture, % 60.17/60.21 ( p16(c17,c20,f9(c19,X31),f13(X31),c22) % 60.17/60.21 | ~ p15(X31,c19) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p16_23,negated_conjecture, % 60.17/60.21 ( p16(c17,c20,f9(c19,X32),f14(X32),c25) % 60.17/60.21 | ~ p15(X32,c19) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p15_24,negated_conjecture, % 60.17/60.21 ( p15(X12,X13) % 60.17/60.21 | ~ p6(X14,X12) % 60.17/60.21 | ~ p8(X15,X13) % 60.17/60.21 | ~ p15(X14,X15) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p8_25,negated_conjecture, % 60.17/60.21 ( p8(f9(X73,X74),f9(X75,X76)) % 60.17/60.21 | ~ p6(X74,X76) % 60.17/60.21 | ~ p8(X73,X75) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p2_26,negated_conjecture, % 60.17/60.21 ( p2(f7(X36,X37),f7(X38,X39)) % 60.17/60.21 | ~ p5(X36,X38) % 60.17/60.21 | ~ p6(X37,X39) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_27,negated_conjecture, % 60.17/60.21 ( p3(f4(X57,X58),f4(X59,X60)) % 60.17/60.21 | ~ p2(X57,X59) % 60.17/60.21 | ~ p3(X58,X60) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_28,negated_conjecture, % 60.17/60.21 ( p3(X5,X6) % 60.17/60.21 | ~ p16(c17,c20,X4,X6,X3) % 60.17/60.21 | ~ p16(c17,c20,X4,X5,c22) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p10_29,negated_conjecture, % 60.17/60.21 ( p10(c22,X3) % 60.17/60.21 | ~ p16(c17,c20,X4,X6,X3) % 60.17/60.21 | ~ p16(c17,c20,X4,X5,c22) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p3_30,negated_conjecture, % 60.17/60.21 ( p3(X10,X11) % 60.17/60.21 | ~ p16(c17,c20,X9,X11,c25) % 60.17/60.21 | ~ p16(c17,c20,X9,X10,f12(c22)) ) ). % 60.17/60.21 % 60.17/60.21 cnf(p10_31,negated_conjecture, % 60.17/60.21 ( p10(f12(c22),c25) % 60.17/60.21 | ~ p16(c17,c20,X9,X11,c25) % 60.17/60.21 | ~ p16(c17,c20,X9,X10,f12(c22)) ) ). % 60.17/60.22 % 60.17/60.22 cnf(p6_32,negated_conjecture, % 60.17/60.22 ( p6(X61,X62) % 60.17/60.22 | p3(f4(f7(c17,X61),f4(f7(c17,X62),X63)),f4(f7(c17,X62),f4(f7(c17,X61),X63))) ) ). % 60.17/60.22 % 60.17/60.22 cnf(p3_33,negated_conjecture, % 60.17/60.22 ( p3(X30,f4(f7(c17,X28),f11(X26,X29,X27,X30,X28))) % 60.17/60.22 | ~ p15(X28,X27) % 60.17/60.22 | ~ p16(c17,X26,X27,X30,f12(X29)) ) ). % 60.17/60.22 % 60.17/60.22 cnf(p16_34,negated_conjecture, % 60.17/60.22 ( p16(c17,X26,f9(X27,X28),f11(X26,X29,X27,X30,X28),X29) % 60.17/60.22 | ~ p15(X28,X27) % 60.17/60.22 | ~ p16(c17,X26,X27,X30,f12(X29)) ) ). % 60.17/60.22 % 60.17/60.22 cnf(p16_35,negated_conjecture, % 60.17/60.22 ( p16(X16,X17,X18,X19,X20) % 60.17/60.22 | ~ p8(X24,X18) % 60.17/60.22 | ~ p5(X22,X16) % 60.17/60.22 | ~ p3(X25,X19) % 60.17/60.22 | ~ p3(X23,X17) % 60.17/60.22 | ~ p10(X21,X20) % 60.17/60.22 | ~ p16(X22,X23,X24,X25,X21) ) ). % 60.17/60.22 % 60.17/60.22 cnf(p3_36,negated_conjecture, % 60.17/60.22 ( p3(f11(X43,X44,X45,X46,X47),f11(X48,X49,X50,X51,X52)) % 60.17/60.22 | ~ p6(X47,X52) % 60.17/60.22 | ~ p8(X45,X50) % 60.17/60.22 | ~ p10(X44,X49) % 60.17/60.22 | ~ p3(X43,X48) % 60.17/60.22 | ~ p3(X46,X51) ) ). % 60.17/60.22 % 60.17/60.22 %-------------------------------------------------------------------------- % 60.17/60.22 %------------------------------------------- % 60.17/60.22 % Proof found % 60.17/60.22 % SZS status Theorem for theBenchmark % 60.17/60.22 % SZS output start Proof % 60.17/60.22 %ClaNum:36(EqnAxiom:0) % 60.17/60.22 %VarNum:203(SingletonVarNum:97) % 60.17/60.22 %MaxLitNum:7 % 60.17/60.22 %MaxfuncDepth:3 % 60.17/60.22 %SharedTerms:18 % 60.17/60.22 %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 % 60.17/60.22 %singleGoalClaCount:10 % 60.17/60.22 [1]P1(a1,a3) % 60.17/60.22 [10]~P6(a4,a10) % 60.17/60.22 [9]P8(a2,a6,f16(a3,a1),a5,a7) % 60.17/60.22 [8]P6(a4,f9(f8(a2,a1),a5)) % 60.17/60.22 [2]P2(x21,x21) % 60.17/60.22 [3]P3(x31,x31) % 60.17/60.22 [4]P4(x41,x41) % 60.17/60.22 [5]P5(x51,x51) % 60.17/60.22 [6]P6(x61,x61) % 60.17/60.22 [7]P7(x71,x71) % 60.17/60.22 [27]~P1(x271,a3)+P8(a2,a6,f16(a3,x271),f14(x271),a12) % 60.17/60.22 [28]~P1(x281,a3)+P8(a2,a6,f16(a3,x281),f15(x281),a7) % 60.17/60.22 [24]~P1(x241,a3)+P6(a4,f9(f8(a2,x241),f15(x241))) % 60.17/60.22 [25]~P1(x251,a3)+P6(a10,f9(f8(a2,x251),f14(x251))) % 60.17/60.22 [11]~P2(x111,x112)+P2(f11(x111),f11(x112)) % 60.17/60.22 [12]~P4(x121,x122)+P6(f14(x121),f14(x122)) % 60.17/60.22 [13]~P4(x131,x132)+P6(f15(x131),f15(x132)) % 60.17/60.22 [26]P4(x261,x262)+P6(f9(f8(a2,x261),f9(f8(a2,x262),x263)),f9(f8(a2,x262),f9(f8(a2,x261),x263))) % 60.17/60.22 [14]~P2(x143,x141)+P2(x141,x142)+~P2(x143,x142) % 60.17/60.22 [15]~P3(x153,x151)+P3(x151,x152)+~P3(x153,x152) % 60.17/60.22 [16]~P4(x163,x161)+P4(x161,x162)+~P4(x163,x162) % 60.17/60.22 [17]~P5(x173,x171)+P5(x171,x172)+~P5(x173,x172) % 60.17/60.22 [18]~P6(x183,x181)+P6(x181,x182)+~P6(x183,x182) % 60.17/60.22 [19]~P7(x193,x191)+P7(x191,x192)+~P7(x193,x192) % 60.17/60.22 [32]P6(x321,x322)+~P8(a2,a6,x323,x322,a12)+~P8(a2,a6,x323,x321,f11(a7)) % 60.17/60.22 [33]~P8(a2,a6,x331,x332,a12)+~P8(a2,a6,x331,x333,f11(a7))+P2(f11(a7),a12) % 60.17/60.22 [30]~P8(a2,a6,x302,x303,x301)+P2(a7,x301)+~P8(a2,a6,x302,x304,a7) % 60.17/60.22 [31]P6(x311,x312)+~P8(a2,a6,x313,x312,x314)+~P8(a2,a6,x313,x311,a7) % 60.17/60.22 [21]~P3(x211,x213)+~P4(x212,x214)+P3(f16(x211,x212),f16(x213,x214)) % 60.17/60.22 [22]~P6(x222,x224)+~P7(x221,x223)+P6(f9(x221,x222),f9(x223,x224)) % 60.17/60.22 [23]~P4(x232,x234)+~P5(x231,x233)+P7(f8(x231,x232),f8(x233,x234)) % 60.17/60.22 [35]~P1(x353,x352)+~P8(a2,x351,x352,x355,f11(x354))+P8(a2,x351,f16(x352,x353),f13(x351,x354,x352,x355,x353),x354) % 60.17/60.22 [36]~P1(x362,x365)+~P8(a2,x363,x365,x361,f11(x364))+P6(x361,f9(f8(a2,x362),f13(x363,x364,x365,x361,x362))) % 60.17/60.22 [20]~P1(x204,x203)+P1(x201,x202)+~P3(x203,x202)+~P4(x204,x201) % 60.17/60.22 [34]~P2(x342,x347)+~P3(x343,x348)+~P4(x345,x3410)+~P6(x344,x349)+~P6(x341,x346)+P6(f13(x341,x342,x343,x344,x345),f13(x346,x347,x348,x349,x3410)) % 60.17/60.22 [29]~P8(x298,x299,x297,x2910,x296)+P8(x291,x292,x293,x294,x295)+~P2(x296,x295)+~P3(x297,x293)+~P5(x298,x291)+~P6(x299,x292)+~P6(x2910,x294) % 60.17/60.22 %EqnAxiom % 60.17/60.22 % 60.17/60.22 %------------------------------------------- % 60.17/60.22 cnf(39,plain, % 60.17/60.22 (P6(f9(f8(a2,a1),a5),a4)), % 60.17/60.22 inference(scs_inference,[],[8,6,18])). % 60.17/60.22 cnf(59,plain, % 60.17/60.22 (P2(a7,a12)), % 60.17/60.22 inference(scs_inference,[],[1,9,27,30])). % 60.17/60.22 cnf(60,plain, % 60.17/60.22 (P2(a12,a7)), % 60.17/60.22 inference(scs_inference,[],[59,2,14])). % 60.17/60.22 cnf(65,plain, % 60.17/60.22 (~P6(f15(a1),x651)+P8(a2,a6,f16(a3,a1),x651,a12)), % 60.17/60.22 inference(scs_inference,[],[1,59,3,5,6,28,29])). % 60.17/60.22 cnf(70,plain, % 60.17/60.22 (P8(a2,a6,f16(a3,a1),f15(a1),a12)), % 60.17/60.22 inference(scs_inference,[],[4,65,13])). % 60.17/60.22 cnf(88,plain, % 60.17/60.22 (~P6(f15(a1),x881)+P8(a2,a6,f16(a3,a1),x881,a7)), % 60.17/60.22 inference(scs_inference,[],[5,70,60,3,6,29])). % 60.17/60.22 cnf(93,plain, % 60.17/60.22 (~P6(f15(a1),x931)+P6(x931,f15(a1))), % 60.17/60.22 inference(scs_inference,[],[5,70,60,3,6,29,31])). % 60.17/60.22 cnf(102,plain, % 60.17/60.22 (P8(a2,a6,f16(a3,a1),f15(a1),a7)), % 60.17/60.22 inference(scs_inference,[],[4,88,13])). % 60.17/60.22 cnf(110,plain, % 60.17/60.22 (~P6(a5,x1101)+P6(x1101,a5)), % 60.17/60.22 inference(scs_inference,[],[9,2,3,6,5,29,31])). % 60.17/60.22 cnf(122,plain, % 60.17/60.22 (~P6(x1221,x1222)+P6(x1223,x1222)+~P6(x1221,x1223)), % 60.17/60.22 inference(rename_variables,[],[18])). % 60.17/60.22 cnf(123,plain, % 60.17/60.22 (~P6(f9(f8(a2,a1),a5),a10)), % 60.17/60.22 inference(scs_inference,[],[39,6,10,18,122])). % 60.17/60.22 cnf(341,plain, % 60.17/60.22 (P6(f15(a1),a5)), % 60.17/60.22 inference(scs_inference,[],[9,70,110,31])). % 60.17/60.22 cnf(372,plain, % 60.17/60.22 (P2(f11(a7),f11(a12))), % 60.17/60.22 inference(scs_inference,[],[102,70,11,30])). % 60.17/60.22 cnf(438,plain, % 60.17/60.22 (P2(f11(a12),f11(a7))), % 60.17/60.22 inference(scs_inference,[],[372,2,14])). % 60.17/60.22 cnf(1319,plain, % 60.17/60.22 (P6(f15(a1),f14(a1))), % 60.17/60.22 inference(scs_inference,[],[1,102,27,31])). % 60.17/60.22 cnf(1320,plain, % 60.17/60.22 (~P6(f14(a1),x13201)+P8(a2,a6,f16(a3,a1),x13201,a7)), % 60.17/60.22 inference(scs_inference,[],[1,60,6,3,5,27,29])). % 60.17/60.22 cnf(1321,plain, % 60.17/60.22 (P8(a2,a6,f16(a3,a1),f14(a1),a7)), % 60.17/60.22 inference(scs_inference,[],[4,1320,12])). % 60.17/60.22 cnf(1415,plain, % 60.17/60.22 (P6(f14(a1),a5)), % 60.17/60.22 inference(scs_inference,[],[341,1321,65,31])). % 60.17/60.22 cnf(2297,plain, % 60.17/60.22 (P6(a10,f9(f8(a2,a1),f14(a1)))), % 60.17/60.22 inference(scs_inference,[],[1,1319,438,11,93,24,25])). % 60.17/60.22 cnf(2439,plain, % 60.17/60.22 (P6(f9(x24391,f14(a1)),f9(x24391,a5))), % 60.17/60.22 inference(scs_inference,[],[1415,7,22])). % 60.17/60.22 cnf(2441,plain, % 60.17/60.22 (~P6(f9(f8(a2,a1),f14(a1)),a10)), % 60.17/60.22 inference(scs_inference,[],[123,1415,7,22,18])). % 60.17/60.22 cnf(2448,plain, % 60.17/60.22 ($false), % 60.17/60.22 inference(scs_inference,[],[2439,2441,2297,7,6,22,18]), % 60.17/60.22 ['proof']). % 60.17/60.22 % SZS output end Proof % 60.17/60.22 % Total time :59.570000s %------------------------------------------------------------------------------