Prepared by:    Roni Khardon
Date:           Nov 25 1999.
Questions to:   roni@cs.tufts.edu


This file includes an example run of the learning algorithm A2
(see "Learning Function Free Horn Expressions" on my publications list)
when learning the following Prolog Program from interpretations.
It was extracted from a run of a system currently under development.

list(X) :- null(X).
list(X) :- cons(X, Head, Tail), list(Tail).

member(I, X) :- cons(X, I, Tail).
member(I, X) :- cons(X, Head, Tail), member(I, Tail).

append(X, L, L) :- null(X), list(L).
append(L1, L2, L3) :- cons(L1, X, T1), cons(L3, X, T3), append(T1, L2, T3).

--------------------------------------------------------------------------

The algorithm learns by asking two types of questions to a user.  The
extract below includes the questions and answers produced in this
process. It is described in a shorthand notation that requires a bit
of explanation:

EQ means an equivalence query for the hypothesis printed.
The learner presents the hypothesis and asks whether this is 
the correct expression/program.  

NCEX and PCEX are the answer. They provide negative or positive
counter examples: examples showing that the hypothesis is not correct.
PCEX is true for the target expression (a model) 
     but false for the hypothesis.
NCEX is false for the target expression (not a model) 
     but true for the hypothesis.

MQ means a membership query for the example printed.
(is this example a model of the target expression?) 
The answer (true or false) is printed after it.

The system uses caching to avoid repeating the same questions
Cache Hit means that a MQ was saved as the information was already available.

To illustrate the notation assume we have a predicate p() of arity 2
and a predicate q() of arity 1.

Clauses are represented as 2-tuple ground terms.
The following is a representation of 3 *clause sets*
[ c([p(1,2),p(2,3)],[p(1,3)]), 
  c([p(1,2)],[p(1,1),p(2,1)]),
  c([p(1,2),q(1)],[q(2)]) ]

The first clause set corresponds to
  [ p(X,Y) p(Y,Z) --> p(X,Z) ]
The second to 
  [ p(X,Y) --> p(X,X)] and [ p(X,Y) --> p(Y,X)]
The third to
  [ p(X,Y) q(X) --> q(Y) ]

So that the first list represents the antecedent and the second one is
a list of consequents each belonging to a different clause.  
The hypotheses of the algorithm are presented in this way below.

An example includes an interpretation and a label (true or false)
as in:
example(i([1,2],[[p(1,1),p(1,2),p(2,1),p(2,2)],[q(1)]]),false).

An interpretation is a 2-tuple. The first argument is a list of domain
elements. (The names are not important. You will see below complex
names like x-h etc., these are just names for domain elements.  They
are created because of the use of Products.)

The second argument describes the extension of predicates.  Atoms not
listed are false in the interpretation.  Note that the second argument
is a list of lists - it is ordered in the same order as the
signature. In our example p() is before q(). Together with the
arities we denote it as [p-2,q-1].

---------------------------------------------------------------------

The actual run restricted the consequents (heads) of clauses to be in the
following list:
:- restrictedcons([list, member, append]).

and used the signature:

:- a2([null-1, cons-3, list-1, member-2, append-3]).

The questions and answers are recorded in the run.  I have also
annotated the run with explanations on the "phases" in the
algorithm. In each phase the algorithm asks an equivalence query.  On
a positive counter example it "cleans" the hypothesis by removing some
clauses (in fact only some consequents of any clause set).  On a
negative counter example, the algorithm first tries to "minimise" it
by dropping parts of it. The algorithm then tries to refine one of the
clause sets, and if this succeeds it replaces this clause set with a
new one. If no clause set was refined then a new clause set is added
to the hypothesis.  This should hopefully help see the logical
structure by which the algorithm progresses.  One can also see obvious
places for improvements.

----------------------------------------------------------------------


EQ []

NCEX i([x],[[null(x)],[],[],[],[]])

Adding a new clause set

EQ [c([null(x)],[list(x),member(x,x),append(x,x,x)])]

PCEX i([x],[[null(x)],[],[list(x)],[],[append(x,x,x)]])

EQ [c([null(x)],[list(x),append(x,x,x)])]

NCEX i([x,h,t],[[],[cons(x,t,h)],[list(h)],[],[]])

Trying to minimise counter example

