Home
last modified time | relevance | path

Searched refs:AVATAR_CONTRADICTION_CLAUSE (Results 1 – 4 of 4) sorted by relevance

/dports/math/vampire/vampire-4.5.1/Kernel/
H A DInference.hpp321 AVATAR_CONTRADICTION_CLAUSE, enumerator
H A DInference.cpp825 case InferenceRule::AVATAR_CONTRADICTION_CLAUSE: in ruleName()
H A DInferenceStore.cpp939 case InferenceRule::AVATAR_CONTRADICTION_CLAUSE: in hideProofStep()
/dports/math/vampire/vampire-4.5.1/Saturation/
H A DSplitter.cpp1661 …nit* scl = new FormulaUnit(f,NonspecificInference1(InferenceRule::AVATAR_CONTRADICTION_CLAUSE,cl)); in handleEmptyClause()