%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Sun Sep 27 08:03:08 AM UTC 2026
% Result : Unsatisfiable 0.14s 5.53s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 13
% Syntax : Number of formulae : 95 ( 27 unt; 0 def)
% Number of atoms : 612 ( 126 equ)
% Maximal formula atoms : 216 ( 6 avg)
% Number of connectives : 885 ( 368 ~; 443 |; 69 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 46 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-4 aty)
% Number of variables : 227 ( 0 sgn 156 !; 6 ?)
% 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(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(odrl_rho1,axiom,
odrl_rel(rho1),
file('theBenchmark.p',odrl_rho1) ).
cnf(c_4,plain,
odrl_rel(rho1),
inference(clausify,[status(thm)],[odrl_rho1]) ).
fof(nnf_1,plain,
! [Rho,A,T] :
( ( ( ! [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) ) )
& ( ? [X2] :
( ! [X3] :
( X3 = X2
| ~ cnt(X3,A,T)
| ~ part_of(X3,Rho)
| ~ no_right(X3) )
& cnt(X2,A,T)
& part_of(X2,Rho)
& no_right(X2) )
| ! [X0] :
( ? [X1] :
( X1 != X0
& cnt(X1,A,T)
& part_of(X1,Rho)
& permission(X1) )
| ~ cnt(X0,A,T)
| ~ part_of(X0,Rho)
| ~ permission(X0) ) ) )
| ~ odrl_rel(Rho) ),
inference(fof_nnf,[status(thm)],[ax_correlativity_permission]) ).
fof(sk_ax_correlativity_permission_sk,plain,
! [Rho,A,T] :
( ( ( ! [N] :
( ( sK3(Rho,A,T,N) != N
& cnt(sK3(Rho,A,T,N),A,T)
& part_of(sK3(Rho,A,T,N),Rho)
& no_right(sK3(Rho,A,T,N)) )
| ~ cnt(N,A,T)
| ~ part_of(N,Rho)
| ~ no_right(N) )
| ( ! [L2] :
( L2 = sK2(Rho,A,T)
| ~ cnt(L2,A,T)
| ~ part_of(L2,Rho)
| ~ permission(L2) )
& cnt(sK2(Rho,A,T),A,T)
& part_of(sK2(Rho,A,T),Rho)
& permission(sK2(Rho,A,T)) ) )
& ( ( ! [X3] :
( X3 = sK1(Rho,A,T)
| ~ cnt(X3,A,T)
| ~ part_of(X3,Rho)
| ~ no_right(X3) )
& cnt(sK1(Rho,A,T),A,T)
& part_of(sK1(Rho,A,T),Rho)
& no_right(sK1(Rho,A,T)) )
| ! [X0] :
( ( sK0(Rho,A,T,X0) != X0
& cnt(sK0(Rho,A,T,X0),A,T)
& part_of(sK0(Rho,A,T,X0),Rho)
& permission(sK0(Rho,A,T,X0)) )
| ~ cnt(X0,A,T)
| ~ part_of(X0,Rho)
| ~ permission(X0) ) ) )
| ~ odrl_rel(Rho) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X1,sK0(Rho,A,T,X0)),skolemize(X2,sK1(Rho,A,T)),skolemize(L,sK2(Rho,A,T)),skolemize(M,sK3(Rho,A,T,N))],[nnf_1]) ).
fof(sk_ax_correlativity_permission,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( sK3(VAR_0,VAR_2,VAR_3,VAR_4) != VAR_4
| ~ cnt(VAR_4,VAR_2,VAR_3)
| ~ part_of(VAR_4,VAR_0)
| ~ no_right(VAR_4)
| VAR_1 = sK2(VAR_0,VAR_2,VAR_3)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( cnt(sK3(VAR_0,VAR_2,VAR_3,VAR_4),VAR_2,VAR_3)
| ~ cnt(VAR_4,VAR_2,VAR_3)
| ~ part_of(VAR_4,VAR_0)
| ~ no_right(VAR_4)
| VAR_1 = sK2(VAR_0,VAR_2,VAR_3)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( part_of(sK3(VAR_0,VAR_2,VAR_3,VAR_4),VAR_0)
| ~ cnt(VAR_4,VAR_2,VAR_3)
| ~ part_of(VAR_4,VAR_0)
| ~ no_right(VAR_4)
| VAR_1 = sK2(VAR_0,VAR_2,VAR_3)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( no_right(sK3(VAR_0,VAR_2,VAR_3,VAR_4))
| ~ cnt(VAR_4,VAR_2,VAR_3)
| ~ part_of(VAR_4,VAR_0)
| ~ no_right(VAR_4)
| VAR_1 = sK2(VAR_0,VAR_2,VAR_3)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( sK3(VAR_0,VAR_1,VAR_2,VAR_3) != VAR_3
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| cnt(sK2(VAR_0,VAR_1,VAR_2),VAR_1,VAR_2)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( cnt(sK3(VAR_0,VAR_1,VAR_2,VAR_3),VAR_1,VAR_2)
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| cnt(sK2(VAR_0,VAR_1,VAR_2),VAR_1,VAR_2)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( part_of(sK3(VAR_0,VAR_1,VAR_2,VAR_3),VAR_0)
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| cnt(sK2(VAR_0,VAR_1,VAR_2),VAR_1,VAR_2)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( no_right(sK3(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| cnt(sK2(VAR_0,VAR_1,VAR_2),VAR_1,VAR_2)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( sK3(VAR_0,VAR_1,VAR_2,VAR_3) != VAR_3
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| part_of(sK2(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( cnt(sK3(VAR_0,VAR_1,VAR_2,VAR_3),VAR_1,VAR_2)
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| part_of(sK2(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( part_of(sK3(VAR_0,VAR_1,VAR_2,VAR_3),VAR_0)
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| part_of(sK2(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( no_right(sK3(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| part_of(sK2(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( sK3(VAR_0,VAR_1,VAR_2,VAR_3) != VAR_3
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| permission(sK2(VAR_0,VAR_1,VAR_2))
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( cnt(sK3(VAR_0,VAR_1,VAR_2,VAR_3),VAR_1,VAR_2)
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| permission(sK2(VAR_0,VAR_1,VAR_2))
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( part_of(sK3(VAR_0,VAR_1,VAR_2,VAR_3),VAR_0)
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| permission(sK2(VAR_0,VAR_1,VAR_2))
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( no_right(sK3(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ cnt(VAR_3,VAR_1,VAR_2)
| ~ part_of(VAR_3,VAR_0)
| ~ no_right(VAR_3)
| permission(sK2(VAR_0,VAR_1,VAR_2))
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( VAR_4 = sK1(VAR_0,VAR_2,VAR_3)
| ~ cnt(VAR_4,VAR_2,VAR_3)
| ~ part_of(VAR_4,VAR_0)
| ~ no_right(VAR_4)
| sK0(VAR_0,VAR_2,VAR_3,VAR_1) != VAR_1
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( cnt(sK1(VAR_0,VAR_2,VAR_3),VAR_2,VAR_3)
| sK0(VAR_0,VAR_2,VAR_3,VAR_1) != VAR_1
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( part_of(sK1(VAR_0,VAR_2,VAR_3),VAR_0)
| sK0(VAR_0,VAR_2,VAR_3,VAR_1) != VAR_1
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( no_right(sK1(VAR_0,VAR_2,VAR_3))
| sK0(VAR_0,VAR_2,VAR_3,VAR_1) != VAR_1
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( VAR_4 = sK1(VAR_0,VAR_2,VAR_3)
| ~ cnt(VAR_4,VAR_2,VAR_3)
| ~ part_of(VAR_4,VAR_0)
| ~ no_right(VAR_4)
| cnt(sK0(VAR_0,VAR_2,VAR_3,VAR_1),VAR_2,VAR_3)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( cnt(sK1(VAR_0,VAR_2,VAR_3),VAR_2,VAR_3)
| cnt(sK0(VAR_0,VAR_2,VAR_3,VAR_1),VAR_2,VAR_3)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( part_of(sK1(VAR_0,VAR_2,VAR_3),VAR_0)
| cnt(sK0(VAR_0,VAR_2,VAR_3,VAR_1),VAR_2,VAR_3)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( no_right(sK1(VAR_0,VAR_2,VAR_3))
| cnt(sK0(VAR_0,VAR_2,VAR_3,VAR_1),VAR_2,VAR_3)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( VAR_4 = sK1(VAR_0,VAR_2,VAR_3)
| ~ cnt(VAR_4,VAR_2,VAR_3)
| ~ part_of(VAR_4,VAR_0)
| ~ no_right(VAR_4)
| part_of(sK0(VAR_0,VAR_2,VAR_3,VAR_1),VAR_0)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( cnt(sK1(VAR_0,VAR_2,VAR_3),VAR_2,VAR_3)
| part_of(sK0(VAR_0,VAR_2,VAR_3,VAR_1),VAR_0)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( part_of(sK1(VAR_0,VAR_2,VAR_3),VAR_0)
| part_of(sK0(VAR_0,VAR_2,VAR_3,VAR_1),VAR_0)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( no_right(sK1(VAR_0,VAR_2,VAR_3))
| part_of(sK0(VAR_0,VAR_2,VAR_3,VAR_1),VAR_0)
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( VAR_4 = sK1(VAR_0,VAR_2,VAR_3)
| ~ cnt(VAR_4,VAR_2,VAR_3)
| ~ part_of(VAR_4,VAR_0)
| ~ no_right(VAR_4)
| permission(sK0(VAR_0,VAR_2,VAR_3,VAR_1))
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( cnt(sK1(VAR_0,VAR_2,VAR_3),VAR_2,VAR_3)
| permission(sK0(VAR_0,VAR_2,VAR_3,VAR_1))
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( part_of(sK1(VAR_0,VAR_2,VAR_3),VAR_0)
| permission(sK0(VAR_0,VAR_2,VAR_3,VAR_1))
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( no_right(sK1(VAR_0,VAR_2,VAR_3))
| permission(sK0(VAR_0,VAR_2,VAR_3,VAR_1))
| ~ cnt(VAR_1,VAR_2,VAR_3)
| ~ part_of(VAR_1,VAR_0)
| ~ permission(VAR_1)
| ~ odrl_rel(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_ax_correlativity_permission_sk]) ).
cnf(c_20,plain,
( E = sK1(A,C,D)
| ~ cnt(E,C,D)
| ~ part_of(E,A)
| ~ no_right(E)
| sK0(A,C,D,B) != B
| ~ cnt(B,C,D)
| ~ part_of(B,A)
| ~ permission(B)
| ~ odrl_rel(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_correlativity_permission]) ).
cnf(c_24,plain,
( E = sK1(A,C,D)
| ~ cnt(E,C,D)
| ~ part_of(E,A)
| ~ no_right(E)
| cnt(sK0(A,C,D,B),C,D)
| ~ cnt(B,C,D)
| ~ part_of(B,A)
| ~ permission(B)
| ~ odrl_rel(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_correlativity_permission]) ).
cnf(c_28,plain,
( E = sK1(A,C,D)
| ~ cnt(E,C,D)
| ~ part_of(E,A)
| ~ no_right(E)
| part_of(sK0(A,C,D,B),A)
| ~ cnt(B,C,D)
| ~ part_of(B,A)
| ~ permission(B)
| ~ odrl_rel(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_correlativity_permission]) ).
cnf(c_32,plain,
( E = sK1(A,C,D)
| ~ cnt(E,C,D)
| ~ part_of(E,A)
| ~ no_right(E)
| permission(sK0(A,C,D,B))
| ~ cnt(B,C,D)
| ~ part_of(B,A)
| ~ permission(B)
| ~ odrl_rel(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_correlativity_permission]) ).
cnf(c_36,plain,
( l = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(clausify,[status(thm)],[perm_l_unique]) ).
fof(n1_neq_n2,axiom,
n1 != n2,
file('theBenchmark.p',n1_neq_n2) ).
cnf(c_37,plain,
n1 != n2,
inference(clausify,[status(thm)],[n1_neq_n2]) ).
cnf(c_38,plain,
n2 != n1,
inference(copy,[status(thm)],[c_37]) ).
fof(cnt_n2,axiom,
cnt(n2,some_action,some_target),
file('theBenchmark.p',cnt_n2) ).
cnf(c_39,plain,
cnt(n2,some_action,some_target),
inference(clausify,[status(thm)],[cnt_n2]) ).
fof(cnt_n1,axiom,
cnt(n1,some_action,some_target),
file('theBenchmark.p',cnt_n1) ).
cnf(c_40,plain,
cnt(n1,some_action,some_target),
inference(clausify,[status(thm)],[cnt_n1]) ).
fof(cnt_l,axiom,
cnt(l,some_action,some_target),
file('theBenchmark.p',cnt_l) ).
cnf(c_41,plain,
cnt(l,some_action,some_target),
inference(clausify,[status(thm)],[cnt_l]) ).
fof(partof_n2,axiom,
part_of(n2,rho1),
file('theBenchmark.p',partof_n2) ).
cnf(c_42,plain,
part_of(n2,rho1),
inference(clausify,[status(thm)],[partof_n2]) ).
fof(partof_n1,axiom,
part_of(n1,rho1),
file('theBenchmark.p',partof_n1) ).
cnf(c_43,plain,
part_of(n1,rho1),
inference(clausify,[status(thm)],[partof_n1]) ).
fof(partof_l,axiom,
part_of(l,rho1),
file('theBenchmark.p',partof_l) ).
cnf(c_44,plain,
part_of(l,rho1),
inference(clausify,[status(thm)],[partof_l]) ).
fof(no_right_n2,axiom,
no_right(n2),
file('theBenchmark.p',no_right_n2) ).
cnf(c_45,plain,
no_right(n2),
inference(clausify,[status(thm)],[no_right_n2]) ).
fof(no_right_n1,axiom,
no_right(n1),
file('theBenchmark.p',no_right_n1) ).
cnf(c_46,plain,
no_right(n1),
inference(clausify,[status(thm)],[no_right_n1]) ).
fof(permission_l,axiom,
permission(l),
file('theBenchmark.p',permission_l) ).
cnf(c_47,plain,
permission(l),
inference(clausify,[status(thm)],[permission_l]) ).
cnf(c_68,plain,
( D = sK1(rho1,B,C)
| ~ cnt(D,B,C)
| ~ part_of(D,rho1)
| ~ no_right(D)
| sK0(rho1,B,C,A) != A
| ~ cnt(A,B,C)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(resolve,[status(thm)],[c_20,c_4]) ).
cnf(c_69,plain,
( sK1(rho1,B,C) = D
| ~ cnt(D,B,C)
| ~ part_of(D,rho1)
| ~ no_right(D)
| sK0(rho1,B,C,A) != A
| ~ cnt(A,B,C)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(copy,[status(thm)],[c_68]) ).
cnf(c_73,plain,
( D = sK1(rho1,B,C)
| ~ cnt(D,B,C)
| ~ part_of(D,rho1)
| ~ no_right(D)
| cnt(sK0(rho1,B,C,A),B,C)
| ~ cnt(A,B,C)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(resolve,[status(thm)],[c_24,c_4]) ).
cnf(c_74,plain,
( sK1(rho1,B,C) = D
| ~ cnt(D,B,C)
| ~ part_of(D,rho1)
| ~ no_right(D)
| cnt(sK0(rho1,B,C,A),B,C)
| ~ cnt(A,B,C)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(copy,[status(thm)],[c_73]) ).
cnf(c_78,plain,
( D = sK1(rho1,B,C)
| ~ cnt(D,B,C)
| ~ part_of(D,rho1)
| ~ no_right(D)
| part_of(sK0(rho1,B,C,A),rho1)
| ~ cnt(A,B,C)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(resolve,[status(thm)],[c_28,c_4]) ).
cnf(c_79,plain,
( sK1(rho1,B,C) = D
| ~ cnt(D,B,C)
| ~ part_of(D,rho1)
| ~ no_right(D)
| part_of(sK0(rho1,B,C,A),rho1)
| ~ cnt(A,B,C)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(copy,[status(thm)],[c_78]) ).
cnf(c_83,plain,
( D = sK1(rho1,B,C)
| ~ cnt(D,B,C)
| ~ part_of(D,rho1)
| ~ no_right(D)
| permission(sK0(rho1,B,C,A))
| ~ cnt(A,B,C)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(resolve,[status(thm)],[c_32,c_4]) ).
cnf(c_84,plain,
( sK1(rho1,B,C) = D
| ~ cnt(D,B,C)
| ~ part_of(D,rho1)
| ~ no_right(D)
| permission(sK0(rho1,B,C,A))
| ~ cnt(A,B,C)
| ~ part_of(A,rho1)
| ~ permission(A) ),
inference(copy,[status(thm)],[c_83]) ).
cnf(c_1878,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| sK0(rho1,some_action,some_target,l) != l
| ~ part_of(l,rho1)
| ~ permission(l) ),
inference(resolve,[status(thm)],[c_69,c_41]) ).
cnf(c_1879,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| sK0(rho1,some_action,some_target,l) != l
| ~ part_of(l,rho1) ),
inference(resolve,[status(thm)],[c_47,c_1878]) ).
cnf(c_158,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| sK0(rho1,some_action,some_target,l) != l ),
inference(resolve,[status(thm)],[c_44,c_1879]) ).
cnf(c_1880,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target)
| ~ part_of(l,rho1)
| ~ permission(l) ),
inference(resolve,[status(thm)],[c_74,c_41]) ).
cnf(c_1881,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target)
| ~ part_of(l,rho1) ),
inference(resolve,[status(thm)],[c_47,c_1880]) ).
cnf(c_173,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolve,[status(thm)],[c_44,c_1881]) ).
cnf(c_1882,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| part_of(sK0(rho1,some_action,some_target,l),rho1)
| ~ part_of(l,rho1)
| ~ permission(l) ),
inference(resolve,[status(thm)],[c_79,c_41]) ).
cnf(c_1883,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| part_of(sK0(rho1,some_action,some_target,l),rho1)
| ~ part_of(l,rho1) ),
inference(resolve,[status(thm)],[c_47,c_1882]) ).
cnf(c_188,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| part_of(sK0(rho1,some_action,some_target,l),rho1) ),
inference(resolve,[status(thm)],[c_44,c_1883]) ).
cnf(c_1884,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| permission(sK0(rho1,some_action,some_target,l))
| ~ part_of(l,rho1)
| ~ permission(l) ),
inference(resolve,[status(thm)],[c_84,c_41]) ).
cnf(c_1885,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| permission(sK0(rho1,some_action,some_target,l))
| ~ part_of(l,rho1) ),
inference(resolve,[status(thm)],[c_47,c_1884]) ).
cnf(c_203,plain,
( sK1(rho1,some_action,some_target) = A
| ~ cnt(A,some_action,some_target)
| ~ part_of(A,rho1)
| ~ no_right(A)
| permission(sK0(rho1,some_action,some_target,l)) ),
inference(resolve,[status(thm)],[c_44,c_1885]) ).
cnf(c_1886,plain,
( sK1(rho1,some_action,some_target) = n1
| ~ part_of(n1,rho1)
| ~ no_right(n1)
| sK0(rho1,some_action,some_target,l) != l ),
inference(resolve,[status(thm)],[c_158,c_40]) ).
cnf(c_1887,plain,
( sK1(rho1,some_action,some_target) = n1
| ~ part_of(n1,rho1)
| sK0(rho1,some_action,some_target,l) != l ),
inference(resolve,[status(thm)],[c_46,c_1886]) ).
cnf(c_1087,plain,
( sK1(rho1,some_action,some_target) = n1
| sK0(rho1,some_action,some_target,l) != l ),
inference(resolve,[status(thm)],[c_43,c_1887]) ).
cnf(c_1888,plain,
( sK1(rho1,some_action,some_target) = n2
| ~ part_of(n2,rho1)
| ~ no_right(n2)
| sK0(rho1,some_action,some_target,l) != l ),
inference(resolve,[status(thm)],[c_158,c_39]) ).
cnf(c_1889,plain,
( sK1(rho1,some_action,some_target) = n2
| ~ part_of(n2,rho1)
| sK0(rho1,some_action,some_target,l) != l ),
inference(resolve,[status(thm)],[c_45,c_1888]) ).
cnf(c_1088,plain,
( sK1(rho1,some_action,some_target) = n2
| sK0(rho1,some_action,some_target,l) != l ),
inference(resolve,[status(thm)],[c_42,c_1889]) ).
cnf(c_1890,plain,
( sK1(rho1,some_action,some_target) = n1
| ~ part_of(n1,rho1)
| ~ no_right(n1)
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolve,[status(thm)],[c_173,c_40]) ).
cnf(c_1891,plain,
( sK1(rho1,some_action,some_target) = n1
| ~ part_of(n1,rho1)
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolve,[status(thm)],[c_46,c_1890]) ).
cnf(c_1183,plain,
( sK1(rho1,some_action,some_target) = n1
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolve,[status(thm)],[c_43,c_1891]) ).
cnf(c_1892,plain,
( sK1(rho1,some_action,some_target) = n2
| ~ part_of(n2,rho1)
| ~ no_right(n2)
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolve,[status(thm)],[c_173,c_39]) ).
cnf(c_1893,plain,
( sK1(rho1,some_action,some_target) = n2
| ~ part_of(n2,rho1)
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolve,[status(thm)],[c_45,c_1892]) ).
cnf(c_1184,plain,
( sK1(rho1,some_action,some_target) = n2
| cnt(sK0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolve,[status(thm)],[c_42,c_1893]) ).
cnf(c_1894,plain,
( l = sK0(rho1,some_action,some_target,l)
| ~ part_of(sK0(rho1,some_action,some_target,l),rho1)
| ~ permission(sK0(rho1,some_action,some_target,l))
| sK1(rho1,some_action,some_target) = n1 ),
inference(resolve,[status(thm)],[c_1183,c_36]) ).
cnf(c_1273,plain,
( sK0(rho1,some_action,some_target,l) = l
| ~ part_of(sK0(rho1,some_action,some_target,l),rho1)
| ~ permission(sK0(rho1,some_action,some_target,l))
| sK1(rho1,some_action,some_target) = n1 ),
inference(copy,[status(thm)],[c_1894]) ).
cnf(c_1895,plain,
( l = sK0(rho1,some_action,some_target,l)
| ~ part_of(sK0(rho1,some_action,some_target,l),rho1)
| ~ permission(sK0(rho1,some_action,some_target,l))
| sK1(rho1,some_action,some_target) = n2 ),
inference(resolve,[status(thm)],[c_1184,c_36]) ).
cnf(c_1332,plain,
( sK0(rho1,some_action,some_target,l) = l
| ~ part_of(sK0(rho1,some_action,some_target,l),rho1)
| ~ permission(sK0(rho1,some_action,some_target,l))
| sK1(rho1,some_action,some_target) = n2 ),
inference(copy,[status(thm)],[c_1895]) ).
cnf(c_1896,plain,
( sK1(rho1,some_action,some_target) = n1
| ~ part_of(n1,rho1)
| ~ no_right(n1)
| part_of(sK0(rho1,some_action,some_target,l),rho1) ),
inference(resolve,[status(thm)],[c_188,c_40]) ).
cnf(c_1897,plain,
( sK1(rho1,some_action,some_target) = n1
| ~ part_of(n1,rho1)
| part_of(sK0(rho1,some_action,some_target,l),rho1) ),
inference(resolve,[status(thm)],[c_46,c_1896]) ).
cnf(c_1396,plain,
( sK1(rho1,some_action,some_target) = n1
| part_of(sK0(rho1,some_action,some_target,l),rho1) ),
inference(resolve,[status(thm)],[c_43,c_1897]) ).
cnf(c_1898,plain,
( sK1(rho1,some_action,some_target) = n2
| ~ part_of(n2,rho1)
| ~ no_right(n2)
| part_of(sK0(rho1,some_action,some_target,l),rho1) ),
inference(resolve,[status(thm)],[c_188,c_39]) ).
cnf(c_1899,plain,
( sK1(rho1,some_action,some_target) = n2
| ~ part_of(n2,rho1)
| part_of(sK0(rho1,some_action,some_target,l),rho1) ),
inference(resolve,[status(thm)],[c_45,c_1898]) ).
cnf(c_1397,plain,
( sK1(rho1,some_action,some_target) = n2
| part_of(sK0(rho1,some_action,some_target,l),rho1) ),
inference(resolve,[status(thm)],[c_42,c_1899]) ).
cnf(c_1900,plain,
( sK1(rho1,some_action,some_target) = n1
| ~ part_of(n1,rho1)
| ~ no_right(n1)
| permission(sK0(rho1,some_action,some_target,l)) ),
inference(resolve,[status(thm)],[c_203,c_40]) ).
cnf(c_1901,plain,
( sK1(rho1,some_action,some_target) = n1
| ~ part_of(n1,rho1)
| permission(sK0(rho1,some_action,some_target,l)) ),
inference(resolve,[status(thm)],[c_46,c_1900]) ).
cnf(c_1492,plain,
( sK1(rho1,some_action,some_target) = n1
| permission(sK0(rho1,some_action,some_target,l)) ),
inference(resolve,[status(thm)],[c_43,c_1901]) ).
cnf(c_1902,plain,
( sK1(rho1,some_action,some_target) = n2
| ~ part_of(n2,rho1)
| ~ no_right(n2)
| permission(sK0(rho1,some_action,some_target,l)) ),
inference(resolve,[status(thm)],[c_203,c_39]) ).
cnf(c_1903,plain,
( sK1(rho1,some_action,some_target) = n2
| ~ part_of(n2,rho1)
| permission(sK0(rho1,some_action,some_target,l)) ),
inference(resolve,[status(thm)],[c_45,c_1902]) ).
cnf(c_1493,plain,
( sK1(rho1,some_action,some_target) = n2
| permission(sK0(rho1,some_action,some_target,l)) ),
inference(resolve,[status(thm)],[c_42,c_1903]) ).
cnf(c_1904,plain,
( sK1(rho1,some_action,some_target) = n1
| sK0(rho1,some_action,some_target,l) = l
| ~ permission(sK0(rho1,some_action,some_target,l))
| sK1(rho1,some_action,some_target) = n1 ),
inference(resolve,[status(thm)],[c_1273,c_1396]) ).
cnf(c_1866,plain,
( sK0(rho1,some_action,some_target,l) = l
| ~ permission(sK0(rho1,some_action,some_target,l))
| sK1(rho1,some_action,some_target) = n1 ),
inference(copy,[status(thm)],[c_1904]) ).
cnf(c_1905,plain,
( sK1(rho1,some_action,some_target) = n1
| sK0(rho1,some_action,some_target,l) = l
| sK1(rho1,some_action,some_target) = n1 ),
inference(resolve,[status(thm)],[c_1866,c_1492]) ).
cnf(c_1869,plain,
( sK0(rho1,some_action,some_target,l) = l
| sK1(rho1,some_action,some_target) = n1 ),
inference(copy,[status(thm)],[c_1905]) ).
cnf(c_1906,plain,
( sK1(rho1,some_action,some_target) = n1
| sK1(rho1,some_action,some_target) = n1 ),
inference(resolve,[status(thm)],[c_1869,c_1087]) ).
cnf(c_1871,plain,
sK1(rho1,some_action,some_target) = n1,
inference(copy,[status(thm)],[c_1906]) ).
cnf(c_1907,plain,
( sK1(rho1,some_action,some_target) = n2
| sK0(rho1,some_action,some_target,l) = l
| ~ permission(sK0(rho1,some_action,some_target,l))
| sK1(rho1,some_action,some_target) = n2 ),
inference(resolve,[status(thm)],[c_1332,c_1397]) ).
cnf(c_1873,plain,
( sK0(rho1,some_action,some_target,l) = l
| ~ permission(sK0(rho1,some_action,some_target,l))
| sK1(rho1,some_action,some_target) = n2 ),
inference(copy,[status(thm)],[c_1907]) ).
cnf(c_1908,plain,
( sK1(rho1,some_action,some_target) = n2
| sK0(rho1,some_action,some_target,l) = l
| sK1(rho1,some_action,some_target) = n2 ),
inference(resolve,[status(thm)],[c_1873,c_1493]) ).
cnf(c_1875,plain,
( sK0(rho1,some_action,some_target,l) = l
| sK1(rho1,some_action,some_target) = n2 ),
inference(copy,[status(thm)],[c_1908]) ).
cnf(c_1909,plain,
( sK1(rho1,some_action,some_target) = n2
| sK1(rho1,some_action,some_target) = n2 ),
inference(resolve,[status(thm)],[c_1875,c_1088]) ).
cnf(c_1876,plain,
sK1(rho1,some_action,some_target) = n2,
inference(copy,[status(thm)],[c_1909]) ).
cnf(c_1910,plain,
n2 = n1,
inference(paramod,[status(thm)],[c_1876,c_1871]) ).
cnf(c_1877,plain,
$false,
inference(resolve,[status(thm)],[c_38,c_1910]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.36 % Computer : n019.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Sat Sep 26 00:14:40 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/5.37 % Process 4060254 was started by sandbox on n019,
% 0.08/5.37 % Sat Sep 26 00:14:40 2026
% 0.08/5.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/5.38
% 0.08/5.38 % From the command line: assign(max_seconds, 300).
% 0.14/5.53
% 0.14/5.53 % SZS status Unsatisfiable for theBenchmark
% 0.14/5.53
% 0.14/5.53 % Proof 1 at 0.10 (+ 0.03) seconds.
% 0.14/5.53 % Length of proof is 48.
% 0.14/5.53 % Level of proof is 10.
% 0.14/5.53 % Maximum clause weight is 42.000.
% 0.14/5.53 % Given clauses 301.
% 0.14/5.53
% 0.14/5.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------