%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT116+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n008.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 : Tue Sep 8 06:04:40 AM UTC 2026
% Result : Theorem 0.26s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT116+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n008.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 : Mon Sep 7 14:10:08 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.14/0.47 start to proof:theBenchmark.p
% 0.26/0.53 % Version : CSI_E---1.1
% 0.26/0.53 % Problem : theBenchmark.p
% 0.26/0.53 % Proof found!
% 0.26/0.53 % SZS status Theorem for theBenchmark.p
% 0.26/0.53 % SZS output start Proof
% 0.26/0.53 fof(ax_B3, axiom, ![X1, X2, X3, X4, X5, X6]:(((((subjection(X1)&cnt(X1,decl(X2),X3))&part_of(X1,X4))&founds_rem(X5,X4,X6))=>about_event(X1,X5))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax_B3)).
% 0.26/0.53 fof(conjecture, conjecture, about_event(s,e1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture)).
% 0.26/0.53 fof(cnt_s, axiom, cnt(s,decl(some_action),some_target), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cnt_s)).
% 0.26/0.53 fof(subj_s, axiom, subjection(s), file('/export/starexec/sandbox/benchmark/theBenchmark.p', subj_s)).
% 0.26/0.53 fof(founds_rem1, axiom, founds_rem(e1,rho_r,f1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', founds_rem1)).
% 0.26/0.53 fof(partof_s, axiom, part_of(s,rho_r), file('/export/starexec/sandbox/benchmark/theBenchmark.p', partof_s)).
% 0.26/0.53 fof(c_0_6, plain, ![X7, X8, X9, X10, X11, X12]:((~subjection(X7)|~cnt(X7,decl(X8),X9)|~part_of(X7,X10)|~founds_rem(X11,X10,X12)|about_event(X7,X11))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_B3])])])).
% 0.26/0.53 fof(c_0_7, negated_conjecture, ~about_event(s,e1), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conjecture])])).
% 0.26/0.53 cnf(c_0_8, plain, (about_event(X1,X5)|~subjection(X1)|~cnt(X1,decl(X2),X3)|~part_of(X1,X4)|~founds_rem(X5,X4,X6)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.26/0.53 cnf(c_0_9, plain, (cnt(s,decl(some_action),some_target)), inference(split_conjunct,[status(thm)],[cnt_s])).
% 0.26/0.53 cnf(c_0_10, plain, (subjection(s)), inference(split_conjunct,[status(thm)],[subj_s])).
% 0.26/0.53 fof(c_0_11, negated_conjecture, ~about_event(s,e1), inference(fof_nnf,[status(thm)],[c_0_7])).
% 0.26/0.53 cnf(c_0_12, plain, (about_event(s,X1)|~founds_rem(X1,X2,X3)|~part_of(s,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_8, c_0_9]), c_0_10])])).
% 0.26/0.53 cnf(c_0_13, plain, (founds_rem(e1,rho_r,f1)), inference(split_conjunct,[status(thm)],[founds_rem1])).
% 0.26/0.53 cnf(c_0_14, plain, (part_of(s,rho_r)), inference(split_conjunct,[status(thm)],[partof_s])).
% 0.26/0.53 cnf(c_0_15, negated_conjecture, (~about_event(s,e1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.26/0.53 cnf(c_0_16, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_14])]), c_0_15]), ['proof']).
% 0.26/0.53 % SZS output end Proof
% 0.26/0.53 % User time : 0.003 s
% 0.26/0.53 % System time : 0.002 s
% 0.26/0.53 % Total time : 0.005 s
% 0.26/0.53 % User time : 0.005 s
% 0.26/0.53 % System time : 0.004 s
% 0.26/0.53 % Total time : 0.009 s
% 0.26/0.53
%------------------------------------------------------------------------------