let rec atom s a =
    Trace.call "rule" "Can" a Atom.pp;
    let b = match a with
      | Atom.True -> Atom.True
      | Atom.Equal(a, b) -> equal s (a, b)
      | Atom.Diseq(a, b) -> diseq s (a, b)
      | Atom.In(a, d) -> sign s (a, d)
      | Atom.False -> Atom.False
    in
      Trace.exit "rule" "Can" b Atom.pp;
      b
      
  and equal s (a, b) = 
    let x' = can s a and y' = can s b in
      match is_equal s x' y' with
        | Three.Yes ->
            Atom.mk_true
        | Three.No -> 
            Atom.mk_false
        | Three.X -> 
            let (x'', y'') = crossmultiply s (x', y') in
              Atom.mk_equal (x'', y'')
 
  and diseq s (a, b) =
    let x' = can s a and y' = can s b in
      match is_equal s x' y' with
        | Three.Yes -> 
            Atom.mk_false
        | Three.No -> 
            Atom.mk_true
        | Three.X ->
            let (x'', y'') = crossmultiply s (x', y') in
              Atom.mk_diseq (x'', y'')

  and crossmultiply s (a, b) =
    let (a', b') = crossmultiply1 s (a, b) in
      if Term.eq a a' && Term.eq b b' then
        (a, b)
      else 
        let (a'', b'') = crossmultiply s (a', b') in
          (can s a'', can s b'')

  and crossmultiply1 s (a, b) =
    let da = Pp.denumerator a in
    let db = Pp.denumerator b in
    let (_, _, d) = Pp.lcm (da, db) in
      if Pp.is_one d then (a, b) else
        (Sig.mk_mult a d, Sig.mk_mult b d)

  and sign s (a, i) =
    let a' = can s a in
      try
        let j = cnstrnt s a' in
        let k = Sign.inter i j in
          if Sign.eq k j then Atom.mk_true 
          else if k = Sign.F then Atom.mk_false
          else Atom.mk_in (a', k)
      with
          Not_found -> Atom.mk_in (a', i)