```c
module Offices

  type office = One | Two | Three
  type person = Ana | Nuno | Pedro | Maria

  predicate hasOffice (person) (office)

  axiom A1 : forall p:person. exists o:office. hasOffice p o
  axiom A2 : forall p:person, o1 o2 : office.
    hasOffice p o1 /\ hasOffice p o2 -> o1 = o2
  
  axiom B : forall o1 o2 : office. hasOffice Pedro o1 /\ hasOffice Nuno o2 ->
      o1 <> o2
  
  predicate alone (p:person) = forall o:office. forall p1:person.
    (hasOffice p o) /\ hasOffice p1 o -> p = p1

  axiom C : alone Ana -> alone Pedro
  axiom D : forall p1 p2 p3: person, o:office.
    hasOffice p1 o /\ hasOffice p2 o /\ hasOffice p3 o ->
        p1 = p2 \/ p1 = p3 \/ p3 = p2

  goal sanity_test : false (*check if the model makes sense*)
  
  goal g1 : hasOffice Maria One -> alone Maria
  goal g2 : forall o1:office. (hasOffice Ana o1 /\ hasOffice Nuno o1) -> 
      exists o2:office. hasOffice Pedro o2 /\ hasOffice Maria o2 

  predicate empty (o:office) = forall p:person. not (hasOffice p o)
  
  lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
      o1 = o2

end 
```