[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/pdtpmsudc8.aig
[runlim] start:			Fri Sep 18 17:32:22 2015
[runlim] main pid:		2985
[runlim] sample:		38.4 time, 10.4 real, 212.8 MB
[runlim] sample:		78.0 time, 20.4 real, 276.4 MB
[runlim] sample:		117.7 time, 30.4 real, 319.2 MB
[runlim] sample:		157.2 time, 40.4 real, 397.7 MB
[runlim] sample:		196.8 time, 50.4 real, 418.9 MB
[runlim] sample:		236.4 time, 60.4 real, 515.0 MB
[runlim] sample:		276.0 time, 70.4 real, 549.0 MB
[runlim] sample:		315.6 time, 80.4 real, 559.1 MB
[runlim] sample:		355.2 time, 90.4 real, 634.9 MB
[runlim] sample:		394.8 time, 100.4 real, 724.7 MB
[runlim] sample:		434.4 time, 110.4 real, 696.9 MB
[runlim] sample:		474.0 time, 120.4 real, 749.9 MB
[runlim] sample:		513.7 time, 130.4 real, 816.4 MB
[runlim] sample:		553.3 time, 140.4 real, 877.3 MB
[runlim] sample:		592.9 time, 150.4 real, 905.7 MB
[runlim] sample:		632.5 time, 160.4 real, 857.6 MB
[runlim] sample:		672.0 time, 170.4 real, 887.1 MB
[runlim] sample:		711.6 time, 180.4 real, 949.2 MB
[runlim] sample:		751.2 time, 190.4 real, 1021.6 MB
[runlim] sample:		790.8 time, 200.4 real, 1056.5 MB
[runlim] sample:		830.4 time, 210.4 real, 1082.5 MB
[runlim] sample:		870.0 time, 220.4 real, 1106.4 MB
[runlim] sample:		909.6 time, 230.4 real, 1140.7 MB
[runlim] sample:		949.2 time, 240.4 real, 1071.2 MB
[runlim] sample:		988.8 time, 250.4 real, 1096.7 MB
[runlim] sample:		1028.4 time, 260.4 real, 1167.0 MB
[runlim] sample:		1068.0 time, 270.4 real, 1200.1 MB
[runlim] sample:		1107.6 time, 280.4 real, 1282.1 MB
[runlim] sample:		1147.2 time, 290.4 real, 1265.2 MB
[runlim] sample:		1186.8 time, 300.4 real, 1280.3 MB
[runlim] sample:		1226.4 time, 310.4 real, 1353.9 MB
[runlim] sample:		1266.0 time, 320.4 real, 1298.8 MB
[runlim] sample:		1305.7 time, 330.4 real, 1310.6 MB
[runlim] sample:		1345.3 time, 340.4 real, 1320.4 MB
[runlim] sample:		1384.9 time, 350.4 real, 1390.7 MB
[runlim] sample:		1424.6 time, 360.4 real, 1368.7 MB
[runlim] sample:		1464.2 time, 370.4 real, 1439.6 MB
[runlim] sample:		1503.8 time, 380.4 real, 1580.7 MB
[runlim] sample:		1543.4 time, 390.4 real, 1613.6 MB
[runlim] sample:		1583.0 time, 400.4 real, 1647.2 MB
[runlim] sample:		1622.6 time, 410.4 real, 1655.2 MB
[runlim] sample:		1662.2 time, 420.4 real, 1580.2 MB
[runlim] sample:		1701.8 time, 430.4 real, 1590.3 MB
[runlim] sample:		1741.4 time, 440.4 real, 1635.4 MB
[runlim] sample:		1781.0 time, 450.4 real, 1654.7 MB
[runlim] sample:		1820.6 time, 460.4 real, 1685.2 MB
[runlim] sample:		1860.3 time, 470.4 real, 1711.1 MB
[runlim] sample:		1899.9 time, 480.4 real, 1687.5 MB
[runlim] sample:		1939.5 time, 490.4 real, 1725.5 MB
[runlim] sample:		1979.0 time, 500.4 real, 1771.8 MB
[runlim] sample:		2018.6 time, 510.4 real, 1786.2 MB
[runlim] sample:		2058.2 time, 520.4 real, 1829.7 MB
[runlim] sample:		2097.8 time, 530.4 real, 1834.6 MB
[runlim] sample:		2137.4 time, 540.4 real, 1876.9 MB
[runlim] sample:		2177.0 time, 550.4 real, 1883.6 MB
[runlim] sample:		2216.6 time, 560.4 real, 1963.9 MB
[runlim] sample:		2256.2 time, 570.4 real, 1975.8 MB
[runlim] sample:		2295.8 time, 580.4 real, 1992.1 MB
[runlim] sample:		2335.4 time, 590.4 real, 2035.6 MB
[runlim] sample:		2375.0 time, 600.4 real, 2040.0 MB
[runlim] sample:		2414.6 time, 610.4 real, 2003.1 MB
[runlim] sample:		2454.3 time, 620.4 real, 1992.2 MB
[runlim] sample:		2493.9 time, 630.4 real, 2040.4 MB
[runlim] sample:		2533.5 time, 640.4 real, 2068.9 MB
[runlim] sample:		2573.1 time, 650.4 real, 2090.0 MB
[runlim] sample:		2612.7 time, 660.4 real, 2184.1 MB
[runlim] sample:		2652.3 time, 670.4 real, 2132.6 MB
[runlim] sample:		2691.9 time, 680.4 real, 2164.6 MB
[runlim] sample:		2731.5 time, 690.4 real, 2387.6 MB
[runlim] sample:		2771.1 time, 700.4 real, 2407.9 MB
[runlim] sample:		2810.8 time, 710.4 real, 2461.8 MB
[runlim] sample:		2850.4 time, 720.4 real, 2447.2 MB
[runlim] sample:		2890.0 time, 730.4 real, 2464.7 MB
[runlim] sample:		2929.6 time, 740.4 real, 2414.1 MB
[runlim] sample:		2969.2 time, 750.4 real, 2500.0 MB
[runlim] sample:		3008.7 time, 760.4 real, 2519.8 MB
[runlim] sample:		3048.3 time, 770.4 real, 2508.4 MB
[runlim] sample:		3087.9 time, 780.4 real, 2568.1 MB
[runlim] sample:		3127.5 time, 790.4 real, 2542.0 MB
[runlim] sample:		3167.0 time, 800.4 real, 2563.3 MB
[runlim] sample:		3206.6 time, 810.4 real, 2620.8 MB
[runlim] sample:		3246.2 time, 820.4 real, 2666.5 MB
[runlim] sample:		3285.8 time, 830.4 real, 2650.1 MB
[runlim] sample:		3325.4 time, 840.4 real, 2631.0 MB
[runlim] sample:		3365.0 time, 850.4 real, 2656.6 MB
[runlim] sample:		3404.6 time, 860.4 real, 2675.1 MB
[runlim] sample:		3444.2 time, 870.4 real, 2791.4 MB
[runlim] sample:		3483.8 time, 880.4 real, 2817.4 MB
[runlim] sample:		3523.4 time, 890.4 real, 2799.4 MB
[runlim] sample:		3563.0 time, 900.4 real, 2818.7 MB
[runlim] sample:		3602.6 time, 910.4 real, 2840.5 MB
[runlim] sample:		3642.2 time, 920.4 real, 2807.1 MB
[runlim] end:			Fri Sep 18 17:47:42 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		36804
[runlim] real:			920.90 seconds
[runlim] time:			3643.00 seconds
[runlim] space:			2894.1 MB
[runlim] samples:		9205
