%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SWX046+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n028.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:55 AM UTC 2025
% Result : Theorem 134.41s 18.42s
% Output : CNFRefutation 134.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 38
% Syntax : Number of clauses : 139 ( 41 unt; 15 nHn; 122 RR)
% Number of literals : 293 ( 71 equ; 157 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 187 ( 20 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_173,plain,
( '@=<_succeeds'(X1,X2)
| ~ '@=<_succeeds'(X3,X2)
| ~ '@=<_succeeds'(X1,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_173) ).
cnf(i_0_200,negated_conjecture,
'@=<_succeeds'(esk43_0,esk44_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_200) ).
cnf(i_0_58,plain,
( '@=<_succeeds'(X1,X2)
| X2 != s(X3)
| X1 != s(X4)
| ~ '@=<_succeeds'(X4,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_58) ).
cnf(i_0_175,plain,
( '@=<_succeeds'(X1,s(X1))
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_175) ).
cnf(i_0_199,negated_conjecture,
nat_succeeds(esk44_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_199) ).
cnf(i_0_160,plain,
( nat_succeeds(X1)
| ~ '@=<_succeeds'(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_160) ).
cnf(i_0_57,plain,
( '@=<_succeeds'(X1,X2)
| X1 != '0' ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_57) ).
cnf(i_0_2,plain,
( X1 = X2
| s(X1) != s(X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_2) ).
cnf(i_0_94,plain,
( X1 = '0'
| s(esk28_1(X1)) = X1
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_94) ).
cnf(i_0_1,plain,
s(X1) != '0',
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_1) ).
cnf(i_0_86,plain,
( '@<_fails'(X1,X2)
| X3 != s(X2)
| X4 != s(X1)
| ~ '@<_fails'(X4,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_86) ).
cnf(i_0_103,plain,
( plus_succeeds(X1,X2,X3)
| '@+'(X1,X2) != X3
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_103) ).
cnf(i_0_120,plain,
( s('@+'(X1,X2)) = '@+'(s(X1),X2)
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_120) ).
cnf(i_0_93,plain,
( X1 = '0'
| nat_succeeds(esk28_1(X1))
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_93) ).
cnf(i_0_152,plain,
( '@<_fails'(X1,X1)
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_152) ).
cnf(i_0_112,plain,
( nat_succeeds(X1)
| ~ nat_succeeds(X2)
| ~ plus_succeeds(X3,X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_112) ).
cnf(i_0_119,plain,
'@+'('0',X1) = X1,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_119) ).
cnf(i_0_91,plain,
( nat_succeeds(X1)
| X1 != '0' ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_91) ).
cnf(i_0_96,plain,
( X1 = '0'
| s(esk29_1(X1)) = X1
| nat_fails(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_96) ).
cnf(i_0_12,plain,
( ~ '@<_succeeds'(X1,X2)
| ~ '@<_fails'(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_12) ).
cnf(i_0_198,negated_conjecture,
~ '@=<_succeeds'('@*'(esk42_0,esk43_0),'@*'(esk42_0,esk44_0)),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_198) ).
cnf(i_0_167,plain,
( '@=<_succeeds'(X1,X2)
| '@=<_succeeds'(X2,X1)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_167) ).
cnf(i_0_123,plain,
( '@+'(X1,'0') = X1
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_123) ).
cnf(i_0_124,plain,
( '@+'(s(X1),X2) = '@+'(X1,s(X2))
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_124) ).
cnf(i_0_95,plain,
( X1 = '0'
| nat_fails(X1)
| ~ nat_fails(esk29_1(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_95) ).
cnf(i_0_168,plain,
( '@=<_succeeds'(X1,X2)
| '@<_succeeds'(X2,X1)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_168) ).
cnf(i_0_136,plain,
( nat_succeeds('@*'(X1,X2))
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_136) ).
cnf(i_0_201,negated_conjecture,
nat_succeeds(esk42_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_201) ).
cnf(i_0_14,plain,
( ~ nat_succeeds(X1)
| ~ nat_fails(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_14) ).
cnf(i_0_183,plain,
( '@=<_succeeds'(X1,'@+'(X1,X2))
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_183) ).
cnf(i_0_166,plain,
( '@=<_succeeds'(X1,X1)
| ~ nat_succeeds(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_166) ).
cnf(i_0_126,plain,
( X1 = X2
| '@+'(X3,X1) != '@+'(X3,X2)
| ~ nat_succeeds(X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_126) ).
cnf(i_0_162,plain,
( '@+'(X1,esk35_2(X1,X2)) = X2
| ~ '@=<_succeeds'(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_162) ).
cnf(i_0_181,plain,
( '@=<_succeeds'('@+'(X1,X2),'@+'(X1,X3))
| ~ nat_succeeds(X1)
| ~ '@=<_succeeds'(X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_181) ).
cnf(i_0_102,plain,
( '@+'(X1,X2) = X3
| ~ nat_succeeds(X1)
| ~ plus_succeeds(X1,X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_102) ).
cnf(i_0_110,plain,
( nat_succeeds(X1)
| ~ plus_succeeds(X1,X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_110) ).
cnf(i_0_144,plain,
( '@+'('@*'(X1,X2),'@*'(X1,X3)) = '@*'(X1,'@+'(X2,X3))
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X3)
| ~ nat_succeeds(X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_144) ).
cnf(i_0_161,plain,
( plus_succeeds(X1,esk34_2(X1,X2),X2)
| ~ '@=<_succeeds'(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-c6a1n808/input.p',i_0_161) ).
cnf(c_0_240,plain,
( '@=<_succeeds'(X1,X2)
| ~ '@=<_succeeds'(X3,X2)
| ~ '@=<_succeeds'(X1,X3) ),
i_0_173 ).
cnf(c_0_241,negated_conjecture,
'@=<_succeeds'(esk43_0,esk44_0),
i_0_200 ).
cnf(c_0_242,negated_conjecture,
( '@=<_succeeds'(esk43_0,X1)
| ~ '@=<_succeeds'(esk44_0,X1) ),
inference(spm,[status(thm)],[c_0_240,c_0_241]) ).
cnf(c_0_243,plain,
( '@=<_succeeds'(X1,X2)
| X2 != s(X3)
| X1 != s(X4)
| ~ '@=<_succeeds'(X4,X3) ),
i_0_58 ).
cnf(c_0_244,plain,
( '@=<_succeeds'(esk43_0,X1)
| ~ '@=<_succeeds'(esk44_0,X2)
| ~ '@=<_succeeds'(X2,X1) ),
inference(spm,[status(thm)],[c_0_242,c_0_240]) ).
cnf(c_0_245,plain,
( '@=<_succeeds'(X1,s(X1))
| ~ nat_succeeds(X1) ),
i_0_175 ).
cnf(c_0_246,negated_conjecture,
nat_succeeds(esk44_0),
i_0_199 ).
cnf(c_0_247,plain,
( nat_succeeds(X1)
| ~ '@=<_succeeds'(X1,X2) ),
i_0_160 ).
cnf(c_0_248,plain,
( '@=<_succeeds'(s(X1),s(X2))
| ~ '@=<_succeeds'(X1,X2) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_243])]) ).
cnf(c_0_249,plain,
( '@=<_succeeds'(X1,X2)
| X1 != '0' ),
i_0_57 ).
cnf(c_0_250,plain,
( '@=<_succeeds'(esk43_0,X1)
| ~ '@=<_succeeds'(s(esk44_0),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_244,c_0_245]),c_0_246])]) ).
cnf(c_0_251,plain,
( X1 = X2
| s(X1) != s(X2) ),
i_0_2 ).
cnf(c_0_252,plain,
( X1 = '0'
| s(esk28_1(X1)) = X1
| ~ nat_succeeds(X1) ),
i_0_94 ).
cnf(c_0_253,plain,
s(X1) != '0',
i_0_1 ).
cnf(c_0_254,plain,
( nat_succeeds(s(X1))
| ~ '@=<_succeeds'(X1,X2) ),
inference(spm,[status(thm)],[c_0_247,c_0_248]) ).
cnf(c_0_255,plain,
'@=<_succeeds'('0',X1),
inference(er,[status(thm)],[c_0_249]) ).
cnf(c_0_256,plain,
( '@<_fails'(X1,X2)
| X3 != s(X2)
| X4 != s(X1)
| ~ '@<_fails'(X4,X3) ),
i_0_86 ).
cnf(c_0_257,plain,
( '@=<_succeeds'(esk43_0,s(X1))
| ~ '@=<_succeeds'(esk44_0,X1) ),
inference(spm,[status(thm)],[c_0_250,c_0_248]) ).
cnf(c_0_258,plain,
( plus_succeeds(X1,X2,X3)
| '@+'(X1,X2) != X3
| ~ nat_succeeds(X1) ),
i_0_103 ).
cnf(c_0_259,plain,
( s('@+'(X1,X2)) = '@+'(s(X1),X2)
| ~ nat_succeeds(X1) ),
i_0_120 ).
cnf(c_0_260,plain,
( X1 = '0'
| nat_succeeds(esk28_1(X1))
| ~ nat_succeeds(X1) ),
i_0_93 ).
cnf(c_0_261,plain,
( esk28_1(s(X1)) = X1
| ~ nat_succeeds(s(X1)) ),
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_251,c_0_252])]),c_0_253]) ).
cnf(c_0_262,plain,
nat_succeeds(s('0')),
inference(spm,[status(thm)],[c_0_254,c_0_255]) ).
cnf(c_0_263,plain,
( '@<_fails'(X1,X2)
| ~ '@<_fails'(s(X1),s(X2)) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_256])]) ).
cnf(c_0_264,plain,
( '@<_fails'(X1,X1)
| ~ nat_succeeds(X1) ),
i_0_152 ).
cnf(c_0_265,plain,
'@=<_succeeds'(esk43_0,s(s(esk44_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_257,c_0_245]),c_0_246])]) ).
cnf(c_0_266,plain,
( nat_succeeds(X1)
| ~ nat_succeeds(X2)
| ~ plus_succeeds(X3,X1,X2) ),
i_0_112 ).
cnf(c_0_267,plain,
( plus_succeeds(X1,X2,'@+'(X1,X2))
| ~ nat_succeeds(X1) ),
inference(er,[status(thm)],[c_0_258]) ).
cnf(c_0_268,plain,
( s('@+'(esk28_1(X1),X2)) = '@+'(X1,X2)
| X1 = '0'
| ~ nat_succeeds(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_259,c_0_252]),c_0_260]) ).
cnf(c_0_269,plain,
esk28_1(s('0')) = '0',
inference(spm,[status(thm)],[c_0_261,c_0_262]) ).
cnf(c_0_270,plain,
'@+'('0',X1) = X1,
i_0_119 ).
cnf(c_0_271,plain,
( '@<_fails'(X1,X1)
| ~ nat_succeeds(s(X1)) ),
inference(spm,[status(thm)],[c_0_263,c_0_264]) ).
cnf(c_0_272,plain,
nat_succeeds(s(esk43_0)),
inference(spm,[status(thm)],[c_0_254,c_0_265]) ).
cnf(c_0_273,plain,
( nat_succeeds(X1)
| X1 != '0' ),
i_0_91 ).
cnf(c_0_274,plain,
( nat_succeeds(X1)
| ~ nat_succeeds('@+'(X2,X1))
| ~ nat_succeeds(X2) ),
inference(spm,[status(thm)],[c_0_266,c_0_267]) ).
cnf(c_0_275,plain,
'@+'(s('0'),X1) = s(X1),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_268,c_0_269]),c_0_270]),c_0_262])]),c_0_253]) ).
cnf(c_0_276,plain,
( X1 = '0'
| s(esk29_1(X1)) = X1
| nat_fails(X1) ),
i_0_96 ).
cnf(c_0_277,plain,
( ~ '@<_succeeds'(X1,X2)
| ~ '@<_fails'(X1,X2) ),
i_0_12 ).
cnf(c_0_278,plain,
'@<_fails'(esk43_0,esk43_0),
inference(spm,[status(thm)],[c_0_271,c_0_272]) ).
cnf(c_0_279,negated_conjecture,
~ '@=<_succeeds'('@*'(esk42_0,esk43_0),'@*'(esk42_0,esk44_0)),
i_0_198 ).
cnf(c_0_280,plain,
( '@=<_succeeds'(X1,X2)
| '@=<_succeeds'(X2,X1)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2) ),
i_0_167 ).
cnf(c_0_281,plain,
( '@+'(X1,'0') = X1
| ~ nat_succeeds(X1) ),
i_0_123 ).
cnf(c_0_282,plain,
( '@+'(s(X1),X2) = '@+'(X1,s(X2))
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1) ),
i_0_124 ).
cnf(c_0_283,plain,
nat_succeeds('0'),
inference(er,[status(thm)],[c_0_273]) ).
cnf(c_0_284,plain,
( nat_succeeds(X1)
| ~ nat_succeeds(s(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_274,c_0_275]),c_0_262])]) ).
cnf(c_0_285,plain,
( X1 = '0'
| nat_fails(X1)
| ~ nat_fails(esk29_1(X1)) ),
i_0_95 ).
cnf(c_0_286,plain,
( esk29_1(s(X1)) = X1
| nat_fails(s(X1)) ),
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_251,c_0_276])]),c_0_253]) ).
cnf(c_0_287,plain,
~ '@<_succeeds'(esk43_0,esk43_0),
inference(spm,[status(thm)],[c_0_277,c_0_278]) ).
cnf(c_0_288,plain,
( '@=<_succeeds'(X1,X2)
| '@<_succeeds'(X2,X1)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2) ),
i_0_168 ).
cnf(c_0_289,negated_conjecture,
nat_succeeds(esk43_0),
inference(spm,[status(thm)],[c_0_247,c_0_241]) ).
cnf(c_0_290,negated_conjecture,
( '@=<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk43_0))
| ~ nat_succeeds('@*'(esk42_0,esk44_0))
| ~ nat_succeeds('@*'(esk42_0,esk43_0)) ),
inference(spm,[status(thm)],[c_0_279,c_0_280]) ).
cnf(c_0_291,plain,
( nat_succeeds('@*'(X1,X2))
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1) ),
i_0_136 ).
cnf(c_0_292,negated_conjecture,
nat_succeeds(esk42_0),
i_0_201 ).
cnf(c_0_293,plain,
( '@+'(X1,s('0')) = s(X1)
| ~ nat_succeeds(s(X1)) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_281,c_0_282]),c_0_283])]),c_0_284]) ).
cnf(c_0_294,plain,
( ~ nat_succeeds(X1)
| ~ nat_fails(X1) ),
i_0_14 ).
cnf(c_0_295,plain,
( nat_fails(s(X1))
| ~ nat_fails(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_285,c_0_286]),c_0_253]) ).
cnf(c_0_296,plain,
( nat_succeeds(s(s(X1)))
| ~ '@=<_succeeds'(X1,X2) ),
inference(spm,[status(thm)],[c_0_254,c_0_248]) ).
cnf(c_0_297,plain,
'@=<_succeeds'(esk43_0,esk43_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_287,c_0_288]),c_0_289])]) ).
cnf(c_0_298,negated_conjecture,
( ~ '@=<_succeeds'(X1,'@*'(esk42_0,esk44_0))
| ~ '@=<_succeeds'('@*'(esk42_0,esk43_0),X1) ),
inference(spm,[status(thm)],[c_0_279,c_0_240]) ).
cnf(c_0_299,plain,
( '@=<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk43_0))
| ~ nat_succeeds('@*'(esk42_0,esk43_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_290,c_0_291]),c_0_246]),c_0_292])]) ).
cnf(c_0_300,plain,
'@+'(esk43_0,s('0')) = s(esk43_0),
inference(spm,[status(thm)],[c_0_293,c_0_272]) ).
cnf(c_0_301,plain,
( '@+'(X1,s(X2)) = s('@+'(X1,X2))
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2) ),
inference(spm,[status(thm)],[c_0_259,c_0_282]) ).
cnf(c_0_302,plain,
esk28_1(s(esk43_0)) = esk43_0,
inference(spm,[status(thm)],[c_0_261,c_0_272]) ).
cnf(c_0_303,plain,
( esk28_1(X1) = esk29_1(X1)
| X1 = '0'
| ~ nat_succeeds(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_261,c_0_276]),c_0_294]) ).
cnf(c_0_304,plain,
( ~ nat_fails(X1)
| ~ nat_succeeds(s(X1)) ),
inference(spm,[status(thm)],[c_0_294,c_0_295]) ).
cnf(c_0_305,plain,
nat_succeeds(s(s(esk43_0))),
inference(spm,[status(thm)],[c_0_296,c_0_297]) ).
cnf(c_0_306,plain,
( ~ '@=<_succeeds'('@*'(esk42_0,esk43_0),X1)
| ~ '@=<_succeeds'(X2,'@*'(esk42_0,esk44_0))
| ~ '@=<_succeeds'(X1,X2) ),
inference(spm,[status(thm)],[c_0_298,c_0_240]) ).
cnf(c_0_307,plain,
( '@=<_succeeds'(X1,'@+'(X1,X2))
| ~ nat_succeeds(X1) ),
i_0_183 ).
cnf(c_0_308,plain,
'@=<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk43_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_299,c_0_291]),c_0_289]),c_0_292])]) ).
cnf(c_0_309,plain,
s('@+'(esk43_0,'0')) = s(esk43_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_300,c_0_301]),c_0_289]),c_0_283])]) ).
cnf(c_0_310,plain,
esk29_1(s(esk43_0)) = esk43_0,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_302,c_0_303]),c_0_272])]),c_0_253]) ).
cnf(c_0_311,plain,
~ nat_fails(s(esk43_0)),
inference(spm,[status(thm)],[c_0_304,c_0_305]) ).
cnf(c_0_312,plain,
( ~ '@=<_succeeds'('@+'('@*'(esk42_0,esk43_0),X1),X2)
| ~ '@=<_succeeds'(X2,'@*'(esk42_0,esk44_0))
| ~ nat_succeeds('@*'(esk42_0,esk43_0)) ),
inference(spm,[status(thm)],[c_0_306,c_0_307]) ).
cnf(c_0_313,plain,
( '@=<_succeeds'(X1,X1)
| ~ nat_succeeds(X1) ),
i_0_166 ).
cnf(c_0_314,plain,
nat_succeeds('@*'(esk42_0,esk44_0)),
inference(spm,[status(thm)],[c_0_247,c_0_308]) ).
cnf(c_0_315,plain,
nat_succeeds(s('@*'(esk42_0,esk44_0))),
inference(spm,[status(thm)],[c_0_254,c_0_308]) ).
cnf(c_0_316,plain,
( X1 = X2
| '@+'(X3,X1) != '@+'(X3,X2)
| ~ nat_succeeds(X3) ),
i_0_126 ).
cnf(c_0_317,plain,
( '@+'(X1,esk35_2(X1,X2)) = X2
| ~ '@=<_succeeds'(X1,X2) ),
i_0_162 ).
cnf(c_0_318,plain,
( '@=<_succeeds'('@+'(X1,X2),'@+'(X1,X3))
| ~ nat_succeeds(X1)
| ~ '@=<_succeeds'(X2,X3) ),
i_0_181 ).
cnf(c_0_319,plain,
'@+'(esk43_0,'0') = esk43_0,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_286,c_0_309]),c_0_310]),c_0_311]) ).
cnf(c_0_320,plain,
( '@+'(X1,X2) = X3
| ~ nat_succeeds(X1)
| ~ plus_succeeds(X1,X2,X3) ),
i_0_102 ).
cnf(c_0_321,plain,
( nat_succeeds(X1)
| ~ plus_succeeds(X1,X2,X3) ),
i_0_110 ).
cnf(c_0_322,plain,
( ~ '@=<_succeeds'('@+'('@*'(esk42_0,esk43_0),X1),'@*'(esk42_0,esk44_0))
| ~ nat_succeeds('@*'(esk42_0,esk43_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_312,c_0_313]),c_0_314])]) ).
cnf(c_0_323,plain,
( '@+'('@*'(X1,X2),'@*'(X1,X3)) = '@*'(X1,'@+'(X2,X3))
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X3)
| ~ nat_succeeds(X2) ),
i_0_144 ).
cnf(c_0_324,plain,
'@<_fails'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk44_0)),
inference(spm,[status(thm)],[c_0_271,c_0_315]) ).
cnf(c_0_325,plain,
( esk35_2(X1,'@+'(X1,X2)) = X2
| ~ '@=<_succeeds'(X1,'@+'(X1,X2)) ),
inference(csr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_316,c_0_317])]),c_0_247]) ).
cnf(c_0_326,plain,
'@=<_succeeds'(esk43_0,'@+'(esk43_0,X1)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_318,c_0_319]),c_0_255]),c_0_289])]) ).
cnf(c_0_327,plain,
( '@+'(X1,X2) = X3
| ~ plus_succeeds(X1,X2,X3) ),
inference(csr,[status(thm)],[c_0_320,c_0_321]) ).
cnf(c_0_328,plain,
( plus_succeeds(X1,esk34_2(X1,X2),X2)
| ~ '@=<_succeeds'(X1,X2) ),
i_0_161 ).
cnf(c_0_329,plain,
( ~ '@=<_succeeds'('@*'(esk42_0,'@+'(esk43_0,X1)),'@*'(esk42_0,esk44_0))
| ~ nat_succeeds('@*'(esk42_0,esk43_0))
| ~ nat_succeeds(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_322,c_0_323]),c_0_289]),c_0_292])]) ).
cnf(c_0_330,plain,
~ '@<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk44_0)),
inference(spm,[status(thm)],[c_0_277,c_0_324]) ).
cnf(c_0_331,plain,
esk35_2(esk43_0,'@+'(esk43_0,X1)) = X1,
inference(spm,[status(thm)],[c_0_325,c_0_326]) ).
cnf(c_0_332,plain,
( '@+'(X1,esk34_2(X1,X2)) = X2
| ~ '@=<_succeeds'(X1,X2) ),
inference(spm,[status(thm)],[c_0_327,c_0_328]) ).
cnf(c_0_333,plain,
( ~ '@=<_succeeds'('@*'(esk42_0,X1),'@*'(esk42_0,esk44_0))
| ~ '@=<_succeeds'(esk43_0,X1)
| ~ nat_succeeds('@*'(esk42_0,esk43_0))
| ~ nat_succeeds(esk35_2(esk43_0,X1)) ),
inference(spm,[status(thm)],[c_0_329,c_0_317]) ).
cnf(c_0_334,plain,
'@=<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk44_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_330,c_0_288]),c_0_314])]) ).
cnf(c_0_335,plain,
( esk34_2(esk43_0,X1) = esk35_2(esk43_0,X1)
| ~ '@=<_succeeds'(esk43_0,X1) ),
inference(spm,[status(thm)],[c_0_331,c_0_332]) ).
cnf(c_0_336,negated_conjecture,
( ~ nat_succeeds('@*'(esk42_0,esk43_0))
| ~ nat_succeeds(esk35_2(esk43_0,esk44_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_333,c_0_241]),c_0_334])]) ).
cnf(c_0_337,plain,
( nat_succeeds(esk34_2(X1,X2))
| ~ '@=<_succeeds'(X1,X2)
| ~ nat_succeeds(X2) ),
inference(spm,[status(thm)],[c_0_266,c_0_328]) ).
cnf(c_0_338,negated_conjecture,
esk34_2(esk43_0,esk44_0) = esk35_2(esk43_0,esk44_0),
inference(spm,[status(thm)],[c_0_335,c_0_241]) ).
cnf(c_0_339,plain,
~ nat_succeeds(esk35_2(esk43_0,esk44_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_336,c_0_291]),c_0_289]),c_0_292])]) ).
cnf(c_0_340,plain,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_337,c_0_338]),c_0_241]),c_0_246])]),c_0_339]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWX046+1 : TPTP v9.1.0. Released v9.1.0.
% 0.11/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n028.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:53:21 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.18/0.44 # ENIGMATIC: Selected complete mode:
% 134.41/18.42 # ENIGMATIC: Solved by autoschedule:
% 134.41/18.42 # No SInE strategy applied
% 134.41/18.42 # Trying AutoSched0 for 150 seconds
% 134.41/18.42 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S07FN
% 134.41/18.42 # and selection function SelectCQArNXTEqFirst.
% 134.41/18.42 #
% 134.41/18.42 # Preprocessing time : 0.031 s
% 134.41/18.42 # Presaturation interreduction done
% 134.41/18.42
% 134.41/18.42 # Proof found!
% 134.41/18.42 # SZS status Theorem
% 134.41/18.42 # SZS output start CNFRefutation
% See solution above
% 134.41/18.42 # Training examples: 0 positive, 0 negative
% 134.41/18.42
% 134.41/18.42 # -------------------------------------------------
% 134.41/18.42 # User time : 15.469 s
% 134.41/18.42 # System time : 0.391 s
% 134.41/18.42 # Total time : 15.859 s
% 134.41/18.42 # Maximum resident set size: 7124 pages
% 134.41/18.42
%------------------------------------------------------------------------------