Unsatcore unclear explanation

[Ingmar Dasseville]

No conflict is clear from the explanation

>>> Unsatisfiable subset found, trying to reduce its size (might take some time, can be interrupted with ctrl-c.
The following is an unsatisfiable subset, given that functions can map to at most one element (and exactly one if not partial) and the interpretation of types and symbols in the structure:
    P is false because the definition at line 17 completely defines P and no rules make it true.
    P <- ~q. instantiated from line 17.
    P <- ~q. instantiated from line 17.
    P is false because the definition at line 13 completely defines P and no rules make it true.
    P <- q. instantiated from line 13.
    P <- q. instantiated from line 13.

[Ingmar Dasseville]

• merging the definitions gives a segfault!

[Bart Bogaerts]

Hoezo, no conflict is clear? Ik zie een regel P<-q en een regel P<- ~q.

Ziet er nogal conflicterend uit...

[Bart Bogaerts]

Bovendien vertelt hij ook nog eens dat er twee definitions "completely define P"

Dat lijkt mij toch een behoorlijke uitleg.

[Bart Bogaerts]

Ook de segfault kan ik niet reproduceren