%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW478+5 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n021.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 1.74s 2.42s % Output : Proof 1.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW478+5 : 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 : n021.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:34:46 EDT 2026 % 0.17/0.34 % CPUTime : % 1.74/2.42 % SZS status Theorem % 1.74/2.42 % SZS output start Proof % 1.74/2.42 % 1.74/2.42 =============================================================== % 1.74/2.42 TPTP Problem: conj_0 (conjecture with 155 axiom(s)) % 1.74/2.42 Axioms: [tsy_c_COMBB_res,tsy_c_COMBC_res,tsy_c_COMBK_res,tsy_c_COMBS_res,tsy_c_Conform_Ohconf_res,tsy_c_Conform_Olconf_res,tsy_c_Expr_Oexp_OBlock_res,tsy_c_Expr_Oexp_OLAss_res,tsy_c_Expr_Oexp_OSeq_res,tsy_c_Expr_Oexp_OVal_res,tsy_c_Fun_Ofun__upd_res,tsy_c_HOL_Oundefined_res,tsy_c_JWellForm_Owf__J__mdecl_res,tsy_c_Option_Ooption_ONone_res,tsy_c_Option_Ooption_OSome_res,tsy_c_Product__Type_OPair_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_SmallStep_Oassigned_res,tsy_c_SmallStep_Ored_res,tsy_c_SmallStep_Oredp_res,tsy_c_State_Ohp_res,tsy_c_TypeRel_Owiden_res,tsy_c_TypeSafe__Mirabelle__mcolmsuaig_Osconf_res,tsy_c_Value_Oval_OUnit_res,tsy_c_WellForm_Owf__prog_res,tsy_c_WellTypeRT_OWTrt_res,tsy_c_fconj_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_widen__trans,fact_36_InitBlockRed_I5_J,fact_37_split__paired__Ex,fact_38_PairE,fact_39_internal__split__conv,fact_40_sconf__def,fact_41_prod__caseI,fact_42_splitI,fact_43_splitD,fact_44_split__weak__cong,fact_45_internal__split__def,fact_46_split__twice,fact_47_split__part,fact_48_prod_Osimps_I2_J,fact_49_split__conv,fact_50_split__eta,fact_51_red__reds_OInitBlockRed,fact_52_red__reds_ORedInitBlock,fact_53_splitI2,fact_54_splitE,fact_55_WTrtBlock,fact_56_mem__splitI,fact_57_WTrtSeq,fact_58_splitD_H,fact_59_red__reds_OSeqRed,fact_60_red__reds_OLAssRed,fact_61_red__reds_ORedSeq,fact_62_red__reds_ORedBlock,fact_63_splitE_H,fact_64_mem__splitE,fact_65_splitI2_H,fact_66_mem__splitI2,fact_67_red__reds_ORedLAss,fact_68_cond__split__eta,fact_69_splitE2,fact_70_exp_Osimps_I143_J,fact_71_exp_Osimps_I196_J,fact_72_exp_Osimps_I3_J,fact_73_exp_Osimps_I11_J,fact_74_exp_Osimps_I6_J,fact_75_ext,fact_76_mem__def,fact_77_exp_Osimps_I10_J,fact_78_exp_Osimps_I84_J,fact_79_exp_Osimps_I74_J,fact_80_exp_Osimps_I85_J,fact_81_exp_Osimps_I75_J,fact_82_exp_Osimps_I82_J,fact_83_exp_Osimps_I83_J,fact_84_exp_Osimps_I145_J,fact_85_exp_Osimps_I144_J,fact_86_exp_Osimps_I197_J,fact_87_exp_Osimps_I142_J,fact_88_redp__redsp_OInitBlockRed,fact_89_red__reds_OBlockRedSome,fact_90_redp__redsp_OSeqRed,fact_91_redp__redsp_OLAssRed,fact_92_redp__redsp_OBlockRedNone,fact_93_redp__redsp_ORedSeq,fact_94_map__upd__nonempty,fact_95_redp__redsp_ORedBlock,fact_96_empty__upd__none,fact_97_redp__redsp_OBlockRedSome,fact_98_redp__red__eq,fact_99_redp__redsp_ORedInitBlock,help_ti_idem,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] % 1.74/2.42 =============================================================== % 1.74/2.42 % 1.74/2.42 Combined formula: 155 axiom(s) => conjecture % 1.74/2.42 % 1.74/2.42 % Equality/functions detected -> nanoCoP oracle mode % 1.74/2.42 nanoCoP : % 1.74/2.42 % 2,153,322 inferences, 0.776 CPU in 0.776 seconds (100% CPU, 2776014 Lips) % 1.74/2.42 % 1.74/2.42 % nanoCoP proof (equality/functions) % 1.74/2.42 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 1.74/2.42 % 1.74/2.42 % SZS output end Proof %------------------------------------------------------------------------------