Counter Example Trace:
Specification of query: Can user0 REACH role1 ?

==> Step 1:
Target User: user0
CAN ASSIGN rule applied to user0: <role3,TRUE,role1>
Administrative user to invoke the rule: user4
Role configuration of user0 before applying rule: No role
Role configuration of user0 after applying rule: role1

user0 can REACH role1
role1 is REACHABLE