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