a one-input two-output turbine
(Forall (?Self ?Time) (<=> (Active ?Time Extraction-Turbine ?Self) (And (Extraction-Turbine ?Self) (Active ?Time Turbine ?Self) (Active ?Time 1-2-Port-Thermal-Component ?Self))))