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?