eq(f0(A,B),1,[f2(C,D,E,F,G),loop_cont_f2(F,G)],[E=0,C>=1,C>=5,C>=2,C>=3]).
eq(f0(A,B),1,[f2(C,D,E,F,G)],[E=1,C>=1,C>=5,C>=2,C>=3]).
eq(f0(A,B),1,[f2(1,C,D,E,F),loop_cont_f2(E,F)],[D=0,0>=4,0>=1]).
eq(f0(A,B),1,[f2(1,C,D,E,F)],[D=1,0>=4,0>=1]).
eq(f0(A,B),1,[f2(C,D,E,F,G),loop_cont_f2(F,G)],[E=0,C>=1,C>=5,0>=C,C>=3]).
eq(f0(A,B),1,[f2(C,D,E,F,G)],[E=1,C>=1,C>=5,0>=C,C>=3]).
eq(f0(A,B),1,[f2(3,C,D,E,F),loop_cont_f2(E,F)],[D=0]).
eq(f0(A,B),1,[f2(3,C,D,E,F)],[D=1]).
eq(f0(A,B),1,[f2(1,C,D,E,F),loop_cont_f2(E,F)],[D=0,0>=1]).
eq(f0(A,B),1,[f2(1,C,D,E,F)],[D=1,0>=1]).
eq(f0(A,B),1,[f2(3,C,D,E,F),loop_cont_f2(E,F)],[D=0,0>=3]).
eq(f0(A,B),1,[f2(3,C,D,E,F)],[D=1,0>=3]).
eq(f2(A,B,C,D,E),1,[f2(B,F,C,D,E)],[B>=5,B>=2,B>=3,A=2*B]).
eq(f2(A,B,C,D,E),1,[f2(B,F,C,D,E)],[B>=5,B>=2,1>=B,A=2*B]).
eq(f2(A,B,C,D,E),1,[f2(B,F,C,D,E)],[B>=5,0>=B,B>=3,A=2*B]).
eq(f2(A,B,C,D,E),1,[f2(B,F,C,D,E)],[B>=5,0>=B,1>=B,A=2*B]).
eq(f2(A,B,C,D,E),1,[f2(B,F,C,D,E)],[B=3,A=6]).
eq(f2(A,B,C,D,E),1,[f2(B,F,C,D,E)],[3>=B,B>=2,1>=B,A=2*B]).
eq(f2(A,B,C,D,E),1,[f2(B,F,C,D,E)],[0>=3,B=3,A=6]).
eq(f2(A,B,C,D,E),1,[f2(B,F,C,D,E)],[3>=B,0>=B,1>=B,A=2*B]).
eq(f2(A,B,C,D,E),1,[f2(6*B+4,F,C,D,E)],[6*B>=1,6*B+2>=0,6*B+1>=0,A=2*B+1]).
eq(f2(A,B,C,D,E),1,[f2(6*B+4,F,C,D,E)],[6*B>=1,6*B+2>=0,0>=3+6*B,A=2*B+1]).
eq(f2(A,B,C,D,E),1,[f2(6*B+4,F,C,D,E)],[6*B>=1,0>=4+6*B,6*B+1>=0,A=2*B+1]).
eq(f2(A,B,C,D,E),1,[f2(6*B+4,F,C,D,E)],[6*B>=1,0>=4+6*B,0>=3+6*B,A=2*B+1]).
eq(f2(A,B,C,D,E),1,[f2(6*B+4,F,C,D,E)],[0>=6*B+1,6*B+2>=0,6*B+1>=0,A=2*B+1]).
eq(f2(A,B,C,D,E),1,[f2(6*B+4,F,C,D,E)],[0>=6*B+1,6*B+2>=0,0>=3+6*B,A=2*B+1]).
eq(f2(A,B,C,D,E),1,[f2(6*B+4,F,C,D,E)],[0>=6*B+1,0>=4+6*B,6*B+1>=0,A=2*B+1]).
eq(f2(A,B,C,D,E),1,[f2(6*B+4,F,C,D,E)],[0>=6*B+1,0>=4+6*B,0>=3+6*B,A=2*B+1]).
eq(f2(A,B,C,A,B),0,[],[C=1]).