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