%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN625-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:08 EDT 2024 % Result : Unsatisfiable 116.25s 117.82s % Output : CNFRefutation 116.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SYN625-1 : TPTP v8.2.0. Released v2.5.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n018.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Sun Jun 23 23:26:24 EDT 2024 % 0.14/0.36 % CPUTime : % 0.58/0.61 start to proof:theBenchmark % 116.25/117.80 %------------------------------------------- % 116.25/117.80 % File :CSE---1.7 % 116.25/117.80 % Problem :theBenchmark % 116.25/117.80 % Transform :cnf % 116.25/117.80 % Format :tptp:raw % 116.25/117.80 % Command :java -jar mcs_scs.jar %d %s % 116.25/117.80 % 116.25/117.80 % Result :Theorem 115.600000s % 116.25/117.80 % Output :CNFRefutation 115.600000s % 116.25/117.80 %------------------------------------------- % 116.25/117.81 %-------------------------------------------------------------------------- % 116.25/117.81 % File : SYN625-1 : TPTP v8.2.0. Released v2.5.0. % 116.25/117.81 % Domain : Syntactic % 116.25/117.81 % Problem : Harrison problem 4030 % 116.25/117.81 % Version : Especial. % 116.25/117.81 % English : % 116.25/117.81 % 116.25/117.81 % Refs : [Har01] Email to G. Sutcliffe % 116.25/117.81 % Source : [Har01] % 116.25/117.81 % Names : % 116.25/117.81 % 116.25/117.81 % Status : Unsatisfiable % 116.25/117.81 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 116.25/117.81 % Syntax : Number of clauses : 35 ( 8 unt; 6 nHn; 27 RR) % 116.25/117.81 % Number of literals : 91 ( 0 equ; 53 neg) % 116.25/117.81 % Maximal clause size : 6 ( 2 avg) % 116.25/117.81 % Maximal term depth : 4 ( 1 avg) % 116.25/117.81 % Number of predicates : 10 ( 10 usr; 0 prp; 1-3 aty) % 116.25/117.81 % Number of functors : 10 ( 10 usr; 3 con; 0-5 aty) % 116.25/117.81 % Number of variables : 104 ( 2 sgn) % 116.25/117.81 % SPC : CNF_UNS_RFO_NEQ_NHN % 116.25/117.81 % 116.25/117.81 % Comments : % 116.25/117.81 %-------------------------------------------------------------------------- % 116.25/117.81 cnf(c21_is_p15_1,negated_conjecture, % 116.25/117.81 p15(c21) ). % 116.25/117.81 % 116.25/117.81 cnf(p10_2,negated_conjecture, % 116.25/117.81 p10(X0,X0) ). % 116.25/117.81 % 116.25/117.81 cnf(p8_3,negated_conjecture, % 116.25/117.81 p8(X71,X71) ). % 116.25/117.81 % 116.25/117.81 cnf(p6_4,negated_conjecture, % 116.25/117.81 p6(X68,X68) ). % 116.25/117.81 % 116.25/117.81 cnf(p5_5,negated_conjecture, % 116.25/117.81 p5(X47,X47) ). % 116.25/117.81 % 116.25/117.81 cnf(p3_6,negated_conjecture, % 116.25/117.81 p3(X40,X40) ). % 116.25/117.81 % 116.25/117.81 cnf(p2_7,negated_conjecture, % 116.25/117.81 p2(X33,X33) ). % 116.25/117.81 % 116.25/117.81 cnf(f4_is_not_p15_8,negated_conjecture, % 116.25/117.81 ~ p15(f4(f7(c19,c20),c21)) ). % 116.25/117.81 % 116.25/117.81 cnf(p16_9,negated_conjecture, % 116.25/117.81 ( p16(X14,X15,X16) % 116.25/117.81 | ~ p5(X15,X16) ) ). % 116.25/117.81 % 116.25/117.81 cnf(not_p15_10,negated_conjecture, % 116.25/117.81 ( ~ p15(X7) % 116.25/117.81 | ~ p18(f9(X7),X76,X76) ) ). % 116.25/117.81 % 116.25/117.81 cnf(p15_11,negated_conjecture, % 116.25/117.81 ( p15(X5) % 116.25/117.81 | ~ p15(X6) % 116.25/117.81 | ~ p3(X6,X5) ) ). % 116.25/117.81 % 116.25/117.81 cnf(p10_12,negated_conjecture, % 116.25/117.81 ( p10(f11(X3),f11(X4)) % 116.25/117.81 | ~ p6(X3,X4) ) ). % 116.25/117.81 % 116.25/117.81 cnf(p8_13,negated_conjecture, % 116.25/117.81 ( p8(f9(X74),f9(X75)) % 116.25/117.81 | ~ p3(X74,X75) ) ). % 116.25/117.81 % 116.25/117.81 cnf(p5_14,negated_conjecture, % 116.25/117.81 ( p5(f14(X66),f14(X67)) % 116.25/117.81 | ~ p3(X66,X67) ) ). % 116.25/117.81 % 116.25/117.81 cnf(p15_15,negated_conjecture, % 116.25/117.81 ( p15(X7) % 116.25/117.81 | p18(f9(X7),f14(X7),f14(X7)) ) ). % 116.25/117.81 % 116.25/117.81 cnf(not_p17_16,negated_conjecture, % 116.25/117.81 ( ~ p17(X77,f11(c20)) % 116.25/117.81 | ~ p16(f9(c21),X77,c19) ) ). % 116.25/117.81 % 116.25/117.81 cnf(p10_17,negated_conjecture, % 116.25/117.81 ( p10(X1,X2) % 116.25/117.81 | ~ p10(X0,X1) % 116.25/117.81 | ~ p10(X0,X2) ) ). % 116.25/117.81 % 116.25/117.82 cnf(p8_18,negated_conjecture, % 116.25/117.82 ( p8(X72,X73) % 116.25/117.82 | ~ p8(X71,X72) % 116.25/117.82 | ~ p8(X71,X73) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p6_19,negated_conjecture, % 116.25/117.82 ( p6(X69,X70) % 116.25/117.82 | ~ p6(X68,X69) % 116.25/117.82 | ~ p6(X68,X70) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p5_20,negated_conjecture, % 116.25/117.82 ( p5(X48,X49) % 116.25/117.82 | ~ p5(X47,X48) % 116.25/117.82 | ~ p5(X47,X49) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p3_21,negated_conjecture, % 116.25/117.82 ( p3(X41,X42) % 116.25/117.82 | ~ p3(X40,X41) % 116.25/117.82 | ~ p3(X40,X42) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p2_22,negated_conjecture, % 116.25/117.82 ( p2(X34,X35) % 116.25/117.82 | ~ p2(X33,X34) % 116.25/117.82 | ~ p2(X33,X35) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p16_23,negated_conjecture, % 116.25/117.82 ( p16(X14,X15,X16) % 116.25/117.82 | ~ p16(X14,X15,X17) % 116.25/117.82 | ~ p16(X14,X17,X16) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p17_24,negated_conjecture, % 116.25/117.82 ( p17(X23,X24) % 116.25/117.82 | ~ p17(X26,X25) % 116.25/117.82 | ~ p5(X26,X23) % 116.25/117.82 | ~ p10(X25,X24) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p3_25,negated_conjecture, % 116.25/117.82 ( p3(f4(X43,X44),f4(X45,X46)) % 116.25/117.82 | ~ p2(X43,X45) % 116.25/117.82 | ~ p3(X44,X46) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p2_26,negated_conjecture, % 116.25/117.82 ( p2(f7(X36,X37),f7(X38,X39)) % 116.25/117.82 | ~ p5(X36,X38) % 116.25/117.82 | ~ p6(X37,X39) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p5_27,negated_conjecture, % 116.25/117.82 ( p5(X15,X16) % 116.25/117.82 | p16(X14,X15,f13(X14,X15,X16)) % 116.25/117.82 | ~ p16(X14,X15,X16) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p5_28,negated_conjecture, % 116.25/117.82 ( p5(X15,X16) % 116.25/117.82 | p16(X14,f13(X14,X15,X16),X16) % 116.25/117.82 | ~ p16(X14,X15,X16) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p16_29,negated_conjecture, % 116.25/117.82 ( p16(X8,X9,X10) % 116.25/117.82 | ~ p8(X11,X8) % 116.25/117.82 | ~ p5(X13,X10) % 116.25/117.82 | ~ p5(X12,X9) % 116.25/117.82 | ~ p16(X11,X12,X13) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p18_30,negated_conjecture, % 116.25/117.82 ( p18(X27,X28,X29) % 116.25/117.82 | ~ p8(X30,X27) % 116.25/117.82 | ~ p5(X32,X29) % 116.25/117.82 | ~ p5(X31,X28) % 116.25/117.82 | ~ p18(X30,X31,X32) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p5_31,negated_conjecture, % 116.25/117.82 ( p5(f13(X60,X61,X62),f13(X63,X64,X65)) % 116.25/117.82 | ~ p5(X62,X65) % 116.25/117.82 | ~ p8(X60,X63) % 116.25/117.82 | ~ p5(X61,X64) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p16_32,negated_conjecture, % 116.25/117.82 ( p16(f9(X18),X19,X20) % 116.25/117.82 | p18(f9(X18),X19,X21) % 116.25/117.82 | ~ p18(f9(f4(f7(X20,X22),X18)),X19,X21) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p18_33,negated_conjecture, % 116.25/117.82 ( p18(f9(X18),X19,X21) % 116.25/117.82 | p17(f12(X18,X20,X22,X19,X21),f11(X22)) % 116.25/117.82 | ~ p18(f9(f4(f7(X20,X22),X18)),X19,X21) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p18_34,negated_conjecture, % 116.25/117.82 ( p18(f9(X18),X19,X21) % 116.25/117.82 | p16(f9(X18),f12(X18,X20,X22,X19,X21),X21) % 116.25/117.82 | ~ p18(f9(f4(f7(X20,X22),X18)),X19,X21) ) ). % 116.25/117.82 % 116.25/117.82 cnf(p5_35,negated_conjecture, % 116.25/117.82 ( p5(f12(X50,X51,X52,X53,X54),f12(X55,X56,X57,X58,X59)) % 116.25/117.82 | ~ p5(X54,X59) % 116.25/117.82 | ~ p6(X52,X57) % 116.25/117.82 | ~ p3(X50,X55) % 116.25/117.82 | ~ p5(X51,X56) % 116.25/117.82 | ~ p5(X53,X58) ) ). % 116.25/117.82 % 116.25/117.82 %-------------------------------------------------------------------------- % 116.25/117.82 %------------------------------------------- % 116.25/117.82 % Proof found % 116.25/117.82 % SZS status Theorem for theBenchmark % 116.25/117.82 % SZS output start Proof % 116.25/117.82 %ClaNum:35(EqnAxiom:0) % 116.25/117.82 %VarNum:228(SingletonVarNum:104) % 116.25/117.82 %MaxLitNum:6 % 116.25/117.82 %MaxfuncDepth:3 % 116.25/117.82 %SharedTerms:9 % 116.25/117.82 %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 % 116.25/117.82 %singleGoalClaCount:8 % 116.25/117.82 [1]P1(a1) % 116.25/117.82 [8]~P1(f5(f4(a2,a3),a1)) % 116.25/117.82 [2]P2(x21,x21) % 116.25/117.82 [3]P3(x31,x31) % 116.25/117.82 [4]P4(x41,x41) % 116.25/117.82 [5]P5(x51,x51) % 116.25/117.82 [6]P6(x61,x61) % 116.25/117.82 [7]P7(x71,x71) % 116.25/117.82 [20]P1(x201)+P9(f10(x201),f7(x201),f7(x201)) % 116.25/117.82 [25]~P10(x251,f6(a3))+~P8(f10(a1),x251,a2) % 116.25/117.82 [10]~P4(x101,x102)+P2(f6(x101),f6(x102)) % 116.25/117.82 [11]~P6(x111,x112)+P3(f10(x111),f10(x112)) % 116.25/117.82 [12]~P6(x121,x122)+P5(f7(x121),f7(x122)) % 116.25/117.82 [22]~P1(x221)+~P9(f10(x221),x222,x222) % 116.25/117.82 [19]~P5(x192,x193)+P8(x191,x192,x193) % 116.25/117.82 [9]~P6(x92,x91)+P1(x91)+~P1(x92) % 116.25/117.82 [13]~P2(x133,x131)+P2(x131,x132)+~P2(x133,x132) % 116.25/117.82 [14]~P3(x143,x141)+P3(x141,x142)+~P3(x143,x142) % 116.25/117.82 [15]~P4(x153,x151)+P4(x151,x152)+~P4(x153,x152) % 116.25/117.82 [16]~P5(x163,x161)+P5(x161,x162)+~P5(x163,x162) % 116.25/117.82 [17]~P6(x173,x171)+P6(x171,x172)+~P6(x173,x172) % 116.25/117.82 [18]~P7(x183,x181)+P7(x181,x182)+~P7(x183,x182) % 116.25/117.82 [29]~P8(x293,x291,x292)+P5(x291,x292)+P8(x293,x291,f8(x293,x291,x292)) % 116.25/117.82 [30]~P8(x303,x301,x302)+P5(x301,x302)+P8(x303,f8(x303,x301,x302),x302) % 116.25/117.82 [28]~P8(x281,x282,x284)+P8(x281,x282,x283)+~P8(x281,x284,x283) % 116.25/117.82 [23]~P6(x232,x234)+~P7(x231,x233)+P6(f5(x231,x232),f5(x233,x234)) % 116.25/117.82 [24]~P4(x242,x244)+~P5(x241,x243)+P7(f4(x241,x242),f4(x243,x244)) % 116.25/117.82 [32]P8(f10(x321),x322,x323)+P9(f10(x321),x322,x324)+~P9(f10(f5(f4(x323,x325),x321)),x322,x324) % 116.25/117.82 [33]P9(f10(x331),x332,x333)+P10(f9(x331,x334,x335,x332,x333),f6(x335))+~P9(f10(f5(f4(x334,x335),x331)),x332,x333) % 116.25/117.82 [34]P8(f10(x341),f9(x341,x344,x345,x342,x343),x343)+P9(f10(x341),x342,x343)+~P9(f10(f5(f4(x344,x345),x341)),x342,x343) % 116.25/117.82 [21]~P10(x214,x213)+P10(x211,x212)+~P2(x213,x212)+~P5(x214,x211) % 116.25/117.82 [31]~P3(x311,x314)+~P5(x313,x316)+~P5(x312,x315)+P5(f8(x311,x312,x313),f8(x314,x315,x316)) % 116.25/117.82 [26]~P8(x264,x265,x266)+P8(x261,x262,x263)+~P3(x264,x261)+~P5(x265,x262)+~P5(x266,x263) % 116.25/117.82 [27]~P9(x274,x275,x276)+P9(x271,x272,x273)+~P3(x274,x271)+~P5(x275,x272)+~P5(x276,x273) % 116.25/117.82 [35]~P4(x353,x358)+~P5(x355,x3510)+~P5(x354,x359)+~P5(x352,x357)+~P6(x351,x356)+P5(f9(x351,x352,x353,x354,x355),f9(x356,x357,x358,x359,x3510)) % 116.25/117.82 %EqnAxiom % 116.25/117.82 % 116.25/117.82 %------------------------------------------- % 116.25/117.83 cnf(54,plain, % 116.25/117.83 (~P9(f10(a1),x541,x541)), % 116.25/117.83 inference(scs_inference,[],[1,6,22,9])). % 116.25/117.83 cnf(63,plain, % 116.25/117.83 (P10(f9(a1,x631,x632,x633,x633),f6(x632))+~P9(f10(f5(f4(x631,x632),a1)),x633,x633)), % 116.25/117.83 inference(scs_inference,[],[1,22,33])). % 116.25/117.83 cnf(67,plain, % 116.25/117.83 (~P9(f10(f5(f4(x671,a3),a1)),x672,x672)+~P8(f10(a1),f9(a1,x671,a3,x672,x672),a2)), % 116.25/117.83 inference(scs_inference,[],[25,63])). % 116.25/117.83 cnf(108,plain, % 116.25/117.83 (P9(f10(f5(f4(a2,a3),a1)),f7(f5(f4(a2,a3),a1)),f7(f5(f4(a2,a3),a1)))), % 116.25/117.83 inference(scs_inference,[],[8,6,9,20])). % 116.25/117.83 cnf(346,plain, % 116.25/117.83 (P8(f10(a1),f7(f5(f4(a2,a3),a1)),a2)), % 116.25/117.83 inference(scs_inference,[],[108,54,32])). % 116.25/117.83 cnf(347,plain, % 116.25/117.83 (~P9(f10(a1),x3471,x3471)), % 116.25/117.83 inference(rename_variables,[],[54])). % 116.25/117.83 cnf(350,plain, % 116.25/117.83 (~P9(f10(a1),x3501,x3501)), % 116.25/117.83 inference(rename_variables,[],[54])). % 116.25/117.83 cnf(352,plain, % 116.25/117.83 (P8(f10(a1),f9(a1,a2,a3,f7(f5(f4(a2,a3),a1)),f7(f5(f4(a2,a3),a1))),f7(f5(f4(a2,a3),a1)))), % 116.25/117.83 inference(scs_inference,[],[108,54,347,350,32,33,34])). % 116.25/117.83 cnf(368,plain, % 116.25/117.83 ($false), % 116.25/117.83 inference(scs_inference,[],[346,352,108,28,67]), % 116.25/117.83 ['proof']). % 116.25/117.83 % SZS output end Proof % 116.25/117.83 % Total time :115.600000s %------------------------------------------------------------------------------