%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT056-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:51 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT056-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 01:23:49 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.14/0.44 % Refutation found
% 0.14/0.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.44 fof(f2,axiom,(
% 0.14/0.44 (![A,B]: (( ~ smaller(A,B)| smaller_or_equal(A,B) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f4,axiom,(
% 0.14/0.44 (![A,B]: (( ~ greater_or_equal(A,B)| greater(A,B)| A = B ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f5,axiom,(
% 0.14/0.44 (![A,B]: (( ~ greater(A,B)| greater_or_equal(A,B) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f7,axiom,(
% 0.14/0.44 (![A,B]: (( ~ smaller(A,B)| greater(B,A) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f8,axiom,(
% 0.14/0.44 (![A,B]: (( ~ greater(A,B)| smaller(B,A) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f9,axiom,(
% 0.14/0.44 (![A,B]: (( ~ greater(A,B)| ~ greater(B,A) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f10,axiom,(
% 0.14/0.44 (![A,B,C]: (( ~ greater(A,B)| ~ greater(B,C)| greater(A,C) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f11,axiom,(
% 0.14/0.44 (![A,B]: (( smaller(A,B)| A = B| greater(A,B) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f13,axiom,(
% 0.14/0.44 (![A,B]: (( ~ has_endowment(A)| ~ smaller_or_equal(age(A,B),eta)| has_immunity(A,B) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f14,axiom,(
% 0.14/0.44 (![A,B]: (( ~ has_endowment(A)| ~ greater(age(A,B),eta)| ~ has_immunity(A,B) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f19,axiom,(
% 0.14/0.44 (![A,B,C]: (( ~ organization(A)| ~ has_immunity(A,B)| ~ has_immunity(A,C)| hazard_of_mortality(A,B) = hazard_of_mortality(A,C) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f20,axiom,(
% 0.14/0.44 (![A,B,C]: (( ~ organization(A)| ~ has_immunity(A,B)| has_immunity(A,C)| greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f21,negated_conjecture,(
% 0.14/0.44 organization(sk2) ),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f22,negated_conjecture,(
% 0.14/0.44 has_endowment(sk2) ),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f23,negated_conjecture,(
% 0.14/0.44 age(sk2,sk3) = zero ),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f24,negated_conjecture,(
% 0.14/0.44 smaller_or_equal(age(sk2,sk4),eta) ),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f25,negated_conjecture,(
% 0.14/0.44 greater(age(sk2,sk5),eta) ),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f26,negated_conjecture,(
% 0.14/0.44 greater_or_equal(eta,sigma) ),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f27,negated_conjecture,(
% 0.14/0.44 greater(sigma,zero) ),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f28,negated_conjecture,(
% 0.14/0.44 ( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f30,plain,(
% 0.14/0.44 ![X0,X1]: (~smaller(X0,X1)|smaller_or_equal(X0,X1))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/0.44 fof(f32,plain,(
% 0.14/0.44 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.44 fof(f33,plain,(
% 0.14/0.44 ![X0,X1]: (~greater(X0,X1)|greater_or_equal(X0,X1))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.44 fof(f35,plain,(
% 0.14/0.44 ![X0,X1]: (~smaller(X0,X1)|greater(X1,X0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.44 fof(f36,plain,(
% 0.14/0.44 ![X0,X1]: (~greater(X0,X1)|smaller(X1,X0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.44 fof(f37,plain,(
% 0.14/0.44 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f9])).
% 0.14/0.44 fof(f38,plain,(
% 0.14/0.44 ![A,C]: ((![B]: (~greater(A,B)|~greater(B,C)))|greater(A,C))),
% 0.14/0.44 inference(miniscoping,[status(thm)],[f10])).
% 0.14/0.44 fof(f39,plain,(
% 0.14/0.44 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f38])).
% 0.14/0.44 fof(f40,plain,(
% 0.14/0.44 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater(X0,X1))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f11])).
% 0.14/0.44 fof(f42,plain,(
% 0.14/0.44 ![X0,X1]: (~has_endowment(X0)|~smaller_or_equal(age(X0,X1),eta)|has_immunity(X0,X1))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/0.44 fof(f43,plain,(
% 0.14/0.44 ![X0,X1]: (~has_endowment(X0)|~greater(age(X0,X1),eta)|~has_immunity(X0,X1))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f14])).
% 0.14/0.44 fof(f48,plain,(
% 0.14/0.44 ![X0,X1,X2]: (~organization(X0)|~has_immunity(X0,X1)|~has_immunity(X0,X2)|hazard_of_mortality(X0,X1)=hazard_of_mortality(X0,X2))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/0.44 fof(f49,plain,(
% 0.14/0.44 ![X0,X1,X2]: (~organization(X0)|~has_immunity(X0,X1)|has_immunity(X0,X2)|greater(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f20])).
% 0.14/0.44 fof(f50,plain,(
% 0.14/0.44 organization(sk2)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f21])).
% 0.14/0.44 fof(f51,plain,(
% 0.14/0.44 has_endowment(sk2)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/0.44 fof(f52,plain,(
% 0.14/0.44 age(sk2,sk3)=zero),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/0.44 fof(f53,plain,(
% 0.14/0.44 smaller_or_equal(age(sk2,sk4),eta)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/0.44 fof(f54,plain,(
% 0.14/0.44 greater(age(sk2,sk5),eta)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f25])).
% 0.14/0.44 fof(f55,plain,(
% 0.14/0.44 greater_or_equal(eta,sigma)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f26])).
% 0.14/0.44 fof(f56,plain,(
% 0.14/0.44 greater(sigma,zero)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/0.44 fof(f57,plain,(
% 0.14/0.44 ~greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))|~hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/0.44 fof(f58,definition,(
% 0.14/0.44 sQ0_spl <=> (greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f60,plain,(
% 0.14/0.44 ~greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))|sQ0_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f58])).
% 0.14/0.44 fof(f61,definition,(
% 0.14/0.44 sQ1_spl <=> (hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f62,plain,(
% 0.14/0.44 hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)|~sQ1_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f61])).
% 0.14/0.44 fof(f63,plain,(
% 0.14/0.44 ~hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)|sQ1_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f61])).
% 0.14/0.44 fof(f64,plain,(
% 0.14/0.44 ~sQ0_spl|~sQ1_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f57,f58,f61])).
% 0.14/0.44 fof(f69,plain,(
% 0.14/0.44 greater(eta,sigma)|eta=sigma),
% 0.14/0.44 inference(resolution,[status(thm)],[f55,f32])).
% 0.14/0.44 fof(f70,definition,(
% 0.14/0.44 sQ2_spl <=> (greater(eta,sigma))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f71,plain,(
% 0.14/0.44 greater(eta,sigma)|~sQ2_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f70])).
% 0.14/0.44 fof(f73,definition,(
% 0.14/0.44 sQ3_spl <=> (eta=sigma)),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f74,plain,(
% 0.14/0.44 eta=sigma|~sQ3_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f73])).
% 0.14/0.44 fof(f76,plain,(
% 0.14/0.44 sQ2_spl|sQ3_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f69,f70,f73])).
% 0.14/0.44 fof(f89,plain,(
% 0.14/0.44 ~greater(zero,sigma)),
% 0.14/0.44 inference(resolution,[status(thm)],[f37,f56])).
% 0.14/0.44 fof(f91,plain,(
% 0.14/0.44 ![X0]: (~greater(zero,X0)|greater(sigma,X0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f39,f56])).
% 0.14/0.44 fof(f92,plain,(
% 0.14/0.44 ~has_endowment(sk2)|~smaller_or_equal(zero,eta)|has_immunity(sk2,sk3)),
% 0.14/0.44 inference(paramodulation,[status(thm)],[f52,f42])).
% 0.14/0.44 fof(f93,definition,(
% 0.14/0.44 sQ6_spl <=> (has_endowment(sk2))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f95,plain,(
% 0.14/0.44 ~has_endowment(sk2)|sQ6_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f93])).
% 0.14/0.44 fof(f96,definition,(
% 0.14/0.44 sQ7_spl <=> (smaller_or_equal(zero,eta))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f98,plain,(
% 0.14/0.44 ~smaller_or_equal(zero,eta)|sQ7_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f96])).
% 0.14/0.44 fof(f99,definition,(
% 0.14/0.44 sQ8_spl <=> (has_immunity(sk2,sk3))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f100,plain,(
% 0.14/0.44 has_immunity(sk2,sk3)|~sQ8_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f99])).
% 0.14/0.44 fof(f102,plain,(
% 0.14/0.44 ~sQ6_spl|~sQ7_spl|sQ8_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f92,f93,f96,f99])).
% 0.14/0.44 fof(f107,plain,(
% 0.14/0.44 ![X0,X1]: (smaller(X0,X1)|X0=X1|smaller(X1,X0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f40,f36])).
% 0.14/0.44 fof(f125,plain,(
% 0.14/0.44 $false|sQ6_spl),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f95,f51])).
% 0.14/0.44 fof(f126,plain,(
% 0.14/0.44 sQ6_spl),
% 0.14/0.44 inference(contradiction_clause,[status(thm)],[f125])).
% 0.14/0.44 fof(f131,plain,(
% 0.14/0.44 ~has_endowment(sk2)|has_immunity(sk2,sk4)),
% 0.14/0.44 inference(resolution,[status(thm)],[f53,f42])).
% 0.14/0.44 fof(f133,definition,(
% 0.14/0.44 sQ12_spl <=> (has_immunity(sk2,sk4))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f134,plain,(
% 0.14/0.44 has_immunity(sk2,sk4)|~sQ12_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f133])).
% 0.14/0.44 fof(f136,plain,(
% 0.14/0.44 ~sQ6_spl|sQ12_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f131,f93,f133])).
% 0.14/0.44 fof(f167,definition,(
% 0.14/0.44 sQ18_spl <=> (smaller(zero,eta))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f168,plain,(
% 0.14/0.44 smaller(zero,eta)|~sQ18_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f167])).
% 0.14/0.44 fof(f170,definition,(
% 0.14/0.44 sQ19_spl <=> (zero=eta)),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f171,plain,(
% 0.14/0.44 zero=eta|~sQ19_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f170])).
% 0.14/0.44 fof(f174,plain,(
% 0.14/0.44 ~has_endowment(sk2)|~has_immunity(sk2,sk5)),
% 0.14/0.44 inference(resolution,[status(thm)],[f54,f43])).
% 0.14/0.44 fof(f175,plain,(
% 0.14/0.44 smaller(eta,age(sk2,sk5))),
% 0.14/0.44 inference(resolution,[status(thm)],[f54,f36])).
% 0.14/0.44 fof(f177,plain,(
% 0.14/0.44 ~greater(eta,age(sk2,sk5))),
% 0.14/0.44 inference(resolution,[status(thm)],[f54,f37])).
% 0.14/0.44 fof(f178,plain,(
% 0.14/0.44 greater_or_equal(age(sk2,sk5),eta)),
% 0.14/0.44 inference(resolution,[status(thm)],[f54,f33])).
% 0.14/0.44 fof(f179,definition,(
% 0.14/0.44 sQ20_spl <=> (has_immunity(sk2,sk5))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f181,plain,(
% 0.14/0.44 ~has_immunity(sk2,sk5)|sQ20_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f179])).
% 0.14/0.44 fof(f182,plain,(
% 0.14/0.44 ~sQ6_spl|~sQ20_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f174,f93,f179])).
% 0.14/0.44 fof(f183,plain,(
% 0.14/0.44 ![X0]: (~organization(sk2)|has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk4))|~sQ12_spl)),
% 0.14/0.44 inference(resolution,[status(thm)],[f134,f49])).
% 0.14/0.44 fof(f184,plain,(
% 0.14/0.44 ![X0]: (~organization(sk2)|~has_immunity(sk2,X0)|hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,X0)|~sQ12_spl)),
% 0.14/0.44 inference(resolution,[status(thm)],[f134,f48])).
% 0.14/0.44 fof(f185,definition,(
% 0.14/0.44 sQ21_spl <=> (organization(sk2))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f187,plain,(
% 0.14/0.44 ~organization(sk2)|sQ21_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f185])).
% 0.14/0.44 fof(f188,definition,(
% 0.14/0.44 ![X0]: (sQ22_spl <=> (has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk4))))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f189,plain,(
% 0.14/0.44 ![X0]: (has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk4))|~sQ22_spl)),
% 0.14/0.44 inference(component_clause,[status(thm)],[f188])).
% 0.14/0.44 fof(f191,plain,(
% 0.14/0.44 ~sQ21_spl|sQ22_spl|~sQ12_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f183,f185,f188,f133])).
% 0.14/0.44 fof(f192,definition,(
% 0.14/0.44 ![X0]: (sQ23_spl <=> (~has_immunity(sk2,X0)|hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,X0)))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f193,plain,(
% 0.14/0.44 ![X0]: (~has_immunity(sk2,X0)|hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,X0)|~sQ23_spl)),
% 0.14/0.44 inference(component_clause,[status(thm)],[f192])).
% 0.14/0.44 fof(f195,plain,(
% 0.14/0.44 ~sQ21_spl|sQ23_spl|~sQ12_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f184,f185,f192,f133])).
% 0.14/0.44 fof(f196,plain,(
% 0.14/0.44 $false|sQ21_spl),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f187,f50])).
% 0.14/0.44 fof(f197,plain,(
% 0.14/0.44 sQ21_spl),
% 0.14/0.44 inference(contradiction_clause,[status(thm)],[f196])).
% 0.14/0.44 fof(f200,plain,(
% 0.14/0.44 smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))|hazard_of_mortality(sk2,sk5)=hazard_of_mortality(sk2,sk4)|sQ0_spl),
% 0.14/0.44 inference(resolution,[status(thm)],[f60,f40])).
% 0.14/0.44 fof(f201,definition,(
% 0.14/0.44 sQ24_spl <=> (smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f204,definition,(
% 0.14/0.44 sQ25_spl <=> (hazard_of_mortality(sk2,sk5)=hazard_of_mortality(sk2,sk4))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f205,plain,(
% 0.14/0.44 hazard_of_mortality(sk2,sk5)=hazard_of_mortality(sk2,sk4)|~sQ25_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f204])).
% 0.14/0.44 fof(f207,plain,(
% 0.14/0.44 sQ24_spl|sQ25_spl|sQ0_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f200,f201,f204,f58])).
% 0.14/0.44 fof(f222,plain,(
% 0.14/0.44 ![X0]: (greater(sigma,X0)|smaller(zero,X0)|zero=X0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f91,f40])).
% 0.14/0.44 fof(f227,plain,(
% 0.14/0.44 ~greater(sigma,eta)|~sQ2_spl),
% 0.14/0.44 inference(resolution,[status(thm)],[f71,f37])).
% 0.14/0.44 fof(f238,plain,(
% 0.14/0.44 smaller_or_equal(zero,eta)|~sQ18_spl),
% 0.14/0.44 inference(resolution,[status(thm)],[f168,f30])).
% 0.14/0.44 fof(f239,plain,(
% 0.14/0.44 $false|sQ7_spl|~sQ18_spl),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f238,f98])).
% 0.14/0.44 fof(f240,plain,(
% 0.14/0.44 sQ7_spl|~sQ18_spl),
% 0.14/0.44 inference(contradiction_clause,[status(thm)],[f239])).
% 0.14/0.44 fof(f244,plain,(
% 0.14/0.44 ![X0,X1]: (X0=X1|smaller(X1,X0)|smaller_or_equal(X0,X1))),
% 0.14/0.44 inference(resolution,[status(thm)],[f107,f30])).
% 0.14/0.44 fof(f254,plain,(
% 0.14/0.44 ~greater(eta,sigma)|~sQ19_spl),
% 0.14/0.44 inference(backward_demodulation,[status(thm)],[f171,f89])).
% 0.14/0.44 fof(f260,plain,(
% 0.14/0.44 $false|~sQ2_spl|~sQ19_spl),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f254,f71])).
% 0.14/0.44 fof(f261,plain,(
% 0.14/0.44 ~sQ2_spl|~sQ19_spl),
% 0.14/0.44 inference(contradiction_clause,[status(thm)],[f260])).
% 0.14/0.44 fof(f284,plain,(
% 0.14/0.44 smaller(eta,age(sk2,sk5))|eta=age(sk2,sk5)),
% 0.14/0.44 inference(resolution,[status(thm)],[f177,f40])).
% 0.14/0.44 fof(f285,definition,(
% 0.14/0.44 sQ26_spl <=> (smaller(eta,age(sk2,sk5)))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f288,definition,(
% 0.14/0.44 sQ27_spl <=> (eta=age(sk2,sk5))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f289,plain,(
% 0.14/0.44 eta=age(sk2,sk5)|~sQ27_spl),
% 0.14/0.44 inference(component_clause,[status(thm)],[f288])).
% 0.14/0.44 fof(f291,plain,(
% 0.14/0.44 sQ26_spl|sQ27_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f284,f285,f288])).
% 0.14/0.44 fof(f292,plain,(
% 0.14/0.44 greater(age(sk2,sk5),eta)|age(sk2,sk5)=eta),
% 0.14/0.44 inference(resolution,[status(thm)],[f178,f32])).
% 0.14/0.44 fof(f293,definition,(
% 0.14/0.44 sQ28_spl <=> (greater(age(sk2,sk5),eta))),
% 0.14/0.44 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.44 fof(f296,plain,(
% 0.14/0.44 sQ28_spl|sQ27_spl),
% 0.14/0.44 inference(split_clause,[status(thm)],[f292,f293,f288])).
% 0.14/0.44 fof(f364,definition,(
% 0.14/0.44 sQ36_spl <=> (smaller(eta,eta))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f365,plain,(
% 0.14/0.45 smaller(eta,eta)|~sQ36_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f364])).
% 0.14/0.45 fof(f366,plain,(
% 0.14/0.45 ~smaller(eta,eta)|sQ36_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f364])).
% 0.14/0.45 fof(f367,definition,(
% 0.14/0.45 sQ37_spl <=> (eta=eta)),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f389,plain,(
% 0.14/0.45 greater(eta,zero)|~sQ3_spl),
% 0.14/0.45 inference(backward_demodulation,[status(thm)],[f74,f56])).
% 0.14/0.45 fof(f396,plain,(
% 0.14/0.45 greater(eta,eta)|~sQ36_spl),
% 0.14/0.45 inference(resolution,[status(thm)],[f365,f35])).
% 0.14/0.45 fof(f400,plain,(
% 0.14/0.45 smaller(zero,eta)|~sQ3_spl),
% 0.14/0.45 inference(resolution,[status(thm)],[f389,f36])).
% 0.14/0.45 fof(f426,plain,(
% 0.14/0.45 ![X0]: (~organization(sk2)|has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk3))|~sQ8_spl)),
% 0.14/0.45 inference(resolution,[status(thm)],[f100,f49])).
% 0.14/0.45 fof(f435,definition,(
% 0.14/0.45 ![X0]: (sQ41_spl <=> (has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk3))))),
% 0.14/0.46 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/0.46 fof(f436,plain,(
% 0.14/0.46 ![X0]: (has_immunity(sk2,X0)|greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk3))|~sQ41_spl)),
% 0.14/0.46 inference(component_clause,[status(thm)],[f435])).
% 0.14/0.46 fof(f438,plain,(
% 0.14/0.46 ~sQ21_spl|sQ41_spl|~sQ8_spl),
% 0.14/0.46 inference(split_clause,[status(thm)],[f426,f185,f435,f99])).
% 0.14/0.46 fof(f473,plain,(
% 0.14/0.46 ~greater(eta,eta)|~sQ36_spl),
% 0.14/0.46 inference(resolution,[status(thm)],[f396,f37])).
% 0.14/0.46 fof(f475,plain,(
% 0.14/0.46 $false|~sQ36_spl),
% 0.14/0.46 inference(forward_subsumption_resolution,[status(thm)],[f473,f396])).
% 0.14/0.46 fof(f476,plain,(
% 0.14/0.46 ~sQ36_spl),
% 0.14/0.46 inference(contradiction_clause,[status(thm)],[f475])).
% 0.14/0.46 fof(f484,plain,(
% 0.14/0.46 has_immunity(sk2,sk5)|greater(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk4))|~sQ22_spl|~sQ25_spl),
% 0.14/0.46 inference(paramodulation,[status(thm)],[f205,f189])).
% 0.14/0.46 fof(f485,definition,(
% 0.14/0.46 sQ43_spl <=> (greater(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk4)))),
% 0.14/0.46 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.46 fof(f488,plain,(
% 0.14/0.46 sQ20_spl|sQ43_spl|~sQ22_spl|~sQ25_spl),
% 0.14/0.46 inference(split_clause,[status(thm)],[f484,f179,f485,f188,f204])).
% 0.14/0.46 fof(f495,plain,(
% 0.14/0.46 hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,sk3)|~sQ23_spl|~sQ8_spl),
% 0.14/0.46 inference(resolution,[status(thm)],[f193,f100])).
% 0.14/0.46 fof(f498,plain,(
% 0.14/0.46 $false|sQ1_spl|~sQ23_spl|~sQ8_spl),
% 0.14/0.46 inference(forward_subsumption_resolution,[status(thm)],[f495,f63])).
% 0.14/0.46 fof(f499,plain,(
% 0.14/0.46 sQ1_spl|~sQ23_spl|~sQ8_spl),
% 0.14/0.46 inference(contradiction_clause,[status(thm)],[f498])).
% 0.14/0.46 fof(f503,plain,(
% 0.14/0.46 ~greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk3))|~sQ1_spl|sQ0_spl),
% 0.14/0.46 inference(forward_demodulation,[status(thm)],[f62,f60])).
% 0.14/0.46 fof(f516,plain,(
% 0.14/0.46 smaller(zero,eta)|zero=eta|~sQ2_spl),
% 0.14/0.46 inference(resolution,[status(thm)],[f222,f227])).
% 0.14/0.46 fof(f522,plain,(
% 0.14/0.46 sQ18_spl|sQ19_spl|~sQ2_spl),
% 0.14/0.46 inference(split_clause,[status(thm)],[f516,f167,f170,f70])).
% 0.14/0.46 fof(f559,plain,(
% 0.14/0.46 sQ18_spl|~sQ3_spl),
% 0.14/0.46 inference(split_clause,[status(thm)],[f400,f167,f73])).
% 0.14/0.46 fof(f601,plain,(
% 0.14/0.46 smaller(eta,eta)|eta=eta|sQ36_spl),
% 0.14/0.46 inference(resolution,[status(thm)],[f366,f107])).
% 0.14/0.46 fof(f604,plain,(
% 0.14/0.46 sQ36_spl|sQ37_spl),
% 0.14/0.46 inference(split_clause,[status(thm)],[f601,f364,f367])).
% 0.14/0.46 fof(f642,plain,(
% 0.14/0.46 smaller(eta,eta)|~sQ27_spl),
% 0.14/0.46 inference(backward_demodulation,[status(thm)],[f289,f175])).
% 0.14/0.46 fof(f646,plain,(
% 0.14/0.46 sQ36_spl|~sQ27_spl),
% 0.14/0.46 inference(split_clause,[status(thm)],[f642,f364,f288])).
% 0.14/0.46 fof(f669,plain,(
% 0.14/0.46 ![X0,X1]: (X0=X1|smaller_or_equal(X0,X1)|greater(X0,X1))),
% 0.14/0.46 inference(resolution,[status(thm)],[f244,f35])).
% 0.14/0.46 fof(f760,plain,(
% 0.14/0.46 eta=age(sk2,sk5)|smaller_or_equal(eta,age(sk2,sk5))),
% 0.14/0.46 inference(resolution,[status(thm)],[f669,f177])).
% 0.14/0.46 fof(f775,definition,(
% 0.14/0.46 sQ53_spl <=> (smaller_or_equal(eta,age(sk2,sk5)))),
% 0.14/0.46 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/0.46 fof(f778,plain,(
% 0.14/0.46 sQ27_spl|sQ53_spl),
% 0.14/0.46 inference(split_clause,[status(thm)],[f760,f288,f775])).
% 0.14/0.46 fof(f984,plain,(
% 0.14/0.46 has_immunity(sk2,sk5)|~sQ41_spl|~sQ1_spl|sQ0_spl),
% 0.14/0.46 inference(resolution,[status(thm)],[f436,f503])).
% 0.14/0.46 fof(f991,plain,(
% 0.14/0.46 $false|sQ20_spl|~sQ41_spl|~sQ1_spl|sQ0_spl),
% 0.14/0.46 inference(forward_subsumption_resolution,[status(thm)],[f984,f181])).
% 0.14/0.46 fof(f992,plain,(
% 0.14/0.46 sQ20_spl|~sQ41_spl|~sQ1_spl|sQ0_spl),
% 0.14/0.46 inference(contradiction_clause,[status(thm)],[f991])).
% 0.14/0.46 fof(f993,plain,(
% 0.14/0.46 $false),
% 0.14/0.46 inference(sat_refutation,[status(thm)],[f64,f76,f102,f126,f136,f182,f191,f195,f197,f207,f240,f261,f291,f296,f438,f476,f488,f499,f522,f559,f604,f646,f778,f992])).
% 0.14/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.46 % Elapsed time: 0.096380 seconds
% 0.14/0.46 % CPU time: 0.552610 seconds
% 0.14/0.46 % Total memory used: 92.995 MB
% 0.14/0.46 % Net memory used: 91.925 MB
%------------------------------------------------------------------------------