MQ i([h,t],[[],[],[list(h)],[],[]]) true

MQ i([x,h],[[],[],[list(h)],[],[]]) true

Trying to replace first clause set (fails)

MQ i([x-x,x-h,x-t],[[],[],[],[],[]]) true

Adding a new clause set

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h),list(h)],
      [list(x),list(t),member(x,x),member(x,h),member(x,t),member(h,x),
       member(h,h),member(h,t),member(t,x),member(t,h),member(t,t),
       append(x,x,x),append(x,x,h),append(x,x,t),append(x,h,x),append(x,h,h),
       append(x,h,t),append(x,t,x),append(x,t,h),append(x,t,t),append(h,x,x),
       append(h,x,h),append(h,x,t),append(h,h,x),append(h,h,h),append(h,h,t),
       append(h,t,x),append(h,t,h),append(h,t,t),append(t,x,x),append(t,x,h),
       append(t,x,t),append(t,h,x),append(t,h,h),append(t,h,t),append(t,t,x),
       append(t,t,h),append(t,t,t)])]

PCEX i([t,h,x],[[],[cons(x,t,h)],[list(h),list(x)],[member(t,x)],[]])

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h),list(h)],[list(x),member(t,x)])]

NCEX i([i,x,h],[[],[cons(x,i,h)],[],[],[]])


Trying to replace first clause set (fails)

MQ i([x-i,x-x,x-h],[[],[],[],[],[]]) true

Trying to replace second clause set (succeeds)

MQ i([x-i,x-x,x-h,h-i,h-x,h-h,t-i,t-x,t-h],
     [[],[cons(x-x,t-i,h-h)],[],[],[]]) false

MQ i([x,h,t],[[],[cons(x,t,h)],[],[],[]]) false

Replacing...

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[list(x),member(t,x),list(h)])]

PCEX i([h,t,x],[[],[cons(x,t,h)],[],[member(t,x)],[]])

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)])]

NCEX i([x,h,t],[[],[cons(x,t,h)],[list(h)],[member(t,x)],[]])

Trying to minimise counter example

Cache Hit i([h,t],[[],[],[list(h)],[],[]]) true

MQ i([x,t],[[],[],[],[member(t,x)],[]]) true

Cache Hit i([x,h],[[],[],[list(h)],[],[]]) true

Trying to replace first clause set (fails)

Cache Hit i([x-x,x-h,x-t],[[],[],[],[],[]]) true

Trying to replace second clause set (fails)

MQ i([x-x,x-h,x-t,h-x,h-h,h-t,t-x,t-h,t-t],
     [[],[cons(x-x,t-t,h-h)],[],[],[]]) false

Adding a new clause set

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)]),
    c([cons(x,t,h),list(h),member(t,x)],
      [list(x),list(t),member(x,x),member(x,h),member(x,t),member(h,x),
       member(h,h),member(h,t),member(t,h),member(t,t),append(x,x,x),
       append(x,x,h),append(x,x,t),append(x,h,x),append(x,h,h),append(x,h,t),
       append(x,t,x),append(x,t,h),append(x,t,t),append(h,x,x),append(h,x,h),
       append(h,x,t),append(h,h,x),append(h,h,h),append(h,h,t),append(h,t,x),
       append(h,t,h),append(h,t,t),append(t,x,x),append(t,x,h),append(t,x,t),
       append(t,h,x),append(t,h,h),append(t,h,t),append(t,t,x),append(t,t,h),
       append(t,t,t)])]

PCEX i([t,h,x],[[],[cons(x,t,h)],[list(h),list(x)],[member(t,x)],[]])

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)]),
    c([cons(x,t,h),list(h),member(t,x)],[list(x)])]

NCEX i([i,x,h,t],[[],[cons(x,t,h)],[],[member(i,h),member(t,x)],[]])

Trying to minimise counter example

Cache Hit i([x,h,t],[[],[cons(x,t,h)],[],[member(t,x)],[]]) true

MQ i([i,h,t],[[],[],[],[member(i,h)],[]]) true

MQ i([i,x,t],[[],[],[],[member(t,x)],[]]) true

MQ i([i,x,h],[[],[],[],[member(i,h)],[]]) true

Trying to replace first clause set (fails)

MQ i([x-i,x-x,x-h,x-t],[[],[],[],[],[]]) true

Trying to replace second clause set (fails)

