eq(f0(A,B,C,D,E,F,G,H,I,J),1,[f16(0,B,C,D,E,F,G,0,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(f0(A,B,C,D,E,F,G,H,I,J),1,[f16(0,B,C,D,E,F,G,0,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,[f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),loop_cont_f33(L,M,N,O,P,Q,R,S,T,U)],[K=0]). eq(loop_cont_f16(A,B,C,D,E,F,G,H,I,J),0,[f33(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_f33(A,B,C,D,E,F,G,H,I,J),0,[f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),loop_cont_f52(L,M,N,O,P,Q,R,S,T,U)],[K=0]). eq(loop_cont_f33(A,B,C,D,E,F,G,H,I,J),0,[f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[K=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,0,C,D,E,F,G,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_f19(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0,19>=A]). 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,0,C,D,E,F,G,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1)],[K=1,V=1,19>=A]). eq(f19(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+1,C,D,E,F,G,V,I,V,K,L,M,N,O,P,Q,R,S,T,U)],[19>=B]). eq(f33(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,0,E,F,G,H,I,J,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,19>=C]). eq(f33(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,0,E,F,G,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1)],[K=1,V=1,19>=C]). eq(f36(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,V,V,J,K,L,M,N,O,P,Q,R,S,T,U)],[19>=D]). eq(f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f55(A,B,C,D,E,0,G,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_f55(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0,19>=E]). eq(f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f55(A,B,C,D,E,0,G,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1)],[K=1,V=1,19>=E]). eq(f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f59(A,B,C,D,E,F,0,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_f59(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0,19>=F]). eq(f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f59(A,B,C,D,E,F,0,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1)],[K=1,V=1,19>=F]). eq(f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[f59(A,B,C,D,E,F,G+1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[19>=G]). eq(loop_cont_f19(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(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,[f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(loop_cont_f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),0,[f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(loop_cont_f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),0,[f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(f16(A,B,C,D,E,F,G,H,I,J,K,A,B,0,D,E,F,G,H,I,J),1,[],[K=0,A>=20]). eq(f19(A,B,C,D,E,F,G,H,I,J,K,A+1,B,C,D,E,F,G,H,I,J),1,[],[K=0,B>=20]). eq(f33(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,0,F,G,H,I,J),1,[],[K=0,C>=20]). eq(f36(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,D>=20]). eq(f52(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),1,[],[K=1,E>=20]). eq(f55(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E+1,F,G,H,I,J),1,[],[K=0,F>=20]). eq(f59(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F+1,G,H,I,J),1,[],[K=0,G>=20]).