eq(f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N),1,[f4(O,P,Q,R,S,F,G,T,U,V,W,0,X,N)],[0>=T,0>=Y]).
eq(f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N),1,[f4(O,P,Q,R,S,F,G,1,T,U,V,D,W,N)],[]).
eq(f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N),1,[f1(O,2,P,Q,P,F,G,O,P,J,K,L,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1),loop_cont_f1(U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1)],[T=0,O>=2]).
eq(f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N),1,[f1(O,2,P,Q,P,F,G,O,P,J,K,L,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1)],[T=1,O>=2]).
eq(f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1),1,[f1(A,1+B,D,D1,D,E1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1)],[A>=B+1,B>=0]).
eq(f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,F,G,U,V,W,X,C,M,N),1,[],[O=1,B>=A,B>=0,Q>=U,U>=2]).