V_254a := MS = TA_RA | MS = TA_only | MS =3 | MS = 4 |           MS = 5 | MS = 6 | MS = 7; V_254b := ASL = 2 | ASL = 3 | ASL = 4 | ASL = 5 |           ASL = 6 | ASL = 7; T_254  := (ASL = 2 & V_254a) | (ASL = 2 & MS = TA_only) |           (V_254b & LG = 2 & V524a); V_257a := LG = 5 | LG = 6 | LG = 7 | LG = none; V_257b := MS = TA_RA | MS = 5 || MS = 6 | MS = 7; V_257c := MS = TA_RA | MS = TA_only | MS = 3 | MS = 4 |           MS = 5 | MS = 6 | MS = 7; V_257d := ASL = 5 | ASL = 6 | ASL = 7; T_257  := (ASL = 5 | V_257a | V_257b) |           (ASL = 5 & MS = TA_only) |           (ASL = 5& LG = 2 & V_257c) |           (V_257d & LG = 5 & V_257b) |           (V_257d & V_257a & MS = 5);