[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/nusmvguidancep8.aig
[runlim] start:			Mon Sep 28 21:02:46 2015
[runlim] main pid:		20803
[runlim] sample:		9.5 time, 10.5 real, 242.2 MB
[runlim] sample:		19.5 time, 20.5 real, 431.5 MB
[runlim] sample:		29.5 time, 30.5 real, 616.9 MB
[runlim] sample:		39.5 time, 40.5 real, 722.5 MB
[runlim] sample:		49.5 time, 50.5 real, 862.0 MB
[runlim] sample:		59.5 time, 60.5 real, 1025.2 MB
[runlim] sample:		69.5 time, 70.5 real, 1176.3 MB
[runlim] sample:		79.4 time, 80.5 real, 1279.4 MB
[runlim] sample:		89.4 time, 90.5 real, 1423.6 MB
[runlim] sample:		99.4 time, 100.5 real, 1537.7 MB
[runlim] sample:		109.4 time, 110.5 real, 1641.2 MB
[runlim] sample:		119.4 time, 120.5 real, 1757.7 MB
[runlim] sample:		129.4 time, 130.5 real, 1891.4 MB
[runlim] sample:		139.3 time, 140.5 real, 2030.8 MB
[runlim] sample:		149.3 time, 150.5 real, 2161.4 MB
[runlim] sample:		159.3 time, 160.5 real, 2308.8 MB
[runlim] sample:		169.3 time, 170.5 real, 2427.2 MB
[runlim] sample:		179.3 time, 180.5 real, 2571.3 MB
[runlim] sample:		189.3 time, 190.5 real, 2690.1 MB
[runlim] sample:		199.3 time, 200.5 real, 2819.2 MB
[runlim] sample:		209.2 time, 210.5 real, 2958.9 MB
[runlim] sample:		219.2 time, 220.5 real, 3077.3 MB
[runlim] sample:		229.2 time, 230.5 real, 3153.5 MB
[runlim] sample:		239.2 time, 240.5 real, 3169.5 MB
[runlim] sample:		249.2 time, 250.5 real, 3236.0 MB
[runlim] sample:		259.2 time, 260.5 real, 3340.6 MB
[runlim] sample:		269.2 time, 270.5 real, 3474.3 MB
[runlim] sample:		279.1 time, 280.5 real, 3576.5 MB
[runlim] sample:		289.1 time, 290.5 real, 3694.8 MB
[runlim] sample:		299.1 time, 300.5 real, 3821.5 MB
[runlim] sample:		309.1 time, 310.5 real, 3957.7 MB
[runlim] sample:		319.1 time, 320.5 real, 4071.3 MB
[runlim] sample:		329.1 time, 330.5 real, 4184.2 MB
[runlim] sample:		339.1 time, 340.5 real, 4287.9 MB
[runlim] sample:		349.0 time, 350.5 real, 4440.2 MB
[runlim] sample:		359.0 time, 360.5 real, 4517.9 MB
[runlim] sample:		369.0 time, 370.5 real, 4549.2 MB
[runlim] sample:		379.0 time, 380.5 real, 4679.9 MB
[runlim] sample:		389.0 time, 390.5 real, 4794.5 MB
[runlim] sample:		399.0 time, 400.5 real, 4905.1 MB
[runlim] sample:		409.0 time, 410.5 real, 5030.2 MB
[runlim] sample:		418.9 time, 420.5 real, 5146.4 MB
[runlim] sample:		428.9 time, 430.5 real, 5256.6 MB
[runlim] sample:		438.9 time, 440.5 real, 5374.4 MB
[runlim] sample:		448.9 time, 450.5 real, 5498.3 MB
[runlim] sample:		458.9 time, 460.5 real, 5612.4 MB
[runlim] sample:		468.9 time, 470.5 real, 5734.5 MB
[runlim] sample:		478.8 time, 480.5 real, 5846.7 MB
[runlim] sample:		488.8 time, 490.5 real, 5962.8 MB
[runlim] sample:		498.8 time, 500.5 real, 6065.0 MB
[runlim] sample:		508.8 time, 510.5 real, 6207.2 MB
[runlim] sample:		518.8 time, 520.5 real, 6307.3 MB
[runlim] sample:		528.8 time, 530.5 real, 6403.5 MB
[runlim] sample:		538.8 time, 540.5 real, 6504.0 MB
[runlim] sample:		548.7 time, 550.5 real, 6606.1 MB
Fatal error: out of memory.
[runlim] sample:		4.5 time, 560.5 real, 110.1 MB
[runlim] sample:		14.5 time, 570.5 real, 356.4 MB
[runlim] sample:		24.5 time, 580.5 real, 581.9 MB
[runlim] sample:		34.5 time, 590.5 real, 754.9 MB
[runlim] sample:		44.5 time, 600.5 real, 953.1 MB
[runlim] sample:		54.5 time, 610.5 real, 1117.9 MB
[runlim] sample:		64.5 time, 620.5 real, 1252.5 MB
[runlim] sample:		74.4 time, 630.5 real, 1431.1 MB
[runlim] sample:		84.4 time, 640.5 real, 1621.0 MB
[runlim] sample:		94.4 time, 650.5 real, 1808.2 MB
[runlim] sample:		104.4 time, 660.5 real, 2007.0 MB
[runlim] sample:		114.4 time, 670.5 real, 2213.6 MB
[runlim] sample:		124.4 time, 680.5 real, 2297.2 MB
[runlim] sample:		134.3 time, 690.5 real, 2424.8 MB
[runlim] sample:		144.3 time, 700.5 real, 2540.0 MB
[runlim] sample:		154.3 time, 710.5 real, 2700.4 MB
[runlim] sample:		164.3 time, 720.5 real, 2887.4 MB
[runlim] sample:		174.3 time, 730.5 real, 3078.0 MB
[runlim] sample:		184.3 time, 740.5 real, 3261.4 MB
[runlim] sample:		194.2 time, 750.5 real, 3438.5 MB
[runlim] sample:		204.2 time, 760.5 real, 3622.8 MB
[runlim] sample:		214.2 time, 770.5 real, 3801.3 MB
[runlim] sample:		224.2 time, 780.5 real, 3987.6 MB
[runlim] sample:		234.2 time, 790.5 real, 4151.0 MB
[runlim] sample:		244.2 time, 800.5 real, 4333.0 MB
[runlim] sample:		254.2 time, 810.5 real, 4514.0 MB
[runlim] sample:		264.2 time, 820.5 real, 4581.9 MB
[runlim] sample:		274.1 time, 830.5 real, 4591.4 MB
[runlim] sample:		284.1 time, 840.5 real, 4719.0 MB
[runlim] sample:		294.1 time, 850.5 real, 4783.2 MB
[runlim] sample:		304.1 time, 860.5 real, 4902.1 MB
[runlim] sample:		314.1 time, 870.5 real, 5036.4 MB
[runlim] sample:		324.1 time, 880.5 real, 5156.5 MB
[runlim] sample:		334.0 time, 890.5 real, 5332.6 MB
[runlim] sample:		344.0 time, 900.5 real, 5488.7 MB
[runlim] sample:		354.0 time, 910.5 real, 5641.6 MB
[runlim] sample:		364.0 time, 920.5 real, 5819.9 MB
[runlim] sample:		374.0 time, 930.5 real, 5978.8 MB
[runlim] sample:		384.0 time, 940.5 real, 6153.1 MB
[runlim] sample:		393.9 time, 950.5 real, 6321.0 MB
[runlim] sample:		403.9 time, 960.5 real, 6477.2 MB
[runlim] sample:		413.9 time, 970.5 real, 6639.6 MB
Fatal error: out of memory.
[runlim] sample:		3.8 time, 980.5 real, 98.4 MB
[runlim] sample:		13.8 time, 990.5 real, 387.8 MB
[runlim] sample:		23.8 time, 1000.5 real, 551.5 MB
[runlim] sample:		33.8 time, 1010.5 real, 663.8 MB
[runlim] sample:		43.8 time, 1020.5 real, 724.4 MB
[runlim] sample:		53.8 time, 1030.5 real, 828.4 MB
[runlim] sample:		63.8 time, 1040.5 real, 902.6 MB
[runlim] sample:		73.8 time, 1050.5 real, 1093.3 MB
[runlim] sample:		83.7 time, 1060.5 real, 1203.8 MB
[runlim] sample:		93.7 time, 1070.5 real, 1270.2 MB
[runlim] sample:		103.7 time, 1080.5 real, 1450.8 MB
[runlim] sample:		113.7 time, 1090.5 real, 1506.6 MB
[runlim] sample:		123.7 time, 1100.5 real, 1516.8 MB
[runlim] sample:		133.7 time, 1110.5 real, 1631.8 MB
[runlim] sample:		143.7 time, 1120.5 real, 1809.2 MB
[runlim] sample:		153.6 time, 1130.5 real, 1863.9 MB
[runlim] sample:		163.6 time, 1140.5 real, 1869.4 MB
[runlim] sample:		173.6 time, 1150.5 real, 1870.8 MB
[runlim] sample:		183.6 time, 1160.5 real, 2013.0 MB
[runlim] sample:		193.6 time, 1170.5 real, 2153.9 MB
[runlim] sample:		203.6 time, 1180.5 real, 2160.2 MB
[runlim] sample:		213.6 time, 1190.5 real, 2172.7 MB
[runlim] sample:		223.5 time, 1200.5 real, 2177.0 MB
[runlim] sample:		233.5 time, 1210.5 real, 2249.7 MB
[runlim] sample:		243.5 time, 1220.5 real, 2388.1 MB
[runlim] sample:		253.5 time, 1230.5 real, 2572.8 MB
[runlim] sample:		263.5 time, 1240.5 real, 2718.4 MB
[runlim] sample:		273.5 time, 1250.5 real, 2793.9 MB
[runlim] sample:		283.4 time, 1260.5 real, 2810.1 MB
[runlim] sample:		293.4 time, 1270.5 real, 2830.3 MB
[runlim] sample:		303.4 time, 1280.5 real, 2830.3 MB
[runlim] sample:		313.4 time, 1290.5 real, 2868.9 MB
[runlim] sample:		323.4 time, 1300.5 real, 2916.8 MB
[runlim] sample:		333.4 time, 1310.5 real, 3029.2 MB
[runlim] sample:		343.4 time, 1320.5 real, 3223.1 MB
[runlim] sample:		353.3 time, 1330.5 real, 3343.7 MB
[runlim] sample:		363.3 time, 1340.5 real, 3365.5 MB
[runlim] sample:		373.3 time, 1350.5 real, 3368.2 MB
[runlim] sample:		383.3 time, 1360.5 real, 3380.9 MB
[runlim] sample:		393.3 time, 1370.5 real, 3391.7 MB
[runlim] sample:		403.3 time, 1380.5 real, 3392.2 MB
[runlim] sample:		413.3 time, 1390.5 real, 3413.7 MB
[runlim] sample:		423.3 time, 1400.5 real, 3546.1 MB
[runlim] sample:		433.2 time, 1410.5 real, 3696.7 MB
[runlim] sample:		443.2 time, 1420.5 real, 3829.5 MB
[runlim] sample:		453.2 time, 1430.5 real, 3961.3 MB
[runlim] sample:		463.2 time, 1440.5 real, 4081.7 MB
[runlim] sample:		473.2 time, 1450.5 real, 4084.0 MB
[runlim] sample:		483.2 time, 1460.5 real, 4086.2 MB
[runlim] sample:		493.2 time, 1470.5 real, 4092.5 MB
[runlim] sample:		503.1 time, 1480.5 real, 4095.0 MB
[runlim] sample:		513.1 time, 1490.5 real, 4115.4 MB
[runlim] sample:		523.1 time, 1500.5 real, 4115.4 MB
[runlim] sample:		533.1 time, 1510.5 real, 4115.4 MB
[runlim] sample:		543.1 time, 1520.5 real, 4189.5 MB
[runlim] sample:		553.1 time, 1530.5 real, 4271.5 MB
[runlim] sample:		563.1 time, 1540.5 real, 4425.2 MB
[runlim] sample:		573.0 time, 1550.5 real, 4575.3 MB
[runlim] sample:		583.0 time, 1560.5 real, 4689.2 MB
[runlim] sample:		593.0 time, 1570.5 real, 4841.8 MB
[runlim] sample:		603.0 time, 1580.5 real, 5017.8 MB
[runlim] sample:		613.0 time, 1590.5 real, 5096.4 MB
[runlim] sample:		623.0 time, 1600.5 real, 5102.6 MB
[runlim] sample:		633.0 time, 1610.5 real, 5105.1 MB
[runlim] sample:		642.9 time, 1620.5 real, 5109.6 MB
[runlim] sample:		652.9 time, 1630.5 real, 5111.9 MB
[runlim] sample:		662.9 time, 1640.5 real, 5111.9 MB
[runlim] sample:		672.9 time, 1650.5 real, 5111.9 MB
[runlim] sample:		682.9 time, 1660.5 real, 5114.1 MB
[runlim] sample:		692.9 time, 1670.5 real, 5118.7 MB
[runlim] sample:		702.8 time, 1680.5 real, 5193.2 MB
[runlim] sample:		712.8 time, 1690.5 real, 5321.8 MB
[runlim] sample:		722.8 time, 1700.5 real, 5413.3 MB
[runlim] sample:		732.8 time, 1710.5 real, 5515.9 MB
[runlim] sample:		742.8 time, 1720.5 real, 5625.6 MB
[runlim] sample:		752.8 time, 1730.5 real, 5733.8 MB
[runlim] sample:		762.8 time, 1740.5 real, 5962.1 MB
[runlim] sample:		772.8 time, 1750.5 real, 6223.0 MB
[runlim] sample:		782.7 time, 1760.5 real, 6229.7 MB
[runlim] sample:		792.7 time, 1770.5 real, 6229.7 MB
[runlim] sample:		802.7 time, 1780.5 real, 6235.9 MB
[runlim] sample:		812.7 time, 1790.5 real, 6248.2 MB
[runlim] sample:		822.7 time, 1800.5 real, 6250.2 MB
[runlim] sample:		832.6 time, 1810.5 real, 6254.4 MB
[runlim] sample:		842.6 time, 1820.5 real, 6260.7 MB
[runlim] sample:		852.6 time, 1830.5 real, 6273.9 MB
[runlim] sample:		862.6 time, 1840.5 real, 6282.0 MB
[runlim] sample:		872.6 time, 1850.5 real, 6294.0 MB
[runlim] sample:		882.6 time, 1860.5 real, 6337.5 MB
[runlim] sample:		892.6 time, 1870.5 real, 6502.5 MB
Fatal error: exception Out of memory
[runlim] end:			Mon Sep 28 21:34:00 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		93681
[runlim] real:			1874.59 seconds
[runlim] time:			896.35 seconds
[runlim] space:			6725.2 MB
[runlim] samples:		18740
