%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n014.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:20:02 AM UTC 2026
% Result : Theorem 0.22s 0.53s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 12
% Syntax : Number of clauses : 52 ( 15 unt; 7 nHn; 52 RR)
% Number of literals : 137 ( 0 equ; 95 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
agent(portal),
file('MGT111+1.p',unknown),
[] ).
cnf(3,axiom,
action(modify_act),
file('MGT111+1.p',unknown),
[] ).
cnf(4,axiom,
target(theater_ds),
file('MGT111+1.p',unknown),
[] ).
cnf(5,axiom,
( ~ skP0(u,v,w)
| permission(skf3(x,y,z)) ),
file('MGT111+1.p',unknown),
[] ).
cnf(6,axiom,
( ~ skP0(u,v,w)
| bearer(skf3(w,x,y),w) ),
file('MGT111+1.p',unknown),
[] ).
cnf(7,axiom,
( ~ permission(u)
| ~ bearer(u,portal)
| ~ cnt(u,modify_act,theater_ds) ),
file('MGT111+1.p',unknown),
[] ).
cnf(8,axiom,
( ~ skP0(u,v,w)
| cnt(skf3(w,u,v),v,u) ),
file('MGT111+1.p',unknown),
[] ).
cnf(9,axiom,
( ~ proh(u)
| ~ activates(v,u)
| ~ aee(u,portal)
| ~ act(u,modify_act) ),
file('MGT111+1.p',unknown),
[] ).
cnf(10,axiom,
( ~ agent(u)
| ~ action(v)
| ~ target(w)
| proh(skf4(x,y))
| skP0(w,v,u) ),
file('MGT111+1.p',unknown),
[] ).
cnf(11,axiom,
( ~ agent(u)
| ~ action(v)
| ~ target(w)
| act(skf4(v,x),v)
| skP0(w,v,u) ),
file('MGT111+1.p',unknown),
[] ).
cnf(12,axiom,
( ~ agent(u)
| ~ action(v)
| ~ target(w)
| aee(skf4(v,u),u)
| skP0(w,v,u) ),
file('MGT111+1.p',unknown),
[] ).
cnf(13,axiom,
( ~ agent(u)
| ~ action(v)
| ~ target(w)
| activates(skf5(x,y),skf4(y,x))
| skP0(w,v,u) ),
file('MGT111+1.p',unknown),
[] ).
cnf(20,plain,
( ~ agent(u)
| ~ action(v)
| ~ target(w)
| skP0(w,v,u) ),
inference(spt,[spt(split,[position(s1)])],[10]),
[iquote('1:Spt:10.0,10.1,10.2,10.4')] ).
cnf(22,plain,
( ~ agent(u)
| ~ action(v)
| ~ target(w)
| bearer(skf3(u,x,y),u) ),
inference(res,[status(thm),theory(equality)],[20,6]),
[iquote('1:Res:20.3,6.0')] ).
cnf(23,plain,
( ~ permission(skf3(u,theater_ds,modify_act))
| ~ skP0(theater_ds,modify_act,u)
| ~ bearer(skf3(u,theater_ds,modify_act),portal) ),
inference(res,[status(thm),theory(equality)],[8,7]),
[iquote('0:Res:8.1,7.2')] ).
cnf(24,plain,
( ~ skP0(theater_ds,modify_act,u)
| ~ bearer(skf3(u,theater_ds,modify_act),portal) ),
inference(mrr,[status(thm)],[23,5]),
[iquote('0:MRR:23.0,5.1')] ).
cnf(29,plain,
( ~ agent(u)
| ~ target(v)
| bearer(skf3(u,w,x),u) ),
inference(ems,[status(thm)],[22,3]),
[iquote('1:EmS:22.1,3.0')] ).
cnf(30,plain,
( ~ agent(u)
| bearer(skf3(u,v,w),u) ),
inference(ems,[status(thm)],[29,4]),
[iquote('1:EmS:29.1,4.0')] ).
cnf(31,plain,
( ~ agent(portal)
| ~ skP0(theater_ds,modify_act,portal) ),
inference(res,[status(thm),theory(equality)],[30,24]),
[iquote('1:Res:30.1,24.1')] ).
cnf(32,plain,
~ skP0(theater_ds,modify_act,portal),
inference(ssi,[status(thm)],[31,1]),
[iquote('1:SSi:31.0,1.0')] ).
cnf(33,plain,
( ~ agent(portal)
| ~ action(modify_act)
| ~ target(theater_ds) ),
inference(res,[status(thm),theory(equality)],[20,32]),
[iquote('1:Res:20.3,32.0')] ).
cnf(34,plain,
$false,
inference(ssi,[status(thm)],[33,4,3,1]),
[iquote('1:SSi:33.2,33.1,33.0,4.0,3.0,1.0')] ).
cnf(35,plain,
proh(skf4(u,v)),
inference(spt,[spt(split,[position(s2)])],[10]),
[iquote('1:Spt:34.0,10.3')] ).
cnf(36,plain,
( ~ agent(u)
| ~ action(v)
| ~ target(w)
| skP0(w,v,u) ),
inference(spt,[spt(split,[position(s2s1)])],[13]),
[iquote('2:Spt:13.0,13.1,13.2,13.4')] ).
cnf(37,plain,
( ~ agent(u)
| ~ action(v)
| ~ target(w)
| bearer(skf3(u,x,y),u) ),
inference(res,[status(thm),theory(equality)],[36,6]),
[iquote('2:Res:36.3,6.0')] ).
cnf(43,plain,
( ~ agent(u)
| ~ target(v)
| bearer(skf3(u,w,x),u) ),
inference(ems,[status(thm)],[37,3]),
[iquote('2:EmS:37.1,3.0')] ).
cnf(44,plain,
( ~ agent(u)
| bearer(skf3(u,v,w),u) ),
inference(ems,[status(thm)],[43,4]),
[iquote('2:EmS:43.1,4.0')] ).
cnf(45,plain,
( ~ agent(portal)
| ~ skP0(theater_ds,modify_act,portal) ),
inference(res,[status(thm),theory(equality)],[44,24]),
[iquote('2:Res:44.1,24.1')] ).
cnf(46,plain,
~ skP0(theater_ds,modify_act,portal),
inference(ssi,[status(thm)],[45,1]),
[iquote('2:SSi:45.0,1.0')] ).
cnf(47,plain,
( ~ agent(portal)
| ~ action(modify_act)
| ~ target(theater_ds) ),
inference(res,[status(thm),theory(equality)],[36,46]),
[iquote('2:Res:36.3,46.0')] ).
cnf(48,plain,
$false,
inference(ssi,[status(thm)],[47,4,3,1]),
[iquote('2:SSi:47.2,47.1,47.0,4.0,3.0,1.0')] ).
cnf(49,plain,
activates(skf5(u,v),skf4(v,u)),
inference(spt,[spt(split,[position(s2s2)])],[13]),
[iquote('2:Spt:48.0,13.3')] ).
cnf(50,plain,
( ~ proh(skf4(u,v))
| ~ aee(skf4(u,v),portal)
| ~ act(skf4(u,v),modify_act) ),
inference(res,[status(thm),theory(equality)],[49,9]),
[iquote('2:Res:49.0,9.1')] ).
cnf(51,plain,
( ~ aee(skf4(u,v),portal)
| ~ act(skf4(u,v),modify_act) ),
inference(ssi,[status(thm)],[50,35]),
[iquote('2:SSi:50.0,35.0')] ).
cnf(52,plain,
( ~ agent(portal)
| ~ action(u)
| ~ target(v)
| ~ act(skf4(u,portal),modify_act)
| skP0(v,u,portal) ),
inference(res,[status(thm),theory(equality)],[12,51]),
[iquote('2:Res:12.3,51.0')] ).
cnf(55,plain,
( ~ action(u)
| ~ target(v)
| ~ act(skf4(u,portal),modify_act)
| skP0(v,u,portal) ),
inference(ssi,[status(thm)],[52,1]),
[iquote('2:SSi:52.0,1.0')] ).
cnf(56,plain,
( ~ agent(u)
| ~ action(modify_act)
| ~ target(v)
| ~ action(modify_act)
| ~ target(w)
| skP0(v,modify_act,u)
| skP0(w,modify_act,portal) ),
inference(res,[status(thm),theory(equality)],[11,55]),
[iquote('2:Res:11.3,55.2')] ).
cnf(59,plain,
( ~ agent(u)
| ~ target(v)
| ~ action(modify_act)
| ~ target(w)
| skP0(v,modify_act,u)
| skP0(w,modify_act,portal) ),
inference(obv,[status(thm),theory(equality)],[56]),
[iquote('2:Obv:56.1')] ).
cnf(60,plain,
( ~ agent(u)
| ~ target(v)
| ~ target(w)
| skP0(v,modify_act,u)
| skP0(w,modify_act,portal) ),
inference(ssi,[status(thm)],[59,3]),
[iquote('2:SSi:59.2,3.0')] ).
cnf(61,plain,
( ~ agent(u)
| ~ target(v)
| skP0(v,modify_act,u) ),
inference(spt,[spt(split,[position(s2s2s1)])],[60]),
[iquote('3:Spt:60.0,60.1,60.3')] ).
cnf(63,plain,
( ~ agent(u)
| ~ target(v)
| bearer(skf3(u,w,x),u) ),
inference(res,[status(thm),theory(equality)],[61,6]),
[iquote('3:Res:61.2,6.0')] ).
cnf(66,plain,
( ~ agent(u)
| bearer(skf3(u,v,w),u) ),
inference(ems,[status(thm)],[63,4]),
[iquote('3:EmS:63.1,4.0')] ).
cnf(68,plain,
( ~ agent(portal)
| ~ skP0(theater_ds,modify_act,portal) ),
inference(res,[status(thm),theory(equality)],[66,24]),
[iquote('3:Res:66.1,24.1')] ).
cnf(69,plain,
~ skP0(theater_ds,modify_act,portal),
inference(ssi,[status(thm)],[68,1]),
[iquote('3:SSi:68.0,1.0')] ).
cnf(70,plain,
( ~ agent(portal)
| ~ target(theater_ds) ),
inference(res,[status(thm),theory(equality)],[61,69]),
[iquote('3:Res:61.2,69.0')] ).
cnf(71,plain,
$false,
inference(ssi,[status(thm)],[70,4,1]),
[iquote('3:SSi:70.1,70.0,4.0,1.0')] ).
cnf(72,plain,
( ~ target(u)
| skP0(u,modify_act,portal) ),
inference(spt,[spt(split,[position(s2s2s2)])],[60]),
[iquote('3:Spt:71.0,60.2,60.4')] ).
cnf(73,plain,
( ~ target(u)
| bearer(skf3(portal,v,w),portal) ),
inference(res,[status(thm),theory(equality)],[72,6]),
[iquote('3:Res:72.1,6.0')] ).
cnf(78,plain,
bearer(skf3(portal,u,v),portal),
inference(ems,[status(thm)],[73,4]),
[iquote('3:EmS:73.0,4.0')] ).
cnf(79,plain,
~ skP0(theater_ds,modify_act,portal),
inference(res,[status(thm),theory(equality)],[78,24]),
[iquote('3:Res:78.0,24.1')] ).
cnf(81,plain,
~ target(theater_ds),
inference(res,[status(thm),theory(equality)],[72,79]),
[iquote('3:Res:72.1,79.0')] ).
cnf(82,plain,
$false,
inference(ssi,[status(thm)],[81,4]),
[iquote('3:SSi:81.0,4.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.07/0.35 % Computer : n014.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 7 14:06:11 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.22/0.53
% 0.22/0.53 SPASS V 3.9
% 0.22/0.53 SPASS beiseite: Proof found.
% 0.22/0.53 % SZS status Theorem
% 0.22/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.53 SPASS derived 48 clauses, backtracked 15 clauses, performed 3 splits and kept 71 clauses.
% 0.22/0.53 SPASS allocated 97858 KBytes.
% 0.22/0.53 SPASS spent 0:00:00.17 on the problem.
% 0.22/0.53 0:00:00.06 for the input.
% 0.22/0.53 0:00:00.05 for the FLOTTER CNF translation.
% 0.22/0.53 0:00:00.00 for inferences.
% 0.22/0.53 0:00:00.00 for the backtracking.
% 0.22/0.53 0:00:00.01 for the reduction.
% 0.22/0.53
% 0.22/0.53
% 0.22/0.53 Here is a proof with depth 9, length 52 :
% 0.22/0.53 % SZS output start Refutation
% See solution above
% 0.22/0.53 Formulae used in the proof : agent_portal action_modify target_theater open_world_closure conjecture no_proh_modify
% 0.22/0.53
%------------------------------------------------------------------------------