%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT005+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Thu Sep 24 01:25:39 PM UTC 2026
% Result : Theorem 7.38s 1.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT005+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.47 % Computer : n001.cluster.edu
% 0.20/0.47 % Model : x86_64 x86_64
% 0.20/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.47 % Memory : 8046.5625MB
% 0.20/0.47 % OS : Linux 6.8.0-71-generic
% 0.20/0.47 % CPULimit : 300
% 0.20/0.47 % WCLimit : 300
% 0.20/0.47 % DateTime : Mon Sep 21 01:26:13 UTC 2026
% 0.20/0.47 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 7.38/1.56 % Refutation found
% 7.38/1.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.38/1.56 % SZS output start CNFRefutation for theBenchmark
% 7.38/1.56 fof(f1,axiom,(
% 7.38/1.56 (! [X,Y] :~ ( greater(X,Y)& X = Y ) )),
% 7.38/1.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.38/1.56 fof(f5,axiom,(
% 7.38/1.56 (! [X,T] :( organization(X,T)=> (? [P] : survival_chance(X,P,T) )) )),
% 7.38/1.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.38/1.56 fof(f6,axiom,(
% 7.38/1.56 (! [X,T,T1,T2] :( ( organization(X,T1)& organization(X,T2)& greater(T,T1)& greater(T2,T) )=> organization(X,T) ) )),
% 7.38/1.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.38/1.56 fof(f7,axiom,(
% 7.38/1.56 (! [X,Ta,Tb] :( reorganization(X,Ta,Tb)=> greater(Tb,Ta) ) )),
% 7.38/1.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.38/1.56 fof(f10,hypothesis,(
% 7.38/1.56 (! [X,Y,Re,C,C1,C2,Ta,Tb,Tc] :( ( organization(X,Ta)& organization(Y,Ta)& organization(Y,Tc)& class(X,C,Ta)& class(Y,C,Ta)& reorganization(X,Ta,Tb)& reorganization(Y,Ta,Tc)& reorganization_type(X,Re,Ta)& reorganization_type(Y,Re,Ta)& complexity(X,C1,Ta)& complexity(Y,C2,Ta)& greater(C2,C1) )=> greater(Tc,Tb) ) )),
% 7.38/1.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.38/1.56 fof(f11,hypothesis,(
% 7.38/1.56 (! [X,Y,Re,C,P,P1,P2,C1,C2,Ta,Tb,Tc] :( ( organization(X,Ta)& organization(Y,Ta)& organization(X,Tb)& organization(Y,Tb)& class(X,C,Ta)& class(Y,C,Ta)& survival_chance(X,P,Ta)& survival_chance(Y,P,Ta)& reorganization(X,Ta,Tb)& reorganization(Y,Ta,Tc)& reorganization_type(X,Re,Ta)& reorganization_type(Y,Re,Ta)& survival_chance(X,P1,Tb)& survival_chance(Y,P2,Tb)& complexity(X,C1,Ta)& complexity(Y,C2,Ta)& greater(C2,C1) )=> ( greater(P1,P2)| P1 = P2 ) ) )),
% 7.38/1.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.38/1.56 fof(f13,conjecture,(
% 7.38/1.56 (! [X,Y,Re,C,P,P1,P2,C1,C2,T,Ta,Tb,Tc] :( ( organization(X,Ta)& organization(Y,Ta)& organization(X,Tc)& organization(Y,Tc)& class(X,C,Ta)& class(Y,C,Ta)& survival_chance(X,P,Ta)& survival_chance(Y,P,Ta)& reorganization(X,Ta,Tb)& reorganization(Y,Ta,Tc)& reorganization_type(X,Re,Ta)& reorganization_type(Y,Re,Ta)& reorganization_free(X,Tb,Tc)& survival_chance(X,P1,T)& survival_chance(Y,P2,T)& complexity(X,C1,Ta)& complexity(Y,C2,Ta)& greater(C2,C1)& ( T = Tc=> greater(P1,P2) ) )=> ( T = Tb=> ( greater(P1,P2)| P1 = P2 ) ) ) )),
% 7.38/1.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.38/1.56 fof(f14,negated_conjecture,(
% 7.38/1.56 ~((! [X,Y,Re,C,P,P1,P2,C1,C2,T,Ta,Tb,Tc] :( ( organization(X,Ta)& organization(Y,Ta)& organization(X,Tc)& organization(Y,Tc)& class(X,C,Ta)& class(Y,C,Ta)& survival_chance(X,P,Ta)& survival_chance(Y,P,Ta)& reorganization(X,Ta,Tb)& reorganization(Y,Ta,Tc)& reorganization_type(X,Re,Ta)& reorganization_type(Y,Re,Ta)& reorganization_free(X,Tb,Tc)& survival_chance(X,P1,T)& survival_chance(Y,P2,T)& complexity(X,C1,Ta)& complexity(Y,C2,Ta)& greater(C2,C1)& ( T = Tc=> greater(P1,P2) ) )=> ( T = Tb=> ( greater(P1,P2)| P1 = P2 ) ) ) ))),
% 7.38/1.56 inference(negated_conjecture,[status(cth)],[f13])).
% 7.38/1.56 fof(f15,plain,(
% 7.38/1.56 ![X,Y]: (~greater(X,Y)|~X=Y)),
% 7.38/1.56 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 7.38/1.56 fof(f16,plain,(
% 7.38/1.56 ![X0,X1]: (~greater(X0,X1)|~X0=X1)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f15])).
% 7.38/1.56 fof(f25,plain,(
% 7.38/1.56 ![X,T]: (~organization(X,T)|(?[P]: survival_chance(X,P,T)))),
% 7.38/1.56 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 7.38/1.56 fof(f26,plain,(
% 7.38/1.56 ![X,T]: (~organization(X,T)|survival_chance(X,sK0_skl(T,X),T))),
% 7.38/1.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(P,sK0_skl(T,X))],[f25])).
% 7.38/1.56 fof(f27,plain,(
% 7.38/1.56 ![X0,X1]: (~organization(X0,X1)|survival_chance(X0,sK0_skl(X1,X0),X1))),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f26])).
% 7.38/1.56 fof(f28,plain,(
% 7.38/1.56 ![X,T,T1,T2]: ((((~organization(X,T1)|~organization(X,T2))|~greater(T,T1))|~greater(T2,T))|organization(X,T))),
% 7.38/1.56 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 7.38/1.56 fof(f29,plain,(
% 7.38/1.56 ![X,T]: ((![T2]: ((![T1]: ((~organization(X,T1)|~organization(X,T2))|~greater(T,T1)))|~greater(T2,T)))|organization(X,T))),
% 7.38/1.56 inference(miniscoping,[status(thm)],[f28])).
% 7.38/1.56 fof(f30,plain,(
% 7.38/1.56 ![X0,X1,X2,X3]: (~organization(X0,X1)|~organization(X0,X2)|~greater(X3,X1)|~greater(X2,X3)|organization(X0,X3))),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f29])).
% 7.38/1.56 fof(f31,plain,(
% 7.38/1.56 ![X,Ta,Tb]: (~reorganization(X,Ta,Tb)|greater(Tb,Ta))),
% 7.38/1.56 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 7.38/1.56 fof(f32,plain,(
% 7.38/1.56 ![Ta,Tb]: ((![X]: ~reorganization(X,Ta,Tb))|greater(Tb,Ta))),
% 7.38/1.56 inference(miniscoping,[status(thm)],[f31])).
% 7.38/1.56 fof(f33,plain,(
% 7.38/1.56 ![X0,X1,X2]: (~reorganization(X0,X1,X2)|greater(X2,X1))),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f32])).
% 7.38/1.56 fof(f40,plain,(
% 7.38/1.56 ![X,Y,Re,C,C1,C2,Ta,Tb,Tc]: ((((((((((((~organization(X,Ta)|~organization(Y,Ta))|~organization(Y,Tc))|~class(X,C,Ta))|~class(Y,C,Ta))|~reorganization(X,Ta,Tb))|~reorganization(Y,Ta,Tc))|~reorganization_type(X,Re,Ta))|~reorganization_type(Y,Re,Ta))|~complexity(X,C1,Ta))|~complexity(Y,C2,Ta))|~greater(C2,C1))|greater(Tc,Tb))),
% 7.38/1.56 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 7.38/1.56 fof(f41,plain,(
% 7.38/1.56 ![Tb,Tc]: ((![C1,C2]: ((![Y,Ta]: ((![X]: ((![Re]: (((((![C]: ((((~organization(X,Ta)|~organization(Y,Ta))|~organization(Y,Tc))|~class(X,C,Ta))|~class(Y,C,Ta)))|~reorganization(X,Ta,Tb))|~reorganization(Y,Ta,Tc))|~reorganization_type(X,Re,Ta))|~reorganization_type(Y,Re,Ta)))|~complexity(X,C1,Ta)))|~complexity(Y,C2,Ta)))|~greater(C2,C1)))|greater(Tc,Tb))),
% 7.38/1.56 inference(miniscoping,[status(thm)],[f40])).
% 7.38/1.56 fof(f42,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~organization(X0,X1)|~organization(X2,X1)|~organization(X2,X3)|~class(X0,X4,X1)|~class(X2,X4,X1)|~reorganization(X0,X1,X5)|~reorganization(X2,X1,X3)|~reorganization_type(X0,X6,X1)|~reorganization_type(X2,X6,X1)|~complexity(X0,X7,X1)|~complexity(X2,X8,X1)|~greater(X8,X7)|greater(X3,X5))),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f41])).
% 7.38/1.56 fof(f43,plain,(
% 7.38/1.56 ![X,Y,Re,C,P,P1,P2,C1,C2,Ta,Tb,Tc]: (((((((((((((((((~organization(X,Ta)|~organization(Y,Ta))|~organization(X,Tb))|~organization(Y,Tb))|~class(X,C,Ta))|~class(Y,C,Ta))|~survival_chance(X,P,Ta))|~survival_chance(Y,P,Ta))|~reorganization(X,Ta,Tb))|~reorganization(Y,Ta,Tc))|~reorganization_type(X,Re,Ta))|~reorganization_type(Y,Re,Ta))|~survival_chance(X,P1,Tb))|~survival_chance(Y,P2,Tb))|~complexity(X,C1,Ta))|~complexity(Y,C2,Ta))|~greater(C2,C1))|(greater(P1,P2)|P1=P2))),
% 7.38/1.56 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 7.38/1.56 fof(f44,plain,(
% 7.38/1.56 ![P1,P2]: ((![C1,C2]: ((![Y,Ta]: ((![X]: ((![Tb]: (((![Re]: (((((![P]: (((![C]: (((((~organization(X,Ta)|~organization(Y,Ta))|~organization(X,Tb))|~organization(Y,Tb))|~class(X,C,Ta))|~class(Y,C,Ta)))|~survival_chance(X,P,Ta))|~survival_chance(Y,P,Ta)))|~reorganization(X,Ta,Tb))|(![Tc]: ~reorganization(Y,Ta,Tc)))|~reorganization_type(X,Re,Ta))|~reorganization_type(Y,Re,Ta)))|~survival_chance(X,P1,Tb))|~survival_chance(Y,P2,Tb)))|~complexity(X,C1,Ta)))|~complexity(Y,C2,Ta)))|~greater(C2,C1)))|(greater(P1,P2)|P1=P2))),
% 7.38/1.56 inference(miniscoping,[status(thm)],[f43])).
% 7.38/1.56 fof(f45,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~organization(X0,X1)|~organization(X2,X1)|~organization(X0,X3)|~organization(X2,X3)|~class(X0,X4,X1)|~class(X2,X4,X1)|~survival_chance(X0,X5,X1)|~survival_chance(X2,X5,X1)|~reorganization(X0,X1,X3)|~reorganization(X2,X1,X6)|~reorganization_type(X0,X7,X1)|~reorganization_type(X2,X7,X1)|~survival_chance(X0,X8,X3)|~survival_chance(X2,X9,X3)|~complexity(X0,X10,X1)|~complexity(X2,X11,X1)|~greater(X11,X10)|greater(X8,X9)|X8=X9)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f44])).
% 7.38/1.56 fof(f54,plain,(
% 7.38/1.56 (?[X,Y,Re,C,P,P1,P2,C1,C2,T,Ta,Tb,Tc]: (((((((((((((((((((organization(X,Ta)&organization(Y,Ta))&organization(X,Tc))&organization(Y,Tc))&class(X,C,Ta))&class(Y,C,Ta))&survival_chance(X,P,Ta))&survival_chance(Y,P,Ta))&reorganization(X,Ta,Tb))&reorganization(Y,Ta,Tc))&reorganization_type(X,Re,Ta))&reorganization_type(Y,Re,Ta))&reorganization_free(X,Tb,Tc))&survival_chance(X,P1,T))&survival_chance(Y,P2,T))&complexity(X,C1,Ta))&complexity(Y,C2,Ta))&greater(C2,C1))&(~T=Tc|greater(P1,P2)))&(T=Tb&(~greater(P1,P2)&~P1=P2))))),
% 7.38/1.56 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 7.38/1.56 fof(f55,plain,(
% 7.38/1.56 ?[P1,P2,T,Tb]: ((?[Tc]: ((?[C1,C2]: ((?[Y,Ta]: ((?[X]: (((((?[Re]: (((((?[P]: (((?[C]: (((((organization(X,Ta)&organization(Y,Ta))&organization(X,Tc))&organization(Y,Tc))&class(X,C,Ta))&class(Y,C,Ta)))&survival_chance(X,P,Ta))&survival_chance(Y,P,Ta)))&reorganization(X,Ta,Tb))&reorganization(Y,Ta,Tc))&reorganization_type(X,Re,Ta))&reorganization_type(Y,Re,Ta)))&reorganization_free(X,Tb,Tc))&survival_chance(X,P1,T))&survival_chance(Y,P2,T))&complexity(X,C1,Ta)))&complexity(Y,C2,Ta)))&greater(C2,C1)))&(~T=Tc|greater(P1,P2))))&(T=Tb&(~greater(P1,P2)&~P1=P2)))),
% 7.38/1.56 inference(miniscoping,[status(thm)],[f54])).
% 7.38/1.56 fof(f56,plain,(
% 7.38/1.56 (((((((((((((((((((organization(sK13_skl,sK12_skl)&organization(sK11_skl,sK12_skl))&organization(sK13_skl,sK8_skl))&organization(sK11_skl,sK8_skl))&class(sK13_skl,sK16_skl,sK12_skl))&class(sK11_skl,sK16_skl,sK12_skl))&survival_chance(sK13_skl,sK15_skl,sK12_skl))&survival_chance(sK11_skl,sK15_skl,sK12_skl))&reorganization(sK13_skl,sK12_skl,sK7_skl))&reorganization(sK11_skl,sK12_skl,sK8_skl))&reorganization_type(sK13_skl,sK14_skl,sK12_skl))&reorganization_type(sK11_skl,sK14_skl,sK12_skl))&reorganization_free(sK13_skl,sK7_skl,sK8_skl))&survival_chance(sK13_skl,sK4_skl,sK6_skl))&survival_chance(sK11_skl,sK5_skl,sK6_skl))&complexity(sK13_skl,sK9_skl,sK12_skl))&complexity(sK11_skl,sK10_skl,sK12_skl))&greater(sK10_skl,sK9_skl))&(~sK6_skl=sK8_skl|greater(sK4_skl,sK5_skl)))&(sK6_skl=sK7_skl&(~greater(sK4_skl,sK5_skl)&~sK4_skl=sK5_skl)))),
% 7.38/1.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl]),skolemize(P1,sK4_skl),skolemize(P2,sK5_skl),skolemize(T,sK6_skl),skolemize(Tb,sK7_skl),skolemize(Tc,sK8_skl),skolemize(C1,sK9_skl),skolemize(C2,sK10_skl),skolemize(Y,sK11_skl),skolemize(Ta,sK12_skl),skolemize(X,sK13_skl),skolemize(Re,sK14_skl),skolemize(P,sK15_skl),skolemize(C,sK16_skl)],[f55])).
% 7.38/1.56 fof(f57,plain,(
% 7.38/1.56 organization(sK13_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f58,plain,(
% 7.38/1.56 organization(sK11_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f59,plain,(
% 7.38/1.56 organization(sK13_skl,sK8_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f60,plain,(
% 7.38/1.56 organization(sK11_skl,sK8_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f61,plain,(
% 7.38/1.56 class(sK13_skl,sK16_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f62,plain,(
% 7.38/1.56 class(sK11_skl,sK16_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f63,plain,(
% 7.38/1.56 survival_chance(sK13_skl,sK15_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f64,plain,(
% 7.38/1.56 survival_chance(sK11_skl,sK15_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f65,plain,(
% 7.38/1.56 reorganization(sK13_skl,sK12_skl,sK7_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f66,plain,(
% 7.38/1.56 reorganization(sK11_skl,sK12_skl,sK8_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f67,plain,(
% 7.38/1.56 reorganization_type(sK13_skl,sK14_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f68,plain,(
% 7.38/1.56 reorganization_type(sK11_skl,sK14_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f70,plain,(
% 7.38/1.56 survival_chance(sK13_skl,sK4_skl,sK6_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f71,plain,(
% 7.38/1.56 survival_chance(sK11_skl,sK5_skl,sK6_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f72,plain,(
% 7.38/1.56 complexity(sK13_skl,sK9_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f73,plain,(
% 7.38/1.56 complexity(sK11_skl,sK10_skl,sK12_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f74,plain,(
% 7.38/1.56 greater(sK10_skl,sK9_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f76,plain,(
% 7.38/1.56 sK6_skl=sK7_skl),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f77,plain,(
% 7.38/1.56 ~greater(sK4_skl,sK5_skl)),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f78,plain,(
% 7.38/1.56 ~sK4_skl=sK5_skl),
% 7.38/1.56 inference(cnf_transformation,[status(thm)],[f56])).
% 7.38/1.56 fof(f82,definition,(
% 7.38/1.56 sQ1_spl <=> (greater(sK4_skl,sK5_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f83,plain,(
% 7.38/1.56 greater(sK4_skl,sK5_skl)|~sQ1_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f82])).
% 7.38/1.56 fof(f86,plain,(
% 7.38/1.56 ![X0]: (~greater(X0,X0))),
% 7.38/1.56 inference(destructive_equality_resolution,[status(thm)],[f16])).
% 7.38/1.56 fof(f90,plain,(
% 7.38/1.56 ![X0,X1]: (~organization(sK11_skl,X0)|~greater(X1,sK12_skl)|~greater(X0,X1)|organization(sK11_skl,X1))),
% 7.38/1.56 inference(resolution,[status(thm)],[f30,f58])).
% 7.38/1.56 fof(f92,plain,(
% 7.38/1.56 ![X0,X1]: (~organization(sK13_skl,X0)|~greater(X1,sK12_skl)|~greater(X0,X1)|organization(sK13_skl,X1))),
% 7.38/1.56 inference(resolution,[status(thm)],[f30,f57])).
% 7.38/1.56 fof(f94,plain,(
% 7.38/1.56 survival_chance(sK11_skl,sK0_skl(sK8_skl,sK11_skl),sK8_skl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f60,f27])).
% 7.38/1.56 fof(f99,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5]: (~organization(sK13_skl,sK12_skl)|~organization(X0,sK12_skl)|~organization(X0,X1)|~class(X0,sK16_skl,sK12_skl)|~reorganization(sK13_skl,sK12_skl,X2)|~reorganization(X0,sK12_skl,X1)|~reorganization_type(sK13_skl,X3,sK12_skl)|~reorganization_type(X0,X3,sK12_skl)|~complexity(sK13_skl,X4,sK12_skl)|~complexity(X0,X5,sK12_skl)|~greater(X5,X4)|greater(X1,X2))),
% 7.38/1.56 inference(resolution,[status(thm)],[f42,f61])).
% 7.38/1.56 fof(f100,definition,(
% 7.38/1.56 sQ2_spl <=> (organization(sK11_skl,sK12_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f102,plain,(
% 7.38/1.56 ~organization(sK11_skl,sK12_skl)|sQ2_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f100])).
% 7.38/1.56 fof(f107,definition,(
% 7.38/1.56 sQ4_spl <=> (organization(sK13_skl,sK12_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f109,plain,(
% 7.38/1.56 ~organization(sK13_skl,sK12_skl)|sQ4_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f107])).
% 7.38/1.56 fof(f110,definition,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5]: (sQ5_spl <=> (~organization(X0,sK12_skl)|~organization(X0,X1)|~class(X0,sK16_skl,sK12_skl)|~reorganization(sK13_skl,sK12_skl,X2)|~reorganization(X0,sK12_skl,X1)|~reorganization_type(sK13_skl,X3,sK12_skl)|~reorganization_type(X0,X3,sK12_skl)|~complexity(sK13_skl,X4,sK12_skl)|~complexity(X0,X5,sK12_skl)|~greater(X5,X4)|greater(X1,X2)))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f111,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5]: (~organization(X0,sK12_skl)|~organization(X0,X1)|~class(X0,sK16_skl,sK12_skl)|~reorganization(sK13_skl,sK12_skl,X2)|~reorganization(X0,sK12_skl,X1)|~reorganization_type(sK13_skl,X3,sK12_skl)|~reorganization_type(X0,X3,sK12_skl)|~complexity(sK13_skl,X4,sK12_skl)|~complexity(X0,X5,sK12_skl)|~greater(X5,X4)|greater(X1,X2)|~sQ5_spl)),
% 7.38/1.56 inference(component_clause,[status(thm)],[f110])).
% 7.38/1.56 fof(f113,plain,(
% 7.38/1.56 ~sQ4_spl|sQ5_spl),
% 7.38/1.56 inference(split_clause,[status(thm)],[f99,f107,f110])).
% 7.38/1.56 fof(f114,plain,(
% 7.38/1.56 $false|sQ4_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f109,f57])).
% 7.38/1.56 fof(f115,plain,(
% 7.38/1.56 sQ4_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f114])).
% 7.38/1.56 fof(f116,plain,(
% 7.38/1.56 $false|sQ2_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f102,f58])).
% 7.38/1.56 fof(f117,plain,(
% 7.38/1.56 sQ2_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f116])).
% 7.38/1.56 fof(f119,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~organization(sK13_skl,sK12_skl)|~organization(X0,sK12_skl)|~organization(sK13_skl,X1)|~organization(X0,X1)|~class(X0,sK16_skl,sK12_skl)|~survival_chance(sK13_skl,X2,sK12_skl)|~survival_chance(X0,X2,sK12_skl)|~reorganization(sK13_skl,sK12_skl,X1)|~reorganization(X0,sK12_skl,X3)|~reorganization_type(sK13_skl,X4,sK12_skl)|~reorganization_type(X0,X4,sK12_skl)|~survival_chance(sK13_skl,X5,X1)|~survival_chance(X0,X6,X1)|~complexity(sK13_skl,X7,sK12_skl)|~complexity(X0,X8,sK12_skl)|~greater(X8,X7)|greater(X5,X6)|X5=X6)),
% 7.38/1.56 inference(resolution,[status(thm)],[f45,f61])).
% 7.38/1.56 fof(f124,definition,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (sQ7_spl <=> (~organization(X0,sK12_skl)|~organization(sK13_skl,X1)|~organization(X0,X1)|~class(X0,sK16_skl,sK12_skl)|~survival_chance(sK13_skl,X2,sK12_skl)|~survival_chance(X0,X2,sK12_skl)|~reorganization(sK13_skl,sK12_skl,X1)|~reorganization(X0,sK12_skl,X3)|~reorganization_type(sK13_skl,X4,sK12_skl)|~reorganization_type(X0,X4,sK12_skl)|~survival_chance(sK13_skl,X5,X1)|~survival_chance(X0,X6,X1)|~complexity(sK13_skl,X7,sK12_skl)|~complexity(X0,X8,sK12_skl)|~greater(X8,X7)|greater(X5,X6)|X5=X6))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f125,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~organization(X0,sK12_skl)|~organization(sK13_skl,X1)|~organization(X0,X1)|~class(X0,sK16_skl,sK12_skl)|~survival_chance(sK13_skl,X2,sK12_skl)|~survival_chance(X0,X2,sK12_skl)|~reorganization(sK13_skl,sK12_skl,X1)|~reorganization(X0,sK12_skl,X3)|~reorganization_type(sK13_skl,X4,sK12_skl)|~reorganization_type(X0,X4,sK12_skl)|~survival_chance(sK13_skl,X5,X1)|~survival_chance(X0,X6,X1)|~complexity(sK13_skl,X7,sK12_skl)|~complexity(X0,X8,sK12_skl)|~greater(X8,X7)|greater(X5,X6)|X5=X6|~sQ7_spl)),
% 7.38/1.56 inference(component_clause,[status(thm)],[f124])).
% 7.38/1.56 fof(f127,plain,(
% 7.38/1.56 ~sQ4_spl|sQ7_spl),
% 7.38/1.56 inference(split_clause,[status(thm)],[f119,f107,f124])).
% 7.38/1.56 fof(f129,plain,(
% 7.38/1.56 reorganization(sK13_skl,sK12_skl,sK6_skl)),
% 7.38/1.56 inference(forward_demodulation,[status(thm)],[f76,f65])).
% 7.38/1.56 fof(f131,plain,(
% 7.38/1.56 greater(sK6_skl,sK12_skl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f129,f33])).
% 7.38/1.56 fof(f149,definition,(
% 7.38/1.56 sQ8_spl <=> (organization(sK13_skl,sK6_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f158,definition,(
% 7.38/1.56 sQ11_spl <=> (greater(sK8_skl,sK6_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f174,plain,(
% 7.38/1.56 ![X0]: (~greater(X0,sK12_skl)|~greater(sK8_skl,X0)|organization(sK11_skl,X0))),
% 7.38/1.56 inference(resolution,[status(thm)],[f90,f60])).
% 7.38/1.56 fof(f178,plain,(
% 7.38/1.56 ![X0]: (~greater(X0,sK12_skl)|~greater(sK8_skl,X0)|organization(sK13_skl,X0))),
% 7.38/1.56 inference(resolution,[status(thm)],[f92,f59])).
% 7.38/1.56 fof(f181,plain,(
% 7.38/1.56 ~greater(sK8_skl,sK6_skl)|organization(sK11_skl,sK6_skl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f174,f131])).
% 7.38/1.56 fof(f185,definition,(
% 7.38/1.56 sQ13_spl <=> (organization(sK11_skl,sK8_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f187,plain,(
% 7.38/1.56 ~organization(sK11_skl,sK8_skl)|sQ13_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f185])).
% 7.38/1.56 fof(f189,definition,(
% 7.38/1.56 sQ14_spl <=> (organization(sK11_skl,sK6_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f192,plain,(
% 7.38/1.56 ~sQ11_spl|sQ14_spl),
% 7.38/1.56 inference(split_clause,[status(thm)],[f181,f158,f189])).
% 7.38/1.56 fof(f194,plain,(
% 7.38/1.56 ~greater(sK8_skl,sK6_skl)|organization(sK13_skl,sK6_skl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f178,f131])).
% 7.38/1.56 fof(f196,plain,(
% 7.38/1.56 ~sQ11_spl|sQ8_spl),
% 7.38/1.56 inference(split_clause,[status(thm)],[f194,f158,f149])).
% 7.38/1.56 fof(f233,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4]: (~organization(X0,sK12_skl)|~organization(X0,X1)|~class(X0,sK16_skl,sK12_skl)|~reorganization(X0,sK12_skl,X1)|~reorganization_type(sK13_skl,X2,sK12_skl)|~reorganization_type(X0,X2,sK12_skl)|~complexity(sK13_skl,X3,sK12_skl)|~complexity(X0,X4,sK12_skl)|~greater(X4,X3)|greater(X1,sK6_skl)|~sQ5_spl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f111,f129])).
% 7.38/1.56 fof(f239,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~organization(X0,sK12_skl)|~organization(sK13_skl,X1)|~organization(X0,X1)|~class(X0,sK16_skl,sK12_skl)|~survival_chance(X0,sK15_skl,sK12_skl)|~reorganization(sK13_skl,sK12_skl,X1)|~reorganization(X0,sK12_skl,X2)|~reorganization_type(sK13_skl,X3,sK12_skl)|~reorganization_type(X0,X3,sK12_skl)|~survival_chance(sK13_skl,X4,X1)|~survival_chance(X0,X5,X1)|~complexity(sK13_skl,X6,sK12_skl)|~complexity(X0,X7,sK12_skl)|~greater(X7,X6)|greater(X4,X5)|X4=X5|~sQ7_spl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f125,f63])).
% 7.38/1.56 fof(f327,definition,(
% 7.38/1.56 sQ34_spl <=> (sK4_skl=sK5_skl)),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f328,plain,(
% 7.38/1.56 sK4_skl=sK5_skl|~sQ34_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f327])).
% 7.38/1.56 fof(f341,plain,(
% 7.38/1.56 $false|~sQ1_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f83,f77])).
% 7.38/1.56 fof(f342,plain,(
% 7.38/1.56 ~sQ1_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f341])).
% 7.38/1.56 fof(f345,plain,(
% 7.38/1.56 $false|~sQ34_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f328,f78])).
% 7.38/1.56 fof(f346,plain,(
% 7.38/1.56 ~sQ34_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f345])).
% 7.38/1.56 fof(f559,plain,(
% 7.38/1.56 ![X0,X1,X2]: (~organization(sK11_skl,sK12_skl)|~organization(sK11_skl,sK8_skl)|~class(sK11_skl,sK16_skl,sK12_skl)|~reorganization_type(sK13_skl,X0,sK12_skl)|~reorganization_type(sK11_skl,X0,sK12_skl)|~complexity(sK13_skl,X1,sK12_skl)|~complexity(sK11_skl,X2,sK12_skl)|~greater(X2,X1)|greater(sK8_skl,sK6_skl)|~sQ5_spl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f233,f66])).
% 7.38/1.56 fof(f561,definition,(
% 7.38/1.56 sQ59_spl <=> (class(sK11_skl,sK16_skl,sK12_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f563,plain,(
% 7.38/1.56 ~class(sK11_skl,sK16_skl,sK12_skl)|sQ59_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f561])).
% 7.38/1.56 fof(f564,definition,(
% 7.38/1.56 ![X0]: (sQ60_spl <=> (~reorganization_type(sK13_skl,X0,sK12_skl)|~reorganization_type(sK11_skl,X0,sK12_skl)))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f565,plain,(
% 7.38/1.56 ![X0]: (~reorganization_type(sK13_skl,X0,sK12_skl)|~reorganization_type(sK11_skl,X0,sK12_skl)|~sQ60_spl)),
% 7.38/1.56 inference(component_clause,[status(thm)],[f564])).
% 7.38/1.56 fof(f567,definition,(
% 7.38/1.56 ![X1,X2]: (sQ61_spl <=> (~complexity(sK13_skl,X1,sK12_skl)|~complexity(sK11_skl,X2,sK12_skl)|~greater(X2,X1)))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f568,plain,(
% 7.38/1.56 ![X0,X1]: (~complexity(sK13_skl,X0,sK12_skl)|~complexity(sK11_skl,X1,sK12_skl)|~greater(X1,X0)|~sQ61_spl)),
% 7.38/1.56 inference(component_clause,[status(thm)],[f567])).
% 7.38/1.56 fof(f570,plain,(
% 7.38/1.56 ~sQ2_spl|~sQ13_spl|~sQ59_spl|sQ60_spl|sQ61_spl|sQ11_spl|~sQ5_spl),
% 7.38/1.56 inference(split_clause,[status(thm)],[f559,f100,f185,f561,f564,f567,f158,f110])).
% 7.38/1.56 fof(f584,plain,(
% 7.38/1.56 $false|sQ59_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f563,f62])).
% 7.38/1.56 fof(f585,plain,(
% 7.38/1.56 sQ59_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f584])).
% 7.38/1.56 fof(f586,plain,(
% 7.38/1.56 $false|sQ13_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f187,f60])).
% 7.38/1.56 fof(f587,plain,(
% 7.38/1.56 sQ13_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f586])).
% 7.38/1.56 fof(f653,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6]: (~organization(X0,sK12_skl)|~organization(sK13_skl,sK6_skl)|~organization(X0,sK6_skl)|~class(X0,sK16_skl,sK12_skl)|~survival_chance(X0,sK15_skl,sK12_skl)|~reorganization(X0,sK12_skl,X1)|~reorganization_type(sK13_skl,X2,sK12_skl)|~reorganization_type(X0,X2,sK12_skl)|~survival_chance(sK13_skl,X3,sK6_skl)|~survival_chance(X0,X4,sK6_skl)|~complexity(sK13_skl,X5,sK12_skl)|~complexity(X0,X6,sK12_skl)|~greater(X6,X5)|greater(X3,X4)|X3=X4|~sQ7_spl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f239,f129])).
% 7.38/1.56 fof(f654,definition,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6]: (sQ77_spl <=> (~organization(X0,sK12_skl)|~organization(X0,sK6_skl)|~class(X0,sK16_skl,sK12_skl)|~survival_chance(X0,sK15_skl,sK12_skl)|~reorganization(X0,sK12_skl,X1)|~reorganization_type(sK13_skl,X2,sK12_skl)|~reorganization_type(X0,X2,sK12_skl)|~survival_chance(sK13_skl,X3,sK6_skl)|~survival_chance(X0,X4,sK6_skl)|~complexity(sK13_skl,X5,sK12_skl)|~complexity(X0,X6,sK12_skl)|~greater(X6,X5)|greater(X3,X4)|X3=X4))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f655,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4,X5,X6]: (~organization(X0,sK12_skl)|~organization(X0,sK6_skl)|~class(X0,sK16_skl,sK12_skl)|~survival_chance(X0,sK15_skl,sK12_skl)|~reorganization(X0,sK12_skl,X1)|~reorganization_type(sK13_skl,X2,sK12_skl)|~reorganization_type(X0,X2,sK12_skl)|~survival_chance(sK13_skl,X3,sK6_skl)|~survival_chance(X0,X4,sK6_skl)|~complexity(sK13_skl,X5,sK12_skl)|~complexity(X0,X6,sK12_skl)|~greater(X6,X5)|greater(X3,X4)|X3=X4|~sQ77_spl)),
% 7.38/1.56 inference(component_clause,[status(thm)],[f654])).
% 7.38/1.56 fof(f657,plain,(
% 7.38/1.56 sQ77_spl|~sQ8_spl|~sQ7_spl),
% 7.38/1.56 inference(split_clause,[status(thm)],[f653,f654,f149,f124])).
% 7.38/1.56 fof(f1718,plain,(
% 7.38/1.56 ~reorganization_type(sK11_skl,sK14_skl,sK12_skl)|~sQ60_spl),
% 7.38/1.56 inference(resolution,[status(thm)],[f565,f67])).
% 7.38/1.56 fof(f1719,plain,(
% 7.38/1.56 $false|~sQ60_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f1718,f68])).
% 7.38/1.56 fof(f1720,plain,(
% 7.38/1.56 ~sQ60_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f1719])).
% 7.38/1.56 fof(f2210,plain,(
% 7.38/1.56 ![X0]: (~complexity(sK11_skl,X0,sK12_skl)|~greater(X0,sK9_skl)|~sQ61_spl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f568,f72])).
% 7.38/1.56 fof(f2214,plain,(
% 7.38/1.56 ~greater(sK10_skl,sK9_skl)|~sQ61_spl),
% 7.38/1.56 inference(resolution,[status(thm)],[f2210,f73])).
% 7.38/1.56 fof(f2215,plain,(
% 7.38/1.56 $false|~sQ61_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f2214,f74])).
% 7.38/1.56 fof(f2216,plain,(
% 7.38/1.56 ~sQ61_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f2215])).
% 7.38/1.56 fof(f2219,plain,(
% 7.38/1.56 ![X0,X1,X2,X3,X4]: (~organization(sK11_skl,sK12_skl)|~organization(sK11_skl,sK6_skl)|~class(sK11_skl,sK16_skl,sK12_skl)|~survival_chance(sK11_skl,sK15_skl,sK12_skl)|~reorganization_type(sK13_skl,X0,sK12_skl)|~reorganization_type(sK11_skl,X0,sK12_skl)|~survival_chance(sK13_skl,X1,sK6_skl)|~survival_chance(sK11_skl,X2,sK6_skl)|~complexity(sK13_skl,X3,sK12_skl)|~complexity(sK11_skl,X4,sK12_skl)|~greater(X4,X3)|greater(X1,X2)|X1=X2|~sQ77_spl)),
% 7.38/1.56 inference(resolution,[status(thm)],[f655,f66])).
% 7.38/1.56 fof(f2220,definition,(
% 7.38/1.56 sQ203_spl <=> (survival_chance(sK13_skl,sK15_skl,sK12_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f2222,plain,(
% 7.38/1.56 ~survival_chance(sK13_skl,sK15_skl,sK12_skl)|sQ203_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f2220])).
% 7.38/1.56 fof(f2227,definition,(
% 7.38/1.56 sQ205_spl <=> (survival_chance(sK11_skl,sK15_skl,sK12_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f2229,plain,(
% 7.38/1.56 ~survival_chance(sK11_skl,sK15_skl,sK12_skl)|sQ205_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f2227])).
% 7.38/1.56 fof(f2230,definition,(
% 7.38/1.56 ![X1,X2]: (sQ206_spl <=> (~survival_chance(sK13_skl,X1,sK6_skl)|~survival_chance(sK11_skl,X2,sK6_skl)|greater(X1,X2)|X1=X2))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f2231,plain,(
% 7.38/1.56 ![X0,X1]: (~survival_chance(sK13_skl,X0,sK6_skl)|~survival_chance(sK11_skl,X1,sK6_skl)|greater(X0,X1)|X0=X1|~sQ206_spl)),
% 7.38/1.56 inference(component_clause,[status(thm)],[f2230])).
% 7.38/1.56 fof(f2233,plain,(
% 7.38/1.56 ~sQ2_spl|~sQ14_spl|~sQ59_spl|~sQ205_spl|sQ60_spl|sQ206_spl|sQ61_spl|~sQ77_spl),
% 7.38/1.56 inference(split_clause,[status(thm)],[f2219,f100,f189,f561,f2227,f564,f2230,f567,f654])).
% 7.38/1.56 fof(f2234,plain,(
% 7.38/1.56 $false|sQ205_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f2229,f64])).
% 7.38/1.56 fof(f2235,plain,(
% 7.38/1.56 sQ205_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f2234])).
% 7.38/1.56 fof(f2236,plain,(
% 7.38/1.56 $false|sQ203_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f2222,f63])).
% 7.38/1.56 fof(f2237,plain,(
% 7.38/1.56 sQ203_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f2236])).
% 7.38/1.56 fof(f2359,definition,(
% 7.38/1.56 sQ212_spl <=> (greater(sK0_skl(sK6_skl,sK13_skl),sK0_skl(sK6_skl,sK13_skl)))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f2360,plain,(
% 7.38/1.56 greater(sK0_skl(sK6_skl,sK13_skl),sK0_skl(sK6_skl,sK13_skl))|~sQ212_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f2359])).
% 7.38/1.56 fof(f2366,plain,(
% 7.38/1.56 $false|~sQ212_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f2360,f86])).
% 7.38/1.56 fof(f2367,plain,(
% 7.38/1.56 ~sQ212_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f2366])).
% 7.38/1.56 fof(f2980,definition,(
% 7.38/1.56 sQ259_spl <=> (survival_chance(sK11_skl,sK0_skl(sK8_skl,sK11_skl),sK8_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 7.38/1.56 fof(f2982,plain,(
% 7.38/1.56 ~survival_chance(sK11_skl,sK0_skl(sK8_skl,sK11_skl),sK8_skl)|sQ259_spl),
% 7.38/1.56 inference(component_clause,[status(thm)],[f2980])).
% 7.38/1.56 fof(f2991,plain,(
% 7.38/1.56 $false|sQ259_spl),
% 7.38/1.56 inference(forward_subsumption_resolution,[status(thm)],[f2982,f94])).
% 7.38/1.56 fof(f2992,plain,(
% 7.38/1.56 sQ259_spl),
% 7.38/1.56 inference(contradiction_clause,[status(thm)],[f2991])).
% 7.38/1.56 fof(f3106,definition,(
% 7.38/1.56 sQ270_spl <=> (survival_chance(sK13_skl,sK4_skl,sK6_skl))),
% 7.38/1.56 introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 7.29/1.58 fof(f3108,plain,(
% 7.29/1.58 ~survival_chance(sK13_skl,sK4_skl,sK6_skl)|sQ270_spl),
% 7.29/1.58 inference(component_clause,[status(thm)],[f3106])).
% 7.29/1.58 fof(f3110,plain,(
% 7.29/1.58 $false|sQ270_spl),
% 7.29/1.58 inference(forward_subsumption_resolution,[status(thm)],[f3108,f70])).
% 7.29/1.58 fof(f3111,plain,(
% 7.29/1.58 sQ270_spl),
% 7.29/1.58 inference(contradiction_clause,[status(thm)],[f3110])).
% 7.29/1.58 fof(f3216,plain,(
% 7.29/1.58 ![X0]: (~survival_chance(sK11_skl,X0,sK6_skl)|greater(sK4_skl,X0)|sK4_skl=X0|~sQ206_spl)),
% 7.29/1.58 inference(resolution,[status(thm)],[f2231,f70])).
% 7.29/1.58 fof(f3228,plain,(
% 7.29/1.58 greater(sK4_skl,sK5_skl)|sK4_skl=sK5_skl|~sQ206_spl),
% 7.29/1.58 inference(resolution,[status(thm)],[f3216,f71])).
% 7.29/1.58 fof(f3230,plain,(
% 7.29/1.58 sQ1_spl|sQ34_spl|~sQ206_spl),
% 7.29/1.58 inference(split_clause,[status(thm)],[f3228,f82,f327,f2230])).
% 7.29/1.58 fof(f3232,plain,(
% 7.29/1.58 $false),
% 7.29/1.58 inference(sat_refutation,[status(thm)],[f113,f115,f117,f127,f192,f196,f342,f346,f570,f585,f587,f657,f1720,f2216,f2233,f2235,f2237,f2367,f2992,f3111,f3230])).
% 7.29/1.58 % SZS output end CNFRefutation for theBenchmark.p
% 7.29/1.59 % Elapsed time: 1.103826 seconds
% 7.29/1.59 % CPU time: 8.475505 seconds
% 7.29/1.59 % Total memory used: 139.598 MB
% 7.29/1.59 % Net memory used: 132.345 MB
%------------------------------------------------------------------------------