To generate auxiliary assertions on small model (N_0=6):
(1) Load the protocol of DINE(6) using tlv
    tlv sys6.smv
(2) Inside of tlv, load the script 
    Load "gen.pf";

To check premises on MEDIUM model (N_0=128)
(1) Load the protocol of DINE(128) using tlv
    tlv -i sys128.ord sys128.smv
(2) Inside of tlv, load the script
    Load "chk.pf";