%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL899+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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 46.06s 46.34s
% Output : CNFRefutation 46.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL899+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.06/0.33 % Computer : n013.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.33 % WCLimit : 300
% 0.06/0.33 % DateTime : Sun Sep 6 01:01:35 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.11/0.40 (re.compile("\."), Token.FullStop),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.11/0.40 (re.compile("\("), Token.OpenPar),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.11/0.40 (re.compile("\)"), Token.ClosePar),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.11/0.40 (re.compile("\["), Token.OpenSquare),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.11/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.40 (re.compile("~\|"), Token.Nor),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.40 (re.compile("\|"), Token.Or),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.11/0.40 (re.compile("\?"), Token.Existential),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.11/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.11/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.11/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.47 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.47 """
% 0.22/0.47 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.47 """
% 0.22/0.56 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.56 """
% 46.06/46.34 % Version: 1.5
% 46.06/46.34 % SZS status Theorem
% 46.06/46.34 % SZS output start CNFRefutation
% 46.06/46.34 fof(goals_14,conjecture,(![X17]:'==>'('==>'(X17,'1'),'1')=X17),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals_14)).
% 46.06/46.34 fof(c3,negated_conjecture,(~(![X17]:'==>'('==>'(X17,'1'),'1')=X17)),inference(assume_negation,[status(cth)],[goals_14])).
% 46.06/46.34 fof(c4,negated_conjecture,(?[X17]:'==>'('==>'(X17,'1'),'1')!=X17),inference(fof_nnf,[status(thm)],[c3])).
% 46.06/46.34 fof(c5,negated_conjecture,(?[X2]:'==>'('==>'(X2,'1'),'1')!=X2),inference(variable_rename,[status(thm)],[c4])).
% 46.06/46.34 fof(c6,negated_conjecture,'==>'('==>'(skolem0001,'1'),'1')!=skolem0001,inference(skolemize,[status(esa)],[c5])).
% 46.06/46.34 cnf(c7,negated_conjecture,'==>'('==>'(skolem0001,'1'),'1')!=skolem0001,inference(split_conjunct,[status(thm)],[c6])).
% 46.06/46.34 cnf(symmetry,axiom,X37!=X38|X38=X37,theory(equality)).
% 46.06/46.34 cnf(transitivity,axiom,X40!=X42|X42!=X41|X40=X41,theory(equality)).
% 46.06/46.34 fof(sos_13,axiom,(![A]:(![B]:'==>'('==>'(A,B),B)='==>'('==>'(B,A),A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_13)).
% 46.06/46.34 fof(c8,plain,(![X3]:(![X4]:'==>'('==>'(X3,X4),X4)='==>'('==>'(X4,X3),X3))),inference(variable_rename,[status(thm)],[sos_13])).
% 46.06/46.34 cnf(c9,plain,'==>'('==>'(X88,X87),X87)='==>'('==>'(X87,X88),X88),inference(split_conjunct,[status(thm)],[c8])).
% 46.06/46.34 cnf(c100,plain,X358!='==>'('==>'(X359,X357),X357)|X358='==>'('==>'(X357,X359),X359),inference(resolution,[status(thm)],[c9, transitivity])).
% 46.06/46.34 fof(sos_06,axiom,(![X3]:(![X4]:(('>='(X3,X4)&'>='(X4,X3))=>X3=X4))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_06)).
% 46.06/46.34 fof(c35,plain,(![X3]:(![X4]:((~'>='(X3,X4)|~'>='(X4,X3))|X3=X4))),inference(fof_nnf,[status(thm)],[sos_06])).
% 46.06/46.34 fof(c36,plain,(![X22]:(![X23]:((~'>='(X22,X23)|~'>='(X23,X22))|X22=X23))),inference(variable_rename,[status(thm)],[c35])).
% 46.06/46.34 cnf(c37,plain,~'>='(X64,X65)|~'>='(X65,X64)|X64=X65,inference(split_conjunct,[status(thm)],[c36])).
% 46.06/46.34 fof(sos_07,axiom,(![X5]:(![X6]:(![X7]:('>='('+'(X5,X6),X7)<=>'>='(X6,'==>'(X5,X7)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_07)).
% 46.06/46.34 fof(c29,plain,(![X5]:(![X6]:(![X7]:((~'>='('+'(X5,X6),X7)|'>='(X6,'==>'(X5,X7)))&(~'>='(X6,'==>'(X5,X7))|'>='('+'(X5,X6),X7)))))),inference(fof_nnf,[status(thm)],[sos_07])).
% 46.06/46.34 fof(c30,plain,((![X5]:(![X6]:(![X7]:(~'>='('+'(X5,X6),X7)|'>='(X6,'==>'(X5,X7))))))&(![X5]:(![X6]:(![X7]:(~'>='(X6,'==>'(X5,X7))|'>='('+'(X5,X6),X7)))))),inference(shift_quantors,[status(thm)],[c29])).
% 46.06/46.34 fof(c32,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(c31,plain,((![X16]:(![X17]:(![X18]:(~'>='('+'(X16,X17),X18)|'>='(X17,'==>'(X16,X18))))))&(![X19]:(![X20]:(![X21]:(~'>='(X20,'==>'(X19,X21))|'>='('+'(X19,X20),X21)))))),inference(variable_rename,[status(thm)],[c30])).])).
% 46.06/46.34 cnf(c33,plain,~'>='('+'(X125,X126),X124)|'>='(X126,'==>'(X125,X124)),inference(split_conjunct,[status(thm)],[c32])).
% 46.06/46.34 fof(sos_02,axiom,(![A]:(![B]:'+'(A,B)='+'(B,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_02)).
% 46.06/46.34 fof(c45,plain,(![X29]:(![X30]:'+'(X29,X30)='+'(X30,X29))),inference(variable_rename,[status(thm)],[sos_02])).
% 46.06/46.34 cnf(c46,plain,'+'(X57,X56)='+'(X56,X57),inference(split_conjunct,[status(thm)],[c45])).
% 46.06/46.34 cnf(reflexivity,axiom,X34=X34,theory(equality)).
% 46.06/46.34 fof(sos_04,axiom,(![A]:'>='(A,A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_04)).
% 46.06/46.34 fof(c41,plain,(![X27]:'>='(X27,X27)),inference(variable_rename,[status(thm)],[sos_04])).
% 46.06/46.34 cnf(c42,plain,'>='(X35,X35),inference(split_conjunct,[status(thm)],[c41])).
% 46.06/46.34 cnf(c2,axiom,X72!=X70|X69!=X71|~'>='(X72,X69)|'>='(X70,X71),theory(equality)).
% 46.06/46.34 cnf(c81,plain,X93!=X94|X93!=X95|'>='(X94,X95),inference(resolution,[status(thm)],[c2, c42])).
% 46.06/46.34 cnf(c118,plain,X102!=X101|'>='(X101,X102),inference(resolution,[status(thm)],[c81, reflexivity])).
% 46.06/46.34 cnf(c125,plain,'>='('+'(X119,X118),'+'(X118,X119)),inference(resolution,[status(thm)],[c118, c46])).
% 46.06/46.34 fof(sos_05,axiom,(![X0]:(![X1]:(![X2]:(('>='(X0,X1)&'>='(X1,X2))=>'>='(X0,X2))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_05)).
% 46.06/46.34 fof(c38,plain,(![X0]:(![X1]:(![X2]:((~'>='(X0,X1)|~'>='(X1,X2))|'>='(X0,X2))))),inference(fof_nnf,[status(thm)],[sos_05])).
% 46.06/46.34 fof(c39,plain,(![X24]:(![X25]:(![X26]:((~'>='(X24,X25)|~'>='(X25,X26))|'>='(X24,X26))))),inference(variable_rename,[status(thm)],[c38])).
% 46.06/46.34 cnf(c40,plain,~'>='(X75,X73)|~'>='(X73,X74)|'>='(X75,X74),inference(split_conjunct,[status(thm)],[c39])).
% 46.06/46.34 cnf(c34,plain,~'>='(X134,'==>'(X133,X135))|'>='('+'(X133,X134),X135),inference(split_conjunct,[status(thm)],[c32])).
% 46.06/46.34 fof(sos_03,axiom,(![A]:'+'(A,'0')=A),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_03)).
% 46.06/46.34 fof(c43,plain,(![X28]:'+'(X28,'0')=X28),inference(variable_rename,[status(thm)],[sos_03])).
% 46.06/46.34 cnf(c44,plain,'+'(X43,'0')=X43,inference(split_conjunct,[status(thm)],[c43])).
% 46.06/46.34 cnf(c52,plain,X81!='+'(X82,'0')|X81=X82,inference(resolution,[status(thm)],[c44, transitivity])).
% 46.06/46.34 cnf(c89,plain,'+'('+'(X218,'0'),'0')=X218,inference(resolution,[status(thm)],[c52, c44])).
% 46.06/46.34 fof(sos_08,axiom,(![A]:'>='(A,'0')),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_08)).
% 46.06/46.34 fof(c27,plain,(![X15]:'>='(X15,'0')),inference(variable_rename,[status(thm)],[sos_08])).
% 46.06/46.34 cnf(c28,plain,'>='(X36,'0'),inference(split_conjunct,[status(thm)],[c27])).
% 46.06/46.34 cnf(c78,plain,~'>='('0',X68)|'0'=X68,inference(resolution,[status(thm)],[c37, c28])).
% 46.06/46.34 cnf(c53,plain,X47='+'(X47,'0'),inference(resolution,[status(thm)],[c44, symmetry])).
% 46.06/46.34 cnf(c131,plain,'>='('+'(X105,'0'),X105),inference(resolution,[status(thm)],[c118, c53])).
% 46.06/46.34 cnf(c183,plain,'>='('0','==>'(X128,X128)),inference(resolution,[status(thm)],[c33, c131])).
% 46.06/46.34 cnf(c201,plain,'0'='==>'(X131,X131),inference(resolution,[status(thm)],[c183, c78])).
% 46.06/46.34 cnf(c82,plain,X301!=X299|'0'!=X300|'>='(X299,X300),inference(resolution,[status(thm)],[c2, c28])).
% 46.06/46.34 cnf(c846,plain,X313!=X312|'>='(X312,'==>'(X311,X311)),inference(resolution,[status(thm)],[c82, c201])).
% 46.06/46.34 cnf(c873,plain,'>='(X315,'==>'(X314,X314)),inference(resolution,[status(thm)],[c846, c89])).
% 46.06/46.34 cnf(c890,plain,'>='('+'(X328,X327),X328),inference(resolution,[status(thm)],[c873, c34])).
% 46.06/46.34 cnf(c918,plain,~'>='(X374,'+'(X375,X373))|'>='(X374,X375),inference(resolution,[status(thm)],[c890, c40])).
% 46.06/46.34 cnf(c1001,plain,'>='('+'(X388,X389),X389),inference(resolution,[status(thm)],[c918, c125])).
% 46.06/46.34 cnf(c1042,plain,'>='(X395,'==>'(X394,X395)),inference(resolution,[status(thm)],[c1001, c33])).
% 46.06/46.34 cnf(c1075,plain,~'>='('==>'(X7416,X7417),X7417)|'==>'(X7416,X7417)=X7417,inference(resolution,[status(thm)],[c1042, c37])).
% 46.06/46.34 cnf(c86,plain,'+'('0',X84)=X84,inference(resolution,[status(thm)],[c52, c46])).
% 46.06/46.34 cnf(c130,plain,'>='(X104,'+'('0',X104)),inference(resolution,[status(thm)],[c118, c86])).
% 46.06/46.34 cnf(c225,plain,'>='('+'(X162,'==>'(X162,X163)),X163),inference(resolution,[status(thm)],[c34, c42])).
% 46.06/46.34 cnf(c307,plain,~'>='(X1783,'+'(X1782,'==>'(X1782,X1784)))|'>='(X1783,X1784),inference(resolution,[status(thm)],[c225, c40])).
% 46.06/46.34 cnf(c7463,plain,'>='('==>'('0',X1794),X1794),inference(resolution,[status(thm)],[c307, c130])).
% 46.06/46.34 cnf(c7506,plain,~'>='(X2927,'==>'('0',X2928))|'>='(X2927,X2928),inference(resolution,[status(thm)],[c7463, c40])).
% 46.06/46.34 fof(sos_10,axiom,(![X11]:(![X12]:(![X13]:('>='(X11,X12)=>'>='('==>'(X12,X13),'==>'(X11,X13)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_10)).
% 46.06/46.34 fof(c17,plain,(![X11]:(![X12]:(![X13]:(~'>='(X11,X12)|'>='('==>'(X12,X13),'==>'(X11,X13)))))),inference(fof_nnf,[status(thm)],[sos_10])).
% 46.06/46.34 fof(c18,plain,(![X11]:(![X12]:(~'>='(X11,X12)|(![X13]:'>='('==>'(X12,X13),'==>'(X11,X13)))))),inference(shift_quantors,[status(thm)],[c17])).
% 46.06/46.34 fof(c20,plain,(![X9]:(![X10]:(![X11]:(~'>='(X9,X10)|'>='('==>'(X10,X11),'==>'(X9,X11)))))),inference(shift_quantors,[status(thm)],[fof(c19,plain,(![X9]:(![X10]:(~'>='(X9,X10)|(![X11]:'>='('==>'(X10,X11),'==>'(X9,X11)))))),inference(variable_rename,[status(thm)],[c18])).])).
% 46.06/46.34 cnf(c21,plain,~'>='(X107,X106)|'>='('==>'(X106,X108),'==>'(X107,X108)),inference(split_conjunct,[status(thm)],[c20])).
% 46.06/46.34 fof(sos_12,axiom,(![A]:'+'(A,'1')='1'),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_12)).
% 46.06/46.34 fof(c10,plain,(![X5]:'+'(X5,'1')='1'),inference(variable_rename,[status(thm)],[sos_12])).
% 46.06/46.34 cnf(c11,plain,'+'(X53,'1')='1',inference(split_conjunct,[status(thm)],[c10])).
% 46.06/46.34 cnf(c127,plain,'>='('1','+'(X112,'1')),inference(resolution,[status(thm)],[c118, c11])).
% 46.06/46.34 cnf(c1002,plain,'>='('1',X378),inference(resolution,[status(thm)],[c918, c127])).
% 46.06/46.34 cnf(c1007,plain,~'>='(X408,'1')|'>='(X408,X409),inference(resolution,[status(thm)],[c1002, c40])).
% 46.06/46.34 cnf(c1121,plain,'>='('+'('1',X413),X412),inference(resolution,[status(thm)],[c1007, c890])).
% 46.06/46.34 cnf(c1134,plain,'>='(X422,'==>'('1',X421)),inference(resolution,[status(thm)],[c1121, c33])).
% 46.06/46.34 cnf(c1176,plain,'>='('==>'('==>'('1',X8379),X8378),'==>'(X8380,X8378)),inference(resolution,[status(thm)],[c1134, c21])).
% 46.06/46.34 cnf(c56672,plain,'>='('==>'('==>'('1',X8381),X8382),X8382),inference(resolution,[status(thm)],[c1176, c7506])).
% 46.06/46.34 cnf(c56691,plain,'==>'('==>'('1',X8383),X8384)=X8384,inference(resolution,[status(thm)],[c56672, c1075])).
% 46.06/46.34 cnf(c56736,plain,X8419='==>'('==>'('1',X8420),X8419),inference(resolution,[status(thm)],[c56691, symmetry])).
% 46.06/46.34 cnf(c57205,plain,X8515='==>'('==>'(X8515,'1'),'1'),inference(resolution,[status(thm)],[c56736, c100])).
% 46.06/46.34 cnf(c57670,plain,'==>'('==>'(X8542,'1'),'1')=X8542,inference(resolution,[status(thm)],[c57205, symmetry])).
% 46.06/46.34 cnf(c58001,plain,$false,inference(resolution,[status(thm)],[c57670, c7])).
% 46.06/46.34 % SZS output end CNFRefutation
% 46.06/46.34
% 46.06/46.34 % Initial clauses : 21
% 46.06/46.34 % Processed clauses : 1099
% 46.06/46.34 % Factors computed : 21
% 46.06/46.34 % Resolvents computed: 58002
% 46.06/46.34 % Tautologies deleted: 4
% 46.06/46.34 % Forward subsumed : 3806
% 46.06/46.34 % Backward subsumed : 84
% 46.06/46.34 % -------- CPU Time ---------
% 46.06/46.34 % User time : 45.825 s
% 46.06/46.34 % System time : 0.177 s
% 46.06/46.34 % Total time : 46.002 s
%------------------------------------------------------------------------------