%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SWX052+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:56 AM UTC 2025
% Result : Theorem 254.02s 33.48s
% Output : CNFRefutation 254.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 18
% Syntax : Number of clauses : 78 ( 14 unt; 48 nHn; 27 RR)
% Number of literals : 208 ( 139 equ; 53 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 134 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_558,plain,
( esk130_0 = nil
| occ(X1,X2) = occ(X1,X3)
| permutation_succeeds(esk134_0,esk133_0)
| ~ permutation_succeeds(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_558) ).
cnf(i_0_564,negated_conjecture,
permutation_succeeds(esk136_0,esk137_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_564) ).
cnf(i_0_534,plain,
( list_succeeds(X1)
| ~ permutation_succeeds(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_534) ).
cnf(i_0_533,plain,
( list_succeeds(X1)
| ~ permutation_succeeds(X2,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_533) ).
cnf(i_0_560,plain,
( esk130_0 = nil
| occ(X1,X2) = occ(X1,X3)
| delete_succeeds(esk132_0,esk130_0,esk134_0)
| ~ permutation_succeeds(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_560) ).
cnf(i_0_563,negated_conjecture,
occ(esk138_0,esk137_0) != occ(esk138_0,esk136_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_563) ).
cnf(i_0_505,plain,
( list_succeeds(X1)
| ~ list_succeeds(X2)
| ~ delete_succeeds(X3,X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_505) ).
cnf(i_0_226,plain,
( list_succeeds(X1)
| X1 != nil ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_226) ).
cnf(i_0_548,plain,
( X1 = X2
| occ(X1,cons(X2,X3)) = occ(X1,X3)
| ~ list_succeeds(X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_548) ).
cnf(i_0_562,plain,
( esk130_0 = nil
| cons(esk132_0,esk133_0) = esk131_0
| occ(X1,X2) = occ(X1,X3)
| ~ permutation_succeeds(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_562) ).
cnf(i_0_552,plain,
( X1 = X2
| occ(X2,X3) = occ(X2,X4)
| ~ list_succeeds(X3)
| ~ delete_succeeds(X1,X3,X4) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_552) ).
cnf(i_0_556,plain,
( esk130_0 = nil
| occ(X1,X2) = occ(X1,X3)
| occ(X4,esk134_0) = occ(X4,esk133_0)
| ~ permutation_succeeds(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_556) ).
cnf(i_0_554,plain,
( occ(X1,X2) = occ(X1,X3)
| occ(esk135_0,esk131_0) != occ(esk135_0,esk130_0)
| ~ permutation_succeeds(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_554) ).
cnf(i_0_549,plain,
( occ(X1,cons(X1,X2)) = s(occ(X1,X2))
| ~ list_succeeds(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_549) ).
cnf(i_0_553,plain,
( occ(X1,X2) = s(occ(X1,X3))
| ~ list_succeeds(X2)
| ~ delete_succeeds(X1,X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_553) ).
cnf(i_0_559,plain,
( esk131_0 = nil
| occ(X1,X2) = occ(X1,X3)
| delete_succeeds(esk132_0,esk130_0,esk134_0)
| ~ permutation_succeeds(X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_559) ).
cnf(i_0_547,plain,
occ(X1,nil) = '0',
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_547) ).
cnf(i_0_2,plain,
s(X1) != '0',
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-xy79ckem/input.p',i_0_2) ).
cnf(c_0_583,plain,
( esk130_0 = nil
| occ(X1,X2) = occ(X1,X3)
| permutation_succeeds(esk134_0,esk133_0)
| ~ permutation_succeeds(X2,X3) ),
i_0_558 ).
cnf(c_0_584,negated_conjecture,
permutation_succeeds(esk136_0,esk137_0),
i_0_564 ).
cnf(c_0_585,plain,
( list_succeeds(X1)
| ~ permutation_succeeds(X1,X2) ),
i_0_534 ).
cnf(c_0_586,negated_conjecture,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| esk130_0 = nil
| permutation_succeeds(esk134_0,esk133_0) ),
inference(spm,[status(thm)],[c_0_583,c_0_584]) ).
cnf(c_0_587,plain,
( list_succeeds(X1)
| ~ permutation_succeeds(X2,X1) ),
i_0_533 ).
cnf(c_0_588,plain,
( esk130_0 = nil
| occ(X1,X2) = occ(X1,X3)
| delete_succeeds(esk132_0,esk130_0,esk134_0)
| ~ permutation_succeeds(X2,X3) ),
i_0_560 ).
cnf(c_0_589,negated_conjecture,
occ(esk138_0,esk137_0) != occ(esk138_0,esk136_0),
i_0_563 ).
cnf(c_0_590,plain,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| esk130_0 = nil
| list_succeeds(esk134_0) ),
inference(spm,[status(thm)],[c_0_585,c_0_586]) ).
cnf(c_0_591,plain,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| esk130_0 = nil
| list_succeeds(esk133_0) ),
inference(spm,[status(thm)],[c_0_587,c_0_586]) ).
cnf(c_0_592,plain,
( list_succeeds(X1)
| ~ list_succeeds(X2)
| ~ delete_succeeds(X3,X1,X2) ),
i_0_505 ).
cnf(c_0_593,negated_conjecture,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| esk130_0 = nil
| delete_succeeds(esk132_0,esk130_0,esk134_0) ),
inference(spm,[status(thm)],[c_0_588,c_0_584]) ).
cnf(c_0_594,negated_conjecture,
( esk130_0 = nil
| list_succeeds(esk134_0) ),
inference(spm,[status(thm)],[c_0_589,c_0_590]) ).
cnf(c_0_595,plain,
( list_succeeds(X1)
| X1 != nil ),
i_0_226 ).
cnf(c_0_596,plain,
( X1 = X2
| occ(X1,cons(X2,X3)) = occ(X1,X3)
| ~ list_succeeds(X3) ),
i_0_548 ).
cnf(c_0_597,negated_conjecture,
( esk130_0 = nil
| list_succeeds(esk133_0) ),
inference(spm,[status(thm)],[c_0_589,c_0_591]) ).
cnf(c_0_598,plain,
( esk130_0 = nil
| cons(esk132_0,esk133_0) = esk131_0
| occ(X1,X2) = occ(X1,X3)
| ~ permutation_succeeds(X2,X3) ),
i_0_562 ).
cnf(c_0_599,plain,
( X1 = X2
| occ(X2,X3) = occ(X2,X4)
| ~ list_succeeds(X3)
| ~ delete_succeeds(X1,X3,X4) ),
i_0_552 ).
cnf(c_0_600,plain,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| list_succeeds(esk130_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_592,c_0_593]),c_0_594]),c_0_595]) ).
cnf(c_0_601,plain,
( occ(X1,cons(X2,esk133_0)) = occ(X1,esk133_0)
| esk130_0 = nil
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_596,c_0_597]) ).
cnf(c_0_602,negated_conjecture,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| cons(esk132_0,esk133_0) = esk131_0
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_598,c_0_584]) ).
cnf(c_0_603,plain,
( esk130_0 = nil
| occ(X1,X2) = occ(X1,X3)
| occ(X4,esk134_0) = occ(X4,esk133_0)
| ~ permutation_succeeds(X2,X3) ),
i_0_556 ).
cnf(c_0_604,plain,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| occ(X2,esk134_0) = occ(X2,esk130_0)
| esk130_0 = nil
| esk132_0 = X2
| ~ list_succeeds(esk130_0) ),
inference(spm,[status(thm)],[c_0_599,c_0_593]) ).
cnf(c_0_605,negated_conjecture,
list_succeeds(esk130_0),
inference(spm,[status(thm)],[c_0_589,c_0_600]) ).
cnf(c_0_606,negated_conjecture,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| occ(X2,esk131_0) = occ(X2,esk133_0)
| esk130_0 = nil
| X2 = esk132_0 ),
inference(spm,[status(thm)],[c_0_601,c_0_602]) ).
cnf(c_0_607,negated_conjecture,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| occ(X2,esk134_0) = occ(X2,esk133_0)
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_603,c_0_584]) ).
cnf(c_0_608,plain,
( occ(X1,esk134_0) = occ(X1,esk130_0)
| occ(X2,esk137_0) = occ(X2,esk136_0)
| esk130_0 = nil
| esk132_0 = X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_604,c_0_605])]) ).
cnf(c_0_609,plain,
( occ(X1,X2) = occ(X1,X3)
| occ(esk135_0,esk131_0) != occ(esk135_0,esk130_0)
| ~ permutation_succeeds(X2,X3) ),
i_0_554 ).
cnf(c_0_610,negated_conjecture,
( occ(X1,esk131_0) = occ(X1,esk133_0)
| esk130_0 = nil
| X1 = esk132_0 ),
inference(spm,[status(thm)],[c_0_589,c_0_606]) ).
cnf(c_0_611,negated_conjecture,
( occ(X1,esk134_0) = occ(X1,esk133_0)
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_589,c_0_607]) ).
cnf(c_0_612,negated_conjecture,
( occ(X1,esk134_0) = occ(X1,esk130_0)
| esk130_0 = nil
| esk132_0 = X1 ),
inference(spm,[status(thm)],[c_0_589,c_0_608]) ).
cnf(c_0_613,plain,
( occ(X1,X2) = occ(X1,X3)
| esk135_0 = esk132_0
| esk130_0 = nil
| occ(esk135_0,esk133_0) != occ(esk135_0,esk130_0)
| ~ permutation_succeeds(X2,X3) ),
inference(spm,[status(thm)],[c_0_609,c_0_610]) ).
cnf(c_0_614,negated_conjecture,
( occ(X1,esk133_0) = occ(X1,esk130_0)
| esk130_0 = nil
| esk132_0 = X1 ),
inference(spm,[status(thm)],[c_0_611,c_0_612]) ).
cnf(c_0_615,plain,
( occ(X1,X2) = occ(X1,X3)
| esk130_0 = nil
| esk135_0 = esk132_0
| ~ permutation_succeeds(X2,X3) ),
inference(spm,[status(thm)],[c_0_613,c_0_614]) ).
cnf(c_0_616,plain,
( occ(X1,cons(X1,X2)) = s(occ(X1,X2))
| ~ list_succeeds(X2) ),
i_0_549 ).
cnf(c_0_617,negated_conjecture,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| esk135_0 = esk132_0
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_615,c_0_584]) ).
cnf(c_0_618,plain,
( occ(X1,cons(X1,esk133_0)) = s(occ(X1,esk133_0))
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_616,c_0_597]) ).
cnf(c_0_619,plain,
( occ(X1,X2) = s(occ(X1,X3))
| ~ list_succeeds(X2)
| ~ delete_succeeds(X1,X2,X3) ),
i_0_553 ).
cnf(c_0_620,negated_conjecture,
( esk130_0 = nil
| esk135_0 = esk132_0 ),
inference(spm,[status(thm)],[c_0_589,c_0_617]) ).
cnf(c_0_621,negated_conjecture,
( occ(esk132_0,esk131_0) = s(occ(esk132_0,esk133_0))
| occ(X1,esk137_0) = occ(X1,esk136_0)
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_618,c_0_602]) ).
cnf(c_0_622,plain,
( s(occ(esk132_0,esk134_0)) = occ(esk132_0,esk130_0)
| occ(X1,esk137_0) = occ(X1,esk136_0)
| esk130_0 = nil ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_619,c_0_593]),c_0_605])]) ).
cnf(c_0_623,plain,
( occ(X1,X2) = occ(X1,X3)
| esk130_0 = nil
| occ(esk132_0,esk131_0) != occ(esk132_0,esk130_0)
| ~ permutation_succeeds(X2,X3) ),
inference(spm,[status(thm)],[c_0_609,c_0_620]) ).
cnf(c_0_624,negated_conjecture,
( occ(esk132_0,esk131_0) = s(occ(esk132_0,esk133_0))
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_589,c_0_621]) ).
cnf(c_0_625,negated_conjecture,
( s(occ(esk132_0,esk134_0)) = occ(esk132_0,esk130_0)
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_589,c_0_622]) ).
cnf(c_0_626,negated_conjecture,
( occ(X1,X2) = occ(X1,X3)
| esk130_0 = nil
| s(occ(esk132_0,esk133_0)) != occ(esk132_0,esk130_0)
| ~ permutation_succeeds(X2,X3) ),
inference(spm,[status(thm)],[c_0_623,c_0_624]) ).
cnf(c_0_627,negated_conjecture,
( s(occ(esk132_0,esk133_0)) = occ(esk132_0,esk130_0)
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_625,c_0_611]) ).
cnf(c_0_628,negated_conjecture,
( occ(X1,X2) = occ(X1,X3)
| esk130_0 = nil
| ~ permutation_succeeds(X2,X3) ),
inference(spm,[status(thm)],[c_0_626,c_0_627]) ).
cnf(c_0_629,negated_conjecture,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| esk130_0 = nil ),
inference(spm,[status(thm)],[c_0_628,c_0_584]) ).
cnf(c_0_630,plain,
( esk131_0 = nil
| occ(X1,X2) = occ(X1,X3)
| delete_succeeds(esk132_0,esk130_0,esk134_0)
| ~ permutation_succeeds(X2,X3) ),
i_0_559 ).
cnf(c_0_631,negated_conjecture,
esk130_0 = nil,
inference(spm,[status(thm)],[c_0_589,c_0_629]) ).
cnf(c_0_632,plain,
( occ(X1,X2) = occ(X1,X3)
| esk131_0 = nil
| delete_succeeds(esk132_0,nil,esk134_0)
| ~ permutation_succeeds(X2,X3) ),
inference(rw,[status(thm)],[c_0_630,c_0_631]) ).
cnf(c_0_633,negated_conjecture,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| esk131_0 = nil
| delete_succeeds(esk132_0,nil,esk134_0) ),
inference(spm,[status(thm)],[c_0_632,c_0_584]) ).
cnf(c_0_634,plain,
occ(X1,nil) = '0',
i_0_547 ).
cnf(c_0_635,plain,
list_succeeds(nil),
inference(er,[status(thm)],[c_0_595]) ).
cnf(c_0_636,plain,
s(X1) != '0',
i_0_2 ).
cnf(c_0_637,plain,
( occ(X1,esk137_0) = occ(X1,esk136_0)
| esk131_0 = nil ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_619,c_0_633]),c_0_634]),c_0_635])]),c_0_636]) ).
cnf(c_0_638,plain,
( occ(X1,X2) = occ(X1,X3)
| occ(esk135_0,esk131_0) != '0'
| ~ permutation_succeeds(X2,X3) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_609,c_0_631]),c_0_634]) ).
cnf(c_0_639,negated_conjecture,
esk131_0 = nil,
inference(spm,[status(thm)],[c_0_589,c_0_637]) ).
cnf(c_0_640,plain,
( occ(X1,X2) = occ(X1,X3)
| ~ permutation_succeeds(X2,X3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_638,c_0_639]),c_0_634])]) ).
cnf(c_0_641,negated_conjecture,
occ(X1,esk137_0) = occ(X1,esk136_0),
inference(spm,[status(thm)],[c_0_640,c_0_584]) ).
cnf(c_0_642,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_589,c_0_641])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWX052+1 : TPTP v9.1.0. Released v9.1.0.
% 0.11/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:06:42 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.20/0.45 # ENIGMATIC: Selected complete mode:
% 254.02/33.48 # ENIGMATIC: Solved by paramils045:
% 254.02/33.48 # Preprocessing time : 0.021 s
% 254.02/33.48
% 254.02/33.48 # Proof found!
% 254.02/33.48 # SZS status Theorem
% 254.02/33.48 # SZS output start CNFRefutation
% See solution above
% 254.02/33.48 # Training examples: 0 positive, 0 negative
% 254.02/33.48
% 254.02/33.48 # -------------------------------------------------
% 254.02/33.48 # User time : 4.522 s
% 254.02/33.48 # System time : 0.058 s
% 254.02/33.48 # Total time : 4.580 s
% 254.02/33.48 # ...preprocessing : 0.021 s
% 254.02/33.48 # ...main loop : 4.559 s
% 254.02/33.48 # Maximum resident set size: 71260 pages
% 254.02/33.48
%------------------------------------------------------------------------------