let simplify ((_, p) as s) atm =
  let id atm = (atm, Jst.dep0) in
  match Atom.atom_of atm with
    | (Atom.TT | Atom.FF) -> 
        id atm
    | Atom.Equal(a, b) -> 
        let (a', rho') = can s a 
        and (b', tau') = can s b in
          if Term.eq a' b' then
            (Atom.mk_true, Jst.dep2 rho' tau')
          else              (* only check for explicit disequalities. *)
            (match Partition.is_diseq p a' b' with 
               | Some(sigma') -> 
                   (Atom.mk_false, Jst.dep3 rho' tau' sigma')
               | None -> 
                   if a == a' && b == b' then
                     id atm
                   else 
                     (Atom.mk_equal (a', b'), Jst.dep2 rho' tau'))   
    | Atom.Diseq(a, b) ->
        let (a', rho') = can s a 
        and (b', tau') = can s b in
          if Term.eq a' b' then
            (Atom.mk_false, Jst.dep2 rho' tau')
          else              (* only check for explicit disequalities. *)
            (match Partition.is_diseq p a' b' with
               | Some(sigma') -> 
                   (Atom.mk_true, Jst.dep3 rho' tau' sigma')
               | None -> 
                   if a == a' && b == b' then
                     id atm
                   else 
                     (Atom.mk_diseq (a', b'), Jst.dep2 rho' tau'))
    | Atom.Nonneg(a) -> 
        let (a', rho') = can s a in
          (match is_nonneg s a' with
            | Jst.Three.Yes(tau') -> 
                (Atom.mk_true, Jst.dep2 rho' tau')
            | Jst.Three.No(tau') ->
                (Atom.mk_false, Jst.dep2 rho' tau')
            | Jst.Three.X ->
                if a == a' then id atm else 
                  (Atom.mk_nonneg a', rho'))
    | Atom.Pos(a) -> 
        let (a', rho') = can s a in
          (match is_pos s a' with
             | Jst.Three.Yes(tau') -> 
                 (Atom.mk_true, Jst.dep2 rho' tau')
             | Jst.Three.No(tau') -> 
                 (Atom.mk_false, Jst.dep2 rho' tau')
             | Jst.Three.X ->
                 if a == a' then id atm else 
                   (Atom.mk_pos a', rho'))