%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:11:59 PM UTC 2026
% Result : Unsatisfiable 3.71s 0.93s
% Output : Proof 3.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of formulae : 102 ( 39 unt; 0 def)
% Number of atoms : 382 ( 99 equ)
% Maximal formula atoms : 29 ( 3 avg)
% Number of connectives : 473 ( 193 ~; 237 |; 38 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 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 : 95 ( 0 sgn 22 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_correlativity_permission) ).
fof(f0_nnf,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) ) )
& ( ? [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(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [Rho,L,A,T,M,L2,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 = 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)) ) )
& ( ( ( M = sk1(Rho,A,T)
| ~ cnt(M,A,T)
| ~ part_of(M,Rho)
| ~ no_right(M) )
& cnt(sk1(Rho,A,T),A,T)
& part_of(sk1(Rho,A,T),Rho)
& no_right(sk1(Rho,A,T)) )
| ( sk0(Rho,A,T,L) != L
& cnt(sk0(Rho,A,T,L),A,T)
& part_of(sk0(Rho,A,T,L),Rho)
& permission(sk0(Rho,A,T,L)) )
| ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L) ) )
| ~ odrl_rel(Rho) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f0_nnf]) ).
cnf(c11,plain,
( X6 = sk1(X0,X1,X2)
| ~ cnt(X6,X1,X2)
| ~ part_of(X6,X0)
| ~ no_right(X6)
| cnt(sk0(X0,X1,X2,X3),X1,X2)
| ~ cnt(X3,X1,X2)
| ~ part_of(X3,X0)
| ~ permission(X3)
| ~ odrl_rel(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f5,axiom,
odrl_rel(rho1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',odrl_rho1) ).
fof(f5_nnf,plain,
odrl_rel(rho1),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c36,plain,
odrl_rel(rho1),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(p99,plain,
( X3 = sk1(rho1,X1,X2)
| ~ cnt(X3,X1,X2)
| ~ part_of(X3,rho1)
| ~ no_right(X3)
| cnt(sk0(rho1,X1,X2,X0),X1,X2)
| ~ cnt(X0,X1,X2)
| ~ part_of(X0,rho1)
| ~ permission(X0) ),
inference(resolution,[status(thm)],[c11,c36]) ).
fof(f6,axiom,
permission(l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permission_l) ).
fof(f6_nnf,plain,
permission(l),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c37,plain,
permission(l),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(p342,plain,
( X2 = sk1(rho1,X0,X1)
| ~ cnt(X2,X0,X1)
| ~ part_of(X2,rho1)
| ~ no_right(X2)
| cnt(sk0(rho1,X0,X1,l),X0,X1)
| ~ cnt(l,X0,X1)
| ~ part_of(l,rho1) ),
inference(resolution,[status(thm)],[p99,c37]) ).
fof(f9,axiom,
part_of(l,rho1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',partof_l) ).
fof(f9_nnf,plain,
part_of(l,rho1),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c40,plain,
part_of(l,rho1),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(p1135,plain,
( X2 = sk1(rho1,X0,X1)
| ~ cnt(X2,X0,X1)
| ~ part_of(X2,rho1)
| ~ no_right(X2)
| cnt(sk0(rho1,X0,X1,l),X0,X1)
| ~ cnt(l,X0,X1) ),
inference(resolution,[status(thm)],[p342,c40]) ).
fof(f12,axiom,
cnt(l,some_action,some_target),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cnt_l) ).
fof(f12_nnf,plain,
cnt(l,some_action,some_target),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c43,plain,
cnt(l,some_action,some_target),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(p1140,plain,
( X0 = sk1(rho1,some_action,some_target)
| ~ cnt(X0,some_action,some_target)
| ~ part_of(X0,rho1)
| ~ no_right(X0)
| cnt(sk0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolution,[status(thm)],[p1135,c43]) ).
fof(f7,axiom,
no_right(n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_right_n1) ).
fof(f7_nnf,plain,
no_right(n1),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c38,plain,
no_right(n1),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(p1141,plain,
( n1 = sk1(rho1,some_action,some_target)
| ~ cnt(n1,some_action,some_target)
| ~ part_of(n1,rho1)
| cnt(sk0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolution,[status(thm)],[p1140,c38]) ).
fof(f10,axiom,
part_of(n1,rho1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',partof_n1) ).
fof(f10_nnf,plain,
part_of(n1,rho1),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c41,plain,
part_of(n1,rho1),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(p1157,plain,
( n1 = sk1(rho1,some_action,some_target)
| ~ cnt(n1,some_action,some_target)
| cnt(sk0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolution,[status(thm)],[p1141,c41]) ).
fof(f13,axiom,
cnt(n1,some_action,some_target),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cnt_n1) ).
fof(f13_nnf,plain,
cnt(n1,some_action,some_target),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c44,plain,
cnt(n1,some_action,some_target),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(p1158,plain,
( n1 = sk1(rho1,some_action,some_target)
| cnt(sk0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolution,[status(thm)],[p1157,c44]) ).
cnf(c7,plain,
( X6 = sk1(X0,X1,X2)
| ~ cnt(X6,X1,X2)
| ~ part_of(X6,X0)
| ~ no_right(X6)
| part_of(sk0(X0,X1,X2,X3),X0)
| ~ cnt(X3,X1,X2)
| ~ part_of(X3,X0)
| ~ permission(X3)
| ~ odrl_rel(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p77,plain,
( X3 = sk1(rho1,X1,X2)
| ~ cnt(X3,X1,X2)
| ~ part_of(X3,rho1)
| ~ no_right(X3)
| part_of(sk0(rho1,X1,X2,X0),rho1)
| ~ cnt(X0,X1,X2)
| ~ part_of(X0,rho1)
| ~ permission(X0) ),
inference(resolution,[status(thm)],[c7,c36]) ).
cnf(p312,plain,
( X2 = sk1(rho1,X0,X1)
| ~ cnt(X2,X0,X1)
| ~ part_of(X2,rho1)
| ~ no_right(X2)
| part_of(sk0(rho1,X0,X1,l),rho1)
| ~ cnt(l,X0,X1)
| ~ part_of(l,rho1) ),
inference(resolution,[status(thm)],[p77,c37]) ).
cnf(p877,plain,
( X2 = sk1(rho1,X0,X1)
| ~ cnt(X2,X0,X1)
| ~ part_of(X2,rho1)
| ~ no_right(X2)
| part_of(sk0(rho1,X0,X1,l),rho1)
| ~ cnt(l,X0,X1) ),
inference(resolution,[status(thm)],[p312,c40]) ).
cnf(p878,plain,
( X0 = sk1(rho1,some_action,some_target)
| ~ cnt(X0,some_action,some_target)
| ~ part_of(X0,rho1)
| ~ no_right(X0)
| part_of(sk0(rho1,some_action,some_target,l),rho1) ),
inference(resolution,[status(thm)],[p877,c43]) ).
cnf(p879,plain,
( n1 = sk1(rho1,some_action,some_target)
| ~ cnt(n1,some_action,some_target)
| ~ part_of(n1,rho1)
| part_of(sk0(rho1,some_action,some_target,l),rho1) ),
inference(resolution,[status(thm)],[p878,c38]) ).
cnf(p903,plain,
( n1 = sk1(rho1,some_action,some_target)
| ~ cnt(n1,some_action,some_target)
| part_of(sk0(rho1,some_action,some_target,l),rho1) ),
inference(resolution,[status(thm)],[p879,c41]) ).
cnf(p905,plain,
( n1 = sk1(rho1,some_action,some_target)
| part_of(sk0(rho1,some_action,some_target,l),rho1) ),
inference(resolution,[status(thm)],[p903,c44]) ).
cnf(c3,plain,
( X6 = sk1(X0,X1,X2)
| ~ cnt(X6,X1,X2)
| ~ part_of(X6,X0)
| ~ no_right(X6)
| permission(sk0(X0,X1,X2,X3))
| ~ cnt(X3,X1,X2)
| ~ part_of(X3,X0)
| ~ permission(X3)
| ~ odrl_rel(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p55,plain,
( X3 = sk1(rho1,X1,X2)
| ~ cnt(X3,X1,X2)
| ~ part_of(X3,rho1)
| ~ no_right(X3)
| permission(sk0(rho1,X1,X2,X0))
| ~ cnt(X0,X1,X2)
| ~ part_of(X0,rho1)
| ~ permission(X0) ),
inference(resolution,[status(thm)],[c3,c36]) ).
cnf(p246,plain,
( X2 = sk1(rho1,X0,X1)
| ~ cnt(X2,X0,X1)
| ~ part_of(X2,rho1)
| ~ no_right(X2)
| permission(sk0(rho1,X0,X1,l))
| ~ cnt(l,X0,X1)
| ~ part_of(l,rho1) ),
inference(resolution,[status(thm)],[p55,c37]) ).
cnf(p463,plain,
( X2 = sk1(rho1,X0,X1)
| ~ cnt(X2,X0,X1)
| ~ part_of(X2,rho1)
| ~ no_right(X2)
| permission(sk0(rho1,X0,X1,l))
| ~ cnt(l,X0,X1) ),
inference(resolution,[status(thm)],[p246,c40]) ).
cnf(p465,plain,
( X0 = sk1(rho1,some_action,some_target)
| ~ cnt(X0,some_action,some_target)
| ~ part_of(X0,rho1)
| ~ no_right(X0)
| permission(sk0(rho1,some_action,some_target,l)) ),
inference(resolution,[status(thm)],[p463,c43]) ).
cnf(p466,plain,
( n1 = sk1(rho1,some_action,some_target)
| ~ cnt(n1,some_action,some_target)
| ~ part_of(n1,rho1)
| permission(sk0(rho1,some_action,some_target,l)) ),
inference(resolution,[status(thm)],[p465,c38]) ).
cnf(p477,plain,
( n1 = sk1(rho1,some_action,some_target)
| ~ cnt(n1,some_action,some_target)
| permission(sk0(rho1,some_action,some_target,l)) ),
inference(resolution,[status(thm)],[p466,c41]) ).
cnf(p478,plain,
( n1 = sk1(rho1,some_action,some_target)
| permission(sk0(rho1,some_action,some_target,l)) ),
inference(resolution,[status(thm)],[p477,c44]) ).
fof(f18,axiom,
! [L2] :
( ( cnt(L2,some_action,some_target)
& part_of(L2,rho1)
& permission(L2) )
=> L2 = l ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',perm_l_unique) ).
fof(f18_nnf,plain,
! [L2] :
( L2 = l
| ~ cnt(L2,some_action,some_target)
| ~ part_of(L2,rho1)
| ~ permission(L2) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [L2] :
( L2 = l
| ~ cnt(L2,some_action,some_target)
| ~ part_of(L2,rho1)
| ~ permission(L2) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c49,plain,
( X0 = l
| ~ cnt(X0,some_action,some_target)
| ~ part_of(X0,rho1)
| ~ permission(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p481,plain,
( sk0(rho1,some_action,some_target,l) = l
| ~ cnt(sk0(rho1,some_action,some_target,l),some_action,some_target)
| ~ part_of(sk0(rho1,some_action,some_target,l),rho1)
| n1 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p478,c49]) ).
cnf(p906,plain,
( sk0(rho1,some_action,some_target,l) = l
| ~ cnt(sk0(rho1,some_action,some_target,l),some_action,some_target)
| n1 = sk1(rho1,some_action,some_target)
| n1 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p905,p481]) ).
cnf(p916,plain,
( sk0(rho1,some_action,some_target,l) = l
| ~ cnt(sk0(rho1,some_action,some_target,l),some_action,some_target)
| n1 = sk1(rho1,some_action,some_target) ),
inference(factoring,[status(thm)],[p906]) ).
cnf(p1164,plain,
( sk0(rho1,some_action,some_target,l) = l
| n1 = sk1(rho1,some_action,some_target)
| n1 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p1158,p916]) ).
cnf(p1166,plain,
( sk0(rho1,some_action,some_target,l) = l
| n1 = sk1(rho1,some_action,some_target) ),
inference(factoring,[status(thm)],[p1164]) ).
cnf(c15,plain,
( X6 = sk1(X0,X1,X2)
| ~ cnt(X6,X1,X2)
| ~ part_of(X6,X0)
| ~ no_right(X6)
| sk0(X0,X1,X2,X3) != X3
| ~ cnt(X3,X1,X2)
| ~ part_of(X3,X0)
| ~ permission(X3)
| ~ odrl_rel(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p122,plain,
( X3 = sk1(rho1,X1,X2)
| ~ cnt(X3,X1,X2)
| ~ part_of(X3,rho1)
| ~ no_right(X3)
| sk0(rho1,X1,X2,X0) != X0
| ~ cnt(X0,X1,X2)
| ~ part_of(X0,rho1)
| ~ permission(X0) ),
inference(resolution,[status(thm)],[c15,c36]) ).
cnf(p372,plain,
( X2 = sk1(rho1,X0,X1)
| ~ cnt(X2,X0,X1)
| ~ part_of(X2,rho1)
| ~ no_right(X2)
| sk0(rho1,X0,X1,l) != l
| ~ cnt(l,X0,X1)
| ~ part_of(l,rho1) ),
inference(resolution,[status(thm)],[p122,c37]) ).
cnf(p973,plain,
( X2 = sk1(rho1,X0,X1)
| ~ cnt(X2,X0,X1)
| ~ part_of(X2,rho1)
| ~ no_right(X2)
| sk0(rho1,X0,X1,l) != l
| ~ cnt(l,X0,X1) ),
inference(resolution,[status(thm)],[p372,c40]) ).
cnf(p974,plain,
( X0 = sk1(rho1,some_action,some_target)
| ~ cnt(X0,some_action,some_target)
| ~ part_of(X0,rho1)
| ~ no_right(X0)
| sk0(rho1,some_action,some_target,l) != l ),
inference(resolution,[status(thm)],[p973,c43]) ).
cnf(p1169,plain,
( X0 = sk1(rho1,some_action,some_target)
| ~ cnt(X0,some_action,some_target)
| ~ part_of(X0,rho1)
| ~ no_right(X0)
| n1 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p1166,p974]) ).
cnf(p1231,plain,
( ~ cnt(n1,some_action,some_target)
| ~ part_of(n1,rho1)
| ~ no_right(n1)
| n1 = sk1(rho1,some_action,some_target) ),
inference(factoring,[status(thm)],[p1169]) ).
cnf(p1244,plain,
( ~ cnt(n1,some_action,some_target)
| ~ part_of(n1,rho1)
| n1 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p1231,c38]) ).
cnf(p1245,plain,
( ~ cnt(n1,some_action,some_target)
| n1 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p1244,c41]) ).
cnf(p1246,plain,
n1 = sk1(rho1,some_action,some_target),
inference(resolution,[status(thm)],[p1245,c44]) ).
fof(f8,axiom,
no_right(n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_right_n2) ).
fof(f8_nnf,plain,
no_right(n2),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c39,plain,
no_right(n2),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(p1142,plain,
( n2 = sk1(rho1,some_action,some_target)
| ~ cnt(n2,some_action,some_target)
| ~ part_of(n2,rho1)
| cnt(sk0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolution,[status(thm)],[p1140,c39]) ).
fof(f11,axiom,
part_of(n2,rho1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',partof_n2) ).
fof(f11_nnf,plain,
part_of(n2,rho1),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c42,plain,
part_of(n2,rho1),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(p1202,plain,
( n2 = sk1(rho1,some_action,some_target)
| ~ cnt(n2,some_action,some_target)
| cnt(sk0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolution,[status(thm)],[p1142,c42]) ).
fof(f14,axiom,
cnt(n2,some_action,some_target),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cnt_n2) ).
fof(f14_nnf,plain,
cnt(n2,some_action,some_target),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c45,plain,
cnt(n2,some_action,some_target),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(p1203,plain,
( n2 = sk1(rho1,some_action,some_target)
| cnt(sk0(rho1,some_action,some_target,l),some_action,some_target) ),
inference(resolution,[status(thm)],[p1202,c45]) ).
cnf(p880,plain,
( n2 = sk1(rho1,some_action,some_target)
| ~ cnt(n2,some_action,some_target)
| ~ part_of(n2,rho1)
| part_of(sk0(rho1,some_action,some_target,l),rho1) ),
inference(resolution,[status(thm)],[p878,c39]) ).
cnf(p908,plain,
( n2 = sk1(rho1,some_action,some_target)
| ~ cnt(n2,some_action,some_target)
| part_of(sk0(rho1,some_action,some_target,l),rho1) ),
inference(resolution,[status(thm)],[p880,c42]) ).
cnf(p909,plain,
( n2 = sk1(rho1,some_action,some_target)
| part_of(sk0(rho1,some_action,some_target,l),rho1) ),
inference(resolution,[status(thm)],[p908,c45]) ).
cnf(p467,plain,
( n2 = sk1(rho1,some_action,some_target)
| ~ cnt(n2,some_action,some_target)
| ~ part_of(n2,rho1)
| permission(sk0(rho1,some_action,some_target,l)) ),
inference(resolution,[status(thm)],[p465,c39]) ).
cnf(p502,plain,
( n2 = sk1(rho1,some_action,some_target)
| ~ cnt(n2,some_action,some_target)
| permission(sk0(rho1,some_action,some_target,l)) ),
inference(resolution,[status(thm)],[p467,c42]) ).
cnf(p503,plain,
( n2 = sk1(rho1,some_action,some_target)
| permission(sk0(rho1,some_action,some_target,l)) ),
inference(resolution,[status(thm)],[p502,c45]) ).
cnf(p504,plain,
( sk0(rho1,some_action,some_target,l) = l
| ~ cnt(sk0(rho1,some_action,some_target,l),some_action,some_target)
| ~ part_of(sk0(rho1,some_action,some_target,l),rho1)
| n2 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p503,c49]) ).
cnf(p915,plain,
( sk0(rho1,some_action,some_target,l) = l
| ~ cnt(sk0(rho1,some_action,some_target,l),some_action,some_target)
| n2 = sk1(rho1,some_action,some_target)
| n2 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p909,p504]) ).
cnf(p941,plain,
( sk0(rho1,some_action,some_target,l) = l
| ~ cnt(sk0(rho1,some_action,some_target,l),some_action,some_target)
| n2 = sk1(rho1,some_action,some_target) ),
inference(factoring,[status(thm)],[p915]) ).
cnf(p1204,plain,
( sk0(rho1,some_action,some_target,l) = l
| n2 = sk1(rho1,some_action,some_target)
| n2 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p1203,p941]) ).
cnf(p1209,plain,
( sk0(rho1,some_action,some_target,l) = l
| n2 = sk1(rho1,some_action,some_target) ),
inference(factoring,[status(thm)],[p1204]) ).
cnf(p1212,plain,
( X0 = sk1(rho1,some_action,some_target)
| ~ cnt(X0,some_action,some_target)
| ~ part_of(X0,rho1)
| ~ no_right(X0)
| n2 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p1209,p974]) ).
cnf(p1311,plain,
( ~ cnt(n2,some_action,some_target)
| ~ part_of(n2,rho1)
| ~ no_right(n2)
| n2 = sk1(rho1,some_action,some_target) ),
inference(factoring,[status(thm)],[p1212]) ).
cnf(p1328,plain,
( ~ cnt(n2,some_action,some_target)
| ~ part_of(n2,rho1)
| n2 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p1311,c39]) ).
cnf(p1329,plain,
( ~ cnt(n2,some_action,some_target)
| n2 = sk1(rho1,some_action,some_target) ),
inference(resolution,[status(thm)],[p1328,c42]) ).
cnf(p1330,plain,
n2 = sk1(rho1,some_action,some_target),
inference(resolution,[status(thm)],[p1329,c45]) ).
cnf(p1373,plain,
n2 = n1,
inference(superposition,[status(thm)],[p1246,p1330]) ).
fof(f17,axiom,
n1 != n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n1_neq_n2) ).
fof(f17_nnf,plain,
n1 != n2,
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
n1 != n2,
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c48,plain,
n1 != n2,
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p1374,plain,
n1 != n1,
inference(demodulation,[status(thm)],[p1373,c48]) ).
cnf(p1380,plain,
$false,
inference(equality_resolution,[status(thm)],[p1374]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 01:25:19 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 3.71/0.93 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.71/0.93 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------