c cleaning 15718 clauses out of 31466 for limit 1.49453449353816E9
c cleaning 8068 clauses out of 16158 for limit 4.3864148664899435E9
c cleaning 3885 clauses out of 7777 for limit 0.30788318284938176
c cleaning 3233 clauses out of 6485 for limit 4.942846414413397
c cleaning 2101 clauses out of 4217 for limit 19.96123269861099
c cleaning 1889 clauses out of 3792 for limit 118.73106491835267
c cleaning 1556 clauses out of 3126 for limit 489.61150869720683
c cleaning 1426 clauses out of 2873 for limit 1961.886175486327
c cleaning 1398 clauses out of 2815 for limit 7869.427535346681
c cleaning 1540 clauses out of 3095 for limit 38359.38566446985
c cleaning 1407 clauses out of 2828 for limit 150032.8571293409
c cleaning 1435 clauses out of 2886 for limit 636691.7274090254
c cleaning 1493 clauses out of 2987 for limit 2860226.302759695
c cleaning 1312 clauses out of 2624 for limit 1.008486508615146E7
c cleaning 1331 clauses out of 2678 for limit 3.87584529684048E7
c cleaning 1275 clauses out of 2573 for limit 1.375462186240033E8
c cleaning 1284 clauses out of 2569 for limit 4.913475582035555E8
c cleaning 1409 clauses out of 2818 for limit 2.0764356049830165E9
c cleaning 1261 clauses out of 2545 for limit 7.164354128919114E9
c cleaning 1880 clauses out of 3769 for limit 5.813001730338732E10
c cleaning 1525 clauses out of 3063 for limit 2.3152421244254172E11
c cleaning 1581 clauses out of 3185 for limit 1.156844183982335E12
c cleaning 1403 clauses out of 2806 for limit 4.370989768063195E12
c cleaning 1504 clauses out of 3013 for limit 2.038131874721453E13
c cleaning 1434 clauses out of 2883 for limit 8.42181986135607E13
c cleaning 1451 clauses out of 2902 for limit 3.580129941815867E14
c cleaning 1300 clauses out of 2602 for limit 1.263025030779303E15
c cleaning 1225 clauses out of 2463 for limit 4.263075337008406E-5
c cleaning 1311 clauses out of 2638 for limit 1.615210435477821E-4
c cleaning 1272 clauses out of 2565 for limit 5.732474213499855E-4
c cleaning 1323 clauses out of 2658 for limit 0.0021676196242604823
c cleaning 1448 clauses out of 2915 for limit 0.00960346802335453
c cleaning 1324 clauses out of 2672 for limit 0.03497976501132224
c cleaning 1532 clauses out of 3074 for limit 0.1709687751026854
c cleaning 1493 clauses out of 3005 for limit 0.7559044681034791
c cleaning 1466 clauses out of 2947 for limit 3.239333397727049
c cleaning 1464 clauses out of 2943 for limit 14.005600556879314
c cleaning 1654 clauses out of 3318 for limit 78.21368876212426
c cleaning 1535 clauses out of 3080 for limit 347.4378317211948
c cleaning 1533 clauses out of 3086 for limit 1620.371308230909
c cleaning 1386 clauses out of 2795 for limit 6198.580952577608
c cleaning 1994 clauses out of 4001 for limit 57910.86560929328
c cleaning 2006 clauses out of 4029 for limit 434824.641485319
c cleaning 1534 clauses out of 3068 for limit 1624504.2935273834
c cleaning 1406 clauses out of 2812 for limit 6366004.622507105
c cleaning 1419 clauses out of 2839 for limit 2.6446746087415148E7
c cleaning 1279 clauses out of 2558 for limit 9.164557424894348E7
c cleaning 1363 clauses out of 2743 for limit 3.697527958366921E8
c cleaning 1542 clauses out of 3085 for limit 1.8101921635740874E9
c cleaning 1469 clauses out of 2941 for limit 7.690105261291788E9
c cleaning 1577 clauses out of 3172 for limit 3.9062869802258965E10
c cleaning 2891 clauses out of 5788 for limit 0.05654909065224466
c cleaning 1913 clauses out of 3842 for limit 0.2192857517191428
c cleaning 1469 clauses out of 2944 for limit 0.7900588084285524
c cleaning 1549 clauses out of 3114 for limit 3.849846506084778
c cleaning 1409 clauses out of 2830 for limit 15.018722098084169
c cleaning 1551 clauses out of 3110 for limit 74.05415216421028
c cleaning 1333 clauses out of 2678 for limit 263.46195224128576
c cleaning 1200 clauses out of 2422 for limit 855.70391720509
c cleaning 1793 clauses out of 3598 for limit 6206.353022096684
c cleaning 1427 clauses out of 2868 for limit 22553.00949489528
c cleaning 1177 clauses out of 2368 for limit 69054.87861628212
c cleaning 1112 clauses out of 2239 for limit 208396.44678251765
c cleaning 1153 clauses out of 2336 for limit 669570.4823550341
c cleaning 1703 clauses out of 3425 for limit 4303124.978176389
c cleaning 1384 clauses out of 2786 for limit 1.5338537450024713E7
c cleaning 1255 clauses out of 2510 for limit 5.158582580121839E7
c cleaning 1150 clauses out of 2310 for limit 1.6106532395057076E8
c cleaning 1037 clauses out of 2097 for limit 4.5305729961483383E8
c cleaning 1022 clauses out of 2053 for limit 1.2497777966709313E9
c cleaning 1080 clauses out of 2161 for limit 3.6776067844462605E9
c cleaning 1088 clauses out of 2195 for limit 1.103650718831186E10
c cleaning 1081 clauses out of 2170 for limit 3.2336458716365738E10
c cleaning 1011 clauses out of 2043 for limit 8.920887377767007E10
c cleaning 994 clauses out of 2004 for limit 2.4050502259690628E11
c cleaning 950 clauses out of 1900 for limit 6.179932698859558E11
c cleaning 949 clauses out of 1898 for limit 1.597196317306798E12
c cleaning 1113 clauses out of 2237 for limit 4.916314860797192E12
c cleaning 998 clauses out of 2014 for limit 1.3303370483342354E13
c cleaning 1024 clauses out of 2049 for limit 3.675613654568273E13
c cleaning 1122 clauses out of 2244 for limit 1.1363675264734439E14
c cleaning 1122 clauses out of 2244 for limit 3.4917329808250575E14
c cleaning 1094 clauses out of 2189 for limit 1.0409795044816428E15
c cleaning 1043 clauses out of 2087 for limit 2.945785846726362E15
c cleaning 998 clauses out of 2004 for limit 8.015990727671373E-5
c cleaning 1044 clauses out of 2098 for limit 2.283159734756698E-4
c cleaning 1087 clauses out of 2201 for limit 6.856567295056789E-4
c cleaning 1108 clauses out of 2237 for limit 0.002074997240596744
c cleaning 1161 clauses out of 2337 for limit 0.006651429897732217
c cleaning 1117 clauses out of 2258 for limit 0.020323173862539966
c cleaning 1770 clauses out of 3568 for limit 0.14583128410115792
c cleaning 1446 clauses out of 2918 for limit 0.5468188094419466
c cleaning 1312 clauses out of 2649 for limit 1.9555419295509155
c cleaning 1284 clauses out of 2584 for limit 6.980600169093542
c cleaning 1334 clauses out of 2696 for limit 27.04231214233829
c cleaning 1283 clauses out of 2579 for limit 95.5241531298155
c cleaning 1204 clauses out of 2418 for limit 313.06206976896834
c cleaning 1109 clauses out of 2236 for limit 941.2088076216489
c cleaning 1085 clauses out of 2189 for limit 2782.0409880866678
c cleaning 1107 clauses out of 2225 for limit 8401.696112144902
c cleaning 1141 clauses out of 2302 for limit 26549.332439775313
c cleaning 2654 clauses out of 5325 for limit 0.03867724972358865
c cleaning 1950 clauses out of 3915 for limit 0.18263166443605758
c cleaning 1530 clauses out of 3065 for limit 0.7011974306799659
c cleaning 1388 clauses out of 2787 for limit 2.698625173745729
c cleaning 1246 clauses out of 2511 for limit 9.111920375518686
c cleaning 1277 clauses out of 2568 for limit 32.81182985557308
c cleaning 1657 clauses out of 3335 for limit 195.28626447088635
c cleaning 1347 clauses out of 2710 for limit 674.8611012240644
c cleaning 1248 clauses out of 2523 for limit 2313.6629630714674
c cleaning 1235 clauses out of 2491 for limit 7910.6092847121845
c cleaning 1193 clauses out of 2397 for limit 25745.039490443407
c cleaning 1107 clauses out of 2227 for limit 77116.43139582724
c cleaning 1073 clauses out of 2164 for limit 225548.62133777342
c cleaning 1050 clauses out of 2118 for limit 643895.024759002
c cleaning 1459 clauses out of 2920 for limit 2979023.843319081
c cleaning 1290 clauses out of 2592 for limit 1.040530104937304E7
c cleaning 1227 clauses out of 2455 for limit 3.482011699878793E7
c cleaning 1760 clauses out of 3534 for limit 2.429961138996712E8
c cleaning 1337 clauses out of 2686 for limit 7.962227879592444E8
c cleaning 1487 clauses out of 2975 for limit 3.657377474599423E9
c cleaning 1186 clauses out of 2393 for limit 1.1244682897006205E10
c cleaning 1088 clauses out of 2187 for limit 3.2799155879942917E10
c cleaning 1506 clauses out of 3031 for limit 1.6353181650943402E11
c cleaning 1287 clauses out of 2574 for limit 5.500250961916094E11
c cleaning 1510 clauses out of 3021 for limit 2.6563404711724497E12
c cleaning 1217 clauses out of 2455 for limit 8.405471550928139E12
c cleaning 1105 clauses out of 2211 for limit 2.4706133999295926E13
c cleaning 1429 clauses out of 2859 for limit 1.1037698315173328E14
c cleaning 1171 clauses out of 2359 for limit 3.388645767574926E14
c cleaning 1409 clauses out of 2833 for limit 1.4631181804680978E15
c cleaning 1148 clauses out of 2307 for limit 4.3466260980986734E-5
c cleaning 1503 clauses out of 3018 for limit 2.1342143233277214E-4
c cleaning 1359 clauses out of 2729 for limit 7.951535893051302E-4
c cleaning 1212 clauses out of 2434 for limit 0.002584964082296402
c cleaning 1655 clauses out of 3322 for limit 0.015482824257584444
c cleaning 1340 clauses out of 2693 for limit 0.053311700929840944
c cleaning 1250 clauses out of 2517 for limit 0.1827878741204896
c cleaning 1206 clauses out of 2428 for limit 0.6054106892460825
c cleaning 1788 clauses out of 3595 for limit 4.3923436582909865
c cleaning 1371 clauses out of 2765 for limit 14.892319694921131
c cleaning 1273 clauses out of 2566 for limit 51.83804727779204
c cleaning 1206 clauses out of 2422 for limit 169.93973611484887