%------------------------------------------------------------------------------
% File : LisaTT---0.9.1
% Problem : MGT117+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 : n007.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:07 PM UTC 2026
% Result : Theorem 3.26s 1.54s
% Output : Proof 3.26s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(ax_perm_relator_strong,axiom,
! [P,X,Y,A,T,E] :
( ( perm(P)
& strong(P)
& aee(P,X)
& aer(P,Y)
& act(P,A)
& tgt(P,T)
& activates(E,P) )
=> ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& immunity(Im)
& bearer(Im,X)
& cnt(Im,A,T)
& part_of(Im,RhoI)
& disability(Db)
& bearer(Db,Y)
& cnt(Db,A,T)
& part_of(Db,RhoI) ) ) ).
fof(rule_p1,axiom,
rule(p1) ).
fof(aer_p1,axiom,
aer(p1,museen) ).
fof(agent_bibliothek,axiom,
agent(bibliothek) ).
fof(event_e1,axiom,
event(e1) ).
fof(aee_p1,axiom,
aee(p1,bibliothek) ).
fof(act_e1_p1,axiom,
activates(e1,p1) ).
fof(agent_museen,axiom,
agent(museen) ).
fof(tgt_p1,axiom,
tgt(p1,museum_api) ).
fof(perm_p1,axiom,
perm(p1) ).
fof(action_read,axiom,
action(read) ).
fof(act_p1,axiom,
act(p1,read) ).
fof(strong_p1,axiom,
strong(p1) ).
fof(target_museum,axiom,
target(museum_api) ).
fof(s0,plain,
( [ aer(p1,museen),perm(p1),activates(e1,p1),act(p1,read),tgt(p1,museum_api),aee(p1,bibliothek),strong(p1),
( ~ strong(p1)
| ~ aer(p1,museen)
| ~ tgt(p1,museum_api)
| ~ activates(e1,p1)
| ~ act(p1,read)
| ~ aee(p1,bibliothek)
| ~ perm(p1) ) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s1,plain,
( [ ? [RhoI,Im,Db] :
( founds_imm(e1,RhoI,p1)
& bearer(Im,bibliothek)
& part_of(Im,RhoI)
& bearer(Db,museen)
& part_of(Db,RhoI)
& cnt(Db,read,museum_api)
& disability(Db)
& cnt(Im,read,museum_api)
& immunity(Im) ),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s2,plain,
( [ aer(p1,museen),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),tgt(p1,museum_api),aee(p1,bibliothek),
( ~ strong(p1)
| ~ aer(p1,museen)
| ~ tgt(p1,museum_api)
| ~ activates(e1,p1)
| ~ act(p1,read)
| ~ aee(p1,bibliothek)
| ~ perm(p1)
| ? [RhoI,Im,Db] :
( founds_imm(e1,RhoI,p1)
& bearer(Im,bibliothek)
& part_of(Im,RhoI)
& bearer(Db,museen)
& part_of(Db,RhoI)
& cnt(Db,read,museum_api)
& disability(Db)
& cnt(Im,read,museum_api)
& immunity(Im) ) ),
perm(p1) ]
--> [ ] ),
inference(left_or,[status(thm)],[s0,s1]) ).
fof(s3,plain,
( [ aer(p1,museen),perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),
! [E] :
( ~ strong(p1)
| ~ aer(p1,museen)
| ~ tgt(p1,museum_api)
| ~ activates(E,p1)
| ~ act(p1,read)
| ~ aee(p1,bibliothek)
| ~ perm(p1)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,p1)
& bearer(Im,bibliothek)
& part_of(Im,RhoI)
& bearer(Db,museen)
& part_of(Db,RhoI)
& cnt(Db,read,museum_api)
& disability(Db)
& cnt(Im,read,museum_api)
& immunity(Im) ) ),
strong(p1),tgt(p1,museum_api),aee(p1,bibliothek) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s2]) ).
fof(s4,plain,
( [ aer(p1,museen),perm(p1),
! [T,E] :
( ~ strong(p1)
| ~ aer(p1,museen)
| ~ tgt(p1,T)
| ~ activates(E,p1)
| ~ act(p1,read)
| ~ aee(p1,bibliothek)
| ~ perm(p1)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,p1)
& bearer(Im,bibliothek)
& part_of(Im,RhoI)
& bearer(Db,museen)
& part_of(Db,RhoI)
& cnt(Db,read,T)
& disability(Db)
& cnt(Im,read,T)
& immunity(Im) ) ),
activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),tgt(p1,museum_api),aee(p1,bibliothek) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s3]) ).
fof(s5,plain,
( [ aer(p1,museen),perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),tgt(p1,museum_api),aee(p1,bibliothek),
! [A,T,E] :
( ~ strong(p1)
| ~ aer(p1,museen)
| ~ tgt(p1,T)
| ~ activates(E,p1)
| ~ act(p1,A)
| ~ aee(p1,bibliothek)
| ~ perm(p1)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,p1)
& bearer(Im,bibliothek)
& part_of(Im,RhoI)
& bearer(Db,museen)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s4]) ).
fof(s6,plain,
( [ aer(p1,museen),perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),aee(p1,bibliothek),
! [Y,A,T,E] :
( ~ strong(p1)
| ~ aer(p1,Y)
| ~ tgt(p1,T)
| ~ activates(E,p1)
| ~ act(p1,A)
| ~ aee(p1,bibliothek)
| ~ perm(p1)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,p1)
& bearer(Im,bibliothek)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ),
tgt(p1,museum_api) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s5]) ).
fof(s7,plain,
( [ aer(p1,museen),
! [X,Y,A,T,E] :
( ~ strong(p1)
| ~ aer(p1,Y)
| ~ tgt(p1,T)
| ~ activates(E,p1)
| ~ act(p1,A)
| ~ aee(p1,X)
| ~ perm(p1)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,p1)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ),
perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),tgt(p1,museum_api),aee(p1,bibliothek) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s6]) ).
fof(s8,plain,
( [ aer(p1,museen),
! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ),
perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),tgt(p1,museum_api),aee(p1,bibliothek) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s7]) ).
fof(s9,plain,
( [ aer(p1,museen),
! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ),
perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),
( tgt(p1,museum_api)
& aee(p1,bibliothek) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s8]) ).
fof(s10,plain,
( [ aer(p1,museen),
! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ),
perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s9]) ).
fof(s11,plain,
( [ perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1),
! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s10]) ).
fof(s12,plain,
( [ ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ),
perm(p1),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek) ),
activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),strong(p1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s11]) ).
fof(s13,plain,
( [ ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ),
perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s12]) ).
fof(s14,plain,
( [ perm(p1),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) ) ),
activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
act(p1,read) ]
--> [ ] ),
inference(weakening,[status(thm)],[s13]) ).
fof(s15,plain,
( [ ( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read) ),
perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s14]) ).
fof(s16,plain,
( [ perm(p1),activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read)
& event(e1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s15]) ).
fof(s17,plain,
( [ perm(p1),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read)
& event(e1)
& rule(p1) ),
activates(e1,p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s16]) ).
fof(s18,plain,
( [ perm(p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read)
& event(e1)
& rule(p1)
& activates(e1,p1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s17]) ).
fof(s19,plain,
( [ perm(p1),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read)
& event(e1)
& rule(p1)
& activates(e1,p1)
& action(read) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s18]) ).
fof(s20,plain,
( [ ! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ),
( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read)
& event(e1)
& rule(p1)
& activates(e1,p1)
& action(read)
& perm(p1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s19]) ).
fof(s21,plain,
( [ ( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read)
& event(e1)
& rule(p1)
& activates(e1,p1)
& action(read)
& perm(p1)
& agent(museen) ),
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s20]) ).
fof(s22,plain,
( [ ( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read)
& event(e1)
& rule(p1)
& activates(e1,p1)
& action(read)
& perm(p1)
& agent(museen)
& ! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s21]) ).
fof(s23,plain,
( [ ( tgt(p1,museum_api)
& aee(p1,bibliothek)
& target(museum_api)
& aer(p1,museen)
& agent(bibliothek)
& strong(p1)
& ! [P,X,Y,A,T,E] :
( ~ strong(P)
| ~ aer(P,Y)
| ~ tgt(P,T)
| ~ activates(E,P)
| ~ act(P,A)
| ~ aee(P,X)
| ~ perm(P)
| ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& bearer(Im,X)
& part_of(Im,RhoI)
& bearer(Db,Y)
& part_of(Db,RhoI)
& cnt(Db,A,T)
& disability(Db)
& cnt(Im,A,T)
& immunity(Im) ) )
& act(p1,read)
& event(e1)
& rule(p1)
& activates(e1,p1)
& action(read)
& perm(p1)
& agent(museen)
& ! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ bearer(Db,museen)
| ~ part_of(Db,RhoI)
| ~ cnt(Db,read,museum_api)
| ~ disability(Db) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s22]) ).
fof(s24,plain,
( [ aer(p1,museen),agent(museen),perm(p1),agent(bibliothek),rule(p1),act(p1,read),strong(p1),action(read),target(museum_api),aee(p1,bibliothek),event(e1),activates(e1,p1),
! [P,X,Y,A,T,E] :
( ( perm(P)
& strong(P)
& aee(P,X)
& aer(P,Y)
& act(P,A)
& tgt(P,T)
& activates(E,P) )
=> ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& immunity(Im)
& bearer(Im,X)
& cnt(Im,A,T)
& part_of(Im,RhoI)
& disability(Db)
& bearer(Db,Y)
& cnt(Db,A,T)
& part_of(Db,RhoI) ) ),
tgt(p1,museum_api) ]
--> [ ? [RhoI,Db] :
( founds_imm(e1,RhoI,p1)
& disability(Db)
& bearer(Db,museen)
& cnt(Db,read,museum_api)
& part_of(Db,RhoI) ) ] ),
inference(restate,[status(thm)],[s23]) ).
fof(final,theorem,
? [RhoI,Db] :
( founds_imm(e1,RhoI,p1)
& disability(Db)
& bearer(Db,museen)
& cnt(Db,read,museum_api)
& part_of(Db,RhoI) ),
inference(big_cut,[status(thm)],[ax_perm_relator_strong,agent_bibliothek,agent_museen,action_read,target_museum,rule_p1,event_e1,perm_p1,strong_p1,aee_p1,aer_p1,act_p1,tgt_p1,act_e1_p1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.35 % Computer : n007.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Tue Apr 28 19:32:38 EDT 2026
% 0.17/0.35 % CPUTime :
% 3.26/1.54 % SZS status Theorem
% 3.26/1.58 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------