Quelle  vectors.summary   Sprache: unbekannt

*** 
*** top (17:34:1 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
*** 
 Proof summary for theory top
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory vectors
    times_TCC1............................proved - complete   [shostak](0.07 s)
    sqv_TCC1..............................proved - complete   [shostak](0.05 s)
    sqv_rew...............................proved - complete   [shostak](0.04 s)
    sqv_sos...............................proved - complete   [shostak](0.04 s)
    unity_TCC1............................proved - complete   [shostak](0.34 s)
    comp_distr_add........................proved - complete   [shostak](0.01 s)
    comp_distr_sub........................proved - complete   [shostak](0.02 s)
    comp_distr_scal.......................proved - complete   [shostak](0.02 s)
    comp_distr_neg........................proved - complete   [shostak](0.02 s)
    comp_zero.............................proved - complete   [shostak](0.01 s)
    comps_eq..............................proved - complete   [shostak](0.10 s)
    norm_comp_eq_0........................proved - complete   [shostak](0.12 s)
    norm_sqv_eq_0.........................proved - complete   [shostak](0.02 s)
    norm_eq_0.............................proved - complete   [shostak](0.04 s)
    norm_zero.............................proved - complete   [shostak](0.01 s)
    sqv_zero..............................proved - complete   [shostak](0.03 s)
    sqv_eq_0..............................proved - complete   [shostak](0.01 s)
    v_neq_zero............................proved - complete   [shostak](0.02 s)
    v_neq_0...............................proved - complete   [shostak](0.15 s)
    sq_dot_eq_0...........................proved - complete   [shostak](0.03 s)
    nzv_comp_neq_0........................proved - complete   [shostak](0.06 s)
    nz_norm_gt_0..........................proved - complete   [shostak](0.01 s)
    nz_sqv_gt_0...........................proved - complete   [shostak](0.01 s)
    normalized_nz.........................proved - complete   [shostak](0.02 s)
    neg_nzv...............................proved - complete   [shostak](0.05 s)
    nz_nzv................................proved - complete   [shostak](0.09 s)
    neg_zero..............................proved - complete   [shostak](0.03 s)
    add_zero_left.........................proved - complete   [shostak](0.03 s)
    add_zero_right........................proved - complete   [shostak](0.03 s)
    add_comm..............................proved - complete   [shostak](0.03 s)
    add_assoc.............................proved - complete   [shostak](0.06 s)
    add_move_left.........................proved - complete   [shostak](0.07 s)
    add_move_right........................proved - complete   [shostak](0.08 s)
    add_move_both.........................proved - complete   [shostak](0.07 s)
    add_neg_sub...........................proved - complete   [shostak](0.04 s)
    add_cancel............................proved - complete   [shostak](0.04 s)
    add_cancel_neg........................proved - complete   [shostak](0.05 s)
    add_cancel2...........................proved - complete   [shostak](0.04 s)
    add_cancel_neg2.......................proved - complete   [shostak](0.04 s)
    add_cancel_left.......................proved - complete   [shostak](0.08 s)
    add_cancel_right......................proved - complete   [shostak](0.08 s)
    add_eq_zero...........................proved - complete   [shostak](0.07 s)
    neg_shift.............................proved - complete   [shostak](0.06 s)
    sub_cancel_left.......................proved - complete   [shostak](0.07 s)
    sub_cancel_right......................proved - complete   [shostak](0.06 s)
    sub_zero_left.........................proved - complete   [shostak](0.02 s)
    sub_zero_right........................proved - complete   [shostak](0.03 s)
    sub_eq_args...........................proved - complete   [shostak](0.02 s)
    sub_eq_zero...........................proved - complete   [shostak](0.03 s)
    sub_cancel............................proved - complete   [shostak](0.03 s)
    sub_cancel_neg........................proved - complete   [shostak](0.04 s)
    neg_add_left..........................proved - complete   [shostak](0.04 s)
    neg_add_right.........................proved - complete   [shostak](0.04 s)
    neg_distr_sub.........................proved - complete   [shostak](0.03 s)
    neg_neg...............................proved - complete   [shostak](0.02 s)
    neg_distr_add.........................proved - complete   [shostak](0.05 s)
    dot_neg_left..........................proved - complete   [shostak](0.18 s)
    dot_neg_right.........................proved - complete   [shostak](0.19 s)
    neg_dot_neg...........................proved - complete   [shostak](0.02 s)
    dot_zero_left.........................proved - complete   [shostak](0.06 s)
    dot_zero_right........................proved - complete   [shostak](0.05 s)
    dot_comm..............................proved - complete   [shostak](0.05 s)
    dot_assoc.............................proved - complete   [shostak](0.09 s)
    dot_eq_args_ge........................proved - complete   [shostak](0.04 s)
    add_comm_assoc_left...................proved - complete   [shostak](0.02 s)
    add_comm_assoc_right..................proved - complete   [shostak](0.02 s)
    dot_add_right.........................proved - complete   [shostak](0.19 s)
    dot_add_left..........................proved - complete   [shostak](0.20 s)
    dot_sub_right.........................proved - complete   [shostak](0.04 s)
    dot_sub_left..........................proved - complete   [shostak](0.05 s)
    dot_divby.............................proved - complete   [shostak](0.15 s)
    dot_scal_left.........................proved - complete   [shostak](0.10 s)
    dot_scal_right........................proved - complete   [shostak](0.10 s)
    dot_scal_comm_assoc...................proved - complete   [shostak](0.04 s)
    scal_comm_assoc.......................proved - complete   [shostak](0.05 s)
    dot_scal_canon........................proved - complete   [shostak](0.09 s)
    scal_add_left.........................proved - complete   [shostak](0.08 s)
    scal_sub_left.........................proved - complete   [shostak](0.09 s)
    scal_add_right........................proved - complete   [shostak](0.10 s)
    scal_sub_right........................proved - complete   [shostak](0.09 s)
    scal_assoc............................proved - complete   [shostak](0.05 s)
    scal_neg..............................proved - complete   [shostak](0.04 s)
    scal_cross............................proved - complete   [shostak](0.12 s)
    scal_div_mult_left....................proved - complete   [shostak](0.16 s)
    scal_div_mult_right...................proved - complete   [shostak](0.15 s)
    scal_zero.............................proved - complete   [shostak](0.03 s)
    scal_0................................proved - complete   [shostak](0.04 s)
    scal_1................................proved - complete   [shostak](0.05 s)
    scal_neg_1............................proved - complete   [shostak](0.04 s)
    scal_cancel...........................proved - complete   [shostak](0.09 s)
    scal_eq_zero..........................proved - complete   [shostak](0.06 s)
    dot_ge_dist...........................proved - complete   [shostak](0.39 s)
    dot_gt_dist...........................proved - complete   [shostak](0.39 s)
    idem_right............................proved - complete   [shostak](0.10 s)
    sqv_neg...............................proved - complete   [shostak](0.07 s)
    sqv_add...............................proved - complete   [shostak](0.09 s)
    sqv_scal..............................proved - complete   [shostak](0.06 s)
    sqv_sub...............................proved - complete   [shostak](0.12 s)
    sqv_sub_scal..........................proved - complete   [shostak](0.30 s)
    sqv_sym...............................proved - complete   [shostak](0.11 s)
    sqrt_sqv_sq...........................proved - complete   [shostak](0.05 s)
    norm_sym..............................proved - complete   [shostak](0.02 s)
    norm_neg..............................proved - complete   [shostak](0.02 s)
    dot_sq_norm...........................proved - complete   [shostak](0.01 s)
    sq_norm...............................proved - complete   [shostak](0.01 s)
    sqrt_sqv_norm.........................proved - complete   [shostak](0.01 s)
    norms_eq_sqv..........................proved - complete   [shostak](0.03 s)
    norms_eq_sos..........................proved - complete   [shostak](0.02 s)
    norm_le_sqv...........................proved - complete   [shostak](0.02 s)
    norm_lt_sqv...........................proved - complete   [shostak](0.02 s)
    norm_scal.............................proved - complete   [shostak](0.09 s)
    caret_TCC1............................proved - complete   [shostak](0.07 s)
    norm_normalize........................proved - complete   [shostak](0.01 s)
    dot_normalize.........................proved - complete   [shostak](0.08 s)
    normalize_normalize...................proved - complete   [shostak](0.14 s)
    normalized_id.........................proved - complete   [shostak](0.09 s)
    normalize_scal........................proved - complete   [shostak](0.33 s)
    cauchy_schwarz........................proved - complete   [shostak](0.41 s)
    dot_norm..............................proved - complete   [shostak](0.14 s)
    schwarz...............................proved - complete   [shostak](0.05 s)
    schwarz_cor...........................proved - complete   [shostak](0.24 s)
    norm_triangle.........................proved - complete   [shostak](0.09 s)
    norm_add_le...........................proved - complete   [shostak](0.33 s)
    norm_sub_le...........................proved - complete   [shostak](0.34 s)
    norm_sub_ge...........................proved - complete   [shostak](0.04 s)
    norm_ge_comps.........................proved - complete   [shostak](0.26 s)
    sq_norm_dist..........................proved - complete   [shostak](0.29 s)
    parallel_refl.........................proved - complete   [shostak](0.02 s)
    parallel_symm.........................proved - complete   [shostak](0.05 s)
    parallel_trans........................proved - complete   [shostak](0.05 s)
    parallel_zero.........................proved - complete   [shostak](0.02 s)
    dir_parallel..........................proved - complete   [shostak](0.02 s)
    pythagorean...........................proved - complete   [shostak](0.07 s)
    norm_add_ge_left......................proved - complete   [shostak](0.09 s)
    norm_add_ge_right.....................proved - complete   [shostak](0.02 s)
    Theory totals: 135 formulas, 135 attempted, 135 succeeded (10.86 s)

 Proof summary for theory nvectors
    difference_TCC1.......................proved - complete   [shostak](0.02 s)
    difference_TCC2.......................proved - complete   [shostak](0.01 s)
    plus_TCC1.............................proved - complete   [shostak](0.04 s)
    plus_TCC2.............................proved - complete   [shostak](0.01 s)
    difference_TCC3.......................proved - complete   [shostak](0.01 s)
    times_TCC1............................proved - complete   [shostak](0.02 s)
    times_TCC2............................proved - complete   [shostak](0.03 s)
    sqv_TCC1..............................proved - complete   [shostak](0.05 s)
    sq_TCC1...............................proved - complete   [shostak](0.01 s)
    zero_TCC1.............................proved - complete   [shostak](0.01 s)
    zero_TCC2.............................proved - complete   [shostak](0.07 s)
    unity_TCC1............................proved - complete   [shostak](0.41 s)
    const_vec_TCC1........................proved - complete   [shostak](0.01 s)
    comp_distr_add........................proved - complete   [shostak](0.02 s)
    comp_distr_sub........................proved - complete   [shostak](0.02 s)
    comp_distr_scal.......................proved - complete   [shostak](0.01 s)
    comp_zero.............................proved - complete   [shostak](0.02 s)
    comp_eq...............................proved - complete   [shostak](0.05 s)
    add_zero_left_TCC1....................proved - complete   [shostak](0.01 s)
    add_zero_left.........................proved - complete   [shostak](0.05 s)
    add_zero_right_TCC1...................proved - complete   [shostak](0.02 s)
    add_zero_right........................proved - complete   [shostak](0.05 s)
    add_comm_TCC1.........................proved - complete   [shostak](0.02 s)
    add_comm..............................proved - complete   [shostak](0.01 s)
    add_assoc_TCC1........................proved - complete   [shostak](0.01 s)
    add_assoc_TCC2........................proved - complete   [shostak](0.02 s)
    add_assoc_TCC3........................proved - complete   [shostak](0.01 s)
    add_assoc.............................proved - complete   [shostak](0.05 s)
    add_move_right........................proved - complete   [shostak](0.13 s)
    add_move_both.........................proved - complete   [shostak](0.14 s)
    add_neg_sub_TCC1......................proved - complete   [shostak](0.01 s)
    add_neg_sub...........................proved - complete   [shostak](0.01 s)
    add_cancel_TCC1.......................proved - complete   [shostak](0.02 s)
    add_cancel............................proved - complete   [shostak](0.09 s)
    add_cancel_neg_TCC1...................proved - complete   [shostak](0.01 s)
    add_cancel_neg_TCC2...................proved - complete   [shostak](0.02 s)
    add_cancel_neg........................proved - complete   [shostak](0.09 s)
    add_cancel2_TCC1......................proved - complete   [shostak](0.02 s)
    add_cancel2...........................proved - complete   [shostak](0.09 s)
    add_cancel_neg2_TCC1..................proved - complete   [shostak](0.01 s)
    add_cancel_neg2.......................proved - complete   [shostak](0.09 s)
    sub_zero_left.........................proved - complete   [shostak](0.04 s)
    sub_zero_right........................proved - complete   [shostak](0.05 s)
    sub_eq_args...........................proved - complete   [shostak](0.03 s)
    sub_eq_zero_TCC1......................proved - complete   [shostak](0.02 s)
    sub_eq_zero...........................proved - complete   [shostak](0.12 s)
    sub_cancel_TCC1.......................proved - complete   [shostak](0.01 s)
    sub_cancel............................proved - complete   [shostak](0.03 s)
    sub_cancel_neg_TCC1...................proved - complete   [shostak](0.02 s)
    sub_cancel_neg........................proved - complete   [shostak](0.02 s)
    neg_add_left_TCC1.....................proved - complete   [shostak](0.01 s)
    neg_add_left..........................proved - complete   [shostak](0.02 s)
    neg_add_right.........................proved - complete   [shostak](0.02 s)
    neg_distr_sub.........................proved - complete   [shostak](0.03 s)
    neg_neg...............................proved - complete   [shostak](0.04 s)
    neg_distr_add_TCC1....................proved - complete   [shostak](0.01 s)
    neg_distr_add.........................proved - complete   [shostak](0.04 s)
    dot_neg_left..........................proved - complete   [shostak](0.11 s)
    dot_neg_right.........................proved - complete   [shostak](0.10 s)
    dot_neg_sq............................proved - complete   [shostak](0.06 s)
    dot_zero_left_TCC1....................proved - complete   [shostak](0.01 s)
    dot_zero_left.........................proved - complete   [shostak](0.10 s)
    dot_zero_right........................proved - complete   [shostak](0.06 s)
    dot_comm..............................proved - complete   [shostak](0.08 s)
    dot_assoc_TCC1........................proved - complete   [shostak](0.02 s)
    dot_assoc.............................proved - complete   [shostak](0.23 s)
    dot_eq_args_ge........................proved - complete   [shostak](0.13 s)
    dot_distr_add_left....................proved - complete   [shostak](0.32 s)
    dot_distr_add_right_TCC1..............proved - complete   [shostak](0.01 s)
    dot_distr_add_right_TCC2..............proved - complete   [shostak](0.02 s)
    dot_distr_add_right...................proved - complete   [shostak](0.19 s)
    dot_distr_sub_left_TCC1...............proved - complete   [shostak](0.02 s)
    dot_distr_sub_left....................proved - complete   [shostak](0.20 s)
    dot_distr_sub_right_TCC1..............proved - complete   [shostak](0.01 s)
    dot_distr_sub_right...................proved - complete   [shostak](0.22 s)
    dot_divby.............................proved - complete   [shostak](0.12 s)
    dot_scal_left_TCC1....................proved - complete   [shostak](0.01 s)
    dot_scal_left.........................proved - complete   [shostak](0.12 s)
    dot_scal_right_TCC1...................proved - complete   [shostak](0.02 s)
    dot_scal_right........................proved - complete   [shostak](0.12 s)
    dot_scal_assoc........................proved - complete   [shostak](0.04 s)
    dot_scal_canon_TCC1...................proved - complete   [shostak](0.01 s)
    dot_scal_canon........................proved - complete   [shostak](0.12 s)
    dot_scal_distr_add_TCC1...............proved - complete   [shostak](0.01 s)
    dot_scal_distr_add....................proved - complete   [shostak](0.06 s)
    dot_scal_distr_sub....................proved - complete   [shostak](0.07 s)
    scal_add_distr_TCC1...................proved - complete   [shostak](0.01 s)
    scal_add_distr........................proved - complete   [shostak](0.07 s)
    scal_sub_distr........................proved - complete   [shostak](0.06 s)
    scal_zero.............................proved - complete   [shostak](0.02 s)
    scal_0................................proved - complete   [shostak](0.02 s)
    scal_1................................proved - complete   [shostak](0.07 s)
    scal_cancel...........................proved - complete   [shostak](0.19 s)
    scal_dot_eq_0.........................proved - complete   [shostak](0.08 s)
    dot_ge_dist_TCC1......................proved - complete   [shostak](0.01 s)
    dot_ge_dist_TCC2......................proved - complete   [shostak](0.05 s)
    dot_ge_dist...........................proved - complete   [shostak](0.33 s)
    dot_gt_dist_TCC1......................proved - complete   [shostak](0.05 s)
    dot_gt_dist...........................proved - complete   [shostak](0.26 s)
    sq_dot_eq.............................proved - complete   [shostak](0.13 s)
    sqv_sq................................proved - complete   [shostak](0.05 s)
    sq_sqv................................proved - complete   [shostak](0.05 s)
    sq_lem................................proved - complete   [shostak](0.04 s)
    sqv_lem...............................proved - complete   [shostak](0.05 s)
    sqv_zero..............................proved - complete   [shostak](0.03 s)
    sqv_eq_0..............................proved - complete   [shostak](0.05 s)
    sqv_neg...............................proved - complete   [shostak](0.05 s)
    sqv_add_TCC1..........................proved - complete   [shostak](0.02 s)
    sqv_add...............................proved - complete   [shostak](0.14 s)
    sqv_sub...............................proved - complete   [shostak](0.14 s)
    sqv_sym...............................proved - complete   [shostak](0.12 s)
    sqv_scal..............................proved - complete   [shostak](0.05 s)
    sqrt_sqv_sq...........................proved - complete   [shostak](0.06 s)
    norm_sym..............................proved - complete   [shostak](0.02 s)
    norm_neg..............................proved - complete   [shostak](0.04 s)
    dot_sq_norm...........................proved - complete   [shostak](0.02 s)
    sq_norm...............................proved - complete   [shostak](0.02 s)
    sqrt_sqv_norm.........................proved - complete   [shostak](0.02 s)
    norm_eq_0.............................proved - complete   [shostak](0.07 s)
    norms_eq_sqv..........................proved - complete   [shostak](0.09 s)
    norm_scal.............................proved - complete   [shostak](0.10 s)
    idem_right............................proved - complete   [shostak](0.11 s)
    caret_TCC1............................proved - complete   [shostak](0.07 s)
    caret_TCC2............................proved - complete   [shostak](0.17 s)
    dot_normalize_TCC1....................proved - complete   [shostak](0.06 s)
    dot_normalize_TCC2....................proved - complete   [shostak](0.17 s)
    dot_normalize.........................proved - complete   [shostak](0.10 s)
    normalize_normalize_TCC1..............proved - complete   [shostak](0.03 s)
    normalize_normalize...................proved - complete   [shostak](0.12 s)
    sqv_minus_dot_TCC1....................proved - complete   [shostak](0.01 s)
    sqv_minus_dot.........................proved - complete   [shostak](0.37 s)
    cauchy_schwarz........................proved - complete   [shostak](0.44 s)
    dot_norm..............................proved - complete   [shostak](0.14 s)
    norm_add_le...........................proved - complete   [shostak](0.34 s)
    norm_sub_le...........................proved - complete   [shostak](0.37 s)
    norm_sub_ge...........................proved - complete   [shostak](0.06 s)
    norm_ge_comps.........................proved - complete   [shostak](0.14 s)
    norm_triangle_TCC1....................proved - complete   [shostak](0.03 s)
    norm_triangle.........................proved - complete   [shostak](0.37 s)
    nzvec_has_nz..........................proved - complete   [shostak](0.05 s)
    nzvec_neq_zero_TCC1...................proved - complete   [shostak](0.01 s)
    nzvec_neq_zero........................proved - complete   [shostak](0.05 s)
    v_neq_0...............................proved - complete   [shostak](0.12 s)
    Theory totals: 143 formulas, 143 attempted, 143 succeeded (10.87 s)

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

 Proof summary for theory vect2D
    vect2D_0..............................proved - complete   [shostak](0.03 s)
    vect2D_1..............................proved - complete   [shostak](0.04 s)
    Eq2D..................................proved - complete   [shostak](0.05 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.12 s)

 Proof summary for theory vect3D
    Eq3D..................................proved - complete   [shostak](0.07 s)
    vect3D_0..............................proved - complete   [shostak](0.03 s)
    vect3D_1..............................proved - complete   [shostak](0.04 s)
    vect3D_2..............................proved - complete   [shostak](0.03 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.17 s)

 Proof summary for theory vectors_2D
    sqv_TCC1..............................proved - complete   [shostak](0.03 s)
    sqv_rew...............................proved - complete   [shostak](0.03 s)
    sqv_sos...............................proved - complete   [shostak](0.03 s)
    iv_TCC1...............................proved - complete   [shostak](0.00 s)
    jv_TCC1...............................proved - complete   [shostak](0.01 s)
    basis.................................proved - complete   [shostak](0.01 s)
    vx_distr_add..........................proved - complete   [shostak](0.00 s)
    vy_distr_add..........................proved - complete   [shostak](0.00 s)
    vx_distr_sub..........................proved - complete   [shostak](0.01 s)
    vy_distr_sub..........................proved - complete   [shostak](0.00 s)
    vx_scal...............................proved - complete   [shostak](0.01 s)
    vy_scal...............................proved - complete   [shostak](0.00 s)
    vx_neg................................proved - complete   [shostak](0.01 s)
    vy_neg................................proved - complete   [shostak](0.00 s)
    comp_eq_x.............................proved - complete   [shostak](0.00 s)
    comp_eq_y.............................proved - complete   [shostak](0.01 s)
    comps_eq..............................proved - complete   [shostak](0.02 s)
    comp_zero_x...........................proved - complete   [shostak](0.00 s)
    comp_zero_y...........................proved - complete   [shostak](0.00 s)
    norm_xy_eq_0..........................proved - complete   [shostak](0.08 s)
    norm_sqv_eq_0.........................proved - complete   [shostak](0.02 s)
    norm_eq_0.............................proved - complete   [shostak](0.02 s)
    norm_zero.............................proved - complete   [shostak](0.01 s)
    sqv_zero..............................proved - complete   [shostak](0.00 s)
    sqv_eq_0..............................proved - complete   [shostak](0.02 s)
    v_neq_zero............................proved - complete   [shostak](0.00 s)
    sq_dot_eq_0...........................proved - complete   [shostak](0.04 s)
    nzv_xy_neq_0..........................proved - complete   [shostak](0.03 s)
    nz_norm_gt_0..........................proved - complete   [shostak](0.01 s)
    nz_sqv_gt_0...........................proved - complete   [shostak](0.00 s)
    nz_nvz_left...........................proved - complete   [shostak](0.00 s)
    nz_nvz_right..........................proved - complete   [shostak](0.00 s)
    normalized_nz.........................proved - complete   [shostak](0.01 s)
    neg_nzv...............................proved - complete   [shostak](0.02 s)
    nz_nzv................................proved - complete   [shostak](0.14 s)
    neg_zero..............................proved - complete   [shostak](0.00 s)
    add_zero_left.........................proved - complete   [shostak](0.01 s)
    add_zero_right........................proved - complete   [shostak](0.01 s)
    add_comm..............................proved - complete   [shostak](0.00 s)
    add_assoc.............................proved - complete   [shostak](0.02 s)
    add_move_left.........................proved - complete   [shostak](0.08 s)
    add_move_right........................proved - complete   [shostak](0.09 s)
    add_move_both.........................proved - complete   [shostak](0.10 s)
    add_neg_sub...........................proved - complete   [shostak](0.00 s)
    add_cancel............................proved - complete   [shostak](0.02 s)
    add_cancel_neg........................proved - complete   [shostak](0.07 s)
    add_cancel2...........................proved - complete   [shostak](0.01 s)
    add_cancel_neg2.......................proved - complete   [shostak](0.02 s)
    add_cancel_left.......................proved - complete   [shostak](0.02 s)
    add_cancel_right......................proved - complete   [shostak](0.01 s)
    add_eq_zero...........................proved - complete   [shostak](0.08 s)
    neg_shift.............................proved - complete   [shostak](0.04 s)
    sub_cancel_left.......................proved - complete   [shostak](0.05 s)
    sub_cancel_right......................proved - complete   [shostak](0.03 s)
    sub_zero_left.........................proved - complete   [shostak](0.00 s)
    sub_zero_right........................proved - complete   [shostak](0.00 s)
    sub_eq_args...........................proved - complete   [shostak](0.00 s)
    sub_eq_zero...........................proved - complete   [shostak](0.04 s)
    sub_cancel............................proved - complete   [shostak](0.00 s)
    sub_cancel_neg........................proved - complete   [shostak](0.02 s)
    neg_add_left..........................proved - complete   [shostak](0.00 s)
    neg_add_right.........................proved - complete   [shostak](0.01 s)
    neg_distr_sub.........................proved - complete   [shostak](0.01 s)
    neg_neg...............................proved - complete   [shostak](0.02 s)
    neg_distr_add.........................proved - complete   [shostak](0.03 s)
    dot_neg_left..........................proved - complete   [shostak](0.04 s)
    dot_neg_right.........................proved - complete   [shostak](0.04 s)
    neg_dot_neg...........................proved - complete   [shostak](0.03 s)
    dot_zero_left.........................proved - complete   [shostak](0.01 s)
    dot_zero_right........................proved - complete   [shostak](0.00 s)
    dot_comm..............................proved - complete   [shostak](0.05 s)
    dot_assoc.............................proved - complete   [shostak](0.03 s)
    dot_eq_args_ge........................proved - complete   [shostak](0.02 s)
    add_comm_assoc_left...................proved - complete   [shostak](0.03 s)
    add_comm_assoc_right..................proved - complete   [shostak](0.03 s)
    dot_add_right.........................proved - complete   [shostak](0.06 s)
    dot_add_left..........................proved - complete   [shostak](0.10 s)
    dot_sub_right.........................proved - complete   [shostak](0.06 s)
    dot_sub_left..........................proved - complete   [shostak](0.11 s)
    add_dot_add...........................proved - complete   [shostak](0.11 s)
    dot_divby.............................proved - complete   [shostak](0.09 s)
    dot_scal_left.........................proved - complete   [shostak](0.03 s)
    dot_scal_right........................proved - complete   [shostak](0.06 s)
    dot_scal_comm_assoc...................proved - complete   [shostak](0.03 s)
    scal_assoc............................proved - complete   [shostak](0.03 s)
    scal_comm_assoc.......................proved - complete   [shostak](0.05 s)
    dot_scal_canon........................proved - complete   [shostak](0.02 s)
    scal_add_left.........................proved - complete   [shostak](0.06 s)
    scal_sub_left.........................proved - complete   [shostak](0.05 s)
    scal_add_right........................proved - complete   [shostak](0.05 s)
    scal_sub_right........................proved - complete   [shostak](0.06 s)
    scal_neg..............................proved - complete   [shostak](0.00 s)
    scal_cross............................proved - complete   [shostak](0.10 s)
    scal_zero.............................proved - complete   [shostak](0.01 s)
    scal_0................................proved - complete   [shostak](0.00 s)
    scal_1................................proved - complete   [shostak](0.04 s)
    scal_neg_1............................proved - complete   [shostak](0.01 s)
    scal_cancel...........................proved - complete   [shostak](0.08 s)
    scal_div_mult_left....................proved - complete   [shostak](0.12 s)
    scal_div_mult_right...................proved - complete   [shostak](0.15 s)
    scal_eq_zero..........................proved - complete   [shostak](0.05 s)
    dot_ge_dist...........................proved - complete   [shostak](0.21 s)
    dot_gt_dist...........................proved - complete   [shostak](0.21 s)
    idem_right............................proved - complete   [shostak](0.08 s)
    sqv_neg...............................proved - complete   [shostak](0.03 s)
    sqv_add...............................proved - complete   [shostak](0.13 s)
    sqv_scal..............................proved - complete   [shostak](0.02 s)
    sqv_sub...............................proved - complete   [shostak](0.12 s)
    sqv_sub_scal..........................proved - complete   [shostak](0.32 s)
    sqv_sym...............................proved - complete   [shostak](0.09 s)
    sqrt_sqv_sq...........................proved - complete   [shostak](0.05 s)
    norm_sym..............................proved - complete   [shostak](0.01 s)
    norm_neg..............................proved - complete   [shostak](0.04 s)
    dot_sq_norm...........................proved - complete   [shostak](0.03 s)
    sq_norm...............................proved - complete   [shostak](0.10 s)
    sqv_eq_norm_eq........................proved - complete   [shostak](0.01 s)
    norm_eq_sqv_eq........................proved - complete   [shostak](0.02 s)
    sqrt_sqv_norm.........................proved - complete   [shostak](0.01 s)
    norms_eq_sqv..........................proved - complete   [shostak](0.01 s)
    norms_eq_sos..........................proved - complete   [shostak](0.02 s)
    norm_le_sqv...........................proved - complete   [shostak](0.01 s)
    norm_lt_sqv...........................proved - complete   [shostak](0.00 s)
    norm_scal.............................proved - complete   [shostak](0.09 s)
    caret_TCC1............................proved - complete   [shostak](0.05 s)
    norm_normalize........................proved - complete   [shostak](0.01 s)
    dot_normalize.........................proved - complete   [shostak](0.06 s)
    normalize_normalize...................proved - complete   [shostak](0.09 s)
    normalized_id.........................proved - complete   [shostak](0.08 s)
    normalize_scal........................proved - complete   [shostak](0.30 s)
    cauchy_schwarz........................proved - complete   [shostak](0.49 s)
    dot_norm..............................proved - complete   [shostak](0.13 s)
    schwarz...............................proved - complete   [shostak](0.04 s)
    schwarz_converse......................proved - complete   [shostak](4.22 s)
    schwarz_cor...........................proved - complete   [shostak](0.23 s)
    norm_triangle.........................proved - complete   [shostak](0.50 s)
    norm_add_le...........................proved - complete   [shostak](0.31 s)
    norm_sub_le...........................proved - complete   [shostak](0.34 s)
    norm_sub_ge...........................proved - complete   [shostak](0.04 s)
    norm_ge_comps.........................proved - complete   [shostak](0.11 s)
    sq_norm_dist..........................proved - complete   [shostak](0.42 s)
    parallel_refl.........................proved - complete   [shostak](0.01 s)
    parallel_symm.........................proved - complete   [shostak](0.04 s)
    parallel_trans........................proved - complete   [shostak](0.04 s)
    parallel_zero.........................proved - complete   [shostak](0.02 s)
    dir_parallel..........................proved - complete   [shostak](0.01 s)
    pythagorean...........................proved - complete   [shostak](0.05 s)
    norm_add_ge_left......................proved - complete   [shostak](0.09 s)
    norm_add_ge_right.....................proved - complete   [shostak](0.01 s)
    bolzano_weierstrass...................proved - complete   [shostak](1.12 s)
    Theory totals: 149 formulas, 149 attempted, 149 succeeded (13.71 s)

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

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

 Proof summary for theory vectors_3D
    sqv_TCC1..............................proved - complete   [shostak](0.04 s)
    sqv_rew...............................proved - complete   [shostak](0.01 s)
    sqv_sos...............................proved - complete   [shostak](0.04 s)
    basis.................................proved - complete   [shostak](0.01 s)
    vx_distr_add..........................proved - complete   [shostak](0.00 s)
    vy_distr_add..........................proved - complete   [shostak](0.00 s)
    vz_distr_add..........................proved - complete   [shostak](0.04 s)
    vx_distr_sub..........................proved - complete   [shostak](0.01 s)
    vy_distr_sub..........................proved - complete   [shostak](0.00 s)
    vz_distr_sub..........................proved - complete   [shostak](0.01 s)
    vx_scal...............................proved - complete   [shostak](0.00 s)
    vy_scal...............................proved - complete   [shostak](0.01 s)
    vz_scal...............................proved - complete   [shostak](0.00 s)
    vx_neg................................proved - complete   [shostak](0.00 s)
    vy_neg................................proved - complete   [shostak](0.01 s)
    vz_neg................................proved - complete   [shostak](0.00 s)
    comp_eq_x.............................proved - complete   [shostak](0.01 s)
    comp_eq_y.............................proved - complete   [shostak](0.00 s)
    comp_eq_z.............................proved - complete   [shostak](0.00 s)
    comps_eq..............................proved - complete   [shostak](0.03 s)
    comp_zero_x...........................proved - complete   [shostak](0.00 s)
    comp_zero_y...........................proved - complete   [shostak](0.01 s)
    comp_zero_z...........................proved - complete   [shostak](0.00 s)
    norm_xyz_eq_0.........................proved - complete   [shostak](0.14 s)
    norm_sqv_eq_0.........................proved - complete   [shostak](0.02 s)
    norm_eq_0.............................proved - complete   [shostak](0.02 s)
    norm_zero.............................proved - complete   [shostak](0.01 s)
    sqv_zero..............................proved - complete   [shostak](0.00 s)
    sqv_eq_0..............................proved - complete   [shostak](0.01 s)
    v_neq_zero............................proved - complete   [shostak](0.01 s)
    sq_dot_eq_0...........................proved - complete   [shostak](0.02 s)
    nzv_xyz_neq_0.........................proved - complete   [shostak](0.03 s)
    nz_norm_gt_0..........................proved - complete   [shostak](0.01 s)
    nz_sqv_gt_0...........................proved - complete   [shostak](0.00 s)
    nz_nvz_left...........................proved - complete   [shostak](0.00 s)
    nz_nvz_middle.........................proved - complete   [shostak](0.01 s)
    nz_nvz_right..........................proved - complete   [shostak](0.00 s)
    normalized_nz.........................proved - complete   [shostak](0.01 s)
    neg_nzv...............................proved - complete   [shostak](0.03 s)
    nz_nzv................................proved - complete   [shostak](0.21 s)
    neg_zero..............................proved - complete   [shostak](0.00 s)
    add_zero_left.........................proved - complete   [shostak](0.02 s)
    add_zero_right........................proved - complete   [shostak](0.01 s)
    add_comm..............................proved - complete   [shostak](0.01 s)
    add_assoc.............................proved - complete   [shostak](0.04 s)
    add_move_left.........................proved - complete   [shostak](0.12 s)
    add_move_right........................proved - complete   [shostak](0.12 s)
    add_move_both.........................proved - complete   [shostak](0.12 s)
    add_neg_sub...........................proved - complete   [shostak](0.01 s)
    add_cancel............................proved - complete   [shostak](0.01 s)
    add_cancel_neg........................proved - complete   [shostak](0.10 s)
    add_cancel2...........................proved - complete   [shostak](0.02 s)
    add_cancel_neg2.......................proved - complete   [shostak](0.02 s)
    add_cancel_left.......................proved - complete   [shostak](0.02 s)
    add_cancel_right......................proved - complete   [shostak](0.02 s)
    add_eq_zero...........................proved - complete   [shostak](0.10 s)
    neg_shift.............................proved - complete   [shostak](0.05 s)
    sub_cancel_left.......................proved - complete   [shostak](0.08 s)
    sub_cancel_right......................proved - complete   [shostak](0.04 s)
    sub_zero_left.........................proved - complete   [shostak](0.01 s)
    sub_zero_right........................proved - complete   [shostak](0.01 s)
    sub_eq_args...........................proved - complete   [shostak](0.01 s)
    sub_eq_zero...........................proved - complete   [shostak](0.05 s)
    sub_cancel............................proved - complete   [shostak](0.01 s)
    sub_cancel_neg........................proved - complete   [shostak](0.02 s)
    neg_add_left..........................proved - complete   [shostak](0.01 s)
    neg_add_right.........................proved - complete   [shostak](0.01 s)
    neg_distr_sub.........................proved - complete   [shostak](0.01 s)
    neg_neg...............................proved - complete   [shostak](0.03 s)
    neg_distr_add.........................proved - complete   [shostak](0.04 s)
    dot_neg_left..........................proved - complete   [shostak](0.05 s)
    dot_neg_right.........................proved - complete   [shostak](0.06 s)
    neg_dot_neg...........................proved - complete   [shostak](0.05 s)
    dot_zero_left.........................proved - complete   [shostak](0.01 s)
    dot_zero_right........................proved - complete   [shostak](0.00 s)
    dot_comm..............................proved - complete   [shostak](0.08 s)
    dot_assoc.............................proved - complete   [shostak](0.05 s)
    dot_eq_args_ge........................proved - complete   [shostak](0.04 s)
    add_comm_assoc_left...................proved - complete   [shostak](0.04 s)
    add_comm_assoc_right..................proved - complete   [shostak](0.04 s)
    dot_add_right.........................proved - complete   [shostak](0.09 s)
    dot_add_left..........................proved - complete   [shostak](0.16 s)
    dot_sub_right.........................proved - complete   [shostak](0.08 s)
    dot_sub_left..........................proved - complete   [shostak](0.15 s)
    dot_divby.............................proved - complete   [shostak](0.12 s)
    dot_scal_left.........................proved - complete   [shostak](0.04 s)
    dot_scal_right........................proved - complete   [shostak](0.09 s)
    dot_scal_comm_assoc...................proved - complete   [shostak](0.05 s)
    scal_comm_assoc.......................proved - complete   [shostak](0.07 s)
    dot_scal_canon........................proved - complete   [shostak](0.03 s)
    scal_add_left.........................proved - complete   [shostak](0.07 s)
    scal_sub_left.........................proved - complete   [shostak](0.08 s)
    scal_add_right........................proved - complete   [shostak](0.07 s)
    scal_sub_right........................proved - complete   [shostak](0.08 s)
    scal_assoc............................proved - complete   [shostak](0.05 s)
    scal_neg..............................proved - complete   [shostak](0.01 s)
    scal_cross............................proved - complete   [shostak](0.14 s)
    scal_zero.............................proved - complete   [shostak](0.01 s)
    scal_0................................proved - complete   [shostak](0.00 s)
    scal_1................................proved - complete   [shostak](0.04 s)
    scal_neg_1............................proved - complete   [shostak](0.01 s)
    scal_cancel...........................proved - complete   [shostak](0.11 s)
    scal_div_mult_left....................proved - complete   [shostak](0.17 s)
    scal_div_mult_right...................proved - complete   [shostak](0.22 s)
    scal_eq_zero..........................proved - complete   [shostak](0.08 s)
    dot_ge_dist...........................proved - complete   [shostak](0.33 s)
    dot_gt_dist...........................proved - complete   [shostak](0.33 s)
    idem_right............................proved - complete   [shostak](0.10 s)
    sqv_neg...............................proved - complete   [shostak](0.05 s)
    sqv_add...............................proved - complete   [shostak](0.17 s)
    sqv_scal..............................proved - complete   [shostak](0.04 s)
    sqv_sub...............................proved - complete   [shostak](0.17 s)
    sqv_sub_scal..........................proved - complete   [shostak](0.37 s)
    sqv_sym...............................proved - complete   [shostak](0.15 s)
    sqrt_sqv_sq...........................proved - complete   [shostak](0.05 s)
    norm_sym..............................proved - complete   [shostak](0.01 s)
    norm_neg..............................proved - complete   [shostak](0.06 s)
    dot_sq_norm...........................proved - complete   [shostak](0.06 s)
    sq_norm...............................proved - complete   [shostak](0.13 s)
    sqrt_sqv_norm.........................proved - complete   [shostak](0.01 s)
    norms_eq_sqv..........................proved - complete   [shostak](0.02 s)
    norms_eq_sos..........................proved - complete   [shostak](0.01 s)
    norm_le_sqv...........................proved - complete   [shostak](0.00 s)
    norm_lt_sqv...........................proved - complete   [shostak](0.01 s)
    norm_scal.............................proved - complete   [shostak](0.08 s)
    caret_TCC1............................proved - complete   [shostak](0.06 s)
    norm_normalize........................proved - complete   [shostak](0.00 s)
    dot_normalize.........................proved - complete   [shostak](0.07 s)
    normalize_normalize...................proved - complete   [shostak](0.08 s)
    normalized_id.........................proved - complete   [shostak](0.08 s)
    normalize_scal........................proved - complete   [shostak](0.29 s)
    cauchy_schwarz........................proved - complete   [shostak](0.64 s)
    dot_norm..............................proved - complete   [shostak](0.13 s)
    schwarz...............................proved - complete   [shostak](0.04 s)
    schwarz_cor...........................proved - complete   [shostak](0.22 s)
    norm_triangle.........................proved - complete   [shostak](0.77 s)
    norm_add_le...........................proved - complete   [shostak](0.31 s)
    norm_sub_le...........................proved - complete   [shostak](0.34 s)
    norm_sub_ge...........................proved - complete   [shostak](0.03 s)
    norm_ge_comps.........................proved - complete   [shostak](0.25 s)
    sq_norm_dist..........................proved - complete   [shostak](0.58 s)
    parallel_refl.........................proved - complete   [shostak](0.01 s)
    parallel_symm.........................proved - complete   [shostak](0.03 s)
    parallel_trans........................proved - complete   [shostak](0.04 s)
    parallel_zero.........................proved - complete   [shostak](0.01 s)
    dir_parallel..........................proved - complete   [shostak](0.01 s)
    pythagorean...........................proved - complete   [shostak](0.05 s)
    norm_add_ge_left......................proved - complete   [shostak](0.08 s)
    norm_add_ge_right.....................proved - complete   [shostak](0.01 s)
    Theory totals: 149 formulas, 149 attempted, 149 succeeded (10.73 s)

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

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

 Proof summary for theory vectors_4D
    sqv_TCC1..............................proved - complete   [shostak](0.05 s)
    sqv_rew...............................proved - complete   [shostak](0.00 s)
    sqv_sos...............................proved - complete   [shostak](0.05 s)
    basis.................................proved - complete   [shostak](0.01 s)
    vx_distr_add..........................proved - complete   [shostak](0.01 s)
    vy_distr_add..........................proved - complete   [shostak](0.00 s)
    vz_distr_add..........................proved - complete   [shostak](0.05 s)
    vt_distr_add..........................proved - complete   [shostak](0.00 s)
    vx_distr_sub..........................proved - complete   [shostak](0.01 s)
    vy_distr_sub..........................proved - complete   [shostak](0.00 s)
    vz_distr_sub..........................proved - complete   [shostak](0.01 s)
    vt_distr_sub..........................proved - complete   [shostak](0.01 s)
    vx_scal...............................proved - complete   [shostak](0.00 s)
    vy_scal...............................proved - complete   [shostak](0.00 s)
    vz_scal...............................proved - complete   [shostak](0.01 s)
    vt_scal...............................proved - complete   [shostak](0.00 s)
    vx_neg................................proved - complete   [shostak](0.01 s)
    vy_neg................................proved - complete   [shostak](0.00 s)
    vz_neg................................proved - complete   [shostak](0.00 s)
    vt_neg................................proved - complete   [shostak](0.01 s)
    comp_eq_x.............................proved - complete   [shostak](0.00 s)
    comp_eq_y.............................proved - complete   [shostak](0.01 s)
    comp_eq_z.............................proved - complete   [shostak](0.00 s)
    comp_eq_t.............................proved - complete   [shostak](0.01 s)
    comps_eq..............................proved - complete   [shostak](0.02 s)
    comp_zero_x...........................proved - complete   [shostak](0.01 s)
    comp_zero_y...........................proved - complete   [shostak](0.00 s)
    comp_zero_z...........................proved - complete   [shostak](0.00 s)
    comp_zero_t...........................proved - complete   [shostak](0.01 s)
    norm_xyz_eq_0.........................proved - complete   [shostak](0.21 s)
    norm_sqv_eq_0.........................proved - complete   [shostak](0.02 s)
    norm_eq_0.............................proved - complete   [shostak](0.03 s)
    norm_zero.............................proved - complete   [shostak](0.01 s)
    sqv_zero..............................proved - complete   [shostak](0.00 s)
    sqv_eq_0..............................proved - complete   [shostak](0.01 s)
    v_neq_zero............................proved - complete   [shostak](0.00 s)
    sq_dot_eq_0...........................proved - complete   [shostak](0.02 s)
    nzv_xyz_neq_0.........................proved - complete   [shostak](0.03 s)
    nz_norm_gt_0..........................proved - complete   [shostak](0.01 s)
    nz_sqv_gt_0...........................proved - complete   [shostak](0.00 s)
    nz_nvz_left...........................proved - complete   [shostak](0.00 s)
    nz_nvz_middle.........................proved - complete   [shostak](0.01 s)
    nz_nvz_right..........................proved - complete   [shostak](0.00 s)
    nz_nvz_time...........................proved - complete   [shostak](0.01 s)
    normalized_nz.........................proved - complete   [shostak](0.01 s)
    neg_nzv...............................proved - complete   [shostak](0.03 s)
    nz_nzv................................proved - complete   [shostak](0.28 s)
    neg_zero..............................proved - complete   [shostak](0.01 s)
    add_zero_left.........................proved - complete   [shostak](0.02 s)
    add_zero_right........................proved - complete   [shostak](0.01 s)
    add_comm..............................proved - complete   [shostak](0.01 s)
    add_assoc.............................proved - complete   [shostak](0.05 s)
    add_move_left.........................proved - complete   [shostak](0.16 s)
    add_move_right........................proved - complete   [shostak](0.16 s)
    add_move_both.........................proved - complete   [shostak](0.17 s)
    add_neg_sub...........................proved - complete   [shostak](0.01 s)
    add_cancel............................proved - complete   [shostak](0.02 s)
    add_cancel_neg........................proved - complete   [shostak](0.12 s)
    add_cancel2...........................proved - complete   [shostak](0.02 s)
    add_cancel_neg2.......................proved - complete   [shostak](0.01 s)
    add_cancel_left.......................proved - complete   [shostak](0.03 s)
    add_cancel_right......................proved - complete   [shostak](0.02 s)
    add_eq_zero...........................proved - complete   [shostak](0.14 s)
    neg_shift.............................proved - complete   [shostak](0.07 s)
    sub_cancel_left.......................proved - complete   [shostak](0.10 s)
    sub_cancel_right......................proved - complete   [shostak](0.05 s)
    sub_zero_left.........................proved - complete   [shostak](0.00 s)
    sub_zero_right........................proved - complete   [shostak](0.02 s)
    sub_eq_args...........................proved - complete   [shostak](0.00 s)
    sub_eq_zero...........................proved - complete   [shostak](0.08 s)
    sub_cancel............................proved - complete   [shostak](0.01 s)
    sub_cancel_neg........................proved - complete   [shostak](0.02 s)
    neg_add_left..........................proved - complete   [shostak](0.01 s)
    neg_add_right.........................proved - complete   [shostak](0.01 s)
    neg_distr_sub.........................proved - complete   [shostak](0.02 s)
    neg_neg...............................proved - complete   [shostak](0.03 s)
    neg_distr_add.........................proved - complete   [shostak](0.05 s)
    dot_neg_left..........................proved - complete   [shostak](0.07 s)
    dot_neg_right.........................proved - complete   [shostak](0.07 s)
    neg_dot_neg...........................proved - complete   [shostak](0.07 s)
    dot_zero_left.........................proved - complete   [shostak](0.01 s)
    dot_zero_right........................proved - complete   [shostak](0.00 s)
    dot_comm..............................proved - complete   [shostak](0.10 s)
    dot_assoc.............................proved - complete   [shostak](0.07 s)
    dot_eq_args_ge........................proved - complete   [shostak](0.05 s)
    add_comm_assoc_left...................proved - complete   [shostak](0.06 s)
    add_comm_assoc_right..................proved - complete   [shostak](0.05 s)
    dot_add_right.........................proved - complete   [shostak](0.12 s)
    dot_add_left..........................proved - complete   [shostak](0.21 s)
    dot_sub_right.........................proved - complete   [shostak](0.12 s)
    dot_sub_left..........................proved - complete   [shostak](0.22 s)
    dot_divby.............................proved - complete   [shostak](0.16 s)
    dot_scal_left.........................proved - complete   [shostak](0.06 s)
    dot_scal_right........................proved - complete   [shostak](0.12 s)
    dot_scal_comm_assoc...................proved - complete   [shostak](0.06 s)
    scal_comm_assoc.......................proved - complete   [shostak](0.09 s)
    dot_scal_canon........................proved - complete   [shostak](0.05 s)
    scal_add_left.........................proved - complete   [shostak](0.09 s)
    scal_sub_left.........................proved - complete   [shostak](0.10 s)
    scal_add_right........................proved - complete   [shostak](0.09 s)
    scal_sub_right........................proved - complete   [shostak](0.10 s)
    scal_assoc............................proved - complete   [shostak](0.06 s)
    scal_neg..............................proved - complete   [shostak](0.01 s)
    scal_cross............................proved - complete   [shostak](0.17 s)
    scal_zero.............................proved - complete   [shostak](0.00 s)
    scal_0................................proved - complete   [shostak](0.01 s)
    scal_1................................proved - complete   [shostak](0.05 s)
    scal_neg_1............................proved - complete   [shostak](0.01 s)
    scal_cancel...........................proved - complete   [shostak](0.16 s)
    scal_div_mult_left....................proved - complete   [shostak](0.24 s)
    scal_div_mult_right...................proved - complete   [shostak](0.29 s)
    scal_eq_zero..........................proved - complete   [shostak](0.09 s)
    dot_ge_dist...........................proved - complete   [shostak](0.46 s)
    dot_gt_dist...........................proved - complete   [shostak](0.46 s)
    idem_right............................proved - complete   [shostak](0.13 s)
    sqv_neg...............................proved - complete   [shostak](0.07 s)
    sqv_add...............................proved - complete   [shostak](0.24 s)
    sqv_scal..............................proved - complete   [shostak](0.05 s)
    sqv_sub...............................proved - complete   [shostak](0.23 s)
    sqv_sub_scal..........................proved - complete   [shostak](0.42 s)
    sqv_sym...............................proved - complete   [shostak](0.21 s)
    sqrt_sqv_sq...........................proved - complete   [shostak](0.04 s)
    norm_sym..............................proved - complete   [shostak](0.02 s)
    norm_neg..............................proved - complete   [shostak](0.09 s)
    dot_sq_norm...........................proved - complete   [shostak](0.06 s)
    sq_norm...............................proved - complete   [shostak](0.17 s)
    sqrt_sqv_norm.........................proved - complete   [shostak](0.01 s)
    norms_eq_sqv..........................proved - complete   [shostak](0.02 s)
    norms_eq_sos..........................proved - complete   [shostak](0.01 s)
    norm_le_sqv...........................proved - complete   [shostak](0.01 s)
    norm_lt_sqv...........................proved - complete   [shostak](0.01 s)
    norm_scal.............................proved - complete   [shostak](0.08 s)
    caret_TCC1............................proved - complete   [shostak](0.06 s)
    norm_normalize........................proved - complete   [shostak](0.00 s)
    dot_normalize.........................proved - complete   [shostak](0.07 s)
    normalize_normalize...................proved - complete   [shostak](0.08 s)
    normalized_id.........................proved - complete   [shostak](0.08 s)
    normalize_scal........................proved - complete   [shostak](0.29 s)
    cauchy_schwarz........................proved - complete   [shostak](0.82 s)
    dot_norm..............................proved - complete   [shostak](0.13 s)
    schwartz..............................proved - complete   [shostak](0.04 s)
    schwartz_cor..........................proved - complete   [shostak](0.22 s)
    norm_triangle.........................proved - complete   [shostak](0.07 s)
    norm_add_le...........................proved - complete   [shostak](0.31 s)
    norm_sub_le...........................proved - complete   [shostak](0.34 s)
    norm_sub_ge...........................proved - complete   [shostak](0.03 s)
    norm_ge_comps.........................proved - complete   [shostak](0.43 s)
    sq_norm_dist..........................proved - complete   [shostak](0.74 s)
    parallel_refl.........................proved - complete   [shostak](0.01 s)
    parallel_symm.........................proved - complete   [shostak](0.04 s)
    parallel_trans........................proved - complete   [shostak](0.05 s)
    parallel_zero.........................proved - complete   [shostak](0.02 s)
    dir_parallel..........................proved - complete   [shostak](0.01 s)
    pythagorean...........................proved - complete   [shostak](0.05 s)
    norm_add_ge_left......................proved - complete   [shostak](0.09 s)
    norm_add_ge_right.....................proved - complete   [shostak](0.01 s)
    Theory totals: 156 formulas, 156 attempted, 156 succeeded (12.54 s)

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

 Proof summary for theory vectors_cos
    cosines_law...........................proved - complete   [shostak](0.84 s)
    angle_exists..........................proved - complete   [shostak](0.37 s)
    angle_between_TCC1....................proved - complete   [shostak](0.13 s)
    cosines_law_bnd.......................proved - complete   [shostak](0.51 s)
    cosines_law_ge........................proved - complete   [shostak](0.09 s)
    cosines_law_le........................proved - complete   [shostak](0.04 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.99 s)

 Proof summary for theory vectors_2D_cos
    cosines_law...........................proved - complete   [shostak](0.79 s)
    angle_exists..........................proved - complete   [shostak](0.35 s)
    angle_between_TCC1....................proved - complete   [shostak](0.11 s)
    cosines_law_bnd.......................proved - complete   [shostak](0.50 s)
    cosines_law_ge........................proved - complete   [shostak](0.08 s)
    cosines_law_le........................proved - complete   [shostak](0.03 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.87 s)

 Proof summary for theory vectors_3D_cos
    cosines_law...........................proved - complete   [shostak](0.80 s)
    angle_exists..........................proved - complete   [shostak](0.36 s)
    angle_between_TCC1....................proved - complete   [shostak](0.11 s)
    cosines_law_bnd.......................proved - complete   [shostak](0.49 s)
    cosines_law_ge........................proved - complete   [shostak](0.08 s)
    cosines_law_le........................proved - complete   [shostak](0.04 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.89 s)

 Proof summary for theory distance
    sq_dist_TCC1..........................proved - complete   [shostak](0.01 s)
    sq_dist_TCC2..........................proved - complete   [shostak](0.01 s)
    sq_dist_TCC3..........................proved - complete   [shostak](0.01 s)
    dist_eq_args..........................proved - complete   [shostak](0.06 s)
    dist_zero_l...........................proved - complete   [shostak](0.04 s)
    dist_zero_r...........................proved - complete   [shostak](0.04 s)
    dist_sym..............................proved - complete   [shostak](0.11 s)
    dist_eq_0.............................proved - complete   [shostak](0.12 s)
    dist_norm.............................proved - complete   [shostak](0.13 s)
    dist_rel..............................proved - complete   [shostak](0.09 s)
    sq_dist_is_dist_sq....................proved - complete   [shostak](0.21 s)
    sq_dist_norm..........................proved - complete   [shostak](0.02 s)
    sq_dist_sym...........................proved - complete   [shostak](0.02 s)
    sq_dist_le............................proved - complete   [shostak](0.02 s)
    sq_dist_lt............................proved - complete   [shostak](0.01 s)
    dist_gt_comp..........................proved - complete   [shostak](0.12 s)
    sq_dist_dist..........................proved - complete   [shostak](0.18 s)
    on_segment_beg........................proved - complete   [shostak](0.02 s)
    on_segment_end........................proved - complete   [shostak](0.05 s)
    on_line_beg...........................proved - complete   [shostak](0.01 s)
    on_line_end...........................proved - complete   [shostak](0.03 s)
    on_segment_on_line....................proved - complete   [shostak](0.01 s)
    Theory totals: 22 formulas, 22 attempted, 22 succeeded (1.33 s)

 Proof summary for theory distance_2D
    dist_eq_args..........................proved - complete   [shostak](0.03 s)
    dist_zero_l...........................proved - complete   [shostak](0.04 s)
    dist_zero_r...........................proved - complete   [shostak](0.04 s)
    dist_sym..............................proved - complete   [shostak](0.16 s)
    dist_eq_0.............................proved - complete   [shostak](0.08 s)
    dist_norm.............................proved - complete   [shostak](0.21 s)
    dist_rel..............................proved - complete   [shostak](0.20 s)
    sq_dist_is_dist_sq....................proved - complete   [shostak](0.32 s)
    sq_dist_norm..........................proved - complete   [shostak](0.01 s)
    sq_dist_sym...........................proved - complete   [shostak](0.01 s)
    sq_dist_le............................proved - complete   [shostak](0.02 s)
    sq_dist_lt............................proved - complete   [shostak](0.01 s)
    dist_ge_x.............................proved - complete   [shostak](0.06 s)
    dist_ge_y.............................proved - complete   [shostak](0.06 s)
    sq_dist_dist..........................proved - complete   [shostak](0.16 s)
    dist_triangle.........................proved - complete   [shostak](0.55 s)
    dist_tri_sub..........................proved - complete   [shostak](0.06 s)
    on_segment_beg........................proved - complete   [shostak](0.05 s)
    on_segment_end........................proved - complete   [shostak](0.06 s)
    on_line_beg...........................proved - complete   [shostak](0.04 s)
    on_line_end...........................proved - complete   [shostak](0.06 s)
    on_segment_on_line....................proved - complete   [shostak](0.00 s)
    Theory totals: 22 formulas, 22 attempted, 22 succeeded (2.27 s)

 Proof summary for theory distance_3D
    dist_eq_args..........................proved - complete   [shostak](0.03 s)
    dist_zero_l...........................proved - complete   [shostak](0.11 s)
    dist_zero_r...........................proved - complete   [shostak](0.05 s)
    dist_sym..............................proved - complete   [shostak](0.24 s)
    dist_eq_0.............................proved - complete   [shostak](0.12 s)
    dist_norm.............................proved - complete   [shostak](0.39 s)
    dist_rel..............................proved - complete   [shostak](0.29 s)
    sq_dist_is_dist_sq....................proved - complete   [shostak](0.52 s)
    sq_dist_norm..........................proved - complete   [shostak](0.01 s)
    sq_dist_sym...........................proved - complete   [shostak](0.02 s)
    sq_dist_le............................proved - complete   [shostak](0.01 s)
    sq_dist_lt............................proved - complete   [shostak](0.01 s)
    dist_ge_x.............................proved - complete   [shostak](0.10 s)
    dist_ge_y.............................proved - complete   [shostak](0.09 s)
    dist_ge_z.............................proved - complete   [shostak](0.09 s)
    sq_dist_dist..........................proved - complete   [shostak](0.16 s)
    dist_triangle.........................proved - complete   [shostak](0.86 s)
    dist_tri_sub..........................proved - complete   [shostak](0.07 s)
    on_segment_beg........................proved - complete   [shostak](0.06 s)
    on_segment_end........................proved - complete   [shostak](0.06 s)
    on_line_beg...........................proved - complete   [shostak](0.06 s)
    on_line_end...........................proved - complete   [shostak](0.06 s)
    on_segment_on_line....................proved - complete   [shostak](0.01 s)
    Theory totals: 23 formulas, 23 attempted, 23 succeeded (3.44 s)

 Proof summary for theory lines
    line_from_TCC1........................proved - complete   [shostak](0.02 s)
    vec_from_eq_args......................proved - complete   [shostak](0.00 s)
    vel_from_tm_TCC1......................proved - complete   [shostak](0.07 s)
    line_from_tm_TCC1.....................proved - complete   [shostak](0.04 s)
    vel_from_tm_nz........................proved - complete   [shostak](0.02 s)
    vel_from_tm_lem.......................proved - complete   [shostak](0.01 s)
    vel_from_tm_rew.......................proved - complete   [shostak](0.10 s)
    vel_from_tm_eq_args...................proved - complete   [shostak](0.03 s)
    vel_from_tm_length....................proved - complete   [shostak](0.29 s)
    vel_from_spd_TCC1.....................proved - complete   [shostak](0.02 s)
    vel_from_spd_lem_TCC1.................proved - complete   [shostak](0.06 s)
    vel_from_spd_lem......................proved - complete   [shostak](0.07 s)
    vel_from_spd_norm_TCC1................proved - complete   [shostak](0.01 s)
    vel_from_spd_norm.....................proved - complete   [shostak](0.09 s)
    gen_speed_TCC1........................proved - complete   [shostak](0.04 s)
    gen_line_spd_TCC1.....................proved - complete   [shostak](0.04 s)
    test1_TCC1............................proved - complete   [shostak](0.01 s)
    test1.................................proved - complete   [shostak](0.05 s)
    test2.................................proved - complete   [shostak](0.07 s)
    test3.................................proved - complete   [shostak](0.06 s)
    test4.................................proved - complete   [shostak](0.10 s)
    vel_from_spd_on_line..................proved - complete   [shostak](0.06 s)
    Theory totals: 22 formulas, 22 attempted, 22 succeeded (1.30 s)

 Proof summary for theory lines_2D
    line_from_TCC1........................proved - complete   [shostak](0.01 s)
    vec_from_eq_args......................proved - complete   [shostak](0.02 s)
    vel_from_tm_TCC1......................proved - complete   [shostak](0.05 s)
    line_from_tm_TCC1.....................proved - complete   [shostak](0.03 s)
    vel_from_tm_nz........................proved - complete   [shostak](0.01 s)
    vel_from_tm_lem.......................proved - complete   [shostak](0.01 s)
    vel_from_tm_rew.......................proved - complete   [shostak](0.15 s)
    vel_from_tm_eq_args...................proved - complete   [shostak](0.05 s)
    vel_from_tm_length....................proved - complete   [shostak](0.17 s)
    vel_from_spd_TCC1.....................proved - complete   [shostak](0.00 s)
    vel_from_spd_lem_TCC1.................proved - complete   [shostak](0.05 s)
    vel_from_spd_lem......................proved - complete   [shostak](0.06 s)
    vel_from_spd_norm_TCC1................proved - complete   [shostak](0.01 s)
    vel_from_spd_norm.....................proved - complete   [shostak](0.08 s)
    gen_speed_TCC1........................proved - complete   [shostak](0.06 s)
    on_line_lem...........................proved - complete   [shostak](0.05 s)
    on_line_neg...........................proved - complete   [shostak](0.07 s)
    on_line_sym_TCC1......................proved - complete   [shostak](0.06 s)
    on_line_sym...........................proved - complete   [shostak](0.13 s)
    gen_line_spd_TCC1.....................proved - complete   [shostak](0.04 s)
    test1_TCC1............................proved - complete   [shostak](0.01 s)
    test1.................................proved - complete   [shostak](0.04 s)
    test2.................................proved - complete   [shostak](0.07 s)
    test3.................................proved - complete   [shostak](0.04 s)
    test4.................................proved - complete   [shostak](0.10 s)
    vel_from_spd_on_line..................proved - complete   [shostak](0.05 s)
    Theory totals: 26 formulas, 26 attempted, 26 succeeded (1.45 s)

 Proof summary for theory lines_3D
    line_from_TCC1........................proved - complete   [shostak](0.01 s)
    vec_from_eq_args......................proved - complete   [shostak](0.02 s)
    vel_from_tm_TCC1......................proved - complete   [shostak](0.07 s)
    line_from_tm_TCC1.....................proved - complete   [shostak](0.03 s)
    vel_from_tm_nz........................proved - complete   [shostak](0.02 s)
    vel_from_tm_lem.......................proved - complete   [shostak](0.01 s)
    vel_from_tm_rew.......................proved - complete   [shostak](0.18 s)
    vel_from_tm_eq_args...................proved - complete   [shostak](0.03 s)
    vel_from_tm_length....................proved - complete   [shostak](0.17 s)
    vel_from_spd_TCC1.....................proved - complete   [shostak](0.01 s)
    vel_from_spd_lem_TCC1.................proved - complete   [shostak](0.05 s)
    vel_from_spd_lem......................proved - complete   [shostak](0.06 s)
    vel_from_spd_norm_TCC1................proved - complete   [shostak](0.01 s)
    vel_from_spd_norm.....................proved - complete   [shostak](0.08 s)
    gen_speed_TCC1........................proved - complete   [shostak](0.03 s)
    on_line_lem...........................proved - complete   [shostak](0.06 s)
    on_line_neg...........................proved - complete   [shostak](0.10 s)
    on_line_sym_TCC1......................proved - complete   [shostak](0.09 s)
    on_line_sym...........................proved - complete   [shostak](0.21 s)
    gen_line_spd_TCC1.....................proved - complete   [shostak](0.03 s)
    test1_TCC1............................proved - complete   [shostak](0.02 s)
    test1.................................proved - complete   [shostak](0.04 s)
    test2.................................proved - complete   [shostak](0.08 s)
    test3.................................proved - complete   [shostak](0.05 s)
    test4.................................proved - complete   [shostak](0.13 s)
    vel_from_spd_on_line..................proved - complete   [shostak](0.05 s)
    Theory totals: 26 formulas, 26 attempted, 26 succeeded (1.67 s)

 Proof summary for theory law_cos_pos_2D
    law_cosines...........................proved - complete   [shostak](0.96 s)
    law_cosines_alt.......................proved - complete   [shostak](0.85 s)
    angle_exists..........................proved - complete   [shostak](0.41 s)
    angle_between_TCC1....................proved - complete   [shostak](0.11 s)
    law_cosines_bnd.......................proved - complete   [shostak](0.57 s)
    law_cosines_bnd_abs...................proved - complete   [shostak](0.28 s)
    law_cosines_le........................proved - complete   [shostak](0.19 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (3.37 s)

 Proof summary for theory law_cos_pos_3D
    law_cosines...........................proved - complete   [shostak](1.56 s)
    law_cosines_alt.......................proved - complete   [shostak](1.43 s)
    angle_exists..........................proved - complete   [shostak](0.42 s)
    angle_between_TCC1....................proved - complete   [shostak](0.11 s)
    law_cosines_bnd.......................proved - complete   [shostak](0.58 s)
    law_cosines_bnd_abs...................proved - complete   [shostak](0.27 s)
    law_cosines_le........................proved - complete   [shostak](0.19 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (4.55 s)

 Proof summary for theory closest_approach
    sq_dist_lem...........................proved - complete   [shostak](0.63 s)
    sq_dist_quad..........................proved - complete   [shostak](1.19 s)
    dist_eq_vel...........................proved - complete   [shostak](0.10 s)
    norm_diff_eq_0........................proved - complete   [shostak](0.03 s)
    time_closest_TCC1.....................proved - complete   [shostak](0.02 s)
    time_closest_lem_TCC1.................proved - complete   [shostak](0.06 s)
    time_closest_lem......................proved - complete   [shostak](0.07 s)
    cpa_prep_mono.........................proved - complete   [shostak](0.25 s)
    time_cpa..............................proved - complete   [shostak](0.37 s)
    dist_cpa..............................proved - complete   [shostak](0.08 s)
    dist_cpa_lt...........................proved - complete   [shostak](0.06 s)
    dist_min..............................proved - complete   [shostak](0.03 s)
    dist_diverges.........................proved - complete   [shostak](0.07 s)
    dist_parallel_lines...................proved - complete   [shostak](0.26 s)
    dot_nneg_tca_npos.....................proved - complete   [shostak](0.08 s)
    divergent_u_neq_v.....................proved - complete   [shostak](0.10 s)
    dot_nneg_divergent....................proved - complete   [shostak](0.06 s)
    divergent_dot_nneg....................proved - complete   [shostak](3.90 s)
    divergent_t1_lt_t2....................proved - complete   [shostak](0.07 s)
    dot_prop_divergent....................proved - complete   [shostak](0.02 s)
    Theory totals: 20 formulas, 20 attempted, 20 succeeded (7.47 s)

 Proof summary for theory closest_approach_2D
    sq_dist_lem...........................proved - complete   [shostak](0.74 s)
    sq_dist_quad..........................proved - complete   [shostak](0.70 s)
    dist_eq_vel...........................proved - complete   [shostak](0.14 s)
    norm_diff_eq_0........................proved - complete   [shostak](0.03 s)
    time_closest_TCC1.....................proved - complete   [shostak](0.01 s)
    time_closest_lem_TCC1.................proved - complete   [shostak](0.05 s)
    time_closest_lem......................proved - complete   [shostak](0.06 s)
    cpa_prep_mono.........................proved - complete   [shostak](0.21 s)
    time_cpa..............................proved - complete   [shostak](0.27 s)
    dist_cpa..............................proved - complete   [shostak](0.06 s)
    dist_cpa_lt...........................proved - complete   [shostak](0.04 s)
    dist_min..............................proved - complete   [shostak](0.02 s)
    dist_diverges.........................proved - complete   [shostak](0.06 s)
    dist_parallel_lines...................proved - complete   [shostak](0.24 s)
    dot_nneg_tca_npos.....................proved - complete   [shostak](0.07 s)
    divergent_u_neq_v.....................proved - complete   [shostak](0.22 s)
    dot_nneg_divergent....................proved - complete   [shostak](0.05 s)
    divergent_dot_nneg....................proved - complete   [shostak](2.75 s)
    divergent_t1_lt_t2....................proved - complete   [shostak](0.07 s)
    dot_prop_divergent....................proved - complete   [shostak](0.02 s)
    pos_dot_divergent.....................proved - complete   [shostak](0.14 s)
    t1_lt_t2_lt_D.........................proved - complete   [shostak](2.78 s)
    lt_D_t1_lt_t2.........................proved - complete   [shostak](2.77 s)
    discr_le_0............................proved - complete   [shostak](0.35 s)
    gt_D_t1_lt_t2.........................proved - complete   [shostak](0.87 s)
    cpa_sqvs_lt...........................proved - complete   [shostak](0.60 s)
    Theory totals: 26 formulas, 26 attempted, 26 succeeded (13.32 s)

 Proof summary for theory closest_approach_relative_2D
    divergent_lem.........................proved - complete   [shostak](0.38 s)
    dot_pos_comm..........................proved - complete   [shostak](0.06 s)
    dot_pos_divergent.....................proved - complete   [shostak](0.08 s)
    divergent_lt..........................proved - complete   [shostak](0.07 s)
    divergent_dot_pos.....................proved - complete   [shostak](0.01 s)
    diverg_dot_nneg.......................proved - complete   [shostak](0.01 s)
    divergent_v_neq_0.....................proved - complete   [shostak](0.01 s)
    dot_nneg_divergent_nzv................proved - complete   [shostak](0.02 s)
    tau_TCC1..............................proved - complete   [shostak](0.00 s)
    tau_is_min............................proved - complete   [shostak](0.26 s)
    dist_tau_min..........................proved - complete   [shostak](0.05 s)
    tau_sqv_min...........................proved - complete   [shostak](0.05 s)
    Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.00 s)

 Proof summary for theory closest_approach_3D
    sq_dist_lem...........................proved - complete   [shostak](1.21 s)
    sq_dist_quad..........................proved - complete   [shostak](1.07 s)
    dist_eq_vel...........................proved - complete   [shostak](0.22 s)
    norm_diff_eq_0........................proved - complete   [shostak](0.03 s)
    time_closest_TCC1.....................proved - complete   [shostak](0.01 s)
    time_closest_lem_TCC1.................proved - complete   [shostak](0.05 s)
    time_closest_lem......................proved - complete   [shostak](0.06 s)
    cpa_prep_mono.........................proved - complete   [shostak](0.21 s)
    time_cpa..............................proved - complete   [shostak](0.27 s)
    dist_cpa..............................proved - complete   [shostak](0.06 s)
    dist_cpa_lt...........................proved - complete   [shostak](0.05 s)
    dist_min..............................proved - complete   [shostak](0.03 s)
    dist_diverges.........................proved - complete   [shostak](0.06 s)
    dist_parallel_lines...................proved - complete   [shostak](0.24 s)
    dot_nneg_tca_npos.....................proved - complete   [shostak](0.07 s)
    divergent_u_neq_v.....................proved - complete   [shostak](0.33 s)
    dot_nneg_divergent....................proved - complete   [shostak](0.05 s)
    divergent_dot_nneg....................proved - complete   [shostak](8.23 s)
    divergent_t1_lt_t2....................proved - complete   [shostak](0.07 s)
    dot_prop_divergent....................proved - complete   [shostak](0.02 s)
    t1_lt_t2_lt_D.........................proved - complete   [shostak](1.24 s)
    lt_D_t1_lt_t2.........................proved - complete   [shostak](1.38 s)
    discr_le_0............................proved - complete   [shostak](0.51 s)
    Theory totals: 23 formulas, 23 attempted, 23 succeeded (15.47 s)

 Proof summary for theory perpendicular_2D
    neg_perpL.............................proved - complete   [shostak](0.01 s)
    neg_perpR.............................proved - complete   [shostak](0.01 s)
    perpL_perpR...........................proved - complete   [shostak](0.01 s)
    dot_perpR_eq_0........................proved - complete   [shostak](0.02 s)
    dot_perpL_eq_0........................proved - complete   [shostak](0.02 s)
    dot_perpR_scal_eq_0...................proved - complete   [shostak](0.04 s)
    dot_perpL_scal_eq_0...................proved - complete   [shostak](0.03 s)
    sqv_perpR.............................proved - complete   [shostak](0.04 s)
    sqv_perpL.............................proved - complete   [shostak](0.03 s)
    perpR_add.............................proved - complete   [shostak](0.02 s)
    perpR_sub.............................proved - complete   [shostak](0.02 s)
    perpR_scal............................proved - complete   [shostak](0.02 s)
    perpR_neg.............................proved - complete   [shostak](0.00 s)
    perpR_eq_zero.........................proved - complete   [shostak](0.02 s)
    perpL_add.............................proved - complete   [shostak](0.02 s)
    perpL_sub.............................proved - complete   [shostak](0.01 s)
    perpL_scal............................proved - complete   [shostak](0.02 s)
    perpL_neg.............................proved - complete   [shostak](0.00 s)
    perpL_eq_zero.........................proved - complete   [shostak](0.02 s)
    perpL_plus_perpR......................proved - complete   [shostak](0.01 s)
    perpR_perpR...........................proved - complete   [shostak](0.01 s)
    perpR_perpL...........................proved - complete   [shostak](0.02 s)
    perpL_nz..............................proved - complete   [shostak](0.02 s)
    perpR_nz..............................proved - complete   [shostak](0.02 s)
    perp_pt_TCC1..........................proved - complete   [shostak](0.01 s)
    perp_is_normal........................proved - complete   [shostak](0.22 s)
    perp_is_min...........................proved - complete   [shostak](1.17 s)
    perp_gt_del...........................proved - complete   [shostak](0.51 s)
    perp_comps............................proved - complete   [shostak](0.54 s)
    perp_pt_TCC2..........................proved - complete   [shostak](0.01 s)
    dist_is_min...........................proved - complete   [shostak](0.05 s)
    perp_pt_perp_TCC1.....................proved - complete   [shostak](0.13 s)
    perp_pt_perp..........................proved - complete   [shostak](0.55 s)
    Theory totals: 33 formulas, 33 attempted, 33 succeeded (3.63 s)

 Proof summary for theory perpendicular_3D
    perp_pt_TCC1..........................proved - complete   [shostak](0.01 s)
    perp_is_normal........................proved - complete   [shostak](0.25 s)
    perp_is_min...........................proved - complete   [shostak](2.62 s)
    perp_gt_del...........................proved - complete   [shostak](0.62 s)
    perp_comps............................proved - complete   [shostak](0.69 s)
    perp_pt_TCC2..........................proved - complete   [shostak](0.01 s)
    dist_is_min...........................proved - complete   [shostak](0.05 s)
    perp_pt_perp_TCC1.....................proved - complete   [shostak](0.25 s)
    perp_pt_perp..........................proved - complete   [shostak](0.55 s)
    Theory totals: 9 formulas, 9 attempted, 9 succeeded (5.06 s)

 Proof summary for theory intersections_2D
    det_line..............................proved - complete   [shostak](0.53 s)
    intersect_pt_TCC1.....................proved - complete   [shostak](0.09 s)
    same_line_sym.........................proved - complete   [shostak](0.67 s)
    intersect_not_parallel................proved - complete   [shostak](0.12 s)
    intersection_lem......................proved - complete   [shostak](1.79 s)
    lines_intersection_TCC1...............proved - complete   [shostak](0.10 s)
    lines_intersection_sound..............proved - complete   [shostak](0.05 s)
    pt_intersect..........................proved - complete   [shostak](0.37 s)
    intersect_pt_unique_TCC1..............proved - complete   [shostak](0.00 s)
    intersect_pt_unique...................proved - complete   [shostak](0.42 s)
    same_line_lem.........................proved - complete   [shostak](0.84 s)
    not_same_line.........................proved - complete   [shostak](0.33 s)
    intersect_pt_lem_TCC1.................proved - complete   [shostak](0.05 s)
    intersect_pt_lem......................proved - complete   [shostak](0.02 s)
    Theory totals: 14 formulas, 14 attempted, 14 succeeded (5.39 s)

 Proof summary for theory det_2D
    det_zero_left.........................proved - complete   [shostak](0.00 s)
    det_zero_right........................proved - complete   [shostak](0.01 s)
    det_eq_0..............................proved - complete   [shostak](0.03 s)
    det_scal_left.........................proved - complete   [shostak](0.05 s)
    det_scal_right........................proved - complete   [shostak](0.08 s)
    det_add_left..........................proved - complete   [shostak](0.06 s)
    det_add_right.........................proved - complete   [shostak](0.11 s)
    det_sub_left..........................proved - complete   [shostak](0.06 s)
    det_sub_right.........................proved - complete   [shostak](0.11 s)
    det_symm..............................proved - complete   [shostak](0.04 s)
    det_asym..............................proved - complete   [shostak](0.06 s)
    det_symm_0............................proved - complete   [shostak](0.01 s)
    sq_det................................proved - complete   [shostak](0.11 s)
    det_norm..............................proved - complete   [shostak](0.12 s)
    det_perpR.............................proved - complete   [shostak](0.03 s)
    det_perpL.............................proved - complete   [shostak](0.04 s)
    dot_perpR.............................proved - complete   [shostak](0.03 s)
    dot_perpL.............................proved - complete   [shostak](0.04 s)
    perpR_dot.............................proved - complete   [shostak](0.04 s)
    perpL_dot.............................proved - complete   [shostak](0.03 s)
    det_dot_0.............................proved - complete   [shostak](0.05 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (1.12 s)

 Proof summary for theory parallel_2D
    abs_det_par...........................proved - complete   [shostak](0.69 s)
    parallel_dot_1........................proved - complete   [shostak](0.49 s)
    parallel_det_0........................proved - complete   [shostak](0.02 s)
    dot_perpL_parallel....................proved - complete   [shostak](0.20 s)
    dot_perpR_parallel....................proved - complete   [shostak](0.20 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.59 s)

 Proof summary for theory basis_2D
    orthogonal_basis_TCC1.................proved - complete   [shostak](0.01 s)
    orthogonal_basis_TCC2.................proved - complete   [shostak](0.01 s)
    orthogonal_basis......................proved - complete   [shostak](1.75 s)
    orthonormal_basis.....................proved - complete   [shostak](0.05 s)
    basis_two_dot_zero....................proved - complete   [shostak](0.12 s)
    basis_add.............................proved - complete   [shostak](0.55 s)
    basis_sub.............................proved - complete   [shostak](0.57 s)
    basis_sqv.............................proved - complete   [shostak](0.23 s)
    basis_dot.............................proved - complete   [shostak](0.27 s)
    basis_perpR...........................proved - complete   [shostak](0.08 s)
    vh_vp_orthon..........................proved - complete   [shostak](0.28 s)
    orthogonal_basis_sqv..................proved - complete   [shostak](0.39 s)
    orthonormal_basis_sqv.................proved - complete   [shostak](0.10 s)
    orthogonal_basis_norm.................proved - complete   [shostak](0.08 s)
    orthonormal_basis_norm................proved - complete   [shostak](0.05 s)
    orthogonal_basis_norm_ge..............proved - complete   [shostak](0.17 s)
    orthonormal_basis_norm_ge.............proved - complete   [shostak](0.06 s)
    orthogonal_basis_dot..................proved - complete   [shostak](0.34 s)
    orthonormal_basis_dot.................proved - complete   [shostak](0.12 s)
    Theory totals: 19 formulas, 19 attempted, 19 succeeded (5.24 s)

 Proof summary for theory matrices
    det_id...............................proved - complete   [shostak]( 0.17 s)
    det_T................................proved - complete   [shostak]( 0.19 s)
    id_left1.............................proved - complete   [shostak]( 0.75 s)
    id_right1............................proved - complete   [shostak]( 0.66 s)
    id_left2.............................proved - complete   [shostak]( 0.33 s)
    id_right2............................proved - complete   [shostak]( 0.28 s)
    associativity_1......................proved - complete   [shostak]( 6.93 s)
    associativity_2......................proved - complete   [shostak]( 1.57 s)
    associativity_3......................proved - complete   [shostak]( 1.32 s)
    distribution_minus...................proved - complete   [shostak]( 1.43 s)
    distribution_add.....................proved - complete   [shostak]( 1.45 s)
    mat2_TCC1............................proved - complete   [shostak]( 0.06 s)
    det_mat2.............................proved - complete   [shostak]( 0.10 s)
    inv_TCC1.............................proved - complete   [shostak]( 0.33 s)
    inv_id_TCC1..........................proved - complete   [shostak]( 0.16 s)
    inv_id...............................proved - complete   [shostak]( 1.14 s)
    inv_left.............................proved - complete   [shostak](16.00 s)
    inv_right............................proved - complete   [shostak](16.94 s)
    sol_eqs_correctness..................proved - complete   [shostak]( 0.06 s)
    Theory totals: 19 formulas, 19 attempted, 19 succeeded (49.87 s)

 Proof summary for theory vect_trig_2D
    sin_range.............................proved - complete   [shostak](0.09 s)
    cos_range.............................proved - complete   [shostak](0.11 s)
    sin2_cos2.............................proved - complete   [shostak](0.13 s)
    sin_asym..............................proved - complete   [shostak](0.04 s)
    cos_symm..............................proved - complete   [shostak](0.03 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.40 s)

 Proof summary for theory vect_trig_3D
    cos_range.............................proved - complete   [shostak](0.09 s)
    cos_symm..............................proved - complete   [shostak](0.03 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.12 s)

 Proof summary for theory cross_3D
    cross_zero_left.......................proved - complete   [shostak](0.01 s)
    cross_zero_right......................proved - complete   [shostak](0.01 s)
    cross_anticomm........................proved - complete   [shostak](0.08 s)
    cross_scal_left.......................proved - complete   [shostak](0.10 s)
    cross_scal_right......................proved - complete   [shostak](0.14 s)
    cross_dist............................proved - complete   [shostak](0.23 s)
    Lagrange_Identity.....................proved - complete   [shostak](0.34 s)
    cross_cross...........................proved - complete   [shostak](0.24 s)
    lin_indep_cross.......................proved - complete   [shostak](1.33 s)
    mixed_prod_perm.......................proved - complete   [shostak](0.20 s)
    mixed_prod_perm2......................proved - complete   [shostak](0.20 s)
    mixed_prod_perm_neg...................proved - complete   [shostak](0.20 s)
    mixed_prod_scal1......................proved - complete   [shostak](0.23 s)
    mixed_prod_scal2......................proved - complete   [shostak](0.27 s)
    mixed_prod_scal3......................proved - complete   [shostak](0.29 s)
    mixed_prod_dist.......................proved - complete   [shostak](0.28 s)
    cross_cross_mixed.....................proved - complete   [shostak](0.62 s)
    Theory totals: 17 formulas, 17 attempted, 17 succeeded (4.80 s)

 Proof summary for theory linear_independence_3D
    get_around_bug........................proved - complete   [shostak](0.02 s)
    test2.................................proved - complete   [shostak](0.70 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.73 s)

 Proof summary for theory fseqs_ops_vect3
    plus_TCC1.............................proved - complete   [shostak](0.04 s)
    times_TCC1............................proved - complete   [shostak](0.04 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.08 s)

 Proof summary for theory sigma_fseq_3D
    sigma_TCC1............................proved - complete   [shostak](0.01 s)
    sigma_TCC2............................proved - complete   [shostak](0.03 s)
    sigma_TCC3............................proved - complete   [shostak](0.03 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.07 s)

 Proof summary for theory sigma_3D
    T_pred_lem............................proved - complete   [shostak](0.03 s)
    high_low_rewrite_TCC1.................proved - complete   [shostak](0.19 s)
    high_low_rewrite......................proved - complete   [shostak](0.01 s)
    sigma_TCC1............................proved - complete   [shostak](0.03 s)
    sigma_TCC2............................proved - complete   [shostak](0.02 s)
    sigma_TCC3............................proved - complete   [shostak](0.04 s)
    sigma_rew_TCC1........................proved - complete   [shostak](0.02 s)
    sigma_rew.............................proved - complete   [shostak](0.02 s)
    sigma_spl_TCC1........................proved - complete   [shostak](0.01 s)
    sigma_spl_TCC2........................proved - complete   [shostak](0.04 s)
    sigma_spl_TCC3........................proved - complete   [shostak](0.06 s)
    sigma_spl.............................proved - complete   [shostak](0.54 s)
    sigma_split_TCC1......................proved - complete   [shostak](0.02 s)
    sigma_split_TCC2......................proved - complete   [shostak](0.05 s)
    sigma_split...........................proved - complete   [shostak](0.25 s)
    sigma_diff............................proved - complete   [shostak](0.04 s)
    sigma_diff_neg........................proved - complete   [shostak](0.05 s)
    sigma_eq_arg..........................proved - complete   [shostak](0.01 s)
    sigma_first_TCC1......................proved - complete   [shostak](0.18 s)
    sigma_first_TCC2......................proved - complete   [shostak](0.05 s)
    sigma_first...........................proved - complete   [shostak](0.03 s)
    sigma_last_TCC1.......................proved - complete   [shostak](0.02 s)
    sigma_last_TCC2.......................proved - complete   [shostak](0.19 s)
    sigma_last............................proved - complete   [shostak](0.03 s)
    sigma_middle_TCC1.....................proved - complete   [shostak](0.03 s)
    sigma_middle_TCC2.....................proved - complete   [shostak](0.03 s)
    sigma_middle..........................proved - complete   [shostak](0.12 s)
    sigma_const...........................proved - complete   [shostak](0.56 s)
    sigma_zero............................proved - complete   [shostak](0.04 s)
    sigma_scal............................proved - complete   [shostak](0.76 s)
    sigma_shift_T_TCC1....................proved - complete   [shostak](0.05 s)
    sigma_shift_T_TCC2....................proved - complete   [shostak](0.07 s)
    sigma_shift_T_TCC3....................proved - complete   [shostak](0.04 s)
    sigma_shift_T.........................proved - complete   [shostak](0.85 s)
    sigma_shift_T2_TCC1...................proved - complete   [shostak](0.01 s)
    sigma_shift_T2_TCC2...................proved - complete   [shostak](0.00 s)
    sigma_shift_T2........................proved - complete   [shostak](0.61 s)
    sigma_sum.............................proved - complete   [shostak](0.60 s)
    sigma_minus...........................proved - complete   [shostak](0.33 s)
    sigma_restrict........................proved - complete   [shostak](0.30 s)
    sigma_restrict_to.....................proved - complete   [shostak](0.40 s)
    sigma_restrict_eq.....................proved - complete   [shostak](0.80 s)
    sigma_eq_TCC1.........................proved - complete   [shostak](0.04 s)
    sigma_eq..............................proved - complete   [shostak](0.03 s)
    sigma_with............................proved - complete   [shostak](0.27 s)
    sum_it_def_TCC1.......................proved - complete   [shostak](0.23 s)
    sum_it_def_TCC2.......................proved - complete   [shostak](0.20 s)
    sum_it_def_TCC3.......................proved - complete   [shostak](0.06 s)
    sum_it_prop_TCC1......................proved - complete   [shostak](0.06 s)
    sum_it_prop...........................proved - complete   [shostak](0.50 s)
    sum_it_sigma..........................proved - complete   [shostak](0.04 s)
    Theory totals: 51 formulas, 51 attempted, 51 succeeded (9.03 s)

 Proof summary for theory sigma_2D
    T_pred_lem............................proved - complete   [shostak](0.04 s)
    high_low_rewrite_TCC1.................proved - complete   [shostak](0.19 s)
    high_low_rewrite......................proved - complete   [shostak](0.01 s)
    sigma_TCC1............................proved - complete   [shostak](0.03 s)
    sigma_TCC2............................proved - complete   [shostak](0.02 s)
    sigma_TCC3............................proved - complete   [shostak](0.04 s)
    sigma_rew_TCC1........................proved - complete   [shostak](0.02 s)
    sigma_rew.............................proved - complete   [shostak](0.02 s)
    sigma_spl_TCC1........................proved - complete   [shostak](0.01 s)
    sigma_spl_TCC2........................proved - complete   [shostak](0.04 s)
    sigma_spl_TCC3........................proved - complete   [shostak](0.06 s)
    sigma_spl.............................proved - complete   [shostak](0.46 s)
    sigma_split_TCC1......................proved - complete   [shostak](0.03 s)
    sigma_split_TCC2......................proved - complete   [shostak](0.05 s)
    sigma_split...........................proved - complete   [shostak](0.25 s)
    sigma_diff............................proved - complete   [shostak](0.03 s)
    sigma_diff_neg........................proved - complete   [shostak](0.05 s)
    sigma_eq_arg..........................proved - complete   [shostak](0.01 s)
    sigma_first_TCC1......................proved - complete   [shostak](0.18 s)
    sigma_first_TCC2......................proved - complete   [shostak](0.05 s)
    sigma_first...........................proved - complete   [shostak](0.03 s)
    sigma_last_TCC1.......................proved - complete   [shostak](0.03 s)
    sigma_last_TCC2.......................proved - complete   [shostak](0.19 s)
    sigma_last............................proved - complete   [shostak](0.02 s)
    sigma_middle_TCC1.....................proved - complete   [shostak](0.04 s)
    sigma_middle_TCC2.....................proved - complete   [shostak](0.03 s)
    sigma_middle..........................proved - complete   [shostak](0.09 s)
    sigma_const...........................proved - complete   [shostak](0.56 s)
    sigma_zero............................proved - complete   [shostak](0.03 s)
    sigma_scal............................proved - complete   [shostak](0.65 s)
    sigma_shift_T_TCC1....................proved - complete   [shostak](0.05 s)
    sigma_shift_T_TCC2....................proved - complete   [shostak](0.06 s)
    sigma_shift_T_TCC3....................proved - complete   [shostak](0.04 s)
    sigma_shift_T.........................proved - complete   [shostak](0.85 s)
    sigma_shift_T2_TCC1...................proved - complete   [shostak](0.00 s)
    sigma_shift_T2_TCC2...................proved - complete   [shostak](0.01 s)
    sigma_shift_T2........................proved - complete   [shostak](0.61 s)
    sigma_sum.............................proved - complete   [shostak](0.51 s)
    sigma_minus...........................proved - complete   [shostak](0.32 s)
    sigma_restrict........................proved - complete   [shostak](0.31 s)
    sigma_restrict_to.....................proved - complete   [shostak](0.39 s)
    sigma_restrict_eq.....................proved - complete   [shostak](0.80 s)
    sigma_eq_TCC1.........................proved - complete   [shostak](0.04 s)
    sigma_eq..............................proved - complete   [shostak](0.03 s)
    sigma_with............................proved - complete   [shostak](0.22 s)
    sum_it_def_TCC1.......................proved - complete   [shostak](0.23 s)
    sum_it_def_TCC2.......................proved - complete   [shostak](0.19 s)
    sum_it_def_TCC3.......................proved - complete   [shostak](0.06 s)
    sum_it_prop_TCC1......................proved - complete   [shostak](0.06 s)
    sum_it_prop...........................proved - complete   [shostak](0.49 s)
    sum_it_sigma..........................proved - complete   [shostak](0.04 s)
    Theory totals: 51 formulas, 51 attempted, 51 succeeded (8.62 s)

 Proof summary for theory vect_3D_2D
    vect2_add.............................proved - complete   [shostak](0.02 s)
    vect2_sub.............................proved - complete   [shostak](0.01 s)
    vect2_scal............................proved - complete   [shostak](0.01 s)
    vect2_neg.............................proved - complete   [shostak](0.01 s)
    vect2_zero............................proved - complete   [shostak](0.01 s)
    vect2_eq..............................proved - complete   [shostak](0.01 s)
    vect2_eq_ext..........................proved - complete   [shostak](0.02 s)
    vect2_ext_id..........................proved - complete   [shostak](0.02 s)
    Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.11 s)

 Proof summary for theory vect_4D_3D_2D
    vect2_add.............................proved - complete   [shostak](0.01 s)
    vect2_sub.............................proved - complete   [shostak](0.02 s)
    vect2_scal............................proved - complete   [shostak](0.01 s)
    vect2_neg.............................proved - complete   [shostak](0.02 s)
    vect2_zero............................proved - complete   [shostak](0.01 s)
    vect2_eq..............................proved - complete   [shostak](0.01 s)
    vect2_eq_ext..........................proved - complete   [shostak](0.03 s)
    vect2_ext_id..........................proved - complete   [shostak](0.02 s)
    vect3_add.............................proved - complete   [shostak](0.02 s)
    vect3_sub.............................proved - complete   [shostak](0.02 s)
    vect3_scal............................proved - complete   [shostak](0.01 s)
    vect3_neg.............................proved - complete   [shostak](0.02 s)
    vect3_zero............................proved - complete   [shostak](0.01 s)
    vect3_eq..............................proved - complete   [shostak](0.01 s)
    vect3_eq_ext..........................proved - complete   [shostak](0.03 s)
    vect3_ext_id..........................proved - complete   [shostak](0.03 s)
    Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.28 s)

 Proof summary for theory parallel_3D
    abs_cross_par.........................proved - complete   [shostak](1.16 s)
    parallel_dot_1........................proved - complete   [shostak](0.76 s)
    parallel_cross_zero...................proved - complete   [shostak](0.02 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.93 s)

 Proof summary for theory angles_2D
    v_from_k_1............................proved - complete   [shostak](0.01 s)
    norm_v_from...........................proved - complete   [shostak](0.19 s)
    angle_exists_x........................proved - complete   [shostak](0.82 s)
    norm_vec_from.........................proved - complete   [shostak](0.01 s)
    vec_from_inj..........................proved - complete   [shostak](0.07 s)
    angle_exists..........................proved - complete   [shostak](1.04 s)
    angle_TCC1............................proved - complete   [shostak](0.04 s)
    vec_from_angle........................proved - complete   [shostak](0.05 s)
    angle_vec_from_TCC1...................proved - complete   [shostak](0.05 s)
    angle_vec_from........................proved - complete   [shostak](0.06 s)
    Angle_TCC1............................proved - complete   [shostak](0.02 s)
    angle_Angle...........................proved - complete   [shostak](0.44 s)
    vec_from_Angle........................proved - complete   [shostak](0.02 s)
    angle_x0_TCC1.........................proved - complete   [shostak](0.01 s)
    angle_x0..............................proved - complete   [shostak](0.01 s)
    angle_0x_TCC1.........................proved - complete   [shostak](0.01 s)
    angle_0x..............................proved - complete   [shostak](0.01 s)
    angle_xx_TCC1.........................proved - complete   [shostak](0.01 s)
    angle_xx..............................proved - complete   [shostak](0.09 s)
    angle_n0_TCC1.........................proved - complete   [shostak](0.01 s)
    angle_n0..............................proved - complete   [shostak](0.02 s)
    angle_0n_TCC1.........................proved - complete   [shostak](0.01 s)
    angle_0n..............................proved - complete   [shostak](0.05 s)
    angle_nx_TCC1.........................proved - complete   [shostak](0.02 s)
    angle_nx..............................proved - complete   [shostak](0.27 s)
    angle_xn_TCC1.........................proved - complete   [shostak](0.02 s)
    angle_xn..............................proved - complete   [shostak](0.21 s)
    angle_nn_TCC1.........................proved - complete   [shostak](0.02 s)
    angle_nn..............................proved - complete   [shostak](0.21 s)
    vfrom_sub.............................proved - complete   [shostak](0.01 s)
    v_from_dot............................proved - complete   [shostak](0.02 s)
    v_from_dot_k..........................proved - complete   [shostak](0.16 s)
    dot_prod_angles.......................proved - complete   [shostak](0.10 s)
    Theory totals: 33 formulas, 33 attempted, 33 succeeded (4.11 s)

 Proof summary for theory angles_2D_scaf
    trig_prop2............................proved - complete   [shostak](0.41 s)
    trig_prop.............................proved - complete   [shostak](1.48 s)
    sin_cos_angle.........................proved - complete   [shostak](0.40 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (2.29 s)

 Proof summary for theory trackAngles_2D
    v_from_TCC1...........................proved - complete   [shostak](0.14 s)
    trk_TCC1..............................proved - complete   [shostak](0.02 s)
    track_TCC1............................proved - complete   [shostak](0.06 s)
    norm_v_from...........................proved - complete   [shostak](0.19 s)
    vec_from_nz...........................proved - complete   [shostak](0.03 s)
    norm_vec_from.........................proved - complete   [shostak](0.01 s)
    vec_from_inj..........................proved - complete   [shostak](0.07 s)
    vec_from_track........................proved - complete   [shostak](0.05 s)
    track_vec_from_TCC1...................proved - complete   [shostak](0.06 s)
    track_vec_from........................proved - complete   [shostak](0.13 s)
    track_trk.............................proved - complete   [shostak](0.14 s)
    vec_from_trk..........................proved - complete   [shostak](0.01 s)
    track_x0_TCC1.........................proved - complete   [shostak](0.01 s)
    track_x0..............................proved - complete   [shostak](0.02 s)
    track_0x_TCC1.........................proved - complete   [shostak](0.01 s)
    track_0x..............................proved - complete   [shostak](0.02 s)
    track_xx_TCC1.........................proved - complete   [shostak](0.01 s)
    track_xx..............................proved - complete   [shostak](0.08 s)
    track_n0_TCC1.........................proved - complete   [shostak](0.01 s)
    track_n0..............................proved - complete   [shostak](0.05 s)
    track_0n_TCC1.........................proved - complete   [shostak](0.01 s)
    track_0n..............................proved - complete   [shostak](0.01 s)
    track_nx_TCC1.........................proved - complete   [shostak](0.02 s)
    track_nx..............................proved - complete   [shostak](0.20 s)
    track_xn_TCC1.........................proved - complete   [shostak](0.02 s)
    track_xn..............................proved - complete   [shostak](0.20 s)
    track_nn_TCC1.........................proved - complete   [shostak](0.02 s)
    track_nn..............................proved - complete   [shostak](0.20 s)
    vfrom_sub.............................proved - complete   [shostak](0.01 s)
    v_from_dot............................proved - complete   [shostak](0.04 s)
    v_from_dot_k..........................proved - complete   [shostak](0.16 s)
    dot_prod_tracks.......................proved - complete   [shostak](0.18 s)
    Theory totals: 32 formulas, 32 attempted, 32 succeeded (2.24 s)

 Proof summary for theory trackAngles_scaf
    track_exists_x........................proved - complete   [shostak](0.73 s)
    track_exists..........................proved - complete   [shostak](0.91 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.64 s)

 Proof summary for theory between_2D
    between_sym...........................proved - complete   [shostak](0.79 s)
    between_cos...........................proved - complete   [shostak](0.87 s)
    is_between............................proved - complete   [shostak](0.06 s)
    is_between2...........................proved - complete   [shostak](0.03 s)
    between_lem...........................proved - complete   [shostak](0.07 s)
    between_thm...........................proved - complete   [shostak](0.07 s)
    betw_between..........................proved - complete   [shostak](0.05 s)
    between_betw..........................proved - complete   [shostak](0.03 s)
    Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.96 s)

 Proof summary for theory vect3_basis
    vect3_orthog_toy_def..................proved - complete   [shostak](0.04 s)
    vect3_orthog_toz_def..................proved - complete   [shostak](0.13 s)
    vect3_orthonorm_toy_TCC1..............proved - complete   [shostak](0.02 s)
    vect3_orthonorm_toz_TCC1..............proved - complete   [shostak](1.70 s)
    vect3_orthonorm_basis.................proved - complete   [shostak](0.79 s)
    Equator_map_def.......................proved - complete   [shostak](1.39 s)
    Equator_map_inv_def...................proved - complete   [shostak](1.82 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (5.89 s)

 Proof summary for theory ECEF
    spherical2xyz_TCC1....................proved - complete   [shostak](0.50 s)
    spherical2xyz_TCC2....................proved - complete   [shostak](0.51 s)
    spherical2xyz_norm....................proved - complete   [shostak](0.51 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.52 s)

 Proof summary for theory vect_fun_ops
    caret_TCC1............................proved - complete   [shostak](0.04 s)
    diff_function.........................proved - complete   [shostak](0.06 s)
    div_function..........................proved - complete   [shostak](0.09 s)
    scal_function.........................proved - complete   [shostak](0.07 s)
    scaldiv_function......................proved - complete   [shostak](0.07 s)
    negneg_function.......................proved - complete   [shostak](0.05 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.38 s)

 Proof summary for theory vect2_fun_ops
    caret_TCC1............................proved - complete   [shostak](0.01 s)
    diff_function.........................proved - complete   [shostak](0.03 s)
    div_function..........................proved - complete   [shostak](0.06 s)
    scal_function.........................proved - complete   [shostak](0.04 s)
    scaldiv_function......................proved - complete   [shostak](0.03 s)
    negneg_function.......................proved - complete   [shostak](0.02 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.19 s)

 Proof summary for theory vect3_fun_ops
    caret_TCC1............................proved - complete   [shostak](0.00 s)
    diff_function.........................proved - complete   [shostak](0.03 s)
    div_function..........................proved - complete   [shostak](0.05 s)
    scal_function.........................proved - complete   [shostak](0.04 s)
    scaldiv_function......................proved - complete   [shostak](0.03 s)
    negneg_function.......................proved - complete   [shostak](0.01 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.16 s)

 Proof summary for theory linear_transformations_2D
    linear_transform_zero.................proved - complete   [shostak](0.01 s)
    linear_transform_scal.................proved - complete   [shostak](0.02 s)
    linear_transform_add..................proved - complete   [shostak](0.01 s)
    linear_transform_sub..................proved - complete   [shostak](0.03 s)
    linear_transform_rew..................proved - complete   [shostak](0.05 s)
    linear_transform_alt_left.............proved - complete   [shostak](0.08 s)
    linear_transform_alt_right............proved - complete   [shostak](0.17 s)
    linear_transform_perp_unique..........proved - complete   [shostak](0.10 s)
    linear_functional_zero................proved - complete   [shostak](0.05 s)
    linear_functional_scal................proved - complete   [shostak](0.07 s)
    linear_functional_add.................proved - complete   [shostak](0.07 s)
    linear_functional_sub.................proved - complete   [shostak](0.07 s)
    kernel_functional_nonempty............proved - complete   [shostak](0.10 s)
    linear_functional_is_dot..............proved - complete   [shostak](0.14 s)
    linear_functional_rew.................proved - complete   [shostak](0.16 s)
    linear_functional_alt_left............proved - complete   [shostak](0.15 s)
    linear_functional_alt_right...........proved - complete   [shostak](0.16 s)
    linear_functional_perp_unique.........proved - complete   [shostak](0.22 s)
    linear_functional_is_perp_dot.........proved - complete   [shostak](0.29 s)
    linear_functional_perp_signs_unique...proved - complete   [shostak](0.37 s)
    Theory totals: 20 formulas, 20 attempted, 20 succeeded (2.35 s)

 Proof summary for theory vectors_dot_alt
    dot_TCC1..............................proved - complete   [shostak](0.04 s)
    dot_rew_prep_TCC1.....................proved - complete   [shostak](0.04 s)
    dot_rew_prep_TCC2.....................proved - complete   [shostak](0.04 s)
    dot_rew_prep..........................proved - complete   [shostak](0.32 s)
    dot_rew...............................proved - complete   [shostak](0.05 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.49 s)

 Proof summary for theory test_vec
    t1....................................proved - complete   [shostak](0.00 s)
    t1b...................................proved - complete   [shostak](0.01 s)
    t1c...................................proved - complete   [shostak](0.01 s)
    t2....................................proved - complete   [shostak](0.00 s)
    t3....................................proved - complete   [shostak](0.01 s)
    t4....................................proved - complete   [shostak](0.01 s)
    t5....................................proved - complete   [shostak](0.01 s)
    t6....................................proved - complete   [shostak](0.01 s)
    t7....................................proved - complete   [shostak](0.00 s)
    t8....................................proved - complete   [shostak](0.02 s)
    t9....................................proved - complete   [shostak](0.03 s)
    t10...................................proved - complete   [shostak](0.02 s)
    t11...................................proved - complete   [shostak](0.01 s)
    t12...................................proved - complete   [shostak](0.01 s)
    t13...................................proved - complete   [shostak](0.01 s)
    t14...................................proved - complete   [shostak](0.00 s)
    t15...................................proved - complete   [shostak](0.21 s)
    t16...................................proved - complete   [shostak](0.04 s)
    t17...................................proved - complete   [shostak](0.02 s)
    t18...................................proved - complete   [shostak](0.03 s)
    t19...................................proved - complete   [shostak](0.02 s)
    t20...................................proved - complete   [shostak](0.06 s)
    t21...................................proved - complete   [shostak](0.06 s)
    t22...................................proved - complete   [shostak](0.08 s)
    t23...................................proved - complete   [shostak](0.03 s)
    t24...................................proved - complete   [shostak](0.04 s)
    t25...................................proved - complete   [shostak](0.09 s)
    t26...................................proved - complete   [shostak](0.05 s)
    t27...................................proved - complete   [shostak](0.10 s)
    t28...................................proved - complete   [shostak](0.13 s)
    t29...................................proved - complete   [shostak](0.09 s)
    t30...................................proved - complete   [shostak](0.16 s)
    t31...................................proved - complete   [shostak](0.01 s)
    t32...................................proved - complete   [shostak](0.01 s)
    t33...................................proved - complete   [shostak](0.08 s)
    t34...................................proved - complete   [shostak](0.03 s)
    t35...................................proved - complete   [shostak](0.05 s)
    t37...................................proved - complete   [shostak](0.15 s)
    t38...................................proved - complete   [shostak](0.05 s)
    t39...................................proved - complete   [shostak](0.19 s)
    t96...................................proved - complete   [shostak](0.12 s)
    Theory totals: 41 formulas, 41 attempted, 41 succeeded (2.11 s)

Grand Totals: 1445 proofs, 1445 attempted, 1445 succeeded (244.81 s)