eq(f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O),1,[f18(A,H,C,D,E,F,P,H,2,Q,Q,Q,Q,3,0)],[A>=H+1,F>=0]). eq(f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O),1,[f18(A,H,C,D,E,F,P,H,2,Q,Q,Q,Q,3,0)],[H>=A+1,F>=0]). eq(f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O),1,[f17(A,P,C,1,Q,F,G,H,I,J,K,L,M,N,O,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),loop_cont_f17(S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[R=0,F>=0,A>=B+1]). eq(f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O),1,[f17(A,P,C,1,Q,F,G,H,I,J,K,L,M,N,O,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[R=1,F>=0,A>=B+1]). eq(f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O),1,[f17(A,P,C,1,Q,F,G,H,I,J,K,L,M,N,O,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),loop_cont_f17(S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[R=0,F>=0,B>=A+1]). eq(f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O),1,[f17(A,P,C,1,Q,F,G,H,I,J,K,L,M,N,O,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[R=1,F>=0,B>=A+1]). eq(f17(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),1,[f17(A,F1,C,1+D,G1,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)],[A>=B+1,C>=0,D>=0]). eq(f17(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),1,[f17(A,F1,C,1+D,G1,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)],[B>=A+1,C>=0,D>=0]). eq(f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,B,B,C,D,E,F,Q,H,I,J,K,L,M,N,O),1,[],[P=1,C>=0,D>=0,B=A]).