BerkMin<p>
16 groups, 311 instances, 1-hour cutoff<p>
Instances solved: 201 (62 SAT + 139 UNSAT)<br>
Time: 450850 seconds / 125.24 hours / 5.22 days<br>
Time on solved instances: 54850 seconds (42956 SAT + 11894 UNSAT)<p>
Instances solved in 10 minutes: 172 (9804 seconds)<br>
Instances solved in 15 minutes: 179 (14786 seconds)<br>
Instances solved in 20 minutes: 183 (18992 seconds)<br>
Instances solved in 30 minutes: 192 (32596 seconds)<br>
Instances solved in 60 minutes: 201 (54850 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>8</td><td>/</td><td>20</td><td width=20></td><td>2112.78</td></tr>
<tr><td>IBM_FV_2002_03_rule</td><td width=20></td><td>13</td><td>/</td><td>20</td><td width=20></td><td>3738.34</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>14859.11</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>2750.36</td></tr>
<tr><td>IBM_FV_2002_06_rule</td><td width=20></td><td>14</td><td>/</td><td>20</td><td width=20></td><td>6470.03</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>107.65</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>2.01</td></tr>
<tr><td>IBM_FV_2004_01</td><td width=20></td><td>6</td><td>/</td><td>19</td><td width=20></td><td>2580.89</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>85.35</td></tr>
<tr><td>IBM_FV_2004_1_11</td><td width=20></td><td>6</td><td>/</td><td>19</td><td width=20></td><td>3462.97</td></tr>
<tr><td>IBM_FV_2004_18</td><td width=20></td><td>7</td><td>/</td><td>19</td><td width=20></td><td>5423.37</td></tr>
<tr><td>IBM_FV_2004_20</td><td width=20></td><td>8</td><td>/</td><td>19</td><td width=20></td><td>4013.01</td></tr>
<tr><td>IBM_FV_2004_2_14</td><td width=20></td><td>11</td><td>/</td><td>19</td><td width=20></td><td>5296.58</td></tr>
<tr><td>IBM_FV_2004_23</td><td width=20></td><td>7</td><td>/</td><td>19</td><td width=20></td><td>2710.35</td></tr>
<tr><td>IBM_FV_2004_26</td><td width=20></td><td>19</td><td>/</td><td>19</td><td width=20></td><td>80.8</td></tr>
<tr><td>IBM_FV_2004_29</td><td width=20></td><td>3</td><td>/</td><td>19</td><td width=20></td><td>1156.69</td></tr>
</table>
<p>

IBM_FV_2002_01_rule
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k45.cnf</td></td></tr>
<tr><td>SAT_dat.k50.cnf</td></td></tr>
<tr><td>SAT_dat.k55.cnf</td></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></tr>
<tr><td>SAT_dat.k75.cnf</td></td></tr>
<tr><td>SAT_dat.k80.cnf</td></td></tr>
<tr><td>SAT_dat.k85.cnf</td></td></tr>
<tr><td>SAT_dat.k90.cnf</td></td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>383</td><td>35</td><td>7</td><td>0.000</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td></td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>6671</td><td>1604</td><td>6</td><td>0.330</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td></td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>29066</td><td>5715</td><td>9</td><td>1.900</td><td>SAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>123198</td><td>37652</td><td>28</td><td>20.660</td><td>SAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>319924</td><td>88574</td><td>52</td><td>65.150</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>825494</td><td>268740</td><td>124</td><td>329.550</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>1272522</td><td>380246</td><td>151</td><td>551.100</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>2017590</td><td>599032</td><td>207</td><td>1144.090</td><td>SAT</td></tr>
<tr><td>Total (8 / 20)</td><td>4594848</td><td>1381598</td><td>584</td><td>2112.78</td><td></td></tr></table><p>
IBM_FV_2002_03_rule
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>88</td><td>10</td><td>3</td><td>0.000</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>4504</td><td>293</td><td>6</td><td>0.130</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td></td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>8829</td><td>724</td><td>6</td><td>0.320</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>15635</td><td>1708</td><td>5</td><td>0.710</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>19619</td><td>1715</td><td>6</td><td>0.900</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>49174</td><td>7397</td><td>7</td><td>3.410</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>148558</td><td>34169</td><td>19</td><td>25.770</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>229232</td><td>54810</td><td>23</td><td>42.490</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>467394</td><td>125958</td><td>43</td><td>139.920</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>712421</td><td>199932</td><td>59</td><td>233.270</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>1226146</td><td>360768</td><td>94</td><td>574.590</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>1940414</td><td>589107</td><td>139</td><td>1126.760</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>2433078</td><td>765519</td><td>165</td><td>1590.070</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td></td></tr>
<tr><td>SAT_dat.k75.cnf</td></td></tr>
<tr><td>SAT_dat.k80.cnf</td></td></tr>
<tr><td>SAT_dat.k85.cnf</td></td></tr>
<tr><td>SAT_dat.k90.cnf</td></td></tr>
<tr><td>SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (13 / 20)</td><td>7255092</td><td>2142110</td><td>575</td><td>3738.34</td><td></td></tr></table><p>
IBM_FV_2002_04_rule
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>8040</td><td>233</td><td>8</td><td>0.000</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>28086</td><td>485</td><td>6</td><td>0.220</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>4857851</td><td>791721</td><td>90</td><td>2364.380</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>51481</td><td>1241</td><td>6</td><td>0.760</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>137102</td><td>5406</td><td>8</td><td>3.970</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>246015</td><td>9374</td><td>11</td><td>9.730</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>360357</td><td>18832</td><td>12</td><td>18.870</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>487351</td><td>27143</td><td>14</td><td>31.980</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>659871</td><td>52027</td><td>18</td><td>58.340</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>861647</td><td>80184</td><td>26</td><td>111.600</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>1106389</td><td>106028</td><td>29</td><td>154.820</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>1291817</td><td>167948</td><td>39</td><td>252.530</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>1645643</td><td>227239</td><td>46</td><td>413.990</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>2128143</td><td>380243</td><td>70</td><td>739.690</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>2322007</td><td>396613</td><td>67</td><td>803.720</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>2875251</td><td>564804</td><td>89</td><td>1320.480</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>3129249</td><td>622255</td><td>90</td><td>1452.050</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>3749489</td><td>736935</td><td>99</td><td>2000.240</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>3873505</td><td>685196</td><td>87</td><td>1779.580</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>4522279</td><td>1048527</td><td>127</td><td>3342.160</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>34341573</td><td>5922434</td><td>942</td><td>14859.11</td><td></td></tr></table><p>
IBM_FV_2002_05_rule
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>367</td><td>23</td><td>5</td><td>0.000</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>25360</td><td>538</td><td>4</td><td>0.430</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>3037830</td><td>39348</td><td>6</td><td>449.930</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>64532</td><td>1299</td><td>5</td><td>1.550</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>119094</td><td>2623</td><td>4</td><td>3.990</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>174128</td><td>3402</td><td>5</td><td>7.090</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>259994</td><td>5070</td><td>4</td><td>12.560</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>481174</td><td>7234</td><td>6</td><td>26.910</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>600070</td><td>13099</td><td>6</td><td>42.430</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>720904</td><td>11211</td><td>6</td><td>44.910</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>860800</td><td>11792</td><td>5</td><td>64.730</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>1027532</td><td>16397</td><td>6</td><td>94.350</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>1279866</td><td>18309</td><td>5</td><td>124.150</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>1434736</td><td>25310</td><td>7</td><td>154.620</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>1599796</td><td>21421</td><td>5</td><td>163.120</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>1838534</td><td>27600</td><td>6</td><td>218.830</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>2099884</td><td>32525</td><td>5</td><td>288.190</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>2364758</td><td>36417</td><td>8</td><td>300.410</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>2562654</td><td>35962</td><td>6</td><td>362.960</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>2793852</td><td>34324</td><td>5</td><td>389.200</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td>23345865</td><td>343904</td><td>109</td><td>2750.36</td><td></td></tr></table><p>
IBM_FV_2002_06_rule
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k95.cnf</td></td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>792</td><td>55</td><td>6</td><td>0.000</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>3762</td><td>398</td><td>5</td><td>0.120</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td></td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>8381</td><td>958</td><td>5</td><td>0.320</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>29554</td><td>3316</td><td>7</td><td>1.550</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>47239</td><td>7298</td><td>6</td><td>3.830</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>70428</td><td>16995</td><td>8</td><td>14.680</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>233204</td><td>57068</td><td>19</td><td>72.370</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>288392</td><td>67541</td><td>20</td><td>85.910</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>472856</td><td>128872</td><td>33</td><td>205.180</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>683052</td><td>182786</td><td>41</td><td>309.380</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>1044047</td><td>296278</td><td>59</td><td>611.020</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>1441756</td><td>394816</td><td>72</td><td>911.410</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>2055790</td><td>587154</td><td>97</td><td>1497.420</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>2989176</td><td>886299</td><td>134</td><td>2756.840</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td></td></tr>
<tr><td>SAT_dat.k80.cnf</td></td></tr>
<tr><td>SAT_dat.k85.cnf</td></td></tr>
<tr><td>SAT_dat.k90.cnf</td></td></tr>
<tr><td>Total (14 / 20)</td><td>9368429</td><td>2629834</td><td>512</td><td>6470.03</td><td></td></tr></table><p>
IBM_FV_2002_07_rule
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>9180</td><td>1135</td><td>7</td><td>0.030</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>508952</td><td>40759</td><td>76</td><td>8.480</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>284551</td><td>23033</td><td>26</td><td>7.450</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>267307</td><td>21586</td><td>42</td><td>3.140</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>270074</td><td>21733</td><td>42</td><td>3.330</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>256904</td><td>22016</td><td>42</td><td>3.480</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>290158</td><td>28369</td><td>55</td><td>4.930</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>276689</td><td>26009</td><td>49</td><td>4.550</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>281899</td><td>26301</td><td>50</td><td>4.840</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>281411</td><td>24455</td><td>46</td><td>4.720</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>274092</td><td>23679</td><td>43</td><td>4.840</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>279099</td><td>25793</td><td>44</td><td>5.370</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>275382</td><td>24145</td><td>39</td><td>5.320</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>276916</td><td>25079</td><td>38</td><td>5.920</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>275800</td><td>23703</td><td>35</td><td>5.960</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>290713</td><td>26956</td><td>38</td><td>6.680</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>266229</td><td>21914</td><td>30</td><td>5.680</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>280677</td><td>23032</td><td>30</td><td>6.240</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>303508</td><td>28200</td><td>34</td><td>8.190</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>314025</td><td>30736</td><td>35</td><td>8.500</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td>5563566</td><td>488633</td><td>801</td><td>107.65</td><td></td></tr></table><p>
IBM_FV_2002_09_rule
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>754</td><td>76</td><td>6</td><td>0.000</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>7950</td><td>255</td><td>5</td><td>0.070</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>3436</td><td>95</td><td>1</td><td>0.180</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>2213</td><td>123</td><td>2</td><td>0.060</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>2130</td><td>100</td><td>1</td><td>0.060</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>2494</td><td>94</td><td>1</td><td>0.060</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>2817</td><td>114</td><td>1</td><td>0.080</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>2572</td><td>91</td><td>1</td><td>0.090</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>2361</td><td>91</td><td>1</td><td>0.080</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>1633</td><td>77</td><td>1</td><td>0.070</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>2548</td><td>96</td><td>1</td><td>0.090</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>3019</td><td>162</td><td>1</td><td>0.100</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>2653</td><td>95</td><td>1</td><td>0.100</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>3620</td><td>100</td><td>1</td><td>0.130</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>2892</td><td>96</td><td>1</td><td>0.120</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>3456</td><td>132</td><td>1</td><td>0.130</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>3198</td><td>137</td><td>1</td><td>0.130</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>3562</td><td>90</td><td>1</td><td>0.150</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>3876</td><td>124</td><td>1</td><td>0.150</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>3408</td><td>120</td><td>1</td><td>0.160</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td>60592</td><td>2268</td><td>30</td><td>2.01</td><td></td></tr></table><p>
IBM_FV_2004_01
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k10.cnf</td><td>22811</td><td>2804</td><td>9</td><td>1.350</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k100.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k15.cnf</td><td>82937</td><td>28915</td><td>41</td><td>12.230</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k20.cnf</td><td>212362</td><td>81306</td><td>84</td><td>52.750</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k25.cnf</td><td>424187</td><td>148867</td><td>122</td><td>131.790</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k30.cnf</td><td>903413</td><td>330927</td><td>226</td><td>445.270</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k35.cnf</td><td>2252031</td><td>852637</td><td>500</td><td>1937.500</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k40.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k45.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k50.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k55.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k60.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k65.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k70.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k75.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k80.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k85.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k90.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (6 / 19)</td><td>3897741</td><td>1445456</td><td>982</td><td>2580.89</td><td></td></tr></table><p>
IBM_FV_2004_07
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k10.cnf</td><td>781373</td><td>62207</td><td>116</td><td>17.240</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k100.cnf</td><td>238723</td><td>19270</td><td>22</td><td>4.560</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k15.cnf</td><td>236290</td><td>20143</td><td>38</td><td>3.030</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k20.cnf</td><td>240895</td><td>17621</td><td>33</td><td>2.790</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k25.cnf</td><td>254378</td><td>19099</td><td>37</td><td>3.180</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k30.cnf</td><td>237812</td><td>20265</td><td>39</td><td>3.270</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k35.cnf</td><td>234540</td><td>17074</td><td>32</td><td>3.050</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k40.cnf</td><td>244386</td><td>18692</td><td>35</td><td>3.360</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k45.cnf</td><td>242478</td><td>18638</td><td>32</td><td>3.540</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k50.cnf</td><td>249233</td><td>19698</td><td>33</td><td>3.640</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k55.cnf</td><td>244081</td><td>20084</td><td>30</td><td>3.930</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k60.cnf</td><td>240099</td><td>19806</td><td>29</td><td>3.840</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k65.cnf</td><td>239370</td><td>18391</td><td>25</td><td>3.940</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k70.cnf</td><td>231261</td><td>17891</td><td>25</td><td>3.700</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k75.cnf</td><td>248506</td><td>20496</td><td>26</td><td>4.640</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k80.cnf</td><td>261037</td><td>19705</td><td>24</td><td>4.400</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k85.cnf</td><td>252621</td><td>19091</td><td>23</td><td>4.220</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k90.cnf</td><td>241772</td><td>19278</td><td>22</td><td>4.350</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k95.cnf</td><td>230565</td><td>18047</td><td>20</td><td>4.670</td><td>UNSAT</td></tr>
<tr><td>Total (19 / 19)</td><td>5149420</td><td>405496</td><td>641</td><td>85.35</td><td></td></tr></table><p>
IBM_FV_2004_1_11
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k10.cnf</td><td>214369</td><td>1525</td><td>7</td><td>9.020</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>310621</td><td>9612</td><td>6</td><td>24.190</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k20.cnf</td><td>410453</td><td>27011</td><td>11</td><td>60.460</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k25.cnf</td><td>704944</td><td>97266</td><td>22</td><td>202.270</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k30.cnf</td><td>1118117</td><td>272960</td><td>49</td><td>617.530</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k35.cnf</td><td>2284443</td><td>860281</td><td>125</td><td>2549.500</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k40.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k45.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k50.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k55.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k60.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k65.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k70.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k75.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k80.cnf</td></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 (6 / 19)</td><td>5042947</td><td>1268655</td><td>220</td><td>3462.97</td><td></td></tr></table><p>
IBM_FV_2004_18
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k10.cnf</td><td>60354</td><td>2102</td><td>7</td><td>2.190</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>111110</td><td>9961</td><td>10</td><td>8.010</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k20.cnf</td><td>202557</td><td>26708</td><td>16</td><td>24.360</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k25.cnf</td><td>325675</td><td>77450</td><td>31</td><td>89.690</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k30.cnf</td><td>738273</td><td>243020</td><td>74</td><td>420.720</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k35.cnf</td><td>1336919</td><td>610841</td><td>156</td><td>1515.200</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k40.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k45.cnf</td><td>2444035</td><td>1157414</td><td>227</td><td>3363.200</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k50.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k55.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k60.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k65.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k70.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k75.cnf</td></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>Total (7 / 19)</td><td>5218923</td><td>2127496</td><td>521</td><td>5423.37</td><td></td></tr></table><p>
IBM_FV_2004_20
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k10.cnf</td><td>68214</td><td>1544</td><td>6</td><td>2.120</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>127470</td><td>11435</td><td>10</td><td>9.180</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k20.cnf</td><td>229608</td><td>28890</td><td>15</td><td>25.090</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k25.cnf</td><td>316981</td><td>58011</td><td>24</td><td>62.930</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k30.cnf</td><td>494720</td><td>84636</td><td>28</td><td>104.870</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k35.cnf</td><td>961788</td><td>321374</td><td>83</td><td>611.320</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k40.cnf</td><td>1378798</td><td>541978</td><td>120</td><td>1364.250</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k45.cnf</td><td>1959049</td><td>702836</td><td>134</td><td>1833.250</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k50.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k55.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k60.cnf</td></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></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></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (8 / 19)</td><td>5536628</td><td>1750704</td><td>420</td><td>4013.01</td><td></td></tr></table><p>
IBM_FV_2004_2_14
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k10.cnf</td><td>128477</td><td>2269</td><td>7</td><td>1.970</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>206720</td><td>5868</td><td>8</td><td>4.580</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k20.cnf</td><td>409465</td><td>17690</td><td>13</td><td>14.280</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k25.cnf</td><td>798535</td><td>35711</td><td>20</td><td>37.480</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k30.cnf</td><td>1018543</td><td>53305</td><td>22</td><td>61.490</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k35.cnf</td><td>1162800</td><td>76123</td><td>28</td><td>96.250</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k40.cnf</td><td>2089920</td><td>168453</td><td>50</td><td>275.740</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k45.cnf</td><td>2417597</td><td>181673</td><td>48</td><td>338.080</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k50.cnf</td><td>3893839</td><td>360308</td><td>85</td><td>777.410</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k55.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k60.cnf</td><td>5359842</td><td>586005</td><td>113</td><td>1582.540</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k65.cnf</td><td>6159638</td><td>752321</td><td>133</td><td>2106.760</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k70.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k75.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k80.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k85.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k90.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (11 / 19)</td><td>23645376</td><td>2239726</td><td>527</td><td>5296.58</td><td></td></tr></table><p>
IBM_FV_2004_23
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k10.cnf</td><td>23546</td><td>776</td><td>6</td><td>0.970</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>161109</td><td>5386</td><td>7</td><td>7.310</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k20.cnf</td><td>252552</td><td>17830</td><td>11</td><td>18.230</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k25.cnf</td><td>471927</td><td>63052</td><td>23</td><td>70.050</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k30.cnf</td><td>797905</td><td>191012</td><td>53</td><td>289.440</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k35.cnf</td><td>1579517</td><td>625124</td><td>139</td><td>1503.010</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k40.cnf</td><td>1889825</td><td>410086</td><td>79</td><td>821.340</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k45.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k50.cnf</td></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></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></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 (7 / 19)</td><td>5176381</td><td>1313266</td><td>318</td><td>2710.35</td><td></td></tr></table><p>
IBM_FV_2004_26
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k10.cnf</td><td>60406</td><td>1012</td><td>1</td><td>1.600</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k100.cnf</td><td>57392</td><td>481</td><td>1</td><td>10.840</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k15.cnf</td><td>55513</td><td>520</td><td>1</td><td>1.730</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k20.cnf</td><td>57392</td><td>481</td><td>1</td><td>2.450</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k25.cnf</td><td>24947</td><td>469</td><td>1</td><td>1.430</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k30.cnf</td><td>50165</td><td>619</td><td>1</td><td>2.950</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k35.cnf</td><td>38624</td><td>515</td><td>1</td><td>2.470</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k40.cnf</td><td>56924</td><td>503</td><td>1</td><td>4.260</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k45.cnf</td><td>16686</td><td>511</td><td>1</td><td>1.080</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k50.cnf</td><td>24281</td><td>490</td><td>1</td><td>2.370</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k55.cnf</td><td>55513</td><td>520</td><td>1</td><td>5.490</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k60.cnf</td><td>57392</td><td>481</td><td>1</td><td>6.710</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k65.cnf</td><td>24947</td><td>469</td><td>1</td><td>3.310</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k70.cnf</td><td>50165</td><td>619</td><td>1</td><td>6.220</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k75.cnf</td><td>38624</td><td>515</td><td>1</td><td>4.870</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k80.cnf</td><td>56924</td><td>503</td><td>1</td><td>8.100</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k85.cnf</td><td>16686</td><td>511</td><td>1</td><td>1.820</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k90.cnf</td><td>24281</td><td>490</td><td>1</td><td>3.970</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k95.cnf</td><td>55513</td><td>520</td><td>1</td><td>9.130</td><td>UNSAT</td></tr>
<tr><td>Total (19 / 19)</td><td>822375</td><td>10229</td><td>19</td><td>80.8</td><td></td></tr></table><p>
IBM_FV_2004_29
<table border=1><tr><td>CNF</td><td>Decisions</td><td>Conflicts</td><td>Restarts</td><td>Time</td><td>Sol</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k10.cnf</td><td>62094</td><td>34130</td><td>63</td><td>12.440</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k100.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k15.cnf</td><td>304892</td><td>171858</td><td>234</td><td>121.030</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k20.cnf</td><td>1157620</td><td>692092</td><td>708</td><td>1023.220</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k25.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k30.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k35.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k40.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k45.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k50.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k55.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k60.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k65.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k70.cnf</td></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></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k85.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k90.cnf</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k95.cnf</td></td></tr>
<tr><td>Total (3 / 19)</td><td>1524606</td><td>898080</td><td>1005</td><td>1156.69</td><td></td></tr></table><p>