%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW478+6 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n006.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:17:00 PM UTC 2026 % Result : Theorem 15.22s 15.91s % Output : Proof 15.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW478+6 : TPTP v9.2.1. Released v5.3.0. % 0.00/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.18/0.34 % Computer : n006.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.34 % WCLimit : 300 % 0.18/0.34 % DateTime : Mon May 11 14:33:47 EDT 2026 % 0.18/0.34 % CPUTime : % 15.22/15.91 % SZS status Theorem % 15.22/15.91 % SZS output start Proof % 15.22/15.91 % 15.22/15.91 =============================================================== % 15.22/15.91 TPTP Problem: conj_0 (conjecture with 604 axiom(s)) % 15.22/15.91 Axioms: [tsy_c_BigStep_Oeval_res,tsy_c_BigStep_Ofinal_res,tsy_c_COMBB_res,tsy_c_COMBC_res,tsy_c_COMBK_res,tsy_c_COMBS_res,tsy_c_Conform_Oconf_res,tsy_c_Conform_Ohconf_res,tsy_c_Conform_Olconf_res,tsy_c_Conform_Ooconf_res,tsy_c_Decl_Ois__class_res,tsy_c_DefAss_O_092_060D_062_res,tsy_c_Exceptions_OClassCast_res,tsy_c_Exceptions_ONullPointer_res,tsy_c_Exceptions_Oaddr__of__sys__xcpt_res,tsy_c_Expr_Obinop_res,tsy_c_Expr_Obop_OAdd_res,tsy_c_Expr_Obop_OEq_res,tsy_c_Expr_Oexp_OBinOp_res,tsy_c_Expr_Oexp_OBlock_res,tsy_c_Expr_Oexp_OCast_res,tsy_c_Expr_Oexp_OFAcc_res,tsy_c_Expr_Oexp_OFAss_res,tsy_c_Expr_Oexp_OLAss_res,tsy_c_Expr_Oexp_OSeq_res,tsy_c_Expr_Oexp_OTryCatch_res,tsy_c_Expr_Oexp_OVal_res,tsy_c_Expr_Oexp_OWhile_res,tsy_c_Expr_Oexp_Othrow_res,tsy_c_Fun_Ofun__upd_res,tsy_c_HOL_Oundefined_res,tsy_c_JWellForm_Owf__J__mdecl_res,tsy_c_Map_Odom_res,tsy_c_Map_Omap__add_res,tsy_c_Objects_Ohext_res,tsy_c_Option_Ooption_ONone_res,tsy_c_Option_Ooption_OSome_res,tsy_c_Option_Othe_res,tsy_c_Product__Type_OPair_res,tsy_c_Product__Type_Ocurry_res,tsy_c_Product__Type_Ointernal__split_res,tsy_c_Product__Type_Oprod_Oprod__case_res,tsy_c_Product__Type_Oprod_Oprod__rec_res,tsy_c_Set_OCollect_res,tsy_c_SmallStep_Oassigned_res,tsy_c_SmallStep_Ored_res,tsy_c_SmallStep_Oredp_res,tsy_c_State_Ohp_res,tsy_c_Transitive__Closure_Ortrancl_res,tsy_c_Transitive__Closure_Ortranclp_res,tsy_c_TypeRel_Ohas__field_res,tsy_c_TypeRel_Osees__field_res,tsy_c_TypeRel_Osubcls1_res,tsy_c_TypeRel_Osubcls1p_res,tsy_c_TypeRel_Owiden_res,tsy_c_TypeSafe__Mirabelle__lrkjpapgnz_Osconf_res,tsy_c_Type_Ois__refT_res,tsy_c_Type_Oty_OClass_res,tsy_c_Type_Oty_ONT_res,tsy_c_Type_Oty_OVoid_res,tsy_c_Value_Oval_OAddr_res,tsy_c_Value_Oval_OBool_res,tsy_c_Value_Oval_ONull_res,tsy_c_Value_Oval_OUnit_res,tsy_c_WWellForm_Owwf__J__mdecl_res,tsy_c_WellForm_Owf__prog_res,tsy_c_WellTypeRT_OWTrt_res,tsy_c_fFalse_res,tsy_c_fNot_res,tsy_c_fTrue_res,tsy_c_fconj_res,tsy_c_fequal_res,tsy_c_hAPP_arg1,tsy_c_hAPP_arg2,tsy_c_hAPP_res,tsy_c_hBOOL_arg1,tsy_c_member_res,tsy_v_E_____res,tsy_v_P_res,tsy_v_T_H_____res,tsy_v_T_____res,tsy_v_V_____res,tsy_v_e_Ha_____res,tsy_v_ea_____res,tsy_v_h_Ha_____res,tsy_v_ha_____res,tsy_v_l_Ha_____res,tsy_v_la_____res,tsy_v_v_H_____res,tsy_v_v_____res,fact_0_InitBlockRed_I3_J,fact_1_InitBlockRed_I1_J,fact_2_fun__upd__triv,fact_3_assms,fact_4_map__upd__Some__unfold,fact_5_map__upd__triv,fact_6_map__upd__eqD1,fact_7_InitBlockRed_I2_J,fact_8_prod__induct6,fact_9_prod__cases6,fact_10_prod__induct5,fact_11_prod__cases5,fact_12_prod__induct4,fact_13_prod__cases4,fact_14_InitBlockRed_I4_J,fact_15_Pair__inject,fact_16_Pair__eq,fact_17_split__paired__All,fact_18_fun__upd__def,fact_19_fun__upd__idem,fact_20_fun__upd__other,fact_21_fun__upd__twist,fact_22_fun__upd__apply,fact_23_fun__upd__same,fact_24_fun__upd__upd,fact_25_fun__upd__idem__iff,fact_26_widen__refl,fact_27_red__preserves__hconf,fact_28_red__preserves__lconf,fact_29_prod__cases3,fact_30_prod__induct3,fact_31_red__preserves__sconf,fact_32_prod_Orecs,fact_33_pred__equals__eq2,fact_34_prod_Oexhaust,fact_35_PairE,fact_36_split__paired__Ex,fact_37_widen__trans,fact_38_InitBlockRed_I5_J,fact_39_internal__split__conv,fact_40_sconf__def,fact_41_red__hext__incr,fact_42_curry__def,fact_43_red__preserves__defass,fact_44_option_Oinject,fact_45_curryI,fact_46_red__lcl__add,fact_47_lconf__upd,fact_48_prod__caseI,fact_49_splitI,fact_50_conf__hext,fact_51_conf__upd__obj,fact_52_map__add__dom__app__simps_I1_J,fact_53_split__weak__cong,fact_54_map__add__dom__app__simps_I3_J,fact_55_map__add__dom__app__simps_I2_J,fact_56_internal__split__def,fact_57_map__add__assoc,fact_58_split__twice,fact_59_split__curry,fact_60_curry__split,fact_61_split__part,fact_62_red__reds_ORedInitBlock,fact_63_conf__widen,fact_64_splitD,fact_65_lconf__hext,fact_66_red__reds_ORedSeq,fact_67_map__add__upd__left,fact_68_red__reds_ORedBlock,fact_69_domI,fact_70_red__reds_OInitBlockRed,fact_71_prod_Osimps_I2_J,fact_72_split__conv,fact_73_map__add__find__right,fact_74_split__eta,fact_75_ext,fact_76_mem__def,fact_77_Collect__def,fact_78_red__reds_OLAssRed,fact_79_red__reds_OSeqRed,fact_80_curryE,fact_81_curryD,fact_82_map__add__upd,fact_83_curry__conv,fact_84_lconf__upd2,fact_85_WTrtBlock,fact_86_splitE,fact_87_splitI2,fact_88_WTrtSeq,fact_89_lconf__def,fact_90_red__reds_ORedLAss,fact_91_hext__refl,fact_92_cond__split__eta,fact_93_domD,fact_94_splitE2,fact_95_mem__splitI,fact_96_splitD_H,fact_97_hext__upd__obj,fact_98_hext__trans,fact_99_WTrt__hext__mono,fact_100_hext__objD,fact_101_hext__def,fact_102_mem__splitI2,fact_103_splitI2_H,fact_104_mem__splitE,fact_105_splitE_H,fact_106__092_060D_062___092_060D_062s_Osimps_I6_J,fact_107_exp_Osimps_I143_J,fact_108_exp_Osimps_I3_J,fact_109_exp_Osimps_I11_J,fact_110_exp_Osimps_I6_J,fact_111_exp_Osimps_I10_J,fact_112_exp_Osimps_I84_J,fact_113_exp_Osimps_I74_J,fact_114_exp_Osimps_I85_J,fact_115_exp_Osimps_I75_J,fact_116_exp_Osimps_I82_J,fact_117_exp_Osimps_I83_J,fact_118__092_060D_062___092_060D_062s_Osimps_I3_J,fact_119_exp_Osimps_I145_J,fact_120_exp_Osimps_I144_J,fact_121_exp_Osimps_I197_J,fact_122_exp_Osimps_I142_J,fact_123_exp_Osimps_I196_J,fact_124_hconf__upd__obj,fact_125_redp__redsp_OInitBlockRed,fact_126_red__reds_OBlockRedSome,fact_127_WTrtLAss,fact_128_LAssRedsVal,fact_129_hextI,fact_130_redp__redsp_ORedLAss,fact_131_lconf__empty,fact_132_option_Osimps_I2_J,fact_133_option_Osimps_I3_J,fact_134_not__Some__eq,fact_135_not__None__eq,fact_136_redp__redsp_OLAssRed,fact_137_redp__redsp_OSeqRed,fact_138_dom__def,fact_139_domIff,fact_140_redp__redsp_OBlockRedNone,fact_141_map__add__None,fact_142_empty__upd__none,fact_143_map__add__empty,fact_144_empty__map__add,fact_145_redp__redsp_ORedSeq,fact_146_map__upd__nonempty,fact_147_redp__redsp_ORedBlock,fact_148_oconf__hext,fact_149_map__add__SomeD,fact_150_map__add__Some__iff,fact_151_SeqReds,fact_152_LAssReds,fact_153_redp__redsp_OBlockRedSome,fact_154_SeqReds2,fact_155_redp__red__eq,fact_156_hconfD,fact_157_redp__redsp_ORedInitBlock,fact_158_red__reds_OBlockRedNone,fact_159_Red__lcl__add,fact_160_oconf__upd__obj,fact_161_WTrt__elim__cases_I1_J,fact_162_InitBlockReds,fact_163_InitBlockRedsFinal,fact_164_assigned__def,fact_165_rtrancl_Ortrancl__refl,fact_166_BlockRedsFinal,fact_167_oconf__fupd,fact_168_r__into__rtrancl,fact_169_the_Osimps,fact_170_hext__new,fact_171_rtrancl__idemp,fact_172_oconf__new,fact_173_hconf__new,fact_174_rtrancl__trans,fact_175_rtrancl_Ortrancl__into__rtrancl,fact_176_converse__rtrancl__into__rtrancl,fact_177_converse__rtranclE2,fact_178_converse__rtrancl__induct2,fact_179_rtrancl__induct2,fact_180_progress,fact_181_option_Oexhaust,fact_182_rtranclE,fact_183_wf__prog__wwf__prog,fact_184_wf__mdecl__wwf__mdecl,fact_185_rtrancl__induct,fact_186_converse__rtrancl__induct,fact_187_converse__rtranclE,fact_188_small__by__big,fact_189_big__iff__small,fact_190_FAssRedsVal,fact_191_red__reds_ORedFAss,fact_192_big__by__small,fact_193_exp_Osimps_I8_J,fact_194_redp__redsp_OFAssRed1,fact_195_exp_Osimps_I78_J,fact_196_exp_Osimps_I79_J,fact_197_exp_Osimps_I139_J,fact_198_exp_Osimps_I174_J,fact_199_exp_Osimps_I138_J,fact_200_exp_Osimps_I175_J,fact_201_exp_Osimps_I172_J,fact_202_exp_Osimps_I173_J,fact_203_redp__redsp_OFAssRed2,fact_204_red__reds_OFAssRed1,fact_205_red__reds_OFAssRed2,fact_206_FAssReds1,fact_207_extend__1__eval,fact_208_FAssReds2,fact_209_redp__redsp_ORedFAss,fact_210_extend__eval,fact_211_FAss,fact_212_LAss,fact_213_Block,fact_214_FAccRedsVal,fact_215_eval__hext,fact_216_exp_Osimps_I7_J,fact_217_redp__redsp_OFAccRed,fact_218_exp_Osimps_I77_J,fact_219_exp_Osimps_I76_J,fact_220_exp_Osimps_I161_J,fact_221_exp_Osimps_I136_J,fact_222_exp_Osimps_I160_J,fact_223_exp_Osimps_I137_J,fact_224_exp_Osimps_I155_J,fact_225_exp_Osimps_I154_J,fact_226_exp_Osimps_I158_J,fact_227_exp_Osimps_I159_J,fact_228__092_060D_062___092_060D_062s_Osimps_I7_J,fact_229_red__reds_OFAccRed,fact_230_FAccReds,fact_231_FAcc,fact_232_Val,fact_233_eval__cases_I2_J,fact_234_eval__final,fact_235_eval__finalId,fact_236_redp__redsp_ORedFAcc,fact_237_red__reds_ORedFAcc,fact_238_Seq,fact_239_eval__cases_I8_J,fact_240_red__reds_OInitBlockThrow,fact_241_val_Osimps_I11_J,fact_242_val_Osimps_I10_J,fact_243_redp__redsp_OInitBlockThrow,fact_244_eval__evals_OThrowThrow,fact_245_redp__redsp_OThrowRed,fact_246_redp__redsp_OThrowThrow,fact_247_exp_Osimps_I14_J,fact_248_exp_Osimps_I90_J,fact_249_exp_Osimps_I91_J,fact_250_exp_Osimps_I150_J,fact_251_exp_Osimps_I210_J,fact_252_exp_Osimps_I151_J,fact_253_exp_Osimps_I211_J,fact_254_exp_Osimps_I181_J,fact_255_exp_Osimps_I180_J,fact_256_exp_Osimps_I202_J,fact_257_exp_Osimps_I203_J,fact_258_exp_Osimps_I167_J,fact_259_exp_Osimps_I166_J,fact_260__092_060D_062___092_060D_062s_Osimps_I14_J,fact_261_eval__evals_OLAssThrow,fact_262_eval__evals_OSeqThrow,fact_263_eval__evals_OFAssThrow1,fact_264_redp__redsp_OLAssThrow,fact_265_redp__redsp_OSeqThrow,fact_266_eval__evals_OFAccThrow,fact_267_redp__redsp_OFAssThrow1,fact_268_redp__redsp_OFAccThrow,fact_269_red__reds_OThrowThrow,fact_270_red__reds_OThrowRed,fact_271_Throw,fact_272_eval__evals_OFAssThrow2,fact_273_redp__redsp_OFAssThrow2,fact_274_val_Osimps_I3_J,fact_275_final__def,fact_276_ThrowReds,fact_277_ThrowRedsThrow,fact_278_red__reds_OLAssThrow,fact_279_red__reds_OSeqThrow,fact_280_red__reds_OFAssThrow1,fact_281_red__reds_OFAccThrow,fact_282_redp__redsp_OBlockThrow,fact_283_red__reds_OFAssThrow2,fact_284_LAssRedsThrow,fact_285_SeqRedsThrow,fact_286_FAssRedsThrow1,fact_287_FAccRedsThrow,fact_288_FAssRedsThrow2,fact_289_red__reds_OBlockThrow,fact_290_eval__cases_I4_J,fact_291_finalE,fact_292_eval__cases_I9_J,fact_293_TryCatchRedsFinal,fact_294_exp_Osimps_I224_J,fact_295_exp_Osimps_I225_J,fact_296_redp__redsp_OTryRed,fact_297_exp_Osimps_I92_J,fact_298_exp_Osimps_I93_J,fact_299_exp_Osimps_I15_J,fact_300_exp_Osimps_I212_J,fact_301_exp_Osimps_I152_J,fact_302_exp_Osimps_I213_J,fact_303_exp_Osimps_I153_J,fact_304_exp_Osimps_I183_J,fact_305_exp_Osimps_I182_J,fact_306_exp_Osimps_I204_J,fact_307_exp_Osimps_I205_J,fact_308_exp_Osimps_I169_J,fact_309_exp_Osimps_I168_J,fact_310_Try,fact_311_redp__redsp_ORedTry,fact_312_has__field__mono,fact_313_red__reds_OTryRed,fact_314_red__reds_ORedTry,fact_315_TryReds,fact_316_TryThrow,fact_317_TryRedsVal,fact_318_red__reds_ORedTryFail,fact_319_TryCatch,fact_320_TryRedsFail,fact_321_red__reds_ORedTryCatch,fact_322_CastRedsAddr,fact_323_red__reds_ORedCast,fact_324_WTrtTry,fact_325_exp_Osimps_I67_J,fact_326_exp_Osimps_I66_J,fact_327_exp_Osimps_I69_J,fact_328_exp_Osimps_I68_J,fact_329_exp_Osimps_I61_J,fact_330_exp_Osimps_I60_J,fact_331_exp_Osimps_I50_J,fact_332_exp_Osimps_I51_J,fact_333_exp_Osimps_I55_J,fact_334_exp_Osimps_I54_J,fact_335_exp_Osimps_I58_J,fact_336_exp_Osimps_I59_J,fact_337_exp_Osimps_I53_J,fact_338_exp_Osimps_I52_J,fact_339__092_060D_062___092_060D_062s_Osimps_I2_J,fact_340_exp_Osimps_I2_J,fact_341_exp_Osimps_I44_J,fact_342_exp_Osimps_I45_J,fact_343_redp__redsp_OCastRed,fact_344_eval__evals_OCastThrow,fact_345_redp__redsp_OCastThrow,fact_346_WTrtFAcc,fact_347_red__reds_OCastRed,fact_348_red__reds_OCastThrow,fact_349_CastReds,fact_350_Class__widen__Class,fact_351_widen__subcls,fact_352_WTrtFAss,fact_353_CastRedsThrow,fact_354_Cast,fact_355_WTrt__elim__cases_I5_J,fact_356_final__addrE,fact_357_CastRedsFail,fact_358_CastFail,fact_359_red__reds_ORedCastFail,fact_360_Class__widen,fact_361_redp__redsp_ORedTryCatch,fact_362_subcls1p__subcls1__eq,fact_363_rtranclp_Ortrancl__refl,fact_364_r__into__rtranclp,fact_365_rtranclp__idemp,fact_366_converse__rtranclp__into__rtranclp,fact_367_rtranclp_Ortrancl__into__rtrancl,fact_368_rtranclp__trans,fact_369_rtranclp__rtrancl__eq,fact_370_redp__redsp_ORedCast,fact_371_redp__redsp_ORedTryFail,fact_372_redp__redsp_ORedCastFail,fact_373_ty_Osimps_I8_J,fact_374_ty_Osimps_I9_J,fact_375_ty_Oinject,fact_376_CastRedsNull,fact_377_widen__Class,fact_378_widen__null,fact_379_ty_Osimps_I21_J,fact_380_ty_Osimps_I20_J,fact_381_ty_Osimps_I6_J,fact_382_ty_Osimps_I7_J,fact_383_val_Osimps_I4_J,fact_384_val_Osimps_I5_J,fact_385_conf__NT,fact_386_conf__Null,fact_387_val_Osimps_I17_J,fact_388_val_Osimps_I16_J,fact_389_WTrtFAccNT,fact_390_CastNull,fact_391_redp__redsp_ORedCastNull,fact_392_WTrtFAssNT,fact_393_red__reds_ORedCastNull,fact_394_WTrt__elim__cases_I7_J,fact_395_widen_Osimps,fact_396_WTrt__elim__cases_I8_J,fact_397_FAccRedsNull,fact_398_ThrowNull,fact_399_redp__redsp_ORedThrowNull,fact_400_FAssNull,fact_401_FAccNull,fact_402_redp__redsp_ORedFAssNull,fact_403_redp__redsp_ORedFAccNull,fact_404_red__reds_ORedThrowNull,fact_405_ThrowRedsNull,fact_406_red__reds_ORedFAssNull,fact_407_red__reds_ORedFAccNull,fact_408_FAssRedsNull,fact_409_eval__cases_I12_J,fact_410_non__npD,fact_411_finalRefE,fact_412_sees__field__decl__above,fact_413_WTrtThrow,fact_414_sees__field__idemp,fact_415_sees__field__fun,fact_416_has__visible__field,fact_417_is__refT__def,fact_418_WTrt__elim__cases_I4_J,fact_419_refTE,fact_420_WTrtCast,fact_421_BinOpRedsThrow2,fact_422_exp_Osimps_I46_J,fact_423_exp_Osimps_I47_J,fact_424_eval__evals_OBinOpThrow1,fact_425_exp_Osimps_I113_J,fact_426_exp_Osimps_I112_J,fact_427_exp_Osimps_I107_J,fact_428_exp_Osimps_I97_J,fact_429_exp_Osimps_I106_J,fact_430_exp_Osimps_I96_J,fact_431_exp_Osimps_I101_J,fact_432_exp_Osimps_I100_J,fact_433_exp_Osimps_I104_J,fact_434_exp_Osimps_I105_J,fact_435_exp_Osimps_I98_J,fact_436_exp_Osimps_I99_J,fact_437_redp__redsp_OBinOpRed1,fact_438_exp_Osimps_I4_J,fact_439_exp_Osimps_I71_J,fact_440_exp_Osimps_I70_J,fact_441_exp_Osimps_I114_J,fact_442_exp_Osimps_I115_J,fact_443_redp__redsp_OBinOpThrow1,fact_444_redp__redsp_OBinOpRed2,fact_445_red__reds_OBinOpRed1,fact_446_eval__evals_OBinOpThrow2,fact_447_redp__redsp_OBinOpThrow2,fact_448_red__reds_OBinOpRed2,fact_449_red__reds_OBinOpThrow1,fact_450_BinOp1Reds,fact_451_red__reds_OBinOpThrow2,fact_452_BinOp2Reds,fact_453_BinOpRedsThrow1,fact_454_WTrt__elim__cases_I6_J,fact_455_BinOpRedsVal,fact_456_BinOp,fact_457_redp__redsp_ORedBinOp,fact_458_red__reds_ORedBinOp,fact_459_eval__cases_I3_J,fact_460_binop_Osimps_I3_J,fact_461_binop_Osimps_I10_J,fact_462_binop_Osimps_I6_J,fact_463_binop_Osimps_I4_J,fact_464_binop_Osimps_I8_J,fact_465_binop_Osimps_I7_J,fact_466_binop_Osimps_I5_J,fact_467_binop_Osimps_I9_J,fact_468_val_Osimps_I12_J,fact_469_val_Osimps_I13_J,fact_470_val_Osimps_I1_J,fact_471_val_Osimps_I6_J,fact_472_val_Osimps_I7_J,fact_473_val_Osimps_I21_J,fact_474_val_Osimps_I20_J,fact_475_binop_Osimps_I1_J,fact_476_WhileFReds,fact_477_exp_Osimps_I111_J,fact_478_exp_Osimps_I110_J,fact_479_WhileCondThrow,fact_480_exp_Osimps_I64_J,fact_481_exp_Osimps_I65_J,fact_482_exp_Osimps_I221_J,fact_483_exp_Osimps_I220_J,fact_484_exp_Osimps_I208_J,fact_485_exp_Osimps_I148_J,fact_486_exp_Osimps_I209_J,fact_487_exp_Osimps_I149_J,fact_488_exp_Osimps_I178_J,fact_489_exp_Osimps_I179_J,fact_490_exp_Osimps_I201_J,fact_491_exp_Osimps_I200_J,fact_492_exp_Osimps_I164_J,fact_493_exp_Osimps_I165_J,fact_494_exp_Osimps_I13_J,fact_495_exp_Osimps_I89_J,fact_496_exp_Osimps_I88_J,fact_497_exp_Osimps_I222_J,fact_498_exp_Osimps_I223_J,fact_499_bop_Oexhaust,help_ti_idem,help_fNot_1_1_U,help_fNot_2_1_U,help_COMBB_1_1_U,help_COMBC_1_1_U,help_COMBK_1_1_U,help_COMBS_1_1_U,help_fconj_1_1_U,help_fconj_2_1_U,help_fconj_3_1_U,help_fFalse_1_1_U,help_fFalse_1_1_T,help_fequal_1_1_T,help_fequal_2_1_T] % 15.22/15.91 =============================================================== % 15.22/15.91 % 15.22/15.91 Combined formula: 604 axiom(s) => conjecture % 15.22/15.91 % 15.22/15.91 % Equality/functions detected -> nanoCoP oracle mode % 15.22/15.91 nanoCoP : % 15.22/15.91 % 16,649,571 inferences, 11.903 CPU in 11.905 seconds (100% CPU, 1398751 Lips) % 15.22/15.91 % 15.22/15.91 % nanoCoP proof (equality/functions) % 15.22/15.91 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 15.22/15.91 % 15.22/15.91 % SZS output end Proof %------------------------------------------------------------------------------