Why3 Proof Results for Project "scc"

Theory "scc.SCCTarjan72": fully verified in 2.23 s

Obligations						Alt-Ergo (2.2.0)	CVC3 (2.4.1)	CVC4 (1.5)	Coq (8.7.2)	Eprover (1.9)	Spass (3.5)	Z3 (4.4.0)	Z3 (4.6.3)
lmem_dec						0.00	---	---	---	---	---	---	---
inter_com						---	0.04	---	---	---	---	---	---
inter_not_add_l						0.01	---	---	---	---	---	---	---
inter_add_l						0.01	---	---	---	---	---	---	---
diff_add_l						0.01	---	---	---	---	---	---	---
diff_add_r						0.02	---	---	---	---	---	---	---
subset_add_r						0.01	---	---	---	---	---	---	---
union_add_l						0.01	---	---	---	---	---	---	---
union_add_r						0.01	---	---	---	---	---	---	---
union_com						0.01	---	---	---	---	---	---	---
union_var_l						0.01	---	---	---	---	---	---	---
union_var_r						0.01	---	---	---	---	---	---	---
elts_cons						0.03	---	---	---	---	---	---	---
elts_app						0.02	---	---	---	---	---	---	---
set_of_elt						---	---	---	---	---	---	---	---
split_goal_wp
	set_of_elt.1					0.02	---	---	---	---	---	---	---
	set_of_elt.2					---	---	---	---	---	2.44	---	---
elt_set_of						---	---	---	---	0.17	---	---	---
subset_set_of						0.04	---	---	---	---	---	---	---
list_simpl_r						---	---	---	---	---	---	---	---
induction_ty_lex
	list_simpl_r.1					---	---	---	---	---	---	---	---
	split_goal_wp
		list_simpl_r.1.1				0.01	---	---	---	---	---	---	---
		list_simpl_r.1.2				---	---	0.24	---	---	---	---	---
list_assoc_cons						---	---	0.06	---	---	---	---	---
rank_not_mem						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_not_mem.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_not_mem.1.1				0.01	---	---	---	---	---	---	---
		rank_not_mem.1.2				0.01	---	---	---	---	---	---	---
rank_range						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_range.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_range.1.1				0.01	---	---	---	---	---	---	---
		rank_range.1.2				0.01	---	---	---	---	---	---	---
		rank_range.1.3				0.01	---	---	---	---	---	---	---
		rank_range.1.4				0.01	---	---	---	---	---	---	---
rank_min						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_min.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_min.1.1				0.01	---	---	---	---	---	---	---
		rank_min.1.2				---	---	0.60	---	---	---	---	---
rank_app_l						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_app_l.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_app_l.1.1				0.01	---	---	---	---	---	---	---
		rank_app_l.1.2				0.10	---	---	---	---	---	---	---
rank_app_r						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_app_r.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_app_r.1.1				0.01	---	---	---	---	---	---	---
		rank_app_r.1.2				0.04	---	---	---	---	---	---	---
simplelist_tl						---	---	0.10	---	---	---	---	---
simplelist_split						---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_split.1					---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_split.1.1				---	---	0.09	---	---	---	---	---
		simplelist_split.1.2				---	---	0.11	---	---	---	---	---
		simplelist_split.1.3				---	---	1.46	---	---	---	---	---
		simplelist_split.1.4				---	---	1.13	---	---	---	---	---
simplelist_app_disjoint						---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_app_disjoint.1					---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_app_disjoint.1.1				---	---	---	---	0.09	---	---	---
		simplelist_app_disjoint.1.2				---	---	1.38	---	---	---	---	---
simplelist_length						---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_length.1					---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_length.1.1				0.01	---	---	---	---	---	---	---
		simplelist_length.1.2				0.01	---	---	---	---	---	---	---
simplelist_hd_max_rank						0.02	---	---	---	---	---	---	---
rank_before_suffix						0.18	---	---	---	---	---	---	---
reachable_trans						---	0.19	---	---	---	---	---	---
xset_path_xedge						---	---	---	---	---	---	---	---
induction_pr
	xset_path_xedge.1					0.01	---	---	---	---	---	---	---
	xset_path_xedge.2					---	---	---	---	0.04	---	---	---
