MiniSat 1.14<p>
16 groups, 311 instances, 1-hour cutoff<p>
Instances solved: 280 (139 SAT + 141 UNSAT)<br>
Time: 189772 seconds / 52.71 hours / 2.20 days<br>
Time on solved instances: 78172 seconds (60182 SAT + 17990 UNSAT)<p>
Instances solved in 10 minutes: 238 (16557 seconds)<br>
Instances solved in 15 minutes: 253 (27970 seconds)<br>
Instances solved in 20 minutes: 257 (32231 seconds)<br>
Instances solved in 30 minutes: 268 (48764 seconds)<br>
Instances solved in 60 minutes: 280 (78172 seconds)<br>
<p>Instances solved and time on solved instances by group:<p><table border=0>
<tr><td>IBM_FV_2002_01_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>5106.62426</td></tr>
<tr><td>IBM_FV_2002_03_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>1459.725631</td></tr>
<tr><td>IBM_FV_2002_04_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>3507.353315</td></tr>
<tr><td>IBM_FV_2002_05_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>802.819154</td></tr>
<tr><td>IBM_FV_2002_06_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>1045.407246</td></tr>
<tr><td>IBM_FV_2002_07_rule</td><td width=20></td><td>17</td><td>/</td><td>20</td><td width=20></td><td>274.532143</td></tr>
<tr><td>IBM_FV_2002_09_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>3.012532</td></tr>
<tr><td>IBM_FV_2004_01</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>2116.242566</td></tr>
<tr><td>IBM_FV_2004_07</td><td width=20></td><td>18</td><td>/</td><td>19</td><td width=20></td><td>2450.23816</td></tr>
<tr><td>IBM_FV_2004_1_11</td><td width=20></td><td>15</td><td>/</td><td>19</td><td width=20></td><td>8205.681885</td></tr>
<tr><td>IBM_FV_2004_18</td><td width=20></td><td>14</td><td>/</td><td>19</td><td width=20></td><td>14789.068964</td></tr>
<tr><td>IBM_FV_2004_20</td><td width=20></td><td>13</td><td>/</td><td>19</td><td width=20></td><td>9854.017519</td></tr>
<tr><td>IBM_FV_2004_2_14</td><td width=20></td><td>18</td><td>/</td><td>19</td><td width=20></td><td>6504.375405</td></tr>
<tr><td>IBM_FV_2004_23</td><td width=20></td><td>11</td><td>/</td><td>19</td><td width=20></td><td>5994.683259</td></tr>
<tr><td>IBM_FV_2004_26</td><td width=20></td><td>17</td><td>/</td><td>19</td><td width=20></td><td>5402.984995</td></tr>
<tr><td>IBM_FV_2004_29</td><td width=20></td><td>18</td><td>/</td><td>19</td><td width=20></td><td>10655.36858</td></tr>
</table>
<p>