MQ i([x-i,x-x,x-h,x-t,h-i,h-x,h-h,h-t,t-i,t-x,t-h,t-t],
     [[],[cons(x-x,t-t,h-h)],[],[],[]]) false

Trying to replace third clause set (fails)

MQ i([x-i,x-x,x-h,x-t,h-i,h-x,h-h,h-t,t-i,t-x,t-h,t-t],
     [[],[cons(x-x,t-t,h-h)],[],[member(t-i,x-h),member(t-t,x-x)],[]]) true

Adding a new clause set

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)]),
    c([cons(x,t,h),list(h),member(t,x)],[list(x)]),
    c([cons(x,t,h),member(i,h),member(t,x)],
      [list(i),list(x),list(h),list(t),member(i,i),member(i,x),member(i,t),
       member(x,i),member(x,x),member(x,h),member(x,t),member(h,i),
       member(h,x),member(h,h),member(h,t),member(t,i),member(t,h),
       member(t,t),append(i,i,i),append(i,i,x),append(i,i,h),append(i,i,t),
       append(i,x,i),append(i,x,x),append(i,x,h),append(i,x,t),append(i,h,i),
       append(i,h,x),append(i,h,h),append(i,h,t),append(i,t,i),append(i,t,x),
       append(i,t,h),append(i,t,t),append(x,i,i),append(x,i,x),append(x,i,h),
       append(x,i,t),append(x,x,i),append(x,x,x),append(x,x,h),append(x,x,t),
       append(x,h,i),append(x,h,x),append(x,h,h),append(x,h,t),append(x,t,i),
       append(x,t,x),append(x,t,h),append(x,t,t),append(h,i,i),append(h,i,x),
       append(h,i,h),append(h,i,t),append(h,x,i),append(h,x,x),append(h,x,h),
       append(h,x,t),append(h,h,i),append(h,h,x),append(h,h,h),append(h,h,t),
       append(h,t,i),append(h,t,x),append(h,t,h),append(h,t,t),append(t,i,i),
       append(t,i,x),append(t,i,h),append(t,i,t),append(t,x,i),append(t,x,x),
       append(t,x,h),append(t,x,t),append(t,h,i),append(t,h,x),append(t,h,h),
       append(t,h,t),append(t,t,i),append(t,t,x),append(t,t,h),append(t,t,t)])]

PCEX i([t,h,x,i],
       [[],[cons(x,t,h)],[],[member(t,x),member(i,h),member(i,x)],[]])

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)]),
    c([cons(x,t,h),list(h),member(t,x)],[list(x)]),
    c([cons(x,t,h),member(i,h),member(t,x)],[member(i,x)])]

NCEX i([x,l],[[null(x)],[],[list(l),list(x)],[],[append(x,x,x)]])

Trying to minimise counter example

MQ i([l],[[],[],[list(l)],[],[]]) true
Cache Hit i([x],[[null(x)],[],[list(x)],[],[append(x,x,x)]]) true

Trying to replace first clause set (fails)

MQ i([x-x,x-l],[[null(x-x)],[],[],[],[]]) false

Trying to replace second clause set (fails)

MQ i([x-x,x-l,h-x,h-l,t-x,t-l],[[],[],[],[],[]]) true

Trying to replace third clause set (fails)

MQ i([x-x,x-l,h-x,h-l,t-x,t-l],[[],[],[list(h-l),list(h-x)],[],[]]) true

Trying to replace fourth clause set (fails)

MQ i([i-x,i-l,x-x,x-l,h-x,h-l,t-x,t-l],[[],[],[],[],[]]) true


Adding a new clause set

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)]),
    c([cons(x,t,h),list(h),member(t,x)],[list(x)]),
    c([cons(x,t,h),member(i,h),member(t,x)],[member(i,x)]),
    c([null(x),list(l),list(x),append(x,x,x)],
      [member(x,x),member(x,l),member(l,x),member(l,l),append(x,x,l),
       append(x,l,x),append(x,l,l),append(l,x,x),append(l,x,l),append(l,l,x),
       append(l,l,l)])]

PCEX i([l,x],[[null(x)],[],[list(x),list(l)],[],[append(x,x,x),append(x,l,l)]])

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)]),
    c([cons(x,t,h),list(h),member(t,x)],[list(x)]),
    c([cons(x,t,h),member(i,h),member(t,x)],[member(i,x)]),
    c([null(x),list(l),list(x),append(x,x,x)],[append(x,l,l)])]

