format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!Y || A || C"
    justification: "Output Y can be energised only through input A or C (series/parallel with a negated contact)."