let main () =
  let problem_file = ref "" in
  Arg.parse [
   ] (fun x -> problem_file := x) "matitaprover [problemfile]";
  let hypotheses, goal = Tptp_cnf.parse !problem_file in
  let module B : Terms.Blob = struct
        type t = Ast.atom
        let eq a b = a = b
        let compare = Pervasives.compare
        let eqP = Ast.True
        let pp x = ""
        let embed x = Terms.Var 0
        let saturate x y = Terms.Var 0,Terms.Var 0
  end
  in
  let module P = Paramod.Paramod(B) in
  let bag = Terms.M.empty, 0 in
  let g_passives = assert false in
  let passives = assert false in
  ignore(P.paramod bag ~g_passives ~passives);
  ()
;;

main ()