%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SWX047+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:14:25 PM UTC 2026
% Result : Theorem 98.80s 16.74s
% Output : CNFRefutation 98.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 45
% Syntax : Number of formulae : 226 ( 56 unt; 0 def)
% Number of atoms : 632 ( 184 equ)
% Maximal formula atoms : 25 ( 2 avg)
% Number of connectives : 675 ( 269 ~; 285 |; 73 &)
% ( 10 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 8 usr; 2 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-2 aty)
% Number of variables : 375 ( 13 sgn 212 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof('lemma-(times:less:second)',conjecture,
! [X18,X19,X20] :
( ( nat_succeeds(X20)
& '@<_succeeds'(X19,X20)
& X18 != '0'
& nat_succeeds(X18) )
=> '@<_succeeds'('@*'(X18,X19),'@*'(X18,X20)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(times:less:second)') ).
fof('theorem-(less:totality)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> ( '@<_succeeds'(X19,X18)
| X18 = X19
| '@<_succeeds'(X18,X19) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem-(less:totality)') ).
fof('corollary-(times:types)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> nat_succeeds('@*'(X18,X19)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(times:types)') ).
fof('lemma-(less:types)',axiom,
! [X18,X19] :
( '@<_succeeds'(X18,X19)
=> nat_succeeds(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(less:types)') ).
fof('lemma-(less:leq)',axiom,
! [X18,X19] :
( '@<_succeeds'(X18,X19)
=> '@=<_succeeds'(X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(less:leq)') ).
fof('lemma-(plus:injective:second)',axiom,
! [X18,X19,X20] :
( ( '@+'(X18,X19) = '@+'(X18,X20)
& nat_succeeds(X18) )
=> X19 = X20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(plus:injective:second)') ).
fof('lemma-(plus:zero)',axiom,
! [X18] :
( nat_succeeds(X18)
=> '@+'(X18,'0') = X18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(plus:zero)') ).
fof('corollary-(less:plus)',axiom,
! [X18,X19] :
( '@<_succeeds'(X18,X19)
=> ? [X20] : '@+'(X18,s(X20)) = X19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(less:plus)') ).
fof(id1,axiom,
! [X1] : '0' != s(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id1) ).
fof('(@+)/2',axiom,
! [X18,X19,X20] :
( nat_succeeds(X18)
=> ( '@+'(X18,X19) = X20
<=> plus_succeeds(X18,X19,X20) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','(@+)/2') ).
fof('corollary-(leq:plus)',axiom,
! [X18,X19] :
( '@=<_succeeds'(X18,X19)
=> ? [X20] : '@+'(X18,X20) = X19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(leq:plus)') ).
fof('theorem-(leq:antisymmetric)',axiom,
! [X18,X19] :
( ( '@=<_succeeds'(X19,X18)
& '@=<_succeeds'(X18,X19) )
=> X18 = X19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem-(leq:antisymmetric)') ).
fof('corollary-(leq:plus:first)',axiom,
! [X18,X19] :
( nat_succeeds(X18)
=> '@=<_succeeds'(X18,'@+'(X18,X19)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(leq:plus:first)') ).
fof('(@*)/2',axiom,
! [X18,X19,X20] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> ( '@*'(X18,X19) = X20
<=> times_succeeds(X18,X19,X20) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','(@*)/2') ).
fof('lemma-(times:leq:second)',axiom,
! [X18,X19,X20] :
( ( nat_succeeds(X20)
& '@=<_succeeds'(X19,X20)
& nat_succeeds(X18) )
=> '@=<_succeeds'('@*'(X18,X19),'@*'(X18,X20)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(times:leq:second)') ).
fof('theorem-(leq:totality)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> ( '@=<_succeeds'(X19,X18)
| '@=<_succeeds'(X18,X19) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem-(leq:totality)') ).
fof(id27,axiom,
! [X16] :
( nat_succeeds(X16)
<=> ( X16 = '0'
| ? [X17] :
( nat_succeeds(X17)
& X16 = s(X17) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id27) ).
fof('theorem-(plus:commutative)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> '@+'(X18,X19) = '@+'(X19,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem-(plus:commutative)') ).
fof('lemma-(plus:types:3)',axiom,
! [X18,X19,X20] :
( ( nat_succeeds(X20)
& plus_succeeds(X18,X19,X20) )
=> nat_succeeds(X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(plus:types:3)') ).
fof(id24,axiom,
! [X16,X17] :
( '@<_succeeds'(X16,X17)
<=> ( ? [X3] :
( X17 = s(X3)
& X16 = '0' )
| ? [X1,X2] :
( '@<_succeeds'(X1,X2)
& X17 = s(X2)
& X16 = s(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id24) ).
fof('lemma-(less:successor)',axiom,
! [X18,X19] :
( '@<_succeeds'(X18,X19)
=> ? [X20] : X19 = s(X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(less:successor)') ).
fof('theorem-(times:commutative)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> '@*'(X18,X19) = '@*'(X19,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem-(times:commutative)') ).
fof('theorem-(times:associative)',axiom,
! [X18,X19,X20] :
( ( nat_succeeds(X20)
& nat_succeeds(X19)
& nat_succeeds(X18) )
=> '@*'('@*'(X18,X19),X20) = '@*'(X18,'@*'(X19,X20)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem-(times:associative)') ).
fof('corollary-(times:zero)',axiom,
! [X19] :
( nat_succeeds(X19)
=> '@*'('0',X19) = '0' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(times:zero)') ).
fof('lemma-(plus:types:1)',axiom,
! [X18,X19,X20] :
( plus_succeeds(X18,X19,X20)
=> nat_succeeds(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(plus:types:1)') ).
fof('lemma-(times:types:1)',axiom,
! [X18,X19,X20] :
( times_succeeds(X18,X19,X20)
=> nat_succeeds(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(times:types:1)') ).
fof('lemma-(leq:plus:inverse)',axiom,
! [X18,X19,X20] :
( ( '@=<_succeeds'('@+'(X18,X19),'@+'(X18,X20))
& nat_succeeds(X18) )
=> '@=<_succeeds'(X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(leq:plus:inverse)') ).
fof('theorem-(leq:reflexive)',axiom,
! [X18] :
( nat_succeeds(X18)
=> '@=<_succeeds'(X18,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem-(leq:reflexive)') ).
fof(id28,axiom,
! [X16] :
( nat_fails(X16)
<=> ( X16 != '0'
& ! [X17] :
( nat_fails(X17)
| X16 != s(X17) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id28) ).
fof('lemma-(times:successor)',axiom,
! [X19,X18] :
( ( nat_succeeds(X18)
& nat_succeeds(X19) )
=> '@+'('@*'(X19,X18),X19) = '@*'(X19,s(X18)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(times:successor)') ).
fof(id25,axiom,
! [X16,X17] :
( '@<_fails'(X16,X17)
<=> ( ! [X3] :
( X17 != s(X3)
| X16 != '0' )
& ! [X1,X2] :
( '@<_fails'(X1,X2)
| X17 != s(X2)
| X16 != s(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id25) ).
fof(id29,axiom,
! [X16] :
( nat_terminates(X16)
<=> ( $true
& ! [X17] :
( ( nat_terminates(X17)
| X16 != s(X17) )
& $true ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id29) ).
fof(id2,axiom,
! [X2,X3] :
( s(X2) = s(X3)
=> X2 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id2) ).
fof('lemma-(times:one)',axiom,
! [X18] :
( nat_succeeds(X18)
=> '@*'(s('0'),X18) = X18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(times:one)') ).
fof('corollary-(plus:zero)',axiom,
! [X19] : '@+'('0',X19) = X19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(plus:zero)') ).
fof('corollary-(times:successor)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> '@*'(s(X18),X19) = '@+'(X19,'@*'(X18,X19)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(times:successor)') ).
fof('lemma-(less:plus:inverse)',axiom,
! [X18,X19,X20] :
( ( '@<_succeeds'('@+'(X18,X19),'@+'(X18,X20))
& nat_succeeds(X18) )
=> '@<_succeeds'(X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(less:plus:inverse)') ).
fof('corollary-(plus:successor)',axiom,
! [X18,X19] :
( nat_succeeds(X18)
=> '@+'(s(X18),X19) = s('@+'(X18,X19)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(plus:successor)') ).
fof(id11,axiom,
! [X13,X14] :
~ ( '@<_fails'(X13,X14)
& '@<_succeeds'(X13,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id11) ).
fof('lemma-(nat:termination)',axiom,
! [X18] :
( nat_succeeds(X18)
=> nat_terminates(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(nat:termination)') ).
fof(id13,axiom,
! [X15] :
~ ( nat_fails(X15)
& nat_succeeds(X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id13) ).
fof('corollary-(leq:plus:second)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> '@=<_succeeds'(X19,'@+'(X18,X19)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(leq:plus:second)') ).
fof('lemma-(plus:successor)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> '@+'(X18,s(X19)) = '@+'(s(X18),X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(plus:successor)') ).
fof(id14,axiom,
! [X15] :
( nat_terminates(X15)
=> ( nat_fails(X15)
| nat_succeeds(X15) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id14) ).
fof('corollary-(less:leq:total)',axiom,
! [X18,X19] :
( ( nat_succeeds(X19)
& nat_succeeds(X18) )
=> ( '@=<_succeeds'(X19,X18)
| '@<_succeeds'(X18,X19) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(less:leq:total)') ).
fof(c_0_45,negated_conjecture,
~ ! [X18,X19,X20] :
( ( nat_succeeds(X20)
& '@<_succeeds'(X19,X20)
& X18 != '0'
& nat_succeeds(X18) )
=> '@<_succeeds'('@*'(X18,X19),'@*'(X18,X20)) ),
inference(assume_negation,[status(cth)],['lemma-(times:less:second)']) ).
fof(c_0_46,negated_conjecture,
~ ! [X18,X19,X20] :
( ( nat_succeeds(X20)
& '@<_succeeds'(X19,X20)
& X18 != '0'
& nat_succeeds(X18) )
=> '@<_succeeds'('@*'(X18,X19),'@*'(X18,X20)) ),
inference(fof_simplification,[status(thm)],[c_0_45]) ).
fof(c_0_47,negated_conjecture,
( ~ '@<_succeeds'('@*'(esk42_0,esk43_0),'@*'(esk42_0,esk44_0))
& nat_succeeds(esk44_0)
& '@<_succeeds'(esk43_0,esk44_0)
& esk42_0 != '0'
& nat_succeeds(esk42_0) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_46])])])]) ).
fof(c_0_48,plain,
! [X300,X301] :
( '@<_succeeds'(X301,X300)
| X300 = X301
| '@<_succeeds'(X300,X301)
| ~ nat_succeeds(X301)
| ~ nat_succeeds(X300) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['theorem-(less:totality)'])])]) ).
cnf(c_0_49,negated_conjecture,
~ '@<_succeeds'('@*'(esk42_0,esk43_0),'@*'(esk42_0,esk44_0)),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_50,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@<_succeeds'(X2,X1)
| X1 = X2
| '@<_succeeds'(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
fof(c_0_51,plain,
! [X260,X261] :
( nat_succeeds('@*'(X260,X261))
| ~ nat_succeeds(X261)
| ~ nat_succeeds(X260) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(times:types)'])])]) ).
fof(c_0_52,plain,
! [X282,X283] :
( nat_succeeds(X282)
| ~ '@<_succeeds'(X282,X283) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(less:types)'])])]) ).
fof(c_0_53,plain,
! [X321,X322] :
( '@=<_succeeds'(X321,X322)
| ~ '@<_succeeds'(X321,X322) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(less:leq)'])])]) ).
cnf(c_0_54,negated_conjecture,
( ~ nat_succeeds('@*'(esk42_0,esk43_0))
| ~ nat_succeeds('@*'(esk42_0,esk44_0))
| '@<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk43_0))
| '@*'(esk42_0,esk43_0) = '@*'(esk42_0,esk44_0) ),
inference(spm,[status(thm)],[c_0_49,c_0_50]) ).
cnf(c_0_55,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| nat_succeeds('@*'(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_56,negated_conjecture,
nat_succeeds(esk44_0),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_57,negated_conjecture,
nat_succeeds(esk42_0),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_58,plain,
( ~ '@<_succeeds'(X1,X2)
| nat_succeeds(X1) ),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
cnf(c_0_59,negated_conjecture,
'@<_succeeds'(esk43_0,esk44_0),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
fof(c_0_60,plain,
! [X232,X233,X234] :
( X233 = X234
| '@+'(X232,X233) != '@+'(X232,X234)
| ~ nat_succeeds(X232) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(plus:injective:second)'])])]) ).
fof(c_0_61,plain,
! [X227] :
( '@+'(X227,'0') = X227
| ~ nat_succeeds(X227) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(plus:zero)'])])]) ).
fof(c_0_62,plain,
! [X318,X319] :
( '@+'(X318,s(esk37_2(X318,X319))) = X319
| ~ '@<_succeeds'(X318,X319) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(less:plus)'])])])]) ).
fof(c_0_63,plain,
! [X1] : '0' != s(X1),
inference(fof_simplification,[status(thm)],[id1]) ).
fof(c_0_64,plain,
! [X177,X178,X179] :
( ( ~ nat_succeeds(X177)
| '@+'(X177,X178) = X179
| ~ plus_succeeds(X177,X178,X179) )
& ( ~ nat_succeeds(X177)
| plus_succeeds(X177,X178,X179)
| '@+'(X177,X178) != X179 ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['(@+)/2'])])])]) ).
fof(c_0_65,plain,
! [X312,X313] :
( '@+'(X312,esk35_2(X312,X313)) = X313
| ~ '@=<_succeeds'(X312,X313) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(leq:plus)'])])])]) ).
cnf(c_0_66,plain,
( ~ '@<_succeeds'(X1,X2)
| '@=<_succeeds'(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
cnf(c_0_67,negated_conjecture,
( ~ nat_succeeds('@*'(esk42_0,esk43_0))
| '@<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk43_0))
| '@*'(esk42_0,esk43_0) = '@*'(esk42_0,esk44_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_56]),c_0_57])]) ).
cnf(c_0_68,negated_conjecture,
nat_succeeds(esk43_0),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
fof(c_0_69,plain,
! [X341,X342] :
( X341 = X342
| ~ '@=<_succeeds'(X342,X341)
| ~ '@=<_succeeds'(X341,X342) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['theorem-(leq:antisymmetric)'])])]) ).
fof(c_0_70,plain,
! [X361,X362] :
( '@=<_succeeds'(X361,'@+'(X361,X362))
| ~ nat_succeeds(X361) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(leq:plus:first)'])])]) ).
cnf(c_0_71,plain,
( '@+'(X1,X2) != '@+'(X1,X3)
| ~ nat_succeeds(X1)
| X2 = X3 ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_72,plain,
( ~ nat_succeeds(X1)
| '@+'(X1,'0') = X1 ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
cnf(c_0_73,plain,
( ~ '@<_succeeds'(X1,X2)
| '@+'(X1,s(esk37_2(X1,X2))) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
fof(c_0_74,plain,
! [X25] : '0' != s(X25),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_63])]) ).
cnf(c_0_75,plain,
( ~ nat_succeeds(X1)
| '@+'(X1,X2) != X3
| plus_succeeds(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_76,plain,
( ~ '@=<_succeeds'(X1,X2)
| '@+'(X1,esk35_2(X1,X2)) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
cnf(c_0_77,negated_conjecture,
'@=<_succeeds'(esk43_0,esk44_0),
inference(spm,[status(thm)],[c_0_66,c_0_59]) ).
fof(c_0_78,plain,
! [X180,X181,X182] :
( ( ~ nat_succeeds(X181)
| ~ nat_succeeds(X180)
| '@*'(X180,X181) = X182
| ~ times_succeeds(X180,X181,X182) )
& ( ~ nat_succeeds(X181)
| ~ nat_succeeds(X180)
| times_succeeds(X180,X181,X182)
| '@*'(X180,X181) != X182 ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['(@*)/2'])])])]) ).
cnf(c_0_79,negated_conjecture,
( '@<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk43_0))
| '@*'(esk42_0,esk43_0) = '@*'(esk42_0,esk44_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_55]),c_0_68]),c_0_57])]) ).
fof(c_0_80,plain,
! [X390,X391,X392] :
( '@=<_succeeds'('@*'(X390,X391),'@*'(X390,X392))
| ~ nat_succeeds(X392)
| ~ '@=<_succeeds'(X391,X392)
| ~ nat_succeeds(X390) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(times:leq:second)'])])]) ).
fof(c_0_81,plain,
! [X324,X325] :
( '@=<_succeeds'(X325,X324)
| '@=<_succeeds'(X324,X325)
| ~ nat_succeeds(X325)
| ~ nat_succeeds(X324) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['theorem-(leq:totality)'])])]) ).
cnf(c_0_82,plain,
( ~ '@=<_succeeds'(X2,X1)
| ~ '@=<_succeeds'(X1,X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
cnf(c_0_83,plain,
( ~ nat_succeeds(X1)
| '@=<_succeeds'(X1,'@+'(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_84,plain,
( ~ nat_succeeds(X2)
| '@+'(X2,X1) != X2
| X1 = '0' ),
inference(spm,[status(thm)],[c_0_71,c_0_72]) ).
cnf(c_0_85,negated_conjecture,
'@+'(esk43_0,s(esk37_2(esk43_0,esk44_0))) = esk44_0,
inference(spm,[status(thm)],[c_0_73,c_0_59]) ).
cnf(c_0_86,plain,
'0' != s(X1),
inference(split_conjunct,[status(thm)],[c_0_74]) ).
fof(c_0_87,plain,
! [X165,X167,X168] :
( ( nat_succeeds(X167)
| X167 != '0' )
& ( nat_succeeds(X167)
| ~ nat_succeeds(X168)
| X167 != s(X168) )
& ( ~ nat_succeeds(X165)
| X165 = '0'
| nat_succeeds(esk28_1(X165)) )
& ( ~ nat_succeeds(X165)
| X165 = '0'
| X165 = s(esk28_1(X165)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[id27])])])])])])]) ).
fof(c_0_88,plain,
! [X230,X231] :
( '@+'(X230,X231) = '@+'(X231,X230)
| ~ nat_succeeds(X231)
| ~ nat_succeeds(X230) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['theorem-(plus:commutative)'])])]) ).
fof(c_0_89,plain,
! [X197,X198,X199] :
( nat_succeeds(X198)
| ~ nat_succeeds(X199)
| ~ plus_succeeds(X197,X198,X199) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(plus:types:3)'])])]) ).
cnf(c_0_90,plain,
( ~ nat_succeeds(X1)
| plus_succeeds(X1,X2,'@+'(X1,X2)) ),
inference(er,[status(thm)],[c_0_75]) ).
cnf(c_0_91,negated_conjecture,
'@+'(esk43_0,esk35_2(esk43_0,esk44_0)) = esk44_0,
inference(spm,[status(thm)],[c_0_76,c_0_77]) ).
fof(c_0_92,plain,
! [X137,X138,X142,X143,X144,X145,X146] :
( ( '@<_succeeds'(X142,X143)
| X143 != s(X146)
| X142 != '0' )
& ( '@<_succeeds'(X142,X143)
| ~ '@<_succeeds'(X144,X145)
| X143 != s(X145)
| X142 != s(X144) )
& ( ~ '@<_succeeds'(X137,X138)
| '@<_succeeds'(esk20_2(X137,X138),esk21_2(X137,X138))
| X138 = s(esk22_2(X137,X138)) )
& ( ~ '@<_succeeds'(X137,X138)
| '@<_succeeds'(esk20_2(X137,X138),esk21_2(X137,X138))
| X137 = '0' )
& ( ~ '@<_succeeds'(X137,X138)
| X138 = s(esk21_2(X137,X138))
| X138 = s(esk22_2(X137,X138)) )
& ( ~ '@<_succeeds'(X137,X138)
| X138 = s(esk21_2(X137,X138))
| X137 = '0' )
& ( ~ '@<_succeeds'(X137,X138)
| X137 = s(esk20_2(X137,X138))
| X138 = s(esk22_2(X137,X138)) )
& ( ~ '@<_succeeds'(X137,X138)
| X137 = s(esk20_2(X137,X138))
| X137 = '0' ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[id24])])])])])])]) ).
fof(c_0_93,plain,
! [X284,X285] :
( X285 = s(esk33_2(X284,X285))
| ~ '@<_succeeds'(X284,X285) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(less:successor)'])])])]) ).
cnf(c_0_94,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@*'(X1,X2) != X3
| times_succeeds(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_78]) ).
fof(c_0_95,plain,
! [X271,X272] :
( '@*'(X271,X272) = '@*'(X272,X271)
| ~ nat_succeeds(X272)
| ~ nat_succeeds(X271) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['theorem-(times:commutative)'])])]) ).
cnf(c_0_96,negated_conjecture,
( '@=<_succeeds'('@*'(esk42_0,esk44_0),'@*'(esk42_0,esk43_0))
| '@*'(esk42_0,esk43_0) = '@*'(esk42_0,esk44_0) ),
inference(spm,[status(thm)],[c_0_66,c_0_79]) ).
cnf(c_0_97,plain,
( ~ nat_succeeds(X3)
| ~ '@=<_succeeds'(X2,X3)
| ~ nat_succeeds(X1)
| '@=<_succeeds'('@*'(X1,X2),'@*'(X1,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_80]) ).
cnf(c_0_98,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@=<_succeeds'(X2,X1)
| '@=<_succeeds'(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_81]) ).
cnf(c_0_99,plain,
( ~ '@=<_succeeds'('@+'(X1,X2),X1)
| ~ nat_succeeds(X1)
| '@+'(X1,X2) = X1 ),
inference(spm,[status(thm)],[c_0_82,c_0_83]) ).
cnf(c_0_100,negated_conjecture,
esk43_0 != esk44_0,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84,c_0_85]),c_0_68])]),c_0_86]) ).
fof(c_0_101,plain,
! [X265,X266,X267] :
( '@*'('@*'(X265,X266),X267) = '@*'(X265,'@*'(X266,X267))
| ~ nat_succeeds(X267)
| ~ nat_succeeds(X266)
| ~ nat_succeeds(X265) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['theorem-(times:associative)'])])]) ).
fof(c_0_102,plain,
! [X257] :
( '@*'('0',X257) = '0'
| ~ nat_succeeds(X257) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(times:zero)'])])]) ).
cnf(c_0_103,plain,
( X1 != '0'
| nat_succeeds(X1) ),
inference(split_conjunct,[status(thm)],[c_0_87]) ).
fof(c_0_104,plain,
! [X191,X192,X193] :
( nat_succeeds(X191)
| ~ plus_succeeds(X191,X192,X193) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(plus:types:1)'])])]) ).
cnf(c_0_105,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@+'(X1,X2) = '@+'(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
cnf(c_0_106,plain,
( ~ nat_succeeds(X3)
| ~ plus_succeeds(X1,X2,X3)
| nat_succeeds(X2) ),
inference(split_conjunct,[status(thm)],[c_0_89]) ).
cnf(c_0_107,negated_conjecture,
plus_succeeds(esk43_0,esk35_2(esk43_0,esk44_0),esk44_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_91]),c_0_68])]) ).
cnf(c_0_108,plain,
( X2 != s(X3)
| X1 != '0'
| '@<_succeeds'(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_92]) ).
cnf(c_0_109,plain,
( ~ '@<_succeeds'(X1,X2)
| X2 = s(esk33_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_93]) ).
fof(c_0_110,plain,
! [X235,X236,X237] :
( nat_succeeds(X235)
| ~ times_succeeds(X235,X236,X237) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(times:types:1)'])])]) ).
cnf(c_0_111,plain,
( ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| times_succeeds(X1,X2,'@*'(X1,X2)) ),
inference(er,[status(thm)],[c_0_94]) ).
cnf(c_0_112,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@*'(X1,X2) = '@*'(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_95]) ).
cnf(c_0_113,negated_conjecture,
( ~ '@=<_succeeds'('@*'(esk42_0,esk43_0),'@*'(esk42_0,esk44_0))
| '@*'(esk42_0,esk43_0) = '@*'(esk42_0,esk44_0) ),
inference(spm,[status(thm)],[c_0_82,c_0_96]) ).
cnf(c_0_114,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X3)
| '@=<_succeeds'(X3,X2)
| '@=<_succeeds'('@*'(X1,X2),'@*'(X1,X3)) ),
inference(spm,[status(thm)],[c_0_97,c_0_98]) ).
cnf(c_0_115,negated_conjecture,
~ '@=<_succeeds'(esk44_0,esk43_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_99,c_0_85]),c_0_68])]),c_0_100]) ).
cnf(c_0_116,plain,
( ~ nat_succeeds(X3)
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@*'('@*'(X1,X2),X3) = '@*'(X1,'@*'(X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_101]) ).
cnf(c_0_117,plain,
( ~ nat_succeeds(X1)
| '@*'('0',X1) = '0' ),
inference(split_conjunct,[status(thm)],[c_0_102]) ).
cnf(c_0_118,plain,
nat_succeeds('0'),
inference(er,[status(thm)],[c_0_103]) ).
fof(c_0_119,plain,
! [X371,X372,X373] :
( '@=<_succeeds'(X372,X373)
| ~ '@=<_succeeds'('@+'(X371,X372),'@+'(X371,X373))
| ~ nat_succeeds(X371) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(leq:plus:inverse)'])])]) ).
fof(c_0_120,plain,
! [X323] :
( '@=<_succeeds'(X323,X323)
| ~ nat_succeeds(X323) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['theorem-(leq:reflexive)'])])]) ).
cnf(c_0_121,plain,
( ~ nat_succeeds(X1)
| ~ plus_succeeds(X1,X2,X3)
| '@+'(X1,X2) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_122,plain,
( ~ plus_succeeds(X1,X2,X3)
| nat_succeeds(X1) ),
inference(split_conjunct,[status(thm)],[c_0_104]) ).
cnf(c_0_123,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| plus_succeeds(X1,X2,'@+'(X2,X1)) ),
inference(spm,[status(thm)],[c_0_90,c_0_105]) ).
cnf(c_0_124,negated_conjecture,
nat_succeeds(esk35_2(esk43_0,esk44_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_107]),c_0_56])]) ).
cnf(c_0_125,plain,
( ~ '@<_succeeds'(X2,X4)
| X3 != s(X4)
| X1 != s(X2)
| '@<_succeeds'(X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_92]) ).
cnf(c_0_126,plain,
'@<_succeeds'('0',s(X1)),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_108])]) ).
cnf(c_0_127,negated_conjecture,
s(esk33_2(esk43_0,esk44_0)) = esk44_0,
inference(spm,[status(thm)],[c_0_109,c_0_59]) ).
cnf(c_0_128,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| ~ times_succeeds(X1,X2,X3)
| '@*'(X1,X2) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_78]) ).
cnf(c_0_129,plain,
( ~ times_succeeds(X1,X2,X3)
| nat_succeeds(X1) ),
inference(split_conjunct,[status(thm)],[c_0_110]) ).
cnf(c_0_130,plain,
( ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| times_succeeds(X1,X2,'@*'(X2,X1)) ),
inference(spm,[status(thm)],[c_0_111,c_0_112]) ).
cnf(c_0_131,negated_conjecture,
'@*'(esk42_0,esk43_0) = '@*'(esk42_0,esk44_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_113,c_0_114]),c_0_56]),c_0_57]),c_0_68])]),c_0_115]) ).
cnf(c_0_132,plain,
( ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| '@*'('0','@*'(X1,X2)) = '@*'('0',X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_116,c_0_117]),c_0_118])]) ).
cnf(c_0_133,plain,
( ~ '@=<_succeeds'('@+'(X1,X2),'@+'(X1,X3))
| ~ nat_succeeds(X1)
| '@=<_succeeds'(X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_119]) ).
cnf(c_0_134,plain,
( ~ nat_succeeds(X1)
| '@=<_succeeds'(X1,X1) ),
inference(split_conjunct,[status(thm)],[c_0_120]) ).
cnf(c_0_135,plain,
( ~ plus_succeeds(X1,X2,X3)
| '@+'(X1,X2) = X3 ),
inference(csr,[status(thm)],[c_0_121,c_0_122]) ).
cnf(c_0_136,negated_conjecture,
plus_succeeds(esk35_2(esk43_0,esk44_0),esk43_0,esk44_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123,c_0_91]),c_0_124]),c_0_68])]) ).
fof(c_0_137,plain,
! [X16] :
( nat_fails(X16)
<=> ( X16 != '0'
& ! [X17] :
( nat_fails(X17)
| X16 != s(X17) ) ) ),
inference(fof_simplification,[status(thm)],[id28]) ).
cnf(c_0_138,plain,
( ~ '@<_succeeds'(X1,X2)
| '@<_succeeds'(s(X1),s(X2)) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_125])]) ).
cnf(c_0_139,negated_conjecture,
'@<_succeeds'('0',esk44_0),
inference(spm,[status(thm)],[c_0_126,c_0_127]) ).
fof(c_0_140,plain,
! [X269,X270] :
( '@+'('@*'(X269,X270),X269) = '@*'(X269,s(X270))
| ~ nat_succeeds(X270)
| ~ nat_succeeds(X269) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(times:successor)'])])]) ).
cnf(c_0_141,plain,
( ~ times_succeeds(X1,X2,X3)
| ~ nat_succeeds(X2)
| '@*'(X1,X2) = X3 ),
inference(csr,[status(thm)],[c_0_128,c_0_129]) ).
cnf(c_0_142,negated_conjecture,
times_succeeds(esk43_0,esk42_0,'@*'(esk42_0,esk44_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_131]),c_0_57]),c_0_68])]) ).
cnf(c_0_143,negated_conjecture,
'@*'('0','@*'(esk42_0,esk44_0)) = '@*'('0',esk43_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_132,c_0_131]),c_0_68]),c_0_57])]) ).
cnf(c_0_144,negated_conjecture,
nat_succeeds('@*'(esk42_0,esk44_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_131]),c_0_68]),c_0_57])]) ).
cnf(c_0_145,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds('@+'(X2,X1))
| '@=<_succeeds'(X1,X1) ),
inference(spm,[status(thm)],[c_0_133,c_0_134]) ).
cnf(c_0_146,negated_conjecture,
'@+'(esk35_2(esk43_0,esk44_0),esk43_0) = esk44_0,
inference(spm,[status(thm)],[c_0_135,c_0_136]) ).
fof(c_0_147,plain,
! [X16,X17] :
( '@<_fails'(X16,X17)
<=> ( ! [X3] :
( X17 != s(X3)
| X16 != '0' )
& ! [X1,X2] :
( '@<_fails'(X1,X2)
| X17 != s(X2)
| X16 != s(X1) ) ) ),
inference(fof_simplification,[status(thm)],[id25]) ).
fof(c_0_148,plain,
! [X16] :
( nat_terminates(X16)
<=> ( $true
& ! [X17] :
( ( nat_terminates(X17)
| X16 != s(X17) )
& $true ) ) ),
inference(fof_simplification,[status(thm)],[id29]) ).
fof(c_0_149,plain,
! [X26,X27] :
( X26 = X27
| s(X26) != s(X27) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[id2])])]) ).
fof(c_0_150,plain,
! [X169,X170,X171] :
( ( nat_fails(X171)
| X171 = '0'
| ~ nat_fails(esk29_1(X171)) )
& ( nat_fails(X171)
| X171 = '0'
| X171 = s(esk29_1(X171)) )
& ( ~ nat_fails(X169)
| X169 != '0' )
& ( ~ nat_fails(X169)
| nat_fails(X170)
| X169 != s(X170) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_137])])])])])])]) ).
fof(c_0_151,plain,
! [X273] :
( '@*'(s('0'),X273) = X273
| ~ nat_succeeds(X273) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(times:one)'])])]) ).
cnf(c_0_152,negated_conjecture,
'@<_succeeds'(s('0'),s(esk44_0)),
inference(spm,[status(thm)],[c_0_138,c_0_139]) ).
cnf(c_0_153,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@+'('@*'(X1,X2),X1) = '@*'(X1,s(X2)) ),
inference(split_conjunct,[status(thm)],[c_0_140]) ).
cnf(c_0_154,negated_conjecture,
'@*'(esk43_0,esk42_0) = '@*'(esk42_0,esk44_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_141,c_0_142]),c_0_57])]) ).
cnf(c_0_155,negated_conjecture,
'@*'('0',esk43_0) = '0',
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_117,c_0_143]),c_0_144])]) ).
fof(c_0_156,plain,
! [X219] : '@+'('0',X219) = X219,
inference(variable_rename,[status(thm)],['corollary-(plus:zero)']) ).
cnf(c_0_157,negated_conjecture,
'@=<_succeeds'(esk43_0,esk43_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_145,c_0_146]),c_0_56]),c_0_124])]) ).
fof(c_0_158,plain,
! [X147,X148,X149,X150,X151,X152,X153] :
( ( '@<_fails'(X152,X153)
| ~ '@<_fails'(esk23_2(X152,X153),esk24_2(X152,X153))
| X153 = s(esk25_2(X152,X153)) )
& ( '@<_fails'(X152,X153)
| ~ '@<_fails'(esk23_2(X152,X153),esk24_2(X152,X153))
| X152 = '0' )
& ( '@<_fails'(X152,X153)
| X153 = s(esk24_2(X152,X153))
| X153 = s(esk25_2(X152,X153)) )
& ( '@<_fails'(X152,X153)
| X153 = s(esk24_2(X152,X153))
| X152 = '0' )
& ( '@<_fails'(X152,X153)
| X152 = s(esk23_2(X152,X153))
| X153 = s(esk25_2(X152,X153)) )
& ( '@<_fails'(X152,X153)
| X152 = s(esk23_2(X152,X153))
| X152 = '0' )
& ( ~ '@<_fails'(X147,X148)
| X148 != s(X151)
| X147 != '0' )
& ( ~ '@<_fails'(X147,X148)
| '@<_fails'(X149,X150)
| X148 != s(X150)
| X147 != s(X149) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_147])])])])])])]) ).
fof(c_0_159,plain,
! [X173,X174,X175] :
( ( nat_terminates(X175)
| ~ $true
| ~ $true
| ~ nat_terminates(esk30_1(X175)) )
& ( nat_terminates(X175)
| ~ $true
| ~ $true
| X175 = s(esk30_1(X175)) )
& ( ~ nat_terminates(X173)
| $true )
& ( ~ nat_terminates(X173)
| nat_terminates(X174)
| X173 != s(X174) )
& ( ~ nat_terminates(X173)
| $true ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_148])])])])])])]) ).
cnf(c_0_160,plain,
( s(X1) != s(X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_149]) ).
cnf(c_0_161,plain,
( nat_fails(X1)
| X1 = '0'
| X1 = s(esk29_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_150]) ).
fof(c_0_162,plain,
! [X258,X259] :
( '@*'(s(X258),X259) = '@+'(X259,'@*'(X258,X259))
| ~ nat_succeeds(X259)
| ~ nat_succeeds(X258) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(times:successor)'])])]) ).
cnf(c_0_163,plain,
( ~ nat_succeeds(X1)
| '@*'(s('0'),X1) = X1 ),
inference(split_conjunct,[status(thm)],[c_0_151]) ).
cnf(c_0_164,negated_conjecture,
nat_succeeds(s('0')),
inference(spm,[status(thm)],[c_0_58,c_0_152]) ).
cnf(c_0_165,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@+'('@*'(X1,X2),X2) = '@*'(X2,s(X1)) ),
inference(spm,[status(thm)],[c_0_153,c_0_112]) ).
cnf(c_0_166,negated_conjecture,
'@*'('0',esk42_0) = '0',
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_132,c_0_154]),c_0_143]),c_0_155]),c_0_57]),c_0_68])]) ).
cnf(c_0_167,plain,
'@+'('0',X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_156]) ).
fof(c_0_168,plain,
! [X365,X366,X367] :
( '@<_succeeds'(X366,X367)
| ~ '@<_succeeds'('@+'(X365,X366),'@+'(X365,X367))
| ~ nat_succeeds(X365) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(less:plus:inverse)'])])]) ).
fof(c_0_169,plain,
! [X220,X221] :
( '@+'(s(X220),X221) = s('@+'(X220,X221))
| ~ nat_succeeds(X220) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(plus:successor)'])])]) ).
cnf(c_0_170,plain,
( ~ nat_succeeds(X2)
| X1 != s(X2)
| nat_succeeds(X1) ),
inference(split_conjunct,[status(thm)],[c_0_87]) ).
cnf(c_0_171,negated_conjecture,
'@+'(esk43_0,esk35_2(esk43_0,esk43_0)) = esk43_0,
inference(spm,[status(thm)],[c_0_76,c_0_157]) ).
fof(c_0_172,plain,
! [X45,X46] :
( ~ '@<_fails'(X45,X46)
| ~ '@<_succeeds'(X45,X46) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[id11])])]) ).
cnf(c_0_173,plain,
( '@<_fails'(X2,X1)
| X1 = s(esk24_2(X2,X1))
| X1 = s(esk25_2(X2,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_158]) ).
cnf(c_0_174,plain,
( ~ nat_terminates(X1)
| X1 != s(X2)
| nat_terminates(X2) ),
inference(split_conjunct,[status(thm)],[c_0_159]) ).
fof(c_0_175,plain,
! [X183] :
( nat_terminates(X183)
| ~ nat_succeeds(X183) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(nat:termination)'])])]) ).
fof(c_0_176,plain,
! [X49] :
( ~ nat_fails(X49)
| ~ nat_succeeds(X49) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[id13])])]) ).
cnf(c_0_177,plain,
( ~ nat_fails(esk29_1(X1))
| nat_fails(X1)
| X1 = '0' ),
inference(split_conjunct,[status(thm)],[c_0_150]) ).
cnf(c_0_178,plain,
( nat_fails(s(X1))
| esk29_1(s(X1)) = X1 ),
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_160,c_0_161])]),c_0_86]) ).
fof(c_0_179,plain,
! [X363,X364] :
( '@=<_succeeds'(X364,'@+'(X363,X364))
| ~ nat_succeeds(X364)
| ~ nat_succeeds(X363) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(leq:plus:second)'])])]) ).
cnf(c_0_180,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@*'(s(X1),X2) = '@+'(X2,'@*'(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_162]) ).
cnf(c_0_181,plain,
( ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| '@*'(s('0'),'@*'(X1,X2)) = '@*'(X1,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_116,c_0_163]),c_0_164])]) ).
cnf(c_0_182,negated_conjecture,
'@*'(esk42_0,s('0')) = esk42_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_165,c_0_166]),c_0_167]),c_0_118]),c_0_57])]) ).
cnf(c_0_183,plain,
( ~ '@<_succeeds'('@+'(X1,X2),'@+'(X1,X3))
| ~ nat_succeeds(X1)
| '@<_succeeds'(X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_168]) ).
cnf(c_0_184,plain,
( ~ nat_succeeds(X1)
| '@+'(s(X1),X2) = s('@+'(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_169]) ).
cnf(c_0_185,plain,
( ~ nat_succeeds(X1)
| nat_succeeds(s(X1)) ),
inference(er,[status(thm)],[c_0_170]) ).
cnf(c_0_186,negated_conjecture,
esk35_2(esk43_0,esk43_0) = '0',
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84,c_0_171]),c_0_68])]) ).
cnf(c_0_187,plain,
( ~ '@<_fails'(X1,X2)
| ~ '@<_succeeds'(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_172]) ).
cnf(c_0_188,plain,
'@<_fails'(X1,'0'),
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_173])]),c_0_86]) ).
cnf(c_0_189,plain,
( ~ nat_terminates(s(X1))
| nat_terminates(X1) ),
inference(er,[status(thm)],[c_0_174]) ).
cnf(c_0_190,plain,
( ~ nat_succeeds(X1)
| nat_terminates(X1) ),
inference(split_conjunct,[status(thm)],[c_0_175]) ).
cnf(c_0_191,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds('@+'(X2,X1))
| nat_succeeds(X1) ),
inference(spm,[status(thm)],[c_0_106,c_0_90]) ).
cnf(c_0_192,plain,
( ~ nat_fails(X1)
| ~ nat_succeeds(X1) ),
inference(split_conjunct,[status(thm)],[c_0_176]) ).
cnf(c_0_193,plain,
( ~ nat_fails(X1)
| nat_fails(s(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_177,c_0_178]),c_0_86]) ).
cnf(c_0_194,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@=<_succeeds'(X2,'@+'(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_179]) ).
cnf(c_0_195,plain,
( ~ nat_succeeds(X1)
| '@*'(s('0'),X1) = '@+'(X1,'0') ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_180,c_0_117]),c_0_118])]) ).
cnf(c_0_196,negated_conjecture,
'@*'(s('0'),esk42_0) = esk42_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_181,c_0_182]),c_0_164]),c_0_57])]) ).
cnf(c_0_197,plain,
( ~ '@<_succeeds'('@+'(s(X3),X1),s('@+'(X3,X2)))
| ~ nat_succeeds(X3)
| '@<_succeeds'(X1,X2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_184]),c_0_185]) ).
cnf(c_0_198,negated_conjecture,
'@+'(esk43_0,'0') = esk43_0,
inference(rw,[status(thm)],[c_0_171,c_0_186]) ).
cnf(c_0_199,plain,
~ '@<_succeeds'(X1,'0'),
inference(spm,[status(thm)],[c_0_187,c_0_188]) ).
fof(c_0_200,plain,
! [X228,X229] :
( '@+'(X228,s(X229)) = '@+'(s(X228),X229)
| ~ nat_succeeds(X229)
| ~ nat_succeeds(X228) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['lemma-(plus:successor)'])])]) ).
fof(c_0_201,plain,
! [X50] :
( nat_fails(X50)
| nat_succeeds(X50)
| ~ nat_terminates(X50) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[id14])])]) ).
cnf(c_0_202,plain,
( ~ nat_succeeds(s(X1))
| nat_terminates(X1) ),
inference(spm,[status(thm)],[c_0_189,c_0_190]) ).
cnf(c_0_203,negated_conjecture,
nat_succeeds(s(esk37_2(esk43_0,esk44_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_85]),c_0_56]),c_0_68])]) ).
cnf(c_0_204,plain,
( ~ nat_succeeds(s(X1))
| ~ nat_fails(X1) ),
inference(spm,[status(thm)],[c_0_192,c_0_193]) ).
cnf(c_0_205,plain,
( ~ '@=<_succeeds'('@+'(X1,X2),X2)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| '@+'(X1,X2) = X2 ),
inference(spm,[status(thm)],[c_0_82,c_0_194]) ).
cnf(c_0_206,negated_conjecture,
'@+'(esk42_0,'0') = esk42_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_196]),c_0_57])]) ).
cnf(c_0_207,negated_conjecture,
esk42_0 != '0',
inference(split_conjunct,[status(thm)],[c_0_47]) ).
fof(c_0_208,plain,
! [X326,X327] :
( '@=<_succeeds'(X327,X326)
| '@<_succeeds'(X326,X327)
| ~ nat_succeeds(X327)
| ~ nat_succeeds(X326) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['corollary-(less:leq:total)'])])]) ).
cnf(c_0_209,negated_conjecture,
~ '@<_succeeds'('@+'(s(esk43_0),X1),s(esk43_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_197,c_0_198]),c_0_68])]),c_0_199]) ).
cnf(c_0_210,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@+'(X1,s(X2)) = '@+'(s(X1),X2) ),
inference(split_conjunct,[status(thm)],[c_0_200]) ).
cnf(c_0_211,plain,
( ~ nat_terminates(X1)
| nat_fails(X1)
| nat_succeeds(X1) ),
inference(split_conjunct,[status(thm)],[c_0_201]) ).
cnf(c_0_212,negated_conjecture,
nat_terminates(esk37_2(esk43_0,esk44_0)),
inference(spm,[status(thm)],[c_0_202,c_0_203]) ).
cnf(c_0_213,negated_conjecture,
~ nat_fails(esk37_2(esk43_0,esk44_0)),
inference(spm,[status(thm)],[c_0_204,c_0_203]) ).
cnf(c_0_214,plain,
( ~ '@=<_succeeds'('@+'(X2,X1),X2)
| ~ nat_succeeds(X2)
| '@=<_succeeds'(X1,'0') ),
inference(spm,[status(thm)],[c_0_133,c_0_72]) ).
cnf(c_0_215,negated_conjecture,
'@+'('@*'(esk42_0,esk44_0),esk42_0) = '@*'(esk42_0,s(esk43_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_153,c_0_131]),c_0_68]),c_0_57])]) ).
cnf(c_0_216,negated_conjecture,
~ '@=<_succeeds'(esk42_0,'0'),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_205,c_0_206]),c_0_118]),c_0_57])]),c_0_207]) ).
cnf(c_0_217,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| '@=<_succeeds'(X2,X1)
| '@<_succeeds'(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_208]) ).
cnf(c_0_218,negated_conjecture,
'@<_succeeds'(s(esk43_0),s(esk44_0)),
inference(spm,[status(thm)],[c_0_138,c_0_59]) ).
cnf(c_0_219,negated_conjecture,
( ~ '@<_succeeds'('@+'(esk43_0,s(X1)),s(esk43_0))
| ~ nat_succeeds(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_209,c_0_210]),c_0_68])]) ).
cnf(c_0_220,negated_conjecture,
nat_succeeds(esk37_2(esk43_0,esk44_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_211,c_0_212]),c_0_213]) ).
cnf(c_0_221,negated_conjecture,
~ '@=<_succeeds'('@*'(esk42_0,s(esk43_0)),'@*'(esk42_0,esk44_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_214,c_0_215]),c_0_144])]),c_0_216]) ).
cnf(c_0_222,plain,
( ~ nat_succeeds(X2)
| ~ nat_succeeds(X3)
| ~ nat_succeeds(X1)
| '@=<_succeeds'('@*'(X3,X2),'@*'(X3,X1))
| '@<_succeeds'(X1,X2) ),
inference(spm,[status(thm)],[c_0_97,c_0_217]) ).
cnf(c_0_223,negated_conjecture,
nat_succeeds(s(esk43_0)),
inference(spm,[status(thm)],[c_0_58,c_0_218]) ).
cnf(c_0_224,negated_conjecture,
~ '@<_succeeds'(esk44_0,s(esk43_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_219,c_0_85]),c_0_220])]) ).
cnf(c_0_225,negated_conjecture,
$false,
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_221,c_0_222]),c_0_56]),c_0_57]),c_0_223])]),c_0_224]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX047+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.36 % Computer : n010.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Mon Sep 21 10:25:10 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.80/16.74 % Version: 3.5.1
% 98.80/16.74 % Preprocessing class: FSLSSMSSSSSNFFN.
% 98.80/16.74 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 98.80/16.74 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 98.80/16.74 % Starting new_bool_3 with 300s (1) cores
% 98.80/16.74 % Starting new_bool_1 with 300s (1) cores
% 98.80/16.74 % Starting sh5l with 300s (1) cores
% 98.80/16.74 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 665022 completed with status 0
% 98.80/16.74 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 98.80/16.74 % Preprocessing class: FSLSSMSSSSSNFFN.
% 98.80/16.74 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 98.80/16.74 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 98.80/16.74 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 98.80/16.74 % No SInE strategy applied
% 98.80/16.74 % Search class: FGHSF-FSLS32-MFFFFFNN
% 98.80/16.74 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 98.80/16.74 % Starting SubtermCWHack with 136s (1) cores
% 98.80/16.74 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 98.80/16.74 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_RG_S04AN with 136s (1) cores
% 98.80/16.74 % Starting new_bool_3 with 136s (1) cores
% 98.80/16.74 % Starting new_bool_1 with 136s (1) cores
% 98.80/16.74 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 665027 completed with status 0
% 98.80/16.74 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 98.80/16.74 % Preprocessing class: FSLSSMSSSSSNFFN.
% 98.80/16.74 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 98.80/16.74 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 98.80/16.74 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 98.80/16.74 % No SInE strategy applied
% 98.80/16.74 % Search class: FGHSF-FSLS32-MFFFFFNN
% 98.80/16.74 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 98.80/16.74 % Starting SubtermCWHack with 136s (1) cores
% 98.80/16.74 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 98.80/16.74 % Preprocessing time : 0.004 s
% 98.80/16.74 % Presaturation interreduction done
% 98.80/16.74
% 98.80/16.74 % Proof found!
% 98.80/16.74 % SZS status Theorem
% 98.80/16.74 % SZS output start CNFRefutation
% See solution above
% 98.80/16.74 % Parsed axioms : 121
% 98.80/16.74 % Removed by relevancy pruning/SinE : 0
% 98.80/16.74 % Initial clauses : 230
% 98.80/16.74 % Removed in clause preprocessing : 16
% 98.80/16.74 % Initial clauses in saturation : 214
% 98.80/16.74 % Processed clauses : 28186
% 98.80/16.74 % ...of these trivial : 684
% 98.80/16.74 % ...subsumed : 19983
% 98.80/16.74 % ...remaining for further processing : 7519
% 98.80/16.74 % Other redundant clauses eliminated : 1484
% 98.80/16.74 % Clauses deleted for lack of memory : 0
% 98.80/16.74 % Backward-subsumed : 320
% 98.80/16.74 % Backward-rewritten : 820
% 98.80/16.74 % Generated clauses : 353904
% 98.80/16.74 % ...of the previous two non-redundant : 330418
% 98.80/16.74 % ...aggressively subsumed : 0
% 98.80/16.74 % Contextual simplify-reflections : 388
% 98.80/16.74 % Paramodulations : 352425
% 98.80/16.74 % Factorizations : 6
% 98.80/16.74 % NegExts : 0
% 98.80/16.74 % Equation resolutions : 1487
% 98.80/16.74 % Disequality decompositions : 0
% 98.80/16.74 % Total rewrite steps : 160224
% 98.80/16.74 % ...of those cached : 156437
% 98.80/16.74 % Propositional unsat checks : 1
% 98.80/16.74 % Propositional check models : 0
% 98.80/16.74 % Propositional check unsatisfiable : 0
% 98.80/16.74 % Propositional clauses : 0
% 98.80/16.74 % Propositional clauses after purity: 0
% 98.80/16.74 % Propositional unsat core size : 0
% 98.80/16.74 % Propositional preprocessing time : 0.000
% 98.80/16.74 % Propositional encoding time : 0.419
% 98.80/16.74 % Propositional solver time : 0.407
% 98.80/16.74 % Success case prop preproc time : 0.000
% 98.80/16.74 % Success case prop encoding time : 0.000
% 98.80/16.74 % Success case prop solver time : 0.000
% 98.80/16.74 % Current number of processed clauses : 6145
% 98.80/16.74 % Positive orientable unit clauses : 772
% 98.80/16.74 % Positive unorientable unit clauses: 0
% 98.80/16.74 % Negative unit clauses : 1546
% 98.80/16.74 % Non-unit-clauses : 3827
% 98.80/16.74 % Current number of unprocessed clauses: 299910
% 98.80/16.74 % ...number of literals in the above : 1291215
% 98.80/16.74 % Current number of archived formulas : 0
% 98.80/16.74 % Current number of archived clauses : 1346
% 98.80/16.74 % Clause-clause subsumption calls (NU) : 2060520
% 98.80/16.74 % Rec. Clause-clause subsumption calls : 975891
% 98.80/16.74 % Non-unit clause-clause subsumptions : 11555
% 98.80/16.74 % Unit Clause-clause subsumption calls : 334815
% 98.80/16.74 % Rewrite failures with RHS unbound : 0
% 98.80/16.74 % BW rewrite match attempts : 797
% 98.80/16.74 % BW rewrite match successes : 208
% 98.80/16.74 % Condensation attempts : 0
% 98.80/16.74 % Condensation successes : 0
% 98.80/16.74 % Termbank termtop insertions : 6446726
% 98.80/16.74 % Search garbage collected termcells : 4038
% 98.80/16.74
% 98.80/16.74 % -------------------------------------------------
% 98.80/16.74 % User time : 13.536 s
% 98.80/16.74 % System time : 0.441 s
% 98.80/16.74 % Total time : 13.977 s
% 98.80/16.74 % Maximum resident set size: 4288 pages
% 98.80/16.74
% 98.80/16.74 % -------------------------------------------------
% 98.80/16.74 % User time : 67.733 s
% 98.80/16.74 % System time : 2.276 s
% 98.80/16.74 % Total time : 70.009 s
% 98.80/16.74 % Maximum resident set size: 4864 pages
% 98.80/16.74 % E exiting
%------------------------------------------------------------------------------