[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]:		--score=5
[runlim] argv[2]:		-v
[runlim] argv[3]:		-n
[runlim] argv[4]:		/data/cnf/sc2014/app/14pipe_q0_k.cnf.bz2
[runlim] start:			Sun Apr 26 22:10:48 2015
[runlim] main pid:		2014
[runlim] sample:		7.4 time, 10.3 real, 298.1 MB
[runlim] sample:		17.4 time, 20.3 real, 254.6 MB
[runlim] sample:		27.4 time, 30.3 real, 169.4 MB
[runlim] sample:		37.4 time, 40.3 real, 300.1 MB
[runlim] sample:		47.4 time, 50.3 real, 266.4 MB
[runlim] sample:		57.4 time, 60.3 real, 266.4 MB
[runlim] sample:		67.3 time, 70.3 real, 295.5 MB
[runlim] sample:		77.3 time, 80.3 real, 308.2 MB
[runlim] sample:		87.3 time, 90.3 real, 266.6 MB
[runlim] sample:		97.3 time, 100.3 real, 273.9 MB
[runlim] sample:		107.3 time, 110.3 real, 273.9 MB
[runlim] sample:		117.3 time, 120.3 real, 323.6 MB
[runlim] sample:		127.2 time, 130.3 real, 263.5 MB
[runlim] sample:		137.2 time, 140.3 real, 258.4 MB
[runlim] sample:		147.2 time, 150.3 real, 253.3 MB
[runlim] sample:		157.2 time, 160.3 real, 253.3 MB
[runlim] sample:		167.2 time, 170.3 real, 266.1 MB
[runlim] sample:		177.2 time, 180.3 real, 253.9 MB
[runlim] sample:		187.1 time, 190.3 real, 253.9 MB
[runlim] sample:		197.1 time, 200.3 real, 254.9 MB
[runlim] sample:		207.1 time, 210.3 real, 254.6 MB
[runlim] sample:		217.1 time, 220.3 real, 299.2 MB
[runlim] sample:		227.1 time, 230.3 real, 363.8 MB
[runlim] sample:		237.1 time, 240.3 real, 253.1 MB
[runlim] sample:		247.1 time, 250.3 real, 275.3 MB
[runlim] sample:		257.1 time, 260.3 real, 261.2 MB
[runlim] sample:		267.1 time, 270.3 real, 260.3 MB
[runlim] sample:		277.0 time, 280.3 real, 260.3 MB
[runlim] sample:		287.0 time, 290.3 real, 260.3 MB
[runlim] sample:		297.0 time, 300.3 real, 262.3 MB
[runlim] sample:		307.0 time, 310.3 real, 263.4 MB
[runlim] sample:		317.0 time, 320.3 real, 263.4 MB
[runlim] sample:		327.0 time, 330.3 real, 263.4 MB
[runlim] sample:		337.0 time, 340.3 real, 263.4 MB
[runlim] sample:		346.9 time, 350.3 real, 335.6 MB
[runlim] sample:		356.9 time, 360.3 real, 266.0 MB
[runlim] sample:		366.9 time, 370.3 real, 266.0 MB
[runlim] sample:		376.9 time, 380.3 real, 266.0 MB
[runlim] sample:		386.9 time, 390.3 real, 266.0 MB
[runlim] sample:		396.9 time, 400.3 real, 266.0 MB
[runlim] sample:		406.9 time, 410.3 real, 266.0 MB
[runlim] sample:		416.9 time, 420.3 real, 193.1 MB
[runlim] sample:		426.9 time, 430.3 real, 280.1 MB
[runlim] sample:		436.8 time, 440.3 real, 265.6 MB
[runlim] sample:		446.8 time, 450.3 real, 265.6 MB
[runlim] sample:		456.8 time, 460.3 real, 265.6 MB
[runlim] sample:		466.8 time, 470.3 real, 265.6 MB
[runlim] sample:		476.8 time, 480.3 real, 265.6 MB
[runlim] sample:		486.8 time, 490.3 real, 265.6 MB
[runlim] sample:		496.8 time, 500.3 real, 266.8 MB
[runlim] sample:		506.8 time, 510.3 real, 266.2 MB
[runlim] sample:		516.7 time, 520.3 real, 266.2 MB
[runlim] sample:		526.7 time, 530.3 real, 266.2 MB
[runlim] sample:		536.7 time, 540.3 real, 266.2 MB
[runlim] sample:		546.7 time, 550.3 real, 266.2 MB
[runlim] sample:		556.7 time, 560.3 real, 266.2 MB
[runlim] sample:		566.7 time, 570.3 real, 266.2 MB
[runlim] sample:		576.6 time, 580.3 real, 310.7 MB
[runlim] sample:		586.6 time, 590.3 real, 265.7 MB
[runlim] sample:		596.6 time, 600.3 real, 265.7 MB
[runlim] sample:		606.6 time, 610.3 real, 265.7 MB
[runlim] sample:		616.6 time, 620.3 real, 265.7 MB
[runlim] sample:		626.6 time, 630.3 real, 265.7 MB
[runlim] sample:		636.6 time, 640.3 real, 265.7 MB
[runlim] sample:		646.6 time, 650.3 real, 265.7 MB
[runlim] sample:		656.5 time, 660.3 real, 265.7 MB
[runlim] sample:		666.5 time, 670.3 real, 265.7 MB
[runlim] sample:		676.5 time, 680.3 real, 265.7 MB
[runlim] sample:		686.5 time, 690.3 real, 265.7 MB
[runlim] sample:		696.5 time, 700.3 real, 265.7 MB
[runlim] sample:		706.5 time, 710.3 real, 276.1 MB
[runlim] sample:		716.5 time, 720.3 real, 261.0 MB
[runlim] sample:		726.5 time, 730.3 real, 261.0 MB
[runlim] sample:		736.4 time, 740.3 real, 261.0 MB
[runlim] sample:		746.4 time, 750.3 real, 261.0 MB
[runlim] sample:		756.4 time, 760.3 real, 261.0 MB
[runlim] sample:		766.4 time, 770.3 real, 261.0 MB
[runlim] sample:		776.4 time, 780.3 real, 261.0 MB
[runlim] sample:		786.4 time, 790.3 real, 260.9 MB
[runlim] sample:		796.3 time, 800.3 real, 260.9 MB
[runlim] end:			Sun Apr 26 22:24:10 2015
[runlim] status:		ok
[runlim] result:		20
[runlim] children:		139
[runlim] real:			802.73 seconds
[runlim] time:			798.63 seconds
[runlim] space:			487.4 MB
[runlim] samples:		8024
