%------------------------------------------------------------------------------
% File : LisaTT---0.9.1
% Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 29 02:09:06 PM UTC 2026
% Result : Theorem 2.26s 1.35s
% Output : Proof 2.26s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(agent_portal,axiom,
agent(portal) ).
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) ) ) ).
fof(agent_ensemble,axiom,
agent(ensemble) ).
fof(action_modify,axiom,
action(modify_act) ).
fof(target_theater,axiom,
target(theater_ds) ).
fof(no_proh_modify,axiom,
~ ? [F,E] :
( proh(F)
& aee(F,portal)
& act(F,modify_act)
& activates(E,F) ) ).
fof(s0,plain,
( [ ( ~ action(modify_act)
| ? [F,E] :
( proh(F)
& act(F,modify_act)
& activates(E,F)
& aee(F,portal) )
| ~ target(theater_ds)
| ~ agent(portal) ),
action(modify_act),agent(portal),target(theater_ds),
! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) ) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s1,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
? [L] :
( permission(L)
& cnt(L,modify_act,theater_ds)
& bearer(L,portal) ) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s2,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
( ~ action(modify_act)
| ? [F,E] :
( proh(F)
& act(F,modify_act)
& activates(E,F)
& aee(F,portal) )
| ~ target(theater_ds)
| ~ agent(portal)
| ? [L] :
( permission(L)
& cnt(L,modify_act,theater_ds)
& bearer(L,portal) ) ),
action(modify_act),agent(portal),target(theater_ds),
! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) ) ]
--> [ ] ),
inference(left_or,[status(thm)],[s0,s1]) ).
fof(s3,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
! [T] :
( ~ action(modify_act)
| ? [F,E] :
( proh(F)
& act(F,modify_act)
& activates(E,F)
& aee(F,portal) )
| ~ target(T)
| ~ agent(portal)
| ? [L] :
( permission(L)
& cnt(L,modify_act,T)
& bearer(L,portal) ) ),
action(modify_act),agent(portal),target(theater_ds),
! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s2]) ).
fof(s4,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
action(modify_act),
! [A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,portal) )
| ~ target(T)
| ~ agent(portal)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,portal) ) ),
agent(portal),target(theater_ds),
! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s3]) ).
fof(s5,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
action(modify_act),agent(portal),
! [X,A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,X) )
| ~ target(T)
| ~ agent(X)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,X) ) ),
target(theater_ds),
! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s4]) ).
fof(s6,plain,
( [ ( ! [X,A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,X) )
| ~ target(T)
| ~ agent(X)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,X) ) )
& agent(ensemble) ),
! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
action(modify_act),agent(portal),target(theater_ds),
! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s5]) ).
fof(s7,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
action(modify_act),
( ! [X,A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,X) )
| ~ target(T)
| ~ agent(X)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,X) ) )
& agent(ensemble)
& agent(portal) ),
target(theater_ds),
! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s6]) ).
fof(s8,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
target(theater_ds),action(modify_act),
( ! [X,A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,X) )
| ~ target(T)
| ~ agent(X)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,X) ) )
& agent(ensemble)
& agent(portal)
& ! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s7]) ).
fof(s9,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
action(modify_act),
( ! [X,A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,X) )
| ~ target(T)
| ~ agent(X)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,X) ) )
& agent(ensemble)
& agent(portal)
& ! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) )
& target(theater_ds) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s8]) ).
fof(s10,plain,
( [ ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ),
( ! [X,A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,X) )
| ~ target(T)
| ~ agent(X)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,X) ) )
& agent(ensemble)
& agent(portal)
& ! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) )
& target(theater_ds)
& action(modify_act) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s9]) ).
fof(s11,plain,
( [ ( ! [X,A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,X) )
| ~ target(T)
| ~ agent(X)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,X) ) )
& agent(ensemble)
& agent(portal)
& ! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) )
& target(theater_ds)
& action(modify_act)
& ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s10]) ).
fof(s12,plain,
( [ ( ! [X,A,T] :
( ~ action(A)
| ? [F,E] :
( proh(F)
& act(F,A)
& activates(E,F)
& aee(F,X) )
| ~ target(T)
| ~ agent(X)
| ? [L] :
( permission(L)
& cnt(L,A,T)
& bearer(L,X) ) )
& agent(ensemble)
& agent(portal)
& ! [F,E] :
( ~ proh(F)
| ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal) )
& target(theater_ds)
& action(modify_act)
& ! [L] :
( ~ permission(L)
| ~ cnt(L,modify_act,theater_ds)
| ~ bearer(L,portal) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s11]) ).
fof(s13,plain,
( [ target(theater_ds),
~ ? [F,E] :
( proh(F)
& aee(F,portal)
& act(F,modify_act)
& activates(E,F) ),
agent(ensemble),action(modify_act),agent(portal),
! [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) ) ) ]
--> [ ? [L] :
( permission(L)
& bearer(L,portal)
& cnt(L,modify_act,theater_ds) ) ] ),
inference(restate,[status(thm)],[s12]) ).
fof(final,theorem,
? [L] :
( permission(L)
& bearer(L,portal)
& cnt(L,modify_act,theater_ds) ),
inference(big_cut,[status(thm)],[agent_portal,agent_ensemble,action_modify,target_theater,no_proh_modify,open_world_closure]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.35 % Computer : n004.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Tue Apr 28 19:29:31 EDT 2026
% 0.16/0.35 % CPUTime :
% 2.26/1.35 % SZS status Theorem
% 2.26/1.38 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------