[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.iprover
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s13.aig
[runlim] start:			Tue Sep 15 17:00:14 2015
[runlim] main pid:		4187
[runlim] sample:		6.6 time, 10.6 real, 304.8 MB
[runlim] sample:		16.6 time, 20.6 real, 585.2 MB
[runlim] sample:		26.6 time, 30.6 real, 690.4 MB
[runlim] sample:		36.6 time, 40.6 real, 699.8 MB
[runlim] sample:		46.6 time, 50.6 real, 741.3 MB
[runlim] sample:		56.5 time, 60.6 real, 771.1 MB
[runlim] sample:		66.5 time, 70.6 real, 779.4 MB
[runlim] sample:		76.5 time, 80.6 real, 787.4 MB
[runlim] sample:		86.5 time, 90.6 real, 791.4 MB
[runlim] sample:		96.5 time, 100.6 real, 797.7 MB
[runlim] sample:		106.5 time, 110.6 real, 801.7 MB
[runlim] sample:		116.5 time, 120.6 real, 827.4 MB
[runlim] sample:		126.5 time, 130.6 real, 849.0 MB
[runlim] sample:		136.5 time, 140.6 real, 878.8 MB
[runlim] sample:		146.4 time, 150.6 real, 889.3 MB
[runlim] sample:		156.4 time, 160.6 real, 900.4 MB
[runlim] sample:		166.4 time, 170.6 real, 908.4 MB
[runlim] sample:		176.4 time, 180.6 real, 914.4 MB
[runlim] sample:		186.4 time, 190.6 real, 920.4 MB
[runlim] sample:		196.4 time, 200.6 real, 928.4 MB
[runlim] sample:		206.3 time, 210.6 real, 934.2 MB
[runlim] sample:		216.3 time, 220.6 real, 942.2 MB
[runlim] sample:		226.3 time, 230.6 real, 948.2 MB
[runlim] sample:		236.3 time, 240.6 real, 954.2 MB
[runlim] sample:		246.3 time, 250.6 real, 958.2 MB
[runlim] sample:		256.3 time, 260.6 real, 964.2 MB
[runlim] sample:		266.3 time, 270.6 real, 873.9 MB
[runlim] sample:		276.3 time, 280.6 real, 884.1 MB
[runlim] sample:		286.3 time, 290.6 real, 894.1 MB
[runlim] sample:		296.3 time, 300.6 real, 903.1 MB
[runlim] sample:		306.3 time, 310.6 real, 909.1 MB
[runlim] sample:		316.2 time, 320.6 real, 917.1 MB
[runlim] sample:		326.2 time, 330.6 real, 925.1 MB
[runlim] sample:		336.2 time, 340.6 real, 932.2 MB
[runlim] sample:		346.2 time, 350.6 real, 938.2 MB
[runlim] sample:		356.2 time, 360.6 real, 946.2 MB
[runlim] sample:		366.2 time, 370.6 real, 950.2 MB
[runlim] sample:		376.2 time, 380.6 real, 956.3 MB
[runlim] sample:		386.2 time, 390.6 real, 962.3 MB
[runlim] sample:		396.1 time, 400.6 real, 968.3 MB
[runlim] sample:		406.1 time, 410.6 real, 972.3 MB
[runlim] sample:		416.1 time, 420.6 real, 977.0 MB
[runlim] sample:		426.1 time, 430.6 real, 983.0 MB
[runlim] sample:		436.1 time, 440.6 real, 870.1 MB
[runlim] sample:		446.1 time, 450.6 real, 880.3 MB
[runlim] sample:		456.1 time, 460.6 real, 890.4 MB
[runlim] sample:		466.1 time, 470.6 real, 896.4 MB
[runlim] sample:		476.1 time, 480.6 real, 903.4 MB
[runlim] sample:		486.1 time, 490.6 real, 909.4 MB
[runlim] sample:		496.1 time, 500.6 real, 917.4 MB
[runlim] sample:		506.0 time, 510.6 real, 923.4 MB
[runlim] sample:		516.0 time, 520.6 real, 927.4 MB
[runlim] sample:		526.0 time, 530.6 real, 932.5 MB
[runlim] sample:		536.0 time, 540.6 real, 936.5 MB
[runlim] sample:		546.0 time, 550.6 real, 942.5 MB
[runlim] sample:		556.0 time, 560.6 real, 948.5 MB
[runlim] sample:		566.0 time, 570.6 real, 952.5 MB
[runlim] sample:		576.0 time, 580.6 real, 956.5 MB
[runlim] sample:		586.0 time, 590.6 real, 962.5 MB
[runlim] sample:		595.9 time, 600.6 real, 968.5 MB
[runlim] sample:		605.9 time, 610.6 real, 976.5 MB
[runlim] sample:		615.9 time, 620.6 real, 981.2 MB
[runlim] sample:		625.9 time, 630.6 real, 936.0 MB
[runlim] sample:		635.9 time, 640.6 real, 963.1 MB
[runlim] sample:		645.9 time, 650.6 real, 1003.3 MB
[runlim] sample:		655.9 time, 660.6 real, 1013.3 MB
[runlim] sample:		665.9 time, 670.6 real, 1021.5 MB
[runlim] sample:		675.9 time, 680.6 real, 1031.5 MB
[runlim] sample:		685.9 time, 690.6 real, 1039.5 MB
[runlim] sample:		695.8 time, 700.6 real, 1048.6 MB
[runlim] sample:		705.8 time, 710.6 real, 1054.6 MB
[runlim] sample:		715.8 time, 720.6 real, 1062.8 MB
[runlim] sample:		725.8 time, 730.6 real, 1070.8 MB
[runlim] sample:		735.8 time, 740.6 real, 1076.8 MB
[runlim] sample:		745.8 time, 750.6 real, 1084.8 MB
[runlim] sample:		755.8 time, 760.6 real, 1090.8 MB
[runlim] sample:		765.8 time, 770.6 real, 1093.8 MB
[runlim] sample:		775.7 time, 780.6 real, 1100.8 MB
[runlim] sample:		785.7 time, 790.6 real, 967.3 MB
[runlim] sample:		795.7 time, 800.6 real, 967.3 MB
[runlim] sample:		805.7 time, 810.6 real, 1005.3 MB
[runlim] sample:		815.7 time, 820.6 real, 1013.3 MB
[runlim] sample:		825.7 time, 830.6 real, 1023.5 MB
[runlim] sample:		835.7 time, 840.6 real, 1031.5 MB
[runlim] sample:		845.7 time, 850.6 real, 1039.5 MB
[runlim] sample:		855.7 time, 860.6 real, 1048.6 MB
[runlim] sample:		865.7 time, 870.6 real, 1056.6 MB
[runlim] sample:		875.6 time, 880.6 real, 1064.8 MB
[runlim] sample:		885.6 time, 890.6 real, 1070.8 MB
[runlim] sample:		895.6 time, 900.6 real, 1076.8 MB
[runlim] sample:		9.3 time, 910.6 real, 366.2 MB
[runlim] sample:		19.3 time, 920.6 real, 644.0 MB
[runlim] sample:		29.3 time, 930.6 real, 782.8 MB
[runlim] sample:		39.2 time, 940.6 real, 793.7 MB
[runlim] sample:		49.2 time, 950.6 real, 904.9 MB
[runlim] sample:		59.2 time, 960.6 real, 913.7 MB
[runlim] sample:		69.2 time, 970.6 real, 926.9 MB
[runlim] sample:		79.2 time, 980.6 real, 964.5 MB
[runlim] sample:		89.2 time, 990.6 real, 972.5 MB
[runlim] sample:		99.2 time, 1000.6 real, 978.7 MB
[runlim] sample:		109.2 time, 1010.6 real, 1031.8 MB
[runlim] sample:		119.2 time, 1020.6 real, 1043.8 MB
[runlim] sample:		129.2 time, 1030.6 real, 1036.4 MB
[runlim] sample:		139.2 time, 1040.6 real, 1044.4 MB
[runlim] sample:		149.2 time, 1050.6 real, 1054.5 MB
[runlim] sample:		159.1 time, 1060.6 real, 1061.0 MB
[runlim] sample:		169.1 time, 1070.6 real, 1069.3 MB
[runlim] sample:		179.1 time, 1080.6 real, 1076.3 MB
[runlim] sample:		189.1 time, 1090.6 real, 1082.5 MB
[runlim] sample:		199.1 time, 1100.6 real, 1090.4 MB
[runlim] sample:		209.1 time, 1110.6 real, 1097.1 MB
[runlim] sample:		219.1 time, 1120.6 real, 1103.9 MB
[runlim] sample:		229.1 time, 1130.6 real, 1112.4 MB
[runlim] sample:		239.1 time, 1140.6 real, 1119.7 MB
[runlim] sample:		249.1 time, 1150.6 real, 1032.8 MB
[runlim] sample:		259.0 time, 1160.6 real, 1071.8 MB
[runlim] sample:		269.0 time, 1170.6 real, 1079.8 MB
[runlim] sample:		279.0 time, 1180.6 real, 1087.8 MB
[runlim] sample:		289.0 time, 1190.6 real, 1096.0 MB
[runlim] sample:		299.0 time, 1200.6 real, 1106.0 MB
[runlim] sample:		309.0 time, 1210.6 real, 1112.0 MB
[runlim] sample:		319.0 time, 1220.6 real, 1118.0 MB
[runlim] sample:		329.0 time, 1230.6 real, 1123.2 MB
[runlim] sample:		339.0 time, 1240.6 real, 1127.2 MB
[runlim] sample:		349.0 time, 1250.6 real, 1131.4 MB
[runlim] sample:		358.9 time, 1260.6 real, 1137.4 MB
[runlim] sample:		368.9 time, 1270.6 real, 1143.4 MB
[runlim] sample:		378.9 time, 1280.6 real, 1149.4 MB
[runlim] sample:		388.9 time, 1290.6 real, 1153.4 MB
[runlim] sample:		398.9 time, 1300.6 real, 1158.2 MB
[runlim] sample:		408.9 time, 1310.6 real, 1162.2 MB
[runlim] sample:		418.9 time, 1320.6 real, 1166.2 MB
[runlim] sample:		428.9 time, 1330.6 real, 1044.1 MB
[runlim] sample:		438.9 time, 1340.6 real, 1048.1 MB
[runlim] sample:		448.9 time, 1350.6 real, 1084.9 MB
[runlim] sample:		458.8 time, 1360.6 real, 1090.9 MB
[runlim] sample:		468.8 time, 1370.6 real, 1095.8 MB
[runlim] sample:		478.8 time, 1380.6 real, 1103.0 MB
[runlim] sample:		488.8 time, 1390.6 real, 1107.4 MB
[runlim] sample:		498.8 time, 1400.6 real, 1113.4 MB
[runlim] sample:		508.8 time, 1410.6 real, 1137.8 MB
[runlim] sample:		518.8 time, 1420.6 real, 1145.8 MB
[runlim] sample:		528.8 time, 1430.6 real, 1159.8 MB
[runlim] sample:		538.8 time, 1440.6 real, 1200.0 MB
[runlim] sample:		548.8 time, 1450.6 real, 1208.3 MB
[runlim] sample:		558.7 time, 1460.6 real, 1217.0 MB
[runlim] sample:		568.7 time, 1470.6 real, 1225.0 MB
[runlim] sample:		578.7 time, 1480.6 real, 1235.1 MB
[runlim] sample:		588.7 time, 1490.6 real, 1242.1 MB
[runlim] sample:		598.7 time, 1500.6 real, 1250.1 MB
[runlim] sample:		608.7 time, 1510.6 real, 1258.3 MB
[runlim] sample:		618.7 time, 1520.6 real, 1264.3 MB
[runlim] sample:		628.6 time, 1530.6 real, 1270.3 MB
[runlim] sample:		638.6 time, 1540.6 real, 1275.3 MB
[runlim] sample:		648.6 time, 1550.6 real, 1283.3 MB
[runlim] sample:		658.6 time, 1560.6 real, 1287.3 MB
[runlim] sample:		668.6 time, 1570.6 real, 1293.8 MB
[runlim] sample:		678.6 time, 1580.6 real, 1299.8 MB
[runlim] sample:		688.6 time, 1590.6 real, 1161.3 MB
[runlim] sample:		698.6 time, 1600.6 real, 1161.3 MB
[runlim] sample:		708.6 time, 1610.6 real, 1201.3 MB
[runlim] sample:		718.6 time, 1620.6 real, 1209.3 MB
[runlim] sample:		728.5 time, 1630.6 real, 1216.5 MB
[runlim] sample:		738.5 time, 1640.6 real, 1222.5 MB
[runlim] sample:		748.5 time, 1650.6 real, 1230.5 MB
[runlim] sample:		758.5 time, 1660.6 real, 1238.5 MB
[runlim] sample:		768.5 time, 1670.6 real, 1245.6 MB
[runlim] sample:		778.5 time, 1680.6 real, 1251.6 MB
[runlim] sample:		788.5 time, 1690.6 real, 1257.8 MB
[runlim] sample:		798.5 time, 1700.6 real, 1265.8 MB
[runlim] sample:		808.5 time, 1710.6 real, 1271.8 MB
[runlim] sample:		818.5 time, 1720.6 real, 1277.8 MB
[runlim] sample:		828.5 time, 1730.6 real, 1283.8 MB
[runlim] sample:		838.4 time, 1740.6 real, 1287.8 MB
[runlim] sample:		848.4 time, 1750.6 real, 1292.3 MB
[runlim] sample:		858.4 time, 1760.6 real, 1300.3 MB
[runlim] sample:		868.4 time, 1770.6 real, 1304.3 MB
[runlim] sample:		878.4 time, 1780.6 real, 1308.3 MB
[runlim] sample:		888.4 time, 1790.6 real, 1312.3 MB
[runlim] sample:		898.4 time, 1800.6 real, 1318.3 MB
[runlim] sample:		9.1 time, 1810.6 real, 366.9 MB
[runlim] sample:		19.1 time, 1820.6 real, 602.6 MB
[runlim] sample:		29.0 time, 1830.6 real, 746.5 MB
[runlim] sample:		39.0 time, 1840.6 real, 923.9 MB
[runlim] sample:		49.0 time, 1850.6 real, 999.0 MB
[runlim] sample:		59.0 time, 1860.6 real, 1091.2 MB
[runlim] sample:		69.0 time, 1870.6 real, 1274.4 MB
[runlim] sample:		79.0 time, 1880.6 real, 1470.1 MB
[runlim] sample:		89.0 time, 1890.6 real, 1593.3 MB
[runlim] sample:		99.0 time, 1900.6 real, 1611.8 MB
[runlim] sample:		109.0 time, 1910.6 real, 1652.4 MB
[runlim] sample:		119.0 time, 1920.6 real, 1669.8 MB
[runlim] sample:		128.9 time, 1930.6 real, 1755.4 MB
[runlim] sample:		138.9 time, 1940.6 real, 1879.7 MB
[runlim] sample:		148.9 time, 1950.6 real, 2021.0 MB
[runlim] sample:		158.9 time, 1960.6 real, 2199.3 MB
[runlim] sample:		168.9 time, 1970.6 real, 2252.8 MB
[runlim] sample:		178.9 time, 1980.6 real, 1860.4 MB
[runlim] sample:		188.9 time, 1990.6 real, 2014.5 MB
[runlim] sample:		198.9 time, 2000.6 real, 2187.6 MB
[runlim] sample:		208.9 time, 2010.6 real, 2375.8 MB
[runlim] sample:		218.9 time, 2020.6 real, 2379.4 MB
[runlim] sample:		228.8 time, 2030.6 real, 2473.0 MB
[runlim] sample:		238.8 time, 2040.6 real, 1750.9 MB
[runlim] sample:		248.8 time, 2050.6 real, 1783.3 MB
[runlim] sample:		258.8 time, 2060.6 real, 1819.9 MB
[runlim] sample:		268.8 time, 2070.6 real, 1864.1 MB
[runlim] sample:		278.8 time, 2080.6 real, 1969.1 MB
[runlim] sample:		288.8 time, 2090.6 real, 2116.7 MB
[runlim] sample:		298.8 time, 2100.6 real, 2265.4 MB
[runlim] sample:		308.8 time, 2110.6 real, 2437.6 MB
[runlim] sample:		318.8 time, 2120.6 real, 2599.6 MB
[runlim] sample:		328.7 time, 2130.6 real, 2763.6 MB
[runlim] sample:		338.7 time, 2140.6 real, 2909.6 MB
[runlim] sample:		348.7 time, 2150.6 real, 2967.0 MB
[runlim] sample:		358.7 time, 2160.6 real, 3021.2 MB
[runlim] sample:		368.7 time, 2170.6 real, 3052.9 MB
[runlim] sample:		378.7 time, 2180.6 real, 3083.1 MB
[runlim] sample:		388.7 time, 2190.6 real, 3107.6 MB
[runlim] sample:		398.7 time, 2200.6 real, 3133.8 MB
[runlim] sample:		408.6 time, 2210.6 real, 3165.8 MB
[runlim] sample:		418.6 time, 2220.6 real, 3195.8 MB
[runlim] sample:		428.6 time, 2230.6 real, 3229.8 MB
[runlim] sample:		438.6 time, 2240.6 real, 2150.4 MB
[runlim] sample:		448.6 time, 2250.6 real, 2219.7 MB
[runlim] sample:		458.6 time, 2260.6 real, 2272.4 MB
[runlim] sample:		468.6 time, 2270.6 real, 2387.0 MB
[runlim] sample:		478.6 time, 2280.6 real, 2535.1 MB
[runlim] sample:		488.5 time, 2290.6 real, 2685.1 MB
[runlim] sample:		498.6 time, 2300.6 real, 2812.1 MB
[runlim] sample:		508.5 time, 2310.6 real, 2964.1 MB
[runlim] sample:		518.5 time, 2320.6 real, 3140.1 MB
[runlim] sample:		528.5 time, 2330.6 real, 3281.5 MB
[runlim] sample:		538.5 time, 2340.6 real, 3415.7 MB
[runlim] sample:		548.5 time, 2350.6 real, 3565.7 MB
[runlim] sample:		558.5 time, 2360.6 real, 3715.7 MB
[runlim] sample:		568.5 time, 2370.6 real, 3867.7 MB
[runlim] sample:		578.5 time, 2380.6 real, 4033.7 MB
[runlim] sample:		588.5 time, 2390.6 real, 4177.6 MB
[runlim] sample:		598.4 time, 2400.6 real, 4327.7 MB
[runlim] sample:		608.4 time, 2410.6 real, 4487.7 MB
[runlim] sample:		618.4 time, 2420.6 real, 4639.7 MB
[runlim] sample:		628.4 time, 2430.6 real, 4801.7 MB
[runlim] sample:		638.4 time, 2440.6 real, 4957.7 MB
[runlim] sample:		648.4 time, 2450.6 real, 5109.7 MB
[runlim] sample:		658.4 time, 2460.6 real, 5259.7 MB
[runlim] sample:		668.4 time, 2470.6 real, 5393.6 MB
[runlim] sample:		678.4 time, 2480.6 real, 5538.1 MB
[runlim] end:			Tue Sep 15 17:41:40 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		149141
[runlim] real:			2486.80 seconds
[runlim] time:			898.99 seconds
[runlim] space:			5624.2 MB
[runlim] samples:		24861
