%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL893+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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 : Mon Sep 7 12:59:28 PM UTC 2026
% Result : Theorem 7.37s 7.62s
% Output : CNFRefutation 7.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL893+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.36 % Computer : n018.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 6 00:28:04 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.11/0.43 (re.compile("\."), Token.FullStop),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.11/0.43 (re.compile("\("), Token.OpenPar),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.11/0.43 (re.compile("\)"), Token.ClosePar),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.11/0.43 (re.compile("\["), Token.OpenSquare),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.11/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.43 (re.compile("~\|"), Token.Nor),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.43 (re.compile("\|"), Token.Or),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.11/0.43 (re.compile("\?"), Token.Existential),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.11/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.11/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.11/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.23/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.34/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.34/0.59 """
% 7.37/7.62 % Version: 1.5
% 7.37/7.62 % SZS status Theorem
% 7.37/7.62 % SZS output start CNFRefutation
% 7.37/7.62 fof(goals_15,conjecture,(![X17]:(h(X17)=X17=>X17='0')),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals_15)).
% 7.37/7.62 fof(c4,negated_conjecture,(~(![X17]:(h(X17)=X17=>X17='0'))),inference(assume_negation,[status(cth)],[goals_15])).
% 7.37/7.62 fof(c5,negated_conjecture,(?[X17]:(h(X17)=X17&X17!='0')),inference(fof_nnf,[status(thm)],[c4])).
% 7.37/7.62 fof(c6,negated_conjecture,(?[X2]:(h(X2)=X2&X2!='0')),inference(variable_rename,[status(thm)],[c5])).
% 7.37/7.62 fof(c7,negated_conjecture,(h(skolem0001)=skolem0001&skolem0001!='0'),inference(skolemize,[status(esa)],[c6])).
% 7.37/7.62 cnf(c9,negated_conjecture,skolem0001!='0',inference(split_conjunct,[status(thm)],[c7])).
% 7.37/7.62 cnf(symmetry,axiom,X39!=X38|X38=X39,theory(equality)).
% 7.37/7.62 cnf(transitivity,axiom,X42!=X41|X41!=X40|X42=X40,theory(equality)).
% 7.37/7.62 cnf(c8,negated_conjecture,h(skolem0001)=skolem0001,inference(split_conjunct,[status(thm)],[c7])).
% 7.37/7.62 cnf(c57,plain,X90!=h(skolem0001)|X90=skolem0001,inference(resolution,[status(thm)],[c8, transitivity])).
% 7.37/7.62 fof(sos_14,axiom,(![A]:h(A)='==>'(h(A),A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_14)).
% 7.37/7.62 fof(c10,plain,(![X3]:h(X3)='==>'(h(X3),X3)),inference(variable_rename,[status(thm)],[sos_14])).
% 7.37/7.62 cnf(c11,plain,h(X65)='==>'(h(X65),X65),inference(split_conjunct,[status(thm)],[c10])).
% 7.37/7.62 cnf(c91,plain,'==>'(h(X69),X69)=h(X69),inference(resolution,[status(thm)],[c11, symmetry])).
% 7.37/7.62 cnf(c103,plain,X354!='==>'(h(X353),X353)|X354=h(X353),inference(resolution,[status(thm)],[c91, transitivity])).
% 7.37/7.62 fof(sos_09,axiom,(![A]:'>='(A,'0')),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_09)).
% 7.37/7.62 fof(c29,plain,(![X15]:'>='(X15,'0')),inference(variable_rename,[status(thm)],[sos_09])).
% 7.37/7.62 cnf(c30,plain,'>='(X37,'0'),inference(split_conjunct,[status(thm)],[c29])).
% 7.37/7.62 fof(sos_07,axiom,(![X3]:(![X4]:(('>='(X3,X4)&'>='(X4,X3))=>X3=X4))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_07)).
% 7.37/7.62 fof(c37,plain,(![X3]:(![X4]:((~'>='(X3,X4)|~'>='(X4,X3))|X3=X4))),inference(fof_nnf,[status(thm)],[sos_07])).
% 7.37/7.62 fof(c38,plain,(![X22]:(![X23]:((~'>='(X22,X23)|~'>='(X23,X22))|X22=X23))),inference(variable_rename,[status(thm)],[c37])).
% 7.37/7.62 cnf(c39,plain,~'>='(X72,X71)|~'>='(X71,X72)|X72=X71,inference(split_conjunct,[status(thm)],[c38])).
% 7.37/7.62 cnf(c108,plain,~'>='('0',X79)|'0'=X79,inference(resolution,[status(thm)],[c39, c30])).
% 7.37/7.62 fof(sos_08,axiom,(![X5]:(![X6]:(![X7]:('>='('+'(X5,X6),X7)<=>'>='(X6,'==>'(X5,X7)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_08)).
% 7.37/7.62 fof(c31,plain,(![X5]:(![X6]:(![X7]:((~'>='('+'(X5,X6),X7)|'>='(X6,'==>'(X5,X7)))&(~'>='(X6,'==>'(X5,X7))|'>='('+'(X5,X6),X7)))))),inference(fof_nnf,[status(thm)],[sos_08])).
% 7.37/7.62 fof(c32,plain,((![X5]:(![X6]:(![X7]:(~'>='('+'(X5,X6),X7)|'>='(X6,'==>'(X5,X7))))))&(![X5]:(![X6]:(![X7]:(~'>='(X6,'==>'(X5,X7))|'>='('+'(X5,X6),X7)))))),inference(shift_quantors,[status(thm)],[c31])).
% 7.37/7.62 fof(c34,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:((~'>='('+'(X16,X17),X18)|'>='(X17,'==>'(X16,X18)))&(~'>='(X20,'==>'(X19,X21))|'>='('+'(X19,X20),X21))))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,((![X16]:(![X17]:(![X18]:(~'>='('+'(X16,X17),X18)|'>='(X17,'==>'(X16,X18))))))&(![X19]:(![X20]:(![X21]:(~'>='(X20,'==>'(X19,X21))|'>='('+'(X19,X20),X21)))))),inference(variable_rename,[status(thm)],[c32])).])).
% 7.37/7.62 cnf(c35,plain,~'>='('+'(X120,X122),X121)|'>='(X122,'==>'(X120,X121)),inference(split_conjunct,[status(thm)],[c34])).
% 7.37/7.62 fof(sos_06,axiom,(![X0]:(![X1]:(![X2]:(('>='(X0,X1)&'>='(X1,X2))=>'>='(X0,X2))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_06)).
% 7.37/7.62 fof(c40,plain,(![X0]:(![X1]:(![X2]:((~'>='(X0,X1)|~'>='(X1,X2))|'>='(X0,X2))))),inference(fof_nnf,[status(thm)],[sos_06])).
% 7.37/7.62 fof(c41,plain,(![X24]:(![X25]:(![X26]:((~'>='(X24,X25)|~'>='(X25,X26))|'>='(X24,X26))))),inference(variable_rename,[status(thm)],[c40])).
% 7.37/7.62 cnf(c42,plain,~'>='(X82,X81)|~'>='(X81,X80)|'>='(X82,X80),inference(split_conjunct,[status(thm)],[c41])).
% 7.37/7.62 cnf(c56,plain,skolem0001=h(skolem0001),inference(resolution,[status(thm)],[c8, symmetry])).
% 7.37/7.62 cnf(reflexivity,axiom,X35=X35,theory(equality)).
% 7.37/7.62 fof(sos_05,axiom,(![A]:'>='(A,A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_05)).
% 7.37/7.62 fof(c43,plain,(![X27]:'>='(X27,X27)),inference(variable_rename,[status(thm)],[sos_05])).
% 7.37/7.62 cnf(c44,plain,'>='(X36,X36),inference(split_conjunct,[status(thm)],[c43])).
% 7.37/7.62 cnf(c3,axiom,X75!=X74|X76!=X77|~'>='(X75,X76)|'>='(X74,X77),theory(equality)).
% 7.37/7.62 cnf(c109,plain,X174!=X175|X174!=X173|'>='(X175,X173),inference(resolution,[status(thm)],[c3, c44])).
% 7.37/7.62 cnf(c381,plain,X181!=X182|'>='(X182,X181),inference(resolution,[status(thm)],[c109, reflexivity])).
% 7.37/7.62 cnf(c412,plain,'>='(h(skolem0001),skolem0001),inference(resolution,[status(thm)],[c381, c56])).
% 7.37/7.62 cnf(c441,plain,~'>='(X352,h(skolem0001))|'>='(X352,skolem0001),inference(resolution,[status(thm)],[c412, c42])).
% 7.37/7.62 cnf(c36,plain,~'>='(X128,'==>'(X129,X130))|'>='('+'(X129,X128),X130),inference(split_conjunct,[status(thm)],[c34])).
% 7.37/7.62 fof(sos_03,axiom,(![A]:'+'(A,'0')=A),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_03)).
% 7.37/7.62 fof(c47,plain,(![X29]:'+'(X29,'0')=X29),inference(variable_rename,[status(thm)],[sos_03])).
% 7.37/7.62 cnf(c48,plain,'+'(X44,'0')=X44,inference(split_conjunct,[status(thm)],[c47])).
% 7.37/7.62 cnf(c58,plain,X52='+'(X52,'0'),inference(resolution,[status(thm)],[c48, symmetry])).
% 7.37/7.62 cnf(c422,plain,'>='('+'(X188,'0'),X188),inference(resolution,[status(thm)],[c381, c58])).
% 7.37/7.62 cnf(c482,plain,'>='('0','==>'(X190,X190)),inference(resolution,[status(thm)],[c422, c35])).
% 7.37/7.62 cnf(c503,plain,'0'='==>'(X196,X196),inference(resolution,[status(thm)],[c482, c108])).
% 7.37/7.62 cnf(c110,plain,X358!=X359|'0'!=X357|'>='(X359,X357),inference(resolution,[status(thm)],[c3, c30])).
% 7.37/7.62 cnf(c2163,plain,X404!=X403|'>='(X403,'==>'(X405,X405)),inference(resolution,[status(thm)],[c110, c503])).
% 7.37/7.62 cnf(c2436,plain,'>='(X406,'==>'(X407,X407)),inference(resolution,[status(thm)],[c2163, c48])).
% 7.37/7.62 cnf(c2489,plain,'>='('+'(X420,X419),X420),inference(resolution,[status(thm)],[c2436, c36])).
% 7.37/7.62 cnf(c2507,plain,'>='('+'(h(skolem0001),X682),skolem0001),inference(resolution,[status(thm)],[c2489, c441])).
% 7.37/7.62 cnf(c3477,plain,'>='(X999,'==>'(h(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c2507, c35])).
% 7.37/7.62 cnf(c5219,plain,'0'='==>'(h(skolem0001),skolem0001),inference(resolution,[status(thm)],[c3477, c108])).
% 7.37/7.62 cnf(c18007,plain,'0'=h(skolem0001),inference(resolution,[status(thm)],[c5219, c103])).
% 7.37/7.62 cnf(c18055,plain,'0'=skolem0001,inference(resolution,[status(thm)],[c18007, c57])).
% 7.37/7.62 cnf(c18101,plain,skolem0001='0',inference(resolution,[status(thm)],[c18055, symmetry])).
% 7.37/7.62 cnf(c18291,plain,$false,inference(resolution,[status(thm)],[c18101, c9])).
% 7.37/7.62 % SZS output end CNFRefutation
% 7.37/7.62
% 7.37/7.62 % Initial clauses : 24
% 7.37/7.62 % Processed clauses : 540
% 7.37/7.62 % Factors computed : 12
% 7.37/7.62 % Resolvents computed: 18240
% 7.37/7.62 % Tautologies deleted: 4
% 7.37/7.62 % Forward subsumed : 1011
% 7.37/7.62 % Backward subsumed : 39
% 7.37/7.62 % -------- CPU Time ---------
% 7.37/7.62 % User time : 7.191 s
% 7.37/7.62 % System time : 0.064 s
% 7.37/7.62 % Total time : 7.255 s
%------------------------------------------------------------------------------