%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT047-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 : n013.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:49 PM UTC 2026
% Result : Unsatisfiable 22.05s 3.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT047-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n013.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 01:23:22 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 22.05/3.25 % Refutation found
% 22.05/3.25 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 22.05/3.25 % SZS output start CNFRefutation for theBenchmark
% 22.05/3.25 fof(f1,axiom,(
% 22.05/3.25 (![A,B]: (( ~ smaller_or_equal(A,B)| smaller(A,B)| A = B ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f2,axiom,(
% 22.05/3.25 (![A,B]: (( ~ smaller(A,B)| smaller_or_equal(A,B) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f3,axiom,(
% 22.05/3.25 (![A,B]: (( A != B| smaller_or_equal(A,B) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f4,axiom,(
% 22.05/3.25 (![A,B]: (( ~ greater_or_equal(A,B)| greater(A,B)| A = B ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f5,axiom,(
% 22.05/3.25 (![A,B]: (( ~ greater(A,B)| greater_or_equal(A,B) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f7,axiom,(
% 22.05/3.25 (![A,B]: (( ~ smaller(A,B)| greater(B,A) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f8,axiom,(
% 22.05/3.25 (![A,B]: (( ~ greater(A,B)| smaller(B,A) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f9,axiom,(
% 22.05/3.25 (![A,B]: (( ~ greater(A,B)| ~ greater(B,A) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f10,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ greater(A,B)| ~ greater(B,C)| greater(A,C) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f11,axiom,(
% 22.05/3.25 (![A,B]: (( smaller(A,B)| A = B| greater(A,B) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f13,axiom,(
% 22.05/3.25 (![A,B]: (( ~ has_endowment(A)| ~ smaller_or_equal(age(A,B),eta)| has_immunity(A,B) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f14,axiom,(
% 22.05/3.25 (![A,B]: (( ~ has_endowment(A)| ~ greater(age(A,B),eta)| ~ has_immunity(A,B) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f19,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| ~ has_immunity(A,B)| ~ has_immunity(A,C)| hazard_of_mortality(A,B) = hazard_of_mortality(A,C) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f20,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| ~ has_immunity(A,B)| has_immunity(A,C)| greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f21,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| has_immunity(A,B)| has_immunity(A,C)| ~ greater(capability(A,C),capability(A,B))| ~ greater_or_equal(position(A,C),position(A,B))| smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f22,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| has_immunity(A,B)| has_immunity(A,C)| ~ greater_or_equal(capability(A,C),capability(A,B))| ~ greater(position(A,C),position(A,B))| smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f24,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| ~ greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))| ~ smaller_or_equal(internal_friction(A,B),internal_friction(A,C))| greater(capability(A,B),capability(A,C)) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f25,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| ~ smaller_or_equal(stock_of_knowledge(A,B),stock_of_knowledge(A,C))| ~ greater(internal_friction(A,B),internal_friction(A,C))| smaller(capability(A,B),capability(A,C)) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f26,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| stock_of_knowledge(A,B) != stock_of_knowledge(A,C)| internal_friction(A,B) != internal_friction(A,C)| capability(A,B) = capability(A,C) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f27,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| ~ greater(external_ties(A,B),external_ties(A,C))| greater(position(A,B),position(A,C)) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f28,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| external_ties(A,B) != external_ties(A,C)| position(A,B) = position(A,C) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f29,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| ~ greater(age(A,B),age(A,C))| greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C)) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f30,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| ~ greater(age(A,B),age(A,C))| greater(external_ties(A,B),external_ties(A,C)) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f31,axiom,(
% 22.05/3.25 (![A,B,C]: (( ~ organization(A)| internal_friction(A,B) = internal_friction(A,C) ) ))),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f32,negated_conjecture,(
% 22.05/3.25 organization(sk2) ),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f33,negated_conjecture,(
% 22.05/3.25 has_endowment(sk2) ),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f34,negated_conjecture,(
% 22.05/3.25 smaller_or_equal(age(sk2,sk3),age(sk2,sk4)) ),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f35,negated_conjecture,(
% 22.05/3.25 smaller_or_equal(age(sk2,sk4),eta) ),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f36,negated_conjecture,(
% 22.05/3.25 greater(age(sk2,sk5),eta) ),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f37,negated_conjecture,(
% 22.05/3.25 greater(age(sk2,sk6),age(sk2,sk5)) ),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f38,negated_conjecture,(
% 22.05/3.25 ( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))| ~ greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4))| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ),
% 22.05/3.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.05/3.25 fof(f39,plain,(
% 22.05/3.25 ![X0,X1]: (~smaller_or_equal(X0,X1)|smaller(X0,X1)|X0=X1)),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f1])).
% 22.05/3.25 fof(f40,plain,(
% 22.05/3.25 ![X0,X1]: (~smaller(X0,X1)|smaller_or_equal(X0,X1))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f2])).
% 22.05/3.25 fof(f41,plain,(
% 22.05/3.25 ![X0,X1]: (~X0=X1|smaller_or_equal(X0,X1))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f3])).
% 22.05/3.25 fof(f42,plain,(
% 22.05/3.25 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f4])).
% 22.05/3.25 fof(f43,plain,(
% 22.05/3.25 ![X0,X1]: (~greater(X0,X1)|greater_or_equal(X0,X1))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f5])).
% 22.05/3.25 fof(f45,plain,(
% 22.05/3.25 ![X0,X1]: (~smaller(X0,X1)|greater(X1,X0))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f7])).
% 22.05/3.25 fof(f46,plain,(
% 22.05/3.25 ![X0,X1]: (~greater(X0,X1)|smaller(X1,X0))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f8])).
% 22.05/3.25 fof(f47,plain,(
% 22.05/3.25 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f9])).
% 22.05/3.25 fof(f48,plain,(
% 22.05/3.25 ![A,C]: ((![B]: (~greater(A,B)|~greater(B,C)))|greater(A,C))),
% 22.05/3.25 inference(miniscoping,[status(thm)],[f10])).
% 22.05/3.25 fof(f49,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f48])).
% 22.05/3.25 fof(f50,plain,(
% 22.05/3.25 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater(X0,X1))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f11])).
% 22.05/3.25 fof(f52,plain,(
% 22.05/3.25 ![X0,X1]: (~has_endowment(X0)|~smaller_or_equal(age(X0,X1),eta)|has_immunity(X0,X1))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f13])).
% 22.05/3.25 fof(f53,plain,(
% 22.05/3.25 ![X0,X1]: (~has_endowment(X0)|~greater(age(X0,X1),eta)|~has_immunity(X0,X1))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f14])).
% 22.05/3.25 fof(f58,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~has_immunity(X0,X1)|~has_immunity(X0,X2)|hazard_of_mortality(X0,X1)=hazard_of_mortality(X0,X2))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f19])).
% 22.05/3.25 fof(f59,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~has_immunity(X0,X1)|has_immunity(X0,X2)|greater(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1)))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f20])).
% 22.05/3.25 fof(f60,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|has_immunity(X0,X1)|has_immunity(X0,X2)|~greater(capability(X0,X2),capability(X0,X1))|~greater_or_equal(position(X0,X2),position(X0,X1))|smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1)))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f21])).
% 22.05/3.25 fof(f61,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|has_immunity(X0,X1)|has_immunity(X0,X2)|~greater_or_equal(capability(X0,X2),capability(X0,X1))|~greater(position(X0,X2),position(X0,X1))|smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1)))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f22])).
% 22.05/3.25 fof(f63,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~greater(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))|~smaller_or_equal(internal_friction(X0,X1),internal_friction(X0,X2))|greater(capability(X0,X1),capability(X0,X2)))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f24])).
% 22.05/3.25 fof(f64,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~smaller_or_equal(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))|~greater(internal_friction(X0,X1),internal_friction(X0,X2))|smaller(capability(X0,X1),capability(X0,X2)))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f25])).
% 22.05/3.25 fof(f65,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~stock_of_knowledge(X0,X1)=stock_of_knowledge(X0,X2)|~internal_friction(X0,X1)=internal_friction(X0,X2)|capability(X0,X1)=capability(X0,X2))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f26])).
% 22.05/3.25 fof(f66,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~greater(external_ties(X0,X1),external_ties(X0,X2))|greater(position(X0,X1),position(X0,X2)))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f27])).
% 22.05/3.25 fof(f67,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~external_ties(X0,X1)=external_ties(X0,X2)|position(X0,X1)=position(X0,X2))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f28])).
% 22.05/3.25 fof(f68,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~greater(age(X0,X1),age(X0,X2))|greater(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2)))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f29])).
% 22.05/3.25 fof(f69,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~greater(age(X0,X1),age(X0,X2))|greater(external_ties(X0,X1),external_ties(X0,X2)))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f30])).
% 22.05/3.25 fof(f70,plain,(
% 22.05/3.25 ![A]: (~organization(A)|(![B,C]: internal_friction(A,B)=internal_friction(A,C)))),
% 22.05/3.25 inference(miniscoping,[status(thm)],[f31])).
% 22.05/3.25 fof(f71,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|internal_friction(X0,X1)=internal_friction(X0,X2))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f70])).
% 22.05/3.25 fof(f72,plain,(
% 22.05/3.25 organization(sk2)),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f32])).
% 22.05/3.25 fof(f73,plain,(
% 22.05/3.25 has_endowment(sk2)),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f33])).
% 22.05/3.25 fof(f74,plain,(
% 22.05/3.25 smaller_or_equal(age(sk2,sk3),age(sk2,sk4))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f34])).
% 22.05/3.25 fof(f75,plain,(
% 22.05/3.25 smaller_or_equal(age(sk2,sk4),eta)),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f35])).
% 22.05/3.25 fof(f76,plain,(
% 22.05/3.25 greater(age(sk2,sk5),eta)),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f36])).
% 22.05/3.25 fof(f77,plain,(
% 22.05/3.25 greater(age(sk2,sk6),age(sk2,sk5))),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f37])).
% 22.05/3.25 fof(f78,plain,(
% 22.05/3.25 ~greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))|~greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4))|~hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)),
% 22.05/3.25 inference(cnf_transformation,[status(thm)],[f38])).
% 22.05/3.25 fof(f79,definition,(
% 22.05/3.25 sQ0_spl <=> (greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f80,plain,(
% 22.05/3.25 greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))|~sQ0_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f79])).
% 22.05/3.25 fof(f82,definition,(
% 22.05/3.25 sQ1_spl <=> (greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f84,plain,(
% 22.05/3.25 ~greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4))|sQ1_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f82])).
% 22.05/3.25 fof(f85,definition,(
% 22.05/3.25 sQ2_spl <=> (hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f86,plain,(
% 22.05/3.25 hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)|~sQ2_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f85])).
% 22.05/3.25 fof(f87,plain,(
% 22.05/3.25 ~hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)|sQ2_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f85])).
% 22.05/3.25 fof(f88,plain,(
% 22.05/3.25 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f78,f79,f82,f85])).
% 22.05/3.25 fof(f89,plain,(
% 22.05/3.25 ![X0]: (smaller_or_equal(X0,X0))),
% 22.05/3.25 inference(destructive_equality_resolution,[status(thm)],[f41])).
% 22.05/3.25 fof(f91,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~stock_of_knowledge(X0,X1)=stock_of_knowledge(X0,X2)|capability(X0,X1)=capability(X0,X2))),
% 22.05/3.25 inference(backward_subsumption_resolution,[status(thm)],[f65,f71])).
% 22.05/3.25 fof(f92,plain,(
% 22.05/3.25 ~greater(age(sk2,sk5),age(sk2,sk6))),
% 22.05/3.25 inference(resolution,[status(thm)],[f47,f77])).
% 22.05/3.25 fof(f93,plain,(
% 22.05/3.25 ~greater(eta,age(sk2,sk5))),
% 22.05/3.25 inference(resolution,[status(thm)],[f47,f76])).
% 22.05/3.25 fof(f94,plain,(
% 22.05/3.25 ~has_endowment(sk2)|has_immunity(sk2,sk4)),
% 22.05/3.25 inference(resolution,[status(thm)],[f52,f75])).
% 22.05/3.25 fof(f95,definition,(
% 22.05/3.25 sQ3_spl <=> (has_endowment(sk2))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f97,plain,(
% 22.05/3.25 ~has_endowment(sk2)|sQ3_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f95])).
% 22.05/3.25 fof(f98,definition,(
% 22.05/3.25 sQ4_spl <=> (has_immunity(sk2,sk4))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f99,plain,(
% 22.05/3.25 has_immunity(sk2,sk4)|~sQ4_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f98])).
% 22.05/3.25 fof(f101,plain,(
% 22.05/3.25 ~sQ3_spl|sQ4_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f94,f95,f98])).
% 22.05/3.25 fof(f102,plain,(
% 22.05/3.25 $false|sQ3_spl),
% 22.05/3.25 inference(forward_subsumption_resolution,[status(thm)],[f97,f73])).
% 22.05/3.25 fof(f103,plain,(
% 22.05/3.25 sQ3_spl),
% 22.05/3.25 inference(contradiction_clause,[status(thm)],[f102])).
% 22.05/3.25 fof(f104,plain,(
% 22.05/3.25 ~has_endowment(sk2)|~has_immunity(sk2,sk5)),
% 22.05/3.25 inference(resolution,[status(thm)],[f53,f76])).
% 22.05/3.25 fof(f105,definition,(
% 22.05/3.25 sQ5_spl <=> (has_immunity(sk2,sk5))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f108,plain,(
% 22.05/3.25 ~sQ3_spl|~sQ5_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f104,f95,f105])).
% 22.05/3.25 fof(f109,plain,(
% 22.05/3.25 ![X0]: (~greater(X0,age(sk2,sk6))|greater(X0,age(sk2,sk5)))),
% 22.05/3.25 inference(resolution,[status(thm)],[f49,f77])).
% 22.05/3.25 fof(f110,plain,(
% 22.05/3.25 ![X0]: (~greater(X0,age(sk2,sk5))|greater(X0,eta))),
% 22.05/3.25 inference(resolution,[status(thm)],[f49,f76])).
% 22.05/3.25 fof(f119,plain,(
% 22.05/3.25 greater_or_equal(age(sk2,sk6),age(sk2,sk5))),
% 22.05/3.25 inference(resolution,[status(thm)],[f43,f77])).
% 22.05/3.25 fof(f120,plain,(
% 22.05/3.25 greater_or_equal(age(sk2,sk5),eta)),
% 22.05/3.25 inference(resolution,[status(thm)],[f43,f76])).
% 22.05/3.25 fof(f123,plain,(
% 22.05/3.25 greater(age(sk2,sk6),eta)),
% 22.05/3.25 inference(resolution,[status(thm)],[f110,f77])).
% 22.05/3.25 fof(f124,plain,(
% 22.05/3.25 ~has_endowment(sk2)|~has_immunity(sk2,sk6)),
% 22.05/3.25 inference(resolution,[status(thm)],[f123,f53])).
% 22.05/3.25 fof(f128,plain,(
% 22.05/3.25 ~greater(eta,age(sk2,sk6))),
% 22.05/3.25 inference(resolution,[status(thm)],[f123,f47])).
% 22.05/3.25 fof(f129,definition,(
% 22.05/3.25 sQ8_spl <=> (has_immunity(sk2,sk6))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f131,plain,(
% 22.05/3.25 ~has_immunity(sk2,sk6)|sQ8_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f129])).
% 22.05/3.25 fof(f132,plain,(
% 22.05/3.25 ~sQ3_spl|~sQ8_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f124,f95,f129])).
% 22.05/3.25 fof(f133,plain,(
% 22.05/3.25 ~organization(sk2)|greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5))),
% 22.05/3.25 inference(resolution,[status(thm)],[f68,f77])).
% 22.05/3.25 fof(f134,definition,(
% 22.05/3.25 sQ9_spl <=> (organization(sk2))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f136,plain,(
% 22.05/3.25 ~organization(sk2)|sQ9_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f134])).
% 22.05/3.25 fof(f137,definition,(
% 22.05/3.25 sQ10_spl <=> (greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f138,plain,(
% 22.05/3.25 greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5))|~sQ10_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f137])).
% 22.05/3.25 fof(f140,plain,(
% 22.05/3.25 ~sQ9_spl|sQ10_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f133,f134,f137])).
% 22.05/3.25 fof(f141,plain,(
% 22.05/3.25 $false|sQ9_spl),
% 22.05/3.25 inference(forward_subsumption_resolution,[status(thm)],[f136,f72])).
% 22.05/3.25 fof(f142,plain,(
% 22.05/3.25 sQ9_spl),
% 22.05/3.25 inference(contradiction_clause,[status(thm)],[f141])).
% 22.05/3.25 fof(f143,plain,(
% 22.05/3.25 ~organization(sk2)|greater(external_ties(sk2,sk6),external_ties(sk2,sk5))),
% 22.05/3.25 inference(resolution,[status(thm)],[f69,f77])).
% 22.05/3.25 fof(f144,definition,(
% 22.05/3.25 sQ11_spl <=> (greater(external_ties(sk2,sk6),external_ties(sk2,sk5)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f145,plain,(
% 22.05/3.25 greater(external_ties(sk2,sk6),external_ties(sk2,sk5))|~sQ11_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f144])).
% 22.05/3.25 fof(f147,plain,(
% 22.05/3.25 ~sQ9_spl|sQ11_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f143,f134,f144])).
% 22.05/3.25 fof(f149,plain,(
% 22.05/3.25 ![X0]: (~organization(sk2)|has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk4))|~sQ4_spl)),
% 22.05/3.25 inference(resolution,[status(thm)],[f99,f59])).
% 22.05/3.25 fof(f150,plain,(
% 22.05/3.25 ![X0]: (~organization(sk2)|~has_immunity(sk2,X0)|hazard_of_mortality(sk2,X0)=hazard_of_mortality(sk2,sk4)|~sQ4_spl)),
% 22.05/3.25 inference(resolution,[status(thm)],[f99,f58])).
% 22.05/3.25 fof(f151,definition,(
% 22.05/3.25 ![X0]: (sQ12_spl <=> (has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk4))))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f154,plain,(
% 22.05/3.25 ~sQ9_spl|sQ12_spl|~sQ4_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f149,f134,f151,f98])).
% 22.05/3.25 fof(f155,definition,(
% 22.05/3.25 ![X0]: (sQ13_spl <=> (~has_immunity(sk2,X0)|hazard_of_mortality(sk2,X0)=hazard_of_mortality(sk2,sk4)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f156,plain,(
% 22.05/3.25 ![X0]: (~has_immunity(sk2,X0)|hazard_of_mortality(sk2,X0)=hazard_of_mortality(sk2,sk4)|~sQ13_spl)),
% 22.05/3.25 inference(component_clause,[status(thm)],[f155])).
% 22.05/3.25 fof(f158,plain,(
% 22.05/3.25 ~sQ9_spl|sQ13_spl|~sQ4_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f150,f134,f155,f98])).
% 22.05/3.25 fof(f159,plain,(
% 22.05/3.25 smaller(age(sk2,sk3),age(sk2,sk4))|age(sk2,sk3)=age(sk2,sk4)),
% 22.05/3.25 inference(resolution,[status(thm)],[f39,f74])).
% 22.05/3.25 fof(f160,plain,(
% 22.05/3.25 smaller(age(sk2,sk4),eta)|age(sk2,sk4)=eta),
% 22.05/3.25 inference(resolution,[status(thm)],[f39,f75])).
% 22.05/3.25 fof(f162,definition,(
% 22.05/3.25 sQ14_spl <=> (smaller(age(sk2,sk3),age(sk2,sk4)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f163,plain,(
% 22.05/3.25 smaller(age(sk2,sk3),age(sk2,sk4))|~sQ14_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f162])).
% 22.05/3.25 fof(f165,definition,(
% 22.05/3.25 sQ15_spl <=> (age(sk2,sk3)=age(sk2,sk4))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f166,plain,(
% 22.05/3.25 age(sk2,sk3)=age(sk2,sk4)|~sQ15_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f165])).
% 22.05/3.25 fof(f168,plain,(
% 22.05/3.25 sQ14_spl|sQ15_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f159,f162,f165])).
% 22.05/3.25 fof(f169,definition,(
% 22.05/3.25 sQ16_spl <=> (smaller(age(sk2,sk4),eta))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f170,plain,(
% 22.05/3.25 smaller(age(sk2,sk4),eta)|~sQ16_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f169])).
% 22.05/3.25 fof(f172,definition,(
% 22.05/3.25 sQ17_spl <=> (age(sk2,sk4)=eta)),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f173,plain,(
% 22.05/3.25 age(sk2,sk4)=eta|~sQ17_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f172])).
% 22.05/3.25 fof(f175,plain,(
% 22.05/3.25 sQ16_spl|sQ17_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f160,f169,f172])).
% 22.05/3.25 fof(f178,plain,(
% 22.05/3.25 smaller(age(sk2,sk3),eta)|~sQ17_spl|~sQ14_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f173,f163])).
% 22.05/3.25 fof(f184,plain,(
% 22.05/3.25 smaller(age(sk2,sk5),age(sk2,sk6))|age(sk2,sk5)=age(sk2,sk6)),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f92])).
% 22.05/3.25 fof(f185,plain,(
% 22.05/3.25 ![X0,X1,X2]: (smaller(age(X0,X1),age(X0,X2))|age(X0,X1)=age(X0,X2)|~organization(X0)|greater(external_ties(X0,X1),external_ties(X0,X2)))),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f69])).
% 22.05/3.25 fof(f186,plain,(
% 22.05/3.25 ![X0,X1,X2]: (smaller(age(X0,X1),age(X0,X2))|age(X0,X1)=age(X0,X2)|~organization(X0)|greater(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2)))),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f68])).
% 22.05/3.25 fof(f188,plain,(
% 22.05/3.25 smaller(eta,age(sk2,sk6))|eta=age(sk2,sk6)),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f128])).
% 22.05/3.25 fof(f189,plain,(
% 22.05/3.25 smaller(eta,age(sk2,sk5))|eta=age(sk2,sk5)),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f93])).
% 22.05/3.25 fof(f190,plain,(
% 22.05/3.25 ![X0]: (smaller(X0,age(sk2,sk6))|X0=age(sk2,sk6)|greater(X0,age(sk2,sk5)))),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f109])).
% 22.05/3.25 fof(f192,plain,(
% 22.05/3.25 ![X0]: (smaller(X0,age(sk2,sk5))|X0=age(sk2,sk5)|greater(X0,eta))),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f110])).
% 22.05/3.25 fof(f193,plain,(
% 22.05/3.25 ![X0,X1]: (smaller(X0,X1)|X0=X1|smaller(X1,X0))),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f46])).
% 22.05/3.25 fof(f194,plain,(
% 22.05/3.25 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater_or_equal(X0,X1))),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f43])).
% 22.05/3.25 fof(f195,plain,(
% 22.05/3.25 ![X0,X1,X2]: (smaller(X0,X1)|X0=X1|~greater(X2,X0)|greater(X2,X1))),
% 22.05/3.25 inference(resolution,[status(thm)],[f50,f49])).
% 22.05/3.25 fof(f197,definition,(
% 22.05/3.25 sQ18_spl <=> (smaller(age(sk2,sk5),age(sk2,sk6)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f200,definition,(
% 22.05/3.25 sQ19_spl <=> (age(sk2,sk5)=age(sk2,sk6))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f201,plain,(
% 22.05/3.25 age(sk2,sk5)=age(sk2,sk6)|~sQ19_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f200])).
% 22.05/3.25 fof(f203,plain,(
% 22.05/3.25 sQ18_spl|sQ19_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f184,f197,f200])).
% 22.05/3.25 fof(f204,definition,(
% 22.05/3.25 sQ20_spl <=> (smaller(eta,age(sk2,sk6)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f207,definition,(
% 22.05/3.25 sQ21_spl <=> (eta=age(sk2,sk6))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f208,plain,(
% 22.05/3.25 eta=age(sk2,sk6)|~sQ21_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f207])).
% 22.05/3.25 fof(f209,plain,(
% 22.05/3.25 ~eta=age(sk2,sk6)|sQ21_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f207])).
% 22.05/3.25 fof(f210,plain,(
% 22.05/3.25 sQ20_spl|sQ21_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f188,f204,f207])).
% 22.05/3.25 fof(f211,definition,(
% 22.05/3.25 sQ22_spl <=> (smaller(eta,age(sk2,sk5)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f214,definition,(
% 22.05/3.25 sQ23_spl <=> (eta=age(sk2,sk5))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f215,plain,(
% 22.05/3.25 eta=age(sk2,sk5)|~sQ23_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f214])).
% 22.05/3.25 fof(f216,plain,(
% 22.05/3.25 ~eta=age(sk2,sk5)|sQ23_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f214])).
% 22.05/3.25 fof(f217,plain,(
% 22.05/3.25 sQ22_spl|sQ23_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f189,f211,f214])).
% 22.05/3.25 fof(f221,plain,(
% 22.05/3.25 ~greater(eta,eta)|~sQ23_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f215,f93])).
% 22.05/3.25 fof(f223,plain,(
% 22.05/3.25 greater(eta,eta)|~sQ23_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f215,f76])).
% 22.05/3.25 fof(f231,plain,(
% 22.05/3.25 ~greater(eta,eta)|~sQ21_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f208,f128])).
% 22.05/3.25 fof(f232,plain,(
% 22.05/3.25 greater(eta,eta)|~sQ21_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f208,f123])).
% 22.05/3.25 fof(f244,plain,(
% 22.05/3.25 greater(age(sk2,sk5),age(sk2,sk5))|~sQ19_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f201,f77])).
% 22.05/3.25 fof(f245,plain,(
% 22.05/3.25 ~greater(age(sk2,sk5),age(sk2,sk5))|~sQ19_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f201,f92])).
% 22.05/3.25 fof(f255,plain,(
% 22.05/3.25 $false|~sQ19_spl),
% 22.05/3.25 inference(forward_subsumption_resolution,[status(thm)],[f245,f244])).
% 22.05/3.25 fof(f256,plain,(
% 22.05/3.25 ~sQ19_spl),
% 22.05/3.25 inference(contradiction_clause,[status(thm)],[f255])).
% 22.05/3.25 fof(f257,plain,(
% 22.05/3.25 ![X0]: (~organization(sk2)|~greater(age(sk2,X0),eta)|greater(external_ties(sk2,X0),external_ties(sk2,sk4))|~sQ17_spl)),
% 22.05/3.25 inference(paramodulation,[status(thm)],[f173,f69])).
% 22.05/3.25 fof(f258,plain,(
% 22.05/3.25 ![X0]: (~organization(sk2)|~greater(eta,age(sk2,X0))|greater(external_ties(sk2,sk4),external_ties(sk2,X0))|~sQ17_spl)),
% 22.05/3.25 inference(paramodulation,[status(thm)],[f173,f69])).
% 22.05/3.25 fof(f259,plain,(
% 22.05/3.25 ![X0]: (~organization(sk2)|~greater(age(sk2,X0),eta)|greater(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk4))|~sQ17_spl)),
% 22.05/3.25 inference(paramodulation,[status(thm)],[f173,f68])).
% 22.05/3.25 fof(f260,plain,(
% 22.05/3.25 ![X0]: (~organization(sk2)|~greater(eta,age(sk2,X0))|greater(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,X0))|~sQ17_spl)),
% 22.05/3.25 inference(paramodulation,[status(thm)],[f173,f68])).
% 22.05/3.25 fof(f261,plain,(
% 22.05/3.25 ~has_endowment(sk2)|~greater(eta,eta)|~has_immunity(sk2,sk4)|~sQ17_spl),
% 22.05/3.25 inference(paramodulation,[status(thm)],[f173,f53])).
% 22.05/3.25 fof(f263,definition,(
% 22.05/3.25 ![X0]: (sQ24_spl <=> (~greater(age(sk2,X0),eta)|greater(external_ties(sk2,X0),external_ties(sk2,sk4))))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f264,plain,(
% 22.05/3.25 ![X0]: (~greater(age(sk2,X0),eta)|greater(external_ties(sk2,X0),external_ties(sk2,sk4))|~sQ24_spl)),
% 22.05/3.25 inference(component_clause,[status(thm)],[f263])).
% 22.05/3.25 fof(f266,plain,(
% 22.05/3.25 ~sQ9_spl|sQ24_spl|~sQ17_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f257,f134,f263,f172])).
% 22.05/3.25 fof(f267,definition,(
% 22.05/3.25 ![X0]: (sQ25_spl <=> (~greater(eta,age(sk2,X0))|greater(external_ties(sk2,sk4),external_ties(sk2,X0))))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f270,plain,(
% 22.05/3.25 ~sQ9_spl|sQ25_spl|~sQ17_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f258,f134,f267,f172])).
% 22.05/3.25 fof(f271,definition,(
% 22.05/3.25 ![X0]: (sQ26_spl <=> (~greater(age(sk2,X0),eta)|greater(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk4))))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f272,plain,(
% 22.05/3.25 ![X0]: (~greater(age(sk2,X0),eta)|greater(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk4))|~sQ26_spl)),
% 22.05/3.25 inference(component_clause,[status(thm)],[f271])).
% 22.05/3.25 fof(f274,plain,(
% 22.05/3.25 ~sQ9_spl|sQ26_spl|~sQ17_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f259,f134,f271,f172])).
% 22.05/3.25 fof(f275,definition,(
% 22.05/3.25 ![X0]: (sQ27_spl <=> (~greater(eta,age(sk2,X0))|greater(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,X0))))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f278,plain,(
% 22.05/3.25 ~sQ9_spl|sQ27_spl|~sQ17_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f260,f134,f275,f172])).
% 22.05/3.25 fof(f279,definition,(
% 22.05/3.25 sQ28_spl <=> (greater(eta,eta))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f281,plain,(
% 22.05/3.25 ~greater(eta,eta)|sQ28_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f279])).
% 22.05/3.25 fof(f282,plain,(
% 22.05/3.25 ~sQ3_spl|~sQ28_spl|~sQ4_spl|~sQ17_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f261,f95,f279,f98,f172])).
% 22.05/3.25 fof(f283,definition,(
% 22.05/3.25 sQ29_spl <=> (smaller_or_equal(eta,eta))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f285,plain,(
% 22.05/3.25 ~smaller_or_equal(eta,eta)|sQ29_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f283])).
% 22.05/3.25 fof(f289,plain,(
% 22.05/3.25 smaller_or_equal(age(sk2,sk3),eta)|~sQ15_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f166,f75])).
% 22.05/3.25 fof(f293,definition,(
% 22.05/3.25 sQ30_spl <=> (smaller(eta,eta))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f294,plain,(
% 22.05/3.25 smaller(eta,eta)|~sQ30_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f293])).
% 22.05/3.25 fof(f295,plain,(
% 22.05/3.25 ~smaller(eta,eta)|sQ30_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f293])).
% 22.05/3.25 fof(f296,definition,(
% 22.05/3.25 sQ31_spl <=> (eta=eta)),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f316,plain,(
% 22.05/3.25 ~has_endowment(sk2)|has_immunity(sk2,sk3)|~sQ15_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f289,f52])).
% 22.05/3.25 fof(f318,definition,(
% 22.05/3.25 sQ32_spl <=> (has_immunity(sk2,sk3))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f319,plain,(
% 22.05/3.25 has_immunity(sk2,sk3)|~sQ32_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f318])).
% 22.05/3.25 fof(f321,plain,(
% 22.05/3.25 ~sQ3_spl|sQ32_spl|~sQ15_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f316,f95,f318,f165])).
% 22.05/3.25 fof(f322,definition,(
% 22.05/3.25 sQ33_spl <=> (smaller(age(sk2,sk3),eta))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f323,plain,(
% 22.05/3.25 smaller(age(sk2,sk3),eta)|~sQ33_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f322])).
% 22.05/3.25 fof(f356,plain,(
% 22.05/3.25 $false|sQ29_spl),
% 22.05/3.25 inference(forward_subsumption_resolution,[status(thm)],[f285,f89])).
% 22.05/3.25 fof(f357,plain,(
% 22.05/3.25 sQ29_spl),
% 22.05/3.25 inference(contradiction_clause,[status(thm)],[f356])).
% 22.05/3.25 fof(f399,plain,(
% 22.05/3.25 greater(eta,eta)|~sQ30_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f294,f45])).
% 22.05/3.25 fof(f404,plain,(
% 22.05/3.25 ~greater(eta,eta)|~sQ30_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f399,f47])).
% 22.05/3.25 fof(f405,plain,(
% 22.05/3.25 $false|~sQ30_spl),
% 22.05/3.25 inference(forward_subsumption_resolution,[status(thm)],[f404,f399])).
% 22.05/3.25 fof(f406,plain,(
% 22.05/3.25 ~sQ30_spl),
% 22.05/3.25 inference(contradiction_clause,[status(thm)],[f405])).
% 22.05/3.25 fof(f407,plain,(
% 22.05/3.25 hazard_of_mortality(sk2,sk3)=hazard_of_mortality(sk2,sk4)|~sQ32_spl|~sQ13_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f319,f156])).
% 22.05/3.25 fof(f408,plain,(
% 22.05/3.25 ![X0]: (~organization(sk2)|has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk3))|~sQ32_spl)),
% 22.05/3.25 inference(resolution,[status(thm)],[f319,f59])).
% 22.05/3.25 fof(f410,plain,(
% 22.05/3.25 $false|sQ2_spl|~sQ32_spl|~sQ13_spl),
% 22.05/3.25 inference(forward_subsumption_resolution,[status(thm)],[f407,f87])).
% 22.05/3.25 fof(f411,plain,(
% 22.05/3.25 sQ2_spl|~sQ32_spl|~sQ13_spl),
% 22.05/3.25 inference(contradiction_clause,[status(thm)],[f410])).
% 22.05/3.25 fof(f418,definition,(
% 22.05/3.25 sQ43_spl <=> (hazard_of_mortality(sk2,sk5)=hazard_of_mortality(sk2,sk6))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f419,plain,(
% 22.05/3.25 hazard_of_mortality(sk2,sk5)=hazard_of_mortality(sk2,sk6)|~sQ43_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f418])).
% 22.05/3.25 fof(f422,plain,(
% 22.05/3.25 ~greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk3))|~sQ2_spl|sQ1_spl),
% 22.05/3.25 inference(forward_demodulation,[status(thm)],[f86,f84])).
% 22.05/3.25 fof(f457,plain,(
% 22.05/3.25 greater(age(sk2,sk5),eta)|age(sk2,sk5)=eta),
% 22.05/3.25 inference(resolution,[status(thm)],[f120,f42])).
% 22.05/3.25 fof(f458,definition,(
% 22.05/3.25 sQ48_spl <=> (greater(age(sk2,sk5),eta))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f461,plain,(
% 22.05/3.25 sQ48_spl|sQ23_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f457,f458,f214])).
% 22.05/3.25 fof(f467,definition,(
% 22.05/3.25 sQ49_spl <=> (greater(age(sk2,sk6),eta))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f474,plain,(
% 22.05/3.25 ~greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk6))|~sQ10_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f138,f47])).
% 22.05/3.25 fof(f478,plain,(
% 22.05/3.25 ~greater(external_ties(sk2,sk5),external_ties(sk2,sk6))|~sQ11_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f145,f47])).
% 22.05/3.25 fof(f480,plain,(
% 22.05/3.25 eta=eta|smaller(eta,eta)|sQ30_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f193,f295])).
% 22.05/3.25 fof(f489,plain,(
% 22.05/3.25 sQ31_spl|sQ30_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f480,f296,f293])).
% 22.05/3.25 fof(f492,plain,(
% 22.05/3.25 ![X0,X1]: (X0=X1|greater_or_equal(X0,X1)|greater(X1,X0))),
% 22.05/3.25 inference(resolution,[status(thm)],[f194,f45])).
% 22.05/3.25 fof(f498,plain,(
% 22.05/3.25 greater(eta,age(sk2,sk4))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f170,f45])).
% 22.05/3.25 fof(f502,plain,(
% 22.05/3.25 ![X0]: (~greater(X0,eta)|greater(X0,age(sk2,sk4))|~sQ16_spl)),
% 22.05/3.25 inference(resolution,[status(thm)],[f498,f49])).
% 22.05/3.25 fof(f503,plain,(
% 22.05/3.25 ~greater(age(sk2,sk4),eta)|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f498,f47])).
% 22.05/3.25 fof(f506,plain,(
% 22.05/3.25 greater(age(sk2,sk6),age(sk2,sk4))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f502,f123])).
% 22.05/3.25 fof(f507,plain,(
% 22.05/3.25 greater(age(sk2,sk5),age(sk2,sk4))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f502,f76])).
% 22.05/3.25 fof(f509,plain,(
% 22.05/3.25 ~organization(sk2)|greater(external_ties(sk2,sk6),external_ties(sk2,sk4))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f506,f69])).
% 22.05/3.25 fof(f510,plain,(
% 22.05/3.25 ~organization(sk2)|greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f506,f68])).
% 22.05/3.25 fof(f514,plain,(
% 22.05/3.25 ~greater(age(sk2,sk4),age(sk2,sk6))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f506,f47])).
% 22.05/3.25 fof(f515,definition,(
% 22.05/3.25 sQ51_spl <=> (greater(external_ties(sk2,sk6),external_ties(sk2,sk4)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f516,plain,(
% 22.05/3.25 greater(external_ties(sk2,sk6),external_ties(sk2,sk4))|~sQ51_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f515])).
% 22.05/3.25 fof(f518,plain,(
% 22.05/3.25 ~sQ9_spl|sQ51_spl|~sQ16_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f509,f134,f515,f169])).
% 22.05/3.25 fof(f519,definition,(
% 22.05/3.25 sQ52_spl <=> (greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f520,plain,(
% 22.05/3.25 greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4))|~sQ52_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f519])).
% 22.05/3.25 fof(f522,plain,(
% 22.05/3.25 ~sQ9_spl|sQ52_spl|~sQ16_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f510,f134,f519,f169])).
% 22.05/3.25 fof(f523,plain,(
% 22.05/3.25 ~organization(sk2)|greater(external_ties(sk2,sk5),external_ties(sk2,sk4))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f507,f69])).
% 22.05/3.25 fof(f524,plain,(
% 22.05/3.25 ~organization(sk2)|greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f507,f68])).
% 22.05/3.25 fof(f528,plain,(
% 22.05/3.25 ~greater(age(sk2,sk4),age(sk2,sk5))|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f507,f47])).
% 22.05/3.25 fof(f529,definition,(
% 22.05/3.25 sQ53_spl <=> (greater(external_ties(sk2,sk5),external_ties(sk2,sk4)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f530,plain,(
% 22.05/3.25 greater(external_ties(sk2,sk5),external_ties(sk2,sk4))|~sQ53_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f529])).
% 22.05/3.25 fof(f531,plain,(
% 22.05/3.25 ~greater(external_ties(sk2,sk5),external_ties(sk2,sk4))|sQ53_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f529])).
% 22.05/3.25 fof(f532,plain,(
% 22.05/3.25 ~sQ9_spl|sQ53_spl|~sQ16_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f523,f134,f529,f169])).
% 22.05/3.25 fof(f533,definition,(
% 22.05/3.25 sQ54_spl <=> (greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f534,plain,(
% 22.05/3.25 greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))|~sQ54_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f533])).
% 22.05/3.25 fof(f536,plain,(
% 22.05/3.25 ~sQ9_spl|sQ54_spl|~sQ16_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f524,f134,f533,f169])).
% 22.05/3.25 fof(f537,plain,(
% 22.05/3.25 smaller(age(sk2,sk4),age(sk2,sk6))|age(sk2,sk4)=age(sk2,sk6)|~sQ16_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f514,f50])).
% 22.05/3.25 fof(f538,definition,(
% 22.05/3.25 sQ55_spl <=> (smaller(age(sk2,sk4),age(sk2,sk6)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f541,definition,(
% 22.05/3.25 sQ56_spl <=> (age(sk2,sk4)=age(sk2,sk6))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f542,plain,(
% 22.05/3.25 age(sk2,sk4)=age(sk2,sk6)|~sQ56_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f541])).
% 22.05/3.25 fof(f544,plain,(
% 22.05/3.25 sQ55_spl|sQ56_spl|~sQ16_spl),
% 22.05/3.25 inference(split_clause,[status(thm)],[f537,f538,f541,f169])).
% 22.05/3.25 fof(f546,plain,(
% 22.05/3.25 greater(age(sk2,sk5),age(sk2,sk6))|~sQ56_spl|~sQ16_spl),
% 22.05/3.25 inference(backward_demodulation,[status(thm)],[f542,f507])).
% 22.05/3.25 fof(f566,plain,(
% 22.05/3.25 $false|~sQ56_spl|~sQ16_spl),
% 22.05/3.25 inference(forward_subsumption_resolution,[status(thm)],[f546,f92])).
% 22.05/3.25 fof(f567,plain,(
% 22.05/3.25 ~sQ56_spl|~sQ16_spl),
% 22.05/3.25 inference(contradiction_clause,[status(thm)],[f566])).
% 22.05/3.25 fof(f578,plain,(
% 22.05/3.25 ~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk5))|greater(capability(sk2,sk6),capability(sk2,sk5))|~sQ10_spl),
% 22.05/3.25 inference(resolution,[status(thm)],[f63,f138])).
% 22.05/3.25 fof(f579,plain,(
% 22.05/3.25 ![X0,X1,X2]: (~organization(X0)|~smaller_or_equal(internal_friction(X0,X1),internal_friction(X0,X2))|greater(capability(X0,X1),capability(X0,X2))|smaller(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))|stock_of_knowledge(X0,X1)=stock_of_knowledge(X0,X2))),
% 22.05/3.25 inference(resolution,[status(thm)],[f63,f50])).
% 22.05/3.25 fof(f580,definition,(
% 22.05/3.25 sQ57_spl <=> (smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk5)))),
% 22.05/3.25 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 22.05/3.25 fof(f581,plain,(
% 22.05/3.25 smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk5))|~sQ57_spl),
% 22.05/3.25 inference(component_clause,[status(thm)],[f580])).
% 22.05/3.25 fof(f582,plain,(
% 22.05/3.25 ~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk5))|sQ57_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f580])).
% 22.05/3.26 fof(f583,definition,(
% 22.05/3.26 sQ58_spl <=> (greater(capability(sk2,sk6),capability(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f584,plain,(
% 22.05/3.26 greater(capability(sk2,sk6),capability(sk2,sk5))|~sQ58_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f583])).
% 22.05/3.26 fof(f586,plain,(
% 22.05/3.26 ~sQ9_spl|~sQ57_spl|sQ58_spl|~sQ10_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f578,f134,f580,f583,f137])).
% 22.05/3.26 fof(f588,plain,(
% 22.05/3.26 ~organization(sk2)|greater(position(sk2,sk6),position(sk2,sk5))|~sQ11_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f66,f145])).
% 22.05/3.26 fof(f589,plain,(
% 22.05/3.26 ![X0,X1,X2]: (~organization(X0)|greater(position(X0,X1),position(X0,X2))|smaller(external_ties(X0,X1),external_ties(X0,X2))|external_ties(X0,X1)=external_ties(X0,X2))),
% 22.05/3.26 inference(resolution,[status(thm)],[f66,f50])).
% 22.05/3.26 fof(f590,definition,(
% 22.05/3.26 sQ59_spl <=> (greater(position(sk2,sk6),position(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f591,plain,(
% 22.05/3.26 greater(position(sk2,sk6),position(sk2,sk5))|~sQ59_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f590])).
% 22.05/3.26 fof(f593,plain,(
% 22.05/3.26 ~sQ9_spl|sQ59_spl|~sQ11_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f588,f134,f590,f144])).
% 22.05/3.26 fof(f617,plain,(
% 22.05/3.26 smaller(age(sk2,sk4),age(sk2,sk5))|age(sk2,sk4)=age(sk2,sk5)|~sQ16_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f528,f50])).
% 22.05/3.26 fof(f618,definition,(
% 22.05/3.26 sQ60_spl <=> (smaller(age(sk2,sk4),age(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f621,definition,(
% 22.05/3.26 sQ61_spl <=> (age(sk2,sk4)=age(sk2,sk5))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f622,plain,(
% 22.05/3.26 age(sk2,sk4)=age(sk2,sk5)|~sQ61_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f621])).
% 22.05/3.26 fof(f624,plain,(
% 22.05/3.26 sQ60_spl|sQ61_spl|~sQ16_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f617,f618,f621,f169])).
% 22.05/3.26 fof(f625,plain,(
% 22.05/3.26 ~greater(age(sk2,sk5),age(sk2,sk5))|~sQ61_spl|~sQ16_spl),
% 22.05/3.26 inference(backward_demodulation,[status(thm)],[f622,f528])).
% 22.05/3.26 fof(f629,plain,(
% 22.05/3.26 greater(age(sk2,sk5),age(sk2,sk5))|~sQ61_spl|~sQ16_spl),
% 22.05/3.26 inference(backward_demodulation,[status(thm)],[f622,f507])).
% 22.05/3.26 fof(f647,plain,(
% 22.05/3.26 $false|~sQ61_spl|~sQ16_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f629,f625])).
% 22.05/3.26 fof(f648,plain,(
% 22.05/3.26 ~sQ61_spl|~sQ16_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f647])).
% 22.05/3.26 fof(f666,plain,(
% 22.05/3.26 ![X0]: (smaller(external_ties(sk2,sk5),X0)|external_ties(sk2,sk5)=X0|greater(external_ties(sk2,sk6),X0)|~sQ11_spl)),
% 22.05/3.26 inference(resolution,[status(thm)],[f195,f145])).
% 22.05/3.26 fof(f667,plain,(
% 22.05/3.26 ![X0]: (smaller(stock_of_knowledge(sk2,sk5),X0)|stock_of_knowledge(sk2,sk5)=X0|greater(stock_of_knowledge(sk2,sk6),X0)|~sQ10_spl)),
% 22.05/3.26 inference(resolution,[status(thm)],[f195,f138])).
% 22.05/3.26 fof(f668,plain,(
% 22.05/3.26 ![X0]: (smaller(age(sk2,sk5),X0)|age(sk2,sk5)=X0|greater(age(sk2,sk6),X0))),
% 22.05/3.26 inference(resolution,[status(thm)],[f195,f77])).
% 22.05/3.26 fof(f670,plain,(
% 22.05/3.26 ![X0]: (smaller(eta,X0)|eta=X0|greater(age(sk2,sk5),X0))),
% 22.05/3.26 inference(resolution,[status(thm)],[f195,f76])).
% 22.05/3.26 fof(f671,plain,(
% 22.05/3.26 ![X0,X1,X2]: (smaller(X0,X1)|X0=X1|greater(X2,X1)|smaller(X2,X0)|X2=X0)),
% 22.05/3.26 inference(resolution,[status(thm)],[f195,f50])).
% 22.05/3.26 fof(f707,plain,(
% 22.05/3.26 age(sk2,sk6)=eta|greater_or_equal(age(sk2,sk6),eta)),
% 22.05/3.26 inference(resolution,[status(thm)],[f492,f128])).
% 22.05/3.26 fof(f708,plain,(
% 22.05/3.26 age(sk2,sk5)=eta|greater_or_equal(age(sk2,sk5),eta)),
% 22.05/3.26 inference(resolution,[status(thm)],[f492,f93])).
% 22.05/3.26 fof(f709,plain,(
% 22.05/3.26 age(sk2,sk6)=age(sk2,sk4)|greater_or_equal(age(sk2,sk6),age(sk2,sk4))|~sQ16_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f492,f514])).
% 22.05/3.26 fof(f710,plain,(
% 22.05/3.26 age(sk2,sk5)=age(sk2,sk4)|greater_or_equal(age(sk2,sk5),age(sk2,sk4))|~sQ16_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f492,f528])).
% 22.05/3.26 fof(f711,plain,(
% 22.05/3.26 eta=age(sk2,sk4)|greater_or_equal(eta,age(sk2,sk4))|~sQ16_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f492,f503])).
% 22.05/3.26 fof(f712,plain,(
% 22.05/3.26 age(sk2,sk6)=age(sk2,sk5)|greater_or_equal(age(sk2,sk6),age(sk2,sk5))),
% 22.05/3.26 inference(resolution,[status(thm)],[f492,f92])).
% 22.05/3.26 fof(f731,definition,(
% 22.05/3.26 sQ63_spl <=> (greater_or_equal(age(sk2,sk6),eta))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f734,plain,(
% 22.05/3.26 sQ21_spl|sQ63_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f707,f207,f731])).
% 22.05/3.26 fof(f735,definition,(
% 22.05/3.26 sQ64_spl <=> (greater_or_equal(age(sk2,sk5),eta))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f738,plain,(
% 22.05/3.26 sQ23_spl|sQ64_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f708,f214,f735])).
% 22.05/3.26 fof(f739,definition,(
% 22.05/3.26 sQ65_spl <=> (greater_or_equal(age(sk2,sk6),age(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f742,plain,(
% 22.05/3.26 sQ56_spl|sQ65_spl|~sQ16_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f709,f541,f739,f169])).
% 22.05/3.26 fof(f743,definition,(
% 22.05/3.26 sQ66_spl <=> (greater_or_equal(age(sk2,sk5),age(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f746,plain,(
% 22.05/3.26 sQ61_spl|sQ66_spl|~sQ16_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f710,f621,f743,f169])).
% 22.05/3.26 fof(f747,definition,(
% 22.05/3.26 sQ67_spl <=> (greater_or_equal(eta,age(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f750,plain,(
% 22.05/3.26 sQ17_spl|sQ67_spl|~sQ16_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f711,f172,f747,f169])).
% 22.05/3.26 fof(f751,definition,(
% 22.05/3.26 sQ68_spl <=> (greater_or_equal(age(sk2,sk6),age(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f754,plain,(
% 22.05/3.26 sQ19_spl|sQ68_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f712,f200,f751])).
% 22.05/3.26 fof(f784,plain,(
% 22.05/3.26 $false|~sQ23_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f221,f223])).
% 22.05/3.26 fof(f785,plain,(
% 22.05/3.26 ~sQ23_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f784])).
% 22.05/3.26 fof(f790,plain,(
% 22.05/3.26 $false|~sQ21_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f232,f231])).
% 22.05/3.26 fof(f791,plain,(
% 22.05/3.26 ~sQ21_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f790])).
% 22.05/3.26 fof(f806,plain,(
% 22.05/3.26 ![X0,X1]: (~external_ties(sk2,X0)=external_ties(sk2,X1)|position(sk2,X0)=position(sk2,X1))),
% 22.05/3.26 inference(resolution,[status(thm)],[f67,f72])).
% 22.05/3.26 fof(f807,plain,(
% 22.05/3.26 ![X0,X1]: (internal_friction(sk2,X0)=internal_friction(sk2,X1))),
% 22.05/3.26 inference(resolution,[status(thm)],[f71,f72])).
% 22.05/3.26 fof(f808,plain,(
% 22.05/3.26 ![X0,X1]: (~stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X1)|capability(sk2,X0)=capability(sk2,X1))),
% 22.05/3.26 inference(resolution,[status(thm)],[f91,f72])).
% 22.05/3.26 fof(f837,definition,(
% 22.05/3.26 sQ69_spl <=> (hazard_of_mortality(sk2,sk5)=hazard_of_mortality(sk2,sk5))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f844,definition,(
% 22.05/3.26 sQ71_spl <=> (smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f845,plain,(
% 22.05/3.26 smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5))|~sQ71_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f844])).
% 22.05/3.26 fof(f846,plain,(
% 22.05/3.26 ~smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5))|sQ71_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f844])).
% 22.05/3.26 fof(f857,definition,(
% 22.05/3.26 sQ72_spl <=> (greater(eta,age(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f858,plain,(
% 22.05/3.26 greater(eta,age(sk2,sk4))|~sQ72_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f857])).
% 22.05/3.26 fof(f871,plain,(
% 22.05/3.26 ![X0,X1,X2]: (~organization(sk2)|~smaller_or_equal(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|~greater(internal_friction(sk2,X0),internal_friction(sk2,X2))|smaller(capability(sk2,X0),capability(sk2,X1)))),
% 22.05/3.26 inference(paramodulation,[status(thm)],[f807,f64])).
% 22.05/3.26 fof(f872,plain,(
% 22.05/3.26 ![X0,X1,X2]: (~organization(sk2)|~smaller_or_equal(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|~greater(internal_friction(sk2,X2),internal_friction(sk2,X1))|smaller(capability(sk2,X0),capability(sk2,X1)))),
% 22.05/3.26 inference(paramodulation,[status(thm)],[f807,f64])).
% 22.05/3.26 fof(f875,definition,(
% 22.05/3.26 ![X0,X1,X2]: (sQ73_spl <=> (~smaller_or_equal(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|~greater(internal_friction(sk2,X0),internal_friction(sk2,X2))|smaller(capability(sk2,X0),capability(sk2,X1))))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f878,plain,(
% 22.05/3.26 ~sQ9_spl|sQ73_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f871,f134,f875])).
% 22.05/3.26 fof(f879,definition,(
% 22.05/3.26 ![X0,X1,X2]: (sQ74_spl <=> (~smaller_or_equal(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|~greater(internal_friction(sk2,X2),internal_friction(sk2,X1))|smaller(capability(sk2,X0),capability(sk2,X1))))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f882,plain,(
% 22.05/3.26 ~sQ9_spl|sQ74_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f872,f134,f879])).
% 22.05/3.26 fof(f937,definition,(
% 22.05/3.26 sQ78_spl <=> (hazard_of_mortality(sk2,sk3)=hazard_of_mortality(sk2,sk3))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f944,definition,(
% 22.05/3.26 sQ80_spl <=> (smaller(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f945,plain,(
% 22.05/3.26 smaller(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3))|~sQ80_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f944])).
% 22.05/3.26 fof(f946,plain,(
% 22.05/3.26 ~smaller(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3))|sQ80_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f944])).
% 22.05/3.26 fof(f974,plain,(
% 22.05/3.26 ![X0,X1]: (smaller(age(sk2,X0),age(sk2,X1))|age(sk2,X0)=age(sk2,X1)|greater(external_ties(sk2,X0),external_ties(sk2,X1)))),
% 22.05/3.26 inference(resolution,[status(thm)],[f185,f72])).
% 22.05/3.26 fof(f975,plain,(
% 22.05/3.26 ![X0,X1]: (smaller(age(sk2,X0),age(sk2,X1))|age(sk2,X0)=age(sk2,X1)|greater(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1)))),
% 22.05/3.26 inference(resolution,[status(thm)],[f186,f72])).
% 22.05/3.26 fof(f981,plain,(
% 22.05/3.26 greater(eta,age(sk2,sk3))|~sQ33_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f323,f45])).
% 22.05/3.26 fof(f982,plain,(
% 22.05/3.26 smaller_or_equal(age(sk2,sk3),eta)|~sQ33_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f323,f40])).
% 22.05/3.26 fof(f986,plain,(
% 22.05/3.26 ![X0]: (~greater(X0,eta)|greater(X0,age(sk2,sk3))|~sQ33_spl)),
% 22.05/3.26 inference(resolution,[status(thm)],[f981,f49])).
% 22.05/3.26 fof(f988,plain,(
% 22.05/3.26 ~has_endowment(sk2)|has_immunity(sk2,sk3)|~sQ33_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f982,f52])).
% 22.05/3.26 fof(f990,plain,(
% 22.05/3.26 ~sQ3_spl|sQ32_spl|~sQ33_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f988,f95,f318,f322])).
% 22.05/3.26 fof(f992,definition,(
% 22.05/3.26 ![X0]: (sQ81_spl <=> (has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk3))))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f993,plain,(
% 22.05/3.26 ![X0]: (has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk3))|~sQ81_spl)),
% 22.05/3.26 inference(component_clause,[status(thm)],[f992])).
% 22.05/3.26 fof(f995,plain,(
% 22.05/3.26 ~sQ9_spl|sQ81_spl|~sQ32_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f408,f134,f992,f318])).
% 22.05/3.26 fof(f1012,plain,(
% 22.05/3.26 ~greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5))|~sQ0_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f80,f47])).
% 22.05/3.26 fof(f1013,plain,(
% 22.05/3.26 hazard_of_mortality(sk2,sk5)=hazard_of_mortality(sk2,sk6)|greater_or_equal(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))|~sQ0_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1012,f492])).
% 22.05/3.26 fof(f1015,definition,(
% 22.05/3.26 sQ83_spl <=> (greater_or_equal(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1018,plain,(
% 22.05/3.26 sQ43_spl|sQ83_spl|~sQ0_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1013,f418,f1015,f79])).
% 22.05/3.26 fof(f1019,definition,(
% 22.05/3.26 sQ84_spl <=> (smaller(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1020,plain,(
% 22.05/3.26 smaller(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5))|~sQ84_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1019])).
% 22.05/3.26 fof(f1026,plain,(
% 22.05/3.26 smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5))|~sQ43_spl|~sQ84_spl),
% 22.05/3.26 inference(backward_demodulation,[status(thm)],[f419,f1020])).
% 22.05/3.26 fof(f1045,plain,(
% 22.05/3.26 greater(age(sk2,sk4),age(sk2,sk3))|~sQ14_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f163,f45])).
% 22.05/3.26 fof(f1053,plain,(
% 22.05/3.26 ~organization(sk2)|greater(external_ties(sk2,sk4),external_ties(sk2,sk3))|~sQ14_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1045,f69])).
% 22.05/3.26 fof(f1054,plain,(
% 22.05/3.26 ~organization(sk2)|greater(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk3))|~sQ14_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1045,f68])).
% 22.05/3.26 fof(f1057,plain,(
% 22.05/3.26 greater_or_equal(age(sk2,sk4),age(sk2,sk3))|~sQ14_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1045,f43])).
% 22.05/3.26 fof(f1058,plain,(
% 22.05/3.26 ![X0]: (~greater(X0,age(sk2,sk4))|greater(X0,age(sk2,sk3))|~sQ14_spl)),
% 22.05/3.26 inference(resolution,[status(thm)],[f1045,f49])).
% 22.05/3.26 fof(f1059,plain,(
% 22.05/3.26 ~greater(age(sk2,sk3),age(sk2,sk4))|~sQ14_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1045,f47])).
% 22.05/3.26 fof(f1060,definition,(
% 22.05/3.26 sQ85_spl <=> (greater(external_ties(sk2,sk4),external_ties(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1061,plain,(
% 22.05/3.26 greater(external_ties(sk2,sk4),external_ties(sk2,sk3))|~sQ85_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1060])).
% 22.05/3.26 fof(f1063,plain,(
% 22.05/3.26 ~sQ9_spl|sQ85_spl|~sQ14_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1053,f134,f1060,f162])).
% 22.05/3.26 fof(f1064,definition,(
% 22.05/3.26 sQ86_spl <=> (greater(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1065,plain,(
% 22.05/3.26 greater(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk3))|~sQ86_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1064])).
% 22.05/3.26 fof(f1066,plain,(
% 22.05/3.26 ~greater(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk3))|sQ86_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1064])).
% 22.05/3.26 fof(f1067,plain,(
% 22.05/3.26 ~sQ9_spl|sQ86_spl|~sQ14_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1054,f134,f1064,f162])).
% 22.05/3.26 fof(f1070,plain,(
% 22.05/3.26 age(sk2,sk4)=age(sk2,sk3)|greater_or_equal(age(sk2,sk4),age(sk2,sk3))|~sQ14_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1059,f492])).
% 22.05/3.26 fof(f1072,definition,(
% 22.05/3.26 sQ87_spl <=> (greater_or_equal(age(sk2,sk4),age(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1075,plain,(
% 22.05/3.26 sQ15_spl|sQ87_spl|~sQ14_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1070,f165,f1072,f162])).
% 22.05/3.26 fof(f1080,plain,(
% 22.05/3.26 greater(eta,age(sk2,sk3))|~sQ14_spl|~sQ16_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1058,f498])).
% 22.05/3.26 fof(f1081,plain,(
% 22.05/3.26 greater(age(sk2,sk5),age(sk2,sk3))|~sQ14_spl|~sQ16_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1058,f507])).
% 22.05/3.26 fof(f1086,plain,(
% 22.05/3.26 smaller(age(sk2,sk3),eta)|~sQ14_spl|~sQ16_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1080,f46])).
% 22.05/3.26 fof(f1090,plain,(
% 22.05/3.26 sQ33_spl|~sQ14_spl|~sQ16_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1086,f322,f162,f169])).
% 22.05/3.26 fof(f1104,plain,(
% 22.05/3.26 greater(eta,eta)|~sQ17_spl|~sQ72_spl),
% 22.05/3.26 inference(backward_demodulation,[status(thm)],[f173,f858])).
% 22.05/3.26 fof(f1109,plain,(
% 22.05/3.26 sQ33_spl|~sQ17_spl|~sQ14_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f178,f322,f172,f162])).
% 22.05/3.26 fof(f1110,plain,(
% 22.05/3.26 eta=age(sk2,sk6)|~sQ17_spl|~sQ56_spl),
% 22.05/3.26 inference(forward_demodulation,[status(thm)],[f173,f542])).
% 22.05/3.26 fof(f1111,plain,(
% 22.05/3.26 $false|sQ21_spl|~sQ17_spl|~sQ56_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f1110,f209])).
% 22.05/3.26 fof(f1112,plain,(
% 22.05/3.26 sQ21_spl|~sQ17_spl|~sQ56_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f1111])).
% 22.05/3.26 fof(f1113,plain,(
% 22.05/3.26 $false|sQ28_spl|~sQ17_spl|~sQ72_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f1104,f281])).
% 22.05/3.26 fof(f1114,plain,(
% 22.05/3.26 sQ28_spl|~sQ17_spl|~sQ72_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f1113])).
% 22.05/3.26 fof(f1120,plain,(
% 22.05/3.26 sQ72_spl|~sQ16_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f498,f857,f169])).
% 22.05/3.26 fof(f1142,plain,(
% 22.05/3.26 smaller(eta,eta)|~sQ17_spl|~sQ16_spl),
% 22.05/3.26 inference(forward_demodulation,[status(thm)],[f173,f170])).
% 22.05/3.26 fof(f1143,plain,(
% 22.05/3.26 $false|sQ30_spl|~sQ17_spl|~sQ16_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f1142,f295])).
% 22.05/3.26 fof(f1144,plain,(
% 22.05/3.26 sQ30_spl|~sQ17_spl|~sQ16_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f1143])).
% 22.05/3.26 fof(f1175,plain,(
% 22.05/3.26 eta=age(sk2,sk5)|~sQ17_spl|~sQ61_spl),
% 22.05/3.26 inference(forward_demodulation,[status(thm)],[f173,f622])).
% 22.05/3.26 fof(f1176,plain,(
% 22.05/3.26 $false|sQ23_spl|~sQ17_spl|~sQ61_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f1175,f216])).
% 22.05/3.26 fof(f1177,plain,(
% 22.05/3.26 sQ23_spl|~sQ17_spl|~sQ61_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f1176])).
% 22.05/3.26 fof(f1209,plain,(
% 22.05/3.26 ![X0,X1,X2]: (~organization(sk2)|~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,X1))|greater(capability(sk2,X2),capability(sk2,X1))|smaller(stock_of_knowledge(sk2,X2),stock_of_knowledge(sk2,X1))|stock_of_knowledge(sk2,X2)=stock_of_knowledge(sk2,X1))),
% 22.05/3.26 inference(paramodulation,[status(thm)],[f807,f579])).
% 22.05/3.26 fof(f1211,plain,(
% 22.05/3.26 ![X0,X1,X2]: (~organization(sk2)|~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,X1))|greater(capability(sk2,X0),capability(sk2,X2))|smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X2))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X2))),
% 22.05/3.26 inference(paramodulation,[status(thm)],[f807,f579])).
% 22.05/3.26 fof(f1213,definition,(
% 22.05/3.26 ![X0,X1,X2]: (sQ89_spl <=> (~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,X1))|greater(capability(sk2,X2),capability(sk2,X1))|smaller(stock_of_knowledge(sk2,X2),stock_of_knowledge(sk2,X1))|stock_of_knowledge(sk2,X2)=stock_of_knowledge(sk2,X1)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1216,plain,(
% 22.05/3.26 ~sQ9_spl|sQ89_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1209,f134,f1213])).
% 22.05/3.26 fof(f1218,definition,(
% 22.05/3.26 ![X0,X1,X2]: (sQ90_spl <=> (~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,X1))|greater(capability(sk2,X0),capability(sk2,X2))|smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X2))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X2)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1219,plain,(
% 22.05/3.26 ![X0,X1,X2]: (~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,X1))|greater(capability(sk2,X0),capability(sk2,X2))|smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X2))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X2)|~sQ90_spl)),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1218])).
% 22.05/3.26 fof(f1221,plain,(
% 22.05/3.26 ~sQ9_spl|sQ90_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1211,f134,f1218])).
% 22.05/3.26 fof(f1223,plain,(
% 22.05/3.26 ![X0,X1]: (greater(position(sk2,X0),position(sk2,X1))|smaller(external_ties(sk2,X0),external_ties(sk2,X1))|external_ties(sk2,X0)=external_ties(sk2,X1))),
% 22.05/3.26 inference(resolution,[status(thm)],[f589,f72])).
% 22.05/3.26 fof(f1248,plain,(
% 22.05/3.26 greater(age(sk2,sk5),age(sk2,sk3))|~sQ33_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f986,f76])).
% 22.05/3.26 fof(f1249,plain,(
% 22.05/3.26 greater(age(sk2,sk6),age(sk2,sk3))|~sQ33_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f986,f123])).
% 22.05/3.26 fof(f1252,plain,(
% 22.05/3.26 ~organization(sk2)|greater(external_ties(sk2,sk5),external_ties(sk2,sk3))|~sQ14_spl|~sQ16_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1081,f69])).
% 22.05/3.26 fof(f1259,definition,(
% 22.05/3.26 sQ91_spl <=> (greater(external_ties(sk2,sk5),external_ties(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1260,plain,(
% 22.05/3.26 greater(external_ties(sk2,sk5),external_ties(sk2,sk3))|~sQ91_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1259])).
% 22.05/3.26 fof(f1262,plain,(
% 22.05/3.26 ~sQ9_spl|sQ91_spl|~sQ14_spl|~sQ16_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1252,f134,f1259,f162,f169])).
% 22.05/3.26 fof(f1263,definition,(
% 22.05/3.26 sQ92_spl <=> (greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1264,plain,(
% 22.05/3.26 greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk3))|~sQ92_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1263])).
% 22.05/3.26 fof(f1304,plain,(
% 22.05/3.26 ~organization(sk2)|greater(external_ties(sk2,sk6),external_ties(sk2,sk3))|~sQ33_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1249,f69])).
% 22.05/3.26 fof(f1305,plain,(
% 22.05/3.26 ~organization(sk2)|greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk3))|~sQ33_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1249,f68])).
% 22.05/3.26 fof(f1311,definition,(
% 22.05/3.26 sQ93_spl <=> (greater(external_ties(sk2,sk6),external_ties(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1312,plain,(
% 22.05/3.26 greater(external_ties(sk2,sk6),external_ties(sk2,sk3))|~sQ93_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1311])).
% 22.05/3.26 fof(f1314,plain,(
% 22.05/3.26 ~sQ9_spl|sQ93_spl|~sQ33_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1304,f134,f1311,f322])).
% 22.05/3.26 fof(f1315,definition,(
% 22.05/3.26 sQ94_spl <=> (greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1316,plain,(
% 22.05/3.26 greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk3))|~sQ94_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1315])).
% 22.05/3.26 fof(f1318,plain,(
% 22.05/3.26 ~sQ9_spl|sQ94_spl|~sQ33_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1305,f134,f1315,f322])).
% 22.05/3.26 fof(f1319,plain,(
% 22.05/3.26 ~organization(sk2)|greater(external_ties(sk2,sk5),external_ties(sk2,sk3))|~sQ33_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1248,f69])).
% 22.05/3.26 fof(f1326,plain,(
% 22.05/3.26 ~sQ9_spl|sQ91_spl|~sQ33_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1319,f134,f1259,f322])).
% 22.05/3.26 fof(f1563,plain,(
% 22.05/3.26 greater(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3))|~sQ80_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f945,f45])).
% 22.05/3.26 fof(f1589,plain,(
% 22.05/3.26 ~greater(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3))|~sQ80_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1563,f47])).
% 22.05/3.26 fof(f1590,plain,(
% 22.05/3.26 $false|~sQ80_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f1589,f1563])).
% 22.05/3.26 fof(f1591,plain,(
% 22.05/3.26 ~sQ80_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f1590])).
% 22.05/3.26 fof(f1625,plain,(
% 22.05/3.26 greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5))|~sQ71_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f845,f45])).
% 22.05/3.26 fof(f1630,plain,(
% 22.05/3.26 sQ71_spl|~sQ43_spl|~sQ84_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1026,f844,f418,f1019])).
% 22.05/3.26 fof(f1690,plain,(
% 22.05/3.26 greater(age(sk2,sk6),age(sk2,sk5))|age(sk2,sk6)=age(sk2,sk5)),
% 22.05/3.26 inference(resolution,[status(thm)],[f119,f42])).
% 22.05/3.26 fof(f1691,definition,(
% 22.05/3.26 sQ104_spl <=> (greater(age(sk2,sk6),age(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1694,plain,(
% 22.05/3.26 sQ104_spl|sQ19_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1690,f1691,f200])).
% 22.05/3.26 fof(f1715,definition,(
% 22.05/3.26 sQ105_spl <=> (stock_of_knowledge(sk2,sk6)=stock_of_knowledge(sk2,sk5))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1716,plain,(
% 22.05/3.26 stock_of_knowledge(sk2,sk6)=stock_of_knowledge(sk2,sk5)|~sQ105_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1715])).
% 22.05/3.26 fof(f1719,plain,(
% 22.05/3.26 stock_of_knowledge(sk2,sk6)=stock_of_knowledge(sk2,sk5)|greater_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5))|~sQ10_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f474,f492])).
% 22.05/3.26 fof(f1720,plain,(
% 22.05/3.26 smaller(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk6))|stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,sk6)|~sQ10_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f474,f50])).
% 22.05/3.26 fof(f1721,definition,(
% 22.05/3.26 sQ106_spl <=> (greater_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1724,plain,(
% 22.05/3.26 sQ105_spl|sQ106_spl|~sQ10_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1719,f1715,f1721,f137])).
% 22.05/3.26 fof(f1725,definition,(
% 22.05/3.26 sQ107_spl <=> (smaller(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk6)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1728,plain,(
% 22.05/3.26 sQ107_spl|sQ105_spl|~sQ10_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1720,f1725,f1715,f137])).
% 22.05/3.26 fof(f1729,plain,(
% 22.05/3.26 ~greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk5))|~sQ105_spl|~sQ10_spl),
% 22.05/3.26 inference(backward_demodulation,[status(thm)],[f1716,f474])).
% 22.05/3.26 fof(f1732,plain,(
% 22.05/3.26 greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk5))|~sQ105_spl|~sQ10_spl),
% 22.05/3.26 inference(backward_demodulation,[status(thm)],[f1716,f138])).
% 22.05/3.26 fof(f1738,plain,(
% 22.05/3.26 $false|~sQ105_spl|~sQ10_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f1732,f1729])).
% 22.05/3.26 fof(f1739,plain,(
% 22.05/3.26 ~sQ105_spl|~sQ10_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f1738])).
% 22.05/3.26 fof(f1743,definition,(
% 22.05/3.26 sQ108_spl <=> (external_ties(sk2,sk6)=external_ties(sk2,sk5))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1744,plain,(
% 22.05/3.26 external_ties(sk2,sk6)=external_ties(sk2,sk5)|~sQ108_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1743])).
% 22.05/3.26 fof(f1747,plain,(
% 22.05/3.26 external_ties(sk2,sk6)=external_ties(sk2,sk5)|greater_or_equal(external_ties(sk2,sk6),external_ties(sk2,sk5))|~sQ11_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f478,f492])).
% 22.05/3.26 fof(f1748,plain,(
% 22.05/3.26 smaller(external_ties(sk2,sk5),external_ties(sk2,sk6))|external_ties(sk2,sk5)=external_ties(sk2,sk6)|~sQ11_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f478,f50])).
% 22.05/3.26 fof(f1749,definition,(
% 22.05/3.26 sQ109_spl <=> (greater_or_equal(external_ties(sk2,sk6),external_ties(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1752,plain,(
% 22.05/3.26 sQ108_spl|sQ109_spl|~sQ11_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1747,f1743,f1749,f144])).
% 22.05/3.26 fof(f1753,definition,(
% 22.05/3.26 sQ110_spl <=> (smaller(external_ties(sk2,sk5),external_ties(sk2,sk6)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1756,plain,(
% 22.05/3.26 sQ110_spl|sQ108_spl|~sQ11_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1748,f1753,f1743,f144])).
% 22.05/3.26 fof(f1757,plain,(
% 22.05/3.26 ~greater(external_ties(sk2,sk5),external_ties(sk2,sk5))|~sQ108_spl|~sQ11_spl),
% 22.05/3.26 inference(backward_demodulation,[status(thm)],[f1744,f478])).
% 22.05/3.26 fof(f1760,plain,(
% 22.05/3.26 greater(external_ties(sk2,sk5),external_ties(sk2,sk5))|~sQ108_spl|~sQ11_spl),
% 22.05/3.26 inference(backward_demodulation,[status(thm)],[f1744,f145])).
% 22.05/3.26 fof(f1766,plain,(
% 22.05/3.26 $false|~sQ108_spl|~sQ11_spl),
% 22.05/3.26 inference(forward_subsumption_resolution,[status(thm)],[f1760,f1757])).
% 22.05/3.26 fof(f1767,plain,(
% 22.05/3.26 ~sQ108_spl|~sQ11_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f1766])).
% 22.05/3.26 fof(f1768,plain,(
% 22.05/3.26 ~organization(sk2)|greater(position(sk2,sk5),position(sk2,sk4))|~sQ53_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f530,f66])).
% 22.05/3.26 fof(f1773,plain,(
% 22.05/3.26 ~greater(external_ties(sk2,sk4),external_ties(sk2,sk5))|~sQ53_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f530,f47])).
% 22.05/3.26 fof(f1774,definition,(
% 22.05/3.26 sQ111_spl <=> (greater(position(sk2,sk5),position(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1775,plain,(
% 22.05/3.26 greater(position(sk2,sk5),position(sk2,sk4))|~sQ111_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1774])).
% 22.05/3.26 fof(f1777,plain,(
% 22.05/3.26 ~sQ9_spl|sQ111_spl|~sQ53_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1768,f134,f1774,f529])).
% 22.05/3.26 fof(f1778,plain,(
% 22.05/3.26 ~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk5),internal_friction(sk2,sk4))|greater(capability(sk2,sk5),capability(sk2,sk4))|~sQ54_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f534,f63])).
% 22.05/3.26 fof(f1783,plain,(
% 22.05/3.26 ~greater(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk5))|~sQ54_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f534,f47])).
% 22.05/3.26 fof(f1784,definition,(
% 22.05/3.26 sQ112_spl <=> (smaller_or_equal(internal_friction(sk2,sk5),internal_friction(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1786,plain,(
% 22.05/3.26 ~smaller_or_equal(internal_friction(sk2,sk5),internal_friction(sk2,sk4))|sQ112_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1784])).
% 22.05/3.26 fof(f1787,definition,(
% 22.05/3.26 sQ113_spl <=> (greater(capability(sk2,sk5),capability(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1788,plain,(
% 22.05/3.26 greater(capability(sk2,sk5),capability(sk2,sk4))|~sQ113_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1787])).
% 22.05/3.26 fof(f1790,plain,(
% 22.05/3.26 ~sQ9_spl|~sQ112_spl|sQ113_spl|~sQ54_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1778,f134,f1784,f1787,f533])).
% 22.05/3.26 fof(f1793,plain,(
% 22.05/3.26 ![X0]: (~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,sk5))|sQ57_spl)),
% 22.05/3.26 inference(paramodulation,[status(thm)],[f807,f582])).
% 22.05/3.26 fof(f1810,plain,(
% 22.05/3.26 $false|sQ57_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1793,f89])).
% 22.05/3.26 fof(f1815,plain,(
% 22.05/3.26 sQ57_spl),
% 22.05/3.26 inference(contradiction_clause,[status(thm)],[f1810])).
% 22.05/3.26 fof(f1818,plain,(
% 22.05/3.26 smaller(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3))|hazard_of_mortality(sk2,sk3)=hazard_of_mortality(sk2,sk3)|sQ80_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f946,f193])).
% 22.05/3.26 fof(f1822,plain,(
% 22.05/3.26 sQ80_spl|sQ78_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1818,f944,f937])).
% 22.05/3.26 fof(f1826,plain,(
% 22.05/3.26 smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5))|hazard_of_mortality(sk2,sk5)=hazard_of_mortality(sk2,sk5)|sQ71_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f846,f193])).
% 22.05/3.26 fof(f1830,plain,(
% 22.05/3.26 sQ71_spl|sQ69_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1826,f844,f837])).
% 22.05/3.26 fof(f1834,plain,(
% 22.05/3.26 ~organization(sk2)|has_immunity(sk2,sk5)|has_immunity(sk2,sk6)|~greater_or_equal(capability(sk2,sk6),capability(sk2,sk5))|smaller(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5))|~sQ59_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f591,f61])).
% 22.05/3.26 fof(f1839,plain,(
% 22.05/3.26 ~greater(position(sk2,sk5),position(sk2,sk6))|~sQ59_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f591,f47])).
% 22.05/3.26 fof(f1840,definition,(
% 22.05/3.26 sQ117_spl <=> (greater_or_equal(capability(sk2,sk6),capability(sk2,sk5)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1842,plain,(
% 22.05/3.26 ~greater_or_equal(capability(sk2,sk6),capability(sk2,sk5))|sQ117_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1840])).
% 22.05/3.26 fof(f1843,plain,(
% 22.05/3.26 ~sQ9_spl|sQ5_spl|sQ8_spl|~sQ117_spl|sQ84_spl|~sQ59_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1834,f134,f105,f129,f1840,f1019,f590])).
% 22.05/3.26 fof(f1844,plain,(
% 22.05/3.26 ~organization(sk2)|greater(position(sk2,sk4),position(sk2,sk3))|~sQ85_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1061,f66])).
% 22.05/3.26 fof(f1849,plain,(
% 22.05/3.26 ~greater(external_ties(sk2,sk3),external_ties(sk2,sk4))|~sQ85_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1061,f47])).
% 22.05/3.26 fof(f1850,definition,(
% 22.05/3.26 sQ118_spl <=> (greater(position(sk2,sk4),position(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1851,plain,(
% 22.05/3.26 greater(position(sk2,sk4),position(sk2,sk3))|~sQ118_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1850])).
% 22.05/3.26 fof(f1853,plain,(
% 22.05/3.26 ~sQ9_spl|sQ118_spl|~sQ85_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1844,f134,f1850,f1060])).
% 22.05/3.26 fof(f1854,plain,(
% 22.05/3.26 ~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk4),internal_friction(sk2,sk3))|greater(capability(sk2,sk4),capability(sk2,sk3))|~sQ86_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1065,f63])).
% 22.05/3.26 fof(f1860,definition,(
% 22.05/3.26 sQ119_spl <=> (smaller_or_equal(internal_friction(sk2,sk4),internal_friction(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1862,plain,(
% 22.05/3.26 ~smaller_or_equal(internal_friction(sk2,sk4),internal_friction(sk2,sk3))|sQ119_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1860])).
% 22.05/3.26 fof(f1863,definition,(
% 22.05/3.26 sQ120_spl <=> (greater(capability(sk2,sk4),capability(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1866,plain,(
% 22.05/3.26 ~sQ9_spl|~sQ119_spl|sQ120_spl|~sQ86_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1854,f134,f1860,f1863,f1064])).
% 22.05/3.26 fof(f1867,plain,(
% 22.05/3.26 ~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk5),internal_friction(sk2,sk3))|greater(capability(sk2,sk5),capability(sk2,sk3))|~sQ92_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1264,f63])).
% 22.05/3.26 fof(f1872,plain,(
% 22.05/3.26 ~greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk5))|~sQ92_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1264,f47])).
% 22.05/3.26 fof(f1873,definition,(
% 22.05/3.26 sQ121_spl <=> (smaller_or_equal(internal_friction(sk2,sk5),internal_friction(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1875,plain,(
% 22.05/3.26 ~smaller_or_equal(internal_friction(sk2,sk5),internal_friction(sk2,sk3))|sQ121_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1873])).
% 22.05/3.26 fof(f1876,definition,(
% 22.05/3.26 sQ122_spl <=> (greater(capability(sk2,sk5),capability(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1877,plain,(
% 22.05/3.26 greater(capability(sk2,sk5),capability(sk2,sk3))|~sQ122_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1876])).
% 22.05/3.26 fof(f1879,plain,(
% 22.05/3.26 ~sQ9_spl|~sQ121_spl|sQ122_spl|~sQ92_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1867,f134,f1873,f1876,f1263])).
% 22.05/3.26 fof(f1880,plain,(
% 22.05/3.26 ~organization(sk2)|greater(position(sk2,sk5),position(sk2,sk3))|~sQ91_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1260,f66])).
% 22.05/3.26 fof(f1885,plain,(
% 22.05/3.26 ~greater(external_ties(sk2,sk3),external_ties(sk2,sk5))|~sQ91_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1260,f47])).
% 22.05/3.26 fof(f1886,definition,(
% 22.05/3.26 sQ123_spl <=> (greater(position(sk2,sk5),position(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1887,plain,(
% 22.05/3.26 greater(position(sk2,sk5),position(sk2,sk3))|~sQ123_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f1886])).
% 22.05/3.26 fof(f1889,plain,(
% 22.05/3.26 ~sQ9_spl|sQ123_spl|~sQ91_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1880,f134,f1886,f1259])).
% 22.05/3.26 fof(f1928,plain,(
% 22.05/3.26 greater(age(sk2,sk4),age(sk2,sk3))|age(sk2,sk4)=age(sk2,sk3)|~sQ14_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1057,f42])).
% 22.05/3.26 fof(f1929,definition,(
% 22.05/3.26 sQ124_spl <=> (greater(age(sk2,sk4),age(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f1932,plain,(
% 22.05/3.26 sQ124_spl|sQ15_spl|~sQ14_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f1928,f1929,f165,f162])).
% 22.05/3.26 fof(f2126,definition,(
% 22.05/3.26 sQ126_spl <=> (greater(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2127,plain,(
% 22.05/3.26 greater(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3))|~sQ126_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f2126])).
% 22.05/3.26 fof(f2187,plain,(
% 22.05/3.26 ~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk3))|greater(capability(sk2,sk6),capability(sk2,sk3))|~sQ94_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1316,f63])).
% 22.05/3.26 fof(f2194,definition,(
% 22.05/3.26 sQ134_spl <=> (smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2196,plain,(
% 22.05/3.26 ~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk3))|sQ134_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f2194])).
% 22.05/3.26 fof(f2197,definition,(
% 22.05/3.26 sQ135_spl <=> (greater(capability(sk2,sk6),capability(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2198,plain,(
% 22.05/3.26 greater(capability(sk2,sk6),capability(sk2,sk3))|~sQ135_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f2197])).
% 22.05/3.26 fof(f2200,plain,(
% 22.05/3.26 ~sQ9_spl|~sQ134_spl|sQ135_spl|~sQ94_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f2187,f134,f2194,f2197,f1315])).
% 22.05/3.26 fof(f2201,plain,(
% 22.05/3.26 ~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk4))|greater(capability(sk2,sk6),capability(sk2,sk4))|~sQ52_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f520,f63])).
% 22.05/3.26 fof(f2207,plain,(
% 22.05/3.26 ~greater(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk6))|~sQ52_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f520,f47])).
% 22.05/3.26 fof(f2208,definition,(
% 22.05/3.26 sQ136_spl <=> (smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2210,plain,(
% 22.05/3.26 ~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk4))|sQ136_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f2208])).
% 22.05/3.26 fof(f2211,definition,(
% 22.05/3.26 sQ137_spl <=> (greater(capability(sk2,sk6),capability(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2214,plain,(
% 22.05/3.26 ~sQ9_spl|~sQ136_spl|sQ137_spl|~sQ52_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f2201,f134,f2208,f2211,f519])).
% 22.05/3.26 fof(f2227,plain,(
% 22.05/3.26 ![X0,X1]: (smaller(age(sk2,X0),age(sk2,X1))|age(sk2,X0)=age(sk2,X1)|~organization(sk2)|greater(position(sk2,X0),position(sk2,X1)))),
% 22.05/3.26 inference(resolution,[status(thm)],[f974,f66])).
% 22.05/3.26 fof(f2235,definition,(
% 22.05/3.26 ![X0,X1]: (sQ138_spl <=> (smaller(age(sk2,X0),age(sk2,X1))|age(sk2,X0)=age(sk2,X1)|greater(position(sk2,X0),position(sk2,X1))))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2238,plain,(
% 22.05/3.26 sQ138_spl|~sQ9_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f2227,f2235,f134])).
% 22.05/3.26 fof(f2240,plain,(
% 22.05/3.26 ![X0,X1]: (smaller(age(sk2,X0),age(sk2,X1))|age(sk2,X0)=age(sk2,X1)|~organization(sk2)|~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,X1))|greater(capability(sk2,X0),capability(sk2,X1)))),
% 22.05/3.26 inference(resolution,[status(thm)],[f975,f63])).
% 22.05/3.26 fof(f2248,definition,(
% 22.05/3.26 ![X0,X1]: (sQ139_spl <=> (smaller(age(sk2,X0),age(sk2,X1))|age(sk2,X0)=age(sk2,X1)|~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,X1))|greater(capability(sk2,X0),capability(sk2,X1))))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2251,plain,(
% 22.05/3.26 sQ139_spl|~sQ9_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f2240,f2248,f134])).
% 22.05/3.26 fof(f2252,plain,(
% 22.05/3.26 ~organization(sk2)|greater(position(sk2,sk6),position(sk2,sk3))|~sQ93_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f1312,f66])).
% 22.05/3.26 fof(f2259,definition,(
% 22.05/3.26 sQ140_spl <=> (greater(position(sk2,sk6),position(sk2,sk3)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2260,plain,(
% 22.05/3.26 greater(position(sk2,sk6),position(sk2,sk3))|~sQ140_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f2259])).
% 22.05/3.26 fof(f2262,plain,(
% 22.05/3.26 ~sQ9_spl|sQ140_spl|~sQ93_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f2252,f134,f2259,f1311])).
% 22.05/3.26 fof(f2263,plain,(
% 22.05/3.26 ~organization(sk2)|greater(position(sk2,sk6),position(sk2,sk4))|~sQ51_spl),
% 22.05/3.26 inference(resolution,[status(thm)],[f516,f66])).
% 22.05/3.26 fof(f2270,definition,(
% 22.05/3.26 sQ141_spl <=> (greater(position(sk2,sk6),position(sk2,sk4)))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2271,plain,(
% 22.05/3.26 greater(position(sk2,sk6),position(sk2,sk4))|~sQ141_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f2270])).
% 22.05/3.26 fof(f2273,plain,(
% 22.05/3.26 ~sQ9_spl|sQ141_spl|~sQ51_spl),
% 22.05/3.26 inference(split_clause,[status(thm)],[f2263,f134,f2270,f515])).
% 22.05/3.26 fof(f2277,definition,(
% 22.05/3.26 sQ142_spl <=> (external_ties(sk2,sk5)=external_ties(sk2,sk4))),
% 22.05/3.26 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 22.05/3.26 fof(f2278,plain,(
% 22.05/3.26 external_ties(sk2,sk5)=external_ties(sk2,sk4)|~sQ142_spl),
% 22.05/3.26 inference(component_clause,[status(thm)],[f2277])).
% 22.05/3.26 fof(f2281,plain,(
% 22.05/3.26 smaller(age(sk2,sk4),age(sk2,sk5))|age(sk2,sk4)=age(sk2,sk5)|~sQ53_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1773,f974])).
% 22.05/3.27 fof(f2283,plain,(
% 22.05/3.27 external_ties(sk2,sk5)=external_ties(sk2,sk4)|greater_or_equal(external_ties(sk2,sk5),external_ties(sk2,sk4))|~sQ53_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1773,f492])).
% 22.05/3.27 fof(f2284,plain,(
% 22.05/3.27 smaller(external_ties(sk2,sk4),external_ties(sk2,sk5))|external_ties(sk2,sk4)=external_ties(sk2,sk5)|~sQ53_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1773,f50])).
% 22.05/3.27 fof(f2285,plain,(
% 22.05/3.27 sQ60_spl|sQ61_spl|~sQ53_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2281,f618,f621,f529])).
% 22.05/3.27 fof(f2286,definition,(
% 22.05/3.27 sQ143_spl <=> (greater_or_equal(external_ties(sk2,sk5),external_ties(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2289,plain,(
% 22.05/3.27 sQ142_spl|sQ143_spl|~sQ53_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2283,f2277,f2286,f529])).
% 22.05/3.27 fof(f2290,definition,(
% 22.05/3.27 sQ144_spl <=> (smaller(external_ties(sk2,sk4),external_ties(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2293,plain,(
% 22.05/3.27 sQ144_spl|sQ142_spl|~sQ53_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2284,f2290,f2277,f529])).
% 22.05/3.27 fof(f2294,plain,(
% 22.05/3.27 ~greater(external_ties(sk2,sk5),external_ties(sk2,sk5))|~sQ142_spl|~sQ53_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f2278,f1773])).
% 22.05/3.27 fof(f2299,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk5),external_ties(sk2,sk5))|~sQ142_spl|~sQ53_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f2278,f530])).
% 22.05/3.27 fof(f2317,plain,(
% 22.05/3.27 $false|~sQ142_spl|~sQ53_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2299,f2294])).
% 22.05/3.27 fof(f2318,plain,(
% 22.05/3.27 ~sQ142_spl|~sQ53_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2317])).
% 22.05/3.27 fof(f2323,plain,(
% 22.05/3.27 greater_or_equal(position(sk2,sk5),position(sk2,sk4))|~sQ111_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1775,f43])).
% 22.05/3.27 fof(f2326,definition,(
% 22.05/3.27 sQ145_spl <=> (greater_or_equal(capability(sk2,sk5),capability(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2328,plain,(
% 22.05/3.27 ~greater_or_equal(capability(sk2,sk5),capability(sk2,sk4))|sQ145_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f2326])).
% 22.05/3.27 fof(f2336,definition,(
% 22.05/3.27 sQ147_spl <=> (stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,sk4))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2337,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,sk4)|~sQ147_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f2336])).
% 22.05/3.27 fof(f2342,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,sk4)|greater_or_equal(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))|~sQ54_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1783,f492])).
% 22.05/3.27 fof(f2343,plain,(
% 22.05/3.27 smaller(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk5))|stock_of_knowledge(sk2,sk4)=stock_of_knowledge(sk2,sk5)|~sQ54_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1783,f50])).
% 22.05/3.27 fof(f2345,definition,(
% 22.05/3.27 sQ148_spl <=> (greater_or_equal(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2348,plain,(
% 22.05/3.27 sQ147_spl|sQ148_spl|~sQ54_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2342,f2336,f2345,f533])).
% 22.05/3.27 fof(f2349,definition,(
% 22.05/3.27 sQ149_spl <=> (smaller(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2352,plain,(
% 22.05/3.27 sQ149_spl|sQ147_spl|~sQ54_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2343,f2349,f2336,f533])).
% 22.05/3.27 fof(f2353,plain,(
% 22.05/3.27 ~greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk5))|~sQ147_spl|~sQ54_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f2337,f1783])).
% 22.05/3.27 fof(f2358,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk5))|~sQ147_spl|~sQ54_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f2337,f534])).
% 22.05/3.27 fof(f2376,plain,(
% 22.05/3.27 $false|~sQ147_spl|~sQ54_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2358,f2353])).
% 22.05/3.27 fof(f2377,plain,(
% 22.05/3.27 ~sQ147_spl|~sQ54_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2376])).
% 22.05/3.27 fof(f2380,plain,(
% 22.05/3.27 ![X0]: (~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,sk4))|sQ112_spl)),
% 22.05/3.27 inference(paramodulation,[status(thm)],[f807,f1786])).
% 22.05/3.27 fof(f2397,plain,(
% 22.05/3.27 $false|sQ112_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2380,f89])).
% 22.05/3.27 fof(f2402,plain,(
% 22.05/3.27 sQ112_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2397])).
% 22.05/3.27 fof(f2407,plain,(
% 22.05/3.27 greater_or_equal(capability(sk2,sk6),capability(sk2,sk5))|~sQ58_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f584,f43])).
% 22.05/3.27 fof(f2409,plain,(
% 22.05/3.27 ~greater(capability(sk2,sk5),capability(sk2,sk6))|~sQ58_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f584,f47])).
% 22.05/3.27 fof(f2410,definition,(
% 22.05/3.27 sQ153_spl <=> (greater_or_equal(position(sk2,sk6),position(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2414,plain,(
% 22.05/3.27 $false|sQ117_spl|~sQ58_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2407,f1842])).
% 22.05/3.27 fof(f2415,plain,(
% 22.05/3.27 sQ117_spl|~sQ58_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2414])).
% 22.05/3.27 fof(f2565,plain,(
% 22.05/3.27 ~greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5))|~sQ71_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1625,f47])).
% 22.05/3.27 fof(f2566,plain,(
% 22.05/3.27 $false|~sQ71_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2565,f1625])).
% 22.05/3.27 fof(f2567,plain,(
% 22.05/3.27 ~sQ71_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2566])).
% 22.05/3.27 fof(f2653,plain,(
% 22.05/3.27 ![X0]: (smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,sk5))|~sQ57_spl)),
% 22.05/3.27 inference(paramodulation,[status(thm)],[f807,f581])).
% 22.05/3.27 fof(f2655,plain,(
% 22.05/3.27 ![X0]: (smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,X0))|~sQ57_spl)),
% 22.05/3.27 inference(paramodulation,[status(thm)],[f807,f581])).
% 22.05/3.27 fof(f2665,plain,(
% 22.05/3.27 $false|~sQ57_spl|sQ136_spl),
% 22.05/3.27 inference(backward_subsumption_resolution,[status(thm)],[f2210,f2655])).
% 22.05/3.27 fof(f2666,plain,(
% 22.05/3.27 $false|~sQ57_spl|sQ134_spl),
% 22.05/3.27 inference(backward_subsumption_resolution,[status(thm)],[f2196,f2655])).
% 22.05/3.27 fof(f2667,plain,(
% 22.05/3.27 ~sQ57_spl|sQ136_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2665])).
% 22.05/3.27 fof(f2668,plain,(
% 22.05/3.27 ~sQ57_spl|sQ134_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2666])).
% 22.05/3.27 fof(f2669,plain,(
% 22.05/3.27 ![X0]: (~organization(sk2)|greater(capability(sk2,X0),capability(sk2,sk5))|smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk5))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,sk5)|~sQ57_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f2653,f579])).
% 22.05/3.27 fof(f2673,plain,(
% 22.05/3.27 ![X0,X1]: (smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,X1))|~sQ57_spl)),
% 22.05/3.27 inference(paramodulation,[status(thm)],[f807,f2653])).
% 22.05/3.27 fof(f2675,definition,(
% 22.05/3.27 ![X0]: (sQ166_spl <=> (greater(capability(sk2,X0),capability(sk2,sk5))|smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk5))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2678,plain,(
% 22.05/3.27 ~sQ9_spl|sQ166_spl|~sQ57_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2669,f134,f2675,f580])).
% 22.05/3.27 fof(f2679,plain,(
% 22.05/3.27 $false|~sQ57_spl|sQ121_spl),
% 22.05/3.27 inference(backward_subsumption_resolution,[status(thm)],[f1875,f2673])).
% 22.05/3.27 fof(f2680,plain,(
% 22.05/3.27 $false|~sQ57_spl|sQ119_spl),
% 22.05/3.27 inference(backward_subsumption_resolution,[status(thm)],[f1862,f2673])).
% 22.05/3.27 fof(f2682,plain,(
% 22.05/3.27 ![X0,X1]: (greater(capability(sk2,X0),capability(sk2,X1))|smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X1)|~sQ57_spl|~sQ90_spl)),
% 22.05/3.27 inference(backward_subsumption_resolution,[status(thm)],[f1219,f2673])).
% 22.05/3.27 fof(f2684,plain,(
% 22.05/3.27 ~sQ57_spl|sQ121_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2679])).
% 22.05/3.27 fof(f2685,plain,(
% 22.05/3.27 ~sQ57_spl|sQ119_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2680])).
% 22.05/3.27 fof(f2686,plain,(
% 22.05/3.27 ![X0,X1]: (~organization(sk2)|greater(capability(sk2,X0),capability(sk2,X1))|smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X1)|~sQ57_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f2673,f579])).
% 22.05/3.27 fof(f2692,definition,(
% 22.05/3.27 ![X0,X1]: (sQ167_spl <=> (greater(capability(sk2,X0),capability(sk2,X1))|smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X1)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2695,plain,(
% 22.05/3.27 ~sQ9_spl|sQ167_spl|~sQ57_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2686,f134,f2692,f580])).
% 22.05/3.27 fof(f2703,definition,(
% 22.05/3.27 sQ169_spl <=> (capability(sk2,sk6)=capability(sk2,sk5))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2704,plain,(
% 22.05/3.27 capability(sk2,sk6)=capability(sk2,sk5)|~sQ169_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f2703])).
% 22.05/3.27 fof(f2707,definition,(
% 22.05/3.27 sQ170_spl <=> (position(sk2,sk6)=position(sk2,sk5))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2708,plain,(
% 22.05/3.27 position(sk2,sk6)=position(sk2,sk5)|~sQ170_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f2707])).
% 22.05/3.27 fof(f2712,plain,(
% 22.05/3.27 position(sk2,sk6)=position(sk2,sk5)|greater_or_equal(position(sk2,sk6),position(sk2,sk5))|~sQ59_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1839,f492])).
% 22.05/3.27 fof(f2713,plain,(
% 22.05/3.27 smaller(position(sk2,sk5),position(sk2,sk6))|position(sk2,sk5)=position(sk2,sk6)|~sQ59_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1839,f50])).
% 22.05/3.27 fof(f2714,plain,(
% 22.05/3.27 sQ170_spl|sQ153_spl|~sQ59_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2712,f2707,f2410,f590])).
% 22.05/3.27 fof(f2715,definition,(
% 22.05/3.27 sQ171_spl <=> (smaller(position(sk2,sk5),position(sk2,sk6)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2718,plain,(
% 22.05/3.27 sQ171_spl|sQ170_spl|~sQ59_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f2713,f2715,f2707,f590])).
% 22.05/3.27 fof(f2719,plain,(
% 22.05/3.27 ~greater(position(sk2,sk5),position(sk2,sk5))|~sQ170_spl|~sQ59_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f2708,f1839])).
% 22.05/3.27 fof(f2722,plain,(
% 22.05/3.27 greater(position(sk2,sk5),position(sk2,sk5))|~sQ170_spl|~sQ59_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f2708,f591])).
% 22.05/3.27 fof(f2730,plain,(
% 22.05/3.27 $false|~sQ170_spl|~sQ59_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2722,f2719])).
% 22.05/3.27 fof(f2731,plain,(
% 22.05/3.27 ~sQ170_spl|~sQ59_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2730])).
% 22.05/3.27 fof(f2736,plain,(
% 22.05/3.27 greater_or_equal(position(sk2,sk4),position(sk2,sk3))|~sQ118_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1851,f43])).
% 22.05/3.27 fof(f2749,definition,(
% 22.05/3.27 sQ174_spl <=> (stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,sk3))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f2750,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,sk3)|~sQ174_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f2749])).
% 22.05/3.27 fof(f2780,plain,(
% 22.05/3.27 has_immunity(sk2,sk6)|~sQ81_spl|~sQ2_spl|sQ1_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f993,f422])).
% 22.05/3.27 fof(f2788,plain,(
% 22.05/3.27 $false|sQ8_spl|~sQ81_spl|~sQ2_spl|sQ1_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2780,f131])).
% 22.05/3.27 fof(f2789,plain,(
% 22.05/3.27 sQ8_spl|~sQ81_spl|~sQ2_spl|sQ1_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2788])).
% 22.05/3.27 fof(f2849,plain,(
% 22.05/3.27 ~greater(hazard_of_mortality(sk2,sk3),hazard_of_mortality(sk2,sk3))|~sQ126_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2127,f47])).
% 22.05/3.27 fof(f2851,plain,(
% 22.05/3.27 $false|~sQ126_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2849,f2127])).
% 22.05/3.27 fof(f2852,plain,(
% 22.05/3.27 ~sQ126_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f2851])).
% 22.05/3.27 fof(f3002,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,sk3)|greater_or_equal(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk3))|~sQ92_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1872,f492])).
% 22.05/3.27 fof(f3003,plain,(
% 22.05/3.27 smaller(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk5))|stock_of_knowledge(sk2,sk3)=stock_of_knowledge(sk2,sk5)|~sQ92_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1872,f50])).
% 22.05/3.27 fof(f3005,definition,(
% 22.05/3.27 sQ180_spl <=> (greater_or_equal(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3008,plain,(
% 22.05/3.27 sQ174_spl|sQ180_spl|~sQ92_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f3002,f2749,f3005,f1263])).
% 22.05/3.27 fof(f3009,definition,(
% 22.05/3.27 sQ181_spl <=> (smaller(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3012,plain,(
% 22.05/3.27 sQ181_spl|sQ174_spl|~sQ92_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f3003,f3009,f2749,f1263])).
% 22.05/3.27 fof(f3182,plain,(
% 22.05/3.27 greater_or_equal(position(sk2,sk5),position(sk2,sk3))|~sQ123_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1887,f43])).
% 22.05/3.27 fof(f3184,plain,(
% 22.05/3.27 ~greater(position(sk2,sk3),position(sk2,sk5))|~sQ123_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1887,f47])).
% 22.05/3.27 fof(f3185,definition,(
% 22.05/3.27 sQ184_spl <=> (greater_or_equal(capability(sk2,sk5),capability(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3193,plain,(
% 22.05/3.27 smaller(capability(sk2,sk5),capability(sk2,sk6))|capability(sk2,sk5)=capability(sk2,sk6)|~sQ58_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2409,f50])).
% 22.05/3.27 fof(f3195,definition,(
% 22.05/3.27 sQ185_spl <=> (smaller(capability(sk2,sk5),capability(sk2,sk6)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3198,plain,(
% 22.05/3.27 sQ185_spl|sQ169_spl|~sQ58_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f3193,f3195,f2703,f583])).
% 22.05/3.27 fof(f3199,plain,(
% 22.05/3.27 ~greater(capability(sk2,sk5),capability(sk2,sk5))|~sQ169_spl|~sQ58_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f2704,f2409])).
% 22.05/3.27 fof(f3201,plain,(
% 22.05/3.27 greater(capability(sk2,sk5),capability(sk2,sk5))|~sQ169_spl|~sQ58_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f2704,f584])).
% 22.05/3.27 fof(f3210,plain,(
% 22.05/3.27 $false|~sQ169_spl|~sQ58_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f3201,f3199])).
% 22.05/3.27 fof(f3211,plain,(
% 22.05/3.27 ~sQ169_spl|~sQ58_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f3210])).
% 22.05/3.27 fof(f3219,definition,(
% 22.05/3.27 sQ186_spl <=> (greater_or_equal(position(sk2,sk4),position(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3221,plain,(
% 22.05/3.27 ~greater_or_equal(position(sk2,sk4),position(sk2,sk3))|sQ186_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f3219])).
% 22.05/3.27 fof(f3247,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk3))|~sQ174_spl|~sQ92_spl),
% 22.05/3.27 inference(forward_demodulation,[status(thm)],[f2750,f1264])).
% 22.05/3.27 fof(f3253,plain,(
% 22.05/3.27 ~greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk3))|~sQ174_spl|~sQ92_spl),
% 22.05/3.27 inference(forward_demodulation,[status(thm)],[f2750,f1872])).
% 22.05/3.27 fof(f3254,plain,(
% 22.05/3.27 $false|~sQ174_spl|~sQ92_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f3253,f3247])).
% 22.05/3.27 fof(f3255,plain,(
% 22.05/3.27 ~sQ174_spl|~sQ92_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f3254])).
% 22.05/3.27 fof(f3386,plain,(
% 22.05/3.27 ![X0,X1]: (smaller(external_ties(sk2,X0),external_ties(sk2,X1))|external_ties(sk2,X0)=external_ties(sk2,X1)|~organization(sk2)|has_immunity(sk2,X1)|has_immunity(sk2,X0)|~greater_or_equal(capability(sk2,X0),capability(sk2,X1))|smaller(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,X1)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f1223,f61])).
% 22.05/3.27 fof(f3394,definition,(
% 22.05/3.27 ![X0,X1]: (sQ187_spl <=> (smaller(external_ties(sk2,X0),external_ties(sk2,X1))|external_ties(sk2,X0)=external_ties(sk2,X1)|has_immunity(sk2,X1)|has_immunity(sk2,X0)|~greater_or_equal(capability(sk2,X0),capability(sk2,X1))|smaller(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,X1))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3397,plain,(
% 22.05/3.27 sQ187_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f3386,f3394,f134])).
% 22.05/3.27 fof(f3398,plain,(
% 22.05/3.27 ![X0]: (smaller(age(sk2,sk5),age(sk2,X0))|age(sk2,sk5)=age(sk2,X0)|~organization(sk2)|greater(external_ties(sk2,sk6),external_ties(sk2,X0)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f668,f69])).
% 22.05/3.27 fof(f3399,plain,(
% 22.05/3.27 ![X0]: (smaller(age(sk2,sk5),age(sk2,X0))|age(sk2,sk5)=age(sk2,X0)|~organization(sk2)|greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,X0)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f668,f68])).
% 22.05/3.27 fof(f3412,definition,(
% 22.05/3.27 ![X0]: (sQ188_spl <=> (smaller(age(sk2,sk5),age(sk2,X0))|age(sk2,sk5)=age(sk2,X0)|greater(external_ties(sk2,sk6),external_ties(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3415,plain,(
% 22.05/3.27 sQ188_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f3398,f3412,f134])).
% 22.05/3.27 fof(f3416,definition,(
% 22.05/3.27 ![X0]: (sQ189_spl <=> (smaller(age(sk2,sk5),age(sk2,X0))|age(sk2,sk5)=age(sk2,X0)|greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3419,plain,(
% 22.05/3.27 sQ189_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f3399,f3416,f134])).
% 22.05/3.27 fof(f3438,definition,(
% 22.05/3.27 sQ195_spl <=> (smaller(age(sk2,sk5),age(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f3439,plain,(
% 22.05/3.27 smaller(age(sk2,sk5),age(sk2,sk5))|~sQ195_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f3438])).
% 22.05/3.27 fof(f4345,plain,(
% 22.05/3.27 ![X0]: (smaller(age(sk2,X0),age(sk2,sk6))|age(sk2,X0)=age(sk2,sk6)|~organization(sk2)|greater(external_ties(sk2,X0),external_ties(sk2,sk5)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f190,f69])).
% 22.05/3.27 fof(f4346,plain,(
% 22.05/3.27 ![X0]: (smaller(age(sk2,X0),age(sk2,sk6))|age(sk2,X0)=age(sk2,sk6)|~organization(sk2)|greater(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk5)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f190,f68])).
% 22.05/3.27 fof(f4355,definition,(
% 22.05/3.27 ![X0]: (sQ219_spl <=> (smaller(age(sk2,X0),age(sk2,sk6))|age(sk2,X0)=age(sk2,sk6)|greater(external_ties(sk2,X0),external_ties(sk2,sk5))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4358,plain,(
% 22.05/3.27 sQ219_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4345,f4355,f134])).
% 22.05/3.27 fof(f4359,definition,(
% 22.05/3.27 ![X0]: (sQ220_spl <=> (smaller(age(sk2,X0),age(sk2,sk6))|age(sk2,X0)=age(sk2,sk6)|greater(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk5))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4362,plain,(
% 22.05/3.27 sQ220_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4346,f4359,f134])).
% 22.05/3.27 fof(f4399,plain,(
% 22.05/3.27 ![X0]: (X0=age(sk2,sk5)|greater(X0,eta)|greater(age(sk2,sk5),X0))),
% 22.05/3.27 inference(resolution,[status(thm)],[f192,f45])).
% 22.05/3.27 fof(f4424,plain,(
% 22.05/3.27 age(sk2,sk6)=age(sk2,sk5)|greater(age(sk2,sk6),eta)),
% 22.05/3.27 inference(resolution,[status(thm)],[f4399,f92])).
% 22.05/3.27 fof(f4426,plain,(
% 22.05/3.27 ![X0]: (age(sk2,X0)=age(sk2,sk5)|greater(age(sk2,X0),eta)|~organization(sk2)|greater(external_ties(sk2,sk5),external_ties(sk2,X0)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f4399,f69])).
% 22.05/3.27 fof(f4427,plain,(
% 22.05/3.27 ![X0]: (age(sk2,X0)=age(sk2,sk5)|greater(age(sk2,X0),eta)|~organization(sk2)|greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,X0)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f4399,f68])).
% 22.05/3.27 fof(f4441,plain,(
% 22.05/3.27 ![X0,X1]: (X0=age(sk2,sk5)|greater(X0,eta)|~greater(X1,age(sk2,sk5))|greater(X1,X0))),
% 22.05/3.27 inference(resolution,[status(thm)],[f4399,f49])).
% 22.05/3.27 fof(f4443,plain,(
% 22.05/3.27 sQ19_spl|sQ49_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4424,f200,f467])).
% 22.05/3.27 fof(f4444,definition,(
% 22.05/3.27 ![X0]: (sQ227_spl <=> (age(sk2,X0)=age(sk2,sk5)|greater(age(sk2,X0),eta)|greater(external_ties(sk2,sk5),external_ties(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4447,plain,(
% 22.05/3.27 sQ227_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4426,f4444,f134])).
% 22.05/3.27 fof(f4448,definition,(
% 22.05/3.27 ![X0]: (sQ228_spl <=> (age(sk2,X0)=age(sk2,sk5)|greater(age(sk2,X0),eta)|greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4451,plain,(
% 22.05/3.27 sQ228_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4427,f4448,f134])).
% 22.05/3.27 fof(f4473,plain,(
% 22.05/3.27 ![X0]: (X0=age(sk2,sk5)|greater(X0,eta)|greater(age(sk2,sk6),X0))),
% 22.05/3.27 inference(resolution,[status(thm)],[f4441,f77])).
% 22.05/3.27 fof(f4487,plain,(
% 22.05/3.27 ![X0]: (age(sk2,X0)=age(sk2,sk5)|greater(age(sk2,X0),eta)|~organization(sk2)|greater(external_ties(sk2,sk6),external_ties(sk2,X0)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f4473,f69])).
% 22.05/3.27 fof(f4488,plain,(
% 22.05/3.27 ![X0]: (age(sk2,X0)=age(sk2,sk5)|greater(age(sk2,X0),eta)|~organization(sk2)|greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,X0)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f4473,f68])).
% 22.05/3.27 fof(f4505,definition,(
% 22.05/3.27 ![X0]: (sQ234_spl <=> (age(sk2,X0)=age(sk2,sk5)|greater(age(sk2,X0),eta)|greater(external_ties(sk2,sk6),external_ties(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4508,plain,(
% 22.05/3.27 sQ234_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4487,f4505,f134])).
% 22.05/3.27 fof(f4509,definition,(
% 22.05/3.27 ![X0]: (sQ235_spl <=> (age(sk2,X0)=age(sk2,sk5)|greater(age(sk2,X0),eta)|greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4512,plain,(
% 22.05/3.27 sQ235_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4488,f4509,f134])).
% 22.05/3.27 fof(f4541,plain,(
% 22.05/3.27 ![X0]: (smaller(eta,age(sk2,X0))|eta=age(sk2,X0)|~organization(sk2)|greater(external_ties(sk2,sk5),external_ties(sk2,X0)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f670,f69])).
% 22.05/3.27 fof(f4542,plain,(
% 22.05/3.27 ![X0]: (smaller(eta,age(sk2,X0))|eta=age(sk2,X0)|~organization(sk2)|greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,X0)))),
% 22.05/3.27 inference(resolution,[status(thm)],[f670,f68])).
% 22.05/3.27 fof(f4561,definition,(
% 22.05/3.27 ![X0]: (sQ236_spl <=> (smaller(eta,age(sk2,X0))|eta=age(sk2,X0)|greater(external_ties(sk2,sk5),external_ties(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4564,plain,(
% 22.05/3.27 sQ236_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4541,f4561,f134])).
% 22.05/3.27 fof(f4565,definition,(
% 22.05/3.27 ![X0]: (sQ237_spl <=> (smaller(eta,age(sk2,X0))|eta=age(sk2,X0)|greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4568,plain,(
% 22.05/3.27 sQ237_spl|~sQ9_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4542,f4565,f134])).
% 22.05/3.27 fof(f4692,plain,(
% 22.05/3.27 greater_or_equal(position(sk2,sk6),position(sk2,sk4))|~sQ141_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2271,f43])).
% 22.05/3.27 fof(f4695,definition,(
% 22.05/3.27 sQ246_spl <=> (greater_or_equal(capability(sk2,sk6),capability(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4697,plain,(
% 22.05/3.27 ~greater_or_equal(capability(sk2,sk6),capability(sk2,sk4))|sQ246_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f4695])).
% 22.05/3.27 fof(f4706,plain,(
% 22.05/3.27 greater_or_equal(position(sk2,sk6),position(sk2,sk3))|~sQ140_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2260,f43])).
% 22.05/3.27 fof(f4708,plain,(
% 22.05/3.27 ~greater(position(sk2,sk3),position(sk2,sk6))|~sQ140_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2260,f47])).
% 22.05/3.27 fof(f4709,definition,(
% 22.05/3.27 sQ248_spl <=> (greater_or_equal(capability(sk2,sk6),capability(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4711,plain,(
% 22.05/3.27 ~greater_or_equal(capability(sk2,sk6),capability(sk2,sk3))|sQ248_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f4709])).
% 22.05/3.27 fof(f4721,definition,(
% 22.05/3.27 sQ250_spl <=> (external_ties(sk2,sk3)=external_ties(sk2,sk4))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4722,plain,(
% 22.05/3.27 external_ties(sk2,sk3)=external_ties(sk2,sk4)|~sQ250_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f4721])).
% 22.05/3.27 fof(f4724,definition,(
% 22.05/3.27 sQ251_spl <=> (greater_or_equal(external_ties(sk2,sk3),external_ties(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4725,plain,(
% 22.05/3.27 greater_or_equal(external_ties(sk2,sk3),external_ties(sk2,sk4))|~sQ251_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f4724])).
% 22.05/3.27 fof(f4736,plain,(
% 22.05/3.27 ~greater(external_ties(sk2,sk5),external_ties(sk2,sk3))|~sQ250_spl|sQ53_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f4722,f531])).
% 22.05/3.27 fof(f4739,plain,(
% 22.05/3.27 position(sk2,sk3)=position(sk2,sk4)|~sQ250_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f4722,f806])).
% 22.05/3.27 fof(f4745,plain,(
% 22.05/3.27 ![X0]: (~organization(sk2)|~greater(external_ties(sk2,X0),external_ties(sk2,sk3))|greater(position(sk2,X0),position(sk2,sk4))|~sQ250_spl)),
% 22.05/3.27 inference(paramodulation,[status(thm)],[f4722,f66])).
% 22.05/3.27 fof(f4746,plain,(
% 22.05/3.27 ![X0]: (~organization(sk2)|~greater(external_ties(sk2,sk3),external_ties(sk2,X0))|greater(position(sk2,sk4),position(sk2,X0))|~sQ250_spl)),
% 22.05/3.27 inference(paramodulation,[status(thm)],[f4722,f66])).
% 22.05/3.27 fof(f4760,definition,(
% 22.05/3.27 ![X0]: (sQ253_spl <=> (~greater(external_ties(sk2,X0),external_ties(sk2,sk3))|greater(position(sk2,X0),position(sk2,sk4))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4763,plain,(
% 22.05/3.27 ~sQ9_spl|sQ253_spl|~sQ250_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4745,f134,f4760,f4721])).
% 22.05/3.27 fof(f4764,definition,(
% 22.05/3.27 ![X0]: (sQ254_spl <=> (~greater(external_ties(sk2,sk3),external_ties(sk2,X0))|greater(position(sk2,sk4),position(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4767,plain,(
% 22.05/3.27 ~sQ9_spl|sQ254_spl|~sQ250_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4746,f134,f4764,f4721])).
% 22.05/3.27 fof(f4772,plain,(
% 22.05/3.27 ![X0]: (smaller(external_ties(sk2,sk5),external_ties(sk2,X0))|external_ties(sk2,sk5)=external_ties(sk2,X0)|~organization(sk2)|greater(position(sk2,sk6),position(sk2,X0))|~sQ11_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f666,f66])).
% 22.05/3.27 fof(f4790,definition,(
% 22.05/3.27 ![X0]: (sQ255_spl <=> (smaller(external_ties(sk2,sk5),external_ties(sk2,X0))|external_ties(sk2,sk5)=external_ties(sk2,X0)|greater(position(sk2,sk6),position(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f4793,plain,(
% 22.05/3.27 sQ255_spl|~sQ9_spl|~sQ11_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4772,f4790,f134,f144])).
% 22.05/3.27 fof(f5533,plain,(
% 22.05/3.27 ![X0,X1]: (smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X1)|~organization(sk2)|has_immunity(sk2,X1)|has_immunity(sk2,X0)|~greater_or_equal(position(sk2,X0),position(sk2,X1))|smaller(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,X1))|~sQ57_spl|~sQ90_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f2682,f60])).
% 22.05/3.27 fof(f5540,definition,(
% 22.05/3.27 ![X0,X1]: (sQ287_spl <=> (smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))|stock_of_knowledge(sk2,X0)=stock_of_knowledge(sk2,X1)|has_immunity(sk2,X1)|has_immunity(sk2,X0)|~greater_or_equal(position(sk2,X0),position(sk2,X1))|smaller(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,X1))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5543,plain,(
% 22.05/3.27 sQ287_spl|~sQ9_spl|~sQ57_spl|~sQ90_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f5533,f5540,f134,f580,f1218])).
% 22.05/3.27 fof(f5574,plain,(
% 22.05/3.27 greater_or_equal(capability(sk2,sk6),capability(sk2,sk3))|~sQ135_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2198,f43])).
% 22.05/3.27 fof(f5576,plain,(
% 22.05/3.27 ~greater(capability(sk2,sk3),capability(sk2,sk6))|~sQ135_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2198,f47])).
% 22.05/3.27 fof(f5577,definition,(
% 22.05/3.27 sQ288_spl <=> (greater_or_equal(position(sk2,sk6),position(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5579,plain,(
% 22.05/3.27 ~greater_or_equal(position(sk2,sk6),position(sk2,sk3))|sQ288_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5577])).
% 22.05/3.27 fof(f5581,plain,(
% 22.05/3.27 $false|~sQ140_spl|sQ288_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f5579,f4706])).
% 22.05/3.27 fof(f5582,plain,(
% 22.05/3.27 ~sQ140_spl|sQ288_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f5581])).
% 22.05/3.27 fof(f5590,definition,(
% 22.05/3.27 sQ289_spl <=> (greater_or_equal(position(sk2,sk6),position(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5592,plain,(
% 22.05/3.27 ~greater_or_equal(position(sk2,sk6),position(sk2,sk4))|sQ289_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5590])).
% 22.05/3.27 fof(f5597,plain,(
% 22.05/3.27 $false|~sQ141_spl|sQ289_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f5592,f4692])).
% 22.05/3.27 fof(f5598,plain,(
% 22.05/3.27 ~sQ141_spl|sQ289_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f5597])).
% 22.05/3.27 fof(f5617,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))|~sQ26_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f272,f76])).
% 22.05/3.27 fof(f5619,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4))|~sQ26_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f272,f123])).
% 22.05/3.27 fof(f5620,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4))|eta=age(sk2,sk5)|greater(eta,eta)|~sQ26_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f272,f4473])).
% 22.05/3.27 fof(f5627,plain,(
% 22.05/3.27 sQ54_spl|~sQ26_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f5617,f533,f271])).
% 22.05/3.27 fof(f5629,plain,(
% 22.05/3.27 sQ52_spl|sQ23_spl|sQ28_spl|~sQ26_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f5620,f519,f214,f279,f271])).
% 22.05/3.27 fof(f5630,definition,(
% 22.05/3.27 sQ292_spl <=> (greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5631,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk4))|~sQ292_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5630])).
% 22.05/3.27 fof(f5637,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk3)=stock_of_knowledge(sk2,sk4)|greater_or_equal(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk4))|sQ86_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1066,f492])).
% 22.05/3.27 fof(f5640,definition,(
% 22.05/3.27 sQ293_spl <=> (stock_of_knowledge(sk2,sk3)=stock_of_knowledge(sk2,sk4))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5641,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk3)=stock_of_knowledge(sk2,sk4)|~sQ293_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5640])).
% 22.05/3.27 fof(f5643,definition,(
% 22.05/3.27 sQ294_spl <=> (greater_or_equal(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5644,plain,(
% 22.05/3.27 greater_or_equal(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk4))|~sQ294_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5643])).
% 22.05/3.27 fof(f5646,plain,(
% 22.05/3.27 sQ293_spl|sQ294_spl|sQ86_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f5637,f5640,f5643,f1064])).
% 22.05/3.27 fof(f5667,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk3))|~sQ293_spl|~sQ54_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f5641,f534])).
% 22.05/3.27 fof(f5694,plain,(
% 22.05/3.27 sQ92_spl|~sQ293_spl|~sQ54_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f5667,f1263,f5640,f533])).
% 22.05/3.27 fof(f5723,definition,(
% 22.05/3.27 sQ297_spl <=> (external_ties(sk2,sk3)=external_ties(sk2,sk5))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5724,plain,(
% 22.05/3.27 external_ties(sk2,sk3)=external_ties(sk2,sk5)|~sQ297_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5723])).
% 22.05/3.27 fof(f5726,definition,(
% 22.05/3.27 sQ298_spl <=> (greater_or_equal(external_ties(sk2,sk3),external_ties(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5727,plain,(
% 22.05/3.27 greater_or_equal(external_ties(sk2,sk3),external_ties(sk2,sk5))|~sQ298_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5726])).
% 22.05/3.27 fof(f5730,definition,(
% 22.05/3.27 sQ299_spl <=> (smaller(external_ties(sk2,sk5),external_ties(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f5731,plain,(
% 22.05/3.27 smaller(external_ties(sk2,sk5),external_ties(sk2,sk3))|~sQ299_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5730])).
% 22.05/3.27 fof(f5732,plain,(
% 22.05/3.27 ~smaller(external_ties(sk2,sk5),external_ties(sk2,sk3))|sQ299_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f5730])).
% 22.05/3.27 fof(f5768,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk3),external_ties(sk2,sk3))|~sQ297_spl|~sQ91_spl),
% 22.05/3.27 inference(forward_demodulation,[status(thm)],[f5724,f1260])).
% 22.05/3.27 fof(f5772,plain,(
% 22.05/3.27 ~greater(external_ties(sk2,sk3),external_ties(sk2,sk3))|~sQ297_spl|~sQ91_spl),
% 22.05/3.27 inference(forward_demodulation,[status(thm)],[f5724,f1885])).
% 22.05/3.27 fof(f5773,plain,(
% 22.05/3.27 $false|~sQ297_spl|~sQ91_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f5772,f5768])).
% 22.05/3.27 fof(f5774,plain,(
% 22.05/3.27 ~sQ297_spl|~sQ91_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f5773])).
% 22.05/3.27 fof(f6217,plain,(
% 22.05/3.27 ![X0]: (smaller(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,X0))|stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,X0)|~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,X0))|greater(capability(sk2,sk6),capability(sk2,X0))|~sQ10_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f667,f63])).
% 22.05/3.27 fof(f6236,definition,(
% 22.05/3.27 ![X0]: (sQ311_spl <=> (smaller(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,X0))|stock_of_knowledge(sk2,sk5)=stock_of_knowledge(sk2,X0)|~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,X0))|greater(capability(sk2,sk6),capability(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f6239,plain,(
% 22.05/3.27 sQ311_spl|~sQ9_spl|~sQ10_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f6217,f6236,f134,f137])).
% 22.05/3.27 fof(f6859,definition,(
% 22.05/3.27 sQ328_spl <=> (smaller(capability(sk2,sk6),capability(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f6860,plain,(
% 22.05/3.27 smaller(capability(sk2,sk6),capability(sk2,sk3))|~sQ328_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f6859])).
% 22.05/3.27 fof(f6861,plain,(
% 22.05/3.27 ~smaller(capability(sk2,sk6),capability(sk2,sk3))|sQ328_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f6859])).
% 22.05/3.27 fof(f6862,definition,(
% 22.05/3.27 sQ329_spl <=> (capability(sk2,sk6)=capability(sk2,sk3))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ329_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f6863,plain,(
% 22.05/3.27 capability(sk2,sk6)=capability(sk2,sk3)|~sQ329_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f6862])).
% 22.05/3.27 fof(f6866,definition,(
% 22.05/3.27 sQ330_spl <=> (position(sk2,sk6)=position(sk2,sk3))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f6867,plain,(
% 22.05/3.27 position(sk2,sk6)=position(sk2,sk3)|~sQ330_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f6866])).
% 22.05/3.27 fof(f6875,plain,(
% 22.05/3.27 ~greater(capability(sk2,sk5),capability(sk2,sk3))|~sQ329_spl|~sQ58_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f6863,f2409])).
% 22.05/3.27 fof(f6896,plain,(
% 22.05/3.27 $false|~sQ122_spl|~sQ329_spl|~sQ58_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f6875,f1877])).
% 22.05/3.27 fof(f6897,plain,(
% 22.05/3.27 ~sQ122_spl|~sQ329_spl|~sQ58_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f6896])).
% 22.05/3.27 fof(f6898,plain,(
% 22.05/3.27 smaller(external_ties(sk2,sk3),external_ties(sk2,sk6))|external_ties(sk2,sk3)=external_ties(sk2,sk6)|~sQ140_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f4708,f1223])).
% 22.05/3.27 fof(f6901,plain,(
% 22.05/3.27 smaller(position(sk2,sk3),position(sk2,sk6))|position(sk2,sk3)=position(sk2,sk6)|~sQ140_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f4708,f50])).
% 22.05/3.27 fof(f6902,definition,(
% 22.05/3.27 sQ331_spl <=> (smaller(external_ties(sk2,sk3),external_ties(sk2,sk6)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f6905,definition,(
% 22.05/3.27 sQ332_spl <=> (external_ties(sk2,sk3)=external_ties(sk2,sk6))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f6906,plain,(
% 22.05/3.27 external_ties(sk2,sk3)=external_ties(sk2,sk6)|~sQ332_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f6905])).
% 22.05/3.27 fof(f6908,plain,(
% 22.05/3.27 sQ331_spl|sQ332_spl|~sQ140_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f6898,f6902,f6905,f2259])).
% 22.05/3.27 fof(f6910,definition,(
% 22.05/3.27 sQ333_spl <=> (smaller(position(sk2,sk3),position(sk2,sk6)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f6913,plain,(
% 22.05/3.27 sQ333_spl|sQ330_spl|~sQ140_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f6901,f6910,f6866,f2259])).
% 22.05/3.27 fof(f6914,plain,(
% 22.05/3.27 ~greater(position(sk2,sk3),position(sk2,sk3))|~sQ330_spl|~sQ140_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f6867,f4708])).
% 22.05/3.27 fof(f6917,plain,(
% 22.05/3.27 greater(position(sk2,sk3),position(sk2,sk3))|~sQ330_spl|~sQ140_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f6867,f2260])).
% 22.05/3.27 fof(f6943,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk3),external_ties(sk2,sk5))|~sQ332_spl|~sQ11_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f6906,f145])).
% 22.05/3.27 fof(f6983,plain,(
% 22.05/3.27 $false|~sQ330_spl|~sQ140_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f6917,f6914])).
% 22.05/3.27 fof(f6984,plain,(
% 22.05/3.27 ~sQ330_spl|~sQ140_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f6983])).
% 22.05/3.27 fof(f6985,plain,(
% 22.05/3.27 $false|~sQ91_spl|~sQ332_spl|~sQ11_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f6943,f1885])).
% 22.05/3.27 fof(f6986,plain,(
% 22.05/3.27 ~sQ91_spl|~sQ332_spl|~sQ11_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f6985])).
% 22.05/3.27 fof(f7032,definition,(
% 22.05/3.27 sQ334_spl <=> (greater(external_ties(sk2,sk3),external_ties(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7053,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk3),external_ties(sk2,sk4))|external_ties(sk2,sk3)=external_ties(sk2,sk4)|~sQ251_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f4725,f42])).
% 22.05/3.27 fof(f7054,plain,(
% 22.05/3.27 sQ334_spl|sQ250_spl|~sQ251_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7053,f7032,f4721,f4724])).
% 22.05/3.27 fof(f7073,plain,(
% 22.05/3.27 ~sQ91_spl|~sQ250_spl|sQ53_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f4736,f1259,f4721,f529])).
% 22.05/3.27 fof(f7151,plain,(
% 22.05/3.27 ~sQ334_spl|~sQ85_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f1849,f7032,f1060])).
% 22.05/3.27 fof(f7156,plain,(
% 22.05/3.27 greater_or_equal(capability(sk2,sk5),capability(sk2,sk4))|~sQ113_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1788,f43])).
% 22.05/3.27 fof(f7158,plain,(
% 22.05/3.27 ~greater(capability(sk2,sk4),capability(sk2,sk5))|~sQ113_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1788,f47])).
% 22.05/3.27 fof(f7159,definition,(
% 22.05/3.27 sQ340_spl <=> (greater_or_equal(position(sk2,sk5),position(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7161,plain,(
% 22.05/3.27 ~greater_or_equal(position(sk2,sk5),position(sk2,sk4))|sQ340_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f7159])).
% 22.05/3.27 fof(f7173,plain,(
% 22.05/3.27 ~greater(capability(sk2,sk3),capability(sk2,sk5))|~sQ122_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1877,f47])).
% 22.05/3.27 fof(f7174,definition,(
% 22.05/3.27 sQ341_spl <=> (greater_or_equal(position(sk2,sk5),position(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7176,plain,(
% 22.05/3.27 ~greater_or_equal(position(sk2,sk5),position(sk2,sk3))|sQ341_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f7174])).
% 22.05/3.27 fof(f7178,plain,(
% 22.05/3.27 $false|~sQ123_spl|sQ341_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f7176,f3182])).
% 22.05/3.27 fof(f7179,plain,(
% 22.05/3.27 ~sQ123_spl|sQ341_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f7178])).
% 22.05/3.27 fof(f7201,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk4))|stock_of_knowledge(sk2,sk3)=stock_of_knowledge(sk2,sk4)|~sQ294_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f5644,f42])).
% 22.05/3.27 fof(f7202,plain,(
% 22.05/3.27 sQ292_spl|sQ293_spl|~sQ294_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7201,f5630,f5640,f5643])).
% 22.05/3.27 fof(f7246,plain,(
% 22.05/3.27 capability(sk2,sk3)=capability(sk2,sk4)|~sQ293_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f5641,f808])).
% 22.05/3.27 fof(f7252,plain,(
% 22.05/3.27 ![X0]: (~organization(sk2)|~greater(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk3))|~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,sk4))|greater(capability(sk2,X0),capability(sk2,sk4))|~sQ293_spl)),
% 22.05/3.27 inference(paramodulation,[status(thm)],[f5641,f63])).
% 22.05/3.27 fof(f7253,plain,(
% 22.05/3.27 ![X0]: (~organization(sk2)|~greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,X0))|~smaller_or_equal(internal_friction(sk2,sk4),internal_friction(sk2,X0))|greater(capability(sk2,sk4),capability(sk2,X0))|~sQ293_spl)),
% 22.05/3.27 inference(paramodulation,[status(thm)],[f5641,f63])).
% 22.05/3.27 fof(f7276,definition,(
% 22.05/3.27 ![X0]: (sQ342_spl <=> (~greater(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,sk3))|~smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,sk4))|greater(capability(sk2,X0),capability(sk2,sk4))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7279,plain,(
% 22.05/3.27 ~sQ9_spl|sQ342_spl|~sQ293_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7252,f134,f7276,f5640])).
% 22.05/3.27 fof(f7280,definition,(
% 22.05/3.27 ![X0]: (sQ343_spl <=> (~greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,X0))|~smaller_or_equal(internal_friction(sk2,sk4),internal_friction(sk2,X0))|greater(capability(sk2,sk4),capability(sk2,X0))))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7283,plain,(
% 22.05/3.27 ~sQ9_spl|sQ343_spl|~sQ293_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7253,f134,f7280,f5640])).
% 22.05/3.27 fof(f7363,definition,(
% 22.05/3.27 sQ346_spl <=> (position(sk2,sk3)=position(sk2,sk4))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7365,plain,(
% 22.05/3.27 ~position(sk2,sk3)=position(sk2,sk4)|sQ346_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f7363])).
% 22.05/3.27 fof(f7411,definition,(
% 22.05/3.27 sQ352_spl <=> (smaller(capability(sk2,sk5),capability(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7412,plain,(
% 22.05/3.27 smaller(capability(sk2,sk5),capability(sk2,sk3))|~sQ352_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f7411])).
% 22.05/3.27 fof(f7413,plain,(
% 22.05/3.27 ~smaller(capability(sk2,sk5),capability(sk2,sk3))|sQ352_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f7411])).
% 22.05/3.27 fof(f7414,definition,(
% 22.05/3.27 sQ353_spl <=> (capability(sk2,sk5)=capability(sk2,sk3))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7415,plain,(
% 22.05/3.27 capability(sk2,sk5)=capability(sk2,sk3)|~sQ353_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f7414])).
% 22.05/3.27 fof(f7418,definition,(
% 22.05/3.27 sQ354_spl <=> (position(sk2,sk5)=position(sk2,sk3))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7419,plain,(
% 22.05/3.27 position(sk2,sk5)=position(sk2,sk3)|~sQ354_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f7418])).
% 22.05/3.27 fof(f7422,plain,(
% 22.05/3.27 greater(capability(sk2,sk3),capability(sk2,sk3))|~sQ353_spl|~sQ122_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f7415,f1877])).
% 22.05/3.27 fof(f7424,plain,(
% 22.05/3.27 ~greater(capability(sk2,sk3),capability(sk2,sk3))|~sQ353_spl|~sQ122_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f7415,f7173])).
% 22.05/3.27 fof(f7440,plain,(
% 22.05/3.27 $false|~sQ353_spl|~sQ122_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f7424,f7422])).
% 22.05/3.27 fof(f7441,plain,(
% 22.05/3.27 ~sQ353_spl|~sQ122_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f7440])).
% 22.05/3.27 fof(f7588,plain,(
% 22.05/3.27 smaller(external_ties(sk2,sk3),external_ties(sk2,sk5))|external_ties(sk2,sk3)=external_ties(sk2,sk5)|~sQ123_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f3184,f1223])).
% 22.05/3.27 fof(f7591,plain,(
% 22.05/3.27 smaller(position(sk2,sk3),position(sk2,sk5))|position(sk2,sk3)=position(sk2,sk5)|~sQ123_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f3184,f50])).
% 22.05/3.27 fof(f7592,definition,(
% 22.05/3.27 sQ357_spl <=> (smaller(external_ties(sk2,sk3),external_ties(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ357_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7595,plain,(
% 22.05/3.27 sQ357_spl|sQ297_spl|~sQ123_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7588,f7592,f5723,f1886])).
% 22.05/3.27 fof(f7597,definition,(
% 22.05/3.27 sQ358_spl <=> (smaller(position(sk2,sk3),position(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7600,plain,(
% 22.05/3.27 sQ358_spl|sQ354_spl|~sQ123_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7591,f7597,f7418,f1886])).
% 22.05/3.27 fof(f7601,plain,(
% 22.05/3.27 ~greater(position(sk2,sk3),position(sk2,sk3))|~sQ354_spl|~sQ123_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f7419,f3184])).
% 22.05/3.27 fof(f7604,plain,(
% 22.05/3.27 greater(position(sk2,sk3),position(sk2,sk3))|~sQ354_spl|~sQ123_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f7419,f1887])).
% 22.05/3.27 fof(f7623,plain,(
% 22.05/3.27 $false|~sQ354_spl|~sQ123_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f7604,f7601])).
% 22.05/3.27 fof(f7624,plain,(
% 22.05/3.27 ~sQ354_spl|~sQ123_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f7623])).
% 22.05/3.27 fof(f7627,plain,(
% 22.05/3.27 external_ties(sk2,sk5)=external_ties(sk2,sk3)|greater_or_equal(external_ties(sk2,sk5),external_ties(sk2,sk3))|~sQ91_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1885,f492])).
% 22.05/3.27 fof(f7630,definition,(
% 22.05/3.27 sQ359_spl <=> (greater_or_equal(external_ties(sk2,sk5),external_ties(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7633,plain,(
% 22.05/3.27 sQ297_spl|sQ359_spl|~sQ91_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7627,f5723,f7630,f1259])).
% 22.05/3.27 fof(f7647,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk3),external_ties(sk2,sk5))|external_ties(sk2,sk3)=external_ties(sk2,sk5)|~sQ298_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f5727,f42])).
% 22.05/3.27 fof(f7648,definition,(
% 22.05/3.27 sQ360_spl <=> (greater(external_ties(sk2,sk3),external_ties(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f7649,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk3),external_ties(sk2,sk5))|~sQ360_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f7648])).
% 22.05/3.27 fof(f7651,plain,(
% 22.05/3.27 sQ360_spl|sQ297_spl|~sQ298_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7647,f7648,f5723,f5726])).
% 22.05/3.27 fof(f7652,plain,(
% 22.05/3.27 $false|~sQ91_spl|~sQ360_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f7649,f1885])).
% 22.05/3.27 fof(f7653,plain,(
% 22.05/3.27 ~sQ91_spl|~sQ360_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f7652])).
% 22.05/3.27 fof(f7654,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk3),external_ties(sk2,sk5))|~sQ299_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f5731,f45])).
% 22.05/3.27 fof(f7656,plain,(
% 22.05/3.27 sQ360_spl|~sQ299_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f7654,f7648,f5730])).
% 22.05/3.27 fof(f7818,plain,(
% 22.05/3.27 $false|~sQ135_spl|sQ248_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f4711,f5574])).
% 22.05/3.27 fof(f7819,plain,(
% 22.05/3.27 ~sQ135_spl|sQ248_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f7818])).
% 22.05/3.27 fof(f7820,plain,(
% 22.05/3.27 ~greater_or_equal(capability(sk2,sk6),capability(sk2,sk3))|~sQ293_spl|sQ246_spl),
% 22.05/3.27 inference(forward_demodulation,[status(thm)],[f7246,f4697])).
% 22.05/3.27 fof(f7821,plain,(
% 22.05/3.27 $false|~sQ135_spl|~sQ293_spl|sQ246_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f7820,f5574])).
% 22.05/3.27 fof(f7822,plain,(
% 22.05/3.27 ~sQ135_spl|~sQ293_spl|sQ246_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f7821])).
% 22.05/3.27 fof(f7876,plain,(
% 22.05/3.27 $false|~sQ118_spl|sQ186_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f3221,f2736])).
% 22.05/3.27 fof(f7877,plain,(
% 22.05/3.27 ~sQ118_spl|sQ186_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f7876])).
% 22.05/3.27 fof(f8243,plain,(
% 22.05/3.27 smaller(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk6))|stock_of_knowledge(sk2,sk3)=stock_of_knowledge(sk2,sk6)|~sQ135_spl|~sQ57_spl|~sQ90_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f5576,f2682])).
% 22.05/3.27 fof(f8246,plain,(
% 22.05/3.27 smaller(capability(sk2,sk3),capability(sk2,sk6))|capability(sk2,sk3)=capability(sk2,sk6)|~sQ135_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f5576,f50])).
% 22.05/3.27 fof(f8247,definition,(
% 22.05/3.27 sQ363_spl <=> (smaller(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk6)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f8250,definition,(
% 22.05/3.27 sQ364_spl <=> (stock_of_knowledge(sk2,sk3)=stock_of_knowledge(sk2,sk6))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ364_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f8251,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk3)=stock_of_knowledge(sk2,sk6)|~sQ364_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f8250])).
% 22.05/3.27 fof(f8253,plain,(
% 22.05/3.27 sQ363_spl|sQ364_spl|~sQ135_spl|~sQ57_spl|~sQ90_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f8243,f8247,f8250,f2197,f580,f1218])).
% 22.05/3.27 fof(f8255,definition,(
% 22.05/3.27 sQ365_spl <=> (smaller(capability(sk2,sk3),capability(sk2,sk6)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ365_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f8258,plain,(
% 22.05/3.27 sQ365_spl|sQ329_spl|~sQ135_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f8246,f8255,f6862,f2197])).
% 22.05/3.27 fof(f8262,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk3),stock_of_knowledge(sk2,sk5))|~sQ364_spl|~sQ10_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f8251,f138])).
% 22.05/3.27 fof(f8315,plain,(
% 22.05/3.27 $false|~sQ92_spl|~sQ364_spl|~sQ10_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f8262,f1872])).
% 22.05/3.27 fof(f8316,plain,(
% 22.05/3.27 ~sQ92_spl|~sQ364_spl|~sQ10_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f8315])).
% 22.05/3.27 fof(f8336,definition,(
% 22.05/3.27 sQ366_spl <=> (smaller(position(sk2,sk6),position(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ366_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f8337,plain,(
% 22.05/3.27 smaller(position(sk2,sk6),position(sk2,sk3))|~sQ366_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f8336])).
% 22.05/3.27 fof(f8388,plain,(
% 22.05/3.27 greater(capability(sk2,sk3),capability(sk2,sk6))|~sQ328_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f6860,f45])).
% 22.05/3.27 fof(f8390,plain,(
% 22.05/3.27 $false|~sQ135_spl|~sQ328_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f8388,f5576])).
% 22.05/3.27 fof(f8391,plain,(
% 22.05/3.27 ~sQ135_spl|~sQ328_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f8390])).
% 22.05/3.27 fof(f8489,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk5),external_ties(sk2,sk4))|~sQ24_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f264,f76])).
% 22.05/3.27 fof(f8493,plain,(
% 22.05/3.27 greater(external_ties(sk2,sk6),external_ties(sk2,sk4))|eta=age(sk2,sk5)|greater(eta,eta)|~sQ24_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f264,f4473])).
% 22.05/3.27 fof(f8499,plain,(
% 22.05/3.27 sQ53_spl|~sQ24_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f8489,f529,f263])).
% 22.05/3.27 fof(f8501,plain,(
% 22.05/3.27 sQ51_spl|sQ23_spl|sQ28_spl|~sQ24_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f8493,f515,f214,f279,f263])).
% 22.05/3.27 fof(f8521,plain,(
% 22.05/3.27 $false|sQ346_spl|~sQ250_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f4739,f7365])).
% 22.05/3.27 fof(f8522,plain,(
% 22.05/3.27 sQ346_spl|~sQ250_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f8521])).
% 22.05/3.27 fof(f8545,plain,(
% 22.05/3.27 $false|sQ340_spl|~sQ111_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2323,f7161])).
% 22.05/3.27 fof(f8546,plain,(
% 22.05/3.27 sQ340_spl|~sQ111_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f8545])).
% 22.05/3.27 fof(f8618,plain,(
% 22.05/3.27 capability(sk2,sk5)=capability(sk2,sk3)|greater_or_equal(capability(sk2,sk5),capability(sk2,sk3))|~sQ122_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f7173,f492])).
% 22.05/3.27 fof(f8619,plain,(
% 22.05/3.27 smaller(capability(sk2,sk3),capability(sk2,sk5))|capability(sk2,sk3)=capability(sk2,sk5)|~sQ122_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f7173,f50])).
% 22.05/3.27 fof(f8621,plain,(
% 22.05/3.27 sQ353_spl|sQ184_spl|~sQ122_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f8618,f7414,f3185,f1876])).
% 22.05/3.27 fof(f8622,definition,(
% 22.05/3.27 sQ371_spl <=> (smaller(capability(sk2,sk3),capability(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f8625,plain,(
% 22.05/3.27 sQ371_spl|sQ353_spl|~sQ122_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f8619,f8622,f7414,f1876])).
% 22.05/3.27 fof(f8628,definition,(
% 22.05/3.27 sQ372_spl <=> (smaller(position(sk2,sk5),position(sk2,sk3)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f8629,plain,(
% 22.05/3.27 smaller(position(sk2,sk5),position(sk2,sk3))|~sQ372_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f8628])).
% 22.05/3.27 fof(f8658,plain,(
% 22.05/3.27 greater(capability(sk2,sk3),capability(sk2,sk5))|~sQ352_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f7412,f45])).
% 22.05/3.27 fof(f8660,plain,(
% 22.05/3.27 $false|~sQ122_spl|~sQ352_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f8658,f7173])).
% 22.05/3.27 fof(f8661,plain,(
% 22.05/3.27 ~sQ122_spl|~sQ352_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f8660])).
% 22.05/3.27 fof(f9099,plain,(
% 22.05/3.27 $false|~sQ113_spl|sQ145_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f2328,f7156])).
% 22.05/3.27 fof(f9100,plain,(
% 22.05/3.27 ~sQ113_spl|sQ145_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f9099])).
% 22.05/3.27 fof(f9552,plain,(
% 22.05/3.27 smaller(capability(sk2,sk4),capability(sk2,sk5))|capability(sk2,sk4)=capability(sk2,sk5)|~sQ113_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f7158,f50])).
% 22.05/3.27 fof(f9554,definition,(
% 22.05/3.27 sQ397_spl <=> (capability(sk2,sk5)=capability(sk2,sk4))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f9555,plain,(
% 22.05/3.27 capability(sk2,sk5)=capability(sk2,sk4)|~sQ397_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f9554])).
% 22.05/3.27 fof(f9558,definition,(
% 22.05/3.27 sQ398_spl <=> (smaller(capability(sk2,sk4),capability(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ398_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f9561,plain,(
% 22.05/3.27 sQ398_spl|sQ397_spl|~sQ113_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f9552,f9558,f9554,f1787])).
% 22.05/3.27 fof(f9562,plain,(
% 22.05/3.27 ~greater(capability(sk2,sk5),capability(sk2,sk5))|~sQ397_spl|~sQ113_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f9555,f7158])).
% 22.05/3.27 fof(f9563,plain,(
% 22.05/3.27 greater(capability(sk2,sk5),capability(sk2,sk5))|~sQ397_spl|~sQ113_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f9555,f1788])).
% 22.05/3.27 fof(f9580,plain,(
% 22.05/3.27 $false|~sQ397_spl|~sQ113_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f9563,f9562])).
% 22.05/3.27 fof(f9581,plain,(
% 22.05/3.27 ~sQ397_spl|~sQ113_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f9580])).
% 22.05/3.27 fof(f9633,plain,(
% 22.05/3.27 ~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk3),internal_friction(sk2,sk4))|greater(capability(sk2,sk3),capability(sk2,sk4))|~sQ292_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f5631,f63])).
% 22.05/3.27 fof(f9640,definition,(
% 22.05/3.27 sQ399_spl <=> (smaller_or_equal(internal_friction(sk2,sk3),internal_friction(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f9642,plain,(
% 22.05/3.27 ~smaller_or_equal(internal_friction(sk2,sk3),internal_friction(sk2,sk4))|sQ399_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f9640])).
% 22.05/3.27 fof(f9643,definition,(
% 22.05/3.27 sQ400_spl <=> (greater(capability(sk2,sk3),capability(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ400_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f9646,plain,(
% 22.05/3.27 ~sQ9_spl|~sQ399_spl|sQ400_spl|~sQ292_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f9633,f134,f9640,f9643,f5630])).
% 22.05/3.27 fof(f9647,plain,(
% 22.05/3.27 $false|~sQ57_spl|sQ399_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f9642,f2673])).
% 22.05/3.27 fof(f9648,plain,(
% 22.05/3.27 ~sQ57_spl|sQ399_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f9647])).
% 22.05/3.27 fof(f9653,plain,(
% 22.05/3.27 greater(age(sk2,sk5),age(sk2,sk5))|~sQ195_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f3439,f45])).
% 22.05/3.27 fof(f9666,plain,(
% 22.05/3.27 ~greater(age(sk2,sk5),age(sk2,sk5))|~sQ195_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f9653,f47])).
% 22.05/3.27 fof(f9677,plain,(
% 22.05/3.27 $false|~sQ195_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f9666,f9653])).
% 22.05/3.27 fof(f9678,plain,(
% 22.05/3.27 ~sQ195_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f9677])).
% 22.05/3.27 fof(f9814,plain,(
% 22.05/3.27 ~organization(sk2)|~smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk4))|greater(capability(sk2,sk6),capability(sk2,sk4))|~sQ26_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f5619,f63])).
% 22.05/3.27 fof(f9821,plain,(
% 22.05/3.27 ~sQ9_spl|~sQ136_spl|sQ137_spl|~sQ26_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f9814,f134,f2208,f2211,f271])).
% 22.05/3.27 fof(f9822,plain,(
% 22.05/3.27 smaller(age(sk2,sk4),age(sk2,sk6))|age(sk2,sk4)=age(sk2,sk6)|~sQ52_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2207,f975])).
% 22.05/3.27 fof(f9824,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk6)=stock_of_knowledge(sk2,sk4)|greater_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4))|~sQ52_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2207,f492])).
% 22.05/3.27 fof(f9825,plain,(
% 22.05/3.27 smaller(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk6))|stock_of_knowledge(sk2,sk4)=stock_of_knowledge(sk2,sk6)|~sQ52_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f2207,f50])).
% 22.05/3.27 fof(f9826,plain,(
% 22.05/3.27 sQ55_spl|sQ56_spl|~sQ52_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f9822,f538,f541,f519])).
% 22.05/3.27 fof(f9827,definition,(
% 22.05/3.27 sQ407_spl <=> (stock_of_knowledge(sk2,sk6)=stock_of_knowledge(sk2,sk4))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f9828,plain,(
% 22.05/3.27 stock_of_knowledge(sk2,sk6)=stock_of_knowledge(sk2,sk4)|~sQ407_spl),
% 22.05/3.27 inference(component_clause,[status(thm)],[f9827])).
% 22.05/3.27 fof(f9830,definition,(
% 22.05/3.27 sQ408_spl <=> (greater_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f9833,plain,(
% 22.05/3.27 sQ407_spl|sQ408_spl|~sQ52_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f9824,f9827,f9830,f519])).
% 22.05/3.27 fof(f9834,definition,(
% 22.05/3.27 sQ409_spl <=> (smaller(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk6)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f9837,plain,(
% 22.05/3.27 sQ409_spl|sQ407_spl|~sQ52_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f9825,f9834,f9827,f519])).
% 22.05/3.27 fof(f9838,plain,(
% 22.05/3.27 ~greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk6))|~sQ407_spl|~sQ52_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f9828,f2207])).
% 22.05/3.27 fof(f9839,plain,(
% 22.05/3.27 greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk6))|~sQ407_spl|~sQ26_spl),
% 22.05/3.27 inference(backward_demodulation,[status(thm)],[f9828,f5619])).
% 22.05/3.27 fof(f9878,plain,(
% 22.05/3.27 $false|~sQ52_spl|~sQ407_spl|~sQ26_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f9839,f9838])).
% 22.05/3.27 fof(f9879,plain,(
% 22.05/3.27 ~sQ52_spl|~sQ407_spl|~sQ26_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f9878])).
% 22.05/3.27 fof(f10027,plain,(
% 22.05/3.27 greater(position(sk2,sk3),position(sk2,sk6))|~sQ366_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f8337,f45])).
% 22.05/3.27 fof(f10029,plain,(
% 22.05/3.27 $false|~sQ140_spl|~sQ366_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f10027,f4708])).
% 22.05/3.27 fof(f10030,plain,(
% 22.05/3.27 ~sQ140_spl|~sQ366_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f10029])).
% 22.05/3.27 fof(f10062,plain,(
% 22.05/3.27 ![X0]: (smaller(capability(sk2,sk3),X0)|capability(sk2,sk3)=X0|greater(capability(sk2,sk6),X0)|capability(sk2,sk6)=capability(sk2,sk3)|sQ328_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f6861,f671])).
% 22.05/3.27 fof(f10063,plain,(
% 22.05/3.27 ![X0]: (capability(sk2,sk6)=capability(sk2,sk3)|greater(X0,capability(sk2,sk3))|smaller(X0,capability(sk2,sk6))|X0=capability(sk2,sk6)|sQ328_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f6861,f671])).
% 22.05/3.27 fof(f10067,definition,(
% 22.05/3.27 ![X0]: (sQ414_spl <=> (smaller(capability(sk2,sk3),X0)|capability(sk2,sk3)=X0|greater(capability(sk2,sk6),X0)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f10070,plain,(
% 22.05/3.27 sQ414_spl|sQ329_spl|sQ328_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f10062,f10067,f6862,f6859])).
% 22.05/3.27 fof(f10071,definition,(
% 22.05/3.27 ![X0]: (sQ415_spl <=> (greater(X0,capability(sk2,sk3))|smaller(X0,capability(sk2,sk6))|X0=capability(sk2,sk6)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f10074,plain,(
% 22.05/3.27 sQ329_spl|sQ415_spl|sQ328_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f10063,f6862,f10071,f6859])).
% 22.05/3.27 fof(f10101,plain,(
% 22.05/3.27 greater(position(sk2,sk3),position(sk2,sk5))|~sQ372_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f8629,f45])).
% 22.05/3.27 fof(f10103,plain,(
% 22.05/3.27 $false|~sQ123_spl|~sQ372_spl),
% 22.05/3.27 inference(forward_subsumption_resolution,[status(thm)],[f10101,f3184])).
% 22.05/3.27 fof(f10104,plain,(
% 22.05/3.27 ~sQ123_spl|~sQ372_spl),
% 22.05/3.27 inference(contradiction_clause,[status(thm)],[f10103])).
% 22.05/3.27 fof(f10107,plain,(
% 22.05/3.27 ![X0]: (smaller(capability(sk2,sk3),X0)|capability(sk2,sk3)=X0|greater(capability(sk2,sk5),X0)|capability(sk2,sk5)=capability(sk2,sk3)|sQ352_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f7413,f671])).
% 22.05/3.27 fof(f10108,plain,(
% 22.05/3.27 ![X0]: (capability(sk2,sk5)=capability(sk2,sk3)|greater(X0,capability(sk2,sk3))|smaller(X0,capability(sk2,sk5))|X0=capability(sk2,sk5)|sQ352_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f7413,f671])).
% 22.05/3.27 fof(f10112,definition,(
% 22.05/3.27 ![X0]: (sQ421_spl <=> (smaller(capability(sk2,sk3),X0)|capability(sk2,sk3)=X0|greater(capability(sk2,sk5),X0)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f10115,plain,(
% 22.05/3.27 sQ421_spl|sQ353_spl|sQ352_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f10107,f10112,f7414,f7411])).
% 22.05/3.27 fof(f10116,definition,(
% 22.05/3.27 ![X0]: (sQ422_spl <=> (greater(X0,capability(sk2,sk3))|smaller(X0,capability(sk2,sk5))|X0=capability(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f10119,plain,(
% 22.05/3.27 sQ353_spl|sQ422_spl|sQ352_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f10108,f7414,f10116,f7411])).
% 22.05/3.27 fof(f10138,plain,(
% 22.05/3.27 ![X0]: (smaller(external_ties(sk2,sk3),X0)|external_ties(sk2,sk3)=X0|greater(external_ties(sk2,sk5),X0)|external_ties(sk2,sk5)=external_ties(sk2,sk3)|sQ299_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f5732,f671])).
% 22.05/3.27 fof(f10139,plain,(
% 22.05/3.27 ![X0]: (external_ties(sk2,sk5)=external_ties(sk2,sk3)|greater(X0,external_ties(sk2,sk3))|smaller(X0,external_ties(sk2,sk5))|X0=external_ties(sk2,sk5)|sQ299_spl)),
% 22.05/3.27 inference(resolution,[status(thm)],[f5732,f671])).
% 22.05/3.27 fof(f10143,definition,(
% 22.05/3.27 ![X0]: (sQ423_spl <=> (smaller(external_ties(sk2,sk3),X0)|external_ties(sk2,sk3)=X0|greater(external_ties(sk2,sk5),X0)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ423_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f10146,plain,(
% 22.05/3.27 sQ423_spl|sQ297_spl|sQ299_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f10138,f10143,f5723,f5730])).
% 22.05/3.27 fof(f10147,definition,(
% 22.05/3.27 ![X0]: (sQ424_spl <=> (greater(X0,external_ties(sk2,sk3))|smaller(X0,external_ties(sk2,sk5))|X0=external_ties(sk2,sk5)))),
% 22.05/3.27 introduced(definition,[new_symbols(definition,[sQ424_spl])],[split_symbol_definition])).
% 22.05/3.27 fof(f10150,plain,(
% 22.05/3.27 sQ297_spl|sQ424_spl|sQ299_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f10139,f5723,f10147,f5730])).
% 22.05/3.27 fof(f10335,plain,(
% 22.05/3.27 greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))|~sQ84_spl),
% 22.05/3.27 inference(resolution,[status(thm)],[f1020,f45])).
% 22.05/3.27 fof(f10337,plain,(
% 22.05/3.27 sQ0_spl|~sQ84_spl),
% 22.05/3.27 inference(split_clause,[status(thm)],[f10335,f79,f1019])).
% 22.05/3.27 fof(f10338,plain,(
% 22.05/3.27 $false),
% 22.05/3.27 inference(sat_refutation,[status(thm)],[f88,f101,f103,f108,f132,f140,f142,f147,f154,f158,f168,f175,f203,f210,f217,f256,f266,f270,f274,f278,f282,f321,f357,f406,f411,f461,f489,f518,f522,f532,f536,f544,f567,f586,f593,f624,f648,f734,f738,f742,f746,f750,f754,f785,f791,f878,f882,f990,f995,f1018,f1063,f1067,f1075,f1090,f1109,f1112,f1114,f1120,f1144,f1177,f1216,f1221,f1262,f1314,f1318,f1326,f1591,f1630,f1694,f1724,f1728,f1739,f1752,f1756,f1767,f1777,f1790,f1815,f1822,f1830,f1843,f1853,f1866,f1879,f1889,f1932,f2200,f2214,f2238,f2251,f2262,f2273,f2285,f2289,f2293,f2318,f2348,f2352,f2377,f2402,f2415,f2567,f2667,f2668,f2678,f2684,f2685,f2695,f2714,f2718,f2731,f2789,f2852,f3008,f3012,f3198,f3211,f3255,f3397,f3415,f3419,f4358,f4362,f4443,f4447,f4451,f4508,f4512,f4564,f4568,f4763,f4767,f4793,f5543,f5582,f5598,f5627,f5629,f5646,f5694,f5774,f6239,f6897,f6908,f6913,f6984,f6986,f7054,f7073,f7151,f7179,f7202,f7279,f7283,f7441,f7595,f7600,f7624,f7633,f7651,f7653,f7656,f7819,f7822,f7877,f8253,f8258,f8316,f8391,f8499,f8501,f8522,f8546,f8621,f8625,f8661,f9100,f9561,f9581,f9646,f9648,f9678,f9821,f9826,f9833,f9837,f9879,f10030,f10070,f10074,f10104,f10115,f10119,f10146,f10150,f10337])).
% 22.05/3.27 % SZS output end CNFRefutation for theBenchmark.p
% 22.05/3.28 % Elapsed time: 2.897054 seconds
% 22.05/3.28 % CPU time: 22.583823 seconds
% 22.05/3.28 % Total memory used: 165.835 MB
% 22.05/3.28 % Net memory used: 148.191 MB
%------------------------------------------------------------------------------