Why3 Proof Results for Project "dfs4"

Theory "dfs4.DfsWhitePathThm": fully verified in 4.56 s

ObligationsAlt-Ergo (2.0.0)CVC4 (1.5)Coq (8.7.1)Eprover (1.9)
whiteaccess_var0.01---------
whiteaccess_covar10.01---------
wpath_covar2------------
induction_pr
  wpath_covar2.10.01---------
wpath_covar2.2---0.06------
whiteaccess_covar2---0.06------
wpath_trans------------
induction_pr
  wpath_trans.10.01---------
wpath_trans.2---0.05------
whiteaccess_trans---0.14------
whiteaccess_cons---3.790.55---
nbtw_path------------
induction_pr
  nbtw_path.10.010.03------
nbtw_path.2---0.05---0.12
9. VC for dfs------------
split_goal_wp
  1. postcondition0.01---------
2. postcondition0.01---------
3. postcondition0.01---------
4. postcondition0.02---------
5. variant decrease0.01---------
6. precondition0.01---------
7. precondition0.01---------
8. postcondition0.01---------
9. postcondition0.01---------
10. postcondition0.01---------
11. postcondition0.20---------
12. variant decrease0.01---------
13. precondition0.01---------
14. precondition0.01---------
15. assertion------------
split_goal_wp
  1. VC for dfs0.01---------
2. VC for dfs0.02---------
3. VC for dfs---------0.10
4. VC for dfs0.01---------
16. assertion0.01---------
17. assertion------------
split_goal_wp
  1. VC for dfs---0.11------
2. VC for dfs---0.17------
18. variant decrease0.03---------
19. precondition0.01---------
20. precondition0.01---------
21. assertion1.24---------
22. assertion------------
split_goal_wp
  1. VC for dfs---0.10------
2. VC for dfs---------0.08
23. postcondition0.01---------
24. postcondition0.01---------
25. postcondition0.01---------
26. postcondition------------
split_goal_wp
  1. VC for dfs0.79---------
2. VC for dfs---0.58------
3. VC for dfs2.77---------