// STRATEGIES -------------------------------------
strategy propagateDownFormulae
  firstRule
    propDownNec
    propDownNotNec
    propDownAnd
    propDownNotAnd
    propDownNoNot
  end
end

strategy resolveWithLittAndAtLeaf
  firstRule
    resolveWhenSat
    resolveWhenNotSat	
    resolveWithNot

    propUpNecAtLeaf
    propUpNotNecAtLeaf
  end
end

strategy propagateUpFormulae
  firstRule
    propUpNecSat
    propUpNecNotSat
    propUpNotNecSat
    propUpNotNecNotSat

    propUpAndLeft
    propUpAndRight
    propUpAndBothSat
    propUpAndBothNotSat

    propUpNotAndLeft
    propUpNotAndRight
    propUpNotAndBothSat
    propUpNotAndBothNotSat

    propUpNoNotSat
    propUpNoNotNotSat
  end
end

//-------------------------------------------------
//Global strategy
strategy modelChecking
allRules
  buildModel
  repeat 
	propagateDownFormulae
  end
  repeat 
	resolveWithLittAndAtLeaf
  end
  repeat 
	propagateUpFormulae
  end
end
end