[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/avy/single.avy
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/bob12s03.aig
[runlim] start:			Sun Sep 20 16:55:26 2015
[runlim] main pid:		19320
[runlim] sample:		16.1 time, 10.3 real, 281.2 MB
[runlim] sample:		55.7 time, 20.3 real, 319.7 MB
[runlim] sample:		95.2 time, 30.3 real, 354.4 MB
[runlim] sample:		134.7 time, 40.3 real, 470.2 MB
[runlim] sample:		174.2 time, 50.3 real, 476.4 MB
[runlim] sample:		213.8 time, 60.3 real, 434.5 MB
[runlim] sample:		253.4 time, 70.3 real, 476.0 MB
[runlim] sample:		292.9 time, 80.3 real, 500.3 MB
[runlim] sample:		332.5 time, 90.3 real, 496.2 MB
[runlim] sample:		372.1 time, 100.3 real, 521.0 MB
[runlim] sample:		411.6 time, 110.3 real, 479.6 MB
[runlim] sample:		451.1 time, 120.3 real, 521.9 MB
[runlim] sample:		490.7 time, 130.3 real, 531.2 MB
[runlim] sample:		530.1 time, 140.3 real, 575.8 MB
[runlim] sample:		569.7 time, 150.3 real, 501.9 MB
[runlim] sample:		609.3 time, 160.3 real, 503.9 MB
[runlim] sample:		648.8 time, 170.3 real, 505.5 MB
[runlim] sample:		688.3 time, 180.3 real, 610.0 MB
[runlim] sample:		727.9 time, 190.3 real, 656.0 MB
[runlim] sample:		767.4 time, 200.3 real, 691.8 MB
[runlim] sample:		806.9 time, 210.3 real, 693.2 MB
[runlim] sample:		846.5 time, 220.3 real, 696.2 MB
[runlim] sample:		886.0 time, 230.3 real, 699.9 MB
[runlim] sample:		925.6 time, 240.3 real, 707.0 MB
[runlim] sample:		965.2 time, 250.3 real, 827.6 MB
[runlim] sample:		1004.7 time, 260.3 real, 847.0 MB
[runlim] sample:		1044.2 time, 270.3 real, 852.0 MB
[runlim] sample:		1083.8 time, 280.3 real, 854.1 MB
[runlim] sample:		1123.2 time, 290.3 real, 855.3 MB
[runlim] sample:		1162.8 time, 300.3 real, 864.3 MB
[runlim] sample:		1202.3 time, 310.3 real, 866.4 MB
[runlim] sample:		1241.9 time, 320.3 real, 867.2 MB
[runlim] sample:		1281.4 time, 330.3 real, 868.0 MB
[runlim] sample:		1320.9 time, 340.3 real, 868.7 MB
[runlim] sample:		1360.5 time, 350.3 real, 869.5 MB
[runlim] sample:		1400.0 time, 360.3 real, 870.0 MB
[runlim] sample:		1439.6 time, 370.3 real, 871.1 MB
[runlim] sample:		1479.1 time, 380.3 real, 873.0 MB
[runlim] sample:		1518.6 time, 390.3 real, 873.8 MB
[runlim] sample:		1558.1 time, 400.3 real, 876.8 MB
[runlim] sample:		1597.7 time, 410.3 real, 877.3 MB
[runlim] sample:		1637.2 time, 420.3 real, 810.3 MB
[runlim] sample:		1676.8 time, 430.3 real, 765.8 MB
[runlim] sample:		1716.3 time, 440.3 real, 777.2 MB
[runlim] sample:		1755.9 time, 450.3 real, 702.8 MB
[runlim] sample:		1795.4 time, 460.3 real, 749.8 MB
[runlim] sample:		1835.0 time, 470.3 real, 755.1 MB
[runlim] sample:		1874.6 time, 480.3 real, 759.2 MB
[runlim] sample:		1914.1 time, 490.3 real, 759.2 MB
[runlim] sample:		1953.7 time, 500.3 real, 752.3 MB
[runlim] sample:		1993.2 time, 510.3 real, 752.3 MB
[runlim] sample:		2032.8 time, 520.3 real, 717.3 MB
[runlim] sample:		2072.4 time, 530.3 real, 723.4 MB
[runlim] sample:		2111.9 time, 540.3 real, 725.4 MB
[runlim] sample:		2151.5 time, 550.3 real, 748.2 MB
[runlim] sample:		2191.1 time, 560.3 real, 702.9 MB
[runlim] sample:		2230.6 time, 570.3 real, 704.1 MB
[runlim] sample:		2270.2 time, 580.3 real, 708.6 MB
[runlim] sample:		2309.8 time, 590.3 real, 709.4 MB
[runlim] sample:		2349.3 time, 600.3 real, 726.1 MB
[runlim] sample:		2388.8 time, 610.3 real, 728.7 MB
[runlim] sample:		2428.4 time, 620.3 real, 731.5 MB
[runlim] sample:		2467.9 time, 630.3 real, 732.8 MB
[runlim] sample:		2507.4 time, 640.3 real, 733.3 MB
[runlim] sample:		2547.0 time, 650.3 real, 733.9 MB
[runlim] sample:		2586.5 time, 660.3 real, 743.9 MB
[runlim] sample:		2626.1 time, 670.3 real, 746.7 MB
[runlim] sample:		2665.6 time, 680.3 real, 778.2 MB
[runlim] sample:		2705.2 time, 690.3 real, 778.9 MB
[runlim] sample:		2744.7 time, 700.3 real, 779.7 MB
[runlim] sample:		2784.2 time, 710.3 real, 781.0 MB
[runlim] sample:		2823.8 time, 720.3 real, 781.8 MB
[runlim] sample:		2863.3 time, 730.3 real, 783.0 MB
[runlim] sample:		2902.8 time, 740.3 real, 785.6 MB
[runlim] sample:		2942.3 time, 750.3 real, 788.1 MB
[runlim] sample:		2981.8 time, 760.3 real, 788.3 MB
[runlim] sample:		3021.3 time, 770.3 real, 790.6 MB
[runlim] sample:		3060.8 time, 780.3 real, 791.1 MB
[runlim] sample:		3100.4 time, 790.3 real, 795.1 MB
[runlim] sample:		3139.9 time, 800.3 real, 797.6 MB
[runlim] end:			Sun Sep 20 17:08:47 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		31848
[runlim] real:			801.04 seconds
[runlim] time:			3141.90 seconds
[runlim] space:			877.5 MB
[runlim] samples:		8007
