%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT062-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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:25:52 PM UTC 2026
% Result : Unsatisfiable 9.14s 11.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT062-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/10.31 % Computer : n012.cluster.edu
% 0.03/10.31 % Model : x86_64 x86_64
% 0.03/10.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/10.31 % Memory : 8046.5625MB
% 0.03/10.31 % OS : Linux 6.8.0-71-generic
% 0.03/10.31 % CPULimit : 300
% 0.03/10.31 % WCLimit : 300
% 0.03/10.31 % DateTime : Mon Sep 21 01:24:32 UTC 2026
% 0.03/10.31 % CPUTime :
% 0.03/10.32 % Drodi V4.1.1
% 9.14/11.52 % Refutation found
% 9.14/11.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.14/11.52 % SZS output start CNFRefutation for theBenchmark
% 9.14/11.52 fof(f2,axiom,(
% 9.14/11.52 (![A,B]: (( ~ smaller(A,B)| smaller_or_equal(A,B) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f3,axiom,(
% 9.14/11.52 (![A,B]: (( A != B| smaller_or_equal(A,B) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f7,axiom,(
% 9.14/11.52 (![A,B]: (( ~ smaller(A,B)| greater(B,A) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f8,axiom,(
% 9.14/11.52 (![A,B]: (( ~ greater(A,B)| smaller(B,A) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f9,axiom,(
% 9.14/11.52 (![A,B]: (( ~ greater(A,B)| ~ greater(B,A) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f10,axiom,(
% 9.14/11.52 (![A,B,C]: (( ~ greater(A,B)| ~ greater(B,C)| greater(A,C) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f11,axiom,(
% 9.14/11.52 (![A,B]: (( smaller(A,B)| A = B| greater(A,B) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f12,axiom,(
% 9.14/11.52 (![A,B]: (( ~ organization(A)| has_endowment(A)| ~ has_immunity(A,B) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f13,axiom,(
% 9.14/11.52 (![A,B,C]: (( ~ dissimilar(A,B,C)| organization(A) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f15,axiom,(
% 9.14/11.52 (![A,B,C]: (( ~ dissimilar(A,B,C)| ~ is_aligned(A,B)| ~ is_aligned(A,C) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f17,axiom,(
% 9.14/11.52 (![A,B,C]: (( ~ organization(A)| ~ is_aligned(A,B)| is_aligned(A,C)| dissimilar(A,B,C) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f20,axiom,(
% 9.14/11.52 (![A,B]: (( ~ organization(A)| age(A,B) != zero| is_aligned(A,B) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f21,axiom,(
% 9.14/11.52 (![A,B,C]: (( ~ organization(A)| age(A,B) != zero| ~ greater(age(A,C),sigma)| dissimilar(A,B,C) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f22,axiom,(
% 9.14/11.52 (![A,B,C]: (( ~ organization(A)| age(A,B) != zero| ~ dissimilar(A,B,C)| greater(age(A,C),sigma) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f23,axiom,(
% 9.14/11.52 (![A,B]: (( ~ robust_position(A)| ~ smaller_or_equal(age(A,B),tau)| ~ positional_advantage(A,B) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f24,axiom,(
% 9.14/11.52 (![A,B]: (( ~ robust_position(A)| ~ greater(age(A,B),tau)| positional_advantage(A,B) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f25,axiom,(
% 9.14/11.52 (![A]: (( smaller_or_equal(age(A,sk1(A)),tau)| greater(age(A,sk1(A)),tau)| robust_position(A) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f27,axiom,(
% 9.14/11.52 (![A]: (( positional_advantage(A,sk1(A))| greater(age(A,sk1(A)),tau)| robust_position(A) ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f31,axiom,(
% 9.14/11.52 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| is_aligned(A,B)| ~ positional_advantage(A,B)| hazard_of_mortality(A,B) = mod1 ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f32,axiom,(
% 9.14/11.52 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| ~ is_aligned(A,B)| positional_advantage(A,B)| hazard_of_mortality(A,B) = mod2 ) ))),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f34,axiom,(
% 9.14/11.52 greater(mod2,mod1) ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f35,negated_conjecture,(
% 9.14/11.52 organization(sk2) ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f36,negated_conjecture,(
% 9.14/11.52 robust_position(sk2) ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f37,negated_conjecture,(
% 9.14/11.52 ~ has_endowment(sk2) ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f38,negated_conjecture,(
% 9.14/11.52 age(sk2,sk3) = zero ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f39,negated_conjecture,(
% 9.14/11.52 greater(sigma,zero) ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f41,negated_conjecture,(
% 9.14/11.52 sigma = tau ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f42,negated_conjecture,(
% 9.14/11.52 smaller_or_equal(age(sk2,sk4),sigma) ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f43,negated_conjecture,(
% 9.14/11.52 greater(age(sk2,sk5),sigma) ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f44,negated_conjecture,(
% 9.14/11.52 ( ~ smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ),
% 9.14/11.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.14/11.52 fof(f46,plain,(
% 9.14/11.52 ![X0,X1]: (~smaller(X0,X1)|smaller_or_equal(X0,X1))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f2])).
% 9.14/11.52 fof(f47,plain,(
% 9.14/11.52 ![X0,X1]: (~X0=X1|smaller_or_equal(X0,X1))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f3])).
% 9.14/11.52 fof(f51,plain,(
% 9.14/11.52 ![X0,X1]: (~smaller(X0,X1)|greater(X1,X0))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f7])).
% 9.14/11.52 fof(f52,plain,(
% 9.14/11.52 ![X0,X1]: (~greater(X0,X1)|smaller(X1,X0))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f8])).
% 9.14/11.52 fof(f53,plain,(
% 9.14/11.52 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f9])).
% 9.14/11.52 fof(f54,plain,(
% 9.14/11.52 ![A,C]: ((![B]: (~greater(A,B)|~greater(B,C)))|greater(A,C))),
% 9.14/11.52 inference(miniscoping,[status(thm)],[f10])).
% 9.14/11.52 fof(f55,plain,(
% 9.14/11.52 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f54])).
% 9.14/11.52 fof(f56,plain,(
% 9.14/11.52 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater(X0,X1))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f11])).
% 9.14/11.52 fof(f57,plain,(
% 9.14/11.52 ![A]: ((~organization(A)|has_endowment(A))|(![B]: ~has_immunity(A,B)))),
% 9.14/11.52 inference(miniscoping,[status(thm)],[f12])).
% 9.14/11.52 fof(f58,plain,(
% 9.14/11.52 ![X0,X1]: (~organization(X0)|has_endowment(X0)|~has_immunity(X0,X1))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f57])).
% 9.14/11.52 fof(f59,plain,(
% 9.14/11.52 ![A]: ((![B,C]: ~dissimilar(A,B,C))|organization(A))),
% 9.14/11.52 inference(miniscoping,[status(thm)],[f13])).
% 9.14/11.52 fof(f60,plain,(
% 9.14/11.52 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|organization(X0))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f59])).
% 9.14/11.52 fof(f63,plain,(
% 9.14/11.52 ![A,C]: ((![B]: (~dissimilar(A,B,C)|~is_aligned(A,B)))|~is_aligned(A,C))),
% 9.14/11.52 inference(miniscoping,[status(thm)],[f15])).
% 9.14/11.52 fof(f64,plain,(
% 9.14/11.52 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f63])).
% 9.14/11.52 fof(f67,plain,(
% 9.14/11.52 ![X0,X1,X2]: (~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2)|dissimilar(X0,X1,X2))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f17])).
% 9.14/11.52 fof(f71,plain,(
% 9.14/11.52 ![X0,X1]: (~organization(X0)|~age(X0,X1)=zero|is_aligned(X0,X1))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f20])).
% 9.14/11.52 fof(f72,plain,(
% 9.14/11.52 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~greater(age(X0,X2),sigma)|dissimilar(X0,X1,X2))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f21])).
% 9.14/11.52 fof(f73,plain,(
% 9.14/11.52 ![A,C]: ((![B]: ((~organization(A)|~age(A,B)=zero)|~dissimilar(A,B,C)))|greater(age(A,C),sigma))),
% 9.14/11.52 inference(miniscoping,[status(thm)],[f22])).
% 9.14/11.52 fof(f74,plain,(
% 9.14/11.52 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~dissimilar(X0,X1,X2)|greater(age(X0,X2),sigma))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f73])).
% 9.14/11.52 fof(f75,plain,(
% 9.14/11.52 ![X0,X1]: (~robust_position(X0)|~smaller_or_equal(age(X0,X1),tau)|~positional_advantage(X0,X1))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f23])).
% 9.14/11.52 fof(f76,plain,(
% 9.14/11.52 ![X0,X1]: (~robust_position(X0)|~greater(age(X0,X1),tau)|positional_advantage(X0,X1))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f24])).
% 9.14/11.52 fof(f77,plain,(
% 9.14/11.52 ![X0]: (smaller_or_equal(age(X0,sk1(X0)),tau)|greater(age(X0,sk1(X0)),tau)|robust_position(X0))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f25])).
% 9.14/11.52 fof(f79,plain,(
% 9.14/11.52 ![X0]: (positional_advantage(X0,sk1(X0))|greater(age(X0,sk1(X0)),tau)|robust_position(X0))),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f27])).
% 9.14/11.52 fof(f83,plain,(
% 9.14/11.52 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod1)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f31])).
% 9.14/11.52 fof(f84,plain,(
% 9.14/11.52 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f32])).
% 9.14/11.52 fof(f86,plain,(
% 9.14/11.52 greater(mod2,mod1)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f34])).
% 9.14/11.52 fof(f87,plain,(
% 9.14/11.52 organization(sk2)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f35])).
% 9.14/11.52 fof(f88,plain,(
% 9.14/11.52 robust_position(sk2)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f36])).
% 9.14/11.52 fof(f89,plain,(
% 9.14/11.52 ~has_endowment(sk2)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f37])).
% 9.14/11.52 fof(f90,plain,(
% 9.14/11.52 age(sk2,sk3)=zero),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f38])).
% 9.14/11.52 fof(f91,plain,(
% 9.14/11.52 greater(sigma,zero)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f39])).
% 9.14/11.52 fof(f93,plain,(
% 9.14/11.52 sigma=tau),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f41])).
% 9.14/11.52 fof(f94,plain,(
% 9.14/11.52 smaller_or_equal(age(sk2,sk4),sigma)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f42])).
% 9.14/11.52 fof(f95,plain,(
% 9.14/11.52 greater(age(sk2,sk5),sigma)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f43])).
% 9.14/11.52 fof(f96,plain,(
% 9.14/11.52 ~smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))|~hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)),
% 9.14/11.52 inference(cnf_transformation,[status(thm)],[f44])).
% 9.14/11.52 fof(f97,definition,(
% 9.14/11.52 sQ0_spl <=> (smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f99,plain,(
% 9.14/11.52 ~smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))|sQ0_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f97])).
% 9.14/11.52 fof(f100,definition,(
% 9.14/11.52 sQ1_spl <=> (hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f102,plain,(
% 9.14/11.52 ~hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)|sQ1_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f100])).
% 9.14/11.52 fof(f103,plain,(
% 9.14/11.52 ~sQ0_spl|~sQ1_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f96,f97,f100])).
% 9.14/11.52 fof(f104,plain,(
% 9.14/11.52 ![X0]: (smaller_or_equal(X0,X0))),
% 9.14/11.52 inference(destructive_equality_resolution,[status(thm)],[f47])).
% 9.14/11.52 fof(f119,plain,(
% 9.14/11.52 smaller(zero,sigma)),
% 9.14/11.52 inference(resolution,[status(thm)],[f52,f91])).
% 9.14/11.52 fof(f120,plain,(
% 9.14/11.52 smaller(mod1,mod2)),
% 9.14/11.52 inference(resolution,[status(thm)],[f52,f86])).
% 9.14/11.52 fof(f121,plain,(
% 9.14/11.52 ~greater(zero,sigma)),
% 9.14/11.52 inference(resolution,[status(thm)],[f53,f91])).
% 9.14/11.52 fof(f132,plain,(
% 9.14/11.52 smaller_or_equal(zero,sigma)),
% 9.14/11.52 inference(resolution,[status(thm)],[f119,f46])).
% 9.14/11.52 fof(f137,plain,(
% 9.14/11.52 ![X0,X1,X2]: (smaller(X0,X1)|X0=X1|~greater(X1,X2)|greater(X0,X2))),
% 9.14/11.52 inference(resolution,[status(thm)],[f56,f55])).
% 9.14/11.52 fof(f139,plain,(
% 9.14/11.52 ![X0,X1]: (smaller(X0,X1)|X0=X1|smaller(X1,X0))),
% 9.14/11.52 inference(resolution,[status(thm)],[f56,f52])).
% 9.14/11.52 fof(f160,plain,(
% 9.14/11.52 ![X0]: (~age(sk2,X0)=zero|is_aligned(sk2,X0))),
% 9.14/11.52 inference(resolution,[status(thm)],[f71,f87])).
% 9.14/11.52 fof(f164,definition,(
% 9.14/11.52 sQ9_spl <=> (organization(sk2))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f166,plain,(
% 9.14/11.52 ~organization(sk2)|sQ9_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f164])).
% 9.14/11.52 fof(f192,plain,(
% 9.14/11.52 ![X0,X1,X2]: (~age(X0,X1)=zero|~dissimilar(X0,X1,X2)|greater(age(X0,X2),sigma))),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f74,f60])).
% 9.14/11.52 fof(f193,plain,(
% 9.14/11.52 ![X0,X1]: (~robust_position(X0)|~smaller_or_equal(age(X0,X1),sigma)|~positional_advantage(X0,X1))),
% 9.14/11.52 inference(forward_demodulation,[status(thm)],[f93,f75])).
% 9.14/11.52 fof(f194,plain,(
% 9.14/11.52 ~robust_position(sk2)|~smaller_or_equal(zero,sigma)|~positional_advantage(sk2,sk3)),
% 9.14/11.52 inference(paramodulation,[status(thm)],[f90,f193])).
% 9.14/11.52 fof(f195,definition,(
% 9.14/11.52 sQ13_spl <=> (robust_position(sk2))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f197,plain,(
% 9.14/11.52 ~robust_position(sk2)|sQ13_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f195])).
% 9.14/11.52 fof(f198,definition,(
% 9.14/11.52 sQ14_spl <=> (smaller_or_equal(zero,sigma))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f200,plain,(
% 9.14/11.52 ~smaller_or_equal(zero,sigma)|sQ14_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f198])).
% 9.14/11.52 fof(f201,definition,(
% 9.14/11.52 sQ15_spl <=> (positional_advantage(sk2,sk3))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f204,plain,(
% 9.14/11.52 ~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f194,f195,f198,f201])).
% 9.14/11.52 fof(f205,plain,(
% 9.14/11.52 $false|sQ14_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f200,f132])).
% 9.14/11.52 fof(f206,plain,(
% 9.14/11.52 sQ14_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f205])).
% 9.14/11.52 fof(f207,plain,(
% 9.14/11.52 $false|sQ13_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f197,f88])).
% 9.14/11.52 fof(f208,plain,(
% 9.14/11.52 sQ13_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f207])).
% 9.14/11.52 fof(f210,definition,(
% 9.14/11.52 sQ16_spl <=> (smaller(zero,zero))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f211,plain,(
% 9.14/11.52 smaller(zero,zero)|~sQ16_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f210])).
% 9.14/11.52 fof(f212,plain,(
% 9.14/11.52 ~smaller(zero,zero)|sQ16_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f210])).
% 9.14/11.52 fof(f213,definition,(
% 9.14/11.52 sQ17_spl <=> (zero=zero)),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f219,plain,(
% 9.14/11.52 ![X0,X1]: (~robust_position(X0)|~greater(age(X0,X1),sigma)|positional_advantage(X0,X1))),
% 9.14/11.52 inference(forward_demodulation,[status(thm)],[f93,f76])).
% 9.14/11.52 fof(f220,plain,(
% 9.14/11.52 ~robust_position(sk2)|positional_advantage(sk2,sk5)),
% 9.14/11.52 inference(resolution,[status(thm)],[f219,f95])).
% 9.14/11.52 fof(f223,definition,(
% 9.14/11.52 sQ18_spl <=> (positional_advantage(sk2,sk5))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f224,plain,(
% 9.14/11.52 positional_advantage(sk2,sk5)|~sQ18_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f223])).
% 9.14/11.52 fof(f226,plain,(
% 9.14/11.52 ~sQ13_spl|sQ18_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f220,f195,f223])).
% 9.14/11.52 fof(f245,plain,(
% 9.14/11.52 ![X0]: (smaller_or_equal(age(X0,sk1(X0)),sigma)|greater(age(X0,sk1(X0)),tau)|robust_position(X0))),
% 9.14/11.52 inference(forward_demodulation,[status(thm)],[f93,f77])).
% 9.14/11.52 fof(f246,plain,(
% 9.14/11.52 ![X0]: (smaller_or_equal(age(X0,sk1(X0)),sigma)|greater(age(X0,sk1(X0)),sigma)|robust_position(X0))),
% 9.14/11.52 inference(forward_demodulation,[status(thm)],[f93,f245])).
% 9.14/11.52 fof(f248,plain,(
% 9.14/11.52 ![X0,X1]: (smaller_or_equal(age(X0,sk1(X0)),sigma)|robust_position(X0)|~greater(sigma,X1)|greater(age(X0,sk1(X0)),X1))),
% 9.14/11.52 inference(resolution,[status(thm)],[f246,f55])).
% 9.14/11.52 fof(f249,plain,(
% 9.14/11.52 ![X0]: (smaller_or_equal(age(X0,sk1(X0)),sigma)|robust_position(X0)|~greater(sigma,age(X0,sk1(X0))))),
% 9.14/11.52 inference(resolution,[status(thm)],[f246,f53])).
% 9.14/11.52 fof(f253,plain,(
% 9.14/11.52 greater(zero,zero)|~sQ16_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f211,f51])).
% 9.14/11.52 fof(f255,plain,(
% 9.14/11.52 ![X0]: (positional_advantage(X0,sk1(X0))|greater(age(X0,sk1(X0)),sigma)|robust_position(X0))),
% 9.14/11.52 inference(forward_demodulation,[status(thm)],[f93,f79])).
% 9.14/11.52 fof(f257,plain,(
% 9.14/11.52 ![X0,X1]: (positional_advantage(X0,sk1(X0))|robust_position(X0)|~greater(sigma,X1)|greater(age(X0,sk1(X0)),X1))),
% 9.14/11.52 inference(resolution,[status(thm)],[f255,f55])).
% 9.14/11.52 fof(f258,plain,(
% 9.14/11.52 ![X0]: (positional_advantage(X0,sk1(X0))|robust_position(X0)|~greater(sigma,age(X0,sk1(X0))))),
% 9.14/11.52 inference(resolution,[status(thm)],[f255,f53])).
% 9.14/11.52 fof(f262,definition,(
% 9.14/11.52 sQ22_spl <=> (has_immunity(sk2,sk5))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f263,plain,(
% 9.14/11.52 has_immunity(sk2,sk5)|~sQ22_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f262])).
% 9.14/11.52 fof(f265,definition,(
% 9.14/11.52 sQ23_spl <=> (is_aligned(sk2,sk5))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f272,plain,(
% 9.14/11.52 $false|sQ9_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f166,f87])).
% 9.14/11.52 fof(f273,plain,(
% 9.14/11.52 sQ9_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f272])).
% 9.14/11.52 fof(f274,plain,(
% 9.14/11.52 ~robust_position(sk2)|~positional_advantage(sk2,sk4)),
% 9.14/11.52 inference(resolution,[status(thm)],[f94,f193])).
% 9.14/11.52 fof(f276,definition,(
% 9.14/11.52 sQ25_spl <=> (positional_advantage(sk2,sk4))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f279,plain,(
% 9.14/11.52 ~sQ13_spl|~sQ25_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f274,f195,f276])).
% 9.14/11.52 fof(f290,definition,(
% 9.14/11.52 ![X0]: (sQ26_spl <=> (~age(sk2,X0)=zero|dissimilar(sk2,X0,sk5)))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f291,plain,(
% 9.14/11.52 ![X0]: (~age(sk2,X0)=zero|dissimilar(sk2,X0,sk5)|~sQ26_spl)),
% 9.14/11.52 inference(component_clause,[status(thm)],[f290])).
% 9.14/11.52 fof(f302,plain,(
% 9.14/11.52 ~organization(sk2)|has_immunity(sk2,sk5)|is_aligned(sk2,sk5)|hazard_of_mortality(sk2,sk5)=mod1|~sQ18_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f83,f224])).
% 9.14/11.52 fof(f303,definition,(
% 9.14/11.52 sQ27_spl <=> (hazard_of_mortality(sk2,sk5)=mod1)),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f304,plain,(
% 9.14/11.52 hazard_of_mortality(sk2,sk5)=mod1|~sQ27_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f303])).
% 9.14/11.52 fof(f306,plain,(
% 9.14/11.52 ~sQ9_spl|sQ22_spl|sQ23_spl|sQ27_spl|~sQ18_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f302,f164,f262,f265,f303,f223])).
% 9.14/11.52 fof(f309,plain,(
% 9.14/11.52 ~organization(sk2)|has_endowment(sk2)|~sQ22_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f263,f58])).
% 9.14/11.52 fof(f314,definition,(
% 9.14/11.52 sQ29_spl <=> (has_endowment(sk2))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f315,plain,(
% 9.14/11.52 has_endowment(sk2)|~sQ29_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f314])).
% 9.14/11.52 fof(f317,plain,(
% 9.14/11.52 ~sQ9_spl|sQ29_spl|~sQ22_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f309,f164,f314,f262])).
% 9.14/11.52 fof(f318,plain,(
% 9.14/11.52 $false|~sQ29_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f315,f89])).
% 9.14/11.52 fof(f319,plain,(
% 9.14/11.52 ~sQ29_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f318])).
% 9.14/11.52 fof(f330,plain,(
% 9.14/11.52 ![X0]: (smaller(X0,age(sk2,sk5))|X0=age(sk2,sk5)|greater(X0,sigma))),
% 9.14/11.52 inference(resolution,[status(thm)],[f137,f95])).
% 9.14/11.52 fof(f358,plain,(
% 9.14/11.52 is_aligned(sk2,sk3)),
% 9.14/11.52 inference(resolution,[status(thm)],[f160,f90])).
% 9.14/11.52 fof(f359,plain,(
% 9.14/11.52 ~zero=zero|is_aligned(sk2,sk3)),
% 9.14/11.52 inference(paramodulation,[status(thm)],[f90,f160])).
% 9.14/11.52 fof(f360,definition,(
% 9.14/11.52 sQ32_spl <=> (is_aligned(sk2,sk3))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f363,plain,(
% 9.14/11.52 ~sQ17_spl|sQ32_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f359,f213,f360])).
% 9.14/11.52 fof(f370,plain,(
% 9.14/11.52 ~organization(sk2)|has_immunity(sk2,sk3)|positional_advantage(sk2,sk3)|hazard_of_mortality(sk2,sk3)=mod2),
% 9.14/11.52 inference(resolution,[status(thm)],[f358,f84])).
% 9.14/11.52 fof(f372,plain,(
% 9.14/11.52 ![X0]: (~organization(sk2)|is_aligned(sk2,X0)|dissimilar(sk2,sk3,X0))),
% 9.14/11.52 inference(resolution,[status(thm)],[f358,f67])).
% 9.14/11.52 fof(f373,definition,(
% 9.14/11.52 sQ33_spl <=> (has_immunity(sk2,sk3))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f374,plain,(
% 9.14/11.52 has_immunity(sk2,sk3)|~sQ33_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f373])).
% 9.14/11.52 fof(f376,definition,(
% 9.14/11.52 sQ34_spl <=> (hazard_of_mortality(sk2,sk3)=mod2)),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f377,plain,(
% 9.14/11.52 hazard_of_mortality(sk2,sk3)=mod2|~sQ34_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f376])).
% 9.14/11.52 fof(f379,plain,(
% 9.14/11.52 ~sQ9_spl|sQ33_spl|sQ15_spl|sQ34_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f370,f164,f373,f201,f376])).
% 9.14/11.52 fof(f384,definition,(
% 9.14/11.52 ![X0]: (sQ36_spl <=> (is_aligned(sk2,X0)|dissimilar(sk2,sk3,X0)))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f385,plain,(
% 9.14/11.52 ![X0]: (is_aligned(sk2,X0)|dissimilar(sk2,sk3,X0)|~sQ36_spl)),
% 9.14/11.52 inference(component_clause,[status(thm)],[f384])).
% 9.14/11.52 fof(f387,plain,(
% 9.14/11.52 ~sQ9_spl|sQ36_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f372,f164,f384])).
% 9.14/11.52 fof(f394,definition,(
% 9.14/11.52 sQ38_spl <=> (sigma=age(sk2,sk5))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f395,plain,(
% 9.14/11.52 sigma=age(sk2,sk5)|~sQ38_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f394])).
% 9.14/11.52 fof(f403,plain,(
% 9.14/11.52 ~greater(zero,zero)|~sQ16_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f253,f53])).
% 9.14/11.52 fof(f406,plain,(
% 9.14/11.52 $false|~sQ16_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f403,f253])).
% 9.14/11.52 fof(f407,plain,(
% 9.14/11.52 ~sQ16_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f406])).
% 9.14/11.52 fof(f417,plain,(
% 9.14/11.52 ~organization(sk2)|has_endowment(sk2)|~sQ33_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f374,f58])).
% 9.14/11.52 fof(f422,plain,(
% 9.14/11.52 ~sQ9_spl|sQ29_spl|~sQ33_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f417,f164,f314,f373])).
% 9.14/11.52 fof(f424,plain,(
% 9.14/11.52 smaller(zero,zero)|zero=zero|sQ16_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f212,f139])).
% 9.14/11.52 fof(f427,plain,(
% 9.14/11.52 sQ16_spl|sQ17_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f424,f210,f213])).
% 9.14/11.52 fof(f430,plain,(
% 9.14/11.52 ![X0,X1]: (smaller_or_equal(age(X0,sk1(X0)),sigma)|robust_position(X0)|greater(age(X0,sk1(X0)),X1)|smaller(sigma,X1)|sigma=X1)),
% 9.14/11.52 inference(resolution,[status(thm)],[f248,f56])).
% 9.14/11.52 fof(f476,plain,(
% 9.14/11.52 ![X0,X1]: (positional_advantage(X0,sk1(X0))|robust_position(X0)|greater(age(X0,sk1(X0)),X1)|smaller(sigma,X1)|sigma=X1)),
% 9.14/11.52 inference(resolution,[status(thm)],[f257,f56])).
% 9.14/11.52 fof(f520,plain,(
% 9.14/11.52 dissimilar(sk2,sk3,sk5)|~sQ26_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f291,f90])).
% 9.14/11.52 fof(f531,definition,(
% 9.14/11.52 sQ48_spl <=> (has_immunity(sk2,sk4))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f532,plain,(
% 9.14/11.52 has_immunity(sk2,sk4)|~sQ48_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f531])).
% 9.14/11.52 fof(f534,definition,(
% 9.14/11.52 sQ49_spl <=> (is_aligned(sk2,sk4))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f535,plain,(
% 9.14/11.52 is_aligned(sk2,sk4)|~sQ49_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f534])).
% 9.14/11.52 fof(f565,plain,(
% 9.14/11.52 ~organization(sk2)|has_immunity(sk2,sk4)|positional_advantage(sk2,sk4)|hazard_of_mortality(sk2,sk4)=mod2|~sQ49_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f535,f84])).
% 9.14/11.52 fof(f568,definition,(
% 9.14/11.52 sQ57_spl <=> (hazard_of_mortality(sk2,sk4)=mod2)),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f569,plain,(
% 9.14/11.52 hazard_of_mortality(sk2,sk4)=mod2|~sQ57_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f568])).
% 9.14/11.52 fof(f571,plain,(
% 9.14/11.52 ~sQ9_spl|sQ48_spl|sQ25_spl|sQ57_spl|~sQ49_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f565,f164,f531,f276,f568,f534])).
% 9.14/11.52 fof(f600,definition,(
% 9.14/11.52 sQ63_spl <=> (greater(sigma,sigma))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f601,plain,(
% 9.14/11.52 greater(sigma,sigma)|~sQ63_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f600])).
% 9.14/11.52 fof(f605,definition,(
% 9.14/11.52 sQ64_spl <=> (smaller_or_equal(sigma,sigma))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f607,plain,(
% 9.14/11.52 ~smaller_or_equal(sigma,sigma)|sQ64_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f605])).
% 9.14/11.52 fof(f611,plain,(
% 9.14/11.52 ~organization(sk2)|has_endowment(sk2)|~sQ48_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f532,f58])).
% 9.14/11.52 fof(f616,plain,(
% 9.14/11.52 ~sQ9_spl|sQ29_spl|~sQ48_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f611,f164,f314,f531])).
% 9.14/11.52 fof(f750,plain,(
% 9.14/11.52 ![X0]: (X0=age(sk2,sk5)|greater(X0,sigma)|greater(age(sk2,sk5),X0))),
% 9.14/11.52 inference(resolution,[status(thm)],[f330,f51])).
% 9.14/11.52 fof(f866,definition,(
% 9.14/11.52 sQ80_spl <=> (greater(mod1,mod1))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f867,plain,(
% 9.14/11.52 greater(mod1,mod1)|~sQ80_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f866])).
% 9.14/11.52 fof(f1049,plain,(
% 9.14/11.52 ~robust_position(sk2)|~smaller_or_equal(sigma,sigma)|~positional_advantage(sk2,sk5)|~sQ38_spl),
% 9.14/11.52 inference(paramodulation,[status(thm)],[f395,f193])).
% 9.14/11.52 fof(f1059,plain,(
% 9.14/11.52 ~sQ13_spl|~sQ64_spl|~sQ18_spl|~sQ38_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f1049,f195,f605,f223,f394])).
% 9.14/11.52 fof(f1060,plain,(
% 9.14/11.52 $false|sQ64_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f607,f104])).
% 9.14/11.52 fof(f1061,plain,(
% 9.14/11.52 sQ64_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f1060])).
% 9.14/11.52 fof(f1158,plain,(
% 9.14/11.52 ![X0,X1,X2]: (smaller_or_equal(age(X0,sk1(X0)),sigma)|robust_position(X0)|smaller(sigma,X1)|sigma=X1|smaller(X2,age(X0,sk1(X0)))|X2=age(X0,sk1(X0))|greater(X2,X1))),
% 9.14/11.52 inference(resolution,[status(thm)],[f430,f137])).
% 9.14/11.52 fof(f1283,plain,(
% 9.14/11.52 ![X0,X1,X2]: (positional_advantage(X0,sk1(X0))|robust_position(X0)|smaller(sigma,X1)|sigma=X1|smaller(X2,age(X0,sk1(X0)))|X2=age(X0,sk1(X0))|greater(X2,X1))),
% 9.14/11.52 inference(resolution,[status(thm)],[f476,f137])).
% 9.14/11.52 fof(f1304,definition,(
% 9.14/11.52 sQ113_spl <=> (age(sk2,sk3)=zero)),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f1306,plain,(
% 9.14/11.52 ~age(sk2,sk3)=zero|sQ113_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f1304])).
% 9.14/11.52 fof(f1316,plain,(
% 9.14/11.52 ~zero=zero|sQ113_spl),
% 9.14/11.52 inference(forward_demodulation,[status(thm)],[f90,f1306])).
% 9.14/11.52 fof(f1317,plain,(
% 9.14/11.52 $false|sQ113_spl),
% 9.14/11.52 inference(trivial_equality_resolution,[status(thm)],[f1316])).
% 9.14/11.52 fof(f1318,plain,(
% 9.14/11.52 sQ113_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f1317])).
% 9.14/11.52 fof(f1357,plain,(
% 9.14/11.52 ~is_aligned(sk2,sk3)|~is_aligned(sk2,sk5)|~sQ26_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f520,f64])).
% 9.14/11.52 fof(f1361,plain,(
% 9.14/11.52 ~sQ32_spl|~sQ23_spl|~sQ26_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f1357,f360,f265,f290])).
% 9.14/11.52 fof(f1469,plain,(
% 9.14/11.52 ~smaller(mod1,hazard_of_mortality(sk2,sk4))|~sQ27_spl|sQ0_spl),
% 9.14/11.52 inference(forward_demodulation,[status(thm)],[f304,f99])).
% 9.14/11.52 fof(f1509,definition,(
% 9.14/11.52 sQ134_spl <=> (dissimilar(sk2,sk3,sk4))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f1510,plain,(
% 9.14/11.52 dissimilar(sk2,sk3,sk4)|~sQ134_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f1509])).
% 9.14/11.52 fof(f1511,plain,(
% 9.14/11.52 ~dissimilar(sk2,sk3,sk4)|sQ134_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f1509])).
% 9.14/11.52 fof(f1561,plain,(
% 9.14/11.52 ~smaller(mod1,mod2)|~sQ57_spl|~sQ27_spl|sQ0_spl),
% 9.14/11.52 inference(backward_demodulation,[status(thm)],[f569,f1469])).
% 9.14/11.52 fof(f1562,plain,(
% 9.14/11.52 $false|~sQ57_spl|~sQ27_spl|sQ0_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f1561,f120])).
% 9.14/11.52 fof(f1563,plain,(
% 9.14/11.52 ~sQ57_spl|~sQ27_spl|sQ0_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f1562])).
% 9.14/11.52 fof(f1565,plain,(
% 9.14/11.52 ~hazard_of_mortality(sk2,sk4)=mod2|~sQ34_spl|sQ1_spl),
% 9.14/11.52 inference(forward_demodulation,[status(thm)],[f377,f102])).
% 9.14/11.52 fof(f1934,plain,(
% 9.14/11.52 ~sQ57_spl|~sQ34_spl|sQ1_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f1565,f568,f376,f100])).
% 9.14/11.52 fof(f2084,plain,(
% 9.14/11.52 ~age(sk2,sk3)=zero|greater(age(sk2,sk4),sigma)|~sQ134_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f1510,f192])).
% 9.14/11.52 fof(f2088,definition,(
% 9.14/11.52 sQ166_spl <=> (greater(age(sk2,sk4),sigma))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f2089,plain,(
% 9.14/11.52 greater(age(sk2,sk4),sigma)|~sQ166_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f2088])).
% 9.14/11.52 fof(f2091,plain,(
% 9.14/11.52 ~sQ113_spl|sQ166_spl|~sQ134_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f2084,f1304,f2088,f1509])).
% 9.14/11.52 fof(f4869,plain,(
% 9.14/11.52 ![X0]: (sigma=age(sk2,sk5)|greater(sigma,sigma)|~organization(sk2)|~age(sk2,X0)=zero|dissimilar(sk2,X0,sk5))),
% 9.14/11.52 inference(resolution,[status(thm)],[f750,f72])).
% 9.14/11.52 fof(f4878,plain,(
% 9.14/11.52 sQ38_spl|sQ63_spl|~sQ9_spl|sQ26_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f4869,f394,f600,f164,f290])).
% 9.14/11.52 fof(f4990,plain,(
% 9.14/11.52 ~greater(sigma,sigma)|~sQ63_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f601,f53])).
% 9.14/11.52 fof(f4995,plain,(
% 9.14/11.52 ~sQ63_spl),
% 9.14/11.52 inference(split_clause,[status(thm)],[f4990,f600])).
% 9.14/11.52 fof(f5408,plain,(
% 9.14/11.52 ~greater(mod1,mod1)|~sQ80_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f867,f53])).
% 9.14/11.52 fof(f5412,plain,(
% 9.14/11.52 $false|~sQ80_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f5408,f867])).
% 9.14/11.52 fof(f5413,plain,(
% 9.14/11.52 ~sQ80_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f5412])).
% 9.14/11.52 fof(f5464,definition,(
% 9.14/11.52 sQ310_spl <=> (smaller(sigma,zero))),
% 9.14/11.52 introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition])).
% 9.14/11.52 fof(f5465,plain,(
% 9.14/11.52 smaller(sigma,zero)|~sQ310_spl),
% 9.14/11.52 inference(component_clause,[status(thm)],[f5464])).
% 9.14/11.52 fof(f5513,plain,(
% 9.14/11.52 greater(zero,sigma)|~sQ310_spl),
% 9.14/11.52 inference(resolution,[status(thm)],[f5465,f51])).
% 9.14/11.52 fof(f5515,plain,(
% 9.14/11.52 $false|~sQ310_spl),
% 9.14/11.52 inference(forward_subsumption_resolution,[status(thm)],[f5513,f121])).
% 9.14/11.52 fof(f5516,plain,(
% 9.14/11.52 ~sQ310_spl),
% 9.14/11.52 inference(contradiction_clause,[status(thm)],[f5515])).
% 9.14/11.52 fof(f8492,definition,(
% 9.14/11.53 ![X0]: (sQ489_spl <=> (smaller(sigma,age(X0,sk1(X0)))|sigma=age(X0,sk1(X0))|positional_advantage(X0,sk1(X0))|robust_position(X0)))),
% 9.14/11.53 introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition])).
% 9.14/11.53 fof(f8496,definition,(
% 9.14/11.53 ![X0]: (sQ490_spl <=> (smaller(sigma,age(X0,sk1(X0)))|sigma=age(X0,sk1(X0))|smaller_or_equal(age(X0,sk1(X0)),sigma)|robust_position(X0)))),
% 9.14/11.53 introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition])).
% 9.14/11.53 fof(f9071,plain,(
% 9.14/11.53 ![X0,X1]: (smaller_or_equal(age(X0,sk1(X0)),sigma)|robust_position(X0)|smaller(sigma,age(X1,sk1(X1)))|sigma=age(X1,sk1(X1))|smaller(sigma,age(X0,sk1(X0)))|sigma=age(X0,sk1(X0))|smaller_or_equal(age(X1,sk1(X1)),sigma)|robust_position(X1))),
% 9.14/11.53 inference(resolution,[status(thm)],[f1158,f249])).
% 9.14/11.53 fof(f9108,plain,(
% 9.14/11.53 sQ490_spl),
% 9.14/11.53 inference(split_clause,[status(thm)],[f9071,f8496])).
% 9.14/11.53 fof(f9630,plain,(
% 9.14/11.53 ![X0,X1]: (positional_advantage(X0,sk1(X0))|robust_position(X0)|smaller(sigma,age(X1,sk1(X1)))|sigma=age(X1,sk1(X1))|smaller(sigma,age(X0,sk1(X0)))|sigma=age(X0,sk1(X0))|positional_advantage(X1,sk1(X1))|robust_position(X1))),
% 9.14/11.53 inference(resolution,[status(thm)],[f1283,f258])).
% 9.14/11.53 fof(f9671,plain,(
% 9.14/11.53 sQ489_spl),
% 9.14/11.53 inference(split_clause,[status(thm)],[f9630,f8492])).
% 9.14/11.53 fof(f13536,plain,(
% 9.14/11.53 ~robust_position(sk2)|positional_advantage(sk2,sk4)|~sQ166_spl),
% 9.14/11.53 inference(resolution,[status(thm)],[f2089,f219])).
% 9.14/11.53 fof(f13551,plain,(
% 9.14/11.53 ~sQ13_spl|sQ25_spl|~sQ166_spl),
% 9.14/11.53 inference(split_clause,[status(thm)],[f13536,f195,f276,f2088])).
% 9.14/11.53 fof(f13566,plain,(
% 9.14/11.53 is_aligned(sk2,sk4)|sQ134_spl|~sQ36_spl),
% 9.14/11.53 inference(resolution,[status(thm)],[f1511,f385])).
% 9.14/11.53 fof(f13567,plain,(
% 9.14/11.53 sQ49_spl|sQ134_spl|~sQ36_spl),
% 9.14/11.53 inference(split_clause,[status(thm)],[f13566,f534,f1509,f384])).
% 9.14/11.53 fof(f13568,plain,(
% 9.14/11.53 $false),
% 9.14/11.53 inference(sat_refutation,[status(thm)],[f103,f204,f206,f208,f226,f273,f279,f306,f317,f319,f363,f379,f387,f407,f422,f427,f571,f616,f1059,f1061,f1318,f1361,f1563,f1934,f2091,f4878,f4995,f5413,f5516,f9108,f9671,f13551,f13567])).
% 9.14/11.53 % SZS output end CNFRefutation for theBenchmark.p
% 9.14/11.53 % Elapsed time: 1.218192 seconds
% 9.14/11.53 % CPU time: 9.530434 seconds
% 9.14/11.53 % Total memory used: 188.454 MB
% 9.14/11.53 % Net memory used: 170.862 MB
%------------------------------------------------------------------------------