%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SWX029+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n002.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:54 AM UTC 2025
% Result : Theorem 107.05s 15.05s
% Output : CNFRefutation 107.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 33
% Syntax : Number of clauses : 122 ( 49 unt; 18 nHn; 110 RR)
% Number of literals : 231 ( 95 equ; 104 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-3 aty)
% Number of variables : 151 ( 40 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_736,plain,
( lh(X1) = '@+'(lh(X2),lh(X3))
| ~ split_succeeds(X1,X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_736) ).
cnf(i_0_738,negated_conjecture,
split_succeeds(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_738) ).
cnf(i_0_81,plain,
( '@=<_succeeds'(X1,'@+'(X1,X2))
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_81) ).
cnf(i_0_743,plain,
( list_succeeds(X1)
| ~ split_succeeds(X2,X1,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_743) ).
cnf(i_0_742,plain,
( list_succeeds(X1)
| ~ split_succeeds(X2,X3,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_742) ).
cnf(i_0_124,plain,
( nat_succeeds(lh(X1))
| ~ list_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_124) ).
cnf(i_0_35,plain,
( '@+'(lh(X1),lh(X2)) = lh('**'(X1,X2))
| ~ list_succeeds(X2)
| ~ list_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_35) ).
cnf(i_0_509,plain,
( X1 = nil
| cons(esk99_3(X1,X2,X3),esk101_3(X1,X2,X3)) = X2
| ~ split_succeeds(X1,X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_509) ).
cnf(i_0_586,plain,
cons(X1,X2) != nil,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_586) ).
cnf(i_0_6,plain,
( plus_succeeds(X1,X2,X3)
| '@+'(X1,X2) != X3
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_6) ).
cnf(i_0_93,plain,
( nat_succeeds(X1)
| ~ '@=<_succeeds'(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_93) ).
cnf(i_0_37,plain,
( '@=<_succeeds'(lh(X1),lh('**'(X2,X1)))
| ~ list_succeeds(X1)
| ~ list_succeeds(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_37) ).
cnf(i_0_671,plain,
( X1 = X2
| cons(X3,X1) != cons(X4,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_671) ).
cnf(i_0_270,plain,
( X1 = nil
| cons(esk40_1(X1),esk41_1(X1)) = X1
| ~ list_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_270) ).
cnf(i_0_404,plain,
s(X1) != '0',
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_404) ).
cnf(i_0_118,plain,
( lh(cons(X1,X2)) = s(lh(X2))
| ~ list_succeeds(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_118) ).
cnf(i_0_505,plain,
( X1 = nil
| split_succeeds(esk100_3(X2,X1,X3),X3,esk101_3(X2,X1,X3))
| ~ split_succeeds(X2,X1,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_505) ).
cnf(i_0_201,plain,
( nat_succeeds(X1)
| ~ nat_succeeds(X2)
| ~ plus_succeeds(X3,X2,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_201) ).
cnf(i_0_107,plain,
( '@<_succeeds'(X1,'@+'(X1,s(X2)))
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_107) ).
cnf(i_0_374,plain,
( X1 = '0'
| s(esk79_1(X1)) = X1
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_374) ).
cnf(i_0_75,plain,
( X1 = X2
| '@<_succeeds'(X1,X2)
| ~ nat_succeeds(X2)
| ~ '@=<_succeeds'(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_75) ).
cnf(i_0_371,plain,
( nat_succeeds(X1)
| X1 != '0' ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_371) ).
cnf(i_0_737,negated_conjecture,
( ~ '@<_succeeds'(lh(esk190_0),lh(cons(esk187_0,cons(esk188_0,esk189_0))))
| ~ '@<_succeeds'(lh(esk191_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_737) ).
cnf(i_0_187,plain,
( X1 = X2
| '@+'(X1,X3) != '@+'(X2,X3)
| ~ nat_succeeds(X3)
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_187) ).
cnf(i_0_206,plain,
'@+'('0',X1) = X1,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_206) ).
cnf(i_0_697,plain,
( delete_succeeds(X1,X2,X3)
| X2 != cons(X1,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_697) ).
cnf(i_0_744,plain,
( list_succeeds(X1)
| ~ split_succeeds(X1,X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_744) ).
cnf(i_0_129,plain,
( list_succeeds(X1)
| ~ list_succeeds(cons(X2,X1)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_129) ).
cnf(i_0_437,plain,
( X1 = X2
| s(X1) != s(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_437) ).
cnf(i_0_52,plain,
( lh(X1) = s(lh(X2))
| ~ list_succeeds(X1)
| ~ delete_succeeds(X3,X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_52) ).
cnf(i_0_125,plain,
( X1 = nil
| lh(X1) != '0'
| ~ list_succeeds(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_125) ).
cnf(i_0_507,plain,
( X1 = nil
| cons(esk99_3(X2,X3,X1),esk101_3(X2,X3,X1)) = X3
| ~ split_succeeds(X2,X3,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_507) ).
cnf(i_0_122,plain,
lh(nil) = '0',
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-x4nrgyjp/input.p',i_0_122) ).
cnf(c_0_778,plain,
( lh(X1) = '@+'(lh(X2),lh(X3))
| ~ split_succeeds(X1,X2,X3) ),
i_0_736 ).
cnf(c_0_779,negated_conjecture,
split_succeeds(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0),
i_0_738 ).
cnf(c_0_780,plain,
( '@=<_succeeds'(X1,'@+'(X1,X2))
| ~ nat_succeeds(X1) ),
i_0_81 ).
cnf(c_0_781,negated_conjecture,
'@+'(lh(esk190_0),lh(esk191_0)) = lh(cons(esk187_0,cons(esk188_0,esk189_0))),
inference(spm,[status(thm)],[c_0_778,c_0_779]) ).
cnf(c_0_782,plain,
( list_succeeds(X1)
| ~ split_succeeds(X2,X1,X3) ),
i_0_743 ).
cnf(c_0_783,plain,
( list_succeeds(X1)
| ~ split_succeeds(X2,X3,X1) ),
i_0_742 ).
cnf(c_0_784,plain,
( '@=<_succeeds'(lh(esk190_0),lh(cons(esk187_0,cons(esk188_0,esk189_0))))
| ~ nat_succeeds(lh(esk190_0)) ),
inference(spm,[status(thm)],[c_0_780,c_0_781]) ).
cnf(c_0_785,plain,
( nat_succeeds(lh(X1))
| ~ list_succeeds(X1) ),
i_0_124 ).
cnf(c_0_786,negated_conjecture,
list_succeeds(esk190_0),
inference(spm,[status(thm)],[c_0_782,c_0_779]) ).
cnf(c_0_787,plain,
( '@+'(lh(X1),lh(X2)) = lh('**'(X1,X2))
| ~ list_succeeds(X2)
| ~ list_succeeds(X1) ),
i_0_35 ).
cnf(c_0_788,negated_conjecture,
list_succeeds(esk191_0),
inference(spm,[status(thm)],[c_0_783,c_0_779]) ).
cnf(c_0_789,plain,
( X1 = nil
| cons(esk99_3(X1,X2,X3),esk101_3(X1,X2,X3)) = X2
| ~ split_succeeds(X1,X2,X3) ),
i_0_509 ).
cnf(c_0_790,plain,
cons(X1,X2) != nil,
i_0_586 ).
cnf(c_0_791,plain,
( plus_succeeds(X1,X2,X3)
| '@+'(X1,X2) != X3
| ~ nat_succeeds(X1) ),
i_0_6 ).
cnf(c_0_792,plain,
( nat_succeeds(X1)
| ~ '@=<_succeeds'(X1,X2) ),
i_0_93 ).
cnf(c_0_793,plain,
'@=<_succeeds'(lh(esk190_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_784,c_0_785]),c_0_786])]) ).
cnf(c_0_794,plain,
( '@=<_succeeds'(lh(X1),lh('**'(X2,X1)))
| ~ list_succeeds(X1)
| ~ list_succeeds(X2) ),
i_0_37 ).
cnf(c_0_795,plain,
lh('**'(esk190_0,esk191_0)) = lh(cons(esk187_0,cons(esk188_0,esk189_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_787,c_0_781]),c_0_788]),c_0_786])]) ).
cnf(c_0_796,negated_conjecture,
cons(esk99_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0),esk101_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0)) = esk190_0,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_789,c_0_779]),c_0_790]) ).
cnf(c_0_797,plain,
( X1 = X2
| cons(X3,X1) != cons(X4,X2) ),
i_0_671 ).
cnf(c_0_798,plain,
( X1 = nil
| cons(esk40_1(X1),esk41_1(X1)) = X1
| ~ list_succeeds(X1) ),
i_0_270 ).
cnf(c_0_799,plain,
( plus_succeeds(X1,X2,'@+'(X1,X2))
| ~ nat_succeeds(X1) ),
inference(er,[status(thm)],[c_0_791]) ).
cnf(c_0_800,plain,
nat_succeeds(lh(esk190_0)),
inference(spm,[status(thm)],[c_0_792,c_0_793]) ).
cnf(c_0_801,plain,
'@=<_succeeds'(lh(esk191_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_794,c_0_795]),c_0_786]),c_0_788])]) ).
cnf(c_0_802,plain,
s(X1) != '0',
i_0_404 ).
cnf(c_0_803,plain,
( lh(cons(X1,X2)) = s(lh(X2))
| ~ list_succeeds(X2) ),
i_0_118 ).
cnf(c_0_804,plain,
( X1 = nil
| split_succeeds(esk100_3(X2,X1,X3),X3,esk101_3(X2,X1,X3))
| ~ split_succeeds(X2,X1,X3) ),
i_0_505 ).
cnf(c_0_805,plain,
esk190_0 != nil,
inference(spm,[status(thm)],[c_0_790,c_0_796]) ).
cnf(c_0_806,plain,
( esk41_1(cons(X1,X2)) = X2
| ~ list_succeeds(cons(X1,X2)) ),
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_797,c_0_798])]),c_0_790]) ).
cnf(c_0_807,plain,
( nat_succeeds(X1)
| ~ nat_succeeds(X2)
| ~ plus_succeeds(X3,X2,X1) ),
i_0_201 ).
cnf(c_0_808,negated_conjecture,
plus_succeeds(lh(esk190_0),lh(esk191_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_799,c_0_781]),c_0_800])]) ).
cnf(c_0_809,plain,
nat_succeeds(lh(esk191_0)),
inference(spm,[status(thm)],[c_0_792,c_0_801]) ).
cnf(c_0_810,plain,
( lh(cons(X1,X2)) != '0'
| ~ list_succeeds(X2) ),
inference(spm,[status(thm)],[c_0_802,c_0_803]) ).
cnf(c_0_811,negated_conjecture,
split_succeeds(esk100_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0),esk191_0,esk101_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_804,c_0_779]),c_0_805]) ).
cnf(c_0_812,negated_conjecture,
esk101_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0) = esk41_1(esk190_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_806,c_0_796]),c_0_786])]) ).
cnf(c_0_813,plain,
( '@<_succeeds'(X1,'@+'(X1,s(X2)))
| ~ nat_succeeds(X1) ),
i_0_107 ).
cnf(c_0_814,plain,
( X1 = '0'
| s(esk79_1(X1)) = X1
| ~ nat_succeeds(X1) ),
i_0_374 ).
cnf(c_0_815,plain,
( X1 = X2
| '@<_succeeds'(X1,X2)
| ~ nat_succeeds(X2)
| ~ '@=<_succeeds'(X1,X2) ),
i_0_75 ).
cnf(c_0_816,plain,
nat_succeeds(lh(cons(esk187_0,cons(esk188_0,esk189_0)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_807,c_0_808]),c_0_809])]) ).
cnf(c_0_817,plain,
( nat_succeeds(X1)
| X1 != '0' ),
i_0_371 ).
cnf(c_0_818,plain,
( lh(esk190_0) != '0'
| ~ list_succeeds(esk101_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0)) ),
inference(spm,[status(thm)],[c_0_810,c_0_796]) ).
cnf(c_0_819,negated_conjecture,
split_succeeds(esk100_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0),esk191_0,esk41_1(esk190_0)),
inference(rw,[status(thm)],[c_0_811,c_0_812]) ).
cnf(c_0_820,plain,
( X1 = '0'
| '@<_succeeds'(X2,'@+'(X2,X1))
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1) ),
inference(spm,[status(thm)],[c_0_813,c_0_814]) ).
cnf(c_0_821,negated_conjecture,
( ~ '@<_succeeds'(lh(esk190_0),lh(cons(esk187_0,cons(esk188_0,esk189_0))))
| ~ '@<_succeeds'(lh(esk191_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))) ),
i_0_737 ).
cnf(c_0_822,plain,
( lh(cons(esk187_0,cons(esk188_0,esk189_0))) = lh(esk190_0)
| '@<_succeeds'(lh(esk190_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_815,c_0_793]),c_0_816])]) ).
cnf(c_0_823,plain,
( X1 = X2
| '@+'(X1,X3) != '@+'(X2,X3)
| ~ nat_succeeds(X3)
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1) ),
i_0_187 ).
cnf(c_0_824,plain,
'@+'('0',X1) = X1,
i_0_206 ).
cnf(c_0_825,plain,
nat_succeeds('0'),
inference(er,[status(thm)],[c_0_817]) ).
cnf(c_0_826,plain,
( lh(esk190_0) != '0'
| ~ list_succeeds(esk41_1(esk190_0)) ),
inference(rw,[status(thm)],[c_0_818,c_0_812]) ).
cnf(c_0_827,plain,
list_succeeds(esk41_1(esk190_0)),
inference(spm,[status(thm)],[c_0_783,c_0_819]) ).
cnf(c_0_828,plain,
( delete_succeeds(X1,X2,X3)
| X2 != cons(X1,X3) ),
i_0_697 ).
cnf(c_0_829,negated_conjecture,
( lh(esk191_0) = '0'
| '@<_succeeds'(lh(esk190_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_820,c_0_781]),c_0_800]),c_0_809])]) ).
cnf(c_0_830,negated_conjecture,
( lh(cons(esk187_0,cons(esk188_0,esk189_0))) = lh(esk190_0)
| ~ '@<_succeeds'(lh(esk191_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))) ),
inference(spm,[status(thm)],[c_0_821,c_0_822]) ).
cnf(c_0_831,plain,
( lh(cons(esk187_0,cons(esk188_0,esk189_0))) = lh(esk191_0)
| '@<_succeeds'(lh(esk191_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_815,c_0_801]),c_0_816])]) ).
cnf(c_0_832,plain,
( X1 = '0'
| '@+'(X1,X2) != X2
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_823,c_0_824]),c_0_825])]) ).
cnf(c_0_833,plain,
lh(esk190_0) != '0',
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_826,c_0_827])]) ).
cnf(c_0_834,plain,
( list_succeeds(X1)
| ~ split_succeeds(X1,X2,X3) ),
i_0_744 ).
cnf(c_0_835,plain,
delete_succeeds(X1,cons(X1,X2),X2),
inference(er,[status(thm)],[c_0_828]) ).
cnf(c_0_836,negated_conjecture,
( lh(esk191_0) = '0'
| ~ '@<_succeeds'(lh(esk191_0),lh(cons(esk187_0,cons(esk188_0,esk189_0)))) ),
inference(spm,[status(thm)],[c_0_821,c_0_829]) ).
cnf(c_0_837,negated_conjecture,
( lh(cons(esk187_0,cons(esk188_0,esk189_0))) = lh(esk190_0)
| lh(cons(esk187_0,cons(esk188_0,esk189_0))) = lh(esk191_0) ),
inference(spm,[status(thm)],[c_0_830,c_0_831]) ).
cnf(c_0_838,negated_conjecture,
lh(cons(esk187_0,cons(esk188_0,esk189_0))) != lh(esk191_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_832,c_0_781]),c_0_809]),c_0_800])]),c_0_833]) ).
cnf(c_0_839,plain,
( list_succeeds(X1)
| ~ list_succeeds(cons(X2,X1)) ),
i_0_129 ).
cnf(c_0_840,negated_conjecture,
list_succeeds(cons(esk187_0,cons(esk188_0,esk189_0))),
inference(spm,[status(thm)],[c_0_834,c_0_779]) ).
cnf(c_0_841,plain,
delete_succeeds(esk99_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0),esk190_0,esk101_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0)),
inference(spm,[status(thm)],[c_0_835,c_0_796]) ).
cnf(c_0_842,plain,
( lh(cons(esk187_0,cons(esk188_0,esk189_0))) = lh(esk191_0)
| lh(esk191_0) = '0' ),
inference(spm,[status(thm)],[c_0_836,c_0_831]) ).
cnf(c_0_843,plain,
( lh(cons(X1,X2)) = lh(cons(X3,X2))
| ~ list_succeeds(X2) ),
inference(spm,[status(thm)],[c_0_803,c_0_803]) ).
cnf(c_0_844,negated_conjecture,
lh(cons(esk187_0,cons(esk188_0,esk189_0))) = lh(esk190_0),
inference(sr,[status(thm)],[c_0_837,c_0_838]) ).
cnf(c_0_845,plain,
list_succeeds(cons(esk188_0,esk189_0)),
inference(spm,[status(thm)],[c_0_839,c_0_840]) ).
cnf(c_0_846,plain,
( X1 = X2
| s(X1) != s(X2) ),
i_0_437 ).
cnf(c_0_847,plain,
( lh(X1) = s(lh(X2))
| ~ list_succeeds(X1)
| ~ delete_succeeds(X3,X1,X2) ),
i_0_52 ).
cnf(c_0_848,plain,
delete_succeeds(esk99_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,esk191_0),esk190_0,esk41_1(esk190_0)),
inference(rw,[status(thm)],[c_0_841,c_0_812]) ).
cnf(c_0_849,plain,
( X1 = nil
| lh(X1) != '0'
| ~ list_succeeds(X1) ),
i_0_125 ).
cnf(c_0_850,plain,
lh(esk191_0) = '0',
inference(sr,[status(thm)],[c_0_842,c_0_838]) ).
cnf(c_0_851,plain,
lh(cons(X1,cons(esk188_0,esk189_0))) = lh(esk190_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_843,c_0_844]),c_0_845])]) ).
cnf(c_0_852,plain,
( esk79_1(s(X1)) = X1
| ~ nat_succeeds(s(X1)) ),
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_846,c_0_814])]),c_0_802]) ).
cnf(c_0_853,plain,
s(lh(esk41_1(esk190_0))) = lh(esk190_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_847,c_0_848]),c_0_786])]) ).
cnf(c_0_854,plain,
esk191_0 = nil,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_849,c_0_850]),c_0_788])]) ).
cnf(c_0_855,plain,
esk41_1(cons(esk188_0,esk189_0)) = esk189_0,
inference(spm,[status(thm)],[c_0_806,c_0_845]) ).
cnf(c_0_856,plain,
s(lh(cons(esk188_0,esk189_0))) = lh(esk190_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_803,c_0_851]),c_0_845])]) ).
cnf(c_0_857,plain,
esk79_1(lh(esk190_0)) = lh(esk41_1(esk190_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_852,c_0_853]),c_0_800])]) ).
cnf(c_0_858,plain,
( X1 = nil
| cons(esk99_3(X2,X3,X1),esk101_3(X2,X3,X1)) = X3
| ~ split_succeeds(X2,X3,X1) ),
i_0_507 ).
cnf(c_0_859,negated_conjecture,
split_succeeds(esk100_3(cons(esk187_0,cons(esk188_0,esk189_0)),esk190_0,nil),nil,esk41_1(esk190_0)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_819,c_0_854]),c_0_854]) ).
cnf(c_0_860,plain,
cons(esk40_1(cons(esk188_0,esk189_0)),esk189_0) = cons(esk188_0,esk189_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_798,c_0_855]),c_0_845])]),c_0_790]) ).
cnf(c_0_861,plain,
list_succeeds(esk189_0),
inference(spm,[status(thm)],[c_0_839,c_0_845]) ).
cnf(c_0_862,plain,
lh(esk41_1(esk190_0)) = lh(cons(esk188_0,esk189_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_852,c_0_856]),c_0_857]),c_0_800])]) ).
cnf(c_0_863,plain,
esk41_1(esk190_0) = nil,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_858,c_0_859]),c_0_790]) ).
cnf(c_0_864,plain,
lh(nil) = '0',
i_0_122 ).
cnf(c_0_865,plain,
lh(cons(esk188_0,esk189_0)) != '0',
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_810,c_0_860]),c_0_861])]) ).
cnf(c_0_866,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_862,c_0_863]),c_0_864]),c_0_865]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWX029+1 : TPTP v9.1.0. Released v9.1.0.
% 0.03/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n002.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.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Mar 31 14:14:28 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.46 # ENIGMATIC: Selected SinE mode:
% 0.19/0.48 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.48 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.19/0.48 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.19/0.48 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 107.05/15.05 # ENIGMATIC: Solved by Enigma+tptp-cade20-model03-h2e15+lgb-t150-d30-l6400-e0.15+coop-eprover66:
% 107.05/15.05 # ENIGMA: LightGBM model '/export/starexec/sandbox/solver/bin/data/Enigma/tptp-cade20-model03-h2e15/lgb-t150-d30-l6400-e0.15/model.lgb' loaded. (hash_base: 32768; conj_feats: 43; version: 991; iters: 150)
% 107.05/15.05 # Preprocessing time : 0.924 s
% 107.05/15.05 # Presaturation interreduction done
% 107.05/15.05
% 107.05/15.05 # Proof found!
% 107.05/15.05 # SZS status Theorem
% 107.05/15.05 # SZS output start CNFRefutation
% See solution above
% 107.05/15.05 # Training examples: 0 positive, 0 negative
% 107.05/15.05
% 107.05/15.05 # -------------------------------------------------
% 107.05/15.05 # User time : 12.179 s
% 107.05/15.05 # System time : 0.206 s
% 107.05/15.05 # Total time : 12.385 s
% 107.05/15.05 # ...preprocessing : 0.924 s
% 107.05/15.05 # ...main loop : 11.460 s
% 107.05/15.05 # Maximum resident set size: 169816 pages
% 107.05/15.05
%------------------------------------------------------------------------------