simple ancestor relation encoding in z3 smt solver

ancestor.smt

(declare-sort Person)
(declare-fun ancestor (Person Person) Bool)

;; anti symmetry
(assert (forall ((x Person) (y Person))
                (=> (ancestor x y) (not (ancestor y x)))))

;; transitivity
(assert (forall ((x Person) (y Person) (z Person))
  (=> (and (ancestor x y) (ancestor y z))
    (ancestor x z)
  )
)) 
              
(declare-var bob Person)
(declare-var joe Person)
(declare-var tim Person)
(assert (ancestor bob joe))
(assert (ancestor joe tim))

(declare-var flip Bool)
(assert (= flip (ancestor joe bob)))

(declare-var transitive Bool)
(assert (= transitive (ancestor bob tim)))

(check-sat)              
(get-model)