NCEX i([l1,l2,l3,t1,t3,x],
       [[],[cons(l3,x,t3),cons(l1,x,t1)],[],
        [member(x,l1),member(x,l3)],[append(t1,l2,t3)]])

Trying to minimise counter example

MQ i([l2,l3,t1,t3,x],
     [[],[cons(l3,x,t3)],[],[member(x,l3)],[append(t1,l2,t3)]]) true

MQ i([l1,l3,t1,t3,x],
     [[],[cons(l3,x,t3),cons(l1,x,t1)],[],[member(x,l1),member(x,l3)],[]]) true

MQ i([l1,l2,t1,t3,x],
     [[],[cons(l1,x,t1)],[],[member(x,l1)],[append(t1,l2,t3)]]) true

MQ i([l1,l2,l3,t3,x],
     [[],[cons(l3,x,t3)],[],[member(x,l1),member(x,l3)],[]]) true

MQ i([l1,l2,l3,t1,x],
     [[],[cons(l1,x,t1)],[],[member(x,l1),member(x,l3)],[]]) true

MQ i([l1,l2,l3,t1,t3],[[],[],[],[],[append(t1,l2,t3)]]) true

Trying to replace first clause set (fails)

MQ i([x-l1,x-l2,x-l3,x-t1,x-t3,x-x],[[],[],[],[],[]]) true

Trying to replace second clause set (fails)

MQ i([x-l1,x-l2,x-l3,x-t1,x-t3,x-x,h-l1,h-l2,h-l3,h-t1,h-t3,h-x,t-l1,
      t-l2,t-l3,t-t1,t-t3,t-x],
     [[],[cons(x-l3,t-x,h-t3),cons(x-l1,t-x,h-t1)],[],[],[]]) false

Trying to replace third clause set (fails)

MQ i([x-l1,x-l2,x-l3,x-t1,x-t3,x-x,h-l1,h-l2,h-l3,h-t1,h-t3,h-x,t-l1,
      t-l2,t-l3,t-t1,t-t3,t-x],
     [[],[cons(x-l3,t-x,h-t3),cons(x-l1,t-x,h-t1)],[],
      [member(t-x,x-l1),member(t-x,x-l3)],[]]) true

Trying to replace fourth clause set (fails)

MQ i([i-l1,i-l2,i-l3,i-t1,i-t3,i-x,x-l1,x-l2,x-l3,x-t1,x-t3,x-x,h-l1,
      h-l2,h-l3,h-t1,h-t3,h-x,t-l1,t-l2,t-l3,t-t1,t-t3,t-x],
     [[],[cons(x-l3,t-x,h-t3),cons(x-l1,t-x,h-t1)],[],
      [member(i-x,h-l1),member(i-x,h-l3),member(t-x,x-l1),
       member(t-x,x-l3)],[]]) true

Trying to replace fifth clause set (fails)

MQ i([x-l1,x-l2,x-l3,x-t1,x-t3,x-x,l-l1,l-l2,l-l3,l-t1,l-t3,l-x],
     [[],[],[],[],[append(x-t1,x-l2,x-t3)]]) true


