%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SEV625+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:51:35 PM UTC 2026
% Result : Theorem 166.25s 26.05s
% Output : CNFRefutation 166.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 6
% Syntax : Number of clauses : 18 ( 4 unt; 6 nHn; 11 RR)
% Number of literals : 32 ( 8 equ; 10 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 44 ( 9 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_3453,plain,
( X1 = X2
| ~ cHahnRelationsBasic_2eeqv__rel___24a4(X3,X4,X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-z4xa7oaa/input.p',i_0_3453) ).
cnf(i_0_348,plain,
( cHahnRelationsBasic_2eeqv__rel___24a4(X1,X2,X3,X4)
| ~ p(happ(happ(happ(happ(cHahnRelationsBasic_2eeqv__rel,X1),X2),X3),X4)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-z4xa7oaa/input.p',i_0_348) ).
cnf(i_0_3455,plain,
( cHahnRelationsBasic_2efunctional___24a2(X1,X2)
| p(happ(happ(X2,esk305_2(X1,X2)),esk307_2(X1,X2))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-z4xa7oaa/input.p',i_0_3455) ).
cnf(i_0_3454,plain,
( cHahnRelationsBasic_2efunctional___24a2(X1,X2)
| esk307_2(X1,X2) != esk306_2(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-z4xa7oaa/input.p',i_0_3454) ).
cnf(i_0_3456,plain,
( cHahnRelationsBasic_2efunctional___24a2(X1,X2)
| p(happ(happ(X2,esk305_2(X1,X2)),esk306_2(X1,X2))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-z4xa7oaa/input.p',i_0_3456) ).
cnf(i_0_3578,negated_conjecture,
~ cHahnRelationsBasic_2efunctional___24a2(cA,happ(happ(cHahnRelationsBasic_2eeqv__rel,cA),cdom)),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-z4xa7oaa/input.p',i_0_3578) ).
cnf(c_0_3585,plain,
( X1 = X2
| ~ cHahnRelationsBasic_2eeqv__rel___24a4(X3,X4,X1,X2) ),
i_0_3453 ).
cnf(c_0_3586,plain,
( cHahnRelationsBasic_2eeqv__rel___24a4(X1,X2,X3,X4)
| ~ p(happ(happ(happ(happ(cHahnRelationsBasic_2eeqv__rel,X1),X2),X3),X4)) ),
i_0_348 ).
cnf(c_0_3587,plain,
( X1 = X2
| ~ p(happ(happ(happ(happ(cHahnRelationsBasic_2eeqv__rel,X3),X4),X1),X2)) ),
inference(spm,[status(thm)],[c_0_3585,c_0_3586]) ).
cnf(c_0_3588,plain,
( cHahnRelationsBasic_2efunctional___24a2(X1,X2)
| p(happ(happ(X2,esk305_2(X1,X2)),esk307_2(X1,X2))) ),
i_0_3455 ).
cnf(c_0_3589,plain,
( cHahnRelationsBasic_2efunctional___24a2(X1,X2)
| esk307_2(X1,X2) != esk306_2(X1,X2) ),
i_0_3454 ).
cnf(c_0_3590,plain,
( esk307_2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3)) = esk305_2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3))
| cHahnRelationsBasic_2efunctional___24a2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3)) ),
inference(spm,[status(thm)],[c_0_3587,c_0_3588]) ).
cnf(c_0_3591,plain,
( cHahnRelationsBasic_2efunctional___24a2(X1,X2)
| p(happ(happ(X2,esk305_2(X1,X2)),esk306_2(X1,X2))) ),
i_0_3456 ).
cnf(c_0_3592,plain,
( cHahnRelationsBasic_2efunctional___24a2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3))
| esk306_2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3)) != esk305_2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3)) ),
inference(spm,[status(thm)],[c_0_3589,c_0_3590]) ).
cnf(c_0_3593,plain,
( esk306_2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3)) = esk305_2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3))
| cHahnRelationsBasic_2efunctional___24a2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3)) ),
inference(spm,[status(thm)],[c_0_3587,c_0_3591]) ).
cnf(c_0_3594,negated_conjecture,
~ cHahnRelationsBasic_2efunctional___24a2(cA,happ(happ(cHahnRelationsBasic_2eeqv__rel,cA),cdom)),
i_0_3578 ).
cnf(c_0_3595,plain,
cHahnRelationsBasic_2efunctional___24a2(X1,happ(happ(cHahnRelationsBasic_2eeqv__rel,X2),X3)),
inference(spm,[status(thm)],[c_0_3592,c_0_3593]) ).
cnf(c_0_3596,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3594,c_0_3595])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV625+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : enigmatic-eprover.py %s %d 1
% 0.17/0.34 % Computer : n013.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue May 5 06:11:42 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.30/0.49 # ENIGMATIC: Selected SinE mode:
% 0.47/0.63 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.63 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.47/0.63 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.47/0.63 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 166.25/26.05 # ENIGMATIC: Solved by Enigma+tptp-cade20-model03-h2e15+lgb-t150-d60-l8000-e0.15+coop-eprover73:
% 166.25/26.05 # ENIGMA: LightGBM model '/export/starexec/sandbox/solver/bin/data/Enigma/tptp-cade20-model03-h2e15/lgb-t150-d60-l8000-e0.15/model.lgb' loaded. (hash_base: 32768; conj_feats: 26; version: 991; iters: 150)
% 166.25/26.05 # Preprocessing time : 7.319 s
% 166.25/26.05 # Presaturation interreduction done
% 166.25/26.05
% 166.25/26.05 # Proof found!
% 166.25/26.05 # SZS status Theorem
% 166.25/26.05 # SZS output start CNFRefutation
% See solution above
% 166.25/26.05 # Training examples: 0 positive, 0 negative
% 166.25/26.05
% 166.25/26.05 # -------------------------------------------------
% 166.25/26.05 # User time : 18.958 s
% 166.25/26.05 # System time : 0.232 s
% 166.25/26.05 # Total time : 19.190 s
% 166.25/26.05 # ...preprocessing : 7.319 s
% 166.25/26.05 # ...main loop : 11.872 s
% 166.25/26.05 # Maximum resident set size: 209544 pages
% 166.25/26.05
%------------------------------------------------------------------------------