[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.iproverdeephc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/beemfwt5b1.aig
[runlim] start:			Tue Sep 29 05:37:42 2015
[runlim] main pid:		24290
[runlim] sample:		9.6 time, 10.3 real, 685.0 MB
[runlim] sample:		19.6 time, 20.3 real, 1265.3 MB
[runlim] sample:		29.6 time, 30.3 real, 1447.1 MB
[runlim] sample:		39.6 time, 40.3 real, 1705.1 MB
[runlim] sample:		49.6 time, 50.3 real, 1905.1 MB
[runlim] sample:		59.5 time, 60.3 real, 1965.2 MB
[runlim] sample:		69.5 time, 70.3 real, 2085.1 MB
[runlim] sample:		79.5 time, 80.3 real, 2550.1 MB
[runlim] sample:		89.5 time, 90.3 real, 2828.5 MB
[runlim] sample:		99.5 time, 100.3 real, 3097.1 MB
[runlim] sample:		109.5 time, 110.3 real, 3454.5 MB
[runlim] sample:		119.5 time, 120.3 real, 3843.9 MB
[runlim] sample:		129.4 time, 130.3 real, 4201.6 MB
[runlim] sample:		139.4 time, 140.3 real, 4476.4 MB
[runlim] sample:		149.4 time, 150.3 real, 4844.3 MB
[runlim] sample:		159.4 time, 160.3 real, 5141.5 MB
[runlim] sample:		169.4 time, 170.3 real, 5188.3 MB
[runlim] sample:		179.3 time, 180.3 real, 5217.8 MB
[runlim] sample:		189.3 time, 190.3 real, 5325.4 MB
[runlim] sample:		199.3 time, 200.3 real, 5475.6 MB
[runlim] sample:		209.3 time, 210.3 real, 5667.8 MB
[runlim] sample:		219.3 time, 220.3 real, 5946.5 MB
[runlim] sample:		229.3 time, 230.3 real, 6115.2 MB
[runlim] sample:		239.2 time, 240.3 real, 6406.4 MB
Fatal error: out of memory.
[runlim] sample:		0.6 time, 250.3 real, 74.1 MB
[runlim] sample:		10.6 time, 260.3 real, 736.0 MB
[runlim] sample:		20.6 time, 270.3 real, 1278.9 MB
[runlim] sample:		30.5 time, 280.3 real, 1469.8 MB
[runlim] sample:		40.5 time, 290.3 real, 1723.8 MB
[runlim] sample:		50.5 time, 300.3 real, 1907.9 MB
[runlim] sample:		60.5 time, 310.3 real, 1977.9 MB
[runlim] sample:		70.5 time, 320.3 real, 2130.0 MB
[runlim] sample:		80.5 time, 330.3 real, 2591.2 MB
[runlim] sample:		90.4 time, 340.3 real, 2804.6 MB
[runlim] sample:		100.4 time, 350.3 real, 3026.1 MB
[runlim] sample:		110.4 time, 360.3 real, 3217.0 MB
[runlim] sample:		120.4 time, 370.3 real, 3503.2 MB
[runlim] sample:		130.4 time, 380.3 real, 3827.2 MB
[runlim] sample:		140.4 time, 390.3 real, 3981.9 MB
[runlim] sample:		150.3 time, 400.3 real, 4371.5 MB
[runlim] sample:		160.3 time, 410.3 real, 4582.4 MB
[runlim] sample:		170.3 time, 420.3 real, 4870.3 MB
[runlim] sample:		180.3 time, 430.3 real, 5080.3 MB
[runlim] sample:		190.3 time, 440.3 real, 5152.6 MB
[runlim] sample:		200.3 time, 450.3 real, 5192.2 MB
[runlim] sample:		210.2 time, 460.3 real, 5203.0 MB
[runlim] sample:		220.2 time, 470.3 real, 5271.4 MB
[runlim] sample:		230.2 time, 480.3 real, 5329.5 MB
[runlim] sample:		240.2 time, 490.3 real, 5710.6 MB
[runlim] sample:		250.2 time, 500.3 real, 5890.1 MB
[runlim] sample:		260.2 time, 510.3 real, 6205.9 MB
[runlim] sample:		270.1 time, 520.3 real, 6404.4 MB
[runlim] sample:		280.1 time, 530.3 real, 6606.6 MB
Fatal error: out of memory.
[runlim] sample:		9.1 time, 540.3 real, 661.3 MB
[runlim] sample:		19.1 time, 550.3 real, 1242.4 MB
[runlim] sample:		29.0 time, 560.3 real, 1440.6 MB
[runlim] sample:		39.0 time, 570.3 real, 1702.6 MB
[runlim] sample:		49.0 time, 580.3 real, 1921.5 MB
[runlim] sample:		59.0 time, 590.3 real, 1975.7 MB
[runlim] sample:		69.0 time, 600.3 real, 2095.6 MB
[runlim] sample:		79.0 time, 610.3 real, 2548.8 MB
[runlim] sample:		88.9 time, 620.3 real, 2811.9 MB
[runlim] sample:		98.9 time, 630.3 real, 3232.6 MB
[runlim] sample:		108.9 time, 640.3 real, 3600.9 MB
[runlim] sample:		118.9 time, 650.3 real, 4006.9 MB
[runlim] sample:		128.9 time, 660.3 real, 4243.2 MB
[runlim] sample:		138.8 time, 670.3 real, 4665.1 MB
[runlim] sample:		148.8 time, 680.3 real, 4955.5 MB
[runlim] sample:		158.8 time, 690.3 real, 4969.0 MB
[runlim] sample:		168.8 time, 700.3 real, 4998.1 MB
[runlim] sample:		178.8 time, 710.3 real, 5158.6 MB
[runlim] sample:		188.8 time, 720.3 real, 5172.3 MB
[runlim] sample:		198.8 time, 730.3 real, 5371.7 MB
[runlim] sample:		208.8 time, 740.3 real, 5625.3 MB
[runlim] sample:		218.7 time, 750.3 real, 5729.1 MB
[runlim] sample:		228.7 time, 760.3 real, 5858.5 MB
[runlim] sample:		238.7 time, 770.3 real, 6125.1 MB
[runlim] sample:		248.7 time, 780.3 real, 6383.5 MB
Fatal error: exception Out of memory
[runlim] end:			Tue Sep 29 05:50:48 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		39280
[runlim] real:			786.25 seconds
[runlim] time:			280.58 seconds
[runlim] space:			6632.7 MB
[runlim] samples:		7859
