signature { propositions { p } nominals { n,m } relations { s : {symmetric} } } theory { n:m; n:p; m:[s][s][s]!p }