; 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 Int Int Int Int) Bool) (declare-fun u1 (Int Int Int Int Int Int Int Int Int) Bool) ;---------- INITIALIZE VARIABLES --------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (= b_0 0) (= track_0_target 0) (= track_0_anyfour1 0) (= track_0_anyfour2 0) (= track_0_anyfour3 0) (= track_0_anyfour4 0) (= track_0_SUPER_ROLE 0) (= track_0_ToCheckRole 0) (= track_0_TargetPrime 0)) (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (= b_1 0) (= track_1_target 0) (= track_1_anyfour1 0) (= track_1_anyfour2 0) (= track_1_anyfour3 0) (= track_1_anyfour4 0) (= track_1_SUPER_ROLE 0) (= track_1_ToCheckRole 0) (= track_1_TargetPrime 0)) (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) ;---------- CONFIGURATION_USERS --------- ; Configuration of SUPER_USER (assert (forall ( (b_0 Int) (b_0_1 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_SUPER_ROLE_1 Int) (track_0_ToCheckRole Int) (track_0_ToCheckRole_1 Int) (track_0_TargetPrime Int)) (=> (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 0) (= b_0_1 1) (= track_0_target 0) (= track_0_anyfour1 0) (= track_0_anyfour2 0) (= track_0_anyfour3 0) (= track_0_anyfour4 0) (= track_0_SUPER_ROLE 0) (= track_0_SUPER_ROLE_1 1) (= track_0_ToCheckRole 0) (= track_0_ToCheckRole_1 1) (= track_0_TargetPrime 0)) (u0 b_0_1 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE_1 track_0_ToCheckRole_1 track_0_TargetPrime)))) ; Configuration of user1 (assert (forall ( (b_1 Int) (b_1_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 0) (= b_1_1 1) (= track_1_target 0) (= track_1_anyfour1 0) (= track_1_anyfour2 0) (= track_1_anyfour3 0) (= track_1_anyfour4 0) (= track_1_SUPER_ROLE 0) (= track_1_ToCheckRole 0) (= track_1_TargetPrime 0)) (u1 b_1_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) ;---------- SIMULATION OF RULES --------- ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour1_1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour1 0) (= track_0_anyfour1_1 1))(u0 b_0 track_0_target track_0_anyfour1_1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour1_1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int) (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour1 0) (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= track_0_anyfour1_1 1))(u0 b_0 track_0_target track_0_anyfour1_1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour1_1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int) (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour1 0) (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= track_1_anyfour1_1 1))(u1 b_1 track_1_target track_1_anyfour1_1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour1_1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour1 0) (= track_1_anyfour1_1 1))(u1 b_1 track_1_target track_1_anyfour1_1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour2_1 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour2 0) (= track_0_anyfour2_1 1))(u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2_1 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour2_1 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int) (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour2 0) (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= track_0_anyfour2_1 1))(u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2_1 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour2_1 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int) (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour2 0) (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= track_1_anyfour2_1 1))(u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2_1 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour2_1 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour2 0) (= track_1_anyfour2_1 1))(u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2_1 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour3_1 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour3 0) (= track_0_anyfour3_1 1))(u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3_1 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour3_1 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int) (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour3 0) (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= track_0_anyfour3_1 1))(u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3_1 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour3_1 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int) (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour3 0) (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= track_1_anyfour3_1 1))(u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3_1 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour3_1 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour3 0) (= track_1_anyfour3_1 1))(u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3_1 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_anyfour4_1 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour4 0) (= track_0_anyfour4_1 1))(u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4_1 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_anyfour4_1 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int) (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour4 0) (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= track_0_anyfour4_1 1))(u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4_1 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_anyfour4_1 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int) (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour4 0) (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= track_1_anyfour4_1 1))(u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4_1 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_anyfour4_1 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour4 0) (= track_1_anyfour4_1 1))(u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4_1 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_target_1 Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour1 1) (= track_0_anyfour2 1) (= track_0_anyfour3 1) (= track_0_anyfour4 1) (= track_0_target 0) (= track_0_target_1 1))(u0 b_0 track_0_target_1 track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_target_1 Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int) (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_0 1) (= track_0_anyfour1 1) (= track_0_anyfour2 1) (= track_0_anyfour3 1) (= track_0_anyfour4 1) (= track_0_target 0) (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= track_0_target_1 1))(u0 b_0 track_0_target_1 track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_target_1 Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int) (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour1 1) (= track_1_anyfour2 1) (= track_1_anyfour3 1) (= track_1_anyfour4 1) (= track_1_target 0) (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= track_1_target_1 1))(u1 b_1 track_1_target_1 track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_target_1 Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_SUPER_ROLE 1)) (= b_1 1) (= track_1_anyfour1 1) (= track_1_anyfour2 1) (= track_1_anyfour3 1) (= track_1_anyfour4 1) (= track_1_target 0) (= track_1_target_1 1))(u1 b_1 track_1_target_1 track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime)))) ;--------------------------Can assign rule------------------------ ;--------- ;--------------------------------------------------------------- (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int) (track_0_TargetPrime_1 Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_ToCheckRole 1)) (= b_0 1) (= track_0_ToCheckRole 1) (= track_0_target 1) (= track_0_TargetPrime 0) (= track_0_TargetPrime_1 1))(u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime_1)))) (assert (forall ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int) (track_0_TargetPrime_1 Int) (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_ToCheckRole 1)) (= b_0 1) (= track_0_ToCheckRole 1) (= track_0_target 1) (= track_0_TargetPrime 0) (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= track_0_TargetPrime_1 1))(u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime_1)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int) (track_1_TargetPrime_1 Int) (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (=> (and (and (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime) (= b_0 1) (= track_0_ToCheckRole 1)) (= b_1 1) (= track_1_ToCheckRole 1) (= track_1_target 1) (= track_1_TargetPrime 0) (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= track_1_TargetPrime_1 1))(u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime_1)))) (assert (forall ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int) (track_1_TargetPrime_1 Int)) (=> (and (and (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime) (= b_1 1) (= track_1_ToCheckRole 1)) (= b_1 1) (= track_1_ToCheckRole 1) (= track_1_target 1) (= track_1_TargetPrime 0) (= track_1_TargetPrime_1 1))(u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime_1)))) ;------------- The query ------------ (assert (not (exists ( (b_0 Int) (track_0_target Int) (track_0_anyfour1 Int) (track_0_anyfour2 Int) (track_0_anyfour3 Int) (track_0_anyfour4 Int) (track_0_SUPER_ROLE Int) (track_0_ToCheckRole Int) (track_0_TargetPrime Int)) (and (= track_0_TargetPrime 1) (u0 b_0 track_0_target track_0_anyfour1 track_0_anyfour2 track_0_anyfour3 track_0_anyfour4 track_0_SUPER_ROLE track_0_ToCheckRole track_0_TargetPrime))))) (assert (not (exists ( (b_1 Int) (track_1_target Int) (track_1_anyfour1 Int) (track_1_anyfour2 Int) (track_1_anyfour3 Int) (track_1_anyfour4 Int) (track_1_SUPER_ROLE Int) (track_1_ToCheckRole Int) (track_1_TargetPrime Int)) (and (= track_1_TargetPrime 1) (u1 b_1 track_1_target track_1_anyfour1 track_1_anyfour2 track_1_anyfour3 track_1_anyfour4 track_1_SUPER_ROLE track_1_ToCheckRole track_1_TargetPrime))))) (check-sat)