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))]]