blob: 800aa4f625fb64b276650d18205694cc307da488 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Require Import Lia ZArith.
Open Scope Z_scope.
Unset Lia Cache.
(* Expected time < 1.00s *)
Goal forall (x2 x3 x : Z)
(H : 0 <= 1073741824 * x + x2 - 67146752)
(H0 : 0 <= -8192 + x2)
(H1 : 0 <= 34816 + - x2)
(H2 : 0 <= -1073741824 * x - x2 + 1073741823),
False.
Proof.
intros.
Time lia.
Qed.
|
