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

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

==> Step 2:
Target User: user0
CAN ASSIGN rule applied to user0: <Admin,Employee&-ST1&-OB1&-SE1,FA1>
Administrative user to invoke the rule: user1
Role configuration of user0 before applying rule: Employee
Role configuration of user0 after applying rule: Employee FA1

==> Step 3:
Target User: user0
CAN ASSIGN rule applied to user0: <Admin,FA1&-FASpecial1&-FAAsst1&-FAJunior1&-FASenior1,FAClerk1>
Administrative user to invoke the rule: user1
Role configuration of user0 before applying rule: Employee FA1
Role configuration of user0 after applying rule: Employee FA1 FAClerk1

==> Step 4:
Target User: user0
CAN ASSIGN rule applied to user0: <Admin,FA1&FAClerk1&-FASpecial1&-FAAsst1&-FAJunior1,FASenior1>
Administrative user to invoke the rule: user1
Role configuration of user0 before applying rule: Employee FA1 FAClerk1
Role configuration of user0 after applying rule: Employee FA1 FAClerk1 FASenior1

==> Step 5:
Target User: user0
CAN ASSIGN rule applied to user0: <Admin,FA1&FASenior1&FAClerk1&-FASpecial1&-FAAsst1,FAJunior1>
Administrative user to invoke the rule: user1
Role configuration of user0 before applying rule: Employee FA1 FAClerk1 FASenior1
Role configuration of user0 after applying rule: Employee FA1 FAClerk1 FASenior1 FAJunior1

==> Step 6:
Target User: user0
CAN ASSIGN rule applied to user0: <Admin,FA1&FAJunior1&FASenior1&FAClerk1&-FAAsst1,FASpecial1>
Administrative user to invoke the rule: user1
Role configuration of user0 before applying rule: Employee FA1 FAClerk1 FASenior1 FAJunior1
Role configuration of user0 after applying rule: Employee FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1

==> Step 7:
Target User: user0
CAN ASSIGN rule applied to user0: <Admin,FAJunior1&FASenior1&FAClerk1&FASpecial1,anyfour1>
Administrative user to invoke the rule: user1
Role configuration of user0 before applying rule: Employee FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1
Role configuration of user0 after applying rule: Employee FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1

==> Step 8:
Target User: user0
CAN ASSIGN rule applied to user0: <Admin,anyfour1,target>
Administrative user to invoke the rule: user1
Role configuration of user0 before applying rule: Employee FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1
Role configuration of user0 after applying rule: Employee FA1 FAClerk1 FASenior1 FAJunior1 FASpecial1 anyfour1 target

user0 can REACH target
target is REACHABLE