[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.iproverdeephc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s119.aig
[runlim] start:			Tue Sep 29 06:12:22 2015
[runlim] main pid:		26023
[runlim] sample:		9.6 time, 10.5 real, 658.1 MB
[runlim] sample:		19.6 time, 20.5 real, 1212.9 MB
[runlim] sample:		29.6 time, 30.5 real, 1497.6 MB
[runlim] sample:		39.6 time, 40.5 real, 1790.9 MB
[runlim] sample:		49.5 time, 50.5 real, 2041.2 MB
[runlim] sample:		59.5 time, 60.5 real, 2298.6 MB
[runlim] sample:		69.5 time, 70.5 real, 2464.4 MB
[runlim] sample:		79.5 time, 80.5 real, 2680.5 MB
[runlim] sample:		89.5 time, 90.5 real, 3100.4 MB
[runlim] sample:		99.5 time, 100.5 real, 3280.4 MB
[runlim] sample:		109.5 time, 110.5 real, 3608.3 MB
[runlim] sample:		119.4 time, 120.5 real, 3929.8 MB
[runlim] sample:		129.4 time, 130.5 real, 4255.1 MB
[runlim] sample:		139.4 time, 140.5 real, 4565.6 MB
[runlim] sample:		149.4 time, 150.5 real, 4838.5 MB
[runlim] sample:		159.4 time, 160.5 real, 5190.8 MB
[runlim] sample:		169.3 time, 170.5 real, 5494.4 MB
[runlim] sample:		179.3 time, 180.5 real, 5779.1 MB
[runlim] sample:		189.3 time, 190.5 real, 5897.7 MB
[runlim] sample:		199.3 time, 200.5 real, 5913.7 MB
[runlim] sample:		209.3 time, 210.5 real, 5926.9 MB
[runlim] sample:		219.3 time, 220.5 real, 6062.6 MB
[runlim] sample:		229.3 time, 230.5 real, 6173.4 MB
[runlim] sample:		239.2 time, 240.5 real, 6245.7 MB
[runlim] sample:		249.2 time, 250.5 real, 6377.9 MB
[runlim] sample:		259.2 time, 260.5 real, 6524.3 MB
Fatal error: exception Out of memory
[runlim] sample:		6.3 time, 270.5 real, 435.1 MB
[runlim] sample:		16.3 time, 280.5 real, 1082.1 MB
[runlim] sample:		26.2 time, 290.5 real, 1452.2 MB
[runlim] sample:		36.2 time, 300.5 real, 1698.1 MB
[runlim] sample:		46.2 time, 310.5 real, 1950.1 MB
[runlim] sample:		56.2 time, 320.5 real, 2204.1 MB
[runlim] sample:		66.2 time, 330.5 real, 2447.9 MB
[runlim] sample:		76.2 time, 340.5 real, 2572.1 MB
[runlim] sample:		86.2 time, 350.5 real, 2963.5 MB
[runlim] sample:		96.1 time, 360.5 real, 3233.4 MB
[runlim] sample:		106.1 time, 370.5 real, 3348.9 MB
[runlim] sample:		116.1 time, 380.5 real, 3604.8 MB
[runlim] sample:		126.1 time, 390.5 real, 3808.7 MB
[runlim] sample:		136.1 time, 400.5 real, 3952.3 MB
[runlim] sample:		146.1 time, 410.5 real, 4250.2 MB
[runlim] sample:		156.0 time, 420.5 real, 4476.8 MB
[runlim] sample:		166.0 time, 430.5 real, 4708.0 MB
[runlim] sample:		176.0 time, 440.5 real, 4822.1 MB
[runlim] sample:		186.0 time, 450.5 real, 5077.6 MB
[runlim] sample:		196.0 time, 460.5 real, 5259.9 MB
[runlim] sample:		206.0 time, 470.5 real, 5500.5 MB
[runlim] sample:		215.9 time, 480.5 real, 5632.7 MB
[runlim] sample:		225.9 time, 490.5 real, 5722.9 MB
[runlim] sample:		235.9 time, 500.5 real, 5877.1 MB
[runlim] sample:		245.9 time, 510.5 real, 5883.7 MB
[runlim] sample:		255.9 time, 520.5 real, 5892.1 MB
[runlim] sample:		265.9 time, 530.5 real, 5956.0 MB
[runlim] sample:		275.9 time, 540.5 real, 5959.1 MB
[runlim] sample:		285.8 time, 550.5 real, 6034.3 MB
[runlim] sample:		295.8 time, 560.5 real, 6180.7 MB
[runlim] sample:		305.8 time, 570.5 real, 6291.1 MB
[runlim] sample:		315.8 time, 580.5 real, 6454.2 MB
Fatal error: out of memory.
[runlim] sample:		2.0 time, 590.5 real, 164.2 MB
[runlim] sample:		12.0 time, 600.5 real, 868.7 MB
[runlim] sample:		22.0 time, 610.5 real, 1410.6 MB
[runlim] sample:		32.0 time, 620.5 real, 1656.6 MB
[runlim] sample:		42.0 time, 630.5 real, 1974.6 MB
[runlim] sample:		52.0 time, 640.5 real, 2179.6 MB
[runlim] sample:		61.9 time, 650.5 real, 2362.5 MB
[runlim] sample:		71.9 time, 660.5 real, 2457.5 MB
[runlim] sample:		81.9 time, 670.5 real, 2833.3 MB
[runlim] sample:		91.9 time, 680.5 real, 3195.1 MB
[runlim] sample:		101.9 time, 690.5 real, 3313.8 MB
[runlim] sample:		111.8 time, 700.5 real, 3532.9 MB
[runlim] sample:		121.8 time, 710.5 real, 3554.4 MB
[runlim] sample:		131.8 time, 720.5 real, 3673.3 MB
[runlim] sample:		141.8 time, 730.5 real, 3749.2 MB
[runlim] sample:		151.8 time, 740.5 real, 4113.6 MB
[runlim] sample:		161.8 time, 750.5 real, 4161.0 MB
[runlim] sample:		171.8 time, 760.5 real, 4236.9 MB
[runlim] sample:		181.7 time, 770.5 real, 4300.7 MB
[runlim] sample:		191.7 time, 780.5 real, 4339.9 MB
[runlim] sample:		201.7 time, 790.5 real, 4377.7 MB
[runlim] sample:		211.7 time, 800.5 real, 4733.7 MB
[runlim] sample:		221.7 time, 810.5 real, 4928.6 MB
[runlim] sample:		231.6 time, 820.5 real, 4957.7 MB
[runlim] sample:		241.6 time, 830.5 real, 5049.0 MB
[runlim] sample:		251.6 time, 840.5 real, 5101.5 MB
[runlim] sample:		261.6 time, 850.5 real, 5147.9 MB
[runlim] sample:		271.6 time, 860.5 real, 5176.2 MB
[runlim] sample:		281.6 time, 870.5 real, 5202.4 MB
[runlim] sample:		291.6 time, 880.5 real, 5224.7 MB
[runlim] sample:		301.5 time, 890.5 real, 5598.6 MB
[runlim] sample:		311.5 time, 900.5 real, 5874.8 MB
[runlim] sample:		321.5 time, 910.5 real, 5909.0 MB
[runlim] sample:		331.5 time, 920.5 real, 5953.7 MB
[runlim] sample:		341.5 time, 930.5 real, 5956.2 MB
[runlim] sample:		351.4 time, 940.5 real, 5956.4 MB
[runlim] sample:		361.4 time, 950.5 real, 5981.7 MB
[runlim] sample:		371.4 time, 960.5 real, 6005.9 MB
[runlim] sample:		381.4 time, 970.5 real, 6020.1 MB
[runlim] sample:		391.4 time, 980.5 real, 6022.1 MB
[runlim] sample:		401.4 time, 990.5 real, 6022.4 MB
[runlim] sample:		411.4 time, 1000.5 real, 6022.4 MB
[runlim] sample:		421.3 time, 1010.5 real, 6058.0 MB
[runlim] sample:		431.3 time, 1020.5 real, 6102.6 MB
[runlim] sample:		441.3 time, 1030.5 real, 6103.4 MB
[runlim] sample:		451.3 time, 1040.5 real, 6109.1 MB
[runlim] sample:		461.3 time, 1050.5 real, 6162.5 MB
[runlim] sample:		471.3 time, 1060.5 real, 6175.5 MB
[runlim] sample:		481.2 time, 1070.5 real, 6175.5 MB
[runlim] sample:		491.2 time, 1080.5 real, 6179.3 MB
[runlim] sample:		501.2 time, 1090.5 real, 6179.6 MB
[runlim] sample:		511.2 time, 1100.5 real, 6179.6 MB
[runlim] sample:		521.2 time, 1110.5 real, 6179.8 MB
[runlim] sample:		531.2 time, 1120.5 real, 6180.1 MB
[runlim] sample:		541.1 time, 1130.5 real, 6180.4 MB
[runlim] sample:		551.1 time, 1140.5 real, 6184.7 MB
[runlim] sample:		561.1 time, 1150.5 real, 6186.7 MB
[runlim] sample:		571.1 time, 1160.5 real, 6191.0 MB
[runlim] sample:		581.1 time, 1170.5 real, 6456.0 MB
Fatal error: exception Out of memory
[runlim] end:			Tue Sep 29 06:31:56 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		58707
[runlim] real:			1174.89 seconds
[runlim] time:			585.16 seconds
[runlim] space:			6593.0 MB
[runlim] samples:		11744
