| Problem | RAReQS-NN | GhostQ | CirQit |
|---|---|---|---|
| counter4_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring4_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter5_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_3.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring5_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter6_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring4_3.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring6_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter7_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_5.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring4_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter5_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter8_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_6.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring4_5.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring5_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_7.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter6_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring4_6.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_8.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring6_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring4_7.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| counter4_9.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore_3.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore3_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter7_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_10.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring4_8.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| counter4_11.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter5_8.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_12.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter8_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_13.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore4_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_14.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring5_8.qpro | 7 (7+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| counter4_15.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter6_8.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore3_3.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter4_16.qpro | 0 (0+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| semaphore_5.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore5_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring6_8.qpro | 27 (27+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter7_8.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore3_4.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore4_3.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore6_2.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter5_16.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter8_8.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore5_3.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring5_16.qpro | 14 (14+0) s cnf 0 (s cnf 0) |
2 (2+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| semaphore4_4.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| dmeSmall_2.qpro | 800 (799+2) | 0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter6_16.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| semaphore6_3.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring6_16.qpro | 71 (71+0) s cnf 0 (s cnf 0) |
5 (5+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
| semaphore5_4.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
1 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter7_16.qpro | 0 (0+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| dme1_2.qpro | 11 (11+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter5_32.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| counter5_33.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| semaphore6_4.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| counter8_16.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring5_32.qpro | 30 (30+0) s cnf 0 (s cnf 0) |
5 (5+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
| ring5_33.qpro | 31 (31+0) s cnf 0 (s cnf 0) |
5 (5+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
| dmeSmall_4.qpro | 11 (11+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter6_32.qpro | 2 (1+0) s cnf 1 (s cnf 1) |
2 (2+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| dme1_3.qpro | 800 (800+0) | 1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| ring6_32.qpro | 147 (147+0) s cnf 0 (s cnf 0) |
13 (13+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| counter7_32.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
3 (3+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| dme1_4.qpro | 800 (800+0) | 1 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| counter8_32.qpro | 2 (2+0) s cnf 1 (s cnf 1) |
5 (4+0) s cnf 1 (s cnf 1) |
2 (2+0) s cnf 1 (s cnf 1) |
| dme1_5.qpro | 794 (794+0) s cnf 1 (s cnf 1) |
2 (1+0) s cnf 1 (s cnf 1) |
0 (0+0) s cnf 1 (s cnf 1) |
| consistency_0_1.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
47 (47+0) s cnf 1 (s cnf 1) |
4 (4+0) s cnf 1 (s cnf 1) |
| possibility1_0_1.qpro | 3 (2+0) s cnf 0 (s cnf 0) |
47 (46+0) s cnf 0 (s cnf 0) |
13 (13+0) s cnf 0 (s cnf 0) |
| assertion11_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| possibility2_0_1.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
43 (43+0) s cnf 0 (s cnf 0) |
18 (17+1) s cnf 0 (s cnf 0) |
| possibility4_0_1.qpro | 3 (3+0) s cnf 0 (s cnf 0) |
41 (41+0) s cnf 0 (s cnf 0) |
2 (2+0) s cnf 0 (s cnf 0) |
| possibility7_0_1.qpro | 1 (1+0) s cnf 1 (s cnf 1) |
75 (75+0) s cnf 1 (s cnf 1) |
4 (4+0) s cnf 1 (s cnf 1) |
| possibility6_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
2 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| assertion12_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| assertion8_0_1.qpro | 7 (7+0) s cnf 0 (s cnf 0) |
119 (119+0) s cnf 0 (s cnf 0) |
20 (20+1) s cnf 0 (s cnf 0) |
| possibility10_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
16 (16+0) s cnf 0 (s cnf 0) |
2 (2+0) s cnf 0 (s cnf 0) |
| possibility11_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
20 (20+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
| dmeSmall_8.qpro | 196 (196+0) s cnf 1 (s cnf 1) |
4 (4+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| possibility9_0_1.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
41 (41+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| possibility3_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
10 (10+0) s cnf 0 (s cnf 0) |
8 (8+0) s cnf 0 (s cnf 0) |
| assertion5_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| assertion9_0_1.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
42 (42+0) s cnf 0 (s cnf 0) |
23 (22+1) s cnf 0 (s cnf 0) |
| possibility12_0_1.qpro | 12 (12+0) s cnf 0 (s cnf 0) |
72 (72+0) s cnf 0 (s cnf 0) |
9 (9+0) s cnf 0 (s cnf 0) |
| assertion6_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
2 (2+0) s cnf 0 (s cnf 0) |
0 (0+0) s cnf 0 (s cnf 0) |
| assertion1_0_1.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
55 (55+0) s cnf 0 (s cnf 0) |
45 (44+1) s cnf 0 (s cnf 0) |
| assertion3_0_1.qpro | 5 (5+0) s cnf 0 (s cnf 0) |
55 (55+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| assertion10_0_1.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
43 (43+0) s cnf 0 (s cnf 0) |
40 (39+1) s cnf 0 (s cnf 0) |
| assertion2_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
18 (18+0) s cnf 0 (s cnf 0) |
5 (5+0) s cnf 0 (s cnf 0) |
| possibility8_0_1.qpro | 17 (17+0) s cnf 0 (s cnf 0) |
54 (53+0) s cnf 0 (s cnf 0) |
4 (4+0) s cnf 0 (s cnf 0) |
| possibility5_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
14 (14+0) s cnf 0 (s cnf 0) |
4 (4+0) s cnf 0 (s cnf 0) |
| counter6_64.qpro | 8 (8+0) s cnf 0 (s cnf 0) |
10 (10+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| assertion4_0_1.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
37 (37+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| assertion7_0_1.qpro | 1 (1+0) s cnf 0 (s cnf 0) |
18 (18+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| counter6_65.qpro | 8 (8+0) s cnf 0 (s cnf 0) |
10 (10+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| dme1_6.qpro | 22 (22+0) s cnf 1 (s cnf 1) |
2 (2+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| dmeSmall_9.qpro | 20 (20+0) s cnf 1 (s cnf 1) |
21 (21+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| ring6_64.qpro | 306 (306+0) s cnf 0 (s cnf 0) |
34 (33+0) s cnf 0 (s cnf 0) |
9 (9+0) s cnf 0 (s cnf 0) |
| ring6_65.qpro | 311 (311+0) s cnf 0 (s cnf 0) |
34 (33+0) s cnf 0 (s cnf 0) |
11 (11+0) s cnf 0 (s cnf 0) |
| dme1_7.qpro | 800 (799+1) | 3 (3+0) s cnf 1 (s cnf 1) |
1 (1+0) s cnf 1 (s cnf 1) |
| counter7_64.qpro | 12 (12+0) s cnf 1 (s cnf 1) |
15 (15+0) s cnf 1 (s cnf 1) |
4 (4+0) s cnf 1 (s cnf 1) |
| dme1_8.qpro | 800 (800+0) | 5 (5+0) s cnf 1 (s cnf 1) |
2 (2+0) s cnf 1 (s cnf 1) |
| counter8_64.qpro | 13 (13+0) s cnf 1 (s cnf 1) |
27 (27+0) s cnf 1 (s cnf 1) |
16 (16+0) s cnf 1 (s cnf 1) |
| consistency_0_2.qpro | 2 (2+0) s cnf 1 (s cnf 1) |
283 (282+0) s cnf 1 (s cnf 1) |
22 (21+0) s cnf 1 (s cnf 1) |
| possibility1_0_2.qpro | 10 (9+0) s cnf 0 (s cnf 0) |
254 (254+0) s cnf 0 (s cnf 0) |
79 (78+1) s cnf 0 (s cnf 0) |
| assertion11_0_2.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
25 (25+0) s cnf 0 (s cnf 0) |
20 (20+0) s cnf 0 (s cnf 0) |
| possibility2_0_2.qpro | 9 (9+1) s cnf 0 (s cnf 0) |
274 (273+0) s cnf 0 (s cnf 0) |
79 (77+1) s cnf 0 (s cnf 0) |
| possibility4_0_2.qpro | 8 (8+1) s cnf 0 (s cnf 0) |
267 (267+0) s cnf 0 (s cnf 0) |
108 (106+2) s cnf 0 (s cnf 0) |
| possibility10_0_2.qpro | 3 (3+0) s cnf 0 (s cnf 0) |
116 (116+0) s cnf 0 (s cnf 0) |
28 (28+0) s cnf 0 (s cnf 0) |
| possibility7_0_2.qpro | 5 (5+0) s cnf 1 (s cnf 1) |
336 (336+0) s cnf 1 (s cnf 1) |
22 (21+0) s cnf 1 (s cnf 1) |
| possibility6_0_2.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
4 (4+0) s cnf 0 (s cnf 0) |
1 (1+0) s cnf 0 (s cnf 0) |
| possibility11_0_2.qpro | 4 (4+0) s cnf 0 (s cnf 0) |
127 (126+0) s cnf 0 (s cnf 0) |
26 (26+0) s cnf 0 (s cnf 0) |
| possibility3_0_2.qpro | 6 (5+0) s cnf 0 (s cnf 0) |
149 (149+0) s cnf 0 (s cnf 0) |
35 (35+1) s cnf 0 (s cnf 0) |
| assertion5_0_2.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
48 (48+0) s cnf 0 (s cnf 0) |
92 (91+1) s cnf 0 (s cnf 0) |
| assertion9_0_2.qpro | 12 (10+1) s cnf 0 (s cnf 0) |
305 (305+0) s cnf 0 (s cnf 0) |
89 (87+2) s cnf 0 (s cnf 0) |
| assertion8_0_2.qpro | 147 (138+9) s cnf 0 (s cnf 0) |
800 (799+1) | 252 (249+3) s cnf 0 (s cnf 0) |
| assertion6_0_2.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
10 (10+0) s cnf 0 (s cnf 0) |
29 (29+0) s cnf 0 (s cnf 0) |
| assertion1_0_2.qpro | 9 (7+1) s cnf 0 (s cnf 0) |
254 (254+0) s cnf 0 (s cnf 0) |
40 (39+1) s cnf 0 (s cnf 0) |
| possibility9_0_2.qpro | 6 (6+1) s cnf 0 (s cnf 0) |
234 (234+0) s cnf 0 (s cnf 0) |
132 (130+2) s cnf 0 (s cnf 0) |
| assertion12_0_2.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
98 (98+0) s cnf 0 (s cnf 0) |
100 (98+2) s cnf 0 (s cnf 0) |
| assertion10_0_2.qpro | 6 (6+0) s cnf 0 (s cnf 0) |
203 (202+0) s cnf 0 (s cnf 0) |
66 (65+1) s cnf 0 (s cnf 0) |
| assertion3_0_2.qpro | 29 (27+2) s cnf 0 (s cnf 0) |
244 (244+0) s cnf 0 (s cnf 0) |
91 (90+2) s cnf 0 (s cnf 0) |
| assertion2_0_2.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
102 (102+0) s cnf 0 (s cnf 0) |
22 (21+0) s cnf 0 (s cnf 0) |
| possibility12_0_2.qpro | 172 (166+7) s cnf 0 (s cnf 0) |
800 (799+1) | 300 (297+4) s cnf 0 (s cnf 0) |
| possibility5_0_2.qpro | 3 (2+0) s cnf 0 (s cnf 0) |
155 (154+0) s cnf 0 (s cnf 0) |
39 (38+1) s cnf 0 (s cnf 0) |
| assertion4_0_2.qpro | 6 (6+0) s cnf 0 (s cnf 0) |
213 (213+0) s cnf 0 (s cnf 0) |
70 (69+1) s cnf 0 (s cnf 0) |
| assertion7_0_2.qpro | 2 (2+0) s cnf 0 (s cnf 0) |
55 (55+0) s cnf 0 (s cnf 0) |
21 (20+0) s cnf 0 (s cnf 0) |
| possibility8_0_2.qpro | 112 (110+2) s cnf 0 (s cnf 0) |
365 (364+0) s cnf 0 (s cnf 0) |
108 (107+2) s cnf 0 (s cnf 0) |
| counter7_128.qpro | 92 (92+0) s cnf 0 (s cnf 0) |
72 (72+0) s cnf 0 (s cnf 0) |
111 (110+1) s cnf 0 (s cnf 0) |
| counter7_129.qpro | 93 (93+0) s cnf 0 (s cnf 0) |
76 (76+0) s cnf 0 (s cnf 0) |
122 (122+1) s cnf 0 (s cnf 0) |
| counter8_128.qpro | 140 (140+0) s cnf 1 (s cnf 1) |
125 (125+0) s cnf 1 (s cnf 1) |
443 (441+2) |
| consistency_0_3.qpro | 3 (3+0) s cnf 1 (s cnf 1) |
800 (800+0) | 81 (80+1) s cnf 1 (s cnf 1) |
| possibility1_0_3.qpro | 19 (17+2) s cnf 0 (s cnf 0) |
671 (670+0) s cnf 0 (s cnf 0) |
178 (176+2) s cnf 0 (s cnf 0) |
| assertion11_0_3.qpro | 4 (4+0) s cnf 0 (s cnf 0) |
150 (149+0) s cnf 0 (s cnf 0) |
60 (59+1) s cnf 0 (s cnf 0) |
| possibility2_0_3.qpro | 22 (19+2) s cnf 0 (s cnf 0) |
800 (800+0) | 209 (206+3) s cnf 0 (s cnf 0) |
| possibility4_0_3.qpro | 24 (23+1) s cnf 0 (s cnf 0) |
622 (622+0) s cnf 0 (s cnf 0) |
447 (441+6) s cnf 0 (s cnf 0) |
| possibility10_0_3.qpro | 6 (5+0) s cnf 0 (s cnf 0) |
335 (334+0) s cnf 0 (s cnf 0) |
150 (148+2) s cnf 0 (s cnf 0) |
| possibility7_0_3.qpro | 29 (23+6) s cnf 1 (s cnf 1) |
800 (800+0) | 203 (200+3) s cnf 1 (s cnf 1) |
| possibility6_0_3.qpro | 4 (4+0) s cnf 0 (s cnf 0) |
6 (6+0) s cnf 0 (s cnf 0) |
3 (3+0) s cnf 0 (s cnf 0) |
| possibility11_0_3.qpro | 9 (8+0) s cnf 0 (s cnf 0) |
309 (309+0) s cnf 0 (s cnf 0) |
147 (145+2) s cnf 0 (s cnf 0) |
| possibility3_0_3.qpro | 20 (18+2) s cnf 0 (s cnf 0) |
498 (498+0) s cnf 0 (s cnf 0) |
105 (104+2) s cnf 0 (s cnf 0) |
| assertion5_0_3.qpro | 4 (4+0) s cnf 0 (s cnf 0) |
180 (180+0) s cnf 0 (s cnf 0) |
364 (360+5) s cnf 0 (s cnf 0) |
| assertion9_0_3.qpro | 66 (60+6) s cnf 0 (s cnf 0) |
786 (786+0) s cnf 0 (s cnf 0) |
207 (204+3) s cnf 0 (s cnf 0) |
| assertion6_0_3.qpro | 4 (3+0) s cnf 0 (s cnf 0) |
31 (31+0) s cnf 0 (s cnf 0) |
99 (97+1) s cnf 0 (s cnf 0) |
| assertion1_0_3.qpro | 19 (16+3) s cnf 0 (s cnf 0) |
800 (800+0) | 142 (140+2) s cnf 0 (s cnf 0) |
| assertion12_0_3.qpro | 5 (4+0) s cnf 0 (s cnf 0) |
362 (362+0) s cnf 0 (s cnf 0) |
97 (96+1) s cnf 0 (s cnf 0) |
| assertion10_0_3.qpro | 14 (14+0) s cnf 0 (s cnf 0) |
580 (580+0) s cnf 0 (s cnf 0) |
138 (136+2) s cnf 0 (s cnf 0) |
| assertion3_0_3.qpro | 97 (79+18) s cnf 0 (s cnf 0) |
673 (673+0) s cnf 0 (s cnf 0) |
394 (388+5) s cnf 0 (s cnf 0) |
| assertion8_0_3.qpro | 502 (424+78) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (793+7) |
| assertion2_0_3.qpro | 4 (4+0) s cnf 0 (s cnf 0) |
467 (467+0) s cnf 0 (s cnf 0) |
159 (157+2) s cnf 0 (s cnf 0) |
| possibility9_0_3.qpro | 12 (12+0) s cnf 0 (s cnf 0) |
800 (800+0) | 522 (515+7) s cnf 0 (s cnf 0) |
| possibility5_0_3.qpro | 5 (5+0) s cnf 0 (s cnf 0) |
512 (512+0) s cnf 0 (s cnf 0) |
367 (362+5) s cnf 0 (s cnf 0) |
| assertion4_0_3.qpro | 13 (12+1) s cnf 0 (s cnf 0) |
551 (551+0) s cnf 0 (s cnf 0) |
393 (388+5) s cnf 0 (s cnf 0) |
| assertion7_0_3.qpro | 4 (3+0) s cnf 0 (s cnf 0) |
69 (69+0) s cnf 0 (s cnf 0) |
186 (183+3) s cnf 0 (s cnf 0) |
| possibility12_0_3.qpro | 634 (582+52) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (792+8) |
| possibility8_0_3.qpro | 130 (120+10) s cnf 0 (s cnf 0) |
800 (800+0) | 331 (326+5) s cnf 0 (s cnf 0) |
| consistency_0_4.qpro | 5 (5+0) s cnf 1 (s cnf 1) |
800 (800+0) | 146 (144+2) s cnf 1 (s cnf 1) |
| possibility1_0_4.qpro | 50 (41+8) s cnf 0 (s cnf 0) |
800 (800+0) | 366 (361+5) s cnf 0 (s cnf 0) |
| assertion11_0_4.qpro | 6 (6+0) s cnf 0 (s cnf 0) |
393 (392+0) s cnf 0 (s cnf 0) |
106 (105+1) s cnf 0 (s cnf 0) |
| possibility2_0_4.qpro | 50 (41+8) s cnf 0 (s cnf 0) |
800 (800+0) | 321 (316+4) s cnf 0 (s cnf 0) |
| possibility4_0_4.qpro | 34 (28+6) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| possibility10_0_4.qpro | 11 (9+1) s cnf 0 (s cnf 0) |
800 (800+0) | 403 (397+5) s cnf 0 (s cnf 0) |
| possibility6_0_4.qpro | 6 (5+0) s cnf 0 (s cnf 0) |
10 (9+0) s cnf 0 (s cnf 0) |
7 (7+0) s cnf 0 (s cnf 0) |
| possibility11_0_4.qpro | 21 (19+3) s cnf 0 (s cnf 0) |
800 (800+0) | 447 (441+5) s cnf 0 (s cnf 0) |
| possibility7_0_4.qpro | 37 (30+7) s cnf 1 (s cnf 1) |
800 (800+0) | 212 (209+3) s cnf 1 (s cnf 1) |
| assertion9_0_4.qpro | 45 (38+7) s cnf 0 (s cnf 0) |
800 (800+0) | 426 (420+6) s cnf 0 (s cnf 0) |
| possibility3_0_4.qpro | 32 (28+5) s cnf 0 (s cnf 0) |
800 (800+0) | 254 (250+4) s cnf 0 (s cnf 0) |
| assertion5_0_4.qpro | 7 (6+0) s cnf 0 (s cnf 0) |
538 (538+0) s cnf 0 (s cnf 0) |
800 (790+10) |
| assertion6_0_4.qpro | 5 (5+0) s cnf 0 (s cnf 0) |
169 (168+0) s cnf 0 (s cnf 0) |
371 (366+5) s cnf 0 (s cnf 0) |
| assertion1_0_4.qpro | 42 (34+9) s cnf 0 (s cnf 0) |
800 (800+0) | 263 (260+3) s cnf 0 (s cnf 0) |
| assertion12_0_4.qpro | 9 (8+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| assertion10_0_4.qpro | 31 (25+5) s cnf 0 (s cnf 0) |
800 (800+0) | 278 (274+4) s cnf 0 (s cnf 0) |
| possibility5_0_4.qpro | 8 (8+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| assertion3_0_4.qpro | 256 (205+50) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| assertion2_0_4.qpro | 6 (5+0) s cnf 0 (s cnf 0) |
800 (800+0) | 249 (246+3) s cnf 0 (s cnf 0) |
| assertion4_0_4.qpro | 30 (24+6) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| assertion7_0_4.qpro | 5 (5+0) s cnf 0 (s cnf 0) |
178 (177+0) s cnf 0 (s cnf 0) |
225 (222+3) s cnf 0 (s cnf 0) |
| assertion8_0_4.qpro | 800 (641+159) | 800 (800+0) | 800 (791+9) |
| possibility9_0_4.qpro | 23 (19+4) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| possibility12_0_4.qpro | 800 (632+168) | 800 (800+0) | 800 (791+9) |
| possibility8_0_4.qpro | 555 (451+105) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| consistency_0_5.qpro | 7 (6+0) s cnf 1 (s cnf 1) |
800 (800+0) | 305 (301+3) s cnf 1 (s cnf 1) |
| possibility1_0_5.qpro | 73 (64+9) s cnf 0 (s cnf 0) |
800 (800+0) | 667 (659+8) s cnf 0 (s cnf 0) |
| assertion11_0_5.qpro | 9 (8+0) s cnf 0 (s cnf 0) |
703 (703+1) s cnf 0 (s cnf 0) |
287 (284+3) s cnf 0 (s cnf 0) |
| possibility2_0_5.qpro | 84 (70+13) s cnf 0 (s cnf 0) |
800 (800+0) | 788 (778+10) s cnf 0 (s cnf 0) |
| possibility4_0_5.qpro | 50 (42+7) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| possibility10_0_5.qpro | 17 (15+2) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| possibility11_0_5.qpro | 28 (27+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| possibility6_0_5.qpro | 8 (8+0) s cnf 0 (s cnf 0) |
14 (13+0) s cnf 0 (s cnf 0) |
19 (19+0) s cnf 0 (s cnf 0) |
| possibility7_0_5.qpro | 111 (86+26) s cnf 1 (s cnf 1) |
800 (800+0) | 293 (290+3) s cnf 1 (s cnf 1) |
| assertion9_0_5.qpro | 71 (55+16) s cnf 0 (s cnf 0) |
800 (800+0) | 667 (659+8) s cnf 0 (s cnf 0) |
| possibility3_0_5.qpro | 50 (44+6) s cnf 0 (s cnf 0) |
800 (800+0) | 528 (522+6) s cnf 0 (s cnf 0) |
| assertion5_0_5.qpro | 10 (9+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| assertion6_0_5.qpro | 7 (7+0) s cnf 0 (s cnf 0) |
163 (163+0) s cnf 0 (s cnf 0) |
313 (309+4) s cnf 0 (s cnf 0) |
| assertion1_0_5.qpro | 70 (56+14) s cnf 0 (s cnf 0) |
800 (800+0) | 498 (492+6) s cnf 0 (s cnf 0) |
| assertion10_0_5.qpro | 40 (34+6) s cnf 0 (s cnf 0) |
800 (800+0) | 562 (556+7) s cnf 0 (s cnf 0) |
| assertion12_0_5.qpro | 14 (13+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| possibility5_0_5.qpro | 13 (12+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| assertion3_0_5.qpro | 349 (284+65) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| assertion4_0_5.qpro | 37 (32+6) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| assertion2_0_5.qpro | 8 (8+0) s cnf 0 (s cnf 0) |
800 (800+0) | 452 (447+5) s cnf 0 (s cnf 0) |
| assertion7_0_5.qpro | 8 (7+0) s cnf 0 (s cnf 0) |
298 (297+0) s cnf 0 (s cnf 0) |
397 (393+5) s cnf 0 (s cnf 0) |
| assertion8_0_5.qpro | 800 (634+166) | 800 (800+0) | 800 (791+9) |
| possibility9_0_5.qpro | 30 (30+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| possibility12_0_5.qpro | 800 (660+140) | 800 (800+0) | 800 (792+8) |
| possibility8_0_5.qpro | 423 (362+62) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (790+10) |
| counter8_256.qpro | 800 (799+2) | 576 (575+1) s cnf 0 (s cnf 0) |
522 (520+2) |
| counter8_257.qpro | 800 (798+2) | 591 (591+1) s cnf 0 (s cnf 0) |
641 (639+2) |
| consistency_0_6.qpro | 9 (9+0) s cnf 1 (s cnf 1) |
800 (800+0) | 444 (439+5) s cnf 1 (s cnf 1) |
| possibility1_0_6.qpro | 109 (93+17) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| assertion11_0_6.qpro | 12 (11+1) s cnf 0 (s cnf 0) |
800 (800+0) | 445 (440+5) s cnf 0 (s cnf 0) |
| possibility2_0_6.qpro | 110 (95+15) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| possibility4_0_6.qpro | 87 (69+18) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (791+9) |
| possibility10_0_6.qpro | 23 (22+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (792+8) |
| possibility11_0_6.qpro | 56 (50+6) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (792+8) |
| assertion9_0_6.qpro | 160 (130+30) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (791+9) |
| possibility3_0_6.qpro | 67 (59+8) s cnf 0 (s cnf 0) |
800 (800+0) | 497 (492+5) s cnf 0 (s cnf 0) |
| assertion5_0_6.qpro | 14 (13+1) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (791+9) |
| possibility6_0_6.qpro | 11 (11+1) s cnf 0 (s cnf 0) |
19 (19+0) s cnf 0 (s cnf 0) |
50 (49+0) s cnf 0 (s cnf 0) |
| possibility7_0_6.qpro | 227 (178+49) s cnf 1 (s cnf 1) |
800 (799+1) | 671 (665+7) s cnf 1 (s cnf 1) |
| assertion6_0_6.qpro | 10 (10+0) s cnf 0 (s cnf 0) |
217 (217+0) s cnf 0 (s cnf 0) |
378 (374+4) s cnf 0 (s cnf 0) |
| assertion10_0_6.qpro | 89 (74+15) s cnf 0 (s cnf 0) |
800 (800+0) | 559 (553+6) s cnf 0 (s cnf 0) |
| assertion12_0_6.qpro | 21 (18+2) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (792+8) |
| assertion1_0_6.qpro | 116 (94+22) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (792+8) |
| possibility5_0_6.qpro | 18 (16+2) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (792+8) |
| assertion4_0_6.qpro | 65 (54+11) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (792+8) |
| assertion3_0_6.qpro | 800 (667+133) | 800 (799+1) | 800 (792+8) |
| assertion7_0_6.qpro | 10 (10+0) s cnf 0 (s cnf 0) |
485 (484+1) s cnf 0 (s cnf 0) |
723 (715+7) s cnf 0 (s cnf 0) |
| assertion2_0_6.qpro | 11 (11+1) s cnf 0 (s cnf 0) |
800 (800+0) | 729 (721+8) s cnf 0 (s cnf 0) |
| possibility9_0_6.qpro | 51 (46+5) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (791+9) |
| assertion8_0_6.qpro | 800 (635+165) | 800 (800+0) | 800 (792+8) |
| possibility12_0_6.qpro | 800 (682+118) | 800 (800+0) | 800 (792+8) |
| possibility8_0_6.qpro | 800 (682+118) | 800 (800+1) | 648 (641+7) s cnf 0 (s cnf 0) |
| consistency_0_7.qpro | 12 (11+0) s cnf 1 (s cnf 1) |
800 (800+0) | 764 (756+8) s cnf 1 (s cnf 1) |
| possibility1_0_7.qpro | 175 (151+24) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (792+8) |
| assertion11_0_7.qpro | 17 (16+1) s cnf 0 (s cnf 0) |
800 (800+1) | 695 (689+7) s cnf 0 (s cnf 0) |
| possibility2_0_7.qpro | 138 (119+19) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (792+8) |
| possibility4_0_7.qpro | 126 (101+26) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (792+8) |
| possibility10_0_7.qpro | 32 (29+3) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| possibility11_0_7.qpro | 104 (90+14) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| assertion9_0_7.qpro | 177 (146+30) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (792+8) |
| possibility3_0_7.qpro | 130 (109+21) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (792+8) |
| assertion5_0_7.qpro | 19 (18+2) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| possibility7_0_7.qpro | 377 (293+84) s cnf 1 (s cnf 1) |
800 (800+1) | 777 (770+7) s cnf 1 (s cnf 1) |
| possibility6_0_7.qpro | 14 (13+1) s cnf 0 (s cnf 0) |
24 (23+1) s cnf 0 (s cnf 0) |
135 (134+1) s cnf 0 (s cnf 0) |
| assertion6_0_7.qpro | 14 (14+1) s cnf 0 (s cnf 0) |
115 (114+1) s cnf 0 (s cnf 0) |
738 (731+7) s cnf 0 (s cnf 0) |
| assertion12_0_7.qpro | 32 (28+4) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (792+8) |
| assertion10_0_7.qpro | 118 (96+22) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (792+8) |
| assertion1_0_7.qpro | 183 (149+34) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (792+8) |
| possibility5_0_7.qpro | 27 (24+3) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| assertion4_0_7.qpro | 96 (79+17) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| assertion7_0_7.qpro | 14 (13+1) s cnf 0 (s cnf 0) |
781 (780+1) s cnf 0 (s cnf 0) |
800 (792+8) |
| assertion3_0_7.qpro | 800 (652+148) | 800 (800+0) | 800 (793+7) |
| assertion2_0_7.qpro | 16 (15+1) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (794+6) |
| possibility9_0_7.qpro | 85 (69+15) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (792+8) |
| assertion8_0_7.qpro | 800 (636+164) | 800 (800+0) | 800 (792+8) |
| possibility12_0_7.qpro | 800 (648+152) | 800 (800+0) | 800 (792+8) |
| possibility8_0_7.qpro | 800 (630+171) | 800 (800+1) | 800 (792+8) |
| consistency_0_8.qpro | 15 (15+0) s cnf 1 (s cnf 1) |
800 (800+1) | 800 (793+7) |
| possibility1_0_8.qpro | 267 (228+39) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (793+7) |
| assertion11_0_8.qpro | 22 (20+1) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (794+6) |
| possibility2_0_8.qpro | 213 (184+29) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (793+7) |
| possibility4_0_8.qpro | 148 (123+24) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (793+7) |
| possibility10_0_8.qpro | 45 (42+4) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (794+6) |
| assertion9_0_8.qpro | 338 (278+60) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (793+7) |
| possibility3_0_8.qpro | 207 (179+29) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| assertion5_0_8.qpro | 25 (23+2) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| possibility11_0_8.qpro | 124 (110+14) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (794+6) |
| assertion6_0_8.qpro | 18 (17+1) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| possibility7_0_8.qpro | 435 (349+86) s cnf 1 (s cnf 1) |
800 (800+1) | 800 (794+6) |
| possibility6_0_8.qpro | 19 (18+1) s cnf 0 (s cnf 0) |
36 (35+0) s cnf 0 (s cnf 0) |
371 (369+2) s cnf 0 (s cnf 0) |
| assertion12_0_8.qpro | 44 (38+5) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (793+7) |
| assertion10_0_8.qpro | 158 (133+25) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| assertion1_0_8.qpro | 265 (205+60) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (793+7) |
| possibility5_0_8.qpro | 35 (31+4) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (795+5) |
| assertion4_0_8.qpro | 108 (89+19) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (796+4) |
| assertion7_0_8.qpro | 18 (17+1) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (793+7) |
| assertion3_0_8.qpro | 800 (626+174) | 800 (800+1) | 800 (793+7) |
| assertion2_0_8.qpro | 20 (19+1) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (794+6) |
| possibility9_0_8.qpro | 156 (123+33) s cnf 0 (s cnf 0) |
800 (800+0) | 800 (794+6) |
| assertion8_0_8.qpro | 800 (653+147) | 800 (800+1) | 800 (793+7) |
| possibility12_0_8.qpro | 800 (634+166) | 800 (800+1) | 800 (793+7) |
| possibility8_0_8.qpro | 800 (712+88) | 800 (800+1) | 800 (793+7) |
| consistency_0_9.qpro | 19 (19+0) s cnf 1 (s cnf 1) |
800 (799+1) | 800 (794+6) |
| possibility1_0_9.qpro | 374 (316+58) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion11_0_9.qpro | 30 (28+3) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| possibility2_0_9.qpro | 342 (286+57) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| possibility4_0_9.qpro | 202 (164+38) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| possibility10_0_9.qpro | 67 (58+9) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion9_0_9.qpro | 398 (324+74) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| possibility3_0_9.qpro | 210 (180+30) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| assertion5_0_9.qpro | 35 (32+3) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| possibility11_0_9.qpro | 225 (196+30) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion6_0_9.qpro | 25 (24+2) s cnf 0 (s cnf 0) |
772 (771+1) s cnf 0 (s cnf 0) |
800 (794+6) |
| possibility7_0_9.qpro | 800 (609+191) | 800 (799+1) | 800 (795+5) |
| possibility6_0_9.qpro | 25 (24+1) s cnf 0 (s cnf 0) |
50 (50+1) s cnf 0 (s cnf 0) |
800 (796+4) |
| assertion10_0_9.qpro | 200 (164+36) s cnf 0 (s cnf 0) |
800 (800+1) | 800 (794+6) |
| assertion12_0_9.qpro | 63 (58+5) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion1_0_9.qpro | 382 (300+82) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| possibility5_0_9.qpro | 49 (43+6) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+6) |
| assertion4_0_9.qpro | 174 (138+36) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion7_0_9.qpro | 23 (23+0) s cnf 0 (s cnf 0) |
744 (744+1) s cnf 0 (s cnf 0) |
800 (794+6) |
| assertion3_0_9.qpro | 800 (633+168) | 800 (799+1) | 800 (794+6) |
| assertion2_0_9.qpro | 27 (25+2) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| possibility9_0_9.qpro | 249 (201+48) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion8_0_9.qpro | 800 (628+172) | 800 (799+1) | 800 (794+6) |
| possibility12_0_9.qpro | 800 (642+158) | 800 (799+1) | 800 (794+6) |
| possibility8_0_9.qpro | 800 (624+176) | 800 (799+1) | 800 (794+6) |
| consistency_0_10.qpro | 24 (24+0) s cnf 1 (s cnf 1) |
800 (799+1) | 800 (795+5) |
| possibility1_0_10.qpro | 494 (414+80) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion11_0_10.qpro | 37 (35+3) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| possibility2_0_10.qpro | 474 (397+77) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| possibility4_0_10.qpro | 258 (216+42) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| possibility10_0_10.qpro | 78 (70+8) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion9_0_10.qpro | 652 (529+123) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+6) |
| possibility3_0_10.qpro | 305 (275+30) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| assertion5_0_10.qpro | 44 (40+4) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| assertion6_0_10.qpro | 33 (31+2) s cnf 0 (s cnf 0) |
177 (176+1) s cnf 0 (s cnf 0) |
800 (795+5) |
| possibility11_0_10.qpro | 275 (231+44) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| assertion10_0_10.qpro | 350 (289+60) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion12_0_10.qpro | 92 (78+14) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| possibility7_0_10.qpro | 800 (628+172) | 800 (799+1) | 800 (796+4) |
| possibility6_0_10.qpro | 33 (31+2) s cnf 0 (s cnf 0) |
90 (89+1) s cnf 0 (s cnf 0) |
800 (797+4) |
| assertion1_0_10.qpro | 519 (405+113) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| possibility5_0_10.qpro | 62 (55+7) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (796+4) |
| assertion4_0_10.qpro | 243 (197+47) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (794+6) |
| assertion7_0_10.qpro | 33 (31+2) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+5) |
| assertion3_0_10.qpro | 800 (643+157) | 800 (799+1) | 800 (795+5) |
| assertion2_0_10.qpro | 34 (31+2) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (796+4) |
| possibility9_0_10.qpro | 215 (180+35) s cnf 0 (s cnf 0) |
800 (799+1) | 800 (795+6) |
| assertion8_0_10.qpro | 800 (680+120) | 800 (799+1) | 800 (795+5) |
| possibility12_0_10.qpro | 800 (661+139) | 800 (799+1) | 800 (795+5) |
| possibility8_0_10.qpro | 800 (645+155) | 800 (799+1) | 800 (795+5) |
| TOTAL | solved: 309 wins: 265 |
solved: 178 wins: 61 |
solved: 206 wins: 100 |
| RAReQS-NN | GhostQ | CirQit |