HTab-1.5.4: examples/unsat/fun_inj1.frm

signature {
propositions { p }
nominals { n,m }
relations { r : { functional } }
}

theory

{
 n:<r><r><r><r><r>p;
 m:<r><r><r><r><r>!p;
 n:m
}