%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n019.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:39 AM UTC 2026
% Result : Theorem 0.24s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n019.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 14:07:52 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.47 start to proof:theBenchmark.p
% 0.24/0.55 % Version : CSI_E---1.1
% 0.24/0.55 % Problem : theBenchmark.p
% 0.24/0.55 % Proof found!
% 0.24/0.55 % SZS status Theorem for theBenchmark.p
% 0.24/0.55 % SZS output start Proof
% 0.24/0.55 fof(ax_proh_relator_remedy, axiom, ![X1, X2, X3, X4, X5, X6]:((((((((proh(X1)&has_rem(X1))&aee(X1,X2))&aer(X1,X3))&act(X1,X4))&tgt(X1,X5))&activates(X6,X1))=>?[X10, X11, X12]:(((((((((founds_rem(X6,X10,X1)&power(X11))&bearer(X11,X3))&cnt(X11,decl(X4),X5))&part_of(X11,X10))&subjection(X12))&bearer(X12,X2))&cnt(X12,decl(X4),X5))&part_of(X12,X10))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax_proh_relator_remedy)).
% 0.24/0.55 fof(act_f1, axiom, act(f1,distrib), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', act_f1)).
% 0.24/0.55 fof(rem_f1, axiom, has_rem(f1), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rem_f1)).
% 0.24/0.55 fof(proh_f1, axiom, proh(f1), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', proh_f1)).
% 0.24/0.55 fof(act_e1_f1, axiom, activates(e1,f1), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', act_e1_f1)).
% 0.24/0.55 fof(conjecture, conjecture, ?[X10, X11, X12]:(((((((((((founds_rem(e1,X10,f1)&power(X11))&bearer(X11,philharmonie))&cnt(X11,decl(distrib),concert_ds))&part_of(X11,X10))&about_event(X11,e1))&subjection(X12))&bearer(X12,marketplace))&cnt(X12,decl(distrib),concert_ds))&part_of(X12,X10))&about_event(X12,e1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conjecture)).
% 0.24/0.55 fof(aee_f1, axiom, aee(f1,marketplace), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', aee_f1)).
% 0.24/0.55 fof(ax_B2, axiom, ![X11, X4, X5, X7, X6, X15]:(((((power(X11)&cnt(X11,decl(X4),X5))&part_of(X11,X7))&founds_rem(X6,X7,X15))=>about_event(X11,X6))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax_B2)).
% 0.24/0.55 fof(ax_B3, axiom, ![X12, X4, X5, X7, X6, X15]:(((((subjection(X12)&cnt(X12,decl(X4),X5))&part_of(X12,X7))&founds_rem(X6,X7,X15))=>about_event(X12,X6))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax_B3)).
% 0.24/0.55 fof(aer_f1, axiom, aer(f1,philharmonie), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', aer_f1)).
% 0.24/0.55 fof(tgt_f1, axiom, tgt(f1,concert_ds), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', tgt_f1)).
% 0.24/0.55 fof(c_0_11, plain, ![X31, X32, X33, X34, X35, X36]:((((((((((founds_rem(X36,esk1_6(X31,X32,X33,X34,X35,X36),X31)|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31)))&(power(esk2_6(X31,X32,X33,X34,X35,X36))|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31))))&(bearer(esk2_6(X31,X32,X33,X34,X35,X36),X33)|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31))))&(cnt(esk2_6(X31,X32,X33,X34,X35,X36),decl(X34),X35)|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31))))&(part_of(esk2_6(X31,X32,X33,X34,X35,X36),esk1_6(X31,X32,X33,X34,X35,X36))|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31))))&(subjection(esk3_6(X31,X32,X33,X34,X35,X36))|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31))))&(bearer(esk3_6(X31,X32,X33,X34,X35,X36),X32)|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31))))&(cnt(esk3_6(X31,X32,X33,X34,X35,X36),decl(X34),X35)|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31))))&(part_of(esk3_6(X31,X32,X33,X34,X35,X36),esk1_6(X31,X32,X33,X34,X35,X36))|(~proh(X31)|~has_rem(X31)|~aee(X31,X32)|~aer(X31,X33)|~act(X31,X34)|~tgt(X31,X35)|~activates(X36,X31))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_proh_relator_remedy])])])])])).
% 0.24/0.55 cnf(c_0_12, plain, (cnt(esk3_6(X1,X2,X3,X4,X5,X6),decl(X4),X5)|~proh(X1)|~has_rem(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_13, plain, (act(f1,distrib)), inference(split_conjunct,[status(thm)],[act_f1])).
% 0.24/0.55 cnf(c_0_14, plain, (has_rem(f1)), inference(split_conjunct,[status(thm)],[rem_f1])).
% 0.24/0.55 cnf(c_0_15, plain, (proh(f1)), inference(split_conjunct,[status(thm)],[proh_f1])).
% 0.24/0.55 cnf(c_0_16, plain, (subjection(esk3_6(X1,X2,X3,X4,X5,X6))|~proh(X1)|~has_rem(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_17, plain, (bearer(esk3_6(X1,X2,X3,X4,X5,X6),X2)|~proh(X1)|~has_rem(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_18, plain, (cnt(esk3_6(f1,X1,X2,distrib,X3,X4),decl(distrib),X3)|~activates(X4,f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_19, plain, (activates(e1,f1)), inference(split_conjunct,[status(thm)],[act_e1_f1])).
% 0.24/0.55 cnf(c_0_20, plain, (subjection(esk3_6(f1,X1,X2,distrib,X3,X4))|~activates(X4,f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_21, plain, (bearer(esk3_6(f1,X1,X2,distrib,X3,X4),X1)|~activates(X4,f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_22, plain, (cnt(esk2_6(X1,X2,X3,X4,X5,X6),decl(X4),X5)|~proh(X1)|~has_rem(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_23, plain, (power(esk2_6(X1,X2,X3,X4,X5,X6))|~proh(X1)|~has_rem(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_24, plain, (bearer(esk2_6(X1,X2,X3,X4,X5,X6),X3)|~proh(X1)|~has_rem(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 fof(c_0_25, negated_conjecture, ~(?[X10, X11, X12]:(((((((((((founds_rem(e1,X10,f1)&power(X11))&bearer(X11,philharmonie))&cnt(X11,decl(distrib),concert_ds))&part_of(X11,X10))&about_event(X11,e1))&subjection(X12))&bearer(X12,marketplace))&cnt(X12,decl(distrib),concert_ds))&part_of(X12,X10))&about_event(X12,e1)))), inference(assume_negation,[status(cth)],[conjecture])).
% 0.24/0.55 cnf(c_0_26, plain, (cnt(esk3_6(f1,X1,X2,distrib,X3,e1),decl(distrib),X3)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 0.24/0.55 cnf(c_0_27, plain, (aee(f1,marketplace)), inference(split_conjunct,[status(thm)],[aee_f1])).
% 0.24/0.55 cnf(c_0_28, plain, (subjection(esk3_6(f1,X1,X2,distrib,X3,e1))|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_20, c_0_19])).
% 0.24/0.55 cnf(c_0_29, plain, (bearer(esk3_6(f1,X1,X2,distrib,X3,e1),X1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_21, c_0_19])).
% 0.24/0.55 cnf(c_0_30, plain, (cnt(esk2_6(f1,X1,X2,distrib,X3,X4),decl(distrib),X3)|~activates(X4,f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_31, plain, (power(esk2_6(f1,X1,X2,distrib,X3,X4))|~activates(X4,f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_32, plain, (bearer(esk2_6(f1,X1,X2,distrib,X3,X4),X2)|~activates(X4,f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_33, plain, (founds_rem(X1,esk1_6(X2,X3,X4,X5,X6,X1),X2)|~proh(X2)|~has_rem(X2)|~aee(X2,X3)|~aer(X2,X4)|~act(X2,X5)|~tgt(X2,X6)|~activates(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 fof(c_0_34, negated_conjecture, ![X16, X17, X18]:((~founds_rem(e1,X16,f1)|~power(X17)|~bearer(X17,philharmonie)|~cnt(X17,decl(distrib),concert_ds)|~part_of(X17,X16)|~about_event(X17,e1)|~subjection(X18)|~bearer(X18,marketplace)|~cnt(X18,decl(distrib),concert_ds)|~part_of(X18,X16)|~about_event(X18,e1))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])])).
% 0.24/0.55 fof(c_0_35, plain, ![X19, X20, X21, X22, X23, X24]:((~power(X19)|~cnt(X19,decl(X20),X21)|~part_of(X19,X22)|~founds_rem(X23,X22,X24)|about_event(X19,X23))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_B2])])])).
% 0.24/0.55 fof(c_0_36, plain, ![X25, X26, X27, X28, X29, X30]:((~subjection(X25)|~cnt(X25,decl(X26),X27)|~part_of(X25,X28)|~founds_rem(X29,X28,X30)|about_event(X25,X29))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_B3])])])).
% 0.24/0.55 cnf(c_0_37, plain, (cnt(esk3_6(f1,marketplace,X1,distrib,X2,e1),decl(distrib),X2)|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 0.24/0.55 cnf(c_0_38, plain, (aer(f1,philharmonie)), inference(split_conjunct,[status(thm)],[aer_f1])).
% 0.24/0.55 cnf(c_0_39, plain, (subjection(esk3_6(f1,marketplace,X1,distrib,X2,e1))|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_28, c_0_27])).
% 0.24/0.55 cnf(c_0_40, plain, (bearer(esk3_6(f1,marketplace,X1,distrib,X2,e1),marketplace)|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_29, c_0_27])).
% 0.24/0.55 cnf(c_0_41, plain, (cnt(esk2_6(f1,X1,X2,distrib,X3,e1),decl(distrib),X3)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_30, c_0_19])).
% 0.24/0.55 cnf(c_0_42, plain, (power(esk2_6(f1,X1,X2,distrib,X3,e1))|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_31, c_0_19])).
% 0.24/0.55 cnf(c_0_43, plain, (bearer(esk2_6(f1,X1,X2,distrib,X3,e1),X2)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_32, c_0_19])).
% 0.24/0.55 cnf(c_0_44, plain, (founds_rem(X1,esk1_6(f1,X2,X3,distrib,X4,X1),f1)|~activates(X1,f1)|~tgt(f1,X4)|~aer(f1,X3)|~aee(f1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_45, plain, (part_of(esk2_6(X1,X2,X3,X4,X5,X6),esk1_6(X1,X2,X3,X4,X5,X6))|~proh(X1)|~has_rem(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_46, negated_conjecture, (~founds_rem(e1,X1,f1)|~power(X2)|~bearer(X2,philharmonie)|~cnt(X2,decl(distrib),concert_ds)|~part_of(X2,X1)|~about_event(X2,e1)|~subjection(X3)|~bearer(X3,marketplace)|~cnt(X3,decl(distrib),concert_ds)|~part_of(X3,X1)|~about_event(X3,e1)), inference(split_conjunct,[status(thm)],[c_0_34])).
% 0.24/0.55 cnf(c_0_47, plain, (about_event(X1,X5)|~power(X1)|~cnt(X1,decl(X2),X3)|~part_of(X1,X4)|~founds_rem(X5,X4,X6)), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.24/0.55 cnf(c_0_48, 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_36])).
% 0.24/0.55 cnf(c_0_49, plain, (cnt(esk3_6(f1,marketplace,philharmonie,distrib,X1,e1),decl(distrib),X1)|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 0.24/0.55 cnf(c_0_50, plain, (tgt(f1,concert_ds)), inference(split_conjunct,[status(thm)],[tgt_f1])).
% 0.24/0.55 cnf(c_0_51, plain, (subjection(esk3_6(f1,marketplace,philharmonie,distrib,X1,e1))|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_39, c_0_38])).
% 0.24/0.55 cnf(c_0_52, plain, (bearer(esk3_6(f1,marketplace,philharmonie,distrib,X1,e1),marketplace)|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_40, c_0_38])).
% 0.24/0.55 cnf(c_0_53, plain, (cnt(esk2_6(f1,marketplace,X1,distrib,X2,e1),decl(distrib),X2)|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_41, c_0_27])).
% 0.24/0.55 cnf(c_0_54, plain, (power(esk2_6(f1,marketplace,X1,distrib,X2,e1))|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_42, c_0_27])).
% 0.24/0.55 cnf(c_0_55, plain, (bearer(esk2_6(f1,marketplace,X1,distrib,X2,e1),X1)|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_43, c_0_27])).
% 0.24/0.55 cnf(c_0_56, plain, (founds_rem(e1,esk1_6(f1,X1,X2,distrib,X3,e1),f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_44, c_0_19])).
% 0.24/0.55 cnf(c_0_57, plain, (part_of(esk2_6(f1,X1,X2,distrib,X3,X4),esk1_6(f1,X1,X2,distrib,X3,X4))|~activates(X4,f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_58, plain, (part_of(esk3_6(X1,X2,X3,X4,X5,X6),esk1_6(X1,X2,X3,X4,X5,X6))|~proh(X1)|~has_rem(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~activates(X6,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_59, negated_conjecture, (~subjection(X1)|~power(X2)|~founds_rem(e1,X3,f1)|~part_of(X1,X3)|~part_of(X2,X3)|~cnt(X1,decl(distrib),concert_ds)|~cnt(X2,decl(distrib),concert_ds)|~bearer(X1,marketplace)|~bearer(X2,philharmonie)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_46, c_0_47]), c_0_48])).
% 0.24/0.55 cnf(c_0_60, plain, (cnt(esk3_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 0.24/0.55 cnf(c_0_61, plain, (subjection(esk3_6(f1,marketplace,philharmonie,distrib,concert_ds,e1))), inference(spm,[status(thm)],[c_0_51, c_0_50])).
% 0.24/0.55 cnf(c_0_62, plain, (bearer(esk3_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)), inference(spm,[status(thm)],[c_0_52, c_0_50])).
% 0.24/0.55 cnf(c_0_63, plain, (cnt(esk2_6(f1,marketplace,philharmonie,distrib,X1,e1),decl(distrib),X1)|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_53, c_0_38])).
% 0.24/0.55 cnf(c_0_64, plain, (power(esk2_6(f1,marketplace,philharmonie,distrib,X1,e1))|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_54, c_0_38])).
% 0.24/0.55 cnf(c_0_65, plain, (bearer(esk2_6(f1,marketplace,philharmonie,distrib,X1,e1),philharmonie)|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_55, c_0_38])).
% 0.24/0.55 cnf(c_0_66, plain, (founds_rem(e1,esk1_6(f1,marketplace,X1,distrib,X2,e1),f1)|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_56, c_0_27])).
% 0.24/0.55 cnf(c_0_67, plain, (part_of(esk2_6(f1,X1,X2,distrib,X3,e1),esk1_6(f1,X1,X2,distrib,X3,e1))|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_57, c_0_19])).
% 0.24/0.55 cnf(c_0_68, plain, (part_of(esk3_6(f1,X1,X2,distrib,X3,X4),esk1_6(f1,X1,X2,distrib,X3,X4))|~activates(X4,f1)|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_13]), c_0_14]), c_0_15])])).
% 0.24/0.55 cnf(c_0_69, negated_conjecture, (~power(X1)|~founds_rem(e1,X2,f1)|~part_of(esk3_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),X2)|~part_of(X1,X2)|~cnt(X1,decl(distrib),concert_ds)|~bearer(X1,philharmonie)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_60]), c_0_61]), c_0_62])])).
% 0.24/0.55 cnf(c_0_70, plain, (cnt(esk2_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)), inference(spm,[status(thm)],[c_0_63, c_0_50])).
% 0.24/0.55 cnf(c_0_71, plain, (power(esk2_6(f1,marketplace,philharmonie,distrib,concert_ds,e1))), inference(spm,[status(thm)],[c_0_64, c_0_50])).
% 0.24/0.55 cnf(c_0_72, plain, (bearer(esk2_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie)), inference(spm,[status(thm)],[c_0_65, c_0_50])).
% 0.24/0.55 cnf(c_0_73, plain, (founds_rem(e1,esk1_6(f1,marketplace,philharmonie,distrib,X1,e1),f1)|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_66, c_0_38])).
% 0.24/0.55 cnf(c_0_74, plain, (part_of(esk2_6(f1,marketplace,X1,distrib,X2,e1),esk1_6(f1,marketplace,X1,distrib,X2,e1))|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_67, c_0_27])).
% 0.24/0.55 cnf(c_0_75, plain, (part_of(esk3_6(f1,X1,X2,distrib,X3,e1),esk1_6(f1,X1,X2,distrib,X3,e1))|~tgt(f1,X3)|~aer(f1,X2)|~aee(f1,X1)), inference(spm,[status(thm)],[c_0_68, c_0_19])).
% 0.24/0.55 cnf(c_0_76, negated_conjecture, (~founds_rem(e1,X1,f1)|~part_of(esk3_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1)|~part_of(esk2_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_70]), c_0_71]), c_0_72])])).
% 0.24/0.55 cnf(c_0_77, plain, (founds_rem(e1,esk1_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1)), inference(spm,[status(thm)],[c_0_73, c_0_50])).
% 0.24/0.55 cnf(c_0_78, plain, (part_of(esk2_6(f1,marketplace,philharmonie,distrib,X1,e1),esk1_6(f1,marketplace,philharmonie,distrib,X1,e1))|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_74, c_0_38])).
% 0.24/0.55 cnf(c_0_79, plain, (part_of(esk3_6(f1,marketplace,X1,distrib,X2,e1),esk1_6(f1,marketplace,X1,distrib,X2,e1))|~tgt(f1,X2)|~aer(f1,X1)), inference(spm,[status(thm)],[c_0_75, c_0_27])).
% 0.24/0.55 cnf(c_0_80, negated_conjecture, (~part_of(esk3_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),esk1_6(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~part_of(esk2_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),esk1_6(f1,marketplace,philharmonie,distrib,concert_ds,e1))), inference(spm,[status(thm)],[c_0_76, c_0_77])).
% 0.24/0.55 cnf(c_0_81, plain, (part_of(esk2_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),esk1_6(f1,marketplace,philharmonie,distrib,concert_ds,e1))), inference(spm,[status(thm)],[c_0_78, c_0_50])).
% 0.24/0.55 cnf(c_0_82, plain, (part_of(esk3_6(f1,marketplace,philharmonie,distrib,X1,e1),esk1_6(f1,marketplace,philharmonie,distrib,X1,e1))|~tgt(f1,X1)), inference(spm,[status(thm)],[c_0_79, c_0_38])).
% 0.24/0.55 cnf(c_0_83, negated_conjecture, (~part_of(esk3_6(f1,marketplace,philharmonie,distrib,concert_ds,e1),esk1_6(f1,marketplace,philharmonie,distrib,concert_ds,e1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_80, c_0_81])])).
% 0.24/0.55 cnf(c_0_84, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_50]), c_0_83]), ['proof']).
% 0.24/0.55 % SZS output end Proof
% 0.24/0.55 % User time : 0.010 s
% 0.24/0.55 % System time : 0.003 s
% 0.24/0.55 % Total time : 0.013 s
% 0.24/0.55 % User time : 0.011 s
% 0.24/0.55 % System time : 0.007 s
% 0.24/0.55 % Total time : 0.018 s
% 0.24/0.55
%------------------------------------------------------------------------------