RSat v1.03<p>
22 groups, 251 instances, 2-hour cutoff<p>
Instances solved: 130 (66 SAT + 64 UNSAT)<br>
Time: 976986 seconds / 271.38 hours / 11.31 days<br>
Time on solved instances: 105786 seconds (41721 SAT + 64065 UNSAT)<p>
Instances solved in 10 minutes: 96 (9406 seconds)<br>
Instances solved in 15 minutes: 100 (12012 seconds)<br>
Instances solved in 20 minutes: 102 (14068 seconds)<br>
Instances solved in 30 minutes: 110 (26142 seconds)<br>
Instances solved in 60 minutes: 118 (46306 seconds)<br>
Instances solved in 90 minutes: 126 (80784 seconds)<br>
<p>Instances solved and time on solved instances by group:<p><table border=0>
<tr><td>dlx_iq_unsat_1.0</td><td width=20></td><td>12</td><td>/</td><td>32</td><td width=20></td><td>46467.99178</td></tr>
<tr><td>engine_unsat_1.0</td><td width=20></td><td>7</td><td>/</td><td>10</td><td width=20></td><td>1854.903</td></tr>
<tr><td>fvp-sat.3.0</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>5282.60691</td></tr>
<tr><td>fvp-unsat.1.0</td><td width=20></td><td>4</td><td>/</td><td>4</td><td width=20></td><td>378.80642</td></tr>
<tr><td>fvp-unsat.2.0</td><td width=20></td><td>20</td><td>/</td><td>22</td><td width=20></td><td>11354.74382</td></tr>
<tr><td>fvp-unsat.3.0</td><td width=20></td><td>0</td><td>/</td><td>6</td><td width=20></td><td>0</td></tr>
<tr><td>liveness_sat_1.0</td><td width=20></td><td>5</td><td>/</td><td>10</td><td width=20></td><td>4024.10223</td></tr>
<tr><td>liveness_unsat_1.0</td><td width=20></td><td>3</td><td>/</td><td>12</td><td width=20></td><td>490.62842</td></tr>
<tr><td>liveness_unsat_2.0</td><td width=20></td><td>3</td><td>/</td><td>9</td><td width=20></td><td>340.60722</td></tr>
<tr><td>npe-1.0</td><td width=20></td><td>4</td><td>/</td><td>6</td><td width=20></td><td>1236.45303</td></tr>
<tr><td>pipe_ooo_unsat_1.0</td><td width=20></td><td>4</td><td>/</td><td>15</td><td width=20></td><td>720.15651</td></tr>
<tr><td>pipe_ooo_unsat_1.1</td><td width=20></td><td>3</td><td>/</td><td>14</td><td width=20></td><td>1957.59939</td></tr>
<tr><td>pipe_sat_1.0</td><td width=20></td><td>9</td><td>/</td><td>10</td><td width=20></td><td>17342.1526</td></tr>
<tr><td>pipe_sat_1.1</td><td width=20></td><td>10</td><td>/</td><td>10</td><td width=20></td><td>2123.45819</td></tr>
<tr><td>pipe_unsat_1.0</td><td width=20></td><td>5</td><td>/</td><td>13</td><td width=20></td><td>5463.54641</td></tr>
<tr><td>pipe_unsat_1.1</td><td width=20></td><td>5</td><td>/</td><td>14</td><td width=20></td><td>2696.3241</td></tr>
<tr><td>vliw_sat_2.0</td><td width=20></td><td>5</td><td>/</td><td>9</td><td width=20></td><td>2735.09421</td></tr>
<tr><td>vliw_sat_2.1</td><td width=20></td><td>1</td><td>/</td><td>10</td><td width=20></td><td>31.16626</td></tr>
<tr><td>vliw_sat_4.0</td><td width=20></td><td>10</td><td>/</td><td>10</td><td width=20></td><td>1285.2696</td></tr>
<tr><td>vliw_unsat_2.0</td><td width=20></td><td>0</td><td>/</td><td>9</td><td width=20></td><td>0</td></tr>
<tr><td>vliw_unsat_3.0</td><td width=20></td><td>0</td><td>/</td><td>2</td><td width=20></td><td>0</td></tr>
<tr><td>vliw_unsat_4.0</td><td width=20></td><td>0</td><td>/</td><td>4</td><td width=20></td><td>0</td></tr>
</table>
<p>

