[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.035-NOTKNOWN.cnf.bz2
[runlim] argv[2]:		/home/biere/bin/glucose23
[runlim] start:			Fri May  8 01:22:59 2015
[runlim] main pid:		29482
[runlim] sample:		8.5 time, 10.8 real, 133.5 MB
[runlim] sample:		18.5 time, 20.8 real, 137.9 MB
[runlim] sample:		28.5 time, 30.8 real, 147.9 MB
[runlim] sample:		38.5 time, 40.8 real, 139.7 MB
[runlim] sample:		48.5 time, 50.8 real, 148.9 MB
[runlim] sample:		58.5 time, 60.8 real, 158.6 MB
[runlim] sample:		68.5 time, 70.8 real, 164.6 MB
[runlim] sample:		78.4 time, 80.8 real, 182.4 MB
[runlim] sample:		88.4 time, 90.8 real, 149.1 MB
[runlim] sample:		98.4 time, 100.8 real, 166.9 MB
[runlim] sample:		108.4 time, 110.8 real, 179.1 MB
[runlim] sample:		118.4 time, 120.8 real, 192.9 MB
[runlim] sample:		128.4 time, 130.8 real, 225.1 MB
[runlim] sample:		138.4 time, 140.8 real, 165.8 MB
[runlim] sample:		148.3 time, 150.8 real, 191.8 MB
[runlim] sample:		158.3 time, 160.8 real, 205.8 MB
[runlim] sample:		168.3 time, 170.8 real, 222.0 MB
[runlim] sample:		178.3 time, 180.8 real, 237.7 MB
[runlim] sample:		188.3 time, 190.8 real, 252.0 MB
[runlim] sample:		198.3 time, 200.8 real, 272.0 MB
[runlim] sample:		208.3 time, 210.8 real, 286.0 MB
[runlim] sample:		218.3 time, 220.8 real, 169.1 MB
[runlim] sample:		228.3 time, 230.8 real, 179.1 MB
[runlim] sample:		238.3 time, 240.8 real, 194.9 MB
[runlim] sample:		248.2 time, 250.8 real, 209.1 MB
[runlim] sample:		258.2 time, 260.8 real, 219.1 MB
[runlim] sample:		268.2 time, 270.8 real, 237.1 MB
[runlim] sample:		278.2 time, 280.8 real, 245.1 MB
[runlim] sample:		288.2 time, 290.8 real, 261.1 MB
[runlim] sample:		298.2 time, 300.8 real, 275.1 MB
[runlim] sample:		308.2 time, 310.8 real, 289.1 MB
[runlim] end:			Fri May  8 01:28:13 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		13
[runlim] real:			314.51 seconds
[runlim] time:			311.78 seconds
[runlim] space:			343.4 MB
[runlim] samples:		3136
