Why3 Proof Results for Project "german.ctc_certif"
Theory "german.ctc_certif.German_ctc_initialisation": fully verified in 4.30 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
initialisation | 27.34 | 1.77 | 0.16 | 0.04 | 2.17 | 0.14 | 0.02 |
Theory "german.ctc_certif.German_ctc_property": fully verified in 4.53 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
property | 0.92 | 0.07 | 0.12 | 0.10 | 3.27 | 0.04 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_1": fully verified in 1.88 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_1 | 0.80 | 0.31 | 0.73 | Timeout (5s) | Timeout (5s) | 0.03 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_2": fully verified in 1.92 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_2 | 0.68 | 0.34 | 0.81 | Timeout (5s) | Timeout (5s) | 0.08 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_3": fully verified in 1.73 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_3 | 0.69 | 0.32 | 0.62 | Timeout (5s) | Timeout (5s) | 0.09 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_4": fully verified in 1.72 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_4 | 0.66 | 0.35 | 0.61 | Timeout (5s) | Timeout (5s) | 0.08 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_5": fully verified in 1.90 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_5 | 0.89 | 0.35 | 0.62 | Timeout (5s) | Timeout (5s) | 0.03 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_6": fully verified in 1.83 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_6 | 0.92 | 0.36 | 0.54 | Timeout (5s) | Timeout (5s) | 3.66 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_7": fully verified in 1.74 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_7 | 0.84 | 0.34 | 0.48 | Timeout (5s) | Timeout (5s) | 0.06 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_8": fully verified in 1.76 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_8 | 0.87 | 0.30 | 0.53 | Timeout (5s) | Timeout (5s) | 0.05 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_9": fully verified in 4.75 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_9 | 0.57 | 0.28 | 0.35 | 0.62 | 2.83 | 0.09 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_10": fully verified in 1.51 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_10 | 0.60 | 0.32 | 0.49 | Timeout (5s) | Timeout (5s) | 0.09 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_11": fully verified in 2.74 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_11 | 0.61 | 0.35 | 0.59 | Timeout (5s) | Timeout (5s) | 1.18 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_12": fully verified in 3.20 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_12 | 0.60 | 0.30 | 0.85 | Timeout (5s) | Timeout (5s) | 1.44 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_13": fully verified in 1.51 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_13 | 0.65 | 0.31 | 0.49 | Timeout (5s) | Timeout (5s) | 0.05 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_14": fully verified in 1.58 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_14 | 0.60 | 0.27 | 0.64 | Timeout (5s) | Timeout (5s) | 0.05 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_15": fully verified in 1.60 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_15 | 0.67 | 0.22 | 0.67 | Timeout (5s) | Timeout (5s) | 0.03 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_16": fully verified in 1.18 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_16 | 0.34 | 0.11 | 0.20 | 0.49 | Timeout (5s) | 0.03 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_17": fully verified in 1.22 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_17 | 0.31 | 0.09 | 0.23 | 0.53 | Timeout (5s) | 0.05 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_18": fully verified in 1.20 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_18 | 0.16 | 0.23 | 0.18 | 0.57 | Timeout (5s) | 0.05 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_19": fully verified in 1.20 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_19 | 0.09 | 0.36 | 0.22 | 0.55 | Timeout (5s) | 0.05 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_20": fully verified in 1.41 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_20 | 0.46 | 0.30 | 0.62 | Timeout (5s) | Timeout (5s) | 0.02 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_21": fully verified in 1.46 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_21 | 0.50 | 0.30 | 0.60 | Timeout (5s) | Timeout (5s) | 0.05 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_22": fully verified in 1.57 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_22 | 0.58 | 0.32 | 0.61 | Timeout (5s) | Timeout (5s) | 0.05 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_23": fully verified in 1.76 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_23 | 0.33 | 0.26 | 0.39 | 0.75 | Timeout (5s) | 0.02 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_24": fully verified in 1.72 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_24 | 0.72 | 0.31 | 0.65 | Timeout (5s) | Timeout (5s) | 0.03 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_25": fully verified in 2.19 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_25 | 0.08 | 0.12 | 0.08 | 0.81 | 1.07 | 0.02 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_26": fully verified in 2.70 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_26 | 0.67 | 0.32 | 1.63 | Timeout (5s) | Timeout (5s) | 0.07 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_27": fully verified in 1.86 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_27 | 0.53 | 0.31 | 0.37 | 0.52 | Timeout (5s) | 0.11 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_28": fully verified in 2.16 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_28 | 0.76 | 0.46 | 0.86 | Timeout (5s) | Timeout (5s) | 0.07 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_29": fully verified in 1.99 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_29 | 0.73 | 0.46 | 0.77 | Timeout (5s) | Timeout (5s) | 0.02 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_30": fully verified in 1.76 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_30 | 0.33 | 0.30 | 0.35 | 0.75 | Timeout (5s) | 0.02 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_31": fully verified in 1.24 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_31 | 0.55 | 0.25 | 0.42 | Timeout (30s) | Timeout (30s) | 5.00 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_32": fully verified in 1.22 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_32 | 0.54 | 0.27 | 0.37 | Timeout (5s) | Timeout (5s) | 0.03 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_33": fully verified in 2.59 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_33 | 0.50 | 0.33 | 0.73 | Timeout (30s) | Timeout (30s) | 1.51 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_34": fully verified in 1.52 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_34 | 0.29 | 0.31 | 0.24 | 0.49 | Timeout (5s) | 0.18 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_35": fully verified in 1.82 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_35 | 0.25 | 0.32 | 0.16 | 0.98 | Timeout (5s) | 0.10 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_36": fully verified in 1.43 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_36 | 0.37 | 0.36 | 0.69 | Timeout (30s) | Timeout (5s) | 5.00 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_37": fully verified in 1.89 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_37 | 0.30 | 0.32 | 0.61 | Timeout (30s) | Timeout (5s) | 0.64 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_38": fully verified in 1.21 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_38 | 0.44 | 0.33 | 0.43 | Timeout (30s) | Timeout (5s) | 14.94 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_39": fully verified in 1.81 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_39 | 0.31 | 0.31 | 0.38 | Timeout (5s) | Timeout (5s) | 0.80 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_40": fully verified in 0.85 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_40 | 0.27 | 0.17 | 0.25 | Timeout (5s) | Timeout (5s) | 0.14 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_41": fully verified in 0.48 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_41 | 0.23 | 1.26 | 0.24 | Timeout (30s) | Timeout (5s) | 1.73 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_42": fully verified in 0.84 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_42 | 0.39 | 0.20 | 0.22 | Timeout (5s) | Timeout (5s) | 4.88 | 0.03 |
Theory "german.ctc_certif.German_ctc_hint_43": fully verified in 0.58 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_43 | 0.36 | 6.80 | 0.21 | Timeout (30s) | Timeout (5s) | 5.03 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_44": fully verified in 0.94 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_44 | 0.30 | 0.19 | 0.22 | Timeout (5s) | Timeout (5s) | 0.22 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_45": fully verified in 0.87 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_45 | 0.26 | 9.30 | 0.33 | Timeout (5s) | Timeout (5s) | 0.27 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_46": fully verified in 1.18 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_46 | 0.42 | 0.22 | 0.32 | Timeout (5s) | Timeout (5s) | 0.21 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_47": fully verified in 0.72 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_47 | 0.37 | Timeout (5s) | 0.33 | Timeout (5s) | Timeout (5s) | 5.04 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_48": fully verified in 4.02 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_48 | 0.27 | 0.22 | 0.22 | 3.12 | Timeout (5s) | 0.18 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_49": fully verified in 2.10 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_49 | 0.72 | 0.35 | 0.96 | Timeout (5s) | Timeout (5s) | 0.05 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_50": fully verified in 2.17 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_50 | 0.90 | 0.45 | 0.80 | Timeout (5s) | Timeout (5s) | 2.85 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_51": fully verified in 2.42 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_51 | 0.85 | 0.45 | 1.07 | Timeout (5s) | Timeout (5s) | 0.04 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_52": fully verified in 2.21 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_52 | 0.83 | 0.45 | 0.39 | Timeout (5s) | Timeout (5s) | 0.52 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_53": fully verified in 1.73 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_53 | 0.87 | 0.42 | 0.42 | Timeout (5s) | Timeout (5s) | 1.87 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_54": fully verified in 1.51 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_54 | 0.31 | 0.33 | 0.27 | 0.59 | Timeout (5s) | 5.03 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_55": fully verified in 1.00 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_55 | 0.35 | 0.28 | 0.11 | Timeout (5s) | Timeout (5s) | 0.25 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_56": fully verified in 2.68 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_56 | 0.85 | 0.37 | 0.84 | Timeout (5s) | Timeout (5s) | 0.60 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_57": fully verified in 1.68 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_57 | 0.74 | 0.39 | 0.54 | Timeout (5s) | Timeout (5s) | 2.54 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_58": fully verified in 2.35 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_58 | 0.32 | 0.26 | 0.22 | 1.54 | Timeout (5s) | 3.48 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_59": fully verified in 1.74 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_59 | 0.33 | 0.24 | 0.15 | 0.81 | Timeout (5s) | 0.20 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_60": fully verified in 0.77 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_60 | 0.40 | 1.16 | 0.35 | Timeout (5s) | Timeout (5s) | 5.06 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_61": fully verified in 2.01 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_61 | 0.81 | 0.40 | 0.70 | Timeout (5s) | Timeout (5s) | 0.08 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_62": fully verified in 4.74 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_62 | 0.51 | 1.60 | 0.14 | Timeout (5s) | 4.08 | 3.31 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_63": fully verified in 5.08 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_63 | 0.53 | 1.57 | 0.14 | Timeout (5s) | 4.40 | 5.04 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_64": fully verified in 0.79 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_64 | 0.46 | 1.64 | 0.31 | Timeout (5s) | Timeout (5s) | 0.93 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_65": fully verified in 0.82 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_65 | 0.27 | 1.82 | 0.33 | Timeout (5s) | Timeout (5s) | 0.20 | 0.02 |
Theory "german.ctc_certif.German_ctc_hint_66": fully verified in 0.90 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_66 | 0.26 | Timeout (5s) | 0.40 | Timeout (5s) | Timeout (5s) | 0.23 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_67": fully verified in 3.17 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_67 | 0.23 | 1.67 | 0.19 | 0.87 | 1.54 | 0.33 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_68": fully verified in 3.64 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_68 | 0.26 | 1.70 | 0.16 | 0.85 | 2.06 | 0.30 | 0.01 |
Theory "german.ctc_certif.German_ctc_hint_69": fully verified in 0.46 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_69 | 0.28 | 1.79 | 0.16 | Timeout (5s) | Timeout (5s) | 0.85 | 0.02 |
Theory "german.ctc_certif.German_ctc_preservation": fully verified in 1.33 s
| Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
preservation | 0.70 | 0.09 | 0.03 | 0.08 | 0.40 | 0.03 | 0.00 |