signature {
propositions { p }
nominals { n,a,b }
relations { r,
            s : { inverseof r, functional } }
}

theory

{
 a:<r><r><r><r><r><r><r><r><r><r><r>n;
 b:<r><r><r><r><r><r><r><r><r><r><r>n;
 a:!b
}