[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/oski15a01b07s.aig
[runlim] start:			Mon Sep 28 15:27:38 2015
[runlim] main pid:		17059
[runlim] sample:		9.5 time, 10.6 real, 616.9 MB
[runlim] sample:		19.5 time, 20.6 real, 1215.2 MB
[runlim] sample:		29.5 time, 30.6 real, 1835.3 MB
[runlim] sample:		39.5 time, 40.6 real, 2433.8 MB
[runlim] sample:		49.5 time, 50.6 real, 2916.4 MB
[runlim] sample:		59.5 time, 60.6 real, 3412.5 MB
[runlim] sample:		69.4 time, 70.6 real, 3646.5 MB
[runlim] sample:		79.4 time, 80.6 real, 3728.4 MB
[runlim] sample:		89.4 time, 90.6 real, 4027.7 MB
[runlim] sample:		99.4 time, 100.6 real, 4313.8 MB
[runlim] sample:		109.4 time, 110.6 real, 4583.8 MB
[runlim] sample:		119.4 time, 120.6 real, 4797.7 MB
[runlim] sample:		129.3 time, 130.6 real, 5028.0 MB
[runlim] sample:		139.3 time, 140.6 real, 5238.2 MB
[runlim] sample:		149.3 time, 150.6 real, 5504.7 MB
[runlim] sample:		159.3 time, 160.6 real, 5720.5 MB
[runlim] sample:		169.3 time, 170.6 real, 5784.4 MB
[runlim] sample:		179.3 time, 180.6 real, 5884.6 MB
[runlim] sample:		189.3 time, 190.6 real, 6036.5 MB
[runlim] sample:		199.2 time, 200.6 real, 6079.7 MB
[runlim] sample:		209.2 time, 210.6 real, 6208.1 MB
[runlim] sample:		219.2 time, 220.6 real, 6562.7 MB
[runlim] sample:		8.9 time, 230.6 real, 557.1 MB
[runlim] sample:		18.9 time, 240.6 real, 1173.4 MB
[runlim] sample:		28.9 time, 250.6 real, 1798.8 MB
[runlim] sample:		38.9 time, 260.6 real, 2381.5 MB
[runlim] sample:		48.8 time, 270.6 real, 2910.5 MB
[runlim] sample:		58.8 time, 280.6 real, 3370.5 MB
[runlim] sample:		68.8 time, 290.6 real, 3638.6 MB
[runlim] sample:		78.8 time, 300.6 real, 3708.5 MB
[runlim] sample:		88.8 time, 310.6 real, 4009.4 MB
[runlim] sample:		98.8 time, 320.6 real, 4289.4 MB
[runlim] sample:		108.8 time, 330.6 real, 4569.4 MB
[runlim] sample:		118.8 time, 340.6 real, 4777.5 MB
[runlim] sample:		128.7 time, 350.6 real, 5007.3 MB
[runlim] sample:		138.7 time, 360.6 real, 5215.3 MB
[runlim] sample:		148.7 time, 370.6 real, 5481.4 MB
[runlim] sample:		158.7 time, 380.6 real, 5657.4 MB
[runlim] sample:		168.7 time, 390.6 real, 5769.3 MB
[runlim] sample:		178.7 time, 400.6 real, 5868.1 MB
[runlim] sample:		188.7 time, 410.6 real, 6020.2 MB
[runlim] sample:		198.6 time, 420.6 real, 6073.5 MB
[runlim] sample:		208.6 time, 430.6 real, 6186.5 MB
[runlim] sample:		218.6 time, 440.6 real, 6522.4 MB
[runlim] sample:		8.1 time, 450.6 real, 487.7 MB
[runlim] sample:		18.0 time, 460.6 real, 1169.2 MB
[runlim] sample:		28.0 time, 470.6 real, 1819.7 MB
[runlim] sample:		38.0 time, 480.6 real, 2427.7 MB
[runlim] sample:		48.0 time, 490.6 real, 2999.8 MB
[runlim] sample:		58.0 time, 500.6 real, 3393.3 MB
[runlim] sample:		68.0 time, 510.6 real, 3709.4 MB
[runlim] sample:		78.0 time, 520.6 real, 3811.4 MB
[runlim] sample:		88.0 time, 530.6 real, 4107.3 MB
[runlim] sample:		97.9 time, 540.6 real, 4386.4 MB
[runlim] sample:		107.9 time, 550.6 real, 4706.4 MB
[runlim] sample:		117.9 time, 560.6 real, 4894.5 MB
[runlim] sample:		127.9 time, 570.6 real, 5128.5 MB
[runlim] sample:		137.9 time, 580.6 real, 5344.8 MB
[runlim] sample:		147.9 time, 590.6 real, 5598.9 MB
[runlim] sample:		157.9 time, 600.6 real, 5766.9 MB
[runlim] sample:		167.8 time, 610.6 real, 5920.1 MB
[runlim] sample:		177.8 time, 620.6 real, 6024.2 MB
[runlim] sample:		187.8 time, 630.6 real, 6160.5 MB
[runlim] sample:		197.8 time, 640.6 real, 6240.5 MB
[runlim] sample:		207.8 time, 650.6 real, 6337.4 MB
[runlim] sample:		217.8 time, 660.6 real, 6574.8 MB
[runlim] sample:		8.8 time, 670.6 real, 549.1 MB
[runlim] sample:		18.8 time, 680.6 real, 1165.4 MB
[runlim] sample:		28.8 time, 690.6 real, 1795.1 MB
[runlim] sample:		38.8 time, 700.6 real, 2375.3 MB
[runlim] sample:		48.8 time, 710.6 real, 2917.1 MB
[runlim] sample:		58.7 time, 720.6 real, 3187.1 MB
[runlim] sample:		68.7 time, 730.6 real, 3443.7 MB
[runlim] sample:		78.7 time, 740.6 real, 3937.7 MB
[runlim] sample:		88.7 time, 750.6 real, 4396.2 MB
[runlim] sample:		98.7 time, 760.6 real, 4465.3 MB
[runlim] sample:		108.7 time, 770.6 real, 4469.2 MB
[runlim] sample:		118.7 time, 780.6 real, 4736.0 MB
[runlim] sample:		128.6 time, 790.6 real, 4835.7 MB
[runlim] sample:		138.6 time, 800.6 real, 4926.8 MB
[runlim] sample:		148.6 time, 810.6 real, 5017.0 MB
[runlim] sample:		158.6 time, 820.6 real, 5137.6 MB
[runlim] end:			Mon Sep 28 15:41:28 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		49743
[runlim] real:			830.24 seconds
[runlim] time:			220.30 seconds
[runlim] space:			6610.9 MB
[runlim] samples:		8296
