(set-logic UFSLIA)
(set-option :produce-models true)

;
 ; Sorts 
;
(declare-sort K_Classifier 0)
(declare-sort K_Type 0)
(declare-const nullInt Int)
(declare-const invalidInt Int)
(declare-const nullString String)
(declare-const invalidString String)
(declare-const nullClassifier K_Classifier)
(declare-const invalidClassifier K_Classifier)
(declare-const nullType K_Type)
(declare-const invalidType K_Type)
(declare-fun ContactInfo_name (K_Classifier) String)
(declare-fun Referral_referredBy (K_Classifier) K_Classifier)
(declare-fun Doctor_substitutedBy (K_Classifier) K_Classifier)
(declare-fun Doctor_patients (K_Classifier K_Classifier) Bool)
(declare-fun Doctor_referralsIn (K_Classifier K_Classifier) Bool)
(declare-fun Nurse_license (K_Classifier) Int)
(declare-fun Doctor_substitutions (K_Classifier K_Classifier) Bool)
(declare-fun ContactInfo_gender (K_Classifier) String)
(declare-fun Professional_surname (K_Classifier) String)
(declare-fun Patient_referrals (K_Classifier K_Classifier) Bool)
(declare-fun ContactInfo_yearOfBirth (K_Classifier) Int)
(declare-fun Doctor_referralsOut (K_Classifier K_Classifier) Bool)
(declare-fun Doctor_license (K_Classifier) String)
(declare-fun MedicalCenter_city (K_Classifier) String)
(declare-fun Professional_login (K_Classifier) String)
(declare-fun Department_patients (K_Classifier K_Classifier) Bool)
(declare-fun Patient_department (K_Classifier) K_Classifier)
(declare-fun Patient_doctor (K_Classifier) K_Classifier)
(declare-fun MedicalCenter_director (K_Classifier) K_Classifier)
(declare-fun Referral_id (K_Classifier) String)
(declare-fun ContactInfo_address (K_Classifier) String)
(declare-fun Professional_password (K_Classifier) String)
(declare-fun Department_doctors (K_Classifier K_Classifier) Bool)
(declare-fun MedicalCenter_zipCode (K_Classifier) String)
(declare-fun Patient_id (K_Classifier) String)
(declare-fun Department_nurses (K_Classifier K_Classifier) Bool)
(declare-fun ContactInfo_surname (K_Classifier) String)
(declare-fun MedicalCenter_address (K_Classifier) String)
(declare-fun Professional_name (K_Classifier) String)
(declare-fun MedicalCenter_departments (K_Classifier K_Classifier) Bool)
(declare-fun Doctor_status (K_Classifier) String)
(declare-fun MedicalCenter_name (K_Classifier) String)
(declare-fun Department_belongsTo (K_Classifier) K_Classifier)
(declare-fun Referral_referringTo (K_Classifier) K_Classifier)
(declare-fun Department_location (K_Classifier) String)
(declare-fun MedicalCenter_employees (K_Classifier K_Classifier) Bool)
(declare-fun Referral_patient (K_Classifier) K_Classifier)
(declare-fun Department_name (K_Classifier) String)
(declare-fun MedicalCenter_country (K_Classifier) String)
(declare-fun Patient_contactInfo (K_Classifier) K_Classifier)
(declare-fun ContactInfo_id (K_Classifier) String)
(declare-fun Department (K_Classifier) Bool)
(declare-const DepartmentType K_Type)
(declare-fun ContactInfo (K_Classifier) Bool)
(declare-const ContactInfoType K_Type)
(declare-fun Director (K_Classifier) Bool)
(declare-const DirectorType K_Type)
(declare-fun Professional (K_Classifier) Bool)
(declare-const ProfessionalType K_Type)
(declare-fun MedicalCenter (K_Classifier) Bool)
(declare-const MedicalCenterType K_Type)
(declare-fun Patient (K_Classifier) Bool)
(declare-const PatientType K_Type)
(declare-fun Doctor (K_Classifier) Bool)
(declare-const DoctorType K_Type)
(declare-fun Referral (K_Classifier) Bool)
(declare-const ReferralType K_Type)
(declare-fun Nurse (K_Classifier) Bool)
(declare-const NurseType K_Type)
;
 ; Elements to create should be differents
