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

==> Step 1:
Target User: user1
CAN ASSIGN rule applied to user1: <role5,TRUE,role0>
Administrative user to invoke the rule: user9
Role configuration of user1 before applying rule: No role
Role configuration of user1 after applying rule: role0

==> Step 2:
Target User: user1
CAN ASSIGN rule applied to user1: <role5,role0&-role2,role1>
Administrative user to invoke the rule: user9
Role configuration of user1 before applying rule: role0
Role configuration of user1 after applying rule: role0 role1

user1 can REACH role1
role1 is REACHABLE