[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/atco_enc2_opt1_20_11.cnf.bz2
[runlim] start:			Fri May  1 14:22:05 2015
[runlim] main pid:		952
[runlim] sample:		12.0 time, 10.0 real, 372.8 MB
[runlim] sample:		16.6 time, 20.0 real, 557.6 MB
[runlim] sample:		26.6 time, 30.0 real, 412.3 MB
[runlim] sample:		36.6 time, 40.0 real, 539.4 MB
[runlim] sample:		46.6 time, 50.0 real, 410.5 MB
[runlim] sample:		56.6 time, 60.0 real, 644.4 MB
[runlim] sample:		66.5 time, 70.0 real, 644.9 MB
[runlim] sample:		76.5 time, 80.0 real, 641.8 MB
[runlim] sample:		86.5 time, 90.0 real, 626.9 MB
[runlim] sample:		96.5 time, 100.0 real, 590.0 MB
[runlim] sample:		106.5 time, 110.0 real, 668.5 MB
[runlim] sample:		116.5 time, 120.0 real, 276.0 MB
[runlim] sample:		126.5 time, 130.0 real, 280.3 MB
[runlim] sample:		136.4 time, 140.0 real, 479.0 MB
[runlim] sample:		146.4 time, 150.0 real, 464.5 MB
[runlim] sample:		156.4 time, 160.0 real, 465.4 MB
[runlim] sample:		166.4 time, 170.0 real, 607.0 MB
[runlim] sample:		176.4 time, 180.0 real, 326.2 MB
[runlim] sample:		186.4 time, 190.0 real, 466.3 MB
[runlim] sample:		196.4 time, 200.0 real, 466.3 MB
[runlim] sample:		206.3 time, 210.0 real, 466.3 MB
[runlim] sample:		216.3 time, 220.0 real, 466.3 MB
[runlim] sample:		226.3 time, 230.0 real, 465.5 MB
[runlim] sample:		236.3 time, 240.0 real, 465.3 MB
[runlim] sample:		246.3 time, 250.0 real, 466.2 MB
[runlim] sample:		256.3 time, 260.0 real, 466.2 MB
[runlim] sample:		266.3 time, 270.0 real, 466.2 MB
[runlim] sample:		276.2 time, 280.0 real, 466.2 MB
[runlim] sample:		286.2 time, 290.0 real, 466.2 MB
[runlim] sample:		296.2 time, 300.0 real, 466.2 MB
[runlim] sample:		306.2 time, 310.0 real, 282.1 MB
[runlim] sample:		316.2 time, 320.0 real, 467.2 MB
[runlim] sample:		326.2 time, 330.0 real, 467.2 MB
[runlim] sample:		336.2 time, 340.0 real, 467.2 MB
[runlim] sample:		346.2 time, 350.0 real, 467.2 MB
[runlim] sample:		356.1 time, 360.0 real, 467.2 MB
[runlim] sample:		366.1 time, 370.0 real, 467.2 MB
[runlim] sample:		376.1 time, 380.0 real, 467.2 MB
[runlim] sample:		386.1 time, 390.0 real, 467.2 MB
[runlim] sample:		396.1 time, 400.0 real, 467.2 MB
[runlim] sample:		406.1 time, 410.0 real, 467.2 MB
[runlim] sample:		416.1 time, 420.0 real, 467.2 MB
[runlim] sample:		426.1 time, 430.0 real, 282.2 MB
[runlim] sample:		436.0 time, 440.0 real, 282.2 MB
[runlim] sample:		446.0 time, 450.0 real, 467.3 MB
[runlim] sample:		456.0 time, 460.0 real, 467.3 MB
[runlim] sample:		466.0 time, 470.0 real, 467.3 MB
[runlim] sample:		476.0 time, 480.0 real, 467.3 MB
[runlim] sample:		486.0 time, 490.0 real, 467.3 MB
[runlim] sample:		495.9 time, 500.0 real, 467.3 MB
[runlim] sample:		505.9 time, 510.0 real, 467.3 MB
[runlim] sample:		515.9 time, 520.0 real, 467.3 MB
[runlim] sample:		525.9 time, 530.0 real, 467.3 MB
[runlim] sample:		535.9 time, 540.0 real, 467.3 MB
[runlim] sample:		545.9 time, 550.0 real, 467.3 MB
[runlim] sample:		555.9 time, 560.0 real, 467.3 MB
[runlim] sample:		565.9 time, 570.0 real, 467.3 MB
[runlim] sample:		575.8 time, 580.0 real, 467.3 MB
[runlim] sample:		585.8 time, 590.0 real, 467.3 MB
[runlim] sample:		595.8 time, 600.0 real, 467.3 MB
[runlim] sample:		605.8 time, 610.0 real, 467.3 MB
[runlim] sample:		615.8 time, 620.0 real, 467.3 MB
[runlim] sample:		625.8 time, 630.0 real, 467.3 MB
[runlim] sample:		635.8 time, 640.0 real, 467.3 MB
[runlim] sample:		645.7 time, 650.0 real, 467.0 MB
[runlim] sample:		655.7 time, 660.0 real, 684.5 MB
[runlim] sample:		665.7 time, 670.0 real, 367.0 MB
[runlim] sample:		675.7 time, 680.0 real, 467.9 MB
[runlim] sample:		685.7 time, 690.0 real, 467.9 MB
[runlim] sample:		695.7 time, 700.0 real, 467.9 MB
[runlim] sample:		705.7 time, 710.0 real, 467.9 MB
[runlim] sample:		715.6 time, 720.0 real, 467.1 MB
[runlim] sample:		725.6 time, 730.0 real, 467.9 MB
[runlim] sample:		735.6 time, 740.0 real, 467.9 MB
[runlim] sample:		745.6 time, 750.0 real, 467.9 MB
[runlim] sample:		755.6 time, 760.0 real, 467.9 MB
[runlim] sample:		765.6 time, 770.0 real, 467.9 MB
[runlim] sample:		775.6 time, 780.0 real, 467.9 MB
[runlim] sample:		785.5 time, 790.0 real, 467.9 MB
[runlim] sample:		795.5 time, 800.0 real, 467.9 MB
[runlim] sample:		805.5 time, 810.0 real, 467.9 MB
[runlim] sample:		815.5 time, 820.0 real, 467.9 MB
[runlim] sample:		825.5 time, 830.0 real, 467.9 MB
[runlim] sample:		835.5 time, 840.0 real, 467.9 MB
[runlim] sample:		845.5 time, 850.0 real, 467.9 MB
[runlim] sample:		855.5 time, 860.0 real, 467.9 MB
[runlim] sample:		865.4 time, 870.0 real, 467.9 MB
[runlim] sample:		875.4 time, 880.0 real, 467.9 MB
[runlim] sample:		885.4 time, 890.0 real, 467.9 MB
[runlim] sample:		895.4 time, 900.0 real, 467.9 MB
[runlim] sample:		905.4 time, 910.0 real, 467.9 MB
[runlim] sample:		915.4 time, 920.0 real, 467.9 MB
[runlim] sample:		925.4 time, 930.0 real, 467.9 MB
[runlim] sample:		935.4 time, 940.0 real, 467.9 MB
[runlim] sample:		945.3 time, 950.0 real, 467.9 MB
[runlim] sample:		955.3 time, 960.0 real, 467.9 MB
[runlim] sample:		965.3 time, 970.0 real, 467.9 MB
[runlim] end:			Fri May  1 14:38:21 2015
[runlim] status:		ok
[runlim] result:		20
[runlim] children:		228
[runlim] real:			976.14 seconds
[runlim] time:			971.33 seconds
[runlim] space:			1038.8 MB
[runlim] samples:		9761
