ainda estamos trabalhando com FOL, logo os axioms de SUMO não são formalizados diretamente, mas sua tradução para FOL é formalizada.