%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL544+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:40 PM UTC 2026
% Result : Theorem 33.88s 34.15s
% Output : CNFRefutation 33.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL544+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.36 % Computer : n029.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 20:16:25 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.10/0.42 (re.compile("\."), Token.FullStop),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.10/0.42 (re.compile("\("), Token.OpenPar),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.10/0.42 (re.compile("\)"), Token.ClosePar),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.10/0.42 (re.compile("\["), Token.OpenSquare),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.10/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.42 (re.compile("~\|"), Token.Nor),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.42 (re.compile("\|"), Token.Or),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.10/0.42 (re.compile("\?"), Token.Existential),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.10/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.10/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.32/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 33.88/34.15 % Version: 1.5
% 33.88/34.15 % SZS status Theorem
% 33.88/34.15 % SZS output start CNFRefutation
% 33.88/34.15 fof(s1_0_axiom_m4,conjecture,axiom_m4,file('/export/starexec/sandbox/benchmark/theBenchmark.p', s1_0_axiom_m4)).
% 33.88/34.15 fof(c10,negated_conjecture,(~axiom_m4),inference(assume_negation,[status(cth)],[s1_0_axiom_m4])).
% 33.88/34.15 fof(c11,negated_conjecture,~axiom_m4,inference(fof_simplification,[status(thm)],[c10])).
% 33.88/34.15 cnf(c12,negated_conjecture,~axiom_m4,inference(split_conjunct,[status(thm)],[c11])).
% 33.88/34.15 fof(axiom_m4,axiom,(axiom_m4<=>(![X]:is_a_theorem(strict_implies(X,and(X,X))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL007+0.ax', axiom_m4)).
% 33.88/34.15 fof(c77,plain,((~axiom_m4|(![X]:is_a_theorem(strict_implies(X,and(X,X)))))&((?[X]:~is_a_theorem(strict_implies(X,and(X,X))))|axiom_m4)),inference(fof_nnf,[status(thm)],[axiom_m4])).
% 33.88/34.15 fof(c78,plain,((~axiom_m4|(![X28]:is_a_theorem(strict_implies(X28,and(X28,X28)))))&((?[X29]:~is_a_theorem(strict_implies(X29,and(X29,X29))))|axiom_m4)),inference(variable_rename,[status(thm)],[c77])).
% 33.88/34.15 fof(c80,plain,(![X28]:((~axiom_m4|is_a_theorem(strict_implies(X28,and(X28,X28))))&(~is_a_theorem(strict_implies(skolem0011,and(skolem0011,skolem0011)))|axiom_m4))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((~axiom_m4|(![X28]:is_a_theorem(strict_implies(X28,and(X28,X28)))))&(~is_a_theorem(strict_implies(skolem0011,and(skolem0011,skolem0011)))|axiom_m4)),inference(skolemize,[status(esa)],[c78])).])).
% 33.88/34.15 cnf(c82,plain,~is_a_theorem(strict_implies(skolem0011,and(skolem0011,skolem0011)))|axiom_m4,inference(split_conjunct,[status(thm)],[c80])).
% 33.88/34.15 cnf(c9,axiom,X238!=X239|~is_a_theorem(X238)|is_a_theorem(X239),theory(equality)).
% 33.88/34.15 cnf(symmetry,axiom,X208!=X207|X207=X208,theory(equality)).
% 33.88/34.15 fof(s1_0_op_strict_implies,axiom,op_strict_implies,file('/export/starexec/sandbox/benchmark/theBenchmark.p', s1_0_op_strict_implies)).
% 33.88/34.15 cnf(c15,plain,op_strict_implies,inference(split_conjunct,[status(thm)],[s1_0_op_strict_implies])).
% 33.88/34.15 fof(op_strict_implies,axiom,(op_strict_implies=>(![X]:(![Y]:strict_implies(X,Y)=necessarily(implies(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL007+1.ax', op_strict_implies)).
% 33.88/34.15 fof(c29,plain,(~op_strict_implies|(![X]:(![Y]:strict_implies(X,Y)=necessarily(implies(X,Y))))),inference(fof_nnf,[status(thm)],[op_strict_implies])).
% 33.88/34.15 fof(c31,plain,(![X4]:(![X5]:(~op_strict_implies|strict_implies(X4,X5)=necessarily(implies(X4,X5))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,(~op_strict_implies|(![X4]:(![X5]:strict_implies(X4,X5)=necessarily(implies(X4,X5))))),inference(variable_rename,[status(thm)],[c29])).])).
% 33.88/34.15 cnf(c32,plain,~op_strict_implies|strict_implies(X268,X267)=necessarily(implies(X268,X267)),inference(split_conjunct,[status(thm)],[c31])).
% 33.88/34.15 cnf(c421,plain,strict_implies(X301,X302)=necessarily(implies(X301,X302)),inference(resolution,[status(thm)],[c32, c15])).
% 33.88/34.15 cnf(c453,plain,necessarily(implies(X304,X305))=strict_implies(X304,X305),inference(resolution,[status(thm)],[c421, symmetry])).
% 33.88/34.15 cnf(c468,plain,~is_a_theorem(necessarily(implies(X602,X603)))|is_a_theorem(strict_implies(X602,X603)),inference(resolution,[status(thm)],[c453, c9])).
% 33.88/34.15 fof(km4b_necessitation,axiom,necessitation,file('/export/starexec/sandbox/benchmark/Axioms/LCL007+3.ax', km4b_necessitation)).
% 33.88/34.15 cnf(c23,plain,necessitation,inference(split_conjunct,[status(thm)],[km4b_necessitation])).
% 33.88/34.15 fof(necessitation,axiom,(necessitation<=>(![X]:(is_a_theorem(X)=>is_a_theorem(necessarily(X))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL007+0.ax', necessitation)).
% 33.88/34.15 fof(c181,plain,((~necessitation|(![X]:(~is_a_theorem(X)|is_a_theorem(necessarily(X)))))&((?[X]:(is_a_theorem(X)&~is_a_theorem(necessarily(X))))|necessitation)),inference(fof_nnf,[status(thm)],[necessitation])).
% 33.88/34.15 fof(c182,plain,((~necessitation|(![X84]:(~is_a_theorem(X84)|is_a_theorem(necessarily(X84)))))&((?[X85]:(is_a_theorem(X85)&~is_a_theorem(necessarily(X85))))|necessitation)),inference(variable_rename,[status(thm)],[c181])).
% 33.88/34.15 fof(c184,plain,(![X84]:((~necessitation|(~is_a_theorem(X84)|is_a_theorem(necessarily(X84))))&((is_a_theorem(skolem0039)&~is_a_theorem(necessarily(skolem0039)))|necessitation))),inference(shift_quantors,[status(thm)],[fof(c183,plain,((~necessitation|(![X84]:(~is_a_theorem(X84)|is_a_theorem(necessarily(X84)))))&((is_a_theorem(skolem0039)&~is_a_theorem(necessarily(skolem0039)))|necessitation)),inference(skolemize,[status(esa)],[c182])).])).
% 33.88/34.15 fof(c185,plain,(![X84]:((~necessitation|(~is_a_theorem(X84)|is_a_theorem(necessarily(X84))))&((is_a_theorem(skolem0039)|necessitation)&(~is_a_theorem(necessarily(skolem0039))|necessitation)))),inference(distribute,[status(thm)],[c184])).
% 33.88/34.15 cnf(c186,plain,~necessitation|~is_a_theorem(X248)|is_a_theorem(necessarily(X248)),inference(split_conjunct,[status(thm)],[c185])).
% 33.88/34.15 fof(hilbert_modus_ponens,axiom,modus_ponens,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+2.ax', hilbert_modus_ponens)).
% 33.88/34.15 cnf(c203,plain,modus_ponens,inference(split_conjunct,[status(thm)],[hilbert_modus_ponens])).
% 33.88/34.15 fof(hilbert_and_3,axiom,and_3,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+2.ax', hilbert_and_3)).
% 33.88/34.15 cnf(c196,plain,and_3,inference(split_conjunct,[status(thm)],[hilbert_and_3])).
% 33.88/34.15 fof(and_3,axiom,(and_3<=>(![X]:(![Y]:is_a_theorem(implies(X,implies(Y,and(X,Y))))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', and_3)).
% 33.88/34.15 fof(c329,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])).
% 33.88/34.15 fof(c330,plain,((~and_3|(![X168]:(![X169]:is_a_theorem(implies(X168,implies(X169,and(X168,X169)))))))&((?[X170]:(?[X171]:~is_a_theorem(implies(X170,implies(X171,and(X170,X171))))))|and_3)),inference(variable_rename,[status(thm)],[c329])).
% 33.88/34.15 fof(c332,plain,(![X168]:(![X169]:((~and_3|is_a_theorem(implies(X168,implies(X169,and(X168,X169)))))&(~is_a_theorem(implies(skolem0076,implies(skolem0077,and(skolem0076,skolem0077))))|and_3)))),inference(shift_quantors,[status(thm)],[fof(c331,plain,((~and_3|(![X168]:(![X169]:is_a_theorem(implies(X168,implies(X169,and(X168,X169)))))))&(~is_a_theorem(implies(skolem0076,implies(skolem0077,and(skolem0076,skolem0077))))|and_3)),inference(skolemize,[status(esa)],[c330])).])).
% 33.88/34.15 cnf(c333,plain,~and_3|is_a_theorem(implies(X366,implies(X367,and(X366,X367)))),inference(split_conjunct,[status(thm)],[c332])).
% 33.88/34.15 cnf(c572,plain,is_a_theorem(implies(X368,implies(X369,and(X368,X369)))),inference(resolution,[status(thm)],[c333, c196])).
% 33.88/34.15 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)).
% 33.88/34.15 fof(c379,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])).
% 33.88/34.15 fof(c380,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)],[c379])).
% 33.88/34.15 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)&is_a_theorem(implies(skolem0093,skolem0094)))&~is_a_theorem(skolem0094))|modus_ponens)))),inference(shift_quantors,[status(thm)],[fof(c381,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)],[c380])).])).
% 33.88/34.15 fof(c383,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)],[c382])).
% 33.88/34.15 cnf(c384,plain,~modus_ponens|~is_a_theorem(X371)|~is_a_theorem(implies(X371,X370))|is_a_theorem(X370),inference(split_conjunct,[status(thm)],[c383])).
% 33.88/34.15 fof(hilbert_implies_2,axiom,implies_2,file('/export/starexec/sandbox/benchmark/Axioms/LCL006+2.ax', hilbert_implies_2)).
% 33.88/34.15 cnf(c200,plain,implies_2,inference(split_conjunct,[status(thm)],[hilbert_implies_2])).
% 33.88/34.15 fof(implies_2,axiom,(implies_2<=>(![X]:(![Y]:is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/LCL006+0.ax', implies_2)).
% 33.88/34.15 fof(c353,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])).
% 33.88/34.15 fof(c354,plain,((~implies_2|(![X186]:(![X187]:is_a_theorem(implies(implies(X186,implies(X186,X187)),implies(X186,X187))))))&((?[X188]:(?[X189]:~is_a_theorem(implies(implies(X188,implies(X188,X189)),implies(X188,X189)))))|implies_2)),inference(variable_rename,[status(thm)],[c353])).
% 33.88/34.15 fof(c356,plain,(![X186]:(![X187]:((~implies_2|is_a_theorem(implies(implies(X186,implies(X186,X187)),implies(X186,X187))))&(~is_a_theorem(implies(implies(skolem0085,implies(skolem0085,skolem0086)),implies(skolem0085,skolem0086)))|implies_2)))),inference(shift_quantors,[status(thm)],[fof(c355,plain,((~implies_2|(![X186]:(![X187]:is_a_theorem(implies(implies(X186,implies(X186,X187)),implies(X186,X187))))))&(~is_a_theorem(implies(implies(skolem0085,implies(skolem0085,skolem0086)),implies(skolem0085,skolem0086)))|implies_2)),inference(skolemize,[status(esa)],[c354])).])).
% 33.88/34.15 cnf(c357,plain,~implies_2|is_a_theorem(implies(implies(X591,implies(X591,X590)),implies(X591,X590))),inference(split_conjunct,[status(thm)],[c356])).
% 33.88/34.15 cnf(c1235,plain,is_a_theorem(implies(implies(X1839,implies(X1839,X1840)),implies(X1839,X1840))),inference(resolution,[status(thm)],[c357, c200])).
% 33.88/34.15 cnf(c9631,plain,~modus_ponens|~is_a_theorem(implies(X7877,implies(X7877,X7878)))|is_a_theorem(implies(X7877,X7878)),inference(resolution,[status(thm)],[c1235, c384])).
% 33.88/34.15 cnf(c48524,plain,~modus_ponens|is_a_theorem(implies(X7914,and(X7914,X7914))),inference(resolution,[status(thm)],[c9631, c572])).
% 33.88/34.15 cnf(c48832,plain,is_a_theorem(implies(X7915,and(X7915,X7915))),inference(resolution,[status(thm)],[c48524, c203])).
% 33.88/34.15 cnf(c48879,plain,~necessitation|is_a_theorem(necessarily(implies(X8070,and(X8070,X8070)))),inference(resolution,[status(thm)],[c48832, c186])).
% 33.88/34.15 cnf(c51624,plain,is_a_theorem(necessarily(implies(X8071,and(X8071,X8071)))),inference(resolution,[status(thm)],[c48879, c23])).
% 33.88/34.15 cnf(c51653,plain,is_a_theorem(strict_implies(X8072,and(X8072,X8072))),inference(resolution,[status(thm)],[c51624, c468])).
% 33.88/34.15 cnf(c51680,plain,axiom_m4,inference(resolution,[status(thm)],[c51653, c82])).
% 33.88/34.15 cnf(c51729,plain,$false,inference(resolution,[status(thm)],[c51680, c12])).
% 33.88/34.15 % SZS output end CNFRefutation
% 33.88/34.15
% 33.88/34.15 % Initial clauses : 160
% 33.88/34.15 % Processed clauses : 1869
% 33.88/34.15 % Factors computed : 8
% 33.88/34.15 % Resolvents computed: 51406
% 33.88/34.15 % Tautologies deleted: 99
% 33.88/34.15 % Forward subsumed : 1938
% 33.88/34.15 % Backward subsumed : 770
% 33.88/34.15 % -------- CPU Time ---------
% 33.88/34.15 % User time : 33.655 s
% 33.88/34.15 % System time : 0.130 s
% 33.88/34.15 % Total time : 33.785 s
%------------------------------------------------------------------------------