%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN643-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 : n029.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:11 EDT 2024 % Result : Unsatisfiable 221.75s 221.81s % Output : CNFRefutation 221.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN643-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n029.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 22:17:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.47/0.55 start to proof:theBenchmark % 221.75/221.76 %------------------------------------------- % 221.75/221.76 % File :CSE---1.7 % 221.75/221.76 % Problem :theBenchmark % 221.75/221.76 % Transform :cnf % 221.75/221.76 % Format :tptp:raw % 221.75/221.76 % Command :java -jar mcs_scs.jar %d %s % 221.75/221.76 % 221.75/221.76 % Result :Theorem 221.100000s % 221.75/221.76 % Output :CNFRefutation 221.100000s % 221.75/221.76 %------------------------------------------- % 221.75/221.80 %-------------------------------------------------------------------------- % 221.75/221.80 % File : SYN643-1 : TPTP v8.2.0. Released v2.5.0. % 221.75/221.80 % Domain : Syntactic % 221.75/221.80 % Problem : Harrison problem 4298 % 221.75/221.80 % Version : Especial. % 221.75/221.80 % English : % 221.75/221.80 % 221.75/221.80 % Refs : [Har01] Email to G. Sutcliffe % 221.75/221.80 % Source : [Har01] % 221.75/221.80 % Names : % 221.75/221.80 % 221.75/221.80 % Status : Unsatisfiable % 221.75/221.80 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v3.5.0, 0.14 v3.4.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 221.75/221.80 % Syntax : Number of clauses : 42 ( 15 unt; 7 nHn; 35 RR) % 221.75/221.80 % Number of literals : 100 ( 0 equ; 51 neg) % 221.75/221.80 % Maximal clause size : 6 ( 2 avg) % 221.75/221.80 % Maximal term depth : 4 ( 1 avg) % 221.75/221.80 % Number of predicates : 8 ( 8 usr; 0 prp; 1-3 aty) % 221.75/221.80 % Number of functors : 11 ( 11 usr; 3 con; 0-2 aty) % 221.75/221.80 % Number of variables : 82 ( 0 sgn) % 221.75/221.80 % SPC : CNF_UNS_RFO_NEQ_NHN % 221.75/221.80 % 221.75/221.80 % Comments : % 221.75/221.80 %-------------------------------------------------------------------------- % 221.75/221.80 cnf(f3_is_p15_1,negated_conjecture, % 221.75/221.80 p15(f3(c19)) ). % 221.75/221.80 % 221.75/221.80 cnf(f3_is_p15_2,negated_conjecture, % 221.75/221.80 p15(f3(c18)) ). % 221.75/221.80 % 221.75/221.80 cnf(p11_3,negated_conjecture, % 221.75/221.80 p11(X0,X0) ). % 221.75/221.80 % 221.75/221.80 cnf(p6_4,negated_conjecture, % 221.75/221.80 p6(X45,X45) ). % 221.75/221.80 % 221.75/221.80 cnf(p4_5,negated_conjecture, % 221.75/221.80 p4(X36,X36) ). % 221.75/221.80 % 221.75/221.80 cnf(p2_6,negated_conjecture, % 221.75/221.80 p2(X27,X27) ). % 221.75/221.81 % 221.75/221.81 cnf(p16_7,negated_conjecture, % 221.75/221.81 p16(X18,X18) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_8,negated_conjecture, % 221.75/221.81 p12(X3,X3) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_9,negated_conjecture, % 221.75/221.81 p6(f8(f3(c19)),f8(c19)) ). % 221.75/221.81 % 221.75/221.81 cnf(p4_10,negated_conjecture, % 221.75/221.81 p4(f5(f3(c18)),f5(c18)) ). % 221.75/221.81 % 221.75/221.81 cnf(p4_11,negated_conjecture, % 221.75/221.81 p4(f5(f3(c19)),f5(c19)) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_12,negated_conjecture, % 221.75/221.81 p6(f7(f3(c18)),f7(c18)) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_13,negated_conjecture, % 221.75/221.81 p6(f7(f3(c19)),f7(c19)) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_14,negated_conjecture, % 221.75/221.81 p6(f8(f3(c18)),f8(c18)) ). % 221.75/221.81 % 221.75/221.81 cnf(p15_15,negated_conjecture, % 221.75/221.81 ( p15(X16) % 221.75/221.81 | ~ p15(X17) % 221.75/221.81 | ~ p2(X17,X16) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_16,negated_conjecture, % 221.75/221.81 ( p12(f13(X6),f13(X7)) % 221.75/221.81 | ~ p11(X6,X7) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_17,negated_conjecture, % 221.75/221.81 ( p6(f8(X54),f8(X55)) % 221.75/221.81 | ~ p2(X54,X55) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_18,negated_conjecture, % 221.75/221.81 ( p6(f7(X52),f7(X53)) % 221.75/221.81 | ~ p2(X52,X53) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p4_19,negated_conjecture, % 221.75/221.81 ( p4(f5(X39),f5(X40)) % 221.75/221.81 | ~ p2(X39,X40) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p2_20,negated_conjecture, % 221.75/221.81 ( p2(f3(X34),f3(X35)) % 221.75/221.81 | ~ p2(X34,X35) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p15_21,negated_conjecture, % 221.75/221.81 ( p15(f10(X14,X15)) % 221.75/221.81 | ~ p15(X14) % 221.75/221.81 | ~ p15(X15) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p11_22,negated_conjecture, % 221.75/221.81 ( p11(X1,X2) % 221.75/221.81 | ~ p11(X0,X1) % 221.75/221.81 | ~ p11(X0,X2) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_23,negated_conjecture, % 221.75/221.81 ( p6(X46,X47) % 221.75/221.81 | ~ p6(X45,X46) % 221.75/221.81 | ~ p6(X45,X47) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p4_24,negated_conjecture, % 221.75/221.81 ( p4(X37,X38) % 221.75/221.81 | ~ p4(X36,X37) % 221.75/221.81 | ~ p4(X36,X38) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p2_25,negated_conjecture, % 221.75/221.81 ( p2(X28,X29) % 221.75/221.81 | ~ p2(X27,X28) % 221.75/221.81 | ~ p2(X27,X29) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p16_26,negated_conjecture, % 221.75/221.81 ( p16(X19,X20) % 221.75/221.81 | ~ p16(X18,X19) % 221.75/221.81 | ~ p16(X18,X20) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_27,negated_conjecture, % 221.75/221.81 ( p12(X4,X5) % 221.75/221.81 | ~ p12(X3,X4) % 221.75/221.81 | ~ p12(X3,X5) ) ). % 221.75/221.81 % 221.75/221.81 cnf(not_p4_28,negated_conjecture, % 221.75/221.81 ~ p4(f5(f10(f3(c19),f3(c18))),f9(f5(c19),f5(c18))) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_29,negated_conjecture, % 221.75/221.81 ( p12(f13(X8),c20) % 221.75/221.81 | p17(X8,X9,c19) % 221.75/221.81 | ~ p17(X8,X9,f3(c19)) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_30,negated_conjecture, % 221.75/221.81 ( p12(f13(X10),c20) % 221.75/221.81 | p17(X10,X11,c18) % 221.75/221.81 | ~ p17(X10,X11,f3(c18)) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_31,negated_conjecture, % 221.75/221.81 ( p12(f13(X8),c20) % 221.75/221.81 | p17(X8,X9,f3(c19)) % 221.75/221.81 | ~ p17(X8,X9,c19) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_32,negated_conjecture, % 221.75/221.81 ( p12(f13(X10),c20) % 221.75/221.81 | p17(X10,X11,f3(c18)) % 221.75/221.81 | ~ p17(X10,X11,c18) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_33,negated_conjecture, % 221.75/221.81 ( p6(f14(X48,X49),f14(X50,X51)) % 221.75/221.81 | ~ p6(X48,X50) % 221.75/221.81 | ~ p6(X49,X51) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p2_34,negated_conjecture, % 221.75/221.81 ( p2(f10(X30,X31),f10(X32,X33)) % 221.75/221.81 | ~ p2(X30,X32) % 221.75/221.81 | ~ p2(X31,X33) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p4_35,negated_conjecture, % 221.75/221.81 ( p4(f9(X41,X42),f9(X43,X44)) % 221.75/221.81 | ~ p4(X42,X44) % 221.75/221.81 | ~ p4(X41,X43) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_36,negated_conjecture, % 221.75/221.81 ( p6(f8(f10(X14,X15)),f14(f8(X14),f8(X15))) % 221.75/221.81 | ~ p15(X14) % 221.75/221.81 | ~ p15(X15) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p4_37,negated_conjecture, % 221.75/221.81 ( p4(f5(f10(X14,X15)),f9(f5(X14),f5(X15))) % 221.75/221.81 | ~ p15(X14) % 221.75/221.81 | ~ p15(X15) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p6_38,negated_conjecture, % 221.75/221.81 ( p6(f7(f10(X14,X15)),f14(f7(X14),f7(X15))) % 221.75/221.81 | ~ p15(X14) % 221.75/221.81 | ~ p15(X15) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p17_39,negated_conjecture, % 221.75/221.81 ( p17(X21,X22,X23) % 221.75/221.81 | ~ p2(X26,X23) % 221.75/221.81 | ~ p16(X25,X22) % 221.75/221.81 | ~ p11(X24,X21) % 221.75/221.81 | ~ p17(X24,X25,X26) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_40,negated_conjecture, % 221.75/221.81 ( p12(f13(X12),c20) % 221.75/221.81 | p17(X12,X13,X14) % 221.75/221.81 | p17(X12,X13,f10(X14,X15)) % 221.75/221.81 | ~ p15(X14) % 221.75/221.81 | ~ p15(X15) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_41,negated_conjecture, % 221.75/221.81 ( p12(f13(X12),c20) % 221.75/221.81 | p17(X12,X13,f10(X14,X15)) % 221.75/221.81 | ~ p15(X14) % 221.75/221.81 | ~ p15(X15) % 221.75/221.81 | ~ p17(X12,X13,X15) ) ). % 221.75/221.81 % 221.75/221.81 cnf(p12_42,negated_conjecture, % 221.75/221.81 ( p12(f13(X12),c20) % 221.75/221.81 | p17(X12,X13,X15) % 221.75/221.81 | ~ p15(X14) % 221.75/221.81 | ~ p15(X15) % 221.75/221.81 | ~ p17(X12,X13,X14) % 221.75/221.81 | ~ p17(X12,X13,f10(X14,X15)) ) ). % 221.75/221.81 % 221.75/221.81 %-------------------------------------------------------------------------- % 221.75/221.81 %------------------------------------------- % 221.75/221.81 % Proof found % 221.75/221.81 % SZS status Theorem for theBenchmark % 221.75/221.81 % SZS output start Proof % 221.75/221.85 %ClaNum:42(EqnAxiom:0) % 221.75/221.85 %VarNum:183(SingletonVarNum:82) % 221.75/221.85 %MaxLitNum:6 % 221.75/221.85 %MaxfuncDepth:3 % 221.75/221.85 %SharedTerms:29 % 221.75/221.85 %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 37 38 39 40 41 42 % 221.75/221.85 %singleGoalClaCount:15 % 221.75/221.85 [1]P1(f3(a1)) % 221.75/221.85 [2]P1(f3(a2)) % 221.75/221.85 [9]P4(f8(f3(a1)),f8(a1)) % 221.75/221.85 [10]P4(f8(f3(a2)),f8(a2)) % 221.75/221.85 [11]P4(f9(f3(a1)),f9(a1)) % 221.75/221.85 [12]P4(f9(f3(a2)),f9(a2)) % 221.75/221.85 [13]P5(f10(f3(a1)),f10(a1)) % 221.75/221.85 [14]P5(f10(f3(a2)),f10(a2)) % 221.75/221.85 [15]~P5(f10(f4(f3(a1),f3(a2))),f11(f10(a1),f10(a2))) % 221.75/221.85 [3]P2(x31,x31) % 221.75/221.85 [4]P4(x41,x41) % 221.75/221.85 [5]P5(x51,x51) % 221.75/221.85 [6]P6(x61,x61) % 221.75/221.85 [7]P7(x71,x71) % 221.75/221.85 [8]P3(x81,x81) % 221.75/221.85 [18]~P6(x181,x182)+P4(f8(x181),f8(x182)) % 221.75/221.85 [19]~P6(x191,x192)+P4(f9(x191),f9(x192)) % 221.75/221.85 [20]~P6(x201,x202)+P5(f10(x201),f10(x202)) % 221.75/221.85 [21]~P6(x211,x212)+P6(f3(x211),f3(x212)) % 221.75/221.85 [22]~P2(x221,x222)+P3(f6(x221),f6(x222)) % 221.75/221.85 [16]~P6(x162,x161)+P1(x161)+~P1(x162) % 221.75/221.85 [17]~P1(x172)+~P1(x171)+P1(f4(x171,x172)) % 221.75/221.85 [35]~P8(x351,x352,a1)+P8(x351,x352,f3(a1))+P3(f6(x351),a5) % 221.75/221.85 [36]~P8(x361,x362,a2)+P8(x361,x362,f3(a2))+P3(f6(x361),a5) % 221.75/221.85 [37]P8(x371,x372,a1)+~P8(x371,x372,f3(a1))+P3(f6(x371),a5) % 221.75/221.85 [38]P8(x381,x382,a2)+~P8(x381,x382,f3(a2))+P3(f6(x381),a5) % 221.75/221.85 [32]~P1(x322)+~P1(x321)+P4(f8(f4(x321,x322)),f7(f8(x321),f8(x322))) % 221.75/221.85 [33]~P1(x332)+~P1(x331)+P4(f9(f4(x331,x332)),f7(f9(x331),f9(x332))) % 221.75/221.85 [34]~P1(x342)+~P1(x341)+P5(f10(f4(x341,x342)),f11(f10(x341),f10(x342))) % 221.75/221.85 [23]~P2(x233,x231)+P2(x231,x232)+~P2(x233,x232) % 221.75/221.85 [24]~P4(x243,x241)+P4(x241,x242)+~P4(x243,x242) % 221.75/221.85 [25]~P5(x253,x251)+P5(x251,x252)+~P5(x253,x252) % 221.75/221.85 [26]~P6(x263,x261)+P6(x261,x262)+~P6(x263,x262) % 221.75/221.85 [27]~P7(x273,x271)+P7(x271,x272)+~P7(x273,x272) % 221.75/221.85 [28]~P3(x283,x281)+P3(x281,x282)+~P3(x283,x282) % 221.75/221.85 [29]~P4(x292,x294)+~P4(x291,x293)+P4(f7(x291,x292),f7(x293,x294)) % 221.75/221.85 [30]~P5(x302,x304)+~P5(x301,x303)+P5(f11(x301,x302),f11(x303,x304)) % 221.75/221.85 [31]~P6(x312,x314)+~P6(x311,x313)+P6(f4(x311,x312),f4(x313,x314)) % 221.75/221.85 [39]~P1(x394)+~P1(x393)+P8(x391,x392,x393)+P8(x391,x392,f4(x393,x394))+P3(f6(x391),a5) % 221.75/221.85 [40]~P1(x404)+~P1(x403)+~P8(x401,x402,x404)+P8(x401,x402,f4(x403,x404))+P3(f6(x401),a5) % 221.75/221.85 [41]~P8(x414,x416,x415)+P8(x411,x412,x413)+~P2(x414,x411)+~P6(x415,x413)+~P7(x416,x412) % 221.75/221.85 [42]~P1(x423)+~P8(x421,x422,x424)+P8(x421,x422,x423)+~P1(x424)+~P8(x421,x422,f4(x424,x423))+P3(f6(x421),a5) % 221.75/221.85 %EqnAxiom % 221.75/221.85 % 221.75/221.85 %------------------------------------------- % 221.92/221.90 cnf(52,plain, % 221.92/221.90 (P4(f9(a1),f9(f3(a1)))), % 221.92/221.90 inference(scs_inference,[],[11,4,24])). % 221.92/221.90 cnf(105,plain, % 221.92/221.90 (~P5(f11(f10(a1),f10(a2)),f10(f4(f3(a1),f3(a2))))), % 221.92/221.90 inference(scs_inference,[],[15,5,25])). % 221.92/221.90 cnf(229,plain, % 221.92/221.90 (P5(f11(f10(f3(a1)),x2291),f11(f10(a1),x2291))), % 221.92/221.90 inference(scs_inference,[],[13,5,30])). % 221.92/221.90 cnf(237,plain, % 221.92/221.90 (P5(f11(x2371,f10(f3(a2))),f11(x2371,f10(a2)))), % 221.92/221.90 inference(scs_inference,[],[14,5,30])). % 221.92/221.90 cnf(275,plain, % 221.92/221.90 (~P5(f11(f10(a1),f10(f3(a2))),f10(f4(f3(a1),f3(a2))))), % 221.92/221.90 inference(scs_inference,[],[52,237,105,4,29,25])). % 221.92/221.90 cnf(3342,plain, % 221.92/221.90 (~P5(f11(f10(f3(a1)),f10(f3(a2))),f10(f4(f3(a1),f3(a2))))), % 221.92/221.90 inference(scs_inference,[],[229,275,25])). % 221.92/221.90 cnf(39698,plain, % 221.92/221.90 (~P5(f10(f4(f3(a1),f3(a2))),f11(f10(f3(a1)),f10(f3(a2))))), % 221.92/221.90 inference(scs_inference,[],[6,3342,20,25])). % 221.92/221.90 cnf(40133,plain, % 221.92/221.90 ($false), % 221.92/221.90 inference(scs_inference,[],[39698,2,1,6,34,16]), % 221.92/221.90 ['proof']). % 221.92/221.93 % SZS output end Proof % 221.92/221.93 % Total time :221.100000s %------------------------------------------------------------------------------