Adding a new clause set
EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)]),
    c([cons(x,t,h),list(h),member(t,x)],[list(x)]),
    c([cons(x,t,h),member(i,h),member(t,x)],[member(i,x)]),
    c([null(x),list(l),list(x),append(x,x,x)],[append(x,l,l)]),
    c([cons(l3,x,t3),cons(l1,x,t1),member(x,l1),member(x,l3),append(t1,l2,t3)],
      [list(l1),list(l2),list(l3),list(t1),list(t3),list(x),member(l1,l1),
       member(l1,l2),member(l1,l3),member(l1,t1),member(l1,t3),member(l1,x),
       member(l2,l1),member(l2,l2),member(l2,l3),member(l2,t1),member(l2,t3),
       member(l2,x),member(l3,l1),member(l3,l2),member(l3,l3),member(l3,t1),
       member(l3,t3),member(l3,x),member(t1,l1),member(t1,l2),member(t1,l3),
       member(t1,t1),member(t1,t3),member(t1,x),member(t3,l1),member(t3,l2),
       member(t3,l3),member(t3,t1),member(t3,t3),member(t3,x),member(x,l2),
       member(x,t1),member(x,t3),member(x,x),append(l1,l1,l1),append(l1,l1,l2),
       append(l1,l1,l3),append(l1,l1,t1),append(l1,l1,t3),append(l1,l1,x),
       append(l1,l2,l1),append(l1,l2,l2),append(l1,l2,l3),append(l1,l2,t1),
       append(l1,l2,t3),append(l1,l2,x),append(l1,l3,l1),append(l1,l3,l2),
       append(l1,l3,l3),append(l1,l3,t1),append(l1,l3,t3),append(l1,l3,x),
       append(l1,t1,l1),append(l1,t1,l2),append(l1,t1,l3),append(l1,t1,t1),
       append(l1,t1,t3),append(l1,t1,x),append(l1,t3,l1),append(l1,t3,l2),
       append(l1,t3,l3),append(l1,t3,t1),append(l1,t3,t3),append(l1,t3,x),
       append(l1,x,l1),append(l1,x,l2),append(l1,x,l3),append(l1,x,t1),
       append(l1,x,t3),append(l1,x,x),append(l2,l1,l1),append(l2,l1,l2),
       append(l2,l1,l3),append(l2,l1,t1),append(l2,l1,t3),append(l2,l1,x),
       append(l2,l2,l1),append(l2,l2,l2),append(l2,l2,l3),append(l2,l2,t1),
       append(l2,l2,t3),append(l2,l2,x),append(l2,l3,l1),append(l2,l3,l2),
       append(l2,l3,l3),append(l2,l3,t1),append(l2,l3,t3),append(l2,l3,x),
       append(l2,t1,l1),append(l2,t1,l2),append(l2,t1,l3),append(l2,t1,t1),
       append(l2,t1,t3),append(l2,t1,x),append(l2,t3,l1),append(l2,t3,l2),
       append(l2,t3,l3),append(l2,t3,t1),append(l2,t3,t3),append(l2,t3,x),
       append(l2,x,l1),append(l2,x,l2),append(l2,x,l3),append(l2,x,t1),
       append(l2,x,t3),append(l2,x,x),append(l3,l1,l1),append(l3,l1,l2),
       append(l3,l1,l3),append(l3,l1,t1),append(l3,l1,t3),append(l3,l1,x),
       append(l3,l2,l1),append(l3,l2,l2),append(l3,l2,l3),append(l3,l2,t1),
       append(l3,l2,t3),append(l3,l2,x),append(l3,l3,l1),append(l3,l3,l2),
       append(l3,l3,l3),append(l3,l3,t1),append(l3,l3,t3),append(l3,l3,x),
       append(l3,t1,l1),append(l3,t1,l2),append(l3,t1,l3),append(l3,t1,t1),
       append(l3,t1,t3),append(l3,t1,x),append(l3,t3,l1),append(l3,t3,l2),
       append(l3,t3,l3),append(l3,t3,t1),append(l3,t3,t3),append(l3,t3,x),
       append(l3,x,l1),append(l3,x,l2),append(l3,x,l3),append(l3,x,t1),
       append(l3,x,t3),append(l3,x,x),append(t1,l1,l1),append(t1,l1,l2),
       append(t1,l1,l3),append(t1,l1,t1),append(t1,l1,t3),append(t1,l1,x),
       append(t1,l2,l1),append(t1,l2,l2),append(t1,l2,l3),append(t1,l2,t1),
       append(t1,l2,x),append(t1,l3,l1),append(t1,l3,l2),append(t1,l3,l3),
       append(t1,l3,t1),append(t1,l3,t3),append(t1,l3,x),append(t1,t1,l1),
       append(t1,t1,l2),append(t1,t1,l3),append(t1,t1,t1),append(t1,t1,t3),
       append(t1,t1,x),append(t1,t3,l1),append(t1,t3,l2),append(t1,t3,l3),
       append(t1,t3,t1),append(t1,t3,t3),append(t1,t3,x),append(t1,x,l1),
       append(t1,x,l2),append(t1,x,l3),append(t1,x,t1),append(t1,x,t3),
       append(t1,x,x),append(t3,l1,l1),append(t3,l1,l2),append(t3,l1,l3),
       append(t3,l1,t1),append(t3,l1,t3),append(t3,l1,x),append(t3,l2,l1),
       append(t3,l2,l2),append(t3,l2,l3),append(t3,l2,t1),append(t3,l2,t3),
       append(t3,l2,x),append(t3,l3,l1),append(t3,l3,l2),append(t3,l3,l3),
       append(t3,l3,t1),append(t3,l3,t3),append(t3,l3,x),append(t3,t1,l1),
       append(t3,t1,l2),append(t3,t1,l3),append(t3,t1,t1),append(t3,t1,t3),
       append(t3,t1,x),append(t3,t3,l1),append(t3,t3,l2),append(t3,t3,l3),
       append(t3,t3,t1),append(t3,t3,t3),append(t3,t3,x),append(t3,x,l1),
       append(t3,x,l2),append(t3,x,l3),append(t3,x,t1),append(t3,x,t3),
       append(t3,x,x),append(x,l1,l1),append(x,l1,l2),append(x,l1,l3),
       append(x,l1,t1),append(x,l1,t3),append(x,l1,x),append(x,l2,l1),
       append(x,l2,l2),append(x,l2,l3),append(x,l2,t1),append(x,l2,t3),
       append(x,l2,x),append(x,l3,l1),append(x,l3,l2),append(x,l3,l3),
       append(x,l3,t1),append(x,l3,t3),append(x,l3,x),append(x,t1,l1),
       append(x,t1,l2),append(x,t1,l3),append(x,t1,t1),append(x,t1,t3),
       append(x,t1,x),append(x,t3,l1),append(x,t3,l2),append(x,t3,l3),
       append(x,t3,t1),append(x,t3,t3),append(x,t3,x),append(x,x,l1),
       append(x,x,l2),append(x,x,l3),append(x,x,t1),append(x,x,t3),
       append(x,x,x)])]

