%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN618-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 : n017.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:07 EDT 2024 % Result : Unsatisfiable 3.59s 3.66s % Output : CNFRefutation 3.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN618-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.12/0.33 % Computer : n017.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 21:16:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 3.56/3.65 %------------------------------------------- % 3.56/3.65 % File :CSE---1.7 % 3.56/3.65 % Problem :theBenchmark % 3.56/3.65 % Transform :cnf % 3.56/3.65 % Format :tptp:raw % 3.56/3.65 % Command :java -jar mcs_scs.jar %d %s % 3.56/3.65 % 3.56/3.65 % Result :Theorem 3.060000s % 3.56/3.65 % Output :CNFRefutation 3.060000s % 3.56/3.65 %------------------------------------------- % 3.59/3.66 %-------------------------------------------------------------------------- % 3.59/3.66 % File : SYN618-1 : TPTP v8.2.0. Released v2.5.0. % 3.59/3.66 % Domain : Syntactic % 3.59/3.66 % Problem : Harrison problem 3944 % 3.59/3.66 % Version : Especial. % 3.59/3.66 % English : % 3.59/3.66 % 3.59/3.66 % Refs : [Har01] Email to G. Sutcliffe % 3.59/3.66 % Source : [Har01] % 3.59/3.66 % Names : % 3.59/3.66 % 3.59/3.66 % Status : Unsatisfiable % 3.59/3.66 % Rating : 0.00 v5.3.0, 0.05 v5.2.0, 0.00 v2.5.0 % 3.59/3.66 % Syntax : Number of clauses : 33 ( 16 unt; 0 nHn; 28 RR) % 3.59/3.66 % Number of literals : 72 ( 0 equ; 40 neg) % 3.59/3.66 % Maximal clause size : 5 ( 2 avg) % 3.59/3.66 % Maximal term depth : 3 ( 1 avg) % 3.59/3.66 % Number of predicates : 10 ( 10 usr; 0 prp; 1-3 aty) % 3.59/3.66 % Number of functors : 13 ( 13 usr; 9 con; 0-2 aty) % 3.59/3.66 % Number of variables : 53 ( 0 sgn) % 3.59/3.66 % SPC : CNF_UNS_RFO_NEQ_HRN % 3.59/3.66 % 3.59/3.66 % Comments : % 3.59/3.66 %-------------------------------------------------------------------------- % 3.59/3.66 cnf(c16_is_p9_1,negated_conjecture, % 3.59/3.66 p9(c16) ). % 3.59/3.66 % 3.59/3.66 cnf(p10_2,negated_conjecture, % 3.59/3.66 p10(X0,X0) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_3,negated_conjecture, % 3.59/3.66 p5(X34,X34) ). % 3.59/3.66 % 3.59/3.66 cnf(p4_4,negated_conjecture, % 3.59/3.66 p4(X29,X29) ). % 3.59/3.66 % 3.59/3.66 cnf(p2_5,negated_conjecture, % 3.59/3.66 p2(X24,X24) ). % 3.59/3.66 % 3.59/3.66 cnf(p14_6,negated_conjecture, % 3.59/3.66 p14(X17,X17) ). % 3.59/3.66 % 3.59/3.66 cnf(p12_7,negated_conjecture, % 3.59/3.66 p12(c19,c20) ). % 3.59/3.66 % 3.59/3.66 cnf(p13_8,negated_conjecture, % 3.59/3.66 p13(c23,c21) ). % 3.59/3.66 % 3.59/3.66 cnf(p13_9,negated_conjecture, % 3.59/3.66 p13(c19,c23) ). % 3.59/3.66 % 3.59/3.66 cnf(p13_10,negated_conjecture, % 3.59/3.66 p13(c19,c21) ). % 3.59/3.66 % 3.59/3.66 cnf(p12_11,negated_conjecture, % 3.59/3.66 p12(c20,c21) ). % 3.59/3.66 % 3.59/3.66 cnf(p2_12,negated_conjecture, % 3.59/3.66 p2(c17,f3(c16)) ). % 3.59/3.66 % 3.59/3.66 cnf(p11_13,negated_conjecture, % 3.59/3.66 p11(c16,c17,c18) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_14,negated_conjecture, % 3.59/3.66 p5(f8(c16,c20),f6(f7(c22))) ). % 3.59/3.66 % 3.59/3.66 cnf(p9_15,negated_conjecture, % 3.59/3.66 ( p9(X44) % 3.59/3.66 | ~ p9(X45) % 3.59/3.66 | ~ p2(X45,X44) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_16,negated_conjecture, % 3.59/3.66 p5(f8(f3(c16),c23),f6(f7(c22))) ). % 3.59/3.66 % 3.59/3.66 cnf(not_p5_17,negated_conjecture, % 3.59/3.66 ~ p5(f8(f3(c16),c20),f6(f7(c22))) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_18,negated_conjecture, % 3.59/3.66 ( p5(f6(X38),f6(X39)) % 3.59/3.66 | ~ p4(X38,X39) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p2_19,negated_conjecture, % 3.59/3.66 ( p2(f3(X27),f3(X28)) % 3.59/3.66 | ~ p2(X27,X28) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p4_20,negated_conjecture, % 3.59/3.66 ( p4(f7(X32),f7(X33)) % 3.59/3.66 | ~ p4(X32,X33) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p10_21,negated_conjecture, % 3.59/3.66 ( p10(X1,X2) % 3.59/3.66 | ~ p10(X0,X1) % 3.59/3.66 | ~ p10(X0,X2) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_22,negated_conjecture, % 3.59/3.66 ( p5(X35,X36) % 3.59/3.66 | ~ p5(X34,X35) % 3.59/3.66 | ~ p5(X34,X36) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p4_23,negated_conjecture, % 3.59/3.66 ( p4(X30,X31) % 3.59/3.66 | ~ p4(X29,X30) % 3.59/3.66 | ~ p4(X29,X31) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p2_24,negated_conjecture, % 3.59/3.66 ( p2(X25,X26) % 3.59/3.66 | ~ p2(X24,X25) % 3.59/3.66 | ~ p2(X24,X26) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p14_25,negated_conjecture, % 3.59/3.66 ( p14(X18,X19) % 3.59/3.66 | ~ p14(X17,X18) % 3.59/3.66 | ~ p14(X17,X19) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p12_26,negated_conjecture, % 3.59/3.66 ( p12(X9,X10) % 3.59/3.66 | ~ p5(X11,X9) % 3.59/3.66 | ~ p5(X12,X10) % 3.59/3.66 | ~ p12(X11,X12) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p15_27,negated_conjecture, % 3.59/3.66 ( p15(X20,X21) % 3.59/3.66 | ~ p14(X23,X20) % 3.59/3.66 | ~ p15(X23,X22) % 3.59/3.66 | ~ p10(X22,X21) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p13_28,negated_conjecture, % 3.59/3.66 ( p13(X13,X14) % 3.59/3.66 | ~ p5(X15,X13) % 3.59/3.66 | ~ p5(X16,X14) % 3.59/3.66 | ~ p13(X15,X16) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_29,negated_conjecture, % 3.59/3.66 ( p5(X37,c20) % 3.59/3.66 | ~ p13(X37,c21) % 3.59/3.66 | ~ p13(c19,X37) % 3.59/3.66 | ~ p15(c24,c18) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_30,negated_conjecture, % 3.59/3.66 ( p5(f8(X40,X41),f8(X42,X43)) % 3.59/3.66 | ~ p2(X40,X42) % 3.59/3.66 | ~ p5(X41,X43) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_31,negated_conjecture, % 3.59/3.66 ( p5(X37,c20) % 3.59/3.66 | ~ p13(X37,c21) % 3.59/3.66 | ~ p13(c19,X37) % 3.59/3.66 | ~ p5(f8(c17,X37),f6(f7(c22))) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p5_32,negated_conjecture, % 3.59/3.66 ( p5(X37,c20) % 3.59/3.66 | ~ p13(X37,c21) % 3.59/3.66 | ~ p13(c19,X37) % 3.59/3.66 | ~ p5(f8(c16,X37),f6(f7(c22))) ) ). % 3.59/3.66 % 3.59/3.66 cnf(p11_33,negated_conjecture, % 3.59/3.66 ( p11(X3,X4,X5) % 3.59/3.66 | ~ p2(X8,X4) % 3.59/3.66 | ~ p2(X7,X3) % 3.59/3.66 | ~ p10(X6,X5) % 3.59/3.66 | ~ p11(X7,X8,X6) ) ). % 3.59/3.66 % 3.59/3.66 %-------------------------------------------------------------------------- % 3.59/3.66 %------------------------------------------- % 3.59/3.66 % Proof found % 3.59/3.66 % SZS status Theorem for theBenchmark % 3.59/3.66 % SZS output start Proof % 3.59/3.66 %ClaNum:33(EqnAxiom:0) % 3.59/3.66 %VarNum:111(SingletonVarNum:53) % 3.59/3.66 %MaxLitNum:5 % 3.59/3.66 %MaxfuncDepth:2 % 3.59/3.66 %SharedTerms:27 % 3.59/3.66 %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 % 3.59/3.66 %singleGoalClaCount:16 % 3.59/3.66 [1]P1(a1) % 3.59/3.66 [2]P2(a2,a5) % 3.59/3.66 [3]P2(a5,a6) % 3.59/3.66 [4]P5(a2,a7) % 3.59/3.66 [5]P5(a2,a6) % 3.59/3.66 [6]P5(a7,a6) % 3.59/3.66 [14]P4(a1,a3,a4) % 3.59/3.66 [12]P8(a3,f9(a1)) % 3.59/3.66 [13]P6(f11(a1,a5),f13(f12(a8))) % 3.59/3.66 [15]P6(f11(f9(a1),a7),f13(f12(a8))) % 3.59/3.66 [16]~P6(f11(f9(a1),a5),f13(f12(a8))) % 3.59/3.66 [7]P3(x71,x71) % 3.59/3.66 [8]P6(x81,x81) % 3.59/3.66 [9]P7(x91,x91) % 3.59/3.66 [10]P8(x101,x101) % 3.59/3.66 [11]P9(x111,x111) % 3.59/3.66 [18]~P7(x181,x182)+P6(f13(x181),f13(x182)) % 3.59/3.66 [19]~P7(x191,x192)+P7(f12(x191),f12(x192)) % 3.59/3.66 [20]~P8(x201,x202)+P8(f9(x201),f9(x202)) % 3.59/3.66 [17]~P8(x172,x171)+P1(x171)+~P1(x172) % 3.59/3.66 [21]~P3(x213,x211)+P3(x211,x212)+~P3(x213,x212) % 3.59/3.66 [22]~P6(x223,x221)+P6(x221,x222)+~P6(x223,x222) % 3.59/3.66 [23]~P7(x233,x231)+P7(x231,x232)+~P7(x233,x232) % 3.59/3.66 [24]~P8(x243,x241)+P8(x241,x242)+~P8(x243,x242) % 3.59/3.66 [25]~P9(x253,x251)+P9(x251,x252)+~P9(x253,x252) % 3.59/3.66 [30]~P6(x302,x304)+~P8(x301,x303)+P6(f11(x301,x302),f11(x303,x304)) % 3.59/3.66 [26]~P5(x261,a6)+~P5(a2,x261)+P6(x261,a5)+~P10(a10,a4) % 3.59/3.66 [31]~P5(x311,a6)+~P5(a2,x311)+P6(x311,a5)+~P6(f11(a1,x311),f13(f12(a8))) % 3.59/3.66 [32]~P5(x321,a6)+~P5(a2,x321)+P6(x321,a5)+~P6(f11(a3,x321),f13(f12(a8))) % 3.59/3.66 [27]~P2(x274,x273)+P2(x271,x272)+~P6(x273,x272)+~P6(x274,x271) % 3.59/3.66 [28]~P5(x284,x283)+P5(x281,x282)+~P6(x283,x282)+~P6(x284,x281) % 3.59/3.66 [29]~P10(x294,x293)+P10(x291,x292)+~P3(x293,x292)+~P9(x294,x291) % 3.59/3.66 [33]~P4(x335,x336,x334)+P4(x331,x332,x333)+~P3(x334,x333)+~P8(x335,x331)+~P8(x336,x332) % 3.59/3.66 %EqnAxiom % 3.59/3.66 % 3.59/3.66 %------------------------------------------- % 3.59/3.66 cnf(40,plain, % 3.59/3.66 (P8(f9(a1),a3)), % 3.59/3.67 inference(scs_inference,[],[12,15,10,8,22,24])). % 3.59/3.67 cnf(901,plain, % 3.59/3.67 (~P6(a7,a5)), % 3.59/3.67 inference(scs_inference,[],[15,10,16,22,30])). % 3.59/3.67 cnf(1656,plain, % 3.59/3.67 (~P6(a2,x16561)+P5(x16561,a7)), % 3.59/3.67 inference(scs_inference,[],[8,4,28])). % 3.59/3.67 cnf(2124,plain, % 3.59/3.67 (~P6(f11(a3,a7),f13(f12(a8)))), % 3.59/3.67 inference(scs_inference,[],[8,901,6,1656,32])). % 3.59/3.67 cnf(2212,plain, % 3.59/3.67 ($false), % 3.59/3.67 inference(scs_inference,[],[2124,40,8,15,22,30]), % 3.59/3.67 ['proof']). % 3.59/3.67 % SZS output end Proof % 3.59/3.67 % Total time :3.060000s %------------------------------------------------------------------------------