% countermodel formalized in coherent logic, using swipl, ['CL.pl'], test('X').

name('X').

:- dynamic 'S'/1,lt/2,'A0'/2,'B0'/2,'A1'/2,'B1'/2,'G'/2,eq0/3,eq1/3,s/3,d1/3,d0/3,fill1/3,fill2/4,fill2/5,loop/3,edge/4.

% domain elements: a1 for a, a2 for a', etc. (Prolog does not support primes i names)
dom(s0). dom(s1). dom(s2). % states, or "days"
dom(a1). dom(a2). % A0
dom(sa1). dom(sa2). % A1
dom(u1). dom(u2). % A1 from day 1 
dom(b1). dom(b2). % B0
dom(sb1). dom(sb2). dom(z1). dom(z2). % B1
dom(v1). dom(v2). % B1 from day 1
dom(w1). dom(w2). % G
dom(x1). dom(x2). % G from day 1

% defining the frame (states, or "days")
_ axiom domS : (true => 'S'(s0),'S'(s1),'S'(s2)).
_ axiom ltSS : (true => lt(s0,s1),lt(s1,s2),lt(s0,s2)).

% defining the graphs
%A
_ axiom dom_A0 : (true => 'A0'(s0,a1),'A0'(s0,a2)).
_ axiom dom_sA1 : (true => 'A1'(s0,sa1),'A1'(s0,sa2)).  % distinct as long as a1<>a2
_ axiom ext_A1 : (true => 'A1'(s1,u1) ,'A1'(s1,u2)). % distinct & ui<>saj as long as a1<>a2
_ axiom diff_s1_ai : (eq0(s1,a1,a2) => false). % implies <>'s in A0,A1 for s0,s1, not for s2!
_ axiom eq_s2_ai : (true => eq0(s2,a1,a2)).
_ axiom eq_s2_sau : (true => eq1(s2,sa1,u1),eq1(s2,sa2,u2),eq1(s2,u1,u2)).
%B
_ axiom dom_B0 : (true => 'B0'(s0,b1),'B0'(s0,b2)).
_ axiom dom_sB1 : (true => 'B1'(s0,sb1),'B1'(s0,sb2)). % distinct as long as b1<>b2
_ axiom dom_B1 : (true => 'B1'(s0,z1), 'B1'(s0,z2)). % distinct as long as b1<>b2 
_ axiom ext_B1 : (true => 'B1'(s1,v1) ,'B1'(s1,v2)). % distinct & vi<>zj,sbj as long as b1<>b2
_ axiom diff_s1_bi : (eq0(s1,b1,b2) => false). % implies <>'s in B0,B1 for s0,s1, not for s2!
_ axiom eq_s2_bi : (true => eq0(s2,b1,b2)).
_ axiom eq_s2_sb : (true => eq1(s2,sb1,sb2)).
_ axiom eq_s2_vz : (true => eq1(s2,v1,v2),eq1(s2,v2,z2),eq1(s2,z2,z1)).
_ axiom diff_sbz : (eq1(s2,sb1,z1) => false). % hence sbi<>zj, also for s0,s1
%G
_ axiom dom0_G  : (true => 'G'(s0,w1),'G'(s0,w2)).
_ axiom ext1_G  : (true => 'G'(s1,x1),'G'(s1,x2)).
_ axiom eq_s2_wx : (true => eq1(s2,w1,w2),eq1(s2,w2,x2),eq1(s2,x2,x1)).

% auxiliaries
_ axiom dedge(S,E,Ps,Pt) : (d1(S,E,Ps),d0(S,E,Pt) => edge(S,E,Ps,Pt)). % introducing edge
_ axiom edged(S,E,Ps,Pt) : (edge(S,E,Ps,Pt) => d1(S,E,Ps),d0(S,E,Pt)). % eliminating edge
_ axiom loop_s(S,E,P) : (loop(S,E,P) => s(S,P,E),edge(S,E,P,P)).     % degenerate loop

% defining the edges
_ axiom loops_sa : (true => loop(s0,sa1,a1),loop(s0,sa2,a2)).
_ axiom loops_sb : (true => loop(s0,sb1,b1),loop(s0,sb2,b2)).
_ axiom edges_z : (true => edge(s0,z1,b1,b1),edge(s0,z2,b2,b2)).
_ axiom edges_u : (true => edge(s1,u1,a1,a2),edge(s1,u2,a2,a1)).
_ axiom edges_v : (true => edge(s1,v1,b1,b2),edge(s1,v2,b2,b1)).
_ axiom edges_w : (true => edge(s0,w1,a1,b1),edge(s0,w2,a2,b2)).
_ axiom edges_x : (true => edge(s1,x1,a1,b2),edge(s1,x2,a2,b1)).