;
(assert (distinct nullClassifier invalidClassifier))
(assert (distinct nullType invalidType  MedicalCenterType DepartmentType ProfessionalType ReferralType DirectorType PatientType ContactInfoType DoctorType NurseType))

(define-fun oclIsTypeOf ((d K_Classifier) (t K_Type)) Bool
(ite (= t MedicalCenterType)
(MedicalCenter d)
(ite (= t DepartmentType)
(Department d)
(ite (= t ProfessionalType)
(Professional d)
(ite (= t ReferralType)
(Referral d)
(ite (= t DirectorType)
(Director d)
(ite (= t PatientType)
(Patient d)
(ite (= t ContactInfoType)
(ContactInfo d)
(ite (= t DoctorType)
(Doctor d)
(ite (= t NurseType)
(Nurse d)
false))))))))))


(define-fun oclIsKindOf ((d K_Classifier) (t K_Type)) Bool
(ite (= t MedicalCenterType)
(MedicalCenter d)
(ite (= t DepartmentType)
(Department d)
(ite (= t ProfessionalType)
(or (Professional d)(Doctor d)(Nurse d)(Director d))
(ite (= t ReferralType)
(Referral d)
(ite (= t DirectorType)
(Director d)
(ite (= t PatientType)
(Patient d)
(ite (= t ContactInfoType)
(ContactInfo d)
(ite (= t DoctorType)
(Doctor d)
(ite (= t NurseType)
(Nurse d)
false))))))))))


(define-fun oclType ((d K_Classifier)) K_Type
(ite (MedicalCenter d)
MedicalCenterType
(ite (Department d)
DepartmentType
(ite (Professional d)
ProfessionalType
(ite (Referral d)
ReferralType
(ite (Director d)
DirectorType
(ite (Patient d)
PatientType
(ite (ContactInfo d)
ContactInfoType
(ite (Doctor d)
DoctorType
(ite (Nurse d)
NurseType
nullType))))))))))

;
 ; Basic Invariants over constants
;
(assert (distinct nullInt invalidInt))
(assert (distinct nullString invalidString "" "available" "unavailable"))
;
 ; States s_0
;
;
 ; Properties over enumUML
;
;
 ; Properties over umlClasses
;
(assert (not (or  (Patient invalidClassifier) (Patient nullClassifier))))
(assert (not (or  (ContactInfo invalidClassifier) (ContactInfo nullClassifier))))
(assert (not (or  (Nurse invalidClassifier) (Nurse nullClassifier))))
(assert (not (or  (Referral invalidClassifier) (Referral nullClassifier))))
(assert (not (or  (Doctor invalidClassifier) (Doctor nullClassifier))))
(assert (not (or  (Director invalidClassifier) (Director nullClassifier))))
(assert (not (or  (Department invalidClassifier) (Department nullClassifier))))
(assert (not (or  (MedicalCenter invalidClassifier) (MedicalCenter nullClassifier))))
(assert (not (or  (Professional invalidClassifier) (Professional nullClassifier))))
;
 ; Propagation null over attributes
;
(assert (= (Patient_id nullClassifier) invalidString))
(assert (= (Patient_contactInfo nullClassifier) invalidClassifier))
(assert (= (ContactInfo_name nullClassifier) invalidString))
(assert (= (ContactInfo_surname nullClassifier) invalidString))
(assert (= (ContactInfo_yearOfBirth nullClassifier) invalidInt))
(assert (= (ContactInfo_gender nullClassifier) invalidString))
(assert (= (ContactInfo_address nullClassifier) invalidString))
(assert (= (ContactInfo_id nullClassifier) invalidString))
(assert (= (Nurse_license nullClassifier) invalidInt))
(assert (= (Referral_id nullClassifier) invalidString))
(assert (= (Doctor_license nullClassifier) invalidString))
(assert (= (Doctor_status nullClassifier) invalidString))
(assert (= (Department_name nullClassifier) invalidString))
(assert (= (Department_location nullClassifier) invalidString))
(assert (= (MedicalCenter_name nullClassifier) invalidString))
(assert (= (MedicalCenter_address nullClassifier) invalidString))
(assert (= (MedicalCenter_zipCode nullClassifier) invalidString))
(assert (= (MedicalCenter_city nullClassifier) invalidString))
(assert (= (MedicalCenter_country nullClassifier) invalidString))
(assert (= (MedicalCenter_director nullClassifier) invalidClassifier))
(assert (= (Professional_login nullClassifier) invalidString))
(assert (= (Professional_password nullClassifier) invalidString))
(assert (= (Professional_name nullClassifier) invalidString))
(assert (= (Professional_surname nullClassifier) invalidString))
;
 ; Propagation invalid over attributes
