nasalib.grandtotals

Processing ints. Writing output to file summaries/ints.summary
Logging PVS information in summaries/ints.log
Grand Totals: 404 proofs, 404 attempted, 404 succeeded (0.07 s)

Processing structures. Writing output to file summaries/structures.summary
Logging PVS information in summaries/structures.log
Grand Totals: 1291 proofs, 1291 attempted, 1291 succeeded (0.29 s)

Processing reals. Writing output to file summaries/reals.summary
Logging PVS information in summaries/reals.log
 Proof summary for theory best_rational
    frac_nn_int_TCC11.....................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 38 formulas, 38 attempted, 37 succeeded (0.02 s)
Grand Totals: 1781 proofs, 1781 attempted, 1780 succeeded (0.89 s)
*** Warning: Missed 1 formula.

Processing orders. Writing output to file summaries/orders.summary
Logging PVS information in summaries/orders.log
Grand Totals: 818 proofs, 818 attempted, 818 succeeded (0.14 s)

Processing analysis. Writing output to file summaries/analysis.summary
Logging PVS information in summaries/analysis.log
 Proof summary for theory integral_split
    partition_join........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 15 formulas, 15 attempted, 14 succeeded (0.02 s)
Grand Totals: 1625 proofs, 1625 attempted, 1624 succeeded (0.80 s)
*** Warning: Missed 1 formula.

Processing sets_aux. Writing output to file summaries/sets_aux.summary
Logging PVS information in summaries/sets_aux.log
Grand Totals: 467 proofs, 467 attempted, 467 succeeded (0.09 s)

Processing numbers. Writing output to file summaries/numbers.summary
Logging PVS information in summaries/numbers.log
Grand Totals: 143 proofs, 143 attempted, 143 succeeded (0.11 s)

Processing series. Writing output to file summaries/series.summary
Logging PVS information in summaries/series.log
Grand Totals: 315 proofs, 315 attempted, 315 succeeded (0.14 s)

Processing trig. Writing output to file summaries/trig.summary
Logging PVS information in summaries/trig.log
Grand Totals: 1080 proofs, 1080 attempted, 1080 succeeded (0.84 s)

Processing vectors. Writing output to file summaries/vectors.summary
Logging PVS information in summaries/vectors.log
Grand Totals: 1483 proofs, 1483 attempted, 1483 succeeded (0.35 s)

Processing sigma_set. Writing output to file summaries/sigma_set.summary
Logging PVS information in summaries/sigma_set.log
 Proof summary for theory sigma_bijection_nat
    series_bijection......................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 2 formulas, 2 attempted, 1 succeeded (0.00 s)
Grand Totals: 166 proofs, 166 attempted, 165 succeeded (0.09 s)
*** Warning: Missed 1 formula.

Processing algebra. Writing output to file summaries/algebra.summary
Logging PVS information in summaries/algebra.log
 Proof summary for theory chinese_remainder_theorem_Z
    Chinese_Remainder_Theorem_for_int.....unfinished          [SHOSTAK](0.00 s)
    Theory totals: 16 formulas, 16 attempted, 15 succeeded (0.01 s)
Grand Totals: 1306 proofs, 1306 attempted, 1304 succeeded (0.66 s)
*** Warning: Missed 2 formulas.

Processing vect_analysis. Writing output to file summaries/vect_analysis.summary
Logging PVS information in summaries/vect_analysis.log
 Proof summary for theory deriv_cont_2D
    derivable_rv_cont_rv..................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 3 formulas, 3 attempted, 2 succeeded (0.00 s)
 Proof summary for theory cont_real_vect2
    continuous_iff_comps..................unfinished          [SHOSTAK](0.00 s)
    cont_rv_iff_comps.....................unfinished          [SHOSTAK](0.00 s)
    scal_continuous_rv....................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 22 formulas, 22 attempted, 19 succeeded (0.00 s)
Grand Totals: 551 proofs, 551 attempted, 547 succeeded (0.08 s)
*** Warning: Missed 4 formulas.

Processing lnexp. Writing output to file summaries/lnexp.summary
Logging PVS information in summaries/lnexp.log
 Proof summary for theory expt
    hathat_cross..........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 41 formulas, 41 attempted, 40 succeeded (0.00 s)
 Proof summary for theory exp_series
    exp_est_is_nat........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 23 formulas, 23 attempted, 22 succeeded (0.01 s)
Grand Totals: 532 proofs, 532 attempted, 530 succeeded (0.33 s)
*** Warning: Missed 2 formulas.

Processing power. Writing output to file summaries/power.summary
Logging PVS information in summaries/power.log
 Proof summary for theory ln_exp_def
    log_derivable_TCC1....................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 17 formulas, 17 attempted, 16 succeeded (0.01 s)
Grand Totals: 307 proofs, 307 attempted, 306 succeeded (0.06 s)
*** Warning: Missed 1 formula.

