|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
power_series_derivseq.prf
Sprache: Lisp
rahmenlose Ansicht.summary DruckansichtMT940 {MT940[881] Hlasm[2385] Haskell[2705]}Entwicklung
***
*** top (18:17:21 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 interval
Member_Proper.........................proved - complete [shostak](0.05 s)
Proper_Member.........................proved - complete [shostak](0.04 s)
r2i_Proper............................proved - complete [shostak](0.02 s)
Proper_eq_NonEmpty....................proved - complete [shostak](0.02 s)
Proper_NonEmpty.......................proved - complete [shostak](0.02 s)
eq_Incl...............................proved - complete [shostak](0.05 s)
Incl_Member...........................proved - complete [shostak](0.04 s)
Member_Incl...........................proved - complete [shostak](0.04 s)
Incl_Proper...........................proved - complete [shostak](0.03 s)
midpoint_inclusion....................proved - complete [shostak](0.05 s)
Lt_Ge.................................proved - complete [shostak](0.03 s)
Le_Gt.................................proved - complete [shostak](0.03 s)
Trichotomy............................proved - complete [shostak](0.05 s)
Abs_TCC1..............................proved - complete [shostak](0.06 s)
Abs_TCC2..............................proved - complete [shostak](0.09 s)
Sq_TCC1...............................proved - complete [shostak](0.03 s)
Sq_TCC2...............................proved - complete [shostak](0.02 s)
Sq_TCC3...............................proved - complete [shostak](0.05 s)
Pow_TCC1..............................proved - complete [shostak](0.06 s)
Pow_TCC2..............................proved - complete [shostak](0.05 s)
Pow_TCC3..............................proved - complete [shostak](0.06 s)
Pow_TCC4..............................proved - complete [shostak](0.05 s)
Pow_TCC5..............................proved - complete [shostak](0.06 s)
Pow_TCC6..............................proved - complete [shostak](0.05 s)
Intersection_inclusion................proved - complete [shostak](0.08 s)
Intersection_left_Empty...............proved - complete [shostak](0.04 s)
Intersection_right_Empty..............proved - complete [shostak](0.04 s)
Add_comm..............................proved - complete [shostak](0.02 s)
Mult_comm.............................proved - complete [shostak](-1.30 s)
Neg_Incl..............................proved - complete [shostak](0.03 s)
Zeroless0.............................proved - complete [shostak](0.03 s)
Neg_Ge_0..............................proved - complete [shostak](0.03 s)
Strict_Lt.............................proved - complete [shostak](0.04 s)
Halves................................proved - complete [shostak](0.09 s)
Halves_Incl...........................proved - complete [shostak](0.05 s)
Halves_inclusion......................proved - complete [shostak](0.06 s)
Incl_trans............................proved - complete [shostak](0.04 s)
Pow2_Sq...............................proved - complete [shostak](0.07 s)
Mult_Neg_Neg..........................proved - complete [shostak](0.98 s)
Mult_Neg_left.........................proved - complete [shostak](0.79 s)
Mult_Neg_right........................proved - complete [shostak](0.54 s)
Sq_Neg_eq.............................proved - complete [shostak](0.13 s)
Union_id..............................proved - complete [shostak](0.04 s)
Union_symm............................proved - complete [shostak](0.06 s)
Union_Incl_left.......................proved - complete [shostak](0.03 s)
Union_Incl_right......................proved - complete [shostak](0.04 s)
Add_0_r...............................proved - complete [shostak](0.03 s)
Add_0_l...............................proved - complete [shostak](0.06 s)
Mult_1_r..............................proved - complete [shostak](0.10 s)
Mult_1_l..............................proved - complete [shostak](0.09 s)
Div_1.................................proved - complete [shostak](0.09 s)
Pow_0.................................proved - complete [shostak](0.03 s)
Pow_1.................................proved - complete [shostak](0.09 s)
lb_interval...........................proved - complete [shostak](0.02 s)
lb_r2i................................proved - complete [shostak](0.02 s)
ub_interval...........................proved - complete [shostak](0.02 s)
ub_r2i................................proved - complete [shostak](0.01 s)
Incl_reflx............................proved - complete [shostak](0.02 s)
Incl_r2i..............................proved - complete [shostak](0.02 s)
Neg_Neg...............................proved - complete [shostak](0.04 s)
ub_inclusion..........................proved - complete [shostak](0.02 s)
lb_inclusion..........................proved - complete [shostak](0.02 s)
Neg_interval..........................proved - complete [shostak](0.02 s)
Pos_Gt_0..............................proved - complete [shostak](0.03 s)
NonNeg_Ge_0...........................proved - complete [shostak](0.02 s)
Pos_Neg_Lt_0..........................proved - complete [shostak](0.03 s)
NonNeg_Neg_Le_0.......................proved - complete [shostak](0.03 s)
r2i_sharp_eq..........................proved - complete [shostak](0.04 s)
r2i_Le................................proved - complete [shostak](0.02 s)
r2i_Lt................................proved - complete [shostak](0.03 s)
r2i_Ge................................proved - complete [shostak](0.03 s)
r2i_Gt................................proved - complete [shostak](0.03 s)
Lt_Le.................................proved - complete [shostak](0.03 s)
Gt_Ge.................................proved - complete [shostak](0.03 s)
inclusion_Gt..........................proved - complete [shostak](0.03 s)
inclusion_Ge..........................proved - complete [shostak](0.03 s)
inclusion_Lt..........................proved - complete [shostak](0.04 s)
inclusion_Le..........................proved - complete [shostak](0.03 s)
r2i_trans.............................proved - complete [shostak](0.04 s)
add2sub...............................proved - complete [shostak](0.06 s)
sub2add...............................proved - complete [shostak](0.06 s)
Member_trans..........................proved - complete [shostak](0.04 s)
r2i_inclusion.........................proved - complete [shostak](0.02 s)
Add_inclusion.........................proved - complete [shostak](0.06 s)
Sub_inclusion.........................proved - complete [shostak](0.06 s)
Neg_inclusion.........................proved - complete [shostak](0.03 s)
pXp...................................proved - complete [shostak](0.23 s)
nXp...................................proved - complete [shostak](0.06 s)
pXn...................................proved - complete [shostak](0.04 s)
nXn...................................proved - complete [shostak](0.23 s)
pXm...................................proved - complete [shostak](0.49 s)
mXp...................................proved - complete [shostak](0.04 s)
nXm...................................proved - complete [shostak](0.05 s)
mXn...................................proved - complete [shostak](0.03 s)
mXm...................................proved - complete [shostak](1.89 s)
Mult_inclusion........................proved - complete [shostak](0.77 s)
Abs_inclusion.........................proved - complete [shostak](0.15 s)
abs_sharp_le..........................proved - complete [shostak](0.04 s)
abs_sharp_lt..........................proved - complete [shostak](0.04 s)
pow_0_0...............................proved - complete [shostak](0.03 s)
pow_sq_TCC1...........................proved - complete [shostak](0.02 s)
pow_sq................................proved - complete [shostak](0.03 s)
pow_neg_n_odd_TCC1....................proved - complete [shostak](0.05 s)
pow_neg_n_odd_TCC2....................proved - complete [shostak](0.06 s)
pow_neg_n_odd.........................proved - complete [shostak](0.28 s)
pow_neg_odd_TCC1......................proved - complete [shostak](0.06 s)
pow_neg_odd_TCC2......................proved - complete [shostak](0.05 s)
pow_neg_odd...........................proved - complete [shostak](0.11 s)
pow_neg_n_even_TCC1...................proved - complete [shostak](0.02 s)
pow_neg_n_even_TCC2...................proved - complete [shostak](0.02 s)
pow_neg_n_even........................proved - complete [shostak](0.12 s)
pow_neg_even_TCC1.....................proved - complete [shostak](0.03 s)
pow_neg_even_TCC2.....................proved - complete [shostak](0.02 s)
pow_neg_even..........................proved - complete [shostak](0.07 s)
pow_pos_TCC1..........................proved - complete [shostak](0.02 s)
pow_pos...............................proved - complete [shostak](0.07 s)
pow_even_n_pos........................proved - complete [shostak](0.07 s)
pow_even_pos..........................proved - complete [shostak](0.06 s)
pow_odd_n_neg.........................proved - complete [shostak](0.22 s)
pow_odd_neg...........................proved - complete [shostak](0.09 s)
pow_incr_pos_TCC1.....................proved - complete [shostak](0.02 s)
pow_incr_pos..........................proved - complete [shostak](0.12 s)
pow_incr_odd_TCC1.....................proved - complete [shostak](0.06 s)
pow_incr_odd..........................proved - complete [shostak](0.19 s)
pow_decr_even_TCC1....................proved - complete [shostak](0.02 s)
pow_decr_even.........................proved - complete [shostak](0.13 s)
Pow_Neg_even..........................proved - complete [shostak](0.46 s)
Pow_inclusion_TCC1....................proved - complete [shostak](0.02 s)
Pow_inclusion.........................proved - complete [shostak](0.25 s)
Sq_inclusion..........................proved - complete [shostak](0.09 s)
Div_inclusion_TCC1....................proved - complete [shostak](0.04 s)
Div_inclusion.........................proved - complete [shostak](0.36 s)
Union_inclusion.......................proved - complete [shostak](0.07 s)
Reunion...............................proved - complete [shostak](0.27 s)
Sigma_TCC1............................proved - complete [shostak](0.03 s)
Sigma_TCC2............................proved - complete [shostak](0.06 s)
Sigma_inclusion_TCC1..................proved - complete [shostak](0.02 s)
Sigma_inclusion_TCC2..................proved - complete [shostak](0.04 s)
Sigma_inclusion.......................proved - complete [shostak](0.24 s)
Add_fundamental.......................proved - complete [shostak](0.07 s)
Sub_fundamental.......................proved - complete [shostak](0.05 s)
Abs_fundamental.......................proved - complete [shostak](0.35 s)
Neg_fundamental.......................proved - complete [shostak](0.03 s)
pXp_fundamental.......................proved - complete [shostak](0.50 s)
pXpm_fundamental......................proved - complete [shostak](0.61 s)
pXmm_fundamental......................proved - complete [shostak](0.66 s)
pX_fundamental........................proved - complete [shostak](1.31 s)
nX_fundamental........................proved - complete [shostak](0.14 s)
pmXpm_fundamental.....................proved - complete [shostak](0.93 s)
pmXmm_fundamental.....................proved - complete [shostak](0.81 s)
mmXmm_fundamental.....................proved - complete [shostak](1.51 s)
mX_fundamental........................proved - complete [shostak](2.17 s)
Mult_fundamental......................proved - complete [shostak](0.07 s)
Sq_p_fundamental......................proved - complete [shostak](0.24 s)
Sq_pm_fundamental.....................proved - complete [shostak](0.29 s)
Sq_fundamental........................proved - complete [shostak](0.75 s)
Div_fundamental.......................proved - complete [shostak](0.62 s)
Pow_p_fundamental.....................proved - complete [shostak](0.12 s)
Pow_pm_fundamental....................proved - complete [shostak](0.18 s)
Pow_m_fundamental.....................proved - complete [shostak](0.54 s)
Pow_fundamental.......................proved - complete [shostak](0.23 s)
Union_fundamental.....................proved - complete [shostak](0.09 s)
Mult_Strict_r2i.......................proved - complete [shostak](0.65 s)
Mult_r2i_Strict.......................proved - complete [shostak](0.65 s)
Pos_Zeroless..........................proved - complete [shostak](0.03 s)
Neg_Zeroless..........................proved - complete [shostak](0.03 s)
Pos_NonNeg............................proved - complete [shostak](0.03 s)
Pos_Add_NonNeg........................proved - complete [shostak](0.06 s)
NonNeg_Add_Pos........................proved - complete [shostak](0.07 s)
Neg_Add...............................proved - complete [shostak](0.07 s)
NonNeg_Add............................proved - complete [shostak](0.07 s)
Neg_Pos...............................proved - complete [shostak](0.03 s)
Pos_Neg...............................proved - complete [shostak](0.03 s)
Pos_Mult..............................proved - complete [shostak](0.87 s)
Neg_Mult..............................proved - complete [shostak](0.85 s)
NonNeg_Mult...........................proved - complete [shostak](-1.28 s)
Pos_Div...............................proved - complete [shostak](1.50 s)
Neg_Div...............................proved - complete [shostak](1.64 s)
NonNeg_Div............................proved - complete [shostak](0.80 s)
r2i_Pos...............................proved - complete [shostak](0.02 s)
r2i_Neg...............................proved - complete [shostak](0.03 s)
r2i_Nneg..............................proved - complete [shostak](0.02 s)
Sq_Pos................................proved - complete [shostak](0.20 s)
Sq_Neg................................proved - complete [shostak](0.19 s)
Abs_Pos...............................proved - complete [shostak](0.10 s)
Abs_Neg...............................proved - complete [shostak](0.10 s)
Proper_midpoint.......................proved - complete [shostak](0.06 s)
Includes_Proper.......................proved - complete [shostak](0.04 s)
Strict_Proper.........................proved - complete [shostak](0.04 s)
Strict_Add............................proved - complete [shostak](0.06 s)
Add_Strict............................proved - complete [shostak](0.06 s)
Proper_Add............................proved - complete [shostak](0.07 s)
Strict_Sub............................proved - complete [shostak](0.05 s)
Sub_Strict............................proved - complete [shostak](0.05 s)
Proper_Sub............................proved - complete [shostak](0.05 s)
Strict_Neg............................proved - complete [shostak](0.03 s)
Proper_Neg............................proved - complete [shostak](0.04 s)
Strict_Abs............................proved - complete [shostak](0.09 s)
Proper_Abs............................proved - complete [shostak](0.11 s)
Proper_Mult...........................proved - complete [shostak](0.06 s)
Proper_Div............................proved - complete [shostak](0.08 s)
Strict_Sq.............................proved - complete [shostak](0.27 s)
Proper_Pow............................proved - complete [shostak](0.06 s)
Proper_Sq.............................proved - complete [shostak](0.27 s)
Proper_size...........................proved - complete [shostak](0.05 s)
Strict_size...........................proved - complete [shostak](0.04 s)
Proper_HalfLeft.......................proved - complete [shostak](0.07 s)
Strict_HalfLeft.......................proved - complete [shostak](0.07 s)
Proper_HalfRight......................proved - complete [shostak](0.07 s)
Strict_HalfRightt.....................proved - complete [shostak](0.07 s)
Zeroless_Precondition.................proved - complete [shostak](0.05 s)
NonNeg_Precondition...................proved - complete [shostak](0.05 s)
Pos_Precondition......................proved - complete [shostak](0.05 s)
Neg_Precondition......................proved - complete [shostak](0.05 s)
Theory totals: 214 formulas, 214 attempted, 214 succeeded (33.64 s)
Proof summary for theory proper_arith
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory safe_arith
Proper_Safe1..........................proved - complete [shostak](0.03 s)
Proper_Safe1_pre......................proved - complete [shostak](0.04 s)
Proper_Safe2..........................proved - complete [shostak](0.04 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.11 s)
Proof summary for theory box
proper_box............................proved - complete [shostak](0.03 s)
proper_append.........................proved - complete [shostak](0.22 s)
vars_in_box_rec_TCC1..................proved - complete [shostak](0.03 s)
vars_in_box_rec_TCC2..................proved - complete [shostak](0.02 s)
vars_in_box_rec_TCC3..................proved - complete [shostak](0.07 s)
vars_in_box_rec_TCC4..................proved - complete [shostak](0.14 s)
vars_in_box_rec_TCC5..................proved - complete [shostak](0.08 s)
vars_in_box_rec_TCC6..................proved - complete [shostak](0.33 s)
vars_in_box...........................proved - complete [shostak](0.45 s)
midvars_TCC1..........................proved - complete [shostak](0.04 s)
Lbbox_TCC1............................proved - complete [shostak](0.02 s)
length_Lbbox..........................proved - complete [shostak](0.03 s)
Ubbox_TCC1............................proved - complete [shostak](0.02 s)
length_Ubbox..........................proved - complete [shostak](0.02 s)
Midbox_TCC1...........................proved - complete [shostak](0.03 s)
length_Midbox.........................proved - complete [shostak](0.02 s)
Inclusion?_TCC1.......................proved - complete [shostak](0.03 s)
Inclusion_reflx.......................proved - complete [shostak](0.03 s)
Inclusion_trans.......................proved - complete [shostak](0.06 s)
Inclusion_Proper......................proved - complete [shostak](0.06 s)
Lbbox_Proper..........................proved - complete [shostak](0.10 s)
Ubbox_Proper..........................proved - complete [shostak](0.09 s)
Midbox_Proper.........................proved - complete [shostak](0.16 s)
Lbbox_Inclusion.......................proved - complete [shostak](0.07 s)
Ubbox_Inclusion.......................proved - complete [shostak](0.08 s)
Midbox_Inclusion......................proved - complete [shostak](0.10 s)
vars_in_box_Inclusion.................proved - complete [shostak](0.07 s)
Theory totals: 27 formulas, 27 attempted, 27 succeeded (2.40 s)
Proof summary for theory interval_expr
r2E_TCC1..............................proved - complete [shostak](0.02 s)
I2E_TCC1..............................proved - complete [shostak](0.06 s)
PreTrue_TCC1..........................proved - complete [shostak](0.02 s)
real_bool_expr........................proved - complete [shostak](0.19 s)
eval_TCC1.............................proved - complete [shostak](0.07 s)
eval_TCC2.............................proved - complete [shostak](0.06 s)
eval_TCC3.............................proved - complete [shostak](0.07 s)
eval_TCC4.............................proved - complete [shostak](0.06 s)
eval_TCC5.............................proved - complete [shostak](0.08 s)
eval_TCC6.............................proved - complete [shostak](0.07 s)
eval_TCC7.............................proved - complete [shostak](0.07 s)
eval_TCC8.............................proved - complete [shostak](0.08 s)
eval_TCC9.............................proved - complete [shostak](0.07 s)
eval_TCC10............................proved - complete [shostak](0.09 s)
eval_TCC11............................proved - complete [shostak](0.08 s)
eval_TCC12............................proved - complete [shostak](0.08 s)
eval_TCC13............................proved - complete [shostak](0.09 s)
eval_TCC14............................proved - complete [shostak](0.08 s)
eval_TCC15............................proved - complete [shostak](0.09 s)
eval_TCC16............................proved - complete [shostak](0.10 s)
eval_TCC17............................proved - complete [shostak](0.09 s)
eval_TCC18............................proved - complete [shostak](0.10 s)
eval_TCC19............................proved - complete [shostak](0.11 s)
eval_TCC20............................proved - complete [shostak](0.10 s)
eval_TCC21............................proved - complete [shostak](0.13 s)
eval_TCC22............................proved - complete [shostak](0.12 s)
eval_TCC23............................proved - complete [shostak](0.10 s)
eval_TCC24............................proved - complete [shostak](0.09 s)
eval_TCC25............................proved - complete [shostak](0.11 s)
eval_TCC26............................proved - complete [shostak](0.10 s)
eval_TCC27............................proved - complete [shostak](0.12 s)
eval_TCC28............................proved - complete [shostak](0.10 s)
eval_TCC29............................proved - complete [shostak](0.14 s)
eval_TCC30............................proved - complete [shostak](0.08 s)
eval_TCC31............................proved - complete [shostak](0.12 s)
Eval_TCC1.............................proved - complete [shostak](0.05 s)
Eval_TCC2.............................proved - complete [shostak](0.11 s)
Eval_TCC3.............................proved - complete [shostak](0.14 s)
well_typed?_TCC1......................proved - complete [shostak](0.06 s)
well_typed?_TCC2......................proved - complete [shostak](0.09 s)
well_typed?_TCC3......................proved - complete [shostak](0.09 s)
well_typed?_TCC4......................proved - complete [shostak](0.10 s)
well_typed?_TCC5......................proved - complete [shostak](0.10 s)
well_typed?_TCC6......................proved - complete [shostak](0.11 s)
well_typed?_TCC7......................proved - complete [shostak](0.11 s)
well_typed?_TCC8......................proved - complete [shostak](0.13 s)
well_typed?_TCC9......................proved - complete [shostak](0.14 s)
Proper_well_typed.....................proved - complete [shostak](1.36 s)
Eval_inclusion........................proved - complete [shostak](1.78 s)
Eval_inclusion_Proper.................proved - complete [shostak](0.04 s)
well_typed_Proper.....................proved - complete [shostak](0.03 s)
Eval_fundamental_aux..................proved - complete [shostak](2.06 s)
well_typed_Inclusion_aux..............proved - complete [shostak](1.74 s)
well_typed_Inclusion..................proved - complete [shostak](0.03 s)
Proper_Inclusion......................proved - complete [shostak](0.05 s)
Eval_fundamental......................proved - complete [shostak](0.05 s)
Eval_fundamental_proper...............proved - complete [shostak](0.05 s)
split_TCC1............................proved - complete [shostak](0.05 s)
split_TCC2............................proved - complete [shostak](0.08 s)
split_TCC3............................proved - complete [shostak](0.05 s)
split_TCC4............................proved - complete [shostak](0.05 s)
split_TCC5............................proved - complete [shostak](0.09 s)
split_TCC6............................proved - complete [shostak](0.03 s)
split_TCC7............................proved - complete [shostak](0.17 s)
split_TCC8............................proved - complete [shostak](0.06 s)
split_TCC9............................proved - complete [shostak](0.28 s)
split_TCC10...........................proved - complete [shostak](0.04 s)
split_TCC11...........................proved - complete [shostak](0.03 s)
split_TCC12...........................proved - complete [shostak](0.03 s)
split_eq_TCC1.........................proved - complete [shostak](0.03 s)
split_eq_TCC2.........................proved - complete [shostak](0.10 s)
split_eq_TCC3.........................proved - complete [shostak](0.07 s)
split_eq_TCC4.........................proved - complete [shostak](0.07 s)
split_vars_in_box.....................proved - complete [shostak](0.17 s)
split_Inclusion.......................proved - complete [shostak](0.28 s)
split_Proper..........................proved - complete [shostak](0.12 s)
length_split_1........................proved - complete [shostak](0.03 s)
length_split_2........................proved - complete [shostak](0.04 s)
Theory totals: 78 formulas, 78 attempted, 78 succeeded (13.44 s)
Proof summary for theory interval_bexpr
beval_TCC1...........................proved - complete [shostak]( 0.06 s)
beval_TCC2...........................proved - complete [shostak]( 0.06 s)
beval_TCC3...........................proved - complete [shostak]( 0.05 s)
beval_TCC4...........................proved - complete [shostak]( 0.07 s)
beval_TCC5...........................proved - complete [shostak]( 0.07 s)
beval_TCC6...........................proved - complete [shostak]( 0.06 s)
beval_TCC7...........................proved - complete [shostak]( 0.07 s)
beval_TCC8...........................proved - complete [shostak]( 0.08 s)
beval_TCC9...........................proved - complete [shostak]( 0.07 s)
beval_TCC10..........................proved - complete [shostak]( 0.07 s)
beval_TCC11..........................proved - complete [shostak]( 0.09 s)
beval_TCC12..........................proved - complete [shostak]( 0.07 s)
beval_TCC13..........................proved - complete [shostak]( 0.09 s)
beval_TCC14..........................proved - complete [shostak]( 0.20 s)
beval_TCC15..........................proved - complete [shostak]( 0.22 s)
beval_TCC16..........................proved - complete [shostak]( 0.26 s)
beval_TCC17..........................proved - complete [shostak]( 0.32 s)
beval_TCC18..........................proved - complete [shostak]( 0.24 s)
beval_TCC19..........................proved - complete [shostak]( 0.07 s)
beval_TCC20..........................proved - complete [shostak]( 0.10 s)
beval_TCC21..........................proved - complete [shostak]( 0.11 s)
beval_TCC22..........................proved - complete [shostak]( 0.11 s)
BEval_TCC1...........................proved - complete [shostak]( 0.06 s)
BEval_TCC2...........................proved - complete [shostak]( 0.07 s)
BEval_TCC3...........................proved - complete [shostak]( 0.08 s)
BEval_TCC4...........................proved - complete [shostak]( 0.08 s)
BEval_TCC5...........................proved - complete [shostak]( 0.08 s)
BEval_TCC6...........................proved - complete [shostak]( 0.08 s)
BEval_TCC7...........................proved - complete [shostak]( 0.09 s)
BEval_TCC8...........................proved - complete [shostak]( 0.22 s)
BEval_TCC9...........................proved - complete [shostak]( 0.24 s)
BEval_TCC10..........................proved - complete [shostak]( 0.25 s)
BEval_TCC11..........................proved - complete [shostak]( 0.12 s)
BEval_TCC12..........................proved - complete [shostak]( 0.12 s)
BEval_TCC13..........................proved - complete [shostak]( 0.12 s)
BEval_TCC14..........................proved - complete [shostak]( 0.13 s)
BEval_inclusion......................proved - complete [shostak]( 3.18 s)
BEval_inclusion_Proper...............proved - complete [shostak]( 0.04 s)
BEval_fundamental....................proved - complete [shostak](18.51 s)
Theory totals: 39 formulas, 39 attempted, 39 succeeded (26.01 s)
Proof summary for theory simple_bandb
altvar_TCC1...........................proved - complete [shostak](0.14 s)
altvar_TCC2...........................proved - complete [shostak](0.22 s)
simple_interval_soundness.............proved - complete [shostak](0.86 s)
simple_test...........................proved - complete [shostak](1.10 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (2.31 s)
Proof summary for theory numerical_bandb
evaluate_TCC1.........................proved - complete [shostak](0.05 s)
evaluate_TCC2.........................proved - complete [shostak](0.05 s)
mindir_maxvar_aux_TCC1................proved - complete [shostak](0.07 s)
mindir_maxvar_aux_TCC2................proved - complete [shostak](0.74 s)
max_rec_TCC1..........................proved - complete [shostak](0.03 s)
max_rec_TCC2..........................proved - complete [shostak](0.11 s)
max_rec_TCC3..........................proved - complete [shostak](0.12 s)
max_rec_TCC4..........................proved - complete [shostak](0.09 s)
max_rec_TCC5..........................proved - complete [shostak](0.12 s)
max_rec_TCC6..........................proved - complete [shostak](0.11 s)
max_rec_TCC7..........................proved - complete [shostak](0.12 s)
max_rec_TCC8..........................proved - complete [shostak](0.09 s)
max_rec_TCC9..........................proved - complete [shostak](-1.59 s)
max_rec_TCC10.........................proved - complete [shostak](0.11 s)
max_rec_TCC11.........................proved - complete [shostak](0.08 s)
max_aux_TCC1..........................proved - complete [shostak](0.03 s)
max_aux_TCC2..........................proved - complete [shostak](0.04 s)
max_aux_TCC3..........................proved - complete [shostak](0.03 s)
max_aux_TCC4..........................proved - complete [shostak](0.05 s)
max_aux_TCC5..........................proved - complete [shostak](0.07 s)
altvar_TCC1...........................proved - complete [shostak](0.05 s)
altvar_TCC2...........................proved - complete [shostak](0.05 s)
interval_minmax_soundness.............proved - complete [shostak](3.59 s)
numerical_soundness...................proved - complete [shostak](0.03 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (4.25 s)
Proof summary for theory interval_bandb
evaluate_TCC1.........................proved - complete [shostak](0.09 s)
combine_TCC1..........................proved - complete [shostak](0.11 s)
max_rec_TCC1..........................proved - complete [shostak](0.03 s)
max_rec_TCC2..........................proved - complete [shostak](0.11 s)
max_rec_TCC3..........................proved - complete [shostak](0.12 s)
max_rec_TCC4..........................proved - complete [shostak](0.08 s)
max_rec_TCC5..........................proved - complete [shostak](0.12 s)
max_rec_TCC6..........................proved - complete [shostak](0.11 s)
max_rec_TCC7..........................proved - complete [shostak](0.12 s)
max_rec_TCC8..........................proved - complete [shostak](0.09 s)
max_rec_TCC9..........................proved - complete [shostak](0.12 s)
max_rec_TCC10.........................proved - complete [shostak](0.11 s)
max_rec_TCC11.........................proved - complete [shostak](0.07 s)
max_aux_TCC1..........................proved - complete [shostak](0.03 s)
max_aux_TCC2..........................proved - complete [shostak](0.05 s)
max_aux_TCC3..........................proved - complete [shostak](0.03 s)
max_aux_TCC4..........................proved - complete [shostak](0.04 s)
max_aux_TCC5..........................proved - complete [shostak](0.08 s)
altvar_TCC1...........................proved - complete [shostak](0.05 s)
altvar_TCC2...........................proved - complete [shostak](0.05 s)
interval_soundness....................proved - complete [shostak](2.44 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (4.06 s)
Proof summary for theory interval_bolzano
bolzano_bisect_TCC1...................proved - complete [shostak](0.16 s)
bolzano_bisect_TCC2...................proved - complete [shostak](0.12 s)
bolzano_bisect_TCC3...................proved - complete [shostak](0.06 s)
bolzano_bisect_TCC4...................proved - complete [shostak](0.16 s)
bolzano_bisect_TCC5...................proved - complete [shostak](0.12 s)
bolzano_bisect_TCC6...................proved - complete [shostak](0.11 s)
bolzano_bisect_TCC7...................proved - complete [shostak](0.12 s)
bolzano_bisect_TCC8...................proved - complete [shostak](0.13 s)
SqrtProp..............................proved - complete [shostak](0.13 s)
sqrt_bisect_TCC1......................proved - complete [shostak](0.28 s)
sqrt_bisect_TCC2......................proved - complete [shostak](0.05 s)
sqrt_bisect_inclusion.................proved - complete [shostak](0.20 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.64 s)
Proof summary for theory interval_sqrt
Sqrt_TCC1.............................proved - complete [shostak](0.03 s)
Sqrt_TCC2.............................proved - complete [shostak](0.02 s)
Sqrt_TCC3.............................proved - complete [shostak](0.03 s)
Sqrt_TCC4.............................proved - complete [shostak](0.02 s)
Sqrt_inclusion_TCC1...................proved - complete [shostak](0.04 s)
Sqrt_inclusion........................proved - complete [shostak](0.09 s)
Sqrt_fundamental......................proved - complete [shostak](0.35 s)
Proper_Sqrt...........................proved - complete [shostak](0.06 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.64 s)
Proof summary for theory interval_trig
cos_error_pi_lbn_bound................proved - incomplete [shostak](-.99 s)
Pi_TCC1...............................proved - incomplete [shostak](0.03 s)
Cos_fundamental.......................proved - incomplete [shostak](3.77 s)
Sin_fundamental.......................proved - incomplete [shostak](8.64 s)
tan_0_pi2_TCC1........................proved - complete [shostak](0.03 s)
tan_0_pi2_TCC2........................proved - complete [shostak](0.03 s)
tan_npi2_pi2_TCC1.....................proved - complete [shostak](0.03 s)
tan_npi2_pi2_TCC2.....................proved - complete [shostak](0.03 s)
tan_npi2_pi2_union....................proved - incomplete [shostak](3.41 s)
Tan_proper............................proved - incomplete [shostak](1.20 s)
Atan_fundamental......................proved - incomplete [shostak](0.05 s)
Pi_inclusion..........................proved - incomplete [shostak](0.04 s)
Pi_proper.............................proved - incomplete [shostak](0.03 s)
sin_npi2_pi2..........................proved - incomplete [shostak](0.40 s)
sin_pi2_pi............................proved - incomplete [shostak](0.35 s)
sin_0_pi..............................proved - incomplete [shostak](0.19 s)
sin_npi_0.............................proved - incomplete [shostak](0.09 s)
sin_npi_npi2..........................proved - incomplete [shostak](0.10 s)
cos_0_pi..............................proved - incomplete [shostak](0.08 s)
cos_npi_0.............................proved - incomplete [shostak](0.07 s)
cos_npi2_pi2..........................proved - incomplete [shostak](0.17 s)
Cos_inclusion.........................proved - incomplete [shostak](0.41 s)
Sin_inclusion.........................proved - incomplete [shostak](-.69 s)
Tan_pi2_def...........................proved - incomplete [shostak](0.11 s)
cos_lb_gt_0_pos.......................proved - incomplete [shostak](0.10 s)
cos_lb_gt_0...........................proved - incomplete [shostak](0.09 s)
cos_ub_gt_0...........................proved - incomplete [shostak](0.06 s)
cos_lb_ub_gt_0........................proved - incomplete [shostak](0.15 s)
tan_0_pi2_TCC3........................proved - incomplete [shostak](0.08 s)
tan_0_pi2.............................proved - incomplete [shostak](0.24 s)
tan_npi2_0_TCC1.......................proved - incomplete [shostak](0.07 s)
tan_npi2_0............................proved - incomplete [shostak](0.09 s)
tan_npi2_pi2_TCC3.....................proved - incomplete [shostak](0.06 s)
tan_npi2_pi2..........................proved - incomplete [shostak](0.25 s)
TAN?_TCC1.............................proved - complete [shostak](0.03 s)
TAN_Tan...............................proved - incomplete [shostak](0.17 s)
Tan_inclusion_TCC1....................proved - incomplete [shostak](0.03 s)
Tan_inclusion.........................proved - incomplete [shostak](0.27 s)
Tan_fundamental.......................proved - incomplete [shostak](7.26 s)
Atan_inclusion........................proved - incomplete [shostak](0.08 s)
Strict_Tan............................proved - incomplete [shostak](0.99 s)
Proper_Sin............................proved - incomplete [shostak](0.04 s)
Proper_Cos............................proved - incomplete [shostak](0.04 s)
Proper_Tan............................proved - incomplete [shostak](0.05 s)
Proper_Atan...........................proved - incomplete [shostak](0.05 s)
Theory totals: 45 formulas, 45 attempted, 45 succeeded (27.78 s)
Proof summary for theory interval_lnexp
Exp_TCC1..............................proved - incomplete [shostak](0.05 s)
Exp_fundamental.......................proved - incomplete [shostak](0.05 s)
Ln_TCC1...............................proved - complete [shostak](0.04 s)
Ln_TCC2...............................proved - complete [shostak](0.03 s)
Ln_fundamental........................proved - incomplete [shostak](0.06 s)
Exp_inclusion.........................proved - incomplete [shostak](0.07 s)
Ln_inclusion_TCC1.....................proved - complete [shostak](0.04 s)
Ln_inclusion..........................proved - incomplete [shostak](0.10 s)
Proper_Ln.............................proved - incomplete [shostak](0.09 s)
Proper_Exp............................proved - incomplete [shostak](0.04 s)
proper_Exp_TCC1.......................proved - incomplete [shostak](0.05 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.62 s)
Proof summary for theory interval_deriv
deriv_domain_Xt.......................proved - complete [shostak](0.17 s)
IMP_derivatives_TCC1..................proved - complete [shostak](0.03 s)
IMP_derivatives_TCC2..................proved - complete [shostak](0.06 s)
D_TCC1................................proved - complete [shostak](0.03 s)
Diffn?_TCC1...........................proved - complete [shostak](0.04 s)
Diffn?_TCC2...........................proved - complete [shostak](0.03 s)
Diffn_derivn..........................proved - complete [shostak](0.21 s)
Dn_TCC1...............................proved - complete [shostak](0.04 s)
Dn_TCC2...............................proved - complete [shostak](0.03 s)
Dn_TCC3...............................proved - complete [shostak](0.04 s)
Dn_TCC4...............................proved - complete [shostak](0.04 s)
Dn_nderiv_TCC1........................proved - complete [shostak](0.03 s)
Dn_nderiv.............................proved - complete [shostak](0.23 s)
Diff_id...............................proved - complete [shostak](0.03 s)
D_id_TCC1.............................proved - complete [shostak](0.03 s)
D_id..................................proved - complete [shostak](0.03 s)
Diff_const............................proved - complete [shostak](0.69 s)
D_const_TCC1..........................proved - complete [shostak](0.03 s)
D_const...............................proved - complete [shostak](0.03 s)
Diff_add..............................proved - complete [shostak](0.05 s)
D_add_TCC1............................proved - complete [shostak](0.04 s)
D_add.................................proved - complete [shostak](0.04 s)
Diff_mult.............................proved - complete [shostak](0.05 s)
D_mult_TCC1...........................proved - complete [shostak](0.03 s)
D_mult................................proved - complete [shostak](0.04 s)
Diff_pow_TCC1.........................proved - complete [shostak](0.04 s)
Diff_pow..............................proved - complete [shostak](0.14 s)
D_pow_TCC1............................proved - complete [shostak](0.03 s)
D_pow_TCC2............................proved - complete [shostak](0.03 s)
D_pow_TCC3............................proved - complete [shostak](0.03 s)
D_pow.................................proved - complete [shostak](0.14 s)
Diff_scal1............................proved - complete [shostak](0.05 s)
D_scal1_TCC1..........................proved - complete [shostak](0.03 s)
D_scal1...............................proved - complete [shostak](0.04 s)
Diff_scal2............................proved - complete [shostak](0.06 s)
D_scal2_TCC1..........................proved - complete [shostak](0.03 s)
D_scal2...............................proved - complete [shostak](0.07 s)
Diff_neg..............................proved - complete [shostak](0.04 s)
D_neg_TCC1............................proved - complete [shostak](0.03 s)
D_neg.................................proved - complete [shostak](0.04 s)
Diff_sub..............................proved - complete [shostak](0.04 s)
D_sub_TCC1............................proved - complete [shostak](0.03 s)
D_sub.................................proved - complete [shostak](0.05 s)
Diff_sq...............................proved - complete [shostak](0.06 s)
D_sq_TCC1.............................proved - complete [shostak](0.03 s)
D_sq..................................proved - complete [shostak](0.12 s)
Diff_div_TCC1.........................proved - complete [shostak](0.04 s)
Diff_div..............................proved - complete [shostak](0.05 s)
D_div_TCC1............................proved - complete [shostak](0.04 s)
D_div_TCC2............................proved - complete [shostak](0.09 s)
D_div.................................proved - complete [shostak](0.14 s)
Diff_scald1...........................proved - complete [shostak](0.06 s)
D_scald1_TCC1.........................proved - complete [shostak](0.03 s)
D_scald1..............................proved - complete [shostak](0.10 s)
Diff_scald2...........................proved - complete [shostak](0.07 s)
D_scald2_TCC1.........................proved - complete [shostak](0.03 s)
D_scald2..............................proved - complete [shostak](0.09 s)
Diff_sin..............................proved - incomplete [shostak](0.04 s)
D_sin_TCC1............................proved - incomplete [shostak](0.03 s)
D_sin.................................proved - incomplete [shostak](0.07 s)
Diff_cos..............................proved - incomplete [shostak](0.04 s)
D_cos_TCC1............................proved - incomplete [shostak](0.02 s)
D_cos.................................proved - incomplete [shostak](0.28 s)
Diff_tan_TCC1.........................proved - complete [shostak](0.03 s)
Diff_tan_TCC2.........................proved - incomplete [shostak](0.79 s)
Diff_tan..............................proved - incomplete [shostak](0.13 s)
D_tan_TCC1............................proved - incomplete [shostak](0.10 s)
D_tan_TCC2............................proved - incomplete [shostak](0.12 s)
D_tan.................................proved - incomplete [shostak](0.25 s)
Diff_atan.............................proved - incomplete [shostak](0.04 s)
D_atan_TCC1...........................proved - incomplete [shostak](0.03 s)
D_atan................................proved - incomplete [shostak](0.17 s)
Diff_sqrt_TCC1........................proved - complete [shostak](0.04 s)
Diff_sqrt.............................proved - complete [shostak](0.11 s)
D_sqrt_TCC1...........................proved - complete [shostak](0.03 s)
D_sqrt_TCC2...........................proved - complete [shostak](0.09 s)
D_sqrt................................proved - complete [shostak](0.47 s)
Diff_exp..............................proved - incomplete [shostak](0.04 s)
D_exp_TCC1............................proved - incomplete [shostak](0.03 s)
D_exp.................................proved - incomplete [shostak](0.07 s)
Diff_ln_TCC1..........................proved - complete [shostak](0.05 s)
Diff_ln...............................proved - incomplete [shostak](0.11 s)
D_ln_TCC1.............................proved - incomplete [shostak](0.03 s)
D_ln_TCC2.............................proved - complete [shostak](0.05 s)
D_ln..................................proved - incomplete [shostak](0.38 s)
Diff_I................................proved - complete [shostak](0.02 s)
D_I_TCC1..............................proved - complete [shostak](0.04 s)
D_I_TCC2..............................proved - complete [shostak](0.04 s)
D_I...................................proved - complete [shostak](0.04 s)
Theory totals: 89 formulas, 89 attempted, 89 succeeded (7.71 s)
Proof summary for theory subinterval_deriv
deriv_domain_Xt.......................proved - complete [shostak](0.17 s)
subinterval_deriv_TCC1................proved - complete [shostak](1.68 s)
subinterval_deriv.....................proved - complete [shostak](0.25 s)
subinterval_derivn_TCC1...............proved - complete [shostak](0.08 s)
subinterval_derivn....................proved - complete [shostak](0.23 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.41 s)
Proof summary for theory interval_chain
IMP_chain_rule_TCC1...................proved - complete [shostak](0.02 s)
IMP_chain_rule_TCC2...................proved - complete [shostak](0.06 s)
IMP_chain_rule_TCC3...................proved - complete [shostak](0.02 s)
IMP_chain_rule_TCC4...................proved - complete [shostak](0.07 s)
Diff_comp_TCC1........................proved - complete [shostak](0.03 s)
Diff_comp.............................proved - complete [shostak](0.05 s)
Deriv_comp_TCC1.......................proved - complete [shostak](0.03 s)
Deriv_comp............................proved - complete [shostak](0.08 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.36 s)
Proof summary for theory interval_taylor
IMP_taylors_TCC1......................proved - complete [shostak](0.05 s)
IMP_taylors_TCC2......................proved - complete [shostak](0.06 s)
Taylor_TCC1...........................proved - complete [shostak](0.05 s)
Taylor................................proved - complete [shostak](0.61 s)
Taylor1_Midpoint......................proved - complete [shostak](0.07 s)
Taylor2_Midpoint_TCC1.................proved - complete [shostak](0.03 s)
Taylor2_Midpoint_TCC2.................proved - complete [shostak](0.05 s)
Taylor2_Midpoint......................proved - complete [shostak](0.10 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.03 s)
Proof summary for theory interval_io
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory interval_expr_sqrt
sqrt_is_safe..........................proved - complete [shostak](0.03 s)
Sqrt_Inclusion........................proved - complete [shostak](0.05 s)
Sqrt_Fundamental......................proved - complete [shostak](0.03 s)
SQRT_n_TCC1...........................proved - complete [shostak](0.02 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.13 s)
Proof summary for theory interval_expr_trig
Pi_Inclusion..........................proved - incomplete [shostak](0.03 s)
Sin_Inclusion.........................proved - incomplete [shostak](0.03 s)
Sin_Fundamental.......................proved - incomplete [shostak](0.04 s)
SIN_n_TCC1............................proved - incomplete [shostak](0.03 s)
Cos_Inclusion.........................proved - incomplete [shostak](0.03 s)
Cos_Fundamental.......................proved - incomplete [shostak](0.03 s)
COS_n_TCC1............................proved - incomplete [shostak](0.03 s)
Tan_Inclusion.........................proved - incomplete [shostak](0.04 s)
Tan_Fundamental.......................proved - incomplete [shostak](0.03 s)
TAN_Precondition......................proved - incomplete [shostak](0.13 s)
TAN_n_TCC1............................proved - incomplete [shostak](0.06 s)
Atan_Inclusion........................proved - incomplete [shostak](0.04 s)
Atan_Fundamental......................proved - incomplete [shostak](0.03 s)
ATAN_n_TCC1...........................proved - incomplete [shostak](0.03 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.57 s)
Proof summary for theory interval_expr_lnexp
ln_safe_TCC1..........................proved - complete [shostak](0.03 s)
Ln_Inclusion..........................proved - incomplete [shostak](0.08 s)
Ln_Fundamental........................proved - incomplete [shostak](0.03 s)
LN_n_TCC1.............................proved - incomplete [shostak](0.03 s)
Exp_Inclusion.........................proved - incomplete [shostak](0.04 s)
Exp_Fundamental.......................proved - incomplete [shostak](0.04 s)
EXP_n_TCC1............................proved - incomplete [shostak](0.05 s)
E_Inclusion...........................proved - incomplete [shostak](0.07 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.37 s)
Proof summary for theory strategies4Q
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory examples4Q
zero_to_one_quarter...................proved - complete [shostak](-.97 s)
Heart_TCC1............................proved - complete [shostak](0.03 s)
Heart_TCC2............................proved - complete [shostak](0.02 s)
hdp_mm_TCC1...........................proved - complete [shostak](0.03 s)
hdp_mm_TCC2...........................proved - complete [shostak](0.03 s)
hdp_mm_TCC3...........................proved - complete [shostak](0.03 s)
hdp_mm_TCC4...........................proved - complete [shostak](0.03 s)
hdp_mm_TCC5...........................proved - complete [shostak](0.02 s)
hdp_mm_TCC6...........................proved - complete [shostak](0.03 s)
hdp_mm................................proved - complete [shostak](4.69 s)
hdp_minmax............................proved - complete [shostak](7.04 s)
common_point_TCC1.....................proved - complete [shostak](0.03 s)
common_point..........................proved - complete [shostak](0.51 s)
simple_ite............................proved - complete [shostak](0.50 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (12.02 s)
Proof summary for theory strategies
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory examples
sqrt23................................proved - incomplete [shostak](1.35 s)
sin6sqrt2.............................proved - incomplete [shostak](1.59 s)
sqrtx3_TCC1...........................proved - complete [shostak](0.04 s)
sqrtx3................................proved - incomplete [shostak](1.24 s)
tr_TCC1...............................proved - incomplete [shostak](0.09 s)
tr_250_35_TCC1........................proved - incomplete [shostak](1.16 s)
tr_250_35.............................proved - incomplete [shostak](2.19 s)
tr_200_250_abs_35.....................proved - incomplete [shostak](2.45 s)
G_TCC1................................proved - complete [shostak](0.03 s)
A_and_S_TCC1..........................proved - complete [shostak](0.05 s)
A_and_S_TCC2..........................proved - complete [shostak](0.06 s)
A_and_S...............................proved - incomplete [shostak](1.03 s)
common_point_TCC1.....................proved - complete [shostak](0.04 s)
common_point_TCC2.....................proved - complete [shostak](0.03 s)
common_point_TCC3.....................proved - incomplete [shostak](-1.51 s)
common_point_TCC4.....................proved - incomplete [shostak](0.21 s)
common_point..........................proved - incomplete [shostak](4.70 s)
r_TCC1................................proved - complete [shostak](0.03 s)
r_TCC2................................proved - complete [shostak](0.03 s)
atan_implementation...................proved - incomplete [shostak](0.26 s)
ex1_ba_TCC1...........................proved - complete [shostak](0.04 s)
ex1_ba_TCC2...........................proved - complete [shostak](0.06 s)
ex1_ba................................proved - incomplete [shostak](1.20 s)
ex2_ba_TCC1...........................proved - complete [shostak](0.05 s)
ex2_ba................................proved - incomplete [shostak](1.10 s)
ex3_ba_TCC1...........................proved - complete [shostak](0.05 s)
ex3_ba................................proved - incomplete [shostak](1.23 s)
ex4_ba................................proved - incomplete [shostak](1.26 s)
ex5_ba_TCC1...........................proved - complete [shostak](0.08 s)
ex5_ba................................proved - incomplete [shostak](1.35 s)
ex6_ba................................proved - incomplete [shostak](1.23 s)
ex7_ba................................proved - incomplete [shostak](1.17 s)
Tunnel_3_IL...........................proved - incomplete [shostak](1.80 s)
Tunnel_3_IL_LU........................proved - incomplete [shostak](1.97 s)
Theory totals: 34 formulas, 34 attempted, 34 succeeded (27.65 s)
Proof summary for theory top_allen
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory allen_interval
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory allen_interval_properties
before_before.........................proved - complete [shostak](0.04 s)
before_during.........................proved - complete [shostak](0.04 s)
before_contains.......................proved - complete [shostak](0.03 s)
before_overlaps.......................proved - complete [shostak](0.03 s)
before_overlapped_by..................proved - complete [shostak](0.04 s)
before_meets..........................proved - complete [shostak](0.03 s)
before_met_by.........................proved - complete [shostak](0.04 s)
before_starts.........................proved - complete [shostak](0.03 s)
before_started_by.....................proved - complete [shostak](0.03 s)
before_finishes.......................proved - complete [shostak](0.04 s)
before_finished_by....................proved - complete [shostak](0.03 s)
after_after...........................proved - complete [shostak](0.03 s)
after_during..........................proved - complete [shostak](0.04 s)
after_contains........................proved - complete [shostak](0.04 s)
after_overlaps........................proved - complete [shostak](0.04 s)
after_meets...........................proved - complete [shostak](0.04 s)
after_met_by..........................proved - complete [shostak](0.03 s)
after_starts..........................proved - complete [shostak](0.04 s)
after_started_by......................proved - complete [shostak](0.03 s)
after_finishes........................proved - complete [shostak](0.03 s)
after_finished_by.....................proved - complete [shostak](0.04 s)
during_before.........................proved - complete [shostak](0.03 s)
during_after..........................proved - complete [shostak](0.03 s)
during_during.........................proved - complete [shostak](0.03 s)
during_overlaps.......................proved - complete [shostak](0.05 s)
during_overlapped_by..................proved - complete [shostak](0.05 s)
during_meets..........................proved - complete [shostak](0.03 s)
during_t_meet_bay.....................proved - complete [shostak](0.03 s)
during_starts.........................proved - complete [shostak](0.03 s)
during_started_by.....................proved - complete [shostak](0.05 s)
during_finished_by....................proved - complete [shostak](0.04 s)
during_finishes.......................proved - complete [shostak](0.04 s)
contains_before.......................proved - complete [shostak](0.05 s)
contains_after........................proved - complete [shostak](0.04 s)
contains_during.......................proved - complete [shostak](0.07 s)
contains_contains.....................proved - complete [shostak](0.03 s)
contains_overlaps.....................proved - complete [shostak](0.05 s)
contains_overlapped_by................proved - complete [shostak](0.04 s)
contains_meets........................proved - complete [shostak](0.04 s)
contains_meet_by......................proved - complete [shostak](0.04 s)
contains_starts.......................proved - complete [shostak](0.04 s)
contains_started_by...................proved - complete [shostak](0.04 s)
contains_finishes.....................proved - complete [shostak](0.04 s)
contains_finished_by..................proved - complete [shostak](0.04 s)
overlaps_before.......................proved - complete [shostak](0.03 s)
overlaps_after........................proved - complete [shostak](0.05 s)
overlaps_during.......................proved - complete [shostak](0.05 s)
overlaps_overlapped_by................proved - complete [shostak](0.07 s)
overlaps_contains.....................proved - complete [shostak](0.05 s)
overlaps_overlaps.....................proved - complete [shostak](0.04 s)
overlaps_meets........................proved - complete [shostak](0.03 s)
overlaps_met_by.......................proved - complete [shostak](0.04 s)
overlaps_starts.......................proved - complete [shostak](0.04 s)
overlaps_start_by.....................proved - complete [shostak](0.05 s)
overlaps_finishes.....................proved - complete [shostak](0.04 s)
overlaps_finished_by..................proved - complete [shostak](0.04 s)
overlapped_by_before..................proved - complete [shostak](0.05 s)
overlapped_by_after...................proved - complete [shostak](0.03 s)
overlapped_by_during..................proved - complete [shostak](0.04 s)
overlapped_by_contains................proved - complete [shostak](0.05 s)
overlapped_by_overlaps................proved - complete [shostak](0.07 s)
overlapped_by_overlapped_by...........proved - complete [shostak](0.05 s)
overlapped_by_meets...................proved - complete [shostak](0.04 s)
overlapped_by_meet_by.................proved - complete [shostak](0.03 s)
overlapped_by_starts..................proved - complete [shostak](0.05 s)
overlapped_by_started_by..............proved - complete [shostak](0.04 s)
overlapped_by_finishes................proved - complete [shostak](0.04 s)
overlapped_by_finished_by.............proved - complete [shostak](0.04 s)
meets_before..........................proved - complete [shostak](0.03 s)
meets_after...........................proved - complete [shostak](0.04 s)
meets_during..........................proved - complete [shostak](0.04 s)
meets_contains........................proved - complete [shostak](0.03 s)
meets_overlaps........................proved - complete [shostak](0.03 s)
meets_overlapped_by...................proved - complete [shostak](0.04 s)
meets_meets...........................proved - complete [shostak](0.03 s)
meets_meet_by.........................proved - complete [shostak](0.03 s)
meets_starts..........................proved - complete [shostak](0.03 s)
meets_started_by......................proved - complete [shostak](0.03 s)
meets_finishes........................proved - complete [shostak](0.04 s)
meets_finished_by.....................proved - complete [shostak](0.03 s)
meet_by_before........................proved - complete [shostak](0.05 s)
meet_by_after.........................proved - complete [shostak](0.02 s)
meet_by_during........................proved - complete [shostak](0.05 s)
meet_by_contains......................proved - complete [shostak](0.03 s)
meet_by_overlaps......................proved - complete [shostak](0.04 s)
meet_by_meet..........................proved - complete [shostak](0.03 s)
meet_by_overlapped_by.................proved - complete [shostak](0.03 s)
meet_by_meet_by.......................proved - complete [shostak](0.03 s)
meet_by_starts........................proved - complete [shostak](0.04 s)
meet_by_started_by....................proved - complete [shostak](0.04 s)
meet_by_finishes......................proved - complete [shostak](0.03 s)
met_by_finished.......................proved - complete [shostak](0.03 s)
starts_by_before......................proved - complete [shostak](0.03 s)
starts_by_after.......................proved - complete [shostak](0.03 s)
starts_by_during......................proved - complete [shostak](0.04 s)
starts_by_contains....................proved - complete [shostak](0.04 s)
starts_by_overlaps....................proved - complete [shostak](0.04 s)
starts_by_overlapped_by...............proved - complete [shostak](0.05 s)
starts_by_meet........................proved - complete [shostak](0.03 s)
starts_by_meet_by.....................proved - complete [shostak](0.02 s)
starts_by_starts......................proved - complete [shostak](0.02 s)
starts_by_started_by..................proved - complete [shostak](0.02 s)
starts_by_finishes....................proved - complete [shostak](0.03 s)
starts_by_finished_by.................proved - complete [shostak](0.04 s)
started_by_before.....................proved - complete [shostak](0.04 s)
started_by_after......................proved - complete [shostak](0.03 s)
started_by_during.....................proved - complete [shostak](0.05 s)
started_by_contains...................proved - complete [shostak](0.03 s)
started_by_overlaps...................proved - complete [shostak](0.05 s)
--> --------------------
--> maximum size reached
--> --------------------
[ Verzeichnis aufwärts0.525unsichere Verbindung
]
|
|
|
|
|
|
