[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/oski15a08b11s.aig
[runlim] start:			Mon Sep 28 17:06:18 2015
[runlim] main pid:		20230
[runlim] sample:		9.5 time, 10.5 real, 505.0 MB
[runlim] sample:		19.5 time, 20.5 real, 988.1 MB
[runlim] sample:		29.4 time, 30.5 real, 1784.7 MB
[runlim] sample:		39.4 time, 40.5 real, 2266.6 MB
[runlim] sample:		49.4 time, 50.5 real, 2869.5 MB
[runlim] sample:		59.4 time, 60.5 real, 3463.8 MB
[runlim] sample:		69.4 time, 70.5 real, 4140.4 MB
[runlim] sample:		79.4 time, 80.5 real, 4610.5 MB
[runlim] sample:		89.4 time, 90.5 real, 5286.2 MB
[runlim] sample:		99.3 time, 100.5 real, 5820.0 MB
[runlim] sample:		109.3 time, 110.5 real, 6332.6 MB
[runlim] sample:		6.5 time, 120.5 real, 334.7 MB
[runlim] sample:		16.5 time, 130.5 real, 742.8 MB
[runlim] sample:		26.5 time, 140.5 real, 1548.9 MB
[runlim] sample:		36.5 time, 150.5 real, 2228.9 MB
[runlim] sample:		46.4 time, 160.5 real, 2662.7 MB
[runlim] sample:		56.4 time, 170.5 real, 3278.3 MB
[runlim] sample:		66.4 time, 180.5 real, 3954.7 MB
[runlim] sample:		76.4 time, 190.5 real, 4448.9 MB
[runlim] sample:		86.4 time, 200.5 real, 5088.8 MB
[runlim] sample:		96.4 time, 210.5 real, 5640.9 MB
[runlim] sample:		106.4 time, 220.5 real, 6179.6 MB
[runlim] sample:		3.6 time, 230.5 real, 246.5 MB
[runlim] sample:		13.6 time, 240.5 real, 621.4 MB
[runlim] sample:		23.6 time, 250.5 real, 1318.8 MB
[runlim] sample:		33.6 time, 260.5 real, 2140.9 MB
[runlim] sample:		43.6 time, 270.5 real, 2523.4 MB
[runlim] sample:		53.5 time, 280.5 real, 3211.1 MB
[runlim] sample:		63.5 time, 290.5 real, 3864.5 MB
[runlim] sample:		73.5 time, 300.5 real, 4369.3 MB
[runlim] sample:		83.5 time, 310.5 real, 5028.3 MB
[runlim] sample:		93.5 time, 320.5 real, 5587.0 MB
[runlim] sample:		103.5 time, 330.5 real, 6119.5 MB
[runlim] sample:		2.6 time, 340.5 real, 209.6 MB
[runlim] sample:		12.6 time, 350.5 real, 622.8 MB
[runlim] sample:		22.6 time, 360.5 real, 1228.7 MB
[runlim] sample:		32.6 time, 370.5 real, 2039.0 MB
[runlim] sample:		42.6 time, 380.5 real, 2407.1 MB
[runlim] sample:		52.5 time, 390.5 real, 3070.0 MB
[runlim] sample:		62.5 time, 400.5 real, 3735.7 MB
[runlim] sample:		72.5 time, 410.5 real, 4299.4 MB
[runlim] sample:		82.5 time, 420.5 real, 4861.0 MB
[runlim] sample:		92.5 time, 430.5 real, 5447.4 MB
[runlim] sample:		102.5 time, 440.5 real, 5972.0 MB
[runlim] sample:		112.5 time, 450.5 real, 4.1 MB
[runlim] sample:		9.6 time, 460.5 real, 513.2 MB
[runlim] sample:		19.6 time, 470.5 real, 996.7 MB
[runlim] sample:		29.6 time, 480.5 real, 1785.3 MB
[runlim] sample:		39.6 time, 490.5 real, 2285.4 MB
[runlim] sample:		49.6 time, 500.5 real, 2897.6 MB
[runlim] sample:		59.6 time, 510.5 real, 3548.2 MB
[runlim] sample:		69.5 time, 520.5 real, 4210.1 MB
[runlim] sample:		79.5 time, 530.5 real, 4698.1 MB
[runlim] sample:		89.5 time, 540.5 real, 5353.8 MB
[runlim] sample:		99.5 time, 550.5 real, 5899.1 MB
[runlim] sample:		109.5 time, 560.5 real, 6424.3 MB
[runlim] end:			Mon Sep 28 17:15:40 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		33668
[runlim] real:			562.26 seconds
[runlim] time:			112.63 seconds
[runlim] space:			6555.7 MB
[runlim] samples:		5617
