[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/oski15a01b03s.aig
[runlim] start:			Mon Sep 28 15:45:06 2015
[runlim] main pid:		24253
[runlim] sample:		9.6 time, 10.4 real, 627.0 MB
[runlim] sample:		19.6 time, 20.4 real, 1223.4 MB
[runlim] sample:		29.6 time, 30.4 real, 1846.5 MB
[runlim] sample:		39.6 time, 40.4 real, 2447.0 MB
[runlim] sample:		49.6 time, 50.4 real, 2924.7 MB
[runlim] sample:		59.6 time, 60.4 real, 3428.9 MB
[runlim] sample:		69.6 time, 70.4 real, 3660.9 MB
[runlim] sample:		79.5 time, 80.4 real, 3748.8 MB
[runlim] sample:		89.5 time, 90.4 real, 4034.6 MB
[runlim] sample:		99.5 time, 100.4 real, 4322.8 MB
[runlim] sample:		109.5 time, 110.4 real, 4588.8 MB
[runlim] sample:		119.5 time, 120.4 real, 4806.7 MB
[runlim] sample:		129.5 time, 130.4 real, 5034.7 MB
[runlim] sample:		139.5 time, 140.4 real, 5244.6 MB
[runlim] sample:		149.5 time, 150.4 real, 5506.6 MB
[runlim] sample:		159.5 time, 160.4 real, 5722.7 MB
[runlim] sample:		169.4 time, 170.4 real, 5786.6 MB
[runlim] sample:		179.4 time, 180.4 real, 5886.0 MB
[runlim] sample:		189.4 time, 190.4 real, 6012.7 MB
[runlim] sample:		199.4 time, 200.4 real, 6050.6 MB
[runlim] sample:		209.4 time, 210.4 real, 6284.7 MB
[runlim] sample:		0.6 time, 220.4 real, 96.3 MB
[runlim] sample:		10.6 time, 230.4 real, 706.8 MB
[runlim] sample:		20.6 time, 240.4 real, 1296.5 MB
[runlim] sample:		30.6 time, 250.4 real, 1891.3 MB
[runlim] sample:		40.5 time, 260.4 real, 2494.0 MB
[runlim] sample:		50.5 time, 270.4 real, 2935.5 MB
[runlim] sample:		60.5 time, 280.4 real, 3483.6 MB
[runlim] sample:		70.5 time, 290.4 real, 3671.4 MB
[runlim] sample:		80.5 time, 300.4 real, 3763.6 MB
[runlim] sample:		90.5 time, 310.4 real, 4060.4 MB
[runlim] sample:		100.5 time, 320.4 real, 4350.5 MB
[runlim] sample:		110.5 time, 330.4 real, 4614.2 MB
[runlim] sample:		120.5 time, 340.4 real, 4832.3 MB
[runlim] sample:		130.4 time, 350.4 real, 5058.3 MB
[runlim] sample:		140.4 time, 360.4 real, 5274.4 MB
[runlim] sample:		150.4 time, 370.4 real, 5534.4 MB
[runlim] sample:		160.4 time, 380.4 real, 5728.2 MB
[runlim] sample:		170.4 time, 390.4 real, 5796.2 MB
[runlim] sample:		180.4 time, 400.4 real, 5904.3 MB
[runlim] sample:		190.3 time, 410.4 real, 6018.2 MB
[runlim] sample:		200.3 time, 420.4 real, 6062.2 MB
[runlim] sample:		210.3 time, 430.4 real, 6297.0 MB
[runlim] sample:		1.8 time, 440.4 real, 127.7 MB
[runlim] sample:		11.8 time, 450.4 real, 811.0 MB
[runlim] sample:		21.8 time, 460.4 real, 1435.6 MB
[runlim] sample:		31.8 time, 470.4 real, 2039.5 MB
[runlim] sample:		41.8 time, 480.4 real, 2663.6 MB
[runlim] sample:		51.8 time, 490.4 real, 3060.7 MB
[runlim] sample:		61.8 time, 500.4 real, 3624.7 MB
[runlim] sample:		71.8 time, 510.4 real, 3760.7 MB
[runlim] sample:		81.8 time, 520.4 real, 3895.6 MB
[runlim] sample:		91.7 time, 530.4 real, 4204.7 MB
[runlim] sample:		101.7 time, 540.4 real, 4500.6 MB
[runlim] sample:		111.7 time, 550.4 real, 4770.7 MB
[runlim] sample:		121.7 time, 560.4 real, 4988.8 MB
[runlim] sample:		131.7 time, 570.4 real, 5214.8 MB
[runlim] sample:		141.7 time, 580.4 real, 5428.9 MB
[runlim] sample:		151.7 time, 590.4 real, 5691.3 MB
[runlim] sample:		161.6 time, 600.4 real, 5821.5 MB
[runlim] sample:		171.6 time, 610.4 real, 5981.3 MB
[runlim] sample:		181.6 time, 620.4 real, 6084.3 MB
[runlim] sample:		191.6 time, 630.4 real, 6224.1 MB
[runlim] sample:		201.6 time, 640.4 real, 6296.2 MB
[runlim] sample:		211.6 time, 650.4 real, 6403.0 MB
[runlim] sample:		1.1 time, 660.4 real, 107.0 MB
[runlim] sample:		11.0 time, 670.4 real, 748.6 MB
[runlim] sample:		21.0 time, 680.4 real, 1326.5 MB
[runlim] sample:		31.0 time, 690.4 real, 1923.8 MB
[runlim] sample:		41.0 time, 700.4 real, 2526.0 MB
[runlim] sample:		51.0 time, 710.4 real, 2939.0 MB
[runlim] sample:		61.0 time, 720.4 real, 3277.0 MB
[runlim] sample:		71.0 time, 730.4 real, 3607.9 MB
[runlim] sample:		81.0 time, 740.4 real, 4029.0 MB
[runlim] sample:		90.9 time, 750.4 real, 4464.6 MB
[runlim] sample:		100.9 time, 760.4 real, 4468.7 MB
[runlim] sample:		110.9 time, 770.4 real, 4687.9 MB
[runlim] sample:		120.9 time, 780.4 real, 4814.0 MB
[runlim] sample:		130.9 time, 790.4 real, 4914.0 MB
[runlim] sample:		140.9 time, 800.4 real, 4985.9 MB
[runlim] sample:		150.9 time, 810.4 real, 5121.9 MB
[runlim] sample:		160.9 time, 820.4 real, 5675.9 MB
[runlim] sample:		170.8 time, 830.4 real, 6210.3 MB
[runlim] sample:		180.8 time, 840.4 real, 6428.1 MB
[runlim] sample:		190.8 time, 850.4 real, 6428.6 MB
[runlim] sample:		200.8 time, 860.4 real, 6428.6 MB
[runlim] sample:		210.8 time, 870.4 real, 6428.8 MB
[runlim] sample:		220.8 time, 880.4 real, 6428.8 MB
[runlim] sample:		230.8 time, 890.4 real, 6428.8 MB
[runlim] sample:		240.8 time, 900.4 real, 6428.8 MB
[runlim] sample:		250.8 time, 910.4 real, 6428.8 MB
[runlim] sample:		260.7 time, 920.4 real, 6428.8 MB
[runlim] sample:		270.7 time, 930.4 real, 6429.1 MB
[runlim] sample:		280.7 time, 940.4 real, 6429.1 MB
[runlim] sample:		3.6 time, 950.4 real, 213.7 MB
[runlim] sample:		13.6 time, 960.4 real, 923.2 MB
[runlim] sample:		23.6 time, 970.4 real, 1538.3 MB
[runlim] sample:		33.6 time, 980.4 real, 2149.2 MB
[runlim] sample:		43.5 time, 990.4 real, 2763.3 MB
[runlim] sample:		53.6 time, 1000.4 real, 3143.5 MB
[runlim] sample:		63.5 time, 1010.4 real, 3704.4 MB
[runlim] sample:		73.5 time, 1020.4 real, 3768.4 MB
[runlim] sample:		83.5 time, 1030.4 real, 3989.5 MB
[runlim] sample:		93.5 time, 1040.4 real, 4257.5 MB
[runlim] sample:		103.5 time, 1050.4 real, 4557.5 MB
[runlim] sample:		113.5 time, 1060.4 real, 4807.9 MB
[runlim] sample:		123.5 time, 1070.4 real, 5039.8 MB
[runlim] sample:		133.5 time, 1080.4 real, 5255.8 MB
[runlim] sample:		143.4 time, 1090.4 real, 5484.4 MB
[runlim] sample:		153.4 time, 1100.4 real, 5722.5 MB
[runlim] sample:		163.4 time, 1110.4 real, 5936.1 MB
[runlim] sample:		173.4 time, 1120.4 real, 6007.3 MB
[runlim] sample:		183.4 time, 1130.4 real, 6109.2 MB
[runlim] sample:		193.4 time, 1140.4 real, 6263.6 MB
[runlim] sample:		203.4 time, 1150.4 real, 6309.2 MB
[runlim] sample:		213.3 time, 1160.4 real, 6443.8 MB
[runlim] end:			Mon Sep 28 16:04:32 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		69965
[runlim] real:			1166.97 seconds
[runlim] time:			286.80 seconds
[runlim] space:			6605.2 MB
[runlim] samples:		11665
