[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/iprover/single.iprover
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s148.aig
[runlim] start:			Tue Sep 15 17:00:14 2015
[runlim] main pid:		25716
[runlim] sample:		9.3 time, 10.6 real, 504.5 MB
[runlim] sample:		19.2 time, 20.6 real, 742.3 MB
[runlim] sample:		29.2 time, 30.6 real, 1000.9 MB
[runlim] sample:		39.2 time, 40.6 real, 1387.3 MB
[runlim] sample:		49.2 time, 50.6 real, 1483.1 MB
[runlim] sample:		59.2 time, 60.6 real, 1748.7 MB
[runlim] sample:		69.2 time, 70.6 real, 1990.4 MB
[runlim] sample:		79.2 time, 80.6 real, 2143.1 MB
[runlim] sample:		89.2 time, 90.6 real, 2397.5 MB
[runlim] sample:		99.2 time, 100.6 real, 2476.4 MB
[runlim] sample:		109.1 time, 110.6 real, 2536.8 MB
[runlim] sample:		119.1 time, 120.6 real, 2551.1 MB
[runlim] sample:		129.1 time, 130.6 real, 2642.3 MB
[runlim] sample:		139.1 time, 140.6 real, 2681.6 MB
[runlim] sample:		149.1 time, 150.6 real, 2700.4 MB
[runlim] sample:		159.1 time, 160.6 real, 2701.7 MB
[runlim] sample:		169.1 time, 170.6 real, 2723.5 MB
[runlim] sample:		179.1 time, 180.6 real, 2846.1 MB
[runlim] sample:		189.0 time, 190.6 real, 2880.9 MB
[runlim] sample:		199.0 time, 200.6 real, 2973.9 MB
[runlim] sample:		209.0 time, 210.6 real, 2974.7 MB
[runlim] sample:		219.0 time, 220.6 real, 3096.6 MB
[runlim] sample:		229.0 time, 230.6 real, 3146.2 MB
[runlim] sample:		239.0 time, 240.6 real, 3164.9 MB
[runlim] sample:		249.0 time, 250.6 real, 3189.4 MB
[runlim] sample:		259.0 time, 260.6 real, 3199.9 MB
[runlim] sample:		268.9 time, 270.6 real, 3249.1 MB
[runlim] sample:		278.9 time, 280.6 real, 3251.9 MB
[runlim] sample:		288.9 time, 290.6 real, 3289.3 MB
[runlim] sample:		298.9 time, 300.6 real, 3290.6 MB
[runlim] sample:		308.9 time, 310.6 real, 3296.0 MB
[runlim] sample:		318.9 time, 320.6 real, 3433.2 MB
[runlim] sample:		328.9 time, 330.6 real, 3439.4 MB
[runlim] sample:		338.9 time, 340.6 real, 3536.7 MB
[runlim] sample:		348.9 time, 350.6 real, 3536.7 MB
[runlim] sample:		358.9 time, 360.6 real, 3562.6 MB
[runlim] sample:		368.8 time, 370.6 real, 3680.1 MB
[runlim] sample:		378.8 time, 380.6 real, 3682.4 MB
[runlim] sample:		388.8 time, 390.6 real, 3682.9 MB
[runlim] sample:		398.8 time, 400.6 real, 3699.4 MB
[runlim] sample:		408.8 time, 410.6 real, 3699.9 MB
[runlim] sample:		418.8 time, 420.6 real, 3726.4 MB
[runlim] sample:		428.8 time, 430.6 real, 3726.9 MB
[runlim] sample:		438.8 time, 440.6 real, 3759.1 MB
[runlim] sample:		448.8 time, 450.6 real, 3779.1 MB
[runlim] sample:		458.8 time, 460.6 real, 3807.1 MB
[runlim] sample:		468.7 time, 470.6 real, 3839.3 MB
[runlim] sample:		478.7 time, 480.6 real, 3865.3 MB
[runlim] sample:		488.7 time, 490.6 real, 3869.3 MB
[runlim] sample:		498.7 time, 500.6 real, 3871.3 MB
[runlim] sample:		508.7 time, 510.6 real, 3873.3 MB
[runlim] sample:		518.7 time, 520.6 real, 3875.3 MB
[runlim] sample:		528.7 time, 530.6 real, 4001.4 MB
[runlim] sample:		538.7 time, 540.6 real, 4005.4 MB
[runlim] sample:		548.7 time, 550.6 real, 4007.4 MB
[runlim] sample:		558.6 time, 560.6 real, 4009.4 MB
[runlim] sample:		568.6 time, 570.6 real, 4057.6 MB
[runlim] sample:		578.6 time, 580.6 real, 4096.1 MB
[runlim] sample:		588.6 time, 590.6 real, 4174.6 MB
[runlim] sample:		598.6 time, 600.6 real, 4174.6 MB
[runlim] sample:		608.6 time, 610.6 real, 4174.6 MB
[runlim] sample:		618.6 time, 620.6 real, 4174.6 MB
[runlim] sample:		628.6 time, 630.6 real, 4174.6 MB
[runlim] sample:		638.6 time, 640.6 real, 4174.6 MB
[runlim] sample:		648.5 time, 650.6 real, 4176.6 MB
[runlim] sample:		658.5 time, 660.6 real, 4176.6 MB
[runlim] sample:		668.5 time, 670.6 real, 4176.6 MB
[runlim] sample:		678.5 time, 680.6 real, 4192.6 MB
[runlim] sample:		688.5 time, 690.6 real, 4305.9 MB
[runlim] sample:		698.5 time, 700.6 real, 4305.9 MB
[runlim] sample:		708.5 time, 710.6 real, 4305.9 MB
[runlim] sample:		718.5 time, 720.6 real, 4322.2 MB
[runlim] sample:		728.4 time, 730.6 real, 4322.2 MB
[runlim] sample:		738.4 time, 740.6 real, 4322.2 MB
[runlim] sample:		748.4 time, 750.6 real, 4322.2 MB
[runlim] sample:		758.4 time, 760.6 real, 4346.2 MB
[runlim] sample:		768.4 time, 770.6 real, 4377.4 MB
[runlim] sample:		778.4 time, 780.6 real, 4377.4 MB
[runlim] sample:		788.4 time, 790.6 real, 4377.4 MB
[runlim] sample:		798.4 time, 800.6 real, 4377.4 MB
[runlim] sample:		808.4 time, 810.6 real, 4399.6 MB
[runlim] sample:		818.3 time, 820.6 real, 4427.6 MB
[runlim] sample:		828.3 time, 830.6 real, 4427.6 MB
[runlim] sample:		838.3 time, 840.6 real, 4479.8 MB
[runlim] sample:		848.3 time, 850.6 real, 4479.8 MB
[runlim] sample:		858.3 time, 860.6 real, 4520.0 MB
[runlim] sample:		868.3 time, 870.6 real, 4522.0 MB
[runlim] sample:		878.3 time, 880.6 real, 4522.0 MB
[runlim] sample:		888.3 time, 890.6 real, 4524.0 MB
[runlim] sample:		898.3 time, 900.6 real, 4526.0 MB
[runlim] sample:		9.2 time, 910.6 real, 506.6 MB
[runlim] sample:		19.2 time, 920.6 real, 744.2 MB
[runlim] sample:		29.2 time, 930.6 real, 997.8 MB
[runlim] sample:		39.2 time, 940.6 real, 1271.8 MB
[runlim] sample:		49.2 time, 950.6 real, 1458.5 MB
[runlim] sample:		59.2 time, 960.6 real, 1586.6 MB
[runlim] sample:		69.2 time, 970.6 real, 1718.4 MB
[runlim] sample:		79.2 time, 980.6 real, 1900.0 MB
[runlim] sample:		89.2 time, 990.6 real, 2131.5 MB
[runlim] sample:		99.2 time, 1000.6 real, 2278.6 MB
[runlim] sample:		109.1 time, 1010.6 real, 2444.0 MB
[runlim] sample:		119.1 time, 1020.6 real, 2505.7 MB
[runlim] sample:		129.1 time, 1030.6 real, 2542.3 MB
[runlim] sample:		139.1 time, 1040.6 real, 2585.0 MB
[runlim] sample:		149.1 time, 1050.6 real, 2734.4 MB
[runlim] sample:		159.1 time, 1060.6 real, 2852.8 MB
[runlim] sample:		169.1 time, 1070.6 real, 3065.5 MB
[runlim] sample:		179.1 time, 1080.6 real, 3121.9 MB
[runlim] sample:		189.0 time, 1090.6 real, 3188.2 MB
[runlim] sample:		199.0 time, 1100.6 real, 3363.6 MB
[runlim] sample:		209.0 time, 1110.6 real, 3508.7 MB
[runlim] sample:		219.0 time, 1120.6 real, 3571.8 MB
[runlim] sample:		229.0 time, 1130.6 real, 3643.2 MB
[runlim] sample:		239.0 time, 1140.6 real, 3836.0 MB
[runlim] sample:		249.0 time, 1150.6 real, 3896.9 MB
[runlim] sample:		259.0 time, 1160.6 real, 3951.1 MB
[runlim] sample:		268.9 time, 1170.6 real, 3971.1 MB
[runlim] sample:		278.9 time, 1180.6 real, 4011.5 MB
[runlim] sample:		288.9 time, 1190.6 real, 4065.5 MB
[runlim] sample:		298.9 time, 1200.6 real, 4147.4 MB
[runlim] sample:		308.9 time, 1210.6 real, 4285.5 MB
[runlim] sample:		318.9 time, 1220.6 real, 4389.7 MB
[runlim] sample:		328.9 time, 1230.6 real, 4437.6 MB
[runlim] sample:		338.9 time, 1240.6 real, 4462.7 MB
[runlim] sample:		348.9 time, 1250.6 real, 4503.0 MB
[runlim] sample:		358.9 time, 1260.6 real, 4556.1 MB
[runlim] sample:		368.8 time, 1270.6 real, 4566.3 MB
[runlim] sample:		378.8 time, 1280.6 real, 4727.7 MB
[runlim] sample:		388.8 time, 1290.6 real, 4860.3 MB
[runlim] sample:		398.8 time, 1300.6 real, 4899.2 MB
[runlim] sample:		408.8 time, 1310.6 real, 4919.2 MB
[runlim] sample:		418.8 time, 1320.6 real, 4939.9 MB
[runlim] sample:		428.8 time, 1330.6 real, 4972.6 MB
[runlim] sample:		438.8 time, 1340.6 real, 5006.0 MB
[runlim] sample:		448.7 time, 1350.6 real, 5006.0 MB
[runlim] sample:		458.7 time, 1360.6 real, 5025.4 MB
[runlim] sample:		468.7 time, 1370.6 real, 5027.4 MB
[runlim] sample:		478.7 time, 1380.6 real, 5027.4 MB
[runlim] sample:		488.7 time, 1390.6 real, 5030.4 MB
[runlim] sample:		498.7 time, 1400.6 real, 5030.4 MB
[runlim] sample:		508.7 time, 1410.6 real, 5069.2 MB
[runlim] sample:		518.7 time, 1420.6 real, 5089.3 MB
[runlim] sample:		528.7 time, 1430.6 real, 5089.6 MB
[runlim] sample:		538.7 time, 1440.6 real, 5140.1 MB
[runlim] sample:		548.6 time, 1450.6 real, 5159.3 MB
[runlim] sample:		558.6 time, 1460.6 real, 5252.1 MB
[runlim] sample:		568.6 time, 1470.6 real, 5252.7 MB
[runlim] sample:		578.6 time, 1480.6 real, 5253.2 MB
[runlim] sample:		588.6 time, 1490.6 real, 5254.0 MB
[runlim] sample:		598.6 time, 1500.6 real, 5268.5 MB
[runlim] sample:		608.6 time, 1510.6 real, 5269.0 MB
[runlim] sample:		618.6 time, 1520.6 real, 5269.5 MB
[runlim] sample:		628.6 time, 1530.6 real, 5287.4 MB
[runlim] sample:		638.5 time, 1540.6 real, 5289.9 MB
[runlim] sample:		648.5 time, 1550.6 real, 5331.9 MB
[runlim] sample:		658.5 time, 1560.6 real, 5356.1 MB
[runlim] sample:		668.5 time, 1570.6 real, 5356.8 MB
[runlim] sample:		678.5 time, 1580.6 real, 5357.1 MB
[runlim] sample:		688.5 time, 1590.6 real, 5357.4 MB
[runlim] sample:		698.5 time, 1600.6 real, 5358.6 MB
[runlim] sample:		708.5 time, 1610.6 real, 5416.7 MB
[runlim] sample:		718.5 time, 1620.6 real, 5416.7 MB
[runlim] sample:		728.4 time, 1630.6 real, 5447.1 MB
[runlim] sample:		738.4 time, 1640.6 real, 5611.3 MB
[runlim] sample:		748.4 time, 1650.6 real, 5635.5 MB
[runlim] sample:		758.4 time, 1660.6 real, 5641.7 MB
[runlim] sample:		768.4 time, 1670.6 real, 5643.7 MB
[runlim] sample:		778.4 time, 1680.6 real, 5726.5 MB
[runlim] sample:		788.4 time, 1690.6 real, 5732.5 MB
[runlim] sample:		798.4 time, 1700.6 real, 5733.3 MB
[runlim] sample:		808.4 time, 1710.6 real, 5734.4 MB
[runlim] sample:		818.3 time, 1720.6 real, 5755.0 MB
[runlim] sample:		828.3 time, 1730.6 real, 5757.0 MB
[runlim] sample:		838.3 time, 1740.6 real, 5773.0 MB
[runlim] sample:		848.3 time, 1750.6 real, 5773.1 MB
[runlim] sample:		858.3 time, 1760.6 real, 5773.3 MB
[runlim] sample:		868.3 time, 1770.6 real, 5773.3 MB
[runlim] sample:		878.3 time, 1780.6 real, 5773.3 MB
[runlim] sample:		888.2 time, 1790.6 real, 5774.4 MB
[runlim] sample:		898.2 time, 1800.6 real, 5801.8 MB
[runlim] sample:		9.0 time, 1810.6 real, 513.8 MB
[runlim] sample:		19.0 time, 1820.6 real, 742.9 MB
[runlim] sample:		29.0 time, 1830.6 real, 988.8 MB
[runlim] sample:		39.0 time, 1840.6 real, 1262.2 MB
[runlim] sample:		49.0 time, 1850.6 real, 1455.3 MB
[runlim] sample:		59.0 time, 1860.6 real, 1585.0 MB
[runlim] sample:		68.9 time, 1870.6 real, 1655.6 MB
[runlim] sample:		78.9 time, 1880.6 real, 1791.0 MB
[runlim] sample:		88.9 time, 1890.6 real, 1972.5 MB
[runlim] sample:		98.9 time, 1900.6 real, 2158.9 MB
[runlim] sample:		108.9 time, 1910.6 real, 2351.5 MB
[runlim] sample:		118.9 time, 1920.6 real, 2372.3 MB
[runlim] sample:		128.9 time, 1930.6 real, 2376.6 MB
[runlim] sample:		138.9 time, 1940.6 real, 2438.9 MB
[runlim] sample:		148.9 time, 1950.6 real, 2554.1 MB
[runlim] sample:		158.8 time, 1960.6 real, 2667.5 MB
[runlim] sample:		168.8 time, 1970.6 real, 2792.3 MB
[runlim] sample:		178.8 time, 1980.6 real, 2948.2 MB
[runlim] sample:		188.8 time, 1990.6 real, 3051.8 MB
[runlim] sample:		198.8 time, 2000.6 real, 3154.6 MB
[runlim] sample:		208.8 time, 2010.6 real, 3244.9 MB
[runlim] sample:		218.8 time, 2020.6 real, 3359.7 MB
[runlim] sample:		228.8 time, 2030.6 real, 3490.4 MB
[runlim] sample:		238.8 time, 2040.6 real, 3630.1 MB
[runlim] sample:		248.8 time, 2050.6 real, 3775.5 MB
[runlim] sample:		258.7 time, 2060.6 real, 3914.6 MB
[runlim] sample:		268.7 time, 2070.6 real, 4000.3 MB
[runlim] sample:		278.7 time, 2080.6 real, 4000.3 MB
[runlim] sample:		288.7 time, 2090.6 real, 4000.3 MB
[runlim] sample:		298.7 time, 2100.6 real, 4000.8 MB
[runlim] sample:		308.7 time, 2110.6 real, 4080.8 MB
[runlim] sample:		318.7 time, 2120.6 real, 4081.0 MB
[runlim] sample:		328.6 time, 2130.6 real, 4146.0 MB
[runlim] sample:		338.6 time, 2140.6 real, 4222.0 MB
[runlim] sample:		348.6 time, 2150.6 real, 4346.8 MB
[runlim] sample:		358.6 time, 2160.6 real, 4373.6 MB
[runlim] sample:		368.6 time, 2170.6 real, 4493.7 MB
[runlim] sample:		378.6 time, 2180.6 real, 4587.4 MB
[runlim] sample:		388.6 time, 2190.6 real, 4747.9 MB
[runlim] sample:		398.6 time, 2200.6 real, 4888.8 MB
[runlim] sample:		408.5 time, 2210.6 real, 5033.4 MB
[runlim] sample:		418.5 time, 2220.6 real, 5220.2 MB
[runlim] sample:		428.5 time, 2230.6 real, 5354.6 MB
[runlim] sample:		438.5 time, 2240.6 real, 5471.2 MB
[runlim] sample:		448.5 time, 2250.6 real, 5583.8 MB
[runlim] sample:		458.5 time, 2260.6 real, 5686.2 MB
[runlim] sample:		468.5 time, 2270.6 real, 5772.4 MB
[runlim] sample:		478.5 time, 2280.6 real, 5832.6 MB
[runlim] sample:		488.5 time, 2290.6 real, 5902.9 MB
[runlim] sample:		498.4 time, 2300.6 real, 5997.0 MB
[runlim] sample:		508.4 time, 2310.6 real, 6110.1 MB
[runlim] sample:		518.4 time, 2320.6 real, 6203.1 MB
[runlim] sample:		528.4 time, 2330.6 real, 6267.2 MB
[runlim] sample:		538.4 time, 2340.6 real, 6297.2 MB
[runlim] sample:		548.4 time, 2350.6 real, 6387.2 MB
[runlim] sample:		558.4 time, 2360.6 real, 6483.4 MB
[runlim] sample:		568.4 time, 2370.6 real, 6549.7 MB
[runlim] sample:		578.4 time, 2380.6 real, 6621.8 MB
[runlim] sample:		588.4 time, 2390.6 real, 6622.0 MB
[runlim] sample:		598.3 time, 2400.6 real, 6688.0 MB
[runlim] sample:		608.3 time, 2410.6 real, 6688.0 MB
[runlim] end:			Tue Sep 15 17:40:25 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		144637
[runlim] real:			2411.82 seconds
[runlim] time:			898.93 seconds
[runlim] space:			6688.0 MB
[runlim] samples:		24112
