[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/intel009.aig
[runlim] start:			Tue Sep 29 05:17:50 2015
[runlim] main pid:		18765
[runlim] sample:		9.5 time, 10.5 real, 671.8 MB
[runlim] sample:		19.4 time, 20.5 real, 1039.9 MB
[runlim] sample:		29.4 time, 30.5 real, 1255.2 MB
[runlim] sample:		39.4 time, 40.5 real, 1409.7 MB
[runlim] sample:		49.4 time, 50.5 real, 1574.6 MB
[runlim] sample:		59.4 time, 60.5 real, 2016.9 MB
[runlim] sample:		69.4 time, 70.5 real, 2403.4 MB
[runlim] sample:		79.4 time, 80.5 real, 2544.5 MB
[runlim] sample:		89.3 time, 90.5 real, 2823.5 MB
[runlim] sample:		99.3 time, 100.5 real, 3178.5 MB
[runlim] sample:		109.3 time, 110.5 real, 3448.0 MB
[runlim] sample:		119.3 time, 120.5 real, 3793.2 MB
[runlim] sample:		129.3 time, 130.5 real, 4034.7 MB
[runlim] sample:		139.3 time, 140.5 real, 4309.0 MB
[runlim] sample:		149.3 time, 150.5 real, 4560.4 MB
[runlim] sample:		159.3 time, 160.5 real, 4599.8 MB
[runlim] sample:		169.2 time, 170.5 real, 4618.9 MB
[runlim] sample:		179.2 time, 180.5 real, 4795.7 MB
[runlim] sample:		189.2 time, 190.5 real, 4908.7 MB
[runlim] sample:		199.2 time, 200.5 real, 5241.5 MB
[runlim] sample:		209.2 time, 210.5 real, 5478.3 MB
[runlim] sample:		219.2 time, 220.5 real, 5604.8 MB
[runlim] sample:		229.2 time, 230.5 real, 5848.8 MB
[runlim] sample:		239.2 time, 240.5 real, 6047.9 MB
[runlim] sample:		249.2 time, 250.5 real, 6262.0 MB
[runlim] sample:		259.1 time, 260.5 real, 6411.2 MB
[runlim] sample:		269.1 time, 270.5 real, 6479.3 MB
[runlim] sample:		6.1 time, 280.5 real, 457.6 MB
[runlim] sample:		16.1 time, 290.5 real, 957.7 MB
[runlim] sample:		26.1 time, 300.5 real, 1192.5 MB
[runlim] sample:		36.0 time, 310.5 real, 1387.6 MB
[runlim] sample:		46.0 time, 320.5 real, 1466.3 MB
[runlim] sample:		56.0 time, 330.5 real, 1900.4 MB
[runlim] sample:		66.0 time, 340.5 real, 2210.4 MB
[runlim] sample:		76.0 time, 350.5 real, 2333.5 MB
[runlim] sample:		86.0 time, 360.5 real, 2467.2 MB
[runlim] sample:		96.0 time, 370.5 real, 2790.7 MB
[runlim] sample:		106.0 time, 380.5 real, 3113.5 MB
[runlim] sample:		116.0 time, 390.5 real, 3266.1 MB
[runlim] sample:		125.9 time, 400.5 real, 3543.2 MB
[runlim] sample:		135.9 time, 410.5 real, 3825.4 MB
[runlim] sample:		145.9 time, 420.5 real, 4023.7 MB
[runlim] sample:		155.9 time, 430.5 real, 4297.1 MB
[runlim] sample:		165.9 time, 440.5 real, 4400.6 MB
[runlim] sample:		175.9 time, 450.5 real, 4491.1 MB
[runlim] sample:		185.9 time, 460.5 real, 4571.0 MB
[runlim] sample:		195.9 time, 470.5 real, 4664.6 MB
[runlim] sample:		205.8 time, 480.5 real, 4766.4 MB
[runlim] sample:		215.8 time, 490.5 real, 4948.7 MB
[runlim] sample:		225.8 time, 500.5 real, 5258.2 MB
[runlim] sample:		235.8 time, 510.5 real, 5398.3 MB
[runlim] sample:		245.8 time, 520.5 real, 5582.9 MB
[runlim] sample:		255.8 time, 530.5 real, 5778.8 MB
[runlim] sample:		265.8 time, 540.5 real, 5950.9 MB
[runlim] sample:		275.8 time, 550.5 real, 6222.3 MB
[runlim] sample:		285.8 time, 560.5 real, 6375.0 MB
[runlim] sample:		295.7 time, 570.5 real, 6541.1 MB
[runlim] sample:		3.3 time, 580.5 real, 256.6 MB
[runlim] sample:		13.3 time, 590.5 real, 878.9 MB
[runlim] sample:		23.3 time, 600.5 real, 1176.8 MB
[runlim] sample:		33.3 time, 610.5 real, 1366.9 MB
[runlim] sample:		43.3 time, 620.5 real, 1471.7 MB
[runlim] sample:		53.2 time, 630.5 real, 1777.5 MB
[runlim] sample:		63.2 time, 640.5 real, 2277.9 MB
[runlim] sample:		73.2 time, 650.5 real, 2832.0 MB
[runlim] sample:		83.2 time, 660.5 real, 3162.0 MB
[runlim] sample:		93.2 time, 670.5 real, 3481.9 MB
[runlim] sample:		103.2 time, 680.5 real, 3730.9 MB
[runlim] sample:		113.2 time, 690.5 real, 3730.9 MB
[runlim] sample:		123.2 time, 700.5 real, 3730.9 MB
[runlim] sample:		133.2 time, 710.5 real, 3888.1 MB
[runlim] sample:		143.1 time, 720.5 real, 4188.1 MB
[runlim] sample:		153.1 time, 730.5 real, 4545.9 MB
[runlim] sample:		163.1 time, 740.5 real, 4875.9 MB
[runlim] sample:		173.1 time, 750.5 real, 5237.8 MB
[runlim] sample:		183.1 time, 760.5 real, 5346.9 MB
[runlim] sample:		193.1 time, 770.5 real, 5346.9 MB
[runlim] sample:		203.1 time, 780.5 real, 5346.9 MB
[runlim] sample:		213.1 time, 790.5 real, 5437.9 MB
[runlim] sample:		223.1 time, 800.5 real, 5737.9 MB
[runlim] sample:		233.0 time, 810.5 real, 6051.0 MB
[runlim] sample:		243.0 time, 820.5 real, 6370.5 MB
[runlim] sample:		253.0 time, 830.5 real, 6675.5 MB
[runlim] sample:		8.9 time, 840.5 real, 638.9 MB
[runlim] sample:		18.9 time, 850.5 real, 1090.0 MB
[runlim] sample:		28.9 time, 860.5 real, 1368.6 MB
[runlim] sample:		38.8 time, 870.5 real, 1768.1 MB
[runlim] sample:		48.8 time, 880.5 real, 2199.9 MB
[runlim] sample:		58.8 time, 890.5 real, 2533.3 MB
[runlim] sample:		68.8 time, 900.5 real, 2791.4 MB
[runlim] sample:		78.8 time, 910.5 real, 3030.2 MB
[runlim] sample:		88.8 time, 920.5 real, 3380.5 MB
[runlim] sample:		98.8 time, 930.5 real, 3635.5 MB
[runlim] sample:		108.7 time, 940.5 real, 4085.8 MB
[runlim] sample:		118.7 time, 950.5 real, 4338.6 MB
[runlim] sample:		128.7 time, 960.5 real, 4596.6 MB
[runlim] sample:		138.7 time, 970.5 real, 4971.2 MB
[runlim] sample:		148.7 time, 980.5 real, 5098.0 MB
[runlim] sample:		158.7 time, 990.5 real, 5546.9 MB
[runlim] sample:		168.7 time, 1000.5 real, 5685.2 MB
[runlim] sample:		178.6 time, 1010.5 real, 5956.8 MB
[runlim] sample:		188.6 time, 1020.5 real, 5963.4 MB
[runlim] sample:		198.6 time, 1030.5 real, 6014.7 MB
[runlim] sample:		208.6 time, 1040.5 real, 6101.0 MB
[runlim] sample:		218.6 time, 1050.5 real, 6424.3 MB
[runlim] sample:		228.6 time, 1060.5 real, 6518.5 MB
[runlim] sample:		2.6 time, 1070.5 real, 231.7 MB
[runlim] sample:		12.6 time, 1080.5 real, 838.9 MB
[runlim] sample:		22.6 time, 1090.5 real, 1158.8 MB
[runlim] sample:		32.6 time, 1100.5 real, 1352.9 MB
[runlim] sample:		42.6 time, 1110.5 real, 1465.7 MB
[runlim] sample:		52.6 time, 1120.5 real, 1746.5 MB
[runlim] sample:		62.5 time, 1130.5 real, 2144.9 MB
[runlim] sample:		72.5 time, 1140.5 real, 2494.0 MB
[runlim] sample:		82.5 time, 1150.5 real, 3277.7 MB
[runlim] sample:		92.5 time, 1160.5 real, 4152.7 MB
[runlim] sample:		102.5 time, 1170.5 real, 4241.9 MB
[runlim] sample:		112.5 time, 1180.5 real, 4734.9 MB
[runlim] sample:		122.5 time, 1190.5 real, 5504.1 MB
[runlim] sample:		132.4 time, 1200.5 real, 5592.7 MB
[runlim] sample:		142.5 time, 1210.5 real, 5934.8 MB
[runlim] sample:		152.4 time, 1220.5 real, 6470.5 MB
[runlim] sample:		162.4 time, 1230.5 real, 6487.9 MB
[runlim] sample:		172.4 time, 1240.5 real, 6499.2 MB
[runlim] end:			Tue Sep 29 05:38:40 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		74934
[runlim] real:			1250.30 seconds
[runlim] time:			301.74 seconds
[runlim] space:			6691.0 MB
[runlim] samples:		12498
