#FAIL: fails even when weakened to AG(lamp=unlit -> EX(lamp=lit))
# or to AG(lamp=lit -> EX(lamp=unlit))
AG(((lamp = lit)->EX(lamp=unlit))*((lamp=unlit)->EX(lamp=lit)));
#PASS: passes even when strengthened to EF(int.state=go3)
# or to EF(int.state=go4).
EF((int.state=go3)+(int.state=go4));
#PASS: no vacuous passes
EF EG((int.state=go3)+(int.state=go4));
#FAIL: no vacuous failures
!EF EG((int.state=go3)+(int.state=go4));
#FAIL: no vacuous failures
AG AF(!(int.state=go3)*!(int.state=go4));
#FAIL: no vacuous failures
AG((interpretation = go) -> (train = absent));
#PASS: passes even when strengthened to AG !(train = present2)
AG((interpretation = go) -> !(train = present2));