:- module( _, [search/2], [assertions , regtypes , basicmodes , nativeprops] ).

search([[ref(loc(1)),num(int(A))],[array(1,[num(int(B))|_1])]],[num(int(1))]) :-
        A=<B,
        A\=B,
        A>B .
search([[ref(loc(1)),num(int(A))],[array(B,[num(int(D))|C])]],[E]) :-
        B\=0,
        F is B-1,
        0=<F,
        F<B,
        G is F+1,
        mynth(G,[num(int(D))|C],num(int(H))),
        A=<H,
        I is B-1,
        0=<I,
        I<B,
        J is I+1,
        mynth(J,[num(int(D))|C],num(int(K))),
        A\=K,
        0<B,
        A>D,
        1\=B,
        L is 0+B,
        M is L//2,
        0=<M,
        M<B,
        N is M+1,
        mynth(N,[num(int(D))|C],num(int(O))),
        A=<O,
        execute_notrace_1(B,C,D,A,M,_1,_2,_3,_4,_5,E,_6) .
search([[ref(loc(1)),num(int(A))],[array(B,[num(int(D))|C])]],[E]) :-
        B\=0,
        F is B-1,
        0=<F,
        F<B,
        G is F+1,
        mynth(G,[num(int(D))|C],num(int(H))),
        A=<H,
        I is B-1,
        0=<I,
        I<B,
        J is I+1,
        mynth(J,[num(int(D))|C],num(int(K))),
        A\=K,
        0<B,
        A>D,
        1\=B,
        L is 0+B,
        M is L//2,
        0=<M,
        M<B,
        N is M+1,
        mynth(N,[num(int(D))|C],num(int(O))),
        A>O,
        execute_notrace_2(B,C,D,A,M,B,M,_1,_2,_3,_4,_5,E,_6) .
search([[ref(loc(1)),num(int(A))],[array(B,[num(int(D))|C])]],[refE(loc(2))]) :-
        B\=0,
        E is B-1,
        0=<E,
        E<B,
        F is E+1,
        mynth(F,[num(int(D))|C],num(int(G))),
        A=<G,
        H is B-1,
        0=<H,
        H<B,
        I is H+1,
        mynth(I,[num(int(D))|C],num(int(J))),
        A\=J,
        0<B,
        A>D,
        1\=B,
        K is 0+B,
        L is K//2,
        L<0 .
search([[ref(loc(1)),num(int(A))],[array(B,[num(int(D))|C])]],[refE(loc(2))]) :-
        B\=0,
        E is B-1,
        0=<E,
        E<B,
        F is E+1,
        mynth(F,[num(int(D))|C],num(int(G))),
        A=<G,
        H is B-1,
        0=<H,
        H<B,
        I is H+1,
        mynth(I,[num(int(D))|C],num(int(J))),
        A\=J,
        0<B,
        A>D,
        1\=B,
        K is 0+B,
        L is K//2,
        L>=B .
search([[ref(loc(1)),num(int(A))],[array(B,[num(int(D))|C])]],[num(int(0))]) :-
        B\=0,
        E is B-1,
        0=<E,
        E<B,
        F is E+1,
        mynth(F,[num(int(D))|C],num(int(G))),
        A=<G,
        H is B-1,
        0=<H,
        H<B,
        I is H+1,
        mynth(I,[num(int(D))|C],num(int(J))),
        A\=J,
        0<B,
        A=<D .
search([[ref(loc(1)),num(int(A))],[array(B,C)]],[refE(loc(2))]) :-
        B\=0,
        D is B-1,
        0=<D,
        D<B,
        E is D+1,
        mynth(E,C,num(int(F))),
        A=<F,
        G is B-1,
        0=<G,
        G<B,
        H is G+1,
        mynth(H,C,num(int(I))),
        A\=I,
        0>=B .
search([[ref(loc(1)),num(int(A))],[array(B,C)]],[num(int(D))]) :-
        B\=0,
        E is B-1,
        0=<E,
        E<B,
        F is E+1,
        mynth(F,C,num(int(G))),
        A=<G,
        H is B-1,
        0=<H,
        H<B,
        I is H+1,
        mynth(I,C,num(int(A))),
        D is B-1 .
