[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/6s329rb19.aig
[runlim] start:			Tue Sep 29 07:14:14 2015
[runlim] main pid:		26291
[runlim] sample:		9.6 time, 10.3 real, 622.7 MB
[runlim] sample:		19.6 time, 20.3 real, 1297.7 MB
[runlim] sample:		29.6 time, 30.3 real, 1854.9 MB
[runlim] sample:		39.6 time, 40.3 real, 2302.7 MB
[runlim] sample:		49.5 time, 50.3 real, 2484.1 MB
[runlim] sample:		59.5 time, 60.3 real, 2834.1 MB
[runlim] sample:		69.5 time, 70.3 real, 3096.1 MB
[runlim] sample:		79.5 time, 80.3 real, 3214.2 MB
[runlim] sample:		89.5 time, 90.3 real, 3460.0 MB
[runlim] sample:		99.5 time, 100.3 real, 3702.1 MB
[runlim] sample:		109.4 time, 110.3 real, 3836.2 MB
[runlim] sample:		119.4 time, 120.3 real, 3892.3 MB
[runlim] sample:		129.4 time, 130.3 real, 4062.9 MB
[runlim] sample:		139.4 time, 140.3 real, 4226.7 MB
[runlim] sample:		149.4 time, 150.3 real, 4653.7 MB
[runlim] sample:		159.3 time, 160.3 real, 5031.7 MB
[runlim] sample:		169.3 time, 170.3 real, 5442.3 MB
[runlim] sample:		179.3 time, 180.3 real, 5721.4 MB
[runlim] sample:		189.3 time, 190.3 real, 5888.3 MB
[runlim] sample:		199.3 time, 200.3 real, 5904.1 MB
[runlim] sample:		209.3 time, 210.3 real, 5925.5 MB
[runlim] sample:		219.2 time, 220.3 real, 5941.5 MB
[runlim] sample:		229.2 time, 230.3 real, 6267.2 MB
[runlim] sample:		236.5 time, 241.2 real, 6489.6 MB
terminate called after throwing an instance of 'Minisat::OutOfMemoryException'
[runlim] sample:		2.5 time, 251.2 real, 167.4 MB
[runlim] sample:		12.5 time, 261.2 real, 853.4 MB
[runlim] sample:		22.5 time, 271.2 real, 1461.8 MB
[runlim] sample:		32.5 time, 281.2 real, 1959.0 MB
[runlim] sample:		42.5 time, 291.2 real, 2366.9 MB
[runlim] sample:		52.5 time, 301.2 real, 2574.9 MB
[runlim] sample:		62.4 time, 311.2 real, 2927.8 MB
[runlim] sample:		72.4 time, 321.2 real, 3119.6 MB
[runlim] sample:		82.4 time, 331.2 real, 3278.8 MB
[runlim] sample:		92.4 time, 341.2 real, 3520.8 MB
[runlim] sample:		102.4 time, 351.2 real, 3759.8 MB
[runlim] sample:		112.3 time, 361.2 real, 3850.8 MB
[runlim] sample:		122.3 time, 371.2 real, 3962.2 MB
[runlim] sample:		132.3 time, 381.2 real, 4104.1 MB
[runlim] sample:		142.3 time, 391.2 real, 4264.3 MB
[runlim] sample:		152.3 time, 401.2 real, 4710.2 MB
[runlim] sample:		162.3 time, 411.2 real, 5082.5 MB
[runlim] sample:		172.2 time, 421.2 real, 5494.2 MB
[runlim] sample:		182.2 time, 431.2 real, 5755.3 MB
[runlim] sample:		192.2 time, 441.2 real, 5862.1 MB
[runlim] sample:		202.2 time, 451.2 real, 5864.6 MB
[runlim] sample:		212.2 time, 461.2 real, 5922.6 MB
[runlim] sample:		222.2 time, 471.2 real, 5982.6 MB
[runlim] sample:		232.2 time, 481.2 real, 6045.7 MB
[runlim] sample:		242.2 time, 491.2 real, 6167.2 MB
[runlim] sample:		252.1 time, 501.2 real, 6249.6 MB
[runlim] sample:		262.1 time, 511.2 real, 6500.6 MB
Fatal error: out of memory.
[runlim] sample:		6.4 time, 521.2 real, 495.2 MB
[runlim] sample:		16.4 time, 531.2 real, 1179.0 MB
[runlim] sample:		26.4 time, 541.2 real, 1759.0 MB
[runlim] sample:		36.4 time, 551.2 real, 2249.5 MB
[runlim] sample:		46.4 time, 561.2 real, 2563.6 MB
[runlim] sample:		56.4 time, 571.2 real, 2836.2 MB
[runlim] sample:		66.3 time, 581.2 real, 3136.2 MB
[runlim] sample:		76.3 time, 591.2 real, 3276.0 MB
[runlim] sample:		86.3 time, 601.2 real, 3542.1 MB
[runlim] sample:		96.3 time, 611.2 real, 3792.1 MB
[runlim] sample:		106.3 time, 621.2 real, 4014.2 MB
[runlim] sample:		116.2 time, 631.2 real, 4070.1 MB
[runlim] sample:		126.2 time, 641.2 real, 4197.8 MB
[runlim] sample:		136.2 time, 651.2 real, 4338.8 MB
[runlim] sample:		146.2 time, 661.2 real, 4609.3 MB
[runlim] sample:		156.2 time, 671.2 real, 5072.1 MB
[runlim] sample:		166.2 time, 681.2 real, 5474.4 MB
[runlim] sample:		176.2 time, 691.2 real, 5551.3 MB
[runlim] sample:		186.1 time, 701.2 real, 5572.8 MB
[runlim] sample:		196.1 time, 711.2 real, 5583.2 MB
[runlim] sample:		206.1 time, 721.2 real, 5593.5 MB
[runlim] sample:		216.1 time, 731.2 real, 5638.4 MB
[runlim] sample:		226.1 time, 741.2 real, 6027.2 MB
[runlim] sample:		236.1 time, 751.2 real, 6095.0 MB
[runlim] sample:		246.0 time, 761.2 real, 6095.2 MB
[runlim] sample:		256.0 time, 771.2 real, 6095.2 MB
[runlim] sample:		266.0 time, 781.2 real, 6095.3 MB
[runlim] sample:		276.0 time, 791.2 real, 6095.3 MB
[runlim] sample:		286.0 time, 801.2 real, 6100.0 MB
[runlim] sample:		295.9 time, 811.2 real, 6101.8 MB
[runlim] sample:		305.9 time, 821.2 real, 6102.8 MB
[runlim] sample:		315.9 time, 831.2 real, 6105.8 MB
[runlim] sample:		325.9 time, 841.2 real, 6109.5 MB
[runlim] sample:		335.9 time, 851.2 real, 6110.0 MB
[runlim] sample:		345.9 time, 861.2 real, 6142.4 MB
[runlim] sample:		355.9 time, 871.2 real, 6270.3 MB
[runlim] sample:		365.9 time, 881.2 real, 6283.2 MB
[runlim] sample:		375.8 time, 891.2 real, 6283.5 MB
[runlim] sample:		385.8 time, 901.2 real, 6285.5 MB
[runlim] sample:		395.8 time, 911.2 real, 6293.0 MB
[runlim] sample:		405.8 time, 921.2 real, 6299.3 MB
[runlim] sample:		415.8 time, 931.2 real, 6307.3 MB
[runlim] sample:		425.8 time, 941.2 real, 6356.3 MB
[runlim] sample:		435.7 time, 951.2 real, 6397.0 MB
[runlim] sample:		445.7 time, 961.2 real, 6421.4 MB
[runlim] sample:		455.7 time, 971.2 real, 6439.5 MB
[runlim] sample:		465.7 time, 981.2 real, 6453.7 MB
[runlim] sample:		475.7 time, 991.2 real, 6465.7 MB
[runlim] sample:		485.7 time, 1001.2 real, 6475.9 MB
[runlim] sample:		495.6 time, 1011.2 real, 6487.9 MB
[runlim] sample:		505.6 time, 1021.2 real, 6512.2 MB
[runlim] sample:		515.6 time, 1031.2 real, 6556.3 MB
[runlim] sample:		525.6 time, 1041.2 real, 6573.6 MB
[runlim] sample:		535.6 time, 1051.2 real, 6591.1 MB
[runlim] sample:		545.6 time, 1061.2 real, 6604.6 MB
Fatal error: exception Out of memory
[runlim] end:			Tue Sep 29 07:32:04 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		53461
[runlim] real:			1070.90 seconds
[runlim] time:			555.05 seconds
[runlim] space:			6623.6 MB
[runlim] samples:		10696