dlx_iq_unsat_1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>1dlx_c_iq42_a.cnf</td><td>UNSAT</td><td>21</td><td>15334368</td><td>1202960</td><td>5790.14976</td></tr>
<tr><td>1dlx_c_iq43_a.cnf</td><td>UNSAT</td><td>20</td><td>11948989</td><td>900356</td><td>4007.39978</td></tr>
<tr><td>1dlx_c_iq44_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq45_a.cnf</td><td>UNSAT</td><td>20</td><td>12672753</td><td>970680</td><td>4714.58827</td></tr>
<tr><td>1dlx_c_iq46_a.cnf</td><td>UNSAT</td><td>20</td><td>11778962</td><td>901286</td><td>5313.49522</td></tr>
<tr><td>1dlx_c_iq47_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq48_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq49_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq50_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq51_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq33_a.cnf</td><td>UNSAT</td><td>20</td><td>6958506</td><td>769607</td><td>2368.56092</td></tr>
<tr><td>1dlx_c_iq52_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq53_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq54_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq55_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq56_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq57_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq58_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq59_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq60_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq61_a.cnf</td><td>SAT</td><td>16</td><td>3913319</td><td>166060</td><td>1693.10161</td></tr>
<tr><td>1dlx_c_iq34_a.cnf</td><td>UNSAT</td><td>20</td><td>7302949</td><td>774653</td><td>2803.65078</td></tr>
<tr><td>1dlx_c_iq62_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq63_a.cnf</td><td>SAT</td><td>19</td><td>15122426</td><td>550077</td><td>5916.59354</td></tr>
<tr><td>1dlx_c_iq64_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq35_a.cnf</td><td>UNSAT</td><td>20</td><td>7101995</td><td>701869</td><td>2555.48251</td></tr>
<tr><td>1dlx_c_iq36_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq37_a.cnf</td></td></tr>
<tr><td>1dlx_c_iq38_a.cnf</td><td>UNSAT</td><td>20</td><td>8673565</td><td>784476</td><td>3364.76348</td></tr>
<tr><td>1dlx_c_iq39_a.cnf</td><td>UNSAT</td><td>20</td><td>9679165</td><td>904425</td><td>3868.70687</td></tr>
<tr><td>1dlx_c_iq40_a.cnf</td><td>UNSAT</td><td>20</td><td>11101447</td><td>946426</td><td>4071.49904</td></tr>
<tr><td>1dlx_c_iq41_a.cnf</td></td></tr>
<tr><td>Total (12 / 32)</td><td></td><td>236</td><td>121588444</td><td>9572875</td><td>46467.99178</td></tr></table><p>
engine_unsat_1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>engine_4.cnf</td><td>UNSAT</td><td>12</td><td>64416</td><td>33747</td><td>17.46634</td></tr>
<tr><td>engine_4_nd.cnf</td><td>UNSAT</td><td>15</td><td>157791</td><td>102990</td><td>73.00290</td></tr>
<tr><td>engine_5.cnf</td><td>UNSAT</td><td>19</td><td>939845</td><td>608824</td><td>1252.95352</td></tr>
<tr><td>engine_5_case1.cnf</td><td>UNSAT</td><td>10</td><td>31629</td><td>14621</td><td>9.91949</td></tr>
<tr><td>engine_5_nd.cnf</td></td></tr>
<tr><td>engine_5_nd_case1.cnf</td><td>UNSAT</td><td>13</td><td>87964</td><td>42690</td><td>36.14650</td></tr>
<tr><td>engine_6.cnf</td></td></tr>
<tr><td>engine_6_case1.cnf</td><td>UNSAT</td><td>13</td><td>120874</td><td>52612</td><td>82.03053</td></tr>
<tr><td>engine_6_nd.cnf</td></td></tr>
<tr><td>engine_6_nd_case1.cnf</td><td>UNSAT</td><td>16</td><td>360916</td><td>186275</td><td>383.38372</td></tr>
<tr><td>Total (7 / 10)</td><td></td><td>98</td><td>1763435</td><td>1041759</td><td>1854.903</td></tr></table><p>
fvp-sat.3.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>pipe_64_4_bug01.cnf</td><td>SAT</td><td>2</td><td>53625</td><td>284</td><td>1.29580</td></tr>
<tr><td>pipe_64_4_bug02.cnf</td><td>SAT</td><td>21</td><td>5366443</td><td>1087818</td><td>911.78539</td></tr>
<tr><td>pipe_64_4_bug03.cnf</td><td>SAT</td><td>0</td><td>12351</td><td>6</td><td>0.90486</td></tr>
<tr><td>pipe_64_4_bug04.cnf</td><td>SAT</td><td>11</td><td>285579</td><td>17608</td><td>7.47386</td></tr>
<tr><td>pipe_64_4_bug05.cnf</td><td>SAT</td><td>16</td><td>1303769</td><td>194554</td><td>91.24913</td></tr>
<tr><td>pipe_64_4_bug06.cnf</td><td>SAT</td><td>8</td><td>163323</td><td>5969</td><td>3.59945</td></tr>
<tr><td>pipe_64_4_bug07.cnf</td><td>SAT</td><td>13</td><td>436708</td><td>54703</td><td>20.15793</td></tr>
<tr><td>pipe_64_4_bug08.cnf</td><td>SAT</td><td>5</td><td>149430</td><td>1564</td><td>1.73974</td></tr>
<tr><td>pipe_64_4_bug09.cnf</td><td>SAT</td><td>3</td><td>67942</td><td>516</td><td>1.43778</td></tr>
<tr><td>pipe_64_4_bug10.cnf</td><td>SAT</td><td>3</td><td>87721</td><td>551</td><td>1.57076</td></tr>
<tr><td>pipe_64_4_bug11.cnf</td><td>SAT</td><td>17</td><td>1216305</td><td>226121</td><td>108.33653</td></tr>
<tr><td>pipe_64_4_bug12.cnf</td><td>SAT</td><td>9</td><td>164394</td><td>9513</td><td>4.62130</td></tr>
<tr><td>pipe_64_4_bug13.cnf</td><td>SAT</td><td>6</td><td>171654</td><td>2594</td><td>2.70859</td></tr>
<tr><td>pipe_64_4_bug14.cnf</td><td>SAT</td><td>14</td><td>715451</td><td>81986</td><td>34.44576</td></tr>
<tr><td>pipe_64_4_bug15.cnf</td><td>SAT</td><td>8</td><td>136934</td><td>5703</td><td>3.25251</td></tr>
<tr><td>pipe_64_4_bug16.cnf</td><td>SAT</td><td>20</td><td>4362417</td><td>792097</td><td>581.92353</td></tr>
<tr><td>pipe_64_4_bug17.cnf</td><td>SAT</td><td>10</td><td>186625</td><td>11443</td><td>5.31019</td></tr>
<tr><td>pipe_64_4_bug18.cnf</td><td>SAT</td><td>19</td><td>3242463</td><td>561737</td><td>347.38019</td></tr>
<tr><td>pipe_64_4_bug19.cnf</td><td>SAT</td><td>22</td><td>9322134</td><td>1611765</td><td>1550.47729</td></tr>
<tr><td>pipe_64_4_bug20.cnf</td><td>SAT</td><td>22</td><td>8732631</td><td>1545545</td><td>1602.93632</td></tr>
<tr><td>Total (20 / 20)</td><td></td><td>229</td><td>36177899</td><td>6212077</td><td>5282.60691</td></tr></table><p>
fvp-unsat.1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>1dlx_c_mc_ex_bp_f.cnf</td><td>UNSAT</td><td>4</td><td>3481</td><td>949</td><td>0.03000</td></tr>
<tr><td>2dlx_ca_mc_ex_bp_f.cnf</td><td>UNSAT</td><td>11</td><td>67679</td><td>24631</td><td>3.47447</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f.cnf</td><td>UNSAT</td><td>11</td><td>71126</td><td>22921</td><td>4.03539</td></tr>
<tr><td>9vliw_bp_mc.cnf</td><td>UNSAT</td><td>19</td><td>2641033</td><td>607892</td><td>371.26656</td></tr>
<tr><td>Total (4 / 4)</td><td></td><td>45</td><td>2783319</td><td>656393</td><td>378.80642</td></tr></table><p>
fvp-unsat.2.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>2pipe.cnf</td><td>UNSAT</td><td>7</td><td>14144</td><td>4897</td><td>0.21197</td></tr>
<tr><td>2pipe_1_ooo.cnf</td><td>UNSAT</td><td>8</td><td>13028</td><td>5666</td><td>0.23896</td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>UNSAT</td><td>8</td><td>13986</td><td>5600</td><td>0.29196</td></tr>
<tr><td>3pipe.cnf</td><td>UNSAT</td><td>13</td><td>137622</td><td>57076</td><td>8.63269</td></tr>
<tr><td>3pipe_1_ooo.cnf</td><td>UNSAT</td><td>12</td><td>75972</td><td>32136</td><td>4.12137</td></tr>
<tr><td>3pipe_2_ooo.cnf</td><td>UNSAT</td><td>13</td><td>119252</td><td>51394</td><td>8.66768</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>UNSAT</td><td>14</td><td>153659</td><td>62037</td><td>14.03587</td></tr>
<tr><td>4pipe.cnf</td><td>UNSAT</td><td>21</td><td>2978662</td><td>1078768</td><td>627.96853</td></tr>
<tr><td>4pipe_1_ooo.cnf</td><td>UNSAT</td><td>14</td><td>188806</td><td>60598</td><td>16.85244</td></tr>
<tr><td>4pipe_2_ooo.cnf</td><td>UNSAT</td><td>17</td><td>614272</td><td>244732</td><td>97.84712</td></tr>
<tr><td>4pipe_3_ooo.cnf</td><td>UNSAT</td><td>19</td><td>1481523</td><td>576688</td><td>396.90166</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>UNSAT</td><td>16</td><td>562979</td><td>191007</td><td>99.41289</td></tr>
<tr><td>5pipe.cnf</td><td>UNSAT</td><td>16</td><td>751896</td><td>174801</td><td>89.15845</td></tr>
<tr><td>5pipe_1_ooo.cnf</td><td>UNSAT</td><td>22</td><td>5176820</td><td>1979611</td><td>4401.82482</td></tr>
<tr><td>5pipe_2_ooo.cnf</td><td>UNSAT</td><td>18</td><td>1286133</td><td>420679</td><td>639.72175</td></tr>
<tr><td>5pipe_3_ooo.cnf</td><td>UNSAT</td><td>17</td><td>883898</td><td>224490</td><td>144.88397</td></tr>
<tr><td>5pipe_4_ooo.cnf</td><td>UNSAT</td><td>21</td><td>3268698</td><td>1227004</td><td>1494.10786</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>UNSAT</td><td>20</td><td>2525134</td><td>828659</td><td>1396.05177</td></tr>
<tr><td>6pipe.cnf</td></td></tr>
<tr><td>6pipe_6_ooo.cnf</td><td>UNSAT</td><td>20</td><td>3376322</td><td>887200</td><td>1782.50302</td></tr>
<tr><td>7pipe.cnf</td></td></tr>
<tr><td>7pipe_bug.cnf</td><td>SAT</td><td>16</td><td>790494</td><td>187053</td><td>131.30904</td></tr>
<tr><td>Total (20 / 22)</td><td></td><td>312</td><td>24413300</td><td>8300096</td><td>11354.74382</td></tr></table><p>
fvp-unsat.3.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>pipe_64_01.cnf</td></td></tr>
<tr><td>pipe_64_02.cnf</td></td></tr>
<tr><td>pipe_64_04.cnf</td></td></tr>
<tr><td>pipe_64_08.cnf</td></td></tr>
<tr><td>pipe_64_16.cnf</td></td></tr>
<tr><td>pipe_64_32.cnf</td></td></tr>
<tr><td>Total (0 / 6)</td><td></td><td></td><td></td><td></td><td>0</td></tr></table><p>
liveness_sat_1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug5_liveness.cnf</td><td>SAT</td><td>13</td><td>684648</td><td>48846</td><td>330.26679</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug6_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug7_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug8_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug9_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug10_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug1_liveness.cnf</td><td>SAT</td><td>11</td><td>320072</td><td>19885</td><td>112.98582</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug2_liveness.cnf</td><td>SAT</td><td>12</td><td>501994</td><td>35402</td><td>162.97322</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug3_liveness.cnf</td><td>SAT</td><td>11</td><td>346968</td><td>25582</td><td>155.05443</td></tr>
<tr><td>2dlx_cc_ex_bp_f_bug4_liveness.cnf</td><td>SAT</td><td>19</td><td>2915307</td><td>528838</td><td>3262.82197</td></tr>
<tr><td>Total (5 / 10)</td><td></td><td>66</td><td>4768989</td><td>658553</td><td>4024.10223</td></tr></table><p>
liveness_unsat_1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>1dlx_c_bp_f_liveness.cnf</td><td>UNSAT</td><td>18</td><td>768282</td><td>370687</td><td>370.06574</td></tr>
<tr><td>1dlx_c_ex_bp_f_liveness.cnf</td></td></tr>
<tr><td>1dlx_c_ex_liveness.cnf</td><td>UNSAT</td><td>15</td><td>325792</td><td>121054</td><td>100.01480</td></tr>
<tr><td>1dlx_c_liveness.cnf</td><td>UNSAT</td><td>14</td><td>159682</td><td>59315</td><td>20.54788</td></tr>
<tr><td>2dlx_ca_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_ex_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_ex_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_liveness.cnf</td></td></tr>
<tr><td>Total (3 / 12)</td><td></td><td>47</td><td>1253756</td><td>551056</td><td>490.62842</td></tr></table><p>
liveness_unsat_2.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>1dlx_c_bp_u_f_liveness.cnf</td><td>UNSAT</td><td>13</td><td>110599</td><td>40376</td><td>12.98203</td></tr>
<tr><td>1dlx_c_ex_bp_u_f_liveness.cnf</td><td>UNSAT</td><td>15</td><td>297956</td><td>106209</td><td>73.85877</td></tr>
<tr><td>1dlx_c_ex_d_liveness.cnf</td><td>UNSAT</td><td>17</td><td>541056</td><td>220088</td><td>253.76642</td></tr>
<tr><td>2dlx_ca_bp_u_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_ex_bp_u_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_ca_ex_d_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_bp_u_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_bp_u_f_liveness.cnf</td></td></tr>
<tr><td>2dlx_cc_ex_d_liveness.cnf</td></td></tr>
<tr><td>Total (3 / 9)</td><td></td><td>45</td><td>949611</td><td>366673</td><td>340.60722</td></tr></table><p>
npe-1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>1dlx_c_bug_no_pe.cnf</td><td>SAT</td><td>5</td><td>9447</td><td>1444</td><td>0.19197</td></tr>
<tr><td>1dlx_c_no_pe.cnf</td><td>UNSAT</td><td>17</td><td>371439</td><td>200476</td><td>80.31179</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_bug044_no_pe.cnf</td><td>SAT</td><td>7</td><td>199609</td><td>3899</td><td>11.20830</td></tr>
<tr><td>2dlx_cc_mc_ex_bp_f2_no_pe.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_bug071_no_pe.cnf</td><td>SAT</td><td>15</td><td>8355389</td><td>91724</td><td>1144.74097</td></tr>
<tr><td>9dlx_vliw_at_bp_mc2_no_pe.cnf</td></td></tr>
<tr><td>Total (4 / 6)</td><td></td><td>44</td><td>8935884</td><td>297543</td><td>1236.45303</td></tr></table><p>
pipe_ooo_unsat_1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>10pipe_10_ooo.cnf</td></td></tr>
<tr><td>11pipe_11_ooo.cnf</td></td></tr>
<tr><td>12pipe_12_ooo.cnf</td></td></tr>
<tr><td>13pipe_13_ooo.cnf</td></td></tr>
<tr><td>14pipe_14_ooo.cnf</td></td></tr>
<tr><td>15pipe_15_ooo.cnf</td></td></tr>
<tr><td>16pipe_16_ooo.cnf</td></td></tr>
<tr><td>2pipe_2_ooo.cnf</td><td>UNSAT</td><td>7</td><td>10682</td><td>4070</td><td>0.17497</td></tr>
<tr><td>3pipe_3_ooo.cnf</td><td>UNSAT</td><td>14</td><td>167696</td><td>59566</td><td>11.03432</td></tr>
<tr><td>4pipe_4_ooo.cnf</td><td>UNSAT</td><td>19</td><td>1412227</td><td>559934</td><td>329.72487</td></tr>
<tr><td>5pipe_5_ooo.cnf</td><td>UNSAT</td><td>19</td><td>1732835</td><td>462607</td><td>379.22235</td></tr>
<tr><td>6pipe_6_ooo.cnf</td></td></tr>
<tr><td>7pipe_7_ooo.cnf</td></td></tr>
<tr><td>8pipe_8_ooo.cnf</td></td></tr>
<tr><td>9pipe_9_ooo.cnf</td></td></tr>
<tr><td>Total (4 / 15)</td><td></td><td>59</td><td>3323440</td><td>1086177</td><td>720.15651</td></tr></table><p>
pipe_ooo_unsat_1.1
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>10pipe_10_ooo_q0_T0.cnf</td></td></tr>
<tr><td>11pipe_11_ooo_q0_T0.cnf</td></td></tr>
<tr><td>12pipe_12_ooo_q0_T0.cnf</td></td></tr>
<tr><td>13pipe_13_ooo_q0_T0.cnf</td></td></tr>
<tr><td>14pipe_14_ooo_q0_T0.cnf</td></td></tr>
<tr><td>15pipe_15_ooo_q0_T0.cnf</td></td></tr>
<tr><td>2pipe_2_ooo_q0_T0.cnf</td><td>UNSAT</td><td>6</td><td>7803</td><td>2755</td><td>0.09998</td></tr>
<tr><td>3pipe_3_ooo_q0_T0.cnf</td><td>UNSAT</td><td>17</td><td>600318</td><td>283902</td><td>67.95667</td></tr>
<tr><td>4pipe_4_ooo_q0_T0.cnf</td><td>UNSAT</td><td>23</td><td>6368415</td><td>2815531</td><td>1889.54274</td></tr>
<tr><td>5pipe_5_ooo_q0_T0.cnf</td></td></tr>
<tr><td>6pipe_6_ooo_q0_T0.cnf</td></td></tr>
<tr><td>7pipe_7_ooo_q0_T0.cnf</td></td></tr>
<tr><td>8pipe_8_ooo_q0_T0.cnf</td></td></tr>
<tr><td>9pipe_9_ooo_q0_T0.cnf</td></td></tr>
<tr><td>Total (3 / 14)</td><td></td><td>46</td><td>6976536</td><td>3102188</td><td>1957.59939</td></tr></table><p>
pipe_sat_1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>12pipe_bug1.cnf</td><td>SAT</td><td>8</td><td>115741</td><td>6036</td><td>33.25294</td></tr>
<tr><td>12pipe_bug10.cnf</td><td>SAT</td><td>22</td><td>11556386</td><td>2225228</td><td>6508.56255</td></tr>
<tr><td>12pipe_bug2.cnf</td><td>SAT</td><td>3</td><td>46844</td><td>686</td><td>12.13016</td></tr>
<tr><td>12pipe_bug3.cnf</td><td>SAT</td><td>7</td><td>90818</td><td>3373</td><td>24.01135</td></tr>
<tr><td>12pipe_bug4.cnf</td><td>SAT</td><td>22</td><td>7847342</td><td>1553151</td><td>3800.08930</td></tr>
<tr><td>12pipe_bug5.cnf</td></td></tr>
<tr><td>12pipe_bug6.cnf</td><td>SAT</td><td>7</td><td>99440</td><td>3299</td><td>19.56703</td></tr>
<tr><td>12pipe_bug7.cnf</td><td>SAT</td><td>13</td><td>370125</td><td>39601</td><td>100.41673</td></tr>
<tr><td>12pipe_bug8.cnf</td><td>SAT</td><td>11</td><td>232043</td><td>18864</td><td>57.36528</td></tr>
<tr><td>12pipe_bug9.cnf</td><td>SAT</td><td>22</td><td>7501102</td><td>2117899</td><td>6786.75726</td></tr>
<tr><td>Total (9 / 10)</td><td></td><td>115</td><td>27859841</td><td>5968137</td><td>17342.1526</td></tr></table><p>
pipe_sat_1.1
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>12pipe_bug10_q0.cnf</td><td>SAT</td><td>3</td><td>63590</td><td>586</td><td>6.10307</td></tr>
<tr><td>12pipe_bug1_q0.cnf</td><td>SAT</td><td>13</td><td>614686</td><td>43523</td><td>122.93631</td></tr>
<tr><td>12pipe_bug2_q0.cnf</td><td>SAT</td><td>1</td><td>66647</td><td>253</td><td>6.34703</td></tr>
<tr><td>12pipe_bug3_q0.cnf</td><td>SAT</td><td>13</td><td>582952</td><td>43013</td><td>127.23766</td></tr>
<tr><td>12pipe_bug4_q0.cnf</td><td>SAT</td><td>6</td><td>123503</td><td>2616</td><td>10.84935</td></tr>
<tr><td>12pipe_bug5_q0.cnf</td><td>SAT</td><td>9</td><td>155810</td><td>7925</td><td>21.93367</td></tr>
<tr><td>12pipe_bug6_q0.cnf</td><td>SAT</td><td>8</td><td>155364</td><td>7029</td><td>20.92382</td></tr>
<tr><td>12pipe_bug7_q0.cnf</td><td>SAT</td><td>16</td><td>1961666</td><td>184972</td><td>498.54721</td></tr>
<tr><td>12pipe_bug8_q0.cnf</td><td>SAT</td><td>19</td><td>4702413</td><td>532705</td><td>1301.26118</td></tr>
<tr><td>12pipe_bug9_q0.cnf</td><td>SAT</td><td>4</td><td>104203</td><td>856</td><td>7.31889</td></tr>
<tr><td>Total (10 / 10)</td><td></td><td>92</td><td>8530834</td><td>823478</td><td>2123.45819</td></tr></table><p>
pipe_unsat_1.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>02pipe_k.cnf</td><td>UNSAT</td><td>6</td><td>9442</td><td>3200</td><td>0.10998</td></tr>
<tr><td>03pipe_k.cnf</td><td>UNSAT</td><td>13</td><td>106398</td><td>41220</td><td>5.43417</td></tr>
<tr><td>04pipe_k.cnf</td><td>UNSAT</td><td>20</td><td>2188388</td><td>847206</td><td>539.51198</td></tr>
<tr><td>05pipe_k.cnf</td><td>UNSAT</td><td>24</td><td>9804437</td><td>3379414</td><td>4299.87732</td></tr>
<tr><td>06pipe_k.cnf</td><td>UNSAT</td><td>19</td><td>3160183</td><td>582350</td><td>618.61296</td></tr>
<tr><td>07pipe_k.cnf</td></td></tr>
<tr><td>08pipe_k.cnf</td></td></tr>
<tr><td>09pipe_k.cnf</td></td></tr>
<tr><td>10pipe_k.cnf</td></td></tr>
<tr><td>11pipe_k.cnf</td></td></tr>
<tr><td>12pipe_k.cnf</td></td></tr>
<tr><td>13pipe_k.cnf</td></td></tr>
<tr><td>14pipe_k.cnf</td></td></tr>
<tr><td>Total (5 / 13)</td><td></td><td>82</td><td>15268848</td><td>4853390</td><td>5463.54641</td></tr></table><p>
pipe_unsat_1.1
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>02pipe_q0_k.cnf</td><td>UNSAT</td><td>7</td><td>9864</td><td>4070</td><td>0.13898</td></tr>
<tr><td>03pipe_q0_k.cnf</td><td>UNSAT</td><td>12</td><td>85234</td><td>31541</td><td>3.81242</td></tr>
<tr><td>04pipe_q0_k.cnf</td><td>UNSAT</td><td>18</td><td>1203739</td><td>438675</td><td>158.82085</td></tr>
<tr><td>05pipe_q0_k.cnf</td><td>UNSAT</td><td>22</td><td>5417683</td><td>2152717</td><td>2067.08376</td></tr>
<tr><td>06pipe_q0_k.cnf</td><td>UNSAT</td><td>19</td><td>2386675</td><td>519933</td><td>466.46809</td></tr>
<tr><td>07pipe_q0_k.cnf</td></td></tr>
<tr><td>08pipe_q0_k.cnf</td></td></tr>
<tr><td>09pipe_q0_k.cnf</td></td></tr>
<tr><td>10pipe_q0_k.cnf</td></td></tr>
<tr><td>11pipe_q0_k.cnf</td></td></tr>
<tr><td>12pipe_q0_k.cnf</td></td></tr>
<tr><td>13pipe_q0_k.cnf</td></td></tr>
<tr><td>14pipe_q0_k.cnf</td></td></tr>
<tr><td>15pipe_q0_k.cnf</td></td></tr>
<tr><td>Total (5 / 14)</td><td></td><td>78</td><td>9103195</td><td>3146936</td><td>2696.3241</td></tr></table><p>
vliw_sat_2.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug1.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug2.cnf</td><td>SAT</td><td>5</td><td>912406</td><td>1476</td><td>17.25738</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug3.cnf</td><td>SAT</td><td>20</td><td>7981163</td><td>724504</td><td>1852.33040</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug4.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug5.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug6.cnf</td><td>SAT</td><td>12</td><td>2097506</td><td>33759</td><td>97.36020</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug7.cnf</td><td>SAT</td><td>12</td><td>1158682</td><td>27142</td><td>48.36765</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug8.cnf</td><td>SAT</td><td>18</td><td>4905830</td><td>352480</td><td>719.77858</td></tr>
<tr><td>9dlx_vliw_at_b_iq6_bug9.cnf</td></td></tr>
<tr><td>Total (5 / 9)</td><td></td><td>67</td><td>17055587</td><td>1139361</td><td>2735.09421</td></tr></table><p>
vliw_sat_2.1
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug1.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug10.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug2.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug3.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug4.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug5.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug6.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug7.cnf</td><td>SAT</td><td>4</td><td>992555</td><td>1226</td><td>31.16626</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug8.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_bug9.cnf</td></td></tr>
<tr><td>Total (1 / 10)</td><td></td><td>4</td><td>992555</td><td>1226</td><td>31.16626</td></tr></table><p>
vliw_sat_4.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug1.cnf</td><td>SAT</td><td>9</td><td>2146499</td><td>10779</td><td>121.47553</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug10.cnf</td><td>SAT</td><td>7</td><td>1665462</td><td>3529</td><td>64.93213</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug2.cnf</td><td>SAT</td><td>6</td><td>1654946</td><td>2613</td><td>65.89998</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug3.cnf</td><td>SAT</td><td>6</td><td>1571661</td><td>2884</td><td>44.35726</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug4.cnf</td><td>SAT</td><td>15</td><td>4855587</td><td>98874</td><td>372.42738</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug5.cnf</td><td>SAT</td><td>12</td><td>2453321</td><td>31233</td><td>209.17320</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug6.cnf</td><td>SAT</td><td>11</td><td>3281376</td><td>19492</td><td>142.00441</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug7.cnf</td><td>SAT</td><td>7</td><td>1448138</td><td>3531</td><td>63.85429</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug8.cnf</td><td>SAT</td><td>10</td><td>2399192</td><td>16302</td><td>114.74056</td></tr>
<tr><td>9vliw_m_9stages_iq3_C1_bug9.cnf</td><td>SAT</td><td>9</td><td>1761107</td><td>7928</td><td>86.40486</td></tr>
<tr><td>Total (10 / 10)</td><td></td><td>92</td><td>23237289</td><td>197165</td><td>1285.2696</td></tr></table><p>
vliw_unsat_2.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>9dlx_vliw_at_b_iq1.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq2.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq3.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq4.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq5.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq6.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq7.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq9.cnf</td></td></tr>
<tr><td>Total (0 / 9)</td><td></td><td></td><td></td><td></td><td>0</td></tr></table><p>
vliw_unsat_3.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24.cnf</td></td></tr>
<tr><td>9dlx_vliw_at_b_iq8_I3_C24_D.cnf</td></td></tr>
<tr><td>Total (0 / 2)</td><td></td><td></td><td></td><td></td><td>0</td></tr></table><p>
vliw_unsat_4.0
<table border=1><tr><td>CNF</td><td>Sol</td><td>Restarts</td><td>Decisions</td><td>Conflicts</td><td>Time</td></tr>
<tr><td>9vliw_m_9stages_C1.cnf</td></td></tr>
<tr><td>9vliw_m_9stages_iq1_C1.cnf</td></td></tr>
<tr><td>9vliw_m_9stages_iq2_C1.cnf</td></td></tr>
<tr><td>9vliw_m_9stages_iq3_C1.cnf</td></td></tr>
<tr><td>Total (0 / 4)</td><td></td><td></td><td></td><td></td><td>0</td></tr></table><p>