%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT063+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 : n010.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:52 PM UTC 2026
% Result : Theorem 62.73s 8.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT063+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n010.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 01:24:55 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 62.73/8.32 % Refutation found
% 62.73/8.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 62.73/8.32 % SZS output start CNFRefutation for theBenchmark
% 62.73/8.32 fof(f1,axiom,(
% 62.73/8.32 (! [X,Y] :( smaller_or_equal(X,Y)<=> ( smaller(X,Y)| X = Y ) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f2,axiom,(
% 62.73/8.32 (! [X,Y] :( greater_or_equal(X,Y)<=> ( greater(X,Y)| X = Y ) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f3,axiom,(
% 62.73/8.32 (! [X,Y] :( smaller(X,Y)<=> greater(Y,X) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f4,axiom,(
% 62.73/8.32 (! [X,Y] :~ ( greater(X,Y)& greater(Y,X) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f5,axiom,(
% 62.73/8.32 (! [X,Y,Z] :( ( greater(X,Y)& greater(Y,Z) )=> greater(X,Z) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f6,axiom,(
% 62.73/8.32 (! [X,Y] :( smaller(X,Y)| X = Y| greater(X,Y) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f8,axiom,(
% 62.73/8.32 (! [X,T] :( ( organization(X)& ~ has_endowment(X) )=> ~ has_immunity(X,T) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f9,axiom,(
% 62.73/8.32 (! [X,T0,T] :( dissimilar(X,T0,T)<=> ( organization(X)& ~ ( is_aligned(X,T0)<=> is_aligned(X,T) ) ) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f10,axiom,(
% 62.73/8.32 (! [X,T] :( ( organization(X)& age(X,T) = zero )=> is_aligned(X,T) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f11,axiom,(
% 62.73/8.32 (! [X,T0,T] :( ( organization(X)& age(X,T0) = zero )=> ( greater(age(X,T),sigma)<=> dissimilar(X,T0,T) ) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f12,axiom,(
% 62.73/8.32 (! [X] :( robust_position(X)<=> (! [T] :( ( smaller_or_equal(age(X,T),tau)=> ~ positional_advantage(X,T) )& ( greater(age(X,T),tau)=> positional_advantage(X,T) ) ) )) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f13,axiom,(
% 62.73/8.32 (! [X,T] :( organization(X)=> ( ( has_immunity(X,T)=> hazard_of_mortality(X,T) = very_low )& ( ~ has_immunity(X,T)=> ( ( ( is_aligned(X,T)& positional_advantage(X,T) )=> hazard_of_mortality(X,T) = low )& ( ( ~ is_aligned(X,T)& positional_advantage(X,T) )=> hazard_of_mortality(X,T) = mod1 )& ( ( is_aligned(X,T)& ~ positional_advantage(X,T) )=> hazard_of_mortality(X,T) = mod2 )& ( ( ~ is_aligned(X,T)& ~ positional_advantage(X,T) )=> hazard_of_mortality(X,T) = high ) ) ) ) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f14,axiom,(
% 62.73/8.32 greater(high,mod1) ),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f15,axiom,(
% 62.73/8.32 greater(mod1,low) ),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f16,axiom,(
% 62.73/8.32 greater(low,very_low) ),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f17,axiom,(
% 62.73/8.32 greater(high,mod2) ),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f18,axiom,(
% 62.73/8.32 greater(mod2,low) ),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f19,axiom,(
% 62.73/8.32 greater(mod2,mod1) ),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f20,conjecture,(
% 62.73/8.32 (! [X,T0,T1,T2,T3] :( ( organization(X)& robust_position(X)& ~ has_endowment(X)& age(X,T0) = zero& greater(sigma,zero)& greater(tau,zero)& smaller(sigma,tau)& smaller_or_equal(age(X,T1),sigma)& greater(age(X,T2),sigma)& smaller_or_equal(age(X,T2),tau)& greater(age(X,T3),tau) )=> ( smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))& smaller(hazard_of_mortality(X,T1),hazard_of_mortality(X,T2))& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) )),
% 62.73/8.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.73/8.32 fof(f21,negated_conjecture,(
% 62.73/8.32 ~((! [X,T0,T1,T2,T3] :( ( organization(X)& robust_position(X)& ~ has_endowment(X)& age(X,T0) = zero& greater(sigma,zero)& greater(tau,zero)& smaller(sigma,tau)& smaller_or_equal(age(X,T1),sigma)& greater(age(X,T2),sigma)& smaller_or_equal(age(X,T2),tau)& greater(age(X,T3),tau) )=> ( smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))& smaller(hazard_of_mortality(X,T1),hazard_of_mortality(X,T2))& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ))),
% 62.73/8.32 inference(negated_conjecture,[status(cth)],[f20])).
% 62.73/8.32 fof(f22,plain,(
% 62.73/8.32 ![X,Y]: ((~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y))&(smaller_or_equal(X,Y)|(~smaller(X,Y)&~X=Y)))),
% 62.73/8.32 inference(NNF_transformation,[status(thm)],[f1])).
% 62.73/8.32 fof(f23,plain,(
% 62.73/8.32 (![X,Y]: (~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y)))&(![X,Y]: (smaller_or_equal(X,Y)|(~smaller(X,Y)&~X=Y)))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f22])).
% 62.73/8.32 fof(f24,plain,(
% 62.73/8.32 ![X0,X1]: (~smaller_or_equal(X0,X1)|smaller(X0,X1)|X0=X1)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f23])).
% 62.73/8.32 fof(f25,plain,(
% 62.73/8.32 ![X0,X1]: (smaller_or_equal(X0,X1)|~smaller(X0,X1))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f23])).
% 62.73/8.32 fof(f27,plain,(
% 62.73/8.32 ![X,Y]: ((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&(greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 62.73/8.32 inference(NNF_transformation,[status(thm)],[f2])).
% 62.73/8.32 fof(f28,plain,(
% 62.73/8.32 (![X,Y]: (~greater_or_equal(X,Y)|(greater(X,Y)|X=Y)))&(![X,Y]: (greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f27])).
% 62.73/8.32 fof(f29,plain,(
% 62.73/8.32 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f28])).
% 62.73/8.32 fof(f30,plain,(
% 62.73/8.32 ![X0,X1]: (greater_or_equal(X0,X1)|~greater(X0,X1))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f28])).
% 62.73/8.32 fof(f32,plain,(
% 62.73/8.32 ![X,Y]: ((~smaller(X,Y)|greater(Y,X))&(smaller(X,Y)|~greater(Y,X)))),
% 62.73/8.32 inference(NNF_transformation,[status(thm)],[f3])).
% 62.73/8.32 fof(f33,plain,(
% 62.73/8.32 (![X,Y]: (~smaller(X,Y)|greater(Y,X)))&(![X,Y]: (smaller(X,Y)|~greater(Y,X)))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f32])).
% 62.73/8.32 fof(f34,plain,(
% 62.73/8.32 ![X0,X1]: (~smaller(X0,X1)|greater(X1,X0))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f33])).
% 62.73/8.32 fof(f35,plain,(
% 62.73/8.32 ![X0,X1]: (smaller(X0,X1)|~greater(X1,X0))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f33])).
% 62.73/8.32 fof(f36,plain,(
% 62.73/8.32 ![X,Y]: (~greater(X,Y)|~greater(Y,X))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 62.73/8.32 fof(f37,plain,(
% 62.73/8.32 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f36])).
% 62.73/8.32 fof(f38,plain,(
% 62.73/8.32 ![X,Y,Z]: ((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 62.73/8.32 fof(f39,plain,(
% 62.73/8.32 ![X,Z]: ((![Y]: (~greater(X,Y)|~greater(Y,Z)))|greater(X,Z))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f38])).
% 62.73/8.32 fof(f40,plain,(
% 62.73/8.32 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f39])).
% 62.73/8.32 fof(f41,plain,(
% 62.73/8.32 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater(X0,X1))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f6])).
% 62.73/8.32 fof(f53,plain,(
% 62.73/8.32 ![X,T]: ((~organization(X)|has_endowment(X))|~has_immunity(X,T))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 62.73/8.32 fof(f54,plain,(
% 62.73/8.32 ![X]: ((~organization(X)|has_endowment(X))|(![T]: ~has_immunity(X,T)))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f53])).
% 62.73/8.32 fof(f55,plain,(
% 62.73/8.32 ![X0,X1]: (~organization(X0)|has_endowment(X0)|~has_immunity(X0,X1))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f54])).
% 62.73/8.32 fof(f56,plain,(
% 62.73/8.32 ![X,T0,T]: (dissimilar(X,T0,T)<=>(organization(X)&(is_aligned(X,T0)<~>is_aligned(X,T))))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 62.73/8.32 fof(f57,plain,(
% 62.73/8.32 ![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))))))),
% 62.73/8.32 inference(NNF_transformation,[status(thm)],[f56])).
% 62.73/8.32 fof(f58,plain,(
% 62.73/8.32 (![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))))))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f57])).
% 62.73/8.32 fof(f59,plain,(
% 62.73/8.32 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|organization(X0))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f58])).
% 62.73/8.32 fof(f61,plain,(
% 62.73/8.32 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f58])).
% 62.73/8.32 fof(f62,plain,(
% 62.73/8.32 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f58])).
% 62.73/8.32 fof(f63,plain,(
% 62.73/8.32 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f58])).
% 62.73/8.32 fof(f64,plain,(
% 62.73/8.32 ![X,T]: ((~organization(X)|~age(X,T)=zero)|is_aligned(X,T))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 62.73/8.32 fof(f65,plain,(
% 62.73/8.32 ![X0,X1]: (~organization(X0)|~age(X0,X1)=zero|is_aligned(X0,X1))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f64])).
% 62.73/8.32 fof(f66,plain,(
% 62.73/8.32 ![X,T0,T]: ((~organization(X)|~age(X,T0)=zero)|(greater(age(X,T),sigma)<=>dissimilar(X,T0,T)))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 62.73/8.32 fof(f67,plain,(
% 62.73/8.32 ![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))))),
% 62.73/8.32 inference(NNF_transformation,[status(thm)],[f66])).
% 62.73/8.32 fof(f68,plain,(
% 62.73/8.32 ![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)))))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f67])).
% 62.73/8.32 fof(f69,plain,(
% 62.73/8.32 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~greater(age(X0,X2),sigma)|dissimilar(X0,X1,X2))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f68])).
% 62.73/8.32 fof(f70,plain,(
% 62.73/8.32 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|greater(age(X0,X2),sigma)|~dissimilar(X0,X1,X2))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f68])).
% 62.73/8.32 fof(f71,plain,(
% 62.73/8.32 ![X]: (robust_position(X)<=>(![T]: ((~smaller_or_equal(age(X,T),tau)|~positional_advantage(X,T))&(~greater(age(X,T),tau)|positional_advantage(X,T)))))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 62.73/8.32 fof(f72,plain,(
% 62.73/8.32 ![X]: ((~robust_position(X)|(![T]: ((~smaller_or_equal(age(X,T),tau)|~positional_advantage(X,T))&(~greater(age(X,T),tau)|positional_advantage(X,T)))))&(robust_position(X)|(?[T]: ((smaller_or_equal(age(X,T),tau)&positional_advantage(X,T))|(greater(age(X,T),tau)&~positional_advantage(X,T))))))),
% 62.73/8.32 inference(NNF_transformation,[status(thm)],[f71])).
% 62.73/8.32 fof(f73,plain,(
% 62.73/8.32 (![X]: (~robust_position(X)|((![T]: (~smaller_or_equal(age(X,T),tau)|~positional_advantage(X,T)))&(![T]: (~greater(age(X,T),tau)|positional_advantage(X,T))))))&(![X]: (robust_position(X)|((?[T]: (smaller_or_equal(age(X,T),tau)&positional_advantage(X,T)))|(?[T]: (greater(age(X,T),tau)&~positional_advantage(X,T))))))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f72])).
% 62.73/8.32 fof(f74,plain,(
% 62.73/8.32 (![X]: (~robust_position(X)|((![T]: (~smaller_or_equal(age(X,T),tau)|~positional_advantage(X,T)))&(![T]: (~greater(age(X,T),tau)|positional_advantage(X,T))))))&(![X]: (robust_position(X)|((smaller_or_equal(age(X,sK2_skl(X)),tau)&positional_advantage(X,sK2_skl(X)))|(greater(age(X,sK3_skl(X)),tau)&~positional_advantage(X,sK3_skl(X))))))),
% 62.73/8.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(T,sK2_skl(X)),skolemize(T,sK3_skl(X))],[f73])).
% 62.73/8.32 fof(f75,plain,(
% 62.73/8.32 ![X0,X1]: (~robust_position(X0)|~smaller_or_equal(age(X0,X1),tau)|~positional_advantage(X0,X1))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f74])).
% 62.73/8.32 fof(f76,plain,(
% 62.73/8.32 ![X0,X1]: (~robust_position(X0)|~greater(age(X0,X1),tau)|positional_advantage(X0,X1))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f74])).
% 62.73/8.32 fof(f77,plain,(
% 62.73/8.32 ![X0]: (robust_position(X0)|smaller_or_equal(age(X0,sK2_skl(X0)),tau)|greater(age(X0,sK3_skl(X0)),tau))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f74])).
% 62.73/8.32 fof(f79,plain,(
% 62.73/8.32 ![X0]: (robust_position(X0)|positional_advantage(X0,sK2_skl(X0))|greater(age(X0,sK3_skl(X0)),tau))),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f74])).
% 62.73/8.32 fof(f81,plain,(
% 62.73/8.32 ![X,T]: (~organization(X)|((~has_immunity(X,T)|hazard_of_mortality(X,T)=very_low)&(has_immunity(X,T)|(((((~is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=low)&((is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=mod1))&((~is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=mod2))&((is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=high)))))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 62.73/8.32 fof(f82,plain,(
% 62.73/8.32 ![X]: (~organization(X)|((![T]: (~has_immunity(X,T)|hazard_of_mortality(X,T)=very_low))&(![T]: (has_immunity(X,T)|(((((~is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=low)&((is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=mod1))&((~is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=mod2))&((is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=high))))))),
% 62.73/8.32 inference(miniscoping,[status(thm)],[f81])).
% 62.73/8.32 fof(f83,plain,(
% 62.73/8.32 ![X0,X1]: (~organization(X0)|~has_immunity(X0,X1)|hazard_of_mortality(X0,X1)=very_low)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f82])).
% 62.73/8.32 fof(f84,plain,(
% 62.73/8.32 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=low)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f82])).
% 62.73/8.32 fof(f85,plain,(
% 62.73/8.32 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod1)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f82])).
% 62.73/8.32 fof(f86,plain,(
% 62.73/8.32 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f82])).
% 62.73/8.32 fof(f87,plain,(
% 62.73/8.32 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=high)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f82])).
% 62.73/8.32 fof(f88,plain,(
% 62.73/8.32 greater(high,mod1)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f14])).
% 62.73/8.32 fof(f89,plain,(
% 62.73/8.32 greater(mod1,low)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f15])).
% 62.73/8.32 fof(f90,plain,(
% 62.73/8.32 greater(low,very_low)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f16])).
% 62.73/8.32 fof(f91,plain,(
% 62.73/8.32 greater(high,mod2)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f17])).
% 62.73/8.32 fof(f92,plain,(
% 62.73/8.32 greater(mod2,low)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f18])).
% 62.73/8.32 fof(f93,plain,(
% 62.73/8.32 greater(mod2,mod1)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f19])).
% 62.73/8.32 fof(f94,plain,(
% 62.73/8.32 (?[X,T0,T1,T2,T3]: (((((((((((organization(X)&robust_position(X))&~has_endowment(X))&age(X,T0)=zero)&greater(sigma,zero))&greater(tau,zero))&smaller(sigma,tau))&smaller_or_equal(age(X,T1),sigma))&greater(age(X,T2),sigma))&smaller_or_equal(age(X,T2),tau))&greater(age(X,T3),tau))&((~smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))|~smaller(hazard_of_mortality(X,T1),hazard_of_mortality(X,T2)))|~hazard_of_mortality(X,T1)=hazard_of_mortality(X,T0))))),
% 62.73/8.32 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 62.73/8.32 fof(f95,plain,(
% 62.73/8.32 (((((((((((organization(sK4_skl)&robust_position(sK4_skl))&~has_endowment(sK4_skl))&age(sK4_skl,sK5_skl)=zero)&greater(sigma,zero))&greater(tau,zero))&smaller(sigma,tau))&smaller_or_equal(age(sK4_skl,sK6_skl),sigma))&greater(age(sK4_skl,sK7_skl),sigma))&smaller_or_equal(age(sK4_skl,sK7_skl),tau))&greater(age(sK4_skl,sK8_skl),tau))&((~smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl))|~smaller(hazard_of_mortality(sK4_skl,sK6_skl),hazard_of_mortality(sK4_skl,sK7_skl)))|~hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl)))),
% 62.73/8.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(X,sK4_skl),skolemize(T0,sK5_skl),skolemize(T1,sK6_skl),skolemize(T2,sK7_skl),skolemize(T3,sK8_skl)],[f94])).
% 62.73/8.32 fof(f96,plain,(
% 62.73/8.32 organization(sK4_skl)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f97,plain,(
% 62.73/8.32 robust_position(sK4_skl)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f98,plain,(
% 62.73/8.32 ~has_endowment(sK4_skl)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f99,plain,(
% 62.73/8.32 age(sK4_skl,sK5_skl)=zero),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f100,plain,(
% 62.73/8.32 greater(sigma,zero)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f101,plain,(
% 62.73/8.32 greater(tau,zero)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f102,plain,(
% 62.73/8.32 smaller(sigma,tau)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f103,plain,(
% 62.73/8.32 smaller_or_equal(age(sK4_skl,sK6_skl),sigma)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f104,plain,(
% 62.73/8.32 greater(age(sK4_skl,sK7_skl),sigma)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f105,plain,(
% 62.73/8.32 smaller_or_equal(age(sK4_skl,sK7_skl),tau)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f106,plain,(
% 62.73/8.32 greater(age(sK4_skl,sK8_skl),tau)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f107,plain,(
% 62.73/8.32 ~smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl))|~smaller(hazard_of_mortality(sK4_skl,sK6_skl),hazard_of_mortality(sK4_skl,sK7_skl))|~hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl)),
% 62.73/8.32 inference(cnf_transformation,[status(thm)],[f95])).
% 62.73/8.32 fof(f108,definition,(
% 62.73/8.32 sQ0_spl <=> (smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl)))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f110,plain,(
% 62.73/8.32 ~smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl))|sQ0_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f108])).
% 62.73/8.32 fof(f111,definition,(
% 62.73/8.32 sQ1_spl <=> (smaller(hazard_of_mortality(sK4_skl,sK6_skl),hazard_of_mortality(sK4_skl,sK7_skl)))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f112,plain,(
% 62.73/8.32 smaller(hazard_of_mortality(sK4_skl,sK6_skl),hazard_of_mortality(sK4_skl,sK7_skl))|~sQ1_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f111])).
% 62.73/8.32 fof(f113,plain,(
% 62.73/8.32 ~smaller(hazard_of_mortality(sK4_skl,sK6_skl),hazard_of_mortality(sK4_skl,sK7_skl))|sQ1_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f111])).
% 62.73/8.32 fof(f114,definition,(
% 62.73/8.32 sQ2_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f116,plain,(
% 62.73/8.32 ~hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl)|sQ2_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f114])).
% 62.73/8.32 fof(f117,plain,(
% 62.73/8.32 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f107,f108,f111,f114])).
% 62.73/8.32 fof(f121,plain,(
% 62.73/8.32 ![X0,X1,X2]: (~age(X0,X1)=zero|greater(age(X0,X2),sigma)|~dissimilar(X0,X1,X2))),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f70,f59])).
% 62.73/8.32 fof(f122,plain,(
% 62.73/8.32 smaller(zero,tau)),
% 62.73/8.32 inference(resolution,[status(thm)],[f35,f101])).
% 62.73/8.32 fof(f123,plain,(
% 62.73/8.32 smaller(zero,sigma)),
% 62.73/8.32 inference(resolution,[status(thm)],[f35,f100])).
% 62.73/8.32 fof(f127,plain,(
% 62.73/8.32 ~greater(zero,tau)),
% 62.73/8.32 inference(resolution,[status(thm)],[f37,f101])).
% 62.73/8.32 fof(f128,plain,(
% 62.73/8.32 ~greater(zero,sigma)),
% 62.73/8.32 inference(resolution,[status(thm)],[f37,f100])).
% 62.73/8.32 fof(f129,plain,(
% 62.73/8.32 ![X0,X1]: (~greater(X0,X1)|~smaller(X0,X1))),
% 62.73/8.32 inference(resolution,[status(thm)],[f37,f34])).
% 62.73/8.32 fof(f130,plain,(
% 62.73/8.32 ~greater(mod1,high)),
% 62.73/8.32 inference(resolution,[status(thm)],[f88,f37])).
% 62.73/8.32 fof(f131,plain,(
% 62.73/8.32 smaller(mod1,high)),
% 62.73/8.32 inference(resolution,[status(thm)],[f88,f35])).
% 62.73/8.32 fof(f132,plain,(
% 62.73/8.32 ~greater(low,mod1)),
% 62.73/8.32 inference(resolution,[status(thm)],[f89,f37])).
% 62.73/8.32 fof(f134,plain,(
% 62.73/8.32 ~greater(very_low,low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f90,f37])).
% 62.73/8.32 fof(f136,plain,(
% 62.73/8.32 ~greater(mod2,high)),
% 62.73/8.32 inference(resolution,[status(thm)],[f91,f37])).
% 62.73/8.32 fof(f137,plain,(
% 62.73/8.32 smaller(mod2,high)),
% 62.73/8.32 inference(resolution,[status(thm)],[f91,f35])).
% 62.73/8.32 fof(f138,plain,(
% 62.73/8.32 ~greater(low,mod2)),
% 62.73/8.32 inference(resolution,[status(thm)],[f92,f37])).
% 62.73/8.32 fof(f139,plain,(
% 62.73/8.32 smaller(low,mod2)),
% 62.73/8.32 inference(resolution,[status(thm)],[f92,f35])).
% 62.73/8.32 fof(f140,plain,(
% 62.73/8.32 ~greater(mod1,mod2)),
% 62.73/8.32 inference(resolution,[status(thm)],[f93,f37])).
% 62.73/8.32 fof(f142,plain,(
% 62.73/8.32 ~smaller(tau,zero)),
% 62.73/8.32 inference(resolution,[status(thm)],[f127,f34])).
% 62.73/8.32 fof(f143,plain,(
% 62.73/8.32 ~smaller(sigma,zero)),
% 62.73/8.32 inference(resolution,[status(thm)],[f128,f34])).
% 62.73/8.32 fof(f144,plain,(
% 62.73/8.32 ~smaller(high,mod1)),
% 62.73/8.32 inference(resolution,[status(thm)],[f130,f34])).
% 62.73/8.32 fof(f146,plain,(
% 62.73/8.32 greater_or_equal(mod2,mod1)),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f93])).
% 62.73/8.32 fof(f147,plain,(
% 62.73/8.32 greater_or_equal(mod2,low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f92])).
% 62.73/8.32 fof(f148,plain,(
% 62.73/8.32 greater_or_equal(low,very_low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f90])).
% 62.73/8.32 fof(f149,plain,(
% 62.73/8.32 greater_or_equal(mod1,low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f89])).
% 62.73/8.32 fof(f150,plain,(
% 62.73/8.32 greater_or_equal(high,mod2)),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f91])).
% 62.73/8.32 fof(f151,plain,(
% 62.73/8.32 greater_or_equal(high,mod1)),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f88])).
% 62.73/8.32 fof(f152,plain,(
% 62.73/8.32 greater_or_equal(tau,zero)),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f101])).
% 62.73/8.32 fof(f153,plain,(
% 62.73/8.32 greater_or_equal(sigma,zero)),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f100])).
% 62.73/8.32 fof(f154,plain,(
% 62.73/8.32 ![X0,X1]: (greater_or_equal(X0,X1)|~smaller(X1,X0))),
% 62.73/8.32 inference(resolution,[status(thm)],[f30,f34])).
% 62.73/8.32 fof(f157,plain,(
% 62.73/8.32 ![X0]: (~greater(zero,X0)|~greater(X0,tau))),
% 62.73/8.32 inference(resolution,[status(thm)],[f40,f127])).
% 62.73/8.32 fof(f159,plain,(
% 62.73/8.32 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|~greater(X2,X0))),
% 62.73/8.32 inference(resolution,[status(thm)],[f40,f37])).
% 62.73/8.32 fof(f161,plain,(
% 62.73/8.32 greater(tau,zero)|tau=zero),
% 62.73/8.32 inference(resolution,[status(thm)],[f152,f29])).
% 62.73/8.32 fof(f162,definition,(
% 62.73/8.32 sQ3_spl <=> (greater(tau,zero))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f165,definition,(
% 62.73/8.32 sQ4_spl <=> (tau=zero)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f166,plain,(
% 62.73/8.32 tau=zero|~sQ4_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f165])).
% 62.73/8.32 fof(f167,plain,(
% 62.73/8.32 ~tau=zero|sQ4_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f165])).
% 62.73/8.32 fof(f168,plain,(
% 62.73/8.32 sQ3_spl|sQ4_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f161,f162,f165])).
% 62.73/8.32 fof(f170,plain,(
% 62.73/8.32 ~smaller(zero,zero)|~sQ4_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f166,f142])).
% 62.73/8.32 fof(f172,plain,(
% 62.73/8.32 smaller(zero,zero)|~sQ4_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f166,f122])).
% 62.73/8.32 fof(f183,plain,(
% 62.73/8.32 $false|~sQ4_spl),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f172,f170])).
% 62.73/8.32 fof(f184,plain,(
% 62.73/8.32 ~sQ4_spl),
% 62.73/8.32 inference(contradiction_clause,[status(thm)],[f183])).
% 62.73/8.32 fof(f185,plain,(
% 62.73/8.32 smaller(age(sK4_skl,sK6_skl),sigma)|age(sK4_skl,sK6_skl)=sigma),
% 62.73/8.32 inference(resolution,[status(thm)],[f103,f24])).
% 62.73/8.32 fof(f186,definition,(
% 62.73/8.32 sQ5_spl <=> (smaller(age(sK4_skl,sK6_skl),sigma))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f187,plain,(
% 62.73/8.32 smaller(age(sK4_skl,sK6_skl),sigma)|~sQ5_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f186])).
% 62.73/8.32 fof(f189,definition,(
% 62.73/8.32 sQ6_spl <=> (age(sK4_skl,sK6_skl)=sigma)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f190,plain,(
% 62.73/8.32 age(sK4_skl,sK6_skl)=sigma|~sQ6_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f189])).
% 62.73/8.32 fof(f192,plain,(
% 62.73/8.32 sQ5_spl|sQ6_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f185,f186,f189])).
% 62.73/8.32 fof(f195,plain,(
% 62.73/8.32 ![X0]: (~greater(low,X0)|~greater(X0,mod1))),
% 62.73/8.32 inference(resolution,[status(thm)],[f132,f40])).
% 62.73/8.32 fof(f196,plain,(
% 62.73/8.32 ~smaller(mod1,low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f132,f34])).
% 62.73/8.32 fof(f198,plain,(
% 62.73/8.32 ~smaller(low,very_low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f134,f34])).
% 62.73/8.32 fof(f200,plain,(
% 62.73/8.32 ~smaller(high,mod2)),
% 62.73/8.32 inference(resolution,[status(thm)],[f136,f34])).
% 62.73/8.32 fof(f201,plain,(
% 62.73/8.32 ![X0]: (~greater(low,X0)|~greater(X0,mod2))),
% 62.73/8.32 inference(resolution,[status(thm)],[f138,f40])).
% 62.73/8.32 fof(f202,plain,(
% 62.73/8.32 ~smaller(mod2,low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f138,f34])).
% 62.73/8.32 fof(f203,plain,(
% 62.73/8.32 smaller(mod2,high)|mod2=high),
% 62.73/8.32 inference(resolution,[status(thm)],[f41,f136])).
% 62.73/8.32 fof(f204,plain,(
% 62.73/8.32 smaller(very_low,low)|very_low=low),
% 62.73/8.32 inference(resolution,[status(thm)],[f41,f134])).
% 62.73/8.32 fof(f205,plain,(
% 62.73/8.32 smaller(low,mod2)|low=mod2),
% 62.73/8.32 inference(resolution,[status(thm)],[f41,f138])).
% 62.73/8.32 fof(f206,plain,(
% 62.73/8.32 smaller(low,mod1)|low=mod1),
% 62.73/8.32 inference(resolution,[status(thm)],[f41,f132])).
% 62.73/8.32 fof(f207,plain,(
% 62.73/8.32 smaller(mod1,high)|mod1=high),
% 62.73/8.32 inference(resolution,[status(thm)],[f41,f130])).
% 62.73/8.32 fof(f208,plain,(
% 62.73/8.32 smaller(zero,sigma)|zero=sigma),
% 62.73/8.32 inference(resolution,[status(thm)],[f41,f128])).
% 62.73/8.32 fof(f209,plain,(
% 62.73/8.32 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater_or_equal(X0,X1))),
% 62.73/8.32 inference(resolution,[status(thm)],[f41,f30])).
% 62.73/8.32 fof(f211,plain,(
% 62.73/8.32 ![X0,X1]: (smaller(X0,X1)|X0=X1|smaller(X1,X0))),
% 62.73/8.32 inference(resolution,[status(thm)],[f41,f35])).
% 62.73/8.32 fof(f212,definition,(
% 62.73/8.32 sQ7_spl <=> (smaller(mod2,high))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f215,definition,(
% 62.73/8.32 sQ8_spl <=> (mod2=high)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f216,plain,(
% 62.73/8.32 mod2=high|~sQ8_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f215])).
% 62.73/8.32 fof(f218,plain,(
% 62.73/8.32 sQ7_spl|sQ8_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f203,f212,f215])).
% 62.73/8.32 fof(f219,definition,(
% 62.73/8.32 sQ9_spl <=> (smaller(very_low,low))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f222,definition,(
% 62.73/8.32 sQ10_spl <=> (very_low=low)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f223,plain,(
% 62.73/8.32 very_low=low|~sQ10_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f222])).
% 62.73/8.32 fof(f225,plain,(
% 62.73/8.32 sQ9_spl|sQ10_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f204,f219,f222])).
% 62.73/8.32 fof(f226,definition,(
% 62.73/8.32 sQ11_spl <=> (smaller(low,mod2))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f229,definition,(
% 62.73/8.32 sQ12_spl <=> (low=mod2)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f230,plain,(
% 62.73/8.32 low=mod2|~sQ12_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f229])).
% 62.73/8.32 fof(f232,plain,(
% 62.73/8.32 sQ11_spl|sQ12_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f205,f226,f229])).
% 62.73/8.32 fof(f233,definition,(
% 62.73/8.32 sQ13_spl <=> (smaller(low,mod1))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f236,definition,(
% 62.73/8.32 sQ14_spl <=> (low=mod1)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f237,plain,(
% 62.73/8.32 low=mod1|~sQ14_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f236])).
% 62.73/8.32 fof(f239,plain,(
% 62.73/8.32 sQ13_spl|sQ14_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f206,f233,f236])).
% 62.73/8.32 fof(f240,definition,(
% 62.73/8.32 sQ15_spl <=> (smaller(mod1,high))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f243,definition,(
% 62.73/8.32 sQ16_spl <=> (mod1=high)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f244,plain,(
% 62.73/8.32 mod1=high|~sQ16_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f243])).
% 62.73/8.32 fof(f246,plain,(
% 62.73/8.32 sQ15_spl|sQ16_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f207,f240,f243])).
% 62.73/8.32 fof(f247,definition,(
% 62.73/8.32 sQ17_spl <=> (smaller(zero,sigma))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f250,definition,(
% 62.73/8.32 sQ18_spl <=> (zero=sigma)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f251,plain,(
% 62.73/8.32 zero=sigma|~sQ18_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f250])).
% 62.73/8.32 fof(f253,plain,(
% 62.73/8.32 sQ17_spl|sQ18_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f208,f247,f250])).
% 62.73/8.32 fof(f254,plain,(
% 62.73/8.32 ~smaller(zero,zero)|~sQ18_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f251,f143])).
% 62.73/8.32 fof(f256,plain,(
% 62.73/8.32 smaller(zero,zero)|~sQ18_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f251,f123])).
% 62.73/8.32 fof(f269,plain,(
% 62.73/8.32 ~greater(high,high)|~sQ16_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f244,f130])).
% 62.73/8.32 fof(f272,plain,(
% 62.73/8.32 greater(high,high)|~sQ16_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f244,f88])).
% 62.73/8.32 fof(f306,plain,(
% 62.73/8.32 $false|~sQ18_spl),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f256,f254])).
% 62.73/8.32 fof(f307,plain,(
% 62.73/8.32 ~sQ18_spl),
% 62.73/8.32 inference(contradiction_clause,[status(thm)],[f306])).
% 62.73/8.32 fof(f314,plain,(
% 62.73/8.32 $false|~sQ16_spl),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f272,f269])).
% 62.73/8.32 fof(f315,plain,(
% 62.73/8.32 ~sQ16_spl),
% 62.73/8.32 inference(contradiction_clause,[status(thm)],[f314])).
% 62.73/8.32 fof(f319,plain,(
% 62.73/8.32 ~greater(very_low,very_low)|~sQ10_spl),
% 62.73/8.32 inference(forward_demodulation,[status(thm)],[f223,f134])).
% 62.73/8.32 fof(f321,plain,(
% 62.73/8.32 greater(very_low,very_low)|~sQ10_spl),
% 62.73/8.32 inference(forward_demodulation,[status(thm)],[f223,f90])).
% 62.73/8.32 fof(f322,plain,(
% 62.73/8.32 $false|~sQ10_spl),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f321,f319])).
% 62.73/8.32 fof(f323,plain,(
% 62.73/8.32 ~sQ10_spl),
% 62.73/8.32 inference(contradiction_clause,[status(thm)],[f322])).
% 62.73/8.32 fof(f328,plain,(
% 62.73/8.32 greater(high,high)|~sQ8_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f216,f91])).
% 62.73/8.32 fof(f329,plain,(
% 62.73/8.32 ~greater(high,high)|~sQ8_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f216,f136])).
% 62.73/8.32 fof(f342,plain,(
% 62.73/8.32 $false|~sQ8_spl),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f329,f328])).
% 62.73/8.32 fof(f343,plain,(
% 62.73/8.32 ~sQ8_spl),
% 62.73/8.32 inference(contradiction_clause,[status(thm)],[f342])).
% 62.73/8.32 fof(f346,plain,(
% 62.73/8.32 smaller(zero,tau)|zero=tau),
% 62.73/8.32 inference(resolution,[status(thm)],[f127,f41])).
% 62.73/8.32 fof(f349,definition,(
% 62.73/8.32 sQ19_spl <=> (smaller(zero,tau))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f352,plain,(
% 62.73/8.32 sQ19_spl|sQ4_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f346,f349,f165])).
% 62.73/8.32 fof(f363,plain,(
% 62.73/8.32 greater(sigma,zero)|sigma=zero),
% 62.73/8.32 inference(resolution,[status(thm)],[f153,f29])).
% 62.73/8.32 fof(f364,definition,(
% 62.73/8.32 sQ20_spl <=> (greater(sigma,zero))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f367,plain,(
% 62.73/8.32 sQ20_spl|sQ18_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f363,f364,f250])).
% 62.73/8.32 fof(f381,plain,(
% 62.73/8.32 greater(low,very_low)|low=very_low),
% 62.73/8.32 inference(resolution,[status(thm)],[f148,f29])).
% 62.73/8.32 fof(f382,definition,(
% 62.73/8.32 sQ21_spl <=> (greater(low,very_low))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f385,plain,(
% 62.73/8.32 sQ21_spl|sQ10_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f381,f382,f222])).
% 62.73/8.32 fof(f389,plain,(
% 62.73/8.32 greater(high,mod1)|high=mod1),
% 62.73/8.32 inference(resolution,[status(thm)],[f151,f29])).
% 62.73/8.32 fof(f390,definition,(
% 62.73/8.32 sQ22_spl <=> (greater(high,mod1))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f393,plain,(
% 62.73/8.32 sQ22_spl|sQ16_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f389,f390,f243])).
% 62.73/8.32 fof(f394,plain,(
% 62.73/8.32 greater(mod1,low)|mod1=low),
% 62.73/8.32 inference(resolution,[status(thm)],[f149,f29])).
% 62.73/8.32 fof(f395,definition,(
% 62.73/8.32 sQ23_spl <=> (greater(mod1,low))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f398,plain,(
% 62.73/8.32 sQ23_spl|sQ14_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f394,f395,f236])).
% 62.73/8.32 fof(f402,plain,(
% 62.73/8.32 greater(high,mod2)|high=mod2),
% 62.73/8.32 inference(resolution,[status(thm)],[f150,f29])).
% 62.73/8.32 fof(f403,definition,(
% 62.73/8.32 sQ24_spl <=> (greater(high,mod2))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f406,plain,(
% 62.73/8.32 sQ24_spl|sQ8_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f402,f403,f215])).
% 62.73/8.32 fof(f414,plain,(
% 62.73/8.32 greater(mod2,low)|mod2=low),
% 62.73/8.32 inference(resolution,[status(thm)],[f147,f29])).
% 62.73/8.32 fof(f415,definition,(
% 62.73/8.32 sQ25_spl <=> (greater(mod2,low))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f418,plain,(
% 62.73/8.32 sQ25_spl|sQ12_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f414,f415,f229])).
% 62.73/8.32 fof(f419,plain,(
% 62.73/8.32 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|is_aligned(X0,X2)|~organization(X0)|~age(X0,X1)=zero)),
% 62.73/8.32 inference(resolution,[status(thm)],[f62,f65])).
% 62.73/8.32 fof(f420,plain,(
% 62.73/8.32 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|is_aligned(X0,X2)|~age(X0,X1)=zero)),
% 62.73/8.32 inference(duplicate_literals_removal,[status(thm)],[f419])).
% 62.73/8.32 fof(f421,plain,(
% 62.73/8.32 ![X0]: (~greater(X0,tau)|smaller(zero,X0)|zero=X0)),
% 62.73/8.32 inference(resolution,[status(thm)],[f157,f41])).
% 62.73/8.32 fof(f424,plain,(
% 62.73/8.32 greater_or_equal(age(sK4_skl,sK8_skl),tau)),
% 62.73/8.32 inference(resolution,[status(thm)],[f106,f30])).
% 62.73/8.32 fof(f425,plain,(
% 62.73/8.32 ~greater(tau,age(sK4_skl,sK8_skl))),
% 62.73/8.32 inference(resolution,[status(thm)],[f106,f37])).
% 62.73/8.32 fof(f426,plain,(
% 62.73/8.32 smaller(tau,age(sK4_skl,sK8_skl))),
% 62.73/8.32 inference(resolution,[status(thm)],[f106,f35])).
% 62.73/8.32 fof(f445,plain,(
% 62.73/8.32 smaller(mod1,mod2)|mod1=mod2),
% 62.73/8.32 inference(resolution,[status(thm)],[f140,f41])).
% 62.73/8.32 fof(f447,plain,(
% 62.73/8.32 ~smaller(mod2,mod1)),
% 62.73/8.32 inference(resolution,[status(thm)],[f140,f34])).
% 62.73/8.32 fof(f448,definition,(
% 62.73/8.32 sQ28_spl <=> (smaller(mod1,mod2))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f451,definition,(
% 62.73/8.32 sQ29_spl <=> (mod1=mod2)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f452,plain,(
% 62.73/8.32 mod1=mod2|~sQ29_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f451])).
% 62.73/8.32 fof(f453,plain,(
% 62.73/8.32 ~mod1=mod2|sQ29_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f451])).
% 62.73/8.32 fof(f454,plain,(
% 62.73/8.32 sQ28_spl|sQ29_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f445,f448,f451])).
% 62.73/8.32 fof(f455,plain,(
% 62.73/8.32 ~greater(mod1,mod1)|~sQ29_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f452,f140])).
% 62.73/8.32 fof(f468,plain,(
% 62.73/8.32 greater(mod1,mod1)|~sQ29_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f452,f93])).
% 62.73/8.32 fof(f475,plain,(
% 62.73/8.32 $false|~sQ29_spl),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f468,f455])).
% 62.73/8.32 fof(f476,plain,(
% 62.73/8.32 ~sQ29_spl),
% 62.73/8.32 inference(contradiction_clause,[status(thm)],[f475])).
% 62.73/8.32 fof(f478,definition,(
% 62.73/8.32 sQ30_spl <=> (greater(tau,sigma))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f479,plain,(
% 62.73/8.32 greater(tau,sigma)|~sQ30_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f478])).
% 62.73/8.32 fof(f481,definition,(
% 62.73/8.32 sQ31_spl <=> (tau=sigma)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f482,plain,(
% 62.73/8.32 tau=sigma|~sQ31_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f481])).
% 62.73/8.32 fof(f487,plain,(
% 62.73/8.32 smaller(sigma,sigma)|~sQ31_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f482,f102])).
% 62.73/8.32 fof(f509,plain,(
% 62.73/8.32 ![X0,X1]: (~age(sK4_skl,X0)=zero|~greater(age(sK4_skl,X1),sigma)|dissimilar(sK4_skl,X0,X1))),
% 62.73/8.32 inference(resolution,[status(thm)],[f69,f96])).
% 62.73/8.32 fof(f540,plain,(
% 62.73/8.32 greater_or_equal(age(sK4_skl,sK7_skl),sigma)),
% 62.73/8.32 inference(resolution,[status(thm)],[f104,f30])).
% 62.73/8.32 fof(f541,plain,(
% 62.73/8.32 ~greater(sigma,age(sK4_skl,sK7_skl))),
% 62.73/8.32 inference(resolution,[status(thm)],[f104,f37])).
% 62.73/8.32 fof(f542,plain,(
% 62.73/8.32 smaller(sigma,age(sK4_skl,sK7_skl))),
% 62.73/8.32 inference(resolution,[status(thm)],[f104,f35])).
% 62.73/8.32 fof(f553,plain,(
% 62.73/8.32 ~greater(sigma,tau)|~sQ30_spl),
% 62.73/8.32 inference(resolution,[status(thm)],[f479,f37])).
% 62.73/8.32 fof(f561,plain,(
% 62.73/8.32 greater(mod2,mod1)|mod2=mod1),
% 62.73/8.32 inference(resolution,[status(thm)],[f146,f29])).
% 62.73/8.32 fof(f562,definition,(
% 62.73/8.32 sQ32_spl <=> (greater(mod2,mod1))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f565,plain,(
% 62.73/8.32 sQ32_spl|sQ29_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f561,f562,f451])).
% 62.73/8.32 fof(f572,plain,(
% 62.73/8.32 ![X0]: (~greater(sigma,X0)|~greater(X0,tau)|~sQ30_spl)),
% 62.73/8.32 inference(resolution,[status(thm)],[f553,f40])).
% 62.73/8.32 fof(f574,definition,(
% 62.73/8.32 sQ33_spl <=> (smaller(sigma,tau))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f584,plain,(
% 62.73/8.32 ~greater(sigma,tau)),
% 62.73/8.32 inference(resolution,[status(thm)],[f129,f102])).
% 62.73/8.32 fof(f591,definition,(
% 62.73/8.32 sQ34_spl <=> (smaller(sigma,sigma))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f592,plain,(
% 62.73/8.32 smaller(sigma,sigma)|~sQ34_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f591])).
% 62.73/8.32 fof(f593,plain,(
% 62.73/8.32 ~smaller(sigma,sigma)|sQ34_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f591])).
% 62.73/8.32 fof(f594,definition,(
% 62.73/8.32 sQ35_spl <=> (sigma=sigma)),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f600,plain,(
% 62.73/8.32 ~greater(sigma,sigma)|~sQ34_spl),
% 62.73/8.32 inference(resolution,[status(thm)],[f592,f129])).
% 62.73/8.32 fof(f603,plain,(
% 62.73/8.32 ~smaller(sigma,sigma)|~sQ34_spl),
% 62.73/8.32 inference(resolution,[status(thm)],[f600,f34])).
% 62.73/8.32 fof(f605,plain,(
% 62.73/8.32 $false|~sQ34_spl),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f603,f592])).
% 62.73/8.32 fof(f606,plain,(
% 62.73/8.32 ~sQ34_spl),
% 62.73/8.32 inference(contradiction_clause,[status(thm)],[f605])).
% 62.73/8.32 fof(f613,plain,(
% 62.73/8.32 greater_or_equal(tau,sigma)),
% 62.73/8.32 inference(resolution,[status(thm)],[f154,f102])).
% 62.73/8.32 fof(f616,plain,(
% 62.73/8.32 ![X0]: (has_immunity(sK4_skl,X0)|is_aligned(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high)),
% 62.73/8.32 inference(resolution,[status(thm)],[f87,f96])).
% 62.73/8.32 fof(f629,plain,(
% 62.73/8.32 tau=zero|greater_or_equal(tau,zero)),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f142])).
% 62.73/8.32 fof(f630,plain,(
% 62.73/8.32 mod2=mod1|greater_or_equal(mod2,mod1)),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f447])).
% 62.73/8.32 fof(f631,plain,(
% 62.73/8.32 mod2=low|greater_or_equal(mod2,low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f202])).
% 62.73/8.32 fof(f632,plain,(
% 62.73/8.32 high=mod2|greater_or_equal(high,mod2)),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f200])).
% 62.73/8.32 fof(f633,plain,(
% 62.73/8.32 high=mod1|greater_or_equal(high,mod1)),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f144])).
% 62.73/8.32 fof(f634,plain,(
% 62.73/8.32 mod1=low|greater_or_equal(mod1,low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f196])).
% 62.73/8.32 fof(f635,plain,(
% 62.73/8.32 low=very_low|greater_or_equal(low,very_low)),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f198])).
% 62.73/8.32 fof(f637,plain,(
% 62.73/8.32 sigma=zero|greater_or_equal(sigma,zero)),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f143])).
% 62.73/8.32 fof(f638,plain,(
% 62.73/8.32 ![X0,X1]: (X0=X1|greater_or_equal(X0,X1)|greater_or_equal(X1,X0))),
% 62.73/8.32 inference(resolution,[status(thm)],[f209,f154])).
% 62.73/8.32 fof(f640,definition,(
% 62.73/8.32 sQ36_spl <=> (greater_or_equal(tau,sigma))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f642,plain,(
% 62.73/8.32 ~greater_or_equal(tau,sigma)|sQ36_spl),
% 62.73/8.32 inference(component_clause,[status(thm)],[f640])).
% 62.73/8.32 fof(f644,definition,(
% 62.73/8.32 sQ37_spl <=> (greater_or_equal(tau,zero))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f647,plain,(
% 62.73/8.32 sQ4_spl|sQ37_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f629,f165,f644])).
% 62.73/8.32 fof(f648,definition,(
% 62.73/8.32 sQ38_spl <=> (greater_or_equal(mod2,mod1))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f651,plain,(
% 62.73/8.32 sQ29_spl|sQ38_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f630,f451,f648])).
% 62.73/8.32 fof(f652,definition,(
% 62.73/8.32 sQ39_spl <=> (greater_or_equal(mod2,low))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f655,plain,(
% 62.73/8.32 sQ12_spl|sQ39_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f631,f229,f652])).
% 62.73/8.32 fof(f656,definition,(
% 62.73/8.32 sQ40_spl <=> (greater_or_equal(high,mod2))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f659,plain,(
% 62.73/8.32 sQ8_spl|sQ40_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f632,f215,f656])).
% 62.73/8.32 fof(f660,definition,(
% 62.73/8.32 sQ41_spl <=> (greater_or_equal(high,mod1))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f663,plain,(
% 62.73/8.32 sQ16_spl|sQ41_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f633,f243,f660])).
% 62.73/8.32 fof(f664,definition,(
% 62.73/8.32 sQ42_spl <=> (greater_or_equal(mod1,low))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f667,plain,(
% 62.73/8.32 sQ14_spl|sQ42_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f634,f236,f664])).
% 62.73/8.32 fof(f668,definition,(
% 62.73/8.32 sQ43_spl <=> (greater_or_equal(low,very_low))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f671,plain,(
% 62.73/8.32 sQ10_spl|sQ43_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f635,f222,f668])).
% 62.73/8.32 fof(f676,definition,(
% 62.73/8.32 sQ45_spl <=> (greater_or_equal(sigma,zero))),
% 62.73/8.32 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 62.73/8.32 fof(f679,plain,(
% 62.73/8.32 sQ18_spl|sQ45_spl),
% 62.73/8.32 inference(split_clause,[status(thm)],[f637,f250,f676])).
% 62.73/8.32 fof(f690,plain,(
% 62.73/8.32 greater(low,low)|~sQ14_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f237,f89])).
% 62.73/8.32 fof(f695,plain,(
% 62.73/8.32 ~greater(low,low)|~sQ14_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f237,f132])).
% 62.73/8.32 fof(f708,plain,(
% 62.73/8.32 ~smaller(low,low)|~sQ12_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f230,f202])).
% 62.73/8.32 fof(f709,plain,(
% 62.73/8.32 smaller(low,low)|~sQ12_spl),
% 62.73/8.32 inference(backward_demodulation,[status(thm)],[f230,f139])).
% 62.73/8.32 fof(f722,plain,(
% 62.73/8.32 $false|~sQ14_spl),
% 62.73/8.32 inference(forward_subsumption_resolution,[status(thm)],[f695,f690])).
% 62.73/8.32 fof(f723,plain,(
% 62.73/8.32 ~sQ14_spl),
% 62.73/8.32 inference(contradiction_clause,[status(thm)],[f722])).
% 62.73/8.34 fof(f724,plain,(
% 62.73/8.34 $false|~sQ12_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f709,f708])).
% 62.73/8.34 fof(f725,plain,(
% 62.73/8.34 ~sQ12_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f724])).
% 62.73/8.34 fof(f732,plain,(
% 62.73/8.34 ![X0]: (~greater(age(sK4_skl,X0),tau)|positional_advantage(sK4_skl,X0))),
% 62.73/8.34 inference(resolution,[status(thm)],[f76,f97])).
% 62.73/8.34 fof(f770,plain,(
% 62.73/8.34 smaller(tau,age(sK4_skl,sK8_skl))|tau=age(sK4_skl,sK8_skl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f425,f41])).
% 62.73/8.34 fof(f772,plain,(
% 62.73/8.34 ~smaller(age(sK4_skl,sK8_skl),tau)),
% 62.73/8.34 inference(resolution,[status(thm)],[f425,f34])).
% 62.73/8.34 fof(f773,definition,(
% 62.73/8.34 sQ46_spl <=> (smaller(tau,age(sK4_skl,sK8_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f776,definition,(
% 62.73/8.34 sQ47_spl <=> (tau=age(sK4_skl,sK8_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f777,plain,(
% 62.73/8.34 tau=age(sK4_skl,sK8_skl)|~sQ47_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f776])).
% 62.73/8.34 fof(f779,plain,(
% 62.73/8.34 sQ46_spl|sQ47_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f770,f773,f776])).
% 62.73/8.34 fof(f780,plain,(
% 62.73/8.34 ~greater(tau,tau)|~sQ47_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f777,f425])).
% 62.73/8.34 fof(f782,plain,(
% 62.73/8.34 greater(tau,tau)|~sQ47_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f777,f106])).
% 62.73/8.34 fof(f786,plain,(
% 62.73/8.34 $false|~sQ47_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f782,f780])).
% 62.73/8.34 fof(f787,plain,(
% 62.73/8.34 ~sQ47_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f786])).
% 62.73/8.34 fof(f823,plain,(
% 62.73/8.34 sigma=sigma|smaller(sigma,sigma)|sQ34_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f211,f593])).
% 62.73/8.34 fof(f853,plain,(
% 62.73/8.34 sQ35_spl|sQ34_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f823,f594,f591])).
% 62.73/8.34 fof(f858,definition,(
% 62.73/8.34 sQ49_spl <=> (greater(zero,tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f879,plain,(
% 62.73/8.34 ![X0]: (~greater(X0,age(sK4_skl,sK7_skl))|~greater(sigma,X0))),
% 62.73/8.34 inference(resolution,[status(thm)],[f159,f104])).
% 62.73/8.34 fof(f887,plain,(
% 62.73/8.34 ![X0,X1,X2,X3]: (~greater(X0,X1)|~greater(X2,X0)|~greater(X1,X3)|~greater(X3,X2))),
% 62.73/8.34 inference(resolution,[status(thm)],[f159,f40])).
% 62.73/8.34 fof(f889,plain,(
% 62.73/8.34 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X2,X0)|~smaller(X2,X1))),
% 62.73/8.34 inference(resolution,[status(thm)],[f159,f34])).
% 62.73/8.34 fof(f904,plain,(
% 62.73/8.34 ![X0]: (~greater(X0,X0)|~greater(X0,X0))),
% 62.73/8.34 inference(factoring,[status(thm)],[f159])).
% 62.73/8.34 fof(f905,plain,(
% 62.73/8.34 ![X0]: (~greater(X0,X0))),
% 62.73/8.34 inference(duplicate_literals_removal,[status(thm)],[f904])).
% 62.73/8.34 fof(f908,plain,(
% 62.73/8.34 ![X0]: (~smaller(X0,X0))),
% 62.73/8.34 inference(resolution,[status(thm)],[f905,f34])).
% 62.73/8.34 fof(f931,plain,(
% 62.73/8.34 greater(age(sK4_skl,sK7_skl),sigma)|age(sK4_skl,sK7_skl)=sigma),
% 62.73/8.34 inference(resolution,[status(thm)],[f540,f29])).
% 62.73/8.34 fof(f932,definition,(
% 62.73/8.34 sQ50_spl <=> (greater(age(sK4_skl,sK7_skl),sigma))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f935,definition,(
% 62.73/8.34 sQ51_spl <=> (age(sK4_skl,sK7_skl)=sigma)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f936,plain,(
% 62.73/8.34 age(sK4_skl,sK7_skl)=sigma|~sQ51_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f935])).
% 62.73/8.34 fof(f938,plain,(
% 62.73/8.34 sQ50_spl|sQ51_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f931,f932,f935])).
% 62.73/8.34 fof(f942,plain,(
% 62.73/8.34 greater(sigma,sigma)|~sQ51_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f936,f104])).
% 62.73/8.34 fof(f948,plain,(
% 62.73/8.34 $false|~sQ51_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f942,f905])).
% 62.73/8.34 fof(f949,plain,(
% 62.73/8.34 ~sQ51_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f948])).
% 62.73/8.34 fof(f953,plain,(
% 62.73/8.34 ![X0]: (~greater(X0,tau)|~smaller(X0,sigma)|~sQ30_spl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f572,f34])).
% 62.73/8.34 fof(f955,plain,(
% 62.73/8.34 ~greater(age(sK4_skl,sK6_skl),sigma)|~sQ5_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f187,f129])).
% 62.73/8.34 fof(f961,definition,(
% 62.73/8.34 sQ52_spl <=> (greater(zero,sigma))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f966,plain,(
% 62.73/8.34 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2|~organization(X0)|~age(X0,X1)=zero)),
% 62.73/8.34 inference(resolution,[status(thm)],[f86,f65])).
% 62.73/8.34 fof(f967,plain,(
% 62.73/8.34 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2|~age(X0,X1)=zero)),
% 62.73/8.34 inference(duplicate_literals_removal,[status(thm)],[f966])).
% 62.73/8.34 fof(f976,plain,(
% 62.73/8.34 age(sK4_skl,sK8_skl)=tau|greater_or_equal(age(sK4_skl,sK8_skl),tau)),
% 62.73/8.34 inference(resolution,[status(thm)],[f772,f209])).
% 62.73/8.34 fof(f979,definition,(
% 62.73/8.34 sQ53_spl <=> (greater_or_equal(age(sK4_skl,sK8_skl),tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f982,plain,(
% 62.73/8.34 sQ47_spl|sQ53_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f976,f776,f979])).
% 62.73/8.34 fof(f983,plain,(
% 62.73/8.34 greater(age(sK4_skl,sK8_skl),tau)|age(sK4_skl,sK8_skl)=tau),
% 62.73/8.34 inference(resolution,[status(thm)],[f424,f29])).
% 62.73/8.34 fof(f984,definition,(
% 62.73/8.34 sQ54_spl <=> (greater(age(sK4_skl,sK8_skl),tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f987,plain,(
% 62.73/8.34 sQ54_spl|sQ47_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f983,f984,f776])).
% 62.73/8.34 fof(f991,plain,(
% 62.73/8.34 ![X0,X1]: (X0=X1|greater_or_equal(X1,X0)|greater(X0,X1)|X0=X1)),
% 62.73/8.34 inference(resolution,[status(thm)],[f638,f29])).
% 62.73/8.34 fof(f994,plain,(
% 62.73/8.34 ![X0,X1]: (X0=X1|greater_or_equal(X1,X0)|greater(X0,X1))),
% 62.73/8.34 inference(duplicate_literals_removal,[status(thm)],[f991])).
% 62.73/8.34 fof(f999,plain,(
% 62.73/8.34 ~greater(very_low,mod2)),
% 62.73/8.34 inference(resolution,[status(thm)],[f201,f90])).
% 62.73/8.34 fof(f1002,plain,(
% 62.73/8.34 ![X0]: (~greater(X0,mod2)|~smaller(X0,low))),
% 62.73/8.34 inference(resolution,[status(thm)],[f201,f34])).
% 62.73/8.34 fof(f1003,plain,(
% 62.73/8.34 smaller(very_low,mod2)|very_low=mod2),
% 62.73/8.34 inference(resolution,[status(thm)],[f999,f41])).
% 62.73/8.34 fof(f1004,plain,(
% 62.73/8.34 ![X0]: (~greater(very_low,X0)|~greater(X0,mod2))),
% 62.73/8.34 inference(resolution,[status(thm)],[f999,f40])).
% 62.73/8.34 fof(f1005,plain,(
% 62.73/8.34 ~smaller(mod2,very_low)),
% 62.73/8.34 inference(resolution,[status(thm)],[f999,f34])).
% 62.73/8.34 fof(f1006,definition,(
% 62.73/8.34 sQ55_spl <=> (smaller(very_low,mod2))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1007,plain,(
% 62.73/8.34 smaller(very_low,mod2)|~sQ55_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1006])).
% 62.73/8.34 fof(f1009,definition,(
% 62.73/8.34 sQ56_spl <=> (very_low=mod2)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1010,plain,(
% 62.73/8.34 very_low=mod2|~sQ56_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1009])).
% 62.73/8.34 fof(f1012,plain,(
% 62.73/8.34 sQ55_spl|sQ56_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1003,f1006,f1009])).
% 62.73/8.34 fof(f1022,plain,(
% 62.73/8.34 ~greater(low,very_low)|~sQ56_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f1010,f138])).
% 62.73/8.34 fof(f1047,plain,(
% 62.73/8.34 $false|~sQ56_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f1022,f90])).
% 62.73/8.34 fof(f1048,plain,(
% 62.73/8.34 ~sQ56_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f1047])).
% 62.73/8.34 fof(f1160,plain,(
% 62.73/8.34 greater_or_equal(mod2,very_low)|~sQ55_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1007,f154])).
% 62.73/8.34 fof(f1165,plain,(
% 62.73/8.34 mod2=very_low|greater_or_equal(mod2,very_low)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1005,f209])).
% 62.73/8.34 fof(f1168,definition,(
% 62.73/8.34 sQ58_spl <=> (greater_or_equal(mod2,very_low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1171,plain,(
% 62.73/8.34 sQ56_spl|sQ58_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1165,f1009,f1168])).
% 62.73/8.34 fof(f1174,plain,(
% 62.73/8.34 $false|sQ36_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f642,f613])).
% 62.73/8.34 fof(f1175,plain,(
% 62.73/8.34 sQ36_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f1174])).
% 62.73/8.34 fof(f1220,plain,(
% 62.73/8.34 sQ34_spl|~sQ31_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f487,f591,f481])).
% 62.73/8.34 fof(f1226,plain,(
% 62.73/8.34 greater(mod2,very_low)|mod2=very_low|~sQ55_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1160,f29])).
% 62.73/8.34 fof(f1227,definition,(
% 62.73/8.34 sQ59_spl <=> (greater(mod2,very_low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1228,plain,(
% 62.73/8.34 greater(mod2,very_low)|~sQ59_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1227])).
% 62.73/8.34 fof(f1230,plain,(
% 62.73/8.34 sQ59_spl|sQ56_spl|~sQ55_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1226,f1227,f1009,f1006])).
% 62.73/8.34 fof(f1261,plain,(
% 62.73/8.34 greater(tau,sigma)|tau=sigma),
% 62.73/8.34 inference(resolution,[status(thm)],[f613,f29])).
% 62.73/8.34 fof(f1262,plain,(
% 62.73/8.34 sQ30_spl|sQ31_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1261,f478,f481])).
% 62.73/8.34 fof(f1263,plain,(
% 62.73/8.34 smaller(sigma,tau)|sigma=tau),
% 62.73/8.34 inference(resolution,[status(thm)],[f584,f41])).
% 62.73/8.34 fof(f1266,plain,(
% 62.73/8.34 sQ33_spl|sQ31_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1263,f574,f481])).
% 62.73/8.34 fof(f1304,plain,(
% 62.73/8.34 ~greater(very_low,mod1)),
% 62.73/8.34 inference(resolution,[status(thm)],[f195,f90])).
% 62.73/8.34 fof(f1308,plain,(
% 62.73/8.34 smaller(very_low,mod1)|very_low=mod1),
% 62.73/8.34 inference(resolution,[status(thm)],[f1304,f41])).
% 62.73/8.34 fof(f1310,plain,(
% 62.73/8.34 ~smaller(mod1,very_low)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1304,f34])).
% 62.73/8.34 fof(f1311,definition,(
% 62.73/8.34 sQ61_spl <=> (smaller(very_low,mod1))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1312,plain,(
% 62.73/8.34 smaller(very_low,mod1)|~sQ61_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1311])).
% 62.73/8.34 fof(f1314,definition,(
% 62.73/8.34 sQ62_spl <=> (very_low=mod1)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1315,plain,(
% 62.73/8.34 very_low=mod1|~sQ62_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1314])).
% 62.73/8.34 fof(f1316,plain,(
% 62.73/8.34 ~very_low=mod1|sQ62_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1314])).
% 62.73/8.34 fof(f1317,plain,(
% 62.73/8.34 sQ61_spl|sQ62_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1308,f1311,f1314])).
% 62.73/8.34 fof(f1328,plain,(
% 62.73/8.34 greater(very_low,low)|~sQ62_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f1315,f89])).
% 62.73/8.34 fof(f1351,plain,(
% 62.73/8.34 $false|~sQ62_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f1328,f134])).
% 62.73/8.34 fof(f1352,plain,(
% 62.73/8.34 ~sQ62_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f1351])).
% 62.73/8.34 fof(f1357,plain,(
% 62.73/8.34 ![X0,X1]: (dissimilar(sK4_skl,X0,X1)|is_aligned(sK4_skl,X1)|~age(sK4_skl,X0)=zero)),
% 62.73/8.34 inference(resolution,[status(thm)],[f420,f96])).
% 62.73/8.34 fof(f1401,plain,(
% 62.73/8.34 ![X0,X1]: (~age(sK4_skl,X0)=zero|~greater(age(sK4_skl,X1),sigma)|~age(sK4_skl,X0)=zero|greater(age(sK4_skl,X1),sigma))),
% 62.73/8.34 inference(resolution,[status(thm)],[f509,f121])).
% 62.73/8.34 fof(f1402,plain,(
% 62.73/8.34 ![X0,X1]: (~age(sK4_skl,X0)=zero|~greater(age(sK4_skl,X1),sigma)|~is_aligned(sK4_skl,X0)|~is_aligned(sK4_skl,X1))),
% 62.73/8.34 inference(resolution,[status(thm)],[f509,f61])).
% 62.73/8.34 fof(f1404,plain,(
% 62.73/8.34 ![X0,X1]: (~age(sK4_skl,X0)=zero|~greater(age(sK4_skl,X1),sigma)|organization(sK4_skl))),
% 62.73/8.34 inference(resolution,[status(thm)],[f509,f59])).
% 62.73/8.34 fof(f1405,definition,(
% 62.73/8.34 ![X0]: (sQ63_spl <=> (~age(sK4_skl,X0)=zero|~age(sK4_skl,X0)=zero))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1406,plain,(
% 62.73/8.34 ![X0]: (~age(sK4_skl,X0)=zero|~age(sK4_skl,X0)=zero|~sQ63_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1405])).
% 62.73/8.34 fof(f1408,definition,(
% 62.73/8.34 ![X1]: (sQ64_spl <=> (~greater(age(sK4_skl,X1),sigma)|greater(age(sK4_skl,X1),sigma)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1411,plain,(
% 62.73/8.34 sQ63_spl|sQ64_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1401,f1405,f1408])).
% 62.73/8.34 fof(f1412,definition,(
% 62.73/8.34 ![X0]: (sQ65_spl <=> (~age(sK4_skl,X0)=zero|~is_aligned(sK4_skl,X0)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1413,plain,(
% 62.73/8.34 ![X0]: (~age(sK4_skl,X0)=zero|~is_aligned(sK4_skl,X0)|~sQ65_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1412])).
% 62.73/8.34 fof(f1415,definition,(
% 62.73/8.34 ![X1]: (sQ66_spl <=> (~greater(age(sK4_skl,X1),sigma)|~is_aligned(sK4_skl,X1)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1416,plain,(
% 62.73/8.34 ![X0]: (~greater(age(sK4_skl,X0),sigma)|~is_aligned(sK4_skl,X0)|~sQ66_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1415])).
% 62.73/8.34 fof(f1418,plain,(
% 62.73/8.34 sQ65_spl|sQ66_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1402,f1412,f1415])).
% 62.73/8.34 fof(f1419,definition,(
% 62.73/8.34 ![X0]: (sQ67_spl <=> (~age(sK4_skl,X0)=zero|is_aligned(sK4_skl,X0)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1420,plain,(
% 62.73/8.34 ![X0]: (~age(sK4_skl,X0)=zero|is_aligned(sK4_skl,X0)|~sQ67_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1419])).
% 62.73/8.34 fof(f1422,definition,(
% 62.73/8.34 ![X1]: (sQ68_spl <=> (~greater(age(sK4_skl,X1),sigma)|is_aligned(sK4_skl,X1)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1423,plain,(
% 62.73/8.34 ![X0]: (~greater(age(sK4_skl,X0),sigma)|is_aligned(sK4_skl,X0)|~sQ68_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1422])).
% 62.73/8.34 fof(f1426,definition,(
% 62.73/8.34 ![X0]: (sQ69_spl <=> (~age(sK4_skl,X0)=zero))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1427,plain,(
% 62.73/8.34 ![X0]: (~age(sK4_skl,X0)=zero|~sQ69_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1426])).
% 62.73/8.34 fof(f1429,definition,(
% 62.73/8.34 ![X1]: (sQ70_spl <=> (~greater(age(sK4_skl,X1),sigma)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1430,plain,(
% 62.73/8.34 ![X0]: (~greater(age(sK4_skl,X0),sigma)|~sQ70_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1429])).
% 62.73/8.34 fof(f1432,definition,(
% 62.73/8.34 sQ71_spl <=> (organization(sK4_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1435,plain,(
% 62.73/8.34 sQ69_spl|sQ70_spl|sQ71_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1404,f1426,f1429,f1432])).
% 62.73/8.34 fof(f1438,plain,(
% 62.73/8.34 ![X0]: (~age(sK4_skl,X0)=zero|~sQ63_spl)),
% 62.73/8.34 inference(duplicate_literals_removal,[status(thm)],[f1406])).
% 62.73/8.34 fof(f1439,plain,(
% 62.73/8.34 $false|~sQ70_spl),
% 62.73/8.34 inference(backward_subsumption_resolution,[status(thm)],[f104,f1430])).
% 62.73/8.34 fof(f1441,plain,(
% 62.73/8.34 ~sQ70_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f1439])).
% 62.73/8.34 fof(f1442,plain,(
% 62.73/8.34 $false|~sQ69_spl),
% 62.73/8.34 inference(backward_subsumption_resolution,[status(thm)],[f99,f1427])).
% 62.73/8.34 fof(f1443,plain,(
% 62.73/8.34 $false|~sQ66_spl|~sQ68_spl),
% 62.73/8.34 inference(backward_subsumption_resolution,[status(thm)],[f104,f1444])).
% 62.73/8.34 fof(f1444,plain,(
% 62.73/8.34 ![X0]: (~greater(age(sK4_skl,X0),sigma)|~sQ66_spl|~sQ68_spl)),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f1423,f1416])).
% 62.73/8.34 fof(f1445,plain,(
% 62.73/8.34 ~sQ69_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f1442])).
% 62.73/8.34 fof(f1446,plain,(
% 62.73/8.34 ~sQ66_spl|~sQ68_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f1443])).
% 62.73/8.34 fof(f1447,plain,(
% 62.73/8.34 sQ69_spl|~sQ63_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1438,f1426,f1405])).
% 62.73/8.34 fof(f1450,plain,(
% 62.73/8.34 smaller(sigma,age(sK4_skl,sK7_skl))|sigma=age(sK4_skl,sK7_skl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f541,f41])).
% 62.73/8.34 fof(f1453,definition,(
% 62.73/8.34 sQ72_spl <=> (smaller(sigma,age(sK4_skl,sK7_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1456,plain,(
% 62.73/8.34 sQ72_spl|sQ51_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1450,f1453,f935])).
% 62.73/8.34 fof(f1484,plain,(
% 62.73/8.34 greater_or_equal(mod1,very_low)|~sQ61_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1312,f154])).
% 62.73/8.34 fof(f1489,plain,(
% 62.73/8.34 mod1=very_low|greater_or_equal(mod1,very_low)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1310,f209])).
% 62.73/8.34 fof(f1492,definition,(
% 62.73/8.34 sQ73_spl <=> (greater_or_equal(mod1,very_low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1495,plain,(
% 62.73/8.34 sQ62_spl|sQ73_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1489,f1314,f1492])).
% 62.73/8.34 fof(f1496,plain,(
% 62.73/8.34 greater(mod1,very_low)|mod1=very_low|~sQ61_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1484,f29])).
% 62.73/8.34 fof(f1497,definition,(
% 62.73/8.34 sQ74_spl <=> (greater(mod1,very_low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1498,plain,(
% 62.73/8.34 greater(mod1,very_low)|~sQ74_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1497])).
% 62.73/8.34 fof(f1500,plain,(
% 62.73/8.34 sQ74_spl|sQ62_spl|~sQ61_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1496,f1497,f1314,f1311])).
% 62.73/8.34 fof(f1512,definition,(
% 62.73/8.34 sQ75_spl <=> (greater(very_low,low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1524,plain,(
% 62.73/8.34 sigma=age(sK4_skl,sK7_skl)|greater_or_equal(age(sK4_skl,sK7_skl),sigma)),
% 62.73/8.34 inference(resolution,[status(thm)],[f994,f541])).
% 62.73/8.34 fof(f1546,definition,(
% 62.73/8.34 sQ77_spl <=> (greater_or_equal(age(sK4_skl,sK7_skl),sigma))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1549,plain,(
% 62.73/8.34 sQ51_spl|sQ77_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1524,f935,f1546])).
% 62.73/8.34 fof(f1568,plain,(
% 62.73/8.34 ![X0]: (~greater(X0,mod2)|very_low=X0|greater_or_equal(X0,very_low))),
% 62.73/8.34 inference(resolution,[status(thm)],[f1004,f994])).
% 62.73/8.34 fof(f1569,plain,(
% 62.73/8.34 ![X0]: (~greater(X0,mod2)|smaller(very_low,X0)|very_low=X0)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1004,f41])).
% 62.73/8.34 fof(f1572,plain,(
% 62.73/8.34 ~smaller(high,low)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1002,f91])).
% 62.73/8.34 fof(f1578,plain,(
% 62.73/8.34 smaller(low,high)|low=high),
% 62.73/8.34 inference(resolution,[status(thm)],[f1572,f211])).
% 62.73/8.34 fof(f1580,plain,(
% 62.73/8.34 high=low|greater_or_equal(high,low)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1572,f209])).
% 62.73/8.34 fof(f1581,definition,(
% 62.73/8.34 sQ78_spl <=> (smaller(low,high))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1582,plain,(
% 62.73/8.34 smaller(low,high)|~sQ78_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1581])).
% 62.73/8.34 fof(f1584,definition,(
% 62.73/8.34 sQ79_spl <=> (low=high)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1585,plain,(
% 62.73/8.34 low=high|~sQ79_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1584])).
% 62.73/8.34 fof(f1587,plain,(
% 62.73/8.34 sQ78_spl|sQ79_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1578,f1581,f1584])).
% 62.73/8.34 fof(f1589,definition,(
% 62.73/8.34 sQ80_spl <=> (greater_or_equal(high,low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1590,plain,(
% 62.73/8.34 greater_or_equal(high,low)|~sQ80_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1589])).
% 62.73/8.34 fof(f1592,plain,(
% 62.73/8.34 sQ79_spl|sQ80_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1580,f1584,f1589])).
% 62.73/8.34 fof(f1597,plain,(
% 62.73/8.34 ~smaller(mod1,high)|~sQ79_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f1585,f196])).
% 62.73/8.34 fof(f1643,plain,(
% 62.73/8.34 $false|~sQ79_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f1597,f131])).
% 62.73/8.34 fof(f1644,plain,(
% 62.73/8.34 ~sQ79_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f1643])).
% 62.73/8.34 fof(f1678,plain,(
% 62.73/8.34 ![X0]: (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|~organization(sK4_skl)|has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2)),
% 62.73/8.34 inference(resolution,[status(thm)],[f616,f86])).
% 62.73/8.34 fof(f1679,plain,(
% 62.73/8.34 ![X0,X1]: (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|dissimilar(sK4_skl,X1,X0)|~organization(sK4_skl)|is_aligned(sK4_skl,X1))),
% 62.73/8.34 inference(resolution,[status(thm)],[f616,f63])).
% 62.73/8.34 fof(f1680,plain,(
% 62.73/8.34 ![X0,X1]: (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|dissimilar(sK4_skl,X0,X1)|~organization(sK4_skl)|is_aligned(sK4_skl,X1))),
% 62.73/8.34 inference(resolution,[status(thm)],[f616,f62])).
% 62.73/8.34 fof(f1681,definition,(
% 62.73/8.34 ![X0]: (sQ81_spl <=> (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1682,plain,(
% 62.73/8.34 ![X0]: (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2|~sQ81_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1681])).
% 62.73/8.34 fof(f1684,plain,(
% 62.73/8.34 sQ81_spl|~sQ71_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1678,f1681,f1432])).
% 62.73/8.34 fof(f1685,definition,(
% 62.73/8.34 ![X0,X1]: (sQ82_spl <=> (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|dissimilar(sK4_skl,X1,X0)|is_aligned(sK4_skl,X1)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1688,plain,(
% 62.73/8.34 sQ82_spl|~sQ71_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1679,f1685,f1432])).
% 62.73/8.34 fof(f1689,definition,(
% 62.73/8.34 ![X0,X1]: (sQ83_spl <=> (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|dissimilar(sK4_skl,X0,X1)|is_aligned(sK4_skl,X1)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1692,plain,(
% 62.73/8.34 sQ83_spl|~sQ71_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1680,f1689,f1432])).
% 62.73/8.34 fof(f1693,plain,(
% 62.73/8.34 ![X0]: (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|~sQ81_spl)),
% 62.73/8.34 inference(duplicate_literals_removal,[status(thm)],[f1682])).
% 62.73/8.34 fof(f1732,plain,(
% 62.73/8.34 ![X0]: (has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero)),
% 62.73/8.34 inference(resolution,[status(thm)],[f967,f96])).
% 62.73/8.34 fof(f1752,plain,(
% 62.73/8.34 greater(high,low)|high=low|~sQ80_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1590,f29])).
% 62.73/8.34 fof(f1753,definition,(
% 62.73/8.34 sQ84_spl <=> (greater(high,low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1754,plain,(
% 62.73/8.34 greater(high,low)|~sQ84_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1753])).
% 62.73/8.34 fof(f1756,plain,(
% 62.73/8.34 sQ84_spl|sQ79_spl|~sQ80_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1752,f1753,f1584,f1589])).
% 62.73/8.34 fof(f1758,plain,(
% 62.73/8.34 ~greater(low,high)|~sQ78_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1582,f129])).
% 62.73/8.34 fof(f1776,definition,(
% 62.73/8.34 sQ85_spl <=> (greater(mod2,high))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1831,plain,(
% 62.73/8.34 ~greater(age(sK4_skl,sK6_skl),tau)|~sQ30_spl|~sQ5_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f953,f187])).
% 62.73/8.34 fof(f1839,definition,(
% 62.73/8.34 sQ88_spl <=> (greater(sigma,tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1869,definition,(
% 62.73/8.34 sQ89_spl <=> (greater(mod1,high))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1897,definition,(
% 62.73/8.34 sQ91_spl <=> (greater(very_low,mod2))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1950,definition,(
% 62.73/8.34 sQ94_spl <=> (greater(low,mod1))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1963,plain,(
% 62.73/8.34 age(sK4_skl,sK6_skl)=tau|greater_or_equal(tau,age(sK4_skl,sK6_skl))|~sQ30_spl|~sQ5_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1831,f994])).
% 62.73/8.34 fof(f1967,definition,(
% 62.73/8.34 sQ96_spl <=> (age(sK4_skl,sK6_skl)=tau)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1968,plain,(
% 62.73/8.34 age(sK4_skl,sK6_skl)=tau|~sQ96_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1967])).
% 62.73/8.34 fof(f1970,definition,(
% 62.73/8.34 sQ97_spl <=> (greater_or_equal(tau,age(sK4_skl,sK6_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1971,plain,(
% 62.73/8.34 greater_or_equal(tau,age(sK4_skl,sK6_skl))|~sQ97_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f1970])).
% 62.73/8.34 fof(f1973,plain,(
% 62.73/8.34 sQ96_spl|sQ97_spl|~sQ30_spl|~sQ5_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1963,f1967,f1970,f478,f186])).
% 62.73/8.34 fof(f1974,definition,(
% 62.73/8.34 sQ98_spl <=> (smaller(age(sK4_skl,sK6_skl),tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f1979,plain,(
% 62.73/8.34 ~greater(tau,sigma)|~sQ96_spl|~sQ5_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f1968,f955])).
% 62.73/8.34 fof(f2007,plain,(
% 62.73/8.34 ~sQ30_spl|~sQ96_spl|~sQ5_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f1979,f478,f1967,f186])).
% 62.73/8.34 fof(f2033,plain,(
% 62.73/8.34 positional_advantage(sK4_skl,sK8_skl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f732,f106])).
% 62.73/8.34 fof(f2037,plain,(
% 62.73/8.34 ![X0]: (positional_advantage(sK4_skl,X0)|smaller(age(sK4_skl,X0),tau)|age(sK4_skl,X0)=tau)),
% 62.73/8.34 inference(resolution,[status(thm)],[f732,f41])).
% 62.73/8.34 fof(f2038,plain,(
% 62.73/8.34 ![X0,X1]: (positional_advantage(sK4_skl,X0)|~greater(age(sK4_skl,X0),X1)|~greater(X1,tau))),
% 62.73/8.34 inference(resolution,[status(thm)],[f732,f40])).
% 62.73/8.34 fof(f2039,plain,(
% 62.73/8.34 ![X0]: (positional_advantage(sK4_skl,X0)|~smaller(tau,age(sK4_skl,X0)))),
% 62.73/8.34 inference(resolution,[status(thm)],[f732,f34])).
% 62.73/8.34 fof(f2045,definition,(
% 62.73/8.34 sQ100_spl <=> (robust_position(sK4_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2047,plain,(
% 62.73/8.34 ~robust_position(sK4_skl)|sQ100_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2045])).
% 62.73/8.34 fof(f2056,definition,(
% 62.73/8.34 sQ103_spl <=> (positional_advantage(sK4_skl,sK6_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2057,plain,(
% 62.73/8.34 positional_advantage(sK4_skl,sK6_skl)|~sQ103_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2056])).
% 62.73/8.34 fof(f2060,definition,(
% 62.73/8.34 sQ104_spl <=> (positional_advantage(sK4_skl,sK5_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2061,plain,(
% 62.73/8.34 positional_advantage(sK4_skl,sK5_skl)|~sQ104_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2060])).
% 62.73/8.34 fof(f2065,plain,(
% 62.73/8.34 ~organization(sK4_skl)|has_immunity(sK4_skl,sK8_skl)|is_aligned(sK4_skl,sK8_skl)|hazard_of_mortality(sK4_skl,sK8_skl)=mod1),
% 62.73/8.34 inference(resolution,[status(thm)],[f2033,f85])).
% 62.73/8.34 fof(f2066,plain,(
% 62.73/8.34 ~robust_position(sK4_skl)|~smaller_or_equal(age(sK4_skl,sK8_skl),tau)),
% 62.73/8.34 inference(resolution,[status(thm)],[f2033,f75])).
% 62.73/8.34 fof(f2067,definition,(
% 62.73/8.34 sQ105_spl <=> (has_immunity(sK4_skl,sK8_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2068,plain,(
% 62.73/8.34 has_immunity(sK4_skl,sK8_skl)|~sQ105_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2067])).
% 62.73/8.34 fof(f2070,definition,(
% 62.73/8.34 sQ106_spl <=> (is_aligned(sK4_skl,sK8_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2071,plain,(
% 62.73/8.34 is_aligned(sK4_skl,sK8_skl)|~sQ106_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2070])).
% 62.73/8.34 fof(f2073,definition,(
% 62.73/8.34 sQ107_spl <=> (hazard_of_mortality(sK4_skl,sK8_skl)=low)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2074,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK8_skl)=low|~sQ107_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2073])).
% 62.73/8.34 fof(f2077,definition,(
% 62.73/8.34 sQ108_spl <=> (hazard_of_mortality(sK4_skl,sK8_skl)=mod1)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2078,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK8_skl)=mod1|~sQ108_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2077])).
% 62.73/8.34 fof(f2080,plain,(
% 62.73/8.34 ~sQ71_spl|sQ105_spl|sQ106_spl|sQ108_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2065,f1432,f2067,f2070,f2077])).
% 62.73/8.34 fof(f2081,definition,(
% 62.73/8.34 sQ109_spl <=> (smaller_or_equal(age(sK4_skl,sK8_skl),tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2084,plain,(
% 62.73/8.34 ~sQ100_spl|~sQ109_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2066,f2045,f2081])).
% 62.73/8.34 fof(f2085,plain,(
% 62.73/8.34 low=mod1|~sQ107_spl|~sQ108_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f2074,f2078])).
% 62.73/8.34 fof(f2086,plain,(
% 62.73/8.34 $false|sQ100_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f2047,f97])).
% 62.73/8.34 fof(f2087,plain,(
% 62.73/8.34 sQ100_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f2086])).
% 62.73/8.34 fof(f2088,plain,(
% 62.73/8.34 sQ14_spl|~sQ107_spl|~sQ108_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2085,f236,f2073,f2077])).
% 62.73/8.34 fof(f2091,plain,(
% 62.73/8.34 ~robust_position(sK4_skl)|~smaller_or_equal(age(sK4_skl,sK5_skl),tau)|~sQ104_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2061,f75])).
% 62.73/8.34 fof(f2092,definition,(
% 62.73/8.34 sQ110_spl <=> (has_immunity(sK4_skl,sK5_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2093,plain,(
% 62.73/8.34 has_immunity(sK4_skl,sK5_skl)|~sQ110_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2092])).
% 62.73/8.34 fof(f2094,plain,(
% 62.73/8.34 ~has_immunity(sK4_skl,sK5_skl)|sQ110_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2092])).
% 62.73/8.34 fof(f2095,definition,(
% 62.73/8.34 sQ111_spl <=> (is_aligned(sK4_skl,sK5_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2096,plain,(
% 62.73/8.34 is_aligned(sK4_skl,sK5_skl)|~sQ111_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2095])).
% 62.73/8.34 fof(f2106,definition,(
% 62.73/8.34 sQ114_spl <=> (smaller_or_equal(age(sK4_skl,sK5_skl),tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2107,plain,(
% 62.73/8.34 smaller_or_equal(age(sK4_skl,sK5_skl),tau)|~sQ114_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2106])).
% 62.73/8.34 fof(f2108,plain,(
% 62.73/8.34 ~smaller_or_equal(age(sK4_skl,sK5_skl),tau)|sQ114_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2106])).
% 62.73/8.34 fof(f2109,plain,(
% 62.73/8.34 ~sQ100_spl|~sQ114_spl|~sQ104_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2091,f2045,f2106,f2060])).
% 62.73/8.34 fof(f2110,plain,(
% 62.73/8.34 ~smaller_or_equal(zero,tau)|sQ114_spl),
% 62.73/8.34 inference(forward_demodulation,[status(thm)],[f99,f2108])).
% 62.73/8.34 fof(f2116,plain,(
% 62.73/8.34 ~robust_position(sK4_skl)|~smaller_or_equal(age(sK4_skl,sK6_skl),tau)|~sQ103_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2057,f75])).
% 62.73/8.34 fof(f2117,definition,(
% 62.73/8.34 sQ115_spl <=> (has_immunity(sK4_skl,sK6_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2118,plain,(
% 62.73/8.34 has_immunity(sK4_skl,sK6_skl)|~sQ115_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2117])).
% 62.73/8.34 fof(f2120,definition,(
% 62.73/8.34 sQ116_spl <=> (is_aligned(sK4_skl,sK6_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2121,plain,(
% 62.73/8.34 is_aligned(sK4_skl,sK6_skl)|~sQ116_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2120])).
% 62.73/8.34 fof(f2122,plain,(
% 62.73/8.34 ~is_aligned(sK4_skl,sK6_skl)|sQ116_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2120])).
% 62.73/8.34 fof(f2127,definition,(
% 62.73/8.34 sQ118_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=mod1)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2128,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK6_skl)=mod1|~sQ118_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2127])).
% 62.73/8.34 fof(f2131,definition,(
% 62.73/8.34 sQ119_spl <=> (smaller_or_equal(age(sK4_skl,sK6_skl),tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2133,plain,(
% 62.73/8.34 ~smaller_or_equal(age(sK4_skl,sK6_skl),tau)|sQ119_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2131])).
% 62.73/8.34 fof(f2134,plain,(
% 62.73/8.34 ~sQ100_spl|~sQ119_spl|~sQ103_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2116,f2045,f2131,f2056])).
% 62.73/8.34 fof(f2135,plain,(
% 62.73/8.34 ~smaller_or_equal(sigma,tau)|~sQ6_spl|sQ119_spl),
% 62.73/8.34 inference(forward_demodulation,[status(thm)],[f190,f2133])).
% 62.73/8.34 fof(f2140,plain,(
% 62.73/8.34 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ105_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2068,f55])).
% 62.73/8.34 fof(f2141,definition,(
% 62.73/8.34 sQ120_spl <=> (hazard_of_mortality(sK4_skl,sK8_skl)=very_low)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2142,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK8_skl)=very_low|~sQ120_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2141])).
% 62.73/8.34 fof(f2145,definition,(
% 62.73/8.34 sQ121_spl <=> (has_endowment(sK4_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2146,plain,(
% 62.73/8.34 has_endowment(sK4_skl)|~sQ121_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2145])).
% 62.73/8.34 fof(f2148,plain,(
% 62.73/8.34 ~sQ71_spl|sQ121_spl|~sQ105_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2140,f1432,f2145,f2067])).
% 62.73/8.34 fof(f2150,plain,(
% 62.73/8.34 $false|~sQ121_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f2146,f98])).
% 62.73/8.34 fof(f2151,plain,(
% 62.73/8.34 ~sQ121_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f2150])).
% 62.73/8.34 fof(f2152,plain,(
% 62.73/8.34 very_low=mod1|~sQ120_spl|~sQ108_spl),
% 62.73/8.34 inference(forward_demodulation,[status(thm)],[f2142,f2078])).
% 62.73/8.34 fof(f2153,plain,(
% 62.73/8.34 $false|sQ62_spl|~sQ120_spl|~sQ108_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f2152,f1316])).
% 62.73/8.34 fof(f2154,plain,(
% 62.73/8.34 sQ62_spl|~sQ120_spl|~sQ108_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f2153])).
% 62.73/8.34 fof(f2158,plain,(
% 62.73/8.34 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ110_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2093,f55])).
% 62.73/8.34 fof(f2163,plain,(
% 62.73/8.34 ~sQ71_spl|sQ121_spl|~sQ110_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2158,f1432,f2145,f2092])).
% 62.73/8.34 fof(f2166,plain,(
% 62.73/8.34 ~smaller(zero,tau)|sQ114_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2110,f25])).
% 62.73/8.34 fof(f2167,plain,(
% 62.73/8.34 $false|sQ114_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f2166,f122])).
% 62.73/8.34 fof(f2168,plain,(
% 62.73/8.34 sQ114_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f2167])).
% 62.73/8.34 fof(f2169,plain,(
% 62.73/8.34 smaller_or_equal(zero,tau)|~sQ114_spl),
% 62.73/8.34 inference(forward_demodulation,[status(thm)],[f99,f2107])).
% 62.73/8.34 fof(f2171,plain,(
% 62.73/8.34 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ115_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2118,f55])).
% 62.73/8.34 fof(f2172,definition,(
% 62.73/8.34 sQ123_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=very_low)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2173,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK6_skl)=very_low|~sQ123_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2172])).
% 62.73/8.34 fof(f2176,plain,(
% 62.73/8.34 ~sQ71_spl|sQ121_spl|~sQ115_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2171,f1432,f2145,f2117])).
% 62.73/8.34 fof(f2179,plain,(
% 62.73/8.34 ~smaller(mod1,hazard_of_mortality(sK4_skl,sK6_skl))|~sQ108_spl|sQ0_spl),
% 62.73/8.34 inference(forward_demodulation,[status(thm)],[f2078,f110])).
% 62.73/8.34 fof(f2181,plain,(
% 62.73/8.34 ~smaller(very_low,hazard_of_mortality(sK4_skl,sK7_skl))|~sQ123_spl|sQ1_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f2173,f113])).
% 62.73/8.34 fof(f2184,plain,(
% 62.73/8.34 smaller(hazard_of_mortality(sK4_skl,sK7_skl),very_low)|hazard_of_mortality(sK4_skl,sK7_skl)=very_low|~sQ123_spl|sQ1_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2181,f211])).
% 62.73/8.34 fof(f2187,definition,(
% 62.73/8.34 sQ124_spl <=> (smaller(hazard_of_mortality(sK4_skl,sK7_skl),very_low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2188,plain,(
% 62.73/8.34 smaller(hazard_of_mortality(sK4_skl,sK7_skl),very_low)|~sQ124_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2187])).
% 62.73/8.34 fof(f2190,definition,(
% 62.73/8.34 sQ125_spl <=> (hazard_of_mortality(sK4_skl,sK7_skl)=very_low)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2191,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK7_skl)=very_low|~sQ125_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2190])).
% 62.73/8.34 fof(f2193,plain,(
% 62.73/8.34 sQ124_spl|sQ125_spl|~sQ123_spl|sQ1_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2184,f2187,f2190,f2172,f111])).
% 62.73/8.34 fof(f2195,definition,(
% 62.73/8.34 sQ126_spl <=> (greater_or_equal(very_low,hazard_of_mortality(sK4_skl,sK7_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2196,plain,(
% 62.73/8.34 greater_or_equal(very_low,hazard_of_mortality(sK4_skl,sK7_skl))|~sQ126_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2195])).
% 62.73/8.34 fof(f2197,plain,(
% 62.73/8.34 ~greater_or_equal(very_low,hazard_of_mortality(sK4_skl,sK7_skl))|sQ126_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2195])).
% 62.73/8.34 fof(f2206,plain,(
% 62.73/8.34 mod1=hazard_of_mortality(sK4_skl,sK6_skl)|greater_or_equal(mod1,hazard_of_mortality(sK4_skl,sK6_skl))|~sQ108_spl|sQ0_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2179,f209])).
% 62.73/8.34 fof(f2212,definition,(
% 62.73/8.34 sQ128_spl <=> (greater_or_equal(mod1,hazard_of_mortality(sK4_skl,sK6_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2213,plain,(
% 62.73/8.34 greater_or_equal(mod1,hazard_of_mortality(sK4_skl,sK6_skl))|~sQ128_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2212])).
% 62.73/8.34 fof(f2215,plain,(
% 62.73/8.34 sQ118_spl|sQ128_spl|~sQ108_spl|sQ0_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2206,f2127,f2212,f2077,f108])).
% 62.73/8.34 fof(f2217,plain,(
% 62.73/8.34 ~smaller(sigma,tau)|~sQ6_spl|sQ119_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2135,f25])).
% 62.73/8.34 fof(f2218,plain,(
% 62.73/8.34 $false|~sQ6_spl|sQ119_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f2217,f102])).
% 62.73/8.34 fof(f2219,plain,(
% 62.73/8.34 ~sQ6_spl|sQ119_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f2218])).
% 62.73/8.34 fof(f2223,definition,(
% 62.73/8.34 sQ129_spl <=> (positional_advantage(sK4_skl,sK8_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2226,definition,(
% 62.73/8.34 sQ130_spl <=> (hazard_of_mortality(sK4_skl,sK8_skl)=high)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2227,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK8_skl)=high|~sQ130_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2226])).
% 62.73/8.34 fof(f2230,definition,(
% 62.73/8.34 sQ131_spl <=> (age(sK4_skl,sK8_skl)=zero)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2231,plain,(
% 62.73/8.34 age(sK4_skl,sK8_skl)=zero|~sQ131_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2230])).
% 62.73/8.34 fof(f2234,plain,(
% 62.73/8.34 high=mod1|~sQ130_spl|~sQ108_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f2227,f2078])).
% 62.73/8.34 fof(f2235,plain,(
% 62.73/8.34 sQ16_spl|~sQ130_spl|~sQ108_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2234,f243,f2226,f2077])).
% 62.73/8.34 fof(f2248,definition,(
% 62.73/8.34 sQ132_spl <=> (has_immunity(sK4_skl,sK3_skl(sK4_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2249,plain,(
% 62.73/8.34 has_immunity(sK4_skl,sK3_skl(sK4_skl))|~sQ132_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2248])).
% 62.73/8.34 fof(f2271,definition,(
% 62.73/8.34 sQ137_spl <=> (has_immunity(sK4_skl,sK2_skl(sK4_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2272,plain,(
% 62.73/8.34 has_immunity(sK4_skl,sK2_skl(sK4_skl))|~sQ137_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2271])).
% 62.73/8.34 fof(f2317,plain,(
% 62.73/8.34 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ132_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2249,f55])).
% 62.73/8.34 fof(f2322,plain,(
% 62.73/8.34 ~sQ71_spl|sQ121_spl|~sQ132_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2317,f1432,f2145,f2248])).
% 62.73/8.34 fof(f2332,plain,(
% 62.73/8.34 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ137_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2272,f55])).
% 62.73/8.34 fof(f2337,plain,(
% 62.73/8.34 ~sQ71_spl|sQ121_spl|~sQ137_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2332,f1432,f2145,f2271])).
% 62.73/8.34 fof(f2379,definition,(
% 62.73/8.34 sQ146_spl <=> (greater(very_low,mod1))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2391,definition,(
% 62.73/8.34 sQ147_spl <=> (greater(mod1,mod2))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2402,definition,(
% 62.73/8.34 sQ148_spl <=> (greater(low,high))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2408,plain,(
% 62.73/8.34 greater(very_low,hazard_of_mortality(sK4_skl,sK7_skl))|very_low=hazard_of_mortality(sK4_skl,sK7_skl)|~sQ126_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2196,f29])).
% 62.73/8.34 fof(f2409,definition,(
% 62.73/8.34 sQ149_spl <=> (greater(very_low,hazard_of_mortality(sK4_skl,sK7_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2410,plain,(
% 62.73/8.34 greater(very_low,hazard_of_mortality(sK4_skl,sK7_skl))|~sQ149_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2409])).
% 62.73/8.34 fof(f2412,plain,(
% 62.73/8.34 sQ149_spl|sQ125_spl|~sQ126_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2408,f2409,f2190,f2195])).
% 62.73/8.34 fof(f2413,plain,(
% 62.73/8.34 greater(mod1,hazard_of_mortality(sK4_skl,sK6_skl))|mod1=hazard_of_mortality(sK4_skl,sK6_skl)|~sQ128_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2213,f29])).
% 62.73/8.34 fof(f2414,definition,(
% 62.73/8.34 sQ150_spl <=> (greater(mod1,hazard_of_mortality(sK4_skl,sK6_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2415,plain,(
% 62.73/8.34 greater(mod1,hazard_of_mortality(sK4_skl,sK6_skl))|~sQ150_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f2414])).
% 62.73/8.34 fof(f2417,plain,(
% 62.73/8.34 sQ150_spl|sQ118_spl|~sQ128_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2413,f2414,f2127,f2212])).
% 62.73/8.34 fof(f2442,plain,(
% 62.73/8.34 ~greater(hazard_of_mortality(sK4_skl,sK7_skl),very_low)|~sQ149_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2410,f37])).
% 62.73/8.34 fof(f2448,plain,(
% 62.73/8.34 ~greater(very_low,low)|~greater(very_low,low)),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f90])).
% 62.73/8.34 fof(f2450,plain,(
% 62.73/8.34 ~greater(low,mod1)|~greater(low,mod1)),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f89])).
% 62.73/8.34 fof(f2452,plain,(
% 62.73/8.34 ~greater(very_low,mod1)|~greater(very_low,mod1)|~sQ74_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f1498])).
% 62.73/8.34 fof(f2456,plain,(
% 62.73/8.34 ~greater(sigma,tau)|~greater(sigma,tau)|~sQ30_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f479])).
% 62.73/8.34 fof(f2458,plain,(
% 62.73/8.34 ~greater(zero,tau)|~greater(zero,tau)),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f101])).
% 62.73/8.34 fof(f2460,plain,(
% 62.73/8.34 ~greater(low,mod2)|~greater(low,mod2)),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f92])).
% 62.73/8.34 fof(f2462,plain,(
% 62.73/8.34 ~greater(mod1,mod2)|~greater(mod1,mod2)),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f93])).
% 62.73/8.34 fof(f2464,plain,(
% 62.73/8.34 ~greater(very_low,mod2)|~greater(very_low,mod2)|~sQ59_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f1228])).
% 62.73/8.34 fof(f2466,plain,(
% 62.73/8.34 ~greater(low,high)|~greater(low,high)|~sQ84_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f1754])).
% 62.73/8.34 fof(f2468,plain,(
% 62.73/8.34 ~greater(mod1,high)|~greater(mod1,high)),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f88])).
% 62.73/8.34 fof(f2470,plain,(
% 62.73/8.34 ~greater(mod2,high)|~greater(mod2,high)),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f91])).
% 62.73/8.34 fof(f2472,plain,(
% 62.73/8.34 ~greater(sigma,age(sK4_skl,sK7_skl))|~greater(sigma,age(sK4_skl,sK7_skl))),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f104])).
% 62.73/8.34 fof(f2474,plain,(
% 62.73/8.34 ~greater(tau,age(sK4_skl,sK8_skl))|~greater(tau,age(sK4_skl,sK8_skl))),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f106])).
% 62.73/8.34 fof(f2480,plain,(
% 62.73/8.34 ~greater(zero,sigma)|~greater(zero,sigma)),
% 62.73/8.34 inference(resolution,[status(thm)],[f887,f100])).
% 62.73/8.34 fof(f2543,plain,(
% 62.73/8.34 ~sQ75_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2448,f1512])).
% 62.73/8.34 fof(f2544,plain,(
% 62.73/8.34 ~sQ94_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2450,f1950])).
% 62.73/8.34 fof(f2545,plain,(
% 62.73/8.34 ~sQ146_spl|~sQ74_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2452,f2379,f1497])).
% 62.73/8.34 fof(f2550,plain,(
% 62.73/8.34 ~sQ88_spl|~sQ30_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2456,f1839,f478])).
% 62.73/8.34 fof(f2551,plain,(
% 62.73/8.34 ~sQ49_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2458,f858])).
% 62.73/8.34 fof(f2552,definition,(
% 62.73/8.34 sQ153_spl <=> (greater(low,mod2))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2555,plain,(
% 62.73/8.34 ~sQ153_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2460,f2552])).
% 62.73/8.34 fof(f2556,plain,(
% 62.73/8.34 ~sQ147_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2462,f2391])).
% 62.73/8.34 fof(f2557,plain,(
% 62.73/8.34 ~sQ91_spl|~sQ59_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2464,f1897,f1227])).
% 62.73/8.34 fof(f2558,plain,(
% 62.73/8.34 ~sQ148_spl|~sQ84_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2466,f2402,f1753])).
% 62.73/8.34 fof(f2559,plain,(
% 62.73/8.34 ~sQ89_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2468,f1869])).
% 62.73/8.34 fof(f2560,plain,(
% 62.73/8.34 ~sQ85_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2470,f1776])).
% 62.73/8.34 fof(f2561,definition,(
% 62.73/8.34 sQ154_spl <=> (greater(sigma,age(sK4_skl,sK7_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2564,plain,(
% 62.73/8.34 ~sQ154_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2472,f2561])).
% 62.73/8.34 fof(f2565,definition,(
% 62.73/8.34 sQ155_spl <=> (greater(tau,age(sK4_skl,sK8_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f2568,plain,(
% 62.73/8.34 ~sQ155_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2474,f2565])).
% 62.73/8.34 fof(f2571,plain,(
% 62.73/8.34 ~sQ52_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f2480,f961])).
% 62.73/8.34 fof(f2578,plain,(
% 62.73/8.34 ![X0]: (~greater(sigma,X0)|~smaller(tau,X0)|~sQ30_spl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f889,f479])).
% 62.73/8.34 fof(f2579,plain,(
% 62.73/8.34 ![X0]: (~greater(zero,X0)|~smaller(tau,X0))),
% 62.73/8.34 inference(resolution,[status(thm)],[f889,f101])).
% 62.73/8.34 fof(f2591,plain,(
% 62.73/8.34 ![X0,X1,X2]: (~greater(X0,X1)|~smaller(X2,X1)|X2=X0|greater_or_equal(X0,X2))),
% 62.73/8.34 inference(resolution,[status(thm)],[f889,f994])).
% 62.73/8.34 fof(f2594,plain,(
% 62.73/8.34 ![X0,X1,X2]: (~greater(X0,X1)|~smaller(X2,X1)|~smaller(X0,X2))),
% 62.73/8.34 inference(resolution,[status(thm)],[f889,f34])).
% 62.73/8.34 fof(f2678,plain,(
% 62.73/8.34 ![X0]: (~smaller(tau,X0)|~smaller(X0,sigma)|~sQ30_spl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f2578,f34])).
% 62.73/8.34 fof(f2679,plain,(
% 62.73/8.34 ![X0]: (~smaller(tau,X0)|zero=X0|greater_or_equal(X0,zero))),
% 62.73/8.34 inference(resolution,[status(thm)],[f2579,f994])).
% 62.73/8.34 fof(f2759,definition,(
% 62.73/8.34 sQ164_spl <=> (smaller(tau,zero))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f3280,plain,(
% 62.73/8.34 ![X0]: (~smaller_or_equal(age(sK4_skl,X0),tau)|~positional_advantage(sK4_skl,X0))),
% 62.73/8.34 inference(resolution,[status(thm)],[f75,f97])).
% 62.73/8.34 fof(f3691,plain,(
% 62.73/8.34 ![X0]: (~age(sK4_skl,X0)=zero|is_aligned(sK4_skl,X0))),
% 62.73/8.34 inference(resolution,[status(thm)],[f65,f96])).
% 62.73/8.34 fof(f3693,plain,(
% 62.73/8.34 $false|~sQ65_spl),
% 62.73/8.34 inference(backward_subsumption_resolution,[status(thm)],[f99,f3694])).
% 62.73/8.34 fof(f3694,plain,(
% 62.73/8.34 ![X0]: (~age(sK4_skl,X0)=zero|~sQ65_spl)),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f3691,f1413])).
% 62.73/8.34 fof(f3695,plain,(
% 62.73/8.34 ~sQ65_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f3693])).
% 62.73/8.34 fof(f4482,definition,(
% 62.73/8.34 sQ202_spl <=> (positional_advantage(sK4_skl,sK7_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4483,plain,(
% 62.73/8.34 positional_advantage(sK4_skl,sK7_skl)|~sQ202_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4482])).
% 62.73/8.34 fof(f4490,definition,(
% 62.73/8.34 sQ203_spl <=> (sigma=age(sK4_skl,sK8_skl))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4491,plain,(
% 62.73/8.34 sigma=age(sK4_skl,sK8_skl)|~sQ203_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4490])).
% 62.73/8.34 fof(f4493,definition,(
% 62.73/8.34 sQ204_spl <=> (greater_or_equal(age(sK4_skl,sK8_skl),sigma))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4494,plain,(
% 62.73/8.34 greater_or_equal(age(sK4_skl,sK8_skl),sigma)|~sQ204_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4493])).
% 62.73/8.34 fof(f4497,definition,(
% 62.73/8.34 sQ205_spl <=> (smaller(sigma,age(sK4_skl,sK8_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4498,plain,(
% 62.73/8.34 smaller(sigma,age(sK4_skl,sK8_skl))|~sQ205_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4497])).
% 62.73/8.34 fof(f4558,plain,(
% 62.73/8.34 greater(age(sK4_skl,sK8_skl),sigma)|age(sK4_skl,sK8_skl)=sigma|~sQ204_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4494,f29])).
% 62.73/8.34 fof(f4559,definition,(
% 62.73/8.34 sQ207_spl <=> (greater(age(sK4_skl,sK8_skl),sigma))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4560,plain,(
% 62.73/8.34 greater(age(sK4_skl,sK8_skl),sigma)|~sQ207_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4559])).
% 62.73/8.34 fof(f4562,plain,(
% 62.73/8.34 sQ207_spl|sQ203_spl|~sQ204_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f4558,f4559,f4490,f4493])).
% 62.73/8.34 fof(f4620,plain,(
% 62.73/8.34 ~greater(sigma,age(sK4_skl,sK8_skl))|~greater(sigma,age(sK4_skl,sK8_skl))|~sQ207_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4560,f887])).
% 62.73/8.34 fof(f4629,definition,(
% 62.73/8.34 sQ208_spl <=> (greater(sigma,age(sK4_skl,sK8_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4632,plain,(
% 62.73/8.34 ~sQ208_spl|~sQ207_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f4620,f4629,f4559])).
% 62.73/8.34 fof(f4635,plain,(
% 62.73/8.34 ![X0]: (~age(sK4_skl,X0)=zero|~organization(sK4_skl)|has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2|~sQ67_spl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1420,f86])).
% 62.73/8.34 fof(f4636,plain,(
% 62.73/8.34 ![X0,X1]: (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X1,X0)|~organization(sK4_skl)|is_aligned(sK4_skl,X1)|~sQ67_spl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1420,f63])).
% 62.73/8.34 fof(f4637,plain,(
% 62.73/8.34 ![X0,X1]: (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,X1)|~organization(sK4_skl)|is_aligned(sK4_skl,X1)|~sQ67_spl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1420,f62])).
% 62.73/8.34 fof(f4638,definition,(
% 62.73/8.34 ![X0]: (sQ209_spl <=> (~age(sK4_skl,X0)=zero|has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4641,plain,(
% 62.73/8.34 sQ209_spl|~sQ71_spl|~sQ67_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f4635,f4638,f1432,f1419])).
% 62.73/8.34 fof(f4642,definition,(
% 62.73/8.34 ![X0,X1]: (sQ210_spl <=> (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X1,X0)|is_aligned(sK4_skl,X1)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4645,plain,(
% 62.73/8.34 sQ210_spl|~sQ71_spl|~sQ67_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f4636,f4642,f1432,f1419])).
% 62.73/8.34 fof(f4646,definition,(
% 62.73/8.34 ![X0,X1]: (sQ211_spl <=> (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,X1)|is_aligned(sK4_skl,X1)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4649,plain,(
% 62.73/8.34 sQ211_spl|~sQ71_spl|~sQ67_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f4637,f4646,f1432,f1419])).
% 62.73/8.34 fof(f4683,plain,(
% 62.73/8.34 ![X0,X1,X2]: (~greater(X0,X1)|~smaller(X0,X2)|X2=X1|greater_or_equal(X2,X1))),
% 62.73/8.34 inference(resolution,[status(thm)],[f2594,f209])).
% 62.73/8.34 fof(f4784,definition,(
% 62.73/8.34 sQ219_spl <=> (smaller(very_low,high))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4785,plain,(
% 62.73/8.34 smaller(very_low,high)|~sQ219_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4784])).
% 62.73/8.34 fof(f4787,definition,(
% 62.73/8.34 sQ220_spl <=> (very_low=high)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4788,plain,(
% 62.73/8.34 very_low=high|~sQ220_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4787])).
% 62.73/8.34 fof(f4792,plain,(
% 62.73/8.34 greater_or_equal(high,very_low)|~sQ219_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4785,f154])).
% 62.73/8.34 fof(f4793,plain,(
% 62.73/8.34 ~greater(very_low,high)|~sQ219_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4785,f129])).
% 62.73/8.34 fof(f4794,plain,(
% 62.73/8.34 greater(high,very_low)|high=very_low|~sQ219_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4792,f29])).
% 62.73/8.34 fof(f4795,definition,(
% 62.73/8.34 sQ221_spl <=> (greater(high,very_low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4796,plain,(
% 62.73/8.34 greater(high,very_low)|~sQ221_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4795])).
% 62.73/8.34 fof(f4798,plain,(
% 62.73/8.34 sQ221_spl|sQ220_spl|~sQ219_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f4794,f4795,f4787,f4784])).
% 62.73/8.34 fof(f4811,plain,(
% 62.73/8.34 ~greater(low,very_low)|~sQ220_spl|~sQ78_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f4788,f1758])).
% 62.73/8.34 fof(f4857,plain,(
% 62.73/8.34 $false|~sQ220_spl|~sQ78_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f4811,f90])).
% 62.73/8.34 fof(f4858,plain,(
% 62.73/8.34 ~sQ220_spl|~sQ78_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f4857])).
% 62.73/8.34 fof(f4861,plain,(
% 62.73/8.34 ~greater(very_low,high)|~greater(very_low,high)|~sQ221_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4796,f887])).
% 62.73/8.34 fof(f4870,definition,(
% 62.73/8.34 sQ222_spl <=> (greater(very_low,high))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4873,plain,(
% 62.73/8.34 ~sQ222_spl|~sQ221_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f4861,f4870,f4795])).
% 62.73/8.34 fof(f4914,definition,(
% 62.73/8.34 sQ223_spl <=> (smaller(zero,age(sK4_skl,sK8_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4915,plain,(
% 62.73/8.34 smaller(zero,age(sK4_skl,sK8_skl))|~sQ223_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f4914])).
% 62.73/8.34 fof(f4921,plain,(
% 62.73/8.34 greater_or_equal(age(sK4_skl,sK8_skl),zero)|~sQ223_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4915,f154])).
% 62.73/8.34 fof(f4922,plain,(
% 62.73/8.34 ~greater(zero,age(sK4_skl,sK8_skl))|~sQ223_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4915,f129])).
% 62.73/8.34 fof(f4923,plain,(
% 62.73/8.34 greater(age(sK4_skl,sK8_skl),zero)|age(sK4_skl,sK8_skl)=zero|~sQ223_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4921,f29])).
% 62.73/8.34 fof(f4924,definition,(
% 62.73/8.34 sQ224_spl <=> (greater(age(sK4_skl,sK8_skl),zero))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f4927,plain,(
% 62.73/8.34 sQ224_spl|sQ131_spl|~sQ223_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f4923,f4924,f2230,f4914])).
% 62.73/8.34 fof(f4946,plain,(
% 62.73/8.34 greater(zero,sigma)|~sQ131_spl|~sQ207_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f2231,f4560])).
% 62.73/8.34 fof(f4977,plain,(
% 62.73/8.34 $false|~sQ131_spl|~sQ207_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f4946,f128])).
% 62.73/8.34 fof(f4978,plain,(
% 62.73/8.34 ~sQ131_spl|~sQ207_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f4977])).
% 62.73/8.34 fof(f5110,plain,(
% 62.73/8.34 ~smaller(high,very_low)|~sQ219_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4793,f34])).
% 62.73/8.34 fof(f5111,definition,(
% 62.73/8.34 sQ225_spl <=> (greater_or_equal(high,very_low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f5316,plain,(
% 62.73/8.34 ![X0]: (~greater(age(sK4_skl,X0),sigma)|has_immunity(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|~sQ66_spl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1416,f616])).
% 62.73/8.34 fof(f5317,plain,(
% 62.73/8.34 ![X0]: (~greater(age(sK4_skl,X0),sigma)|~age(sK4_skl,X0)=zero|~sQ66_spl|~sQ67_spl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1416,f1420])).
% 62.73/8.34 fof(f5331,plain,(
% 62.73/8.34 has_immunity(sK4_skl,sK6_skl)|positional_advantage(sK4_skl,sK6_skl)|hazard_of_mortality(sK4_skl,sK6_skl)=high|sQ116_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2122,f616])).
% 62.73/8.34 fof(f5333,definition,(
% 62.73/8.34 sQ226_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=high)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f5334,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK6_skl)=high|~sQ226_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f5333])).
% 62.73/8.34 fof(f5336,plain,(
% 62.73/8.34 sQ115_spl|sQ103_spl|sQ226_spl|sQ116_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f5331,f2117,f2056,f5333,f2120])).
% 62.73/8.34 fof(f5352,plain,(
% 62.73/8.34 greater_or_equal(age(sK4_skl,sK8_skl),sigma)|~sQ205_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4498,f154])).
% 62.73/8.34 fof(f5367,definition,(
% 62.73/8.34 sQ227_spl <=> (greater(zero,age(sK4_skl,sK8_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f5368,plain,(
% 62.73/8.34 greater(zero,age(sK4_skl,sK8_skl))|~sQ227_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f5367])).
% 62.73/8.34 fof(f5378,plain,(
% 62.73/8.34 ~smaller(age(sK4_skl,sK8_skl),zero)|~sQ223_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f4922,f34])).
% 62.73/8.34 fof(f5379,definition,(
% 62.73/8.34 sQ228_spl <=> (greater_or_equal(age(sK4_skl,sK8_skl),zero))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f5482,plain,(
% 62.73/8.34 ~organization(sK4_skl)|has_immunity(sK4_skl,sK6_skl)|positional_advantage(sK4_skl,sK6_skl)|hazard_of_mortality(sK4_skl,sK6_skl)=mod2|~sQ116_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2121,f86])).
% 62.73/8.34 fof(f5485,definition,(
% 62.73/8.34 sQ231_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=mod2)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f5486,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK6_skl)=mod2|~sQ231_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f5485])).
% 62.73/8.34 fof(f5488,plain,(
% 62.73/8.34 ~sQ71_spl|sQ115_spl|sQ103_spl|sQ231_spl|~sQ116_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f5482,f1432,f2117,f2056,f5485,f2120])).
% 62.73/8.34 fof(f5497,plain,(
% 62.73/8.34 mod1=mod2|~sQ118_spl|~sQ231_spl),
% 62.73/8.34 inference(forward_demodulation,[status(thm)],[f2128,f5486])).
% 62.73/8.34 fof(f5498,plain,(
% 62.73/8.34 $false|sQ29_spl|~sQ118_spl|~sQ231_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f5497,f453])).
% 62.73/8.34 fof(f5499,plain,(
% 62.73/8.34 sQ29_spl|~sQ118_spl|~sQ231_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f5498])).
% 62.73/8.34 fof(f5510,plain,(
% 62.73/8.34 greater(mod1,mod2)|~sQ231_spl|~sQ150_spl),
% 62.73/8.34 inference(forward_demodulation,[status(thm)],[f5486,f2415])).
% 62.73/8.34 fof(f5511,plain,(
% 62.73/8.34 $false|~sQ231_spl|~sQ150_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f5510,f140])).
% 62.73/8.34 fof(f5512,plain,(
% 62.73/8.34 ~sQ231_spl|~sQ150_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f5511])).
% 62.73/8.34 fof(f5521,plain,(
% 62.73/8.34 ~smaller(mod2,hazard_of_mortality(sK4_skl,sK7_skl))|~sQ231_spl|sQ1_spl),
% 62.73/8.34 inference(forward_demodulation,[status(thm)],[f5486,f113])).
% 62.73/8.34 fof(f5523,plain,(
% 62.73/8.34 ~greater(age(sK4_skl,sK8_skl),sigma)|~sQ106_spl|~sQ66_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2071,f1416])).
% 62.73/8.34 fof(f5527,plain,(
% 62.73/8.34 $false|~sQ207_spl|~sQ106_spl|~sQ66_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f5523,f4560])).
% 62.73/8.34 fof(f5528,plain,(
% 62.73/8.34 ~sQ207_spl|~sQ106_spl|~sQ66_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f5527])).
% 62.73/8.34 fof(f5642,plain,(
% 62.73/8.34 ~greater(tau,sigma)|~sQ203_spl),
% 62.73/8.34 inference(backward_demodulation,[status(thm)],[f4491,f425])).
% 62.73/8.34 fof(f5662,plain,(
% 62.73/8.34 ~sQ30_spl|~sQ203_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f5642,f478,f4490])).
% 62.73/8.34 fof(f5941,definition,(
% 62.73/8.34 sQ235_spl <=> (has_immunity(sK4_skl,sK0_skl(sK4_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f5942,plain,(
% 62.73/8.34 has_immunity(sK4_skl,sK0_skl(sK4_skl))|~sQ235_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f5941])).
% 62.73/8.34 fof(f5958,plain,(
% 62.73/8.34 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ235_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f5942,f55])).
% 62.73/8.34 fof(f5963,plain,(
% 62.73/8.34 ~sQ71_spl|sQ121_spl|~sQ235_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f5958,f1432,f2145,f5941])).
% 62.73/8.34 fof(f5967,plain,(
% 62.73/8.34 sQ204_spl|~sQ205_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f5352,f4493,f4497])).
% 62.73/8.34 fof(f6070,plain,(
% 62.73/8.34 ~positional_advantage(sK4_skl,sK7_skl)),
% 62.73/8.34 inference(resolution,[status(thm)],[f3280,f105])).
% 62.73/8.34 fof(f6071,plain,(
% 62.73/8.34 ![X0]: (~positional_advantage(sK4_skl,X0)|~smaller(age(sK4_skl,X0),tau))),
% 62.73/8.34 inference(resolution,[status(thm)],[f3280,f25])).
% 62.73/8.34 fof(f6073,definition,(
% 62.73/8.34 sQ244_spl <=> (smaller_or_equal(zero,tau))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6075,plain,(
% 62.73/8.34 ~smaller_or_equal(zero,tau)|sQ244_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6073])).
% 62.73/8.34 fof(f6093,plain,(
% 62.73/8.34 greater(tau,age(sK4_skl,sK6_skl))|tau=age(sK4_skl,sK6_skl)|~sQ97_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1971,f29])).
% 62.73/8.34 fof(f6094,definition,(
% 62.73/8.34 sQ245_spl <=> (greater(tau,age(sK4_skl,sK6_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6095,plain,(
% 62.73/8.34 greater(tau,age(sK4_skl,sK6_skl))|~sQ245_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6094])).
% 62.73/8.34 fof(f6097,plain,(
% 62.73/8.34 sQ245_spl|sQ96_spl|~sQ97_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f6093,f6094,f1967,f1970])).
% 62.73/8.34 fof(f6098,plain,(
% 62.73/8.34 ~smaller(age(sK4_skl,sK6_skl),tau)|sQ119_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2133,f25])).
% 62.73/8.34 fof(f6099,plain,(
% 62.73/8.34 ~sQ98_spl|sQ119_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f6098,f1974,f2131])).
% 62.73/8.34 fof(f6123,definition,(
% 62.73/8.34 sQ246_spl <=> (smaller(hazard_of_mortality(sK4_skl,sK7_skl),mod2))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6124,plain,(
% 62.73/8.34 smaller(hazard_of_mortality(sK4_skl,sK7_skl),mod2)|~sQ246_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6123])).
% 62.73/8.34 fof(f6125,plain,(
% 62.73/8.34 ~smaller(hazard_of_mortality(sK4_skl,sK7_skl),mod2)|sQ246_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6123])).
% 62.73/8.34 fof(f6153,definition,(
% 62.73/8.34 sQ249_spl <=> (smaller(hazard_of_mortality(sK4_skl,sK7_skl),high))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6154,plain,(
% 62.73/8.34 smaller(hazard_of_mortality(sK4_skl,sK7_skl),high)|~sQ249_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6153])).
% 62.73/8.34 fof(f6156,definition,(
% 62.73/8.34 sQ250_spl <=> (hazard_of_mortality(sK4_skl,sK7_skl)=high)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6157,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK7_skl)=high|~sQ250_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6156])).
% 62.73/8.34 fof(f6434,definition,(
% 62.73/8.34 sQ256_spl <=> (smaller(age(sK4_skl,sK8_skl),sigma))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6435,plain,(
% 62.73/8.34 smaller(age(sK4_skl,sK8_skl),sigma)|~sQ256_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6434])).
% 62.73/8.34 fof(f6439,definition,(
% 62.73/8.34 sQ257_spl <=> (greater_or_equal(sigma,age(sK4_skl,sK8_skl)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6440,plain,(
% 62.73/8.34 greater_or_equal(sigma,age(sK4_skl,sK8_skl))|~sQ257_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6439])).
% 62.73/8.34 fof(f6441,plain,(
% 62.73/8.34 ~greater_or_equal(sigma,age(sK4_skl,sK8_skl))|sQ257_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6439])).
% 62.73/8.34 fof(f6476,plain,(
% 62.73/8.34 ![X0,X1]: (is_aligned(sK4_skl,X0)|~age(sK4_skl,X1)=zero|~age(sK4_skl,X1)=zero|greater(age(sK4_skl,X0),sigma))),
% 62.73/8.34 inference(resolution,[status(thm)],[f1357,f121])).
% 62.73/8.34 fof(f6480,definition,(
% 62.73/8.34 ![X0]: (sQ258_spl <=> (is_aligned(sK4_skl,X0)|greater(age(sK4_skl,X0),sigma)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6481,plain,(
% 62.73/8.34 ![X0]: (is_aligned(sK4_skl,X0)|greater(age(sK4_skl,X0),sigma)|~sQ258_spl)),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6480])).
% 62.73/8.34 fof(f6483,plain,(
% 62.73/8.34 sQ258_spl|sQ63_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f6476,f6480,f1405])).
% 62.73/8.34 fof(f6484,definition,(
% 62.73/8.34 ![X0]: (sQ259_spl <=> (is_aligned(sK4_skl,X0)|~is_aligned(sK4_skl,X0)))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6538,plain,(
% 62.73/8.34 smaller(hazard_of_mortality(sK4_skl,sK7_skl),very_low)|hazard_of_mortality(sK4_skl,sK7_skl)=very_low|~sQ149_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f2442,f41])).
% 62.73/8.34 fof(f6542,plain,(
% 62.73/8.34 sQ124_spl|sQ125_spl|~sQ149_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f6538,f2187,f2190,f2409])).
% 62.73/8.34 fof(f6543,plain,(
% 62.73/8.34 $false|~sQ202_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f4483,f6070])).
% 62.73/8.34 fof(f6544,plain,(
% 62.73/8.34 ~sQ202_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f6543])).
% 62.73/8.34 fof(f6550,plain,(
% 62.73/8.34 $false|~sQ114_spl|sQ244_spl),
% 62.73/8.34 inference(forward_subsumption_resolution,[status(thm)],[f6075,f2169])).
% 62.73/8.34 fof(f6551,plain,(
% 62.73/8.34 ~sQ114_spl|sQ244_spl),
% 62.73/8.34 inference(contradiction_clause,[status(thm)],[f6550])).
% 62.73/8.34 fof(f6582,plain,(
% 62.73/8.34 positional_advantage(sK4_skl,sK5_skl)|hazard_of_mortality(sK4_skl,sK5_skl)=mod2|~age(sK4_skl,sK5_skl)=zero|sQ110_spl),
% 62.73/8.34 inference(resolution,[status(thm)],[f1732,f2094])).
% 62.73/8.34 fof(f6584,plain,(
% 62.73/8.34 ![X0]: (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero|~organization(sK4_skl)|hazard_of_mortality(sK4_skl,X0)=very_low)),
% 62.73/8.34 inference(resolution,[status(thm)],[f1732,f83])).
% 62.73/8.34 fof(f6585,plain,(
% 62.73/8.34 ![X0]: (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero|~organization(sK4_skl)|has_endowment(sK4_skl))),
% 62.73/8.34 inference(resolution,[status(thm)],[f1732,f55])).
% 62.73/8.34 fof(f6608,definition,(
% 62.73/8.34 sQ269_spl <=> (hazard_of_mortality(sK4_skl,sK5_skl)=mod2)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6609,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK5_skl)=mod2|~sQ269_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6608])).
% 62.73/8.34 fof(f6611,definition,(
% 62.73/8.34 sQ270_spl <=> (age(sK4_skl,sK5_skl)=zero)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6613,plain,(
% 62.73/8.34 ~age(sK4_skl,sK5_skl)=zero|sQ270_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6611])).
% 62.73/8.34 fof(f6614,plain,(
% 62.73/8.34 sQ104_spl|sQ269_spl|~sQ270_spl|sQ110_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f6582,f2060,f6608,f6611,f2092])).
% 62.73/8.34 fof(f6615,definition,(
% 62.73/8.34 sQ271_spl <=> (hazard_of_mortality(sK4_skl,sK8_skl)=mod2)),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6616,plain,(
% 62.73/8.34 hazard_of_mortality(sK4_skl,sK8_skl)=mod2|~sQ271_spl),
% 62.73/8.34 inference(component_clause,[status(thm)],[f6615])).
% 62.73/8.34 fof(f6619,definition,(
% 62.73/8.34 ![X0]: (sQ272_spl <=> (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero|hazard_of_mortality(sK4_skl,X0)=very_low))),
% 62.73/8.34 introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition])).
% 62.73/8.34 fof(f6622,plain,(
% 62.73/8.34 sQ272_spl|~sQ71_spl),
% 62.73/8.34 inference(split_clause,[status(thm)],[f6584,f6619,f1432])).
% 62.73/8.34 fof(f6623,definition,(
% 62.73/8.34 ![X0]: (sQ273_spl <=> (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f6624,plain,(
% 62.73/8.35 ![X0]: (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero|~sQ273_spl)),
% 62.73/8.35 inference(component_clause,[status(thm)],[f6623])).
% 62.73/8.35 fof(f6626,plain,(
% 62.73/8.35 sQ273_spl|~sQ71_spl|sQ121_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f6585,f6623,f1432,f2145])).
% 62.73/8.35 fof(f6631,plain,(
% 62.73/8.35 mod1=mod2|~sQ108_spl|~sQ271_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f2078,f6616])).
% 62.73/8.35 fof(f6632,plain,(
% 62.73/8.35 $false|sQ29_spl|~sQ108_spl|~sQ271_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f6631,f453])).
% 62.73/8.35 fof(f6633,plain,(
% 62.73/8.35 sQ29_spl|~sQ108_spl|~sQ271_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f6632])).
% 62.73/8.35 fof(f6634,plain,(
% 62.73/8.35 ~zero=zero|sQ270_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f99,f6613])).
% 62.73/8.35 fof(f6635,plain,(
% 62.73/8.35 $false|sQ270_spl),
% 62.73/8.35 inference(trivial_equality_resolution,[status(thm)],[f6634])).
% 62.73/8.35 fof(f6636,plain,(
% 62.73/8.35 sQ270_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f6635])).
% 62.73/8.35 fof(f6656,plain,(
% 62.73/8.35 ![X0]: (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|~organization(sK4_skl)|hazard_of_mortality(sK4_skl,X0)=very_low|~sQ81_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f1693,f83])).
% 62.73/8.35 fof(f6657,plain,(
% 62.73/8.35 ![X0]: (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ81_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f1693,f55])).
% 62.73/8.35 fof(f6668,definition,(
% 62.73/8.35 sQ276_spl <=> (hazard_of_mortality(sK4_skl,sK5_skl)=high)),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f6669,plain,(
% 62.73/8.35 hazard_of_mortality(sK4_skl,sK5_skl)=high|~sQ276_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f6668])).
% 62.73/8.35 fof(f6673,definition,(
% 62.73/8.35 ![X0]: (sQ277_spl <=> (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|hazard_of_mortality(sK4_skl,X0)=very_low))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f6676,plain,(
% 62.73/8.35 sQ277_spl|~sQ71_spl|~sQ81_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f6656,f6673,f1432,f1681])).
% 62.73/8.35 fof(f6677,definition,(
% 62.73/8.35 ![X0]: (sQ278_spl <=> (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f6678,plain,(
% 62.73/8.35 ![X0]: (positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|~sQ278_spl)),
% 62.73/8.35 inference(component_clause,[status(thm)],[f6677])).
% 62.73/8.35 fof(f6680,plain,(
% 62.73/8.35 sQ278_spl|~sQ71_spl|sQ121_spl|~sQ81_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f6657,f6677,f1432,f2145,f1681])).
% 62.73/8.35 fof(f6681,plain,(
% 62.73/8.35 high=mod2|~sQ276_spl|~sQ269_spl),
% 62.73/8.35 inference(backward_demodulation,[status(thm)],[f6669,f6609])).
% 62.73/8.35 fof(f6690,plain,(
% 62.73/8.35 sQ8_spl|~sQ276_spl|~sQ269_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f6681,f215,f6668,f6608])).
% 62.73/8.35 fof(f6782,plain,(
% 62.73/8.35 ~greater(age(sK4_skl,sK8_skl),tau)|~sQ256_spl|~sQ30_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f6435,f953])).
% 62.73/8.35 fof(f6787,plain,(
% 62.73/8.35 $false|~sQ256_spl|~sQ30_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f6782,f106])).
% 62.73/8.35 fof(f6788,plain,(
% 62.73/8.35 ~sQ256_spl|~sQ30_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f6787])).
% 62.73/8.35 fof(f6978,plain,(
% 62.73/8.35 greater(sigma,age(sK4_skl,sK8_skl))|sigma=age(sK4_skl,sK8_skl)|~sQ257_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f6440,f29])).
% 62.73/8.35 fof(f6979,plain,(
% 62.73/8.35 sQ208_spl|sQ203_spl|~sQ257_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f6978,f4629,f4490,f6439])).
% 62.73/8.35 fof(f7628,plain,(
% 62.73/8.35 ~greater(age(sK4_skl,sK6_skl),tau)|~sQ245_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f6095,f37])).
% 62.73/8.35 fof(f7808,definition,(
% 62.73/8.35 ![X1]: (sQ293_spl <=> (~age(sK4_skl,X1)=zero|greater(age(sK4_skl,X1),sigma)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f7809,plain,(
% 62.73/8.35 ![X0]: (~age(sK4_skl,X0)=zero|greater(age(sK4_skl,X0),sigma)|~sQ293_spl)),
% 62.73/8.35 inference(component_clause,[status(thm)],[f7808])).
% 62.73/8.35 fof(f7815,plain,(
% 62.73/8.35 $false|~sQ66_spl|~sQ67_spl|~sQ293_spl),
% 62.73/8.35 inference(backward_subsumption_resolution,[status(thm)],[f99,f7816])).
% 62.73/8.35 fof(f7816,plain,(
% 62.73/8.35 ![X0]: (~age(sK4_skl,X0)=zero|~sQ66_spl|~sQ67_spl|~sQ293_spl)),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f7809,f5317])).
% 62.73/8.35 fof(f7817,plain,(
% 62.73/8.35 ~sQ66_spl|~sQ67_spl|~sQ293_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f7815])).
% 62.73/8.35 fof(f7872,plain,(
% 62.73/8.35 ~smaller(age(sK4_skl,sK8_skl),tau)),
% 62.73/8.35 inference(resolution,[status(thm)],[f6071,f2033])).
% 62.73/8.35 fof(f7915,definition,(
% 62.73/8.35 sQ298_spl <=> (age(sK4_skl,sK5_skl)=tau)),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f7916,plain,(
% 62.73/8.35 age(sK4_skl,sK5_skl)=tau|~sQ298_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f7915])).
% 62.73/8.35 fof(f7920,plain,(
% 62.73/8.35 zero=tau|~sQ298_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f99,f7916])).
% 62.73/8.35 fof(f7921,plain,(
% 62.73/8.35 $false|sQ4_spl|~sQ298_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f7920,f167])).
% 62.73/8.35 fof(f7922,plain,(
% 62.73/8.35 sQ4_spl|~sQ298_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f7921])).
% 62.73/8.35 fof(f7985,plain,(
% 62.73/8.35 positional_advantage(sK4_skl,sK8_skl)|age(sK4_skl,sK8_skl)=tau),
% 62.73/8.35 inference(resolution,[status(thm)],[f7872,f2037])).
% 62.73/8.35 fof(f7990,plain,(
% 62.73/8.35 sQ129_spl|sQ47_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f7985,f2223,f776])).
% 62.73/8.35 fof(f8032,plain,(
% 62.73/8.35 ~smaller(age(sK4_skl,sK8_skl),sigma)|~sQ30_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f426,f2678])).
% 62.73/8.35 fof(f8088,plain,(
% 62.73/8.35 ![X0,X1]: (positional_advantage(sK4_skl,X0)|~greater(age(sK4_skl,X0),age(X1,sK3_skl(X1)))|robust_position(X1)|smaller_or_equal(age(X1,sK2_skl(X1)),tau))),
% 62.73/8.35 inference(resolution,[status(thm)],[f2038,f77])).
% 62.73/8.35 fof(f8089,plain,(
% 62.73/8.35 ![X0,X1]: (positional_advantage(sK4_skl,X0)|~greater(age(sK4_skl,X0),age(X1,sK3_skl(X1)))|robust_position(X1)|positional_advantage(X1,sK2_skl(X1)))),
% 62.73/8.35 inference(resolution,[status(thm)],[f2038,f79])).
% 62.73/8.35 fof(f8092,plain,(
% 62.73/8.35 ![X0,X1]: (positional_advantage(sK4_skl,X0)|~greater(age(sK4_skl,X0),X1)|smaller(X1,tau)|X1=tau)),
% 62.73/8.35 inference(resolution,[status(thm)],[f2038,f41])).
% 62.73/8.35 fof(f8289,plain,(
% 62.73/8.35 positional_advantage(sK4_skl,sK5_skl)|~smaller(tau,zero)),
% 62.73/8.35 inference(paramodulation,[status(thm)],[f99,f2039])).
% 62.73/8.35 fof(f8292,plain,(
% 62.73/8.35 sQ104_spl|~sQ164_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f8289,f2060,f2759])).
% 62.73/8.35 fof(f8294,plain,(
% 62.73/8.35 ~greater(zero,age(sK4_skl,sK7_skl))),
% 62.73/8.35 inference(resolution,[status(thm)],[f879,f100])).
% 62.73/8.35 fof(f8307,plain,(
% 62.73/8.35 zero=age(sK4_skl,sK7_skl)|greater_or_equal(age(sK4_skl,sK7_skl),zero)),
% 62.73/8.35 inference(resolution,[status(thm)],[f8294,f994])).
% 62.73/8.35 fof(f8308,plain,(
% 62.73/8.35 smaller(zero,age(sK4_skl,sK7_skl))|zero=age(sK4_skl,sK7_skl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f8294,f41])).
% 62.73/8.35 fof(f8311,definition,(
% 62.73/8.35 sQ312_spl <=> (zero=age(sK4_skl,sK7_skl))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f8312,plain,(
% 62.73/8.35 zero=age(sK4_skl,sK7_skl)|~sQ312_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f8311])).
% 62.73/8.35 fof(f8314,definition,(
% 62.73/8.35 sQ313_spl <=> (greater_or_equal(age(sK4_skl,sK7_skl),zero))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f8315,plain,(
% 62.73/8.35 greater_or_equal(age(sK4_skl,sK7_skl),zero)|~sQ313_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f8314])).
% 62.73/8.35 fof(f8317,plain,(
% 62.73/8.35 sQ312_spl|sQ313_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f8307,f8311,f8314])).
% 62.73/8.35 fof(f8318,definition,(
% 62.73/8.35 sQ314_spl <=> (smaller(zero,age(sK4_skl,sK7_skl)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f8321,plain,(
% 62.73/8.35 sQ314_spl|sQ312_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f8308,f8318,f8311])).
% 62.73/8.35 fof(f8331,plain,(
% 62.73/8.35 smaller(sigma,zero)|~sQ312_spl),
% 62.73/8.35 inference(backward_demodulation,[status(thm)],[f8312,f542])).
% 62.73/8.35 fof(f8363,plain,(
% 62.73/8.35 greater(age(sK4_skl,sK7_skl),zero)|age(sK4_skl,sK7_skl)=zero|~sQ313_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f8315,f29])).
% 62.73/8.35 fof(f8364,definition,(
% 62.73/8.35 sQ315_spl <=> (greater(age(sK4_skl,sK7_skl),zero))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f8365,plain,(
% 62.73/8.35 greater(age(sK4_skl,sK7_skl),zero)|~sQ315_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f8364])).
% 62.73/8.35 fof(f8367,plain,(
% 62.73/8.35 sQ315_spl|sQ312_spl|~sQ313_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f8363,f8364,f8311,f8314])).
% 62.73/8.35 fof(f8368,plain,(
% 62.73/8.35 $false|~sQ312_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f8331,f143])).
% 62.73/8.35 fof(f8369,plain,(
% 62.73/8.35 ~sQ312_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f8368])).
% 62.73/8.35 fof(f8521,plain,(
% 62.73/8.35 ~greater(zero,age(sK4_skl,sK7_skl))|~greater(zero,age(sK4_skl,sK7_skl))|~sQ315_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f8365,f887])).
% 62.73/8.35 fof(f8530,definition,(
% 62.73/8.35 sQ317_spl <=> (greater(zero,age(sK4_skl,sK7_skl)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f8533,plain,(
% 62.73/8.35 ~sQ317_spl|~sQ315_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f8521,f8530,f8364])).
% 62.73/8.35 fof(f8823,plain,(
% 62.73/8.35 very_low=high|greater_or_equal(high,very_low)),
% 62.73/8.35 inference(resolution,[status(thm)],[f1568,f91])).
% 62.73/8.35 fof(f8828,plain,(
% 62.73/8.35 sQ220_spl|sQ225_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f8823,f4787,f5111])).
% 62.73/8.35 fof(f8829,plain,(
% 62.73/8.35 smaller(very_low,high)|very_low=high),
% 62.73/8.35 inference(resolution,[status(thm)],[f1569,f91])).
% 62.73/8.35 fof(f8834,plain,(
% 62.73/8.35 sQ219_spl|sQ220_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f8829,f4784,f4787])).
% 62.73/8.35 fof(f8925,plain,(
% 62.73/8.35 smaller(sigma,age(sK4_skl,sK8_skl))|sigma=age(sK4_skl,sK8_skl)|~sQ30_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f8032,f211])).
% 62.73/8.35 fof(f8928,plain,(
% 62.73/8.35 sQ205_spl|sQ203_spl|~sQ30_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f8925,f4497,f4490,f478])).
% 62.73/8.35 fof(f9484,definition,(
% 62.73/8.35 sQ361_spl <=> (smaller(age(sK4_skl,sK8_skl),zero))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f9485,plain,(
% 62.73/8.35 smaller(age(sK4_skl,sK8_skl),zero)|~sQ361_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f9484])).
% 62.73/8.35 fof(f9489,definition,(
% 62.73/8.35 sQ362_spl <=> (greater_or_equal(zero,age(sK4_skl,sK8_skl)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f9490,plain,(
% 62.73/8.35 greater_or_equal(zero,age(sK4_skl,sK8_skl))|~sQ362_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f9489])).
% 62.73/8.35 fof(f9491,plain,(
% 62.73/8.35 ~greater_or_equal(zero,age(sK4_skl,sK8_skl))|sQ362_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f9489])).
% 62.73/8.35 fof(f9493,plain,(
% 62.73/8.35 $false|~sQ361_spl|~sQ223_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f5378,f9485])).
% 62.73/8.35 fof(f9494,plain,(
% 62.73/8.35 ~sQ361_spl|~sQ223_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f9493])).
% 62.73/8.35 fof(f9495,plain,(
% 62.73/8.35 greater(zero,age(sK4_skl,sK8_skl))|zero=age(sK4_skl,sK8_skl)|~sQ362_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f9490,f29])).
% 62.73/8.35 fof(f9496,plain,(
% 62.73/8.35 sQ227_spl|sQ131_spl|~sQ362_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f9495,f5367,f2230,f9489])).
% 62.73/8.35 fof(f9769,plain,(
% 62.73/8.35 ~greater(age(sK4_skl,sK8_skl),tau)|~sQ227_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f5368,f157])).
% 62.73/8.35 fof(f9800,plain,(
% 62.73/8.35 $false|~sQ227_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f9769,f106])).
% 62.73/8.35 fof(f9801,plain,(
% 62.73/8.35 ~sQ227_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f9800])).
% 62.73/8.35 fof(f10088,plain,(
% 62.73/8.35 is_aligned(sK4_skl,sK6_skl)|~sQ258_spl|~sQ5_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f6481,f955])).
% 62.73/8.35 fof(f10115,plain,(
% 62.73/8.35 is_aligned(sK4_skl,sK5_skl)|greater(zero,sigma)|~sQ258_spl),
% 62.73/8.35 inference(paramodulation,[status(thm)],[f99,f6481])).
% 62.73/8.35 fof(f10116,plain,(
% 62.73/8.35 sQ116_spl|~sQ258_spl|~sQ5_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f10088,f2120,f6480,f186])).
% 62.73/8.35 fof(f10122,plain,(
% 62.73/8.35 sQ111_spl|sQ52_spl|~sQ258_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f10115,f2095,f961,f6480])).
% 62.73/8.35 fof(f10466,plain,(
% 62.73/8.35 ![X0]: (dissimilar(sK4_skl,X0,sK5_skl)|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ111_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f2096,f63])).
% 62.73/8.35 fof(f10467,plain,(
% 62.73/8.35 ![X0]: (dissimilar(sK4_skl,sK5_skl,X0)|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ111_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f2096,f62])).
% 62.73/8.35 fof(f10469,definition,(
% 62.73/8.35 ![X0]: (sQ365_spl <=> (dissimilar(sK4_skl,X0,sK5_skl)|is_aligned(sK4_skl,X0)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ365_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f10470,plain,(
% 62.73/8.35 ![X0]: (dissimilar(sK4_skl,X0,sK5_skl)|is_aligned(sK4_skl,X0)|~sQ365_spl)),
% 62.73/8.35 inference(component_clause,[status(thm)],[f10469])).
% 62.73/8.35 fof(f10472,plain,(
% 62.73/8.35 sQ365_spl|~sQ71_spl|~sQ111_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f10466,f10469,f1432,f2095])).
% 62.73/8.35 fof(f10473,definition,(
% 62.73/8.35 ![X0]: (sQ366_spl <=> (dissimilar(sK4_skl,sK5_skl,X0)|is_aligned(sK4_skl,X0)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ366_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f10476,plain,(
% 62.73/8.35 sQ366_spl|~sQ71_spl|~sQ111_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f10467,f10473,f1432,f2095])).
% 62.73/8.35 fof(f11074,plain,(
% 62.73/8.35 ![X0]: (hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|~organization(sK4_skl)|has_immunity(sK4_skl,X0)|~is_aligned(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=low|~sQ278_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f6678,f84])).
% 62.73/8.35 fof(f11075,plain,(
% 62.73/8.35 ![X0]: (hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|~organization(sK4_skl)|has_immunity(sK4_skl,X0)|is_aligned(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod1|~sQ278_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f6678,f85])).
% 62.73/8.35 fof(f11083,definition,(
% 62.73/8.35 ![X0]: (sQ367_spl <=> (hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|has_immunity(sK4_skl,X0)|~is_aligned(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=low))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ367_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f11086,plain,(
% 62.73/8.35 sQ367_spl|~sQ71_spl|~sQ278_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f11074,f11083,f1432,f6677])).
% 62.73/8.35 fof(f11087,definition,(
% 62.73/8.35 ![X0]: (sQ368_spl <=> (hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=mod2|has_immunity(sK4_skl,X0)|is_aligned(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod1))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ368_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f11090,plain,(
% 62.73/8.35 sQ368_spl|~sQ71_spl|~sQ278_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f11075,f11087,f1432,f6677])).
% 62.73/8.35 fof(f11347,plain,(
% 62.73/8.35 ![X0]: (is_aligned(sK4_skl,X0)|~age(sK4_skl,X0)=zero|greater(age(sK4_skl,sK5_skl),sigma)|~sQ365_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f10470,f121])).
% 62.73/8.35 fof(f11348,plain,(
% 62.73/8.35 ![X0]: (is_aligned(sK4_skl,X0)|~is_aligned(sK4_skl,X0)|~is_aligned(sK4_skl,sK5_skl)|~sQ365_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f10470,f61])).
% 62.73/8.35 fof(f11351,definition,(
% 62.73/8.35 sQ372_spl <=> (greater(age(sK4_skl,sK5_skl),sigma))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f11352,plain,(
% 62.73/8.35 greater(age(sK4_skl,sK5_skl),sigma)|~sQ372_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f11351])).
% 62.73/8.35 fof(f11354,plain,(
% 62.73/8.35 sQ67_spl|sQ372_spl|~sQ365_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f11347,f1419,f11351,f10469])).
% 62.73/8.35 fof(f11355,plain,(
% 62.73/8.35 sQ259_spl|~sQ111_spl|~sQ365_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f11348,f6484,f2095,f10469])).
% 62.73/8.35 fof(f11360,plain,(
% 62.73/8.35 smaller(zero,age(sK4_skl,sK8_skl))|zero=age(sK4_skl,sK8_skl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f421,f106])).
% 62.73/8.35 fof(f11373,plain,(
% 62.73/8.35 sQ223_spl|sQ131_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f11360,f4914,f2230])).
% 62.73/8.35 fof(f11587,plain,(
% 62.73/8.35 ![X0]: (hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero|~organization(sK4_skl)|has_immunity(sK4_skl,X0)|~is_aligned(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=low|~sQ273_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f6624,f84])).
% 62.73/8.35 fof(f11588,plain,(
% 62.73/8.35 ![X0]: (hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero|~organization(sK4_skl)|has_immunity(sK4_skl,X0)|is_aligned(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod1|~sQ273_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f6624,f85])).
% 62.73/8.35 fof(f11596,definition,(
% 62.73/8.35 ![X0]: (sQ381_spl <=> (hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero|has_immunity(sK4_skl,X0)|~is_aligned(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=low))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f11599,plain,(
% 62.73/8.35 sQ381_spl|~sQ71_spl|~sQ273_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f11587,f11596,f1432,f6623])).
% 62.73/8.35 fof(f11600,definition,(
% 62.73/8.35 ![X0]: (sQ382_spl <=> (hazard_of_mortality(sK4_skl,X0)=mod2|~age(sK4_skl,X0)=zero|has_immunity(sK4_skl,X0)|is_aligned(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=mod1))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ382_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f11603,plain,(
% 62.73/8.35 sQ382_spl|~sQ71_spl|~sQ273_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f11588,f11600,f1432,f6623])).
% 62.73/8.35 fof(f11606,plain,(
% 62.73/8.35 greater(zero,sigma)|~sQ372_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f99,f11352])).
% 62.73/8.35 fof(f11607,plain,(
% 62.73/8.35 $false|~sQ372_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f11606,f128])).
% 62.73/8.35 fof(f11608,plain,(
% 62.73/8.35 ~sQ372_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f11607])).
% 62.73/8.35 fof(f11638,plain,(
% 62.73/8.35 ~smaller(mod2,high)|~sQ250_spl|~sQ231_spl|sQ1_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f6157,f5521])).
% 62.73/8.35 fof(f11639,plain,(
% 62.73/8.35 $false|~sQ250_spl|~sQ231_spl|sQ1_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f11638,f137])).
% 62.73/8.35 fof(f11640,plain,(
% 62.73/8.35 ~sQ250_spl|~sQ231_spl|sQ1_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f11639])).
% 62.73/8.35 fof(f11641,plain,(
% 62.73/8.35 smaller(high,mod2)|~sQ250_spl|~sQ246_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f6157,f6124])).
% 62.73/8.35 fof(f11642,plain,(
% 62.73/8.35 $false|~sQ250_spl|~sQ246_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f11641,f200])).
% 62.73/8.35 fof(f11643,plain,(
% 62.73/8.35 ~sQ250_spl|~sQ246_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f11642])).
% 62.73/8.35 fof(f11648,plain,(
% 62.73/8.35 smaller(high,very_low)|~sQ250_spl|~sQ124_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f6157,f2188])).
% 62.73/8.35 fof(f11649,plain,(
% 62.73/8.35 $false|~sQ219_spl|~sQ250_spl|~sQ124_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f11648,f5110])).
% 62.73/8.35 fof(f11650,plain,(
% 62.73/8.35 ~sQ219_spl|~sQ250_spl|~sQ124_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f11649])).
% 62.73/8.35 fof(f11774,plain,(
% 62.73/8.35 smaller(age(sK4_skl,sK6_skl),tau)|age(sK4_skl,sK6_skl)=tau|~sQ245_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f7628,f41])).
% 62.73/8.35 fof(f11778,plain,(
% 62.73/8.35 sQ98_spl|sQ96_spl|~sQ245_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f11774,f1974,f1967,f6094])).
% 62.73/8.35 fof(f12377,plain,(
% 62.73/8.35 ![X0]: (positional_advantage(sK4_skl,sK5_skl)|~greater(zero,age(X0,sK3_skl(X0)))|robust_position(X0)|smaller_or_equal(age(X0,sK2_skl(X0)),tau))),
% 62.73/8.35 inference(paramodulation,[status(thm)],[f99,f8088])).
% 62.73/8.35 fof(f12382,definition,(
% 62.73/8.35 ![X0]: (sQ390_spl <=> (~greater(zero,age(X0,sK3_skl(X0)))|robust_position(X0)|smaller_or_equal(age(X0,sK2_skl(X0)),tau)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f12385,plain,(
% 62.73/8.35 sQ104_spl|sQ390_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f12377,f2060,f12382])).
% 62.73/8.35 fof(f12391,plain,(
% 62.73/8.35 ![X0]: (positional_advantage(sK4_skl,sK5_skl)|~greater(zero,age(X0,sK3_skl(X0)))|robust_position(X0)|positional_advantage(X0,sK2_skl(X0)))),
% 62.73/8.35 inference(paramodulation,[status(thm)],[f99,f8089])).
% 62.73/8.35 fof(f12396,definition,(
% 62.73/8.35 ![X0]: (sQ392_spl <=> (~greater(zero,age(X0,sK3_skl(X0)))|robust_position(X0)|positional_advantage(X0,sK2_skl(X0))))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f12399,plain,(
% 62.73/8.35 sQ104_spl|sQ392_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f12391,f2060,f12396])).
% 62.73/8.35 fof(f12540,plain,(
% 62.73/8.35 ![X0]: (positional_advantage(sK4_skl,sK5_skl)|~greater(zero,X0)|smaller(X0,tau)|X0=tau)),
% 62.73/8.35 inference(paramodulation,[status(thm)],[f99,f8092])).
% 62.73/8.35 fof(f12555,definition,(
% 62.73/8.35 ![X0]: (sQ399_spl <=> (~greater(zero,X0)|smaller(X0,tau)|X0=tau))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f12558,plain,(
% 62.73/8.35 sQ104_spl|sQ399_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f12540,f2060,f12555])).
% 62.73/8.35 fof(f13018,plain,(
% 62.73/8.35 zero=age(sK4_skl,sK8_skl)|greater_or_equal(age(sK4_skl,sK8_skl),zero)),
% 62.73/8.35 inference(resolution,[status(thm)],[f2679,f426])).
% 62.73/8.35 fof(f13030,plain,(
% 62.73/8.35 sQ131_spl|sQ228_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f13018,f2230,f5379])).
% 62.73/8.35 fof(f13556,definition,(
% 62.73/8.35 sQ414_spl <=> (greater(sigma,sigma))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f13557,plain,(
% 62.73/8.35 greater(sigma,sigma)|~sQ414_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f13556])).
% 62.73/8.35 fof(f14611,plain,(
% 62.73/8.35 has_immunity(sK4_skl,sK7_skl)|positional_advantage(sK4_skl,sK7_skl)|hazard_of_mortality(sK4_skl,sK7_skl)=high|~sQ66_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f5316,f104])).
% 62.73/8.35 fof(f14621,definition,(
% 62.73/8.35 sQ426_spl <=> (has_immunity(sK4_skl,sK7_skl))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f14622,plain,(
% 62.73/8.35 has_immunity(sK4_skl,sK7_skl)|~sQ426_spl),
% 62.73/8.35 inference(component_clause,[status(thm)],[f14621])).
% 62.73/8.35 fof(f14624,plain,(
% 62.73/8.35 sQ426_spl|sQ202_spl|sQ250_spl|~sQ66_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f14611,f14621,f4482,f6156,f1415])).
% 62.73/8.35 fof(f14630,plain,(
% 62.73/8.35 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ426_spl),
% 62.73/8.35 inference(resolution,[status(thm)],[f14622,f55])).
% 62.73/8.35 fof(f14632,plain,(
% 62.73/8.35 ~sQ71_spl|sQ121_spl|~sQ426_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f14630,f1432,f2145,f14621])).
% 62.73/8.35 fof(f15017,plain,(
% 62.73/8.35 ~smaller(very_low,mod2)|~sQ125_spl|sQ246_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f2191,f6125])).
% 62.73/8.35 fof(f15018,plain,(
% 62.73/8.35 $false|~sQ55_spl|~sQ125_spl|sQ246_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f15017,f1007])).
% 62.73/8.35 fof(f15019,plain,(
% 62.73/8.35 ~sQ55_spl|~sQ125_spl|sQ246_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f15018])).
% 62.73/8.35 fof(f15185,plain,(
% 62.73/8.35 smaller(high,hazard_of_mortality(sK4_skl,sK7_skl))|~sQ226_spl|~sQ1_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f5334,f112])).
% 62.73/8.35 fof(f15186,plain,(
% 62.73/8.35 smaller(high,high)|~sQ250_spl|~sQ226_spl|~sQ1_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f6157,f15185])).
% 62.73/8.35 fof(f15187,plain,(
% 62.73/8.35 $false|~sQ250_spl|~sQ226_spl|~sQ1_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f15186,f908])).
% 62.73/8.35 fof(f15188,plain,(
% 62.73/8.35 ~sQ250_spl|~sQ226_spl|~sQ1_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f15187])).
% 62.73/8.35 fof(f15192,plain,(
% 62.73/8.35 ~greater_or_equal(very_low,high)|~sQ250_spl|sQ126_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f6157,f2197])).
% 62.73/8.35 fof(f15193,plain,(
% 62.73/8.35 ~hazard_of_mortality(sK4_skl,sK6_skl)=mod2|~sQ269_spl|sQ2_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f6609,f116])).
% 62.73/8.35 fof(f15197,plain,(
% 62.73/8.35 $false|~sQ269_spl|sQ2_spl|~sQ231_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f5486,f15193])).
% 62.73/8.35 fof(f15198,plain,(
% 62.73/8.35 ~sQ269_spl|sQ2_spl|~sQ231_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f15197])).
% 62.73/8.35 fof(f15807,plain,(
% 62.73/8.35 smaller(high,high)|~sQ250_spl|~sQ249_spl),
% 62.73/8.35 inference(forward_demodulation,[status(thm)],[f6157,f6154])).
% 62.73/8.35 fof(f15808,plain,(
% 62.73/8.35 $false|~sQ250_spl|~sQ249_spl),
% 62.73/8.35 inference(forward_subsumption_resolution,[status(thm)],[f15807,f908])).
% 62.73/8.35 fof(f15809,plain,(
% 62.73/8.35 ~sQ250_spl|~sQ249_spl),
% 62.73/8.35 inference(contradiction_clause,[status(thm)],[f15808])).
% 62.73/8.35 fof(f19108,plain,(
% 62.73/8.35 ![X0]: (~greater(sigma,X0)|~smaller(age(sK4_skl,sK8_skl),X0)|age(sK4_skl,sK8_skl)=sigma|sQ257_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f2591,f6441])).
% 62.73/8.35 fof(f19111,plain,(
% 62.73/8.35 ![X0]: (~greater(very_low,X0)|~smaller(high,X0)|high=very_low|~sQ250_spl|sQ126_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f2591,f15192])).
% 62.73/8.35 fof(f19112,plain,(
% 62.73/8.35 ![X0]: (~greater(zero,X0)|~smaller(age(sK4_skl,sK8_skl),X0)|age(sK4_skl,sK8_skl)=zero|sQ362_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f2591,f9491])).
% 62.73/8.35 fof(f19140,definition,(
% 62.73/8.35 ![X0]: (sQ450_spl <=> (~greater(sigma,X0)|~smaller(age(sK4_skl,sK8_skl),X0)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ450_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f19143,plain,(
% 62.73/8.35 sQ450_spl|sQ203_spl|sQ257_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f19108,f19140,f4490,f6439])).
% 62.73/8.35 fof(f19152,definition,(
% 62.73/8.35 ![X0]: (sQ453_spl <=> (~greater(very_low,X0)|~smaller(high,X0)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ453_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f19155,plain,(
% 62.73/8.35 sQ453_spl|sQ220_spl|~sQ250_spl|sQ126_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f19111,f19152,f4787,f6156,f2195])).
% 62.73/8.35 fof(f19156,definition,(
% 62.73/8.35 ![X0]: (sQ454_spl <=> (~greater(zero,X0)|~smaller(age(sK4_skl,sK8_skl),X0)))),
% 62.73/8.35 introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition])).
% 62.73/8.35 fof(f19159,plain,(
% 62.73/8.35 sQ454_spl|sQ131_spl|sQ362_spl),
% 62.73/8.35 inference(split_clause,[status(thm)],[f19112,f19156,f2230,f9489])).
% 62.73/8.35 fof(f19333,plain,(
% 62.73/8.35 ![X0]: (~greater(X0,age(sK4_skl,sK8_skl))|~smaller(X0,sigma)|sigma=age(sK4_skl,sK8_skl)|sQ257_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f4683,f6441])).
% 62.73/8.35 fof(f19336,plain,(
% 62.73/8.35 ![X0]: (~greater(X0,high)|~smaller(X0,very_low)|very_low=high|~sQ250_spl|sQ126_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f4683,f15192])).
% 62.73/8.35 fof(f19337,plain,(
% 62.73/8.35 ![X0]: (~greater(X0,age(sK4_skl,sK8_skl))|~smaller(X0,zero)|zero=age(sK4_skl,sK8_skl)|sQ362_spl)),
% 62.73/8.35 inference(resolution,[status(thm)],[f4683,f9491])).
% 62.73/8.35 fof(f19368,definition,(
% 62.73/8.36 ![X0]: (sQ464_spl <=> (~greater(X0,age(sK4_skl,sK8_skl))|~smaller(X0,sigma)))),
% 62.73/8.36 introduced(definition,[new_symbols(definition,[sQ464_spl])],[split_symbol_definition])).
% 62.73/8.36 fof(f19371,plain,(
% 62.73/8.36 sQ464_spl|sQ203_spl|sQ257_spl),
% 62.73/8.36 inference(split_clause,[status(thm)],[f19333,f19368,f4490,f6439])).
% 62.73/8.36 fof(f19380,definition,(
% 62.73/8.36 ![X0]: (sQ467_spl <=> (~greater(X0,high)|~smaller(X0,very_low)))),
% 62.73/8.36 introduced(definition,[new_symbols(definition,[sQ467_spl])],[split_symbol_definition])).
% 62.73/8.36 fof(f19383,plain,(
% 62.73/8.36 sQ467_spl|sQ220_spl|~sQ250_spl|sQ126_spl),
% 62.73/8.36 inference(split_clause,[status(thm)],[f19336,f19380,f4787,f6156,f2195])).
% 62.73/8.36 fof(f19384,definition,(
% 62.73/8.36 ![X0]: (sQ468_spl <=> (~greater(X0,age(sK4_skl,sK8_skl))|~smaller(X0,zero)))),
% 62.73/8.36 introduced(definition,[new_symbols(definition,[sQ468_spl])],[split_symbol_definition])).
% 62.73/8.36 fof(f19387,plain,(
% 62.73/8.36 sQ468_spl|sQ131_spl|sQ362_spl),
% 62.73/8.36 inference(split_clause,[status(thm)],[f19337,f19384,f2230,f9489])).
% 62.73/8.36 fof(f19553,plain,(
% 62.73/8.36 is_aligned(sK4_skl,sK6_skl)|greater(sigma,sigma)|~sQ258_spl|~sQ6_spl),
% 62.73/8.36 inference(paramodulation,[status(thm)],[f190,f6481])).
% 62.73/8.36 fof(f19558,plain,(
% 62.73/8.36 sQ116_spl|sQ414_spl|~sQ258_spl|~sQ6_spl),
% 62.73/8.36 inference(split_clause,[status(thm)],[f19553,f2120,f13556,f6480,f189])).
% 62.73/8.36 fof(f19560,plain,(
% 62.73/8.36 $false|~sQ414_spl),
% 62.73/8.36 inference(forward_subsumption_resolution,[status(thm)],[f13557,f905])).
% 62.73/8.36 fof(f19561,plain,(
% 62.73/8.36 ~sQ414_spl),
% 62.73/8.36 inference(contradiction_clause,[status(thm)],[f19560])).
% 62.73/8.36 fof(f19562,plain,(
% 62.73/8.36 $false),
% 62.73/8.36 inference(sat_refutation,[status(thm)],[f117,f168,f184,f192,f218,f225,f232,f239,f246,f253,f307,f315,f323,f343,f352,f367,f385,f393,f398,f406,f418,f454,f476,f565,f606,f647,f651,f655,f659,f663,f667,f671,f679,f723,f725,f779,f787,f853,f938,f949,f982,f987,f1012,f1048,f1171,f1175,f1220,f1230,f1262,f1266,f1317,f1352,f1411,f1418,f1435,f1441,f1445,f1446,f1447,f1456,f1495,f1500,f1549,f1587,f1592,f1644,f1684,f1688,f1692,f1756,f1973,f2007,f2080,f2084,f2087,f2088,f2109,f2134,f2148,f2151,f2154,f2163,f2168,f2176,f2193,f2215,f2219,f2235,f2322,f2337,f2412,f2417,f2543,f2544,f2545,f2550,f2551,f2555,f2556,f2557,f2558,f2559,f2560,f2564,f2568,f2571,f3695,f4562,f4632,f4641,f4645,f4649,f4798,f4858,f4873,f4927,f4978,f5336,f5488,f5499,f5512,f5528,f5662,f5963,f5967,f6097,f6099,f6483,f6542,f6544,f6551,f6614,f6622,f6626,f6633,f6636,f6676,f6680,f6690,f6788,f6979,f7817,f7922,f7990,f8292,f8317,f8321,f8367,f8369,f8533,f8828,f8834,f8928,f9494,f9496,f9801,f10116,f10122,f10472,f10476,f11086,f11090,f11354,f11355,f11373,f11599,f11603,f11608,f11640,f11643,f11650,f11778,f12385,f12399,f12558,f13030,f14624,f14632,f15019,f15188,f15198,f15809,f19143,f19155,f19159,f19371,f19383,f19387,f19558,f19561])).
% 62.73/8.36 % SZS output end CNFRefutation for theBenchmark.p
% 62.73/8.37 % Elapsed time: 8.009593 seconds
% 62.73/8.37 % CPU time: 63.167713 seconds
% 62.73/8.37 % Total memory used: 335.984 MB
% 62.73/8.37 % Net memory used: 289.490 MB
%------------------------------------------------------------------------------