%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SWX060+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n017.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:57 AM UTC 2025
% Result : Theorem 98.08s 13.84s
% Output : CNFRefutation 98.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 15
% Syntax : Number of clauses : 48 ( 17 unt; 10 nHn; 32 RR)
% Number of literals : 114 ( 0 equ; 61 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 67 ( 14 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_537,plain,
( member2_terminates(X1,X2,X3)
| ~ list_succeeds(X3)
| ~ list_succeeds(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_537) ).
cnf(i_0_551,negated_conjecture,
list_succeeds(esk134_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_551) ).
cnf(i_0_552,negated_conjecture,
list_succeeds(esk133_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_552) ).
cnf(i_0_18,plain,
( member2_succeeds(X1,X2,X3)
| member2_fails(X1,X2,X3)
| ~ member2_terminates(X1,X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_18) ).
cnf(i_0_539,plain,
( gr(X1)
| ~ gr(X2)
| ~ gr(X3)
| ~ member2_succeeds(X1,X3,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_539) ).
cnf(i_0_550,negated_conjecture,
gr(esk133_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_550) ).
cnf(i_0_549,negated_conjecture,
gr(esk134_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_549) ).
cnf(i_0_538,plain,
( occ_terminates(X1,X2,X3)
| ~ gr(X1)
| ~ gr(X2)
| ~ list_succeeds(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_538) ).
cnf(i_0_126,plain,
( not_same_occ_terminates(X1,X2)
| ~ member2_fails(esk20_2(X1,X2),X1,X2)
| ~ member2_terminates(esk19_2(X1,X2),X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_126) ).
cnf(i_0_548,negated_conjecture,
~ not_same_occ_terminates(esk133_0,esk134_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_548) ).
cnf(i_0_20,plain,
( occ_succeeds(X1,X2,X3)
| occ_fails(X1,X2,X3)
| ~ occ_terminates(X1,X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_20) ).
cnf(i_0_123,plain,
( not_same_occ_terminates(X1,X2)
| ~ gr(esk22_2(X1,X2))
| ~ gr(esk24_2(X1,X2))
| ~ member2_terminates(esk19_2(X1,X2),X1,X2)
| ~ occ_terminates(esk20_2(X1,X2),X2,esk23_2(X1,X2))
| ~ occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_123) ).
cnf(i_0_540,plain,
( gr(X1)
| ~ occ_succeeds(X2,X3,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_540) ).
cnf(i_0_124,plain,
( not_same_occ_terminates(X1,X2)
| ~ member2_terminates(esk19_2(X1,X2),X1,X2)
| ~ occ_fails(esk20_2(X1,X2),X2,esk24_2(X1,X2))
| ~ occ_terminates(esk20_2(X1,X2),X2,esk23_2(X1,X2))
| ~ occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_124) ).
cnf(i_0_125,plain,
( not_same_occ_terminates(X1,X2)
| ~ member2_terminates(esk19_2(X1,X2),X1,X2)
| ~ occ_fails(esk20_2(X1,X2),X1,esk22_2(X1,X2))
| ~ occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-ctwlim8d/input.p',i_0_125) ).
cnf(c_0_568,plain,
( member2_terminates(X1,X2,X3)
| ~ list_succeeds(X3)
| ~ list_succeeds(X2) ),
i_0_537 ).
cnf(c_0_569,negated_conjecture,
list_succeeds(esk134_0),
i_0_551 ).
cnf(c_0_570,negated_conjecture,
( member2_terminates(X1,X2,esk134_0)
| ~ list_succeeds(X2) ),
inference(spm,[status(thm)],[c_0_568,c_0_569]) ).
cnf(c_0_571,negated_conjecture,
list_succeeds(esk133_0),
i_0_552 ).
cnf(c_0_572,plain,
( member2_succeeds(X1,X2,X3)
| member2_fails(X1,X2,X3)
| ~ member2_terminates(X1,X2,X3) ),
i_0_18 ).
cnf(c_0_573,negated_conjecture,
member2_terminates(X1,esk133_0,esk134_0),
inference(spm,[status(thm)],[c_0_570,c_0_571]) ).
cnf(c_0_574,plain,
( gr(X1)
| ~ gr(X2)
| ~ gr(X3)
| ~ member2_succeeds(X1,X3,X2) ),
i_0_539 ).
cnf(c_0_575,negated_conjecture,
( member2_fails(X1,esk133_0,esk134_0)
| member2_succeeds(X1,esk133_0,esk134_0) ),
inference(spm,[status(thm)],[c_0_572,c_0_573]) ).
cnf(c_0_576,negated_conjecture,
gr(esk133_0),
i_0_550 ).
cnf(c_0_577,negated_conjecture,
gr(esk134_0),
i_0_549 ).
cnf(c_0_578,plain,
( occ_terminates(X1,X2,X3)
| ~ gr(X1)
| ~ gr(X2)
| ~ list_succeeds(X2) ),
i_0_538 ).
cnf(c_0_579,plain,
( not_same_occ_terminates(X1,X2)
| ~ member2_fails(esk20_2(X1,X2),X1,X2)
| ~ member2_terminates(esk19_2(X1,X2),X1,X2) ),
i_0_126 ).
cnf(c_0_580,plain,
( member2_fails(X1,esk133_0,esk134_0)
| gr(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_574,c_0_575]),c_0_576]),c_0_577])]) ).
cnf(c_0_581,negated_conjecture,
~ not_same_occ_terminates(esk133_0,esk134_0),
i_0_548 ).
cnf(c_0_582,negated_conjecture,
( occ_terminates(X1,esk134_0,X2)
| ~ gr(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_578,c_0_569]),c_0_577])]) ).
cnf(c_0_583,plain,
gr(esk20_2(esk133_0,esk134_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_579,c_0_580]),c_0_573])]),c_0_581]) ).
cnf(c_0_584,plain,
( occ_succeeds(X1,X2,X3)
| occ_fails(X1,X2,X3)
| ~ occ_terminates(X1,X2,X3) ),
i_0_20 ).
cnf(c_0_585,negated_conjecture,
occ_terminates(esk20_2(esk133_0,esk134_0),esk134_0,X1),
inference(spm,[status(thm)],[c_0_582,c_0_583]) ).
cnf(c_0_586,negated_conjecture,
( occ_terminates(X1,esk133_0,X2)
| ~ gr(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_578,c_0_571]),c_0_576])]) ).
cnf(c_0_587,plain,
( not_same_occ_terminates(X1,X2)
| ~ gr(esk22_2(X1,X2))
| ~ gr(esk24_2(X1,X2))
| ~ member2_terminates(esk19_2(X1,X2),X1,X2)
| ~ occ_terminates(esk20_2(X1,X2),X2,esk23_2(X1,X2))
| ~ occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2)) ),
i_0_123 ).
cnf(c_0_588,plain,
( gr(X1)
| ~ occ_succeeds(X2,X3,X1) ),
i_0_540 ).
cnf(c_0_589,plain,
( occ_fails(esk20_2(esk133_0,esk134_0),esk134_0,X1)
| occ_succeeds(esk20_2(esk133_0,esk134_0),esk134_0,X1) ),
inference(spm,[status(thm)],[c_0_584,c_0_585]) ).
cnf(c_0_590,negated_conjecture,
occ_terminates(esk20_2(esk133_0,esk134_0),esk133_0,X1),
inference(spm,[status(thm)],[c_0_586,c_0_583]) ).
cnf(c_0_591,plain,
( ~ occ_terminates(esk20_2(esk133_0,esk134_0),esk133_0,esk21_2(esk133_0,esk134_0))
| ~ gr(esk22_2(esk133_0,esk134_0))
| ~ gr(esk24_2(esk133_0,esk134_0)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_587,c_0_585]),c_0_573])]),c_0_581]) ).
cnf(c_0_592,plain,
( not_same_occ_terminates(X1,X2)
| ~ member2_terminates(esk19_2(X1,X2),X1,X2)
| ~ occ_fails(esk20_2(X1,X2),X2,esk24_2(X1,X2))
| ~ occ_terminates(esk20_2(X1,X2),X2,esk23_2(X1,X2))
| ~ occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2)) ),
i_0_124 ).
cnf(c_0_593,plain,
( occ_fails(esk20_2(esk133_0,esk134_0),esk134_0,X1)
| gr(X1) ),
inference(spm,[status(thm)],[c_0_588,c_0_589]) ).
cnf(c_0_594,plain,
( occ_fails(esk20_2(esk133_0,esk134_0),esk133_0,X1)
| occ_succeeds(esk20_2(esk133_0,esk134_0),esk133_0,X1) ),
inference(spm,[status(thm)],[c_0_584,c_0_590]) ).
cnf(c_0_595,plain,
( ~ gr(esk22_2(esk133_0,esk134_0))
| ~ gr(esk24_2(esk133_0,esk134_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_591,c_0_590])]) ).
cnf(c_0_596,plain,
gr(esk24_2(esk133_0,esk134_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_592,c_0_593]),c_0_585]),c_0_590]),c_0_573])]),c_0_581]) ).
cnf(c_0_597,plain,
( not_same_occ_terminates(X1,X2)
| ~ member2_terminates(esk19_2(X1,X2),X1,X2)
| ~ occ_fails(esk20_2(X1,X2),X1,esk22_2(X1,X2))
| ~ occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2)) ),
i_0_125 ).
cnf(c_0_598,plain,
( occ_fails(esk20_2(esk133_0,esk134_0),esk133_0,X1)
| gr(X1) ),
inference(spm,[status(thm)],[c_0_588,c_0_594]) ).
cnf(c_0_599,plain,
~ gr(esk22_2(esk133_0,esk134_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_595,c_0_596])]) ).
cnf(c_0_600,plain,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_597,c_0_598]),c_0_590]),c_0_573])]),c_0_581]),c_0_599]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWX060+1 : TPTP v9.1.0. Released v9.1.0.
% 0.06/0.13 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % 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:25:27 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.19/0.45 # ENIGMATIC: Selected complete mode:
% 98.08/13.84 # ENIGMATIC: Solved by Enigma+tptp-cade20-model02-h2e15+lgb-t150-d30-l4800-e0.15+coop-paramils157:
% 98.08/13.84 # SinE strategy is GSinE(CountFormulas,hypos,5.0,,3,500,1.0)
% 98.08/13.84 # ENIGMA: LightGBM model '/export/starexec/sandbox/solver/bin/data/Enigma/tptp-cade20-model02-h2e15/lgb-t150-d30-l4800-e0.15/model.lgb' loaded. (hash_base: 32768; conj_feats: 25; version: 991; iters: 150)
% 98.08/13.84 # Preprocessing time : 0.748 s
% 98.08/13.84
% 98.08/13.84 # Proof found!
% 98.08/13.84 # SZS status Theorem
% 98.08/13.84 # SZS output start CNFRefutation
% See solution above
% 98.08/13.84 # Training examples: 0 positive, 0 negative
% 98.08/13.84
% 98.08/13.84 # -------------------------------------------------
% 98.08/13.84 # User time : 10.970 s
% 98.08/13.84 # System time : 0.243 s
% 98.08/13.84 # Total time : 11.213 s
% 98.08/13.84 # ...preprocessing : 0.748 s
% 98.08/13.84 # ...main loop : 10.465 s
% 98.08/13.84 # Maximum resident set size: 152912 pages
% 98.08/13.84
%------------------------------------------------------------------------------