function abs(x: int) : int = (if (0 <= x) then x else (-x))

logic div : int, int -> int

logic mod : int, int -> int

predicate divides(d: int, n: int) = (if (d = 0) then (n = 0) else (mod(n, d) = 0))

axiom dividesqtspec :
  (forall d:int. forall n:int. (divides(d, n) -> (exists q:int. (n = (q * d)))))

logic ac gcd : int, int -> int

axiom gcd_def1 : (forall a:int. forall b:int. divides(gcd(a, b), a))

axiom gcd_def2 : (forall a:int. forall b:int. divides(gcd(a, b), b))

axiom gcd_def3 :
  (forall a:int. forall b:int. forall x:int. (divides(x, a) -> (divides(x, b) -> divides(x, gcd(a, b)))))

axiom gcd_0_pos : (forall a:int. ((0 <= a) -> (gcd(a, 0) = a)))

axiom gcd_0_neg : (forall a:int. ((a <  0) -> (gcd(a, 0) = (-a))))

axiom gcd_opp : (forall a:int. forall b:int. (gcd(a, b) = gcd((-a), b)))

axiom gcd_mult :
  (forall a:int. forall b:int. forall c:int. ((0 <= c) -> (gcd((c * a), (c * b)) = (c * gcd(a, b)))))

goal wp_goal :
  (forall i:int. forall i1:int. forall i2:int. ((gcd(i1, 0) = gcd(i, i2)) ->
  ((0 <= i1) -> ((abs(i2) <= 2147483647) -> not (abs(i) <= 2147483647)))))