[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.iproverhc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/6s385rb444.aig
[runlim] start:			Tue Sep 29 05:51:50 2015
[runlim] main pid:		27434
[runlim] sample:		9.3 time, 10.5 real, 617.3 MB
[runlim] sample:		19.3 time, 20.5 real, 1228.3 MB
[runlim] sample:		29.3 time, 30.5 real, 1649.9 MB
[runlim] sample:		39.3 time, 40.5 real, 1895.9 MB
[runlim] sample:		49.3 time, 50.5 real, 2192.0 MB
[runlim] sample:		59.3 time, 60.5 real, 2500.5 MB
[runlim] sample:		69.3 time, 70.5 real, 2640.1 MB
[runlim] sample:		79.3 time, 80.5 real, 2878.3 MB
[runlim] sample:		89.3 time, 90.5 real, 3022.4 MB
[runlim] sample:		99.3 time, 100.5 real, 3379.4 MB
[runlim] sample:		109.3 time, 110.5 real, 3828.7 MB
[runlim] sample:		119.3 time, 120.5 real, 4137.3 MB
[runlim] sample:		129.3 time, 130.5 real, 4502.9 MB
[runlim] sample:		139.3 time, 140.5 real, 4893.7 MB
[runlim] sample:		149.3 time, 150.5 real, 5006.4 MB
[runlim] sample:		159.3 time, 160.5 real, 5018.8 MB
[runlim] sample:		169.3 time, 170.5 real, 5173.5 MB
[runlim] sample:		179.3 time, 180.5 real, 5344.2 MB
[runlim] sample:		189.3 time, 190.5 real, 5497.3 MB
[runlim] sample:		199.3 time, 200.5 real, 5642.3 MB
[runlim] sample:		209.3 time, 210.5 real, 6009.4 MB
[runlim] sample:		219.3 time, 220.5 real, 6194.6 MB
[runlim] sample:		229.3 time, 230.5 real, 6509.6 MB
[runlim] sample:		6.5 time, 240.5 real, 423.2 MB
[runlim] sample:		16.5 time, 250.5 real, 1074.7 MB
[runlim] sample:		26.5 time, 260.5 real, 1550.5 MB
[runlim] sample:		36.5 time, 270.5 real, 1778.6 MB
[runlim] sample:		46.5 time, 280.5 real, 2128.5 MB
[runlim] sample:		56.5 time, 290.5 real, 2412.4 MB
[runlim] sample:		66.5 time, 300.5 real, 2638.9 MB
[runlim] sample:		76.5 time, 310.5 real, 2819.4 MB
[runlim] sample:		86.5 time, 320.5 real, 2989.5 MB
[runlim] sample:		96.5 time, 330.5 real, 3247.5 MB
[runlim] sample:		106.5 time, 340.5 real, 3692.1 MB
[runlim] sample:		116.5 time, 350.5 real, 4060.8 MB
[runlim] sample:		126.5 time, 360.5 real, 4231.9 MB
[runlim] sample:		136.4 time, 370.5 real, 4326.7 MB
[runlim] sample:		146.5 time, 380.5 real, 4613.2 MB
[runlim] sample:		156.4 time, 390.5 real, 4778.9 MB
[runlim] sample:		166.5 time, 400.5 real, 4868.3 MB
[runlim] sample:		176.5 time, 410.5 real, 4872.8 MB
[runlim] sample:		186.4 time, 420.5 real, 4894.6 MB
[runlim] sample:		196.4 time, 430.5 real, 4913.6 MB
[runlim] sample:		206.4 time, 440.5 real, 4917.2 MB
[runlim] sample:		216.4 time, 450.5 real, 4954.4 MB
[runlim] sample:		226.4 time, 460.5 real, 5030.4 MB
[runlim] sample:		236.4 time, 470.5 real, 5083.8 MB
[runlim] sample:		246.4 time, 480.5 real, 5284.6 MB
[runlim] sample:		256.4 time, 490.5 real, 5393.6 MB
[runlim] sample:		266.4 time, 500.5 real, 5575.7 MB
[runlim] sample:		276.4 time, 510.5 real, 5725.8 MB
[runlim] sample:		286.4 time, 520.5 real, 5799.3 MB
[runlim] sample:		296.4 time, 530.5 real, 6047.8 MB
[runlim] sample:		306.4 time, 540.5 real, 6202.2 MB
[runlim] sample:		316.4 time, 550.5 real, 6303.7 MB
[runlim] sample:		326.4 time, 560.5 real, 6501.5 MB
[runlim] sample:		3.5 time, 570.5 real, 242.3 MB
[runlim] sample:		13.5 time, 580.5 real, 917.4 MB
[runlim] sample:		23.5 time, 590.5 real, 1401.7 MB
[runlim] sample:		33.5 time, 600.5 real, 1767.6 MB
[runlim] sample:		43.6 time, 610.5 real, 2077.6 MB
[runlim] sample:		53.5 time, 620.5 real, 2365.7 MB
[runlim] sample:		63.5 time, 630.5 real, 2631.7 MB
[runlim] sample:		73.5 time, 640.5 real, 2809.7 MB
[runlim] sample:		83.5 time, 650.5 real, 3004.6 MB
[runlim] sample:		93.5 time, 660.5 real, 3188.4 MB
[runlim] sample:		103.5 time, 670.5 real, 3588.8 MB
[runlim] sample:		113.5 time, 680.5 real, 4050.7 MB
[runlim] sample:		123.5 time, 690.5 real, 4227.9 MB
[runlim] sample:		133.5 time, 700.5 real, 4381.4 MB
[runlim] sample:		143.5 time, 710.5 real, 4514.5 MB
[runlim] sample:		153.5 time, 720.5 real, 4692.0 MB
[runlim] sample:		163.5 time, 730.5 real, 4892.9 MB
[runlim] sample:		173.5 time, 740.5 real, 4892.9 MB
[runlim] sample:		183.5 time, 750.5 real, 4892.9 MB
[runlim] sample:		193.5 time, 760.5 real, 4892.9 MB
[runlim] sample:		203.5 time, 770.5 real, 4984.2 MB
[runlim] sample:		213.5 time, 780.5 real, 5069.5 MB
[runlim] sample:		223.5 time, 790.5 real, 5159.3 MB
[runlim] sample:		233.5 time, 800.5 real, 5199.8 MB
[runlim] sample:		243.5 time, 810.5 real, 5206.7 MB
[runlim] sample:		253.5 time, 820.5 real, 5380.0 MB
[runlim] sample:		263.5 time, 830.5 real, 5608.1 MB
[runlim] sample:		273.5 time, 840.5 real, 5652.1 MB
[runlim] sample:		283.5 time, 850.5 real, 5716.8 MB
[runlim] sample:		293.5 time, 860.5 real, 5821.1 MB
[runlim] sample:		303.5 time, 870.5 real, 5991.1 MB
[runlim] sample:		313.5 time, 880.5 real, 6076.9 MB
[runlim] sample:		323.4 time, 890.5 real, 6135.1 MB
[runlim] sample:		333.4 time, 900.5 real, 6171.2 MB
[runlim] sample:		343.4 time, 910.5 real, 6261.7 MB
[runlim] sample:		353.4 time, 920.5 real, 6386.3 MB
[runlim] sample:		363.4 time, 930.5 real, 6548.0 MB
[runlim] sample:		373.4 time, 940.5 real, 6646.4 MB
[runlim] sample:		7.8 time, 950.5 real, 512.0 MB
[runlim] sample:		17.8 time, 960.5 real, 1164.7 MB
[runlim] sample:		27.8 time, 970.5 real, 1485.0 MB
[runlim] sample:		37.8 time, 980.5 real, 1989.0 MB
[runlim] sample:		47.8 time, 990.5 real, 2281.4 MB
[runlim] sample:		57.8 time, 1000.5 real, 2595.1 MB
[runlim] sample:		67.8 time, 1010.5 real, 2942.9 MB
[runlim] sample:		77.8 time, 1020.5 real, 3044.7 MB
[runlim] sample:		87.8 time, 1030.5 real, 3548.9 MB
[runlim] sample:		97.8 time, 1040.5 real, 3925.1 MB
[runlim] sample:		107.8 time, 1050.5 real, 4048.0 MB
[runlim] sample:		117.7 time, 1060.5 real, 4550.3 MB
[runlim] sample:		127.8 time, 1070.5 real, 4774.8 MB
[runlim] sample:		137.7 time, 1080.5 real, 4966.9 MB
[runlim] sample:		147.7 time, 1090.5 real, 5517.7 MB
[runlim] sample:		157.7 time, 1100.5 real, 5716.3 MB
[runlim] sample:		167.7 time, 1110.5 real, 5828.4 MB
[runlim] sample:		177.7 time, 1120.5 real, 6209.6 MB
[runlim] sample:		187.7 time, 1130.5 real, 6219.9 MB
[runlim] sample:		197.7 time, 1140.5 real, 6223.4 MB
[runlim] sample:		0.0 time, 1150.5 real, 2.7 MB
[runlim] sample:		9.8 time, 1160.5 real, 675.4 MB
[runlim] sample:		19.8 time, 1170.5 real, 1270.1 MB
[runlim] sample:		29.7 time, 1180.5 real, 1705.3 MB
[runlim] sample:		39.7 time, 1190.5 real, 1951.3 MB
[runlim] sample:		49.7 time, 1200.5 real, 2253.6 MB
[runlim] sample:		59.7 time, 1210.5 real, 2557.0 MB
[runlim] sample:		69.7 time, 1220.5 real, 2696.9 MB
[runlim] sample:		79.7 time, 1230.5 real, 2931.4 MB
[runlim] sample:		89.7 time, 1240.5 real, 3077.6 MB
[runlim] sample:		99.7 time, 1250.5 real, 3431.4 MB
[runlim] sample:		109.7 time, 1260.5 real, 3899.5 MB
[runlim] sample:		119.7 time, 1270.5 real, 4202.5 MB
[runlim] sample:		129.7 time, 1280.5 real, 4350.2 MB
[runlim] sample:		139.7 time, 1290.5 real, 4687.0 MB
[runlim] sample:		149.7 time, 1300.5 real, 4798.9 MB
[runlim] sample:		159.7 time, 1310.5 real, 4948.7 MB
[runlim] sample:		169.7 time, 1320.5 real, 4954.2 MB
[runlim] sample:		179.7 time, 1330.5 real, 5006.2 MB
[runlim] sample:		189.7 time, 1340.5 real, 5056.3 MB
[runlim] sample:		199.7 time, 1350.5 real, 5090.8 MB
[runlim] sample:		209.7 time, 1360.5 real, 5205.6 MB
[runlim] sample:		219.7 time, 1370.5 real, 5333.8 MB
[runlim] sample:		229.7 time, 1380.5 real, 5486.5 MB
[runlim] sample:		239.7 time, 1390.5 real, 5708.7 MB
[runlim] sample:		249.7 time, 1400.5 real, 5795.0 MB
[runlim] sample:		259.7 time, 1410.5 real, 5855.4 MB
[runlim] sample:		269.7 time, 1420.5 real, 5948.4 MB
[runlim] sample:		279.7 time, 1430.5 real, 6031.6 MB
[runlim] sample:		289.7 time, 1440.5 real, 6182.4 MB
[runlim] sample:		299.7 time, 1450.5 real, 6510.1 MB
[runlim] end:			Tue Sep 29 06:16:06 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		87335
[runlim] real:			1456.99 seconds
[runlim] time:			375.23 seconds
[runlim] space:			6664.1 MB
[runlim] samples:		14564
