eq(f0(A,B,C,D,E,F,G,H,I,J),1,[f16(A,1,0,1,K,0,L,M,N,J,O,P,Q,R,S,T,U,V,W,X,Y),loop_cont_f16(P,Q,R,S,T,U,V,W,X,Y)],[O=0,N>=0,M>=N,M>=0,L>=M,K>=0,L>=0]). eq(f0(A,B,C,D,E,F,G,H,I,J),1,[f16(A,1,0,1,K,0,L,M,N,J,O,P,Q,R,S,T,U,V,W,X,Y)],[O=1,N>=0,M>=N,M>=0,L>=M,K>=0,L>=0]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f25(0,B,C,D,E,F+1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=1,0>=F,0>=E]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f25(V,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=1,F>=2,0>=E,1>=V,V>=0]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f25(1,B,C+1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=1,0>=E,0>=C,F=1]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f25(0,B,0,D-1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=1,0>=E,D>=1,F=1,C=1]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f25(V,B+1,0,B+1,W,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=1,0>=E,V>=0,1>=V,C>=2,W>=0,F=1]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f25(V,B+1,0,B+1,W,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=1,0>=E,0>=D,V>=0,1>=V,W>=0,F=1,C=1]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f25(V,B,C,D,E-1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=1,E>=1,1>=V,V>=0]). eq(f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[0>=A]). eq(f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f50(A,B,C,D,E,F+1,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U)],[A>=1,0>=F,0>=E]). eq(f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f50(A,B,C,D,E,F,G,H,I,V,K,L,M,N,O,P,Q,R,S,T,U)],[A>=1,F>=2,0>=E,1>=V,V>=0]). eq(f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f50(A,B,C+1,D,E,F,G,H,I,1,K,L,M,N,O,P,Q,R,S,T,U)],[A>=1,0>=E,0>=C,F=1]). eq(f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f50(A,B,0,D-1,E,F,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U)],[A>=1,0>=E,D>=1,F=1,C=1]). eq(f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f50(A,B+1,0,B+1,V,0,G,H,I,W,K,L,M,N,O,P,Q,R,S,T,U)],[A>=1,0>=E,W>=0,1>=W,C>=2,V>=0,F=1]). eq(f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f50(A,B+1,0,B+1,V,0,G,H,I,W,K,L,M,N,O,P,Q,R,S,T,U)],[A>=1,0>=E,0>=D,W>=0,1>=W,V>=0,F=1,C=1]). eq(f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f50(A,B,C,D,E-1,F,G,H,I,V,K,L,M,N,O,P,Q,R,S,T,U)],[A>=1,E>=1,1>=V,V>=0]). eq(f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=H,J>=1]). eq(f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f16(A,B,C,D,E,F,G,H,I+1,J,K,L,M,N,O,P,Q,R,S,T,U)],[H>=I+1,J>=1]). eq(f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f16(A,B,C,D,E,F,G,H,I-1,J,K,L,M,N,O,P,Q,R,S,T,U)],[0>=J]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),1,[],[K=1,0>=I]).