[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.iprover
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/beempgmprot1f2.aig
[runlim] start:			Sun Sep 20 12:12:22 2015
[runlim] main pid:		9553
[runlim] sample:		9.8 time, 10.3 real, 381.8 MB
[runlim] sample:		19.8 time, 20.3 real, 688.3 MB
[runlim] sample:		29.8 time, 30.3 real, 1023.2 MB
[runlim] sample:		39.8 time, 40.3 real, 1212.9 MB
[runlim] sample:		49.8 time, 50.3 real, 1443.4 MB
[runlim] sample:		59.8 time, 60.3 real, 1714.0 MB
[runlim] sample:		69.8 time, 70.3 real, 1936.1 MB
[runlim] sample:		79.8 time, 80.3 real, 2167.7 MB
[runlim] sample:		89.7 time, 90.3 real, 2314.7 MB
[runlim] sample:		99.7 time, 100.3 real, 2437.5 MB
[runlim] sample:		109.7 time, 110.3 real, 2648.0 MB
[runlim] sample:		119.7 time, 120.3 real, 2852.3 MB
[runlim] sample:		129.7 time, 130.3 real, 3111.3 MB
[runlim] sample:		139.7 time, 140.3 real, 3345.5 MB
[runlim] sample:		149.7 time, 150.3 real, 3523.6 MB
[runlim] sample:		159.7 time, 160.3 real, 3711.4 MB
[runlim] sample:		169.7 time, 170.3 real, 3895.3 MB
[runlim] sample:		179.6 time, 180.3 real, 4077.1 MB
[runlim] sample:		189.6 time, 190.3 real, 4261.4 MB
[runlim] sample:		199.6 time, 200.3 real, 4462.8 MB
[runlim] sample:		209.6 time, 210.3 real, 4561.5 MB
[runlim] sample:		219.6 time, 220.3 real, 4626.5 MB
[runlim] sample:		229.6 time, 230.3 real, 4631.9 MB
[runlim] sample:		239.6 time, 240.3 real, 4702.1 MB
[runlim] sample:		249.5 time, 250.3 real, 4844.1 MB
[runlim] sample:		259.5 time, 260.3 real, 5018.7 MB
[runlim] sample:		269.5 time, 270.3 real, 5193.2 MB
[runlim] sample:		279.5 time, 280.3 real, 5229.9 MB
[runlim] sample:		289.5 time, 290.3 real, 5238.1 MB
[runlim] sample:		299.5 time, 300.3 real, 5246.6 MB
[runlim] sample:		309.5 time, 310.3 real, 5255.1 MB
[runlim] sample:		319.5 time, 320.3 real, 5265.4 MB
[runlim] sample:		329.5 time, 330.3 real, 5272.8 MB
[runlim] sample:		339.4 time, 340.3 real, 5283.1 MB
[runlim] sample:		349.4 time, 350.3 real, 5291.3 MB
[runlim] sample:		359.4 time, 360.3 real, 5299.5 MB
[runlim] sample:		369.4 time, 370.3 real, 5387.9 MB
[runlim] sample:		379.4 time, 380.3 real, 5490.6 MB
[runlim] sample:		389.4 time, 390.3 real, 5500.6 MB
[runlim] sample:		399.4 time, 400.3 real, 5509.2 MB
[runlim] sample:		409.4 time, 410.3 real, 5517.2 MB
[runlim] sample:		419.4 time, 420.3 real, 5525.2 MB
[runlim] sample:		429.4 time, 430.3 real, 5533.2 MB
[runlim] sample:		439.4 time, 440.3 real, 5543.4 MB
[runlim] sample:		449.3 time, 450.3 real, 5601.4 MB
[runlim] sample:		459.3 time, 460.3 real, 5727.5 MB
[runlim] sample:		469.3 time, 470.3 real, 5735.8 MB
[runlim] sample:		479.3 time, 480.3 real, 5747.0 MB
[runlim] sample:		489.3 time, 490.3 real, 5756.3 MB
[runlim] sample:		499.3 time, 500.3 real, 5766.1 MB
[runlim] sample:		509.3 time, 510.3 real, 5774.1 MB
[runlim] sample:		519.3 time, 520.3 real, 5782.3 MB
[runlim] sample:		529.3 time, 530.3 real, 5790.6 MB
[runlim] sample:		539.3 time, 540.3 real, 5800.6 MB
[runlim] sample:		549.2 time, 550.3 real, 5809.6 MB
[runlim] sample:		559.2 time, 560.3 real, 5817.9 MB
[runlim] sample:		569.2 time, 570.3 real, 5826.4 MB
[runlim] sample:		579.2 time, 580.3 real, 5834.6 MB
[runlim] sample:		589.2 time, 590.3 real, 5840.6 MB
[runlim] sample:		599.2 time, 600.3 real, 5846.8 MB
[runlim] sample:		609.2 time, 610.3 real, 5855.1 MB
[runlim] sample:		619.2 time, 620.3 real, 5863.3 MB
[runlim] sample:		629.2 time, 630.3 real, 5871.6 MB
[runlim] sample:		639.2 time, 640.3 real, 5878.1 MB
[runlim] sample:		649.1 time, 650.3 real, 5884.1 MB
[runlim] sample:		659.1 time, 660.3 real, 6006.7 MB
[runlim] sample:		669.1 time, 670.3 real, 6076.1 MB
[runlim] sample:		679.1 time, 680.3 real, 6084.8 MB
[runlim] sample:		689.1 time, 690.3 real, 6093.8 MB
[runlim] sample:		699.1 time, 700.3 real, 6102.8 MB
[runlim] sample:		709.1 time, 710.3 real, 6112.6 MB
[runlim] sample:		719.1 time, 720.3 real, 6121.1 MB
[runlim] sample:		729.1 time, 730.3 real, 6129.6 MB
[runlim] sample:		739.0 time, 740.3 real, 6138.6 MB
[runlim] sample:		749.0 time, 750.3 real, 6149.2 MB
[runlim] sample:		759.0 time, 760.3 real, 6158.4 MB
[runlim] sample:		769.0 time, 770.3 real, 6167.2 MB
[runlim] sample:		779.0 time, 780.3 real, 6176.2 MB
[runlim] sample:		789.0 time, 790.3 real, 6183.9 MB
[runlim] sample:		799.0 time, 800.3 real, 6192.2 MB
[runlim] sample:		809.1 time, 810.4 real, 6189.9 MB
[runlim] sample:		819.1 time, 820.4 real, 6198.8 MB
[runlim] sample:		829.1 time, 830.4 real, 6207.2 MB
[runlim] sample:		839.1 time, 840.4 real, 6215.4 MB
[runlim] sample:		849.1 time, 850.4 real, 6224.4 MB
[runlim] sample:		859.0 time, 860.4 real, 6232.9 MB
[runlim] sample:		869.0 time, 870.4 real, 6240.4 MB
[runlim] sample:		879.0 time, 880.4 real, 6248.1 MB
[runlim] sample:		889.0 time, 890.4 real, 6256.6 MB
[runlim] sample:		899.0 time, 900.4 real, 6265.6 MB
[runlim] sample:		9.6 time, 910.4 real, 381.3 MB
[runlim] sample:		19.6 time, 920.4 real, 641.5 MB
[runlim] sample:		29.6 time, 930.4 real, 893.6 MB
[runlim] sample:		39.5 time, 940.4 real, 1116.9 MB
[runlim] sample:		49.5 time, 950.4 real, 1243.1 MB
[runlim] sample:		59.5 time, 960.4 real, 1488.1 MB
[runlim] sample:		69.5 time, 970.4 real, 1682.3 MB
[runlim] sample:		79.5 time, 980.4 real, 1854.6 MB
[runlim] sample:		89.5 time, 990.4 real, 2066.3 MB
[runlim] sample:		99.5 time, 1000.4 real, 2193.7 MB
[runlim] sample:		109.5 time, 1010.4 real, 2296.2 MB
[runlim] sample:		119.5 time, 1020.4 real, 2478.2 MB
[runlim] sample:		129.4 time, 1030.4 real, 2654.3 MB
[runlim] sample:		139.4 time, 1040.4 real, 2839.6 MB
[runlim] sample:		149.4 time, 1050.4 real, 3019.8 MB
[runlim] sample:		159.4 time, 1060.4 real, 3188.1 MB
[runlim] sample:		169.4 time, 1070.4 real, 3386.4 MB
[runlim] sample:		179.4 time, 1080.4 real, 3608.4 MB
[runlim] sample:		189.4 time, 1090.4 real, 3786.4 MB
[runlim] sample:		199.4 time, 1100.4 real, 3944.6 MB
[runlim] sample:		209.3 time, 1110.4 real, 4140.0 MB
[runlim] sample:		219.3 time, 1120.4 real, 4320.1 MB
[runlim] sample:		229.3 time, 1130.4 real, 4470.9 MB
[runlim] sample:		239.3 time, 1140.4 real, 4537.4 MB
[runlim] sample:		249.3 time, 1150.4 real, 4589.6 MB
[runlim] sample:		259.3 time, 1160.4 real, 4629.5 MB
[runlim] sample:		269.3 time, 1170.4 real, 4788.9 MB
[runlim] sample:		279.3 time, 1180.4 real, 4928.1 MB
[runlim] sample:		289.2 time, 1190.4 real, 5087.0 MB
[runlim] sample:		299.2 time, 1200.4 real, 5258.9 MB
[runlim] sample:		309.2 time, 1210.4 real, 5431.7 MB
[runlim] sample:		319.2 time, 1220.4 real, 5590.1 MB
[runlim] sample:		329.2 time, 1230.4 real, 5745.0 MB
[runlim] sample:		339.2 time, 1240.4 real, 5917.2 MB
[runlim] sample:		349.2 time, 1250.4 real, 6068.8 MB
[runlim] sample:		359.2 time, 1260.4 real, 6231.9 MB
[runlim] sample:		369.1 time, 1270.4 real, 6390.9 MB
[runlim] sample:		379.1 time, 1280.4 real, 6549.7 MB
[runlim] end:			Sun Sep 20 12:33:49 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		77183
[runlim] real:			1287.02 seconds
[runlim] time:			899.09 seconds
[runlim] space:			6652.0 MB
[runlim] samples:		12866
