[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/iimc/single.iimc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/shift1add524288.aig
[runlim] start:			Fri Sep 18 15:44:10 2015
[runlim] main pid:		9664
[runlim] sample:		39.2 time, 10.4 real, 76.5 MB
[runlim] sample:		78.8 time, 20.4 real, 114.0 MB
[runlim] sample:		118.5 time, 30.4 real, 137.7 MB
[runlim] sample:		158.2 time, 40.4 real, 141.6 MB
[runlim] sample:		197.8 time, 50.4 real, 186.0 MB
[runlim] sample:		237.5 time, 60.4 real, 193.7 MB
[runlim] sample:		277.1 time, 70.4 real, 311.9 MB
[runlim] sample:		316.8 time, 80.4 real, 264.6 MB
[runlim] sample:		356.4 time, 90.4 real, 265.3 MB
[runlim] sample:		396.1 time, 100.4 real, 277.2 MB
[runlim] sample:		435.8 time, 110.4 real, 281.0 MB
[runlim] sample:		475.4 time, 120.4 real, 285.1 MB
[runlim] sample:		515.1 time, 130.4 real, 196.2 MB
[runlim] sample:		554.8 time, 140.4 real, 198.0 MB
[runlim] sample:		594.5 time, 150.4 real, 202.9 MB
[runlim] sample:		634.2 time, 160.4 real, 206.3 MB
[runlim] sample:		673.9 time, 170.4 real, 207.6 MB
[runlim] sample:		713.6 time, 180.4 real, 209.6 MB
[runlim] sample:		753.2 time, 190.4 real, 225.7 MB
[runlim] sample:		792.9 time, 200.4 real, 289.1 MB
[runlim] sample:		832.6 time, 210.4 real, 239.7 MB
[runlim] sample:		872.3 time, 220.4 real, 305.7 MB
[runlim] sample:		912.0 time, 230.4 real, 305.9 MB
[runlim] sample:		951.6 time, 240.4 real, 306.7 MB
[runlim] sample:		991.3 time, 250.4 real, 307.2 MB
[runlim] sample:		1031.0 time, 260.4 real, 310.0 MB
[runlim] sample:		1070.7 time, 270.4 real, 310.8 MB
[runlim] sample:		1110.4 time, 280.4 real, 312.6 MB
[runlim] sample:		1150.0 time, 290.4 real, 313.9 MB
[runlim] sample:		1189.7 time, 300.4 real, 317.7 MB
[runlim] sample:		1229.4 time, 310.4 real, 320.0 MB
[runlim] sample:		1269.1 time, 320.4 real, 321.8 MB
[runlim] sample:		1308.8 time, 330.4 real, 322.3 MB
[runlim] sample:		1348.4 time, 340.4 real, 322.8 MB
[runlim] sample:		1388.1 time, 350.4 real, 323.9 MB
[runlim] sample:		1427.8 time, 360.4 real, 324.8 MB
[runlim] sample:		1467.5 time, 370.4 real, 325.6 MB
[runlim] sample:		1507.1 time, 380.4 real, 341.7 MB
[runlim] sample:		1546.8 time, 390.4 real, 342.0 MB
[runlim] sample:		1586.5 time, 400.4 real, 344.5 MB
[runlim] sample:		1626.1 time, 410.4 real, 344.6 MB
[runlim] sample:		1665.8 time, 420.4 real, 344.5 MB
[runlim] sample:		1705.5 time, 430.4 real, 345.6 MB
[runlim] sample:		1745.1 time, 440.4 real, 345.8 MB
[runlim] sample:		1784.8 time, 450.4 real, 347.0 MB
[runlim] sample:		1824.4 time, 460.4 real, 347.5 MB
[runlim] sample:		1864.1 time, 470.4 real, 349.9 MB
[runlim] sample:		1903.8 time, 480.4 real, 351.5 MB
[runlim] sample:		1943.4 time, 490.4 real, 354.5 MB
[runlim] sample:		1983.1 time, 500.4 real, 354.6 MB
[runlim] sample:		2022.7 time, 510.4 real, 355.3 MB
[runlim] sample:		2062.4 time, 520.4 real, 355.7 MB
[runlim] sample:		2102.1 time, 530.4 real, 358.5 MB
[runlim] sample:		2141.7 time, 540.4 real, 358.8 MB
[runlim] sample:		2181.4 time, 550.4 real, 358.8 MB
[runlim] sample:		2221.0 time, 560.4 real, 360.8 MB
[runlim] sample:		2260.7 time, 570.4 real, 360.0 MB
[runlim] sample:		2300.3 time, 580.4 real, 364.7 MB
[runlim] sample:		2340.0 time, 590.4 real, 364.9 MB
[runlim] sample:		2379.7 time, 600.4 real, 365.0 MB
[runlim] sample:		2419.3 time, 610.4 real, 365.8 MB
[runlim] sample:		2458.9 time, 620.4 real, 364.9 MB
[runlim] sample:		2498.6 time, 630.4 real, 372.5 MB
[runlim] sample:		2538.2 time, 640.4 real, 376.0 MB
[runlim] sample:		2577.9 time, 650.4 real, 376.0 MB
[runlim] sample:		2617.5 time, 660.4 real, 376.5 MB
[runlim] sample:		2657.2 time, 670.4 real, 376.8 MB
[runlim] sample:		2696.8 time, 680.4 real, 377.0 MB
[runlim] sample:		2736.5 time, 690.4 real, 377.0 MB
[runlim] sample:		2776.2 time, 700.4 real, 377.3 MB
[runlim] sample:		2815.8 time, 710.4 real, 377.5 MB
[runlim] sample:		2855.4 time, 720.4 real, 377.8 MB
[runlim] sample:		2895.1 time, 730.4 real, 378.1 MB
[runlim] sample:		2934.7 time, 740.4 real, 601.6 MB
[runlim] sample:		2974.4 time, 750.4 real, 859.9 MB
[runlim] sample:		3014.0 time, 760.4 real, 860.6 MB
[runlim] sample:		3053.7 time, 770.4 real, 860.6 MB
[runlim] sample:		3093.4 time, 780.4 real, 893.1 MB
[runlim] sample:		3133.0 time, 790.4 real, 893.4 MB
[runlim] sample:		3172.7 time, 800.4 real, 894.8 MB
[runlim] sample:		3212.3 time, 810.4 real, 894.8 MB
[runlim] sample:		3252.0 time, 820.4 real, 894.8 MB
[runlim] sample:		3291.6 time, 830.4 real, 895.3 MB
[runlim] sample:		3331.3 time, 840.4 real, 895.6 MB
[runlim] sample:		3370.9 time, 850.4 real, 896.1 MB
[runlim] sample:		3410.6 time, 860.4 real, 896.3 MB
[runlim] sample:		3450.2 time, 870.4 real, 896.6 MB
[runlim] sample:		3489.9 time, 880.4 real, 898.6 MB
[runlim] sample:		3529.5 time, 890.4 real, 899.7 MB
[runlim] sample:		3569.1 time, 900.4 real, 899.9 MB
[runlim] sample:		3608.8 time, 910.4 real, 902.2 MB
[runlim] sample:		3648.4 time, 920.4 real, 904.5 MB
[runlim] sample:		3688.1 time, 930.4 real, 906.2 MB
[runlim] sample:		3727.7 time, 940.4 real, 910.4 MB
[runlim] sample:		3767.4 time, 950.4 real, 910.7 MB
[runlim] sample:		3807.0 time, 960.4 real, 911.0 MB
[runlim] sample:		3846.7 time, 970.4 real, 911.2 MB
[runlim] sample:		3886.3 time, 980.4 real, 911.5 MB
[runlim] sample:		3925.9 time, 990.4 real, 911.5 MB
[runlim] sample:		3965.5 time, 1000.4 real, 911.5 MB
[runlim] sample:		4005.1 time, 1010.4 real, 911.7 MB
[runlim] sample:		4044.7 time, 1020.4 real, 912.2 MB
[runlim] sample:		4084.4 time, 1030.4 real, 912.2 MB
[runlim] sample:		4124.0 time, 1040.4 real, 912.8 MB
[runlim] end:			Fri Sep 18 16:01:37 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			1047.30 seconds
[runlim] time:			4150.50 seconds
[runlim] space:			928.7 MB
[runlim] samples:		10469