% monotonicity
_ axiom mon_A0(S1,S2,P) : (lt(S1,S2),'A0'(S1,P) => 'A0'(S2,P)).
_ axiom mon_B0(S1,S2,P) : (lt(S1,S2),'B0'(S1,P) => 'B0'(S2,P)).
_ axiom mon_A1(S1,S2,E) : (lt(S1,S2),'A1'(S1,E) => 'A1'(S2,E)).
_ axiom mon_B1(S1,S2,E) : (lt(S1,S2),'B1'(S1,E) => 'B1'(S2,E)).
_ axiom mon_G(S1,S2,E)  : (lt(S1,S2), 'G'(S1,E) =>  'G'(S2,E)).
_ axiom mon_eq0(S1,S2,P1,P2) : (lt(S1,S2),eq0(S1,P1,P2) => eq0(S2,P1,P2)).
_ axiom mon_eq1(S1,S2,E1,E2) : (lt(S1,S2),eq1(S1,E1,E2) => eq1(S2,E1,E2)).
_ axiom mon_d1(S1,S2,E,P) : (lt(S1,S2),d1(S1,E,P) => d1(S2,E,P)).
_ axiom mon_d0(S1,S2,E,P) : (lt(S1,S2),d0(S1,E,P) => d0(S2,E,P)).
_ axiom mon_s(S1,S2,E,P) : (lt(S1,S2),s(S1,P,E) => s(S2,P,E)).

% functionality
_ axiom func_d1(S,X,Y1,Y2) : (d1(S,X,Y1),d1(S,X,Y2) => eq0(S,Y1,Y2)).
_ axiom func_d0(S,X,Y1,Y2) : (d0(S,X,Y1),d0(S,X,Y2) => eq0(S,Y1,Y2)).
_ axiom func_s(S,X,Y1,Y2) : (s(S,X,Y1) ,s(S,X,Y2)  => eq1(S,Y1,Y2)).

% eq0,eq1 equivalences
_ axiom ref_eq0(S,P) : ('A0'(S,P) => eq0(S,P,P)).
_ axiom ref_eq0(S,P) : ('B0'(S,P) => eq0(S,P,P)).
_ axiom ref_eq1(S,E) : ('A1'(S,E) => eq1(S,E,E)).
_ axiom ref_eq1(S,E) : ('B1'(S,E) => eq1(S,E,E)).
_ axiom ref_eq1(S,E) : ('G'(S,E) => eq1(S,E,E)).
_ axiom sym_eq0(S,X,Y) : (eq0(S,X,Y) => eq0(S,Y,X)).
_ axiom sym_eq1(S,X,Y) : (eq1(S,X,Y) => eq1(S,Y,X)).
_ axiom trans_eq0(S,X,Y,Z) : (eq0(S,X,Y),eq0(S,Y,Z) => eq0(S,X,Z)).
_ axiom trans_eq1(S,X,Y,Z) : (eq1(S,X,Y),eq1(S,Y,Z) => eq1(S,X,Z)).

% eq0,eq1 congruences
_ axiom congr_s(S,P1,P2,E1,E2) : (eq0(S,P1,P2),eq1(S,E1,E2),s(S,P1,E1) => s(S,P2,E2)).
_ axiom congr_d1(S,P1,P2,E1,E2) : (eq1(S,E1,E2),eq0(S,P1,P2),d1(S,E1,P1) => d1(S,E2,P2)).
_ axiom congr_d0(S,P1,P2,E1,E2) : (eq1(S,E1,E2),eq0(S,P1,P2),d0(S,E1,P1) => d0(S,E2,P2)).

