%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL491+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:36 PM UTC 2026
% Result : Theorem 0.40s 0.66s
% Output : CNFRefutation 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL491+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 4 14:10:06 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.42 (re.compile("\."), Token.FullStop),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.42 (re.compile("\("), Token.OpenPar),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.42 (re.compile("\)"), Token.ClosePar),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.42 (re.compile("\["), Token.OpenSquare),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("~\|"), Token.Nor),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("\|"), Token.Or),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.23/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.33/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.58 """
% 0.40/0.66 % Version: 1.5
% 0.40/0.66 % SZS status Theorem
% 0.40/0.66 % SZS output start CNFRefutation
% 0.40/0.66 fof(hilbert_or_2,conjecture,or_2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', hilbert_or_2)).
% 0.40/0.66 fof(c6,negated_conjecture,(~or_2),inference(assume_negation,[status(cth)],[hilbert_or_2])).
% 0.40/0.66 fof(c7,negated_conjecture,~or_2,inference(fof_simplification,[status(thm)],[c6])).
% 0.40/0.66 cnf(c8,negated_conjecture,~or_2,inference(split_conjunct,[status(thm)],[c7])).
% 0.40/0.66 fof(principia_r2,axiom,r2,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+4.ax', principia_r2)).
% 0.40/0.66 cnf(c16,plain,r2,inference(split_conjunct,[status(thm)],[principia_r2])).
% 0.40/0.66 fof(r2,axiom,(r2<=>(![P]:(![Q]:is_a_theorem(implies(Q,or(P,Q)))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', r2)).
% 0.40/0.66 fof(c60,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.40/0.66 fof(c61,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)],[c60])).
% 0.40/0.66 fof(c63,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(c62,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)],[c61])).])).
% 0.40/0.66 cnf(c64,plain,~r2|is_a_theorem(implies(X139,or(X140,X139))),inference(split_conjunct,[status(thm)],[c63])).
% 0.40/0.66 cnf(c209,plain,is_a_theorem(implies(X146,or(X145,X146))),inference(resolution,[status(thm)],[c64, c16])).
% 0.40/0.66 fof(or_2,axiom,(or_2<=>(![X]:(![Y]:is_a_theorem(implies(Y,or(X,Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', or_2)).
% 0.40/0.66 fof(c132,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.40/0.66 fof(c133,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)],[c132])).
% 0.40/0.66 fof(c135,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(c134,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)],[c133])).])).
% 0.40/0.66 cnf(c137,plain,~is_a_theorem(implies(skolem0034,or(skolem0033,skolem0034)))|or_2,inference(split_conjunct,[status(thm)],[c135])).
% 0.40/0.66 cnf(c238,plain,or_2,inference(resolution,[status(thm)],[c137, c209])).
% 0.40/0.66 cnf(c239,plain,$false,inference(resolution,[status(thm)],[c238, c8])).
% 0.40/0.66 % SZS output end CNFRefutation
% 0.40/0.66
% 0.40/0.66 % Initial clauses : 83
% 0.40/0.66 % Processed clauses : 48
% 0.40/0.66 % Factors computed : 5
% 0.40/0.66 % Resolvents computed: 32
% 0.40/0.66 % Tautologies deleted: 3
% 0.40/0.66 % Forward subsumed : 12
% 0.40/0.66 % Backward subsumed : 5
% 0.40/0.66 % -------- CPU Time ---------
% 0.40/0.66 % User time : 0.280 s
% 0.40/0.66 % System time : 0.024 s
% 0.40/0.66 % Total time : 0.304 s
%------------------------------------------------------------------------------