Processing interval_arith. Writing output to file summaries/interval_arith.summary
Logging PVS information in summaries/interval_arith.log
 Proof summary for theory interval_expr
    eval_vs_idempotence...................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 93 formulas, 93 attempted, 92 succeeded (0.03 s)
 Proof summary for theory numerical_bandb
    mindir_maxvar_aux_TCC1................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 25 formulas, 25 attempted, 24 succeeded (0.02 s)
 Proof summary for theory subinterval_deriv
    subinterval_deriv.....................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 5 formulas, 5 attempted, 4 succeeded (0.00 s)
Grand Totals: 884 proofs, 884 attempted, 881 succeeded (0.32 s)
*** Warning: Missed 3 formulas.

Processing affine_arith. Writing output to file summaries/affine_arith.summary
Logging PVS information in summaries/affine_arith.log
    ErrorTerms_TCC1.......................proved - complete   [SHOSTAK](0.00 s)
    null_is_ErrorTerms....................proved - incomplete [SHOSTAK](0.00 s)
Grand Totals: 835 proofs, 835 attempted, 835 succeeded (1.46 s)

Processing matrices. Writing output to file summaries/matrices.summary
Logging PVS information in summaries/matrices.log
Grand Totals: 526 proofs, 526 attempted, 526 succeeded (0.32 s)

Processing Bernstein. Writing output to file summaries/Bernstein.summary
Logging PVS information in summaries/Bernstein.log
Grand Totals: 310 proofs, 310 attempted, 310 succeeded (0.14 s)

Processing Sturm. Writing output to file summaries/Sturm.summary
Logging PVS information in summaries/Sturm.log

Processing Tarski. Writing output to file summaries/Tarski.summary
Logging PVS information in summaries/Tarski.log
Grand Totals: 515 proofs, 515 attempted, 515 succeeded (0.52 s)

Processing MetiTarski. Writing output to file summaries/MetiTarski.summary
Logging PVS information in summaries/MetiTarski.log
 Proof summary for theory metit_examples
    simple................................unfinished          [SHOSTAK](0.00 s)
    simple_abs............................unfinished          [SHOSTAK](0.00 s)
    sqrtx3................................unfinished          [SHOSTAK](0.00 s)
    tr_35_TCC1............................unfinished          [SHOSTAK](0.00 s)
    tr_35.................................unfinished          [SHOSTAK](0.00 s)
    tr_35_le_TCC1.........................unfinished          [SHOSTAK](0.00 s)
    tr_35_le..............................unfinished          [SHOSTAK](0.00 s)
    sqrt23................................unfinished          [SHOSTAK](0.00 s)
    sin6sqrt2.............................unfinished          [SHOSTAK](0.00 s)
    A_and_S...............................unfinished          [SHOSTAK](0.00 s)
    atan_implementation...................unfinished          [SHOSTAK](0.00 s)
    ajn...................................unfinished          [SHOSTAK](0.00 s)
    double_quad_simple_min................unfinished          [SHOSTAK](0.00 s)
    ex1_ba................................unfinished          [SHOSTAK](0.00 s)
    ex2_ba................................unfinished          [SHOSTAK](0.00 s)
    ex3_ba................................unfinished          [SHOSTAK](0.00 s)
    ex4_ba................................unfinished          [SHOSTAK](0.00 s)
    ex5_ba................................unfinished          [SHOSTAK](0.00 s)
    ex6_ba................................unfinished          [SHOSTAK](0.00 s)
    ex7_ba................................unfinished          [SHOSTAK](0.00 s)
    quadratic.............................unfinished          [SHOSTAK](0.00 s)
    Tunnel_3_IL...........................unfinished          [SHOSTAK](0.00 s)
    Tunnel_3_IL_LU........................unfinished          [SHOSTAK](0.00 s)
    Ayad_Marche...........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 33 formulas, 33 attempted, 9 succeeded (0.00 s)
Grand Totals: 33 proofs, 33 attempted, 9 succeeded (0.00 s)
*** Warning: Missed 24 formulas.

Processing fast_approx. Writing output to file summaries/fast_approx.summary
Logging PVS information in summaries/fast_approx.log
 Proof summary for theory fast_approx
    tan_pos_TCC2..........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 61 formulas, 61 attempted, 60 succeeded (0.04 s)
 Proof summary for theory tan_props
    tan_fast_approx_bound.................unfinished          [SHOSTAK](0.02 s)
    Theory totals: 3 formulas, 3 attempted, 2 succeeded (0.03 s)
Grand Totals: 172 proofs, 172 attempted, 170 succeeded (0.20 s)
*** Warning: Missed 2 formulas.

