eq(f0(A,B,C,D,E,F,G,H,I,J,K),1,[f11(A,10,20,1,20,0,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),loop_cont_f11(M,N,O,P,Q,R,S,T,U,V,W)],[L=0]). eq(f0(A,B,C,D,E,F,G,H,I,J,K),1,[f11(A,10,20,1,20,0,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[L=1]). eq(f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f11(A,B,C,D,E,F,1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[D>=E,G=0]). eq(f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f11(A,B,C,D,E,F,1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[D+1>=E,E>=2+D,G=0]). eq(f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f11(A,B,C,D,D+1,F,1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[E=D+1,G=0]). eq(f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f11(A,B,C,D,D+1,F,1,X,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[Y>=Z+1,E=D+1,G=0]). eq(f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f40(E,B,C,D,E,F,0,X,Y,D+1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1),loop_cont_f40(B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,L,M,N,O,P,Q,R,S,T,U,V,W)],[A1=0,E>=2+D,G=0]). eq(f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f40(E,B,C,D,E,F,0,X,Y,D+1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1)],[L=1,A1=1,E>=2+D,G=0]). eq(f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f43(A,B,C,D,E,0,G,H,I,J+1,K,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1),loop_cont_f43(Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,L,M,N,O,P,Q,R,S,T,U,V,W)],[X=0,F=0]). eq(f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f43(A,B,C,D,E,0,G,H,I,J+1,K,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1)],[L=1,X=1,F=0]). eq(f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f43(A,B,C,D,E,F,G,H,I,J+1,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[K>=X+1]). eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f48(A-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[]). eq(loop_cont_f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[]). eq(loop_cont_f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f48(A,B,C,D,E,F,G,H,I,J,K,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1),loop_cont_f48(Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,L,M,N,O,P,Q,R,S,T,U,V,W)],[X=0]). eq(loop_cont_f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f48(A,B,C,D,E,F,G,H,I,J,K,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1)],[L=1,X=1]). eq(f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[B>=A+1]). eq(f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f63(A,B,C,D,A-1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[A>=B]). eq(loop_cont_f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[]). eq(f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[A>=1+B]). eq(f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f11(A,B,C,J,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[B>=A]). eq(f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[0>=F+1]). eq(f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[F>=1]). eq(f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f40(A,B,C,D,E,0,G,X,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[F=0]). eq(f11(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,K),1,[],[L=1,0>=G+1]). eq(f11(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,K),1,[],[L=1,G>=1]). eq(f40(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,K),1,[],[L=0,0>=F+1]). eq(f40(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,K),0,[],[L=1,F>=0]). eq(f40(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,K),1,[],[L=0,F>=1]). eq(f40(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,K),0,[],[L=1,1>=F+1]). eq(f43(A,B,C,D,E,F,G,H,I,J,K,L,A-1,B,C,D,E,F,G,H,I,J,K),1,[],[L=0]). eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,K),1,[],[L=0,A>=J]). eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,1,G,H,I,J,K),1,[],[L=0,J>=A+1]). eq(f48(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,K),0,[],[L=1,A>=J]).