[runlim] version:		1.8
[runlim] time limit:		1000 seconds
[runlim] real time limit:	311040000 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/src/lingeling/lingeling
[runlim] argv[1]:		-v
[runlim] argv[2]:		-n
[runlim] argv[3]:		/data/cnf/sc2014/app/post-cbmc-zfcp-2.8-u2.cnf.bz2
[runlim] start:			Sat Oct 11 14:09:46 2014
[runlim] main pid:		16240
[runlim] sample:		11.6 time, 10.1 real, 634.9 MB
[runlim] sample:		25.1 time, 21.3 real, 1263.1 MB
[runlim] sample:		37.1 time, 31.3 real, 2007.0 MB
[runlim] sample:		27.7 time, 41.3 real, 2115.7 MB
[runlim] sample:		37.7 time, 51.3 real, 2635.4 MB
[runlim] sample:		47.7 time, 61.3 real, 2107.0 MB
[runlim] sample:		57.6 time, 71.3 real, 2112.8 MB
[runlim] sample:		67.6 time, 81.3 real, 2152.4 MB
[runlim] sample:		77.6 time, 91.3 real, 2673.9 MB
[runlim] sample:		87.6 time, 101.3 real, 2673.9 MB
[runlim] sample:		97.6 time, 111.3 real, 2101.3 MB
[runlim] sample:		107.6 time, 121.3 real, 2157.3 MB
[runlim] sample:		117.6 time, 131.3 real, 1594.5 MB
[runlim] sample:		127.5 time, 141.3 real, 2162.4 MB
[runlim] sample:		137.5 time, 151.3 real, 2162.4 MB
[runlim] sample:		147.5 time, 161.3 real, 2242.7 MB
[runlim] sample:		157.5 time, 171.3 real, 2242.7 MB
[runlim] sample:		167.5 time, 181.3 real, 2242.7 MB
[runlim] sample:		177.5 time, 191.3 real, 2370.4 MB
[runlim] sample:		187.5 time, 201.3 real, 2370.4 MB
[runlim] sample:		197.5 time, 211.3 real, 2370.4 MB
[runlim] sample:		207.4 time, 221.3 real, 2370.4 MB
[runlim] sample:		217.4 time, 231.3 real, 2370.4 MB
[runlim] sample:		227.4 time, 241.3 real, 2370.4 MB
[runlim] end:			Sat Oct 11 14:13:51 2014
[runlim] status:		ok
[runlim] result:		10
[runlim] children:		670
[runlim] real:			245.86 seconds
[runlim] time:			231.86 seconds
[runlim] space:			2793.6 MB
[runlim] samples:		2445
