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