Processing shapes. Writing output to file summaries/shapes.summary
Logging PVS information in summaries/shapes.log
 Proof summary for theory rectangle_2D
    point_in_rectangle_eq.................unfinished          [SHOSTAK](0.01 s)
    point_strictly_in_rectangle_eq........unfinished          [SHOSTAK](0.01 s)
    Theory totals: 26 formulas, 26 attempted, 24 succeeded (0.04 s)
Grand Totals: 130 proofs, 130 attempted, 128 succeeded (0.11 s)
*** Warning: Missed 2 formulas.

Processing complex. Writing output to file summaries/complex.summary
Logging PVS information in summaries/complex.log
 Proof summary for theory complex_types
    closed_neg............................unfinished          [SHOSTAK](0.00 s)
    closed_times..........................unfinished          [SHOSTAK](0.00 s)
    closed_divides........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 21 formulas, 21 attempted, 18 succeeded (0.00 s)
 Proof summary for theory number_fields_bis
    nznum_times_nznum_is_nznum............unfinished          [SHOSTAK](0.00 s)
    minus_nznum_is_nznum..................unfinished          [SHOSTAK](0.00 s)
    both_sides_times1.....................unfinished          [SHOSTAK](0.00 s)
    inv_ne_0..............................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 50 formulas, 50 attempted, 46 succeeded (0.01 s)
 Proof summary for theory exp
    ln_exp................................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 22 formulas, 22 attempted, 21 succeeded (0.01 s)
Grand Totals: 248 proofs, 248 attempted, 240 succeeded (0.10 s)
*** Warning: Missed 8 formulas.

Processing digraphs. Writing output to file summaries/digraphs.summary
Logging PVS information in summaries/digraphs.log
Grand Totals: 789 proofs, 789 attempted, 789 succeeded (0.52 s)

Processing float/axm_bnd. Writing output to file summaries/float-axm_bnd.summary
Logging PVS information in summaries/float-axm_bnd.log
 Proof summary for theory ieee754_domain
    zero_is_er............................unfinished          [SHOSTAK](0.00 s)
    ulp_TCC4..............................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 36 formulas, 36 attempted, 34 succeeded (0.01 s)
 Proof summary for theory ieee754_qlt
    qlt_finite_def........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 1 formulas, 1 attempted, 0 succeeded (0.00 s)
 Proof summary for theory ieee754_qle
    qle_finite_def........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 1 formulas, 1 attempted, 0 succeeded (0.00 s)
 Proof summary for theory ieee754_qgt
    qgt_finite_def........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 1 formulas, 1 attempted, 0 succeeded (0.00 s)
 Proof summary for theory ieee754_qge
    qge_finite_def........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 1 formulas, 1 attempted, 0 succeeded (0.00 s)
 Proof summary for theory ieee754_qeq
    qeq_finite_def........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 1 formulas, 1 attempted, 0 succeeded (0.00 s)
 Proof summary for theory ieee754_add
    add_finite_def........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 3 formulas, 3 attempted, 2 succeeded (0.00 s)
 Proof summary for theory ieee754_sub
    sub_finite_def........................unfinished          [SHOSTAK](0.00 s)
    finite?_projs_finite?_sub.............unfinished          [SHOSTAK](0.00 s)
    Theory totals: 4 formulas, 4 attempted, 2 succeeded (0.01 s)
 Proof summary for theory ieee754_mul
    mul_finite_def........................unfinished          [SHOSTAK](0.00 s)
    finite?_projs_finite?_mul.............unfinished          [SHOSTAK](0.00 s)
    Theory totals: 3 formulas, 3 attempted, 1 succeeded (0.02 s)
 Proof summary for theory ieee754_div
    finite?_projs_finite?_div.............unfinished          [SHOSTAK](0.00 s)
    Theory totals: 6 formulas, 6 attempted, 5 succeeded (0.01 s)
Grand Totals: 138 proofs, 138 attempted, 125 succeeded (0.06 s)
*** Warning: Missed 13 formulas.

Processing float/fnd_bnd. Writing output to file summaries/float-fnd_bnd.summary
Logging PVS information in summaries/float-fnd_bnd.log
 Proof summary for theory extended_float_exactly_representable_reals
    er_rat_to_er_int__significand_TCC1....unfinished          [SHOSTAK](0.00 s)
    er_rat_to_er_int__significand_TCC4....unfinished          [SHOSTAK](0.00 s)
    er_rat_to_er_int__significand__abs_lt_radix_pow_prec...unfinished          [SHOSTAK](0.00 s)
    er_rat_to_er_int_value................unfinished          [SHOSTAK](0.00 s)
    er_ub_correspondent...................unfinished          [SHOSTAK](0.00 s)
    er_min_pos_correspondent..............unfinished          [SHOSTAK](0.00 s)
    er_rat_er_int.........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 19 formulas, 19 attempted, 12 succeeded (0.01 s)
 Proof summary for theory domain_equivalence
    axm_ulp_fnd_ulp_pos...................unfinished          [SHOSTAK](0.01 s)
    axm_ulp_fnd_ulp.......................unfinished          [SHOSTAK](0.01 s)
    Theory totals: 4 formulas, 4 attempted, 2 succeeded (0.01 s)
