%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : MGT109+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n007.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 : Satisfiable 1.35s 1.66s
% Output : Saturation 1.35s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 88ERROR: Could not build tree for root 370ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(384,plain,
( ~ perm(u)
| ~ disability(skf37(v,w,x,y,u,z))
| ~ proh(x1)
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,v)
| ~ bearer(skf37(v,w,x,y,u,z),x2)
| ~ tgt(x1,x)
| ~ aee(x1,x3)
| ~ aer(x1,x2)
| ~ act(x1,y) ),
inference(res,[status(thm),theory(equality)],[121,105]),
[iquote('0:Res:121.6,105.7')] ).
cnf(368,plain,
( ~ perm(u)
| ~ disability(skf38(v,w,x,y,u,z))
| ~ proh(x1)
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,v)
| ~ aer(u,y)
| ~ bearer(skf38(v,w,x,y,u,z),x2)
| ~ tgt(x1,w)
| ~ aee(x1,x3)
| ~ aer(x1,x2)
| ~ act(x1,v) ),
inference(res,[status(thm),theory(equality)],[122,105]),
[iquote('0:Res:122.6,105.7')] ).
cnf(382,plain,
( ~ perm(u)
| ~ subjection(skf37(v,w,x,decl(y),u,z))
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,decl(y))
| ~ aer(u,v)
| ~ part_of(skf37(v,w,x,decl(y),u,z),x1)
| ~ founds_rem(x2,x1,x3)
| about_event(skf37(v,w,x,decl(y),u,z),x2) ),
inference(res,[status(thm),theory(equality)],[121,62]),
[iquote('0:Res:121.6,62.3')] ).
cnf(383,plain,
( ~ perm(u)
| ~ power(skf37(v,w,x,decl(y),u,z))
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,decl(y))
| ~ aer(u,v)
| ~ part_of(skf37(v,w,x,decl(y),u,z),x1)
| ~ founds_rem(x2,x1,x3)
| about_event(skf37(v,w,x,decl(y),u,z),x2) ),
inference(res,[status(thm),theory(equality)],[121,63]),
[iquote('0:Res:121.6,63.3')] ).
cnf(366,plain,
( ~ perm(u)
| ~ subjection(skf38(decl(v),w,x,y,u,z))
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,decl(v))
| ~ aer(u,y)
| ~ part_of(skf38(decl(v),w,x,y,u,z),x1)
| ~ founds_rem(x2,x1,x3)
| about_event(skf38(decl(v),w,x,y,u,z),x2) ),
inference(res,[status(thm),theory(equality)],[122,62]),
[iquote('0:Res:122.6,62.3')] ).
cnf(367,plain,
( ~ perm(u)
| ~ power(skf38(decl(v),w,x,y,u,z))
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,decl(v))
| ~ aer(u,y)
| ~ part_of(skf38(decl(v),w,x,y,u,z),x1)
| ~ founds_rem(x2,x1,x3)
| about_event(skf38(decl(v),w,x,y,u,z),x2) ),
inference(res,[status(thm),theory(equality)],[122,63]),
[iquote('0:Res:122.6,63.3')] ).
cnf(370,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ disability(skf37(w,x,y,z,u,x1))
| ~ aee(u,x)
| ~ activates(x1,u)
| ~ tgt(u,y)
| ~ act(u,z)
| ~ aer(u,w)
| ~ part_of(skf37(w,x,y,z,u,x1),v)
| equal(skf37(w,x,y,z,u,x1),skf69(v,y,z)) ),
inference(res,[status(thm),theory(equality)],[121,155]),
[iquote('3:Res:121.6,155.3')] ).
cnf(371,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ right(skf37(w,x,y,z,u,x1))
| ~ aee(u,x)
| ~ activates(x1,u)
| ~ tgt(u,y)
| ~ act(u,z)
| ~ aer(u,w)
| ~ part_of(skf37(w,x,y,z,u,x1),v)
| equal(skf37(w,x,y,z,u,x1),skf57(v,y,z)) ),
inference(res,[status(thm),theory(equality)],[121,153]),
[iquote('2:Res:121.6,153.3')] ).
cnf(372,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ subjection(skf37(w,x,y,z,u,x1))
| ~ aee(u,x)
| ~ activates(x1,u)
| ~ tgt(u,y)
| ~ act(u,z)
| ~ aer(u,w)
| ~ part_of(skf37(w,x,y,z,u,x1),v)
| equal(skf37(w,x,y,z,u,x1),skf63(v,y,z)) ),
inference(res,[status(thm),theory(equality)],[121,151]),
[iquote('1:Res:121.6,151.3')] ).
cnf(354,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ disability(skf38(w,x,y,z,u,x1))
| ~ aee(u,y)
| ~ activates(x1,u)
| ~ tgt(u,x)
| ~ act(u,w)
| ~ aer(u,z)
| ~ part_of(skf38(w,x,y,z,u,x1),v)
| equal(skf38(w,x,y,z,u,x1),skf69(v,x,w)) ),
inference(res,[status(thm),theory(equality)],[122,155]),
[iquote('3:Res:122.6,155.3')] ).
cnf(355,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ right(skf38(w,x,y,z,u,x1))
| ~ aee(u,y)
| ~ activates(x1,u)
| ~ tgt(u,x)
| ~ act(u,w)
| ~ aer(u,z)
| ~ part_of(skf38(w,x,y,z,u,x1),v)
| equal(skf38(w,x,y,z,u,x1),skf57(v,x,w)) ),
inference(res,[status(thm),theory(equality)],[122,153]),
[iquote('2:Res:122.6,153.3')] ).
cnf(356,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ subjection(skf38(w,x,y,z,u,x1))
| ~ aee(u,y)
| ~ activates(x1,u)
| ~ tgt(u,x)
| ~ act(u,w)
| ~ aer(u,z)
| ~ part_of(skf38(w,x,y,z,u,x1),v)
| equal(skf38(w,x,y,z,u,x1),skf63(v,x,w)) ),
inference(res,[status(thm),theory(equality)],[122,151]),
[iquote('1:Res:122.6,151.3')] ).
cnf(385,plain,
( ~ perm(u)
| ~ permission(v)
| ~ duty(skf37(w,x,y,rfr(z),u,x1))
| ~ aee(u,x)
| ~ activates(x1,u)
| ~ tgt(u,y)
| ~ act(u,rfr(z))
| ~ aer(u,w)
| ~ bearer(v,x2)
| ~ bearer(skf37(w,x,y,rfr(z),u,x1),x2)
| ~ cnt(v,z,y) ),
inference(res,[status(thm),theory(equality)],[121,83]),
[iquote('0:Res:121.6,83.5')] ).
cnf(369,plain,
( ~ perm(u)
| ~ permission(v)
| ~ duty(skf38(rfr(w),x,y,z,u,x1))
| ~ aee(u,y)
| ~ activates(x1,u)
| ~ tgt(u,x)
| ~ act(u,rfr(w))
| ~ aer(u,z)
| ~ bearer(v,x2)
| ~ bearer(skf38(rfr(w),x,y,z,u,x1),x2)
| ~ cnt(v,w,x) ),
inference(res,[status(thm),theory(equality)],[122,83]),
[iquote('0:Res:122.6,83.5')] ).
cnf(376,plain,
( ~ perm(u)
| ~ immunity(skf37(v,w,x,y,u,z))
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,v)
| ~ part_of(skf37(v,w,x,y,u,z),x1)
| equal(skf37(v,w,x,y,u,z),skf72(x1,x,y)) ),
inference(res,[status(thm),theory(equality)],[121,161]),
[iquote('6:Res:121.6,161.2')] ).
cnf(377,plain,
( ~ perm(u)
| ~ power(skf37(v,w,x,y,u,z))
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,v)
| ~ part_of(skf37(v,w,x,y,u,z),x1)
| equal(skf37(v,w,x,y,u,z),skf66(x1,x,y)) ),
inference(res,[status(thm),theory(equality)],[121,159]),
[iquote('5:Res:121.6,159.2')] ).
cnf(378,plain,
( ~ perm(u)
| ~ duty(skf37(v,w,x,y,u,z))
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,v)
| ~ part_of(skf37(v,w,x,y,u,z),x1)
| equal(skf37(v,w,x,y,u,z),skf60(x1,x,y)) ),
inference(res,[status(thm),theory(equality)],[121,157]),
[iquote('4:Res:121.6,157.2')] ).
cnf(360,plain,
( ~ perm(u)
| ~ immunity(skf38(v,w,x,y,u,z))
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,v)
| ~ aer(u,y)
| ~ part_of(skf38(v,w,x,y,u,z),x1)
| equal(skf38(v,w,x,y,u,z),skf72(x1,w,v)) ),
inference(res,[status(thm),theory(equality)],[122,161]),
[iquote('6:Res:122.6,161.2')] ).
cnf(361,plain,
( ~ perm(u)
| ~ power(skf38(v,w,x,y,u,z))
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,v)
| ~ aer(u,y)
| ~ part_of(skf38(v,w,x,y,u,z),x1)
| equal(skf38(v,w,x,y,u,z),skf66(x1,w,v)) ),
inference(res,[status(thm),theory(equality)],[122,159]),
[iquote('5:Res:122.6,159.2')] ).
cnf(362,plain,
( ~ perm(u)
| ~ duty(skf38(v,w,x,y,u,z))
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,v)
| ~ aer(u,y)
| ~ part_of(skf38(v,w,x,y,u,z),x1)
| equal(skf38(v,w,x,y,u,z),skf60(x1,w,v)) ),
inference(res,[status(thm),theory(equality)],[122,157]),
[iquote('4:Res:122.6,157.2')] ).
cnf(336,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ disability(skf53(v,w,x,u))
| ~ proh(y)
| ~ part_of(v,u)
| ~ cnt(v,x,w)
| ~ bearer(skf53(v,w,x,u),z)
| ~ tgt(y,w)
| ~ aee(y,x1)
| ~ aer(y,z)
| ~ act(y,x)
| skP0(w,x,u) ),
inference(res,[status(thm),theory(equality)],[102,105]),
[iquote('0:Res:102.5,105.7')] ).
cnf(332,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ subjection(skf53(v,w,decl(x),u))
| ~ part_of(v,u)
| ~ cnt(v,decl(x),w)
| ~ part_of(skf53(v,w,decl(x),u),y)
| ~ founds_rem(z,y,x1)
| skP0(w,decl(x),u)
| about_event(skf53(v,w,decl(x),u),z) ),
inference(res,[status(thm),theory(equality)],[102,62]),
[iquote('0:Res:102.5,62.3')] ).
cnf(333,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ power(skf53(v,w,decl(x),u))
| ~ part_of(v,u)
| ~ cnt(v,decl(x),w)
| ~ part_of(skf53(v,w,decl(x),u),y)
| ~ founds_rem(z,y,x1)
| skP0(w,decl(x),u)
| about_event(skf53(v,w,decl(x),u),z) ),
inference(res,[status(thm),theory(equality)],[102,63]),
[iquote('0:Res:102.5,63.3')] ).
cnf(335,plain,
( ~ permission(u)
| ~ disability(skf55(u,v,w,x))
| ~ proh(y)
| ~ part_of(u,x)
| ~ cnt(u,w,v)
| ~ bearer(skf55(u,v,w,x),z)
| ~ tgt(y,v)
| ~ aee(y,x1)
| ~ aer(y,z)
| ~ act(y,w)
| skP0(v,w,x) ),
inference(res,[status(thm),theory(equality)],[82,105]),
[iquote('0:Res:82.4,105.7')] ).
cnf(373,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ disability(skf37(w,x,y,z,u,x1))
| ~ aee(u,x)
| ~ activates(x1,u)
| ~ tgt(u,y)
| ~ act(u,z)
| ~ aer(u,w)
| ~ part_of(skf37(w,x,y,z,u,x1),v)
| skP3(y,z,v) ),
inference(res,[status(thm),theory(equality)],[121,154]),
[iquote('3:Res:121.6,154.3')] ).
cnf(374,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ right(skf37(w,x,y,z,u,x1))
| ~ aee(u,x)
| ~ activates(x1,u)
| ~ tgt(u,y)
| ~ act(u,z)
| ~ aer(u,w)
| ~ part_of(skf37(w,x,y,z,u,x1),v)
| skP1(y,z,v) ),
inference(res,[status(thm),theory(equality)],[121,152]),
[iquote('2:Res:121.6,152.3')] ).
cnf(375,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ subjection(skf37(w,x,y,z,u,x1))
| ~ aee(u,x)
| ~ activates(x1,u)
| ~ tgt(u,y)
| ~ act(u,z)
| ~ aer(u,w)
| ~ part_of(skf37(w,x,y,z,u,x1),v)
| skP2(y,z,v) ),
inference(res,[status(thm),theory(equality)],[121,150]),
[iquote('1:Res:121.6,150.3')] ).
cnf(357,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ disability(skf38(w,x,y,z,u,x1))
| ~ aee(u,y)
| ~ activates(x1,u)
| ~ tgt(u,x)
| ~ act(u,w)
| ~ aer(u,z)
| ~ part_of(skf38(w,x,y,z,u,x1),v)
| skP3(x,w,v) ),
inference(res,[status(thm),theory(equality)],[122,154]),
[iquote('3:Res:122.6,154.3')] ).
cnf(334,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ permission(w)
| ~ duty(skf53(v,x,rfr(y),u))
| ~ part_of(v,u)
| ~ cnt(v,rfr(y),x)
| ~ bearer(w,z)
| ~ bearer(skf53(v,x,rfr(y),u),z)
| ~ cnt(w,y,x)
| skP0(x,rfr(y),u) ),
inference(res,[status(thm),theory(equality)],[102,83]),
[iquote('0:Res:102.5,83.5')] ).
cnf(358,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ right(skf38(w,x,y,z,u,x1))
| ~ aee(u,y)
| ~ activates(x1,u)
| ~ tgt(u,x)
| ~ act(u,w)
| ~ aer(u,z)
| ~ part_of(skf38(w,x,y,z,u,x1),v)
| skP1(x,w,v) ),
inference(res,[status(thm),theory(equality)],[122,152]),
[iquote('2:Res:122.6,152.3')] ).
cnf(359,plain,
( ~ perm(u)
| ~ odrl_rel(v)
| ~ subjection(skf38(w,x,y,z,u,x1))
| ~ aee(u,y)
| ~ activates(x1,u)
| ~ tgt(u,x)
| ~ act(u,w)
| ~ aer(u,z)
| ~ part_of(skf38(w,x,y,z,u,x1),v)
| skP2(x,w,v) ),
inference(res,[status(thm),theory(equality)],[122,150]),
[iquote('1:Res:122.6,150.3')] ).
cnf(308,plain,
( ~ permission(u)
| ~ subjection(skf55(u,v,decl(w),x))
| ~ part_of(u,x)
| ~ cnt(u,decl(w),v)
| ~ part_of(skf55(u,v,decl(w),x),y)
| ~ founds_rem(z,y,x1)
| skP0(v,decl(w),x)
| about_event(skf55(u,v,decl(w),x),z) ),
inference(res,[status(thm),theory(equality)],[82,62]),
[iquote('0:Res:82.4,62.3')] ).
cnf(309,plain,
( ~ permission(u)
| ~ power(skf55(u,v,decl(w),x))
| ~ part_of(u,x)
| ~ cnt(u,decl(w),v)
| ~ part_of(skf55(u,v,decl(w),x),y)
| ~ founds_rem(z,y,x1)
| skP0(v,decl(w),x)
| about_event(skf55(u,v,decl(w),x),z) ),
inference(res,[status(thm),theory(equality)],[82,63]),
[iquote('0:Res:82.4,63.3')] ).
cnf(320,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ odrl_rel(w)
| ~ disability(skf53(v,x,y,u))
| ~ part_of(v,u)
| ~ cnt(v,y,x)
| ~ part_of(skf53(v,x,y,u),w)
| skP0(x,y,u)
| equal(skf53(v,x,y,u),skf69(w,x,y)) ),
inference(res,[status(thm),theory(equality)],[102,155]),
[iquote('3:Res:102.5,155.3')] ).
cnf(321,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ odrl_rel(w)
| ~ right(skf53(v,x,y,u))
| ~ part_of(v,u)
| ~ cnt(v,y,x)
| ~ part_of(skf53(v,x,y,u),w)
| skP0(x,y,u)
| equal(skf53(v,x,y,u),skf57(w,x,y)) ),
inference(res,[status(thm),theory(equality)],[102,153]),
[iquote('2:Res:102.5,153.3')] ).
cnf(322,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ odrl_rel(w)
| ~ subjection(skf53(v,x,y,u))
| ~ part_of(v,u)
| ~ cnt(v,y,x)
| ~ part_of(skf53(v,x,y,u),w)
| skP0(x,y,u)
| equal(skf53(v,x,y,u),skf63(w,x,y)) ),
inference(res,[status(thm),theory(equality)],[102,151]),
[iquote('1:Res:102.5,151.3')] ).
cnf(379,plain,
( ~ perm(u)
| ~ immunity(skf37(v,w,x,y,u,z))
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,v)
| ~ part_of(skf37(v,w,x,y,u,z),x1)
| skP3(x,y,x1) ),
inference(res,[status(thm),theory(equality)],[121,160]),
[iquote('6:Res:121.6,160.2')] ).
cnf(380,plain,
( ~ perm(u)
| ~ power(skf37(v,w,x,y,u,z))
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,v)
| ~ part_of(skf37(v,w,x,y,u,z),x1)
| skP2(x,y,x1) ),
inference(res,[status(thm),theory(equality)],[121,158]),
[iquote('5:Res:121.6,158.2')] ).
cnf(310,plain,
( ~ permission(u)
| ~ permission(v)
| ~ duty(skf55(u,w,rfr(x),y))
| ~ part_of(u,y)
| ~ cnt(u,rfr(x),w)
| ~ bearer(v,z)
| ~ bearer(skf55(u,w,rfr(x),y),z)
| ~ cnt(v,x,w)
| skP0(w,rfr(x),y) ),
inference(res,[status(thm),theory(equality)],[82,83]),
[iquote('0:Res:82.4,83.5')] ).
cnf(381,plain,
( ~ perm(u)
| ~ duty(skf37(v,w,x,y,u,z))
| ~ aee(u,w)
| ~ activates(z,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,v)
| ~ part_of(skf37(v,w,x,y,u,z),x1)
| skP1(x,y,x1) ),
inference(res,[status(thm),theory(equality)],[121,156]),
[iquote('4:Res:121.6,156.2')] ).
cnf(363,plain,
( ~ perm(u)
| ~ immunity(skf38(v,w,x,y,u,z))
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,v)
| ~ aer(u,y)
| ~ part_of(skf38(v,w,x,y,u,z),x1)
| skP3(w,v,x1) ),
inference(res,[status(thm),theory(equality)],[122,160]),
[iquote('6:Res:122.6,160.2')] ).
cnf(364,plain,
( ~ perm(u)
| ~ power(skf38(v,w,x,y,u,z))
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,v)
| ~ aer(u,y)
| ~ part_of(skf38(v,w,x,y,u,z),x1)
| skP2(w,v,x1) ),
inference(res,[status(thm),theory(equality)],[122,158]),
[iquote('5:Res:122.6,158.2')] ).
cnf(365,plain,
( ~ perm(u)
| ~ duty(skf38(v,w,x,y,u,z))
| ~ aee(u,x)
| ~ activates(z,u)
| ~ tgt(u,w)
| ~ act(u,v)
| ~ aer(u,y)
| ~ part_of(skf38(v,w,x,y,u,z),x1)
| skP1(w,v,x1) ),
inference(res,[status(thm),theory(equality)],[122,156]),
[iquote('4:Res:122.6,156.2')] ).
cnf(326,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ immunity(skf53(v,w,x,u))
| ~ part_of(v,u)
| ~ cnt(v,x,w)
| ~ part_of(skf53(v,w,x,u),y)
| skP0(w,x,u)
| equal(skf53(v,w,x,u),skf72(y,w,x)) ),
inference(res,[status(thm),theory(equality)],[102,161]),
[iquote('6:Res:102.5,161.2')] ).
cnf(327,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ power(skf53(v,w,x,u))
| ~ part_of(v,u)
| ~ cnt(v,x,w)
| ~ part_of(skf53(v,w,x,u),y)
| skP0(w,x,u)
| equal(skf53(v,w,x,u),skf66(y,w,x)) ),
inference(res,[status(thm),theory(equality)],[102,159]),
[iquote('5:Res:102.5,159.2')] ).
cnf(328,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ duty(skf53(v,w,x,u))
| ~ part_of(v,u)
| ~ cnt(v,x,w)
| ~ part_of(skf53(v,w,x,u),y)
| skP0(w,x,u)
| equal(skf53(v,w,x,u),skf60(y,w,x)) ),
inference(res,[status(thm),theory(equality)],[102,157]),
[iquote('4:Res:102.5,157.2')] ).
cnf(296,plain,
( ~ permission(u)
| ~ odrl_rel(v)
| ~ disability(skf55(u,w,x,y))
| ~ part_of(u,y)
| ~ cnt(u,x,w)
| ~ part_of(skf55(u,w,x,y),v)
| skP0(w,x,y)
| equal(skf55(u,w,x,y),skf69(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[82,155]),
[iquote('3:Res:82.4,155.3')] ).
cnf(297,plain,
( ~ permission(u)
| ~ odrl_rel(v)
| ~ right(skf55(u,w,x,y))
| ~ part_of(u,y)
| ~ cnt(u,x,w)
| ~ part_of(skf55(u,w,x,y),v)
| skP0(w,x,y)
| equal(skf55(u,w,x,y),skf57(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[82,153]),
[iquote('2:Res:82.4,153.3')] ).
cnf(298,plain,
( ~ permission(u)
| ~ odrl_rel(v)
| ~ subjection(skf55(u,w,x,y))
| ~ part_of(u,y)
| ~ cnt(u,x,w)
| ~ part_of(skf55(u,w,x,y),v)
| skP0(w,x,y)
| equal(skf55(u,w,x,y),skf63(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[82,151]),
[iquote('1:Res:82.4,151.3')] ).
cnf(302,plain,
( ~ permission(u)
| ~ immunity(skf55(u,v,w,x))
| ~ part_of(u,x)
| ~ cnt(u,w,v)
| ~ part_of(skf55(u,v,w,x),y)
| skP0(v,w,x)
| equal(skf55(u,v,w,x),skf72(y,v,w)) ),
inference(res,[status(thm),theory(equality)],[82,161]),
[iquote('6:Res:82.4,161.2')] ).
cnf(303,plain,
( ~ permission(u)
| ~ power(skf55(u,v,w,x))
| ~ part_of(u,x)
| ~ cnt(u,w,v)
| ~ part_of(skf55(u,v,w,x),y)
| skP0(v,w,x)
| equal(skf55(u,v,w,x),skf66(y,v,w)) ),
inference(res,[status(thm),theory(equality)],[82,159]),
[iquote('5:Res:82.4,159.2')] ).
cnf(304,plain,
( ~ permission(u)
| ~ duty(skf55(u,v,w,x))
| ~ part_of(u,x)
| ~ cnt(u,w,v)
| ~ part_of(skf55(u,v,w,x),y)
| skP0(v,w,x)
| equal(skf55(u,v,w,x),skf60(y,v,w)) ),
inference(res,[status(thm),theory(equality)],[82,157]),
[iquote('4:Res:82.4,157.2')] ).
cnf(146,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| part_of(skf46(w,y,z,v,u,x),skf48(u,x,v,z,y,w)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(147,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| part_of(skf47(v,y,z,w,u,x),skf48(u,x,v,z,y,w)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(148,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| part_of(skf40(v,y,z,w,u,x),skf42(u,x,w,z,y,v)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(323,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ odrl_rel(w)
| ~ disability(skf53(v,x,y,u))
| ~ part_of(v,u)
| ~ cnt(v,y,x)
| ~ part_of(skf53(v,x,y,u),w)
| skP0(x,y,u)
| skP3(x,y,w) ),
inference(res,[status(thm),theory(equality)],[102,154]),
[iquote('3:Res:102.5,154.3')] ).
cnf(324,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ odrl_rel(w)
| ~ right(skf53(v,x,y,u))
| ~ part_of(v,u)
| ~ cnt(v,y,x)
| ~ part_of(skf53(v,x,y,u),w)
| skP0(x,y,u)
| skP1(x,y,w) ),
inference(res,[status(thm),theory(equality)],[102,152]),
[iquote('2:Res:102.5,152.3')] ).
cnf(325,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ odrl_rel(w)
| ~ subjection(skf53(v,x,y,u))
| ~ part_of(v,u)
| ~ cnt(v,y,x)
| ~ part_of(skf53(v,x,y,u),w)
| skP0(x,y,u)
| skP2(x,y,w) ),
inference(res,[status(thm),theory(equality)],[102,150]),
[iquote('1:Res:102.5,150.3')] ).
cnf(149,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| part_of(skf41(w,y,z,v,u,x),skf42(u,x,w,z,y,v)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(337,plain,
( ~ odrl_rel(u)
| ~ disability(skf52(v,w,u))
| ~ proh(x)
| ~ skP0(v,w,u)
| ~ bearer(skf52(v,w,u),y)
| ~ tgt(x,v)
| ~ aee(x,z)
| ~ aer(x,y)
| ~ act(x,w) ),
inference(res,[status(thm),theory(equality)],[57,105]),
[iquote('0:Res:57.2,105.7')] ).
cnf(339,plain,
( ~ odrl_rel(u)
| ~ disability(skf63(u,v,w))
| ~ proh(x)
| ~ skP2(v,w,u)
| ~ bearer(skf63(u,v,w),y)
| ~ tgt(x,v)
| ~ aee(x,z)
| ~ aer(x,y)
| ~ act(x,w) ),
inference(res,[status(thm),theory(equality)],[59,105]),
[iquote('0:Res:59.2,105.7')] ).
cnf(340,plain,
( ~ odrl_rel(u)
| ~ disability(skf57(u,v,w))
| ~ proh(x)
| ~ skP1(v,w,u)
| ~ bearer(skf57(u,v,w),y)
| ~ tgt(x,v)
| ~ aee(x,z)
| ~ aer(x,y)
| ~ act(x,w) ),
inference(res,[status(thm),theory(equality)],[58,105]),
[iquote('0:Res:58.2,105.7')] ).
cnf(142,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| part_of(skf43(z,x,y,v,u,w),skf45(u,w,v,y,x,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(143,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| part_of(skf44(v,x,y,z,u,w),skf45(u,w,v,y,x,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(446,plain,
( ~ aee(p1,u)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| part_of(skf37(x,u,v,w,p1,e1),skf39(p1,e1,y,z,x1,x2)) ),
inference(mrr,[status(thm)],[445,12]),
[iquote('0:MRR:445.1,12.0')] ).
cnf(144,axiom,
( ~ perm(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| part_of(skf37(z,v,x,y,u,w),skf39(u,w,y,x,v,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(440,plain,
( ~ aee(p1,u)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| part_of(skf38(w,v,u,x,p1,e1),skf39(p1,e1,y,z,x1,x2)) ),
inference(mrr,[status(thm)],[439,12]),
[iquote('0:MRR:439.1,12.0')] ).
cnf(145,axiom,
( ~ perm(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| part_of(skf38(y,x,v,z,u,w),skf39(u,w,y,x,v,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(140,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| part_of(skf49(z,x,y,v,u,w),skf51(u,w,v,y,x,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(329,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ immunity(skf53(v,w,x,u))
| ~ part_of(v,u)
| ~ cnt(v,x,w)
| ~ part_of(skf53(v,w,x,u),y)
| skP0(w,x,u)
| skP3(w,x,y) ),
inference(res,[status(thm),theory(equality)],[102,160]),
[iquote('6:Res:102.5,160.2')] ).
cnf(330,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ power(skf53(v,w,x,u))
| ~ part_of(v,u)
| ~ cnt(v,x,w)
| ~ part_of(skf53(v,w,x,u),y)
| skP0(w,x,u)
| skP2(w,x,y) ),
inference(res,[status(thm),theory(equality)],[102,158]),
[iquote('5:Res:102.5,158.2')] ).
cnf(331,plain,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ duty(skf53(v,w,x,u))
| ~ part_of(v,u)
| ~ cnt(v,x,w)
| ~ part_of(skf53(v,w,x,u),y)
| skP0(w,x,u)
| skP1(w,x,y) ),
inference(res,[status(thm),theory(equality)],[102,156]),
[iquote('4:Res:102.5,156.2')] ).
cnf(299,plain,
( ~ permission(u)
| ~ odrl_rel(v)
| ~ disability(skf55(u,w,x,y))
| ~ part_of(u,y)
| ~ cnt(u,x,w)
| ~ part_of(skf55(u,w,x,y),v)
| skP0(w,x,y)
| skP3(w,x,v) ),
inference(res,[status(thm),theory(equality)],[82,154]),
[iquote('3:Res:82.4,154.3')] ).
cnf(141,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| part_of(skf50(v,x,y,z,u,w),skf51(u,w,v,y,x,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(300,plain,
( ~ permission(u)
| ~ odrl_rel(v)
| ~ right(skf55(u,w,x,y))
| ~ part_of(u,y)
| ~ cnt(u,x,w)
| ~ part_of(skf55(u,w,x,y),v)
| skP0(w,x,y)
| skP1(w,x,v) ),
inference(res,[status(thm),theory(equality)],[82,152]),
[iquote('2:Res:82.4,152.3')] ).
cnf(301,plain,
( ~ permission(u)
| ~ odrl_rel(v)
| ~ subjection(skf55(u,w,x,y))
| ~ part_of(u,y)
| ~ cnt(u,x,w)
| ~ part_of(skf55(u,w,x,y),v)
| skP0(w,x,y)
| skP2(w,x,v) ),
inference(res,[status(thm),theory(equality)],[82,150]),
[iquote('1:Res:82.4,150.3')] ).
cnf(341,plain,
( ~ disability(skf54(u,v,w))
| ~ proh(x)
| ~ skP0(u,v,w)
| ~ bearer(skf54(u,v,w),y)
| ~ tgt(x,u)
| ~ aee(x,z)
| ~ aer(x,y)
| ~ act(x,v) ),
inference(res,[status(thm),theory(equality)],[39,105]),
[iquote('0:Res:39.1,105.7')] ).
cnf(436,plain,
( ~ proh(p1)
| ~ has_rem(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| cnt(skf46(u,w,x,y,z,x1),decl(x),w) ),
inference(res,[status(thm),theory(equality)],[9,138]),
[iquote('0:Res:9.0,138.2')] ).
cnf(138,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| cnt(skf46(w,y,z,x1,x2,x3),decl(z),y) ),
file('MGT109+1.p',unknown),
[] ).
cnf(342,plain,
( ~ disability(skf72(u,v,w))
| ~ proh(x)
| ~ skP3(v,w,u)
| ~ bearer(skf72(u,v,w),y)
| ~ tgt(x,v)
| ~ aee(x,z)
| ~ aer(x,y)
| ~ act(x,w) ),
inference(res,[status(thm),theory(equality)],[42,105]),
[iquote('0:Res:42.1,105.7')] ).
cnf(343,plain,
( ~ disability(skf66(u,v,w))
| ~ proh(x)
| ~ skP2(v,w,u)
| ~ bearer(skf66(u,v,w),y)
| ~ tgt(x,v)
| ~ aee(x,z)
| ~ aer(x,y)
| ~ act(x,w) ),
inference(res,[status(thm),theory(equality)],[41,105]),
[iquote('0:Res:41.1,105.7')] ).
cnf(344,plain,
( ~ disability(skf60(u,v,w))
| ~ proh(x)
| ~ skP1(v,w,u)
| ~ bearer(skf60(u,v,w),y)
| ~ tgt(x,v)
| ~ aee(x,z)
| ~ aer(x,y)
| ~ act(x,w) ),
inference(res,[status(thm),theory(equality)],[40,105]),
[iquote('0:Res:40.1,105.7')] ).
cnf(435,plain,
( ~ proh(p1)
| ~ has_rem(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| cnt(skf47(ensemble,w,x,y,z,x1),decl(x),w) ),
inference(res,[status(thm),theory(equality)],[9,139]),
[iquote('0:Res:9.0,139.2')] ).
cnf(139,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| cnt(skf47(v,y,z,x1,x2,x3),decl(z),y) ),
file('MGT109+1.p',unknown),
[] ).
cnf(260,plain,
( ~ odrl_rel(u)
| ~ subjection(skf52(v,decl(w),u))
| ~ skP0(v,decl(w),u)
| ~ part_of(skf52(v,decl(w),u),x)
| ~ founds_rem(y,x,z)
| about_event(skf52(v,decl(w),u),y) ),
inference(res,[status(thm),theory(equality)],[57,62]),
[iquote('0:Res:57.2,62.3')] ).
cnf(261,plain,
( ~ odrl_rel(u)
| ~ subjection(skf69(u,v,decl(w)))
| ~ skP3(v,decl(w),u)
| ~ part_of(skf69(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf69(u,v,decl(w)),y) ),
inference(res,[status(thm),theory(equality)],[60,62]),
[iquote('0:Res:60.2,62.3')] ).
cnf(263,plain,
( ~ odrl_rel(u)
| ~ subjection(skf57(u,v,decl(w)))
| ~ skP1(v,decl(w),u)
| ~ part_of(skf57(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf57(u,v,decl(w)),y) ),
inference(res,[status(thm),theory(equality)],[58,62]),
[iquote('0:Res:58.2,62.3')] ).
cnf(434,plain,
( ~ proh(p1)
| ~ has_rem(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| founds_rem(v,skf48(p1,v,y,z,x1,x2),p1) ),
inference(res,[status(thm),theory(equality)],[9,134]),
[iquote('0:Res:9.0,134.2')] ).
cnf(134,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| founds_rem(x,skf48(u,x,x1,x2,x3,x4),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(251,plain,
( ~ odrl_rel(u)
| ~ power(skf52(v,decl(w),u))
| ~ skP0(v,decl(w),u)
| ~ part_of(skf52(v,decl(w),u),x)
| ~ founds_rem(y,x,z)
| about_event(skf52(v,decl(w),u),y) ),
inference(res,[status(thm),theory(equality)],[57,63]),
[iquote('0:Res:57.2,63.3')] ).
cnf(252,plain,
( ~ odrl_rel(u)
| ~ power(skf69(u,v,decl(w)))
| ~ skP3(v,decl(w),u)
| ~ part_of(skf69(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf69(u,v,decl(w)),y) ),
inference(res,[status(thm),theory(equality)],[60,63]),
[iquote('0:Res:60.2,63.3')] ).
cnf(254,plain,
( ~ odrl_rel(u)
| ~ power(skf57(u,v,decl(w)))
| ~ skP1(v,decl(w),u)
| ~ part_of(skf57(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf57(u,v,decl(w)),y) ),
inference(res,[status(thm),theory(equality)],[58,63]),
[iquote('0:Res:58.2,63.3')] ).
cnf(433,plain,
( ~ strong(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| founds_imm(v,skf42(p1,v,y,z,x1,x2),p1) ),
inference(ssi,[status(thm)],[432,5,7]),
[iquote('0:SSi:432.0,5.0,7.0')] ).
cnf(137,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| founds_imm(x,skf42(u,x,x1,x2,x3,x4),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(311,plain,
( ~ odrl_rel(u)
| ~ permission(v)
| ~ duty(skf52(w,rfr(x),u))
| ~ skP0(w,rfr(x),u)
| ~ bearer(v,y)
| ~ bearer(skf52(w,rfr(x),u),y)
| ~ cnt(v,x,w) ),
inference(res,[status(thm),theory(equality)],[57,83]),
[iquote('0:Res:57.2,83.5')] ).
cnf(312,plain,
( ~ odrl_rel(u)
| ~ permission(v)
| ~ duty(skf69(u,w,rfr(x)))
| ~ skP3(w,rfr(x),u)
| ~ bearer(v,y)
| ~ bearer(skf69(u,w,rfr(x)),y)
| ~ cnt(v,x,w) ),
inference(res,[status(thm),theory(equality)],[60,83]),
[iquote('0:Res:60.2,83.5')] ).
cnf(313,plain,
( ~ odrl_rel(u)
| ~ permission(v)
| ~ duty(skf63(u,w,rfr(x)))
| ~ skP2(w,rfr(x),u)
| ~ bearer(v,y)
| ~ bearer(skf63(u,w,rfr(x)),y)
| ~ cnt(v,x,w) ),
inference(res,[status(thm),theory(equality)],[59,83]),
[iquote('0:Res:59.2,83.5')] ).
cnf(431,plain,
( ~ strong(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| cnt(skf40(ensemble,w,x,y,z,x1),x,w) ),
inference(ssi,[status(thm)],[430,5,7]),
[iquote('0:SSi:430.0,5.0,7.0')] ).
cnf(135,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| cnt(skf40(v,y,z,x1,x2,x3),z,y) ),
file('MGT109+1.p',unknown),
[] ).
cnf(314,plain,
( ~ odrl_rel(u)
| ~ permission(v)
| ~ duty(skf57(u,w,rfr(x)))
| ~ skP1(w,rfr(x),u)
| ~ bearer(v,y)
| ~ bearer(skf57(u,w,rfr(x)),y)
| ~ cnt(v,x,w) ),
inference(res,[status(thm),theory(equality)],[58,83]),
[iquote('0:Res:58.2,83.5')] ).
cnf(305,plain,
( ~ permission(u)
| ~ immunity(skf55(u,v,w,x))
| ~ part_of(u,x)
| ~ cnt(u,w,v)
| ~ part_of(skf55(u,v,w,x),y)
| skP0(v,w,x)
| skP3(v,w,y) ),
inference(res,[status(thm),theory(equality)],[82,160]),
[iquote('6:Res:82.4,160.2')] ).
cnf(306,plain,
( ~ permission(u)
| ~ power(skf55(u,v,w,x))
| ~ part_of(u,x)
| ~ cnt(u,w,v)
| ~ part_of(skf55(u,v,w,x),y)
| skP0(v,w,x)
| skP2(v,w,y) ),
inference(res,[status(thm),theory(equality)],[82,158]),
[iquote('5:Res:82.4,158.2')] ).
cnf(429,plain,
( ~ strong(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| cnt(skf41(u,w,x,y,z,x1),x,w) ),
inference(ssi,[status(thm)],[428,5,7]),
[iquote('0:SSi:428.0,5.0,7.0')] ).
cnf(136,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| cnt(skf41(w,y,z,x1,x2,x3),z,y) ),
file('MGT109+1.p',unknown),
[] ).
cnf(307,plain,
( ~ permission(u)
| ~ duty(skf55(u,v,w,x))
| ~ part_of(u,x)
| ~ cnt(u,w,v)
| ~ part_of(skf55(u,v,w,x),y)
| skP0(v,w,x)
| skP1(v,w,y) ),
inference(res,[status(thm),theory(equality)],[82,156]),
[iquote('4:Res:82.4,156.2')] ).
cnf(427,plain,
( ~ proh(p1)
| ~ has_rem(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| bearer(skf46(u,y,z,x1,x2,x3),u) ),
inference(res,[status(thm),theory(equality)],[9,130]),
[iquote('0:Res:9.0,130.2')] ).
cnf(130,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| bearer(skf46(w,x1,x2,x3,x4,x5),w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(426,plain,
( ~ proh(p1)
| ~ has_rem(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| bearer(skf47(ensemble,y,z,x1,x2,x3),ensemble) ),
inference(res,[status(thm),theory(equality)],[9,131]),
[iquote('0:Res:9.0,131.2')] ).
cnf(131,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| bearer(skf47(v,x1,x2,x3,x4,x5),v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(425,plain,
( ~ strong(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| bearer(skf40(ensemble,y,z,x1,x2,x3),ensemble) ),
inference(ssi,[status(thm)],[424,5,7]),
[iquote('0:SSi:424.0,5.0,7.0')] ).
cnf(132,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| bearer(skf40(v,x1,x2,x3,x4,x5),v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(421,plain,
( ~ proh(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| cnt(skf43(x,v,w,y,z,x1),rfr(w),v) ),
inference(res,[status(thm),theory(equality)],[8,126]),
[iquote('0:Res:8.0,126.1')] ).
cnf(423,plain,
( ~ strong(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| bearer(skf41(u,y,z,x1,x2,x3),u) ),
inference(ssi,[status(thm)],[422,5,7]),
[iquote('0:SSi:422.0,5.0,7.0')] ).
cnf(133,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| bearer(skf41(w,x1,x2,x3,x4,x5),w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(126,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| cnt(skf43(z,x,y,x1,x2,x3),rfr(y),x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(420,plain,
( ~ proh(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| cnt(skf44(bibliothek,v,w,y,z,x1),rfr(w),v) ),
inference(res,[status(thm),theory(equality)],[8,127]),
[iquote('0:Res:8.0,127.1')] ).
cnf(127,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| cnt(skf44(v,x,y,x1,x2,x3),rfr(y),x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(419,plain,
( ~ proh(p1)
| ~ has_rem(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| subjection(skf46(y,z,x1,x2,x3,x4)) ),
inference(res,[status(thm),theory(equality)],[9,124]),
[iquote('0:Res:9.0,124.2')] ).
cnf(124,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| subjection(skf46(x1,x2,x3,x4,x5,x6)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(345,plain,
( ~ odrl_rel(u)
| ~ proh(v)
| ~ skP3(w,x,u)
| ~ bearer(skf69(u,w,x),y)
| ~ tgt(v,w)
| ~ aee(v,z)
| ~ aer(v,y)
| ~ act(v,x) ),
inference(mrr,[status(thm)],[338,52]),
[iquote('0:MRR:338.1,52.2')] ).
cnf(287,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ disability(skf52(w,x,u))
| ~ skP0(w,x,u)
| ~ part_of(skf52(w,x,u),v)
| equal(skf52(w,x,u),skf69(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[57,155]),
[iquote('3:Res:57.2,155.3')] ).
cnf(289,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ disability(skf63(u,w,x))
| ~ skP2(w,x,u)
| ~ part_of(skf63(u,w,x),v)
| equal(skf63(u,w,x),skf69(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[59,155]),
[iquote('3:Res:59.2,155.3')] ).
cnf(418,plain,
( ~ proh(p1)
| ~ has_rem(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| power(skf47(y,z,x1,x2,x3,x4)) ),
inference(res,[status(thm),theory(equality)],[9,125]),
[iquote('0:Res:9.0,125.2')] ).
cnf(125,axiom,
( ~ proh(u)
| ~ has_rem(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| power(skf47(x1,x2,x3,x4,x5,x6)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(290,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ disability(skf57(u,w,x))
| ~ skP1(w,x,u)
| ~ part_of(skf57(u,w,x),v)
| equal(skf57(u,w,x),skf69(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[58,155]),
[iquote('3:Res:58.2,155.3')] ).
cnf(278,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ right(skf52(w,x,u))
| ~ skP0(w,x,u)
| ~ part_of(skf52(w,x,u),v)
| equal(skf52(w,x,u),skf57(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[57,153]),
[iquote('2:Res:57.2,153.3')] ).
cnf(279,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ right(skf69(u,w,x))
| ~ skP3(w,x,u)
| ~ part_of(skf69(u,w,x),v)
| equal(skf69(u,w,x),skf57(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[60,153]),
[iquote('2:Res:60.2,153.3')] ).
cnf(417,plain,
( ~ strong(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| disability(skf40(y,z,x1,x2,x3,x4)) ),
inference(ssi,[status(thm)],[416,5,7]),
[iquote('0:SSi:416.0,5.0,7.0')] ).
cnf(128,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| disability(skf40(x1,x2,x3,x4,x5,x6)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(280,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ right(skf63(u,w,x))
| ~ skP2(w,x,u)
| ~ part_of(skf63(u,w,x),v)
| equal(skf63(u,w,x),skf57(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[59,153]),
[iquote('2:Res:59.2,153.3')] ).
cnf(395,plain,
( ~ proh(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| founds(u,skf45(p1,u,y,z,x1,x2),p1) ),
inference(res,[status(thm),theory(equality)],[8,120]),
[iquote('0:Res:8.0,120.1')] ).
cnf(405,plain,
( ~ strong(p1)
| ~ aee(p1,u)
| ~ activates(v,p1)
| ~ tgt(p1,w)
| ~ act(p1,x)
| immunity(skf41(y,z,x1,x2,x3,x4)) ),
inference(ssi,[status(thm)],[404,5,7]),
[iquote('0:SSi:404.0,5.0,7.0')] ).
cnf(402,plain,
equal(skf39(p1,e1,u,v,w,x),skf39(p1,e1,y,z,x1,x2)),
inference(res,[status(thm),theory(equality)],[394,399]),
[iquote('0:Res:394.0,399.0')] ).
cnf(129,axiom,
( ~ perm(u)
| ~ strong(u)
| ~ aer(u,v)
| ~ aee(u,w)
| ~ activates(x,u)
| ~ tgt(u,y)
| ~ act(u,z)
| immunity(skf41(x1,x2,x3,x4,x5,x6)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(400,plain,
( ~ founds(u,skf39(p1,e1,v,w,x,y),p1)
| equal(u,e1) ),
inference(res,[status(thm),theory(equality)],[394,45]),
[iquote('0:Res:394.0,45.0')] ).
cnf(399,plain,
( ~ founds(e1,u,p1)
| equal(u,skf39(p1,e1,v,w,x,y)) ),
inference(res,[status(thm),theory(equality)],[394,44]),
[iquote('0:Res:394.0,44.0')] ).
cnf(401,plain,
odrl_rel(skf39(p1,e1,u,v,w,x)),
inference(ssi,[status(thm)],[397,5,7]),
[iquote('0:SSi:397.0,5.0,7.0')] ).
cnf(394,plain,
founds(e1,skf39(p1,e1,u,v,w,x),p1),
inference(res,[status(thm),theory(equality)],[9,393]),
[iquote('0:Res:9.0,393.0')] ).
cnf(120,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| founds(w,skf45(u,w,x1,x2,x3,x4),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(390,plain,
( ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| founds(u,skf39(p1,u,y,z,x1,x2),p1) ),
inference(ssi,[status(thm)],[389,5,7]),
[iquote('0:SSi:389.0,5.0,7.0')] ).
cnf(123,axiom,
( ~ perm(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| founds(w,skf39(u,w,x1,x2,x3,x4),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(269,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ subjection(skf52(w,x,u))
| ~ skP0(w,x,u)
| ~ part_of(skf52(w,x,u),v)
| equal(skf52(w,x,u),skf63(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[57,151]),
[iquote('1:Res:57.2,151.3')] ).
cnf(270,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ subjection(skf69(u,w,x))
| ~ skP3(w,x,u)
| ~ part_of(skf69(u,w,x),v)
| equal(skf69(u,w,x),skf63(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[60,151]),
[iquote('1:Res:60.2,151.3')] ).
cnf(272,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ subjection(skf57(u,w,x))
| ~ skP1(w,x,u)
| ~ part_of(skf57(u,w,x),v)
| equal(skf57(u,w,x),skf63(v,w,x)) ),
inference(res,[status(thm),theory(equality)],[58,151]),
[iquote('1:Res:58.2,151.3')] ).
cnf(388,plain,
( ~ obl(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| founds(u,skf51(p1,u,y,z,x1,x2),p1) ),
inference(res,[status(thm),theory(equality)],[8,119]),
[iquote('0:Res:8.0,119.1')] ).
cnf(119,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| founds(w,skf51(u,w,x1,x2,x3,x4),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(264,plain,
( ~ subjection(skf54(u,decl(v),w))
| ~ skP0(u,decl(v),w)
| ~ part_of(skf54(u,decl(v),w),x)
| ~ founds_rem(y,x,z)
| about_event(skf54(u,decl(v),w),y) ),
inference(res,[status(thm),theory(equality)],[39,62]),
[iquote('0:Res:39.1,62.3')] ).
cnf(265,plain,
( ~ subjection(skf72(u,v,decl(w)))
| ~ skP3(v,decl(w),u)
| ~ part_of(skf72(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf72(u,v,decl(w)),y) ),
inference(res,[status(thm),theory(equality)],[42,62]),
[iquote('0:Res:42.1,62.3')] ).
cnf(267,plain,
( ~ subjection(skf60(u,v,decl(w)))
| ~ skP1(v,decl(w),u)
| ~ part_of(skf60(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf60(u,v,decl(w)),y) ),
inference(res,[status(thm),theory(equality)],[40,62]),
[iquote('0:Res:40.1,62.3')] ).
cnf(387,plain,
( ~ obl(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| cnt(skf49(x,v,w,y,z,x1),w,v) ),
inference(res,[status(thm),theory(equality)],[8,117]),
[iquote('0:Res:8.0,117.1')] ).
cnf(117,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| cnt(skf49(z,x,y,x1,x2,x3),y,x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(255,plain,
( ~ power(skf54(u,decl(v),w))
| ~ skP0(u,decl(v),w)
| ~ part_of(skf54(u,decl(v),w),x)
| ~ founds_rem(y,x,z)
| about_event(skf54(u,decl(v),w),y) ),
inference(res,[status(thm),theory(equality)],[39,63]),
[iquote('0:Res:39.1,63.3')] ).
cnf(256,plain,
( ~ power(skf72(u,v,decl(w)))
| ~ skP3(v,decl(w),u)
| ~ part_of(skf72(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf72(u,v,decl(w)),y) ),
inference(res,[status(thm),theory(equality)],[42,63]),
[iquote('0:Res:42.1,63.3')] ).
cnf(258,plain,
( ~ power(skf60(u,v,decl(w)))
| ~ skP1(v,decl(w),u)
| ~ part_of(skf60(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf60(u,v,decl(w)),y) ),
inference(res,[status(thm),theory(equality)],[40,63]),
[iquote('0:Res:40.1,63.3')] ).
cnf(386,plain,
( ~ obl(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| cnt(skf50(bibliothek,v,w,y,z,x1),w,v) ),
inference(res,[status(thm),theory(equality)],[8,118]),
[iquote('0:Res:8.0,118.1')] ).
cnf(118,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| cnt(skf50(v,x,y,x1,x2,x3),y,x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(315,plain,
( ~ permission(u)
| ~ duty(skf54(v,rfr(w),x))
| ~ skP0(v,rfr(w),x)
| ~ bearer(u,y)
| ~ bearer(skf54(v,rfr(w),x),y)
| ~ cnt(u,w,v) ),
inference(res,[status(thm),theory(equality)],[39,83]),
[iquote('0:Res:39.1,83.5')] ).
cnf(316,plain,
( ~ permission(u)
| ~ duty(skf72(v,w,rfr(x)))
| ~ skP3(w,rfr(x),v)
| ~ bearer(u,y)
| ~ bearer(skf72(v,w,rfr(x)),y)
| ~ cnt(u,x,w) ),
inference(res,[status(thm),theory(equality)],[42,83]),
[iquote('0:Res:42.1,83.5')] ).
cnf(317,plain,
( ~ permission(u)
| ~ duty(skf66(v,w,rfr(x)))
| ~ skP2(w,rfr(x),v)
| ~ bearer(u,y)
| ~ bearer(skf66(v,w,rfr(x)),y)
| ~ cnt(u,x,w) ),
inference(res,[status(thm),theory(equality)],[41,83]),
[iquote('0:Res:41.1,83.5')] ).
cnf(291,plain,
( ~ odrl_rel(u)
| ~ disability(skf54(v,w,x))
| ~ skP0(v,w,x)
| ~ part_of(skf54(v,w,x),u)
| equal(skf54(v,w,x),skf69(u,v,w)) ),
inference(res,[status(thm),theory(equality)],[39,155]),
[iquote('3:Res:39.1,155.3')] ).
cnf(121,axiom,
( ~ perm(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| cnt(skf37(z,v,x,y,u,w),y,x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(292,plain,
( ~ odrl_rel(u)
| ~ disability(skf72(v,w,x))
| ~ skP3(w,x,v)
| ~ part_of(skf72(v,w,x),u)
| equal(skf72(v,w,x),skf69(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[42,155]),
[iquote('3:Res:42.1,155.3')] ).
cnf(293,plain,
( ~ odrl_rel(u)
| ~ disability(skf66(v,w,x))
| ~ skP2(w,x,v)
| ~ part_of(skf66(v,w,x),u)
| equal(skf66(v,w,x),skf69(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[41,155]),
[iquote('3:Res:41.1,155.3')] ).
cnf(294,plain,
( ~ odrl_rel(u)
| ~ disability(skf60(v,w,x))
| ~ skP1(w,x,v)
| ~ part_of(skf60(v,w,x),u)
| equal(skf60(v,w,x),skf69(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[40,155]),
[iquote('3:Res:40.1,155.3')] ).
cnf(282,plain,
( ~ odrl_rel(u)
| ~ right(skf54(v,w,x))
| ~ skP0(v,w,x)
| ~ part_of(skf54(v,w,x),u)
| equal(skf54(v,w,x),skf57(u,v,w)) ),
inference(res,[status(thm),theory(equality)],[39,153]),
[iquote('2:Res:39.1,153.3')] ).
cnf(122,axiom,
( ~ perm(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| cnt(skf38(y,x,v,z,u,w),y,x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(283,plain,
( ~ odrl_rel(u)
| ~ right(skf72(v,w,x))
| ~ skP3(w,x,v)
| ~ part_of(skf72(v,w,x),u)
| equal(skf72(v,w,x),skf57(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[42,153]),
[iquote('2:Res:42.1,153.3')] ).
cnf(284,plain,
( ~ odrl_rel(u)
| ~ right(skf66(v,w,x))
| ~ skP2(w,x,v)
| ~ part_of(skf66(v,w,x),u)
| equal(skf66(v,w,x),skf57(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[41,153]),
[iquote('2:Res:41.1,153.3')] ).
cnf(285,plain,
( ~ odrl_rel(u)
| ~ right(skf60(v,w,x))
| ~ skP1(w,x,v)
| ~ part_of(skf60(v,w,x),u)
| equal(skf60(v,w,x),skf57(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[40,153]),
[iquote('2:Res:40.1,153.3')] ).
cnf(353,plain,
( ~ proh(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| bearer(skf43(x,y,z,x1,x2,x3),x) ),
inference(res,[status(thm),theory(equality)],[8,112]),
[iquote('0:Res:8.0,112.1')] ).
cnf(112,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| bearer(skf43(z,x1,x2,x3,x4,x5),z) ),
file('MGT109+1.p',unknown),
[] ).
cnf(273,plain,
( ~ odrl_rel(u)
| ~ subjection(skf54(v,w,x))
| ~ skP0(v,w,x)
| ~ part_of(skf54(v,w,x),u)
| equal(skf54(v,w,x),skf63(u,v,w)) ),
inference(res,[status(thm),theory(equality)],[39,151]),
[iquote('1:Res:39.1,151.3')] ).
cnf(274,plain,
( ~ odrl_rel(u)
| ~ subjection(skf72(v,w,x))
| ~ skP3(w,x,v)
| ~ part_of(skf72(v,w,x),u)
| equal(skf72(v,w,x),skf63(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[42,151]),
[iquote('1:Res:42.1,151.3')] ).
cnf(275,plain,
( ~ odrl_rel(u)
| ~ subjection(skf66(v,w,x))
| ~ skP2(w,x,v)
| ~ part_of(skf66(v,w,x),u)
| equal(skf66(v,w,x),skf63(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[41,151]),
[iquote('1:Res:41.1,151.3')] ).
cnf(352,plain,
( ~ proh(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| bearer(skf44(bibliothek,y,z,x1,x2,x3),bibliothek) ),
inference(res,[status(thm),theory(equality)],[8,113]),
[iquote('0:Res:8.0,113.1')] ).
cnf(113,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| bearer(skf44(v,x1,x2,x3,x4,x5),v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(276,plain,
( ~ odrl_rel(u)
| ~ subjection(skf60(v,w,x))
| ~ skP1(w,x,v)
| ~ part_of(skf60(v,w,x),u)
| equal(skf60(v,w,x),skf63(u,w,x)) ),
inference(res,[status(thm),theory(equality)],[40,151]),
[iquote('1:Res:40.1,151.3')] ).
cnf(242,plain,
( ~ odrl_rel(u)
| ~ immunity(skf52(v,w,u))
| ~ skP0(v,w,u)
| ~ part_of(skf52(v,w,u),x)
| equal(skf52(v,w,u),skf72(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[57,161]),
[iquote('6:Res:57.2,161.2')] ).
cnf(243,plain,
( ~ odrl_rel(u)
| ~ immunity(skf69(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf69(u,v,w),x)
| equal(skf69(u,v,w),skf72(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[60,161]),
[iquote('6:Res:60.2,161.2')] ).
cnf(351,plain,
( ~ obl(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| bearer(skf49(x,y,z,x1,x2,x3),x) ),
inference(res,[status(thm),theory(equality)],[8,110]),
[iquote('0:Res:8.0,110.1')] ).
cnf(110,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| bearer(skf49(z,x1,x2,x3,x4,x5),z) ),
file('MGT109+1.p',unknown),
[] ).
cnf(244,plain,
( ~ odrl_rel(u)
| ~ immunity(skf63(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf63(u,v,w),x)
| equal(skf63(u,v,w),skf72(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[59,161]),
[iquote('6:Res:59.2,161.2')] ).
cnf(245,plain,
( ~ odrl_rel(u)
| ~ immunity(skf57(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf57(u,v,w),x)
| equal(skf57(u,v,w),skf72(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[58,161]),
[iquote('6:Res:58.2,161.2')] ).
cnf(233,plain,
( ~ odrl_rel(u)
| ~ power(skf52(v,w,u))
| ~ skP0(v,w,u)
| ~ part_of(skf52(v,w,u),x)
| equal(skf52(v,w,u),skf66(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[57,159]),
[iquote('5:Res:57.2,159.2')] ).
cnf(350,plain,
( ~ obl(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| bearer(skf50(bibliothek,y,z,x1,x2,x3),bibliothek) ),
inference(res,[status(thm),theory(equality)],[8,111]),
[iquote('0:Res:8.0,111.1')] ).
cnf(111,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| bearer(skf50(v,x1,x2,x3,x4,x5),v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(234,plain,
( ~ odrl_rel(u)
| ~ power(skf69(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf69(u,v,w),x)
| equal(skf69(u,v,w),skf66(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[60,159]),
[iquote('5:Res:60.2,159.2')] ).
cnf(235,plain,
( ~ odrl_rel(u)
| ~ power(skf63(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf63(u,v,w),x)
| equal(skf63(u,v,w),skf66(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[59,159]),
[iquote('5:Res:59.2,159.2')] ).
cnf(236,plain,
( ~ odrl_rel(u)
| ~ power(skf57(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf57(u,v,w),x)
| equal(skf57(u,v,w),skf66(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[58,159]),
[iquote('5:Res:58.2,159.2')] ).
cnf(224,plain,
( ~ odrl_rel(u)
| ~ duty(skf52(v,w,u))
| ~ skP0(v,w,u)
| ~ part_of(skf52(v,w,u),x)
| equal(skf52(v,w,u),skf60(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[57,157]),
[iquote('4:Res:57.2,157.2')] ).
cnf(114,axiom,
( ~ perm(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| bearer(skf37(z,v,x,y,u,w),z) ),
file('MGT109+1.p',unknown),
[] ).
cnf(225,plain,
( ~ odrl_rel(u)
| ~ duty(skf69(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf69(u,v,w),x)
| equal(skf69(u,v,w),skf60(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[60,157]),
[iquote('4:Res:60.2,157.2')] ).
cnf(226,plain,
( ~ odrl_rel(u)
| ~ duty(skf63(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf63(u,v,w),x)
| equal(skf63(u,v,w),skf60(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[59,157]),
[iquote('4:Res:59.2,157.2')] ).
cnf(227,plain,
( ~ odrl_rel(u)
| ~ duty(skf57(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf57(u,v,w),x)
| equal(skf57(u,v,w),skf60(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[58,157]),
[iquote('4:Res:58.2,157.2')] ).
cnf(268,plain,
( ~ odrl_rel(u)
| ~ skP2(v,decl(w),u)
| ~ part_of(skf63(u,v,decl(w)),x)
| ~ founds_rem(y,x,z)
| about_event(skf63(u,v,decl(w)),y) ),
inference(mrr,[status(thm)],[262,51]),
[iquote('0:MRR:262.1,51.2')] ).
cnf(115,axiom,
( ~ perm(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| bearer(skf38(y,x,v,z,u,w),v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(217,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ disability(skf57(u,w,x))
| ~ skP1(w,x,u)
| ~ part_of(skf57(u,w,x),v)
| skP3(w,x,v) ),
inference(res,[status(thm),theory(equality)],[58,154]),
[iquote('3:Res:58.2,154.3')] ).
cnf(219,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ subjection(skf57(u,w,x))
| ~ skP1(w,x,u)
| ~ part_of(skf57(u,w,x),v)
| skP2(w,x,v) ),
inference(res,[status(thm),theory(equality)],[58,150]),
[iquote('1:Res:58.2,150.3')] ).
cnf(210,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ disability(skf63(u,w,x))
| ~ skP2(w,x,u)
| ~ part_of(skf63(u,w,x),v)
| skP3(w,x,v) ),
inference(res,[status(thm),theory(equality)],[59,154]),
[iquote('3:Res:59.2,154.3')] ).
cnf(349,plain,
( ~ proh(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| duty(skf44(y,z,x1,x2,x3,x4)) ),
inference(res,[status(thm),theory(equality)],[8,109]),
[iquote('0:Res:8.0,109.1')] ).
cnf(109,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| duty(skf44(x1,x2,x3,x4,x5,x6)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(211,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ right(skf63(u,w,x))
| ~ skP2(w,x,u)
| ~ part_of(skf63(u,w,x),v)
| skP1(w,x,v) ),
inference(res,[status(thm),theory(equality)],[59,152]),
[iquote('2:Res:59.2,152.3')] ).
cnf(204,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ right(skf69(u,w,x))
| ~ skP3(w,x,u)
| ~ part_of(skf69(u,w,x),v)
| skP1(w,x,v) ),
inference(res,[status(thm),theory(equality)],[60,152]),
[iquote('2:Res:60.2,152.3')] ).
cnf(205,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ subjection(skf69(u,w,x))
| ~ skP3(w,x,u)
| ~ part_of(skf69(u,w,x),v)
| skP2(w,x,v) ),
inference(res,[status(thm),theory(equality)],[60,150]),
[iquote('1:Res:60.2,150.3')] ).
cnf(348,plain,
( ~ obl(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| duty(skf50(y,z,x1,x2,x3,x4)) ),
inference(res,[status(thm),theory(equality)],[8,107]),
[iquote('0:Res:8.0,107.1')] ).
cnf(107,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| duty(skf50(x1,x2,x3,x4,x5,x6)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(197,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ disability(skf52(w,x,u))
| ~ skP0(w,x,u)
| ~ part_of(skf52(w,x,u),v)
| skP3(w,x,v) ),
inference(res,[status(thm),theory(equality)],[57,154]),
[iquote('3:Res:57.2,154.3')] ).
cnf(198,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ right(skf52(w,x,u))
| ~ skP0(w,x,u)
| ~ part_of(skf52(w,x,u),v)
| skP1(w,x,v) ),
inference(res,[status(thm),theory(equality)],[57,152]),
[iquote('2:Res:57.2,152.3')] ).
cnf(199,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ subjection(skf52(w,x,u))
| ~ skP0(w,x,u)
| ~ part_of(skf52(w,x,u),v)
| skP2(w,x,v) ),
inference(res,[status(thm),theory(equality)],[57,150]),
[iquote('1:Res:57.2,150.3')] ).
cnf(347,plain,
( ~ proh(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| right(skf43(y,z,x1,x2,x3,x4)) ),
inference(res,[status(thm),theory(equality)],[8,108]),
[iquote('0:Res:8.0,108.1')] ).
cnf(108,axiom,
( ~ proh(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| right(skf43(x1,x2,x3,x4,x5,x6)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(246,plain,
( ~ immunity(skf54(u,v,w))
| ~ skP0(u,v,w)
| ~ part_of(skf54(u,v,w),x)
| equal(skf54(u,v,w),skf72(x,u,v)) ),
inference(res,[status(thm),theory(equality)],[39,161]),
[iquote('6:Res:39.1,161.2')] ).
cnf(248,plain,
( ~ immunity(skf66(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf66(u,v,w),x)
| equal(skf66(u,v,w),skf72(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[41,161]),
[iquote('6:Res:41.1,161.2')] ).
cnf(249,plain,
( ~ immunity(skf60(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf60(u,v,w),x)
| equal(skf60(u,v,w),skf72(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[40,161]),
[iquote('6:Res:40.1,161.2')] ).
cnf(346,plain,
( ~ obl(p1)
| ~ activates(u,p1)
| ~ tgt(p1,v)
| ~ act(p1,w)
| ~ aer(p1,x)
| right(skf49(y,z,x1,x2,x3,x4)) ),
inference(res,[status(thm),theory(equality)],[8,106]),
[iquote('0:Res:8.0,106.1')] ).
cnf(106,axiom,
( ~ obl(u)
| ~ aee(u,v)
| ~ activates(w,u)
| ~ tgt(u,x)
| ~ act(u,y)
| ~ aer(u,z)
| right(skf49(x1,x2,x3,x4,x5,x6)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(237,plain,
( ~ power(skf54(u,v,w))
| ~ skP0(u,v,w)
| ~ part_of(skf54(u,v,w),x)
| equal(skf54(u,v,w),skf66(x,u,v)) ),
inference(res,[status(thm),theory(equality)],[39,159]),
[iquote('5:Res:39.1,159.2')] ).
cnf(238,plain,
( ~ power(skf72(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf72(u,v,w),x)
| equal(skf72(u,v,w),skf66(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[42,159]),
[iquote('5:Res:42.1,159.2')] ).
cnf(240,plain,
( ~ power(skf60(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf60(u,v,w),x)
| equal(skf60(u,v,w),skf66(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[40,159]),
[iquote('5:Res:40.1,159.2')] ).
cnf(228,plain,
( ~ duty(skf54(u,v,w))
| ~ skP0(u,v,w)
| ~ part_of(skf54(u,v,w),x)
| equal(skf54(u,v,w),skf60(x,u,v)) ),
inference(res,[status(thm),theory(equality)],[39,157]),
[iquote('4:Res:39.1,157.2')] ).
cnf(104,axiom,
( ~ has_rem(u)
| ~ proh(u)
| ~ aee(u,v)
| ~ tgt(u,w)
| ~ act(u,x)
| ~ does(v,x,w)
| norm_state_change(v,skf79(u,w,v),w,duty_rem) ),
file('MGT109+1.p',unknown),
[] ).
cnf(229,plain,
( ~ duty(skf72(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf72(u,v,w),x)
| equal(skf72(u,v,w),skf60(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[42,157]),
[iquote('4:Res:42.1,157.2')] ).
cnf(230,plain,
( ~ duty(skf66(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf66(u,v,w),x)
| equal(skf66(u,v,w),skf60(x,v,w)) ),
inference(res,[status(thm),theory(equality)],[41,157]),
[iquote('4:Res:41.1,157.2')] ).
cnf(295,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ skP3(w,x,u)
| ~ part_of(skf69(u,w,x),v)
| equal(skf69(u,w,x),skf69(v,w,x)) ),
inference(mrr,[status(thm)],[288,52]),
[iquote('3:MRR:288.2,52.2')] ).
cnf(286,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ skP1(w,x,u)
| ~ part_of(skf57(u,w,x),v)
| equal(skf57(u,w,x),skf57(v,w,x)) ),
inference(mrr,[status(thm)],[281,50]),
[iquote('2:MRR:281.2,50.2')] ).
cnf(105,axiom,
( ~ disability(u)
| ~ proh(v)
| ~ bearer(u,w)
| ~ tgt(v,x)
| ~ aee(v,y)
| ~ aer(v,w)
| ~ act(v,z)
| ~ cnt(u,z,x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(277,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ skP2(w,x,u)
| ~ part_of(skf63(u,w,x),v)
| equal(skf63(u,w,x),skf63(v,w,x)) ),
inference(mrr,[status(thm)],[271,51]),
[iquote('1:MRR:271.2,51.2')] ).
cnf(259,plain,
( ~ skP2(u,decl(v),w)
| ~ part_of(skf66(w,u,decl(v)),x)
| ~ founds_rem(y,x,z)
| about_event(skf66(w,u,decl(v)),y) ),
inference(mrr,[status(thm)],[257,33]),
[iquote('0:MRR:257.0,33.1')] ).
cnf(319,plain,
( ~ permission(u)
| ~ skP1(v,rfr(w),x)
| ~ bearer(u,y)
| ~ bearer(skf60(x,v,rfr(w)),y)
| ~ cnt(u,w,v) ),
inference(mrr,[status(thm)],[318,32]),
[iquote('0:MRR:318.1,32.1')] ).
cnf(220,plain,
( ~ odrl_rel(u)
| ~ immunity(skf57(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf57(u,v,w),x)
| skP3(v,w,x) ),
inference(res,[status(thm),theory(equality)],[58,160]),
[iquote('6:Res:58.2,160.2')] ).
cnf(103,axiom,
( ~ has_rem(u)
| ~ proh(u)
| ~ aee(u,v)
| ~ tgt(u,w)
| ~ act(u,x)
| ~ does(v,x,w)
| rem_act(u,skf79(u,y,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(221,plain,
( ~ odrl_rel(u)
| ~ power(skf57(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf57(u,v,w),x)
| skP2(v,w,x) ),
inference(res,[status(thm),theory(equality)],[58,158]),
[iquote('5:Res:58.2,158.2')] ).
cnf(222,plain,
( ~ odrl_rel(u)
| ~ duty(skf57(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf57(u,v,w),x)
| skP1(v,w,x) ),
inference(res,[status(thm),theory(equality)],[58,156]),
[iquote('4:Res:58.2,156.2')] ).
cnf(213,plain,
( ~ odrl_rel(u)
| ~ immunity(skf63(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf63(u,v,w),x)
| skP3(v,w,x) ),
inference(res,[status(thm),theory(equality)],[59,160]),
[iquote('6:Res:59.2,160.2')] ).
cnf(214,plain,
( ~ odrl_rel(u)
| ~ power(skf63(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf63(u,v,w),x)
| skP2(v,w,x) ),
inference(res,[status(thm),theory(equality)],[59,158]),
[iquote('5:Res:59.2,158.2')] ).
cnf(102,axiom,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ part_of(v,u)
| ~ cnt(v,w,x)
| skP0(x,w,u)
| cnt(skf53(v,x,w,u),w,x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(215,plain,
( ~ odrl_rel(u)
| ~ duty(skf63(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf63(u,v,w),x)
| skP1(v,w,x) ),
inference(res,[status(thm),theory(equality)],[59,156]),
[iquote('4:Res:59.2,156.2')] ).
cnf(206,plain,
( ~ odrl_rel(u)
| ~ immunity(skf69(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf69(u,v,w),x)
| skP3(v,w,x) ),
inference(res,[status(thm),theory(equality)],[60,160]),
[iquote('6:Res:60.2,160.2')] ).
cnf(207,plain,
( ~ odrl_rel(u)
| ~ power(skf69(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf69(u,v,w),x)
| skP2(v,w,x) ),
inference(res,[status(thm),theory(equality)],[60,158]),
[iquote('5:Res:60.2,158.2')] ).
cnf(208,plain,
( ~ odrl_rel(u)
| ~ duty(skf69(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf69(u,v,w),x)
| skP1(v,w,x) ),
inference(res,[status(thm),theory(equality)],[60,156]),
[iquote('4:Res:60.2,156.2')] ).
cnf(101,axiom,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ part_of(v,u)
| ~ equal(skf53(v,w,x,u),v)
| ~ cnt(v,x,w)
| skP0(w,x,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(200,plain,
( ~ odrl_rel(u)
| ~ immunity(skf52(v,w,u))
| ~ skP0(v,w,u)
| ~ part_of(skf52(v,w,u),x)
| skP3(v,w,x) ),
inference(res,[status(thm),theory(equality)],[57,160]),
[iquote('6:Res:57.2,160.2')] ).
cnf(201,plain,
( ~ odrl_rel(u)
| ~ power(skf52(v,w,u))
| ~ skP0(v,w,u)
| ~ part_of(skf52(v,w,u),x)
| skP2(v,w,x) ),
inference(res,[status(thm),theory(equality)],[57,158]),
[iquote('5:Res:57.2,158.2')] ).
cnf(202,plain,
( ~ odrl_rel(u)
| ~ duty(skf52(v,w,u))
| ~ skP0(v,w,u)
| ~ part_of(skf52(v,w,u),x)
| skP1(v,w,x) ),
inference(res,[status(thm),theory(equality)],[57,156]),
[iquote('4:Res:57.2,156.2')] ).
cnf(187,plain,
( ~ odrl_rel(u)
| ~ disability(skf60(v,w,x))
| ~ skP1(w,x,v)
| ~ part_of(skf60(v,w,x),u)
| skP3(w,x,u) ),
inference(res,[status(thm),theory(equality)],[40,154]),
[iquote('3:Res:40.1,154.3')] ).
cnf(93,axiom,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ part_of(v,u)
| ~ cnt(v,w,x)
| part_of(skf53(v,x,w,u),u)
| skP0(x,w,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(189,plain,
( ~ odrl_rel(u)
| ~ subjection(skf60(v,w,x))
| ~ skP1(w,x,v)
| ~ part_of(skf60(v,w,x),u)
| skP2(w,x,u) ),
inference(res,[status(thm),theory(equality)],[40,150]),
[iquote('1:Res:40.1,150.3')] ).
cnf(180,plain,
( ~ odrl_rel(u)
| ~ disability(skf66(v,w,x))
| ~ skP2(w,x,v)
| ~ part_of(skf66(v,w,x),u)
| skP3(w,x,u) ),
inference(res,[status(thm),theory(equality)],[41,154]),
[iquote('3:Res:41.1,154.3')] ).
cnf(181,plain,
( ~ odrl_rel(u)
| ~ right(skf66(v,w,x))
| ~ skP2(w,x,v)
| ~ part_of(skf66(v,w,x),u)
| skP1(w,x,u) ),
inference(res,[status(thm),theory(equality)],[41,152]),
[iquote('2:Res:41.1,152.3')] ).
cnf(174,plain,
( ~ odrl_rel(u)
| ~ right(skf72(v,w,x))
| ~ skP3(w,x,v)
| ~ part_of(skf72(v,w,x),u)
| skP1(w,x,u) ),
inference(res,[status(thm),theory(equality)],[42,152]),
[iquote('2:Res:42.1,152.3')] ).
cnf(94,axiom,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ part_of(v,u)
| ~ skP0(w,x,u)
| ~ cnt(v,x,w)
| equal(v,skf52(w,x,u)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(175,plain,
( ~ odrl_rel(u)
| ~ subjection(skf72(v,w,x))
| ~ skP3(w,x,v)
| ~ part_of(skf72(v,w,x),u)
| skP2(w,x,u) ),
inference(res,[status(thm),theory(equality)],[42,150]),
[iquote('1:Res:42.1,150.3')] ).
cnf(167,plain,
( ~ odrl_rel(u)
| ~ disability(skf54(v,w,x))
| ~ skP0(v,w,x)
| ~ part_of(skf54(v,w,x),u)
| skP3(v,w,u) ),
inference(res,[status(thm),theory(equality)],[39,154]),
[iquote('3:Res:39.1,154.3')] ).
cnf(168,plain,
( ~ odrl_rel(u)
| ~ right(skf54(v,w,x))
| ~ skP0(v,w,x)
| ~ part_of(skf54(v,w,x),u)
| skP1(v,w,u) ),
inference(res,[status(thm),theory(equality)],[39,152]),
[iquote('2:Res:39.1,152.3')] ).
cnf(169,plain,
( ~ odrl_rel(u)
| ~ subjection(skf54(v,w,x))
| ~ skP0(v,w,x)
| ~ part_of(skf54(v,w,x),u)
| skP2(v,w,u) ),
inference(res,[status(thm),theory(equality)],[39,150]),
[iquote('1:Res:39.1,150.3')] ).
cnf(83,axiom,
( ~ permission(u)
| ~ duty(v)
| ~ bearer(u,w)
| ~ bearer(v,w)
| ~ cnt(u,x,y)
| ~ cnt(v,rfr(x),y) ),
file('MGT109+1.p',unknown),
[] ).
cnf(82,axiom,
( ~ permission(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| skP0(x,w,v)
| cnt(skf55(u,x,w,v),w,x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(190,plain,
( ~ immunity(skf60(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf60(u,v,w),x)
| skP3(v,w,x) ),
inference(res,[status(thm),theory(equality)],[40,160]),
[iquote('6:Res:40.1,160.2')] ).
cnf(191,plain,
( ~ power(skf60(u,v,w))
| ~ skP1(v,w,u)
| ~ part_of(skf60(u,v,w),x)
| skP2(v,w,x) ),
inference(res,[status(thm),theory(equality)],[40,158]),
[iquote('5:Res:40.1,158.2')] ).
cnf(183,plain,
( ~ immunity(skf66(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf66(u,v,w),x)
| skP3(v,w,x) ),
inference(res,[status(thm),theory(equality)],[41,160]),
[iquote('6:Res:41.1,160.2')] ).
cnf(81,axiom,
( ~ permission(u)
| ~ part_of(u,v)
| ~ equal(skf55(u,w,x,v),u)
| ~ cnt(u,x,w)
| skP0(w,x,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(185,plain,
( ~ duty(skf66(u,v,w))
| ~ skP2(v,w,u)
| ~ part_of(skf66(u,v,w),x)
| skP1(v,w,x) ),
inference(res,[status(thm),theory(equality)],[41,156]),
[iquote('4:Res:41.1,156.2')] ).
cnf(177,plain,
( ~ power(skf72(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf72(u,v,w),x)
| skP2(v,w,x) ),
inference(res,[status(thm),theory(equality)],[42,158]),
[iquote('5:Res:42.1,158.2')] ).
cnf(178,plain,
( ~ duty(skf72(u,v,w))
| ~ skP3(v,w,u)
| ~ part_of(skf72(u,v,w),x)
| skP1(v,w,x) ),
inference(res,[status(thm),theory(equality)],[42,156]),
[iquote('4:Res:42.1,156.2')] ).
cnf(170,plain,
( ~ immunity(skf54(u,v,w))
| ~ skP0(u,v,w)
| ~ part_of(skf54(u,v,w),x)
| skP3(u,v,x) ),
inference(res,[status(thm),theory(equality)],[39,160]),
[iquote('6:Res:39.1,160.2')] ).
cnf(73,axiom,
( ~ permission(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| part_of(skf55(u,x,w,v),v)
| skP0(x,w,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(171,plain,
( ~ power(skf54(u,v,w))
| ~ skP0(u,v,w)
| ~ part_of(skf54(u,v,w),x)
| skP2(u,v,x) ),
inference(res,[status(thm),theory(equality)],[39,158]),
[iquote('5:Res:39.1,158.2')] ).
cnf(172,plain,
( ~ duty(skf54(u,v,w))
| ~ skP0(u,v,w)
| ~ part_of(skf54(u,v,w),x)
| skP1(u,v,x) ),
inference(res,[status(thm),theory(equality)],[39,156]),
[iquote('4:Res:39.1,156.2')] ).
cnf(223,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ skP1(w,x,u)
| ~ part_of(skf57(u,w,x),v)
| skP1(w,x,v) ),
inference(mrr,[status(thm)],[218,50]),
[iquote('2:MRR:218.2,50.2')] ).
cnf(216,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ skP2(w,x,u)
| ~ part_of(skf63(u,w,x),v)
| skP2(w,x,v) ),
inference(mrr,[status(thm)],[212,51]),
[iquote('1:MRR:212.2,51.2')] ).
cnf(74,axiom,
( ~ permission(u)
| ~ part_of(u,v)
| ~ skP0(w,x,v)
| ~ cnt(u,x,w)
| equal(u,skf54(w,x,v)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(209,plain,
( ~ odrl_rel(u)
| ~ odrl_rel(v)
| ~ skP3(w,x,u)
| ~ part_of(skf69(u,w,x),v)
| skP3(w,x,v) ),
inference(mrr,[status(thm)],[203,52]),
[iquote('3:MRR:203.2,52.2')] ).
cnf(250,plain,
( ~ skP3(u,v,w)
| ~ part_of(skf72(w,u,v),x)
| equal(skf72(w,u,v),skf72(x,u,v)) ),
inference(mrr,[status(thm)],[247,34]),
[iquote('6:MRR:247.0,34.1')] ).
cnf(241,plain,
( ~ skP2(u,v,w)
| ~ part_of(skf66(w,u,v),x)
| equal(skf66(w,u,v),skf66(x,u,v)) ),
inference(mrr,[status(thm)],[239,33]),
[iquote('5:MRR:239.0,33.1')] ).
cnf(232,plain,
( ~ skP1(u,v,w)
| ~ part_of(skf60(w,u,v),x)
| equal(skf60(w,u,v),skf60(x,u,v)) ),
inference(mrr,[status(thm)],[231,32]),
[iquote('4:MRR:231.0,32.1')] ).
cnf(155,plain,
( ~ odrl_rel(u)
| ~ disability(v)
| ~ part_of(v,u)
| ~ cnt(v,w,x)
| equal(v,skf69(u,x,w)) ),
inference(mrr,[status(thm)],[88,154]),
[iquote('3:MRR:88.3,154.4')] ).
cnf(153,plain,
( ~ odrl_rel(u)
| ~ right(v)
| ~ part_of(v,u)
| ~ cnt(v,w,x)
| equal(v,skf57(u,x,w)) ),
inference(mrr,[status(thm)],[92,152]),
[iquote('2:MRR:92.3,152.4')] ).
cnf(151,plain,
( ~ odrl_rel(u)
| ~ subjection(v)
| ~ part_of(v,u)
| ~ cnt(v,w,x)
| equal(v,skf63(u,x,w)) ),
inference(mrr,[status(thm)],[90,150]),
[iquote('1:MRR:90.3,150.4')] ).
cnf(62,axiom,
( ~ subjection(u)
| ~ part_of(u,v)
| ~ founds_rem(w,v,x)
| ~ cnt(u,decl(y),z)
| about_event(u,w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(63,axiom,
( ~ power(u)
| ~ part_of(u,v)
| ~ founds_rem(w,v,x)
| ~ cnt(u,decl(y),z)
| about_event(u,w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(161,plain,
( ~ immunity(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| equal(u,skf72(v,x,w)) ),
inference(mrr,[status(thm)],[68,160]),
[iquote('6:MRR:68.2,160.3')] ).
cnf(159,plain,
( ~ power(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| equal(u,skf66(v,x,w)) ),
inference(mrr,[status(thm)],[70,158]),
[iquote('5:MRR:70.2,158.3')] ).
cnf(157,plain,
( ~ duty(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| equal(u,skf60(v,x,w)) ),
inference(mrr,[status(thm)],[72,156]),
[iquote('4:MRR:72.2,156.3')] ).
cnf(193,plain,
( ~ skP1(u,v,w)
| ~ part_of(skf60(w,u,v),x)
| skP1(u,v,x) ),
inference(mrr,[status(thm)],[192,32]),
[iquote('4:MRR:192.0,32.1')] ).
cnf(186,plain,
( ~ skP2(u,v,w)
| ~ part_of(skf66(w,u,v),x)
| skP2(u,v,x) ),
inference(mrr,[status(thm)],[184,33]),
[iquote('5:MRR:184.0,33.1')] ).
cnf(61,axiom,
( ~ norm_state_change(u,v,w,x)
| triggers(skf74(x,w,v,u),u,v,w,x) ),
file('MGT109+1.p',unknown),
[] ).
cnf(179,plain,
( ~ skP3(u,v,w)
| ~ part_of(skf72(w,u,v),x)
| skP3(u,v,x) ),
inference(mrr,[status(thm)],[176,34]),
[iquote('6:MRR:176.0,34.1')] ).
cnf(58,axiom,
( ~ odrl_rel(u)
| ~ skP1(v,w,u)
| cnt(skf57(u,v,w),w,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ odrl_rel(u)
| ~ skP2(v,w,u)
| cnt(skf63(u,v,w),w,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ odrl_rel(u)
| ~ skP3(v,w,u)
| cnt(skf69(u,v,w),w,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ odrl_rel(u)
| ~ skP0(v,w,u)
| cnt(skf52(v,w,u),w,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ odrl_rel(u)
| ~ skP1(v,w,u)
| part_of(skf57(u,x,y),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ odrl_rel(u)
| ~ skP2(v,w,u)
| part_of(skf63(u,x,y),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ odrl_rel(u)
| ~ skP3(v,w,u)
| part_of(skf69(u,x,y),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ odrl_rel(u)
| ~ skP0(v,w,u)
| part_of(skf52(v,w,u),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ founds(u,v,w)
| ~ founds(u,x,w)
| equal(x,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ founds(u,v,w)
| ~ founds(x,v,w)
| equal(x,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ founds_rem(u,v,w)
| ~ founds_rem(u,x,w)
| equal(x,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(47,axiom,
( ~ founds_rem(u,v,w)
| ~ founds_rem(x,v,w)
| equal(x,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(48,axiom,
( ~ founds_imm(u,v,w)
| ~ founds_imm(u,x,w)
| equal(x,v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ founds_imm(u,v,w)
| ~ founds_imm(x,v,w)
| equal(x,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ odrl_rel(u)
| ~ skP2(v,w,u)
| subjection(skf63(x,y,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ odrl_rel(u)
| ~ skP1(v,w,u)
| right(skf57(x,y,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(194,plain,
( ~ norm_state_change(u,v,w,x)
| bearer(skf76(y),skf77(y)) ),
inference(ems,[status(thm)],[165,43]),
[iquote('0:EmS:165.0,43.1')] ).
cnf(195,plain,
( ~ norm_state_change(u,v,w,x)
| power(skf78(y,z)) ),
inference(ems,[status(thm)],[164,43]),
[iquote('0:EmS:164.0,43.1')] ).
cnf(52,axiom,
( ~ odrl_rel(u)
| ~ skP3(v,w,u)
| disability(skf69(x,y,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(196,plain,
( ~ norm_state_change(u,v,w,x)
| subjection(skf76(y)) ),
inference(ems,[status(thm)],[162,43]),
[iquote('0:EmS:162.0,43.1')] ).
cnf(43,axiom,
( ~ norm_state_change(u,v,w,x)
| inst_event(skf74(y,z,x1,x2)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ skP1(u,v,w)
| cnt(skf60(w,u,v),v,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ skP2(u,v,w)
| cnt(skf66(w,u,v),v,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ skP3(u,v,w)
| cnt(skf72(w,u,v),v,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ skP0(u,v,w)
| cnt(skf54(u,v,w),v,u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ skP1(u,v,w)
| part_of(skf60(w,x,y),w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(37,axiom,
( ~ skP2(u,v,w)
| part_of(skf66(w,x,y),w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ skP3(u,v,w)
| part_of(skf72(w,x,y),w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ skP0(u,v,w)
| part_of(skf54(u,v,w),w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ skP1(u,v,w)
| duty(skf60(x,y,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ skP2(u,v,w)
| power(skf66(x,y,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ skP3(u,v,w)
| immunity(skf72(x,y,z)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ proh(u)
| ~ founds(v,w,u)
| odrl_rel(w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(27,axiom,
( ~ perm(u)
| ~ founds(v,w,u)
| odrl_rel(w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ obl(u)
| ~ founds(v,w,u)
| odrl_rel(w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ proh(u)
| ~ founds_rem(v,w,u)
| odrl_rel(w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(31,axiom,
( ~ perm(u)
| ~ founds_imm(v,w,u)
| odrl_rel(w) ),
file('MGT109+1.p',unknown),
[] ).
cnf(166,plain,
( ~ inst_event(u)
| about_event(skf78(u,v),u) ),
inference(res,[status(thm),theory(equality)],[18,26]),
[iquote('0:Res:18.1,26.0')] ).
cnf(26,axiom,
( ~ competent_for(u,v)
| about_event(skf78(v,w),v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ competent_for(u,v)
| bearer(skf78(v,u),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(165,plain,
( ~ inst_event(u)
| bearer(skf76(v),skf77(v)) ),
inference(res,[status(thm),theory(equality)],[18,24]),
[iquote('0:Res:18.1,24.0')] ).
cnf(24,axiom,
( ~ competent_for(u,v)
| bearer(skf76(w),skf77(w)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(20,axiom,
permission(skf38(u,v,w,x,y,z)),
file('MGT109+1.p',unknown),
[] ).
cnf(21,axiom,
no_right(skf37(u,v,w,x,y,z)),
file('MGT109+1.p',unknown),
[] ).
cnf(164,plain,
( ~ inst_event(u)
| power(skf78(v,w)) ),
inference(res,[status(thm),theory(equality)],[18,23]),
[iquote('0:Res:18.1,23.0')] ).
cnf(23,axiom,
( ~ competent_for(u,v)
| power(skf78(w,x)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(163,plain,
( ~ inst_event(u)
| about_event(skf76(u),u) ),
inference(res,[status(thm),theory(equality)],[18,22]),
[iquote('0:Res:18.1,22.0')] ).
cnf(162,plain,
( ~ inst_event(u)
| subjection(skf76(v)) ),
inference(res,[status(thm),theory(equality)],[18,19]),
[iquote('0:Res:18.1,19.0')] ).
cnf(22,axiom,
( ~ competent_for(u,v)
| about_event(skf76(v),v) ),
file('MGT109+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ competent_for(u,v)
| subjection(skf76(w)) ),
file('MGT109+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ inst_event(u)
| competent_for(skf75(u),u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(16,axiom,
permission(skf55(u,v,w,x)),
file('MGT109+1.p',unknown),
[] ).
cnf(17,axiom,
no_right(skf53(u,v,w,x)),
file('MGT109+1.p',unknown),
[] ).
cnf(13,axiom,
permission(skf54(u,v,w)),
file('MGT109+1.p',unknown),
[] ).
cnf(14,axiom,
no_right(skf52(u,v,w)),
file('MGT109+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ odrl_rel(u)
| legal_relator(u) ),
file('MGT109+1.p',unknown),
[] ).
cnf(8,axiom,
aee(p1,bibliothek),
file('MGT109+1.p',unknown),
[] ).
cnf(10,axiom,
act(p1,read),
file('MGT109+1.p',unknown),
[] ).
cnf(11,axiom,
tgt(p1,theater_ds),
file('MGT109+1.p',unknown),
[] ).
cnf(9,axiom,
aer(p1,ensemble),
file('MGT109+1.p',unknown),
[] ).
cnf(12,axiom,
activates(e1,p1),
file('MGT109+1.p',unknown),
[] ).
cnf(7,axiom,
perm(p1),
file('MGT109+1.p',unknown),
[] ).
cnf(1,axiom,
agent(bibliothek),
file('MGT109+1.p',unknown),
[] ).
cnf(2,axiom,
agent(ensemble),
file('MGT109+1.p',unknown),
[] ).
cnf(3,axiom,
action(read),
file('MGT109+1.p',unknown),
[] ).
cnf(4,axiom,
target(theater_ds),
file('MGT109+1.p',unknown),
[] ).
cnf(5,axiom,
rule(p1),
file('MGT109+1.p',unknown),
[] ).
cnf(6,axiom,
event(e1),
file('MGT109+1.p',unknown),
[] ).
cnf(160,plain,
( ~ immunity(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| skP3(x,w,v) ),
inference(spt,[],[64]),
[iquote('6:Spt:64.0,64.1,64.2,64.4')] ).
cnf(158,plain,
( ~ power(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| skP2(x,w,v) ),
inference(spt,[],[65]),
[iquote('5:Spt:65.0,65.1,65.2,65.4')] ).
cnf(156,plain,
( ~ duty(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| skP1(x,w,v) ),
inference(spt,[],[66]),
[iquote('4:Spt:66.0,66.1,66.2,66.4')] ).
cnf(154,plain,
( ~ odrl_rel(u)
| ~ disability(v)
| ~ part_of(v,u)
| ~ cnt(v,w,x)
| skP3(x,w,u) ),
inference(spt,[],[84]),
[iquote('3:Spt:84.0,84.1,84.2,84.3,84.5')] ).
cnf(152,plain,
( ~ odrl_rel(u)
| ~ right(v)
| ~ part_of(v,u)
| ~ cnt(v,w,x)
| skP1(x,w,u) ),
inference(spt,[],[86]),
[iquote('2:Spt:86.0,86.1,86.2,86.3,86.5')] ).
cnf(150,plain,
( ~ odrl_rel(u)
| ~ subjection(v)
| ~ part_of(v,u)
| ~ cnt(v,w,x)
| skP2(x,w,u) ),
inference(spt,[],[85]),
[iquote('1:Spt:85.0,85.1,85.2,85.3,85.5')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT109+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 14:01:41 UTC 2026
% 0.02/0.36 % CPUTime :
% 1.35/1.66
% 1.35/1.66 SPASS V 3.9
% 1.35/1.66 SPASS beiseite: Completion found.
% 1.35/1.66 % SZS status CounterSatisfiable
% 1.35/1.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.35/1.66 SPASS derived 270 clauses, backtracked 0 clauses, performed 6 splits and kept 396 clauses.
% 1.35/1.66 SPASS allocated 103443 KBytes.
% 1.35/1.66 SPASS spent 0:00:01.29 on the problem.
% 1.35/1.66 0:00:00.06 for the input.
% 1.35/1.66 0:00:00.97 for the FLOTTER CNF translation.
% 1.35/1.66 0:00:00.02 for inferences.
% 1.35/1.66 0:00:00.00 for the backtracking.
% 1.35/1.66 0:00:00.15 for the reduction.
% 1.35/1.66
% 1.35/1.66
% 1.35/1.66 The saturated set of worked-off clauses is :
% 1.35/1.66 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------