%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW473+1 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n011.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 : Tue May 12 07:16:55 PM UTC 2026 % Result : Theorem 1.45s 2.42s % Output : Proof 1.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SWW473+1 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.17/0.34 % Computer : n011.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Mon May 11 14:32:48 EDT 2026 % 0.17/0.35 % CPUTime : % 1.45/2.42 % SZS status Theorem % 1.45/2.42 % SZS output start Proof % 1.45/2.42 % 1.45/2.42 =============================================================== % 1.45/2.42 TPTP Problem: conj_6 (conjecture with 448 axiom(s)) % 1.45/2.42 Axioms: [gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000t__a,gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Opname,gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_It__a_Mtc__HOL__Obool,gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Com__Opname_Mtc_,gsy_c_COMBS_000t__a_000tc__HOL__Obool_000tc__HOL__Obool,gsy_c_COMBS_000tc__Com__Opname_000tc__HOL__Obool_000tc__HOL__Obool,gsy_c_COMBS_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool_000tc__HOL__Obo,gsy_c_COMBS_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__Obool_000t,gsy_c_Finite__Set_Ofinite_000t__a,gsy_c_Finite__Set_Ofinite_000tc__Com__Opname,gsy_c_HOL_Oundefined_000t__a,gsy_c_HOL_Oundefined_000tc__Com__Opname,gsy_c_HOL_Oundefined_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_HOL_Oundefined_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,gsy_c_HOL_Oundefined_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool,gsy_c_HOL_Oundefined_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc_,gsy_c_Set_OCollect_000t__a,gsy_c_Set_OCollect_000tc__Com__Opname,gsy_c_Set_OCollect_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_Set_OCollect_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,gsy_c_Set_Oimage_000t__a_000t__a,gsy_c_Set_Oimage_000t__a_000tc__Com__Opname,gsy_c_Set_Oimage_000tc__Com__Opname_000t__a,gsy_c_Set_Oimage_000tc__Com__Opname_000tc__Com__Opname,gsy_c_Set_Oimage_000tc__Com__Opname_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_Set_Oimage_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_,gsy_c_Set_Oimage_000tc__Nat__Onat_000t__a,gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__Com__Opname,gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,gsy_c_Set_Oimage_000tc__fun_It__a_Mtc__HOL__Obool_J_000t__a,gsy_c_Set_Oimage_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opname,gsy_c_Set_Oimage_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000t__a,gsy_c_Set_Oimage_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__Com__Opnam,gsy_c_Set_Oimage_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000t__a,gsy_c_Set_Oimage_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__Com__Opname,gsy_c_Set_Oimage_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_0,gsy_c_Set_Oimage_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_0_001,gsy_c_Set_Oimage_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL,gsy_c_Set_Oimage_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL_002,gsy_c_Set_Oimage_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HOL__,gsy_c_Set_Oimage_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HOL___003,gsy_c_Set_Oinsert_000t__a,gsy_c_Set_Oinsert_000tc__Com__Opname,gsy_c_Set_Oinsert_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_Set_Oinsert_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,gsy_c_hAPP_000t__a_000tc__HOL__Obool,gsy_c_hAPP_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_hAPP_000t__a_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,gsy_c_hAPP_000t__a_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J,gsy_c_hAPP_000tc__Com__Opname_000t__a,gsy_c_hAPP_000tc__Com__Opname_000tc__HOL__Obool,gsy_c_hAPP_000tc__Com__Opname_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_hAPP_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,gsy_c_hAPP_000tc__Com__Opname_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obo,gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool,gsy_c_hAPP_000tc__Nat__Onat_000tc__HOL__Obool,gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool,gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__a_Mtc__HOL,gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__Obool,gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_Itc__Com__Op,gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_Itc,gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obool,gsy_c_hAPP_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_000tc__,gsy_c_hAPP_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_000tc___004,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL__Oboo,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL__Oboo_005,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HOL__Obool_,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HO,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HO,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Oboo,gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_,gsy_v_G,gsy_v_P,gsy_v_U,gsy_v_pn,fact_0_assms_I1_J,fact_1_finite__Collect__subsets,fact_2_finite__Collect__subsets,fact_3_finite__Collect__subsets,fact_4_finite__Collect__subsets,fact_5_finite__Collect__subsets,fact_6_finite__Collect__subsets,fact_7_finite__Collect__subsets,fact_8_finite__Collect__subsets,fact_9_finite__Collect__subsets,fact_10_finite__imageI,fact_11_finite__imageI,fact_12_finite__imageI,fact_13_finite__imageI,fact_14_finite__imageI,fact_15_finite__imageI,fact_16_finite__imageI,fact_17_finite__imageI,fact_18_finite__imageI,fact_19_finite__imageI,fact_20_finite__imageI,fact_21_finite__imageI,fact_22_finite__imageI,fact_23_finite__imageI,fact_24_finite__imageI,fact_25_finite__imageI,fact_26_finite__imageI,fact_27_finite__imageI,fact_28_finite__imageI,fact_29_finite__imageI,fact_30_finite__imageI,fact_31_finite__imageI,fact_32_finite__imageI,fact_33_finite__imageI,fact_34_finite__imageI,fact_35_finite__imageI,fact_36_finite__imageI,fact_37_finite__imageI,fact_38_finite__imageI,fact_39_finite__imageI,fact_40_finite__imageI,fact_41_finite__imageI,fact_42_finite__imageI,fact_43_finite__imageI,fact_44_finite__imageI,fact_45_finite_OinsertI,fact_46_finite_OinsertI,fact_47_finite_OinsertI,fact_48_finite_OinsertI,fact_49_finite_OinsertI,fact_50_finite_OinsertI,fact_51_finite_OinsertI,fact_52_finite_OinsertI,fact_53_finite_OinsertI,fact_54_card__image__le,fact_55_card__image__le,fact_56_card__image__le,fact_57_card__image__le,fact_58_card__image__le,fact_59_card__image__le,fact_60_card__image__le,fact_61_card__image__le,fact_62_card__image__le,fact_63_card__image__le,fact_64_card__image__le,fact_65_card__image__le,fact_66_card__image__le,fact_67_card__image__le,fact_68_card__image__le,fact_69_card__image__le,fact_70_card__image__le,fact_71_card__image__le,fact_72_card__image__le,fact_73_card__image__le,fact_74_card__image__le,fact_75_card__image__le,fact_76_card__image__le,fact_77_card__image__le,fact_78_card__image__le,fact_79_card__image__le,fact_80_card__mono,fact_81_card__mono,fact_82_card__mono,fact_83_card__mono,fact_84_card__mono,fact_85_card__mono,fact_86_card__seteq,fact_87_card__seteq,fact_88_card__seteq,fact_89_card__seteq,fact_90_card__seteq,fact_91_card__seteq,fact_92_card__insert__le,fact_93_card__insert__le,fact_94_card__insert__le,fact_95_card__insert__le,fact_96_card__insert__le,fact_97_card__insert__le,fact_98_card__insert__if,fact_99_card__insert__if,fact_100_card__insert__if,fact_101_card__insert__if,fact_102_card__insert__if,fact_103_card__insert__if,fact_104_card__insert__disjoint,fact_105_card__insert__disjoint,fact_106_card__insert__disjoint,fact_107_card__insert__disjoint,fact_108_card__insert__disjoint,fact_109_card__insert__disjoint,fact_110_finite__Collect__conjI,fact_111_finite__Collect__conjI,fact_112_finite__Collect__conjI,fact_113_finite__Collect__conjI,fact_114_finite__Collect__conjI,fact_115_finite__Collect__conjI,fact_116_Suc__diff__le,fact_117_finite__Collect__le__nat,fact_118_card__Collect__le__nat,fact_119_Suc__inject,fact_120_nat_Oinject,fact_121_Suc__n__not__n,fact_122_n__not__Suc__n,fact_123_le__antisym,fact_124_le__trans,fact_125_eq__imp__le,fact_126_nat__le__linear,fact_127_le__refl,fact_128_diff__commute,fact_129_finite__Collect__disjI,fact_130_finite__Collect__disjI,fact_131_finite__Collect__disjI,fact_132_finite__Collect__disjI,fact_133_finite__Collect__disjI,fact_134_finite__Collect__disjI,fact_135_finite__insert,fact_136_finite__insert,fact_137_finite__insert,fact_138_finite__insert,fact_139_finite__insert,fact_140_finite__insert,fact_141_finite__subset,fact_142_finite__subset,fact_143_finite__subset,fact_144_finite__subset,fact_145_finite__subset,fact_146_finite__subset,fact_147_rev__finite__subset,fact_148_rev__finite__subset,fact_149_rev__finite__subset,fact_150_rev__finite__subset,fact_151_rev__finite__subset,fact_152_rev__finite__subset,fact_153_Suc__leD,fact_154_le__SucE,fact_155_le__SucI,fact_156_Suc__le__mono,fact_157_le__Suc__eq,fact_158_not__less__eq__eq,fact_159_Suc__n__not__le__n,fact_160_Suc__diff__diff,fact_161_diff__Suc__Suc,fact_162_le__diff__iff,fact_163_Nat_Odiff__diff__eq,fact_164_eq__diff__iff,fact_165_diff__diff__cancel,fact_166_diff__le__mono,fact_167_diff__le__mono2,fact_168_diff__le__self,fact_169_finite__surj,fact_170_finite__subset__image,fact_171_lift__Suc__mono__le,fact_172_lift__Suc__mono__le,fact_173_lift__Suc__mono__le,fact_174_lift__Suc__mono__le,fact_175_pigeonhole__infinite,fact_176_image__eqI,fact_177_equalityI,fact_178_equalityI,fact_179_equalityI,fact_180_subsetD,fact_181_subsetD,fact_182_subsetD,fact_183_insertCI,fact_184_insertCI,fact_185_insertCI,fact_186_insertE,fact_187_insertE,fact_188_insertE,fact_189_insertI1,fact_190_insertI1,fact_191_insertI1,fact_192_insert__compr,fact_193_insert__compr,fact_194_insert__compr,fact_195_insert__compr,fact_196_insert__compr,fact_197_insert__compr,fact_198_insert__Collect,fact_199_insert__Collect,fact_200_insert__Collect,fact_201_insert__Collect,fact_202_insert__Collect,fact_203_insert__Collect,fact_204_insert__absorb2,fact_205_insert__absorb2,fact_206_insert__absorb2,fact_207_insert__commute,fact_208_insert__commute,fact_209_insert__commute,fact_210_insert__iff,fact_211_insert__iff,fact_212_insert__iff,fact_213_insert__code,fact_214_insert__code,fact_215_insert__code,fact_216_insert__ident,fact_217_insert__ident,fact_218_insert__ident,fact_219_insertI2,fact_220_insertI2,fact_221_insertI2,fact_222_insert__absorb,fact_223_insert__absorb,fact_224_insert__absorb,fact_225_subset__refl,fact_226_subset__refl,fact_227_subset__refl,fact_228_set__eq__subset,fact_229_set__eq__subset,fact_230_set__eq__subset,fact_231_equalityD1,fact_232_equalityD1,fact_233_equalityD1,fact_234_equalityD2,fact_235_equalityD2,fact_236_equalityD2,fact_237_in__mono,fact_238_in__mono,fact_239_in__mono,fact_240_set__rev__mp,fact_241_set__rev__mp,fact_242_set__rev__mp,fact_243_set__mp,fact_244_set__mp,fact_245_set__mp,fact_246_subset__trans,fact_247_subset__trans,fact_248_subset__trans,fact_249_equalityE,fact_250_equalityE,fact_251_equalityE,fact_252_mem__def,fact_253_mem__def,fact_254_mem__def,fact_255_Collect__def,fact_256_Collect__def,fact_257_Collect__def,fact_258_Collect__def,fact_259_Collect__def,fact_260_image__iff,fact_261_imageI,fact_262_rev__image__eqI,fact_263_insert__compr__raw,fact_264_insert__compr__raw,fact_265_insert__compr__raw,fact_266_insert__compr__raw,fact_267_insert__compr__raw,fact_268_insert__compr__raw,fact_269_subset__insertI,fact_270_subset__insertI,fact_271_subset__insertI,fact_272_insert__subset,fact_273_insert__subset,fact_274_insert__subset,fact_275_subset__insert,fact_276_subset__insert,fact_277_subset__insert,fact_278_subset__insertI2,fact_279_subset__insertI2,fact_280_subset__insertI2,fact_281_insert__mono,fact_282_insert__mono,fact_283_insert__mono,fact_284_image__insert,fact_285_insert__image,fact_286_subset__image__iff,fact_287_image__mono,fact_288_imageE,fact_289_subsetI,fact_290_subsetI,fact_291_subsetI,fact_292_zero__induct__lemma,fact_293_Suc__le__D,fact_294_image__subsetI,fact_295_order__refl,fact_296_order__refl,fact_297_order__refl,fact_298_order__refl,fact_299_finite__nat__set__iff__bounded__le,help_fNot_1_1_U,help_fNot_2_1_U,help_fconj_1_1_U,help_fconj_2_1_U,help_fconj_3_1_U,help_fdisj_1_1_U,help_fdisj_2_1_U,help_fdisj_3_1_U,help_fimplies_1_1_U,help_fimplies_2_1_U,help_fimplies_3_1_U,help_fequal_1_1_fequal_000t__a_T,help_fequal_2_1_fequal_000t__a_T,help_fequal_1_1_fequal_000tc__Nat__Onat_T,help_fequal_2_1_fequal_000tc__Nat__Onat_T,help_fequal_1_1_fequal_000tc__Com__Opname_T,help_fequal_2_1_fequal_000tc__Com__Opname_T,help_COMBC_1_1_COMBC_000t__a_000t__a_000tc__HOL__Obool_U,help_fequal_1_1_fequal_000tc__fun_It__a_Mtc__HOL__Obool_J_T,help_fequal_2_1_fequal_000tc__fun_It__a_Mtc__HOL__Obool_J_T,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000t__a_U,help_COMBS_1_1_COMBS_000t__a_000tc__HOL__Obool_000tc__HOL__Obool_U,help_COMBC_1_1_COMBC_000tc__Com__Opname_000t__a_000tc__HOL__Obool_U,help_fequal_1_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T,help_fequal_2_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T,help_fequal_1_1_fequal_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_T,help_fequal_2_1_fequal_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_T,help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__Nat__Onat_000tc__HOL__Obool_U,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Nat__Onat_U,help_COMBS_1_1_COMBS_000tc__Nat__Onat_000tc__HOL__Obool_000tc__HOL__Obool_U,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Opname_U,help_COMBS_1_1_COMBS_000tc__Com__Opname_000tc__HOL__Obool_000tc__HOL__Obool_U,help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__Com__Opname_000tc__HOL__Obool_U,help_COMBC_1_1_COMBC_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Oboo,help_COMBB_1_1_COMBB_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opna,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_It__a_Mtc__H,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo,help_COMBS_1_1_COMBS_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool_000tc_,help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Nat__On,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_006,help_COMBS_1_1_COMBS_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obo,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Com__Op,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_007,help_COMBS_1_1_COMBS_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__O,help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob,help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HO,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_008,help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc_,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_009,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_010,help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It,help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__,help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__011,help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_012,help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool,help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__H,help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc_,help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__H,help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool,help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obo,conj_0,conj_1,conj_2,conj_3,conj_4,conj_5] % 1.45/2.42 =============================================================== % 1.45/2.42 % 1.45/2.42 Combined formula: 448 axiom(s) => conjecture % 1.45/2.42 % 1.45/2.42 % Equality/functions detected -> nanoCoP oracle mode % 1.45/2.42 nanoCoP : % 1.45/2.42 % 1,030,649 inferences, 0.758 CPU in 0.759 seconds (100% CPU, 1360342 Lips) % 1.45/2.42 % 1.45/2.42 % nanoCoP proof (equality/functions) % 1.45/2.42 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 1.45/2.42 % 1.45/2.42 % SZS output end Proof %------------------------------------------------------------------------------