%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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:38 PM UTC 2026
% Result : Theorem 0.96s 1.20s
% Output : CNFRefutation 0.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 13:13:20 UTC 2026
% 0.09/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.22/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.32/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 0.96/1.20 % Version: 1.5
% 0.96/1.20 % SZS status Theorem
% 0.96/1.20 % SZS output start CNFRefutation
% 0.96/1.20 fof(s1_0_modus_ponens_strict_implies,conjecture,modus_ponens_strict_implies,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_0_modus_ponens_strict_implies)).
% 0.96/1.20 fof(c10,negated_conjecture,(~modus_ponens_strict_implies),inference(assume_negation,[status(cth)],[s1_0_modus_ponens_strict_implies])).
% 0.96/1.20 fof(c11,negated_conjecture,~modus_ponens_strict_implies,inference(fof_simplification,[status(thm)],[c10])).
% 0.96/1.20 cnf(c12,negated_conjecture,~modus_ponens_strict_implies,inference(split_conjunct,[status(thm)],[c11])).
% 0.96/1.20 fof(modus_ponens_strict_implies,axiom,(modus_ponens_strict_implies<=>(![X]:(![Y]:((is_a_theorem(X)&is_a_theorem(strict_implies(X,Y)))=>is_a_theorem(Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', modus_ponens_strict_implies)).
% 0.96/1.20 fof(c171,plain,((~modus_ponens_strict_implies|(![X]:(![Y]:((~is_a_theorem(X)|~is_a_theorem(strict_implies(X,Y)))|is_a_theorem(Y)))))&((?[X]:(?[Y]:((is_a_theorem(X)&is_a_theorem(strict_implies(X,Y)))&~is_a_theorem(Y))))|modus_ponens_strict_implies)),inference(fof_nnf,[status(thm)],[modus_ponens_strict_implies])).
% 0.96/1.20 fof(c172,plain,((~modus_ponens_strict_implies|(![X80]:(![X81]:((~is_a_theorem(X80)|~is_a_theorem(strict_implies(X80,X81)))|is_a_theorem(X81)))))&((?[X82]:(?[X83]:((is_a_theorem(X82)&is_a_theorem(strict_implies(X82,X83)))&~is_a_theorem(X83))))|modus_ponens_strict_implies)),inference(variable_rename,[status(thm)],[c171])).
% 0.96/1.20 fof(c174,plain,(![X80]:(![X81]:((~modus_ponens_strict_implies|((~is_a_theorem(X80)|~is_a_theorem(strict_implies(X80,X81)))|is_a_theorem(X81)))&(((is_a_theorem(skolem0037)&is_a_theorem(strict_implies(skolem0037,skolem0038)))&~is_a_theorem(skolem0038))|modus_ponens_strict_implies)))),inference(shift_quantors,[status(thm)],[fof(c173,plain,((~modus_ponens_strict_implies|(![X80]:(![X81]:((~is_a_theorem(X80)|~is_a_theorem(strict_implies(X80,X81)))|is_a_theorem(X81)))))&(((is_a_theorem(skolem0037)&is_a_theorem(strict_implies(skolem0037,skolem0038)))&~is_a_theorem(skolem0038))|modus_ponens_strict_implies)),inference(skolemize,[status(esa)],[c172])).])).
% 0.96/1.20 fof(c175,plain,(![X80]:(![X81]:((~modus_ponens_strict_implies|((~is_a_theorem(X80)|~is_a_theorem(strict_implies(X80,X81)))|is_a_theorem(X81)))&(((is_a_theorem(skolem0037)|modus_ponens_strict_implies)&(is_a_theorem(strict_implies(skolem0037,skolem0038))|modus_ponens_strict_implies))&(~is_a_theorem(skolem0038)|modus_ponens_strict_implies))))),inference(distribute,[status(thm)],[c174])).
% 0.96/1.20 cnf(c179,plain,~is_a_theorem(skolem0038)|modus_ponens_strict_implies,inference(split_conjunct,[status(thm)],[c175])).
% 0.96/1.20 fof(hilbert_modus_ponens,axiom,modus_ponens,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_modus_ponens)).
% 0.96/1.20 cnf(c202,plain,modus_ponens,inference(split_conjunct,[status(thm)],[hilbert_modus_ponens])).
% 0.96/1.20 cnf(c177,plain,is_a_theorem(skolem0037)|modus_ponens_strict_implies,inference(split_conjunct,[status(thm)],[c175])).
% 0.96/1.20 cnf(c395,plain,is_a_theorem(skolem0037),inference(resolution,[status(thm)],[c177, c12])).
% 0.96/1.20 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.96/1.20 fof(c378,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.96/1.20 fof(c379,plain,((~modus_ponens|(![X202]:(![X203]:((~is_a_theorem(X202)|~is_a_theorem(implies(X202,X203)))|is_a_theorem(X203)))))&((?[X204]:(?[X205]:((is_a_theorem(X204)&is_a_theorem(implies(X204,X205)))&~is_a_theorem(X205))))|modus_ponens)),inference(variable_rename,[status(thm)],[c378])).
% 0.96/1.20 fof(c381,plain,(![X202]:(![X203]:((~modus_ponens|((~is_a_theorem(X202)|~is_a_theorem(implies(X202,X203)))|is_a_theorem(X203)))&(((is_a_theorem(skolem0093)&is_a_theorem(implies(skolem0093,skolem0094)))&~is_a_theorem(skolem0094))|modus_ponens)))),inference(shift_quantors,[status(thm)],[fof(c380,plain,((~modus_ponens|(![X202]:(![X203]:((~is_a_theorem(X202)|~is_a_theorem(implies(X202,X203)))|is_a_theorem(X203)))))&(((is_a_theorem(skolem0093)&is_a_theorem(implies(skolem0093,skolem0094)))&~is_a_theorem(skolem0094))|modus_ponens)),inference(skolemize,[status(esa)],[c379])).])).
% 0.96/1.20 fof(c382,plain,(![X202]:(![X203]:((~modus_ponens|((~is_a_theorem(X202)|~is_a_theorem(implies(X202,X203)))|is_a_theorem(X203)))&(((is_a_theorem(skolem0093)|modus_ponens)&(is_a_theorem(implies(skolem0093,skolem0094))|modus_ponens))&(~is_a_theorem(skolem0094)|modus_ponens))))),inference(distribute,[status(thm)],[c381])).
% 0.96/1.20 cnf(c383,plain,~modus_ponens|~is_a_theorem(X373)|~is_a_theorem(implies(X373,X372))|is_a_theorem(X372),inference(split_conjunct,[status(thm)],[c382])).
% 0.96/1.20 fof(km5_axiom_M,axiom,axiom_M,file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+2.ax', km5_axiom_M)).
% 0.96/1.20 cnf(c20,plain,axiom_M,inference(split_conjunct,[status(thm)],[km5_axiom_M])).
% 0.96/1.20 fof(axiom_M,axiom,(axiom_M<=>(![X]:is_a_theorem(implies(necessarily(X),X)))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', axiom_M)).
% 0.96/1.20 fof(c142,plain,((~axiom_M|(![X]:is_a_theorem(implies(necessarily(X),X))))&((?[X]:~is_a_theorem(implies(necessarily(X),X)))|axiom_M)),inference(fof_nnf,[status(thm)],[axiom_M])).
% 0.96/1.20 fof(c143,plain,((~axiom_M|(![X66]:is_a_theorem(implies(necessarily(X66),X66))))&((?[X67]:~is_a_theorem(implies(necessarily(X67),X67)))|axiom_M)),inference(variable_rename,[status(thm)],[c142])).
% 0.96/1.20 fof(c145,plain,(![X66]:((~axiom_M|is_a_theorem(implies(necessarily(X66),X66)))&(~is_a_theorem(implies(necessarily(skolem0030),skolem0030))|axiom_M))),inference(shift_quantors,[status(thm)],[fof(c144,plain,((~axiom_M|(![X66]:is_a_theorem(implies(necessarily(X66),X66))))&(~is_a_theorem(implies(necessarily(skolem0030),skolem0030))|axiom_M)),inference(skolemize,[status(esa)],[c143])).])).
% 0.96/1.20 cnf(c146,plain,~axiom_M|is_a_theorem(implies(necessarily(X242),X242)),inference(split_conjunct,[status(thm)],[c145])).
% 0.96/1.20 cnf(c402,plain,is_a_theorem(implies(necessarily(X247),X247)),inference(resolution,[status(thm)],[c146, c20])).
% 0.96/1.20 cnf(c633,plain,~modus_ponens|~is_a_theorem(necessarily(X374))|is_a_theorem(X374),inference(resolution,[status(thm)],[c383, c402])).
% 0.96/1.20 cnf(c178,plain,is_a_theorem(strict_implies(skolem0037,skolem0038))|modus_ponens_strict_implies,inference(split_conjunct,[status(thm)],[c175])).
% 0.96/1.20 cnf(c405,plain,is_a_theorem(strict_implies(skolem0037,skolem0038)),inference(resolution,[status(thm)],[c178, c12])).
% 0.96/1.20 cnf(c9,axiom,X239!=X238|~is_a_theorem(X239)|is_a_theorem(X238),theory(equality)).
% 0.96/1.20 fof(s1_0_op_strict_implies,axiom,op_strict_implies,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_0_op_strict_implies)).
% 0.96/1.20 cnf(c15,plain,op_strict_implies,inference(split_conjunct,[status(thm)],[s1_0_op_strict_implies])).
% 0.96/1.20 fof(op_strict_implies,axiom,(op_strict_implies=>(![X]:(![Y]:strict_implies(X,Y)=necessarily(implies(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+1.ax', op_strict_implies)).
% 0.96/1.20 fof(c28,plain,(~op_strict_implies|(![X]:(![Y]:strict_implies(X,Y)=necessarily(implies(X,Y))))),inference(fof_nnf,[status(thm)],[op_strict_implies])).
% 0.96/1.20 fof(c30,plain,(![X4]:(![X5]:(~op_strict_implies|strict_implies(X4,X5)=necessarily(implies(X4,X5))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,(~op_strict_implies|(![X4]:(![X5]:strict_implies(X4,X5)=necessarily(implies(X4,X5))))),inference(variable_rename,[status(thm)],[c28])).])).
% 0.96/1.20 cnf(c31,plain,~op_strict_implies|strict_implies(X263,X264)=necessarily(implies(X263,X264)),inference(split_conjunct,[status(thm)],[c30])).
% 0.96/1.20 cnf(c424,plain,strict_implies(X301,X300)=necessarily(implies(X301,X300)),inference(resolution,[status(thm)],[c31, c15])).
% 0.96/1.20 cnf(c456,plain,~is_a_theorem(strict_implies(X651,X650))|is_a_theorem(necessarily(implies(X651,X650))),inference(resolution,[status(thm)],[c424, c9])).
% 0.96/1.20 cnf(c1482,plain,is_a_theorem(necessarily(implies(skolem0037,skolem0038))),inference(resolution,[status(thm)],[c456, c405])).
% 0.96/1.20 cnf(c1484,plain,~modus_ponens|is_a_theorem(implies(skolem0037,skolem0038)),inference(resolution,[status(thm)],[c1482, c633])).
% 0.96/1.20 cnf(c1491,plain,is_a_theorem(implies(skolem0037,skolem0038)),inference(resolution,[status(thm)],[c1484, c202])).
% 0.96/1.20 cnf(c1496,plain,~modus_ponens|~is_a_theorem(skolem0037)|is_a_theorem(skolem0038),inference(resolution,[status(thm)],[c1491, c383])).
% 0.96/1.20 cnf(c1500,plain,~modus_ponens|is_a_theorem(skolem0038),inference(resolution,[status(thm)],[c1496, c395])).
% 0.96/1.20 cnf(c1508,plain,is_a_theorem(skolem0038),inference(resolution,[status(thm)],[c1500, c202])).
% 0.96/1.20 cnf(c1515,plain,modus_ponens_strict_implies,inference(resolution,[status(thm)],[c1508, c179])).
% 0.96/1.20 cnf(c1517,plain,$false,inference(resolution,[status(thm)],[c1515, c12])).
% 0.96/1.20 % SZS output end CNFRefutation
% 0.96/1.20
% 0.96/1.20 % Initial clauses : 159
% 0.96/1.20 % Processed clauses : 330
% 0.96/1.20 % Factors computed : 8
% 0.96/1.20 % Resolvents computed: 1123
% 0.96/1.20 % Tautologies deleted: 8
% 0.96/1.20 % Forward subsumed : 97
% 0.96/1.20 % Backward subsumed : 94
% 0.96/1.20 % -------- CPU Time ---------
% 0.96/1.20 % User time : 0.808 s
% 0.96/1.20 % System time : 0.033 s
% 0.96/1.20 % Total time : 0.841 s
%------------------------------------------------------------------------------