Why3 Proof Results for Project "dfs77"

Theory "dfs77.DFSWhitePathGrayCompteness": fully verified in 0.21 s

ObligationsAlt-Ergo (2.0.0)CVC4 (1.5)Coq (8.7.1)Eprover (1.9)Spass (3.5)Z3 (4.4.0)
whiteaccess_var0.01---------------
whiteaccess_minus0.01---------------
nbtw_path------------------
induction_pr
  nbtw_path.1---0.05------------
nbtw_path.2Timeout (5s)0.05------------
nbtw_whiteaccess0.01---------------
diff_emptyTimeout (15s)0.06------------
whiteaccess_roots_result0.12---------------
7. VC for dfs------------------
split_goal_wp
  1. postcondition0.01---------------
2. postcondition0.01---------------
3. postcondition0.00---------------
4. postcondition0.10---------------
5. variant decrease0.01---------------
6. precondition0.01---------------
7. precondition0.01---------------
8. precondition0.01---------------
9. precondition0.01---------------
10. postcondition0.01---------------
11. postcondition0.01---------------
12. postcondition0.01---------------
13. postcondition1.07---------------
14. variant decrease0.01---------------
15. precondition0.01---------------
16. precondition0.01---------------
17. precondition0.01---------------
18. precondition0.03---------------
19. assertion0.47---------------
20. variant decrease0.02---------------
21. precondition0.02---------------
22. precondition0.02---------------
23. precondition0.01---------------
24. precondition0.17---------------
25. assertion3.46---------------
26. postcondition0.01---------------
27. postcondition0.01---------------
28. postcondition0.01---------------
29. postcondition------------------
split_goal_wp
  1. VC for dfs---0.15------------
2. VC for dfs7.666.15------------
3. VC for dfsTimeout (5s) (obsolete)0.09Not yet run (obsolete)Timeout (5s) (obsolete)Timeout (15s) (obsolete)Timeout (15s) (obsolete)