[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/SAT_dat.k85-24_1_rule_2.cnf.bz2
[runlim] start:			Sun Apr 26 22:25:56 2015
[runlim] main pid:		3181
[runlim] sample:		5.6 time, 10.3 real, 303.2 MB
[runlim] sample:		15.6 time, 20.3 real, 238.2 MB
[runlim] sample:		25.6 time, 30.3 real, 309.1 MB
[runlim] sample:		35.6 time, 40.3 real, 250.6 MB
[runlim] sample:		45.6 time, 50.3 real, 309.9 MB
[runlim] sample:		55.6 time, 60.3 real, 324.0 MB
[runlim] sample:		65.6 time, 70.3 real, 313.6 MB
[runlim] sample:		75.5 time, 80.3 real, 359.7 MB
[runlim] sample:		85.5 time, 90.3 real, 245.8 MB
[runlim] sample:		95.5 time, 100.3 real, 286.3 MB
[runlim] sample:		105.5 time, 110.3 real, 280.8 MB
[runlim] sample:		115.5 time, 120.3 real, 320.1 MB
[runlim] sample:		125.5 time, 130.3 real, 338.1 MB
[runlim] sample:		135.4 time, 140.3 real, 282.4 MB
[runlim] sample:		145.4 time, 150.3 real, 280.0 MB
[runlim] sample:		155.4 time, 160.3 real, 279.6 MB
[runlim] sample:		165.4 time, 170.3 real, 318.5 MB
[runlim] sample:		175.4 time, 180.3 real, 336.9 MB
[runlim] sample:		185.3 time, 190.3 real, 229.0 MB
[runlim] sample:		195.3 time, 200.3 real, 274.4 MB
[runlim] sample:		205.3 time, 210.3 real, 274.1 MB
[runlim] sample:		215.3 time, 220.3 real, 273.3 MB
[runlim] sample:		225.3 time, 230.3 real, 345.1 MB
[runlim] sample:		235.3 time, 240.3 real, 272.8 MB
[runlim] sample:		245.3 time, 250.3 real, 272.8 MB
[runlim] sample:		255.2 time, 260.3 real, 272.3 MB
[runlim] sample:		265.2 time, 270.3 real, 270.8 MB
[runlim] sample:		275.2 time, 280.3 real, 271.5 MB
[runlim] sample:		285.2 time, 290.3 real, 268.5 MB
[runlim] sample:		295.2 time, 300.3 real, 268.5 MB
[runlim] sample:		305.2 time, 310.3 real, 268.5 MB
[runlim] sample:		315.2 time, 320.3 real, 268.5 MB
[runlim] sample:		325.1 time, 330.3 real, 267.9 MB
[runlim] sample:		335.1 time, 340.3 real, 267.0 MB
[runlim] sample:		345.1 time, 350.3 real, 267.0 MB
[runlim] sample:		355.1 time, 360.3 real, 267.0 MB
[runlim] sample:		365.1 time, 370.3 real, 267.0 MB
[runlim] sample:		375.1 time, 380.3 real, 267.0 MB
[runlim] sample:		385.1 time, 390.3 real, 322.0 MB
[runlim] sample:		395.0 time, 400.3 real, 322.0 MB
[runlim] sample:		405.0 time, 410.3 real, 264.5 MB
[runlim] sample:		415.0 time, 420.3 real, 266.6 MB
[runlim] sample:		425.0 time, 430.3 real, 316.5 MB
[runlim] sample:		435.0 time, 440.3 real, 263.8 MB
[runlim] sample:		445.0 time, 450.3 real, 222.4 MB
[runlim] sample:		455.0 time, 460.3 real, 315.3 MB
[runlim] sample:		465.0 time, 470.3 real, 221.8 MB
[runlim] sample:		474.9 time, 480.3 real, 313.5 MB
[runlim] sample:		484.9 time, 490.3 real, 258.2 MB
[runlim] sample:		494.9 time, 500.3 real, 258.2 MB
[runlim] sample:		504.9 time, 510.3 real, 258.2 MB
[runlim] sample:		514.9 time, 520.3 real, 258.2 MB
[runlim] sample:		524.9 time, 530.3 real, 258.2 MB
[runlim] sample:		534.9 time, 540.3 real, 259.5 MB
[runlim] sample:		544.9 time, 550.3 real, 311.2 MB
[runlim] sample:		554.8 time, 560.3 real, 254.9 MB
[runlim] sample:		564.8 time, 570.3 real, 263.4 MB
[runlim] sample:		574.8 time, 580.3 real, 309.4 MB
[runlim] sample:		584.8 time, 590.3 real, 253.7 MB
[runlim] sample:		594.8 time, 600.3 real, 309.1 MB
[runlim] sample:		604.8 time, 610.3 real, 254.4 MB
[runlim] sample:		614.8 time, 620.3 real, 254.4 MB
[runlim] sample:		624.8 time, 630.3 real, 254.4 MB
[runlim] sample:		634.7 time, 640.3 real, 254.4 MB
[runlim] sample:		644.7 time, 650.3 real, 254.4 MB
[runlim] sample:		654.7 time, 660.3 real, 254.4 MB
[runlim] sample:		664.7 time, 670.3 real, 254.4 MB
[runlim] sample:		674.7 time, 680.3 real, 255.1 MB
[runlim] sample:		684.7 time, 690.3 real, 250.7 MB
[runlim] sample:		694.7 time, 700.3 real, 250.7 MB
[runlim] sample:		704.6 time, 710.3 real, 260.2 MB
[runlim] sample:		714.6 time, 720.3 real, 303.6 MB
[runlim] sample:		724.6 time, 730.3 real, 260.2 MB
[runlim] sample:		734.6 time, 740.3 real, 246.3 MB
[runlim] sample:		744.6 time, 750.3 real, 246.2 MB
[runlim] sample:		754.6 time, 760.3 real, 246.2 MB
[runlim] sample:		764.6 time, 770.3 real, 246.2 MB
[runlim] sample:		774.6 time, 780.3 real, 246.2 MB
[runlim] sample:		784.5 time, 790.3 real, 246.2 MB
[runlim] sample:		794.5 time, 800.3 real, 246.2 MB
[runlim] sample:		804.5 time, 810.3 real, 246.2 MB
[runlim] sample:		814.5 time, 820.3 real, 246.8 MB
[runlim] sample:		824.5 time, 830.3 real, 245.7 MB
[runlim] sample:		834.5 time, 840.3 real, 243.9 MB
[runlim] sample:		844.5 time, 850.3 real, 213.8 MB
[runlim] sample:		854.5 time, 860.3 real, 242.3 MB
[runlim] sample:		864.4 time, 870.3 real, 242.3 MB
[runlim] sample:		874.4 time, 880.3 real, 242.3 MB
[runlim] sample:		884.4 time, 890.3 real, 242.3 MB
[runlim] sample:		894.4 time, 900.3 real, 242.3 MB
[runlim] sample:		904.4 time, 910.3 real, 242.3 MB
[runlim] sample:		914.4 time, 920.3 real, 242.3 MB
[runlim] sample:		924.4 time, 930.3 real, 297.2 MB
[runlim] sample:		934.3 time, 940.3 real, 243.3 MB
[runlim] sample:		944.3 time, 950.3 real, 243.3 MB
[runlim] sample:		954.3 time, 960.3 real, 243.3 MB
[runlim] sample:		964.3 time, 970.3 real, 243.3 MB
[runlim] sample:		974.3 time, 980.3 real, 243.3 MB
[runlim] sample:		984.3 time, 990.3 real, 243.3 MB
[runlim] sample:		994.2 time, 1000.3 real, 243.3 MB
[runlim] end:			Sun Apr 26 22:42:42 2015
[runlim] status:		out of time
[runlim] result:		1
[runlim] children:		159
[runlim] real:			1006.17 seconds
[runlim] time:			1000.04 seconds
[runlim] space:			522.9 MB
[runlim] samples:		10058
