HTab-1.5.4: examples/unsat/fun_inj2.frm

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
}