[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/aigbmc/single.aigbmc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/6s326rb08.aig
[runlim] start:			Sun Sep 20 13:47:42 2015
[runlim] main pid:		9840
[runlim] sample:		9.9 time, 10.3 real, 607.8 MB
[runlim] sample:		19.9 time, 20.3 real, 867.2 MB
[runlim] sample:		29.8 time, 30.3 real, 1013.2 MB
[runlim] sample:		39.8 time, 40.3 real, 1113.1 MB
[runlim] sample:		49.8 time, 50.3 real, 1233.1 MB
[runlim] sample:		59.7 time, 60.3 real, 1502.3 MB
[runlim] sample:		69.7 time, 70.3 real, 1699.2 MB
[runlim] sample:		79.7 time, 80.3 real, 1140.7 MB
[runlim] sample:		89.7 time, 90.3 real, 1186.8 MB
[runlim] sample:		99.6 time, 100.3 real, 1230.7 MB
[runlim] sample:		109.6 time, 110.3 real, 2209.1 MB
[runlim] sample:		119.6 time, 120.3 real, 2285.5 MB
[runlim] sample:		129.5 time, 130.3 real, 1756.9 MB
[runlim] sample:		139.5 time, 140.3 real, 2430.0 MB
[runlim] sample:		149.5 time, 150.3 real, 1563.8 MB
[runlim] sample:		159.4 time, 160.3 real, 2566.0 MB
[runlim] sample:		169.4 time, 170.3 real, 2646.0 MB
[runlim] sample:		179.4 time, 180.3 real, 2469.7 MB
[runlim] sample:		189.4 time, 190.3 real, 2768.8 MB
[runlim] sample:		199.3 time, 200.3 real, 2828.2 MB
[runlim] sample:		209.3 time, 210.3 real, 2276.3 MB
[runlim] sample:		219.3 time, 220.3 real, 2939.0 MB
[runlim] sample:		229.2 time, 230.3 real, 2928.3 MB
[runlim] sample:		239.2 time, 240.3 real, 2279.8 MB
[runlim] sample:		249.2 time, 250.3 real, 3351.3 MB
[runlim] sample:		259.2 time, 260.3 real, 3410.6 MB
[runlim] sample:		269.1 time, 270.3 real, 3461.6 MB
[runlim] sample:		279.1 time, 280.3 real, 3261.6 MB
[runlim] sample:		289.1 time, 290.3 real, 2230.6 MB
[runlim] sample:		299.1 time, 300.3 real, 3039.6 MB
[runlim] sample:		309.0 time, 310.3 real, 3469.6 MB
[runlim] sample:		319.0 time, 320.3 real, 3424.4 MB
[runlim] sample:		329.0 time, 330.3 real, 2923.4 MB
[runlim] sample:		338.9 time, 340.3 real, 3793.1 MB
[runlim] sample:		348.9 time, 350.3 real, 3296.7 MB
[runlim] sample:		358.9 time, 360.3 real, 3882.4 MB
[runlim] sample:		368.8 time, 370.3 real, 3925.0 MB
[runlim] sample:		378.8 time, 380.3 real, 3967.5 MB
[runlim] sample:		388.8 time, 390.3 real, 4010.1 MB
[runlim] sample:		398.7 time, 400.3 real, 4052.7 MB
[runlim] sample:		408.7 time, 410.3 real, 3084.2 MB
[runlim] sample:		418.7 time, 420.3 real, 4389.7 MB
[runlim] sample:		428.6 time, 430.3 real, 2955.9 MB
[runlim] sample:		438.6 time, 440.3 real, 3989.5 MB
[runlim] sample:		448.5 time, 450.3 real, 4509.1 MB
[runlim] sample:		458.5 time, 460.3 real, 4547.3 MB
[runlim] sample:		468.5 time, 470.3 real, 4585.7 MB
[runlim] sample:		478.4 time, 480.3 real, 4624.2 MB
[runlim] sample:		488.4 time, 490.3 real, 4240.4 MB
[runlim] sample:		498.4 time, 500.3 real, 3390.8 MB
[runlim] sample:		508.4 time, 510.3 real, 4735.2 MB
[runlim] sample:		518.3 time, 520.3 real, 4182.4 MB
[runlim] sample:		528.3 time, 530.3 real, 4807.7 MB
[runlim] sample:		538.2 time, 540.3 real, 3922.1 MB
[runlim] sample:		548.2 time, 550.3 real, 4879.3 MB
[runlim] sample:		558.2 time, 560.3 real, 4912.9 MB
[runlim] sample:		568.1 time, 570.3 real, 3073.0 MB
[runlim] sample:		578.1 time, 580.3 real, 3256.5 MB
[runlim] sample:		588.1 time, 590.3 real, 3398.9 MB
[runlim] sample:		598.0 time, 600.3 real, 3313.3 MB
[runlim] sample:		608.0 time, 610.3 real, 3141.4 MB
[runlim] sample:		618.0 time, 620.3 real, 5113.7 MB
[runlim] sample:		627.9 time, 630.3 real, 5147.3 MB
[runlim] sample:		637.9 time, 640.3 real, 4088.0 MB
[runlim] sample:		647.9 time, 650.3 real, 5243.2 MB
[runlim] sample:		657.8 time, 660.3 real, 5067.5 MB
[runlim] sample:		667.8 time, 670.3 real, 3275.1 MB
[runlim] end:			Sun Sep 20 13:59:00 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			678.53 seconds
[runlim] time:			675.93 seconds
[runlim] space:			5332.4 MB
[runlim] samples:		6782
