[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/oski15/submission/single/oski15a14b10s.aig
[runlim] start:			Thu Sep 17 08:02:38 2015
[runlim] main pid:		425
[runlim] sample:		35.3 time, 10.3 real, 1137.1 MB
[runlim] sample:		67.6 time, 20.3 real, 1067.4 MB
[runlim] sample:		107.2 time, 30.3 real, 1124.0 MB
[runlim] sample:		139.1 time, 40.3 real, 1113.3 MB
[runlim] sample:		168.5 time, 50.3 real, 1111.9 MB
[runlim] sample:		207.9 time, 60.3 real, 1141.0 MB
[runlim] sample:		230.1 time, 70.3 real, 1060.1 MB
[runlim] sample:		269.6 time, 80.3 real, 1073.9 MB
[runlim] sample:		255.1 time, 90.3 real, 1110.7 MB
[runlim] sample:		9.3 time, 100.3 real, 570.9 MB
[runlim] sample:		48.9 time, 110.3 real, 685.0 MB
[runlim] sample:		88.5 time, 120.3 real, 719.4 MB
[runlim] sample:		128.0 time, 130.3 real, 777.5 MB
[runlim] sample:		167.6 time, 140.3 real, 805.8 MB
[runlim] sample:		207.2 time, 150.3 real, 818.8 MB
[runlim] sample:		246.7 time, 160.3 real, 842.5 MB
[runlim] sample:		286.3 time, 170.3 real, 849.9 MB
[runlim] sample:		325.9 time, 180.3 real, 857.7 MB
[runlim] sample:		365.4 time, 190.3 real, 877.4 MB
[runlim] sample:		405.0 time, 200.3 real, 884.1 MB
[runlim] sample:		444.6 time, 210.3 real, 895.0 MB
[runlim] sample:		484.2 time, 220.3 real, 899.6 MB
[runlim] sample:		523.7 time, 230.3 real, 931.7 MB
[runlim] sample:		563.2 time, 240.3 real, 937.0 MB
[runlim] sample:		602.8 time, 250.3 real, 939.1 MB
[runlim] sample:		642.4 time, 260.3 real, 943.6 MB
[runlim] sample:		681.9 time, 270.3 real, 950.8 MB
[runlim] sample:		721.5 time, 280.3 real, 957.9 MB
[runlim] sample:		761.0 time, 290.3 real, 962.6 MB
[runlim] sample:		800.6 time, 300.3 real, 967.8 MB
[runlim] sample:		840.2 time, 310.3 real, 973.1 MB
[runlim] sample:		879.7 time, 320.3 real, 978.0 MB
[runlim] sample:		919.3 time, 330.3 real, 985.5 MB
[runlim] sample:		958.9 time, 340.3 real, 1003.8 MB
[runlim] sample:		998.4 time, 350.3 real, 1008.5 MB
[runlim] sample:		1038.0 time, 360.3 real, 1018.1 MB
[runlim] sample:		1077.6 time, 370.3 real, 1021.2 MB
[runlim] sample:		1117.2 time, 380.3 real, 1027.3 MB
[runlim] sample:		1156.7 time, 390.3 real, 1045.4 MB
[runlim] sample:		1196.3 time, 400.3 real, 1053.0 MB
[runlim] sample:		1235.8 time, 410.3 real, 1057.6 MB
[runlim] sample:		1275.4 time, 420.3 real, 1067.7 MB
[runlim] sample:		1315.0 time, 430.3 real, 1069.4 MB
[runlim] sample:		1354.5 time, 440.3 real, 1074.0 MB
[runlim] sample:		1394.1 time, 450.3 real, 1083.4 MB
[runlim] sample:		1433.7 time, 460.3 real, 1086.3 MB
[runlim] sample:		1473.2 time, 470.3 real, 1095.5 MB
[runlim] sample:		1512.8 time, 480.3 real, 1104.7 MB
[runlim] sample:		1552.4 time, 490.3 real, 1108.1 MB
[runlim] sample:		1592.0 time, 500.3 real, 1110.0 MB
[runlim] sample:		1631.6 time, 510.3 real, 1113.6 MB
[runlim] sample:		1671.1 time, 520.3 real, 1129.8 MB
[runlim] sample:		1710.7 time, 530.3 real, 1162.1 MB
[runlim] sample:		1750.3 time, 540.3 real, 1164.9 MB
[runlim] sample:		1789.9 time, 550.3 real, 1170.5 MB
[runlim] sample:		1829.4 time, 560.3 real, 1173.8 MB
[runlim] sample:		1869.0 time, 570.3 real, 1176.8 MB
[runlim] sample:		1908.5 time, 580.3 real, 1183.3 MB
[runlim] sample:		1948.1 time, 590.3 real, 1187.6 MB
[runlim] sample:		1987.7 time, 600.3 real, 1193.7 MB
[runlim] sample:		2027.2 time, 610.3 real, 1205.2 MB
[runlim] sample:		2066.8 time, 620.3 real, 1219.0 MB
[runlim] sample:		2106.3 time, 630.3 real, 1226.6 MB
[runlim] sample:		2145.9 time, 640.3 real, 1234.1 MB
[runlim] sample:		2185.4 time, 650.3 real, 1246.0 MB
[runlim] sample:		2225.0 time, 660.3 real, 1251.0 MB
[runlim] sample:		2264.6 time, 670.3 real, 1257.1 MB
[runlim] sample:		2304.2 time, 680.3 real, 1257.4 MB
[runlim] sample:		2343.7 time, 690.3 real, 1261.2 MB
[runlim] sample:		2383.3 time, 700.3 real, 1266.1 MB
[runlim] sample:		2422.9 time, 710.3 real, 1269.6 MB
[runlim] sample:		2462.5 time, 720.3 real, 1277.8 MB
[runlim] sample:		2502.1 time, 730.3 real, 1276.8 MB
[runlim] sample:		2541.6 time, 740.3 real, 1281.6 MB
[runlim] sample:		2581.2 time, 750.3 real, 1282.5 MB
[runlim] sample:		2620.8 time, 760.3 real, 1289.1 MB
[runlim] sample:		2660.3 time, 770.3 real, 1290.9 MB
[runlim] sample:		2699.9 time, 780.3 real, 1294.4 MB
[runlim] sample:		2739.5 time, 790.3 real, 1301.2 MB
[runlim] sample:		2779.1 time, 800.3 real, 1304.6 MB
[runlim] sample:		2818.7 time, 810.3 real, 1307.6 MB
[runlim] sample:		2858.3 time, 820.3 real, 1312.0 MB
[runlim] end:			Thu Sep 17 08:16:24 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		104298
[runlim] real:			826.43 seconds
[runlim] time:			2881.24 seconds
[runlim] space:			1314.3 MB
[runlim] samples:		8261