/* the axioms for the functions f0,g0,f1,g1 must be commented out for model check,
%   if included they give the desired contradiction

:- dynamic f0/3,g0/3,f1/3,g1/3.

% monotonicity for f0,g0,f1,g1
_ axiom mon_f0(S1,S2,X,Y) : (lt(S1,S2),f0(S1,X,Y) => f0(S2,X,Y)).
_ axiom mon_g0(S1,S2,X,Y) : (lt(S1,S2),g0(S1,X,Y) => g0(S2,X,Y)).
_ axiom mon_f1(S1,S2,X,Y) : (lt(S1,S2),f1(S1,X,Y) => f1(S2,X,Y)).
_ axiom mon_g1(S1,S2,X,Y) : (lt(S1,S2),g1(S1,X,Y) => g1(S2,X,Y)).

% congruences for f0,g0,f1,g1
_ axiom congr_f0(S,X1,X2,Y1,Y2) : (eq0(S,X1,X2),eq0(S,Y1,Y2),f0(S,X1,Y1) => f0(S,X2,Y2)).
_ axiom congr_g0(S,X1,X2,Y1,Y2) : (eq0(S,X1,X2),eq0(S,Y1,Y2),g0(S,X1,Y1) => g0(S,X2,Y2)).
_ axiom congr_f1(S,X1,X2,Y1,Y2) : (eq1(S,X1,X2),eq1(S,Y1,Y2),f1(S,X1,Y1) => f1(S,X2,Y2)).
_ axiom congr_g1(S,X1,X2,Y1,Y2) : (eq1(S,X1,X2),eq1(S,Y1,Y2),g1(S,X1,Y1) => g1(S,X2,Y2)).

% homotopy equivalence f0,g0,f1,g1
_ axiom htp_fg0(X1,Y,X2) : ('A0'(s0,X1),'A0'(s0,X2),'B0'(s0,Y),f0(s0,X1,Y),g0(s0,Y,X2) => eq0(s0,X1,X2)).
_ axiom htp_gf0(X1,Y,X2) : ('B0'(s0,X1),'B0'(s0,X2),'A0'(s0,Y),g0(s0,X1,Y),f0(s0,Y,X2) => eq0(s0,X1,X2)).
_ axiom nat_f1(S,X1,X2,Y1,Y2,E,F) :(edge(S,E,X1,X2),f0(S,X1,Y1),f0(S,X2,Y2),f1(S,E,F) => edge(S,F,Y1,Y2)).
_ axiom nat_f1_s(S,X,Y,E,F) :(f0(S,X,Y),s(S,X,E),s(S,Y,F) => f1(S,E,F)).
_ axiom nat_g1(S,X1,X2,Y1,Y2,E,F) :(edge(S,E,X1,X2),g0(S,X1,Y1),g0(S,X2,Y2),g1(S,E,F) => edge(S,F,Y1,Y2)).
_ axiom nat_g1_s(S,X,Y,E,F) :(g0(S,X,Y),s(S,X,E),s(S,Y,F) => g1(S,E,F)).

% functionality of f0,g0,f1,g1
_ axiom func_f0(S,X,Y1,Y2) : (f0(S,X,Y1),f0(S,X,Y2) => eq0(S,Y1,Y2)).
_ axiom func_g0(S,X,Y1,Y2) : (g0(S,X,Y1),g0(S,X,Y2) => eq0(S,Y1,Y2)).
_ axiom func_f1(S,X,Y1,Y2) : (f1(S,X,Y1),f1(S,X,Y2) => eq1(S,Y1,Y2)).
_ axiom func_g1(S,X,Y1,Y2) : (g1(S,X,Y1),g1(S,X,Y2) => eq1(S,Y1,Y2)).

% disjunctions for the totality of f0,g0,f1,g1, put last to make depth-first search efficient
_ axiom total_f0(S,X) : ('A0'(S,X) => f0(S,X,b1) ; f0(S,X,b2)).
_ axiom total_g0(S,X) : ('B0'(S,X) => g0(S,X,a1) ; g0(S,X,a2)).
_ axiom total_f1_s0(X) : ('A1'(s0,X) => f1(s0,X,sb1) ; f1(s0,X,sb2) ; f1(s0,X,z1) ; f1(s0,X,z2)).
_ axiom total_f1_s1(X) : ('A1'(s1,X) => f1(s1,X,sb1) ; f1(s1,X,sb2) ; f1(s1,X,z1) ; f1(s1,X,z2) ; f1(s1,X,v1) ; f1(s1,X,v2)).
_ axiom total_f1_s2(X) : ('A1'(s2,X) => f1(s2,X,sb1) ; f1(s2,X,sb2) ; f1(s2,X,z1) ; f1(s2,X,z2) ; f1(s2,X,v1) ; f1(s2,X,v2)).
_ axiom total_g1_s0(X) : ('B1'(s0,X) => g1(s0,X,sa1) ; g1(s0,X,sa2)).
_ axiom total_g1_s1(X) : ('B1'(s1,X) => g1(s1,X,sa1) ; g1(s1,X,sa2) ; g1(s1,X,u1) ; g1(s1,X,u2)).
_ axiom total_g1_s2(X) : ('B1'(s2,X) => g1(s2,X,sa1) ; g1(s2,X,sa2) ; g1(s2,X,u1) ; g1(s2,X,u2)).

 */ % end axioms for the functions f0,g0,f1,g1

