[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_enc2_opt2_20_11.cnf.bz2
[runlim] argv[2]:		/home/biere/bin/glucose23
[runlim] start:			Fri May  8 01:40:43 2015
[runlim] main pid:		31249
[runlim] sample:		5.5 time, 10.7 real, 409.3 MB
[runlim] sample:		15.4 time, 20.7 real, 413.6 MB
[runlim] sample:		25.4 time, 30.7 real, 419.6 MB
[runlim] sample:		35.4 time, 40.7 real, 423.6 MB
[runlim] sample:		45.4 time, 50.7 real, 427.6 MB
[runlim] sample:		55.3 time, 60.7 real, 431.6 MB
[runlim] sample:		65.3 time, 70.7 real, 435.6 MB
[runlim] sample:		75.3 time, 80.7 real, 437.6 MB
[runlim] sample:		85.3 time, 90.7 real, 441.6 MB
[runlim] sample:		95.2 time, 100.7 real, 445.6 MB
[runlim] sample:		105.2 time, 110.7 real, 413.4 MB
[runlim] sample:		115.2 time, 120.7 real, 417.4 MB
[runlim] sample:		125.2 time, 130.7 real, 421.4 MB
[runlim] sample:		135.2 time, 140.7 real, 423.4 MB
[runlim] sample:		145.1 time, 150.7 real, 427.5 MB
[runlim] sample:		155.1 time, 160.7 real, 431.7 MB
[runlim] sample:		165.1 time, 170.7 real, 435.7 MB
[runlim] sample:		175.1 time, 180.7 real, 439.7 MB
[runlim] sample:		185.1 time, 190.7 real, 442.2 MB
[runlim] sample:		195.1 time, 200.7 real, 446.2 MB
[runlim] sample:		205.0 time, 210.7 real, 413.7 MB
[runlim] sample:		215.0 time, 220.7 real, 415.7 MB
[runlim] sample:		225.0 time, 230.7 real, 419.9 MB
[runlim] sample:		235.0 time, 240.7 real, 424.2 MB
[runlim] sample:		245.0 time, 250.7 real, 426.2 MB
[runlim] sample:		255.0 time, 260.7 real, 430.2 MB
[runlim] sample:		264.9 time, 270.7 real, 434.2 MB
[runlim] sample:		274.9 time, 280.7 real, 438.2 MB
[runlim] sample:		284.9 time, 290.7 real, 440.2 MB
[runlim] sample:		294.9 time, 300.7 real, 444.2 MB
[runlim] sample:		304.9 time, 310.7 real, 413.1 MB
[runlim] sample:		314.9 time, 320.7 real, 419.1 MB
[runlim] sample:		324.9 time, 330.7 real, 421.3 MB
[runlim] sample:		334.8 time, 340.7 real, 425.3 MB
[runlim] sample:		344.8 time, 350.7 real, 429.8 MB
[runlim] end:			Fri May  8 01:46:41 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		31
[runlim] real:			358.62 seconds
[runlim] time:			352.61 seconds
[runlim] space:			582.3 MB
[runlim] samples:		3578
