%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW473+2 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n003.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 9.23s 9.64s % Output : Proof 9.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW473+2 : TPTP v9.2.1. Released v5.3.0. % 0.00/0.12 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.15/0.33 % Computer : n003.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 11 14:33:12 EDT 2026 % 0.15/0.33 % CPUTime : % 9.23/9.64 % SZS status Theorem % 9.23/9.64 % SZS output start Proof % 9.23/9.64 % 9.23/9.64 =============================================================== % 9.23/9.64 TPTP Problem: conj_6 (conjecture with 916 axiom(s)) % 9.23/9.64 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_COMBK_000tc__HOL__Obool_000t__a,gsy_c_COMBK_000tc__HOL__Obool_000tc__Com__Opname,gsy_c_COMBK_000tc__HOL__Obool_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_COMBK_000tc__HOL__Obool_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,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_Orderings_Obot__class_Obot_000tc__HOL__Obool,gsy_c_Orderings_Obot__class_Obot_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_Orderings_Obot__class_Obot_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,gsy_c_Orderings_Obot__class_Obot_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc,gsy_c_Orderings_Obot__class_Obot_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__,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_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J,gsy_c_Set_Oimage_000t__a_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J,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_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_fFalse,gsy_c_fTrue,gsy_c_hAPP_000t__a_000t__a,gsy_c_hAPP_000t__a_000tc__Com__Opname,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_000t__a_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__H,gsy_c_hAPP_000tc__Com__Opname_000t__a,gsy_c_hAPP_000tc__Com__Opname_000tc__Com__Opname,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_It__a_Mtc__HOL__Obool_J_Mtc__H,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_000t__a,gsy_c_hAPP_000tc__Nat__Onat_000tc__Com__Opname,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__Nat__Onat_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL,gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool,gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opname,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__Com__Opname_Mtc__H,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__Com__Opname,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_It__a_Mtc__H,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__Com__Opname,gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obool,gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HOL,gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__Com__Opna,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___001,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_002,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_v_G,gsy_v_P,gsy_v_U,gsy_v_mgt,gsy_v_pn,gsy_v_wt,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__imageI,fact_8_finite__imageI,fact_9_finite__imageI,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_OinsertI,fact_24_finite_OinsertI,fact_25_finite_OinsertI,fact_26_finite_OinsertI,fact_27_finite_OinsertI,fact_28_finite_OinsertI,fact_29_card__image__le,fact_30_card__image__le,fact_31_card__image__le,fact_32_card__image__le,fact_33_card__image__le,fact_34_card__image__le,fact_35_card__image__le,fact_36_card__image__le,fact_37_card__image__le,fact_38_card__image__le,fact_39_card__image__le,fact_40_card__image__le,fact_41_card__image__le,fact_42_card__mono,fact_43_card__mono,fact_44_card__mono,fact_45_card__mono,fact_46_card__mono,fact_47_card__mono,fact_48_card__seteq,fact_49_card__seteq,fact_50_card__seteq,fact_51_card__seteq,fact_52_card__seteq,fact_53_card__seteq,fact_54_card__insert__le,fact_55_card__insert__le,fact_56_card__insert__le,fact_57_card__insert__le,fact_58_card__insert__le,fact_59_card__insert__le,fact_60_card__insert__if,fact_61_card__insert__if,fact_62_card__insert__if,fact_63_card__insert__if,fact_64_card__insert__if,fact_65_card__insert__if,fact_66_card__insert__disjoint,fact_67_card__insert__disjoint,fact_68_card__insert__disjoint,fact_69_card__insert__disjoint,fact_70_card__insert__disjoint,fact_71_card__insert__disjoint,fact_72_finite__Collect__conjI,fact_73_finite__Collect__conjI,fact_74_finite__Collect__conjI,fact_75_finite__Collect__conjI,fact_76_finite__Collect__conjI,fact_77_finite__Collect__conjI,fact_78_Suc__diff__le,fact_79_finite__Collect__le__nat,fact_80_card__Collect__le__nat,fact_81_Suc__inject,fact_82_nat_Oinject,fact_83_Suc__n__not__n,fact_84_n__not__Suc__n,fact_85_le__antisym,fact_86_le__trans,fact_87_eq__imp__le,fact_88_nat__le__linear,fact_89_le__refl,fact_90_diff__commute,fact_91_finite__Collect__disjI,fact_92_finite__Collect__disjI,fact_93_finite__Collect__disjI,fact_94_finite__Collect__disjI,fact_95_finite__Collect__disjI,fact_96_finite__Collect__disjI,fact_97_finite__insert,fact_98_finite__insert,fact_99_finite__insert,fact_100_finite__insert,fact_101_finite__insert,fact_102_finite__insert,fact_103_finite__subset,fact_104_finite__subset,fact_105_finite__subset,fact_106_finite__subset,fact_107_finite__subset,fact_108_finite__subset,fact_109_rev__finite__subset,fact_110_rev__finite__subset,fact_111_rev__finite__subset,fact_112_rev__finite__subset,fact_113_rev__finite__subset,fact_114_rev__finite__subset,fact_115_Suc__leD,fact_116_le__SucE,fact_117_le__SucI,fact_118_Suc__le__mono,fact_119_le__Suc__eq,fact_120_not__less__eq__eq,fact_121_Suc__n__not__le__n,fact_122_Suc__diff__diff,fact_123_diff__Suc__Suc,fact_124_le__diff__iff,fact_125_Nat_Odiff__diff__eq,fact_126_eq__diff__iff,fact_127_diff__diff__cancel,fact_128_diff__le__mono,fact_129_diff__le__mono2,fact_130_diff__le__self,fact_131_finite__surj,fact_132_finite__surj,fact_133_finite__surj,fact_134_finite__surj,fact_135_finite__surj,fact_136_finite__surj,fact_137_finite__surj,fact_138_finite__surj,fact_139_finite__surj,fact_140_finite__surj,fact_141_finite__surj,fact_142_finite__surj,fact_143_finite__surj,fact_144_finite__surj,fact_145_finite__surj,fact_146_finite__surj,fact_147_finite__surj,fact_148_finite__surj,fact_149_finite__surj,fact_150_finite__surj,fact_151_finite__surj,fact_152_finite__surj,fact_153_finite__surj,fact_154_finite__surj,fact_155_finite__subset__image,fact_156_finite__subset__image,fact_157_finite__subset__image,fact_158_finite__subset__image,fact_159_finite__subset__image,fact_160_finite__subset__image,fact_161_finite__subset__image,fact_162_finite__subset__image,fact_163_finite__subset__image,fact_164_finite__subset__image,fact_165_finite__subset__image,fact_166_finite__subset__image,fact_167_finite__subset__image,fact_168_finite__subset__image,fact_169_finite__subset__image,fact_170_finite__subset__image,fact_171_finite__subset__image,fact_172_finite__subset__image,fact_173_finite__subset__image,fact_174_finite__subset__image,fact_175_finite__subset__image,fact_176_finite__subset__image,fact_177_finite__subset__image,fact_178_finite__subset__image,fact_179_finite__subset__image,fact_180_finite__subset__image,fact_181_finite__subset__image,fact_182_lift__Suc__mono__le,fact_183_lift__Suc__mono__le,fact_184_lift__Suc__mono__le,fact_185_lift__Suc__mono__le,fact_186_lift__Suc__mono__le,fact_187_pigeonhole__infinite,fact_188_pigeonhole__infinite,fact_189_pigeonhole__infinite,fact_190_pigeonhole__infinite,fact_191_pigeonhole__infinite,fact_192_pigeonhole__infinite,fact_193_pigeonhole__infinite,fact_194_pigeonhole__infinite,fact_195_pigeonhole__infinite,fact_196_pigeonhole__infinite,fact_197_pigeonhole__infinite,fact_198_pigeonhole__infinite,fact_199_pigeonhole__infinite,fact_200_pigeonhole__infinite,fact_201_pigeonhole__infinite,fact_202_pigeonhole__infinite,fact_203_pigeonhole__infinite,fact_204_pigeonhole__infinite,fact_205_pigeonhole__infinite,fact_206_pigeonhole__infinite,fact_207_pigeonhole__infinite,fact_208_pigeonhole__infinite,fact_209_pigeonhole__infinite,fact_210_pigeonhole__infinite,fact_211_image__eqI,fact_212_image__eqI,fact_213_image__eqI,fact_214_image__eqI,fact_215_image__eqI,fact_216_equalityI,fact_217_equalityI,fact_218_equalityI,fact_219_subsetD,fact_220_subsetD,fact_221_subsetD,fact_222_insertCI,fact_223_insertCI,fact_224_insertCI,fact_225_insertE,fact_226_insertE,fact_227_insertE,fact_228_zero__induct__lemma,fact_229_Suc__le__D,fact_230_insertI1,fact_231_insertI1,fact_232_insertI1,fact_233_insert__compr,fact_234_insert__compr,fact_235_insert__compr,fact_236_insert__compr,fact_237_insert__compr,fact_238_insert__compr,fact_239_insert__Collect,fact_240_insert__Collect,fact_241_insert__Collect,fact_242_insert__Collect,fact_243_insert__Collect,fact_244_insert__Collect,fact_245_insert__absorb2,fact_246_insert__absorb2,fact_247_insert__absorb2,fact_248_insert__commute,fact_249_insert__commute,fact_250_insert__commute,fact_251_insert__iff,fact_252_insert__iff,fact_253_insert__iff,fact_254_insert__code,fact_255_insert__code,fact_256_insert__code,fact_257_insert__ident,fact_258_insert__ident,fact_259_insert__ident,fact_260_insertI2,fact_261_insertI2,fact_262_insertI2,fact_263_insert__absorb,fact_264_insert__absorb,fact_265_insert__absorb,fact_266_subset__refl,fact_267_subset__refl,fact_268_subset__refl,fact_269_set__eq__subset,fact_270_set__eq__subset,fact_271_set__eq__subset,fact_272_equalityD1,fact_273_equalityD1,fact_274_equalityD1,fact_275_equalityD2,fact_276_equalityD2,fact_277_equalityD2,fact_278_in__mono,fact_279_in__mono,fact_280_in__mono,fact_281_set__rev__mp,fact_282_set__rev__mp,fact_283_set__rev__mp,fact_284_set__mp,fact_285_set__mp,fact_286_set__mp,fact_287_mem__def,fact_288_mem__def,fact_289_mem__def,fact_290_Collect__def,fact_291_Collect__def,fact_292_Collect__def,fact_293_Collect__def,fact_294_Collect__def,fact_295_Collect__def,fact_296_subset__trans,fact_297_subset__trans,fact_298_subset__trans,fact_299_equalityE,fact_300_equalityE,fact_301_equalityE,fact_302_image__iff,fact_303_imageI,fact_304_imageI,fact_305_imageI,fact_306_imageI,fact_307_imageI,fact_308_rev__image__eqI,fact_309_rev__image__eqI,fact_310_rev__image__eqI,fact_311_rev__image__eqI,fact_312_rev__image__eqI,fact_313_insert__compr__raw,fact_314_insert__compr__raw,fact_315_insert__compr__raw,fact_316_insert__compr__raw,fact_317_insert__compr__raw,fact_318_insert__compr__raw,fact_319_subset__insertI,fact_320_subset__insertI,fact_321_subset__insertI,fact_322_insert__subset,fact_323_insert__subset,fact_324_insert__subset,fact_325_subset__insert,fact_326_subset__insert,fact_327_subset__insert,fact_328_subset__insertI2,fact_329_subset__insertI2,fact_330_subset__insertI2,fact_331_insert__mono,fact_332_insert__mono,fact_333_insert__mono,fact_334_image__insert,fact_335_image__insert,fact_336_image__insert,fact_337_image__insert,fact_338_insert__image,fact_339_insert__image,fact_340_insert__image,fact_341_insert__image,fact_342_insert__image,fact_343_insert__image,fact_344_subset__image__iff,fact_345_subset__image__iff,fact_346_subset__image__iff,fact_347_subset__image__iff,fact_348_image__mono,fact_349_image__mono,fact_350_image__mono,fact_351_image__mono,fact_352_imageE,fact_353_imageE,fact_354_imageE,fact_355_imageE,fact_356_imageE,fact_357_subsetI,fact_358_subsetI,fact_359_subsetI,fact_360_image__subsetI,fact_361_image__subsetI,fact_362_image__subsetI,fact_363_image__subsetI,fact_364_image__subsetI,fact_365_image__subsetI,fact_366_image__subsetI,fact_367_order__refl,fact_368_order__refl,fact_369_order__refl,fact_370_order__refl,fact_371_order__refl,fact_372_finite__nat__set__iff__bounded__le,fact_373_assms_I3_J,fact_374_le__fun__def,fact_375_le__fun__def,fact_376_le__fun__def,fact_377_le__funD,fact_378_le__funD,fact_379_le__funD,fact_380_le__funE,fact_381_le__funE,fact_382_le__funE,fact_383_emptyE,fact_384_emptyE,fact_385_emptyE,fact_386_finite_OemptyI,fact_387_finite_OemptyI,fact_388_finite_OemptyI,fact_389_finite_OemptyI,fact_390_finite_OemptyI,fact_391_finite_OemptyI,fact_392_empty__subsetI,fact_393_empty__subsetI,fact_394_empty__subsetI,fact_395_equals0D,fact_396_equals0D,fact_397_equals0D,fact_398_Collect__empty__eq,fact_399_Collect__empty__eq,fact_400_Collect__empty__eq,fact_401_Collect__empty__eq,fact_402_Collect__empty__eq,fact_403_Collect__empty__eq,fact_404_empty__iff,fact_405_empty__iff,fact_406_empty__iff,fact_407_empty__Collect__eq,fact_408_empty__Collect__eq,fact_409_empty__Collect__eq,fact_410_empty__Collect__eq,fact_411_empty__Collect__eq,fact_412_empty__Collect__eq,fact_413_ex__in__conv,fact_414_ex__in__conv,fact_415_ex__in__conv,fact_416_all__not__in__conv,fact_417_all__not__in__conv,fact_418_all__not__in__conv,fact_419_empty__def,fact_420_empty__def,fact_421_empty__def,fact_422_empty__def,fact_423_empty__def,fact_424_empty__def,fact_425_bot__fun__def,fact_426_bot__fun__def,fact_427_bot__fun__def,fact_428_bot__apply,fact_429_bot__apply,fact_430_bot__apply,fact_431_le__bot,fact_432_le__bot,fact_433_le__bot,fact_434_le__bot,fact_435_le__bot,fact_436_bot__unique,fact_437_bot__unique,fact_438_bot__unique,fact_439_bot__unique,fact_440_bot__unique,fact_441_bot__least,fact_442_bot__least,fact_443_bot__least,fact_444_bot__least,fact_445_bot__least,fact_446_singleton__inject,fact_447_singleton__inject,fact_448_singleton__inject,fact_449_singletonE,fact_450_singletonE,fact_451_singletonE,fact_452_doubleton__eq__iff,fact_453_doubleton__eq__iff,fact_454_doubleton__eq__iff,fact_455_singleton__iff,fact_456_singleton__iff,fact_457_singleton__iff,fact_458_insert__not__empty,fact_459_insert__not__empty,fact_460_insert__not__empty,fact_461_empty__not__insert,fact_462_empty__not__insert,fact_463_empty__not__insert,fact_464_subset__empty,fact_465_subset__empty,fact_466_subset__empty,fact_467_image__is__empty,fact_468_image__empty,fact_469_empty__is__image,fact_470_Collect__conv__if,fact_471_Collect__conv__if,fact_472_Collect__conv__if,fact_473_Collect__conv__if,fact_474_Collect__conv__if,fact_475_Collect__conv__if,fact_476_Collect__conv__if2,fact_477_Collect__conv__if2,fact_478_Collect__conv__if2,fact_479_Collect__conv__if2,fact_480_Collect__conv__if2,fact_481_Collect__conv__if2,fact_482_singleton__conv,fact_483_singleton__conv,fact_484_singleton__conv,fact_485_singleton__conv,fact_486_singleton__conv,fact_487_singleton__conv,fact_488_singleton__conv2,fact_489_singleton__conv2,fact_490_singleton__conv2,fact_491_singleton__conv2,fact_492_singleton__conv2,fact_493_singleton__conv2,fact_494_subset__singletonD,fact_495_subset__singletonD,fact_496_subset__singletonD,fact_497_image__constant,fact_498_image__constant__conv,fact_499_linorder__le__cases,fact_500_xt1_I6_J,fact_501_xt1_I6_J,fact_502_xt1_I6_J,fact_503_xt1_I6_J,fact_504_xt1_I6_J,fact_505_xt1_I5_J,fact_506_xt1_I5_J,fact_507_xt1_I5_J,fact_508_xt1_I5_J,fact_509_xt1_I5_J,fact_510_order__trans,fact_511_order__trans,fact_512_order__trans,fact_513_order__trans,fact_514_order__trans,fact_515_order__antisym,fact_516_order__antisym,fact_517_order__antisym,fact_518_order__antisym,fact_519_order__antisym,fact_520_xt1_I4_J,fact_521_xt1_I4_J,fact_522_xt1_I4_J,fact_523_xt1_I4_J,fact_524_xt1_I4_J,fact_525_ord__le__eq__trans,fact_526_ord__le__eq__trans,fact_527_ord__le__eq__trans,fact_528_ord__le__eq__trans,fact_529_ord__le__eq__trans,fact_530_xt1_I3_J,fact_531_xt1_I3_J,fact_532_xt1_I3_J,fact_533_xt1_I3_J,fact_534_xt1_I3_J,fact_535_ord__eq__le__trans,fact_536_ord__eq__le__trans,fact_537_ord__eq__le__trans,fact_538_ord__eq__le__trans,fact_539_ord__eq__le__trans,fact_540_order__antisym__conv,fact_541_order__antisym__conv,fact_542_order__antisym__conv,fact_543_order__antisym__conv,fact_544_order__antisym__conv,fact_545_order__eq__refl,fact_546_order__eq__refl,fact_547_order__eq__refl,fact_548_order__eq__refl,fact_549_order__eq__refl,fact_550_order__eq__iff,fact_551_order__eq__iff,fact_552_order__eq__iff,fact_553_order__eq__iff,fact_554_order__eq__iff,fact_555_linorder__linear,fact_556_finite__subset__induct,fact_557_finite__subset__induct,fact_558_finite__subset__induct,fact_559_finite__subset__induct,fact_560_finite__subset__induct,fact_561_finite__subset__induct,fact_562_assms_I2_J,fact_563_finite__induct,fact_564_finite__induct,fact_565_finite__induct,fact_566_finite__less__ub,fact_567_assms_I4_J,fact_568_diff__Suc__eq__diff__pred,fact_569_diff__Suc__1,fact_570_less__eq__nat_Osimps_I2_J,fact_571_add__Suc__right,fact_572_add__Suc,fact_573_add__Suc__shift,fact_574_nat__add__right__cancel,fact_575_nat__add__left__cancel,fact_576_nat__add__assoc,fact_577_nat__add__left__commute,fact_578_nat__add__commute,fact_579_diff__add__inverse2,fact_580_diff__add__inverse,fact_581_diff__diff__left,fact_582_diff__cancel,fact_583_diff__cancel2,fact_584_le__add2,fact_585_le__add1,fact_586_le__iff__add,fact_587_nat__add__left__cancel__le,fact_588_trans__le__add1,fact_589_trans__le__add2,fact_590_add__le__mono1,fact_591_add__le__mono,fact_592_add__leD2,fact_593_add__leD1,fact_594_add__leE,fact_595_diff__add__assoc2,fact_596_add__diff__assoc2,fact_597_diff__add__assoc,fact_598_le__imp__diff__is__add,fact_599_le__add__diff__inverse2,fact_600_le__diff__conv2,fact_601_add__diff__assoc,fact_602_le__add__diff__inverse,fact_603_le__add__diff,fact_604_le__diff__conv,fact_605_diff__diff__right,fact_606_Suc__eq__plus1,fact_607_Suc__eq__plus1__left,fact_608_diff__Suc__diff__eq2,fact_609_diff__Suc__diff__eq1,fact_610_termination__basic__simps_I3_J,fact_611_termination__basic__simps_I4_J,fact_612_lessI,fact_613_Suc__mono,fact_614_finite__Collect__less__nat,fact_615_termination__basic__simps_I1_J,fact_616_termination__basic__simps_I2_J,fact_617_add__lessD1,fact_618_less__add__eq__less,fact_619_add__less__mono,fact_620_add__less__mono1,fact_621_trans__less__add2,fact_622_trans__less__add1,fact_623_nat__add__left__cancel__less,fact_624_not__add__less2,fact_625_not__add__less1,fact_626_Suc__less__SucD,fact_627_Suc__lessD,fact_628_less__SucE,fact_629_less__trans__Suc,fact_630_Suc__lessI,fact_631_less__SucI,fact_632_less__antisym,fact_633_not__less__less__Suc__eq,fact_634_Suc__less__eq,fact_635_less__Suc__eq,fact_636_not__less__eq,fact_637_less__or__eq__imp__le,fact_638_le__neq__implies__less,fact_639_less__imp__le__nat,fact_640_le__eq__less__or__eq,fact_641_nat__less__le,fact_642_diff__less__mono2,fact_643_less__imp__diff__less,fact_644_termination__basic__simps_I5_J,fact_645_less__not__refl,fact_646_nat__neq__iff,fact_647_linorder__neqE__nat,fact_648_less__irrefl__nat,fact_649_less__not__refl2,fact_650_less__not__refl3,fact_651_nat__less__cases,fact_652_finite__nat__set__iff__bounded,fact_653_card__Collect__less__nat,fact_654_finite__M__bounded__by__nat,fact_655_less__add__Suc1,fact_656_less__add__Suc2,fact_657_less__iff__Suc__add,fact_658_less__eq__Suc__le,fact_659_less__Suc__eq__le,fact_660_Suc__le__eq,fact_661_le__imp__less__Suc,fact_662_Suc__leI,fact_663_le__less__Suc__eq,fact_664_Suc__le__lessD,fact_665_diff__less__Suc,fact_666_add__diff__inverse,fact_667_less__diff__conv,fact_668_diff__less__mono,fact_669_less__diff__iff,fact_670_less__eq__Suc__le__raw,fact_671_mono__nat__linear__lb,fact_672_inc__induct,fact_673_less__imp__Suc__add,fact_674_bounded__nat__set__is__finite,fact_675_less__mono__imp__le__mono,fact_676_Suc__lessE,fact_677_lessE,fact_678_less__zeroE,fact_679_le0,fact_680_zero__less__Suc,fact_681_add__is__1,fact_682_one__is__add,fact_683_diff__add__0,fact_684_diff__is__0__eq_H,fact_685_diff__is__0__eq,fact_686_One__nat__def,fact_687_diffs0__imp__equal,fact_688_diff__self__eq__0,fact_689_minus__nat_Odiff__0,fact_690_diff__0__eq__0,fact_691_Suc__neq__Zero,fact_692_Zero__neq__Suc,fact_693_nat_Osimps_I3_J,fact_694_Suc__not__Zero,fact_695_nat_Osimps_I2_J,fact_696_Zero__not__Suc,fact_697_bot__nat__def,fact_698_le__0__eq,fact_699_less__eq__nat_Osimps_I1_J,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_fFalse_1_1_U,help_fFalse_1_1_T,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_COMBK_1_1_COMBK_000tc__HOL__Obool_000t__a_U,help_COMBK_1_1_COMBK_000t__a_000tc__Com__Opname_U,help_COMBC_1_1_COMBC_000t__a_000t__a_000tc__HOL__Obool_U,help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Nat__Onat_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_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Opname_U,help_COMBC_1_1_COMBC_000t__a_000tc__Nat__Onat_000tc__HOL__Obool_U,help_COMBC_1_1_COMBC_000tc__Nat__Onat_000t__a_000tc__HOL__Obool_U,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_000t__a_000tc__Com__Opname_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_COMBB_1_1_COMBB_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000t__a_U,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_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__fun_It__a_Mtc__HOL__Obool_J_U,help_COMBS_1_1_COMBS_000tc__Nat__Onat_000tc__HOL__Obool_000tc__HOL__Obool_U,help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__Nat__Onat_000tc__HOL__Obool_U,help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__Com__Opname_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_COMBB_1_1_COMBB_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Nat__Onat,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_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool,help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obo,help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_,help_COMBC_1_1_COMBC_000t__a_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__,help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__,help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Nat__Onat_000tc__,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_000t__a_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc,help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc,help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opname_000tc,help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob,help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__003,help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_,help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__Nat__Ona,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_004,help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__005,help_COMBS_1_1_COMBS_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obo,help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Oboo,help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Com__Opname_Mtc__HOL__Oboo,help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__Nat__O,help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__Com__Opn,help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_006,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_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__Com__O,help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_008,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__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__009,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_010,help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_011,help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__012,help_COMBB_1_1_COMBB_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_,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_013,help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__014,help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_015,help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_016,help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It,help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_017,help_COMBB_1_1_COMBB_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It___018,help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__,help_COMBB_1_1_COMBB_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It___019,help_COMBB_1_1_COMBB_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc_,help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It,help_COMBB_1_1_COMBB_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__020,help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__021,help_COMBB_1_1_COMBB_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__022,help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_023,help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_024,help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_025,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_,conj_0,conj_1,conj_2,conj_3,conj_4,conj_5] % 9.23/9.64 =============================================================== % 9.23/9.64 % 9.23/9.64 Combined formula: 916 axiom(s) => conjecture % 9.23/9.64 % 9.23/9.64 % Equality/functions detected -> nanoCoP oracle mode % 9.23/9.64 nanoCoP : % 9.23/9.64 % 12,131,312 inferences, 7.866 CPU in 7.865 seconds (100% CPU, 1542321 Lips) % 9.23/9.64 % 9.23/9.64 % nanoCoP proof (equality/functions) % 9.23/9.64 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 9.23/9.64 % 9.23/9.64 % SZS output end Proof %------------------------------------------------------------------------------