Quelle  ACCoRD.summary   Sprache: unbekannt

*** 
*** top (19:20:38 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
*** Trusted Oracles
***   MetiTarski: MetiTarski Theorem Prover via PVS proof rule metit
*** 
 Proof summary for theory top
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory util
    eq_correct_1..........................proved - complete   [shostak](0.48 s)
    eq_neg................................proved - complete   [shostak](0.12 s)
    gt_correct_1..........................proved - complete   [shostak](1.35 s)
    lt_correct_1..........................proved - complete   [shostak](0.06 s)
    ge_correct_1..........................proved - complete   [shostak](0.05 s)
    le_correct_1..........................proved - complete   [shostak](0.04 s)
    gt_correct_2..........................proved - complete   [shostak](0.35 s)
    lt_correct_2..........................proved - complete   [shostak](0.09 s)
    ge_correct_2..........................proved - complete   [shostak](0.08 s)
    le_correct_2..........................proved - complete   [shostak](0.08 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (2.70 s)

 Proof summary for theory horizontal_dist_convexity
    horiz_dist_convex_scaf................proved - complete   [shostak](1.25 s)
    horiz_dist_strictly_convex_scaf.......proved - complete   [shostak](1.25 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (2.50 s)

 Proof summary for theory vertical_dist_convexity
    vert_dist_convex_scaf.................proved - complete   [shostak](0.12 s)
    vert_dist_strictly_convex_scaf........proved - complete   [shostak](0.53 s)
    vert_dist_scaf_quad_eq_0..............proved - complete   [shostak](0.31 s)
    vert_dist_scaf_quad_ge_0..............proved - complete   [shostak](0.44 s)
    vert_dist_scaf_quad_gt_0..............proved - complete   [shostak](0.52 s)
    vert_dist_scaf_quad_le_0..............proved - complete   [shostak](0.45 s)
    vert_dist_scaf_quad_lt_0..............proved - complete   [shostak](0.51 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (2.88 s)

 Proof summary for theory definitions
    horizontalCoordination_symm...........proved - complete   [shostak](0.03 s)
    Horizontal_Strategy_TCC1..............proved - complete   [shostak](0.03 s)
    horizontalCoordination_strategy.......proved - complete   [shostak](0.02 s)
    horizontal_tca_gt_0_TCC1..............proved - complete   [shostak](0.09 s)
    horizontal_tca_gt_0...................proved - complete   [shostak](0.06 s)
    horizontal_tca_nzv_gt_0...............proved - complete   [shostak](0.06 s)
    horizontal_tca_lt_0_TCC1..............proved - complete   [shostak](0.07 s)
    horizontal_tca_lt_0...................proved - complete   [shostak](0.06 s)
    horizontal_tca_nzv_lt_0...............proved - complete   [shostak](0.06 s)
    horizontal_tca_dot_zero...............proved - complete   [shostak](-.03 s)
    horizontal_sq_dtca_eq.................proved - complete   [shostak](0.39 s)
    horizontal_tca_min....................proved - complete   [shostak](0.35 s)
    sqv_decreasing_before_horizontal_tca...proved - complete   [shostak](0.71 s)
    sqv_increasing_after_horizontal_tca...proved - complete   [shostak](0.72 s)
    le_rel................................proved - complete   [shostak](0.08 s)
    Vdir_perp.............................proved - complete   [shostak](0.09 s)
    W0_dot................................proved - complete   [shostak](0.04 s)
    nz_W0.................................proved - complete   [shostak](0.03 s)
    nz_W..................................proved - complete   [shostak](0.08 s)
    W_dot.................................proved - complete   [shostak](0.07 s)
    dot_W.................................proved - complete   [shostak](0.60 s)
    s_dot_Vdir_eq_0.......................proved - complete   [shostak](0.07 s)
    W0_dot_Vdir_eq_0......................proved - complete   [shostak](0.10 s)
    norm_W0_ge............................proved - complete   [shostak](0.58 s)
    dot_pos_divergent.....................proved - complete   [shostak](0.10 s)
    dot_nneg_divergent....................proved - complete   [shostak](0.50 s)
    gs_nz.................................proved - complete   [shostak](0.02 s)
    gs_only_id............................proved - complete   [shostak](0.02 s)
    gs_only_scal..........................proved - complete   [shostak](0.02 s)
    gs_only_symm..........................proved - complete   [shostak](0.08 s)
    gs_only_trans.........................proved - complete   [shostak](0.07 s)
    gs_only_normalize.....................proved - complete   [shostak](0.09 s)
    gs_only_zero_left.....................proved - complete   [shostak](0.03 s)
    gs_only_zero_right....................proved - complete   [shostak](0.03 s)
    trk_only_id...........................proved - complete   [shostak](0.02 s)
    trk_only_symm.........................proved - complete   [shostak](0.16 s)
    trk_only_zero_left....................proved - complete   [shostak](0.03 s)
    trk_only_zero_right...................proved - complete   [shostak](0.02 s)
    optimal_id............................proved - complete   [shostak](0.02 s)
    z_at_vertical_tau_eq_0................proved - complete   [shostak](0.03 s)
    Theory totals: 40 formulas, 40 attempted, 40 succeeded (5.60 s)

 Proof summary for theory gs_only
    k_l_det...............................proved - complete   [shostak](0.37 s)
    k_l_det_nz............................proved - complete   [shostak](1.88 s)
    gs_only_line_k_l_TCC1.................proved - complete   [shostak](0.08 s)
    gs_only_line_k_l_TCC2.................proved - complete   [shostak](0.02 s)
    gs_only_line_k_l_complete.............proved - complete   [shostak](0.17 s)
    gs_only_line_TCC1.....................proved - complete   [shostak](0.04 s)
    same_gs_only_line.....................proved - complete   [shostak](0.26 s)
    gs_only_line_complete.................proved - complete   [shostak](0.08 s)
    gs_only_dot_TCC1......................proved - complete   [shostak](0.13 s)
    gs_only_dot_complete..................proved - complete   [shostak](0.25 s)
    gs_only_circle_TCC1...................proved - complete   [shostak](0.17 s)
    gs_only_circle_TCC2...................proved - complete   [shostak](0.03 s)
    gs_only_circle_TCC3...................proved - complete   [shostak](0.03 s)
    gs_only_circle_solution...............proved - complete   [shostak](1.89 s)
    gs_only_circle_complete...............proved - complete   [shostak](0.92 s)
    gs_only_vertical_TCC1.................proved - complete   [shostak](0.03 s)
    gs_only_vertical_TCC2.................proved - complete   [shostak](0.06 s)
    gs_only_vertical_TCC3.................proved - complete   [shostak](0.05 s)
    gs_only_vertical_TCC4.................proved - complete   [shostak](0.02 s)
    gs_only_vertical_on_D.................proved - complete   [shostak](0.85 s)
    Theory totals: 20 formulas, 20 attempted, 20 succeeded (7.33 s)

 Proof summary for theory horizontal
    ss_nzv................................proved - complete   [shostak](0.09 s)
    ss_sp.................................proved - complete   [shostak](0.12 s)
    neg_ss................................proved - complete   [shostak](0.03 s)
    neg_sp................................proved - complete   [shostak](0.11 s)
    horizontal_conflict_sum_closed........proved - complete   [shostak](1.80 s)
    horizontal_conflict_neg...............proved - complete   [shostak](0.44 s)
    horizontal_conflict_symm..............proved - complete   [shostak](0.03 s)
    horizontal_conflict_scal..............proved - complete   [shostak](0.08 s)
    horizontal_conflict_ever..............proved - complete   [shostak](0.03 s)
    horizontal_conflict_ever_scal.........proved - complete   [shostak](0.07 s)
    Delta_zero_eq_0.......................proved - complete   [shostak](0.05 s)
    Delta_scal............................proved - complete   [shostak](0.18 s)
    Delta_eq..............................proved - complete   [shostak](0.11 s)
    Delta_symm............................proved - complete   [shostak](0.06 s)
    Delta_discr2b.........................proved - complete   [shostak](0.09 s)
    Delta_gt_0_nzv........................proved - complete   [shostak](0.05 s)
    ground_speed..........................proved - complete   [shostak](0.03 s)
    Delta_gt_0............................proved - complete   [shostak](0.31 s)
    Delta_gt_0_on_D.......................proved - complete   [shostak](-1.19 s)
    Delta_eq_0_dot_on_D...................proved - complete   [shostak](0.24 s)
    Delta_ge_0............................proved - complete   [shostak](0.65 s)
    Delta_ge_0_2..........................proved - complete   [shostak](0.06 s)
    Delta_eq_0_eq_tca.....................proved - complete   [shostak](3.14 s)
    sdotv_lt_0............................proved - complete   [shostak](0.62 s)
    Theta_D_TCC1..........................proved - complete   [shostak](0.04 s)
    Theta_D_on_D..........................proved - complete   [shostak](0.63 s)
    Theta_D_unique_eps....................proved - complete   [shostak](0.22 s)
    Theta_D_unique........................proved - complete   [shostak](0.06 s)
    Theta_D_symm_TCC1.....................proved - complete   [shostak](0.03 s)
    Theta_D_symm..........................proved - complete   [shostak](0.05 s)
    Theta_D_scal_TCC1.....................proved - complete   [shostak](0.05 s)
    Theta_D_scal..........................proved - complete   [shostak](-.37 s)
    Theta_D_neg_nzv_TCC1..................proved - complete   [shostak](0.44 s)
    Theta_D_neg_nzv.......................proved - complete   [shostak](0.39 s)
    Theta_D_le............................proved - complete   [shostak](0.15 s)
    Theta_D_lt_TCC1.......................proved - complete   [shostak](0.02 s)
    Theta_D_lt............................proved - complete   [shostak](0.15 s)
    Theta_D_Delta_eq_0....................proved - complete   [shostak](0.12 s)
    Theta_D_eq_0..........................proved - complete   [shostak](0.16 s)
    Theta_D_ge_0..........................proved - complete   [shostak](0.45 s)
    Theta_D_neq_0.........................proved - complete   [shostak](0.34 s)
    horizontal_conflict...................proved - complete   [shostak](0.18 s)
    horizontal_conflict_on_D..............proved - complete   [shostak](1.14 s)
    horizontal_entry_le...................proved - complete   [shostak](0.55 s)
    not_horizontal_entry_lt...............proved - complete   [shostak](0.49 s)
    horizontal_los_inside_Theta...........proved - complete   [shostak](0.10 s)
    horizontal_sep_outside_Theta..........proved - complete   [shostak](0.42 s)
    not_horiz_sep_inside_closed_Theta.....proved - complete   [shostak](0.25 s)
    Theta_D_entry_gt_0_TCC1...............proved - complete   [shostak](0.06 s)
    Theta_D_entry_gt_0....................proved - complete   [shostak](0.06 s)
    Theta_D_exit_gt_0.....................proved - complete   [shostak](0.64 s)
    Theta_D_entry_lt_t_TCC1...............proved - complete   [shostak](0.57 s)
    Theta_D_entry_lt_t....................proved - complete   [shostak](0.79 s)
    horizontal_conflict_entry_TCC1........proved - complete   [shostak](0.05 s)
    horizontal_conflict_entry.............proved - complete   [shostak](0.09 s)
    not_horizontal_conflict_exit_TCC1.....proved - complete   [shostak](0.04 s)
    not_horizontal_conflict_exit..........proved - complete   [shostak](0.09 s)
    Theta_D_horizontal_dir_TCC1...........proved - complete   [shostak](0.41 s)
    Theta_D_horizontal_dir................proved - complete   [shostak](0.60 s)
    horizontal_tca_midpoint...............proved - complete   [shostak](0.33 s)
    horizontal_tca_entry_exit_TCC1........proved - complete   [shostak](0.29 s)
    horizontal_tca_entry_exit.............proved - complete   [shostak](0.06 s)
    horizontal_tca_los....................proved - complete   [shostak](0.05 s)
    horizontal_tca_le_D...................proved - complete   [shostak](0.05 s)
    horizontal_tca_pos....................proved - complete   [shostak](0.06 s)
    Theta_D_positive_conflict.............proved - complete   [shostak](0.09 s)
    circle_solution_2D_horizontal_sep.....proved - complete   [shostak](0.07 s)
    Theta_D_circle_solution_2D............proved - complete   [shostak](0.08 s)
    circle_solution_2D_Delta_ge_0.........proved - complete   [shostak](0.03 s)
    circle_solution_2D_Theta_D_TCC1.......proved - complete   [shostak](0.03 s)
    circle_solution_2D_Theta_D............proved - complete   [shostak](0.60 s)
    circle_solution_2D_strict_horizontal_sep...proved - complete   [shostak](0.06 s)
    Theta_D_line_intersection.............proved - complete   [shostak](-1.32 s)
    tangent_line_intersection_v_independent...proved - complete   [shostak](0.26 s)
    tangent_vector_not_conflict...........proved - complete   [shostak](0.44 s)
    horizontal_conflict_is_an_open_set....proved - complete   [shostak](0.55 s)
    Theory totals: 76 formulas, 76 attempted, 76 succeeded (18.40 s)

 Proof summary for theory trk_only
    trk_only_line_TCC1....................proved - complete   [shostak](0.51 s)
    trk_only_line_TCC2....................proved - complete   [shostak](0.03 s)
    same_trk_only_line....................proved - complete   [shostak](0.05 s)
    trk_only_line_complete................proved - complete   [shostak](0.37 s)
    trk_only_line_lt......................proved - complete   [shostak](0.20 s)
    trk_only_dot_TCC1.....................proved - complete   [shostak](0.13 s)
    trk_only_dot_complete.................proved - complete   [shostak](0.25 s)
    trk_only_circle_eq_dot................proved - complete   [shostak](0.67 s)
    trk_spc_on_D..........................proved - complete   [shostak](0.13 s)
    trk_spc_Delta_ge_0....................proved - complete   [shostak](0.05 s)
    trk_spc_dot...........................proved - complete   [shostak](0.20 s)
    trk_spc_line_solution.................proved - complete   [shostak](0.06 s)
    trk_spc_horizontal_dir................proved - complete   [shostak](0.51 s)
    trk_only_circle_TCC1..................proved - complete   [shostak](0.15 s)
    trk_only_circle_TCC2..................proved - complete   [shostak](0.03 s)
    trk_only_circle_TCC3..................proved - complete   [shostak](0.02 s)
    trk_only_circle_solution..............proved - complete   [shostak](0.77 s)
    trk_only_circle_complete..............proved - complete   [shostak](1.24 s)
    trk_only_vertical_TCC1................proved - complete   [shostak](0.03 s)
    trk_only_vertical_TCC2................proved - complete   [shostak](0.06 s)
    trk_only_vertical_TCC3................proved - complete   [shostak](0.06 s)
    trk_only_vertical_TCC4................proved - complete   [shostak](0.02 s)
    trk_only_vertical_on_D................proved - complete   [shostak](0.85 s)
    Theory totals: 23 formulas, 23 attempted, 23 succeeded (6.39 s)

 Proof summary for theory line_solutions
    line_solution_dot_neg.................proved - complete   [shostak](0.11 s)
    line_solution_sep_dot_negative........proved - complete   [shostak](0.23 s)
    line_solution_on_D_TCC1...............proved - complete   [shostak](0.03 s)
    line_solution_on_D....................proved - complete   [shostak](0.23 s)
    on_D_line.............................proved - complete   [shostak](0.11 s)
    line_solution_scal....................proved - complete   [shostak](1.04 s)
    line_solution_zero_eps................proved - complete   [shostak](0.10 s)
    line_solution_zero....................proved - complete   [shostak](0.20 s)
    line_solution_Delta...................proved - complete   [shostak](1.94 s)
    det_neq_0.............................proved - complete   [shostak](0.15 s)
    line_solution_eps.....................proved - complete   [shostak](0.17 s)
    line_solution_eps_line................proved - complete   [shostak](0.04 s)
    line_solution_meets_horizontal_criterion...proved - complete   [shostak](0.09 s)
    line_solution_independence............proved - complete   [shostak](0.25 s)
    line_solution_invariant_TCC1..........proved - complete   [shostak](0.05 s)
    line_solution_invariant...............proved - complete   [shostak](0.11 s)
    line_solution_rewrite.................proved - complete   [shostak](1.90 s)
    line_solution_det.....................proved - complete   [shostak](0.92 s)
    line_solution_scal_unique.............proved - complete   [shostak](2.71 s)
    line_solution_coordination............proved - complete   [shostak](0.14 s)
    line_solution_along_line_TCC1.........proved - complete   [shostak](0.50 s)
    line_solution_along_line..............proved - complete   [shostak](0.26 s)
    Theory totals: 22 formulas, 22 attempted, 22 succeeded (11.30 s)

 Proof summary for theory horizontal_criteria
    R_TCC1................................proved - complete   [shostak](0.03 s)
    R_eq_0................................proved - complete   [shostak](0.21 s)
    R_gt_0................................proved - complete   [shostak](0.03 s)
    R_symm................................proved - complete   [shostak](0.04 s)
    sq_R_det..............................proved - complete   [shostak](0.11 s)
    Delta_sq_det..........................proved - complete   [shostak](1.70 s)
    Delta_sq_det_equality.................proved - complete   [shostak](1.18 s)
    Delta_zero_eps_line_equality..........proved - complete   [shostak](0.67 s)
    horizontal_solution...................proved - complete   [shostak](1.50 s)
    horizontal_criterion_scal.............proved - complete   [shostak](0.20 s)
    horizontal_criterion_eps..............proved - complete   [shostak](0.34 s)
    horizontal_criterion_symmetric........proved - complete   [shostak](0.71 s)
    horizontal_criterion_eps_unique.......proved - complete   [shostak](0.15 s)
    horizontal_criterion_independence.....proved - complete   [shostak](0.45 s)
    horizontal_criterion_sum_closed.......proved - complete   [shostak](0.76 s)
    horizontal_criterion_coordination.....proved - complete   [shostak](0.13 s)
    horizontal_sep_dir....................proved - complete   [shostak](0.48 s)
    horizontal_exit_independence..........proved - complete   [shostak](-1.87 s)
    horizontal_exit_coordination..........proved - complete   [shostak](0.27 s)
    Theory totals: 19 formulas, 19 attempted, 19 succeeded (7.09 s)

 Proof summary for theory predicate_coordination_2D
    coordinated_symmetric_2D..............proved - complete   [shostak](0.10 s)
    sum_indep_coordinated_2D..............proved - complete   [shostak](0.20 s)
    coordinated_sum_indep_2D..............proved - complete   [shostak](0.50 s)
    sum_indep_coordinated_antisym_2D......proved - complete   [shostak](0.20 s)
    coordinated_antisym_sum_indep_2D......proved - complete   [shostak](0.52 s)
    deriv_0_2D............................proved - complete   [shostak](0.03 s)
    deriv_subset_2D.......................proved - complete   [shostak](0.08 s)
    deriv_coordinated_2D..................proved - complete   [shostak](0.35 s)
    deriv_coordinated_1...................proved - complete   [shostak](0.05 s)
    Comb_coordinated_2D...................proved - complete   [shostak](0.15 s)
    coordinated_implies_independent_2D....proved - complete   [shostak](0.04 s)
    Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.22 s)

 Proof summary for theory opt_trk_gs
    k_opt_tangent.........................proved - complete   [shostak](0.06 s)
    opt_trk_gs_line_TCC1..................proved - complete   [shostak](0.53 s)
    opt_trk_gs_line_TCC2..................proved - complete   [shostak](0.07 s)
    opt_trk_gs_dot_TCC1...................proved - complete   [shostak](0.12 s)
    opt_trk_gs_vertical_TCC1..............proved - complete   [shostak](0.03 s)
    opt_trk_gs_vertical_TCC2..............proved - complete   [shostak](0.06 s)
    opt_trk_gs_vertical_on_D..............proved - complete   [shostak](0.91 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.78 s)

 Proof summary for theory horizontal_criterion_line
    horizontal_criterion_rewrite..........proved - complete   [shostak](3.05 s)
    horizontal_criterion_special_coordination...proved - complete   [shostak](0.58 s)
    horizontal_criterion_dot_equality.....proved - complete   [shostak](0.23 s)
    horizontal_criterion_line_invariance...proved - complete   [shostak](0.37 s)
    horizontal_criterion_line_coordination...proved - complete   [shostak](0.04 s)
    horizontal_criterion_ext_subset.......proved - complete   [shostak](0.55 s)
    horizontal_criterion_ext_restrict.....proved - complete   [shostak](0.06 s)
    horizontal_criterion_ext_restrict_conflict...proved - complete   [shostak](0.05 s)
    horizontal_criterion_ext_independence...proved - complete   [shostak](0.03 s)
    horizontal_criterion_ext_coordinated...proved - complete   [shostak](2.00 s)
    horizontal_criterion_ext_sum_closed...proved - complete   [shostak](1.15 s)
    horizontal_criterion_ext_scal.........proved - complete   [shostak](0.34 s)
    horizontal_criterion_ext_seg_convex...proved - complete   [shostak](1.13 s)
    horizontal_criterion_ext_seg_independence_TCC1...proved - complete   [shostak](0.53 s)
    horizontal_criterion_ext_seg_independence...proved - complete   [shostak](0.46 s)
    horizontal_criterion_ext_seg_coordination_TCC1...proved - complete   [shostak](0.87 s)
    horizontal_criterion_ext_seg_coordination_TCC2...proved - complete   [shostak](3.98 s)
    horizontal_criterion_ext_seg_coordination...proved - complete   [shostak](-.58 s)
    Theory totals: 18 formulas, 18 attempted, 18 succeeded (14.86 s)

 Proof summary for theory tangent_line
    alpha_TCC1............................proved - complete   [shostak](0.12 s)
    beta_TCC1.............................proved - complete   [shostak](0.03 s)
    alpha_neg.............................proved - complete   [shostak](0.03 s)
    beta_neg..............................proved - complete   [shostak](0.09 s)
    sq_alpha_beta.........................proved - complete   [shostak](0.29 s)
    Q_on_D................................proved - complete   [shostak](0.40 s)
    Q_asymm...............................proved - complete   [shostak](0.22 s)
    Qs_asymm..............................proved - complete   [shostak](0.05 s)
    sqv_Qs................................proved - complete   [shostak](0.59 s)
    Qs_nzv................................proved - complete   [shostak](0.04 s)
    s_dot_Qs_lt_0.........................proved - complete   [shostak](0.36 s)
    det_s_Qs_lt_0.........................proved - complete   [shostak](0.54 s)
    alpha_D...............................proved - complete   [shostak](0.04 s)
    beta_R................................proved - complete   [shostak](0.14 s)
    alpha_beta............................proved - complete   [shostak](0.16 s)
    beta_alpha............................proved - complete   [shostak](0.11 s)
    det_v_Q...............................proved - complete   [shostak](0.30 s)
    s_dot_Q...............................proved - complete   [shostak](0.15 s)
    det_s_Qs..............................proved - complete   [shostak](0.17 s)
    det_Q_s...............................proved - complete   [shostak](0.31 s)
    Q_eq_Qs_perp_TCC1.....................proved - complete   [shostak](0.14 s)
    Q_eq_Qs_perp..........................proved - complete   [shostak](1.07 s)
    line_solution_Qs......................proved - complete   [shostak](0.59 s)
    parallel_nzv_Qs.......................proved - complete   [shostak](1.49 s)
    parallel_nzv_perp.....................proved - complete   [shostak](0.80 s)
    tangent_line_TCC1.....................proved - complete   [shostak](0.10 s)
    tangent_line_TCC2.....................proved - complete   [shostak](0.02 s)
    tangent_line_asymm....................proved - complete   [shostak](0.16 s)
    line_solution_tangent_line............proved - complete   [shostak](0.04 s)
    parallel_nzv_tangent_line.............proved - complete   [shostak](0.05 s)
    tangent_line_solution.................proved - complete   [shostak](0.07 s)
    tangent_line_independence.............proved - complete   [shostak](0.03 s)
    tangent_line_coordination.............proved - complete   [shostak](0.05 s)
    Theory totals: 33 formulas, 33 attempted, 33 succeeded (8.76 s)

 Proof summary for theory trk_line
    trk_line_eps_irt_TCC1.................proved - complete   [shostak](0.04 s)
    trk_line_eps_irt_TCC2.................proved - complete   [shostak](0.03 s)
    trk_line_eps_irt_tangent_line.........proved - complete   [shostak](0.17 s)
    trk_line_eps_irt_dot..................proved - complete   [shostak](0.51 s)
    irt_trk_line_eps......................proved - complete   [shostak](0.05 s)
    trk_line_eps_tangent_line.............proved - complete   [shostak](0.04 s)
    trk_line_is_line_solution.............proved - complete   [shostak](0.03 s)
    trk_line_complete.....................proved - complete   [shostak](0.07 s)
    Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.94 s)

 Proof summary for theory gs_line
    gs_line_eps_TCC1......................proved - complete   [shostak](0.03 s)
    gs_line_eps_TCC2......................proved - complete   [shostak](0.02 s)
    gs_line_eps_tangent_line..............proved - complete   [shostak](0.16 s)
    gs_line_is_line_solution..............proved - complete   [shostak](0.04 s)
    gs_line_complete......................proved - complete   [shostak](0.07 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.32 s)

 Proof summary for theory opt_line
    opt_line_eps_TCC1.....................proved - complete   [shostak](0.03 s)
    opt_line_eps_TCC2.....................proved - complete   [shostak](0.03 s)
    opt_line_eps_tangent_line.............proved - complete   [shostak](0.17 s)
    opt_line_is_line_solution.............proved - complete   [shostak](0.04 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.27 s)

 Proof summary for theory horizontal_cr
    horizontal_cr_is_line_solution........proved - complete   [shostak](0.05 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s)

 Proof summary for theory repulsive
    tca_TCC1.............................proved - complete   [shostak]( 0.02 s)
    repulsive_simple.....................proved - complete   [shostak]( 0.43 s)
    repulsive_transitive.................proved - complete   [shostak]( 0.68 s)
    not_repulsive_sum_closed.............proved - complete   [shostak]( 1.40 s)
    repulsive_criteria_scal_s............proved - complete   [shostak]( 0.62 s)
    repulsive_criteria_scal_nv...........proved - complete   [shostak]( 1.69 s)
    wedge_containment....................proved - complete   [shostak]( 3.27 s)
    repulsive_criteria_transitive........proved - complete   [shostak]( 2.94 s)
    repulsive_criteria_transitive_odd1...proved - complete   [shostak]( 2.15 s)
    rep_crit_odd2_ax.....................proved - complete   [shostak]( 0.77 s)
    repulsive_criteria_transitive_odd2...proved - complete   [shostak]( 3.16 s)
    repulsive_criteria_transitive_odd3...proved - complete   [shostak]( 4.00 s)
    repulsive_criteria_sum_closed........proved - complete   [shostak]( 1.45 s)
    repulsive_criteria_indep_of_length...proved - complete   [shostak]( 0.51 s)
    repulsive_criteria_repulsive.........proved - complete   [shostak]( 3.12 s)
    repulsive_criteria_repulsive2........proved - complete   [shostak]( 3.83 s)
    repulsive_criteria_symmetric.........proved - complete   [shostak]( 0.95 s)
    repulsive_criteria_coordinately_repulsive...proved - complete   [shostak]( 1.56 s)
    foo..................................proved - complete   [shostak](32.74 s)
    repulsive_increases_dist_TCC1........proved - complete   [shostak]( 0.75 s)
    repulsive_increases_dist.............proved - complete   [shostak]( 0.62 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (66.64 s)

 Proof summary for theory horizontal_los_criterion
    horizontal_los_criterion_repulsive....proved - complete   [shostak](0.03 s)
    horizontal_los_criterion_coordinately_repulsive...proved - complete   [shostak](0.03 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.06 s)

 Proof summary for theory horizontal_los
    sDs_TCC1..............................proved - complete   [shostak](0.38 s)
    gs_los_TCC1...........................proved - complete   [shostak](0.41 s)
    gs_los_TCC2...........................proved - complete   [shostak](0.04 s)
    gs_los_def............................proved - complete   [shostak](2.04 s)
    trk_los_TCC1..........................proved - complete   [shostak](0.33 s)
    trk_los_TCC2..........................proved - complete   [shostak](0.04 s)
    trk_los_def...........................proved - complete   [shostak](1.79 s)
    los_recovery_meets_criteria...........proved - complete   [shostak](0.46 s)
    los_recovery_independence.............proved - complete   [shostak](0.09 s)
    los_recovery_coordination_TCC1........proved - complete   [shostak](0.04 s)
    los_recovery_coordination.............proved - complete   [shostak](0.32 s)
    Theory totals: 11 formulas, 11 attempted, 11 succeeded (5.93 s)

 Proof summary for theory old_horiz_los_criterion
    horizontal_los_crit_symm..............proved - complete   [shostak](0.43 s)
    horizontal_los_crit_independent.......proved - complete   [shostak](0.03 s)
    horizontal_los_crit_coordinated.......proved - complete   [shostak](0.42 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.88 s)

 Proof summary for theory circle_optimum_2D
    intersects_circle_fun_scal...........proved - complete   [shostak]( 0.31 s)
    intersects_circle_fun_def............proved - complete   [shostak]( 0.64 s)
    intersects_circle_fun_inc............proved - complete   [shostak]( 1.98 s)
    inter_circle_max_time_TCC1...........proved - complete   [shostak]( 0.38 s)
    inter_circle_max_time_TCC2...........proved - complete   [shostak]( 0.16 s)
    inter_circle_max_time_scal...........proved - complete   [shostak]( 0.38 s)
    inter_circle_max_time_def............proved - complete   [shostak]( 0.71 s)
    inter_circle_max_norm_scal...........proved - complete   [shostak]( 0.60 s)
    max_norm_increasing..................proved - complete   [shostak](12.54 s)
    max_circle_point_in_slice_TCC1.......proved - complete   [shostak]( 0.07 s)
    lem1.................................proved - complete   [shostak]( 0.38 s)
    lem2.................................proved - complete   [shostak]( 0.58 s)
    max_circle_point_in_slice_intersection...proved - complete   [shostak]( 4.14 s)
    max_circle_point_in_slice_union......proved - complete   [shostak]( 0.39 s)
    dot_gt_dot_equals_slice_intersection...proved - complete   [shostak]( 7.79 s)
    dot_gt_dot_equals_slice_union........proved - complete   [shostak]( 7.20 s)
    max_circle_point_in_slice_lem........proved - complete   [shostak]( 3.97 s)
    max_circle_point_in_slice_lem_eq.....proved - complete   [shostak]( 0.61 s)
    max_circle_point_in_slide_sym_lem....proved - complete   [shostak]( 3.94 s)
    max_circle_point_in_slice_def........proved - complete   [shostak]( 6.80 s)
    max_circle_point_in_slice_complete...proved - complete   [shostak]( 1.10 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (54.67 s)

 Proof summary for theory wedge_optimum_2D
    intersects_segment_fun?_TCC1..........proved - complete   [shostak](0.06 s)
    intersects_segment_fun?_TCC2..........proved - complete   [shostak](0.23 s)
    intersects_segment_fun?_TCC3..........proved - complete   [shostak](0.32 s)
    intersects_segment_fun?_TCC4..........proved - complete   [shostak](0.47 s)
    intersects_segment_fun_def............proved - complete   [shostak](1.61 s)
    intersects_segment_sym................proved - complete   [shostak](-1.98 s)
    on_segment_in_wedge_sym...............proved - complete   [shostak](0.07 s)
    max_segment_point_in_slice_TCC1.......proved - complete   [shostak](0.13 s)
    max_segment_point_in_slice_TCC2.......proved - complete   [shostak](0.43 s)
    max_segment_point_in_slice_TCC3.......proved - complete   [shostak](0.43 s)
    max_segment_point_in_slice_def........proved - complete   [shostak](3.48 s)
    max_segment_point_in_slice_complete...proved - complete   [shostak](0.05 s)
    Theory totals: 12 formulas, 12 attempted, 12 succeeded (5.30 s)

 Proof summary for theory vertical_los_criterion
    time_vertical_exit_by_TCC1............proved - complete   [shostak](0.13 s)
    time_vertical_exit_by_TCC2............proved - complete   [shostak](0.07 s)
    time_vertical_exit_by_TCC3............proved - complete   [shostak](0.15 s)
    time_vertical_exit_by_symm............proved - complete   [shostak](0.18 s)
    min_rel_vert_speed_TCC1...............proved - complete   [shostak](0.03 s)
    min_rel_vert_speed_TCC2...............proved - complete   [shostak](0.11 s)
    min_rel_vert_speed_symm...............proved - complete   [shostak](0.12 s)
    vs_bound_crit_indep_TCC1..............proved - complete   [shostak](0.04 s)
    vs_bound_crit_indep_TCC2..............proved - complete   [shostak](0.04 s)
    vs_bound_crit_indep...................proved - complete   [shostak](8.20 s)
    vs_bound_crit_coord...................proved - complete   [shostak](7.72 s)
    vs_bound_dir..........................proved - complete   [shostak](0.13 s)
    vertical_los_criterion_coord..........proved - complete   [shostak](1.79 s)
    vertical_sep_after_def................proved - complete   [shostak](0.25 s)
    z_los_vertical_sep....................proved - complete   [shostak](1.26 s)
    Theory totals: 15 formulas, 15 attempted, 15 succeeded (20.22 s)

 Proof summary for theory vertical
    nz_spz................................proved - complete   [shostak](0.04 s)
    neg_spz...............................proved - complete   [shostak](0.05 s)
    on_signed_H...........................proved - complete   [shostak](0.08 s)
    vertical_conflict_neg.................proved - complete   [shostak](0.57 s)
    vertical_conflict_symm................proved - complete   [shostak](0.04 s)
    Theta_H_symm..........................proved - complete   [shostak](0.18 s)
    Theta_H_lt............................proved - complete   [shostak](0.36 s)
    Theta_H_on_H..........................proved - complete   [shostak](0.31 s)
    Theta_H_eq_0..........................proved - complete   [shostak](0.57 s)
    Theta_H_ge_0..........................proved - complete   [shostak](0.74 s)
    Theta_H_exit_gt_0.....................proved - complete   [shostak](0.34 s)
    Theta_H_unique_eps....................proved - complete   [shostak](0.41 s)
    Theta_H_unique........................proved - complete   [shostak](0.21 s)
    vertical_los_entry....................proved - complete   [shostak](0.62 s)
    Theta_H_entry_lt_t....................proved - complete   [shostak](0.40 s)
    vertical_conflict.....................proved - complete   [shostak](1.05 s)
    vertical_los_inside_Theta.............proved - complete   [shostak](0.77 s)
    vertical_sep_outside_Theta............proved - complete   [shostak](0.16 s)
    Theta_H_vertical_dir..................proved - complete   [shostak](0.38 s)
    vertical_tau_entry_exit...............proved - complete   [shostak](0.33 s)
    vertical_tau_midpoint.................proved - complete   [shostak](0.11 s)
    vertical_tau_pos......................proved - complete   [shostak](0.19 s)
    vs_at_neg.............................proved - complete   [shostak](0.09 s)
    vs_at_H...............................proved - complete   [shostak](0.08 s)
    vs_at_complete........................proved - complete   [shostak](0.15 s)
    vertical_sep_dir......................proved - complete   [shostak](2.43 s)
    vertical_sep_at_sign..................proved - complete   [shostak](0.82 s)
    vertical_solution_vertical_sep........proved - complete   [shostak](0.20 s)
    vertical_solution_strict_vertical_sep...proved - complete   [shostak](0.66 s)
    Theta_H_vertical_solution.............proved - complete   [shostak](0.19 s)
    vertical_solution_Theta_H.............proved - complete   [shostak](0.62 s)
    vs_at_complete_vertical_solution......proved - complete   [shostak](0.41 s)
    vs_at_complete_dir....................proved - complete   [shostak](0.35 s)
    vertical_solution_exit................proved - complete   [shostak](2.14 s)
    vs_circle_at_direction................proved - complete   [shostak](0.84 s)
    vs_circle_at?_TCC1....................proved - complete   [shostak](0.13 s)
    vs_circle_at_complete_TCC1............proved - complete   [shostak](0.04 s)
    vs_circle_at_complete_TCC2............proved - complete   [shostak](0.22 s)
    vs_circle_at_complete.................proved - complete   [shostak](3.03 s)
    Theory totals: 39 formulas, 39 attempted, 39 succeeded (20.31 s)

 Proof summary for theory space_3D
    conflict_symm.........................proved - complete   [shostak](0.44 s)
    conflict_ever.........................proved - complete   [shostak](0.11 s)
    conflict_ever_shift...................proved - complete   [shostak](0.51 s)
    conflict_sum_closed...................proved - complete   [shostak](2.57 s)
    conflict_is_an_open_set...............proved - complete   [shostak](1.59 s)
    vertical_horizontal_conflict..........proved - complete   [shostak](0.09 s)
    neg_spz...............................proved - complete   [shostak](0.06 s)
    neg_sp2...............................proved - complete   [shostak](0.12 s)
    neg_sp................................proved - complete   [shostak](0.14 s)
    spv2..................................proved - complete   [shostak](0.13 s)
    ssv2..................................proved - complete   [shostak](0.04 s)
    sp_nzv................................proved - complete   [shostak](0.09 s)
    verticalCoordinationConflict_TCC1.....proved - complete   [shostak](0.48 s)
    verticalCoordinationConflict_asymm....proved - complete   [shostak](1.12 s)
    Vertical_Strategy_TCC1................proved - complete   [shostak](0.04 s)
    verticalCoordinationConflict_strategy...proved - complete   [shostak](0.04 s)
    verticalCoordinationConflict_correct_TCC1...proved - complete   [shostak](0.04 s)
    verticalCoordinationConflict_correct...proved - complete   [shostak](-.64 s)
    vs_los_strategy_TCC1..................proved - complete   [shostak](0.07 s)
    vs_los_vertical_strategy..............proved - complete   [shostak](1.03 s)
    Theory totals: 20 formulas, 20 attempted, 20 succeeded (8.07 s)

 Proof summary for theory definitions_3D
    nzv2..................................proved - complete   [shostak](0.02 s)
    break_symmetry_neg....................proved - complete   [shostak](0.12 s)
    vs_only_symm..........................proved - complete   [shostak](0.03 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.17 s)

 Proof summary for theory vertical_los_crit_CA
    Decision_Vector_TCC1..................proved - complete   [shostak](0.24 s)
    dv_to_ec_antisymmetric................proved - complete   [shostak](0.07 s)
    vertical_decision_vect_TCC1...........proved - complete   [shostak](0.14 s)
    vertical_decision_vect_TCC2...........proved - complete   [shostak](0.22 s)
    vertical_decision_vect_TCC3...........proved - complete   [shostak](0.03 s)
    vertical_decision_vect_TCC4...........proved - complete   [shostak](0.03 s)
    vertical_decision_vect_TCC5...........proved - complete   [shostak](0.25 s)
    vertical_decision_vect_TCC6...........proved - complete   [shostak](0.13 s)
    vertical_decision_vect_antisymmetric...proved - complete   [shostak](2.16 s)
    vertical_los_crit_CA_independent_TCC1...proved - complete   [shostak](0.03 s)
    vertical_los_crit_CA_independent_TCC2...proved - complete   [shostak](0.04 s)
    vertical_los_crit_CA_independent......proved - complete   [shostak](0.16 s)
    vertical_los_crit_CA_independent_strong_TCC1...proved - complete   [shostak](0.03 s)
    vertical_los_crit_CA_independent_strong_TCC2...proved - complete   [shostak](0.04 s)
    vertical_los_crit_CA_independent_strong...proved - complete   [shostak](3.32 s)
    vertical_los_crit_CA_independent_vspeed...proved - complete   [shostak](0.12 s)
    vertical_los_crit_CA_coordinated_vspeed...proved - complete   [shostak](0.32 s)
    vertical_los_crit_CA_coordinated......proved - complete   [shostak](0.20 s)
    vertical_los_crit_CA_coordinated_strong_TCC1...proved - complete   [shostak](0.04 s)
    vertical_los_crit_CA_coordinated_strong_TCC2...proved - complete   [shostak](0.04 s)
    vertical_los_crit_CA_coordinated_strong...proved - complete   [shostak](1.17 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (8.79 s)

 Proof summary for theory cd3d
    conflict_3D_2D_stable_TCC1............proved - complete   [shostak](0.16 s)
    conflict_3D_2D_stable_TCC2............proved - complete   [shostak](0.32 s)
    conflict_3D_2D_stable_TCC3............proved - complete   [shostak](-1.45 s)
    conflict_3D_2D_stable.................proved - complete   [shostak](4.06 s)
    conflict_3D_vz_swap...................proved - complete   [shostak](0.22 s)
    conflict_3D_on_open_interval..........proved - complete   [shostak](1.77 s)
    conflict_3D_vertical_TCC1.............proved - complete   [shostak](0.06 s)
    conflict_3D_vertical_TCC2.............proved - complete   [shostak](0.22 s)
    conflict_3D_vertical..................proved - complete   [shostak](0.53 s)
    detection_TCC1........................proved - complete   [shostak](0.23 s)
    detection_TCC2........................proved - complete   [shostak](0.19 s)
    detection_TCC3........................proved - complete   [shostak](0.05 s)
    detection_TCC4........................proved - complete   [shostak](0.04 s)
    detection_TCC5........................proved - complete   [shostak](0.05 s)
    detection_TCC6........................proved - complete   [shostak](0.04 s)
    detection_TCC7........................proved - complete   [shostak](0.12 s)
    detection_TCC8........................proved - complete   [shostak](0.12 s)
    detection_TCC9........................proved - complete   [shostak](0.10 s)
    detection_TCC10.......................proved - complete   [shostak](0.09 s)
    detection_TCC11.......................proved - complete   [shostak](0.85 s)
    detection_TCC12.......................proved - complete   [shostak](0.34 s)
    detection_correct.....................proved - complete   [shostak](6.01 s)
    detection_complete....................proved - complete   [shostak](5.11 s)
    conflict_detection....................proved - complete   [shostak](0.29 s)
    cd3d_rewrite_TCC1.....................proved - complete   [shostak](0.08 s)
    cd3d_rewrite_TCC2.....................proved - complete   [shostak](0.17 s)
    cd3d_rewrite..........................proved - complete   [shostak](4.75 s)
    cd3d_test.............................proved - complete   [shostak](1.20 s)
    cd3d_correct..........................proved - complete   [shostak](0.34 s)
    cd3d_complete.........................proved - complete   [shostak](1.35 s)
    cd3d..................................proved - complete   [shostak](0.03 s)
    cd3d_rewrite_vertical_TCC1............proved - complete   [shostak](0.04 s)
    cd3d_rewrite_vertical_TCC2............proved - complete   [shostak](0.07 s)
    cd3d_rewrite_vertical_TCC3............proved - complete   [shostak](0.21 s)
    cd3d_rewrite_vertical.................proved - complete   [shostak](0.94 s)
    vertical_solution_not_conflict_3D.....proved - complete   [shostak](0.13 s)
    conflict_3D_horizontal_conflict.......proved - complete   [shostak](0.09 s)
    conflict_3D_vertical_conflict.........proved - complete   [shostak](0.11 s)
    circle_solution_2D_not_conflict_3D....proved - complete   [shostak](0.12 s)
    Theory totals: 39 formulas, 39 attempted, 39 succeeded (29.16 s)

 Proof summary for theory circle_criterion
    vertical_sep_independence.............proved - complete   [shostak](0.08 s)
    nogs_criterion_independence...........proved - complete   [shostak](0.26 s)
    circle_criterion_independence.........proved - complete   [shostak](0.26 s)
    circle_criterion_at_independence......proved - complete   [shostak](0.04 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.64 s)

 Proof summary for theory vz_criteria
    vertical_exit_independence............proved - complete   [shostak](0.26 s)
    vertical_exit_coordination............proved - complete   [shostak](0.33 s)
    vertical_sep_dir_at...................proved - complete   [shostak](2.88 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (3.47 s)

 Proof summary for theory cd_vertical
    cd_vertical_rewrite...................proved - complete   [shostak](1.51 s)
    cd_vertical_correct...................proved - complete   [shostak](0.44 s)
    cd_vertical_complete..................proved - complete   [shostak](0.29 s)
    cd_vertical...........................proved - complete   [shostak](0.03 s)
    conflict_vertical_on_open_interval....proved - complete   [shostak](1.55 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (3.82 s)

 Proof summary for theory Lookahead
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory omega_2D
    IMP_metric_space_real_fun_TCC1........proved - complete   [shostak](0.02 s)
    IMP_ms_composition_cont_TCC1..........proved - complete   [shostak](0.02 s)
    IMP_ms_composition_cont_TCC2..........proved - complete   [shostak](0.03 s)
    horiz_dist_cont_scaf..................proved - complete   [shostak](1.25 s)
    conflict_2D_on_open_interval..........proved - complete   [shostak](1.03 s)
    circle_hit............................proved - complete   [shostak](0.38 s)
    horiz_dist_scaf_bounded_below.........proved - complete   [shostak](0.05 s)
    omega_2D_TCC1.........................proved - complete   [shostak](0.05 s)
    omega_2D_TCC2.........................proved - complete   [shostak](0.03 s)
    tau_2D_nonempty.......................proved - incomplete [shostak](0.28 s)
    tau_2D_TCC1...........................proved - incomplete [shostak](0.02 s)
    tau_2D_def............................proved - incomplete [shostak](0.04 s)
    omega_2D_min_rew_TCC1.................proved - incomplete [shostak](0.17 s)
    omega_2D_min_rew......................proved - incomplete [shostak](0.30 s)
    tau_2D_min............................proved - incomplete [shostak](0.22 s)
    omega_2D_continuous...................proved - incomplete [shostak](0.29 s)
    tau_2D_unique.........................proved - incomplete [shostak](0.13 s)
    tau_2D_connected......................proved - incomplete [shostak](0.15 s)
    tau_2D_v2.............................proved - incomplete [shostak](0.08 s)
    omega_2D_horizontal_omega.............proved - incomplete [shostak](0.06 s)
    omega_2D_conflict.....................proved - incomplete [shostak](0.07 s)
    omega_2D_eq_0.........................proved - incomplete [shostak](0.04 s)
    parts_of_v_nonzero_2D.................proved - incomplete [shostak](0.04 s)
    lower_circle_hit_solution.............proved - incomplete [shostak](0.87 s)
    circle_hit_solution...................proved - incomplete [shostak](0.99 s)
    no_horiz_speed_on_D...................proved - incomplete [shostak](0.05 s)
    omega_2D_Delta........................proved - incomplete [shostak](0.12 s)
    Theta_Ds_equal_line_sol_2D_TCC1.......proved - incomplete [shostak](0.06 s)
    Theta_Ds_equal_line_sol_2D_TCC2.......proved - complete   [shostak](0.95 s)
    Theta_Ds_equal_line_sol_2D............proved - incomplete [shostak](0.30 s)
    critical_points_2D....................proved - incomplete [shostak](0.07 s)
    Theory totals: 31 formulas, 31 attempted, 31 succeeded (8.15 s)

 Proof summary for theory cd2d
    conflict_2D_horizontal................proved - complete   [shostak](0.03 s)
    on_D_conflict.........................proved - complete   [shostak](1.74 s)
    tau_v2_TCC1...........................proved - complete   [shostak](0.09 s)
    tau_vv................................proved - complete   [shostak](0.18 s)
    tau_vv_continuous.....................proved - complete   [shostak](0.16 s)
    horizontal_omega_min..................proved - complete   [shostak](0.66 s)
    horizontal_omega_conflict.............proved - complete   [shostak](0.07 s)
    omega_vv_continuous...................proved - complete   [shostak](0.25 s)
    omega_vv..............................proved - complete   [shostak](0.39 s)
    omega_vv_conflict.....................proved - complete   [shostak](0.23 s)
    omega_vv_zero_TCC1....................proved - complete   [shostak](0.05 s)
    omega_vv_zero.........................proved - complete   [shostak](0.26 s)
    omega_half_line.......................proved - complete   [shostak](2.40 s)
    detection_2D_TCC1.....................proved - complete   [shostak](0.04 s)
    detection_2D_TCC2.....................proved - complete   [shostak](0.03 s)
    detection_2D_TCC3.....................proved - complete   [shostak](0.03 s)
    detection_2D_TCC4.....................proved - complete   [shostak](0.58 s)
    detection_2D_TCC5.....................proved - complete   [shostak](0.58 s)
    detection_2D_TCC6.....................proved - complete   [shostak](0.03 s)
    detection_2D_correct..................proved - complete   [shostak](0.30 s)
    detection_2D_complete.................proved - complete   [shostak](-1.71 s)
    conflict_detection_2D.................proved - complete   [shostak](0.22 s)
    cd2d..................................proved - complete   [shostak](0.06 s)
    Theory totals: 23 formulas, 23 attempted, 23 succeeded (6.67 s)

 Proof summary for theory cd3d_ever
    conflict_2D_stable_TCC1...............proved - complete   [shostak](0.10 s)
    conflict_2D_stable_TCC2...............proved - complete   [shostak](0.17 s)
    conflict_2D_stable_TCC3...............proved - complete   [shostak](0.09 s)
    conflict_2D_stable....................proved - complete   [shostak](2.62 s)
    conflict_vz_swap......................proved - complete   [shostak](0.19 s)
    conflict_on_open_interval.............proved - complete   [shostak](0.96 s)
    cd3d_ever_rewrite_TCC1................proved - complete   [shostak](0.06 s)
    cd3d_ever_rewrite_TCC2................proved - complete   [shostak](0.08 s)
    cd3d_ever_rewrite.....................proved - complete   [shostak](3.48 s)
    cd3d_ever_correct.....................proved - complete   [shostak](0.23 s)
    cd3d_ever_complete....................proved - complete   [shostak](0.68 s)
    cd3d_ever.............................proved - complete   [shostak](0.03 s)
    Theory totals: 12 formulas, 12 attempted, 12 succeeded (8.68 s)

 Proof summary for theory cd2d_ever
    cd2d_ever_def.........................proved - complete   [shostak](1.23 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (1.23 s)

 Proof summary for theory omega_v2
    omega_v2_generic......................proved - complete   [shostak](0.03 s)
    omega_v2_conflict.....................proved - incomplete [shostak](0.05 s)
    omega_v2_2D_eq_0......................proved - incomplete [shostak](0.13 s)
    omega_v2_critical_points..............proved - incomplete [shostak](0.11 s)
    omega_v2_continuous...................proved - incomplete [shostak](0.83 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.15 s)

 Proof summary for theory horizontal_sq_dtca
    IMP_vect_deriv_2D_TCC1................proved - complete   [shostak](0.06 s)
    IMP_vect_deriv_2D_TCC2................proved - complete   [shostak](0.02 s)
    horizontal_sq_dtca_diff_TCC1..........proved - complete   [shostak](0.02 s)
    horizontal_sq_dtca_diff...............proved - complete   [shostak](0.10 s)
    horizontal_sq_dtca_deriv_TCC1.........proved - complete   [shostak](0.03 s)
    horizontal_sq_dtca_deriv_TCC2.........proved - complete   [shostak](0.04 s)
    horizontal_sq_dtca_deriv..............proved - complete   [shostak](0.50 s)
    horizontal_sq_dtca_deriv_simpl........proved - complete   [shostak](1.88 s)
    horizontal_sq_dtca_deriv_sign_TCC1....proved - complete   [shostak](0.03 s)
    horizontal_sq_dtca_deriv_sign.........proved - complete   [shostak](2.12 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (4.80 s)

 Proof summary for theory cd2d_inf
    detection_2D_inf_TCC1.................proved - complete   [shostak](0.28 s)
    detection_2D_inf_correct..............proved - complete   [shostak](0.08 s)
    detection_2D_inf_complete.............proved - complete   [shostak](0.09 s)
    conflict_detection_2D_inf.............proved - complete   [shostak](0.10 s)
    cd2d_inf..............................proved - complete   [shostak](0.15 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.70 s)

 Proof summary for theory cd3d_inf
    conflict_3D_2D_inf_stable_TCC1........proved - complete   [shostak](0.10 s)
    conflict_3D_2D_inf_stable_TCC2........proved - complete   [shostak](0.13 s)
    conflict_3D_2D_inf_stable_TCC3........proved - complete   [shostak](0.13 s)
    conflict_3D_2D_inf_stable.............proved - complete   [shostak](2.20 s)
    conflict_vz_swap......................proved - complete   [shostak](0.20 s)
    conflict_on_open_interval.............proved - complete   [shostak](1.32 s)
    detection_inf_TCC1....................proved - complete   [shostak](0.05 s)
    detection_inf_TCC2....................proved - complete   [shostak](0.41 s)
    detection_inf_TCC3....................proved - complete   [shostak](0.21 s)
    detection_inf_TCC4....................proved - complete   [shostak](0.07 s)
    detection_inf_TCC5....................proved - complete   [shostak](1.59 s)
    detection_inf_TCC6....................proved - complete   [shostak](1.63 s)
    detection_inf_correct.................proved - complete   [shostak](2.00 s)
    detection_inf_complete................proved - complete   [shostak](2.41 s)
    conflict_detection_inf................proved - complete   [shostak](-1.71 s)
    cd3d_inf_rewrite_TCC1.................proved - complete   [shostak](0.18 s)
    cd3d_inf_rewrite_TCC2.................proved - complete   [shostak](0.18 s)
    cd3d_inf_rewrite......................proved - complete   [shostak](3.40 s)
    cd3d_inf_correct......................proved - complete   [shostak](0.25 s)
    cd3d_inf_complete.....................proved - complete   [shostak](4.77 s)
    cd3d_inf..............................proved - complete   [shostak](0.03 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (19.55 s)

 Proof summary for theory bands_util
    trk2v2_TCC1...........................proved - incomplete [shostak](0.24 s)
    trk2v2_Nzv............................proved - incomplete [shostak](0.05 s)
    gs2v2_gs_only.........................proved - complete   [shostak](0.09 s)
    gs2v2_id..............................proved - complete   [shostak](0.12 s)
    trk2v3_TCC1...........................proved - incomplete [shostak](0.20 s)
    vect2_trk2v3..........................proved - incomplete [shostak](0.04 s)
    trk2v3_Nzv............................proved - incomplete [shostak](0.03 s)
    Vtrk_3D_TCC1..........................proved - incomplete [shostak](0.24 s)
    trk2v3_trk2v3.........................proved - incomplete [shostak](0.38 s)
    trk2v3_0..............................proved - incomplete [shostak](0.08 s)
    gs2v3_gs_only.........................proved - complete   [shostak](0.09 s)
    vect2_gs2v3...........................proved - complete   [shostak](0.03 s)
    Vgs_3D_TCC1...........................proved - complete   [shostak](0.11 s)
    vs2v3_TCC1............................proved - complete   [shostak](0.03 s)
    vect2_vs2v3...........................proved - complete   [shostak](0.03 s)
    Vs_TCC1...............................proved - complete   [shostak](0.04 s)
    Theory totals: 16 formulas, 16 attempted, 16 succeeded (1.81 s)

 Proof summary for theory track
    trkgs2vect_TCC1.......................proved - incomplete [shostak](0.60 s)
    track_TCC1............................proved - complete   [shostak](0.04 s)
    sin_track.............................proved - incomplete [shostak](3.70 s)
    cos_track.............................proved - incomplete [shostak](2.08 s)
    norm_id...............................proved - incomplete [shostak](0.23 s)
    track_id..............................proved - incomplete [shostak](0.09 s)
    trkgs2vect_id.........................proved - incomplete [shostak](0.08 s)
    ordered_eps_1_TCC1....................proved - incomplete [shostak](0.45 s)
    ordered_eps_1.........................proved - incomplete [shostak](2.29 s)
    ordered_det_ge........................proved - incomplete [shostak](-.13 s)
    ordered_eps_neg_1.....................proved - incomplete [shostak](0.33 s)
    ordered_eps_1_dot_gt_0................proved - incomplete [shostak](3.19 s)
    ordered_eps_1_dot_ge_0................proved - incomplete [shostak](2.91 s)
    ordered_eps_1_dot_lt_0................proved - incomplete [shostak](1.08 s)
    ordered_eps_1_dot_le_0................proved - incomplete [shostak](1.09 s)
    Theory totals: 15 formulas, 15 attempted, 15 succeeded (18.03 s)

 Proof summary for theory gs_bands_2D
    gs_band_pos...........................proved - complete   [shostak](0.03 s)
    gs2v2_continuous......................proved - complete   [shostak](0.05 s)
    Vgs_continuous........................proved - complete   [shostak](0.06 s)
    Omega_gs_TCC1.........................proved - incomplete [shostak](0.54 s)
    Omega_gs_critical.....................proved - incomplete [shostak](0.10 s)
    gs_green_two_parallel.................proved - complete   [shostak](0.29 s)
    gs_line_color.........................proved - complete   [shostak](3.60 s)
    gs_green_band.........................proved - incomplete [shostak](0.13 s)
    gs_red_band...........................proved - incomplete [shostak](0.10 s)
    Theory totals: 9 formulas, 9 attempted, 9 succeeded (4.90 s)

 Proof summary for theory trk_bands_2D
    trk_band..............................proved - complete   [shostak](0.47 s)
    trk2v2_continuous.....................proved - incomplete [shostak](0.07 s)
    Vtrk_continuous.......................proved - incomplete [shostak](0.06 s)
    Omega_trk_spc.........................proved - incomplete [shostak](0.10 s)
    trk_special_case_invariant............proved - incomplete [shostak](0.09 s)
    Omega_trk_spc_separated...............proved - incomplete [shostak](0.71 s)
    Omega_trk_spc_critical_TCC1...........proved - incomplete [shostak](0.05 s)
    Omega_trk_spc_critical................proved - incomplete [shostak](0.12 s)
    trk_special_case_conflict_T...........proved - incomplete [shostak](0.36 s)
    trk_special_case_conflict_B...........proved - incomplete [shostak](0.12 s)
    Omega_trk_spc_conflict_T..............proved - incomplete [shostak](1.02 s)
    Omega_trk_spc_conflict_B..............proved - incomplete [shostak](0.89 s)
    Omega_trk_TCC1........................proved - incomplete [shostak](0.53 s)
    Omega_trk_critical....................proved - incomplete [shostak](0.11 s)
    trk_line_sort_eps.....................proved - complete   [shostak](0.31 s)
    trk_line_sort_eps_angle_TCC1..........proved - incomplete [shostak](0.11 s)
    trk_line_sort_eps_angle_TCC2..........proved - incomplete [shostak](0.17 s)
    trk_line_sort_eps_angle_TCC3..........proved - incomplete [shostak](0.18 s)
    trk_line_sort_eps_angle...............proved - incomplete [shostak](0.43 s)
    trk_line_sort_eps_1_angle_case1_TCC1...proved - incomplete [shostak](0.09 s)
    trk_line_sort_eps_1_angle_case1_TCC2...proved - incomplete [shostak](0.08 s)
    trk_line_sort_eps_1_angle_case1.......proved - incomplete [shostak](0.45 s)
    trk_line_sort_eps_1_angle_case2_TCC1...proved - incomplete [shostak](0.08 s)
    trk_line_sort_eps_1_angle_case2_TCC2...proved - incomplete [shostak](0.08 s)
    trk_line_sort_eps_1_angle_case2.......proved - incomplete [shostak](2.10 s)
    trk_line_color........................proved - complete   [shostak](3.02 s)
    trk_green_band........................proved - incomplete [shostak](0.51 s)
    trk_red_band..........................proved - incomplete [shostak](0.51 s)
    Theory totals: 28 formulas, 28 attempted, 28 succeeded (12.83 s)

 Proof summary for theory bands_2D
    trk_critical_TCC1....................proved - incomplete [shostak]( 0.15 s)
    trk_critical_TCC2....................proved - incomplete [shostak]( 0.11 s)
    trk_critical_rew.....................proved - incomplete [shostak]( 0.88 s)
    member_trk_critical_TCC1.............proved - incomplete [shostak]( 0.11 s)
    member_trk_critical..................proved - incomplete [shostak]( 0.10 s)
    trk_critical_composition.............proved - incomplete [shostak]( 1.05 s)
    trk_bands_TCC1.......................proved - incomplete [shostak]( 0.23 s)
    trk_bands_not_empty..................proved - incomplete [shostak](15.79 s)
    trk_bands_critical...................proved - incomplete [shostak]( 1.53 s)
    gs_critical_TCC1.....................proved - complete   [shostak]( 0.09 s)
    gs_critical_TCC2.....................proved - complete   [shostak]( 0.06 s)
    gs_critical_rew......................proved - incomplete [shostak]( 0.89 s)
    member_gs_critical...................proved - incomplete [shostak]( 0.11 s)
    gs_critical_composition..............proved - incomplete [shostak]( 1.09 s)
    gs_bands_TCC1........................proved - incomplete [shostak]( 0.06 s)
    gs_bands_TCC2........................proved - incomplete [shostak]( 0.11 s)
    gs_bands_TCC3........................proved - incomplete [shostak]( 0.11 s)
    gs_bands_TCC4........................proved - incomplete [shostak]( 0.15 s)
    gs_bands_not_empty...................proved - incomplete [shostak]( 2.65 s)
    gs_bands_critical_TCC1...............proved - complete   [shostak]( 0.04 s)
    gs_bands_critical....................proved - incomplete [shostak]( 1.01 s)
    red_trk_band?_TCC1...................proved - incomplete [shostak]( 0.04 s)
    red_trk_band?_TCC2...................proved - incomplete [shostak]( 0.07 s)
    trk_red_bands........................proved - incomplete [shostak]( 0.39 s)
    trk_green_bands......................proved - incomplete [shostak]( 0.41 s)
    red_gs_band?_TCC1....................proved - complete   [shostak]( 0.04 s)
    red_gs_band?_TCC2....................proved - complete   [shostak]( 0.07 s)
    gs_red_bands.........................proved - incomplete [shostak]( 0.37 s)
    gs_green_bands.......................proved - incomplete [shostak]( 0.41 s)
    Theory totals: 29 formulas, 29 attempted, 29 succeeded (28.14 s)

 Proof summary for theory fseqs_aux_2D
    empty_trk_fseq........................proved - incomplete [shostak](0.08 s)
    comp_trk_fseq.........................proved - incomplete [shostak](1.14 s)
    sort_trk_fseq.........................proved - incomplete [shostak](0.12 s)
    empty_gs_fseq.........................proved - incomplete [shostak](0.04 s)
    comp_gs_fseq..........................proved - complete   [shostak](1.06 s)
    sort_gs_fseq..........................proved - complete   [shostak](0.08 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.52 s)

 Proof summary for theory vertical_criterion
    closed_region_3D_t_def................proved - complete   [shostak](0.12 s)
    closed_region_3D_t_direction..........proved - complete   [shostak](1.35 s)
    closed_region_3D_sum_closed...........proved - complete   [shostak](3.00 s)
    vertical_criterion?_TCC1..............proved - complete   [shostak](0.08 s)
    vertical_criterion_sum_closed.........proved - complete   [shostak](0.45 s)
    vertical_criterion_antisymmetric......proved - complete   [shostak](1.41 s)
    vertical_criterion_independence.......proved - complete   [shostak](5.49 s)
    vertical_criterion_coordination.......proved - complete   [shostak](0.09 s)
    horizontal_meets_vertical_criterion_TCC1...proved - complete   [shostak](0.09 s)
    horizontal_meets_vertical_criterion_TCC2...proved - complete   [shostak](0.06 s)
    horizontal_meets_vertical_criterion...proved - complete   [shostak](2.14 s)
    safe_p_TCC1...........................proved - complete   [shostak](0.04 s)
    vertical_criterion_rewrite_TCC1.......proved - complete   [shostak](0.04 s)
    vertical_criterion_rewrite............proved - complete   [shostak](2.20 s)
    Theory totals: 14 formulas, 14 attempted, 14 succeeded (16.55 s)

 Proof summary for theory predicate_coordination
    coordinated_symmetric.................proved - complete   [shostak](0.12 s)
    sum_indep_coordinated.................proved - complete   [shostak](0.26 s)
    coordinated_sum_indep.................proved - complete   [shostak](0.59 s)
    sum_indep_coordinated_antisym.........proved - complete   [shostak](0.27 s)
    coordinated_antisym_sum_indep.........proved - complete   [shostak](0.62 s)
    deriv_0...............................proved - complete   [shostak](0.04 s)
    deriv_subset..........................proved - complete   [shostak](0.10 s)
    deriv_coordinated.....................proved - complete   [shostak](0.47 s)
    deriv_coordinated_1...................proved - complete   [shostak](0.05 s)
    Comb_coordinated......................proved - complete   [shostak](0.17 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (2.69 s)

 Proof summary for theory circle_solutions
    circle_solution_horizontal............proved - complete   [shostak](0.09 s)
    circle_solution_vertical_TCC1.........proved - complete   [shostak](0.05 s)
    circle_solution_vertical..............proved - complete   [shostak](0.11 s)
    circle_solution_meets_criterion.......proved - complete   [shostak](0.25 s)
    circle_solution_independence..........proved - complete   [shostak](0.04 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.54 s)

 Proof summary for theory criteria_3D
    criterion_3D?_TCC1....................proved - complete   [shostak](1.25 s)
    criterion_3D_independence.............proved - complete   [shostak](0.06 s)
    criterion_3D_coordination.............proved - complete   [shostak](0.56 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.87 s)

 Proof summary for theory gs_circle
    gs_circle_TCC1........................proved - complete   [shostak](0.02 s)
    gs_circle_TCC2........................proved - complete   [shostak](0.03 s)
    gs_circle_TCC3........................proved - complete   [shostak](0.05 s)
    gs_circle_TCC4........................proved - complete   [shostak](0.07 s)
    gs_circle_TCC5........................proved - complete   [shostak](0.04 s)
    gs_vertical_TCC1......................proved - complete   [shostak](0.05 s)
    gs_vertical_TCC2......................proved - complete   [shostak](0.06 s)
    gs_vertical_TCC3......................proved - complete   [shostak](0.07 s)
    gs_vertical_TCC4......................proved - complete   [shostak](0.13 s)
    gs_vertical_TCC5......................proved - complete   [shostak](0.08 s)
    gs_vertical_TCC6......................proved - complete   [shostak](0.05 s)
    gs_circle_nzvz........................proved - complete   [shostak](0.04 s)
    gs_circle_solution_2D_TCC1............proved - complete   [shostak](0.04 s)
    gs_circle_solution_2D.................proved - complete   [shostak](0.11 s)
    gs_circle_solution....................proved - complete   [shostak](0.77 s)
    gs_circle_independence................proved - complete   [shostak](0.05 s)
    gs_circle_complete....................proved - complete   [shostak](0.12 s)
    gs_vertical_meets_horizontal_criterion...proved - complete   [shostak](0.32 s)
    gs_vertical_meets_vertical_criterion...proved - complete   [shostak](-1.58 s)
    Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.52 s)

 Proof summary for theory trk_circle
    trk_circle_TCC1.......................proved - complete   [shostak](0.03 s)
    trk_circle_TCC2.......................proved - complete   [shostak](0.04 s)
    trk_circle_TCC3.......................proved - complete   [shostak](0.04 s)
    trk_circle_TCC4.......................proved - complete   [shostak](0.06 s)
    trk_circle_TCC5.......................proved - complete   [shostak](0.03 s)
    trk_vertical_irt_TCC1.................proved - complete   [shostak](0.06 s)
    trk_vertical_irt_TCC2.................proved - complete   [shostak](0.06 s)
    trk_vertical_irt_TCC3.................proved - complete   [shostak](0.07 s)
    trk_vertical_irt_TCC4.................proved - complete   [shostak](0.13 s)
    trk_vertical_irt_TCC5.................proved - complete   [shostak](0.08 s)
    trk_vertical_irt_TCC6.................proved - complete   [shostak](0.05 s)
    trk_circle_nzvz.......................proved - complete   [shostak](0.05 s)
    trk_circle_solution_2D_TCC1...........proved - complete   [shostak](0.04 s)
    trk_circle_solution_2D................proved - complete   [shostak](0.10 s)
    trk_circle_solution...................proved - complete   [shostak](0.81 s)
    trk_circle_independence...............proved - complete   [shostak](0.05 s)
    trk_circle_complete_TCC1..............proved - complete   [shostak](0.05 s)
    trk_circle_complete...................proved - complete   [shostak](0.12 s)
    trk_vertical_eps......................proved - complete   [shostak](0.12 s)
    trk_vertical_meets_horizontal_criterion...proved - complete   [shostak](0.32 s)
    trk_vertical_meets_vertical_criterion...proved - complete   [shostak](0.47 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (2.78 s)

 Proof summary for theory opt_vertical
    opt_vertical_TCC1.....................proved - complete   [shostak](0.03 s)
    opt_vertical_TCC2.....................proved - complete   [shostak](0.06 s)
    opt_vertical_TCC3.....................proved - complete   [shostak](0.06 s)
    opt_vertical_TCC4.....................proved - complete   [shostak](0.08 s)
    opt_vertical_TCC5.....................proved - complete   [shostak](0.03 s)
    opt_vertical_TCC6.....................proved - complete   [shostak](0.08 s)
    opt_vertical_TCC7.....................proved - complete   [shostak](0.05 s)
    opt_vertical_meets_horizontal_criterion...proved - complete   [shostak](0.32 s)
    opt_vertical_meets_vertical_criterion...proved - complete   [shostak](0.47 s)
    Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.18 s)

 Proof summary for theory vs_only
    vs_only_TCC1..........................proved - complete   [shostak](0.07 s)
    vs_only_TCC2..........................proved - complete   [shostak](0.10 s)
    vs_only_TCC3..........................proved - complete   [shostak](0.34 s)
    circle_vs_only_ge.....................proved - complete   [shostak](0.44 s)
    vs_entry_meets_circle_criterion_TCC1...proved - complete   [shostak](0.10 s)
    vs_entry_meets_circle_criterion_TCC2...proved - complete   [shostak](0.09 s)
    vs_entry_meets_circle_criterion.......proved - complete   [shostak](1.60 s)
    vs_exit_meets_circle_criterion_TCC1...proved - complete   [shostak](0.09 s)
    vs_exit_meets_circle_criterion_TCC2...proved - complete   [shostak](0.10 s)
    vs_exit_meets_circle_criterion........proved - complete   [shostak](0.95 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (3.88 s)

 Proof summary for theory vs_circle
    vs_circle_TCC1........................proved - complete   [shostak](0.03 s)
    vs_circle_TCC2........................proved - complete   [shostak](0.04 s)
    vs_circle_TCC3........................proved - complete   [shostak](0.06 s)
    vs_circle_TCC4........................proved - complete   [shostak](0.04 s)
    vs_circle_TCC5........................proved - complete   [shostak](0.03 s)
    vs_circle_meets_vertical_criterion....proved - complete   [shostak](2.16 s)
    vs_only_vs_criterion_ge_vz............proved - complete   [shostak](0.99 s)
    vs_circle_independence................proved - complete   [shostak](0.05 s)
    vs_circle_coordination................proved - complete   [shostak](0.27 s)
    Theory totals: 9 formulas, 9 attempted, 9 succeeded (3.67 s)

 Proof summary for theory vertical_cr
    hor_circle_horizontal_only............proved - complete   [shostak](0.07 s)
    vertical_cr_meets_vertical_criterion...proved - complete   [shostak](0.07 s)
    hor_circle_meets_horizontal_criterion...proved - complete   [shostak](0.08 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.22 s)

 Proof summary for theory cd_sphere
    cd_sphere_def.........................proved - complete   [shostak](1.68 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (1.68 s)

 Proof summary for theory delay_3D
    delay_conflict_free_rel...............proved - complete   [shostak](-.27 s)
    delay_conflict_free...................proved - complete   [shostak](0.17 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (-0.10 s)

 Proof summary for theory tca_3D
    IMP_metric_space_real_fun_TCC1........proved - complete   [shostak](0.03 s)
    cyl_norm_sq_diff_cont.................proved - complete   [shostak](2.36 s)
    cyl_norm_sq_IVT1......................proved - complete   [shostak](0.92 s)
    cyl_norm_sq_IVT2......................proved - complete   [shostak](0.88 s)
    cyl_norm_sq_fun_convex................proved - complete   [shostak](0.66 s)
    cyl_norm_sq_fun_cont..................proved - complete   [shostak](2.50 s)
    cyl_norm_min_exists...................proved - incomplete [shostak](0.13 s)
    cyl_norm_min_exists_inf...............proved - incomplete [shostak](1.25 s)
    conflict_at_cyl_norm_sq...............proved - complete   [shostak](0.45 s)
    minimum_info_TCC1.....................proved - complete   [shostak](0.04 s)
    minimum_info_TCC2.....................proved - complete   [shostak](0.04 s)
    horizontal_min_info_TCC1..............proved - complete   [shostak](0.91 s)
    horizontal_min_info_TCC2..............proved - complete   [shostak](0.10 s)
    horizontal_min_info_TCC3..............proved - complete   [shostak](0.03 s)
    horizontal_min_info_TCC4..............proved - complete   [shostak](0.04 s)
    horiz_vert_min_info_TCC1..............proved - complete   [shostak](0.07 s)
    horiz_vert_min_info_TCC2..............proved - complete   [shostak](0.04 s)
    horiz_vert_min_info_TCC3..............proved - complete   [shostak](0.04 s)
    horiz_vert_min_info_TCC4..............proved - complete   [shostak](0.10 s)
    cyl_intersect_time_TCC1...............proved - complete   [shostak](0.50 s)
    cyl_intersect_time_TCC2...............proved - complete   [shostak](0.22 s)
    cyl_intersect_time_TCC3...............proved - complete   [shostak](0.67 s)
    cyl_intersect_time_lt.................proved - complete   [shostak](-.73 s)
    cyl_intersect_time_id.................proved - complete   [shostak](3.91 s)
    cyl_intersect_min_info_TCC1...........proved - complete   [shostak](0.32 s)
    cyl_intersect_min_info_TCC2...........proved - complete   [shostak](0.06 s)
    cyl_intersect_min_info_TCC3...........proved - complete   [shostak](0.36 s)
    cyl_intersect_min_info_TCC4...........proved - complete   [shostak](1.82 s)
    cyl_intersect_min_info_TCC5...........proved - complete   [shostak](0.35 s)
    cyl_intersect_min_info_TCC6...........proved - complete   [shostak](0.36 s)
    cyl_intersect_min_info_TCC7...........proved - complete   [shostak](3.34 s)
    tca_3D_id_TCC1........................proved - complete   [shostak](0.03 s)
    tca_3D_id_TCC2........................proved - complete   [shostak](0.03 s)
    tca_3D_id.............................proved - complete   [shostak](1.58 s)
    tca_3D_vect2_zero.....................proved - complete   [shostak](0.38 s)
    tca_3D_vz_zero........................proved - complete   [shostak](0.51 s)
    tca_3D_def............................proved - incomplete [shostak](2.30 s)
    tca_3D_conflict.......................proved - incomplete [shostak](0.15 s)
    tca_3D_conflict_at....................proved - incomplete [shostak](0.06 s)
    tca_3D_left_decreasing................proved - incomplete [shostak](0.06 s)
    tca_3D_right_increasing...............proved - incomplete [shostak](0.07 s)
    Theory totals: 41 formulas, 41 attempted, 41 succeeded (26.92 s)

 Proof summary for theory tca_3D_interval
    tca_3D_interval_TCC1..................proved - complete   [shostak](0.31 s)
    tca_3D_interval_TCC2..................proved - complete   [shostak](0.45 s)
    tca_3D_interval_TCC3..................proved - complete   [shostak](0.46 s)
    tca_3D_interval_def...................proved - incomplete [shostak](0.08 s)
    tca_3D_interval_conflict..............proved - incomplete [shostak](0.27 s)
    tca_3D_interval_conflict_at...........proved - incomplete [shostak](0.08 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.65 s)

 Proof summary for theory cr3d
    cr_satifies_criterion_3D..............proved - complete   [shostak](0.76 s)
    cr3d_satifies_criterion_3D............proved - complete   [shostak](0.05 s)
    cr_independence.......................proved - complete   [shostak](0.05 s)
    cr3d_independence.....................proved - complete   [shostak](0.03 s)
    cr_coordination.......................proved - complete   [shostak](0.54 s)
    cr3d_coordination.....................proved - complete   [shostak](0.05 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.48 s)

 Proof summary for theory vs_bands
    vs_bands_vertical_dir_exclusive......proved - complete   [shostak]( 4.86 s)
    band_critical_on_H...................proved - complete   [shostak](30.64 s)
    vs_band_critical_B_sz_sign...........proved - complete   [shostak]( 0.63 s)
    vs_band_critical_T_sz_sign...........proved - complete   [shostak]( 0.53 s)
    vs_green_band........................proved - complete   [shostak]( 4.41 s)
    vs_red_band..........................proved - complete   [shostak]( 4.38 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (45.44 s)

 Proof summary for theory bands_3D
    trk_bands_3D_TCC1.....................proved - complete   [shostak](0.06 s)
    trk_bands_3D_TCC2.....................proved - complete   [shostak](0.08 s)
    trk_bands_3D_TCC3.....................proved - complete   [shostak](0.44 s)
    trk_bands_3D_TCC4.....................proved - complete   [shostak](0.45 s)
    trk_bands_3D_TCC5.....................proved - complete   [shostak](0.42 s)
    trk_bands_3D_TCC6.....................proved - complete   [shostak](0.19 s)
    trk_bands_3D_TCC7.....................proved - incomplete [shostak](0.26 s)
    trk_bands_3D_TCC8.....................proved - complete   [shostak](0.05 s)
    trk_bands_3D_TCC9.....................proved - incomplete [shostak](0.20 s)
    gs_bands_3D_TCC1......................proved - complete   [shostak](0.65 s)
    gs_bands_3D_TCC2......................proved - complete   [shostak](0.17 s)
    vs_bands_3D_TCC1......................proved - complete   [shostak](0.17 s)
    vs_bands_3D_TCC2......................proved - complete   [shostak](0.05 s)
    vs_bands_3D_TCC3......................proved - complete   [shostak](0.12 s)
    vs_bands_3D_TCC4......................proved - complete   [shostak](0.14 s)
    vs_bands_3D_TCC5......................proved - complete   [shostak](0.09 s)
    vs_bands_3D_TCC6......................proved - complete   [shostak](0.06 s)
    vs_bands_3D_TCC7......................proved - complete   [shostak](0.23 s)
    vs_bands_3D_TCC8......................proved - complete   [shostak](0.04 s)
    vs_bands_3D_TCC9......................proved - complete   [shostak](0.17 s)
    trk_bands_3D_not_empty................proved - incomplete [shostak](0.39 s)
    trk_bands_last_TCC1...................proved - incomplete [shostak](0.06 s)
    trk_bands_last........................proved - incomplete [shostak](0.59 s)
    trk_bands_first.......................proved - incomplete [shostak](0.61 s)
    gs_bands_3D_not_empty.................proved - incomplete [shostak](0.31 s)
    gs_bands_last_TCC1....................proved - incomplete [shostak](0.05 s)
    gs_bands_last.........................proved - incomplete [shostak](0.47 s)
    gs_bands_first........................proved - incomplete [shostak](0.46 s)
    vs_bands_3D_not_empty.................proved - incomplete [shostak](0.32 s)
    vs_bands_last_TCC1....................proved - incomplete [shostak](0.05 s)
    vs_bands_last.........................proved - incomplete [shostak](0.52 s)
    vs_bands_first........................proved - complete   [shostak](0.50 s)
    red_trk_band_3D?_TCC1.................proved - incomplete [shostak](0.06 s)
    red_trk_band_3D?_TCC2.................proved - incomplete [shostak](0.07 s)
    red_gs_band_3D?_TCC1..................proved - complete   [shostak](0.04 s)
    red_gs_band_3D?_TCC2..................proved - complete   [shostak](0.05 s)
    red_vs_band_3D?_TCC1..................proved - complete   [shostak](0.04 s)
    red_vs_band_3D?_TCC2..................proved - complete   [shostak](0.04 s)
    trk_red_bands_3D......................proved - incomplete [shostak](7.40 s)
    trk_green_bands_3D....................proved - incomplete [shostak](7.22 s)
    trk_bands_equivalence_TCC1............proved - incomplete [shostak](0.18 s)
    trk_bands_equivalence.................proved - incomplete [shostak](0.89 s)
    gs_red_bands_3D.......................proved - incomplete [shostak](7.22 s)
    gs_green_bands_3D.....................proved - incomplete [shostak](8.89 s)
    gs_bands_equivalence_TCC1.............proved - incomplete [shostak](0.12 s)
    gs_bands_equivalence..................proved - incomplete [shostak](0.80 s)
    vs_red_bands_3D.......................proved - complete   [shostak](5.27 s)
    vs_green_bands_3D.....................proved - complete   [shostak](5.28 s)
    vs_bands_equivalence_TCC1.............proved - complete   [shostak](0.17 s)
    vs_bands_equivalence..................proved - incomplete [shostak](0.80 s)
    Theory totals: 50 formulas, 50 attempted, 50 succeeded (52.91 s)

 Proof summary for theory bands_1D
    vs_critical_TCC1......................proved - complete   [shostak](0.07 s)
    vs_critical_TCC2......................proved - complete   [shostak](0.06 s)
    vs_critical_rew.......................proved - complete   [shostak](0.73 s)
    member_vs_critical....................proved - complete   [shostak](0.13 s)
    vs_critical_composition...............proved - complete   [shostak](0.92 s)
    vs_bands_TCC1.........................proved - complete   [shostak](0.16 s)
    vs_bands_not_empty....................proved - incomplete [shostak](0.93 s)
    vs_bands_critical.....................proved - complete   [shostak](0.48 s)
    red_vs_band?_TCC1.....................proved - complete   [shostak](0.04 s)
    red_vs_band?_TCC2.....................proved - complete   [shostak](0.04 s)
    vs_red_bands..........................proved - complete   [shostak](0.33 s)
    vs_green_bands........................proved - complete   [shostak](0.34 s)
    Theory totals: 12 formulas, 12 attempted, 12 succeeded (4.23 s)

 Proof summary for theory fseqs_aux_vertical
    empty_vs_fseq.........................proved - complete   [shostak](0.04 s)
    comp_vs_fseq..........................proved - complete   [shostak](1.06 s)
    sort_vs_fseq..........................proved - complete   [shostak](0.08 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.18 s)

 Proof summary for theory repulsive_iterative
    man_pos_seq_TCC1.....................proved - complete   [shostak]( 0.04 s)
    man_pos_seq_TCC2.....................proved - complete   [shostak]( 0.04 s)
    man_pos_seq_TCC3.....................proved - complete   [shostak]( 0.02 s)
    man_pos_seq_test.....................proved - complete   [shostak]( 0.15 s)
    manuever_position_at_def.............proved - complete   [shostak]( 0.78 s)
    repulsive_criteria_iterative_TCC1....proved - complete   [shostak]( 0.22 s)
    repulsive_criteria_iterative_TCC2....proved - complete   [shostak]( 0.21 s)
    repulsive_criteria_iterative_repulsive...proved - complete   [shostak]( 1.14 s)
    repulsive_criteria_iterative_reduces_seq...proved - complete   [shostak]( 7.19 s)
    repulsive_criteria_iterative_reduces...proved - complete   [shostak]( 0.73 s)
    repulsive_criteria_iterative_reduces_seq_divergent_special...proved - complete   [shostak](34.26 s)
    repulsive_criteria_iterative_reduces_seq_divergent...proved - complete   [shostak]( 7.62 s)
    repulsive_criteria_iterative_reduces_seq_div...proved - complete   [shostak]( 2.87 s)
    repulsive_criteria_iterative_reduces_div...proved - complete   [shostak]( 1.60 s)
    repulsive_criteria_iterative_coordinated...proved - complete   [shostak]( 5.62 s)
    Theory totals: 15 formulas, 15 attempted, 15 succeeded (62.48 s)

 Proof summary for theory losr_iterative
    incr_trk_vect_TCC1....................proved - complete   [shostak](0.42 s)
    losr_trk_iter_i_TCC1..................proved - complete   [shostak](0.11 s)
    losr_trk_iter_i_TCC2..................proved - complete   [shostak](0.09 s)
    losr_trk_iter_i_TCC3..................proved - complete   [shostak](0.12 s)
    losr_trk_iter_i_TCC4..................proved - complete   [shostak](0.11 s)
    losr_trk_iter_i_TCC5..................proved - complete   [shostak](0.31 s)
    losr_trk_iter_TCC1....................proved - complete   [shostak](0.03 s)
    losr_trk_iter_TCC2....................proved - complete   [shostak](0.05 s)
    losr_trk_iter_TCC3....................proved - complete   [shostak](0.04 s)
    losr_trk_iter_TCC4....................proved - complete   [shostak](0.06 s)
    losr_trk_iter_TCC5....................proved - complete   [shostak](0.03 s)
    incr_gs_vect_TCC1.....................proved - complete   [shostak](0.11 s)
    losr_gs_iter_i_TCC1...................proved - complete   [shostak](0.13 s)
    losr_gs_iter_i_TCC2...................proved - complete   [shostak](0.18 s)
    losr_gs_iter_i_TCC3...................proved - complete   [shostak](0.21 s)
    losr_gs_iter_i_TCC4...................proved - complete   [shostak](0.52 s)
    losr_gs_iter_i_TCC5...................proved - complete   [shostak](-.81 s)
    losr_gs_iter_i_TCC6...................proved - complete   [shostak](0.15 s)
    losr_gs_iter_TCC1.....................proved - complete   [shostak](0.03 s)
    losr_gs_iter_TCC2.....................proved - complete   [shostak](0.05 s)
    losr_gs_iter_TCC3.....................proved - complete   [shostak](0.21 s)
    losr_gs_iter_TCC4.....................proved - complete   [shostak](0.24 s)
    losr_gs_iter_TCC5.....................proved - complete   [shostak](0.10 s)
    Theory totals: 23 formulas, 23 attempted, 23 succeeded (2.49 s)

 Proof summary for theory kb
    angle_from_to_TCC1...................proved - incomplete [shostak]( 0.10 s)
    angle_from_to_id.....................proved - incomplete [shostak]( 0.50 s)
    angle_from_to_lt_pi..................proved - incomplete [shostak]( 0.38 s)
    angle_from_to_test...................proved - incomplete [shostak]( 1.54 s)
    chirel_star_TCC1.....................proved - complete   [shostak]( 0.14 s)
    chirel_star_equiv_TCC1...............proved - complete   [shostak]( 0.14 s)
    chirel_star_equiv....................proved - incomplete [shostak]( 0.31 s)
    chirel_star_test_TCC1................proved - incomplete [shostak]( 0.80 s)
    chirel_star_test.....................proved - incomplete [shostak]( 1.55 s)
    chirel_star_0_id.....................proved - incomplete [shostak]( 0.08 s)
    chirel_star_1_id.....................proved - incomplete [shostak]( 0.60 s)
    chirel_star_f_entry_scaf.............proved - incomplete [shostak]( 2.82 s)
    chirel_star_tangent..................proved - incomplete [shostak]( 8.36 s)
    chirel_star_f_entry..................proved - incomplete [shostak]( 1.07 s)
    chi_hc_TCC1..........................proved - incomplete [shostak]( 0.08 s)
    chi_hc_TCC2..........................proved - complete   [shostak]( 0.03 s)
    chi_hc_TCC3..........................proved - incomplete [shostak]( 0.09 s)
    chi_hc_TCC4..........................proved - incomplete [shostak]( 0.21 s)
    sin_track_minus......................proved - incomplete [shostak]( 0.57 s)
    chi_hc_sin_equivalence_2_TCC1........proved - incomplete [shostak]( 0.17 s)
    chi_hc_sin_equivalence_2.............proved - incomplete [shostak]( 4.01 s)
    chi_hc_track_eq......................proved - incomplete [shostak]( 1.92 s)
    chi_hc_1_chirel_TCC1.................proved - incomplete [shostak]( 0.47 s)
    chi_hc_1_chirel_TCC2.................proved - incomplete [shostak]( 0.20 s)
    chi_hc_1_chirel......................proved - incomplete [shostak]( 3.34 s)
    chi_hc_f_chirel_TCC1.................proved - incomplete [shostak]( 0.39 s)
    chi_hc_f_chirel_TCC2.................proved - incomplete [shostak]( 0.36 s)
    chi_hc_f_chirel......................proved - incomplete [shostak]( 3.36 s)
    chi_hc_0_id_TCC1.....................proved - incomplete [shostak]( 0.17 s)
    chi_hc_0_id..........................proved - incomplete [shostak]( 0.66 s)
    chi_hc_0_id_rel_TCC1.................proved - incomplete [shostak]( 0.20 s)
    chi_hc_0_id_rel_TCC2.................proved - incomplete [shostak]( 0.40 s)
    chi_hc_0_id_rel......................proved - incomplete [shostak]( 3.86 s)
    kb_0_id..............................proved - incomplete [shostak]( 0.11 s)
    kb_tangent_line......................proved - incomplete [shostak]( 0.50 s)
    kb_is_independent_TCC1...............proved - complete   [shostak]( 0.04 s)
    kb_is_independent_TCC2...............proved - incomplete [shostak]( 1.01 s)
    kb_is_independent_TCC3...............proved - incomplete [shostak]( 1.06 s)
    kb_is_independent_TCC4...............proved - incomplete [shostak]( 1.06 s)
    kb_is_independent....................proved - incomplete [shostak]( 0.08 s)
    kb_is_not_coordinated_1..............proved - incomplete [shostak](17.79 s)
    kb_is_not_coordinated_2..............proved - incomplete [shostak](16.98 s)
    kb_is_not_coordinated_3..............proved - incomplete [shostak](11.99 s)
    Theory totals: 43 formulas, 43 attempted, 43 succeeded (89.52 s)

 Proof summary for theory flightplan
    j_TCC1................................proved - complete   [shostak](0.03 s)
    FlightPlan_TCC1.......................proved - complete   [shostak](0.03 s)
    FlightPlan_TCC2.......................proved - complete   [shostak](0.03 s)
    start_time_TCC1.......................proved - complete   [shostak](0.03 s)
    end_time_TCC1.........................proved - complete   [shostak](0.03 s)
    flight_plan_ascending_time............proved - complete   [shostak](0.17 s)
    flight_plan_unique_times..............proved - complete   [shostak](0.04 s)
    FlightTimes_TCC1......................proved - complete   [shostak](0.11 s)
    velocity_TCC1.........................proved - complete   [shostak](0.03 s)
    velocity_TCC2.........................proved - complete   [shostak](0.03 s)
    velocity_TCC3.........................proved - complete   [shostak](0.08 s)
    velocity_def..........................proved - complete   [shostak](0.13 s)
    FlightPlan_nz_TCC1....................proved - complete   [shostak](0.04 s)
    segment_max_TCC1......................proved - incomplete [shostak](0.21 s)
    segment_TCC1..........................proved - complete   [shostak](0.07 s)
    segment_TCC2..........................proved - incomplete [shostak](0.27 s)
    segment_def_TCC1......................proved - incomplete [shostak](0.26 s)
    segment_def...........................proved - incomplete [shostak](0.20 s)
    segment_index.........................proved - incomplete [shostak](0.12 s)
    segment_max...........................proved - incomplete [shostak](0.15 s)
    segment_ident_TCC1....................proved - incomplete [shostak](0.10 s)
    segment_ident.........................proved - incomplete [shostak](0.08 s)
    location_at_TCC1......................proved - incomplete [shostak](0.08 s)
    location_at_check_TCC1................proved - complete   [shostak](0.07 s)
    location_at_check.....................proved - incomplete [shostak](0.21 s)
    Theory totals: 25 formulas, 25 attempted, 25 succeeded (2.60 s)

 Proof summary for theory cd3d_si
    j_TCC1................................proved - complete   [shostak](0.03 s)
    FlightPlanRelevant_TCC1...............proved - complete   [shostak](0.03 s)
    FlightPlanRelevant_TCC2...............proved - complete   [shostak](0.06 s)
    FlightPlanRelevant_TCC3...............proved - complete   [shostak](0.04 s)
    FlightPlanRelevant_TCC4...............proved - complete   [shostak](0.18 s)
    seg_lh_top_TCC1.......................proved - complete   [shostak](0.03 s)
    seg_lh_top_TCC2.......................proved - complete   [shostak](0.02 s)
    seg_lh_bottom_TCC1....................proved - complete   [shostak](0.11 s)
    seg_lh_top_positive...................proved - complete   [shostak](0.12 s)
    nontrivial_lookahead_TCC1.............proved - complete   [shostak](0.20 s)
    nontrivial_lookahead..................proved - complete   [shostak](0.38 s)
    conflict_3D_rew_TCC1..................proved - complete   [shostak](0.24 s)
    conflict_3D_rew.......................proved - incomplete [shostak](5.42 s)
    conflict_3D_flightplan_open_interval_TCC1...proved - complete   [shostak](0.17 s)
    conflict_3D_flightplan_open_interval...proved - incomplete [shostak](2.40 s)
    conflict_3D_rew_absolute_time_TCC1....proved - complete   [shostak](0.26 s)
    conflict_3D_rew_absolute_time_TCC2....proved - complete   [shostak](0.26 s)
    conflict_3D_rew_absolute_time.........proved - incomplete [shostak](2.27 s)
    cd3d_ind?_TCC1........................proved - complete   [shostak](0.44 s)
    cd3d_si?_TCC1.........................proved - complete   [shostak](0.03 s)
    cd3d_ind_correct......................proved - complete   [shostak](0.24 s)
    cd3d_ind_complete.....................proved - complete   [shostak](0.70 s)
    cd3d_si_correct.......................proved - incomplete [shostak](0.06 s)
    cd3d_si_complete......................proved - incomplete [shostak](0.06 s)
    Theory totals: 24 formulas, 24 attempted, 24 succeeded (13.74 s)

 Proof summary for theory cd3d_ii
    FlightPlanRelevant2_TCC1..............proved - complete   [shostak](0.02 s)
    FlightPlanRelevant2_TCC2..............proved - complete   [shostak](0.04 s)
    FlightPlanRelevant2_TCC3..............proved - complete   [shostak](0.04 s)
    FlightPlanRelevant2_TCC4..............proved - complete   [shostak](0.05 s)
    FlightPlanRelevant2_TCC5..............proved - complete   [shostak](0.03 s)
    FlightPlanRelevant2_TCC6..............proved - complete   [shostak](0.22 s)
    FlightTimesRelevant2_TCC1.............proved - complete   [shostak](0.03 s)
    FlightTimesRelevant2_TCC2.............proved - complete   [shostak](0.09 s)
    FlightTimesLimited2_TCC1..............proved - complete   [shostak](0.03 s)
    FlightTimesLimited2_TCC2..............proved - complete   [shostak](0.03 s)
    FlightTimesLimited2_TCC3..............proved - complete   [shostak](0.03 s)
    FlightTimesLimited2_TCC4..............proved - complete   [shostak](0.14 s)
    conflict_3D_ii?_TCC1..................proved - complete   [shostak](0.04 s)
    conflict_3D_ii?_TCC2..................proved - complete   [shostak](0.04 s)
    seg_allowable_TCC1....................proved - incomplete [shostak](0.47 s)
    seg_allowable.........................proved - incomplete [shostak](0.23 s)
    time_in_range_TCC1....................proved - incomplete [shostak](0.12 s)
    time_in_range_TCC2....................proved - incomplete [shostak](0.28 s)
    time_in_range_TCC3....................proved - incomplete [shostak](0.16 s)
    time_in_range.........................proved - incomplete [shostak](0.74 s)
    limited_bounds_TCC1...................proved - incomplete [shostak](0.18 s)
    limited_bounds_TCC2...................proved - incomplete [shostak](0.35 s)
    limited_bounds........................proved - incomplete [shostak](0.36 s)
    upper_seg_bounds_TCC1.................proved - incomplete [shostak](0.14 s)
    upper_seg_bounds......................proved - incomplete [shostak](0.33 s)
    cd3d_ii_rew_TCC1......................proved - incomplete [shostak](0.20 s)
    cd3d_ii_rew_TCC2......................proved - incomplete [shostak](0.16 s)
    cd3d_ii_rew_TCC3......................proved - incomplete [shostak](0.29 s)
    cd3d_ii_rew...........................proved - incomplete [shostak](2.89 s)
    cd3d_ii_ind?_TCC1.....................proved - complete   [shostak](0.03 s)
    cd3d_ii_ind?_TCC2.....................proved - complete   [shostak](0.37 s)
    cd3d_ii_ind?_TCC3.....................proved - complete   [shostak](0.18 s)
    cd3d_ii_ind?_TCC4.....................proved - complete   [shostak](0.15 s)
    cd3d_ii_ind?_TCC5.....................proved - complete   [shostak](0.11 s)
    some_cd3d_ii..........................proved - complete   [shostak](0.25 s)
    cd3d_ii?_TCC1.........................proved - complete   [shostak](0.03 s)
    cd3d_ii_ind_correct...................proved - incomplete [shostak](1.08 s)
    cd3d_ii_ind_complete..................proved - incomplete [shostak](1.29 s)
    cd3d_si_complete_parameters_TCC1......proved - complete   [shostak](0.09 s)
    cd3d_si_complete_parameters_TCC2......proved - incomplete [shostak](2.42 s)
    cd3d_si_complete_parameters...........proved - incomplete [shostak](0.12 s)
    cd3d_ii_correct.......................proved - incomplete [shostak](0.35 s)
    cd3d_ii_complete......................proved - incomplete [shostak](2.24 s)
    Theory totals: 43 formulas, 43 attempted, 43 succeeded (16.45 s)

 Proof summary for theory bands_si
    FlightPlanRelevant_nz_TCC1............proved - complete   [shostak](0.06 s)
    FlightPlanRelevant_nz_TCC2............proved - complete   [shostak](0.04 s)
    FlightPlanRelevant_nz_TCC3............proved - complete   [shostak](0.04 s)
    FlightPlanRelevant_nz_TCC4............proved - complete   [shostak](0.08 s)
    FlightPlanRelevant_nz_TCC5............proved - complete   [shostak](0.26 s)
    trk_bands_si_i_TCC1...................proved - complete   [shostak](0.05 s)
    trk_bands_si_i_TCC2...................proved - complete   [shostak](0.05 s)
    trk_bands_si_i_TCC3...................proved - incomplete [shostak](0.22 s)
    trk_bands_si_i_TCC4...................proved - complete   [shostak](3.61 s)
    trk_bands_si_i_TCC5...................proved - complete   [shostak](2.32 s)
    trk_bands_si_i_TCC6...................proved - complete   [shostak](0.31 s)
    expand_trk_bands_si_i_TCC1............proved - complete   [shostak](0.04 s)
    expand_trk_bands_si_i_TCC2............proved - complete   [shostak](0.05 s)
    expand_trk_bands_si_i_TCC3............proved - complete   [shostak](0.07 s)
    expand_trk_bands_si_i_TCC4............proved - complete   [shostak](0.51 s)
    expand_trk_bands_si_i_TCC5............proved - complete   [shostak](0.30 s)
    expand_trk_bands_si_i_TCC6............proved - complete   [shostak](0.26 s)
    expand_trk_bands_si_i.................proved - incomplete [shostak](0.21 s)
    trk_bands_si_TCC1.....................proved - complete   [shostak](0.04 s)
    trk_bands_si_TCC2.....................proved - complete   [shostak](0.07 s)
    trk_bands_si_TCC3.....................proved - complete   [shostak](0.05 s)
    trk_bands_si_TCC4.....................proved - incomplete [shostak](0.07 s)
    gs_bands_si_i_TCC1....................proved - complete   [shostak](0.17 s)
    gs_bands_si_TCC1......................proved - incomplete [shostak](0.08 s)
    vs_bands_si_i_TCC1....................proved - complete   [shostak](0.17 s)
    vs_bands_si_TCC1......................proved - complete   [shostak](0.07 s)
    red_trk_band_fp?_TCC1.................proved - incomplete [shostak](0.07 s)
    red_trk_band_fp?_TCC2.................proved - incomplete [shostak](0.07 s)
    red_gs_band_fp?_TCC1..................proved - complete   [shostak](0.06 s)
    red_gs_band_fp?_TCC2..................proved - complete   [shostak](0.06 s)
    red_vs_band_fp?_TCC1..................proved - complete   [shostak](0.05 s)
    red_vs_band_fp?_TCC2..................proved - complete   [shostak](0.06 s)
    segdefs_TCC1..........................proved - complete   [shostak](0.04 s)
    segdefs_TCC2..........................proved - complete   [shostak](0.04 s)
    segdefs_TCC3..........................proved - complete   [shostak](0.08 s)
    segdefs...............................proved - complete   [shostak](0.14 s)
    trk_bands_si_combines_TCC1............proved - complete   [shostak](0.05 s)
    trk_bands_si_combines.................proved - incomplete [shostak](0.33 s)
    empty_no_members_TCC1.................proved - complete   [shostak](0.04 s)
    empty_no_members......................proved - complete   [shostak](0.05 s)
    trk_bands_si_component_TCC1...........proved - complete   [shostak](0.05 s)
    trk_bands_si_component_TCC2...........proved - complete   [shostak](0.07 s)
    trk_bands_si_component_TCC3...........proved - complete   [shostak](0.09 s)
    trk_bands_si_component_TCC4...........proved - complete   [shostak](0.54 s)
    trk_bands_si_component_TCC5...........proved - complete   [shostak](0.31 s)
    trk_bands_si_component_TCC6...........proved - complete   [shostak](0.23 s)
    trk_bands_si_component................proved - incomplete [shostak](0.34 s)
    trk_bands_si_length...................proved - incomplete [shostak](0.36 s)
    trk_bands_si_i_relevant_TCC1..........proved - complete   [shostak](0.05 s)
    trk_bands_si_i_relevant...............proved - incomplete [shostak](0.42 s)
    trk_bands_si_i_relevant_has_2.........proved - incomplete [shostak](0.51 s)
    trk_bands_si_relevant_TCC1............proved - complete   [shostak](0.05 s)
    trk_bands_si_relevant.................proved - incomplete [shostak](0.71 s)
    trk_bands_si_relevant_has_2...........proved - incomplete [shostak](0.53 s)
    trk_bands_si_equivalence_TCC1.........proved - complete   [shostak](0.05 s)
    trk_bands_si_equivalence_TCC2.........proved - incomplete [shostak](0.18 s)
    trk_bands_si_equivalence..............proved - incomplete [shostak](2.01 s)
    trk_red_bands_si......................proved - incomplete [shostak](-1.68 s)
    trk_green_bands_si....................proved - incomplete [shostak](0.48 s)
    gs_bands_si_combines..................proved - incomplete [shostak](0.36 s)
    gs_bands_si_component.................proved - incomplete [shostak](0.34 s)
    gs_bands_si_equivalence_TCC1..........proved - incomplete [shostak](0.13 s)
    gs_bands_si_equivalence...............proved - incomplete [shostak](1.99 s)
    gs_red_bands_si.......................proved - incomplete [shostak](0.47 s)
    gs_green_bands_si.....................proved - incomplete [shostak](0.46 s)
    vs_bands_si_combines..................proved - complete   [shostak](0.33 s)
    vs_bands_si_component.................proved - complete   [shostak](0.34 s)
    vs_bands_si_equivalence_TCC1..........proved - complete   [shostak](0.12 s)
    vs_bands_si_equivalence...............proved - incomplete [shostak](1.96 s)
    vs_red_bands_si.......................proved - incomplete [shostak](0.46 s)
    vs_green_bands_si.....................proved - incomplete [shostak](0.43 s)
    Theory totals: 71 formulas, 71 attempted, 71 succeeded (23.02 s)

Grand Totals: 1210 proofs, 1210 attempted, 1210 succeeded (820.29 s)