[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/6s344rb150.aig
[runlim] start:			Tue Sep 29 05:21:18 2015
[runlim] main pid:		4401
[runlim] sample:		9.3 time, 10.8 real, 618.4 MB
[runlim] sample:		19.3 time, 20.8 real, 963.4 MB
[runlim] sample:		29.3 time, 30.8 real, 1215.7 MB
[runlim] sample:		39.3 time, 40.8 real, 1349.8 MB
[runlim] sample:		49.2 time, 50.8 real, 1697.0 MB
[runlim] sample:		59.2 time, 60.8 real, 2024.1 MB
[runlim] sample:		69.2 time, 70.8 real, 2180.6 MB
[runlim] sample:		79.2 time, 80.8 real, 2521.5 MB
[runlim] sample:		89.2 time, 90.8 real, 2875.7 MB
[runlim] sample:		99.2 time, 100.8 real, 3173.8 MB
[runlim] sample:		109.2 time, 110.8 real, 3454.6 MB
[runlim] sample:		119.1 time, 120.8 real, 3621.0 MB
[runlim] sample:		129.1 time, 130.8 real, 3650.3 MB
[runlim] sample:		139.1 time, 140.8 real, 3767.9 MB
[runlim] sample:		149.1 time, 150.8 real, 3952.1 MB
[runlim] sample:		159.1 time, 160.8 real, 4256.0 MB
[runlim] sample:		169.0 time, 170.8 real, 4467.1 MB
[runlim] sample:		179.0 time, 180.8 real, 4789.9 MB
[runlim] sample:		189.0 time, 190.8 real, 4964.7 MB
[runlim] sample:		199.0 time, 200.8 real, 5249.4 MB
[runlim] sample:		209.0 time, 210.8 real, 5504.0 MB
[runlim] sample:		218.9 time, 220.8 real, 5758.0 MB
[runlim] sample:		228.9 time, 230.8 real, 6093.7 MB
[runlim] sample:		238.9 time, 240.8 real, 6310.7 MB
Fatal error: out of memory.
[runlim] sample:		0.8 time, 250.8 real, 74.7 MB
[runlim] sample:		10.8 time, 260.8 real, 676.0 MB
[runlim] sample:		20.8 time, 270.8 real, 992.2 MB
[runlim] sample:		30.8 time, 280.8 real, 1256.2 MB
[runlim] sample:		40.7 time, 290.8 real, 1364.2 MB
[runlim] sample:		50.7 time, 300.8 real, 1767.2 MB
[runlim] sample:		60.7 time, 310.8 real, 1966.6 MB
[runlim] sample:		70.7 time, 320.8 real, 2101.6 MB
[runlim] sample:		80.7 time, 330.8 real, 2321.6 MB
[runlim] sample:		90.7 time, 340.8 real, 2517.4 MB
[runlim] sample:		100.6 time, 350.8 real, 2793.9 MB
[runlim] sample:		110.6 time, 360.8 real, 2975.3 MB
[runlim] sample:		120.6 time, 370.8 real, 3248.0 MB
[runlim] sample:		130.6 time, 380.8 real, 3452.4 MB
[runlim] sample:		140.6 time, 390.8 real, 3614.6 MB
[runlim] sample:		150.6 time, 400.8 real, 3683.1 MB
[runlim] sample:		160.6 time, 410.8 real, 3688.6 MB
[runlim] sample:		170.5 time, 420.8 real, 3731.4 MB
[runlim] sample:		180.5 time, 430.8 real, 3839.3 MB
[runlim] sample:		190.5 time, 440.8 real, 3922.7 MB
[runlim] sample:		200.5 time, 450.8 real, 4117.7 MB
[runlim] sample:		210.5 time, 460.8 real, 4296.9 MB
[runlim] sample:		220.4 time, 470.8 real, 4483.2 MB
[runlim] sample:		230.4 time, 480.8 real, 4639.9 MB
[runlim] sample:		240.4 time, 490.8 real, 4870.9 MB
[runlim] sample:		250.4 time, 500.8 real, 5112.0 MB
[runlim] sample:		260.4 time, 510.8 real, 5293.8 MB
[runlim] sample:		270.4 time, 520.8 real, 5456.9 MB
[runlim] sample:		280.4 time, 530.8 real, 5663.8 MB
[runlim] sample:		290.3 time, 540.8 real, 5840.4 MB
[runlim] sample:		300.3 time, 550.8 real, 6017.6 MB
[runlim] sample:		310.3 time, 560.8 real, 6183.7 MB
[runlim] sample:		320.3 time, 570.8 real, 6392.7 MB
[runlim] sample:		330.3 time, 580.8 real, 6623.3 MB
Fatal error: exception Out of memory
[runlim] sample:		2.5 time, 590.8 real, 184.1 MB
[runlim] sample:		12.5 time, 600.8 real, 797.6 MB
[runlim] sample:		22.4 time, 610.8 real, 1071.6 MB
[runlim] sample:		32.4 time, 620.8 real, 1331.6 MB
[runlim] sample:		42.4 time, 630.8 real, 1439.7 MB
[runlim] sample:		52.4 time, 640.8 real, 1816.7 MB
[runlim] sample:		62.4 time, 650.8 real, 2071.5 MB
[runlim] sample:		72.4 time, 660.8 real, 2203.5 MB
[runlim] sample:		82.3 time, 670.8 real, 2343.0 MB
[runlim] sample:		92.3 time, 680.8 real, 2597.6 MB
[runlim] sample:		102.3 time, 690.8 real, 2787.9 MB
[runlim] sample:		112.3 time, 700.8 real, 3005.6 MB
[runlim] sample:		122.3 time, 710.8 real, 3311.9 MB
[runlim] sample:		132.2 time, 720.8 real, 3398.8 MB
[runlim] sample:		142.2 time, 730.8 real, 3559.1 MB
[runlim] sample:		152.2 time, 740.8 real, 3808.0 MB
[runlim] sample:		162.2 time, 750.8 real, 3819.6 MB
[runlim] sample:		172.2 time, 760.8 real, 3824.7 MB
[runlim] sample:		182.2 time, 770.8 real, 3831.0 MB
[runlim] sample:		192.2 time, 780.8 real, 3862.1 MB
[runlim] sample:		202.1 time, 790.8 real, 3934.3 MB
[runlim] sample:		212.1 time, 800.8 real, 3992.8 MB
[runlim] sample:		222.1 time, 810.8 real, 4017.5 MB
[runlim] sample:		232.1 time, 820.8 real, 4065.1 MB
[runlim] sample:		242.1 time, 830.8 real, 4153.2 MB
[runlim] sample:		252.1 time, 840.8 real, 4430.7 MB
[runlim] sample:		262.0 time, 850.8 real, 4737.5 MB
[runlim] sample:		272.0 time, 860.8 real, 4947.0 MB
[runlim] sample:		282.0 time, 870.8 real, 5019.7 MB
[runlim] sample:		292.0 time, 880.8 real, 5070.4 MB
[runlim] sample:		302.0 time, 890.8 real, 5100.7 MB
[runlim] sample:		312.0 time, 900.8 real, 5173.2 MB
[runlim] sample:		321.9 time, 910.8 real, 5233.6 MB
[runlim] sample:		331.9 time, 920.8 real, 5437.7 MB
[runlim] sample:		341.9 time, 930.8 real, 5682.5 MB
[runlim] sample:		351.9 time, 940.8 real, 5914.9 MB
[runlim] sample:		361.9 time, 950.8 real, 6078.3 MB
[runlim] sample:		371.9 time, 960.8 real, 6134.7 MB
[runlim] sample:		381.9 time, 970.8 real, 6181.0 MB
[runlim] sample:		391.8 time, 980.8 real, 6213.4 MB
[runlim] sample:		401.8 time, 990.8 real, 6275.9 MB
[runlim] sample:		411.8 time, 1000.8 real, 6332.3 MB
[runlim] sample:		421.8 time, 1010.8 real, 6404.9 MB
Fatal error: out of memory.
[runlim] end:			Tue Sep 29 05:38:16 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		50868
[runlim] real:			1018.72 seconds
[runlim] time:			429.56 seconds
[runlim] space:			6665.0 MB
[runlim] samples:		10179
