eq(f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f1(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)],[A=1]).
eq(f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f13(A,1,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),loop_cont_f13(T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[S=0,0>=A]).
eq(f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f13(A,1,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)],[S=1,0>=A]).
eq(f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f13(A,1,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),loop_cont_f13(T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[S=0,A>=2]).
eq(f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f13(A,1,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)],[S=1,A>=2]).
eq(f13(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),1,[f20(A,B,B+1,L1,M1,1,G,H,I,J,K,L,M,N,O,P,Q,R,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2),loop_cont_f20(O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[N1=0,A>=B]).
eq(f13(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),1,[f20(A,B,B+1,L1,M1,1,G,H,I,J,K,L,M,N,O,P,Q,R,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2)],[S=1,N1=1,A>=B]).
eq(f20(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),1,[f20(A,B,C,L1,M1,F+1,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)],[B>=F]).
eq(f31(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),1,[f31(A,B,C,D,E,F+1,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)],[B>=F]).
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,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1),1,[f45(A,B,C,D,E,F+1,L1,M1,N1,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)],[B>=F]).
eq(f60(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),1,[f60(A,B,C,D,E,F+1,G,H,I,J,K-1,L1,M1,N1,O1,K,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[J>=F]).
eq(loop_cont_f20(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),0,[f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2),loop_cont_f31(M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[L1=0]).
eq(loop_cont_f31(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),0,[f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2),loop_cont_f45(M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[L1=0]).
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,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1),0,[f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2),loop_cont_f60(M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[L1=0]).
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,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1),0,[f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2)],[S=1,L1=1]).
eq(loop_cont_f60(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),0,[f13(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)],[]).
eq(f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[],[S=1,F>=1+B,A=C]).
eq(f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[],[S=1,B>=1+A]).
eq(f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R),1,[],[S=0,0>=E+1,F>=1+B]).
eq(f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),0,[],[S=1]).
eq(f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R),1,[],[S=0,E>=1,F>=1+B]).
eq(f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R),1,[],[S=0,F>=1+B,E=0]).
eq(f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,1,T,U,V,J,K,L,M,N,O,P,Q,R),1,[],[S=0,A>=C+1,F>=1+B]).
eq(f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),0,[],[S=1]).
eq(f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,1,T,U,V,J,K,L,M,N,O,P,Q,R),1,[],[S=0,C>=1+A,F>=1+B]).
eq(f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B,C,D,E,1,G,H,I,T,B,L,M,N,O,P,U,V),1,[],[S=0,F>=1+B]).
eq(f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,A,B+1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[],[S=0,F>=1+J]).