%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:25:57 PM UTC 2026
% Result : Unsatisfiable 0.11s 5.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.58 % Computer : n009.cluster.edu
% 0.11/5.58 % Model : x86_64 x86_64
% 0.11/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.58 % Memory : 8046.5625MB
% 0.11/5.58 % OS : Linux 6.8.0-71-generic
% 0.11/5.58 % CPULimit : 300
% 0.11/5.58 % WCLimit : 300
% 0.11/5.58 % DateTime : Mon Sep 21 01:26:47 UTC 2026
% 0.11/5.58 % CPUTime :
% 0.11/5.59 % Drodi V4.1.1
% 0.11/5.60 % Refutation found
% 0.11/5.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.11/5.60 % SZS output start CNFRefutation for theBenchmark
% 0.11/5.60 fof(f1,axiom,(
% 0.11/5.60 (! [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 ) )) )) ) )),
% 0.11/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.60 fof(f6,axiom,(
% 0.11/5.60 odrl_rel(rho1) ),
% 0.11/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.60 fof(f7,axiom,(
% 0.11/5.60 permission(l) ),
% 0.11/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.60 fof(f8,axiom,(
% 0.11/5.60 no_right(n1) ),
% 0.11/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.60 fof(f9,axiom,(
% 0.11/5.60 no_right(n2) ),
% 0.11/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.60 fof(f10,axiom,(
% 0.11/5.60 part_of(l,rho1) ),
% 0.11/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.60 fof(f11,axiom,(
% 0.11/5.60 part_of(n1,rho1) ),
% 0.14/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f12,axiom,(
% 0.14/5.60 part_of(n2,rho1) ),
% 0.14/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f13,axiom,(
% 0.14/5.60 cnt(l,some_action,some_target) ),
% 0.14/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f14,axiom,(
% 0.14/5.60 cnt(n1,some_action,some_target) ),
% 0.14/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f15,axiom,(
% 0.14/5.60 cnt(n2,some_action,some_target) ),
% 0.14/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f18,axiom,(
% 0.14/5.60 n1 != n2 ),
% 0.14/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f19,axiom,(
% 0.14/5.60 (! [L2] :( ( permission(L2)& part_of(L2,rho1)& cnt(L2,some_action,some_target) )=> L2 = l ) )),
% 0.14/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f20,plain,(
% 0.14/5.60 ![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))))))),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.14/5.60 fof(f21,definition,(
% 0.14/5.60 ![Rho,A,T,L,L2]: (sP0_prd(L2,L,T,A,Rho)<=>(((~permission(L2)|~part_of(L2,Rho))|~cnt(L2,A,T))|L2=L))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.14/5.60 fof(f22,definition,(
% 0.14/5.60 ![Rho,A,T,N,M]: (sP1_prd(M,N,T,A,Rho)<=>(((~no_right(M)|~part_of(M,Rho))|~cnt(M,A,T))|M=N))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.14/5.60 fof(f23,plain,(
% 0.14/5.60 ![Rho,A,T]: (~odrl_rel(Rho)|((?[L]: (((permission(L)&part_of(L,Rho))&cnt(L,A,T))&(![L2]: sP0_prd(L2,L,T,A,Rho))))<=>(?[N]: (((no_right(N)&part_of(N,Rho))&cnt(N,A,T))&(![M]: sP1_prd(M,N,T,A,Rho))))))),
% 0.14/5.60 inference(formula_renaming,[status(thm)],[f20,f22,f21])).
% 0.14/5.60 fof(f24,plain,(
% 0.14/5.60 ![Rho,A,T]: (~odrl_rel(Rho)|(((![L]: (((~permission(L)|~part_of(L,Rho))|~cnt(L,A,T))|(?[L2]: ~sP0_prd(L2,L,T,A,Rho))))|(?[N]: (((no_right(N)&part_of(N,Rho))&cnt(N,A,T))&(![M]: sP1_prd(M,N,T,A,Rho)))))&((?[L]: (((permission(L)&part_of(L,Rho))&cnt(L,A,T))&(![L2]: sP0_prd(L2,L,T,A,Rho))))|(![N]: (((~no_right(N)|~part_of(N,Rho))|~cnt(N,A,T))|(?[M]: ~sP1_prd(M,N,T,A,Rho)))))))),
% 0.14/5.60 inference(NNF_transformation,[status(thm)],[f23])).
% 0.14/5.60 fof(f25,plain,(
% 0.14/5.60 ![Rho]: (~odrl_rel(Rho)|((![A,T]: ((![L]: (((~permission(L)|~part_of(L,Rho))|~cnt(L,A,T))|(?[L2]: ~sP0_prd(L2,L,T,A,Rho))))|(?[N]: (((no_right(N)&part_of(N,Rho))&cnt(N,A,T))&(![M]: sP1_prd(M,N,T,A,Rho))))))&(![A,T]: ((?[L]: (((permission(L)&part_of(L,Rho))&cnt(L,A,T))&(![L2]: sP0_prd(L2,L,T,A,Rho))))|(![N]: (((~no_right(N)|~part_of(N,Rho))|~cnt(N,A,T))|(?[M]: ~sP1_prd(M,N,T,A,Rho))))))))),
% 0.14/5.60 inference(miniscoping,[status(thm)],[f24])).
% 0.14/5.60 fof(f26,plain,(
% 0.14/5.60 ![Rho]: (~odrl_rel(Rho)|((![A,T]: ((![L]: (((~permission(L)|~part_of(L,Rho))|~cnt(L,A,T))|~sP0_prd(sK0_skl(L,T,A,Rho),L,T,A,Rho)))|(((no_right(sK1_skl(T,A,Rho))&part_of(sK1_skl(T,A,Rho),Rho))&cnt(sK1_skl(T,A,Rho),A,T))&(![M]: sP1_prd(M,sK1_skl(T,A,Rho),T,A,Rho)))))&(![A,T]: ((((permission(sK2_skl(T,A,Rho))&part_of(sK2_skl(T,A,Rho),Rho))&cnt(sK2_skl(T,A,Rho),A,T))&(![L2]: sP0_prd(L2,sK2_skl(T,A,Rho),T,A,Rho)))|(![N]: (((~no_right(N)|~part_of(N,Rho))|~cnt(N,A,T))|~sP1_prd(sK3_skl(N,T,A,Rho),N,T,A,Rho)))))))),
% 0.14/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(L2,sK0_skl(L,T,A,Rho)),skolemize(N,sK1_skl(T,A,Rho)),skolemize(L,sK2_skl(T,A,Rho)),skolemize(M,sK3_skl(N,T,A,Rho))],[f25])).
% 0.14/5.60 fof(f30,plain,(
% 0.14/5.60 ![X0,X1,X2,X3,X4]: (~odrl_rel(X0)|~permission(X1)|~part_of(X1,X0)|~cnt(X1,X2,X3)|~sP0_prd(sK0_skl(X1,X3,X2,X0),X1,X3,X2,X0)|sP1_prd(X4,sK1_skl(X3,X2,X0),X3,X2,X0))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f26])).
% 0.14/5.60 fof(f39,plain,(
% 0.14/5.60 odrl_rel(rho1)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/5.60 fof(f40,plain,(
% 0.14/5.60 permission(l)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/5.60 fof(f41,plain,(
% 0.14/5.60 no_right(n1)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/5.60 fof(f42,plain,(
% 0.14/5.60 no_right(n2)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f9])).
% 0.14/5.60 fof(f43,plain,(
% 0.14/5.60 part_of(l,rho1)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f10])).
% 0.14/5.60 fof(f44,plain,(
% 0.14/5.60 part_of(n1,rho1)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f11])).
% 0.14/5.60 fof(f45,plain,(
% 0.14/5.60 part_of(n2,rho1)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.60 fof(f46,plain,(
% 0.14/5.60 cnt(l,some_action,some_target)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/5.60 fof(f47,plain,(
% 0.14/5.60 cnt(n1,some_action,some_target)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f14])).
% 0.14/5.60 fof(f48,plain,(
% 0.14/5.60 cnt(n2,some_action,some_target)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f15])).
% 0.14/5.60 fof(f51,plain,(
% 0.14/5.60 ~n1=n2),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f18])).
% 0.14/5.60 fof(f52,plain,(
% 0.14/5.60 ![L2]: (((~permission(L2)|~part_of(L2,rho1))|~cnt(L2,some_action,some_target))|L2=l)),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.14/5.60 fof(f53,plain,(
% 0.14/5.60 ![X0]: (~permission(X0)|~part_of(X0,rho1)|~cnt(X0,some_action,some_target)|X0=l)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f52])).
% 0.14/5.60 fof(f54,plain,(
% 0.14/5.60 ![Rho,A,T,L,L2]: ((~sP0_prd(L2,L,T,A,Rho)|(((~permission(L2)|~part_of(L2,Rho))|~cnt(L2,A,T))|L2=L))&(sP0_prd(L2,L,T,A,Rho)|(((permission(L2)&part_of(L2,Rho))&cnt(L2,A,T))&~L2=L)))),
% 0.14/5.60 inference(NNF_transformation,[status(thm)],[f21])).
% 0.14/5.60 fof(f55,plain,(
% 0.14/5.60 (![Rho,A,T,L,L2]: (~sP0_prd(L2,L,T,A,Rho)|(((~permission(L2)|~part_of(L2,Rho))|~cnt(L2,A,T))|L2=L)))&(![Rho,A,T,L,L2]: (sP0_prd(L2,L,T,A,Rho)|(((permission(L2)&part_of(L2,Rho))&cnt(L2,A,T))&~L2=L)))),
% 0.14/5.60 inference(miniscoping,[status(thm)],[f54])).
% 0.14/5.60 fof(f57,plain,(
% 0.14/5.60 ![X0,X1,X2,X3,X4]: (sP0_prd(X0,X1,X2,X3,X4)|permission(X0))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/5.60 fof(f58,plain,(
% 0.14/5.60 ![X0,X1,X2,X3,X4]: (sP0_prd(X0,X1,X2,X3,X4)|part_of(X0,X4))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/5.60 fof(f59,plain,(
% 0.14/5.60 ![X0,X1,X2,X3,X4]: (sP0_prd(X0,X1,X2,X3,X4)|cnt(X0,X3,X2))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/5.60 fof(f60,plain,(
% 0.14/5.60 ![X0,X1,X2,X3,X4]: (sP0_prd(X0,X1,X2,X3,X4)|~X0=X1)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/5.60 fof(f61,plain,(
% 0.14/5.60 ![Rho,A,T,N,M]: ((~sP1_prd(M,N,T,A,Rho)|(((~no_right(M)|~part_of(M,Rho))|~cnt(M,A,T))|M=N))&(sP1_prd(M,N,T,A,Rho)|(((no_right(M)&part_of(M,Rho))&cnt(M,A,T))&~M=N)))),
% 0.14/5.60 inference(NNF_transformation,[status(thm)],[f22])).
% 0.14/5.60 fof(f62,plain,(
% 0.14/5.60 (![Rho,A,T,N,M]: (~sP1_prd(M,N,T,A,Rho)|(((~no_right(M)|~part_of(M,Rho))|~cnt(M,A,T))|M=N)))&(![Rho,A,T,N,M]: (sP1_prd(M,N,T,A,Rho)|(((no_right(M)&part_of(M,Rho))&cnt(M,A,T))&~M=N)))),
% 0.14/5.60 inference(miniscoping,[status(thm)],[f61])).
% 0.14/5.60 fof(f63,plain,(
% 0.14/5.60 ![X0,X1,X2,X3,X4]: (~sP1_prd(X0,X1,X2,X3,X4)|~no_right(X0)|~part_of(X0,X4)|~cnt(X0,X3,X2)|X0=X1)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f62])).
% 0.14/5.60 fof(f68,plain,(
% 0.14/5.60 ![X0,X1,X2,X3]: (sP0_prd(X0,X0,X1,X2,X3))),
% 0.14/5.60 inference(destructive_equality_resolution,[status(thm)],[f60])).
% 0.14/5.60 fof(f72,definition,(
% 0.14/5.60 sQ0_spl <=> (odrl_rel(rho1))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.60 fof(f74,plain,(
% 0.14/5.60 ~odrl_rel(rho1)|sQ0_spl),
% 0.14/5.60 inference(component_clause,[status(thm)],[f72])).
% 0.14/5.60 fof(f75,definition,(
% 0.14/5.60 sQ1_spl <=> (permission(l))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.60 fof(f77,plain,(
% 0.14/5.60 ~permission(l)|sQ1_spl),
% 0.14/5.60 inference(component_clause,[status(thm)],[f75])).
% 0.14/5.60 fof(f90,plain,(
% 0.14/5.60 $false|sQ0_spl),
% 0.14/5.60 inference(forward_subsumption_resolution,[status(thm)],[f74,f39])).
% 0.14/5.60 fof(f91,plain,(
% 0.14/5.60 sQ0_spl),
% 0.14/5.60 inference(contradiction_clause,[status(thm)],[f90])).
% 0.14/5.60 fof(f92,plain,(
% 0.14/5.60 $false|sQ1_spl),
% 0.14/5.60 inference(forward_subsumption_resolution,[status(thm)],[f77,f40])).
% 0.14/5.60 fof(f93,plain,(
% 0.14/5.60 sQ1_spl),
% 0.14/5.60 inference(contradiction_clause,[status(thm)],[f92])).
% 0.14/5.60 fof(f102,plain,(
% 0.14/5.60 ![X0,X1]: (~odrl_rel(X0)|~permission(l)|~part_of(l,X0)|~sP0_prd(sK0_skl(l,some_target,some_action,X0),l,some_target,some_action,X0)|sP1_prd(X1,sK1_skl(some_target,some_action,X0),some_target,some_action,X0))),
% 0.14/5.60 inference(resolution,[status(thm)],[f46,f30])).
% 0.14/5.60 fof(f104,definition,(
% 0.14/5.60 ![X0,X1]: (sQ7_spl <=> (~odrl_rel(X0)|~part_of(l,X0)|~sP0_prd(sK0_skl(l,some_target,some_action,X0),l,some_target,some_action,X0)|sP1_prd(X1,sK1_skl(some_target,some_action,X0),some_target,some_action,X0)))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/5.60 fof(f105,plain,(
% 0.14/5.60 ![X0,X1]: (~odrl_rel(X0)|~part_of(l,X0)|~sP0_prd(sK0_skl(l,some_target,some_action,X0),l,some_target,some_action,X0)|sP1_prd(X1,sK1_skl(some_target,some_action,X0),some_target,some_action,X0)|~sQ7_spl)),
% 0.14/5.60 inference(component_clause,[status(thm)],[f104])).
% 0.14/5.60 fof(f107,plain,(
% 0.14/5.60 sQ7_spl|~sQ1_spl),
% 0.14/5.60 inference(split_clause,[status(thm)],[f102,f104,f75])).
% 0.14/5.60 fof(f149,plain,(
% 0.14/5.60 ![X0,X1,X2,X3]: (~sP1_prd(n2,X0,X1,X2,X3)|~part_of(n2,X3)|~cnt(n2,X2,X1)|n2=X0)),
% 0.14/5.60 inference(resolution,[status(thm)],[f63,f42])).
% 0.14/5.60 fof(f150,plain,(
% 0.14/5.60 ![X0,X1,X2,X3]: (~sP1_prd(n1,X0,X1,X2,X3)|~part_of(n1,X3)|~cnt(n1,X2,X1)|n1=X0)),
% 0.14/5.60 inference(resolution,[status(thm)],[f63,f41])).
% 0.14/5.60 fof(f198,plain,(
% 0.14/5.60 ![X0,X1,X2]: (~sP1_prd(n2,X0,X1,X2,rho1)|~cnt(n2,X2,X1)|n2=X0)),
% 0.14/5.60 inference(resolution,[status(thm)],[f149,f45])).
% 0.14/5.60 fof(f199,plain,(
% 0.14/5.60 ![X0]: (~sP1_prd(n2,X0,some_target,some_action,rho1)|n2=X0)),
% 0.14/5.60 inference(resolution,[status(thm)],[f198,f48])).
% 0.14/5.60 fof(f235,plain,(
% 0.14/5.60 ![X0,X1,X2]: (~sP1_prd(n1,X0,X1,X2,rho1)|~cnt(n1,X2,X1)|n1=X0)),
% 0.14/5.60 inference(resolution,[status(thm)],[f150,f44])).
% 0.14/5.60 fof(f236,plain,(
% 0.14/5.60 ![X0]: (~sP1_prd(n1,X0,some_target,some_action,rho1)|n1=X0)),
% 0.14/5.60 inference(resolution,[status(thm)],[f235,f47])).
% 0.14/5.60 fof(f277,definition,(
% 0.14/5.60 sQ29_spl <=> (sP0_prd(sK0_skl(l,some_target,some_action,rho1),l,some_target,some_action,rho1))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/5.60 fof(f279,plain,(
% 0.14/5.60 ~sP0_prd(sK0_skl(l,some_target,some_action,rho1),l,some_target,some_action,rho1)|sQ29_spl),
% 0.14/5.60 inference(component_clause,[status(thm)],[f277])).
% 0.14/5.60 fof(f285,plain,(
% 0.14/5.60 cnt(sK0_skl(l,some_target,some_action,rho1),some_action,some_target)|sQ29_spl),
% 0.14/5.60 inference(resolution,[status(thm)],[f279,f59])).
% 0.14/5.60 fof(f286,plain,(
% 0.14/5.60 part_of(sK0_skl(l,some_target,some_action,rho1),rho1)|sQ29_spl),
% 0.14/5.60 inference(resolution,[status(thm)],[f279,f58])).
% 0.14/5.60 fof(f287,plain,(
% 0.14/5.60 permission(sK0_skl(l,some_target,some_action,rho1))|sQ29_spl),
% 0.14/5.60 inference(resolution,[status(thm)],[f279,f57])).
% 0.14/5.60 fof(f289,plain,(
% 0.14/5.60 ~part_of(sK0_skl(l,some_target,some_action,rho1),rho1)|~cnt(sK0_skl(l,some_target,some_action,rho1),some_action,some_target)|sK0_skl(l,some_target,some_action,rho1)=l|sQ29_spl),
% 0.14/5.60 inference(resolution,[status(thm)],[f287,f53])).
% 0.14/5.60 fof(f291,definition,(
% 0.14/5.60 sQ31_spl <=> (part_of(sK0_skl(l,some_target,some_action,rho1),rho1))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/5.60 fof(f293,plain,(
% 0.14/5.60 ~part_of(sK0_skl(l,some_target,some_action,rho1),rho1)|sQ31_spl),
% 0.14/5.60 inference(component_clause,[status(thm)],[f291])).
% 0.14/5.60 fof(f294,definition,(
% 0.14/5.60 sQ32_spl <=> (cnt(sK0_skl(l,some_target,some_action,rho1),some_action,some_target))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/5.60 fof(f296,plain,(
% 0.14/5.60 ~cnt(sK0_skl(l,some_target,some_action,rho1),some_action,some_target)|sQ32_spl),
% 0.14/5.60 inference(component_clause,[status(thm)],[f294])).
% 0.14/5.60 fof(f297,definition,(
% 0.14/5.60 sQ33_spl <=> (sK0_skl(l,some_target,some_action,rho1)=l)),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/5.60 fof(f298,plain,(
% 0.14/5.60 sK0_skl(l,some_target,some_action,rho1)=l|~sQ33_spl),
% 0.14/5.60 inference(component_clause,[status(thm)],[f297])).
% 0.14/5.60 fof(f300,plain,(
% 0.14/5.60 ~sQ31_spl|~sQ32_spl|sQ33_spl|sQ29_spl),
% 0.14/5.60 inference(split_clause,[status(thm)],[f289,f291,f294,f297,f277])).
% 0.14/5.60 fof(f309,plain,(
% 0.14/5.60 ![X0]: (~odrl_rel(rho1)|~sP0_prd(sK0_skl(l,some_target,some_action,rho1),l,some_target,some_action,rho1)|sP1_prd(X0,sK1_skl(some_target,some_action,rho1),some_target,some_action,rho1)|~sQ7_spl)),
% 0.14/5.60 inference(resolution,[status(thm)],[f105,f43])).
% 0.14/5.60 fof(f310,definition,(
% 0.14/5.60 ![X0]: (sQ36_spl <=> (sP1_prd(X0,sK1_skl(some_target,some_action,rho1),some_target,some_action,rho1)))),
% 0.14/5.60 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/5.60 fof(f311,plain,(
% 0.14/5.60 ![X0]: (sP1_prd(X0,sK1_skl(some_target,some_action,rho1),some_target,some_action,rho1)|~sQ36_spl)),
% 0.14/5.60 inference(component_clause,[status(thm)],[f310])).
% 0.14/5.60 fof(f313,plain,(
% 0.14/5.60 ~sQ0_spl|~sQ29_spl|sQ36_spl|~sQ7_spl),
% 0.14/5.60 inference(split_clause,[status(thm)],[f309,f72,f277,f310,f104])).
% 0.14/5.60 fof(f332,plain,(
% 0.14/5.60 n1=sK1_skl(some_target,some_action,rho1)|~sQ36_spl),
% 0.14/5.60 inference(resolution,[status(thm)],[f311,f236])).
% 0.14/5.60 fof(f333,plain,(
% 0.14/5.60 n2=sK1_skl(some_target,some_action,rho1)|~sQ36_spl),
% 0.14/5.60 inference(resolution,[status(thm)],[f311,f199])).
% 0.14/5.60 fof(f353,plain,(
% 0.14/5.60 ~sP0_prd(l,l,some_target,some_action,rho1)|~sQ33_spl|sQ29_spl),
% 0.14/5.60 inference(forward_demodulation,[status(thm)],[f298,f279])).
% 0.14/5.60 fof(f354,plain,(
% 0.14/5.60 $false|~sQ33_spl|sQ29_spl),
% 0.14/5.60 inference(forward_subsumption_resolution,[status(thm)],[f353,f68])).
% 0.14/5.60 fof(f355,plain,(
% 0.14/5.60 ~sQ33_spl|sQ29_spl),
% 0.14/5.60 inference(contradiction_clause,[status(thm)],[f354])).
% 0.14/5.60 fof(f383,plain,(
% 0.14/5.60 $false|sQ31_spl|sQ29_spl),
% 0.14/5.60 inference(forward_subsumption_resolution,[status(thm)],[f286,f293])).
% 0.14/5.60 fof(f384,plain,(
% 0.14/5.60 sQ31_spl|sQ29_spl),
% 0.14/5.60 inference(contradiction_clause,[status(thm)],[f383])).
% 0.14/5.60 fof(f414,plain,(
% 0.14/5.60 $false|sQ29_spl|sQ32_spl),
% 0.14/5.60 inference(forward_subsumption_resolution,[status(thm)],[f296,f285])).
% 0.14/5.60 fof(f415,plain,(
% 0.14/5.60 sQ29_spl|sQ32_spl),
% 0.14/5.60 inference(contradiction_clause,[status(thm)],[f414])).
% 0.14/5.60 fof(f436,plain,(
% 0.14/5.60 n2=n1|~sQ36_spl),
% 0.14/5.60 inference(forward_demodulation,[status(thm)],[f332,f333])).
% 0.14/5.60 fof(f437,plain,(
% 0.14/5.60 $false|~sQ36_spl),
% 0.14/5.60 inference(forward_subsumption_resolution,[status(thm)],[f436,f51])).
% 0.14/5.60 fof(f438,plain,(
% 0.14/5.60 ~sQ36_spl),
% 0.14/5.60 inference(contradiction_clause,[status(thm)],[f437])).
% 0.14/5.60 fof(f439,plain,(
% 0.14/5.60 $false),
% 0.14/5.60 inference(sat_refutation,[status(thm)],[f91,f93,f107,f300,f313,f355,f384,f415,f438])).
% 0.14/5.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.62 % Elapsed time: 0.030757 seconds
% 0.14/5.62 % CPU time: 0.120350 seconds
% 0.14/5.62 % Total memory used: 4.547 MB
% 0.14/5.62 % Net memory used: 4.440 MB
%------------------------------------------------------------------------------