Why3 Proof Results for Project "blocking_semantics5"

Theory "Syntax": fully verified

ObligationsAlt-Ergo (0.95.1)
mident_decide0.01
ident_decide0.00
decide_is_skip0.01

Theory "SemOp": fully verified

ObligationsAlt-Ergo (0.95.1)CVC3 (2.2)CVC3 (2.4.1)Coq (8.4pl2)Z3 (3.2)Z3 (4.3.1)
get_stack_eq0.010.030.02---0.040.03
get_stack_neq0.020.030.02---0.200.20
steps_non_neg---------1.02------

Theory "TestSemantics": fully verified

ObligationsAlt-Ergo (0.95.1)CVC3 (2.4.1)CVC4 (1.2)Coq (8.4pl2)
Test130.02---0.03---
Test420.03---------
Test00.05---------
Test55------0.04---
Ass420.050.05------
If42---------1.85

Theory "TypingAndSemantics": fully verified

ObligationsAlt-Ergo (0.95.1)CVC3 (2.2)CVC3 (2.4.1)Coq (8.4pl2)Z3 (3.2)Z3 (4.3.1)
type_inversion0.020.040.931.65Timeout (5s)Timeout (5s)
induction_ty_lex
  1.0.080.040.10---0.070.07
eval_type_term------------------
induction_ty_lex
  1.------------------
split_goal_wp
  1.0.070.040.06---Timeout (5s)Timeout (5s)
2.0.060.040.04---Timeout (5s)Timeout (5s)
3.0.080.040.05---Timeout (5s)Timeout (5s)
4.Timeout (5s)---Timeout (5s)2.52Timeout (5s)Timeout (5s)
type_preservation---------2.53------

Theory "FreshVariables": fully verified

ObligationsAlt-Ergo (0.95.1)CVC3 (2.2)CVC3 (2.4.1)Coq (8.4pl2)Z3 (3.2)Z3 (4.3.1)
Cons_append0.03---------------
Append_nil_l0.03---------------
eval_msubst_term------------------
induction_ty_lex
  1.------------------
split_goal_wp
  1.0.040.040.04---Timeout (5s)Timeout (5s)
2.0.040.040.04---Timeout (5s)Timeout (5s)
3.0.050.040.04---Timeout (5s)Timeout (5s)
4.0.120.050.06---Timeout (5s)Timeout (5s)
eval_msubst------------------
induction_ty_lex
  1.------------------
split_goal_wp
  1.0.050.060.10---Timeout (30s)Out Of Memory (1000M)
2.0.040.060.08---Timeout (30s)Out Of Memory (1000M)
3.0.040.08Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
4.0.060.10Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
5.0.040.080.55---Timeout (30s)Out Of Memory (1000M)
6.0.040.08Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
7.0.070.090.30---Timeout (30s)Out Of Memory (1000M)
8.0.030.09Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
9.1.520.705.751.36Timeout (30s)Out Of Memory (1000M)
10.0.171.10Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
11.Out Of Memory (1000M)Timeout (30s)Timeout (30s)2.57Out Of Memory (1000M)Out Of Memory (1000M)
12.0.77Timeout (30s)Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
eval_swap_term------------------
induction_ty_lex
  1.------------------
split_goal_wp
  1.0.040.040.08---Timeout (30s)Timeout (30s)
2.Timeout (30s)Timeout (30s)Timeout (30s)2.00Timeout (30s)Timeout (30s)
3.0.050.060.05---Timeout (30s)Timeout (30s)
4.0.030.050.25---Timeout (30s)Timeout (30s)
eval_swap_gen------------------
induction_ty_lex
  1.------------------
split_goal_wp
  1.0.040.050.24---Timeout (30s)Timeout (30s)
2.0.150.050.23---Timeout (30s)Timeout (30s)
3.0.100.260.43---Timeout (30s)Timeout (30s)
4.0.110.270.46---Timeout (30s)Timeout (30s)
5.0.050.220.37---Timeout (30s)Timeout (30s)
6.0.160.210.34---Timeout (30s)Timeout (30s)
7.0.040.250.41---Timeout (30s)Timeout (30s)
8.0.040.240.42---Timeout (30s)Timeout (30s)
9.0.14Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
10.0.15Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
11.9.52Timeout (30s)Timeout (30s)2.00Timeout (30s)Timeout (30s)
12.8.60Timeout (30s)Timeout (30s)2.00Timeout (30s)Timeout (30s)
eval_swapTimeout (5s)Timeout (5s)Timeout (5s)1.07Timeout (5s)Timeout (5s)
eval_term_change_free------------------
induction_ty_lex
  1.------------------
