eq(f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[f7(8,0,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,L1,M1,N1,O1),loop_cont_f7(V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1)],[U=0]). eq(f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[f7(8,0,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,L1,M1,N1,O1)],[U=1]). eq(loop_cont_f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),0,[f62(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,L1,M1,N1,O1),loop_cont_f62(V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1)],[U=0]). eq(loop_cont_f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),0,[f62(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,L1,M1,N1,O1)],[U=1]). eq(f7(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,L1,M1,N1,O1),1,[f7(A,B+1,P1+Q1,R1,S1+T1,U1,V1+W1,X1,Y1+Z1,A2,P1+Q1+Y1+Z1,P1+Q1-Y1-Z1,S1+T1+V1+W1,S1+T1-V1-W1,-3196,B2,C2,D2+E2,F2+E2,E2,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1)],[7>=B]). eq(f62(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,L1,M1,N1,O1),1,[f62(A,B+1,P1+Q1,R1,S1+T1,U1,V1+W1,X1,Y1+Z1,A2,P1+Q1+Y1+Z1,P1+Q1-Y1-Z1,S1+T1+V1+W1,S1+T1-V1-W1,-3196,B2,C2,D2+E2,F2+E2,E2,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1)],[7>=B]). eq(f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,A,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[],[U=0,B>=8]). eq(f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[],[U=1,B>=8]).