Grand Totals: 190 proofs, 190 attempted, 180 succeeded (0.11 s)
*** Warning: Missed 10 formulas.

Processing float/fnd_unb. Writing output to file summaries/float-fnd_unb.summary
Logging PVS information in summaries/float-fnd_unb.log
*** Error: There is no applicable method for the generic function
*** Error occurred while typechecking ieee754sp

Processing float/ieee854. Writing output to file summaries/float-ieee854.summary
Logging PVS information in summaries/float-ieee854.log
*** Error: Cannot find theory float[radix]
*** Error occurred while typechecking mod_lems

Processing fault_tolerance. Writing output to file summaries/fault_tolerance.summary
Logging PVS information in summaries/fault_tolerance.log
Grand Totals: 585 proofs, 585 attempted, 585 succeeded (0.12 s)

Processing graphs. Writing output to file summaries/graphs.summary
Logging PVS information in summaries/graphs.log
Grand Totals: 792 proofs, 792 attempted, 792 succeeded (0.35 s)

Processing PVSioChecker. Writing output to file summaries/PVSioChecker.summary
Logging PVS information in summaries/PVSioChecker.log
Grand Totals: 39 proofs, 39 attempted, 39 succeeded (0.00 s)

Processing LTL. Writing output to file summaries/LTL.summary
Logging PVS information in summaries/LTL.log
Grand Totals: 163 proofs, 163 attempted, 163 succeeded (0.08 s)

Processing exact_real_arith. Writing output to file summaries/exact_real_arith.summary
Logging PVS information in summaries/exact_real_arith.log

Processing aviation. Writing output to file summaries/aviation.summary
Logging PVS information in summaries/aviation.log
 Proof summary for theory error_proj
    error_valid_simple_def................unfinished          [SHOSTAK](0.01 s)
    error_valid_simple_edgebound_def......unfinished          [SHOSTAK](0.01 s)
    sphere_to_2D_plane_error_simple_27780...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_1852...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_3704...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_5556...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_7408...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_9260...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_11112...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_12964...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_14816...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_16668...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_18520...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_20372...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_22224...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_24076...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_25928...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_37040...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_46300...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_55560...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_64820...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_74080...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_83340...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_92600...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_111120...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_129640...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_148160...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_166680...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_185200...unfinished          [SHOSTAK](0.00 s)
    sphere_to_2D_plane_error_simple_185200_27780...unfinished          [SHOSTAK](0.01 s)
    Theory totals: 70 formulas, 70 attempted, 40 succeeded (0.14 s)
Grand Totals: 514 proofs, 514 attempted, 484 succeeded (0.78 s)
*** Warning: Missed 30 formulas.

Processing ACCoRD. Writing output to file summaries/ACCoRD.summary
Logging PVS information in summaries/ACCoRD.log

Processing sorting. Writing output to file summaries/sorting.summary
Logging PVS information in summaries/sorting.log
 Proof summary for theory firt_phase_ford_johnson
    comparePeservesElements...............unfinished          [SHOSTAK](0.01 s)
    Theory totals: 37 formulas, 37 attempted, 36 succeeded (0.02 s)
Grand Totals: 652 proofs, 652 attempted, 651 succeeded (0.35 s)
*** Warning: Missed 1 formula.

