%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT037-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:46 PM UTC 2026
% Result : Unsatisfiable 0.14s 15.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT037-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/15.38 % Computer : n005.cluster.edu
% 0.10/15.38 % Model : x86_64 x86_64
% 0.10/15.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/15.38 % Memory : 8046.5625MB
% 0.10/15.38 % OS : Linux 6.8.0-71-generic
% 0.10/15.38 % CPULimit : 300
% 0.10/15.38 % WCLimit : 300
% 0.10/15.38 % DateTime : Mon Sep 21 01:23:18 UTC 2026
% 0.10/15.38 % CPUTime :
% 0.10/15.39 % Drodi V4.1.1
% 0.14/15.42 % Refutation found
% 0.14/15.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/15.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/15.42 fof(f1,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ greater_or_equal(B,appear(efficient_producers,A))| cardinality_at_time(efficient_producers,B) != zero| greater(sk1(B,A),appear(efficient_producers,A)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f2,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ greater_or_equal(B,appear(efficient_producers,A))| cardinality_at_time(efficient_producers,B) != zero| in_environment(A,sk1(B,A)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f3,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ greater_or_equal(B,appear(efficient_producers,A))| cardinality_at_time(efficient_producers,B) != zero| greater(B,sk1(B,A)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f4,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ greater_or_equal(B,appear(efficient_producers,A))| cardinality_at_time(efficient_producers,B) != zero| greater(zero,growth_rate(efficient_producers,sk1(B,A))) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f5,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| ~ greater(appear(an_organisation,A),B)| number_of_organizations(A,B) = zero ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f6,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| decreases(number_of_organizations(A,B))| subpopulation(sk2(B,A),A,B) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f7,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| decreases(number_of_organizations(A,B))| greater(cardinality_at_time(sk2(B,A),B),zero) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f8,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| decreases(number_of_organizations(A,B))| ~ greater(zero,growth_rate(sk2(B,A),B)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f9,axiom,(
% 0.14/15.42 (![A,B,C]: (( ~ environment(A)| ~ in_environment(A,B)| number_of_organizations(A,B) != zero| ~ subpopulation(C,A,B)| cardinality_at_time(C,B) = zero ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f10,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| subpopulation(first_movers,A,B) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f11,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| subpopulation(efficient_producers,A,B) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f12,axiom,(
% 0.14/15.42 (![A,B]: (( cardinality_at_time(A,B) != zero| ~ greater(zero,growth_rate(A,B)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f13,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| cardinality_at_time(efficient_producers,B) = zero| greater(cardinality_at_time(efficient_producers,B),zero) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f14,axiom,(
% 0.14/15.42 (![A]: (( ~ constant(A)| ~ decreases(A) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f15,axiom,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| greater_or_equal(B,appear(an_organisation,A))| greater(appear(an_organisation,A),B) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f16,hypothesis,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| ~ greater(number_of_organizations(A,B),zero)| ~ greater(equilibrium(A),B)| decreases(resources(A,B)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f17,hypothesis,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| ~ greater(number_of_organizations(A,B),zero)| greater(equilibrium(A),B)| constant(resources(A,B)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f18,hypothesis,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| ~ greater_or_equal(B,appear(an_organisation,A))| greater(number_of_organizations(A,B),zero) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f19,hypothesis,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| ~ decreases(resources(A,B))| ~ decreases(number_of_organizations(A,B)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f20,hypothesis,(
% 0.14/15.42 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| ~ constant(resources(A,B))| constant(number_of_organizations(A,B)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f21,hypothesis,(
% 0.14/15.42 (![A,B,C,D]: (( ~ environment(A)| ~ in_environment(A,B)| greater(zero,growth_rate(C,B))| ~ greater(resilience(D),resilience(C))| ~ greater(zero,growth_rate(D,B)) ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f22,hypothesis,(
% 0.14/15.42 greater(resilience(efficient_producers),resilience(first_movers)) ),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f23,hypothesis,(
% 0.14/15.42 (![A,B,C]: (( ~ environment(A)| ~ subpopulation(B,A,C)| ~ greater(cardinality_at_time(B,C),zero)| B = efficient_producers| B = first_movers ) ))),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f24,negated_conjecture,(
% 0.14/15.42 environment(sk3) ),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f25,negated_conjecture,(
% 0.14/15.42 in_environment(sk3,sk4) ),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f26,negated_conjecture,(
% 0.14/15.42 greater_or_equal(sk4,appear(efficient_producers,sk3)) ),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f27,negated_conjecture,(
% 0.14/15.42 ~ greater(cardinality_at_time(efficient_producers,sk4),zero) ),
% 0.14/15.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/15.42 fof(f28,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~greater_or_equal(X1,appear(efficient_producers,X0))|~cardinality_at_time(efficient_producers,X1)=zero|greater(sk1(X1,X0),appear(efficient_producers,X0)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/15.42 fof(f29,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~greater_or_equal(X1,appear(efficient_producers,X0))|~cardinality_at_time(efficient_producers,X1)=zero|in_environment(X0,sk1(X1,X0)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/15.42 fof(f30,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~greater_or_equal(X1,appear(efficient_producers,X0))|~cardinality_at_time(efficient_producers,X1)=zero|greater(X1,sk1(X1,X0)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/15.42 fof(f31,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~greater_or_equal(X1,appear(efficient_producers,X0))|~cardinality_at_time(efficient_producers,X1)=zero|greater(zero,growth_rate(efficient_producers,sk1(X1,X0))))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/15.42 fof(f32,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater(appear(an_organisation,X0),X1)|number_of_organizations(X0,X1)=zero)),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/15.42 fof(f33,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|decreases(number_of_organizations(X0,X1))|subpopulation(sk2(X1,X0),X0,X1))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/15.42 fof(f34,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|decreases(number_of_organizations(X0,X1))|greater(cardinality_at_time(sk2(X1,X0),X1),zero))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/15.42 fof(f35,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|decreases(number_of_organizations(X0,X1))|~greater(zero,growth_rate(sk2(X1,X0),X1)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/15.42 fof(f36,plain,(
% 0.14/15.42 ![B,C]: ((![A]: (((~environment(A)|~in_environment(A,B))|~number_of_organizations(A,B)=zero)|~subpopulation(C,A,B)))|cardinality_at_time(C,B)=zero)),
% 0.14/15.42 inference(miniscoping,[status(thm)],[f9])).
% 0.14/15.42 fof(f37,plain,(
% 0.14/15.42 ![X0,X1,X2]: (~environment(X0)|~in_environment(X0,X1)|~number_of_organizations(X0,X1)=zero|~subpopulation(X2,X0,X1)|cardinality_at_time(X2,X1)=zero)),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f36])).
% 0.14/15.42 fof(f38,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|subpopulation(first_movers,X0,X1))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f10])).
% 0.14/15.42 fof(f39,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|subpopulation(efficient_producers,X0,X1))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f11])).
% 0.14/15.42 fof(f40,plain,(
% 0.14/15.42 ![X0,X1]: (~cardinality_at_time(X0,X1)=zero|~greater(zero,growth_rate(X0,X1)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/15.42 fof(f41,plain,(
% 0.14/15.42 ![B]: (((![A]: (~environment(A)|~in_environment(A,B)))|cardinality_at_time(efficient_producers,B)=zero)|greater(cardinality_at_time(efficient_producers,B),zero))),
% 0.14/15.42 inference(miniscoping,[status(thm)],[f13])).
% 0.14/15.42 fof(f42,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|cardinality_at_time(efficient_producers,X1)=zero|greater(cardinality_at_time(efficient_producers,X1),zero))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/15.42 fof(f43,plain,(
% 0.14/15.42 ![X0]: (~constant(X0)|~decreases(X0))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f14])).
% 0.14/15.42 fof(f44,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|greater_or_equal(X1,appear(an_organisation,X0))|greater(appear(an_organisation,X0),X1))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.14/15.42 fof(f45,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater(number_of_organizations(X0,X1),zero)|~greater(equilibrium(X0),X1)|decreases(resources(X0,X1)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f16])).
% 0.14/15.42 fof(f46,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater(number_of_organizations(X0,X1),zero)|greater(equilibrium(X0),X1)|constant(resources(X0,X1)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.14/15.42 fof(f47,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater_or_equal(X1,appear(an_organisation,X0))|greater(number_of_organizations(X0,X1),zero))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f18])).
% 0.14/15.42 fof(f48,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~decreases(resources(X0,X1))|~decreases(number_of_organizations(X0,X1)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/15.42 fof(f49,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~constant(resources(X0,X1))|constant(number_of_organizations(X0,X1)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f20])).
% 0.14/15.42 fof(f50,plain,(
% 0.14/15.42 ![B,D]: ((![C]: (((![A]: (~environment(A)|~in_environment(A,B)))|greater(zero,growth_rate(C,B)))|~greater(resilience(D),resilience(C))))|~greater(zero,growth_rate(D,B)))),
% 0.14/15.42 inference(miniscoping,[status(thm)],[f21])).
% 0.14/15.42 fof(f51,plain,(
% 0.14/15.42 ![X0,X1,X2,X3]: (~environment(X0)|~in_environment(X0,X1)|greater(zero,growth_rate(X2,X1))|~greater(resilience(X3),resilience(X2))|~greater(zero,growth_rate(X3,X1)))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/15.42 fof(f52,plain,(
% 0.14/15.42 greater(resilience(efficient_producers),resilience(first_movers))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/15.42 fof(f53,plain,(
% 0.14/15.42 ![B]: (((![C]: ((![A]: (~environment(A)|~subpopulation(B,A,C)))|~greater(cardinality_at_time(B,C),zero)))|B=efficient_producers)|B=first_movers)),
% 0.14/15.42 inference(miniscoping,[status(thm)],[f23])).
% 0.14/15.42 fof(f54,plain,(
% 0.14/15.42 ![X0,X1,X2]: (~environment(X0)|~subpopulation(X1,X0,X2)|~greater(cardinality_at_time(X1,X2),zero)|X1=efficient_producers|X1=first_movers)),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f53])).
% 0.14/15.42 fof(f55,plain,(
% 0.14/15.42 environment(sk3)),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/15.42 fof(f56,plain,(
% 0.14/15.42 in_environment(sk3,sk4)),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f25])).
% 0.14/15.42 fof(f57,plain,(
% 0.14/15.42 greater_or_equal(sk4,appear(efficient_producers,sk3))),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f26])).
% 0.14/15.42 fof(f58,plain,(
% 0.14/15.42 ~greater(cardinality_at_time(efficient_producers,sk4),zero)),
% 0.14/15.42 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/15.42 fof(f59,plain,(
% 0.14/15.42 ~environment(sk3)|cardinality_at_time(efficient_producers,sk4)=zero|greater(cardinality_at_time(efficient_producers,sk4),zero)),
% 0.14/15.42 inference(resolution,[status(thm)],[f42,f56])).
% 0.14/15.42 fof(f60,definition,(
% 0.14/15.42 sQ0_spl <=> (environment(sk3))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f62,plain,(
% 0.14/15.42 ~environment(sk3)|sQ0_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f60])).
% 0.14/15.42 fof(f63,definition,(
% 0.14/15.42 sQ1_spl <=> (cardinality_at_time(efficient_producers,sk4)=zero)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f64,plain,(
% 0.14/15.42 cardinality_at_time(efficient_producers,sk4)=zero|~sQ1_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f63])).
% 0.14/15.42 fof(f66,definition,(
% 0.14/15.42 sQ2_spl <=> (greater(cardinality_at_time(efficient_producers,sk4),zero))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f67,plain,(
% 0.14/15.42 greater(cardinality_at_time(efficient_producers,sk4),zero)|~sQ2_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f66])).
% 0.14/15.42 fof(f69,plain,(
% 0.14/15.42 ~sQ0_spl|sQ1_spl|sQ2_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f59,f60,f63,f66])).
% 0.14/15.42 fof(f70,plain,(
% 0.14/15.42 $false|~sQ2_spl),
% 0.14/15.42 inference(forward_subsumption_resolution,[status(thm)],[f67,f58])).
% 0.14/15.42 fof(f71,plain,(
% 0.14/15.42 ~sQ2_spl),
% 0.14/15.42 inference(contradiction_clause,[status(thm)],[f70])).
% 0.14/15.42 fof(f72,plain,(
% 0.14/15.42 $false|sQ0_spl),
% 0.14/15.42 inference(forward_subsumption_resolution,[status(thm)],[f62,f55])).
% 0.14/15.42 fof(f73,plain,(
% 0.14/15.42 sQ0_spl),
% 0.14/15.42 inference(contradiction_clause,[status(thm)],[f72])).
% 0.14/15.42 fof(f74,plain,(
% 0.14/15.42 ~greater(zero,zero)|~sQ1_spl),
% 0.14/15.42 inference(backward_demodulation,[status(thm)],[f64,f58])).
% 0.14/15.42 fof(f75,plain,(
% 0.14/15.42 ~environment(sk3)|~cardinality_at_time(efficient_producers,sk4)=zero|greater(sk1(sk4,sk3),appear(efficient_producers,sk3))),
% 0.14/15.42 inference(resolution,[status(thm)],[f28,f57])).
% 0.14/15.42 fof(f76,definition,(
% 0.14/15.42 sQ3_spl <=> (greater(sk1(sk4,sk3),appear(efficient_producers,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f79,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ1_spl|sQ3_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f75,f60,f63,f76])).
% 0.14/15.42 fof(f80,plain,(
% 0.14/15.42 ~environment(sk3)|subpopulation(first_movers,sk3,sk4)),
% 0.14/15.42 inference(resolution,[status(thm)],[f38,f56])).
% 0.14/15.42 fof(f81,definition,(
% 0.14/15.42 sQ4_spl <=> (subpopulation(first_movers,sk3,sk4))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f82,plain,(
% 0.14/15.42 subpopulation(first_movers,sk3,sk4)|~sQ4_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f81])).
% 0.14/15.42 fof(f84,plain,(
% 0.14/15.42 ~sQ0_spl|sQ4_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f80,f60,f81])).
% 0.14/15.42 fof(f85,plain,(
% 0.14/15.42 ~environment(sk3)|~cardinality_at_time(efficient_producers,sk4)=zero|in_environment(sk3,sk1(sk4,sk3))),
% 0.14/15.42 inference(resolution,[status(thm)],[f29,f57])).
% 0.14/15.42 fof(f86,definition,(
% 0.14/15.42 sQ5_spl <=> (in_environment(sk3,sk1(sk4,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f87,plain,(
% 0.14/15.42 in_environment(sk3,sk1(sk4,sk3))|~sQ5_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f86])).
% 0.14/15.42 fof(f89,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ1_spl|sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f85,f60,f63,f86])).
% 0.14/15.42 fof(f90,plain,(
% 0.14/15.42 ~environment(sk3)|~cardinality_at_time(efficient_producers,sk4)=zero|greater(sk4,sk1(sk4,sk3))),
% 0.14/15.42 inference(resolution,[status(thm)],[f30,f57])).
% 0.14/15.42 fof(f91,definition,(
% 0.14/15.42 sQ6_spl <=> (greater(sk4,sk1(sk4,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f94,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ1_spl|sQ6_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f90,f60,f63,f91])).
% 0.14/15.42 fof(f95,plain,(
% 0.14/15.42 ~environment(sk3)|~cardinality_at_time(efficient_producers,sk4)=zero|greater(zero,growth_rate(efficient_producers,sk1(sk4,sk3)))),
% 0.14/15.42 inference(resolution,[status(thm)],[f31,f57])).
% 0.14/15.42 fof(f96,definition,(
% 0.14/15.42 sQ7_spl <=> (greater(zero,growth_rate(efficient_producers,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f97,plain,(
% 0.14/15.42 greater(zero,growth_rate(efficient_producers,sk1(sk4,sk3)))|~sQ7_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f96])).
% 0.14/15.42 fof(f99,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ1_spl|sQ7_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f95,f60,f63,f96])).
% 0.14/15.42 fof(f100,plain,(
% 0.14/15.42 ~environment(sk3)|decreases(number_of_organizations(sk3,sk4))|subpopulation(sk2(sk4,sk3),sk3,sk4)),
% 0.14/15.42 inference(resolution,[status(thm)],[f33,f56])).
% 0.14/15.42 fof(f101,definition,(
% 0.14/15.42 sQ8_spl <=> (decreases(number_of_organizations(sk3,sk4)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f104,definition,(
% 0.14/15.42 sQ9_spl <=> (subpopulation(sk2(sk4,sk3),sk3,sk4))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f105,plain,(
% 0.14/15.42 subpopulation(sk2(sk4,sk3),sk3,sk4)|~sQ9_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f104])).
% 0.14/15.42 fof(f107,plain,(
% 0.14/15.42 ~sQ0_spl|sQ8_spl|sQ9_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f100,f60,f101,f104])).
% 0.14/15.42 fof(f108,plain,(
% 0.14/15.42 ~environment(sk3)|decreases(number_of_organizations(sk3,sk4))|greater(cardinality_at_time(sk2(sk4,sk3),sk4),zero)),
% 0.14/15.42 inference(resolution,[status(thm)],[f34,f56])).
% 0.14/15.42 fof(f109,definition,(
% 0.14/15.42 sQ10_spl <=> (greater(cardinality_at_time(sk2(sk4,sk3),sk4),zero))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f110,plain,(
% 0.14/15.42 greater(cardinality_at_time(sk2(sk4,sk3),sk4),zero)|~sQ10_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f109])).
% 0.14/15.42 fof(f112,plain,(
% 0.14/15.42 ~sQ0_spl|sQ8_spl|sQ10_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f108,f60,f101,f109])).
% 0.14/15.42 fof(f113,plain,(
% 0.14/15.42 ~environment(sk3)|decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|greater(cardinality_at_time(sk2(sk1(sk4,sk3),sk3),sk1(sk4,sk3)),zero)|~sQ5_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f87,f34])).
% 0.14/15.42 fof(f114,plain,(
% 0.14/15.42 ~environment(sk3)|decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|subpopulation(sk2(sk1(sk4,sk3),sk3),sk3,sk1(sk4,sk3))|~sQ5_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f87,f33])).
% 0.14/15.42 fof(f115,plain,(
% 0.14/15.42 ~environment(sk3)|subpopulation(first_movers,sk3,sk1(sk4,sk3))|~sQ5_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f87,f38])).
% 0.14/15.42 fof(f116,plain,(
% 0.14/15.42 ~environment(sk3)|cardinality_at_time(efficient_producers,sk1(sk4,sk3))=zero|greater(cardinality_at_time(efficient_producers,sk1(sk4,sk3)),zero)|~sQ5_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f87,f42])).
% 0.14/15.42 fof(f117,definition,(
% 0.14/15.42 sQ11_spl <=> (decreases(number_of_organizations(sk3,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f118,plain,(
% 0.14/15.42 decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|~sQ11_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f117])).
% 0.14/15.42 fof(f120,definition,(
% 0.14/15.42 sQ12_spl <=> (greater(cardinality_at_time(sk2(sk1(sk4,sk3),sk3),sk1(sk4,sk3)),zero))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f121,plain,(
% 0.14/15.42 greater(cardinality_at_time(sk2(sk1(sk4,sk3),sk3),sk1(sk4,sk3)),zero)|~sQ12_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f120])).
% 0.14/15.42 fof(f123,plain,(
% 0.14/15.42 ~sQ0_spl|sQ11_spl|sQ12_spl|~sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f113,f60,f117,f120,f86])).
% 0.14/15.42 fof(f124,definition,(
% 0.14/15.42 sQ13_spl <=> (subpopulation(sk2(sk1(sk4,sk3),sk3),sk3,sk1(sk4,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f125,plain,(
% 0.14/15.42 subpopulation(sk2(sk1(sk4,sk3),sk3),sk3,sk1(sk4,sk3))|~sQ13_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f124])).
% 0.14/15.42 fof(f127,plain,(
% 0.14/15.42 ~sQ0_spl|sQ11_spl|sQ13_spl|~sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f114,f60,f117,f124,f86])).
% 0.14/15.42 fof(f128,definition,(
% 0.14/15.42 sQ14_spl <=> (subpopulation(first_movers,sk3,sk1(sk4,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f131,plain,(
% 0.14/15.42 ~sQ0_spl|sQ14_spl|~sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f115,f60,f128,f86])).
% 0.14/15.42 fof(f132,definition,(
% 0.14/15.42 sQ15_spl <=> (cardinality_at_time(efficient_producers,sk1(sk4,sk3))=zero)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f133,plain,(
% 0.14/15.42 cardinality_at_time(efficient_producers,sk1(sk4,sk3))=zero|~sQ15_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f132])).
% 0.14/15.42 fof(f135,definition,(
% 0.14/15.42 sQ16_spl <=> (greater(cardinality_at_time(efficient_producers,sk1(sk4,sk3)),zero))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f138,plain,(
% 0.14/15.42 ~sQ0_spl|sQ15_spl|sQ16_spl|~sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f116,f60,f132,f135,f86])).
% 0.14/15.42 fof(f139,plain,(
% 0.14/15.42 ~environment(sk3)|subpopulation(efficient_producers,sk3,sk1(sk4,sk3))|~sQ5_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f39,f87])).
% 0.14/15.42 fof(f140,plain,(
% 0.14/15.42 ~environment(sk3)|subpopulation(efficient_producers,sk3,sk4)),
% 0.14/15.42 inference(resolution,[status(thm)],[f39,f56])).
% 0.14/15.42 fof(f141,definition,(
% 0.14/15.42 sQ17_spl <=> (subpopulation(efficient_producers,sk3,sk1(sk4,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f142,plain,(
% 0.14/15.42 subpopulation(efficient_producers,sk3,sk1(sk4,sk3))|~sQ17_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f141])).
% 0.14/15.42 fof(f144,plain,(
% 0.14/15.42 ~sQ0_spl|sQ17_spl|~sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f139,f60,f141,f86])).
% 0.14/15.42 fof(f145,definition,(
% 0.14/15.42 sQ18_spl <=> (subpopulation(efficient_producers,sk3,sk4))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f146,plain,(
% 0.14/15.42 subpopulation(efficient_producers,sk3,sk4)|~sQ18_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f145])).
% 0.14/15.42 fof(f148,plain,(
% 0.14/15.42 ~sQ0_spl|sQ18_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f140,f60,f145])).
% 0.14/15.42 fof(f149,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|~number_of_organizations(sk3,sk1(sk4,sk3))=zero|cardinality_at_time(efficient_producers,sk1(sk4,sk3))=zero|~sQ17_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f37,f142])).
% 0.14/15.42 fof(f152,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk4)|~number_of_organizations(sk3,sk4)=zero|cardinality_at_time(first_movers,sk4)=zero|~sQ4_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f37,f82])).
% 0.14/15.42 fof(f153,definition,(
% 0.14/15.42 sQ19_spl <=> (number_of_organizations(sk3,sk1(sk4,sk3))=zero)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f156,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|~sQ19_spl|sQ15_spl|~sQ17_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f149,f60,f86,f153,f132,f141])).
% 0.14/15.42 fof(f157,definition,(
% 0.14/15.42 sQ20_spl <=> (in_environment(sk3,sk4))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f159,plain,(
% 0.14/15.42 ~in_environment(sk3,sk4)|sQ20_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f157])).
% 0.14/15.42 fof(f160,definition,(
% 0.14/15.42 sQ21_spl <=> (number_of_organizations(sk3,sk4)=zero)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f168,definition,(
% 0.14/15.42 sQ23_spl <=> (cardinality_at_time(first_movers,sk4)=zero)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f171,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ20_spl|~sQ21_spl|sQ23_spl|~sQ4_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f152,f60,f157,f160,f168,f81])).
% 0.14/15.42 fof(f172,plain,(
% 0.14/15.42 ~cardinality_at_time(efficient_producers,sk1(sk4,sk3))=zero|~sQ7_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f40,f97])).
% 0.14/15.42 fof(f173,plain,(
% 0.14/15.42 ~zero=zero|~sQ15_spl|~sQ7_spl),
% 0.14/15.42 inference(forward_demodulation,[status(thm)],[f133,f172])).
% 0.14/15.42 fof(f174,plain,(
% 0.14/15.42 $false|~sQ15_spl|~sQ7_spl),
% 0.14/15.42 inference(trivial_equality_resolution,[status(thm)],[f173])).
% 0.14/15.42 fof(f175,plain,(
% 0.14/15.42 ~sQ15_spl|~sQ7_spl),
% 0.14/15.42 inference(contradiction_clause,[status(thm)],[f174])).
% 0.14/15.42 fof(f176,plain,(
% 0.14/15.42 ~environment(sk3)|greater_or_equal(sk1(sk4,sk3),appear(an_organisation,sk3))|greater(appear(an_organisation,sk3),sk1(sk4,sk3))|~sQ5_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f44,f87])).
% 0.14/15.42 fof(f177,plain,(
% 0.14/15.42 ~environment(sk3)|greater_or_equal(sk4,appear(an_organisation,sk3))|greater(appear(an_organisation,sk3),sk4)),
% 0.14/15.42 inference(resolution,[status(thm)],[f44,f56])).
% 0.14/15.42 fof(f178,definition,(
% 0.14/15.42 sQ24_spl <=> (greater_or_equal(sk1(sk4,sk3),appear(an_organisation,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f179,plain,(
% 0.14/15.42 greater_or_equal(sk1(sk4,sk3),appear(an_organisation,sk3))|~sQ24_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f178])).
% 0.14/15.42 fof(f181,definition,(
% 0.14/15.42 sQ25_spl <=> (greater(appear(an_organisation,sk3),sk1(sk4,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f182,plain,(
% 0.14/15.42 greater(appear(an_organisation,sk3),sk1(sk4,sk3))|~sQ25_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f181])).
% 0.14/15.42 fof(f184,plain,(
% 0.14/15.42 ~sQ0_spl|sQ24_spl|sQ25_spl|~sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f176,f60,f178,f181,f86])).
% 0.14/15.42 fof(f185,definition,(
% 0.14/15.42 sQ26_spl <=> (greater_or_equal(sk4,appear(an_organisation,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f186,plain,(
% 0.14/15.42 greater_or_equal(sk4,appear(an_organisation,sk3))|~sQ26_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f185])).
% 0.14/15.42 fof(f188,definition,(
% 0.14/15.42 sQ27_spl <=> (greater(appear(an_organisation,sk3),sk4))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f189,plain,(
% 0.14/15.42 greater(appear(an_organisation,sk3),sk4)|~sQ27_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f188])).
% 0.14/15.42 fof(f191,plain,(
% 0.14/15.42 ~sQ0_spl|sQ26_spl|sQ27_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f177,f60,f185,f188])).
% 0.14/15.42 fof(f192,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk4)|greater(number_of_organizations(sk3,sk4),zero)|~sQ26_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f186,f47])).
% 0.14/15.42 fof(f193,definition,(
% 0.14/15.42 sQ28_spl <=> (greater(number_of_organizations(sk3,sk4),zero))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f194,plain,(
% 0.14/15.42 greater(number_of_organizations(sk3,sk4),zero)|~sQ28_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f193])).
% 0.14/15.42 fof(f196,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ20_spl|sQ28_spl|~sQ26_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f192,f60,f157,f193,f185])).
% 0.14/15.42 fof(f197,plain,(
% 0.14/15.42 $false|sQ20_spl),
% 0.14/15.42 inference(forward_subsumption_resolution,[status(thm)],[f159,f56])).
% 0.14/15.42 fof(f198,plain,(
% 0.14/15.42 sQ20_spl),
% 0.14/15.42 inference(contradiction_clause,[status(thm)],[f197])).
% 0.14/15.42 fof(f199,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk4)|number_of_organizations(sk3,sk4)=zero|~sQ27_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f189,f32])).
% 0.14/15.42 fof(f200,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ20_spl|sQ21_spl|~sQ27_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f199,f60,f157,f160,f188])).
% 0.14/15.42 fof(f201,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk4)|greater(equilibrium(sk3),sk4)|constant(resources(sk3,sk4))|~sQ28_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f194,f46])).
% 0.14/15.42 fof(f202,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk4)|~greater(equilibrium(sk3),sk4)|decreases(resources(sk3,sk4))|~sQ28_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f194,f45])).
% 0.14/15.42 fof(f203,definition,(
% 0.14/15.42 sQ29_spl <=> (greater(equilibrium(sk3),sk4))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f206,definition,(
% 0.14/15.42 sQ30_spl <=> (constant(resources(sk3,sk4)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f207,plain,(
% 0.14/15.42 constant(resources(sk3,sk4))|~sQ30_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f206])).
% 0.14/15.42 fof(f209,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ20_spl|sQ29_spl|sQ30_spl|~sQ28_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f201,f60,f157,f203,f206,f193])).
% 0.14/15.42 fof(f210,definition,(
% 0.14/15.42 sQ31_spl <=> (decreases(resources(sk3,sk4)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f211,plain,(
% 0.14/15.42 decreases(resources(sk3,sk4))|~sQ31_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f210])).
% 0.14/15.42 fof(f213,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ20_spl|~sQ29_spl|sQ31_spl|~sQ28_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f202,f60,f157,f203,f210,f193])).
% 0.14/15.42 fof(f216,plain,(
% 0.14/15.42 ~decreases(resources(sk3,sk4))|~sQ30_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f207,f43])).
% 0.14/15.42 fof(f217,plain,(
% 0.14/15.42 $false|~sQ31_spl|~sQ30_spl),
% 0.14/15.42 inference(forward_subsumption_resolution,[status(thm)],[f216,f211])).
% 0.14/15.42 fof(f218,plain,(
% 0.14/15.42 ~sQ31_spl|~sQ30_spl),
% 0.14/15.42 inference(contradiction_clause,[status(thm)],[f217])).
% 0.14/15.42 fof(f219,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk4)|~decreases(number_of_organizations(sk3,sk4))|~sQ31_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f48,f211])).
% 0.14/15.42 fof(f220,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ20_spl|~sQ8_spl|~sQ31_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f219,f60,f157,f101,f210])).
% 0.14/15.42 fof(f221,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|greater(zero,growth_rate(first_movers,X1))|~greater(zero,growth_rate(efficient_producers,X1)))),
% 0.14/15.42 inference(resolution,[status(thm)],[f51,f52])).
% 0.14/15.42 fof(f222,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,sk1(sk4,sk3))|greater(zero,growth_rate(X1,sk1(sk4,sk3)))|~greater(resilience(efficient_producers),resilience(X1))|~sQ7_spl)),
% 0.14/15.42 inference(resolution,[status(thm)],[f51,f97])).
% 0.14/15.42 fof(f223,definition,(
% 0.14/15.42 ![X0]: (sQ32_spl <=> (~environment(X0)|~in_environment(X0,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f224,plain,(
% 0.14/15.42 ![X0]: (~environment(X0)|~in_environment(X0,sk1(sk4,sk3))|~sQ32_spl)),
% 0.14/15.42 inference(component_clause,[status(thm)],[f223])).
% 0.14/15.42 fof(f226,definition,(
% 0.14/15.42 ![X1]: (sQ33_spl <=> (greater(zero,growth_rate(X1,sk1(sk4,sk3)))|~greater(resilience(efficient_producers),resilience(X1))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f229,plain,(
% 0.14/15.42 sQ32_spl|sQ33_spl|~sQ7_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f222,f223,f226,f96])).
% 0.14/15.42 fof(f232,definition,(
% 0.14/15.42 ![X0]: (sQ34_spl <=> (~environment(X0)|~subpopulation(efficient_producers,X0,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f233,plain,(
% 0.14/15.42 ![X0]: (~environment(X0)|~subpopulation(efficient_producers,X0,sk1(sk4,sk3))|~sQ34_spl)),
% 0.14/15.42 inference(component_clause,[status(thm)],[f232])).
% 0.14/15.42 fof(f242,definition,(
% 0.14/15.42 ![X0]: (sQ37_spl <=> (~environment(X0)|~subpopulation(efficient_producers,X0,sk4)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f243,plain,(
% 0.14/15.42 ![X0]: (~environment(X0)|~subpopulation(efficient_producers,X0,sk4)|~sQ37_spl)),
% 0.14/15.42 inference(component_clause,[status(thm)],[f242])).
% 0.14/15.42 fof(f264,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk4)|~number_of_organizations(sk3,sk4)=zero|cardinality_at_time(sk2(sk4,sk3),sk4)=zero|~sQ9_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f105,f37])).
% 0.14/15.42 fof(f265,definition,(
% 0.14/15.42 sQ39_spl <=> (cardinality_at_time(sk2(sk4,sk3),sk4)=zero)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f268,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ20_spl|~sQ21_spl|sQ39_spl|~sQ9_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f264,f60,f157,f160,f265,f104])).
% 0.14/15.42 fof(f269,plain,(
% 0.14/15.42 ![X0]: (~environment(X0)|~subpopulation(sk2(sk4,sk3),X0,sk4)|sk2(sk4,sk3)=efficient_producers|sk2(sk4,sk3)=first_movers|~sQ10_spl)),
% 0.14/15.42 inference(resolution,[status(thm)],[f110,f54])).
% 0.14/15.42 fof(f270,definition,(
% 0.14/15.42 ![X0]: (sQ40_spl <=> (~environment(X0)|~subpopulation(sk2(sk4,sk3),X0,sk4)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f271,plain,(
% 0.14/15.42 ![X0]: (~environment(X0)|~subpopulation(sk2(sk4,sk3),X0,sk4)|~sQ40_spl)),
% 0.14/15.42 inference(component_clause,[status(thm)],[f270])).
% 0.14/15.42 fof(f273,definition,(
% 0.14/15.42 sQ41_spl <=> (sk2(sk4,sk3)=efficient_producers)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f274,plain,(
% 0.14/15.42 sk2(sk4,sk3)=efficient_producers|~sQ41_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f273])).
% 0.14/15.42 fof(f276,definition,(
% 0.14/15.42 sQ42_spl <=> (sk2(sk4,sk3)=first_movers)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f277,plain,(
% 0.14/15.42 sk2(sk4,sk3)=first_movers|~sQ42_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f276])).
% 0.14/15.42 fof(f279,plain,(
% 0.14/15.42 sQ40_spl|sQ41_spl|sQ42_spl|~sQ10_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f269,f270,f273,f276,f109])).
% 0.14/15.42 fof(f292,plain,(
% 0.14/15.42 greater(cardinality_at_time(efficient_producers,sk4),zero)|~sQ41_spl|~sQ10_spl),
% 0.14/15.42 inference(forward_demodulation,[status(thm)],[f274,f110])).
% 0.14/15.42 fof(f293,plain,(
% 0.14/15.42 greater(zero,zero)|~sQ1_spl|~sQ41_spl|~sQ10_spl),
% 0.14/15.42 inference(forward_demodulation,[status(thm)],[f64,f292])).
% 0.14/15.42 fof(f294,plain,(
% 0.14/15.42 $false|~sQ1_spl|~sQ41_spl|~sQ10_spl),
% 0.14/15.42 inference(forward_subsumption_resolution,[status(thm)],[f293,f74])).
% 0.14/15.42 fof(f295,plain,(
% 0.14/15.42 ~sQ1_spl|~sQ41_spl|~sQ10_spl),
% 0.14/15.42 inference(contradiction_clause,[status(thm)],[f294])).
% 0.14/15.42 fof(f300,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|greater(number_of_organizations(sk3,sk1(sk4,sk3)),zero)|~sQ24_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f179,f47])).
% 0.14/15.42 fof(f301,definition,(
% 0.14/15.42 sQ45_spl <=> (greater(number_of_organizations(sk3,sk1(sk4,sk3)),zero))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f302,plain,(
% 0.14/15.42 greater(number_of_organizations(sk3,sk1(sk4,sk3)),zero)|~sQ45_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f301])).
% 0.14/15.42 fof(f304,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|sQ45_spl|~sQ24_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f300,f60,f86,f301,f178])).
% 0.14/15.42 fof(f306,plain,(
% 0.14/15.42 ~environment(sk3)|~sQ37_spl|~sQ18_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f243,f146])).
% 0.14/15.42 fof(f307,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ37_spl|~sQ18_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f306,f60,f242,f145])).
% 0.14/15.42 fof(f312,plain,(
% 0.14/15.42 ~environment(sk3)|greater(zero,growth_rate(first_movers,sk1(sk4,sk3)))|~greater(zero,growth_rate(efficient_producers,sk1(sk4,sk3)))|~sQ5_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f221,f87])).
% 0.14/15.42 fof(f313,plain,(
% 0.14/15.42 ~environment(sk3)|greater(zero,growth_rate(first_movers,sk4))|~greater(zero,growth_rate(efficient_producers,sk4))),
% 0.14/15.42 inference(resolution,[status(thm)],[f221,f56])).
% 0.14/15.42 fof(f314,definition,(
% 0.14/15.42 sQ46_spl <=> (greater(zero,growth_rate(first_movers,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f315,plain,(
% 0.14/15.42 greater(zero,growth_rate(first_movers,sk1(sk4,sk3)))|~sQ46_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f314])).
% 0.14/15.42 fof(f317,plain,(
% 0.14/15.42 ~sQ0_spl|sQ46_spl|~sQ7_spl|~sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f312,f60,f314,f96,f86])).
% 0.14/15.42 fof(f318,definition,(
% 0.14/15.42 sQ47_spl <=> (greater(zero,growth_rate(first_movers,sk4)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f321,definition,(
% 0.14/15.42 sQ48_spl <=> (greater(zero,growth_rate(efficient_producers,sk4)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f324,plain,(
% 0.14/15.42 ~sQ0_spl|sQ47_spl|~sQ48_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f313,f60,f318,f321])).
% 0.14/15.42 fof(f325,plain,(
% 0.14/15.42 ~environment(sk3)|~sQ32_spl|~sQ5_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f224,f87])).
% 0.14/15.42 fof(f326,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ32_spl|~sQ5_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f325,f60,f223,f86])).
% 0.14/15.42 fof(f329,plain,(
% 0.14/15.42 ~environment(sk3)|~sQ40_spl|~sQ9_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f271,f105])).
% 0.14/15.42 fof(f330,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ40_spl|~sQ9_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f329,f60,f270,f104])).
% 0.14/15.42 fof(f336,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|number_of_organizations(sk3,sk1(sk4,sk3))=zero|~sQ25_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f182,f32])).
% 0.14/15.42 fof(f337,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|sQ19_spl|~sQ25_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f336,f60,f86,f153,f181])).
% 0.14/15.42 fof(f338,plain,(
% 0.14/15.42 ![X0,X1]: (~environment(X0)|~in_environment(X0,sk1(sk4,sk3))|greater(zero,growth_rate(X1,sk1(sk4,sk3)))|~greater(resilience(first_movers),resilience(X1))|~sQ46_spl)),
% 0.14/15.42 inference(resolution,[status(thm)],[f315,f51])).
% 0.14/15.42 fof(f340,definition,(
% 0.14/15.42 ![X1]: (sQ49_spl <=> (greater(zero,growth_rate(X1,sk1(sk4,sk3)))|~greater(resilience(first_movers),resilience(X1))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f343,plain,(
% 0.14/15.42 sQ32_spl|sQ49_spl|~sQ46_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f338,f223,f340,f314])).
% 0.14/15.42 fof(f344,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk4)|decreases(number_of_organizations(sk3,sk4))|~greater(zero,growth_rate(first_movers,sk4))|~sQ42_spl),
% 0.14/15.42 inference(paramodulation,[status(thm)],[f277,f35])).
% 0.14/15.42 fof(f345,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ20_spl|sQ8_spl|~sQ47_spl|~sQ42_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f344,f60,f157,f101,f318,f276])).
% 0.14/15.42 fof(f349,plain,(
% 0.14/15.42 ~environment(sk3)|~sQ34_spl|~sQ17_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f233,f142])).
% 0.14/15.42 fof(f350,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ34_spl|~sQ17_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f349,f60,f232,f141])).
% 0.14/15.42 fof(f351,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|greater(equilibrium(sk3),sk1(sk4,sk3))|constant(resources(sk3,sk1(sk4,sk3)))|~sQ45_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f302,f46])).
% 0.14/15.42 fof(f352,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|~greater(equilibrium(sk3),sk1(sk4,sk3))|decreases(resources(sk3,sk1(sk4,sk3)))|~sQ45_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f302,f45])).
% 0.14/15.42 fof(f353,definition,(
% 0.14/15.42 sQ50_spl <=> (greater(equilibrium(sk3),sk1(sk4,sk3)))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f356,definition,(
% 0.14/15.42 sQ51_spl <=> (constant(resources(sk3,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f357,plain,(
% 0.14/15.42 constant(resources(sk3,sk1(sk4,sk3)))|~sQ51_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f356])).
% 0.14/15.42 fof(f359,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|sQ50_spl|sQ51_spl|~sQ45_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f351,f60,f86,f353,f356,f301])).
% 0.14/15.42 fof(f360,definition,(
% 0.14/15.42 sQ52_spl <=> (decreases(resources(sk3,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f361,plain,(
% 0.14/15.42 decreases(resources(sk3,sk1(sk4,sk3)))|~sQ52_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f360])).
% 0.14/15.42 fof(f363,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|~sQ50_spl|sQ52_spl|~sQ45_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f352,f60,f86,f353,f360,f301])).
% 0.14/15.42 fof(f364,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|constant(number_of_organizations(sk3,sk1(sk4,sk3)))|~sQ51_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f357,f49])).
% 0.14/15.42 fof(f366,definition,(
% 0.14/15.42 sQ53_spl <=> (constant(number_of_organizations(sk3,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f367,plain,(
% 0.14/15.42 constant(number_of_organizations(sk3,sk1(sk4,sk3)))|~sQ53_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f366])).
% 0.14/15.42 fof(f369,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|sQ53_spl|~sQ51_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f364,f60,f86,f366,f356])).
% 0.14/15.42 fof(f372,plain,(
% 0.14/15.42 ~decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|~sQ53_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f367,f43])).
% 0.14/15.42 fof(f373,plain,(
% 0.14/15.42 $false|~sQ11_spl|~sQ53_spl),
% 0.14/15.42 inference(forward_subsumption_resolution,[status(thm)],[f372,f118])).
% 0.14/15.42 fof(f374,plain,(
% 0.14/15.42 ~sQ11_spl|~sQ53_spl),
% 0.14/15.42 inference(contradiction_clause,[status(thm)],[f373])).
% 0.14/15.42 fof(f375,plain,(
% 0.14/15.42 ![X0]: (~environment(X0)|~subpopulation(sk2(sk1(sk4,sk3),sk3),X0,sk1(sk4,sk3))|sk2(sk1(sk4,sk3),sk3)=efficient_producers|sk2(sk1(sk4,sk3),sk3)=first_movers|~sQ12_spl)),
% 0.14/15.42 inference(resolution,[status(thm)],[f121,f54])).
% 0.14/15.42 fof(f376,definition,(
% 0.14/15.42 ![X0]: (sQ54_spl <=> (~environment(X0)|~subpopulation(sk2(sk1(sk4,sk3),sk3),X0,sk1(sk4,sk3))))),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f377,plain,(
% 0.14/15.42 ![X0]: (~environment(X0)|~subpopulation(sk2(sk1(sk4,sk3),sk3),X0,sk1(sk4,sk3))|~sQ54_spl)),
% 0.14/15.42 inference(component_clause,[status(thm)],[f376])).
% 0.14/15.42 fof(f379,definition,(
% 0.14/15.42 sQ55_spl <=> (sk2(sk1(sk4,sk3),sk3)=efficient_producers)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f380,plain,(
% 0.14/15.42 sk2(sk1(sk4,sk3),sk3)=efficient_producers|~sQ55_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f379])).
% 0.14/15.42 fof(f382,definition,(
% 0.14/15.42 sQ56_spl <=> (sk2(sk1(sk4,sk3),sk3)=first_movers)),
% 0.14/15.42 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.14/15.42 fof(f383,plain,(
% 0.14/15.42 sk2(sk1(sk4,sk3),sk3)=first_movers|~sQ56_spl),
% 0.14/15.42 inference(component_clause,[status(thm)],[f382])).
% 0.14/15.42 fof(f385,plain,(
% 0.14/15.42 sQ54_spl|sQ55_spl|sQ56_spl|~sQ12_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f375,f376,f379,f382,f120])).
% 0.14/15.42 fof(f404,plain,(
% 0.14/15.42 ~environment(sk3)|~sQ54_spl|~sQ13_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f377,f125])).
% 0.14/15.42 fof(f405,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ54_spl|~sQ13_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f404,f60,f376,f124])).
% 0.14/15.42 fof(f419,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|~greater(zero,growth_rate(efficient_producers,sk1(sk4,sk3)))|~sQ55_spl),
% 0.14/15.42 inference(paramodulation,[status(thm)],[f380,f35])).
% 0.14/15.42 fof(f420,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|sQ11_spl|~sQ7_spl|~sQ55_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f419,f60,f86,f117,f96,f379])).
% 0.14/15.42 fof(f425,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|~greater(zero,growth_rate(first_movers,sk1(sk4,sk3)))|~sQ56_spl),
% 0.14/15.42 inference(paramodulation,[status(thm)],[f383,f35])).
% 0.14/15.42 fof(f426,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|sQ11_spl|~sQ46_spl|~sQ56_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f425,f60,f86,f117,f314,f382])).
% 0.14/15.42 fof(f427,plain,(
% 0.14/15.42 ~environment(sk3)|~in_environment(sk3,sk1(sk4,sk3))|~decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|~sQ52_spl),
% 0.14/15.42 inference(resolution,[status(thm)],[f361,f48])).
% 0.14/15.42 fof(f428,plain,(
% 0.14/15.42 ~sQ0_spl|~sQ5_spl|~sQ11_spl|~sQ52_spl),
% 0.14/15.42 inference(split_clause,[status(thm)],[f427,f60,f86,f117,f360])).
% 0.14/15.42 fof(f429,plain,(
% 0.14/15.42 $false),
% 0.14/15.42 inference(sat_refutation,[status(thm)],[f69,f71,f73,f79,f84,f89,f94,f99,f107,f112,f123,f127,f131,f138,f144,f148,f156,f171,f175,f184,f191,f196,f198,f200,f209,f213,f218,f220,f229,f268,f279,f295,f304,f307,f317,f324,f326,f330,f337,f343,f345,f350,f359,f363,f369,f374,f385,f405,f420,f426,f428])).
% 0.14/15.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/15.44 % Elapsed time: 0.053993 seconds
% 0.14/15.44 % CPU time: 0.163425 seconds
% 0.14/15.44 % Total memory used: 81.506 MB
% 0.14/15.44 % Net memory used: 81.278 MB
%------------------------------------------------------------------------------