_ axiom fill1 : (true => 
fill1(s0,a1,w1),
fill1(s0,a2,w2),
fill1(s0,b1,w1),
fill1(s0,b2,w2)
).

_ axiom fill2 : (true =>
%A 
fill2(s0,sa1,sa1,sa1),
fill2(s0,sa2,sa2,sa2),
fill2(s1,sa1, u1, u1),
fill2(s1, u1,sa1, u2),
fill2(s1, u1, u1,sa2),
fill2(s1, u2,sa2, u1),
fill2(s1, u2, u2,sa1),
fill2(s1,sa2, u2, u2),
%B
fill2(s0,sb1,sb1,sb1),
fill2(s0, z1, z1, z1), 
fill2(s0,sb1, z1, z1), % must be z1, sb1 is wrong
fill2(s0, z1,sb1, z1), % must be z1, sb1 is wrong

fill2(s0, z2, z2, z2),
fill2(s0,sb2,sb2,sb2),
fill2(s0,sb2, z2, z2),
fill2(s0, z2,sb2, z2),

fill2(s1,sb1, v1, v1),
fill2(s1, v1,sb1, v2),
fill2(s1, v2,sb2, v1),
fill2(s1,sb2, v2, v2),

fill2(s1, z1, v1, v1),
fill2(s1, v1, z1, v2),
fill2(s1, v2, z2, v1),
fill2(s1, z2, v2, v2),

fill2(s1, v1, v1, z2),
fill2(s1, v2, v2, z1),

%G
fill2(s0,a1,sa1,w1, w1),
fill2(s0,a1, w1,w1, z1), % must be z1, sb1 is wrong
fill2(s0,w1,sb1,b1, w1),
fill2(s0,w1, w1,b1,sa1),
fill2(s0,w1, z1,b1, w1),

fill2(s0,a2,sa2,w2, w2),
fill2(s0,a2, w2,w2, z2),
fill2(s0,w2,sb2,b2, w2),
fill2(s0,w2, w2,b2,sa2),
fill2(s0,w2, z2,b2, w2),

fill2(s1,a1,sa1,x1, x1),
fill2(s1,a1, x1,x1, z2),
fill2(s1,x1,sb2,b2, x1),
fill2(s1,x1, x1,b2,sa1),
fill2(s1,x1, z2,b2, x1),

fill2(s1,a2,sa2,x2, x2),
fill2(s1,a2, x2,x2, z1),
fill2(s1,x2,sb1,b1, x2),
fill2(s1,x2, x2,b1,sa2),
fill2(s1,x2, z1,b1, x2),

fill2(s1,a1, w1,x1, v1),
fill2(s1,a1, x1,w1, v2),
fill2(s1,a2, w2,x2, v2),
fill2(s1,a2, x2,w2, v1),

fill2(s1,w1, x2,b1, u1),
fill2(s1,x2, w1,b1, u2),
fill2(s1,w2, x1,b2, u2),
fill2(s1,x1, w2,b2, u1),

fill2(s1,a1, u1,w1, x2),
fill2(s1,a1, u1,x1, w2),
fill2(s1,a2, u2,w2, x1),
fill2(s1,a2, u2,x2, w1),

fill2(s1,w1, v2,b1, x1),
fill2(s1,x2, v2,b1, w2),
fill2(s1,w2, v1,b2, x2),
fill2(s1,x1, v1,b2, w1)

).

% monotonicity for fill1,fill2
_ axiom mon_fill1(S1,S2,P,E) : (lt(S1,S2),fill1(S1,P,E) => fill1(S2,P,E)).
_ axiom mon_fill2AB(S1,S2,E1,E2,E3) : (lt(S1,S2),fill2(S1,E1,E2,E3) => fill2(S2,E1,E2,E3)).
_ axiom mon_fill2PE(S1,S2,P,E1,E2,E3) : (lt(S1,S2),fill2(S1,P,E1,E2,E3) => fill2(S2,P,E1,E2,E3)).
_ axiom mon_fill2EP(S1,S2,E1,E2,P,E3) : (lt(S1,S2),fill2(S1,E1,E2,P,E3) => fill2(S2,E1,E2,P,E3)).

