%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL538+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n007.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 11:21:08 AM UTC 2026
% Result : Theorem 0.25s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL538+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.10/0.35 % Computer : n007.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 5 05:38:39 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.25/0.47 start to proof:theBenchmark.p
% 0.25/0.54 % Version : CSI_E---1.1
% 0.25/0.54 % Problem : theBenchmark.p
% 0.25/0.54 % Proof found!
% 0.25/0.54 % SZS status Theorem for theBenchmark.p
% 0.25/0.54 % SZS output start Proof
% 0.25/0.54 fof(modus_ponens, axiom, (modus_ponens<=>![X1, X2]:((is_a_theorem(X1)&is_a_theorem(implies(X1,X2)))=>is_a_theorem(X2))), file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax', modus_ponens)).
% 0.25/0.54 fof(axiom_M, axiom, (axiom_M<=>![X1]:is_a_theorem(implies(necessarily(X1),X1))), file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', axiom_M)).
% 0.25/0.54 fof(hilbert_modus_ponens, axiom, modus_ponens, file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax', hilbert_modus_ponens)).
% 0.25/0.54 fof(km4b_axiom_M, axiom, axiom_M, file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+3.ax', km4b_axiom_M)).
% 0.25/0.54 fof(op_strict_implies, axiom, (op_strict_implies=>![X1, X2]:strict_implies(X1,X2)=necessarily(implies(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+1.ax', op_strict_implies)).
% 0.25/0.54 fof(s1_0_op_strict_implies, axiom, op_strict_implies, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_0_op_strict_implies)).
% 0.25/0.54 fof(modus_ponens_strict_implies, axiom, (modus_ponens_strict_implies<=>![X1, X2]:((is_a_theorem(X1)&is_a_theorem(strict_implies(X1,X2)))=>is_a_theorem(X2))), file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax', modus_ponens_strict_implies)).
% 0.25/0.54 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.25/0.54 fof(c_0_8, plain, ![X117, X118]:((~modus_ponens|(~is_a_theorem(X117)|~is_a_theorem(implies(X117,X118))|is_a_theorem(X118)))&(((is_a_theorem(esk1_0)|modus_ponens)&(is_a_theorem(implies(esk1_0,esk2_0))|modus_ponens))&(~is_a_theorem(esk2_0)|modus_ponens))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[modus_ponens])])])])])).
% 0.25/0.54 fof(c_0_9, plain, ![X255]:((~axiom_M|is_a_theorem(implies(necessarily(X255),X255)))&(~is_a_theorem(implies(necessarily(esk65_0),esk65_0))|axiom_M)), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_M])])])])).
% 0.25/0.54 cnf(c_0_10, plain, (is_a_theorem(X2)|~modus_ponens|~is_a_theorem(X1)|~is_a_theorem(implies(X1,X2))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.25/0.54 cnf(c_0_11, plain, (modus_ponens), inference(split_conjunct,[status(thm)],[hilbert_modus_ponens])).
% 0.25/0.54 cnf(c_0_12, plain, (is_a_theorem(implies(necessarily(X1),X1))|~axiom_M), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.54 cnf(c_0_13, plain, (axiom_M), inference(split_conjunct,[status(thm)],[km4b_axiom_M])).
% 0.25/0.54 fof(c_0_14, plain, ![X317, X318]:(~op_strict_implies|strict_implies(X317,X318)=necessarily(implies(X317,X318))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[op_strict_implies])])])).
% 0.25/0.54 cnf(c_0_15, plain, (is_a_theorem(X1)|~is_a_theorem(implies(X2,X1))|~is_a_theorem(X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 0.25/0.54 cnf(c_0_16, plain, (is_a_theorem(implies(necessarily(X1),X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_13])])).
% 0.25/0.54 cnf(c_0_17, plain, (strict_implies(X1,X2)=necessarily(implies(X1,X2))|~op_strict_implies), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.25/0.54 cnf(c_0_18, plain, (op_strict_implies), inference(split_conjunct,[status(thm)],[s1_0_op_strict_implies])).
% 0.25/0.54 fof(c_0_19, plain, ![X239, X240]:((~modus_ponens_strict_implies|(~is_a_theorem(X239)|~is_a_theorem(strict_implies(X239,X240))|is_a_theorem(X240)))&(((is_a_theorem(esk57_0)|modus_ponens_strict_implies)&(is_a_theorem(strict_implies(esk57_0,esk58_0))|modus_ponens_strict_implies))&(~is_a_theorem(esk58_0)|modus_ponens_strict_implies))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[modus_ponens_strict_implies])])])])])).
% 0.25/0.54 fof(c_0_20, negated_conjecture, ~modus_ponens_strict_implies, inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[s1_0_modus_ponens_strict_implies])])).
% 0.25/0.54 cnf(c_0_21, plain, (is_a_theorem(X1)|~is_a_theorem(necessarily(X1))), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 0.25/0.54 cnf(c_0_22, plain, (necessarily(implies(X1,X2))=strict_implies(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])])).
% 0.25/0.54 cnf(c_0_23, plain, (is_a_theorem(strict_implies(esk57_0,esk58_0))|modus_ponens_strict_implies), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.25/0.54 cnf(c_0_24, negated_conjecture, (~modus_ponens_strict_implies), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.25/0.54 cnf(c_0_25, plain, (is_a_theorem(implies(X1,X2))|~is_a_theorem(strict_implies(X1,X2))), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 0.25/0.54 cnf(c_0_26, plain, (is_a_theorem(strict_implies(esk57_0,esk58_0))), inference(sr,[status(thm)],[c_0_23, c_0_24])).
% 0.25/0.54 cnf(c_0_27, plain, (is_a_theorem(esk57_0)|modus_ponens_strict_implies), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.25/0.54 cnf(c_0_28, plain, (modus_ponens_strict_implies|~is_a_theorem(esk58_0)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.25/0.54 cnf(c_0_29, plain, (is_a_theorem(implies(esk57_0,esk58_0))), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 0.25/0.54 cnf(c_0_30, plain, (is_a_theorem(esk57_0)), inference(sr,[status(thm)],[c_0_27, c_0_24])).
% 0.25/0.54 cnf(c_0_31, plain, (~is_a_theorem(esk58_0)), inference(sr,[status(thm)],[c_0_28, c_0_24])).
% 0.25/0.54 cnf(c_0_32, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_29]), c_0_30])]), c_0_31]), ['proof']).
% 0.25/0.54 % SZS output end Proof
% 0.25/0.54 % User time : 0.044 s
% 0.25/0.54 % System time : 0.006 s
% 0.25/0.54 % Total time : 0.050 s
% 0.25/0.54
%------------------------------------------------------------------------------