%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL455+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n031.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 0.38s 0.65s
% Output : CNFRefutation 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL455+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.34 % Computer : n031.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 5 06:33:54 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.40 (re.compile("\."), Token.FullStop),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.40 (re.compile("\("), Token.OpenPar),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.40 (re.compile("\)"), Token.ClosePar),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.40 (re.compile("\["), Token.OpenSquare),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.12/0.47 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.47 """
% 0.12/0.48 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.48 """
% 0.25/0.56 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.56 """
% 0.38/0.65 % Version: 1.5
% 0.38/0.65 % SZS status Theorem
% 0.38/0.65 % SZS output start CNFRefutation
% 0.38/0.65 fof(principia_r2,conjecture,r2,file('/export/starexec/sandbox/benchmark/theBenchmark.p', principia_r2)).
% 0.38/0.65 fof(c6,negated_conjecture,(~r2),inference(assume_negation,[status(cth)],[principia_r2])).
% 0.38/0.65 fof(c7,negated_conjecture,~r2,inference(fof_simplification,[status(thm)],[c6])).
% 0.38/0.65 cnf(c8,negated_conjecture,~r2,inference(split_conjunct,[status(thm)],[c7])).
% 0.38/0.65 fof(hilbert_or_2,axiom,or_2,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+2.ax', hilbert_or_2)).
% 0.38/0.65 cnf(c17,plain,or_2,inference(split_conjunct,[status(thm)],[hilbert_or_2])).
% 0.38/0.65 fof(or_2,axiom,(or_2<=>(![X]:(![Y]:is_a_theorem(implies(Y,or(X,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', or_2)).
% 0.38/0.65 fof(c140,plain,((~or_2|(![X]:(![Y]:is_a_theorem(implies(Y,or(X,Y))))))&((?[X]:(?[Y]:~is_a_theorem(implies(Y,or(X,Y)))))|or_2)),inference(fof_nnf,[status(thm)],[or_2])).
% 0.38/0.65 fof(c141,plain,((~or_2|(![X76]:(![X77]:is_a_theorem(implies(X77,or(X76,X77))))))&((?[X78]:(?[X79]:~is_a_theorem(implies(X79,or(X78,X79)))))|or_2)),inference(variable_rename,[status(thm)],[c140])).
% 0.38/0.65 fof(c143,plain,(![X76]:(![X77]:((~or_2|is_a_theorem(implies(X77,or(X76,X77))))&(~is_a_theorem(implies(skolem0034,or(skolem0033,skolem0034)))|or_2)))),inference(shift_quantors,[status(thm)],[fof(c142,plain,((~or_2|(![X76]:(![X77]:is_a_theorem(implies(X77,or(X76,X77))))))&(~is_a_theorem(implies(skolem0034,or(skolem0033,skolem0034)))|or_2)),inference(skolemize,[status(esa)],[c141])).])).
% 0.38/0.65 cnf(c144,plain,~or_2|is_a_theorem(implies(X156,or(X157,X156))),inference(split_conjunct,[status(thm)],[c143])).
% 0.38/0.65 cnf(c222,plain,is_a_theorem(implies(X158,or(X159,X158))),inference(resolution,[status(thm)],[c144, c17])).
% 0.38/0.65 fof(r2,axiom,(r2<=>(![P]:(![Q]:is_a_theorem(implies(Q,or(P,Q)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', r2)).
% 0.38/0.65 fof(c68,plain,((~r2|(![P]:(![Q]:is_a_theorem(implies(Q,or(P,Q))))))&((?[P]:(?[Q]:~is_a_theorem(implies(Q,or(P,Q)))))|r2)),inference(fof_nnf,[status(thm)],[r2])).
% 0.38/0.65 fof(c69,plain,((~r2|(![X28]:(![X29]:is_a_theorem(implies(X29,or(X28,X29))))))&((?[X30]:(?[X31]:~is_a_theorem(implies(X31,or(X30,X31)))))|r2)),inference(variable_rename,[status(thm)],[c68])).
% 0.38/0.65 fof(c71,plain,(![X28]:(![X29]:((~r2|is_a_theorem(implies(X29,or(X28,X29))))&(~is_a_theorem(implies(skolem0010,or(skolem0009,skolem0010)))|r2)))),inference(shift_quantors,[status(thm)],[fof(c70,plain,((~r2|(![X28]:(![X29]:is_a_theorem(implies(X29,or(X28,X29))))))&(~is_a_theorem(implies(skolem0010,or(skolem0009,skolem0010)))|r2)),inference(skolemize,[status(esa)],[c69])).])).
% 0.38/0.65 cnf(c73,plain,~is_a_theorem(implies(skolem0010,or(skolem0009,skolem0010)))|r2,inference(split_conjunct,[status(thm)],[c71])).
% 0.38/0.65 cnf(c247,plain,r2,inference(resolution,[status(thm)],[c73, c222])).
% 0.38/0.65 cnf(c249,plain,$false,inference(resolution,[status(thm)],[c247, c8])).
% 0.38/0.65 % SZS output end CNFRefutation
% 0.38/0.65
% 0.38/0.65 % Initial clauses : 91
% 0.38/0.65 % Processed clauses : 54
% 0.38/0.65 % Factors computed : 5
% 0.38/0.65 % Resolvents computed: 34
% 0.38/0.65 % Tautologies deleted: 3
% 0.38/0.65 % Forward subsumed : 10
% 0.38/0.65 % Backward subsumed : 8
% 0.38/0.65 % -------- CPU Time ---------
% 0.38/0.65 % User time : 0.268 s
% 0.38/0.65 % System time : 0.030 s
% 0.38/0.65 % Total time : 0.298 s
%------------------------------------------------------------------------------