eq(f0(A,B,C,D,E,F,G,H,I,J),1,[f10(1,B,0,9,1,K,G,H,I,J,L,M,N,O,P,Q,R,S,T,U,V),loop_cont_f10(M,N,O,P,Q,R,S,T,U,V)],[L=0]). eq(f0(A,B,C,D,E,F,G,H,I,J),1,[f10(1,B,0,9,1,K,G,H,I,J,L,M,N,O,P,Q,R,S,T,U,V)],[L=1]). eq(f49(A,B,C,D,E,F,G,H,I,J),1,[f56(A,B,C,D,E,F,G,H,I,0)],[0>=A+1]). eq(f49(A,B,C,D,E,F,G,H,I,J),1,[f56(A,B,C,D,E,F,G,H,I,0)],[A>=1]). eq(f49(A,B,C,D,E,F,G,H,I,J),1,[f56(0,B,C,D,E,F,G,H,I,1)],[A=0]). eq(loop_cont_f10(A,B,C,D,E,F,G,H,I,J),0,[f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),loop_cont_f16(L,M,N,O,P,Q,R,S,T,U)],[K=0]). eq(loop_cont_f10(A,B,C,D,E,F,G,H,I,J),0,[f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[K=1]). eq(loop_cont_f16(A,B,C,D,E,F,G,H,I,J),0,[f49(A,B,C,D,E,F,G,H,I,J)],[]). eq(f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f10(A,B,C+1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[D>=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,[f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[0>=E+1,D>=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,[f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[E>=1,D>=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,[f27(A,0,C,D,0,F,0,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_f27(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0,D>=C+1,E=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,[f27(A,0,C,D,0,F,0,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1)],[K=1,V=1,D>=C+1,E=0]). eq(f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[D>=B+1,B>=C+1]). eq(f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[C>=1+B,D>=B+1]). eq(f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f27(A,C+1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[D>=B+1,C=B]). eq(f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f27(A,0,C,D,1,F,1,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_f27(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0,D>=G1+1]). eq(f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f27(A,0,C,D,0,F,0,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_f27(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0]). eq(f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f27(A,0,C,D,0,F,0,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_f27(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0,0>=G1+1]). eq(loop_cont_f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),0,[f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[0>=A+1]). eq(f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[A>=1]). eq(f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(0,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[A=0]). eq(f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(1,B,C,D,E,F,G,1,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[V>=W+1]). eq(f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(1,B,C,D,E,F,G,1,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f36(0,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[0>=A+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,[f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[A>=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,[f27(0,B+1,C,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U)],[A=0]). eq(f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[B+V>=C+W+1]). eq(f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[C+V>=1+B+W]). eq(f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f27(0,B+1,C,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f27(1,B+1,C,D,E,F,G,H,1,J,K,L,M,N,O,P,Q,R,S,T,U)],[B+V>=C+W+1]). eq(f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f27(1,B+1,C,D,E,F,G,H,1,J,K,L,M,N,O,P,Q,R,S,T,U)],[C+V>=1+B+W]). eq(f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f27(0,B+1,C,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(f10(A,B,C,D,E,F,G,H,I,J,K,A,B,0,D,E,F,G,H,I,J),1,[],[K=0,C>=D]). 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=0,0>=E+1,C>=D]). eq(f16(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(f16(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),1,[],[K=0,E>=1,C>=D]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,0,F,G,H,I,1),1,[],[K=1,C>=D,E=0]). eq(f27(A,B,C,D,E,F,G,H,I,J,K,A,B,C+1,D,E,F,G,H,I,J),1,[],[K=0,B>=D]). eq(f27(A,B,C,D+1,E,F,G,H,I,J,K,A,B,C,D+1,E,F,G,H,I,J),0,[],[K=1,D>=B]).