[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/6s387rb181.aig
[runlim] start:			Tue Sep 29 07:58:02 2015
[runlim] main pid:		25140
[runlim] sample:		9.5 time, 10.4 real, 385.1 MB
[runlim] sample:		19.5 time, 20.4 real, 982.3 MB
[runlim] sample:		29.5 time, 30.4 real, 1626.1 MB
[runlim] sample:		39.5 time, 40.4 real, 2241.3 MB
[runlim] sample:		49.5 time, 50.4 real, 2780.1 MB
[runlim] sample:		59.4 time, 60.4 real, 3155.6 MB
[runlim] sample:		69.4 time, 70.4 real, 3731.6 MB
[runlim] sample:		79.4 time, 80.4 real, 3981.6 MB
[runlim] sample:		89.4 time, 90.4 real, 4123.8 MB
[runlim] sample:		99.4 time, 100.4 real, 4409.7 MB
[runlim] sample:		109.3 time, 110.4 real, 4731.7 MB
[runlim] sample:		119.3 time, 120.4 real, 5025.7 MB
[runlim] sample:		129.3 time, 130.4 real, 5257.7 MB
[runlim] sample:		139.3 time, 140.4 real, 5539.7 MB
[runlim] sample:		149.3 time, 150.4 real, 5826.9 MB
[runlim] sample:		159.3 time, 160.4 real, 6059.5 MB
[runlim] sample:		169.3 time, 170.4 real, 6137.7 MB
[runlim] sample:		179.2 time, 180.4 real, 6319.1 MB
[runlim] sample:		189.2 time, 190.4 real, 6493.7 MB
Fatal error: out of memory.
[runlim] sample:		4.5 time, 200.4 real, 203.9 MB
[runlim] sample:		14.5 time, 210.4 real, 712.9 MB
[runlim] sample:		24.5 time, 220.4 real, 1302.0 MB
[runlim] sample:		34.4 time, 230.4 real, 1944.1 MB
[runlim] sample:		44.4 time, 240.4 real, 2543.9 MB
[runlim] sample:		54.4 time, 250.4 real, 3063.9 MB
[runlim] sample:		64.4 time, 260.4 real, 3444.6 MB
[runlim] sample:		74.4 time, 270.4 real, 3900.7 MB
[runlim] sample:		84.4 time, 280.4 real, 4050.8 MB
[runlim] sample:		94.4 time, 290.4 real, 4253.0 MB
[runlim] sample:		104.3 time, 300.4 real, 4559.0 MB
[runlim] sample:		114.3 time, 310.4 real, 4882.8 MB
[runlim] sample:		124.3 time, 320.4 real, 5130.9 MB
[runlim] sample:		134.3 time, 330.4 real, 5398.9 MB
[runlim] sample:		144.3 time, 340.4 real, 5676.9 MB
[runlim] sample:		154.2 time, 350.4 real, 5930.9 MB
[runlim] sample:		164.2 time, 360.4 real, 6089.2 MB
[runlim] sample:		174.2 time, 370.4 real, 6217.3 MB
[runlim] sample:		184.2 time, 380.4 real, 6408.7 MB
[runlim] sample:		194.2 time, 390.4 real, 6592.9 MB
Fatal error: out of memory.
[runlim] sample:		8.8 time, 400.4 real, 367.3 MB
[runlim] sample:		18.8 time, 410.4 real, 986.6 MB
[runlim] sample:		28.8 time, 420.4 real, 1637.2 MB
[runlim] sample:		38.8 time, 430.4 real, 2252.5 MB
[runlim] sample:		48.8 time, 440.4 real, 2799.5 MB
[runlim] sample:		58.7 time, 450.4 real, 3246.2 MB
[runlim] sample:		68.7 time, 460.4 real, 3742.1 MB
[runlim] sample:		78.7 time, 470.4 real, 4076.8 MB
[runlim] sample:		88.7 time, 480.4 real, 4228.9 MB
[runlim] sample:		98.7 time, 490.4 real, 4467.0 MB
[runlim] sample:		108.7 time, 500.4 real, 4786.8 MB
[runlim] sample:		118.6 time, 510.4 real, 5080.9 MB
[runlim] sample:		128.6 time, 520.4 real, 5326.9 MB
[runlim] sample:		138.6 time, 530.4 real, 5595.6 MB
[runlim] sample:		148.6 time, 540.4 real, 5851.6 MB
[runlim] sample:		158.6 time, 550.4 real, 5979.7 MB
[runlim] sample:		168.6 time, 560.4 real, 6164.9 MB
[runlim] sample:		178.6 time, 570.4 real, 6340.7 MB
[runlim] sample:		188.5 time, 580.4 real, 6546.8 MB
Fatal error: out of memory.
[runlim] end:			Tue Sep 29 08:07:47 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		29247
[runlim] real:			585.46 seconds
[runlim] time:			195.15 seconds
[runlim] space:			6619.7 MB
[runlim] samples:		5851
