%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN693-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 : n021.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:19 EDT 2024 % Result : Unsatisfiable 108.36s 108.42s % Output : CNFRefutation 108.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN693-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.12/0.33 % Computer : n021.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:14:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 108.36/108.40 %------------------------------------------- % 108.36/108.40 % File :CSE---1.7 % 108.36/108.40 % Problem :theBenchmark % 108.36/108.40 % Transform :cnf % 108.36/108.40 % Format :tptp:raw % 108.36/108.40 % Command :java -jar mcs_scs.jar %d %s % 108.36/108.40 % 108.36/108.40 % Result :Theorem 107.790000s % 108.36/108.40 % Output :CNFRefutation 107.790000s % 108.36/108.40 %------------------------------------------- % 108.36/108.41 %-------------------------------------------------------------------------- % 108.36/108.41 % File : SYN693-1 : TPTP v8.2.0. Released v2.5.0. % 108.36/108.41 % Domain : Syntactic % 108.36/108.41 % Problem : Harrison problem 4627 % 108.36/108.41 % Version : Especial. % 108.36/108.41 % English : % 108.36/108.41 % 108.36/108.41 % Refs : [Har01] Email to G. Sutcliffe % 108.36/108.41 % Source : [Har01] % 108.36/108.41 % Names : % 108.36/108.41 % 108.36/108.41 % Status : Unsatisfiable % 108.36/108.41 % Rating : 0.00 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.20 v5.2.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.29 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 108.36/108.41 % Syntax : Number of clauses : 69 ( 27 unt; 2 nHn; 59 RR) % 108.36/108.41 % Number of literals : 149 ( 0 equ; 80 neg) % 108.36/108.41 % Maximal clause size : 5 ( 2 avg) % 108.36/108.41 % Maximal term depth : 6 ( 1 avg) % 108.36/108.41 % Number of predicates : 18 ( 18 usr; 0 prp; 1-3 aty) % 108.36/108.41 % Number of functors : 27 ( 27 usr; 13 con; 0-2 aty) % 108.36/108.41 % Number of variables : 131 ( 5 sgn) % 108.36/108.41 % SPC : CNF_UNS_RFO_NEQ_NHN % 108.36/108.41 % 108.36/108.41 % Comments : % 108.36/108.41 %-------------------------------------------------------------------------- % 108.36/108.41 cnf(c34_is_p25_1,negated_conjecture, % 108.36/108.41 p25(c34) ). % 108.36/108.41 % 108.36/108.41 cnf(c36_is_p29_2,negated_conjecture, % 108.36/108.41 p29(c36) ). % 108.36/108.41 % 108.36/108.41 cnf(f18_is_p30_3,negated_conjecture, % 108.36/108.41 p30(f18(c41)) ). % 108.36/108.41 % 108.36/108.41 cnf(f16_is_p28_4,negated_conjecture, % 108.36/108.41 p28(f16(c38)) ). % 108.36/108.41 % 108.36/108.41 cnf(f16_is_p28_5,negated_conjecture, % 108.36/108.41 p28(f16(c39)) ). % 108.36/108.41 % 108.36/108.41 cnf(f18_is_p30_6,negated_conjecture, % 108.36/108.41 p30(f18(c40)) ). % 108.36/108.41 % 108.36/108.41 cnf(p10_7,negated_conjecture, % 108.36/108.41 p10(X5,X5) ). % 108.36/108.41 % 108.36/108.41 cnf(p7_8,negated_conjecture, % 108.36/108.41 p7(X111,X111) ). % 108.36/108.41 % 108.36/108.41 cnf(p6_9,negated_conjecture, % 108.36/108.41 p6(X108,X108) ). % 108.36/108.41 % 108.36/108.41 cnf(p3_10,negated_conjecture, % 108.36/108.41 p3(X87,X87) ). % 108.36/108.41 % 108.36/108.41 cnf(p21_11,negated_conjecture, % 108.36/108.41 p21(X67,X67) ). % 108.36/108.41 % 108.36/108.41 cnf(p2_12,negated_conjecture, % 108.36/108.41 p2(X43,X43) ). % 108.36/108.41 % 108.36/108.41 cnf(p17_13,negated_conjecture, % 108.36/108.41 p17(X28,X28) ). % 108.36/108.41 % 108.36/108.41 cnf(p14_14,negated_conjecture, % 108.36/108.42 p14(X19,X19) ). % 108.36/108.42 % 108.36/108.42 cnf(p12_15,negated_conjecture, % 108.36/108.42 p12(X12,X12) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_16,negated_conjecture, % 108.36/108.42 p2(c44,c46) ). % 108.36/108.42 % 108.36/108.42 cnf(p31_17,negated_conjecture, % 108.36/108.42 p31(c46,f5(c42)) ). % 108.36/108.42 % 108.36/108.42 cnf(p31_18,negated_conjecture, % 108.36/108.42 p31(c44,f5(c42)) ). % 108.36/108.42 % 108.36/108.42 cnf(p7_19,negated_conjecture, % 108.36/108.42 p7(f8(c35),c36) ). % 108.36/108.42 % 108.36/108.42 cnf(p32_20,negated_conjecture, % 108.36/108.42 p32(f22(c34,c45),c43) ). % 108.36/108.42 % 108.36/108.42 cnf(p31_21,negated_conjecture, % 108.36/108.42 p31(f23(c44,f9(f20(c37))),c46) ). % 108.36/108.42 % 108.36/108.42 cnf(p26_22,negated_conjecture, % 108.36/108.42 p26(c34,f4(f5(X78)),f4(X78)) ). % 108.36/108.42 % 108.36/108.42 cnf(p25_23,negated_conjecture, % 108.36/108.42 ( p25(X70) % 108.36/108.42 | ~ p25(X71) % 108.36/108.42 | ~ p21(X71,X70) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p30_24,negated_conjecture, % 108.36/108.42 ( p30(X92) % 108.36/108.42 | ~ p30(X93) % 108.36/108.42 | ~ p17(X93,X92) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p29_25,negated_conjecture, % 108.36/108.42 ( p29(X85) % 108.36/108.42 | ~ p29(X86) % 108.36/108.42 | ~ p7(X86,X85) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p28_26,negated_conjecture, % 108.36/108.42 ( p28(X83) % 108.36/108.42 | ~ p28(X84) % 108.36/108.42 | ~ p14(X84,X83) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p7_27,negated_conjecture, % 108.36/108.42 ( p7(f8(X114),f8(X115)) % 108.36/108.42 | ~ p6(X114,X115) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p14_28,negated_conjecture, % 108.36/108.42 ( p14(f16(X26),f16(X27)) % 108.36/108.42 | ~ p14(X26,X27) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p17_29,negated_conjecture, % 108.36/108.42 ( p17(f18(X31),f18(X32)) % 108.36/108.42 | ~ p17(X31,X32) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_30,negated_conjecture, % 108.36/108.42 ( p2(f20(X55),f20(X56)) % 108.36/108.42 | ~ p2(X55,X56) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_31,negated_conjecture, % 108.36/108.42 ( p2(f24(X61),f24(X62)) % 108.36/108.42 | ~ p2(X61,X62) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_32,negated_conjecture, % 108.36/108.42 ( p2(f5(X63),f5(X64)) % 108.36/108.42 | ~ p2(X63,X64) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_33,negated_conjecture, % 108.36/108.42 ( p2(f9(X65),f9(X66)) % 108.36/108.42 | ~ p2(X65,X66) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p3_34,negated_conjecture, % 108.36/108.42 ( p3(f4(X90),f4(X91)) % 108.36/108.42 | ~ p2(X90,X91) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p10_35,negated_conjecture, % 108.36/108.42 ( p10(X6,X7) % 108.36/108.42 | ~ p10(X5,X6) % 108.36/108.42 | ~ p10(X5,X7) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p7_36,negated_conjecture, % 108.36/108.42 ( p7(X112,X113) % 108.36/108.42 | ~ p7(X111,X112) % 108.36/108.42 | ~ p7(X111,X113) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p6_37,negated_conjecture, % 108.36/108.42 ( p6(X109,X110) % 108.36/108.42 | ~ p6(X108,X109) % 108.36/108.42 | ~ p6(X108,X110) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p3_38,negated_conjecture, % 108.36/108.42 ( p3(X88,X89) % 108.36/108.42 | ~ p3(X87,X88) % 108.36/108.42 | ~ p3(X87,X89) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p21_39,negated_conjecture, % 108.36/108.42 ( p21(X68,X69) % 108.36/108.42 | ~ p21(X67,X68) % 108.36/108.42 | ~ p21(X67,X69) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_40,negated_conjecture, % 108.36/108.42 ( p2(X44,X45) % 108.36/108.42 | ~ p2(X43,X44) % 108.36/108.42 | ~ p2(X43,X45) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p17_41,negated_conjecture, % 108.36/108.42 ( p17(X29,X30) % 108.36/108.42 | ~ p17(X28,X29) % 108.36/108.42 | ~ p17(X28,X30) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p14_42,negated_conjecture, % 108.36/108.42 ( p14(X20,X21) % 108.36/108.42 | ~ p14(X19,X20) % 108.36/108.42 | ~ p14(X19,X21) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p12_43,negated_conjecture, % 108.36/108.42 ( p12(X13,X14) % 108.36/108.42 | ~ p12(X12,X13) % 108.36/108.42 | ~ p12(X12,X14) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p33_44,negated_conjecture, % 108.36/108.42 p33(f11(f4(f5(c42)),c45),f11(f4(c42),c45)) ). % 108.36/108.42 % 108.36/108.42 cnf(p31_45,negated_conjecture, % 108.36/108.42 ( p31(X94,f24(X94)) % 108.36/108.42 | ~ p31(X94,c44) % 108.36/108.42 | ~ p31(X94,f5(c42)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p31_46,negated_conjecture, % 108.36/108.42 ( p31(f24(X94),f5(c42)) % 108.36/108.42 | ~ p31(X94,c44) % 108.36/108.42 | ~ p31(X94,f5(c42)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p33_47,negated_conjecture, % 108.36/108.42 ( p33(X104,X105) % 108.36/108.42 | ~ p2(X107,X105) % 108.36/108.42 | ~ p33(X106,X107) % 108.36/108.42 | ~ p2(X106,X104) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p27_48,negated_conjecture, % 108.36/108.42 ( p27(X79,X80) % 108.36/108.42 | ~ p14(X82,X79) % 108.36/108.42 | ~ p27(X82,X81) % 108.36/108.42 | ~ p12(X81,X80) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p31_49,negated_conjecture, % 108.36/108.42 ( p31(X95,X96) % 108.36/108.42 | ~ p2(X98,X96) % 108.36/108.42 | ~ p31(X97,X98) % 108.36/108.42 | ~ p2(X97,X95) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p32_50,negated_conjecture, % 108.36/108.42 ( p32(X99,X100) % 108.36/108.42 | ~ p17(X102,X99) % 108.36/108.42 | ~ p32(X102,X101) % 108.36/108.42 | ~ p10(X101,X100) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_51,negated_conjecture, % 108.36/108.42 p2(f11(f4(c42),c45),f11(f4(f23(c42,f9(f20(c37)))),c45)) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_52,negated_conjecture, % 108.36/108.42 p2(f11(f4(f23(c44,f9(f20(c37)))),c43),f11(f4(c44),c43)) ). % 108.36/108.42 % 108.36/108.42 cnf(not_p2_53,negated_conjecture, % 108.36/108.42 ~ p2(f11(f4(c46),c43),f11(f4(f23(c44,f9(f20(c37)))),c43)) ). % 108.36/108.42 % 108.36/108.42 cnf(p10_54,negated_conjecture, % 108.36/108.42 ( p10(X0,c43) % 108.36/108.42 | ~ p31(f11(f4(f5(c42)),X0),f11(f4(c42),X0)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p12_55,negated_conjecture, % 108.36/108.42 ( p12(f13(X15,X16),f13(X17,X18)) % 108.36/108.42 | ~ p10(X15,X17) % 108.36/108.42 | ~ p2(X16,X18) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_56,negated_conjecture, % 108.36/108.42 ( p2(f23(X57,X58),f23(X59,X60)) % 108.36/108.42 | ~ p2(X57,X59) % 108.36/108.42 | ~ p2(X58,X60) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_57,negated_conjecture, % 108.36/108.42 ( p2(f19(X51,X52),f19(X53,X54)) % 108.36/108.42 | ~ p2(X51,X53) % 108.36/108.42 | ~ p2(X52,X54) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_58,negated_conjecture, % 108.36/108.42 ( p2(f11(X46,X47),f11(X48,X49)) % 108.36/108.42 | ~ p10(X47,X49) % 108.36/108.42 | ~ p3(X46,X48) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p17_59,negated_conjecture, % 108.36/108.42 ( p17(f22(X33,X34),f22(X35,X36)) % 108.36/108.42 | ~ p10(X34,X36) % 108.36/108.42 | ~ p21(X33,X35) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p14_60,negated_conjecture, % 108.36/108.42 ( p14(f15(X22,X23),f15(X24,X25)) % 108.36/108.42 | ~ p12(X23,X25) % 108.36/108.42 | ~ p7(X22,X24) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_61,negated_conjecture, % 108.36/108.42 p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),f11(f4(c42),c43)) ). % 108.36/108.42 % 108.36/108.42 cnf(p32_62,negated_conjecture, % 108.36/108.42 ( p32(f22(c34,X103),c43) % 108.36/108.42 | ~ p33(f11(f4(f5(c42)),X103),f11(f4(c42),X103)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_63,negated_conjecture, % 108.36/108.42 ( p2(f11(f4(X50),c43),f11(f4(c44),c43)) % 108.36/108.42 | ~ p31(c44,X50) % 108.36/108.42 | ~ p31(X50,f5(c42)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p10_64,negated_conjecture, % 108.36/108.42 ( p10(X1,X2) % 108.36/108.42 | p32(f22(c34,X1),X2) % 108.36/108.42 | ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(not_p31_65,negated_conjecture, % 108.36/108.42 ( ~ p31(X94,c44) % 108.36/108.42 | ~ p31(X94,f5(c42)) % 108.36/108.42 | ~ p2(f11(f4(f24(X94)),c43),f11(f4(X94),c43)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p26_66,negated_conjecture, % 108.36/108.42 ( p26(X72,X73,X74) % 108.36/108.42 | ~ p3(X77,X74) % 108.36/108.42 | ~ p3(X76,X73) % 108.36/108.42 | ~ p21(X75,X72) % 108.36/108.42 | ~ p26(X75,X76,X77) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p10_67,negated_conjecture, % 108.36/108.42 ( p10(X8,X9) % 108.36/108.42 | ~ p2(f11(f4(X10),X8),f9(c37)) % 108.36/108.42 | ~ p27(f15(c36,f13(X8,X10)),f13(X9,X11)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p2_68,negated_conjecture, % 108.36/108.42 ( p2(X37,X38) % 108.36/108.42 | ~ p27(f15(c36,f13(X39,X37)),f13(X40,X41)) % 108.36/108.42 | ~ p27(f15(c36,f13(X42,X38)),f13(X40,X41)) ) ). % 108.36/108.42 % 108.36/108.42 cnf(p32_69,negated_conjecture, % 108.36/108.42 ( p32(f22(c34,X1),X2) % 108.36/108.42 | p31(f11(f4(X3),X2),f11(f4(X4),X2)) % 108.36/108.42 | ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4)) ) ). % 108.36/108.42 % 108.36/108.42 %-------------------------------------------------------------------------- % 108.36/108.42 %------------------------------------------- % 108.36/108.42 % Proof found % 108.36/108.42 % SZS status Theorem for theBenchmark % 108.36/108.42 % SZS output start Proof % 108.36/108.43 %ClaNum:69(EqnAxiom:0) % 108.36/108.43 %VarNum:270(SingletonVarNum:131) % 108.36/108.43 %MaxLitNum:5 % 108.43/108.43 %MaxfuncDepth:5 % 108.43/108.43 %SharedTerms:57 % 108.43/108.43 %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 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 % 108.43/108.43 %singleGoalClaCount:27 % 108.43/108.43 [1]P1(a1) % 108.43/108.43 [2]P8(a2) % 108.43/108.43 [7]P2(a11,a14) % 108.43/108.43 [3]P12(f9(a4)) % 108.43/108.43 [4]P12(f9(a5)) % 108.43/108.43 [5]P9(f10(a6)) % 108.43/108.43 [6]P9(f10(a8)) % 108.43/108.43 [17]P16(a11,f19(a12)) % 108.43/108.43 [18]P16(a14,f19(a12)) % 108.43/108.43 [19]P14(f26(a3),a2) % 108.43/108.43 [20]P17(f20(a1,a15),a13) % 108.43/108.43 [21]P16(f23(a11,f27(f21(a7))),a14) % 108.43/108.43 [23]P18(f16(f24(f19(a12)),a15),f16(f24(a12),a15)) % 108.43/108.43 [24]P2(f22(f16(f24(f19(a12)),a13),f27(f21(a7))),f16(f24(a12),a13)) % 108.43/108.43 [25]P2(f16(f24(a12),a15),f16(f24(f23(a12,f27(f21(a7)))),a15)) % 108.43/108.43 [26]P2(f16(f24(f23(a11,f27(f21(a7)))),a13),f16(f24(a11),a13)) % 108.43/108.43 [27]~P2(f16(f24(a14),a13),f16(f24(f23(a11,f27(f21(a7)))),a13)) % 108.43/108.43 [8]P3(x81,x81) % 108.43/108.43 [9]P14(x91,x91) % 108.43/108.43 [10]P15(x101,x101) % 108.43/108.43 [11]P13(x111,x111) % 108.43/108.43 [12]P7(x121,x121) % 108.43/108.43 [13]P2(x131,x131) % 108.43/108.43 [14]P4(x141,x141) % 108.43/108.43 [15]P5(x151,x151) % 108.43/108.43 [16]P6(x161,x161) % 108.43/108.43 [22]P10(a1,f24(f19(x221)),f24(x221)) % 108.43/108.43 [62]P3(x621,a13)+~P16(f16(f24(f19(a12)),x621),f16(f24(a12),x621)) % 108.43/108.43 [63]P17(f20(a1,x631),a13)+~P18(f16(f24(f19(a12)),x631),f16(f24(a12),x631)) % 108.43/108.43 [32]~P15(x321,x322)+P14(f26(x321),f26(x322)) % 108.43/108.43 [33]~P2(x331,x332)+P13(f24(x331),f24(x332)) % 108.43/108.43 [34]~P2(x341,x342)+P2(f19(x341),f19(x342)) % 108.43/108.43 [35]~P2(x351,x352)+P2(f21(x351),f21(x352)) % 108.43/108.43 [36]~P2(x361,x362)+P2(f27(x361),f27(x362)) % 108.43/108.43 [37]~P2(x371,x372)+P2(f25(x371),f25(x372)) % 108.43/108.43 [38]~P4(x381,x382)+P4(f9(x381),f9(x382)) % 108.43/108.43 [39]~P5(x391,x392)+P5(f10(x391),f10(x392)) % 108.43/108.43 [49]~P16(x491,a11)+P16(x491,f25(x491))+~P16(x491,f19(a12)) % 108.43/108.43 [50]~P16(x501,a11)+~P16(x501,f19(a12))+P16(f25(x501),f19(a12)) % 108.43/108.43 [61]~P16(a11,x611)+~P16(x611,f19(a12))+P2(f16(f24(x611),a13),f16(f24(a11),a13)) % 108.43/108.43 [65]~P16(x651,a11)+~P16(x651,f19(a12))+~P2(f16(f24(f25(x651)),a13),f16(f24(x651),a13)) % 108.43/108.43 [28]~P7(x282,x281)+P1(x281)+~P1(x282) % 108.43/108.43 [29]~P14(x292,x291)+P8(x291)+~P8(x292) % 108.43/108.43 [30]~P4(x302,x301)+P12(x301)+~P12(x302) % 108.43/108.43 [31]~P5(x312,x311)+P9(x311)+~P9(x312) % 108.43/108.43 [40]~P3(x403,x401)+P3(x401,x402)+~P3(x403,x402) % 108.43/108.43 [41]~P14(x413,x411)+P14(x411,x412)+~P14(x413,x412) % 108.43/108.43 [42]~P15(x423,x421)+P15(x421,x422)+~P15(x423,x422) % 108.43/108.43 [43]~P13(x433,x431)+P13(x431,x432)+~P13(x433,x432) % 108.43/108.43 [44]~P7(x443,x441)+P7(x441,x442)+~P7(x443,x442) % 108.43/108.43 [45]~P2(x453,x451)+P2(x451,x452)+~P2(x453,x452) % 108.43/108.43 [46]~P4(x463,x461)+P4(x461,x462)+~P4(x463,x462) % 108.43/108.43 [47]~P5(x473,x471)+P5(x471,x472)+~P5(x473,x472) % 108.43/108.43 [48]~P6(x483,x481)+P6(x481,x482)+~P6(x483,x482) % 108.43/108.43 [55]~P2(x552,x554)+~P2(x551,x553)+P2(f23(x551,x552),f23(x553,x554)) % 108.43/108.43 [56]~P3(x562,x564)+~P13(x561,x563)+P2(f16(x561,x562),f16(x563,x564)) % 108.43/108.43 [57]~P2(x572,x574)+~P2(x571,x573)+P2(f22(x571,x572),f22(x573,x574)) % 108.43/108.43 [58]~P3(x582,x584)+~P7(x581,x583)+P4(f20(x581,x582),f20(x583,x584)) % 108.43/108.43 [59]~P14(x591,x593)+~P6(x592,x594)+P5(f17(x591,x592),f17(x593,x594)) % 108.43/108.43 [60]~P3(x601,x603)+~P2(x602,x604)+P6(f18(x601,x602),f18(x603,x604)) % 108.43/108.43 [66]P3(x661,x662)+P17(f20(a1,x661),x662)+~P11(f17(a2,f18(x661,x663)),f18(x662,x664)) % 108.43/108.43 [67]P3(x671,x672)+~P11(f17(a2,f18(x671,x673)),f18(x672,x674))+~P2(f16(f24(x673),x671),f27(a7)) % 108.43/108.43 [68]P17(f20(a1,x681),x682)+P16(f16(f24(x683),x682),f16(f24(x684),x682))+~P11(f17(a2,f18(x681,x683)),f18(x682,x684)) % 108.43/108.43 [69]P2(x691,x692)+~P11(f17(a2,f18(x693,x692)),f18(x694,x695))+~P11(f17(a2,f18(x696,x691)),f18(x694,x695)) % 108.43/108.43 [51]~P16(x513,x514)+P16(x511,x512)+~P2(x513,x511)+~P2(x514,x512) % 108.43/108.43 [52]~P17(x524,x523)+P17(x521,x522)+~P3(x523,x522)+~P4(x524,x521) % 108.43/108.43 [53]~P18(x533,x534)+P18(x531,x532)+~P2(x533,x531)+~P2(x534,x532) % 108.43/108.43 [54]~P11(x543,x544)+P11(x541,x542)+~P5(x543,x541)+~P6(x544,x542) % 108.43/108.43 [64]~P10(x646,x644,x645)+P10(x641,x642,x643)+~P13(x644,x642)+~P13(x645,x643)+~P7(x646,x641) % 108.43/108.43 %EqnAxiom % 108.43/108.43 % 108.43/108.43 %------------------------------------------- % 108.43/108.43 cnf(70,plain, % 108.43/108.43 (~P13(f24(a14),f24(f23(a11,f27(f21(a7)))))), % 108.43/108.43 inference(scs_inference,[],[8,27,56])). % 108.43/108.43 cnf(82,plain, % 108.43/108.43 (P2(a14,a11)), % 108.43/108.43 inference(scs_inference,[],[7,13,45])). % 108.43/108.43 cnf(137,plain, % 108.43/108.43 (P2(f27(f25(a14)),f27(f25(a11)))), % 108.43/108.43 inference(scs_inference,[],[82,36,37])). % 108.43/108.43 cnf(168,plain, % 108.43/108.43 (P14(a2,f26(a3))), % 108.43/108.43 inference(scs_inference,[],[19,9,41])). % 108.43/108.43 cnf(172,plain, % 108.43/108.43 (P5(f10(f17(a2,x1721)),f10(f17(f26(a3),x1721)))), % 108.43/108.43 inference(scs_inference,[],[168,16,39,59])). % 108.43/108.43 cnf(173,plain, % 108.43/108.43 (P5(f10(f17(f26(a3),x1731)),f10(f17(a2,x1731)))), % 108.43/108.43 inference(scs_inference,[],[172,15,47])). % 108.43/108.43 cnf(959,plain, % 108.43/108.43 (P2(f19(f27(a14)),f19(f27(a11)))), % 108.43/108.43 inference(scs_inference,[],[82,34,36])). % 108.43/108.43 cnf(1899,plain, % 108.43/108.43 (P5(f10(f10(f17(a2,x18991))),f10(f10(f17(f26(a3),x18991))))), % 108.43/108.43 inference(scs_inference,[],[25,172,34,35,36,37,39])). % 108.43/108.43 cnf(1903,plain, % 108.43/108.43 (P2(f23(f19(f27(a14)),f19(f27(a14))),f23(f19(f27(a11)),f19(f27(a11))))), % 108.43/108.43 inference(scs_inference,[],[25,959,172,34,35,36,37,39,33,55])). % 108.43/108.43 cnf(1905,plain, % 108.43/108.43 (P2(f22(f19(f27(a14)),f19(f27(a14))),f22(f19(f27(a11)),f19(f27(a11))))), % 108.43/108.43 inference(scs_inference,[],[25,959,172,34,35,36,37,39,33,55,57])). % 108.43/108.43 cnf(1935,plain, % 108.43/108.43 (P2(f23(f27(f25(a14)),f27(f25(a14))),f23(f27(f25(a11)),f27(f25(a11))))), % 108.43/108.43 inference(scs_inference,[],[1903,1899,137,8,36,34,39,37,35,33,60,55])). % 108.43/108.43 cnf(1946,plain, % 108.43/108.43 (P5(f10(f10(f17(f26(a3),x19461))),f10(f10(f17(a2,x19461))))), % 108.43/108.43 inference(scs_inference,[],[1935,173,36,39])). % 108.43/108.43 cnf(1958,plain, % 108.43/108.43 (P2(f23(a11,a11),f23(a14,a14))), % 108.43/108.43 inference(scs_inference,[],[1935,1905,173,7,8,36,39,34,35,37,33,60,55])). % 108.43/108.43 cnf(1987,plain, % 108.43/108.43 (P2(f23(f23(a11,a11),f23(a11,a11)),f23(f23(a14,a14),f23(a14,a14)))), % 108.43/108.43 inference(scs_inference,[],[1958,1946,8,36,34,39,37,35,33,60,55])). % 108.43/108.43 cnf(4626,plain, % 108.43/108.43 (P2(f27(f23(f23(a11,a11),f23(a11,a11))),f27(f23(f23(a14,a14),f23(a14,a14))))), % 108.43/108.43 inference(scs_inference,[],[1987,37,33,35,36])). % 108.43/108.43 cnf(4664,plain, % 108.43/108.43 (P13(f24(f27(f23(f23(a11,a11),f23(a11,a11)))),f24(f27(f23(f23(a14,a14),f23(a14,a14)))))), % 108.43/108.43 inference(scs_inference,[],[4626,37,33])). % 108.43/108.43 cnf(4901,plain, % 108.43/108.43 (P2(f19(a11),f19(a14))), % 108.43/108.43 inference(scs_inference,[],[7,34])). % 108.43/108.43 cnf(4903,plain, % 108.43/108.43 (P2(f25(a11),f25(a14))), % 108.43/108.43 inference(scs_inference,[],[7,34,37])). % 108.43/108.43 cnf(4909,plain, % 108.43/108.43 (P2(f27(a11),f27(a14))), % 108.43/108.43 inference(scs_inference,[],[7,34,37,33,35,36])). % 108.43/108.43 cnf(4913,plain, % 108.43/108.43 (P6(f18(x49131,a11),f18(x49131,a14))), % 108.43/108.43 inference(scs_inference,[],[7,13,8,34,37,33,35,36,57,60])). % 108.43/108.43 cnf(4919,plain, % 108.43/108.43 (P2(f16(f24(a11),x49191),f16(f24(a14),x49191))), % 108.43/108.43 inference(scs_inference,[],[7,70,13,8,34,37,33,35,36,57,60,55,43,56])). % 108.43/108.43 cnf(4941,plain, % 108.43/108.43 (~P2(f16(f24(a11),a13),f16(f24(f23(a11,f27(f21(a7)))),a13))), % 108.43/108.43 inference(scs_inference,[],[4901,4903,4919,27,34,37,33,35,36,45])). % 108.43/108.43 cnf(4957,plain, % 108.43/108.43 (P5(f10(f17(f26(a3),f18(x49571,a11))),f10(f17(a2,f18(x49571,a14))))), % 108.43/108.43 inference(scs_inference,[],[4901,4903,4913,4919,4664,27,19,22,11,12,8,34,37,33,35,36,45,59,57,60,55,64,39])). % 108.43/108.43 cnf(4974,plain, % 108.43/108.43 ($false), % 108.43/108.43 inference(scs_inference,[],[4909,4957,4941,26,13,39,34,37,33,35,36,45]), % 108.43/108.43 ['proof']). % 108.43/108.43 % SZS output end Proof % 108.43/108.43 % Total time :107.790000s %------------------------------------------------------------------------------