split_goal_wp
  1.0.040.040.05---Timeout (20s)Out Of Memory (1000M)
2.0.040.110.06---Timeout (20s)Out Of Memory (1000M)
3.0.040.030.04---Timeout (30s)Out Of Memory (1000M)
4.0.070.030.05---Timeout (30s)Out Of Memory (1000M)
eval_change_free------------------
induction_ty_lex
  1.------------------
split_goal_wp
  1.0.050.050.06---Timeout (30s)Out Of Memory (1000M)
2.0.060.040.15---Timeout (30s)Out Of Memory (1000M)
3.0.080.050.07---Timeout (30s)Out Of Memory (1000M)
4.0.120.060.07---Timeout (30s)Out Of Memory (1000M)
5.0.050.050.06---Timeout (20s)Out Of Memory (1000M)
6.0.060.050.06---Timeout (30s)Out Of Memory (1000M)
7.0.070.060.07---Timeout (30s)Out Of Memory (1000M)
8.0.040.060.07---Timeout (30s)Out Of Memory (1000M)
9.0.58---0.291.11Timeout (20s)Out Of Memory (1000M)
10.0.070.390.501.12Timeout (20s)Out Of Memory (1000M)
11.Timeout (30s)Timeout (30s)Timeout (30s)2.00Timeout (30s)Out Of Memory (1000M)
12.0.18Timeout (30s)Timeout (30s)1.53Timeout (30s)Out Of Memory (1000M)

Theory "HoareLogic": fully verified

ObligationsCVC3 (2.2)CVC3 (2.4.1)Coq (8.4pl2)Z3 (3.2)Z3 (4.3.1)
many_steps_seq------1.73------
consequence_rule0.080.15---------
skip_rule------1.14------
assign_rule------1.96------
seq_rule---------0.090.06
if_rule------1.71------
assert_rule------1.23------
assert_rule_ext------1.47------
while_rule------1.39------

Theory "WP": fully verified

ObligationsAlt-Ergo (0.95.1)CVC3 (2.2)CVC3 (2.4.1)CVC4 (1.2)Coq (8.4pl2)Eprover (1.6)Vampire (0.6)Z3 (3.2)Z3 (4.3.1)
monotonicity---------------------------
induction_ty_lex
  1.---------------------------
split_goal_wp
  1.0.040.060.08------------0.090.10
2.Timeout (5s)Timeout (5s)Timeout (5s)---1.67------Timeout (5s)Timeout (5s)
3.0.060.110.14------------Timeout (5s)Timeout (5s)
4.------0.24Timeout (5s)1.64---------Timeout (5s)
5.Timeout (5s)0.070.09------------Timeout (5s)Timeout (5s)
6.Timeout (5s)Timeout (5s)Timeout (5s)---1.16------Timeout (5s)Timeout (5s)
distrib_conj---------------------------
induction_ty_lex
  1.---------------------------
split_goal_wp
  1.0.060.060.07------------Timeout (5s)Timeout (5s)
2.6.07Timeout (5s)Timeout (5s)---2.03------Timeout (5s)Timeout (5s)
3.Timeout (5s)Timeout (5s)Timeout (5s)---1.62------Timeout (5s)Timeout (5s)
4.0.960.58Timeout (5s)0.08---------Timeout (5s)Timeout (5s)
5.0.400.270.27------------Timeout (5s)Timeout (5s)
6.Timeout (5s)Timeout (5s)Timeout (5s)---1.31------Timeout (5s)Timeout (5s)
wp_preserved_by_reduction------------4.74------------
progress---------------------------
induction_ty_lex
  1.---------------------------
split_goal_wp
  1.0.040.050.06------------0.000.00
2.Timeout (5s)Timeout (5s)Timeout (5s)---1.17------Timeout (5s)Timeout (5s)
3.Timeout (5s)Timeout (5s)Timeout (5s)---1.56------Timeout (5s)Timeout (5s)
4.Timeout (5s)---Timeout (5s)Timeout (5s)1.45------Timeout (5s)Timeout (5s)
5.---0.31------1.150.200.34------
6.Timeout (5s)Timeout (5s)Timeout (5s)---1.19------Timeout (5s)Timeout (5s)
wp_soundnessTimeout (5s)Timeout (5s)Timeout (5s)---1.27------Timeout (5s)Timeout (5s)