[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/atco_enc3_opt1_03_53.cnf.bz2
[runlim] argv[2]:		/home/biere/bin/glucose23
[runlim] start:			Fri May  8 01:45:11 2015
[runlim] main pid:		1782
[runlim] sample:		6.7 time, 11.0 real, 467.0 MB
[runlim] sample:		16.7 time, 21.0 real, 467.5 MB
[runlim] sample:		26.6 time, 31.0 real, 467.5 MB
[runlim] sample:		36.6 time, 41.0 real, 467.5 MB
[runlim] sample:		46.6 time, 51.0 real, 469.5 MB
[runlim] sample:		56.6 time, 61.0 real, 469.5 MB
[runlim] sample:		66.6 time, 71.0 real, 469.5 MB
[runlim] sample:		76.6 time, 81.0 real, 469.5 MB
[runlim] sample:		86.6 time, 91.0 real, 469.5 MB
[runlim] sample:		96.5 time, 101.0 real, 469.5 MB
[runlim] sample:		106.5 time, 111.0 real, 469.5 MB
[runlim] sample:		116.5 time, 121.0 real, 471.7 MB
[runlim] sample:		126.5 time, 131.0 real, 472.0 MB
[runlim] sample:		136.5 time, 141.0 real, 472.2 MB
[runlim] sample:		146.4 time, 151.0 real, 473.3 MB
[runlim] sample:		156.4 time, 161.0 real, 473.3 MB
[runlim] sample:		166.4 time, 171.0 real, 473.3 MB
[runlim] sample:		176.4 time, 181.0 real, 473.5 MB
[runlim] sample:		186.4 time, 191.0 real, 473.5 MB
[runlim] sample:		196.4 time, 201.0 real, 475.5 MB
[runlim] sample:		206.3 time, 211.0 real, 475.5 MB
[runlim] sample:		216.3 time, 221.0 real, 475.5 MB
[runlim] sample:		226.3 time, 231.0 real, 475.5 MB
[runlim] sample:		236.3 time, 241.0 real, 475.5 MB
[runlim] sample:		246.3 time, 251.0 real, 475.5 MB
[runlim] sample:		256.3 time, 261.0 real, 475.5 MB
[runlim] sample:		266.3 time, 271.0 real, 475.5 MB
[runlim] sample:		276.2 time, 281.0 real, 477.5 MB
[runlim] sample:		286.2 time, 291.0 real, 477.5 MB
[runlim] sample:		296.2 time, 301.0 real, 477.5 MB
[runlim] sample:		306.2 time, 311.0 real, 477.5 MB
[runlim] sample:		316.2 time, 321.0 real, 477.5 MB
[runlim] sample:		326.2 time, 331.0 real, 477.5 MB
[runlim] sample:		336.1 time, 341.0 real, 477.5 MB
[runlim] sample:		346.1 time, 351.0 real, 477.5 MB
[runlim] sample:		356.1 time, 361.0 real, 479.5 MB
[runlim] sample:		366.1 time, 371.0 real, 479.5 MB
[runlim] sample:		376.1 time, 381.0 real, 479.5 MB
[runlim] sample:		386.1 time, 391.0 real, 479.5 MB
[runlim] sample:		396.1 time, 401.0 real, 479.5 MB
[runlim] sample:		406.0 time, 411.0 real, 479.5 MB
[runlim] sample:		416.0 time, 421.0 real, 479.5 MB
[runlim] sample:		426.0 time, 431.0 real, 481.5 MB
[runlim] sample:		436.0 time, 441.0 real, 481.5 MB
[runlim] sample:		446.0 time, 451.0 real, 481.5 MB
[runlim] sample:		456.0 time, 461.0 real, 481.5 MB
[runlim] sample:		465.9 time, 471.0 real, 481.5 MB
[runlim] sample:		475.9 time, 481.0 real, 481.5 MB
[runlim] sample:		485.9 time, 491.0 real, 481.5 MB
[runlim] sample:		495.9 time, 501.0 real, 483.5 MB
[runlim] sample:		505.9 time, 511.0 real, 483.5 MB
[runlim] sample:		515.9 time, 521.0 real, 483.5 MB
[runlim] sample:		525.9 time, 531.0 real, 483.5 MB
[runlim] sample:		535.8 time, 541.0 real, 483.5 MB
[runlim] sample:		545.8 time, 551.0 real, 483.5 MB
[runlim] sample:		555.8 time, 561.0 real, 483.5 MB
[runlim] sample:		565.8 time, 571.0 real, 485.5 MB
[runlim] sample:		575.8 time, 581.0 real, 485.5 MB
[runlim] sample:		585.8 time, 591.0 real, 485.5 MB
[runlim] sample:		595.8 time, 601.0 real, 485.5 MB
[runlim] sample:		605.7 time, 611.0 real, 485.5 MB
[runlim] sample:		615.7 time, 621.0 real, 485.5 MB
[runlim] sample:		625.7 time, 631.0 real, 485.5 MB
[runlim] sample:		635.7 time, 641.0 real, 487.5 MB
[runlim] sample:		645.7 time, 651.0 real, 487.5 MB
[runlim] sample:		655.7 time, 661.0 real, 487.5 MB
[runlim] sample:		665.6 time, 671.0 real, 487.5 MB
[runlim] sample:		675.6 time, 681.0 real, 487.5 MB
[runlim] sample:		685.6 time, 691.0 real, 487.5 MB
[runlim] sample:		695.6 time, 701.0 real, 487.5 MB
[runlim] sample:		705.6 time, 711.0 real, 489.5 MB
[runlim] sample:		715.6 time, 721.0 real, 489.5 MB
[runlim] sample:		724.6 time, 731.0 real, 0.0 MB
[runlim] end:			Fri May  8 01:57:22 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		27
[runlim] real:			731.10 seconds
[runlim] time:			724.65 seconds
[runlim] space:			557.4 MB
[runlim] samples:		7301
