# Station interlocking: dispatcher command permissions, rules 1, 2, 3, 4, 5
# Generated by codegen.py from the rule clauses Foras proved (Foras 0.4.0).
# Equivalence (checked when generated): the compiled C agrees with the clauses on all 768 states x 4 commands,
# and the brute-force search with this code as the guards reaches the same states and verdict.
# Do not edit: regenerate from the clauses.

CLEAR_S1      = orange ≠ S_MAIN ∧ s2 = RED ∧ s3 = RED ∧ orange ≠ S_EAST ∧ silver ≠ S_EAST
CLEAR_S2      = blue ≠ S_EAST ∧ silver ≠ S_EAST ∧ s1 = RED ∧ s3 = RED ∧ (blue = A_W ∨ blue = OUT_B) ∧ points = NRM
CLEAR_S3      = blue ≠ S_EAST ∧ orange ≠ S_EAST ∧ s1 = RED ∧ s2 = RED ∧ (blue = A_W ∨ blue = OUT_B)
THROW_POINTS  = s1 = RED ∧ s2 = RED ∧ s3 = RED ∧ (blue = A_W ∨ blue = OUT_B) ∧ orange ≠ S_EAST ∧ silver ≠ S_EAST