%------------------------------------------------------------------------------
% File : LisaTT---0.9.1
% Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n031.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 6.50s 2.23s
% Output : Proof 6.95s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(ax_proh_relator_conduct,axiom,
! [F,X,Y,A,T,E] :
( ( proh(F)
& aee(F,X)
& aer(F,Y)
& act(F,A)
& tgt(F,T)
& activates(E,F) )
=> ? [Rho,D,C] :
( founds(E,Rho,F)
& duty(D)
& bearer(D,X)
& cnt(D,rfr(A),T)
& part_of(D,Rho)
& right(C)
& bearer(C,Y)
& cnt(C,rfr(A),T)
& part_of(C,Rho) ) ) ).
fof(ax_B1,axiom,
! [F,X,A,T] :
( ( proh(F)
& has_rem(F)
& act(F,A)
& tgt(F,T)
& aee(F,X)
& does(X,A,T) )
=> ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) ) ).
fof(action_distrib,axiom,
action(distrib) ).
fof(proh_f1,axiom,
proh(f1) ).
fof(act_e1_f1,axiom,
activates(e1,f1) ).
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) ) ) ).
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) ) ).
fof(marketplace_does,axiom,
does(marketplace,distrib,concert_ds) ).
fof(agent_philharmonie,axiom,
agent(philharmonie) ).
fof(event_e1,axiom,
event(e1) ).
fof(ax_A1,axiom,
! [X,A,T,Q] :
( norm_state_change(X,A,T,Q)
=> ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) ) ).
fof(aer_f1,axiom,
aer(f1,philharmonie) ).
fof(rule_f1,axiom,
rule(f1) ).
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) ) ).
fof(ax_A2,axiom,
! [E] :
( inst_event(E)
=> ? [Y] : competent_for(Y,E) ) ).
fof(act_f1,axiom,
act(f1,distrib) ).
fof(aee_f1,axiom,
aee(f1,marketplace) ).
fof(target_concert,axiom,
target(concert_ds) ).
fof(agent_marketplace,axiom,
agent(marketplace) ).
fof(tgt_f1,axiom,
tgt(f1,concert_ds) ).
fof(ax_A3,axiom,
! [Y,E] :
( competent_for(Y,E)
=> ? [Pw,S,X] :
( power(Pw)
& bearer(Pw,Y)
& about_event(Pw,E)
& subjection(S)
& bearer(S,X)
& about_event(S,E) ) ) ).
fof(rem_f1,axiom,
has_rem(f1) ).
fof(s0,plain,
( [ activates(e1,f1),aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
( ~ has_rem(f1)
| ~ aer(f1,philharmonie)
| ~ tgt(f1,concert_ds)
| ~ activates(e1,f1)
| ~ act(f1,distrib)
| ~ aee(f1,marketplace)
| ~ proh(f1) ),
act(f1,distrib),proh(f1) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s1,plain,
( [ ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
? [RhoR,Pw,S] :
( founds_rem(e1,RhoR,f1)
& bearer(Pw,philharmonie)
& part_of(Pw,RhoR)
& bearer(S,marketplace)
& part_of(S,RhoR)
& cnt(S,decl(distrib),concert_ds)
& subjection(S)
& cnt(Pw,decl(distrib),concert_ds)
& power(Pw) ) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s2,plain,
( [ activates(e1,f1),aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
( ~ has_rem(f1)
| ~ aer(f1,philharmonie)
| ~ tgt(f1,concert_ds)
| ~ activates(e1,f1)
| ~ act(f1,distrib)
| ~ aee(f1,marketplace)
| ~ proh(f1)
| ? [RhoR,Pw,S] :
( founds_rem(e1,RhoR,f1)
& bearer(Pw,philharmonie)
& part_of(Pw,RhoR)
& bearer(S,marketplace)
& part_of(S,RhoR)
& cnt(S,decl(distrib),concert_ds)
& subjection(S)
& cnt(Pw,decl(distrib),concert_ds)
& power(Pw) ) ),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
act(f1,distrib),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
proh(f1) ]
--> [ ] ),
inference(left_or,[status(thm)],[s0,s1]) ).
fof(s3,plain,
( [ activates(e1,f1),aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
act(f1,distrib),
! [E] :
( ~ has_rem(f1)
| ~ aer(f1,philharmonie)
| ~ tgt(f1,concert_ds)
| ~ activates(E,f1)
| ~ act(f1,distrib)
| ~ aee(f1,marketplace)
| ~ proh(f1)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,f1)
& bearer(Pw,philharmonie)
& part_of(Pw,RhoR)
& bearer(S,marketplace)
& part_of(S,RhoR)
& cnt(S,decl(distrib),concert_ds)
& subjection(S)
& cnt(Pw,decl(distrib),concert_ds)
& power(Pw) ) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
proh(f1) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s2]) ).
fof(s4,plain,
( [ activates(e1,f1),
! [T,E] :
( ~ has_rem(f1)
| ~ aer(f1,philharmonie)
| ~ tgt(f1,T)
| ~ activates(E,f1)
| ~ act(f1,distrib)
| ~ aee(f1,marketplace)
| ~ proh(f1)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,f1)
& bearer(Pw,philharmonie)
& part_of(Pw,RhoR)
& bearer(S,marketplace)
& part_of(S,RhoR)
& cnt(S,decl(distrib),T)
& subjection(S)
& cnt(Pw,decl(distrib),T)
& power(Pw) ) ),
aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
act(f1,distrib),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
proh(f1) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s3]) ).
fof(s5,plain,
( [ activates(e1,f1),aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
act(f1,distrib),proh(f1),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
! [A,T,E] :
( ~ has_rem(f1)
| ~ aer(f1,philharmonie)
| ~ tgt(f1,T)
| ~ activates(E,f1)
| ~ act(f1,A)
| ~ aee(f1,marketplace)
| ~ proh(f1)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,f1)
& bearer(Pw,philharmonie)
& part_of(Pw,RhoR)
& bearer(S,marketplace)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s4]) ).
fof(s6,plain,
( [ activates(e1,f1),
! [Y,A,T,E] :
( ~ has_rem(f1)
| ~ aer(f1,Y)
| ~ tgt(f1,T)
| ~ activates(E,f1)
| ~ act(f1,A)
| ~ aee(f1,marketplace)
| ~ proh(f1)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,f1)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,marketplace)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) ),
aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
act(f1,distrib),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
proh(f1) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s5]) ).
fof(s7,plain,
( [ activates(e1,f1),aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
proh(f1),act(f1,distrib),
! [X,Y,A,T,E] :
( ~ has_rem(f1)
| ~ aer(f1,Y)
| ~ tgt(f1,T)
| ~ activates(E,f1)
| ~ act(f1,A)
| ~ aee(f1,X)
| ~ proh(f1)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,f1)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s6]) ).
fof(s8,plain,
( [ activates(e1,f1),aee(f1,marketplace),tgt(f1,concert_ds),aer(f1,philharmonie),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
act(f1,distrib),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
proh(f1),
! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) ),
has_rem(f1) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s7]) ).
fof(s9,plain,
( [ activates(e1,f1),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
proh(f1),aee(f1,marketplace),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s8]) ).
fof(s10,plain,
( [ activates(e1,f1),aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),aer(f1,philharmonie),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) ) ),
proh(f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s9]) ).
fof(s11,plain,
( [ activates(e1,f1),tgt(f1,concert_ds),has_rem(f1),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
proh(f1),aee(f1,marketplace),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s10]) ).
fof(s12,plain,
( [ activates(e1,f1),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1) ),
aee(f1,marketplace),tgt(f1,concert_ds),has_rem(f1),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s11]) ).
fof(s13,plain,
( [ tgt(f1,concert_ds),has_rem(f1),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
aee(f1,marketplace),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s12]) ).
fof(s14,plain,
( [ aee(f1,marketplace),tgt(f1,concert_ds),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) ) ),
has_rem(f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s13]) ).
fof(s15,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds) ),
aee(f1,marketplace),has_rem(f1),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s14]) ).
fof(s16,plain,
( [ has_rem(f1),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace) ),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s15]) ).
fof(s17,plain,
( [ has_rem(f1),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s16]) ).
fof(s18,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1) ),
has_rem(f1),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s17]) ).
fof(s19,plain,
( [ ! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s18]) ).
fof(s20,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie) ),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s19]) ).
fof(s21,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds) ),
! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s20]) ).
fof(s22,plain,
( [ ! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s21]) ).
fof(s23,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) ) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s22]) ).
fof(s24,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) )
& target(concert_ds) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s23]) ).
fof(s25,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) )
& target(concert_ds)
& action(distrib) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s24]) ).
fof(s26,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) )
& target(concert_ds)
& action(distrib)
& agent(marketplace) ),
! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s25]) ).
fof(s27,plain,
( [ ! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ),
( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) )
& target(concert_ds)
& action(distrib)
& agent(marketplace)
& ! [E] :
( ~ inst_event(E)
| ? [Y] : competent_for(Y,E) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s26]) ).
fof(s28,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) )
& target(concert_ds)
& action(distrib)
& agent(marketplace)
& ! [E] :
( ~ inst_event(E)
| ? [Y] : competent_for(Y,E) )
& ! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s27]) ).
fof(s29,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) )
& target(concert_ds)
& action(distrib)
& agent(marketplace)
& ! [E] :
( ~ inst_event(E)
| ? [Y] : competent_for(Y,E) )
& ! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) )
& ! [Y,E] :
( ~ competent_for(Y,E)
| ? [Pw,S,X] :
( power(Pw)
& about_event(Pw,E)
& bearer(S,X)
& about_event(S,E)
& subjection(S)
& bearer(Pw,Y) ) ) ),
! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s28]) ).
fof(s30,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) )
& target(concert_ds)
& action(distrib)
& agent(marketplace)
& ! [E] :
( ~ inst_event(E)
| ? [Y] : competent_for(Y,E) )
& ! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) )
& ! [Y,E] :
( ~ competent_for(Y,E)
| ? [Pw,S,X] :
( power(Pw)
& about_event(Pw,E)
& bearer(S,X)
& about_event(S,E)
& subjection(S)
& bearer(Pw,Y) ) )
& ! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s29]) ).
fof(s31,plain,
( [ ( ! [F,X,Y,A,T,E] :
( ~ has_rem(F)
| ~ aer(F,Y)
| ~ tgt(F,T)
| ~ activates(E,F)
| ~ act(F,A)
| ~ aee(F,X)
| ~ proh(F)
| ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& bearer(Pw,Y)
& part_of(Pw,RhoR)
& bearer(S,X)
& part_of(S,RhoR)
& cnt(S,decl(A),T)
& subjection(S)
& cnt(Pw,decl(A),T)
& power(Pw) ) )
& act(f1,distrib)
& ! [X,A,T,Q] :
( ~ norm_state_change(X,A,T,Q)
| ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) )
& aer(f1,philharmonie)
& proh(f1)
& activates(e1,f1)
& ! [F,X,A,T] :
( ~ has_rem(F)
| ~ tgt(F,T)
| ~ does(X,A,T)
| ~ aee(F,X)
| ~ act(F,A)
| ~ proh(F)
| ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) )
& tgt(f1,concert_ds)
& aee(f1,marketplace)
& rule(f1)
& event(e1)
& has_rem(f1)
& agent(philharmonie)
& does(marketplace,distrib,concert_ds)
& ! [S,A,T,Rho,E,R] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) )
& ! [F,X,Y,A,T,E] :
( ~ aee(F,X)
| ~ act(F,A)
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ aer(F,Y)
| ~ proh(F)
| ? [Rho,D,C] :
( founds(E,Rho,F)
& bearer(D,X)
& part_of(D,Rho)
& bearer(C,Y)
& part_of(C,Rho)
& cnt(C,rfr(A),T)
& right(C)
& cnt(D,rfr(A),T)
& duty(D) ) )
& target(concert_ds)
& action(distrib)
& agent(marketplace)
& ! [E] :
( ~ inst_event(E)
| ? [Y] : competent_for(Y,E) )
& ! [Pw,A,T,Rho,E,R] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) )
& ! [Y,E] :
( ~ competent_for(Y,E)
| ? [Pw,S,X] :
( power(Pw)
& about_event(Pw,E)
& bearer(S,X)
& about_event(S,E)
& subjection(S)
& bearer(Pw,Y) ) )
& ! [RhoR,Pw,S] :
( ~ founds_rem(e1,RhoR,f1)
| ~ bearer(Pw,philharmonie)
| ~ part_of(Pw,RhoR)
| ~ subjection(S)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ bearer(S,marketplace)
| ~ about_event(Pw,e1)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ power(Pw) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s30]) ).
fof(s32,plain,
( [ activates(e1,f1),
! [X,A,T,Q] :
( norm_state_change(X,A,T,Q)
=> ? [E] :
( inst_event(E)
& triggers(E,X,A,T,Q) ) ),
! [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) ),
action(distrib),
! [Y,E] :
( competent_for(Y,E)
=> ? [Pw,S,X] :
( power(Pw)
& bearer(Pw,Y)
& about_event(Pw,E)
& subjection(S)
& bearer(S,X)
& about_event(S,E) ) ),
event(e1),aer(f1,philharmonie),rule(f1),
! [F,X,Y,A,T,E] :
( ( proh(F)
& aee(F,X)
& aer(F,Y)
& act(F,A)
& tgt(F,T)
& activates(E,F) )
=> ? [Rho,D,C] :
( founds(E,Rho,F)
& duty(D)
& bearer(D,X)
& cnt(D,rfr(A),T)
& part_of(D,Rho)
& right(C)
& bearer(C,Y)
& cnt(C,rfr(A),T)
& part_of(C,Rho) ) ),
act(f1,distrib),target(concert_ds),does(marketplace,distrib,concert_ds),proh(f1),
! [E] :
( inst_event(E)
=> ? [Y] : competent_for(Y,E) ),
agent(marketplace),aee(f1,marketplace),
! [F,X,A,T] :
( ( proh(F)
& has_rem(F)
& act(F,A)
& tgt(F,T)
& aee(F,X)
& does(X,A,T) )
=> ? [B] :
( rem_act(F,B)
& norm_state_change(X,B,T,duty_rem) ) ),
tgt(f1,concert_ds),
! [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) ),
! [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) ) ),
agent(philharmonie),has_rem(f1) ]
--> [ ? [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(restate,[status(thm)],[s31]) ).
fof(final,theorem,
? [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(big_cut,[status(thm)],[ax_proh_relator_conduct,ax_proh_relator_remedy,ax_A1,ax_A2,ax_A3,ax_B1,ax_B2,ax_B3,agent_marketplace,agent_philharmonie,action_distrib,target_concert,rule_f1,event_e1,proh_f1,rem_f1,aee_f1,aer_f1,act_f1,tgt_f1,act_e1_f1,marketplace_does]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n031.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue Apr 28 19:32:47 EDT 2026
% 0.15/0.33 % CPUTime :
% 6.50/2.23 % SZS status Theorem
% 6.95/2.30 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------