IBM_FV_2002_01_rule
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>15</td><td>86273</td><td>207538</td><td>30.9813</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>17</td><td>152999</td><td>366956</td><td>71.9701</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>19</td><td>297497</td><td>624730</td><td>304.665</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>19</td><td>349333</td><td>788811</td><td>322.374</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>19</td><td>324354</td><td>711368</td><td>253.048</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>20</td><td>494591</td><td>1041963</td><td>657.466</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>19</td><td>377763</td><td>893305</td><td>309.28</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>20</td><td>619203</td><td>1385450</td><td>763.844</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>20</td><td>530011</td><td>1166776</td><td>643.593</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>21</td><td>891805</td><td>1986635</td><td>1400.67</td><td>SAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>0</td><td>0</td><td>0</td><td>0.001999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>19</td><td>310009</td><td>737560</td><td>223.587</td><td>SAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>3</td><td>378</td><td>859</td><td>0.110983</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>7</td><td>2962</td><td>6763</td><td>0.598908</td><td>SAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>11</td><td>15774</td><td>36366</td><td>4.19436</td><td>SAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>10</td><td>10429</td><td>27850</td><td>2.55061</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>15</td><td>81017</td><td>177576</td><td>58.3691</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>14</td><td>42631</td><td>101120</td><td>12.995</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>15</td><td>77999</td><td>174050</td><td>32.816</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>14</td><td>51463</td><td>127189</td><td>13.5089</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>297</td><td>4716491</td><td>10562865</td><td>5106.62426</td><td></td></tr></table><p>
IBM_FV_2002_03_rule
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>0</td><td>0</td><td>0</td><td>0.000999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>0</td><td>0</td><td>0</td><td>0.025996</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>19</td><td>419079</td><td>1028595</td><td>294.821</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>0</td><td>0</td><td>0</td><td>0.043993</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>0</td><td>0</td><td>0</td><td>0.06499</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>0</td><td>0</td><td>0</td><td>0.074988</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>2</td><td>129</td><td>1046</td><td>0.160975</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>10</td><td>10346</td><td>35191</td><td>3.07153</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>9</td><td>6109</td><td>21301</td><td>1.54876</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>13</td><td>30939</td><td>92728</td><td>11.4233</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>13</td><td>36403</td><td>104037</td><td>10.4784</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>14</td><td>42284</td><td>123544</td><td>12.1102</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>16</td><td>94626</td><td>262238</td><td>39.167</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>16</td><td>108484</td><td>289985</td><td>48.7096</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>16</td><td>126401</td><td>343234</td><td>50.9343</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>16</td><td>117647</td><td>328747</td><td>48.6496</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>19</td><td>343812</td><td>824320</td><td>260.001</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>19</td><td>379394</td><td>913546</td><td>304.672</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>19</td><td>344142</td><td>859416</td><td>240.177</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>18</td><td>255316</td><td>684714</td><td>133.59</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>219</td><td>2315111</td><td>5912642</td><td>1459.725631</td><td></td></tr></table><p>
IBM_FV_2002_04_rule
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>0</td><td>0</td><td>0</td><td>0.000999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>0</td><td>0</td><td>0</td><td>0.032994</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>19</td><td>358267</td><td>1073859</td><td>682.134</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>1</td><td>12</td><td>65</td><td>0.06399</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>3</td><td>356</td><td>2089</td><td>0.179972</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>8</td><td>3474</td><td>15053</td><td>1.13683</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>9</td><td>7360</td><td>28435</td><td>2.58561</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>11</td><td>13054</td><td>56885</td><td>5.32419</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>12</td><td>18721</td><td>76198</td><td>8.38273</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>13</td><td>30263</td><td>123989</td><td>15.5586</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>14</td><td>42179</td><td>175839</td><td>26.087</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>15</td><td>60224</td><td>234683</td><td>47.2178</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>15</td><td>87061</td><td>312838</td><td>87.8826</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>16</td><td>119152</td><td>394887</td><td>149.665</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>17</td><td>186346</td><td>557979</td><td>276.222</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>18</td><td>197344</td><td>594192</td><td>270.706</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>18</td><td>250275</td><td>772178</td><td>364.275</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>18</td><td>269543</td><td>774781</td><td>371.775</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>19</td><td>308106</td><td>909704</td><td>461.487</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>19</td><td>388652</td><td>1058556</td><td>736.636</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>245</td><td>2340389</td><td>7162210</td><td>3507.353315</td><td></td></tr></table><p>
IBM_FV_2002_05_rule
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>1</td><td>2</td><td>1</td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>2</td><td>190</td><td>568</td><td>0.110983</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>16</td><td>122202</td><td>773565</td><td>140.111</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>4</td><td>527</td><td>1265</td><td>0.199969</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>5</td><td>991</td><td>2699</td><td>0.300954</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>6</td><td>1508</td><td>4142</td><td>0.427934</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>6</td><td>1563</td><td>4945</td><td>0.498924</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>10</td><td>7728</td><td>60223</td><td>4.51131</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>11</td><td>11465</td><td>81744</td><td>6.72498</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>12</td><td>19206</td><td>127796</td><td>12.6281</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>12</td><td>22738</td><td>163107</td><td>15.0777</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>14</td><td>48740</td><td>296547</td><td>31.8692</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>14</td><td>52825</td><td>305990</td><td>41.4477</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>15</td><td>77702</td><td>460671</td><td>56.5724</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>15</td><td>62066</td><td>383596</td><td>43.7394</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>15</td><td>65907</td><td>440881</td><td>49.9104</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>16</td><td>92703</td><td>553411</td><td>80.9147</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>14</td><td>53524</td><td>392211</td><td>52.909</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>17</td><td>152039</td><td>834162</td><td>182.581</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>16</td><td>96791</td><td>679541</td><td>82.2835</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>221</td><td>890417</td><td>5567065</td><td>802.819154</td><td></td></tr></table><p>
IBM_FV_2002_06_rule
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>18</td><td>264282</td><td>693675</td><td>183.307</td><td>SAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>0</td><td>0</td><td>0</td><td>0.000999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>0</td><td>0</td><td>0</td><td>0.041993</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>19</td><td>377287</td><td>888377</td><td>280.143</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>1</td><td>22</td><td>68</td><td>0.078987</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>4</td><td>579</td><td>2463</td><td>0.245962</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>6</td><td>1476</td><td>5363</td><td>0.819875</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>10</td><td>7566</td><td>26330</td><td>4.64429</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>10</td><td>8742</td><td>34153</td><td>4.90925</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>9</td><td>6906</td><td>31009</td><td>2.49862</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>13</td><td>31594</td><td>92865</td><td>15.0227</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>12</td><td>18920</td><td>65318</td><td>7.54985</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>10</td><td>10287</td><td>45075</td><td>4.43532</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>15</td><td>62156</td><td>184153</td><td>29.8595</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>14</td><td>46934</td><td>164685</td><td>21.3228</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>16</td><td>103221</td><td>280216</td><td>50.1474</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>17</td><td>156678</td><td>414892</td><td>103.519</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>17</td><td>180479</td><td>435163</td><td>122.287</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>15</td><td>68758</td><td>187624</td><td>28.3687</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>18</td><td>279699</td><td>668032</td><td>186.205</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>224</td><td>1625586</td><td>4219461</td><td>1045.407246</td><td></td></tr></table><p>
IBM_FV_2002_07_rule
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>6</td><td>1502</td><td>6666</td><td>0.039993</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>16</td><td>128057</td><td>761015</td><td>24.7312</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>13</td><td>25972</td><td>145230</td><td>5.06623</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>13</td><td>33588</td><td>226220</td><td>4.01739</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>14</td><td>42930</td><td>190032</td><td>6.29904</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>13</td><td>35731</td><td>181007</td><td>4.93125</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>14</td><td>47064</td><td>277595</td><td>7.00993</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>17</td><td>149095</td><td>561622</td><td>32.649</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>13</td><td>34591</td><td>253845</td><td>5.17621</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>17</td><td>131552</td><td>448924</td><td>29.4285</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>14</td><td>54047</td><td>296724</td><td>9.8285</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>17</td><td>144886</td><td>554037</td><td>36.0255</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td></td></tr>
<tr><td>SAT_dat.k65.cnf</td></td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>13</td><td>34823</td><td>158002</td><td>6.63099</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>13</td><td>33275</td><td>181481</td><td>5.29919</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>14</td><td>57991</td><td>295492</td><td>13.406</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>18</td><td>214798</td><td>740183</td><td>78.2321</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td></td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>13</td><td>31363</td><td>188308</td><td>5.76112</td><td>UNSAT</td></tr>
<tr><td>Total (17 / 20)</td><td>238</td><td>1201265</td><td>5466383</td><td>274.532143</td><td></td></tr></table><p>
IBM_FV_2002_09_rule
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>0</td><td>0</td><td>0</td><td>0.000999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>1</td><td>54</td><td>639</td><td>0.026995</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>2</td><td>182</td><td>7015</td><td>0.284956</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>1</td><td>59</td><td>1177</td><td>0.039993</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>3</td><td>263</td><td>2564</td><td>0.081987</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>2</td><td>164</td><td>3560</td><td>0.082987</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>3</td><td>347</td><td>3841</td><td>0.116982</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>3</td><td>293</td><td>3776</td><td>0.107983</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>2</td><td>220</td><td>3339</td><td>0.117982</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>2</td><td>118</td><td>1982</td><td>0.119981</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>2</td><td>199</td><td>4268</td><td>0.143978</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>2</td><td>224</td><td>4219</td><td>0.159975</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>2</td><td>115</td><td>2352</td><td>0.164974</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>2</td><td>201</td><td>3908</td><td>0.181972</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>2</td><td>146</td><td>5489</td><td>0.19397</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>2</td><td>134</td><td>2923</td><td>0.201969</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>2</td><td>156</td><td>4671</td><td>0.229965</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>2</td><td>194</td><td>5005</td><td>0.248962</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>2</td><td>155</td><td>2732</td><td>0.245962</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>2</td><td>133</td><td>3889</td><td>0.25996</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td>39</td><td>3357</td><td>67349</td><td>3.012532</td><td></td></tr></table><p>
IBM_FV_2004_01
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k50.cnf</td><td>14</td><td>47150</td><td>112112</td><td>18.0083</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k55.cnf</td><td>14</td><td>53593</td><td>146672</td><td>16.9324</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k60.cnf</td><td>16</td><td>103881</td><td>240084</td><td>42.4445</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k65.cnf</td><td>14</td><td>55342</td><td>145905</td><td>17.4274</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k70.cnf</td><td>17</td><td>172161</td><td>399180</td><td>88.0466</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k75.cnf</td><td>18</td><td>245963</td><td>571897</td><td>176.958</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k80.cnf</td><td>19</td><td>340623</td><td>768337</td><td>269.153</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k85.cnf</td><td>20</td><td>646651</td><td>1408821</td><td>772.393</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k90.cnf</td><td>18</td><td>270450</td><td>628375</td><td>180.593</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k95.cnf</td><td>18</td><td>290041</td><td>673799</td><td>213.19</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k10.cnf</td><td>2</td><td>244</td><td>434</td><td>0.06299</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k100.cnf</td><td>19</td><td>339226</td><td>772092</td><td>244.867</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k15.cnf</td><td>9</td><td>5382</td><td>10461</td><td>0.876866</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k20.cnf</td><td>12</td><td>17482</td><td>36405</td><td>4.72528</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k25.cnf</td><td>15</td><td>58512</td><td>114613</td><td>22.9895</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k30.cnf</td><td>12</td><td>24038</td><td>54647</td><td>6.596</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k35.cnf</td><td>13</td><td>35428</td><td>80642</td><td>9.60554</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k40.cnf</td><td>13</td><td>34359</td><td>82445</td><td>9.93349</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k45.cnf</td><td>14</td><td>55465</td><td>126354</td><td>21.4397</td><td>SAT</td></tr>
<tr><td>Total (19 / 19)</td><td>277</td><td>2795991</td><td>6373275</td><td>2116.242566</td><td></td></tr></table><p>
IBM_FV_2004_07
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k50.cnf</td><td>13</td><td>27293</td><td>166624</td><td>3.46647</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k55.cnf</td><td>13</td><td>34802</td><td>207967</td><td>5.30119</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k60.cnf</td><td>13</td><td>36084</td><td>173054</td><td>6.37403</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k65.cnf</td><td>14</td><td>42000</td><td>244019</td><td>7.29689</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k70.cnf</td><td>14</td><td>45520</td><td>271578</td><td>8.28474</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k75.cnf</td><td>15</td><td>59884</td><td>305199</td><td>13.6959</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k80.cnf</td><td>17</td><td>166071</td><td>495892</td><td>56.4184</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k85.cnf</td><td>13</td><td>29752</td><td>179354</td><td>5.2942</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k90.cnf</td><td>14</td><td>41850</td><td>285994</td><td>7.59584</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k95.cnf</td><td>15</td><td>70508</td><td>321098</td><td>19.1061</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k10.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k100.cnf</td><td>23</td><td>2150353</td><td>3927763</td><td>1737.51</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k15.cnf</td><td>22</td><td>1479858</td><td>2873179</td><td>530.144</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k20.cnf</td><td>14</td><td>46567</td><td>239012</td><td>6.96994</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k25.cnf</td><td>14</td><td>45635</td><td>252345</td><td>7.19191</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k30.cnf</td><td>15</td><td>67407</td><td>271102</td><td>14.8847</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k35.cnf</td><td>13</td><td>29725</td><td>201792</td><td>4.05938</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k40.cnf</td><td>14</td><td>48135</td><td>240334</td><td>8.46871</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k45.cnf</td><td>14</td><td>46603</td><td>247365</td><td>8.17576</td><td>UNSAT</td></tr>
<tr><td>Total (18 / 19)</td><td>270</td><td>4468047</td><td>10903671</td><td>2450.23816</td><td></td></tr></table><p>
IBM_FV_2004_1_11
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k10.cnf</td><td>3</td><td>309</td><td>2357</td><td>0.160975</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k100.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k15.cnf</td><td>6</td><td>1802</td><td>10933</td><td>1.13183</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k20.cnf</td><td>8</td><td>4151</td><td>20534</td><td>2.08668</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k25.cnf</td><td>12</td><td>20145</td><td>82280</td><td>16.0676</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k30.cnf</td><td>13</td><td>28659</td><td>117023</td><td>17.1994</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k35.cnf</td><td>15</td><td>71852</td><td>276400</td><td>63.3594</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k40.cnf</td><td>16</td><td>107498</td><td>423254</td><td>106.178</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k45.cnf</td><td>16</td><td>128562</td><td>505888</td><td>138.697</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k50.cnf</td><td>18</td><td>204090</td><td>752820</td><td>265.84</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k55.cnf</td><td>18</td><td>233009</td><td>883428</td><td>336.057</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k60.cnf</td><td>18</td><td>216576</td><td>839485</td><td>273.152</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k65.cnf</td><td>19</td><td>411945</td><td>1345072</td><td>897.372</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k70.cnf</td><td>21</td><td>667579</td><td>2049688</td><td>1699.81</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k75.cnf</td><td>21</td><td>684715</td><td>2148631</td><td>1887.92</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k80.cnf</td><td>21</td><td>841873</td><td>2518447</td><td>2500.65</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k85.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k90.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (15 / 19)</td><td>225</td><td>3622765</td><td>11976240</td><td>8205.681885</td><td></td></tr></table><p>
IBM_FV_2004_18
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k50.cnf</td><td>19</td><td>437016</td><td>1051246</td><td>1172.41</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k55.cnf</td><td>21</td><td>673115</td><td>1521669</td><td>2442.35</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k60.cnf</td><td>19</td><td>381542</td><td>1127320</td><td>866.467</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k65.cnf</td><td>21</td><td>717065</td><td>1862732</td><td>2140.23</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k70.cnf</td><td>21</td><td>747755</td><td>1939184</td><td>2529.1</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k75.cnf</td><td>20</td><td>533887</td><td>1664209</td><td>1357.59</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k80.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k85.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k90.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k95.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k10.cnf</td><td>3</td><td>339</td><td>1054</td><td>0.083987</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k100.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k15.cnf</td><td>7</td><td>2451</td><td>10625</td><td>0.673897</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k20.cnf</td><td>11</td><td>13229</td><td>43787</td><td>6.71198</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k25.cnf</td><td>14</td><td>57792</td><td>145127</td><td>52.2691</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k30.cnf</td><td>16</td><td>116752</td><td>295248</td><td>171.461</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k35.cnf</td><td>18</td><td>223139</td><td>513214</td><td>445.302</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k40.cnf</td><td>19</td><td>414465</td><td>884721</td><td>1218.98</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k45.cnf</td><td>20</td><td>574481</td><td>1213902</td><td>2385.44</td><td>SAT</td></tr>
<tr><td>Total (14 / 19)</td><td>229</td><td>4893028</td><td>12274038</td><td>14789.068964</td><td></td></tr></table><p>
IBM_FV_2004_20
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k10.cnf</td><td>1</td><td>60</td><td>203</td><td>0.068989</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k100.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k15.cnf</td><td>7</td><td>2744</td><td>10939</td><td>0.98085</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k20.cnf</td><td>11</td><td>12115</td><td>40825</td><td>6.03508</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k25.cnf</td><td>13</td><td>29554</td><td>97989</td><td>19.1951</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k30.cnf</td><td>15</td><td>61568</td><td>182353</td><td>49.2225</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k35.cnf</td><td>16</td><td>126583</td><td>329078</td><td>156.297</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k40.cnf</td><td>18</td><td>245606</td><td>587880</td><td>466.397</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k45.cnf</td><td>19</td><td>360065</td><td>849249</td><td>990.307</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k50.cnf</td><td>19</td><td>388339</td><td>984180</td><td>988.004</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k55.cnf</td><td>19</td><td>436170</td><td>1054568</td><td>1110.17</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k60.cnf</td><td>20</td><td>633814</td><td>1416778</td><td>3028.05</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k65.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k70.cnf</td><td>20</td><td>580676</td><td>1548548</td><td>1498.01</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k75.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k80.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k85.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k90.cnf</td><td>21</td><td>708170</td><td>2115326</td><td>1541.28</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (13 / 19)</td><td>199</td><td>3585464</td><td>9217916</td><td>9854.017519</td><td></td></tr></table><p>
IBM_FV_2004_2_14
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k10.cnf</td><td>4</td><td>530</td><td>3463</td><td>0.098984</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k100.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k15.cnf</td><td>6</td><td>1755</td><td>9048</td><td>0.318951</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k20.cnf</td><td>9</td><td>5869</td><td>30954</td><td>1.34279</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k25.cnf</td><td>10</td><td>9894</td><td>52341</td><td>2.78058</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k30.cnf</td><td>12</td><td>19211</td><td>100253</td><td>5.9351</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k35.cnf</td><td>13</td><td>25838</td><td>141445</td><td>9.1896</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k40.cnf</td><td>13</td><td>36179</td><td>209278</td><td>13.9379</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k45.cnf</td><td>14</td><td>49044</td><td>304401</td><td>23.2855</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k50.cnf</td><td>15</td><td>62653</td><td>348069</td><td>33.075</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k55.cnf</td><td>15</td><td>84935</td><td>480224</td><td>52.299</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k60.cnf</td><td>17</td><td>192455</td><td>758159</td><td>194.844</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k65.cnf</td><td>17</td><td>153684</td><td>768449</td><td>132.668</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k70.cnf</td><td>17</td><td>143659</td><td>779328</td><td>102.155</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k75.cnf</td><td>18</td><td>204416</td><td>915882</td><td>196.837</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k80.cnf</td><td>19</td><td>413388</td><td>1429705</td><td>678.97</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k85.cnf</td><td>19</td><td>430366</td><td>1474384</td><td>830.292</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k90.cnf</td><td>21</td><td>914362</td><td>2432169</td><td>3379.35</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k95.cnf</td><td>20</td><td>456815</td><td>1766684</td><td>846.996</td><td>UNSAT</td></tr>
<tr><td>Total (18 / 19)</td><td>259</td><td>3205053</td><td>12004236</td><td>6504.375405</td><td></td></tr></table><p>
IBM_FV_2004_23
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k10.cnf</td><td>1</td><td>6</td><td>6</td><td>0.05999</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k100.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k15.cnf</td><td>5</td><td>1307</td><td>5125</td><td>0.397939</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k20.cnf</td><td>9</td><td>7322</td><td>27204</td><td>3.76243</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k25.cnf</td><td>13</td><td>38077</td><td>117703</td><td>26.7309</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k30.cnf</td><td>16</td><td>109395</td><td>318768</td><td>139.493</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k35.cnf</td><td>18</td><td>292049</td><td>737473</td><td>828.668</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k40.cnf</td><td>17</td><td>137839</td><td>532533</td><td>186.688</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k45.cnf</td><td>20</td><td>494053</td><td>1362225</td><td>1669.88</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k50.cnf</td><td>19</td><td>353395</td><td>1196515</td><td>558.677</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k55.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k60.cnf</td><td>19</td><td>336412</td><td>1267306</td><td>417.176</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k65.cnf</td><td>21</td><td>847476</td><td>2588788</td><td>2163.15</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k70.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k75.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k80.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k85.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k90.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (11 / 19)</td><td>158</td><td>2617331</td><td>8153646</td><td>5994.683259</td><td></td></tr></table><p>
IBM_FV_2004_26
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k10.cnf</td><td>11</td><td>16560</td><td>102544</td><td>4.33534</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k100.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k15.cnf</td><td>4</td><td>815</td><td>25720</td><td>0.422935</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k20.cnf</td><td>15</td><td>58540</td><td>265810</td><td>35.5116</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k25.cnf</td><td>14</td><td>46159</td><td>283974</td><td>39.424</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k30.cnf</td><td>14</td><td>52280</td><td>255578</td><td>51.7831</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k35.cnf</td><td>4</td><td>693</td><td>25752</td><td>0.804877</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k40.cnf</td><td>4</td><td>757</td><td>27601</td><td>0.832873</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k45.cnf</td><td>18</td><td>243839</td><td>1048504</td><td>273.482</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k50.cnf</td><td>22</td><td>1009036</td><td>3373494</td><td>1842.53</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k55.cnf</td><td>4</td><td>762</td><td>40165</td><td>1.18182</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k60.cnf</td><td>5</td><td>1317</td><td>46270</td><td>1.37979</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k65.cnf</td><td>23</td><td>1517854</td><td>4514167</td><td>3142.46</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k70.cnf</td><td>4</td><td>701</td><td>23188</td><td>1.40479</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k75.cnf</td><td>5</td><td>1205</td><td>69534</td><td>2.17367</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k80.cnf</td><td>4</td><td>677</td><td>31819</td><td>1.71074</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k85.cnf</td><td>4</td><td>765</td><td>32222</td><td>1.71674</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k90.cnf</td><td>4</td><td>755</td><td>63836</td><td>1.83072</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (17 / 19)</td><td>159</td><td>2952715</td><td>10230178</td><td>5402.984995</td><td></td></tr></table><p>
IBM_FV_2004_29
<table border=1><tr><td>CNF</td><td>Restarts</td><td>Conflicts</td><td>Decisions</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k25.cnf</td><td>21</td><td>932264</td><td>1468325</td><td>1255.05</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k30.cnf</td><td>22</td><td>1114896</td><td>1816319</td><td>1707.55</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k35.cnf</td><td>21</td><td>675182</td><td>1168762</td><td>825.654</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k40.cnf</td><td>17</td><td>162678</td><td>332478</td><td>118.124</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k45.cnf</td><td>20</td><td>576405</td><td>1079933</td><td>669.592</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k50.cnf</td><td>15</td><td>71001</td><td>171720</td><td>35.4026</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k55.cnf</td><td>18</td><td>252001</td><td>523814</td><td>244.861</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k60.cnf</td><td>21</td><td>991356</td><td>1775483</td><td>1967.16</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k65.cnf</td><td>20</td><td>506386</td><td>938202</td><td>713.737</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k70.cnf</td><td>18</td><td>277054</td><td>592862</td><td>258.958</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k75.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k80.cnf</td><td>16</td><td>128091</td><td>318370</td><td>59.068</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k85.cnf</td><td>18</td><td>260761</td><td>592134</td><td>221.107</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k90.cnf</td><td>21</td><td>825753</td><td>1643077</td><td>1446.17</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k95.cnf</td><td>19</td><td>402361</td><td>892608</td><td>499.098</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k10.cnf</td><td>12</td><td>17516</td><td>27359</td><td>4.76828</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k100.cnf</td><td>19</td><td>313695</td><td>706383</td><td>336.13</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k15.cnf</td><td>15</td><td>62627</td><td>108613</td><td>28.4237</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k20.cnf</td><td>19</td><td>322630</td><td>520710</td><td>264.515</td><td>UNSAT</td></tr>
<tr><td>Total (18 / 19)</td><td>332</td><td>7892657</td><td>14677152</td><td>10655.36858</td><td></td></tr></table><p>