eq(f2(A,B,C,D,E),1,[f1(A,F,C,D,E)],[1>=A]).
eq(f2(A,B,C,D,E),1,[f300(A,B,C,D,E,F,G,H,I,J,K),loop_cont_f300(G,H,I,J,K)],[F=0,A>=2,C>=2]).
eq(f2(A,B,C,D,E),1,[f300(A,B,C,D,E,F,G,H,I,J,K)],[F=1,A>=2,C>=2]).
eq(f300(A,B,C,D,E,F,G,H,I,J,K),1,[f300(A,B,C,1+D,1+E,F,G,H,I,J,K)],[E>=0,0>=2+D]).
eq(f300(A,B,C,D,E,F,G,H,I,J,K),1,[f300(A,B,C,1+D,1+E,F,G,H,I,J,K)],[0>=2+E,0>=2+D]).
eq(f300(A,B,C,D,E,F,A,G,C,D,E),1,[],[F=1,D+1>=0]).