[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/SAT_dat.k75-24_1_rule_3.cnf.bz2
[runlim] argv[2]:		/home/biere/src/minisat/build/release/bin/minisat
[runlim] start:			Thu May  7 20:54:19 2015
[runlim] main pid:		24053
[runlim] sample:		5.2 time, 10.4 real, 521.6 MB
[runlim] sample:		15.2 time, 20.4 real, 587.6 MB
[runlim] sample:		25.2 time, 30.4 real, 482.7 MB
[runlim] sample:		35.1 time, 40.4 real, 482.7 MB
[runlim] sample:		45.1 time, 50.4 real, 484.7 MB
[runlim] sample:		55.1 time, 60.4 real, 484.7 MB
[runlim] sample:		65.1 time, 70.4 real, 486.7 MB
[runlim] sample:		75.1 time, 80.4 real, 486.7 MB
[runlim] sample:		85.1 time, 90.4 real, 486.7 MB
[runlim] sample:		95.0 time, 100.4 real, 490.7 MB
[runlim] sample:		105.0 time, 110.4 real, 492.8 MB
[runlim] sample:		115.0 time, 120.4 real, 493.0 MB
[runlim] sample:		125.0 time, 130.4 real, 496.8 MB
[runlim] sample:		135.0 time, 140.4 real, 499.3 MB
[runlim] sample:		144.9 time, 150.4 real, 502.8 MB
[runlim] sample:		154.9 time, 160.4 real, 507.5 MB
[runlim] sample:		164.9 time, 170.4 real, 510.1 MB
[runlim] sample:		174.9 time, 180.4 real, 512.1 MB
[runlim] sample:		184.9 time, 190.4 real, 516.1 MB
[runlim] sample:		194.8 time, 200.4 real, 518.1 MB
[runlim] sample:		204.8 time, 210.4 real, 520.1 MB
[runlim] sample:		214.8 time, 220.4 real, 522.1 MB
[runlim] sample:		224.8 time, 230.4 real, 524.1 MB
[runlim] sample:		234.8 time, 240.4 real, 526.8 MB
[runlim] sample:		244.8 time, 250.4 real, 530.3 MB
[runlim] sample:		254.8 time, 260.4 real, 534.3 MB
[runlim] sample:		264.7 time, 270.4 real, 536.3 MB
[runlim] sample:		274.7 time, 280.4 real, 536.5 MB
[runlim] sample:		284.7 time, 290.4 real, 538.5 MB
[runlim] sample:		294.7 time, 300.4 real, 540.5 MB
[runlim] sample:		304.7 time, 310.4 real, 542.5 MB
[runlim] sample:		314.6 time, 320.4 real, 544.5 MB
[runlim] sample:		324.6 time, 330.4 real, 546.5 MB
[runlim] sample:		334.6 time, 340.4 real, 546.5 MB
[runlim] sample:		344.6 time, 350.4 real, 548.5 MB
[runlim] sample:		354.6 time, 360.4 real, 550.5 MB
[runlim] sample:		364.6 time, 370.4 real, 552.5 MB
[runlim] sample:		374.6 time, 380.4 real, 552.5 MB
[runlim] sample:		384.5 time, 390.4 real, 556.5 MB
[runlim] sample:		394.5 time, 400.4 real, 556.5 MB
[runlim] sample:		404.5 time, 410.4 real, 558.5 MB
[runlim] sample:		414.5 time, 420.4 real, 558.5 MB
[runlim] sample:		424.5 time, 430.4 real, 560.5 MB
[runlim] sample:		434.5 time, 440.4 real, 562.5 MB
[runlim] sample:		444.4 time, 450.4 real, 562.5 MB
[runlim] sample:		454.4 time, 460.4 real, 564.5 MB
[runlim] sample:		464.4 time, 470.4 real, 566.5 MB
[runlim] sample:		474.4 time, 480.4 real, 568.5 MB
[runlim] sample:		484.4 time, 490.4 real, 570.5 MB
[runlim] sample:		494.4 time, 500.4 real, 570.5 MB
[runlim] sample:		504.4 time, 510.4 real, 572.5 MB
[runlim] sample:		514.4 time, 520.4 real, 574.5 MB
[runlim] sample:		524.3 time, 530.4 real, 574.5 MB
[runlim] sample:		534.3 time, 540.4 real, 575.5 MB
[runlim] sample:		544.3 time, 550.4 real, 578.3 MB
[runlim] sample:		554.3 time, 560.4 real, 580.5 MB
[runlim] sample:		564.3 time, 570.4 real, 582.5 MB
[runlim] sample:		574.3 time, 580.4 real, 584.5 MB
[runlim] sample:		584.2 time, 590.4 real, 586.5 MB
[runlim] sample:		594.2 time, 600.4 real, 586.5 MB
[runlim] sample:		604.2 time, 610.4 real, 590.5 MB
[runlim] sample:		614.2 time, 620.4 real, 590.5 MB
[runlim] sample:		624.2 time, 630.4 real, 592.5 MB
[runlim] sample:		634.2 time, 640.4 real, 592.5 MB
[runlim] sample:		644.2 time, 650.4 real, 592.5 MB
[runlim] sample:		654.1 time, 660.4 real, 594.5 MB
[runlim] sample:		664.1 time, 670.4 real, 594.5 MB
[runlim] sample:		674.1 time, 680.4 real, 596.5 MB
[runlim] sample:		684.1 time, 690.4 real, 598.5 MB
[runlim] sample:		694.1 time, 700.4 real, 598.5 MB
[runlim] sample:		704.1 time, 710.4 real, 602.5 MB
[runlim] sample:		714.1 time, 720.4 real, 602.5 MB
[runlim] sample:		724.0 time, 730.4 real, 604.5 MB
[runlim] sample:		734.0 time, 740.4 real, 606.5 MB
[runlim] sample:		744.0 time, 750.4 real, 606.5 MB
[runlim] sample:		754.0 time, 760.4 real, 608.5 MB
[runlim] sample:		764.0 time, 770.4 real, 608.5 MB
[runlim] sample:		774.0 time, 780.4 real, 610.5 MB
[runlim] sample:		784.0 time, 790.4 real, 612.5 MB
[runlim] sample:		793.9 time, 800.4 real, 612.5 MB
[runlim] sample:		803.9 time, 810.4 real, 614.5 MB
[runlim] sample:		813.9 time, 820.4 real, 616.5 MB
[runlim] sample:		823.9 time, 830.4 real, 618.5 MB
[runlim] sample:		833.9 time, 840.4 real, 618.5 MB
[runlim] sample:		843.9 time, 850.4 real, 620.5 MB
[runlim] sample:		853.9 time, 860.4 real, 622.5 MB
[runlim] sample:		863.9 time, 870.4 real, 624.5 MB
[runlim] sample:		873.8 time, 880.4 real, 626.5 MB
[runlim] sample:		883.8 time, 890.4 real, 628.5 MB
[runlim] sample:		893.8 time, 900.4 real, 628.5 MB
[runlim] sample:		903.8 time, 910.4 real, 630.5 MB
[runlim] sample:		913.8 time, 920.4 real, 630.5 MB
[runlim] sample:		923.8 time, 930.4 real, 632.5 MB
[runlim] sample:		933.8 time, 940.4 real, 632.5 MB
[runlim] sample:		943.7 time, 950.4 real, 634.5 MB
[runlim] sample:		953.7 time, 960.4 real, 634.5 MB
[runlim] sample:		963.7 time, 970.4 real, 634.5 MB
[runlim] sample:		973.7 time, 980.4 real, 636.5 MB
[runlim] sample:		983.7 time, 990.4 real, 638.5 MB
[runlim] sample:		993.7 time, 1000.4 real, 640.5 MB
[runlim] end:			Thu May  7 21:11:05 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		40
[runlim] real:			1006.89 seconds
[runlim] time:			1000.05 seconds
[runlim] space:			640.5 MB
[runlim] samples:		10064
