Error in rewriting of nested biconditionals during parsing

[thahmann]

something is off, it seems like the outer universal quantifier is lost and then during PCNF creation, an existential is introduced (note that the original file contained a biconditional, though this is now changed to a conditional only):

C:\Users\torsten\GitHub\colore\ontologies\multidim_mereotopology_codi\definitions\areal_region.clif Axiom: \forall x\;[((~ArealRegion(x) | \forall y\;[((~Curve(y) | Covers(x,y)) & (~Covers(x,y) | Curve(y)))]) & (~\forall y\;[((~Curve(y) | Covers(x,y)) & (~Covers(x,y) | Curve(y)))] | ArealRegion(x)))] from C:\Users\torsten\GitHub\colore\ontologies\multidim_mereotopology_codi\definitions\areal_region.clif ((((~Covers(z,y) | Curve(y)) & (~Curve(y) | Covers(z,y))) | ~ArealRegion(z)) & ((Covers(z,x) & ~Curve(x)) | (Curve(x) & ~Covers(z,x)) | ArealRegion(z))) FF-PCNF: \forall z,y\;[\exists x\;[((~ArealRegion(z) | ~Covers(z,y) | Curve(y)) & (~ArealRegion(z) | ~Curve(y) | Covers(z,y)) & (Covers(z,x) | ArealRegion(z) | Curve(x)) & (ArealRegion(z)) & (~Curve(x) | ArealRegion(z) | ~Covers(z,x)))]]

• yielded: \forall y,z\;[(~ArealRegion(z) | ~Covers(z,y) | Curve(y))]
  • pattern all_values
• yielded: \forall y,z\;[(~ArealRegion(z) | ~Curve(y) | Covers(z,y))]
• yielded: \forall z\;[\exists x\;[(Covers(z,x) | ArealRegion(z) | Curve(x))]]
• yielded: \forall z\;[(ArealRegion(z))]
  • pattern universe
• yielded: \forall z\;[\exists x\;[(~Curve(x) | ArealRegion(z) | ~Covers(z,x))]]