%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 : Thu Sep 24 08:50:53 AM UTC 2026
% Result : Unsatisfiable 265.15s 265.45s
% Output : Proof 268.60s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(ax_correlativity_permission,axiom,
! [Rho,A,T] :
( odrl_rel(Rho)
=> ( ? [L] :
( ! [L2] :
( ( cnt(L2,A,T)
& part_of(L2,Rho)
& permission(L2) )
=> L2 = L )
& cnt(L,A,T)
& part_of(L,Rho)
& permission(L) )
<=> ? [N] :
( ! [M] :
( ( cnt(M,A,T)
& part_of(M,Rho)
& no_right(M) )
=> M = N )
& cnt(N,A,T)
& part_of(N,Rho)
& no_right(N) ) ) ),
file('theBenchmark.p',ax_correlativity_permission) ).
fof(pos_l,axiom,
position(l),
file('theBenchmark.p',pos_l) ).
fof(pos_n1,axiom,
position(n1),
file('theBenchmark.p',pos_n1) ).
fof(pos_n2,axiom,
position(n2),
file('theBenchmark.p',pos_n2) ).
fof(rel_rho1,axiom,
legal_relator(rho1),
file('theBenchmark.p',rel_rho1) ).
fof(odrl_rho1,axiom,
odrl_rel(rho1),
file('theBenchmark.p',odrl_rho1) ).
fof(permission_l,axiom,
permission(l),
file('theBenchmark.p',permission_l) ).
fof(no_right_n1,axiom,
no_right(n1),
file('theBenchmark.p',no_right_n1) ).
fof(no_right_n2,axiom,
no_right(n2),
file('theBenchmark.p',no_right_n2) ).
fof(partof_l,axiom,
part_of(l,rho1),
file('theBenchmark.p',partof_l) ).
fof(partof_n1,axiom,
part_of(n1,rho1),
file('theBenchmark.p',partof_n1) ).
fof(partof_n2,axiom,
part_of(n2,rho1),
file('theBenchmark.p',partof_n2) ).
fof(cnt_l,axiom,
cnt(l,some_action,some_target),
file('theBenchmark.p',cnt_l) ).
fof(cnt_n1,axiom,
cnt(n1,some_action,some_target),
file('theBenchmark.p',cnt_n1) ).
fof(cnt_n2,axiom,
cnt(n2,some_action,some_target),
file('theBenchmark.p',cnt_n2) ).
fof(action_typed,axiom,
action(some_action),
file('theBenchmark.p',action_typed) ).
fof(target_typed,axiom,
target(some_target),
file('theBenchmark.p',target_typed) ).
fof(n1_neq_n2,axiom,
n1 != n2,
file('theBenchmark.p',n1_neq_n2) ).
fof(perm_l_unique,axiom,
! [L2] :
( ( cnt(L2,some_action,some_target)
& part_of(L2,rho1)
& permission(L2) )
=> L2 = l ),
file('theBenchmark.p',perm_l_unique) ).
fof(f_1_1,plain,
! [Rho,A,T] :
( ( ( ? [L] :
( ! [L2] :
( L2 = L
| ~ cnt(L2,A,T)
| ~ part_of(L2,Rho)
| ~ permission(L2) )
& cnt(L,A,T)
& part_of(L,Rho)
& permission(L) )
| ! [N] :
( ? [M] :
( M != N
& cnt(M,A,T)
& part_of(M,Rho)
& no_right(M) )
| ~ cnt(N,A,T)
| ~ part_of(N,Rho)
| ~ no_right(N) ) )
& ( ? [N] :
( ! [M] :
( M = N
| ~ cnt(M,A,T)
| ~ part_of(M,Rho)
| ~ no_right(M) )
& cnt(N,A,T)
& part_of(N,Rho)
& no_right(N) )
| ! [L] :
( ? [L2] :
( L2 != L
& cnt(L2,A,T)
& part_of(L2,Rho)
& permission(L2) )
| ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L) ) ) )
| ~ odrl_rel(Rho) ),
inference(fof_nnf,[status(thm)],[ax_correlativity_permission]) ).
fof(f_1_2,plain,
! [U_10,U_9,U_8] :
( ( ( ? [U_7] :
( ! [U_6] :
( U_6 = U_7
| ~ cnt(U_6,U_9,U_8)
| ~ part_of(U_6,U_10)
| ~ permission(U_6) )
& cnt(U_7,U_9,U_8)
& part_of(U_7,U_10)
& permission(U_7) )
| ! [U_5] :
( ? [U_4] :
( U_4 != U_5
& cnt(U_4,U_9,U_8)
& part_of(U_4,U_10)
& no_right(U_4) )
| ~ cnt(U_5,U_9,U_8)
| ~ part_of(U_5,U_10)
| ~ no_right(U_5) ) )
& ( ? [U_3] :
( ! [U_2] :
( U_2 = U_3
| ~ cnt(U_2,U_9,U_8)
| ~ part_of(U_2,U_10)
| ~ no_right(U_2) )
& cnt(U_3,U_9,U_8)
& part_of(U_3,U_10)
& no_right(U_3) )
| ! [U_1] :
( ? [U_0] :
( U_0 != U_1
& cnt(U_0,U_9,U_8)
& part_of(U_0,U_10)
& permission(U_0) )
| ~ cnt(U_1,U_9,U_8)
| ~ part_of(U_1,U_10)
| ~ permission(U_1) ) ) )
| ~ odrl_rel(U_10) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
! [U_10] :
( ( ! [U_14,U_12] :
( ? [U_7] :
( ! [U_6] :
( U_6 = U_7
| ~ cnt(U_6,U_14,U_12)
| ~ part_of(U_6,U_10)
| ~ permission(U_6) )
& cnt(U_7,U_14,U_12)
& part_of(U_7,U_10)
& permission(U_7) )
| ! [U_5] :
( ? [U_4] :
( U_4 != U_5
& cnt(U_4,U_14,U_12)
& part_of(U_4,U_10)
& no_right(U_4) )
| ~ cnt(U_5,U_14,U_12)
| ~ part_of(U_5,U_10)
| ~ no_right(U_5) ) )
& ! [U_13,U_11] :
( ? [U_3] :
( ! [U_2] :
( U_2 = U_3
| ~ cnt(U_2,U_13,U_11)
| ~ part_of(U_2,U_10)
| ~ no_right(U_2) )
& cnt(U_3,U_13,U_11)
& part_of(U_3,U_10)
& no_right(U_3) )
| ! [U_1] :
( ? [U_0] :
( U_0 != U_1
& cnt(U_0,U_13,U_11)
& part_of(U_0,U_10)
& permission(U_0) )
| ~ cnt(U_1,U_13,U_11)
| ~ part_of(U_1,U_10)
| ~ permission(U_1) ) ) )
| ~ odrl_rel(U_10) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
fof(f_1_4,plain,
! [U_10] :
( ( ! [U_14,U_12] :
( ? [U_7] :
( ! [U_6] :
( U_6 = U_7
| ~ cnt(U_6,U_14,U_12)
| ~ part_of(U_6,U_10)
| ~ permission(U_6) )
& cnt(U_7,U_14,U_12)
& part_of(U_7,U_10)
& permission(U_7) )
| ! [U_5] :
( ? [U_4] :
( U_4 != U_5
& cnt(U_4,U_14,U_12)
& part_of(U_4,U_10)
& no_right(U_4) )
| ~ cnt(U_5,U_14,U_12)
| ~ part_of(U_5,U_10)
| ~ no_right(U_5) ) )
& ! [U_13,U_11] :
( ? [U_3] :
( ! [U_2] :
( U_2 = U_3
| ~ cnt(U_2,U_13,U_11)
| ~ part_of(U_2,U_10)
| ~ no_right(U_2) )
& cnt(U_3,U_13,U_11)
& part_of(U_3,U_10)
& no_right(U_3) )
| ! [U_1] :
( ( sK1(U_10,U_13,U_11,U_1) != U_1
& cnt(sK1(U_10,U_13,U_11,U_1),U_13,U_11)
& part_of(sK1(U_10,U_13,U_11,U_1),U_10)
& permission(sK1(U_10,U_13,U_11,U_1)) )
| ~ cnt(U_1,U_13,U_11)
| ~ part_of(U_1,U_10)
| ~ permission(U_1) ) ) )
| ~ odrl_rel(U_10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_0,sK1(U_10,U_13,U_11,U_1))],[f_1_3]) ).
fof(f_1_5,plain,
! [U_10] :
( ( ! [U_14,U_12] :
( ? [U_7] :
( ! [U_6] :
( U_6 = U_7
| ~ cnt(U_6,U_14,U_12)
| ~ part_of(U_6,U_10)
| ~ permission(U_6) )
& cnt(U_7,U_14,U_12)
& part_of(U_7,U_10)
& permission(U_7) )
| ! [U_5] :
( ? [U_4] :
( U_4 != U_5
& cnt(U_4,U_14,U_12)
& part_of(U_4,U_10)
& no_right(U_4) )
| ~ cnt(U_5,U_14,U_12)
| ~ part_of(U_5,U_10)
| ~ no_right(U_5) ) )
& ! [U_13,U_11] :
( ( ! [U_2] :
( U_2 = sK2(U_10,U_13,U_11)
| ~ cnt(U_2,U_13,U_11)
| ~ part_of(U_2,U_10)
| ~ no_right(U_2) )
& cnt(sK2(U_10,U_13,U_11),U_13,U_11)
& part_of(sK2(U_10,U_13,U_11),U_10)
& no_right(sK2(U_10,U_13,U_11)) )
| ! [U_1] :
( ( sK1(U_10,U_13,U_11,U_1) != U_1
& cnt(sK1(U_10,U_13,U_11,U_1),U_13,U_11)
& part_of(sK1(U_10,U_13,U_11,U_1),U_10)
& permission(sK1(U_10,U_13,U_11,U_1)) )
| ~ cnt(U_1,U_13,U_11)
| ~ part_of(U_1,U_10)
| ~ permission(U_1) ) ) )
| ~ odrl_rel(U_10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_3,sK2(U_10,U_13,U_11))],[f_1_4]) ).
fof(f_1_6,plain,
! [U_10] :
( ( ! [U_14,U_12] :
( ? [U_7] :
( ! [U_6] :
( U_6 = U_7
| ~ cnt(U_6,U_14,U_12)
| ~ part_of(U_6,U_10)
| ~ permission(U_6) )
& cnt(U_7,U_14,U_12)
& part_of(U_7,U_10)
& permission(U_7) )
| ! [U_5] :
( ( sK3(U_10,U_14,U_12,U_5) != U_5
& cnt(sK3(U_10,U_14,U_12,U_5),U_14,U_12)
& part_of(sK3(U_10,U_14,U_12,U_5),U_10)
& no_right(sK3(U_10,U_14,U_12,U_5)) )
| ~ cnt(U_5,U_14,U_12)
| ~ part_of(U_5,U_10)
| ~ no_right(U_5) ) )
& ! [U_13,U_11] :
( ( ! [U_2] :
( U_2 = sK2(U_10,U_13,U_11)
| ~ cnt(U_2,U_13,U_11)
| ~ part_of(U_2,U_10)
| ~ no_right(U_2) )
& cnt(sK2(U_10,U_13,U_11),U_13,U_11)
& part_of(sK2(U_10,U_13,U_11),U_10)
& no_right(sK2(U_10,U_13,U_11)) )
| ! [U_1] :
( ( sK1(U_10,U_13,U_11,U_1) != U_1
& cnt(sK1(U_10,U_13,U_11,U_1),U_13,U_11)
& part_of(sK1(U_10,U_13,U_11,U_1),U_10)
& permission(sK1(U_10,U_13,U_11,U_1)) )
| ~ cnt(U_1,U_13,U_11)
| ~ part_of(U_1,U_10)
| ~ permission(U_1) ) ) )
| ~ odrl_rel(U_10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_4,sK3(U_10,U_14,U_12,U_5))],[f_1_5]) ).
fof(f_1_7,plain,
! [U_10] :
( ( ! [U_14,U_12] :
( ( ! [U_6] :
( U_6 = sK4(U_10,U_14,U_12)
| ~ cnt(U_6,U_14,U_12)
| ~ part_of(U_6,U_10)
| ~ permission(U_6) )
& cnt(sK4(U_10,U_14,U_12),U_14,U_12)
& part_of(sK4(U_10,U_14,U_12),U_10)
& permission(sK4(U_10,U_14,U_12)) )
| ! [U_5] :
( ( sK3(U_10,U_14,U_12,U_5) != U_5
& cnt(sK3(U_10,U_14,U_12,U_5),U_14,U_12)
& part_of(sK3(U_10,U_14,U_12,U_5),U_10)
& no_right(sK3(U_10,U_14,U_12,U_5)) )
| ~ cnt(U_5,U_14,U_12)
| ~ part_of(U_5,U_10)
| ~ no_right(U_5) ) )
& ! [U_13,U_11] :
( ( ! [U_2] :
( U_2 = sK2(U_10,U_13,U_11)
| ~ cnt(U_2,U_13,U_11)
| ~ part_of(U_2,U_10)
| ~ no_right(U_2) )
& cnt(sK2(U_10,U_13,U_11),U_13,U_11)
& part_of(sK2(U_10,U_13,U_11),U_10)
& no_right(sK2(U_10,U_13,U_11)) )
| ! [U_1] :
( ( sK1(U_10,U_13,U_11,U_1) != U_1
& cnt(sK1(U_10,U_13,U_11,U_1),U_13,U_11)
& part_of(sK1(U_10,U_13,U_11,U_1),U_10)
& permission(sK1(U_10,U_13,U_11,U_1)) )
| ~ cnt(U_1,U_13,U_11)
| ~ part_of(U_1,U_10)
| ~ permission(U_1) ) ) )
| ~ odrl_rel(U_10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_7,sK4(U_10,U_14,U_12))],[f_1_6]) ).
fof(f_1_8,plain,
( ! [U_10,U_14,U_6,U_12] :
( U_6 = sK4(U_10,U_14,U_12)
| ~ cnt(U_6,U_14,U_12)
| ~ part_of(U_6,U_10)
| ~ permission(U_6)
| ~ sP3(U_10,U_14,U_6,U_12) )
& ! [U_10,U_14,U_6,U_12] :
( cnt(sK4(U_10,U_14,U_12),U_14,U_12)
| ~ sP3(U_10,U_14,U_6,U_12) )
& ! [U_10,U_14,U_6,U_12] :
( part_of(sK4(U_10,U_14,U_12),U_10)
| ~ sP3(U_10,U_14,U_6,U_12) )
& ! [U_10,U_14,U_6,U_12] :
( permission(sK4(U_10,U_14,U_12))
| ~ sP3(U_10,U_14,U_6,U_12) )
& ! [U_5,U_10,U_14,U_12] :
( sK3(U_10,U_14,U_12,U_5) != U_5
| ~ sP2(U_5,U_10,U_14,U_12) )
& ! [U_5,U_10,U_14,U_12] :
( cnt(sK3(U_10,U_14,U_12,U_5),U_14,U_12)
| ~ sP2(U_5,U_10,U_14,U_12) )
& ! [U_5,U_10,U_14,U_12] :
( part_of(sK3(U_10,U_14,U_12,U_5),U_10)
| ~ sP2(U_5,U_10,U_14,U_12) )
& ! [U_5,U_10,U_14,U_12] :
( no_right(sK3(U_10,U_14,U_12,U_5))
| ~ sP2(U_5,U_10,U_14,U_12) )
& ! [U_2,U_10,U_13,U_11] :
( U_2 = sK2(U_10,U_13,U_11)
| ~ cnt(U_2,U_13,U_11)
| ~ part_of(U_2,U_10)
| ~ no_right(U_2)
| ~ sP1(U_2,U_10,U_13,U_11) )
& ! [U_2,U_10,U_13,U_11] :
( cnt(sK2(U_10,U_13,U_11),U_13,U_11)
| ~ sP1(U_2,U_10,U_13,U_11) )
& ! [U_2,U_10,U_13,U_11] :
( part_of(sK2(U_10,U_13,U_11),U_10)
| ~ sP1(U_2,U_10,U_13,U_11) )
& ! [U_2,U_10,U_13,U_11] :
( no_right(sK2(U_10,U_13,U_11))
| ~ sP1(U_2,U_10,U_13,U_11) )
& ! [U_1,U_10,U_13,U_11] :
( sK1(U_10,U_13,U_11,U_1) != U_1
| ~ sP0(U_1,U_10,U_13,U_11) )
& ! [U_1,U_10,U_13,U_11] :
( cnt(sK1(U_10,U_13,U_11,U_1),U_13,U_11)
| ~ sP0(U_1,U_10,U_13,U_11) )
& ! [U_1,U_10,U_13,U_11] :
( part_of(sK1(U_10,U_13,U_11,U_1),U_10)
| ~ sP0(U_1,U_10,U_13,U_11) )
& ! [U_1,U_10,U_13,U_11] :
( permission(sK1(U_10,U_13,U_11,U_1))
| ~ sP0(U_1,U_10,U_13,U_11) )
& ! [U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12] :
( sP3(U_10,U_14,U_6,U_12)
| sP2(U_5,U_10,U_14,U_12)
| ~ cnt(U_5,U_14,U_12)
| ~ part_of(U_5,U_10)
| ~ no_right(U_5)
| ~ sP4(U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12) )
& ! [U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12] :
( sP1(U_2,U_10,U_13,U_11)
| sP0(U_1,U_10,U_13,U_11)
| ~ cnt(U_1,U_13,U_11)
| ~ part_of(U_1,U_10)
| ~ permission(U_1)
| ~ sP4(U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12) )
& ! [U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12] :
( sP4(U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12)
| ~ odrl_rel(U_10) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2,sP3,sP4])],[f_1_7]) ).
cnf(f_1_9,plain,
( sP4(U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12)
| ~ odrl_rel(U_10) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_10,plain,
( sP1(U_2,U_10,U_13,U_11)
| sP0(U_1,U_10,U_13,U_11)
| ~ cnt(U_1,U_13,U_11)
| ~ part_of(U_1,U_10)
| ~ permission(U_1)
| ~ sP4(U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_11,plain,
( sP3(U_10,U_14,U_6,U_12)
| sP2(U_5,U_10,U_14,U_12)
| ~ cnt(U_5,U_14,U_12)
| ~ part_of(U_5,U_10)
| ~ no_right(U_5)
| ~ sP4(U_2,U_5,U_1,U_10,U_13,U_14,U_6,U_11,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_12,plain,
( permission(sK1(U_10,U_13,U_11,U_1))
| ~ sP0(U_1,U_10,U_13,U_11) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_13,plain,
( part_of(sK1(U_10,U_13,U_11,U_1),U_10)
| ~ sP0(U_1,U_10,U_13,U_11) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_14,plain,
( cnt(sK1(U_10,U_13,U_11,U_1),U_13,U_11)
| ~ sP0(U_1,U_10,U_13,U_11) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_15,plain,
( sK1(U_10,U_13,U_11,U_1) != U_1
| ~ sP0(U_1,U_10,U_13,U_11) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_16,plain,
( no_right(sK2(U_10,U_13,U_11))
| ~ sP1(U_2,U_10,U_13,U_11) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_17,plain,
( part_of(sK2(U_10,U_13,U_11),U_10)
| ~ sP1(U_2,U_10,U_13,U_11) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_18,plain,
( cnt(sK2(U_10,U_13,U_11),U_13,U_11)
| ~ sP1(U_2,U_10,U_13,U_11) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_19,plain,
( U_2 = sK2(U_10,U_13,U_11)
| ~ cnt(U_2,U_13,U_11)
| ~ part_of(U_2,U_10)
| ~ no_right(U_2)
| ~ sP1(U_2,U_10,U_13,U_11) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_20,plain,
( no_right(sK3(U_10,U_14,U_12,U_5))
| ~ sP2(U_5,U_10,U_14,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_21,plain,
( part_of(sK3(U_10,U_14,U_12,U_5),U_10)
| ~ sP2(U_5,U_10,U_14,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_22,plain,
( cnt(sK3(U_10,U_14,U_12,U_5),U_14,U_12)
| ~ sP2(U_5,U_10,U_14,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_23,plain,
( sK3(U_10,U_14,U_12,U_5) != U_5
| ~ sP2(U_5,U_10,U_14,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_24,plain,
( permission(sK4(U_10,U_14,U_12))
| ~ sP3(U_10,U_14,U_6,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_25,plain,
( part_of(sK4(U_10,U_14,U_12),U_10)
| ~ sP3(U_10,U_14,U_6,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_26,plain,
( cnt(sK4(U_10,U_14,U_12),U_14,U_12)
| ~ sP3(U_10,U_14,U_6,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_27,plain,
( U_6 = sK4(U_10,U_14,U_12)
| ~ cnt(U_6,U_14,U_12)
| ~ part_of(U_6,U_10)
| ~ permission(U_6)
| ~ sP3(U_10,U_14,U_6,U_12) ),
inference(clausify,[status(thm)],[f_1_8]) ).
fof(f_2_1,plain,
position(l),
inference(fof_nnf,[status(thm)],[pos_l]) ).
fof(f_2_2,plain,
position(l),
inference(definitional_conversion,[status(esa)],[f_2_1]) ).
cnf(f_2_3,plain,
position(l),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
position(n1),
inference(fof_nnf,[status(thm)],[pos_n1]) ).
fof(f_3_2,plain,
position(n1),
inference(definitional_conversion,[status(esa)],[f_3_1]) ).
cnf(f_3_3,plain,
position(n1),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
position(n2),
inference(fof_nnf,[status(thm)],[pos_n2]) ).
fof(f_4_2,plain,
position(n2),
inference(definitional_conversion,[status(esa)],[f_4_1]) ).
cnf(f_4_3,plain,
position(n2),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
legal_relator(rho1),
inference(fof_nnf,[status(thm)],[rel_rho1]) ).
fof(f_5_2,plain,
legal_relator(rho1),
inference(definitional_conversion,[status(esa)],[f_5_1]) ).
cnf(f_5_3,plain,
legal_relator(rho1),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
odrl_rel(rho1),
inference(fof_nnf,[status(thm)],[odrl_rho1]) ).
fof(f_6_2,plain,
odrl_rel(rho1),
inference(definitional_conversion,[status(esa)],[f_6_1]) ).
cnf(f_6_3,plain,
odrl_rel(rho1),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
permission(l),
inference(fof_nnf,[status(thm)],[permission_l]) ).
fof(f_7_2,plain,
permission(l),
inference(definitional_conversion,[status(esa)],[f_7_1]) ).
cnf(f_7_3,plain,
permission(l),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
no_right(n1),
inference(fof_nnf,[status(thm)],[no_right_n1]) ).
fof(f_8_2,plain,
no_right(n1),
inference(definitional_conversion,[status(esa)],[f_8_1]) ).
cnf(f_8_3,plain,
no_right(n1),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
no_right(n2),
inference(fof_nnf,[status(thm)],[no_right_n2]) ).
fof(f_9_2,plain,
no_right(n2),
inference(definitional_conversion,[status(esa)],[f_9_1]) ).
cnf(f_9_3,plain,
no_right(n2),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
part_of(l,rho1),
inference(fof_nnf,[status(thm)],[partof_l]) ).
fof(f_10_2,plain,
part_of(l,rho1),
inference(definitional_conversion,[status(esa)],[f_10_1]) ).
cnf(f_10_3,plain,
part_of(l,rho1),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
part_of(n1,rho1),
inference(fof_nnf,[status(thm)],[partof_n1]) ).
fof(f_11_2,plain,
part_of(n1,rho1),
inference(definitional_conversion,[status(esa)],[f_11_1]) ).
cnf(f_11_3,plain,
part_of(n1,rho1),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
part_of(n2,rho1),
inference(fof_nnf,[status(thm)],[partof_n2]) ).
fof(f_12_2,plain,
part_of(n2,rho1),
inference(definitional_conversion,[status(esa)],[f_12_1]) ).
cnf(f_12_3,plain,
part_of(n2,rho1),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
cnt(l,some_action,some_target),
inference(fof_nnf,[status(thm)],[cnt_l]) ).
fof(f_13_2,plain,
cnt(l,some_action,some_target),
inference(definitional_conversion,[status(esa)],[f_13_1]) ).
cnf(f_13_3,plain,
cnt(l,some_action,some_target),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
cnt(n1,some_action,some_target),
inference(fof_nnf,[status(thm)],[cnt_n1]) ).
fof(f_14_2,plain,
cnt(n1,some_action,some_target),
inference(definitional_conversion,[status(esa)],[f_14_1]) ).
cnf(f_14_3,plain,
cnt(n1,some_action,some_target),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
cnt(n2,some_action,some_target),
inference(fof_nnf,[status(thm)],[cnt_n2]) ).
fof(f_15_2,plain,
cnt(n2,some_action,some_target),
inference(definitional_conversion,[status(esa)],[f_15_1]) ).
cnf(f_15_3,plain,
cnt(n2,some_action,some_target),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
action(some_action),
inference(fof_nnf,[status(thm)],[action_typed]) ).
fof(f_16_2,plain,
action(some_action),
inference(definitional_conversion,[status(esa)],[f_16_1]) ).
cnf(f_16_3,plain,
action(some_action),
inference(clausify,[status(thm)],[f_16_2]) ).
fof(f_17_1,plain,
target(some_target),
inference(fof_nnf,[status(thm)],[target_typed]) ).
fof(f_17_2,plain,
target(some_target),
inference(definitional_conversion,[status(esa)],[f_17_1]) ).
cnf(f_17_3,plain,
target(some_target),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
n1 != n2,
inference(fof_nnf,[status(thm)],[n1_neq_n2]) ).
fof(f_18_2,plain,
n1 != n2,
inference(definitional_conversion,[status(esa)],[f_18_1]) ).
cnf(f_18_3,plain,
n1 != n2,
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [L2] :
( L2 = l
| ~ cnt(L2,some_action,some_target)
| ~ part_of(L2,rho1)
| ~ permission(L2) ),
inference(fof_nnf,[status(thm)],[perm_l_unique]) ).
fof(f_19_2,plain,
! [U_15] :
( U_15 = l
| ~ cnt(U_15,some_action,some_target)
| ~ part_of(U_15,rho1)
| ~ permission(U_15) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
! [U_15] :
( U_15 = l
| ~ cnt(U_15,some_action,some_target)
| ~ part_of(U_15,rho1)
| ~ permission(U_15) ),
inference(definitional_conversion,[status(esa)],[f_19_2]) ).
cnf(f_19_4,plain,
( U_15 = l
| ~ cnt(U_15,some_action,some_target)
| ~ part_of(U_15,rho1)
| ~ permission(U_15) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( sK1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( sK2(Eq_x_0,Eq_x_1,Eq_x_2) = sK2(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sK3(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK3(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( sK4(Eq_x_0,Eq_x_1,Eq_x_2) = sK4(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( odrl_rel(Eq_y_0)
| ~ odrl_rel(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_9,axiom,
( permission(Eq_y_0)
| ~ permission(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( part_of(Eq_y_0,Eq_y_1)
| ~ part_of(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( cnt(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ cnt(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( no_right(Eq_y_0)
| ~ no_right(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( position(Eq_y_0)
| ~ position(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( legal_relator(Eq_y_0)
| ~ legal_relator(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( action(Eq_y_0)
| ~ action(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( target(Eq_y_0)
| ~ target(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( sP0(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP0(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( sP1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( sP2(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP2(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( sP3(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP3(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( sP4(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5,Eq_y_6,Eq_y_7,Eq_y_8)
| ~ sP4(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5,Eq_x_6,Eq_x_7,Eq_x_8)
| Eq_x_8 != Eq_y_8
| Eq_x_7 != Eq_y_7
| Eq_x_6 != Eq_y_6
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 This is a FOF_UNS_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n010.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 19 16:21:53 UTC 2026
% 0.10/0.35 % CPUTime :
% 265.15/265.45 % SZS status Unsatisfiable for theBenchmark
% 265.15/265.45 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------