[runlim] version:		1.9
[runlim] time limit:		1000 seconds
[runlim] real time limit:	311040000 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/bin/bunzip2-and-then
[runlim] argv[1]:		/data/cnf/sc2014/app/grid-strips-grid-y-3.065-SAT.cnf.bz2
[runlim] argv[2]:		/home/biere/bin/glucose23
[runlim] start:			Fri May  8 01:37:43 2015
[runlim] main pid:		596
[runlim] sample:		7.7 time, 10.8 real, 297.7 MB
[runlim] sample:		17.7 time, 20.8 real, 264.7 MB
[runlim] sample:		27.7 time, 30.8 real, 274.7 MB
[runlim] sample:		37.7 time, 40.8 real, 286.7 MB
[runlim] sample:		47.7 time, 50.8 real, 263.6 MB
[runlim] sample:		57.6 time, 60.8 real, 277.6 MB
[runlim] sample:		67.6 time, 70.8 real, 291.4 MB
[runlim] sample:		77.6 time, 80.8 real, 307.6 MB
[runlim] sample:		87.6 time, 90.8 real, 282.2 MB
[runlim] sample:		97.6 time, 100.8 real, 301.1 MB
[runlim] sample:		107.6 time, 110.8 real, 319.4 MB
[runlim] sample:		117.6 time, 120.8 real, 334.3 MB
[runlim] sample:		127.6 time, 130.8 real, 347.6 MB
[runlim] sample:		137.6 time, 140.8 real, 276.8 MB
[runlim] sample:		147.5 time, 150.8 real, 281.5 MB
[runlim] sample:		157.5 time, 160.8 real, 290.5 MB
[runlim] sample:		167.5 time, 170.8 real, 296.5 MB
[runlim] sample:		177.5 time, 180.8 real, 308.8 MB
[runlim] sample:		187.5 time, 190.8 real, 322.8 MB
[runlim] sample:		197.5 time, 200.8 real, 336.5 MB
[runlim] sample:		207.5 time, 210.8 real, 356.8 MB
[runlim] sample:		217.5 time, 220.8 real, 368.8 MB
[runlim] sample:		227.5 time, 230.8 real, 285.9 MB
[runlim] sample:		237.5 time, 240.8 real, 295.9 MB
[runlim] sample:		247.4 time, 250.8 real, 307.9 MB
[runlim] sample:		257.4 time, 260.8 real, 326.1 MB
[runlim] sample:		267.4 time, 270.8 real, 341.9 MB
[runlim] end:			Fri May  8 01:42:18 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		21
[runlim] real:			275.52 seconds
[runlim] time:			271.73 seconds
[runlim] space:			424.8 MB
[runlim] samples:		2747
