[tradeoff R=3.0] T = 3.00018e+12 (current verification): fails at (753.985, 754.485) [tradeoff R=3.0] T = 4.24276e+13: closes (723 s) [tradeoff R=3.0] T = 1.12823e+13: fails at (1048.4850000000001, 1048.9850000000001) (953 s) [tradeoff R=3.0] T = 2.18788e+13: fails at (1236.9850000000001, 1237.4850000000001) (1181 s) [tradeoff R=3.0] T = 3.04675e+13: fails at (1343.4850000000001, 1343.9850000000001) (1379 s) [tradeoff R=3.0] T = 3.59536e+13: closes (1640 s) [tradeoff R=3.0] T = 3.30971e+13: closes (1899 s) [tradeoff R=3.0] T = 3.1755e+13: closes (2146 s) [tradeoff R=3.0] T = 3.11046e+13: closes (2393 s) [tradeoff R=3.0] T = 3.07844e+13: fails at (1346.9850000000001, 1347.4850000000001) (2603 s) [tradeoff R=3.0] T = 3.09441e+13: closes (2871 s) [tradeoff R=3.0] T = 3.08641e+13: closes (3132 s) [tradeoff R=3.0] T = 3.08242e+13: fails at (1347.4850000000001, 1347.9850000000001) (3353 s) [tradeoff R=3.0, TR3.0] RH to height 3.08641e+13 suffices; fails at 3.08242e+13 (3353 s)