%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n003.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:03:08 AM UTC 2026
% Result : Unsatisfiable 9.89s 4.10s
% Output : CNFRefutation 10.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 13
% Syntax : Number of formulae : 71 ( 30 unt; 0 typ; 0 def)
% Number of atoms : 303 ( 61 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 425 ( 193 ~; 215 |; 12 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-4 aty)
% Number of variables : 73 ( 71 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ cnt > part_of > target > position > permission > odrl_rel > no_right > legal_relator > action > #nlpp > some_target > some_action > rho1 > n2 > n1 > l > #skF_4 > #skF_2 > #skF_3 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(odrl_rel,type,
odrl_rel: $i > $o ).
tff(no_right,type,
no_right: $i > $o ).
tff(l,type,
l: $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i ) > $i ).
tff(part_of,type,
part_of: ( $i * $i ) > $o ).
tff(cnt,type,
cnt: ( $i * $i * $i ) > $o ).
tff(n1,type,
n1: $i ).
tff(rho1,type,
rho1: $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $i ).
tff(position,type,
position: $i > $o ).
tff(target,type,
target: $i > $o ).
tff(some_action,type,
some_action: $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i * $i ) > $i ).
tff(n2,type,
n2: $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i * $i * $i ) > $i ).
tff(legal_relator,type,
legal_relator: $i > $o ).
tff(action,type,
action: $i > $o ).
tff(some_target,type,
some_target: $i ).
tff(permission,type,
permission: $i > $o ).
tff(f_81,axiom,
n1 != n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n1_neq_n2) ).
tff(f_70,axiom,
no_right(n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_right_n1) ).
tff(f_73,axiom,
part_of(n1,rho1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',partof_n1) ).
tff(f_76,axiom,
cnt(n1,some_action,some_target),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cnt_n1) ).
tff(f_68,axiom,
odrl_rel(rho1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',odrl_rho1) ).
tff(f_69,axiom,
permission(l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permission_l) ).
tff(f_72,axiom,
part_of(l,rho1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',partof_l) ).
tff(f_75,axiom,
cnt(l,some_action,some_target),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cnt_l) ).
tff(f_74,axiom,
part_of(n2,rho1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',partof_n2) ).
tff(f_71,axiom,
no_right(n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_right_n2) ).
tff(f_77,axiom,
cnt(n2,some_action,some_target),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cnt_n2) ).
tff(f_62,axiom,
! [Rho,A,T] :
( odrl_rel(Rho)
=> ( ? [L] :
( permission(L)
& part_of(L,Rho)
& cnt(L,A,T)
& ! [L2] :
( ( permission(L2)
& part_of(L2,Rho)
& cnt(L2,A,T) )
=> ( L2 = L ) ) )
<=> ? [N] :
( no_right(N)
& part_of(N,Rho)
& cnt(N,A,T)
& ! [M] :
( ( no_right(M)
& part_of(M,Rho)
& cnt(M,A,T) )
=> ( M = N ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_correlativity_permission) ).
tff(f_89,axiom,
! [L2] :
( ( permission(L2)
& part_of(L2,rho1)
& cnt(L2,some_action,some_target) )
=> ( L2 = l ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',perm_l_unique) ).
tff(c_98,plain,
n2 != n1,
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_78,plain,
no_right(n1),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_84,plain,
part_of(n1,rho1),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_90,plain,
cnt(n1,some_action,some_target),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_74,plain,
odrl_rel(rho1),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_76,plain,
permission(l),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_82,plain,
part_of(l,rho1),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_88,plain,
cnt(l,some_action,some_target),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_86,plain,
part_of(n2,rho1),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_80,plain,
no_right(n2),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_92,plain,
cnt(n2,some_action,some_target),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_360,plain,
! [M_155,T_159,Rho_156,A_157,L_158] :
( part_of('#skF_1'(Rho_156,A_157,T_159,L_158),Rho_156)
| ( M_155 = '#skF_2'(Rho_156,A_157,T_159) )
| ~ cnt(M_155,A_157,T_159)
| ~ part_of(M_155,Rho_156)
| ~ no_right(M_155)
| ~ cnt(L_158,A_157,T_159)
| ~ part_of(L_158,Rho_156)
| ~ permission(L_158)
| ~ odrl_rel(Rho_156) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_390,plain,
! [Rho_156,L_158] :
( part_of('#skF_1'(Rho_156,some_action,some_target,L_158),Rho_156)
| ( '#skF_2'(Rho_156,some_action,some_target) = n2 )
| ~ part_of(n2,Rho_156)
| ~ no_right(n2)
| ~ cnt(L_158,some_action,some_target)
| ~ part_of(L_158,Rho_156)
| ~ permission(L_158)
| ~ odrl_rel(Rho_156) ),
inference(resolution,[status(thm)],[c_92,c_360]) ).
tff(c_409,plain,
! [Rho_156,L_158] :
( part_of('#skF_1'(Rho_156,some_action,some_target,L_158),Rho_156)
| ( '#skF_2'(Rho_156,some_action,some_target) = n2 )
| ~ part_of(n2,Rho_156)
| ~ cnt(L_158,some_action,some_target)
| ~ part_of(L_158,Rho_156)
| ~ permission(L_158)
| ~ odrl_rel(Rho_156) ),
inference(demodulation,[status(thm),theory(equality)],[c_80,c_390]) ).
tff(c_411,plain,
! [L_165,M_162,A_164,Rho_163,T_166] :
( cnt('#skF_1'(Rho_163,A_164,T_166,L_165),A_164,T_166)
| ( M_162 = '#skF_2'(Rho_163,A_164,T_166) )
| ~ cnt(M_162,A_164,T_166)
| ~ part_of(M_162,Rho_163)
| ~ no_right(M_162)
| ~ cnt(L_165,A_164,T_166)
| ~ part_of(L_165,Rho_163)
| ~ permission(L_165)
| ~ odrl_rel(Rho_163) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_441,plain,
! [Rho_163,L_165] :
( cnt('#skF_1'(Rho_163,some_action,some_target,L_165),some_action,some_target)
| ( '#skF_2'(Rho_163,some_action,some_target) = n2 )
| ~ part_of(n2,Rho_163)
| ~ no_right(n2)
| ~ cnt(L_165,some_action,some_target)
| ~ part_of(L_165,Rho_163)
| ~ permission(L_165)
| ~ odrl_rel(Rho_163) ),
inference(resolution,[status(thm)],[c_92,c_411]) ).
tff(c_482,plain,
! [Rho_171,L_172] :
( cnt('#skF_1'(Rho_171,some_action,some_target,L_172),some_action,some_target)
| ( '#skF_2'(Rho_171,some_action,some_target) = n2 )
| ~ part_of(n2,Rho_171)
| ~ cnt(L_172,some_action,some_target)
| ~ part_of(L_172,Rho_171)
| ~ permission(L_172)
| ~ odrl_rel(Rho_171) ),
inference(demodulation,[status(thm),theory(equality)],[c_80,c_441]) ).
tff(c_100,plain,
! [L2_24] :
( ( l = L2_24 )
| ~ cnt(L2_24,some_action,some_target)
| ~ part_of(L2_24,rho1)
| ~ permission(L2_24) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_1062,plain,
! [Rho_216,L_217] :
( ( '#skF_1'(Rho_216,some_action,some_target,L_217) = l )
| ~ part_of('#skF_1'(Rho_216,some_action,some_target,L_217),rho1)
| ~ permission('#skF_1'(Rho_216,some_action,some_target,L_217))
| ( '#skF_2'(Rho_216,some_action,some_target) = n2 )
| ~ part_of(n2,Rho_216)
| ~ cnt(L_217,some_action,some_target)
| ~ part_of(L_217,Rho_216)
| ~ permission(L_217)
| ~ odrl_rel(Rho_216) ),
inference(resolution,[status(thm)],[c_482,c_100]) ).
tff(c_1066,plain,
! [L_158] :
( ( '#skF_1'(rho1,some_action,some_target,L_158) = l )
| ~ permission('#skF_1'(rho1,some_action,some_target,L_158))
| ( '#skF_2'(rho1,some_action,some_target) = n2 )
| ~ part_of(n2,rho1)
| ~ cnt(L_158,some_action,some_target)
| ~ part_of(L_158,rho1)
| ~ permission(L_158)
| ~ odrl_rel(rho1) ),
inference(resolution,[status(thm)],[c_409,c_1062]) ).
tff(c_1085,plain,
! [L_158] :
( ( '#skF_1'(rho1,some_action,some_target,L_158) = l )
| ~ permission('#skF_1'(rho1,some_action,some_target,L_158))
| ( '#skF_2'(rho1,some_action,some_target) = n2 )
| ~ cnt(L_158,some_action,some_target)
| ~ part_of(L_158,rho1)
| ~ permission(L_158) ),
inference(demodulation,[status(thm),theory(equality)],[c_74,c_86,c_1066]) ).
tff(c_1098,plain,
'#skF_2'(rho1,some_action,some_target) = n2,
inference(splitLeft,[status(thm)],[c_1085]) ).
tff(c_257,plain,
! [Rho_135,L_137,A_136,T_138,M_134] :
( permission('#skF_1'(Rho_135,A_136,T_138,L_137))
| ( M_134 = '#skF_2'(Rho_135,A_136,T_138) )
| ~ cnt(M_134,A_136,T_138)
| ~ part_of(M_134,Rho_135)
| ~ no_right(M_134)
| ~ cnt(L_137,A_136,T_138)
| ~ part_of(L_137,Rho_135)
| ~ permission(L_137)
| ~ odrl_rel(Rho_135) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_285,plain,
! [Rho_135,L_137] :
( permission('#skF_1'(Rho_135,some_action,some_target,L_137))
| ( '#skF_2'(Rho_135,some_action,some_target) = n1 )
| ~ part_of(n1,Rho_135)
| ~ no_right(n1)
| ~ cnt(L_137,some_action,some_target)
| ~ part_of(L_137,Rho_135)
| ~ permission(L_137)
| ~ odrl_rel(Rho_135) ),
inference(resolution,[status(thm)],[c_90,c_257]) ).
tff(c_303,plain,
! [Rho_135,L_137] :
( permission('#skF_1'(Rho_135,some_action,some_target,L_137))
| ( '#skF_2'(Rho_135,some_action,some_target) = n1 )
| ~ part_of(n1,Rho_135)
| ~ cnt(L_137,some_action,some_target)
| ~ part_of(L_137,Rho_135)
| ~ permission(L_137)
| ~ odrl_rel(Rho_135) ),
inference(demodulation,[status(thm),theory(equality)],[c_78,c_285]) ).
tff(c_388,plain,
! [Rho_156,L_158] :
( part_of('#skF_1'(Rho_156,some_action,some_target,L_158),Rho_156)
| ( '#skF_2'(Rho_156,some_action,some_target) = n1 )
| ~ part_of(n1,Rho_156)
| ~ no_right(n1)
| ~ cnt(L_158,some_action,some_target)
| ~ part_of(L_158,Rho_156)
| ~ permission(L_158)
| ~ odrl_rel(Rho_156) ),
inference(resolution,[status(thm)],[c_90,c_360]) ).
tff(c_406,plain,
! [Rho_156,L_158] :
( part_of('#skF_1'(Rho_156,some_action,some_target,L_158),Rho_156)
| ( '#skF_2'(Rho_156,some_action,some_target) = n1 )
| ~ part_of(n1,Rho_156)
| ~ cnt(L_158,some_action,some_target)
| ~ part_of(L_158,Rho_156)
| ~ permission(L_158)
| ~ odrl_rel(Rho_156) ),
inference(demodulation,[status(thm),theory(equality)],[c_78,c_388]) ).
tff(c_439,plain,
! [Rho_163,L_165] :
( cnt('#skF_1'(Rho_163,some_action,some_target,L_165),some_action,some_target)
| ( '#skF_2'(Rho_163,some_action,some_target) = n1 )
| ~ part_of(n1,Rho_163)
| ~ no_right(n1)
| ~ cnt(L_165,some_action,some_target)
| ~ part_of(L_165,Rho_163)
| ~ permission(L_165)
| ~ odrl_rel(Rho_163) ),
inference(resolution,[status(thm)],[c_90,c_411]) ).
tff(c_462,plain,
! [Rho_169,L_170] :
( cnt('#skF_1'(Rho_169,some_action,some_target,L_170),some_action,some_target)
| ( '#skF_2'(Rho_169,some_action,some_target) = n1 )
| ~ part_of(n1,Rho_169)
| ~ cnt(L_170,some_action,some_target)
| ~ part_of(L_170,Rho_169)
| ~ permission(L_170)
| ~ odrl_rel(Rho_169) ),
inference(demodulation,[status(thm),theory(equality)],[c_78,c_439]) ).
tff(c_1166,plain,
! [Rho_224,L_225] :
( ( '#skF_1'(Rho_224,some_action,some_target,L_225) = l )
| ~ part_of('#skF_1'(Rho_224,some_action,some_target,L_225),rho1)
| ~ permission('#skF_1'(Rho_224,some_action,some_target,L_225))
| ( '#skF_2'(Rho_224,some_action,some_target) = n1 )
| ~ part_of(n1,Rho_224)
| ~ cnt(L_225,some_action,some_target)
| ~ part_of(L_225,Rho_224)
| ~ permission(L_225)
| ~ odrl_rel(Rho_224) ),
inference(resolution,[status(thm)],[c_462,c_100]) ).
tff(c_1174,plain,
! [L_158] :
( ( '#skF_1'(rho1,some_action,some_target,L_158) = l )
| ~ permission('#skF_1'(rho1,some_action,some_target,L_158))
| ( '#skF_2'(rho1,some_action,some_target) = n1 )
| ~ part_of(n1,rho1)
| ~ cnt(L_158,some_action,some_target)
| ~ part_of(L_158,rho1)
| ~ permission(L_158)
| ~ odrl_rel(rho1) ),
inference(resolution,[status(thm)],[c_406,c_1166]) ).
tff(c_1193,plain,
! [L_158] :
( ( '#skF_1'(rho1,some_action,some_target,L_158) = l )
| ~ permission('#skF_1'(rho1,some_action,some_target,L_158))
| ( n2 = n1 )
| ~ cnt(L_158,some_action,some_target)
| ~ part_of(L_158,rho1)
| ~ permission(L_158) ),
inference(demodulation,[status(thm),theory(equality)],[c_74,c_84,c_1098,c_1174]) ).
tff(c_1207,plain,
! [L_226] :
( ( '#skF_1'(rho1,some_action,some_target,L_226) = l )
| ~ permission('#skF_1'(rho1,some_action,some_target,L_226))
| ~ cnt(L_226,some_action,some_target)
| ~ part_of(L_226,rho1)
| ~ permission(L_226) ),
inference(negUnitSimplification,[status(thm)],[c_98,c_1193]) ).
tff(c_1215,plain,
! [L_137] :
( ( '#skF_1'(rho1,some_action,some_target,L_137) = l )
| ( '#skF_2'(rho1,some_action,some_target) = n1 )
| ~ part_of(n1,rho1)
| ~ cnt(L_137,some_action,some_target)
| ~ part_of(L_137,rho1)
| ~ permission(L_137)
| ~ odrl_rel(rho1) ),
inference(resolution,[status(thm)],[c_303,c_1207]) ).
tff(c_1233,plain,
! [L_137] :
( ( '#skF_1'(rho1,some_action,some_target,L_137) = l )
| ( n2 = n1 )
| ~ cnt(L_137,some_action,some_target)
| ~ part_of(L_137,rho1)
| ~ permission(L_137) ),
inference(demodulation,[status(thm),theory(equality)],[c_74,c_84,c_1098,c_1215]) ).
tff(c_1244,plain,
! [L_227] :
( ( '#skF_1'(rho1,some_action,some_target,L_227) = l )
| ~ cnt(L_227,some_action,some_target)
| ~ part_of(L_227,rho1)
| ~ permission(L_227) ),
inference(negUnitSimplification,[status(thm)],[c_98,c_1233]) ).
tff(c_1310,plain,
( ( '#skF_1'(rho1,some_action,some_target,l) = l )
| ~ part_of(l,rho1)
| ~ permission(l) ),
inference(resolution,[status(thm)],[c_88,c_1244]) ).
tff(c_1336,plain,
'#skF_1'(rho1,some_action,some_target,l) = l,
inference(demodulation,[status(thm),theory(equality)],[c_76,c_82,c_1310]) ).
tff(c_34,plain,
! [T_3,Rho_1,L_16,M_19,A_2] :
( ( '#skF_1'(Rho_1,A_2,T_3,L_16) != L_16 )
| ( M_19 = '#skF_2'(Rho_1,A_2,T_3) )
| ~ cnt(M_19,A_2,T_3)
| ~ part_of(M_19,Rho_1)
| ~ no_right(M_19)
| ~ cnt(L_16,A_2,T_3)
| ~ part_of(L_16,Rho_1)
| ~ permission(L_16)
| ~ odrl_rel(Rho_1) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_1373,plain,
! [M_19] :
( ( M_19 = '#skF_2'(rho1,some_action,some_target) )
| ~ cnt(M_19,some_action,some_target)
| ~ part_of(M_19,rho1)
| ~ no_right(M_19)
| ~ cnt(l,some_action,some_target)
| ~ part_of(l,rho1)
| ~ permission(l)
| ~ odrl_rel(rho1) ),
inference(superposition,[status(thm),theory(equality)],[c_1336,c_34]) ).
tff(c_1454,plain,
! [M_228] :
( ( n2 = M_228 )
| ~ cnt(M_228,some_action,some_target)
| ~ part_of(M_228,rho1)
| ~ no_right(M_228) ),
inference(demodulation,[status(thm),theory(equality)],[c_74,c_76,c_82,c_88,c_1098,c_1373]) ).
tff(c_1523,plain,
( ( n2 = n1 )
| ~ part_of(n1,rho1)
| ~ no_right(n1) ),
inference(resolution,[status(thm)],[c_90,c_1454]) ).
tff(c_1549,plain,
n2 = n1,
inference(demodulation,[status(thm),theory(equality)],[c_78,c_84,c_1523]) ).
tff(c_1551,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_98,c_1549]) ).
tff(c_1553,plain,
'#skF_2'(rho1,some_action,some_target) != n2,
inference(splitRight,[status(thm)],[c_1085]) ).
tff(c_287,plain,
! [Rho_135,L_137] :
( permission('#skF_1'(Rho_135,some_action,some_target,L_137))
| ( '#skF_2'(Rho_135,some_action,some_target) = n2 )
| ~ part_of(n2,Rho_135)
| ~ no_right(n2)
| ~ cnt(L_137,some_action,some_target)
| ~ part_of(L_137,Rho_135)
| ~ permission(L_137)
| ~ odrl_rel(Rho_135) ),
inference(resolution,[status(thm)],[c_92,c_257]) ).
tff(c_306,plain,
! [Rho_135,L_137] :
( permission('#skF_1'(Rho_135,some_action,some_target,L_137))
| ( '#skF_2'(Rho_135,some_action,some_target) = n2 )
| ~ part_of(n2,Rho_135)
| ~ cnt(L_137,some_action,some_target)
| ~ part_of(L_137,Rho_135)
| ~ permission(L_137)
| ~ odrl_rel(Rho_135) ),
inference(demodulation,[status(thm),theory(equality)],[c_80,c_287]) ).
tff(c_1554,plain,
! [L_229] :
( ( '#skF_1'(rho1,some_action,some_target,L_229) = l )
| ~ permission('#skF_1'(rho1,some_action,some_target,L_229))
| ~ cnt(L_229,some_action,some_target)
| ~ part_of(L_229,rho1)
| ~ permission(L_229) ),
inference(splitRight,[status(thm)],[c_1085]) ).
tff(c_1558,plain,
! [L_137] :
( ( '#skF_1'(rho1,some_action,some_target,L_137) = l )
| ( '#skF_2'(rho1,some_action,some_target) = n2 )
| ~ part_of(n2,rho1)
| ~ cnt(L_137,some_action,some_target)
| ~ part_of(L_137,rho1)
| ~ permission(L_137)
| ~ odrl_rel(rho1) ),
inference(resolution,[status(thm)],[c_306,c_1554]) ).
tff(c_1577,plain,
! [L_137] :
( ( '#skF_1'(rho1,some_action,some_target,L_137) = l )
| ( '#skF_2'(rho1,some_action,some_target) = n2 )
| ~ cnt(L_137,some_action,some_target)
| ~ part_of(L_137,rho1)
| ~ permission(L_137) ),
inference(demodulation,[status(thm),theory(equality)],[c_74,c_86,c_1558]) ).
tff(c_1606,plain,
! [L_236] :
( ( '#skF_1'(rho1,some_action,some_target,L_236) = l )
| ~ cnt(L_236,some_action,some_target)
| ~ part_of(L_236,rho1)
| ~ permission(L_236) ),
inference(negUnitSimplification,[status(thm)],[c_1553,c_1577]) ).
tff(c_1675,plain,
( ( '#skF_1'(rho1,some_action,some_target,l) = l )
| ~ part_of(l,rho1)
| ~ permission(l) ),
inference(resolution,[status(thm)],[c_88,c_1606]) ).
tff(c_1704,plain,
'#skF_1'(rho1,some_action,some_target,l) = l,
inference(demodulation,[status(thm),theory(equality)],[c_76,c_82,c_1675]) ).
tff(c_1738,plain,
! [M_19] :
( ( M_19 = '#skF_2'(rho1,some_action,some_target) )
| ~ cnt(M_19,some_action,some_target)
| ~ part_of(M_19,rho1)
| ~ no_right(M_19)
| ~ cnt(l,some_action,some_target)
| ~ part_of(l,rho1)
| ~ permission(l)
| ~ odrl_rel(rho1) ),
inference(superposition,[status(thm),theory(equality)],[c_1704,c_34]) ).
tff(c_1817,plain,
! [M_237] :
( ( M_237 = '#skF_2'(rho1,some_action,some_target) )
| ~ cnt(M_237,some_action,some_target)
| ~ part_of(M_237,rho1)
| ~ no_right(M_237) ),
inference(demodulation,[status(thm),theory(equality)],[c_74,c_76,c_82,c_88,c_1738]) ).
tff(c_1892,plain,
( ( '#skF_2'(rho1,some_action,some_target) = n2 )
| ~ part_of(n2,rho1)
| ~ no_right(n2) ),
inference(resolution,[status(thm)],[c_92,c_1817]) ).
tff(c_1922,plain,
'#skF_2'(rho1,some_action,some_target) = n2,
inference(demodulation,[status(thm),theory(equality)],[c_80,c_86,c_1892]) ).
tff(c_1924,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1553,c_1922]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.07/0.33 % Computer : n003.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Mon Sep 7 14:09:24 UTC 2026
% 0.07/0.34 % CPUTime :
% 9.89/4.10 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.89/4.11
% 9.89/4.11 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------