%------------------------------------------------------------------------------
% File : LisaTT---0.9.1
% Problem : MGT116+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 : 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:06 PM UTC 2026
% Result : Theorem 2.06s 1.27s
% Output : Proof 2.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
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(action_a,axiom,
action(some_action) ).
fof(founds_rem1,axiom,
founds_rem(e1,rho_r,f1) ).
fof(pos_s,axiom,
position(s) ).
fof(target_t,axiom,
target(some_target) ).
fof(partof_s,axiom,
part_of(s,rho_r) ).
fof(rel_rho_r,axiom,
legal_relator(rho_r) ).
fof(subj_s,axiom,
subjection(s) ).
fof(rule_f1,axiom,
rule(f1) ).
fof(cnt_s,axiom,
cnt(s,decl(some_action),some_target) ).
fof(event_e1,axiom,
event(e1) ).
fof(s0,plain,
( [ ( ~ cnt(s,decl(some_action),some_target)
| ~ founds_rem(e1,rho_r,f1)
| ~ part_of(s,rho_r)
| ~ subjection(s) ),
part_of(s,rho_r),cnt(s,decl(some_action),some_target),subjection(s),founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s1,plain,
( [ about_event(s,e1),~ about_event(s,e1) ]
--> [ ] ),
inference(restate_true,[status(thm)],[]) ).
fof(s2,plain,
( [ ~ about_event(s,e1),cnt(s,decl(some_action),some_target),subjection(s),founds_rem(e1,rho_r,f1),part_of(s,rho_r),
( ~ cnt(s,decl(some_action),some_target)
| ~ founds_rem(e1,rho_r,f1)
| ~ part_of(s,rho_r)
| ~ subjection(s)
| about_event(s,e1) ) ]
--> [ ] ),
inference(left_or,[status(thm)],[s0,s1]) ).
fof(s3,plain,
( [ part_of(s,rho_r),
! [R] :
( ~ cnt(s,decl(some_action),some_target)
| ~ founds_rem(e1,rho_r,R)
| ~ part_of(s,rho_r)
| ~ subjection(s)
| about_event(s,e1) ),
~ about_event(s,e1),cnt(s,decl(some_action),some_target),subjection(s),founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s2]) ).
fof(s4,plain,
( [ part_of(s,rho_r),~ about_event(s,e1),
! [E,R] :
( ~ cnt(s,decl(some_action),some_target)
| ~ founds_rem(E,rho_r,R)
| ~ part_of(s,rho_r)
| ~ subjection(s)
| about_event(s,E) ),
cnt(s,decl(some_action),some_target),subjection(s),founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s3]) ).
fof(s5,plain,
( [ part_of(s,rho_r),~ about_event(s,e1),
! [Rho,E,R] :
( ~ cnt(s,decl(some_action),some_target)
| ~ founds_rem(E,Rho,R)
| ~ part_of(s,Rho)
| ~ subjection(s)
| about_event(s,E) ),
cnt(s,decl(some_action),some_target),subjection(s),founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s4]) ).
fof(s6,plain,
( [ part_of(s,rho_r),cnt(s,decl(some_action),some_target),subjection(s),founds_rem(e1,rho_r,f1),~ about_event(s,e1),
! [T,Rho,E,R] :
( ~ cnt(s,decl(some_action),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(s,Rho)
| ~ subjection(s)
| about_event(s,E) ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s5]) ).
fof(s7,plain,
( [ part_of(s,rho_r),~ about_event(s,e1),cnt(s,decl(some_action),some_target),subjection(s),founds_rem(e1,rho_r,f1),
! [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(left_forall,[status(thm)],[s6]) ).
fof(s8,plain,
( [ part_of(s,rho_r),~ about_event(s,e1),cnt(s,decl(some_action),some_target),subjection(s),
! [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) ),
founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s7]) ).
fof(s9,plain,
( [ part_of(s,rho_r),
( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target) ),
~ about_event(s,e1),subjection(s),
! [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) ),
founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s8]) ).
fof(s10,plain,
( [ part_of(s,rho_r),~ about_event(s,e1),
( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target) ),
subjection(s),
! [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) ),
founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s9]) ).
fof(s11,plain,
( [ part_of(s,rho_r),~ about_event(s,e1),
( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target)
& event(e1) ),
subjection(s),
! [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) ),
founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s10]) ).
fof(s12,plain,
( [ ~ about_event(s,e1),
( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target)
& event(e1)
& part_of(s,rho_r) ),
subjection(s),
! [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) ),
founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s11]) ).
fof(s13,plain,
( [ ( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target)
& event(e1)
& part_of(s,rho_r)
& ! [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) ) ),
~ about_event(s,e1),subjection(s),founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s12]) ).
fof(s14,plain,
( [ ~ about_event(s,e1),
( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target)
& event(e1)
& part_of(s,rho_r)
& ! [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) )
& subjection(s) ),
founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s13]) ).
fof(s15,plain,
( [ ( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target)
& event(e1)
& part_of(s,rho_r)
& ! [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) )
& subjection(s)
& rule(f1) ),
~ about_event(s,e1),founds_rem(e1,rho_r,f1) ]
--> [ ] ),
inference(weakening,[status(thm)],[s14]) ).
fof(s16,plain,
( [ ~ about_event(s,e1),
( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target)
& event(e1)
& part_of(s,rho_r)
& ! [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) )
& subjection(s)
& rule(f1)
& founds_rem(e1,rho_r,f1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s15]) ).
fof(s17,plain,
( [ ( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target)
& event(e1)
& part_of(s,rho_r)
& ! [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) )
& subjection(s)
& rule(f1)
& founds_rem(e1,rho_r,f1)
& ~ about_event(s,e1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s16]) ).
fof(s18,plain,
( [ ( legal_relator(rho_r)
& action(some_action)
& position(s)
& cnt(s,decl(some_action),some_target)
& target(some_target)
& event(e1)
& part_of(s,rho_r)
& ! [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) )
& subjection(s)
& rule(f1)
& founds_rem(e1,rho_r,f1)
& ~ about_event(s,e1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s17]) ).
fof(s19,plain,
( [ part_of(s,rho_r),
! [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) ),
position(s),event(e1),action(some_action),founds_rem(e1,rho_r,f1),legal_relator(rho_r),cnt(s,decl(some_action),some_target),target(some_target),subjection(s),rule(f1) ]
--> [ about_event(s,e1) ] ),
inference(restate,[status(thm)],[s18]) ).
fof(final,theorem,
about_event(s,e1),
inference(big_cut,[status(thm)],[ax_B3,pos_s,rel_rho_r,rule_f1,event_e1,action_a,target_t,subj_s,cnt_s,partof_s,founds_rem1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : MGT116+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.14/0.33 % Computer : n007.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue Apr 28 19:32:08 EDT 2026
% 0.14/0.33 % CPUTime :
% 2.06/1.27 % SZS status Theorem
% 2.54/1.30 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------