% functionality of fill1,fill2
_ axiom func_fill1(S,P,E1,E2) : (fill1(S,P,E1),fill1(S,P,E2) => eq1(S,E1,E2)).
_ axiom func_fill2(S,E,F,G1,G2) : (fill2(S,E,F,G1),fill2(S,E,F,G2) => eq1(S,G1,G2)).
_ axiom func_fill2(S,P,E,F,G1,G2) : (fill2(S,P,E,F,G1),fill2(S,P,E,F,G2) => eq1(S,G1,G2)).
_ axiom func_fill2(S,E,F,P,G1,G2) : (fill2(S,E,F,P,G1),fill2(S,E,F,P,G2) => eq1(S,G1,G2)).

% eq0,eq1 congruences wrt fill1,fill2
_ axiom congr_fill1(S,P1,P2,E1,E2) : (eq0(S,P1,P2),eq1(S,E1,E2),fill1(S,P1,E1) => fill1(S,P2,E2)).
% we avoid conjunctive query matching (NP) for the large fill2 table by replacing the next axiom by congr1,2,3_fill2AB, etc.
% axiom congr_fill2AB(S,E1,E2,F1,F2,G1,G2) : (eq1(S,E1,E2),eq1(S,F1,F2),eq1(S,G1,G2),fill2(S,E1,F1,G1) => fill2(S,E2,F2,G2)).
_ axiom congr1_fill2AB(S,E1,E2,F,G) : (eq1(S,E1,E2),fill2(S,E1,F,G) => fill2(S,E2,F,G)).
_ axiom congr2_fill2AB(S,E,F1,F2,G) : (eq1(S,F1,F2),fill2(S,E,F1,G) => fill2(S,E,F2,G)).
_ axiom congr3_fill2AB(S,E,F,G1,G2) : (eq1(S,G1,G2),fill2(S,E,F,G1) => fill2(S,E,F,G2)).
_ axiom congr1_fill2PE(S,P1,P2,E,F,G) : (eq0(S,P1,P2),fill2(S,P1,E,F,G) => fill2(S,P2,E,F,G)).
_ axiom congr2_fill2PE(S,P,E1,E2,F,G) : (eq1(S,E1,E2),fill2(S,P,E1,F,G) => fill2(S,P,E2,F,G)).
_ axiom congr3_fill2PE(S,P,E,F1,F2,G) : (eq1(S,F1,F2),fill2(S,P,E,F1,G) => fill2(S,P,E,F2,G)).
_ axiom congr4_fill2PE(S,P,E,F,G1,G2) : (eq1(S,G1,G2),fill2(S,P,E,F,G1) => fill2(S,P,E,F,G2)).
_ axiom congr1_fill2EP(S,P1,P2,E,F,G) : (eq0(S,P1,P2),fill2(S,E,F,P1,G) => fill2(S,E,F,P2,G)).
_ axiom congr2_fill2EP(S,P,E1,E2,F,G) : (eq1(S,E1,E2),fill2(S,E1,F,P,G) => fill2(S,E2,F,P,G)).
_ axiom congr3_fill2EP(S,P,E,F1,F2,G) : (eq1(S,F1,F2),fill2(S,E,F1,P,G) => fill2(S,E,F2,P,G)).
_ axiom congr4_fill2EP(S,P,E,F,G1,G2) : (eq1(S,G1,G2),fill2(S,E,F,P,G1) => fill2(S,E,F,P,G2)).

% Kan properties
_ axiom kanAAA(S,P1,P2,P3,E1,E2) : (/* P1-E1->P2,P1-E2->P3 => P2-E3->P3 in A */
'A0'(S,P1),'A0'(S,P2),'A0'(S,P3),'A1'(S,E1),'A1'(S,E2),edge(S,E1,P1,P2),edge(S,E2,P1,P3) => 
dom(E3),fill2(S,E1,E2,E3),edge(S,E3,P2,P3);write('KANPANIC1 '),write([S,P1,P2,P3,E1,E2]),nl
).

_ axiom kanBBB(S,P1,P2,P3,E1,E2) : (/* P1-E1->P2,P1-E2->P3 => P2-E3->P3 in B */
'B0'(S,P1),'B0'(S,P2),'B0'(S,P3),'B1'(S,E1),'B1'(S,E2),edge(S,E1,P1,P2),edge(S,E2,P1,P3) => 
dom(E3),fill2(S,E1,E2,E3),edge(S,E3,P2,P3);write('KANPANIC2 '),write([S,P1,P2,P3,E1,E2]),nl
).

