[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/oski15/submission/single/oski15a01b57s.aig
[runlim] start:			Mon Sep 28 15:27:22 2015
[runlim] main pid:		24287
[runlim] sample:		9.1 time, 10.7 real, 578.3 MB
[runlim] sample:		19.1 time, 20.7 real, 1188.0 MB
[runlim] sample:		29.1 time, 30.7 real, 1817.5 MB
[runlim] sample:		39.1 time, 40.7 real, 2409.4 MB
[runlim] sample:		49.0 time, 50.7 real, 2909.8 MB
[runlim] sample:		59.0 time, 60.7 real, 3385.6 MB
[runlim] sample:		69.0 time, 70.7 real, 3645.7 MB
[runlim] sample:		79.0 time, 80.7 real, 3719.9 MB
[runlim] sample:		89.0 time, 90.7 real, 4010.2 MB
[runlim] sample:		99.0 time, 100.7 real, 4294.7 MB
[runlim] sample:		109.0 time, 110.7 real, 4570.8 MB
[runlim] sample:		119.0 time, 120.7 real, 4778.9 MB
[runlim] sample:		129.0 time, 130.7 real, 5006.7 MB
[runlim] sample:		139.0 time, 140.7 real, 5214.8 MB
[runlim] sample:		149.0 time, 150.7 real, 5480.8 MB
[runlim] sample:		159.0 time, 160.7 real, 5630.6 MB
[runlim] sample:		169.0 time, 170.7 real, 5780.8 MB
[runlim] sample:		179.0 time, 180.7 real, 5878.7 MB
[runlim] sample:		189.0 time, 190.7 real, 6012.8 MB
[runlim] sample:		199.0 time, 200.7 real, 6128.7 MB
[runlim] sample:		208.9 time, 210.7 real, 6184.7 MB
[runlim] sample:		218.9 time, 220.7 real, 6409.7 MB
Fatal error: out of memory.
[runlim] sample:		4.8 time, 230.7 real, 248.1 MB
[runlim] sample:		14.8 time, 240.7 real, 909.6 MB
[runlim] sample:		24.8 time, 250.7 real, 1563.6 MB
[runlim] sample:		34.8 time, 260.7 real, 2180.0 MB
[runlim] sample:		44.8 time, 270.7 real, 2768.1 MB
[runlim] sample:		54.8 time, 280.7 real, 3149.4 MB
[runlim] sample:		64.8 time, 290.7 real, 3605.3 MB
[runlim] sample:		74.7 time, 300.7 real, 3686.9 MB
[runlim] sample:		84.7 time, 310.7 real, 3907.3 MB
[runlim] sample:		94.7 time, 320.7 real, 4182.4 MB
[runlim] sample:		104.7 time, 330.7 real, 4476.3 MB
[runlim] sample:		114.7 time, 340.7 real, 4682.3 MB
[runlim] sample:		124.7 time, 350.7 real, 4920.3 MB
[runlim] sample:		134.7 time, 360.7 real, 5128.2 MB
[runlim] sample:		144.7 time, 370.7 real, 5376.2 MB
[runlim] sample:		154.7 time, 380.7 real, 5586.3 MB
[runlim] sample:		164.7 time, 390.7 real, 5762.1 MB
[runlim] sample:		174.7 time, 400.7 real, 5838.0 MB
[runlim] sample:		184.7 time, 410.7 real, 5949.2 MB
[runlim] sample:		194.7 time, 420.7 real, 6112.1 MB
[runlim] sample:		204.7 time, 430.7 real, 6154.0 MB
[runlim] sample:		214.7 time, 440.7 real, 6288.2 MB
Fatal error: out of memory.
[runlim] sample:		0.9 time, 450.7 real, 102.7 MB
[runlim] sample:		10.9 time, 460.7 real, 736.1 MB
[runlim] sample:		20.9 time, 470.7 real, 1377.1 MB
[runlim] sample:		30.9 time, 480.7 real, 1988.4 MB
[runlim] sample:		40.9 time, 490.7 real, 2598.5 MB
[runlim] sample:		50.9 time, 500.7 real, 3042.2 MB
[runlim] sample:		60.8 time, 510.7 real, 3556.2 MB
[runlim] sample:		70.8 time, 520.7 real, 3738.2 MB
[runlim] sample:		80.8 time, 530.7 real, 3880.2 MB
[runlim] sample:		90.8 time, 540.7 real, 4172.9 MB
[runlim] sample:		100.8 time, 550.7 real, 4464.9 MB
[runlim] sample:		110.8 time, 560.7 real, 4740.8 MB
[runlim] sample:		120.8 time, 570.7 real, 4960.9 MB
[runlim] sample:		130.8 time, 580.7 real, 5184.9 MB
[runlim] sample:		140.8 time, 590.7 real, 5396.8 MB
[runlim] sample:		150.8 time, 600.7 real, 5658.8 MB
[runlim] sample:		160.8 time, 610.7 real, 5862.8 MB
[runlim] sample:		170.8 time, 620.7 real, 5940.8 MB
[runlim] sample:		180.8 time, 630.7 real, 6042.7 MB
[runlim] sample:		190.8 time, 640.7 real, 6196.8 MB
[runlim] sample:		200.8 time, 650.7 real, 6242.7 MB
[runlim] sample:		210.7 time, 660.7 real, 6370.8 MB
Fatal error: out of memory.
[runlim] end:			Mon Sep 28 15:38:30 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		33385
[runlim] real:			668.74 seconds
[runlim] time:			223.94 seconds
[runlim] space:			6596.4 MB
[runlim] samples:		6680
