| TIME/MEM OUT/ERR | WRONG | SOLVED | WIN | UNIQUE | SUBOPTIMAL | NOT-RUN |
| Problem | cvc5_mbqi | cvc5_str | cvc5_sygus | lmb | vam | vam_long | z3 | VBS |
|---|---|---|---|---|---|---|---|---|
| C10_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| C11_sol1 | 600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
602 (sec) n |
600 (sec) n |
311 (sec) n |
600 (sec) n |
| C12_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| C13_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| C1_sol1 | 600 (sec) n |
0 (sec) s unsat |
601 (sec) n |
601 (sec) n |
569 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| C2_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
603 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| C3_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
578 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| C4_sol1 | 601 (sec) n |
200 (sec) s unsat |
600 (sec) n |
600 (sec) n |
557 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| C5_sol1 | 600 (sec) n |
209 (sec) s unsat |
600 (sec) n |
600 (sec) n |
556 (sec) n |
25 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| C6_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| C7_sol1 | 600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
602 (sec) n |
581 (sec) n |
600 (sec) n |
600 (sec) n |
| C8_sol1 | 600 (sec) n |
600 (sec) n |
0 (sec) n |
600 (sec) n |
603 (sec) n |
0 (sec) n |
600 (sec) n |
600 (sec) n |
| C9_sol1 | 600 (sec) n |
1 (sec) s unsat |
600 (sec) n |
600 (sec) n |
304 (sec) s unsat |
63 (sec) n |
0 (sec) n |
1 (sec) s unsat |
| C9a_sol1 | 600 (sec) n |
1 (sec) s unsat |
600 (sec) n |
600 (sec) n |
602 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U10_sol1 | 600 (sec) n |
200 (sec) s unsat |
600 (sec) n |
600 (sec) n |
574 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U11_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U12_sol1 | 601 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
586 (sec) n |
28 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U13_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U14_sol1 | 8 (sec) s unsat |
56 (sec) s unsat |
601 (sec) n |
601 (sec) n |
579 (sec) n |
597 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U15_sol1 | 600 (sec) n |
118 (sec) n |
600 (sec) n |
600 (sec) n |
556 (sec) n |
0 (sec) n |
600 (sec) n |
600 (sec) n |
| U15_sol2 | 601 (sec) n |
400 (sec) n |
600 (sec) n |
601 (sec) n |
580 (sec) n |
596 (sec) n |
300 (sec) n |
600 (sec) n |
| U16_sol1 | 600 (sec) n |
3 (sec) s unsat |
0 (sec) n |
600 (sec) n |
1 (sec) s unsat |
0 (sec) s unsat |
9 (sec) n |
0 (sec) s unsat |
| U17_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U19_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U1_sol1 | 601 (sec) n |
400 (sec) n |
600 (sec) n |
600 (sec) n |
586 (sec) n |
595 (sec) n |
600 (sec) n |
600 (sec) n |
| U20_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U20_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U20_sol3 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U21_sol1 | 600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
577 (sec) n |
26 (sec) n |
180 (sec) n |
600 (sec) n |
| U22_sol1 | 600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
597 (sec) n |
206 (sec) n |
600 (sec) n |
| U23_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U24_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U25_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U25_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U26_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
2 (sec) s unsat |
537 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U26_sol2 | 7 (sec) s unsat |
2 (sec) s unsat |
600 (sec) n |
600 (sec) n |
603 (sec) n |
599 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U27_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
602 (sec) n |
351 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U29_sol1 | 600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
556 (sec) n |
589 (sec) n |
304 (sec) n |
600 (sec) n |
| U2_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
1 (sec) s unsat |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U33_sol1 | 601 (sec) n |
500 (sec) n |
600 (sec) n |
600 (sec) n |
575 (sec) n |
576 (sec) n |
600 (sec) n |
600 (sec) n |
| U37_sol1 | 600 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
574 (sec) n |
28 (sec) n |
600 (sec) n |
600 (sec) n |
| U39_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
570 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U3_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U40_sol1 | 601 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
580 (sec) n |
0 (sec) n |
600 (sec) n |
600 (sec) n |
| U41_sol1 | 600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
603 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U41_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U41_sol3 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U42_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U43_sol1 | 600 (sec) n |
600 (sec) n |
601 (sec) n |
601 (sec) n |
580 (sec) n |
587 (sec) n |
137 (sec) n |
600 (sec) n |
| U44_sol1 | 3 (sec) s unsat |
202 (sec) s unsat |
600 (sec) n |
1 (sec) s unsat |
6 (sec) s unsat |
573 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U44_sol2 | 600 (sec) n |
601 (sec) n |
600 (sec) n |
600 (sec) n |
577 (sec) n |
598 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U45_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
1 (sec) s unsat |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U45_sol2 | 1 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
1 (sec) s unsat |
12 (sec) s unsat |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U46_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U46_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U48_sol1 | 601 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U48_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U49_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U49_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U4_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
600 (sec) n |
582 (sec) n |
588 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U50_sol1 | 23 (sec) s unsat |
600 (sec) n |
600 (sec) n |
600 (sec) n |
571 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U50_sol2 | 1 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
1 (sec) s unsat |
580 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U50_sol3 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U51_sol1 | 600 (sec) n |
600 (sec) n |
601 (sec) n |
600 (sec) n |
139 (sec) s unsat |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U53_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U54_sol1 | 1 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
1 (sec) s unsat |
569 (sec) n |
30 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U54_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U56_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U56_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
603 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U57_sol1 | 600 (sec) n |
0 (sec) s unsat |
600 (sec) n |
600 (sec) n |
3 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U5_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U61_sol1 | 600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
602 (sec) n |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U62_sol1 | 151 (sec) s unsat |
201 (sec) s unsat |
600 (sec) n |
600 (sec) n |
13 (sec) s unsat |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U64_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U66_sol1 | 3 (sec) s unsat |
200 (sec) s unsat |
601 (sec) n |
601 (sec) n |
591 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U66_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U67_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
34 (sec) s unsat |
31 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U68_sol1 | 601 (sec) n |
600 (sec) n |
600 (sec) n |
601 (sec) n |
1 (sec) s unsat |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U6_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
602 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U71_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U72_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U72_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U73_sol1 | 600 (sec) n |
600 (sec) n |
600 (sec) n |
600 (sec) n |
585 (sec) n |
574 (sec) n |
601 (sec) n |
600 (sec) n |
| U75_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U75_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U76_sol1 | 600 (sec) n |
201 (sec) s unsat |
600 (sec) n |
600 (sec) n |
587 (sec) n |
599 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U7_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U81_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U82_sol1 | 601 (sec) n |
0 (sec) s unsat |
600 (sec) n |
601 (sec) n |
577 (sec) n |
554 (sec) n |
601 (sec) n |
0 (sec) s unsat |
| U87_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U87_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U89_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U8_sol1 | 0 (sec) s unsat |
200 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
582 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U8_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U90_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
601 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
3 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U91_sol1 | 2 (sec) s unsat |
13 (sec) s unsat |
600 (sec) n |
1 (sec) s unsat |
575 (sec) n |
0 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U91_sol2 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U92_sol1 | 600 (sec) n |
0 (sec) s unsat |
601 (sec) n |
1 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| U93_sol1 | 92 (sec) s unsat |
36 (sec) s unsat |
600 (sec) n |
600 (sec) n |
562 (sec) n |
30 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
| U9_sol1 | 0 (sec) s unsat |
0 (sec) s unsat |
600 (sec) n |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
0 (sec) s unsat |
| TOTAL (100) | solved:68 wins:60 subopts:0 wrongs:0 uniq:0 |
solved:78 wins:65 subopts:0 wrongs:0 uniq:1 |
solved:0 wins:0 subopts:0 wrongs:0 uniq:0 |
solved:62 wins:62 subopts:0 wrongs:0 uniq:0 |
solved:59 wins:51 subopts:0 wrongs:0 uniq:0 |
solved:51 wins:49 subopts:0 wrongs:0 uniq:0 |
solved:83 wins:83 subopts:0 wrongs:0 uniq:4 |
solved:86 wins:86 subopts:0 wrongs:0 uniq:5 |
| cvc5_mbqi | cvc5_str | cvc5_sygus | lmb | vam | vam_long | z3 | VBS |