[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/6s329rb20.aig
[runlim] start:			Tue Sep 29 07:15:42 2015
[runlim] main pid:		22941
[runlim] sample:		9.6 time, 10.5 real, 623.3 MB
[runlim] sample:		19.6 time, 20.5 real, 1300.4 MB
[runlim] sample:		29.6 time, 30.5 real, 1856.2 MB
[runlim] sample:		39.5 time, 40.5 real, 2302.1 MB
[runlim] sample:		49.5 time, 50.5 real, 2488.0 MB
[runlim] sample:		59.5 time, 60.5 real, 2840.2 MB
[runlim] sample:		69.5 time, 70.5 real, 3108.1 MB
[runlim] sample:		79.5 time, 80.5 real, 3241.4 MB
[runlim] sample:		89.5 time, 90.5 real, 3474.6 MB
[runlim] sample:		99.4 time, 100.5 real, 3717.0 MB
[runlim] sample:		109.4 time, 110.5 real, 3851.1 MB
[runlim] sample:		119.4 time, 120.5 real, 3909.1 MB
[runlim] sample:		129.4 time, 130.5 real, 4072.2 MB
[runlim] sample:		139.4 time, 140.5 real, 4228.1 MB
[runlim] sample:		149.3 time, 150.5 real, 4620.3 MB
[runlim] sample:		159.3 time, 160.5 real, 5011.3 MB
[runlim] sample:		169.3 time, 170.5 real, 5426.7 MB
[runlim] sample:		179.3 time, 180.5 real, 5724.1 MB
[runlim] sample:		189.3 time, 190.5 real, 5881.7 MB
[runlim] sample:		199.3 time, 200.5 real, 6026.5 MB
[runlim] sample:		209.3 time, 210.5 real, 6047.1 MB
[runlim] sample:		219.2 time, 220.5 real, 6061.2 MB
[runlim] sample:		229.2 time, 230.5 real, 6218.1 MB
[runlim] sample:		239.2 time, 240.5 real, 6571.3 MB
Fatal error: exception Out of memory
[runlim] sample:		9.5 time, 250.5 real, 616.5 MB
[runlim] sample:		19.5 time, 260.5 real, 1295.9 MB
[runlim] sample:		29.4 time, 270.5 real, 1853.1 MB
[runlim] sample:		39.4 time, 280.5 real, 2301.0 MB
[runlim] sample:		49.4 time, 290.5 real, 2485.2 MB
[runlim] sample:		59.4 time, 300.5 real, 2839.2 MB
[runlim] sample:		69.4 time, 310.5 real, 3107.2 MB
[runlim] sample:		79.4 time, 320.5 real, 3240.3 MB
[runlim] sample:		89.4 time, 330.5 real, 3476.6 MB
[runlim] sample:		99.3 time, 340.5 real, 3718.6 MB
[runlim] sample:		109.3 time, 350.5 real, 3854.5 MB
[runlim] sample:		119.3 time, 360.5 real, 3910.5 MB
[runlim] sample:		129.3 time, 370.5 real, 4072.4 MB
[runlim] sample:		139.3 time, 380.5 real, 4230.5 MB
[runlim] sample:		149.2 time, 390.5 real, 4616.4 MB
[runlim] sample:		159.2 time, 400.5 real, 5010.8 MB
[runlim] sample:		169.2 time, 410.5 real, 5426.1 MB
[runlim] sample:		179.2 time, 420.5 real, 5709.8 MB
[runlim] sample:		189.2 time, 430.5 real, 5788.1 MB
[runlim] sample:		199.2 time, 440.5 real, 5800.8 MB
[runlim] sample:		209.2 time, 450.5 real, 5838.7 MB
[runlim] sample:		219.2 time, 460.5 real, 5925.5 MB
[runlim] sample:		229.1 time, 470.5 real, 5932.0 MB
[runlim] sample:		239.1 time, 480.5 real, 6138.1 MB
[runlim] sample:		249.1 time, 490.5 real, 6268.6 MB
[runlim] sample:		259.1 time, 500.5 real, 6326.9 MB
Fatal error: out of memory.
[runlim] sample:		2.3 time, 510.5 real, 159.8 MB
[runlim] sample:		12.3 time, 520.5 real, 889.5 MB
[runlim] sample:		22.2 time, 530.5 real, 1532.6 MB
[runlim] sample:		32.2 time, 540.5 real, 2022.8 MB
[runlim] sample:		42.2 time, 550.5 real, 2496.7 MB
[runlim] sample:		52.2 time, 560.5 real, 2693.5 MB
[runlim] sample:		62.2 time, 570.5 real, 3069.5 MB
[runlim] sample:		72.2 time, 580.5 real, 3202.5 MB
[runlim] sample:		82.2 time, 590.5 real, 3441.6 MB
[runlim] sample:		92.1 time, 600.5 real, 3693.4 MB
[runlim] sample:		102.1 time, 610.5 real, 3939.4 MB
[runlim] sample:		112.1 time, 620.5 real, 4053.6 MB
[runlim] sample:		122.1 time, 630.5 real, 4109.0 MB
[runlim] sample:		132.1 time, 640.5 real, 4289.1 MB
[runlim] sample:		142.1 time, 650.5 real, 4469.0 MB
[runlim] sample:		152.0 time, 660.5 real, 4893.1 MB
[runlim] sample:		162.0 time, 670.5 real, 5274.6 MB
[runlim] sample:		172.0 time, 680.5 real, 5539.2 MB
[runlim] sample:		182.0 time, 690.5 real, 5567.3 MB
[runlim] sample:		192.0 time, 700.5 real, 5581.5 MB
[runlim] sample:		201.9 time, 710.5 real, 5594.0 MB
[runlim] sample:		211.9 time, 720.5 real, 5602.3 MB
[runlim] sample:		221.9 time, 730.5 real, 5923.8 MB
[runlim] sample:		231.9 time, 740.5 real, 6102.8 MB
[runlim] sample:		241.9 time, 750.5 real, 6102.8 MB
[runlim] sample:		251.9 time, 760.5 real, 6103.0 MB
[runlim] sample:		261.9 time, 770.5 real, 6103.3 MB
[runlim] sample:		271.9 time, 780.5 real, 6103.3 MB
[runlim] sample:		281.8 time, 790.5 real, 6104.6 MB
[runlim] sample:		291.8 time, 800.5 real, 6106.9 MB
[runlim] sample:		301.8 time, 810.5 real, 6107.9 MB
[runlim] sample:		311.8 time, 820.5 real, 6109.2 MB
[runlim] sample:		321.8 time, 830.5 real, 6113.1 MB
[runlim] sample:		331.8 time, 840.5 real, 6114.3 MB
[runlim] sample:		341.7 time, 850.5 real, 6115.2 MB
[runlim] sample:		351.7 time, 860.5 real, 6257.9 MB
[runlim] sample:		361.7 time, 870.5 real, 6279.3 MB
[runlim] sample:		371.7 time, 880.5 real, 6280.1 MB
[runlim] sample:		381.7 time, 890.5 real, 6281.6 MB
[runlim] sample:		391.6 time, 900.5 real, 6290.3 MB
[runlim] sample:		401.6 time, 910.5 real, 6297.3 MB
[runlim] sample:		411.6 time, 920.5 real, 6304.0 MB
[runlim] sample:		421.6 time, 930.5 real, 6350.8 MB
[runlim] sample:		431.6 time, 940.5 real, 6392.0 MB
[runlim] sample:		441.6 time, 950.5 real, 6417.0 MB
[runlim] sample:		451.6 time, 960.5 real, 6435.5 MB
[runlim] sample:		461.6 time, 970.5 real, 6450.2 MB
[runlim] sample:		471.5 time, 980.5 real, 6462.5 MB
[runlim] sample:		481.5 time, 990.5 real, 6473.6 MB
[runlim] sample:		491.5 time, 1000.5 real, 6483.4 MB
[runlim] sample:		501.5 time, 1010.5 real, 6508.8 MB
[runlim] sample:		511.5 time, 1020.5 real, 6548.5 MB
[runlim] sample:		521.5 time, 1030.5 real, 6564.7 MB
[runlim] sample:		531.4 time, 1040.5 real, 6581.4 MB
[runlim] sample:		541.4 time, 1050.5 real, 6594.6 MB
[runlim] sample:		551.4 time, 1060.5 real, 6609.9 MB
Fatal error: exception Out of memory
[runlim] end:			Tue Sep 29 07:33:26 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		53186
[runlim] real:			1064.61 seconds
[runlim] time:			555.27 seconds
[runlim] space:			6615.6 MB
[runlim] samples:		10641
