%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT064+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 15.01s 2.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT064+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.46 % Computer : n020.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Mon Sep 21 01:25:32 UTC 2026
% 0.18/0.47 % CPUTime :
% 0.18/0.50 % Drodi V4.1.1
% 15.01/2.50 % Refutation found
% 15.01/2.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.01/2.50 % SZS output start CNFRefutation for theBenchmark
% 15.01/2.50 fof(f1,axiom,(
% 15.01/2.50 (! [X,Y] :( smaller_or_equal(X,Y)<=> ( smaller(X,Y)| X = Y ) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f2,axiom,(
% 15.01/2.50 (! [X,Y] :( greater_or_equal(X,Y)<=> ( greater(X,Y)| X = Y ) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f3,axiom,(
% 15.01/2.50 (! [X,Y] :( smaller(X,Y)<=> greater(Y,X) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f4,axiom,(
% 15.01/2.50 (! [X,Y] :~ ( greater(X,Y)& greater(Y,X) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f5,axiom,(
% 15.01/2.50 (! [X,Y,Z] :( ( greater(X,Y)& greater(Y,Z) )=> greater(X,Z) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f6,axiom,(
% 15.01/2.50 (! [X,Y] :( smaller(X,Y)| X = Y| greater(X,Y) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f7,axiom,(
% 15.01/2.50 (! [X] :( has_endowment(X)<=> (! [T] :( organization(X)& ( smaller_or_equal(age(X,T),eta)=> has_immunity(X,T) )& ( greater(age(X,T),eta)=> ~ has_immunity(X,T) ) ) )) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f8,axiom,(
% 15.01/2.50 (! [X,T] :( ( organization(X)& ~ has_endowment(X) )=> ~ has_immunity(X,T) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f9,axiom,(
% 15.01/2.50 (! [X,T0,T] :( dissimilar(X,T0,T)<=> ( organization(X)& ~ ( is_aligned(X,T0)<=> is_aligned(X,T) ) ) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f10,axiom,(
% 15.01/2.50 (! [X,T] :( ( organization(X)& age(X,T) = zero )=> is_aligned(X,T) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f11,axiom,(
% 15.01/2.50 (! [X,T0,T] :( ( organization(X)& age(X,T0) = zero )=> ( greater(age(X,T),sigma)<=> dissimilar(X,T0,T) ) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f12,axiom,(
% 15.01/2.50 (! [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) ) ) )) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f13,axiom,(
% 15.01/2.50 (! [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 ) ) ) ) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f14,axiom,(
% 15.01/2.50 greater(high,mod1) ),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f15,axiom,(
% 15.01/2.50 greater(mod1,low) ),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f16,axiom,(
% 15.01/2.50 greater(low,very_low) ),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f17,axiom,(
% 15.01/2.50 greater(high,mod2) ),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f18,axiom,(
% 15.01/2.50 greater(mod2,low) ),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f19,axiom,(
% 15.01/2.50 greater(mod2,mod1) ),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f20,conjecture,(
% 15.01/2.50 (! [X,T0,T1,T2,T3] :( ( organization(X)& robust_position(X)& ~ has_endowment(X)& age(X,T0) = zero& greater(sigma,zero)& greater(tau,zero)& greater(sigma,tau)& smaller_or_equal(age(X,T1),tau)& greater(age(X,T2),tau)& smaller_or_equal(age(X,T2),sigma)& greater(age(X,T3),sigma) )=> ( smaller(hazard_of_mortality(X,T2),hazard_of_mortality(X,T3))& smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) )),
% 15.01/2.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.01/2.50 fof(f21,negated_conjecture,(
% 15.01/2.50 ~((! [X,T0,T1,T2,T3] :( ( organization(X)& robust_position(X)& ~ has_endowment(X)& age(X,T0) = zero& greater(sigma,zero)& greater(tau,zero)& greater(sigma,tau)& smaller_or_equal(age(X,T1),tau)& greater(age(X,T2),tau)& smaller_or_equal(age(X,T2),sigma)& greater(age(X,T3),sigma) )=> ( smaller(hazard_of_mortality(X,T2),hazard_of_mortality(X,T3))& smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ))),
% 15.01/2.50 inference(negated_conjecture,[status(cth)],[f20])).
% 15.01/2.50 fof(f22,plain,(
% 15.01/2.50 ![X,Y]: ((~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y))&(smaller_or_equal(X,Y)|(~smaller(X,Y)&~X=Y)))),
% 15.01/2.50 inference(NNF_transformation,[status(thm)],[f1])).
% 15.01/2.50 fof(f23,plain,(
% 15.01/2.50 (![X,Y]: (~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y)))&(![X,Y]: (smaller_or_equal(X,Y)|(~smaller(X,Y)&~X=Y)))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f22])).
% 15.01/2.50 fof(f24,plain,(
% 15.01/2.50 ![X0,X1]: (~smaller_or_equal(X0,X1)|smaller(X0,X1)|X0=X1)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f23])).
% 15.01/2.50 fof(f25,plain,(
% 15.01/2.50 ![X0,X1]: (smaller_or_equal(X0,X1)|~smaller(X0,X1))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f23])).
% 15.01/2.50 fof(f26,plain,(
% 15.01/2.50 ![X0,X1]: (smaller_or_equal(X0,X1)|~X0=X1)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f23])).
% 15.01/2.50 fof(f27,plain,(
% 15.01/2.50 ![X,Y]: ((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&(greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 15.01/2.50 inference(NNF_transformation,[status(thm)],[f2])).
% 15.01/2.50 fof(f28,plain,(
% 15.01/2.50 (![X,Y]: (~greater_or_equal(X,Y)|(greater(X,Y)|X=Y)))&(![X,Y]: (greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f27])).
% 15.01/2.50 fof(f29,plain,(
% 15.01/2.50 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f28])).
% 15.01/2.50 fof(f30,plain,(
% 15.01/2.50 ![X0,X1]: (greater_or_equal(X0,X1)|~greater(X0,X1))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f28])).
% 15.01/2.50 fof(f32,plain,(
% 15.01/2.50 ![X,Y]: ((~smaller(X,Y)|greater(Y,X))&(smaller(X,Y)|~greater(Y,X)))),
% 15.01/2.50 inference(NNF_transformation,[status(thm)],[f3])).
% 15.01/2.50 fof(f33,plain,(
% 15.01/2.50 (![X,Y]: (~smaller(X,Y)|greater(Y,X)))&(![X,Y]: (smaller(X,Y)|~greater(Y,X)))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f32])).
% 15.01/2.50 fof(f34,plain,(
% 15.01/2.50 ![X0,X1]: (~smaller(X0,X1)|greater(X1,X0))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f33])).
% 15.01/2.50 fof(f35,plain,(
% 15.01/2.50 ![X0,X1]: (smaller(X0,X1)|~greater(X1,X0))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f33])).
% 15.01/2.50 fof(f36,plain,(
% 15.01/2.50 ![X,Y]: (~greater(X,Y)|~greater(Y,X))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 15.01/2.50 fof(f37,plain,(
% 15.01/2.50 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f36])).
% 15.01/2.50 fof(f38,plain,(
% 15.01/2.50 ![X,Y,Z]: ((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 15.01/2.50 fof(f39,plain,(
% 15.01/2.50 ![X,Z]: ((![Y]: (~greater(X,Y)|~greater(Y,Z)))|greater(X,Z))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f38])).
% 15.01/2.50 fof(f40,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f39])).
% 15.01/2.50 fof(f41,plain,(
% 15.01/2.50 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater(X0,X1))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f6])).
% 15.01/2.50 fof(f42,plain,(
% 15.01/2.50 ![X]: (has_endowment(X)<=>(![T]: ((organization(X)&(~smaller_or_equal(age(X,T),eta)|has_immunity(X,T)))&(~greater(age(X,T),eta)|~has_immunity(X,T)))))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 15.01/2.50 fof(f43,plain,(
% 15.01/2.50 ![X]: ((~has_endowment(X)|(![T]: ((organization(X)&(~smaller_or_equal(age(X,T),eta)|has_immunity(X,T)))&(~greater(age(X,T),eta)|~has_immunity(X,T)))))&(has_endowment(X)|(?[T]: ((~organization(X)|(smaller_or_equal(age(X,T),eta)&~has_immunity(X,T)))|(greater(age(X,T),eta)&has_immunity(X,T))))))),
% 15.01/2.50 inference(NNF_transformation,[status(thm)],[f42])).
% 15.01/2.50 fof(f44,plain,(
% 15.01/2.50 (![X]: (~has_endowment(X)|((organization(X)&(![T]: (~smaller_or_equal(age(X,T),eta)|has_immunity(X,T))))&(![T]: (~greater(age(X,T),eta)|~has_immunity(X,T))))))&(![X]: (has_endowment(X)|((~organization(X)|(?[T]: (smaller_or_equal(age(X,T),eta)&~has_immunity(X,T))))|(?[T]: (greater(age(X,T),eta)&has_immunity(X,T))))))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f43])).
% 15.01/2.50 fof(f45,plain,(
% 15.01/2.50 (![X]: (~has_endowment(X)|((organization(X)&(![T]: (~smaller_or_equal(age(X,T),eta)|has_immunity(X,T))))&(![T]: (~greater(age(X,T),eta)|~has_immunity(X,T))))))&(![X]: (has_endowment(X)|((~organization(X)|(smaller_or_equal(age(X,sK0_skl(X)),eta)&~has_immunity(X,sK0_skl(X))))|(greater(age(X,sK1_skl(X)),eta)&has_immunity(X,sK1_skl(X))))))),
% 15.01/2.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(T,sK0_skl(X)),skolemize(T,sK1_skl(X))],[f44])).
% 15.01/2.50 fof(f48,plain,(
% 15.01/2.50 ![X0,X1]: (~has_endowment(X0)|~greater(age(X0,X1),eta)|~has_immunity(X0,X1))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f45])).
% 15.01/2.50 fof(f50,plain,(
% 15.01/2.50 ![X0]: (has_endowment(X0)|~organization(X0)|smaller_or_equal(age(X0,sK0_skl(X0)),eta)|has_immunity(X0,sK1_skl(X0)))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f45])).
% 15.01/2.50 fof(f53,plain,(
% 15.01/2.50 ![X,T]: ((~organization(X)|has_endowment(X))|~has_immunity(X,T))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 15.01/2.50 fof(f54,plain,(
% 15.01/2.50 ![X]: ((~organization(X)|has_endowment(X))|(![T]: ~has_immunity(X,T)))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f53])).
% 15.01/2.50 fof(f55,plain,(
% 15.01/2.50 ![X0,X1]: (~organization(X0)|has_endowment(X0)|~has_immunity(X0,X1))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f54])).
% 15.01/2.50 fof(f56,plain,(
% 15.01/2.50 ![X,T0,T]: (dissimilar(X,T0,T)<=>(organization(X)&(is_aligned(X,T0)<~>is_aligned(X,T))))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 15.01/2.50 fof(f57,plain,(
% 15.01/2.50 ![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))))))),
% 15.01/2.50 inference(NNF_transformation,[status(thm)],[f56])).
% 15.01/2.50 fof(f58,plain,(
% 15.01/2.50 (![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))))))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f57])).
% 15.01/2.50 fof(f59,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|organization(X0))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f58])).
% 15.01/2.50 fof(f60,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|is_aligned(X0,X1)|is_aligned(X0,X2))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f58])).
% 15.01/2.50 fof(f61,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f58])).
% 15.01/2.50 fof(f62,plain,(
% 15.01/2.50 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f58])).
% 15.01/2.50 fof(f63,plain,(
% 15.01/2.50 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f58])).
% 15.01/2.50 fof(f64,plain,(
% 15.01/2.50 ![X,T]: ((~organization(X)|~age(X,T)=zero)|is_aligned(X,T))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 15.01/2.50 fof(f65,plain,(
% 15.01/2.50 ![X0,X1]: (~organization(X0)|~age(X0,X1)=zero|is_aligned(X0,X1))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f64])).
% 15.01/2.50 fof(f66,plain,(
% 15.01/2.50 ![X,T0,T]: ((~organization(X)|~age(X,T0)=zero)|(greater(age(X,T),sigma)<=>dissimilar(X,T0,T)))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 15.01/2.50 fof(f67,plain,(
% 15.01/2.50 ![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))))),
% 15.01/2.50 inference(NNF_transformation,[status(thm)],[f66])).
% 15.01/2.50 fof(f68,plain,(
% 15.01/2.50 ![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)))))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f67])).
% 15.01/2.50 fof(f69,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~greater(age(X0,X2),sigma)|dissimilar(X0,X1,X2))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f68])).
% 15.01/2.50 fof(f70,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|greater(age(X0,X2),sigma)|~dissimilar(X0,X1,X2))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f68])).
% 15.01/2.50 fof(f71,plain,(
% 15.01/2.50 ![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)))))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 15.01/2.50 fof(f72,plain,(
% 15.01/2.50 ![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))))))),
% 15.01/2.50 inference(NNF_transformation,[status(thm)],[f71])).
% 15.01/2.50 fof(f73,plain,(
% 15.01/2.50 (![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))))))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f72])).
% 15.01/2.50 fof(f74,plain,(
% 15.01/2.50 (![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))))))),
% 15.01/2.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(T,sK2_skl(X)),skolemize(T,sK3_skl(X))],[f73])).
% 15.01/2.50 fof(f75,plain,(
% 15.01/2.50 ![X0,X1]: (~robust_position(X0)|~smaller_or_equal(age(X0,X1),tau)|~positional_advantage(X0,X1))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f74])).
% 15.01/2.50 fof(f76,plain,(
% 15.01/2.50 ![X0,X1]: (~robust_position(X0)|~greater(age(X0,X1),tau)|positional_advantage(X0,X1))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f74])).
% 15.01/2.50 fof(f79,plain,(
% 15.01/2.50 ![X0]: (robust_position(X0)|positional_advantage(X0,sK2_skl(X0))|greater(age(X0,sK3_skl(X0)),tau))),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f74])).
% 15.01/2.50 fof(f81,plain,(
% 15.01/2.50 ![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)))))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 15.01/2.50 fof(f82,plain,(
% 15.01/2.50 ![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))))))),
% 15.01/2.50 inference(miniscoping,[status(thm)],[f81])).
% 15.01/2.50 fof(f83,plain,(
% 15.01/2.50 ![X0,X1]: (~organization(X0)|~has_immunity(X0,X1)|hazard_of_mortality(X0,X1)=very_low)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f82])).
% 15.01/2.50 fof(f84,plain,(
% 15.01/2.50 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=low)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f82])).
% 15.01/2.50 fof(f85,plain,(
% 15.01/2.50 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod1)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f82])).
% 15.01/2.50 fof(f86,plain,(
% 15.01/2.50 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f82])).
% 15.01/2.50 fof(f87,plain,(
% 15.01/2.50 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=high)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f82])).
% 15.01/2.50 fof(f88,plain,(
% 15.01/2.50 greater(high,mod1)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f14])).
% 15.01/2.50 fof(f89,plain,(
% 15.01/2.50 greater(mod1,low)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f15])).
% 15.01/2.50 fof(f90,plain,(
% 15.01/2.50 greater(low,very_low)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f16])).
% 15.01/2.50 fof(f91,plain,(
% 15.01/2.50 greater(high,mod2)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f17])).
% 15.01/2.50 fof(f92,plain,(
% 15.01/2.50 greater(mod2,low)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f18])).
% 15.01/2.50 fof(f93,plain,(
% 15.01/2.50 greater(mod2,mod1)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f19])).
% 15.01/2.50 fof(f94,plain,(
% 15.01/2.50 (?[X,T0,T1,T2,T3]: (((((((((((organization(X)&robust_position(X))&~has_endowment(X))&age(X,T0)=zero)&greater(sigma,zero))&greater(tau,zero))&greater(sigma,tau))&smaller_or_equal(age(X,T1),tau))&greater(age(X,T2),tau))&smaller_or_equal(age(X,T2),sigma))&greater(age(X,T3),sigma))&((~smaller(hazard_of_mortality(X,T2),hazard_of_mortality(X,T3))|~smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1)))|~hazard_of_mortality(X,T1)=hazard_of_mortality(X,T0))))),
% 15.01/2.50 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 15.01/2.50 fof(f95,plain,(
% 15.01/2.50 (((((((((((organization(sK4_skl)&robust_position(sK4_skl))&~has_endowment(sK4_skl))&age(sK4_skl,sK5_skl)=zero)&greater(sigma,zero))&greater(tau,zero))&greater(sigma,tau))&smaller_or_equal(age(sK4_skl,sK6_skl),tau))&greater(age(sK4_skl,sK7_skl),tau))&smaller_or_equal(age(sK4_skl,sK7_skl),sigma))&greater(age(sK4_skl,sK8_skl),sigma))&((~smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl))|~smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl)))|~hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl)))),
% 15.01/2.50 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])).
% 15.01/2.50 fof(f96,plain,(
% 15.01/2.50 organization(sK4_skl)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f97,plain,(
% 15.01/2.50 robust_position(sK4_skl)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f98,plain,(
% 15.01/2.50 ~has_endowment(sK4_skl)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f99,plain,(
% 15.01/2.50 age(sK4_skl,sK5_skl)=zero),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f100,plain,(
% 15.01/2.50 greater(sigma,zero)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f101,plain,(
% 15.01/2.50 greater(tau,zero)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f102,plain,(
% 15.01/2.50 greater(sigma,tau)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f103,plain,(
% 15.01/2.50 smaller_or_equal(age(sK4_skl,sK6_skl),tau)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f104,plain,(
% 15.01/2.50 greater(age(sK4_skl,sK7_skl),tau)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f105,plain,(
% 15.01/2.50 smaller_or_equal(age(sK4_skl,sK7_skl),sigma)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f106,plain,(
% 15.01/2.50 greater(age(sK4_skl,sK8_skl),sigma)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f107,plain,(
% 15.01/2.50 ~smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl))|~smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl))|~hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl)),
% 15.01/2.50 inference(cnf_transformation,[status(thm)],[f95])).
% 15.01/2.50 fof(f108,definition,(
% 15.01/2.50 sQ0_spl <=> (smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f110,plain,(
% 15.01/2.50 ~smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl))|sQ0_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f108])).
% 15.01/2.50 fof(f111,definition,(
% 15.01/2.50 sQ1_spl <=> (smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl)))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f113,plain,(
% 15.01/2.50 ~smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl))|sQ1_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f111])).
% 15.01/2.50 fof(f114,definition,(
% 15.01/2.50 sQ2_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f115,plain,(
% 15.01/2.50 hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl)|~sQ2_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f114])).
% 15.01/2.50 fof(f116,plain,(
% 15.01/2.50 ~hazard_of_mortality(sK4_skl,sK6_skl)=hazard_of_mortality(sK4_skl,sK5_skl)|sQ2_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f114])).
% 15.01/2.50 fof(f117,plain,(
% 15.01/2.50 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f107,f108,f111,f114])).
% 15.01/2.50 fof(f118,plain,(
% 15.01/2.50 ![X0]: (smaller_or_equal(X0,X0))),
% 15.01/2.50 inference(destructive_equality_resolution,[status(thm)],[f26])).
% 15.01/2.50 fof(f120,plain,(
% 15.01/2.50 smaller(zero,tau)),
% 15.01/2.50 inference(resolution,[status(thm)],[f35,f101])).
% 15.01/2.50 fof(f121,plain,(
% 15.01/2.50 smaller(tau,sigma)),
% 15.01/2.50 inference(resolution,[status(thm)],[f35,f102])).
% 15.01/2.50 fof(f122,plain,(
% 15.01/2.50 smaller(zero,sigma)),
% 15.01/2.50 inference(resolution,[status(thm)],[f35,f100])).
% 15.01/2.50 fof(f124,plain,(
% 15.01/2.50 smaller_or_equal(zero,tau)),
% 15.01/2.50 inference(resolution,[status(thm)],[f120,f25])).
% 15.01/2.50 fof(f126,plain,(
% 15.01/2.50 smaller_or_equal(tau,sigma)),
% 15.01/2.50 inference(resolution,[status(thm)],[f121,f25])).
% 15.01/2.50 fof(f128,plain,(
% 15.01/2.50 smaller_or_equal(zero,sigma)),
% 15.01/2.50 inference(resolution,[status(thm)],[f122,f25])).
% 15.01/2.50 fof(f129,plain,(
% 15.01/2.50 smaller(zero,tau)|zero=tau),
% 15.01/2.50 inference(resolution,[status(thm)],[f24,f124])).
% 15.01/2.50 fof(f131,definition,(
% 15.01/2.50 sQ3_spl <=> (smaller(zero,tau))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f134,definition,(
% 15.01/2.50 sQ4_spl <=> (zero=tau)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f135,plain,(
% 15.01/2.50 zero=tau|~sQ4_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f134])).
% 15.01/2.50 fof(f137,plain,(
% 15.01/2.50 sQ3_spl|sQ4_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f129,f131,f134])).
% 15.01/2.50 fof(f138,plain,(
% 15.01/2.50 ~greater(zero,tau)),
% 15.01/2.50 inference(resolution,[status(thm)],[f37,f101])).
% 15.01/2.50 fof(f139,plain,(
% 15.01/2.50 ~greater(tau,sigma)),
% 15.01/2.50 inference(resolution,[status(thm)],[f37,f102])).
% 15.01/2.50 fof(f143,plain,(
% 15.01/2.50 smaller(tau,tau)|~sQ4_spl),
% 15.01/2.50 inference(backward_demodulation,[status(thm)],[f135,f120])).
% 15.01/2.50 fof(f147,plain,(
% 15.01/2.50 ~greater(mod1,high)),
% 15.01/2.50 inference(resolution,[status(thm)],[f88,f37])).
% 15.01/2.50 fof(f148,plain,(
% 15.01/2.50 smaller(mod1,high)),
% 15.01/2.50 inference(resolution,[status(thm)],[f88,f35])).
% 15.01/2.50 fof(f149,plain,(
% 15.01/2.50 ~greater(low,mod1)),
% 15.01/2.50 inference(resolution,[status(thm)],[f89,f37])).
% 15.01/2.50 fof(f150,plain,(
% 15.01/2.50 smaller(low,mod1)),
% 15.01/2.50 inference(resolution,[status(thm)],[f89,f35])).
% 15.01/2.50 fof(f151,plain,(
% 15.01/2.50 ~greater(very_low,low)),
% 15.01/2.50 inference(resolution,[status(thm)],[f90,f37])).
% 15.01/2.50 fof(f152,plain,(
% 15.01/2.50 smaller(very_low,low)),
% 15.01/2.50 inference(resolution,[status(thm)],[f90,f35])).
% 15.01/2.50 fof(f153,plain,(
% 15.01/2.50 ~greater(mod2,high)),
% 15.01/2.50 inference(resolution,[status(thm)],[f91,f37])).
% 15.01/2.50 fof(f154,plain,(
% 15.01/2.50 smaller(mod2,high)),
% 15.01/2.50 inference(resolution,[status(thm)],[f91,f35])).
% 15.01/2.50 fof(f158,plain,(
% 15.01/2.50 smaller(mod1,mod2)),
% 15.01/2.50 inference(resolution,[status(thm)],[f93,f35])).
% 15.01/2.50 fof(f159,plain,(
% 15.01/2.50 smaller(tau,sigma)|tau=sigma),
% 15.01/2.50 inference(resolution,[status(thm)],[f126,f24])).
% 15.01/2.50 fof(f160,definition,(
% 15.01/2.50 sQ5_spl <=> (smaller(tau,sigma))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f163,definition,(
% 15.01/2.50 sQ6_spl <=> (tau=sigma)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f164,plain,(
% 15.01/2.50 tau=sigma|~sQ6_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f163])).
% 15.01/2.50 fof(f166,plain,(
% 15.01/2.50 sQ5_spl|sQ6_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f159,f160,f163])).
% 15.01/2.50 fof(f169,plain,(
% 15.01/2.50 greater(tau,tau)|~sQ6_spl),
% 15.01/2.50 inference(backward_demodulation,[status(thm)],[f164,f102])).
% 15.01/2.50 fof(f172,plain,(
% 15.01/2.50 ~greater(tau,tau)|~sQ4_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f135,f138])).
% 15.01/2.50 fof(f176,plain,(
% 15.01/2.50 greater(tau,tau)|~sQ4_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f143,f34])).
% 15.01/2.50 fof(f178,plain,(
% 15.01/2.50 $false|~sQ4_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f176,f172])).
% 15.01/2.50 fof(f179,plain,(
% 15.01/2.50 ~sQ4_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f178])).
% 15.01/2.50 fof(f185,plain,(
% 15.01/2.50 greater_or_equal(mod2,mod1)),
% 15.01/2.50 inference(resolution,[status(thm)],[f30,f93])).
% 15.01/2.50 fof(f187,plain,(
% 15.01/2.50 greater_or_equal(low,very_low)),
% 15.01/2.50 inference(resolution,[status(thm)],[f30,f90])).
% 15.01/2.50 fof(f188,plain,(
% 15.01/2.50 greater_or_equal(mod1,low)),
% 15.01/2.50 inference(resolution,[status(thm)],[f30,f89])).
% 15.01/2.50 fof(f189,plain,(
% 15.01/2.50 greater_or_equal(high,mod2)),
% 15.01/2.50 inference(resolution,[status(thm)],[f30,f91])).
% 15.01/2.50 fof(f190,plain,(
% 15.01/2.50 greater_or_equal(high,mod1)),
% 15.01/2.50 inference(resolution,[status(thm)],[f30,f88])).
% 15.01/2.50 fof(f193,plain,(
% 15.01/2.50 ![X0]: (~greater(X0,low)|greater(X0,very_low))),
% 15.01/2.50 inference(resolution,[status(thm)],[f40,f90])).
% 15.01/2.50 fof(f194,plain,(
% 15.01/2.50 ![X0]: (~greater(X0,mod1)|greater(X0,low))),
% 15.01/2.50 inference(resolution,[status(thm)],[f40,f89])).
% 15.01/2.50 fof(f199,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater_or_equal(X0,X2))),
% 15.01/2.50 inference(resolution,[status(thm)],[f40,f30])).
% 15.01/2.50 fof(f200,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|~greater(X2,X0))),
% 15.01/2.50 inference(resolution,[status(thm)],[f40,f37])).
% 15.01/2.50 fof(f201,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|smaller(X2,X0))),
% 15.01/2.50 inference(resolution,[status(thm)],[f40,f35])).
% 15.01/2.50 fof(f206,plain,(
% 15.01/2.50 ~greater(tau,tau)|~sQ6_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f169,f37])).
% 15.01/2.50 fof(f208,plain,(
% 15.01/2.50 $false|~sQ6_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f206,f169])).
% 15.01/2.50 fof(f209,plain,(
% 15.01/2.50 ~sQ6_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f208])).
% 15.01/2.50 fof(f211,plain,(
% 15.01/2.50 smaller(age(sK4_skl,sK6_skl),tau)|age(sK4_skl,sK6_skl)=tau),
% 15.01/2.50 inference(resolution,[status(thm)],[f103,f24])).
% 15.01/2.50 fof(f212,definition,(
% 15.01/2.50 sQ7_spl <=> (smaller(age(sK4_skl,sK6_skl),tau))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f213,plain,(
% 15.01/2.50 smaller(age(sK4_skl,sK6_skl),tau)|~sQ7_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f212])).
% 15.01/2.50 fof(f215,definition,(
% 15.01/2.50 sQ8_spl <=> (age(sK4_skl,sK6_skl)=tau)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f216,plain,(
% 15.01/2.50 age(sK4_skl,sK6_skl)=tau|~sQ8_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f215])).
% 15.01/2.50 fof(f218,plain,(
% 15.01/2.50 sQ7_spl|sQ8_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f211,f212,f215])).
% 15.01/2.50 fof(f221,plain,(
% 15.01/2.50 smaller_or_equal(mod1,high)),
% 15.01/2.50 inference(resolution,[status(thm)],[f148,f25])).
% 15.01/2.50 fof(f224,plain,(
% 15.01/2.50 smaller_or_equal(low,mod1)),
% 15.01/2.50 inference(resolution,[status(thm)],[f150,f25])).
% 15.01/2.50 fof(f227,plain,(
% 15.01/2.50 smaller_or_equal(very_low,low)),
% 15.01/2.50 inference(resolution,[status(thm)],[f152,f25])).
% 15.01/2.50 fof(f230,plain,(
% 15.01/2.50 smaller_or_equal(mod2,high)),
% 15.01/2.50 inference(resolution,[status(thm)],[f154,f25])).
% 15.01/2.50 fof(f234,plain,(
% 15.01/2.50 ![X0,X1]: (X0=X1|greater(X0,X1)|greater(X1,X0))),
% 15.01/2.50 inference(resolution,[status(thm)],[f41,f34])).
% 15.01/2.50 fof(f241,plain,(
% 15.01/2.50 greater(tau,zero)),
% 15.01/2.50 inference(resolution,[status(thm)],[f120,f34])).
% 15.01/2.50 fof(f243,plain,(
% 15.01/2.50 ![X0]: (~greater(X0,tau)|greater(X0,zero))),
% 15.01/2.50 inference(resolution,[status(thm)],[f101,f40])).
% 15.01/2.50 fof(f244,plain,(
% 15.01/2.50 greater_or_equal(tau,zero)),
% 15.01/2.50 inference(resolution,[status(thm)],[f101,f30])).
% 15.01/2.50 fof(f282,definition,(
% 15.01/2.50 sQ13_spl <=> (greater(mod2,very_low))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f283,plain,(
% 15.01/2.50 greater(mod2,very_low)|~sQ13_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f282])).
% 15.01/2.50 fof(f284,plain,(
% 15.01/2.50 ~greater(mod2,very_low)|sQ13_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f282])).
% 15.01/2.50 fof(f285,definition,(
% 15.01/2.50 sQ14_spl <=> (mod2=very_low)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f286,plain,(
% 15.01/2.50 mod2=very_low|~sQ14_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f285])).
% 15.01/2.50 fof(f287,plain,(
% 15.01/2.50 ~mod2=very_low|sQ14_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f285])).
% 15.01/2.50 fof(f292,plain,(
% 15.01/2.50 greater(high,mod2)|high=mod2),
% 15.01/2.50 inference(resolution,[status(thm)],[f189,f29])).
% 15.01/2.50 fof(f293,definition,(
% 15.01/2.50 sQ15_spl <=> (greater(high,mod2))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f296,definition,(
% 15.01/2.50 sQ16_spl <=> (high=mod2)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f297,plain,(
% 15.01/2.50 high=mod2|~sQ16_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f296])).
% 15.01/2.50 fof(f299,plain,(
% 15.01/2.50 sQ15_spl|sQ16_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f292,f293,f296])).
% 15.01/2.50 fof(f307,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~has_endowment(X0)|~has_immunity(X0,X1)|~greater(age(X0,X1),X2)|~greater(X2,eta))),
% 15.01/2.50 inference(resolution,[status(thm)],[f48,f40])).
% 15.01/2.50 fof(f309,definition,(
% 15.01/2.50 sQ17_spl <=> (has_endowment(sK4_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f310,plain,(
% 15.01/2.50 has_endowment(sK4_skl)|~sQ17_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f309])).
% 15.01/2.50 fof(f312,definition,(
% 15.01/2.50 sQ18_spl <=> (smaller_or_equal(age(sK4_skl,sK0_skl(sK4_skl)),eta))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f313,plain,(
% 15.01/2.50 smaller_or_equal(age(sK4_skl,sK0_skl(sK4_skl)),eta)|~sQ18_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f312])).
% 15.01/2.50 fof(f315,definition,(
% 15.01/2.50 sQ19_spl <=> (greater(age(sK4_skl,sK1_skl(sK4_skl)),eta))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f316,plain,(
% 15.01/2.50 greater(age(sK4_skl,sK1_skl(sK4_skl)),eta)|~sQ19_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f315])).
% 15.01/2.50 fof(f319,plain,(
% 15.01/2.50 $false|~sQ17_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f310,f98])).
% 15.01/2.50 fof(f320,plain,(
% 15.01/2.50 ~sQ17_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f319])).
% 15.01/2.50 fof(f322,plain,(
% 15.01/2.50 greater_or_equal(sigma,zero)),
% 15.01/2.50 inference(resolution,[status(thm)],[f100,f30])).
% 15.01/2.50 fof(f323,plain,(
% 15.01/2.50 ~greater(zero,sigma)),
% 15.01/2.50 inference(resolution,[status(thm)],[f100,f37])).
% 15.01/2.50 fof(f327,plain,(
% 15.01/2.50 smaller(zero,sigma)|zero=sigma),
% 15.01/2.50 inference(resolution,[status(thm)],[f128,f24])).
% 15.01/2.50 fof(f328,definition,(
% 15.01/2.50 sQ20_spl <=> (smaller(zero,sigma))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f331,definition,(
% 15.01/2.50 sQ21_spl <=> (zero=sigma)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f332,plain,(
% 15.01/2.50 zero=sigma|~sQ21_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f331])).
% 15.01/2.50 fof(f334,plain,(
% 15.01/2.50 sQ20_spl|sQ21_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f327,f328,f331])).
% 15.01/2.50 fof(f346,plain,(
% 15.01/2.50 greater_or_equal(age(sK4_skl,sK7_skl),tau)),
% 15.01/2.50 inference(resolution,[status(thm)],[f104,f30])).
% 15.01/2.50 fof(f348,plain,(
% 15.01/2.50 smaller(tau,age(sK4_skl,sK7_skl))),
% 15.01/2.50 inference(resolution,[status(thm)],[f104,f35])).
% 15.01/2.50 fof(f349,plain,(
% 15.01/2.50 ![X0]: (~greater(tau,X0)|~greater(X0,sigma))),
% 15.01/2.50 inference(resolution,[status(thm)],[f139,f40])).
% 15.01/2.50 fof(f354,plain,(
% 15.01/2.50 ![X0]: (~greater(X0,sigma)|greater(X0,tau))),
% 15.01/2.50 inference(resolution,[status(thm)],[f102,f40])).
% 15.01/2.50 fof(f355,plain,(
% 15.01/2.50 greater_or_equal(sigma,tau)),
% 15.01/2.50 inference(resolution,[status(thm)],[f102,f30])).
% 15.01/2.50 fof(f358,plain,(
% 15.01/2.50 smaller(mod1,high)|mod1=high),
% 15.01/2.50 inference(resolution,[status(thm)],[f221,f24])).
% 15.01/2.50 fof(f359,definition,(
% 15.01/2.50 sQ22_spl <=> (smaller(mod1,high))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f360,plain,(
% 15.01/2.50 smaller(mod1,high)|~sQ22_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f359])).
% 15.01/2.50 fof(f362,definition,(
% 15.01/2.50 sQ23_spl <=> (mod1=high)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f363,plain,(
% 15.01/2.50 mod1=high|~sQ23_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f362])).
% 15.01/2.50 fof(f365,plain,(
% 15.01/2.50 sQ22_spl|sQ23_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f358,f359,f362])).
% 15.01/2.50 fof(f369,definition,(
% 15.01/2.50 sQ24_spl <=> (smaller(low,high))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f370,plain,(
% 15.01/2.50 smaller(low,high)|~sQ24_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f369])).
% 15.01/2.50 fof(f372,definition,(
% 15.01/2.50 sQ25_spl <=> (low=high)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f373,plain,(
% 15.01/2.50 low=high|~sQ25_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f372])).
% 15.01/2.50 fof(f387,plain,(
% 15.01/2.50 greater(tau,sigma)|~sQ21_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f332,f241])).
% 15.01/2.50 fof(f388,plain,(
% 15.01/2.50 $false|~sQ21_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f387,f139])).
% 15.01/2.50 fof(f389,plain,(
% 15.01/2.50 ~sQ21_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f388])).
% 15.01/2.50 fof(f390,plain,(
% 15.01/2.50 greater(tau,zero)|tau=zero),
% 15.01/2.50 inference(resolution,[status(thm)],[f244,f29])).
% 15.01/2.50 fof(f391,definition,(
% 15.01/2.50 sQ26_spl <=> (greater(tau,zero))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f394,plain,(
% 15.01/2.50 sQ26_spl|sQ4_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f390,f391,f134])).
% 15.01/2.50 fof(f411,plain,(
% 15.01/2.50 greater(mod2,mod2)|~sQ14_spl|~sQ13_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f286,f283])).
% 15.01/2.50 fof(f414,plain,(
% 15.01/2.50 ~greater(mod2,mod2)|~sQ14_spl|~sQ13_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f411,f37])).
% 15.01/2.50 fof(f416,plain,(
% 15.01/2.50 $false|~sQ14_spl|~sQ13_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f414,f411])).
% 15.01/2.50 fof(f417,plain,(
% 15.01/2.50 ~sQ14_spl|~sQ13_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f416])).
% 15.01/2.50 fof(f418,plain,(
% 15.01/2.50 ![X0]: (has_endowment(X0)|~organization(X0)|smaller_or_equal(age(X0,sK0_skl(X0)),eta))),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f50,f55])).
% 15.01/2.50 fof(f419,plain,(
% 15.01/2.50 has_endowment(sK4_skl)|smaller_or_equal(age(sK4_skl,sK0_skl(sK4_skl)),eta)),
% 15.01/2.50 inference(resolution,[status(thm)],[f418,f96])).
% 15.01/2.50 fof(f420,plain,(
% 15.01/2.50 sQ17_spl|sQ18_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f419,f309,f312])).
% 15.01/2.50 fof(f421,plain,(
% 15.01/2.50 greater(sigma,zero)|sigma=zero),
% 15.01/2.50 inference(resolution,[status(thm)],[f322,f29])).
% 15.01/2.50 fof(f422,definition,(
% 15.01/2.50 sQ27_spl <=> (greater(sigma,zero))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f425,plain,(
% 15.01/2.50 sQ27_spl|sQ21_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f421,f422,f331])).
% 15.01/2.50 fof(f431,plain,(
% 15.01/2.50 smaller(age(sK4_skl,sK7_skl),sigma)|age(sK4_skl,sK7_skl)=sigma),
% 15.01/2.50 inference(resolution,[status(thm)],[f105,f24])).
% 15.01/2.50 fof(f432,definition,(
% 15.01/2.50 sQ28_spl <=> (smaller(age(sK4_skl,sK7_skl),sigma))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f433,plain,(
% 15.01/2.50 smaller(age(sK4_skl,sK7_skl),sigma)|~sQ28_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f432])).
% 15.01/2.50 fof(f435,definition,(
% 15.01/2.50 sQ29_spl <=> (age(sK4_skl,sK7_skl)=sigma)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f436,plain,(
% 15.01/2.50 age(sK4_skl,sK7_skl)=sigma|~sQ29_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f435])).
% 15.01/2.50 fof(f438,plain,(
% 15.01/2.50 sQ28_spl|sQ29_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f431,f432,f435])).
% 15.01/2.50 fof(f449,plain,(
% 15.01/2.50 greater(sigma,tau)|sigma=tau),
% 15.01/2.50 inference(resolution,[status(thm)],[f355,f29])).
% 15.01/2.50 fof(f450,definition,(
% 15.01/2.50 sQ30_spl <=> (greater(sigma,tau))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f453,plain,(
% 15.01/2.50 sQ30_spl|sQ6_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f449,f450,f163])).
% 15.01/2.50 fof(f454,plain,(
% 15.01/2.50 greater(high,mod1)|~sQ22_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f360,f34])).
% 15.01/2.50 fof(f459,plain,(
% 15.01/2.50 smaller_or_equal(high,mod1)|~sQ25_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f373,f224])).
% 15.01/2.50 fof(f460,plain,(
% 15.01/2.50 smaller(high,mod1)|high=mod1|~sQ25_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f459,f24])).
% 15.01/2.50 fof(f461,definition,(
% 15.01/2.50 sQ31_spl <=> (smaller(high,mod1))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f462,plain,(
% 15.01/2.50 smaller(high,mod1)|~sQ31_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f461])).
% 15.01/2.50 fof(f464,plain,(
% 15.01/2.50 sQ31_spl|sQ23_spl|~sQ25_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f460,f461,f362,f372])).
% 15.01/2.50 fof(f471,plain,(
% 15.01/2.50 ~robust_position(sK4_skl)|~positional_advantage(sK4_skl,sK6_skl)),
% 15.01/2.50 inference(resolution,[status(thm)],[f75,f103])).
% 15.01/2.50 fof(f472,definition,(
% 15.01/2.50 sQ32_spl <=> (robust_position(sK4_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f474,plain,(
% 15.01/2.50 ~robust_position(sK4_skl)|sQ32_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f472])).
% 15.01/2.50 fof(f475,definition,(
% 15.01/2.50 sQ33_spl <=> (positional_advantage(sK4_skl,sK6_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f478,plain,(
% 15.01/2.50 ~sQ32_spl|~sQ33_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f471,f472,f475])).
% 15.01/2.50 fof(f479,plain,(
% 15.01/2.50 $false|sQ32_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f474,f97])).
% 15.01/2.50 fof(f480,plain,(
% 15.01/2.50 sQ32_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f479])).
% 15.01/2.50 fof(f481,plain,(
% 15.01/2.50 greater(low,very_low)|low=very_low),
% 15.01/2.50 inference(resolution,[status(thm)],[f187,f29])).
% 15.01/2.50 fof(f482,definition,(
% 15.01/2.50 sQ34_spl <=> (greater(low,very_low))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f483,plain,(
% 15.01/2.50 greater(low,very_low)|~sQ34_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f482])).
% 15.01/2.50 fof(f485,definition,(
% 15.01/2.50 sQ35_spl <=> (low=very_low)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f486,plain,(
% 15.01/2.50 low=very_low|~sQ35_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f485])).
% 15.01/2.50 fof(f488,plain,(
% 15.01/2.50 sQ34_spl|sQ35_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f481,f482,f485])).
% 15.01/2.50 fof(f497,plain,(
% 15.01/2.50 greater(low,low)|~sQ35_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f486,f90])).
% 15.01/2.50 fof(f500,plain,(
% 15.01/2.50 ~greater(low,low)|~sQ35_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f497,f37])).
% 15.01/2.50 fof(f502,plain,(
% 15.01/2.50 $false|~sQ35_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f500,f497])).
% 15.01/2.50 fof(f503,plain,(
% 15.01/2.50 ~sQ35_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f502])).
% 15.01/2.50 fof(f512,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~age(X0,X1)=zero|greater(age(X0,X2),sigma)|~dissimilar(X0,X1,X2))),
% 15.01/2.50 inference(backward_subsumption_resolution,[status(thm)],[f70,f59])).
% 15.01/2.50 fof(f523,plain,(
% 15.01/2.50 smaller(mod2,high)|mod2=high),
% 15.01/2.50 inference(resolution,[status(thm)],[f230,f24])).
% 15.01/2.50 fof(f524,definition,(
% 15.01/2.50 sQ37_spl <=> (smaller(mod2,high))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f527,plain,(
% 15.01/2.50 sQ37_spl|sQ16_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f523,f524,f296])).
% 15.01/2.50 fof(f528,plain,(
% 15.01/2.50 greater(high,mod2)),
% 15.01/2.50 inference(resolution,[status(thm)],[f154,f34])).
% 15.01/2.50 fof(f531,plain,(
% 15.01/2.50 greater(mod2,mod1)),
% 15.01/2.50 inference(resolution,[status(thm)],[f158,f34])).
% 15.01/2.50 fof(f539,plain,(
% 15.01/2.50 ~robust_position(sK4_skl)|positional_advantage(sK4_skl,sK7_skl)),
% 15.01/2.50 inference(resolution,[status(thm)],[f76,f104])).
% 15.01/2.50 fof(f540,plain,(
% 15.01/2.50 ![X0,X1,X2]: (~robust_position(X0)|positional_advantage(X0,X1)|~greater(age(X0,X1),X2)|~greater(X2,tau))),
% 15.01/2.50 inference(resolution,[status(thm)],[f76,f40])).
% 15.01/2.50 fof(f541,definition,(
% 15.01/2.50 sQ38_spl <=> (positional_advantage(sK4_skl,sK7_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f544,plain,(
% 15.01/2.50 ~sQ32_spl|sQ38_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f539,f472,f541])).
% 15.01/2.50 fof(f545,plain,(
% 15.01/2.50 greater(high,mod1)|high=mod1),
% 15.01/2.50 inference(resolution,[status(thm)],[f190,f29])).
% 15.01/2.50 fof(f546,definition,(
% 15.01/2.50 sQ39_spl <=> (greater(high,mod1))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f549,plain,(
% 15.01/2.50 sQ39_spl|sQ23_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f545,f546,f362])).
% 15.01/2.50 fof(f564,plain,(
% 15.01/2.50 greater_or_equal(mod2,high)|~sQ23_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f363,f185])).
% 15.01/2.50 fof(f565,plain,(
% 15.01/2.50 greater(mod2,high)|mod2=high|~sQ23_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f564,f29])).
% 15.01/2.50 fof(f566,definition,(
% 15.01/2.50 sQ40_spl <=> (greater(mod2,high))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f567,plain,(
% 15.01/2.50 greater(mod2,high)|~sQ40_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f566])).
% 15.01/2.50 fof(f569,plain,(
% 15.01/2.50 sQ40_spl|sQ16_spl|~sQ23_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f565,f566,f296,f362])).
% 15.01/2.50 fof(f570,plain,(
% 15.01/2.50 $false|~sQ40_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f567,f153])).
% 15.01/2.50 fof(f571,plain,(
% 15.01/2.50 ~sQ40_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f570])).
% 15.01/2.50 fof(f591,plain,(
% 15.01/2.50 greater(mod1,high)|~sQ31_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f462,f34])).
% 15.01/2.50 fof(f593,plain,(
% 15.01/2.50 smaller(low,mod1)|low=mod1),
% 15.01/2.50 inference(resolution,[status(thm)],[f224,f24])).
% 15.01/2.50 fof(f594,definition,(
% 15.01/2.50 sQ41_spl <=> (smaller(low,mod1))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f595,plain,(
% 15.01/2.50 smaller(low,mod1)|~sQ41_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f594])).
% 15.01/2.50 fof(f597,definition,(
% 15.01/2.50 sQ42_spl <=> (low=mod1)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f598,plain,(
% 15.01/2.50 low=mod1|~sQ42_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f597])).
% 15.01/2.50 fof(f599,plain,(
% 15.01/2.50 ~low=mod1|sQ42_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f597])).
% 15.01/2.50 fof(f600,plain,(
% 15.01/2.50 sQ41_spl|sQ42_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f593,f594,f597])).
% 15.01/2.50 fof(f605,plain,(
% 15.01/2.50 ~robust_position(sK4_skl)|~greater(zero,tau)|positional_advantage(sK4_skl,sK5_skl)),
% 15.01/2.50 inference(paramodulation,[status(thm)],[f99,f76])).
% 15.01/2.50 fof(f606,plain,(
% 15.01/2.50 ~robust_position(sK4_skl)|~smaller_or_equal(zero,tau)|~positional_advantage(sK4_skl,sK5_skl)),
% 15.01/2.50 inference(paramodulation,[status(thm)],[f99,f75])).
% 15.01/2.50 fof(f609,definition,(
% 15.01/2.50 sQ43_spl <=> (greater(zero,tau))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f612,definition,(
% 15.01/2.50 sQ44_spl <=> (positional_advantage(sK4_skl,sK5_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f615,plain,(
% 15.01/2.50 ~sQ32_spl|~sQ43_spl|sQ44_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f605,f472,f609,f612])).
% 15.01/2.50 fof(f616,definition,(
% 15.01/2.50 sQ45_spl <=> (smaller_or_equal(zero,tau))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f618,plain,(
% 15.01/2.50 ~smaller_or_equal(zero,tau)|sQ45_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f616])).
% 15.01/2.50 fof(f619,plain,(
% 15.01/2.50 ~sQ32_spl|~sQ45_spl|~sQ44_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f606,f472,f616,f612])).
% 15.01/2.50 fof(f623,definition,(
% 15.01/2.50 sQ47_spl <=> (has_immunity(sK4_skl,sK5_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f624,plain,(
% 15.01/2.50 has_immunity(sK4_skl,sK5_skl)|~sQ47_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f623])).
% 15.01/2.50 fof(f631,plain,(
% 15.01/2.50 $false|sQ45_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f618,f124])).
% 15.01/2.50 fof(f632,plain,(
% 15.01/2.50 sQ45_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f631])).
% 15.01/2.50 fof(f646,plain,(
% 15.01/2.50 ~greater(mod1,mod1)|~sQ42_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f598,f149])).
% 15.01/2.50 fof(f648,plain,(
% 15.01/2.50 smaller(mod1,mod1)|~sQ42_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f598,f150])).
% 15.01/2.50 fof(f649,plain,(
% 15.01/2.50 greater(mod1,mod1)|~sQ42_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f648,f34])).
% 15.01/2.50 fof(f651,plain,(
% 15.01/2.50 $false|~sQ42_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f649,f646])).
% 15.01/2.50 fof(f652,plain,(
% 15.01/2.50 ~sQ42_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f651])).
% 15.01/2.50 fof(f655,plain,(
% 15.01/2.50 smaller(very_low,low)|very_low=low),
% 15.01/2.50 inference(resolution,[status(thm)],[f227,f24])).
% 15.01/2.50 fof(f656,definition,(
% 15.01/2.50 sQ49_spl <=> (smaller(very_low,low))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f659,plain,(
% 15.01/2.50 sQ49_spl|sQ35_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f655,f656,f485])).
% 15.01/2.50 fof(f660,plain,(
% 15.01/2.50 ![X0]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK8_skl))),
% 15.01/2.50 inference(resolution,[status(thm)],[f69,f106])).
% 15.01/2.50 fof(f661,plain,(
% 15.01/2.50 ![X0,X1,X2,X3]: (~organization(X0)|~age(X0,X1)=zero|dissimilar(X0,X1,X2)|~greater(age(X0,X2),X3)|~greater(X3,sigma))),
% 15.01/2.50 inference(resolution,[status(thm)],[f69,f40])).
% 15.01/2.50 fof(f662,plain,(
% 15.01/2.50 ![X0]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|~greater(zero,sigma)|dissimilar(sK4_skl,X0,sK5_skl))),
% 15.01/2.50 inference(paramodulation,[status(thm)],[f99,f69])).
% 15.01/2.50 fof(f663,definition,(
% 15.01/2.50 sQ50_spl <=> (organization(sK4_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f665,plain,(
% 15.01/2.50 ~organization(sK4_skl)|sQ50_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f663])).
% 15.01/2.50 fof(f666,definition,(
% 15.01/2.50 ![X0]: (sQ51_spl <=> (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK8_skl)))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f667,plain,(
% 15.01/2.50 ![X0]: (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK8_skl)|~sQ51_spl)),
% 15.01/2.50 inference(component_clause,[status(thm)],[f666])).
% 15.01/2.50 fof(f669,plain,(
% 15.01/2.50 ~sQ50_spl|sQ51_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f660,f663,f666])).
% 15.01/2.50 fof(f670,definition,(
% 15.01/2.50 ![X0]: (sQ52_spl <=> (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK5_skl)))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f671,plain,(
% 15.01/2.50 ![X0]: (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK5_skl)|~sQ52_spl)),
% 15.01/2.50 inference(component_clause,[status(thm)],[f670])).
% 15.01/2.50 fof(f673,definition,(
% 15.01/2.50 sQ53_spl <=> (greater(zero,sigma))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f676,plain,(
% 15.01/2.50 ~sQ50_spl|sQ52_spl|~sQ53_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f662,f663,f670,f673])).
% 15.01/2.50 fof(f677,plain,(
% 15.01/2.50 $false|sQ50_spl),
% 15.01/2.50 inference(forward_subsumption_resolution,[status(thm)],[f665,f96])).
% 15.01/2.50 fof(f678,plain,(
% 15.01/2.50 sQ50_spl),
% 15.01/2.50 inference(contradiction_clause,[status(thm)],[f677])).
% 15.01/2.50 fof(f679,plain,(
% 15.01/2.50 ~organization(sK4_skl)|is_aligned(sK4_skl,sK5_skl)),
% 15.01/2.50 inference(resolution,[status(thm)],[f65,f99])).
% 15.01/2.50 fof(f681,definition,(
% 15.01/2.50 sQ54_spl <=> (is_aligned(sK4_skl,sK5_skl))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f682,plain,(
% 15.01/2.50 is_aligned(sK4_skl,sK5_skl)|~sQ54_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f681])).
% 15.01/2.50 fof(f684,plain,(
% 15.01/2.50 ~sQ50_spl|sQ54_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f679,f663,f681])).
% 15.01/2.50 fof(f685,definition,(
% 15.01/2.50 sQ55_spl <=> (zero=zero)),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f687,plain,(
% 15.01/2.50 ~zero=zero|sQ55_spl),
% 15.01/2.50 inference(component_clause,[status(thm)],[f685])).
% 15.01/2.50 fof(f693,plain,(
% 15.01/2.50 greater(mod1,low)|mod1=low),
% 15.01/2.50 inference(resolution,[status(thm)],[f188,f29])).
% 15.01/2.50 fof(f694,definition,(
% 15.01/2.50 sQ56_spl <=> (greater(mod1,low))),
% 15.01/2.50 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 15.01/2.50 fof(f697,plain,(
% 15.01/2.50 sQ56_spl|sQ42_spl),
% 15.01/2.50 inference(split_clause,[status(thm)],[f693,f694,f597])).
% 15.01/2.50 fof(f718,plain,(
% 15.01/2.50 greater(high,high)|~sQ16_spl),
% 15.01/2.50 inference(forward_demodulation,[status(thm)],[f297,f528])).
% 15.01/2.50 fof(f721,plain,(
% 15.01/2.50 ~greater(high,high)|~sQ16_spl),
% 15.01/2.50 inference(resolution,[status(thm)],[f718,f37])).
% 15.01/2.50 fof(f723,plain,(
% 15.01/2.50 $false|~sQ16_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f721,f718])).
% 15.01/2.51 fof(f724,plain,(
% 15.01/2.51 ~sQ16_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f723])).
% 15.01/2.51 fof(f730,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,X0,sK5_skl)|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ54_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f682,f63])).
% 15.01/2.51 fof(f731,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,sK5_skl,X0)|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ54_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f682,f62])).
% 15.01/2.51 fof(f732,definition,(
% 15.01/2.51 ![X0]: (sQ57_spl <=> (dissimilar(sK4_skl,X0,sK5_skl)|is_aligned(sK4_skl,X0)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f733,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,X0,sK5_skl)|is_aligned(sK4_skl,X0)|~sQ57_spl)),
% 15.01/2.51 inference(component_clause,[status(thm)],[f732])).
% 15.01/2.51 fof(f735,plain,(
% 15.01/2.51 sQ57_spl|~sQ50_spl|~sQ54_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f730,f732,f663,f681])).
% 15.01/2.51 fof(f736,definition,(
% 15.01/2.51 ![X0]: (sQ58_spl <=> (dissimilar(sK4_skl,sK5_skl,X0)|is_aligned(sK4_skl,X0)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f737,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,sK5_skl,X0)|is_aligned(sK4_skl,X0)|~sQ58_spl)),
% 15.01/2.51 inference(component_clause,[status(thm)],[f736])).
% 15.01/2.51 fof(f739,plain,(
% 15.01/2.51 sQ58_spl|~sQ50_spl|~sQ54_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f731,f736,f663,f681])).
% 15.01/2.51 fof(f743,plain,(
% 15.01/2.51 ~robust_position(sK4_skl)|~greater(tau,tau)|positional_advantage(sK4_skl,sK6_skl)|~sQ8_spl),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f216,f76])).
% 15.01/2.51 fof(f747,definition,(
% 15.01/2.51 sQ59_spl <=> (is_aligned(sK4_skl,sK6_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f754,definition,(
% 15.01/2.51 sQ61_spl <=> (greater(tau,sigma))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f758,definition,(
% 15.01/2.51 sQ62_spl <=> (greater(tau,tau))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f760,plain,(
% 15.01/2.51 ~greater(tau,tau)|sQ62_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f758])).
% 15.01/2.51 fof(f761,plain,(
% 15.01/2.51 ~sQ32_spl|~sQ62_spl|sQ33_spl|~sQ8_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f743,f472,f758,f475,f215])).
% 15.01/2.51 fof(f762,definition,(
% 15.01/2.51 sQ63_spl <=> (smaller_or_equal(tau,tau))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f764,plain,(
% 15.01/2.51 ~smaller_or_equal(tau,tau)|sQ63_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f762])).
% 15.01/2.51 fof(f766,definition,(
% 15.01/2.51 sQ64_spl <=> (greater(tau,eta))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f768,plain,(
% 15.01/2.51 ~greater(tau,eta)|sQ64_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f766])).
% 15.01/2.51 fof(f769,definition,(
% 15.01/2.51 sQ65_spl <=> (has_immunity(sK4_skl,sK6_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f770,plain,(
% 15.01/2.51 has_immunity(sK4_skl,sK6_skl)|~sQ65_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f769])).
% 15.01/2.51 fof(f771,plain,(
% 15.01/2.51 ~has_immunity(sK4_skl,sK6_skl)|sQ65_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f769])).
% 15.01/2.51 fof(f812,plain,(
% 15.01/2.51 $false|~sQ31_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f591,f147])).
% 15.01/2.51 fof(f813,plain,(
% 15.01/2.51 ~sQ31_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f812])).
% 15.01/2.51 fof(f823,plain,(
% 15.01/2.51 greater(high,low)|~sQ24_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f370,f34])).
% 15.01/2.51 fof(f828,definition,(
% 15.01/2.51 sQ69_spl <=> (hazard_of_mortality(sK4_skl,sK5_skl)=low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f829,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK5_skl)=low|~sQ69_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f828])).
% 15.01/2.51 fof(f830,plain,(
% 15.01/2.51 ~hazard_of_mortality(sK4_skl,sK5_skl)=low|sQ69_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f828])).
% 15.01/2.51 fof(f833,definition,(
% 15.01/2.51 sQ70_spl <=> (has_immunity(sK4_skl,sK7_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f834,plain,(
% 15.01/2.51 has_immunity(sK4_skl,sK7_skl)|~sQ70_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f833])).
% 15.01/2.51 fof(f836,definition,(
% 15.01/2.51 sQ71_spl <=> (is_aligned(sK4_skl,sK7_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f837,plain,(
% 15.01/2.51 is_aligned(sK4_skl,sK7_skl)|~sQ71_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f836])).
% 15.01/2.51 fof(f839,definition,(
% 15.01/2.51 sQ72_spl <=> (hazard_of_mortality(sK4_skl,sK7_skl)=mod1)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f840,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK7_skl)=mod1|~sQ72_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f839])).
% 15.01/2.51 fof(f844,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ47_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f624,f55])).
% 15.01/2.51 fof(f849,plain,(
% 15.01/2.51 ~sQ50_spl|sQ17_spl|~sQ47_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f844,f663,f309,f623])).
% 15.01/2.51 fof(f850,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_immunity(sK4_skl,sK7_skl)|~positional_advantage(sK4_skl,sK7_skl)|hazard_of_mortality(sK4_skl,sK7_skl)=low|~sQ71_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f837,f84])).
% 15.01/2.51 fof(f851,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,X0,sK7_skl)|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ71_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f837,f63])).
% 15.01/2.51 fof(f852,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,sK7_skl,X0)|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ71_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f837,f62])).
% 15.01/2.51 fof(f853,definition,(
% 15.01/2.51 sQ74_spl <=> (hazard_of_mortality(sK4_skl,sK7_skl)=low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f854,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK7_skl)=low|~sQ74_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f853])).
% 15.01/2.51 fof(f856,plain,(
% 15.01/2.51 ~sQ50_spl|sQ70_spl|~sQ38_spl|sQ74_spl|~sQ71_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f850,f663,f833,f541,f853,f836])).
% 15.01/2.51 fof(f857,definition,(
% 15.01/2.51 ![X0]: (sQ75_spl <=> (dissimilar(sK4_skl,X0,sK7_skl)|is_aligned(sK4_skl,X0)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f860,plain,(
% 15.01/2.51 sQ75_spl|~sQ50_spl|~sQ71_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f851,f857,f663,f836])).
% 15.01/2.51 fof(f861,definition,(
% 15.01/2.51 ![X0]: (sQ76_spl <=> (dissimilar(sK4_skl,sK7_skl,X0)|is_aligned(sK4_skl,X0)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f864,plain,(
% 15.01/2.51 sQ76_spl|~sQ50_spl|~sQ71_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f852,f861,f663,f836])).
% 15.01/2.51 fof(f866,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ70_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f834,f55])).
% 15.01/2.51 fof(f867,definition,(
% 15.01/2.51 sQ77_spl <=> (hazard_of_mortality(sK4_skl,sK7_skl)=very_low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f868,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK7_skl)=very_low|~sQ77_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f867])).
% 15.01/2.51 fof(f871,plain,(
% 15.01/2.51 ~sQ50_spl|sQ17_spl|~sQ70_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f866,f663,f309,f833])).
% 15.01/2.51 fof(f878,plain,(
% 15.01/2.51 greater(tau,age(sK4_skl,sK6_skl))|~sQ7_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f213,f34])).
% 15.01/2.51 fof(f897,plain,(
% 15.01/2.51 greater(mod1,very_low)),
% 15.01/2.51 inference(resolution,[status(thm)],[f193,f89])).
% 15.01/2.51 fof(f904,plain,(
% 15.01/2.51 greater(mod2,very_low)),
% 15.01/2.51 inference(resolution,[status(thm)],[f92,f193])).
% 15.01/2.51 fof(f912,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_immunity(sK4_skl,sK5_skl)|positional_advantage(sK4_skl,sK5_skl)|hazard_of_mortality(sK4_skl,sK5_skl)=mod2|~sQ54_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f86,f682])).
% 15.01/2.51 fof(f913,definition,(
% 15.01/2.51 sQ79_spl <=> (hazard_of_mortality(sK4_skl,sK7_skl)=mod2)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f914,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK7_skl)=mod2|~sQ79_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f913])).
% 15.01/2.51 fof(f917,definition,(
% 15.01/2.51 sQ80_spl <=> (hazard_of_mortality(sK4_skl,sK5_skl)=mod2)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f918,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK5_skl)=mod2|~sQ80_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f917])).
% 15.01/2.51 fof(f920,plain,(
% 15.01/2.51 ~sQ50_spl|sQ47_spl|sQ44_spl|sQ80_spl|~sQ54_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f912,f663,f623,f612,f917,f681])).
% 15.01/2.51 fof(f921,plain,(
% 15.01/2.51 ![X0]: (has_immunity(sK4_skl,X0)|is_aligned(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high)),
% 15.01/2.51 inference(resolution,[status(thm)],[f87,f96])).
% 15.01/2.51 fof(f922,plain,(
% 15.01/2.51 greater(high,low)|~sQ22_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f194,f454])).
% 15.01/2.51 fof(f934,definition,(
% 15.01/2.51 ![X0]: (sQ81_spl <=> (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK7_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f935,plain,(
% 15.01/2.51 ![X0]: (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK7_skl)|~sQ81_spl)),
% 15.01/2.51 inference(component_clause,[status(thm)],[f934])).
% 15.01/2.51 fof(f946,definition,(
% 15.01/2.51 sQ84_spl <=> (greater(sigma,eta))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f947,plain,(
% 15.01/2.51 greater(sigma,eta)|~sQ84_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f946])).
% 15.01/2.51 fof(f959,plain,(
% 15.01/2.51 greater(high,very_low)|~sQ24_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f823,f193])).
% 15.01/2.51 fof(f962,plain,(
% 15.01/2.51 ~greater(low,high)|~sQ24_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f823,f37])).
% 15.01/2.51 fof(f974,plain,(
% 15.01/2.51 greater_or_equal(mod1,very_low)),
% 15.01/2.51 inference(resolution,[status(thm)],[f897,f30])).
% 15.01/2.51 fof(f976,plain,(
% 15.01/2.51 smaller(very_low,mod1)),
% 15.01/2.51 inference(resolution,[status(thm)],[f897,f35])).
% 15.01/2.51 fof(f980,plain,(
% 15.01/2.51 smaller(very_low,mod2)),
% 15.01/2.51 inference(resolution,[status(thm)],[f904,f35])).
% 15.01/2.51 fof(f982,plain,(
% 15.01/2.51 greater_or_equal(high,very_low)|~sQ24_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f959,f30])).
% 15.01/2.51 fof(f984,plain,(
% 15.01/2.51 smaller(very_low,high)|~sQ24_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f959,f35])).
% 15.01/2.51 fof(f986,definition,(
% 15.01/2.51 sQ86_spl <=> (greater(high,low))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f987,plain,(
% 15.01/2.51 greater(high,low)|~sQ86_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f986])).
% 15.01/2.51 fof(f990,plain,(
% 15.01/2.51 greater(mod1,very_low)|mod1=very_low),
% 15.01/2.51 inference(resolution,[status(thm)],[f974,f29])).
% 15.01/2.51 fof(f991,definition,(
% 15.01/2.51 sQ87_spl <=> (greater(mod1,very_low))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f994,definition,(
% 15.01/2.51 sQ88_spl <=> (mod1=very_low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f995,plain,(
% 15.01/2.51 mod1=very_low|~sQ88_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f994])).
% 15.01/2.51 fof(f997,plain,(
% 15.01/2.51 sQ87_spl|sQ88_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f990,f991,f994])).
% 15.01/2.51 fof(f1003,plain,(
% 15.01/2.51 ~greater(mod1,low)|~sQ88_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f995,f151])).
% 15.01/2.51 fof(f1010,plain,(
% 15.01/2.51 $false|~sQ88_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f1003,f89])).
% 15.01/2.51 fof(f1011,plain,(
% 15.01/2.51 ~sQ88_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f1010])).
% 15.01/2.51 fof(f1014,plain,(
% 15.01/2.51 smaller_or_equal(very_low,mod1)),
% 15.01/2.51 inference(resolution,[status(thm)],[f976,f25])).
% 15.01/2.51 fof(f1045,plain,(
% 15.01/2.51 mod1=low|~sQ72_spl|~sQ74_spl),
% 15.01/2.51 inference(forward_demodulation,[status(thm)],[f840,f854])).
% 15.01/2.51 fof(f1046,plain,(
% 15.01/2.51 $false|sQ42_spl|~sQ72_spl|~sQ74_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f1045,f599])).
% 15.01/2.51 fof(f1047,plain,(
% 15.01/2.51 sQ42_spl|~sQ72_spl|~sQ74_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f1046])).
% 15.01/2.51 fof(f1052,plain,(
% 15.01/2.51 smaller_or_equal(very_low,mod2)),
% 15.01/2.51 inference(resolution,[status(thm)],[f980,f25])).
% 15.01/2.51 fof(f1058,plain,(
% 15.01/2.51 smaller(low,high)|~sQ86_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f987,f35])).
% 15.01/2.51 fof(f1082,plain,(
% 15.01/2.51 ![X0]: (~greater(X0,tau)|greater_or_equal(X0,zero))),
% 15.01/2.51 inference(resolution,[status(thm)],[f199,f241])).
% 15.01/2.51 fof(f1083,plain,(
% 15.01/2.51 ![X0]: (~greater(X0,sigma)|greater_or_equal(X0,zero))),
% 15.01/2.51 inference(resolution,[status(thm)],[f199,f100])).
% 15.01/2.51 fof(f1084,plain,(
% 15.01/2.51 ![X0]: (~greater(X0,sigma)|greater_or_equal(X0,tau))),
% 15.01/2.51 inference(resolution,[status(thm)],[f199,f102])).
% 15.01/2.51 fof(f1103,plain,(
% 15.01/2.51 smaller(very_low,mod1)|very_low=mod1),
% 15.01/2.51 inference(resolution,[status(thm)],[f1014,f24])).
% 15.01/2.51 fof(f1104,definition,(
% 15.01/2.51 sQ89_spl <=> (smaller(very_low,mod1))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1107,plain,(
% 15.01/2.51 sQ89_spl|sQ88_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1103,f1104,f994])).
% 15.01/2.51 fof(f1108,plain,(
% 15.01/2.51 smaller(very_low,mod2)|very_low=mod2),
% 15.01/2.51 inference(resolution,[status(thm)],[f1052,f24])).
% 15.01/2.51 fof(f1109,definition,(
% 15.01/2.51 sQ90_spl <=> (smaller(very_low,mod2))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1112,plain,(
% 15.01/2.51 sQ90_spl|sQ14_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1108,f1109,f285])).
% 15.01/2.51 fof(f1113,plain,(
% 15.01/2.51 $false|sQ13_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f284,f904])).
% 15.01/2.51 fof(f1114,plain,(
% 15.01/2.51 sQ13_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f1113])).
% 15.01/2.51 fof(f1119,plain,(
% 15.01/2.51 smaller_or_equal(low,high)|~sQ86_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1058,f25])).
% 15.01/2.51 fof(f1162,plain,(
% 15.01/2.51 ![X0]: (~greater(X0,tau)|smaller(zero,X0))),
% 15.01/2.51 inference(resolution,[status(thm)],[f201,f241])).
% 15.01/2.51 fof(f1163,plain,(
% 15.01/2.51 ![X0]: (~greater(X0,sigma)|smaller(zero,X0))),
% 15.01/2.51 inference(resolution,[status(thm)],[f201,f100])).
% 15.01/2.51 fof(f1164,plain,(
% 15.01/2.51 ![X0]: (~greater(X0,sigma)|smaller(tau,X0))),
% 15.01/2.51 inference(resolution,[status(thm)],[f201,f102])).
% 15.01/2.51 fof(f1186,plain,(
% 15.01/2.51 tau=tau|greater(tau,tau)|sQ62_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f234,f760])).
% 15.01/2.51 fof(f1272,definition,(
% 15.01/2.51 sQ92_spl <=> (tau=tau)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1275,plain,(
% 15.01/2.51 sQ92_spl|sQ62_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1186,f1272,f758])).
% 15.01/2.51 fof(f1282,definition,(
% 15.01/2.51 sQ94_spl <=> (mod1=mod1)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1305,plain,(
% 15.01/2.51 ~hazard_of_mortality(sK4_skl,sK6_skl)=mod2|~sQ80_spl|sQ2_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f918,f116])).
% 15.01/2.51 fof(f1306,plain,(
% 15.01/2.51 mod2=very_low|~sQ79_spl|~sQ77_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f914,f868])).
% 15.01/2.51 fof(f1307,plain,(
% 15.01/2.51 sQ14_spl|~sQ79_spl|~sQ77_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1306,f285,f913,f867])).
% 15.01/2.51 fof(f1308,plain,(
% 15.01/2.51 ~mod2=low|~sQ80_spl|sQ69_spl),
% 15.01/2.51 inference(forward_demodulation,[status(thm)],[f918,f830])).
% 15.01/2.51 fof(f1309,plain,(
% 15.01/2.51 smaller(low,high)|low=high|~sQ86_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1119,f24])).
% 15.01/2.51 fof(f1310,plain,(
% 15.01/2.51 sQ24_spl|sQ25_spl|~sQ86_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1309,f369,f372,f986])).
% 15.01/2.51 fof(f1311,plain,(
% 15.01/2.51 sQ86_spl|~sQ22_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f922,f986,f359])).
% 15.01/2.51 fof(f1341,plain,(
% 15.01/2.51 greater(high,very_low)|high=very_low|~sQ24_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f982,f29])).
% 15.01/2.51 fof(f1342,definition,(
% 15.01/2.51 sQ96_spl <=> (greater(high,very_low))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1345,definition,(
% 15.01/2.51 sQ97_spl <=> (high=very_low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1346,plain,(
% 15.01/2.51 high=very_low|~sQ97_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1345])).
% 15.01/2.51 fof(f1348,plain,(
% 15.01/2.51 sQ96_spl|sQ97_spl|~sQ24_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1341,f1342,f1345,f369])).
% 15.01/2.51 fof(f1355,plain,(
% 15.01/2.51 greater(low,high)|~sQ97_spl|~sQ34_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f1346,f483])).
% 15.01/2.51 fof(f1370,plain,(
% 15.01/2.51 $false|~sQ24_spl|~sQ97_spl|~sQ34_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f1355,f962])).
% 15.01/2.51 fof(f1371,plain,(
% 15.01/2.51 ~sQ24_spl|~sQ97_spl|~sQ34_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f1370])).
% 15.01/2.51 fof(f1394,plain,(
% 15.01/2.51 smaller_or_equal(very_low,high)|~sQ24_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f984,f25])).
% 15.01/2.51 fof(f1399,plain,(
% 15.01/2.51 ![X0]: (~has_endowment(X0)|~has_immunity(X0,sK3_skl(X0))|~greater(tau,eta)|robust_position(X0)|positional_advantage(X0,sK2_skl(X0)))),
% 15.01/2.51 inference(resolution,[status(thm)],[f307,f79])).
% 15.01/2.51 fof(f1407,definition,(
% 15.01/2.51 sQ98_spl <=> (has_immunity(sK4_skl,sK8_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1408,plain,(
% 15.01/2.51 has_immunity(sK4_skl,sK8_skl)|~sQ98_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1407])).
% 15.01/2.51 fof(f1411,definition,(
% 15.01/2.51 ![X0]: (sQ99_spl <=> (~has_endowment(X0)|~has_immunity(X0,sK3_skl(X0))|robust_position(X0)|positional_advantage(X0,sK2_skl(X0))))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1414,plain,(
% 15.01/2.51 sQ99_spl|~sQ64_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1399,f1411,f766])).
% 15.01/2.51 fof(f1431,definition,(
% 15.01/2.51 sQ101_spl <=> (has_immunity(sK4_skl,sK1_skl(sK4_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1432,plain,(
% 15.01/2.51 has_immunity(sK4_skl,sK1_skl(sK4_skl))|~sQ101_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1431])).
% 15.01/2.51 fof(f1433,plain,(
% 15.01/2.51 ~has_immunity(sK4_skl,sK1_skl(sK4_skl))|sQ101_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1431])).
% 15.01/2.51 fof(f1439,plain,(
% 15.01/2.51 eta=tau|greater(eta,tau)|sQ64_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f768,f234])).
% 15.01/2.51 fof(f1442,definition,(
% 15.01/2.51 sQ103_spl <=> (eta=tau)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1443,plain,(
% 15.01/2.51 eta=tau|~sQ103_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1442])).
% 15.01/2.51 fof(f1445,definition,(
% 15.01/2.51 sQ104_spl <=> (greater(eta,tau))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1446,plain,(
% 15.01/2.51 greater(eta,tau)|~sQ104_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1445])).
% 15.01/2.51 fof(f1448,plain,(
% 15.01/2.51 sQ103_spl|sQ104_spl|sQ64_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1439,f1442,f1445,f766])).
% 15.01/2.51 fof(f1452,plain,(
% 15.01/2.51 ![X0]: (has_endowment(X0)|~organization(X0)|smaller_or_equal(age(X0,sK0_skl(X0)),tau)|~sQ103_spl)),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f1443,f418])).
% 15.01/2.51 fof(f1455,plain,(
% 15.01/2.51 greater(tau,tau)|~sQ103_spl|~sQ104_spl),
% 15.01/2.51 inference(forward_demodulation,[status(thm)],[f1443,f1446])).
% 15.01/2.51 fof(f1458,plain,(
% 15.01/2.51 ~greater(tau,tau)|~sQ103_spl|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1455,f200])).
% 15.01/2.51 fof(f1471,plain,(
% 15.01/2.51 $false|~sQ103_spl|~sQ104_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f1458,f1455])).
% 15.01/2.51 fof(f1472,plain,(
% 15.01/2.51 ~sQ103_spl|~sQ104_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f1471])).
% 15.01/2.51 fof(f1473,plain,(
% 15.01/2.51 greater(eta,zero)|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1446,f243])).
% 15.01/2.51 fof(f1483,plain,(
% 15.01/2.51 smaller(tau,eta)|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1446,f35])).
% 15.01/2.51 fof(f1484,plain,(
% 15.01/2.51 smaller(age(sK4_skl,sK0_skl(sK4_skl)),eta)|age(sK4_skl,sK0_skl(sK4_skl))=eta|~sQ18_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f313,f24])).
% 15.01/2.51 fof(f1485,definition,(
% 15.01/2.51 sQ105_spl <=> (smaller(age(sK4_skl,sK0_skl(sK4_skl)),eta))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1488,definition,(
% 15.01/2.51 sQ106_spl <=> (age(sK4_skl,sK0_skl(sK4_skl))=eta)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1489,plain,(
% 15.01/2.51 age(sK4_skl,sK0_skl(sK4_skl))=eta|~sQ106_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1488])).
% 15.01/2.51 fof(f1491,plain,(
% 15.01/2.51 sQ105_spl|sQ106_spl|~sQ18_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1484,f1485,f1488,f312])).
% 15.01/2.51 fof(f1577,plain,(
% 15.01/2.51 smaller(very_low,high)|very_low=high|~sQ24_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1394,f24])).
% 15.01/2.51 fof(f1578,definition,(
% 15.01/2.51 sQ107_spl <=> (smaller(very_low,high))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1581,plain,(
% 15.01/2.51 sQ107_spl|sQ97_spl|~sQ24_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1577,f1578,f1345,f369])).
% 15.01/2.51 fof(f1589,plain,(
% 15.01/2.51 greater_or_equal(eta,zero)|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1473,f30])).
% 15.01/2.51 fof(f1591,plain,(
% 15.01/2.51 smaller(zero,eta)|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1473,f35])).
% 15.01/2.51 fof(f1607,definition,(
% 15.01/2.51 sQ108_spl <=> (has_immunity(sK4_skl,sK0_skl(sK4_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1608,plain,(
% 15.01/2.51 has_immunity(sK4_skl,sK0_skl(sK4_skl))|~sQ108_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1607])).
% 15.01/2.51 fof(f1609,plain,(
% 15.01/2.51 ~has_immunity(sK4_skl,sK0_skl(sK4_skl))|sQ108_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1607])).
% 15.01/2.51 fof(f1617,definition,(
% 15.01/2.51 sQ109_spl <=> (greater(age(sK4_skl,sK7_skl),tau))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1626,plain,(
% 15.01/2.51 smaller_or_equal(tau,eta)|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1483,f25])).
% 15.01/2.51 fof(f1627,plain,(
% 15.01/2.51 greater(eta,zero)|eta=zero|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1589,f29])).
% 15.01/2.51 fof(f1628,definition,(
% 15.01/2.51 sQ111_spl <=> (greater(eta,zero))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1631,definition,(
% 15.01/2.51 sQ112_spl <=> (eta=zero)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1632,plain,(
% 15.01/2.51 eta=zero|~sQ112_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1631])).
% 15.01/2.51 fof(f1634,plain,(
% 15.01/2.51 sQ111_spl|sQ112_spl|~sQ104_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1627,f1628,f1631,f1445])).
% 15.01/2.51 fof(f1639,plain,(
% 15.01/2.51 tau=zero|~sQ103_spl|~sQ112_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f1443,f1632])).
% 15.01/2.51 fof(f1640,plain,(
% 15.01/2.51 sQ4_spl|~sQ103_spl|~sQ112_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1639,f134,f1442,f1631])).
% 15.01/2.51 fof(f1641,plain,(
% 15.01/2.51 greater(age(sK4_skl,sK7_skl),tau)|age(sK4_skl,sK7_skl)=tau),
% 15.01/2.51 inference(resolution,[status(thm)],[f346,f29])).
% 15.01/2.51 fof(f1642,definition,(
% 15.01/2.51 sQ113_spl <=> (age(sK4_skl,sK7_skl)=tau)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1643,plain,(
% 15.01/2.51 age(sK4_skl,sK7_skl)=tau|~sQ113_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1642])).
% 15.01/2.51 fof(f1645,plain,(
% 15.01/2.51 sQ109_spl|sQ113_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1641,f1617,f1642])).
% 15.01/2.51 fof(f1680,plain,(
% 15.01/2.51 smaller_or_equal(zero,eta)|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1591,f25])).
% 15.01/2.51 fof(f1690,plain,(
% 15.01/2.51 smaller(tau,eta)|tau=eta|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1626,f24])).
% 15.01/2.51 fof(f1691,definition,(
% 15.01/2.51 sQ114_spl <=> (smaller(tau,eta))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1692,plain,(
% 15.01/2.51 smaller(tau,eta)|~sQ114_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1691])).
% 15.01/2.51 fof(f1694,plain,(
% 15.01/2.51 sQ114_spl|sQ103_spl|~sQ104_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1690,f1691,f1442,f1445])).
% 15.01/2.51 fof(f1697,plain,(
% 15.01/2.51 smaller(zero,eta)|zero=eta|~sQ104_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1680,f24])).
% 15.01/2.51 fof(f1698,definition,(
% 15.01/2.51 sQ115_spl <=> (smaller(zero,eta))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1701,plain,(
% 15.01/2.51 sQ115_spl|sQ112_spl|~sQ104_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1697,f1698,f1631,f1445])).
% 15.01/2.51 fof(f1710,plain,(
% 15.01/2.51 has_endowment(sK4_skl)|smaller_or_equal(age(sK4_skl,sK0_skl(sK4_skl)),tau)|~sQ103_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1452,f96])).
% 15.01/2.51 fof(f1711,definition,(
% 15.01/2.51 sQ116_spl <=> (smaller_or_equal(age(sK4_skl,sK0_skl(sK4_skl)),tau))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1712,plain,(
% 15.01/2.51 smaller_or_equal(age(sK4_skl,sK0_skl(sK4_skl)),tau)|~sQ116_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1711])).
% 15.01/2.51 fof(f1714,plain,(
% 15.01/2.51 sQ17_spl|sQ116_spl|~sQ103_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1710,f309,f1711,f1442])).
% 15.01/2.51 fof(f1725,plain,(
% 15.01/2.51 smaller_or_equal(tau,age(sK4_skl,sK7_skl))),
% 15.01/2.51 inference(resolution,[status(thm)],[f348,f25])).
% 15.01/2.51 fof(f1748,plain,(
% 15.01/2.51 greater(age(sK4_skl,sK8_skl),tau)),
% 15.01/2.51 inference(resolution,[status(thm)],[f354,f106])).
% 15.01/2.51 fof(f1775,plain,(
% 15.01/2.51 ~robust_position(sK4_skl)|~smaller_or_equal(tau,tau)|~positional_advantage(sK4_skl,sK7_skl)|~sQ113_spl),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f1643,f75])).
% 15.01/2.51 fof(f1781,plain,(
% 15.01/2.51 ~sQ32_spl|~sQ63_spl|~sQ38_spl|~sQ113_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1775,f472,f762,f541,f1642])).
% 15.01/2.51 fof(f1782,plain,(
% 15.01/2.51 $false|sQ63_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f764,f118])).
% 15.01/2.51 fof(f1783,plain,(
% 15.01/2.51 sQ63_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f1782])).
% 15.01/2.51 fof(f1865,definition,(
% 15.01/2.51 sQ122_spl <=> (greater(age(sK4_skl,sK8_skl),sigma))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1922,definition,(
% 15.01/2.51 sQ127_spl <=> (is_aligned(sK4_skl,sK8_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1927,definition,(
% 15.01/2.51 sQ128_spl <=> (positional_advantage(sK4_skl,sK8_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1928,plain,(
% 15.01/2.51 positional_advantage(sK4_skl,sK8_skl)|~sQ128_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1927])).
% 15.01/2.51 fof(f1953,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ98_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1408,f55])).
% 15.01/2.51 fof(f1954,definition,(
% 15.01/2.51 sQ133_spl <=> (hazard_of_mortality(sK4_skl,sK8_skl)=very_low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f1955,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK8_skl)=very_low|~sQ133_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f1954])).
% 15.01/2.51 fof(f1958,plain,(
% 15.01/2.51 ~sQ50_spl|sQ17_spl|~sQ98_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f1953,f663,f309,f1407])).
% 15.01/2.51 fof(f2017,plain,(
% 15.01/2.51 ![X0]: (~robust_position(sK4_skl)|positional_advantage(sK4_skl,sK5_skl)|~greater(zero,X0)|~greater(X0,tau))),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f99,f540])).
% 15.01/2.51 fof(f2027,definition,(
% 15.01/2.51 ![X0]: (sQ136_spl <=> (~greater(zero,X0)|~greater(X0,tau)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2030,plain,(
% 15.01/2.51 ~sQ32_spl|sQ44_spl|sQ136_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2017,f472,f612,f2027])).
% 15.01/2.51 fof(f2041,plain,(
% 15.01/2.51 ![X0,X1]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK5_skl)|~greater(zero,X1)|~greater(X1,sigma))),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f99,f661])).
% 15.01/2.51 fof(f2051,definition,(
% 15.01/2.51 ![X1]: (sQ139_spl <=> (~greater(zero,X1)|~greater(X1,sigma)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2054,plain,(
% 15.01/2.51 ~sQ50_spl|sQ52_spl|sQ139_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2041,f663,f670,f2051])).
% 15.01/2.51 fof(f2055,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_immunity(sK4_skl,sK8_skl)|is_aligned(sK4_skl,sK8_skl)|hazard_of_mortality(sK4_skl,sK8_skl)=mod1|~sQ128_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1928,f85])).
% 15.01/2.51 fof(f2056,definition,(
% 15.01/2.51 sQ140_spl <=> (hazard_of_mortality(sK4_skl,sK8_skl)=mod1)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2057,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK8_skl)=mod1|~sQ140_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2056])).
% 15.01/2.51 fof(f2059,plain,(
% 15.01/2.51 ~sQ50_spl|sQ98_spl|sQ127_spl|sQ140_spl|~sQ128_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2055,f663,f1407,f1922,f2056,f1927])).
% 15.01/2.51 fof(f2060,plain,(
% 15.01/2.51 mod1=very_low|~sQ140_spl|~sQ133_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f2057,f1955])).
% 15.01/2.51 fof(f2061,plain,(
% 15.01/2.51 sQ88_spl|~sQ140_spl|~sQ133_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2060,f994,f2056,f1954])).
% 15.01/2.51 fof(f2066,plain,(
% 15.01/2.51 ~greater(age(sK4_skl,sK6_skl),sigma)|~sQ7_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f878,f349])).
% 15.01/2.51 fof(f2074,plain,(
% 15.01/2.51 greater_or_equal(tau,age(sK4_skl,sK6_skl))|~sQ7_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f878,f30])).
% 15.01/2.51 fof(f2085,plain,(
% 15.01/2.51 ![X0]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK7_skl)|~greater(tau,sigma))),
% 15.01/2.51 inference(resolution,[status(thm)],[f104,f661])).
% 15.01/2.51 fof(f2099,plain,(
% 15.01/2.51 ~sQ50_spl|sQ81_spl|~sQ61_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2085,f663,f934,f754])).
% 15.01/2.51 fof(f2101,plain,(
% 15.01/2.51 dissimilar(sK4_skl,sK5_skl,sK5_skl)|~sQ52_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f671,f99])).
% 15.01/2.51 fof(f2103,definition,(
% 15.01/2.51 sQ141_spl <=> (dissimilar(sK4_skl,sK5_skl,sK5_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2104,plain,(
% 15.01/2.51 dissimilar(sK4_skl,sK5_skl,sK5_skl)|~sQ141_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2103])).
% 15.01/2.51 fof(f2107,plain,(
% 15.01/2.51 $false|sQ55_spl),
% 15.01/2.51 inference(trivial_equality_resolution,[status(thm)],[f687])).
% 15.01/2.51 fof(f2108,plain,(
% 15.01/2.51 sQ55_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f2107])).
% 15.01/2.51 fof(f2110,plain,(
% 15.01/2.51 ~is_aligned(sK4_skl,sK5_skl)|~is_aligned(sK4_skl,sK5_skl)|~sQ52_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2101,f61])).
% 15.01/2.51 fof(f2113,definition,(
% 15.01/2.51 sQ142_spl <=> (age(sK4_skl,sK5_skl)=zero)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2115,plain,(
% 15.01/2.51 ~age(sK4_skl,sK5_skl)=zero|sQ142_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2113])).
% 15.01/2.51 fof(f2116,definition,(
% 15.01/2.51 sQ143_spl <=> (greater(age(sK4_skl,sK5_skl),sigma))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2117,plain,(
% 15.01/2.51 greater(age(sK4_skl,sK5_skl),sigma)|~sQ143_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2116])).
% 15.01/2.51 fof(f2120,plain,(
% 15.01/2.51 ~sQ54_spl|~sQ52_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2110,f681,f670])).
% 15.01/2.51 fof(f2122,plain,(
% 15.01/2.51 greater(zero,sigma)|~sQ143_spl),
% 15.01/2.51 inference(forward_demodulation,[status(thm)],[f99,f2117])).
% 15.01/2.51 fof(f2123,plain,(
% 15.01/2.51 $false|~sQ143_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f2122,f323])).
% 15.01/2.51 fof(f2124,plain,(
% 15.01/2.51 ~sQ143_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f2123])).
% 15.01/2.51 fof(f2125,plain,(
% 15.01/2.51 ~zero=zero|sQ142_spl),
% 15.01/2.51 inference(forward_demodulation,[status(thm)],[f99,f2115])).
% 15.01/2.51 fof(f2126,plain,(
% 15.01/2.51 $false|sQ142_spl),
% 15.01/2.51 inference(trivial_equality_resolution,[status(thm)],[f2125])).
% 15.01/2.51 fof(f2127,plain,(
% 15.01/2.51 sQ142_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f2126])).
% 15.01/2.51 fof(f2130,plain,(
% 15.01/2.51 ~is_aligned(sK4_skl,sK5_skl)|~is_aligned(sK4_skl,sK5_skl)|~sQ141_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2104,f61])).
% 15.01/2.51 fof(f2134,plain,(
% 15.01/2.51 ~sQ54_spl|~sQ141_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2130,f681,f2103])).
% 15.01/2.51 fof(f2206,plain,(
% 15.01/2.51 dissimilar(sK4_skl,sK5_skl,sK8_skl)|~sQ51_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f667,f99])).
% 15.01/2.51 fof(f2207,plain,(
% 15.01/2.51 ~zero=zero|dissimilar(sK4_skl,sK5_skl,sK8_skl)|~sQ51_spl),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f99,f667])).
% 15.01/2.51 fof(f2208,definition,(
% 15.01/2.51 sQ149_spl <=> (dissimilar(sK4_skl,sK5_skl,sK8_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2211,plain,(
% 15.01/2.51 ~sQ55_spl|sQ149_spl|~sQ51_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2207,f685,f2208,f666])).
% 15.01/2.51 fof(f2218,plain,(
% 15.01/2.51 ~age(sK4_skl,sK5_skl)=zero|greater(age(sK4_skl,sK8_skl),sigma)|~sQ51_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2206,f512])).
% 15.01/2.51 fof(f2219,plain,(
% 15.01/2.51 ~is_aligned(sK4_skl,sK5_skl)|~is_aligned(sK4_skl,sK8_skl)|~sQ51_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2206,f61])).
% 15.01/2.51 fof(f2222,plain,(
% 15.01/2.51 ~sQ142_spl|sQ122_spl|~sQ51_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2218,f2113,f1865,f666])).
% 15.01/2.51 fof(f2223,plain,(
% 15.01/2.51 ~sQ54_spl|~sQ127_spl|~sQ51_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2219,f681,f1922,f666])).
% 15.01/2.51 fof(f2239,plain,(
% 15.01/2.51 greater_or_equal(age(sK4_skl,sK8_skl),zero)),
% 15.01/2.51 inference(resolution,[status(thm)],[f1083,f106])).
% 15.01/2.51 fof(f2250,plain,(
% 15.01/2.51 greater_or_equal(age(sK4_skl,sK8_skl),tau)),
% 15.01/2.51 inference(resolution,[status(thm)],[f1084,f106])).
% 15.01/2.51 fof(f2264,plain,(
% 15.01/2.51 ![X0]: (is_aligned(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|~organization(sK4_skl)|hazard_of_mortality(sK4_skl,X0)=very_low)),
% 15.01/2.51 inference(resolution,[status(thm)],[f921,f83])).
% 15.01/2.51 fof(f2265,plain,(
% 15.01/2.51 ![X0]: (is_aligned(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|~organization(sK4_skl)|has_endowment(sK4_skl))),
% 15.01/2.51 inference(resolution,[status(thm)],[f921,f55])).
% 15.01/2.51 fof(f2266,definition,(
% 15.01/2.51 sQ153_spl <=> (hazard_of_mortality(sK4_skl,sK8_skl)=high)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2267,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK8_skl)=high|~sQ153_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2266])).
% 15.01/2.51 fof(f2270,definition,(
% 15.01/2.51 sQ154_spl <=> (hazard_of_mortality(sK4_skl,sK7_skl)=high)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2271,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK7_skl)=high|~sQ154_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2270])).
% 15.01/2.51 fof(f2274,definition,(
% 15.01/2.51 sQ155_spl <=> (hazard_of_mortality(sK4_skl,sK5_skl)=high)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2275,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK5_skl)=high|~sQ155_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2274])).
% 15.01/2.51 fof(f2278,definition,(
% 15.01/2.51 ![X0]: (sQ156_spl <=> (is_aligned(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high|hazard_of_mortality(sK4_skl,X0)=very_low))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2281,plain,(
% 15.01/2.51 sQ156_spl|~sQ50_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2264,f2278,f663])).
% 15.01/2.51 fof(f2282,definition,(
% 15.01/2.51 ![X0]: (sQ157_spl <=> (is_aligned(sK4_skl,X0)|positional_advantage(sK4_skl,X0)|hazard_of_mortality(sK4_skl,X0)=high))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2285,plain,(
% 15.01/2.51 sQ157_spl|~sQ50_spl|sQ17_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2265,f2282,f663,f309])).
% 15.01/2.51 fof(f2286,plain,(
% 15.01/2.51 high=mod2|~sQ155_spl|~sQ80_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f2275,f918])).
% 15.01/2.51 fof(f2287,plain,(
% 15.01/2.51 sQ16_spl|~sQ155_spl|~sQ80_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2286,f296,f2274,f917])).
% 15.01/2.51 fof(f2288,plain,(
% 15.01/2.51 high=low|~sQ154_spl|~sQ74_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f2271,f854])).
% 15.01/2.51 fof(f2289,plain,(
% 15.01/2.51 sQ25_spl|~sQ154_spl|~sQ74_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2288,f372,f2270,f853])).
% 15.01/2.51 fof(f2290,plain,(
% 15.01/2.51 high=mod1|~sQ153_spl|~sQ140_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f2267,f2057])).
% 15.01/2.51 fof(f2291,plain,(
% 15.01/2.51 sQ23_spl|~sQ153_spl|~sQ140_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2290,f362,f2266,f2056])).
% 15.01/2.51 fof(f2368,plain,(
% 15.01/2.51 ![X0]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK1_skl(sK4_skl))|~greater(eta,sigma)|~sQ19_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f316,f661])).
% 15.01/2.51 fof(f2369,plain,(
% 15.01/2.51 ~robust_position(sK4_skl)|positional_advantage(sK4_skl,sK1_skl(sK4_skl))|~greater(eta,tau)|~sQ19_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f316,f540])).
% 15.01/2.51 fof(f2381,definition,(
% 15.01/2.51 ![X0]: (sQ163_spl <=> (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK1_skl(sK4_skl))))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2384,definition,(
% 15.01/2.51 sQ164_spl <=> (greater(eta,sigma))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2386,plain,(
% 15.01/2.51 ~greater(eta,sigma)|sQ164_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2384])).
% 15.01/2.51 fof(f2387,plain,(
% 15.01/2.51 ~sQ50_spl|sQ163_spl|~sQ164_spl|~sQ19_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2368,f663,f2381,f2384,f315])).
% 15.01/2.51 fof(f2388,definition,(
% 15.01/2.51 sQ165_spl <=> (positional_advantage(sK4_skl,sK1_skl(sK4_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2389,plain,(
% 15.01/2.51 positional_advantage(sK4_skl,sK1_skl(sK4_skl))|~sQ165_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2388])).
% 15.01/2.51 fof(f2391,plain,(
% 15.01/2.51 ~sQ32_spl|sQ165_spl|~sQ104_spl|~sQ19_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2369,f472,f2388,f1445,f315])).
% 15.01/2.51 fof(f2405,plain,(
% 15.01/2.51 sigma=eta|greater(sigma,eta)|sQ164_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2386,f234])).
% 15.01/2.51 fof(f2408,definition,(
% 15.01/2.51 sQ166_spl <=> (sigma=eta)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2409,plain,(
% 15.01/2.51 sigma=eta|~sQ166_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2408])).
% 15.01/2.51 fof(f2411,plain,(
% 15.01/2.51 sQ166_spl|sQ84_spl|sQ164_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2405,f2408,f946,f2384])).
% 15.01/2.51 fof(f2428,plain,(
% 15.01/2.51 greater(sigma,sigma)|~sQ166_spl|~sQ84_spl),
% 15.01/2.51 inference(forward_demodulation,[status(thm)],[f2409,f947])).
% 15.01/2.51 fof(f2434,plain,(
% 15.01/2.51 ~greater(sigma,sigma)|~sQ166_spl|~sQ84_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2428,f200])).
% 15.01/2.51 fof(f2447,plain,(
% 15.01/2.51 $false|~sQ166_spl|~sQ84_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f2434,f2428])).
% 15.01/2.51 fof(f2448,plain,(
% 15.01/2.51 ~sQ166_spl|~sQ84_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f2447])).
% 15.01/2.51 fof(f2460,plain,(
% 15.01/2.51 smaller(eta,sigma)|~sQ84_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f947,f35])).
% 15.01/2.51 fof(f2484,plain,(
% 15.01/2.51 greater(eta,tau)|~sQ114_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1692,f34])).
% 15.01/2.51 fof(f2528,plain,(
% 15.01/2.51 smaller_or_equal(eta,sigma)|~sQ84_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2460,f25])).
% 15.01/2.51 fof(f2529,plain,(
% 15.01/2.51 smaller(eta,sigma)|eta=sigma|~sQ84_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2528,f24])).
% 15.01/2.51 fof(f2530,definition,(
% 15.01/2.51 sQ167_spl <=> (smaller(eta,sigma))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2533,plain,(
% 15.01/2.51 sQ167_spl|sQ166_spl|~sQ84_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2529,f2530,f2408,f946])).
% 15.01/2.51 fof(f2534,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_immunity(sK4_skl,sK1_skl(sK4_skl))|is_aligned(sK4_skl,sK1_skl(sK4_skl))|hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=mod1|~sQ165_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2389,f85])).
% 15.01/2.51 fof(f2535,definition,(
% 15.01/2.51 sQ168_spl <=> (is_aligned(sK4_skl,sK1_skl(sK4_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2536,plain,(
% 15.01/2.51 is_aligned(sK4_skl,sK1_skl(sK4_skl))|~sQ168_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2535])).
% 15.01/2.51 fof(f2538,definition,(
% 15.01/2.51 sQ169_spl <=> (hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=mod1)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2539,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=mod1|~sQ169_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2538])).
% 15.01/2.51 fof(f2541,plain,(
% 15.01/2.51 ~sQ50_spl|sQ101_spl|sQ168_spl|sQ169_spl|~sQ165_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2534,f663,f1431,f2535,f2538,f2388])).
% 15.01/2.51 fof(f2542,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_immunity(sK4_skl,sK1_skl(sK4_skl))|positional_advantage(sK4_skl,sK1_skl(sK4_skl))|hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=mod2|~sQ168_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2536,f86])).
% 15.01/2.51 fof(f2543,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_immunity(sK4_skl,sK1_skl(sK4_skl))|~positional_advantage(sK4_skl,sK1_skl(sK4_skl))|hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=low|~sQ168_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2536,f84])).
% 15.01/2.51 fof(f2544,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,X0,sK1_skl(sK4_skl))|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ168_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f2536,f63])).
% 15.01/2.51 fof(f2545,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,sK1_skl(sK4_skl),X0)|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ168_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f2536,f62])).
% 15.01/2.51 fof(f2546,definition,(
% 15.01/2.51 sQ170_spl <=> (hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=mod2)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2547,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=mod2|~sQ170_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2546])).
% 15.01/2.51 fof(f2549,plain,(
% 15.01/2.51 ~sQ50_spl|sQ101_spl|sQ165_spl|sQ170_spl|~sQ168_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2542,f663,f1431,f2388,f2546,f2535])).
% 15.01/2.51 fof(f2550,definition,(
% 15.01/2.51 sQ171_spl <=> (hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2551,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=low|~sQ171_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2550])).
% 15.01/2.51 fof(f2553,plain,(
% 15.01/2.51 ~sQ50_spl|sQ101_spl|~sQ165_spl|sQ171_spl|~sQ168_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2543,f663,f1431,f2388,f2550,f2535])).
% 15.01/2.51 fof(f2554,definition,(
% 15.01/2.51 ![X0]: (sQ172_spl <=> (dissimilar(sK4_skl,X0,sK1_skl(sK4_skl))|is_aligned(sK4_skl,X0)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2557,plain,(
% 15.01/2.51 sQ172_spl|~sQ50_spl|~sQ168_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2544,f2554,f663,f2535])).
% 15.01/2.51 fof(f2558,definition,(
% 15.01/2.51 ![X0]: (sQ173_spl <=> (dissimilar(sK4_skl,sK1_skl(sK4_skl),X0)|is_aligned(sK4_skl,X0)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2561,plain,(
% 15.01/2.51 sQ173_spl|~sQ50_spl|~sQ168_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2545,f2558,f663,f2535])).
% 15.01/2.51 fof(f2563,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ101_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1432,f55])).
% 15.01/2.51 fof(f2564,definition,(
% 15.01/2.51 sQ174_spl <=> (hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=very_low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2565,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=very_low|~sQ174_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2564])).
% 15.01/2.51 fof(f2568,plain,(
% 15.01/2.51 ~sQ50_spl|sQ17_spl|~sQ101_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2563,f663,f309,f1431])).
% 15.01/2.51 fof(f2569,plain,(
% 15.01/2.51 is_aligned(sK4_skl,sK1_skl(sK4_skl))|positional_advantage(sK4_skl,sK1_skl(sK4_skl))|hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=high|sQ101_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1433,f921])).
% 15.01/2.51 fof(f2570,definition,(
% 15.01/2.51 sQ175_spl <=> (hazard_of_mortality(sK4_skl,sK1_skl(sK4_skl))=high)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2573,plain,(
% 15.01/2.51 sQ168_spl|sQ165_spl|sQ175_spl|sQ101_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2569,f2535,f2388,f2570,f1431])).
% 15.01/2.51 fof(f2594,plain,(
% 15.01/2.51 ~robust_position(sK4_skl)|~positional_advantage(sK4_skl,sK0_skl(sK4_skl))|~sQ116_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1712,f75])).
% 15.01/2.51 fof(f2595,plain,(
% 15.01/2.51 smaller(age(sK4_skl,sK0_skl(sK4_skl)),tau)|age(sK4_skl,sK0_skl(sK4_skl))=tau|~sQ116_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1712,f24])).
% 15.01/2.51 fof(f2596,definition,(
% 15.01/2.51 sQ176_spl <=> (positional_advantage(sK4_skl,sK0_skl(sK4_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2599,plain,(
% 15.01/2.51 ~sQ32_spl|~sQ176_spl|~sQ116_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2594,f472,f2596,f1711])).
% 15.01/2.51 fof(f2600,definition,(
% 15.01/2.51 sQ177_spl <=> (smaller(age(sK4_skl,sK0_skl(sK4_skl)),tau))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2603,definition,(
% 15.01/2.51 sQ178_spl <=> (age(sK4_skl,sK0_skl(sK4_skl))=tau)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2604,plain,(
% 15.01/2.51 age(sK4_skl,sK0_skl(sK4_skl))=tau|~sQ178_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2603])).
% 15.01/2.51 fof(f2606,plain,(
% 15.01/2.51 sQ177_spl|sQ178_spl|~sQ116_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2595,f2600,f2603,f1711])).
% 15.01/2.51 fof(f2607,plain,(
% 15.01/2.51 greater(sigma,age(sK4_skl,sK7_skl))|~sQ28_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f433,f34])).
% 15.01/2.51 fof(f2686,plain,(
% 15.01/2.51 smaller(zero,age(sK4_skl,sK8_skl))),
% 15.01/2.51 inference(resolution,[status(thm)],[f1163,f106])).
% 15.01/2.51 fof(f2694,plain,(
% 15.01/2.51 smaller(tau,age(sK4_skl,sK8_skl))),
% 15.01/2.51 inference(resolution,[status(thm)],[f1164,f106])).
% 15.01/2.51 fof(f2721,plain,(
% 15.01/2.51 ~eta=zero|dissimilar(sK4_skl,sK0_skl(sK4_skl),sK8_skl)|~sQ51_spl|~sQ106_spl),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f1489,f667])).
% 15.01/2.51 fof(f2725,plain,(
% 15.01/2.51 ![X0,X1]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK0_skl(sK4_skl))|~greater(eta,X1)|~greater(X1,sigma)|~sQ106_spl)),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f1489,f661])).
% 15.01/2.51 fof(f2726,plain,(
% 15.01/2.51 ![X0]: (~robust_position(sK4_skl)|positional_advantage(sK4_skl,sK0_skl(sK4_skl))|~greater(eta,X0)|~greater(X0,tau)|~sQ106_spl)),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f1489,f540])).
% 15.01/2.51 fof(f2727,plain,(
% 15.01/2.51 ~organization(sK4_skl)|~eta=zero|is_aligned(sK4_skl,sK0_skl(sK4_skl))|~sQ106_spl),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f1489,f65])).
% 15.01/2.51 fof(f2728,plain,(
% 15.01/2.51 ![X0]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|~greater(eta,sigma)|dissimilar(sK4_skl,X0,sK0_skl(sK4_skl))|~sQ106_spl)),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f1489,f69])).
% 15.01/2.51 fof(f2729,plain,(
% 15.01/2.51 ~robust_position(sK4_skl)|~greater(eta,tau)|positional_advantage(sK4_skl,sK0_skl(sK4_skl))|~sQ106_spl),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f1489,f76])).
% 15.01/2.51 fof(f2730,plain,(
% 15.01/2.51 ~robust_position(sK4_skl)|~smaller_or_equal(eta,tau)|~positional_advantage(sK4_skl,sK0_skl(sK4_skl))|~sQ106_spl),
% 15.01/2.51 inference(paramodulation,[status(thm)],[f1489,f75])).
% 15.01/2.51 fof(f2731,definition,(
% 15.01/2.51 sQ179_spl <=> (dissimilar(sK4_skl,sK0_skl(sK4_skl),sK8_skl))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2732,plain,(
% 15.01/2.51 dissimilar(sK4_skl,sK0_skl(sK4_skl),sK8_skl)|~sQ179_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2731])).
% 15.01/2.51 fof(f2734,plain,(
% 15.01/2.51 ~sQ112_spl|sQ179_spl|~sQ51_spl|~sQ106_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2721,f1631,f2731,f666,f1488])).
% 15.01/2.51 fof(f2744,definition,(
% 15.01/2.51 ![X0]: (sQ182_spl <=> (~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK0_skl(sK4_skl))))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2747,definition,(
% 15.01/2.51 ![X1]: (sQ183_spl <=> (~greater(eta,X1)|~greater(X1,sigma)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2750,plain,(
% 15.01/2.51 ~sQ50_spl|sQ182_spl|sQ183_spl|~sQ106_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2725,f663,f2744,f2747,f1488])).
% 15.01/2.51 fof(f2751,definition,(
% 15.01/2.51 ![X0]: (sQ184_spl <=> (~greater(eta,X0)|~greater(X0,tau)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2754,plain,(
% 15.01/2.51 ~sQ32_spl|sQ176_spl|sQ184_spl|~sQ106_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2726,f472,f2596,f2751,f1488])).
% 15.01/2.51 fof(f2755,definition,(
% 15.01/2.51 sQ185_spl <=> (is_aligned(sK4_skl,sK0_skl(sK4_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2756,plain,(
% 15.01/2.51 is_aligned(sK4_skl,sK0_skl(sK4_skl))|~sQ185_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2755])).
% 15.01/2.51 fof(f2757,plain,(
% 15.01/2.51 ~is_aligned(sK4_skl,sK0_skl(sK4_skl))|sQ185_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2755])).
% 15.01/2.51 fof(f2758,plain,(
% 15.01/2.51 ~sQ50_spl|~sQ112_spl|sQ185_spl|~sQ106_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2727,f663,f1631,f2755,f1488])).
% 15.01/2.51 fof(f2759,plain,(
% 15.01/2.51 ~sQ50_spl|sQ182_spl|~sQ164_spl|~sQ106_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2728,f663,f2744,f2384,f1488])).
% 15.01/2.51 fof(f2760,plain,(
% 15.01/2.51 ~sQ32_spl|~sQ104_spl|sQ176_spl|~sQ106_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2729,f472,f1445,f2596,f1488])).
% 15.01/2.51 fof(f2761,definition,(
% 15.01/2.51 sQ186_spl <=> (smaller_or_equal(eta,tau))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2763,plain,(
% 15.01/2.51 ~smaller_or_equal(eta,tau)|sQ186_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2761])).
% 15.01/2.51 fof(f2764,plain,(
% 15.01/2.51 ~sQ32_spl|~sQ186_spl|~sQ176_spl|~sQ106_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2730,f472,f2761,f2596,f1488])).
% 15.01/2.51 fof(f2765,plain,(
% 15.01/2.51 sQ104_spl|~sQ114_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2484,f1445,f1691])).
% 15.01/2.51 fof(f2784,plain,(
% 15.01/2.51 ~smaller_or_equal(tau,tau)|~sQ103_spl|sQ186_spl),
% 15.01/2.51 inference(forward_demodulation,[status(thm)],[f1443,f2763])).
% 15.01/2.51 fof(f2785,plain,(
% 15.01/2.51 $false|~sQ103_spl|sQ186_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f2784,f118])).
% 15.01/2.51 fof(f2786,plain,(
% 15.01/2.51 ~sQ103_spl|sQ186_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f2785])).
% 15.01/2.51 fof(f2811,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_immunity(sK4_skl,sK0_skl(sK4_skl))|positional_advantage(sK4_skl,sK0_skl(sK4_skl))|hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=mod2|~sQ185_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2756,f86])).
% 15.01/2.51 fof(f2812,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_immunity(sK4_skl,sK0_skl(sK4_skl))|~positional_advantage(sK4_skl,sK0_skl(sK4_skl))|hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=low|~sQ185_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2756,f84])).
% 15.01/2.51 fof(f2813,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,X0,sK0_skl(sK4_skl))|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ185_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f2756,f63])).
% 15.01/2.51 fof(f2814,plain,(
% 15.01/2.51 ![X0]: (dissimilar(sK4_skl,sK0_skl(sK4_skl),X0)|~organization(sK4_skl)|is_aligned(sK4_skl,X0)|~sQ185_spl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f2756,f62])).
% 15.01/2.51 fof(f2815,definition,(
% 15.01/2.51 sQ187_spl <=> (hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=mod2)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2816,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=mod2|~sQ187_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2815])).
% 15.01/2.51 fof(f2818,plain,(
% 15.01/2.51 ~sQ50_spl|sQ108_spl|sQ176_spl|sQ187_spl|~sQ185_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2811,f663,f1607,f2596,f2815,f2755])).
% 15.01/2.51 fof(f2819,definition,(
% 15.01/2.51 sQ188_spl <=> (hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2820,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=low|~sQ188_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2819])).
% 15.01/2.51 fof(f2822,plain,(
% 15.01/2.51 ~sQ50_spl|sQ108_spl|~sQ176_spl|sQ188_spl|~sQ185_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2812,f663,f1607,f2596,f2819,f2755])).
% 15.01/2.51 fof(f2823,definition,(
% 15.01/2.51 ![X0]: (sQ189_spl <=> (dissimilar(sK4_skl,X0,sK0_skl(sK4_skl))|is_aligned(sK4_skl,X0)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2826,plain,(
% 15.01/2.51 sQ189_spl|~sQ50_spl|~sQ185_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2813,f2823,f663,f2755])).
% 15.01/2.51 fof(f2827,definition,(
% 15.01/2.51 ![X0]: (sQ190_spl <=> (dissimilar(sK4_skl,sK0_skl(sK4_skl),X0)|is_aligned(sK4_skl,X0)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2830,plain,(
% 15.01/2.51 sQ190_spl|~sQ50_spl|~sQ185_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2814,f2827,f663,f2755])).
% 15.01/2.51 fof(f2832,plain,(
% 15.01/2.51 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ108_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1608,f55])).
% 15.01/2.51 fof(f2833,definition,(
% 15.01/2.51 sQ191_spl <=> (hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=very_low)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2834,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=very_low|~sQ191_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2833])).
% 15.01/2.51 fof(f2837,plain,(
% 15.01/2.51 ~sQ50_spl|sQ17_spl|~sQ108_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2832,f663,f309,f1607])).
% 15.01/2.51 fof(f2838,plain,(
% 15.01/2.51 is_aligned(sK4_skl,sK0_skl(sK4_skl))|positional_advantage(sK4_skl,sK0_skl(sK4_skl))|hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=high|sQ108_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f1609,f921])).
% 15.01/2.51 fof(f2839,definition,(
% 15.01/2.51 sQ192_spl <=> (hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=high)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2840,plain,(
% 15.01/2.51 hazard_of_mortality(sK4_skl,sK0_skl(sK4_skl))=high|~sQ192_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f2839])).
% 15.01/2.51 fof(f2842,plain,(
% 15.01/2.51 sQ185_spl|sQ176_spl|sQ192_spl|sQ108_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2838,f2755,f2596,f2839,f1607])).
% 15.01/2.51 fof(f2949,plain,(
% 15.01/2.51 smaller(tau,age(sK4_skl,sK7_skl))|tau=age(sK4_skl,sK7_skl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f1725,f24])).
% 15.01/2.51 fof(f2950,definition,(
% 15.01/2.51 sQ197_spl <=> (smaller(tau,age(sK4_skl,sK7_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f2953,plain,(
% 15.01/2.51 sQ197_spl|sQ113_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2949,f2950,f1642])).
% 15.01/2.51 fof(f2955,plain,(
% 15.01/2.51 ~robust_position(sK4_skl)|positional_advantage(sK4_skl,sK8_skl)),
% 15.01/2.51 inference(resolution,[status(thm)],[f1748,f76])).
% 15.01/2.51 fof(f2972,plain,(
% 15.01/2.51 ~sQ32_spl|sQ128_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f2955,f472,f1927])).
% 15.01/2.51 fof(f3108,plain,(
% 15.01/2.51 greater(tau,age(sK4_skl,sK6_skl))|tau=age(sK4_skl,sK6_skl)|~sQ7_spl),
% 15.01/2.51 inference(resolution,[status(thm)],[f2074,f29])).
% 15.01/2.51 fof(f3109,definition,(
% 15.01/2.51 sQ202_spl <=> (greater(tau,age(sK4_skl,sK6_skl)))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f3110,plain,(
% 15.01/2.51 greater(tau,age(sK4_skl,sK6_skl))|~sQ202_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f3109])).
% 15.01/2.51 fof(f3112,plain,(
% 15.01/2.51 sQ202_spl|sQ8_spl|~sQ7_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f3108,f3109,f215,f212])).
% 15.01/2.51 fof(f3147,plain,(
% 15.01/2.51 greater(age(sK4_skl,sK8_skl),zero)|age(sK4_skl,sK8_skl)=zero),
% 15.01/2.51 inference(resolution,[status(thm)],[f2239,f29])).
% 15.01/2.51 fof(f3148,definition,(
% 15.01/2.51 sQ203_spl <=> (greater(age(sK4_skl,sK8_skl),zero))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f3151,definition,(
% 15.01/2.51 sQ204_spl <=> (age(sK4_skl,sK8_skl)=zero)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f3152,plain,(
% 15.01/2.51 age(sK4_skl,sK8_skl)=zero|~sQ204_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f3151])).
% 15.01/2.51 fof(f3154,plain,(
% 15.01/2.51 sQ203_spl|sQ204_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f3147,f3148,f3151])).
% 15.01/2.51 fof(f3157,plain,(
% 15.01/2.51 greater(zero,tau)|~sQ204_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f3152,f1748])).
% 15.01/2.51 fof(f3176,plain,(
% 15.01/2.51 $false|~sQ204_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f3157,f138])).
% 15.01/2.51 fof(f3177,plain,(
% 15.01/2.51 ~sQ204_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f3176])).
% 15.01/2.51 fof(f3178,plain,(
% 15.01/2.51 greater(age(sK4_skl,sK8_skl),tau)|age(sK4_skl,sK8_skl)=tau),
% 15.01/2.51 inference(resolution,[status(thm)],[f2250,f29])).
% 15.01/2.51 fof(f3179,definition,(
% 15.01/2.51 sQ205_spl <=> (greater(age(sK4_skl,sK8_skl),tau))),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f3182,definition,(
% 15.01/2.51 sQ206_spl <=> (age(sK4_skl,sK8_skl)=tau)),
% 15.01/2.51 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 15.01/2.51 fof(f3183,plain,(
% 15.01/2.51 age(sK4_skl,sK8_skl)=tau|~sQ206_spl),
% 15.01/2.51 inference(component_clause,[status(thm)],[f3182])).
% 15.01/2.51 fof(f3185,plain,(
% 15.01/2.51 sQ205_spl|sQ206_spl),
% 15.01/2.51 inference(split_clause,[status(thm)],[f3178,f3179,f3182])).
% 15.01/2.51 fof(f3210,plain,(
% 15.01/2.51 greater(tau,sigma)|~sQ206_spl),
% 15.01/2.51 inference(backward_demodulation,[status(thm)],[f3183,f106])).
% 15.01/2.51 fof(f3223,plain,(
% 15.01/2.51 $false|~sQ206_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f3210,f139])).
% 15.01/2.51 fof(f3224,plain,(
% 15.01/2.51 ~sQ206_spl),
% 15.01/2.51 inference(contradiction_clause,[status(thm)],[f3223])).
% 15.01/2.51 fof(f3261,plain,(
% 15.01/2.51 mod1=low|~sQ169_spl|~sQ171_spl),
% 15.01/2.51 inference(forward_demodulation,[status(thm)],[f2539,f2551])).
% 15.01/2.51 fof(f3262,plain,(
% 15.01/2.51 $false|sQ42_spl|~sQ169_spl|~sQ171_spl),
% 15.01/2.51 inference(forward_subsumption_resolution,[status(thm)],[f3261,f599])).
% 15.01/2.51 fof(f3263,plain,(
% 15.01/2.52 sQ42_spl|~sQ169_spl|~sQ171_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3262])).
% 15.01/2.52 fof(f3272,plain,(
% 15.01/2.52 mod2=very_low|~sQ170_spl|~sQ174_spl),
% 15.01/2.52 inference(forward_demodulation,[status(thm)],[f2547,f2565])).
% 15.01/2.52 fof(f3273,plain,(
% 15.01/2.52 $false|sQ14_spl|~sQ170_spl|~sQ174_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f3272,f287])).
% 15.01/2.52 fof(f3274,plain,(
% 15.01/2.52 sQ14_spl|~sQ170_spl|~sQ174_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3273])).
% 15.01/2.52 fof(f3281,plain,(
% 15.01/2.52 ![X0,X1]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK0_skl(sK4_skl))|~greater(tau,X1)|~greater(X1,sigma)|~sQ178_spl)),
% 15.01/2.52 inference(paramodulation,[status(thm)],[f2604,f661])).
% 15.01/2.52 fof(f3282,plain,(
% 15.01/2.52 ![X0]: (~robust_position(sK4_skl)|positional_advantage(sK4_skl,sK0_skl(sK4_skl))|~greater(tau,X0)|~greater(X0,tau)|~sQ178_spl)),
% 15.01/2.52 inference(paramodulation,[status(thm)],[f2604,f540])).
% 15.01/2.52 fof(f3284,plain,(
% 15.01/2.52 ![X0]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|~greater(tau,sigma)|dissimilar(sK4_skl,X0,sK0_skl(sK4_skl))|~sQ178_spl)),
% 15.01/2.52 inference(paramodulation,[status(thm)],[f2604,f69])).
% 15.01/2.52 fof(f3285,plain,(
% 15.01/2.52 ~robust_position(sK4_skl)|~greater(tau,tau)|positional_advantage(sK4_skl,sK0_skl(sK4_skl))|~sQ178_spl),
% 15.01/2.52 inference(paramodulation,[status(thm)],[f2604,f76])).
% 15.01/2.52 fof(f3286,plain,(
% 15.01/2.52 ~robust_position(sK4_skl)|~smaller_or_equal(tau,tau)|~positional_advantage(sK4_skl,sK0_skl(sK4_skl))|~sQ178_spl),
% 15.01/2.52 inference(paramodulation,[status(thm)],[f2604,f75])).
% 15.01/2.52 fof(f3288,definition,(
% 15.01/2.52 ![X0]: (sQ207_spl <=> (~greater(tau,X0)|~greater(X0,tau)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3294,definition,(
% 15.01/2.52 ![X1]: (sQ208_spl <=> (~greater(tau,X1)|~greater(X1,sigma)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3297,plain,(
% 15.01/2.52 ~sQ50_spl|sQ182_spl|sQ208_spl|~sQ178_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3281,f663,f2744,f3294,f2603])).
% 15.01/2.52 fof(f3298,plain,(
% 15.01/2.52 ~sQ32_spl|sQ176_spl|sQ207_spl|~sQ178_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3282,f472,f2596,f3288,f2603])).
% 15.01/2.52 fof(f3300,plain,(
% 15.01/2.52 ~sQ50_spl|sQ182_spl|~sQ61_spl|~sQ178_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3284,f663,f2744,f754,f2603])).
% 15.01/2.52 fof(f3301,plain,(
% 15.01/2.52 ~sQ32_spl|~sQ62_spl|sQ176_spl|~sQ178_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3285,f472,f758,f2596,f2603])).
% 15.01/2.52 fof(f3302,plain,(
% 15.01/2.52 ~sQ32_spl|~sQ63_spl|~sQ176_spl|~sQ178_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3286,f472,f762,f2596,f2603])).
% 15.01/2.52 fof(f3327,plain,(
% 15.01/2.52 smaller_or_equal(zero,age(sK4_skl,sK8_skl))),
% 15.01/2.52 inference(resolution,[status(thm)],[f2686,f25])).
% 15.01/2.52 fof(f3329,plain,(
% 15.01/2.52 smaller_or_equal(tau,age(sK4_skl,sK8_skl))),
% 15.01/2.52 inference(resolution,[status(thm)],[f2694,f25])).
% 15.01/2.52 fof(f3337,plain,(
% 15.01/2.52 is_aligned(sK4_skl,sK0_skl(sK4_skl))|is_aligned(sK4_skl,sK8_skl)|~sQ179_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f2732,f60])).
% 15.01/2.52 fof(f3344,plain,(
% 15.01/2.52 sQ185_spl|sQ127_spl|~sQ179_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3337,f2755,f1922,f2731])).
% 15.01/2.52 fof(f3345,plain,(
% 15.01/2.52 mod2=low|~sQ187_spl|~sQ188_spl),
% 15.01/2.52 inference(backward_demodulation,[status(thm)],[f2816,f2820])).
% 15.01/2.52 fof(f3346,plain,(
% 15.01/2.52 $false|~sQ80_spl|sQ69_spl|~sQ187_spl|~sQ188_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f3345,f1308])).
% 15.01/2.52 fof(f3347,plain,(
% 15.01/2.52 ~sQ80_spl|sQ69_spl|~sQ187_spl|~sQ188_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3346])).
% 15.01/2.52 fof(f3348,plain,(
% 15.01/2.52 high=very_low|~sQ192_spl|~sQ191_spl),
% 15.01/2.52 inference(backward_demodulation,[status(thm)],[f2840,f2834])).
% 15.01/2.52 fof(f3349,plain,(
% 15.01/2.52 sQ97_spl|~sQ192_spl|~sQ191_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3348,f1345,f2839,f2833])).
% 15.01/2.52 fof(f3471,plain,(
% 15.01/2.52 smaller(zero,age(sK4_skl,sK8_skl))|zero=age(sK4_skl,sK8_skl)),
% 15.01/2.52 inference(resolution,[status(thm)],[f3327,f24])).
% 15.01/2.52 fof(f3472,definition,(
% 15.01/2.52 sQ214_spl <=> (smaller(zero,age(sK4_skl,sK8_skl)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3475,plain,(
% 15.01/2.52 sQ214_spl|sQ204_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3471,f3472,f3151])).
% 15.01/2.52 fof(f3476,plain,(
% 15.01/2.52 smaller(tau,age(sK4_skl,sK8_skl))|tau=age(sK4_skl,sK8_skl)),
% 15.01/2.52 inference(resolution,[status(thm)],[f3329,f24])).
% 15.01/2.52 fof(f3477,definition,(
% 15.01/2.52 sQ215_spl <=> (smaller(tau,age(sK4_skl,sK8_skl)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3480,plain,(
% 15.01/2.52 sQ215_spl|sQ206_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3476,f3477,f3182])).
% 15.01/2.52 fof(f3482,plain,(
% 15.01/2.52 ![X0]: (is_aligned(sK4_skl,X0)|~age(sK4_skl,X0)=zero|greater(age(sK4_skl,sK5_skl),sigma)|~sQ57_spl)),
% 15.01/2.52 inference(resolution,[status(thm)],[f733,f512])).
% 15.01/2.52 fof(f3483,plain,(
% 15.01/2.52 ![X0]: (is_aligned(sK4_skl,X0)|~is_aligned(sK4_skl,X0)|~is_aligned(sK4_skl,sK5_skl)|~sQ57_spl)),
% 15.01/2.52 inference(resolution,[status(thm)],[f733,f61])).
% 15.01/2.52 fof(f3486,definition,(
% 15.01/2.52 ![X0]: (sQ216_spl <=> (is_aligned(sK4_skl,X0)|~age(sK4_skl,X0)=zero))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3489,plain,(
% 15.01/2.52 sQ216_spl|sQ143_spl|~sQ57_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3482,f3486,f2116,f732])).
% 15.01/2.52 fof(f3490,definition,(
% 15.01/2.52 ![X0]: (sQ217_spl <=> (is_aligned(sK4_skl,X0)|~is_aligned(sK4_skl,X0)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3493,plain,(
% 15.01/2.52 sQ217_spl|~sQ54_spl|~sQ57_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3483,f3490,f681,f732])).
% 15.01/2.52 fof(f3498,definition,(
% 15.01/2.52 ![X0]: (sQ219_spl <=> (is_aligned(sK4_skl,X0)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3499,plain,(
% 15.01/2.52 ![X0]: (is_aligned(sK4_skl,X0)|~sQ219_spl)),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3498])).
% 15.01/2.52 fof(f3503,plain,(
% 15.01/2.52 $false|~sQ219_spl|sQ185_spl),
% 15.01/2.52 inference(backward_subsumption_resolution,[status(thm)],[f2757,f3499])).
% 15.01/2.52 fof(f3511,plain,(
% 15.01/2.52 ~sQ219_spl|sQ185_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3503])).
% 15.01/2.52 fof(f3512,plain,(
% 15.01/2.52 mod2=low|~sQ80_spl|~sQ69_spl),
% 15.01/2.52 inference(forward_demodulation,[status(thm)],[f918,f829])).
% 15.01/2.52 fof(f3548,plain,(
% 15.01/2.52 ~greater(mod2,mod1)|~sQ80_spl|~sQ69_spl),
% 15.01/2.52 inference(backward_demodulation,[status(thm)],[f3512,f149])).
% 15.01/2.52 fof(f3555,plain,(
% 15.01/2.52 $false|~sQ80_spl|~sQ69_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f3548,f531])).
% 15.01/2.52 fof(f3556,plain,(
% 15.01/2.52 ~sQ80_spl|~sQ69_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3555])).
% 15.01/2.52 fof(f3688,definition,(
% 15.01/2.52 sQ223_spl <=> (has_immunity(sK4_skl,sK2_skl(sK4_skl)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3689,plain,(
% 15.01/2.52 has_immunity(sK4_skl,sK2_skl(sK4_skl))|~sQ223_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3688])).
% 15.01/2.52 fof(f3706,definition,(
% 15.01/2.52 sQ227_spl <=> (has_immunity(sK4_skl,sK3_skl(sK4_skl)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3707,plain,(
% 15.01/2.52 has_immunity(sK4_skl,sK3_skl(sK4_skl))|~sQ227_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3706])).
% 15.01/2.52 fof(f3734,plain,(
% 15.01/2.52 ![X0]: (is_aligned(sK4_skl,X0)|~age(sK4_skl,sK5_skl)=zero|greater(age(sK4_skl,X0),sigma)|~sQ58_spl)),
% 15.01/2.52 inference(resolution,[status(thm)],[f737,f512])).
% 15.01/2.52 fof(f3738,definition,(
% 15.01/2.52 ![X0]: (sQ233_spl <=> (is_aligned(sK4_skl,X0)|greater(age(sK4_skl,X0),sigma)))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3741,plain,(
% 15.01/2.52 sQ233_spl|~sQ142_spl|~sQ58_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3734,f3738,f2113,f736])).
% 15.01/2.52 fof(f3787,plain,(
% 15.01/2.52 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ223_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3689,f55])).
% 15.01/2.52 fof(f3792,plain,(
% 15.01/2.52 ~sQ50_spl|sQ17_spl|~sQ223_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3787,f663,f309,f3688])).
% 15.01/2.52 fof(f3795,plain,(
% 15.01/2.52 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ227_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3707,f55])).
% 15.01/2.52 fof(f3801,plain,(
% 15.01/2.52 ~sQ50_spl|sQ17_spl|~sQ227_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3795,f663,f309,f3706])).
% 15.01/2.52 fof(f3820,definition,(
% 15.01/2.52 sQ242_spl <=> (dissimilar(sK4_skl,sK5_skl,sK6_skl))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3821,plain,(
% 15.01/2.52 dissimilar(sK4_skl,sK5_skl,sK6_skl)|~sQ242_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3820])).
% 15.01/2.52 fof(f3822,plain,(
% 15.01/2.52 ~dissimilar(sK4_skl,sK5_skl,sK6_skl)|sQ242_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3820])).
% 15.01/2.52 fof(f3835,plain,(
% 15.01/2.52 ~age(sK4_skl,sK5_skl)=zero|greater(age(sK4_skl,sK6_skl),sigma)|~sQ242_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3821,f512])).
% 15.01/2.52 fof(f3836,plain,(
% 15.01/2.52 ~is_aligned(sK4_skl,sK5_skl)|~is_aligned(sK4_skl,sK6_skl)|~sQ242_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3821,f61])).
% 15.01/2.52 fof(f3839,definition,(
% 15.01/2.52 sQ244_spl <=> (greater(age(sK4_skl,sK6_skl),sigma))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3840,plain,(
% 15.01/2.52 greater(age(sK4_skl,sK6_skl),sigma)|~sQ244_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3839])).
% 15.01/2.52 fof(f3842,plain,(
% 15.01/2.52 ~sQ142_spl|sQ244_spl|~sQ242_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3835,f2113,f3839,f3820])).
% 15.01/2.52 fof(f3843,plain,(
% 15.01/2.52 ~sQ54_spl|~sQ59_spl|~sQ242_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3836,f681,f747,f3820])).
% 15.01/2.52 fof(f3845,plain,(
% 15.01/2.52 $false|~sQ7_spl|~sQ244_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f3840,f2066])).
% 15.01/2.52 fof(f3846,plain,(
% 15.01/2.52 ~sQ7_spl|~sQ244_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3845])).
% 15.01/2.52 fof(f3847,plain,(
% 15.01/2.52 is_aligned(sK4_skl,sK6_skl)|sQ242_spl|~sQ58_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3822,f737])).
% 15.01/2.52 fof(f3849,plain,(
% 15.01/2.52 ~organization(sK4_skl)|has_immunity(sK4_skl,sK6_skl)|positional_advantage(sK4_skl,sK6_skl)|hazard_of_mortality(sK4_skl,sK6_skl)=mod2|sQ242_spl|~sQ58_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3847,f86])).
% 15.01/2.52 fof(f3856,definition,(
% 15.01/2.52 sQ246_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=mod2)),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3857,plain,(
% 15.01/2.52 hazard_of_mortality(sK4_skl,sK6_skl)=mod2|~sQ246_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3856])).
% 15.01/2.52 fof(f3859,plain,(
% 15.01/2.52 ~sQ50_spl|sQ65_spl|sQ33_spl|sQ246_spl|sQ242_spl|~sQ58_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3849,f663,f769,f475,f3856,f3820,f736])).
% 15.01/2.52 fof(f3862,plain,(
% 15.01/2.52 $false|~sQ80_spl|sQ2_spl|~sQ246_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f3857,f1305])).
% 15.01/2.52 fof(f3863,plain,(
% 15.01/2.52 ~sQ80_spl|sQ2_spl|~sQ246_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3862])).
% 15.01/2.52 fof(f3866,plain,(
% 15.01/2.52 hazard_of_mortality(sK4_skl,sK6_skl)=mod2|~sQ80_spl|~sQ2_spl),
% 15.01/2.52 inference(forward_demodulation,[status(thm)],[f918,f115])).
% 15.01/2.52 fof(f3868,plain,(
% 15.01/2.52 ~organization(sK4_skl)|has_endowment(sK4_skl)|~sQ65_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f770,f55])).
% 15.01/2.52 fof(f3869,definition,(
% 15.01/2.52 sQ247_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=very_low)),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3870,plain,(
% 15.01/2.52 hazard_of_mortality(sK4_skl,sK6_skl)=very_low|~sQ247_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3869])).
% 15.01/2.52 fof(f3873,plain,(
% 15.01/2.52 ~sQ50_spl|sQ17_spl|~sQ65_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3868,f663,f309,f769])).
% 15.01/2.52 fof(f3876,definition,(
% 15.01/2.52 sQ248_spl <=> (greater(mod1,mod1))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3877,plain,(
% 15.01/2.52 greater(mod1,mod1)|~sQ248_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3876])).
% 15.01/2.52 fof(f3878,plain,(
% 15.01/2.52 ~greater(mod1,mod1)|sQ248_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3876])).
% 15.01/2.52 fof(f3880,plain,(
% 15.01/2.52 ~smaller(mod1,hazard_of_mortality(sK4_skl,sK6_skl))|~sQ140_spl|sQ1_spl),
% 15.01/2.52 inference(forward_demodulation,[status(thm)],[f2057,f113])).
% 15.01/2.52 fof(f3881,plain,(
% 15.01/2.52 is_aligned(sK4_skl,sK6_skl)|positional_advantage(sK4_skl,sK6_skl)|hazard_of_mortality(sK4_skl,sK6_skl)=high|sQ65_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f771,f921])).
% 15.01/2.52 fof(f3882,definition,(
% 15.01/2.52 sQ249_spl <=> (hazard_of_mortality(sK4_skl,sK6_skl)=high)),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f3883,plain,(
% 15.01/2.52 hazard_of_mortality(sK4_skl,sK6_skl)=high|~sQ249_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f3882])).
% 15.01/2.52 fof(f3885,plain,(
% 15.01/2.52 sQ59_spl|sQ33_spl|sQ249_spl|sQ65_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3881,f747,f475,f3882,f769])).
% 15.01/2.52 fof(f3893,plain,(
% 15.01/2.52 ~greater(mod1,mod1)|~sQ248_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3877,f200])).
% 15.01/2.52 fof(f3906,plain,(
% 15.01/2.52 $false|~sQ248_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f3893,f3877])).
% 15.01/2.52 fof(f3907,plain,(
% 15.01/2.52 ~sQ248_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3906])).
% 15.01/2.52 fof(f3909,plain,(
% 15.01/2.52 mod1=mod1|greater(mod1,mod1)|sQ248_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3878,f234])).
% 15.01/2.52 fof(f3913,plain,(
% 15.01/2.52 sQ94_spl|sQ248_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3909,f1282,f3876])).
% 15.01/2.52 fof(f3951,plain,(
% 15.01/2.52 high=very_low|~sQ249_spl|~sQ247_spl),
% 15.01/2.52 inference(backward_demodulation,[status(thm)],[f3883,f3870])).
% 15.01/2.52 fof(f3952,plain,(
% 15.01/2.52 sQ97_spl|~sQ249_spl|~sQ247_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f3951,f1345,f3882,f3869])).
% 15.01/2.52 fof(f3955,plain,(
% 15.01/2.52 ~smaller(mod1,high)|~sQ249_spl|~sQ140_spl|sQ1_spl),
% 15.01/2.52 inference(forward_demodulation,[status(thm)],[f3883,f3880])).
% 15.01/2.52 fof(f3956,plain,(
% 15.01/2.52 $false|~sQ22_spl|~sQ249_spl|~sQ140_spl|sQ1_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f3955,f360])).
% 15.01/2.52 fof(f3957,plain,(
% 15.01/2.52 ~sQ22_spl|~sQ249_spl|~sQ140_spl|sQ1_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f3956])).
% 15.01/2.52 fof(f4021,plain,(
% 15.01/2.52 ~zero=zero|dissimilar(sK4_skl,sK5_skl,sK7_skl)|~sQ81_spl),
% 15.01/2.52 inference(paramodulation,[status(thm)],[f99,f935])).
% 15.01/2.52 fof(f4026,definition,(
% 15.01/2.52 sQ254_spl <=> (dissimilar(sK4_skl,sK5_skl,sK7_skl))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f4027,plain,(
% 15.01/2.52 dissimilar(sK4_skl,sK5_skl,sK7_skl)|~sQ254_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f4026])).
% 15.01/2.52 fof(f4028,plain,(
% 15.01/2.52 ~dissimilar(sK4_skl,sK5_skl,sK7_skl)|sQ254_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f4026])).
% 15.01/2.52 fof(f4029,plain,(
% 15.01/2.52 ~sQ55_spl|sQ254_spl|~sQ81_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f4021,f685,f4026,f934])).
% 15.01/2.52 fof(f4030,plain,(
% 15.01/2.52 ~age(sK4_skl,sK5_skl)=zero|greater(age(sK4_skl,sK7_skl),sigma)|~sQ254_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f4027,f512])).
% 15.01/2.52 fof(f4034,definition,(
% 15.01/2.52 sQ255_spl <=> (greater(age(sK4_skl,sK7_skl),sigma))),
% 15.01/2.52 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 15.01/2.52 fof(f4035,plain,(
% 15.01/2.52 greater(age(sK4_skl,sK7_skl),sigma)|~sQ255_spl),
% 15.01/2.52 inference(component_clause,[status(thm)],[f4034])).
% 15.01/2.52 fof(f4037,plain,(
% 15.01/2.52 ~sQ142_spl|sQ255_spl|~sQ254_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f4030,f2113,f4034,f4026])).
% 15.01/2.52 fof(f4040,plain,(
% 15.01/2.52 is_aligned(sK4_skl,sK7_skl)|sQ254_spl|~sQ58_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f4028,f737])).
% 15.01/2.52 fof(f4041,plain,(
% 15.01/2.52 sQ71_spl|sQ254_spl|~sQ58_spl),
% 15.01/2.52 inference(split_clause,[status(thm)],[f4040,f836,f4026,f736])).
% 15.01/2.52 fof(f4042,plain,(
% 15.01/2.52 ~smaller(hazard_of_mortality(sK4_skl,sK7_skl),mod1)|~sQ140_spl|sQ0_spl),
% 15.01/2.52 inference(forward_demodulation,[status(thm)],[f2057,f110])).
% 15.01/2.52 fof(f4060,plain,(
% 15.01/2.52 smaller(zero,age(sK4_skl,sK7_skl))),
% 15.01/2.52 inference(resolution,[status(thm)],[f104,f1162])).
% 15.01/2.52 fof(f4061,plain,(
% 15.01/2.52 greater_or_equal(age(sK4_skl,sK7_skl),zero)),
% 15.01/2.52 inference(resolution,[status(thm)],[f104,f1082])).
% 15.01/2.52 fof(f4195,plain,(
% 15.01/2.52 ~smaller(low,mod1)|~sQ74_spl|~sQ140_spl|sQ0_spl),
% 15.01/2.52 inference(forward_demodulation,[status(thm)],[f854,f4042])).
% 15.01/2.52 fof(f4196,plain,(
% 15.01/2.52 $false|~sQ41_spl|~sQ74_spl|~sQ140_spl|sQ0_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f4195,f595])).
% 15.01/2.52 fof(f4197,plain,(
% 15.01/2.52 ~sQ41_spl|~sQ74_spl|~sQ140_spl|sQ0_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f4196])).
% 15.01/2.52 fof(f4270,plain,(
% 15.01/2.52 ~greater(age(sK4_skl,sK6_skl),sigma)|~sQ202_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f3110,f349])).
% 15.01/2.52 fof(f4337,plain,(
% 15.01/2.52 greater(sigma,sigma)|~sQ29_spl|~sQ255_spl),
% 15.01/2.52 inference(forward_demodulation,[status(thm)],[f436,f4035])).
% 15.01/2.52 fof(f4345,plain,(
% 15.01/2.52 ~greater(sigma,sigma)|~sQ29_spl|~sQ255_spl),
% 15.01/2.52 inference(resolution,[status(thm)],[f4337,f200])).
% 15.01/2.52 fof(f4358,plain,(
% 15.01/2.52 $false|~sQ29_spl|~sQ255_spl),
% 15.01/2.52 inference(forward_subsumption_resolution,[status(thm)],[f4345,f4337])).
% 15.01/2.52 fof(f4359,plain,(
% 15.01/2.52 ~sQ29_spl|~sQ255_spl),
% 15.01/2.52 inference(contradiction_clause,[status(thm)],[f4358])).
% 15.01/2.52 fof(f4368,plain,(
% 15.01/2.52 smaller_or_equal(zero,age(sK4_skl,sK7_skl))),
% 15.01/2.53 inference(resolution,[status(thm)],[f4060,f25])).
% 15.01/2.53 fof(f4369,plain,(
% 15.01/2.53 greater(age(sK4_skl,sK7_skl),zero)|age(sK4_skl,sK7_skl)=zero),
% 15.01/2.53 inference(resolution,[status(thm)],[f4061,f29])).
% 15.01/2.53 fof(f4370,definition,(
% 15.01/2.53 sQ259_spl <=> (greater(age(sK4_skl,sK7_skl),zero))),
% 15.01/2.53 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 15.01/2.53 fof(f4373,definition,(
% 15.01/2.53 sQ260_spl <=> (age(sK4_skl,sK7_skl)=zero)),
% 15.01/2.53 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 15.01/2.53 fof(f4374,plain,(
% 15.01/2.53 age(sK4_skl,sK7_skl)=zero|~sQ260_spl),
% 15.01/2.53 inference(component_clause,[status(thm)],[f4373])).
% 15.01/2.53 fof(f4376,plain,(
% 15.01/2.53 sQ259_spl|sQ260_spl),
% 15.01/2.53 inference(split_clause,[status(thm)],[f4369,f4370,f4373])).
% 15.01/2.53 fof(f4392,plain,(
% 15.01/2.53 ~robust_position(sK4_skl)|~smaller_or_equal(zero,tau)|~positional_advantage(sK4_skl,sK7_skl)|~sQ260_spl),
% 15.01/2.53 inference(paramodulation,[status(thm)],[f4374,f75])).
% 15.01/2.53 fof(f4403,plain,(
% 15.01/2.53 ~sQ32_spl|~sQ45_spl|~sQ38_spl|~sQ260_spl),
% 15.01/2.53 inference(split_clause,[status(thm)],[f4392,f472,f616,f541,f4373])).
% 15.01/2.53 fof(f4456,plain,(
% 15.01/2.53 ![X0]: (~organization(sK4_skl)|~age(sK4_skl,X0)=zero|dissimilar(sK4_skl,X0,sK7_skl)|~sQ255_spl)),
% 15.01/2.53 inference(resolution,[status(thm)],[f4035,f69])).
% 15.01/2.53 fof(f4476,plain,(
% 15.01/2.53 ~sQ50_spl|sQ81_spl|~sQ255_spl),
% 15.01/2.53 inference(split_clause,[status(thm)],[f4456,f663,f934,f4034])).
% 15.01/2.53 fof(f4516,plain,(
% 15.01/2.53 ~greater(age(sK4_skl,sK7_skl),sigma)|~sQ28_spl),
% 15.01/2.53 inference(resolution,[status(thm)],[f2607,f37])).
% 15.01/2.53 fof(f4518,plain,(
% 15.01/2.53 $false|~sQ255_spl|~sQ28_spl),
% 15.01/2.53 inference(forward_subsumption_resolution,[status(thm)],[f4516,f4035])).
% 15.01/2.53 fof(f4519,plain,(
% 15.01/2.53 ~sQ255_spl|~sQ28_spl),
% 15.01/2.53 inference(contradiction_clause,[status(thm)],[f4518])).
% 15.01/2.53 fof(f4521,plain,(
% 15.01/2.53 ~smaller(mod1,mod2)|~sQ80_spl|~sQ2_spl|~sQ140_spl|sQ1_spl),
% 15.01/2.53 inference(forward_demodulation,[status(thm)],[f3866,f3880])).
% 15.01/2.53 fof(f4522,plain,(
% 15.01/2.53 $false|~sQ80_spl|~sQ2_spl|~sQ140_spl|sQ1_spl),
% 15.01/2.53 inference(forward_subsumption_resolution,[status(thm)],[f4521,f158])).
% 15.01/2.53 fof(f4523,plain,(
% 15.01/2.53 ~sQ80_spl|~sQ2_spl|~sQ140_spl|sQ1_spl),
% 15.01/2.53 inference(contradiction_clause,[status(thm)],[f4522])).
% 15.01/2.53 fof(f4526,plain,(
% 15.01/2.53 ~sQ244_spl|~sQ202_spl),
% 15.01/2.53 inference(split_clause,[status(thm)],[f4270,f3839,f3109])).
% 15.01/2.53 fof(f4584,plain,(
% 15.01/2.53 smaller(zero,age(sK4_skl,sK7_skl))|zero=age(sK4_skl,sK7_skl)),
% 15.01/2.53 inference(resolution,[status(thm)],[f4368,f24])).
% 15.01/2.53 fof(f4585,definition,(
% 15.01/2.53 sQ262_spl <=> (smaller(zero,age(sK4_skl,sK7_skl)))),
% 15.01/2.53 introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 15.01/2.53 fof(f4588,plain,(
% 15.01/2.53 sQ262_spl|sQ260_spl),
% 15.01/2.53 inference(split_clause,[status(thm)],[f4584,f4585,f4373])).
% 15.01/2.53 fof(f4604,plain,(
% 15.01/2.53 greater(tau,sigma)|~sQ8_spl|~sQ244_spl),
% 15.01/2.53 inference(forward_demodulation,[status(thm)],[f216,f3840])).
% 15.01/2.53 fof(f4605,plain,(
% 15.01/2.53 $false|~sQ8_spl|~sQ244_spl),
% 15.01/2.53 inference(forward_subsumption_resolution,[status(thm)],[f4604,f139])).
% 15.01/2.53 fof(f4606,plain,(
% 15.01/2.53 ~sQ8_spl|~sQ244_spl),
% 15.01/2.53 inference(contradiction_clause,[status(thm)],[f4605])).
% 15.01/2.53 fof(f4607,plain,(
% 15.01/2.53 $false),
% 15.01/2.53 inference(sat_refutation,[status(thm)],[f117,f137,f166,f179,f209,f218,f299,f320,f334,f365,f389,f394,f417,f420,f425,f438,f453,f464,f478,f480,f488,f503,f527,f544,f549,f569,f571,f600,f615,f619,f632,f652,f659,f669,f676,f678,f684,f697,f724,f735,f739,f761,f813,f849,f856,f860,f864,f871,f920,f997,f1011,f1047,f1107,f1112,f1114,f1275,f1307,f1310,f1311,f1348,f1371,f1414,f1448,f1472,f1491,f1581,f1634,f1640,f1645,f1694,f1701,f1714,f1781,f1783,f1958,f2030,f2054,f2059,f2061,f2099,f2108,f2120,f2124,f2127,f2134,f2211,f2222,f2223,f2281,f2285,f2287,f2289,f2291,f2387,f2391,f2411,f2448,f2533,f2541,f2549,f2553,f2557,f2561,f2568,f2573,f2599,f2606,f2734,f2750,f2754,f2758,f2759,f2760,f2764,f2765,f2786,f2818,f2822,f2826,f2830,f2837,f2842,f2953,f2972,f3112,f3154,f3177,f3185,f3224,f3263,f3274,f3297,f3298,f3300,f3301,f3302,f3344,f3347,f3349,f3475,f3480,f3489,f3493,f3511,f3556,f3741,f3792,f3801,f3842,f3843,f3846,f3859,f3863,f3873,f3885,f3907,f3913,f3952,f3957,f4029,f4037,f4041,f4197,f4359,f4376,f4403,f4476,f4519,f4523,f4526,f4588,f4606])).
% 15.01/2.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.50/2.54 % Elapsed time: 2.051395 seconds
% 0.50/2.54 % CPU time: 15.548661 seconds
% 0.50/2.54 % Total memory used: 173.007 MB
% 0.50/2.54 % Net memory used: 160.360 MB
%------------------------------------------------------------------------------