PCEX i([x,t3,t1,l3,l2,l1],
       [[],[cons(l1,x,t1),cons(l3,x,t3)],[],
        [member(x,l3),member(x,l1)],[append(t1,l2,t3),append(l1,l2,l3)]])

EQ [c([null(x)],[list(x),append(x,x,x)]),
    c([cons(x,t,h)],[member(t,x)]),
    c([cons(x,t,h),list(h),member(t,x)],[list(x)]),
    c([cons(x,t,h),member(i,h),member(t,x)],[member(i,x)]),
    c([null(x),list(l),list(x),append(x,x,x)],[append(x,l,l)]),
    c([cons(l3,x,t3),cons(l1,x,t1),member(x,l1),member(x,l3),append(t1,l2,t3)],
      [append(l1,l2,l3)])]


EQ answers "yes" here indicating that this is the right hypothesis.

The Final Hypothesis is:


[null(A)]  ---->  list(A)

[null(A)]  ---->  append(A,A,A)

[cons(B,C,D)]  ---->  member(C,B)

[cons(E,F,G),list(G),member(F,E)]  ---->  list(E)

[cons(H,I,J),member(K,J),member(I,H)]  ---->  member(K,H)

[null(L),list(M),list(L),append(L,L,L)]  ---->  append(L,M,M)

[cons(N,O,P),cons(Q,O,R),member(O,Q),member(O,N),append(R,S,P)]  
                                                     ---->  append(Q,S,N)

Using Logical Reduction to Simplify Hypothesis.
The Final Hypothesis is:


[null(A)]  ---->  list(A)

[cons(B,C,D)]  ---->  member(C,B)

[cons(E,F,G),list(G)]  ---->  list(E)

[cons(H,I,J),member(K,J)]  ---->  member(K,H)

[null(L),list(M)]  ---->  append(L,M,M)

[cons(N,O,P),cons(Q,O,R),append(R,S,P)]  ---->  append(Q,S,N)

Summary:
number of EQs: 15; 
number of MQs: 30; 
number of MQ cache hits: 5.

----------------------------------------------------------------------

The answers in this run were generated automatically by comparing the
algorithm's question to the program listed at the top. The examples
are quite helpful since they provide the "smallest" possible counter
example to the current hypothesis.  The algorithm is guaranteed to
work correctly for any choice of examples as long as the answers to
its questions are correct.  To find out more about the algorithm, how
it decides what to ask and how it generates hypotheses see the paper
mentioned above.

----------------------------------------------------------------------