Splitting of conjunctions with existentials

[thahmann]

It seems like some axioms are not fully splitted into separate FF-PCNF conjunction, for example:

Axiom: \forall x,y\;[(~((AB(x) | PD(x)) & ~P(x,y)) | \exists z\;[(P(z,x) & ~O(z,y))])] from http://colore.oor.net/dolce_mereology/dolce_mereology.clif FF-PCNF: \forall z,y\;[\exists x\;[((~AB(z) | P(z,y) | P(x,z)) & (~AB(z) | P(z,y) | ~O(x,y)) & (~PD(z) | P(z,y) | P(x,z)) & (~PD(z) | P(z,y) | ~O(x,y)))]]

• yielded: \forall z,y\;[\exists x\;[((~AB(z) | P(z,y) | P(x,z)) & (~AB(z) | P(z,y) | ~O(x,y)) & (~PD(z) | P(z,y) | P(x,z)) & (~PD(z) | P(z,y) | ~O(x,y)))]]

I believe FF-PCNF: \forall z,y\;[\exists x\;[((~AB(z) | P(z,y) | P(x,z)) & (~AB(z) | P(z,y) | ~O(x,y)) & (~PD(z) | P(z,y) | P(x,z)) & (~PD(z) | P(z,y) | ~O(x,y)))]] should be split into four separate PCNF sentences: \forall z,y\;[\exists x\;[(~AB(z) | P(z,y) | P(x,z))]] \forall z,y\;[\exists x\;[(~AB(z) | P(z,y) | ~O(x,y))]] \forall z,y\;[\exists x\;[(~PD(z) | P(z,y) | P(x,z))]] \forall z,y\;[\exists x\;[(~PD(z) | P(z,y) | ~O(x,y))]]

I don't think this splitting would yield additional OWL axioms in this particular example, but it might in other cases (e.g. someValuesFrom statements)).

[thahmann]

Resolved by commit #ca9e5107c9c791cb65446900a34e4e083596b05f