[runlim] version:		1.9
[runlim] time limit:		311040000 seconds
[runlim] real time limit:	3600 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/hwmcc15/solvers/blimc/single.blimc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s339rb19.aig
[runlim] start:			Wed Sep 16 03:22:58 2015
[runlim] main pid:		29924
c [blimc] BLIMC Bounded Lingeling Model Checker
c [blimc] 
c [blimc] Version bas 67f8c2b0db74be9343c0b7d4c974e5121193fe90
c [blimc] 
c [blimc] Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c [blimc] All rights reserved.
c [blimc] 
c [blimc] released Tue Sep  8 16:12:24 CEST 2015
c [blimc] compiled Tue Sep  8 16:12:24 CEST 2015
c [blimc] 
c [blimc] gcc (Ubuntu 4.9.2-0ubuntu1~14.04) 4.9.2
c [blimc] -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
c [blimc] -DNLGLFILES -DNLGLDEMA
c [blimc] Linux sili7 3.13.0-63-generic x86_64
c [blimc] 
c [blimc] 0.00 reading /home/biere/hwmcc15/benchmarks/hwmcc14/single/6s339rb19.aig
c [blimc] 0.01 MILOA 16237 365 1594 1 14278
c [blimc] 0.01 BCJK 0 0 0 0 14278
c [blimc] 0.01 1594 latches initialized to 0
c [blimc] 0.01 0 latches initialized to 1
c [blimc] 0.01 0 latches uninitialized
c [blimc] 0.01 literals  in COI:       8675 =  53% out of 16237
c [blimc] 0.01 inputs    in COI:        145 =  40% out of 365
c [blimc] 0.01 latches   in COI:        999 =  63% out of 1594
c [blimc] 0.01 constants in COI:          1 = 100% out of 1
c [blimc] 0.01 ands      in COI:       7530 =  53% out of 14278
c [blimc] 0.02 encoded
c [blimc] 0.92 simplified
c [blimc] 0.92 extracted
c [lglopt]    0.901 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    0.901 100% all
c [lglopt] 
c [lglopt]             0 conflicts,           0.0 confs/sec
c [lglopt]             0 ternaries,           0.0 confs/ternary
c [lglopt]             0 binaries,            0.0 confs/binary
c [lglopt]             0 iterations,          0.0 confs/iteration
c [lglopt] 
c [lglopt]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lglopt]             0 restarts,            0.0 rests/sec,      0.0 confs/restart
c [lglopt]             0 decisions,           0.0 decis/sec,      0.0 decis/conflict
c [lglopt]        152213 propagations,   168872.4 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 0.9 seconds, 1.9 MB
c [blimc] 0.92 mapped 4509 variables
c [blimc] 0.92 maxk 1000
c [blimc] 0.92 bound 0
c [blimc] 0.93 bound 1
c [blimc] 0.94 bound 2
c [blimc] 0.94 bound 3
c [blimc] 0.99 bound 4
c [blimc] 0.99 bound 5
c [blimc] 1.00 bound 6
c [blimc] 1.00 bound 7
c [blimc] 1.18 bound 8
c [blimc] 1.18 bound 9
c [blimc] 1.19 bound 10
c [blimc] 1.19 bound 11
c [blimc] 1.20 bound 12
c [blimc] 1.20 bound 13
c [blimc] 1.21 bound 14
c [blimc] 1.21 bound 15
c [blimc] 1.78 bound 16
c [blimc] 1.79 bound 17
c [blimc] 1.79 bound 18
c [blimc] 1.80 bound 19
c [blimc] 2.10 bound 20
c [blimc] 2.10 bound 21
c [blimc] 2.11 bound 22
c [blimc] 2.80 bound 23
c [blimc] 2.81 bound 24
c [blimc] 2.81 bound 25
c [blimc] 3.14 bound 26
c [blimc] 3.15 bound 27
c [blimc] 3.15 bound 28
c [blimc] 3.96 bound 29
c [blimc] 3.97 bound 30
c [blimc] 3.97 bound 31
c [blimc] 3.98 bound 32
c [blimc] 4.40 bound 33
c [blimc] 4.41 bound 34
c [blimc] 4.41 bound 35
c [blimc] 4.42 bound 36
c [blimc] 5.53 bound 37
c [blimc] 5.53 bound 38
c [blimc] 5.54 bound 39
c [blimc] 5.55 bound 40
c [blimc] 5.55 bound 41
c [blimc] 6.11 bound 42
c [blimc] 6.12 bound 43
c [blimc] 6.13 bound 44
c [blimc] 6.14 bound 45
c [blimc] 6.15 bound 46
c [blimc] 7.60 bound 47
c [blimc] 7.65 bound 48
c [blimc] 7.65 bound 49
[runlim] sample:		10.0 time, 10.2 real, 38.5 MB
c [blimc] 10.25 bound 50
c [blimc] 13.09 bound 51
c [blimc] 16.29 bound 52
[runlim] sample:		20.0 time, 20.2 real, 34.1 MB
c [blimc] 21.20 bound 53
c [blimc] 21.22 bound 54
c [blimc] 21.23 bound 55
c [blimc] 21.24 bound 56
c [blimc] 21.25 bound 57
c [blimc] 21.26 bound 58
c [blimc] 21.27 bound 59
c [blimc] 23.04 bound 60
c [blimc] 23.05 bound 61
c [blimc] 23.06 bound 62
c [blimc] 23.07 bound 63
c [blimc] 23.10 bound 64
c [blimc] 23.11 bound 65
c [blimc] 24.04 bound 66
c [blimc] 24.09 bound 67
c [blimc] 27.79 bound 68
c [blimc] 29.94 bound 69
[runlim] sample:		30.0 time, 30.2 real, 37.7 MB
c [blimc] 31.95 bound 70
c [blimc] 31.98 bound 71
c [blimc] 34.08 bound 72
c [blimc] 34.13 bound 73
c [blimc] 34.18 bound 74
c [blimc] 34.19 bound 75
c [blimc] 37.49 bound 76
c [blimc] 37.52 bound 77
[runlim] sample:		40.0 time, 40.2 real, 60.1 MB
c [blimc] 41.93 bound 78
c [blimc] 46.68 bound 79
[runlim] sample:		49.9 time, 50.2 real, 61.1 MB
c [blimc] 50.05 bound 80
c [blimc] 53.16 bound 81
c [blimc] 55.98 bound 82
[runlim] sample:		59.9 time, 60.2 real, 68.7 MB
c [blimc] 61.79 bound 83
[runlim] sample:		69.9 time, 70.2 real, 64.2 MB
c [blimc] 73.60 bound 84
c [blimc] 78.36 bound 85
[runlim] sample:		79.9 time, 80.2 real, 75.8 MB
c [blimc] 86.10 bound 86
[runlim] sample:		89.9 time, 90.2 real, 72.1 MB
[runlim] sample:		99.9 time, 100.2 real, 71.7 MB
c [blimc] 103.09 bound 87
c [blimc] 108.45 bound 88
[runlim] sample:		109.9 time, 110.2 real, 73.3 MB
c [blimc] 113.62 bound 89
c [blimc] 114.59 bound 90
c [blimc] 114.67 bound 91
[runlim] sample:		119.9 time, 120.2 real, 81.0 MB
c [blimc] 120.54 bound 92
c [blimc] 121.78 bound 93
c [blimc] 125.95 bound 94
[runlim] sample:		129.9 time, 130.2 real, 77.6 MB
c [blimc] 130.46 bound 95
[runlim] sample:		139.9 time, 140.2 real, 79.2 MB
c [blimc] 140.84 bound 96
[runlim] sample:		149.8 time, 150.2 real, 73.6 MB
c [blimc] 156.14 bound 97
[runlim] sample:		159.8 time, 160.2 real, 77.3 MB
c [blimc] 163.45 bound 98
c [blimc] 168.18 bound 99
[runlim] sample:		169.8 time, 170.2 real, 83.7 MB
[runlim] sample:		179.8 time, 180.2 real, 86.2 MB
[runlim] sample:		189.8 time, 190.2 real, 87.2 MB
[runlim] sample:		199.8 time, 200.2 real, 86.2 MB
[runlim] sample:		209.8 time, 210.2 real, 85.8 MB
c [blimc] 215.37 bound 100
[runlim] sample:		219.8 time, 220.2 real, 81.2 MB
c [blimc] 225.46 bound 101
[runlim] sample:		229.8 time, 230.2 real, 79.8 MB
c [blimc] 235.65 bound 102
[runlim] sample:		239.8 time, 240.2 real, 82.2 MB
c [blimc] 245.39 bound 103
[runlim] sample:		249.8 time, 250.2 real, 83.2 MB
c [blimc] 250.49 bound 104
c [blimc] 258.86 bound 105
[runlim] sample:		259.8 time, 260.2 real, 76.3 MB
c [blimc] 269.39 bound 106
[runlim] sample:		269.8 time, 270.2 real, 55.2 MB
[runlim] sample:		279.7 time, 280.2 real, 77.1 MB
c [blimc] 286.52 bound 107
[runlim] sample:		289.7 time, 290.2 real, 87.7 MB
[runlim] sample:		299.7 time, 300.2 real, 91.5 MB
c [blimc] 299.83 bound 108
[runlim] sample:		309.7 time, 310.2 real, 93.7 MB
c [blimc] 315.61 bound 109
[runlim] sample:		319.7 time, 320.2 real, 87.1 MB
[runlim] sample:		329.7 time, 330.2 real, 94.0 MB
c [blimc] 330.30 bound 110
[runlim] sample:		339.7 time, 340.2 real, 94.4 MB
c [blimc] 344.57 bound 111
[runlim] sample:		349.7 time, 350.2 real, 91.9 MB
[runlim] sample:		359.7 time, 360.2 real, 91.9 MB
[runlim] sample:		369.7 time, 370.2 real, 90.4 MB
c [blimc] 371.97 bound 112
[runlim] sample:		379.6 time, 380.2 real, 92.5 MB
c [blimc] 388.57 bound 113
[runlim] sample:		389.6 time, 390.2 real, 95.5 MB
[runlim] sample:		399.6 time, 400.2 real, 99.0 MB
[runlim] sample:		409.6 time, 410.2 real, 97.3 MB
c [blimc] 417.55 bound 114
[runlim] sample:		419.6 time, 420.2 real, 98.5 MB
[runlim] sample:		429.6 time, 430.2 real, 96.9 MB
[runlim] sample:		439.6 time, 440.2 real, 96.5 MB
[runlim] sample:		449.6 time, 450.2 real, 96.0 MB
c [blimc] 452.32 bound 115
[runlim] sample:		459.6 time, 460.2 real, 93.9 MB
[runlim] sample:		469.6 time, 470.2 real, 101.5 MB
[runlim] sample:		479.6 time, 480.2 real, 99.9 MB
c [blimc] 488.75 bound 116
[runlim] sample:		489.6 time, 490.2 real, 70.3 MB
[runlim] sample:		499.6 time, 500.2 real, 107.3 MB
c [blimc] 506.14 bound 117
[runlim] sample:		509.5 time, 510.2 real, 110.0 MB
[runlim] sample:		519.5 time, 520.2 real, 112.5 MB
[runlim] sample:		529.5 time, 530.2 real, 114.2 MB
c [blimc] 535.61 bound 118
[runlim] sample:		539.5 time, 540.2 real, 94.7 MB
[runlim] sample:		549.5 time, 550.2 real, 105.7 MB
c [blimc] 556.97 bound 119
[runlim] sample:		559.5 time, 560.2 real, 110.7 MB
[runlim] sample:		569.5 time, 570.2 real, 109.5 MB
[runlim] sample:		579.5 time, 580.2 real, 114.8 MB
[runlim] sample:		589.5 time, 590.2 real, 122.1 MB
c [blimc] 595.82 bound 120
[runlim] sample:		599.5 time, 600.2 real, 69.0 MB
[runlim] sample:		609.5 time, 610.2 real, 102.0 MB
[runlim] sample:		619.5 time, 620.2 real, 110.1 MB
c [blimc] 622.96 bound 121
[runlim] sample:		629.4 time, 630.2 real, 119.3 MB
[runlim] sample:		639.4 time, 640.2 real, 119.4 MB
[runlim] sample:		649.4 time, 650.2 real, 115.8 MB
[runlim] sample:		659.4 time, 660.2 real, 115.0 MB
c [blimc] 664.24 bound 122
[runlim] sample:		669.4 time, 670.2 real, 109.6 MB
[runlim] sample:		679.4 time, 680.2 real, 110.1 MB
[runlim] sample:		689.4 time, 690.2 real, 109.1 MB
[runlim] sample:		699.4 time, 700.2 real, 106.7 MB
[runlim] sample:		709.4 time, 710.2 real, 108.0 MB
[runlim] sample:		719.4 time, 720.2 real, 100.5 MB
c [blimc] 719.79 bound 123
[runlim] sample:		729.4 time, 730.2 real, 118.7 MB
[runlim] sample:		739.4 time, 740.2 real, 118.6 MB
[runlim] sample:		749.3 time, 750.2 real, 116.0 MB
c [blimc] 756.40 bound 124
[runlim] sample:		759.3 time, 760.2 real, 87.8 MB
[runlim] sample:		769.3 time, 770.2 real, 111.6 MB
[runlim] sample:		779.3 time, 780.2 real, 114.2 MB
[runlim] sample:		789.3 time, 790.2 real, 111.1 MB
[runlim] sample:		799.3 time, 800.2 real, 110.2 MB
[runlim] sample:		809.3 time, 810.2 real, 109.3 MB
c [blimc] 814.65 bound 125
[runlim] sample:		819.3 time, 820.2 real, 120.9 MB
[runlim] sample:		829.3 time, 830.2 real, 120.5 MB
[runlim] sample:		839.3 time, 840.2 real, 119.7 MB
[runlim] sample:		849.3 time, 850.2 real, 118.4 MB
c [blimc] 855.97 bound 126
[runlim] sample:		859.2 time, 860.2 real, 116.4 MB
[runlim] sample:		869.2 time, 870.2 real, 106.5 MB
[runlim] sample:		879.2 time, 880.2 real, 113.2 MB
[runlim] sample:		889.2 time, 890.2 real, 112.3 MB
[runlim] sample:		899.2 time, 900.2 real, 111.8 MB
c [blimc] 907.30 bound 127
[runlim] sample:		909.2 time, 910.2 real, 121.9 MB
[runlim] sample:		919.2 time, 920.2 real, 121.1 MB
[runlim] sample:		929.2 time, 930.2 real, 119.6 MB
c [blimc] 932.37 bound 128
[runlim] sample:		939.2 time, 940.2 real, 117.3 MB
[runlim] sample:		949.2 time, 950.2 real, 116.9 MB
[runlim] sample:		959.1 time, 960.2 real, 115.8 MB
[runlim] sample:		969.1 time, 970.2 real, 114.7 MB
[runlim] sample:		979.1 time, 980.2 real, 114.2 MB
[runlim] sample:		989.1 time, 990.2 real, 114.6 MB
c [blimc] 993.56 bound 129
[runlim] sample:		999.1 time, 1000.2 real, 124.0 MB
[runlim] sample:		1009.1 time, 1010.2 real, 115.0 MB
[runlim] sample:		1019.1 time, 1020.2 real, 123.7 MB
[runlim] sample:		1029.1 time, 1030.2 real, 115.4 MB
[runlim] sample:		1039.1 time, 1040.2 real, 121.4 MB
[runlim] sample:		1049.1 time, 1050.2 real, 115.3 MB
[runlim] sample:		1059.1 time, 1060.2 real, 121.0 MB
[runlim] sample:		1069.1 time, 1070.2 real, 120.6 MB
[runlim] sample:		1079.1 time, 1080.2 real, 121.5 MB
c [blimc] 1085.74 bound 130
[runlim] sample:		1089.0 time, 1090.2 real, 90.2 MB
[runlim] sample:		1099.0 time, 1100.2 real, 116.8 MB
[runlim] sample:		1109.0 time, 1110.2 real, 114.9 MB
[runlim] sample:		1119.0 time, 1120.2 real, 119.4 MB
[runlim] sample:		1129.0 time, 1130.2 real, 118.4 MB
c [blimc] 1135.35 bound 131
[runlim] sample:		1139.0 time, 1140.2 real, 83.8 MB
[runlim] sample:		1149.0 time, 1150.2 real, 120.5 MB
[runlim] sample:		1159.0 time, 1160.2 real, 122.6 MB
[runlim] sample:		1169.0 time, 1170.2 real, 112.8 MB
c [blimc] 1170.09 bound 132
[runlim] sample:		1179.0 time, 1180.2 real, 124.9 MB
[runlim] sample:		1189.0 time, 1190.2 real, 127.3 MB
[runlim] sample:		1199.0 time, 1200.2 real, 135.1 MB
[runlim] sample:		1208.9 time, 1210.2 real, 125.8 MB
c [blimc] 1215.70 bound 133
[runlim] sample:		1218.9 time, 1220.2 real, 89.3 MB
[runlim] sample:		1228.9 time, 1230.2 real, 121.8 MB
[runlim] sample:		1238.9 time, 1240.2 real, 122.9 MB
[runlim] sample:		1248.9 time, 1250.2 real, 120.9 MB
[runlim] sample:		1258.9 time, 1260.2 real, 121.6 MB
[runlim] sample:		1268.9 time, 1270.2 real, 120.6 MB
[runlim] sample:		1278.9 time, 1280.2 real, 120.9 MB
[runlim] sample:		1288.9 time, 1290.2 real, 121.0 MB
[runlim] sample:		1298.9 time, 1300.2 real, 121.5 MB
[runlim] sample:		1308.9 time, 1310.2 real, 121.5 MB
[runlim] sample:		1318.9 time, 1320.2 real, 123.1 MB
[runlim] sample:		1328.8 time, 1330.2 real, 119.5 MB
c [blimc] 1333.28 bound 134
[runlim] sample:		1338.8 time, 1340.2 real, 135.2 MB
[runlim] sample:		1348.8 time, 1350.2 real, 115.8 MB
[runlim] sample:		1358.8 time, 1360.2 real, 131.4 MB
[runlim] sample:		1368.8 time, 1370.2 real, 115.5 MB
c [blimc] 1377.05 bound 135
[runlim] sample:		1378.8 time, 1380.2 real, 89.9 MB
[runlim] sample:		1388.8 time, 1390.2 real, 123.5 MB
[runlim] sample:		1398.8 time, 1400.2 real, 123.3 MB
[runlim] sample:		1408.8 time, 1410.2 real, 122.1 MB
[runlim] sample:		1418.8 time, 1420.2 real, 120.9 MB
[runlim] sample:		1428.8 time, 1430.2 real, 121.4 MB
[runlim] sample:		1438.8 time, 1440.2 real, 119.9 MB
c [blimc] 1443.44 bound 136
[runlim] sample:		1448.7 time, 1450.2 real, 121.1 MB
[runlim] sample:		1458.7 time, 1460.2 real, 131.7 MB
[runlim] sample:		1468.7 time, 1470.2 real, 130.4 MB
c [blimc] 1473.59 bound 137
[runlim] sample:		1478.7 time, 1480.2 real, 128.2 MB
[runlim] sample:		1488.7 time, 1490.2 real, 121.5 MB
[runlim] sample:		1498.7 time, 1500.2 real, 132.7 MB
[runlim] sample:		1508.7 time, 1510.2 real, 133.9 MB
[runlim] sample:		1518.7 time, 1520.2 real, 132.3 MB
[runlim] sample:		1528.7 time, 1530.2 real, 131.5 MB
c [blimc] 1530.70 bound 138
[runlim] sample:		1538.7 time, 1540.2 real, 116.1 MB
[runlim] sample:		1548.7 time, 1550.2 real, 126.3 MB
[runlim] sample:		1558.7 time, 1560.2 real, 126.1 MB
[runlim] sample:		1568.7 time, 1570.2 real, 115.7 MB
[runlim] sample:		1578.6 time, 1580.2 real, 123.9 MB
[runlim] sample:		1588.6 time, 1590.2 real, 124.6 MB
[runlim] sample:		1598.6 time, 1600.2 real, 123.6 MB
[runlim] sample:		1608.6 time, 1610.2 real, 123.6 MB
c [blimc] 1608.94 bound 139
[runlim] sample:		1618.6 time, 1620.2 real, 133.6 MB
[runlim] sample:		1628.6 time, 1630.2 real, 133.2 MB
[runlim] sample:		1638.6 time, 1640.2 real, 131.8 MB
[runlim] sample:		1648.6 time, 1650.2 real, 130.9 MB
[runlim] sample:		1658.6 time, 1660.2 real, 131.8 MB
[runlim] sample:		1668.5 time, 1670.2 real, 129.4 MB
[runlim] sample:		1678.5 time, 1680.2 real, 129.3 MB
[runlim] sample:		1688.5 time, 1690.2 real, 129.3 MB
[runlim] sample:		1698.5 time, 1700.2 real, 129.3 MB
[runlim] sample:		1708.5 time, 1710.2 real, 130.2 MB
c [blimc] 1718.30 bound 140
[runlim] sample:		1718.5 time, 1720.2 real, 80.2 MB
[runlim] sample:		1728.5 time, 1730.2 real, 127.1 MB
[runlim] sample:		1738.5 time, 1740.2 real, 125.4 MB
[runlim] sample:		1748.5 time, 1750.2 real, 126.5 MB
[runlim] sample:		1758.5 time, 1760.2 real, 127.0 MB
[runlim] sample:		1768.5 time, 1770.2 real, 115.4 MB
c [blimc] 1775.93 bound 141
[runlim] sample:		1778.5 time, 1780.2 real, 91.1 MB
[runlim] sample:		1788.5 time, 1790.2 real, 127.7 MB
[runlim] sample:		1798.4 time, 1800.2 real, 132.2 MB
[runlim] sample:		1808.4 time, 1810.2 real, 140.9 MB
[runlim] sample:		1818.4 time, 1820.2 real, 137.9 MB
[runlim] sample:		1828.4 time, 1830.2 real, 140.3 MB
[runlim] sample:		1838.4 time, 1840.2 real, 140.3 MB
[runlim] sample:		1848.4 time, 1850.2 real, 144.0 MB
[runlim] sample:		1858.4 time, 1860.2 real, 143.4 MB
[runlim] sample:		1868.4 time, 1870.2 real, 145.6 MB
c [blimc] 1870.81 bound 142
[runlim] sample:		1878.4 time, 1880.2 real, 137.1 MB
[runlim] sample:		1888.4 time, 1890.2 real, 143.7 MB
[runlim] sample:		1898.4 time, 1900.2 real, 133.1 MB
[runlim] sample:		1908.3 time, 1910.2 real, 142.9 MB
[runlim] sample:		1918.3 time, 1920.2 real, 141.4 MB
c [blimc] 1926.31 bound 143
[runlim] sample:		1928.3 time, 1930.2 real, 96.7 MB
[runlim] sample:		1938.3 time, 1940.2 real, 131.4 MB
[runlim] sample:		1948.3 time, 1950.2 real, 130.9 MB
[runlim] sample:		1958.3 time, 1960.2 real, 120.1 MB
[runlim] sample:		1968.3 time, 1970.2 real, 131.5 MB
[runlim] sample:		1978.3 time, 1980.2 real, 128.2 MB
[runlim] sample:		1988.3 time, 1990.2 real, 127.1 MB
[runlim] sample:		1998.3 time, 2000.2 real, 126.5 MB
[runlim] sample:		2008.3 time, 2010.2 real, 126.0 MB
[runlim] sample:		2018.3 time, 2020.2 real, 128.0 MB
[runlim] sample:		2028.3 time, 2030.2 real, 127.6 MB
c [blimc] 2030.67 bound 144
[runlim] sample:		2038.2 time, 2040.2 real, 137.2 MB
[runlim] sample:		2048.2 time, 2050.2 real, 136.4 MB
[runlim] sample:		2058.2 time, 2060.2 real, 136.7 MB
[runlim] sample:		2068.2 time, 2070.2 real, 137.5 MB
[runlim] sample:		2078.2 time, 2080.2 real, 136.0 MB
[runlim] sample:		2088.2 time, 2090.2 real, 136.6 MB
[runlim] sample:		2098.2 time, 2100.2 real, 136.9 MB
[runlim] sample:		2108.2 time, 2110.2 real, 136.0 MB
c [blimc] 2111.94 bound 145
[runlim] sample:		2118.2 time, 2120.2 real, 118.4 MB
[runlim] sample:		2128.2 time, 2130.2 real, 128.6 MB
[runlim] sample:		2138.2 time, 2140.2 real, 130.9 MB
[runlim] sample:		2148.2 time, 2150.2 real, 130.9 MB
[runlim] sample:		2158.1 time, 2160.2 real, 132.5 MB
[runlim] sample:		2168.1 time, 2170.2 real, 129.3 MB
[runlim] sample:		2178.1 time, 2180.2 real, 130.0 MB
[runlim] sample:		2188.1 time, 2190.2 real, 129.5 MB
[runlim] sample:		2198.1 time, 2200.2 real, 129.4 MB
[runlim] sample:		2208.1 time, 2210.2 real, 129.0 MB
[runlim] sample:		2218.1 time, 2220.2 real, 152.6 MB
[runlim] sample:		2228.1 time, 2230.2 real, 138.4 MB
[runlim] sample:		2238.1 time, 2240.2 real, 138.4 MB
[runlim] sample:		2248.1 time, 2250.2 real, 151.2 MB
c [blimc] 2251.70 bound 146
[runlim] sample:		2258.1 time, 2260.2 real, 140.5 MB
c [blimc] 2258.75 bound 147
[runlim] sample:		2268.1 time, 2270.2 real, 134.4 MB
[runlim] sample:		2278.0 time, 2280.2 real, 131.8 MB
[runlim] sample:		2288.0 time, 2290.2 real, 133.8 MB
[runlim] sample:		2298.0 time, 2300.2 real, 133.6 MB
[runlim] sample:		2308.0 time, 2310.2 real, 133.0 MB
[runlim] sample:		2318.0 time, 2320.2 real, 131.4 MB
[runlim] sample:		2328.0 time, 2330.2 real, 132.4 MB
[runlim] sample:		2338.0 time, 2340.2 real, 132.3 MB
[runlim] sample:		2348.0 time, 2350.2 real, 132.5 MB
[runlim] sample:		2358.0 time, 2360.2 real, 131.9 MB
[runlim] sample:		2367.9 time, 2370.2 real, 123.5 MB
[runlim] sample:		2377.9 time, 2380.2 real, 131.2 MB
[runlim] sample:		2387.9 time, 2390.2 real, 131.2 MB
[runlim] sample:		2397.9 time, 2400.2 real, 134.8 MB
[runlim] sample:		2407.9 time, 2410.2 real, 134.8 MB
[runlim] sample:		2417.9 time, 2420.2 real, 134.8 MB
[runlim] sample:		2427.9 time, 2430.2 real, 137.1 MB
c [blimc] 2435.91 bound 148
[runlim] sample:		2437.9 time, 2440.2 real, 143.0 MB
[runlim] sample:		2447.9 time, 2450.2 real, 141.7 MB
[runlim] sample:		2457.9 time, 2460.2 real, 139.7 MB
[runlim] sample:		2467.9 time, 2470.2 real, 164.1 MB
[runlim] sample:		2477.9 time, 2480.2 real, 164.7 MB
[runlim] sample:		2487.9 time, 2490.2 real, 151.8 MB
[runlim] sample:		2497.9 time, 2500.2 real, 152.4 MB
[runlim] sample:		2507.8 time, 2510.2 real, 164.6 MB
[runlim] sample:		2517.8 time, 2520.2 real, 151.5 MB
[runlim] sample:		2527.8 time, 2530.2 real, 150.2 MB
[runlim] sample:		2537.8 time, 2540.2 real, 150.1 MB
[runlim] sample:		2547.8 time, 2550.2 real, 150.1 MB
c [blimc] 2555.61 bound 149
[runlim] sample:		2557.8 time, 2560.2 real, 103.0 MB
[runlim] sample:		2567.8 time, 2570.2 real, 135.4 MB
[runlim] sample:		2577.8 time, 2580.2 real, 134.7 MB
[runlim] sample:		2587.8 time, 2590.2 real, 134.1 MB
[runlim] sample:		2597.8 time, 2600.2 real, 133.8 MB
[runlim] sample:		2607.8 time, 2610.2 real, 134.8 MB
[runlim] sample:		2617.8 time, 2620.2 real, 133.8 MB
[runlim] sample:		2627.8 time, 2630.2 real, 134.3 MB
[runlim] sample:		2637.7 time, 2640.2 real, 134.7 MB
[runlim] sample:		2647.7 time, 2650.2 real, 135.0 MB
[runlim] sample:		2657.7 time, 2660.2 real, 133.5 MB
[runlim] sample:		2667.7 time, 2670.2 real, 135.6 MB
[runlim] sample:		2677.7 time, 2680.2 real, 135.2 MB
[runlim] sample:		2687.7 time, 2690.2 real, 135.8 MB
[runlim] sample:		2697.7 time, 2700.2 real, 131.7 MB
c [blimc] 2700.72 bound 150
[runlim] sample:		2707.7 time, 2710.2 real, 142.9 MB
[runlim] sample:		2717.7 time, 2720.2 real, 144.4 MB
[runlim] sample:		2727.7 time, 2730.2 real, 142.5 MB
c [blimc] 2734.43 bound 151
[runlim] sample:		2737.7 time, 2740.2 real, 123.5 MB
[runlim] sample:		2747.6 time, 2750.2 real, 139.1 MB
[runlim] sample:		2757.6 time, 2760.2 real, 137.3 MB
[runlim] sample:		2767.6 time, 2770.2 real, 136.7 MB
[runlim] sample:		2777.6 time, 2780.2 real, 138.2 MB
[runlim] sample:		2787.6 time, 2790.2 real, 136.2 MB
[runlim] sample:		2797.6 time, 2800.2 real, 136.1 MB
[runlim] sample:		2807.6 time, 2810.2 real, 136.2 MB
[runlim] sample:		2817.6 time, 2820.2 real, 160.5 MB
[runlim] sample:		2827.6 time, 2830.2 real, 148.3 MB
[runlim] sample:		2837.6 time, 2840.2 real, 161.2 MB
[runlim] sample:		2847.6 time, 2850.2 real, 147.6 MB
[runlim] sample:		2857.6 time, 2860.2 real, 146.1 MB
[runlim] sample:		2867.5 time, 2870.2 real, 148.2 MB
[runlim] sample:		2877.5 time, 2880.2 real, 148.2 MB
c [blimc] 2886.27 bound 152
[runlim] sample:		2887.5 time, 2890.2 real, 148.5 MB
[runlim] sample:		2897.5 time, 2900.2 real, 137.0 MB
c [blimc] 2903.78 bound 153
[runlim] sample:		2907.5 time, 2910.2 real, 105.4 MB
[runlim] sample:		2917.5 time, 2920.2 real, 141.6 MB
[runlim] sample:		2927.5 time, 2930.2 real, 140.5 MB
[runlim] sample:		2937.5 time, 2940.2 real, 139.4 MB
[runlim] sample:		2947.5 time, 2950.2 real, 139.4 MB
[runlim] sample:		2957.5 time, 2960.2 real, 138.1 MB
[runlim] sample:		2967.5 time, 2970.2 real, 139.7 MB
[runlim] sample:		2977.4 time, 2980.2 real, 140.1 MB
[runlim] sample:		2987.4 time, 2990.2 real, 140.8 MB
[runlim] sample:		2997.4 time, 3000.2 real, 140.8 MB
[runlim] sample:		3007.4 time, 3010.2 real, 140.8 MB
[runlim] sample:		3017.4 time, 3020.2 real, 143.3 MB
[runlim] sample:		3027.4 time, 3030.2 real, 153.9 MB
[runlim] sample:		3037.4 time, 3040.2 real, 153.9 MB
[runlim] sample:		3047.4 time, 3050.2 real, 157.3 MB
[runlim] sample:		3057.4 time, 3060.2 real, 158.4 MB
[runlim] sample:		3067.4 time, 3070.2 real, 158.4 MB
[runlim] sample:		3077.4 time, 3080.2 real, 158.4 MB
[runlim] sample:		3087.3 time, 3090.2 real, 158.4 MB
[runlim] sample:		3097.3 time, 3100.2 real, 158.4 MB
[runlim] sample:		3107.3 time, 3110.2 real, 160.7 MB
[runlim] sample:		3117.3 time, 3120.2 real, 160.7 MB
[runlim] sample:		3127.3 time, 3130.2 real, 160.7 MB
[runlim] sample:		3137.3 time, 3140.2 real, 160.7 MB
[runlim] sample:		3147.3 time, 3150.2 real, 160.7 MB
[runlim] sample:		3157.3 time, 3160.2 real, 185.9 MB
[runlim] sample:		3167.3 time, 3170.2 real, 185.9 MB
[runlim] sample:		3177.3 time, 3180.2 real, 185.9 MB
[runlim] sample:		3187.3 time, 3190.2 real, 185.9 MB
[runlim] sample:		3197.3 time, 3200.2 real, 185.9 MB
[runlim] sample:		3207.2 time, 3210.2 real, 185.9 MB
[runlim] sample:		3217.2 time, 3220.2 real, 178.2 MB
[runlim] sample:		3227.2 time, 3230.2 real, 178.2 MB
[runlim] sample:		3237.2 time, 3240.2 real, 178.2 MB
[runlim] sample:		3247.2 time, 3250.2 real, 178.2 MB
[runlim] sample:		3257.2 time, 3260.2 real, 180.6 MB
[runlim] sample:		3267.2 time, 3270.2 real, 180.8 MB
[runlim] sample:		3277.2 time, 3280.2 real, 180.8 MB
[runlim] sample:		3287.2 time, 3290.2 real, 208.8 MB
[runlim] sample:		3297.2 time, 3300.2 real, 209.1 MB
[runlim] sample:		3307.2 time, 3310.2 real, 209.1 MB
[runlim] sample:		3317.2 time, 3320.2 real, 209.3 MB
[runlim] sample:		3327.2 time, 3330.2 real, 211.6 MB
[runlim] sample:		3337.1 time, 3340.2 real, 181.2 MB
[runlim] sample:		3347.1 time, 3350.2 real, 192.2 MB
[runlim] sample:		3357.1 time, 3360.2 real, 214.2 MB
[runlim] sample:		3367.1 time, 3370.2 real, 214.2 MB
[runlim] sample:		3377.1 time, 3380.2 real, 214.2 MB
[runlim] sample:		3387.1 time, 3390.2 real, 214.2 MB
[runlim] sample:		3397.1 time, 3400.2 real, 214.2 MB
[runlim] sample:		3407.1 time, 3410.2 real, 214.2 MB
[runlim] sample:		3417.1 time, 3420.2 real, 214.2 MB
[runlim] sample:		3427.1 time, 3430.2 real, 214.2 MB
[runlim] sample:		3437.1 time, 3440.2 real, 214.2 MB
[runlim] sample:		3447.1 time, 3450.2 real, 214.2 MB
[runlim] sample:		3457.1 time, 3460.2 real, 196.7 MB
[runlim] sample:		3467.1 time, 3470.2 real, 191.7 MB
c [blimc] 3468.98 bound 154
[runlim] sample:		3477.0 time, 3480.2 real, 170.5 MB
[runlim] sample:		3487.0 time, 3490.2 real, 170.5 MB
[runlim] sample:		3497.0 time, 3500.2 real, 170.5 MB
[runlim] sample:		3507.0 time, 3510.2 real, 193.0 MB
[runlim] sample:		3517.0 time, 3520.2 real, 193.0 MB
c [blimc] 3517.66 bound 155
[runlim] sample:		3527.0 time, 3530.2 real, 165.3 MB
[runlim] sample:		3537.0 time, 3540.2 real, 165.3 MB
[runlim] sample:		3547.0 time, 3550.2 real, 165.3 MB
[runlim] sample:		3557.0 time, 3560.2 real, 165.3 MB
[runlim] sample:		3566.9 time, 3570.2 real, 165.3 MB
[runlim] sample:		3576.9 time, 3580.2 real, 165.3 MB
[runlim] sample:		3586.9 time, 3590.2 real, 165.3 MB
s UNKNOWN
c [blimc]
c [blimc] CAUGHT SIGNAL 15
c [blimc]
c [lgl155clone83]  189.864  86% simplifying
c [lgl155clone83]   31.337  14% search
c [lgl155clone83] ==================================
c [lgl155clone83]  221.776 100% all
c [lgl155clone83] 
c [lgl155clone83]        311819 conflicts,        1406.0 confs/sec
c [lgl155clone83]          3954 ternaries,          78.9 confs/ternary
c [lgl155clone83]           819 binaries,          380.7 confs/binary
c [lgl155clone83]           145 iterations,       2150.5 confs/iteration
c [lgl155clone83] 
c [lgl155clone83]             5 reductions,          0.0 redus/sec,  62363.8 confs/reduction
c [lgl155clone83]          6173 restarts,           27.8 rests/sec,     50.5 confs/restart
c [lgl155clone83]        788156 decisions,        3553.8 decis/sec,      2.5 decis/conflict
c [lgl155clone83]     105818854 propagations,   477143.5 props/sec,    134.3 props/decision
c [lgl155clone83] 
c [lgl155clone83] 221.8 seconds, 83.0 MB
c [lgl155]  135.514  93% simplifying
c [lgl155]    8.865   6% search
c [lgl155] ==================================
c [lgl155]  144.941 100% all
c [lgl155] 
c [lgl155]         91755 conflicts,         633.1 confs/sec
c [lgl155]          2326 ternaries,          39.4 confs/ternary
c [lgl155]           633 binaries,          145.0 confs/binary
c [lgl155]           121 iterations,        758.3 confs/iteration
c [lgl155] 
c [lgl155]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lgl155]          2140 restarts,           14.8 rests/sec,     42.9 confs/restart
c [lgl155]        215326 decisions,        1485.6 decis/sec,      2.3 decis/conflict
c [lgl155]      40984791 propagations,   282768.8 props/sec,    190.3 props/decision
c [lgl155] 
c [lgl155] 144.9 seconds, 77.1 MB
c [blimc] 3596.75 reached k = 155
c [blimc] 3596.75 cloned 84 solvers
c [blimc] 3596.75 max 184.9 MB
c [blimc]
c [blimc] CAUGHT SIGNAL 15
c [blimc]
[runlim] end:			Wed Sep 16 04:22:58 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.09 seconds
[runlim] time:			3596.73 seconds
[runlim] space:			246.4 MB
[runlim] samples:		35998
