eq(f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f1(S,T,U,V,W,F,G,H,I,J,K,L,M,N,O,P,Q,R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1),loop_cont_f1(Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1)],[X=0]).
eq(f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R),1,[f1(S,T,U,V,W,F,G,H,I,J,K,L,M,N,O,P,Q,R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1)],[X=1]).
eq(f1(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,[f1(A,B,C,D,E,F,G,256,L1,M1,N1,O1,P1,Q1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[G>=1+F,R1>=1,H=256]).
eq(f1(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,[f1(A,B,C,D,E,F,G,H,L1,M1,N1,O1,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1)],[G>=1+F,0>=H]).
eq(f1(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,T,U,K,L,M,N,0,0,0,R),1,[],[S=1,F>=G]).
eq(f1(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,T,U,V,W,X,Y,H,H,H,Z),1,[],[S=1,H>=1,G>=1+F,H>=257]).
eq(f1(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,T,U,V,W,X,Y,H,H,H,Z),1,[],[S=1,H>=1,G>=1+F,255>=H]).