%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT027+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:43 PM UTC 2026
% Result : Theorem 0.14s 5.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT027+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n026.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 01:25:13 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.39 % Drodi V4.1.1
% 0.14/5.42 % Refutation found
% 0.14/5.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.42 fof(f1,axiom,(
% 0.14/5.42 (! [E,To] :( ( environment(E)& stable(E)& in_environment(E,To)& (! [T] :( ( greater(cardinality_at_time(first_movers,T),zero)& greater_or_equal(T,To) )=> greater(zero,growth_rate(first_movers,T)) ) ))=> contracts_from(To,first_movers) ) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f2,axiom,(
% 0.14/5.42 (! [E,T] :( ( environment(E)& in_environment(E,T)& greater(cardinality_at_time(first_movers,T),zero)& greater(cardinality_at_time(efficient_producers,T),zero) )=> subpopulations(first_movers,efficient_producers,E,T) ) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f3,axiom,(
% 0.14/5.42 (! [E,T1,T2] :( ( environment(E)& stable(E)& in_environment(E,T1)& greater(T2,T1) )=> in_environment(E,T2) ) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f4,axiom,(
% 0.14/5.42 (! [E] :( ( environment(E)& stable(E) )=> in_environment(E,appear(efficient_producers,E)) ) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f5,axiom,(
% 0.14/5.42 (! [X,Y,Z] :( ( greater(X,Y)& greater(Y,Z) )=> greater(X,Z) ) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f6,axiom,(
% 0.14/5.42 (! [X,Y] :( greater_or_equal(X,Y)<=> ( greater(X,Y)| X = Y ) ) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f7,hypothesis,(
% 0.14/5.42 (! [E,T] :( ( environment(E)& in_environment(E,T)& greater_or_equal(T,appear(efficient_producers,E)) )=> greater(cardinality_at_time(efficient_producers,T),zero) ) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f8,hypothesis,(
% 0.14/5.42 (! [E] :( ( environment(E)& stable(E) )=> (? [To] :( greater(To,appear(efficient_producers,E))& (! [T] :( ( subpopulations(first_movers,efficient_producers,E,T)& greater_or_equal(T,To) )=> greater(zero,growth_rate(first_movers,T)) ) )) )) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f9,conjecture,(
% 0.14/5.42 (! [E] :( ( environment(E)& stable(E) )=> (? [To] :( greater(To,appear(efficient_producers,E))& contracts_from(To,first_movers) ) )) )),
% 0.14/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f10,negated_conjecture,(
% 0.14/5.42 ~((! [E] :( ( environment(E)& stable(E) )=> (? [To] :( greater(To,appear(efficient_producers,E))& contracts_from(To,first_movers) ) )) ))),
% 0.14/5.42 inference(negated_conjecture,[status(cth)],[f9])).
% 0.14/5.42 fof(f11,plain,(
% 0.14/5.42 ![E,To]: ((((~environment(E)|~stable(E))|~in_environment(E,To))|(?[T]: ((greater(cardinality_at_time(first_movers,T),zero)&greater_or_equal(T,To))&~greater(zero,growth_rate(first_movers,T)))))|contracts_from(To,first_movers))),
% 0.14/5.42 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.14/5.42 fof(f12,plain,(
% 0.14/5.42 ![To]: (((![E]: ((~environment(E)|~stable(E))|~in_environment(E,To)))|(?[T]: ((greater(cardinality_at_time(first_movers,T),zero)&greater_or_equal(T,To))&~greater(zero,growth_rate(first_movers,T)))))|contracts_from(To,first_movers))),
% 0.14/5.42 inference(miniscoping,[status(thm)],[f11])).
% 0.14/5.42 fof(f13,plain,(
% 0.14/5.42 ![To]: (((![E]: ((~environment(E)|~stable(E))|~in_environment(E,To)))|((greater(cardinality_at_time(first_movers,sK0_skl(To)),zero)&greater_or_equal(sK0_skl(To),To))&~greater(zero,growth_rate(first_movers,sK0_skl(To)))))|contracts_from(To,first_movers))),
% 0.14/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(T,sK0_skl(To))],[f12])).
% 0.14/5.42 fof(f14,plain,(
% 0.14/5.42 ![X0,X1]: (~environment(X0)|~stable(X0)|~in_environment(X0,X1)|greater(cardinality_at_time(first_movers,sK0_skl(X1)),zero)|contracts_from(X1,first_movers))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/5.42 fof(f15,plain,(
% 0.14/5.42 ![X0,X1]: (~environment(X0)|~stable(X0)|~in_environment(X0,X1)|greater_or_equal(sK0_skl(X1),X1)|contracts_from(X1,first_movers))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/5.42 fof(f16,plain,(
% 0.14/5.42 ![X0,X1]: (~environment(X0)|~stable(X0)|~in_environment(X0,X1)|~greater(zero,growth_rate(first_movers,sK0_skl(X1)))|contracts_from(X1,first_movers))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/5.42 fof(f17,plain,(
% 0.14/5.42 ![E,T]: ((((~environment(E)|~in_environment(E,T))|~greater(cardinality_at_time(first_movers,T),zero))|~greater(cardinality_at_time(efficient_producers,T),zero))|subpopulations(first_movers,efficient_producers,E,T))),
% 0.14/5.42 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/5.42 fof(f18,plain,(
% 0.14/5.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater(cardinality_at_time(first_movers,X1),zero)|~greater(cardinality_at_time(efficient_producers,X1),zero)|subpopulations(first_movers,efficient_producers,X0,X1))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.14/5.42 fof(f19,plain,(
% 0.14/5.42 ![E,T1,T2]: ((((~environment(E)|~stable(E))|~in_environment(E,T1))|~greater(T2,T1))|in_environment(E,T2))),
% 0.14/5.42 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/5.42 fof(f20,plain,(
% 0.14/5.42 ![E,T2]: ((![T1]: (((~environment(E)|~stable(E))|~in_environment(E,T1))|~greater(T2,T1)))|in_environment(E,T2))),
% 0.14/5.42 inference(miniscoping,[status(thm)],[f19])).
% 0.14/5.42 fof(f21,plain,(
% 0.14/5.42 ![X0,X1,X2]: (~environment(X0)|~stable(X0)|~in_environment(X0,X1)|~greater(X2,X1)|in_environment(X0,X2))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f20])).
% 0.14/5.42 fof(f22,plain,(
% 0.14/5.42 ![E]: ((~environment(E)|~stable(E))|in_environment(E,appear(efficient_producers,E)))),
% 0.14/5.42 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.14/5.42 fof(f23,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~stable(X0)|in_environment(X0,appear(efficient_producers,X0)))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/5.42 fof(f24,plain,(
% 0.14/5.42 ![X,Y,Z]: ((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))),
% 0.14/5.42 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.14/5.42 fof(f25,plain,(
% 0.14/5.42 ![X,Z]: ((![Y]: (~greater(X,Y)|~greater(Y,Z)))|greater(X,Z))),
% 0.14/5.42 inference(miniscoping,[status(thm)],[f24])).
% 0.14/5.42 fof(f26,plain,(
% 0.14/5.42 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f25])).
% 0.14/5.42 fof(f27,plain,(
% 0.14/5.42 ![X,Y]: ((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&(greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 0.14/5.42 inference(NNF_transformation,[status(thm)],[f6])).
% 0.14/5.42 fof(f28,plain,(
% 0.14/5.42 (![X,Y]: (~greater_or_equal(X,Y)|(greater(X,Y)|X=Y)))&(![X,Y]: (greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 0.14/5.42 inference(miniscoping,[status(thm)],[f27])).
% 0.14/5.42 fof(f29,plain,(
% 0.14/5.42 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/5.42 fof(f30,plain,(
% 0.14/5.42 ![X0,X1]: (greater_or_equal(X0,X1)|~greater(X0,X1))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/5.42 fof(f31,plain,(
% 0.14/5.42 ![X0,X1]: (greater_or_equal(X0,X1)|~X0=X1)),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/5.42 fof(f32,plain,(
% 0.14/5.42 ![E,T]: (((~environment(E)|~in_environment(E,T))|~greater_or_equal(T,appear(efficient_producers,E)))|greater(cardinality_at_time(efficient_producers,T),zero))),
% 0.14/5.42 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.14/5.42 fof(f33,plain,(
% 0.14/5.42 ![T]: ((![E]: ((~environment(E)|~in_environment(E,T))|~greater_or_equal(T,appear(efficient_producers,E))))|greater(cardinality_at_time(efficient_producers,T),zero))),
% 0.14/5.42 inference(miniscoping,[status(thm)],[f32])).
% 0.14/5.42 fof(f34,plain,(
% 0.14/5.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater_or_equal(X1,appear(efficient_producers,X0))|greater(cardinality_at_time(efficient_producers,X1),zero))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f33])).
% 0.14/5.42 fof(f35,plain,(
% 0.14/5.42 ![E]: ((~environment(E)|~stable(E))|(?[To]: (greater(To,appear(efficient_producers,E))&(![T]: ((~subpopulations(first_movers,efficient_producers,E,T)|~greater_or_equal(T,To))|greater(zero,growth_rate(first_movers,T)))))))),
% 0.14/5.42 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.14/5.42 fof(f36,plain,(
% 0.14/5.42 ![E]: ((~environment(E)|~stable(E))|(greater(sK1_skl(E),appear(efficient_producers,E))&(![T]: ((~subpopulations(first_movers,efficient_producers,E,T)|~greater_or_equal(T,sK1_skl(E)))|greater(zero,growth_rate(first_movers,T))))))),
% 0.14/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(To,sK1_skl(E))],[f35])).
% 0.14/5.42 fof(f37,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~stable(X0)|greater(sK1_skl(X0),appear(efficient_producers,X0)))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f36])).
% 0.14/5.42 fof(f38,plain,(
% 0.14/5.42 ![X0,X1]: (~environment(X0)|~stable(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,sK1_skl(X0))|greater(zero,growth_rate(first_movers,X1)))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f36])).
% 0.14/5.42 fof(f39,plain,(
% 0.14/5.42 (?[E]: ((environment(E)&stable(E))&(![To]: (~greater(To,appear(efficient_producers,E))|~contracts_from(To,first_movers)))))),
% 0.14/5.42 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.14/5.42 fof(f40,plain,(
% 0.14/5.42 ((environment(sK2_skl)&stable(sK2_skl))&(![To]: (~greater(To,appear(efficient_producers,sK2_skl))|~contracts_from(To,first_movers))))),
% 0.14/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(E,sK2_skl)],[f39])).
% 0.14/5.42 fof(f41,plain,(
% 0.14/5.42 environment(sK2_skl)),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f40])).
% 0.14/5.42 fof(f42,plain,(
% 0.14/5.42 stable(sK2_skl)),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f40])).
% 0.14/5.42 fof(f43,plain,(
% 0.14/5.42 ![X0]: (~greater(X0,appear(efficient_producers,sK2_skl))|~contracts_from(X0,first_movers))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f40])).
% 0.14/5.42 fof(f44,plain,(
% 0.14/5.42 ![X0]: (greater_or_equal(X0,X0))),
% 0.14/5.42 inference(destructive_equality_resolution,[status(thm)],[f31])).
% 0.14/5.42 fof(f45,plain,(
% 0.14/5.42 ~stable(sK2_skl)|in_environment(sK2_skl,appear(efficient_producers,sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f23,f41])).
% 0.14/5.42 fof(f46,plain,(
% 0.14/5.42 in_environment(sK2_skl,appear(efficient_producers,sK2_skl))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f45,f42])).
% 0.14/5.42 fof(f47,plain,(
% 0.14/5.42 ![X0]: (~environment(sK2_skl)|~stable(sK2_skl)|~greater(X0,appear(efficient_producers,sK2_skl))|in_environment(sK2_skl,X0))),
% 0.14/5.42 inference(resolution,[status(thm)],[f21,f46])).
% 0.14/5.42 fof(f48,plain,(
% 0.14/5.42 ![X0]: (~stable(sK2_skl)|~greater(X0,appear(efficient_producers,sK2_skl))|in_environment(sK2_skl,X0))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f47,f41])).
% 0.14/5.42 fof(f49,plain,(
% 0.14/5.42 ![X0]: (~greater(X0,appear(efficient_producers,sK2_skl))|in_environment(sK2_skl,X0))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f48,f42])).
% 0.14/5.42 fof(f62,plain,(
% 0.14/5.42 ~stable(sK2_skl)|greater(sK1_skl(sK2_skl),appear(efficient_producers,sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f37,f41])).
% 0.14/5.42 fof(f63,plain,(
% 0.14/5.42 greater(sK1_skl(sK2_skl),appear(efficient_producers,sK2_skl))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f62,f42])).
% 0.14/5.42 fof(f64,plain,(
% 0.14/5.42 in_environment(sK2_skl,sK1_skl(sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f63,f49])).
% 0.14/5.42 fof(f65,plain,(
% 0.14/5.42 ~contracts_from(sK1_skl(sK2_skl),first_movers)),
% 0.14/5.42 inference(resolution,[status(thm)],[f63,f43])).
% 0.14/5.42 fof(f66,plain,(
% 0.14/5.42 greater_or_equal(sK1_skl(sK2_skl),appear(efficient_producers,sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f63,f30])).
% 0.14/5.42 fof(f67,plain,(
% 0.14/5.42 ![X0]: (~greater(X0,sK1_skl(sK2_skl))|greater(X0,appear(efficient_producers,sK2_skl)))),
% 0.14/5.42 inference(resolution,[status(thm)],[f63,f26])).
% 0.14/5.42 fof(f68,plain,(
% 0.14/5.42 ~environment(sK2_skl)|~stable(sK2_skl)|greater(cardinality_at_time(first_movers,sK0_skl(sK1_skl(sK2_skl))),zero)|contracts_from(sK1_skl(sK2_skl),first_movers)),
% 0.14/5.42 inference(resolution,[status(thm)],[f64,f14])).
% 0.14/5.42 fof(f69,plain,(
% 0.14/5.42 ![X0]: (~environment(sK2_skl)|~stable(sK2_skl)|~greater(X0,sK1_skl(sK2_skl))|in_environment(sK2_skl,X0))),
% 0.14/5.42 inference(resolution,[status(thm)],[f64,f21])).
% 0.14/5.42 fof(f70,plain,(
% 0.14/5.42 ~stable(sK2_skl)|greater(cardinality_at_time(first_movers,sK0_skl(sK1_skl(sK2_skl))),zero)|contracts_from(sK1_skl(sK2_skl),first_movers)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f68,f41])).
% 0.14/5.42 fof(f71,plain,(
% 0.14/5.42 ![X0]: (~stable(sK2_skl)|~greater(X0,sK1_skl(sK2_skl))|in_environment(sK2_skl,X0))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f69,f41])).
% 0.14/5.42 fof(f72,plain,(
% 0.14/5.42 ~environment(sK2_skl)|~in_environment(sK2_skl,sK1_skl(sK2_skl))|greater(cardinality_at_time(efficient_producers,sK1_skl(sK2_skl)),zero)),
% 0.14/5.42 inference(resolution,[status(thm)],[f66,f34])).
% 0.14/5.42 fof(f74,plain,(
% 0.14/5.42 ~in_environment(sK2_skl,sK1_skl(sK2_skl))|greater(cardinality_at_time(efficient_producers,sK1_skl(sK2_skl)),zero)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f72,f41])).
% 0.14/5.42 fof(f75,plain,(
% 0.14/5.42 ![X0]: (~greater(X0,sK1_skl(sK2_skl))|in_environment(sK2_skl,X0))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f71,f42])).
% 0.14/5.42 fof(f76,plain,(
% 0.14/5.42 greater(cardinality_at_time(efficient_producers,sK1_skl(sK2_skl)),zero)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f74,f64])).
% 0.14/5.42 fof(f80,plain,(
% 0.14/5.42 ~environment(sK2_skl)|~stable(sK2_skl)|greater_or_equal(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|contracts_from(sK1_skl(sK2_skl),first_movers)),
% 0.14/5.42 inference(resolution,[status(thm)],[f15,f64])).
% 0.14/5.42 fof(f82,plain,(
% 0.14/5.42 ~stable(sK2_skl)|greater_or_equal(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|contracts_from(sK1_skl(sK2_skl),first_movers)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f80,f41])).
% 0.14/5.42 fof(f84,plain,(
% 0.14/5.42 greater_or_equal(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|contracts_from(sK1_skl(sK2_skl),first_movers)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f82,f42])).
% 0.14/5.42 fof(f85,plain,(
% 0.14/5.42 contracts_from(sK1_skl(sK2_skl),first_movers)|greater(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)),
% 0.14/5.42 inference(resolution,[status(thm)],[f84,f29])).
% 0.14/5.42 fof(f86,plain,(
% 0.14/5.42 greater(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f85,f65])).
% 0.14/5.42 fof(f87,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|in_environment(sK2_skl,sK0_skl(sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(resolution,[status(thm)],[f86,f75])).
% 0.14/5.42 fof(f88,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|greater(sK0_skl(sK1_skl(sK2_skl)),appear(efficient_producers,sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f86,f67])).
% 0.14/5.42 fof(f89,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|greater_or_equal(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f86,f30])).
% 0.14/5.42 fof(f102,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|greater_or_equal(sK0_skl(sK1_skl(sK2_skl)),appear(efficient_producers,sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f88,f30])).
% 0.14/5.42 fof(f104,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~environment(sK2_skl)|~in_environment(sK2_skl,sK0_skl(sK1_skl(sK2_skl)))|greater(cardinality_at_time(efficient_producers,sK0_skl(sK1_skl(sK2_skl))),zero)),
% 0.14/5.42 inference(resolution,[status(thm)],[f102,f34])).
% 0.14/5.42 fof(f106,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~in_environment(sK2_skl,sK0_skl(sK1_skl(sK2_skl)))|greater(cardinality_at_time(efficient_producers,sK0_skl(sK1_skl(sK2_skl))),zero)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f104,f41])).
% 0.14/5.42 fof(f108,plain,(
% 0.14/5.42 greater(cardinality_at_time(first_movers,sK0_skl(sK1_skl(sK2_skl))),zero)|contracts_from(sK1_skl(sK2_skl),first_movers)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f70,f42])).
% 0.14/5.42 fof(f109,plain,(
% 0.14/5.42 ![X0]: (contracts_from(sK1_skl(sK2_skl),first_movers)|~environment(X0)|~in_environment(X0,sK0_skl(sK1_skl(sK2_skl)))|~greater(cardinality_at_time(efficient_producers,sK0_skl(sK1_skl(sK2_skl))),zero)|subpopulations(first_movers,efficient_producers,X0,sK0_skl(sK1_skl(sK2_skl))))),
% 0.14/5.42 inference(resolution,[status(thm)],[f108,f18])).
% 0.14/5.42 fof(f112,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~in_environment(X0,sK0_skl(sK1_skl(sK2_skl)))|~greater(cardinality_at_time(efficient_producers,sK0_skl(sK1_skl(sK2_skl))),zero)|subpopulations(first_movers,efficient_producers,X0,sK0_skl(sK1_skl(sK2_skl))))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f109,f65])).
% 0.14/5.42 fof(f124,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|greater(cardinality_at_time(efficient_producers,sK0_skl(sK1_skl(sK2_skl))),zero)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f106,f87])).
% 0.14/5.42 fof(f128,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~in_environment(X0,sK0_skl(sK1_skl(sK2_skl)))|subpopulations(first_movers,efficient_producers,X0,sK0_skl(sK1_skl(sK2_skl)))|sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f112,f124])).
% 0.14/5.42 fof(f129,plain,(
% 0.14/5.42 ~environment(sK2_skl)|subpopulations(first_movers,efficient_producers,sK2_skl,sK0_skl(sK1_skl(sK2_skl)))|sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)),
% 0.14/5.42 inference(resolution,[status(thm)],[f128,f87])).
% 0.14/5.42 fof(f130,plain,(
% 0.14/5.42 ~environment(sK2_skl)|subpopulations(first_movers,efficient_producers,sK2_skl,sK0_skl(sK1_skl(sK2_skl)))|sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)),
% 0.14/5.42 inference(duplicate_literals_removal,[status(thm)],[f129])).
% 0.14/5.42 fof(f131,plain,(
% 0.14/5.42 subpopulations(first_movers,efficient_producers,sK2_skl,sK0_skl(sK1_skl(sK2_skl)))|sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f130,f41])).
% 0.14/5.42 fof(f132,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~environment(sK2_skl)|~stable(sK2_skl)|~greater_or_equal(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|greater(zero,growth_rate(first_movers,sK0_skl(sK1_skl(sK2_skl))))),
% 0.14/5.42 inference(resolution,[status(thm)],[f131,f38])).
% 0.14/5.42 fof(f133,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~stable(sK2_skl)|~greater_or_equal(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|greater(zero,growth_rate(first_movers,sK0_skl(sK1_skl(sK2_skl))))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f132,f41])).
% 0.14/5.42 fof(f157,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~greater_or_equal(sK0_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|greater(zero,growth_rate(first_movers,sK0_skl(sK1_skl(sK2_skl))))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f133,f42])).
% 0.14/5.42 fof(f158,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|greater(zero,growth_rate(first_movers,sK0_skl(sK1_skl(sK2_skl))))|sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)),
% 0.14/5.42 inference(resolution,[status(thm)],[f157,f89])).
% 0.14/5.42 fof(f160,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|greater(zero,growth_rate(first_movers,sK0_skl(sK1_skl(sK2_skl))))),
% 0.14/5.42 inference(duplicate_literals_removal,[status(thm)],[f158])).
% 0.14/5.42 fof(f162,plain,(
% 0.14/5.42 ![X0]: (sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~environment(X0)|~stable(X0)|~in_environment(X0,sK1_skl(sK2_skl))|contracts_from(sK1_skl(sK2_skl),first_movers))),
% 0.14/5.42 inference(resolution,[status(thm)],[f160,f16])).
% 0.14/5.42 fof(f165,plain,(
% 0.14/5.42 ![X0]: (sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~environment(X0)|~stable(X0)|~in_environment(X0,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f162,f65])).
% 0.14/5.42 fof(f166,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~environment(sK2_skl)|~stable(sK2_skl)),
% 0.14/5.42 inference(resolution,[status(thm)],[f165,f64])).
% 0.14/5.42 fof(f167,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~stable(sK2_skl)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f166,f41])).
% 0.14/5.42 fof(f176,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~in_environment(X0,sK0_skl(sK1_skl(sK2_skl)))|~greater(cardinality_at_time(efficient_producers,sK0_skl(sK1_skl(sK2_skl))),zero)|subpopulations(first_movers,efficient_producers,X0,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f194,f112])).
% 0.14/5.42 fof(f194,plain,(
% 0.14/5.42 sK0_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f167,f42])).
% 0.14/5.42 fof(f195,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~stable(X0)|~in_environment(X0,sK1_skl(sK2_skl))|~greater(zero,growth_rate(first_movers,sK1_skl(sK2_skl)))|contracts_from(sK1_skl(sK2_skl),first_movers))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f194,f16])).
% 0.14/5.42 fof(f196,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~in_environment(X0,sK1_skl(sK2_skl))|~greater(cardinality_at_time(efficient_producers,sK0_skl(sK1_skl(sK2_skl))),zero)|subpopulations(first_movers,efficient_producers,X0,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f194,f176])).
% 0.14/5.42 fof(f197,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~in_environment(X0,sK1_skl(sK2_skl))|~greater(cardinality_at_time(efficient_producers,sK1_skl(sK2_skl)),zero)|subpopulations(first_movers,efficient_producers,X0,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f194,f196])).
% 0.14/5.42 fof(f198,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~in_environment(X0,sK1_skl(sK2_skl))|subpopulations(first_movers,efficient_producers,X0,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f197,f76])).
% 0.14/5.42 fof(f201,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~stable(X0)|~in_environment(X0,sK1_skl(sK2_skl))|~greater(zero,growth_rate(first_movers,sK1_skl(sK2_skl))))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f195,f65])).
% 0.14/5.42 fof(f211,plain,(
% 0.14/5.42 ~environment(sK2_skl)|subpopulations(first_movers,efficient_producers,sK2_skl,sK1_skl(sK2_skl))),
% 0.14/5.42 inference(resolution,[status(thm)],[f198,f64])).
% 0.14/5.42 fof(f212,plain,(
% 0.14/5.42 subpopulations(first_movers,efficient_producers,sK2_skl,sK1_skl(sK2_skl))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f211,f41])).
% 0.14/5.42 fof(f213,plain,(
% 0.14/5.42 ~environment(sK2_skl)|~stable(sK2_skl)|~greater_or_equal(sK1_skl(sK2_skl),sK1_skl(sK2_skl))|greater(zero,growth_rate(first_movers,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(resolution,[status(thm)],[f212,f38])).
% 0.14/5.42 fof(f214,plain,(
% 0.14/5.42 ~stable(sK2_skl)|~greater_or_equal(sK1_skl(sK2_skl),sK1_skl(sK2_skl))|greater(zero,growth_rate(first_movers,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f213,f41])).
% 0.14/5.42 fof(f218,plain,(
% 0.14/5.42 ~greater_or_equal(sK1_skl(sK2_skl),sK1_skl(sK2_skl))|greater(zero,growth_rate(first_movers,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f214,f42])).
% 0.14/5.42 fof(f219,plain,(
% 0.14/5.42 greater(zero,growth_rate(first_movers,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(resolution,[status(thm)],[f218,f44])).
% 0.14/5.42 fof(f220,plain,(
% 0.14/5.42 ![X0]: (~environment(X0)|~stable(X0)|~in_environment(X0,sK1_skl(sK2_skl)))),
% 0.14/5.42 inference(backward_subsumption_resolution,[status(thm)],[f201,f219])).
% 0.14/5.42 fof(f224,plain,(
% 0.14/5.42 ~environment(sK2_skl)|~stable(sK2_skl)),
% 0.14/5.42 inference(resolution,[status(thm)],[f220,f64])).
% 0.14/5.42 fof(f225,plain,(
% 0.14/5.42 ~stable(sK2_skl)),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f224,f41])).
% 0.14/5.42 fof(f226,plain,(
% 0.14/5.42 $false),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f225,f42])).
% 0.14/5.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.44 % Elapsed time: 0.057985 seconds
% 0.14/5.44 % CPU time: 0.215542 seconds
% 0.14/5.44 % Total memory used: 79.607 MB
% 0.14/5.44 % Net memory used: 79.185 MB
%------------------------------------------------------------------------------