;
(assert (= (Patient_id invalidClassifier) invalidString))
(assert (= (Patient_contactInfo invalidClassifier) invalidClassifier))
(assert (= (ContactInfo_name invalidClassifier) invalidString))
(assert (= (ContactInfo_surname invalidClassifier) invalidString))
(assert (= (ContactInfo_yearOfBirth invalidClassifier) invalidInt))
(assert (= (ContactInfo_gender invalidClassifier) invalidString))
(assert (= (ContactInfo_address invalidClassifier) invalidString))
(assert (= (ContactInfo_id invalidClassifier) invalidString))
(assert (= (Nurse_license invalidClassifier) invalidInt))
(assert (= (Referral_id invalidClassifier) invalidString))
(assert (= (Doctor_license invalidClassifier) invalidString))
(assert (= (Doctor_status invalidClassifier) invalidString))
(assert (= (Department_name invalidClassifier) invalidString))
(assert (= (Department_location invalidClassifier) invalidString))
(assert (= (MedicalCenter_name invalidClassifier) invalidString))
(assert (= (MedicalCenter_address invalidClassifier) invalidString))
(assert (= (MedicalCenter_zipCode invalidClassifier) invalidString))
(assert (= (MedicalCenter_city invalidClassifier) invalidString))
(assert (= (MedicalCenter_country invalidClassifier) invalidString))
(assert (= (MedicalCenter_director invalidClassifier) invalidClassifier))
(assert (= (Professional_login invalidClassifier) invalidString))
(assert (= (Professional_password invalidClassifier) invalidString))
(assert (= (Professional_name invalidClassifier) invalidString))
(assert (= (Professional_surname invalidClassifier) invalidString))
;
 ; Other properties over attributes
;
(assert (forall((x K_Classifier))(=> (Patient x) (not(= (Patient_id x) invalidString)))))
(assert (forall((x K_Classifier))(=> (Patient x) (or  (= (Patient_contactInfo x) nullClassifier) (ContactInfo (Patient_contactInfo x))))))
(assert (forall((x K_Classifier))(=> (ContactInfo x) (not(= (ContactInfo_name x) invalidString)))))
(assert (forall((x K_Classifier))(=> (ContactInfo x) (not(= (ContactInfo_surname x) invalidString)))))
(assert (forall((x K_Classifier))(=> (ContactInfo x) (not(= (ContactInfo_yearOfBirth x) invalidInt)))))
(assert (forall((x K_Classifier))(=> (ContactInfo x) (not(= (ContactInfo_gender x) invalidString)))))
(assert (forall((x K_Classifier))(=> (ContactInfo x) (not(= (ContactInfo_address x) invalidString)))))
(assert (forall((x K_Classifier))(=> (ContactInfo x) (not(= (ContactInfo_id x) invalidString)))))
(assert (forall((x K_Classifier))(=> (Nurse x) (not(= (Nurse_license x) invalidInt)))))
(assert (forall((x K_Classifier))(=> (Referral x) (not(= (Referral_id x) invalidString)))))
(assert (forall((x K_Classifier))(=> (Doctor x) (not(= (Doctor_license x) invalidString)))))
(assert (forall((x K_Classifier))(=> (Doctor x) (not(= (Doctor_status x) invalidString)))))
(assert (forall((x K_Classifier))(=> (Department x) (not(= (Department_name x) invalidString)))))
(assert (forall((x K_Classifier))(=> (Department x) (not(= (Department_location x) invalidString)))))
(assert (forall((x K_Classifier))(=> (MedicalCenter x) (not(= (MedicalCenter_name x) invalidString)))))
(assert (forall((x K_Classifier))(=> (MedicalCenter x) (not(= (MedicalCenter_address x) invalidString)))))
(assert (forall((x K_Classifier))(=> (MedicalCenter x) (not(= (MedicalCenter_zipCode x) invalidString)))))
(assert (forall((x K_Classifier))(=> (MedicalCenter x) (not(= (MedicalCenter_city x) invalidString)))))
(assert (forall((x K_Classifier))(=> (MedicalCenter x) (not(= (MedicalCenter_country x) invalidString)))))
(assert (forall((x K_Classifier))(=> (MedicalCenter x) (or  (= (MedicalCenter_director x) nullClassifier) (or  (Director (MedicalCenter_director x)) (Professional (MedicalCenter_director x)))))))
(assert (forall((x K_Classifier))(=> (or  (Professional x) (Doctor x) (Nurse x) (Director x)) (not(= (Professional_login x) invalidString)))))
(assert (forall((x K_Classifier))(=> (or  (Professional x) (Doctor x) (Nurse x) (Director x)) (not(= (Professional_password x) invalidString)))))
(assert (forall((x K_Classifier))(=> (or  (Professional x) (Doctor x) (Nurse x) (Director x)) (not(= (Professional_name x) invalidString)))))
(assert (forall((x K_Classifier))(=> (or  (Professional x) (Doctor x) (Nurse x) (Director x)) (not(= (Professional_surname x) invalidString)))))
;
 ; Properties over associationEnds 0..1
