Before the question, let me explain better what is E-KRHyper:

E-KRHyper is a theorem proving and model generation system for ﬁrst-order logic with equality. It is an implementation of the E-hyper tableau calculus, which integrates a superposition-based handling of equality into the hyper tableau calculus (source: System Description: E-KRHyper).

I am interested in the complexity of system E-KRHyper because it is used in the question-answer system Log-Answer (LogAnswer – A Deduction-Based Question Answering System (System Description)).

I have found a partial answer:

our calculus is a non-trivial decision procedure for this fragment (with equality), which captures the complexity class

NEXPTIME(source: Hyper Tableaux with Equality).

I don’t understand much of complexity theory so my question is:

What is the complexity of a theorem to be proved in terms of the number of axioms in the database and in terms of some parameter of the question to be answered?