[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.k70-24_1_rule_3.cnf.bz2
[runlim] argv[2]:		/home/biere/src/minisat/build/release/bin/minisat
[runlim] start:			Thu May  7 20:52:21 2015
[runlim] main pid:		24241
[runlim] sample:		5.1 time, 10.9 real, 514.5 MB
[runlim] sample:		15.1 time, 20.9 real, 448.2 MB
[runlim] sample:		25.1 time, 30.9 real, 450.2 MB
[runlim] sample:		35.1 time, 40.9 real, 450.2 MB
[runlim] sample:		45.1 time, 50.9 real, 452.2 MB
[runlim] sample:		55.0 time, 60.9 real, 452.2 MB
[runlim] sample:		65.0 time, 70.9 real, 454.2 MB
[runlim] sample:		75.0 time, 80.9 real, 454.2 MB
[runlim] sample:		85.0 time, 90.9 real, 458.3 MB
[runlim] sample:		95.0 time, 100.9 real, 460.3 MB
[runlim] sample:		104.9 time, 110.9 real, 460.3 MB
[runlim] sample:		114.9 time, 120.9 real, 462.3 MB
[runlim] sample:		124.9 time, 130.9 real, 463.9 MB
[runlim] sample:		134.9 time, 140.9 real, 466.2 MB
[runlim] sample:		144.8 time, 150.9 real, 469.6 MB
[runlim] sample:		154.8 time, 160.9 real, 473.4 MB
[runlim] sample:		164.8 time, 170.9 real, 476.3 MB
[runlim] sample:		174.8 time, 180.9 real, 481.5 MB
[runlim] sample:		184.8 time, 190.9 real, 483.5 MB
[runlim] sample:		194.8 time, 200.9 real, 485.5 MB
[runlim] sample:		204.7 time, 210.9 real, 490.4 MB
[runlim] sample:		214.7 time, 220.9 real, 490.6 MB
[runlim] sample:		224.7 time, 230.9 real, 494.6 MB
[runlim] sample:		234.7 time, 240.9 real, 496.6 MB
[runlim] sample:		244.7 time, 250.9 real, 498.6 MB
[runlim] sample:		254.7 time, 260.9 real, 505.0 MB
[runlim] sample:		264.6 time, 270.9 real, 507.0 MB
[runlim] sample:		274.6 time, 280.9 real, 509.0 MB
[runlim] sample:		284.6 time, 290.9 real, 511.0 MB
[runlim] sample:		294.6 time, 300.9 real, 513.0 MB
[runlim] sample:		304.6 time, 310.9 real, 515.0 MB
[runlim] sample:		314.5 time, 320.9 real, 517.0 MB
[runlim] sample:		324.5 time, 330.9 real, 519.0 MB
[runlim] sample:		334.5 time, 340.9 real, 519.0 MB
[runlim] sample:		344.5 time, 350.9 real, 523.1 MB
[runlim] sample:		354.4 time, 360.9 real, 525.1 MB
[runlim] sample:		364.4 time, 370.9 real, 525.1 MB
[runlim] sample:		374.4 time, 380.9 real, 527.1 MB
[runlim] sample:		384.4 time, 390.9 real, 529.1 MB
[runlim] sample:		394.4 time, 400.9 real, 533.1 MB
[runlim] sample:		404.4 time, 410.9 real, 537.1 MB
[runlim] sample:		414.4 time, 420.9 real, 539.1 MB
[runlim] sample:		424.4 time, 430.9 real, 541.1 MB
[runlim] sample:		434.3 time, 440.9 real, 543.1 MB
[runlim] sample:		444.3 time, 450.9 real, 545.1 MB
[runlim] sample:		454.3 time, 460.9 real, 545.1 MB
[runlim] sample:		464.3 time, 470.9 real, 547.1 MB
[runlim] sample:		474.3 time, 480.9 real, 547.7 MB
[runlim] sample:		484.3 time, 490.9 real, 548.5 MB
[runlim] sample:		494.3 time, 500.9 real, 551.0 MB
[runlim] sample:		504.2 time, 510.9 real, 553.0 MB
[runlim] sample:		514.2 time, 520.9 real, 555.0 MB
[runlim] sample:		524.2 time, 530.9 real, 557.0 MB
[runlim] sample:		534.2 time, 540.9 real, 557.0 MB
[runlim] sample:		544.2 time, 550.9 real, 559.0 MB
[runlim] sample:		554.2 time, 560.9 real, 561.0 MB
[runlim] sample:		564.1 time, 570.9 real, 561.0 MB
[runlim] sample:		574.1 time, 580.9 real, 563.0 MB
[runlim] sample:		584.1 time, 590.9 real, 565.0 MB
[runlim] sample:		594.1 time, 600.9 real, 569.0 MB
[runlim] sample:		604.1 time, 610.9 real, 571.0 MB
[runlim] sample:		614.1 time, 620.9 real, 571.0 MB
[runlim] sample:		624.1 time, 630.9 real, 575.0 MB
[runlim] sample:		634.0 time, 640.9 real, 577.0 MB
[runlim] sample:		644.0 time, 650.9 real, 579.0 MB
[runlim] sample:		654.0 time, 660.9 real, 579.0 MB
[runlim] sample:		664.0 time, 670.9 real, 581.0 MB
[runlim] sample:		674.0 time, 680.9 real, 583.0 MB
[runlim] sample:		684.0 time, 690.9 real, 585.0 MB
[runlim] sample:		694.0 time, 700.9 real, 587.0 MB
[runlim] sample:		703.9 time, 710.9 real, 589.0 MB
[runlim] sample:		713.9 time, 720.9 real, 591.0 MB
[runlim] sample:		723.9 time, 730.9 real, 591.0 MB
[runlim] sample:		733.9 time, 740.9 real, 593.0 MB
[runlim] sample:		743.9 time, 750.9 real, 595.0 MB
[runlim] sample:		753.9 time, 760.9 real, 597.0 MB
[runlim] sample:		763.9 time, 770.9 real, 599.0 MB
[runlim] sample:		773.8 time, 780.9 real, 599.0 MB
[runlim] sample:		783.8 time, 790.9 real, 601.0 MB
[runlim] sample:		793.8 time, 800.9 real, 603.0 MB
[runlim] sample:		803.8 time, 810.9 real, 603.0 MB
[runlim] sample:		813.8 time, 820.9 real, 605.0 MB
[runlim] sample:		823.8 time, 830.9 real, 607.0 MB
[runlim] sample:		833.8 time, 840.9 real, 609.0 MB
[runlim] sample:		843.7 time, 850.9 real, 609.0 MB
[runlim] sample:		853.7 time, 860.9 real, 611.0 MB
[runlim] sample:		863.7 time, 870.9 real, 611.0 MB
[runlim] sample:		873.7 time, 880.9 real, 613.0 MB
[runlim] sample:		883.7 time, 890.9 real, 615.0 MB
[runlim] sample:		893.7 time, 900.9 real, 615.0 MB
[runlim] sample:		903.6 time, 910.9 real, 617.0 MB
[runlim] sample:		913.6 time, 920.9 real, 619.0 MB
[runlim] sample:		923.6 time, 930.9 real, 619.0 MB
[runlim] sample:		933.6 time, 940.9 real, 621.0 MB
[runlim] sample:		943.6 time, 950.9 real, 623.0 MB
[runlim] sample:		953.6 time, 960.9 real, 623.0 MB
[runlim] sample:		963.6 time, 970.9 real, 625.0 MB
[runlim] sample:		973.5 time, 980.9 real, 627.0 MB
[runlim] sample:		983.5 time, 990.9 real, 627.4 MB
[runlim] sample:		993.5 time, 1000.9 real, 628.6 MB
[runlim] end:			Thu May  7 21:09:08 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		38
[runlim] real:			1007.62 seconds
[runlim] time:			1000.02 seconds
[runlim] space:			630.9 MB
[runlim] samples:		10067