search([[ref(loc(1)),num(int(A))],[array(B,C)]],[refE(loc(2))]) :-
        B\=0,
        D is B-1,
        0=<D,
        D<B,
        E is D+1,
        mynth(E,C,num(int(F))),
        A=<F,
        G is B-1,
        G<0 .
search([[ref(loc(1)),num(int(A))],[array(B,C)]],[refE(loc(2))]) :-
        B\=0,
        D is B-1,
        0=<D,
        D<B,
        E is D+1,
        mynth(E,C,num(int(F))),
        A=<F,
        G is B-1,
        G>=B .
search([[ref(loc(1)),num(int(A))],[array(B,C)]],[num(int(B))]) :-
        B\=0,
        D is B-1,
        0=<D,
        D<B,
        E is D+1,
        mynth(E,C,num(int(F))),
        A>F .
search([[ref(loc(1)),num(int(_1))],[array(A,_2)]],[refE(loc(2))]) :-
        A\=0,
        B is A-1,
        B<0 .
search([[ref(loc(1)),num(int(_1))],[array(A,_2)]],[refE(loc(2))]) :-
        A\=0,
        B is A-1,
        B>=A .
search([[ref(loc(1)),num(int(_1))],[array(0,_2)]],[num(int(0))]).
search([[null,num(int(_1))],[]],[refE(loc(1))]).

execute_notrace_1(A,B,C,_1,1,[array(A,[num(int(C))|B])],_2,_3,_4,_5,num(int(1)),[]).
execute_notrace_1(A,B,C,D,E,F,G,H,I,J,K,L) :-
        1\=E,
        M is 0+E,
        N is M//2,
        0=<N,
        N<A,
        O is N+1,
        mynth(O,[num(int(C))|B],num(int(P))),
        D=<P,
        execute_notrace_1(A,B,C,D,N,F,G,H,I,J,K,L) .
execute_notrace_1(A,B,C,D,E,F,G,H,I,J,K,L) :-
        1\=E,
        M is 0+E,
        N is M//2,
        0=<N,
        N<A,
        O is N+1,
        mynth(O,[num(int(C))|B],num(int(P))),
        D>P,
        execute_notrace_2(A,B,C,D,N,E,N,F,G,H,I,J,K,L) .
execute_notrace_1(A,B,C,_1,D,[array(A,[num(int(C))|B]),[]],_2,_3,_4,_5,refE(loc(2)),[]) :-
        1\=D,
        E is 0+D,
        F is E//2,
        F<0 .
execute_notrace_1(A,B,C,_1,D,[array(A,[num(int(C))|B]),[]],_2,_3,_4,_5,refE(loc(2)),[]) :-
        1\=D,
        E is 0+D,
        F is E//2,
        F>=A .

execute_notrace_2(A,B,C,_1,_2,D,E,[array(A,[num(int(C))|B])],_3,_4,_5,_6,num(int(D)),[]) :-
        D is E+1 .
execute_notrace_2(A,B,C,D,_1,E,F,G,H,I,J,K,L,M) :-
        N is F+1,
        N\=E,
        O is F+E,
        P is O//2,
        0=<P,
        P<A,
        Q is P+1,
        mynth(Q,[num(int(C))|B],num(int(R))),
        D=<R,
        execute_notrace_2(A,B,C,D,P,P,F,G,H,I,J,K,L,M) .
execute_notrace_2(A,B,C,D,_1,E,F,G,H,I,J,K,L,M) :-
        N is F+1,
        N\=E,
        O is F+E,
        P is O//2,
        0=<P,
        P<A,
        Q is P+1,
        mynth(Q,[num(int(C))|B],num(int(R))),
        D>R,
        execute_notrace_2(A,B,C,D,P,E,P,G,H,I,J,K,L,M) .
execute_notrace_2(A,B,C,_1,_2,D,E,[array(A,[num(int(C))|B]),[]],_3,_4,_5,_6,refE(loc(2)),[]) :-
        F is E+1,
        F\=D,
        G is E+D,
        H is G//2,
        H<0 .
execute_notrace_2(A,B,C,_1,_2,D,E,[array(A,[num(int(C))|B]),[]],_3,_4,_5,_6,refE(loc(2)),[]) :-
        F is E+1,
        F\=D,
        G is E+D,
        H is G//2,
        H>=A .