same_scc_refl						---	---	---	---	0.07	---	---	---
same_scc_sym						0.01	---	---	---	---	---	---	---
same_scc_trans						0.02	---	---	---	---	---	---	---
subscc_add						0.04	---	---	---	---	---	---	---
scc_max						---	---	0.23	---	---	---	---	---
subscc_after_last_gray						---	---	---	---	---	---	---	---
split_goal_wp
	subscc_after_last_gray.1					---	---	0.48	---	---	---	---	---
	subscc_after_last_gray.2					2.01	---	---	---	---	---	---	---
	subscc_after_last_gray.3					---	---	1.63	---	---	---	---	---
	subscc_after_last_gray.4					---	---	---	---	---	---	---	---
	inline_goal
		subscc_after_last_gray.4.1				---	---	---	---	1.20	---	---	---
wf_color_postcond_split						---	---	0.31	---	---	---	---	---
wf_color_sccs						---	---	0.39	---	---	---	---	---
wf_color_3_cases						---	---	0.16	---	---	---	---	---
42. VC for split						---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition					0.01	---	---	---	---	---	---	---
	2. postcondition					0.01	---	---	---	---	---	---	---
	3. postcondition					0.01	---	---	---	---	---	---	---
	4. postcondition					---	0.20	---	---	---	---	---	---
	5. variant decrease					0.03	---	---	---	---	---	---	---
	6. postcondition					0.01	---	---	---	---	---	---	---
	7. postcondition					0.05	---	---	---	---	---	---	---
43. VC for add_stack_incr						0.01	---	---	---	---	---	---	---
44. VC for add_blacks						0.01	---	---	---	---	---	---	---
45. VC for set_infty						0.02	---	---	---	---	---	---	---
46. VC for dfs1						---	---	---	---	---	---	---	---
split_goal_wp
	1. variant decrease					---	---	---	---	---	---	---	---
	introduce_premises
		1. variant decrease				---	---	---	---	---	---	---	---
		inline_goal
			1. variant decrease			0.08	---	---	---	---	---	---	---
	2. precondition					0.03	---	---	---	---	---	---	---
	3. precondition					---	---	---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	---	0.90	---	---	---
	4. precondition					---	---	---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. precondition			0.18	---	---	---	---	---	---	---
			2. precondition			---	---	---	---	---	---	---	---
			inline_goal
				1. precondition		---	---	---	---	---	---	---	---
				split_goal_wp
					1. precondition	0.11	---	---	---	---	---	---	---
					2. precondition	0.05	---	---	---	---	---	---	---
					3. precondition	0.07	---	---	---	---	---	---	---
					4. precondition	0.06	---	---	---	---	---	---	---
					5. precondition	0.11	---	---	---	---	---	---	---
					6. precondition	0.06	---	---	---	---	---	---	---
					7. precondition	---	---	21.89	---	---	---	---	---
					8. precondition	---	---	20.68	---	---	---	---	---
			3. precondition			0.06	---	---	---	---	---	---	---
			4. precondition			0.19	---	---	---	---	---	---	---
			5. precondition			3.27	---	---	---	---	---	---	---
			6. precondition			1.43	---	---	---	---	---	---	---
	5. precondition					---	---	---	---	---	---	---	---
	split_goal_wp
		1. precondition				0.01	---	---	---	---	---	---	---
		2. precondition				0.01	---	---	---	---	---	---	---
		3. precondition				0.01	---	---	---	---	---	---	---
	6. assertion					---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1				0.66	---	---	---	---	---	---	---
		2. VC for dfs1				0.66	---	---	---	---	---	---	---
		3. VC for dfs1				1.59	---	---	---	---	---	---	---
	7. assertion					---	---	9.98	---	---	---	---	---
	8. assertion					---	---	---	1.13	---	---	---	---
	9. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. postcondition			---	---	18.57	---	---	---	---	---
			2. postcondition			---	---	---	---	---	---	---	---
			inline_goal
				1. postcondition		---	---	---	---	---	---	---	---
				split_goal_wp
					1. postcondition	---	---	0.31	---	---	---	---	---
					2. postcondition	---	---	19.12	---	---	---	---	---
					3. postcondition	---	---	0.25	---	---	---	---	---
					4. postcondition	---	---	0.25	---	---	---	---	---
					5. postcondition	---	---	1.33	---	---	---	---	---
					6. postcondition	---	---	1.09	---	---	---	---	---
					7. postcondition	0.08	---	---	---	4.73	---	---	---
					8. postcondition	0.08	---	---	---	4.62	---	---	---
			3. postcondition			---	---	1.67	---	---	---	---	---
			4. postcondition			0.02	---	---	---	---	---	---	---
			5. postcondition			---	---	0.21	---	---	---	---	---
			6. postcondition			---	---	22.75	---	---	---	---	---
	10. postcondition					---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition				0.28	---	---	---	---	---	---	---
	2. postcondition				0.03	---	---	---	---	---	---	---
	3. postcondition				---	---	---	---	---	---	---	4.56
11. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	0.23	---	---	---	---	---
12. postcondition					10.04	---	---	---	---	---	---	---
13. postcondition					---	---	1.69	---	---	---	---	---
14. postcondition					0.01	---	---	---	---	---	---	---
15. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	---	---	---	1.11	---	---	---
		2. VC for dfs1			0.13	---	---	---	---	---	---	---
		3. VC for dfs1			0.02	---	---	---	---	---	---	---
		4. VC for dfs1			---	---	---	---	0.33	---	---	---
		5. VC for dfs1			0.86	---	---	---	---	---	---	---
16. assertion					---	---	---	1.12	---	---	---	---
17. assertion					---	---	---	---	---	---	---	---
inline_goal
	1. assertion				---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	---	0.35	---	---	---	---	---
		2. VC for dfs1			0.03	---	---	---	---	---	---	---
		3. VC for dfs1			---	---	---	---	5.38	---	---	---
18. assertion					---	---	---	---	---	---	---	---
split_goal_wp
	1. VC for dfs1				---	---	---	---	---	---	---	---
	inline_goal
		1. VC for dfs1			---	---	---	---	---	---	---	---
		split_goal_wp
			1. VC for dfs1		---	---	0.73	---	---	---	---	---
			2. VC for dfs1		---	---	0.13	---	---	---	---	---
	2. VC for dfs1				0.02	---	---	---	---	---	---	---
19. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	---	---	---	---	---	---	---
		inline_goal
			1. VC for dfs1		---	---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs1	0.84	---	---	---	---	---	---	---
				2. VC for dfs1	6.54	---	---	---	---	---	---	---
				3. VC for dfs1	---	---	151.47	---	---	---	---	---
				4. VC for dfs1	0.93	---	---	---	---	---	---	---
		2. VC for dfs1			---	---	---	---	---	---	---	---
		inline_goal
			1. VC for dfs1		---	---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs1	0.13	---	0.42	---	7.21	---	0.12	---
				2. VC for dfs1	---	---	---	---	52.39	---	---	---
				3. VC for dfs1	0.38	---	0.41	---	---	---	0.56	---
				4. VC for dfs1	---	---	---	---	---	---	0.13	---
				5. VC for dfs1	---	---	2.57	---	---	---	---	---
				6. VC for dfs1	---	---	---	---	---	---	8.39	---
				7. VC for dfs1	---	---	---	---	14.59	---	---	---
				8. VC for dfs1	---	---	---	---	16.99	---	---	---
		3. VC for dfs1			---	---	---	---	---	---	---	---
		inline_goal
			1. VC for dfs1		---	---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs1	---	---	1.49	---	---	---	---	---
		4. VC for dfs1			0.02	---	---	---	---	---	---	---
		5. VC for dfs1			0.02	---	---	---	---	---	---	---
		6. VC for dfs1			---	---	---	---	---	---	---	---
		inline_goal
			1. VC for dfs1		---	---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs1	---	---	2.65	---	---	---	---	---
20. postcondition					---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition				0.41	---	---	---	---	---	---	---
	2. postcondition				0.02	---	---	---	---	---	---	---
	3. postcondition				---	---	---	---	8.28	---	---	---
21. postcondition					0.18	---	---	---	---	---	---	---
22. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	0.07	---	---	---	---	---
23. postcondition					0.03	---	---	---	---	---	---	---
24. postcondition					0.02	---	---	---	---	---	---	---
25. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	---	---	---	0.10	---	---	---
		2. VC for dfs1			0.02	---	---	---	---	---	---	---
		3. VC for dfs1			0.02	---	---	---	---	---	---	---
		4. VC for dfs1			---	---	---	---	0.33	---	---	---
		5. VC for dfs1			0.02	---	---	---	---	---	---	---
