Using the symbolization key given below, symbolize each English sentence in FOL (First-Order Logic). Here is the key for inputting the logical connectives and quantifiers into Carnap:

type ~ or "not" for negation
type \/ or "or" for disjunction
type /\ or "and" for conjunction
type > or -> for conditional
type <> or <-> for biconditional
type Ax for the universal quantifier
type Ex for the existential quantifier
Here is the symbolization key:

Domain: people
C(x) = x knows the combination to the safe.
S(x) = x is a spy.
V(x) = x is a vegetarian.
h = Hofthor
g = Galadriel

Translate:
Every spy who knows the combination to the safe is a vegetarian if, and only if, either Hofthor is not a spy or Hofthor does not know the combination to the safe.