Why3 Proof Results for Project "szymanski_na_certif"
Theory "szymanski_na_certif.Szymanski_na_initialisation": fully verified in 5.37 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.01 | Timeout (5s) | 0.23 | 0.03 | 0.27 | 3.41 | 4.84 |
Theory "szymanski_na_certif.Szymanski_na_property": fully verified in 0.77 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.02 | 0.02 | 0.07 | 0.03 | 0.60 | 0.02 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_1": fully verified in 4.77 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.04 | 0.23 | 0.25 | 1.46 | 2.70 | 0.07 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_2": fully verified in 1.49 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 | 4.11 | 0.04 | 1.46 | Timeout (5s) | 5.00 | 0.03 |
Theory "szymanski_na_certif.Szymanski_na_hint_3": fully verified in 2.09 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.05 | 0.27 | 0.33 | 1.32 | Timeout (5s) | 0.10 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_4": fully verified in 2.25 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.04 | 0.22 | 0.53 | 1.35 | Timeout (5s) | 0.09 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_5": fully verified in 3.54 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.18 | 0.43 | 1.12 | 1.68 | 0.08 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_6": fully verified in 1.19 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.04 | 0.13 | 0.31 | 0.62 | Timeout (5s) | 0.07 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_7": fully verified in 3.93 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.05 | 0.24 | 0.28 | 1.04 | 2.26 | 0.05 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_8": fully verified in 3.76 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.05 | 0.12 | 0.42 | 3.07 | Timeout (5s) | 0.09 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_9": fully verified in 4.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) |
hint_9 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.05 | 0.13 | 0.50 | 3.84 | Timeout (5s) | 0.06 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_10": 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_10 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.02 | 1.27 | Timeout (5s) | Timeout (5s) | Timeout (5s) | 5.00 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_11": fully verified in 1.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_11 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.03 | 3.87 | 0.06 | 1.86 | Timeout (5s) | 5.00 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_12": fully verified in 1.94 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.04 | 0.23 | 0.41 | 1.16 | Timeout (5s) | 0.09 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_13": fully verified in 1.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_13 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.04 | 0.23 | 0.33 | 1.06 | Timeout (5s) | 0.04 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_14": fully verified in 2.12 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.04 | 1.85 | 0.95 | 1.15 | Timeout (5s) | 5.00 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_15": fully verified in 1.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_15 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.02 | 1.70 | 0.04 | 1.67 | Timeout (5s) | 5.00 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_16": fully verified in 3.08 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.06 | 1.44 | 3.06 | Timeout (5s) | Timeout (5s) | 5.01 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_17": fully verified in 3.13 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.07 | 0.19 | 0.52 | 2.32 | Timeout (5s) | 5.00 | 0.03 |
Theory "szymanski_na_certif.Szymanski_na_hint_18": fully verified in 3.78 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.05 | 0.15 | 0.60 | 2.96 | Timeout (5s) | 4.99 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_19": fully verified in 4.53 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.06 | 0.17 | 0.65 | 3.63 | Timeout (5s) | 5.00 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_20": 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_20 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.06 | 0.13 | 0.42 | Timeout (5s) | Timeout (5s) | 0.28 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_21": fully verified in 1.77 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.04 | 0.18 | 0.31 | 1.16 | Timeout (5s) | 0.06 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_22": fully verified in 2.11 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.03 | 0.20 | 0.34 | 1.47 | Timeout (5s) | 0.05 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_23": fully verified in 1.83 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.20 | 0.41 | 1.12 | Timeout (5s) | 0.06 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_24": fully verified in 0.77 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.06 | 0.16 | 0.53 | Timeout (5s) | Timeout (5s) | 5.00 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_25": fully verified in 1.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_25 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.06 | 0.13 | 0.38 | 0.93 | Timeout (5s) | 5.00 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_26": fully verified in 1.57 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.05 | 0.11 | 0.40 | 1.05 | Timeout (5s) | 5.00 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_27": 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_27 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.05 | 0.18 | 0.51 | Timeout (5s) | Timeout (5s) | 0.09 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_28": fully verified in 0.89 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.06 | 0.14 | 0.74 | Timeout (5s) | Timeout (5s) | 5.00 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_29": fully verified in 4.00 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.04 | 0.09 | 0.51 | 3.26 | Timeout (5s) | 0.09 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_30": fully verified in 0.77 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.05 | 0.09 | 0.51 | Timeout (5s) | Timeout (5s) | 0.10 | 0.02 |
Theory "szymanski_na_certif.Szymanski_na_hint_31": fully verified in 4.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_31 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.03 | 0.19 | 0.42 | 1.08 | 2.85 | 0.06 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_32": fully verified in 5.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_32 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.04 | 0.22 | 0.45 | 1.48 | 2.75 | 0.07 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_33": fully verified in 3.63 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_33 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.04 | 0.22 | 0.48 | 1.16 | 1.65 | 0.07 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_34": fully verified in 3.96 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_34 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.04 | 0.20 | 0.42 | 1.50 | 1.73 | 0.06 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_35": fully verified in 4.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_35 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.04 | 0.20 | 0.38 | 1.27 | 2.51 | 0.05 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_36": fully verified in 2.14 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_36 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.04 | 0.22 | 0.44 | 1.38 | Timeout (5s) | 0.05 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_37": fully verified in 2.03 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_37 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.04 | 0.22 | 0.46 | 1.23 | Timeout (5s) | 0.07 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_hint_38": 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_38 | --- | --- | --- | --- | --- | --- | --- |
| inline_all | | | | | | | |
| 1. | 0.06 | 0.19 | 0.45 | Timeout (5s) | Timeout (5s) | 0.08 | 0.01 |
Theory "szymanski_na_certif.Szymanski_na_preservation": fully verified in 2.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) |
preservation | 0.19 | 0.06 | 0.05 | 0.06 | 1.63 | 0.03 | 0.00 |