%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n016.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:16:18 AM UTC 2026
% Result : Theorem 0.22s 0.51s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 7
% Syntax : Number of formulae : 106 ( 19 unt; 1 def)
% Number of atoms : 340 ( 0 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 396 ( 162 ~; 193 |; 38 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 133 ( 13 sgn 59 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(agent_portal,axiom,
agent(portal) ).
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(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(conjecture,conjecture,
? [L] :
( permission(L)
& bearer(L,portal)
& cnt(L,modify_act,theater_ds) ) ).
fof(definition_0,definition,
! [A,L,T,X] :
( definitionFOFtoCNF_0(A,L,T,X)
<=> ( bearer(L,X)
& cnt(L,A,T)
& permission(L) ) ) ).
fof(subgoal_0,plain,
? [L] :
( permission(L)
& bearer(L,portal)
& cnt(L,modify_act,theater_ds) ),
inference(strip,[],[conjecture]) ).
fof(negate_0_0,plain,
~ ? [L] :
( permission(L)
& bearer(L,portal)
& cnt(L,modify_act,theater_ds) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [L] :
( ~ bearer(L,portal)
| ~ cnt(L,modify_act,theater_ds)
| ~ permission(L) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
! [L] :
( ~ bearer(L,portal)
| ~ cnt(L,modify_act,theater_ds)
| ~ permission(L) ),
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [A,L,T,X] :
( ~ definitionFOFtoCNF_0(A,L,T,X)
<=> ( ~ bearer(L,X)
| ~ cnt(L,A,T)
| ~ permission(L) ) ),
inference(canonicalize,[],[definition_0]) ).
fof(normalize_0_3,plain,
! [A,L,T,X] :
( ( ~ definitionFOFtoCNF_0(A,L,T,X)
| bearer(L,X) )
& ( ~ definitionFOFtoCNF_0(A,L,T,X)
| cnt(L,A,T) )
& ( ~ definitionFOFtoCNF_0(A,L,T,X)
| permission(L) )
& ( ~ bearer(L,X)
| ~ cnt(L,A,T)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,T,X) ) ),
inference(clausify,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [A,L,T,X] :
( ~ definitionFOFtoCNF_0(A,L,T,X)
| cnt(L,A,T) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
action(modify_act),
inference(canonicalize,[],[action_modify]) ).
fof(normalize_0_6,plain,
agent(portal),
inference(canonicalize,[],[agent_portal]) ).
fof(normalize_0_7,plain,
target(theater_ds),
inference(canonicalize,[],[target_theater]) ).
fof(normalize_0_8,plain,
! [A,T,X] :
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| ? [F] :
( act(F,A)
& aee(F,X)
& proh(F)
& ? [E] : activates(E,F) )
| ? [L] :
( bearer(L,X)
& cnt(L,A,T)
& permission(L) ) ),
inference(canonicalize,[],[open_world_closure]) ).
fof(normalize_0_9,plain,
! [A,T,X] :
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| ? [F] :
( act(F,A)
& aee(F,X)
& proh(F)
& ? [E] : activates(E,F) )
| ? [L] :
( bearer(L,X)
& cnt(L,A,T)
& permission(L) ) ),
inference(specialize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [A,T,X] :
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| ? [F] :
( act(F,A)
& aee(F,X)
& proh(F)
& ? [E] : activates(E,F) )
| ? [L] : definitionFOFtoCNF_0(A,L,T,X) ),
inference(simplify,[],[normalize_0_9,normalize_0_2]) ).
fof(normalize_0_11,plain,
! [A,T,X] :
( ( ~ action(A)
| ~ agent(X)
| ~ target(T)
| act(skolemFOFtoCNF_F(A,X),A)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) )
& ( ~ action(A)
| ~ agent(X)
| ~ target(T)
| activates(skolemFOFtoCNF_E(A,X),skolemFOFtoCNF_F(A,X))
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) )
& ( ~ action(A)
| ~ agent(X)
| ~ target(T)
| aee(skolemFOFtoCNF_F(A,X),X)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) )
& ( ~ action(A)
| ~ agent(X)
| ~ target(T)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X)
| proh(skolemFOFtoCNF_F(A,X)) ) ),
inference(clausify,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [A,T,X] :
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| activates(skolemFOFtoCNF_E(A,X),skolemFOFtoCNF_F(A,X))
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [F] :
( ~ act(F,modify_act)
| ~ aee(F,portal)
| ~ proh(F)
| ! [E] : ~ activates(E,F) ),
inference(canonicalize,[],[no_proh_modify]) ).
fof(normalize_0_14,plain,
! [F] :
( ~ act(F,modify_act)
| ~ aee(F,portal)
| ~ proh(F)
| ! [E] : ~ activates(E,F) ),
inference(specialize,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [E,F] :
( ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal)
| ~ proh(F) ),
inference(clausify,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
! [A,L,T,X] :
( ~ definitionFOFtoCNF_0(A,L,T,X)
| bearer(L,X) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_17,plain,
! [A,T,X] :
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| aee(skolemFOFtoCNF_F(A,X),X)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_18,plain,
! [A,L,T,X] :
( ~ definitionFOFtoCNF_0(A,L,T,X)
| permission(L) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_19,plain,
! [A,T,X] :
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| act(skolemFOFtoCNF_F(A,X),A)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_20,plain,
! [A,T,X] :
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X)
| proh(skolemFOFtoCNF_F(A,X)) ),
inference(conjunct,[],[normalize_0_11]) ).
cnf(refute_0_0,plain,
( ~ bearer(L,portal)
| ~ cnt(L,modify_act,theater_ds)
| ~ permission(L) ),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( ~ bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal)
| ~ cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds)
| ~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(subst,[],[refute_0_0:[bind(L,$fot(skolemFOFtoCNF_L(modify_act,theater_ds,portal)))]]) ).
cnf(refute_0_2,plain,
( ~ definitionFOFtoCNF_0(A,L,T,X)
| cnt(L,A,T) ),
inference(canonicalize,[],[normalize_0_4]) ).
cnf(refute_0_3,plain,
( ~ definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal)
| cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds) ),
inference(subst,[],[refute_0_2:[bind(A,$fot(modify_act)),bind(L,$fot(skolemFOFtoCNF_L(modify_act,theater_ds,portal))),bind(T,$fot(theater_ds)),bind(X,$fot(portal))]]) ).
cnf(refute_0_4,plain,
action(modify_act),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_5,plain,
agent(portal),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_6,plain,
target(theater_ds),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_7,plain,
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| activates(skolemFOFtoCNF_E(A,X),skolemFOFtoCNF_F(A,X))
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) ),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_8,plain,
( ~ action(X_44)
| ~ agent(X_46)
| ~ target(theater_ds)
| activates(skolemFOFtoCNF_E(X_44,X_46),skolemFOFtoCNF_F(X_44,X_46))
| definitionFOFtoCNF_0(X_44,skolemFOFtoCNF_L(X_44,theater_ds,X_46),theater_ds,X_46) ),
inference(subst,[],[refute_0_7:[bind(A,$fot(X_44)),bind(T,$fot(theater_ds)),bind(X,$fot(X_46))]]) ).
cnf(refute_0_9,plain,
( ~ action(X_44)
| ~ agent(X_46)
| activates(skolemFOFtoCNF_E(X_44,X_46),skolemFOFtoCNF_F(X_44,X_46))
| definitionFOFtoCNF_0(X_44,skolemFOFtoCNF_L(X_44,theater_ds,X_46),theater_ds,X_46) ),
inference(resolve,[$cnf( target(theater_ds) )],[refute_0_6,refute_0_8]) ).
cnf(refute_0_10,plain,
( ~ action(X_47)
| ~ agent(portal)
| activates(skolemFOFtoCNF_E(X_47,portal),skolemFOFtoCNF_F(X_47,portal))
| definitionFOFtoCNF_0(X_47,skolemFOFtoCNF_L(X_47,theater_ds,portal),theater_ds,portal) ),
inference(subst,[],[refute_0_9:[bind(X_44,$fot(X_47)),bind(X_46,$fot(portal))]]) ).
cnf(refute_0_11,plain,
( ~ action(X_47)
| activates(skolemFOFtoCNF_E(X_47,portal),skolemFOFtoCNF_F(X_47,portal))
| definitionFOFtoCNF_0(X_47,skolemFOFtoCNF_L(X_47,theater_ds,portal),theater_ds,portal) ),
inference(resolve,[$cnf( agent(portal) )],[refute_0_5,refute_0_10]) ).
cnf(refute_0_12,plain,
( ~ action(modify_act)
| activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal))
| definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) ),
inference(subst,[],[refute_0_11:[bind(X_47,$fot(modify_act))]]) ).
cnf(refute_0_13,plain,
( activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal))
| definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) ),
inference(resolve,[$cnf( action(modify_act) )],[refute_0_4,refute_0_12]) ).
cnf(refute_0_14,plain,
( activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal))
| cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_13,refute_0_3]) ).
cnf(refute_0_15,plain,
( ~ act(F,modify_act)
| ~ activates(E,F)
| ~ aee(F,portal)
| ~ proh(F) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_16,plain,
( ~ act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| ~ activates(E,skolemFOFtoCNF_F(modify_act,portal))
| ~ aee(skolemFOFtoCNF_F(modify_act,portal),portal)
| ~ proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(subst,[],[refute_0_15:[bind(F,$fot(skolemFOFtoCNF_F(modify_act,portal)))]]) ).
cnf(refute_0_17,plain,
( ~ definitionFOFtoCNF_0(A,L,T,X)
| bearer(L,X) ),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_18,plain,
( ~ definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal)
| bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal) ),
inference(subst,[],[refute_0_17:[bind(A,$fot(modify_act)),bind(L,$fot(skolemFOFtoCNF_L(modify_act,theater_ds,portal))),bind(T,$fot(theater_ds)),bind(X,$fot(portal))]]) ).
cnf(refute_0_19,plain,
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| aee(skolemFOFtoCNF_F(A,X),X)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) ),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_20,plain,
( ~ action(X_35)
| ~ agent(X_37)
| ~ target(theater_ds)
| aee(skolemFOFtoCNF_F(X_35,X_37),X_37)
| definitionFOFtoCNF_0(X_35,skolemFOFtoCNF_L(X_35,theater_ds,X_37),theater_ds,X_37) ),
inference(subst,[],[refute_0_19:[bind(A,$fot(X_35)),bind(T,$fot(theater_ds)),bind(X,$fot(X_37))]]) ).
cnf(refute_0_21,plain,
( ~ action(X_35)
| ~ agent(X_37)
| aee(skolemFOFtoCNF_F(X_35,X_37),X_37)
| definitionFOFtoCNF_0(X_35,skolemFOFtoCNF_L(X_35,theater_ds,X_37),theater_ds,X_37) ),
inference(resolve,[$cnf( target(theater_ds) )],[refute_0_6,refute_0_20]) ).
cnf(refute_0_22,plain,
( ~ action(X_38)
| ~ agent(portal)
| aee(skolemFOFtoCNF_F(X_38,portal),portal)
| definitionFOFtoCNF_0(X_38,skolemFOFtoCNF_L(X_38,theater_ds,portal),theater_ds,portal) ),
inference(subst,[],[refute_0_21:[bind(X_35,$fot(X_38)),bind(X_37,$fot(portal))]]) ).
cnf(refute_0_23,plain,
( ~ action(X_38)
| aee(skolemFOFtoCNF_F(X_38,portal),portal)
| definitionFOFtoCNF_0(X_38,skolemFOFtoCNF_L(X_38,theater_ds,portal),theater_ds,portal) ),
inference(resolve,[$cnf( agent(portal) )],[refute_0_5,refute_0_22]) ).
cnf(refute_0_24,plain,
( ~ action(modify_act)
| aee(skolemFOFtoCNF_F(modify_act,portal),portal)
| definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) ),
inference(subst,[],[refute_0_23:[bind(X_38,$fot(modify_act))]]) ).
cnf(refute_0_25,plain,
( aee(skolemFOFtoCNF_F(modify_act,portal),portal)
| definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) ),
inference(resolve,[$cnf( action(modify_act) )],[refute_0_4,refute_0_24]) ).
cnf(refute_0_26,plain,
( aee(skolemFOFtoCNF_F(modify_act,portal),portal)
| bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_25,refute_0_18]) ).
cnf(refute_0_27,plain,
( aee(skolemFOFtoCNF_F(modify_act,portal),portal)
| cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_25,refute_0_3]) ).
cnf(refute_0_28,plain,
( ~ bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal)
| ~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal))
| aee(skolemFOFtoCNF_F(modify_act,portal),portal) ),
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds) )],[refute_0_27,refute_0_1]) ).
cnf(refute_0_29,plain,
( ~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal))
| aee(skolemFOFtoCNF_F(modify_act,portal),portal) ),
inference(resolve,[$cnf( bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal) )],[refute_0_26,refute_0_28]) ).
cnf(refute_0_30,plain,
( ~ definitionFOFtoCNF_0(A,L,T,X)
| permission(L) ),
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_31,plain,
( ~ definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal)
| permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(subst,[],[refute_0_30:[bind(A,$fot(modify_act)),bind(L,$fot(skolemFOFtoCNF_L(modify_act,theater_ds,portal))),bind(T,$fot(theater_ds)),bind(X,$fot(portal))]]) ).
cnf(refute_0_32,plain,
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| act(skolemFOFtoCNF_F(A,X),A)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X) ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_33,plain,
( ~ action(X_27)
| ~ agent(X_29)
| ~ target(theater_ds)
| act(skolemFOFtoCNF_F(X_27,X_29),X_27)
| definitionFOFtoCNF_0(X_27,skolemFOFtoCNF_L(X_27,theater_ds,X_29),theater_ds,X_29) ),
inference(subst,[],[refute_0_32:[bind(A,$fot(X_27)),bind(T,$fot(theater_ds)),bind(X,$fot(X_29))]]) ).
cnf(refute_0_34,plain,
( ~ action(X_27)
| ~ agent(X_29)
| act(skolemFOFtoCNF_F(X_27,X_29),X_27)
| definitionFOFtoCNF_0(X_27,skolemFOFtoCNF_L(X_27,theater_ds,X_29),theater_ds,X_29) ),
inference(resolve,[$cnf( target(theater_ds) )],[refute_0_6,refute_0_33]) ).
cnf(refute_0_35,plain,
( ~ action(X_30)
| ~ agent(portal)
| act(skolemFOFtoCNF_F(X_30,portal),X_30)
| definitionFOFtoCNF_0(X_30,skolemFOFtoCNF_L(X_30,theater_ds,portal),theater_ds,portal) ),
inference(subst,[],[refute_0_34:[bind(X_27,$fot(X_30)),bind(X_29,$fot(portal))]]) ).
cnf(refute_0_36,plain,
( ~ action(X_30)
| act(skolemFOFtoCNF_F(X_30,portal),X_30)
| definitionFOFtoCNF_0(X_30,skolemFOFtoCNF_L(X_30,theater_ds,portal),theater_ds,portal) ),
inference(resolve,[$cnf( agent(portal) )],[refute_0_5,refute_0_35]) ).
cnf(refute_0_37,plain,
( ~ action(modify_act)
| act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) ),
inference(subst,[],[refute_0_36:[bind(X_30,$fot(modify_act))]]) ).
cnf(refute_0_38,plain,
( act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) ),
inference(resolve,[$cnf( action(modify_act) )],[refute_0_4,refute_0_37]) ).
cnf(refute_0_39,plain,
( act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_38,refute_0_31]) ).
cnf(refute_0_40,plain,
( aee(skolemFOFtoCNF_F(modify_act,portal),portal)
| permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_25,refute_0_31]) ).
cnf(refute_0_41,plain,
( ~ act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| ~ activates(E,skolemFOFtoCNF_F(modify_act,portal))
| ~ proh(skolemFOFtoCNF_F(modify_act,portal))
| permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(resolve,[$cnf( aee(skolemFOFtoCNF_F(modify_act,portal),portal) )],[refute_0_40,refute_0_16]) ).
cnf(refute_0_42,plain,
( ~ action(A)
| ~ agent(X)
| ~ target(T)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,T,X),T,X)
| proh(skolemFOFtoCNF_F(A,X)) ),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_43,plain,
( ~ action(X_19)
| ~ agent(X_21)
| ~ target(theater_ds)
| definitionFOFtoCNF_0(X_19,skolemFOFtoCNF_L(X_19,theater_ds,X_21),theater_ds,X_21)
| proh(skolemFOFtoCNF_F(X_19,X_21)) ),
inference(subst,[],[refute_0_42:[bind(A,$fot(X_19)),bind(T,$fot(theater_ds)),bind(X,$fot(X_21))]]) ).
cnf(refute_0_44,plain,
( ~ action(X_19)
| ~ agent(X_21)
| definitionFOFtoCNF_0(X_19,skolemFOFtoCNF_L(X_19,theater_ds,X_21),theater_ds,X_21)
| proh(skolemFOFtoCNF_F(X_19,X_21)) ),
inference(resolve,[$cnf( target(theater_ds) )],[refute_0_6,refute_0_43]) ).
cnf(refute_0_45,plain,
( ~ action(X_22)
| ~ agent(portal)
| definitionFOFtoCNF_0(X_22,skolemFOFtoCNF_L(X_22,theater_ds,portal),theater_ds,portal)
| proh(skolemFOFtoCNF_F(X_22,portal)) ),
inference(subst,[],[refute_0_44:[bind(X_19,$fot(X_22)),bind(X_21,$fot(portal))]]) ).
cnf(refute_0_46,plain,
( ~ action(X_22)
| definitionFOFtoCNF_0(X_22,skolemFOFtoCNF_L(X_22,theater_ds,portal),theater_ds,portal)
| proh(skolemFOFtoCNF_F(X_22,portal)) ),
inference(resolve,[$cnf( agent(portal) )],[refute_0_5,refute_0_45]) ).
cnf(refute_0_47,plain,
( ~ action(modify_act)
| definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal)
| proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(subst,[],[refute_0_46:[bind(X_22,$fot(modify_act))]]) ).
cnf(refute_0_48,plain,
( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal)
| proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(resolve,[$cnf( action(modify_act) )],[refute_0_4,refute_0_47]) ).
cnf(refute_0_49,plain,
( permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal))
| proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_48,refute_0_31]) ).
cnf(refute_0_50,plain,
( bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal)
| proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_48,refute_0_18]) ).
cnf(refute_0_51,plain,
( cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds)
| proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_48,refute_0_3]) ).
cnf(refute_0_52,plain,
( ~ bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal)
| ~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal))
| proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds) )],[refute_0_51,refute_0_1]) ).
cnf(refute_0_53,plain,
( ~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal))
| proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(resolve,[$cnf( bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal) )],[refute_0_50,refute_0_52]) ).
cnf(refute_0_54,plain,
proh(skolemFOFtoCNF_F(modify_act,portal)),
inference(resolve,[$cnf( permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) )],[refute_0_49,refute_0_53]) ).
cnf(refute_0_55,plain,
( ~ act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| ~ activates(E,skolemFOFtoCNF_F(modify_act,portal))
| permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(resolve,[$cnf( proh(skolemFOFtoCNF_F(modify_act,portal)) )],[refute_0_54,refute_0_41]) ).
cnf(refute_0_56,plain,
( ~ act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| ~ activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal))
| permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(subst,[],[refute_0_55:[bind(E,$fot(skolemFOFtoCNF_E(modify_act,portal)))]]) ).
cnf(refute_0_57,plain,
( activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal))
| permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_13,refute_0_31]) ).
cnf(refute_0_58,plain,
( ~ act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(resolve,[$cnf( activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal)) )],[refute_0_57,refute_0_56]) ).
cnf(refute_0_59,plain,
permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)),
inference(resolve,[$cnf( act(skolemFOFtoCNF_F(modify_act,portal),modify_act) )],[refute_0_39,refute_0_58]) ).
cnf(refute_0_60,plain,
aee(skolemFOFtoCNF_F(modify_act,portal),portal),
inference(resolve,[$cnf( permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) )],[refute_0_59,refute_0_29]) ).
cnf(refute_0_61,plain,
( ~ act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| ~ activates(E,skolemFOFtoCNF_F(modify_act,portal))
| ~ proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(resolve,[$cnf( aee(skolemFOFtoCNF_F(modify_act,portal),portal) )],[refute_0_60,refute_0_16]) ).
cnf(refute_0_62,plain,
( act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_38,refute_0_18]) ).
cnf(refute_0_63,plain,
( act(skolemFOFtoCNF_F(modify_act,portal),modify_act)
| cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_38,refute_0_3]) ).
cnf(refute_0_64,plain,
( ~ bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal)
| ~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal))
| act(skolemFOFtoCNF_F(modify_act,portal),modify_act) ),
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds) )],[refute_0_63,refute_0_1]) ).
cnf(refute_0_65,plain,
( ~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal))
| act(skolemFOFtoCNF_F(modify_act,portal),modify_act) ),
inference(resolve,[$cnf( bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal) )],[refute_0_62,refute_0_64]) ).
cnf(refute_0_66,plain,
act(skolemFOFtoCNF_F(modify_act,portal),modify_act),
inference(resolve,[$cnf( permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) )],[refute_0_59,refute_0_65]) ).
cnf(refute_0_67,plain,
( ~ activates(E,skolemFOFtoCNF_F(modify_act,portal))
| ~ proh(skolemFOFtoCNF_F(modify_act,portal)) ),
inference(resolve,[$cnf( act(skolemFOFtoCNF_F(modify_act,portal),modify_act) )],[refute_0_66,refute_0_61]) ).
cnf(refute_0_68,plain,
~ activates(E,skolemFOFtoCNF_F(modify_act,portal)),
inference(resolve,[$cnf( proh(skolemFOFtoCNF_F(modify_act,portal)) )],[refute_0_54,refute_0_67]) ).
cnf(refute_0_69,plain,
~ activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal)),
inference(subst,[],[refute_0_68:[bind(E,$fot(skolemFOFtoCNF_E(modify_act,portal)))]]) ).
cnf(refute_0_70,plain,
cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds),
inference(resolve,[$cnf( activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal)) )],[refute_0_14,refute_0_69]) ).
cnf(refute_0_71,plain,
( ~ bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal)
| ~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) ),
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_L(modify_act,theater_ds,portal),modify_act,theater_ds) )],[refute_0_70,refute_0_1]) ).
cnf(refute_0_72,plain,
( activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal))
| bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(modify_act,skolemFOFtoCNF_L(modify_act,theater_ds,portal),theater_ds,portal) )],[refute_0_13,refute_0_18]) ).
cnf(refute_0_73,plain,
bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal),
inference(resolve,[$cnf( activates(skolemFOFtoCNF_E(modify_act,portal),skolemFOFtoCNF_F(modify_act,portal)) )],[refute_0_72,refute_0_69]) ).
cnf(refute_0_74,plain,
~ permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)),
inference(resolve,[$cnf( bearer(skolemFOFtoCNF_L(modify_act,theater_ds,portal),portal) )],[refute_0_73,refute_0_71]) ).
cnf(refute_0_75,plain,
$false,
inference(resolve,[$cnf( permission(skolemFOFtoCNF_L(modify_act,theater_ds,portal)) )],[refute_0_59,refute_0_74]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.06 % Command : metis --show proof --show saturation %s
% 0.22/0.46 % Computer : n016.cluster.edu
% 0.22/0.46 % Model : x86_64 x86_64
% 0.22/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.46 % Memory : 8046.5625MB
% 0.22/0.46 % OS : Linux 6.8.0-71-generic
% 0.22/0.46 % CPULimit : 300
% 0.22/0.46 % WCLimit : 300
% 0.22/0.46 % DateTime : Mon Sep 7 14:10:17 UTC 2026
% 0.22/0.47 % CPUTime :
% 0.22/0.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.22/0.51 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.51
% 0.22/0.51 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.26/0.54
%------------------------------------------------------------------------------