%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n004.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:03 AM UTC 2026
% Result : Unsatisfiable 0.21s 0.54s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 23
% Syntax : Number of clauses : 53 ( 24 unt; 6 nHn; 53 RR)
% Number of literals : 146 ( 0 equ; 87 neg)
% Maximal clause size : 9 ( 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; 10 con; 0-4 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
position(l),
file('MGT114+1.p',unknown),
[] ).
cnf(2,axiom,
position(n1),
file('MGT114+1.p',unknown),
[] ).
cnf(3,axiom,
position(n2),
file('MGT114+1.p',unknown),
[] ).
cnf(4,axiom,
legal_relator(rho1),
file('MGT114+1.p',unknown),
[] ).
cnf(5,axiom,
odrl_rel(rho1),
file('MGT114+1.p',unknown),
[] ).
cnf(6,axiom,
permission(l),
file('MGT114+1.p',unknown),
[] ).
cnf(7,axiom,
no_right(n1),
file('MGT114+1.p',unknown),
[] ).
cnf(8,axiom,
no_right(n2),
file('MGT114+1.p',unknown),
[] ).
cnf(9,axiom,
action(some_action),
file('MGT114+1.p',unknown),
[] ).
cnf(10,axiom,
target(some_target),
file('MGT114+1.p',unknown),
[] ).
cnf(11,axiom,
part_of(l,rho1),
file('MGT114+1.p',unknown),
[] ).
cnf(12,axiom,
part_of(n1,rho1),
file('MGT114+1.p',unknown),
[] ).
cnf(13,axiom,
part_of(n2,rho1),
file('MGT114+1.p',unknown),
[] ).
cnf(14,axiom,
cnt(l,some_action,some_target),
file('MGT114+1.p',unknown),
[] ).
cnf(15,axiom,
cnt(n1,some_action,some_target),
file('MGT114+1.p',unknown),
[] ).
cnf(16,axiom,
cnt(n2,some_action,some_target),
file('MGT114+1.p',unknown),
[] ).
cnf(17,axiom,
~ equal(n2,n1),
file('MGT114+1.p',unknown),
[] ).
cnf(20,axiom,
permission(skf7(u,v,w,x)),
file('MGT114+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ permission(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| equal(u,l) ),
file('MGT114+1.p',unknown),
[] ).
cnf(27,axiom,
( ~ permission(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| part_of(skf7(u,x,w,v),v)
| skP0(x,w,v) ),
file('MGT114+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ permission(u)
| ~ part_of(u,v)
| ~ equal(skf7(u,w,x,v),u)
| ~ cnt(u,x,w)
| skP0(w,x,v) ),
file('MGT114+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ permission(u)
| ~ part_of(u,v)
| ~ cnt(u,w,x)
| skP0(x,w,v)
| cnt(skf7(u,x,w,v),w,x) ),
file('MGT114+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ odrl_rel(u)
| ~ no_right(v)
| ~ part_of(v,u)
| ~ skP0(w,x,u)
| ~ cnt(v,x,w)
| equal(v,skf4(w,x,u)) ),
file('MGT114+1.p',unknown),
[] ).
cnf(53,plain,
( ~ permission(u)
| ~ permission(skf7(u,some_target,some_action,v))
| ~ part_of(u,v)
| ~ cnt(u,some_action,some_target)
| ~ part_of(skf7(u,some_target,some_action,v),rho1)
| skP0(some_target,some_action,v)
| equal(skf7(u,some_target,some_action,v),l) ),
inference(res,[status(thm),theory(equality)],[30,26]),
[iquote('0:Res:30.4,26.2')] ).
cnf(54,plain,
( ~ permission(u)
| ~ part_of(u,v)
| ~ cnt(u,some_action,some_target)
| ~ part_of(skf7(u,some_target,some_action,v),rho1)
| skP0(some_target,some_action,v)
| equal(skf7(u,some_target,some_action,v),l) ),
inference(ssi,[status(thm)],[53,20,10,9]),
[iquote('0:SSi:53.1,20.0,10.0,9.0')] ).
cnf(56,plain,
( ~ permission(u)
| ~ permission(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| skP0(some_target,some_action,rho1)
| skP0(some_target,some_action,rho1)
| equal(skf7(u,some_target,some_action,rho1),l) ),
inference(res,[status(thm),theory(equality)],[27,54]),
[iquote('0:Res:27.3,54.3')] ).
cnf(57,plain,
( ~ permission(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| skP0(some_target,some_action,rho1)
| equal(skf7(u,some_target,some_action,rho1),l) ),
inference(obv,[status(thm),theory(equality)],[56]),
[iquote('0:Obv:56.6')] ).
cnf(58,plain,
( ~ permission(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| equal(skf7(u,some_target,some_action,rho1),l) ),
inference(spt,[spt(split,[position(s1)])],[57]),
[iquote('1:Spt:57.0,57.1,57.2,57.4')] ).
cnf(63,plain,
( ~ permission(u)
| ~ permission(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| ~ part_of(u,rho1)
| ~ equal(l,u)
| ~ cnt(u,some_action,some_target)
| skP0(some_target,some_action,rho1) ),
inference(spl,[status(thm),theory(equality)],[58,29]),
[iquote('1:SpL:58.3,29.2')] ).
cnf(66,plain,
( ~ permission(u)
| ~ part_of(u,rho1)
| ~ equal(l,u)
| ~ cnt(u,some_action,some_target)
| skP0(some_target,some_action,rho1) ),
inference(obv,[status(thm),theory(equality)],[63]),
[iquote('1:Obv:63.3')] ).
cnf(71,plain,
( ~ permission(l)
| ~ part_of(l,rho1)
| ~ equal(l,l)
| skP0(some_target,some_action,rho1) ),
inference(res,[status(thm),theory(equality)],[14,66]),
[iquote('1:Res:14.0,66.3')] ).
cnf(82,plain,
( ~ permission(l)
| ~ part_of(l,rho1)
| skP0(some_target,some_action,rho1) ),
inference(obv,[status(thm),theory(equality)],[71]),
[iquote('1:Obv:71.2')] ).
cnf(83,plain,
( ~ part_of(l,rho1)
| skP0(some_target,some_action,rho1) ),
inference(ssi,[status(thm)],[82,1,6]),
[iquote('1:SSi:82.0,1.0,6.0')] ).
cnf(84,plain,
skP0(some_target,some_action,rho1),
inference(mrr,[status(thm)],[83,11]),
[iquote('1:MRR:83.0,11.0')] ).
cnf(86,plain,
( ~ odrl_rel(rho1)
| ~ no_right(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| equal(u,skf4(some_target,some_action,rho1)) ),
inference(res,[status(thm),theory(equality)],[84,32]),
[iquote('1:Res:84.0,32.3')] ).
cnf(89,plain,
( ~ no_right(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| equal(u,skf4(some_target,some_action,rho1)) ),
inference(ssi,[status(thm)],[86,4,5]),
[iquote('1:SSi:86.0,4.0,5.0')] ).
cnf(95,plain,
( ~ no_right(n2)
| ~ part_of(n2,rho1)
| equal(skf4(some_target,some_action,rho1),n2) ),
inference(res,[status(thm),theory(equality)],[16,89]),
[iquote('1:Res:16.0,89.2')] ).
cnf(96,plain,
( ~ no_right(n1)
| ~ part_of(n1,rho1)
| equal(skf4(some_target,some_action,rho1),n1) ),
inference(res,[status(thm),theory(equality)],[15,89]),
[iquote('1:Res:15.0,89.2')] ).
cnf(102,plain,
( ~ part_of(n2,rho1)
| equal(skf4(some_target,some_action,rho1),n2) ),
inference(ssi,[status(thm)],[95,3,8]),
[iquote('1:SSi:95.0,3.0,8.0')] ).
cnf(103,plain,
equal(skf4(some_target,some_action,rho1),n2),
inference(mrr,[status(thm)],[102,13]),
[iquote('1:MRR:102.0,13.0')] ).
cnf(105,plain,
( ~ no_right(n1)
| ~ part_of(n1,rho1)
| equal(n2,n1) ),
inference(rew,[status(thm),theory(equality)],[103,96]),
[iquote('1:Rew:103.0,96.2')] ).
cnf(106,plain,
( ~ part_of(n1,rho1)
| equal(n2,n1) ),
inference(ssi,[status(thm)],[105,2,7]),
[iquote('1:SSi:105.0,2.0,7.0')] ).
cnf(107,plain,
$false,
inference(mrr,[status(thm)],[106,12,17]),
[iquote('1:MRR:106.0,106.1,12.0,17.0')] ).
cnf(120,plain,
skP0(some_target,some_action,rho1),
inference(spt,[spt(split,[position(s2)])],[57]),
[iquote('1:Spt:107.0,57.3')] ).
cnf(122,plain,
( ~ odrl_rel(rho1)
| ~ no_right(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| equal(u,skf4(some_target,some_action,rho1)) ),
inference(res,[status(thm),theory(equality)],[120,32]),
[iquote('1:Res:120.0,32.3')] ).
cnf(125,plain,
( ~ no_right(u)
| ~ part_of(u,rho1)
| ~ cnt(u,some_action,some_target)
| equal(u,skf4(some_target,some_action,rho1)) ),
inference(ssi,[status(thm)],[122,4,5]),
[iquote('1:SSi:122.0,4.0,5.0')] ).
cnf(131,plain,
( ~ no_right(n2)
| ~ part_of(n2,rho1)
| equal(skf4(some_target,some_action,rho1),n2) ),
inference(res,[status(thm),theory(equality)],[16,125]),
[iquote('1:Res:16.0,125.2')] ).
cnf(132,plain,
( ~ no_right(n1)
| ~ part_of(n1,rho1)
| equal(skf4(some_target,some_action,rho1),n1) ),
inference(res,[status(thm),theory(equality)],[15,125]),
[iquote('1:Res:15.0,125.2')] ).
cnf(138,plain,
( ~ part_of(n2,rho1)
| equal(skf4(some_target,some_action,rho1),n2) ),
inference(ssi,[status(thm)],[131,3,8]),
[iquote('1:SSi:131.0,3.0,8.0')] ).
cnf(139,plain,
equal(skf4(some_target,some_action,rho1),n2),
inference(mrr,[status(thm)],[138,13]),
[iquote('1:MRR:138.0,13.0')] ).
cnf(141,plain,
( ~ no_right(n1)
| ~ part_of(n1,rho1)
| equal(n2,n1) ),
inference(rew,[status(thm),theory(equality)],[139,132]),
[iquote('1:Rew:139.0,132.2')] ).
cnf(142,plain,
( ~ part_of(n1,rho1)
| equal(n2,n1) ),
inference(ssi,[status(thm)],[141,2,7]),
[iquote('1:SSi:141.0,2.0,7.0')] ).
cnf(143,plain,
$false,
inference(mrr,[status(thm)],[142,12,17]),
[iquote('1:MRR:142.0,142.1,12.0,17.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.11/0.37 % Computer : n004.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 7 14:07:45 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.21/0.54
% 0.21/0.54 SPASS V 3.9
% 0.21/0.54 SPASS beiseite: Proof found.
% 0.21/0.54 % SZS status Theorem
% 0.21/0.54 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.54 SPASS derived 63 clauses, backtracked 4 clauses, performed 1 splits and kept 74 clauses.
% 0.21/0.54 SPASS allocated 97772 KBytes.
% 0.21/0.54 SPASS spent 0:00:00.16 on the problem.
% 0.21/0.54 0:00:00.06 for the input.
% 0.21/0.54 0:00:00.05 for the FLOTTER CNF translation.
% 0.21/0.54 0:00:00.00 for inferences.
% 0.21/0.54 0:00:00.00 for the backtracking.
% 0.21/0.54 0:00:00.01 for the reduction.
% 0.21/0.54
% 0.21/0.54
% 0.21/0.54 Here is a proof with depth 7, length 53 :
% 0.21/0.54 % SZS output start Refutation
% See solution above
% 0.21/0.54 Formulae used in the proof : pos_l pos_n1 pos_n2 rel_rho1 odrl_rho1 permission_l no_right_n1 no_right_n2 action_typed target_typed partof_l partof_n1 partof_n2 cnt_l cnt_n1 cnt_n2 n1_neq_n2 ax_correlativity_permission perm_l_unique
% 0.21/0.54
%------------------------------------------------------------------------------