[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/transport-transport-city-sequential-25nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.040-NOTKNOWN.cnf.bz2
[runlim] start:			Fri May  1 14:00:37 2015
[runlim] main pid:		15112
[runlim] sample:		8.1 time, 10.3 real, 135.2 MB
[runlim] sample:		18.1 time, 20.3 real, 143.6 MB
[runlim] sample:		28.0 time, 30.3 real, 141.7 MB
[runlim] sample:		38.0 time, 40.3 real, 139.3 MB
[runlim] sample:		48.0 time, 50.3 real, 155.7 MB
[runlim] sample:		58.0 time, 60.3 real, 156.5 MB
[runlim] sample:		68.0 time, 70.3 real, 156.5 MB
[runlim] sample:		78.0 time, 80.3 real, 189.7 MB
[runlim] sample:		88.0 time, 90.3 real, 210.4 MB
[runlim] sample:		98.0 time, 100.3 real, 223.2 MB
[runlim] sample:		107.9 time, 110.3 real, 222.6 MB
[runlim] sample:		117.9 time, 120.3 real, 222.6 MB
[runlim] sample:		127.9 time, 130.3 real, 220.3 MB
[runlim] sample:		137.9 time, 140.3 real, 220.6 MB
[runlim] sample:		147.9 time, 150.3 real, 220.1 MB
[runlim] sample:		157.9 time, 160.3 real, 220.3 MB
[runlim] sample:		167.8 time, 170.3 real, 235.2 MB
[runlim] sample:		177.8 time, 180.3 real, 259.7 MB
[runlim] sample:		187.8 time, 190.3 real, 238.2 MB
[runlim] sample:		197.8 time, 200.3 real, 309.5 MB
[runlim] sample:		207.8 time, 210.3 real, 308.8 MB
[runlim] sample:		217.8 time, 220.3 real, 309.3 MB
[runlim] sample:		227.8 time, 230.3 real, 351.2 MB
[runlim] sample:		237.8 time, 240.3 real, 349.8 MB
[runlim] sample:		247.8 time, 250.3 real, 350.5 MB
[runlim] sample:		257.7 time, 260.3 real, 350.5 MB
[runlim] sample:		267.7 time, 270.3 real, 350.4 MB
[runlim] sample:		277.7 time, 280.3 real, 363.2 MB
[runlim] sample:		287.7 time, 290.3 real, 393.3 MB
[runlim] sample:		297.7 time, 300.3 real, 393.2 MB
[runlim] sample:		307.7 time, 310.3 real, 393.3 MB
[runlim] sample:		317.6 time, 320.3 real, 393.3 MB
[runlim] sample:		327.6 time, 330.3 real, 393.6 MB
[runlim] sample:		337.6 time, 340.3 real, 395.4 MB
[runlim] sample:		347.6 time, 350.3 real, 392.4 MB
[runlim] sample:		357.6 time, 360.3 real, 392.1 MB
[runlim] sample:		367.6 time, 370.3 real, 393.0 MB
[runlim] sample:		377.6 time, 380.3 real, 392.9 MB
[runlim] sample:		387.6 time, 390.3 real, 393.0 MB
[runlim] sample:		397.6 time, 400.3 real, 397.1 MB
[runlim] sample:		407.6 time, 410.3 real, 415.1 MB
[runlim] sample:		417.5 time, 420.3 real, 437.2 MB
[runlim] sample:		427.5 time, 430.3 real, 437.2 MB
[runlim] sample:		437.5 time, 440.3 real, 520.8 MB
[runlim] sample:		447.5 time, 450.3 real, 396.0 MB
[runlim] sample:		457.5 time, 460.3 real, 401.4 MB
[runlim] sample:		467.5 time, 470.3 real, 400.2 MB
[runlim] sample:		477.4 time, 480.3 real, 414.7 MB
[runlim] sample:		487.4 time, 490.3 real, 437.2 MB
[runlim] sample:		497.4 time, 500.3 real, 461.3 MB
[runlim] sample:		507.4 time, 510.3 real, 461.4 MB
[runlim] sample:		517.4 time, 520.3 real, 401.5 MB
[runlim] sample:		527.4 time, 530.3 real, 429.9 MB
[runlim] sample:		537.4 time, 540.3 real, 452.1 MB
[runlim] sample:		547.4 time, 550.3 real, 467.9 MB
[runlim] end:			Fri May  1 14:09:50 2015
[runlim] status:		ok
[runlim] result:		10
[runlim] children:		61
[runlim] real:			553.61 seconds
[runlim] time:			550.55 seconds
[runlim] space:			530.9 MB
[runlim] samples:		5532