Processing TRS. Writing output to file summaries/TRS.summary
Logging PVS information in summaries/TRS.log
 Proof summary for theory substitution
    SigmaP_equivalence_TCC1...............unfinished          [SHOSTAK](0.00 s)
    SigmaP_equivalence_TCC2...............unfinished          [SHOSTAK](0.00 s)
    SigmaP_equivalence....................unfinished          [SHOSTAK](0.00 s)
    SigmaP_vs_replaceTerm_linearR_TCC3....unfinished          [SHOSTAK](0.00 s)
    SigmaP_vs_replaceTerm_linearR_TCC4....unfinished          [SHOSTAK](0.00 s)
    SigmaP_vs_replaceTerm_linearR.........unfinished          [SHOSTAK](0.00 s)
    Theory totals: 94 formulas, 94 attempted, 88 succeeded (0.05 s)
 Proof summary for theory replacement
    equality_replaceTerm..................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 30 formulas, 30 attempted, 29 succeeded (0.02 s)
 Proof summary for theory subterm
    Var_occurs_only_once_TCC1.............unfinished          [SHOSTAK](0.00 s)
    Var_occurs_only_once..................unfinished          [SHOSTAK](0.00 s)
    Var_occurs_only_once_also_in_subterms_TCC1...unfinished          [SHOSTAK](0.00 s)
    Var_occurs_only_once_also_in_subterms...unfinished          [SHOSTAK](0.00 s)
    equal_subterms_equal_term.............unfinished          [SHOSTAK](0.00 s)
    length_comp_p.........................unfinished          [SHOSTAK](0.00 s)
    m_neq_n...............................unfinished          [SHOSTAK](0.00 s)
    term_eq_subterm.......................unfinished          [SHOSTAK](0.00 s)
    app_term..............................unfinished          [SHOSTAK](0.00 s)
    positions_of_a_term...................unfinished          [SHOSTAK](0.00 s)
    equal_term_TCC1.......................unfinished          [SHOSTAK](0.00 s)
    equal_term_TCC2.......................unfinished          [SHOSTAK](0.00 s)
    equal_term............................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 59 formulas, 59 attempted, 46 succeeded (0.02 s)
 Proof summary for theory positions
    pos_ax................................unfinished          [SHOSTAK](0.00 s)
    parallel_pos_same_prefix..............unfinished          [SHOSTAK](0.00 s)
    comp_preservs_parallel_pos2...........unfinished          [SHOSTAK](0.00 s)
    comp_preservs_parallel_pos3...........unfinished          [SHOSTAK](0.00 s)
    parallel_pos_are_dif..................unfinished          [SHOSTAK](0.00 s)
    comp_SPP_commute......................unfinished          [SHOSTAK](0.00 s)
    left_pos_transitive...................unfinished          [SHOSTAK](0.00 s)
    lwc_transitive........................unfinished          [SHOSTAK](0.00 s)
    subterm_if_le_arity...................unfinished          [SHOSTAK](0.00 s)
    subterms_acc_arity....................unfinished          [SHOSTAK](0.00 s)
    lwc_add_last_delete_TCC1..............unfinished          [SHOSTAK](0.00 s)
    lwc_add_last_delete_TCC2..............unfinished          [SHOSTAK](0.00 s)
    lwc_add_last_delete...................unfinished          [SHOSTAK](0.00 s)
    lwc_add_last_delete1_TCC1.............unfinished          [SHOSTAK](0.00 s)
    lwc_add_last_delete1..................unfinished          [SHOSTAK](0.00 s)
    leftmost_pos..........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 46 formulas, 46 attempted, 30 succeeded (0.01 s)
 Proof summary for theory confluence_commute
    RC_o_RTC_is_RTC.......................unfinished          [SHOSTAK](0.00 s)
    RTC_converse_RTC_R....................unfinished          [SHOSTAK](0.00 s)
    semi_comm_implies_comm................unfinished          [SHOSTAK](0.00 s)
    conf_local_request_implies_request....unfinished          [SHOSTAK](0.00 s)
    hip_Hindley_implies_semi_comm.........unfinished          [SHOSTAK](0.00 s)
    ref_condition_to_refcomp..............unfinished          [SHOSTAK](0.00 s)
    semi_implies_CR.......................unfinished          [SHOSTAK](0.00 s)
    semi_implies_conf.....................unfinished          [SHOSTAK](0.00 s)
    sub_comm_implies_semi_conf............unfinished          [SHOSTAK](0.00 s)
    lemma_Rosen_1973......................unfinished          [SHOSTAK](0.00 s)
    lcomm_and_snunion_implies_comm........unfinished          [SHOSTAK](0.00 s)
    UN_implies_UNseta.....................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 23 formulas, 23 attempted, 11 succeeded (0.01 s)
 Proof summary for theory unification
    uni_diff_equal_length_arg.............unfinished          [SHOSTAK](0.00 s)
    resolving_diff_TCC3...................unfinished          [SHOSTAK](0.00 s)
    resolving_diff_TCC5...................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 57 formulas, 57 attempted, 54 succeeded (0.04 s)
 Proof summary for theory orthogonality_basis
    D_TCC1................................unfinished          [SHOSTAK](0.00 s)
    G_TCC1................................unfinished          [SHOSTAK](0.00 s)
    linear?_TCC1..........................unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_TCC3..................unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_TCC5..................unfinished          [SHOSTAK](0.00 s)
    subtermsOF_TCC1.......................unfinished          [SHOSTAK](0.00 s)
    complement_pos_character..............unfinished          [SHOSTAK](0.00 s)
    complement_pos_is_PP..................unfinished          [SHOSTAK](0.00 s)
    complement_pos_empty..................unfinished          [SHOSTAK](0.00 s)
    comp_pos_rest.........................unfinished          [SHOSTAK](0.00 s)
    comp_pos_preservs_length..............unfinished          [SHOSTAK](0.00 s)
    comp_pos_character_TCC1...............unfinished          [SHOSTAK](0.00 s)
    comp_pos_is_PP........................unfinished          [SHOSTAK](0.00 s)
    comp_pos_in_PP_preservs_PP............unfinished          [SHOSTAK](0.00 s)
    subtermsOF_rest.......................unfinished          [SHOSTAK](0.00 s)
    Orth_lemma_aux........................unfinished          [SHOSTAK](0.00 s)
    Linear_and_Non_ambiguous_implies_sub_comm...unfinished          [SHOSTAK](0.00 s)
    parallel_reduction_inclusion..........unfinished          [SHOSTAK](0.00 s)
    parallel_reduction_RTC................unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_preservs_pos..........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_preservs_PP_o_PP_TCC1...unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_equivalence_TCC3......unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_equivalence_TCC6......unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_equivalence...........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_equivalence1_TCC3.....unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_equivalence1..........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_preservs_subterm......unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_comp_TCC2.............unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_comp_TCC3.............unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_comp..................unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_comp_commute_TCC1.....unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_comp_commute..........unfinished          [SHOSTAK](0.00 s)
    replace_replace_par_pos_TCC1..........unfinished          [SHOSTAK](0.00 s)
    comp_pos_in_SP_preservs_SP_in_replace...unfinished          [SHOSTAK](0.00 s)
    comp_pos_in_SPP_preservs_SPP_in_replace_par_pos...unfinished          [SHOSTAK](0.00 s)
    parallel_reduction_reflexive..........unfinished          [SHOSTAK](0.00 s)
    non_ambiguous_implies_same_term.......unfinished          [SHOSTAK](0.00 s)
    parallel_reduction_context_aux........unfinished          [SHOSTAK](0.00 s)
    parallel_reduction_context............unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_of_app_is_app.........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_preservs_f_TCC1.......unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_preservs_f............unfinished          [SHOSTAK](0.00 s)
    parallel_reduction_variables_context...unfinished          [SHOSTAK](0.00 s)
    parallel_reduction_result.............unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_subterm2_TCC2.........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_subterm2_TCC3.........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_subterm2_TCC4.........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_subterm2..............unfinished          [SHOSTAK](0.00 s)
    parallel_reduction_variables..........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_dominance_TCC1........unfinished          [SHOSTAK](0.00 s)
    replace_par_pos_dominance.............unfinished          [SHOSTAK](0.00 s)
    Parallel_Moves_Lemma..................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 104 formulas, 104 attempted, 52 succeeded (0.06 s)
 Proof summary for theory predicate_fseq2set
    seq2set_comp..........................unfinished          [SHOSTAK](0.00 s)
    subseq_rest...........................unfinished          [SHOSTAK](0.00 s)
    subset_empty_seq......................unfinished          [SHOSTAK](0.00 s)
    seq_construct1........................unfinished          [SHOSTAK](0.00 s)
    seq_construct2........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 58 formulas, 58 attempted, 53 succeeded (0.01 s)
 Proof summary for theory inn_dp_termination
    mint_is_nr_inn_terminating............unfinished          [SHOSTAK](0.00 s)
    Theory totals: 56 formulas, 56 attempted, 55 succeeded (0.17 s)
