%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN623-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 : n024.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.66s 0.77s % Output : CNFRefutation 0.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN623-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.11/0.33 % Computer : n024.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 19:21:24 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 0.66/0.75 %------------------------------------------- % 0.66/0.75 % File :CSE---1.7 % 0.66/0.75 % Problem :theBenchmark % 0.66/0.76 % Transform :cnf % 0.66/0.76 % Format :tptp:raw % 0.66/0.76 % Command :java -jar mcs_scs.jar %d %s % 0.66/0.76 % 0.66/0.76 % Result :Theorem 0.150000s % 0.66/0.76 % Output :CNFRefutation 0.150000s % 0.66/0.76 %------------------------------------------- % 0.66/0.76 %-------------------------------------------------------------------------- % 0.66/0.76 % File : SYN623-1 : TPTP v8.2.0. Released v2.5.0. % 0.66/0.76 % Domain : Syntactic % 0.66/0.76 % Problem : Harrison problem 4027 % 0.66/0.76 % Version : Especial. % 0.66/0.76 % English : % 0.66/0.76 % 0.66/0.76 % Refs : [Har01] Email to G. Sutcliffe % 0.66/0.76 % Source : [Har01] % 0.66/0.76 % Names : % 0.66/0.76 % 0.66/0.76 % Status : Unsatisfiable % 0.66/0.76 % Rating : 0.00 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v5.2.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.07 v4.1.0, 0.00 v2.5.0 % 0.66/0.76 % Syntax : Number of clauses : 35 ( 15 unt; 1 nHn; 26 RR) % 0.66/0.76 % Number of literals : 80 ( 0 equ; 45 neg) % 0.66/0.76 % Maximal clause size : 5 ( 2 avg) % 0.66/0.76 % Maximal term depth : 4 ( 1 avg) % 0.66/0.76 % Number of predicates : 11 ( 11 usr; 0 prp; 2-2 aty) % 0.66/0.76 % Number of functors : 17 ( 17 usr; 11 con; 0-2 aty) % 0.66/0.76 % Number of variables : 78 ( 0 sgn) % 0.66/0.76 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.66/0.76 % 0.66/0.76 % Comments : % 0.66/0.76 %-------------------------------------------------------------------------- % 0.66/0.76 cnf(p10_1,negated_conjecture, % 0.66/0.76 p10(X0,X0) ). % 0.66/0.76 % 0.66/0.76 cnf(p8_2,negated_conjecture, % 0.66/0.76 p8(X58,X58) ). % 0.66/0.76 % 0.66/0.76 cnf(p7_3,negated_conjecture, % 0.66/0.76 p7(X51,X51) ). % 0.66/0.76 % 0.66/0.76 cnf(p5_4,negated_conjecture, % 0.66/0.76 p5(X48,X48) ). % 0.66/0.76 % 0.66/0.76 cnf(p3_5,negated_conjecture, % 0.66/0.76 p3(X37,X37) ). % 0.66/0.76 % 0.66/0.76 cnf(p2_6,negated_conjecture, % 0.66/0.76 p2(X30,X30) ). % 0.66/0.76 % 0.66/0.76 cnf(p17_7,negated_conjecture, % 0.66/0.76 p17(X23,X23) ). % 0.66/0.76 % 0.66/0.76 cnf(p14_8,negated_conjecture, % 0.66/0.76 p14(X10,X10) ). % 0.66/0.76 % 0.66/0.76 cnf(p12_9,negated_conjecture, % 0.66/0.76 p12(X3,X3) ). % 0.66/0.76 % 0.66/0.76 cnf(p18_10,negated_conjecture, % 0.66/0.76 p18(c26,c25) ). % 0.66/0.76 % 0.66/0.76 cnf(p3_11,negated_conjecture, % 0.66/0.76 p3(c22,c23) ). % 0.66/0.76 % 0.66/0.76 cnf(p2_12,negated_conjecture, % 0.66/0.76 p2(c24,c25) ). % 0.66/0.76 % 0.66/0.76 cnf(not_p16_13,negated_conjecture, % 0.66/0.76 ~ p16(c22,c21) ). % 0.66/0.76 % 0.66/0.76 cnf(p3_14,negated_conjecture, % 0.66/0.76 p3(c23,f4(c24,c20)) ). % 0.66/0.76 % 0.66/0.76 cnf(p16_15,negated_conjecture, % 0.66/0.76 p16(f4(c19,c20),c21) ). % 0.66/0.76 % 0.66/0.76 cnf(p10_16,negated_conjecture, % 0.66/0.76 ( p10(X1,X2) % 0.66/0.76 | ~ p10(X0,X1) % 0.66/0.76 | ~ p10(X0,X2) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p8_17,negated_conjecture, % 0.66/0.76 ( p8(X59,X60) % 0.66/0.76 | ~ p8(X58,X59) % 0.66/0.76 | ~ p8(X58,X60) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p7_18,negated_conjecture, % 0.66/0.76 ( p7(X52,X53) % 0.66/0.76 | ~ p7(X51,X52) % 0.66/0.76 | ~ p7(X51,X53) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p5_19,negated_conjecture, % 0.66/0.76 ( p5(X49,X50) % 0.66/0.76 | ~ p5(X48,X49) % 0.66/0.76 | ~ p5(X48,X50) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p3_20,negated_conjecture, % 0.66/0.76 ( p3(X38,X39) % 0.66/0.76 | ~ p3(X37,X38) % 0.66/0.76 | ~ p3(X37,X39) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p2_21,negated_conjecture, % 0.66/0.76 ( p2(X31,X32) % 0.66/0.76 | ~ p2(X30,X31) % 0.66/0.76 | ~ p2(X30,X32) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p17_22,negated_conjecture, % 0.66/0.76 ( p17(X24,X25) % 0.66/0.76 | ~ p17(X23,X24) % 0.66/0.76 | ~ p17(X23,X25) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p14_23,negated_conjecture, % 0.66/0.76 ( p14(X11,X12) % 0.66/0.76 | ~ p14(X10,X11) % 0.66/0.76 | ~ p14(X10,X12) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p12_24,negated_conjecture, % 0.66/0.76 ( p12(X4,X5) % 0.66/0.76 | ~ p12(X3,X4) % 0.66/0.76 | ~ p12(X3,X5) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p16_25,negated_conjecture, % 0.66/0.76 ( p16(f4(c25,X21),X22) % 0.66/0.76 | ~ p16(f4(f6(c27,c25),X21),X22) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p16_26,negated_conjecture, % 0.66/0.76 ( p16(X13,X14) % 0.66/0.76 | ~ p3(X15,X13) % 0.66/0.76 | ~ p8(X16,X14) % 0.66/0.76 | ~ p16(X15,X16) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p18_27,negated_conjecture, % 0.66/0.76 ( p18(X26,X27) % 0.66/0.76 | ~ p18(X28,X29) % 0.66/0.76 | ~ p2(X29,X27) % 0.66/0.76 | ~ p17(X28,X26) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p8_28,negated_conjecture, % 0.66/0.76 ( p8(f9(X61,X62),f9(X63,X64)) % 0.66/0.76 | ~ p2(X62,X64) % 0.66/0.76 | ~ p7(X61,X63) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p12_29,negated_conjecture, % 0.66/0.76 ( p12(f15(X6,X7),f15(X8,X9)) % 0.66/0.76 | ~ p14(X6,X8) % 0.66/0.76 | ~ p2(X7,X9) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p2_30,negated_conjecture, % 0.66/0.76 ( p2(f6(X33,X34),f6(X35,X36)) % 0.66/0.76 | ~ p2(X34,X36) % 0.66/0.76 | ~ p5(X33,X35) ) ). % 0.66/0.76 % 0.66/0.76 cnf(p3_31,negated_conjecture, % 0.66/0.76 ( p3(f13(X40,X41),f13(X42,X43)) % 0.66/0.76 | ~ p12(X40,X42) % 0.66/0.77 | ~ p2(X41,X43) ) ). % 0.66/0.77 % 0.66/0.77 cnf(p3_32,negated_conjecture, % 0.66/0.77 ( p3(f4(X44,X45),f4(X46,X47)) % 0.66/0.77 | ~ p2(X44,X46) % 0.66/0.77 | ~ p3(X45,X47) ) ). % 0.66/0.77 % 0.66/0.77 cnf(p7_33,negated_conjecture, % 0.66/0.77 ( p7(f11(X54,X55),f11(X56,X57)) % 0.66/0.77 | ~ p10(X54,X56) % 0.66/0.77 | ~ p2(X55,X57) ) ). % 0.66/0.77 % 0.66/0.77 cnf(p16_34,negated_conjecture, % 0.66/0.77 ( p16(f4(X17,X18),X19) % 0.66/0.77 | ~ p2(X17,X20) % 0.66/0.77 | ~ p18(c26,X20) % 0.66/0.77 | ~ p16(f4(c19,X18),X19) % 0.66/0.77 | ~ p16(f4(X20,f13(f15(c28,X17),X20)),f9(f11(c29,X17),X20)) ) ). % 0.66/0.77 % 0.66/0.77 cnf(p16_35,negated_conjecture, % 0.66/0.77 ( p16(f4(X17,X18),X19) % 0.66/0.77 | p16(f4(f6(c27,X20),f13(f15(c28,X17),X20)),f9(f11(c29,X17),X20)) % 0.66/0.77 | ~ p2(X17,X20) % 0.66/0.77 | ~ p18(c26,X20) % 0.66/0.77 | ~ p16(f4(c19,X18),X19) ) ). % 0.66/0.77 % 0.66/0.77 %-------------------------------------------------------------------------- % 0.66/0.77 %------------------------------------------- % 0.66/0.77 % Proof found % 0.66/0.77 % SZS status Theorem for theBenchmark % 0.66/0.77 % SZS output start Proof % 0.66/0.77 %ClaNum:35(EqnAxiom:0) % 0.66/0.77 %VarNum:166(SingletonVarNum:78) % 0.66/0.77 %MaxLitNum:5 % 0.66/0.77 %MaxfuncDepth:3 % 0.66/0.77 %SharedTerms:20 % 0.66/0.77 %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 % 0.66/0.77 %singleGoalClaCount:15 % 0.66/0.77 [1]P1(a1,a5) % 0.66/0.77 [2]P2(a6,a7) % 0.66/0.77 [3]P3(a8,a7) % 0.66/0.77 [15]~P8(a1,a4) % 0.66/0.77 [13]P1(a5,f9(a6,a2)) % 0.66/0.77 [14]P8(f9(a3,a2),a4) % 0.66/0.77 [4]P4(x41,x41) % 0.66/0.77 [5]P9(x51,x51) % 0.66/0.77 [6]P10(x61,x61) % 0.66/0.77 [7]P11(x71,x71) % 0.66/0.77 [8]P1(x81,x81) % 0.66/0.77 [9]P2(x91,x91) % 0.66/0.77 [10]P5(x101,x101) % 0.66/0.77 [11]P6(x111,x111) % 0.66/0.77 [12]P7(x121,x121) % 0.66/0.77 [33]P8(f9(a7,x331),x332)+~P8(f9(f17(a11,a7),x331),x332) % 0.66/0.77 [16]~P4(x163,x161)+P4(x161,x162)+~P4(x163,x162) % 0.66/0.77 [17]~P9(x173,x171)+P9(x171,x172)+~P9(x173,x172) % 0.66/0.77 [18]~P10(x183,x181)+P10(x181,x182)+~P10(x183,x182) % 0.66/0.77 [19]~P11(x193,x191)+P11(x191,x192)+~P11(x193,x192) % 0.66/0.77 [20]~P1(x203,x201)+P1(x201,x202)+~P1(x203,x202) % 0.66/0.77 [21]~P2(x213,x211)+P2(x211,x212)+~P2(x213,x212) % 0.66/0.77 [22]~P5(x223,x221)+P5(x221,x222)+~P5(x223,x222) % 0.66/0.77 [23]~P6(x233,x231)+P6(x231,x232)+~P6(x233,x232) % 0.66/0.77 [24]~P7(x243,x241)+P7(x241,x242)+~P7(x243,x242) % 0.66/0.77 [27]~P10(x271,x273)+~P2(x272,x274)+P9(f16(x271,x272),f16(x273,x274)) % 0.66/0.77 [28]~P4(x281,x283)+~P2(x282,x284)+P10(f10(x281,x282),f10(x283,x284)) % 0.66/0.77 [29]~P1(x292,x294)+~P2(x291,x293)+P1(f9(x291,x292),f9(x293,x294)) % 0.66/0.77 [30]~P2(x302,x304)+~P7(x301,x303)+P1(f14(x301,x302),f14(x303,x304)) % 0.66/0.77 [31]~P11(x311,x313)+~P2(x312,x314)+P2(f17(x311,x312),f17(x313,x314)) % 0.66/0.77 [32]~P2(x322,x324)+~P6(x321,x323)+P7(f15(x321,x322),f15(x323,x324)) % 0.66/0.77 [25]~P3(x254,x253)+P3(x251,x252)+~P2(x253,x252)+~P5(x254,x251) % 0.66/0.77 [26]~P8(x264,x263)+P8(x261,x262)+~P9(x263,x262)+~P1(x264,x261) % 0.66/0.77 [34]~P2(x341,x344)+~P3(a8,x344)+P8(f9(x341,x342),x343)+~P8(f9(a3,x342),x343)+P8(f9(f17(a11,x344),f14(f15(a12,x341),x344)),f16(f10(a13,x341),x344)) % 0.66/0.77 [35]~P2(x351,x354)+~P3(a8,x354)+P8(f9(x351,x352),x353)+~P8(f9(a3,x352),x353)+~P8(f9(x354,f14(f15(a12,x351),x354)),f16(f10(a13,x351),x354)) % 0.66/0.77 %EqnAxiom % 0.66/0.77 % 0.66/0.77 %------------------------------------------- % 0.66/0.77 cnf(36,plain, % 0.66/0.77 (P1(a5,a1)), % 0.66/0.77 inference(scs_inference,[],[1,8,20])). % 0.66/0.77 cnf(39,plain, % 0.66/0.77 (~P3(x391,a6)+P3(x391,a7)), % 0.66/0.77 inference(scs_inference,[],[1,8,10,2,20,25])). % 0.66/0.77 cnf(46,plain, % 0.66/0.77 (P3(a8,a6)), % 0.66/0.77 inference(scs_inference,[],[2,9,3,10,21,25])). % 0.66/0.77 cnf(49,plain, % 0.66/0.77 (P8(f9(a6,a2),a4)+P8(f9(f17(a11,a7),f14(f15(a12,a6),a7)),f16(f10(a13,a6),a7))), % 0.66/0.77 inference(scs_inference,[],[46,14,2,39,34])). % 0.66/0.77 cnf(50,plain, % 0.66/0.77 (P8(f9(a6,a2),a4)+~P8(f9(f17(a11,a7),f14(f15(a12,a6),a7)),f16(f10(a13,a6),a7))), % 0.66/0.77 inference(scs_inference,[],[14,3,2,33,35])). % 0.66/0.77 cnf(51,plain, % 0.66/0.77 (P8(f9(a6,a2),a4)), % 0.66/0.77 inference(scs_inference,[],[49,50])). % 0.66/0.77 cnf(83,plain, % 0.66/0.77 (P1(f9(a6,a2),a5)), % 0.66/0.77 inference(scs_inference,[],[13,8,20])). % 0.66/0.77 cnf(100,plain, % 0.66/0.77 (~P8(a5,a4)), % 0.66/0.77 inference(scs_inference,[],[36,5,15,26])). % 0.66/0.77 cnf(133,plain, % 0.66/0.77 ($false), % 0.66/0.77 inference(scs_inference,[],[83,51,5,100,26]), % 0.66/0.77 ['proof']). % 0.66/0.77 % SZS output end Proof % 0.66/0.77 % Total time :0.150000s %------------------------------------------------------------------------------