[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/iimc/single.iimc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b74s.aig
[runlim] start:			Fri Sep 18 07:28:14 2015
[runlim] main pid:		6257
[runlim] sample:		9.9 time, 10.2 real, 236.8 MB
[runlim] sample:		19.9 time, 20.2 real, 259.7 MB
[runlim] sample:		29.9 time, 30.2 real, 281.9 MB
[runlim] sample:		39.8 time, 40.2 real, 311.5 MB
[runlim] sample:		49.8 time, 50.2 real, 311.5 MB
[runlim] sample:		59.8 time, 60.2 real, 311.7 MB
[runlim] sample:		69.8 time, 70.2 real, 311.7 MB
[runlim] sample:		79.8 time, 80.2 real, 319.7 MB
[runlim] sample:		89.8 time, 90.2 real, 789.4 MB
[runlim] sample:		99.8 time, 100.2 real, 790.5 MB
[runlim] sample:		109.8 time, 110.2 real, 807.9 MB
[runlim] sample:		119.8 time, 120.2 real, 1021.5 MB
[runlim] sample:		129.8 time, 130.2 real, 1021.5 MB
[runlim] sample:		141.3 time, 140.2 real, 1129.3 MB
[runlim] sample:		172.9 time, 150.2 real, 1729.6 MB
[runlim] sample:		197.8 time, 160.2 real, 1982.1 MB
[runlim] sample:		226.8 time, 170.2 real, 2089.8 MB
[runlim] sample:		249.7 time, 180.2 real, 2262.2 MB
[runlim] sample:		268.5 time, 190.2 real, 2369.2 MB
[runlim] sample:		297.5 time, 200.2 real, 3626.6 MB
[runlim] sample:		333.6 time, 210.2 real, 5444.1 MB
[runlim] sample:		373.2 time, 220.2 real, 5903.7 MB
[runlim] sample:		412.9 time, 230.2 real, 6105.5 MB
[runlim] sample:		452.5 time, 240.2 real, 6229.7 MB
[runlim] sample:		492.1 time, 250.2 real, 6431.7 MB
[runlim] sample:		531.7 time, 260.2 real, 6431.9 MB
[runlim] sample:		571.3 time, 270.2 real, 6437.7 MB
[runlim] sample:		611.0 time, 280.2 real, 6487.6 MB
[runlim] sample:		650.6 time, 290.2 real, 6535.3 MB
[runlim] sample:		690.2 time, 300.2 real, 6592.0 MB
[runlim] sample:		729.8 time, 310.2 real, 6596.0 MB
[runlim] sample:		769.5 time, 320.2 real, 6596.0 MB
[runlim] sample:		809.1 time, 330.2 real, 6596.0 MB
[runlim] sample:		848.7 time, 340.2 real, 6596.0 MB
[runlim] sample:		888.3 time, 350.2 real, 6598.0 MB
[runlim] sample:		928.0 time, 360.2 real, 6598.0 MB
[runlim] sample:		967.6 time, 370.2 real, 6600.0 MB
[runlim] sample:		1007.2 time, 380.2 real, 6525.2 MB
[runlim] sample:		1046.8 time, 390.2 real, 6593.9 MB
[runlim] sample:		1086.4 time, 400.2 real, 6593.9 MB
[runlim] sample:		1126.1 time, 410.2 real, 6595.9 MB
[runlim] sample:		1165.7 time, 420.2 real, 6595.9 MB
[runlim] sample:		1205.3 time, 430.2 real, 6595.9 MB
[runlim] sample:		1244.9 time, 440.2 real, 6595.9 MB
[runlim] sample:		1284.5 time, 450.2 real, 6596.8 MB
[runlim] sample:		1324.2 time, 460.2 real, 6596.8 MB
[runlim] sample:		1363.8 time, 470.2 real, 6596.8 MB
[runlim] sample:		1403.4 time, 480.2 real, 6596.8 MB
[runlim] sample:		1443.0 time, 490.2 real, 6598.8 MB
[runlim] sample:		1482.7 time, 500.2 real, 6600.6 MB
[runlim] sample:		1522.3 time, 510.2 real, 6602.6 MB
[runlim] sample:		1562.0 time, 520.2 real, 6602.6 MB
[runlim] sample:		1601.6 time, 530.2 real, 6602.6 MB
[runlim] sample:		1641.3 time, 540.2 real, 6602.6 MB
[runlim] sample:		1680.9 time, 550.2 real, 6737.2 MB
[runlim] sample:		1720.6 time, 560.2 real, 6661.6 MB
[runlim] sample:		1760.2 time, 570.2 real, 6662.3 MB
[runlim] sample:		1799.8 time, 580.2 real, 6662.3 MB
[runlim] sample:		1839.5 time, 590.2 real, 6662.3 MB
[runlim] sample:		1879.1 time, 600.2 real, 6662.3 MB
[runlim] sample:		1918.7 time, 610.2 real, 6662.3 MB
[runlim] sample:		1958.4 time, 620.2 real, 6662.3 MB
[runlim] sample:		1998.0 time, 630.2 real, 6662.3 MB
[runlim] sample:		2037.6 time, 640.2 real, 6662.3 MB
[runlim] sample:		2077.2 time, 650.2 real, 6662.3 MB
[runlim] sample:		2116.9 time, 660.2 real, 6662.6 MB
[runlim] sample:		2156.5 time, 670.2 real, 6662.6 MB
[runlim] sample:		2196.1 time, 680.2 real, 6662.6 MB
[runlim] sample:		2235.8 time, 690.2 real, 6662.7 MB
[runlim] sample:		2275.4 time, 700.2 real, 6662.7 MB
[runlim] sample:		2315.0 time, 710.2 real, 6662.7 MB
[runlim] sample:		2354.6 time, 720.2 real, 6662.7 MB
[runlim] sample:		2394.3 time, 730.2 real, 6662.7 MB
[runlim] sample:		2433.9 time, 740.2 real, 6662.7 MB
[runlim] sample:		2473.5 time, 750.2 real, 6662.7 MB
[runlim] sample:		2513.1 time, 760.2 real, 6662.7 MB
[runlim] sample:		2552.8 time, 770.2 real, 6664.7 MB
[runlim] sample:		2592.4 time, 780.2 real, 6664.7 MB
[runlim] sample:		2632.0 time, 790.2 real, 6664.7 MB
[runlim] sample:		2671.7 time, 800.2 real, 6664.9 MB
[runlim] sample:		2711.2 time, 810.2 real, 6664.9 MB
[runlim] sample:		2750.9 time, 820.2 real, 6665.2 MB
[runlim] sample:		2790.4 time, 830.2 real, 6665.2 MB
[runlim] sample:		2830.0 time, 840.2 real, 6665.4 MB
[runlim] sample:		2869.6 time, 850.2 real, 6665.4 MB
[runlim] sample:		2909.3 time, 860.2 real, 6665.6 MB
[runlim] sample:		2948.9 time, 870.2 real, 6665.6 MB
[runlim] sample:		2988.5 time, 880.2 real, 6665.8 MB
[runlim] sample:		3028.0 time, 890.2 real, 6666.1 MB
[runlim] sample:		3067.7 time, 900.2 real, 6666.1 MB
[runlim] sample:		3107.3 time, 910.2 real, 6666.1 MB
[runlim] sample:		3146.9 time, 920.2 real, 6666.2 MB
[runlim] sample:		3186.5 time, 930.2 real, 6666.2 MB
[runlim] sample:		3226.1 time, 940.2 real, 6666.4 MB
[runlim] sample:		3265.7 time, 950.2 real, 6666.4 MB
[runlim] sample:		3305.3 time, 960.2 real, 6666.4 MB
[runlim] sample:		3345.0 time, 970.2 real, 6666.7 MB
[runlim] sample:		3384.6 time, 980.2 real, 6666.7 MB
[runlim] sample:		3424.3 time, 990.2 real, 6684.2 MB
[runlim] sample:		3463.9 time, 1000.2 real, 6684.5 MB
[runlim] sample:		3503.5 time, 1010.2 real, 6684.5 MB
[runlim] sample:		3543.2 time, 1020.2 real, 6709.5 MB
[runlim] sample:		3582.8 time, 1030.2 real, 6841.3 MB
[runlim] sample:		3622.3 time, 1040.2 real, 6808.8 MB
[runlim] sample:		3661.9 time, 1050.2 real, 6808.8 MB
[runlim] sample:		3701.6 time, 1060.2 real, 6808.8 MB
[runlim] sample:		3741.2 time, 1070.2 real, 6808.8 MB
[runlim] sample:		3780.8 time, 1080.2 real, 6808.8 MB
[runlim] sample:		3820.4 time, 1090.2 real, 6808.8 MB
[runlim] sample:		3860.1 time, 1100.2 real, 6808.8 MB
[runlim] sample:		3899.7 time, 1110.2 real, 6808.8 MB
[runlim] sample:		3939.3 time, 1120.2 real, 6808.8 MB
[runlim] sample:		3978.9 time, 1130.2 real, 6809.1 MB
[runlim] sample:		4018.6 time, 1140.2 real, 6809.1 MB
[runlim] sample:		4058.2 time, 1150.2 real, 6809.3 MB
[runlim] sample:		4097.9 time, 1160.2 real, 6809.3 MB
[runlim] sample:		4137.5 time, 1170.2 real, 6809.8 MB
[runlim] sample:		4177.2 time, 1180.2 real, 6809.8 MB
[runlim] sample:		4216.8 time, 1190.2 real, 6809.8 MB
[runlim] sample:		4256.5 time, 1200.2 real, 6809.8 MB
[runlim] sample:		4296.1 time, 1210.2 real, 6809.8 MB
[runlim] sample:		4335.8 time, 1220.2 real, 6809.8 MB
[runlim] sample:		4375.4 time, 1230.2 real, 6722.8 MB
[runlim] sample:		4415.1 time, 1240.2 real, 6791.0 MB
[runlim] sample:		4454.7 time, 1250.2 real, 6791.0 MB
[runlim] sample:		4494.4 time, 1260.2 real, 6791.0 MB
[runlim] sample:		4534.0 time, 1270.2 real, 6791.0 MB
[runlim] sample:		4573.6 time, 1280.2 real, 6791.0 MB
[runlim] sample:		4613.3 time, 1290.2 real, 6791.0 MB
[runlim] sample:		4652.9 time, 1300.2 real, 6791.0 MB
[runlim] sample:		4692.6 time, 1310.2 real, 6791.0 MB
[runlim] sample:		4732.2 time, 1320.2 real, 6791.0 MB
[runlim] sample:		4771.8 time, 1330.2 real, 6791.0 MB
[runlim] sample:		4811.4 time, 1340.2 real, 6791.0 MB
[runlim] sample:		4851.1 time, 1350.2 real, 6791.0 MB
[runlim] sample:		4890.7 time, 1360.2 real, 6791.0 MB
[runlim] sample:		4930.4 time, 1370.2 real, 6792.2 MB
[runlim] sample:		4970.0 time, 1380.2 real, 6792.2 MB
[runlim] sample:		5009.6 time, 1390.2 real, 6792.2 MB
[runlim] sample:		5049.3 time, 1400.2 real, 6792.5 MB
[runlim] sample:		5088.9 time, 1410.2 real, 6792.5 MB
[runlim] sample:		5128.6 time, 1420.2 real, 6792.5 MB
[runlim] sample:		5168.2 time, 1430.2 real, 6792.7 MB
[runlim] sample:		5207.9 time, 1440.2 real, 6792.7 MB
[runlim] sample:		5247.5 time, 1450.2 real, 6793.0 MB
[runlim] sample:		5287.1 time, 1460.2 real, 6793.0 MB
[runlim] sample:		5326.8 time, 1470.2 real, 6793.0 MB
[runlim] sample:		5366.4 time, 1480.2 real, 6809.1 MB
[runlim] sample:		5406.1 time, 1490.2 real, 6809.4 MB
[runlim] sample:		5445.7 time, 1500.2 real, 6809.9 MB
[runlim] sample:		5485.4 time, 1510.2 real, 6810.1 MB
[runlim] sample:		5525.0 time, 1520.2 real, 6810.6 MB
[runlim] sample:		5564.6 time, 1530.2 real, 6811.4 MB
[runlim] sample:		5604.3 time, 1540.2 real, 6811.9 MB
[runlim] sample:		5643.9 time, 1550.2 real, 6812.7 MB
[runlim] sample:		5683.6 time, 1560.2 real, 6813.4 MB
[runlim] sample:		5723.2 time, 1570.2 real, 6813.7 MB
[runlim] sample:		5762.8 time, 1580.2 real, 6814.2 MB
[runlim] sample:		5802.5 time, 1590.2 real, 6815.0 MB
[runlim] sample:		5842.1 time, 1600.2 real, 6815.5 MB
[runlim] sample:		5881.8 time, 1610.2 real, 6816.0 MB
[runlim] sample:		5921.4 time, 1620.2 real, 6816.5 MB
[runlim] sample:		5961.1 time, 1630.2 real, 6817.0 MB
[runlim] sample:		6000.7 time, 1640.2 real, 6817.5 MB
[runlim] sample:		6040.4 time, 1650.2 real, 6818.1 MB
[runlim] sample:		6080.0 time, 1660.2 real, 6818.6 MB
[runlim] sample:		6119.7 time, 1670.2 real, 6819.1 MB
[runlim] sample:		6159.4 time, 1680.2 real, 6819.9 MB
[runlim] sample:		6199.0 time, 1690.2 real, 6820.1 MB
[runlim] sample:		6238.6 time, 1700.2 real, 6820.6 MB
[runlim] sample:		6278.3 time, 1710.2 real, 6821.9 MB
[runlim] sample:		6317.9 time, 1720.2 real, 6822.7 MB
[runlim] sample:		6357.6 time, 1730.2 real, 6823.2 MB
[runlim] sample:		6397.3 time, 1740.2 real, 6823.7 MB
[runlim] sample:		6436.9 time, 1750.2 real, 6824.2 MB
[runlim] sample:		6476.6 time, 1760.2 real, 6825.0 MB
[runlim] sample:		6516.2 time, 1770.2 real, 6825.2 MB
[runlim] sample:		6555.9 time, 1780.2 real, 6825.8 MB
[runlim] sample:		6595.5 time, 1790.2 real, 6826.3 MB
[runlim] sample:		6635.1 time, 1800.2 real, 6889.1 MB
[runlim] end:			Fri Sep 18 07:58:22 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		0
[runlim] real:			1808.86 seconds
[runlim] time:			6668.33 seconds
[runlim] space:			7001.0 MB
[runlim] samples:		18086