Grand Totals: 1047 proofs, 1047 attempted, 938 succeeded (1.09 s)
*** Warning: Missed 109 formulas.

Processing CCG. Writing output to file summaries/CCG.summary
Logging PVS information in summaries/CCG.log
Grand Totals: 348 proofs, 348 attempted, 348 succeeded (0.99 s)

Processing PVS0. Writing output to file summaries/PVS0.summary
Logging PVS information in summaries/PVS0.log
Grand Totals: 667 proofs, 667 attempted, 667 succeeded (0.54 s)

Processing Riemann. Writing output to file summaries/Riemann.summary
Logging PVS information in summaries/Riemann.log
Grand Totals: 93 proofs, 93 attempted, 93 succeeded (0.08 s)

Processing examples. Writing output to file summaries/examples.summary
Logging PVS information in summaries/examples.log
*** Error reading proof file /Users/mmoscato/nasa/pvslib/pvslib-gitlab-pvs-8.0-fixes/examples/hutch_examples.prf:
*** Error reading proof file /Users/mmoscato/nasa/pvslib/pvslib-gitlab-pvs-8.0-fixes/examples/hutch_examples.prf:
*** Error reading proof file /Users/mmoscato/nasa/pvslib/pvslib-gitlab-pvs-8.0-fixes/examples/hutch_examples.prf:
*** Error: Value of PRECISION in (/ PRECISION 3.322) is 210_TCC1, not a NUMBER. (examples)
*** Error occurred while rerunning proof of era_examples.sqrt2_num_b210_TCC1

Processing topology. Writing output to file summaries/topology.summary
Logging PVS information in summaries/topology.log
Grand Totals: 143 proofs, 143 attempted, 143 succeeded (0.02 s)

Processing complex_alt. Writing output to file summaries/complex_alt.summary
Logging PVS information in summaries/complex_alt.log
Grand Totals: 373 proofs, 373 attempted, 373 succeeded (0.17 s)

