sig
  val main :
    Numeral.t option ->
    bool ->
    bool ->
    bool ->
    'InputSystem.t ->
    Analysis.param ->
    TransSys.t -> (TransSys.t * Term.TermSet.t * Term.TermSet.t) list
  val exit : '-> unit
end