%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL469+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:35 PM UTC 2026
% Result : Theorem 0.46s 0.78s
% Output : CNFRefutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL469+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.02 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.06/0.30 % Computer : n012.cluster.edu
% 0.06/0.30 % Model : x86_64 x86_64
% 0.06/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.30 % Memory : 8046.5625MB
% 0.06/0.30 % OS : Linux 6.8.0-71-generic
% 0.06/0.30 % CPULimit : 300
% 0.06/0.30 % WCLimit : 300
% 0.06/0.30 % DateTime : Fri Sep 4 18:43:57 UTC 2026
% 0.06/0.30 % CPUTime :
% 0.10/0.33 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.10/0.33 (re.compile("\."), Token.FullStop),
% 0.10/0.33 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.10/0.33 (re.compile("\("), Token.OpenPar),
% 0.10/0.33 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.10/0.33 (re.compile("\)"), Token.ClosePar),
% 0.10/0.33 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.10/0.33 (re.compile("\["), Token.OpenSquare),
% 0.10/0.33 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.10/0.33 (re.compile("\]"), Token.CloseSquare),
% 0.10/0.33 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.33 (re.compile("~\|"), Token.Nor),
% 0.10/0.34 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.34 (re.compile("\|"), Token.Or),
% 0.10/0.34 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.10/0.34 (re.compile("\?"), Token.Existential),
% 0.10/0.34 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.10/0.34 (re.compile("\s+"), Token.WhiteSpace),
% 0.10/0.34 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.10/0.34 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.10/0.37 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.10/0.37 """
% 0.10/0.38 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.10/0.38 """
% 0.10/0.42 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.10/0.42 """
% 0.46/0.78 % Version: 1.5
% 0.46/0.78 % SZS status Theorem
% 0.46/0.78 % SZS output start CNFRefutation
% 0.46/0.78 fof(hilbert_or_1,conjecture,or_1,file('/export/starexec/sandbox/benchmark/theBenchmark.p', hilbert_or_1)).
% 0.46/0.78 fof(c6,negated_conjecture,(~or_1),inference(assume_negation,[status(cth)],[hilbert_or_1])).
% 0.46/0.78 fof(c7,negated_conjecture,~or_1,inference(fof_simplification,[status(thm)],[c6])).
% 0.46/0.78 cnf(c8,negated_conjecture,~or_1,inference(split_conjunct,[status(thm)],[c7])).
% 0.46/0.78 fof(or_1,axiom,(or_1<=>(![X]:(![Y]:is_a_theorem(implies(X,or(X,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', or_1)).
% 0.46/0.78 fof(c136,plain,((~or_1|(![X]:(![Y]:is_a_theorem(implies(X,or(X,Y))))))&((?[X]:(?[Y]:~is_a_theorem(implies(X,or(X,Y)))))|or_1)),inference(fof_nnf,[status(thm)],[or_1])).
% 0.46/0.78 fof(c137,plain,((~or_1|(![X80]:(![X81]:is_a_theorem(implies(X80,or(X80,X81))))))&((?[X82]:(?[X83]:~is_a_theorem(implies(X82,or(X82,X83)))))|or_1)),inference(variable_rename,[status(thm)],[c136])).
% 0.46/0.78 fof(c139,plain,(![X80]:(![X81]:((~or_1|is_a_theorem(implies(X80,or(X80,X81))))&(~is_a_theorem(implies(skolem0035,or(skolem0035,skolem0036)))|or_1)))),inference(shift_quantors,[status(thm)],[fof(c138,plain,((~or_1|(![X80]:(![X81]:is_a_theorem(implies(X80,or(X80,X81))))))&(~is_a_theorem(implies(skolem0035,or(skolem0035,skolem0036)))|or_1)),inference(skolemize,[status(esa)],[c137])).])).
% 0.46/0.78 cnf(c141,plain,~is_a_theorem(implies(skolem0035,or(skolem0035,skolem0036)))|or_1,inference(split_conjunct,[status(thm)],[c139])).
% 0.46/0.78 fof(luka_modus_ponens,axiom,modus_ponens,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+3.ax', luka_modus_ponens)).
% 0.46/0.78 cnf(c16,plain,modus_ponens,inference(split_conjunct,[status(thm)],[luka_modus_ponens])).
% 0.46/0.78 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/sandbox/benchmark/Axioms/LCL006+0.ax', modus_ponens)).
% 0.46/0.78 fof(c192,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.46/0.78 fof(c193,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)],[c192])).
% 0.46/0.78 fof(c195,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(c194,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)],[c193])).])).
% 0.46/0.78 fof(c196,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)],[c195])).
% 0.46/0.78 cnf(c197,plain,~modus_ponens|~is_a_theorem(X192)|~is_a_theorem(implies(X192,X193))|is_a_theorem(X193),inference(split_conjunct,[status(thm)],[c196])).
% 0.46/0.78 fof(luka_cn2,axiom,cn2,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+3.ax', luka_cn2)).
% 0.46/0.78 cnf(c14,plain,cn2,inference(split_conjunct,[status(thm)],[luka_cn2])).
% 0.46/0.78 fof(cn2,axiom,(cn2<=>(![P]:(![Q]:is_a_theorem(implies(P,implies(not(P),Q)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', cn2)).
% 0.46/0.78 fof(c76,plain,((~cn2|(![P]:(![Q]:is_a_theorem(implies(P,implies(not(P),Q))))))&((?[P]:(?[Q]:~is_a_theorem(implies(P,implies(not(P),Q)))))|cn2)),inference(fof_nnf,[status(thm)],[cn2])).
% 0.46/0.78 fof(c77,plain,((~cn2|(![X36]:(![X37]:is_a_theorem(implies(X36,implies(not(X36),X37))))))&((?[X38]:(?[X39]:~is_a_theorem(implies(X38,implies(not(X38),X39)))))|cn2)),inference(variable_rename,[status(thm)],[c76])).
% 0.46/0.78 fof(c79,plain,(![X36]:(![X37]:((~cn2|is_a_theorem(implies(X36,implies(not(X36),X37))))&(~is_a_theorem(implies(skolem0013,implies(not(skolem0013),skolem0014)))|cn2)))),inference(shift_quantors,[status(thm)],[fof(c78,plain,((~cn2|(![X36]:(![X37]:is_a_theorem(implies(X36,implies(not(X36),X37))))))&(~is_a_theorem(implies(skolem0013,implies(not(skolem0013),skolem0014)))|cn2)),inference(skolemize,[status(esa)],[c77])).])).
% 0.46/0.78 cnf(c80,plain,~cn2|is_a_theorem(implies(X171,implies(not(X171),X170))),inference(split_conjunct,[status(thm)],[c79])).
% 0.46/0.78 cnf(c213,plain,is_a_theorem(implies(X173,implies(not(X173),X172))),inference(resolution,[status(thm)],[c80, c14])).
% 0.46/0.78 fof(luka_cn1,axiom,cn1,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+3.ax', luka_cn1)).
% 0.46/0.78 cnf(c15,plain,cn1,inference(split_conjunct,[status(thm)],[luka_cn1])).
% 0.46/0.78 fof(cn1,axiom,(cn1<=>(![P]:(![Q]:(![R]:is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', cn1)).
% 0.46/0.78 fof(c82,plain,((~cn1|(![P]:(![Q]:(![R]:is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))))))&((?[P]:(?[Q]:(?[R]:~is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))))))|cn1)),inference(fof_nnf,[status(thm)],[cn1])).
% 0.46/0.78 fof(c83,plain,((~cn1|(![X40]:(![X41]:(![X42]:is_a_theorem(implies(implies(X40,X41),implies(implies(X41,X42),implies(X40,X42))))))))&((?[X43]:(?[X44]:(?[X45]:~is_a_theorem(implies(implies(X43,X44),implies(implies(X44,X45),implies(X43,X45)))))))|cn1)),inference(variable_rename,[status(thm)],[c82])).
% 0.46/0.78 fof(c85,plain,(![X40]:(![X41]:(![X42]:((~cn1|is_a_theorem(implies(implies(X40,X41),implies(implies(X41,X42),implies(X40,X42)))))&(~is_a_theorem(implies(implies(skolem0015,skolem0016),implies(implies(skolem0016,skolem0017),implies(skolem0015,skolem0017))))|cn1))))),inference(shift_quantors,[status(thm)],[fof(c84,plain,((~cn1|(![X40]:(![X41]:(![X42]:is_a_theorem(implies(implies(X40,X41),implies(implies(X41,X42),implies(X40,X42))))))))&(~is_a_theorem(implies(implies(skolem0015,skolem0016),implies(implies(skolem0016,skolem0017),implies(skolem0015,skolem0017))))|cn1)),inference(skolemize,[status(esa)],[c83])).])).
% 0.46/0.78 cnf(c86,plain,~cn1|is_a_theorem(implies(implies(X271,X270),implies(implies(X270,X269),implies(X271,X269)))),inference(split_conjunct,[status(thm)],[c85])).
% 0.46/0.78 cnf(c333,plain,is_a_theorem(implies(implies(X375,X376),implies(implies(X376,X374),implies(X375,X374)))),inference(resolution,[status(thm)],[c86, c15])).
% 0.46/0.78 cnf(c465,plain,~modus_ponens|~is_a_theorem(implies(X607,X609))|is_a_theorem(implies(implies(X609,X608),implies(X607,X608))),inference(resolution,[status(thm)],[c333, c197])).
% 0.46/0.78 cnf(c1296,plain,~modus_ponens|is_a_theorem(implies(implies(implies(not(X614),X615),X616),implies(X614,X616))),inference(resolution,[status(thm)],[c465, c213])).
% 0.46/0.78 cnf(c1302,plain,is_a_theorem(implies(implies(implies(not(X617),X619),X618),implies(X617,X618))),inference(resolution,[status(thm)],[c1296, c16])).
% 0.46/0.78 cnf(c1303,plain,~modus_ponens|~is_a_theorem(implies(implies(not(X640),X639),X641))|is_a_theorem(implies(X640,X641)),inference(resolution,[status(thm)],[c1302, c197])).
% 0.46/0.78 fof(luka_cn3,axiom,cn3,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+3.ax', luka_cn3)).
% 0.46/0.78 cnf(c13,plain,cn3,inference(split_conjunct,[status(thm)],[luka_cn3])).
% 0.46/0.78 fof(cn3,axiom,(cn3<=>(![P]:is_a_theorem(implies(implies(not(P),P),P)))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', cn3)).
% 0.46/0.78 fof(c70,plain,((~cn3|(![P]:is_a_theorem(implies(implies(not(P),P),P))))&((?[P]:~is_a_theorem(implies(implies(not(P),P),P)))|cn3)),inference(fof_nnf,[status(thm)],[cn3])).
% 0.46/0.78 fof(c71,plain,((~cn3|(![X34]:is_a_theorem(implies(implies(not(X34),X34),X34))))&((?[X35]:~is_a_theorem(implies(implies(not(X35),X35),X35)))|cn3)),inference(variable_rename,[status(thm)],[c70])).
% 0.46/0.78 fof(c73,plain,(![X34]:((~cn3|is_a_theorem(implies(implies(not(X34),X34),X34)))&(~is_a_theorem(implies(implies(not(skolem0012),skolem0012),skolem0012))|cn3))),inference(shift_quantors,[status(thm)],[fof(c72,plain,((~cn3|(![X34]:is_a_theorem(implies(implies(not(X34),X34),X34))))&(~is_a_theorem(implies(implies(not(skolem0012),skolem0012),skolem0012))|cn3)),inference(skolemize,[status(esa)],[c71])).])).
% 0.46/0.78 cnf(c74,plain,~cn3|is_a_theorem(implies(implies(not(X164),X164),X164)),inference(split_conjunct,[status(thm)],[c73])).
% 0.46/0.78 cnf(c210,plain,is_a_theorem(implies(implies(not(X165),X165),X165)),inference(resolution,[status(thm)],[c74, c13])).
% 0.46/0.78 cnf(c1392,plain,~modus_ponens|is_a_theorem(implies(X642,X642)),inference(resolution,[status(thm)],[c1303, c210])).
% 0.46/0.78 cnf(c1397,plain,is_a_theorem(implies(X643,X643)),inference(resolution,[status(thm)],[c1392, c16])).
% 0.46/0.78 cnf(c5,axiom,X133!=X132|~is_a_theorem(X133)|is_a_theorem(X132),theory(equality)).
% 0.46/0.78 cnf(reflexivity,axiom,X122=X122,theory(equality)).
% 0.46/0.78 cnf(c0,axiom,X138!=X135|X136!=X137|implies(X138,X136)=implies(X135,X137),theory(equality)).
% 0.46/0.78 cnf(c206,plain,X203!=X202|implies(X203,X204)=implies(X202,X204),inference(resolution,[status(thm)],[c0, reflexivity])).
% 0.46/0.78 fof(hilbert_op_or,axiom,op_or,file('/export/starexec/sandbox/benchmark/theBenchmark.p', hilbert_op_or)).
% 0.46/0.78 cnf(c11,plain,op_or,inference(split_conjunct,[status(thm)],[hilbert_op_or])).
% 0.46/0.78 fof(op_or,axiom,(op_or=>(![X]:(![Y]:or(X,Y)=not(and(not(X),not(Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+1.ax', op_or)).
% 0.46/0.78 fof(c36,plain,(~op_or|(![X]:(![Y]:or(X,Y)=not(and(not(X),not(Y)))))),inference(fof_nnf,[status(thm)],[op_or])).
% 0.46/0.78 fof(c38,plain,(![X10]:(![X11]:(~op_or|or(X10,X11)=not(and(not(X10),not(X11)))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,(~op_or|(![X10]:(![X11]:or(X10,X11)=not(and(not(X10),not(X11)))))),inference(variable_rename,[status(thm)],[c36])).])).
% 0.46/0.78 cnf(c39,plain,~op_or|or(X211,X210)=not(and(not(X211),not(X210))),inference(split_conjunct,[status(thm)],[c38])).
% 0.46/0.78 cnf(c225,plain,or(X248,X247)=not(and(not(X248),not(X247))),inference(resolution,[status(thm)],[c39, c11])).
% 0.46/0.78 cnf(transitivity,axiom,X127!=X126|X126!=X128|X127=X128,theory(equality)).
% 0.46/0.78 cnf(symmetry,axiom,X124!=X123|X123=X124,theory(equality)).
% 0.46/0.78 fof(hilbert_op_implies_and,axiom,op_implies_and,file('/export/starexec/sandbox/benchmark/theBenchmark.p', hilbert_op_implies_and)).
% 0.46/0.78 cnf(c10,plain,op_implies_and,inference(split_conjunct,[status(thm)],[hilbert_op_implies_and])).
% 0.46/0.78 fof(op_implies_and,axiom,(op_implies_and=>(![X]:(![Y]:implies(X,Y)=not(and(X,not(Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+1.ax', op_implies_and)).
% 0.46/0.78 fof(c28,plain,(~op_implies_and|(![X]:(![Y]:implies(X,Y)=not(and(X,not(Y)))))),inference(fof_nnf,[status(thm)],[op_implies_and])).
% 0.46/0.78 fof(c30,plain,(![X6]:(![X7]:(~op_implies_and|implies(X6,X7)=not(and(X6,not(X7)))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,(~op_implies_and|(![X6]:(![X7]:implies(X6,X7)=not(and(X6,not(X7)))))),inference(variable_rename,[status(thm)],[c28])).])).
% 0.46/0.78 cnf(c31,plain,~op_implies_and|implies(X191,X190)=not(and(X191,not(X190))),inference(split_conjunct,[status(thm)],[c30])).
% 0.46/0.78 cnf(c217,plain,implies(X237,X236)=not(and(X237,not(X236))),inference(resolution,[status(thm)],[c31, c10])).
% 0.46/0.78 cnf(c238,plain,not(and(X238,not(X239)))=implies(X238,X239),inference(resolution,[status(thm)],[c217, symmetry])).
% 0.46/0.78 cnf(c251,plain,X297!=not(and(X299,not(X298)))|X297=implies(X299,X298),inference(resolution,[status(thm)],[c238, transitivity])).
% 0.46/0.78 cnf(c364,plain,or(X303,X302)=implies(not(X303),X302),inference(resolution,[status(thm)],[c251, c225])).
% 0.46/0.78 cnf(c368,plain,implies(or(X386,X387),X388)=implies(implies(not(X386),X387),X388),inference(resolution,[status(thm)],[c364, c206])).
% 0.46/0.78 cnf(c484,plain,~is_a_theorem(implies(or(X950,X951),X952))|is_a_theorem(implies(implies(not(X950),X951),X952)),inference(resolution,[status(thm)],[c368, c5])).
% 0.46/0.78 cnf(c2364,plain,is_a_theorem(implies(implies(not(X957),X958),or(X957,X958))),inference(resolution,[status(thm)],[c484, c1397])).
% 0.46/0.78 cnf(c2426,plain,~modus_ponens|is_a_theorem(implies(X960,or(X960,X959))),inference(resolution,[status(thm)],[c2364, c1303])).
% 0.46/0.78 cnf(c2434,plain,is_a_theorem(implies(X961,or(X961,X962))),inference(resolution,[status(thm)],[c2426, c16])).
% 0.46/0.78 cnf(c2438,plain,or_1,inference(resolution,[status(thm)],[c2434, c141])).
% 0.46/0.78 cnf(c2446,plain,$false,inference(resolution,[status(thm)],[c2438, c8])).
% 0.46/0.78 % SZS output end CNFRefutation
% 0.46/0.78
% 0.46/0.78 % Initial clauses : 81
% 0.46/0.78 % Processed clauses : 259
% 0.46/0.78 % Factors computed : 5
% 0.46/0.78 % Resolvents computed: 2241
% 0.46/0.78 % Tautologies deleted: 4
% 0.46/0.78 % Forward subsumed : 131
% 0.46/0.78 % Backward subsumed : 29
% 0.46/0.78 % -------- CPU Time ---------
% 0.46/0.78 % User time : 0.467 s
% 0.46/0.78 % System time : 0.016 s
% 0.46/0.78 % Total time : 0.483 s
%------------------------------------------------------------------------------