             
% Version 1.1-2

%1
% Aggiunto fail_rules f26, f26BIS, f26TER

%2
% Corretto titolo
% eliminato op per ein e enin
% eliminato equiv_rules generali
% eliminato replace_rules generali
% aggiunto parametro in equiv_rules
% correto bug in f17 (non veniva selezionata)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%
% Filtering rules 
% for using {log} for the Test Template Framework (TTF)
% (for {log} version 4.7.0-1 or newer)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%
%           by Maximiliano Cristia' and  Gianfranco Rossi
%                          April 2014 
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%% equivalence rules %%%%%%%%%%%%%%%%%%%%%%%%

% equiv_rule(A,B), with A, B {log} predicates: if the input goal contains B then  
% then B matches with both filtering rule for A and filtering rule for B (since B => A)

equiv_rule(e1,is_rel(R),is_pfun(R)).             % e1. is_pfun(R) => is_rel(R)   
equiv_rule(e7,dom(Rel,Dom),dom_size_rel(Rel,Dom,_NDom)).       % e7.   
equiv_rule(e8,ran(Rel,Ran),ran_subset_ran(Rel,Ran,_S)).                 % e8.   
%TO BE COMPLETED: dis_pfun,  ...


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%% replace rules %%%%%%%%%%%%%%%%%%%%%%%%%%

%replace_rule(W: when,
%               C: atomic constraint
%               C_Conds: list of conditions for C
%               D: list of other atomic constraints to be checked
%               D_Conds: list of conditions for atomic constraints in D and C
%               AddC: constraint to be replaced to C)


% dom(Rel,Dom) & size(Dom,NDom) -replace-> dom_size_rel(Rel,Dom,NDom)   
replace_rule(initial(r1),dom(Rel,Dom),[var(Dom),var(Rel)],[size(Dom1,NDom)],[Dom1==Dom],dom_size_rel(Rel,Dom,NDom)).

% ran(Rel,Ran) & dsubset(Ran,S) -replace-> ran_subset_ran(Rel,Ran,S)
replace_rule(initial(r2),ran(Rel,Ran),[var(Ran),var(Rel)],[dsubset(Ran1,S)],[Ran1==Ran],ran_subset_ran(Rel,Ran,S)).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%% inference rules %%%%%%%%%%%%%%%%%%%%%%%%%

%inference_rule(W: when,
%               C: atomic constraint
%               C_Conds: list of conditions for C
%               D: list of other atomic constraints to be checked
%               D_Conds: list of conditions for atomic constraints in D and C
%               E: list of constraints in D to be NOT checked
%               AddC: constraint to be added)
        

%%%%%%%%%%%% using only set predicates
%%%%%%%%%%%% (they would not be necessary if all set predicates would be dealt with
%%%%%%%%%%%% as constraints or otherwise they would be executed before user-defined predicates)
%%%%%%%%%%%% e.g. dom(R,{1}) & dinters({A},Y,Z) & Z = {} & A in Y 
%%%%%%%%%%%% loops forever if the rule (i1) is not applied; fails if the rule (i1) (along with (bf3))
%%%%%%%%%%%% is applied; rule (i1) not necessary at all if inters is used in place of dinters

% NotMembershipEquivalences
% i1. dinters({A},Y,Z) & Z = {} -add-> A nin Y   
inference_rule(initial,dinters(X,Y,Z),[nonvar(X),X={} with A],[Z1=E],[nonvar(E),E={},Z1==Z],[], A nin Y).        

