packages feed

HTab-1.6.0: examples/unsat/symmetry1.frm

signature {
propositions { p }
nominals { n,m }
relations { s : {symmetric} }
}

theory

{
 n:<s><s><s>m;
 n:p;
 m:[s][s][s]!p

}