The GLiDeS Strategy
Input clauses other than the top clause are the
model clauses
Centre clause literals resolved against input clauses are required to be FALSE in models of the model clauses
TRUE centre clause literals resolve against ancestors