eq(f0(A,B,C,D,E,F,G,H,I,J),1,[f15(1,4,K,0,L,0,0,0,0,0,M,N,O,P,Q,R,S,T,U,V,W),loop_cont_f15(N,O,P,Q,R,S,T,U,V,W)],[M=0,K>=0,L>=0]).
eq(f0(A,B,C,D,E,F,G,H,I,J),1,[f15(1,4,K,0,L,0,0,0,0,0,M,N,O,P,Q,R,S,T,U,V,W)],[M=1,K>=0,L>=0]).
eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A,B,C,D+1,E,0,0,0,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_f36(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0,0>=D,0>=C,B>=1,I=0]).
eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A,B-1,C,0,E,V,0,0,0,0,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),loop_cont_f36(X,Y,Z,A1,B1,C1,D1,E1,F1,G1,K,L,M,N,O,P,Q,R,S,T,U)],[W=0,D>=1,0>=C,V>=0,B>=1,1>=V,I=0]).
eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A+1,A+4,V,0,E,W,0,0,0,0,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1),loop_cont_f36(Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,K,L,M,N,O,P,Q,R,S,T,U)],[X=0,0>=C,W>=0,1>=W,0>=B,V>=0,I=0]).
eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A,B,C-1,D,E,V,0,0,0,0,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),loop_cont_f36(X,Y,Z,A1,B1,C1,D1,E1,F1,G1,K,L,M,N,O,P,Q,R,S,T,U)],[W=0,C>=1,1>=V,V>=0,I=0]).
eq(f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f48(A,B,C,D+1,E,F,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[E>=J,0>=H,0>=D,0>=C,B>=1]).
eq(f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f48(A,B-1,C,0,E,F,V,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[E>=J,0>=H,D>=1,0>=C,V>=0,B>=1,1>=V]).
eq(f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f48(A+1,A+4,V,0,E,F,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[E>=J,0>=H,0>=C,W>=0,1>=W,0>=B,V>=0]).
eq(f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f48(A,B,C-1,D,E,F,V,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[E>=J,0>=H,C>=1,1>=V,V>=0]).
eq(loop_cont_f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),0,[f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[]).
eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A,B,C,D,E,F,G,H,I,J+1,K,L,M,N,O,P,Q,R,S,T,U)],[E+1>=A,0>=G]).
eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A,B,C,D,E,F,G,H,I,J+1,K,L,M,N,O,P,Q,R,S,T,U)],[G>=1,E+1>=A,F>=1]).
eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A,B,C,D+1,E,F,G,0,I,J+1,K,L,M,N,O,P,Q,R,S,T,U)],[G>=1,0>=F,E+1>=A,0>=D,0>=C,B>=1]).
eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A,B-1,C,0,E,F,G,V,I,J+1,K,L,M,N,O,P,Q,R,S,T,U)],[G>=1,0>=F,E+1>=A,D>=1,0>=C,V>=0,B>=1,1>=V]).
eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A+1,A+4,V,0,E,F,G,W,I,J+1,K,L,M,N,O,P,Q,R,S,T,U)],[G>=1,0>=F,E>=A,0>=C,W>=0,1>=W,0>=B,V>=0]).
eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(A,B,C-1,D,E,F,G,V,I,J+1,K,L,M,N,O,P,Q,R,S,T,U)],[G>=1,0>=F,E+1>=A,C>=1,1>=V,V>=0]).
eq(f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[E+1>=A,H>=1]).
eq(f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f15(A,B,C,D,E,F,G,H,1,J,K,L,M,N,O,P,Q,R,S,T,U)],[E+1>=A,0>=H]).
eq(f15(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+1]).
eq(f15(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),1,[],[K=1,I>=1]).
eq(f36(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),1,[],[K=0,0>=H,J>=1+E]).
eq(f36(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),0,[],[K=1]).
eq(f36(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),1,[],[K=0,H>=1]).
eq(f36(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),0,[],[K=1,1>=H+1]).