forall t: P(t) -> Q(t), exists t': P(t') |- exists t': Q(t') (7)



forall t':
input(first_officer, throttle_back(engine_2),20_05_24) <- not(observe(first_officer, pei(engine_1), t') v
observe(first_officer, pei(engine_2), t')) ^
before(t', 20_05_24).

[Instantiating 20_05_24 for t in (5) given (1)] (8)




input(first_officer, throttle_back, engine_2, 20_05_24)

[Applying (7) to (8), given (3)] (9)