%%% -*- prolog -*-

mem(X, [X|_]).			% R1
mem(X, [_|Xs]) :- mem(X, Xs).	% R2

%%% WANT TO PROVE:
%%%   mem(b, [a,b,c])
%%%     fails to unify: X1=b & X1=a           [R1]
%%%     mem(b, [b,c])  X2=b, _2=a, Xs2=[b,c]  [R2]
%%%       true X3=b, X3=b, _3=[c]             [R1]   <- solution
%%%       mem(b, [c])   X4=b, _4=b, Xs4=[c]   [R2]
%%%         fails to unify: X5=b, X5=c, _5=[] [R1]
%%%         mem(b, [])  X6=b, _6=c, Xs6=[]    [R2]
%%%           fails to unify   [R1]
%%%           fails to unify   [R2]

c(X) :- a(X), b(X).		% R1
a(1).				% a1
a(2).				% a2
a(3).				% a3
b(1).				% b1
b(2).				% b2
b(3).				% b3

%%% TO PROVE:
%%%   c(X)
%%%     a(X), b(X) X1=X         [R1]
%%%     ^
%%%       true X=1 [a1]
%%%           ^
%%%           true [b1]   <- success
%%%           fails to unify: 1 w/ 2 [b2]
%%%           fails to unify: 1 w/ 3 [b3]
%%%       true X=2 [a2]
%%%           fails to unify: 2 w/ 1 [b1]
%%%           true [b2]   <- success
%%%           fails to unify: 2 w/ 3 [b3]
%%%   ...
