[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/oski15a01b19s.aig
[runlim] start:			Mon Sep 28 15:31:06 2015
[runlim] main pid:		21607
[runlim] sample:		9.6 time, 10.4 real, 624.3 MB
[runlim] sample:		19.6 time, 20.4 real, 1223.6 MB
[runlim] sample:		29.5 time, 30.4 real, 1846.3 MB
[runlim] sample:		39.5 time, 40.4 real, 2446.0 MB
[runlim] sample:		49.5 time, 50.4 real, 2917.2 MB
[runlim] sample:		59.5 time, 60.4 real, 3419.2 MB
[runlim] sample:		69.5 time, 70.4 real, 3647.1 MB
[runlim] sample:		79.5 time, 80.4 real, 3727.2 MB
[runlim] sample:		89.5 time, 90.4 real, 4024.3 MB
[runlim] sample:		99.4 time, 100.4 real, 4310.4 MB
[runlim] sample:		109.4 time, 110.4 real, 4580.3 MB
[runlim] sample:		119.4 time, 120.4 real, 4788.5 MB
[runlim] sample:		129.4 time, 130.4 real, 5016.3 MB
[runlim] sample:		139.4 time, 140.4 real, 5224.4 MB
[runlim] sample:		149.3 time, 150.4 real, 5486.4 MB
[runlim] sample:		159.3 time, 160.4 real, 5630.5 MB
[runlim] sample:		169.3 time, 170.4 real, 5782.4 MB
[runlim] sample:		179.3 time, 180.4 real, 5882.3 MB
[runlim] sample:		189.3 time, 190.4 real, 6014.4 MB
[runlim] sample:		199.3 time, 200.4 real, 6056.4 MB
[runlim] sample:		209.2 time, 210.4 real, 6185.5 MB
[runlim] sample:		219.2 time, 220.4 real, 6556.5 MB
Fatal error: out of memory.
[runlim] sample:		8.8 time, 230.4 real, 556.2 MB
[runlim] sample:		18.8 time, 240.4 real, 1174.3 MB
[runlim] sample:		28.8 time, 250.4 real, 1802.1 MB
[runlim] sample:		38.8 time, 260.4 real, 2384.3 MB
[runlim] sample:		48.8 time, 270.4 real, 2908.8 MB
[runlim] sample:		58.8 time, 280.4 real, 3370.6 MB
[runlim] sample:		68.8 time, 290.4 real, 3638.6 MB
[runlim] sample:		78.7 time, 300.4 real, 3702.8 MB
[runlim] sample:		88.7 time, 310.4 real, 4005.7 MB
[runlim] sample:		98.7 time, 320.4 real, 4288.6 MB
[runlim] sample:		108.7 time, 330.4 real, 4567.8 MB
[runlim] sample:		118.7 time, 340.4 real, 4771.8 MB
[runlim] sample:		128.6 time, 350.4 real, 5001.6 MB
[runlim] sample:		138.6 time, 360.4 real, 5211.7 MB
[runlim] sample:		148.6 time, 370.4 real, 5477.7 MB
[runlim] sample:		158.6 time, 380.4 real, 5627.8 MB
[runlim] sample:		168.6 time, 390.4 real, 5775.7 MB
[runlim] sample:		178.6 time, 400.4 real, 5877.6 MB
[runlim] sample:		188.5 time, 410.4 real, 6007.7 MB
[runlim] sample:		198.5 time, 420.4 real, 6056.3 MB
[runlim] sample:		208.5 time, 430.4 real, 6179.8 MB
[runlim] sample:		218.5 time, 440.4 real, 6544.4 MB
Fatal error: out of memory.
[runlim] sample:		8.5 time, 450.4 real, 534.3 MB
[runlim] sample:		18.5 time, 460.4 real, 1220.4 MB
[runlim] sample:		28.5 time, 470.4 real, 1844.2 MB
[runlim] sample:		38.5 time, 480.4 real, 2453.0 MB
[runlim] sample:		48.4 time, 490.4 real, 3010.0 MB
[runlim] sample:		58.4 time, 500.4 real, 3425.9 MB
[runlim] sample:		68.4 time, 510.4 real, 3739.9 MB
[runlim] sample:		78.4 time, 520.4 real, 3828.0 MB
[runlim] sample:		88.4 time, 530.4 real, 4120.1 MB
[runlim] sample:		98.3 time, 540.4 real, 4400.0 MB
[runlim] sample:		108.3 time, 550.4 real, 4709.9 MB
[runlim] sample:		118.3 time, 560.4 real, 4898.0 MB
[runlim] sample:		128.3 time, 570.4 real, 5128.7 MB
[runlim] sample:		138.3 time, 580.4 real, 5341.8 MB
[runlim] sample:		148.3 time, 590.4 real, 5591.8 MB
[runlim] sample:		158.3 time, 600.4 real, 5785.9 MB
[runlim] sample:		168.2 time, 610.4 real, 5937.8 MB
[runlim] sample:		178.2 time, 620.4 real, 6021.9 MB
[runlim] sample:		188.2 time, 630.4 real, 6150.3 MB
[runlim] sample:		198.2 time, 640.4 real, 6231.0 MB
[runlim] sample:		208.2 time, 650.4 real, 6314.6 MB
[runlim] sample:		218.2 time, 660.4 real, 6541.8 MB
Fatal error: out of memory.
[runlim] end:			Mon Sep 28 15:42:08 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		33077
[runlim] real:			662.14 seconds
[runlim] time:			220.12 seconds
[runlim] space:			6606.9 MB
[runlim] samples:		6617
