Tinisat 0.22<p>
16 groups, 311 instances, 1-hour cutoff<p>
Instances solved: 279 (133 SAT + 146 UNSAT)<br>
Time: 203183 seconds / 56.44 hours / 2.35 days<br>
Time on solved instances: 87983 seconds (74602 SAT + 13381 UNSAT)<p>
Instances solved in 10 minutes: 238 (16362 seconds)<br>
Instances solved in 15 minutes: 244 (20621 seconds)<br>
Instances solved in 20 minutes: 253 (30175 seconds)<br>
Instances solved in 30 minutes: 262 (43939 seconds)<br>
Instances solved in 60 minutes: 279 (87983 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>7386.53</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>1170.77</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>10583.7</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>810.67</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>889.4</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>118.23</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>58.24</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>3067.83</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>99.7</td></tr>
<tr><td>IBM_FV_2004_1_11</td><td width=20></td><td>12</td><td>/</td><td>19</td><td width=20></td><td>6053.16</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>15594.14</td></tr>
<tr><td>IBM_FV_2004_20</td><td width=20></td><td>11</td><td>/</td><td>19</td><td width=20></td><td>9517.17</td></tr>
<tr><td>IBM_FV_2004_2_14</td><td width=20></td><td>17</td><td>/</td><td>19</td><td width=20></td><td>6436.45</td></tr>
<tr><td>IBM_FV_2004_23</td><td width=20></td><td>12</td><td>/</td><td>19</td><td width=20></td><td>8133.04</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>133</td></tr>
<tr><td>IBM_FV_2004_29</td><td width=20></td><td>16</td><td>/</td><td>19</td><td width=20></td><td>17930.78</td></tr>
</table>
<p>

IBM_FV_2002_01_rule
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>41148</td><td>210435</td><td>361158</td><td>60919</td><td>51</td><td>33.85</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>45703</td><td>233875</td><td>687175</td><td>137750</td><td>93</td><td>103.9</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>50258</td><td>257315</td><td>69122</td><td>8014</td><td>9</td><td>4.22</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>54813</td><td>280755</td><td>1180312</td><td>249126</td><td>147</td><td>251.17</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>59368</td><td>304195</td><td>1429025</td><td>287050</td><td>173</td><td>289.71</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>63923</td><td>327635</td><td>1112515</td><td>201455</td><td>126</td><td>142.13</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>68478</td><td>351075</td><td>2426933</td><td>552359</td><td>283</td><td>940.29</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>73033</td><td>374515</td><td>296779</td><td>39452</td><td>30</td><td>19.88</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>77588</td><td>397955</td><td>2310793</td><td>470422</td><td>254</td><td>469.42</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>82143</td><td>421395</td><td>4170425</td><td>931132</td><td>506</td><td>1836.14</td><td>SAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>996</td><td>3868</td><td>0</td><td>1</td><td>0</td><td>0.01</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>86698</td><td>444835</td><td>3651801</td><td>788013</td><td>412</td><td>1474.66</td><td>SAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>9299</td><td>46511</td><td>525</td><td>339</td><td>0</td><td>0.12</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>91253</td><td>468275</td><td>4349992</td><td>899519</td><td>483</td><td>1753.33</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>13818</td><td>69795</td><td>2920</td><td>1204</td><td>2</td><td>0.33</td><td>SAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>18373</td><td>93235</td><td>26517</td><td>8470</td><td>10</td><td>2.85</td><td>SAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>22928</td><td>116675</td><td>50818</td><td>11123</td><td>13</td><td>3.82</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>27483</td><td>140115</td><td>99211</td><td>22946</td><td>22</td><td>8.86</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>32038</td><td>163555</td><td>227392</td><td>47543</td><td>38</td><td>23.45</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>36593</td><td>186995</td><td>266613</td><td>52724</td><td>44</td><td>28.39</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>22720026</td><td>4769561</td><td>2696</td><td>7386.53</td><td></td></tr></table><p>
IBM_FV_2002_03_rule
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>49161</td><td>208067</td><td>11945</td><td>1135</td><td>2</td><td>1.2</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>54801</td><td>231927</td><td>155894</td><td>20068</td><td>20</td><td>12.77</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>60441</td><td>255787</td><td>237895</td><td>32075</td><td>29</td><td>21.77</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>66081</td><td>279647</td><td>367515</td><td>52544</td><td>44</td><td>42.8</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>71721</td><td>303507</td><td>248801</td><td>28177</td><td>28</td><td>20.3</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>77361</td><td>327367</td><td>660032</td><td>103803</td><td>69</td><td>94.5</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>83001</td><td>351227</td><td>843874</td><td>132038</td><td>93</td><td>130.31</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>88641</td><td>375087</td><td>841130</td><td>126298</td><td>91</td><td>126.22</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>94281</td><td>398947</td><td>1695346</td><td>307775</td><td>188</td><td>414.92</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>99921</td><td>422807</td><td>855976</td><td>122833</td><td>87</td><td>101.07</td><td>SAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>300</td><td>966</td><td>0</td><td>1</td><td>0</td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>105561</td><td>446667</td><td>977017</td><td>136479</td><td>93</td><td>134.96</td><td>SAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>9691</td><td>41102</td><td>0</td><td>1</td><td>0</td><td>0.07</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>111201</td><td>470527</td><td>612293</td><td>77411</td><td>61</td><td>63.45</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>15321</td><td>64907</td><td>0</td><td>1</td><td>0</td><td>0.11</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>20961</td><td>88767</td><td>0</td><td>1</td><td>0</td><td>0.15</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>26601</td><td>112627</td><td>0</td><td>1</td><td>0</td><td>0.19</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>32241</td><td>136487</td><td>3702</td><td>514</td><td>1</td><td>0.46</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>37881</td><td>160347</td><td>37721</td><td>4655</td><td>6</td><td>2.59</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>43521</td><td>184207</td><td>40469</td><td>4767</td><td>6</td><td>2.93</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>7589610</td><td>1150577</td><td>818</td><td>1170.77</td><td></td></tr></table><p>
IBM_FV_2002_04_rule
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>456</td><td>1035</td><td>0</td><td>1</td><td>0</td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>10165</td><td>44388</td><td>0</td><td>1</td><td>0</td><td>0.07</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>131390</td><td>575708</td><td>2185497</td><td>488963</td><td>254</td><td>1729.69</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>16895</td><td>73868</td><td>16</td><td>12</td><td>0</td><td>0.13</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>23630</td><td>103388</td><td>937</td><td>300</td><td>0</td><td>0.2</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>30365</td><td>132908</td><td>3254</td><td>508</td><td>0</td><td>0.31</td><td>SAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>37100</td><td>162428</td><td>28374</td><td>4329</td><td>6</td><td>1.68</td><td>SAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>43835</td><td>191948</td><td>46155</td><td>8405</td><td>10</td><td>2.88</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>50570</td><td>221468</td><td>80882</td><td>11567</td><td>13</td><td>5.15</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>57305</td><td>250988</td><td>154282</td><td>23996</td><td>24</td><td>14.49</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>64040</td><td>280508</td><td>215842</td><td>27072</td><td>28</td><td>16.1</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>70775</td><td>310028</td><td>288178</td><td>41904</td><td>32</td><td>34.79</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>77510</td><td>339548</td><td>427873</td><td>61740</td><td>52</td><td>54.61</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>84245</td><td>369068</td><td>602108</td><td>132259</td><td>93</td><td>215.26</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>90980</td><td>398588</td><td>743132</td><td>103895</td><td>69</td><td>152.23</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>97715</td><td>428108</td><td>752769</td><td>134662</td><td>93</td><td>212.68</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>104450</td><td>457628</td><td>1284703</td><td>341611</td><td>204</td><td>1503.73</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>111185</td><td>487148</td><td>1775563</td><td>506275</td><td>254</td><td>3083.43</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>117920</td><td>516668</td><td>1485251</td><td>322828</td><td>189</td><td>1213</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>124655</td><td>546188</td><td>1651651</td><td>587331</td><td>307</td><td>2343.27</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>11726467</td><td>2797659</td><td>1628</td><td>10583.7</td><td></td></tr></table><p>
IBM_FV_2002_05_rule
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>712</td><td>1791</td><td>1</td><td>2</td><td>0</td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>16705</td><td>89286</td><td>241</td><td>71</td><td>0</td><td>0.15</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>200570</td><td>1087061</td><td>1623079</td><td>86234</td><td>62</td><td>146.63</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>26915</td><td>144666</td><td>1307</td><td>440</td><td>0</td><td>0.29</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>37130</td><td>200101</td><td>4544</td><td>1298</td><td>2</td><td>0.5</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>47345</td><td>255536</td><td>5958</td><td>1360</td><td>2</td><td>0.7</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>57560</td><td>310971</td><td>9860</td><td>2259</td><td>3</td><td>0.97</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>67775</td><td>366406</td><td>48672</td><td>4578</td><td>6</td><td>3.65</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>77990</td><td>421841</td><td>68845</td><td>5249</td><td>6</td><td>5.21</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>88205</td><td>477276</td><td>132676</td><td>8452</td><td>10</td><td>9.62</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>98420</td><td>532711</td><td>154333</td><td>11317</td><td>13</td><td>10.96</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>108635</td><td>588146</td><td>273046</td><td>17355</td><td>16</td><td>19.42</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>118850</td><td>643581</td><td>279493</td><td>17027</td><td>16</td><td>20.13</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>129065</td><td>699016</td><td>537450</td><td>31304</td><td>29</td><td>37.69</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>139280</td><td>754451</td><td>664081</td><td>40661</td><td>30</td><td>54.45</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>149495</td><td>809886</td><td>828320</td><td>47371</td><td>38</td><td>66.04</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>159710</td><td>865321</td><td>486277</td><td>31817</td><td>29</td><td>36.79</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>169925</td><td>920756</td><td>1246903</td><td>62769</td><td>52</td><td>106.06</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>180140</td><td>976191</td><td>1536490</td><td>85113</td><td>62</td><td>153.06</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>190355</td><td>1031626</td><td>1422824</td><td>79162</td><td>61</td><td>138.35</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>9324400</td><td>533839</td><td>437</td><td>810.67</td><td></td></tr></table><p>
IBM_FV_2002_06_rule
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>753</td><td>3010</td><td>0</td><td>1</td><td>0</td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>12830</td><td>57204</td><td>0</td><td>1</td><td>0</td><td>0.09</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>138255</td><td>615764</td><td>1015406</td><td>123808</td><td>89</td><td>174.21</td><td>SAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>19765</td><td>88084</td><td>358</td><td>69</td><td>0</td><td>0.18</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>26735</td><td>119124</td><td>1673</td><td>291</td><td>0</td><td>0.41</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>33705</td><td>150164</td><td>5390</td><td>1191</td><td>2</td><td>1.07</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>40675</td><td>181204</td><td>28002</td><td>5771</td><td>6</td><td>5.81</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>47645</td><td>212244</td><td>33346</td><td>3631</td><td>5</td><td>3.13</td><td>SAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>54615</td><td>243284</td><td>82375</td><td>11178</td><td>13</td><td>11.72</td><td>SAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>61585</td><td>274324</td><td>65451</td><td>6648</td><td>7</td><td>6.47</td><td>SAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>68555</td><td>305364</td><td>71802</td><td>5398</td><td>6</td><td>5.68</td><td>SAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>75525</td><td>336404</td><td>106399</td><td>9688</td><td>12</td><td>10.17</td><td>SAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>82495</td><td>367444</td><td>121308</td><td>11403</td><td>13</td><td>13.3</td><td>SAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>89465</td><td>398484</td><td>194550</td><td>20028</td><td>20</td><td>21.12</td><td>SAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>96435</td><td>429524</td><td>465575</td><td>50922</td><td>43</td><td>59.48</td><td>SAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>103405</td><td>460564</td><td>553282</td><td>69763</td><td>60</td><td>85.71</td><td>SAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>110375</td><td>491604</td><td>310655</td><td>36044</td><td>30</td><td>38.96</td><td>SAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>117345</td><td>522644</td><td>540945</td><td>56350</td><td>45</td><td>69.47</td><td>SAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>124315</td><td>553684</td><td>861961</td><td>113064</td><td>77</td><td>136.71</td><td>SAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>131285</td><td>584724</td><td>1200414</td><td>174128</td><td>124</td><td>245.71</td><td>SAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>5658892</td><td>699377</td><td>552</td><td>889.4</td><td></td></tr></table><p>
IBM_FV_2002_07_rule
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>23707</td><td>58913</td><td>350395</td><td>24783</td><td>25</td><td>6.46</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k1.cnf</td><td>1257</td><td>3778</td><td>8196</td><td>1344</td><td>2</td><td>0.04</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>8403</td><td>26314</td><td>874236</td><td>74514</td><td>61</td><td>24.06</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>24767</td><td>61378</td><td>322658</td><td>20365</td><td>20</td><td>5.58</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>6747</td><td>19473</td><td>371673</td><td>28998</td><td>29</td><td>4.96</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>7807</td><td>21938</td><td>367612</td><td>27124</td><td>28</td><td>4.35</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>8867</td><td>24403</td><td>310136</td><td>21989</td><td>21</td><td>3.38</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>9927</td><td>26868</td><td>365344</td><td>25605</td><td>27</td><td>4.78</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>10987</td><td>29333</td><td>334194</td><td>24591</td><td>25</td><td>4.4</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>12047</td><td>31798</td><td>371247</td><td>25154</td><td>26</td><td>5.06</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>13107</td><td>34263</td><td>343543</td><td>21770</td><td>21</td><td>4.04</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>14167</td><td>36728</td><td>348801</td><td>24625</td><td>25</td><td>5.14</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>15227</td><td>39193</td><td>334518</td><td>25763</td><td>27</td><td>5.29</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>16287</td><td>41658</td><td>352928</td><td>24608</td><td>25</td><td>5.3</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>17347</td><td>44123</td><td>342480</td><td>26022</td><td>27</td><td>5.67</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>18407</td><td>46588</td><td>327536</td><td>25065</td><td>25</td><td>5.53</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>19467</td><td>49053</td><td>346113</td><td>23704</td><td>24</td><td>5.52</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>20527</td><td>51518</td><td>339884</td><td>24048</td><td>24</td><td>5.86</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>21587</td><td>53983</td><td>378959</td><td>27192</td><td>28</td><td>7.1</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>22647</td><td>56448</td><td>337313</td><td>23480</td><td>23</td><td>5.71</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>7127766</td><td>520744</td><td>513</td><td>118.23</td><td></td></tr></table><p>
IBM_FV_2002_09_rule
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>270</td><td>647</td><td>0</td><td>1</td><td>0</td><td>0</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k10.cnf</td><td>6139</td><td>26305</td><td>438</td><td>37</td><td>0</td><td>0.04</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k100.cnf</td><td>69392</td><td>303954</td><td>1184269</td><td>20526</td><td>21</td><td>16.82</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k15.cnf</td><td>9637</td><td>41644</td><td>3113</td><td>63</td><td>0</td><td>0.08</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k20.cnf</td><td>13152</td><td>57074</td><td>4411</td><td>124</td><td>0</td><td>0.13</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k25.cnf</td><td>16667</td><td>72504</td><td>9222</td><td>139</td><td>0</td><td>0.19</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k30.cnf</td><td>20182</td><td>87934</td><td>9928</td><td>129</td><td>0</td><td>0.22</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k35.cnf</td><td>23697</td><td>103364</td><td>7597</td><td>128</td><td>0</td><td>0.24</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k40.cnf</td><td>27212</td><td>118794</td><td>26154</td><td>258</td><td>0</td><td>0.4</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k45.cnf</td><td>30727</td><td>134224</td><td>36467</td><td>352</td><td>0</td><td>0.52</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k50.cnf</td><td>34242</td><td>149654</td><td>79595</td><td>1189</td><td>2</td><td>1.09</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k55.cnf</td><td>37757</td><td>165084</td><td>174439</td><td>4966</td><td>6</td><td>2.34</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k60.cnf</td><td>41272</td><td>180514</td><td>98781</td><td>875</td><td>1</td><td>1.03</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k65.cnf</td><td>44787</td><td>195944</td><td>40600</td><td>246</td><td>0</td><td>0.74</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k70.cnf</td><td>48302</td><td>211374</td><td>60050</td><td>417</td><td>0</td><td>0.85</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k75.cnf</td><td>51817</td><td>226804</td><td>117720</td><td>531</td><td>1</td><td>1.35</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k80.cnf</td><td>55332</td><td>242234</td><td>535106</td><td>10616</td><td>13</td><td>6.98</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k85.cnf</td><td>58847</td><td>257664</td><td>884578</td><td>19574</td><td>20</td><td>12.99</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k90.cnf</td><td>62362</td><td>273094</td><td>835373</td><td>14791</td><td>14</td><td>11.46</td><td>UNSAT</td></tr>
<tr><td>SAT_dat.k95.cnf</td><td>65877</td><td>288524</td><td>19664</td><td>132</td><td>0</td><td>0.77</td><td>UNSAT</td></tr>
<tr><td>Total (20 / 20)</td><td colspan=2></td><td>4127505</td><td>75094</td><td>78</td><td>58.24</td><td></td></tr></table><p>
IBM_FV_2004_01
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>9275</td><td>38802</td><td>407</td><td>238</td><td>0</td><td>0.1</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k100.cnf</td><td>71789</td><td>306560</td><td>1489855</td><td>269410</td><td>157</td><td>192.86</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k15.cnf</td><td>11524</td><td>48585</td><td>4571</td><td>2165</td><td>3</td><td>0.38</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k20.cnf</td><td>15069</td><td>63760</td><td>11642</td><td>4775</td><td>6</td><td>0.8</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k25.cnf</td><td>18614</td><td>78935</td><td>48265</td><td>12217</td><td>13</td><td>3.38</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k30.cnf</td><td>22159</td><td>94110</td><td>68492</td><td>14124</td><td>14</td><td>4.52</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k35.cnf</td><td>25704</td><td>109285</td><td>366073</td><td>91771</td><td>62</td><td>52.67</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k40.cnf</td><td>29249</td><td>124460</td><td>368041</td><td>85562</td><td>62</td><td>46.69</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k45.cnf</td><td>32794</td><td>139635</td><td>60442</td><td>8110</td><td>9</td><td>3.46</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k50.cnf</td><td>36339</td><td>154810</td><td>439726</td><td>80044</td><td>61</td><td>42.58</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k55.cnf</td><td>39884</td><td>169985</td><td>173628</td><td>29363</td><td>29</td><td>10.79</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k60.cnf</td><td>43429</td><td>185160</td><td>1645591</td><td>361234</td><td>220</td><td>385.03</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k65.cnf</td><td>46974</td><td>200335</td><td>1353426</td><td>277900</td><td>167</td><td>264.84</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k70.cnf</td><td>50519</td><td>215510</td><td>1670236</td><td>342431</td><td>204</td><td>332.17</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k75.cnf</td><td>54064</td><td>230685</td><td>1496251</td><td>286310</td><td>172</td><td>290.82</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k80.cnf</td><td>57609</td><td>245860</td><td>2178170</td><td>470963</td><td>254</td><td>559.57</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k85.cnf</td><td>61154</td><td>261035</td><td>1265807</td><td>215533</td><td>126</td><td>143.07</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k90.cnf</td><td>64699</td><td>276210</td><td>2455215</td><td>498306</td><td>254</td><td>598.46</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_01_SAT_dat.k95.cnf</td><td>68244</td><td>291385</td><td>1247152</td><td>218655</td><td>126</td><td>135.64</td><td>SAT</td></tr>
<tr><td>Total (19 / 19)</td><td colspan=2></td><td>16342990</td><td>3269111</td><td>1939</td><td>3067.83</td><td></td></tr></table><p>
IBM_FV_2004_07
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>9587</td><td>30286</td><td>1018959</td><td>69818</td><td>60</td><td>24.46</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k100.cnf</td><td>25571</td><td>65124</td><td>313113</td><td>20503</td><td>21</td><td>5.46</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k15.cnf</td><td>7976</td><td>23729</td><td>326952</td><td>18879</td><td>18</td><td>2.77</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k20.cnf</td><td>9011</td><td>26164</td><td>290297</td><td>19695</td><td>20</td><td>2.87</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k25.cnf</td><td>10046</td><td>28599</td><td>280621</td><td>18763</td><td>18</td><td>2.8</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k30.cnf</td><td>11081</td><td>31034</td><td>304496</td><td>18339</td><td>17</td><td>2.98</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k35.cnf</td><td>12116</td><td>33469</td><td>312944</td><td>19186</td><td>19</td><td>3.28</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k40.cnf</td><td>13151</td><td>35904</td><td>345843</td><td>18933</td><td>18</td><td>3.55</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k45.cnf</td><td>14186</td><td>38339</td><td>334996</td><td>21088</td><td>21</td><td>4.2</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k50.cnf</td><td>15221</td><td>40774</td><td>318273</td><td>21798</td><td>21</td><td>4.22</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k55.cnf</td><td>16256</td><td>43209</td><td>280594</td><td>16860</td><td>15</td><td>3.14</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k60.cnf</td><td>17291</td><td>45644</td><td>335799</td><td>19843</td><td>20</td><td>4.27</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k65.cnf</td><td>18326</td><td>48079</td><td>348767</td><td>22624</td><td>22</td><td>5.14</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k70.cnf</td><td>19361</td><td>50514</td><td>322309</td><td>20577</td><td>21</td><td>4.52</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k75.cnf</td><td>20396</td><td>52949</td><td>341856</td><td>25176</td><td>26</td><td>5.8</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k80.cnf</td><td>21431</td><td>55384</td><td>341808</td><td>22590</td><td>22</td><td>5.41</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k85.cnf</td><td>22466</td><td>57819</td><td>327364</td><td>19362</td><td>19</td><td>4.83</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k90.cnf</td><td>23501</td><td>60254</td><td>310521</td><td>18422</td><td>17</td><td>4.71</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_07_SAT_dat.k95.cnf</td><td>24536</td><td>62689</td><td>316220</td><td>20213</td><td>20</td><td>5.29</td><td>UNSAT</td></tr>
<tr><td>Total (19 / 19)</td><td colspan=2></td><td>6771732</td><td>432669</td><td>415</td><td>99.7</td><td></td></tr></table><p>
IBM_FV_2004_1_11
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>28280</td><td>111519</td><td>1843</td><td>246</td><td>0</td><td>0.26</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k100.cnf</td><td>329828</td><td>1313030</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k15.cnf</td><td>44993</td><td>178110</td><td>7375</td><td>1066</td><td>2</td><td>1.12</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k20.cnf</td><td>61748</td><td>244870</td><td>22844</td><td>3109</td><td>5</td><td>2.34</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k25.cnf</td><td>78503</td><td>311630</td><td>51424</td><td>10932</td><td>13</td><td>7.77</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k30.cnf</td><td>95258</td><td>378390</td><td>204360</td><td>45498</td><td>37</td><td>45.4</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k35.cnf</td><td>112013</td><td>445150</td><td>446682</td><td>115365</td><td>79</td><td>180.87</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k40.cnf</td><td>128768</td><td>511910</td><td>695119</td><td>142862</td><td>99</td><td>246.01</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k45.cnf</td><td>145523</td><td>578670</td><td>749243</td><td>126557</td><td>91</td><td>185.8</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k50.cnf</td><td>162278</td><td>645430</td><td>1358019</td><td>301274</td><td>187</td><td>700.22</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k55.cnf</td><td>179033</td><td>712190</td><td>1969524</td><td>511947</td><td>254</td><td>1755.22</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k60.cnf</td><td>195788</td><td>778950</td><td>2206710</td><td>548500</td><td>279</td><td>1899.65</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k65.cnf</td><td>212543</td><td>845710</td><td>2181829</td><td>417644</td><td>252</td><td>1028.5</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k70.cnf</td><td>229298</td><td>912470</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k75.cnf</td><td>246053</td><td>979230</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k80.cnf</td><td>262808</td><td>1045990</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k85.cnf</td><td>279563</td><td>1112750</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k90.cnf</td><td>296318</td><td>1179510</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_1_11_SAT_dat.k95.cnf</td><td>313073</td><td>1246270</td></td></tr>
<tr><td>Total (12 / 19)</td><td colspan=2></td><td>9894972</td><td>2225000</td><td>1298</td><td>6053.16</td><td></td></tr></table><p>
IBM_FV_2004_18
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>17141</td><td>69989</td><td>2230</td><td>342</td><td>0</td><td>0.17</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k100.cnf</td><td>177725</td><td>735240</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k15.cnf</td><td>25915</td><td>106325</td><td>16580</td><td>4457</td><td>6</td><td>1.72</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k20.cnf</td><td>34845</td><td>143320</td><td>88112</td><td>26348</td><td>27</td><td>18.16</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k25.cnf</td><td>43775</td><td>180315</td><td>249282</td><td>76855</td><td>61</td><td>103.26</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k30.cnf</td><td>52705</td><td>217310</td><td>558562</td><td>216726</td><td>126</td><td>583.62</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k35.cnf</td><td>61635</td><td>254305</td><td>802080</td><td>278506</td><td>167</td><td>795.54</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k40.cnf</td><td>70565</td><td>291300</td><td>923407</td><td>244754</td><td>141</td><td>493.21</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k45.cnf</td><td>79495</td><td>328295</td><td>1589038</td><td>535100</td><td>268</td><td>2044.35</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k50.cnf</td><td>88425</td><td>365290</td><td>1559717</td><td>409444</td><td>251</td><td>1135.5</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k55.cnf</td><td>97355</td><td>402285</td><td>1572510</td><td>380486</td><td>234</td><td>902.57</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k60.cnf</td><td>106285</td><td>439280</td><td>1912944</td><td>468635</td><td>254</td><td>1155.95</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k65.cnf</td><td>115215</td><td>476275</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k70.cnf</td><td>124145</td><td>513270</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k75.cnf</td><td>133075</td><td>550265</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k80.cnf</td><td>142005</td><td>587260</td><td>4076162</td><td>947987</td><td>507</td><td>3569.23</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k85.cnf</td><td>150935</td><td>624255</td><td>3302114</td><td>562143</td><td>285</td><td>1298.62</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k90.cnf</td><td>159865</td><td>661250</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_18_SAT_dat.k95.cnf</td><td>168795</td><td>698245</td><td>5314611</td><td>1023156</td><td>509</td><td>3492.24</td><td>SAT</td></tr>
<tr><td>Total (14 / 19)</td><td colspan=2></td><td>21967349</td><td>5174939</td><td>2836</td><td>15594.14</td><td></td></tr></table><p>
IBM_FV_2004_20
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>17567</td><td>72087</td><td>1214</td><td>355</td><td>0</td><td>0.19</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k100.cnf</td><td>182021</td><td>756955</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k15.cnf</td><td>26556</td><td>109510</td><td>2638</td><td>714</td><td>1</td><td>0.47</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k20.cnf</td><td>35701</td><td>147595</td><td>84648</td><td>21164</td><td>21</td><td>15.04</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k25.cnf</td><td>44846</td><td>185680</td><td>143924</td><td>30536</td><td>29</td><td>24.53</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k30.cnf</td><td>53991</td><td>223765</td><td>211592</td><td>54721</td><td>45</td><td>56.19</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k35.cnf</td><td>63136</td><td>261850</td><td>651972</td><td>246647</td><td>143</td><td>684.18</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k40.cnf</td><td>72281</td><td>299935</td><td>880345</td><td>334619</td><td>198</td><td>1116.6</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k45.cnf</td><td>81426</td><td>338020</td><td>1045179</td><td>289951</td><td>178</td><td>751.09</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k50.cnf</td><td>90571</td><td>376105</td><td>1148069</td><td>270252</td><td>157</td><td>545.27</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k55.cnf</td><td>99716</td><td>414190</td><td>2008632</td><td>673485</td><td>361</td><td>2791.31</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k60.cnf</td><td>108861</td><td>452275</td><td>2433396</td><td>787345</td><td>412</td><td>3532.3</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k65.cnf</td><td>118006</td><td>490360</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k70.cnf</td><td>127151</td><td>528445</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k75.cnf</td><td>136296</td><td>566530</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k80.cnf</td><td>145441</td><td>604615</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k85.cnf</td><td>154586</td><td>642700</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k90.cnf</td><td>163731</td><td>680785</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_20_SAT_dat.k95.cnf</td><td>172876</td><td>718870</td></td></tr>
<tr><td>Total (11 / 19)</td><td colspan=2></td><td>8611609</td><td>2709789</td><td>1545</td><td>9517.17</td><td></td></tr></table><p>
IBM_FV_2004_2_14
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>12859</td><td>49351</td><td>3559</td><td>461</td><td>0</td><td>0.16</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k100.cnf</td><td>147037</td><td>573435</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k15.cnf</td><td>20302</td><td>78395</td><td>20539</td><td>2672</td><td>4</td><td>0.82</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k20.cnf</td><td>27757</td><td>107515</td><td>52734</td><td>5002</td><td>6</td><td>2.11</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k25.cnf</td><td>35212</td><td>136635</td><td>86483</td><td>11012</td><td>13</td><td>4.99</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k30.cnf</td><td>42667</td><td>165755</td><td>170452</td><td>18895</td><td>18</td><td>9.81</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k35.cnf</td><td>50122</td><td>194875</td><td>331772</td><td>27803</td><td>28</td><td>18.68</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k40.cnf</td><td>57577</td><td>223995</td><td>546579</td><td>52958</td><td>44</td><td>43.46</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k45.cnf</td><td>65032</td><td>253115</td><td>871730</td><td>75679</td><td>61</td><td>70.39</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k50.cnf</td><td>72487</td><td>282235</td><td>633972</td><td>86009</td><td>62</td><td>78.9</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k55.cnf</td><td>79942</td><td>311355</td><td>830288</td><td>105826</td><td>72</td><td>111.6</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k60.cnf</td><td>87397</td><td>340475</td><td>1164020</td><td>134207</td><td>93</td><td>166.54</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k65.cnf</td><td>94852</td><td>369595</td><td>1303081</td><td>164690</td><td>120</td><td>222.43</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k70.cnf</td><td>102307</td><td>398715</td><td>3275361</td><td>354801</td><td>218</td><td>723.79</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k75.cnf</td><td>109762</td><td>427835</td><td>2504998</td><td>293576</td><td>181</td><td>535.31</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k80.cnf</td><td>117217</td><td>456955</td><td>4083053</td><td>470749</td><td>254</td><td>1137.11</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k85.cnf</td><td>124672</td><td>486075</td><td>3470185</td><td>644739</td><td>339</td><td>2018.42</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k90.cnf</td><td>132127</td><td>515195</td><td>4252138</td><td>499759</td><td>254</td><td>1291.93</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_2_14_SAT_dat.k95.cnf</td><td>139582</td><td>544315</td></td></tr>
<tr><td>Total (17 / 19)</td><td colspan=2></td><td>23600944</td><td>2948838</td><td>1767</td><td>6436.45</td><td></td></tr></table><p>
IBM_FV_2004_23
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>18612</td><td>76086</td><td>1</td><td>2</td><td>0</td><td>0.12</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k100.cnf</td><td>207606</td><td>861175</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k15.cnf</td><td>29106</td><td>119635</td><td>4777</td><td>1020</td><td>1</td><td>0.45</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k20.cnf</td><td>39606</td><td>163255</td><td>41941</td><td>10079</td><td>12</td><td>5.47</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k25.cnf</td><td>50106</td><td>206875</td><td>196599</td><td>54802</td><td>45</td><td>66.98</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k30.cnf</td><td>60606</td><td>250495</td><td>384584</td><td>122262</td><td>87</td><td>235.12</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k35.cnf</td><td>71106</td><td>294115</td><td>863012</td><td>292530</td><td>179</td><td>987.2</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k40.cnf</td><td>81606</td><td>337735</td><td>1080025</td><td>247460</td><td>144</td><td>603.56</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k45.cnf</td><td>92106</td><td>381355</td><td>1590715</td><td>270554</td><td>158</td><td>508.2</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k50.cnf</td><td>102606</td><td>424975</td><td>1457010</td><td>297956</td><td>186</td><td>589.43</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k55.cnf</td><td>113106</td><td>468595</td><td>1623910</td><td>216844</td><td>126</td><td>292.6</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k60.cnf</td><td>123606</td><td>512215</td><td>3316789</td><td>673019</td><td>361</td><td>2278.97</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k65.cnf</td><td>134106</td><td>555835</td><td>3967023</td><td>783911</td><td>411</td><td>2564.94</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k70.cnf</td><td>144606</td><td>599455</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k75.cnf</td><td>155106</td><td>643075</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k80.cnf</td><td>165606</td><td>686695</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k85.cnf</td><td>176106</td><td>730315</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k90.cnf</td><td>186606</td><td>773935</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_23_SAT_dat.k95.cnf</td><td>197106</td><td>817555</td></td></tr>
<tr><td>Total (12 / 19)</td><td colspan=2></td><td>14526386</td><td>2970439</td><td>1710</td><td>8133.04</td><td></td></tr></table><p>
IBM_FV_2004_26
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>55591</td><td>277611</td><td>59938</td><td>737</td><td>1</td><td>2.52</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k100.cnf</td><td>493741</td><td>2498691</td><td>79264</td><td>330</td><td>0</td><td>12.81</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k15.cnf</td><td>76731</td><td>385166</td><td>18555</td><td>330</td><td>0</td><td>1</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k20.cnf</td><td>101261</td><td>509491</td><td>31605</td><td>329</td><td>0</td><td>2.37</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k25.cnf</td><td>125791</td><td>633816</td><td>23342</td><td>352</td><td>0</td><td>2.4</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k30.cnf</td><td>150321</td><td>758141</td><td>41889</td><td>354</td><td>0</td><td>3.49</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k35.cnf</td><td>174851</td><td>882466</td><td>39996</td><td>353</td><td>0</td><td>5.41</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k40.cnf</td><td>199381</td><td>1006791</td><td>43296</td><td>355</td><td>0</td><td>5.63</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k45.cnf</td><td>223911</td><td>1131116</td><td>43017</td><td>346</td><td>0</td><td>5.28</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k50.cnf</td><td>248441</td><td>1255441</td><td>49402</td><td>334</td><td>0</td><td>6.17</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k55.cnf</td><td>272971</td><td>1379766</td><td>33179</td><td>363</td><td>0</td><td>3.99</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k60.cnf</td><td>297501</td><td>1504091</td><td>75076</td><td>334</td><td>0</td><td>10.67</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k65.cnf</td><td>322031</td><td>1628416</td><td>72055</td><td>387</td><td>0</td><td>7.27</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k70.cnf</td><td>346561</td><td>1752741</td><td>61701</td><td>350</td><td>0</td><td>8.74</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k75.cnf</td><td>371091</td><td>1877066</td><td>92036</td><td>332</td><td>0</td><td>13.26</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k80.cnf</td><td>395621</td><td>2001391</td><td>57920</td><td>424</td><td>0</td><td>7.01</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k85.cnf</td><td>420151</td><td>2125716</td><td>101646</td><td>330</td><td>0</td><td>15.04</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k90.cnf</td><td>444681</td><td>2250041</td><td>78703</td><td>333</td><td>0</td><td>13.1</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_26_SAT_dat.k95.cnf</td><td>469211</td><td>2374366</td><td>55860</td><td>347</td><td>0</td><td>6.84</td><td>UNSAT</td></tr>
<tr><td>Total (19 / 19)</td><td colspan=2></td><td>1058480</td><td>7020</td><td>1</td><td>133</td><td></td></tr></table><p>
IBM_FV_2004_29
<table border=1><tr><td>CNF</td><td>Vars</td><td>Clauses</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>8356</td><td>36920</td><td>14426</td><td>7761</td><td>9</td><td>1.9</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k100.cnf</td><td>68044</td><td>305308</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k15.cnf</td><td>10754</td><td>47758</td><td>99063</td><td>43474</td><td>34</td><td>21.04</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k20.cnf</td><td>14124</td><td>62908</td><td>401341</td><td>207124</td><td>126</td><td>303.02</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k25.cnf</td><td>17494</td><td>78058</td><td>1273996</td><td>711230</td><td>380</td><td>2824.82</td><td>UNSAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k30.cnf</td><td>20864</td><td>93208</td><td>643228</td><td>246607</td><td>143</td><td>316.87</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k35.cnf</td><td>24234</td><td>108358</td><td>1004585</td><td>391264</td><td>243</td><td>599.25</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k40.cnf</td><td>27604</td><td>123508</td><td>1688014</td><td>683805</td><td>369</td><td>1744.29</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k45.cnf</td><td>30974</td><td>138658</td><td>697780</td><td>189048</td><td>125</td><td>174.13</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k50.cnf</td><td>34344</td><td>153808</td><td>722771</td><td>180509</td><td>125</td><td>125.26</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k55.cnf</td><td>37714</td><td>168958</td><td>1152671</td><td>315588</td><td>189</td><td>332.07</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k60.cnf</td><td>41084</td><td>184108</td><td>2516036</td><td>886610</td><td>475</td><td>2226.63</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k65.cnf</td><td>44454</td><td>199258</td><td>3006027</td><td>934090</td><td>507</td><td>2157.43</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k70.cnf</td><td>47824</td><td>214408</td><td>2539642</td><td>708275</td><td>380</td><td>1150.12</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k75.cnf</td><td>51194</td><td>229558</td><td>3689560</td><td>1085165</td><td>510</td><td>2472.34</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k80.cnf</td><td>54564</td><td>244708</td><td>3839578</td><td>1204674</td><td>536</td><td>2908.34</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k85.cnf</td><td>57934</td><td>259858</td></td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k90.cnf</td><td>61304</td><td>275008</td><td>2094020</td><td>509202</td><td>254</td><td>573.27</td><td>SAT</td></tr>
<tr><td>IBM_FV_2004_rule_batch_29_SAT_dat.k95.cnf</td><td>64674</td><td>290158</td></td></tr>
<tr><td>Total (16 / 19)</td><td colspan=2></td><td>25382738</td><td>8304426</td><td>4405</td><td>17930.78</td><td></td></tr></table><p>