[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/beemandrsn4b1.aig
[runlim] start:			Sat Sep 19 06:38:58 2015
[runlim] main pid:		5013
[runlim] sample:		39.0 time, 10.4 real, 120.9 MB
[runlim] sample:		78.6 time, 20.4 real, 120.3 MB
[runlim] sample:		118.3 time, 30.4 real, 128.9 MB
[runlim] sample:		157.9 time, 40.4 real, 145.4 MB
[runlim] sample:		197.6 time, 50.4 real, 148.5 MB
[runlim] sample:		237.2 time, 60.4 real, 150.5 MB
[runlim] sample:		276.8 time, 70.4 real, 150.0 MB
[runlim] sample:		316.4 time, 80.4 real, 151.0 MB
[runlim] sample:		356.0 time, 90.4 real, 151.0 MB
[runlim] sample:		395.7 time, 100.4 real, 158.3 MB
[runlim] sample:		435.3 time, 110.4 real, 158.3 MB
[runlim] sample:		474.9 time, 120.4 real, 158.8 MB
[runlim] sample:		514.5 time, 130.4 real, 152.2 MB
[runlim] sample:		554.1 time, 140.4 real, 159.0 MB
[runlim] sample:		593.8 time, 150.4 real, 159.5 MB
[runlim] sample:		633.4 time, 160.4 real, 166.8 MB
[runlim] sample:		673.0 time, 170.4 real, 169.1 MB
[runlim] sample:		712.6 time, 180.4 real, 169.6 MB
[runlim] sample:		752.2 time, 190.4 real, 169.9 MB
[runlim] sample:		791.8 time, 200.4 real, 169.9 MB
[runlim] sample:		831.5 time, 210.4 real, 167.5 MB
[runlim] sample:		871.0 time, 220.4 real, 171.1 MB
[runlim] sample:		902.9 time, 230.4 real, 172.2 MB
[runlim] sample:		933.6 time, 240.4 real, 164.9 MB
[runlim] sample:		963.8 time, 250.4 real, 187.1 MB
[runlim] sample:		1001.7 time, 260.4 real, 194.6 MB
[runlim] sample:		1041.4 time, 270.4 real, 198.9 MB
[runlim] sample:		1081.1 time, 280.4 real, 197.4 MB
[runlim] sample:		1120.7 time, 290.4 real, 201.2 MB
[runlim] sample:		1160.4 time, 300.4 real, 198.8 MB
[runlim] sample:		1200.0 time, 310.4 real, 199.1 MB
[runlim] sample:		1239.7 time, 320.4 real, 199.4 MB
[runlim] sample:		1279.3 time, 330.4 real, 199.4 MB
[runlim] sample:		1319.0 time, 340.4 real, 192.3 MB
[runlim] sample:		1358.6 time, 350.4 real, 193.9 MB
[runlim] sample:		1398.2 time, 360.4 real, 193.9 MB
[runlim] sample:		1437.9 time, 370.4 real, 194.6 MB
[runlim] sample:		1477.5 time, 380.4 real, 197.2 MB
[runlim] sample:		1517.2 time, 390.4 real, 198.2 MB
[runlim] sample:		1556.8 time, 400.4 real, 199.0 MB
[runlim] sample:		1596.5 time, 410.4 real, 201.2 MB
[runlim] sample:		1636.1 time, 420.4 real, 201.7 MB
[runlim] sample:		1675.8 time, 430.4 real, 203.3 MB
[runlim] sample:		1715.4 time, 440.4 real, 205.7 MB
[runlim] sample:		1755.0 time, 450.4 real, 207.1 MB
[runlim] sample:		1794.7 time, 460.4 real, 210.8 MB
[runlim] sample:		1834.3 time, 470.4 real, 210.8 MB
[runlim] sample:		1873.9 time, 480.4 real, 211.1 MB
[runlim] sample:		1913.5 time, 490.4 real, 211.4 MB
[runlim] sample:		1953.2 time, 500.4 real, 203.1 MB
[runlim] sample:		1992.8 time, 510.4 real, 203.4 MB
[runlim] sample:		2032.4 time, 520.4 real, 197.9 MB
[runlim] sample:		2072.1 time, 530.4 real, 197.9 MB
[runlim] sample:		2111.8 time, 540.4 real, 198.2 MB
[runlim] sample:		2151.5 time, 550.4 real, 199.4 MB
[runlim] sample:		2191.1 time, 560.4 real, 199.9 MB
[runlim] sample:		2230.7 time, 570.4 real, 200.2 MB
[runlim] sample:		2270.4 time, 580.4 real, 200.4 MB
[runlim] sample:		2310.0 time, 590.4 real, 203.0 MB
[runlim] sample:		2349.6 time, 600.4 real, 203.2 MB
[runlim] sample:		2389.2 time, 610.4 real, 203.7 MB
[runlim] sample:		2428.8 time, 620.4 real, 209.3 MB
[runlim] sample:		2468.4 time, 630.4 real, 212.6 MB
[runlim] sample:		2508.0 time, 640.4 real, 212.9 MB
[runlim] sample:		2547.7 time, 650.4 real, 215.8 MB
[runlim] sample:		2587.3 time, 660.4 real, 219.9 MB
[runlim] sample:		2627.0 time, 670.4 real, 215.9 MB
[runlim] sample:		2666.6 time, 680.4 real, 217.9 MB
[runlim] sample:		2706.2 time, 690.4 real, 209.7 MB
[runlim] sample:		2745.8 time, 700.4 real, 211.0 MB
[runlim] sample:		2785.5 time, 710.4 real, 214.0 MB
[runlim] sample:		2825.2 time, 720.4 real, 214.3 MB
[runlim] sample:		2864.8 time, 730.4 real, 214.5 MB
[runlim] sample:		2904.4 time, 740.4 real, 214.8 MB
[runlim] sample:		2944.0 time, 750.4 real, 219.1 MB
[runlim] sample:		2983.6 time, 760.4 real, 219.1 MB
[runlim] sample:		3023.3 time, 770.4 real, 219.6 MB
[runlim] sample:		3062.9 time, 780.4 real, 221.9 MB
[runlim] sample:		3102.6 time, 790.4 real, 219.7 MB
[runlim] sample:		3142.3 time, 800.4 real, 220.0 MB
[runlim] sample:		3182.0 time, 810.4 real, 220.0 MB
[runlim] sample:		3221.6 time, 820.4 real, 220.2 MB
[runlim] sample:		3261.2 time, 830.4 real, 220.5 MB
[runlim] sample:		3300.9 time, 840.4 real, 220.5 MB
[runlim] sample:		3340.4 time, 850.4 real, 220.8 MB
[runlim] sample:		3380.1 time, 860.4 real, 221.0 MB
[runlim] end:			Sat Sep 19 06:53:24 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		34656
[runlim] real:			866.96 seconds
[runlim] time:			3405.80 seconds
[runlim] space:			230.0 MB
[runlim] samples:		8666
