"The flight crew did not assimilate the readings on the engine instruments before they decided to throttle back the No. 2 engine. after throttling back the No. 2 engine, they did not assimilate the maximum vibration indication apparent on the No. 1 engine before they shut down the number 2 engine 2 minutes 7 seconds after the onset of vibration, and 5nm south of EMA (East Midlands Airport).'' (Finding 7, page 142)

forall t: not(observe(first_officer, pei(engine_1), t)^
observe(first_officer, pei(engine_2), t))^
before(t, 20_05_24) (3)

forall t: not(observe(commander, pei(engine_1), t)^
observe(commander, pei(engine_2), t))^
before(t, 20_05_24) (4)

• More complex example.