%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT063-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 : Unsatisfiable 65.09s 8.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT063-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n017.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 01:19:56 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 65.09/8.70 % Refutation found
% 65.09/8.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 65.09/8.70 % SZS output start CNFRefutation for theBenchmark
% 65.09/8.70 fof(f1,axiom,(
% 65.09/8.70 (![A,B]: (( ~ smaller_or_equal(A,B)| smaller(A,B)| A = B ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f2,axiom,(
% 65.09/8.70 (![A,B]: (( ~ smaller(A,B)| smaller_or_equal(A,B) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f4,axiom,(
% 65.09/8.70 (![A,B]: (( ~ greater_or_equal(A,B)| greater(A,B)| A = B ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f5,axiom,(
% 65.09/8.70 (![A,B]: (( ~ greater(A,B)| greater_or_equal(A,B) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f7,axiom,(
% 65.09/8.70 (![A,B]: (( ~ smaller(A,B)| greater(B,A) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f8,axiom,(
% 65.09/8.70 (![A,B]: (( ~ greater(A,B)| smaller(B,A) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f9,axiom,(
% 65.09/8.70 (![A,B]: (( ~ greater(A,B)| ~ greater(B,A) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f10,axiom,(
% 65.09/8.70 (![A,B,C]: (( ~ greater(A,B)| ~ greater(B,C)| greater(A,C) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f11,axiom,(
% 65.09/8.70 (![A,B]: (( smaller(A,B)| A = B| greater(A,B) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f19,axiom,(
% 65.09/8.70 (![A,B]: (( ~ organization(A)| has_endowment(A)| ~ has_immunity(A,B) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f20,axiom,(
% 65.09/8.70 (![A,B,C]: (( ~ dissimilar(A,B,C)| organization(A) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f21,axiom,(
% 65.09/8.70 (![A,B,C]: (( ~ dissimilar(A,B,C)| is_aligned(A,B)| is_aligned(A,C) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f22,axiom,(
% 65.09/8.70 (![A,B,C]: (( ~ dissimilar(A,B,C)| ~ is_aligned(A,B)| ~ is_aligned(A,C) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f24,axiom,(
% 65.09/8.70 (![A,B,C]: (( ~ organization(A)| ~ is_aligned(A,B)| is_aligned(A,C)| dissimilar(A,B,C) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f25,axiom,(
% 65.09/8.70 (![A,B,C]: (( ~ organization(A)| ~ is_aligned(A,B)| is_aligned(A,C)| dissimilar(A,C,B) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f27,axiom,(
% 65.09/8.70 (![A,B]: (( ~ organization(A)| age(A,B) != zero| is_aligned(A,B) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f28,axiom,(
% 65.09/8.70 (![A,B,C]: (( ~ organization(A)| age(A,B) != zero| ~ greater(age(A,C),sigma)| dissimilar(A,B,C) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f29,axiom,(
% 65.09/8.70 (![A,B,C]: (( ~ organization(A)| age(A,B) != zero| ~ dissimilar(A,B,C)| greater(age(A,C),sigma) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f30,axiom,(
% 65.09/8.70 (![A,B]: (( ~ robust_position(A)| ~ smaller_or_equal(age(A,B),tau)| ~ positional_advantage(A,B) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f31,axiom,(
% 65.09/8.70 (![A,B]: (( ~ robust_position(A)| ~ greater(age(A,B),tau)| positional_advantage(A,B) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f32,axiom,(
% 65.09/8.70 (![A]: (( smaller_or_equal(age(A,sk2(A)),tau)| greater(age(A,sk2(A)),tau)| robust_position(A) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f34,axiom,(
% 65.09/8.70 (![A]: (( positional_advantage(A,sk2(A))| greater(age(A,sk2(A)),tau)| robust_position(A) ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f36,axiom,(
% 65.09/8.70 (![A,B]: (( ~ organization(A)| ~ has_immunity(A,B)| hazard_of_mortality(A,B) = very_low ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f37,axiom,(
% 65.09/8.70 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| ~ is_aligned(A,B)| ~ positional_advantage(A,B)| hazard_of_mortality(A,B) = low ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f38,axiom,(
% 65.09/8.70 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| is_aligned(A,B)| ~ positional_advantage(A,B)| hazard_of_mortality(A,B) = mod1 ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f39,axiom,(
% 65.09/8.70 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| ~ is_aligned(A,B)| positional_advantage(A,B)| hazard_of_mortality(A,B) = mod2 ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f40,axiom,(
% 65.09/8.70 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| is_aligned(A,B)| positional_advantage(A,B)| hazard_of_mortality(A,B) = high ) ))),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f41,axiom,(
% 65.09/8.70 greater(high,mod1) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f42,axiom,(
% 65.09/8.70 greater(mod1,low) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f43,axiom,(
% 65.09/8.70 greater(low,very_low) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f44,axiom,(
% 65.09/8.70 greater(high,mod2) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f45,axiom,(
% 65.09/8.70 greater(mod2,low) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f46,axiom,(
% 65.09/8.70 greater(mod2,mod1) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f47,negated_conjecture,(
% 65.09/8.70 organization(sk3) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f48,negated_conjecture,(
% 65.09/8.70 robust_position(sk3) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f49,negated_conjecture,(
% 65.09/8.70 ~ has_endowment(sk3) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f50,negated_conjecture,(
% 65.09/8.70 age(sk3,sk4) = zero ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f51,negated_conjecture,(
% 65.09/8.70 greater(sigma,zero) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f52,negated_conjecture,(
% 65.09/8.70 greater(tau,zero) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f53,negated_conjecture,(
% 65.09/8.70 smaller(sigma,tau) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f54,negated_conjecture,(
% 65.09/8.70 smaller_or_equal(age(sk3,sk5),sigma) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f55,negated_conjecture,(
% 65.09/8.70 greater(age(sk3,sk6),sigma) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f56,negated_conjecture,(
% 65.09/8.70 smaller_or_equal(age(sk3,sk6),tau) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f57,negated_conjecture,(
% 65.09/8.70 greater(age(sk3,sk7),tau) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f58,negated_conjecture,(
% 65.09/8.70 ( ~ smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))| ~ smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6))| hazard_of_mortality(sk3,sk5) != hazard_of_mortality(sk3,sk4) ) ),
% 65.09/8.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.09/8.70 fof(f59,plain,(
% 65.09/8.70 ![X0,X1]: (~smaller_or_equal(X0,X1)|smaller(X0,X1)|X0=X1)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f1])).
% 65.09/8.70 fof(f60,plain,(
% 65.09/8.70 ![X0,X1]: (~smaller(X0,X1)|smaller_or_equal(X0,X1))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f2])).
% 65.09/8.70 fof(f62,plain,(
% 65.09/8.70 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f4])).
% 65.09/8.70 fof(f63,plain,(
% 65.09/8.70 ![X0,X1]: (~greater(X0,X1)|greater_or_equal(X0,X1))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f5])).
% 65.09/8.70 fof(f65,plain,(
% 65.09/8.70 ![X0,X1]: (~smaller(X0,X1)|greater(X1,X0))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f7])).
% 65.09/8.70 fof(f66,plain,(
% 65.09/8.70 ![X0,X1]: (~greater(X0,X1)|smaller(X1,X0))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f8])).
% 65.09/8.70 fof(f67,plain,(
% 65.09/8.70 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f9])).
% 65.09/8.70 fof(f68,plain,(
% 65.09/8.70 ![A,C]: ((![B]: (~greater(A,B)|~greater(B,C)))|greater(A,C))),
% 65.09/8.70 inference(miniscoping,[status(thm)],[f10])).
% 65.09/8.70 fof(f69,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f68])).
% 65.09/8.70 fof(f70,plain,(
% 65.09/8.70 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater(X0,X1))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f11])).
% 65.09/8.70 fof(f78,plain,(
% 65.09/8.70 ![A]: ((~organization(A)|has_endowment(A))|(![B]: ~has_immunity(A,B)))),
% 65.09/8.70 inference(miniscoping,[status(thm)],[f19])).
% 65.09/8.70 fof(f79,plain,(
% 65.09/8.70 ![X0,X1]: (~organization(X0)|has_endowment(X0)|~has_immunity(X0,X1))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f78])).
% 65.09/8.70 fof(f80,plain,(
% 65.09/8.70 ![A]: ((![B,C]: ~dissimilar(A,B,C))|organization(A))),
% 65.09/8.70 inference(miniscoping,[status(thm)],[f20])).
% 65.09/8.70 fof(f81,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|organization(X0))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f80])).
% 65.09/8.70 fof(f82,plain,(
% 65.09/8.70 ![A,C]: ((![B]: (~dissimilar(A,B,C)|is_aligned(A,B)))|is_aligned(A,C))),
% 65.09/8.70 inference(miniscoping,[status(thm)],[f21])).
% 65.09/8.70 fof(f83,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|is_aligned(X0,X1)|is_aligned(X0,X2))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f82])).
% 65.09/8.70 fof(f84,plain,(
% 65.09/8.70 ![A,C]: ((![B]: (~dissimilar(A,B,C)|~is_aligned(A,B)))|~is_aligned(A,C))),
% 65.09/8.70 inference(miniscoping,[status(thm)],[f22])).
% 65.09/8.70 fof(f85,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f84])).
% 65.09/8.70 fof(f88,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2)|dissimilar(X0,X1,X2))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f24])).
% 65.09/8.70 fof(f89,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2)|dissimilar(X0,X2,X1))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f25])).
% 65.09/8.70 fof(f92,plain,(
% 65.09/8.70 ![X0,X1]: (~organization(X0)|~age(X0,X1)=zero|is_aligned(X0,X1))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f27])).
% 65.09/8.70 fof(f93,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~greater(age(X0,X2),sigma)|dissimilar(X0,X1,X2))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f28])).
% 65.09/8.70 fof(f94,plain,(
% 65.09/8.70 ![A,C]: ((![B]: ((~organization(A)|~age(A,B)=zero)|~dissimilar(A,B,C)))|greater(age(A,C),sigma))),
% 65.09/8.70 inference(miniscoping,[status(thm)],[f29])).
% 65.09/8.70 fof(f95,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~dissimilar(X0,X1,X2)|greater(age(X0,X2),sigma))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f94])).
% 65.09/8.70 fof(f96,plain,(
% 65.09/8.70 ![X0,X1]: (~robust_position(X0)|~smaller_or_equal(age(X0,X1),tau)|~positional_advantage(X0,X1))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f30])).
% 65.09/8.70 fof(f97,plain,(
% 65.09/8.70 ![X0,X1]: (~robust_position(X0)|~greater(age(X0,X1),tau)|positional_advantage(X0,X1))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f31])).
% 65.09/8.70 fof(f98,plain,(
% 65.09/8.70 ![X0]: (smaller_or_equal(age(X0,sk2(X0)),tau)|greater(age(X0,sk2(X0)),tau)|robust_position(X0))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f32])).
% 65.09/8.70 fof(f100,plain,(
% 65.09/8.70 ![X0]: (positional_advantage(X0,sk2(X0))|greater(age(X0,sk2(X0)),tau)|robust_position(X0))),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f34])).
% 65.09/8.70 fof(f102,plain,(
% 65.09/8.70 ![X0,X1]: (~organization(X0)|~has_immunity(X0,X1)|hazard_of_mortality(X0,X1)=very_low)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f36])).
% 65.09/8.70 fof(f103,plain,(
% 65.09/8.70 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=low)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f37])).
% 65.09/8.70 fof(f104,plain,(
% 65.09/8.70 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod1)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f38])).
% 65.09/8.70 fof(f105,plain,(
% 65.09/8.70 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f39])).
% 65.09/8.70 fof(f106,plain,(
% 65.09/8.70 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=high)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f40])).
% 65.09/8.70 fof(f107,plain,(
% 65.09/8.70 greater(high,mod1)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f41])).
% 65.09/8.70 fof(f108,plain,(
% 65.09/8.70 greater(mod1,low)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f42])).
% 65.09/8.70 fof(f109,plain,(
% 65.09/8.70 greater(low,very_low)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f43])).
% 65.09/8.70 fof(f110,plain,(
% 65.09/8.70 greater(high,mod2)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f44])).
% 65.09/8.70 fof(f111,plain,(
% 65.09/8.70 greater(mod2,low)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f45])).
% 65.09/8.70 fof(f112,plain,(
% 65.09/8.70 greater(mod2,mod1)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f46])).
% 65.09/8.70 fof(f113,plain,(
% 65.09/8.70 organization(sk3)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f47])).
% 65.09/8.70 fof(f114,plain,(
% 65.09/8.70 robust_position(sk3)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f48])).
% 65.09/8.70 fof(f115,plain,(
% 65.09/8.70 ~has_endowment(sk3)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f49])).
% 65.09/8.70 fof(f116,plain,(
% 65.09/8.70 age(sk3,sk4)=zero),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f50])).
% 65.09/8.70 fof(f117,plain,(
% 65.09/8.70 greater(sigma,zero)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f51])).
% 65.09/8.70 fof(f118,plain,(
% 65.09/8.70 greater(tau,zero)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f52])).
% 65.09/8.70 fof(f119,plain,(
% 65.09/8.70 smaller(sigma,tau)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f53])).
% 65.09/8.70 fof(f120,plain,(
% 65.09/8.70 smaller_or_equal(age(sk3,sk5),sigma)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f54])).
% 65.09/8.70 fof(f121,plain,(
% 65.09/8.70 greater(age(sk3,sk6),sigma)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f55])).
% 65.09/8.70 fof(f122,plain,(
% 65.09/8.70 smaller_or_equal(age(sk3,sk6),tau)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f56])).
% 65.09/8.70 fof(f123,plain,(
% 65.09/8.70 greater(age(sk3,sk7),tau)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f57])).
% 65.09/8.70 fof(f124,plain,(
% 65.09/8.70 ~smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))|~smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6))|~hazard_of_mortality(sk3,sk5)=hazard_of_mortality(sk3,sk4)),
% 65.09/8.70 inference(cnf_transformation,[status(thm)],[f58])).
% 65.09/8.70 fof(f125,definition,(
% 65.09/8.70 sQ0_spl <=> (smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f126,plain,(
% 65.09/8.70 smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))|~sQ0_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f125])).
% 65.09/8.70 fof(f127,plain,(
% 65.09/8.70 ~smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))|sQ0_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f125])).
% 65.09/8.70 fof(f128,definition,(
% 65.09/8.70 sQ1_spl <=> (smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6)))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f129,plain,(
% 65.09/8.70 smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6))|~sQ1_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f128])).
% 65.09/8.70 fof(f130,plain,(
% 65.09/8.70 ~smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6))|sQ1_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f128])).
% 65.09/8.70 fof(f131,definition,(
% 65.09/8.70 sQ2_spl <=> (hazard_of_mortality(sk3,sk5)=hazard_of_mortality(sk3,sk4))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f133,plain,(
% 65.09/8.70 ~hazard_of_mortality(sk3,sk5)=hazard_of_mortality(sk3,sk4)|sQ2_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f131])).
% 65.09/8.70 fof(f134,plain,(
% 65.09/8.70 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f124,f125,f128,f131])).
% 65.09/8.70 fof(f138,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~age(X0,X1)=zero|~dissimilar(X0,X1,X2)|greater(age(X0,X2),sigma))),
% 65.09/8.70 inference(forward_subsumption_resolution,[status(thm)],[f95,f81])).
% 65.09/8.70 fof(f139,plain,(
% 65.09/8.70 smaller(zero,tau)),
% 65.09/8.70 inference(resolution,[status(thm)],[f66,f118])).
% 65.09/8.70 fof(f140,plain,(
% 65.09/8.70 smaller(zero,sigma)),
% 65.09/8.70 inference(resolution,[status(thm)],[f66,f117])).
% 65.09/8.70 fof(f144,plain,(
% 65.09/8.70 ~greater(zero,tau)),
% 65.09/8.70 inference(resolution,[status(thm)],[f67,f118])).
% 65.09/8.70 fof(f145,plain,(
% 65.09/8.70 ~greater(zero,sigma)),
% 65.09/8.70 inference(resolution,[status(thm)],[f67,f117])).
% 65.09/8.70 fof(f146,plain,(
% 65.09/8.70 ![X0,X1]: (~greater(X0,X1)|~smaller(X0,X1))),
% 65.09/8.70 inference(resolution,[status(thm)],[f67,f65])).
% 65.09/8.70 fof(f147,plain,(
% 65.09/8.70 ~greater(mod1,high)),
% 65.09/8.70 inference(resolution,[status(thm)],[f107,f67])).
% 65.09/8.70 fof(f148,plain,(
% 65.09/8.70 smaller(mod1,high)),
% 65.09/8.70 inference(resolution,[status(thm)],[f107,f66])).
% 65.09/8.70 fof(f149,plain,(
% 65.09/8.70 ~greater(low,mod1)),
% 65.09/8.70 inference(resolution,[status(thm)],[f108,f67])).
% 65.09/8.70 fof(f151,plain,(
% 65.09/8.70 ~greater(very_low,low)),
% 65.09/8.70 inference(resolution,[status(thm)],[f109,f67])).
% 65.09/8.70 fof(f153,plain,(
% 65.09/8.70 ~greater(mod2,high)),
% 65.09/8.70 inference(resolution,[status(thm)],[f110,f67])).
% 65.09/8.70 fof(f154,plain,(
% 65.09/8.70 smaller(mod2,high)),
% 65.09/8.70 inference(resolution,[status(thm)],[f110,f66])).
% 65.09/8.70 fof(f155,plain,(
% 65.09/8.70 ~greater(low,mod2)),
% 65.09/8.70 inference(resolution,[status(thm)],[f111,f67])).
% 65.09/8.70 fof(f156,plain,(
% 65.09/8.70 smaller(low,mod2)),
% 65.09/8.70 inference(resolution,[status(thm)],[f111,f66])).
% 65.09/8.70 fof(f157,plain,(
% 65.09/8.70 ~greater(mod1,mod2)),
% 65.09/8.70 inference(resolution,[status(thm)],[f112,f67])).
% 65.09/8.70 fof(f158,plain,(
% 65.09/8.70 smaller(mod1,mod2)),
% 65.09/8.70 inference(resolution,[status(thm)],[f112,f66])).
% 65.09/8.70 fof(f159,plain,(
% 65.09/8.70 ~smaller(tau,zero)),
% 65.09/8.70 inference(resolution,[status(thm)],[f144,f65])).
% 65.09/8.70 fof(f160,plain,(
% 65.09/8.70 ~smaller(sigma,zero)),
% 65.09/8.70 inference(resolution,[status(thm)],[f145,f65])).
% 65.09/8.70 fof(f161,plain,(
% 65.09/8.70 ~smaller(high,mod1)),
% 65.09/8.70 inference(resolution,[status(thm)],[f147,f65])).
% 65.09/8.70 fof(f163,plain,(
% 65.09/8.70 greater_or_equal(mod2,mod1)),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f112])).
% 65.09/8.70 fof(f164,plain,(
% 65.09/8.70 greater_or_equal(mod2,low)),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f111])).
% 65.09/8.70 fof(f165,plain,(
% 65.09/8.70 greater_or_equal(low,very_low)),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f109])).
% 65.09/8.70 fof(f166,plain,(
% 65.09/8.70 greater_or_equal(mod1,low)),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f108])).
% 65.09/8.70 fof(f167,plain,(
% 65.09/8.70 greater_or_equal(high,mod2)),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f110])).
% 65.09/8.70 fof(f168,plain,(
% 65.09/8.70 greater_or_equal(high,mod1)),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f107])).
% 65.09/8.70 fof(f169,plain,(
% 65.09/8.70 greater_or_equal(tau,zero)),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f118])).
% 65.09/8.70 fof(f170,plain,(
% 65.09/8.70 greater_or_equal(sigma,zero)),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f117])).
% 65.09/8.70 fof(f171,plain,(
% 65.09/8.70 ![X0,X1]: (greater_or_equal(X0,X1)|~smaller(X1,X0))),
% 65.09/8.70 inference(resolution,[status(thm)],[f63,f65])).
% 65.09/8.70 fof(f176,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|~greater(X2,X0))),
% 65.09/8.70 inference(resolution,[status(thm)],[f69,f67])).
% 65.09/8.70 fof(f178,plain,(
% 65.09/8.70 greater(tau,zero)|tau=zero),
% 65.09/8.70 inference(resolution,[status(thm)],[f169,f62])).
% 65.09/8.70 fof(f179,definition,(
% 65.09/8.70 sQ3_spl <=> (greater(tau,zero))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f182,definition,(
% 65.09/8.70 sQ4_spl <=> (tau=zero)),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f183,plain,(
% 65.09/8.70 tau=zero|~sQ4_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f182])).
% 65.09/8.70 fof(f184,plain,(
% 65.09/8.70 ~tau=zero|sQ4_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f182])).
% 65.09/8.70 fof(f185,plain,(
% 65.09/8.70 sQ3_spl|sQ4_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f178,f179,f182])).
% 65.09/8.70 fof(f187,plain,(
% 65.09/8.70 ~smaller(zero,zero)|~sQ4_spl),
% 65.09/8.70 inference(backward_demodulation,[status(thm)],[f183,f159])).
% 65.09/8.70 fof(f189,plain,(
% 65.09/8.70 smaller(zero,zero)|~sQ4_spl),
% 65.09/8.70 inference(backward_demodulation,[status(thm)],[f183,f139])).
% 65.09/8.70 fof(f200,plain,(
% 65.09/8.70 $false|~sQ4_spl),
% 65.09/8.70 inference(forward_subsumption_resolution,[status(thm)],[f189,f187])).
% 65.09/8.70 fof(f201,plain,(
% 65.09/8.70 ~sQ4_spl),
% 65.09/8.70 inference(contradiction_clause,[status(thm)],[f200])).
% 65.09/8.70 fof(f202,plain,(
% 65.09/8.70 smaller(age(sk3,sk5),sigma)|age(sk3,sk5)=sigma),
% 65.09/8.70 inference(resolution,[status(thm)],[f120,f59])).
% 65.09/8.70 fof(f203,definition,(
% 65.09/8.70 sQ5_spl <=> (smaller(age(sk3,sk5),sigma))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f204,plain,(
% 65.09/8.70 smaller(age(sk3,sk5),sigma)|~sQ5_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f203])).
% 65.09/8.70 fof(f206,definition,(
% 65.09/8.70 sQ6_spl <=> (age(sk3,sk5)=sigma)),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f207,plain,(
% 65.09/8.70 age(sk3,sk5)=sigma|~sQ6_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f206])).
% 65.09/8.70 fof(f209,plain,(
% 65.09/8.70 sQ5_spl|sQ6_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f202,f203,f206])).
% 65.09/8.70 fof(f212,plain,(
% 65.09/8.70 ![X0]: (~greater(low,X0)|~greater(X0,mod1))),
% 65.09/8.70 inference(resolution,[status(thm)],[f149,f69])).
% 65.09/8.70 fof(f213,plain,(
% 65.09/8.70 ~smaller(mod1,low)),
% 65.09/8.70 inference(resolution,[status(thm)],[f149,f65])).
% 65.09/8.70 fof(f215,plain,(
% 65.09/8.70 ~smaller(low,very_low)),
% 65.09/8.70 inference(resolution,[status(thm)],[f151,f65])).
% 65.09/8.70 fof(f217,plain,(
% 65.09/8.70 ~smaller(high,mod2)),
% 65.09/8.70 inference(resolution,[status(thm)],[f153,f65])).
% 65.09/8.70 fof(f218,plain,(
% 65.09/8.70 ![X0]: (~greater(low,X0)|~greater(X0,mod2))),
% 65.09/8.70 inference(resolution,[status(thm)],[f155,f69])).
% 65.09/8.70 fof(f219,plain,(
% 65.09/8.70 ~smaller(mod2,low)),
% 65.09/8.70 inference(resolution,[status(thm)],[f155,f65])).
% 65.09/8.70 fof(f220,plain,(
% 65.09/8.70 smaller(mod2,high)|mod2=high),
% 65.09/8.70 inference(resolution,[status(thm)],[f70,f153])).
% 65.09/8.70 fof(f221,plain,(
% 65.09/8.70 smaller(very_low,low)|very_low=low),
% 65.09/8.70 inference(resolution,[status(thm)],[f70,f151])).
% 65.09/8.70 fof(f222,plain,(
% 65.09/8.70 smaller(low,mod2)|low=mod2),
% 65.09/8.70 inference(resolution,[status(thm)],[f70,f155])).
% 65.09/8.70 fof(f223,plain,(
% 65.09/8.70 smaller(low,mod1)|low=mod1),
% 65.09/8.70 inference(resolution,[status(thm)],[f70,f149])).
% 65.09/8.70 fof(f224,plain,(
% 65.09/8.70 smaller(mod1,high)|mod1=high),
% 65.09/8.70 inference(resolution,[status(thm)],[f70,f147])).
% 65.09/8.70 fof(f225,plain,(
% 65.09/8.70 smaller(zero,sigma)|zero=sigma),
% 65.09/8.70 inference(resolution,[status(thm)],[f70,f145])).
% 65.09/8.70 fof(f226,plain,(
% 65.09/8.70 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater_or_equal(X0,X1))),
% 65.09/8.70 inference(resolution,[status(thm)],[f70,f63])).
% 65.09/8.70 fof(f228,plain,(
% 65.09/8.70 ![X0,X1]: (smaller(X0,X1)|X0=X1|smaller(X1,X0))),
% 65.09/8.70 inference(resolution,[status(thm)],[f70,f66])).
% 65.09/8.70 fof(f229,definition,(
% 65.09/8.70 sQ7_spl <=> (smaller(mod2,high))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f232,definition,(
% 65.09/8.70 sQ8_spl <=> (mod2=high)),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f233,plain,(
% 65.09/8.70 mod2=high|~sQ8_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f232])).
% 65.09/8.70 fof(f234,plain,(
% 65.09/8.70 ~mod2=high|sQ8_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f232])).
% 65.09/8.70 fof(f235,plain,(
% 65.09/8.70 sQ7_spl|sQ8_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f220,f229,f232])).
% 65.09/8.70 fof(f236,definition,(
% 65.09/8.70 sQ9_spl <=> (smaller(very_low,low))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f239,definition,(
% 65.09/8.70 sQ10_spl <=> (very_low=low)),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f240,plain,(
% 65.09/8.70 very_low=low|~sQ10_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f239])).
% 65.09/8.70 fof(f242,plain,(
% 65.09/8.70 sQ9_spl|sQ10_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f221,f236,f239])).
% 65.09/8.70 fof(f243,definition,(
% 65.09/8.70 sQ11_spl <=> (smaller(low,mod2))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f246,definition,(
% 65.09/8.70 sQ12_spl <=> (low=mod2)),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f247,plain,(
% 65.09/8.70 low=mod2|~sQ12_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f246])).
% 65.09/8.70 fof(f249,plain,(
% 65.09/8.70 sQ11_spl|sQ12_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f222,f243,f246])).
% 65.09/8.70 fof(f250,definition,(
% 65.09/8.70 sQ13_spl <=> (smaller(low,mod1))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f253,definition,(
% 65.09/8.70 sQ14_spl <=> (low=mod1)),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f254,plain,(
% 65.09/8.70 low=mod1|~sQ14_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f253])).
% 65.09/8.70 fof(f256,plain,(
% 65.09/8.70 sQ13_spl|sQ14_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f223,f250,f253])).
% 65.09/8.70 fof(f257,definition,(
% 65.09/8.70 sQ15_spl <=> (smaller(mod1,high))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f260,definition,(
% 65.09/8.70 sQ16_spl <=> (mod1=high)),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f261,plain,(
% 65.09/8.70 mod1=high|~sQ16_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f260])).
% 65.09/8.70 fof(f263,plain,(
% 65.09/8.70 sQ15_spl|sQ16_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f224,f257,f260])).
% 65.09/8.70 fof(f264,definition,(
% 65.09/8.70 sQ17_spl <=> (smaller(zero,sigma))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f267,definition,(
% 65.09/8.70 sQ18_spl <=> (zero=sigma)),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f268,plain,(
% 65.09/8.70 zero=sigma|~sQ18_spl),
% 65.09/8.70 inference(component_clause,[status(thm)],[f267])).
% 65.09/8.70 fof(f270,plain,(
% 65.09/8.70 sQ17_spl|sQ18_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f225,f264,f267])).
% 65.09/8.70 fof(f271,plain,(
% 65.09/8.70 ~smaller(zero,zero)|~sQ18_spl),
% 65.09/8.70 inference(backward_demodulation,[status(thm)],[f268,f160])).
% 65.09/8.70 fof(f273,plain,(
% 65.09/8.70 smaller(zero,zero)|~sQ18_spl),
% 65.09/8.70 inference(backward_demodulation,[status(thm)],[f268,f140])).
% 65.09/8.70 fof(f286,plain,(
% 65.09/8.70 ~greater(high,high)|~sQ16_spl),
% 65.09/8.70 inference(backward_demodulation,[status(thm)],[f261,f147])).
% 65.09/8.70 fof(f289,plain,(
% 65.09/8.70 greater(high,high)|~sQ16_spl),
% 65.09/8.70 inference(backward_demodulation,[status(thm)],[f261,f107])).
% 65.09/8.70 fof(f323,plain,(
% 65.09/8.70 $false|~sQ18_spl),
% 65.09/8.70 inference(forward_subsumption_resolution,[status(thm)],[f273,f271])).
% 65.09/8.70 fof(f324,plain,(
% 65.09/8.70 ~sQ18_spl),
% 65.09/8.70 inference(contradiction_clause,[status(thm)],[f323])).
% 65.09/8.70 fof(f331,plain,(
% 65.09/8.70 $false|~sQ16_spl),
% 65.09/8.70 inference(forward_subsumption_resolution,[status(thm)],[f289,f286])).
% 65.09/8.70 fof(f332,plain,(
% 65.09/8.70 ~sQ16_spl),
% 65.09/8.70 inference(contradiction_clause,[status(thm)],[f331])).
% 65.09/8.70 fof(f336,plain,(
% 65.09/8.70 ~greater(very_low,very_low)|~sQ10_spl),
% 65.09/8.70 inference(forward_demodulation,[status(thm)],[f240,f151])).
% 65.09/8.70 fof(f338,plain,(
% 65.09/8.70 greater(very_low,very_low)|~sQ10_spl),
% 65.09/8.70 inference(forward_demodulation,[status(thm)],[f240,f109])).
% 65.09/8.70 fof(f339,plain,(
% 65.09/8.70 $false|~sQ10_spl),
% 65.09/8.70 inference(forward_subsumption_resolution,[status(thm)],[f338,f336])).
% 65.09/8.70 fof(f340,plain,(
% 65.09/8.70 ~sQ10_spl),
% 65.09/8.70 inference(contradiction_clause,[status(thm)],[f339])).
% 65.09/8.70 fof(f345,plain,(
% 65.09/8.70 greater(high,high)|~sQ8_spl),
% 65.09/8.70 inference(backward_demodulation,[status(thm)],[f233,f110])).
% 65.09/8.70 fof(f346,plain,(
% 65.09/8.70 ~greater(high,high)|~sQ8_spl),
% 65.09/8.70 inference(backward_demodulation,[status(thm)],[f233,f153])).
% 65.09/8.70 fof(f359,plain,(
% 65.09/8.70 $false|~sQ8_spl),
% 65.09/8.70 inference(forward_subsumption_resolution,[status(thm)],[f346,f345])).
% 65.09/8.70 fof(f360,plain,(
% 65.09/8.70 ~sQ8_spl),
% 65.09/8.70 inference(contradiction_clause,[status(thm)],[f359])).
% 65.09/8.70 fof(f363,plain,(
% 65.09/8.70 smaller(zero,tau)|zero=tau),
% 65.09/8.70 inference(resolution,[status(thm)],[f144,f70])).
% 65.09/8.70 fof(f366,definition,(
% 65.09/8.70 sQ19_spl <=> (smaller(zero,tau))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f369,plain,(
% 65.09/8.70 sQ19_spl|sQ4_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f363,f366,f182])).
% 65.09/8.70 fof(f380,plain,(
% 65.09/8.70 greater(sigma,zero)|sigma=zero),
% 65.09/8.70 inference(resolution,[status(thm)],[f170,f62])).
% 65.09/8.70 fof(f381,definition,(
% 65.09/8.70 sQ20_spl <=> (greater(sigma,zero))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f384,plain,(
% 65.09/8.70 sQ20_spl|sQ18_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f380,f381,f267])).
% 65.09/8.70 fof(f398,plain,(
% 65.09/8.70 greater(low,very_low)|low=very_low),
% 65.09/8.70 inference(resolution,[status(thm)],[f165,f62])).
% 65.09/8.70 fof(f399,definition,(
% 65.09/8.70 sQ21_spl <=> (greater(low,very_low))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f402,plain,(
% 65.09/8.70 sQ21_spl|sQ10_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f398,f399,f239])).
% 65.09/8.70 fof(f406,plain,(
% 65.09/8.70 greater(high,mod1)|high=mod1),
% 65.09/8.70 inference(resolution,[status(thm)],[f168,f62])).
% 65.09/8.70 fof(f407,definition,(
% 65.09/8.70 sQ22_spl <=> (greater(high,mod1))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f410,plain,(
% 65.09/8.70 sQ22_spl|sQ16_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f406,f407,f260])).
% 65.09/8.70 fof(f411,plain,(
% 65.09/8.70 greater(mod1,low)|mod1=low),
% 65.09/8.70 inference(resolution,[status(thm)],[f166,f62])).
% 65.09/8.70 fof(f412,definition,(
% 65.09/8.70 sQ23_spl <=> (greater(mod1,low))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f415,plain,(
% 65.09/8.70 sQ23_spl|sQ14_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f411,f412,f253])).
% 65.09/8.70 fof(f419,plain,(
% 65.09/8.70 greater(high,mod2)|high=mod2),
% 65.09/8.70 inference(resolution,[status(thm)],[f167,f62])).
% 65.09/8.70 fof(f420,definition,(
% 65.09/8.70 sQ24_spl <=> (greater(high,mod2))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f423,plain,(
% 65.09/8.70 sQ24_spl|sQ8_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f419,f420,f232])).
% 65.09/8.70 fof(f431,plain,(
% 65.09/8.70 greater(mod2,low)|mod2=low),
% 65.09/8.70 inference(resolution,[status(thm)],[f164,f62])).
% 65.09/8.70 fof(f432,definition,(
% 65.09/8.70 sQ25_spl <=> (greater(mod2,low))),
% 65.09/8.70 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 65.09/8.70 fof(f435,plain,(
% 65.09/8.70 sQ25_spl|sQ12_spl),
% 65.09/8.70 inference(split_clause,[status(thm)],[f431,f432,f246])).
% 65.09/8.70 fof(f436,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~organization(X0)|is_aligned(X0,X1)|dissimilar(X0,X2,X1)|~organization(X0)|~age(X0,X2)=zero)),
% 65.09/8.70 inference(resolution,[status(thm)],[f88,f92])).
% 65.09/8.70 fof(f437,plain,(
% 65.09/8.70 ![X0,X1,X2]: (~organization(X0)|is_aligned(X0,X1)|dissimilar(X0,X2,X1)|~age(X0,X2)=zero)),
% 65.09/8.71 inference(duplicate_literals_removal,[status(thm)],[f436])).
% 65.09/8.71 fof(f441,plain,(
% 65.09/8.71 greater_or_equal(age(sk3,sk7),tau)),
% 65.09/8.71 inference(resolution,[status(thm)],[f123,f63])).
% 65.09/8.71 fof(f442,plain,(
% 65.09/8.71 ~greater(tau,age(sk3,sk7))),
% 65.09/8.71 inference(resolution,[status(thm)],[f123,f67])).
% 65.09/8.71 fof(f443,plain,(
% 65.09/8.71 smaller(tau,age(sk3,sk7))),
% 65.09/8.71 inference(resolution,[status(thm)],[f123,f66])).
% 65.09/8.71 fof(f462,plain,(
% 65.09/8.71 smaller(mod1,mod2)|mod1=mod2),
% 65.09/8.71 inference(resolution,[status(thm)],[f157,f70])).
% 65.09/8.71 fof(f464,plain,(
% 65.09/8.71 ~smaller(mod2,mod1)),
% 65.09/8.71 inference(resolution,[status(thm)],[f157,f65])).
% 65.09/8.71 fof(f465,definition,(
% 65.09/8.71 sQ28_spl <=> (smaller(mod1,mod2))),
% 65.09/8.71 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 65.09/8.71 fof(f468,definition,(
% 65.09/8.71 sQ29_spl <=> (mod1=mod2)),
% 65.09/8.71 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 65.09/8.71 fof(f469,plain,(
% 65.09/8.71 mod1=mod2|~sQ29_spl),
% 65.09/8.71 inference(component_clause,[status(thm)],[f468])).
% 65.09/8.71 fof(f470,plain,(
% 65.09/8.71 ~mod1=mod2|sQ29_spl),
% 65.09/8.71 inference(component_clause,[status(thm)],[f468])).
% 65.09/8.71 fof(f471,plain,(
% 65.09/8.71 sQ28_spl|sQ29_spl),
% 65.09/8.71 inference(split_clause,[status(thm)],[f462,f465,f468])).
% 65.09/8.71 fof(f472,plain,(
% 65.09/8.71 ~greater(mod1,mod1)|~sQ29_spl),
% 65.09/8.71 inference(backward_demodulation,[status(thm)],[f469,f157])).
% 65.09/8.71 fof(f485,plain,(
% 65.09/8.71 greater(mod1,mod1)|~sQ29_spl),
% 65.09/8.71 inference(backward_demodulation,[status(thm)],[f469,f112])).
% 65.09/8.71 fof(f492,plain,(
% 65.09/8.71 $false|~sQ29_spl),
% 65.09/8.71 inference(forward_subsumption_resolution,[status(thm)],[f485,f472])).
% 65.09/8.71 fof(f493,plain,(
% 65.09/8.71 ~sQ29_spl),
% 65.09/8.71 inference(contradiction_clause,[status(thm)],[f492])).
% 65.09/8.71 fof(f495,definition,(
% 65.09/8.71 sQ30_spl <=> (greater(tau,sigma))),
% 65.09/8.71 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 65.09/8.71 fof(f496,plain,(
% 65.09/8.71 greater(tau,sigma)|~sQ30_spl),
% 65.09/8.71 inference(component_clause,[status(thm)],[f495])).
% 65.09/8.71 fof(f498,definition,(
% 65.09/8.71 sQ31_spl <=> (tau=sigma)),
% 65.09/8.71 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 65.09/8.71 fof(f499,plain,(
% 65.09/8.71 tau=sigma|~sQ31_spl),
% 65.09/8.71 inference(component_clause,[status(thm)],[f498])).
% 65.09/8.71 fof(f504,plain,(
% 65.09/8.71 smaller(sigma,sigma)|~sQ31_spl),
% 65.09/8.71 inference(backward_demodulation,[status(thm)],[f499,f119])).
% 65.09/8.71 fof(f526,plain,(
% 65.09/8.71 ![X0,X1]: (~age(sk3,X0)=zero|~greater(age(sk3,X1),sigma)|dissimilar(sk3,X0,X1))),
% 65.09/8.71 inference(resolution,[status(thm)],[f93,f113])).
% 65.09/8.71 fof(f557,plain,(
% 65.09/8.71 greater_or_equal(age(sk3,sk6),sigma)),
% 65.09/8.71 inference(resolution,[status(thm)],[f121,f63])).
% 65.09/8.71 fof(f558,plain,(
% 65.09/8.71 ~greater(sigma,age(sk3,sk6))),
% 65.09/8.71 inference(resolution,[status(thm)],[f121,f67])).
% 65.09/8.71 fof(f559,plain,(
% 65.09/8.71 smaller(sigma,age(sk3,sk6))),
% 65.09/8.71 inference(resolution,[status(thm)],[f121,f66])).
% 65.09/8.71 fof(f570,plain,(
% 65.09/8.71 ~greater(sigma,tau)|~sQ30_spl),
% 65.09/8.71 inference(resolution,[status(thm)],[f496,f67])).
% 65.09/8.71 fof(f578,plain,(
% 65.09/8.71 greater(mod2,mod1)|mod2=mod1),
% 65.09/8.71 inference(resolution,[status(thm)],[f163,f62])).
% 65.09/8.71 fof(f579,definition,(
% 65.09/8.71 sQ32_spl <=> (greater(mod2,mod1))),
% 65.09/8.71 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 65.09/8.71 fof(f582,plain,(
% 65.09/8.71 sQ32_spl|sQ29_spl),
% 65.09/8.71 inference(split_clause,[status(thm)],[f578,f579,f468])).
% 65.09/8.71 fof(f589,plain,(
% 65.09/8.71 ![X0]: (~greater(sigma,X0)|~greater(X0,tau)|~sQ30_spl)),
% 65.09/8.71 inference(resolution,[status(thm)],[f570,f69])).
% 65.09/8.71 fof(f591,definition,(
% 65.09/8.71 sQ33_spl <=> (smaller(sigma,tau))),
% 65.09/8.71 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 65.09/8.71 fof(f601,plain,(
% 65.09/8.71 ~greater(sigma,tau)),
% 65.09/8.71 inference(resolution,[status(thm)],[f146,f119])).
% 65.09/8.71 fof(f608,definition,(
% 65.09/8.71 sQ34_spl <=> (smaller(sigma,sigma))),
% 65.09/8.71 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 65.09/8.71 fof(f609,plain,(
% 65.09/8.71 smaller(sigma,sigma)|~sQ34_spl),
% 65.09/8.71 inference(component_clause,[status(thm)],[f608])).
% 65.09/8.71 fof(f610,plain,(
% 65.09/8.71 ~smaller(sigma,sigma)|sQ34_spl),
% 65.09/8.71 inference(component_clause,[status(thm)],[f608])).
% 65.09/8.71 fof(f611,definition,(
% 65.09/8.71 sQ35_spl <=> (sigma=sigma)),
% 65.09/8.71 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 65.09/8.71 fof(f617,plain,(
% 65.09/8.71 ~greater(sigma,sigma)|~sQ34_spl),
% 65.09/8.71 inference(resolution,[status(thm)],[f609,f146])).
% 65.09/8.72 fof(f620,plain,(
% 65.09/8.72 ~smaller(sigma,sigma)|~sQ34_spl),
% 65.09/8.72 inference(resolution,[status(thm)],[f617,f65])).
% 65.09/8.72 fof(f622,plain,(
% 65.09/8.72 $false|~sQ34_spl),
% 65.09/8.72 inference(forward_subsumption_resolution,[status(thm)],[f620,f609])).
% 65.09/8.72 fof(f623,plain,(
% 65.09/8.72 ~sQ34_spl),
% 65.09/8.72 inference(contradiction_clause,[status(thm)],[f622])).
% 65.09/8.72 fof(f630,plain,(
% 65.09/8.72 greater_or_equal(tau,sigma)),
% 65.09/8.72 inference(resolution,[status(thm)],[f171,f119])).
% 65.09/8.72 fof(f633,plain,(
% 65.09/8.72 ![X0]: (has_immunity(sk3,X0)|is_aligned(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high)),
% 65.09/8.72 inference(resolution,[status(thm)],[f106,f113])).
% 65.09/8.72 fof(f635,plain,(
% 65.09/8.72 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2|~organization(X0)|~age(X0,X1)=zero)),
% 65.09/8.72 inference(resolution,[status(thm)],[f105,f92])).
% 65.09/8.72 fof(f636,plain,(
% 65.09/8.72 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2|~age(X0,X1)=zero)),
% 65.09/8.72 inference(duplicate_literals_removal,[status(thm)],[f635])).
% 65.09/8.72 fof(f648,plain,(
% 65.09/8.72 tau=zero|greater_or_equal(tau,zero)),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f159])).
% 65.09/8.72 fof(f649,plain,(
% 65.09/8.72 mod2=mod1|greater_or_equal(mod2,mod1)),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f464])).
% 65.09/8.72 fof(f650,plain,(
% 65.09/8.72 mod2=low|greater_or_equal(mod2,low)),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f219])).
% 65.09/8.72 fof(f651,plain,(
% 65.09/8.72 high=mod2|greater_or_equal(high,mod2)),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f217])).
% 65.09/8.72 fof(f652,plain,(
% 65.09/8.72 high=mod1|greater_or_equal(high,mod1)),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f161])).
% 65.09/8.72 fof(f653,plain,(
% 65.09/8.72 mod1=low|greater_or_equal(mod1,low)),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f213])).
% 65.09/8.72 fof(f654,plain,(
% 65.09/8.72 low=very_low|greater_or_equal(low,very_low)),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f215])).
% 65.09/8.72 fof(f656,plain,(
% 65.09/8.72 sigma=zero|greater_or_equal(sigma,zero)),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f160])).
% 65.09/8.72 fof(f657,plain,(
% 65.09/8.72 ![X0,X1]: (X0=X1|greater_or_equal(X0,X1)|greater_or_equal(X1,X0))),
% 65.09/8.72 inference(resolution,[status(thm)],[f226,f171])).
% 33.28/8.72 fof(f659,definition,(
% 33.28/8.72 sQ36_spl <=> (greater_or_equal(tau,sigma))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f661,plain,(
% 33.28/8.72 ~greater_or_equal(tau,sigma)|sQ36_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f659])).
% 33.28/8.72 fof(f663,definition,(
% 33.28/8.72 sQ37_spl <=> (greater_or_equal(tau,zero))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f666,plain,(
% 33.28/8.72 sQ4_spl|sQ37_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f648,f182,f663])).
% 33.28/8.72 fof(f667,definition,(
% 33.28/8.72 sQ38_spl <=> (greater_or_equal(mod2,mod1))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f670,plain,(
% 33.28/8.72 sQ29_spl|sQ38_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f649,f468,f667])).
% 33.28/8.72 fof(f671,definition,(
% 33.28/8.72 sQ39_spl <=> (greater_or_equal(mod2,low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f674,plain,(
% 33.28/8.72 sQ12_spl|sQ39_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f650,f246,f671])).
% 33.28/8.72 fof(f675,definition,(
% 33.28/8.72 sQ40_spl <=> (greater_or_equal(high,mod2))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f678,plain,(
% 33.28/8.72 sQ8_spl|sQ40_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f651,f232,f675])).
% 33.28/8.72 fof(f679,definition,(
% 33.28/8.72 sQ41_spl <=> (greater_or_equal(high,mod1))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f682,plain,(
% 33.28/8.72 sQ16_spl|sQ41_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f652,f260,f679])).
% 33.28/8.72 fof(f683,definition,(
% 33.28/8.72 sQ42_spl <=> (greater_or_equal(mod1,low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f686,plain,(
% 33.28/8.72 sQ14_spl|sQ42_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f653,f253,f683])).
% 33.28/8.72 fof(f687,definition,(
% 33.28/8.72 sQ43_spl <=> (greater_or_equal(low,very_low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f690,plain,(
% 33.28/8.72 sQ10_spl|sQ43_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f654,f239,f687])).
% 33.28/8.72 fof(f695,definition,(
% 33.28/8.72 sQ45_spl <=> (greater_or_equal(sigma,zero))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f698,plain,(
% 33.28/8.72 sQ18_spl|sQ45_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f656,f267,f695])).
% 33.28/8.72 fof(f709,plain,(
% 33.28/8.72 greater(low,low)|~sQ14_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f254,f108])).
% 33.28/8.72 fof(f714,plain,(
% 33.28/8.72 ~greater(low,low)|~sQ14_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f254,f149])).
% 33.28/8.72 fof(f728,plain,(
% 33.28/8.72 ~smaller(low,low)|~sQ12_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f247,f219])).
% 33.28/8.72 fof(f729,plain,(
% 33.28/8.72 smaller(low,low)|~sQ12_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f247,f156])).
% 33.28/8.72 fof(f742,plain,(
% 33.28/8.72 $false|~sQ14_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f714,f709])).
% 33.28/8.72 fof(f743,plain,(
% 33.28/8.72 ~sQ14_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f742])).
% 33.28/8.72 fof(f744,plain,(
% 33.28/8.72 $false|~sQ12_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f729,f728])).
% 33.28/8.72 fof(f745,plain,(
% 33.28/8.72 ~sQ12_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f744])).
% 33.28/8.72 fof(f752,plain,(
% 33.28/8.72 ![X0]: (~greater(age(sk3,X0),tau)|positional_advantage(sk3,X0))),
% 33.28/8.72 inference(resolution,[status(thm)],[f97,f114])).
% 33.28/8.72 fof(f790,plain,(
% 33.28/8.72 smaller(tau,age(sk3,sk7))|tau=age(sk3,sk7)),
% 33.28/8.72 inference(resolution,[status(thm)],[f442,f70])).
% 33.28/8.72 fof(f792,plain,(
% 33.28/8.72 ~smaller(age(sk3,sk7),tau)),
% 33.28/8.72 inference(resolution,[status(thm)],[f442,f65])).
% 33.28/8.72 fof(f793,definition,(
% 33.28/8.72 sQ46_spl <=> (smaller(tau,age(sk3,sk7)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f796,definition,(
% 33.28/8.72 sQ47_spl <=> (tau=age(sk3,sk7))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f797,plain,(
% 33.28/8.72 tau=age(sk3,sk7)|~sQ47_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f796])).
% 33.28/8.72 fof(f799,plain,(
% 33.28/8.72 sQ46_spl|sQ47_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f790,f793,f796])).
% 33.28/8.72 fof(f800,plain,(
% 33.28/8.72 ~greater(tau,tau)|~sQ47_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f797,f442])).
% 33.28/8.72 fof(f802,plain,(
% 33.28/8.72 greater(tau,tau)|~sQ47_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f797,f123])).
% 33.28/8.72 fof(f806,plain,(
% 33.28/8.72 $false|~sQ47_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f802,f800])).
% 33.28/8.72 fof(f807,plain,(
% 33.28/8.72 ~sQ47_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f806])).
% 33.28/8.72 fof(f843,plain,(
% 33.28/8.72 sigma=sigma|smaller(sigma,sigma)|sQ34_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f228,f610])).
% 33.28/8.72 fof(f873,plain,(
% 33.28/8.72 sQ35_spl|sQ34_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f843,f611,f608])).
% 33.28/8.72 fof(f878,definition,(
% 33.28/8.72 sQ49_spl <=> (greater(zero,tau))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f907,plain,(
% 33.28/8.72 ![X0,X1,X2,X3]: (~greater(X0,X1)|~greater(X2,X0)|~greater(X1,X3)|~greater(X3,X2))),
% 33.28/8.72 inference(resolution,[status(thm)],[f176,f69])).
% 33.28/8.72 fof(f909,plain,(
% 33.28/8.72 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X2,X0)|~smaller(X2,X1))),
% 33.28/8.72 inference(resolution,[status(thm)],[f176,f65])).
% 33.28/8.72 fof(f924,plain,(
% 33.28/8.72 ![X0]: (~greater(X0,X0)|~greater(X0,X0))),
% 33.28/8.72 inference(factoring,[status(thm)],[f176])).
% 33.28/8.72 fof(f925,plain,(
% 33.28/8.72 ![X0]: (~greater(X0,X0))),
% 33.28/8.72 inference(duplicate_literals_removal,[status(thm)],[f924])).
% 33.28/8.72 fof(f928,plain,(
% 33.28/8.72 ![X0]: (~smaller(X0,X0))),
% 33.28/8.72 inference(resolution,[status(thm)],[f925,f65])).
% 33.28/8.72 fof(f951,plain,(
% 33.28/8.72 greater(age(sk3,sk6),sigma)|age(sk3,sk6)=sigma),
% 33.28/8.72 inference(resolution,[status(thm)],[f557,f62])).
% 33.28/8.72 fof(f952,definition,(
% 33.28/8.72 sQ50_spl <=> (greater(age(sk3,sk6),sigma))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f955,definition,(
% 33.28/8.72 sQ51_spl <=> (age(sk3,sk6)=sigma)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f956,plain,(
% 33.28/8.72 age(sk3,sk6)=sigma|~sQ51_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f955])).
% 33.28/8.72 fof(f958,plain,(
% 33.28/8.72 sQ50_spl|sQ51_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f951,f952,f955])).
% 33.28/8.72 fof(f962,plain,(
% 33.28/8.72 greater(sigma,sigma)|~sQ51_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f956,f121])).
% 33.28/8.72 fof(f968,plain,(
% 33.28/8.72 $false|~sQ51_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f962,f925])).
% 33.28/8.72 fof(f969,plain,(
% 33.28/8.72 ~sQ51_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f968])).
% 33.28/8.72 fof(f973,plain,(
% 33.28/8.72 ![X0]: (~greater(X0,tau)|~smaller(X0,sigma)|~sQ30_spl)),
% 33.28/8.72 inference(resolution,[status(thm)],[f589,f65])).
% 33.28/8.72 fof(f975,plain,(
% 33.28/8.72 ~greater(age(sk3,sk5),sigma)|~sQ5_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f204,f146])).
% 33.28/8.72 fof(f981,definition,(
% 33.28/8.72 sQ52_spl <=> (greater(zero,sigma))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f996,plain,(
% 33.28/8.72 age(sk3,sk7)=tau|greater_or_equal(age(sk3,sk7),tau)),
% 33.28/8.72 inference(resolution,[status(thm)],[f792,f226])).
% 33.28/8.72 fof(f999,definition,(
% 33.28/8.72 sQ53_spl <=> (greater_or_equal(age(sk3,sk7),tau))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1002,plain,(
% 33.28/8.72 sQ47_spl|sQ53_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f996,f796,f999])).
% 33.28/8.72 fof(f1003,plain,(
% 33.28/8.72 greater(age(sk3,sk7),tau)|age(sk3,sk7)=tau),
% 33.28/8.72 inference(resolution,[status(thm)],[f441,f62])).
% 33.28/8.72 fof(f1004,definition,(
% 33.28/8.72 sQ54_spl <=> (greater(age(sk3,sk7),tau))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1007,plain,(
% 33.28/8.72 sQ54_spl|sQ47_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1003,f1004,f796])).
% 33.28/8.72 fof(f1011,plain,(
% 33.28/8.72 ![X0,X1]: (X0=X1|greater_or_equal(X1,X0)|greater(X0,X1)|X0=X1)),
% 33.28/8.72 inference(resolution,[status(thm)],[f657,f62])).
% 33.28/8.72 fof(f1014,plain,(
% 33.28/8.72 ![X0,X1]: (X0=X1|greater_or_equal(X1,X0)|greater(X0,X1))),
% 33.28/8.72 inference(duplicate_literals_removal,[status(thm)],[f1011])).
% 33.28/8.72 fof(f1019,plain,(
% 33.28/8.72 ~greater(very_low,mod2)),
% 33.28/8.72 inference(resolution,[status(thm)],[f218,f109])).
% 33.28/8.72 fof(f1022,plain,(
% 33.28/8.72 ![X0]: (~greater(X0,mod2)|~smaller(X0,low))),
% 33.28/8.72 inference(resolution,[status(thm)],[f218,f65])).
% 33.28/8.72 fof(f1023,plain,(
% 33.28/8.72 smaller(very_low,mod2)|very_low=mod2),
% 33.28/8.72 inference(resolution,[status(thm)],[f1019,f70])).
% 33.28/8.72 fof(f1024,plain,(
% 33.28/8.72 ![X0]: (~greater(very_low,X0)|~greater(X0,mod2))),
% 33.28/8.72 inference(resolution,[status(thm)],[f1019,f69])).
% 33.28/8.72 fof(f1025,plain,(
% 33.28/8.72 ~smaller(mod2,very_low)),
% 33.28/8.72 inference(resolution,[status(thm)],[f1019,f65])).
% 33.28/8.72 fof(f1026,definition,(
% 33.28/8.72 sQ55_spl <=> (smaller(very_low,mod2))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1027,plain,(
% 33.28/8.72 smaller(very_low,mod2)|~sQ55_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1026])).
% 33.28/8.72 fof(f1029,definition,(
% 33.28/8.72 sQ56_spl <=> (very_low=mod2)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1030,plain,(
% 33.28/8.72 very_low=mod2|~sQ56_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1029])).
% 33.28/8.72 fof(f1032,plain,(
% 33.28/8.72 sQ55_spl|sQ56_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1023,f1026,f1029])).
% 33.28/8.72 fof(f1042,plain,(
% 33.28/8.72 ~greater(low,very_low)|~sQ56_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f1030,f155])).
% 33.28/8.72 fof(f1067,plain,(
% 33.28/8.72 $false|~sQ56_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f1042,f109])).
% 33.28/8.72 fof(f1068,plain,(
% 33.28/8.72 ~sQ56_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f1067])).
% 33.28/8.72 fof(f1180,plain,(
% 33.28/8.72 greater_or_equal(mod2,very_low)|~sQ55_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f1027,f171])).
% 33.28/8.72 fof(f1185,plain,(
% 33.28/8.72 mod2=very_low|greater_or_equal(mod2,very_low)),
% 33.28/8.72 inference(resolution,[status(thm)],[f1025,f226])).
% 33.28/8.72 fof(f1188,definition,(
% 33.28/8.72 sQ58_spl <=> (greater_or_equal(mod2,very_low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1191,plain,(
% 33.28/8.72 sQ56_spl|sQ58_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1185,f1029,f1188])).
% 33.28/8.72 fof(f1194,plain,(
% 33.28/8.72 $false|sQ36_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f661,f630])).
% 33.28/8.72 fof(f1195,plain,(
% 33.28/8.72 sQ36_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f1194])).
% 33.28/8.72 fof(f1240,plain,(
% 33.28/8.72 sQ34_spl|~sQ31_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f504,f608,f498])).
% 33.28/8.72 fof(f1246,plain,(
% 33.28/8.72 greater(mod2,very_low)|mod2=very_low|~sQ55_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f1180,f62])).
% 33.28/8.72 fof(f1247,definition,(
% 33.28/8.72 sQ59_spl <=> (greater(mod2,very_low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1248,plain,(
% 33.28/8.72 greater(mod2,very_low)|~sQ59_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1247])).
% 33.28/8.72 fof(f1250,plain,(
% 33.28/8.72 sQ59_spl|sQ56_spl|~sQ55_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1246,f1247,f1029,f1026])).
% 33.28/8.72 fof(f1285,plain,(
% 33.28/8.72 greater(tau,sigma)|tau=sigma),
% 33.28/8.72 inference(resolution,[status(thm)],[f630,f62])).
% 33.28/8.72 fof(f1286,plain,(
% 33.28/8.72 sQ30_spl|sQ31_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1285,f495,f498])).
% 33.28/8.72 fof(f1287,plain,(
% 33.28/8.72 smaller(sigma,tau)|sigma=tau),
% 33.28/8.72 inference(resolution,[status(thm)],[f601,f70])).
% 33.28/8.72 fof(f1290,plain,(
% 33.28/8.72 sQ33_spl|sQ31_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1287,f591,f498])).
% 33.28/8.72 fof(f1324,plain,(
% 33.28/8.72 ~greater(very_low,mod1)),
% 33.28/8.72 inference(resolution,[status(thm)],[f212,f109])).
% 33.28/8.72 fof(f1328,plain,(
% 33.28/8.72 smaller(very_low,mod1)|very_low=mod1),
% 33.28/8.72 inference(resolution,[status(thm)],[f1324,f70])).
% 33.28/8.72 fof(f1330,plain,(
% 33.28/8.72 ~smaller(mod1,very_low)),
% 33.28/8.72 inference(resolution,[status(thm)],[f1324,f65])).
% 33.28/8.72 fof(f1331,definition,(
% 33.28/8.72 sQ61_spl <=> (smaller(very_low,mod1))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1332,plain,(
% 33.28/8.72 smaller(very_low,mod1)|~sQ61_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1331])).
% 33.28/8.72 fof(f1334,definition,(
% 33.28/8.72 sQ62_spl <=> (very_low=mod1)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1335,plain,(
% 33.28/8.72 very_low=mod1|~sQ62_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1334])).
% 33.28/8.72 fof(f1336,plain,(
% 33.28/8.72 ~very_low=mod1|sQ62_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1334])).
% 33.28/8.72 fof(f1337,plain,(
% 33.28/8.72 sQ61_spl|sQ62_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1328,f1331,f1334])).
% 33.28/8.72 fof(f1348,plain,(
% 33.28/8.72 greater(very_low,low)|~sQ62_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f1335,f108])).
% 33.28/8.72 fof(f1371,plain,(
% 33.28/8.72 $false|~sQ62_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f1348,f151])).
% 33.28/8.72 fof(f1372,plain,(
% 33.28/8.72 ~sQ62_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f1371])).
% 33.28/8.72 fof(f1377,plain,(
% 33.28/8.72 ![X0,X1]: (is_aligned(sk3,X0)|dissimilar(sk3,X1,X0)|~age(sk3,X1)=zero)),
% 33.28/8.72 inference(resolution,[status(thm)],[f437,f113])).
% 33.28/8.72 fof(f1421,plain,(
% 33.28/8.72 ![X0,X1]: (~age(sk3,X0)=zero|~greater(age(sk3,X1),sigma)|~age(sk3,X0)=zero|greater(age(sk3,X1),sigma))),
% 33.28/8.72 inference(resolution,[status(thm)],[f526,f138])).
% 33.28/8.72 fof(f1422,plain,(
% 33.28/8.72 ![X0,X1]: (~age(sk3,X0)=zero|~greater(age(sk3,X1),sigma)|~is_aligned(sk3,X0)|~is_aligned(sk3,X1))),
% 33.28/8.72 inference(resolution,[status(thm)],[f526,f85])).
% 33.28/8.72 fof(f1423,plain,(
% 33.28/8.72 ![X0,X1]: (~age(sk3,X0)=zero|~greater(age(sk3,X1),sigma)|is_aligned(sk3,X0)|is_aligned(sk3,X1))),
% 33.28/8.72 inference(resolution,[status(thm)],[f526,f83])).
% 33.28/8.72 fof(f1424,plain,(
% 33.28/8.72 ![X0,X1]: (~age(sk3,X0)=zero|~greater(age(sk3,X1),sigma)|organization(sk3))),
% 33.28/8.72 inference(resolution,[status(thm)],[f526,f81])).
% 33.28/8.72 fof(f1425,definition,(
% 33.28/8.72 ![X0]: (sQ63_spl <=> (~age(sk3,X0)=zero|~age(sk3,X0)=zero))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1426,plain,(
% 33.28/8.72 ![X0]: (~age(sk3,X0)=zero|~age(sk3,X0)=zero|~sQ63_spl)),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1425])).
% 33.28/8.72 fof(f1428,definition,(
% 33.28/8.72 ![X1]: (sQ64_spl <=> (~greater(age(sk3,X1),sigma)|greater(age(sk3,X1),sigma)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1431,plain,(
% 33.28/8.72 sQ63_spl|sQ64_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1421,f1425,f1428])).
% 33.28/8.72 fof(f1432,definition,(
% 33.28/8.72 ![X0]: (sQ65_spl <=> (~age(sk3,X0)=zero|~is_aligned(sk3,X0)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1433,plain,(
% 33.28/8.72 ![X0]: (~age(sk3,X0)=zero|~is_aligned(sk3,X0)|~sQ65_spl)),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1432])).
% 33.28/8.72 fof(f1435,definition,(
% 33.28/8.72 ![X1]: (sQ66_spl <=> (~greater(age(sk3,X1),sigma)|~is_aligned(sk3,X1)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1436,plain,(
% 33.28/8.72 ![X0]: (~greater(age(sk3,X0),sigma)|~is_aligned(sk3,X0)|~sQ66_spl)),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1435])).
% 33.28/8.72 fof(f1438,plain,(
% 33.28/8.72 sQ65_spl|sQ66_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1422,f1432,f1435])).
% 33.28/8.72 fof(f1439,definition,(
% 33.28/8.72 ![X0]: (sQ67_spl <=> (~age(sk3,X0)=zero|is_aligned(sk3,X0)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1442,definition,(
% 33.28/8.72 ![X1]: (sQ68_spl <=> (~greater(age(sk3,X1),sigma)|is_aligned(sk3,X1)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1443,plain,(
% 33.28/8.72 ![X0]: (~greater(age(sk3,X0),sigma)|is_aligned(sk3,X0)|~sQ68_spl)),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1442])).
% 33.28/8.72 fof(f1445,plain,(
% 33.28/8.72 sQ67_spl|sQ68_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1423,f1439,f1442])).
% 33.28/8.72 fof(f1446,definition,(
% 33.28/8.72 ![X0]: (sQ69_spl <=> (~age(sk3,X0)=zero))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1447,plain,(
% 33.28/8.72 ![X0]: (~age(sk3,X0)=zero|~sQ69_spl)),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1446])).
% 33.28/8.72 fof(f1449,definition,(
% 33.28/8.72 ![X1]: (sQ70_spl <=> (~greater(age(sk3,X1),sigma)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1450,plain,(
% 33.28/8.72 ![X0]: (~greater(age(sk3,X0),sigma)|~sQ70_spl)),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1449])).
% 33.28/8.72 fof(f1452,definition,(
% 33.28/8.72 sQ71_spl <=> (organization(sk3))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1455,plain,(
% 33.28/8.72 sQ69_spl|sQ70_spl|sQ71_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1424,f1446,f1449,f1452])).
% 33.28/8.72 fof(f1458,plain,(
% 33.28/8.72 ![X0]: (~age(sk3,X0)=zero|~sQ63_spl)),
% 33.28/8.72 inference(duplicate_literals_removal,[status(thm)],[f1426])).
% 33.28/8.72 fof(f1459,plain,(
% 33.28/8.72 $false|~sQ70_spl),
% 33.28/8.72 inference(backward_subsumption_resolution,[status(thm)],[f121,f1450])).
% 33.28/8.72 fof(f1461,plain,(
% 33.28/8.72 ~sQ70_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f1459])).
% 33.28/8.72 fof(f1462,plain,(
% 33.28/8.72 $false|~sQ69_spl),
% 33.28/8.72 inference(backward_subsumption_resolution,[status(thm)],[f116,f1447])).
% 33.28/8.72 fof(f1463,plain,(
% 33.28/8.72 $false|~sQ66_spl|~sQ68_spl),
% 33.28/8.72 inference(backward_subsumption_resolution,[status(thm)],[f121,f1464])).
% 33.28/8.72 fof(f1464,plain,(
% 33.28/8.72 ![X0]: (~greater(age(sk3,X0),sigma)|~sQ66_spl|~sQ68_spl)),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f1443,f1436])).
% 33.28/8.72 fof(f1465,plain,(
% 33.28/8.72 ~sQ69_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f1462])).
% 33.28/8.72 fof(f1466,plain,(
% 33.28/8.72 ~sQ66_spl|~sQ68_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f1463])).
% 33.28/8.72 fof(f1467,plain,(
% 33.28/8.72 sQ69_spl|~sQ63_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1458,f1446,f1425])).
% 33.28/8.72 fof(f1470,plain,(
% 33.28/8.72 smaller(sigma,age(sk3,sk6))|sigma=age(sk3,sk6)),
% 33.28/8.72 inference(resolution,[status(thm)],[f558,f70])).
% 33.28/8.72 fof(f1472,plain,(
% 33.28/8.72 ~smaller(age(sk3,sk6),sigma)),
% 33.28/8.72 inference(resolution,[status(thm)],[f558,f65])).
% 33.28/8.72 fof(f1473,definition,(
% 33.28/8.72 sQ72_spl <=> (smaller(sigma,age(sk3,sk6)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1476,plain,(
% 33.28/8.72 sQ72_spl|sQ51_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1470,f1473,f955])).
% 33.28/8.72 fof(f1504,plain,(
% 33.28/8.72 greater_or_equal(mod1,very_low)|~sQ61_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f1332,f171])).
% 33.28/8.72 fof(f1509,plain,(
% 33.28/8.72 mod1=very_low|greater_or_equal(mod1,very_low)),
% 33.28/8.72 inference(resolution,[status(thm)],[f1330,f226])).
% 33.28/8.72 fof(f1512,definition,(
% 33.28/8.72 sQ73_spl <=> (greater_or_equal(mod1,very_low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1515,plain,(
% 33.28/8.72 sQ62_spl|sQ73_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1509,f1334,f1512])).
% 33.28/8.72 fof(f1516,plain,(
% 33.28/8.72 greater(mod1,very_low)|mod1=very_low|~sQ61_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f1504,f62])).
% 33.28/8.72 fof(f1517,definition,(
% 33.28/8.72 sQ74_spl <=> (greater(mod1,very_low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1518,plain,(
% 33.28/8.72 greater(mod1,very_low)|~sQ74_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1517])).
% 33.28/8.72 fof(f1520,plain,(
% 33.28/8.72 sQ74_spl|sQ62_spl|~sQ61_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1516,f1517,f1334,f1331])).
% 33.28/8.72 fof(f1532,definition,(
% 33.28/8.72 sQ75_spl <=> (greater(very_low,low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1544,plain,(
% 33.28/8.72 sigma=age(sk3,sk6)|greater_or_equal(age(sk3,sk6),sigma)),
% 33.28/8.72 inference(resolution,[status(thm)],[f1014,f558])).
% 33.28/8.72 fof(f1566,definition,(
% 33.28/8.72 sQ77_spl <=> (greater_or_equal(age(sk3,sk6),sigma))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1569,plain,(
% 33.28/8.72 sQ51_spl|sQ77_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1544,f955,f1566])).
% 33.28/8.72 fof(f1588,plain,(
% 33.28/8.72 ![X0]: (~greater(X0,mod2)|very_low=X0|greater_or_equal(X0,very_low))),
% 33.28/8.72 inference(resolution,[status(thm)],[f1024,f1014])).
% 33.28/8.72 fof(f1589,plain,(
% 33.28/8.72 ![X0]: (~greater(X0,mod2)|smaller(very_low,X0)|very_low=X0)),
% 33.28/8.72 inference(resolution,[status(thm)],[f1024,f70])).
% 33.28/8.72 fof(f1592,plain,(
% 33.28/8.72 ~smaller(high,low)),
% 33.28/8.72 inference(resolution,[status(thm)],[f1022,f110])).
% 33.28/8.72 fof(f1598,plain,(
% 33.28/8.72 smaller(low,high)|low=high),
% 33.28/8.72 inference(resolution,[status(thm)],[f1592,f228])).
% 33.28/8.72 fof(f1600,plain,(
% 33.28/8.72 high=low|greater_or_equal(high,low)),
% 33.28/8.72 inference(resolution,[status(thm)],[f1592,f226])).
% 33.28/8.72 fof(f1601,definition,(
% 33.28/8.72 sQ78_spl <=> (smaller(low,high))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1602,plain,(
% 33.28/8.72 smaller(low,high)|~sQ78_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1601])).
% 33.28/8.72 fof(f1604,definition,(
% 33.28/8.72 sQ79_spl <=> (low=high)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1605,plain,(
% 33.28/8.72 low=high|~sQ79_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1604])).
% 33.28/8.72 fof(f1607,plain,(
% 33.28/8.72 sQ78_spl|sQ79_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1598,f1601,f1604])).
% 33.28/8.72 fof(f1609,definition,(
% 33.28/8.72 sQ80_spl <=> (greater_or_equal(high,low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1610,plain,(
% 33.28/8.72 greater_or_equal(high,low)|~sQ80_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1609])).
% 33.28/8.72 fof(f1612,plain,(
% 33.28/8.72 sQ79_spl|sQ80_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1600,f1604,f1609])).
% 33.28/8.72 fof(f1617,plain,(
% 33.28/8.72 ~smaller(mod1,high)|~sQ79_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f1605,f213])).
% 33.28/8.72 fof(f1663,plain,(
% 33.28/8.72 $false|~sQ79_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f1617,f148])).
% 33.28/8.72 fof(f1664,plain,(
% 33.28/8.72 ~sQ79_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f1663])).
% 33.28/8.72 fof(f1698,plain,(
% 33.28/8.72 ![X0]: (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|~organization(sk3)|has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2)),
% 33.28/8.72 inference(resolution,[status(thm)],[f633,f105])).
% 33.28/8.72 fof(f1699,plain,(
% 33.28/8.72 ![X0,X1]: (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|~organization(sk3)|is_aligned(sk3,X1)|dissimilar(sk3,X1,X0))),
% 33.28/8.72 inference(resolution,[status(thm)],[f633,f89])).
% 33.28/8.72 fof(f1700,plain,(
% 33.28/8.72 ![X0,X1]: (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|~organization(sk3)|is_aligned(sk3,X1)|dissimilar(sk3,X0,X1))),
% 33.28/8.72 inference(resolution,[status(thm)],[f633,f88])).
% 33.28/8.72 fof(f1701,definition,(
% 33.28/8.72 ![X0]: (sQ81_spl <=> (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1702,plain,(
% 33.28/8.72 ![X0]: (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2|~sQ81_spl)),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1701])).
% 33.28/8.72 fof(f1704,plain,(
% 33.28/8.72 sQ81_spl|~sQ71_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1698,f1701,f1452])).
% 33.28/8.72 fof(f1705,definition,(
% 33.28/8.72 ![X0,X1]: (sQ82_spl <=> (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|is_aligned(sk3,X1)|dissimilar(sk3,X1,X0)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1708,plain,(
% 33.28/8.72 sQ82_spl|~sQ71_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1699,f1705,f1452])).
% 33.28/8.72 fof(f1709,definition,(
% 33.28/8.72 ![X0,X1]: (sQ83_spl <=> (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|is_aligned(sk3,X1)|dissimilar(sk3,X0,X1)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1712,plain,(
% 33.28/8.72 sQ83_spl|~sQ71_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1700,f1709,f1452])).
% 33.28/8.72 fof(f1713,plain,(
% 33.28/8.72 ![X0]: (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|~sQ81_spl)),
% 33.28/8.72 inference(duplicate_literals_removal,[status(thm)],[f1702])).
% 33.28/8.72 fof(f1752,plain,(
% 33.28/8.72 ![X0]: (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero)),
% 33.28/8.72 inference(resolution,[status(thm)],[f636,f113])).
% 33.28/8.72 fof(f1772,plain,(
% 33.28/8.72 greater(high,low)|high=low|~sQ80_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f1610,f62])).
% 33.28/8.72 fof(f1773,definition,(
% 33.28/8.72 sQ84_spl <=> (greater(high,low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1774,plain,(
% 33.28/8.72 greater(high,low)|~sQ84_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1773])).
% 33.28/8.72 fof(f1776,plain,(
% 33.28/8.72 sQ84_spl|sQ79_spl|~sQ80_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1772,f1773,f1604,f1609])).
% 33.28/8.72 fof(f1778,plain,(
% 33.28/8.72 ~greater(low,high)|~sQ78_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f1602,f146])).
% 33.28/8.72 fof(f1796,definition,(
% 33.28/8.72 sQ85_spl <=> (greater(mod2,high))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1851,plain,(
% 33.28/8.72 ~greater(age(sk3,sk5),tau)|~sQ30_spl|~sQ5_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f973,f204])).
% 33.28/8.72 fof(f1859,definition,(
% 33.28/8.72 sQ88_spl <=> (greater(sigma,tau))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1889,definition,(
% 33.28/8.72 sQ89_spl <=> (greater(mod1,high))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1917,definition,(
% 33.28/8.72 sQ91_spl <=> (greater(very_low,mod2))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1970,definition,(
% 33.28/8.72 sQ94_spl <=> (greater(low,mod1))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1984,plain,(
% 33.28/8.72 smaller(age(sk3,sk5),tau)|age(sk3,sk5)=tau|~sQ30_spl|~sQ5_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f1851,f70])).
% 33.28/8.72 fof(f1987,definition,(
% 33.28/8.72 sQ96_spl <=> (age(sk3,sk5)=tau)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1988,plain,(
% 33.28/8.72 age(sk3,sk5)=tau|~sQ96_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f1987])).
% 33.28/8.72 fof(f1994,definition,(
% 33.28/8.72 sQ98_spl <=> (smaller(age(sk3,sk5),tau))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f1997,plain,(
% 33.28/8.72 sQ98_spl|sQ96_spl|~sQ30_spl|~sQ5_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1984,f1994,f1987,f495,f203])).
% 33.28/8.72 fof(f1999,plain,(
% 33.28/8.72 ~greater(tau,sigma)|~sQ96_spl|~sQ5_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f1988,f975])).
% 33.28/8.72 fof(f2027,plain,(
% 33.28/8.72 ~sQ30_spl|~sQ96_spl|~sQ5_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f1999,f495,f1987,f203])).
% 33.28/8.72 fof(f2053,plain,(
% 33.28/8.72 positional_advantage(sk3,sk7)),
% 33.28/8.72 inference(resolution,[status(thm)],[f752,f123])).
% 33.28/8.72 fof(f2057,plain,(
% 33.28/8.72 ![X0]: (positional_advantage(sk3,X0)|smaller(age(sk3,X0),tau)|age(sk3,X0)=tau)),
% 33.28/8.72 inference(resolution,[status(thm)],[f752,f70])).
% 33.28/8.72 fof(f2058,plain,(
% 33.28/8.72 ![X0,X1]: (positional_advantage(sk3,X0)|~greater(age(sk3,X0),X1)|~greater(X1,tau))),
% 33.28/8.72 inference(resolution,[status(thm)],[f752,f69])).
% 33.28/8.72 fof(f2059,plain,(
% 33.28/8.72 ![X0]: (positional_advantage(sk3,X0)|~smaller(tau,age(sk3,X0)))),
% 33.28/8.72 inference(resolution,[status(thm)],[f752,f65])).
% 33.28/8.72 fof(f2068,definition,(
% 33.28/8.72 sQ101_spl <=> (robust_position(sk3))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2070,plain,(
% 33.28/8.72 ~robust_position(sk3)|sQ101_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2068])).
% 33.28/8.72 fof(f2073,definition,(
% 33.28/8.72 sQ102_spl <=> (positional_advantage(sk3,sk5))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2074,plain,(
% 33.28/8.72 positional_advantage(sk3,sk5)|~sQ102_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2073])).
% 33.28/8.72 fof(f2077,definition,(
% 33.28/8.72 sQ103_spl <=> (positional_advantage(sk3,sk4))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2078,plain,(
% 33.28/8.72 positional_advantage(sk3,sk4)|~sQ103_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2077])).
% 33.28/8.72 fof(f2082,plain,(
% 33.28/8.72 ~organization(sk3)|has_immunity(sk3,sk7)|is_aligned(sk3,sk7)|hazard_of_mortality(sk3,sk7)=mod1),
% 33.28/8.72 inference(resolution,[status(thm)],[f2053,f104])).
% 33.28/8.72 fof(f2083,plain,(
% 33.28/8.72 ~robust_position(sk3)|~smaller_or_equal(age(sk3,sk7),tau)),
% 33.28/8.72 inference(resolution,[status(thm)],[f2053,f96])).
% 33.28/8.72 fof(f2084,definition,(
% 33.28/8.72 sQ104_spl <=> (has_immunity(sk3,sk7))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2085,plain,(
% 33.28/8.72 has_immunity(sk3,sk7)|~sQ104_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2084])).
% 33.28/8.72 fof(f2087,definition,(
% 33.28/8.72 sQ105_spl <=> (is_aligned(sk3,sk7))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2088,plain,(
% 33.28/8.72 is_aligned(sk3,sk7)|~sQ105_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2087])).
% 33.28/8.72 fof(f2090,definition,(
% 33.28/8.72 sQ106_spl <=> (hazard_of_mortality(sk3,sk7)=low)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2091,plain,(
% 33.28/8.72 hazard_of_mortality(sk3,sk7)=low|~sQ106_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2090])).
% 33.28/8.72 fof(f2094,definition,(
% 33.28/8.72 sQ107_spl <=> (hazard_of_mortality(sk3,sk7)=mod1)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2095,plain,(
% 33.28/8.72 hazard_of_mortality(sk3,sk7)=mod1|~sQ107_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2094])).
% 33.28/8.72 fof(f2097,plain,(
% 33.28/8.72 ~sQ71_spl|sQ104_spl|sQ105_spl|sQ107_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2082,f1452,f2084,f2087,f2094])).
% 33.28/8.72 fof(f2098,definition,(
% 33.28/8.72 sQ108_spl <=> (smaller_or_equal(age(sk3,sk7),tau))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2101,plain,(
% 33.28/8.72 ~sQ101_spl|~sQ108_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2083,f2068,f2098])).
% 33.28/8.72 fof(f2102,plain,(
% 33.28/8.72 low=mod1|~sQ106_spl|~sQ107_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f2091,f2095])).
% 33.28/8.72 fof(f2103,plain,(
% 33.28/8.72 $false|sQ101_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f2070,f114])).
% 33.28/8.72 fof(f2104,plain,(
% 33.28/8.72 sQ101_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f2103])).
% 33.28/8.72 fof(f2105,plain,(
% 33.28/8.72 sQ14_spl|~sQ106_spl|~sQ107_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2102,f253,f2090,f2094])).
% 33.28/8.72 fof(f2108,plain,(
% 33.28/8.72 ~robust_position(sk3)|~smaller_or_equal(age(sk3,sk4),tau)|~sQ103_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2078,f96])).
% 33.28/8.72 fof(f2109,definition,(
% 33.28/8.72 sQ109_spl <=> (has_immunity(sk3,sk4))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2110,plain,(
% 33.28/8.72 has_immunity(sk3,sk4)|~sQ109_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2109])).
% 33.28/8.72 fof(f2111,plain,(
% 33.28/8.72 ~has_immunity(sk3,sk4)|sQ109_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2109])).
% 33.28/8.72 fof(f2112,definition,(
% 33.28/8.72 sQ110_spl <=> (is_aligned(sk3,sk4))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2113,plain,(
% 33.28/8.72 is_aligned(sk3,sk4)|~sQ110_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2112])).
% 33.28/8.72 fof(f2123,definition,(
% 33.28/8.72 sQ113_spl <=> (smaller_or_equal(age(sk3,sk4),tau))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2125,plain,(
% 33.28/8.72 ~smaller_or_equal(age(sk3,sk4),tau)|sQ113_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2123])).
% 33.28/8.72 fof(f2126,plain,(
% 33.28/8.72 ~sQ101_spl|~sQ113_spl|~sQ103_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2108,f2068,f2123,f2077])).
% 33.28/8.72 fof(f2127,plain,(
% 33.28/8.72 ~smaller_or_equal(zero,tau)|sQ113_spl),
% 33.28/8.72 inference(forward_demodulation,[status(thm)],[f116,f2125])).
% 33.28/8.72 fof(f2133,plain,(
% 33.28/8.72 ~robust_position(sk3)|~smaller_or_equal(age(sk3,sk5),tau)|~sQ102_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2074,f96])).
% 33.28/8.72 fof(f2134,definition,(
% 33.28/8.72 sQ114_spl <=> (has_immunity(sk3,sk5))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2135,plain,(
% 33.28/8.72 has_immunity(sk3,sk5)|~sQ114_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2134])).
% 33.28/8.72 fof(f2137,definition,(
% 33.28/8.72 sQ115_spl <=> (is_aligned(sk3,sk5))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2138,plain,(
% 33.28/8.72 is_aligned(sk3,sk5)|~sQ115_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2137])).
% 33.28/8.72 fof(f2139,plain,(
% 33.28/8.72 ~is_aligned(sk3,sk5)|sQ115_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2137])).
% 33.28/8.72 fof(f2144,definition,(
% 33.28/8.72 sQ117_spl <=> (hazard_of_mortality(sk3,sk5)=mod1)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2145,plain,(
% 33.28/8.72 hazard_of_mortality(sk3,sk5)=mod1|~sQ117_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2144])).
% 33.28/8.72 fof(f2148,definition,(
% 33.28/8.72 sQ118_spl <=> (smaller_or_equal(age(sk3,sk5),tau))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2150,plain,(
% 33.28/8.72 ~smaller_or_equal(age(sk3,sk5),tau)|sQ118_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2148])).
% 33.28/8.72 fof(f2151,plain,(
% 33.28/8.72 ~sQ101_spl|~sQ118_spl|~sQ102_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2133,f2068,f2148,f2073])).
% 33.28/8.72 fof(f2152,plain,(
% 33.28/8.72 ~smaller_or_equal(sigma,tau)|~sQ6_spl|sQ118_spl),
% 33.28/8.72 inference(forward_demodulation,[status(thm)],[f207,f2150])).
% 33.28/8.72 fof(f2157,plain,(
% 33.28/8.72 ~organization(sk3)|has_endowment(sk3)|~sQ104_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2085,f79])).
% 33.28/8.72 fof(f2158,definition,(
% 33.28/8.72 sQ119_spl <=> (hazard_of_mortality(sk3,sk7)=very_low)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2159,plain,(
% 33.28/8.72 hazard_of_mortality(sk3,sk7)=very_low|~sQ119_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2158])).
% 33.28/8.72 fof(f2162,definition,(
% 33.28/8.72 sQ120_spl <=> (has_endowment(sk3))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2163,plain,(
% 33.28/8.72 has_endowment(sk3)|~sQ120_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2162])).
% 33.28/8.72 fof(f2165,plain,(
% 33.28/8.72 ~sQ71_spl|sQ120_spl|~sQ104_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2157,f1452,f2162,f2084])).
% 33.28/8.72 fof(f2167,plain,(
% 33.28/8.72 $false|~sQ120_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f2163,f115])).
% 33.28/8.72 fof(f2168,plain,(
% 33.28/8.72 ~sQ120_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f2167])).
% 33.28/8.72 fof(f2169,plain,(
% 33.28/8.72 very_low=mod1|~sQ119_spl|~sQ107_spl),
% 33.28/8.72 inference(forward_demodulation,[status(thm)],[f2159,f2095])).
% 33.28/8.72 fof(f2170,plain,(
% 33.28/8.72 $false|sQ62_spl|~sQ119_spl|~sQ107_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f2169,f1336])).
% 33.28/8.72 fof(f2171,plain,(
% 33.28/8.72 sQ62_spl|~sQ119_spl|~sQ107_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f2170])).
% 33.28/8.72 fof(f2175,plain,(
% 33.28/8.72 ~organization(sk3)|has_endowment(sk3)|~sQ109_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2110,f79])).
% 33.28/8.72 fof(f2180,plain,(
% 33.28/8.72 ~sQ71_spl|sQ120_spl|~sQ109_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2175,f1452,f2162,f2109])).
% 33.28/8.72 fof(f2183,plain,(
% 33.28/8.72 ~smaller(zero,tau)|sQ113_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2127,f60])).
% 33.28/8.72 fof(f2184,plain,(
% 33.28/8.72 $false|sQ113_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f2183,f139])).
% 33.28/8.72 fof(f2185,plain,(
% 33.28/8.72 sQ113_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f2184])).
% 33.28/8.72 fof(f2188,plain,(
% 33.28/8.72 ~organization(sk3)|has_endowment(sk3)|~sQ114_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2135,f79])).
% 33.28/8.72 fof(f2189,definition,(
% 33.28/8.72 sQ122_spl <=> (hazard_of_mortality(sk3,sk5)=very_low)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2190,plain,(
% 33.28/8.72 hazard_of_mortality(sk3,sk5)=very_low|~sQ122_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2189])).
% 33.28/8.72 fof(f2191,plain,(
% 33.28/8.72 ~hazard_of_mortality(sk3,sk5)=very_low|sQ122_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2189])).
% 33.28/8.72 fof(f2193,plain,(
% 33.28/8.72 ~sQ71_spl|sQ120_spl|~sQ114_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2188,f1452,f2162,f2134])).
% 33.28/8.72 fof(f2196,plain,(
% 33.28/8.72 ~smaller(mod1,hazard_of_mortality(sk3,sk5))|~sQ107_spl|sQ0_spl),
% 33.28/8.72 inference(forward_demodulation,[status(thm)],[f2095,f127])).
% 33.28/8.72 fof(f2198,plain,(
% 33.28/8.72 ~smaller(very_low,hazard_of_mortality(sk3,sk6))|~sQ122_spl|sQ1_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f2190,f130])).
% 33.28/8.72 fof(f2203,plain,(
% 33.28/8.72 very_low=hazard_of_mortality(sk3,sk6)|greater_or_equal(very_low,hazard_of_mortality(sk3,sk6))|~sQ122_spl|sQ1_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2198,f226])).
% 33.28/8.72 fof(f2204,definition,(
% 33.28/8.72 sQ123_spl <=> (smaller(hazard_of_mortality(sk3,sk6),very_low))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2205,plain,(
% 33.28/8.72 smaller(hazard_of_mortality(sk3,sk6),very_low)|~sQ123_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2204])).
% 33.28/8.72 fof(f2206,plain,(
% 33.28/8.72 ~smaller(hazard_of_mortality(sk3,sk6),very_low)|sQ123_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2204])).
% 33.28/8.72 fof(f2207,definition,(
% 33.28/8.72 sQ124_spl <=> (hazard_of_mortality(sk3,sk6)=very_low)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2208,plain,(
% 33.28/8.72 hazard_of_mortality(sk3,sk6)=very_low|~sQ124_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2207])).
% 33.28/8.72 fof(f2212,definition,(
% 33.28/8.72 sQ125_spl <=> (greater_or_equal(very_low,hazard_of_mortality(sk3,sk6)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2213,plain,(
% 33.28/8.72 greater_or_equal(very_low,hazard_of_mortality(sk3,sk6))|~sQ125_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2212])).
% 33.28/8.72 fof(f2214,plain,(
% 33.28/8.72 ~greater_or_equal(very_low,hazard_of_mortality(sk3,sk6))|sQ125_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2212])).
% 33.28/8.72 fof(f2215,plain,(
% 33.28/8.72 sQ124_spl|sQ125_spl|~sQ122_spl|sQ1_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2203,f2207,f2212,f2189,f128])).
% 33.28/8.72 fof(f2217,plain,(
% 33.28/8.72 smaller(very_low,very_low)|~sQ124_spl|~sQ123_spl),
% 33.28/8.72 inference(forward_demodulation,[status(thm)],[f2208,f2205])).
% 33.28/8.72 fof(f2218,plain,(
% 33.28/8.72 $false|~sQ124_spl|~sQ123_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f2217,f928])).
% 33.28/8.72 fof(f2219,plain,(
% 33.28/8.72 ~sQ124_spl|~sQ123_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f2218])).
% 33.28/8.72 fof(f2223,plain,(
% 33.28/8.72 mod1=hazard_of_mortality(sk3,sk5)|greater_or_equal(mod1,hazard_of_mortality(sk3,sk5))|~sQ107_spl|sQ0_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2196,f226])).
% 33.28/8.72 fof(f2229,definition,(
% 33.28/8.72 sQ127_spl <=> (greater_or_equal(mod1,hazard_of_mortality(sk3,sk5)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2230,plain,(
% 33.28/8.72 greater_or_equal(mod1,hazard_of_mortality(sk3,sk5))|~sQ127_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2229])).
% 33.28/8.72 fof(f2231,plain,(
% 33.28/8.72 ~greater_or_equal(mod1,hazard_of_mortality(sk3,sk5))|sQ127_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2229])).
% 33.28/8.72 fof(f2232,plain,(
% 33.28/8.72 sQ117_spl|sQ127_spl|~sQ107_spl|sQ0_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2223,f2144,f2229,f2094,f125])).
% 33.28/8.72 fof(f2233,plain,(
% 33.28/8.72 smaller(mod1,hazard_of_mortality(sk3,sk5))|~sQ107_spl|~sQ0_spl),
% 33.28/8.72 inference(forward_demodulation,[status(thm)],[f2095,f126])).
% 33.28/8.72 fof(f2234,plain,(
% 33.28/8.72 ~smaller(sigma,tau)|~sQ6_spl|sQ118_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2152,f60])).
% 33.28/8.72 fof(f2235,plain,(
% 33.28/8.72 $false|~sQ6_spl|sQ118_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f2234,f119])).
% 33.28/8.72 fof(f2236,plain,(
% 33.28/8.72 ~sQ6_spl|sQ118_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f2235])).
% 33.28/8.72 fof(f2240,definition,(
% 33.28/8.72 sQ128_spl <=> (positional_advantage(sk3,sk7))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2243,definition,(
% 33.28/8.72 sQ129_spl <=> (hazard_of_mortality(sk3,sk7)=high)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2244,plain,(
% 33.28/8.72 hazard_of_mortality(sk3,sk7)=high|~sQ129_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2243])).
% 33.28/8.72 fof(f2247,definition,(
% 33.28/8.72 sQ130_spl <=> (age(sk3,sk7)=zero)),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2248,plain,(
% 33.28/8.72 age(sk3,sk7)=zero|~sQ130_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2247])).
% 33.28/8.72 fof(f2251,plain,(
% 33.28/8.72 high=mod1|~sQ129_spl|~sQ107_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f2244,f2095])).
% 33.28/8.72 fof(f2252,plain,(
% 33.28/8.72 sQ16_spl|~sQ129_spl|~sQ107_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2251,f260,f2243,f2094])).
% 33.28/8.72 fof(f2263,definition,(
% 33.28/8.72 sQ131_spl <=> (has_immunity(sk3,sk2(sk3)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2264,plain,(
% 33.28/8.72 has_immunity(sk3,sk2(sk3))|~sQ131_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2263])).
% 33.28/8.72 fof(f2281,plain,(
% 33.28/8.72 ~greater(mod1,hazard_of_mortality(sk3,sk5))|~sQ107_spl|~sQ0_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2233,f146])).
% 33.28/8.72 fof(f2283,plain,(
% 33.28/8.72 smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk5))|hazard_of_mortality(sk3,sk6)=hazard_of_mortality(sk3,sk5)|sQ1_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f130,f228])).
% 33.28/8.72 fof(f2286,definition,(
% 33.28/8.72 sQ135_spl <=> (smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk5)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2287,plain,(
% 33.28/8.72 smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk5))|~sQ135_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2286])).
% 33.28/8.72 fof(f2288,plain,(
% 33.28/8.72 ~smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk5))|sQ135_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2286])).
% 33.28/8.72 fof(f2289,definition,(
% 33.28/8.72 sQ136_spl <=> (hazard_of_mortality(sk3,sk6)=hazard_of_mortality(sk3,sk5))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2290,plain,(
% 33.28/8.72 hazard_of_mortality(sk3,sk6)=hazard_of_mortality(sk3,sk5)|~sQ136_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2289])).
% 33.28/8.72 fof(f2291,plain,(
% 33.28/8.72 ~hazard_of_mortality(sk3,sk6)=hazard_of_mortality(sk3,sk5)|sQ136_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2289])).
% 33.28/8.72 fof(f2292,plain,(
% 33.28/8.72 sQ135_spl|sQ136_spl|sQ1_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2283,f2286,f2289,f128])).
% 33.28/8.72 fof(f2298,plain,(
% 33.28/8.72 ~hazard_of_mortality(sk3,sk6)=very_low|~sQ136_spl|sQ122_spl),
% 33.28/8.72 inference(backward_demodulation,[status(thm)],[f2290,f2191])).
% 33.28/8.72 fof(f2303,plain,(
% 33.28/8.72 smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk6))|~sQ136_spl|~sQ135_spl),
% 33.28/8.72 inference(forward_demodulation,[status(thm)],[f2290,f2287])).
% 33.28/8.72 fof(f2304,plain,(
% 33.28/8.72 $false|~sQ136_spl|~sQ135_spl),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f2303,f928])).
% 33.28/8.72 fof(f2305,plain,(
% 33.28/8.72 ~sQ136_spl|~sQ135_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f2304])).
% 33.28/8.72 fof(f2309,plain,(
% 33.28/8.72 ~organization(sk3)|has_endowment(sk3)|~sQ131_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2264,f79])).
% 33.28/8.72 fof(f2314,plain,(
% 33.28/8.72 ~sQ71_spl|sQ120_spl|~sQ131_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2309,f1452,f2162,f2263])).
% 33.28/8.72 fof(f2357,plain,(
% 33.28/8.72 ~greater(very_low,low)|~greater(very_low,low)),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f109])).
% 33.28/8.72 fof(f2359,plain,(
% 33.28/8.72 ~greater(low,mod1)|~greater(low,mod1)),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f108])).
% 33.28/8.72 fof(f2361,plain,(
% 33.28/8.72 ~greater(very_low,mod1)|~greater(very_low,mod1)|~sQ74_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f1518])).
% 33.28/8.72 fof(f2365,plain,(
% 33.28/8.72 ~greater(sigma,tau)|~greater(sigma,tau)|~sQ30_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f496])).
% 33.28/8.72 fof(f2367,plain,(
% 33.28/8.72 ~greater(zero,tau)|~greater(zero,tau)),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f118])).
% 33.28/8.72 fof(f2369,plain,(
% 33.28/8.72 ~greater(low,mod2)|~greater(low,mod2)),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f111])).
% 33.28/8.72 fof(f2371,plain,(
% 33.28/8.72 ~greater(mod1,mod2)|~greater(mod1,mod2)),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f112])).
% 33.28/8.72 fof(f2373,plain,(
% 33.28/8.72 ~greater(very_low,mod2)|~greater(very_low,mod2)|~sQ59_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f1248])).
% 33.28/8.72 fof(f2375,plain,(
% 33.28/8.72 ~greater(low,high)|~greater(low,high)|~sQ84_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f1774])).
% 33.28/8.72 fof(f2377,plain,(
% 33.28/8.72 ~greater(mod1,high)|~greater(mod1,high)),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f107])).
% 33.28/8.72 fof(f2379,plain,(
% 33.28/8.72 ~greater(mod2,high)|~greater(mod2,high)),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f110])).
% 33.28/8.72 fof(f2381,plain,(
% 33.28/8.72 ~greater(sigma,age(sk3,sk6))|~greater(sigma,age(sk3,sk6))),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f121])).
% 33.28/8.72 fof(f2383,plain,(
% 33.28/8.72 ~greater(tau,age(sk3,sk7))|~greater(tau,age(sk3,sk7))),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f123])).
% 33.28/8.72 fof(f2389,plain,(
% 33.28/8.72 ~greater(zero,sigma)|~greater(zero,sigma)),
% 33.28/8.72 inference(resolution,[status(thm)],[f907,f117])).
% 33.28/8.72 fof(f2446,plain,(
% 33.28/8.72 ~sQ75_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2357,f1532])).
% 33.28/8.72 fof(f2447,plain,(
% 33.28/8.72 ~sQ94_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2359,f1970])).
% 33.28/8.72 fof(f2448,definition,(
% 33.28/8.72 sQ139_spl <=> (greater(very_low,mod1))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2451,plain,(
% 33.28/8.72 ~sQ139_spl|~sQ74_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2361,f2448,f1517])).
% 33.28/8.72 fof(f2456,plain,(
% 33.28/8.72 ~sQ88_spl|~sQ30_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2365,f1859,f495])).
% 33.28/8.72 fof(f2457,plain,(
% 33.28/8.72 ~sQ49_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2367,f878])).
% 33.28/8.72 fof(f2458,definition,(
% 33.28/8.72 sQ141_spl <=> (greater(low,mod2))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2461,plain,(
% 33.28/8.72 ~sQ141_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2369,f2458])).
% 33.28/8.72 fof(f2462,definition,(
% 33.28/8.72 sQ142_spl <=> (greater(mod1,mod2))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2465,plain,(
% 33.28/8.72 ~sQ142_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2371,f2462])).
% 33.28/8.72 fof(f2466,plain,(
% 33.28/8.72 ~sQ91_spl|~sQ59_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2373,f1917,f1247])).
% 33.28/8.72 fof(f2467,definition,(
% 33.28/8.72 sQ143_spl <=> (greater(low,high))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2470,plain,(
% 33.28/8.72 ~sQ143_spl|~sQ84_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2375,f2467,f1773])).
% 33.28/8.72 fof(f2471,plain,(
% 33.28/8.72 ~sQ89_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2377,f1889])).
% 33.28/8.72 fof(f2472,plain,(
% 33.28/8.72 ~sQ85_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2379,f1796])).
% 33.28/8.72 fof(f2473,definition,(
% 33.28/8.72 sQ144_spl <=> (greater(sigma,age(sk3,sk6)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2476,plain,(
% 33.28/8.72 ~sQ144_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2381,f2473])).
% 33.28/8.72 fof(f2477,definition,(
% 33.28/8.72 sQ145_spl <=> (greater(tau,age(sk3,sk7)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2480,plain,(
% 33.28/8.72 ~sQ145_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2383,f2477])).
% 33.28/8.72 fof(f2483,plain,(
% 33.28/8.72 ~sQ52_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2389,f981])).
% 33.28/8.72 fof(f2511,plain,(
% 33.28/8.72 greater(very_low,hazard_of_mortality(sk3,sk6))|very_low=hazard_of_mortality(sk3,sk6)|~sQ125_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2213,f62])).
% 33.28/8.72 fof(f2512,definition,(
% 33.28/8.72 sQ146_spl <=> (greater(very_low,hazard_of_mortality(sk3,sk6)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2513,plain,(
% 33.28/8.72 greater(very_low,hazard_of_mortality(sk3,sk6))|~sQ146_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2512])).
% 33.28/8.72 fof(f2515,plain,(
% 33.28/8.72 sQ146_spl|sQ124_spl|~sQ125_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2511,f2512,f2207,f2212])).
% 33.28/8.72 fof(f2516,plain,(
% 33.28/8.72 greater(mod1,hazard_of_mortality(sk3,sk5))|mod1=hazard_of_mortality(sk3,sk5)|~sQ127_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2230,f62])).
% 33.28/8.72 fof(f2517,definition,(
% 33.28/8.72 sQ147_spl <=> (greater(mod1,hazard_of_mortality(sk3,sk5)))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 33.28/8.72 fof(f2518,plain,(
% 33.28/8.72 greater(mod1,hazard_of_mortality(sk3,sk5))|~sQ147_spl),
% 33.28/8.72 inference(component_clause,[status(thm)],[f2517])).
% 33.28/8.72 fof(f2520,plain,(
% 33.28/8.72 sQ147_spl|sQ117_spl|~sQ127_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2516,f2517,f2144,f2229])).
% 33.28/8.72 fof(f2540,plain,(
% 33.28/8.72 ~greater(hazard_of_mortality(sk3,sk6),mod2)|~sQ146_spl),
% 33.28/8.72 inference(resolution,[status(thm)],[f2513,f1024])).
% 33.28/8.72 fof(f2577,plain,(
% 33.28/8.72 ~sQ124_spl|~sQ136_spl|sQ122_spl),
% 33.28/8.72 inference(split_clause,[status(thm)],[f2298,f2207,f2289,f2189])).
% 33.28/8.72 fof(f2617,plain,(
% 33.28/8.72 ![X0]: (~greater(sigma,X0)|~smaller(tau,X0)|~sQ30_spl)),
% 33.28/8.72 inference(resolution,[status(thm)],[f909,f496])).
% 33.28/8.72 fof(f2618,plain,(
% 33.28/8.72 ![X0]: (~greater(zero,X0)|~smaller(tau,X0))),
% 33.28/8.72 inference(resolution,[status(thm)],[f909,f118])).
% 33.28/8.72 fof(f2629,plain,(
% 33.28/8.72 ![X0]: (~greater(zero,X0)|~smaller(sigma,X0))),
% 33.28/8.72 inference(resolution,[status(thm)],[f909,f117])).
% 33.28/8.72 fof(f2630,plain,(
% 33.28/8.72 ![X0,X1,X2]: (~greater(X0,X1)|~smaller(X2,X1)|X2=X0|greater_or_equal(X0,X2))),
% 33.28/8.72 inference(resolution,[status(thm)],[f909,f1014])).
% 33.28/8.72 fof(f2633,plain,(
% 33.28/8.72 ![X0,X1,X2]: (~greater(X0,X1)|~smaller(X2,X1)|~smaller(X0,X2))),
% 33.28/8.72 inference(resolution,[status(thm)],[f909,f65])).
% 33.28/8.72 fof(f2671,plain,(
% 33.28/8.72 ![X0]: (~smaller(tau,X0)|~smaller(X0,sigma)|~sQ30_spl)),
% 33.28/8.72 inference(resolution,[status(thm)],[f2617,f65])).
% 33.28/8.72 fof(f2675,plain,(
% 33.28/8.72 ![X0]: (~smaller(tau,X0)|~smaller(X0,zero))),
% 33.28/8.72 inference(resolution,[status(thm)],[f2618,f65])).
% 33.28/8.72 fof(f2685,plain,(
% 33.28/8.72 ![X0]: (~smaller(sigma,X0)|zero=X0|greater_or_equal(X0,zero))),
% 33.28/8.72 inference(resolution,[status(thm)],[f2629,f1014])).
% 33.28/8.72 fof(f2686,plain,(
% 33.28/8.72 ![X0]: (~smaller(sigma,X0)|smaller(zero,X0)|zero=X0)),
% 33.28/8.72 inference(resolution,[status(thm)],[f2629,f70])).
% 33.28/8.72 fof(f3034,plain,(
% 33.28/8.72 ![X0]: (~age(sk3,X0)=zero|is_aligned(sk3,X0))),
% 33.28/8.72 inference(resolution,[status(thm)],[f92,f113])).
% 33.28/8.72 fof(f3036,plain,(
% 33.28/8.72 $false|~sQ65_spl),
% 33.28/8.72 inference(backward_subsumption_resolution,[status(thm)],[f116,f3037])).
% 33.28/8.72 fof(f3037,plain,(
% 33.28/8.72 ![X0]: (~age(sk3,X0)=zero|~sQ65_spl)),
% 33.28/8.72 inference(forward_subsumption_resolution,[status(thm)],[f3034,f1433])).
% 33.28/8.72 fof(f3038,plain,(
% 33.28/8.72 ~sQ65_spl),
% 33.28/8.72 inference(contradiction_clause,[status(thm)],[f3036])).
% 33.28/8.72 fof(f3210,plain,(
% 33.28/8.72 ![X0]: (~smaller_or_equal(age(sk3,X0),tau)|~positional_advantage(sk3,X0))),
% 33.28/8.72 inference(resolution,[status(thm)],[f96,f114])).
% 33.28/8.72 fof(f3269,definition,(
% 33.28/8.72 sQ174_spl <=> (smaller(tau,zero))),
% 33.28/8.72 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3283,plain,(
% 33.28/8.73 ~smaller(age(sk3,sk7),zero)),
% 33.28/8.73 inference(resolution,[status(thm)],[f443,f2675])).
% 33.28/8.73 fof(f3284,plain,(
% 33.28/8.73 ~smaller(age(sk3,sk7),sigma)|~sQ30_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f443,f2671])).
% 33.28/8.73 fof(f3378,plain,(
% 33.28/8.73 smaller(zero,age(sk3,sk7))|zero=age(sk3,sk7)),
% 33.28/8.73 inference(resolution,[status(thm)],[f3283,f228])).
% 33.28/8.73 fof(f3380,plain,(
% 33.28/8.73 age(sk3,sk7)=zero|greater_or_equal(age(sk3,sk7),zero)),
% 33.28/8.73 inference(resolution,[status(thm)],[f3283,f226])).
% 33.28/8.73 fof(f3381,definition,(
% 33.28/8.73 sQ175_spl <=> (smaller(zero,age(sk3,sk7)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3382,plain,(
% 33.28/8.73 smaller(zero,age(sk3,sk7))|~sQ175_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3381])).
% 33.28/8.73 fof(f3384,plain,(
% 33.28/8.73 sQ175_spl|sQ130_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3378,f3381,f2247])).
% 33.28/8.73 fof(f3386,definition,(
% 33.28/8.73 sQ176_spl <=> (greater_or_equal(age(sk3,sk7),zero))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3389,plain,(
% 33.28/8.73 sQ130_spl|sQ176_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3380,f2247,f3386])).
% 33.28/8.73 fof(f3391,plain,(
% 33.28/8.73 smaller(sigma,age(sk3,sk7))|sigma=age(sk3,sk7)|~sQ30_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3284,f228])).
% 33.28/8.73 fof(f3394,definition,(
% 33.28/8.73 sQ177_spl <=> (smaller(sigma,age(sk3,sk7)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3395,plain,(
% 33.28/8.73 smaller(sigma,age(sk3,sk7))|~sQ177_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3394])).
% 33.28/8.73 fof(f3397,definition,(
% 33.28/8.73 sQ178_spl <=> (sigma=age(sk3,sk7))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3398,plain,(
% 33.28/8.73 sigma=age(sk3,sk7)|~sQ178_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3397])).
% 33.28/8.73 fof(f3400,plain,(
% 33.28/8.73 sQ177_spl|sQ178_spl|~sQ30_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3391,f3394,f3397,f495])).
% 33.28/8.73 fof(f3402,definition,(
% 33.28/8.73 sQ179_spl <=> (greater_or_equal(age(sk3,sk7),sigma))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3403,plain,(
% 33.28/8.73 greater_or_equal(age(sk3,sk7),sigma)|~sQ179_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3402])).
% 33.28/8.73 fof(f3409,plain,(
% 33.28/8.73 ~greater(tau,sigma)|~sQ178_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f3398,f442])).
% 33.28/8.73 fof(f3452,plain,(
% 33.28/8.73 ~greater(sigma,age(sk3,sk7))|~sQ177_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3395,f146])).
% 33.28/8.73 fof(f3453,plain,(
% 33.28/8.73 greater(age(sk3,sk7),sigma)|age(sk3,sk7)=sigma|~sQ179_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3403,f62])).
% 33.28/8.73 fof(f3454,definition,(
% 33.28/8.73 sQ182_spl <=> (greater(age(sk3,sk7),sigma))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3455,plain,(
% 33.28/8.73 greater(age(sk3,sk7),sigma)|~sQ182_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3454])).
% 33.28/8.73 fof(f3457,plain,(
% 33.28/8.73 sQ182_spl|sQ178_spl|~sQ179_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3453,f3454,f3397,f3402])).
% 33.28/8.73 fof(f3534,definition,(
% 33.28/8.73 sQ184_spl <=> (greater(age(sk3,sk7),zero))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3535,plain,(
% 33.28/8.73 greater(age(sk3,sk7),zero)|~sQ184_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3534])).
% 33.28/8.73 fof(f3538,plain,(
% 33.28/8.73 greater_or_equal(age(sk3,sk7),zero)|~sQ175_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3382,f171])).
% 33.28/8.73 fof(f3540,plain,(
% 33.28/8.73 sigma=age(sk3,sk7)|greater_or_equal(age(sk3,sk7),sigma)|~sQ177_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3452,f1014])).
% 33.28/8.73 fof(f3544,plain,(
% 33.28/8.73 sQ178_spl|sQ179_spl|~sQ177_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3540,f3397,f3402,f3394])).
% 33.28/8.73 fof(f3548,plain,(
% 33.28/8.73 ~greater(sigma,age(sk3,sk7))|~greater(sigma,age(sk3,sk7))|~sQ182_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3455,f907])).
% 33.28/8.73 fof(f3557,definition,(
% 33.28/8.73 sQ185_spl <=> (greater(sigma,age(sk3,sk7)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3560,plain,(
% 33.28/8.73 ~sQ185_spl|~sQ182_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3548,f3557,f3454])).
% 33.28/8.73 fof(f3722,plain,(
% 33.28/8.73 ~greater(zero,age(sk3,sk7))|~greater(zero,age(sk3,sk7))|~sQ184_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3535,f907])).
% 33.28/8.73 fof(f3731,definition,(
% 33.28/8.73 sQ190_spl <=> (greater(zero,age(sk3,sk7)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3734,plain,(
% 33.28/8.73 ~sQ190_spl|~sQ184_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3722,f3731,f3534])).
% 33.28/8.73 fof(f3760,plain,(
% 33.28/8.73 ![X0]: (~age(sk3,X0)=zero|~organization(sk3)|has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2)),
% 33.28/8.73 inference(resolution,[status(thm)],[f3034,f105])).
% 33.28/8.73 fof(f3761,plain,(
% 33.28/8.73 ![X0,X1]: (~age(sk3,X0)=zero|~organization(sk3)|is_aligned(sk3,X1)|dissimilar(sk3,X1,X0))),
% 33.28/8.73 inference(resolution,[status(thm)],[f3034,f89])).
% 33.28/8.73 fof(f3762,plain,(
% 33.28/8.73 ![X0,X1]: (~age(sk3,X0)=zero|~organization(sk3)|is_aligned(sk3,X1)|dissimilar(sk3,X0,X1))),
% 33.28/8.73 inference(resolution,[status(thm)],[f3034,f88])).
% 33.28/8.73 fof(f3763,definition,(
% 33.28/8.73 ![X0]: (sQ192_spl <=> (~age(sk3,X0)=zero|has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3766,plain,(
% 33.28/8.73 sQ192_spl|~sQ71_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3760,f3763,f1452])).
% 33.28/8.73 fof(f3767,definition,(
% 33.28/8.73 ![X0,X1]: (sQ193_spl <=> (~age(sk3,X0)=zero|is_aligned(sk3,X1)|dissimilar(sk3,X1,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3770,plain,(
% 33.28/8.73 sQ193_spl|~sQ71_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3761,f3767,f1452])).
% 33.28/8.73 fof(f3771,definition,(
% 33.28/8.73 ![X0,X1]: (sQ194_spl <=> (~age(sk3,X0)=zero|is_aligned(sk3,X1)|dissimilar(sk3,X0,X1)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3774,plain,(
% 33.28/8.73 sQ194_spl|~sQ71_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3762,f3771,f1452])).
% 33.28/8.73 fof(f3797,plain,(
% 33.28/8.73 ![X0,X1,X2]: (~smaller(X0,X1)|~smaller(X2,X0)|X2=X1|greater_or_equal(X1,X2))),
% 33.28/8.73 inference(resolution,[status(thm)],[f2633,f1014])).
% 33.28/8.73 fof(f3913,definition,(
% 33.28/8.73 sQ199_spl <=> (smaller(very_low,high))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3914,plain,(
% 33.28/8.73 smaller(very_low,high)|~sQ199_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3913])).
% 33.28/8.73 fof(f3916,definition,(
% 33.28/8.73 sQ200_spl <=> (very_low=high)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3917,plain,(
% 33.28/8.73 very_low=high|~sQ200_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3916])).
% 33.28/8.73 fof(f3922,plain,(
% 33.28/8.73 greater_or_equal(high,very_low)|~sQ199_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3914,f171])).
% 33.28/8.73 fof(f3924,plain,(
% 33.28/8.73 greater(high,very_low)|high=very_low|~sQ199_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3922,f62])).
% 33.28/8.73 fof(f3925,definition,(
% 33.28/8.73 sQ201_spl <=> (greater(high,very_low))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f3926,plain,(
% 33.28/8.73 greater(high,very_low)|~sQ201_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f3925])).
% 33.28/8.73 fof(f3928,plain,(
% 33.28/8.73 sQ201_spl|sQ200_spl|~sQ199_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3924,f3925,f3916,f3913])).
% 33.28/8.73 fof(f3939,plain,(
% 33.28/8.73 ~greater(low,very_low)|~sQ200_spl|~sQ78_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f3917,f1778])).
% 33.28/8.73 fof(f3985,plain,(
% 33.28/8.73 $false|~sQ200_spl|~sQ78_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f3939,f109])).
% 33.28/8.73 fof(f3986,plain,(
% 33.28/8.73 ~sQ200_spl|~sQ78_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f3985])).
% 33.28/8.73 fof(f4021,plain,(
% 33.28/8.73 smaller(zero,age(sk3,sk6))|zero=age(sk3,sk6)),
% 33.28/8.73 inference(resolution,[status(thm)],[f2686,f559])).
% 33.28/8.73 fof(f4030,definition,(
% 33.28/8.73 sQ202_spl <=> (smaller(zero,age(sk3,sk6)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4031,plain,(
% 33.28/8.73 smaller(zero,age(sk3,sk6))|~sQ202_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f4030])).
% 33.28/8.73 fof(f4033,definition,(
% 33.28/8.73 sQ203_spl <=> (zero=age(sk3,sk6))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4034,plain,(
% 33.28/8.73 zero=age(sk3,sk6)|~sQ203_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f4033])).
% 33.28/8.73 fof(f4036,plain,(
% 33.28/8.73 sQ202_spl|sQ203_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4021,f4030,f4033])).
% 33.28/8.73 fof(f4041,plain,(
% 33.28/8.73 greater_or_equal(age(sk3,sk6),zero)|~sQ202_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f4031,f171])).
% 33.28/8.73 fof(f4043,plain,(
% 33.28/8.73 greater(age(sk3,sk6),zero)|age(sk3,sk6)=zero|~sQ202_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f4041,f62])).
% 33.28/8.73 fof(f4044,definition,(
% 33.28/8.73 sQ204_spl <=> (greater(age(sk3,sk6),zero))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4045,plain,(
% 33.28/8.73 greater(age(sk3,sk6),zero)|~sQ204_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f4044])).
% 33.28/8.73 fof(f4047,plain,(
% 33.28/8.73 sQ204_spl|sQ203_spl|~sQ202_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4043,f4044,f4033,f4030])).
% 33.28/8.73 fof(f4055,plain,(
% 33.28/8.73 ~smaller(zero,sigma)|~sQ203_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f4034,f1472])).
% 33.28/8.73 fof(f4069,plain,(
% 33.28/8.73 $false|~sQ203_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f4055,f140])).
% 33.28/8.73 fof(f4070,plain,(
% 33.28/8.73 ~sQ203_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f4069])).
% 33.28/8.73 fof(f4076,plain,(
% 33.28/8.73 ~greater(very_low,high)|~greater(very_low,high)|~sQ201_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3926,f907])).
% 33.28/8.73 fof(f4085,definition,(
% 33.28/8.73 sQ205_spl <=> (greater(very_low,high))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4088,plain,(
% 33.28/8.73 ~sQ205_spl|~sQ201_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4076,f4085,f3925])).
% 33.28/8.73 fof(f4186,definition,(
% 33.28/8.73 sQ206_spl <=> (greater_or_equal(high,very_low))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4217,plain,(
% 33.28/8.73 ~greater(zero,age(sk3,sk6))|~greater(zero,age(sk3,sk6))|~sQ204_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f4045,f907])).
% 33.28/8.73 fof(f4226,definition,(
% 33.28/8.73 sQ207_spl <=> (greater(zero,age(sk3,sk6)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4229,plain,(
% 33.28/8.73 ~sQ207_spl|~sQ204_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4217,f4226,f4044])).
% 33.28/8.73 fof(f4360,definition,(
% 33.28/8.73 sQ209_spl <=> (greater_or_equal(age(sk3,sk6),zero))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4383,plain,(
% 33.28/8.73 zero=age(sk3,sk6)|greater_or_equal(age(sk3,sk6),zero)),
% 33.28/8.73 inference(resolution,[status(thm)],[f2685,f559])).
% 33.28/8.73 fof(f4392,plain,(
% 33.28/8.73 sQ203_spl|sQ209_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4383,f4033,f4360])).
% 33.28/8.73 fof(f4424,plain,(
% 33.28/8.73 positional_advantage(sk3,sk7)|age(sk3,sk7)=tau),
% 33.28/8.73 inference(resolution,[status(thm)],[f2057,f792])).
% 33.28/8.73 fof(f4432,plain,(
% 33.28/8.73 sQ128_spl|sQ47_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4424,f2240,f796])).
% 33.28/8.73 fof(f4433,definition,(
% 33.28/8.73 sQ210_spl <=> (age(sk3,sk4)=tau)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4434,plain,(
% 33.28/8.73 age(sk3,sk4)=tau|~sQ210_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f4433])).
% 33.28/8.73 fof(f4480,plain,(
% 33.28/8.73 very_low=high|greater_or_equal(high,very_low)),
% 33.28/8.73 inference(resolution,[status(thm)],[f1588,f110])).
% 33.28/8.73 fof(f4485,plain,(
% 33.28/8.73 sQ200_spl|sQ206_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4480,f3916,f4186])).
% 33.28/8.73 fof(f4486,plain,(
% 33.28/8.73 smaller(very_low,high)|very_low=high),
% 33.28/8.73 inference(resolution,[status(thm)],[f1589,f110])).
% 33.28/8.73 fof(f4491,plain,(
% 33.28/8.73 sQ199_spl|sQ200_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4486,f3913,f3916])).
% 33.28/8.73 fof(f4502,plain,(
% 33.28/8.73 ![X0,X1]: (positional_advantage(sk3,X0)|~greater(age(sk3,X0),age(X1,sk2(X1)))|smaller_or_equal(age(X1,sk2(X1)),tau)|robust_position(X1))),
% 33.28/8.73 inference(resolution,[status(thm)],[f2058,f98])).
% 33.28/8.73 fof(f4503,plain,(
% 33.28/8.73 ![X0,X1]: (positional_advantage(sk3,X0)|~greater(age(sk3,X0),age(X1,sk2(X1)))|positional_advantage(X1,sk2(X1))|robust_position(X1))),
% 33.28/8.73 inference(resolution,[status(thm)],[f2058,f100])).
% 33.28/8.73 fof(f4505,plain,(
% 33.28/8.73 ![X0,X1]: (positional_advantage(sk3,X0)|~greater(age(sk3,X0),X1)|smaller(X1,tau)|X1=tau)),
% 33.28/8.73 inference(resolution,[status(thm)],[f2058,f70])).
% 33.28/8.73 fof(f4615,plain,(
% 33.28/8.73 positional_advantage(sk3,sk4)|~smaller(tau,zero)),
% 33.28/8.73 inference(paramodulation,[status(thm)],[f116,f2059])).
% 33.28/8.73 fof(f4619,plain,(
% 33.28/8.73 sQ103_spl|~sQ174_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4615,f2077,f3269])).
% 33.28/8.73 fof(f4632,plain,(
% 33.28/8.73 has_immunity(sk3,sk5)|positional_advantage(sk3,sk5)|hazard_of_mortality(sk3,sk5)=high|sQ115_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f2139,f633])).
% 33.28/8.73 fof(f4634,definition,(
% 33.28/8.73 sQ216_spl <=> (hazard_of_mortality(sk3,sk5)=high)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4635,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk5)=high|~sQ216_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f4634])).
% 33.28/8.73 fof(f4637,plain,(
% 33.28/8.73 sQ114_spl|sQ102_spl|sQ216_spl|sQ115_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4632,f2134,f2073,f4634,f2137])).
% 33.28/8.73 fof(f4639,plain,(
% 33.28/8.73 ~sQ30_spl|~sQ178_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f3409,f495,f3397])).
% 33.28/8.73 fof(f4651,definition,(
% 33.28/8.73 sQ217_spl <=> (has_immunity(sk3,sk1(sk3)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f4652,plain,(
% 33.28/8.73 has_immunity(sk3,sk1(sk3))|~sQ217_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f4651])).
% 33.28/8.73 fof(f4668,plain,(
% 33.28/8.73 ~organization(sk3)|has_endowment(sk3)|~sQ217_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f4652,f79])).
% 33.28/8.73 fof(f4673,plain,(
% 33.28/8.73 ~sQ71_spl|sQ120_spl|~sQ217_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4668,f1452,f2162,f4651])).
% 33.28/8.73 fof(f4677,plain,(
% 33.28/8.73 high=mod1|~sQ216_spl|~sQ117_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f4635,f2145])).
% 33.28/8.73 fof(f4684,plain,(
% 33.28/8.73 zero=tau|~sQ210_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f116,f4434])).
% 33.28/8.73 fof(f4685,plain,(
% 33.28/8.73 $false|sQ4_spl|~sQ210_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f4684,f184])).
% 33.28/8.73 fof(f4686,plain,(
% 33.28/8.73 sQ4_spl|~sQ210_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f4685])).
% 33.28/8.73 fof(f4767,plain,(
% 33.28/8.73 sQ16_spl|~sQ216_spl|~sQ117_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f4677,f260,f4634,f2144])).
% 33.28/8.73 fof(f5412,plain,(
% 33.28/8.73 ~smaller(age(sk3,sk5),tau)|sQ118_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f2150,f60])).
% 33.28/8.73 fof(f5413,plain,(
% 33.28/8.73 ~sQ98_spl|sQ118_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f5412,f1994,f2148])).
% 33.28/8.73 fof(f5419,plain,(
% 33.28/8.73 ~organization(sk3)|has_immunity(sk3,sk5)|positional_advantage(sk3,sk5)|hazard_of_mortality(sk3,sk5)=mod2|~sQ115_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f2138,f105])).
% 33.28/8.73 fof(f5422,definition,(
% 33.28/8.73 sQ231_spl <=> (hazard_of_mortality(sk3,sk5)=mod2)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5423,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk5)=mod2|~sQ231_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5422])).
% 33.28/8.73 fof(f5425,plain,(
% 33.28/8.73 ~sQ71_spl|sQ114_spl|sQ102_spl|sQ231_spl|~sQ115_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f5419,f1452,f2134,f2073,f5422,f2137])).
% 33.28/8.73 fof(f5444,plain,(
% 33.28/8.73 smaller(hazard_of_mortality(sk3,sk6),mod2)|~sQ231_spl|~sQ135_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5423,f2287])).
% 33.28/8.73 fof(f5520,definition,(
% 33.28/8.73 sQ235_spl <=> (smaller(hazard_of_mortality(sk3,sk6),mod2))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5521,plain,(
% 33.28/8.73 smaller(hazard_of_mortality(sk3,sk6),mod2)|~sQ235_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5520])).
% 33.28/8.73 fof(f5522,plain,(
% 33.28/8.73 ~smaller(hazard_of_mortality(sk3,sk6),mod2)|sQ235_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5520])).
% 33.28/8.73 fof(f5523,definition,(
% 33.28/8.73 sQ236_spl <=> (hazard_of_mortality(sk3,sk6)=mod2)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5524,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk6)=mod2|~sQ236_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5523])).
% 33.28/8.73 fof(f5539,plain,(
% 33.28/8.73 ~hazard_of_mortality(sk3,sk6)=high|~sQ216_spl|sQ136_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f4635,f2291])).
% 33.28/8.73 fof(f5542,plain,(
% 33.28/8.73 ~greater_or_equal(mod1,high)|~sQ216_spl|sQ127_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f4635,f2231])).
% 33.28/8.73 fof(f5550,definition,(
% 33.28/8.73 sQ238_spl <=> (smaller(hazard_of_mortality(sk3,sk6),high))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5551,plain,(
% 33.28/8.73 smaller(hazard_of_mortality(sk3,sk6),high)|~sQ238_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5550])).
% 33.28/8.73 fof(f5553,definition,(
% 33.28/8.73 sQ239_spl <=> (hazard_of_mortality(sk3,sk6)=high)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5554,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk6)=high|~sQ239_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5553])).
% 33.28/8.73 fof(f5562,plain,(
% 33.28/8.73 $false|~sQ216_spl|sQ136_spl|~sQ239_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f5554,f5539])).
% 33.28/8.73 fof(f5563,plain,(
% 33.28/8.73 ~sQ216_spl|sQ136_spl|~sQ239_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f5562])).
% 33.28/8.73 fof(f5707,plain,(
% 33.28/8.73 ![X0,X1]: (is_aligned(sk3,X0)|~age(sk3,X1)=zero|~age(sk3,X1)=zero|greater(age(sk3,X0),sigma))),
% 33.28/8.73 inference(resolution,[status(thm)],[f1377,f138])).
% 33.28/8.73 fof(f5711,definition,(
% 33.28/8.73 ![X0]: (sQ243_spl <=> (is_aligned(sk3,X0)|greater(age(sk3,X0),sigma)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5712,plain,(
% 33.28/8.73 ![X0]: (is_aligned(sk3,X0)|greater(age(sk3,X0),sigma)|~sQ243_spl)),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5711])).
% 33.28/8.73 fof(f5714,plain,(
% 33.28/8.73 sQ243_spl|sQ63_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f5707,f5711,f1425])).
% 33.28/8.73 fof(f5715,definition,(
% 33.28/8.73 ![X0]: (sQ244_spl <=> (is_aligned(sk3,X0)|~is_aligned(sk3,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5762,plain,(
% 33.28/8.73 positional_advantage(sk3,sk4)|hazard_of_mortality(sk3,sk4)=mod2|~age(sk3,sk4)=zero|sQ109_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f1752,f2111])).
% 33.28/8.73 fof(f5764,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero|~organization(sk3)|hazard_of_mortality(sk3,X0)=very_low)),
% 33.28/8.73 inference(resolution,[status(thm)],[f1752,f102])).
% 33.28/8.73 fof(f5765,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero|~organization(sk3)|has_endowment(sk3))),
% 33.28/8.73 inference(resolution,[status(thm)],[f1752,f79])).
% 33.28/8.73 fof(f5781,definition,(
% 33.28/8.73 sQ253_spl <=> (hazard_of_mortality(sk3,sk4)=mod2)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5782,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk4)=mod2|~sQ253_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5781])).
% 33.28/8.73 fof(f5784,definition,(
% 33.28/8.73 sQ254_spl <=> (age(sk3,sk4)=zero)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5786,plain,(
% 33.28/8.73 ~age(sk3,sk4)=zero|sQ254_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5784])).
% 33.28/8.73 fof(f5787,plain,(
% 33.28/8.73 sQ103_spl|sQ253_spl|~sQ254_spl|sQ109_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f5762,f2077,f5781,f5784,f2109])).
% 33.28/8.73 fof(f5788,definition,(
% 33.28/8.73 sQ255_spl <=> (hazard_of_mortality(sk3,sk7)=mod2)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5789,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk7)=mod2|~sQ255_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5788])).
% 33.28/8.73 fof(f5792,definition,(
% 33.28/8.73 ![X0]: (sQ256_spl <=> (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero|hazard_of_mortality(sk3,X0)=very_low))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5795,plain,(
% 33.28/8.73 sQ256_spl|~sQ71_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f5764,f5792,f1452])).
% 33.28/8.73 fof(f5796,definition,(
% 33.28/8.73 ![X0]: (sQ257_spl <=> (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f5797,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero|~sQ257_spl)),
% 33.28/8.73 inference(component_clause,[status(thm)],[f5796])).
% 33.28/8.73 fof(f5799,plain,(
% 33.28/8.73 sQ257_spl|~sQ71_spl|sQ120_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f5765,f5796,f1452,f2162])).
% 33.28/8.73 fof(f5851,plain,(
% 33.28/8.73 mod1=mod2|~sQ107_spl|~sQ255_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f2095,f5789])).
% 33.28/8.73 fof(f5852,plain,(
% 33.28/8.73 $false|sQ29_spl|~sQ107_spl|~sQ255_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f5851,f470])).
% 33.28/8.73 fof(f5853,plain,(
% 33.28/8.73 sQ29_spl|~sQ107_spl|~sQ255_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f5852])).
% 33.28/8.73 fof(f5854,plain,(
% 33.28/8.73 ~zero=zero|sQ254_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f116,f5786])).
% 33.28/8.73 fof(f5855,plain,(
% 33.28/8.73 $false|sQ254_spl),
% 33.28/8.73 inference(trivial_equality_resolution,[status(thm)],[f5854])).
% 33.28/8.73 fof(f5856,plain,(
% 33.28/8.73 sQ254_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f5855])).
% 33.28/8.73 fof(f5902,plain,(
% 33.28/8.73 ~greater(high,mod2)|~sQ239_spl|~sQ146_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f5554,f2540])).
% 33.28/8.73 fof(f5924,plain,(
% 33.28/8.73 ~smaller(hazard_of_mortality(sk3,sk5),high)|~sQ239_spl|sQ1_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5554,f130])).
% 33.28/8.73 fof(f5930,plain,(
% 33.28/8.73 smaller(high,mod2)|~sQ239_spl|~sQ231_spl|~sQ135_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5554,f5444])).
% 33.28/8.73 fof(f5931,plain,(
% 33.28/8.73 $false|~sQ239_spl|~sQ231_spl|~sQ135_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f5930,f217])).
% 33.28/8.73 fof(f5932,plain,(
% 33.28/8.73 ~sQ239_spl|~sQ231_spl|~sQ135_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f5931])).
% 33.28/8.73 fof(f5944,plain,(
% 33.28/8.73 mod2=hazard_of_mortality(sk3,sk5)|~sQ236_spl|~sQ136_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5524,f2290])).
% 33.28/8.73 fof(f5945,plain,(
% 33.28/8.73 mod2=high|~sQ216_spl|~sQ236_spl|~sQ136_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f4635,f5944])).
% 33.28/8.73 fof(f5946,plain,(
% 33.28/8.73 $false|sQ8_spl|~sQ216_spl|~sQ236_spl|~sQ136_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f5945,f234])).
% 33.28/8.73 fof(f5947,plain,(
% 33.28/8.73 sQ8_spl|~sQ216_spl|~sQ236_spl|~sQ136_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f5946])).
% 33.28/8.73 fof(f5955,plain,(
% 33.28/8.73 smaller(mod2,mod2)|~sQ236_spl|~sQ235_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5524,f5521])).
% 33.28/8.73 fof(f5956,plain,(
% 33.28/8.73 $false|~sQ236_spl|~sQ235_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f5955,f928])).
% 33.28/8.73 fof(f5957,plain,(
% 33.28/8.73 ~sQ236_spl|~sQ235_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f5956])).
% 33.28/8.73 fof(f5979,plain,(
% 33.28/8.73 ~smaller(very_low,mod2)|~sQ124_spl|sQ235_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f2208,f5522])).
% 33.28/8.73 fof(f5980,plain,(
% 33.28/8.73 $false|~sQ55_spl|~sQ124_spl|sQ235_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f5979,f1027])).
% 33.28/8.73 fof(f5981,plain,(
% 33.28/8.73 ~sQ55_spl|~sQ124_spl|sQ235_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f5980])).
% 33.28/8.73 fof(f6018,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|~organization(sk3)|hazard_of_mortality(sk3,X0)=very_low|~sQ81_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f1713,f102])).
% 33.28/8.73 fof(f6019,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|~organization(sk3)|has_endowment(sk3)|~sQ81_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f1713,f79])).
% 33.28/8.73 fof(f6023,definition,(
% 33.28/8.73 sQ260_spl <=> (hazard_of_mortality(sk3,sk4)=high)),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f6024,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk4)=high|~sQ260_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f6023])).
% 33.28/8.73 fof(f6028,definition,(
% 33.28/8.73 ![X0]: (sQ261_spl <=> (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|hazard_of_mortality(sk3,X0)=very_low))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f6031,plain,(
% 33.28/8.73 sQ261_spl|~sQ71_spl|~sQ81_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6018,f6028,f1452,f1701])).
% 33.28/8.73 fof(f6032,definition,(
% 33.28/8.73 ![X0]: (sQ262_spl <=> (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f6033,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|~sQ262_spl)),
% 33.28/8.73 inference(component_clause,[status(thm)],[f6032])).
% 33.28/8.73 fof(f6035,plain,(
% 33.28/8.73 sQ262_spl|~sQ71_spl|sQ120_spl|~sQ81_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6019,f6032,f1452,f2162,f1701])).
% 33.28/8.73 fof(f6036,plain,(
% 33.28/8.73 high=mod2|~sQ260_spl|~sQ253_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f6024,f5782])).
% 33.28/8.73 fof(f6039,plain,(
% 33.28/8.73 sQ8_spl|~sQ260_spl|~sQ253_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6036,f232,f6023,f5781])).
% 33.28/8.73 fof(f6464,plain,(
% 33.28/8.73 smaller(high,hazard_of_mortality(sk3,sk6))|~sQ216_spl|~sQ1_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f4635,f129])).
% 33.28/8.73 fof(f6466,plain,(
% 33.28/8.73 very_low=high|~sQ122_spl|~sQ216_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f2190,f4635])).
% 33.28/8.73 fof(f6473,plain,(
% 33.28/8.73 ~smaller(zero,sigma)|~sQ130_spl|~sQ30_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f2248,f3284])).
% 33.28/8.73 fof(f6507,plain,(
% 33.28/8.73 smaller(high,high)|~sQ136_spl|~sQ216_spl|~sQ1_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f6509,f6464])).
% 33.28/8.73 fof(f6509,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk6)=high|~sQ216_spl|~sQ136_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f4635,f2290])).
% 33.28/8.73 fof(f6515,plain,(
% 33.28/8.73 greater(mod1,high)|~sQ216_spl|~sQ147_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f4635,f2518])).
% 33.28/8.73 fof(f6516,plain,(
% 33.28/8.73 $false|~sQ216_spl|~sQ147_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f6515,f147])).
% 33.28/8.73 fof(f6517,plain,(
% 33.28/8.73 ~sQ216_spl|~sQ147_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f6516])).
% 33.28/8.73 fof(f6533,plain,(
% 33.28/8.73 sQ200_spl|~sQ122_spl|~sQ216_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6466,f3916,f2189,f4634])).
% 33.28/8.73 fof(f6534,plain,(
% 33.28/8.73 $false|~sQ130_spl|~sQ30_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f6473,f140])).
% 33.28/8.73 fof(f6535,plain,(
% 33.28/8.73 ~sQ130_spl|~sQ30_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f6534])).
% 33.28/8.73 fof(f6536,plain,(
% 33.28/8.73 $false|~sQ136_spl|~sQ216_spl|~sQ1_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f6507,f928])).
% 33.28/8.73 fof(f6537,plain,(
% 33.28/8.73 ~sQ136_spl|~sQ216_spl|~sQ1_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f6536])).
% 33.28/8.73 fof(f6588,plain,(
% 33.28/8.73 ![X0]: (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=high|~greater(age(sk3,X0),sigma)|~sQ66_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f633,f1436])).
% 33.28/8.73 fof(f6612,plain,(
% 33.28/8.73 greater(age(sk3,sk7),zero)|age(sk3,sk7)=zero|~sQ175_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f3538,f62])).
% 33.28/8.73 fof(f6613,plain,(
% 33.28/8.73 sQ184_spl|sQ130_spl|~sQ175_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6612,f3534,f2247,f3381])).
% 33.28/8.73 fof(f6775,definition,(
% 33.28/8.73 sQ286_spl <=> (greater_or_equal(hazard_of_mortality(sk3,sk6),mod2))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f6776,plain,(
% 33.28/8.73 greater_or_equal(hazard_of_mortality(sk3,sk6),mod2)|~sQ286_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f6775])).
% 33.28/8.73 fof(f6795,plain,(
% 33.28/8.73 ~greater_or_equal(very_low,mod2)|~sQ236_spl|sQ125_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f5524,f2214])).
% 33.28/8.73 fof(f6817,plain,(
% 33.28/8.73 greater(hazard_of_mortality(sk3,sk6),mod2)|hazard_of_mortality(sk3,sk6)=mod2|~sQ286_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f6776,f62])).
% 33.28/8.73 fof(f6818,definition,(
% 33.28/8.73 sQ288_spl <=> (greater(hazard_of_mortality(sk3,sk6),mod2))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f6821,plain,(
% 33.28/8.73 sQ288_spl|sQ236_spl|~sQ286_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6817,f6818,f5523,f6775])).
% 33.28/8.73 fof(f6870,plain,(
% 33.28/8.73 smaller(very_low,hazard_of_mortality(sk3,sk6))|very_low=hazard_of_mortality(sk3,sk6)|sQ123_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f2206,f228])).
% 33.28/8.73 fof(f6872,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk6)=very_low|greater_or_equal(hazard_of_mortality(sk3,sk6),very_low)|sQ123_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f2206,f226])).
% 33.28/8.73 fof(f6873,definition,(
% 33.28/8.73 sQ290_spl <=> (smaller(very_low,hazard_of_mortality(sk3,sk6)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f6876,plain,(
% 33.28/8.73 sQ290_spl|sQ124_spl|sQ123_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6870,f6873,f2207,f2204])).
% 33.28/8.73 fof(f6878,definition,(
% 33.28/8.73 sQ291_spl <=> (greater_or_equal(hazard_of_mortality(sk3,sk6),very_low))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ291_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f6881,plain,(
% 33.28/8.73 sQ124_spl|sQ291_spl|sQ123_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6872,f2207,f6878,f2204])).
% 33.28/8.73 fof(f6884,plain,(
% 33.28/8.73 $false|~sQ239_spl|~sQ146_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f5902,f110])).
% 33.28/8.73 fof(f6885,plain,(
% 33.28/8.73 ~sQ239_spl|~sQ146_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f6884])).
% 33.28/8.73 fof(f6890,plain,(
% 33.28/8.73 ~smaller(hazard_of_mortality(sk3,sk6),high)|~sQ216_spl|sQ135_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f4635,f2288])).
% 33.28/8.73 fof(f6891,plain,(
% 33.28/8.73 $false|~sQ216_spl|sQ135_spl|~sQ238_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f5551,f6890])).
% 33.28/8.73 fof(f6892,plain,(
% 33.28/8.73 ~sQ216_spl|sQ135_spl|~sQ238_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f6891])).
% 33.28/8.73 fof(f6893,plain,(
% 33.28/8.73 ~greater(age(sk3,sk7),sigma)|~sQ105_spl|~sQ66_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f2088,f1436])).
% 33.28/8.73 fof(f6897,plain,(
% 33.28/8.73 $false|~sQ182_spl|~sQ105_spl|~sQ66_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f6893,f3455])).
% 33.28/8.73 fof(f6898,plain,(
% 33.28/8.73 ~sQ182_spl|~sQ105_spl|~sQ66_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f6897])).
% 33.28/8.73 fof(f6908,plain,(
% 33.28/8.73 ~greater(mod1,hazard_of_mortality(sk3,sk6))|~sQ136_spl|~sQ107_spl|~sQ0_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f2290,f2281])).
% 33.28/8.73 fof(f6911,plain,(
% 33.28/8.73 hazard_of_mortality(sk3,sk6)=mod2|~sQ231_spl|~sQ136_spl),
% 33.28/8.73 inference(backward_demodulation,[status(thm)],[f5423,f2290])).
% 33.28/8.73 fof(f6947,plain,(
% 33.28/8.73 ~greater(mod1,very_low)|~sQ124_spl|~sQ136_spl|~sQ107_spl|~sQ0_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f2208,f6908])).
% 33.28/8.73 fof(f6948,plain,(
% 33.28/8.73 $false|~sQ74_spl|~sQ124_spl|~sQ136_spl|~sQ107_spl|~sQ0_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f6947,f1518])).
% 33.28/8.73 fof(f6949,plain,(
% 33.28/8.73 ~sQ74_spl|~sQ124_spl|~sQ136_spl|~sQ107_spl|~sQ0_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f6948])).
% 33.28/8.73 fof(f6950,plain,(
% 33.28/8.73 sQ236_spl|~sQ231_spl|~sQ136_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f6911,f5523,f5422,f2289])).
% 33.28/8.73 fof(f7028,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,sk4)|~greater(zero,age(X0,sk2(X0)))|positional_advantage(X0,sk2(X0))|robust_position(X0))),
% 33.28/8.73 inference(paramodulation,[status(thm)],[f116,f4503])).
% 33.28/8.73 fof(f7029,definition,(
% 33.28/8.73 ![X0]: (sQ293_spl <=> (~greater(zero,age(X0,sk2(X0)))|positional_advantage(X0,sk2(X0))|robust_position(X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f7032,plain,(
% 33.28/8.73 sQ103_spl|sQ293_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f7028,f2077,f7029])).
% 33.28/8.73 fof(f8381,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,sk4)|~greater(zero,X0)|smaller(X0,tau)|X0=tau)),
% 33.28/8.73 inference(paramodulation,[status(thm)],[f116,f4505])).
% 33.28/8.73 fof(f8386,definition,(
% 33.28/8.73 sQ334_spl <=> (positional_advantage(sk3,sk6))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f8387,plain,(
% 33.28/8.73 positional_advantage(sk3,sk6)|~sQ334_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f8386])).
% 33.28/8.73 fof(f8393,definition,(
% 33.28/8.73 ![X0]: (sQ335_spl <=> (~greater(zero,X0)|smaller(X0,tau)|X0=tau))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f8396,plain,(
% 33.28/8.73 sQ103_spl|sQ335_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f8381,f2077,f8393])).
% 33.28/8.73 fof(f8405,plain,(
% 33.28/8.73 ![X0]: (positional_advantage(sk3,sk4)|~greater(zero,age(X0,sk2(X0)))|smaller_or_equal(age(X0,sk2(X0)),tau)|robust_position(X0))),
% 33.28/8.73 inference(paramodulation,[status(thm)],[f116,f4502])).
% 33.28/8.73 fof(f8408,definition,(
% 33.28/8.73 ![X0]: (sQ337_spl <=> (~greater(zero,age(X0,sk2(X0)))|smaller_or_equal(age(X0,sk2(X0)),tau)|robust_position(X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f8411,plain,(
% 33.28/8.73 sQ103_spl|sQ337_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f8405,f2077,f8408])).
% 33.28/8.73 fof(f10536,plain,(
% 33.28/8.73 ![X0]: (hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero|~organization(sk3)|has_immunity(sk3,X0)|~is_aligned(sk3,X0)|hazard_of_mortality(sk3,X0)=low|~sQ257_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f5797,f103])).
% 33.28/8.73 fof(f10537,plain,(
% 33.28/8.73 ![X0]: (hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero|~organization(sk3)|has_immunity(sk3,X0)|is_aligned(sk3,X0)|hazard_of_mortality(sk3,X0)=mod1|~sQ257_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f5797,f104])).
% 33.28/8.73 fof(f10543,definition,(
% 33.28/8.73 ![X0]: (sQ352_spl <=> (hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero|has_immunity(sk3,X0)|~is_aligned(sk3,X0)|hazard_of_mortality(sk3,X0)=low))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f10546,plain,(
% 33.28/8.73 sQ352_spl|~sQ71_spl|~sQ257_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f10536,f10543,f1452,f5796])).
% 33.28/8.73 fof(f10547,definition,(
% 33.28/8.73 ![X0]: (sQ353_spl <=> (hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero|has_immunity(sk3,X0)|is_aligned(sk3,X0)|hazard_of_mortality(sk3,X0)=mod1))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f10550,plain,(
% 33.28/8.73 sQ353_spl|~sQ71_spl|~sQ257_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f10537,f10547,f1452,f5796])).
% 33.28/8.73 fof(f10642,plain,(
% 33.28/8.73 ![X0]: (hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|~organization(sk3)|has_immunity(sk3,X0)|~is_aligned(sk3,X0)|hazard_of_mortality(sk3,X0)=low|~sQ262_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f6033,f103])).
% 33.28/8.73 fof(f10643,plain,(
% 33.28/8.73 ![X0]: (hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|~organization(sk3)|has_immunity(sk3,X0)|is_aligned(sk3,X0)|hazard_of_mortality(sk3,X0)=mod1|~sQ262_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f6033,f104])).
% 33.28/8.73 fof(f10649,definition,(
% 33.28/8.73 ![X0]: (sQ354_spl <=> (hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|has_immunity(sk3,X0)|~is_aligned(sk3,X0)|hazard_of_mortality(sk3,X0)=low))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f10652,plain,(
% 33.28/8.73 sQ354_spl|~sQ71_spl|~sQ262_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f10642,f10649,f1452,f6032])).
% 33.28/8.73 fof(f10653,definition,(
% 33.28/8.73 ![X0]: (sQ355_spl <=> (hazard_of_mortality(sk3,X0)=high|hazard_of_mortality(sk3,X0)=mod2|has_immunity(sk3,X0)|is_aligned(sk3,X0)|hazard_of_mortality(sk3,X0)=mod1))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f10656,plain,(
% 33.28/8.73 sQ355_spl|~sQ71_spl|~sQ262_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f10643,f10653,f1452,f6032])).
% 33.28/8.73 fof(f12714,plain,(
% 33.28/8.73 ![X0]: (~greater(very_low,X0)|~smaller(mod2,X0)|mod2=very_low|~sQ236_spl|sQ125_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f2630,f6795])).
% 33.28/8.73 fof(f12725,definition,(
% 33.28/8.73 ![X0]: (sQ378_spl <=> (~greater(very_low,X0)|~smaller(mod2,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f12728,plain,(
% 33.28/8.73 sQ378_spl|sQ56_spl|~sQ236_spl|sQ125_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f12714,f12725,f1029,f5523,f2212])).
% 33.28/8.73 fof(f12758,plain,(
% 33.28/8.73 ![X0]: (~smaller(X0,very_low)|~smaller(mod2,X0)|mod2=very_low|~sQ236_spl|sQ125_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f3797,f6795])).
% 33.28/8.73 fof(f12769,definition,(
% 33.28/8.73 ![X0]: (sQ382_spl <=> (~smaller(X0,very_low)|~smaller(mod2,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ382_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f12772,plain,(
% 33.28/8.73 sQ382_spl|sQ56_spl|~sQ236_spl|sQ125_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f12758,f12769,f1029,f5523,f2212])).
% 33.28/8.73 fof(f13348,definition,(
% 33.28/8.73 sQ404_spl <=> (greater(eta,eta))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f13349,plain,(
% 33.28/8.73 greater(eta,eta)|~sQ404_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f13348])).
% 33.28/8.73 fof(f13373,plain,(
% 33.28/8.73 $false|~sQ404_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f13349,f925])).
% 33.28/8.73 fof(f13374,plain,(
% 33.28/8.73 ~sQ404_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f13373])).
% 33.28/8.73 fof(f13455,plain,(
% 33.28/8.73 ![X0]: (~organization(sk3)|is_aligned(sk3,X0)|dissimilar(sk3,X0,sk4)|~sQ110_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f2113,f89])).
% 33.28/8.73 fof(f13456,plain,(
% 33.28/8.73 ![X0]: (~organization(sk3)|is_aligned(sk3,X0)|dissimilar(sk3,sk4,X0)|~sQ110_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f2113,f88])).
% 33.28/8.73 fof(f13459,definition,(
% 33.28/8.73 ![X0]: (sQ406_spl <=> (is_aligned(sk3,X0)|dissimilar(sk3,X0,sk4)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f13460,plain,(
% 33.28/8.73 ![X0]: (is_aligned(sk3,X0)|dissimilar(sk3,X0,sk4)|~sQ406_spl)),
% 33.28/8.73 inference(component_clause,[status(thm)],[f13459])).
% 33.28/8.73 fof(f13462,plain,(
% 33.28/8.73 ~sQ71_spl|sQ406_spl|~sQ110_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f13455,f1452,f13459,f2112])).
% 33.28/8.73 fof(f13463,definition,(
% 33.28/8.73 ![X0]: (sQ407_spl <=> (is_aligned(sk3,X0)|dissimilar(sk3,sk4,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f13466,plain,(
% 33.28/8.73 ~sQ71_spl|sQ407_spl|~sQ110_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f13456,f1452,f13463,f2112])).
% 33.28/8.73 fof(f13510,definition,(
% 33.28/8.73 sQ408_spl <=> (has_immunity(sk3,sk6))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f13511,plain,(
% 33.28/8.73 has_immunity(sk3,sk6)|~sQ408_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f13510])).
% 33.28/8.73 fof(f13516,plain,(
% 33.28/8.73 ~smaller_or_equal(age(sk3,sk6),tau)|~sQ334_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f8387,f3210])).
% 33.28/8.73 fof(f13519,plain,(
% 33.28/8.73 $false|~sQ334_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f13516,f122])).
% 33.28/8.73 fof(f13520,plain,(
% 33.28/8.73 ~sQ334_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f13519])).
% 33.28/8.73 fof(f13538,plain,(
% 33.28/8.73 ~smaller(mod2,high)|~sQ231_spl|~sQ239_spl|sQ1_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5423,f5924])).
% 33.28/8.73 fof(f13539,plain,(
% 33.28/8.73 $false|~sQ231_spl|~sQ239_spl|sQ1_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f13538,f154])).
% 33.28/8.73 fof(f13540,plain,(
% 33.28/8.73 ~sQ231_spl|~sQ239_spl|sQ1_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f13539])).
% 33.28/8.73 fof(f15810,plain,(
% 33.28/8.73 is_aligned(sk3,sk5)|~sQ243_spl|~sQ5_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f5712,f975])).
% 33.28/8.73 fof(f15839,plain,(
% 33.28/8.73 is_aligned(sk3,sk4)|greater(zero,sigma)|~sQ243_spl),
% 33.28/8.73 inference(paramodulation,[status(thm)],[f116,f5712])).
% 33.28/8.73 fof(f15845,definition,(
% 33.28/8.73 sQ414_spl <=> (greater(sigma,sigma))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f15846,plain,(
% 33.28/8.73 greater(sigma,sigma)|~sQ414_spl),
% 33.28/8.73 inference(component_clause,[status(thm)],[f15845])).
% 33.28/8.73 fof(f15849,plain,(
% 33.28/8.73 sQ110_spl|sQ52_spl|~sQ243_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f15839,f2112,f981,f5711])).
% 33.28/8.73 fof(f15850,plain,(
% 33.28/8.73 $false|~sQ414_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f15846,f925])).
% 33.28/8.73 fof(f15851,plain,(
% 33.28/8.73 ~sQ414_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f15850])).
% 33.28/8.73 fof(f15983,plain,(
% 33.28/8.73 has_immunity(sk3,sk6)|positional_advantage(sk3,sk6)|hazard_of_mortality(sk3,sk6)=high|~sQ66_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f6588,f121])).
% 33.28/8.73 fof(f15992,plain,(
% 33.28/8.73 sQ408_spl|sQ334_spl|sQ239_spl|~sQ66_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f15983,f13510,f8386,f5553,f1435])).
% 33.28/8.73 fof(f16253,plain,(
% 33.28/8.73 ~organization(sk3)|has_endowment(sk3)|~sQ408_spl),
% 33.28/8.73 inference(resolution,[status(thm)],[f13511,f79])).
% 33.28/8.73 fof(f16255,plain,(
% 33.28/8.73 ~sQ71_spl|sQ120_spl|~sQ408_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f16253,f1452,f2162,f13510])).
% 33.28/8.73 fof(f16303,plain,(
% 33.28/8.73 sQ115_spl|~sQ243_spl|~sQ5_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f15810,f2137,f5711,f203])).
% 33.28/8.73 fof(f16370,plain,(
% 33.28/8.73 ~greater_or_equal(very_low,high)|~sQ239_spl|sQ125_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5554,f2214])).
% 33.28/8.73 fof(f16614,plain,(
% 33.28/8.73 ![X0]: (~smaller(X0,mod1)|~smaller(high,X0)|high=mod1|~sQ216_spl|sQ127_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f5542,f3797])).
% 33.28/8.73 fof(f16615,plain,(
% 33.28/8.73 ![X0]: (~greater(mod1,X0)|~smaller(high,X0)|high=mod1|~sQ216_spl|sQ127_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f5542,f2630])).
% 33.28/8.73 fof(f16619,definition,(
% 33.28/8.73 ![X0]: (sQ415_spl <=> (~smaller(X0,mod1)|~smaller(high,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f16622,plain,(
% 33.28/8.73 sQ415_spl|sQ16_spl|~sQ216_spl|sQ127_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f16614,f16619,f260,f4634,f2229])).
% 33.28/8.73 fof(f16623,definition,(
% 33.28/8.73 ![X0]: (sQ416_spl <=> (~greater(mod1,X0)|~smaller(high,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f16626,plain,(
% 33.28/8.73 sQ416_spl|sQ16_spl|~sQ216_spl|sQ127_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f16615,f16623,f260,f4634,f2229])).
% 33.28/8.73 fof(f16634,definition,(
% 33.28/8.73 ![X0]: (sQ417_spl <=> (~smaller(X0,very_low)|~smaller(high,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f16638,definition,(
% 33.28/8.73 ![X0]: (sQ418_spl <=> (~greater(very_low,X0)|~smaller(high,X0)))),
% 33.28/8.73 introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition])).
% 33.28/8.73 fof(f16902,plain,(
% 33.28/8.73 ~smaller(mod1,hazard_of_mortality(sk3,sk5))|~sQ107_spl|sQ0_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f2095,f127])).
% 33.28/8.73 fof(f16903,plain,(
% 33.28/8.73 ~smaller(mod1,mod2)|~sQ231_spl|~sQ107_spl|sQ0_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5423,f16902])).
% 33.28/8.73 fof(f16904,plain,(
% 33.28/8.73 $false|~sQ231_spl|~sQ107_spl|sQ0_spl),
% 33.28/8.73 inference(forward_subsumption_resolution,[status(thm)],[f16903,f158])).
% 33.28/8.73 fof(f16905,plain,(
% 33.28/8.73 ~sQ231_spl|~sQ107_spl|sQ0_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f16904])).
% 33.28/8.73 fof(f16960,plain,(
% 33.28/8.73 ~mod2=hazard_of_mortality(sk3,sk4)|~sQ231_spl|sQ2_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5423,f133])).
% 33.28/8.73 fof(f16961,plain,(
% 33.28/8.73 ~mod2=mod2|~sQ253_spl|~sQ231_spl|sQ2_spl),
% 33.28/8.73 inference(forward_demodulation,[status(thm)],[f5782,f16960])).
% 33.28/8.73 fof(f16962,plain,(
% 33.28/8.73 $false|~sQ253_spl|~sQ231_spl|sQ2_spl),
% 33.28/8.73 inference(trivial_equality_resolution,[status(thm)],[f16961])).
% 33.28/8.73 fof(f16963,plain,(
% 33.28/8.73 ~sQ253_spl|~sQ231_spl|sQ2_spl),
% 33.28/8.73 inference(contradiction_clause,[status(thm)],[f16962])).
% 33.28/8.73 fof(f17066,plain,(
% 33.28/8.73 ![X0]: (~smaller(X0,very_low)|~smaller(high,X0)|high=very_low|~sQ239_spl|sQ125_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f16370,f3797])).
% 33.28/8.73 fof(f17067,plain,(
% 33.28/8.73 ![X0]: (~greater(very_low,X0)|~smaller(high,X0)|high=very_low|~sQ239_spl|sQ125_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f16370,f2630])).
% 33.28/8.73 fof(f17071,plain,(
% 33.28/8.73 sQ417_spl|sQ200_spl|~sQ239_spl|sQ125_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f17066,f16634,f3916,f5553,f2212])).
% 33.28/8.73 fof(f17072,plain,(
% 33.28/8.73 sQ418_spl|sQ200_spl|~sQ239_spl|sQ125_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f17067,f16638,f3916,f5553,f2212])).
% 33.28/8.73 fof(f18551,plain,(
% 33.28/8.73 ![X0]: (is_aligned(sk3,X0)|~is_aligned(sk3,X0)|~is_aligned(sk3,sk4)|~sQ406_spl)),
% 33.28/8.73 inference(resolution,[status(thm)],[f13460,f85])).
% 33.28/8.73 fof(f18558,plain,(
% 33.28/8.73 sQ244_spl|~sQ110_spl|~sQ406_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f18551,f5715,f2112,f13459])).
% 33.28/8.73 fof(f19841,plain,(
% 33.28/8.73 is_aligned(sk3,sk5)|greater(sigma,sigma)|~sQ243_spl|~sQ6_spl),
% 33.28/8.73 inference(paramodulation,[status(thm)],[f207,f5712])).
% 33.28/8.73 fof(f19848,plain,(
% 33.28/8.73 sQ115_spl|sQ414_spl|~sQ243_spl|~sQ6_spl),
% 33.28/8.73 inference(split_clause,[status(thm)],[f19841,f2137,f15845,f5711,f206])).
% 33.28/8.73 fof(f19850,plain,(
% 33.28/8.73 $false),
% 33.28/8.73 inference(sat_refutation,[status(thm)],[f134,f185,f201,f209,f235,f242,f249,f256,f263,f270,f324,f332,f340,f360,f369,f384,f402,f410,f415,f423,f435,f471,f493,f582,f623,f666,f670,f674,f678,f682,f686,f690,f698,f743,f745,f799,f807,f873,f958,f969,f1002,f1007,f1032,f1068,f1191,f1195,f1240,f1250,f1286,f1290,f1337,f1372,f1431,f1438,f1445,f1455,f1461,f1465,f1466,f1467,f1476,f1515,f1520,f1569,f1607,f1612,f1664,f1704,f1708,f1712,f1776,f1997,f2027,f2097,f2101,f2104,f2105,f2126,f2151,f2165,f2168,f2171,f2180,f2185,f2193,f2215,f2219,f2232,f2236,f2252,f2292,f2305,f2314,f2446,f2447,f2451,f2456,f2457,f2461,f2465,f2466,f2470,f2471,f2472,f2476,f2480,f2483,f2515,f2520,f2577,f3038,f3384,f3389,f3400,f3457,f3544,f3560,f3734,f3766,f3770,f3774,f3928,f3986,f4036,f4047,f4070,f4088,f4229,f4392,f4432,f4485,f4491,f4619,f4637,f4639,f4673,f4686,f4767,f5413,f5425,f5563,f5714,f5787,f5795,f5799,f5853,f5856,f5932,f5947,f5957,f5981,f6031,f6035,f6039,f6517,f6533,f6535,f6537,f6613,f6821,f6876,f6881,f6885,f6892,f6898,f6949,f6950,f7032,f8396,f8411,f10546,f10550,f10652,f10656,f12728,f12772,f13374,f13462,f13466,f13520,f13540,f15849,f15851,f15992,f16255,f16303,f16622,f16626,f16905,f16963,f17071,f17072,f18558,f19848])).
% 33.28/8.73 % SZS output end CNFRefutation for theBenchmark.p
% 33.28/8.74 % Elapsed time: 8.374622 seconds
% 33.28/8.74 % CPU time: 66.115374 seconds
% 33.28/8.74 % Total memory used: 341.591 MB
% 33.28/8.74 % Net memory used: 293.193 MB
%------------------------------------------------------------------------------