_ axiom kanGGB(S,P1,P2,P3,E1,E2) : (/* P1-E1->P2,P1-E2->P3 in G => P2-E3->P3 in B */
'A0'(S,P1),'B0'(S,P2),'B0'(S,P3),'G'(S,E1),'G'(S,E2),edge(S,E1,P1,P2),edge(S,E2,P1,P3) => 
dom(E3),fill2(S,P1,E1,E2,E3),edge(S,E3,P2,P3);write('KANPANIC3 '),write([S,P1,P2,P3,E1,E2]),nl
).

_ axiom kanAGG(S,P1,P2,P3,E1,E2) : (/* P1-E1->P2 in A, P1-E2->P3 in G => P2-E3->P3 in G */
'A0'(S,P1),'A0'(S,P2),'B0'(S,P3),'A1'(S,E1),'G'(S,E2),edge(S,E1,P1,P2),edge(S,E2,P1,P3) => 
dom(E3),fill2(S,P1,E1,E2,E3),edge(S,E3,P2,P3);write('KANPANIC4 '),write([S,P1,P2,P3,E1,E2]),nl                          
).

_ axiom kanGGA(S,P1,P2,P3,E1,E2) : (/* P1-E1->P3,P2-E2->P3 in G => P1-E3->P2 in A */
'A0'(S,P1),'A0'(S,P2),'B0'(S,P3),'G'(S,E1),'G'(S,E2),edge(S,E1,P1,P3),edge(S,E2,P2,P3) => 
dom(E3),fill2(S,E1,E2,P3,E3),edge(S,E3,P1,P2);write('KANPANIC5 '),write([S,P1,P2,P3,E1,E2]),nl                          
).

_ axiom kanGBG(S,P1,P2,P3,E1,E2) : (/* P1-E1->P2 in G,P3-E2->P2 in B => P1-E3->P3 in G */
'A0'(S,P1),'B0'(S,P2),'B0'(S,P3),'G'(S,E1),'B1'(S,E2),edge(S,E1,P1,P2),edge(S,E2,P3,P2) => 
dom(E3),fill2(S,E1,E2,P2,E3),edge(S,E3,P1,P3);write('KANPANIC6 '),write([S,P1,P2,P3,E1,E2]),nl
).

% report the model
_ axiom report: (true => model).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% operational stuff %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

eq0_class(S,P,L) :- setof(X,eq0(S,P,X),L).
quot0_eq0(S,LL) :- setof(L,P^(eq0(S,P,P),eq0_class(S,P,L)),LL).
eq1_class(S,E,L) :- setof(X,eq1(S,E,X),L).
quot1_eq1(S,LL) :- setof(L,E^(eq1(S,E,E),eq1_class(S,E,L)),LL).

edges(S) :- quot1_eq1(S,LL),
            forall(member([E|T],LL),
                   (d1(S,E,Ps),d0(S,E,Pt),
                    eq0_class(S,Ps,Ls),eq0_class(S,Pt,Lt),
                    nl,write([E|T]),write(' : '),write(Ls),write('->'),write(Lt))
                  ).

fill1(S,L) :- setof(fill1(PL,EL),P^E^(fill1(S,P,E),eq0_class(S,P,PL),eq1_class(S,E,EL)),L).

fill1(S) :- fill1(S,LL),forall(member(L,LL),(nl,write(L))).

fill2(S,L) :- setof(fill2(EL1,EL2,EL3),
              E1^E2^E3^(fill2(S,E1,E2,E3),eq1_class(S,E1,EL1),eq1_class(S,E2,EL2),eq1_class(S,E3,EL3)),L).
fill2(S,L) :- setof(fill2(PL,EL1,EL2,EL3),
              P^E1^E2^E3^(fill2(S,P,E1,E2,E3),eq0_class(S,P,PL),eq1_class(S,E1,EL1),eq1_class(S,E2,EL2),eq1_class(S,E3,EL3)),L).
fill2(S,L) :- setof(fill2(EL1,EL2,PL,EL3),
              P^E1^E2^E3^(fill2(S,E1,E2,P,E3),eq0_class(S,P,PL),eq1_class(S,E1,EL1),eq1_class(S,E2,EL2),eq1_class(S,E3,EL3)),L).

fill2(S) :- forall(fill2(S,LL),forall(member(L,LL),(nl,write(L)))).

model :- forall('S'(S),
                (write(S),edges(S),fill1(S),fill2(S),nl)
               ).



