%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT061+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 : 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:52 PM UTC 2026
% Result : Theorem 3.97s 0.96s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT061+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.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:24:18 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 3.97/0.96 % Refutation found
% 3.97/0.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.97/0.96 % SZS output start CNFRefutation for theBenchmark
% 3.97/0.96 fof(f1,axiom,(
% 3.97/0.96 (! [X,Y] :( smaller_or_equal(X,Y)<=> ( smaller(X,Y)| X = Y ) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f3,axiom,(
% 3.97/0.96 (! [X,Y] :( smaller(X,Y)<=> greater(Y,X) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f5,axiom,(
% 3.97/0.96 (! [X,Y,Z] :( ( greater(X,Y)& greater(Y,Z) )=> greater(X,Z) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f7,axiom,(
% 3.97/0.96 (! [X,T] :( ( organization(X)& ~ has_endowment(X) )=> ~ has_immunity(X,T) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f8,axiom,(
% 3.97/0.96 (! [X,T0,T] :( dissimilar(X,T0,T)<=> ( organization(X)& ~ ( is_aligned(X,T0)<=> is_aligned(X,T) ) ) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f9,axiom,(
% 3.97/0.96 (! [X,T] :( ( organization(X)& age(X,T) = zero )=> is_aligned(X,T) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f10,axiom,(
% 3.97/0.96 (! [X,T0,T] :( ( organization(X)& age(X,T0) = zero )=> ( greater(age(X,T),sigma)<=> dissimilar(X,T0,T) ) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f11,axiom,(
% 3.97/0.96 (! [X] :( fragile_position(X)<=> (! [T] :( ( smaller_or_equal(age(X,T),sigma)=> positional_advantage(X,T) )& ( greater(age(X,T),sigma)=> ~ positional_advantage(X,T) ) ) )) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f12,axiom,(
% 3.97/0.96 (! [X,T] :( organization(X)=> ( ( has_immunity(X,T)=> hazard_of_mortality(X,T) = very_low )& ( ~ has_immunity(X,T)=> ( ( ( is_aligned(X,T)& positional_advantage(X,T) )=> hazard_of_mortality(X,T) = low )& ( ( ~ is_aligned(X,T)& positional_advantage(X,T) )=> hazard_of_mortality(X,T) = mod1 )& ( ( is_aligned(X,T)& ~ positional_advantage(X,T) )=> hazard_of_mortality(X,T) = mod2 )& ( ( ~ is_aligned(X,T)& ~ positional_advantage(X,T) )=> hazard_of_mortality(X,T) = high ) ) ) ) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f13,axiom,(
% 3.97/0.96 greater(high,mod1) ),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f14,axiom,(
% 3.97/0.96 greater(mod1,low) ),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f18,conjecture,(
% 3.97/0.96 (! [X,T0,T1,T2] :( ( organization(X)& fragile_position(X)& ~ has_endowment(X)& age(X,T0) = zero& greater(sigma,zero)& smaller_or_equal(age(X,T1),sigma)& greater(age(X,T2),sigma) )=> ( greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) )),
% 3.97/0.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.97/0.96 fof(f19,negated_conjecture,(
% 3.97/0.96 ~((! [X,T0,T1,T2] :( ( organization(X)& fragile_position(X)& ~ has_endowment(X)& age(X,T0) = zero& greater(sigma,zero)& smaller_or_equal(age(X,T1),sigma)& greater(age(X,T2),sigma) )=> ( greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ))),
% 3.97/0.96 inference(negated_conjecture,[status(cth)],[f18])).
% 3.97/0.96 fof(f20,plain,(
% 3.97/0.96 ![X,Y]: ((~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y))&(smaller_or_equal(X,Y)|(~smaller(X,Y)&~X=Y)))),
% 3.97/0.96 inference(NNF_transformation,[status(thm)],[f1])).
% 3.97/0.96 fof(f21,plain,(
% 3.97/0.96 (![X,Y]: (~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y)))&(![X,Y]: (smaller_or_equal(X,Y)|(~smaller(X,Y)&~X=Y)))),
% 3.97/0.96 inference(miniscoping,[status(thm)],[f20])).
% 3.97/0.96 fof(f23,plain,(
% 3.97/0.96 ![X0,X1]: (smaller_or_equal(X0,X1)|~smaller(X0,X1))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f21])).
% 3.97/0.96 fof(f30,plain,(
% 3.97/0.96 ![X,Y]: ((~smaller(X,Y)|greater(Y,X))&(smaller(X,Y)|~greater(Y,X)))),
% 3.97/0.96 inference(NNF_transformation,[status(thm)],[f3])).
% 3.97/0.96 fof(f31,plain,(
% 3.97/0.96 (![X,Y]: (~smaller(X,Y)|greater(Y,X)))&(![X,Y]: (smaller(X,Y)|~greater(Y,X)))),
% 3.97/0.96 inference(miniscoping,[status(thm)],[f30])).
% 3.97/0.96 fof(f33,plain,(
% 3.97/0.96 ![X0,X1]: (smaller(X0,X1)|~greater(X1,X0))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f31])).
% 3.97/0.96 fof(f36,plain,(
% 3.97/0.96 ![X,Y,Z]: ((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))),
% 3.97/0.96 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 3.97/0.96 fof(f37,plain,(
% 3.97/0.96 ![X,Z]: ((![Y]: (~greater(X,Y)|~greater(Y,Z)))|greater(X,Z))),
% 3.97/0.96 inference(miniscoping,[status(thm)],[f36])).
% 3.97/0.96 fof(f38,plain,(
% 3.97/0.96 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f37])).
% 3.97/0.96 fof(f40,plain,(
% 3.97/0.96 ![X,T]: ((~organization(X)|has_endowment(X))|~has_immunity(X,T))),
% 3.97/0.96 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 3.97/0.96 fof(f41,plain,(
% 3.97/0.96 ![X]: ((~organization(X)|has_endowment(X))|(![T]: ~has_immunity(X,T)))),
% 3.97/0.96 inference(miniscoping,[status(thm)],[f40])).
% 3.97/0.96 fof(f42,plain,(
% 3.97/0.96 ![X0,X1]: (~organization(X0)|has_endowment(X0)|~has_immunity(X0,X1))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f41])).
% 3.97/0.96 fof(f43,plain,(
% 3.97/0.96 ![X,T0,T]: (dissimilar(X,T0,T)<=>(organization(X)&(is_aligned(X,T0)<~>is_aligned(X,T))))),
% 3.97/0.96 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 3.97/0.96 fof(f44,plain,(
% 3.97/0.96 ![X,T0,T]: ((~dissimilar(X,T0,T)|(organization(X)&((is_aligned(X,T0)|is_aligned(X,T))&(~is_aligned(X,T0)|~is_aligned(X,T)))))&(dissimilar(X,T0,T)|(~organization(X)|((~is_aligned(X,T0)|is_aligned(X,T))&(is_aligned(X,T0)|~is_aligned(X,T))))))),
% 3.97/0.96 inference(NNF_transformation,[status(thm)],[f43])).
% 3.97/0.96 fof(f45,plain,(
% 3.97/0.96 (![X,T0,T]: (~dissimilar(X,T0,T)|(organization(X)&((is_aligned(X,T0)|is_aligned(X,T))&(~is_aligned(X,T0)|~is_aligned(X,T))))))&(![X,T0,T]: (dissimilar(X,T0,T)|(~organization(X)|((~is_aligned(X,T0)|is_aligned(X,T))&(is_aligned(X,T0)|~is_aligned(X,T))))))),
% 3.97/0.96 inference(miniscoping,[status(thm)],[f44])).
% 3.97/0.96 fof(f46,plain,(
% 3.97/0.96 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|organization(X0))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f45])).
% 3.97/0.96 fof(f48,plain,(
% 3.97/0.96 ![X0,X1,X2]: (~dissimilar(X0,X1,X2)|~is_aligned(X0,X1)|~is_aligned(X0,X2))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f45])).
% 3.97/0.96 fof(f49,plain,(
% 3.97/0.96 ![X0,X1,X2]: (dissimilar(X0,X1,X2)|~organization(X0)|~is_aligned(X0,X1)|is_aligned(X0,X2))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f45])).
% 3.97/0.96 fof(f51,plain,(
% 3.97/0.96 ![X,T]: ((~organization(X)|~age(X,T)=zero)|is_aligned(X,T))),
% 3.97/0.96 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 3.97/0.96 fof(f52,plain,(
% 3.97/0.96 ![X0,X1]: (~organization(X0)|~age(X0,X1)=zero|is_aligned(X0,X1))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f51])).
% 3.97/0.96 fof(f53,plain,(
% 3.97/0.96 ![X,T0,T]: ((~organization(X)|~age(X,T0)=zero)|(greater(age(X,T),sigma)<=>dissimilar(X,T0,T)))),
% 3.97/0.96 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 3.97/0.96 fof(f54,plain,(
% 3.97/0.96 ![X,T0,T]: ((~organization(X)|~age(X,T0)=zero)|((~greater(age(X,T),sigma)|dissimilar(X,T0,T))&(greater(age(X,T),sigma)|~dissimilar(X,T0,T))))),
% 3.97/0.96 inference(NNF_transformation,[status(thm)],[f53])).
% 3.97/0.96 fof(f55,plain,(
% 3.97/0.96 ![X,T0]: ((~organization(X)|~age(X,T0)=zero)|((![T]: (~greater(age(X,T),sigma)|dissimilar(X,T0,T)))&(![T]: (greater(age(X,T),sigma)|~dissimilar(X,T0,T)))))),
% 3.97/0.96 inference(miniscoping,[status(thm)],[f54])).
% 3.97/0.96 fof(f56,plain,(
% 3.97/0.96 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|~greater(age(X0,X2),sigma)|dissimilar(X0,X1,X2))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f55])).
% 3.97/0.96 fof(f57,plain,(
% 3.97/0.96 ![X0,X1,X2]: (~organization(X0)|~age(X0,X1)=zero|greater(age(X0,X2),sigma)|~dissimilar(X0,X1,X2))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f55])).
% 3.97/0.96 fof(f58,plain,(
% 3.97/0.96 ![X]: (fragile_position(X)<=>(![T]: ((~smaller_or_equal(age(X,T),sigma)|positional_advantage(X,T))&(~greater(age(X,T),sigma)|~positional_advantage(X,T)))))),
% 3.97/0.96 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 3.97/0.96 fof(f59,plain,(
% 3.97/0.96 ![X]: ((~fragile_position(X)|(![T]: ((~smaller_or_equal(age(X,T),sigma)|positional_advantage(X,T))&(~greater(age(X,T),sigma)|~positional_advantage(X,T)))))&(fragile_position(X)|(?[T]: ((smaller_or_equal(age(X,T),sigma)&~positional_advantage(X,T))|(greater(age(X,T),sigma)&positional_advantage(X,T))))))),
% 3.97/0.96 inference(NNF_transformation,[status(thm)],[f58])).
% 3.97/0.96 fof(f60,plain,(
% 3.97/0.96 (![X]: (~fragile_position(X)|((![T]: (~smaller_or_equal(age(X,T),sigma)|positional_advantage(X,T)))&(![T]: (~greater(age(X,T),sigma)|~positional_advantage(X,T))))))&(![X]: (fragile_position(X)|((?[T]: (smaller_or_equal(age(X,T),sigma)&~positional_advantage(X,T)))|(?[T]: (greater(age(X,T),sigma)&positional_advantage(X,T))))))),
% 3.97/0.96 inference(miniscoping,[status(thm)],[f59])).
% 3.97/0.96 fof(f61,plain,(
% 3.97/0.96 (![X]: (~fragile_position(X)|((![T]: (~smaller_or_equal(age(X,T),sigma)|positional_advantage(X,T)))&(![T]: (~greater(age(X,T),sigma)|~positional_advantage(X,T))))))&(![X]: (fragile_position(X)|((smaller_or_equal(age(X,sK0_skl(X)),sigma)&~positional_advantage(X,sK0_skl(X)))|(greater(age(X,sK1_skl(X)),sigma)&positional_advantage(X,sK1_skl(X))))))),
% 3.97/0.96 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(T,sK0_skl(X)),skolemize(T,sK1_skl(X))],[f60])).
% 3.97/0.96 fof(f62,plain,(
% 3.97/0.96 ![X0,X1]: (~fragile_position(X0)|~smaller_or_equal(age(X0,X1),sigma)|positional_advantage(X0,X1))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f61])).
% 3.97/0.96 fof(f63,plain,(
% 3.97/0.96 ![X0,X1]: (~fragile_position(X0)|~greater(age(X0,X1),sigma)|~positional_advantage(X0,X1))),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f61])).
% 3.97/0.96 fof(f68,plain,(
% 3.97/0.96 ![X,T]: (~organization(X)|((~has_immunity(X,T)|hazard_of_mortality(X,T)=very_low)&(has_immunity(X,T)|(((((~is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=low)&((is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=mod1))&((~is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=mod2))&((is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=high)))))),
% 3.97/0.96 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 3.97/0.96 fof(f69,plain,(
% 3.97/0.96 ![X]: (~organization(X)|((![T]: (~has_immunity(X,T)|hazard_of_mortality(X,T)=very_low))&(![T]: (has_immunity(X,T)|(((((~is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=low)&((is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=mod1))&((~is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=mod2))&((is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=high))))))),
% 3.97/0.96 inference(miniscoping,[status(thm)],[f68])).
% 3.97/0.96 fof(f71,plain,(
% 3.97/0.96 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|~is_aligned(X0,X1)|~positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=low)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f69])).
% 3.97/0.96 fof(f74,plain,(
% 3.97/0.96 ![X0,X1]: (~organization(X0)|has_immunity(X0,X1)|is_aligned(X0,X1)|positional_advantage(X0,X1)|hazard_of_mortality(X0,X1)=high)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f69])).
% 3.97/0.96 fof(f75,plain,(
% 3.97/0.96 greater(high,mod1)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f13])).
% 3.97/0.96 fof(f76,plain,(
% 3.97/0.96 greater(mod1,low)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f14])).
% 3.97/0.96 fof(f80,plain,(
% 3.97/0.96 (?[X,T0,T1,T2]: (((((((organization(X)&fragile_position(X))&~has_endowment(X))&age(X,T0)=zero)&greater(sigma,zero))&smaller_or_equal(age(X,T1),sigma))&greater(age(X,T2),sigma))&(~greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))|~hazard_of_mortality(X,T1)=hazard_of_mortality(X,T0))))),
% 3.97/0.96 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 3.97/0.96 fof(f81,plain,(
% 3.97/0.96 (((((((organization(sK2_skl)&fragile_position(sK2_skl))&~has_endowment(sK2_skl))&age(sK2_skl,sK3_skl)=zero)&greater(sigma,zero))&smaller_or_equal(age(sK2_skl,sK4_skl),sigma))&greater(age(sK2_skl,sK5_skl),sigma))&(~greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl))|~hazard_of_mortality(sK2_skl,sK4_skl)=hazard_of_mortality(sK2_skl,sK3_skl)))),
% 3.97/0.96 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(X,sK2_skl),skolemize(T0,sK3_skl),skolemize(T1,sK4_skl),skolemize(T2,sK5_skl)],[f80])).
% 3.97/0.96 fof(f82,plain,(
% 3.97/0.96 organization(sK2_skl)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f81])).
% 3.97/0.96 fof(f83,plain,(
% 3.97/0.96 fragile_position(sK2_skl)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f81])).
% 3.97/0.96 fof(f84,plain,(
% 3.97/0.96 ~has_endowment(sK2_skl)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f81])).
% 3.97/0.96 fof(f85,plain,(
% 3.97/0.96 age(sK2_skl,sK3_skl)=zero),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f81])).
% 3.97/0.96 fof(f86,plain,(
% 3.97/0.96 greater(sigma,zero)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f81])).
% 3.97/0.96 fof(f87,plain,(
% 3.97/0.96 smaller_or_equal(age(sK2_skl,sK4_skl),sigma)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f81])).
% 3.97/0.96 fof(f88,plain,(
% 3.97/0.96 greater(age(sK2_skl,sK5_skl),sigma)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f81])).
% 3.97/0.96 fof(f89,plain,(
% 3.97/0.96 ~greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl))|~hazard_of_mortality(sK2_skl,sK4_skl)=hazard_of_mortality(sK2_skl,sK3_skl)),
% 3.97/0.96 inference(cnf_transformation,[status(thm)],[f81])).
% 3.97/0.96 fof(f96,plain,(
% 3.97/0.96 ![X0]: (~age(sK2_skl,X0)=zero|is_aligned(sK2_skl,X0))),
% 3.97/0.96 inference(resolution,[status(thm)],[f52,f82])).
% 3.97/0.96 fof(f97,plain,(
% 3.97/0.96 is_aligned(sK2_skl,sK3_skl)),
% 3.97/0.96 inference(resolution,[status(thm)],[f96,f85])).
% 3.97/0.96 fof(f101,plain,(
% 3.97/0.96 ![X0]: (~organization(sK2_skl)|~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,sK5_skl))),
% 3.97/0.96 inference(resolution,[status(thm)],[f56,f88])).
% 3.97/0.96 fof(f103,plain,(
% 3.97/0.96 ![X0]: (~age(sK2_skl,X0)=zero|dissimilar(sK2_skl,X0,sK5_skl))),
% 3.97/0.96 inference(forward_subsumption_resolution,[status(thm)],[f101,f82])).
% 3.97/0.96 fof(f104,plain,(
% 3.97/0.96 ![X0]: (~greater(mod1,X0)|greater(high,X0))),
% 3.97/0.96 inference(resolution,[status(thm)],[f75,f38])).
% 3.97/0.96 fof(f135,plain,(
% 3.97/0.96 dissimilar(sK2_skl,sK3_skl,sK5_skl)),
% 3.97/0.96 inference(resolution,[status(thm)],[f103,f85])).
% 3.97/0.96 fof(f141,plain,(
% 3.97/0.96 greater(high,low)),
% 3.97/0.96 inference(resolution,[status(thm)],[f104,f76])).
% 3.97/0.96 fof(f156,plain,(
% 3.97/0.96 ~fragile_position(sK2_skl)|positional_advantage(sK2_skl,sK4_skl)),
% 3.97/0.96 inference(resolution,[status(thm)],[f62,f87])).
% 3.97/0.96 fof(f157,plain,(
% 3.97/0.96 ~fragile_position(sK2_skl)|~smaller_or_equal(zero,sigma)|positional_advantage(sK2_skl,sK3_skl)),
% 3.97/0.96 inference(paramodulation,[status(thm)],[f85,f62])).
% 3.97/0.96 fof(f158,plain,(
% 3.97/0.96 positional_advantage(sK2_skl,sK4_skl)),
% 3.97/0.96 inference(forward_subsumption_resolution,[status(thm)],[f156,f83])).
% 3.97/0.96 fof(f159,plain,(
% 3.97/0.96 ~smaller_or_equal(zero,sigma)|positional_advantage(sK2_skl,sK3_skl)),
% 3.97/0.96 inference(forward_subsumption_resolution,[status(thm)],[f157,f83])).
% 3.97/0.96 fof(f160,plain,(
% 3.97/0.96 ~fragile_position(sK2_skl)|~positional_advantage(sK2_skl,sK5_skl)),
% 3.97/0.96 inference(resolution,[status(thm)],[f63,f88])).
% 3.97/0.96 fof(f162,plain,(
% 3.97/0.96 ~positional_advantage(sK2_skl,sK5_skl)),
% 3.97/0.96 inference(forward_subsumption_resolution,[status(thm)],[f160,f83])).
% 3.97/0.96 fof(f173,plain,(
% 3.97/0.96 smaller(zero,sigma)),
% 3.97/0.96 inference(resolution,[status(thm)],[f33,f86])).
% 3.97/0.96 fof(f191,plain,(
% 3.97/0.96 smaller_or_equal(zero,sigma)),
% 3.97/0.96 inference(resolution,[status(thm)],[f173,f23])).
% 3.97/0.96 fof(f219,plain,(
% 3.97/0.96 ![X0,X1,X2]: (~age(X0,X1)=zero|greater(age(X0,X2),sigma)|~dissimilar(X0,X1,X2))),
% 3.97/0.96 inference(backward_subsumption_resolution,[status(thm)],[f57,f46])).
% 3.97/0.96 fof(f229,plain,(
% 3.97/0.96 positional_advantage(sK2_skl,sK3_skl)),
% 3.97/0.96 inference(forward_subsumption_resolution,[status(thm)],[f159,f191])).
% 3.97/0.96 fof(f323,plain,(
% 3.97/0.96 ~is_aligned(sK2_skl,sK3_skl)|~is_aligned(sK2_skl,sK5_skl)),
% 3.97/0.96 inference(resolution,[status(thm)],[f48,f135])).
% 3.97/0.96 fof(f324,plain,(
% 3.97/0.96 ~is_aligned(sK2_skl,sK5_skl)),
% 3.97/0.96 inference(forward_subsumption_resolution,[status(thm)],[f323,f97])).
% 3.97/0.96 fof(f355,plain,(
% 3.97/0.96 ![X0]: (dissimilar(sK2_skl,sK3_skl,X0)|~organization(sK2_skl)|is_aligned(sK2_skl,X0))),
% 3.97/0.96 inference(resolution,[status(thm)],[f49,f97])).
% 3.97/0.96 fof(f356,plain,(
% 3.97/0.96 ![X0]: (dissimilar(sK2_skl,sK3_skl,X0)|is_aligned(sK2_skl,X0))),
% 3.97/0.96 inference(forward_subsumption_resolution,[status(thm)],[f355,f82])).
% 3.97/0.96 fof(f367,plain,(
% 3.97/0.96 ![X0]: (is_aligned(sK2_skl,X0)|~age(sK2_skl,sK3_skl)=zero|greater(age(sK2_skl,X0),sigma))),
% 3.97/0.96 inference(resolution,[status(thm)],[f356,f219])).
% 3.97/0.96 fof(f370,plain,(
% 3.97/0.96 ![X0]: (is_aligned(sK2_skl,X0)|~zero=zero|greater(age(sK2_skl,X0),sigma))),
% 3.97/0.96 inference(forward_demodulation,[status(thm)],[f85,f367])).
% 3.97/0.96 fof(f371,plain,(
% 3.97/0.96 ![X0]: (is_aligned(sK2_skl,X0)|greater(age(sK2_skl,X0),sigma))),
% 3.97/0.96 inference(trivial_equality_resolution,[status(thm)],[f370])).
% 3.97/0.96 fof(f982,plain,(
% 3.97/0.96 ~organization(sK2_skl)|has_immunity(sK2_skl,sK3_skl)|~is_aligned(sK2_skl,sK3_skl)|hazard_of_mortality(sK2_skl,sK3_skl)=low),
% 3.97/0.96 inference(resolution,[status(thm)],[f71,f229])).
% 3.97/0.96 fof(f983,plain,(
% 3.97/0.96 ~organization(sK2_skl)|has_immunity(sK2_skl,sK4_skl)|~is_aligned(sK2_skl,sK4_skl)|hazard_of_mortality(sK2_skl,sK4_skl)=low),
% 3.97/0.96 inference(resolution,[status(thm)],[f71,f158])).
% 3.97/0.96 fof(f984,plain,(
% 3.97/0.96 has_immunity(sK2_skl,sK3_skl)|~is_aligned(sK2_skl,sK3_skl)|hazard_of_mortality(sK2_skl,sK3_skl)=low),
% 3.97/0.96 inference(forward_subsumption_resolution,[status(thm)],[f982,f82])).
% 3.97/0.96 fof(f985,plain,(
% 3.97/0.96 has_immunity(sK2_skl,sK4_skl)|~is_aligned(sK2_skl,sK4_skl)|hazard_of_mortality(sK2_skl,sK4_skl)=low),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f983,f82])).
% 3.97/0.98 fof(f1351,plain,(
% 3.97/0.98 ![X0]: (has_immunity(sK2_skl,X0)|is_aligned(sK2_skl,X0)|positional_advantage(sK2_skl,X0)|hazard_of_mortality(sK2_skl,X0)=high)),
% 3.97/0.98 inference(resolution,[status(thm)],[f74,f82])).
% 3.97/0.98 fof(f1405,plain,(
% 3.97/0.98 has_immunity(sK2_skl,sK5_skl)|is_aligned(sK2_skl,sK5_skl)|hazard_of_mortality(sK2_skl,sK5_skl)=high),
% 3.97/0.98 inference(resolution,[status(thm)],[f1351,f162])).
% 3.97/0.98 fof(f1411,plain,(
% 3.97/0.98 has_immunity(sK2_skl,sK5_skl)|hazard_of_mortality(sK2_skl,sK5_skl)=high),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1405,f324])).
% 3.97/0.98 fof(f1879,plain,(
% 3.97/0.98 has_immunity(sK2_skl,sK3_skl)|hazard_of_mortality(sK2_skl,sK3_skl)=low),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f984,f97])).
% 3.97/0.98 fof(f1881,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK3_skl)=low|~organization(sK2_skl)|has_endowment(sK2_skl)),
% 3.97/0.98 inference(resolution,[status(thm)],[f1879,f42])).
% 3.97/0.98 fof(f1883,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK3_skl)=low|has_endowment(sK2_skl)),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1881,f82])).
% 3.97/0.98 fof(f1886,plain,(
% 3.97/0.98 ~greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl))|~hazard_of_mortality(sK2_skl,sK4_skl)=low),
% 3.97/0.98 inference(backward_demodulation,[status(thm)],[f1887,f89])).
% 3.97/0.98 fof(f1887,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK3_skl)=low),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1883,f84])).
% 3.97/0.98 fof(f2575,plain,(
% 3.97/0.98 ![X0]: (is_aligned(sK2_skl,X0)|~fragile_position(sK2_skl)|~positional_advantage(sK2_skl,X0))),
% 3.97/0.98 inference(resolution,[status(thm)],[f371,f63])).
% 3.97/0.98 fof(f2588,plain,(
% 3.97/0.98 ![X0]: (is_aligned(sK2_skl,X0)|~positional_advantage(sK2_skl,X0))),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2575,f83])).
% 3.97/0.98 fof(f2602,plain,(
% 3.97/0.98 is_aligned(sK2_skl,sK4_skl)),
% 3.97/0.98 inference(resolution,[status(thm)],[f2588,f158])).
% 3.97/0.98 fof(f2603,plain,(
% 3.97/0.98 has_immunity(sK2_skl,sK4_skl)|hazard_of_mortality(sK2_skl,sK4_skl)=low),
% 3.97/0.98 inference(backward_subsumption_resolution,[status(thm)],[f985,f2602])).
% 3.97/0.98 fof(f3023,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK5_skl)=high|~organization(sK2_skl)|has_endowment(sK2_skl)),
% 3.97/0.98 inference(resolution,[status(thm)],[f1411,f42])).
% 3.97/0.98 fof(f3025,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK5_skl)=high|has_endowment(sK2_skl)),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f3023,f82])).
% 3.97/0.98 fof(f3028,plain,(
% 3.97/0.98 ~greater(high,hazard_of_mortality(sK2_skl,sK4_skl))|~hazard_of_mortality(sK2_skl,sK4_skl)=low),
% 3.97/0.98 inference(backward_demodulation,[status(thm)],[f3029,f1886])).
% 3.97/0.98 fof(f3029,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK5_skl)=high),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f3025,f84])).
% 3.97/0.98 fof(f3782,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK4_skl)=low|~organization(sK2_skl)|has_endowment(sK2_skl)),
% 3.97/0.98 inference(resolution,[status(thm)],[f2603,f42])).
% 3.97/0.98 fof(f3784,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK4_skl)=low|has_endowment(sK2_skl)),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f3782,f82])).
% 3.97/0.98 fof(f3787,plain,(
% 3.97/0.98 ~greater(high,hazard_of_mortality(sK2_skl,sK4_skl))|~low=low),
% 3.97/0.98 inference(backward_demodulation,[status(thm)],[f3788,f3028])).
% 3.97/0.98 fof(f3788,plain,(
% 3.97/0.98 hazard_of_mortality(sK2_skl,sK4_skl)=low),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f3784,f84])).
% 3.97/0.98 fof(f3792,plain,(
% 3.97/0.98 ~greater(high,low)|~low=low),
% 3.97/0.98 inference(forward_demodulation,[status(thm)],[f3788,f3787])).
% 3.97/0.98 fof(f3793,plain,(
% 3.97/0.98 ~greater(high,low)),
% 3.97/0.98 inference(trivial_equality_resolution,[status(thm)],[f3792])).
% 3.97/0.98 fof(f3794,plain,(
% 3.97/0.98 $false),
% 3.97/0.98 inference(forward_subsumption_resolution,[status(thm)],[f3793,f141])).
% 3.97/0.98 % SZS output end CNFRefutation for theBenchmark.p
% 3.97/0.99 % Elapsed time: 0.614232 seconds
% 3.97/0.99 % CPU time: 4.531508 seconds
% 3.97/0.99 % Total memory used: 140.775 MB
% 3.97/0.99 % Net memory used: 134.474 MB
%------------------------------------------------------------------------------