Here is only query log for that as it is. ‘true’ is for 1.
I need time for understanding other parts of your posts.
I hope you could reproduce the query like this.
?- use_module(library(pac)). % version 1.8.3
?- module(pac).
pac: ?- use_module(zdd(zdd)).
?- time((sat(.....
query result
% ?- time((sat(true#T2*T3#T2*Y1#T3*Y1#Y1), psa,
% sat(T1=:=T1*Y2#T1*Y3#Y2*Y3), psa,
% sat(T1=\=Y1), psa,
% sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3), psa,
% sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3), psa)).
%@ zid = 56
%@ [-B,-C]
%@ [-A,-C]
%@ [-A,-B,-C]
%@ [-A,B,C]
%@ [A,-B,C]
%@ [A,B,C]
%@ -------------------
%@ zid = 126
%@ [-B,-C,-D,-F]
%@ [-B,-C,-D,-E]
%@ [-B,-C,D,-E,F]
%@ [-B,-C,D,E,-F]
%@ [-B,-C,D,E,F]
%@ [-A,-C,-D,-F]
%@ [-A,-C,-D,-E]
%@ [-A,-C,D,-E,F]
%@ [-A,-C,D,E,-F]
%@ [-A,-C,D,E,F]
%@ [-A,-B,-C,-D,-F]
%@ [-A,-B,-C,-D,-E]
%@ [-A,-B,-C,D,-E,F]
%@ [-A,-B,-C,D,E,-F]
%@ [-A,-B,-C,D,E,F]
%@ [-A,B,C,-D,-F]
%@ [-A,B,C,-D,-E]
%@ [-A,B,C,D,-E,F]
%@ [-A,B,C,D,E,-F]
%@ [-A,B,C,D,E,F]
%@ [A,-B,C,-D,-F]
%@ [A,-B,C,-D,-E]
%@ [A,-B,C,D,-E,F]
%@ [A,-B,C,D,E,-F]
%@ [A,-B,C,D,E,F]
%@ [A,B,C,-D,-F]
%@ [A,B,C,-D,-E]
%@ [A,B,C,D,-E,F]
%@ [A,B,C,D,E,-F]
%@ [A,B,C,D,E,F]
%@ -------------------
%@ zid = 174
%@ [-B,-C,D,-E,F]
%@ [-B,-C,D,E,-F]
%@ [-B,-C,D,E,F]
%@ [-A,-C,D,-E,F]
%@ [-A,-C,D,E,-F]
%@ [-A,-C,D,E,F]
%@ [-A,-B,-C,D,-E,F]
%@ [-A,-B,-C,D,E,-F]
%@ [-A,-B,-C,D,E,F]
%@ [-A,B,C,-D,-F]
%@ [-A,B,C,-D,-E]
%@ [A,-B,C,-D,-F]
%@ [A,-B,C,-D,-E]
%@ [A,B,C,-D,-F]
%@ [A,B,C,-D,-E]
%@ -------------------
%@ zid = 336
%@ [-A,-B,-C,D,-E,F]
%@ [-A,-B,-C,D,E,-F]
%@ [-A,-B,-C,D,E,F]
%@ [-A,B,-C,D,-E,F]
%@ [-A,B,-C,D,E,-F]
%@ [-A,B,-C,D,E,F]
%@ [-A,B,C,-D,-F]
%@ [-A,B,C,-D,-E]
%@ [A,-B,-C,D,-E,F]
%@ [A,-B,-C,D,E,-F]
%@ [A,-B,-C,D,E,F]
%@ [A,-B,C,-D,-F]
%@ [A,-B,C,-D,-E]
%@ [A,B,C,-D,-F]
%@ [A,B,C,-D,-E]
%@ -------------------
%@ zid = 424
%@ [-A,-B,-C,D,-E,F]
%@ [-A,-B,-C,D,E,-F]
%@ [-A,-B,-C,D,E,F]
%@ [-A,B,-C,D,-E,F]
%@ [-A,B,-C,D,E,-F]
%@ [-A,B,-C,D,E,F]
%@ [-A,B,C,-D,-E,-F]
%@ [-A,B,C,-D,-E,F]
%@ [-A,B,C,-D,E,-F]
%@ [A,-B,-C,D,-E,F]
%@ [A,-B,-C,D,E,-F]
%@ [A,-B,-C,D,E,F]
%@ [A,-B,C,-D,-E,-F]
%@ [A,-B,C,-D,-E,F]
%@ [A,-B,C,-D,E,-F]
%@ [A,B,C,-D,-E,-F]
%@ [A,B,C,-D,-E,F]
%@ [A,B,C,-D,E,-F]
%@ -------------------
%@ % 63,375 inferences, 0.005 CPU in 0.007 seconds (72% CPU, 12708041 Lips)
%@ T2 = A,
%@ T3 = B,
%@ Y1 = C,
%@ T1 = D,
%@ Y2 = E,
%@ Y3 = F.