
/*
applyBC(I,VBLL,R):-
        subst_VBL_(XScopeSet,II,[I],R),!.

% get a set of vars/bindings for this clause
getClVars([],_,[]):-!.
getClVars([[_X,T]|C],VBL,[[V,LL]|R]):-
        newVarTerm(T,C,VBL,V,L),
        checkVBLNil(L,LL),!,
	getClVars(C,VBL,R),!.
getClVars([[_X,_Y]|C],VBL,R):-
	getClVars(C,VBL,R),!.

checkVBLNil([],[I]):-!,next_var(I).
checkVBLNil(I,I):-!.

newVarTerm(v(V),CL,_VBL,_V,_L):-
    member([_,v(V)],CL),!,fail.
newVarTerm(v(V),CL,_VBL,_V,_L):-
    member([_,f(_,v(V))],CL),!,fail.

newVarTerm(f(_,v(V)),CL,_VBL,_V,_L):-
    member([_,v(V)],CL),!,fail.
newVarTerm(f(_,v(V)),CL,_VBL,_V,_L):-
    member([_,f(_,v(V))],CL),!,fail.

newVarTerm(v(V),_CL,VBL,v(V),L):-
    member([v(V),L],VBL),!.
newVarTerm(v(V),_CL,_VBL,v(V),[]):-!.
newVarTerm(f(_,v(V)),_CL,VBL,v(V),L):-
    member([v(V),L],VBL),!.
newVarTerm(f(_,v(V)),_CL,_VBL,v(V),[]):-!.


checkScope([],_,_,[]):-!.
checkScope([[v(_),L]|VL],Scope,VBL,XScope):-
    unscoped(L,Scope,USV),!,
    addUnscoped(USV,VBL,XScope1),!,
    append(Scope,XScope1,NScope),!,
    checkScope(VL,NScope,VBL,XScope2),!,
    append(XScope1,XScope2,XScope),!.

unscoped([],_,[]):-!.
unscoped([f(_,v(V))|J],S,[v(V)|R]):-
    not(member([v(V),_],S)),!,
    unscoped(J,[v(V)|S],R),!.
unscoped([_|J],S,R):-
    unscoped(J,S,R),!.

addUnscoped([],_,[]):-!.
addUnscoped([V|USV],VBL,[[V,L]|VBLR]):-
    member([V,L],VBL),!,
    addUnscoped(USV,VBL,VBLR).

% substitute into substitution list, then into clauses
subst_VBL_([],SL,CLL,R):-subst(SL,CLL,R),!.

subst_VBL_(VSL,SL,CLL,R):-
    subst_VBL(VSL,[SL],SLL),!,
    rep_subst(SLL,CLL,R),!.

subst_VBL([],R,R):-!.
subst_VBL([[v(V),L]|VSL],SLL,R):-
    rep_sub_VBL(L,v(V),SLL,R1),!,
    subst_VBL(VSL,R1,R),!.

rep_sub_VBL([],_,_,[]):-!.
rep_sub_VBL([I|J],v(V),SLL,R):-!,
    subVBL(I,v(V),SLL,SL0),
    rep_sub_VBL(J,v(V),SLL,SL1),!,
    append(SL0,SL1,R),!.

subVBL(_,_,[],[]):-!.
subVBL(I,V,[CL|L],[CR|R]):-!,
    sub_VBL(I,V,CL,CR),!,
    subVBL(I,V,L,R),!.

sub_VBL(_,_,[],[]):-!.
sub_VBL(I,V,[[W,WBL]|L],[[W,WBLL]|R]):-!,
    sub_bl(I,V,WBL,WBLL),!,
    sub_VBL(I,V,L,R).
sub_VBL(I,V,[T|L],[T|R]):-!,
    sub_VBL(I,V,L,R).

sub_bl(_,_,[],[]):-!.
sub_bl(I,V,[f(X,V)|L],[f(X,I)|R]):-!,
    sub_bl(I,V,L,R),!.
sub_bl(I,V,[f(X,Y)|L],[f(X,Y)|R]):-!,
    sub_bl(I,V,L,R),!.
sub_bl(I,V,[X|L],[X|R]):-!,
    sub_bl(I,V,L,R),!.

rep_subst([],_,[]):-!.
rep_subst([SL|SLL],CLL,R):-!,
    subst(SL,CLL,R0),!,
    rep_subst(SLL,CLL,R1),!,
    append(R0,R1,R),!.



% substitute a var/[] into clause(s)

subst([],R,R):-!.
subst([[v(V),L]|SL],CLL,R):-
    rep_sub(L,v(V),CLL,R1),!,
    subst(SL,R1,R),!.

rep_sub([],_,_,[]):-!.
rep_sub([I|J],V,CLL,R):-
    subCLL(I,V,CLL,R0),!,
    rep_sub(J,V,CLL,R1),!,
    append(R0,R1,R),!.

subCLL(_,_,[],[]):-!.
subCLL(I,V,[CL|L],[CR|R]):-!,
    sub(I,V,CL,CR),!,
    subCLL(I,V,L,R),!.
sub(_,_,[],[]):-!.
sub(I,V,[[P,V]|L],[[P,I]|R]):-!,
    sub(I,V,L,R).
sub(I,V,[[P,f(V,X)]|L],[[P,f(I,X)]|R]):-!,
    sub(I,V,L,R).
sub(I,V,[[P,f(X,V)]|L],[[P,f(X,I)]|R]):-!,
    sub(I,V,L,R).
sub(I,V,[[P,X]|L],[[P,X]|R]):-!,
    sub(I,V,L,R).
*/
