Introduction to Artificial Inteligence
Assignment 3 - Solutions
Homework assignment - simulators, agents, search, games, logic, inference
1) Consider the following search problem over first-order logic (also known as
LEAST-COST PROOF, which is NP-hard, even if it is known that a proof with
a given finite n steps exists).
You have a list KB of clauses F1,...Fk. Each Fi is of the form:
l1 or l2 or ... lm
where the l's are literals, i.e. an atomic sentence or its negation.
You need to apply the operators: a) resolution b) simplification
in order to prove a propositional statement (by contradiction).
Assume that applying resolution costs 1, and
simplification costs 2 (simplification means: in a clause that contains
2 or more instances of the same literal - remove one of them. Note that only
ONE literal is removed at each step (e.g. reducing 3 copies of the same
litral to 1 copy takes 2 steps).
The problem is: given clauses KB and a sentence Y, find the proof P
that has the least cost. For example, we have the KB consisting of the
clauses:
C1: ~P(x) or Q(y)
C2: ~R(x) or Q(x)
C3: ~Q(z)
and need to prove the sentence Y: ~P(2) or ~R(M(1))
(hint - before the search, you need to add a transformed Y into your KB)
a) Write the above problem as a formal search problem. Note that the
path cost has to reflect the proof cost.
Initial state: the given KB with the negated sentence expressed in CNF added.
Goal test: True if the set of clauses contains the empty clause (a contradiction)
Operators: a) Resolution applied to any 2 clauses
b) Simplification applied to any clause
Path cost: Total cost of operators applied along path, 2 for simplification
and 1 for resolution.
In the example, the initial state contains: C1, C2, C3, and the negated Y, which becomes
TWO separate clauses: Y1': P(2) and Y2': R(M(1))
b) Consider the heuristic h(n) = number of literals in the shortest
clause. Is h(n) an admissible heuristic? Prove or disprove it.
This heuristic is admissible.
Proof:
1) Exact for goal: n is a goal state iff it contains the empty clause, which has length 0,
and thus h(n)=0 iff n is a goal state. (This claim is actually stronger than needed)
2) Optimistic: Simplification works on only one clause, costs 2, and decreases its
length by 1. Resolution creates a clause that is in the best case shorter by 1 than
the shorter of the 2 clauses, and its cost is 1.
Let h*(n) be the true cost to reach the goal. Since non of the operators decrease the
size of the minimum cost by more than 1, the number of operators to be applied NO(n)
in the optimal proof is at least h(n). But since each oparator costs at least 1, we
have h*(n) >= NO(n) >= h(n).
c) Find another another admissible heuristic h1 that performs better than h,
for at least SOME cases (and provide an example or prove that it dominates
h).
Resolution can only decrease the length of the longer clasue if one
of the clauses is a unit clause. Therefore, if there is no unit clause
in the KB and no clause with duplicate literals, adding 1 to the length
of the shortest clause still results in an admissible heuristic. Clearly
h1 as defined here dominates h, so we need no examples...
(Above is called "proof by intimidation".)
d) Find a non-admissible heuristic h2 and an example where it performs better
than h and h1.
Multiplying an admissible heuristic by a large enough constant K will
make a heuristic inadmissible. For example, making K approach infinity
will result in A* acting like greedy search. The performance will thus
be better every time greedy search works better than A*. An example
is where there are many proofs of equal length, where there appears
to be no initial headway. In this case, greedy will find a solution
fast (sometimes even an optimal solution), while A* can take a very
long time!
e) Would keeping track of repeated states help in the search algorithm? If so,
give an example.
YES, because, for example, exchanging the steps in a proof can be possible in many cases,
leading to the same state and with the same path cost. This can save (potentially)
an exponential number of expansions. Example KB: A v A, B v B, ~A v ~B
In this case we can begin by simplifying the first clause to A, or the 2nd clause to B,
or 2 possible resolutions. Now, for the case where we simplified the 1st clause,
we can simplify the 2nd clause, to get the KB: A, B, ~A v ~B. Likewise, for the case
where we earlier simplified the 2nd clause, we can now simplify the 1st clause, to
get the KB: A, B, ~A v ~B. Now from each of the KBs we have 2 possible resolutions, so
clearly it is better to remove the redundant duplicate KB - which has the exact
same path cost - in order to save on search!
f) Can the algorithm be made more efficient in SPACE requirements, if
we need to find ANY proof, rather than the shortest proof? How, and
how much more efficient, asymptotically?
Yes, since if we do not care about length of proof, all we need do is reach an empty clause,
and can keep just ONE set of clauses, and just add to it all the generated clauses. That
is because FOL is MONOTONIC.
2) For each of the following English sentences, represent them in FOL
using the predicates given. Then, show the steps in converting them
into conjunctive normal form.
a) Every politician is popular in some state.
(predicates: politician(x), popular_in(x, y), state(y))
Forall x politician(x) => exists y state(y) and popular_in(x, y)
1. Remove =>
Forall x not politician(x) or ( exists y state(y) and popular_in(x, y))
2,3. Move negation inwards, standardize apart - no need, already correct
4. Move quantifiers left:
Forall x Exists y (not politician(x) or ( state(y) and popular_in(x, y)))
5. Skolemize: existential y in scope of universal x, use Skolem function StateOf(x)
Note: name of function is immaterial, as long as it is a NEW function name...
Forall x not politician(x) or ( state(StateOf(x)) and popular_in(x, StateOf(x)))
6. Remove universals:
not politician(x) or ( state(StateOf(x)) and popular_in(x, StateOf(x)))
7. Distribute and over or (generates TWO clauses):
a1: not politician(x) or state(StateOf(x))
a2: not politician(x) or popular_in(x, StateOf(x))
b) Every dog that has at least three unbroken legs can walk.
(predicates: dog(x), can_walk(x), has(x, y), leg(y), broken(y), equality ("="))
Forall x (dog(x) and
Exists y1, y2, y3 has(x, y1) and leg(y1) and not broken(y1) and
has(x, y2) and leg(y2) and not broken(y2) and
has(x, y3) and leg(y3) and not broken(y3) and
not (y1=y2) and not (y1=y3) and not (y2=y3) ) =>
can_walk(x)
1. Remove =>
Forall x not (dog(x) and
Exists y1, y2, y3 has(x, y1) and leg(y1) and not broken(y1) and
has(x, y2) and leg(y2) and not broken(y2) and
has(x, y3) and leg(y3) and not broken(y3) and
not (y1=y2) and not (y1=y3) and not (y2=y3) )
or can_walk(x)
2. Move negation inwards
Forall x not dog(x) or
(Forall y1, y2, y3 not has(x, y1) or not leg(y1) or broken(y1) or
not has(x, y2) or not leg(y2) or broken(y2) or
not has(x, y3) or not leg(y3) or broken(y3) or
y1=y2 or y1=y3 or y2=y3 )
or can_walk(x)
3. Standardize apart - not needed here.
4. Move quantifiers left:
Forall x, y1, y2, y3 not dog(x) or
not has(x, y1) or not leg(y1) or broken(y1) or
not has(x, y2) or not leg(y2) or broken(y2) or
not has(x, y3) or not leg(y3) or broken(y3) or
y1=y2 or y1=y3 or y2=y3
or can_walk(x)
5. Skolemize: not needed (no exsistential quantifiers)
6. Drop universal quantifiers:
b: not dog(x) or
not has(x, y1) or not leg(y1) or broken(y1) or
not has(x, y2) or not leg(y2) or broken(y2) or
not has(x, y3) or not leg(y3) or broken(y3) or
y1=y2 or y1=y3 or y2=y3 or can_walk(x)
The above clause is already one (somewhat long) CNF clause, no further steps necessary.
c) Some politicians can fool some of the people all of the time
(predicates: politician(x), can_fool(x, y, t), person(y))
Exists x, y politician(x) and person(x) and Forall t can_fool(x, y, t)
1,2,3: Remove =>, move negation, standardize apart - not needed.
4: Move quantifiers left:
Exists x, y Forall t politician(x) and person(x) and can_fool(x, y, t)
5: Skolemize - we have two existential variables not in the scope of universals, so
two Skolem constants, call them POLI and FOOLED
Forall t politician(POLI) and person(FOOLED) and can_fool(POLI, FOOLED, t)
6: Remove universals.
politician(POLI) and person(FOOLED) and can_fool(POLI, FOOLED, t)
The above is three separate CNF clauses:
c1: politician(POLI)
c2: person(FOOLED)
c3: can_fool(POLI, FOOLED, t)
3) We have a search problem where the cost of each operator is 1. The branching
factor is bounded by b. We have a heuristic evaluation function h(n) that
is admissible, and such that h(n) >= h*(n) - 3 (that is, it is never off by more than 3).
We use h(n) as a search heuristic in the A* algorithm.
a) Suppose that there is only one solution to the problem. How many nodes will be
expanded by A* using h(n) above as a heuristic, in the worst case, if
h*(initial_state) = d ?
Actually, the question can be read in more than 1 way, we could have only one path
to a solution, or multile paths to the SAME solution. We will solve this under
both definitions, either of which constitutes a correct answer.
If there is only one solution PATH, then every node not on this path must have
infinite h*(n), and thus also infinite h(n), and will never be expanded. As a result,
only d+1 nodes will be expanded.
If solution is just the STATE (only one such solution) but many paths to the solution,
still the number of paths is bounded due to the branching factor. But there are a LOT of ways
of equal length in the worst case, so this number is exponential in d. In fact, it can
be as much as b^(d+2). Henceforth we will thus assume in following questions that
a solution is a PATH (i.e. one solution means one path).
b) How does the above change if there is more than one solution, but any other solution
has path cost at least 4 greater than d?
Using the former assumption - only one optimal PATH. In this case AGAIN the number of
expanded nodes is d+1, as follows. Let n be a node in the queue, with f(n)=g(n)+h(n),
that is not on the optimal path. This implies n is either on a non-solution path,
and has infinite h(n) (thus never expanded), or is on the optimal path to some other solution
g, with g(g) => d+4. Now, f(n) =g(n) + h(n) >= g(n) + h*(n) - 3 = g(g) - 3 > d.
This means that n will never be expanded, because the optimal node g* will be expanded
earlier.
c) Same as in (b), but there is also ONE solution with cost d+2.
In this case, nodes on the path to the secondary goal may also be expanded, and
in fact all the nodes on that path up to but not including the secondary goal
may be expanded in the worst case. Total expansions would be: 2d + 3.
4) Consider the stochastic game to be implemented in assignment 2: grid based environment,
agents can move forward, turn right or left, and shoot (hitting with probability p/d, where
d is the distance). You may assume a time limit as desired for the length of the game in
each scenario.
a) Show a scenario (with no bullets) where for the first agent to move, under zero-sum scoring,
moving forward loses, but under total flags collected scoring the optimal move is to move forward.
Consider the following scenario, with agent A to move, and where the game ends after
a time limit of 6 ply (3 moves by each agent).
+------+------+------+------+
| F1 | F2 | A | |
| (1) | (1) | <-- | |
| | | | |
+------+------+------+------+
| B | | F3 | F4 |
| --> | | (1) | (10) |
| | | | |
+------+------+------+------+
Observe that without opposition, B can reach either F1 or F3 and F4, but A can only reach F1 and
F2 (by moving forward) or F3. If A moves forward, then B will be able to reach the F3 and F4
flags, and under zero-sum scoring the score will be at best -9 for A. Therefore, the best action
for A is to turn left and then take F3, in which case B will take F1 for a total score
difference of 0.
However, under total flags collected scoring, A should move forward in order to collect
F2 and F1 for a score of 2, allowing B to collect F3 and F4 for a score of 11.
b) In the game with bullets, show a scenario where the the first agent to move loses.
+------+------+------+
| | F | |
| | (1) | |
| | | |
+------+------+------+
| B | | A |
| --> | | <-- |
| | | |
+------+------+------+
| | F | |
| | (1) | |
| | | |
+------+------+------+
Suppose that A is to move, and p=1 and k=1. There are 4 possibilities here:
A: Forward loses - score is -2 because then B shoots and kills A, and can then
get both flags. No need for search to prove this.
Turn left or right loses (consider just one of them, due to symmetry):
B: Shoots. This has two outcomes, each with probability 0.5
A dies, and then B collects flags to get score of 2 (i.e. -2 for A)
A lives, and then:
A: Forward to collect a flag, and gets it, but B can get the other flag
(score here is 0).
A: Turn left (in order to shoot).
B: Turn right (or left, which is the same) in order to run and collect a flag.
A: Shoots, and then with probability 0.5:
B dies, and A scores 2, or -2 for B.
B lives, and can then collect 1 flag (score 0).
(expected score here is 1 for A).
B: forward (A shoots and score is 2 for A)
(So in the case B should turn, and expected score is 1 for A).
A: Other actions: score of 0 for A (each collects a flag).
(Best action for A is thus turn left, expected score 1).
(Expected value of B's shot is thus -0.5 for A and 0.5 for B).
Since the scenario is symmetric, if B moves first then B's expected score is -0.5,
i.e. the first player to move is expected to lose!)
In both cases, you must PROVE the scores by generating the respective game tree, either
to a terminal position or prove that you can prune some branches.
c) Suggest heuristic evaluation functions for the total-flags scoring version of the game:
1) One that is a lower bound, but non-trivial.
A trivial lower bound is value of flags already collected.
To that, we can safely add value of flags in partial spanning tree with cost
that is less than half the manhattan distance between agent A and agent B
(so that B will not be able to block A).
2) One that is optimistic an upper bound, but non-trivial
A rather trivial upper bound is value of flags collected plus value of all
remaining flags. From this we can safely subtract the values of flags the opposing
agent can reach before we can reach them (or block the opponent), that is,
the part of the spanning tree for the opponent with total distance less than half
the manhattan distance between agent A and agent B (so that we cannot collect these
flags before the opponent, and cannot block its way).
5) Completing the proof from wumpus world done in class, plus a bit more...
a) Write the following domain axioms in FOL:
1. A wumpus stinks up all ajacent squares. ("square" and "location" are used interchangably here)
Forall l1, l2 Wumpus(l1) and Adjacent (l1, l2) => Stinky(l2)
(also need to restrict l1 and l2 to be legal locations, but we can do that in
the requirements for "Adjacent")
2. Only at most one square contains a wumpus. (This is a new one, to make it interesting).
Forall l1, l2 Wumpus(l1) and Wumpus(l2) => l1 = l2
(Note that although these should also be Legal locations, we can ignore
this requirement for our limited application)
3. A stinky square implies a wumpus in an adjacent square.
Forall l1, l2 Stinky(l1) => Exists l2 Wumpus(l2) and Adjacent(l1, l2)
4. Zero is an integer, and a successor of an integer is an integer.
(We need to add an "Integer" predicate in order to encode this).
Integer(0) and (forall x Integer(x) => IntegerS(x))
5. The successor of 0 is 1, ... the successor of 3 is 4...
S(0) = 1 and S(1) = 2 and S(2) = 3 and S(3) = 4
6. An integer is greater-than-or equal to itself, and a successor of an
integer x is greater-than-or-equal to x.
Forall x (x >= x) and (S(x) => x)
7. The value of the function first(x) is the first element of x.
Forall x, y x = First([x, y])
8. The value of the function second(x) is the second element of x.
Forall x, y y = Second([x, y])
9. Squares (locations) are adjacent if and only if they have one coordinate
equal to the other, and in the other coordinate one is the successor of
another, and both are legal.
Forall x1, x2, y1, y2 Adjacent([x1, y1], [x2, y2]) <=>
(Legal([x1, y1]) and Legal([x2, y2]) and
((x1=x2 and (y1 = S(y2) or y2 = S(y1))) or
(y1=y2 and (x1 = S(x2) or x2 = S(x1)))))
10. A square (location) is legal if and only if its first and second
coordinates are between 1 and 4.
Forall x, y Legal([x, y]) <=>
(Integer(x) and Integer(y) and x >= 1 and 4 >= x and y >= 1 and 4 >= y)
11. A location with no wumpus is safe.
Forall x, y not Wumpus([x, y]) => Safe([x,y])
The predicates to use are:
Wumpus(loc), Legal(loc), Adjacent(loc1, loc2), Stinky(loc), Safe(loc), x=y, x >= y
Constants to be used are: 0, 1, 2, 3, 4, 5, ...
Functions to be used are: S(x), First(x), Second(x).
b) Convert the above into conjunctive normal form, this is your basic KB.
1. not Wumpus(l1) or not Adjacent (l1, l2) or Stinky(l2)
2. not Wumpus(l1) or not Wumpus(l2) or l1 = l2
3a. not Stinky(l1) or Wumpus(WumpusLocationFor(l1))
3b. not Stinky(l1) or Adjacent(l1, WumpusLocationFor(l1))
(Using a Skolem function of one argument WumpusLocationFor(l1))
4a. Integer(0)
4b. not Integer(x) or Integer(S(x))
5a. S(0) = 1
5b. S(1) = 2
5c. S(2) = 3
5d. S(3) = 4
6a. x >= x
6b. S(x) => x
7. x = First([x, y])
8. y = Second([x, y])
Due to complicated and/or structure, 9 breaks up into quite a number of CNF clauses:
9a. not Adjacent([x1, y1], [x2, y2]) or Legal([x1, y1])
9b. not Adjacent([x1, y1], [x2, y2]) or Legal([x2, y2])
9c. not Adjacent([x1, y1], [x2, y2]) or x1=x2 or y1=y2
9d. not Adjacent([x1, y1], [x2, y2]) or x1=x2 or x1=S(x2) or x2=S(x1)
9e. not Adjacent([x1, y1], [x2, y2]) or y1=y2 or y1=S(y2) or y2=S(y1)
9f. not Adjacent([x1, y1], [x2, y2]) or x1=S(x2) or x2=S(x1) or y1=S(y2) or y2=S(y1)
9g. Adjacent([x1, y1], [x2, y2]) or not Legal([x1, y1]) or not Legal([x2, y2])
or not x1=x2 or not y1=S(y2)
9h. Adjacent([x1, y1], [x2, y2]) or not Legal([x1, y1]) or not Legal([x2, y2])
or not x1=x2 or not y2=S(y1)
9i. Adjacent([x1, y1], [x2, y2]) or not Legal([x1, y1]) or not Legal([x2, y2])
or not y1=y2 or not x1=S(x2)
9j. Adjacent([x1, y1], [x2, y2]) or not Legal([x1, y1]) or not Legal([x2, y2])
or not y1=y2 or not x2=S(x1)
Same goes for 10:
10a. Legal([x, y]) or not Integer(x) or not Integer(y) or not x >= 1 or not 4 >= x or
not y >= 1 or not 4 >= y
10b. not Legal([x, y]) or Integer(x)
10c. not Legal([x, y]) or Integer(x)
10d. not Legal([x, y]) or x >= 1
10e. not Legal([x, y]) or 4 >= x
10d. not Legal([x, y]) or y >= 1
10d. not Legal([x, y]) or 4 >= y
11. Wumpus([x, y]) or Safe([x,y])
c) Add the following to the basic KB:
13. not Stinky([2,1])
Prove by refutation (using just resolution) that Safe([2,2]).
We add the negation (already a single clause):
14. not Safe([2,2])
And now we can start the proof. 14 resolves with 11, {x/2, y/2} to get:
15. Wumpus([2,2])
Resolving 15 with 1, {l1/[2,2]} we get:
16. not Adjacent([2,2], l2) or Stinky (l2)
Resolving 16 with 13, {l2/[2, 1]} we get:
17. not Adjacent([2,2], [2,1])
Resolving 17 with 9g, {x1/2, y1/2, x2/2. y2/1} we get:
18. not Legal([2, 2]) or not Legal([2, 1]) or not 2=2 or not 2=S(1)
Here we find that we are missing axioms fr equality! Let us have:
=a. x=x (= is reflexive)
=b. not x=y or y=x (= is symmetric)
=c. not x=y or not y=z or x=x (= is transitive)
Now, resolving 18 with =a, {x/2} we get:
19. not Legal([2, 2]) or not Legal([2, 1]) or not 2=S(1)
Resolving 19 with =b, {y/2, x/S(1)} we get:
20. not Legal([2, 2]) or not Legal([2, 1]) or not S(1)=2
Resolving 20 with 5a:
21. not Legal([2, 2]) or not Legal([2, 1])
Now, let us assume for simplicity that we have already added the sentences Lij: Legal([i,j])
(see appendix on how this is done).
Resolving 21 with L22 we get:
22. not Legal([2, 1])
and finally, resolving 22 with L21 we get the empty clause, which proves
the "theorem" Safe([2, 2]) by contradiction.
d) In addition to the above, add to the KB: Stinky([3,1]) and Stinky([2,2]).
Prove by refutation (using just resolution): Safe([1,2]).
We begin by adding:
D1: Stinky([3,1])
D2: Stinky([2,2])
And then in order to begin the proof, we add the negation of the query:
Q2: not Safe([1,2])
Now we can begin, resolving Q2 with 11, {x/1, y/2} to get:
D3: Wumpus([1,2])
Resolve D3 with 2, {l1/[1,2} to get:
D4: not Wumpus(l2) or [1,2] = l2
Now we resolve D1 with 3a, {l1/[3,1]} to get:
D5: Wumpus(WumpusLocationFor([3,1])
Likewise, we resolve D1 with 3b wo get:
D6: Adjacent([3,1], WumpusLocationFor([3,1]))
Resolve D5 with D4, {l2/WumpusLocationFor([3,1])} to get:
D7: [1,2] = WumpusLocationFor([3,1])
We are missing YET ANOTHER equality axiom, which is:
EE: not Adjacent(l1, l2) or not l3=l2 or Adjacent(l1, l3)
Resolve EE with D6, {l1/[3,1], l2/WumpusLocationFor([3,1])} we get:
D8: not l3=WumpusLocationFor([3,1]) or Adjacent([3,1], l3)
Resolve D8 with D7, {l3/[1,2]} to get:
D9: Adjacent([3,1], [1,2])
Now, resolve D9 with the 9c axiom for adjacency, with {x1/3, y1/1, x2/1, y2/2} to get:
D10: 3=1 or 1=2
Now we are missing some MORE trivial axioms, for example we need to know that not 3=1,
etc. Let us assume that we already have axioms NEij for all such cases...
(This is a lot of axioms! however we can start with:
NE: not S(x) = x
NE': not S(x) = y or not x >= z or not y=z
EQ': not y=x or y=z or not x=z
And from these we can quickly get what we need, e.g. resolving EQ' with 5b,
with {y/S(1), x/1} we get:
S(1)=z or not 2=z
Resolving the latter with NE, {x/1, z/1} we get:
NE10: not 2=1
In this way we can show all the required inequalities NEij.
)
Now, we can finally resolve D10 with NE31 followed by resolving the result with NE12 to
get the empty clause!
----------------------------------------------------------------------------------------------
Appendix: we need to prove the statements Lij: Legal([i, j]) for some of the i, j in
order to complete the proofs. Note that this is NOT query dependent, in the sense
that we can do it for all integer i, j greater than 0 and less than 5. But we don't need
ALL of them here, just the ones for the actual queries. Nevertheless, below is the
method to obtain them by resolution.
First, we generate the required integers and their comparative size. We need additional
axioms for equality (these could be avoided with an inference rule treating equality in
a special way that allows unification up to equality):
I1: not Integer(x) or not x=y or Integer(y)
I2: not (S(x) >= x) or not (S(x) = y) or y >=x
Resolving 4a with 4b, {x/0} we get:
A1: Integer(S(0))
Resolving A1 with I1, {x/S(0)} we get:
A2: not S(0) = y or Integer(y)
Resolving A2 with 5a, {y/1} we get:
A3: Integer(1)
In a similar wa we resolve A3 with 4b, then with I1, then with 5b, to get,
A4: Integer(2)
And likewise:
A5: Integer(3)
Now we need to prove some auxilliary i => j statements.
Resolving 6b with I2, {x/x, y/2} we get (note wierd notation - we actually should have
had a different variable, say x', instead of x in I2, and then the substitution would
have been: {x'/x, y/2}):
A6: not (S(x) = y) or y >= x
Now we resolve A7 with 5b, {x/1, y/2} to get:
A8: 2 >=1
Resolving A6 with 5c, {x/2, y/3} we get:
A9: 3 >=2
And resolving A6 with 5d, {x/3, y/4} we get:
A10: 4 >= 3
We now also need transitivity of =>:
GE: not x=> y or not y=>z or x=>z
Resolving GE with A8 then the result with A9, unifiers {y/2, z/1} and {x/3} respectively, we get:
A11: 3 >= 1
Likewise resolving GE with A9 and A10 we get:
A12: 4 >= 2
And resolving GE with A12 and A8 we get:
A13: 4 >= 1
Now we can try to prove some Legal([i,j]) statements. For example, resolving 10a
with A4, {x/2} we get:
A14: Legal([2, y]) or not Integer(y) or not 2 >= 1 or not 4 >= 2 or not y >= 1 or not 4 >= y
Resolving A14 with A8 and A13 we get:
A15: Legal([2, y]) or not Integer(y) not y >= 1 or not 4 >= y
Resolving A15 with A3, {y/1} we get:
A15: Legal([2, 1]) or not 1 >= 1 or not 4 >= 1
And finally resolving A15 with 6a, {x/1} and then with A13 we get:
L21: Legal([2, 1])
In a similar way we can resolve A14 with A4, {y/2} to get:
A16: Legal([2, 2]) or not 2 >= 1 or not 4 >= 2
And then resolve A16 with A8 followed by resolution with A12 to get:
L22: Legal([2, 2])
Likewise for all the othe Lij statements we need...