[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/nuxmv/single.nuxmv
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/intel035.aig
[runlim] start:			Sun Sep 20 20:43:06 2015
[runlim] main pid:		14742
[runlim] sample:		36.3 time, 10.5 real, 912.6 MB
[runlim] sample:		75.9 time, 20.5 real, 1200.9 MB
[runlim] sample:		115.5 time, 30.5 real, 1337.0 MB
[runlim] sample:		155.1 time, 40.5 real, 1644.0 MB
[runlim] sample:		194.8 time, 50.5 real, 1716.6 MB
[runlim] sample:		234.3 time, 60.5 real, 1720.9 MB
[runlim] sample:		273.9 time, 70.5 real, 1736.3 MB
[runlim] sample:		313.5 time, 80.5 real, 1722.3 MB
[runlim] sample:		353.1 time, 90.5 real, 1771.2 MB
[runlim] sample:		392.6 time, 100.5 real, 1824.4 MB
[runlim] sample:		432.2 time, 110.5 real, 1844.0 MB
[runlim] sample:		471.8 time, 120.5 real, 1898.2 MB
[runlim] sample:		511.4 time, 130.5 real, 1920.9 MB
[runlim] sample:		551.0 time, 140.5 real, 1841.3 MB
[runlim] sample:		590.6 time, 150.5 real, 1841.8 MB
[runlim] sample:		630.2 time, 160.5 real, 1842.3 MB
[runlim] sample:		669.8 time, 170.5 real, 1844.8 MB
[runlim] sample:		709.4 time, 180.5 real, 1844.8 MB
[runlim] sample:		749.0 time, 190.5 real, 1844.8 MB
[runlim] sample:		788.6 time, 200.5 real, 1845.0 MB
[runlim] sample:		828.2 time, 210.5 real, 1847.0 MB
[runlim] sample:		867.9 time, 220.5 real, 1847.0 MB
[runlim] sample:		907.5 time, 230.5 real, 1847.0 MB
[runlim] sample:		947.1 time, 240.5 real, 1847.0 MB
[runlim] sample:		986.7 time, 250.5 real, 1852.5 MB
[runlim] sample:		1026.3 time, 260.5 real, 1854.5 MB
[runlim] sample:		1065.9 time, 270.5 real, 1857.3 MB
[runlim] sample:		1105.5 time, 280.5 real, 1855.6 MB
[runlim] sample:		1145.1 time, 290.5 real, 1857.4 MB
[runlim] sample:		1184.7 time, 300.5 real, 1860.4 MB
[runlim] sample:		1224.3 time, 310.5 real, 1862.4 MB
[runlim] sample:		1263.9 time, 320.5 real, 1880.4 MB
[runlim] sample:		1303.5 time, 330.5 real, 1945.1 MB
[runlim] sample:		1343.1 time, 340.5 real, 1945.8 MB
[runlim] sample:		1382.7 time, 350.5 real, 1953.2 MB
[runlim] sample:		1422.3 time, 360.5 real, 1870.9 MB
[runlim] sample:		1462.0 time, 370.5 real, 1870.9 MB
[runlim] sample:		1501.6 time, 380.5 real, 1870.9 MB
[runlim] sample:		1541.2 time, 390.5 real, 1870.9 MB
[runlim] sample:		1580.8 time, 400.5 real, 1870.9 MB
[runlim] sample:		1620.4 time, 410.5 real, 1870.9 MB
[runlim] sample:		1660.1 time, 420.5 real, 1870.9 MB
[runlim] sample:		1699.7 time, 430.5 real, 1870.9 MB
[runlim] sample:		1739.2 time, 440.5 real, 1871.2 MB
[runlim] end:			Sun Sep 20 20:50:33 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		17831
[runlim] real:			447.29 seconds
[runlim] time:			1764.26 seconds
[runlim] space:			1955.4 MB
[runlim] samples:		4468
