%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL460+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:34 PM UTC 2026
% Result : Theorem 0.39s 0.68s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL460+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.37 % Computer : n020.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 5 10:28:57 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.43 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.11/0.43 (re.compile("\."), Token.FullStop),
% 0.11/0.43 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.11/0.43 (re.compile("\("), Token.OpenPar),
% 0.11/0.43 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.11/0.43 (re.compile("\)"), Token.ClosePar),
% 0.11/0.43 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.11/0.43 (re.compile("\["), Token.OpenSquare),
% 0.11/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.11/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.11/0.43 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.43 (re.compile("~\|"), Token.Nor),
% 0.11/0.43 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.43 (re.compile("\|"), Token.Or),
% 0.11/0.43 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.11/0.43 (re.compile("\?"), Token.Existential),
% 0.11/0.43 /export/starexec/sandbox/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/sandbox/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/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.23/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.32/0.60 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.60 """
% 0.39/0.68 % Version: 1.5
% 0.39/0.68 % SZS status Theorem
% 0.39/0.68 % SZS output start CNFRefutation
% 0.39/0.68 fof(rosser_kn2,conjecture,kn2,file('/export/starexec/sandbox/benchmark/theBenchmark.p', rosser_kn2)).
% 0.39/0.68 fof(c6,negated_conjecture,(~kn2),inference(assume_negation,[status(cth)],[rosser_kn2])).
% 0.39/0.68 fof(c7,negated_conjecture,~kn2,inference(fof_simplification,[status(thm)],[c6])).
% 0.39/0.68 cnf(c8,negated_conjecture,~kn2,inference(split_conjunct,[status(thm)],[c7])).
% 0.39/0.68 fof(hilbert_and_1,axiom,and_1,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+2.ax', hilbert_and_1)).
% 0.39/0.68 cnf(c21,plain,and_1,inference(split_conjunct,[status(thm)],[hilbert_and_1])).
% 0.39/0.68 fof(and_1,axiom,(and_1<=>(![X]:(![Y]:is_a_theorem(implies(and(X,Y),X))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', and_1)).
% 0.39/0.68 fof(c164,plain,((~and_1|(![X]:(![Y]:is_a_theorem(implies(and(X,Y),X)))))&((?[X]:(?[Y]:~is_a_theorem(implies(and(X,Y),X))))|and_1)),inference(fof_nnf,[status(thm)],[and_1])).
% 0.39/0.68 fof(c165,plain,((~and_1|(![X92]:(![X93]:is_a_theorem(implies(and(X92,X93),X92)))))&((?[X94]:(?[X95]:~is_a_theorem(implies(and(X94,X95),X94))))|and_1)),inference(variable_rename,[status(thm)],[c164])).
% 0.39/0.68 fof(c167,plain,(![X92]:(![X93]:((~and_1|is_a_theorem(implies(and(X92,X93),X92)))&(~is_a_theorem(implies(and(skolem0041,skolem0042),skolem0041))|and_1)))),inference(shift_quantors,[status(thm)],[fof(c166,plain,((~and_1|(![X92]:(![X93]:is_a_theorem(implies(and(X92,X93),X92)))))&(~is_a_theorem(implies(and(skolem0041,skolem0042),skolem0041))|and_1)),inference(skolemize,[status(esa)],[c165])).])).
% 0.39/0.68 cnf(c168,plain,~and_1|is_a_theorem(implies(and(X172,X173),X172)),inference(split_conjunct,[status(thm)],[c167])).
% 0.39/0.68 cnf(c227,plain,is_a_theorem(implies(and(X174,X175),X174)),inference(resolution,[status(thm)],[c168, c21])).
% 0.39/0.68 fof(kn2,axiom,(kn2<=>(![P]:(![Q]:is_a_theorem(implies(and(P,Q),P))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', kn2)).
% 0.39/0.68 fof(c104,plain,((~kn2|(![P]:(![Q]:is_a_theorem(implies(and(P,Q),P)))))&((?[P]:(?[Q]:~is_a_theorem(implies(and(P,Q),P))))|kn2)),inference(fof_nnf,[status(thm)],[kn2])).
% 0.39/0.68 fof(c105,plain,((~kn2|(![X52]:(![X53]:is_a_theorem(implies(and(X52,X53),X52)))))&((?[X54]:(?[X55]:~is_a_theorem(implies(and(X54,X55),X54))))|kn2)),inference(variable_rename,[status(thm)],[c104])).
% 0.39/0.68 fof(c107,plain,(![X52]:(![X53]:((~kn2|is_a_theorem(implies(and(X52,X53),X52)))&(~is_a_theorem(implies(and(skolem0021,skolem0022),skolem0021))|kn2)))),inference(shift_quantors,[status(thm)],[fof(c106,plain,((~kn2|(![X52]:(![X53]:is_a_theorem(implies(and(X52,X53),X52)))))&(~is_a_theorem(implies(and(skolem0021,skolem0022),skolem0021))|kn2)),inference(skolemize,[status(esa)],[c105])).])).
% 0.39/0.68 cnf(c109,plain,~is_a_theorem(implies(and(skolem0021,skolem0022),skolem0021))|kn2,inference(split_conjunct,[status(thm)],[c107])).
% 0.39/0.68 cnf(c231,plain,kn2,inference(resolution,[status(thm)],[c109, c227])).
% 0.39/0.68 cnf(c233,plain,$false,inference(resolution,[status(thm)],[c231, c8])).
% 0.39/0.68 % SZS output end CNFRefutation
% 0.39/0.68
% 0.39/0.68 % Initial clauses : 91
% 0.39/0.68 % Processed clauses : 53
% 0.39/0.68 % Factors computed : 5
% 0.39/0.68 % Resolvents computed: 18
% 0.39/0.68 % Tautologies deleted: 3
% 0.39/0.68 % Forward subsumed : 11
% 0.39/0.68 % Backward subsumed : 8
% 0.39/0.68 % -------- CPU Time ---------
% 0.39/0.68 % User time : 0.276 s
% 0.39/0.68 % System time : 0.029 s
% 0.39/0.68 % Total time : 0.305 s
%------------------------------------------------------------------------------