• Missing backtracking
• Missing backtracking on successful first-order unification
• Missing backtracking/postponing on failing too complex problem
• Backtracking points lost when using unification incrementally
• Inverting tuples in instances of existential variables
• Inverting case analysis on existential variables
• Another example of disjunction of problems
• Solvable second-order problems
• Investigation in further heuristics
• Extending the first-order unification heuristic into a "pattern-unification" heuristic
• Extending the first-order unification heuristic into a Libal-Miller functions-as-constructors heuristic
• See also