open LTO
-- check if the property holds
  red (ens12(s,i,n) /\ ens13(s,i,n)) => lto14(s,i,n) .
close