%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n014.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.36s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.34 % Computer : n014.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 7 14:09:56 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.13/0.41 start to proof:theBenchmark.p
% 0.36/0.47 % Version : CSI_E---1.1
% 0.36/0.47 % Problem : theBenchmark.p
% 0.36/0.47 % Proof found!
% 0.36/0.47 % SZS status Theorem for theBenchmark.p
% 0.36/0.47 % SZS output start Proof
% 0.36/0.47 fof(ax_perm_relator_strong, axiom, ![X1, X2, X3, X4, X5, X6]:((((((((perm(X1)&strong(X1))&aee(X1,X2))&aer(X1,X3))&act(X1,X4))&tgt(X1,X5))&activates(X6,X1))=>?[X7, X8, X9]:(((((((((founds_imm(X6,X7,X1)&immunity(X8))&bearer(X8,X2))&cnt(X8,X4,X5))&part_of(X8,X7))&disability(X9))&bearer(X9,X3))&cnt(X9,X4,X5))&part_of(X9,X7))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax_perm_relator_strong)).
% 0.36/0.47 fof(act_p1, axiom, act(p1,read), file('/export/starexec/sandbox/benchmark/theBenchmark.p', act_p1)).
% 0.36/0.47 fof(strong_p1, axiom, strong(p1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', strong_p1)).
% 0.36/0.47 fof(perm_p1, axiom, perm(p1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', perm_p1)).
% 0.36/0.47 fof(act_e1_p1, axiom, activates(e1,p1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', act_e1_p1)).
% 0.36/0.47 fof(aee_p1, axiom, aee(p1,bibliothek), file('/export/starexec/sandbox/benchmark/theBenchmark.p', aee_p1)).
% 0.36/0.47 fof(conjecture, conjecture, ?[X7, X9]:(((((founds_imm(e1,X7,p1)&disability(X9))&bearer(X9,museen))&cnt(X9,read,museum_api))&part_of(X9,X7))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture)).
% 0.36/0.47 fof(aer_p1, axiom, aer(p1,museen), file('/export/starexec/sandbox/benchmark/theBenchmark.p', aer_p1)).
% 0.36/0.47 fof(tgt_p1, axiom, tgt(p1,museum_api), file('/export/starexec/sandbox/benchmark/theBenchmark.p', tgt_p1)).
% 0.36/0.47 fof(c_0_9, plain, ![X12, X13, X14, X15, X16, X17]:((((((((((founds_imm(X17,esk1_6(X12,X13,X14,X15,X16,X17),X12)|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12)))&(immunity(esk2_6(X12,X13,X14,X15,X16,X17))|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12))))&(bearer(esk2_6(X12,X13,X14,X15,X16,X17),X13)|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12))))&(cnt(esk2_6(X12,X13,X14,X15,X16,X17),X15,X16)|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12))))&(part_of(esk2_6(X12,X13,X14,X15,X16,X17),esk1_6(X12,X13,X14,X15,X16,X17))|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12))))&(disability(esk3_6(X12,X13,X14,X15,X16,X17))|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12))))&(bearer(esk3_6(X12,X13,X14,X15,X16,X17),X14)|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12))))&(cnt(esk3_6(X12,X13,X14,X15,X16,X17),X15,X16)|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12))))&(part_of(esk3_6(X12,X13,X14,X15,X16,X17),esk1_6(X12,X13,X14,X15,X16,X17))|(~perm(X12)|~strong(X12)|~aee(X12,X13)|~aer(X12,X14)|~act(X12,X15)|~tgt(X12,X16)|~activates(X17,X12))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_perm_relator_strong])])])])])).
% 0.36/0.47 cnf(c_0_10, plain, (cnt(esk3_6(X1,X2,X3,X4,X5,X6),X4,X5)|~perm(X1)|~strong(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.36/0.47 cnf(c_0_11, plain, (act(p1,read)), inference(split_conjunct,[status(thm)],[act_p1])).
% 0.36/0.47 cnf(c_0_12, plain, (strong(p1)), inference(split_conjunct,[status(thm)],[strong_p1])).
% 0.36/0.47 cnf(c_0_13, plain, (perm(p1)), inference(split_conjunct,[status(thm)],[perm_p1])).
% 0.36/0.47 cnf(c_0_14, plain, (disability(esk3_6(X1,X2,X3,X4,X5,X6))|~perm(X1)|~strong(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.36/0.47 cnf(c_0_15, plain, (bearer(esk3_6(X1,X2,X3,X4,X5,X6),X3)|~perm(X1)|~strong(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.36/0.47 cnf(c_0_16, plain, (cnt(esk3_6(p1,X1,X2,read,X3,X4),read,X3)|~activates(X4,p1)|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_11]), c_0_12]), c_0_13])])).
% 0.36/0.47 cnf(c_0_17, plain, (activates(e1,p1)), inference(split_conjunct,[status(thm)],[act_e1_p1])).
% 0.36/0.47 cnf(c_0_18, plain, (disability(esk3_6(p1,X1,X2,read,X3,X4))|~activates(X4,p1)|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14, c_0_11]), c_0_12]), c_0_13])])).
% 0.36/0.47 cnf(c_0_19, plain, (bearer(esk3_6(p1,X1,X2,read,X3,X4),X2)|~activates(X4,p1)|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_11]), c_0_12]), c_0_13])])).
% 0.36/0.47 cnf(c_0_20, plain, (founds_imm(X1,esk1_6(X2,X3,X4,X5,X6,X1),X2)|~perm(X2)|~strong(X2)|~aee(X2,X3)|~aer(X2,X4)|~act(X2,X5)|~tgt(X2,X6)|~activates(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.36/0.47 cnf(c_0_21, plain, (cnt(esk3_6(p1,X1,X2,read,X3,e1),read,X3)|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 0.36/0.47 cnf(c_0_22, plain, (aee(p1,bibliothek)), inference(split_conjunct,[status(thm)],[aee_p1])).
% 0.36/0.47 cnf(c_0_23, plain, (disability(esk3_6(p1,X1,X2,read,X3,e1))|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(spm,[status(thm)],[c_0_18, c_0_17])).
% 0.36/0.47 cnf(c_0_24, plain, (bearer(esk3_6(p1,X1,X2,read,X3,e1),X2)|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(spm,[status(thm)],[c_0_19, c_0_17])).
% 0.36/0.47 cnf(c_0_25, plain, (founds_imm(X1,esk1_6(p1,X2,X3,read,X4,X1),p1)|~activates(X1,p1)|~tgt(p1,X4)|~aer(p1,X3)|~aee(p1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_11]), c_0_12]), c_0_13])])).
% 0.36/0.47 cnf(c_0_26, plain, (part_of(esk3_6(X1,X2,X3,X4,X5,X6),esk1_6(X1,X2,X3,X4,X5,X6))|~perm(X1)|~strong(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.36/0.47 fof(c_0_27, negated_conjecture, ~(?[X7, X9]:(((((founds_imm(e1,X7,p1)&disability(X9))&bearer(X9,museen))&cnt(X9,read,museum_api))&part_of(X9,X7)))), inference(assume_negation,[status(cth)],[conjecture])).
% 0.36/0.47 cnf(c_0_28, plain, (cnt(esk3_6(p1,bibliothek,X1,read,X2,e1),read,X2)|~tgt(p1,X2)|~aer(p1,X1)), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 0.36/0.47 cnf(c_0_29, plain, (aer(p1,museen)), inference(split_conjunct,[status(thm)],[aer_p1])).
% 0.36/0.47 cnf(c_0_30, plain, (disability(esk3_6(p1,bibliothek,X1,read,X2,e1))|~tgt(p1,X2)|~aer(p1,X1)), inference(spm,[status(thm)],[c_0_23, c_0_22])).
% 0.36/0.47 cnf(c_0_31, plain, (bearer(esk3_6(p1,bibliothek,X1,read,X2,e1),X1)|~tgt(p1,X2)|~aer(p1,X1)), inference(spm,[status(thm)],[c_0_24, c_0_22])).
% 0.36/0.47 cnf(c_0_32, plain, (founds_imm(e1,esk1_6(p1,X1,X2,read,X3,e1),p1)|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(spm,[status(thm)],[c_0_25, c_0_17])).
% 0.36/0.47 cnf(c_0_33, plain, (part_of(esk3_6(p1,X1,X2,read,X3,X4),esk1_6(p1,X1,X2,read,X3,X4))|~activates(X4,p1)|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_11]), c_0_12]), c_0_13])])).
% 0.36/0.47 fof(c_0_34, negated_conjecture, ![X10, X11]:((~founds_imm(e1,X10,p1)|~disability(X11)|~bearer(X11,museen)|~cnt(X11,read,museum_api)|~part_of(X11,X10))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_27])])])).
% 0.36/0.47 cnf(c_0_35, plain, (cnt(esk3_6(p1,bibliothek,museen,read,X1,e1),read,X1)|~tgt(p1,X1)), inference(spm,[status(thm)],[c_0_28, c_0_29])).
% 0.36/0.47 cnf(c_0_36, plain, (tgt(p1,museum_api)), inference(split_conjunct,[status(thm)],[tgt_p1])).
% 0.36/0.47 cnf(c_0_37, plain, (disability(esk3_6(p1,bibliothek,museen,read,X1,e1))|~tgt(p1,X1)), inference(spm,[status(thm)],[c_0_30, c_0_29])).
% 0.36/0.47 cnf(c_0_38, plain, (bearer(esk3_6(p1,bibliothek,museen,read,X1,e1),museen)|~tgt(p1,X1)), inference(spm,[status(thm)],[c_0_31, c_0_29])).
% 0.36/0.47 cnf(c_0_39, plain, (founds_imm(e1,esk1_6(p1,bibliothek,X1,read,X2,e1),p1)|~tgt(p1,X2)|~aer(p1,X1)), inference(spm,[status(thm)],[c_0_32, c_0_22])).
% 0.36/0.47 cnf(c_0_40, plain, (part_of(esk3_6(p1,X1,X2,read,X3,e1),esk1_6(p1,X1,X2,read,X3,e1))|~tgt(p1,X3)|~aer(p1,X2)|~aee(p1,X1)), inference(spm,[status(thm)],[c_0_33, c_0_17])).
% 0.36/0.47 cnf(c_0_41, negated_conjecture, (~founds_imm(e1,X1,p1)|~disability(X2)|~bearer(X2,museen)|~cnt(X2,read,museum_api)|~part_of(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_34])).
% 0.36/0.47 cnf(c_0_42, plain, (cnt(esk3_6(p1,bibliothek,museen,read,museum_api,e1),read,museum_api)), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 0.36/0.47 cnf(c_0_43, plain, (disability(esk3_6(p1,bibliothek,museen,read,museum_api,e1))), inference(spm,[status(thm)],[c_0_37, c_0_36])).
% 0.36/0.47 cnf(c_0_44, plain, (bearer(esk3_6(p1,bibliothek,museen,read,museum_api,e1),museen)), inference(spm,[status(thm)],[c_0_38, c_0_36])).
% 0.36/0.47 cnf(c_0_45, plain, (founds_imm(e1,esk1_6(p1,bibliothek,museen,read,X1,e1),p1)|~tgt(p1,X1)), inference(spm,[status(thm)],[c_0_39, c_0_29])).
% 0.36/0.47 cnf(c_0_46, plain, (part_of(esk3_6(p1,bibliothek,X1,read,X2,e1),esk1_6(p1,bibliothek,X1,read,X2,e1))|~tgt(p1,X2)|~aer(p1,X1)), inference(spm,[status(thm)],[c_0_40, c_0_22])).
% 0.36/0.47 cnf(c_0_47, negated_conjecture, (~part_of(esk3_6(p1,bibliothek,museen,read,museum_api,e1),X1)|~founds_imm(e1,X1,p1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_43]), c_0_44])])).
% 0.36/0.47 cnf(c_0_48, plain, (founds_imm(e1,esk1_6(p1,bibliothek,museen,read,museum_api,e1),p1)), inference(spm,[status(thm)],[c_0_45, c_0_36])).
% 0.36/0.47 cnf(c_0_49, plain, (part_of(esk3_6(p1,bibliothek,museen,read,X1,e1),esk1_6(p1,bibliothek,museen,read,X1,e1))|~tgt(p1,X1)), inference(spm,[status(thm)],[c_0_46, c_0_29])).
% 0.36/0.47 cnf(c_0_50, negated_conjecture, (~part_of(esk3_6(p1,bibliothek,museen,read,museum_api,e1),esk1_6(p1,bibliothek,museen,read,museum_api,e1))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 0.36/0.47 cnf(c_0_51, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_36]), c_0_50]), ['proof']).
% 0.36/0.47 % SZS output end Proof
% 0.36/0.47 % User time : 0.007 s
% 0.36/0.47 % System time : 0.005 s
% 0.36/0.47 % Total time : 0.012 s
% 0.36/0.47 % User time : 0.008 s
% 0.36/0.47 % System time : 0.008 s
% 0.36/0.47 % Total time : 0.016 s
% 0.36/0.47
%------------------------------------------------------------------------------