[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/iimc/single.iimc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/pdtfifo1to0.aig
[runlim] start:			Sat Sep 19 06:09:22 2015
[runlim] main pid:		3574
[runlim] sample:		39.1 time, 10.3 real, 58.3 MB
[runlim] sample:		78.8 time, 20.3 real, 69.1 MB
[runlim] sample:		118.5 time, 30.3 real, 80.6 MB
[runlim] sample:		158.2 time, 40.3 real, 82.7 MB
[runlim] sample:		197.9 time, 50.3 real, 93.4 MB
[runlim] sample:		237.5 time, 60.3 real, 97.5 MB
[runlim] sample:		277.2 time, 70.3 real, 107.5 MB
[runlim] sample:		316.9 time, 80.3 real, 126.4 MB
[runlim] sample:		356.5 time, 90.3 real, 129.4 MB
[runlim] sample:		396.1 time, 100.3 real, 134.5 MB
[runlim] sample:		435.8 time, 110.3 real, 140.9 MB
[runlim] sample:		475.4 time, 120.3 real, 137.5 MB
[runlim] sample:		515.1 time, 130.3 real, 141.2 MB
[runlim] sample:		554.7 time, 140.3 real, 176.0 MB
[runlim] sample:		594.4 time, 150.3 real, 175.9 MB
[runlim] sample:		634.0 time, 160.3 real, 176.3 MB
[runlim] sample:		673.7 time, 170.3 real, 176.1 MB
[runlim] sample:		713.3 time, 180.3 real, 181.5 MB
[runlim] sample:		753.0 time, 190.3 real, 185.3 MB
[runlim] sample:		792.6 time, 200.3 real, 196.7 MB
[runlim] sample:		832.2 time, 210.3 real, 200.8 MB
[runlim] sample:		871.9 time, 220.3 real, 210.4 MB
[runlim] sample:		911.5 time, 230.3 real, 207.4 MB
[runlim] sample:		951.1 time, 240.3 real, 209.6 MB
[runlim] sample:		990.8 time, 250.3 real, 208.5 MB
[runlim] sample:		1030.4 time, 260.3 real, 216.9 MB
[runlim] sample:		1070.0 time, 270.3 real, 208.8 MB
[runlim] sample:		1109.7 time, 280.3 real, 216.2 MB
[runlim] sample:		1149.3 time, 290.3 real, 227.7 MB
[runlim] sample:		1189.0 time, 300.3 real, 230.3 MB
[runlim] sample:		1228.6 time, 310.3 real, 229.2 MB
[runlim] sample:		1268.2 time, 320.3 real, 246.0 MB
[runlim] sample:		1307.8 time, 330.3 real, 242.3 MB
[runlim] sample:		1347.5 time, 340.3 real, 250.0 MB
[runlim] sample:		1387.1 time, 350.3 real, 237.9 MB
[runlim] sample:		1426.7 time, 360.3 real, 243.9 MB
[runlim] sample:		1466.4 time, 370.3 real, 247.0 MB
[runlim] sample:		1506.0 time, 380.3 real, 249.3 MB
[runlim] sample:		1545.7 time, 390.3 real, 253.2 MB
[runlim] sample:		1585.3 time, 400.3 real, 249.7 MB
[runlim] sample:		1624.9 time, 410.3 real, 259.8 MB
[runlim] sample:		1664.6 time, 420.3 real, 259.6 MB
[runlim] sample:		1704.2 time, 430.3 real, 264.7 MB
[runlim] sample:		1743.8 time, 440.3 real, 266.8 MB
[runlim] sample:		1783.4 time, 450.3 real, 277.4 MB
[runlim] sample:		1823.0 time, 460.3 real, 285.7 MB
[runlim] sample:		1862.7 time, 470.3 real, 283.6 MB
[runlim] sample:		1902.3 time, 480.3 real, 289.0 MB
[runlim] sample:		1941.9 time, 490.3 real, 274.1 MB
[runlim] sample:		1981.5 time, 500.3 real, 277.4 MB
[runlim] end:			Sat Sep 19 06:17:45 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			503.67 seconds
[runlim] time:			1993.85 seconds
[runlim] space:			292.0 MB
[runlim] samples:		5033
