%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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.39s 0.66s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 7 14:01:09 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.10/0.43 (re.compile("\."), Token.FullStop),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.10/0.43 (re.compile("\("), Token.OpenPar),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.10/0.43 (re.compile("\)"), Token.ClosePar),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.10/0.43 (re.compile("\["), Token.OpenSquare),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.10/0.44 (re.compile("\]"), Token.CloseSquare),
% 0.10/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.44 (re.compile("~\|"), Token.Nor),
% 0.10/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.44 (re.compile("\|"), Token.Or),
% 0.10/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.10/0.44 (re.compile("\?"), Token.Existential),
% 0.10/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.10/0.44 (re.compile("\s+"), Token.WhiteSpace),
% 0.10/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.10/0.44 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.22/0.51 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.51 """
% 0.32/0.60 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.60 """
% 0.39/0.66 % Version: 1.5
% 0.39/0.66 % SZS status Theorem
% 0.39/0.66 % SZS output start CNFRefutation
% 0.39/0.66 fof(agent_portal,axiom,agent(portal),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', agent_portal)).
% 0.39/0.66 cnf(c29,plain,agent(portal),inference(split_conjunct,[status(thm)],[agent_portal])).
% 0.39/0.66 fof(action_modify,axiom,action(modify_act),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', action_modify)).
% 0.39/0.66 cnf(c27,plain,action(modify_act),inference(split_conjunct,[status(thm)],[action_modify])).
% 0.39/0.66 fof(target_theater,axiom,target(theater_ds),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', target_theater)).
% 0.39/0.66 cnf(c26,plain,target(theater_ds),inference(split_conjunct,[status(thm)],[target_theater])).
% 0.39/0.66 fof(open_world_closure,axiom,(![X]:(![A]:(![T]:((((agent(X)&action(A))&target(T))&(~(?[F]:(?[E]:(((proh(F)&aee(F,X))&act(F,A))&activates(E,F))))))=>(?[L]:((permission(L)&bearer(L,X))&cnt(L,A,T))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', open_world_closure)).
% 0.39/0.66 fof(c4,plain,(![X]:(![A]:(![T]:((((~agent(X)|~action(A))|~target(T))|(?[F]:(?[E]:(((proh(F)&aee(F,X))&act(F,A))&activates(E,F)))))|(?[L]:((permission(L)&bearer(L,X))&cnt(L,A,T))))))),inference(fof_nnf,[status(thm)],[open_world_closure])).
% 0.39/0.66 fof(c5,plain,(![X]:(![A]:(![T]:((((~agent(X)|~action(A))|~target(T))|(?[F]:(((proh(F)&aee(F,X))&act(F,A))&(?[E]:activates(E,F)))))|(?[L]:((permission(L)&bearer(L,X))&cnt(L,A,T))))))),inference(shift_quantors,[status(thm)],[c4])).
% 0.39/0.66 fof(c6,plain,(![X3]:(![X4]:(![X5]:((((~agent(X3)|~action(X4))|~target(X5))|(?[X6]:(((proh(X6)&aee(X6,X3))&act(X6,X4))&(?[X7]:activates(X7,X6)))))|(?[X8]:((permission(X8)&bearer(X8,X3))&cnt(X8,X4,X5))))))),inference(variable_rename,[status(thm)],[c5])).
% 0.39/0.66 fof(c7,plain,(![X3]:(![X4]:(![X5]:((((~agent(X3)|~action(X4))|~target(X5))|(((proh(skolem0001(X3,X4,X5))&aee(skolem0001(X3,X4,X5),X3))&act(skolem0001(X3,X4,X5),X4))&activates(skolem0002(X3,X4,X5),skolem0001(X3,X4,X5))))|((permission(skolem0003(X3,X4,X5))&bearer(skolem0003(X3,X4,X5),X3))&cnt(skolem0003(X3,X4,X5),X4,X5)))))),inference(skolemize,[status(esa)],[c6])).
% 0.39/0.66 fof(c8,plain,(![X3]:(![X4]:(![X5]:(((((((((~agent(X3)|~action(X4))|~target(X5))|proh(skolem0001(X3,X4,X5)))|permission(skolem0003(X3,X4,X5)))&((((~agent(X3)|~action(X4))|~target(X5))|proh(skolem0001(X3,X4,X5)))|bearer(skolem0003(X3,X4,X5),X3)))&((((~agent(X3)|~action(X4))|~target(X5))|proh(skolem0001(X3,X4,X5)))|cnt(skolem0003(X3,X4,X5),X4,X5)))&((((((~agent(X3)|~action(X4))|~target(X5))|aee(skolem0001(X3,X4,X5),X3))|permission(skolem0003(X3,X4,X5)))&((((~agent(X3)|~action(X4))|~target(X5))|aee(skolem0001(X3,X4,X5),X3))|bearer(skolem0003(X3,X4,X5),X3)))&((((~agent(X3)|~action(X4))|~target(X5))|aee(skolem0001(X3,X4,X5),X3))|cnt(skolem0003(X3,X4,X5),X4,X5))))&((((((~agent(X3)|~action(X4))|~target(X5))|act(skolem0001(X3,X4,X5),X4))|permission(skolem0003(X3,X4,X5)))&((((~agent(X3)|~action(X4))|~target(X5))|act(skolem0001(X3,X4,X5),X4))|bearer(skolem0003(X3,X4,X5),X3)))&((((~agent(X3)|~action(X4))|~target(X5))|act(skolem0001(X3,X4,X5),X4))|cnt(skolem0003(X3,X4,X5),X4,X5))))&((((((~agent(X3)|~action(X4))|~target(X5))|activates(skolem0002(X3,X4,X5),skolem0001(X3,X4,X5)))|permission(skolem0003(X3,X4,X5)))&((((~agent(X3)|~action(X4))|~target(X5))|activates(skolem0002(X3,X4,X5),skolem0001(X3,X4,X5)))|bearer(skolem0003(X3,X4,X5),X3)))&((((~agent(X3)|~action(X4))|~target(X5))|activates(skolem0002(X3,X4,X5),skolem0001(X3,X4,X5)))|cnt(skolem0003(X3,X4,X5),X4,X5))))))),inference(distribute,[status(thm)],[c7])).
% 0.39/0.66 cnf(c9,plain,~agent(X13)|~action(X14)|~target(X12)|proh(skolem0001(X13,X14,X12))|permission(skolem0003(X13,X14,X12)),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c30,plain,~agent(X17)|~action(X18)|proh(skolem0001(X17,X18,theater_ds))|permission(skolem0003(X17,X18,theater_ds)),inference(resolution,[status(thm)],[c9, c26])).
% 0.39/0.66 cnf(c31,plain,~agent(X19)|proh(skolem0001(X19,modify_act,theater_ds))|permission(skolem0003(X19,modify_act,theater_ds)),inference(resolution,[status(thm)],[c30, c27])).
% 0.39/0.66 cnf(c33,plain,proh(skolem0001(portal,modify_act,theater_ds))|permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c31, c29])).
% 0.39/0.66 cnf(c10,plain,~agent(X21)|~action(X22)|~target(X20)|proh(skolem0001(X21,X22,X20))|bearer(skolem0003(X21,X22,X20),X21),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c34,plain,~agent(X24)|~action(X23)|proh(skolem0001(X24,X23,theater_ds))|bearer(skolem0003(X24,X23,theater_ds),X24),inference(resolution,[status(thm)],[c10, c26])).
% 0.39/0.66 cnf(c35,plain,~agent(X25)|proh(skolem0001(X25,modify_act,theater_ds))|bearer(skolem0003(X25,modify_act,theater_ds),X25),inference(resolution,[status(thm)],[c34, c27])).
% 0.39/0.66 cnf(c37,plain,proh(skolem0001(portal,modify_act,theater_ds))|bearer(skolem0003(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c35, c29])).
% 0.39/0.66 fof(conjecture,conjecture,(?[L]:((permission(L)&bearer(L,portal))&cnt(L,modify_act,theater_ds))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conjecture)).
% 0.39/0.66 fof(c0,negated_conjecture,(~(?[L]:((permission(L)&bearer(L,portal))&cnt(L,modify_act,theater_ds)))),inference(assume_negation,[status(cth)],[conjecture])).
% 0.39/0.66 fof(c1,negated_conjecture,(![L]:((~permission(L)|~bearer(L,portal))|~cnt(L,modify_act,theater_ds))),inference(fof_nnf,[status(thm)],[c0])).
% 0.39/0.66 fof(c2,negated_conjecture,(![X2]:((~permission(X2)|~bearer(X2,portal))|~cnt(X2,modify_act,theater_ds))),inference(variable_rename,[status(thm)],[c1])).
% 0.39/0.66 cnf(c3,negated_conjecture,~permission(X11)|~bearer(X11,portal)|~cnt(X11,modify_act,theater_ds),inference(split_conjunct,[status(thm)],[c2])).
% 0.39/0.66 cnf(c11,plain,~agent(X30)|~action(X31)|~target(X29)|proh(skolem0001(X30,X31,X29))|cnt(skolem0003(X30,X31,X29),X31,X29),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c39,plain,~agent(X59)|~action(X60)|proh(skolem0001(X59,X60,theater_ds))|cnt(skolem0003(X59,X60,theater_ds),X60,theater_ds),inference(resolution,[status(thm)],[c11, c26])).
% 0.39/0.66 cnf(c57,plain,~agent(X61)|proh(skolem0001(X61,modify_act,theater_ds))|cnt(skolem0003(X61,modify_act,theater_ds),modify_act,theater_ds),inference(resolution,[status(thm)],[c39, c27])).
% 0.39/0.66 cnf(c59,plain,proh(skolem0001(portal,modify_act,theater_ds))|cnt(skolem0003(portal,modify_act,theater_ds),modify_act,theater_ds),inference(resolution,[status(thm)],[c57, c29])).
% 0.39/0.66 cnf(c62,plain,proh(skolem0001(portal,modify_act,theater_ds))|~permission(skolem0003(portal,modify_act,theater_ds))|~bearer(skolem0003(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c59, c3])).
% 0.39/0.66 cnf(c89,plain,proh(skolem0001(portal,modify_act,theater_ds))|~permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c62, c37])).
% 0.39/0.66 cnf(c90,plain,proh(skolem0001(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c89, c33])).
% 0.39/0.66 cnf(c12,plain,~agent(X27)|~action(X28)|~target(X26)|aee(skolem0001(X27,X28,X26),X27)|permission(skolem0003(X27,X28,X26)),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c38,plain,~agent(X33)|~action(X32)|aee(skolem0001(X33,X32,theater_ds),X33)|permission(skolem0003(X33,X32,theater_ds)),inference(resolution,[status(thm)],[c12, c26])).
% 0.39/0.66 cnf(c40,plain,~agent(X34)|aee(skolem0001(X34,modify_act,theater_ds),X34)|permission(skolem0003(X34,modify_act,theater_ds)),inference(resolution,[status(thm)],[c38, c27])).
% 0.39/0.66 cnf(c42,plain,aee(skolem0001(portal,modify_act,theater_ds),portal)|permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c40, c29])).
% 0.39/0.66 cnf(c13,plain,~agent(X39)|~action(X40)|~target(X38)|aee(skolem0001(X39,X40,X38),X39)|bearer(skolem0003(X39,X40,X38),X39),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c44,plain,~agent(X44)|~action(X45)|aee(skolem0001(X44,X45,theater_ds),X44)|bearer(skolem0003(X44,X45,theater_ds),X44),inference(resolution,[status(thm)],[c13, c26])).
% 0.39/0.66 cnf(c48,plain,~agent(X49)|aee(skolem0001(X49,modify_act,theater_ds),X49)|bearer(skolem0003(X49,modify_act,theater_ds),X49),inference(resolution,[status(thm)],[c44, c27])).
% 0.39/0.66 cnf(c51,plain,aee(skolem0001(portal,modify_act,theater_ds),portal)|bearer(skolem0003(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c48, c29])).
% 0.39/0.66 cnf(c14,plain,~agent(X47)|~action(X48)|~target(X46)|aee(skolem0001(X47,X48,X46),X47)|cnt(skolem0003(X47,X48,X46),X48,X46),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c49,plain,~agent(X66)|~action(X65)|aee(skolem0001(X66,X65,theater_ds),X66)|cnt(skolem0003(X66,X65,theater_ds),X65,theater_ds),inference(resolution,[status(thm)],[c14, c26])).
% 0.39/0.66 cnf(c63,plain,~agent(X69)|aee(skolem0001(X69,modify_act,theater_ds),X69)|cnt(skolem0003(X69,modify_act,theater_ds),modify_act,theater_ds),inference(resolution,[status(thm)],[c49, c27])).
% 0.39/0.66 cnf(c66,plain,aee(skolem0001(portal,modify_act,theater_ds),portal)|cnt(skolem0003(portal,modify_act,theater_ds),modify_act,theater_ds),inference(resolution,[status(thm)],[c63, c29])).
% 0.39/0.66 cnf(c69,plain,aee(skolem0001(portal,modify_act,theater_ds),portal)|~permission(skolem0003(portal,modify_act,theater_ds))|~bearer(skolem0003(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c66, c3])).
% 0.39/0.66 cnf(c96,plain,aee(skolem0001(portal,modify_act,theater_ds),portal)|~permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c69, c51])).
% 0.39/0.66 cnf(c98,plain,aee(skolem0001(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c96, c42])).
% 0.39/0.66 cnf(c15,plain,~agent(X36)|~action(X37)|~target(X35)|act(skolem0001(X36,X37,X35),X37)|permission(skolem0003(X36,X37,X35)),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c43,plain,~agent(X41)|~action(X42)|act(skolem0001(X41,X42,theater_ds),X42)|permission(skolem0003(X41,X42,theater_ds)),inference(resolution,[status(thm)],[c15, c26])).
% 0.39/0.66 cnf(c45,plain,~agent(X43)|act(skolem0001(X43,modify_act,theater_ds),modify_act)|permission(skolem0003(X43,modify_act,theater_ds)),inference(resolution,[status(thm)],[c43, c27])).
% 0.39/0.66 cnf(c47,plain,act(skolem0001(portal,modify_act,theater_ds),modify_act)|permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c45, c29])).
% 0.39/0.66 cnf(c16,plain,~agent(X51)|~action(X52)|~target(X50)|act(skolem0001(X51,X52,X50),X52)|bearer(skolem0003(X51,X52,X50),X51),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c52,plain,~agent(X53)|~action(X54)|act(skolem0001(X53,X54,theater_ds),X54)|bearer(skolem0003(X53,X54,theater_ds),X53),inference(resolution,[status(thm)],[c16, c26])).
% 0.39/0.66 cnf(c53,plain,~agent(X58)|act(skolem0001(X58,modify_act,theater_ds),modify_act)|bearer(skolem0003(X58,modify_act,theater_ds),X58),inference(resolution,[status(thm)],[c52, c27])).
% 0.39/0.66 cnf(c56,plain,act(skolem0001(portal,modify_act,theater_ds),modify_act)|bearer(skolem0003(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c53, c29])).
% 0.39/0.66 cnf(c17,plain,~agent(X56)|~action(X57)|~target(X55)|act(skolem0001(X56,X57,X55),X57)|cnt(skolem0003(X56,X57,X55),X57,X55),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c54,plain,~agent(X67)|~action(X68)|act(skolem0001(X67,X68,theater_ds),X68)|cnt(skolem0003(X67,X68,theater_ds),X68,theater_ds),inference(resolution,[status(thm)],[c17, c26])).
% 0.39/0.66 cnf(c64,plain,~agent(X73)|act(skolem0001(X73,modify_act,theater_ds),modify_act)|cnt(skolem0003(X73,modify_act,theater_ds),modify_act,theater_ds),inference(resolution,[status(thm)],[c54, c27])).
% 0.39/0.66 cnf(c71,plain,act(skolem0001(portal,modify_act,theater_ds),modify_act)|cnt(skolem0003(portal,modify_act,theater_ds),modify_act,theater_ds),inference(resolution,[status(thm)],[c64, c29])).
% 0.39/0.66 cnf(c73,plain,act(skolem0001(portal,modify_act,theater_ds),modify_act)|~permission(skolem0003(portal,modify_act,theater_ds))|~bearer(skolem0003(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c71, c3])).
% 0.39/0.66 cnf(c107,plain,act(skolem0001(portal,modify_act,theater_ds),modify_act)|~permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c73, c56])).
% 0.39/0.66 cnf(c111,plain,act(skolem0001(portal,modify_act,theater_ds),modify_act),inference(resolution,[status(thm)],[c107, c47])).
% 0.39/0.66 fof(no_proh_modify,axiom,(~(?[F]:(?[E]:(((proh(F)&aee(F,portal))&act(F,modify_act))&activates(E,F))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', no_proh_modify)).
% 0.39/0.66 fof(c21,plain,(![F]:(![E]:(((~proh(F)|~aee(F,portal))|~act(F,modify_act))|~activates(E,F)))),inference(fof_nnf,[status(thm)],[no_proh_modify])).
% 0.39/0.66 fof(c22,plain,(![F]:(((~proh(F)|~aee(F,portal))|~act(F,modify_act))|(![E]:~activates(E,F)))),inference(shift_quantors,[status(thm)],[c21])).
% 0.39/0.66 fof(c24,plain,(![X9]:(![X10]:(((~proh(X9)|~aee(X9,portal))|~act(X9,modify_act))|~activates(X10,X9)))),inference(shift_quantors,[status(thm)],[fof(c23,plain,(![X9]:(((~proh(X9)|~aee(X9,portal))|~act(X9,modify_act))|(![X10]:~activates(X10,X9)))),inference(variable_rename,[status(thm)],[c22])).])).
% 0.39/0.66 cnf(c25,plain,~proh(X15)|~aee(X15,portal)|~act(X15,modify_act)|~activates(X16,X15),inference(split_conjunct,[status(thm)],[c24])).
% 0.39/0.66 cnf(c18,plain,~agent(X63)|~action(X64)|~target(X62)|activates(skolem0002(X63,X64,X62),skolem0001(X63,X64,X62))|permission(skolem0003(X63,X64,X62)),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c60,plain,~agent(X78)|~action(X77)|activates(skolem0002(X78,X77,theater_ds),skolem0001(X78,X77,theater_ds))|permission(skolem0003(X78,X77,theater_ds)),inference(resolution,[status(thm)],[c18, c26])).
% 0.39/0.66 cnf(c75,plain,~agent(X79)|activates(skolem0002(X79,modify_act,theater_ds),skolem0001(X79,modify_act,theater_ds))|permission(skolem0003(X79,modify_act,theater_ds)),inference(resolution,[status(thm)],[c60, c27])).
% 0.39/0.66 cnf(c77,plain,activates(skolem0002(portal,modify_act,theater_ds),skolem0001(portal,modify_act,theater_ds))|permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c75, c29])).
% 0.39/0.66 cnf(c79,plain,permission(skolem0003(portal,modify_act,theater_ds))|~proh(skolem0001(portal,modify_act,theater_ds))|~aee(skolem0001(portal,modify_act,theater_ds),portal)|~act(skolem0001(portal,modify_act,theater_ds),modify_act),inference(resolution,[status(thm)],[c77, c25])).
% 0.39/0.66 cnf(c113,plain,permission(skolem0003(portal,modify_act,theater_ds))|~proh(skolem0001(portal,modify_act,theater_ds))|~aee(skolem0001(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c79, c111])).
% 0.39/0.66 cnf(c114,plain,permission(skolem0003(portal,modify_act,theater_ds))|~proh(skolem0001(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c113, c98])).
% 0.39/0.66 cnf(c115,plain,permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c114, c90])).
% 0.39/0.66 cnf(c19,plain,~agent(X71)|~action(X72)|~target(X70)|activates(skolem0002(X71,X72,X70),skolem0001(X71,X72,X70))|bearer(skolem0003(X71,X72,X70),X71),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c67,plain,~agent(X81)|~action(X80)|activates(skolem0002(X81,X80,theater_ds),skolem0001(X81,X80,theater_ds))|bearer(skolem0003(X81,X80,theater_ds),X81),inference(resolution,[status(thm)],[c19, c26])).
% 0.39/0.66 cnf(c80,plain,~agent(X82)|activates(skolem0002(X82,modify_act,theater_ds),skolem0001(X82,modify_act,theater_ds))|bearer(skolem0003(X82,modify_act,theater_ds),X82),inference(resolution,[status(thm)],[c67, c27])).
% 0.39/0.66 cnf(c82,plain,activates(skolem0002(portal,modify_act,theater_ds),skolem0001(portal,modify_act,theater_ds))|bearer(skolem0003(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c80, c29])).
% 0.39/0.66 cnf(c20,plain,~agent(X75)|~action(X76)|~target(X74)|activates(skolem0002(X75,X76,X74),skolem0001(X75,X76,X74))|cnt(skolem0003(X75,X76,X74),X76,X74),inference(split_conjunct,[status(thm)],[c8])).
% 0.39/0.66 cnf(c74,plain,~agent(X84)|~action(X83)|activates(skolem0002(X84,X83,theater_ds),skolem0001(X84,X83,theater_ds))|cnt(skolem0003(X84,X83,theater_ds),X83,theater_ds),inference(resolution,[status(thm)],[c20, c26])).
% 0.39/0.66 cnf(c85,plain,~agent(X85)|activates(skolem0002(X85,modify_act,theater_ds),skolem0001(X85,modify_act,theater_ds))|cnt(skolem0003(X85,modify_act,theater_ds),modify_act,theater_ds),inference(resolution,[status(thm)],[c74, c27])).
% 0.39/0.66 cnf(c101,plain,activates(skolem0002(portal,modify_act,theater_ds),skolem0001(portal,modify_act,theater_ds))|cnt(skolem0003(portal,modify_act,theater_ds),modify_act,theater_ds),inference(resolution,[status(thm)],[c85, c29])).
% 0.39/0.66 cnf(c105,plain,activates(skolem0002(portal,modify_act,theater_ds),skolem0001(portal,modify_act,theater_ds))|~permission(skolem0003(portal,modify_act,theater_ds))|~bearer(skolem0003(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c101, c3])).
% 0.39/0.66 cnf(c119,plain,activates(skolem0002(portal,modify_act,theater_ds),skolem0001(portal,modify_act,theater_ds))|~permission(skolem0003(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c105, c82])).
% 0.39/0.66 cnf(c120,plain,activates(skolem0002(portal,modify_act,theater_ds),skolem0001(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c119, c115])).
% 0.39/0.66 cnf(c121,plain,~proh(skolem0001(portal,modify_act,theater_ds))|~aee(skolem0001(portal,modify_act,theater_ds),portal)|~act(skolem0001(portal,modify_act,theater_ds),modify_act),inference(resolution,[status(thm)],[c120, c25])).
% 0.39/0.66 cnf(c123,plain,~proh(skolem0001(portal,modify_act,theater_ds))|~aee(skolem0001(portal,modify_act,theater_ds),portal),inference(resolution,[status(thm)],[c121, c111])).
% 0.39/0.66 cnf(c124,plain,~proh(skolem0001(portal,modify_act,theater_ds)),inference(resolution,[status(thm)],[c123, c98])).
% 0.39/0.66 cnf(c125,plain,$false,inference(resolution,[status(thm)],[c124, c90])).
% 0.39/0.66 % SZS output end CNFRefutation
% 0.39/0.66
% 0.39/0.66 % Initial clauses : 18
% 0.39/0.66 % Processed clauses : 94
% 0.39/0.66 % Factors computed : 0
% 0.39/0.66 % Resolvents computed: 96
% 0.39/0.66 % Tautologies deleted: 0
% 0.39/0.66 % Forward subsumed : 11
% 0.39/0.66 % Backward subsumed : 28
% 0.39/0.66 % -------- CPU Time ---------
% 0.39/0.66 % User time : 0.262 s
% 0.39/0.66 % System time : 0.024 s
% 0.39/0.66 % Total time : 0.286 s
%------------------------------------------------------------------------------