:- ['BASE_LITTERALE'].
:- use_module(library(clpb)).
:- use_module(library(lists)).

% MON EXEMPLE : ( (C + B) * (B =< ((C =< D) * (C + (A =:= ~D))) ) )
% | ?- oubases(bl([A,B,C,D], [(0, 1), (0, 1), (0, 1), (0, 1)]), bl([A,B,C,D],[(0,0),(0,0),(0,0),(0,0)]), _Base_ABC), interpretation(_Base_ABC,_I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 0,
% D = 0 ? ;
% no

% | ?- oubases_it([A,B,C,D], [(0, 1), (0, 1), (0, 1), (0, 1)]), bl([A,B,C,D],[(0,0),(0,0),(0,0),(0,0)]), _Base_ABC), interpretation(_Base_ABC,_I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 0,
% D = 0 ? ;
% no


% | ?- oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D],  [(0, 1), (0, 1), (1, 0), (1, 0)]), _Base_ABnC), interpretation(_Base_ABnC,_I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% no


% | ?- oubases_it(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D],  [(0, 1), (0, 1), (1, 0), (1, 0)]), _Base_ABnC), interpretation(_Base_ABnC,_I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% no

% | ?- oubases(bl([A,B,C,D], [(0,1),(1,0),(0,1),(0,1)]), bl([A,B,C,D],[(0, 1), (1, 0), (0, 1), (1, 0)]), _Base_AnBC), interpretation(_Base_AnBC,_I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% no

% | ?- oubases(bl([A,B,C,D], [(0,1),(1,0),(0,1),(0,1)]), bl([A,B,C,D],[(0, 1), (1, 0), (0, 1), (1, 0)]), _Base_AnBC), interpretation(_Base_AnBC,_I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% no


% | ?- oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]),  bl([A,B,C,D],  [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_AnBnC), interpretation(_Base_AnBnC,_I), sat(_I),labeling([A,B,C,D]).
% no


% | ?- oubases_it(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]),  bl([A,B,C,D],  [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_AnBnC), interpretation(_Base_AnBnC,_I), sat(_I),labeling([A,B,C,D]).
% no

% | ?- oubases(bl([A,B,C,D], [(1,0),(0,1),(0,1),(0,1)]), bl([A,B,C,D],  [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABC), interpretation(_Base_nABC,_I), sat(_I), labeling([A,B,C,D]).
% A = 1,
% B = 0,
% C = 0,
% D = 0 ? ;
% no

% | ?- oubases_it(bl([A,B,C,D], [(1,0),(0,1),(0,1),(0,1)]), bl([A,B,C,D],  [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABC), interpretation(_Base_nABC,_I), sat(_I), labeling([A,B,C,D]).
% A = 1,
% B = 0,
% C = 0,
% D = 0 ? ;
% no

% | ?- oubases(bl([A,B,C,D], [(1,0),(0,1),(1,0),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABnC), interpretation(_Base_nABnC,_I), sat(_I), labeling([A,B,C,D]).
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% no

% | ?- oubases_it(bl([A,B,C,D], [(1,0),(0,1),(1,0),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABnC), interpretation(_Base_nABnC,_I), sat(_I), labeling([A,B,C,D]).
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% no

% | ?- oubases(bl([A,B,C,D], [(1,0),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(1, 0), (1, 0), (0, 1), (1, 0)]), _Base_nAnBC), interpretation(_Base_nAnBC,_I), sat(_I),labeling([A,B,C,D]).
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 1 ? ;
% no


% | ?- oubases_it(bl([A,B,C,D], [(1,0),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(1, 0), (1, 0), (0, 1), (1, 0)]), _Base_nAnBC), interpretation(_Base_nAnBC,_I), sat(_I),labeling([A,B,C,D]).
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 1 ? ;
% no


% | ?- oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nAnBnC), interpretation(_Base_nAnBnC,_I), sat(_I), labeling([A,B,C,D]).
% no

% | ?- oubases_it(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nAnBnC), interpretation(_Base_nAnBnC,_I), sat(_I), labeling([A,B,C,D]).
% no


% A, B
% | ?- oubases(bl([A,B,C,D], [(0, 1), (0, 1), (0, 1), (0, 1)]), bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), _Base_ABC),  oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 1), (0, 1), (1, 0), (1, 0)]), _Base_ABnC), oubases(_Base_ABC, _Base_ABnC, _Base_AB), interpretation(_Base_AB, _I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% no



% A, B
% | ?- oubases_it(bl([A,B,C,D], [(0, 1), (0, 1), (0, 1), (0, 1)]), bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), _Base_ABC),  oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 1), (0, 1), (1, 0), (1, 0)]), _Base_ABnC), oubases(_Base_ABC, _Base_ABnC, _Base_AB), interpretation(_Base_AB, _I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% no


% A,  ~B 
% | ?- oubases(bl([A,B,C,D], [(0,1),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(0, 1), (1, 0), (0, 1), (1, 0)]), _Base_AnBC), oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_AnBnC), oubases(_Base_AnBC, _Base_AnBnC, _Base_AnB), interpretation(_Base_AnB, _I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% no

% A,  ~B 
% | ?- oubases_it(bl([A,B,C,D], [(0,1),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(0, 1), (1, 0), (0, 1), (1, 0)]), _Base_AnBC), oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_AnBnC), oubases(_Base_AnBC, _Base_AnBnC, _Base_AnB), interpretation(_Base_AnB, _I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% no


% ~A, B
% | ?- oubases(bl([A,B,C,D], [(1,0),(0,1),(0,1),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABC), oubases(bl([A,B,C,D], [(1,0),(0,1),(1,0),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABnC), oubases(_Base_nABC, _Base_nABnC, _Base_nAB), interpretation(_Base_nAB, _I), sat(_I), labeling([A,B,C,D]).
% A = 1,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% no

% ~A, B
% | ?- oubases_it(bl([A,B,C,D], [(1,0),(0,1),(0,1),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABC), oubases(bl([A,B,C,D], [(1,0),(0,1),(1,0),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABnC), oubases(_Base_nABC, _Base_nABnC, _Base_nAB), interpretation(_Base_nAB, _I), sat(_I), labeling([A,B,C,D]).
% A = 1,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% no


% ~A, ~B
% | ?- oubases(bl([A,B,C,D], [(1,0),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(1, 0), (1, 0), (0, 1), (1, 0)]), _Base_nAnBC),oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nAnBnC),oubases(_Base_nAnBC,_Base_nAnBnC,_Base_nAnB), interpretation(_Base_nAnB, _I), sat(_I),labeling([A,B,C,D]).
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 1 ? ;
% no

% ~A, ~B
% | ?- oubases_it(bl([A,B,C,D], [(1,0),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(1, 0), (1, 0), (0, 1), (1, 0)]), _Base_nAnBC),oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nAnBnC),oubases(_Base_nAnBC,_Base_nAnBnC,_Base_nAnB), interpretation(_Base_nAnB, _I), sat(_I),labeling([A,B,C,D]).
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 1 ? ;
% no


% A
% | ?- oubases(bl([A,B,C,D], [(0, 1), (0, 1), (0, 1), (0, 1)]), bl([A,B,C,D],[(0,0),(0,0),(0,0),(0,0)]), _Base_ABC),  oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 1), (0, 1), (1, 0), (1, 0)]), _Base_ABnC), oubases(_Base_ABC, _Base_ABnC, _Base_AB), oubases(bl([A,B,C,D], [(0,1),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(0, 1), (1, 0), (0, 1), (1, 0)]), _Base_AnBC), oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_AnBnC), oubases(_Base_AnBC, _Base_AnBnC, _Base_AnB), oubases(_Base_AB, _Base_AnB, _Base_A), interpretation(_Base_A, _I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% no


% A
% | ?- oubases_it(bl([A,B,C,D], [(0, 1), (0, 1), (0, 1), (0, 1)]), bl([A,B,C,D],[(0,0),(0,0),(0,0),(0,0)]), _Base_ABC),  oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 1), (0, 1), (1, 0), (1, 0)]), _Base_ABnC), oubases(_Base_ABC, _Base_ABnC, _Base_AB), oubases(bl([A,B,C,D], [(0,1),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(0, 1), (1, 0), (0, 1), (1, 0)]), _Base_AnBC), oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_AnBnC), oubases(_Base_AnBC, _Base_AnBnC, _Base_AnB), oubases(_Base_AB, _Base_AnB, _Base_A), interpretation(_Base_A, _I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% no

% ~A
% | ?- oubases(bl([A,B,C,D], [(1,0),(0,1),(0,1),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABC), oubases(bl([A,B,C,D], [(1,0),(0,1),(1,0),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABnC), oubases(_Base_nABC, _Base_nABnC, _Base_nAB), oubases(bl([A,B,C,D], [(1,0),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(1, 0), (1, 0), (0, 1), (1, 0)]), _Base_nAnBC),oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nAnBnC),oubases(_Base_nAnBC,_Base_nAnBnC,_Base_nAnB), oubases(_Base_nAB,_Base_nAnB,_Base_nA), interpretation(_Base_nA, _I), sat(_I), labeling([A,B,C,D]).
% A = 1,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 1 ? ;
% no


% ~A
% | ?- oubases_it(bl([A,B,C,D], [(1,0),(0,1),(0,1),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABC), oubases(bl([A,B,C,D], [(1,0),(0,1),(1,0),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABnC), oubases(_Base_nABC, _Base_nABnC, _Base_nAB), oubases(bl([A,B,C,D], [(1,0),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(1, 0), (1, 0), (0, 1), (1, 0)]), _Base_nAnBC),oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nAnBnC),oubases(_Base_nAnBC,_Base_nAnBnC,_Base_nAnB), oubases(_Base_nAB,_Base_nAnB,_Base_nA), interpretation(_Base_nA, _I), sat(_I), labeling([A,B,C,D]).
% A = 1,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 1 ? ;
% no

 
% | ?- oubases(bl([A,B,C,D], [(0, 1), (0, 1), (0, 1), (0, 1)]), bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), _Base_ABC),  oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 1), (0, 1), (1, 0), (1, 0)]), _Base_ABnC), oubases(_Base_ABC, _Base_ABnC, _Base_AB), oubases(bl([A,B,C,D], [(0,1),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(0, 1), (1, 0), (0, 1), (1, 0)]), _Base_AnBC), oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_AnBnC), oubases(_Base_AnBC, _Base_AnBnC, _Base_AnB), oubases(_Base_AB, _Base_AnB, _Base_A),oubases(bl([A,B,C,D], [(1,0),(0,1),(0,1),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABC), oubases(bl([A,B,C,D], [(1,0),(0,1),(1,0),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABnC), oubases(_Base_nABC, _Base_nABnC, _Base_nAB), oubases(bl([A,B,C,D], [(1,0),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(1, 0), (1, 0), (0, 1), (1, 0)]), _Base_nAnBC),oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nAnBnC),oubases( _Base_nAnBC,_Base_nAnBnC,_Base_nAnB), oubases( _Base_nAB,_Base_nAnB,_Base_nA), oubases(_Base_A,_Base_nA, _Base), interpretation(_Base, _I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 1 ? ;
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% no


 
% | ?- oubases_it(bl([A,B,C,D], [(0, 1), (0, 1), (0, 1), (0, 1)]), bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), _Base_ABC),  oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 1), (0, 1), (1, 0), (1, 0)]), _Base_ABnC), oubases(_Base_ABC, _Base_ABnC, _Base_AB), oubases(bl([A,B,C,D], [(0,1),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(0, 1), (1, 0), (0, 1), (1, 0)]), _Base_AnBC), oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_AnBnC), oubases(_Base_AnBC, _Base_AnBnC, _Base_AnB), oubases(_Base_AB, _Base_AnB, _Base_A),oubases(bl([A,B,C,D], [(1,0),(0,1),(0,1),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABC), oubases(bl([A,B,C,D], [(1,0),(0,1),(1,0),(0,1)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nABnC), oubases(_Base_nABC, _Base_nABnC, _Base_nAB), oubases(bl([A,B,C,D], [(1,0),(1,0),(0,1),(0,1)]), bl([A,B,C,D], [(1, 0), (1, 0), (0, 1), (1, 0)]), _Base_nAnBC),oubases(bl([A,B,C,D], [(0,0),(0,0),(0,0),(0,0)]), bl([A,B,C,D], [(0, 0), (0, 0), (0, 0), (0, 0)]), _Base_nAnBnC),oubases( _Base_nAnBC,_Base_nAnBnC,_Base_nAnB), oubases( _Base_nAB,_Base_nAnB,_Base_nA), oubases(_Base_A,_Base_nA, _Base), interpretation(_Base, _I), sat(_I), labeling([A,B,C,D]).
% A = 0,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 0,
% C = 0,
% D = 0 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% A = 1,
% B = 1,
% C = 0,
% D = 1 ? ;
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% no


%%% EXEMPLE HABILITATION AaEcAdEe ~~~((d =< c) =< ~(e =< a))

% A C D E x A C D ~E : valide x valide =E= valide
% | ?- oubases(bl([A,C,D,E], [(1, 0), (1, 0), (1, 0), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(1,0),(0,1)]), _Base_ACD), interpretation(_Base_ACD,_I), sat(_I), labeling([A,C,D,E]).
% A = 1,
% C = 1,
% D = 1,
% E = 0 ? ;
% A = 1,
% C = 1,
% D = 1,
% E = 1 ? ;
% no


% A C ~D E x A C ~D ~E : valide x valide =E= valide
% | ?- oubases(bl([A,C,D,E], [(1, 0), (1, 0), (0, 1), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(0,1),(0,1)]), _Base_ACnD), interpretation(_Base_ACnD,_I), sat(_I), labeling([A,C,D,E]).
% A = 1,
% C = 1,
% D = 0,
% E = 0 ? ;
% A = 1,
% C = 1,
% D = 0,
% E = 1 ? ;
% no

% A ~C D E x A ~C D ~E : non_valide x non_valide =E= non_valide

% A ~C ~D E x A ~C ~D ~E : valide x valide =E= valide
% | ?- oubases(bl([A,C,D,E], [(1, 0), (0, 1), (0, 1), (1, 0)]), bl([A,C,D,E],[(1,0),(0,1),(0,1),(0,1)]), _Base_AnCnD), interpretation(_Base_AnCnD,_I), sat(_I), labeling([A,C,D,E]).
% A = 1,
% C = 0,
% D = 0,
% E = 0 ? ;
% A = 1,
% C = 0,
% D = 0,
% E = 1 ? ;
% no


% ~A C D E x ~A C D ~E : non_valide x valide =E= valide
% | ?- _Base_nACD = bl([A,C,D,E],[(0,1),(1,0),(1,0),(0,1)]).

% ~A C ~D E x ~A C ~D ~E : non_valide x valide =E= valide
% | ?- _Base_nACnD = bl([A,C,D,E],[(0,1),(1,0),(0,1),(0,1)]).

% ~A ~C D E x ~A ~C D ~E : non_valide x non_valide =E= non_valide
% | ?- oubases(bl([A,C,D,E], [(0, 1), (0, 1), (0, 1), (1, 0)]), bl([A,C,D,E],[(0,1),(0,1),(0,1),(0,1)]), _Base_nAnCD), interpretation(_Base_nAnCD,_I), sat(_I), labeling([A,C,D,E])

% ~A ~C ~D E x ~A ~C ~D ~E : non_valide x valide =E= valide
% | ?- _Base_nAnCn = bl([A,C,D,E],[(0,1),(0,1),(0,1),(0,1)]).

% (A C D E x A C D ~E) x (A C ~D E x A C ~D ~E) : valide x valide =A= valide
% | ?- oubases(bl([A,C,D,E], [(1, 0), (1, 0), (1, 0), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(1,0),(0,1)]), _Base_ACD), oubases(bl([A,C,D,E], [(1, 0), (1, 0), (0, 1), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(0,1),(0,1)]), _Base_ACnD), oubases(_Base_ACD, _Base_ACnD, _Base_AC),interpretation(_Base_AC,_I), sat(_I), labeling([A,C,D]).
% A = 1,
% C = 1,
% D = 0 ? ;
% A = 1,
% C = 1,
% D = 1 ? ;
% no

% (A ~C D E x A ~C D ~E) x (A ~C ~D E x A ~C ~D ~E) : non_valide x valide =A= non_valide

% (~A C D E x ~A C D ~E) x (~A C ~D E x ~A C ~D ~E) : valide x valide =A= valide
% | ?- _Base_nACD = bl([A,C,D,E],[(0,1),(1,0),(1,0),(0,1)]), _Base_nACnD = bl([A,C,D,E],[(0,1),(1,0),(0,1),(0,1)]), oubases(_Base_nACD, _Base_nACnD, _Base_nAC), interpretation(_Base_nAC, _I), sat(_I), labeling([A,C,D]).
% A = 0,
% C = 1,
% D = 0,
% E = 0 ? ;
% A = 0,
% C = 1,
% D = 1,
% E = 0 ? ;
% no

% (~A ~C D E x ~A ~C D ~E) x (~A ~C ~D E x ~A ~C ~D ~E) : non_valide x valide =A= non_valide

% ((A C D E x A C D ~E) x (A C ~D E x A C ~D ~E)) x ((A ~C D E x A ~C D ~E) x (A ~C ~D E x A ~C ~D ~E)) : valide x non_valide  =E= valide
% | ?- oubases(bl([A,C,D,E], [(1, 0), (1, 0), (1, 0), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(1,0),(0,1)]), _Base_ACD), oubases(bl([A,C,D,E], [(1, 0), (1, 0), (0, 1), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(0,1),(0,1)]), _Base_ACnD), oubases(_Base_ACD, _Base_ACnD, _Base_AC), _Base_A = _Base_AC,interpretation(_Base_A,_I), sat(_I), labeling([A,C,D,E]).
% A = 1,
% C = 1,
% D = 0,
% E = 0 ? ;
% A = 1,
% C = 1,
% D = 0,
% E = 1 ? ;
% A = 1,
% C = 1,
% D = 1,
% E = 0 ? ;
% A = 1,
% C = 1,
% D = 1,
% E = 1 ? ;
% no
% | ?- oubases(bl([A,C,D,E], [(1, 0), (1, 0), (1, 0), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(1,0),(0,1)]), _Base_ACD), oubases(bl([A,C,D,E], [(1, 0), (1, 0), (0, 1), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(0,1),(0,1)]), _Base_ACnD), oubases(_Base_ACD, _Base_ACnD, _Base_AC), Base_A = _Base_AC.
% Base_A = bl([A,C,D,E],[(1,0),(~A*1+(A*1+0),0),(C*(A*1)+0,C*(A*1)+0),(~D*(C*(A*1))+(D*(C*(A*1))+0),~D*(C*(A*1))+(D*(C*(A*1))+0))]) ? ;
% no

% ((~A C D E x ~A C D ~E) x (~A C ~D E x ~A C ~D ~E)) x ((~A ~C D E x ~A ~C D ~E) x (~A ~C ~D E x ~A ~C ~D ~E)) : valide x non_valide =E= valide
% | ?- _Base_nACD = bl([A,C,D,E],[(0,1),(1,0),(1,0),(0,1)]), _Base_nACnD = bl([A,C,D,E],[(0,1),(1,0),(0,1),(0,1)]), oubases(_Base_nACD, _Base_nACnD, _Base_nAC), _Base_nA = _Base_nAC, interpretation(_Base_nA, _I), sat(_I), labeling([A,C,D,E]).
% A = 0,
% C = 1,
% D = 0,
% E = 0 ? ;
% A = 0,
% C = 1,
% D = 1,
% E = 0 ? ;
% no
% | ?- _Base_nACD = bl([A,C,D,E],[(0,1),(1,0),(1,0),(0,1)]), _Base_nACnD = bl([A,C,D,E],[(0,1),(1,0),(0,1),(0,1)]), oubases(_Base_nACD, _Base_nACnD, _Base_nAC), Base_nA = _Base_nAC.
% Base_nA = bl([A,C,D,E],[(0,1),(~A*1+(A*1+0),0),(C*(~A*1)+0,C*(~A*1)+0),(0,~D*(~C*(~A*1))+(~D*(~C*(A*1))+(~D*(C*(~A*1))+(~D*(C*(A*1))+(D*(~C*(~A*1))+(D*(~C*(A*1))+(D*(C*(~A*1))+(D*(C*(A*1))+0))))))))]) ? ;
% no


% (((A C D E x A C D ~E) x (A C ~D E x A C ~D ~E)) x ((A ~C D E x A ~C D ~E) x (A ~C ~D E x A ~C ~D ~E))) x (((~A C D E x ~A C D ~E) x (~A C ~D E x ~A C ~D ~E)) x ((~A ~C D E x ~A ~C D ~E) x (~A ~C ~D E x ~A ~C ~D ~E))) : valide x valide  =A= valide
% | ?- oubases(bl([A,C,D,E], [(1, 0), (1, 0), (1, 0), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(1,0),(0,1)]), _Base_ACD), oubases(bl([A,C,D,E], [(1, 0), (1, 0), (0, 1), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(0,1),(0,1)]), _Base_ACnD), oubases(_Base_ACD, _Base_ACnD, _Base_AC), _Base_A = _Base_AC, _Base_nACD = bl([A,C,D,E],[(0,1),(1,0),(1,0),(0,1)]), _Base_nACnD = bl([A,C,D,E],[(0,1),(1,0),(0,1),(0,1)]), oubases(_Base_nACD, _Base_nACnD, _Base_nAC), _Base_nA = _Base_nAC, oubases(_Base_A, _Base_nA, Base).
% Base = bl([A,C,D,E],[(1,1),(~A*1+(A*1+0),0),(C*(~A*1)+(C*(A*1)+0),C*(~A*1)+(C*(A*1)+0)),(~D*(C*(A*1))+(D*(C*(A*1))+0),~D*(C*(~A*1))+(~D*(C*(A*1))+(D*(C*(~A*1))+(D*(C*(A*1))+0))))]) ? ;
% no
% | ?- oubases(bl([A,C,D,E], [(1, 0), (1, 0), (1, 0), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(1,0),(0,1)]), _Base_ACD), oubases(bl([A,C,D,E], [(1, 0), (1, 0), (0, 1), (1, 0)]), bl([A,C,D,E],[(1,0),(1,0),(0,1),(0,1)]), _Base_ACnD), oubases(_Base_ACD, _Base_ACnD, _Base_AC), _Base_A = _Base_AC, _Base_nACD = bl([A,C,D,E],[(0,1),(1,0),(1,0),(0,1)]), _Base_nACnD = bl([A,C,D,E],[(0,1),(1,0),(0,1),(0,1)]), oubases(_Base_nACD, _Base_nACnD, _Base_nAC), _Base_nA = _Base_nAC, oubases(_Base_A, _Base_nA, _Base), interpretation(_Base, _I), sat(_I), labeling([A,C,D,E]).
% A = 0,
% C = 1,
% D = 0,
% E = 0 ? ;
% A = 1,
% C = 1,
% D = 0,
% E = 0 ? ;
% A = 1,
% C = 1,
% D = 0,
% E = 1 ? ;
% A = 0,
% C = 1,
% D = 1,
% E = 0 ? ;
% A = 1,
% C = 1,
% D = 1,
% E = 0 ? ;
% A = 1,
% C = 1,
% D = 1,
% E = 1 ? ;
% no