%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL542+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:40 PM UTC 2026
% Result : Theorem 0.80s 1.13s
% Output : CNFRefutation 0.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL542+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 21:52:36 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.42 (re.compile("\."), Token.FullStop),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.42 (re.compile("\("), Token.OpenPar),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.42 (re.compile("\)"), Token.ClosePar),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.42 (re.compile("\["), Token.OpenSquare),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("~\|"), Token.Nor),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("\|"), Token.Or),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.42 (re.compile("\?"), Token.Existential),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.25/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.49 """
% 0.25/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.49 """
% 0.25/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.58 """
% 0.80/1.13 % Version: 1.5
% 0.80/1.13 % SZS status Theorem
% 0.80/1.13 % SZS output start CNFRefutation
% 0.80/1.13 fof(s1_0_axiom_m2,conjecture,axiom_m2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_0_axiom_m2)).
% 0.80/1.13 fof(c10,negated_conjecture,(~axiom_m2),inference(assume_negation,[status(cth)],[s1_0_axiom_m2])).
% 0.80/1.13 fof(c11,negated_conjecture,~axiom_m2,inference(fof_simplification,[status(thm)],[c10])).
% 0.80/1.13 cnf(c12,negated_conjecture,~axiom_m2,inference(split_conjunct,[status(thm)],[c11])).
% 0.80/1.13 fof(axiom_m2,axiom,(axiom_m2<=>(![X]:(![Y]:is_a_theorem(strict_implies(and(X,Y),X))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', axiom_m2)).
% 0.80/1.13 fof(c89,plain,((~axiom_m2|(![X]:(![Y]:is_a_theorem(strict_implies(and(X,Y),X)))))&((?[X]:(?[Y]:~is_a_theorem(strict_implies(and(X,Y),X))))|axiom_m2)),inference(fof_nnf,[status(thm)],[axiom_m2])).
% 0.80/1.13 fof(c90,plain,((~axiom_m2|(![X36]:(![X37]:is_a_theorem(strict_implies(and(X36,X37),X36)))))&((?[X38]:(?[X39]:~is_a_theorem(strict_implies(and(X38,X39),X38))))|axiom_m2)),inference(variable_rename,[status(thm)],[c89])).
% 0.80/1.14 fof(c92,plain,(![X36]:(![X37]:((~axiom_m2|is_a_theorem(strict_implies(and(X36,X37),X36)))&(~is_a_theorem(strict_implies(and(skolem0015,skolem0016),skolem0015))|axiom_m2)))),inference(shift_quantors,[status(thm)],[fof(c91,plain,((~axiom_m2|(![X36]:(![X37]:is_a_theorem(strict_implies(and(X36,X37),X36)))))&(~is_a_theorem(strict_implies(and(skolem0015,skolem0016),skolem0015))|axiom_m2)),inference(skolemize,[status(esa)],[c90])).])).
% 0.80/1.14 cnf(c94,plain,~is_a_theorem(strict_implies(and(skolem0015,skolem0016),skolem0015))|axiom_m2,inference(split_conjunct,[status(thm)],[c92])).
% 0.80/1.14 fof(km4b_necessitation,axiom,necessitation,file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+3.ax', km4b_necessitation)).
% 0.80/1.14 cnf(c23,plain,necessitation,inference(split_conjunct,[status(thm)],[km4b_necessitation])).
% 0.80/1.14 fof(necessitation,axiom,(necessitation<=>(![X]:(is_a_theorem(X)=>is_a_theorem(necessarily(X))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', necessitation)).
% 0.80/1.14 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])).
% 0.80/1.14 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])).
% 0.80/1.14 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])).])).
% 0.80/1.14 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])).
% 0.80/1.14 cnf(c186,plain,~necessitation|~is_a_theorem(X248)|is_a_theorem(necessarily(X248)),inference(split_conjunct,[status(thm)],[c185])).
% 0.80/1.14 fof(hilbert_and_1,axiom,and_1,file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_and_1)).
% 0.80/1.14 cnf(c198,plain,and_1,inference(split_conjunct,[status(thm)],[hilbert_and_1])).
% 0.80/1.14 fof(and_1,axiom,(and_1<=>(![X]:(![Y]:is_a_theorem(implies(and(X,Y),X))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', and_1)).
% 0.80/1.14 fof(c341,plain,((~and_1|(![X]:(![Y]:is_a_theorem(implies(and(X,Y),X)))))&((?[X]:(?[Y]:~is_a_theorem(implies(and(X,Y),X))))|and_1)),inference(fof_nnf,[status(thm)],[and_1])).
% 0.80/1.14 fof(c342,plain,((~and_1|(![X176]:(![X177]:is_a_theorem(implies(and(X176,X177),X176)))))&((?[X178]:(?[X179]:~is_a_theorem(implies(and(X178,X179),X178))))|and_1)),inference(variable_rename,[status(thm)],[c341])).
% 0.80/1.14 fof(c344,plain,(![X176]:(![X177]:((~and_1|is_a_theorem(implies(and(X176,X177),X176)))&(~is_a_theorem(implies(and(skolem0080,skolem0081),skolem0080))|and_1)))),inference(shift_quantors,[status(thm)],[fof(c343,plain,((~and_1|(![X176]:(![X177]:is_a_theorem(implies(and(X176,X177),X176)))))&(~is_a_theorem(implies(and(skolem0080,skolem0081),skolem0080))|and_1)),inference(skolemize,[status(esa)],[c342])).])).
% 0.80/1.14 cnf(c345,plain,~and_1|is_a_theorem(implies(and(X283,X282),X283)),inference(split_conjunct,[status(thm)],[c344])).
% 0.80/1.14 cnf(c428,plain,is_a_theorem(implies(and(X285,X284),X285)),inference(resolution,[status(thm)],[c345, c198])).
% 0.80/1.14 cnf(c429,plain,~necessitation|is_a_theorem(necessarily(implies(and(X329,X330),X329))),inference(resolution,[status(thm)],[c428, c186])).
% 0.80/1.14 cnf(c498,plain,is_a_theorem(necessarily(implies(and(X332,X331),X332))),inference(resolution,[status(thm)],[c429, c23])).
% 0.80/1.14 cnf(c9,axiom,X238!=X239|~is_a_theorem(X238)|is_a_theorem(X239),theory(equality)).
% 0.80/1.14 cnf(symmetry,axiom,X208!=X207|X207=X208,theory(equality)).
% 0.80/1.14 fof(s1_0_op_strict_implies,axiom,op_strict_implies,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_0_op_strict_implies)).
% 0.80/1.14 cnf(c15,plain,op_strict_implies,inference(split_conjunct,[status(thm)],[s1_0_op_strict_implies])).
% 0.80/1.14 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.80/1.14 fof(c29,plain,(~op_strict_implies|(![X]:(![Y]:strict_implies(X,Y)=necessarily(implies(X,Y))))),inference(fof_nnf,[status(thm)],[op_strict_implies])).
% 0.80/1.14 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])).])).
% 0.80/1.14 cnf(c32,plain,~op_strict_implies|strict_implies(X268,X267)=necessarily(implies(X268,X267)),inference(split_conjunct,[status(thm)],[c31])).
% 0.80/1.14 cnf(c421,plain,strict_implies(X302,X301)=necessarily(implies(X302,X301)),inference(resolution,[status(thm)],[c32, c15])).
% 0.80/1.14 cnf(c445,plain,necessarily(implies(X305,X304))=strict_implies(X305,X304),inference(resolution,[status(thm)],[c421, symmetry])).
% 0.80/1.14 cnf(c471,plain,~is_a_theorem(necessarily(implies(X602,X603)))|is_a_theorem(strict_implies(X602,X603)),inference(resolution,[status(thm)],[c445, c9])).
% 0.80/1.14 cnf(c1329,plain,is_a_theorem(strict_implies(and(X616,X615),X616)),inference(resolution,[status(thm)],[c471, c498])).
% 0.80/1.14 cnf(c1416,plain,axiom_m2,inference(resolution,[status(thm)],[c1329, c94])).
% 0.80/1.14 cnf(c1427,plain,$false,inference(resolution,[status(thm)],[c1416, c12])).
% 0.80/1.14 % SZS output end CNFRefutation
% 0.80/1.14
% 0.80/1.14 % Initial clauses : 160
% 0.80/1.14 % Processed clauses : 321
% 0.80/1.14 % Factors computed : 8
% 0.80/1.14 % Resolvents computed: 1032
% 0.80/1.14 % Tautologies deleted: 7
% 0.80/1.14 % Forward subsumed : 93
% 0.80/1.14 % Backward subsumed : 111
% 0.80/1.14 % -------- CPU Time ---------
% 0.80/1.14 % User time : 0.743 s
% 0.80/1.14 % System time : 0.030 s
% 0.80/1.14 % Total time : 0.773 s
%------------------------------------------------------------------------------