The GLiDeS Strategy Backtracks

• 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