[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/all/selection/random/intel035.aig
[runlim] start:			Tue Sep 29 05:13:46 2015
[runlim] main pid:		25965
[runlim] sample:		9.3 time, 10.6 real, 644.9 MB
[runlim] sample:		19.3 time, 20.6 real, 962.4 MB
[runlim] sample:		29.3 time, 30.6 real, 1148.5 MB
[runlim] sample:		39.3 time, 40.6 real, 1250.7 MB
[runlim] sample:		49.3 time, 50.6 real, 1680.9 MB
[runlim] sample:		59.3 time, 60.6 real, 2064.4 MB
[runlim] sample:		69.2 time, 70.6 real, 2201.2 MB
[runlim] sample:		79.2 time, 80.6 real, 2565.7 MB
[runlim] sample:		89.2 time, 90.6 real, 2832.9 MB
[runlim] sample:		99.2 time, 100.6 real, 3144.5 MB
[runlim] sample:		109.2 time, 110.6 real, 3424.6 MB
[runlim] sample:		119.2 time, 120.6 real, 3805.5 MB
[runlim] sample:		129.1 time, 130.6 real, 4052.5 MB
[runlim] sample:		139.1 time, 140.6 real, 4266.0 MB
[runlim] sample:		149.1 time, 150.6 real, 4276.6 MB
[runlim] sample:		159.1 time, 160.6 real, 4363.9 MB
[runlim] sample:		169.1 time, 170.6 real, 4494.0 MB
[runlim] sample:		179.1 time, 180.6 real, 4752.7 MB
[runlim] sample:		189.0 time, 190.6 real, 4963.1 MB
[runlim] sample:		199.0 time, 200.6 real, 5117.8 MB
[runlim] sample:		209.0 time, 210.6 real, 5421.9 MB
[runlim] sample:		219.0 time, 220.6 real, 5684.8 MB
[runlim] sample:		229.0 time, 230.6 real, 5948.7 MB
[runlim] sample:		239.0 time, 240.6 real, 5990.7 MB
[runlim] sample:		248.9 time, 250.6 real, 6228.1 MB
[runlim] sample:		258.9 time, 260.6 real, 6415.6 MB
Fatal error: out of memory.
[runlim] sample:		1.1 time, 270.6 real, 109.6 MB
[runlim] sample:		11.1 time, 280.6 real, 741.9 MB
[runlim] sample:		21.1 time, 290.6 real, 989.4 MB
[runlim] sample:		31.1 time, 300.6 real, 1161.7 MB
[runlim] sample:		41.1 time, 310.6 real, 1331.5 MB
[runlim] sample:		51.1 time, 320.6 real, 1683.7 MB
[runlim] sample:		61.1 time, 330.6 real, 2005.3 MB
[runlim] sample:		71.0 time, 340.6 real, 2131.6 MB
[runlim] sample:		81.0 time, 350.6 real, 2329.2 MB
[runlim] sample:		91.0 time, 360.6 real, 2593.6 MB
[runlim] sample:		101.0 time, 370.6 real, 2904.0 MB
[runlim] sample:		111.0 time, 380.6 real, 3135.7 MB
[runlim] sample:		121.0 time, 390.6 real, 3341.6 MB
[runlim] sample:		130.9 time, 400.6 real, 3608.4 MB
[runlim] sample:		140.9 time, 410.6 real, 3785.0 MB
[runlim] sample:		150.9 time, 420.6 real, 3908.0 MB
[runlim] sample:		160.9 time, 430.6 real, 3931.0 MB
[runlim] sample:		170.9 time, 440.6 real, 3995.2 MB
[runlim] sample:		180.9 time, 450.6 real, 4148.5 MB
[runlim] sample:		190.9 time, 460.6 real, 4290.3 MB
[runlim] sample:		200.8 time, 470.6 real, 4599.9 MB
[runlim] sample:		210.8 time, 480.6 real, 4771.4 MB
[runlim] sample:		220.8 time, 490.6 real, 5068.6 MB
[runlim] sample:		230.8 time, 500.6 real, 5247.0 MB
[runlim] sample:		240.8 time, 510.6 real, 5382.8 MB
[runlim] sample:		250.8 time, 520.6 real, 5639.2 MB
[runlim] sample:		260.8 time, 530.6 real, 5791.2 MB
[runlim] sample:		270.7 time, 540.6 real, 6100.9 MB
[runlim] sample:		280.7 time, 550.6 real, 6253.0 MB
[runlim] sample:		290.7 time, 560.6 real, 6416.9 MB
[runlim] sample:		300.7 time, 570.6 real, 6639.1 MB
Fatal error: out of memory.
[runlim] sample:		9.0 time, 580.6 real, 644.5 MB
[runlim] sample:		19.0 time, 590.6 real, 962.6 MB
[runlim] sample:		29.0 time, 600.6 real, 1162.0 MB
[runlim] sample:		39.0 time, 610.6 real, 1263.6 MB
[runlim] sample:		49.0 time, 620.6 real, 1691.1 MB
[runlim] sample:		58.9 time, 630.6 real, 2128.7 MB
[runlim] sample:		68.9 time, 640.6 real, 2744.3 MB
[runlim] sample:		78.9 time, 650.6 real, 3092.1 MB
[runlim] sample:		88.9 time, 660.6 real, 3461.2 MB
[runlim] sample:		98.9 time, 670.6 real, 3656.3 MB
[runlim] sample:		108.9 time, 680.6 real, 3759.4 MB
[runlim] sample:		118.8 time, 690.6 real, 4033.0 MB
[runlim] sample:		128.8 time, 700.6 real, 4114.3 MB
[runlim] sample:		138.8 time, 710.6 real, 4389.5 MB
[runlim] sample:		148.8 time, 720.6 real, 4768.2 MB
[runlim] sample:		158.8 time, 730.6 real, 4865.9 MB
[runlim] sample:		168.8 time, 740.6 real, 5270.9 MB
[runlim] sample:		178.8 time, 750.6 real, 5661.9 MB
[runlim] sample:		188.7 time, 760.6 real, 5776.6 MB
[runlim] sample:		198.7 time, 770.6 real, 5915.1 MB
[runlim] sample:		208.7 time, 780.6 real, 5930.0 MB
[runlim] sample:		218.7 time, 790.6 real, 5934.5 MB
[runlim] sample:		228.7 time, 800.6 real, 5953.0 MB
[runlim] sample:		238.7 time, 810.6 real, 6003.2 MB
[runlim] sample:		248.7 time, 820.6 real, 6191.8 MB
[runlim] sample:		258.6 time, 830.6 real, 6246.5 MB
[runlim] sample:		268.6 time, 840.6 real, 6540.6 MB
[runlim] sample:		278.6 time, 850.6 real, 6605.4 MB
Fatal error: exception Out of memory
[runlim] end:			Tue Sep 29 05:27:59 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		42624
[runlim] real:			853.68 seconds
[runlim] time:			301.35 seconds
[runlim] space:			6648.9 MB
[runlim] samples:		8531
