eq(start(A,B,C,D,E,F,G,H),1,[f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),loop_cont_f2(J,K,L,M,N,O,P,Q)],[I=0]). eq(start(A,B,C,D,E,F,G,H),1,[f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[I=1]). eq(f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f8(A,B,0,B,E,F,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_f8(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,A>=B+1]). eq(f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f8(A,B,0,B,E,F,G,H,R,S,T,U,V,W,X,Y,Z)],[I=1,R=1,A>=B+1]). eq(f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f8(A,B,C,D,E+1,R,S,H,I,J,K,L,M,N,O,P,Q)],[A>=E,S>=R]). eq(f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f8(A,B,R,E,E+1,S,T,H,I,J,K,L,M,N,O,P,Q)],[A>=E,S>=1+T]). eq(f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f19(A,B,C,D,E+1,F,G,R,I,J,K,L,M,N,O,P,Q)],[A>=E]). eq(f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f27(A,B,C,D,E+1,F,G,R,I,J,K,L,M,N,O,P,Q)],[A>=E]). eq(f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f36(A,B,C,D+1,E,F,G,0,I,J,K,L,M,N,O,P,Q)],[A>=D]). eq(f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f43(A,B,C,D,E,F,G,R,S,T,U,V,W,X,Y,Z,A1),loop_cont_f43(T,U,V,W,X,Y,Z,A1,I,J,K,L,M,N,O,P,Q)],[S=0,A>=D,0>=B1+1]). eq(f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f43(A,B,C,D,E,F,G,R,S,T,U,V,W,X,Y,Z,A1),loop_cont_f43(T,U,V,W,X,Y,Z,A1,I,J,K,L,M,N,O,P,Q)],[S=0,A>=D,B1>=1]). eq(f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f43(A,B,C,D,E+1,F,G,H,I,J,K,L,M,N,O,P,Q)],[A>=E]). eq(f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f49(A,B,C,D,E+1,F,G,H,I,J,K,L,M,N,O,P,Q)],[A>=E]). eq(loop_cont_f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[]). eq(loop_cont_f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f19(A,B,C,D,E,F,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_f19(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0]). eq(loop_cont_f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f49(A,B,C,D,E,F,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_f49(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0]). eq(loop_cont_f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f49(A,B,C,D,E,F,G,H,R,S,T,U,V,W,X,Y,Z)],[I=1,R=1]). eq(f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f2(A,B+1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[C=0]). eq(f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f36(A,B,C,D,E,F,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_f36(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,0>=C+1]). eq(f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[f36(A,B,C,D,E,F,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_f36(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,C>=1]). eq(loop_cont_f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f27(A,B,C,D,E,F,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_f27(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0]). eq(loop_cont_f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f27(A,B,C,D,E,F,G,H,R,S,T,U,V,W,X,Y,Z)],[I=1,R=1]). eq(loop_cont_f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[]). eq(loop_cont_f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[]). eq(loop_cont_f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[]). eq(f2(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=1,B>=A]). eq(f8(A,B,C,D,E,F,G,H,I,A,B,C,B,E,F,G,H),1,[],[I=0,E>=1+A,B=D]). eq(f8(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),0,[],[I=1]). eq(f8(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=0,B>=D+1,E>=1+A]). eq(f8(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=0,D>=1+B,E>=1+A]). eq(f19(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=0,E>=1+A]). eq(f27(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=0,E>=1+A]). eq(f36(A,B,C,D,E,F,G,H,I,A,B+1,C,D,E,F,G,H),1,[],[I=0,D>=1+A]). eq(f43(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=0,E>=1+A]). eq(f49(A,B,C,D,E,F,G,H,I,A,B,C,D+1,E,F,G,H),1,[],[I=0,E>=1+A]).