[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/eijks1423.aig
[runlim] start:			Fri Sep 18 22:55:18 2015
[runlim] main pid:		11538
[runlim] sample:		38.9 time, 10.4 real, 90.1 MB
[runlim] sample:		78.5 time, 20.4 real, 95.7 MB
[runlim] sample:		118.0 time, 30.4 real, 101.8 MB
[runlim] sample:		157.6 time, 40.4 real, 111.8 MB
[runlim] sample:		197.1 time, 50.4 real, 119.9 MB
[runlim] sample:		236.7 time, 60.4 real, 122.1 MB
[runlim] sample:		276.4 time, 70.4 real, 122.4 MB
[runlim] sample:		315.9 time, 80.4 real, 122.8 MB
[runlim] sample:		355.5 time, 90.4 real, 122.8 MB
[runlim] sample:		395.2 time, 100.4 real, 118.7 MB
[runlim] sample:		434.9 time, 110.4 real, 124.8 MB
[runlim] sample:		474.5 time, 120.4 real, 125.6 MB
[runlim] sample:		514.2 time, 130.4 real, 125.8 MB
[runlim] sample:		553.8 time, 140.4 real, 126.1 MB
[runlim] sample:		593.3 time, 150.4 real, 130.1 MB
[runlim] sample:		632.9 time, 160.4 real, 132.7 MB
[runlim] sample:		672.6 time, 170.4 real, 134.5 MB
[runlim] sample:		712.2 time, 180.4 real, 135.5 MB
[runlim] sample:		751.9 time, 190.4 real, 135.7 MB
[runlim] sample:		791.5 time, 200.4 real, 136.1 MB
[runlim] sample:		831.2 time, 210.4 real, 136.6 MB
[runlim] sample:		870.8 time, 220.4 real, 141.2 MB
[runlim] sample:		910.4 time, 230.4 real, 139.7 MB
[runlim] sample:		950.0 time, 240.4 real, 136.8 MB
[runlim] sample:		989.6 time, 250.4 real, 143.9 MB
[runlim] sample:		1029.1 time, 260.4 real, 142.5 MB
[runlim] sample:		1068.7 time, 270.4 real, 143.3 MB
[runlim] sample:		1108.3 time, 280.4 real, 145.5 MB
[runlim] sample:		1147.9 time, 290.4 real, 147.5 MB
[runlim] sample:		1187.4 time, 300.4 real, 149.6 MB
[runlim] sample:		1226.9 time, 310.4 real, 151.1 MB
[runlim] sample:		1266.5 time, 320.4 real, 151.6 MB
[runlim] sample:		1306.1 time, 330.4 real, 146.6 MB
[runlim] sample:		1345.8 time, 340.4 real, 151.7 MB
[runlim] sample:		1385.4 time, 350.4 real, 152.0 MB
[runlim] sample:		1425.1 time, 360.4 real, 152.3 MB
[runlim] sample:		1464.7 time, 370.4 real, 152.5 MB
[runlim] sample:		1504.4 time, 380.4 real, 153.0 MB
[runlim] sample:		1544.0 time, 390.4 real, 153.1 MB
[runlim] sample:		1583.7 time, 400.4 real, 153.6 MB
[runlim] sample:		1623.3 time, 410.4 real, 156.6 MB
[runlim] end:			Fri Sep 18 23:02:18 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		16781
[runlim] real:			420.01 seconds
[runlim] time:			1661.22 seconds
[runlim] space:			161.6 MB
[runlim] samples:		4196