Processing scott. Writing output to file summaries/scott.summary
Logging PVS information in summaries/scott.log
Grand Totals: 72 proofs, 72 attempted, 72 succeeded (0.02 s)

Processing while. Writing output to file summaries/while.summary
Logging PVS information in summaries/while.log
Grand Totals: 154 proofs, 154 attempted, 154 succeeded (0.09 s)

Processing extended_nnreal. Writing output to file summaries/extended_nnreal.summary
Logging PVS information in summaries/extended_nnreal.log
Grand Totals: 74 proofs, 74 attempted, 74 succeeded (0.02 s)

Processing metric_space. Writing output to file summaries/metric_space.summary
Logging PVS information in summaries/metric_space.log
Grand Totals: 147 proofs, 147 attempted, 147 succeeded (0.13 s)

Processing measure_integration. Writing output to file summaries/measure_integration.summary
Logging PVS information in summaries/measure_integration.log

Processing complex_integration. Writing output to file summaries/complex_integration.summary
Logging PVS information in summaries/complex_integration.log
Grand Totals: 178 proofs, 178 attempted, 178 succeeded (0.21 s)

Processing lebesgue. Writing output to file summaries/lebesgue.summary
Logging PVS information in summaries/lebesgue.log

Processing probability. Writing output to file summaries/probability.summary
Logging PVS information in summaries/probability.log
Grand Totals: 72 proofs, 72 attempted, 72 succeeded (0.08 s)

Processing co_structures. Writing output to file summaries/co_structures.summary
Logging PVS information in summaries/co_structures.log
Grand Totals: 726 proofs, 726 attempted, 726 succeeded (0.15 s)

Processing TU_Games. Writing output to file summaries/TU_Games.summary
Logging PVS information in summaries/TU_Games.log
 Proof summary for theory tu_game
    COV_core..............................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 14 formulas, 14 attempted, 13 succeeded (0.00 s)
Grand Totals: 24 proofs, 24 attempted, 23 succeeded (0.00 s)
*** Warning: Missed 1 formula.

Processing linear_algebra. Writing output to file summaries/linear_algebra.summary
Logging PVS information in summaries/linear_algebra.log
 Proof summary for theory elementary_matrices
    elem_product_left_TCC2................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 53 formulas, 53 attempted, 52 succeeded (0.03 s)
Grand Totals: 450 proofs, 450 attempted, 449 succeeded (0.16 s)
*** Warning: Missed 1 formula.

Processing ASP. Writing output to file summaries/ASP.summary
Logging PVS information in summaries/ASP.log
 Proof summary for theory Sig_prop
    RT_classic............................unfinished          [SHOSTAK](0.00 s)
    RT_ord_uniq...........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 56 formulas, 56 attempted, 54 succeeded (0.01 s)
Grand Totals: 110 proofs, 110 attempted, 108 succeeded (0.03 s)
*** Warning: Missed 2 formulas.

Processing line_segments. Writing output to file summaries/line_segments.summary
Logging PVS information in summaries/line_segments.log
*** Error: Invalid index 1 for (SIMPLE-VECTOR 1), should be a non-negative integer below 1.*** Error occurred while typechecking quad_minmax

Processing polygons. Writing output to file summaries/polygons.summary
Logging PVS information in summaries/polygons.log
*** Error: Invalid index 1 for (SIMPLE-VECTOR 1), should be a non-negative integer below 1.*** Error occurred while typechecking vertex_list

Processing polygon_merge. Writing output to file summaries/polygon_merge.summary
Logging PVS information in summaries/polygon_merge.log
*** Error: Invalid index 1 for (SIMPLE-VECTOR 1), should be a non-negative integer below 1.*** Error occurred while typechecking vertex_list

Processing mv_analysis. Writing output to file summaries/mv_analysis.summary
Logging PVS information in summaries/mv_analysis.log
 Proof summary for theory vector_arithmetic
    zero_cdr..............................unfinished          [SHOSTAK](0.00 s)
    add_zero_imp_eq.......................unfinished          [SHOSTAK](0.00 s)
    neg_1.................................unfinished          [SHOSTAK](0.00 s)
    quad_move.............................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 129 formulas, 129 attempted, 125 succeeded (0.04 s)
 Proof summary for theory norms
    abs_max_lists.........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 70 formulas, 70 attempted, 69 succeeded (0.03 s)
 Proof summary for theory derivative_domain_multi
    d_con_ends............................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 44 formulas, 44 attempted, 43 succeeded (0.01 s)
 Proof summary for theory init_partial_def
    diff_imp_init_partial.................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 67 formulas, 67 attempted, 66 succeeded (0.03 s)
 Proof summary for theory directional_deriv_def
    diff_imp_direction....................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 64 formulas, 64 attempted, 63 succeeded (0.04 s)
 Proof summary for theory partial_def
    F_partials_e_TCC1.....................unfinished          [SHOSTAK](0.00 s)
    F_partials_e..........................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 20 formulas, 20 attempted, 18 succeeded (0.01 s)
 Proof summary for theory Taylor_Thrm_Multi
    g_thm_dif.............................unfinished          [SHOSTAK](0.01 s)
    g_thm_dif_connect.....................unfinished          [SHOSTAK](0.01 s)
    Theory totals: 39 formulas, 39 attempted, 37 succeeded (0.19 s)
 Proof summary for theory convergence_vec2vec
    every_mat.............................unfinished          [SHOSTAK](0.00 s)
    Theory totals: 83 formulas, 83 attempted, 82 succeeded (0.07 s)
