%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n012.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:16:19 AM UTC 2026
% Result : Unsatisfiable 0.09s 0.33s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 19
% Syntax : Number of formulae : 105 ( 41 unt; 1 def)
% Number of atoms : 388 ( 65 equ)
% Maximal formula atoms : 39 ( 3 avg)
% Number of connectives : 484 ( 201 ~; 226 |; 47 &)
% ( 6 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-4 aty)
% Number of variables : 111 ( 1 sgn 63 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax_correlativity_permission,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 ) ) ) ) ).
fof(odrl_rho1,axiom,
odrl_rel(rho1) ).
fof(permission_l,axiom,
permission(l) ).
fof(no_right_n1,axiom,
no_right(n1) ).
fof(no_right_n2,axiom,
no_right(n2) ).
fof(partof_l,axiom,
part_of(l,rho1) ).
fof(partof_n1,axiom,
part_of(n1,rho1) ).
fof(partof_n2,axiom,
part_of(n2,rho1) ).
fof(cnt_l,axiom,
cnt(l,some_action,some_target) ).
fof(cnt_n1,axiom,
cnt(n1,some_action,some_target) ).
fof(cnt_n2,axiom,
cnt(n2,some_action,some_target) ).
fof(n1_neq_n2,axiom,
n1 != n2 ).
fof(perm_l_unique,axiom,
! [L2] :
( ( permission(L2)
& part_of(L2,rho1)
& cnt(L2,some_action,some_target) )
=> L2 = l ) ).
fof(definition_0,definition,
! [A,L,Rho,T] :
( definitionFOFtoCNF_0(A,L,Rho,T)
<=> ( cnt(L,A,T)
& part_of(L,Rho)
& permission(L)
& ! [L2] :
( ~ cnt(L2,A,T)
| ~ part_of(L2,Rho)
| ~ permission(L2)
| L2 = L ) ) ) ).
fof(normalize_0_0,plain,
cnt(n2,some_action,some_target),
inference(canonicalize,[],[cnt_n2]) ).
fof(normalize_0_1,plain,
! [A,L,Rho,T] :
( ~ definitionFOFtoCNF_0(A,L,Rho,T)
<=> ( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| ? [L2] :
( L2 != L
& cnt(L2,A,T)
& part_of(L2,Rho)
& permission(L2) ) ) ),
inference(canonicalize,[],[definition_0]) ).
fof(normalize_0_2,plain,
! [A,L,L2,Rho,T] :
( ( ~ definitionFOFtoCNF_0(A,L,Rho,T)
| cnt(L,A,T) )
& ( ~ definitionFOFtoCNF_0(A,L,Rho,T)
| part_of(L,Rho) )
& ( ~ definitionFOFtoCNF_0(A,L,Rho,T)
| permission(L) )
& ( skolemFOFtoCNF_L2(A,L,Rho,T) != L
| ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T) )
& ( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| cnt(skolemFOFtoCNF_L2(A,L,Rho,T),A,T)
| definitionFOFtoCNF_0(A,L,Rho,T) )
& ( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T)
| part_of(skolemFOFtoCNF_L2(A,L,Rho,T),Rho) )
& ( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T)
| permission(skolemFOFtoCNF_L2(A,L,Rho,T)) )
& ( ~ cnt(L2,A,T)
| ~ definitionFOFtoCNF_0(A,L,Rho,T)
| ~ part_of(L2,Rho)
| ~ permission(L2)
| L2 = L ) ),
inference(clausify,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
! [A,L,Rho,T] :
( skolemFOFtoCNF_L2(A,L,Rho,T) != L
| ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T) ),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
part_of(l,rho1),
inference(canonicalize,[],[partof_l]) ).
fof(normalize_0_5,plain,
cnt(l,some_action,some_target),
inference(canonicalize,[],[cnt_l]) ).
fof(normalize_0_6,plain,
! [A,L,Rho,T] :
( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T)
| permission(skolemFOFtoCNF_L2(A,L,Rho,T)) ),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_7,plain,
permission(l),
inference(canonicalize,[],[permission_l]) ).
fof(normalize_0_8,plain,
! [L2] :
( ~ cnt(L2,some_action,some_target)
| ~ part_of(L2,rho1)
| ~ permission(L2)
| L2 = l ),
inference(canonicalize,[],[perm_l_unique]) ).
fof(normalize_0_9,plain,
! [L2] :
( ~ cnt(L2,some_action,some_target)
| ~ part_of(L2,rho1)
| ~ permission(L2)
| L2 = l ),
inference(specialize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [A,L,Rho,T] :
( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| cnt(skolemFOFtoCNF_L2(A,L,Rho,T),A,T)
| definitionFOFtoCNF_0(A,L,Rho,T) ),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_11,plain,
! [A,L,Rho,T] :
( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T)
| part_of(skolemFOFtoCNF_L2(A,L,Rho,T),Rho) ),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_12,plain,
! [Rho] :
( ~ odrl_rel(Rho)
| ! [A,T] :
( ? [L] :
( cnt(L,A,T)
& part_of(L,Rho)
& permission(L)
& ! [L2] :
( ~ cnt(L2,A,T)
| ~ part_of(L2,Rho)
| ~ permission(L2)
| L2 = L ) )
<=> ? [N] :
( cnt(N,A,T)
& no_right(N)
& part_of(N,Rho)
& ! [M] :
( ~ cnt(M,A,T)
| ~ no_right(M)
| ~ part_of(M,Rho)
| M = N ) ) ) ),
inference(canonicalize,[],[ax_correlativity_permission]) ).
fof(normalize_0_13,plain,
! [Rho] :
( ~ odrl_rel(Rho)
| ! [A,T] :
( ? [L] :
( cnt(L,A,T)
& part_of(L,Rho)
& permission(L)
& ! [L2] :
( ~ cnt(L2,A,T)
| ~ part_of(L2,Rho)
| ~ permission(L2)
| L2 = L ) )
<=> ? [N] :
( cnt(N,A,T)
& no_right(N)
& part_of(N,Rho)
& ! [M] :
( ~ cnt(M,A,T)
| ~ no_right(M)
| ~ part_of(M,Rho)
| M = N ) ) ) ),
inference(specialize,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [Rho] :
( ~ odrl_rel(Rho)
| ! [A,T] :
( ? [L] : definitionFOFtoCNF_0(A,L,Rho,T)
<=> ? [N] :
( cnt(N,A,T)
& no_right(N)
& part_of(N,Rho)
& ! [M] :
( ~ cnt(M,A,T)
| ~ no_right(M)
| ~ part_of(M,Rho)
| M = N ) ) ) ),
inference(simplify,[],[normalize_0_13,normalize_0_1]) ).
fof(normalize_0_15,plain,
! [A,L,M,N,Rho,T] :
( ( ~ definitionFOFtoCNF_0(A,L,Rho,T)
| ~ odrl_rel(Rho)
| cnt(skolemFOFtoCNF_N(A,Rho,T),A,T) )
& ( ~ definitionFOFtoCNF_0(A,L,Rho,T)
| ~ odrl_rel(Rho)
| no_right(skolemFOFtoCNF_N(A,Rho,T)) )
& ( ~ definitionFOFtoCNF_0(A,L,Rho,T)
| ~ odrl_rel(Rho)
| part_of(skolemFOFtoCNF_N(A,Rho,T),Rho) )
& ( skolemFOFtoCNF_M(A,N,Rho,T) != N
| ~ cnt(N,A,T)
| ~ no_right(N)
| ~ odrl_rel(Rho)
| ~ part_of(N,Rho)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,Rho,T),Rho,T) )
& ( ~ cnt(M,A,T)
| ~ definitionFOFtoCNF_0(A,L,Rho,T)
| ~ no_right(M)
| ~ odrl_rel(Rho)
| ~ part_of(M,Rho)
| M = skolemFOFtoCNF_N(A,Rho,T) )
& ( ~ cnt(N,A,T)
| ~ no_right(N)
| ~ odrl_rel(Rho)
| ~ part_of(N,Rho)
| cnt(skolemFOFtoCNF_M(A,N,Rho,T),A,T)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,Rho,T),Rho,T) )
& ( ~ cnt(N,A,T)
| ~ no_right(N)
| ~ odrl_rel(Rho)
| ~ part_of(N,Rho)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,Rho,T),Rho,T)
| no_right(skolemFOFtoCNF_M(A,N,Rho,T)) )
& ( ~ cnt(N,A,T)
| ~ no_right(N)
| ~ odrl_rel(Rho)
| ~ part_of(N,Rho)
| definitionFOFtoCNF_0(A,skolemFOFtoCNF_L(A,Rho,T),Rho,T)
| part_of(skolemFOFtoCNF_M(A,N,Rho,T),Rho) ) ),
inference(clausify,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
! [A,L,M,Rho,T] :
( ~ cnt(M,A,T)
| ~ definitionFOFtoCNF_0(A,L,Rho,T)
| ~ no_right(M)
| ~ odrl_rel(Rho)
| ~ part_of(M,Rho)
| M = skolemFOFtoCNF_N(A,Rho,T) ),
inference(conjunct,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
odrl_rel(rho1),
inference(canonicalize,[],[odrl_rho1]) ).
fof(normalize_0_18,plain,
cnt(n1,some_action,some_target),
inference(canonicalize,[],[cnt_n1]) ).
fof(normalize_0_19,plain,
no_right(n1),
inference(canonicalize,[],[no_right_n1]) ).
fof(normalize_0_20,plain,
part_of(n1,rho1),
inference(canonicalize,[],[partof_n1]) ).
fof(normalize_0_21,plain,
no_right(n2),
inference(canonicalize,[],[no_right_n2]) ).
fof(normalize_0_22,plain,
part_of(n2,rho1),
inference(canonicalize,[],[partof_n2]) ).
fof(normalize_0_23,plain,
n1 != n2,
inference(canonicalize,[],[n1_neq_n2]) ).
cnf(refute_0_0,plain,
cnt(n2,some_action,some_target),
inference(canonicalize,[],[normalize_0_0]) ).
cnf(refute_0_1,plain,
( skolemFOFtoCNF_L2(A,L,Rho,T) != L
| ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T) ),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_2,plain,
( skolemFOFtoCNF_L2(some_action,l,rho1,some_target) != l
| ~ cnt(l,some_action,some_target)
| ~ part_of(l,rho1)
| ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(subst,[],[refute_0_1:[bind(A,$fot(some_action)),bind(L,$fot(l)),bind(Rho,$fot(rho1)),bind(T,$fot(some_target))]]) ).
cnf(refute_0_3,plain,
part_of(l,rho1),
inference(canonicalize,[],[normalize_0_4]) ).
cnf(refute_0_4,plain,
cnt(l,some_action,some_target),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_5,plain,
( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T)
| permission(skolemFOFtoCNF_L2(A,L,Rho,T)) ),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_6,plain,
( ~ cnt(l,some_action,some_target)
| ~ part_of(l,X_27)
| ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,X_27,some_target)
| permission(skolemFOFtoCNF_L2(some_action,l,X_27,some_target)) ),
inference(subst,[],[refute_0_5:[bind(A,$fot(some_action)),bind(L,$fot(l)),bind(Rho,$fot(X_27)),bind(T,$fot(some_target))]]) ).
cnf(refute_0_7,plain,
( ~ part_of(l,X_27)
| ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,X_27,some_target)
| permission(skolemFOFtoCNF_L2(some_action,l,X_27,some_target)) ),
inference(resolve,[$cnf( cnt(l,some_action,some_target) )],[refute_0_4,refute_0_6]) ).
cnf(refute_0_8,plain,
permission(l),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_9,plain,
( ~ part_of(l,X_27)
| definitionFOFtoCNF_0(some_action,l,X_27,some_target)
| permission(skolemFOFtoCNF_L2(some_action,l,X_27,some_target)) ),
inference(resolve,[$cnf( permission(l) )],[refute_0_8,refute_0_7]) ).
cnf(refute_0_10,plain,
( ~ part_of(l,rho1)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target)
| permission(skolemFOFtoCNF_L2(some_action,l,rho1,some_target)) ),
inference(subst,[],[refute_0_9:[bind(X_27,$fot(rho1))]]) ).
cnf(refute_0_11,plain,
( definitionFOFtoCNF_0(some_action,l,rho1,some_target)
| permission(skolemFOFtoCNF_L2(some_action,l,rho1,some_target)) ),
inference(resolve,[$cnf( part_of(l,rho1) )],[refute_0_3,refute_0_10]) ).
cnf(refute_0_12,plain,
( ~ cnt(L2,some_action,some_target)
| ~ part_of(L2,rho1)
| ~ permission(L2)
| L2 = l ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_13,plain,
( ~ cnt(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),some_action,some_target)
| ~ part_of(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),rho1)
| ~ permission(skolemFOFtoCNF_L2(some_action,l,rho1,some_target))
| skolemFOFtoCNF_L2(some_action,l,rho1,some_target) = l ),
inference(subst,[],[refute_0_12:[bind(L2,$fot(skolemFOFtoCNF_L2(some_action,l,rho1,some_target)))]]) ).
cnf(refute_0_14,plain,
( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| cnt(skolemFOFtoCNF_L2(A,L,Rho,T),A,T)
| definitionFOFtoCNF_0(A,L,Rho,T) ),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_15,plain,
( ~ cnt(l,some_action,some_target)
| ~ part_of(l,X_39)
| ~ permission(l)
| cnt(skolemFOFtoCNF_L2(some_action,l,X_39,some_target),some_action,some_target)
| definitionFOFtoCNF_0(some_action,l,X_39,some_target) ),
inference(subst,[],[refute_0_14:[bind(A,$fot(some_action)),bind(L,$fot(l)),bind(Rho,$fot(X_39)),bind(T,$fot(some_target))]]) ).
cnf(refute_0_16,plain,
( ~ part_of(l,X_39)
| ~ permission(l)
| cnt(skolemFOFtoCNF_L2(some_action,l,X_39,some_target),some_action,some_target)
| definitionFOFtoCNF_0(some_action,l,X_39,some_target) ),
inference(resolve,[$cnf( cnt(l,some_action,some_target) )],[refute_0_4,refute_0_15]) ).
cnf(refute_0_17,plain,
( ~ part_of(l,X_39)
| cnt(skolemFOFtoCNF_L2(some_action,l,X_39,some_target),some_action,some_target)
| definitionFOFtoCNF_0(some_action,l,X_39,some_target) ),
inference(resolve,[$cnf( permission(l) )],[refute_0_8,refute_0_16]) ).
cnf(refute_0_18,plain,
( ~ part_of(l,rho1)
| cnt(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),some_action,some_target)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(subst,[],[refute_0_17:[bind(X_39,$fot(rho1))]]) ).
cnf(refute_0_19,plain,
( cnt(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),some_action,some_target)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( part_of(l,rho1) )],[refute_0_3,refute_0_18]) ).
cnf(refute_0_20,plain,
( ~ part_of(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),rho1)
| ~ permission(skolemFOFtoCNF_L2(some_action,l,rho1,some_target))
| skolemFOFtoCNF_L2(some_action,l,rho1,some_target) = l
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),some_action,some_target) )],[refute_0_19,refute_0_13]) ).
cnf(refute_0_21,plain,
( ~ cnt(L,A,T)
| ~ part_of(L,Rho)
| ~ permission(L)
| definitionFOFtoCNF_0(A,L,Rho,T)
| part_of(skolemFOFtoCNF_L2(A,L,Rho,T),Rho) ),
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_22,plain,
( ~ cnt(l,some_action,some_target)
| ~ part_of(l,X_50)
| ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,X_50,some_target)
| part_of(skolemFOFtoCNF_L2(some_action,l,X_50,some_target),X_50) ),
inference(subst,[],[refute_0_21:[bind(A,$fot(some_action)),bind(L,$fot(l)),bind(Rho,$fot(X_50)),bind(T,$fot(some_target))]]) ).
cnf(refute_0_23,plain,
( ~ part_of(l,X_50)
| ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,X_50,some_target)
| part_of(skolemFOFtoCNF_L2(some_action,l,X_50,some_target),X_50) ),
inference(resolve,[$cnf( cnt(l,some_action,some_target) )],[refute_0_4,refute_0_22]) ).
cnf(refute_0_24,plain,
( ~ part_of(l,X_50)
| definitionFOFtoCNF_0(some_action,l,X_50,some_target)
| part_of(skolemFOFtoCNF_L2(some_action,l,X_50,some_target),X_50) ),
inference(resolve,[$cnf( permission(l) )],[refute_0_8,refute_0_23]) ).
cnf(refute_0_25,plain,
( ~ part_of(l,rho1)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target)
| part_of(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),rho1) ),
inference(subst,[],[refute_0_24:[bind(X_50,$fot(rho1))]]) ).
cnf(refute_0_26,plain,
( definitionFOFtoCNF_0(some_action,l,rho1,some_target)
| part_of(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),rho1) ),
inference(resolve,[$cnf( part_of(l,rho1) )],[refute_0_3,refute_0_25]) ).
cnf(refute_0_27,plain,
( ~ permission(skolemFOFtoCNF_L2(some_action,l,rho1,some_target))
| skolemFOFtoCNF_L2(some_action,l,rho1,some_target) = l
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( part_of(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),rho1) )],[refute_0_26,refute_0_20]) ).
cnf(refute_0_28,plain,
( skolemFOFtoCNF_L2(some_action,l,rho1,some_target) = l
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( permission(skolemFOFtoCNF_L2(some_action,l,rho1,some_target)) )],[refute_0_11,refute_0_27]) ).
cnf(refute_0_29,plain,
( l != l
| skolemFOFtoCNF_L2(some_action,l,rho1,some_target) != l
| skolemFOFtoCNF_L2(some_action,l,rho1,some_target) = l ),
introduced(tautology,[equality,[$cnf( $equal(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),l) ),[0,1],$fot(l)]]) ).
cnf(refute_0_30,plain,
( l != l
| skolemFOFtoCNF_L2(some_action,l,rho1,some_target) = l
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),l) )],[refute_0_28,refute_0_29]) ).
cnf(refute_0_31,plain,
( l != l
| ~ cnt(l,some_action,some_target)
| ~ part_of(l,rho1)
| ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_L2(some_action,l,rho1,some_target),l) )],[refute_0_30,refute_0_2]) ).
cnf(refute_0_32,plain,
l = l,
introduced(tautology,[refl,[$fot(l)]]) ).
cnf(refute_0_33,plain,
( ~ cnt(l,some_action,some_target)
| ~ part_of(l,rho1)
| ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( $equal(l,l) )],[refute_0_32,refute_0_31]) ).
cnf(refute_0_34,plain,
( ~ part_of(l,rho1)
| ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( cnt(l,some_action,some_target) )],[refute_0_4,refute_0_33]) ).
cnf(refute_0_35,plain,
( ~ permission(l)
| definitionFOFtoCNF_0(some_action,l,rho1,some_target) ),
inference(resolve,[$cnf( part_of(l,rho1) )],[refute_0_3,refute_0_34]) ).
cnf(refute_0_36,plain,
definitionFOFtoCNF_0(some_action,l,rho1,some_target),
inference(resolve,[$cnf( permission(l) )],[refute_0_8,refute_0_35]) ).
cnf(refute_0_37,plain,
( ~ cnt(M,A,T)
| ~ definitionFOFtoCNF_0(A,L,Rho,T)
| ~ no_right(M)
| ~ odrl_rel(Rho)
| ~ part_of(M,Rho)
| M = skolemFOFtoCNF_N(A,Rho,T) ),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_38,plain,
( ~ cnt(X_89,some_action,some_target)
| ~ definitionFOFtoCNF_0(some_action,l,rho1,some_target)
| ~ no_right(X_89)
| ~ odrl_rel(rho1)
| ~ part_of(X_89,rho1)
| X_89 = skolemFOFtoCNF_N(some_action,rho1,some_target) ),
inference(subst,[],[refute_0_37:[bind(A,$fot(some_action)),bind(L,$fot(l)),bind(M,$fot(X_89)),bind(Rho,$fot(rho1)),bind(T,$fot(some_target))]]) ).
cnf(refute_0_39,plain,
( ~ cnt(X_89,some_action,some_target)
| ~ no_right(X_89)
| ~ odrl_rel(rho1)
| ~ part_of(X_89,rho1)
| X_89 = skolemFOFtoCNF_N(some_action,rho1,some_target) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(some_action,l,rho1,some_target) )],[refute_0_36,refute_0_38]) ).
cnf(refute_0_40,plain,
odrl_rel(rho1),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_41,plain,
( ~ cnt(X_89,some_action,some_target)
| ~ no_right(X_89)
| ~ part_of(X_89,rho1)
| X_89 = skolemFOFtoCNF_N(some_action,rho1,some_target) ),
inference(resolve,[$cnf( odrl_rel(rho1) )],[refute_0_40,refute_0_39]) ).
cnf(refute_0_42,plain,
( ~ cnt(n2,some_action,some_target)
| ~ no_right(n2)
| ~ part_of(n2,rho1)
| n2 = skolemFOFtoCNF_N(some_action,rho1,some_target) ),
inference(subst,[],[refute_0_41:[bind(X_89,$fot(n2))]]) ).
cnf(refute_0_43,plain,
( ~ no_right(n2)
| ~ part_of(n2,rho1)
| n2 = skolemFOFtoCNF_N(some_action,rho1,some_target) ),
inference(resolve,[$cnf( cnt(n2,some_action,some_target) )],[refute_0_0,refute_0_42]) ).
cnf(refute_0_44,plain,
cnt(n1,some_action,some_target),
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_45,plain,
( ~ cnt(n1,some_action,some_target)
| ~ no_right(n1)
| ~ part_of(n1,rho1)
| n1 = skolemFOFtoCNF_N(some_action,rho1,some_target) ),
inference(subst,[],[refute_0_41:[bind(X_89,$fot(n1))]]) ).
cnf(refute_0_46,plain,
( ~ no_right(n1)
| ~ part_of(n1,rho1)
| n1 = skolemFOFtoCNF_N(some_action,rho1,some_target) ),
inference(resolve,[$cnf( cnt(n1,some_action,some_target) )],[refute_0_44,refute_0_45]) ).
cnf(refute_0_47,plain,
no_right(n1),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_48,plain,
( ~ part_of(n1,rho1)
| n1 = skolemFOFtoCNF_N(some_action,rho1,some_target) ),
inference(resolve,[$cnf( no_right(n1) )],[refute_0_47,refute_0_46]) ).
cnf(refute_0_49,plain,
part_of(n1,rho1),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_50,plain,
n1 = skolemFOFtoCNF_N(some_action,rho1,some_target),
inference(resolve,[$cnf( part_of(n1,rho1) )],[refute_0_49,refute_0_48]) ).
cnf(refute_0_51,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_0_52,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_0_53,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_0_51,refute_0_52]) ).
cnf(refute_0_54,plain,
( n1 != skolemFOFtoCNF_N(some_action,rho1,some_target)
| skolemFOFtoCNF_N(some_action,rho1,some_target) = n1 ),
inference(subst,[],[refute_0_53:[bind(X,$fot(n1)),bind(Y,$fot(skolemFOFtoCNF_N(some_action,rho1,some_target)))]]) ).
cnf(refute_0_55,plain,
skolemFOFtoCNF_N(some_action,rho1,some_target) = n1,
inference(resolve,[$cnf( $equal(n1,skolemFOFtoCNF_N(some_action,rho1,some_target)) )],[refute_0_50,refute_0_54]) ).
cnf(refute_0_56,plain,
( n2 != skolemFOFtoCNF_N(some_action,rho1,some_target)
| skolemFOFtoCNF_N(some_action,rho1,some_target) != n1
| n2 = n1 ),
introduced(tautology,[equality,[$cnf( ~ $equal(n2,n1) ),[0],$fot(skolemFOFtoCNF_N(some_action,rho1,some_target))]]) ).
cnf(refute_0_57,plain,
( n2 != skolemFOFtoCNF_N(some_action,rho1,some_target)
| n2 = n1 ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_N(some_action,rho1,some_target),n1) )],[refute_0_55,refute_0_56]) ).
cnf(refute_0_58,plain,
( ~ no_right(n2)
| ~ part_of(n2,rho1)
| n2 = n1 ),
inference(resolve,[$cnf( $equal(n2,skolemFOFtoCNF_N(some_action,rho1,some_target)) )],[refute_0_43,refute_0_57]) ).
cnf(refute_0_59,plain,
no_right(n2),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_60,plain,
( ~ part_of(n2,rho1)
| n2 = n1 ),
inference(resolve,[$cnf( no_right(n2) )],[refute_0_59,refute_0_58]) ).
cnf(refute_0_61,plain,
part_of(n2,rho1),
inference(canonicalize,[],[normalize_0_22]) ).
cnf(refute_0_62,plain,
n2 = n1,
inference(resolve,[$cnf( part_of(n2,rho1) )],[refute_0_61,refute_0_60]) ).
cnf(refute_0_63,plain,
n1 != n2,
inference(canonicalize,[],[normalize_0_23]) ).
cnf(refute_0_64,plain,
( n2 != n1
| n1 = n2 ),
inference(subst,[],[refute_0_53:[bind(X,$fot(n2)),bind(Y,$fot(n1))]]) ).
cnf(refute_0_65,plain,
n2 != n1,
inference(resolve,[$cnf( $equal(n1,n2) )],[refute_0_64,refute_0_63]) ).
cnf(refute_0_66,plain,
$false,
inference(resolve,[$cnf( $equal(n2,n1) )],[refute_0_62,refute_0_65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.02 % Command : metis --show proof --show saturation %s
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 7 14:07:41 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.09/0.33 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.33
% 0.09/0.33 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.09/0.34
%------------------------------------------------------------------------------