[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/6s194.aig
[runlim] start:			Tue Sep 29 02:15:46 2015
[runlim] main pid:		20926
[runlim] sample:		9.5 time, 10.5 real, 315.0 MB
[runlim] sample:		19.5 time, 20.5 real, 620.7 MB
[runlim] sample:		29.5 time, 30.5 real, 885.9 MB
[runlim] sample:		39.5 time, 40.5 real, 1067.2 MB
[runlim] sample:		49.4 time, 50.5 real, 1335.1 MB
[runlim] sample:		59.4 time, 60.5 real, 1598.3 MB
[runlim] sample:		69.4 time, 70.5 real, 1842.1 MB
[runlim] sample:		79.4 time, 80.5 real, 2073.0 MB
[runlim] sample:		89.4 time, 90.5 real, 2283.9 MB
[runlim] sample:		99.3 time, 100.5 real, 2379.3 MB
[runlim] sample:		109.3 time, 110.5 real, 2593.9 MB
[runlim] sample:		119.3 time, 120.5 real, 2807.5 MB
[runlim] sample:		129.3 time, 130.5 real, 3049.9 MB
[runlim] sample:		139.3 time, 140.5 real, 3254.8 MB
[runlim] sample:		149.3 time, 150.5 real, 3451.8 MB
[runlim] sample:		159.2 time, 160.5 real, 3699.5 MB
[runlim] sample:		169.2 time, 170.5 real, 3895.1 MB
[runlim] sample:		179.2 time, 180.5 real, 4139.9 MB
[runlim] sample:		189.2 time, 190.5 real, 4332.5 MB
[runlim] sample:		199.2 time, 200.5 real, 4541.9 MB
[runlim] sample:		209.2 time, 210.5 real, 4660.8 MB
[runlim] sample:		219.1 time, 220.5 real, 4723.5 MB
[runlim] sample:		229.1 time, 230.5 real, 4723.5 MB
[runlim] sample:		239.1 time, 240.5 real, 4812.5 MB
[runlim] sample:		249.1 time, 250.5 real, 4951.8 MB
[runlim] sample:		259.1 time, 260.5 real, 5141.1 MB
[runlim] sample:		269.1 time, 270.5 real, 5278.0 MB
[runlim] sample:		279.0 time, 280.5 real, 5522.4 MB
[runlim] sample:		289.0 time, 290.5 real, 5719.5 MB
[runlim] sample:		299.0 time, 300.5 real, 5859.8 MB
[runlim] sample:		309.0 time, 310.5 real, 6058.2 MB
[runlim] sample:		319.0 time, 320.5 real, 6227.6 MB
[runlim] sample:		329.0 time, 330.5 real, 6393.7 MB
[runlim] sample:		338.9 time, 340.5 real, 6610.7 MB
Fatal error: out of memory.
[runlim] sample:		7.2 time, 350.5 real, 283.8 MB
[runlim] sample:		17.2 time, 360.5 real, 547.4 MB
[runlim] sample:		27.2 time, 370.5 real, 681.2 MB
[runlim] sample:		37.1 time, 380.5 real, 911.5 MB
[runlim] sample:		47.1 time, 390.5 real, 1088.5 MB
[runlim] sample:		57.1 time, 400.5 real, 1283.4 MB
[runlim] sample:		67.1 time, 410.5 real, 1497.1 MB
[runlim] sample:		77.1 time, 420.5 real, 1724.8 MB
[runlim] sample:		87.0 time, 430.5 real, 1935.2 MB
[runlim] sample:		97.0 time, 440.5 real, 2140.5 MB
[runlim] sample:		107.0 time, 450.5 real, 2231.7 MB
[runlim] sample:		117.0 time, 460.5 real, 2343.0 MB
[runlim] sample:		127.0 time, 470.5 real, 2521.9 MB
[runlim] sample:		137.0 time, 480.5 real, 2720.0 MB
[runlim] sample:		146.9 time, 490.5 real, 2926.4 MB
[runlim] sample:		156.9 time, 500.5 real, 3120.2 MB
[runlim] sample:		166.9 time, 510.5 real, 3315.6 MB
[runlim] sample:		176.9 time, 520.5 real, 3548.6 MB
[runlim] sample:		186.9 time, 530.5 real, 3728.6 MB
[runlim] sample:		196.9 time, 540.5 real, 3914.1 MB
[runlim] sample:		206.8 time, 550.5 real, 4128.5 MB
[runlim] sample:		216.8 time, 560.5 real, 4329.5 MB
[runlim] sample:		226.8 time, 570.5 real, 4538.6 MB
[runlim] sample:		236.8 time, 580.5 real, 4699.0 MB
[runlim] sample:		246.8 time, 590.5 real, 4829.8 MB
[runlim] sample:		256.8 time, 600.5 real, 4832.7 MB
[runlim] sample:		266.7 time, 610.5 real, 4897.6 MB
[runlim] sample:		276.7 time, 620.5 real, 5047.3 MB
[runlim] sample:		286.7 time, 630.5 real, 5245.9 MB
[runlim] sample:		296.7 time, 640.5 real, 5410.2 MB
[runlim] sample:		306.7 time, 650.5 real, 5593.4 MB
[runlim] sample:		316.7 time, 660.5 real, 5771.8 MB
[runlim] sample:		326.6 time, 670.5 real, 5959.5 MB
[runlim] sample:		336.6 time, 680.5 real, 6157.8 MB
[runlim] sample:		346.6 time, 690.5 real, 6348.6 MB
[runlim] sample:		356.6 time, 700.5 real, 6538.7 MB
Fatal error: out of memory.
[runlim] sample:		2.5 time, 710.5 real, 213.1 MB
[runlim] sample:		12.5 time, 720.5 real, 419.5 MB
[runlim] sample:		22.5 time, 730.5 real, 685.8 MB
[runlim] sample:		32.5 time, 740.5 real, 926.2 MB
[runlim] sample:		42.4 time, 750.5 real, 1126.4 MB
[runlim] sample:		52.4 time, 760.5 real, 1220.9 MB
[runlim] sample:		62.4 time, 770.5 real, 1406.5 MB
[runlim] sample:		72.4 time, 780.5 real, 1645.9 MB
[runlim] sample:		82.4 time, 790.5 real, 1824.3 MB
[runlim] sample:		92.3 time, 800.5 real, 2018.3 MB
[runlim] sample:		102.3 time, 810.5 real, 2178.7 MB
[runlim] sample:		112.3 time, 820.5 real, 2317.3 MB
[runlim] sample:		122.3 time, 830.5 real, 2385.9 MB
[runlim] sample:		132.3 time, 840.5 real, 2525.1 MB
[runlim] sample:		142.3 time, 850.5 real, 2655.7 MB
[runlim] sample:		152.3 time, 860.5 real, 2812.8 MB
[runlim] sample:		162.2 time, 870.5 real, 2951.5 MB
[runlim] sample:		172.2 time, 880.5 real, 3129.1 MB
[runlim] sample:		182.2 time, 890.5 real, 3299.1 MB
[runlim] sample:		192.2 time, 900.5 real, 3418.3 MB
[runlim] sample:		202.2 time, 910.5 real, 3608.7 MB
[runlim] sample:		212.2 time, 920.5 real, 3749.4 MB
[runlim] sample:		222.1 time, 930.5 real, 3897.8 MB
[runlim] sample:		232.1 time, 940.5 real, 3996.5 MB
[runlim] sample:		242.1 time, 950.5 real, 4198.0 MB
[runlim] sample:		252.1 time, 960.5 real, 4352.3 MB
[runlim] sample:		262.1 time, 970.5 real, 4537.8 MB
[runlim] sample:		272.1 time, 980.5 real, 4618.8 MB
[runlim] sample:		282.1 time, 990.5 real, 4685.3 MB
[runlim] sample:		292.0 time, 1000.5 real, 4685.8 MB
[runlim] sample:		302.0 time, 1010.5 real, 4691.0 MB
[runlim] sample:		312.0 time, 1020.5 real, 4760.0 MB
[runlim] sample:		322.0 time, 1030.5 real, 4828.6 MB
[runlim] sample:		332.0 time, 1040.5 real, 4998.6 MB
[runlim] sample:		342.0 time, 1050.5 real, 5136.9 MB
[runlim] sample:		351.9 time, 1060.5 real, 5297.4 MB
[runlim] sample:		361.9 time, 1070.5 real, 5410.1 MB
[runlim] sample:		371.9 time, 1080.5 real, 5502.3 MB
[runlim] sample:		381.9 time, 1090.5 real, 5699.9 MB
[runlim] sample:		391.9 time, 1100.5 real, 5828.1 MB
[runlim] sample:		401.9 time, 1110.5 real, 5997.5 MB
[runlim] sample:		411.8 time, 1120.5 real, 6109.9 MB
[runlim] sample:		421.8 time, 1130.5 real, 6190.3 MB
[runlim] sample:		431.8 time, 1140.5 real, 6407.5 MB
[runlim] sample:		441.8 time, 1150.5 real, 6582.5 MB
terminate called after throwing an instance of 'Minisat::OutOfMemoryException'
[runlim] end:			Tue Sep 29 02:35:00 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		57705
[runlim] real:			1155.01 seconds
[runlim] time:			446.10 seconds
[runlim] space:			6671.1 MB
[runlim] samples:		11544
