%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN689-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 : n020.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:18 EDT 2024 % Result : Unsatisfiable 58.71s 58.77s % Output : CNFRefutation 58.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN689-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 : n020.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 23:56:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.49/0.56 start to proof:theBenchmark % 58.71/58.75 %------------------------------------------- % 58.71/58.75 % File :CSE---1.7 % 58.71/58.75 % Problem :theBenchmark % 58.71/58.75 % Transform :cnf % 58.71/58.75 % Format :tptp:raw % 58.71/58.75 % Command :java -jar mcs_scs.jar %d %s % 58.71/58.75 % 58.71/58.75 % Result :Theorem 58.160000s % 58.71/58.75 % Output :CNFRefutation 58.160000s % 58.71/58.75 %------------------------------------------- % 58.71/58.76 %-------------------------------------------------------------------------- % 58.71/58.76 % File : SYN689-1 : TPTP v8.2.0. Released v2.5.0. % 58.71/58.76 % Domain : Syntactic % 58.71/58.76 % Problem : Harrison problem 4606 % 58.71/58.76 % Version : Especial. % 58.71/58.76 % English : % 58.71/58.76 % 58.71/58.76 % Refs : [Har01] Email to G. Sutcliffe % 58.71/58.76 % Source : [Har01] % 58.71/58.76 % Names : % 58.71/58.76 % 58.71/58.76 % Status : Unsatisfiable % 58.71/58.76 % Rating : 0.00 v8.1.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.14 v3.7.0, 0.00 v2.5.0 % 58.71/58.76 % Syntax : Number of clauses : 62 ( 28 unt; 0 nHn; 55 RR) % 58.71/58.76 % Number of literals : 129 ( 0 equ; 72 neg) % 58.71/58.76 % Maximal clause size : 4 ( 2 avg) % 58.71/58.76 % Maximal term depth : 28 ( 5 avg) % 58.71/58.76 % Number of predicates : 15 ( 15 usr; 0 prp; 1-2 aty) % 58.71/58.76 % Number of functors : 30 ( 30 usr; 17 con; 0-2 aty) % 58.71/58.76 % Number of variables : 100 ( 0 sgn) % 58.71/58.76 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.71/58.76 % 58.71/58.76 % Comments : % 58.71/58.76 %-------------------------------------------------------------------------- % 58.71/58.76 cnf(c34_is_p27_1,negated_conjecture, % 58.71/58.76 p27(c34) ). % 58.71/58.76 % 58.71/58.76 cnf(c43_is_p27_2,negated_conjecture, % 58.71/58.76 p27(c43) ). % 58.71/58.76 % 58.71/58.76 cnf(c35_is_p27_3,negated_conjecture, % 58.71/58.76 p27(c35) ). % 58.71/58.76 % 58.71/58.76 cnf(c43_is_not_p23_4,negated_conjecture, % 58.71/58.76 ~ p23(c43) ). % 58.71/58.76 % 58.71/58.76 cnf(p10_5,negated_conjecture, % 58.71/58.76 p10(X0,X0) ). % 58.71/58.76 % 58.71/58.76 cnf(p9_6,negated_conjecture, % 58.71/58.76 p9(X81,X81) ). % 58.71/58.76 % 58.71/58.76 cnf(p3_7,negated_conjecture, % 58.71/58.76 p3(X74,X74) ). % 58.71/58.76 % 58.71/58.76 cnf(p21_8,negated_conjecture, % 58.71/58.76 p21(X39,X39) ). % 58.71/58.76 % 58.71/58.76 cnf(p2_9,negated_conjecture, % 58.71/58.76 p2(X26,X26) ). % 58.71/58.76 % 58.71/58.76 cnf(p18_10,negated_conjecture, % 58.71/58.76 p18(X18,X18) ). % 58.71/58.76 % 58.71/58.76 cnf(p12_11,negated_conjecture, % 58.71/58.76 p12(X11,X11) ). % 58.71/58.76 % 58.71/58.76 cnf(p22_12,negated_conjecture, % 58.71/58.76 p22(c41,c42) ). % 58.71/58.76 % 58.71/58.76 cnf(not_p24_13,negated_conjecture, % 58.71/58.76 ~ p24(c43,c46) ). % 58.71/58.76 % 58.71/58.76 cnf(not_p24_14,negated_conjecture, % 58.71/58.76 ~ p24(c43,c45) ). % 58.71/58.76 % 58.71/58.76 cnf(not_p26_15,negated_conjecture, % 58.71/58.76 ~ p26(f17(c43),c35) ). % 58.71/58.76 % 58.71/58.76 cnf(not_p25_16,negated_conjecture, % 58.71/58.76 ~ p25(f17(c43),c34) ). % 58.71/58.76 % 58.71/58.76 cnf(p27_17,negated_conjecture, % 58.71/58.76 ( p27(f17(X23)) % 58.71/58.76 | ~ p27(X23) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p28_18,negated_conjecture, % 58.71/58.76 p28(f20(f19(c43)),f19(c35)) ). % 58.71/58.76 % 58.71/58.76 cnf(p3_19,negated_conjecture, % 58.71/58.76 p3(f15(f16(c43,c36)),c44) ). % 58.71/58.76 % 58.71/58.76 cnf(p23_20,negated_conjecture, % 58.71/58.76 ( p23(X46) % 58.71/58.76 | ~ p23(X47) % 58.71/58.76 | ~ p10(X47,X46) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p27_21,negated_conjecture, % 58.71/58.76 ( p27(X64) % 58.71/58.76 | ~ p27(X65) % 58.71/58.76 | ~ p10(X65,X64) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p3_22,negated_conjecture, % 58.71/58.76 ( p3(f4(X79),f4(X80)) % 58.71/58.76 | ~ p2(X79,X80) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p10_23,negated_conjecture, % 58.71/58.76 ( p10(f11(X3),f11(X4)) % 58.71/58.76 | ~ p9(X3,X4) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p10_24,negated_conjecture, % 58.71/58.76 ( p10(f17(X9),f17(X10)) % 58.71/58.76 | ~ p10(X9,X10) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p18_25,negated_conjecture, % 58.71/58.76 ( p18(f19(X21),f19(X22)) % 58.71/58.76 | ~ p10(X21,X22) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p18_26,negated_conjecture, % 58.71/58.76 ( p18(f20(X24),f20(X25)) % 58.71/58.76 | ~ p18(X24,X25) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p2_27,negated_conjecture, % 58.71/58.76 ( p2(f5(X29),f5(X30)) % 58.71/58.76 | ~ p2(X29,X30) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p2_28,negated_conjecture, % 58.71/58.76 ( p2(f6(X31),f6(X32)) % 58.71/58.76 | ~ p2(X31,X32) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p2_29,negated_conjecture, % 58.71/58.76 ( p2(f7(X33),f7(X34)) % 58.71/58.76 | ~ p2(X33,X34) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p3_30,negated_conjecture, % 58.71/58.76 ( p3(f15(X77),f15(X78)) % 58.71/58.76 | ~ p10(X77,X78) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p18_31,negated_conjecture, % 58.71/58.76 ( p18(f19(f17(X23)),f20(f19(X23))) % 58.71/58.76 | ~ p27(X23) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p10_32,negated_conjecture, % 58.71/58.76 ( p10(X1,X2) % 58.71/58.76 | ~ p10(X0,X1) % 58.71/58.76 | ~ p10(X0,X2) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p9_33,negated_conjecture, % 58.71/58.76 ( p9(X82,X83) % 58.71/58.76 | ~ p9(X81,X82) % 58.71/58.76 | ~ p9(X81,X83) ) ). % 58.71/58.76 % 58.71/58.76 cnf(p3_34,negated_conjecture, % 58.71/58.77 ( p3(X75,X76) % 58.71/58.77 | ~ p3(X74,X75) % 58.71/58.77 | ~ p3(X74,X76) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p21_35,negated_conjecture, % 58.71/58.77 ( p21(X40,X41) % 58.71/58.77 | ~ p21(X39,X40) % 58.71/58.77 | ~ p21(X39,X41) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p2_36,negated_conjecture, % 58.71/58.77 ( p2(X27,X28) % 58.71/58.77 | ~ p2(X26,X27) % 58.71/58.77 | ~ p2(X26,X28) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p18_37,negated_conjecture, % 58.71/58.77 ( p18(X19,X20) % 58.71/58.77 | ~ p18(X18,X19) % 58.71/58.77 | ~ p18(X18,X20) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p12_38,negated_conjecture, % 58.71/58.77 ( p12(X12,X13) % 58.71/58.77 | ~ p12(X11,X12) % 58.71/58.77 | ~ p12(X11,X13) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p3_39,negated_conjecture, % 58.71/58.77 p3(c30,f4(f5(f6(f6(f6(f6(f6(f7(c31))))))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p25_40,negated_conjecture, % 58.71/58.77 ( p25(X56,X57) % 58.71/58.77 | ~ p27(X56) % 58.71/58.77 | ~ p27(X57) % 58.71/58.77 | ~ p29(f19(X56),f19(X57)) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p26_41,negated_conjecture, % 58.71/58.77 ( p26(X62,X63) % 58.71/58.77 | ~ p27(X62) % 58.71/58.77 | ~ p27(X63) % 58.71/58.77 | ~ p28(f19(X62),f19(X63)) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p22_42,negated_conjecture, % 58.71/58.77 ( p22(X42,X43) % 58.71/58.77 | ~ p21(X45,X43) % 58.71/58.77 | ~ p22(X44,X45) % 58.71/58.77 | ~ p21(X44,X42) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p29_43,negated_conjecture, % 58.71/58.77 ( p29(X70,X71) % 58.71/58.77 | ~ p18(X73,X71) % 58.71/58.77 | ~ p29(X72,X73) % 58.71/58.77 | ~ p18(X72,X70) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p28_44,negated_conjecture, % 58.71/58.77 ( p28(X66,X67) % 58.71/58.77 | ~ p18(X69,X67) % 58.71/58.77 | ~ p28(X68,X69) % 58.71/58.77 | ~ p18(X68,X66) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p26_45,negated_conjecture, % 58.71/58.77 ( p26(X58,X59) % 58.71/58.77 | ~ p10(X61,X59) % 58.71/58.77 | ~ p26(X60,X61) % 58.71/58.77 | ~ p10(X60,X58) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p25_46,negated_conjecture, % 58.71/58.77 ( p25(X52,X53) % 58.71/58.77 | ~ p10(X55,X53) % 58.71/58.77 | ~ p25(X54,X55) % 58.71/58.77 | ~ p10(X54,X52) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p24_47,negated_conjecture, % 58.71/58.77 ( p24(X48,X49) % 58.71/58.77 | ~ p10(X51,X49) % 58.71/58.77 | ~ p24(X50,X51) % 58.71/58.77 | ~ p10(X50,X48) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p29_48,negated_conjecture, % 58.71/58.77 ( p29(f19(X56),f19(X57)) % 58.71/58.77 | ~ p27(X57) % 58.71/58.77 | ~ p27(X56) % 58.71/58.77 | ~ p25(X56,X57) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p28_49,negated_conjecture, % 58.71/58.77 ( p28(f19(X62),f19(X63)) % 58.71/58.77 | ~ p27(X63) % 58.71/58.77 | ~ p27(X62) % 58.71/58.77 | ~ p26(X62,X63) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p9_50,negated_conjecture, % 58.71/58.77 ( p9(f13(X84,X85),f13(X86,X87)) % 58.71/58.77 | ~ p12(X85,X87) % 58.71/58.77 | ~ p2(X84,X86) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_51,negated_conjecture, % 58.71/58.77 ( p10(f16(X5,X6),f16(X7,X8)) % 58.71/58.77 | ~ p10(X5,X7) % 58.71/58.77 | ~ p10(X6,X8) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p12_52,negated_conjecture, % 58.71/58.77 ( p12(f14(X14,X15),f14(X16,X17)) % 58.71/58.77 | ~ p2(X14,X16) % 58.71/58.77 | ~ p2(X15,X17) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p2_53,negated_conjecture, % 58.71/58.77 ( p2(f8(X35,X36),f8(X37,X38)) % 58.71/58.77 | ~ p2(X36,X38) % 58.71/58.77 | ~ p2(X35,X37) ) ). % 58.71/58.77 % 58.71/58.77 cnf(p3_54,negated_conjecture, % 58.71/58.77 p3(c32,f4(f8(f5(f6(f7(c31))),f5(f7(f6(f6(f7(c31)))))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_55,negated_conjecture, % 58.71/58.77 p10(c33,f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_56,negated_conjecture, % 58.71/58.77 p10(c35,f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_57,negated_conjecture, % 58.71/58.77 p10(c39,f11(f13(f5(c31),f14(f5(f6(f7(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f6(f6(f6(f7(c31)))))))))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_58,negated_conjecture, % 58.71/58.77 p10(c40,f11(f13(f5(c31),f14(f5(f6(f6(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(c31))))))))))))))))))))))))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_59,negated_conjecture, % 58.71/58.77 p10(c37,f11(f13(f5(c31),f14(f5(f7(f6(f6(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f6(f6(f6(f6(f6(f6(f6(f7(f6(f6(f7(f7(f7(f6(f7(f6(f6(f6(f7(f7(c31))))))))))))))))))))))))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_60,negated_conjecture, % 58.71/58.77 p10(c38,f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f7(f7(f7(f7(f6(f7(f7(f7(f7(f7(f7(f7(c31))))))))))))))))))))))))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_61,negated_conjecture, % 58.71/58.77 p10(c36,f11(f13(f5(c31),f14(f5(f6(f6(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f7(f7(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f6(f7(f6(f7(f6(f6(f6(f7(f7(f7(c31))))))))))))))))))))))))))) ). % 58.71/58.77 % 58.71/58.77 cnf(p10_62,negated_conjecture, % 58.71/58.77 p10(c34,f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f6(f7(f6(f7(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f7(f6(f6(f6(f7(f7(f7(f6(f7(c31)))))))))))))))))))))))))))) ). % 58.71/58.77 % 58.71/58.77 %-------------------------------------------------------------------------- % 58.71/58.77 %------------------------------------------- % 58.71/58.77 % Proof found % 58.71/58.77 % SZS status Theorem for theBenchmark % 58.71/58.77 % SZS output start Proof % 58.71/58.77 %ClaNum:62(EqnAxiom:0) % 58.71/58.77 %VarNum:209(SingletonVarNum:100) % 58.71/58.77 %MaxLitNum:4 % 58.71/58.77 %MaxfuncDepth:27 % 58.71/58.77 %SharedTerms:166 % 58.71/58.77 %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 % 58.71/58.77 %singleGoalClaCount:28 % 58.71/58.77 [1]P1(a1) % 58.71/58.77 [2]P1(a6) % 58.71/58.77 [3]P1(a7) % 58.71/58.77 [4]P2(a8,a14) % 58.71/58.77 [24]~P8(a6) % 58.71/58.77 [25]~P9(a6,a22) % 58.71/58.77 [26]~P9(a6,a23) % 58.71/58.77 [27]~P10(f24(a6),a7) % 58.71/58.77 [28]~P11(f24(a6),a1) % 58.71/58.77 [12]P14(f25(f15(a6)),f15(a7)) % 58.71/58.77 [13]P13(f17(f16(a6,a9)),a18) % 58.71/58.77 [16]P3(a7,f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3))))) % 58.71/58.77 [17]P3(a5,f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3))))) % 58.71/58.77 [14]P13(a2,f29(f30(f28(f27(f26(a3))),f28(f26(f27(f27(f26(a3)))))))) % 58.71/58.77 [15]P13(a4,f29(f28(f27(f27(f27(f27(f27(f26(a3))))))))) % 58.71/58.77 [18]P3(a10,f21(f20(f28(a3),f19(f28(f27(f26(f26(f26(f26(f26(f26(a3)))))))),f28(f27(f27(f26(f27(f27(f27(f26(a3)))))))))))) % 58.71/58.77 [19]P3(a13,f21(f20(f28(a3),f19(f28(f27(f27(f26(f26(f26(f26(f26(a3)))))))),f28(f27(f27(f26(f26(f27(f26(f26(f26(f27(f26(f27(f26(f27(f26(f27(f26(f27(f26(f27(f26(f27(f26(a3))))))))))))))))))))))))))) % 58.71/58.77 [20]P3(a11,f21(f20(f28(a3),f19(f28(f26(f27(f27(f26(f26(f26(f26(a3)))))))),f28(f27(f27(f27(f27(f27(f27(f27(f27(f27(f26(f27(f27(f26(f26(f26(f27(f26(f27(f27(f27(f26(f26(a3))))))))))))))))))))))))))) % 58.71/58.77 [21]P3(a12,f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(f27(f26(f26(f26(f27(f27(f27(f26(f27(f26(f26(f26(f26(f26(f27(f26(f26(f26(f26(f26(f26(f26(a3))))))))))))))))))))))))))) % 58.71/58.77 [22]P3(a9,f21(f20(f28(a3),f19(f28(f27(f27(f26(f27(f27(f27(f27(f26(a3))))))))),f28(f26(f26(f27(f26(f26(f26(f27(f27(f27(f26(f27(f26(f27(f26(f27(f26(f27(f27(f27(f26(f26(f26(a3))))))))))))))))))))))))))) % 58.71/58.77 [23]P3(a1,f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f27(f27(f26(a3))))))))),f28(f27(f26(f27(f26(f26(f26(f27(f26(f26(f26(f27(f26(f27(f26(f26(f27(f27(f27(f26(f26(f26(f27(f26(a3)))))))))))))))))))))))))))) % 58.71/58.77 [5]P3(x51,x51) % 58.71/58.77 [6]P12(x61,x61) % 58.71/58.77 [7]P13(x71,x71) % 58.71/58.77 [8]P4(x81,x81) % 58.71/58.77 [9]P5(x91,x91) % 58.71/58.77 [10]P6(x101,x101) % 58.71/58.77 [11]P7(x111,x111) % 58.71/58.77 [29]~P1(x291)+P1(f24(x291)) % 58.71/58.77 [41]~P1(x411)+P6(f15(f24(x411)),f25(f15(x411))) % 58.71/58.77 [32]~P3(x321,x322)+P3(f24(x321),f24(x322)) % 58.71/58.77 [33]~P12(x331,x332)+P3(f21(x331),f21(x332)) % 58.71/58.77 [34]~P3(x341,x342)+P13(f17(x341),f17(x342)) % 58.71/58.77 [35]~P5(x351,x352)+P13(f29(x351),f29(x352)) % 58.71/58.77 [36]~P5(x361,x362)+P5(f28(x361),f28(x362)) % 58.71/58.77 [37]~P5(x371,x372)+P5(f27(x371),f27(x372)) % 58.71/58.77 [38]~P5(x381,x382)+P5(f26(x381),f26(x382)) % 58.71/58.77 [39]~P3(x391,x392)+P6(f15(x391),f15(x392)) % 58.71/58.77 [40]~P6(x401,x402)+P6(f25(x401),f25(x402)) % 58.71/58.77 [30]~P3(x302,x301)+P1(x301)+~P1(x302) % 58.71/58.77 [31]~P3(x312,x311)+P8(x311)+~P8(x312) % 58.71/58.77 [42]~P3(x423,x421)+P3(x421,x422)+~P3(x423,x422) % 58.71/58.77 [43]~P12(x433,x431)+P12(x431,x432)+~P12(x433,x432) % 58.71/58.77 [44]~P13(x443,x441)+P13(x441,x442)+~P13(x443,x442) % 58.71/58.77 [45]~P4(x453,x451)+P4(x451,x452)+~P4(x453,x452) % 58.71/58.77 [46]~P5(x463,x461)+P5(x461,x462)+~P5(x463,x462) % 58.71/58.77 [47]~P6(x473,x471)+P6(x471,x472)+~P6(x473,x472) % 58.71/58.77 [48]~P7(x483,x481)+P7(x481,x482)+~P7(x483,x482) % 58.71/58.77 [59]~P3(x592,x594)+~P3(x591,x593)+P3(f16(x591,x592),f16(x593,x594)) % 58.71/58.77 [60]~P5(x601,x603)+~P7(x602,x604)+P12(f20(x601,x602),f20(x603,x604)) % 58.71/58.77 [61]~P5(x612,x614)+~P5(x611,x613)+P5(f30(x611,x612),f30(x613,x614)) % 58.71/58.77 [62]~P5(x622,x624)+~P5(x621,x623)+P7(f19(x621,x622),f19(x623,x624)) % 58.71/58.77 [49]~P1(x492)+~P1(x491)+~P10(x491,x492)+P14(f15(x491),f15(x492)) % 58.71/58.77 [50]~P1(x502)+~P1(x501)+~P11(x501,x502)+P15(f15(x501),f15(x502)) % 58.71/58.77 [51]~P1(x512)+~P1(x511)+P10(x511,x512)+~P14(f15(x511),f15(x512)) % 58.71/58.77 [52]~P1(x522)+~P1(x521)+P11(x521,x522)+~P15(f15(x521),f15(x522)) % 58.71/58.77 [53]~P2(x533,x534)+P2(x531,x532)+~P4(x533,x531)+~P4(x534,x532) % 58.71/58.77 [54]~P9(x543,x544)+P9(x541,x542)+~P3(x543,x541)+~P3(x544,x542) % 58.71/58.77 [55]~P10(x553,x554)+P10(x551,x552)+~P3(x553,x551)+~P3(x554,x552) % 58.71/58.77 [56]~P11(x563,x564)+P11(x561,x562)+~P3(x563,x561)+~P3(x564,x562) % 58.71/58.77 [57]~P14(x573,x574)+P14(x571,x572)+~P6(x573,x571)+~P6(x574,x572) % 58.71/58.77 [58]~P15(x583,x584)+P15(x581,x582)+~P6(x583,x581)+~P6(x584,x582) % 58.71/58.77 %EqnAxiom % 58.71/58.77 % 58.71/58.77 %------------------------------------------- % 58.71/58.77 cnf(66,plain, % 58.71/58.77 (P3(f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3)))),a7)), % 58.71/58.77 inference(scs_inference,[],[16,5,42])). % 58.71/58.77 cnf(74,plain, % 58.71/58.77 (~P10(f24(a6),f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3)))))), % 58.71/58.77 inference(scs_inference,[],[66,27,5,55])). % 58.71/58.77 cnf(111,plain, % 58.71/58.77 (P1(f24(a6))), % 58.71/58.77 inference(scs_inference,[],[2,5,29,30])). % 58.71/58.77 cnf(191,plain, % 58.71/58.77 (P3(f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3)))),a5)), % 58.71/58.77 inference(scs_inference,[],[17,5,42])). % 58.71/58.77 cnf(192,plain, % 58.71/58.77 (P3(x1921,x1921)), % 58.71/58.77 inference(rename_variables,[],[5])). % 58.71/58.77 cnf(196,plain, % 58.71/58.77 (~P6(f15(a7),x1961)+P14(f25(f15(a6)),x1961)), % 58.71/58.77 inference(scs_inference,[],[17,5,192,10,12,42,55,57])). % 58.71/58.77 cnf(355,plain, % 58.71/58.77 (P3(f16(f24(f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3))))),f24(f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3)))))),f16(f24(a7),f24(a7)))), % 58.71/58.77 inference(scs_inference,[],[66,59,32])). % 58.71/58.77 cnf(572,plain, % 58.71/58.77 (P1(f24(a1))), % 58.71/58.77 inference(scs_inference,[],[1,5,29,30])). % 58.71/58.77 cnf(738,plain, % 58.71/58.77 (P3(f24(f16(f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3)))),f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3)))))),f24(f16(a7,a7)))), % 58.71/58.77 inference(scs_inference,[],[66,32,59])). % 58.71/58.77 cnf(770,plain, % 58.71/58.77 (P6(f25(f15(f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3)))))),f25(f15(a7)))), % 58.71/58.77 inference(scs_inference,[],[66,39,40])). % 58.71/58.77 cnf(862,plain, % 58.71/58.77 (P14(f25(f15(a6)),f15(f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3))))))), % 58.71/58.77 inference(scs_inference,[],[16,39,196])). % 58.71/58.77 cnf(2016,plain, % 58.71/58.77 (P1(f24(f24(a1)))), % 58.71/58.77 inference(scs_inference,[],[572,29])). % 58.71/58.77 cnf(2026,plain, % 58.71/58.77 (P6(f15(f24(a6)),f25(f15(a6)))), % 58.71/58.77 inference(scs_inference,[],[2,770,572,738,29,32,34,39,40,41])). % 58.71/58.77 cnf(2028,plain, % 58.71/58.77 (P1(f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3)))))), % 58.71/58.77 inference(scs_inference,[],[2,770,572,738,3,16,29,32,34,39,40,41,30])). % 58.71/58.77 cnf(2030,plain, % 58.71/58.77 (P3(f16(f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3)))),f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3))))),f16(a5,a5))), % 58.71/58.77 inference(scs_inference,[],[2,770,572,738,191,3,16,29,32,34,39,40,41,30,59])). % 58.71/58.77 cnf(2091,plain, % 58.71/58.77 (P1(f24(f24(f24(a1))))), % 58.71/58.77 inference(scs_inference,[],[2016,41,29])). % 58.71/58.77 cnf(2099,plain, % 58.71/58.77 (P6(f25(f15(f24(a6))),f25(f25(f15(a6))))), % 58.71/58.77 inference(scs_inference,[],[2016,2026,2030,355,41,29,34,39,32,40])). % 58.71/58.77 cnf(2101,plain, % 58.71/58.77 (P3(f16(f16(f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3)))),f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3))))),f16(f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3)))),f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3)))))),f16(f16(a5,a5),f16(a5,a5)))), % 58.71/58.77 inference(scs_inference,[],[2016,2026,2030,355,41,29,34,39,32,40,59])). % 58.71/58.77 cnf(2111,plain, % 58.71/58.77 (P6(f25(f25(f15(f24(a6)))),f25(f25(f25(f15(a6)))))), % 58.71/58.77 inference(scs_inference,[],[2091,2099,2101,41,34,40])). % 58.71/58.77 cnf(2113,plain, % 58.71/58.77 (P1(f24(f24(f24(f24(a1)))))), % 58.71/58.77 inference(scs_inference,[],[2091,2099,2101,41,34,40,29])). % 58.71/58.77 cnf(2119,plain, % 58.71/58.77 (P3(f16(a5,a5),f16(f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3)))),f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3))))))), % 58.71/58.77 inference(scs_inference,[],[2091,2099,2101,17,41,34,40,29,39,32,59])). % 58.71/58.77 cnf(2142,plain, % 58.71/58.77 (P6(x21421,x21421)), % 58.71/58.77 inference(rename_variables,[],[10])). % 58.71/58.77 cnf(2144,plain, % 58.71/58.77 ($false), % 58.71/58.77 inference(scs_inference,[],[2113,2111,74,2119,2028,862,2026,191,111,16,10,2142,41,40,34,29,32,39,59,51,57,47]), % 58.71/58.77 ['proof']). % 58.71/58.77 % SZS output end Proof % 58.71/58.77 % Total time :58.160000s %------------------------------------------------------------------------------