%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN596-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 : 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:04 EDT 2024 % Result : Unsatisfiable 0.18s 0.58s % Output : CNFRefutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SYN596-1 : TPTP v8.2.0. Released v2.5.0. % 0.10/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n024.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sun Jun 23 19:55:09 EDT 2024 % 0.17/0.32 % CPUTime : % 0.18/0.53 start to proof:theBenchmark % 0.18/0.57 %------------------------------------------- % 0.18/0.57 % File :CSE---1.7 % 0.18/0.57 % Problem :theBenchmark % 0.18/0.57 % Transform :cnf % 0.18/0.57 % Format :tptp:raw % 0.18/0.57 % Command :java -jar mcs_scs.jar %d %s % 0.18/0.57 % 0.18/0.57 % Result :Theorem 0.000000s % 0.18/0.57 % Output :CNFRefutation 0.000000s % 0.18/0.57 %------------------------------------------- % 0.18/0.57 %-------------------------------------------------------------------------- % 0.18/0.57 % File : SYN596-1 : TPTP v8.2.0. Released v2.5.0. % 0.18/0.57 % Domain : Syntactic % 0.18/0.57 % Problem : Harrison problem 3669 % 0.18/0.57 % Version : Especial. % 0.18/0.57 % English : % 0.18/0.57 % 0.18/0.57 % Refs : [Har01] Email to G. Sutcliffe % 0.18/0.57 % Source : [Har01] % 0.18/0.57 % Names : % 0.18/0.57 % 0.18/0.57 % Status : Unsatisfiable % 0.18/0.57 % Rating : 0.00 v5.3.0, 0.05 v5.2.0, 0.00 v2.5.0 % 0.18/0.57 % Syntax : Number of clauses : 28 ( 11 unt; 0 nHn; 23 RR) % 0.18/0.57 % Number of literals : 60 ( 0 equ; 33 neg) % 0.18/0.57 % Maximal clause size : 4 ( 2 avg) % 0.18/0.57 % Maximal term depth : 5 ( 1 avg) % 0.18/0.57 % Number of predicates : 8 ( 8 usr; 0 prp; 2-2 aty) % 0.18/0.57 % Number of functors : 15 ( 15 usr; 6 con; 0-3 aty) % 0.18/0.57 % Number of variables : 58 ( 0 sgn) % 0.18/0.57 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.18/0.57 % 0.18/0.57 % Comments : % 0.18/0.57 %-------------------------------------------------------------------------- % 0.18/0.57 cnf(p10_1,negated_conjecture, % 0.18/0.57 p10(X0,X0) ). % 0.18/0.57 % 0.18/0.57 cnf(p9_2,negated_conjecture, % 0.18/0.57 p9(X50,X50) ). % 0.18/0.57 % 0.18/0.57 cnf(p3_3,negated_conjecture, % 0.18/0.57 p3(X35,X35) ). % 0.18/0.57 % 0.18/0.57 cnf(p2_4,negated_conjecture, % 0.18/0.57 p2(X28,X28) ). % 0.18/0.57 % 0.18/0.57 cnf(p12_5,negated_conjecture, % 0.18/0.57 p12(X9,X9) ). % 0.18/0.57 % 0.18/0.57 cnf(p16_6,negated_conjecture, % 0.18/0.57 p16(c21,c22) ). % 0.18/0.57 % 0.18/0.57 cnf(p17_7,negated_conjecture, % 0.18/0.57 p17(c21,f8(c20)) ). % 0.18/0.57 % 0.18/0.57 cnf(p16_8,negated_conjecture, % 0.18/0.57 p16(f5(f6(f7(c19))),f4(c20)) ). % 0.18/0.57 % 0.18/0.57 cnf(p3_9,negated_conjecture, % 0.18/0.57 ( p3(f8(X48),f8(X49)) % 0.18/0.57 | ~ p2(X48,X49) ) ). % 0.18/0.57 % 0.18/0.57 cnf(p3_10,negated_conjecture, % 0.18/0.57 ( p3(f15(X38),f15(X39)) % 0.18/0.57 | ~ p2(X38,X39) ) ). % 0.18/0.57 % 0.18/0.57 cnf(p3_11,negated_conjecture, % 0.18/0.57 ( p3(f4(X40),f4(X41)) % 0.18/0.57 | ~ p2(X40,X41) ) ). % 0.18/0.57 % 0.18/0.57 cnf(p3_12,negated_conjecture, % 0.18/0.57 ( p3(f5(X42),f5(X43)) % 0.18/0.57 | ~ p3(X42,X43) ) ). % 0.18/0.57 % 0.18/0.57 cnf(p3_13,negated_conjecture, % 0.18/0.57 ( p3(f6(X44),f6(X45)) % 0.18/0.57 | ~ p3(X44,X45) ) ). % 0.18/0.57 % 0.18/0.57 cnf(p3_14,negated_conjecture, % 0.18/0.57 ( p3(f7(X46),f7(X47)) % 0.18/0.57 | ~ p3(X46,X47) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p10_15,negated_conjecture, % 0.18/0.58 ( p10(X1,X2) % 0.18/0.58 | ~ p10(X0,X1) % 0.18/0.58 | ~ p10(X0,X2) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p9_16,negated_conjecture, % 0.18/0.58 ( p9(X51,X52) % 0.18/0.58 | ~ p9(X50,X51) % 0.18/0.58 | ~ p9(X50,X52) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p3_17,negated_conjecture, % 0.18/0.58 ( p3(X36,X37) % 0.18/0.58 | ~ p3(X35,X36) % 0.18/0.58 | ~ p3(X35,X37) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p2_18,negated_conjecture, % 0.18/0.58 ( p2(X29,X30) % 0.18/0.58 | ~ p2(X28,X29) % 0.18/0.58 | ~ p2(X28,X30) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p12_19,negated_conjecture, % 0.18/0.58 ( p12(X10,X11) % 0.18/0.58 | ~ p12(X9,X10) % 0.18/0.58 | ~ p12(X9,X11) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p18_20,negated_conjecture, % 0.18/0.58 p18(c20,f11(f13(f15(c20),f14(f4(c20),c21)),c23,c24)) ). % 0.18/0.58 % 0.18/0.58 cnf(not_p18_21,negated_conjecture, % 0.18/0.58 ~ p18(c20,f11(f13(f15(c20),f14(f4(c20),c22)),c23,c24)) ). % 0.18/0.58 % 0.18/0.58 cnf(p16_22,negated_conjecture, % 0.18/0.58 ( p16(X16,X17) % 0.18/0.58 | ~ p3(X18,X16) % 0.18/0.58 | ~ p3(X19,X17) % 0.18/0.58 | ~ p16(X18,X19) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p18_23,negated_conjecture, % 0.18/0.58 ( p18(X24,X25) % 0.18/0.58 | ~ p18(X27,X26) % 0.18/0.58 | ~ p2(X27,X24) % 0.18/0.58 | ~ p10(X26,X25) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p17_24,negated_conjecture, % 0.18/0.58 ( p17(X20,X21) % 0.18/0.58 | ~ p3(X22,X20) % 0.18/0.58 | ~ p3(X23,X21) % 0.18/0.58 | ~ p17(X22,X23) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p2_25,negated_conjecture, % 0.18/0.58 ( p2(f13(X31,X32),f13(X33,X34)) % 0.18/0.58 | ~ p12(X32,X34) % 0.18/0.58 | ~ p3(X31,X33) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p12_26,negated_conjecture, % 0.18/0.58 ( p12(f14(X12,X13),f14(X14,X15)) % 0.18/0.58 | ~ p3(X12,X14) % 0.18/0.58 | ~ p3(X13,X15) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p10_27,negated_conjecture, % 0.18/0.58 ( p10(f11(X3,X4,X5),f11(X6,X7,X8)) % 0.18/0.58 | ~ p2(X3,X6) % 0.18/0.58 | ~ p9(X4,X7) % 0.18/0.58 | ~ p10(X5,X8) ) ). % 0.18/0.58 % 0.18/0.58 cnf(p10_28,negated_conjecture, % 0.18/0.58 p10(f11(f13(f15(c20),f14(f4(c20),c22)),c23,c24),f11(f13(f15(c20),f14(f4(c20),c21)),c23,c24)) ). % 0.18/0.58 % 0.18/0.58 %-------------------------------------------------------------------------- % 0.18/0.58 %------------------------------------------- % 0.18/0.58 % Proof found % 0.18/0.58 % SZS status Theorem for theBenchmark % 0.18/0.58 % SZS output start Proof % 0.18/0.58 %ClaNum:28(EqnAxiom:0) % 0.18/0.58 %VarNum:116(SingletonVarNum:58) % 0.18/0.58 %MaxLitNum:4 % 0.18/0.58 %MaxfuncDepth:4 % 0.18/0.58 %SharedTerms:24 % 0.18/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 % 0.18/0.58 %singleGoalClaCount:11 % 0.18/0.58 [1]P1(a1,a4) % 0.18/0.58 [7]P7(a1,f5(a2)) % 0.18/0.58 [8]P1(f8(f7(f6(a3))),f9(a2)) % 0.18/0.58 [9]P8(a2,f15(f12(f10(a2),f11(f9(a2),a1)),a13,a14)) % 0.18/0.58 [10]P2(f15(f12(f10(a2),f11(f9(a2),a4)),a13,a14),f15(f12(f10(a2),f11(f9(a2),a1)),a13,a14)) % 0.18/0.58 [11]~P8(a2,f15(f12(f10(a2),f11(f9(a2),a4)),a13,a14)) % 0.18/0.58 [2]P2(x21,x21) % 0.18/0.58 [3]P4(x31,x31) % 0.18/0.58 [4]P5(x41,x41) % 0.18/0.58 [5]P6(x51,x51) % 0.18/0.58 [6]P3(x61,x61) % 0.18/0.58 [12]~P6(x121,x122)+P5(f5(x121),f5(x122)) % 0.18/0.58 [13]~P5(x131,x132)+P5(f6(x131),f6(x132)) % 0.18/0.58 [14]~P5(x141,x142)+P5(f7(x141),f7(x142)) % 0.18/0.58 [15]~P5(x151,x152)+P5(f8(x151),f8(x152)) % 0.18/0.58 [16]~P6(x161,x162)+P5(f9(x161),f9(x162)) % 0.18/0.58 [17]~P6(x171,x172)+P5(f10(x171),f10(x172)) % 0.18/0.58 [18]~P2(x183,x181)+P2(x181,x182)+~P2(x183,x182) % 0.18/0.58 [19]~P4(x193,x191)+P4(x191,x192)+~P4(x193,x192) % 0.18/0.58 [20]~P5(x203,x201)+P5(x201,x202)+~P5(x203,x202) % 0.18/0.58 [21]~P6(x213,x211)+P6(x211,x212)+~P6(x213,x212) % 0.18/0.58 [22]~P3(x223,x221)+P3(x221,x222)+~P3(x223,x222) % 0.18/0.58 [26]~P5(x261,x263)+~P3(x262,x264)+P6(f12(x261,x262),f12(x263,x264)) % 0.18/0.58 [27]~P5(x272,x274)+~P5(x271,x273)+P3(f11(x271,x272),f11(x273,x274)) % 0.18/0.58 [23]~P1(x234,x233)+P1(x231,x232)+~P5(x233,x232)+~P5(x234,x231) % 0.18/0.58 [24]~P7(x244,x243)+P7(x241,x242)+~P5(x243,x242)+~P5(x244,x241) % 0.18/0.58 [25]~P8(x254,x253)+P8(x251,x252)+~P2(x253,x252)+~P6(x254,x251) % 0.18/0.58 [28]~P2(x283,x286)+~P4(x282,x285)+~P6(x281,x284)+P2(f15(x281,x282,x283),f15(x284,x285,x286)) % 0.18/0.58 %EqnAxiom % 0.18/0.58 % 0.18/0.58 %------------------------------------------- % 0.18/0.58 cnf(42,plain, % 0.18/0.58 ($false), % 0.18/0.58 inference(scs_inference,[],[10,2,11,9,5,18,25]), % 0.18/0.58 ['proof']). % 0.18/0.58 % SZS output end Proof % 0.18/0.58 % Total time :0.000000s %------------------------------------------------------------------------------