Доказательство теоремы с доказательством 9 - противоречивый результат

Question

Я использую Prover9 для доказательства теорем первого порядка, с интерфейсом Python nltk.

Я получаю разные результаты для двух эквивалентных формул (без предположений):
Пусть р1:

-exists x0.(-exists x3 x1.(R0(x3,x0) & R0(x1,x1)) & exists x1 x2.(R0(x1,x2) & R0(x1,x0)))

И р2:

-exists x3.(-exists x0 x2.(R0(x2,x2) & R0(x0,x3)) & exists x1 x0.(R0(x1,x0) & R0(x1,x3)))

Используя следующий код Python:

import nltk as nk
read_expr = nk.sem.Expression.fromstring

prove_command1 = nk.Prover9Command(goal=read_expr(p1),timeout=20, prover=nk.Prover9())
prove_command2 = nk.Prover9Command(goal=read_expr(p2),timeout=20, prover=nk.Prover9())
print(prove_command1.prove()) # False
print(prove_command2.prove()) # True

Странно то, что когда я печатаю доказательство для каждого из них, цель в обоих случаях эквивалентна:

-(exists x (-(exists y exists z (R0(y,x) & R0(z,z))) & (exists z exists u (R0(z,u) & R0(z,x))))).

Правильный ответ для p1 и p2 - False, и я не понимаю, как это возможно, что два выражения переведены в одну и ту же цель, но ответ отличается.

любой совет?