let f1 = T::Formula ModalK

let h1 = genPV f1

let aux1=head h1

let ro1 = roFromPV aux1

let xx1 = head ro1

let mr1 = matchRO xx1

let yy1 = head mr1

let cl1 = guessClause yy1

let zz1 = head cl1

let ff1 = negSubst zz1 xx1 f1

let f1 = Mapp (Mop (ModalK ()) Square) T :: Formula ModalK

let h1 = genPV f1

let ro1 = map roFromPV h1

let mr1 = map (map matchRO) ro1

let cl1 = map (map (map guessClause)) mr1

let f1 = F :: Formula ModalK

let h1 = genPV f1

let ro1 = map roFromPV h1

let mr1 = map (map matchRO) ro1

let cl1 = map (map (map guessClause)) mr1