Why3 Proof Results for Project "szymanski_at_certif"

Theory "szymanski_at_certif.Szymanski_at_initialisation": fully verified in 0.31 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
initialisation		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.06	0.10	0.01	0.12	0.01	0.01

Theory "szymanski_at_certif.Szymanski_at_property": fully verified in 0.27 s

Obligations	Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
property	0.01	0.02	0.03	0.02	0.18	0.01	0.00

Theory "szymanski_at_certif.Szymanski_at_hint_1": fully verified in 0.45 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_1		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.04	0.08	0.19	0.10	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_2": fully verified in 0.90 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_2		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.04	0.09	0.14	0.58	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_3": fully verified in 0.02 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_3		---	---	---	---	---	---	---
inline_all
	1.	0.03	0.63	0.06	Timeout (5s)	Timeout (5s)	0.85	0.02

Theory "szymanski_at_certif.Szymanski_at_hint_4": fully verified in 0.85 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_4		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.03	0.09	0.13	0.54	0.03	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_5": fully verified in 0.71 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_5		---	---	---	---	---	---	---
inline_all
	1.	0.03	0.07	0.09	0.42	0.12	0.65	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_6": fully verified in 0.65 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_6		---	---	---	---	---	---	---
inline_all
	1.	0.03	0.05	0.09	0.33	0.11	0.03	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_7": fully verified in 0.99 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_7		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.04	0.09	0.14	0.67	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_8": fully verified in 0.92 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_8		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.09	0.10	0.57	0.15	0.67	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_9": fully verified in 0.61 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_9		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.06	0.09	0.30	0.10	0.03	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_10": fully verified in 0.39 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_10		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.04	0.08	0.16	0.07	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_11": fully verified in 0.40 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_11		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.04	0.08	0.17	0.07	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_12": fully verified in 0.38 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_12		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.04	0.07	0.14	0.09	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_13": fully verified in 0.79 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_13		---	---	---	---	---	---	---
inline_all
	1.	0.03	0.15	0.13	0.27	0.23	5.00	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_14": fully verified in 0.39 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_14		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.10	0.11	0.17	Timeout (5s)	5.00	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_15": fully verified in 0.45 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_15		---	---	---	---	---	---	---
inline_all
	1.	0.04	0.06	0.16	0.22	Timeout (5s)	5.01	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_16": fully verified in 0.43 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_16		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.03	0.07	0.19	0.10	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_17": fully verified in 0.35 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_17		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.03	0.06	0.13	0.09	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_18": fully verified in 0.44 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_18		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.05	0.08	0.16	0.09	0.03	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_19": fully verified in 0.41 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_19		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.05	0.09	0.14	0.08	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_20": fully verified in 0.38 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_20		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.04	0.09	0.14	0.07	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_21": fully verified in 0.41 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_21		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.06	0.11	0.12	0.07	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_22": fully verified in 0.38 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_22		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.05	0.10	0.12	0.07	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_23": fully verified in 0.65 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_23		---	---	---	---	---	---	---
inline_all
	1.	0.03	0.07	0.11	0.37	0.09	0.53	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_24": fully verified in 0.64 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_24		---	---	---	---	---	---	---
inline_all
	1.	0.04	0.06	0.10	0.37	0.10	0.54	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_25": fully verified in 0.91 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_25		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.03	0.09	0.13	0.61	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_26": fully verified in 0.95 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_26		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.03	0.10	0.15	0.61	0.03	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_27": fully verified in 0.88 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_27		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.03	0.11	0.18	0.51	0.03	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_28": fully verified in 0.86 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_28		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.03	0.12	0.13	0.53	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_29": fully verified in 0.69 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_29		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.03	0.13	0.13	0.36	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_30": fully verified in 0.45 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_30		---	---	---	---	---	---	---
inline_all
	1.	0.01	0.03	0.09	0.18	0.11	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_hint_31": fully verified in 0.46 s

Obligations		Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
hint_31		---	---	---	---	---	---	---
inline_all
	1.	0.02	0.03	0.10	0.19	0.09	0.02	0.01

Theory "szymanski_at_certif.Szymanski_at_preservation": fully verified in 0.60 s

Obligations	Alt-Ergo (0.99 nb1noE)	CVC3 (2.4.1)	CVC4 (1.4)	Eprover (1.8-001)	Spass (3.5)	Yices (1.0.40)	Z3 (4.3.2)
preservation	0.11	0.05	0.05	0.03	0.30	0.03	0.03