TRUE(t(x))  TRUE(l(x))
-TRUE(t(x))  -TRUE(l(x)).
-TRUE(t(x))  -TRUE(said(x,y))  TRUE(y).
-TRUE(l(x))  -TRUE(said(x,y))  -TRUE(y).
-TRUE(y)  -TRUE(said(x,y))  TRUE(t(x)).
TRUE(y)  -TRUE(said(x,y))  TRUE(l(x)).
TRUE(said(b,said(a,l(a)))).
TRUE(said(c,l(b))).

Place the first six clauses in the usable list, and
place the last two in the set of support.
Select the focal clause using the following method:
make the weight of a clause equal to the number of
symbols in the clause, excluding commas and parentheses.
Thus, the weight of clause 7 is 7,
and the weight of clause 8 is 5
(TRUE counts as a single symbol).
Now apply the algorithm and compute the generated clauses,
the results of subsumption,
the selection of the focal clause,
and whatever else is produced with the algorithm.
Use hyperresolution as the inference rule.