MiniSat 2.0<p>
16 groups, 311 instances, 1-hour cutoff<p>
Instances solved: 304 (162 SAT + 142 UNSAT)<br>
Time: 93632 seconds / 26.01 hours / 1.08 days<br>
Time on solved instances: 68432 seconds (58152 SAT + 10280 UNSAT)<p>
Instances solved in 10 minutes: 269 (19620 seconds)<br>
Instances solved in 15 minutes: 278 (26646 seconds)<br>
Instances solved in 20 minutes: 290 (39031 seconds)<br>
Instances solved in 30 minutes: 296 (47340 seconds)<br>
Instances solved in 60 minutes: 304 (68432 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>2486.211177</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>490.418952</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>716.677226</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>128.938321</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>515.442251</td></tr>
<tr><td>IBM_FV_2002_07_rule</td><td width=20></td><td>20</td><td>/</td><td>20</td><td width=20></td><td>379.671344</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>12.355105</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>1608.738769</td></tr>
<tr><td>IBM_FV_2004_07</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>131.2281</td></tr>
<tr><td>IBM_FV_2004_1_11</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>3340.06906</td></tr>
<tr><td>IBM_FV_2004_18</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>7443.513294</td></tr>
<tr><td>IBM_FV_2004_20</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>13444.68674</td></tr>
<tr><td>IBM_FV_2004_2_14</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>3111.862632</td></tr>
<tr><td>IBM_FV_2004_23</td><td width=20></td><td>18</td><td>/</td><td>19</td><td width=20></td><td>17814.993529</td></tr>
<tr><td>IBM_FV_2004_26</td><td width=20></td><td>13</td><td>/</td><td>19</td><td width=20></td><td>4683.01799</td></tr>
<tr><td>IBM_FV_2004_29</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>12123.81708</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.k45.cnf</td><td>16</td><td>98549</td><td>220514</td><td>48.5056</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>16</td><td>99675</td><td>232327</td><td>45.1631</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>15</td><td>71981</td><td>179981</td><td>23.5664</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>16</td><td>121860</td><td>302562</td><td>49.1375</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>18</td><td>250298</td><td>558192</td><td>206.777</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>13</td><td>36521</td><td>96157</td><td>10.8184</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>17</td><td>172160</td><td>416098</td><td>99.8688</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>19</td><td>357649</td><td>793057</td><td>328.553</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>15</td><td>76392</td><td>177638</td><td>31.1813</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>19</td><td>403945</td><td>916433</td><td>353.929</td><td>SAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>20</td><td>602901</td><td>1345401</td><td>723.752</td><td>SAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>3</td><td>297</td><td>703</td><td>0.200969</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>20</td><td>467166</td><td>1060510</td><td>479.598</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>6</td><td>1838</td><td>4322</td><td>0.536918</td><td>SAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>9</td><td>7420</td><td>16302</td><td>2.03569</td><td>SAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>14</td><td>54237</td><td>103235</td><td>33.5389</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>12</td><td>24293</td><td>58501</td><td>7.8888</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>13</td><td>33310</td><td>77752</td><td>13.403</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>15</td><td>66337</td><td>165210</td><td>27.7568</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>276</td><td>2946829</td><td>6724895</td><td>2486.211177</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></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>18</td><td>280054</td><td>667648</td><td>167.8</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>1</td><td>8</td><td>31</td><td>0.507922</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>8</td><td>4091</td><td>10921</td><td>1.19682</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>10</td><td>9775</td><td>30415</td><td>3.2505</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>10</td><td>9272</td><td>28003</td><td>3.06953</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>11</td><td>13996</td><td>37443</td><td>3.84142</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>11</td><td>17026</td><td>50998</td><td>4.84826</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>14</td><td>49384</td><td>124936</td><td>13.9999</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>13</td><td>37171</td><td>103933</td><td>11.5762</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>15</td><td>62055</td><td>155828</td><td>21.2218</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>15</td><td>61518</td><td>170603</td><td>20.2529</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>17</td><td>136045</td><td>335289</td><td>53.6288</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>16</td><td>96399</td><td>251399</td><td>35.6196</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>17</td><td>171094</td><td>450223</td><td>85.1421</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>17</td><td>154523</td><td>395781</td><td>64.4632</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>193</td><td>1102411</td><td>2813451</td><td>490.418952</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></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>17</td><td>166266</td><td>556309</td><td>161.321</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>1</td><td>17</td><td>55</td><td>0.168974</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>3</td><td>299</td><td>678</td><td>0.316951</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>6</td><td>1832</td><td>4949</td><td>0.777881</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>8</td><td>4395</td><td>11412</td><td>1.48877</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>9</td><td>7168</td><td>20035</td><td>2.56061</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>11</td><td>14633</td><td>44080</td><td>5.54216</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>11</td><td>14900</td><td>53212</td><td>5.39818</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>12</td><td>24411</td><td>81768</td><td>10.4944</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>12</td><td>23434</td><td>84743</td><td>10.3064</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>14</td><td>46131</td><td>150671</td><td>24.8012</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>15</td><td>72993</td><td>223768</td><td>48.6276</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>15</td><td>75122</td><td>238352</td><td>51.9501</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>15</td><td>65850</td><td>241575</td><td>40.8738</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>16</td><td>116212</td><td>371386</td><td>92.5379</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>15</td><td>84363</td><td>286303</td><td>65.773</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>16</td><td>99082</td><td>349848</td><td>63.8153</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>17</td><td>143857</td><td>498591</td><td>129.923</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>213</td><td>960965</td><td>3217735</td><td>716.677226</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>0</td><td>0</td><td>0</td><td>0.002999</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>2</td><td>182</td><td>450</td><td>0.245962</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>12</td><td>17473</td><td>144371</td><td>17.0214</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>3</td><td>301</td><td>822</td><td>0.426935</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>5</td><td>829</td><td>2320</td><td>0.686895</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>5</td><td>1008</td><td>3467</td><td>1.09483</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>6</td><td>1645</td><td>8367</td><td>1.70774</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>7</td><td>2322</td><td>10960</td><td>2.32665</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>7</td><td>2536</td><td>15615</td><td>3.06853</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>8</td><td>4079</td><td>24031</td><td>4.04439</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>10</td><td>7631</td><td>52193</td><td>6.34504</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>9</td><td>5187</td><td>34671</td><td>5.65614</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>9</td><td>5376</td><td>34388</td><td>5.74113</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>10</td><td>7875</td><td>66963</td><td>7.57585</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>9</td><td>7292</td><td>67214</td><td>8.34073</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>10</td><td>9724</td><td>73727</td><td>10.3674</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>11</td><td>15349</td><td>116945</td><td>13.7019</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>11</td><td>13242</td><td>105103</td><td>13.112</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>10</td><td>10925</td><td>103764</td><td>13.8049</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>11</td><td>11360</td><td>116044</td><td>13.6669</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>155</td><td>124336</td><td>981415</td><td>128.938321</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>17</td><td>133701</td><td>319269</td><td>81.6826</td><td>SAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>17</td><td>135378</td><td>337417</td><td>71.5991</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>1</td><td>60</td><td>328</td><td>0.340948</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>3</td><td>454</td><td>1208</td><td>0.634903</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>4</td><td>728</td><td>2827</td><td>1.06584</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>8</td><td>4255</td><td>13620</td><td>3.52046</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>8</td><td>3783</td><td>13598</td><td>2.6406</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>9</td><td>5730</td><td>19500</td><td>3.53446</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>10</td><td>8074</td><td>24542</td><td>4.33734</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>8</td><td>3789</td><td>16412</td><td>2.97355</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>12</td><td>24276</td><td>74561</td><td>11.7542</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>10</td><td>9529</td><td>35633</td><td>5.56415</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>10</td><td>11072</td><td>45497</td><td>6.603</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>15</td><td>62756</td><td>154641</td><td>29.9245</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>15</td><td>74104</td><td>191165</td><td>40.3009</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>16</td><td>117218</td><td>296435</td><td>76.3394</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>16</td><td>103070</td><td>234292</td><td>50.7123</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>17</td><td>194076</td><td>417036</td><td>121.914</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>196</td><td>892053</td><td>2197981</td><td>515.442251</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>1798</td><td>9444</td><td>0.032994</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>22</td><td>1489334</td><td>8288159</td><td>322.748</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>14</td><td>44785</td><td>305776</td><td>2.81357</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>13</td><td>36864</td><td>284934</td><td>2.05669</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>14</td><td>41805</td><td>295690</td><td>2.73058</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>13</td><td>30625</td><td>215060</td><td>1.74174</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>14</td><td>50378</td><td>249128</td><td>3.41148</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>14</td><td>43650</td><td>343003</td><td>2.76058</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>15</td><td>60339</td><td>474576</td><td>3.81642</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>13</td><td>27387</td><td>157095</td><td>1.60976</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>15</td><td>64786</td><td>485167</td><td>4.19936</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>13</td><td>36737</td><td>233784</td><td>2.12368</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>14</td><td>49126</td><td>410820</td><td>3.54146</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>14</td><td>52241</td><td>391997</td><td>3.63945</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>15</td><td>69829</td><td>460208</td><td>5.85611</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>14</td><td>54987</td><td>285346</td><td>3.51946</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>15</td><td>64861</td><td>532528</td><td>4.55631</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>15</td><td>58539</td><td>437171</td><td>4.14537</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>14</td><td>41691</td><td>329289</td><td>2.92355</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>13</td><td>26374</td><td>180586</td><td>1.44478</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td>280</td><td>2346136</td><td>14369761</td><td>379.671344</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></td><td></td><td></td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>0</td><td>0</td><td>0</td><td>0.057991</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>0</td><td>0</td><td>0</td><td>1.2838</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>0</td><td>0</td><td>0</td><td>0.12598</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>0</td><td>0</td><td>0</td><td>0.19197</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>0</td><td>0</td><td>0</td><td>0.254961</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>0</td><td>0</td><td>0</td><td>0.319951</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>0</td><td>0</td><td>0</td><td>0.374943</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>0</td><td>0</td><td>0</td><td>0.460929</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>0</td><td>0</td><td>0</td><td>0.509922</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>0</td><td>0</td><td>0</td><td>0.574912</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>0</td><td>0</td><td>0</td><td>0.639902</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>0</td><td>0</td><td>0</td><td>0.709892</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>1</td><td>18</td><td>245</td><td>0.821875</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>0</td><td>0</td><td>0</td><td>0.834873</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>1</td><td>18</td><td>259</td><td>0.979851</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>0</td><td>0</td><td>0</td><td>0.955854</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>0</td><td>0</td><td>0</td><td>0.989849</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>0</td><td>0</td><td>0</td><td>1.09983</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>0</td><td>0</td><td>0</td><td>1.16782</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td>2</td><td>36</td><td>504</td><td>12.355105</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.k10.cnf</td><td>3</td><td>270</td><td>502</td><td>0.156976</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k100.cnf</td><td>20</td><td>503601</td><td>1103626</td><td>483.111</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k15.cnf</td><td>7</td><td>2408</td><td>5483</td><td>0.434933</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k20.cnf</td><td>12</td><td>18901</td><td>39426</td><td>5.09123</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k25.cnf</td><td>12</td><td>17864</td><td>42516</td><td>5.03423</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k30.cnf</td><td>16</td><td>101005</td><td>194133</td><td>56.1415</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k35.cnf</td><td>14</td><td>42289</td><td>95386</td><td>14.1339</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k40.cnf</td><td>14</td><td>48158</td><td>121042</td><td>14.2728</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k45.cnf</td><td>14</td><td>50774</td><td>131824</td><td>12.6411</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k50.cnf</td><td>13</td><td>36785</td><td>87504</td><td>11.3603</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k55.cnf</td><td>14</td><td>47550</td><td>121191</td><td>12.0672</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k60.cnf</td><td>17</td><td>132945</td><td>300377</td><td>74.7216</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k65.cnf</td><td>18</td><td>212654</td><td>504095</td><td>134.425</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k70.cnf</td><td>19</td><td>353656</td><td>775294</td><td>257.968</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k75.cnf</td><td>18</td><td>219331</td><td>502899</td><td>115.231</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k80.cnf</td><td>17</td><td>156752</td><td>377642</td><td>69.4984</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k85.cnf</td><td>18</td><td>218111</td><td>496698</td><td>129.643</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k90.cnf</td><td>17</td><td>150093</td><td>375684</td><td>61.8526</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k95.cnf</td><td>18</td><td>250598</td><td>579870</td><td>150.954</td><td>SAT</td></tr>
<tr><td>Total (19 / 19)</td><td>281</td><td>2563745</td><td>5855192</td><td>1608.738769</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.k10.cnf</td><td>20</td><td>519098</td><td>3164433</td><td>97.6672</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k100.cnf</td><td>14</td><td>45577</td><td>342322</td><td>2.94655</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k15.cnf</td><td>13</td><td>34408</td><td>233672</td><td>1.79373</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k20.cnf</td><td>13</td><td>29681</td><td>160581</td><td>1.40379</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k25.cnf</td><td>13</td><td>26062</td><td>192919</td><td>1.36779</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k30.cnf</td><td>13</td><td>28933</td><td>201482</td><td>1.62875</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k35.cnf</td><td>13</td><td>38018</td><td>247761</td><td>2.26865</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k40.cnf</td><td>14</td><td>44102</td><td>290936</td><td>2.59061</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k45.cnf</td><td>12</td><td>23337</td><td>132774</td><td>1.19982</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k50.cnf</td><td>13</td><td>36394</td><td>236601</td><td>1.9727</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k55.cnf</td><td>13</td><td>27235</td><td>177311</td><td>1.44978</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k60.cnf</td><td>13</td><td>26237</td><td>160343</td><td>1.36679</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k65.cnf</td><td>13</td><td>29736</td><td>199529</td><td>1.69074</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k70.cnf</td><td>13</td><td>31309</td><td>227307</td><td>1.77273</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k75.cnf</td><td>13</td><td>33843</td><td>203183</td><td>2.05869</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k80.cnf</td><td>13</td><td>34031</td><td>230460</td><td>1.93571</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k85.cnf</td><td>13</td><td>33651</td><td>214347</td><td>2.04369</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k90.cnf</td><td>13</td><td>31412</td><td>254384</td><td>2.02169</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k95.cnf</td><td>13</td><td>32088</td><td>261765</td><td>2.04869</td><td>UNSAT</td></tr>
<tr><td>Total (19 / 19)</td><td>255</td><td>1105152</td><td>7132110</td><td>131.2281</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>2</td><td>252</td><td>1707</td><td>0.447931</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k100.cnf</td><td>20</td><td>536655</td><td>1694793</td><td>1048.34</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k15.cnf</td><td>4</td><td>732</td><td>2962</td><td>0.924859</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k20.cnf</td><td>8</td><td>3332</td><td>14450</td><td>2.06369</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k25.cnf</td><td>10</td><td>9808</td><td>30526</td><td>4.73728</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k30.cnf</td><td>12</td><td>24282</td><td>85475</td><td>15.4996</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k35.cnf</td><td>15</td><td>60608</td><td>181239</td><td>47.0209</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k40.cnf</td><td>14</td><td>47307</td><td>164423</td><td>30.2054</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k45.cnf</td><td>15</td><td>61341</td><td>233828</td><td>47.1078</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k50.cnf</td><td>16</td><td>102033</td><td>334728</td><td>94.6306</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k55.cnf</td><td>16</td><td>128265</td><td>463202</td><td>119.296</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k60.cnf</td><td>16</td><td>117721</td><td>398640</td><td>129.059</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k65.cnf</td><td>17</td><td>168731</td><td>577176</td><td>168.624</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k70.cnf</td><td>17</td><td>172928</td><td>634258</td><td>171.692</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k75.cnf</td><td>18</td><td>203933</td><td>752546</td><td>216.052</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k80.cnf</td><td>17</td><td>150870</td><td>578167</td><td>121.725</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k85.cnf</td><td>18</td><td>260346</td><td>853205</td><td>287.271</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k90.cnf</td><td>18</td><td>291072</td><td>1035291</td><td>372.459</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k95.cnf</td><td>19</td><td>369124</td><td>1269402</td><td>462.913</td><td>SAT</td></tr>
<tr><td>Total (19 / 19)</td><td>272</td><td>2709340</td><td>9306018</td><td>3340.06906</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.k10.cnf</td><td>2</td><td>208</td><td>619</td><td>0.297954</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k100.cnf</td><td>20</td><td>613553</td><td>1384578</td><td>1047.97</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k15.cnf</td><td>7</td><td>2481</td><td>6775</td><td>1.03084</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k20.cnf</td><td>11</td><td>13232</td><td>32436</td><td>5.2742</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k25.cnf</td><td>13</td><td>37111</td><td>71341</td><td>19.809</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k30.cnf</td><td>15</td><td>76526</td><td>146436</td><td>57.1073</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k35.cnf</td><td>17</td><td>157573</td><td>273856</td><td>195.373</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k40.cnf</td><td>18</td><td>235332</td><td>405842</td><td>346.769</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k45.cnf</td><td>17</td><td>170231</td><td>342559</td><td>234.808</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k50.cnf</td><td>18</td><td>215333</td><td>404318</td><td>333.954</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k55.cnf</td><td>18</td><td>205386</td><td>440613</td><td>283.626</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k60.cnf</td><td>18</td><td>199968</td><td>464521</td><td>227.503</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k65.cnf</td><td>18</td><td>204845</td><td>468194</td><td>270.851</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k70.cnf</td><td>18</td><td>234304</td><td>578574</td><td>352.93</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k75.cnf</td><td>19</td><td>321822</td><td>745454</td><td>461.151</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k80.cnf</td><td>20</td><td>579413</td><td>1216203</td><td>1141.31</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k85.cnf</td><td>20</td><td>559781</td><td>1191359</td><td>969.287</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k90.cnf</td><td>19</td><td>310579</td><td>743745</td><td>528.857</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k95.cnf</td><td>20</td><td>469109</td><td>1090696</td><td>965.605</td><td>SAT</td></tr>
<tr><td>Total (19 / 19)</td><td>308</td><td>4606787</td><td>10008119</td><td>7443.513294</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>2</td><td>124</td><td>219</td><td>0.301954</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k100.cnf</td><td>21</td><td>809928</td><td>1626018</td><td>3422.21</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k15.cnf</td><td>4</td><td>558</td><td>1761</td><td>0.616906</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k20.cnf</td><td>9</td><td>7294</td><td>18390</td><td>2.75758</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k25.cnf</td><td>13</td><td>33186</td><td>69051</td><td>16.1136</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k30.cnf</td><td>14</td><td>42240</td><td>96745</td><td>23.5874</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k35.cnf</td><td>16</td><td>109850</td><td>224001</td><td>96.4383</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k40.cnf</td><td>17</td><td>178250</td><td>345221</td><td>217.31</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k45.cnf</td><td>18</td><td>247466</td><td>480192</td><td>385.979</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k50.cnf</td><td>19</td><td>318815</td><td>606296</td><td>571.196</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k55.cnf</td><td>18</td><td>240485</td><td>507381</td><td>329.661</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k60.cnf</td><td>18</td><td>224221</td><td>491499</td><td>326.634</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k65.cnf</td><td>19</td><td>434563</td><td>877217</td><td>933.263</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k70.cnf</td><td>20</td><td>609379</td><td>1154165</td><td>2099.7</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k75.cnf</td><td>19</td><td>307593</td><td>722173</td><td>489.546</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k80.cnf</td><td>20</td><td>537168</td><td>1111855</td><td>1574.06</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k85.cnf</td><td>20</td><td>497592</td><td>1090395</td><td>1151.82</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k90.cnf</td><td>20</td><td>501008</td><td>1045663</td><td>1313.76</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k95.cnf</td><td>19</td><td>337024</td><td>886872</td><td>489.732</td><td>SAT</td></tr>
<tr><td>Total (19 / 19)</td><td>306</td><td>5436744</td><td>11355114</td><td>13444.68674</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>3</td><td>336</td><td>975</td><td>0.229965</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k100.cnf</td><td>20</td><td>653753</td><td>1779991</td><td>1262.58</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k15.cnf</td><td>5</td><td>1055</td><td>4541</td><td>0.543917</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k20.cnf</td><td>8</td><td>4739</td><td>19536</td><td>1.39479</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k25.cnf</td><td>9</td><td>6653</td><td>29814</td><td>2.16867</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k30.cnf</td><td>11</td><td>16210</td><td>62304</td><td>5.53516</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k35.cnf</td><td>12</td><td>24220</td><td>95215</td><td>9.02563</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k40.cnf</td><td>13</td><td>29328</td><td>134254</td><td>10.9013</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k45.cnf</td><td>15</td><td>61698</td><td>253260</td><td>28.5367</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k50.cnf</td><td>15</td><td>86498</td><td>284330</td><td>46.8259</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k55.cnf</td><td>15</td><td>78545</td><td>338364</td><td>42.9285</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k60.cnf</td><td>16</td><td>112798</td><td>498120</td><td>65.66</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k65.cnf</td><td>16</td><td>119318</td><td>466429</td><td>71.9301</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k70.cnf</td><td>17</td><td>159701</td><td>661127</td><td>120.021</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k75.cnf</td><td>18</td><td>216278</td><td>777806</td><td>178.909</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k80.cnf</td><td>18</td><td>246434</td><td>915683</td><td>241.907</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k85.cnf</td><td>18</td><td>224928</td><td>860939</td><td>184.02</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k90.cnf</td><td>18</td><td>266548</td><td>1029223</td><td>235.849</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k95.cnf</td><td>20</td><td>450106</td><td>1392064</td><td>602.896</td><td>UNSAT</td></tr>
<tr><td>Total (19 / 19)</td><td>267</td><td>2759146</td><td>9603975</td><td>3111.862632</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>5</td><td>8</td><td>0.272958</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k100.cnf</td><td>21</td><td>921563</td><td>2141853</td><td>3323.65</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k15.cnf</td><td>4</td><td>801</td><td>2034</td><td>0.646901</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k20.cnf</td><td>8</td><td>4896</td><td>13475</td><td>2.17867</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k25.cnf</td><td>12</td><td>25087</td><td>59444</td><td>13.134</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k30.cnf</td><td>16</td><td>96221</td><td>189348</td><td>100.339</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k35.cnf</td><td>17</td><td>174896</td><td>333525</td><td>231.091</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k40.cnf</td><td>19</td><td>338642</td><td>617200</td><td>796.247</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k45.cnf</td><td>17</td><td>154414</td><td>365686</td><td>173.367</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k50.cnf</td><td>19</td><td>396585</td><td>795897</td><td>1168.56</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k55.cnf</td><td>19</td><td>350243</td><td>754561</td><td>898.345</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k60.cnf</td><td>19</td><td>300169</td><td>714355</td><td>594.161</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k65.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k70.cnf</td><td>19</td><td>429743</td><td>1057957</td><td>938.627</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k75.cnf</td><td>19</td><td>390859</td><td>981126</td><td>855.868</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k80.cnf</td><td>19</td><td>363264</td><td>995748</td><td>655.916</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k85.cnf</td><td>21</td><td>898309</td><td>1974231</td><td>2791.41</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k90.cnf</td><td>21</td><td>823754</td><td>1847481</td><td>2873.51</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k95.cnf</td><td>21</td><td>682003</td><td>1624106</td><td>2397.67</td><td>SAT</td></tr>
<tr><td>Total (18 / 19)</td><td>292</td><td>6351454</td><td>14468035</td><td>17814.993529</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>8</td><td>4053</td><td>66141</td><td>3.64545</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>7</td><td>2897</td><td>54439</td><td>4.91725</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k20.cnf</td><td>10</td><td>8233</td><td>102330</td><td>9.96049</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k25.cnf</td><td>14</td><td>55170</td><td>306062</td><td>48.9146</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k30.cnf</td><td>12</td><td>21449</td><td>132343</td><td>18.8491</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k35.cnf</td><td>17</td><td>135336</td><td>524072</td><td>144.214</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k40.cnf</td><td>21</td><td>772668</td><td>2094395</td><td>1346.13</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k45.cnf</td><td>11</td><td>14191</td><td>160643</td><td>28.6706</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k50.cnf</td><td>20</td><td>489694</td><td>1498806</td><td>742.154</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k55.cnf</td><td>3</td><td>403</td><td>34611</td><td>13.9809</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k60.cnf</td><td>22</td><td>1177311</td><td>3026661</td><td>2266.31</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k65.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k70.cnf</td><td>4</td><td>793</td><td>46091</td><td>22.8205</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k75.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k80.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k85.cnf</td><td>3</td><td>354</td><td>39596</td><td>32.4511</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k90.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (13 / 19)</td><td>152</td><td>2682552</td><td>8086190</td><td>4683.01799</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.k10.cnf</td><td>13</td><td>27965</td><td>40388</td><td>8.66968</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k100.cnf</td><td>19</td><td>358625</td><td>822282</td><td>313.401</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k15.cnf</td><td>15</td><td>60017</td><td>95992</td><td>21.2348</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k20.cnf</td><td>18</td><td>239105</td><td>383323</td><td>127.404</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k25.cnf</td><td>22</td><td>1133321</td><td>1751378</td><td>1038.54</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k30.cnf</td><td>20</td><td>454410</td><td>770302</td><td>364.903</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k35.cnf</td><td>18</td><td>258987</td><td>466784</td><td>152.999</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k40.cnf</td><td>19</td><td>403108</td><td>713885</td><td>364.269</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k45.cnf</td><td>18</td><td>226978</td><td>448134</td><td>148.504</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k50.cnf</td><td>20</td><td>615864</td><td>1138546</td><td>598.635</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k55.cnf</td><td>20</td><td>463525</td><td>940204</td><td>434.989</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k60.cnf</td><td>22</td><td>1223355</td><td>2153325</td><td>1574.4</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k65.cnf</td><td>21</td><td>701078</td><td>1272265</td><td>874.9</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k70.cnf</td><td>21</td><td>837902</td><td>1645008</td><td>1038.38</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k75.cnf</td><td>21</td><td>677664</td><td>1289435</td><td>876.093</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k80.cnf</td><td>21</td><td>992854</td><td>1953351</td><td>1237.67</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k85.cnf</td><td>21</td><td>815350</td><td>1671723</td><td>943.651</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k90.cnf</td><td>17</td><td>157530</td><td>353883</td><td>88.0346</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k95.cnf</td><td>22</td><td>1250755</td><td>2440572</td><td>1917.14</td><td>SAT</td></tr>
<tr><td>Total (19 / 19)</td><td>368</td><td>10898393</td><td>20350780</td><td>12123.81708</td><td></td></tr></table><p>