Проблемы с функцией TransitiveClosure в Z3Py

Я пытаюсь смоделировать графическое соединение с Z3. В частности, я разбиваю граф и хочу, чтобы подграфы оставались связанными. Однако TransitiveClosure работает не так, как я ожидал. Я моделирую кромки буквой F

Вот MWE:

s = Solver()
N = DeclareSort('N')
a,b,c = Consts('a b c', N)
F = Function(N,N,BoolSort())
s.add(F(A,B) == True)
s.add(F(B,A) == True)

s.add(F(B,C) == False)
s.add(F(C,B) == False)
s.add(F(A,C) == False)
s.add(F(C,A) == False)

s.add(A != B, B != C, C != A)

FX = TransitiveClosure(F)
s.add(FX(A,C))

Очевидно, это SAT, что для меня не имеет особого смысла. Если я изменю s.add(FX(A,C)) на s.add(Not(FX(A,C))).

Почему это? C не должен быть членом FX. Я как-то выставляю FX(A,C) == True), добавляя в модель? Почему это не противоречит определению FX.

Линии вывода / подключения модели трудно понять, поэтому я не совсем уверен, что происходит.