[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/all/selection/random/6s350rb46.aig
[runlim] start:			Tue Sep 29 06:09:38 2015
[runlim] main pid:		19183
[runlim] sample:		9.3 time, 10.4 real, 524.5 MB
[runlim] sample:		19.3 time, 20.4 real, 1016.7 MB
[runlim] sample:		29.2 time, 30.4 real, 1392.6 MB
[runlim] sample:		39.2 time, 40.4 real, 2228.4 MB
[runlim] sample:		49.2 time, 50.4 real, 3008.5 MB
[runlim] sample:		59.2 time, 60.4 real, 3818.5 MB
[runlim] sample:		69.2 time, 70.4 real, 4620.3 MB
[runlim] sample:		79.2 time, 80.4 real, 4992.4 MB
[runlim] sample:		89.2 time, 90.4 real, 5228.5 MB
[runlim] sample:		99.2 time, 100.4 real, 5694.1 MB
[runlim] sample:		109.1 time, 110.4 real, 6422.3 MB
[runlim] sample:		6.5 time, 120.4 real, 429.2 MB
[runlim] sample:		16.5 time, 130.4 real, 899.6 MB
[runlim] sample:		26.5 time, 140.4 real, 1229.8 MB
[runlim] sample:		36.5 time, 150.4 real, 2010.1 MB
[runlim] sample:		46.5 time, 160.4 real, 2808.1 MB
[runlim] sample:		56.4 time, 170.4 real, 3612.5 MB
[runlim] sample:		66.4 time, 180.4 real, 4464.5 MB
[runlim] sample:		76.4 time, 190.4 real, 4976.3 MB
[runlim] sample:		86.4 time, 200.4 real, 5164.4 MB
[runlim] sample:		96.4 time, 210.4 real, 5516.8 MB
[runlim] sample:		106.4 time, 220.4 real, 6242.1 MB
[runlim] sample:		3.9 time, 230.4 real, 365.3 MB
[runlim] sample:		13.9 time, 240.4 real, 769.8 MB
[runlim] sample:		23.9 time, 250.4 real, 1167.7 MB
[runlim] sample:		33.9 time, 260.4 real, 1784.2 MB
[runlim] sample:		43.9 time, 270.4 real, 2610.1 MB
[runlim] sample:		53.9 time, 280.4 real, 3397.7 MB
[runlim] sample:		63.9 time, 290.4 real, 4223.8 MB
[runlim] sample:		73.8 time, 300.4 real, 4945.6 MB
[runlim] sample:		83.8 time, 310.4 real, 5483.7 MB
[runlim] sample:		93.8 time, 320.4 real, 5660.8 MB
[runlim] sample:		103.8 time, 330.4 real, 6140.4 MB
[runlim] sample:		3.3 time, 340.4 real, 353.3 MB
[runlim] sample:		13.3 time, 350.4 real, 736.6 MB
[runlim] sample:		23.3 time, 360.4 real, 1149.1 MB
[runlim] sample:		33.3 time, 370.4 real, 1740.9 MB
[runlim] sample:		43.3 time, 380.4 real, 2554.9 MB
[runlim] sample:		53.3 time, 390.4 real, 3343.7 MB
[runlim] sample:		63.2 time, 400.4 real, 4166.3 MB
[runlim] sample:		73.2 time, 410.4 real, 4810.4 MB
[runlim] sample:		83.2 time, 420.4 real, 5068.5 MB
[runlim] sample:		93.2 time, 430.4 real, 5320.2 MB
[runlim] sample:		103.2 time, 440.4 real, 5991.1 MB
[runlim] sample:		0.4 time, 450.4 real, 147.6 MB
[runlim] sample:		10.4 time, 460.4 real, 588.5 MB
[runlim] sample:		20.4 time, 470.4 real, 1084.5 MB
[runlim] sample:		30.4 time, 480.4 real, 1502.6 MB
[runlim] sample:		40.4 time, 490.4 real, 2330.6 MB
[runlim] sample:		50.4 time, 500.4 real, 3108.1 MB
[runlim] sample:		60.4 time, 510.4 real, 3918.5 MB
[runlim] sample:		70.3 time, 520.4 real, 4708.5 MB
[runlim] sample:		80.3 time, 530.4 real, 5338.5 MB
[runlim] sample:		90.3 time, 540.4 real, 5568.7 MB
[runlim] sample:		100.3 time, 550.4 real, 5833.1 MB
[runlim] end:			Tue Sep 29 06:18:58 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		33565
[runlim] real:			560.21 seconds
[runlim] time:			112.49 seconds
[runlim] space:			6690.9 MB
[runlim] samples:		5598
