; Declare options and fixedpoint (set-logic HORN) ;---------- FUNCTION DECLARATION --------- ; Declare the relations, each relation manage one intended user (declare-fun u0 (Int Int Int Int Int) Bool) (declare-fun u1 (Int Int Int Int Int) Bool) ;---------- INITIALIZE VARIABLES --------- (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (= b_0 0) (= track_0_Patient 0) (= track_0_PrimaryDoctor 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (= b_1 0) (= track_1_Patient 0) (= track_1_PrimaryDoctor 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) ;---------- CONFIGURATION_USERS --------- ; Configuration of user0 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Patient 0) (= track_0_PrimaryDoctor 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Patient 0) (= track_1_PrimaryDoctor 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) ; Configuration of user1 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Patient 0) (= track_0_PrimaryDoctor 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Patient 0) (= track_1_PrimaryDoctor 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) ; Configuration of SUPER_USER (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (track_0_SUPER_ROLE_1 Int)) (=> (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Patient 0) (= track_0_PrimaryDoctor 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0) (= track_0_SUPER_ROLE_1 1)) (u0 b_0_1 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE_1)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int) (track_1_SUPER_ROLE_1 Int)) (=> (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Patient 0) (= track_1_PrimaryDoctor 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0) (= track_1_SUPER_ROLE_1 1)) (u1 b_1_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE_1)))) ; Configuration of user101 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_PrimaryDoctor_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Patient 0) (= track_0_PrimaryDoctor 0) (= track_0_PrimaryDoctor_1 1) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Patient track_0_PrimaryDoctor_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_PrimaryDoctor_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Patient 0) (= track_1_PrimaryDoctor 0) (= track_1_PrimaryDoctor_1 1) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Patient track_1_PrimaryDoctor_1 track_1_target track_1_SUPER_ROLE)))) ; Configuration of user102 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_PrimaryDoctor_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Patient 0) (= track_0_PrimaryDoctor 0) (= track_0_PrimaryDoctor_1 1) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Patient track_0_PrimaryDoctor_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_PrimaryDoctor_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Patient 0) (= track_1_PrimaryDoctor 0) (= track_1_PrimaryDoctor_1 1) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Patient track_1_PrimaryDoctor_1 track_1_target track_1_SUPER_ROLE)))) ; Configuration of user331 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Patient Int) (track_0_Patient_1 Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Patient 0) (= track_0_Patient_1 1) (= track_0_PrimaryDoctor 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Patient_1 track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Patient Int) (track_1_Patient_1 Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Patient 0) (= track_1_Patient_1 1) (= track_1_PrimaryDoctor 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Patient_1 track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) ; Configuration of user332 (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_Patient Int) (track_0_Patient_1 Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 0) (= b_0_1 1) (= track_0_Patient 0) (= track_0_Patient_1 1) (= track_0_PrimaryDoctor 0) (= track_0_target 0) (= track_0_SUPER_ROLE 0)) (u0 b_0_1 track_0_Patient_1 track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_Patient Int) (track_1_Patient_1 Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 0) (= b_1_1 1) (= track_1_Patient 0) (= track_1_Patient_1 1) (= track_1_PrimaryDoctor 0) (= track_1_target 0) (= track_1_SUPER_ROLE 0)) (u1 b_1_1 track_1_Patient_1 track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) ;---------- SIMULATION OF RULES --------- ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_target_1 Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_PrimaryDoctor 1) (= track_0_Patient 1) (= track_0_target 0) (= track_0_target_1 1))(u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target_1 track_0_SUPER_ROLE)))) (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_target_1 Int) (track_0_SUPER_ROLE Int) (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_PrimaryDoctor 1) (= track_0_Patient 1) (= track_0_target 0) (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= track_0_target_1 1))(u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target_1 track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_target_1 Int) (track_1_SUPER_ROLE Int) (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_PrimaryDoctor 1) (= track_1_Patient 1) (= track_1_target 0) (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= track_1_target_1 1))(u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target_1 track_1_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_target_1 Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_PrimaryDoctor 1) (= track_1_Patient 1) (= track_1_target 0) (= track_1_target_1 1))(u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target_1 track_1_SUPER_ROLE)))) ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_PrimaryDoctor_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_Patient 0) (= track_0_PrimaryDoctor 0) (= track_0_PrimaryDoctor_1 1))(u0 b_0 track_0_Patient track_0_PrimaryDoctor_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_PrimaryDoctor_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_Patient 0) (= track_0_PrimaryDoctor 0) (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= track_0_PrimaryDoctor_1 1))(u0 b_0 track_0_Patient track_0_PrimaryDoctor_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_PrimaryDoctor_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int) (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_Patient 0) (= track_1_PrimaryDoctor 0) (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= track_1_PrimaryDoctor_1 1))(u1 b_1 track_1_Patient track_1_PrimaryDoctor_1 track_1_target track_1_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_PrimaryDoctor_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_Patient 0) (= track_1_PrimaryDoctor 0) (= track_1_PrimaryDoctor_1 1))(u1 b_1 track_1_Patient track_1_PrimaryDoctor_1 track_1_target track_1_SUPER_ROLE)))) ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_Patient_1 Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_PrimaryDoctor 0) (= track_0_Patient 0) (= track_0_Patient_1 1))(u0 b_0 track_0_Patient_1 track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_Patient_1 Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_PrimaryDoctor 0) (= track_0_Patient 0) (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= track_0_Patient_1 1))(u0 b_0 track_0_Patient_1 track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_Patient_1 Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int) (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_PrimaryDoctor 0) (= track_1_Patient 0) (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= track_1_Patient_1 1))(u1 b_1 track_1_Patient_1 track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_Patient_1 Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_PrimaryDoctor 0) (= track_1_Patient 0) (= track_1_Patient_1 1))(u1 b_1 track_1_Patient_1 track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) ;-----------------------Can revoke rule------------------------ ;----------- ;------------------------------------------------------------ (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_PrimaryDoctor_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_PrimaryDoctor 1) (= track_0_PrimaryDoctor_1 0))(u0 b_0 track_0_Patient track_0_PrimaryDoctor_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_PrimaryDoctor_1 Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_PrimaryDoctor 1) (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= track_0_PrimaryDoctor_1 0))(u0 b_0 track_0_Patient track_0_PrimaryDoctor_1 track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_PrimaryDoctor_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int) (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_PrimaryDoctor 1) (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= track_1_PrimaryDoctor_1 0))(u1 b_1 track_1_Patient track_1_PrimaryDoctor_1 track_1_target track_1_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_PrimaryDoctor_1 Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_PrimaryDoctor 1) (= track_1_PrimaryDoctor_1 0))(u1 b_1 track_1_Patient track_1_PrimaryDoctor_1 track_1_target track_1_SUPER_ROLE)))) ;-----------------------Can revoke rule------------------------ ;----------- ;------------------------------------------------------------ (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_Patient_1 Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_Patient 1) (= track_0_Patient_1 0))(u0 b_0 track_0_Patient_1 track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_0 Int) (track_0_Patient Int) (track_0_Patient_1 Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int) (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_Patient 1) (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= track_0_Patient_1 0))(u0 b_0 track_0_Patient_1 track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_Patient_1 Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int) (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (=> (and (and (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_Patient 1) (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= track_1_Patient_1 0))(u1 b_1 track_1_Patient_1 track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) (assert (forall ( (b_1 Int) (track_1_Patient Int) (track_1_Patient_1 Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (=> (and (and (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_Patient 1) (= track_1_Patient_1 0))(u1 b_1 track_1_Patient_1 track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE)))) ;------------- The query ------------ (assert (not (exists ( (b_0 Int) (track_0_Patient Int) (track_0_PrimaryDoctor Int) (track_0_target Int) (track_0_SUPER_ROLE Int)) (and (= track_0_target 1) (u0 b_0 track_0_Patient track_0_PrimaryDoctor track_0_target track_0_SUPER_ROLE))))) (assert (not (exists ( (b_1 Int) (track_1_Patient Int) (track_1_PrimaryDoctor Int) (track_1_target Int) (track_1_SUPER_ROLE Int)) (and (= track_1_target 1) (u1 b_1 track_1_Patient track_1_PrimaryDoctor track_1_target track_1_SUPER_ROLE))))) (check-sat)