compare proofs given by LT to those found in Principia
in cases where LT found a much more general proof
what's happening in chs4 and 5?
is LT getting lost in search (branching factor too large)?
what happens to dumb rote when you put learned theorems in front?
incorporate measure like Minton's utility into EBL LT?
...
change control structure so LT isn't forced to produce linear trees
experiment with an EBL version of LT that stores macro operators
forget about known theorems used
just store compositions of chaining and dt