[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.iproverhc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/bobtuint17neg.aig
[runlim] start:			Mon Sep 28 21:25:50 2015
[runlim] main pid:		23167
[runlim] sample:		9.7 time, 10.4 real, 242.4 MB
[runlim] sample:		19.7 time, 20.4 real, 406.5 MB
[runlim] sample:		29.7 time, 30.4 real, 622.8 MB
[runlim] sample:		39.6 time, 40.4 real, 795.8 MB
[runlim] sample:		49.6 time, 50.4 real, 997.0 MB
[runlim] sample:		59.6 time, 60.4 real, 1198.6 MB
[runlim] sample:		69.6 time, 70.4 real, 1335.4 MB
[runlim] sample:		79.6 time, 80.4 real, 1468.1 MB
[runlim] sample:		89.6 time, 90.4 real, 1650.0 MB
[runlim] sample:		99.6 time, 100.4 real, 1823.8 MB
[runlim] sample:		109.6 time, 110.4 real, 1990.3 MB
[runlim] sample:		119.5 time, 120.4 real, 2160.4 MB
[runlim] sample:		129.5 time, 130.4 real, 2326.1 MB
[runlim] sample:		139.5 time, 140.4 real, 2479.4 MB
[runlim] sample:		149.5 time, 150.4 real, 2656.5 MB
[runlim] sample:		159.5 time, 160.4 real, 2809.1 MB
[runlim] sample:		169.5 time, 170.4 real, 2915.7 MB
[runlim] sample:		179.5 time, 180.4 real, 2980.0 MB
[runlim] sample:		189.4 time, 190.4 real, 3127.6 MB
[runlim] sample:		199.4 time, 200.4 real, 3261.0 MB
[runlim] sample:		209.4 time, 210.4 real, 3403.4 MB
[runlim] sample:		219.4 time, 220.4 real, 3563.7 MB
[runlim] sample:		229.4 time, 230.4 real, 3709.0 MB
[runlim] sample:		239.4 time, 240.4 real, 3851.3 MB
[runlim] sample:		249.4 time, 250.4 real, 4003.7 MB
[runlim] sample:		259.3 time, 260.4 real, 4146.1 MB
[runlim] sample:		269.4 time, 270.4 real, 4320.4 MB
[runlim] sample:		279.3 time, 280.4 real, 4454.5 MB
[runlim] sample:		289.3 time, 290.4 real, 4592.6 MB
[runlim] sample:		299.3 time, 300.4 real, 4741.3 MB
[runlim] sample:		309.3 time, 310.4 real, 4882.2 MB
[runlim] sample:		319.3 time, 320.4 real, 5016.6 MB
[runlim] sample:		329.3 time, 330.4 real, 5180.2 MB
[runlim] sample:		339.3 time, 340.4 real, 5325.8 MB
[runlim] sample:		349.3 time, 350.4 real, 5466.2 MB
[runlim] sample:		359.2 time, 360.4 real, 5622.2 MB
[runlim] sample:		369.2 time, 370.4 real, 5761.3 MB
[runlim] sample:		379.2 time, 380.4 real, 5901.8 MB
[runlim] sample:		389.2 time, 390.4 real, 6038.4 MB
[runlim] sample:		399.2 time, 400.4 real, 6223.5 MB
[runlim] sample:		409.2 time, 410.4 real, 6317.9 MB
[runlim] sample:		419.2 time, 420.4 real, 6392.8 MB
[runlim] sample:		429.2 time, 430.4 real, 6427.3 MB
[runlim] sample:		439.1 time, 440.4 real, 6468.1 MB
[runlim] sample:		449.1 time, 450.4 real, 6532.5 MB
[runlim] sample:		459.1 time, 460.4 real, 6630.7 MB
[runlim] sample:		6.8 time, 470.4 real, 114.8 MB
[runlim] sample:		16.8 time, 480.4 real, 313.7 MB
[runlim] sample:		26.7 time, 490.4 real, 554.3 MB
[runlim] sample:		36.7 time, 500.4 real, 723.5 MB
[runlim] sample:		46.7 time, 510.4 real, 929.4 MB
[runlim] sample:		56.7 time, 520.4 real, 1141.1 MB
[runlim] sample:		66.7 time, 530.4 real, 1241.7 MB
[runlim] sample:		76.7 time, 540.4 real, 1447.2 MB
[runlim] sample:		86.7 time, 550.4 real, 1640.2 MB
[runlim] sample:		96.6 time, 560.4 real, 1842.8 MB
[runlim] sample:		106.6 time, 570.4 real, 2037.9 MB
[runlim] sample:		116.6 time, 580.4 real, 2251.1 MB
[runlim] sample:		126.6 time, 590.4 real, 2372.2 MB
[runlim] sample:		136.6 time, 600.4 real, 2477.8 MB
[runlim] sample:		146.6 time, 610.4 real, 2619.2 MB
[runlim] sample:		156.6 time, 620.4 real, 2771.6 MB
[runlim] sample:		166.6 time, 630.4 real, 2954.1 MB
[runlim] sample:		176.5 time, 640.4 real, 3134.3 MB
[runlim] sample:		186.5 time, 650.4 real, 3316.6 MB
[runlim] sample:		196.5 time, 660.4 real, 3488.9 MB
[runlim] sample:		206.5 time, 670.4 real, 3667.5 MB
[runlim] sample:		216.5 time, 680.4 real, 3864.2 MB
[runlim] sample:		226.5 time, 690.4 real, 4058.4 MB
[runlim] sample:		236.5 time, 700.4 real, 4244.9 MB
[runlim] sample:		246.5 time, 710.4 real, 4443.2 MB
[runlim] sample:		256.4 time, 720.4 real, 4615.3 MB
[runlim] sample:		266.4 time, 730.4 real, 4803.7 MB
[runlim] sample:		276.4 time, 740.4 real, 4805.0 MB
[runlim] sample:		286.4 time, 750.4 real, 4805.8 MB
[runlim] sample:		296.4 time, 760.4 real, 4872.5 MB
[runlim] sample:		306.4 time, 770.4 real, 4941.2 MB
[runlim] sample:		316.4 time, 780.4 real, 5072.3 MB
[runlim] sample:		326.4 time, 790.4 real, 5244.5 MB
[runlim] sample:		336.3 time, 800.4 real, 5418.6 MB
[runlim] sample:		346.3 time, 810.4 real, 5592.6 MB
[runlim] sample:		356.3 time, 820.4 real, 5767.0 MB
[runlim] sample:		366.3 time, 830.4 real, 5953.6 MB
[runlim] sample:		376.3 time, 840.4 real, 6123.9 MB
[runlim] sample:		386.3 time, 850.4 real, 6293.7 MB
[runlim] sample:		396.3 time, 860.4 real, 6463.1 MB
[runlim] sample:		406.3 time, 870.4 real, 6628.1 MB
[runlim] sample:		6.3 time, 880.4 real, 163.8 MB
[runlim] sample:		16.3 time, 890.4 real, 309.7 MB
[runlim] sample:		26.3 time, 900.4 real, 459.1 MB
[runlim] sample:		36.3 time, 910.4 real, 529.8 MB
[runlim] sample:		46.2 time, 920.4 real, 654.5 MB
[runlim] sample:		56.2 time, 930.4 real, 761.5 MB
[runlim] sample:		66.2 time, 940.4 real, 863.4 MB
[runlim] sample:		76.2 time, 950.4 real, 897.8 MB
[runlim] sample:		86.2 time, 960.4 real, 994.7 MB
[runlim] sample:		96.2 time, 970.4 real, 1131.6 MB
[runlim] sample:		106.2 time, 980.4 real, 1235.1 MB
[runlim] sample:		116.2 time, 990.4 real, 1344.0 MB
[runlim] sample:		126.2 time, 1000.4 real, 1461.3 MB
[runlim] sample:		136.2 time, 1010.4 real, 1528.6 MB
[runlim] sample:		146.1 time, 1020.4 real, 1532.1 MB
[runlim] sample:		156.1 time, 1030.4 real, 1606.1 MB
[runlim] sample:		166.1 time, 1040.4 real, 1687.1 MB
[runlim] sample:		176.1 time, 1050.4 real, 1825.1 MB
[runlim] sample:		186.1 time, 1060.4 real, 1953.7 MB
[runlim] sample:		196.1 time, 1070.4 real, 2054.2 MB
[runlim] sample:		206.0 time, 1080.4 real, 2169.6 MB
[runlim] sample:		216.0 time, 1090.4 real, 2273.3 MB
[runlim] sample:		226.0 time, 1100.4 real, 2383.0 MB
[runlim] sample:		236.0 time, 1110.4 real, 2510.6 MB
[runlim] sample:		246.0 time, 1120.4 real, 2619.5 MB
[runlim] sample:		256.0 time, 1130.4 real, 2729.3 MB
[runlim] sample:		266.0 time, 1140.4 real, 2798.8 MB
[runlim] sample:		276.0 time, 1150.4 real, 2802.6 MB
[runlim] sample:		286.0 time, 1160.4 real, 2804.1 MB
[runlim] sample:		295.9 time, 1170.4 real, 2806.8 MB
[runlim] sample:		305.9 time, 1180.4 real, 2838.0 MB
[runlim] sample:		315.9 time, 1190.4 real, 2930.8 MB
[runlim] sample:		325.9 time, 1200.4 real, 3015.8 MB
[runlim] sample:		335.9 time, 1210.4 real, 3135.5 MB
[runlim] sample:		345.9 time, 1220.4 real, 3236.5 MB
[runlim] sample:		355.9 time, 1230.4 real, 3332.9 MB
[runlim] sample:		365.8 time, 1240.4 real, 3428.0 MB
[runlim] sample:		375.8 time, 1250.4 real, 3545.5 MB
[runlim] sample:		385.8 time, 1260.4 real, 3661.9 MB
[runlim] sample:		395.8 time, 1270.4 real, 3758.6 MB
[runlim] sample:		405.8 time, 1280.4 real, 3843.0 MB
[runlim] sample:		415.8 time, 1290.4 real, 3947.7 MB
[runlim] sample:		425.8 time, 1300.4 real, 4099.9 MB
[runlim] sample:		435.8 time, 1310.4 real, 4174.3 MB
[runlim] sample:		445.7 time, 1320.4 real, 4338.4 MB
[runlim] sample:		455.7 time, 1330.4 real, 4480.4 MB
[runlim] sample:		465.7 time, 1340.4 real, 4593.5 MB
[runlim] sample:		475.7 time, 1350.4 real, 4717.0 MB
[runlim] sample:		485.7 time, 1360.4 real, 4847.5 MB
[runlim] sample:		495.7 time, 1370.4 real, 4950.1 MB
[runlim] sample:		505.7 time, 1380.4 real, 5070.8 MB
[runlim] sample:		515.6 time, 1390.4 real, 5153.3 MB
[runlim] sample:		525.6 time, 1400.4 real, 5263.9 MB
[runlim] sample:		535.6 time, 1410.4 real, 5263.9 MB
[runlim] sample:		545.6 time, 1420.4 real, 5270.4 MB
[runlim] sample:		555.6 time, 1430.4 real, 5277.4 MB
[runlim] sample:		565.6 time, 1440.4 real, 5277.9 MB
[runlim] sample:		575.5 time, 1450.4 real, 5284.1 MB
[runlim] sample:		585.5 time, 1460.4 real, 5287.1 MB
[runlim] sample:		595.5 time, 1470.4 real, 5287.6 MB
[runlim] sample:		605.5 time, 1480.4 real, 5287.9 MB
[runlim] sample:		615.5 time, 1490.4 real, 5384.9 MB
[runlim] sample:		625.5 time, 1500.4 real, 5457.3 MB
[runlim] sample:		635.5 time, 1510.4 real, 5536.0 MB
[runlim] sample:		645.5 time, 1520.4 real, 5622.1 MB
[runlim] sample:		655.4 time, 1530.4 real, 5716.6 MB
[runlim] sample:		665.4 time, 1540.4 real, 5831.2 MB
[runlim] sample:		675.4 time, 1550.4 real, 5932.1 MB
[runlim] sample:		685.4 time, 1560.4 real, 6055.0 MB
[runlim] sample:		695.4 time, 1570.4 real, 6168.5 MB
[runlim] sample:		705.4 time, 1580.4 real, 6254.7 MB
[runlim] sample:		715.4 time, 1590.4 real, 6391.1 MB
[runlim] sample:		725.3 time, 1600.4 real, 6453.2 MB
[runlim] sample:		735.3 time, 1610.4 real, 6616.4 MB
[runlim] sample:		0.9 time, 1620.4 real, 83.1 MB
[runlim] sample:		10.9 time, 1630.4 real, 411.9 MB
[runlim] sample:		20.9 time, 1640.4 real, 633.0 MB
[runlim] sample:		30.8 time, 1650.4 real, 844.5 MB
[runlim] sample:		40.8 time, 1660.4 real, 990.6 MB
[runlim] sample:		50.8 time, 1670.4 real, 1178.2 MB
[runlim] sample:		60.8 time, 1680.4 real, 1354.5 MB
[runlim] sample:		70.8 time, 1690.4 real, 1535.0 MB
[runlim] sample:		80.8 time, 1700.4 real, 1701.6 MB
[runlim] sample:		90.8 time, 1710.4 real, 1851.7 MB
[runlim] sample:		100.8 time, 1720.4 real, 1888.1 MB
[runlim] sample:		110.7 time, 1730.4 real, 1997.5 MB
[runlim] sample:		120.7 time, 1740.4 real, 2136.2 MB
[runlim] sample:		130.7 time, 1750.4 real, 2276.3 MB
[runlim] sample:		140.7 time, 1760.4 real, 2406.0 MB
[runlim] sample:		150.7 time, 1770.4 real, 2537.4 MB
[runlim] sample:		160.7 time, 1780.4 real, 2674.9 MB
[runlim] sample:		170.7 time, 1790.4 real, 2807.2 MB
[runlim] sample:		180.7 time, 1800.4 real, 2929.1 MB
[runlim] sample:		190.6 time, 1810.4 real, 3081.6 MB
[runlim] sample:		200.6 time, 1820.4 real, 3204.4 MB
[runlim] sample:		210.6 time, 1830.4 real, 3330.4 MB
[runlim] sample:		220.6 time, 1840.4 real, 3444.6 MB
[runlim] sample:		230.6 time, 1850.4 real, 3560.8 MB
[runlim] sample:		240.6 time, 1860.4 real, 3680.8 MB
[runlim] sample:		250.6 time, 1870.4 real, 3797.7 MB
[runlim] sample:		260.6 time, 1880.4 real, 3905.2 MB
[runlim] sample:		270.5 time, 1890.4 real, 4018.6 MB
[runlim] sample:		280.5 time, 1900.4 real, 4083.4 MB
[runlim] sample:		290.5 time, 1910.4 real, 4087.2 MB
[runlim] sample:		300.5 time, 1920.4 real, 4118.2 MB
[runlim] sample:		310.5 time, 1930.4 real, 4184.4 MB
[runlim] sample:		320.5 time, 1940.4 real, 4276.6 MB
[runlim] sample:		330.5 time, 1950.4 real, 4393.9 MB
[runlim] sample:		340.5 time, 1960.4 real, 4499.3 MB
[runlim] sample:		350.5 time, 1970.4 real, 4604.3 MB
[runlim] sample:		360.4 time, 1980.4 real, 4713.0 MB
[runlim] sample:		370.4 time, 1990.4 real, 4838.5 MB
[runlim] sample:		380.4 time, 2000.4 real, 4941.0 MB
[runlim] sample:		390.4 time, 2010.4 real, 5043.4 MB
[runlim] sample:		400.4 time, 2020.4 real, 5139.8 MB
[runlim] sample:		410.4 time, 2030.4 real, 5236.2 MB
[runlim] sample:		420.4 time, 2040.4 real, 5332.0 MB
[runlim] sample:		430.4 time, 2050.4 real, 5432.4 MB
[runlim] sample:		440.4 time, 2060.4 real, 5528.6 MB
[runlim] sample:		450.3 time, 2070.4 real, 5673.2 MB
[runlim] sample:		460.3 time, 2080.4 real, 5773.6 MB
[runlim] sample:		470.3 time, 2090.4 real, 5868.0 MB
[runlim] sample:		480.3 time, 2100.4 real, 5968.6 MB
[runlim] sample:		490.3 time, 2110.4 real, 6066.6 MB
[runlim] sample:		500.3 time, 2120.4 real, 6151.6 MB
[runlim] sample:		510.3 time, 2130.4 real, 6238.2 MB
[runlim] sample:		520.2 time, 2140.4 real, 6326.8 MB
[runlim] sample:		530.2 time, 2150.4 real, 6422.1 MB
[runlim] sample:		540.2 time, 2160.4 real, 6517.3 MB
[runlim] sample:		550.2 time, 2170.4 real, 6614.5 MB
[runlim] end:			Mon Sep 28 22:02:01 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		130238
[runlim] real:			2171.42 seconds
[runlim] time:			744.12 seconds
[runlim] space:			6681.4 MB
[runlim] samples:		21710
