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

theory

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

}