Commit 2a599ab7 authored by Jonathan Shahen's avatar Jonathan Shahen

Testsuite B and Testsuite C

parent 93da7dd0
/* Generated On : 2015/02/07 20:24:54.341
* Generated With : Mohawk Reverse Converter: ASAPTime SA
* Number of Roles : 30
* Number of Timeslots : 5
* Number of Rules : 229
*
* Roles : |Size=30| [role1, role2, role3, role4, role5, role6, role7, role8, role9, role10, role11, role12, role13, role14, role15, role16, role17, role18, role19, role20, role21, role23, role24, role25, role26, role27, role28, role29, role31, role32]
* Timeslots : |Size=5| [t1, t2, t3, t4, t5]
*
*
* TESTCASE COMMENTS:
*
*/
Query: t5, [role7]
Expected: UNKNOWN
/*
* Number of Rules : 229
* Largest Precondition : 4
* Largest Role Schedule : 1
* Startable Rules : 3
* Truly Startable Rules : 3
*/
CanAssign {
/* 1 */ <TRUE, t2, role8, t2, role1>
/* 2 */ <TRUE, t1, role8, t3, role1>
/* 3 */ <TRUE, t5, role8, t4, role1>
/* 4 */ <TRUE, t3, role28, t3, role1>
/* 5 */ <TRUE, t1, role28, t5, role1>
/* 6 */ <TRUE, t2, NOT ~ role16, t4, role1>
/* 7 */ <TRUE, t1, role16, t5, role1>
/* 8 */ <TRUE, t3, role3, t2, role1>
/* 9 */ <TRUE, t1, role15 & NOT ~ role6 & NOT ~ role2 & NOT ~ role5, t5, role1>
/* 10 */ <TRUE, t4, role29 & NOT ~ role4 & NOT ~ role6 & NOT ~ role5, t2, role1>
/* 11 */ <TRUE, t2, role29 & NOT ~ role4 & NOT ~ role6 & NOT ~ role5, t3, role1>
/* 12 */ <TRUE, t2, role32, t3, role1>
/* 13 */ <TRUE, t5, role32, t4, role1>
/* 14 */ <TRUE, t1, role32, t1, role1>
/* 15 */ <TRUE, t3, role26 & NOT ~ role5 & NOT ~ role3 & NOT ~ role4, t3, role1>
/* 16 */ <TRUE, t1, role12 & NOT ~ role1 & NOT ~ role1 & NOT ~ role5, t3, role3>
/* 17 */ <TRUE, t2, role12 & NOT ~ role1 & NOT ~ role1 & NOT ~ role5, t4, role3>
/* 18 */ <TRUE, t4, role7, t1, role4>
/* 19 */ <TRUE, t5, role32 & NOT ~ role3 & NOT ~ role4 & NOT ~ role7, t1, role5>
/* 20 */ <TRUE, t1, role32 & NOT ~ role3 & NOT ~ role4 & NOT ~ role7, t5, role5>
/* 21 */ <TRUE, t3, role32 & NOT ~ role3 & NOT ~ role4 & NOT ~ role7, t2, role5>
/* 22 */ <TRUE, t3, role8, t5, role6>
/* 23 */ <TRUE, t4, role8, t4, role6>
/* 24 */ <TRUE, t2, role21, t2, role6>
/* 25 */ <TRUE, t2, role16, t2, role6>
/* 26 */ <TRUE, t3, role16, t3, role6>
/* 27 */ <TRUE, t5, role10, t3, role6>
/* 28 */ <TRUE, t3, role5, t5, role6>
/* 29 */ <TRUE, t4, role5, t2, role6>
/* 30 */ <TRUE, t2, role5, t4, role6>
/* 31 */ <TRUE, t4, role26, t1, role6>
/* 32 */ <TRUE, t5, role31, t3, role6>
/* 33 */ <TRUE, t2, role31, t4, role6>
/* 34 */ <TRUE, t1, role31, t2, role6>
/* 35 */ <TRUE, t1, role16, t3, role6>
/* 36 */ <TRUE, t3, role23 & NOT ~ role4 & NOT ~ role2 & NOT ~ role8, t1, role7>
/* 37 */ <TRUE, t5, role23 & NOT ~ role4 & NOT ~ role2 & NOT ~ role8, t5, role7>
/* 38 */ <TRUE, t4, role23 & NOT ~ role4 & NOT ~ role2 & NOT ~ role8, t2, role7>
/* 39 */ <TRUE, t5, role19 & role12, t5, role24>
/* 40 */ <TRUE, t4, role1, t5, role13>
/* 41 */ <TRUE, t3, role1, t5, role14>
/* 42 */ <TRUE, t4, role1, t5, role15>
/* 43 */ <TRUE, t4, role1, t5, role16>
/* 44 */ <TRUE, t5, role14, t5, role21>
/* 45 */ <TRUE, t4, role19, t5, role11>
/* 46 */ <TRUE, t1, role19 & NOT ~ role31, t5, role12>
/* 47 */ <TRUE, t3, role13, t5, role13>
/* 48 */ <TRUE, t4, role13, t5, role14>
/* 49 */ <TRUE, t3, role13, t5, role15>
/* 50 */ <TRUE, t5, role13, t5, role16>
/* 51 */ <TRUE, t1, role19, t5, role17>
/* 52 */ <TRUE, t2, role13, t5, role18>
/* 53 */ <TRUE, t3, role12 & NOT ~ role11, t5, role31>
/* 54 */ <TRUE, t4, role11 & NOT ~ role12, t5, role31>
/* 55 */ <TRUE, t1, role14 & NOT ~ role13, t5, role31>
/* 56 */ <TRUE, t2, role13 & NOT ~ role14, t5, role31>
/* 57 */ <TRUE, t2, role16 & NOT ~ role15, t5, role31>
/* 58 */ <TRUE, t3, role15 & NOT ~ role16, t5, role31>
/* 59 */ <TRUE, t5, role20 & NOT ~ role19, t5, role31>
/* 60 */ <TRUE, t3, role31 & NOT ~ role21, t5, role12>
/* 61 */ <TRUE, t5, role21, t5, role15>
/* 62 */ <TRUE, t4, TRUE, t5, role1>
/* 63 */ <TRUE, t2, TRUE, t5, role19>
/* 64 */ <TRUE, t1, role4, t5, role8>
/* 65 */ <TRUE, t1, role5, t2, role8>
/* 66 */ <TRUE, t4, role5, t1, role8>
/* 67 */ <TRUE, t3, role5, t4, role8>
/* 68 */ <TRUE, t4, role12 & NOT ~ role7 & NOT ~ role2 & NOT ~ role7, t5, role8>
/* 69 */ <TRUE, t1, role12 & NOT ~ role7 & NOT ~ role2 & NOT ~ role7, t3, role8>
/* 70 */ <TRUE, t3, role12 & NOT ~ role7 & NOT ~ role2 & NOT ~ role7, t4, role8>
/* 71 */ <TRUE, t1, role21 & NOT ~ role7 & NOT ~ role7 & NOT ~ role5, t1, role8>
/* 72 */ <TRUE, t4, role21 & NOT ~ role7 & NOT ~ role7 & NOT ~ role5, t2, role8>
/* 73 */ <TRUE, t2, role21 & NOT ~ role7 & NOT ~ role7 & NOT ~ role5, t3, role8>
/* 74 */ <TRUE, t2, role23, t3, role8>
/* 75 */ <TRUE, t4, role23, t1, role8>
/* 76 */ <TRUE, t3, role23, t2, role8>
/* 77 */ <TRUE, t3, role27, t5, role8>
/* 78 */ <TRUE, t4, role27, t1, role8>
/* 79 */ <TRUE, t5, role27, t2, role8>
/* 80 */ <TRUE, t5, role31, t4, role8>
/* 81 */ <TRUE, t1, role31, t3, role8>
/* 82 */ <TRUE, t3, role17 & NOT ~ role5 & NOT ~ role6 & NOT ~ role5, t1, role8>
/* 83 */ <TRUE, t1, role17 & NOT ~ role5 & NOT ~ role6 & NOT ~ role5, t2, role8>
/* 84 */ <TRUE, t4, role17 & NOT ~ role5 & NOT ~ role6 & NOT ~ role5, t3, role8>
/* 85 */ <TRUE, t1, role16 & NOT ~ role2 & NOT ~ role3 & NOT ~ role1, t2, role9>
/* 86 */ <TRUE, t5, role28, t4, role10>
/* 87 */ <TRUE, t2, role28, t3, role10>
/* 88 */ <TRUE, t1, role28, t5, role10>
/* 89 */ <TRUE, t2, role32, t4, role11>
/* 90 */ <TRUE, t5, role32, t3, role11>
/* 91 */ <TRUE, t1, role3, t4, role12>
/* 92 */ <TRUE, t4, role32, t1, role13>
/* 93 */ <TRUE, t3, role32, t2, role13>
/* 94 */ <TRUE, t1, role11, t3, role13>
/* 95 */ <TRUE, t4, role4 & NOT ~ role5 & NOT ~ role2 & NOT ~ role3, t2, role13>
/* 96 */ <TRUE, t5, role31, t3, role13>
/* 97 */ <TRUE, t4, role31, t5, role13>
/* 98 */ <TRUE, t1, role31, t4, role13>
/* 99 */ <TRUE, t5, role21, t2, role13>
/* 100 */ <TRUE, t4, role21, t4, role13>
/* 101 */ <TRUE, t1, role21, t5, role13>
/* 102 */ <TRUE, t1, role19, t5, role13>
/* 103 */ <TRUE, t4, role19, t3, role13>
/* 104 */ <TRUE, t2, role19, t1, role13>
/* 105 */ <TRUE, t2, role17, t5, role13>
/* 106 */ <TRUE, t3, role1, t3, role13>
/* 107 */ <TRUE, t1, role5, t2, role13>
/* 108 */ <TRUE, t2, role5, t5, role13>
/* 109 */ <TRUE, t3, role5, t1, role13>
/* 110 */ <TRUE, t4, role16, t4, role15>
/* 111 */ <TRUE, t5, role16, t3, role15>
/* 112 */ <TRUE, t1, role16, t5, role15>
/* 113 */ <TRUE, t3, role10 & NOT ~ role7 & NOT ~ role6 & NOT ~ role8, t2, role16>
/* 114 */ <TRUE, t4, role23 & NOT ~ role7 & NOT ~ role1 & NOT ~ role8, t3, role17>
/* 115 */ <TRUE, t5, role13, t4, role17>
/* 116 */ <TRUE, t4, role15 & NOT ~ role4 & NOT ~ role1 & NOT ~ role7, t5, role17>
/* 117 */ <TRUE, t5, role13, t2, role17>
/* 118 */ <TRUE, t2, role19, t4, role17>
/* 119 */ <TRUE, t4, role19, t2, role17>
/* 120 */ <TRUE, t1, role26, t4, role17>
/* 121 */ <TRUE, t1, role16, t4, role17>
/* 122 */ <TRUE, t2, role16, t3, role17>
/* 123 */ <TRUE, t3, role16, t1, role17>
/* 124 */ <TRUE, t4, role6, t1, role17>
/* 125 */ <TRUE, t1, role6, t2, role17>
/* 126 */ <TRUE, t2, role25, t5, role17>
/* 127 */ <TRUE, t1, role25, t1, role17>
/* 128 */ <TRUE, t3, role25, t2, role17>
/* 129 */ <TRUE, t2, role5, t4, role18>
/* 130 */ <TRUE, t4, role5, t2, role18>
/* 131 */ <TRUE, t2, role23, t3, role18>
/* 132 */ <TRUE, t3, role5, t1, role18>
/* 133 */ <TRUE, t2, role5, t2, role18>
/* 134 */ <TRUE, t4, role5, t3, role18>
/* 135 */ <TRUE, t5, role21 & NOT ~ role3 & NOT ~ role3 & NOT ~ role8, t1, role18>
/* 136 */ <TRUE, t2, role21 & NOT ~ role3 & NOT ~ role3 & NOT ~ role8, t4, role18>
/* 137 */ <TRUE, t1, role21 & NOT ~ role3 & NOT ~ role3 & NOT ~ role8, t5, role18>
/* 138 */ <TRUE, t5, role7, t5, role18>
/* 139 */ <TRUE, t1, role19 & NOT ~ role3 & NOT ~ role1 & NOT ~ role5, t2, role18>
/* 140 */ <TRUE, t5, role19 & NOT ~ role3 & NOT ~ role1 & NOT ~ role5, t5, role18>
/* 141 */ <TRUE, t2, role19 & NOT ~ role3 & NOT ~ role1 & NOT ~ role5, t3, role18>
/* 142 */ <TRUE, t5, role15, t5, role18>
/* 143 */ <TRUE, t1, role15, t1, role18>
/* 144 */ <TRUE, t2, role15, t2, role18>
/* 145 */ <TRUE, t5, role28, t1, role18>
/* 146 */ <TRUE, t2, role28, t2, role18>
/* 147 */ <TRUE, t2, role10 & NOT ~ role3 & NOT ~ role5 & NOT ~ role3, t1, role19>
/* 148 */ <TRUE, t5, role10 & NOT ~ role3 & NOT ~ role5 & NOT ~ role3, t2, role19>
/* 149 */ <TRUE, t3, role10 & NOT ~ role3 & NOT ~ role5 & NOT ~ role3, t3, role19>
/* 150 */ <TRUE, t2, role9, t5, role19>
/* 151 */ <TRUE, t3, role9, t2, role19>
/* 152 */ <TRUE, t3, role23 & NOT ~ role4 & NOT ~ role2 & NOT ~ role4, t3, role19>
/* 153 */ <TRUE, t1, role23 & NOT ~ role4 & NOT ~ role2 & NOT ~ role4, t1, role19>
/* 154 */ <TRUE, t4, role4, t1, role19>
/* 155 */ <TRUE, t1, role4, t5, role19>
/* 156 */ <TRUE, t3, role25, t5, role19>
/* 157 */ <TRUE, t4, role25, t4, role19>
/* 158 */ <TRUE, t5, role25, t1, role19>
/* 159 */ <TRUE, t4, role27, t5, role19>
/* 160 */ <TRUE, t3, role27, t3, role19>
/* 161 */ <TRUE, t5, role3, t5, role19>
/* 162 */ <TRUE, t5, role6, t2, role19>
/* 163 */ <TRUE, t1, role6, t5, role19>
/* 164 */ <TRUE, t2, role16, t3, role20>
/* 165 */ <TRUE, t3, role16, t1, role20>
/* 166 */ <TRUE, t1, role6, t4, role21>
/* 167 */ <TRUE, t5, role6, t1, role21>
/* 168 */ <TRUE, t3, role6, t2, role21>
/* 169 */ <TRUE, t3, role18, t2, role21>
/* 170 */ <TRUE, t4, role16, t3, role21>
/* 171 */ <TRUE, t5, role16, t1, role21>
/* 172 */ <TRUE, t1, role16, t2, role21>
/* 173 */ <TRUE, t5, role3 & NOT ~ role5 & NOT ~ role4 & NOT ~ role4, t2, role21>
/* 174 */ <TRUE, t1, role3 & NOT ~ role5 & NOT ~ role4 & NOT ~ role4, t3, role21>
/* 175 */ <TRUE, t5, role29, t5, role21>
/* 176 */ <TRUE, t1, role29, t4, role21>
/* 177 */ <TRUE, t2, role10, t3, role21>
/* 178 */ <TRUE, t1, role20, t4, role21>
/* 179 */ <TRUE, t2, role20, t5, role21>
/* 180 */ <TRUE, t4, role20, t2, role21>
/* 181 */ <TRUE, t4, role25 & NOT ~ role2 & NOT ~ role4 & NOT ~ role8, t1, role21>
/* 182 */ <TRUE, t3, role25 & NOT ~ role2 & NOT ~ role4 & NOT ~ role8, t4, role21>
/* 183 */ <TRUE, t5, role25 & NOT ~ role2 & NOT ~ role4 & NOT ~ role8, t2, role21>
/* 184 */ <TRUE, t3, role3, t4, role23>
/* 185 */ <TRUE, t1, role3, t1, role23>
/* 186 */ <TRUE, t2, role3, t2, role23>
/* 187 */ <TRUE, t2, role1, t5, role23>
/* 188 */ <TRUE, t3, role1, t4, role23>
/* 189 */ <TRUE, t5, role10, t3, role23>
/* 190 */ <TRUE, t2, role10, t4, role23>
/* 191 */ <TRUE, t3, role10, t5, role23>
/* 192 */ <TRUE, t2, role21, t4, role23>
/* 193 */ <TRUE, t3, role21, t5, role23>
/* 194 */ <TRUE, t1, role18 & NOT ~ role1 & NOT ~ role7 & NOT ~ role6, t2, role23>
/* 195 */ <TRUE, t4, role28 & NOT ~ role6 & NOT ~ role4 & NOT ~ role8, t5, role23>
/* 196 */ <TRUE, t1, role28 & NOT ~ role6 & NOT ~ role4 & NOT ~ role8, t1, role23>
/* 197 */ <TRUE, t2, role27 & NOT ~ role7 & NOT ~ role2 & NOT ~ role6, t4, role23>
/* 198 */ <TRUE, t4, role27 & NOT ~ role7 & NOT ~ role2 & NOT ~ role6, t1, role23>
/* 199 */ <TRUE, t4, role29 & NOT ~ role7 & NOT ~ role6 & NOT ~ role5, t1, role25>
/* 200 */ <TRUE, t3, role29 & NOT ~ role7 & NOT ~ role6 & NOT ~ role5, t5, role25>
/* 201 */ <TRUE, t1, role29 & NOT ~ role7 & NOT ~ role6 & NOT ~ role5, t3, role25>
/* 202 */ <TRUE, t3, role18, t5, role26>
/* 203 */ <TRUE, t1, role18, t2, role26>
/* 204 */ <TRUE, t4, role23, t3, role27>
/* 205 */ <TRUE, t5, role23, t1, role27>
/* 206 */ <TRUE, t2, role21, t5, role28>
/* 207 */ <TRUE, t3, role21, t4, role28>
/* 208 */ <TRUE, t1, role21, t1, role28>
/* 209 */ <TRUE, t5, role17, t3, role29>
/* 210 */ <TRUE, t3, role17, t1, role29>
/* 211 */ <TRUE, t3, role32, t3, role31>
/* 212 */ <TRUE, t2, role32, t5, role31>
/* 213 */ <TRUE, t5, role32, t1, role31>
/* 214 */ <TRUE, t5, role9, t4, role31>
/* 215 */ <TRUE, t1, role16, t4, role31>
/* 216 */ <TRUE, t3, role16, t1, role31>
/* 217 */ <TRUE, t2, role16, t2, role31>
/* 218 */ <TRUE, t4, role7, t1, role31>
/* 219 */ <TRUE, t1, role7, t5, role31>
/* 220 */ <TRUE, t3, role7, t2, role31>
/* 221 */ <TRUE, t5, role25, t4, role31>
/* 222 */ <TRUE, t3, role25, t2, role31>
/* 223 */ <TRUE, t4, role25, t3, role31>
/* 224 */ <TRUE, t4, role25 & NOT ~ role6 & NOT ~ role5 & NOT ~ role4, t4, role31>
/* 225 */ <TRUE, t2, role25 & NOT ~ role6 & NOT ~ role5 & NOT ~ role4, t5, role31>
/* 226 */ <TRUE, t4, role12, t3, role31>
/* 227 */ <TRUE, t3, role12, t1, role31>
/* 228 */ <TRUE, t2, role3, t5, role32>
/* 229 */ <TRUE, t4, role3, t2, role32>
}
CanRevoke { }
CanEnable { }
CanDisable { }
\ No newline at end of file
/* Generated On : 2015/02/07 20:24:54.376
* Generated With : Mohawk Reverse Converter: ASAPTime SA
* Number of Roles : 29
* Number of Timeslots : 5
* Number of Rules : 259
*
* Roles : |Size=29| [role1, role2, role3, role4, role5, role6, role7, role8, role9, role10, role11, role12, role13, role14, role15, role16, role18, role19, role20, role21, role22, role23, role24, role25, role27, role29, role30, role31, role32]
* Timeslots : |Size=5| [t1, t2, t3, t4, t5]
*
*
* TESTCASE COMMENTS:
*
*/
Query: t5, [role7]
Expected: UNKNOWN
/*
* Number of Rules : 259
* Largest Precondition : 4
* Largest Role Schedule : 1
* Startable Rules : 13
* Truly Startable Rules : 13
*/
CanAssign {
/* 1 */ <TRUE, t1, role31, t5, role1>
/* 2 */ <TRUE, t3, role31, t1, role1>
/* 3 */ <TRUE, t4, role12, t3, role2>
/* 4 */ <TRUE, t1, role12, t4, role2>
/* 5 */ <TRUE, t4, role1, t5, role2>
/* 6 */ <TRUE, t2, role1, t1, role2>
/* 7 */ <TRUE, t5, role12, t3, role2>
/* 8 */ <TRUE, t1, role12, t2, role2>
/* 9 */ <TRUE, t2, role12, t4, role2>
/* 10 */ <TRUE, t1, role1, t5, role2>
/* 11 */ <TRUE, t2, role1, t3, role2>
/* 12 */ <TRUE, t1, role12, t2, role2>
/* 13 */ <TRUE, t1, role21, t2, role2>
/* 14 */ <TRUE, t5, role21, t5, role2>
/* 15 */ <TRUE, t3, role21, t1, role2>
/* 16 */ <TRUE, t4, role16, t5, role2>
/* 17 */ <TRUE, t3, role16, t1, role2>
/* 18 */ <TRUE, t1, role16, t4, role2>
/* 19 */ <TRUE, t5, role22, t4, role3>
/* 20 */ <TRUE, t4, role22, t2, role3>
/* 21 */ <TRUE, t4, role22, t4, role5>
/* 22 */ <TRUE, t3, role27, t1, role6>
/* 23 */ <TRUE, t4, role27, t4, role6>
/* 24 */ <TRUE, t5, role27, t5, role6>
/* 25 */ <TRUE, t4, role23, t5, role7>
/* 26 */ <TRUE, t5, role19 & role12, t5, role24>
/* 27 */ <TRUE, t5, role14, t5, role21>
/* 28 */ <TRUE, t4, role19, t5, role11>
/* 29 */ <TRUE, t1, role19 & NOT ~ role31, t5, role12>
/* 30 */ <TRUE, t3, role12 & NOT ~ role11, t5, role31>
/* 31 */ <TRUE, t4, role11 & NOT ~ role12, t5, role31>
/* 32 */ <TRUE, t3, role31 & NOT ~ role21, t5, role12>
/* 33 */ <TRUE, t5, role21, t5, role15>
/* 34 */ <TRUE, t4, TRUE, t5, role1>
/* 35 */ <TRUE, t2, TRUE, t5, role19>
/* 36 */ <TRUE, t2, role11, t3, role8>
/* 37 */ <TRUE, t2, role16, t1, role8>
/* 38 */ <TRUE, t4, role13, t3, role8>
/* 39 */ <TRUE, t5, role13, t4, role8>
/* 40 */ <TRUE, t3, TRUE, t5, role8>
/* 41 */ <TRUE, t2, TRUE, t4, role8>
/* 42 */ <TRUE, t1, role18 & NOT ~ role4 & NOT ~ role4 & NOT ~ role5, t4, role8>
/* 43 */ <TRUE, t2, role14 & NOT ~ role7 & NOT ~ role4 & NOT ~ role5, t5, role8>
/* 44 */ <TRUE, t1, role10, t1, role8>
/* 45 */ <TRUE, t2, role32, t5, role8>
/* 46 */ <TRUE, t3, role10 & NOT ~ role5 & NOT ~ role2 & NOT ~ role8, t2, role9>
/* 47 */ <TRUE, t4, role10 & NOT ~ role5 & NOT ~ role2 & NOT ~ role8, t3, role9>
/* 48 */ <TRUE, t5, role10 & NOT ~ role5 & NOT ~ role2 & NOT ~ role8, t4, role9>
/* 49 */ <TRUE, t4, role18, t5, role9>
/* 50 */ <TRUE, t3, role18, t4, role9>
/* 51 */ <TRUE, t5, role18, t1, role9>
/* 52 */ <TRUE, t2, role27, t5, role9>
/* 53 */ <TRUE, t3, role27, t1, role9>
/* 54 */ <TRUE, t3, role16, t2, role9>
/* 55 */ <TRUE, t1, role16, t3, role9>
/* 56 */ <TRUE, t2, role1, t3, role9>
/* 57 */ <TRUE, t1, role1, t1, role9>
/* 58 */ <TRUE, t2, role16 & NOT ~ role7 & NOT ~ role5 & NOT ~ role3, t4, role9>
/* 59 */ <TRUE, t3, role16 & NOT ~ role7 & NOT ~ role5 & NOT ~ role3, t5, role9>
/* 60 */ <TRUE, t4, role3, t4, role9>
/* 61 */ <TRUE, t1, role3, t5, role9>
/* 62 */ <TRUE, t2, role3, t1, role9>
/* 63 */ <TRUE, t4, role18, t5, role9>
/* 64 */ <TRUE, t2, role18, t3, role9>
/* 65 */ <TRUE, t2, role18, t4, role9>
/* 66 */ <TRUE, t1, role7, t4, role10>
/* 67 */ <TRUE, t3, role7, t5, role10>
/* 68 */ <TRUE, t1, role25, t2, role10>
/* 69 */ <TRUE, t5, role25, t3, role10>
/* 70 */ <TRUE, t3, role3, t4, role10>
/* 71 */ <TRUE, t1, role3, t3, role10>
/* 72 */ <TRUE, t3, role32, t4, role10>
/* 73 */ <TRUE, t5, role32, t3, role10>
/* 74 */ <TRUE, t4, role9, t5, role10>
/* 75 */ <TRUE, t3, role9, t1, role10>
/* 76 */ <TRUE, t5, role9, t3, role10>
/* 77 */ <TRUE, t3, role12, t5, role10>
/* 78 */ <TRUE, t5, role12, t4, role10>
/* 79 */ <TRUE, t4, role30, t4, role10>
/* 80 */ <TRUE, t1, role30, t2, role10>
/* 81 */ <TRUE, t2, role30, t3, role10>
/* 82 */ <TRUE, t5, role16, t3, role10>
/* 83 */ <TRUE, t5, role23, t5, role11>
/* 84 */ <TRUE, t3, role9, t5, role12>
/* 85 */ <TRUE, t4, role9, t1, role12>
/* 86 */ <TRUE, t5, role9, t3, role12>
/* 87 */ <TRUE, t1, role1 & NOT ~ role7 & NOT ~ role7 & NOT ~ role8, t5, role12>
/* 88 */ <TRUE, t5, role1 & NOT ~ role7 & NOT ~ role7 & NOT ~ role8, t3, role12>
/* 89 */ <TRUE, t5, role8, t2, role12>
/* 90 */ <TRUE, t2, role8, t3, role12>
/* 91 */ <TRUE, t1, role8, t5, role12>
/* 92 */ <TRUE, t3, role21, t1, role12>
/* 93 */ <TRUE, t4, role21, t4, role12>
/* 94 */ <TRUE, t5, role21, t2, role12>
/* 95 */ <TRUE, t4, role14, t5, role12>
/* 96 */ <TRUE, t1, role14, t1, role12>
/* 97 */ <TRUE, t2, role14, t2, role12>
/* 98 */ <TRUE, t4, role16, t5, role12>
/* 99 */ <TRUE, t5, role16, t2, role12>
/* 100 */ <TRUE, t2, role16, t3, role12>
/* 101 */ <TRUE, t1, role11, t4, role13>
/* 102 */ <TRUE, t2, role11, t5, role13>
/* 103 */ <TRUE, t5, role11, t1, role13>
/* 104 */ <TRUE, t3, role9, t1, role13>
/* 105 */ <TRUE, t5, role9, t4, role13>
/* 106 */ <TRUE, t1, role5, t5, role13>
/* 107 */ <TRUE, t4, role5, t2, role13>
/* 108 */ <TRUE, t5, role5, t1, role13>
/* 109 */ <TRUE, t1, role2, t3, role13>
/* 110 */ <TRUE, t4, role2, t4, role13>
/* 111 */ <TRUE, t2, role2, t5, role13>
/* 112 */ <TRUE, t5, role23 & NOT ~ role5 & NOT ~ role5 & NOT ~ role6, t4, role13>
/* 113 */ <TRUE, t1, role23 & NOT ~ role5 & NOT ~ role5 & NOT ~ role6, t2, role13>
/* 114 */ <TRUE, t3, role31, t4, role13>
/* 115 */ <TRUE, t4, role31, t2, role13>
/* 116 */ <TRUE, t2, role10, t4, role13>
/* 117 */ <TRUE, t3, role10, t1, role13>
/* 118 */ <TRUE, t1, role10, t2, role13>
/* 119 */ <TRUE, t1, role7, t2, role13>
/* 120 */ <TRUE, t5, role7, t4, role13>
/* 121 */ <TRUE, t4, role22 & NOT ~ role5 & NOT ~ role5 & NOT ~ role8, t5, role13>
/* 122 */ <TRUE, t5, role22 & NOT ~ role5 & NOT ~ role5 & NOT ~ role8, t4, role13>
/* 123 */ <TRUE, t1, role22 & NOT ~ role5 & NOT ~ role5 & NOT ~ role8, t1, role13>
/* 124 */ <TRUE, t1, role8, t3, role13>
/* 125 */ <TRUE, t4, role8, t1, role13>
/* 126 */ <TRUE, t2, role8, t2, role13>
/* 127 */ <TRUE, t5, role2, t5, role14>
/* 128 */ <TRUE, t2, role2, t3, role14>
/* 129 */ <TRUE, t3, role2, t2, role14>
/* 130 */ <TRUE, t4, role8 & NOT ~ role3 & NOT ~ role3 & NOT ~ role3, t3, role14>
/* 131 */ <TRUE, t5, role8 & NOT ~ role3 & NOT ~ role3 & NOT ~ role3, t4, role14>
/* 132 */ <TRUE, t1, role8 & NOT ~ role3 & NOT ~ role3 & NOT ~ role3, t5, role14>
/* 133 */ <TRUE, t3, role5, t4, role14>
/* 134 */ <TRUE, t4, role13 & NOT ~ role4 & NOT ~ role2 & NOT ~ role7, t1, role14>
/* 135 */ <TRUE, t3, role13 & NOT ~ role4 & NOT ~ role2 & NOT ~ role7, t5, role14>
/* 136 */ <TRUE, t5, role21, t1, role14>
/* 137 */ <TRUE, t4, role10, t4, role14>
/* 138 */ <TRUE, t3, role21, t4, role14>
/* 139 */ <TRUE, t2, role21, t5, role14>
/* 140 */ <TRUE, t2, role14, t2, role15>
/* 141 */ <TRUE, t4, role14, t4, role15>
/* 142 */ <TRUE, t4, role25 & NOT ~ role1 & NOT ~ role7 & NOT ~ role7, t4, role15>
/* 143 */ <TRUE, t2, role25 & NOT ~ role1 & NOT ~ role7 & NOT ~ role7, t1, role15>
/* 144 */ <TRUE, t5, role25 & NOT ~ role1 & NOT ~ role7 & NOT ~ role7, t5, role15>
/* 145 */ <TRUE, t4, role1, t3, role15>
/* 146 */ <TRUE, t3, role1, t4, role15>
/* 147 */ <TRUE, t1, role16, t2, role15>
/* 148 */ <TRUE, t4, role16, t4, role15>
/* 149 */ <TRUE, t2, role1, t2, role15>
/* 150 */ <TRUE, t3, role1, t1, role15>
/* 151 */ <TRUE, t5, role1, t3, role15>
/* 152 */ <TRUE, t5, role23, t1, role15>
/* 153 */ <TRUE, t5, role13 & NOT ~ role4 & NOT ~ role2 & NOT ~ role1, t2, role15>
/* 154 */ <TRUE, t4, role13 & NOT ~ role4 & NOT ~ role2 & NOT ~ role1, t3, role15>
/* 155 */ <TRUE, t1, role13 & NOT ~ role4 & NOT ~ role2 & NOT ~ role1, t5, role15>
/* 156 */ <TRUE, t3, role6, t2, role15>
/* 157 */ <TRUE, t1, role14, t1, role16>
/* 158 */ <TRUE, t2, role11 & NOT ~ role4 & NOT ~ role1 & NOT ~ role6, t2, role16>
/* 159 */ <TRUE, t3, role30 & NOT ~ role4 & NOT ~ role3 & NOT ~ role4, t2, role16>
/* 160 */ <TRUE, t4, role14, t5, role16>
/* 161 */ <TRUE, t2, role14, t4, role16>
/* 162 */ <TRUE, t5, role14, t1, role16>
/* 163 */ <TRUE, t5, role23, t5, role16>
/* 164 */ <TRUE, t3, role12, t5, role18>
/* 165 */ <TRUE, t2, role13, t5, role18>
/* 166 */ <TRUE, t2, role27, t2, role18>
/* 167 */ <TRUE, t1, role27, t4, role18>
/* 168 */ <TRUE, t3, role27, t5, role18>
/* 169 */ <TRUE, t1, role3, t4, role18>
/* 170 */ <TRUE, t4, role3, t3, role18>
/* 171 */ <TRUE, t4, role14, t4, role18>
/* 172 */ <TRUE, t5, role2, t1, role18>
/* 173 */ <TRUE, t3, role2, t2, role18>
/* 174 */ <TRUE, t4, role2, t3, role18>
/* 175 */ <TRUE, t4, role29, t1, role18>
/* 176 */ <TRUE, t3, TRUE, t3, role18>
/* 177 */ <TRUE, t5, TRUE, t5, role18>
/* 178 */ <TRUE, t2, role9, t4, role18>
/* 179 */ <TRUE, t5, role5, t2, role21>
/* 180 */ <TRUE, t3, role5, t4, role21>
/* 181 */ <TRUE, t4, role5, t3, role21>
/* 182 */ <TRUE, t3, role7, t3, role21>
/* 183 */ <TRUE, t1, role9 & NOT ~ role2 & NOT ~ role2 & NOT ~ role8, t1, role21>
/* 184 */ <TRUE, t2, role9 & NOT ~ role2 & NOT ~ role2 & NOT ~ role8, t5, role21>
/* 185 */ <TRUE, t3, role27, t3, role21>
/* 186 */ <TRUE, t4, role27, t4, role21>
/* 187 */ <TRUE, t3, role1, t4, role21>
/* 188 */ <TRUE, t4, role1, t5, role21>
/* 189 */ <TRUE, t1, role10, t1, role21>
/* 190 */ <TRUE, t4, role10, t2, role21>
/* 191 */ <TRUE, t5, role12, t5, role21>
/* 192 */ <TRUE, t4, role12, t4, role21>
/* 193 */ <TRUE, t1, role12, t1, role21>
/* 194 */ <TRUE, t3, role12, t2, role21>
/* 195 */ <TRUE, t5, role12, t4, role21>
/* 196 */ <TRUE, t2, role12, t3, role21>
/* 197 */ <TRUE, t4, role13, t1, role21>
/* 198 */ <TRUE, t2, TRUE, t4, role22>
/* 199 */ <TRUE, t3, TRUE, t5, role22>
/* 200 */ <TRUE, t3, role20, t3, role23>
/* 201 */ <TRUE, t5, role20, t3, role23>
/* 202 */ <TRUE, t5, role20 & NOT ~ role1 & NOT ~ role5 & NOT ~ role5, t3, role23>
/* 203 */ <TRUE, t2, role20 & NOT ~ role1 & NOT ~ role4 & NOT ~ role1, t1, role23>
/* 204 */ <TRUE, t3, role20 & NOT ~ role1 & NOT ~ role4 & NOT ~ role1, t4, role23>
/* 205 */ <TRUE, t4, role20 & NOT ~ role1 & NOT ~ role4 & NOT ~ role1, t2, role23>
/* 206 */ <TRUE, t1, role20 & NOT ~ role7 & NOT ~ role6 & NOT ~ role6, t5, role23>
/* 207 */ <TRUE, t3, role20 & NOT ~ role7 & NOT ~ role6 & NOT ~ role6, t2, role23>
/* 208 */ <TRUE, t3, role20, t4, role23>
/* 209 */ <TRUE, t4, role20, t3, role23>
/* 210 */ <TRUE, t1, role20, t5, role23>
/* 211 */ <TRUE, t4, role20, t3, role23>
/* 212 */ <TRUE, t1, role20, t1, role23>
/* 213 */ <TRUE, t2, role20, t2, role23>
/* 214 */ <TRUE, t2, role22, t4, role24>
/* 215 */ <TRUE, t3, role22, t5, role24>
/* 216 */ <TRUE, t4, role22, t1, role24>
/* 217 */ <TRUE, t3, role18 & NOT ~ role5 & NOT ~ role8, t5, role25>
/* 218 */ <TRUE, t4, role18 & NOT ~ role5 & NOT ~ role8, t3, role25>
/* 219 */ <TRUE, t2, role22, t2, role27>
/* 220 */ <TRUE, t5, TRUE, t4, role27>
/* 221 */ <TRUE, t1, TRUE, t2, role27>
/* 222 */ <TRUE, t3, role11, t1, role27>
/* 223 */ <TRUE, t1, role11, t5, role27>
/* 224 */ <TRUE, t2, role11, t4, role27>
/* 225 */ <TRUE, t2, role3 & NOT ~ role5 & NOT ~ role4 & NOT ~ role1, t3, role27>
/* 226 */ <TRUE, t3, role24, t4, role27>
/* 227 */ <TRUE, t1, role30, t4, role27>
/* 228 */ <TRUE, t2, role30, t5, role27>
/* 229 */ <TRUE, t3, role30, t1, role27>
/* 230 */ <TRUE, t4, role7, t4, role27>
/* 231 */ <TRUE, t3, role7, t5, role27>
/* 232 */ <TRUE, t2, role18 & NOT ~ role5 & NOT ~ role2 & NOT ~ role5, t1, role29>
/* 233 */ <TRUE, t4, role18 & NOT ~ role5 & NOT ~ role2 & NOT ~ role5, t2, role29>
/* 234 */ <TRUE, t5, role18 & NOT ~ role5 & NOT ~ role2 & NOT ~ role5, t3, role29>
/* 235 */ <TRUE, t4, role11, t2, role30>
/* 236 */ <TRUE, t1, role29, t1, role31>
/* 237 */ <TRUE, t4, role29, t2, role31>
/* 238 */ <TRUE, t2, role29, t3, role31>
/* 239 */ <TRUE, t1, role6, t1, role31>
/* 240 */ <TRUE, t4, role6, t5, role31>
/* 241 */ <TRUE, t5, role6, t2, role31>
/* 242 */ <TRUE, t2, role13 & NOT ~ role4 & NOT ~ role6 & NOT ~ role6, t3, role31>
/* 243 */ <TRUE, t5, role13 & NOT ~ role4 & NOT ~ role6 & NOT ~ role6, t1, role31>
/* 244 */ <TRUE, t3, role13 & NOT ~ role4 & NOT ~ role6 & NOT ~ role6, t4, role31>