[runlim] version:		1.9
[runlim] time limit:		1000 seconds
[runlim] real time limit:	311040000 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/bin/bunzip2-and-then
[runlim] argv[1]:		/data/cnf/sc2014/app/dated-10-17-u.cnf.bz2
[runlim] argv[2]:		/home/biere/bin/glucose23
[runlim] start:			Fri May  8 01:10:47 2015
[runlim] main pid:		27824
[runlim] sample:		8.8 time, 11.0 real, 105.1 MB
[runlim] sample:		18.8 time, 21.0 real, 106.2 MB
[runlim] sample:		28.8 time, 31.0 real, 106.5 MB
[runlim] sample:		38.8 time, 41.0 real, 113.7 MB
[runlim] sample:		48.8 time, 51.0 real, 116.8 MB
[runlim] sample:		58.7 time, 61.0 real, 120.5 MB
[runlim] sample:		68.7 time, 71.0 real, 124.5 MB
[runlim] sample:		78.7 time, 81.0 real, 126.4 MB
[runlim] sample:		88.7 time, 91.0 real, 128.4 MB
[runlim] sample:		98.7 time, 101.0 real, 128.4 MB
[runlim] sample:		108.7 time, 111.0 real, 128.4 MB
[runlim] sample:		118.7 time, 121.0 real, 132.2 MB
[runlim] sample:		128.6 time, 131.0 real, 132.2 MB
[runlim] sample:		138.6 time, 141.0 real, 132.2 MB
[runlim] sample:		148.6 time, 151.0 real, 132.2 MB
[runlim] sample:		158.6 time, 161.0 real, 132.2 MB
[runlim] sample:		168.6 time, 171.0 real, 134.2 MB
[runlim] sample:		178.6 time, 181.0 real, 134.2 MB
[runlim] sample:		188.6 time, 191.0 real, 134.2 MB
[runlim] sample:		198.5 time, 201.0 real, 134.2 MB
[runlim] sample:		208.5 time, 211.0 real, 134.2 MB
[runlim] sample:		218.5 time, 221.0 real, 134.2 MB
[runlim] sample:		228.5 time, 231.0 real, 134.2 MB
[runlim] sample:		238.5 time, 241.0 real, 134.2 MB
[runlim] sample:		248.5 time, 251.0 real, 134.2 MB
[runlim] sample:		258.4 time, 261.0 real, 134.2 MB
[runlim] sample:		268.4 time, 271.0 real, 134.2 MB
[runlim] sample:		278.4 time, 281.0 real, 134.2 MB
[runlim] sample:		288.4 time, 291.0 real, 136.4 MB
[runlim] sample:		298.4 time, 301.0 real, 136.4 MB
[runlim] sample:		308.4 time, 311.0 real, 136.4 MB
[runlim] sample:		318.4 time, 321.0 real, 136.4 MB
[runlim] sample:		328.3 time, 331.0 real, 136.4 MB
[runlim] sample:		338.3 time, 341.0 real, 136.4 MB
[runlim] sample:		348.3 time, 351.0 real, 136.4 MB
[runlim] sample:		358.3 time, 361.0 real, 136.4 MB
[runlim] sample:		368.3 time, 371.0 real, 136.4 MB
[runlim] sample:		378.3 time, 381.0 real, 136.4 MB
[runlim] sample:		388.2 time, 391.0 real, 136.4 MB
[runlim] sample:		398.2 time, 401.0 real, 136.4 MB
[runlim] sample:		408.2 time, 411.0 real, 152.4 MB
[runlim] sample:		418.2 time, 421.0 real, 153.7 MB
[runlim] sample:		428.2 time, 431.0 real, 153.7 MB
[runlim] sample:		438.2 time, 441.0 real, 153.7 MB
[runlim] sample:		448.2 time, 451.0 real, 153.7 MB
[runlim] sample:		458.1 time, 461.0 real, 155.7 MB
[runlim] sample:		468.1 time, 471.0 real, 155.7 MB
[runlim] sample:		478.1 time, 481.0 real, 155.7 MB
[runlim] sample:		488.1 time, 491.0 real, 155.7 MB
[runlim] sample:		498.1 time, 501.0 real, 155.7 MB
[runlim] sample:		508.1 time, 511.0 real, 155.7 MB
[runlim] sample:		518.1 time, 521.0 real, 155.7 MB
[runlim] sample:		528.0 time, 531.0 real, 155.7 MB
[runlim] sample:		538.0 time, 541.0 real, 155.7 MB
[runlim] sample:		548.0 time, 551.0 real, 155.7 MB
[runlim] sample:		558.0 time, 561.0 real, 155.7 MB
[runlim] sample:		568.0 time, 571.0 real, 155.7 MB
[runlim] sample:		578.0 time, 581.0 real, 155.7 MB
[runlim] sample:		588.0 time, 591.0 real, 155.7 MB
[runlim] sample:		597.9 time, 601.0 real, 155.7 MB
[runlim] sample:		607.9 time, 611.0 real, 155.7 MB
[runlim] sample:		617.9 time, 621.0 real, 155.7 MB
[runlim] sample:		627.9 time, 631.0 real, 155.7 MB
[runlim] sample:		637.9 time, 641.0 real, 157.7 MB
[runlim] sample:		647.9 time, 651.0 real, 157.7 MB
[runlim] sample:		657.8 time, 661.0 real, 157.7 MB
[runlim] sample:		667.8 time, 671.0 real, 157.7 MB
[runlim] sample:		677.8 time, 681.0 real, 157.7 MB
[runlim] sample:		687.8 time, 691.0 real, 157.7 MB
[runlim] sample:		697.8 time, 701.0 real, 157.7 MB
[runlim] sample:		707.8 time, 711.0 real, 157.7 MB
[runlim] sample:		717.8 time, 721.0 real, 157.7 MB
[runlim] sample:		727.7 time, 731.0 real, 157.7 MB
[runlim] sample:		737.7 time, 741.0 real, 157.7 MB
[runlim] sample:		747.7 time, 751.0 real, 157.7 MB
[runlim] sample:		757.7 time, 761.0 real, 157.7 MB
[runlim] sample:		767.7 time, 771.0 real, 157.7 MB
[runlim] sample:		777.7 time, 781.0 real, 157.7 MB
[runlim] sample:		787.6 time, 791.0 real, 157.7 MB
[runlim] sample:		797.6 time, 801.0 real, 157.7 MB
[runlim] sample:		807.6 time, 811.0 real, 157.7 MB
[runlim] sample:		817.6 time, 821.0 real, 157.7 MB
[runlim] sample:		827.6 time, 831.0 real, 157.7 MB
[runlim] sample:		837.6 time, 841.0 real, 157.7 MB
[runlim] sample:		847.6 time, 851.0 real, 157.7 MB
[runlim] sample:		857.5 time, 861.0 real, 157.8 MB
[runlim] sample:		867.5 time, 871.0 real, 157.8 MB
[runlim] sample:		877.5 time, 881.0 real, 157.8 MB
[runlim] sample:		887.5 time, 891.0 real, 157.8 MB
[runlim] sample:		897.5 time, 901.0 real, 157.8 MB
[runlim] sample:		907.5 time, 911.0 real, 157.8 MB
[runlim] sample:		917.5 time, 921.0 real, 157.8 MB
[runlim] sample:		927.4 time, 931.0 real, 157.8 MB
[runlim] sample:		937.4 time, 941.0 real, 157.8 MB
[runlim] sample:		947.4 time, 951.0 real, 157.8 MB
[runlim] sample:		957.4 time, 961.0 real, 157.8 MB
[runlim] sample:		967.4 time, 971.0 real, 157.8 MB
[runlim] sample:		977.4 time, 981.0 real, 157.8 MB
[runlim] sample:		987.4 time, 991.0 real, 157.8 MB
[runlim] sample:		997.3 time, 1001.0 real, 157.8 MB
[runlim] end:			Fri May  8 01:27:30 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		10
[runlim] real:			1003.73 seconds
[runlim] time:			1000.03 seconds
[runlim] space:			188.7 MB
[runlim] samples:		10027
