%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL459+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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.89s 1.17s
% Output : CNFRefutation 0.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL459+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 4 14:30:23 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.15/0.42 (re.compile("\."), Token.FullStop),
% 0.15/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.15/0.43 (re.compile("\("), Token.OpenPar),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.15/0.43 (re.compile("\)"), Token.ClosePar),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.15/0.43 (re.compile("\["), Token.OpenSquare),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.15/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.43 (re.compile("~\|"), Token.Nor),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.43 (re.compile("\|"), Token.Or),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.15/0.43 (re.compile("\?"), Token.Existential),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.15/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.15/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.15/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.15/0.49 """
% 0.26/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.26/0.50 """
% 0.26/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.26/0.58 """
% 0.89/1.17 % Version: 1.5
% 0.89/1.17 % SZS status Theorem
% 0.89/1.17 % SZS output start CNFRefutation
% 0.89/1.17 fof(rosser_kn1,conjecture,kn1,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rosser_kn1)).
% 0.89/1.17 fof(c6,negated_conjecture,(~kn1),inference(assume_negation,[status(cth)],[rosser_kn1])).
% 0.89/1.17 fof(c7,negated_conjecture,~kn1,inference(fof_simplification,[status(thm)],[c6])).
% 0.89/1.17 cnf(c8,negated_conjecture,~kn1,inference(split_conjunct,[status(thm)],[c7])).
% 0.89/1.17 fof(kn1,axiom,(kn1<=>(![P]:is_a_theorem(implies(P,and(P,P))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', kn1)).
% 0.89/1.17 fof(c110,plain,((~kn1|(![P]:is_a_theorem(implies(P,and(P,P)))))&((?[P]:~is_a_theorem(implies(P,and(P,P))))|kn1)),inference(fof_nnf,[status(thm)],[kn1])).
% 0.89/1.17 fof(c111,plain,((~kn1|(![X56]:is_a_theorem(implies(X56,and(X56,X56)))))&((?[X57]:~is_a_theorem(implies(X57,and(X57,X57))))|kn1)),inference(variable_rename,[status(thm)],[c110])).
% 0.89/1.17 fof(c113,plain,(![X56]:((~kn1|is_a_theorem(implies(X56,and(X56,X56))))&(~is_a_theorem(implies(skolem0023,and(skolem0023,skolem0023)))|kn1))),inference(shift_quantors,[status(thm)],[fof(c112,plain,((~kn1|(![X56]:is_a_theorem(implies(X56,and(X56,X56)))))&(~is_a_theorem(implies(skolem0023,and(skolem0023,skolem0023)))|kn1)),inference(skolemize,[status(esa)],[c111])).])).
% 0.89/1.17 cnf(c115,plain,~is_a_theorem(implies(skolem0023,and(skolem0023,skolem0023)))|kn1,inference(split_conjunct,[status(thm)],[c113])).
% 0.89/1.17 fof(hilbert_modus_ponens,axiom,modus_ponens,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_modus_ponens)).
% 0.89/1.17 cnf(c26,plain,modus_ponens,inference(split_conjunct,[status(thm)],[hilbert_modus_ponens])).
% 0.89/1.17 fof(hilbert_and_3,axiom,and_3,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_and_3)).
% 0.89/1.17 cnf(c19,plain,and_3,inference(split_conjunct,[status(thm)],[hilbert_and_3])).
% 0.89/1.17 fof(and_3,axiom,(and_3<=>(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,and(X,Y))))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', and_3)).
% 0.89/1.17 fof(c152,plain,((~and_3|(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,and(X,Y)))))))&((?[X]:(?[Y]:~is_a_theorem(implies(X,implies(Y,and(X,Y))))))|and_3)),inference(fof_nnf,[status(thm)],[and_3])).
% 0.89/1.17 fof(c153,plain,((~and_3|(![X84]:(![X85]:is_a_theorem(implies(X84,implies(X85,and(X84,X85)))))))&((?[X86]:(?[X87]:~is_a_theorem(implies(X86,implies(X87,and(X86,X87))))))|and_3)),inference(variable_rename,[status(thm)],[c152])).
% 0.89/1.17 fof(c155,plain,(![X84]:(![X85]:((~and_3|is_a_theorem(implies(X84,implies(X85,and(X84,X85)))))&(~is_a_theorem(implies(skolem0037,implies(skolem0038,and(skolem0037,skolem0038))))|and_3)))),inference(shift_quantors,[status(thm)],[fof(c154,plain,((~and_3|(![X84]:(![X85]:is_a_theorem(implies(X84,implies(X85,and(X84,X85)))))))&(~is_a_theorem(implies(skolem0037,implies(skolem0038,and(skolem0037,skolem0038))))|and_3)),inference(skolemize,[status(esa)],[c153])).])).
% 0.89/1.17 cnf(c156,plain,~and_3|is_a_theorem(implies(X203,implies(X204,and(X203,X204)))),inference(split_conjunct,[status(thm)],[c155])).
% 0.89/1.17 cnf(c235,plain,is_a_theorem(implies(X205,implies(X206,and(X205,X206)))),inference(resolution,[status(thm)],[c156, c19])).
% 0.89/1.17 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)).
% 0.89/1.17 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])).
% 0.89/1.17 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])).
% 0.89/1.17 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])).])).
% 0.89/1.18 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])).
% 0.89/1.18 cnf(c207,plain,~modus_ponens|~is_a_theorem(X209)|~is_a_theorem(implies(X209,X210))|is_a_theorem(X210),inference(split_conjunct,[status(thm)],[c206])).
% 0.89/1.18 fof(hilbert_implies_2,axiom,implies_2,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_implies_2)).
% 0.89/1.18 cnf(c23,plain,implies_2,inference(split_conjunct,[status(thm)],[hilbert_implies_2])).
% 0.89/1.18 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)).
% 0.89/1.18 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])).
% 0.89/1.18 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])).
% 0.89/1.18 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])).])).
% 0.89/1.18 cnf(c180,plain,~implies_2|is_a_theorem(implies(implies(X468,implies(X468,X469)),implies(X468,X469))),inference(split_conjunct,[status(thm)],[c179])).
% 0.89/1.18 cnf(c542,plain,is_a_theorem(implies(implies(X470,implies(X470,X471)),implies(X470,X471))),inference(resolution,[status(thm)],[c180, c23])).
% 0.89/1.18 cnf(c547,plain,~modus_ponens|~is_a_theorem(implies(X989,implies(X989,X988)))|is_a_theorem(implies(X989,X988)),inference(resolution,[status(thm)],[c542, c207])).
% 0.89/1.18 cnf(c1129,plain,~modus_ponens|is_a_theorem(implies(X1013,and(X1013,X1013))),inference(resolution,[status(thm)],[c547, c235])).
% 0.89/1.18 cnf(c1145,plain,is_a_theorem(implies(X1014,and(X1014,X1014))),inference(resolution,[status(thm)],[c1129, c26])).
% 0.89/1.18 cnf(c1150,plain,kn1,inference(resolution,[status(thm)],[c1145, c115])).
% 0.89/1.18 cnf(c1154,plain,$false,inference(resolution,[status(thm)],[c1150, c8])).
% 0.89/1.18 % SZS output end CNFRefutation
% 0.89/1.18
% 0.89/1.18 % Initial clauses : 91
% 0.89/1.18 % Processed clauses : 297
% 0.89/1.18 % Factors computed : 5
% 0.89/1.18 % Resolvents computed: 939
% 0.89/1.18 % Tautologies deleted: 4
% 0.89/1.18 % Forward subsumed : 60
% 0.89/1.18 % Backward subsumed : 94
% 0.89/1.18 % -------- CPU Time ---------
% 0.89/1.18 % User time : 0.778 s
% 0.89/1.18 % System time : 0.029 s
% 0.89/1.18 % Total time : 0.807 s
%------------------------------------------------------------------------------