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