Incorrect model

[AnzhelaSukhanova]

Hello,
For this instance

(set-logic HORN)

(declare-fun P ( ) Bool)

(assert (forall ((A Int)
         (B Int)
         (C Int)
         (D Int)
         (E Int)
         (F Int)
         (G Int)
         (H Int)
         (I (Array Int Int))
         (J (Array Int Int))
         (K (Array Int Int)))
  (let ((a!1 (and (= (select J H) (select J G))
                  (= (+ A) (select J A))
                  (= G A)
                  (not (<= G (+ H)))
                  (or (<= (select J H) H)))))
    (=> a!1 P))))

(assert (=> P false))

(check-sat)
(get-model)
(exit)

z3 returns

sat
(
  (define-fun P () Bool
    true)
)

This interpretation is incorrect for the last clause.