%%%% N.B. usando dinters nella filtring rule se nel goal si usa inters allora la regola non si applica.
%%%% Se invece uso inters nella filtering rule allora nel goal posso usare sia inters che dinters
%%%% (questo e' dovuto al modo in cui si applicano la equiv_rule che non sono simmetriche).
%%%% Dunque se si e' sicuri che nel goal si usa dinters allora va bene usare dinters anche
%%%% nella regola (cosi' risulta leggermente piu' efficiente); altrimenti e' meglio usare inters
%%%% nella regola:
%%%% inference_rule(initial,inters(X,Y,Z),[nonvar(X),X={} with A],[Z1=E],[nonvar(E),E={},Z1==Z],[], A nin Y).        

% NotMembershipEquivalences
% i2. dnsubset({A},Y) -add-> A nin Y
inference_rule(initial,dnsubset(X,Y),[nonvar(X),X={} with A],[],[],[], A nin Y). 

% MembershipEquivalences
% i5. dinters(X,{A},Y) & Y neq {} -add-> A in X            
% i5bis. dinters({A},Y,Z) & Z neq {} -add-> A in Y
inference_rule(initial,dinters(X,Y,Z),[nonvar(Y),Y={} with A],[Z1 neq E],[nonvar(E),E={},Z1==Z],[], A ein X). 
inference_rule(initial,dinters(X,Y,Z),[nonvar(X),X={} with A],[Z1 neq E],[nonvar(E),E={},Z1==Z],[], A ein Y).
  
% MembershipEquivalences
% i7. dssubset({A},Y) -add-> A in Y
inference_rule(initial,dssubset(S,Y),[nonvar(S),S={} with A],[],[],[], A in Y).     

%%%%%%%%%%%% using TTF predicates over relations

% NotMembershipEquivalences
% i3. dinters(Y,D,Z) & Z = {} & dom({[A,B]},D) -add-> A nin Y
inference_rule(initial,dinters(Y,D,Z),[],[Z1=E,dom(R,D1)],[nonvar(E),E={},nonvar(R),R={} with [A,_B],Z1==Z,D==D1],[], A nin Y).     

% NotMembershipEquivalences
% i4. dnsubset(D,Y) & dom({[A,B]},D) -add-> A nin Y
inference_rule(initial,dnsubset(D,Y),[],[dom(R,D1)],[nonvar(R),R={} with [A,_B],D==D1],[], A nin Y).        

% i6. dom({[A,B]},D) -add-> D = {A}    %%% ATTN a questa regola - fa una sostituzione
%%%%%%%%%%%%inference_rule(initial,dom(S,D),[subsumes({} with [A,_],S),var(D)],[],[],[],D={} with A).                
inference_rule(initial,dom(S,D),[nonvar(S),S={} with [A,_],var(D),D={} with A],[],[],[],D={} with A).   
%
%ATTN. Questa regola non e' del tutto corretta perche' la condizione
%nonvar(S),S={} with [A,_] "cattura" anche i termini del tipo {[A,B]/R}  per i 
%quali non sarebbe corretto fare la riscrittura indicata          

% i8. ran(R,A) & R neq {}  -add-> A neq {}
inference_rule(initial,ran(R,A),[var(R)],[R1 neq E],[nonvar(E),E={},R1==R],[], A neq {}).     

% NotEmptyRelEquivalences
% i9. ran(R,A) & A neq {}  -add-> R neq {}
inference_rule(initial,ran(R,A),[var(A)],[A1 neq E],[nonvar(E),E={},A1==A],[], R neq {}).        


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%% fail rules %%%%%%%%%%%%%%%%%%%%%%%%%%%%

%     fail_rule(W: when,
%               C: atomic constraint
%               C_Conds: list of conditions for C
%               D: list of other atomic constraints to be checked
%               D_Conds: list of conditions for atomic constraints in D and C
%               E: list of constraints in D to be NOT checked)


%%%%%%%%%%%% using only set predicates (all terminating)
%%%%%%%%%%%% (they would not be necessary if all set predicates would be dealt with
%%%%%%%%%%%% as constraints or otherwise they would be executed before user-defined predicates)

% f1. dinters(X,Y,Z) & X = {} & Z neq {}   
fail_rule(initial,dinters(X,_,Z),[var(X),var(Z)],[X1=E,Z1 neq EE],[nonvar(E),E={},nonvar(EE),EE={},X1==X,Z1==Z],[]).
% normalized:
% f1. dinters({},Y,Z) & Z neq {}
% fail_rule(initial,dinters(X,_,Z),[nonvar(X),X={},var(Z)],[Z1 neq EE],[nonvar(EE),EE={},Z1==Z],[]).

% f18. dsubset(A,X) & X = {X1,X2} & dssubset({X1},A) & dinters({X2},A,T) & T = {}
fail_rule(initial,dssubset(S,A),[nonvar(S),S={} with X1],[dsubset(A1,X),XX=P,dinters(R,A2,T),T1=E],[nonvar(P),P={} with X2 with X11,nonvar(R),R={} with X2,nonvar(E),E={},A==A1,X==XX,A==A2,T==T1,X1==X11],[]). 

% f19. dsubset(A,X) & X = {X1,X2} & A neq {} & dinters({X1},A,W) & W = {} & dinters({X2},A,T) & T = {} 
fail_rule(initial,dinters(S,A,W),[nonvar(S),S={} with X1,var(W)],[W=E,dsubset(A1,X),XX=P,A2 neq EE,dinters(R,A2,T),T1=EEE],[nonvar(P),P={} with X2 with X11,nonvar(R),R={} with X2,nonvar(E),E={},nonvar(EE),EE={},nonvar(EEE),EEE={},A==A1,X==XX,A==A2,T==T1,X1==X11],[]). 

% f20. dsubset(A,X) & X = {X1,X2} & A neq {} & dinters({X1},A,W) & W = {} & dnsubset({X2},A) 
fail_rule(initial,dnsubset(R,A),[nonvar(R),R={} with X2],[dsubset(A1,X),XX=P,A2 neq EE,dinters(S,A2,W),W1=E],[nonvar(P),P={} with X2 with X11,nonvar(S),S={} with X1,nonvar(E),E={},nonvar(EE),EE={},A==A1,A==A2,X==XX,X1==X11,W==W1],[]). 

% f26. dinters(X,Y,Z) & X neq {} & Y neq {} & Z = {} & dssubset(X,Y).
fail_rule(initial,dinters(X,Y,Z),[var(X),var(Y),var(Z)],
                                 [dssubset(X1,Y1),X2 neq E,Y2 neq EE, Z1 = EEE],
                                 [nonvar(E),E={},nonvar(EE),EE={},nonvar(EEE),EEE={},
                                  X1==X,Y1==Y,Z1==Z,X2==X,Y2==Y],[]).
% f26BIS. dinters(X,Y,Z) & X neq {} & Y neq {} & Z = {} & dssubset(Y,X).
fail_rule(initial,dinters(X,Y,Z),[var(X),var(Y),var(Z)],
                                 [dssubset(Y1,X1),X2 neq E,Y2 neq EE, Z1 = EEE],
                                 [nonvar(E),E={},nonvar(EE),EE={},nonvar(EEE),EEE={},
                                  X1==X,Y1==Y,Z1==Z,X2==X,Y2==Y],[]).
% f26TER. dinters(X,Y,Z) & X neq {} & Y neq {} & Z = {} & X = Y.  
fail_rule(initial,dinters(Y,X,Z),[var(X),var(Y),var(Z)],
                                 [X1 = Y1,X2 neq E,Y2 neq EE, Z1 = EEE],
                                 [nonvar(E),E={},nonvar(EE),EE={},nonvar(EEE),EEE={},
                                  X1==X,Y1==Y,Z1==Z,X2==X,Y2==Y],[]).
% normalized:
% f26TER. dinters(Y,Y,Z) & Y neq {} & Z = {}.  
% fail_rule(initial,dinters(Y,Y,Z),[var(Y),var(Z)],
%                                 [Y1 neq E,Z1 = EE],
%                                 [nonvar(E),E={},nonvar(EE),EE={},Y1==Y,Z1==Z],[]).


%%%%%%%%%%%% using TTF predicates over relations (all not terminating)

% DomNotSubsetOfSingleton
% f2. is_rel(R) & R neq {} & dom(R,D) & ssubset(D,{X})  
fail_rule(initial,ssubset(D,S),[nonvar(S),S={} with _],[is_rel(RR),dom(R,DD),RRR neq {}],[R==RR,RR==RRR,D==DD],[]).

% SingletonNotSubsetRel.pl
% f3. is_rel(R) & ssubset({[X,Y] / Q},R) & dom(R,D) & X nin D (not terminating)
fail_rule(initial,ssubset(S,R),[nonvar(S),S=_ with [X,_]],[is_rel(R3),dom(R2,D),X2 nin D2],[R==R2,R2==R3,D==D2,X==X2],[]).

% DresCapEqual
% f4. is_rel(R) & R neq {} & dom(R,D) & dres(A,R,Q) & A = D & inters(R,Q,{})    
fail_rule(initial,dres(A,R,Q),[],[inters(R2,QQ,E),dom(R3,D),AA=DD,is_rel(R4),R5 neq EE],[nonvar(E),E={},nonvar(EE),EE={},R==R2,R2==R3,Q==QQ,A==AA,D==DD,R3==R4,R4==R5],[]).
% normalized:
% f4. is_rel(R) & R neq {} & dom(R,D) & dres(D,R,Q) & inters(R,Q,Z) & Z = {}     
% fail_rule(initial,dres(D,R,Q),[], [inters(R2,QQ,Z),Z1 = E,dom(R3,DD),is_rel(R4),R5 neq EE], [nonvar(E),E={},nonvar(EE),EE={},Z==Z1,R==R2,R2==R3,Q==QQ,D==DD,R3==R4,R4==R5],[]).

% DresEmpty2
% f5. is_rel(R) & dres(A,R,Q) & A = {} & dom(Q,D) & D neq {}
fail_rule(initial,dres(A,R,Q),[],[AA=E,is_rel(RR),dom(QQ,D),DD neq EE],[nonvar(E),E={},nonvar(EE),EE={},A==AA,R==RR,Q==QQ,D==DD],[]).

% DresEmpty
% f6. is_rel(R) & dres(A,R,Q) & A = {} & Q neq {}
fail_rule(initial,dres(A,R,Q),[],[AA=E,is_rel(RR),QQ neq EE],[nonvar(E),E={},nonvar(EE),EE={},A==AA,R==RR,Q==QQ],[]).

% DresEqual
% f7. is_rel(R) & R neq {} & dom(R,D) & dres(A,R,{}) & A = D  
fail_rule(initial,dres(A,R,E1),[nonvar(E1),E1={}],[dom(R2,D),AA=DD,is_rel(R3),R4 neq E2],[nonvar(E2),E2={},A==AA,R==R2,R2==R3,R3==R4,D==DD],[]).
% normalized:
% f7. is_rel(R) & R neq {} & dom(R,D) & dres(D,R,{})    
% fail_rule(initial,dres(D,R,E1),[nonvar(E1),E1={}],[dom(R2,DD),is_rel(R3),R4 neq E2],[nonvar(E2),E2={},R==R2,R2==R3,R3==R4,D==DD],[]).

% DresSubsetEqual
% f8. is_rel(R) & R neq {} & dom(R,D) & dres(A,R,Q) & A = D & ssubset(R,Q) 
fail_rule(initial,dres(A,R,Q),[],[ssubset(R2,QQ),is_rel(R3),R4 neq E,dom(R5,D),AA=DD],[nonvar(E),E={},R==R2,R2==R3,R3==R4,R4==R5,A==AA,D==DD,Q==QQ],[]).
% normalized:
% f8. is_rel(R) & R neq {} & dom(R,D) & dres(D,R,Q) & ssubset(R,Q)  
% fail_rule(initial,dres(D,R,Q),[],[ssubset(R2,QQ),is_rel(R3),R4 neq E,dom(R5,DD)],[nonvar(E),E={},R==R2,R2==R3,R3==R4,R4==R5,D==DD,Q==QQ],[]).

% ExtensionalUndefinition
% f9. dom(F,D) & X nin D & apply(F,X,Y)
fail_rule(initial,apply(F,X,_Y),[var(X)],[dom(FF,D),XX nin DD],[F==FF,X==XX,D==DD],[]).

% NrresCap
% f10. is_rel(R) & nrres(A,R,Q) & dom(Q,DQ) & X in DQ & dom(R,D) & inters({X / B},D,Z) & Z = {} 
fail_rule(initial,nrres(_A,R,Q),[],[inters(S,D,Z),Z2=E,is_rel(R2),dom(R3,D2),dom(Q2,DQ),X2 in DQ2],[nonvar(S),S=_B with X,nonvar(E),E={},R==R2,R2==R3,D==D2,Q==Q2,DQ==DQ2,X==X2,Z==Z2],[]).

% RanNotSubsetOfSingleton
% f11. is_rel(R) & R neq {} & ran(R,Ran) & ssubset(Ran,{Y})
fail_rule(initial,ssubset(Ran,S),[nonvar(S),S={} with _Y],[ran(R,Ran2),is_rel(R2),R3 neq E],[nonvar(E),E={},R==R2,R2==R3,Ran==Ran2],[]).

% RresEmpty2
% f12. is_rel(R) & rres(A,R,Q) & A = {} & dom(Q,DQ) &  DQ neq {}
fail_rule(initial,rres(A,R,Q),[],[AA={},is_rel(RR),dom(QQ,DQ),DDQ neq E],[nonvar(E),E={},A==AA,R==RR,Q==QQ,DQ==DDQ],[]).

% RresEmpty4
% f13. is_rel(R) & ran(R,RRan) & inters(A,RRan,{}) & rres(A,R,Q) & dom(Q,DQ) &  DQ neq {}  
fail_rule(initial,rres(A,R,Q),[],[inters(AA,RRan,E),is_rel(RR),ran(RR,RRRan),dom(QQ,DQ),DDQ neq EE],[nonvar(E),E={},nonvar(EE),EE={},A==AA,R==RR,Q==QQ,DQ==DDQ,RRan==RRRan],[]).
% normalized:
% f13. is_rel(R) & ran(R,RRan) & inters(A,RRan,Z) & Z={} & rres(A,R,Q) & dom(Q,DQ) &  DQ neq {}  
% fail_rule(initial,rres(A,R,Q),[],[inters(AA,RRan,Z),Z1=E,is_rel(RR),ran(RR,RRRan),dom(QQ,DQ),DDQ neq EE], [nonvar(E),E={},nonvar(EE),EE={},Z==Z1,A==AA,R==RR,Q==QQ,DQ==DDQ,RRan==RRRan],[]).

% SingletonMappletNotEqualRel1
% f14. is_rel(R) & R = {[X,Y] / Q} & dom(R,D) & X nin D
fail_rule(initial,R = S,[nonvar(S),S=_Q with [X,_Y]],[dom(R2,D),is_rel(R3),X2 nin D2],[R==R2,R2==R3,D==D2,X==X2],[]).

% SingletonMappletNotInDom
% f15. is_rel(R) & dom(R,D) & X nin D & dom({[X,Y] / B},DS) & D = DS 
fail_rule(initial,dom(S,DS),[nonvar(S),S=_B with [X,_Y]],[dom(R,D),is_rel(R2),X2 nin D2,D3=DS2],[R==R2,D==D2,D2==D3,X==X2,DS==DS2],[]).
% normalized:
% f15. is_rel(R) & dom(R,DS) & X nin DS & dom({[X,Y] / B},DS)  
% fail_rule(initial,dom(S,DS),[nonvar(S),S=_B with [X,_Y]],[dom(R,DS1),is_rel(R2),X2 nin DS2],[R==R2,X==X2,DS==DS1,DS==DS2],[]).

% SingletonNotSubsetDom
% f16. is_rel(R) & dom(R,D) & X nin D & dom({[X,Y] / B},DS) & ssubset(DS,D)
fail_rule(initial,dom(S,DS),[nonvar(S),S=_B with [X,_Y]],[dom(R,D),is_rel(R2),X2 nin D2,ssubset(DS2,D3)],[R==R2,D==D2,D2==D3,X==X2,DS==DS2],[]).

% NotSubsetOfSingletonMapplet
% f17. R neq {} & dom(R,D) & dom({[X,Y]},M) & ssubset(D,M)
fail_rule(initial,ssubset(D,M),[var(D)], [R neq E,dom(R1,D1),dom(S,M1)], [nonvar(E),E={},nonvar(S),S={} with [_X,_Y],D1==D,M1==M,R1==R],[]).


%%%%%%%%%%%% using relations over integers
%%%%%%%%%%%% (terminating, provided all variables have "not too big" domains)

% f21. NatRangeNotEq3
% I=int(X,Y) & J=int(a,b) & I=J & X is Z+N & Y is Z+M & N is V*h & M =< P & P is W*h & W is V+k  
% and a,b,h,k integer constants >= 0 and it holds that b-a > k*h
%
fail_rule(initial,I=int(X,Y),
                  [var(I),var(X),var(Y)],
                  [X1 is Z+N, Y1 is Z1+M, N is V*H, P >= M, P1 is W*H, W is V1+K, J=int(A,B), I1=J1],
                  [integer(A),A>=0,integer(B),B>=0,var(J),
                   var(I1),var(J1),var(X1),var(Y1),
                   var(N),integer(H),H>=0,
                   var(P),var(M),var(P1),
                   var(W),integer(K),K>=0, B-A > K*H,
                   I==I1,J==J1,X==X1,Y==Y1,Z==Z1,P==P1,V==V1],[]).
% normalized:
% I=int(X,Y) & I=int(a,b) & X is Z+N & Y is Z+M & N is V*h & M =< P & P is W*h & W is V+k  
%
% fail_rule(initial,I=int(X,Y),
%                  [var(I),var(X),var(Y)],
%                  [X1 is Z+N, Y1 is Z1+M, N is V*H, P >= M, P1 is W*H, W is V1+K, I1=int(A,B)],
%                  [integer(A),A>=0,integer(B),B>=0, var(I1),var(X1),var(Y1), var(N),integer(H),H>=0, var(P),var(M),var(P1), var(W),integer(K),K>=0, B-A > K*H, I==I1,X==X1,Y==Y1,Z==Z1,P==P1,V==V1],[]).

% f22. NatRangeNotSubset
% I=int(X,Y) & J=int(Kn,Km) & essubset(J,I) & X is N+Za & Y is N+Zb & Za is M*Kp & Zb is Zc*Kp & Zc is M+Kq
% with Km-Kn > Kq*Kp
%
fail_rule(initial,I=int(X,Y),
                  [var(I),var(X),var(Y)],
                  [X1 is N+Za, Y1 is N1+Zb, Za1 is M*Kp, Zb1 is Zc*Kp, Zc1 is M1+Kq, J=int(Kn,Km), essubset(J1,I1)],
                  [integer(Kn),Kn>=0,integer(Km),Km>=0,var(J),
                   var(I1),var(J1),var(X1),var(Y1),
                   var(N),var(M),var(Za),var(Zb),var(Zc),
                   var(N1),var(M1),var(Za1),var(Zb1),var(Zc1),
                   integer(Kq),Kq>=0,integer(Kp),Kq>=0,Km-Kn > Kq*Kp,
                   I==I1,J==J1,X==X1,Y==Y1,N==N1,M==M1,Za=Za1,Zb==Zb1,Zc==Zc1],[]).

% f23. NatRangeNotEq
% I=int(X,Y) & J=int(Kn,Km) & I=J & X is N+Za & Y is N+Zb & Za is M*Kp & Zb is Zc*Kp & Zc is M+Kq 
% with Km-Kn > Kq*Kp
%
fail_rule(initial,I=int(X,Y),
                  [var(I),var(X),var(Y)],
                  [X1 is N+Za, Y1 is N1+Zb, Za1 is M*Kp, Zb1 is Zc*Kp, Zc1 is M1+Kq, J=int(Kn,Km), I1=J1],
                  [integer(Kn),Kn>=0,integer(Km),Km>=0,var(J),
                   var(I1),var(J1),var(X1),var(Y1),
                   var(N),var(M),var(Za),var(Zb),var(Zc),
                   var(N1),var(M1),var(Za1),var(Zb1),var(Zc1),
                   integer(Kq),Kq>=0,integer(Kp),Kq>=0,Km-Kn > Kq*Kp,
                   I==I1,J==J1,X==X1,Y==Y1,N==N1,M==M1,Za=Za1,Zb==Zb1,Zc==Zc1],[]).
% normalized
% I=int(X,Y) & I=int(Kn,Km) & X is N+Za & Y is N+Zb & Za is M*Kp & Zb is Zc*Kp & Zc is M+Kq   
%
% fail_rule(initial,I=int(X,Y),
%                  [var(I),var(X),var(Y)],
%                  [X1 is N+Za, Y1 is N1+Zb, Za1 is M*Kp, Zb1 is Zc*Kp, Zc1 is M1+Kq, I1=int(Kn,Km)],
%                  [integer(Kn),Kn>=0,integer(Km),Km>=0,var(I1),var(X1),var(Y1), var(N),var(M),var(Za),var(Zb),var(Zc), var(N1),var(M1),var(Za1),var(Zb1),var(Zc1),
%                   integer(Kq),Kq>=0,integer(Kp),Kq>=0,Km-Kn > Kq*Kp, I==I1,X==X1,Y==Y1,N==N1,M==M1,Za=Za1,Zb==Zb1,Zc==Zc1],[]).

% f24. NatRangeNotEmpty3
% I=int(X,Y) & I={} & X is N+Za & Y is N+Zb &  Za is M*Kn & Zb is Zc*Kn & Zc is M+Km
%
fail_rule(initial,I=int(X,Y),
                  [var(I),var(X),var(Y)],
                  [X1 is N+Za, Y1 is N1+Zb, Za1 is M*Kn, Zb1 is Zc*Kn, Zc1 is M1+Km, I1=E],
                  [nonvar(E),E={},
                   integer(Kn),Kn>=0,integer(Km),Km>=0,
                   var(I1),var(X1),var(Y1),
                   var(N),var(M),var(Za),var(Zb),var(Zc),
                   var(N1),var(M1),var(Za1),var(Zb1),var(Zc1),
                   I==I1,X==X1,Y==Y1,N==N1,M==M1,Za=Za1,Zb==Zb1,Zc==Zc1],[]).

% f25. NatRangeNotEmpty4
% I=int(N,Y) & I={} & Y is N+M
%
fail_rule(initial,I=int(N,Y),
                  [var(I),var(N),var(Y)],
                  [Y1 is N1+M, I1=E],
                  [nonvar(E),E={},var(I1),var(Y1),var(N),var(N1),var(M),I==I1,Y==Y1,N==N1],[]).
