eq(f0(A,B,C,D,E,F,G,H,I,J,K),1,[f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),loop_cont_f12(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,[f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[L=1]). eq(loop_cont_f12(A,B,C,D,E,F,G,H,I,J,K),0,[f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),loop_cont_f28(M,N,O,P,Q,R,S,T,U,V,W)],[L=0]). eq(loop_cont_f12(A,B,C,D,E,F,G,H,I,J,K),0,[f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[L=1]). eq(f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f15(A,B,0,D,E,F,G,H,I,J,K,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1),loop_cont_f15(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,A>=B]). eq(f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f15(A,B,0,D,E,F,G,H,I,J,K,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1)],[L=1,X=1,A>=B]). eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f15(A,B,C,D+1,X,X,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[C>=X,A>=D]). eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f15(A,B,X,D+1,X,X,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[X>=1+C,A>=D]). eq(f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f30(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_f30(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,A>=D]). eq(f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f30(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,A>=D]). eq(f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f33(A,B,C,D,E,F,X,H,I,J,K,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1),loop_cont_f33(Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,M,N,O,P,Q,R,S,T,U,V,W)],[Y=0,D>=B+1]). eq(f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f33(A,B,C,D,E,F,X,H,I,J,K,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1)],[L=1,Y=1,D>=B+1]). eq(f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f33(A,B,C,D,E,F,X,H+1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[B>=H+1]). eq(f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f45(A,B,C,D,E,F,X,H,I,J,K,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1),loop_cont_f45(Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,M,N,O,P,Q,R,S,T,U,V,W)],[Y=0,A>=B]). eq(f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f45(A,B,C,D,E,F,X,H,I,J,K,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1)],[L=1,Y=1,A>=B]). eq(f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f45(A,B,C,D,E,F,X,H+1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[D>=H+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,[f59(A,B,C,D,E,F,G,H+1,X,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[A>=H]). eq(f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f73(A,B+1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[A>=B]). eq(loop_cont_f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f12(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_f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f42(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_f42(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_f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f42(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(loop_cont_f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f30(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_f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f42(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_f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f69(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_f42(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,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1),loop_cont_f59(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(f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[0>=X+1]). eq(f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f71(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_f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[]). eq(f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f28(A,B,C,A+1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[A=D]). eq(f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f73(A,B,C,D,E,F,G,H,X,J,K,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1),loop_cont_f73(Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,M,N,O,P,Q,R,S,T,U,V,W)],[Y=0,A>=D+1]). eq(f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),1,[f73(A,B,C,D,E,F,G,H,X,J,K,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1),loop_cont_f73(Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,M,N,O,P,Q,R,S,T,U,V,W)],[Y=0,D>=1+A]). eq(loop_cont_f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W),0,[f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W)],[]). eq(f12(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,B>=1+A]). eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,A,B+1,C,D,E,F,G,H,I,J,K),1,[],[L=0,0>=C+1,D>=1+A]). eq(f15(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]). eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,A,B+1,C,D,E,F,G,H,I,J,K),1,[],[L=0,C>=1,D>=1+A]). eq(f15(A,B,C,D,E,F,G,H,I,J,K,L,A,B+1,0,D,E,F,G,H,I,J,K),1,[],[L=0,D>=1+A,C=0]). eq(f28(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,D>=1+A]). eq(f30(A,B,C,D,E,F,G,H,I,J,K,L,A,B,0,D,E,F,G,H,I,J,K),1,[],[L=0,B>=D]). eq(f33(A,B,C,D,E,F,G,H,I,J,K,L,A,B+1,C,D,E,F,G,H,I,J,K),1,[],[L=0,H>=B]). eq(f42(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,B>=1+A,K>=D+1]). eq(f42(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]). eq(f42(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,B>=1+A,D>=1+K]). eq(f42(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D,E,F,G,H,I,J,D),1,[],[L=0,B>=1+A,D=K]). eq(f45(A,B,C,D,E,F,G,H,I,J,K,L,A,B+1,C,D,E,F,G,H,M,N,K),1,[],[L=0,C>=M+1,H>=D]). eq(f45(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]). eq(f45(A,B,C,D,E,F,G,H,I,J,K,L,A,B+1,M,D,E,F,G,H,M,N,B),1,[],[L=0,M>=C,H>=D]). eq(f59(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,H>=1+A]). eq(f73(A,B,C,D,E,F,G,H,I,J,K,L,A,B,C,D+1,E,F,G,H,I,J,K),1,[],[L=0,B>=1+A]).