[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/oski15a01b41s.aig
[runlim] start:			Mon Sep 28 15:38:34 2015
[runlim] main pid:		1320
[runlim] sample:		9.5 time, 10.5 real, 616.4 MB
[runlim] sample:		19.5 time, 20.5 real, 1222.7 MB
[runlim] sample:		29.5 time, 30.5 real, 1839.2 MB
[runlim] sample:		39.5 time, 40.5 real, 2443.8 MB
[runlim] sample:		49.5 time, 50.5 real, 2921.0 MB
[runlim] sample:		59.4 time, 60.5 real, 3423.1 MB
[runlim] sample:		69.4 time, 70.5 real, 3643.2 MB
[runlim] sample:		79.4 time, 80.5 real, 3731.1 MB
[runlim] sample:		89.4 time, 90.5 real, 4026.5 MB
[runlim] sample:		99.4 time, 100.5 real, 4310.5 MB
[runlim] sample:		109.4 time, 110.5 real, 4582.5 MB
[runlim] sample:		119.3 time, 120.5 real, 4796.5 MB
[runlim] sample:		129.3 time, 130.5 real, 5022.5 MB
[runlim] sample:		139.3 time, 140.5 real, 5228.6 MB
[runlim] sample:		149.3 time, 150.5 real, 5496.6 MB
[runlim] sample:		159.3 time, 160.5 real, 5690.5 MB
[runlim] sample:		169.2 time, 170.5 real, 5782.6 MB
[runlim] sample:		179.2 time, 180.5 real, 5882.6 MB
[runlim] sample:		189.2 time, 190.5 real, 6022.4 MB
[runlim] sample:		199.2 time, 200.5 real, 6086.6 MB
[runlim] sample:		209.2 time, 210.5 real, 6198.6 MB
[runlim] sample:		219.2 time, 220.5 real, 6415.6 MB
Fatal error: out of memory.
[runlim] sample:		6.1 time, 230.5 real, 318.3 MB
[runlim] sample:		16.1 time, 240.5 real, 979.6 MB
[runlim] sample:		26.1 time, 250.5 real, 1633.4 MB
[runlim] sample:		36.1 time, 260.5 real, 2232.1 MB
[runlim] sample:		46.1 time, 270.5 real, 2823.5 MB
[runlim] sample:		56.0 time, 280.5 real, 3204.2 MB
[runlim] sample:		66.0 time, 290.5 real, 3618.5 MB
[runlim] sample:		76.0 time, 300.5 real, 3682.7 MB
[runlim] sample:		86.0 time, 310.5 real, 3931.7 MB
[runlim] sample:		96.0 time, 320.5 real, 4201.8 MB
[runlim] sample:		106.0 time, 330.5 real, 4497.7 MB
[runlim] sample:		116.0 time, 340.5 real, 4709.8 MB
[runlim] sample:		125.9 time, 350.5 real, 4943.6 MB
[runlim] sample:		135.9 time, 360.5 real, 5149.7 MB
[runlim] sample:		145.9 time, 370.5 real, 5395.7 MB
[runlim] sample:		155.9 time, 380.5 real, 5607.7 MB
[runlim] sample:		165.9 time, 390.5 real, 5751.0 MB
[runlim] sample:		175.8 time, 400.5 real, 5837.4 MB
[runlim] sample:		185.8 time, 410.5 real, 5970.5 MB
[runlim] sample:		195.8 time, 420.5 real, 6076.7 MB
[runlim] sample:		205.8 time, 430.5 real, 6142.8 MB
[runlim] sample:		215.8 time, 440.5 real, 6381.9 MB
Fatal error: out of memory.
[runlim] sample:		2.5 time, 450.5 real, 151.2 MB
[runlim] sample:		12.4 time, 460.5 real, 864.4 MB
[runlim] sample:		22.4 time, 470.5 real, 1470.5 MB
[runlim] sample:		32.4 time, 480.5 real, 2098.4 MB
[runlim] sample:		42.4 time, 490.5 real, 2701.1 MB
[runlim] sample:		52.4 time, 500.5 real, 3087.4 MB
[runlim] sample:		62.4 time, 510.5 real, 3663.4 MB
[runlim] sample:		72.3 time, 520.5 real, 3769.5 MB
[runlim] sample:		82.3 time, 530.5 real, 3925.4 MB
[runlim] sample:		92.3 time, 540.5 real, 4231.4 MB
[runlim] sample:		102.3 time, 550.5 real, 4533.4 MB
[runlim] sample:		112.3 time, 560.5 real, 4789.2 MB
[runlim] sample:		122.3 time, 570.5 real, 5018.0 MB
[runlim] sample:		132.2 time, 580.5 real, 5242.1 MB
[runlim] sample:		142.2 time, 590.5 real, 5462.1 MB
[runlim] sample:		152.2 time, 600.5 real, 5712.2 MB
[runlim] sample:		162.2 time, 610.5 real, 5916.0 MB
[runlim] sample:		172.2 time, 620.5 real, 5996.2 MB
[runlim] sample:		182.2 time, 630.5 real, 6100.1 MB
[runlim] sample:		192.2 time, 640.5 real, 6250.0 MB
[runlim] sample:		202.1 time, 650.5 real, 6308.1 MB
[runlim] sample:		212.1 time, 660.5 real, 6424.0 MB
Fatal error: out of memory.
[runlim] end:			Mon Sep 28 15:49:42 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		33396
[runlim] real:			668.68 seconds
[runlim] time:			223.12 seconds
[runlim] space:			6604.7 MB
[runlim] samples:		6682