;
(assert (= (Patient_department nullClassifier) invalidClassifier))
(assert (= (Patient_department invalidClassifier) invalidClassifier))
(assert (forall((x K_Classifier))(=> (Patient x) (or  (= (Patient_department x) nullClassifier) (Department (Patient_department x))))))
(assert (= (Patient_doctor nullClassifier) invalidClassifier))
(assert (= (Patient_doctor invalidClassifier) invalidClassifier))
(assert (forall((x K_Classifier))(=> (Patient x) (or  (= (Patient_doctor x) nullClassifier) (Doctor (Patient_doctor x))))))
(assert (= (Referral_referredBy nullClassifier) invalidClassifier))
(assert (= (Referral_referredBy invalidClassifier) invalidClassifier))
(assert (forall((x K_Classifier))(=> (Referral x) (or  (= (Referral_referredBy x) nullClassifier) (Doctor (Referral_referredBy x))))))
(assert (= (Referral_patient nullClassifier) invalidClassifier))
(assert (= (Referral_patient invalidClassifier) invalidClassifier))
(assert (forall((x K_Classifier))(=> (Referral x) (or  (= (Referral_patient x) nullClassifier) (Patient (Referral_patient x))))))
(assert (= (Referral_referringTo nullClassifier) invalidClassifier))
(assert (= (Referral_referringTo invalidClassifier) invalidClassifier))
(assert (forall((x K_Classifier))(=> (Referral x) (or  (= (Referral_referringTo x) nullClassifier) (Doctor (Referral_referringTo x))))))
(assert (= (Doctor_substitutedBy nullClassifier) invalidClassifier))
(assert (= (Doctor_substitutedBy invalidClassifier) invalidClassifier))
(assert (forall((x K_Classifier))(=> (Doctor x) (or  (= (Doctor_substitutedBy x) nullClassifier) (Doctor (Doctor_substitutedBy x))))))
(assert (= (Department_belongsTo nullClassifier) invalidClassifier))
(assert (= (Department_belongsTo invalidClassifier) invalidClassifier))
(assert (forall((x K_Classifier))(=> (Department x) (or  (= (Department_belongsTo x) nullClassifier) (MedicalCenter (Department_belongsTo x))))))
;
 ; Properties over associationEnds *
;
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Patient_referrals x y) (and (Patient x) (Referral y))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Doctor_referralsOut x y) (and (Doctor x) (Referral y))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Doctor_substitutions x y) (and (Doctor x) (Doctor y))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Doctor_referralsIn x y) (and (Doctor x) (Referral y))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Doctor_patients x y) (and (Doctor x) (Patient y))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Department_doctors x y) (and (Department x) (Doctor y))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Department_nurses x y) (and (Department x) (Nurse y))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Department_patients x y) (and (Department x) (Patient y))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (MedicalCenter_employees x y) (and (MedicalCenter x) (or  (Professional y) (Doctor y) (Nurse y) (Director y)))))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (MedicalCenter_departments x y) (and (MedicalCenter x) (Department y))))))
;
 ; Definition of association. Asso <=> AssocOp
