c cleaning 9585 clauses out of 19182 for limit 11269.66386012475
c cleaning 10610 clauses out of 21235 for limit 1.1603810021892016E9
c cleaning 5494 clauses out of 11009 for limit 3.2866807769488106E9
c cleaning 3273 clauses out of 6572 for limit 1.585209939725708E10
c cleaning 2130 clauses out of 4285 for limit 6.520218122057807E10
c cleaning 1876 clauses out of 3756 for limit 3.6909717174942957E11
c cleaning 2970 clauses out of 5952 for limit 0.06479644157983182
c cleaning 2672 clauses out of 5352 for limit 0.7717753060006907
c cleaning 2660 clauses out of 5336 for limit 11.037086195937965
c cleaning 1889 clauses out of 3791 for limit 47.4020472411736
c cleaning 2008 clauses out of 4036 for limit 376.5718495233886
c cleaning 1532 clauses out of 3089 for limit 1422.3225412607123
c cleaning 1279 clauses out of 2579 for limit 4736.26171055701
c cleaning 1346 clauses out of 2706 for limit 18428.194876778358
c cleaning 1202 clauses out of 2420 for limit 59508.32181645713
c cleaning 1233 clauses out of 2488 for limit 206239.87934658115
c cleaning 1276 clauses out of 2578 for limit 747823.6333392236
c cleaning 1154 clauses out of 2308 for limit 2285415.345623018
c cleaning 1233 clauses out of 2484 for limit 8034336.395804538
c cleaning 1069 clauses out of 2151 for limit 2.283083468122903E7
c cleaning 1006 clauses out of 2032 for limit 6.2520822300553344E7
c cleaning 966 clauses out of 1932 for limit 1.6278295583825997E8
c cleaning 1017 clauses out of 2036 for limit 4.505737399134112E8
c cleaning 1658 clauses out of 3316 for limit 2.754245658458837E9
c cleaning 1401 clauses out of 2803 for limit 1.0244955560190296E10
c cleaning 1136 clauses out of 2284 for limit 3.0386204880191086E10
c cleaning 1001 clauses out of 2020 for limit 8.220826051115617E10
c cleaning 940 clauses out of 1903 for limit 2.1131797884806815E11
c cleaning 1573 clauses out of 3146 for limit 1.135417858836705E12
c cleaning 2254 clauses out of 4509 for limit 1.4947231897633604E13
c cleaning 1611 clauses out of 3222 for limit 5.504125872296791E13
c cleaning 1292 clauses out of 2601 for limit 1.835862696116461E14
c cleaning 1116 clauses out of 2232 for limit 5.38692248862136E14
c cleaning 1602 clauses out of 3225 for limit 3.075321534329977E-5
c cleaning 1863 clauses out of 3735 for limit 2.1969415816609363E-4
c cleaning 1353 clauses out of 2730 for limit 7.091817811626112E-4
c cleaning 1250 clauses out of 2509 for limit 0.0023948972427518707
c cleaning 1247 clauses out of 2510 for limit 0.008369279140432492
c cleaning 1218 clauses out of 2448 for limit 0.028083214255105134
c cleaning 1448 clauses out of 2915 for limit 0.12728347011854482
c cleaning 1574 clauses out of 3164 for limit 0.6405316171213291
c cleaning 1420 clauses out of 2864 for limit 2.53146561661101
c cleaning 1326 clauses out of 2682 for limit 9.328500719241172
c cleaning 1472 clauses out of 2956 for limit 41.955126180552384
c cleaning 1529 clauses out of 3076 for limit 198.26491784907378
c cleaning 1356 clauses out of 2727 for limit 728.2340157546223
c cleaning 1411 clauses out of 2838 for limit 3036.4943700614617
c cleaning 1692 clauses out of 3397 for limit 18208.640405574202
c cleaning 1362 clauses out of 2741 for limit 63623.598456231084
c cleaning 1966 clauses out of 3942 for limit 0.013095702281372683
c cleaning 2695 clauses out of 5403 for limit 0.2946336155677429
c cleaning 1931 clauses out of 3866 for limit 1.3116562933892408
c cleaning 1259 clauses out of 2530 for limit 3.6349285738341446
c cleaning 998 clauses out of 2018 for limit 9.622225618781025
c cleaning 959 clauses out of 1930 for limit 25.00605045531014
c cleaning 1060 clauses out of 2134 for limit 72.40110428234328
c cleaning 995 clauses out of 2003 for limit 195.39799096229646
c cleaning 1672 clauses out of 3371 for limit 1234.7914477440938
c cleaning 1298 clauses out of 2612 for limit 3972.724442927252
c cleaning 1118 clauses out of 2254 for limit 11790.94927247919
c cleaning 1232 clauses out of 2478 for limit 41069.19415178664
c cleaning 1748 clauses out of 3512 for limit 279683.377802103
c cleaning 1243 clauses out of 2503 for limit 821986.1778255616
c cleaning 1424 clauses out of 2850 for limit 3542861.9083103943
c cleaning 1378 clauses out of 2756 for limit 1.3861828812314378E7
c cleaning 1032 clauses out of 2086 for limit 3.718945177921265E7
c cleaning 1846 clauses out of 3709 for limit 2.97924354548124E8
c cleaning 1596 clauses out of 3208 for limit 1.322960315280702E9
c cleaning 1204 clauses out of 2433 for limit 3.966187432241988E9
c cleaning 1340 clauses out of 2697 for limit 1.5541669911737587E10
c cleaning 1365 clauses out of 2749 for limit 6.1382458209290184E10
c cleaning 1441 clauses out of 2882 for limit 2.620738433063064E11
c cleaning 1123 clauses out of 2246 for limit 7.524711962838649E11
c cleaning 1292 clauses out of 2586 for limit 2.8246317540245493E12
c cleaning 1030 clauses out of 2060 for limit 7.63060822161963E12
c cleaning 1342 clauses out of 2697 for limit 3.089417180365086E13
c cleaning 1374 clauses out of 2768 for limit 1.2375323333919238E14
c cleaning 1052 clauses out of 2125 for limit 3.3495912462295206E14
c cleaning 1451 clauses out of 2911 for limit 0.0063215207631817805
c cleaning 1473 clauses out of 2956 for limit 0.0278092296394968
c cleaning 1678 clauses out of 3366 for limit 0.16068115577238903
c cleaning 1118 clauses out of 2246 for limit 0.42084955912063426
c cleaning 1272 clauses out of 2560 for limit 1.547096927239504
c cleaning 958 clauses out of 1926 for limit 3.893316567931291
c cleaning 826 clauses out of 1667 for limit 9.052408232242191
c cleaning 842 clauses out of 1709 for limit 21.04330199556689
c cleaning 1179 clauses out of 2374 for limit 68.4202220653875
c cleaning 1305 clauses out of 2631 for limit 259.71871976023897
c cleaning 906 clauses out of 1828 for limit 617.6932004599984
c cleaning 753 clauses out of 1519 for limit 1350.8115559571263
c cleaning 715 clauses out of 1452 for limit 2807.1201507636433
c cleaning 940 clauses out of 1900 for limit 6867.698333801384
c cleaning 1719 clauses out of 3453 for limit 45772.65305949537
c cleaning 1110 clauses out of 2238 for limit 116932.84488412525
c cleaning 1164 clauses out of 2343 for limit 376665.73528090795
c cleaning 979 clauses out of 1974 for limit 990417.0668314482
c cleaning 975 clauses out of 1970 for limit 2632376.5742883775
c cleaning 1458 clauses out of 2938 for limit 1.2331582959697109E7
c cleaning 1168 clauses out of 2354 for limit 3.690009229205949E7
c cleaning 1090 clauses out of 2199 for limit 1.088351320715752E8
c cleaning 1271 clauses out of 2543 for limit 3.9512805050504017E8
c cleaning 1076 clauses out of 2153 for limit 1.1267953990631347E9