Grand Totals: 1014 proofs, 1014 attempted, 1001 succeeded (0.75 s)
*** Warning: Missed 13 formulas.

Processing ODEs. Writing output to file summaries/ODEs.summary
Logging PVS information in summaries/ODEs.log

Processing dL. Writing output to file summaries/dL.summary
Logging PVS information in summaries/dL.log

Processing mult_poly. Writing output to file summaries/mult_poly.summary
Logging PVS information in summaries/mult_poly.log

ints                     Proving... [OK]
structures               Proving... [OK]
reals                    Proving... [MISS]
orders                   Proving... [OK]
analysis                 Proving... [MISS]
sets_aux                 Proving... [OK]
numbers                  Proving... [OK]
series                   Proving... [OK]
trig                     Proving... [OK]
vectors                  Proving... [OK]
sigma_set                Proving... [MISS]
algebra                  Proving... [MISS]
vect_analysis            Proving... [MISS]
lnexp                    Proving... [MISS]
power                    Proving... [MISS]
interval_arith           Proving... [MISS]
affine_arith             Proving... [OK]
matrices                 Proving... [OK]
Bernstein                Proving... [OK]
Sturm                    Proving... [OK]
Tarski                   Proving... [OK]
MetiTarski               Proving... [MISS]
fast_approx              Proving... [MISS]
shapes                   Proving... [MISS]
complex                  Proving... [MISS]
digraphs                 Proving... [OK]
float/axm_bnd            Proving... [MISS]
float/fnd_bnd            Proving... [MISS]
float/fnd_unb            Proving... [FAIL: Error: There is no applicable method for the generic function
*** Error occurred while typechecking ieee754sp]
float/ieee854            Proving... [FAIL: Error: Cannot find theory float[radix]
*** Error occurred while typechecking mod_lems]
fault_tolerance     Proving... [OK]
graphs                   Proving... [OK]
PVSioChecker             Proving... [OK]
LTL                      Proving... [OK]
exact_real_arith     Proving... [OK]
aviation                 Proving... [MISS]
ACCoRD                   Proving... [OK]
sorting                  Proving... [MISS]
TRS                      Proving... [MISS]
CCG                      Proving... [OK]
PVS0                     Proving... [OK]
Riemann                  Proving... [OK]
examples                 Proving... [FAIL: Error reading proof file /Users/mmoscato/nasa/pvslib/pvslib-gitlab-pvs-8.0-fixes/examples/hutch_examples.prf:
*** Error reading proof file /Users/mmoscato/nasa/pvslib/pvslib-gitlab-pvs-8.0-fixes/examples/hutch_examples.prf:
*** Error reading proof file /Users/mmoscato/nasa/pvslib/pvslib-gitlab-pvs-8.0-fixes/examples/hutch_examples.prf:
*** Error: Value of PRECISION in (/ PRECISION 3.322) is 210_TCC1, not a NUMBER. (examples)
*** Error occurred while rerunning proof of era_examples.sqrt2_num_b210_TCC1]
topology                 Proving... [OK]
complex_alt              Proving... [OK]
scott                    Proving... [OK]
while                    Proving... [OK]
extended_nnreal     Proving... [OK]
metric_space             Proving... [OK]
measure_integration     Proving... [OK]
complex_integration     Proving... [OK]
lebesgue                 Proving... [OK]
probability              Proving... [OK]
co_structures            Proving... [OK]
TU_Games                 Proving... [MISS]
linear_algebra           Proving... [MISS]
ASP                      Proving... [MISS]
line_segments            Proving... [FAIL: Error: Invalid index 1 for (SIMPLE-VECTOR 1), should be a non-negative integer below 1.*** Error occurred while typechecking quad_minmax]
polygons                 Proving... [FAIL: Error: Invalid index 1 for (SIMPLE-VECTOR 1), should be a non-negative integer below 1.*** Error occurred while typechecking vertex_list]
polygon_merge            Proving... [FAIL: Error: Invalid index 1 for (SIMPLE-VECTOR 1), should be a non-negative integer below 1.*** Error occurred while typechecking vertex_list]
mv_analysis              Proving... [MISS]
ODEs                     Proving... [OK]
dL                       Proving... [OK]
mult_poly                Proving... [OK]

*** Number of libraries: 64