%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL484+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 74.43s 74.87s
% Output : CNFRefutation 74.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL484+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 : n005.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 09:43:36 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.15/0.43 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.15/0.43 (re.compile("\."), Token.FullStop),
% 0.15/0.43 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.15/0.43 (re.compile("\("), Token.OpenPar),
% 0.15/0.43 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.15/0.43 (re.compile("\)"), Token.ClosePar),
% 0.15/0.43 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.15/0.43 (re.compile("\["), Token.OpenSquare),
% 0.15/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.15/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.15/0.43 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.43 (re.compile("~\|"), Token.Nor),
% 0.15/0.43 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.43 (re.compile("\|"), Token.Or),
% 0.15/0.43 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.15/0.43 (re.compile("\?"), Token.Existential),
% 0.15/0.43 /export/starexec/sandbox/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/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.15/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.25/0.50 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.50 """
% 0.25/0.51 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.51 """
% 0.36/0.60 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.36/0.60 """
% 74.43/74.87 % Version: 1.5
% 74.43/74.87 % SZS status Theorem
% 74.43/74.87 % SZS output start CNFRefutation
% 74.43/74.87 fof(hilbert_implies_1,conjecture,implies_1,file('/export/starexec/sandbox/benchmark/theBenchmark.p', hilbert_implies_1)).
% 74.43/74.87 fof(c6,negated_conjecture,(~implies_1),inference(assume_negation,[status(cth)],[hilbert_implies_1])).
% 74.43/74.87 fof(c7,negated_conjecture,~implies_1,inference(fof_simplification,[status(thm)],[c6])).
% 74.43/74.87 cnf(c8,negated_conjecture,~implies_1,inference(split_conjunct,[status(thm)],[c7])).
% 74.43/74.87 fof(implies_1,axiom,(implies_1<=>(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,X)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', implies_1)).
% 74.43/74.87 fof(c174,plain,((~implies_1|(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,X))))))&((?[X]:(?[Y]:~is_a_theorem(implies(X,implies(Y,X)))))|implies_1)),inference(fof_nnf,[status(thm)],[implies_1])).
% 74.43/74.87 fof(c175,plain,((~implies_1|(![X106]:(![X107]:is_a_theorem(implies(X106,implies(X107,X106))))))&((?[X108]:(?[X109]:~is_a_theorem(implies(X108,implies(X109,X108)))))|implies_1)),inference(variable_rename,[status(thm)],[c174])).
% 74.43/74.87 fof(c177,plain,(![X106]:(![X107]:((~implies_1|is_a_theorem(implies(X106,implies(X107,X106))))&(~is_a_theorem(implies(skolem0048,implies(skolem0049,skolem0048)))|implies_1)))),inference(shift_quantors,[status(thm)],[fof(c176,plain,((~implies_1|(![X106]:(![X107]:is_a_theorem(implies(X106,implies(X107,X106))))))&(~is_a_theorem(implies(skolem0048,implies(skolem0049,skolem0048)))|implies_1)),inference(skolemize,[status(esa)],[c175])).])).
% 74.43/74.87 cnf(c179,plain,~is_a_theorem(implies(skolem0048,implies(skolem0049,skolem0048)))|implies_1,inference(split_conjunct,[status(thm)],[c177])).
% 74.43/74.87 cnf(c5,axiom,X137!=X136|~is_a_theorem(X137)|is_a_theorem(X136),theory(equality)).
% 74.43/74.87 cnf(symmetry,axiom,X124!=X123|X123=X124,theory(equality)).
% 74.43/74.87 fof(principia_op_implies_or,axiom,op_implies_or,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+4.ax', principia_op_implies_or)).
% 74.43/74.87 cnf(c21,plain,op_implies_or,inference(split_conjunct,[status(thm)],[principia_op_implies_or])).
% 74.43/74.87 fof(op_implies_or,axiom,(op_implies_or=>(![X]:(![Y]:implies(X,Y)=or(not(X),Y)))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+1.ax', op_implies_or)).
% 74.43/74.87 fof(c26,plain,(~op_implies_or|(![X]:(![Y]:implies(X,Y)=or(not(X),Y)))),inference(fof_nnf,[status(thm)],[op_implies_or])).
% 74.43/74.87 fof(c28,plain,(![X4]:(![X5]:(~op_implies_or|implies(X4,X5)=or(not(X4),X5)))),inference(shift_quantors,[status(thm)],[fof(c27,plain,(~op_implies_or|(![X4]:(![X5]:implies(X4,X5)=or(not(X4),X5)))),inference(variable_rename,[status(thm)],[c26])).])).
% 74.43/74.87 cnf(c29,plain,~op_implies_or|implies(X174,X175)=or(not(X174),X175),inference(split_conjunct,[status(thm)],[c28])).
% 74.43/74.87 cnf(c216,plain,implies(X180,X181)=or(not(X180),X181),inference(resolution,[status(thm)],[c29, c21])).
% 74.43/74.87 cnf(c223,plain,or(not(X182),X183)=implies(X182,X183),inference(resolution,[status(thm)],[c216, symmetry])).
% 74.43/74.87 cnf(c232,plain,~is_a_theorem(or(not(X252),X253))|is_a_theorem(implies(X252,X253)),inference(resolution,[status(thm)],[c223, c5])).
% 74.43/74.87 fof(principia_modus_ponens,axiom,modus_ponens,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+4.ax', principia_modus_ponens)).
% 74.43/74.87 cnf(c18,plain,modus_ponens,inference(split_conjunct,[status(thm)],[principia_modus_ponens])).
% 74.43/74.87 fof(principia_r3,axiom,r3,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+4.ax', principia_r3)).
% 74.43/74.87 cnf(c15,plain,r3,inference(split_conjunct,[status(thm)],[principia_r3])).
% 74.43/74.87 fof(r3,axiom,(r3<=>(![P]:(![Q]:is_a_theorem(implies(or(P,Q),or(Q,P)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', r3)).
% 74.43/74.87 fof(c54,plain,((~r3|(![P]:(![Q]:is_a_theorem(implies(or(P,Q),or(Q,P))))))&((?[P]:(?[Q]:~is_a_theorem(implies(or(P,Q),or(Q,P)))))|r3)),inference(fof_nnf,[status(thm)],[r3])).
% 74.43/74.87 fof(c55,plain,((~r3|(![X24]:(![X25]:is_a_theorem(implies(or(X24,X25),or(X25,X24))))))&((?[X26]:(?[X27]:~is_a_theorem(implies(or(X26,X27),or(X27,X26)))))|r3)),inference(variable_rename,[status(thm)],[c54])).
% 74.43/74.87 fof(c57,plain,(![X24]:(![X25]:((~r3|is_a_theorem(implies(or(X24,X25),or(X25,X24))))&(~is_a_theorem(implies(or(skolem0007,skolem0008),or(skolem0008,skolem0007)))|r3)))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((~r3|(![X24]:(![X25]:is_a_theorem(implies(or(X24,X25),or(X25,X24))))))&(~is_a_theorem(implies(or(skolem0007,skolem0008),or(skolem0008,skolem0007)))|r3)),inference(skolemize,[status(esa)],[c55])).])).
% 74.43/74.87 cnf(c58,plain,~r3|is_a_theorem(implies(or(X186,X187),or(X187,X186))),inference(split_conjunct,[status(thm)],[c57])).
% 74.43/74.87 cnf(c235,plain,is_a_theorem(implies(or(X188,X189),or(X189,X188))),inference(resolution,[status(thm)],[c58, c15])).
% 74.43/74.87 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)).
% 74.43/74.87 fof(c194,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])).
% 74.43/74.87 fof(c195,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)],[c194])).
% 74.43/74.87 fof(c197,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(c196,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)],[c195])).])).
% 74.43/74.87 fof(c198,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)],[c197])).
% 74.43/74.87 cnf(c199,plain,~modus_ponens|~is_a_theorem(X203)|~is_a_theorem(implies(X203,X202))|is_a_theorem(X202),inference(split_conjunct,[status(thm)],[c198])).
% 74.43/74.87 cnf(c242,plain,~modus_ponens|~is_a_theorem(or(X260,X259))|is_a_theorem(or(X259,X260)),inference(resolution,[status(thm)],[c199, c235])).
% 74.43/74.87 fof(principia_r2,axiom,r2,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+4.ax', principia_r2)).
% 74.43/74.87 cnf(c16,plain,r2,inference(split_conjunct,[status(thm)],[principia_r2])).
% 74.43/74.87 fof(r2,axiom,(r2<=>(![P]:(![Q]:is_a_theorem(implies(Q,or(P,Q)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', r2)).
% 74.43/74.87 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])).
% 74.43/74.87 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])).
% 74.43/74.87 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])).])).
% 74.43/74.87 cnf(c64,plain,~r2|is_a_theorem(implies(X140,or(X139,X140))),inference(split_conjunct,[status(thm)],[c63])).
% 74.43/74.87 cnf(c209,plain,is_a_theorem(implies(X146,or(X145,X146))),inference(resolution,[status(thm)],[c64, c16])).
% 74.43/74.87 cnf(c224,plain,~is_a_theorem(implies(X247,X248))|is_a_theorem(or(not(X247),X248)),inference(resolution,[status(thm)],[c216, c5])).
% 74.43/74.87 cnf(c273,plain,is_a_theorem(or(not(X250),or(X249,X250))),inference(resolution,[status(thm)],[c224, c209])).
% 74.43/74.87 cnf(c296,plain,~modus_ponens|is_a_theorem(or(or(X261,X262),not(X262))),inference(resolution,[status(thm)],[c242, c273])).
% 74.43/74.87 cnf(c298,plain,is_a_theorem(or(or(X264,X263),not(X263))),inference(resolution,[status(thm)],[c296, c18])).
% 74.43/74.87 cnf(reflexivity,axiom,X122=X122,theory(equality)).
% 74.43/74.87 cnf(c4,axiom,X178!=X176|X179!=X177|or(X178,X179)=or(X176,X177),theory(equality)).
% 74.43/74.87 cnf(c218,plain,X243!=X244|or(X243,X242)=or(X244,X242),inference(resolution,[status(thm)],[c4, reflexivity])).
% 74.43/74.87 cnf(c271,plain,or(or(not(X810),X812),X811)=or(implies(X810,X812),X811),inference(resolution,[status(thm)],[c218, c223])).
% 74.43/74.87 cnf(c1177,plain,~is_a_theorem(or(or(not(X11677),X11676),X11678))|is_a_theorem(or(implies(X11677,X11676),X11678)),inference(resolution,[status(thm)],[c271, c5])).
% 74.43/74.87 cnf(c81969,plain,is_a_theorem(or(implies(X11683,X11684),not(X11684))),inference(resolution,[status(thm)],[c1177, c298])).
% 74.43/74.87 cnf(c82030,plain,~modus_ponens|is_a_theorem(or(not(X11728),implies(X11727,X11728))),inference(resolution,[status(thm)],[c81969, c242])).
% 74.43/74.87 cnf(c82906,plain,is_a_theorem(or(not(X11730),implies(X11729,X11730))),inference(resolution,[status(thm)],[c82030, c18])).
% 74.43/74.87 cnf(c82916,plain,is_a_theorem(implies(X11732,implies(X11731,X11732))),inference(resolution,[status(thm)],[c82906, c232])).
% 74.43/74.87 cnf(c82928,plain,implies_1,inference(resolution,[status(thm)],[c82916, c179])).
% 74.43/74.87 cnf(c82952,plain,$false,inference(resolution,[status(thm)],[c82928, c8])).
% 74.43/74.87 % SZS output end CNFRefutation
% 74.43/74.87
% 74.43/74.87 % Initial clauses : 83
% 74.43/74.87 % Processed clauses : 1790
% 74.43/74.87 % Factors computed : 5
% 74.43/74.87 % Resolvents computed: 82871
% 74.43/74.87 % Tautologies deleted: 5
% 74.43/74.87 % Forward subsumed : 2657
% 74.43/74.87 % Backward subsumed : 260
% 74.43/74.87 % -------- CPU Time ---------
% 74.43/74.87 % User time : 74.049 s
% 74.43/74.87 % System time : 0.317 s
% 74.43/74.87 % Total time : 74.366 s
%------------------------------------------------------------------------------