%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:18:53 AM UTC 2026
% Result : Theorem 0.56s 0.81s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.07/0.34 % Computer : n015.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 14:10:30 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.40 (re.compile("\."), Token.FullStop),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.40 (re.compile("\("), Token.OpenPar),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.40 (re.compile("\)"), Token.ClosePar),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.40 (re.compile("\["), Token.OpenSquare),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.40 (re.compile("~\|"), Token.Nor),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.40 (re.compile("\|"), Token.Or),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.40 (re.compile("\?"), Token.Existential),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.12/0.47 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.47 """
% 0.24/0.48 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.48 """
% 0.32/0.57 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.57 """
% 0.56/0.81 % Version: 1.5
% 0.56/0.81 % SZS status Theorem
% 0.56/0.81 % SZS output start CNFRefutation
% 0.56/0.81 fof(proh_f1,axiom,proh(f1),file('/export/starexec/sandbox/benchmark/theBenchmark.p', proh_f1)).
% 0.56/0.81 cnf(c11,plain,proh(f1),inference(split_conjunct,[status(thm)],[proh_f1])).
% 0.56/0.81 fof(rem_f1,axiom,has_rem(f1),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rem_f1)).
% 0.56/0.81 cnf(c10,plain,has_rem(f1),inference(split_conjunct,[status(thm)],[rem_f1])).
% 0.56/0.81 fof(aee_f1,axiom,aee(f1,marketplace),file('/export/starexec/sandbox/benchmark/theBenchmark.p', aee_f1)).
% 0.56/0.81 cnf(c9,plain,aee(f1,marketplace),inference(split_conjunct,[status(thm)],[aee_f1])).
% 0.56/0.81 fof(aer_f1,axiom,aer(f1,philharmonie),file('/export/starexec/sandbox/benchmark/theBenchmark.p', aer_f1)).
% 0.56/0.81 cnf(c8,plain,aer(f1,philharmonie),inference(split_conjunct,[status(thm)],[aer_f1])).
% 0.56/0.81 fof(act_f1,axiom,act(f1,distrib),file('/export/starexec/sandbox/benchmark/theBenchmark.p', act_f1)).
% 0.56/0.81 cnf(c7,plain,act(f1,distrib),inference(split_conjunct,[status(thm)],[act_f1])).
% 0.56/0.81 fof(tgt_f1,axiom,tgt(f1,concert_ds),file('/export/starexec/sandbox/benchmark/theBenchmark.p', tgt_f1)).
% 0.56/0.81 cnf(c6,plain,tgt(f1,concert_ds),inference(split_conjunct,[status(thm)],[tgt_f1])).
% 0.56/0.81 fof(act_e1_f1,axiom,activates(e1,f1),file('/export/starexec/sandbox/benchmark/theBenchmark.p', act_e1_f1)).
% 0.56/0.81 cnf(c5,plain,activates(e1,f1),inference(split_conjunct,[status(thm)],[act_e1_f1])).
% 0.56/0.81 fof(ax_proh_relator_remedy,axiom,(![F]:(![X]:(![Y]:(![A]:(![T]:(![E]:(((((((proh(F)&has_rem(F))&aee(F,X))&aer(F,Y))&act(F,A))&tgt(F,T))&activates(E,F))=>(?[RhoR]:(?[Pw]:(?[S]:((((((((founds_rem(E,RhoR,F)&power(Pw))&bearer(Pw,Y))&cnt(Pw,decl(A),T))&part_of(Pw,RhoR))&subjection(S))&bearer(S,X))&cnt(S,decl(A),T))&part_of(S,RhoR)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax_proh_relator_remedy)).
% 0.56/0.81 fof(c55,plain,(![F]:(![X]:(![Y]:(![A]:(![T]:(![E]:(((((((~proh(F)|~has_rem(F))|~aee(F,X))|~aer(F,Y))|~act(F,A))|~tgt(F,T))|~activates(E,F))|(?[RhoR]:(?[Pw]:(?[S]:((((((((founds_rem(E,RhoR,F)&power(Pw))&bearer(Pw,Y))&cnt(Pw,decl(A),T))&part_of(Pw,RhoR))&subjection(S))&bearer(S,X))&cnt(S,decl(A),T))&part_of(S,RhoR)))))))))))),inference(fof_nnf,[status(thm)],[ax_proh_relator_remedy])).
% 0.56/0.81 fof(c56,plain,(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|(?[X40]:(?[X41]:(?[X42]:((((((((founds_rem(X39,X40,X34)&power(X41))&bearer(X41,X36))&cnt(X41,decl(X37),X38))&part_of(X41,X40))&subjection(X42))&bearer(X42,X35))&cnt(X42,decl(X37),X38))&part_of(X42,X40)))))))))))),inference(variable_rename,[status(thm)],[c55])).
% 0.56/0.81 fof(c57,plain,(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|((((((((founds_rem(X39,skolem0007(X34,X35,X36,X37,X38,X39),X34)&power(skolem0008(X34,X35,X36,X37,X38,X39)))&bearer(skolem0008(X34,X35,X36,X37,X38,X39),X36))&cnt(skolem0008(X34,X35,X36,X37,X38,X39),decl(X37),X38))&part_of(skolem0008(X34,X35,X36,X37,X38,X39),skolem0007(X34,X35,X36,X37,X38,X39)))&subjection(skolem0009(X34,X35,X36,X37,X38,X39)))&bearer(skolem0009(X34,X35,X36,X37,X38,X39),X35))&cnt(skolem0009(X34,X35,X36,X37,X38,X39),decl(X37),X38))&part_of(skolem0009(X34,X35,X36,X37,X38,X39),skolem0007(X34,X35,X36,X37,X38,X39)))))))))),inference(skolemize,[status(esa)],[c56])).
% 0.56/0.81 fof(c58,plain,(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(((((((((((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|founds_rem(X39,skolem0007(X34,X35,X36,X37,X38,X39),X34))&(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|power(skolem0008(X34,X35,X36,X37,X38,X39))))&(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|bearer(skolem0008(X34,X35,X36,X37,X38,X39),X36)))&(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|cnt(skolem0008(X34,X35,X36,X37,X38,X39),decl(X37),X38)))&(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|part_of(skolem0008(X34,X35,X36,X37,X38,X39),skolem0007(X34,X35,X36,X37,X38,X39))))&(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|subjection(skolem0009(X34,X35,X36,X37,X38,X39))))&(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|bearer(skolem0009(X34,X35,X36,X37,X38,X39),X35)))&(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|cnt(skolem0009(X34,X35,X36,X37,X38,X39),decl(X37),X38)))&(((((((~proh(X34)|~has_rem(X34))|~aee(X34,X35))|~aer(X34,X36))|~act(X34,X37))|~tgt(X34,X38))|~activates(X39,X34))|part_of(skolem0009(X34,X35,X36,X37,X38,X39),skolem0007(X34,X35,X36,X37,X38,X39)))))))))),inference(distribute,[status(thm)],[c57])).
% 0.56/0.81 cnf(c60,plain,~proh(X133)|~has_rem(X133)|~aee(X133,X138)|~aer(X133,X134)|~act(X133,X137)|~tgt(X133,X135)|~activates(X136,X133)|power(skolem0008(X133,X138,X134,X137,X135,X136)),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.81 cnf(c95,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X262)|~aer(f1,X264)|~act(f1,X265)|~tgt(f1,X263)|power(skolem0008(f1,X262,X264,X265,X263,e1)),inference(resolution,[status(thm)],[c60, c5])).
% 0.56/0.81 cnf(c141,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X268)|~aer(f1,X267)|~act(f1,X266)|power(skolem0008(f1,X268,X267,X266,concert_ds,e1)),inference(resolution,[status(thm)],[c95, c6])).
% 0.56/0.81 cnf(c142,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X269)|~aer(f1,X270)|power(skolem0008(f1,X269,X270,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c141, c7])).
% 0.56/0.81 cnf(c143,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X275)|power(skolem0008(f1,X275,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c142, c8])).
% 0.56/0.81 cnf(c145,plain,~proh(f1)|~has_rem(f1)|power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c143, c9])).
% 0.56/0.81 cnf(c146,plain,~proh(f1)|power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c145, c10])).
% 0.56/0.81 cnf(c147,plain,power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c146, c11])).
% 0.56/0.81 cnf(c64,plain,~proh(X145)|~has_rem(X145)|~aee(X145,X150)|~aer(X145,X146)|~act(X145,X149)|~tgt(X145,X147)|~activates(X148,X145)|subjection(skolem0009(X145,X150,X146,X149,X147,X148)),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.81 cnf(c97,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X281)|~aer(f1,X282)|~act(f1,X279)|~tgt(f1,X280)|subjection(skolem0009(f1,X281,X282,X279,X280,e1)),inference(resolution,[status(thm)],[c64, c5])).
% 0.56/0.81 cnf(c149,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X291)|~aer(f1,X292)|~act(f1,X290)|subjection(skolem0009(f1,X291,X292,X290,concert_ds,e1)),inference(resolution,[status(thm)],[c97, c6])).
% 0.56/0.81 cnf(c155,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X294)|~aer(f1,X293)|subjection(skolem0009(f1,X294,X293,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c149, c7])).
% 0.56/0.81 cnf(c156,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X295)|subjection(skolem0009(f1,X295,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c155, c8])).
% 0.56/0.81 cnf(c157,plain,~proh(f1)|~has_rem(f1)|subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c156, c9])).
% 0.56/0.81 cnf(c158,plain,~proh(f1)|subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c157, c10])).
% 0.56/0.81 cnf(c159,plain,subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c158, c11])).
% 0.56/0.81 cnf(c61,plain,~proh(X139)|~has_rem(X139)|~aee(X139,X144)|~aer(X139,X140)|~act(X139,X143)|~tgt(X139,X141)|~activates(X142,X139)|bearer(skolem0008(X139,X144,X140,X143,X141,X142),X140),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.82 cnf(c96,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X274)|~aer(f1,X272)|~act(f1,X273)|~tgt(f1,X271)|bearer(skolem0008(f1,X274,X272,X273,X271,e1),X272),inference(resolution,[status(thm)],[c61, c5])).
% 0.56/0.82 cnf(c144,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X276)|~aer(f1,X277)|~act(f1,X278)|bearer(skolem0008(f1,X276,X277,X278,concert_ds,e1),X277),inference(resolution,[status(thm)],[c96, c6])).
% 0.56/0.82 cnf(c148,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X283)|~aer(f1,X284)|bearer(skolem0008(f1,X283,X284,distrib,concert_ds,e1),X284),inference(resolution,[status(thm)],[c144, c7])).
% 0.56/0.82 cnf(c150,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X285)|bearer(skolem0008(f1,X285,philharmonie,distrib,concert_ds,e1),philharmonie),inference(resolution,[status(thm)],[c148, c8])).
% 0.56/0.82 cnf(c151,plain,~proh(f1)|~has_rem(f1)|bearer(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie),inference(resolution,[status(thm)],[c150, c9])).
% 0.56/0.82 cnf(c152,plain,~proh(f1)|bearer(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie),inference(resolution,[status(thm)],[c151, c10])).
% 0.56/0.82 cnf(c153,plain,bearer(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie),inference(resolution,[status(thm)],[c152, c11])).
% 0.56/0.82 cnf(c59,plain,~proh(X121)|~has_rem(X121)|~aee(X121,X126)|~aer(X121,X122)|~act(X121,X125)|~tgt(X121,X123)|~activates(X124,X121)|founds_rem(X124,skolem0007(X121,X126,X122,X125,X123,X124),X121),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.82 cnf(c91,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X259)|~aer(f1,X258)|~act(f1,X261)|~tgt(f1,X260)|founds_rem(e1,skolem0007(f1,X259,X258,X261,X260,e1),f1),inference(resolution,[status(thm)],[c59, c5])).
% 0.56/0.82 cnf(c139,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X344)|~aer(f1,X343)|~act(f1,X342)|founds_rem(e1,skolem0007(f1,X344,X343,X342,concert_ds,e1),f1),inference(resolution,[status(thm)],[c91, c6])).
% 0.56/0.82 cnf(c186,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X346)|~aer(f1,X345)|founds_rem(e1,skolem0007(f1,X346,X345,distrib,concert_ds,e1),f1),inference(resolution,[status(thm)],[c139, c7])).
% 0.56/0.82 cnf(c187,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X347)|founds_rem(e1,skolem0007(f1,X347,philharmonie,distrib,concert_ds,e1),f1),inference(resolution,[status(thm)],[c186, c8])).
% 0.56/0.82 cnf(c188,plain,~proh(f1)|~has_rem(f1)|founds_rem(e1,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1),inference(resolution,[status(thm)],[c187, c9])).
% 0.56/0.82 cnf(c189,plain,~proh(f1)|founds_rem(e1,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1),inference(resolution,[status(thm)],[c188, c10])).
% 0.56/0.82 cnf(c190,plain,founds_rem(e1,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1),inference(resolution,[status(thm)],[c189, c11])).
% 0.56/0.82 cnf(c63,plain,~proh(X176)|~has_rem(X176)|~aee(X176,X181)|~aer(X176,X177)|~act(X176,X180)|~tgt(X176,X178)|~activates(X179,X176)|part_of(skolem0008(X176,X181,X177,X180,X178,X179),skolem0007(X176,X181,X177,X180,X178,X179)),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.82 cnf(c107,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X299)|~aer(f1,X297)|~act(f1,X296)|~tgt(f1,X298)|part_of(skolem0008(f1,X299,X297,X296,X298,e1),skolem0007(f1,X299,X297,X296,X298,e1)),inference(resolution,[status(thm)],[c63, c5])).
% 0.56/0.82 cnf(c160,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X358)|~aer(f1,X359)|~act(f1,X360)|part_of(skolem0008(f1,X358,X359,X360,concert_ds,e1),skolem0007(f1,X358,X359,X360,concert_ds,e1)),inference(resolution,[status(thm)],[c107, c6])).
% 0.56/0.82 cnf(c196,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X382)|~aer(f1,X383)|part_of(skolem0008(f1,X382,X383,distrib,concert_ds,e1),skolem0007(f1,X382,X383,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c160, c7])).
% 0.56/0.82 cnf(c220,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X384)|part_of(skolem0008(f1,X384,philharmonie,distrib,concert_ds,e1),skolem0007(f1,X384,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c196, c8])).
% 0.56/0.82 cnf(c221,plain,~proh(f1)|~has_rem(f1)|part_of(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c220, c9])).
% 0.56/0.82 cnf(c222,plain,~proh(f1)|part_of(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c221, c10])).
% 0.56/0.82 cnf(c223,plain,part_of(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c222, c11])).
% 0.56/0.82 fof(ax_B2,axiom,(![Pw]:(![A]:(![T]:(![Rho]:(![E]:(![R]:((((power(Pw)&cnt(Pw,decl(A),T))&part_of(Pw,Rho))&founds_rem(E,Rho,R))=>about_event(Pw,E)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax_B2)).
% 0.56/0.82 fof(c23,plain,(![Pw]:(![A]:(![T]:(![Rho]:(![E]:(![R]:((((~power(Pw)|~cnt(Pw,decl(A),T))|~part_of(Pw,Rho))|~founds_rem(E,Rho,R))|about_event(Pw,E)))))))),inference(fof_nnf,[status(thm)],[ax_B2])).
% 0.56/0.82 fof(c24,plain,(![Pw]:(![A]:(![T]:(![Rho]:(![E]:((((~power(Pw)|~cnt(Pw,decl(A),T))|~part_of(Pw,Rho))|(![R]:~founds_rem(E,Rho,R)))|about_event(Pw,E))))))),inference(shift_quantors,[status(thm)],[c23])).
% 0.56/0.82 fof(c26,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((((~power(X11)|~cnt(X11,decl(X12),X13))|~part_of(X11,X14))|~founds_rem(X15,X14,X16))|about_event(X11,X15)))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:((((~power(X11)|~cnt(X11,decl(X12),X13))|~part_of(X11,X14))|(![X16]:~founds_rem(X15,X14,X16)))|about_event(X11,X15))))))),inference(variable_rename,[status(thm)],[c24])).])).
% 0.56/0.82 cnf(c27,plain,~power(X77)|~cnt(X77,decl(X74),X78)|~part_of(X77,X79)|~founds_rem(X76,X79,X75)|about_event(X77,X76),inference(split_conjunct,[status(thm)],[c26])).
% 0.56/0.82 cnf(c62,plain,~proh(X161)|~has_rem(X161)|~aee(X161,X166)|~aer(X161,X162)|~act(X161,X165)|~tgt(X161,X163)|~activates(X164,X161)|cnt(skolem0008(X161,X166,X162,X165,X163,X164),decl(X165),X163),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.82 cnf(c102,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X288)|~aer(f1,X286)|~act(f1,X289)|~tgt(f1,X287)|cnt(skolem0008(f1,X288,X286,X289,X287,e1),decl(X289),X287),inference(resolution,[status(thm)],[c62, c5])).
% 0.56/0.82 cnf(c154,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X352)|~aer(f1,X354)|~act(f1,X353)|cnt(skolem0008(f1,X352,X354,X353,concert_ds,e1),decl(X353),concert_ds),inference(resolution,[status(thm)],[c102, c6])).
% 0.56/0.82 cnf(c192,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X355)|~aer(f1,X356)|cnt(skolem0008(f1,X355,X356,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c154, c7])).
% 0.56/0.82 cnf(c193,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X357)|cnt(skolem0008(f1,X357,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c192, c8])).
% 0.56/0.82 cnf(c194,plain,~proh(f1)|~has_rem(f1)|cnt(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c193, c9])).
% 0.56/0.82 cnf(c195,plain,~proh(f1)|cnt(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c194, c10])).
% 0.56/0.82 cnf(c197,plain,cnt(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c195, c11])).
% 0.56/0.82 cnf(c199,plain,~power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~part_of(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),X395)|~founds_rem(X394,X395,X393)|about_event(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),X394),inference(resolution,[status(thm)],[c197, c27])).
% 0.56/0.82 cnf(c230,plain,~power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~founds_rem(X396,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1),X397)|about_event(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),X396),inference(resolution,[status(thm)],[c199, c223])).
% 0.56/0.82 cnf(c231,plain,~power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1))|about_event(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),inference(resolution,[status(thm)],[c230, c190])).
% 0.56/0.82 cnf(c232,plain,about_event(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),inference(resolution,[status(thm)],[c231, c147])).
% 0.56/0.82 cnf(c65,plain,~proh(X183)|~has_rem(X183)|~aee(X183,X188)|~aer(X183,X184)|~act(X183,X187)|~tgt(X183,X185)|~activates(X186,X183)|bearer(skolem0009(X183,X188,X184,X187,X185,X186),X188),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.82 cnf(c110,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X313)|~aer(f1,X312)|~act(f1,X311)|~tgt(f1,X310)|bearer(skolem0009(f1,X313,X312,X311,X310,e1),X313),inference(resolution,[status(thm)],[c65, c5])).
% 0.56/0.82 cnf(c165,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X314)|~aer(f1,X315)|~act(f1,X316)|bearer(skolem0009(f1,X314,X315,X316,concert_ds,e1),X314),inference(resolution,[status(thm)],[c110, c6])).
% 0.56/0.82 cnf(c167,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X317)|~aer(f1,X318)|bearer(skolem0009(f1,X317,X318,distrib,concert_ds,e1),X317),inference(resolution,[status(thm)],[c165, c7])).
% 0.56/0.82 cnf(c168,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X319)|bearer(skolem0009(f1,X319,philharmonie,distrib,concert_ds,e1),X319),inference(resolution,[status(thm)],[c167, c8])).
% 0.56/0.82 cnf(c169,plain,~proh(f1)|~has_rem(f1)|bearer(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),inference(resolution,[status(thm)],[c168, c9])).
% 0.56/0.82 cnf(c171,plain,~proh(f1)|bearer(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),inference(resolution,[status(thm)],[c169, c10])).
% 0.56/0.82 cnf(c172,plain,bearer(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),inference(resolution,[status(thm)],[c171, c11])).
% 0.56/0.82 cnf(c67,plain,~proh(X217)|~has_rem(X217)|~aee(X217,X222)|~aer(X217,X218)|~act(X217,X221)|~tgt(X217,X219)|~activates(X220,X217)|part_of(skolem0009(X217,X222,X218,X221,X219,X220),skolem0007(X217,X222,X218,X221,X219,X220)),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.82 cnf(c118,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X334)|~aer(f1,X333)|~act(f1,X331)|~tgt(f1,X332)|part_of(skolem0009(f1,X334,X333,X331,X332,e1),skolem0007(f1,X334,X333,X331,X332,e1)),inference(resolution,[status(thm)],[c67, c5])).
% 0.56/0.82 cnf(c175,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X369)|~aer(f1,X367)|~act(f1,X368)|part_of(skolem0009(f1,X369,X367,X368,concert_ds,e1),skolem0007(f1,X369,X367,X368,concert_ds,e1)),inference(resolution,[status(thm)],[c118, c6])).
% 0.56/0.82 cnf(c205,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X386)|~aer(f1,X385)|part_of(skolem0009(f1,X386,X385,distrib,concert_ds,e1),skolem0007(f1,X386,X385,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c175, c7])).
% 0.56/0.82 cnf(c224,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X387)|part_of(skolem0009(f1,X387,philharmonie,distrib,concert_ds,e1),skolem0007(f1,X387,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c205, c8])).
% 0.56/0.82 cnf(c225,plain,~proh(f1)|~has_rem(f1)|part_of(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c224, c9])).
% 0.56/0.82 cnf(c226,plain,~proh(f1)|part_of(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c225, c10])).
% 0.56/0.82 cnf(c227,plain,part_of(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c226, c11])).
% 0.56/0.82 fof(ax_B3,axiom,(![S]:(![A]:(![T]:(![Rho]:(![E]:(![R]:((((subjection(S)&cnt(S,decl(A),T))&part_of(S,Rho))&founds_rem(E,Rho,R))=>about_event(S,E)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax_B3)).
% 0.56/0.82 fof(c18,plain,(![S]:(![A]:(![T]:(![Rho]:(![E]:(![R]:((((~subjection(S)|~cnt(S,decl(A),T))|~part_of(S,Rho))|~founds_rem(E,Rho,R))|about_event(S,E)))))))),inference(fof_nnf,[status(thm)],[ax_B3])).
% 0.56/0.82 fof(c19,plain,(![S]:(![A]:(![T]:(![Rho]:(![E]:((((~subjection(S)|~cnt(S,decl(A),T))|~part_of(S,Rho))|(![R]:~founds_rem(E,Rho,R)))|about_event(S,E))))))),inference(shift_quantors,[status(thm)],[c18])).
% 0.56/0.82 fof(c21,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((((~subjection(X5)|~cnt(X5,decl(X6),X7))|~part_of(X5,X8))|~founds_rem(X9,X8,X10))|about_event(X5,X9)))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((((~subjection(X5)|~cnt(X5,decl(X6),X7))|~part_of(X5,X8))|(![X10]:~founds_rem(X9,X8,X10)))|about_event(X5,X9))))))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.56/0.82 cnf(c22,plain,~subjection(X62)|~cnt(X62,decl(X60),X63)|~part_of(X62,X58)|~founds_rem(X59,X58,X61)|about_event(X62,X59),inference(split_conjunct,[status(thm)],[c21])).
% 0.56/0.82 cnf(c66,plain,~proh(X195)|~has_rem(X195)|~aee(X195,X200)|~aer(X195,X196)|~act(X195,X199)|~tgt(X195,X197)|~activates(X198,X195)|cnt(skolem0009(X195,X200,X196,X199,X197,X198),decl(X199),X197),inference(split_conjunct,[status(thm)],[c58])).
% 0.56/0.82 cnf(c112,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X322)|~aer(f1,X320)|~act(f1,X321)|~tgt(f1,X323)|cnt(skolem0009(f1,X322,X320,X321,X323,e1),decl(X321),X323),inference(resolution,[status(thm)],[c66, c5])).
% 0.56/0.82 cnf(c170,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X361)|~aer(f1,X363)|~act(f1,X362)|cnt(skolem0009(f1,X361,X363,X362,concert_ds,e1),decl(X362),concert_ds),inference(resolution,[status(thm)],[c112, c6])).
% 0.56/0.82 cnf(c202,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X365)|~aer(f1,X364)|cnt(skolem0009(f1,X365,X364,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c170, c7])).
% 0.56/0.82 cnf(c203,plain,~proh(f1)|~has_rem(f1)|~aee(f1,X366)|cnt(skolem0009(f1,X366,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c202, c8])).
% 0.56/0.82 cnf(c204,plain,~proh(f1)|~has_rem(f1)|cnt(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c203, c9])).
% 0.56/0.82 cnf(c206,plain,~proh(f1)|cnt(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c204, c10])).
% 0.56/0.82 cnf(c207,plain,cnt(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),inference(resolution,[status(thm)],[c206, c11])).
% 0.56/0.82 cnf(c208,plain,~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~part_of(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),X400)|~founds_rem(X402,X400,X401)|about_event(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),X402),inference(resolution,[status(thm)],[c207, c22])).
% 0.56/0.82 cnf(c235,plain,~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~founds_rem(X403,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1),X404)|about_event(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),X403),inference(resolution,[status(thm)],[c208, c227])).
% 0.56/0.82 cnf(c236,plain,~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1))|about_event(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),inference(resolution,[status(thm)],[c235, c190])).
% 0.56/0.82 cnf(c237,plain,about_event(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),inference(resolution,[status(thm)],[c236, c159])).
% 0.56/0.82 fof(conjecture,conjecture,(?[RhoR]:(?[Pw]:(?[S]:((((((((((founds_rem(e1,RhoR,f1)&power(Pw))&bearer(Pw,philharmonie))&cnt(Pw,decl(distrib),concert_ds))&part_of(Pw,RhoR))&about_event(Pw,e1))&subjection(S))&bearer(S,marketplace))&cnt(S,decl(distrib),concert_ds))&part_of(S,RhoR))&about_event(S,e1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture)).
% 0.56/0.82 fof(c0,negated_conjecture,(~(?[RhoR]:(?[Pw]:(?[S]:((((((((((founds_rem(e1,RhoR,f1)&power(Pw))&bearer(Pw,philharmonie))&cnt(Pw,decl(distrib),concert_ds))&part_of(Pw,RhoR))&about_event(Pw,e1))&subjection(S))&bearer(S,marketplace))&cnt(S,decl(distrib),concert_ds))&part_of(S,RhoR))&about_event(S,e1)))))),inference(assume_negation,[status(cth)],[conjecture])).
% 0.56/0.82 fof(c1,negated_conjecture,(![RhoR]:(![Pw]:(![S]:((((((((((~founds_rem(e1,RhoR,f1)|~power(Pw))|~bearer(Pw,philharmonie))|~cnt(Pw,decl(distrib),concert_ds))|~part_of(Pw,RhoR))|~about_event(Pw,e1))|~subjection(S))|~bearer(S,marketplace))|~cnt(S,decl(distrib),concert_ds))|~part_of(S,RhoR))|~about_event(S,e1))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.56/0.82 fof(c2,negated_conjecture,(![X2]:(![X3]:(![X4]:((((((((((~founds_rem(e1,X2,f1)|~power(X3))|~bearer(X3,philharmonie))|~cnt(X3,decl(distrib),concert_ds))|~part_of(X3,X2))|~about_event(X3,e1))|~subjection(X4))|~bearer(X4,marketplace))|~cnt(X4,decl(distrib),concert_ds))|~part_of(X4,X2))|~about_event(X4,e1))))),inference(variable_rename,[status(thm)],[c1])).
% 0.56/0.82 cnf(c3,negated_conjecture,~founds_rem(e1,X53,f1)|~power(X54)|~bearer(X54,philharmonie)|~cnt(X54,decl(distrib),concert_ds)|~part_of(X54,X53)|~about_event(X54,e1)|~subjection(X52)|~bearer(X52,marketplace)|~cnt(X52,decl(distrib),concert_ds)|~part_of(X52,X53)|~about_event(X52,e1),inference(split_conjunct,[status(thm)],[c2])).
% 0.56/0.82 cnf(c210,plain,~founds_rem(e1,X414,f1)|~power(X415)|~bearer(X415,philharmonie)|~cnt(X415,decl(distrib),concert_ds)|~part_of(X415,X414)|~about_event(X415,e1)|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~bearer(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)|~part_of(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),X414)|~about_event(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),inference(resolution,[status(thm)],[c207, c3])).
% 0.56/0.82 cnf(c244,plain,~founds_rem(e1,X418,f1)|~power(X417)|~bearer(X417,philharmonie)|~cnt(X417,decl(distrib),concert_ds)|~part_of(X417,X418)|~about_event(X417,e1)|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~bearer(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)|~part_of(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),X418),inference(resolution,[status(thm)],[c210, c237])).
% 0.56/0.82 cnf(c246,plain,~founds_rem(e1,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1)|~power(X419)|~bearer(X419,philharmonie)|~cnt(X419,decl(distrib),concert_ds)|~part_of(X419,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~about_event(X419,e1)|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~bearer(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),inference(resolution,[status(thm)],[c244, c227])).
% 0.56/0.82 cnf(c247,plain,~power(X420)|~bearer(X420,philharmonie)|~cnt(X420,decl(distrib),concert_ds)|~part_of(X420,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~about_event(X420,e1)|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~bearer(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),inference(resolution,[status(thm)],[c246, c190])).
% 0.56/0.82 cnf(c248,plain,~power(X421)|~bearer(X421,philharmonie)|~cnt(X421,decl(distrib),concert_ds)|~part_of(X421,skolem0007(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~about_event(X421,e1)|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c247, c172])).
% 0.56/0.82 cnf(c250,plain,~power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~bearer(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie)|~cnt(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)|~about_event(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c248, c223])).
% 0.56/0.82 cnf(c254,plain,~power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~bearer(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie)|~about_event(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c250, c197])).
% 0.56/0.82 cnf(c255,plain,~power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~bearer(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie)|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c254, c232])).
% 0.56/0.82 cnf(c256,plain,~power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1))|~subjection(skolem0009(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c255, c153])).
% 0.56/0.82 cnf(c257,plain,~power(skolem0008(f1,marketplace,philharmonie,distrib,concert_ds,e1)),inference(resolution,[status(thm)],[c256, c159])).
% 0.56/0.82 cnf(c258,plain,$false,inference(resolution,[status(thm)],[c257, c147])).
% 0.56/0.82 % SZS output end CNFRefutation
% 0.56/0.82
% 0.56/0.82 % Initial clauses : 46
% 0.56/0.82 % Processed clauses : 217
% 0.56/0.82 % Factors computed : 5
% 0.56/0.82 % Resolvents computed: 173
% 0.56/0.82 % Tautologies deleted: 0
% 0.56/0.82 % Forward subsumed : 2
% 0.56/0.82 % Backward subsumed : 53
% 0.56/0.82 % -------- CPU Time ---------
% 0.56/0.82 % User time : 0.446 s
% 0.56/0.82 % System time : 0.029 s
% 0.56/0.82 % Total time : 0.475 s
%------------------------------------------------------------------------------