;
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (and (Patient x) (Referral y) (= (Referral_patient y) x)) (Patient_referrals x y)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Patient_referrals x y) (= (Referral_patient y) x)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (and (Doctor x) (Referral y) (= (Referral_referredBy y) x)) (Doctor_referralsOut x y)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Doctor_referralsOut x y) (= (Referral_referredBy y) x)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (and (Doctor x) (Doctor y) (= (Doctor_substitutedBy y) x)) (Doctor_substitutions x y)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Doctor_substitutions x y) (= (Doctor_substitutedBy y) x)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (and (Doctor x) (Referral y) (= (Referral_referringTo y) x)) (Doctor_referralsIn x y)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Doctor_referralsIn x y) (= (Referral_referringTo y) x)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (and (Doctor x) (Patient y) (= (Patient_doctor y) x)) (Doctor_patients x y)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Doctor_patients x y) (= (Patient_doctor y) x)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (and (Department x) (Patient y) (= (Patient_department y) x)) (Department_patients x y)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (Department_patients x y) (= (Patient_department y) x)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (and (MedicalCenter x) (Department y) (= (Department_belongsTo y) x)) (MedicalCenter_departments x y)))))
(assert (forall((y K_Classifier))(forall((x K_Classifier))(=> (MedicalCenter_departments x y) (= (Department_belongsTo y) x)))))
;
 ; Definition required inheritance
;
(assert (forall((x K_Classifier))(=> (Patient x) (not (or  (ContactInfo x) (Doctor x) (Nurse x) (Director x) (Department x) (MedicalCenter x) (Referral x) (Professional x))))))
(assert (forall((x K_Classifier))(=> (ContactInfo x) (not (or  (Patient x) (Doctor x) (Nurse x) (Director x) (Department x) (MedicalCenter x) (Referral x) (Professional x))))))
(assert (forall((x K_Classifier))(=> (Doctor x) (not (or  (Patient x) (ContactInfo x) (Nurse x) (Director x) (Department x) (MedicalCenter x) (Referral x) (Professional x))))))
(assert (forall((x K_Classifier))(=> (Nurse x) (not (or  (Patient x) (ContactInfo x) (Doctor x) (Director x) (Department x) (MedicalCenter x) (Referral x) (Professional x))))))
(assert (forall((x K_Classifier))(=> (Director x) (not (or  (Patient x) (ContactInfo x) (Doctor x) (Nurse x) (Department x) (MedicalCenter x) (Referral x) (Professional x))))))
(assert (forall((x K_Classifier))(=> (Department x) (not (or  (Patient x) (ContactInfo x) (Doctor x) (Nurse x) (Director x) (MedicalCenter x) (Referral x) (Professional x))))))
(assert (forall((x K_Classifier))(=> (MedicalCenter x) (not (or  (Patient x) (ContactInfo x) (Doctor x) (Nurse x) (Director x) (Department x) (Referral x) (Professional x))))))
(assert (forall((x K_Classifier))(=> (Referral x) (not (or  (Patient x) (ContactInfo x) (Doctor x) (Nurse x) (Director x) (Department x) (MedicalCenter x) (Professional x))))))
(assert (forall((x K_Classifier))(=> (Professional x) (not (or  (Patient x) (ContactInfo x) (Doctor x) (Nurse x) (Director x) (Department x) (MedicalCenter x) (Referral x))))))
;
 ; Definitions of subexpressions required by the main expression
;
;
 ; Subdefinitions. Checking that the set does not contain any invalid value 
;
;
 ; Invariants Initial state + conditionals + postconditionals 
