let dep5 j1 j2 j3 j4 j5 = 
  match !proofmode with
    | No -> Atom.Set.empty
    | Dep -> Atom.Set.union j1 (Atom.Set.union j2 (Atom.Set.union j3 (Atom.Set.union j4 j5)))