eq(f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f9(17,1,0,S,E,F,G,H,I,J,K,T,M,N,O,P,Q,R,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1),loop_cont_f9(V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1)],[U=0]).
eq(f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f9(17,1,0,S,E,F,G,H,I,J,K,T,M,N,O,P,Q,R,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1)],[U=1]).
eq(loop_cont_f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),0,[f5(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),loop_cont_f5(T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[S=0]).
eq(loop_cont_f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),0,[f5(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)],[S=1]).
eq(f9(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),1,[f9(A,1+B,1+C,L1,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)],[A>=1+B,C>=0]).
eq(f5(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),1,[f5(A,B,C,D,1+E,-1+F,M,0,L1,M1,K,M,N,N1,O1,E,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[P1>=Q1,E>=0,F>=0,H=0]).
eq(f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,1,T-3+C,U,0,V,W,K,U,X,Y,Z,P,D,-2+C),1,[],[S=0,C>=2,B>=A,A1>=B1]).
eq(f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),0,[],[S=1]).
eq(f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,F,T,G,U,V,W,L,M,N,O,P,Q,R),1,[],[S=1,X>=Y+1,E>=1,F>=0]).
eq(f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,F,G,0,T,U,K,M,M,0,O,E,V,R),1,[],[S=1,W>=X,E>=0,F>=0,N=0,H=0]).