[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.abcsuprove
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/intel043.aig
[runlim] start:			Sun Sep 20 22:05:38 2015
[runlim] main pid:		20243
[runlim] sample:		15.2 time, 10.3 real, 981.9 MB
[runlim] sample:		54.2 time, 20.3 real, 2153.8 MB
[runlim] sample:		93.8 time, 30.3 real, 3116.8 MB
[runlim] sample:		133.3 time, 40.3 real, 3243.7 MB
[runlim] sample:		154.2 time, 50.3 real, 3191.9 MB
[runlim] sample:		193.0 time, 60.3 real, 3492.4 MB
[runlim] sample:		232.5 time, 70.3 real, 3423.4 MB
[runlim] sample:		272.1 time, 80.3 real, 3600.2 MB
[runlim] sample:		288.7 time, 90.3 real, 3397.8 MB
[runlim] sample:		328.3 time, 100.3 real, 3441.2 MB
[runlim] sample:		367.8 time, 110.3 real, 3498.8 MB
[runlim] sample:		360.9 time, 120.3 real, 3352.2 MB
[runlim] sample:		400.4 time, 130.3 real, 3545.5 MB
[runlim] sample:		383.7 time, 140.3 real, 3373.3 MB
[runlim] sample:		423.3 time, 150.3 real, 3169.9 MB
[runlim] sample:		418.0 time, 160.3 real, 3047.2 MB
[runlim] sample:		457.6 time, 170.3 real, 3068.4 MB
[runlim] sample:		497.1 time, 180.3 real, 3074.0 MB
[runlim] sample:		536.7 time, 190.3 real, 2916.5 MB
[runlim] sample:		576.3 time, 200.3 real, 3137.5 MB
[runlim] sample:		615.6 time, 210.3 real, 3517.7 MB
[runlim] sample:		655.2 time, 220.3 real, 3543.2 MB
[runlim] sample:		665.2 time, 230.3 real, 3156.4 MB
[runlim] sample:		38.5 time, 240.3 real, 1891.3 MB
[runlim] sample:		78.0 time, 250.3 real, 2406.2 MB
[runlim] sample:		117.6 time, 260.3 real, 2750.5 MB
[runlim] sample:		157.1 time, 270.3 real, 2851.4 MB
[runlim] sample:		196.6 time, 280.3 real, 2958.9 MB
[runlim] sample:		236.2 time, 290.3 real, 3117.1 MB
[runlim] sample:		118.7 time, 300.3 real, 1118.9 MB
[runlim] sample:		157.7 time, 310.3 real, 1124.2 MB
[runlim] sample:		197.3 time, 320.3 real, 1173.6 MB
[runlim] sample:		236.2 time, 330.3 real, 1201.5 MB
[runlim] sample:		274.3 time, 340.3 real, 1227.0 MB
[runlim] sample:		313.9 time, 350.3 real, 1229.1 MB
[runlim] sample:		353.4 time, 360.3 real, 1231.2 MB
[runlim] sample:		392.9 time, 370.3 real, 1237.7 MB
[runlim] sample:		432.5 time, 380.3 real, 1240.5 MB
[runlim] sample:		472.0 time, 390.3 real, 1244.2 MB
[runlim] sample:		511.6 time, 400.3 real, 1253.0 MB
[runlim] sample:		551.2 time, 410.3 real, 1260.7 MB
[runlim] sample:		590.7 time, 420.3 real, 1262.0 MB
[runlim] sample:		629.6 time, 430.3 real, 1277.8 MB
[runlim] sample:		669.1 time, 440.3 real, 1279.6 MB
[runlim] sample:		708.6 time, 450.3 real, 1281.6 MB
[runlim] sample:		748.2 time, 460.3 real, 1285.8 MB
[runlim] sample:		787.7 time, 470.3 real, 1292.6 MB
[runlim] sample:		827.3 time, 480.3 real, 1294.7 MB
[runlim] sample:		866.8 time, 490.3 real, 1297.4 MB
[runlim] sample:		906.4 time, 500.3 real, 1299.0 MB
[runlim] sample:		945.9 time, 510.3 real, 1301.1 MB
[runlim] sample:		985.5 time, 520.3 real, 1302.4 MB
[runlim] sample:		1025.0 time, 530.3 real, 1305.0 MB
[runlim] sample:		1064.5 time, 540.3 real, 1308.0 MB
[runlim] sample:		1104.0 time, 550.3 real, 1312.0 MB
[runlim] end:			Sun Sep 20 22:14:58 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		65235
[runlim] real:			560.11 seconds
[runlim] time:			1129.73 seconds
[runlim] space:			3645.3 MB
[runlim] samples:		5598
