%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL536+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:39 PM UTC 2026
% Result : Theorem 1.79s 2.08s
% Output : CNFRefutation 1.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL536+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 02:50:16 UTC 2026
% 0.08/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 """
% 1.79/2.08 % Version: 1.5
% 1.79/2.08 % SZS status Theorem
% 1.79/2.08 % SZS output start CNFRefutation
% 1.79/2.08 fof(s1_0_m10_axiom_m10,conjecture,axiom_m10,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_0_m10_axiom_m10)).
% 1.79/2.08 fof(c10,negated_conjecture,(~axiom_m10),inference(assume_negation,[status(cth)],[s1_0_m10_axiom_m10])).
% 1.79/2.08 fof(c11,negated_conjecture,~axiom_m10,inference(fof_simplification,[status(thm)],[c10])).
% 1.79/2.08 cnf(c12,negated_conjecture,~axiom_m10,inference(split_conjunct,[status(thm)],[c11])).
% 1.79/2.08 fof(axiom_m10,axiom,(axiom_m10<=>(![X]:is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X)))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', axiom_m10)).
% 1.79/2.08 fof(c40,plain,((~axiom_m10|(![X]:is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))))&((?[X]:~is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X)))))|axiom_m10)),inference(fof_nnf,[status(thm)],[axiom_m10])).
% 1.79/2.08 fof(c41,plain,((~axiom_m10|(![X8]:is_a_theorem(strict_implies(possibly(X8),necessarily(possibly(X8))))))&((?[X9]:~is_a_theorem(strict_implies(possibly(X9),necessarily(possibly(X9)))))|axiom_m10)),inference(variable_rename,[status(thm)],[c40])).
% 1.79/2.08 fof(c43,plain,(![X8]:((~axiom_m10|is_a_theorem(strict_implies(possibly(X8),necessarily(possibly(X8)))))&(~is_a_theorem(strict_implies(possibly(skolem0001),necessarily(possibly(skolem0001))))|axiom_m10))),inference(shift_quantors,[status(thm)],[fof(c42,plain,((~axiom_m10|(![X8]:is_a_theorem(strict_implies(possibly(X8),necessarily(possibly(X8))))))&(~is_a_theorem(strict_implies(possibly(skolem0001),necessarily(possibly(skolem0001))))|axiom_m10)),inference(skolemize,[status(esa)],[c41])).])).
% 1.79/2.08 cnf(c45,plain,~is_a_theorem(strict_implies(possibly(skolem0001),necessarily(possibly(skolem0001))))|axiom_m10,inference(split_conjunct,[status(thm)],[c43])).
% 1.79/2.08 cnf(c9,axiom,X235!=X236|~is_a_theorem(X235)|is_a_theorem(X236),theory(equality)).
% 1.79/2.08 cnf(symmetry,axiom,X207!=X208|X208=X207,theory(equality)).
% 1.79/2.08 fof(s1_0_op_strict_implies,axiom,op_strict_implies,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_0_op_strict_implies)).
% 1.79/2.08 cnf(c15,plain,op_strict_implies,inference(split_conjunct,[status(thm)],[s1_0_op_strict_implies])).
% 1.79/2.08 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)).
% 1.79/2.08 fof(c28,plain,(~op_strict_implies|(![X]:(![Y]:strict_implies(X,Y)=necessarily(implies(X,Y))))),inference(fof_nnf,[status(thm)],[op_strict_implies])).
% 1.79/2.08 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])).])).
% 1.79/2.08 cnf(c31,plain,~op_strict_implies|strict_implies(X270,X269)=necessarily(implies(X270,X269)),inference(split_conjunct,[status(thm)],[c30])).
% 1.79/2.08 cnf(c421,plain,strict_implies(X300,X299)=necessarily(implies(X300,X299)),inference(resolution,[status(thm)],[c31, c15])).
% 1.79/2.08 cnf(c445,plain,necessarily(implies(X303,X304))=strict_implies(X303,X304),inference(resolution,[status(thm)],[c421, symmetry])).
% 1.79/2.08 cnf(c466,plain,~is_a_theorem(necessarily(implies(X568,X567)))|is_a_theorem(strict_implies(X568,X567)),inference(resolution,[status(thm)],[c445, c9])).
% 1.79/2.08 fof(km5_necessitation,axiom,necessitation,file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+2.ax', km5_necessitation)).
% 1.79/2.08 cnf(c22,plain,necessitation,inference(split_conjunct,[status(thm)],[km5_necessitation])).
% 1.79/2.08 fof(necessitation,axiom,(necessitation<=>(![X]:(is_a_theorem(X)=>is_a_theorem(necessarily(X))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', necessitation)).
% 1.79/2.08 fof(c180,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])).
% 1.79/2.08 fof(c181,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)],[c180])).
% 1.79/2.08 fof(c183,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(c182,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)],[c181])).])).
% 1.79/2.08 fof(c184,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)],[c183])).
% 1.79/2.08 cnf(c185,plain,~necessitation|~is_a_theorem(X248)|is_a_theorem(necessarily(X248)),inference(split_conjunct,[status(thm)],[c184])).
% 1.79/2.08 fof(km5_axiom_5,axiom,axiom_5,file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+2.ax', km5_axiom_5)).
% 1.79/2.08 cnf(c19,plain,axiom_5,inference(split_conjunct,[status(thm)],[km5_axiom_5])).
% 1.79/2.08 fof(axiom_5,axiom,(axiom_5<=>(![X]:is_a_theorem(implies(possibly(X),necessarily(possibly(X)))))),file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', axiom_5)).
% 1.79/2.08 fof(c124,plain,((~axiom_5|(![X]:is_a_theorem(implies(possibly(X),necessarily(possibly(X))))))&((?[X]:~is_a_theorem(implies(possibly(X),necessarily(possibly(X)))))|axiom_5)),inference(fof_nnf,[status(thm)],[axiom_5])).
% 1.79/2.08 fof(c125,plain,((~axiom_5|(![X60]:is_a_theorem(implies(possibly(X60),necessarily(possibly(X60))))))&((?[X61]:~is_a_theorem(implies(possibly(X61),necessarily(possibly(X61)))))|axiom_5)),inference(variable_rename,[status(thm)],[c124])).
% 1.79/2.08 fof(c127,plain,(![X60]:((~axiom_5|is_a_theorem(implies(possibly(X60),necessarily(possibly(X60)))))&(~is_a_theorem(implies(possibly(skolem0027),necessarily(possibly(skolem0027))))|axiom_5))),inference(shift_quantors,[status(thm)],[fof(c126,plain,((~axiom_5|(![X60]:is_a_theorem(implies(possibly(X60),necessarily(possibly(X60))))))&(~is_a_theorem(implies(possibly(skolem0027),necessarily(possibly(skolem0027))))|axiom_5)),inference(skolemize,[status(esa)],[c125])).])).
% 1.79/2.08 cnf(c128,plain,~axiom_5|is_a_theorem(implies(possibly(X339),necessarily(possibly(X339)))),inference(split_conjunct,[status(thm)],[c127])).
% 1.79/2.08 cnf(c499,plain,is_a_theorem(implies(possibly(X340),necessarily(possibly(X340)))),inference(resolution,[status(thm)],[c128, c19])).
% 1.79/2.08 cnf(c500,plain,~necessitation|is_a_theorem(necessarily(implies(possibly(X1243),necessarily(possibly(X1243))))),inference(resolution,[status(thm)],[c499, c185])).
% 1.79/2.08 cnf(c2998,plain,is_a_theorem(necessarily(implies(possibly(X1415),necessarily(possibly(X1415))))),inference(resolution,[status(thm)],[c500, c22])).
% 1.79/2.08 cnf(c4123,plain,is_a_theorem(strict_implies(possibly(X1416),necessarily(possibly(X1416)))),inference(resolution,[status(thm)],[c2998, c466])).
% 1.79/2.08 cnf(c4153,plain,axiom_m10,inference(resolution,[status(thm)],[c4123, c45])).
% 1.79/2.08 cnf(c4158,plain,$false,inference(resolution,[status(thm)],[c4153, c12])).
% 1.79/2.08 % SZS output end CNFRefutation
% 1.79/2.08
% 1.79/2.08 % Initial clauses : 159
% 1.79/2.08 % Processed clauses : 495
% 1.79/2.08 % Factors computed : 8
% 1.79/2.08 % Resolvents computed: 3764
% 1.79/2.08 % Tautologies deleted: 12
% 1.79/2.08 % Forward subsumed : 256
% 1.79/2.08 % Backward subsumed : 166
% 1.79/2.08 % -------- CPU Time ---------
% 1.79/2.08 % User time : 1.682 s
% 1.79/2.08 % System time : 0.041 s
% 1.79/2.08 % Total time : 1.723 s
%------------------------------------------------------------------------------