[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/bjrb07amba10andenv.aig
[runlim] start:			Tue Sep 29 05:27:18 2015
[runlim] main pid:		22013
[runlim] sample:		9.6 time, 10.6 real, 656.2 MB
[runlim] sample:		19.6 time, 20.6 real, 1163.5 MB
[runlim] sample:		29.5 time, 30.6 real, 1377.6 MB
[runlim] sample:		39.5 time, 40.6 real, 1650.8 MB
[runlim] sample:		49.5 time, 50.6 real, 1919.0 MB
[runlim] sample:		59.5 time, 60.6 real, 2083.0 MB
[runlim] sample:		69.5 time, 70.6 real, 2389.5 MB
[runlim] sample:		79.5 time, 80.6 real, 2569.3 MB
[runlim] sample:		89.4 time, 90.6 real, 2962.8 MB
[runlim] sample:		99.4 time, 100.6 real, 3310.2 MB
[runlim] sample:		109.4 time, 110.6 real, 3643.4 MB
[runlim] sample:		119.4 time, 120.6 real, 3970.6 MB
[runlim] sample:		129.4 time, 130.6 real, 4308.7 MB
[runlim] sample:		139.4 time, 140.6 real, 4335.1 MB
[runlim] sample:		149.3 time, 150.6 real, 4344.0 MB
[runlim] sample:		159.3 time, 160.6 real, 4370.3 MB
[runlim] sample:		169.3 time, 170.6 real, 4388.7 MB
[runlim] sample:		179.3 time, 180.6 real, 4461.3 MB
[runlim] sample:		189.3 time, 190.6 real, 4513.3 MB
[runlim] sample:		199.3 time, 200.6 real, 4513.3 MB
[runlim] sample:		209.2 time, 210.6 real, 4561.2 MB
[runlim] sample:		219.2 time, 220.6 real, 4619.4 MB
[runlim] sample:		229.2 time, 230.6 real, 4619.4 MB
[runlim] sample:		239.2 time, 240.6 real, 4619.6 MB
[runlim] sample:		249.2 time, 250.6 real, 4649.3 MB
[runlim] sample:		259.2 time, 260.6 real, 4725.3 MB
[runlim] sample:		269.2 time, 270.6 real, 4725.4 MB
[runlim] sample:		279.1 time, 280.6 real, 4725.7 MB
[runlim] sample:		289.1 time, 290.6 real, 4725.7 MB
[runlim] sample:		299.1 time, 300.6 real, 4897.9 MB
[runlim] sample:		309.1 time, 310.6 real, 4960.0 MB
[runlim] sample:		319.1 time, 320.6 real, 4960.0 MB
[runlim] sample:		329.1 time, 330.6 real, 4960.0 MB
[runlim] sample:		339.1 time, 340.6 real, 4960.1 MB
[runlim] sample:		349.1 time, 350.6 real, 4960.6 MB
[runlim] sample:		359.0 time, 360.6 real, 4962.6 MB
[runlim] sample:		369.0 time, 370.6 real, 4962.6 MB
[runlim] sample:		379.0 time, 380.6 real, 5221.5 MB
[runlim] sample:		389.0 time, 390.6 real, 5286.6 MB
[runlim] sample:		399.0 time, 400.6 real, 5336.6 MB
[runlim] sample:		408.9 time, 410.6 real, 5345.1 MB
[runlim] sample:		418.9 time, 420.6 real, 5345.4 MB
[runlim] sample:		428.9 time, 430.6 real, 5345.6 MB
[runlim] sample:		438.9 time, 440.6 real, 5345.6 MB
[runlim] sample:		448.9 time, 450.6 real, 5348.4 MB
[runlim] sample:		458.9 time, 460.6 real, 5348.4 MB
[runlim] sample:		468.9 time, 470.6 real, 5348.4 MB
[runlim] sample:		478.8 time, 480.6 real, 5348.4 MB
[runlim] sample:		488.8 time, 490.6 real, 5557.2 MB
[runlim] sample:		498.8 time, 500.6 real, 5615.2 MB
[runlim] sample:		508.8 time, 510.6 real, 5615.2 MB
[runlim] sample:		518.8 time, 520.6 real, 5615.2 MB
[runlim] sample:		528.8 time, 530.6 real, 5615.2 MB
[runlim] sample:		538.8 time, 540.6 real, 5615.2 MB
[runlim] sample:		548.8 time, 550.6 real, 5617.2 MB
[runlim] sample:		558.7 time, 560.6 real, 5617.2 MB
[runlim] sample:		568.7 time, 570.6 real, 5617.2 MB
[runlim] sample:		578.7 time, 580.6 real, 5617.2 MB
[runlim] sample:		588.7 time, 590.6 real, 5617.4 MB
[runlim] sample:		598.7 time, 600.6 real, 5619.4 MB
[runlim] sample:		608.6 time, 610.6 real, 5619.4 MB
[runlim] sample:		618.6 time, 620.6 real, 5829.9 MB
[runlim] sample:		628.6 time, 630.6 real, 5874.2 MB
[runlim] sample:		638.6 time, 640.6 real, 5892.4 MB
[runlim] sample:		648.6 time, 650.6 real, 5892.4 MB
[runlim] sample:		658.6 time, 660.6 real, 5892.6 MB
[runlim] sample:		668.6 time, 670.6 real, 5892.6 MB
[runlim] sample:		678.5 time, 680.6 real, 5892.6 MB
[runlim] sample:		688.5 time, 690.6 real, 5892.9 MB
[runlim] sample:		698.5 time, 700.6 real, 5894.9 MB
[runlim] sample:		708.5 time, 710.6 real, 5895.2 MB
[runlim] sample:		718.5 time, 720.6 real, 5895.2 MB
[runlim] sample:		728.5 time, 730.6 real, 5895.4 MB
[runlim] sample:		738.5 time, 740.6 real, 5895.4 MB
[runlim] sample:		748.4 time, 750.6 real, 5897.4 MB
[runlim] sample:		758.4 time, 760.6 real, 5897.7 MB
[runlim] sample:		768.4 time, 770.6 real, 5897.9 MB
[runlim] sample:		778.4 time, 780.6 real, 5897.9 MB
[runlim] sample:		788.4 time, 790.6 real, 5898.2 MB
[runlim] sample:		798.4 time, 800.6 real, 5900.2 MB
[runlim] sample:		808.4 time, 810.6 real, 5900.4 MB
[runlim] sample:		818.3 time, 820.6 real, 6099.0 MB
[runlim] sample:		828.3 time, 830.6 real, 6148.9 MB
[runlim] sample:		838.3 time, 840.6 real, 6158.9 MB
[runlim] sample:		848.3 time, 850.6 real, 6159.1 MB
[runlim] sample:		858.3 time, 860.6 real, 6159.7 MB
[runlim] sample:		868.3 time, 870.6 real, 6160.2 MB
[runlim] sample:		878.2 time, 880.6 real, 6160.4 MB
[runlim] sample:		888.2 time, 890.6 real, 6160.6 MB
[runlim] sample:		898.2 time, 900.6 real, 6161.2 MB
[runlim] sample:		908.2 time, 910.6 real, 6161.4 MB
[runlim] sample:		918.2 time, 920.6 real, 6161.9 MB
[runlim] sample:		928.2 time, 930.6 real, 6163.5 MB
[runlim] sample:		938.2 time, 940.6 real, 6163.7 MB
[runlim] sample:		948.1 time, 950.6 real, 6166.0 MB
[runlim] sample:		958.1 time, 960.6 real, 6166.0 MB
[runlim] sample:		968.1 time, 970.6 real, 6166.2 MB
[runlim] sample:		978.1 time, 980.6 real, 6166.2 MB
[runlim] sample:		988.1 time, 990.6 real, 6166.2 MB
[runlim] sample:		998.1 time, 1000.6 real, 6166.7 MB
[runlim] sample:		1008.0 time, 1010.6 real, 6168.7 MB
[runlim] sample:		1018.0 time, 1020.6 real, 6168.7 MB
[runlim] sample:		1028.0 time, 1030.6 real, 6168.7 MB
[runlim] sample:		1038.0 time, 1040.6 real, 6169.0 MB
[runlim] sample:		1048.0 time, 1050.6 real, 6169.0 MB
[runlim] sample:		1058.0 time, 1060.6 real, 6171.0 MB
[runlim] sample:		1068.0 time, 1070.6 real, 6171.2 MB
[runlim] sample:		1077.9 time, 1080.6 real, 6171.5 MB
[runlim] sample:		1087.9 time, 1090.6 real, 6171.5 MB
[runlim] sample:		1097.9 time, 1100.6 real, 6171.8 MB
[runlim] sample:		1107.9 time, 1110.6 real, 6172.0 MB
[runlim] sample:		1117.9 time, 1120.6 real, 6174.0 MB
[runlim] sample:		1127.9 time, 1130.6 real, 6174.0 MB
[runlim] sample:		1137.8 time, 1140.6 real, 6174.3 MB
[runlim] sample:		1147.8 time, 1150.6 real, 6320.3 MB
[runlim] sample:		1157.8 time, 1160.6 real, 6382.1 MB
[runlim] sample:		1167.8 time, 1170.6 real, 6422.7 MB
[runlim] sample:		1177.8 time, 1180.6 real, 6444.6 MB
[runlim] sample:		1187.8 time, 1190.6 real, 6444.6 MB
[runlim] sample:		1197.8 time, 1200.6 real, 6444.9 MB
[runlim] sample:		1207.8 time, 1210.6 real, 6444.9 MB
[runlim] sample:		1217.7 time, 1220.6 real, 6444.9 MB
[runlim] sample:		1227.7 time, 1230.6 real, 6444.9 MB
[runlim] sample:		1237.7 time, 1240.6 real, 6447.1 MB
[runlim] sample:		1247.7 time, 1250.6 real, 6447.4 MB
[runlim] sample:		1257.7 time, 1260.6 real, 6447.6 MB
[runlim] sample:		1267.7 time, 1270.6 real, 6447.9 MB
[runlim] sample:		1277.6 time, 1280.6 real, 6448.2 MB
[runlim] sample:		1287.6 time, 1290.6 real, 6450.4 MB
[runlim] sample:		1297.6 time, 1300.6 real, 6450.7 MB
[runlim] sample:		1307.6 time, 1310.6 real, 6450.7 MB
[runlim] sample:		1317.6 time, 1320.6 real, 6450.9 MB
[runlim] sample:		1327.6 time, 1330.6 real, 6450.9 MB
[runlim] sample:		1337.5 time, 1340.6 real, 6450.9 MB
[runlim] sample:		1347.5 time, 1350.6 real, 6453.2 MB
[runlim] sample:		1357.5 time, 1360.6 real, 6453.2 MB
[runlim] sample:		1367.5 time, 1370.6 real, 6453.2 MB
[runlim] sample:		1377.5 time, 1380.6 real, 6453.4 MB
[runlim] sample:		1387.5 time, 1390.6 real, 6454.0 MB
[runlim] sample:		1397.5 time, 1400.6 real, 6454.0 MB
[runlim] sample:		1407.5 time, 1410.6 real, 6456.0 MB
[runlim] sample:		1417.4 time, 1420.6 real, 6458.0 MB
[runlim] sample:		1427.4 time, 1430.6 real, 6458.0 MB
[runlim] sample:		1437.4 time, 1440.6 real, 6458.0 MB
[runlim] sample:		1447.4 time, 1450.6 real, 6458.0 MB
[runlim] sample:		1457.4 time, 1460.6 real, 6458.0 MB
Fatal error: out of memory.
[runlim] end:			Tue Sep 29 05:51:47 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		73443
[runlim] real:			1469.74 seconds
[runlim] time:			1466.25 seconds
[runlim] space:			6598.9 MB
[runlim] samples:		14691