;
(assert (exists ((var1 K_Classifier))(MedicalCenter var1)))
(assert (forall((m K_Classifier))(=> (MedicalCenter m) (not (or  (= nullString (MedicalCenter_name m)) (or  (= invalidClassifier m) (= nullClassifier m)))))))
(assert (forall((m1 K_Classifier))(=> (MedicalCenter m1) (forall((m2 K_Classifier))(=> (MedicalCenter m2) (or  (and (= m1 m2) (not (= invalidClassifier m1))) (or  (or  (or  (or  (or  (= invalidClassifier m1) (= nullClassifier m1)) (not (= (MedicalCenter_address m1) (MedicalCenter_address m2)))) (or  (or  (= invalidClassifier m1) (= nullClassifier m1)) (not (= (MedicalCenter_zipCode m1) (MedicalCenter_zipCode m2))))) (or  (or  (= invalidClassifier m1) (= nullClassifier m1)) (not (= (MedicalCenter_city m1) (MedicalCenter_city m2))))) (or  (or  (= invalidClassifier m1) (= nullClassifier m1)) (not (= (MedicalCenter_country m1) (MedicalCenter_country m2)))))))))))
(assert (forall((m K_Classifier))(=> (MedicalCenter m) (and (not (or  (= nullString (MedicalCenter_city m)) (or  (= invalidClassifier m) (= nullClassifier m)))) (not (or  (= nullString (MedicalCenter_country m)) (or  (= invalidClassifier m) (= nullClassifier m))))))))
(assert (forall((m K_Classifier))(=> (MedicalCenter m) (and (exists ((var1 K_Classifier))(MedicalCenter_employees m var1)) (not (or  (= invalidClassifier m) (= nullClassifier m)))))))
(assert (exists ((var1 K_Classifier))(Department var1)))
(assert (forall((d K_Classifier))(=> (Department d) (not (or  (= nullString (Department_name d)) (or  (= invalidClassifier d) (= nullClassifier d)))))))
(assert (forall((d K_Classifier))(=> (Department d) (not (or  (= nullClassifier (Department_belongsTo d)) (or  (= invalidClassifier d) (= nullClassifier d)))))))
(assert (forall((d K_Classifier))(=> (Department d) (and (exists ((var1 K_Classifier))(Department_doctors d var1)) (not (or  (= invalidClassifier d) (= nullClassifier d)))))))
(assert (forall((d K_Classifier))(=> (Department d) (and (exists ((var1 K_Classifier))(Department_nurses d var1)) (not (or  (= invalidClassifier d) (= nullClassifier d)))))))
(assert (exists ((var1 K_Classifier))(or  (Professional var1) (Doctor var1) (Nurse var1) (Director var1))))
(assert (forall((p K_Classifier))(=> (or  (Professional p) (Doctor p) (Nurse p) (Director p)) (not (or  (= nullString (Professional_name p)) (or  (= invalidClassifier p) (= nullClassifier p)))))))
(assert (forall((p K_Classifier))(=> (or  (Professional p) (Doctor p) (Nurse p) (Director p)) (or  (or  (= invalidClassifier p) (= nullClassifier p)) (not (= (Professional_password p) ""))))))
(assert (forall((d K_Classifier))(=> (Doctor d) (or  (and (forall((var1 K_Classifier))(not (Doctor_substitutions d var1))) (not (or  (= invalidClassifier d) (= nullClassifier d)))) (and (= (Doctor_status d) "available") (not (or  (= invalidClassifier d) (= nullClassifier d))))))))
(assert (forall((m K_Classifier))(=> (MedicalCenter m) (not (or  (= nullClassifier (MedicalCenter_director m)) (or  (= invalidClassifier m) (= nullClassifier m)))))))
(assert (forall((p K_Classifier))(=> (or  (Professional p) (Doctor p) (Nurse p) (Director p)) (not (or  (= nullString (Professional_surname p)) (or  (= invalidClassifier p) (= nullClassifier p)))))))
(assert (forall((p K_Classifier))(=> (or  (Professional p) (Doctor p) (Nurse p) (Director p)) (not (or  (= nullString (Professional_login p)) (or  (= invalidClassifier p) (= nullClassifier p)))))))
(assert (forall((p K_Classifier))(=> (or  (Professional p) (Doctor p) (Nurse p) (Director p)) (or  (or  (= invalidClassifier p) (= nullClassifier p)) (not (= (Professional_login p) ""))))))
(assert (forall((p1 K_Classifier))(=> (or  (Professional p1) (Doctor p1) (Nurse p1) (Director p1)) (forall((p2 K_Classifier))(=> (or  (Professional p2) (Doctor p2) (Nurse p2) (Director p2)) (or  (and (= p1 p2) (not (= invalidClassifier p1))) (or  (or  (= invalidClassifier p1) (= nullClassifier p1)) (not (= (Professional_login p1) (Professional_login p2))))))))))
(assert (forall((p K_Classifier))(=> (or  (Professional p) (Doctor p) (Nurse p) (Director p)) (not (or  (= nullString (Professional_password p)) (or  (= invalidClassifier p) (= nullClassifier p)))))))
(assert (exists ((var1 K_Classifier))(Director var1)))
(assert (exists ((var1 K_Classifier))(Doctor var1)))
(assert (forall((d1 K_Classifier))(=> (Doctor d1) (forall((d2 K_Classifier))(=> (Doctor d2) (or  (and (= d1 d2) (not (= invalidClassifier d1))) (or  (or  (= invalidClassifier d1) (= nullClassifier d1)) (not (= (Doctor_license d1) (Doctor_license d2))))))))))
(assert (forall((d K_Classifier))(=> (Doctor d) (or  (or  (or  (= invalidClassifier d) (= nullClassifier d)) (not (= (Doctor_status d) "unavailable"))) (and (not (or  (= nullClassifier (Doctor_substitutedBy d)) (or  (= invalidClassifier d) (= nullClassifier d)))) (or  (or  (= invalidClassifier d) (= nullClassifier d)) (not (= (Doctor_substitutedBy d) d))))))))
(assert (forall((d K_Classifier))(=> (Doctor d) (or  (or  (or  (= invalidClassifier d) (= nullClassifier d)) (not (= (Doctor_status d) "available"))) (or  (= nullClassifier (Doctor_substitutedBy d)) (or  (= invalidClassifier d) (= nullClassifier d)))))))
(assert (exists ((var1 K_Classifier))(Nurse var1)))
(assert (forall((n K_Classifier))(=> (Nurse n) (not (or  (= nullInt (Nurse_license n)) (or  (= invalidClassifier n) (= nullClassifier n)))))))
(assert (forall((n1 K_Classifier))(=> (Nurse n1) (forall((n2 K_Classifier))(=> (Nurse n2) (or  (and (= n1 n2) (not (= invalidClassifier n1))) (or  (or  (= invalidClassifier n1) (= nullClassifier n1)) (not (= (Nurse_license n1) (Nurse_license n2))))))))))
(assert (exists ((var1 K_Classifier))(Referral var1)))
(assert (forall((r K_Classifier))(=> (Referral r) (and (not (or  (= nullClassifier (Referral_patient r)) (or  (= invalidClassifier r) (= nullClassifier r)))) (not (or  (= nullClassifier (Referral_referredBy r)) (or  (= invalidClassifier r) (= nullClassifier r))))))))
(assert (forall((r K_Classifier))(=> (Referral r) (or  (and (or  (= nullClassifier (Referral_patient r)) (or  (= invalidClassifier r) (= nullClassifier r))) (or  (= nullClassifier (Referral_referringTo r)) (or  (= invalidClassifier r) (= nullClassifier r)))) (or  (or  (= invalidClassifier r) (= nullClassifier r)) (not (= (Referral_referringTo r) (Referral_referredBy r))))))))
(assert (forall((r1 K_Classifier))(=> (Referral r1) (forall((r2 K_Classifier))(=> (Referral r2) (or  (and (= r1 r2) (not (= invalidClassifier r1))) (or  (or  (or  (or  (= invalidClassifier r1) (= nullClassifier r1)) (not (= (Referral_patient r1) (Referral_patient r2)))) (or  (or  (= invalidClassifier r1) (= nullClassifier r1)) (not (= (Referral_referringTo r1) (Referral_referringTo r2))))) (or  (or  (= invalidClassifier r1) (= nullClassifier r1)) (not (= (Referral_referredBy r1) (Referral_referredBy r2)))))))))))
(assert (exists ((var1 K_Classifier))(Patient var1)))
(assert (forall((p K_Classifier))(=> (Patient p) (and (exists ((d K_Classifier))(and (Department_doctors d (Patient_doctor p)) (and (= d (Patient_department p)) (not (= invalidClassifier d))))) (not (or  (or  (= invalidClassifier p) (= nullClassifier p)) (= nullClassifier (Patient_doctor p))))))))
(assert (forall((p K_Classifier))(=> (Patient p) (not (or  (= nullClassifier (Patient_doctor p)) (or  (= invalidClassifier p) (= nullClassifier p)))))))
(assert (forall((p K_Classifier))(=> (Patient p) (not (or  (= nullClassifier (Patient_department p)) (or  (= invalidClassifier p) (= nullClassifier p)))))))
(assert (forall((p K_Classifier))(=> (Patient p) (not (or  (= nullClassifier (Patient_contactInfo p)) (or  (= invalidClassifier p) (= nullClassifier p)))))))
(assert (exists ((var1 K_Classifier))(ContactInfo var1)))
(assert (exists ((p K_Classifier))(and (Doctor p) (forall((q K_Classifier))(=> (Doctor q) (and (= p q) (not (= invalidClassifier p))))))))
;
 ; Invariant to check 
;
(assert true)
(check-sat)
(get-model)