[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/oski15a01b15s.aig
[runlim] start:			Mon Sep 28 15:27:38 2015
[runlim] main pid:		15792
[runlim] sample:		9.2 time, 10.6 real, 578.5 MB
[runlim] sample:		19.1 time, 20.6 real, 1185.5 MB
[runlim] sample:		29.1 time, 30.6 real, 1820.3 MB
[runlim] sample:		39.1 time, 40.6 real, 2413.4 MB
[runlim] sample:		49.1 time, 50.6 real, 2927.6 MB
[runlim] sample:		59.1 time, 60.6 real, 3395.7 MB
[runlim] sample:		69.0 time, 70.6 real, 3686.3 MB
[runlim] sample:		79.0 time, 80.6 real, 3777.6 MB
[runlim] sample:		89.0 time, 90.6 real, 4025.6 MB
[runlim] sample:		99.0 time, 100.6 real, 4305.9 MB
[runlim] sample:		109.0 time, 110.6 real, 4583.9 MB
[runlim] sample:		119.0 time, 120.6 real, 4793.4 MB
[runlim] sample:		129.0 time, 130.6 real, 5021.8 MB
[runlim] sample:		138.9 time, 140.6 real, 5229.9 MB
[runlim] sample:		148.9 time, 150.6 real, 5487.9 MB
[runlim] sample:		158.9 time, 160.6 real, 5673.7 MB
[runlim] sample:		168.9 time, 170.6 real, 5815.8 MB
[runlim] sample:		178.9 time, 180.6 real, 5897.7 MB
[runlim] sample:		188.8 time, 190.6 real, 6023.6 MB
[runlim] sample:		198.8 time, 200.6 real, 6169.8 MB
[runlim] sample:		208.8 time, 210.6 real, 6207.7 MB
[runlim] sample:		218.8 time, 220.6 real, 6401.8 MB
Fatal error: out of memory.
[runlim] sample:		1.8 time, 230.6 real, 125.3 MB
[runlim] sample:		11.8 time, 240.6 real, 808.5 MB
[runlim] sample:		21.8 time, 250.6 real, 1366.0 MB
[runlim] sample:		31.8 time, 260.6 real, 1967.9 MB
[runlim] sample:		41.7 time, 270.6 real, 2569.2 MB
[runlim] sample:		51.7 time, 280.6 real, 2986.4 MB
[runlim] sample:		61.7 time, 290.6 real, 3554.3 MB
[runlim] sample:		71.7 time, 300.6 real, 3722.2 MB
[runlim] sample:		81.7 time, 310.6 real, 3864.4 MB
[runlim] sample:		91.7 time, 320.6 real, 4096.4 MB
[runlim] sample:		101.6 time, 330.6 real, 4390.9 MB
[runlim] sample:		111.6 time, 340.6 real, 4644.7 MB
[runlim] sample:		121.6 time, 350.6 real, 4864.7 MB
[runlim] sample:		131.6 time, 360.6 real, 5090.8 MB
[runlim] sample:		141.6 time, 370.6 real, 5304.8 MB
[runlim] sample:		151.6 time, 380.6 real, 5560.7 MB
[runlim] sample:		161.6 time, 390.6 real, 5770.7 MB
[runlim] sample:		171.5 time, 400.6 real, 5846.7 MB
[runlim] sample:		181.5 time, 410.6 real, 5942.8 MB
[runlim] sample:		191.5 time, 420.6 real, 6076.2 MB
[runlim] sample:		201.5 time, 430.6 real, 6184.6 MB
[runlim] sample:		211.5 time, 440.6 real, 6252.2 MB
[runlim] sample:		221.4 time, 450.6 real, 6478.5 MB
Fatal error: out of memory.
[runlim] sample:		5.4 time, 460.6 real, 264.3 MB
[runlim] sample:		15.4 time, 470.6 real, 949.1 MB
[runlim] sample:		25.4 time, 480.6 real, 1646.2 MB
[runlim] sample:		35.4 time, 490.6 real, 2262.5 MB
[runlim] sample:		45.4 time, 500.6 real, 2846.1 MB
[runlim] sample:		55.3 time, 510.6 real, 3232.4 MB
[runlim] sample:		65.3 time, 520.6 real, 3746.4 MB
[runlim] sample:		75.3 time, 530.6 real, 3838.8 MB
[runlim] sample:		85.3 time, 540.6 real, 4046.7 MB
[runlim] sample:		95.3 time, 550.6 real, 4320.7 MB
[runlim] sample:		105.2 time, 560.6 real, 4638.8 MB
[runlim] sample:		115.2 time, 570.6 real, 4850.6 MB
[runlim] sample:		125.2 time, 580.6 real, 5084.6 MB
[runlim] sample:		135.2 time, 590.6 real, 5296.7 MB
[runlim] sample:		145.2 time, 600.6 real, 5534.7 MB
[runlim] sample:		155.2 time, 610.6 real, 5768.7 MB
[runlim] sample:		165.2 time, 620.6 real, 5932.6 MB
[runlim] sample:		175.1 time, 630.6 real, 6014.6 MB
[runlim] sample:		185.1 time, 640.6 real, 6134.7 MB
[runlim] sample:		195.1 time, 650.6 real, 6260.6 MB
[runlim] sample:		205.1 time, 660.6 real, 6302.6 MB
[runlim] sample:		215.1 time, 670.6 real, 6536.6 MB
Fatal error: out of memory.
[runlim] end:			Mon Sep 28 15:38:52 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		33665
[runlim] real:			674.27 seconds
[runlim] time:			226.78 seconds
[runlim] space:			6657.3 MB
[runlim] samples:		6736
