%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n001.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:18:53 AM UTC 2026
% Result : Unsatisfiable 4.36s 4.69s
% Output : CNFRefutation 4.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 14:13:07 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.42 (re.compile("\."), Token.FullStop),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.42 (re.compile("\("), Token.OpenPar),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.42 (re.compile("\)"), Token.ClosePar),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.42 (re.compile("\["), Token.OpenSquare),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("~\|"), Token.Nor),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("\|"), Token.Or),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.42 (re.compile("\?"), Token.Existential),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.23/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.33/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.58 """
% 4.36/4.69 % Version: 1.5
% 4.36/4.69 % SZS status Unsatisfiable
% 4.36/4.69 % SZS output start CNFRefutation
% 4.36/4.69 fof(n1_neq_n2,axiom,n1!=n2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', n1_neq_n2)).
% 4.36/4.69 cnf(c12,plain,n1!=n2,inference(split_conjunct,[status(thm)],[n1_neq_n2])).
% 4.36/4.69 cnf(transitivity,axiom,X21!=X19|X19!=X20|X21=X20,theory(equality)).
% 4.36/4.69 cnf(symmetry,axiom,X18!=X17|X17=X18,theory(equality)).
% 4.36/4.69 fof(odrl_rho1,axiom,odrl_rel(rho1),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', odrl_rho1)).
% 4.36/4.69 cnf(c24,plain,odrl_rel(rho1),inference(split_conjunct,[status(thm)],[odrl_rho1])).
% 4.36/4.69 fof(permission_l,axiom,permission(l),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', permission_l)).
% 4.36/4.69 cnf(c23,plain,permission(l),inference(split_conjunct,[status(thm)],[permission_l])).
% 4.36/4.69 fof(no_right_n2,axiom,no_right(n2),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', no_right_n2)).
% 4.36/4.69 cnf(c21,plain,no_right(n2),inference(split_conjunct,[status(thm)],[no_right_n2])).
% 4.36/4.69 fof(partof_l,axiom,part_of(l,rho1),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', partof_l)).
% 4.36/4.69 cnf(c20,plain,part_of(l,rho1),inference(split_conjunct,[status(thm)],[partof_l])).
% 4.36/4.69 fof(partof_n2,axiom,part_of(n2,rho1),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', partof_n2)).
% 4.36/4.69 cnf(c18,plain,part_of(n2,rho1),inference(split_conjunct,[status(thm)],[partof_n2])).
% 4.36/4.69 fof(cnt_l,axiom,cnt(l,some_action,some_target),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cnt_l)).
% 4.36/4.69 cnf(c17,plain,cnt(l,some_action,some_target),inference(split_conjunct,[status(thm)],[cnt_l])).
% 4.36/4.69 fof(cnt_n2,axiom,cnt(n2,some_action,some_target),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cnt_n2)).
% 4.36/4.69 cnf(c15,plain,cnt(n2,some_action,some_target),inference(split_conjunct,[status(thm)],[cnt_n2])).
% 4.36/4.69 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))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax_correlativity_permission)).
% 4.36/4.69 fof(c29,plain,(![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)))))&((![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))))|(?[L]:(((permission(L)&part_of(L,Rho))&cnt(L,A,T))&(![L2]:(((~permission(L2)|~part_of(L2,Rho))|~cnt(L2,A,T))|L2=L)))))))))),inference(fof_nnf,[status(thm)],[ax_correlativity_permission])).
% 4.36/4.69 fof(c30,plain,(![Rho]:(~odrl_rel(Rho)|((![A]:(![T]:((![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)))))))&(![A]:(![T]:((![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))))|(?[L]:(((permission(L)&part_of(L,Rho))&cnt(L,A,T))&(![L2]:(((~permission(L2)|~part_of(L2,Rho))|~cnt(L2,A,T))|L2=L)))))))))),inference(shift_quantors,[status(thm)],[c29])).
% 4.36/4.69 fof(c31,plain,(![X3]:(~odrl_rel(X3)|((![X4]:(![X5]:((![X6]:(((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|(?[X7]:(((permission(X7)&part_of(X7,X3))&cnt(X7,X4,X5))&X7!=X6))))|(?[X8]:(((no_right(X8)&part_of(X8,X3))&cnt(X8,X4,X5))&(![X9]:(((~no_right(X9)|~part_of(X9,X3))|~cnt(X9,X4,X5))|X9=X8)))))))&(![X10]:(![X11]:((![X12]:(((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|(?[X13]:(((no_right(X13)&part_of(X13,X3))&cnt(X13,X10,X11))&X13!=X12))))|(?[X14]:(((permission(X14)&part_of(X14,X3))&cnt(X14,X10,X11))&(![X15]:(((~permission(X15)|~part_of(X15,X3))|~cnt(X15,X10,X11))|X15=X14)))))))))),inference(variable_rename,[status(thm)],[c30])).
% 4.36/4.69 fof(c33,plain,(![X3]:(![X4]:(![X5]:(![X6]:(![X9]:(![X10]:(![X11]:(![X12]:(![X15]:(~odrl_rel(X3)|(((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|(((permission(skolem0001(X3,X4,X5,X6))&part_of(skolem0001(X3,X4,X5,X6),X3))&cnt(skolem0001(X3,X4,X5,X6),X4,X5))&skolem0001(X3,X4,X5,X6)!=X6))|(((no_right(skolem0002(X3,X4,X5))&part_of(skolem0002(X3,X4,X5),X3))&cnt(skolem0002(X3,X4,X5),X4,X5))&(((~no_right(X9)|~part_of(X9,X3))|~cnt(X9,X4,X5))|X9=skolem0002(X3,X4,X5))))&((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|(((no_right(skolem0003(X3,X10,X11,X12))&part_of(skolem0003(X3,X10,X11,X12),X3))&cnt(skolem0003(X3,X10,X11,X12),X10,X11))&skolem0003(X3,X10,X11,X12)!=X12))|(((permission(skolem0004(X3,X10,X11))&part_of(skolem0004(X3,X10,X11),X3))&cnt(skolem0004(X3,X10,X11),X10,X11))&(((~permission(X15)|~part_of(X15,X3))|~cnt(X15,X10,X11))|X15=skolem0004(X3,X10,X11))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,(![X3]:(~odrl_rel(X3)|((![X4]:(![X5]:((![X6]:(((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|(((permission(skolem0001(X3,X4,X5,X6))&part_of(skolem0001(X3,X4,X5,X6),X3))&cnt(skolem0001(X3,X4,X5,X6),X4,X5))&skolem0001(X3,X4,X5,X6)!=X6)))|(((no_right(skolem0002(X3,X4,X5))&part_of(skolem0002(X3,X4,X5),X3))&cnt(skolem0002(X3,X4,X5),X4,X5))&(![X9]:(((~no_right(X9)|~part_of(X9,X3))|~cnt(X9,X4,X5))|X9=skolem0002(X3,X4,X5)))))))&(![X10]:(![X11]:((![X12]:(((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|(((no_right(skolem0003(X3,X10,X11,X12))&part_of(skolem0003(X3,X10,X11,X12),X3))&cnt(skolem0003(X3,X10,X11,X12),X10,X11))&skolem0003(X3,X10,X11,X12)!=X12)))|(((permission(skolem0004(X3,X10,X11))&part_of(skolem0004(X3,X10,X11),X3))&cnt(skolem0004(X3,X10,X11),X10,X11))&(![X15]:(((~permission(X15)|~part_of(X15,X3))|~cnt(X15,X10,X11))|X15=skolem0004(X3,X10,X11)))))))))),inference(skolemize,[status(esa)],[c31])).])).
% 4.36/4.69 fof(c34,plain,(![X3]:(![X4]:(![X5]:(![X6]:(![X9]:(![X10]:(![X11]:(![X12]:(![X15]:((((((((~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|permission(skolem0001(X3,X4,X5,X6)))|no_right(skolem0002(X3,X4,X5))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|permission(skolem0001(X3,X4,X5,X6)))|part_of(skolem0002(X3,X4,X5),X3))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|permission(skolem0001(X3,X4,X5,X6)))|cnt(skolem0002(X3,X4,X5),X4,X5))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|permission(skolem0001(X3,X4,X5,X6)))|(((~no_right(X9)|~part_of(X9,X3))|~cnt(X9,X4,X5))|X9=skolem0002(X3,X4,X5)))))&((((~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|part_of(skolem0001(X3,X4,X5,X6),X3))|no_right(skolem0002(X3,X4,X5))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|part_of(skolem0001(X3,X4,X5,X6),X3))|part_of(skolem0002(X3,X4,X5),X3))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|part_of(skolem0001(X3,X4,X5,X6),X3))|cnt(skolem0002(X3,X4,X5),X4,X5))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|part_of(skolem0001(X3,X4,X5,X6),X3))|(((~no_right(X9)|~part_of(X9,X3))|~cnt(X9,X4,X5))|X9=skolem0002(X3,X4,X5))))))&((((~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|cnt(skolem0001(X3,X4,X5,X6),X4,X5))|no_right(skolem0002(X3,X4,X5))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|cnt(skolem0001(X3,X4,X5,X6),X4,X5))|part_of(skolem0002(X3,X4,X5),X3))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|cnt(skolem0001(X3,X4,X5,X6),X4,X5))|cnt(skolem0002(X3,X4,X5),X4,X5))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|cnt(skolem0001(X3,X4,X5,X6),X4,X5))|(((~no_right(X9)|~part_of(X9,X3))|~cnt(X9,X4,X5))|X9=skolem0002(X3,X4,X5))))))&((((~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|skolem0001(X3,X4,X5,X6)!=X6)|no_right(skolem0002(X3,X4,X5))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|skolem0001(X3,X4,X5,X6)!=X6)|part_of(skolem0002(X3,X4,X5),X3))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|skolem0001(X3,X4,X5,X6)!=X6)|cnt(skolem0002(X3,X4,X5),X4,X5))))&(~odrl_rel(X3)|((((~permission(X6)|~part_of(X6,X3))|~cnt(X6,X4,X5))|skolem0001(X3,X4,X5,X6)!=X6)|(((~no_right(X9)|~part_of(X9,X3))|~cnt(X9,X4,X5))|X9=skolem0002(X3,X4,X5))))))&(((((((~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|no_right(skolem0003(X3,X10,X11,X12)))|permission(skolem0004(X3,X10,X11))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|no_right(skolem0003(X3,X10,X11,X12)))|part_of(skolem0004(X3,X10,X11),X3))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|no_right(skolem0003(X3,X10,X11,X12)))|cnt(skolem0004(X3,X10,X11),X10,X11))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|no_right(skolem0003(X3,X10,X11,X12)))|(((~permission(X15)|~part_of(X15,X3))|~cnt(X15,X10,X11))|X15=skolem0004(X3,X10,X11)))))&((((~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|part_of(skolem0003(X3,X10,X11,X12),X3))|permission(skolem0004(X3,X10,X11))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|part_of(skolem0003(X3,X10,X11,X12),X3))|part_of(skolem0004(X3,X10,X11),X3))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|part_of(skolem0003(X3,X10,X11,X12),X3))|cnt(skolem0004(X3,X10,X11),X10,X11))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|part_of(skolem0003(X3,X10,X11,X12),X3))|(((~permission(X15)|~part_of(X15,X3))|~cnt(X15,X10,X11))|X15=skolem0004(X3,X10,X11))))))&((((~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|cnt(skolem0003(X3,X10,X11,X12),X10,X11))|permission(skolem0004(X3,X10,X11))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|cnt(skolem0003(X3,X10,X11,X12),X10,X11))|part_of(skolem0004(X3,X10,X11),X3))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|cnt(skolem0003(X3,X10,X11,X12),X10,X11))|cnt(skolem0004(X3,X10,X11),X10,X11))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|cnt(skolem0003(X3,X10,X11,X12),X10,X11))|(((~permission(X15)|~part_of(X15,X3))|~cnt(X15,X10,X11))|X15=skolem0004(X3,X10,X11))))))&((((~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|skolem0003(X3,X10,X11,X12)!=X12)|permission(skolem0004(X3,X10,X11))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|skolem0003(X3,X10,X11,X12)!=X12)|part_of(skolem0004(X3,X10,X11),X3))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|skolem0003(X3,X10,X11,X12)!=X12)|cnt(skolem0004(X3,X10,X11),X10,X11))))&(~odrl_rel(X3)|((((~no_right(X12)|~part_of(X12,X3))|~cnt(X12,X10,X11))|skolem0003(X3,X10,X11,X12)!=X12)|(((~permission(X15)|~part_of(X15,X3))|~cnt(X15,X10,X11))|X15=skolem0004(X3,X10,X11)))))))))))))))),inference(distribute,[status(thm)],[c33])).
% 4.36/4.69 cnf(c50,plain,~odrl_rel(X188)|~permission(X190)|~part_of(X190,X188)|~cnt(X190,X186,X187)|skolem0001(X188,X186,X187,X190)!=X190|~no_right(X189)|~part_of(X189,X188)|~cnt(X189,X186,X187)|X189=skolem0002(X188,X186,X187),inference(split_conjunct,[status(thm)],[c34])).
% 4.36/4.69 cnf(c38,plain,~odrl_rel(X93)|~permission(X95)|~part_of(X95,X93)|~cnt(X95,X91,X92)|permission(skolem0001(X93,X91,X92,X95))|~no_right(X94)|~part_of(X94,X93)|~cnt(X94,X91,X92)|X94=skolem0002(X93,X91,X92),inference(split_conjunct,[status(thm)],[c34])).
% 4.36/4.69 cnf(c110,plain,~odrl_rel(X260)|~permission(X261)|~part_of(X261,X260)|~cnt(X261,some_action,some_target)|permission(skolem0001(X260,some_action,some_target,X261))|~no_right(n2)|~part_of(n2,X260)|n2=skolem0002(X260,some_action,some_target),inference(resolution,[status(thm)],[c38, c15])).
% 4.36/4.69 cnf(c236,plain,~odrl_rel(X437)|~permission(l)|~part_of(l,X437)|permission(skolem0001(X437,some_action,some_target,l))|~no_right(n2)|~part_of(n2,X437)|n2=skolem0002(X437,some_action,some_target),inference(resolution,[status(thm)],[c110, c17])).
% 4.36/4.69 cnf(c1342,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|permission(skolem0001(rho1,some_action,some_target,l))|~no_right(n2)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c236, c18])).
% 4.36/4.69 cnf(c1443,plain,~odrl_rel(rho1)|~permission(l)|permission(skolem0001(rho1,some_action,some_target,l))|~no_right(n2)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1342, c20])).
% 4.36/4.69 cnf(c1444,plain,~odrl_rel(rho1)|~permission(l)|permission(skolem0001(rho1,some_action,some_target,l))|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1443, c21])).
% 4.36/4.69 cnf(c1445,plain,~odrl_rel(rho1)|permission(skolem0001(rho1,some_action,some_target,l))|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1444, c23])).
% 4.36/4.69 cnf(c1446,plain,permission(skolem0001(rho1,some_action,some_target,l))|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1445, c24])).
% 4.36/4.69 cnf(c1455,plain,permission(skolem0001(rho1,some_action,some_target,l))|skolem0002(rho1,some_action,some_target)=n2,inference(resolution,[status(thm)],[c1446, symmetry])).
% 4.36/4.69 cnf(c1470,plain,permission(skolem0001(rho1,some_action,some_target,l))|X565!=skolem0002(rho1,some_action,some_target)|X565=n2,inference(resolution,[status(thm)],[c1455, transitivity])).
% 4.36/4.69 fof(no_right_n1,axiom,no_right(n1),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', no_right_n1)).
% 4.36/4.69 cnf(c22,plain,no_right(n1),inference(split_conjunct,[status(thm)],[no_right_n1])).
% 4.36/4.69 fof(partof_n1,axiom,part_of(n1,rho1),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', partof_n1)).
% 4.36/4.69 cnf(c19,plain,part_of(n1,rho1),inference(split_conjunct,[status(thm)],[partof_n1])).
% 4.36/4.69 fof(cnt_n1,axiom,cnt(n1,some_action,some_target),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cnt_n1)).
% 4.36/4.69 cnf(c16,plain,cnt(n1,some_action,some_target),inference(split_conjunct,[status(thm)],[cnt_n1])).
% 4.36/4.69 cnf(c112,plain,~odrl_rel(X271)|~permission(X272)|~part_of(X272,X271)|~cnt(X272,some_action,some_target)|permission(skolem0001(X271,some_action,some_target,X272))|~no_right(n1)|~part_of(n1,X271)|n1=skolem0002(X271,some_action,some_target),inference(resolution,[status(thm)],[c38, c16])).
% 4.36/4.69 cnf(c251,plain,~odrl_rel(X460)|~permission(l)|~part_of(l,X460)|permission(skolem0001(X460,some_action,some_target,l))|~no_right(n1)|~part_of(n1,X460)|n1=skolem0002(X460,some_action,some_target),inference(resolution,[status(thm)],[c112, c17])).
% 4.36/4.69 cnf(c1359,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|permission(skolem0001(rho1,some_action,some_target,l))|~no_right(n1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c251, c19])).
% 4.36/4.69 cnf(c1516,plain,~odrl_rel(rho1)|~permission(l)|permission(skolem0001(rho1,some_action,some_target,l))|~no_right(n1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1359, c20])).
% 4.36/4.69 cnf(c1517,plain,~odrl_rel(rho1)|~permission(l)|permission(skolem0001(rho1,some_action,some_target,l))|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1516, c22])).
% 4.36/4.69 cnf(c1521,plain,~odrl_rel(rho1)|permission(skolem0001(rho1,some_action,some_target,l))|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1517, c23])).
% 4.36/4.69 cnf(c1522,plain,permission(skolem0001(rho1,some_action,some_target,l))|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1521, c24])).
% 4.36/4.69 cnf(c1529,plain,permission(skolem0001(rho1,some_action,some_target,l))|n1=n2,inference(resolution,[status(thm)],[c1522, c1470])).
% 4.36/4.69 cnf(c1547,plain,permission(skolem0001(rho1,some_action,some_target,l)),inference(resolution,[status(thm)],[c1529, c12])).
% 4.36/4.69 cnf(c42,plain,~odrl_rel(X156)|~permission(X158)|~part_of(X158,X156)|~cnt(X158,X154,X155)|part_of(skolem0001(X156,X154,X155,X158),X156)|~no_right(X157)|~part_of(X157,X156)|~cnt(X157,X154,X155)|X157=skolem0002(X156,X154,X155),inference(split_conjunct,[status(thm)],[c34])).
% 4.36/4.69 cnf(c147,plain,~odrl_rel(X318)|~permission(X319)|~part_of(X319,X318)|~cnt(X319,some_action,some_target)|part_of(skolem0001(X318,some_action,some_target,X319),X318)|~no_right(n2)|~part_of(n2,X318)|n2=skolem0002(X318,some_action,some_target),inference(resolution,[status(thm)],[c42, c15])).
% 4.36/4.69 cnf(c480,plain,~odrl_rel(X670)|~permission(l)|~part_of(l,X670)|part_of(skolem0001(X670,some_action,some_target,l),X670)|~no_right(n2)|~part_of(n2,X670)|n2=skolem0002(X670,some_action,some_target),inference(resolution,[status(thm)],[c147, c17])).
% 4.36/4.69 cnf(c1773,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|part_of(skolem0001(rho1,some_action,some_target,l),rho1)|~no_right(n2)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c480, c18])).
% 4.36/4.69 cnf(c1797,plain,~odrl_rel(rho1)|~permission(l)|part_of(skolem0001(rho1,some_action,some_target,l),rho1)|~no_right(n2)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1773, c20])).
% 4.36/4.69 cnf(c1798,plain,~odrl_rel(rho1)|~permission(l)|part_of(skolem0001(rho1,some_action,some_target,l),rho1)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1797, c21])).
% 4.36/4.69 cnf(c1799,plain,~odrl_rel(rho1)|part_of(skolem0001(rho1,some_action,some_target,l),rho1)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1798, c23])).
% 4.36/4.69 cnf(c1800,plain,part_of(skolem0001(rho1,some_action,some_target,l),rho1)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1799, c24])).
% 4.36/4.69 cnf(c1816,plain,part_of(skolem0001(rho1,some_action,some_target,l),rho1)|skolem0002(rho1,some_action,some_target)=n2,inference(resolution,[status(thm)],[c1800, symmetry])).
% 4.36/4.69 cnf(c1827,plain,part_of(skolem0001(rho1,some_action,some_target,l),rho1)|X705!=skolem0002(rho1,some_action,some_target)|X705=n2,inference(resolution,[status(thm)],[c1816, transitivity])).
% 4.36/4.69 cnf(c149,plain,~odrl_rel(X333)|~permission(X334)|~part_of(X334,X333)|~cnt(X334,some_action,some_target)|part_of(skolem0001(X333,some_action,some_target,X334),X333)|~no_right(n1)|~part_of(n1,X333)|n1=skolem0002(X333,some_action,some_target),inference(resolution,[status(thm)],[c42, c16])).
% 4.36/4.69 cnf(c591,plain,~odrl_rel(X677)|~permission(l)|~part_of(l,X677)|part_of(skolem0001(X677,some_action,some_target,l),X677)|~no_right(n1)|~part_of(n1,X677)|n1=skolem0002(X677,some_action,some_target),inference(resolution,[status(thm)],[c149, c17])).
% 4.36/4.69 cnf(c1778,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|part_of(skolem0001(rho1,some_action,some_target,l),rho1)|~no_right(n1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c591, c19])).
% 4.36/4.69 cnf(c1916,plain,~odrl_rel(rho1)|~permission(l)|part_of(skolem0001(rho1,some_action,some_target,l),rho1)|~no_right(n1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1778, c20])).
% 4.36/4.69 cnf(c1917,plain,~odrl_rel(rho1)|~permission(l)|part_of(skolem0001(rho1,some_action,some_target,l),rho1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1916, c22])).
% 4.36/4.69 cnf(c1918,plain,~odrl_rel(rho1)|part_of(skolem0001(rho1,some_action,some_target,l),rho1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1917, c23])).
% 4.36/4.69 cnf(c1919,plain,part_of(skolem0001(rho1,some_action,some_target,l),rho1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c1918, c24])).
% 4.36/4.69 cnf(c1925,plain,part_of(skolem0001(rho1,some_action,some_target,l),rho1)|n1=n2,inference(resolution,[status(thm)],[c1919, c1827])).
% 4.36/4.69 cnf(c1946,plain,part_of(skolem0001(rho1,some_action,some_target,l),rho1),inference(resolution,[status(thm)],[c1925, c12])).
% 4.36/4.69 fof(perm_l_unique,axiom,(![L2]:(((permission(L2)&part_of(L2,rho1))&cnt(L2,some_action,some_target))=>L2=l)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', perm_l_unique)).
% 4.36/4.69 fof(c9,plain,(![L2]:(((~permission(L2)|~part_of(L2,rho1))|~cnt(L2,some_action,some_target))|L2=l)),inference(fof_nnf,[status(thm)],[perm_l_unique])).
% 4.36/4.69 fof(c10,plain,(![X2]:(((~permission(X2)|~part_of(X2,rho1))|~cnt(X2,some_action,some_target))|X2=l)),inference(variable_rename,[status(thm)],[c9])).
% 4.36/4.69 cnf(c11,plain,~permission(X60)|~part_of(X60,rho1)|~cnt(X60,some_action,some_target)|X60=l,inference(split_conjunct,[status(thm)],[c10])).
% 4.36/4.69 cnf(c46,plain,~odrl_rel(X178)|~permission(X180)|~part_of(X180,X178)|~cnt(X180,X176,X177)|cnt(skolem0001(X178,X176,X177,X180),X176,X177)|~no_right(X179)|~part_of(X179,X178)|~cnt(X179,X176,X177)|X179=skolem0002(X178,X176,X177),inference(split_conjunct,[status(thm)],[c34])).
% 4.36/4.69 cnf(c166,plain,~odrl_rel(X353)|~permission(X352)|~part_of(X352,X353)|~cnt(X352,some_action,some_target)|cnt(skolem0001(X353,some_action,some_target,X352),some_action,some_target)|~no_right(n2)|~part_of(n2,X353)|n2=skolem0002(X353,some_action,some_target),inference(resolution,[status(thm)],[c46, c15])).
% 4.36/4.69 cnf(c738,plain,~odrl_rel(X837)|~permission(l)|~part_of(l,X837)|cnt(skolem0001(X837,some_action,some_target,l),some_action,some_target)|~no_right(n2)|~part_of(n2,X837)|n2=skolem0002(X837,some_action,some_target),inference(resolution,[status(thm)],[c166, c17])).
% 4.36/4.69 cnf(c2285,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|~no_right(n2)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c738, c18])).
% 4.36/4.69 cnf(c2286,plain,~odrl_rel(rho1)|~permission(l)|cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|~no_right(n2)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2285, c20])).
% 4.36/4.69 cnf(c2287,plain,~odrl_rel(rho1)|~permission(l)|cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2286, c21])).
% 4.36/4.69 cnf(c2288,plain,~odrl_rel(rho1)|cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2287, c23])).
% 4.36/4.70 cnf(c2289,plain,cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2288, c24])).
% 4.36/4.70 cnf(c2354,plain,cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|skolem0002(rho1,some_action,some_target)=n2,inference(resolution,[status(thm)],[c2289, symmetry])).
% 4.36/4.70 cnf(c2413,plain,cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|X850!=skolem0002(rho1,some_action,some_target)|X850=n2,inference(resolution,[status(thm)],[c2354, transitivity])).
% 4.36/4.70 cnf(c168,plain,~odrl_rel(X363)|~permission(X362)|~part_of(X362,X363)|~cnt(X362,some_action,some_target)|cnt(skolem0001(X363,some_action,some_target,X362),some_action,some_target)|~no_right(n1)|~part_of(n1,X363)|n1=skolem0002(X363,some_action,some_target),inference(resolution,[status(thm)],[c46, c16])).
% 4.36/4.70 cnf(c812,plain,~odrl_rel(X881)|~permission(l)|~part_of(l,X881)|cnt(skolem0001(X881,some_action,some_target,l),some_action,some_target)|~no_right(n1)|~part_of(n1,X881)|n1=skolem0002(X881,some_action,some_target),inference(resolution,[status(thm)],[c168, c17])).
% 4.36/4.70 cnf(c2564,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|~no_right(n1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c812, c19])).
% 4.36/4.70 cnf(c2565,plain,~odrl_rel(rho1)|~permission(l)|cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|~no_right(n1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2564, c20])).
% 4.36/4.70 cnf(c2566,plain,~odrl_rel(rho1)|~permission(l)|cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2565, c22])).
% 4.36/4.70 cnf(c2573,plain,~odrl_rel(rho1)|cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2566, c23])).
% 4.36/4.70 cnf(c2574,plain,cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2573, c24])).
% 4.36/4.70 cnf(c2633,plain,cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target)|n1=n2,inference(resolution,[status(thm)],[c2574, c2413])).
% 4.36/4.70 cnf(c2699,plain,cnt(skolem0001(rho1,some_action,some_target,l),some_action,some_target),inference(resolution,[status(thm)],[c2633, c12])).
% 4.36/4.70 cnf(c2720,plain,~permission(skolem0001(rho1,some_action,some_target,l))|~part_of(skolem0001(rho1,some_action,some_target,l),rho1)|skolem0001(rho1,some_action,some_target,l)=l,inference(resolution,[status(thm)],[c2699, c11])).
% 4.36/4.70 cnf(c2790,plain,~permission(skolem0001(rho1,some_action,some_target,l))|skolem0001(rho1,some_action,some_target,l)=l,inference(resolution,[status(thm)],[c2720, c1946])).
% 4.36/4.70 cnf(c2798,plain,skolem0001(rho1,some_action,some_target,l)=l,inference(resolution,[status(thm)],[c2790, c1547])).
% 4.36/4.70 cnf(c2814,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|~cnt(l,some_action,some_target)|~no_right(X1193)|~part_of(X1193,rho1)|~cnt(X1193,some_action,some_target)|X1193=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2798, c50])).
% 4.36/4.70 cnf(c4558,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|~cnt(l,some_action,some_target)|~no_right(n2)|~part_of(n2,rho1)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2814, c15])).
% 4.36/4.70 cnf(c4586,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|~no_right(n2)|~part_of(n2,rho1)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4558, c17])).
% 4.36/4.70 cnf(c4587,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|~no_right(n2)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4586, c18])).
% 4.36/4.70 cnf(c4588,plain,~odrl_rel(rho1)|~permission(l)|~no_right(n2)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4587, c20])).
% 4.36/4.70 cnf(c4589,plain,~odrl_rel(rho1)|~permission(l)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4588, c21])).
% 4.36/4.70 cnf(c4590,plain,~odrl_rel(rho1)|n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4589, c23])).
% 4.36/4.70 cnf(c4591,plain,n2=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4590, c24])).
% 4.36/4.70 cnf(c4600,plain,skolem0002(rho1,some_action,some_target)=n2,inference(resolution,[status(thm)],[c4591, symmetry])).
% 4.36/4.70 cnf(c4608,plain,X1209!=skolem0002(rho1,some_action,some_target)|X1209=n2,inference(resolution,[status(thm)],[c4600, transitivity])).
% 4.36/4.70 cnf(c4563,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|~cnt(l,some_action,some_target)|~no_right(n1)|~part_of(n1,rho1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c2814, c16])).
% 4.36/4.70 cnf(c4622,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|~no_right(n1)|~part_of(n1,rho1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4563, c17])).
% 4.36/4.70 cnf(c4623,plain,~odrl_rel(rho1)|~permission(l)|~part_of(l,rho1)|~no_right(n1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4622, c19])).
% 4.36/4.70 cnf(c4624,plain,~odrl_rel(rho1)|~permission(l)|~no_right(n1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4623, c20])).
% 4.36/4.70 cnf(c4625,plain,~odrl_rel(rho1)|~permission(l)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4624, c22])).
% 4.36/4.70 cnf(c4626,plain,~odrl_rel(rho1)|n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4625, c23])).
% 4.36/4.70 cnf(c4627,plain,n1=skolem0002(rho1,some_action,some_target),inference(resolution,[status(thm)],[c4626, c24])).
% 4.36/4.70 cnf(c4628,plain,n1=n2,inference(resolution,[status(thm)],[c4627, c4608])).
% 4.36/4.70 cnf(c4652,plain,$false,inference(resolution,[status(thm)],[c4628, c12])).
% 4.36/4.70 % SZS output end CNFRefutation
% 4.36/4.70
% 4.36/4.70 % Initial clauses : 62
% 4.36/4.70 % Processed clauses : 1154
% 4.36/4.70 % Factors computed : 40
% 4.36/4.70 % Resolvents computed: 4546
% 4.36/4.70 % Tautologies deleted: 9
% 4.36/4.70 % Forward subsumed : 712
% 4.36/4.70 % Backward subsumed : 416
% 4.36/4.70 % -------- CPU Time ---------
% 4.36/4.70 % User time : 4.288 s
% 4.36/4.70 % System time : 0.048 s
% 4.36/4.70 % Total time : 4.336 s
%------------------------------------------------------------------------------