47. VC for dfs						---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition					0.01	---	---	---	---	---	---	---
	2. postcondition					0.01	---	---	---	---	---	---	---
	3. postcondition					0.01	---	---	---	---	---	---	---
	4. postcondition					0.01	---	---	---	---	---	---	---
	5. postcondition					0.01	---	---	---	---	---	---	---
	6. postcondition					0.01	---	---	---	---	---	---	---
	7. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. VC for dfs			---	---	0.18	---	---	---	---	---
			2. VC for dfs			0.01	---	---	---	---	---	---	---
			3. VC for dfs			0.01	---	---	---	---	---	---	---
			4. VC for dfs			0.01	---	---	---	---	---	---	---
			5. VC for dfs			0.01	---	---	---	---	---	---	---
	8. assertion					---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs				0.06	---	---	---	---	---	---	---
		2. VC for dfs				---	---	---	---	---	---	0.19	---
	9. variant decrease					0.02	---	---	---	---	---	---	---
	10. precondition					0.01	---	---	---	---	---	---	---
	11. precondition					0.01	---	---	---	---	---	---	---
	12. precondition					0.01	---	---	---	---	---	---	---
	13. precondition					0.01	---	---	---	---	---	---	---
	14. postcondition					0.01	---	---	---	---	---	---	---
	15. postcondition					0.01	---	---	---	---	---	---	---
	16. postcondition					---	---	1.08	---	---	---	---	---
	17. postcondition					---	19.67	---	---	---	---	---	---
	18. postcondition					0.01	---	---	---	---	---	---	---
	19. postcondition					0.31	---	---	---	---	---	---	---
	20. postcondition					0.01	---	---	---	---	---	---	---
	21. variant decrease					0.01	---	---	---	---	---	---	---
	22. precondition					0.01	---	---	---	---	---	---	---
	23. precondition					0.01	---	---	---	---	---	---	---
	24. precondition					0.03	---	---	---	---	---	---	---
	25. precondition					0.01	---	---	---	---	---	---	---
	26. precondition					0.01	---	---	---	---	---	---	---
	27. variant decrease					---	---	---	---	---	---	---	---
	split_all_full
		1. variant decrease				0.02	---	---	---	---	---	---	---
		2. variant decrease				0.02	---	---	---	---	---	---	---
		3. variant decrease				0.02	---	---	---	---	---	---	---
		4. variant decrease				0.02	---	---	---	---	---	---	---
		5. variant decrease				0.02	---	---	---	---	---	---	---
		6. variant decrease				---	---	---	---	---	---	---	---
		inline_all
			1. variant decrease			---	---	---	---	---	---	---	0.36
		7. variant decrease				0.02	---	---	---	---	---	---	---
		8. variant decrease				0.02	---	---	---	---	---	---	---
		9. variant decrease				0.02	---	---	---	---	---	---	---
		10. variant decrease				0.02	---	---	---	---	---	---	---
	28. precondition					0.02	---	---	---	---	---	---	---
	29. precondition					0.04	---	---	---	---	---	---	---
	30. precondition					0.01	---	---	---	---	---	---	---
	31. precondition					0.02	---	---	---	---	---	---	---
	32. postcondition					0.02	---	---	---	---	---	---	---
	33. postcondition					0.02	---	---	---	---	---	---	---
	34. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	---	2.46	---	---	---	---	---
	35. postcondition					0.39	---	---	---	---	---	---	---
	36. postcondition					2.40	---	---	---	---	---	---	---
	37. postcondition					0.03	---	---	---	---	---	---	---
	38. postcondition					---	---	---	---	---	---	---	---
introduce_premises
	1. postcondition				---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition			---	---	---	---	---	---	---	---
		split_goal_wp
			1. VC for dfs		11.80	---	---	---	---	---	---	---
			2. VC for dfs		0.03	---	---	---	---	---	---	---
			3. VC for dfs		0.03	---	---	---	---	---	---	---
			4. VC for dfs		0.10	---	---	---	---	---	---	---
			5. VC for dfs		0.03	---	---	---	---	---	---	---
48. VC for tarjan						---	---	---	---	---	---	---	---
split_goal_wp
	1. precondition					0.01	---	---	---	---	---	---	---
	2. precondition					0.01	---	---	---	---	---	---	---
	3. precondition					---	---	---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. precondition			0.05	---	---	---	---	---	---	---
			2. precondition			0.04	---	---	---	---	---	---	---
			3. precondition			0.01	---	---	---	---	---	---	---
			4. precondition			0.01	---	---	---	---	---	---	---
			5. precondition			0.01	---	---	---	---	---	---	---
			6. precondition			0.01	---	---	---	---	---	---	---
	4. precondition					0.01	---	---	---	---	---	---	---
	5. assertion					0.02	---	---	---	---	---	---	---
	6. postcondition					---	---	---	---	---	---	---	---
	split_goal_wp
		1. postcondition				0.23	---	---	---	---	---	---	---
		2. postcondition				0.02	---	---	---	---	---	---	---
		3. postcondition				0.02	---	---	---	---	---	---	---