%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL454+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:58:33 PM UTC 2026
% Result : Theorem 39.81s 40.09s
% Output : CNFRefutation 39.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL454+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.36 % Computer : n016.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 : Sat Sep 5 21:44:45 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.11/0.42 (re.compile("\."), Token.FullStop),
% 0.11/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.11/0.42 (re.compile("\("), Token.OpenPar),
% 0.11/0.42 /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.33/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.59 """
% 39.81/40.09 % Version: 1.5
% 39.81/40.09 % SZS status Theorem
% 39.81/40.09 % SZS output start CNFRefutation
% 39.81/40.09 fof(principia_r1,conjecture,r1,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', principia_r1)).
% 39.81/40.09 fof(c6,negated_conjecture,(~r1),inference(assume_negation,[status(cth)],[principia_r1])).
% 39.81/40.09 fof(c7,negated_conjecture,~r1,inference(fof_simplification,[status(thm)],[c6])).
% 39.81/40.09 cnf(c8,negated_conjecture,~r1,inference(split_conjunct,[status(thm)],[c7])).
% 39.81/40.09 fof(r1,axiom,(r1<=>(![P]:is_a_theorem(implies(or(P,P),P)))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', r1)).
% 39.81/40.09 fof(c74,plain,((~r1|(![P]:is_a_theorem(implies(or(P,P),P))))&((?[P]:~is_a_theorem(implies(or(P,P),P)))|r1)),inference(fof_nnf,[status(thm)],[r1])).
% 39.81/40.09 fof(c75,plain,((~r1|(![X32]:is_a_theorem(implies(or(X32,X32),X32))))&((?[X33]:~is_a_theorem(implies(or(X33,X33),X33)))|r1)),inference(variable_rename,[status(thm)],[c74])).
% 39.81/40.09 fof(c77,plain,(![X32]:((~r1|is_a_theorem(implies(or(X32,X32),X32)))&(~is_a_theorem(implies(or(skolem0011,skolem0011),skolem0011))|r1))),inference(shift_quantors,[status(thm)],[fof(c76,plain,((~r1|(![X32]:is_a_theorem(implies(or(X32,X32),X32))))&(~is_a_theorem(implies(or(skolem0011,skolem0011),skolem0011))|r1)),inference(skolemize,[status(esa)],[c75])).])).
% 39.81/40.09 cnf(c79,plain,~is_a_theorem(implies(or(skolem0011,skolem0011),skolem0011))|r1,inference(split_conjunct,[status(thm)],[c77])).
% 39.81/40.09 fof(hilbert_modus_ponens,axiom,modus_ponens,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_modus_ponens)).
% 39.81/40.09 cnf(c26,plain,modus_ponens,inference(split_conjunct,[status(thm)],[hilbert_modus_ponens])).
% 39.81/40.09 fof(hilbert_implies_1,axiom,implies_1,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_implies_1)).
% 39.81/40.09 cnf(c24,plain,implies_1,inference(split_conjunct,[status(thm)],[hilbert_implies_1])).
% 39.81/40.09 fof(implies_1,axiom,(implies_1<=>(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,X)))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', implies_1)).
% 39.81/40.09 fof(c182,plain,((~implies_1|(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,X))))))&((?[X]:(?[Y]:~is_a_theorem(implies(X,implies(Y,X)))))|implies_1)),inference(fof_nnf,[status(thm)],[implies_1])).
% 39.81/40.09 fof(c183,plain,((~implies_1|(![X106]:(![X107]:is_a_theorem(implies(X106,implies(X107,X106))))))&((?[X108]:(?[X109]:~is_a_theorem(implies(X108,implies(X109,X108)))))|implies_1)),inference(variable_rename,[status(thm)],[c182])).
% 39.81/40.09 fof(c185,plain,(![X106]:(![X107]:((~implies_1|is_a_theorem(implies(X106,implies(X107,X106))))&(~is_a_theorem(implies(skolem0048,implies(skolem0049,skolem0048)))|implies_1)))),inference(shift_quantors,[status(thm)],[fof(c184,plain,((~implies_1|(![X106]:(![X107]:is_a_theorem(implies(X106,implies(X107,X106))))))&(~is_a_theorem(implies(skolem0048,implies(skolem0049,skolem0048)))|implies_1)),inference(skolemize,[status(esa)],[c183])).])).
% 39.81/40.09 cnf(c186,plain,~implies_1|is_a_theorem(implies(X179,implies(X178,X179))),inference(split_conjunct,[status(thm)],[c185])).
% 39.81/40.09 cnf(c229,plain,is_a_theorem(implies(X180,implies(X181,X180))),inference(resolution,[status(thm)],[c186, c24])).
% 39.81/40.09 fof(modus_ponens,axiom,(modus_ponens<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))=>is_a_theorem(Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', modus_ponens)).
% 39.81/40.09 fof(c202,plain,((~modus_ponens|(![X]:(![Y]:((~is_a_theorem(X)|~is_a_theorem(implies(X,Y)))|is_a_theorem(Y)))))&((?[X]:(?[Y]:((is_a_theorem(X)&is_a_theorem(implies(X,Y)))&~is_a_theorem(Y))))|modus_ponens)),inference(fof_nnf,[status(thm)],[modus_ponens])).
% 39.81/40.09 fof(c203,plain,((~modus_ponens|(![X118]:(![X119]:((~is_a_theorem(X118)|~is_a_theorem(implies(X118,X119)))|is_a_theorem(X119)))))&((?[X120]:(?[X121]:((is_a_theorem(X120)&is_a_theorem(implies(X120,X121)))&~is_a_theorem(X121))))|modus_ponens)),inference(variable_rename,[status(thm)],[c202])).
% 39.81/40.09 fof(c205,plain,(![X118]:(![X119]:((~modus_ponens|((~is_a_theorem(X118)|~is_a_theorem(implies(X118,X119)))|is_a_theorem(X119)))&(((is_a_theorem(skolem0054)&is_a_theorem(implies(skolem0054,skolem0055)))&~is_a_theorem(skolem0055))|modus_ponens)))),inference(shift_quantors,[status(thm)],[fof(c204,plain,((~modus_ponens|(![X118]:(![X119]:((~is_a_theorem(X118)|~is_a_theorem(implies(X118,X119)))|is_a_theorem(X119)))))&(((is_a_theorem(skolem0054)&is_a_theorem(implies(skolem0054,skolem0055)))&~is_a_theorem(skolem0055))|modus_ponens)),inference(skolemize,[status(esa)],[c203])).])).
% 39.81/40.09 fof(c206,plain,(![X118]:(![X119]:((~modus_ponens|((~is_a_theorem(X118)|~is_a_theorem(implies(X118,X119)))|is_a_theorem(X119)))&(((is_a_theorem(skolem0054)|modus_ponens)&(is_a_theorem(implies(skolem0054,skolem0055))|modus_ponens))&(~is_a_theorem(skolem0055)|modus_ponens))))),inference(distribute,[status(thm)],[c205])).
% 39.81/40.09 cnf(c207,plain,~modus_ponens|~is_a_theorem(X219)|~is_a_theorem(implies(X219,X218))|is_a_theorem(X218),inference(split_conjunct,[status(thm)],[c206])).
% 39.81/40.09 fof(hilbert_implies_2,axiom,implies_2,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_implies_2)).
% 39.81/40.09 cnf(c23,plain,implies_2,inference(split_conjunct,[status(thm)],[hilbert_implies_2])).
% 39.81/40.09 fof(implies_2,axiom,(implies_2<=>(![X]:(![Y]:is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', implies_2)).
% 39.81/40.09 fof(c176,plain,((~implies_2|(![X]:(![Y]:is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))))))&((?[X]:(?[Y]:~is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))))|implies_2)),inference(fof_nnf,[status(thm)],[implies_2])).
% 39.81/40.09 fof(c177,plain,((~implies_2|(![X102]:(![X103]:is_a_theorem(implies(implies(X102,implies(X102,X103)),implies(X102,X103))))))&((?[X104]:(?[X105]:~is_a_theorem(implies(implies(X104,implies(X104,X105)),implies(X104,X105)))))|implies_2)),inference(variable_rename,[status(thm)],[c176])).
% 39.81/40.09 fof(c179,plain,(![X102]:(![X103]:((~implies_2|is_a_theorem(implies(implies(X102,implies(X102,X103)),implies(X102,X103))))&(~is_a_theorem(implies(implies(skolem0046,implies(skolem0046,skolem0047)),implies(skolem0046,skolem0047)))|implies_2)))),inference(shift_quantors,[status(thm)],[fof(c178,plain,((~implies_2|(![X102]:(![X103]:is_a_theorem(implies(implies(X102,implies(X102,X103)),implies(X102,X103))))))&(~is_a_theorem(implies(implies(skolem0046,implies(skolem0046,skolem0047)),implies(skolem0046,skolem0047)))|implies_2)),inference(skolemize,[status(esa)],[c177])).])).
% 39.81/40.09 cnf(c180,plain,~implies_2|is_a_theorem(implies(implies(X477,implies(X477,X478)),implies(X477,X478))),inference(split_conjunct,[status(thm)],[c179])).
% 39.81/40.09 cnf(c577,plain,is_a_theorem(implies(implies(X479,implies(X479,X480)),implies(X479,X480))),inference(resolution,[status(thm)],[c180, c23])).
% 39.81/40.09 cnf(c583,plain,~modus_ponens|~is_a_theorem(implies(X1221,implies(X1221,X1220)))|is_a_theorem(implies(X1221,X1220)),inference(resolution,[status(thm)],[c577, c207])).
% 39.81/40.09 cnf(c1834,plain,~modus_ponens|is_a_theorem(implies(X1222,X1222)),inference(resolution,[status(thm)],[c583, c229])).
% 39.81/40.09 cnf(c1838,plain,is_a_theorem(implies(X1227,X1227)),inference(resolution,[status(thm)],[c1834, c26])).
% 39.81/40.09 fof(hilbert_or_3,axiom,or_3,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_or_3)).
% 39.81/40.09 cnf(c16,plain,or_3,inference(split_conjunct,[status(thm)],[hilbert_or_3])).
% 39.81/40.09 fof(or_3,axiom,(or_3<=>(![X]:(![Y]:(![Z]:is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', or_3)).
% 39.81/40.09 fof(c134,plain,((~or_3|(![X]:(![Y]:(![Z]:is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))))))&((?[X]:(?[Y]:(?[Z]:~is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))))))|or_3)),inference(fof_nnf,[status(thm)],[or_3])).
% 39.81/40.09 fof(c135,plain,((~or_3|(![X70]:(![X71]:(![X72]:is_a_theorem(implies(implies(X70,X72),implies(implies(X71,X72),implies(or(X70,X71),X72))))))))&((?[X73]:(?[X74]:(?[X75]:~is_a_theorem(implies(implies(X73,X75),implies(implies(X74,X75),implies(or(X73,X74),X75)))))))|or_3)),inference(variable_rename,[status(thm)],[c134])).
% 39.81/40.09 fof(c137,plain,(![X70]:(![X71]:(![X72]:((~or_3|is_a_theorem(implies(implies(X70,X72),implies(implies(X71,X72),implies(or(X70,X71),X72)))))&(~is_a_theorem(implies(implies(skolem0030,skolem0032),implies(implies(skolem0031,skolem0032),implies(or(skolem0030,skolem0031),skolem0032))))|or_3))))),inference(shift_quantors,[status(thm)],[fof(c136,plain,((~or_3|(![X70]:(![X71]:(![X72]:is_a_theorem(implies(implies(X70,X72),implies(implies(X71,X72),implies(or(X70,X71),X72))))))))&(~is_a_theorem(implies(implies(skolem0030,skolem0032),implies(implies(skolem0031,skolem0032),implies(or(skolem0030,skolem0031),skolem0032))))|or_3)),inference(skolemize,[status(esa)],[c135])).])).
% 39.81/40.10 cnf(c138,plain,~or_3|is_a_theorem(implies(implies(X407,X408),implies(implies(X409,X408),implies(or(X407,X409),X408)))),inference(split_conjunct,[status(thm)],[c137])).
% 39.81/40.10 cnf(c469,plain,is_a_theorem(implies(implies(X1873,X1874),implies(implies(X1872,X1874),implies(or(X1873,X1872),X1874)))),inference(resolution,[status(thm)],[c138, c16])).
% 39.81/40.10 cnf(c3502,plain,~modus_ponens|is_a_theorem(implies(implies(X6936,X6937),implies(or(X6936,X6936),X6937))),inference(resolution,[status(thm)],[c469, c583])).
% 39.81/40.10 cnf(c28684,plain,is_a_theorem(implies(implies(X6939,X6938),implies(or(X6939,X6939),X6938))),inference(resolution,[status(thm)],[c3502, c26])).
% 39.81/40.10 cnf(c28690,plain,~modus_ponens|~is_a_theorem(implies(X9758,X9757))|is_a_theorem(implies(or(X9758,X9758),X9757)),inference(resolution,[status(thm)],[c28684, c207])).
% 39.81/40.10 cnf(c47749,plain,~modus_ponens|is_a_theorem(implies(or(X9759,X9759),X9759)),inference(resolution,[status(thm)],[c28690, c1838])).
% 39.81/40.10 cnf(c47819,plain,is_a_theorem(implies(or(X9760,X9760),X9760)),inference(resolution,[status(thm)],[c47749, c26])).
% 39.81/40.10 cnf(c47831,plain,r1,inference(resolution,[status(thm)],[c47819, c79])).
% 39.81/40.10 cnf(c47855,plain,$false,inference(resolution,[status(thm)],[c47831, c8])).
% 39.81/40.10 % SZS output end CNFRefutation
% 39.81/40.10
% 39.81/40.10 % Initial clauses : 91
% 39.81/40.10 % Processed clauses : 1778
% 39.81/40.10 % Factors computed : 5
% 39.81/40.10 % Resolvents computed: 47640
% 39.81/40.10 % Tautologies deleted: 4
% 39.81/40.10 % Forward subsumed : 1780
% 39.81/40.10 % Backward subsumed : 416
% 39.81/40.10 % -------- CPU Time ---------
% 39.81/40.10 % User time : 39.572 s
% 39.81/40.10 % System time : 0.155 s
% 39.81/40.10 % Total time : 39.727 s
%------------------------------------------------------------------------------