%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT064-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:25:52 PM UTC 2026
% Result : Unsatisfiable 53.13s 7.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT064-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n008.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 01:25:24 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.48 % Drodi V4.1.1
% 53.13/7.65 % Refutation found
% 53.13/7.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 53.13/7.65 % SZS output start CNFRefutation for theBenchmark
% 53.13/7.65 fof(f1,axiom,(
% 53.13/7.65 (![A,B]: (( ~ smaller_or_equal(A,B)| smaller(A,B)| A = B ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f2,axiom,(
% 53.13/7.65 (![A,B]: (( ~ smaller(A,B)| smaller_or_equal(A,B) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f4,axiom,(
% 53.13/7.65 (![A,B]: (( ~ greater_or_equal(A,B)| greater(A,B)| A = B ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f5,axiom,(
% 53.13/7.65 (![A,B]: (( ~ greater(A,B)| greater_or_equal(A,B) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f7,axiom,(
% 53.13/7.65 (![A,B]: (( ~ smaller(A,B)| greater(B,A) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f8,axiom,(
% 53.13/7.65 (![A,B]: (( ~ greater(A,B)| smaller(B,A) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f9,axiom,(
% 53.13/7.65 (![A,B]: (( ~ greater(A,B)| ~ greater(B,A) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f10,axiom,(
% 53.13/7.65 (![A,B,C]: (( ~ greater(A,B)| ~ greater(B,C)| greater(A,C) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f11,axiom,(
% 53.13/7.65 (![A,B]: (( smaller(A,B)| A = B| greater(A,B) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f19,axiom,(
% 53.13/7.65 (![A,B]: (( ~ organization(A)| has_endowment(A)| ~ has_immunity(A,B) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f20,axiom,(
% 53.13/7.65 (![A,B,C]: (( ~ dissimilar(A,B,C)| organization(A) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f22,axiom,(
% 53.13/7.65 (![A,B,C]: (( ~ dissimilar(A,B,C)| ~ is_aligned(A,B)| ~ is_aligned(A,C) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f24,axiom,(
% 53.13/7.65 (![A,B,C]: (( ~ organization(A)| ~ is_aligned(A,B)| is_aligned(A,C)| dissimilar(A,B,C) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f25,axiom,(
% 53.13/7.65 (![A,B,C]: (( ~ organization(A)| ~ is_aligned(A,B)| is_aligned(A,C)| dissimilar(A,C,B) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f27,axiom,(
% 53.13/7.65 (![A,B]: (( ~ organization(A)| age(A,B) != zero| is_aligned(A,B) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f28,axiom,(
% 53.13/7.65 (![A,B,C]: (( ~ organization(A)| age(A,B) != zero| ~ greater(age(A,C),sigma)| dissimilar(A,B,C) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f29,axiom,(
% 53.13/7.65 (![A,B,C]: (( ~ organization(A)| age(A,B) != zero| ~ dissimilar(A,B,C)| greater(age(A,C),sigma) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f30,axiom,(
% 53.13/7.65 (![A,B]: (( ~ robust_position(A)| ~ smaller_or_equal(age(A,B),tau)| ~ positional_advantage(A,B) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f31,axiom,(
% 53.13/7.65 (![A,B]: (( ~ robust_position(A)| ~ greater(age(A,B),tau)| positional_advantage(A,B) ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f37,axiom,(
% 53.13/7.65 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| ~ is_aligned(A,B)| ~ positional_advantage(A,B)| hazard_of_mortality(A,B) = low ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f38,axiom,(
% 53.13/7.65 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| is_aligned(A,B)| ~ positional_advantage(A,B)| hazard_of_mortality(A,B) = mod1 ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f39,axiom,(
% 53.13/7.65 (![A,B]: (( ~ organization(A)| has_immunity(A,B)| ~ is_aligned(A,B)| positional_advantage(A,B)| hazard_of_mortality(A,B) = mod2 ) ))),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f42,axiom,(
% 53.13/7.65 greater(mod1,low) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f46,axiom,(
% 53.13/7.65 greater(mod2,mod1) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f47,negated_conjecture,(
% 53.13/7.65 organization(sk3) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f48,negated_conjecture,(
% 53.13/7.65 robust_position(sk3) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f49,negated_conjecture,(
% 53.13/7.65 ~ has_endowment(sk3) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f50,negated_conjecture,(
% 53.13/7.65 age(sk3,sk4) = zero ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f51,negated_conjecture,(
% 53.13/7.65 greater(sigma,zero) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f52,negated_conjecture,(
% 53.13/7.65 greater(tau,zero) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f53,negated_conjecture,(
% 53.13/7.65 greater(sigma,tau) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f54,negated_conjecture,(
% 53.13/7.65 smaller_or_equal(age(sk3,sk5),tau) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f55,negated_conjecture,(
% 53.13/7.65 greater(age(sk3,sk6),tau) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f56,negated_conjecture,(
% 53.13/7.65 smaller_or_equal(age(sk3,sk6),sigma) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f57,negated_conjecture,(
% 53.13/7.65 greater(age(sk3,sk7),sigma) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f58,negated_conjecture,(
% 53.13/7.65 ( ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))| ~ smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))| hazard_of_mortality(sk3,sk5) != hazard_of_mortality(sk3,sk4) ) ),
% 53.13/7.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.13/7.65 fof(f59,plain,(
% 53.13/7.65 ![X0,X1]: (~smaller_or_equal(X0,X1)|smaller(X0,X1)|X0=X1)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f1])).
% 53.13/7.65 fof(f60,plain,(
% 53.13/7.65 ![X0,X1]: (~smaller(X0,X1)|smaller_or_equal(X0,X1))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f2])).
% 53.13/7.65 fof(f62,plain,(
% 53.13/7.65 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f4])).
% 53.13/7.65 fof(f63,plain,(
% 53.13/7.65 ![X0,X1]: (~greater(X0,X1)|greater_or_equal(X0,X1))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f5])).
% 53.13/7.65 fof(f65,plain,(
% 53.13/7.65 ![X0,X1]: (~smaller(X0,X1)|greater(X1,X0))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f7])).
% 53.13/7.65 fof(f66,plain,(
% 53.13/7.65 ![X0,X1]: (~greater(X0,X1)|smaller(X1,X0))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f8])).
% 53.13/7.65 fof(f67,plain,(
% 53.13/7.65 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f9])).
% 53.13/7.65 fof(f68,plain,(
% 53.13/7.65 ![A,C]: ((![B]: (~greater(A,B)|~greater(B,C)))|greater(A,C))),
% 53.13/7.65 inference(miniscoping,[status(thm)],[f10])).
% 53.13/7.65 fof(f69,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f68])).
% 53.13/7.65 fof(f70,plain,(
% 53.13/7.65 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater(X0,X1))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f11])).
% 53.13/7.65 fof(f78,plain,(
% 53.13/7.65 ![A]: ((~organization(A)|has_endowment(A))|(![B]: ~has_immunity(A,B)))),
% 53.13/7.65 inference(miniscoping,[status(thm)],[f19])).
% 53.13/7.65 fof(f79,plain,(
% 53.13/7.65 ![X0,X1]: (~organization(X0)|has_endowment(X0)|~has_immunity(X0,X1))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f78])).
% 53.13/7.65 fof(f80,plain,(
% 53.13/7.65 ![A]: ((![B,C]: ~dissimilar(A,B,C))|organization(A))),
% 53.13/7.65 inference(miniscoping,[status(thm)],[f20])).
% 53.13/7.65 fof(f81,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|organization(X0))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f80])).
% 53.13/7.65 fof(f84,plain,(
% 53.13/7.65 ![A,C]: ((![B]: (~dissimilar(A,B,C)|~is_aligned(A,B)))|~is_aligned(A,C))),
% 53.13/7.65 inference(miniscoping,[status(thm)],[f22])).
% 53.13/7.65 fof(f85,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f84])).
% 53.13/7.65 fof(f88,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2)|dissimilar(X0,X1,X2))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f24])).
% 53.13/7.65 fof(f89,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2)|dissimilar(X0,X2,X1))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f25])).
% 53.13/7.65 fof(f92,plain,(
% 53.13/7.65 ![X0,X1]: (~organization(X0)|~age(X0,X1)=zero|is_aligned(X0,X1))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f27])).
% 53.13/7.65 fof(f93,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~greater(age(X0,X2),sigma)|dissimilar(X0,X1,X2))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f28])).
% 53.13/7.65 fof(f94,plain,(
% 53.13/7.65 ![A,C]: ((![B]: ((~organization(A)|~age(A,B)=zero)|~dissimilar(A,B,C)))|greater(age(A,C),sigma))),
% 53.13/7.65 inference(miniscoping,[status(thm)],[f29])).
% 53.13/7.65 fof(f95,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~dissimilar(X0,X1,X2)|greater(age(X0,X2),sigma))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f94])).
% 53.13/7.65 fof(f96,plain,(
% 53.13/7.65 ![X0,X1]: (~robust_position(X0)|~smaller_or_equal(age(X0,X1),tau)|~positional_advantage(X0,X1))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f30])).
% 53.13/7.65 fof(f97,plain,(
% 53.13/7.65 ![X0,X1]: (~robust_position(X0)|~greater(age(X0,X1),tau)|positional_advantage(X0,X1))),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f31])).
% 53.13/7.65 fof(f103,plain,(
% 53.13/7.65 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=low)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f37])).
% 53.13/7.65 fof(f104,plain,(
% 53.13/7.65 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod1)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f38])).
% 53.13/7.65 fof(f105,plain,(
% 53.13/7.65 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f39])).
% 53.13/7.65 fof(f108,plain,(
% 53.13/7.65 greater(mod1,low)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f42])).
% 53.13/7.65 fof(f112,plain,(
% 53.13/7.65 greater(mod2,mod1)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f46])).
% 53.13/7.65 fof(f113,plain,(
% 53.13/7.65 organization(sk3)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f47])).
% 53.13/7.65 fof(f114,plain,(
% 53.13/7.65 robust_position(sk3)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f48])).
% 53.13/7.65 fof(f115,plain,(
% 53.13/7.65 ~has_endowment(sk3)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f49])).
% 53.13/7.65 fof(f116,plain,(
% 53.13/7.65 age(sk3,sk4)=zero),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f50])).
% 53.13/7.65 fof(f117,plain,(
% 53.13/7.65 greater(sigma,zero)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f51])).
% 53.13/7.65 fof(f118,plain,(
% 53.13/7.65 greater(tau,zero)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f52])).
% 53.13/7.65 fof(f119,plain,(
% 53.13/7.65 greater(sigma,tau)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f53])).
% 53.13/7.65 fof(f120,plain,(
% 53.13/7.65 smaller_or_equal(age(sk3,sk5),tau)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f54])).
% 53.13/7.65 fof(f121,plain,(
% 53.13/7.65 greater(age(sk3,sk6),tau)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f55])).
% 53.13/7.65 fof(f122,plain,(
% 53.13/7.65 smaller_or_equal(age(sk3,sk6),sigma)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f56])).
% 53.13/7.65 fof(f123,plain,(
% 53.13/7.65 greater(age(sk3,sk7),sigma)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f57])).
% 53.13/7.65 fof(f124,plain,(
% 53.13/7.65 ~smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))|~smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))|~hazard_of_mortality(sk3,sk5)=hazard_of_mortality(sk3,sk4)),
% 53.13/7.65 inference(cnf_transformation,[status(thm)],[f58])).
% 53.13/7.65 fof(f125,definition,(
% 53.13/7.65 sQ0_spl <=> (smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f127,plain,(
% 53.13/7.65 ~smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))|sQ0_spl),
% 53.13/7.65 inference(component_clause,[status(thm)],[f125])).
% 53.13/7.65 fof(f128,definition,(
% 53.13/7.65 sQ1_spl <=> (smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f130,plain,(
% 53.13/7.65 ~smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))|sQ1_spl),
% 53.13/7.65 inference(component_clause,[status(thm)],[f128])).
% 53.13/7.65 fof(f131,definition,(
% 53.13/7.65 sQ2_spl <=> (hazard_of_mortality(sk3,sk5)=hazard_of_mortality(sk3,sk4))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f133,plain,(
% 53.13/7.65 ~hazard_of_mortality(sk3,sk5)=hazard_of_mortality(sk3,sk4)|sQ2_spl),
% 53.13/7.65 inference(component_clause,[status(thm)],[f131])).
% 53.13/7.65 fof(f134,plain,(
% 53.13/7.65 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 53.13/7.65 inference(split_clause,[status(thm)],[f124,f125,f128,f131])).
% 53.13/7.65 fof(f138,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~age(X0,X1)=zero|~dissimilar(X0,X1,X2)|greater(age(X0,X2),sigma))),
% 53.13/7.65 inference(forward_subsumption_resolution,[status(thm)],[f95,f81])).
% 53.13/7.65 fof(f139,plain,(
% 53.13/7.65 smaller(zero,tau)),
% 53.13/7.65 inference(resolution,[status(thm)],[f66,f118])).
% 53.13/7.65 fof(f146,plain,(
% 53.13/7.65 ~greater(tau,sigma)),
% 53.13/7.65 inference(resolution,[status(thm)],[f67,f119])).
% 53.13/7.65 fof(f147,plain,(
% 53.13/7.65 ~greater(zero,sigma)),
% 53.13/7.65 inference(resolution,[status(thm)],[f67,f117])).
% 53.13/7.65 fof(f148,plain,(
% 53.13/7.65 ![X0,X1]: (~greater(X0,X1)|~smaller(X0,X1))),
% 53.13/7.65 inference(resolution,[status(thm)],[f67,f65])).
% 53.13/7.65 fof(f152,plain,(
% 53.13/7.65 smaller(low,mod1)),
% 53.13/7.65 inference(resolution,[status(thm)],[f108,f66])).
% 53.13/7.65 fof(f160,plain,(
% 53.13/7.65 smaller(mod1,mod2)),
% 53.13/7.65 inference(resolution,[status(thm)],[f112,f66])).
% 53.13/7.65 fof(f162,plain,(
% 53.13/7.65 ~smaller(sigma,tau)),
% 53.13/7.65 inference(resolution,[status(thm)],[f146,f65])).
% 53.13/7.65 fof(f175,plain,(
% 53.13/7.65 ![X0]: (~greater(tau,X0)|~greater(X0,sigma))),
% 53.13/7.65 inference(resolution,[status(thm)],[f69,f146])).
% 53.13/7.65 fof(f179,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|~greater(X2,X0))),
% 53.13/7.65 inference(resolution,[status(thm)],[f69,f67])).
% 53.13/7.65 fof(f210,plain,(
% 53.13/7.65 smaller(age(sk3,sk6),sigma)|age(sk3,sk6)=sigma),
% 53.13/7.65 inference(resolution,[status(thm)],[f122,f59])).
% 53.13/7.65 fof(f211,definition,(
% 53.13/7.65 sQ5_spl <=> (smaller(age(sk3,sk6),sigma))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f212,plain,(
% 53.13/7.65 smaller(age(sk3,sk6),sigma)|~sQ5_spl),
% 53.13/7.65 inference(component_clause,[status(thm)],[f211])).
% 53.13/7.65 fof(f214,definition,(
% 53.13/7.65 sQ6_spl <=> (age(sk3,sk6)=sigma)),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f215,plain,(
% 53.13/7.65 age(sk3,sk6)=sigma|~sQ6_spl),
% 53.13/7.65 inference(component_clause,[status(thm)],[f214])).
% 53.13/7.65 fof(f217,plain,(
% 53.13/7.65 sQ5_spl|sQ6_spl),
% 53.13/7.65 inference(split_clause,[status(thm)],[f210,f211,f214])).
% 53.13/7.65 fof(f234,plain,(
% 53.13/7.65 ![X0,X1]: (smaller(X0,X1)|X0=X1|greater_or_equal(X0,X1))),
% 53.13/7.65 inference(resolution,[status(thm)],[f70,f63])).
% 53.13/7.65 fof(f386,definition,(
% 53.13/7.65 sQ19_spl <=> (sigma=tau)),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f387,plain,(
% 53.13/7.65 sigma=tau|~sQ19_spl),
% 53.13/7.65 inference(component_clause,[status(thm)],[f386])).
% 53.13/7.65 fof(f398,plain,(
% 53.13/7.65 ~greater(sigma,sigma)|~sQ19_spl),
% 53.13/7.65 inference(backward_demodulation,[status(thm)],[f387,f146])).
% 53.13/7.65 fof(f400,plain,(
% 53.13/7.65 greater(sigma,sigma)|~sQ19_spl),
% 53.13/7.65 inference(backward_demodulation,[status(thm)],[f387,f119])).
% 53.13/7.65 fof(f475,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~organization(X0)|is_aligned(X0,X1)|dissimilar(X0,X2,X1)|~organization(X0)|~age(X0,X2)=zero)),
% 53.13/7.65 inference(resolution,[status(thm)],[f88,f92])).
% 53.13/7.65 fof(f476,plain,(
% 53.13/7.65 ![X0,X1,X2]: (~organization(X0)|is_aligned(X0,X1)|dissimilar(X0,X2,X1)|~age(X0,X2)=zero)),
% 53.13/7.65 inference(duplicate_literals_removal,[status(thm)],[f475])).
% 53.13/7.65 fof(f487,plain,(
% 53.13/7.65 ~greater(sigma,age(sk3,sk7))),
% 53.13/7.65 inference(resolution,[status(thm)],[f123,f67])).
% 53.13/7.65 fof(f502,plain,(
% 53.13/7.65 ![X0,X1]: (~age(sk3,X0)=zero|~greater(age(sk3,X1),sigma)|dissimilar(sk3,X0,X1))),
% 53.13/7.65 inference(resolution,[status(thm)],[f93,f113])).
% 53.13/7.65 fof(f591,plain,(
% 53.13/7.65 ![X0]: (~greater(age(sk3,X0),tau)|positional_advantage(sk3,X0))),
% 53.13/7.65 inference(resolution,[status(thm)],[f97,f114])).
% 53.13/7.65 fof(f614,plain,(
% 53.13/7.65 ~greater(age(sk3,sk6),sigma)|~sQ5_spl),
% 53.13/7.65 inference(resolution,[status(thm)],[f148,f212])).
% 53.13/7.65 fof(f710,plain,(
% 53.13/7.65 $false|~sQ19_spl),
% 53.13/7.65 inference(forward_subsumption_resolution,[status(thm)],[f400,f398])).
% 53.13/7.65 fof(f711,plain,(
% 53.13/7.65 ~sQ19_spl),
% 53.13/7.65 inference(contradiction_clause,[status(thm)],[f710])).
% 53.13/7.65 fof(f843,plain,(
% 53.13/7.65 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2|~organization(X0)|~age(X0,X1)=zero)),
% 53.13/7.65 inference(resolution,[status(thm)],[f105,f92])).
% 53.13/7.65 fof(f844,plain,(
% 53.13/7.65 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=mod2|~age(X0,X1)=zero)),
% 53.13/7.65 inference(duplicate_literals_removal,[status(thm)],[f843])).
% 53.13/7.65 fof(f851,plain,(
% 53.13/7.65 ![X0]: (~greater(X0,sigma)|~smaller(X0,tau))),
% 53.13/7.65 inference(resolution,[status(thm)],[f175,f65])).
% 53.13/7.65 fof(f923,plain,(
% 53.13/7.65 ![X0,X1,X2,X3]: (~greater(X0,X1)|~greater(X2,X0)|~greater(X1,X3)|~greater(X3,X2))),
% 53.13/7.65 inference(resolution,[status(thm)],[f179,f69])).
% 53.13/7.65 fof(f941,plain,(
% 53.13/7.65 ![X0]: (~greater(X0,X0)|~greater(X0,X0))),
% 53.13/7.65 inference(factoring,[status(thm)],[f179])).
% 53.13/7.65 fof(f942,plain,(
% 53.13/7.65 ![X0]: (~greater(X0,X0))),
% 53.13/7.65 inference(duplicate_literals_removal,[status(thm)],[f941])).
% 53.13/7.65 fof(f1040,definition,(
% 53.13/7.65 sQ54_spl <=> (greater(zero,sigma))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1165,plain,(
% 53.13/7.65 ![X0,X1]: (is_aligned(sk3,X0)|dissimilar(sk3,X1,X0)|~age(sk3,X1)=zero)),
% 53.13/7.65 inference(resolution,[status(thm)],[f476,f113])).
% 53.13/7.65 fof(f1168,plain,(
% 53.13/7.65 ![X0,X1]: (~age(sk3,X0)=zero|~greater(age(sk3,X1),sigma)|~is_aligned(sk3,X0)|~is_aligned(sk3,X1))),
% 53.13/7.65 inference(resolution,[status(thm)],[f502,f85])).
% 53.13/7.65 fof(f1170,plain,(
% 53.13/7.65 ![X0,X1]: (~age(sk3,X0)=zero|~greater(age(sk3,X1),sigma)|organization(sk3))),
% 53.13/7.65 inference(resolution,[status(thm)],[f502,f81])).
% 53.13/7.65 fof(f1171,definition,(
% 53.13/7.65 ![X0]: (sQ60_spl <=> (~age(sk3,X0)=zero|~age(sk3,X0)=zero))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1172,plain,(
% 53.13/7.65 ![X0]: (~age(sk3,X0)=zero|~age(sk3,X0)=zero|~sQ60_spl)),
% 53.13/7.65 inference(component_clause,[status(thm)],[f1171])).
% 53.13/7.65 fof(f1178,definition,(
% 53.13/7.65 ![X0]: (sQ62_spl <=> (~age(sk3,X0)=zero|~is_aligned(sk3,X0)))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1179,plain,(
% 53.13/7.65 ![X0]: (~age(sk3,X0)=zero|~is_aligned(sk3,X0)|~sQ62_spl)),
% 53.13/7.65 inference(component_clause,[status(thm)],[f1178])).
% 53.13/7.65 fof(f1181,definition,(
% 53.13/7.65 ![X1]: (sQ63_spl <=> (~greater(age(sk3,X1),sigma)|~is_aligned(sk3,X1)))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1182,plain,(
% 53.13/7.65 ![X0]: (~greater(age(sk3,X0),sigma)|~is_aligned(sk3,X0)|~sQ63_spl)),
% 53.13/7.65 inference(component_clause,[status(thm)],[f1181])).
% 53.13/7.65 fof(f1184,plain,(
% 53.13/7.65 sQ62_spl|sQ63_spl),
% 53.13/7.65 inference(split_clause,[status(thm)],[f1168,f1178,f1181])).
% 53.13/7.65 fof(f1185,definition,(
% 53.13/7.65 ![X0]: (sQ64_spl <=> (~age(sk3,X0)=zero|is_aligned(sk3,X0)))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1186,plain,(
% 53.13/7.65 ![X0]: (~age(sk3,X0)=zero|is_aligned(sk3,X0)|~sQ64_spl)),
% 53.13/7.65 inference(component_clause,[status(thm)],[f1185])).
% 53.13/7.65 fof(f1192,definition,(
% 53.13/7.65 ![X0]: (sQ66_spl <=> (~age(sk3,X0)=zero))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1193,plain,(
% 53.13/7.65 ![X0]: (~age(sk3,X0)=zero|~sQ66_spl)),
% 53.13/7.65 inference(component_clause,[status(thm)],[f1192])).
% 53.13/7.65 fof(f1195,definition,(
% 53.13/7.65 ![X1]: (sQ67_spl <=> (~greater(age(sk3,X1),sigma)))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1196,plain,(
% 53.13/7.65 ![X0]: (~greater(age(sk3,X0),sigma)|~sQ67_spl)),
% 53.13/7.65 inference(component_clause,[status(thm)],[f1195])).
% 53.13/7.65 fof(f1198,definition,(
% 53.13/7.65 sQ68_spl <=> (organization(sk3))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1201,plain,(
% 53.13/7.65 sQ66_spl|sQ67_spl|sQ68_spl),
% 53.13/7.65 inference(split_clause,[status(thm)],[f1170,f1192,f1195,f1198])).
% 53.13/7.65 fof(f1202,plain,(
% 53.13/7.65 $false|~sQ64_spl|~sQ62_spl),
% 53.13/7.65 inference(backward_subsumption_resolution,[status(thm)],[f116,f1203])).
% 53.13/7.65 fof(f1203,plain,(
% 53.13/7.65 ![X0]: (~age(sk3,X0)=zero|~sQ64_spl|~sQ62_spl)),
% 53.13/7.65 inference(forward_subsumption_resolution,[status(thm)],[f1179,f1186])).
% 53.13/7.65 fof(f1204,plain,(
% 53.13/7.65 ![X0]: (~age(sk3,X0)=zero|~sQ60_spl)),
% 53.13/7.65 inference(duplicate_literals_removal,[status(thm)],[f1172])).
% 53.13/7.65 fof(f1205,plain,(
% 53.13/7.65 $false|~sQ67_spl),
% 53.13/7.65 inference(backward_subsumption_resolution,[status(thm)],[f123,f1196])).
% 53.13/7.65 fof(f1206,plain,(
% 53.13/7.65 ~sQ64_spl|~sQ62_spl),
% 53.13/7.65 inference(contradiction_clause,[status(thm)],[f1202])).
% 53.13/7.65 fof(f1207,plain,(
% 53.13/7.65 ~sQ67_spl),
% 53.13/7.65 inference(contradiction_clause,[status(thm)],[f1205])).
% 53.13/7.65 fof(f1208,plain,(
% 53.13/7.65 $false|~sQ66_spl),
% 53.13/7.65 inference(backward_subsumption_resolution,[status(thm)],[f116,f1193])).
% 53.13/7.65 fof(f1211,plain,(
% 53.13/7.65 ~sQ66_spl),
% 53.13/7.65 inference(contradiction_clause,[status(thm)],[f1208])).
% 53.13/7.65 fof(f1213,plain,(
% 53.13/7.65 sQ66_spl|~sQ60_spl),
% 53.13/7.65 inference(split_clause,[status(thm)],[f1204,f1192,f1171])).
% 53.13/7.65 fof(f1230,plain,(
% 53.13/7.65 ~smaller(age(sk3,sk7),tau)),
% 53.13/7.65 inference(resolution,[status(thm)],[f123,f851])).
% 53.13/7.65 fof(f1438,plain,(
% 53.13/7.65 positional_advantage(sk3,sk6)),
% 53.13/7.65 inference(resolution,[status(thm)],[f591,f121])).
% 53.13/7.65 fof(f1442,plain,(
% 53.13/7.65 ![X0,X1]: (positional_advantage(sk3,X0)|~greater(age(sk3,X0),X1)|~greater(X1,tau))),
% 53.13/7.65 inference(resolution,[status(thm)],[f591,f69])).
% 53.13/7.65 fof(f1448,definition,(
% 53.13/7.65 sQ81_spl <=> (robust_position(sk3))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1450,plain,(
% 53.13/7.65 ~robust_position(sk3)|sQ81_spl),
% 53.13/7.65 inference(component_clause,[status(thm)],[f1448])).
% 53.13/7.65 fof(f1456,definition,(
% 53.13/7.65 sQ83_spl <=> (positional_advantage(sk3,sk4))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 53.13/7.65 fof(f1457,plain,(
% 53.13/7.65 positional_advantage(sk3,sk4)|~sQ83_spl),
% 53.13/7.65 inference(component_clause,[status(thm)],[f1456])).
% 53.13/7.65 fof(f1466,plain,(
% 53.13/7.65 ~organization(sk3)|has_immunity(sk3,sk6)|~is_aligned(sk3,sk6)|hazard_of_mortality(sk3,sk6)=low),
% 53.13/7.65 inference(resolution,[status(thm)],[f1438,f103])).
% 53.13/7.65 fof(f1469,definition,(
% 53.13/7.65 sQ84_spl <=> (has_immunity(sk3,sk6))),
% 53.13/7.65 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1470,plain,(
% 53.13/7.66 has_immunity(sk3,sk6)|~sQ84_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1469])).
% 53.13/7.66 fof(f1472,definition,(
% 53.13/7.66 sQ85_spl <=> (is_aligned(sk3,sk6))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1475,definition,(
% 53.13/7.66 sQ86_spl <=> (hazard_of_mortality(sk3,sk6)=low)),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1476,plain,(
% 53.13/7.66 hazard_of_mortality(sk3,sk6)=low|~sQ86_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1475])).
% 53.13/7.66 fof(f1478,plain,(
% 53.13/7.66 ~sQ68_spl|sQ84_spl|~sQ85_spl|sQ86_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f1466,f1198,f1469,f1472,f1475])).
% 53.13/7.66 fof(f1491,plain,(
% 53.13/7.66 ~robust_position(sk3)|~smaller_or_equal(age(sk3,sk4),tau)|~sQ83_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f1457,f96])).
% 53.13/7.66 fof(f1492,definition,(
% 53.13/7.66 sQ89_spl <=> (has_immunity(sk3,sk4))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1493,plain,(
% 53.13/7.66 has_immunity(sk3,sk4)|~sQ89_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1492])).
% 53.13/7.66 fof(f1494,plain,(
% 53.13/7.66 ~has_immunity(sk3,sk4)|sQ89_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1492])).
% 53.13/7.66 fof(f1495,definition,(
% 53.13/7.66 sQ90_spl <=> (is_aligned(sk3,sk4))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1496,plain,(
% 53.13/7.66 is_aligned(sk3,sk4)|~sQ90_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1495])).
% 53.13/7.66 fof(f1506,definition,(
% 53.13/7.66 sQ93_spl <=> (smaller_or_equal(age(sk3,sk4),tau))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1508,plain,(
% 53.13/7.66 ~smaller_or_equal(age(sk3,sk4),tau)|sQ93_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1506])).
% 53.13/7.66 fof(f1509,plain,(
% 53.13/7.66 ~sQ81_spl|~sQ93_spl|~sQ83_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f1491,f1448,f1506,f1456])).
% 53.13/7.66 fof(f1510,plain,(
% 53.13/7.66 ~smaller_or_equal(zero,tau)|sQ93_spl),
% 53.13/7.66 inference(forward_demodulation,[status(thm)],[f116,f1508])).
% 53.13/7.66 fof(f1513,plain,(
% 53.13/7.66 $false|sQ81_spl),
% 53.13/7.66 inference(forward_subsumption_resolution,[status(thm)],[f1450,f114])).
% 53.13/7.66 fof(f1514,plain,(
% 53.13/7.66 sQ81_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f1513])).
% 53.13/7.66 fof(f1517,plain,(
% 53.13/7.66 ~organization(sk3)|has_endowment(sk3)|~sQ84_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f1470,f79])).
% 53.13/7.66 fof(f1522,definition,(
% 53.13/7.66 sQ95_spl <=> (has_endowment(sk3))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1523,plain,(
% 53.13/7.66 has_endowment(sk3)|~sQ95_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1522])).
% 53.13/7.66 fof(f1525,plain,(
% 53.13/7.66 ~sQ68_spl|sQ95_spl|~sQ84_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f1517,f1198,f1522,f1469])).
% 53.13/7.66 fof(f1527,plain,(
% 53.13/7.66 $false|~sQ95_spl),
% 53.13/7.66 inference(forward_subsumption_resolution,[status(thm)],[f1523,f115])).
% 53.13/7.66 fof(f1528,plain,(
% 53.13/7.66 ~sQ95_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f1527])).
% 53.13/7.66 fof(f1535,plain,(
% 53.13/7.66 ~organization(sk3)|has_endowment(sk3)|~sQ89_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f1493,f79])).
% 53.13/7.66 fof(f1540,plain,(
% 53.13/7.66 ~sQ68_spl|sQ95_spl|~sQ89_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f1535,f1198,f1522,f1492])).
% 53.13/7.66 fof(f1543,plain,(
% 53.13/7.66 ~smaller(zero,tau)|sQ93_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f1510,f60])).
% 53.13/7.66 fof(f1544,plain,(
% 53.13/7.66 $false|sQ93_spl),
% 53.13/7.66 inference(forward_subsumption_resolution,[status(thm)],[f1543,f139])).
% 53.13/7.66 fof(f1545,plain,(
% 53.13/7.66 sQ93_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f1544])).
% 53.13/7.66 fof(f1670,definition,(
% 53.13/7.66 sQ111_spl <=> (smaller(sigma,tau))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1671,plain,(
% 53.13/7.66 smaller(sigma,tau)|~sQ111_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1670])).
% 53.13/7.66 fof(f1681,plain,(
% 53.13/7.66 age(sk3,sk7)=tau|greater_or_equal(age(sk3,sk7),tau)),
% 53.13/7.66 inference(resolution,[status(thm)],[f1230,f234])).
% 53.13/7.66 fof(f1685,definition,(
% 53.13/7.66 sQ114_spl <=> (tau=age(sk3,sk7))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1686,plain,(
% 53.13/7.66 tau=age(sk3,sk7)|~sQ114_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1685])).
% 53.13/7.66 fof(f1690,definition,(
% 53.13/7.66 sQ115_spl <=> (greater_or_equal(age(sk3,sk7),tau))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1691,plain,(
% 53.13/7.66 greater_or_equal(age(sk3,sk7),tau)|~sQ115_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1690])).
% 53.13/7.66 fof(f1693,plain,(
% 53.13/7.66 sQ114_spl|sQ115_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f1681,f1685,f1690])).
% 53.13/7.66 fof(f1695,plain,(
% 53.13/7.66 ~greater(sigma,tau)|~sQ114_spl),
% 53.13/7.66 inference(backward_demodulation,[status(thm)],[f1686,f487])).
% 53.13/7.66 fof(f1783,plain,(
% 53.13/7.66 $false|~sQ114_spl),
% 53.13/7.66 inference(forward_subsumption_resolution,[status(thm)],[f1695,f119])).
% 53.13/7.66 fof(f1784,plain,(
% 53.13/7.66 ~sQ114_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f1783])).
% 53.13/7.66 fof(f1949,plain,(
% 53.13/7.66 greater(age(sk3,sk7),tau)|age(sk3,sk7)=tau|~sQ115_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f1691,f62])).
% 53.13/7.66 fof(f1950,definition,(
% 53.13/7.66 sQ127_spl <=> (greater(age(sk3,sk7),tau))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1951,plain,(
% 53.13/7.66 greater(age(sk3,sk7),tau)|~sQ127_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1950])).
% 53.13/7.66 fof(f1953,plain,(
% 53.13/7.66 sQ127_spl|sQ114_spl|~sQ115_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f1949,f1950,f1685,f1690])).
% 53.13/7.66 fof(f1962,plain,(
% 53.13/7.66 ![X0]: (has_immunity(sk3,X0)|positional_advantage(sk3,X0)|hazard_of_mortality(sk3,X0)=mod2|~age(sk3,X0)=zero)),
% 53.13/7.66 inference(resolution,[status(thm)],[f844,f113])).
% 53.13/7.66 fof(f1990,plain,(
% 53.13/7.66 ![X0,X1]: (is_aligned(sk3,X0)|~age(sk3,X1)=zero|~age(sk3,X1)=zero|greater(age(sk3,X0),sigma))),
% 53.13/7.66 inference(resolution,[status(thm)],[f1165,f138])).
% 53.13/7.66 fof(f1994,definition,(
% 53.13/7.66 ![X0]: (sQ128_spl <=> (is_aligned(sk3,X0)|greater(age(sk3,X0),sigma)))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f1995,plain,(
% 53.13/7.66 ![X0]: (is_aligned(sk3,X0)|greater(age(sk3,X0),sigma)|~sQ128_spl)),
% 53.13/7.66 inference(component_clause,[status(thm)],[f1994])).
% 53.13/7.66 fof(f1997,plain,(
% 53.13/7.66 sQ128_spl|sQ60_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f1990,f1994,f1171])).
% 53.13/7.66 fof(f2089,plain,(
% 53.13/7.66 positional_advantage(sk3,sk7)|~sQ127_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f1951,f591])).
% 53.13/7.66 fof(f2096,plain,(
% 53.13/7.66 ~organization(sk3)|has_immunity(sk3,sk7)|is_aligned(sk3,sk7)|hazard_of_mortality(sk3,sk7)=mod1|~sQ127_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f2089,f104])).
% 53.13/7.66 fof(f2098,definition,(
% 53.13/7.66 sQ137_spl <=> (has_immunity(sk3,sk7))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f2099,plain,(
% 53.13/7.66 has_immunity(sk3,sk7)|~sQ137_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f2098])).
% 53.13/7.66 fof(f2101,definition,(
% 53.13/7.66 sQ138_spl <=> (is_aligned(sk3,sk7))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f2102,plain,(
% 53.13/7.66 is_aligned(sk3,sk7)|~sQ138_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f2101])).
% 53.13/7.66 fof(f2108,definition,(
% 53.13/7.66 sQ140_spl <=> (hazard_of_mortality(sk3,sk7)=mod1)),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f2109,plain,(
% 53.13/7.66 hazard_of_mortality(sk3,sk7)=mod1|~sQ140_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f2108])).
% 53.13/7.66 fof(f2111,plain,(
% 53.13/7.66 ~sQ68_spl|sQ137_spl|sQ138_spl|sQ140_spl|~sQ127_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f2096,f1198,f2098,f2101,f2108,f1950])).
% 53.13/7.66 fof(f2119,plain,(
% 53.13/7.66 ~organization(sk3)|has_endowment(sk3)|~sQ137_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f2099,f79])).
% 53.13/7.66 fof(f2124,plain,(
% 53.13/7.66 ~sQ68_spl|sQ95_spl|~sQ137_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f2119,f1198,f1522,f2098])).
% 53.13/7.66 fof(f2192,definition,(
% 53.13/7.66 sQ150_spl <=> (positional_advantage(sk3,sk5))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f2199,definition,(
% 53.13/7.66 sQ151_spl <=> (has_immunity(sk3,sk5))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f2200,plain,(
% 53.13/7.66 has_immunity(sk3,sk5)|~sQ151_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f2199])).
% 53.13/7.66 fof(f2202,definition,(
% 53.13/7.66 sQ152_spl <=> (is_aligned(sk3,sk5))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f2203,plain,(
% 53.13/7.66 is_aligned(sk3,sk5)|~sQ152_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f2202])).
% 53.13/7.66 fof(f2204,plain,(
% 53.13/7.66 ~is_aligned(sk3,sk5)|sQ152_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f2202])).
% 53.13/7.66 fof(f2233,plain,(
% 53.13/7.66 ~organization(sk3)|has_endowment(sk3)|~sQ151_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f2200,f79])).
% 53.13/7.66 fof(f2238,plain,(
% 53.13/7.66 ~sQ68_spl|sQ95_spl|~sQ151_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f2233,f1198,f1522,f2199])).
% 53.13/7.66 fof(f2241,plain,(
% 53.13/7.66 ~smaller(mod1,hazard_of_mortality(sk3,sk5))|~sQ140_spl|sQ1_spl),
% 53.13/7.66 inference(forward_demodulation,[status(thm)],[f2109,f130])).
% 53.13/7.66 fof(f2268,definition,(
% 53.13/7.66 sQ158_spl <=> (hazard_of_mortality(sk3,sk5)=mod2)),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f2269,plain,(
% 53.13/7.66 hazard_of_mortality(sk3,sk5)=mod2|~sQ158_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f2268])).
% 53.13/7.66 fof(f2286,definition,(
% 53.13/7.66 sQ163_spl <=> (hazard_of_mortality(sk3,sk4)=mod2)),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f2287,plain,(
% 53.13/7.66 hazard_of_mortality(sk3,sk4)=mod2|~sQ163_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f2286])).
% 53.13/7.66 fof(f2556,plain,(
% 53.13/7.66 ~greater(zero,sigma)|~greater(zero,sigma)),
% 53.13/7.66 inference(resolution,[status(thm)],[f923,f117])).
% 53.13/7.66 fof(f2656,plain,(
% 53.13/7.66 ~sQ54_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f2556,f1040])).
% 53.13/7.66 fof(f2813,plain,(
% 53.13/7.66 ![X0,X1]: (positional_advantage(sk3,X0)|~greater(age(sk3,X0),X1)|smaller(X1,tau)|X1=tau)),
% 53.13/7.66 inference(resolution,[status(thm)],[f1442,f70])).
% 53.13/7.66 fof(f4387,plain,(
% 53.13/7.66 ~robust_position(sk3)|~positional_advantage(sk3,sk5)),
% 53.13/7.66 inference(resolution,[status(thm)],[f120,f96])).
% 53.13/7.66 fof(f4389,plain,(
% 53.13/7.66 ~sQ81_spl|~sQ150_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f4387,f1448,f2192])).
% 53.13/7.66 fof(f6679,plain,(
% 53.13/7.66 positional_advantage(sk3,sk4)|hazard_of_mortality(sk3,sk4)=mod2|~age(sk3,sk4)=zero|sQ89_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f1962,f1494])).
% 53.13/7.66 fof(f6696,definition,(
% 53.13/7.66 sQ265_spl <=> (age(sk3,sk4)=zero)),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f6698,plain,(
% 53.13/7.66 ~age(sk3,sk4)=zero|sQ265_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f6696])).
% 53.13/7.66 fof(f6699,plain,(
% 53.13/7.66 sQ83_spl|sQ163_spl|~sQ265_spl|sQ89_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f6679,f1456,f2286,f6696,f1492])).
% 53.13/7.66 fof(f6709,plain,(
% 53.13/7.66 ~zero=zero|sQ265_spl),
% 53.13/7.66 inference(forward_demodulation,[status(thm)],[f116,f6698])).
% 53.13/7.66 fof(f6710,plain,(
% 53.13/7.66 $false|sQ265_spl),
% 53.13/7.66 inference(trivial_equality_resolution,[status(thm)],[f6709])).
% 53.13/7.66 fof(f6711,plain,(
% 53.13/7.66 sQ265_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f6710])).
% 53.13/7.66 fof(f10276,plain,(
% 53.13/7.66 is_aligned(sk3,sk6)|~sQ128_spl|~sQ5_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f1995,f614])).
% 53.13/7.66 fof(f10312,plain,(
% 53.13/7.66 is_aligned(sk3,sk4)|greater(zero,sigma)|~sQ128_spl),
% 53.13/7.66 inference(paramodulation,[status(thm)],[f116,f1995])).
% 53.13/7.66 fof(f10314,plain,(
% 53.13/7.66 sQ85_spl|~sQ128_spl|~sQ5_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f10276,f1472,f1994,f211])).
% 53.13/7.66 fof(f10321,plain,(
% 53.13/7.66 sQ90_spl|sQ54_spl|~sQ128_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f10312,f1495,f1040,f1994])).
% 53.13/7.66 fof(f10460,plain,(
% 53.13/7.66 ~smaller(hazard_of_mortality(sk3,sk6),mod1)|~sQ140_spl|sQ0_spl),
% 53.13/7.66 inference(forward_demodulation,[status(thm)],[f2109,f127])).
% 53.13/7.66 fof(f10652,plain,(
% 53.13/7.66 ![X0]: (~organization(sk3)|is_aligned(sk3,X0)|dissimilar(sk3,X0,sk4)|~sQ90_spl)),
% 53.13/7.66 inference(resolution,[status(thm)],[f1496,f89])).
% 53.13/7.66 fof(f10656,definition,(
% 53.13/7.66 ![X0]: (sQ320_spl <=> (is_aligned(sk3,X0)|dissimilar(sk3,X0,sk4)))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f10657,plain,(
% 53.13/7.66 ![X0]: (is_aligned(sk3,X0)|dissimilar(sk3,X0,sk4)|~sQ320_spl)),
% 53.13/7.66 inference(component_clause,[status(thm)],[f10656])).
% 53.13/7.66 fof(f10659,plain,(
% 53.13/7.66 ~sQ68_spl|sQ320_spl|~sQ90_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f10652,f1198,f10656,f1495])).
% 53.13/7.66 fof(f10665,plain,(
% 53.13/7.66 ~organization(sk3)|has_immunity(sk3,sk5)|positional_advantage(sk3,sk5)|hazard_of_mortality(sk3,sk5)=mod2|~sQ152_spl),
% 53.13/7.66 inference(resolution,[status(thm)],[f2203,f105])).
% 53.13/7.66 fof(f10669,plain,(
% 53.13/7.66 ~sQ68_spl|sQ151_spl|sQ150_spl|sQ158_spl|~sQ152_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f10665,f1198,f2199,f2192,f2268,f2202])).
% 53.13/7.66 fof(f11345,plain,(
% 53.13/7.66 ![X0]: (is_aligned(sk3,X0)|~age(sk3,X0)=zero|greater(age(sk3,sk4),sigma)|~sQ320_spl)),
% 53.13/7.66 inference(resolution,[status(thm)],[f10657,f138])).
% 53.13/7.66 fof(f11349,definition,(
% 53.13/7.66 sQ331_spl <=> (greater(age(sk3,sk4),sigma))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f11350,plain,(
% 53.13/7.66 greater(age(sk3,sk4),sigma)|~sQ331_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f11349])).
% 53.13/7.66 fof(f11352,plain,(
% 53.13/7.66 sQ64_spl|sQ331_spl|~sQ320_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f11345,f1185,f11349,f10656])).
% 53.13/7.66 fof(f11356,plain,(
% 53.13/7.66 greater(zero,sigma)|~sQ331_spl),
% 53.13/7.66 inference(forward_demodulation,[status(thm)],[f116,f11350])).
% 53.13/7.66 fof(f11357,plain,(
% 53.13/7.66 $false|~sQ331_spl),
% 53.13/7.66 inference(forward_subsumption_resolution,[status(thm)],[f11356,f147])).
% 53.13/7.66 fof(f11358,plain,(
% 53.13/7.66 ~sQ331_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f11357])).
% 53.13/7.66 fof(f11899,plain,(
% 53.13/7.66 ![X0]: (is_aligned(sk3,X0)|positional_advantage(sk3,X0)|smaller(sigma,tau)|sigma=tau|~sQ128_spl)),
% 53.13/7.66 inference(resolution,[status(thm)],[f1995,f2813])).
% 53.13/7.66 fof(f11930,plain,(
% 53.13/7.66 is_aligned(sk3,sk6)|greater(sigma,sigma)|~sQ128_spl|~sQ6_spl),
% 53.13/7.66 inference(paramodulation,[status(thm)],[f215,f1995])).
% 53.13/7.66 fof(f11933,definition,(
% 53.13/7.66 ![X0]: (sQ343_spl <=> (is_aligned(sk3,X0)|positional_advantage(sk3,X0)))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f11934,plain,(
% 53.13/7.66 ![X0]: (is_aligned(sk3,X0)|positional_advantage(sk3,X0)|~sQ343_spl)),
% 53.13/7.66 inference(component_clause,[status(thm)],[f11933])).
% 53.13/7.66 fof(f11936,plain,(
% 53.13/7.66 sQ343_spl|sQ111_spl|sQ19_spl|~sQ128_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f11899,f11933,f1670,f386,f1994])).
% 53.13/7.66 fof(f11939,definition,(
% 53.13/7.66 sQ344_spl <=> (greater(sigma,sigma))),
% 53.13/7.66 introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition])).
% 53.13/7.66 fof(f11940,plain,(
% 53.13/7.66 greater(sigma,sigma)|~sQ344_spl),
% 53.13/7.66 inference(component_clause,[status(thm)],[f11939])).
% 53.13/7.66 fof(f11942,plain,(
% 53.13/7.66 sQ85_spl|sQ344_spl|~sQ128_spl|~sQ6_spl),
% 53.13/7.66 inference(split_clause,[status(thm)],[f11930,f1472,f11939,f1994,f214])).
% 53.13/7.66 fof(f11945,plain,(
% 53.13/7.66 $false|~sQ344_spl),
% 53.13/7.66 inference(forward_subsumption_resolution,[status(thm)],[f11940,f942])).
% 53.13/7.66 fof(f11946,plain,(
% 53.13/7.66 ~sQ344_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f11945])).
% 53.13/7.66 fof(f11947,plain,(
% 53.13/7.66 $false|~sQ111_spl),
% 53.13/7.66 inference(forward_subsumption_resolution,[status(thm)],[f1671,f162])).
% 53.13/7.66 fof(f11948,plain,(
% 53.13/7.66 ~sQ111_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f11947])).
% 53.13/7.66 fof(f11950,plain,(
% 53.13/7.66 ~smaller(low,mod1)|~sQ86_spl|~sQ140_spl|sQ0_spl),
% 53.13/7.66 inference(backward_demodulation,[status(thm)],[f1476,f10460])).
% 53.13/7.66 fof(f11951,plain,(
% 53.13/7.66 $false|~sQ86_spl|~sQ140_spl|sQ0_spl),
% 53.13/7.66 inference(forward_subsumption_resolution,[status(thm)],[f11950,f152])).
% 53.13/7.66 fof(f11952,plain,(
% 53.13/7.66 ~sQ86_spl|~sQ140_spl|sQ0_spl),
% 53.13/7.66 inference(contradiction_clause,[status(thm)],[f11951])).
% 53.13/7.66 fof(f11955,plain,(
% 53.13/7.69 ~smaller(mod1,mod2)|~sQ158_spl|~sQ140_spl|sQ1_spl),
% 53.13/7.69 inference(forward_demodulation,[status(thm)],[f2269,f2241])).
% 53.13/7.69 fof(f11956,plain,(
% 53.13/7.69 $false|~sQ158_spl|~sQ140_spl|sQ1_spl),
% 53.13/7.69 inference(forward_subsumption_resolution,[status(thm)],[f11955,f160])).
% 53.13/7.69 fof(f11957,plain,(
% 53.13/7.69 ~sQ158_spl|~sQ140_spl|sQ1_spl),
% 53.13/7.69 inference(contradiction_clause,[status(thm)],[f11956])).
% 53.13/7.69 fof(f11960,plain,(
% 53.13/7.69 ~mod2=hazard_of_mortality(sk3,sk4)|~sQ158_spl|sQ2_spl),
% 53.13/7.69 inference(forward_demodulation,[status(thm)],[f2269,f133])).
% 53.13/7.69 fof(f11961,plain,(
% 53.13/7.69 ~mod2=mod2|~sQ163_spl|~sQ158_spl|sQ2_spl),
% 53.13/7.69 inference(forward_demodulation,[status(thm)],[f2287,f11960])).
% 53.13/7.69 fof(f11962,plain,(
% 53.13/7.69 $false|~sQ163_spl|~sQ158_spl|sQ2_spl),
% 53.13/7.69 inference(trivial_equality_resolution,[status(thm)],[f11961])).
% 53.13/7.69 fof(f11963,plain,(
% 53.13/7.69 ~sQ163_spl|~sQ158_spl|sQ2_spl),
% 53.13/7.69 inference(contradiction_clause,[status(thm)],[f11962])).
% 53.13/7.69 fof(f11979,plain,(
% 53.13/7.69 positional_advantage(sk3,sk5)|~sQ343_spl|sQ152_spl),
% 53.13/7.69 inference(resolution,[status(thm)],[f11934,f2204])).
% 53.13/7.69 fof(f11987,plain,(
% 53.13/7.69 sQ150_spl|~sQ343_spl|sQ152_spl),
% 53.13/7.69 inference(split_clause,[status(thm)],[f11979,f2192,f11933,f2202])).
% 53.13/7.69 fof(f12095,plain,(
% 53.13/7.69 ~greater(age(sk3,sk7),sigma)|~sQ138_spl|~sQ63_spl),
% 53.13/7.69 inference(resolution,[status(thm)],[f2102,f1182])).
% 53.13/7.69 fof(f12099,plain,(
% 53.13/7.69 $false|~sQ138_spl|~sQ63_spl),
% 53.13/7.69 inference(forward_subsumption_resolution,[status(thm)],[f12095,f123])).
% 53.13/7.69 fof(f12100,plain,(
% 53.13/7.69 ~sQ138_spl|~sQ63_spl),
% 53.13/7.69 inference(contradiction_clause,[status(thm)],[f12099])).
% 53.13/7.69 fof(f12101,plain,(
% 53.13/7.69 $false),
% 53.13/7.69 inference(sat_refutation,[status(thm)],[f134,f217,f711,f1184,f1201,f1206,f1207,f1211,f1213,f1478,f1509,f1514,f1525,f1528,f1540,f1545,f1693,f1784,f1953,f1997,f2111,f2124,f2238,f2656,f4389,f6699,f6711,f10314,f10321,f10659,f10669,f11352,f11358,f11936,f11942,f11946,f11948,f11952,f11957,f11963,f11987,f12100])).
% 53.13/7.69 % SZS output end CNFRefutation for theBenchmark.p
% 9.25/7.70 % Elapsed time: 7.229723 seconds
% 9.25/7.70 % CPU time: 56.549630 seconds
% 9.25/7.70 % Total memory used: 267.533 MB
% 9.25/7.70 % Net memory used: 236.151 MB
%------------------------------------------------------------------------------