eq(f0(A,B,C,D,E,F,G,H,I),1,[f9(0,1,1,0,0,J,G,H,I,K,L,M,N,O,P,Q,R,S,T),loop_cont_f9(L,M,N,O,P,Q,R,S,T)],[K=0,J>=1]).
eq(f0(A,B,C,D,E,F,G,H,I),1,[f9(0,1,1,0,0,J,G,H,I,K,L,M,N,O,P,Q,R,S,T)],[K=1,J>=1]).
eq(f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f20(A,B,C-1,D,D,0,A-2,1,A-2,J,K,L,M,N,O,P,Q,R,S)],[A>=3,C>=1,D=E,F=0]).
eq(f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f20(A,B,C-1,D,D,0,A,0,A,J,K,L,M,N,O,P,Q,R,S)],[2>=A,C>=1,D=E,F=0]).
eq(f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f20(0,B+1,B+1,D,D,T,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[T>=1,A>=3,0>=C,D=E,F=0]).
eq(f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f20(A+1,B+1,B+1,D,D,T,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[T>=1,2>=A,0>=C,D=E,F=0]).
eq(f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f20(A,B,C,D,D,F-1,G,T,U,J,K,L,M,N,O,P,Q,R,S)],[0>=F+1,D=E]).
eq(f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f20(A,B,C,D,D,F-1,G,T,U,J,K,L,M,N,O,P,Q,R,S)],[F>=1,D=E]).
eq(f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f32(A,B,C,0,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S)],[I=0]).
eq(f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f32(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[0>=I+1]).
eq(f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f32(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[I>=1]).
eq(f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f9(A,B,C,D,0,F,G,0,I,J,K,L,M,N,O,P,Q,R,S)],[H=0]).
eq(f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f9(A,B,C,D,1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[0>=H+1]).
eq(f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[f9(A,B,C,D,1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[H>=1]).
eq(f9(A,B,C,D,E,F,G,H,I,J,A,B,C,D,E,F,G,H,I),1,[],[J=1,E>=D+1]).
eq(f9(A,B,C,D,E,F,G,H,I,J,A,B,C,D,E,F,G,H,I),1,[],[J=1,D>=1+E]).