%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SWX055+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n020.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 Apr 1 02:12:56 AM UTC 2025
% Result : Theorem 269.81s 35.41s
% Output : CNFRefutation 269.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of clauses : 43 ( 15 unt; 14 nHn; 28 RR)
% Number of literals : 91 ( 15 equ; 37 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 64 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_129,plain,
( member_succeeds(X1,X2)
| member_fails(X1,X2)
| ~ list_succeeds(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_129) ).
cnf(i_0_557,negated_conjecture,
list_succeeds(esk138_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_557) ).
cnf(i_0_543,plain,
( occ(X1,X2) = '0'
| ~ list_succeeds(X2)
| ~ member_fails(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_543) ).
cnf(i_0_558,negated_conjecture,
list_succeeds(esk137_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_558) ).
cnf(i_0_555,negated_conjecture,
occ(esk139_0,esk138_0) != occ(esk139_0,esk137_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_555) ).
cnf(i_0_233,plain,
( member2_succeeds(X1,X2,X3)
| ~ member_succeeds(X1,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_233) ).
cnf(i_0_562,plain,
( occ_succeeds(X1,X2,X3)
| occ(X1,X2) != X3
| ~ list_succeeds(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_562) ).
cnf(i_0_297,plain,
( X1 = X2
| not_same_occ_succeeds(X3,X4)
| ~ member2_succeeds(X5,X3,X4)
| ~ occ_succeeds(X5,X4,X2)
| ~ occ_succeeds(X5,X3,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_297) ).
cnf(i_0_317,plain,
( not_same_occ_fails(X1,X2)
| ~ same_occ_succeeds(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_317) ).
cnf(i_0_556,negated_conjecture,
same_occ_succeeds(esk137_0,esk138_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_556) ).
cnf(i_0_201,plain,
( ~ not_same_occ_succeeds(X1,X2)
| ~ not_same_occ_fails(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_201) ).
cnf(i_0_232,plain,
( member2_succeeds(X1,X2,X3)
| ~ member_succeeds(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-zcc31uag/input.p',i_0_232) ).
cnf(c_0_575,plain,
( member_succeeds(X1,X2)
| member_fails(X1,X2)
| ~ list_succeeds(X2) ),
i_0_129 ).
cnf(c_0_576,negated_conjecture,
list_succeeds(esk138_0),
i_0_557 ).
cnf(c_0_577,plain,
( occ(X1,X2) = '0'
| ~ list_succeeds(X2)
| ~ member_fails(X1,X2) ),
i_0_543 ).
cnf(c_0_578,negated_conjecture,
( member_fails(X1,esk138_0)
| member_succeeds(X1,esk138_0) ),
inference(spm,[status(thm)],[c_0_575,c_0_576]) ).
cnf(c_0_579,negated_conjecture,
list_succeeds(esk137_0),
i_0_558 ).
cnf(c_0_580,negated_conjecture,
occ(esk139_0,esk138_0) != occ(esk139_0,esk137_0),
i_0_555 ).
cnf(c_0_581,plain,
( occ(X1,esk138_0) = '0'
| member_succeeds(X1,esk138_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_577,c_0_578]),c_0_576])]) ).
cnf(c_0_582,negated_conjecture,
( member_fails(X1,esk137_0)
| member_succeeds(X1,esk137_0) ),
inference(spm,[status(thm)],[c_0_575,c_0_579]) ).
cnf(c_0_583,negated_conjecture,
( member_succeeds(esk139_0,esk138_0)
| occ(esk139_0,esk137_0) != '0' ),
inference(spm,[status(thm)],[c_0_580,c_0_581]) ).
cnf(c_0_584,plain,
( occ(X1,esk137_0) = '0'
| member_succeeds(X1,esk137_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_577,c_0_582]),c_0_579])]) ).
cnf(c_0_585,plain,
( member2_succeeds(X1,X2,X3)
| ~ member_succeeds(X1,X3) ),
i_0_233 ).
cnf(c_0_586,plain,
( member_succeeds(esk139_0,esk137_0)
| member_succeeds(esk139_0,esk138_0) ),
inference(spm,[status(thm)],[c_0_583,c_0_584]) ).
cnf(c_0_587,plain,
( occ_succeeds(X1,X2,X3)
| occ(X1,X2) != X3
| ~ list_succeeds(X2) ),
i_0_562 ).
cnf(c_0_588,plain,
( X1 = X2
| not_same_occ_succeeds(X3,X4)
| ~ member2_succeeds(X5,X3,X4)
| ~ occ_succeeds(X5,X4,X2)
| ~ occ_succeeds(X5,X3,X1) ),
i_0_297 ).
cnf(c_0_589,plain,
( member2_succeeds(esk139_0,X1,esk138_0)
| member_succeeds(esk139_0,esk137_0) ),
inference(spm,[status(thm)],[c_0_585,c_0_586]) ).
cnf(c_0_590,plain,
( occ_succeeds(X1,X2,occ(X1,X2))
| ~ list_succeeds(X2) ),
inference(er,[status(thm)],[c_0_587]) ).
cnf(c_0_591,plain,
( not_same_occ_fails(X1,X2)
| ~ same_occ_succeeds(X1,X2) ),
i_0_317 ).
cnf(c_0_592,negated_conjecture,
same_occ_succeeds(esk137_0,esk138_0),
i_0_556 ).
cnf(c_0_593,plain,
( X1 = X2
| not_same_occ_succeeds(X3,esk138_0)
| member_succeeds(esk139_0,esk137_0)
| ~ occ_succeeds(esk139_0,esk138_0,X2)
| ~ occ_succeeds(esk139_0,X3,X1) ),
inference(spm,[status(thm)],[c_0_588,c_0_589]) ).
cnf(c_0_594,negated_conjecture,
occ_succeeds(X1,esk138_0,occ(X1,esk138_0)),
inference(spm,[status(thm)],[c_0_590,c_0_576]) ).
cnf(c_0_595,plain,
( ~ not_same_occ_succeeds(X1,X2)
| ~ not_same_occ_fails(X1,X2) ),
i_0_201 ).
cnf(c_0_596,negated_conjecture,
not_same_occ_fails(esk137_0,esk138_0),
inference(spm,[status(thm)],[c_0_591,c_0_592]) ).
cnf(c_0_597,negated_conjecture,
( X1 = occ(esk139_0,esk138_0)
| not_same_occ_succeeds(X2,esk138_0)
| member_succeeds(esk139_0,esk137_0)
| ~ occ_succeeds(esk139_0,X2,X1) ),
inference(spm,[status(thm)],[c_0_593,c_0_594]) ).
cnf(c_0_598,negated_conjecture,
occ_succeeds(X1,esk137_0,occ(X1,esk137_0)),
inference(spm,[status(thm)],[c_0_590,c_0_579]) ).
cnf(c_0_599,plain,
~ not_same_occ_succeeds(esk137_0,esk138_0),
inference(spm,[status(thm)],[c_0_595,c_0_596]) ).
cnf(c_0_600,plain,
( member2_succeeds(X1,X2,X3)
| ~ member_succeeds(X1,X2) ),
i_0_232 ).
cnf(c_0_601,negated_conjecture,
member_succeeds(esk139_0,esk137_0),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_597,c_0_598]),c_0_580]),c_0_599]) ).
cnf(c_0_602,plain,
member2_succeeds(esk139_0,esk137_0,X1),
inference(spm,[status(thm)],[c_0_600,c_0_601]) ).
cnf(c_0_603,plain,
( X1 = X2
| not_same_occ_succeeds(esk137_0,X3)
| ~ occ_succeeds(esk139_0,esk137_0,X1)
| ~ occ_succeeds(esk139_0,X3,X2) ),
inference(spm,[status(thm)],[c_0_588,c_0_602]) ).
cnf(c_0_604,negated_conjecture,
( occ(esk139_0,esk137_0) = X1
| not_same_occ_succeeds(esk137_0,X2)
| ~ occ_succeeds(esk139_0,X2,X1) ),
inference(spm,[status(thm)],[c_0_603,c_0_598]) ).
cnf(c_0_605,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_604,c_0_594]),c_0_580]),c_0_599]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWX055+1 : TPTP v9.1.0. Released v9.1.0.
% 0.07/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Mar 31 15:14:05 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.19/0.45 # ENIGMATIC: Selected SinE mode:
% 0.19/0.47 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.47 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.19/0.47 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.19/0.47 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 252.36/33.20 eprover: CPU time limit exceeded, terminating
% 269.81/35.41 # ENIGMATIC: Solved by Enigma+tptp-cade20-model03-h2e15+lgb-t150-d30-l4800-e0.15+coop-paramils157:
% 269.81/35.41 # SinE strategy is GSinE(CountFormulas,hypos,5.0,,3,500,1.0)
% 269.81/35.41 # ENIGMA: LightGBM model '/export/starexec/sandbox/solver/bin/data/Enigma/tptp-cade20-model03-h2e15/lgb-t150-d30-l4800-e0.15/model.lgb' loaded. (hash_base: 32768; conj_feats: 31; version: 991; iters: 150)
% 269.81/35.41 # Preprocessing time : 0.739 s
% 269.81/35.41
% 269.81/35.41 # Proof found!
% 269.81/35.41 # SZS status Theorem
% 269.81/35.41 # SZS output start CNFRefutation
% See solution above
% 269.81/35.41 # Training examples: 0 positive, 0 negative
% 269.81/35.41
% 269.81/35.41 # -------------------------------------------------
% 269.81/35.41 # User time : 2.785 s
% 269.81/35.41 # System time : 0.108 s
% 269.81/35.41 # Total time : 2.893 s
% 269.81/35.41 # ...preprocessing : 0.739 s
% 269.81/35.41 # ...main loop : 2.155 s
% 269.81/35.41 # Maximum resident set size: 155776 pages
% 269.81/35.41
%------------------------------------------------------------------------------