Odpověď na názor

Podle mě prázdnou klauzuli z b != b pravidly rezoluce, faktorizace a paramodulace bez použití axiomu reflexivity neodvodíte. Důvod je jednoduchý - žádné z těch pravidel nejde použít.

Lze ale reflexivitu spojit s rezolucí a udělat pravidlo (s != t ⋁ R) → Rσ, kde σ = mgu(s, t).

Ještě jedna poznámka - u axiomů rovnosti vám chybí schémata kongruence.