[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=3
[runlim] argv[2]:		-v
[runlim] argv[3]:		-n
[runlim] argv[4]:		/data/cnf/sc2014/app/esawn_uw3.debugged.cnf.bz2
[runlim] start:			Mon Apr 27 10:49:32 2015
[runlim] main pid:		21395
[runlim] sample:		11.7 time, 10.8 real, 652.4 MB
[runlim] sample:		23.7 time, 20.8 real, 1304.6 MB
[runlim] sample:		35.9 time, 30.8 real, 1826.7 MB
[runlim] sample:		47.2 time, 40.8 real, 2602.6 MB
[runlim] sample:		61.9 time, 52.7 real, 2618.6 MB
[runlim] sample:		74.0 time, 62.7 real, 3642.6 MB
[runlim] sample:		45.8 time, 72.7 real, 3439.6 MB
[runlim] sample:		55.8 time, 82.7 real, 3185.6 MB
[runlim] sample:		65.7 time, 92.7 real, 4590.3 MB
[runlim] sample:		75.7 time, 102.7 real, 3663.6 MB
[runlim] sample:		85.7 time, 112.7 real, 2470.5 MB
[runlim] sample:		95.7 time, 122.7 real, 3366.2 MB
[runlim] sample:		105.7 time, 132.7 real, 3933.3 MB
[runlim] sample:		115.6 time, 142.7 real, 3933.3 MB
[runlim] sample:		125.6 time, 152.7 real, 3684.4 MB
[runlim] sample:		135.6 time, 162.7 real, 2405.7 MB
[runlim] sample:		145.6 time, 172.7 real, 3313.6 MB
[runlim] sample:		155.6 time, 182.7 real, 2237.7 MB
[runlim] sample:		165.6 time, 192.7 real, 2237.7 MB
[runlim] sample:		175.5 time, 202.7 real, 3353.5 MB
[runlim] sample:		185.5 time, 212.7 real, 3513.4 MB
[runlim] sample:		195.5 time, 222.7 real, 3513.4 MB
[runlim] sample:		205.5 time, 232.7 real, 4501.9 MB
[runlim] sample:		215.5 time, 242.7 real, 3228.1 MB
[runlim] sample:		225.4 time, 252.7 real, 3565.9 MB
[runlim] sample:		235.4 time, 262.7 real, 4682.4 MB
[runlim] sample:		245.4 time, 272.7 real, 3266.7 MB
[runlim] sample:		255.4 time, 282.7 real, 3448.4 MB
[runlim] sample:		265.4 time, 292.7 real, 4701.9 MB
[runlim] sample:		275.4 time, 302.7 real, 3272.3 MB
[runlim] sample:		285.3 time, 312.7 real, 3478.9 MB
[runlim] sample:		295.3 time, 322.7 real, 3478.9 MB
[runlim] sample:		305.3 time, 332.7 real, 3478.9 MB
[runlim] sample:		315.3 time, 342.7 real, 3478.9 MB
[runlim] sample:		325.3 time, 352.7 real, 3478.9 MB
[runlim] sample:		335.3 time, 362.7 real, 3478.9 MB
[runlim] sample:		345.3 time, 372.7 real, 3478.9 MB
[runlim] sample:		355.3 time, 382.7 real, 3478.9 MB
[runlim] sample:		365.3 time, 392.7 real, 2355.3 MB
[runlim] sample:		375.2 time, 402.7 real, 3931.0 MB
[runlim] sample:		385.2 time, 412.7 real, 3699.7 MB
[runlim] sample:		395.2 time, 422.7 real, 4413.5 MB
[runlim] sample:		405.2 time, 432.7 real, 3360.8 MB
[runlim] sample:		415.2 time, 442.7 real, 3368.0 MB
[runlim] sample:		425.2 time, 452.7 real, 2321.3 MB
[runlim] sample:		435.2 time, 462.7 real, 2321.3 MB
[runlim] sample:		445.1 time, 472.7 real, 3330.0 MB
[runlim] sample:		455.1 time, 482.7 real, 3330.0 MB
[runlim] end:			Mon Apr 27 10:57:40 2015
[runlim] status:		ok
[runlim] result:		10
[runlim] children:		1278
[runlim] real:			488.48 seconds
[runlim] time:			460.86 seconds
[runlim] space:			4701.9 MB
[runlim] samples:		4858
