%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT055+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Thu Sep 24 01:25:51 PM UTC 2026
% Result : Theorem 12.29s 1.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT055+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 01:23:52 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 12.29/1.91 % Refutation found
% 12.29/1.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.29/1.91 % SZS output start CNFRefutation for theBenchmark
% 12.29/1.91 fof(f1,axiom,(
% 12.29/1.91 (! [X,Y] :( smaller_or_equal(X,Y)<=> ( smaller(X,Y)| X = Y ) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f2,axiom,(
% 12.29/1.91 (! [X,Y] :( greater_or_equal(X,Y)<=> ( greater(X,Y)| X = Y ) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f3,axiom,(
% 12.29/1.91 (! [X,Y] :( smaller(X,Y)<=> greater(Y,X) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f4,axiom,(
% 12.29/1.91 (! [X,Y] :~ ( greater(X,Y)& greater(Y,X) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f5,axiom,(
% 12.29/1.91 (! [X,Y,Z] :( ( greater(X,Y)& greater(Y,Z) )=> greater(X,Z) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f6,axiom,(
% 12.29/1.91 (! [X,Y] :( smaller(X,Y)| X = Y| greater(X,Y) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f7,axiom,(
% 12.29/1.91 (! [X] :( has_endowment(X)<=> (! [T] :( organization(X)& ( smaller_or_equal(age(X,T),eta)=> has_immunity(X,T) )& ( greater(age(X,T),eta)=> ~ has_immunity(X,T) ) ) )) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f8,axiom,(
% 12.29/1.91 (! [X,T0,T] :( ( organization(X)& has_immunity(X,T0)& has_immunity(X,T) )=> hazard_of_mortality(X,T0) = hazard_of_mortality(X,T) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f9,axiom,(
% 12.29/1.91 (! [X,T0,T] :( ( organization(X)& has_immunity(X,T0)& ~ has_immunity(X,T) )=> greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f10,axiom,(
% 12.29/1.91 (! [X,T0,T] :( dissimilar(X,T0,T)<=> ( organization(X)& ~ ( is_aligned(X,T0)<=> is_aligned(X,T) ) ) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f11,axiom,(
% 12.29/1.91 (! [X,T] :( ( organization(X)& age(X,T) = zero )=> is_aligned(X,T) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f12,axiom,(
% 12.29/1.91 (! [X,T0,T] :( ( organization(X)& is_aligned(X,T0)& ~ is_aligned(X,T) )=> greater(capability(X,T0),capability(X,T)) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f13,axiom,(
% 12.29/1.91 (! [X,T0,T] :( ( organization(X)& age(X,T0) = zero )=> ( greater(age(X,T),sigma)<=> dissimilar(X,T0,T) ) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f14,axiom,(
% 12.29/1.91 (! [X,T0,T] :( ( organization(X)& ~ has_immunity(X,T0)& ~ has_immunity(X,T)& greater(capability(X,T),capability(X,T0)) )=> greater(hazard_of_mortality(X,T0),hazard_of_mortality(X,T)) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f15,conjecture,(
% 12.29/1.91 (! [X,T0,T1,T2,T3] :( ( organization(X)& has_endowment(X)& age(X,T0) = zero& smaller_or_equal(age(X,T1),eta)& greater(age(X,T2),eta)& smaller_or_equal(age(X,T2),sigma)& greater(age(X,T3),sigma)& greater(sigma,eta)& greater(eta,zero) )=> ( greater(hazard_of_mortality(X,T3),hazard_of_mortality(X,T2))& greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) )),
% 12.29/1.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.29/1.91 fof(f16,negated_conjecture,(
% 12.29/1.91 ~((! [X,T0,T1,T2,T3] :( ( organization(X)& has_endowment(X)& age(X,T0) = zero& smaller_or_equal(age(X,T1),eta)& greater(age(X,T2),eta)& smaller_or_equal(age(X,T2),sigma)& greater(age(X,T3),sigma)& greater(sigma,eta)& greater(eta,zero) )=> ( greater(hazard_of_mortality(X,T3),hazard_of_mortality(X,T2))& greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ))),
% 12.29/1.91 inference(negated_conjecture,[status(cth)],[f15])).
% 12.29/1.91 fof(f17,plain,(
% 12.29/1.91 ![X,Y]: ((~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y))&(smaller_or_equal(X,Y)|(~smaller(X,Y)&~X=Y)))),
% 12.29/1.91 inference(NNF_transformation,[status(thm)],[f1])).
% 12.29/1.91 fof(f18,plain,(
% 12.29/1.91 (![X,Y]: (~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y)))&(![X,Y]: (smaller_or_equal(X,Y)|(~smaller(X,Y)&~X=Y)))),
% 12.29/1.91 inference(miniscoping,[status(thm)],[f17])).
% 12.29/1.91 fof(f19,plain,(
% 12.29/1.91 ![X0,X1]: (~smaller_or_equal(X0,X1)|smaller(X0,X1)|X0=X1)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f18])).
% 12.29/1.91 fof(f20,plain,(
% 12.29/1.91 ![X0,X1]: (smaller_or_equal(X0,X1)|~smaller(X0,X1))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f18])).
% 12.29/1.91 fof(f21,plain,(
% 12.29/1.91 ![X0,X1]: (smaller_or_equal(X0,X1)|~X0=X1)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f18])).
% 12.29/1.91 fof(f22,plain,(
% 12.29/1.91 ![X,Y]: ((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&(greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 12.29/1.91 inference(NNF_transformation,[status(thm)],[f2])).
% 12.29/1.91 fof(f23,plain,(
% 12.29/1.91 (![X,Y]: (~greater_or_equal(X,Y)|(greater(X,Y)|X=Y)))&(![X,Y]: (greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 12.29/1.91 inference(miniscoping,[status(thm)],[f22])).
% 12.29/1.91 fof(f24,plain,(
% 12.29/1.91 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f23])).
% 12.29/1.91 fof(f25,plain,(
% 12.29/1.91 ![X0,X1]: (greater_or_equal(X0,X1)|~greater(X0,X1))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f23])).
% 12.29/1.91 fof(f27,plain,(
% 12.29/1.91 ![X,Y]: ((~smaller(X,Y)|greater(Y,X))&(smaller(X,Y)|~greater(Y,X)))),
% 12.29/1.91 inference(NNF_transformation,[status(thm)],[f3])).
% 12.29/1.91 fof(f28,plain,(
% 12.29/1.91 (![X,Y]: (~smaller(X,Y)|greater(Y,X)))&(![X,Y]: (smaller(X,Y)|~greater(Y,X)))),
% 12.29/1.91 inference(miniscoping,[status(thm)],[f27])).
% 12.29/1.91 fof(f29,plain,(
% 12.29/1.91 ![X0,X1]: (~smaller(X0,X1)|greater(X1,X0))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f28])).
% 12.29/1.91 fof(f30,plain,(
% 12.29/1.91 ![X0,X1]: (smaller(X0,X1)|~greater(X1,X0))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f28])).
% 12.29/1.91 fof(f31,plain,(
% 12.29/1.91 ![X,Y]: (~greater(X,Y)|~greater(Y,X))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 12.29/1.91 fof(f32,plain,(
% 12.29/1.91 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f31])).
% 12.29/1.91 fof(f33,plain,(
% 12.29/1.91 ![X,Y,Z]: ((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 12.29/1.91 fof(f34,plain,(
% 12.29/1.91 ![X,Z]: ((![Y]: (~greater(X,Y)|~greater(Y,Z)))|greater(X,Z))),
% 12.29/1.91 inference(miniscoping,[status(thm)],[f33])).
% 12.29/1.91 fof(f35,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f34])).
% 12.29/1.91 fof(f36,plain,(
% 12.29/1.91 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater(X0,X1))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f6])).
% 12.29/1.91 fof(f37,plain,(
% 12.29/1.91 ![X]: (has_endowment(X)<=>(![T]: ((organization(X)&(~smaller_or_equal(age(X,T),eta)|has_immunity(X,T)))&(~greater(age(X,T),eta)|~has_immunity(X,T)))))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 12.29/1.91 fof(f38,plain,(
% 12.29/1.91 ![X]: ((~has_endowment(X)|(![T]: ((organization(X)&(~smaller_or_equal(age(X,T),eta)|has_immunity(X,T)))&(~greater(age(X,T),eta)|~has_immunity(X,T)))))&(has_endowment(X)|(?[T]: ((~organization(X)|(smaller_or_equal(age(X,T),eta)&~has_immunity(X,T)))|(greater(age(X,T),eta)&has_immunity(X,T))))))),
% 12.29/1.91 inference(NNF_transformation,[status(thm)],[f37])).
% 12.29/1.91 fof(f39,plain,(
% 12.29/1.91 (![X]: (~has_endowment(X)|((organization(X)&(![T]: (~smaller_or_equal(age(X,T),eta)|has_immunity(X,T))))&(![T]: (~greater(age(X,T),eta)|~has_immunity(X,T))))))&(![X]: (has_endowment(X)|((~organization(X)|(?[T]: (smaller_or_equal(age(X,T),eta)&~has_immunity(X,T))))|(?[T]: (greater(age(X,T),eta)&has_immunity(X,T))))))),
% 12.29/1.91 inference(miniscoping,[status(thm)],[f38])).
% 12.29/1.91 fof(f40,plain,(
% 12.29/1.91 (![X]: (~has_endowment(X)|((organization(X)&(![T]: (~smaller_or_equal(age(X,T),eta)|has_immunity(X,T))))&(![T]: (~greater(age(X,T),eta)|~has_immunity(X,T))))))&(![X]: (has_endowment(X)|((~organization(X)|(smaller_or_equal(age(X,sK0_skl(X)),eta)&~has_immunity(X,sK0_skl(X))))|(greater(age(X,sK1_skl(X)),eta)&has_immunity(X,sK1_skl(X))))))),
% 12.29/1.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(T,sK0_skl(X)),skolemize(T,sK1_skl(X))],[f39])).
% 12.29/1.91 fof(f42,plain,(
% 12.29/1.91 ![X0,X1]: (~has_endowment(X0)|~smaller_or_equal(age(X0,X1),eta)|has_immunity(X0,X1))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f40])).
% 12.29/1.91 fof(f43,plain,(
% 12.29/1.91 ![X0,X1]: (~has_endowment(X0)|~greater(age(X0,X1),eta)|~has_immunity(X0,X1))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f40])).
% 12.29/1.91 fof(f48,plain,(
% 12.29/1.91 ![X,T0,T]: (((~organization(X)|~has_immunity(X,T0))|~has_immunity(X,T))|hazard_of_mortality(X,T0)=hazard_of_mortality(X,T))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 12.29/1.91 fof(f49,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|~has_immunity(X0,X1)|~has_immunity(X0,X2)|hazard_of_mortality(X0,X1)=hazard_of_mortality(X0,X2))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f48])).
% 12.29/1.91 fof(f50,plain,(
% 12.29/1.91 ![X,T0,T]: (((~organization(X)|~has_immunity(X,T0))|has_immunity(X,T))|greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 12.29/1.91 fof(f51,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|~has_immunity(X0,X1)|has_immunity(X0,X2)|greater(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1)))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f50])).
% 12.29/1.91 fof(f52,plain,(
% 12.29/1.91 ![X,T0,T]: (dissimilar(X,T0,T)<=>(organization(X)&(is_aligned(X,T0)<~>is_aligned(X,T))))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 12.29/1.91 fof(f53,plain,(
% 12.29/1.91 ![X,T0,T]: ((~dissimilar(X,T0,T)|(organization(X)&((is_aligned(X,T0)|is_aligned(X,T))&(~is_aligned(X,T0)|~is_aligned(X,T)))))&(dissimilar(X,T0,T)|(~organization(X)|((~is_aligned(X,T0)|is_aligned(X,T))&(is_aligned(X,T0)|~is_aligned(X,T))))))),
% 12.29/1.91 inference(NNF_transformation,[status(thm)],[f52])).
% 12.29/1.91 fof(f54,plain,(
% 12.29/1.91 (![X,T0,T]: (~dissimilar(X,T0,T)|(organization(X)&((is_aligned(X,T0)|is_aligned(X,T))&(~is_aligned(X,T0)|~is_aligned(X,T))))))&(![X,T0,T]: (dissimilar(X,T0,T)|(~organization(X)|((~is_aligned(X,T0)|is_aligned(X,T))&(is_aligned(X,T0)|~is_aligned(X,T))))))),
% 12.29/1.91 inference(miniscoping,[status(thm)],[f53])).
% 12.29/1.91 fof(f55,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|organization(X0))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f54])).
% 12.29/1.91 fof(f56,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|is_aligned(X0,X1)|is_aligned(X0,X2))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f54])).
% 12.29/1.91 fof(f57,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f54])).
% 12.29/1.91 fof(f58,plain,(
% 12.29/1.91 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f54])).
% 12.29/1.91 fof(f59,plain,(
% 12.29/1.91 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f54])).
% 12.29/1.91 fof(f60,plain,(
% 12.29/1.91 ![X,T]: ((~organization(X)|~age(X,T)=zero)|is_aligned(X,T))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 12.29/1.91 fof(f61,plain,(
% 12.29/1.91 ![X0,X1]: (~organization(X0)|~age(X0,X1)=zero|is_aligned(X0,X1))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f60])).
% 12.29/1.91 fof(f62,plain,(
% 12.29/1.91 ![X,T0,T]: (((~organization(X)|~is_aligned(X,T0))|is_aligned(X,T))|greater(capability(X,T0),capability(X,T)))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 12.29/1.91 fof(f63,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2)|greater(capability(X0,X1),capability(X0,X2)))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f62])).
% 12.29/1.91 fof(f64,plain,(
% 12.29/1.91 ![X,T0,T]: ((~organization(X)|~age(X,T0)=zero)|(greater(age(X,T),sigma)<=>dissimilar(X,T0,T)))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 12.29/1.91 fof(f65,plain,(
% 12.29/1.91 ![X,T0,T]: ((~organization(X)|~age(X,T0)=zero)|((~greater(age(X,T),sigma)|dissimilar(X,T0,T))&(greater(age(X,T),sigma)|~dissimilar(X,T0,T))))),
% 12.29/1.91 inference(NNF_transformation,[status(thm)],[f64])).
% 12.29/1.91 fof(f66,plain,(
% 12.29/1.91 ![X,T0]: ((~organization(X)|~age(X,T0)=zero)|((![T]: (~greater(age(X,T),sigma)|dissimilar(X,T0,T)))&(![T]: (greater(age(X,T),sigma)|~dissimilar(X,T0,T)))))),
% 12.29/1.91 inference(miniscoping,[status(thm)],[f65])).
% 12.29/1.91 fof(f67,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~greater(age(X0,X2),sigma)|dissimilar(X0,X1,X2))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f66])).
% 12.29/1.91 fof(f68,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|greater(age(X0,X2),sigma)|~dissimilar(X0,X1,X2))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f66])).
% 12.29/1.91 fof(f69,plain,(
% 12.29/1.91 ![X,T0,T]: ((((~organization(X)|has_immunity(X,T0))|has_immunity(X,T))|~greater(capability(X,T),capability(X,T0)))|greater(hazard_of_mortality(X,T0),hazard_of_mortality(X,T)))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 12.29/1.91 fof(f70,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|has_immunity(X0,X1)|has_immunity(X0,X2)|~greater(capability(X0,X2),capability(X0,X1))|greater(hazard_of_mortality(X0,X1),hazard_of_mortality(X0,X2)))),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f69])).
% 12.29/1.91 fof(f71,plain,(
% 12.29/1.91 (?[X,T0,T1,T2,T3]: (((((((((organization(X)&has_endowment(X))&age(X,T0)=zero)&smaller_or_equal(age(X,T1),eta))&greater(age(X,T2),eta))&smaller_or_equal(age(X,T2),sigma))&greater(age(X,T3),sigma))&greater(sigma,eta))&greater(eta,zero))&((~greater(hazard_of_mortality(X,T3),hazard_of_mortality(X,T2))|~greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)))|~hazard_of_mortality(X,T1)=hazard_of_mortality(X,T0))))),
% 12.29/1.91 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 12.29/1.91 fof(f72,plain,(
% 12.29/1.91 (((((((((organization(sK2_skl)&has_endowment(sK2_skl))&age(sK2_skl,sK3_skl)=zero)&smaller_or_equal(age(sK2_skl,sK4_skl),eta))&greater(age(sK2_skl,sK5_skl),eta))&smaller_or_equal(age(sK2_skl,sK5_skl),sigma))&greater(age(sK2_skl,sK6_skl),sigma))&greater(sigma,eta))&greater(eta,zero))&((~greater(hazard_of_mortality(sK2_skl,sK6_skl),hazard_of_mortality(sK2_skl,sK5_skl))|~greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)))|~hazard_of_mortality(sK2_skl,sK4_skl)=hazard_of_mortality(sK2_skl,sK3_skl)))),
% 12.29/1.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(X,sK2_skl),skolemize(T0,sK3_skl),skolemize(T1,sK4_skl),skolemize(T2,sK5_skl),skolemize(T3,sK6_skl)],[f71])).
% 12.29/1.91 fof(f73,plain,(
% 12.29/1.91 organization(sK2_skl)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f74,plain,(
% 12.29/1.91 has_endowment(sK2_skl)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f75,plain,(
% 12.29/1.91 age(sK2_skl,sK3_skl)=zero),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f76,plain,(
% 12.29/1.91 smaller_or_equal(age(sK2_skl,sK4_skl),eta)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f77,plain,(
% 12.29/1.91 greater(age(sK2_skl,sK5_skl),eta)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f78,plain,(
% 12.29/1.91 smaller_or_equal(age(sK2_skl,sK5_skl),sigma)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f79,plain,(
% 12.29/1.91 greater(age(sK2_skl,sK6_skl),sigma)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f80,plain,(
% 12.29/1.91 greater(sigma,eta)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f81,plain,(
% 12.29/1.91 greater(eta,zero)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f82,plain,(
% 12.29/1.91 ~greater(hazard_of_mortality(sK2_skl,sK6_skl),hazard_of_mortality(sK2_skl,sK5_skl))|~greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl))|~hazard_of_mortality(sK2_skl,sK4_skl)=hazard_of_mortality(sK2_skl,sK3_skl)),
% 12.29/1.91 inference(cnf_transformation,[status(thm)],[f72])).
% 12.29/1.91 fof(f83,definition,(
% 12.29/1.91 sQ0_spl <=> (greater(hazard_of_mortality(sK2_skl,sK6_skl),hazard_of_mortality(sK2_skl,sK5_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f85,plain,(
% 12.29/1.91 ~greater(hazard_of_mortality(sK2_skl,sK6_skl),hazard_of_mortality(sK2_skl,sK5_skl))|sQ0_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f83])).
% 12.29/1.91 fof(f86,definition,(
% 12.29/1.91 sQ1_spl <=> (greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f87,plain,(
% 12.29/1.91 greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl))|~sQ1_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f86])).
% 12.29/1.91 fof(f88,plain,(
% 12.29/1.91 ~greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl))|sQ1_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f86])).
% 12.29/1.91 fof(f89,definition,(
% 12.29/1.91 sQ2_spl <=> (hazard_of_mortality(sK2_skl,sK4_skl)=hazard_of_mortality(sK2_skl,sK3_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f91,plain,(
% 12.29/1.91 ~hazard_of_mortality(sK2_skl,sK4_skl)=hazard_of_mortality(sK2_skl,sK3_skl)|sQ2_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f89])).
% 12.29/1.91 fof(f92,plain,(
% 12.29/1.91 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f82,f83,f86,f89])).
% 12.29/1.91 fof(f93,plain,(
% 12.29/1.91 ![X0]: (smaller_or_equal(X0,X0))),
% 12.29/1.91 inference(destructive_equality_resolution,[status(thm)],[f21])).
% 12.29/1.91 fof(f95,plain,(
% 12.29/1.91 ~greater(zero,eta)),
% 12.29/1.91 inference(resolution,[status(thm)],[f32,f81])).
% 12.29/1.91 fof(f96,plain,(
% 12.29/1.91 ~greater(eta,sigma)),
% 12.29/1.91 inference(resolution,[status(thm)],[f32,f80])).
% 12.29/1.91 fof(f97,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|~greater(X2,X0))),
% 12.29/1.91 inference(resolution,[status(thm)],[f35,f32])).
% 12.29/1.91 fof(f98,plain,(
% 12.29/1.91 ![X0]: (~greater(zero,X0)|~greater(X0,eta))),
% 12.29/1.91 inference(resolution,[status(thm)],[f95,f35])).
% 12.29/1.91 fof(f99,plain,(
% 12.29/1.91 ![X0]: (~greater(eta,X0)|~greater(X0,sigma))),
% 12.29/1.91 inference(resolution,[status(thm)],[f96,f35])).
% 12.29/1.91 fof(f100,plain,(
% 12.29/1.91 greater_or_equal(eta,zero)),
% 12.29/1.91 inference(resolution,[status(thm)],[f25,f81])).
% 12.29/1.91 fof(f101,plain,(
% 12.29/1.91 greater_or_equal(sigma,eta)),
% 12.29/1.91 inference(resolution,[status(thm)],[f25,f80])).
% 12.29/1.91 fof(f105,plain,(
% 12.29/1.91 smaller(zero,eta)),
% 12.29/1.91 inference(resolution,[status(thm)],[f30,f81])).
% 12.29/1.91 fof(f108,plain,(
% 12.29/1.91 greater(eta,zero)|eta=zero),
% 12.29/1.91 inference(resolution,[status(thm)],[f100,f24])).
% 12.29/1.91 fof(f109,definition,(
% 12.29/1.91 sQ3_spl <=> (greater(eta,zero))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f112,definition,(
% 12.29/1.91 sQ4_spl <=> (eta=zero)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f113,plain,(
% 12.29/1.91 eta=zero|~sQ4_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f112])).
% 12.29/1.91 fof(f115,plain,(
% 12.29/1.91 sQ3_spl|sQ4_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f108,f109,f112])).
% 12.29/1.91 fof(f128,plain,(
% 12.29/1.91 ![X0]: (~smaller_or_equal(age(sK2_skl,X0),eta)|has_immunity(sK2_skl,X0))),
% 12.29/1.91 inference(resolution,[status(thm)],[f42,f74])).
% 12.29/1.91 fof(f132,plain,(
% 12.29/1.91 ~greater(eta,eta)|~sQ4_spl),
% 12.29/1.91 inference(backward_demodulation,[status(thm)],[f113,f95])).
% 12.29/1.91 fof(f133,plain,(
% 12.29/1.91 greater(eta,eta)|~sQ4_spl),
% 12.29/1.91 inference(backward_demodulation,[status(thm)],[f113,f81])).
% 12.29/1.91 fof(f136,plain,(
% 12.29/1.91 $false|~sQ4_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f133,f132])).
% 12.29/1.91 fof(f137,plain,(
% 12.29/1.91 ~sQ4_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f136])).
% 12.29/1.91 fof(f139,plain,(
% 12.29/1.91 smaller(zero,eta)|zero=eta),
% 12.29/1.91 inference(resolution,[status(thm)],[f36,f95])).
% 12.29/1.91 fof(f140,plain,(
% 12.29/1.91 smaller(eta,sigma)|eta=sigma),
% 12.29/1.91 inference(resolution,[status(thm)],[f36,f96])).
% 12.29/1.91 fof(f141,plain,(
% 12.29/1.91 ![X0,X1]: (smaller(X0,X1)|X0=X1|smaller(X1,X0))),
% 12.29/1.91 inference(resolution,[status(thm)],[f36,f30])).
% 12.29/1.91 fof(f144,definition,(
% 12.29/1.91 sQ7_spl <=> (smaller(zero,eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f147,plain,(
% 12.29/1.91 sQ7_spl|sQ4_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f139,f144,f112])).
% 12.29/1.91 fof(f148,definition,(
% 12.29/1.91 sQ8_spl <=> (smaller(eta,sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f151,definition,(
% 12.29/1.91 sQ9_spl <=> (eta=sigma)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f152,plain,(
% 12.29/1.91 eta=sigma|~sQ9_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f151])).
% 12.29/1.91 fof(f154,plain,(
% 12.29/1.91 sQ8_spl|sQ9_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f140,f148,f151])).
% 12.29/1.91 fof(f157,definition,(
% 12.29/1.91 sQ10_spl <=> (has_endowment(sK2_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f159,plain,(
% 12.29/1.91 ~has_endowment(sK2_skl)|sQ10_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f157])).
% 12.29/1.91 fof(f172,plain,(
% 12.29/1.91 greater_or_equal(age(sK2_skl,sK5_skl),eta)),
% 12.29/1.91 inference(resolution,[status(thm)],[f77,f25])).
% 12.29/1.91 fof(f173,plain,(
% 12.29/1.91 ~greater(eta,age(sK2_skl,sK5_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f77,f32])).
% 12.29/1.91 fof(f177,plain,(
% 12.29/1.91 greater(eta,eta)|~sQ9_spl),
% 12.29/1.91 inference(backward_demodulation,[status(thm)],[f152,f80])).
% 12.29/1.91 fof(f180,definition,(
% 12.29/1.91 sQ13_spl <=> (smaller(eta,eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f181,plain,(
% 12.29/1.91 smaller(eta,eta)|~sQ13_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f180])).
% 12.29/1.91 fof(f182,plain,(
% 12.29/1.91 ~smaller(eta,eta)|sQ13_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f180])).
% 12.29/1.91 fof(f183,definition,(
% 12.29/1.91 sQ14_spl <=> (eta=eta)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f188,plain,(
% 12.29/1.91 ![X0]: (~greater(eta,X0)|~greater(X0,sigma))),
% 12.29/1.91 inference(resolution,[status(thm)],[f96,f35])).
% 12.29/1.91 fof(f194,plain,(
% 12.29/1.91 greater(sigma,eta)|sigma=eta),
% 12.29/1.91 inference(resolution,[status(thm)],[f101,f24])).
% 12.29/1.91 fof(f195,definition,(
% 12.29/1.91 sQ15_spl <=> (greater(sigma,eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f198,plain,(
% 12.29/1.91 sQ15_spl|sQ9_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f194,f195,f151])).
% 12.29/1.91 fof(f200,plain,(
% 12.29/1.91 smaller_or_equal(zero,eta)),
% 12.29/1.91 inference(resolution,[status(thm)],[f105,f20])).
% 12.29/1.91 fof(f208,plain,(
% 12.29/1.91 smaller(age(sK2_skl,sK5_skl),sigma)|age(sK2_skl,sK5_skl)=sigma),
% 12.29/1.91 inference(resolution,[status(thm)],[f78,f19])).
% 12.29/1.91 fof(f209,definition,(
% 12.29/1.91 sQ16_spl <=> (smaller(age(sK2_skl,sK5_skl),sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f210,plain,(
% 12.29/1.91 smaller(age(sK2_skl,sK5_skl),sigma)|~sQ16_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f209])).
% 12.29/1.91 fof(f212,definition,(
% 12.29/1.91 sQ17_spl <=> (age(sK2_skl,sK5_skl)=sigma)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f213,plain,(
% 12.29/1.91 age(sK2_skl,sK5_skl)=sigma|~sQ17_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f212])).
% 12.29/1.91 fof(f215,plain,(
% 12.29/1.91 sQ16_spl|sQ17_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f208,f209,f212])).
% 12.29/1.91 fof(f220,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~age(X0,X1)=zero|greater(age(X0,X2),sigma)|~dissimilar(X0,X1,X2))),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f68,f55])).
% 12.29/1.91 fof(f223,plain,(
% 12.29/1.91 greater_or_equal(age(sK2_skl,sK6_skl),sigma)),
% 12.29/1.91 inference(resolution,[status(thm)],[f79,f25])).
% 12.29/1.91 fof(f224,plain,(
% 12.29/1.91 ~greater(sigma,age(sK2_skl,sK6_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f79,f32])).
% 12.29/1.91 fof(f225,plain,(
% 12.29/1.91 greater(eta,eta)|~sQ13_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f181,f29])).
% 12.29/1.91 fof(f229,plain,(
% 12.29/1.91 ~greater(eta,eta)|~sQ13_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f225,f32])).
% 12.29/1.91 fof(f230,plain,(
% 12.29/1.91 $false|~sQ13_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f229,f225])).
% 12.29/1.91 fof(f231,plain,(
% 12.29/1.91 ~sQ13_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f230])).
% 12.29/1.91 fof(f232,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~organization(X0)|~age(X0,X2)=zero)),
% 12.29/1.91 inference(resolution,[status(thm)],[f57,f61])).
% 12.29/1.91 fof(f233,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~age(X0,X2)=zero)),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f232,f55])).
% 12.29/1.91 fof(f239,plain,(
% 12.29/1.91 ![X0]: (~greater(X0,eta)|smaller(zero,X0)|zero=X0)),
% 12.29/1.91 inference(resolution,[status(thm)],[f98,f36])).
% 12.29/1.91 fof(f244,plain,(
% 12.29/1.91 ~greater(zero,sigma)),
% 12.29/1.91 inference(resolution,[status(thm)],[f99,f81])).
% 12.29/1.91 fof(f245,plain,(
% 12.29/1.91 ![X0]: (~greater(X0,sigma)|smaller(eta,X0)|eta=X0)),
% 12.29/1.91 inference(resolution,[status(thm)],[f99,f36])).
% 12.29/1.91 fof(f248,plain,(
% 12.29/1.91 ![X0]: (~greater(zero,X0)|~greater(X0,sigma))),
% 12.29/1.91 inference(resolution,[status(thm)],[f244,f35])).
% 12.29/1.91 fof(f249,definition,(
% 12.29/1.91 sQ18_spl <=> (smaller(zero,sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f250,plain,(
% 12.29/1.91 smaller(zero,sigma)|~sQ18_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f249])).
% 12.29/1.91 fof(f252,definition,(
% 12.29/1.91 sQ19_spl <=> (zero=sigma)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f253,plain,(
% 12.29/1.91 zero=sigma|~sQ19_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f252])).
% 12.29/1.91 fof(f254,plain,(
% 12.29/1.91 ~zero=sigma|sQ19_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f252])).
% 12.29/1.91 fof(f265,plain,(
% 12.29/1.91 greater(zero,eta)|~sQ19_spl),
% 12.29/1.91 inference(backward_demodulation,[status(thm)],[f253,f80])).
% 12.29/1.91 fof(f267,plain,(
% 12.29/1.91 $false|~sQ19_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f265,f95])).
% 12.29/1.91 fof(f268,plain,(
% 12.29/1.91 ~sQ19_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f267])).
% 12.29/1.91 fof(f285,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|is_aligned(X0,X1)|greater(capability(X0,X2),capability(X0,X1))|~organization(X0)|~age(X0,X2)=zero)),
% 12.29/1.91 inference(resolution,[status(thm)],[f63,f61])).
% 12.29/1.91 fof(f286,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|is_aligned(X0,X1)|greater(capability(X0,X2),capability(X0,X1))|~age(X0,X2)=zero)),
% 12.29/1.91 inference(duplicate_literals_removal,[status(thm)],[f285])).
% 12.29/1.91 fof(f287,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|has_immunity(X0,X1)|~greater(capability(X0,X2),capability(X0,X1))|greater(hazard_of_mortality(X0,X1),hazard_of_mortality(X0,X2)))),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f70,f51])).
% 12.29/1.91 fof(f288,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~organization(X0)|has_immunity(X0,X1)|greater(hazard_of_mortality(X0,X1),hazard_of_mortality(X0,X2))|smaller(capability(X0,X2),capability(X0,X1))|capability(X0,X2)=capability(X0,X1))),
% 12.29/1.91 inference(resolution,[status(thm)],[f287,f36])).
% 12.29/1.91 fof(f290,plain,(
% 12.29/1.91 greater(sigma,zero)|~sQ18_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f250,f29])).
% 12.29/1.91 fof(f292,plain,(
% 12.29/1.91 has_immunity(sK2_skl,sK4_skl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f128,f76])).
% 12.29/1.91 fof(f295,plain,(
% 12.29/1.91 ~smaller_or_equal(zero,eta)|has_immunity(sK2_skl,sK3_skl)),
% 12.29/1.91 inference(paramodulation,[status(thm)],[f75,f128])).
% 12.29/1.91 fof(f299,definition,(
% 12.29/1.91 sQ21_spl <=> (organization(sK2_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f301,plain,(
% 12.29/1.91 ~organization(sK2_skl)|sQ21_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f299])).
% 12.29/1.91 fof(f309,definition,(
% 12.29/1.91 sQ24_spl <=> (has_immunity(sK2_skl,sK5_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f310,plain,(
% 12.29/1.91 has_immunity(sK2_skl,sK5_skl)|~sQ24_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f309])).
% 12.29/1.91 fof(f313,definition,(
% 12.29/1.91 sQ25_spl <=> (smaller_or_equal(zero,eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f315,plain,(
% 12.29/1.91 ~smaller_or_equal(zero,eta)|sQ25_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f313])).
% 12.29/1.91 fof(f316,definition,(
% 12.29/1.91 sQ26_spl <=> (has_immunity(sK2_skl,sK3_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f317,plain,(
% 12.29/1.91 has_immunity(sK2_skl,sK3_skl)|~sQ26_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f316])).
% 12.29/1.91 fof(f319,plain,(
% 12.29/1.91 ~sQ25_spl|sQ26_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f295,f313,f316])).
% 12.29/1.91 fof(f320,plain,(
% 12.29/1.91 $false|sQ25_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f315,f200])).
% 12.29/1.91 fof(f321,plain,(
% 12.29/1.91 sQ25_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f320])).
% 12.29/1.91 fof(f322,plain,(
% 12.29/1.91 $false|sQ21_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f301,f73])).
% 12.29/1.91 fof(f323,plain,(
% 12.29/1.91 sQ21_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f322])).
% 12.29/1.91 fof(f325,plain,(
% 12.29/1.91 greater_or_equal(sigma,zero)|~sQ18_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f290,f25])).
% 12.29/1.91 fof(f329,plain,(
% 12.29/1.91 ![X0]: (~organization(sK2_skl)|has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK4_skl)))),
% 12.29/1.91 inference(resolution,[status(thm)],[f292,f51])).
% 12.29/1.91 fof(f330,plain,(
% 12.29/1.91 ![X0]: (~organization(sK2_skl)|~has_immunity(sK2_skl,X0)|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK4_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f292,f49])).
% 12.29/1.91 fof(f331,plain,(
% 12.29/1.91 ~has_endowment(sK2_skl)|~greater(age(sK2_skl,sK4_skl),eta)),
% 12.29/1.91 inference(resolution,[status(thm)],[f292,f43])).
% 12.29/1.91 fof(f332,definition,(
% 12.29/1.91 ![X0]: (sQ27_spl <=> (has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK4_skl))))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f335,plain,(
% 12.29/1.91 ~sQ21_spl|sQ27_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f329,f299,f332])).
% 12.29/1.91 fof(f336,definition,(
% 12.29/1.91 ![X0]: (sQ28_spl <=> (~has_immunity(sK2_skl,X0)|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK4_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f337,plain,(
% 12.29/1.91 ![X0]: (~has_immunity(sK2_skl,X0)|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK4_skl)|~sQ28_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f336])).
% 12.29/1.91 fof(f339,plain,(
% 12.29/1.91 ~sQ21_spl|sQ28_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f330,f299,f336])).
% 12.29/1.91 fof(f340,definition,(
% 12.29/1.91 sQ29_spl <=> (greater(age(sK2_skl,sK4_skl),eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f342,plain,(
% 12.29/1.91 ~greater(age(sK2_skl,sK4_skl),eta)|sQ29_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f340])).
% 12.29/1.91 fof(f343,plain,(
% 12.29/1.91 ~sQ10_spl|~sQ29_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f331,f157,f340])).
% 12.29/1.91 fof(f344,plain,(
% 12.29/1.91 $false|sQ10_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f159,f74])).
% 12.29/1.91 fof(f345,plain,(
% 12.29/1.91 sQ10_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f344])).
% 12.29/1.91 fof(f346,plain,(
% 12.29/1.91 ![X0]: (~organization(sK2_skl)|has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ26_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f317,f51])).
% 12.29/1.91 fof(f347,plain,(
% 12.29/1.91 ![X0]: (~organization(sK2_skl)|~has_immunity(sK2_skl,X0)|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK3_skl)|~sQ26_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f317,f49])).
% 12.29/1.91 fof(f348,plain,(
% 12.29/1.91 ~has_endowment(sK2_skl)|~greater(age(sK2_skl,sK3_skl),eta)|~sQ26_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f317,f43])).
% 12.29/1.91 fof(f349,definition,(
% 12.29/1.91 ![X0]: (sQ30_spl <=> (has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK3_skl))))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f350,plain,(
% 12.29/1.91 ![X0]: (has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ30_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f349])).
% 12.29/1.91 fof(f352,plain,(
% 12.29/1.91 ~sQ21_spl|sQ30_spl|~sQ26_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f346,f299,f349,f316])).
% 12.29/1.91 fof(f353,definition,(
% 12.29/1.91 ![X0]: (sQ31_spl <=> (~has_immunity(sK2_skl,X0)|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK3_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f356,plain,(
% 12.29/1.91 ~sQ21_spl|sQ31_spl|~sQ26_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f347,f299,f353,f316])).
% 12.29/1.91 fof(f357,definition,(
% 12.29/1.91 sQ32_spl <=> (greater(age(sK2_skl,sK3_skl),eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f360,plain,(
% 12.29/1.91 ~sQ10_spl|~sQ32_spl|~sQ26_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f348,f157,f357,f316])).
% 12.29/1.91 fof(f362,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,X1),sigma)|dissimilar(sK2_skl,X0,X1))),
% 12.29/1.91 inference(resolution,[status(thm)],[f67,f73])).
% 12.29/1.91 fof(f368,plain,(
% 12.29/1.91 ~has_endowment(sK2_skl)|~greater(age(sK2_skl,sK5_skl),eta)|~sQ24_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f310,f43])).
% 12.29/1.91 fof(f377,definition,(
% 12.29/1.91 sQ35_spl <=> (greater(age(sK2_skl,sK5_skl),eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f380,plain,(
% 12.29/1.91 ~sQ10_spl|~sQ35_spl|~sQ24_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f368,f157,f377,f309])).
% 12.29/1.91 fof(f391,plain,(
% 12.29/1.91 ![X0]: (~greater(X0,age(sK2_skl,sK5_skl))|~greater(eta,X0))),
% 12.29/1.91 inference(resolution,[status(thm)],[f97,f77])).
% 12.29/1.91 fof(f397,plain,(
% 12.29/1.91 ![X0,X1,X2,X3]: (~greater(X0,X1)|~greater(X2,X0)|~greater(X1,X3)|~greater(X3,X2))),
% 12.29/1.91 inference(resolution,[status(thm)],[f97,f35])).
% 12.29/1.91 fof(f405,plain,(
% 12.29/1.91 ![X0]: (~greater(X0,X0)|~greater(X0,X0))),
% 12.29/1.91 inference(factoring,[status(thm)],[f97])).
% 12.29/1.91 fof(f406,plain,(
% 12.29/1.91 ![X0]: (~greater(X0,X0))),
% 12.29/1.91 inference(duplicate_literals_removal,[status(thm)],[f405])).
% 12.29/1.91 fof(f408,plain,(
% 12.29/1.91 eta=eta|smaller(eta,eta)|sQ13_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f141,f182])).
% 12.29/1.91 fof(f412,plain,(
% 12.29/1.91 ![X0,X1]: (X0=X1|smaller(X1,X0)|smaller_or_equal(X0,X1))),
% 12.29/1.91 inference(resolution,[status(thm)],[f141,f20])).
% 12.29/1.91 fof(f417,plain,(
% 12.29/1.91 sQ14_spl|sQ13_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f408,f183,f180])).
% 12.29/1.91 fof(f426,plain,(
% 12.29/1.91 greater(sigma,zero)|sigma=zero|~sQ18_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f325,f24])).
% 12.29/1.91 fof(f427,definition,(
% 12.29/1.91 sQ36_spl <=> (greater(sigma,zero))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f430,plain,(
% 12.29/1.91 sQ36_spl|sQ19_spl|~sQ18_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f426,f427,f252,f249])).
% 12.29/1.91 fof(f486,plain,(
% 12.29/1.91 greater(age(sK2_skl,sK5_skl),eta)|age(sK2_skl,sK5_skl)=eta),
% 12.29/1.91 inference(resolution,[status(thm)],[f172,f24])).
% 12.29/1.91 fof(f487,definition,(
% 12.29/1.91 sQ44_spl <=> (age(sK2_skl,sK5_skl)=eta)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f488,plain,(
% 12.29/1.91 age(sK2_skl,sK5_skl)=eta|~sQ44_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f487])).
% 12.29/1.91 fof(f490,plain,(
% 12.29/1.91 sQ35_spl|sQ44_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f486,f377,f487])).
% 12.29/1.91 fof(f493,plain,(
% 12.29/1.91 greater(eta,eta)|~sQ44_spl),
% 12.29/1.91 inference(backward_demodulation,[status(thm)],[f488,f77])).
% 12.29/1.91 fof(f497,plain,(
% 12.29/1.91 $false|~sQ44_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f493,f406])).
% 12.29/1.91 fof(f498,plain,(
% 12.29/1.91 ~sQ44_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f497])).
% 12.29/1.91 fof(f508,plain,(
% 12.29/1.91 smaller(eta,age(sK2_skl,sK5_skl))|eta=age(sK2_skl,sK5_skl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f173,f36])).
% 12.29/1.91 fof(f510,definition,(
% 12.29/1.91 sQ45_spl <=> (smaller(eta,age(sK2_skl,sK5_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f513,plain,(
% 12.29/1.91 sQ45_spl|sQ44_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f508,f510,f487])).
% 12.29/1.91 fof(f521,plain,(
% 12.29/1.91 greater(age(sK2_skl,sK6_skl),sigma)|age(sK2_skl,sK6_skl)=sigma),
% 12.29/1.91 inference(resolution,[status(thm)],[f223,f24])).
% 12.29/1.91 fof(f522,definition,(
% 12.29/1.91 sQ46_spl <=> (greater(age(sK2_skl,sK6_skl),sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f525,definition,(
% 12.29/1.91 sQ47_spl <=> (age(sK2_skl,sK6_skl)=sigma)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f526,plain,(
% 12.29/1.91 age(sK2_skl,sK6_skl)=sigma|~sQ47_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f525])).
% 12.29/1.91 fof(f528,plain,(
% 12.29/1.91 sQ46_spl|sQ47_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f521,f522,f525])).
% 12.29/1.91 fof(f531,plain,(
% 12.29/1.91 greater(sigma,sigma)|~sQ47_spl),
% 12.29/1.91 inference(backward_demodulation,[status(thm)],[f526,f79])).
% 12.29/1.91 fof(f533,plain,(
% 12.29/1.91 $false|~sQ47_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f531,f406])).
% 12.29/1.91 fof(f534,plain,(
% 12.29/1.91 ~sQ47_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f533])).
% 12.29/1.91 fof(f540,plain,(
% 12.29/1.91 smaller(sigma,age(sK2_skl,sK6_skl))|sigma=age(sK2_skl,sK6_skl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f224,f36])).
% 12.29/1.91 fof(f542,definition,(
% 12.29/1.91 sQ48_spl <=> (smaller(sigma,age(sK2_skl,sK6_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f545,plain,(
% 12.29/1.91 sQ48_spl|sQ47_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f540,f542,f525])).
% 12.29/1.91 fof(f548,plain,(
% 12.29/1.91 ![X0]: (~greater(X0,sigma)|smaller(zero,X0)|zero=X0)),
% 12.29/1.91 inference(resolution,[status(thm)],[f248,f36])).
% 12.29/1.91 fof(f558,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,sK6_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f362,f79])).
% 12.29/1.91 fof(f559,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,X1)|smaller(age(sK2_skl,X1),sigma)|age(sK2_skl,X1)=sigma)),
% 12.29/1.91 inference(resolution,[status(thm)],[f362,f36])).
% 12.29/1.91 fof(f560,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,X1)|~greater(age(sK2_skl,X1),X2)|~greater(X2,sigma))),
% 12.29/1.91 inference(resolution,[status(thm)],[f362,f35])).
% 12.29/1.91 fof(f562,definition,(
% 12.29/1.91 ![X0]: (sQ49_spl <=> (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,sK3_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f563,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,sK3_skl)|~sQ49_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f562])).
% 12.29/1.91 fof(f565,definition,(
% 12.29/1.91 sQ50_spl <=> (greater(zero,sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f570,plain,(
% 12.29/1.91 ![X0]: (~greater(age(sK2_skl,sK4_skl),X0)|~greater(X0,eta)|sQ29_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f342,f35])).
% 12.29/1.91 fof(f576,plain,(
% 12.29/1.91 ![X0,X1]: (is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,X1),capability(sK2_skl,X0))|~age(sK2_skl,X1)=zero)),
% 12.29/1.91 inference(resolution,[status(thm)],[f286,f73])).
% 12.29/1.91 fof(f578,plain,(
% 12.29/1.91 ![X0,X1]: (has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,X1))|smaller(capability(sK2_skl,X1),capability(sK2_skl,X0))|capability(sK2_skl,X1)=capability(sK2_skl,X0))),
% 12.29/1.91 inference(resolution,[status(thm)],[f288,f73])).
% 12.29/1.91 fof(f581,plain,(
% 12.29/1.91 ![X0,X1]: (X0=X1|smaller_or_equal(X0,X1)|greater(X0,X1))),
% 12.29/1.91 inference(resolution,[status(thm)],[f412,f29])).
% 12.29/1.91 fof(f583,definition,(
% 12.29/1.91 sQ51_spl <=> (smaller_or_equal(eta,eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f585,plain,(
% 12.29/1.91 ~smaller_or_equal(eta,eta)|sQ51_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f583])).
% 12.29/1.91 fof(f596,definition,(
% 12.29/1.91 sQ53_spl <=> (greater(eta,sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f603,plain,(
% 12.29/1.91 $false|sQ51_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f585,f93])).
% 12.29/1.91 fof(f604,plain,(
% 12.29/1.91 sQ51_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f603])).
% 12.29/1.91 fof(f647,definition,(
% 12.29/1.91 sQ56_spl <=> (greater(sigma,sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f648,plain,(
% 12.29/1.91 greater(sigma,sigma)|~sQ56_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f647])).
% 12.29/1.91 fof(f656,plain,(
% 12.29/1.91 sigma=age(sK2_skl,sK6_skl)|smaller_or_equal(sigma,age(sK2_skl,sK6_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f581,f224])).
% 12.29/1.91 fof(f658,plain,(
% 12.29/1.91 eta=sigma|smaller_or_equal(eta,sigma)),
% 12.29/1.91 inference(resolution,[status(thm)],[f581,f96])).
% 12.29/1.91 fof(f659,plain,(
% 12.29/1.91 ![X0]: (eta=X0|smaller_or_equal(eta,X0)|~greater(X0,sigma))),
% 12.29/1.91 inference(resolution,[status(thm)],[f581,f188])).
% 12.29/1.91 fof(f662,plain,(
% 12.29/1.91 ![X0]: (zero=X0|smaller_or_equal(zero,X0)|~greater(X0,sigma))),
% 12.29/1.91 inference(resolution,[status(thm)],[f581,f248])).
% 12.29/1.91 fof(f663,plain,(
% 12.29/1.91 ![X0]: (zero=X0|smaller_or_equal(zero,X0)|~greater(X0,eta))),
% 12.29/1.91 inference(resolution,[status(thm)],[f581,f98])).
% 12.29/1.91 fof(f671,plain,(
% 12.29/1.91 ![X0,X1]: (X0=X1|smaller_or_equal(X0,X1)|~greater(X1,X0))),
% 12.29/1.91 inference(resolution,[status(thm)],[f581,f32])).
% 12.29/1.91 fof(f676,definition,(
% 12.29/1.91 sQ58_spl <=> (smaller_or_equal(sigma,age(sK2_skl,sK6_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f679,plain,(
% 12.29/1.91 sQ47_spl|sQ58_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f656,f525,f676])).
% 12.29/1.91 fof(f680,definition,(
% 12.29/1.91 sQ59_spl <=> (smaller_or_equal(eta,sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f683,plain,(
% 12.29/1.91 sQ9_spl|sQ59_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f658,f151,f680])).
% 12.29/1.91 fof(f684,definition,(
% 12.29/1.91 sQ60_spl <=> (smaller_or_equal(zero,sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f689,plain,(
% 12.29/1.91 $false|~sQ9_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f177,f406])).
% 12.29/1.91 fof(f690,plain,(
% 12.29/1.91 ~sQ9_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f689])).
% 12.29/1.91 fof(f695,definition,(
% 12.29/1.91 ![X0]: (sQ61_spl <=> (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,sK4_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f696,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,sK4_skl)|~sQ61_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f695])).
% 12.29/1.91 fof(f699,definition,(
% 12.29/1.91 sQ62_spl <=> (has_immunity(sK2_skl,sK4_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f737,plain,(
% 12.29/1.91 greater(sigma,age(sK2_skl,sK5_skl))|~sQ16_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f210,f29])).
% 12.29/1.91 fof(f779,plain,(
% 12.29/1.91 eta=age(sK2_skl,sK5_skl)|smaller_or_equal(eta,age(sK2_skl,sK5_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f173,f581])).
% 12.29/1.91 fof(f782,definition,(
% 12.29/1.91 sQ65_spl <=> (smaller_or_equal(eta,age(sK2_skl,sK5_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f785,plain,(
% 12.29/1.91 sQ44_spl|sQ65_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f779,f487,f782])).
% 12.29/1.91 fof(f831,plain,(
% 12.29/1.91 ~greater(age(sK2_skl,sK5_skl),sigma)|~greater(age(sK2_skl,sK5_skl),sigma)|~sQ16_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f397,f737])).
% 12.29/1.91 fof(f833,plain,(
% 12.29/1.91 ~greater(zero,sigma)|~greater(zero,sigma)|~sQ18_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f397,f290])).
% 12.29/1.91 fof(f835,plain,(
% 12.29/1.91 ~greater(eta,sigma)|~greater(eta,sigma)),
% 12.29/1.91 inference(resolution,[status(thm)],[f397,f80])).
% 12.29/1.91 fof(f837,plain,(
% 12.29/1.91 ~greater(eta,age(sK2_skl,sK5_skl))|~greater(eta,age(sK2_skl,sK5_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f397,f77])).
% 12.29/1.91 fof(f839,plain,(
% 12.29/1.91 ~greater(sigma,age(sK2_skl,sK6_skl))|~greater(sigma,age(sK2_skl,sK6_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f397,f79])).
% 12.29/1.91 fof(f841,plain,(
% 12.29/1.91 ~greater(zero,eta)|~greater(zero,eta)),
% 12.29/1.91 inference(resolution,[status(thm)],[f397,f81])).
% 12.29/1.91 fof(f844,plain,(
% 12.29/1.91 ![X0,X1,X2,X3]: (~greater(X0,X1)|~greater(X1,X2)|~greater(X2,X3)|X3=X0|smaller_or_equal(X3,X0))),
% 12.29/1.91 inference(resolution,[status(thm)],[f397,f581])).
% 12.29/1.91 fof(f846,plain,(
% 12.29/1.91 ![X0,X1,X2,X3]: (~greater(X0,X1)|~greater(X1,X2)|~greater(X2,X3)|smaller(X3,X0)|X3=X0)),
% 12.29/1.91 inference(resolution,[status(thm)],[f397,f36])).
% 12.29/1.91 fof(f871,definition,(
% 12.29/1.91 sQ66_spl <=> (greater(age(sK2_skl,sK5_skl),sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f873,plain,(
% 12.29/1.91 ~greater(age(sK2_skl,sK5_skl),sigma)|sQ66_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f871])).
% 12.29/1.91 fof(f874,plain,(
% 12.29/1.91 ~sQ66_spl|~sQ16_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f831,f871,f209])).
% 12.29/1.91 fof(f875,plain,(
% 12.29/1.91 ~sQ50_spl|~sQ18_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f833,f565,f249])).
% 12.29/1.91 fof(f876,plain,(
% 12.29/1.91 ~sQ53_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f835,f596])).
% 12.29/1.91 fof(f877,definition,(
% 12.29/1.91 sQ67_spl <=> (greater(eta,age(sK2_skl,sK5_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f880,plain,(
% 12.29/1.91 ~sQ67_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f837,f877])).
% 12.29/1.91 fof(f881,definition,(
% 12.29/1.91 sQ68_spl <=> (greater(sigma,age(sK2_skl,sK6_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f884,plain,(
% 12.29/1.91 ~sQ68_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f839,f881])).
% 12.29/1.91 fof(f885,definition,(
% 12.29/1.91 sQ69_spl <=> (greater(zero,eta))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f888,plain,(
% 12.29/1.91 ~sQ69_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f841,f885])).
% 12.29/1.91 fof(f1037,definition,(
% 12.29/1.91 ![X0]: (sQ72_spl <=> (is_aligned(sK2_skl,X0)|~age(sK2_skl,X0)=zero))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1038,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|~age(sK2_skl,X0)=zero|~sQ72_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1037])).
% 12.29/1.91 fof(f1040,definition,(
% 12.29/1.91 ![X1]: (sQ73_spl <=> (~age(sK2_skl,X1)=zero|~is_aligned(sK2_skl,X1)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1041,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|~is_aligned(sK2_skl,X0)|~sQ73_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1040])).
% 12.29/1.91 fof(f1044,definition,(
% 12.29/1.91 ![X0]: (sQ74_spl <=> (is_aligned(sK2_skl,X0)|greater(age(sK2_skl,X0),sigma)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1045,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|greater(age(sK2_skl,X0),sigma)|~sQ74_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1044])).
% 12.29/1.91 fof(f1047,definition,(
% 12.29/1.91 ![X1]: (sQ75_spl <=> (~age(sK2_skl,X1)=zero|~age(sK2_skl,X1)=zero))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1048,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|~age(sK2_skl,X0)=zero|~sQ75_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1047])).
% 12.29/1.91 fof(f1051,definition,(
% 12.29/1.91 ![X0]: (sQ76_spl <=> (is_aligned(sK2_skl,X0)|is_aligned(sK2_skl,X0)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1052,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|is_aligned(sK2_skl,X0)|~sQ76_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1051])).
% 12.29/1.91 fof(f1055,definition,(
% 12.29/1.91 ![X0]: (sQ77_spl <=> (is_aligned(sK2_skl,X0)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1056,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|~sQ77_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1055])).
% 12.29/1.91 fof(f1058,definition,(
% 12.29/1.91 ![X1]: (sQ78_spl <=> (~age(sK2_skl,X1)=zero))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1059,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|~sQ78_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1058])).
% 12.29/1.91 fof(f1062,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|~sQ76_spl)),
% 12.29/1.91 inference(duplicate_literals_removal,[status(thm)],[f1052])).
% 12.29/1.91 fof(f1063,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|~sQ75_spl)),
% 12.29/1.91 inference(duplicate_literals_removal,[status(thm)],[f1048])).
% 12.29/1.91 fof(f1067,plain,(
% 12.29/1.91 ![X0,X1]: (~dissimilar(sK2_skl,X0,X1)|~is_aligned(sK2_skl,X0)|~sQ77_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1056,f57])).
% 12.29/1.91 fof(f1072,definition,(
% 12.29/1.91 ![X0,X1]: (sQ80_spl <=> (dissimilar(sK2_skl,X0,X1)|is_aligned(sK2_skl,X0)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1073,plain,(
% 12.29/1.91 ![X0,X1]: (dissimilar(sK2_skl,X0,X1)|is_aligned(sK2_skl,X0)|~sQ80_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1072])).
% 12.29/1.91 fof(f1076,definition,(
% 12.29/1.91 ![X0,X1]: (sQ81_spl <=> (dissimilar(sK2_skl,X0,X1)|is_aligned(sK2_skl,X1)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1077,plain,(
% 12.29/1.91 ![X0,X1]: (dissimilar(sK2_skl,X0,X1)|is_aligned(sK2_skl,X1)|~sQ81_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1076])).
% 12.29/1.91 fof(f1080,plain,(
% 12.29/1.91 ![X0,X1]: (~dissimilar(sK2_skl,X0,X1)|~sQ77_spl)),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f1067,f1056])).
% 12.29/1.91 fof(f1084,plain,(
% 12.29/1.91 ![X0,X1]: (~dissimilar(sK2_skl,X0,X1)|~is_aligned(sK2_skl,X0)|~sQ76_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1062,f57])).
% 12.29/1.91 fof(f1088,plain,(
% 12.29/1.91 ![X0,X1]: (~dissimilar(sK2_skl,X0,X1)|~sQ76_spl)),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f1084,f1062])).
% 12.29/1.91 fof(f1089,plain,(
% 12.29/1.91 $false|~sQ78_spl),
% 12.29/1.91 inference(backward_subsumption_resolution,[status(thm)],[f75,f1059])).
% 12.29/1.91 fof(f1091,plain,(
% 12.29/1.91 ~sQ78_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f1089])).
% 12.29/1.91 fof(f1094,plain,(
% 12.29/1.91 $false|~sQ75_spl),
% 12.29/1.91 inference(backward_subsumption_resolution,[status(thm)],[f75,f1063])).
% 12.29/1.91 fof(f1096,plain,(
% 12.29/1.91 ~sQ75_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f1094])).
% 12.29/1.91 fof(f1099,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,X1),sigma)|~is_aligned(sK2_skl,X0)|~age(sK2_skl,X1)=zero)),
% 12.29/1.91 inference(resolution,[status(thm)],[f362,f233])).
% 12.29/1.91 fof(f1100,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,X1),sigma)|~age(sK2_skl,X0)=zero|greater(age(sK2_skl,X1),sigma))),
% 12.29/1.91 inference(resolution,[status(thm)],[f362,f220])).
% 12.29/1.91 fof(f1103,definition,(
% 12.29/1.91 ![X1]: (sQ82_spl <=> (~greater(age(sK2_skl,X1),sigma)|~age(sK2_skl,X1)=zero))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1104,plain,(
% 12.29/1.91 ![X0]: (~greater(age(sK2_skl,X0),sigma)|~age(sK2_skl,X0)=zero|~sQ82_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1103])).
% 12.29/1.91 fof(f1106,plain,(
% 12.29/1.91 sQ73_spl|sQ82_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1099,f1040,f1103])).
% 12.29/1.91 fof(f1107,definition,(
% 12.29/1.91 ![X1]: (sQ83_spl <=> (~greater(age(sK2_skl,X1),sigma)|greater(age(sK2_skl,X1),sigma)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1110,plain,(
% 12.29/1.91 sQ75_spl|sQ83_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1100,f1047,f1107])).
% 12.29/1.91 fof(f1111,definition,(
% 12.29/1.91 ![X1]: (sQ84_spl <=> (~greater(age(sK2_skl,X1),sigma)|is_aligned(sK2_skl,X1)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1112,plain,(
% 12.29/1.91 ![X0]: (~greater(age(sK2_skl,X0),sigma)|is_aligned(sK2_skl,X0)|~sQ84_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1111])).
% 12.29/1.91 fof(f1115,definition,(
% 12.29/1.91 ![X1]: (sQ85_spl <=> (~greater(age(sK2_skl,X1),sigma)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1116,plain,(
% 12.29/1.91 ![X0]: (~greater(age(sK2_skl,X0),sigma)|~sQ85_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1115])).
% 12.29/1.91 fof(f1124,definition,(
% 12.29/1.91 ![X0]: (sQ86_spl <=> (is_aligned(sK2_skl,X0)|~is_aligned(sK2_skl,X0)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1128,definition,(
% 12.29/1.91 ![X1]: (sQ87_spl <=> (~age(sK2_skl,X1)=zero|greater(age(sK2_skl,X1),sigma)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1129,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|greater(age(sK2_skl,X0),sigma)|~sQ87_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1128])).
% 12.29/1.91 fof(f1134,plain,(
% 12.29/1.91 $false|~sQ85_spl),
% 12.29/1.91 inference(backward_subsumption_resolution,[status(thm)],[f79,f1116])).
% 12.29/1.91 fof(f1140,plain,(
% 12.29/1.91 ~sQ85_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f1134])).
% 12.29/1.91 fof(f1162,plain,(
% 12.29/1.91 ![X0,X1]: (is_aligned(sK2_skl,X0)|is_aligned(sK2_skl,X1)|is_aligned(sK2_skl,X0)|~sQ81_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1077,f56])).
% 12.29/1.91 fof(f1164,definition,(
% 12.29/1.91 ![X1]: (sQ88_spl <=> (~is_aligned(sK2_skl,X1)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1165,plain,(
% 12.29/1.91 ![X0]: (~is_aligned(sK2_skl,X0)|~sQ88_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1164])).
% 12.29/1.91 fof(f1169,plain,(
% 12.29/1.91 sQ76_spl|sQ77_spl|~sQ81_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1162,f1051,f1055,f1076])).
% 12.29/1.91 fof(f1173,plain,(
% 12.29/1.91 ![X0]: (~organization(sK2_skl)|~age(sK2_skl,X0)=zero|~sQ88_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1165,f61])).
% 12.29/1.91 fof(f1174,plain,(
% 12.29/1.91 ~sQ21_spl|sQ78_spl|~sQ88_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1173,f299,f1058,f1164])).
% 12.29/1.91 fof(f1182,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,X1),sigma)|~sQ76_spl)),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f362,f1088])).
% 12.29/1.91 fof(f1183,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|~sQ76_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1182,f79])).
% 12.29/1.91 fof(f1189,plain,(
% 12.29/1.91 sQ78_spl|~sQ76_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1183,f1058,f1051])).
% 12.29/1.91 fof(f1214,plain,(
% 12.29/1.91 ![X0,X1]: (is_aligned(sK2_skl,X0)|is_aligned(sK2_skl,X0)|is_aligned(sK2_skl,X1)|~sQ80_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1073,f56])).
% 12.29/1.91 fof(f1221,plain,(
% 12.29/1.91 sQ76_spl|sQ77_spl|~sQ80_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1214,f1051,f1055,f1072])).
% 12.29/1.91 fof(f1224,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,X1),sigma)|~sQ77_spl)),
% 12.29/1.91 inference(backward_subsumption_resolution,[status(thm)],[f362,f1080])).
% 12.29/1.91 fof(f1225,plain,(
% 12.29/1.91 sQ78_spl|sQ85_spl|~sQ77_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1224,f1058,f1115,f1055])).
% 12.29/1.91 fof(f1273,definition,(
% 12.29/1.91 sQ93_spl <=> (age(sK2_skl,sK6_skl)=zero)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1278,definition,(
% 12.29/1.91 sQ94_spl <=> (is_aligned(sK2_skl,sK6_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1279,plain,(
% 12.29/1.91 is_aligned(sK2_skl,sK6_skl)|~sQ94_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1278])).
% 12.29/1.91 fof(f1280,plain,(
% 12.29/1.91 ~is_aligned(sK2_skl,sK6_skl)|sQ94_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1278])).
% 12.29/1.91 fof(f1286,plain,(
% 12.29/1.91 ![X0]: (~dissimilar(sK2_skl,X0,sK6_skl)|~is_aligned(sK2_skl,X0)|~sQ94_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1279,f57])).
% 12.29/1.91 fof(f1291,definition,(
% 12.29/1.91 ![X0]: (sQ96_spl <=> (dissimilar(sK2_skl,X0,sK6_skl)|is_aligned(sK2_skl,X0)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1292,plain,(
% 12.29/1.91 ![X0]: (dissimilar(sK2_skl,X0,sK6_skl)|is_aligned(sK2_skl,X0)|~sQ96_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1291])).
% 12.29/1.91 fof(f1295,definition,(
% 12.29/1.91 ![X0]: (sQ97_spl <=> (dissimilar(sK2_skl,sK6_skl,X0)|is_aligned(sK2_skl,X0)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1296,plain,(
% 12.29/1.91 ![X0]: (dissimilar(sK2_skl,sK6_skl,X0)|is_aligned(sK2_skl,X0)|~sQ97_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1295])).
% 12.29/1.91 fof(f1299,plain,(
% 12.29/1.91 ~organization(sK2_skl)|~age(sK2_skl,sK6_skl)=zero|sQ94_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f1280,f61])).
% 12.29/1.91 fof(f1300,plain,(
% 12.29/1.91 ~sQ21_spl|~sQ93_spl|sQ94_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1299,f299,f1273,f1278])).
% 12.29/1.91 fof(f1302,plain,(
% 12.29/1.91 ![X0]: (~zero=zero|dissimilar(sK2_skl,sK3_skl,X0)|smaller(age(sK2_skl,X0),sigma)|age(sK2_skl,X0)=sigma)),
% 12.29/1.91 inference(paramodulation,[status(thm)],[f75,f559])).
% 12.29/1.91 fof(f1304,definition,(
% 12.29/1.91 sQ98_spl <=> (zero=zero)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1306,plain,(
% 12.29/1.91 ~zero=zero|sQ98_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1304])).
% 12.29/1.91 fof(f1307,definition,(
% 12.29/1.91 ![X0]: (sQ99_spl <=> (dissimilar(sK2_skl,sK3_skl,X0)|smaller(age(sK2_skl,X0),sigma)|age(sK2_skl,X0)=sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1310,plain,(
% 12.29/1.91 ~sQ98_spl|sQ99_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1302,f1304,f1307])).
% 12.29/1.91 fof(f1315,plain,(
% 12.29/1.91 $false|sQ98_spl),
% 12.29/1.91 inference(trivial_equality_resolution,[status(thm)],[f1306])).
% 12.29/1.91 fof(f1316,plain,(
% 12.29/1.91 sQ98_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f1315])).
% 12.29/1.91 fof(f1326,plain,(
% 12.29/1.91 ![X0,X1,X2]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,X1)|~greater(age(sK2_skl,X1),X2)|smaller(X2,sigma)|X2=sigma)),
% 12.29/1.91 inference(resolution,[status(thm)],[f560,f36])).
% 12.29/1.91 fof(f1329,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|~age(sK2_skl,X0)=zero|greater(age(sK2_skl,sK3_skl),sigma)|~sQ49_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f563,f220])).
% 12.29/1.91 fof(f1332,definition,(
% 12.29/1.91 sQ101_spl <=> (age(sK2_skl,sK3_skl)=zero)),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1334,plain,(
% 12.29/1.91 ~age(sK2_skl,sK3_skl)=zero|sQ101_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1332])).
% 12.29/1.91 fof(f1336,definition,(
% 12.29/1.91 sQ102_spl <=> (greater(age(sK2_skl,sK3_skl),sigma))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1337,plain,(
% 12.29/1.91 greater(age(sK2_skl,sK3_skl),sigma)|~sQ102_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1336])).
% 12.29/1.91 fof(f1339,plain,(
% 12.29/1.91 sQ75_spl|sQ102_spl|~sQ49_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1329,f1047,f1336,f562])).
% 12.29/1.91 fof(f1340,definition,(
% 12.29/1.91 sQ103_spl <=> (is_aligned(sK2_skl,sK3_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1341,plain,(
% 12.29/1.91 is_aligned(sK2_skl,sK3_skl)|~sQ103_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1340])).
% 12.29/1.91 fof(f1342,plain,(
% 12.29/1.91 ~is_aligned(sK2_skl,sK3_skl)|sQ103_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1340])).
% 12.29/1.91 fof(f1345,plain,(
% 12.29/1.91 greater(zero,sigma)|~sQ102_spl),
% 12.29/1.91 inference(forward_demodulation,[status(thm)],[f75,f1337])).
% 12.29/1.91 fof(f1346,plain,(
% 12.29/1.91 $false|~sQ102_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f1345,f244])).
% 12.29/1.91 fof(f1347,plain,(
% 12.29/1.91 ~sQ102_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f1346])).
% 12.29/1.91 fof(f1348,plain,(
% 12.29/1.91 ~zero=zero|sQ101_spl),
% 12.29/1.91 inference(forward_demodulation,[status(thm)],[f75,f1334])).
% 12.29/1.91 fof(f1349,plain,(
% 12.29/1.91 $false|sQ101_spl),
% 12.29/1.91 inference(trivial_equality_resolution,[status(thm)],[f1348])).
% 12.29/1.91 fof(f1350,plain,(
% 12.29/1.91 sQ101_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f1349])).
% 12.29/1.91 fof(f1352,plain,(
% 12.29/1.91 ![X0]: (~organization(sK2_skl)|is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,sK3_skl),capability(sK2_skl,X0))|~sQ103_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1341,f63])).
% 12.29/1.91 fof(f1353,plain,(
% 12.29/1.91 ![X0]: (dissimilar(sK2_skl,X0,sK3_skl)|~organization(sK2_skl)|is_aligned(sK2_skl,X0)|~sQ103_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1341,f59])).
% 12.29/1.91 fof(f1354,plain,(
% 12.29/1.91 ![X0]: (dissimilar(sK2_skl,sK3_skl,X0)|~organization(sK2_skl)|is_aligned(sK2_skl,X0)|~sQ103_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1341,f58])).
% 12.29/1.91 fof(f1355,plain,(
% 12.29/1.91 ![X0]: (~dissimilar(sK2_skl,X0,sK3_skl)|~is_aligned(sK2_skl,X0)|~sQ103_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1341,f57])).
% 12.29/1.91 fof(f1356,definition,(
% 12.29/1.91 ![X0]: (sQ104_spl <=> (is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,sK3_skl),capability(sK2_skl,X0))))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1357,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,sK3_skl),capability(sK2_skl,X0))|~sQ104_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1356])).
% 12.29/1.91 fof(f1359,plain,(
% 12.29/1.91 ~sQ21_spl|sQ104_spl|~sQ103_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1352,f299,f1356,f1340])).
% 12.29/1.91 fof(f1360,definition,(
% 12.29/1.91 ![X0]: (sQ105_spl <=> (dissimilar(sK2_skl,X0,sK3_skl)|is_aligned(sK2_skl,X0)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1361,plain,(
% 12.29/1.91 ![X0]: (dissimilar(sK2_skl,X0,sK3_skl)|is_aligned(sK2_skl,X0)|~sQ105_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1360])).
% 12.29/1.91 fof(f1363,plain,(
% 12.29/1.91 sQ105_spl|~sQ21_spl|~sQ103_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1353,f1360,f299,f1340])).
% 12.29/1.91 fof(f1364,definition,(
% 12.29/1.91 ![X0]: (sQ106_spl <=> (dissimilar(sK2_skl,sK3_skl,X0)|is_aligned(sK2_skl,X0)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1365,plain,(
% 12.29/1.91 ![X0]: (dissimilar(sK2_skl,sK3_skl,X0)|is_aligned(sK2_skl,X0)|~sQ106_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1364])).
% 12.29/1.91 fof(f1367,plain,(
% 12.29/1.91 sQ106_spl|~sQ21_spl|~sQ103_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1354,f1364,f299,f1340])).
% 12.29/1.91 fof(f1368,plain,(
% 12.29/1.91 ~organization(sK2_skl)|~age(sK2_skl,sK3_skl)=zero|sQ103_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f1342,f61])).
% 12.29/1.91 fof(f1369,plain,(
% 12.29/1.91 ~sQ21_spl|~sQ101_spl|sQ103_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1368,f299,f1332,f1340])).
% 12.29/1.91 fof(f1379,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|~organization(sK2_skl)|is_aligned(sK2_skl,X1)|greater(capability(sK2_skl,X0),capability(sK2_skl,X1))|~sQ72_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1038,f63])).
% 12.29/1.91 fof(f1380,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X1,X0)|~organization(sK2_skl)|is_aligned(sK2_skl,X1)|~sQ72_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1038,f59])).
% 12.29/1.91 fof(f1381,plain,(
% 12.29/1.91 ![X0,X1]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,X1)|~organization(sK2_skl)|is_aligned(sK2_skl,X1)|~sQ72_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1038,f58])).
% 12.29/1.91 fof(f1383,definition,(
% 12.29/1.91 ![X0,X1]: (sQ107_spl <=> (~age(sK2_skl,X0)=zero|is_aligned(sK2_skl,X1)|greater(capability(sK2_skl,X0),capability(sK2_skl,X1))))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1386,plain,(
% 12.29/1.91 sQ107_spl|~sQ21_spl|~sQ72_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1379,f1383,f299,f1037])).
% 12.29/1.91 fof(f1387,definition,(
% 12.29/1.91 ![X0,X1]: (sQ108_spl <=> (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X1,X0)|is_aligned(sK2_skl,X1)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1390,plain,(
% 12.29/1.91 sQ108_spl|~sQ21_spl|~sQ72_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1380,f1387,f299,f1037])).
% 12.29/1.91 fof(f1391,definition,(
% 12.29/1.91 ![X0,X1]: (sQ109_spl <=> (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,X1)|is_aligned(sK2_skl,X1)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1394,plain,(
% 12.29/1.91 sQ109_spl|~sQ21_spl|~sQ72_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1381,f1391,f299,f1037])).
% 12.29/1.91 fof(f1395,plain,(
% 12.29/1.91 ![X0,X1]: (is_aligned(sK2_skl,X0)|~age(sK2_skl,X1)=zero|~organization(sK2_skl)|has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,X1)))),
% 12.29/1.91 inference(resolution,[status(thm)],[f576,f287])).
% 12.29/1.91 fof(f1410,plain,(
% 12.29/1.91 ![X0,X1]: (is_aligned(sK2_skl,X0)|~age(sK2_skl,X1)=zero|~greater(capability(sK2_skl,X0),capability(sK2_skl,X1)))),
% 12.29/1.91 inference(resolution,[status(thm)],[f576,f32])).
% 12.29/1.91 fof(f1411,definition,(
% 12.29/1.91 ![X0,X1]: (sQ110_spl <=> (is_aligned(sK2_skl,X0)|~age(sK2_skl,X1)=zero|has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,X1))))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1412,plain,(
% 12.29/1.91 ![X0,X1]: (is_aligned(sK2_skl,X0)|~age(sK2_skl,X1)=zero|has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,X1))|~sQ110_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1411])).
% 12.29/1.91 fof(f1414,plain,(
% 12.29/1.91 sQ110_spl|~sQ21_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1395,f1411,f299])).
% 12.29/1.91 fof(f1431,plain,(
% 12.29/1.91 $false|~sQ72_spl|~sQ73_spl),
% 12.29/1.91 inference(backward_subsumption_resolution,[status(thm)],[f75,f1432])).
% 12.29/1.91 fof(f1432,plain,(
% 12.29/1.91 ![X0]: (~age(sK2_skl,X0)=zero|~sQ72_spl|~sQ73_spl)),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f1041,f1038])).
% 12.29/1.91 fof(f1434,plain,(
% 12.29/1.91 ~sQ72_spl|~sQ73_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f1431])).
% 12.29/1.91 fof(f1450,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|is_aligned(sK2_skl,sK6_skl)|is_aligned(sK2_skl,X0)|~sQ97_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1296,f56])).
% 12.29/1.91 fof(f1455,plain,(
% 12.29/1.91 sQ76_spl|sQ94_spl|~sQ97_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1450,f1051,f1278,f1295])).
% 12.29/1.91 fof(f1461,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|is_aligned(sK2_skl,X0)|is_aligned(sK2_skl,sK6_skl)|~sQ96_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1292,f56])).
% 12.29/1.91 fof(f1465,plain,(
% 12.29/1.91 sQ76_spl|sQ94_spl|~sQ96_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1461,f1051,f1278,f1291])).
% 12.29/1.91 fof(f1473,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|~age(sK2_skl,sK3_skl)=zero|greater(age(sK2_skl,X0),sigma)|~sQ106_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1365,f220])).
% 12.29/1.91 fof(f1478,plain,(
% 12.29/1.91 sQ74_spl|~sQ101_spl|~sQ106_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1473,f1044,f1332,f1364])).
% 12.29/1.91 fof(f1482,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|~is_aligned(sK2_skl,X0)|~age(sK2_skl,sK3_skl)=zero|~sQ105_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1361,f233])).
% 12.29/1.91 fof(f1486,plain,(
% 12.29/1.91 sQ86_spl|~sQ101_spl|~sQ105_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1482,f1124,f1332,f1360])).
% 12.29/1.91 fof(f1500,plain,(
% 12.29/1.91 smaller(zero,age(sK2_skl,sK5_skl))|zero=age(sK2_skl,sK5_skl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f239,f77])).
% 12.29/1.91 fof(f1502,plain,(
% 12.29/1.91 ![X0]: (smaller(zero,X0)|zero=X0|smaller(X0,eta)|X0=eta)),
% 12.29/1.91 inference(resolution,[status(thm)],[f239,f36])).
% 12.29/1.91 fof(f1512,definition,(
% 12.29/1.91 sQ113_spl <=> (smaller(zero,age(sK2_skl,sK5_skl)))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1513,plain,(
% 12.29/1.91 smaller(zero,age(sK2_skl,sK5_skl))|~sQ113_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1512])).
% 12.29/1.91 fof(f1515,definition,(
% 12.29/1.91 sQ114_spl <=> (zero=age(sK2_skl,sK5_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1516,plain,(
% 12.29/1.91 zero=age(sK2_skl,sK5_skl)|~sQ114_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1515])).
% 12.29/1.91 fof(f1518,plain,(
% 12.29/1.91 sQ113_spl|sQ114_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1500,f1512,f1515])).
% 12.29/1.91 fof(f1527,plain,(
% 12.29/1.91 ~greater(eta,zero)|~sQ114_spl),
% 12.29/1.91 inference(backward_demodulation,[status(thm)],[f1516,f173])).
% 12.29/1.91 fof(f1533,plain,(
% 12.29/1.91 $false|~sQ114_spl),
% 12.29/1.91 inference(forward_subsumption_resolution,[status(thm)],[f1527,f81])).
% 12.29/1.91 fof(f1534,plain,(
% 12.29/1.91 ~sQ114_spl),
% 12.29/1.91 inference(contradiction_clause,[status(thm)],[f1533])).
% 12.29/1.91 fof(f1557,plain,(
% 12.29/1.91 greater(age(sK2_skl,sK5_skl),zero)|~sQ113_spl),
% 12.29/1.91 inference(resolution,[status(thm)],[f1513,f29])).
% 12.29/1.91 fof(f1616,definition,(
% 12.29/1.91 sQ115_spl <=> (is_aligned(sK2_skl,sK5_skl))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1617,plain,(
% 12.29/1.91 is_aligned(sK2_skl,sK5_skl)|~sQ115_spl),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1616])).
% 12.29/1.91 fof(f1621,plain,(
% 12.29/1.91 ![X0]: (~organization(sK2_skl)|is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,sK5_skl),capability(sK2_skl,X0))|~sQ115_spl)),
% 12.29/1.91 inference(resolution,[status(thm)],[f1617,f63])).
% 12.29/1.91 fof(f1625,definition,(
% 12.29/1.91 ![X0]: (sQ116_spl <=> (is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,sK5_skl),capability(sK2_skl,X0))))),
% 12.29/1.91 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 12.29/1.91 fof(f1626,plain,(
% 12.29/1.91 ![X0]: (is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,sK5_skl),capability(sK2_skl,X0))|~sQ116_spl)),
% 12.29/1.91 inference(component_clause,[status(thm)],[f1625])).
% 12.29/1.91 fof(f1628,plain,(
% 12.29/1.91 ~sQ21_spl|sQ116_spl|~sQ115_spl),
% 12.29/1.91 inference(split_clause,[status(thm)],[f1621,f299,f1625,f1616])).
% 12.29/1.91 fof(f1640,plain,(
% 12.29/1.91 ~greater(zero,age(sK2_skl,sK5_skl))),
% 12.29/1.91 inference(resolution,[status(thm)],[f391,f81])).
% 12.29/1.91 fof(f1645,plain,(
% 12.29/1.92 ~greater(zero,age(sK2_skl,sK5_skl))|~greater(zero,age(sK2_skl,sK5_skl))|~sQ113_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1557,f397])).
% 12.29/1.92 fof(f1653,plain,(
% 12.29/1.92 greater_or_equal(age(sK2_skl,sK5_skl),zero)|~sQ113_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1557,f25])).
% 12.29/1.92 fof(f1655,definition,(
% 12.29/1.92 sQ119_spl <=> (greater(zero,age(sK2_skl,sK5_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1658,plain,(
% 12.29/1.92 ~sQ119_spl|~sQ113_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1645,f1655,f1512])).
% 12.29/1.92 fof(f1660,definition,(
% 12.29/1.92 sQ120_spl <=> (smaller_or_equal(zero,age(sK2_skl,sK5_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1667,plain,(
% 12.29/1.92 ![X0]: (~age(sK2_skl,X0)=zero|~age(sK2_skl,X0)=zero|greater(age(sK2_skl,sK4_skl),sigma)|~sQ61_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f696,f220])).
% 12.29/1.92 fof(f1674,definition,(
% 12.29/1.92 sQ122_spl <=> (greater(age(sK2_skl,sK4_skl),sigma))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1677,plain,(
% 12.29/1.92 sQ75_spl|sQ122_spl|~sQ61_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1667,f1047,f1674,f695])).
% 12.29/1.92 fof(f1678,definition,(
% 12.29/1.92 sQ123_spl <=> (is_aligned(sK2_skl,sK4_skl))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1679,plain,(
% 12.29/1.92 is_aligned(sK2_skl,sK4_skl)|~sQ123_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f1678])).
% 12.29/1.92 fof(f1688,plain,(
% 12.29/1.92 ![X0]: (~organization(sK2_skl)|is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,sK4_skl),capability(sK2_skl,X0))|~sQ123_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1679,f63])).
% 12.29/1.92 fof(f1689,plain,(
% 12.29/1.92 ![X0]: (dissimilar(sK2_skl,X0,sK4_skl)|~organization(sK2_skl)|is_aligned(sK2_skl,X0)|~sQ123_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1679,f59])).
% 12.29/1.92 fof(f1690,plain,(
% 12.29/1.92 ![X0]: (dissimilar(sK2_skl,sK4_skl,X0)|~organization(sK2_skl)|is_aligned(sK2_skl,X0)|~sQ123_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1679,f58])).
% 12.29/1.92 fof(f1691,plain,(
% 12.29/1.92 ![X0]: (~dissimilar(sK2_skl,X0,sK4_skl)|~is_aligned(sK2_skl,X0)|~sQ123_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1679,f57])).
% 12.29/1.92 fof(f1692,definition,(
% 12.29/1.92 ![X0]: (sQ124_spl <=> (is_aligned(sK2_skl,X0)|greater(capability(sK2_skl,sK4_skl),capability(sK2_skl,X0))))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1695,plain,(
% 12.29/1.92 ~sQ21_spl|sQ124_spl|~sQ123_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1688,f299,f1692,f1678])).
% 12.29/1.92 fof(f1696,definition,(
% 12.29/1.92 ![X0]: (sQ125_spl <=> (dissimilar(sK2_skl,X0,sK4_skl)|is_aligned(sK2_skl,X0)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1699,plain,(
% 12.29/1.92 sQ125_spl|~sQ21_spl|~sQ123_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1689,f1696,f299,f1678])).
% 12.29/1.92 fof(f1700,definition,(
% 12.29/1.92 ![X0]: (sQ126_spl <=> (dissimilar(sK2_skl,sK4_skl,X0)|is_aligned(sK2_skl,X0)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1703,plain,(
% 12.29/1.92 sQ126_spl|~sQ21_spl|~sQ123_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1690,f1700,f299,f1678])).
% 12.29/1.92 fof(f1708,plain,(
% 12.29/1.92 zero=age(sK2_skl,sK5_skl)|smaller_or_equal(zero,age(sK2_skl,sK5_skl))),
% 12.29/1.92 inference(resolution,[status(thm)],[f1640,f581])).
% 12.29/1.92 fof(f1711,plain,(
% 12.29/1.92 sQ114_spl|sQ120_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1708,f1515,f1660])).
% 12.29/1.92 fof(f1713,plain,(
% 12.29/1.92 greater(age(sK2_skl,sK5_skl),zero)|age(sK2_skl,sK5_skl)=zero|~sQ113_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1653,f24])).
% 12.29/1.92 fof(f1714,definition,(
% 12.29/1.92 sQ127_spl <=> (greater(age(sK2_skl,sK5_skl),zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1717,plain,(
% 12.29/1.92 sQ127_spl|sQ114_spl|~sQ113_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1713,f1714,f1515,f1512])).
% 12.29/1.92 fof(f1737,plain,(
% 12.29/1.92 is_aligned(sK2_skl,sK6_skl)|~sQ84_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1112,f79])).
% 12.29/1.92 fof(f1743,plain,(
% 12.29/1.92 sQ94_spl|~sQ84_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1737,f1278,f1111])).
% 12.29/1.92 fof(f1903,plain,(
% 12.29/1.92 smaller(eta,age(sK2_skl,sK6_skl))|eta=age(sK2_skl,sK6_skl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f245,f79])).
% 12.29/1.92 fof(f1904,plain,(
% 12.29/1.92 ![X0]: (smaller(eta,X0)|eta=X0|X0=sigma|smaller_or_equal(X0,sigma))),
% 12.29/1.92 inference(resolution,[status(thm)],[f245,f581])).
% 12.29/1.92 fof(f1905,plain,(
% 12.29/1.92 ![X0]: (smaller(eta,X0)|eta=X0|smaller(X0,sigma)|X0=sigma)),
% 12.29/1.92 inference(resolution,[status(thm)],[f245,f36])).
% 12.29/1.92 fof(f1907,definition,(
% 12.29/1.92 sQ131_spl <=> (smaller(eta,age(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1908,plain,(
% 12.29/1.92 smaller(eta,age(sK2_skl,sK6_skl))|~sQ131_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f1907])).
% 12.29/1.92 fof(f1910,definition,(
% 12.29/1.92 sQ132_spl <=> (eta=age(sK2_skl,sK6_skl))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1911,plain,(
% 12.29/1.92 eta=age(sK2_skl,sK6_skl)|~sQ132_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f1910])).
% 12.29/1.92 fof(f1913,plain,(
% 12.29/1.92 sQ131_spl|sQ132_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1903,f1907,f1910])).
% 12.29/1.92 fof(f1915,plain,(
% 12.29/1.92 greater(eta,sigma)|~sQ132_spl),
% 12.29/1.92 inference(backward_demodulation,[status(thm)],[f1911,f79])).
% 12.29/1.92 fof(f1925,plain,(
% 12.29/1.92 $false|~sQ132_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f1915,f96])).
% 12.29/1.92 fof(f1926,plain,(
% 12.29/1.92 ~sQ132_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f1925])).
% 12.29/1.92 fof(f1945,plain,(
% 12.29/1.92 greater(age(sK2_skl,sK6_skl),eta)|~sQ131_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1908,f29])).
% 12.29/1.92 fof(f1960,plain,(
% 12.29/1.92 ~greater(eta,age(sK2_skl,sK6_skl))|~greater(eta,age(sK2_skl,sK6_skl))|~sQ131_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1945,f397])).
% 12.29/1.92 fof(f1968,plain,(
% 12.29/1.92 greater_or_equal(age(sK2_skl,sK6_skl),eta)|~sQ131_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1945,f25])).
% 12.29/1.92 fof(f1970,definition,(
% 12.29/1.92 sQ133_spl <=> (smaller(zero,age(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1971,plain,(
% 12.29/1.92 smaller(zero,age(sK2_skl,sK6_skl))|~sQ133_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f1970])).
% 12.29/1.92 fof(f1974,definition,(
% 12.29/1.92 sQ134_spl <=> (greater(eta,age(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1977,plain,(
% 12.29/1.92 ~sQ134_spl|~sQ131_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1960,f1974,f1907])).
% 12.29/1.92 fof(f1979,definition,(
% 12.29/1.92 sQ135_spl <=> (smaller_or_equal(eta,age(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1988,plain,(
% 12.29/1.92 greater(age(sK2_skl,sK6_skl),eta)|age(sK2_skl,sK6_skl)=eta|~sQ131_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1968,f24])).
% 12.29/1.92 fof(f1989,definition,(
% 12.29/1.92 sQ136_spl <=> (greater(age(sK2_skl,sK6_skl),eta))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f1992,plain,(
% 12.29/1.92 sQ136_spl|sQ132_spl|~sQ131_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f1988,f1989,f1910,f1907])).
% 12.29/1.92 fof(f1998,plain,(
% 12.29/1.92 greater(age(sK2_skl,sK6_skl),zero)|~sQ133_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1971,f29])).
% 12.29/1.92 fof(f2001,plain,(
% 12.29/1.92 ~greater(zero,age(sK2_skl,sK6_skl))|~greater(zero,age(sK2_skl,sK6_skl))|~sQ133_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1998,f397])).
% 12.29/1.92 fof(f2009,plain,(
% 12.29/1.92 greater_or_equal(age(sK2_skl,sK6_skl),zero)|~sQ133_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1998,f25])).
% 12.29/1.92 fof(f2011,definition,(
% 12.29/1.92 sQ137_spl <=> (greater(zero,age(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2014,plain,(
% 12.29/1.92 ~sQ137_spl|~sQ133_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2001,f2011,f1970])).
% 12.29/1.92 fof(f2016,definition,(
% 12.29/1.92 sQ138_spl <=> (smaller_or_equal(zero,age(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2025,plain,(
% 12.29/1.92 greater(age(sK2_skl,sK6_skl),zero)|age(sK2_skl,sK6_skl)=zero|~sQ133_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2009,f24])).
% 12.29/1.92 fof(f2026,definition,(
% 12.29/1.92 sQ139_spl <=> (greater(age(sK2_skl,sK6_skl),zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2029,plain,(
% 12.29/1.92 sQ139_spl|sQ93_spl|~sQ133_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2025,f2026,f1273,f1970])).
% 12.29/1.92 fof(f2062,plain,(
% 12.29/1.92 hazard_of_mortality(sK2_skl,sK3_skl)=hazard_of_mortality(sK2_skl,sK4_skl)|~sQ28_spl|~sQ26_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f337,f317])).
% 12.29/1.92 fof(f2064,plain,(
% 12.29/1.92 $false|sQ2_spl|~sQ28_spl|~sQ26_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f2062,f91])).
% 12.29/1.92 fof(f2065,plain,(
% 12.29/1.92 sQ2_spl|~sQ28_spl|~sQ26_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f2064])).
% 12.29/1.92 fof(f2074,plain,(
% 12.29/1.92 has_immunity(sK2_skl,sK6_skl)|smaller(capability(sK2_skl,sK5_skl),capability(sK2_skl,sK6_skl))|capability(sK2_skl,sK5_skl)=capability(sK2_skl,sK6_skl)|sQ0_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f85,f578])).
% 12.29/1.92 fof(f2077,plain,(
% 12.29/1.92 ![X0]: (~greater(hazard_of_mortality(sK2_skl,sK6_skl),X0)|~greater(X0,hazard_of_mortality(sK2_skl,sK5_skl))|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f85,f35])).
% 12.29/1.92 fof(f2078,definition,(
% 12.29/1.92 sQ142_spl <=> (has_immunity(sK2_skl,sK6_skl))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2079,plain,(
% 12.29/1.92 has_immunity(sK2_skl,sK6_skl)|~sQ142_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2078])).
% 12.29/1.92 fof(f2081,definition,(
% 12.29/1.92 sQ143_spl <=> (smaller(capability(sK2_skl,sK5_skl),capability(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2082,plain,(
% 12.29/1.92 smaller(capability(sK2_skl,sK5_skl),capability(sK2_skl,sK6_skl))|~sQ143_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2081])).
% 12.29/1.92 fof(f2084,definition,(
% 12.29/1.92 sQ144_spl <=> (capability(sK2_skl,sK5_skl)=capability(sK2_skl,sK6_skl))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2085,plain,(
% 12.29/1.92 capability(sK2_skl,sK5_skl)=capability(sK2_skl,sK6_skl)|~sQ144_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2084])).
% 12.29/1.92 fof(f2087,plain,(
% 12.29/1.92 sQ142_spl|sQ143_spl|sQ144_spl|sQ0_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2074,f2078,f2081,f2084,f83])).
% 12.29/1.92 fof(f2108,plain,(
% 12.29/1.92 ~has_endowment(sK2_skl)|~greater(age(sK2_skl,sK6_skl),eta)|~sQ142_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2079,f43])).
% 12.29/1.92 fof(f2117,plain,(
% 12.29/1.92 ~sQ10_spl|~sQ136_spl|~sQ142_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2108,f157,f1989,f2078])).
% 12.29/1.92 fof(f2135,plain,(
% 12.29/1.92 has_immunity(sK2_skl,sK4_skl)|greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ30_spl|~sQ28_spl|~sQ26_spl),
% 12.29/1.92 inference(paramodulation,[status(thm)],[f2062,f350])).
% 12.29/1.92 fof(f2136,definition,(
% 12.29/1.92 sQ151_spl <=> (greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK3_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2137,plain,(
% 12.29/1.92 greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ151_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2136])).
% 12.29/1.92 fof(f2144,definition,(
% 12.29/1.92 sQ152_spl <=> (greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2148,plain,(
% 12.29/1.92 sQ62_spl|sQ151_spl|~sQ30_spl|~sQ28_spl|~sQ26_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2135,f699,f2136,f349,f336,f316])).
% 12.29/1.92 fof(f2156,plain,(
% 12.29/1.92 ![X0]: (~greater(hazard_of_mortality(sK2_skl,sK6_skl),hazard_of_mortality(sK2_skl,X0))|has_immunity(sK2_skl,X0)|smaller(capability(sK2_skl,sK5_skl),capability(sK2_skl,X0))|capability(sK2_skl,sK5_skl)=capability(sK2_skl,X0)|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2077,f578])).
% 12.29/1.92 fof(f2158,plain,(
% 12.29/1.92 ![X0]: (~greater(hazard_of_mortality(sK2_skl,sK6_skl),X0)|smaller(X0,hazard_of_mortality(sK2_skl,sK5_skl))|X0=hazard_of_mortality(sK2_skl,sK5_skl)|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2077,f36])).
% 12.29/1.92 fof(f2159,plain,(
% 12.29/1.92 ![X0,X1]: (~greater(hazard_of_mortality(sK2_skl,sK6_skl),X0)|~greater(X0,X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2077,f35])).
% 12.29/1.92 fof(f2160,plain,(
% 12.29/1.92 smaller(zero,age(sK2_skl,sK6_skl))|zero=age(sK2_skl,sK6_skl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f548,f79])).
% 12.29/1.92 fof(f2164,plain,(
% 12.29/1.92 sQ133_spl|sQ93_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2160,f1970,f1273])).
% 12.29/1.92 fof(f2165,plain,(
% 12.29/1.92 eta=age(sK2_skl,sK6_skl)|smaller_or_equal(eta,age(sK2_skl,sK6_skl))),
% 12.29/1.92 inference(resolution,[status(thm)],[f659,f79])).
% 12.29/1.92 fof(f2169,plain,(
% 12.29/1.92 sQ132_spl|sQ135_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2165,f1910,f1979])).
% 12.29/1.92 fof(f2170,plain,(
% 12.29/1.92 zero=age(sK2_skl,sK6_skl)|smaller_or_equal(zero,age(sK2_skl,sK6_skl))),
% 12.29/1.92 inference(resolution,[status(thm)],[f662,f79])).
% 12.29/1.92 fof(f2174,plain,(
% 12.29/1.92 sQ93_spl|sQ138_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2170,f1273,f2016])).
% 12.29/1.92 fof(f2180,plain,(
% 12.29/1.92 ![X0]: (zero=X0|smaller_or_equal(zero,X0)|smaller(X0,eta)|X0=eta)),
% 12.29/1.92 inference(resolution,[status(thm)],[f663,f36])).
% 12.29/1.92 fof(f2189,plain,(
% 12.29/1.92 ![X0]: (smaller(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK5_skl))|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK5_skl)|has_immunity(sK2_skl,sK6_skl)|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2158,f578])).
% 12.29/1.92 fof(f2193,definition,(
% 12.29/1.92 sQ153_spl <=> (smaller(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2196,definition,(
% 12.29/1.92 sQ154_spl <=> (hazard_of_mortality(sK2_skl,sK3_skl)=hazard_of_mortality(sK2_skl,sK5_skl))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2197,plain,(
% 12.29/1.92 hazard_of_mortality(sK2_skl,sK3_skl)=hazard_of_mortality(sK2_skl,sK5_skl)|~sQ154_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2196])).
% 12.29/1.92 fof(f2200,definition,(
% 12.29/1.92 ![X0]: (sQ155_spl <=> (smaller(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK5_skl))|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK5_skl)|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2203,plain,(
% 12.29/1.92 sQ155_spl|sQ142_spl|sQ0_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2189,f2200,f2078,f83])).
% 12.29/1.92 fof(f2204,plain,(
% 12.29/1.92 ~greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ28_spl|~sQ26_spl|sQ1_spl),
% 12.29/1.92 inference(forward_demodulation,[status(thm)],[f2062,f88])).
% 12.29/1.92 fof(f2205,plain,(
% 12.29/1.92 has_immunity(sK2_skl,sK5_skl)|~sQ28_spl|~sQ26_spl|sQ1_spl|~sQ30_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2204,f350])).
% 12.29/1.92 fof(f2210,plain,(
% 12.29/1.92 sQ24_spl|~sQ28_spl|~sQ26_spl|sQ1_spl|~sQ30_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2205,f309,f336,f316,f86,f349])).
% 12.29/1.92 fof(f2222,definition,(
% 12.29/1.92 sQ159_spl <=> (smaller(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2223,plain,(
% 12.29/1.92 smaller(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ159_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2222])).
% 12.29/1.92 fof(f2224,plain,(
% 12.29/1.92 ~smaller(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl))|sQ159_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2222])).
% 12.29/1.92 fof(f2226,plain,(
% 12.29/1.92 greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(forward_demodulation,[status(thm)],[f2062,f87])).
% 12.29/1.92 fof(f2227,plain,(
% 12.29/1.92 has_immunity(sK2_skl,sK5_skl)|greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ30_spl|~sQ154_spl),
% 12.29/1.92 inference(paramodulation,[status(thm)],[f2197,f350])).
% 12.29/1.92 fof(f2230,plain,(
% 12.29/1.92 sQ24_spl|sQ151_spl|~sQ30_spl|~sQ154_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2227,f309,f2136,f349,f2196])).
% 12.29/1.92 fof(f2235,plain,(
% 12.29/1.92 $false|~sQ151_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f2137,f406])).
% 12.29/1.92 fof(f2236,plain,(
% 12.29/1.92 ~sQ151_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f2235])).
% 12.29/1.92 fof(f2252,plain,(
% 12.29/1.92 ~greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl))|~greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl))|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2226,f397])).
% 12.29/1.92 fof(f2256,plain,(
% 12.29/1.92 hazard_of_mortality(sK2_skl,sK3_skl)=hazard_of_mortality(sK2_skl,sK5_skl)|smaller_or_equal(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl))|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2226,f671])).
% 12.29/1.92 fof(f2260,plain,(
% 12.29/1.92 greater_or_equal(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2226,f25])).
% 12.29/1.92 fof(f2261,plain,(
% 12.29/1.92 ~greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl))|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2226,f32])).
% 12.29/1.92 fof(f2262,definition,(
% 12.29/1.92 sQ161_spl <=> (greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2265,plain,(
% 12.29/1.92 ~sQ161_spl|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2252,f2262,f336,f316,f86])).
% 12.29/1.92 fof(f2267,definition,(
% 12.29/1.92 sQ162_spl <=> (smaller_or_equal(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2270,plain,(
% 12.29/1.92 sQ154_spl|sQ162_spl|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2256,f2196,f2267,f336,f316,f86])).
% 12.29/1.92 fof(f2275,plain,(
% 12.29/1.92 smaller(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl))|hazard_of_mortality(sK2_skl,sK3_skl)=hazard_of_mortality(sK2_skl,sK5_skl)|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2261,f36])).
% 12.29/1.92 fof(f2282,plain,(
% 12.29/1.92 sQ153_spl|sQ154_spl|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2275,f2193,f2196,f336,f316,f86])).
% 12.29/1.92 fof(f2290,plain,(
% 12.29/1.92 greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl))|hazard_of_mortality(sK2_skl,sK5_skl)=hazard_of_mortality(sK2_skl,sK3_skl)|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2260,f24])).
% 12.29/1.92 fof(f2291,plain,(
% 12.29/1.92 sQ152_spl|sQ154_spl|~sQ28_spl|~sQ26_spl|~sQ1_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2290,f2144,f2196,f336,f316,f86])).
% 12.29/1.92 fof(f2472,plain,(
% 12.29/1.92 is_aligned(sK2_skl,sK5_skl)|~sQ74_spl|sQ66_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1045,f873])).
% 12.29/1.92 fof(f2486,plain,(
% 12.29/1.92 ![X0,X1]: (is_aligned(sK2_skl,X0)|~greater(sigma,X1)|~greater(X1,age(sK2_skl,X0))|~sQ74_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1045,f97])).
% 12.29/1.92 fof(f2488,plain,(
% 12.29/1.92 ![X0]: (is_aligned(sK2_skl,X0)|smaller(sigma,age(sK2_skl,X0))|~sQ74_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1045,f30])).
% 12.29/1.92 fof(f2493,plain,(
% 12.29/1.92 sQ115_spl|~sQ74_spl|sQ66_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2472,f1616,f1044,f871])).
% 12.29/1.92 fof(f2530,plain,(
% 12.29/1.92 $false|~sQ56_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f648,f406])).
% 12.29/1.92 fof(f2531,plain,(
% 12.29/1.92 ~sQ56_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f2530])).
% 12.29/1.92 fof(f2548,definition,(
% 12.29/1.92 sQ168_spl <=> (sigma=sigma)),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2555,definition,(
% 12.29/1.92 sQ170_spl <=> (smaller(sigma,sigma))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2556,plain,(
% 12.29/1.92 smaller(sigma,sigma)|~sQ170_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2555])).
% 12.29/1.92 fof(f2557,plain,(
% 12.29/1.92 ~smaller(sigma,sigma)|sQ170_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2555])).
% 12.29/1.92 fof(f2618,definition,(
% 12.29/1.92 sQ172_spl <=> (age(sK2_skl,sK4_skl)=sigma)),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f2619,plain,(
% 12.29/1.92 age(sK2_skl,sK4_skl)=sigma|~sQ172_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f2618])).
% 12.29/1.92 fof(f2650,plain,(
% 12.29/1.92 ~greater(sigma,eta)|~sQ172_spl|sQ29_spl),
% 12.29/1.92 inference(backward_demodulation,[status(thm)],[f2619,f342])).
% 12.29/1.92 fof(f2659,plain,(
% 12.29/1.92 $false|~sQ172_spl|sQ29_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f2650,f80])).
% 12.29/1.92 fof(f2660,plain,(
% 12.29/1.92 ~sQ172_spl|sQ29_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f2659])).
% 12.29/1.92 fof(f2673,plain,(
% 12.29/1.92 ![X0]: (~is_aligned(sK2_skl,X0)|~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,sK4_skl),sigma)|~sQ123_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1691,f362])).
% 12.29/1.92 fof(f2677,plain,(
% 12.29/1.92 sQ73_spl|~sQ122_spl|~sQ123_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f2673,f1040,f1674,f1678])).
% 12.29/1.92 fof(f2861,definition,(
% 12.29/1.92 ![X0]: (sQ180_spl <=> (~greater(X0,hazard_of_mortality(sK2_skl,sK5_skl))|~greater(hazard_of_mortality(sK2_skl,sK3_skl),X0)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3015,plain,(
% 12.29/1.92 greater(capability(sK2_skl,sK6_skl),capability(sK2_skl,sK5_skl))|~sQ143_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2082,f29])).
% 12.29/1.92 fof(f3066,plain,(
% 12.29/1.92 is_aligned(sK2_skl,sK5_skl)|smaller(sigma,sigma)|~sQ74_spl|~sQ17_spl),
% 12.29/1.92 inference(paramodulation,[status(thm)],[f213,f2488])).
% 12.29/1.92 fof(f3068,plain,(
% 12.29/1.92 sQ115_spl|sQ170_spl|~sQ74_spl|~sQ17_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3066,f1616,f2555,f1044,f212])).
% 12.29/1.92 fof(f3069,definition,(
% 12.29/1.92 sQ198_spl <=> (smaller(sigma,zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3070,plain,(
% 12.29/1.92 smaller(sigma,zero)|~sQ198_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f3069])).
% 12.29/1.92 fof(f3084,plain,(
% 12.29/1.92 ~greater(sigma,eta)|is_aligned(sK2_skl,sK4_skl)|sQ29_spl|~sQ74_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f570,f1045])).
% 12.29/1.92 fof(f3088,plain,(
% 12.29/1.92 ~sQ15_spl|sQ123_spl|sQ29_spl|~sQ74_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3084,f195,f1678,f340,f1044])).
% 12.29/1.92 fof(f3107,definition,(
% 12.29/1.92 sQ201_spl <=> (greater_or_equal(eta,sigma))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3108,plain,(
% 12.29/1.92 greater_or_equal(eta,sigma)|~sQ201_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f3107])).
% 12.29/1.92 fof(f3111,definition,(
% 12.29/1.92 sQ202_spl <=> (smaller(sigma,eta))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3112,plain,(
% 12.29/1.92 smaller(sigma,eta)|~sQ202_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f3111])).
% 12.29/1.92 fof(f3113,plain,(
% 12.29/1.92 ~smaller(sigma,eta)|sQ202_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f3111])).
% 12.29/1.92 fof(f3163,plain,(
% 12.29/1.92 ~greater(capability(sK2_skl,sK5_skl),capability(sK2_skl,sK6_skl))|~sQ143_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f3015,f32])).
% 12.29/1.92 fof(f3197,definition,(
% 12.29/1.92 sQ209_spl <=> (age(sK2_skl,sK3_skl)=sigma)),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3198,plain,(
% 12.29/1.92 age(sK2_skl,sK3_skl)=sigma|~sQ209_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f3197])).
% 12.29/1.92 fof(f3249,definition,(
% 12.29/1.92 sQ210_spl <=> (smaller_or_equal(sigma,zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3250,plain,(
% 12.29/1.92 smaller_or_equal(sigma,zero)|~sQ210_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f3249])).
% 12.29/1.92 fof(f3251,plain,(
% 12.29/1.92 ~smaller_or_equal(sigma,zero)|sQ210_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f3249])).
% 12.29/1.92 fof(f3266,plain,(
% 12.29/1.92 ![X0,X1]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,sK4_skl),X1)|smaller(X1,sigma)|X1=sigma|~is_aligned(sK2_skl,X0)|~sQ123_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1326,f1691])).
% 12.29/1.92 fof(f3267,plain,(
% 12.29/1.92 ![X0,X1]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,sK3_skl),X1)|smaller(X1,sigma)|X1=sigma|~is_aligned(sK2_skl,X0)|~sQ103_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1326,f1355])).
% 12.29/1.92 fof(f3268,plain,(
% 12.29/1.92 ![X0,X1,X2]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,X1),X2)|smaller(X2,sigma)|X2=sigma|~is_aligned(sK2_skl,X0)|~age(sK2_skl,X1)=zero)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1326,f233])).
% 12.29/1.92 fof(f3269,plain,(
% 12.29/1.92 ![X0,X1,X2]: (~age(sK2_skl,X0)=zero|~greater(age(sK2_skl,X1),X2)|smaller(X2,sigma)|X2=sigma|~age(sK2_skl,X0)=zero|greater(age(sK2_skl,X1),sigma))),
% 12.29/1.92 inference(resolution,[status(thm)],[f1326,f220])).
% 12.29/1.92 fof(f3279,definition,(
% 12.29/1.92 ![X1]: (sQ212_spl <=> (~greater(age(sK2_skl,sK4_skl),X1)|smaller(X1,sigma)|X1=sigma))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3282,plain,(
% 12.29/1.92 sQ73_spl|sQ212_spl|~sQ123_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3266,f1040,f3279,f1678])).
% 12.29/1.92 fof(f3283,definition,(
% 12.29/1.92 ![X1]: (sQ213_spl <=> (~greater(age(sK2_skl,sK3_skl),X1)|smaller(X1,sigma)|X1=sigma))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3286,plain,(
% 12.29/1.92 sQ73_spl|sQ213_spl|~sQ103_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3267,f1040,f3283,f1340])).
% 12.29/1.92 fof(f3287,definition,(
% 12.29/1.92 ![X1,X2]: (sQ214_spl <=> (~greater(age(sK2_skl,X1),X2)|smaller(X2,sigma)|X2=sigma|~age(sK2_skl,X1)=zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3290,plain,(
% 12.29/1.92 sQ73_spl|sQ214_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3268,f1040,f3287])).
% 12.29/1.92 fof(f3291,definition,(
% 12.29/1.92 ![X1,X2]: (sQ215_spl <=> (~greater(age(sK2_skl,X1),X2)|smaller(X2,sigma)|X2=sigma|greater(age(sK2_skl,X1),sigma)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3294,plain,(
% 12.29/1.92 sQ75_spl|sQ215_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3269,f1047,f3291])).
% 12.29/1.92 fof(f3389,plain,(
% 12.29/1.92 ![X0]: (~dissimilar(sK2_skl,X0,sK6_skl)|~age(sK2_skl,X0)=zero|~sQ94_spl|~sQ72_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1286,f1038])).
% 12.29/1.92 fof(f3391,plain,(
% 12.29/1.92 ![X0]: (~age(sK2_skl,X0)=zero|~sQ94_spl|~sQ72_spl)),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f3389,f558])).
% 12.29/1.92 fof(f3392,definition,(
% 12.29/1.92 ![X0]: (sQ221_spl <=> (~dissimilar(sK2_skl,X0,sK6_skl)|~age(sK2_skl,X0)=zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3393,plain,(
% 12.29/1.92 ![X0]: (~dissimilar(sK2_skl,X0,sK6_skl)|~age(sK2_skl,X0)=zero|~sQ221_spl)),
% 12.29/1.92 inference(component_clause,[status(thm)],[f3392])).
% 12.29/1.92 fof(f3423,plain,(
% 12.29/1.92 ![X0]: (~age(sK2_skl,X0)=zero|~sQ221_spl)),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f3393,f558])).
% 12.29/1.92 fof(f3424,plain,(
% 12.29/1.92 sQ78_spl|~sQ94_spl|~sQ72_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3391,f1058,f1278,f1037])).
% 12.29/1.92 fof(f3448,plain,(
% 12.29/1.92 ![X0,X1]: (is_aligned(sK2_skl,X0)|~age(sK2_skl,X1)=zero|is_aligned(sK2_skl,X1)|~age(sK2_skl,X0)=zero)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1410,f576])).
% 12.29/1.92 fof(f3453,plain,(
% 12.29/1.92 sQ72_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3448,f1037])).
% 12.29/1.92 fof(f3460,plain,(
% 12.29/1.92 ![X0]: (smaller(zero,X0)|zero=X0|X0=eta|greater(eta,X0))),
% 12.29/1.92 inference(resolution,[status(thm)],[f1502,f29])).
% 12.29/1.92 fof(f3464,plain,(
% 12.29/1.92 greater(sigma,sigma)|~sQ170_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2556,f29])).
% 12.29/1.92 fof(f3466,plain,(
% 12.29/1.92 sQ56_spl|~sQ170_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3464,f647,f2555])).
% 12.29/1.92 fof(f3521,plain,(
% 12.29/1.92 smaller(sigma,sigma)|sigma=sigma|sQ170_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2557,f141])).
% 12.29/1.92 fof(f3527,plain,(
% 12.29/1.92 sQ170_spl|sQ168_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3521,f2555,f2548])).
% 12.29/1.92 fof(f3634,plain,(
% 12.29/1.92 ![X0]: (is_aligned(sK2_skl,sK6_skl)|~age(sK2_skl,X0)=zero|has_immunity(sK2_skl,sK6_skl)|smaller(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK5_skl))|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK5_skl)|~sQ110_spl|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1412,f2158])).
% 12.29/1.92 fof(f3665,definition,(
% 12.29/1.92 ![X0]: (sQ230_spl <=> (~age(sK2_skl,X0)=zero|smaller(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK5_skl))|hazard_of_mortality(sK2_skl,X0)=hazard_of_mortality(sK2_skl,sK5_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3668,plain,(
% 12.29/1.92 sQ94_spl|sQ230_spl|sQ142_spl|~sQ110_spl|sQ0_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3634,f1278,f3665,f2078,f1411,f83])).
% 12.29/1.92 fof(f3685,definition,(
% 12.29/1.92 ![X0]: (sQ235_spl <=> (is_aligned(sK2_skl,X0)|has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK3_skl))))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3823,plain,(
% 12.29/1.92 greater(eta,sigma)|~sQ202_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f3112,f29])).
% 12.29/1.92 fof(f3825,plain,(
% 12.29/1.92 $false|~sQ202_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f3823,f96])).
% 12.29/1.92 fof(f3826,plain,(
% 12.29/1.92 ~sQ202_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f3825])).
% 12.29/1.92 fof(f3827,plain,(
% 12.29/1.92 greater(eta,sigma)|eta=sigma|~sQ201_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f3108,f24])).
% 12.29/1.92 fof(f3828,plain,(
% 12.29/1.92 sQ53_spl|sQ9_spl|~sQ201_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3827,f596,f151,f3107])).
% 12.29/1.92 fof(f3830,plain,(
% 12.29/1.92 ![X0,X1]: (~greater(eta,X0)|~greater(X0,X1)|~greater(X1,sigma)|sigma=eta|sQ202_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f3113,f846])).
% 12.29/1.92 fof(f3836,definition,(
% 12.29/1.92 ![X0,X1]: (sQ246_spl <=> (~greater(eta,X0)|~greater(X0,X1)|~greater(X1,sigma)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f3839,plain,(
% 12.29/1.92 sQ246_spl|sQ9_spl|sQ202_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3830,f3836,f151,f3111])).
% 12.29/1.92 fof(f4055,definition,(
% 12.29/1.92 ![X0]: (sQ253_spl <=> (smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)|~greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK5_skl))))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f4150,plain,(
% 12.29/1.92 ![X0,X1,X2]: (~greater(hazard_of_mortality(sK2_skl,sK6_skl),X0)|~greater(X0,X1)|~greater(X1,X2)|~greater(X2,hazard_of_mortality(sK2_skl,sK5_skl))|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2159,f35])).
% 12.29/1.92 fof(f4264,plain,(
% 12.29/1.92 zero=sigma|~sQ209_spl),
% 12.29/1.92 inference(forward_demodulation,[status(thm)],[f75,f3198])).
% 12.29/1.92 fof(f4265,plain,(
% 12.29/1.92 $false|sQ19_spl|~sQ209_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f4264,f254])).
% 12.29/1.92 fof(f4266,plain,(
% 12.29/1.92 sQ19_spl|~sQ209_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f4265])).
% 12.29/1.92 fof(f4267,plain,(
% 12.29/1.92 sQ78_spl|~sQ221_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f3423,f1058,f3392])).
% 12.29/1.92 fof(f4273,plain,(
% 12.29/1.92 ![X0]: (~age(sK2_skl,X0)=zero|~sQ82_spl|~sQ87_spl)),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f1129,f1104])).
% 12.29/1.92 fof(f4276,plain,(
% 12.29/1.92 greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK5_skl))|~sQ159_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f2223,f29])).
% 12.29/1.92 fof(f4278,plain,(
% 12.29/1.92 $false|~sQ28_spl|~sQ26_spl|~sQ1_spl|~sQ159_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f4276,f2261])).
% 12.29/1.92 fof(f4279,plain,(
% 12.29/1.92 ~sQ28_spl|~sQ26_spl|~sQ1_spl|~sQ159_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f4278])).
% 12.29/1.92 fof(f4280,plain,(
% 12.29/1.92 ![X0,X1]: (~greater(hazard_of_mortality(sK2_skl,sK3_skl),X0)|~greater(X0,X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))|hazard_of_mortality(sK2_skl,sK5_skl)=hazard_of_mortality(sK2_skl,sK3_skl)|sQ159_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2224,f846])).
% 12.29/1.92 fof(f4285,definition,(
% 12.29/1.92 ![X0,X1]: (sQ257_spl <=> (~greater(hazard_of_mortality(sK2_skl,sK3_skl),X0)|~greater(X0,X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f4288,plain,(
% 12.29/1.92 sQ257_spl|sQ154_spl|sQ159_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f4280,f4285,f2196,f2222])).
% 12.29/1.92 fof(f4305,plain,(
% 12.29/1.92 smaller(sigma,zero)|sigma=zero|~sQ210_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f3250,f19])).
% 12.29/1.92 fof(f4306,plain,(
% 12.29/1.92 sQ198_spl|sQ19_spl|~sQ210_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f4305,f3069,f252,f3249])).
% 12.29/1.92 fof(f4447,plain,(
% 12.29/1.92 greater(zero,sigma)|~sQ198_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f3070,f29])).
% 12.29/1.92 fof(f4449,plain,(
% 12.29/1.92 $false|~sQ198_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f4447,f244])).
% 12.29/1.92 fof(f4450,plain,(
% 12.29/1.92 ~sQ198_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f4449])).
% 12.29/1.92 fof(f4461,definition,(
% 12.29/1.92 ![X0,X1]: (sQ274_spl <=> (~greater(zero,X0)|~greater(X0,X1)|~greater(X1,sigma)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f4675,plain,(
% 12.29/1.92 ![X0]: (has_immunity(sK2_skl,X0)|smaller(capability(sK2_skl,sK5_skl),capability(sK2_skl,X0))|capability(sK2_skl,sK5_skl)=capability(sK2_skl,X0)|is_aligned(sK2_skl,sK6_skl)|~age(sK2_skl,X0)=zero|has_immunity(sK2_skl,sK6_skl)|sQ0_spl|~sQ110_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2156,f1412])).
% 12.29/1.92 fof(f4676,plain,(
% 12.29/1.92 ![X0]: (has_immunity(sK2_skl,X0)|smaller(capability(sK2_skl,sK5_skl),capability(sK2_skl,X0))|capability(sK2_skl,sK5_skl)=capability(sK2_skl,X0)|has_immunity(sK2_skl,sK6_skl)|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2156,f578])).
% 12.29/1.92 fof(f4683,definition,(
% 12.29/1.92 ![X0]: (sQ280_spl <=> (has_immunity(sK2_skl,X0)|smaller(capability(sK2_skl,sK5_skl),capability(sK2_skl,X0))|capability(sK2_skl,sK5_skl)=capability(sK2_skl,X0)|~age(sK2_skl,X0)=zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f4686,plain,(
% 12.29/1.92 sQ280_spl|sQ94_spl|sQ142_spl|sQ0_spl|~sQ110_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f4675,f4683,f1278,f2078,f83,f1411])).
% 12.29/1.92 fof(f4687,definition,(
% 12.29/1.92 ![X0]: (sQ281_spl <=> (has_immunity(sK2_skl,X0)|smaller(capability(sK2_skl,sK5_skl),capability(sK2_skl,X0))|capability(sK2_skl,sK5_skl)=capability(sK2_skl,X0)|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f4690,plain,(
% 12.29/1.92 sQ281_spl|sQ142_spl|sQ0_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f4676,f4687,f2078,f83])).
% 12.29/1.92 fof(f4691,definition,(
% 12.29/1.92 sQ282_spl <=> (greater(hazard_of_mortality(sK2_skl,sK6_skl),hazard_of_mortality(sK2_skl,sK3_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f4692,plain,(
% 12.29/1.92 greater(hazard_of_mortality(sK2_skl,sK6_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ282_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f4691])).
% 12.29/1.92 fof(f4693,plain,(
% 12.29/1.92 ~greater(hazard_of_mortality(sK2_skl,sK6_skl),hazard_of_mortality(sK2_skl,sK3_skl))|sQ282_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f4691])).
% 12.29/1.92 fof(f4967,plain,(
% 12.29/1.92 ![X0]: (eta=X0|X0=sigma|smaller_or_equal(X0,sigma)|greater(X0,eta))),
% 12.29/1.92 inference(resolution,[status(thm)],[f1904,f29])).
% 12.29/1.92 fof(f4973,plain,(
% 12.29/1.92 ![X0]: (eta=X0|smaller(X0,sigma)|X0=sigma|greater(X0,eta))),
% 12.29/1.92 inference(resolution,[status(thm)],[f1905,f29])).
% 12.29/1.92 fof(f5018,plain,(
% 12.29/1.92 ![X0]: (zero=X0|smaller_or_equal(zero,X0)|X0=eta|greater(eta,X0))),
% 12.29/1.92 inference(resolution,[status(thm)],[f2180,f29])).
% 12.29/1.92 fof(f6096,plain,(
% 12.29/1.92 ![X0,X1]: (~greater(hazard_of_mortality(sK2_skl,sK6_skl),X0)|~greater(X0,X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2077,f35])).
% 12.29/1.92 fof(f6137,plain,(
% 12.29/1.92 sQ78_spl|~sQ82_spl|~sQ87_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f4273,f1058,f1103,f1128])).
% 12.29/1.92 fof(f6334,plain,(
% 12.29/1.92 is_aligned(sK2_skl,sK6_skl)|~age(sK2_skl,sK3_skl)=zero|has_immunity(sK2_skl,sK6_skl)|sQ282_spl|~sQ110_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f4693,f1412])).
% 12.29/1.92 fof(f6339,plain,(
% 12.29/1.92 sQ94_spl|~sQ101_spl|sQ142_spl|sQ282_spl|~sQ110_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f6334,f1278,f1332,f2078,f4691,f1411])).
% 12.29/1.92 fof(f6347,definition,(
% 12.29/1.92 sQ369_spl <=> (hazard_of_mortality(sK2_skl,sK6_skl)=hazard_of_mortality(sK2_skl,sK3_skl))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f6348,plain,(
% 12.29/1.92 hazard_of_mortality(sK2_skl,sK6_skl)=hazard_of_mortality(sK2_skl,sK3_skl)|~sQ369_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f6347])).
% 12.29/1.92 fof(f7054,plain,(
% 12.29/1.92 ![X0,X1]: (~greater(hazard_of_mortality(sK2_skl,sK6_skl),X0)|~greater(X0,X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2077,f35])).
% 12.29/1.92 fof(f7113,plain,(
% 12.29/1.92 ![X0,X1]: (~greater(hazard_of_mortality(sK2_skl,X0),X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))|is_aligned(sK2_skl,sK6_skl)|~age(sK2_skl,X0)=zero|has_immunity(sK2_skl,sK6_skl)|sQ0_spl|~sQ110_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f6096,f1412])).
% 12.29/1.92 fof(f7114,plain,(
% 12.29/1.92 ![X0,X1]: (~greater(hazard_of_mortality(sK2_skl,X0),X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))|has_immunity(sK2_skl,sK6_skl)|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f6096,f578])).
% 12.29/1.92 fof(f7120,definition,(
% 12.29/1.92 ![X0,X1]: (sQ414_spl <=> (~greater(hazard_of_mortality(sK2_skl,X0),X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))|~age(sK2_skl,X0)=zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f7123,plain,(
% 12.29/1.92 sQ414_spl|sQ94_spl|sQ142_spl|sQ0_spl|~sQ110_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f7113,f7120,f1278,f2078,f83,f1411])).
% 12.29/1.92 fof(f7124,definition,(
% 12.29/1.92 ![X0,X1]: (sQ415_spl <=> (~greater(hazard_of_mortality(sK2_skl,X0),X1)|~greater(X1,hazard_of_mortality(sK2_skl,sK5_skl))|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f7127,plain,(
% 12.29/1.92 sQ415_spl|sQ142_spl|sQ0_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f7114,f7124,f2078,f83])).
% 12.29/1.92 fof(f8541,definition,(
% 12.29/1.92 ![X0]: (sQ443_spl <=> (~greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK5_skl))|~age(sK2_skl,X0)=zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f8846,plain,(
% 12.29/1.92 ![X0,X1,X2]: (~greater(hazard_of_mortality(sK2_skl,X0),X1)|~greater(X1,X2)|~greater(X2,hazard_of_mortality(sK2_skl,sK5_skl))|is_aligned(sK2_skl,sK6_skl)|~age(sK2_skl,X0)=zero|has_immunity(sK2_skl,sK6_skl)|sQ0_spl|~sQ110_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f4150,f1412])).
% 12.29/1.92 fof(f8847,plain,(
% 12.29/1.92 ![X0,X1,X2]: (~greater(hazard_of_mortality(sK2_skl,X0),X1)|~greater(X1,X2)|~greater(X2,hazard_of_mortality(sK2_skl,sK5_skl))|has_immunity(sK2_skl,sK6_skl)|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f4150,f578])).
% 12.29/1.92 fof(f8853,definition,(
% 12.29/1.92 ![X0,X1,X2]: (sQ451_spl <=> (~greater(hazard_of_mortality(sK2_skl,X0),X1)|~greater(X1,X2)|~greater(X2,hazard_of_mortality(sK2_skl,sK5_skl))|~age(sK2_skl,X0)=zero))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ451_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f8856,plain,(
% 12.29/1.92 sQ451_spl|sQ94_spl|sQ142_spl|sQ0_spl|~sQ110_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f8846,f8853,f1278,f2078,f83,f1411])).
% 12.29/1.92 fof(f8857,definition,(
% 12.29/1.92 ![X0,X1,X2]: (sQ452_spl <=> (~greater(hazard_of_mortality(sK2_skl,X0),X1)|~greater(X1,X2)|~greater(X2,hazard_of_mortality(sK2_skl,sK5_skl))|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f8860,plain,(
% 12.29/1.92 sQ452_spl|sQ142_spl|sQ0_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f8847,f8857,f2078,f83])).
% 12.29/1.92 fof(f8946,plain,(
% 12.29/1.92 ~greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK6_skl))|~greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK6_skl))|~sQ282_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f4692,f397])).
% 12.29/1.92 fof(f8950,plain,(
% 12.29/1.92 hazard_of_mortality(sK2_skl,sK3_skl)=hazard_of_mortality(sK2_skl,sK6_skl)|smaller_or_equal(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK6_skl))|~sQ282_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f4692,f671])).
% 12.29/1.92 fof(f8962,definition,(
% 12.29/1.92 sQ456_spl <=> (greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ456_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f8972,plain,(
% 12.29/1.92 ~sQ456_spl|~sQ282_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f8946,f8962,f4691])).
% 12.29/1.92 fof(f8974,definition,(
% 12.29/1.92 sQ458_spl <=> (smaller_or_equal(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ458_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f8975,plain,(
% 12.29/1.92 smaller_or_equal(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK6_skl))|~sQ458_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f8974])).
% 12.29/1.92 fof(f8977,plain,(
% 12.29/1.92 sQ369_spl|sQ458_spl|~sQ282_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f8950,f6347,f8974,f4691])).
% 12.29/1.92 fof(f8978,plain,(
% 12.29/1.92 greater(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ369_spl|~sQ282_spl),
% 12.29/1.92 inference(backward_demodulation,[status(thm)],[f6348,f4692])).
% 12.29/1.92 fof(f9022,plain,(
% 12.29/1.92 sQ151_spl|~sQ369_spl|~sQ282_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f8978,f2136,f6347,f4691])).
% 12.29/1.92 fof(f9048,definition,(
% 12.29/1.92 sQ459_spl <=> (smaller(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK6_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ459_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f9067,plain,(
% 12.29/1.92 ![X0]: (~greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK5_skl))|is_aligned(sK2_skl,sK6_skl)|~age(sK2_skl,X0)=zero|has_immunity(sK2_skl,sK6_skl)|sQ0_spl|~sQ110_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2077,f1412])).
% 12.29/1.92 fof(f9068,plain,(
% 12.29/1.92 ![X0]: (~greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK5_skl))|has_immunity(sK2_skl,sK6_skl)|smaller(capability(sK2_skl,X0),capability(sK2_skl,sK6_skl))|capability(sK2_skl,X0)=capability(sK2_skl,sK6_skl)|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2077,f578])).
% 12.29/1.92 fof(f9074,plain,(
% 12.29/1.92 sQ443_spl|sQ94_spl|sQ142_spl|sQ0_spl|~sQ110_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f9067,f8541,f1278,f2078,f83,f1411])).
% 12.29/1.92 fof(f9075,plain,(
% 12.29/1.92 sQ253_spl|sQ142_spl|sQ0_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f9068,f4055,f2078,f83])).
% 12.29/1.92 fof(f9473,plain,(
% 12.29/1.92 ![X0]: (has_immunity(sK2_skl,sK6_skl)|~greater(hazard_of_mortality(sK2_skl,sK3_skl),X0)|~greater(X0,hazard_of_mortality(sK2_skl,sK5_skl))|~sQ30_spl|sQ0_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f350,f7054])).
% 12.29/1.92 fof(f9510,plain,(
% 12.29/1.92 sQ142_spl|sQ180_spl|~sQ30_spl|sQ0_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f9473,f2078,f2861,f349,f83])).
% 12.29/1.92 fof(f9591,plain,(
% 12.29/1.92 smaller(hazard_of_mortality(sK2_skl,sK3_skl),hazard_of_mortality(sK2_skl,sK6_skl))|hazard_of_mortality(sK2_skl,sK3_skl)=hazard_of_mortality(sK2_skl,sK6_skl)|~sQ458_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f8975,f19])).
% 12.29/1.92 fof(f9592,plain,(
% 12.29/1.92 sQ459_spl|sQ369_spl|~sQ458_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f9591,f9048,f6347,f8974])).
% 12.29/1.92 fof(f9868,plain,(
% 12.29/1.92 eta=zero|zero=sigma|smaller_or_equal(zero,sigma)),
% 12.29/1.92 inference(resolution,[status(thm)],[f4967,f95])).
% 12.29/1.92 fof(f9937,plain,(
% 12.29/1.92 sQ4_spl|sQ19_spl|sQ60_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f9868,f112,f252,f684])).
% 12.29/1.92 fof(f9977,plain,(
% 12.29/1.92 eta=zero|smaller(zero,sigma)|zero=sigma),
% 12.29/1.92 inference(resolution,[status(thm)],[f4973,f95])).
% 12.29/1.92 fof(f10034,plain,(
% 12.29/1.92 sQ4_spl|sQ18_spl|sQ19_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f9977,f112,f249,f252])).
% 12.29/1.92 fof(f11379,plain,(
% 12.29/1.92 ![X0]: (is_aligned(sK2_skl,X0)|~organization(sK2_skl)|has_immunity(sK2_skl,X0)|greater(hazard_of_mortality(sK2_skl,X0),hazard_of_mortality(sK2_skl,sK3_skl))|~sQ104_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f1357,f287])).
% 12.29/1.92 fof(f11408,plain,(
% 12.29/1.92 sQ235_spl|~sQ21_spl|~sQ104_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f11379,f3685,f299,f1356])).
% 12.29/1.92 fof(f11424,plain,(
% 12.29/1.92 ![X0,X1]: (~greater(zero,X0)|~greater(X0,X1)|~greater(X1,sigma)|sigma=zero|sQ210_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f844,f3251])).
% 12.29/1.92 fof(f11429,plain,(
% 12.29/1.92 sQ274_spl|sQ19_spl|sQ210_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f11424,f4461,f252,f3249])).
% 12.29/1.92 fof(f11595,plain,(
% 12.29/1.92 ![X0]: (is_aligned(sK2_skl,X0)|~greater(sigma,eta)|zero=age(sK2_skl,X0)|smaller_or_equal(zero,age(sK2_skl,X0))|age(sK2_skl,X0)=eta|~sQ74_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2486,f5018])).
% 12.29/1.92 fof(f11596,plain,(
% 12.29/1.92 ![X0]: (is_aligned(sK2_skl,X0)|~greater(sigma,eta)|smaller(zero,age(sK2_skl,X0))|zero=age(sK2_skl,X0)|age(sK2_skl,X0)=eta|~sQ74_spl)),
% 12.29/1.92 inference(resolution,[status(thm)],[f2486,f3460])).
% 12.29/1.92 fof(f11620,definition,(
% 12.29/1.92 ![X0]: (sQ523_spl <=> (is_aligned(sK2_skl,X0)|zero=age(sK2_skl,X0)|smaller_or_equal(zero,age(sK2_skl,X0))|age(sK2_skl,X0)=eta))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f11623,plain,(
% 12.29/1.92 sQ523_spl|~sQ15_spl|~sQ74_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f11595,f11620,f195,f1044])).
% 12.29/1.92 fof(f11624,definition,(
% 12.29/1.92 ![X0]: (sQ524_spl <=> (is_aligned(sK2_skl,X0)|smaller(zero,age(sK2_skl,X0))|zero=age(sK2_skl,X0)|age(sK2_skl,X0)=eta))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ524_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f11627,plain,(
% 12.29/1.92 sQ524_spl|~sQ15_spl|~sQ74_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f11596,f11624,f195,f1044])).
% 12.29/1.92 fof(f11635,plain,(
% 12.29/1.92 is_aligned(sK2_skl,sK6_skl)|~sQ116_spl|~sQ143_spl),
% 12.29/1.92 inference(resolution,[status(thm)],[f1626,f3163])).
% 12.29/1.92 fof(f11667,plain,(
% 12.29/1.92 sQ94_spl|~sQ116_spl|~sQ143_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f11635,f1278,f1625,f2081])).
% 12.29/1.92 fof(f11673,definition,(
% 12.29/1.92 sQ526_spl <=> (greater(capability(sK2_skl,sK5_skl),capability(sK2_skl,sK5_skl)))),
% 12.29/1.92 introduced(definition,[new_symbols(definition,[sQ526_spl])],[split_symbol_definition])).
% 12.29/1.92 fof(f11674,plain,(
% 12.29/1.92 greater(capability(sK2_skl,sK5_skl),capability(sK2_skl,sK5_skl))|~sQ526_spl),
% 12.29/1.92 inference(component_clause,[status(thm)],[f11673])).
% 12.29/1.92 fof(f11701,plain,(
% 12.29/1.92 is_aligned(sK2_skl,sK6_skl)|greater(capability(sK2_skl,sK5_skl),capability(sK2_skl,sK5_skl))|~sQ116_spl|~sQ144_spl),
% 12.29/1.92 inference(paramodulation,[status(thm)],[f2085,f1626])).
% 12.29/1.92 fof(f11730,plain,(
% 12.29/1.92 sQ94_spl|sQ526_spl|~sQ116_spl|~sQ144_spl),
% 12.29/1.92 inference(split_clause,[status(thm)],[f11701,f1278,f11673,f1625,f2084])).
% 12.29/1.92 fof(f11800,plain,(
% 12.29/1.92 $false|~sQ526_spl),
% 12.29/1.92 inference(forward_subsumption_resolution,[status(thm)],[f11674,f406])).
% 12.29/1.92 fof(f11801,plain,(
% 12.29/1.92 ~sQ526_spl),
% 12.29/1.92 inference(contradiction_clause,[status(thm)],[f11800])).
% 12.29/1.92 fof(f11802,plain,(
% 12.29/1.92 $false),
% 12.29/1.92 inference(sat_refutation,[status(thm)],[f92,f115,f137,f147,f154,f198,f215,f231,f268,f319,f321,f323,f335,f339,f343,f345,f352,f356,f360,f380,f417,f430,f490,f498,f513,f528,f534,f545,f604,f679,f683,f690,f785,f874,f875,f876,f880,f884,f888,f1091,f1096,f1106,f1110,f1140,f1169,f1174,f1189,f1221,f1225,f1300,f1310,f1316,f1339,f1347,f1350,f1359,f1363,f1367,f1369,f1386,f1390,f1394,f1414,f1434,f1455,f1465,f1478,f1486,f1518,f1534,f1628,f1658,f1677,f1695,f1699,f1703,f1711,f1717,f1743,f1913,f1926,f1977,f1992,f2014,f2029,f2065,f2087,f2117,f2148,f2164,f2169,f2174,f2203,f2210,f2230,f2236,f2265,f2270,f2282,f2291,f2493,f2531,f2660,f2677,f3068,f3088,f3282,f3286,f3290,f3294,f3424,f3453,f3466,f3527,f3668,f3826,f3828,f3839,f4266,f4267,f4279,f4288,f4306,f4450,f4686,f4690,f6137,f6339,f7123,f7127,f8856,f8860,f8972,f8977,f9022,f9074,f9075,f9510,f9592,f9937,f10034,f11408,f11429,f11623,f11627,f11667,f11730,f11801])).
% 12.29/1.92 % SZS output end CNFRefutation for theBenchmark.p
% 12.29/1.93 % Elapsed time: 1.622517 seconds
% 12.29/1.93 % CPU time: 12.614956 seconds
% 12.29/1.93 % Total memory used: 202.289 MB
% 12.29/1.93 % Net memory used: 183.990 MB
%------------------------------------------------------------------------------