[runlim] version:		1.9
[runlim] time limit:		311040000 seconds
[runlim] real time limit:	3600 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/hwmcc15/solvers/iprover/single.iproverhc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b37s.aig
[runlim] start:			Mon Sep 28 16:42:02 2015
[runlim] main pid:		24961
[runlim] sample:		9.7 time, 10.2 real, 634.7 MB
[runlim] sample:		19.7 time, 20.2 real, 1235.9 MB
[runlim] sample:		29.7 time, 30.2 real, 1852.5 MB
[runlim] sample:		39.7 time, 40.2 real, 2443.8 MB
[runlim] sample:		49.7 time, 50.2 real, 2920.9 MB
[runlim] sample:		59.7 time, 60.2 real, 3419.0 MB
[runlim] sample:		69.7 time, 70.2 real, 3657.0 MB
[runlim] sample:		79.7 time, 80.2 real, 3741.1 MB
[runlim] sample:		89.7 time, 90.2 real, 4025.6 MB
[runlim] sample:		99.7 time, 100.2 real, 4313.6 MB
[runlim] sample:		109.7 time, 110.2 real, 4581.6 MB
[runlim] sample:		119.7 time, 120.2 real, 4797.4 MB
[runlim] sample:		129.7 time, 130.2 real, 5027.7 MB
[runlim] sample:		139.7 time, 140.2 real, 5237.6 MB
[runlim] sample:		149.7 time, 150.2 real, 5499.6 MB
[runlim] sample:		159.7 time, 160.2 real, 5643.7 MB
[runlim] sample:		169.7 time, 170.2 real, 5797.6 MB
[runlim] sample:		179.7 time, 180.2 real, 5899.4 MB
[runlim] sample:		189.7 time, 190.2 real, 6035.6 MB
[runlim] sample:		199.7 time, 200.2 real, 6142.2 MB
[runlim] sample:		209.7 time, 210.2 real, 6211.4 MB
[runlim] sample:		219.7 time, 220.2 real, 6433.5 MB
[runlim] sample:		6.0 time, 230.2 real, 313.2 MB
[runlim] sample:		15.9 time, 240.2 real, 980.4 MB
[runlim] sample:		25.9 time, 250.2 real, 1628.1 MB
[runlim] sample:		35.9 time, 260.2 real, 2228.9 MB
[runlim] sample:		45.9 time, 270.2 real, 2821.0 MB
[runlim] sample:		55.9 time, 280.2 real, 3204.2 MB
[runlim] sample:		65.9 time, 290.2 real, 3618.3 MB
[runlim] sample:		75.9 time, 300.2 real, 3684.2 MB
[runlim] sample:		85.9 time, 310.2 real, 3937.4 MB
[runlim] sample:		95.9 time, 320.2 real, 4211.2 MB
[runlim] sample:		105.9 time, 330.2 real, 4513.4 MB
[runlim] sample:		115.9 time, 340.2 real, 4717.3 MB
[runlim] sample:		125.9 time, 350.2 real, 4953.4 MB
[runlim] sample:		135.9 time, 360.2 real, 5167.4 MB
[runlim] sample:		145.9 time, 370.2 real, 5419.2 MB
[runlim] sample:		155.9 time, 380.2 real, 5623.3 MB
[runlim] sample:		165.9 time, 390.2 real, 5773.4 MB
[runlim] sample:		175.9 time, 400.2 real, 5857.5 MB
[runlim] sample:		185.9 time, 410.2 real, 5988.6 MB
[runlim] sample:		195.9 time, 420.2 real, 6135.3 MB
[runlim] sample:		205.9 time, 430.2 real, 6174.4 MB
[runlim] sample:		215.9 time, 440.2 real, 6402.5 MB
[runlim] sample:		2.7 time, 450.2 real, 165.5 MB
[runlim] sample:		12.7 time, 460.2 real, 883.3 MB
[runlim] sample:		22.7 time, 470.2 real, 1489.7 MB
[runlim] sample:		32.7 time, 480.2 real, 2114.6 MB
[runlim] sample:		42.7 time, 490.2 real, 2717.4 MB
[runlim] sample:		52.7 time, 500.2 real, 3105.2 MB
[runlim] sample:		62.7 time, 510.2 real, 3685.2 MB
[runlim] sample:		72.7 time, 520.2 real, 3767.8 MB
[runlim] sample:		82.7 time, 530.2 real, 3949.2 MB
[runlim] sample:		92.7 time, 540.2 real, 4237.9 MB
[runlim] sample:		102.7 time, 550.2 real, 4536.9 MB
[runlim] sample:		112.7 time, 560.2 real, 4786.5 MB
[runlim] sample:		122.7 time, 570.2 real, 5012.3 MB
[runlim] sample:		132.7 time, 580.2 real, 5234.4 MB
[runlim] sample:		142.7 time, 590.2 real, 5454.4 MB
[runlim] sample:		152.7 time, 600.2 real, 5700.5 MB
[runlim] sample:		162.7 time, 610.2 real, 5854.3 MB
[runlim] sample:		172.7 time, 620.2 real, 5982.4 MB
[runlim] sample:		182.7 time, 630.2 real, 6084.4 MB
[runlim] sample:		192.7 time, 640.2 real, 6216.4 MB
[runlim] sample:		202.7 time, 650.2 real, 6258.4 MB
[runlim] sample:		212.7 time, 660.2 real, 6484.2 MB
[runlim] sample:		3.9 time, 670.2 real, 229.4 MB
[runlim] sample:		13.8 time, 680.2 real, 895.7 MB
[runlim] sample:		23.8 time, 690.2 real, 1481.6 MB
[runlim] sample:		33.8 time, 700.2 real, 2122.3 MB
[runlim] sample:		43.8 time, 710.2 real, 2671.7 MB
[runlim] sample:		53.8 time, 720.2 real, 3002.2 MB
[runlim] sample:		63.8 time, 730.2 real, 3296.4 MB
[runlim] sample:		73.8 time, 740.2 real, 3774.1 MB
[runlim] sample:		83.8 time, 750.2 real, 4179.8 MB
[runlim] sample:		93.8 time, 760.2 real, 4461.6 MB
[runlim] sample:		103.8 time, 770.2 real, 4466.4 MB
[runlim] sample:		113.8 time, 780.2 real, 4674.8 MB
[runlim] sample:		123.8 time, 790.2 real, 4800.9 MB
[runlim] sample:		133.8 time, 800.2 real, 4896.9 MB
[runlim] sample:		143.8 time, 810.2 real, 4969.1 MB
[runlim] sample:		153.8 time, 820.2 real, 5097.0 MB
[runlim] end:			Mon Sep 28 16:55:52 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		49767
[runlim] real:			830.07 seconds
[runlim] time:			223.45 seconds
[runlim] space:			6600.4 MB
[runlim] samples:		8298
