eprover output differs from expected output. EFOLReasoner does not work.

[NicoHubrach]

Hello Folks,

first I would like to thank you for your work on this library.
I am using your piece of software to implement a query language and so far the experience has been delightful.
Right now I am facing an issue that I cannot easily seem to fix.
I've installed the most recent version of eprover, that is:

$ eprover --version
E 3.5.1 Countess Grey (25808ee34733f8641fc5962acc203d453d9dbf1a)

and I am trying to evaluate a closed FO formula over a signature/structure.
This is the relevant code,

FolReasoner.setDefaultReasoner(new EFOLReasoner("eprover"));
FolReasoner prover = FolReasoner.getDefaultReasoner();
// ...
prover.query(bs, substitutedformula)

Since this is an easy example, I know for a fact that the query is true under the assumptions.
Nonetheless, your library returns false.

After some digging, I found that this line returns,

% Scheduled 1 strats onto 1 cores with 300 seconds (300 total)
% Starting G-E--_302_C18_F1_URBAN_RG_S04BN with 300s (1) cores
% G-E--_302_C18_F1_URBAN_RG_S04BN with pid 33403 completed with status 0
% Result found by G-E--_302_C18_F1_URBAN_RG_S04BN
% (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% No SInE strategy applied
% Search class: FUUNF-FFSM00-SFFFFFNN
% partial match(1): FUUNF-FFSF00-SFFFFFNN
% Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% Starting SubtermCWHack with 28s (1) cores
% SubtermCWHack with pid 33404 completed with status 0
% Result found by SubtermCWHack
% Initializing proof state
% Scanning for AC axioms
%
%cnf(i_0_1, plain, (Packages(pWithoutBody))).
%
%cnf(i_0_2, plain, (Packages(pWithNestationDeep))).
%
%cnf(i_0_3, plain, (Packages(pWithNestation))).
%
%cnf(i_0_4, plain, (Packages(pWithNestationDeepRealDeep))).
%
%cnf(i_0_7, plain, (isPackage(pWithoutBody))).
%
%cnf(i_0_6, plain, (isPackage(pWithNestationDeep))).
%
%cnf(i_0_10, plain, (isPackage(pWithNestation))).
%
%cnf(i_0_8, plain, (isPackage(pWithNestationDeepRealDeep))).
%
% Proof found!
% SZS status Theorem

which means that eprover successfully verifies the statement.

But the very next line checks in particular for a #.
You can clearly see that # has been changed to % at some point.

Hence, even though eprover verifies the statement, prover.query(...) returns false.
Fixing this is not hard, of course.
I propose instead of replacing # on line 115, you instead simply check for the string "Proof found!", to prevent such an error in the future.
But due to my lack of understanding of how maven works I am unable to locally build this and use the new jars.

Could you maybe push a fix to upstream some time soon or give some advice on how I can locally build your project and use the jars.
My deadline for my query language project is in a month :<

Thanks in advance and best regards from rwth!