[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/abc/single.abcsimple
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/beempgsol4f1.aig
[runlim] start:			Sat Sep 19 03:38:42 2015
[runlim] main pid:		2974
[runlim] sample:		26.7 time, 10.3 real, 430.2 MB
[runlim] sample:		66.4 time, 20.3 real, 474.5 MB
[runlim] sample:		106.0 time, 30.3 real, 510.3 MB
[runlim] sample:		145.6 time, 40.3 real, 546.4 MB
[runlim] sample:		185.2 time, 50.3 real, 575.2 MB
[runlim] sample:		224.8 time, 60.3 real, 615.2 MB
[runlim] sample:		264.5 time, 70.3 real, 662.4 MB
[runlim] sample:		304.1 time, 80.3 real, 694.1 MB
[runlim] sample:		343.7 time, 90.3 real, 720.7 MB
[runlim] sample:		383.3 time, 100.3 real, 738.4 MB
[runlim] sample:		422.9 time, 110.3 real, 752.5 MB
[runlim] sample:		462.5 time, 120.3 real, 766.2 MB
[runlim] sample:		502.1 time, 130.3 real, 780.1 MB
[runlim] sample:		541.7 time, 140.3 real, 797.2 MB
[runlim] sample:		581.3 time, 150.3 real, 829.2 MB
[runlim] sample:		620.9 time, 160.3 real, 846.3 MB
[runlim] sample:		660.5 time, 170.3 real, 860.9 MB
[runlim] sample:		700.1 time, 180.3 real, 874.2 MB
[runlim] sample:		739.7 time, 190.3 real, 894.2 MB
[runlim] sample:		779.3 time, 200.3 real, 909.6 MB
[runlim] sample:		818.9 time, 210.3 real, 926.1 MB
[runlim] sample:		858.5 time, 220.3 real, 939.1 MB
[runlim] sample:		898.1 time, 230.3 real, 951.1 MB
[runlim] sample:		937.7 time, 240.3 real, 964.3 MB
[runlim] sample:		977.3 time, 250.3 real, 976.4 MB
[runlim] sample:		1016.9 time, 260.3 real, 991.5 MB
[runlim] sample:		1056.5 time, 270.3 real, 1011.6 MB
[runlim] sample:		1096.0 time, 280.3 real, 1059.2 MB
[runlim] sample:		1135.6 time, 290.3 real, 1037.0 MB
[runlim] sample:		1175.2 time, 300.3 real, 1051.6 MB
[runlim] sample:		1214.8 time, 310.3 real, 1067.1 MB
[runlim] sample:		1254.4 time, 320.3 real, 1082.7 MB
[runlim] sample:		1294.0 time, 330.3 real, 1095.5 MB
[runlim] sample:		1333.6 time, 340.3 real, 1104.9 MB
[runlim] sample:		1373.2 time, 350.3 real, 1118.3 MB
[runlim] sample:		1412.8 time, 360.3 real, 1129.1 MB
[runlim] sample:		1452.4 time, 370.3 real, 1139.4 MB
[runlim] sample:		1492.0 time, 380.3 real, 1156.7 MB
[runlim] sample:		1531.5 time, 390.3 real, 1169.1 MB
[runlim] sample:		1571.1 time, 400.3 real, 1181.1 MB
[runlim] sample:		1610.7 time, 410.3 real, 1192.5 MB
[runlim] sample:		1650.3 time, 420.3 real, 1205.4 MB
[runlim] sample:		1689.9 time, 430.3 real, 1221.1 MB
[runlim] sample:		1729.4 time, 440.3 real, 1237.1 MB
[runlim] sample:		1769.1 time, 450.3 real, 1258.1 MB
[runlim] sample:		1808.6 time, 460.3 real, 1280.6 MB
[runlim] sample:		1848.2 time, 470.3 real, 1294.0 MB
[runlim] sample:		1887.8 time, 480.3 real, 1310.0 MB
[runlim] sample:		1927.4 time, 490.3 real, 1323.6 MB
[runlim] sample:		1967.0 time, 500.3 real, 1336.3 MB
[runlim] sample:		2006.5 time, 510.3 real, 1343.7 MB
[runlim] sample:		2046.1 time, 520.3 real, 1352.8 MB
[runlim] sample:		2085.7 time, 530.3 real, 1402.0 MB
[runlim] sample:		2125.3 time, 540.3 real, 1378.9 MB
[runlim] sample:		2164.9 time, 550.3 real, 1391.9 MB
[runlim] sample:		2204.5 time, 560.3 real, 1435.2 MB
[runlim] sample:		2244.0 time, 570.3 real, 1453.8 MB
[runlim] sample:		2283.6 time, 580.3 real, 1416.5 MB
[runlim] sample:		2323.2 time, 590.3 real, 1428.3 MB
[runlim] sample:		2362.8 time, 600.3 real, 1479.7 MB
[runlim] sample:		2402.3 time, 610.3 real, 1498.4 MB
[runlim] sample:		2441.9 time, 620.3 real, 1515.9 MB
[runlim] sample:		2481.5 time, 630.3 real, 1473.3 MB
[runlim] sample:		2521.1 time, 640.3 real, 1521.6 MB
[runlim] sample:		2560.7 time, 650.3 real, 1540.2 MB
[runlim] sample:		2600.2 time, 660.3 real, 1556.2 MB
[runlim] sample:		2639.8 time, 670.3 real, 1572.3 MB
[runlim] sample:		2679.4 time, 680.3 real, 1531.9 MB
[runlim] sample:		2719.0 time, 690.3 real, 1539.7 MB
[runlim] sample:		2758.6 time, 700.3 real, 1584.8 MB
[runlim] sample:		2798.2 time, 710.3 real, 1602.6 MB
[runlim] end:			Sat Sep 19 03:50:35 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		92626
[runlim] real:			713.20 seconds
[runlim] time:			2808.84 seconds
[runlim] space:			1610.7 MB
[runlim] samples:		7128
