%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN701-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 : n023.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:20 EDT 2024 % Result : Unsatisfiable 111.39s 111.36s % Output : CNFRefutation 111.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN701-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n023.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 19:18:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/0.56 start to proof:theBenchmark % 111.31/111.33 %------------------------------------------- % 111.31/111.33 % File :CSE---1.7 % 111.31/111.33 % Problem :theBenchmark % 111.31/111.33 % Transform :cnf % 111.31/111.33 % Format :tptp:raw % 111.31/111.33 % Command :java -jar mcs_scs.jar %d %s % 111.31/111.33 % 111.31/111.33 % Result :Theorem 110.730000s % 111.31/111.33 % Output :CNFRefutation 110.730000s % 111.31/111.33 %------------------------------------------- % 111.31/111.34 %-------------------------------------------------------------------------- % 111.31/111.34 % File : SYN701-1 : TPTP v8.2.0. Released v2.5.0. % 111.31/111.34 % Domain : Syntactic % 111.31/111.34 % Problem : Harrison problem 4653 % 111.36/111.34 % Version : Especial. % 111.36/111.34 % English : % 111.36/111.34 % 111.36/111.34 % Refs : [Har01] Email to G. Sutcliffe % 111.36/111.34 % Source : [Har01] % 111.36/111.34 % Names : % 111.36/111.34 % 111.36/111.34 % Status : Unsatisfiable % 111.36/111.34 % Rating : 0.00 v7.0.0, 0.25 v6.4.0, 0.12 v6.3.0, 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 % 111.36/111.34 % Syntax : Number of clauses : 74 ( 31 unt; 2 nHn; 64 RR) % 111.36/111.34 % Number of literals : 156 ( 0 equ; 83 neg) % 111.36/111.34 % Maximal clause size : 5 ( 2 avg) % 111.36/111.34 % Maximal term depth : 6 ( 1 avg) % 111.36/111.34 % Number of predicates : 18 ( 18 usr; 0 prp; 1-3 aty) % 111.36/111.34 % Number of functors : 29 ( 29 usr; 15 con; 0-2 aty) % 111.36/111.34 % Number of variables : 132 ( 5 sgn) % 111.36/111.34 % SPC : CNF_UNS_RFO_NEQ_NHN % 111.36/111.34 % 111.36/111.34 % Comments : % 111.36/111.34 %-------------------------------------------------------------------------- % 111.36/111.34 cnf(c34_is_p25_1,negated_conjecture, % 111.36/111.34 p25(c34) ). % 111.36/111.34 % 111.36/111.34 cnf(c36_is_p29_2,negated_conjecture, % 111.36/111.34 p29(c36) ). % 111.36/111.34 % 111.36/111.34 cnf(f18_is_p30_3,negated_conjecture, % 111.36/111.34 p30(f18(c41)) ). % 111.36/111.34 % 111.36/111.34 cnf(f16_is_p28_4,negated_conjecture, % 111.36/111.34 p28(f16(c38)) ). % 111.36/111.34 % 111.36/111.34 cnf(f16_is_p28_5,negated_conjecture, % 111.36/111.34 p28(f16(c39)) ). % 111.36/111.34 % 111.36/111.34 cnf(f18_is_p30_6,negated_conjecture, % 111.36/111.34 p30(f18(c40)) ). % 111.36/111.34 % 111.36/111.34 cnf(p10_7,negated_conjecture, % 111.36/111.34 p10(X5,X5) ). % 111.36/111.34 % 111.36/111.34 cnf(p7_8,negated_conjecture, % 111.36/111.34 p7(X112,X112) ). % 111.36/111.34 % 111.36/111.34 cnf(p6_9,negated_conjecture, % 111.36/111.34 p6(X109,X109) ). % 111.36/111.34 % 111.36/111.34 cnf(p3_10,negated_conjecture, % 111.36/111.34 p3(X88,X88) ). % 111.36/111.34 % 111.36/111.34 cnf(p21_11,negated_conjecture, % 111.36/111.34 p21(X68,X68) ). % 111.36/111.34 % 111.36/111.34 cnf(p2_12,negated_conjecture, % 111.36/111.34 p2(X43,X43) ). % 111.36/111.35 % 111.36/111.35 cnf(p17_13,negated_conjecture, % 111.36/111.35 p17(X28,X28) ). % 111.36/111.35 % 111.36/111.35 cnf(p14_14,negated_conjecture, % 111.36/111.35 p14(X19,X19) ). % 111.36/111.35 % 111.36/111.35 cnf(p12_15,negated_conjecture, % 111.36/111.35 p12(X12,X12) ). % 111.36/111.35 % 111.36/111.35 cnf(p2_16,negated_conjecture, % 111.36/111.35 p2(c44,c46) ). % 111.36/111.35 % 111.36/111.35 cnf(p31_17,negated_conjecture, % 111.36/111.35 p31(c47,c42) ). % 111.36/111.35 % 111.36/111.35 cnf(p31_18,negated_conjecture, % 111.36/111.35 p31(c46,f5(c42)) ). % 111.36/111.35 % 111.36/111.35 cnf(p31_19,negated_conjecture, % 111.36/111.35 p31(c44,f5(c42)) ). % 111.36/111.35 % 111.36/111.35 cnf(p7_20,negated_conjecture, % 111.36/111.35 p7(f8(c35),c36) ). % 111.36/111.35 % 111.36/111.35 cnf(p32_21,negated_conjecture, % 111.36/111.35 p32(f22(c34,c45),c48) ). % 111.36/111.35 % 111.36/111.35 cnf(p32_22,negated_conjecture, % 111.36/111.35 p32(f22(c34,c45),c43) ). % 111.36/111.35 % 111.36/111.35 cnf(p31_23,negated_conjecture, % 111.36/111.35 p31(f23(c44,f9(f20(c37))),c46) ). % 111.36/111.35 % 111.36/111.35 cnf(p26_24,negated_conjecture, % 111.36/111.35 p26(c34,f4(f5(X79)),f4(X79)) ). % 111.36/111.35 % 111.36/111.35 cnf(p25_25,negated_conjecture, % 111.36/111.35 ( p25(X71) % 111.36/111.35 | ~ p25(X72) % 111.36/111.35 | ~ p21(X72,X71) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p30_26,negated_conjecture, % 111.36/111.35 ( p30(X93) % 111.36/111.35 | ~ p30(X94) % 111.36/111.35 | ~ p17(X94,X93) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p29_27,negated_conjecture, % 111.36/111.35 ( p29(X86) % 111.36/111.35 | ~ p29(X87) % 111.36/111.35 | ~ p7(X87,X86) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p28_28,negated_conjecture, % 111.36/111.35 ( p28(X84) % 111.36/111.35 | ~ p28(X85) % 111.36/111.35 | ~ p14(X85,X84) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p14_29,negated_conjecture, % 111.36/111.35 ( p14(f16(X26),f16(X27)) % 111.36/111.35 | ~ p14(X26,X27) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p7_30,negated_conjecture, % 111.36/111.35 ( p7(f8(X115),f8(X116)) % 111.36/111.35 | ~ p6(X115,X116) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p3_31,negated_conjecture, % 111.36/111.35 ( p3(f4(X91),f4(X92)) % 111.36/111.35 | ~ p2(X91,X92) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p2_32,negated_conjecture, % 111.36/111.35 ( p2(f9(X66),f9(X67)) % 111.36/111.35 | ~ p2(X66,X67) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p2_33,negated_conjecture, % 111.36/111.35 ( p2(f5(X64),f5(X65)) % 111.36/111.35 | ~ p2(X64,X65) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p2_34,negated_conjecture, % 111.36/111.35 ( p2(f24(X62),f24(X63)) % 111.36/111.35 | ~ p2(X62,X63) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p2_35,negated_conjecture, % 111.36/111.35 ( p2(f20(X56),f20(X57)) % 111.36/111.35 | ~ p2(X56,X57) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p17_36,negated_conjecture, % 111.36/111.35 ( p17(f18(X31),f18(X32)) % 111.36/111.35 | ~ p17(X31,X32) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p10_37,negated_conjecture, % 111.36/111.35 ( p10(X6,X7) % 111.36/111.35 | ~ p10(X5,X6) % 111.36/111.35 | ~ p10(X5,X7) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p7_38,negated_conjecture, % 111.36/111.35 ( p7(X113,X114) % 111.36/111.35 | ~ p7(X112,X113) % 111.36/111.35 | ~ p7(X112,X114) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p6_39,negated_conjecture, % 111.36/111.35 ( p6(X110,X111) % 111.36/111.35 | ~ p6(X109,X110) % 111.36/111.35 | ~ p6(X109,X111) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p3_40,negated_conjecture, % 111.36/111.35 ( p3(X89,X90) % 111.36/111.35 | ~ p3(X88,X89) % 111.36/111.35 | ~ p3(X88,X90) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p21_41,negated_conjecture, % 111.36/111.35 ( p21(X69,X70) % 111.36/111.35 | ~ p21(X68,X69) % 111.36/111.35 | ~ p21(X68,X70) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p2_42,negated_conjecture, % 111.36/111.35 ( p2(X44,X45) % 111.36/111.35 | ~ p2(X43,X44) % 111.36/111.35 | ~ p2(X43,X45) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p17_43,negated_conjecture, % 111.36/111.35 ( p17(X29,X30) % 111.36/111.35 | ~ p17(X28,X29) % 111.36/111.35 | ~ p17(X28,X30) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p14_44,negated_conjecture, % 111.36/111.35 ( p14(X20,X21) % 111.36/111.35 | ~ p14(X19,X20) % 111.36/111.35 | ~ p14(X19,X21) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p12_45,negated_conjecture, % 111.36/111.35 ( p12(X13,X14) % 111.36/111.35 | ~ p12(X12,X13) % 111.36/111.35 | ~ p12(X12,X14) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p33_46,negated_conjecture, % 111.36/111.35 p33(f11(f4(f5(c42)),c45),f11(f4(c42),c45)) ). % 111.36/111.35 % 111.36/111.35 cnf(p31_47,negated_conjecture, % 111.36/111.35 ( p31(X95,f24(X95)) % 111.36/111.35 | ~ p31(X95,c44) % 111.36/111.35 | ~ p31(X95,f5(c42)) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p31_48,negated_conjecture, % 111.36/111.35 ( p31(f24(X95),f5(c42)) % 111.36/111.35 | ~ p31(X95,c44) % 111.36/111.35 | ~ p31(X95,f5(c42)) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p33_49,negated_conjecture, % 111.36/111.35 ( p33(X105,X106) % 111.36/111.35 | ~ p2(X108,X106) % 111.36/111.35 | ~ p33(X107,X108) % 111.36/111.35 | ~ p2(X107,X105) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p27_50,negated_conjecture, % 111.36/111.35 ( p27(X80,X81) % 111.36/111.35 | ~ p14(X83,X80) % 111.36/111.35 | ~ p27(X83,X82) % 111.36/111.35 | ~ p12(X82,X81) ) ). % 111.36/111.35 % 111.36/111.35 cnf(p31_51,negated_conjecture, % 111.36/111.35 ( p31(X96,X97) % 111.36/111.35 | ~ p2(X99,X97) % 111.36/111.35 | ~ p31(X98,X99) % 111.36/111.35 | ~ p2(X98,X96) ) ). % 111.36/111.35 % 111.39/111.35 cnf(p32_52,negated_conjecture, % 111.39/111.35 ( p32(X100,X101) % 111.39/111.35 | ~ p17(X103,X100) % 111.39/111.35 | ~ p32(X103,X102) % 111.39/111.35 | ~ p10(X102,X101) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_53,negated_conjecture, % 111.39/111.35 p2(f11(f4(c47),c48),f19(f11(f4(c42),c48),f9(f20(c37)))) ). % 111.39/111.35 % 111.39/111.35 cnf(p33_54,negated_conjecture, % 111.39/111.35 p33(f11(f4(c42),c45),f11(f4(f23(c42,f9(f20(c37)))),c45)) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_55,negated_conjecture, % 111.39/111.35 p2(f11(f4(f23(c44,f9(f20(c37)))),c43),f11(f4(c44),c43)) ). % 111.39/111.35 % 111.39/111.35 cnf(not_p2_56,negated_conjecture, % 111.39/111.35 ~ p2(f11(f4(c46),c43),f11(f4(f23(c44,f9(f20(c37)))),c43)) ). % 111.39/111.35 % 111.39/111.35 cnf(not_p2_57,negated_conjecture, % 111.39/111.35 ~ p2(f11(f4(f23(c47,f9(f20(c37)))),c48),f11(f4(c47),c48)) ). % 111.39/111.35 % 111.39/111.35 cnf(p10_58,negated_conjecture, % 111.39/111.35 ( p10(X0,c43) % 111.39/111.35 | ~ p31(f11(f4(f5(c42)),X0),f11(f4(c42),X0)) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p12_59,negated_conjecture, % 111.39/111.35 ( p12(f13(X15,X16),f13(X17,X18)) % 111.39/111.35 | ~ p10(X15,X17) % 111.39/111.35 | ~ p2(X16,X18) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_60,negated_conjecture, % 111.39/111.35 ( p2(f23(X58,X59),f23(X60,X61)) % 111.39/111.35 | ~ p2(X58,X60) % 111.39/111.35 | ~ p2(X59,X61) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_61,negated_conjecture, % 111.39/111.35 ( p2(f19(X52,X53),f19(X54,X55)) % 111.39/111.35 | ~ p2(X52,X54) % 111.39/111.35 | ~ p2(X53,X55) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_62,negated_conjecture, % 111.39/111.35 ( p2(f11(X46,X47),f11(X48,X49)) % 111.39/111.35 | ~ p10(X47,X49) % 111.39/111.35 | ~ p3(X46,X48) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p17_63,negated_conjecture, % 111.39/111.35 ( p17(f22(X33,X34),f22(X35,X36)) % 111.39/111.35 | ~ p10(X34,X36) % 111.39/111.35 | ~ p21(X33,X35) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p14_64,negated_conjecture, % 111.39/111.35 ( p14(f15(X22,X23),f15(X24,X25)) % 111.39/111.35 | ~ p12(X23,X25) % 111.39/111.35 | ~ p7(X22,X24) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_65,negated_conjecture, % 111.39/111.35 p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),f11(f4(c42),c43)) ). % 111.39/111.35 % 111.39/111.35 cnf(p32_66,negated_conjecture, % 111.39/111.35 ( p32(f22(c34,X104),c43) % 111.39/111.35 | ~ p33(f11(f4(f5(c42)),X104),f11(f4(c42),X104)) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_67,negated_conjecture, % 111.39/111.35 ( p2(f11(f4(X51),c48),f11(f4(c47),c48)) % 111.39/111.35 | ~ p31(X51,c42) % 111.39/111.35 | ~ p31(c47,X51) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_68,negated_conjecture, % 111.39/111.35 ( p2(f11(f4(X50),c43),f11(f4(c44),c43)) % 111.39/111.35 | ~ p31(c44,X50) % 111.39/111.35 | ~ p31(X50,f5(c42)) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p10_69,negated_conjecture, % 111.39/111.35 ( p10(X1,X2) % 111.39/111.35 | p32(f22(c34,X1),X2) % 111.39/111.35 | ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4)) ) ). % 111.39/111.35 % 111.39/111.35 cnf(not_p31_70,negated_conjecture, % 111.39/111.35 ( ~ p31(X95,c44) % 111.39/111.35 | ~ p31(X95,f5(c42)) % 111.39/111.35 | ~ p2(f11(f4(f24(X95)),c43),f11(f4(X95),c43)) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p26_71,negated_conjecture, % 111.39/111.35 ( p26(X73,X74,X75) % 111.39/111.35 | ~ p3(X78,X75) % 111.39/111.35 | ~ p3(X77,X74) % 111.39/111.35 | ~ p21(X76,X73) % 111.39/111.35 | ~ p26(X76,X77,X78) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p10_72,negated_conjecture, % 111.39/111.35 ( p10(X8,X9) % 111.39/111.35 | ~ p2(f11(f4(X10),X8),f9(c37)) % 111.39/111.35 | ~ p27(f15(c36,f13(X8,X10)),f13(X9,X11)) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p2_73,negated_conjecture, % 111.39/111.35 ( p2(X37,X38) % 111.39/111.35 | ~ p27(f15(c36,f13(X39,X37)),f13(X40,X41)) % 111.39/111.35 | ~ p27(f15(c36,f13(X42,X38)),f13(X40,X41)) ) ). % 111.39/111.35 % 111.39/111.35 cnf(p32_74,negated_conjecture, % 111.39/111.35 ( p32(f22(c34,X1),X2) % 111.39/111.35 | p31(f11(f4(X3),X2),f11(f4(X4),X2)) % 111.39/111.35 | ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4)) ) ). % 111.39/111.35 % 111.39/111.35 %-------------------------------------------------------------------------- % 111.39/111.35 %------------------------------------------- % 111.39/111.36 % Proof found % 111.39/111.36 % SZS status Theorem for theBenchmark % 111.39/111.36 % SZS output start Proof % 111.39/111.36 %ClaNum:74(EqnAxiom:0) % 111.39/111.36 %VarNum:273(SingletonVarNum:132) % 111.39/111.36 %MaxLitNum:5 % 111.39/111.36 %MaxfuncDepth:5 % 111.39/111.36 %SharedTerms:70 % 111.39/111.36 %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 70 71 72 73 74 % 111.39/111.36 %singleGoalClaCount:31 % 111.39/111.36 [1]P1(a1) % 111.39/111.36 [2]P8(a2) % 111.39/111.36 [7]P2(a11,a14) % 111.39/111.36 [8]P14(a16,a12) % 111.39/111.36 [3]P12(f9(a4)) % 111.39/111.36 [4]P12(f9(a5)) % 111.39/111.36 [5]P9(f10(a6)) % 111.39/111.36 [6]P9(f10(a8)) % 111.39/111.36 [18]P14(a11,f21(a12)) % 111.39/111.36 [19]P14(a14,f21(a12)) % 111.39/111.36 [20]P15(f28(a3),a2) % 111.39/111.36 [21]P17(f22(a1,a15),a17) % 111.39/111.36 [22]P17(f22(a1,a15),a13) % 111.39/111.36 [23]P14(f25(a11,f29(f23(a7))),a14) % 111.39/111.36 [25]P18(f18(f26(f21(a12)),a15),f18(f26(a12),a15)) % 111.39/111.36 [26]P2(f18(f26(a16),a17),f24(f18(f26(a12),a17),f29(f23(a7)))) % 111.39/111.36 [27]P2(f24(f18(f26(f21(a12)),a13),f29(f23(a7))),f18(f26(a12),a13)) % 111.39/111.36 [28]P18(f18(f26(a12),a15),f18(f26(f25(a12,f29(f23(a7)))),a15)) % 111.39/111.36 [29]P2(f18(f26(f25(a11,f29(f23(a7)))),a13),f18(f26(a11),a13)) % 111.39/111.36 [30]~P2(f18(f26(a14),a13),f18(f26(f25(a11,f29(f23(a7)))),a13)) % 111.39/111.36 [31]~P2(f18(f26(f25(a16,f29(f23(a7)))),a17),f18(f26(a16),a17)) % 111.39/111.36 [9]P3(x91,x91) % 111.39/111.36 [10]P15(x101,x101) % 111.39/111.36 [11]P16(x111,x111) % 111.39/111.36 [12]P13(x121,x121) % 111.39/111.36 [13]P7(x131,x131) % 111.39/111.36 [14]P2(x141,x141) % 111.39/111.36 [15]P4(x151,x151) % 111.39/111.36 [16]P5(x161,x161) % 111.39/111.36 [17]P6(x171,x171) % 111.39/111.36 [24]P10(a1,f26(f21(x241)),f26(x241)) % 111.39/111.36 [67]P3(x671,a13)+~P14(f18(f26(f21(a12)),x671),f18(f26(a12),x671)) % 111.39/111.36 [68]P17(f22(a1,x681),a13)+~P18(f18(f26(f21(a12)),x681),f18(f26(a12),x681)) % 111.39/111.36 [36]~P16(x361,x362)+P15(f28(x361),f28(x362)) % 111.39/111.36 [37]~P2(x371,x372)+P13(f26(x371),f26(x372)) % 111.39/111.36 [38]~P2(x381,x382)+P2(f21(x381),f21(x382)) % 111.39/111.36 [39]~P2(x391,x392)+P2(f23(x391),f23(x392)) % 111.39/111.36 [40]~P2(x401,x402)+P2(f29(x401),f29(x402)) % 111.39/111.36 [41]~P2(x411,x412)+P2(f27(x411),f27(x412)) % 111.39/111.36 [42]~P4(x421,x422)+P4(f9(x421),f9(x422)) % 111.39/111.36 [43]~P5(x431,x432)+P5(f10(x431),f10(x432)) % 111.39/111.36 [53]~P14(x531,a11)+P14(x531,f27(x531))+~P14(x531,f21(a12)) % 111.39/111.36 [54]~P14(x541,a11)+~P14(x541,f21(a12))+P14(f27(x541),f21(a12)) % 111.39/111.36 [65]~P14(x651,a12)+~P14(a16,x651)+P2(f18(f26(x651),a17),f18(f26(a16),a17)) % 111.39/111.36 [66]~P14(a11,x661)+~P14(x661,f21(a12))+P2(f18(f26(x661),a13),f18(f26(a11),a13)) % 111.39/111.36 [70]~P14(x701,a11)+~P14(x701,f21(a12))+~P2(f18(f26(f27(x701)),a13),f18(f26(x701),a13)) % 111.39/111.36 [32]~P7(x322,x321)+P1(x321)+~P1(x322) % 111.39/111.36 [33]~P15(x332,x331)+P8(x331)+~P8(x332) % 111.39/111.36 [34]~P4(x342,x341)+P12(x341)+~P12(x342) % 111.39/111.36 [35]~P5(x352,x351)+P9(x351)+~P9(x352) % 111.39/111.36 [44]~P3(x443,x441)+P3(x441,x442)+~P3(x443,x442) % 111.39/111.36 [45]~P15(x453,x451)+P15(x451,x452)+~P15(x453,x452) % 111.39/111.36 [46]~P16(x463,x461)+P16(x461,x462)+~P16(x463,x462) % 111.39/111.36 [47]~P13(x473,x471)+P13(x471,x472)+~P13(x473,x472) % 111.39/111.36 [48]~P7(x483,x481)+P7(x481,x482)+~P7(x483,x482) % 111.39/111.36 [49]~P2(x493,x491)+P2(x491,x492)+~P2(x493,x492) % 111.39/111.36 [50]~P4(x503,x501)+P4(x501,x502)+~P4(x503,x502) % 111.39/111.36 [51]~P5(x513,x511)+P5(x511,x512)+~P5(x513,x512) % 111.39/111.36 [52]~P6(x523,x521)+P6(x521,x522)+~P6(x523,x522) % 111.39/111.36 [59]~P2(x592,x594)+~P2(x591,x593)+P2(f25(x591,x592),f25(x593,x594)) % 111.39/111.36 [60]~P3(x602,x604)+~P13(x601,x603)+P2(f18(x601,x602),f18(x603,x604)) % 111.39/111.36 [61]~P2(x612,x614)+~P2(x611,x613)+P2(f24(x611,x612),f24(x613,x614)) % 111.39/111.36 [62]~P3(x622,x624)+~P7(x621,x623)+P4(f22(x621,x622),f22(x623,x624)) % 111.39/111.36 [63]~P15(x631,x633)+~P6(x632,x634)+P5(f19(x631,x632),f19(x633,x634)) % 111.39/111.36 [64]~P3(x641,x643)+~P2(x642,x644)+P6(f20(x641,x642),f20(x643,x644)) % 111.39/111.36 [71]P3(x711,x712)+P17(f22(a1,x711),x712)+~P11(f19(a2,f20(x711,x713)),f20(x712,x714)) % 111.39/111.36 [72]P3(x721,x722)+~P11(f19(a2,f20(x721,x723)),f20(x722,x724))+~P2(f18(f26(x723),x721),f29(a7)) % 111.39/111.36 [73]P17(f22(a1,x731),x732)+P14(f18(f26(x733),x732),f18(f26(x734),x732))+~P11(f19(a2,f20(x731,x733)),f20(x732,x734)) % 111.39/111.36 [74]P2(x741,x742)+~P11(f19(a2,f20(x743,x742)),f20(x744,x745))+~P11(f19(a2,f20(x746,x741)),f20(x744,x745)) % 111.39/111.36 [55]~P14(x553,x554)+P14(x551,x552)+~P2(x553,x551)+~P2(x554,x552) % 111.39/111.36 [56]~P17(x564,x563)+P17(x561,x562)+~P3(x563,x562)+~P4(x564,x561) % 111.39/111.36 [57]~P18(x573,x574)+P18(x571,x572)+~P2(x573,x571)+~P2(x574,x572) % 111.39/111.36 [58]~P11(x583,x584)+P11(x581,x582)+~P5(x583,x581)+~P6(x584,x582) % 111.39/111.36 [69]~P10(x696,x694,x695)+P10(x691,x692,x693)+~P13(x694,x692)+~P13(x695,x693)+~P7(x696,x691) % 111.39/111.36 %EqnAxiom % 111.39/111.36 % 111.39/111.36 %------------------------------------------- % 111.39/111.36 cnf(80,plain, % 111.39/111.36 (P14(a11,f27(a11))+~P14(a11,a11)), % 111.39/111.36 inference(scs_inference,[],[9,18,31,60,37,53])). % 111.39/111.36 cnf(89,plain, % 111.39/111.36 (P2(a14,a11)), % 111.39/111.36 inference(scs_inference,[],[7,14,49])). % 111.39/111.36 cnf(92,plain, % 111.39/111.36 (~P13(f26(a14),f26(f25(a11,f29(f23(a7)))))), % 111.39/111.36 inference(scs_inference,[],[7,30,9,14,49,60])). % 111.39/111.36 cnf(147,plain, % 111.39/111.36 (P2(f21(f23(a14)),f21(f23(a11)))), % 111.39/111.36 inference(scs_inference,[],[89,38,39])). % 111.39/111.36 cnf(152,plain, % 111.39/111.36 (P2(f29(f27(a14)),f29(f27(a11)))), % 111.39/111.36 inference(scs_inference,[],[89,40,41])). % 111.39/111.36 cnf(187,plain, % 111.39/111.36 (P15(a2,f28(a3))), % 111.39/111.36 inference(scs_inference,[],[20,10,45])). % 111.39/111.36 cnf(191,plain, % 111.39/111.36 (P5(f10(f19(a2,x1911)),f10(f19(f28(a3),x1911)))), % 111.39/111.36 inference(scs_inference,[],[187,17,43,63])). % 111.39/111.36 cnf(192,plain, % 111.39/111.36 (P5(f10(f19(f28(a3),x1921)),f10(f19(a2,x1921)))), % 111.39/111.36 inference(scs_inference,[],[191,16,51])). % 111.39/111.36 cnf(492,plain, % 111.39/111.36 (~P14(a11,a11)+~P2(f27(a11),x4921)+P14(a11,x4921)), % 111.39/111.36 inference(scs_inference,[],[14,80,55])). % 111.39/111.36 cnf(842,plain, % 111.39/111.36 (P2(f18(f26(a14),x8421),f18(f26(a11),x8421))), % 111.39/111.36 inference(scs_inference,[],[89,9,37,60])). % 111.39/111.36 cnf(928,plain, % 111.39/111.36 (P2(f21(f23(a11)),f21(f23(a14)))), % 111.39/111.36 inference(scs_inference,[],[7,38,39])). % 111.39/111.36 cnf(1244,plain, % 111.39/111.36 (P2(f27(f25(f21(f23(a14)),f21(f23(a14)))),f27(f25(f21(f23(a11)),f21(f23(a11)))))), % 111.39/111.36 inference(scs_inference,[],[147,41,59])). % 111.39/111.36 cnf(1772,plain, % 111.39/111.36 (P5(f10(f10(f19(a2,x17721))),f10(f10(f19(f28(a3),x17721))))), % 111.39/111.36 inference(scs_inference,[],[1244,191,38,39,40,41,43])). % 111.39/111.36 cnf(1813,plain, % 111.39/111.36 (P2(f24(f18(f26(a14),x18131),f18(f26(a14),x18131)),f24(f18(f26(a11),x18131),f18(f26(a11),x18131)))), % 111.39/111.36 inference(scs_inference,[],[1772,29,842,40,41,39,37,43,38,61])). % 111.39/111.36 cnf(1840,plain, % 111.39/111.36 (P5(f10(f10(f19(f28(a3),x18401))),f10(f10(f19(a2,x18401))))), % 111.39/111.36 inference(scs_inference,[],[1813,192,39,41,37,40,38,43])). % 111.39/111.36 cnf(1846,plain, % 111.39/111.36 (P2(f25(f21(f23(a11)),f21(f23(a11))),f25(f21(f23(a14)),f21(f23(a14))))), % 111.39/111.36 inference(scs_inference,[],[1813,928,192,9,39,41,37,40,38,43,64,61,59])). % 111.39/111.36 cnf(1864,plain, % 111.39/111.36 (P2(f24(f29(f27(a14)),f29(f27(a14))),f24(f29(f27(a11)),f29(f27(a11))))), % 111.39/111.36 inference(scs_inference,[],[1846,1840,152,37,41,40,39,43,38,61])). % 111.39/111.36 cnf(1896,plain, % 111.39/111.36 (P2(f25(a11,a11),f25(a14,a14))), % 111.39/111.36 inference(scs_inference,[],[1864,7,9,41,40,39,37,38,64,61,59])). % 111.39/111.36 cnf(1925,plain, % 111.39/111.36 (P2(f27(f25(a11,a11)),f27(f25(a14,a14)))), % 111.39/111.36 inference(scs_inference,[],[1896,40,37,41])). % 111.39/111.36 cnf(4934,plain, % 111.39/111.36 (P2(f21(f27(f25(a11,a11))),f21(f27(f25(a14,a14))))), % 111.39/111.36 inference(scs_inference,[],[1925,39,41,40,37,38])). % 111.39/111.36 cnf(4982,plain, % 111.39/111.36 (P13(f26(f21(f27(f25(a11,a11)))),f26(f21(f27(f25(a14,a14)))))), % 111.39/111.36 inference(scs_inference,[],[4934,37])). % 111.39/111.36 cnf(5007,plain, % 111.39/111.36 (P2(f21(a11),f21(a14))), % 111.39/111.36 inference(scs_inference,[],[7,37,38])). % 111.39/111.36 cnf(5009,plain, % 111.39/111.36 (P2(f23(a11),f23(a14))), % 111.39/111.36 inference(scs_inference,[],[7,37,38,39])). % 111.39/111.36 cnf(5013,plain, % 111.39/111.36 (P2(f29(a11),f29(a14))), % 111.39/111.36 inference(scs_inference,[],[7,37,38,39,41,40])). % 111.39/111.36 cnf(5015,plain, % 111.39/111.36 (P6(f20(x50151,a11),f20(x50151,a14))), % 111.39/111.36 inference(scs_inference,[],[7,9,37,38,39,41,40,64])). % 111.39/111.36 cnf(5017,plain, % 111.39/111.36 (P2(f24(a11,x50171),f24(a14,x50171))), % 111.39/111.36 inference(scs_inference,[],[7,9,14,37,38,39,41,40,64,61])). % 111.39/111.36 cnf(5032,plain, % 111.39/111.36 (~P2(f18(f26(a11),a13),f18(f26(f25(a11,f29(f23(a7)))),a13))), % 111.39/111.36 inference(scs_inference,[],[7,4982,92,30,24,12,13,9,14,37,38,39,41,40,64,61,59,69,47,60,492,49])). % 111.39/111.36 cnf(5034,plain, % 111.39/111.36 (P5(f19(f28(a3),f20(a13,a11)),f19(a2,f20(a13,a14)))), % 111.39/111.36 inference(scs_inference,[],[7,4982,92,30,20,24,12,13,9,14,37,38,39,41,40,64,61,59,69,47,60,492,49,63])). % 111.39/111.36 cnf(5045,plain, % 111.39/111.36 (P5(f10(f19(f28(a3),f20(a13,a11))),f10(f19(a2,f20(a13,a14))))), % 111.39/111.36 inference(scs_inference,[],[5007,5034,37,38,43])). % 111.39/111.36 cnf(5059,plain, % 111.39/111.36 (P5(f19(a2,f20(x50591,a11)),f19(f28(a3),f20(x50591,a14)))), % 111.39/111.36 inference(scs_inference,[],[5007,5015,5034,187,9,37,38,43,39,41,40,64,61,59,63])). % 111.39/111.36 cnf(5074,plain, % 111.39/111.36 (P5(f10(f19(a2,f20(x50741,a11))),f10(f19(f28(a3),f20(x50741,a14))))), % 111.39/111.36 inference(scs_inference,[],[5009,5013,5059,37,38,43])). % 111.39/111.36 cnf(5111,plain, % 111.39/111.36 (P13(f26(f24(a11,x51111)),f26(f24(a14,x51111)))), % 111.39/111.36 inference(scs_inference,[],[5017,37])). % 111.39/111.36 cnf(5123,plain, % 111.39/111.36 (P2(f24(f24(a11,x51231),f24(a11,x51231)),f24(f24(a14,x51231),f24(a14,x51231)))), % 111.39/111.36 inference(scs_inference,[],[5017,5045,37,38,43,39,41,40,61])). % 111.39/111.36 cnf(5153,plain, % 111.39/111.36 ($false), % 111.39/111.36 inference(scs_inference,[],[5123,5111,5074,5032,29,9,14,37,38,43,39,41,40,60,61,59,49]), % 111.39/111.36 ['proof']). % 111.39/111.36 % SZS output end Proof % 111.39/111.36 % Total time :110.730000s %------------------------------------------------------------------------------