| TIME/MEM OUT/ERR | WRONG | SOLVED | WIN | UNIQUE | SUBOPTIMAL | NOT-RUN |
| Problem | cvc5_mbqi | cvc5_mf | cvc5_mf_rnd | cvc5_str1 | vam | z3 | VBS |
|---|---|---|---|---|---|---|---|
| C1 | 0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
448 (sec) s unsat |
193 (sec) n |
0 (sec) s unsat |
| C10 | 604 (sec) n |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
6 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| C11 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
256 (sec) n |
600 (sec) n |
| C12 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
323 (sec) n |
600 (sec) n |
| C13 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| C2 | 0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
600 (sec) n |
283 (sec) s unsat |
604 (sec) n |
0 (sec) s unsat |
| C3 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
532 (sec) s unsat |
2 (sec) n |
532 (sec) s unsat |
| C4 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
542 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| C5 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| C6 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
604 (sec) n |
601 (sec) n |
600 (sec) n |
| C7 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| C8 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| C9 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
1 (sec) s unsat |
601 (sec) n |
1 (sec) s unsat |
| U1 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
247 (sec) n |
600 (sec) n |
| U10 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U11 | 603 (sec) n |
600 (sec) n |
602 (sec) n |
324 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U12 | 604 (sec) n |
600 (sec) n |
604 (sec) n |
601 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U13 | 0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
2 (sec) s unsat |
109 (sec) n |
0 (sec) s unsat |
| U14 | 600 (sec) n |
600 (sec) n |
601 (sec) n |
0 (sec) n |
603 (sec) n |
15 (sec) n |
600 (sec) n |
| U15 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
477 (sec) n |
600 (sec) n |
| U16 | 600 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
| U17 | 0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U19 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U2 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
0 (sec) n |
604 (sec) n |
602 (sec) n |
600 (sec) n |
| U20 | 603 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
603 (sec) n |
282 (sec) n |
600 (sec) n |
| U21 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
604 (sec) n |
270 (sec) n |
600 (sec) n |
| U22 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
15 (sec) s unsat |
0 (sec) s unsat |
360 (sec) n |
0 (sec) s unsat |
| U23 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
604 (sec) n |
600 (sec) n |
600 (sec) n |
| U24 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
15 (sec) s unsat |
603 (sec) n |
213 (sec) n |
15 (sec) s unsat |
| U25 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
439 (sec) n |
600 (sec) n |
| U26 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U27 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U28 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
0 (sec) n |
600 (sec) n |
| U29 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U3 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
135 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
| U30 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
604 (sec) n |
600 (sec) n |
600 (sec) n |
| U31 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
300 (sec) n |
600 (sec) n |
| U33 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U37 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
603 (sec) n |
600 (sec) n |
| U38 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U39 | 601 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U4 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
15 (sec) s unsat |
458 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U40 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
313 (sec) n |
600 (sec) n |
| U41 | 606 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
606 (sec) n |
600 (sec) n |
| U42 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
233 (sec) n |
600 (sec) n |
| U43 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
460 (sec) n |
600 (sec) n |
| U44 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U45 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U46 | 600 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
285 (sec) n |
600 (sec) n |
| U47 | 603 (sec) n |
600 (sec) n |
604 (sec) n |
600 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U48 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
289 (sec) n |
600 (sec) n |
| U49 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
602 (sec) n |
306 (sec) n |
600 (sec) n |
| U5 | 600 (sec) n |
600 (sec) n |
229 (sec) s unsat |
241 (sec) s unsat |
15 (sec) s unsat |
316 (sec) n |
15 (sec) s unsat |
| U50 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
320 (sec) n |
600 (sec) n |
| U51 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U53 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U54 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
602 (sec) n |
296 (sec) n |
600 (sec) n |
| U56 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
604 (sec) n |
357 (sec) n |
600 (sec) n |
| U57 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
0 (sec) s unsat |
3 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U6 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U61 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U62 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
603 (sec) n |
600 (sec) n |
| U64 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
291 (sec) n |
600 (sec) n |
| U65 | 603 (sec) n |
601 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
248 (sec) n |
600 (sec) n |
| U66 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
591 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U67 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
604 (sec) n |
600 (sec) n |
| U68 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
1 (sec) n |
600 (sec) n |
| U7 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U70 | 600 (sec) n |
600 (sec) n |
601 (sec) n |
0 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U71 | 28 (sec) s unsat |
27 (sec) s unsat |
27 (sec) s unsat |
195 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
| U72 | 603 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U73 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
495 (sec) n |
600 (sec) n |
| U75 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
604 (sec) n |
601 (sec) n |
600 (sec) n |
| U76 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U79 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
15 (sec) n |
603 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U8 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
302 (sec) n |
600 (sec) n |
| U81 | 603 (sec) n |
24 (sec) s unsat |
601 (sec) n |
134 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U82 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
16 (sec) s unsat |
603 (sec) n |
601 (sec) n |
16 (sec) s unsat |
| U87 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U88 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| U89 | 604 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
101 (sec) n |
600 (sec) n |
| U9 | 603 (sec) n |
600 (sec) n |
600 (sec) n |
16 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
| U90 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
601 (sec) n |
600 (sec) n |
| U91 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
602 (sec) n |
600 (sec) n |
| U92 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
603 (sec) n |
602 (sec) n |
600 (sec) n |
| U93 | 603 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
603 (sec) n |
600 (sec) n |
600 (sec) n |
| TOTAL (86) | solved:5 wins:4 subopts:0 wrongs:0 uniq:0 |
solved:6 wins:4 subopts:0 wrongs:0 uniq:0 |
solved:6 wins:4 subopts:0 wrongs:0 uniq:0 |
solved:15 wins:7 subopts:0 wrongs:0 uniq:2 |
solved:18 wins:12 subopts:0 wrongs:0 uniq:3 |
solved:8 wins:8 subopts:0 wrongs:0 uniq:1 |
solved:21 wins:21 subopts:0 wrongs:0 uniq:6 |
| cvc5_mbqi | cvc5_mf | cvc5_mf_rnd | cvc5_str1 | vam | z3 | VBS |