Proof summary for theory newton1 newton_x_TCC1...............................proved - complete [O](0.32 s) newton_x_TCC2...............................proved - complete [O](0.25 s) delta_i_lem_TCC1............................proved - complete [O](0.26 s) delta_i_lem.................................proved - complete [O](0.32 s) delta_bound.................................proved - complete [O](0.53 s) delta_ge0...................................proved - complete [O](0.51 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.19 s) Proof summary for theory md_unpack_correct md_unp_unimpl..............................proved - complete [O]( 1.36 s) md_unp_SNANs...............................proved - complete [O]( 9.37 s) md_unp_QNANs...............................proved - complete [O](27.95 s) md_unp_SNANd...............................proved - complete [O]( 9.13 s) md_unp_QNANd...............................proved - complete [O](27.51 s) md_unp_inf_times_zero_s....................proved - complete [O]( 8.88 s) md_unp_inf_times_fininf_s..................proved - complete [O]( 9.69 s) md_unp_zero_times_finzero_s................proved - complete [O]( 9.25 s) md_unp_spec_sign_s.........................proved - complete [O](41.89 s) md_unp_inf_times_zero_d....................proved - complete [O]( 8.67 s) md_unp_inf_times_fininf_d..................proved - complete [O]( 9.45 s) md_unp_zero_times_finzero_d................proved - complete [O]( 9.06 s) md_unp_spec_sign_d.........................proved - complete [O](41.43 s) md_unp_infz_div_infz_s.....................proved - complete [O]( 8.94 s) md_unp_div_resinf_s........................proved - complete [O]( 9.49 s) md_unp_fin_div_z_s.........................proved - complete [O]( 9.29 s) md_unp_div_reszero_s.......................proved - complete [O]( 9.52 s) md_unp_infz_div_infz_d.....................proved - complete [O]( 8.75 s) md_unp_div_resinf_d........................proved - complete [O]( 9.28 s) md_unp_fin_div_z_d.........................proved - complete [O]( 9.10 s) md_unp_div_reszero_d.......................proved - complete [O]( 9.34 s) md_unp_special.............................proved - complete [O](20.56 s) md_unp_spec_cover..........................proved - complete [O]( 2.74 s) smul_rdinp_TCC1............................proved - complete [O]( 0.27 s) smul_rdinp_TCC2............................proved - complete [O]( 0.33 s) smul_rdinp_TCC3............................proved - complete [O]( 0.25 s) smul_rdinp_TCC4............................proved - complete [O]( 0.36 s) smul_rdinp_TCC5............................proved - complete [O]( 0.39 s) smul_rdinp_TCC6............................proved - complete [O]( 0.38 s) smul_rdinp_TCC7............................proved - complete [O]( 0.36 s) smul_rdinp_TCC8............................proved - complete [O]( 1.81 s) smul_rdinp_TCC9............................proved - complete [O]( 1.70 s) smul_rdinp_TCC10...........................proved - complete [O]( 0.43 s) smul_rdinp_TCC11...........................proved - complete [O]( 0.45 s) smul_rdinp.................................proved - complete [O](23.58 s) dmul_rdinp_TCC1............................proved - complete [O]( 0.27 s) dmul_rdinp_TCC2............................proved - complete [O]( 0.37 s) dmul_rdinp_TCC3............................proved - complete [O]( 0.35 s) dmul_rdinp_TCC4............................proved - complete [O]( 0.35 s) dmul_rdinp_TCC5............................proved - complete [O]( 0.39 s) dmul_rdinp_TCC6............................proved - complete [O]( 0.37 s) dmul_rdinp_TCC7............................proved - complete [O]( 0.36 s) dmul_rdinp_TCC8............................proved - complete [O]( 1.80 s) dmul_rdinp_TCC9............................proved - complete [O]( 0.39 s) dmul_rdinp_TCC10...........................proved - complete [O]( 0.44 s) dmul_rdinp_TCC11...........................proved - complete [O]( 0.45 s) dmul_rdinp.................................proved - complete [O](19.52 s) mul_rdinp_passthrough......................proved - complete [O]( 0.69 s) sdiv_rdinp_TCC1............................proved - complete [O]( 0.49 s) sdiv_rdinp_TCC2............................proved - complete [O]( 0.64 s) sdiv_rdinp_TCC3............................proved - complete [O]( 0.28 s) sdiv_rdinp_TCC4............................proved - complete [O]( 0.27 s) sdiv_rdinp_TCC5............................proved - complete [O]( 0.66 s) sdiv_rdinp_TCC6............................proved - complete [O]( 0.28 s) sdiv_rdinp_TCC7............................proved - complete [O]( 0.28 s) sdiv_rdinp_TCC8............................proved - complete [O]( 0.72 s) sdiv_rdinp_TCC9............................proved - complete [O]( 2.13 s) sdiv_rdinp_TCC10...........................proved - complete [O]( 0.28 s) sdiv_rdinp_TCC11...........................proved - complete [O]( 0.77 s) sdiv_rdinp_TCC12...........................proved - complete [O]( 0.28 s) sdiv_rdinp_TCC13...........................proved - complete [O]( 0.29 s) sdiv_rdinp.................................proved - complete [O](85.23 s) sdiv_rdinp_passthrough.....................proved - complete [O]( 4.78 s) ddiv_rdinp_TCC1............................proved - complete [O]( 0.28 s) ddiv_rdinp_TCC2............................proved - complete [O]( 0.81 s) ddiv_rdinp_TCC3............................proved - complete [O]( 0.29 s) ddiv_rdinp_TCC4............................proved - complete [O]( 0.28 s) ddiv_rdinp_TCC5............................proved - complete [O]( 0.85 s) ddiv_rdinp_TCC6............................proved - complete [O]( 0.28 s) ddiv_rdinp_TCC7............................proved - complete [O]( 0.28 s) ddiv_rdinp_TCC8............................proved - complete [O]( 0.92 s) ddiv_rdinp_TCC9............................proved - complete [O]( 2.31 s) ddiv_rdinp_TCC10...........................proved - complete [O]( 0.29 s) ddiv_rdinp_TCC11...........................proved - complete [O]( 0.97 s) ddiv_rdinp_TCC12...........................proved - complete [O]( 0.29 s) ddiv_rdinp_TCC13...........................proved - complete [O]( 0.29 s) ddiv_rdinp.................................proved - complete [O](92.53 s) ddiv_rdinp_passthrough.....................proved - complete [O]( 7.33 s) Theory totals: 78 formulas, 78 attempted, 78 succeeded (572.09 s) Proof summary for theory md_unpack md_unpack_spec_TCC1.........................proved - complete [O](0.24 s) md_unpack_spec_TCC2.........................proved - complete [O](0.32 s) md_unpack_spec_TCC3.........................proved - complete [O](0.49 s) md_unpack_spec_TCC4.........................proved - complete [O](0.49 s) md_unpack_spec_TCC5.........................proved - complete [O](0.49 s) md_unpack_spec_TCC6.........................proved - complete [O](0.48 s) md_unpack_spec_TCC7.........................proved - complete [O](0.49 s) md_unpack_spec_TCC8.........................proved - complete [O](0.50 s) md_unpack_spec_TCC9.........................proved - complete [O](0.49 s) md_unpack_spec_TCC10........................proved - complete [O](0.49 s) md_unpack_spec_TCC11........................proved - complete [O](0.49 s) md_unpack_spec_TCC12........................proved - complete [O](0.49 s) md_unpack_spec_TCC13........................proved - complete [O](0.49 s) md_unpack_spec_TCC14........................proved - complete [O](0.49 s) md_unpack_spec_TCC15........................proved - complete [O](0.49 s) md_unpack_TCC1..............................proved - complete [O](1.11 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (8.04 s) Proof summary for theory ieee_md ieee_mul_thm_TCC1..........................proved - complete [O]( 1.82 s) ieee_mul_thm_TCC2..........................proved - complete [O]( 0.65 s) ieee_mul_thm...............................proved - complete [O](19.94 s) ieee_mul_range_TCC1........................proved - complete [O]( 1.18 s) ieee_mul_range_TCC2........................proved - complete [O]( 1.31 s) ieee_mul_range_TCC3........................proved - complete [O]( 0.41 s) ieee_mul_range.............................proved - complete [O]( 8.96 s) ieee_div_thm_TCC1..........................proved - complete [O]( 0.35 s) ieee_div_thm_TCC2..........................proved - complete [O]( 1.82 s) ieee_div_thm_TCC3..........................proved - complete [O]( 0.37 s) ieee_div_thm_TCC4..........................proved - complete [O]( 2.08 s) ieee_div_thm...............................proved - complete [O](17.15 s) ieee_div_range_TCC1........................proved - complete [O]( 1.09 s) ieee_div_range_TCC2........................proved - complete [O]( 4.34 s) ieee_div_range.............................proved - complete [O]( 8.75 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (70.22 s) Proof summary for theory md_stg2 md_stg2_TCC1...............................proved - complete [O](13.80 s) md_stg2_TCC2...............................proved - complete [O](13.77 s) div_stg12_it_TCC1..........................proved - complete [O]( 0.25 s) div_stg12_it_TCC2..........................proved - complete [O]( 0.26 s) div_stg12_it...............................proved - complete [O](12.80 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (40.88 s) Proof summary for theory md_stg1 md_stg1_TCC1................................proved - complete [O](0.45 s) md_stg1_TCC2................................proved - complete [O](0.54 s) md_stg1_TCC3................................proved - complete [O](0.62 s) md_stg1_TCC4................................proved - complete [O](0.71 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (2.32 s) Proof summary for theory exp_md md_add_lz_TCC1..............................proved - complete [O](0.31 s) md_add_lz_TCC2..............................proved - complete [O](0.31 s) exp_md_TCC1.................................proved - complete [O](0.42 s) exp_md_TCC2.................................proved - complete [O](0.46 s) exp_md_mul..................................proved - complete [O](5.25 s) exp_md_div..................................proved - complete [O](5.13 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (11.88 s) Proof summary for theory selfd_stg selfd_stg_TCC1..............................proved - complete [O](0.24 s) selfd_stg_TCC2..............................proved - complete [O](0.24 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.48 s) Proof summary for theory mul_div_comb mul_div_stage2_TCC1........................proved - complete [O]( 2.97 s) mul_div_stage2_TCC2........................proved - complete [O]( 3.07 s) mul_div_stage2_TCC3........................proved - complete [O]( 2.94 s) mul_div_stage2_TCC4........................proved - complete [O]( 2.94 s) mul_div_stage2_TCC5........................proved - complete [O]( 2.94 s) mul_div_stage2_TCC6........................proved - complete [O]( 2.94 s) mul_div_stage2_TCC7........................proved - complete [O]( 2.94 s) mul_div_stage2_TCC8........................proved - complete [O]( 2.94 s) mul_div_stage2_TCC9........................proved - complete [O]( 2.94 s) mul_div_stage2_TCC10.......................proved - complete [O]( 3.03 s) mul_div_stage2_x...........................proved - complete [O]( 3.47 s) mul_div_stage2_A...........................proved - complete [O]( 1.49 s) mul_div_stage2_E_sgl.......................proved - complete [O](10.79 s) mul_div_stage2_E_dbl.......................proved - complete [O]( 8.17 s) mul_div_stage2_Eb..........................proved - complete [O]( 4.01 s) div_comb_TCC1..............................proved - complete [O]( 0.29 s) div_comb_TCC2..............................proved - complete [O]( 0.24 s) div_comb_cor_TCC1..........................proved - complete [O]( 0.71 s) div_comb_cor_TCC2..........................proved - complete [O]( 0.47 s) div_comb_cor...............................proved - complete [O](23.76 s) div_comb_sgl_TCC1..........................proved - complete [O]( 0.89 s) div_comb_sgl_TCC2..........................proved - complete [O]( 0.93 s) div_comb_sgl...............................proved - complete [O]( 8.81 s) div_comb_dbl_TCC1..........................proved - complete [O]( 0.89 s) div_comb_dbl_TCC2..........................proved - complete [O]( 0.93 s) div_comb_dbl...............................proved - complete [O]( 5.32 s) div_comb_E_TCC1............................proved - complete [O]( 0.26 s) div_comb_E.................................proved - complete [O]( 0.81 s) div_comb_quot_sgl_TCC1.....................proved - complete [O]( 0.44 s) div_comb_quot_sgl_TCC2.....................proved - complete [O]( 0.44 s) div_comb_quot_sgl..........................proved - complete [O](41.88 s) div_comb_quot_dbl_TCC1.....................proved - complete [O]( 0.43 s) div_comb_quot_dbl_TCC2.....................proved - complete [O]( 0.45 s) div_comb_quot_dbl..........................proved - complete [O](37.36 s) mul_comb...................................proved - complete [O]( 6.77 s) Theory totals: 35 formulas, 35 attempted, 35 succeeded (189.66 s) Proof summary for theory multiplier58 mult_stg1_TCC1..............................proved - complete [O](0.24 s) mult_stg1_TCC2..............................proved - complete [O](0.24 s) mult_stg1_TCC3..............................proved - complete [O](0.26 s) mult58_correct..............................proved - complete [O](0.38 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.12 s) Proof summary for theory div_rep div_rep_comp_aux...........................proved - complete [O]( 0.32 s) div_rep_comp...............................proved - complete [O](13.65 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (13.97 s) Proof summary for theory div_initial IMP_newton_fin_TCC1........................proved - complete [O]( 0.91 s) reziprok_convex............................proved - complete [O]( 4.18 s) prod_pow_2_TCC1............................proved - complete [O]( 0.48 s) prod_pow_2_TCC2............................proved - complete [O]( 0.46 s) prod_pow_2.................................proved - complete [O]( 8.17 s) lookup_impl_TCC1...........................proved - complete [O]( 0.86 s) initial_impl_TCC1..........................proved - complete [O]( 0.29 s) initial_impl_TCC2..........................proved - complete [O]( 0.31 s) initial_ok_TCC1............................proved - complete [O]( 0.89 s) initial_ok_TCC2............................proved - complete [O]( 0.87 s) initial_ok_TCC3............................proved - complete [O]( 0.73 s) initial_ok_TCC4............................proved - complete [O]( 0.76 s) initial_ok.................................proved - complete [O](27.15 s) initial_ok2_TCC1...........................proved - complete [O]( 1.14 s) initial_ok2_TCC2...........................proved - complete [O]( 0.63 s) initial_ok2_TCC3...........................proved - complete [O]( 1.01 s) initial_ok2_TCC4...........................proved - complete [O]( 0.84 s) initial_ok2_TCC5...........................proved - complete [O]( 1.22 s) initial_ok2_TCC6...........................proved - complete [O]( 0.65 s) initial_ok2_TCC7...........................proved - complete [O]( 1.28 s) initial_ok2_TCC8...........................proved - complete [O]( 0.71 s) initial_ok2_TCC9...........................proved - complete [O]( 0.96 s) initial_ok2_TCC10..........................proved - complete [O]( 0.59 s) initial_ok2_TCC11..........................proved - complete [O]( 1.07 s) initial_ok2_TCC12..........................proved - complete [O]( 0.71 s) initial_ok2_TCC13..........................proved - complete [O]( 1.10 s) initial_ok2_TCC14..........................proved - complete [O]( 0.61 s) initial_ok2_TCC15..........................proved - complete [O]( 1.07 s) initial_ok2_TCC16..........................proved - complete [O]( 0.70 s) initial_ok2................................proved - complete [O](16.62 s) delta_bound_57_TCC1........................proved - complete [O]( 1.00 s) delta_bound_57_TCC2........................proved - complete [O]( 0.76 s) delta_bound_57_TCC3........................proved - complete [O]( 1.29 s) delta_bound_57_TCC4........................proved - complete [O]( 0.67 s) delta_bound_57_TCC5........................proved - complete [O]( 1.08 s) delta_bound_57_TCC6........................proved - complete [O]( 0.78 s) delta_bound_57_TCC7........................proved - complete [O]( 1.31 s) delta_bound_57_TCC8........................proved - complete [O]( 0.85 s) delta_bound_57_TCC9........................proved - complete [O]( 1.53 s) delta_bound_57_TCC10.......................proved - complete [O]( 0.68 s) delta_bound_57_TCC11.......................proved - complete [O]( 1.61 s) delta_bound_57_TCC12.......................proved - complete [O]( 0.62 s) delta_bound_57_TCC13.......................proved - complete [O]( 0.90 s) delta_bound_57_TCC14.......................proved - complete [O]( 0.70 s) delta_bound_57_TCC15.......................proved - complete [O]( 1.25 s) delta_bound_57_TCC16.......................proved - complete [O]( 0.74 s) delta_bound_57_TCC17.......................proved - complete [O]( 1.03 s) delta_bound_57_TCC18.......................proved - complete [O]( 0.52 s) delta_bound_57_TCC19.......................proved - complete [O]( 1.13 s) delta_bound_57_TCC20.......................proved - complete [O]( 0.52 s) delta_bound_57_TCC21.......................proved - complete [O]( 1.33 s) delta_bound_57_TCC22.......................proved - complete [O]( 0.53 s) delta_bound_57_TCC23.......................proved - complete [O]( 1.38 s) delta_bound_57_TCC24.......................proved - complete [O]( 0.54 s) delta_bound_57.............................proved - complete [O](18.06 s) Theory totals: 55 formulas, 55 attempted, 55 succeeded (117.78 s) Proof summary for theory mul_div_import Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory lookup lookup_div_TCC1...........................proved - complete [O]( 10.63 s) lookup_div_correct........................proved - complete [O](290.67 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (301.30 s) Proof summary for theory trunc minus_trunc.................................proved - complete [O](2.08 s) plus_trunc..................................proved - complete [O](2.06 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (4.14 s) Proof summary for theory newton_fin newton_x_TCC1..............................proved - complete [O]( 0.33 s) newton_x_TCC2..............................proved - complete [O]( 0.25 s) delta_bound_TCC1...........................proved - complete [O]( 0.56 s) delta_bound_TCC2...........................proved - complete [O]( 0.31 s) delta_bound................................proved - complete [O](14.07 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (15.52 s) Proof summary for theory select_fd select_fd_comp_TCC1........................proved - complete [O]( 0.32 s) select_fd_sum_sgl_TCC1.....................proved - complete [O]( 0.32 s) select_fd_sum_sgl..........................proved - complete [O](15.04 s) select_fd_sum_dbl_TCC1.....................proved - complete [O]( 0.31 s) select_fd_sum_dbl..........................proved - complete [O](13.50 s) select_fd_comp_gt_sgl......................proved - complete [O]( 4.84 s) select_fd_comp_gt_dbl......................proved - complete [O]( 4.86 s) select_fd_comp_eq_sgl......................proved - complete [O](11.67 s) select_fd_comp_eq_dbl......................proved - complete [O](11.83 s) select_fd_comp_gt..........................proved - complete [O]( 0.62 s) select_fd_E_TCC1...........................proved - complete [O]( 0.24 s) select_fd_E_TCC2...........................proved - complete [O]( 0.24 s) select_fd_E_TCC3...........................proved - complete [O]( 0.24 s) select_fd_E_TCC4...........................proved - complete [O]( 0.25 s) select_fd_E_sgl_TCC1.......................proved - complete [O]( 0.42 s) select_fd_E_sgl............................proved - complete [O]( 7.32 s) select_fd_E_dbl............................proved - complete [O]( 0.81 s) select_fd_TCC1.............................proved - complete [O]( 1.98 s) select_fd_TCC2.............................proved - complete [O]( 1.75 s) select_fd_TCC3.............................proved - complete [O]( 1.89 s) select_fd_TCC4.............................proved - complete [O]( 1.76 s) select_fd_TCC5.............................proved - complete [O]( 1.94 s) select_fd_TCC6.............................proved - complete [O]( 1.77 s) select_fd_sgl_TCC1.........................proved - complete [O]( 0.37 s) select_fd_sgl..............................proved - complete [O](29.51 s) select_fd_sgl_shift1_TCC1..................proved - complete [O]( 0.24 s) select_fd_sgl_shift1_TCC2..................proved - complete [O]( 0.25 s) select_fd_sgl_shift1_TCC3..................proved - complete [O]( 0.39 s) select_fd_sgl_shift1.......................proved - complete [O]( 5.02 s) select_fd_dbl_TCC1.........................proved - complete [O]( 0.37 s) select_fd_dbl..............................proved - complete [O](23.43 s) select_fd_dbl_shift1_TCC1..................proved - complete [O]( 0.24 s) select_fd_dbl_shift1_TCC2..................proved - complete [O]( 0.24 s) select_fd_dbl_shift1_TCC3..................proved - complete [O]( 0.39 s) select_fd_dbl_shift1.......................proved - complete [O]( 5.01 s) Theory totals: 35 formulas, 35 attempted, 35 succeeded (149.38 s) Proof summary for theory md_comb md_unimpl..................................proved - complete [O]( 4.92 s) md_SNANs...................................proved - complete [O]( 0.89 s) md_QNANs...................................proved - complete [O]( 1.56 s) md_SNANd...................................proved - complete [O]( 0.92 s) md_QNANd...................................proved - complete [O]( 1.49 s) md_inf_times_zero_s........................proved - complete [O]( 0.95 s) md_inf_times_fininf_s......................proved - complete [O]( 0.81 s) md_zero_times_finzero_s....................proved - complete [O]( 1.04 s) md_inf_times_zero_d........................proved - complete [O]( 0.92 s) md_inf_times_fininf_d......................proved - complete [O]( 0.92 s) md_zero_times_finzero_d....................proved - complete [O]( 0.91 s) md_infz_div_infz_s.........................proved - complete [O]( 0.88 s) md_div_resinf_s............................proved - complete [O]( 0.91 s) md_fin_div_z_s.............................proved - complete [O]( 0.74 s) md_div_reszero_s...........................proved - complete [O]( 0.99 s) md_infz_div_infz_d.........................proved - complete [O]( 0.88 s) md_div_resinf_d............................proved - complete [O]( 0.76 s) md_fin_div_z_d.............................proved - complete [O]( 1.02 s) md_div_reszero_d...........................proved - complete [O]( 0.80 s) md_special.................................proved - complete [O]( 0.59 s) smul_rdinp_TCC1............................proved - complete [O]( 0.91 s) smul_rdinp_TCC2............................proved - complete [O]( 0.57 s) smul_rdinp_TCC3............................proved - complete [O]( 0.70 s) smul_rdinp_TCC4............................proved - complete [O]( 0.92 s) smul_rdinp_TCC5............................proved - complete [O]( 0.97 s) smul_rdinp_TCC6............................proved - complete [O]( 1.17 s) smul_rdinp.................................proved - complete [O](10.36 s) dmul_rdinp_TCC1............................proved - complete [O]( 0.81 s) dmul_rdinp_TCC2............................proved - complete [O]( 0.64 s) dmul_rdinp_TCC3............................proved - complete [O]( 0.66 s) dmul_rdinp_TCC4............................proved - complete [O]( 1.08 s) dmul_rdinp_TCC5............................proved - complete [O]( 0.87 s) dmul_rdinp_TCC6............................proved - complete [O]( 1.01 s) dmul_rdinp.................................proved - complete [O]( 8.92 s) sdiv_rdinp_TCC1............................proved - complete [O]( 0.83 s) sdiv_rdinp_TCC2............................proved - complete [O]( 0.83 s) sdiv_rdinp_TCC3............................proved - complete [O]( 0.78 s) sdiv_rdinp_TCC4............................proved - complete [O]( 1.53 s) sdiv_rdinp_TCC5............................proved - complete [O]( 1.27 s) sdiv_rdinp_TCC6............................proved - complete [O]( 1.18 s) sdiv_rdinp_TCC7............................proved - complete [O]( 0.53 s) sdiv_rdinp.................................proved - complete [O](10.58 s) ddiv_rdinp_TCC1............................proved - complete [O]( 0.66 s) ddiv_rdinp_TCC2............................proved - complete [O]( 0.59 s) ddiv_rdinp_TCC3............................proved - complete [O]( 0.59 s) ddiv_rdinp_TCC4............................proved - complete [O]( 0.97 s) ddiv_rdinp_TCC5............................proved - complete [O]( 0.82 s) ddiv_rdinp_TCC6............................proved - complete [O]( 0.82 s) ddiv_rdinp_TCC7............................proved - complete [O]( 0.37 s) ddiv_rdinp.................................proved - complete [O](11.29 s) md_double_flag.............................proved - complete [O]( 5.72 s) Theory totals: 51 formulas, 51 attempted, 51 succeeded (91.85 s) Proof summary for theory mul_div Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Grand Totals: 323 proofs, 323 attempted, 323 succeeded (1592.82 s)