%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:24 PM UTC 2026
% Result : Theorem 0.21s 6.10s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 80
% Syntax : Number of formulae : 368 ( 16 unt; 61 def)
% Number of atoms : 1185 ( 52 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1467 ( 650 ~; 687 |; 48 &)
% ( 62 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 73 ( 71 usr; 62 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-2 aty)
% Number of variables : 208 ( 204 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [E,S1,S2,T] :
( ( greater(growth_rate(S2,T),growth_rate(S1,T))
& subpopulations(S1,S2,E,T)
& environment(E) )
=> selection_favors(S2,S1,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [E,S1,S2,T] :
( ( cardinality_at_time(S2,T) = zero
& greater(cardinality_at_time(S1,T),zero)
& subpopulation(S2,E,T)
& subpopulation(S1,E,T)
& environment(E) )
=> selection_favors(S1,S2,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [P] :
( ( ! [E] :
( ( in_environment(P,E)
& environment(E) )
=> selection_favors(efficient_producers,first_movers,end_time(E)) )
& propagation_strategy(efficient_producers)
& propagation_strategy(first_movers)
& observational_period(P) )
=> selection_favors(efficient_producers,first_movers,P) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [P] :
( ( slow_change(P)
& observational_period(P) )
=> ! [E] :
( ( in_environment(P,E)
& environment(E) )
=> ? [T] :
( greater(T,critical_point(E))
& in_environment(E,T) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
propagation_strategy(first_movers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
propagation_strategy(efficient_producers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [E,T] :
( ( greater_or_equal(end_time(E),T)
& greater_or_equal(T,start_time(E))
& environment(E) )
=> in_environment(E,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> greater_or_equal(end_time(E),T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [E,T] :
( ( greater(cardinality_at_time(efficient_producers,T),zero)
& greater(cardinality_at_time(first_movers,T),zero)
& in_environment(E,T)
& environment(E) )
=> subpopulations(first_movers,efficient_producers,E,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> greater_or_equal(cardinality_at_time(first_movers,T),zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> ( subpopulation(efficient_producers,E,T)
& subpopulation(first_movers,E,T) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [E] :
( environment(E)
=> greater_or_equal(critical_point(E),appear(efficient_producers,E)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [E] :
( environment(E)
=> greater_or_equal(critical_point(E),start_time(E)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,Y,Z] :
( ( greater(Y,Z)
& greater(X,Y) )
=> greater(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [E,T] :
( ( ~ greater(T,end_time(E))
& greater(T,start_time(E))
& environment(E) )
=> greater_or_equal(end_time(E),T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X,Y] :
( greater_or_equal(X,Y)
<=> ( X = Y
| greater(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
! [E,Tc] :
( ( Tc = critical_point(E)
& environment(E) )
=> ( ! [T] :
( ( greater(T,Tc)
& subpopulations(first_movers,efficient_producers,E,T) )
=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) )
& ~ greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
! [E,T] :
( ( greater_or_equal(T,appear(efficient_producers,E))
& in_environment(E,T)
& environment(E) )
=> greater(cardinality_at_time(efficient_producers,T),zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
! [P] :
( ( slow_change(P)
& observational_period(P) )
=> selection_favors(efficient_producers,first_movers,P) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ ! [P] :
( ( slow_change(P)
& observational_period(P) )
=> selection_favors(efficient_producers,first_movers,P) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [E,S1,S2,T] :
( selection_favors(S2,S1,T)
| ~ greater(growth_rate(S2,T),growth_rate(S1,T))
| ~ subpopulations(S1,S2,E,T)
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
! [S1,S2,T] :
( selection_favors(S2,S1,T)
| ~ greater(growth_rate(S2,T),growth_rate(S1,T))
| ! [E] :
( ~ subpopulations(S1,S2,E,T)
| ~ environment(E) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( selection_favors(X2,X1,X3)
| ~ greater(growth_rate(X2,X3),growth_rate(X1,X3))
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [E,S1,S2,T] :
( selection_favors(S1,S2,T)
| cardinality_at_time(S2,T) != zero
| ~ greater(cardinality_at_time(S1,T),zero)
| ~ subpopulation(S2,E,T)
| ~ subpopulation(S1,E,T)
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f25,plain,
! [S1,S2,T] :
( selection_favors(S1,S2,T)
| cardinality_at_time(S2,T) != zero
| ~ greater(cardinality_at_time(S1,T),zero)
| ! [E] :
( ~ subpopulation(S2,E,T)
| ~ subpopulation(S1,E,T)
| ~ environment(E) ) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f26,plain,
! [X0,X1,X2,X3] :
( selection_favors(X1,X3,X2)
| cardinality_at_time(X3,X2) != zero
| ~ greater(cardinality_at_time(X1,X2),zero)
| ~ subpopulation(X3,X0,X2)
| ~ subpopulation(X1,X0,X2)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f27,plain,
! [P] :
( selection_favors(efficient_producers,first_movers,P)
| ? [E] :
( ~ selection_favors(efficient_producers,first_movers,end_time(E))
& in_environment(P,E)
& environment(E) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(P) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f28,plain,
! [P] :
( selection_favors(efficient_producers,first_movers,P)
| ( ~ selection_favors(efficient_producers,first_movers,end_time(sK0_skl(P)))
& in_environment(P,sK0_skl(P))
& environment(sK0_skl(P)) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(E,sK0_skl(P))],[f27]) ).
fof(f29,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| environment(sK0_skl(X0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sK0_skl(X0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f31,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0_skl(X0)))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f32,plain,
! [P] :
( ! [E] :
( ? [T] :
( greater(T,critical_point(E))
& in_environment(E,T) )
| ~ in_environment(P,E)
| ~ environment(E) )
| ~ slow_change(P)
| ~ observational_period(P) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f33,plain,
! [P] :
( ! [E] :
( ( greater(sK1_skl(E,P),critical_point(E))
& in_environment(E,sK1_skl(E,P)) )
| ~ in_environment(P,E)
| ~ environment(E) )
| ~ slow_change(P)
| ~ observational_period(P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(T,sK1_skl(E,P))],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( in_environment(X1,sK1_skl(X1,X0))
| ~ in_environment(X0,X1)
| ~ environment(X1)
| ~ slow_change(X0)
| ~ observational_period(X0) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [X0,X1] :
( greater(sK1_skl(X1,X0),critical_point(X1))
| ~ in_environment(X0,X1)
| ~ environment(X1)
| ~ slow_change(X0)
| ~ observational_period(X0) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f36,plain,
propagation_strategy(first_movers),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f37,plain,
propagation_strategy(efficient_producers),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f38,plain,
! [E,T] :
( in_environment(E,T)
| ~ greater_or_equal(end_time(E),T)
| ~ greater_or_equal(T,start_time(E))
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f39,plain,
! [X0,X1] :
( in_environment(X0,X1)
| ~ greater_or_equal(end_time(X0),X1)
| ~ greater_or_equal(X1,start_time(X0))
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f40,plain,
! [E,T] :
( greater_or_equal(end_time(E),T)
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f41,plain,
! [X0,X1] :
( greater_or_equal(end_time(X0),X1)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f42,plain,
! [E,T] :
( subpopulations(first_movers,efficient_producers,E,T)
| ~ greater(cardinality_at_time(efficient_producers,T),zero)
| ~ greater(cardinality_at_time(first_movers,T),zero)
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f43,plain,
! [X0,X1] :
( subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f44,plain,
! [E,T] :
( greater_or_equal(cardinality_at_time(first_movers,T),zero)
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f45,plain,
! [T] :
( greater_or_equal(cardinality_at_time(first_movers,T),zero)
| ! [E] :
( ~ in_environment(E,T)
| ~ environment(E) ) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0,X1] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
! [E,T] :
( ( subpopulation(efficient_producers,E,T)
& subpopulation(first_movers,E,T) )
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f48,plain,
! [X0,X1] :
( subpopulation(first_movers,X0,X1)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( subpopulation(efficient_producers,X0,X1)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f50,plain,
! [E] :
( greater_or_equal(critical_point(E),appear(efficient_producers,E))
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f51,plain,
! [X0] :
( greater_or_equal(critical_point(X0),appear(efficient_producers,X0))
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [E] :
( greater_or_equal(critical_point(E),start_time(E))
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f53,plain,
! [X0] :
( greater_or_equal(critical_point(X0),start_time(X0))
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f55,plain,
! [X,Z] :
( greater(X,Z)
| ! [Y] :
( ~ greater(Y,Z)
| ~ greater(X,Y) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f56,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [E,T] :
( greater_or_equal(end_time(E),T)
| greater(T,end_time(E))
| ~ greater(T,start_time(E))
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f58,plain,
! [X0,X1] :
( greater_or_equal(end_time(X0),X1)
| greater(X1,end_time(X0))
| ~ greater(X1,start_time(X0))
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X,Y] :
( ( ( X != Y
& ~ greater(X,Y) )
| greater_or_equal(X,Y) )
& ( X = Y
| greater(X,Y)
| ~ greater_or_equal(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f16]) ).
fof(f60,plain,
( ! [X,Y] :
( ( X != Y
& ~ greater(X,Y) )
| greater_or_equal(X,Y) )
& ! [X,Y] :
( X = Y
| greater(X,Y)
| ~ greater_or_equal(X,Y) ) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f61,plain,
! [X0,X1] :
( X0 = X1
| greater(X0,X1)
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f63,plain,
! [X0,X1] :
( X0 != X1
| greater_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f64,plain,
! [E,Tc] :
( ( ! [T] :
( greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T))
| ~ greater(T,Tc)
| ~ subpopulations(first_movers,efficient_producers,E,T) )
& ~ greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc)) )
| Tc != critical_point(E)
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f65,plain,
! [X0,X1] :
( ~ greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| X1 != critical_point(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X0,X1,X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ greater(X2,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| X1 != critical_point(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f67,plain,
! [E,T] :
( greater(cardinality_at_time(efficient_producers,T),zero)
| ~ greater_or_equal(T,appear(efficient_producers,E))
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f68,plain,
! [T] :
( greater(cardinality_at_time(efficient_producers,T),zero)
| ! [E] :
( ~ greater_or_equal(T,appear(efficient_producers,E))
| ~ in_environment(E,T)
| ~ environment(E) ) ),
inference(miniscoping,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0,X1] :
( greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater_or_equal(X1,appear(efficient_producers,X0))
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
? [P] :
( ~ selection_favors(efficient_producers,first_movers,P)
& slow_change(P)
& observational_period(P) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f71,plain,
( ~ selection_favors(efficient_producers,first_movers,sK2_skl)
& slow_change(sK2_skl)
& observational_period(sK2_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(P,sK2_skl)],[f70]) ).
fof(f72,plain,
observational_period(sK2_skl),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
slow_change(sK2_skl),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
~ selection_favors(efficient_producers,first_movers,sK2_skl),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f75,definition,
! [X0] :
( sQ0_spl
<=> ( selection_favors(efficient_producers,first_movers,X0)
| environment(sK0_skl(X0))
| ~ observational_period(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f76,plain,
! [X0] :
( ~ sQ0_spl
| selection_favors(efficient_producers,first_movers,X0)
| environment(sK0_skl(X0))
| ~ observational_period(X0) ),
inference(component_clause,[status(thm)],[f75]) ).
fof(f78,definition,
( sQ1_spl
<=> propagation_strategy(first_movers) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f80,plain,
( sQ1_spl
| ~ propagation_strategy(first_movers) ),
inference(component_clause,[status(thm)],[f78]) ).
fof(f81,definition,
( sQ2_spl
<=> propagation_strategy(efficient_producers) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f83,plain,
( sQ2_spl
| ~ propagation_strategy(efficient_producers) ),
inference(component_clause,[status(thm)],[f81]) ).
fof(f84,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f29,f75,f78,f81]) ).
fof(f85,definition,
! [X0] :
( sQ3_spl
<=> ( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sK0_skl(X0))
| ~ observational_period(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f86,plain,
! [X0] :
( ~ sQ3_spl
| selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sK0_skl(X0))
| ~ observational_period(X0) ),
inference(component_clause,[status(thm)],[f85]) ).
fof(f88,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f30,f85,f78,f81]) ).
fof(f89,definition,
! [X0] :
( sQ4_spl
<=> ( selection_favors(efficient_producers,first_movers,X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0_skl(X0)))
| ~ observational_period(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f90,plain,
! [X0] :
( ~ sQ4_spl
| selection_favors(efficient_producers,first_movers,X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0_skl(X0)))
| ~ observational_period(X0) ),
inference(component_clause,[status(thm)],[f89]) ).
fof(f92,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f31,f89,f78,f81]) ).
fof(f93,plain,
! [X0] : greater_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f63]) ).
fof(f94,plain,
! [X0] :
( ~ greater(growth_rate(efficient_producers,critical_point(X0)),growth_rate(first_movers,critical_point(X0)))
| ~ environment(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f65]) ).
fof(f95,plain,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ greater(X1,critical_point(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f66]) ).
fof(f96,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f83,f37]) ).
fof(f97,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f96]) ).
fof(f98,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f80,f36]) ).
fof(f99,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f98]) ).
fof(f102,plain,
( ~ sQ0_spl
| selection_favors(efficient_producers,first_movers,sK2_skl)
| environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f76,f72]) ).
fof(f103,definition,
( sQ5_spl
<=> environment(sK0_skl(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f104,plain,
( ~ sQ5_spl
| environment(sK0_skl(sK2_skl)) ),
inference(component_clause,[status(thm)],[f103]) ).
fof(f106,definition,
( sQ6_spl
<=> selection_favors(efficient_producers,first_movers,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f107,plain,
( ~ sQ6_spl
| selection_favors(efficient_producers,first_movers,sK2_skl) ),
inference(component_clause,[status(thm)],[f106]) ).
fof(f109,plain,
( ~ sQ0_spl
| sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f102,f103,f106,f75]) ).
fof(f110,plain,
( ~ sQ5_spl
| greater_or_equal(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f104,f51]) ).
fof(f111,plain,
! [X0] :
( ~ sQ5_spl
| subpopulation(efficient_producers,sK0_skl(sK2_skl),X0)
| ~ in_environment(sK0_skl(sK2_skl),X0) ),
inference(resolution,[status(thm)],[f104,f49]) ).
fof(f112,plain,
! [X0] :
( ~ sQ5_spl
| subpopulation(first_movers,sK0_skl(sK2_skl),X0)
| ~ in_environment(sK0_skl(sK2_skl),X0) ),
inference(resolution,[status(thm)],[f104,f48]) ).
fof(f113,plain,
! [X0] :
( ~ sQ5_spl
| greater_or_equal(end_time(sK0_skl(sK2_skl)),X0)
| ~ in_environment(sK0_skl(sK2_skl),X0) ),
inference(resolution,[status(thm)],[f104,f41]) ).
fof(f114,plain,
( ~ sQ5_spl
| greater_or_equal(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f104,f53]) ).
fof(f115,plain,
! [X0] :
( ~ sQ5_spl
| in_environment(sK0_skl(sK2_skl),sK1_skl(sK0_skl(sK2_skl),X0))
| ~ in_environment(X0,sK0_skl(sK2_skl))
| ~ slow_change(X0)
| ~ observational_period(X0) ),
inference(resolution,[status(thm)],[f104,f34]) ).
fof(f116,plain,
( ~ sQ5_spl
| critical_point(sK0_skl(sK2_skl)) = start_time(sK0_skl(sK2_skl))
| greater(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f114,f61]) ).
fof(f117,definition,
( sQ7_spl
<=> greater(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f118,plain,
( ~ sQ7_spl
| greater(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f117]) ).
fof(f120,definition,
( sQ8_spl
<=> critical_point(sK0_skl(sK2_skl)) = start_time(sK0_skl(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f121,plain,
( ~ sQ8_spl
| critical_point(sK0_skl(sK2_skl)) = start_time(sK0_skl(sK2_skl)) ),
inference(component_clause,[status(thm)],[f120]) ).
fof(f123,plain,
( ~ sQ5_spl
| sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f116,f117,f120,f103]) ).
fof(f124,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f107,f74]) ).
fof(f125,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f124]) ).
fof(f126,plain,
! [X0] :
( ~ sQ5_spl
| in_environment(sK0_skl(sK2_skl),X0)
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),X0)
| ~ greater_or_equal(X0,start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f104,f39]) ).
fof(f127,plain,
! [X0] :
( ~ sQ5_spl
| greater(sK1_skl(sK0_skl(sK2_skl),X0),critical_point(sK0_skl(sK2_skl)))
| ~ in_environment(X0,sK0_skl(sK2_skl))
| ~ slow_change(X0)
| ~ observational_period(X0) ),
inference(resolution,[status(thm)],[f104,f35]) ).
fof(f134,plain,
! [X0] :
( ~ sQ7_spl
| greater(X0,start_time(sK0_skl(sK2_skl)))
| ~ greater(X0,critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f118,f56]) ).
fof(f137,plain,
( ~ sQ5_spl
| critical_point(sK0_skl(sK2_skl)) = appear(efficient_producers,sK0_skl(sK2_skl))
| greater(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f110,f61]) ).
fof(f138,definition,
( sQ9_spl
<=> greater(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f139,plain,
( ~ sQ9_spl
| greater(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f138]) ).
fof(f141,definition,
( sQ10_spl
<=> critical_point(sK0_skl(sK2_skl)) = appear(efficient_producers,sK0_skl(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f142,plain,
( ~ sQ10_spl
| critical_point(sK0_skl(sK2_skl)) = appear(efficient_producers,sK0_skl(sK2_skl)) ),
inference(component_clause,[status(thm)],[f141]) ).
fof(f144,plain,
( ~ sQ5_spl
| sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f137,f138,f141,f103]) ).
fof(f145,plain,
! [X0] :
( ~ sQ5_spl
| ~ greater(end_time(sK0_skl(sK2_skl)),X0)
| in_environment(sK0_skl(sK2_skl),X0)
| ~ greater_or_equal(X0,start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f126,f62]) ).
fof(f146,plain,
( ~ sQ5_spl
| in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f126,f93]) ).
fof(f147,definition,
( sQ11_spl
<=> greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f148,plain,
( ~ sQ11_spl
| greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f147]) ).
fof(f149,plain,
( sQ11_spl
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f147]) ).
fof(f150,definition,
( sQ12_spl
<=> in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f151,plain,
( ~ sQ12_spl
| in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f153,plain,
( ~ sQ5_spl
| sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f146,f147,f150,f103]) ).
fof(f154,plain,
( sQ11_spl
| ~ greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f149,f62]) ).
fof(f155,plain,
( ~ sQ3_spl
| selection_favors(efficient_producers,first_movers,sK2_skl)
| in_environment(sK2_skl,sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f86,f72]) ).
fof(f156,definition,
( sQ13_spl
<=> in_environment(sK2_skl,sK0_skl(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f157,plain,
( ~ sQ13_spl
| in_environment(sK2_skl,sK0_skl(sK2_skl)) ),
inference(component_clause,[status(thm)],[f156]) ).
fof(f159,plain,
( ~ sQ3_spl
| sQ6_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f155,f156,f106,f85]) ).
fof(f160,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| in_environment(sK0_skl(sK2_skl),sK1_skl(sK0_skl(sK2_skl),sK2_skl))
| ~ slow_change(sK2_skl)
| ~ observational_period(sK2_skl) ),
inference(resolution,[status(thm)],[f157,f115]) ).
fof(f162,definition,
( sQ14_spl
<=> observational_period(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f164,plain,
( sQ14_spl
| ~ observational_period(sK2_skl) ),
inference(component_clause,[status(thm)],[f162]) ).
fof(f165,definition,
( sQ15_spl
<=> slow_change(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f167,plain,
( sQ15_spl
| ~ slow_change(sK2_skl) ),
inference(component_clause,[status(thm)],[f165]) ).
fof(f168,definition,
( sQ16_spl
<=> in_environment(sK0_skl(sK2_skl),sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f169,plain,
( ~ sQ16_spl
| in_environment(sK0_skl(sK2_skl),sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f171,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f160,f162,f165,f168,f156,f103]) ).
fof(f203,plain,
! [X0] :
( ~ sQ5_spl
| greater_or_equal(end_time(sK0_skl(sK2_skl)),X0)
| greater(X0,end_time(sK0_skl(sK2_skl)))
| ~ greater(X0,start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f58,f104]) ).
fof(f208,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f167,f73]) ).
fof(f209,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f208]) ).
fof(f210,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f164,f72]) ).
fof(f211,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f210]) ).
fof(f212,plain,
( ~ sQ5_spl
| greater(sK1_skl(sK0_skl(sK2_skl),sK2_skl),critical_point(sK0_skl(sK2_skl)))
| ~ in_environment(sK2_skl,sK0_skl(sK2_skl))
| ~ observational_period(sK2_skl) ),
inference(resolution,[status(thm)],[f127,f73]) ).
fof(f213,definition,
( sQ25_spl
<=> greater(sK1_skl(sK0_skl(sK2_skl),sK2_skl),critical_point(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( ~ sQ25_spl
| greater(sK1_skl(sK0_skl(sK2_skl),sK2_skl),critical_point(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f213]) ).
fof(f216,plain,
( ~ sQ5_spl
| sQ25_spl
| ~ sQ13_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f212,f162,f156,f213,f103]) ).
fof(f218,plain,
( ~ sQ12_spl
| greater_or_equal(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero)
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f151,f46]) ).
fof(f219,definition,
( sQ26_spl
<=> greater_or_equal(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( ~ sQ26_spl
| greater_or_equal(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,plain,
( ~ sQ12_spl
| sQ26_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f218,f103,f219,f150]) ).
fof(f223,plain,
( sQ11_spl
| ~ sQ8_spl
| ~ greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
inference(backward_demodulation,[status(thm)],[f121,f154]) ).
fof(f228,plain,
( ~ sQ5_spl
| ~ sQ16_spl
| greater_or_equal(end_time(sK0_skl(sK2_skl)),sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
inference(resolution,[status(thm)],[f169,f113]) ).
fof(f229,plain,
( ~ sQ16_spl
| greater_or_equal(cardinality_at_time(first_movers,sK1_skl(sK0_skl(sK2_skl),sK2_skl)),zero)
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f169,f46]) ).
fof(f230,definition,
( sQ27_spl
<=> greater_or_equal(cardinality_at_time(first_movers,sK1_skl(sK0_skl(sK2_skl),sK2_skl)),zero) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f233,plain,
( ~ sQ16_spl
| sQ27_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f229,f103,f230,f168]) ).
fof(f235,plain,
( ~ sQ26_spl
| cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))) = zero
| greater(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero) ),
inference(resolution,[status(thm)],[f220,f61]) ).
fof(f236,definition,
( sQ28_spl
<=> greater(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f237,plain,
( ~ sQ28_spl
| greater(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero) ),
inference(component_clause,[status(thm)],[f236]) ).
fof(f239,definition,
( sQ29_spl
<=> cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))) = zero ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f242,plain,
( ~ sQ26_spl
| sQ29_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f235,f236,f239,f219]) ).
fof(f246,definition,
! [X0] :
( sQ30_spl
<=> ( subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| ~ in_environment(X0,end_time(sK0_skl(sK2_skl)))
| ~ environment(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f247,plain,
! [X0] :
( ~ sQ30_spl
| subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| ~ in_environment(X0,end_time(sK0_skl(sK2_skl)))
| ~ environment(X0) ),
inference(component_clause,[status(thm)],[f246]) ).
fof(f249,definition,
( sQ31_spl
<=> greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( ~ sQ31_spl
| greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero) ),
inference(component_clause,[status(thm)],[f249]) ).
fof(f251,plain,
( sQ31_spl
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero) ),
inference(component_clause,[status(thm)],[f249]) ).
fof(f263,definition,
( sQ34_spl
<=> greater(growth_rate(efficient_producers,critical_point(sK0_skl(sK2_skl))),growth_rate(first_movers,critical_point(sK0_skl(sK2_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f264,plain,
( ~ sQ34_spl
| greater(growth_rate(efficient_producers,critical_point(sK0_skl(sK2_skl))),growth_rate(first_movers,critical_point(sK0_skl(sK2_skl)))) ),
inference(component_clause,[status(thm)],[f263]) ).
fof(f267,plain,
! [X0] :
( ~ sQ28_spl
| subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)
| ~ in_environment(X0,end_time(sK0_skl(sK2_skl)))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[f237,f43]) ).
fof(f270,plain,
( ~ sQ28_spl
| ~ sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f267,f246,f249,f236]) ).
fof(f276,plain,
! [X0] :
( ~ sQ5_spl
| greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0_skl(sK2_skl)))
| ~ in_environment(sK0_skl(sK2_skl),X0) ),
inference(resolution,[status(thm)],[f69,f104]) ).
fof(f277,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ10_spl
| greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,critical_point(sK0_skl(sK2_skl)))
| ~ in_environment(sK0_skl(sK2_skl),X0) ),
inference(forward_demodulation,[status(thm)],[f142,f276]) ).
fof(f283,definition,
( sQ35_spl
<=> greater(critical_point(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f286,definition,
( sQ36_spl
<=> greater_or_equal(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( sQ36_spl
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f286]) ).
fof(f292,definition,
( sQ37_spl
<=> greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( ~ sQ37_spl
| greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f292]) ).
fof(f295,definition,
( sQ38_spl
<=> end_time(sK0_skl(sK2_skl)) = critical_point(sK0_skl(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f296,plain,
( ~ sQ38_spl
| end_time(sK0_skl(sK2_skl)) = critical_point(sK0_skl(sK2_skl)) ),
inference(component_clause,[status(thm)],[f295]) ).
fof(f312,plain,
( ~ sQ37_spl
| greater(growth_rate(efficient_producers,end_time(sK0_skl(sK2_skl))),growth_rate(first_movers,end_time(sK0_skl(sK2_skl))))
| ~ subpopulations(first_movers,efficient_producers,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f293,f95]) ).
fof(f313,plain,
! [X0] :
( ~ sQ37_spl
| greater(X0,critical_point(sK0_skl(sK2_skl)))
| ~ greater(X0,end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f293,f56]) ).
fof(f314,definition,
( sQ39_spl
<=> subpopulations(first_movers,efficient_producers,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f317,definition,
( sQ40_spl
<=> greater(growth_rate(efficient_producers,end_time(sK0_skl(sK2_skl))),growth_rate(first_movers,end_time(sK0_skl(sK2_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f318,plain,
( ~ sQ40_spl
| greater(growth_rate(efficient_producers,end_time(sK0_skl(sK2_skl))),growth_rate(first_movers,end_time(sK0_skl(sK2_skl)))) ),
inference(component_clause,[status(thm)],[f317]) ).
fof(f320,plain,
( ~ sQ37_spl
| sQ40_spl
| ~ sQ39_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f312,f103,f314,f317,f292]) ).
fof(f321,plain,
( ~ sQ11_spl
| end_time(sK0_skl(sK2_skl)) = start_time(sK0_skl(sK2_skl))
| greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f148,f61]) ).
fof(f322,definition,
( sQ41_spl
<=> greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f323,plain,
( ~ sQ41_spl
| greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f324,plain,
( sQ41_spl
| ~ greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f325,definition,
( sQ42_spl
<=> end_time(sK0_skl(sK2_skl)) = start_time(sK0_skl(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f326,plain,
( ~ sQ42_spl
| end_time(sK0_skl(sK2_skl)) = start_time(sK0_skl(sK2_skl)) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f328,plain,
( ~ sQ11_spl
| sQ42_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f321,f322,f325,f147]) ).
fof(f332,definition,
( sQ43_spl
<=> greater_or_equal(start_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( sQ43_spl
| ~ greater_or_equal(start_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f332]) ).
fof(f335,definition,
( sQ44_spl
<=> in_environment(sK0_skl(sK2_skl),start_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( ~ sQ44_spl
| in_environment(sK0_skl(sK2_skl),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f340,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f334,f93]) ).
fof(f341,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f340]) ).
fof(f344,definition,
( sQ45_spl
<=> in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f345,plain,
( ~ sQ45_spl
| in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f344]) ).
fof(f347,definition,
( sQ46_spl
<=> greater(cardinality_at_time(efficient_producers,critical_point(sK0_skl(sK2_skl))),zero) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( ~ sQ46_spl
| greater(cardinality_at_time(efficient_producers,critical_point(sK0_skl(sK2_skl))),zero) ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f357,plain,
( ~ sQ5_spl
| ~ sQ42_spl
| greater_or_equal(critical_point(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
inference(forward_demodulation,[status(thm)],[f326,f114]) ).
fof(f358,plain,
( ~ sQ5_spl
| ~ sQ42_spl
| critical_point(sK0_skl(sK2_skl)) = end_time(sK0_skl(sK2_skl))
| greater(critical_point(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f357,f61]) ).
fof(f359,plain,
( ~ sQ5_spl
| ~ sQ42_spl
| sQ38_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f358,f283,f295,f325,f103]) ).
fof(f360,definition,
! [X0] :
( sQ47_spl
<=> ( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ greater(X0,end_time(sK0_skl(sK2_skl)))
| ~ subpopulations(first_movers,efficient_producers,sK0_skl(sK2_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f372,plain,
( ~ sQ5_spl
| ~ sQ44_spl
| greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f336,f113]) ).
fof(f373,plain,
( ~ sQ44_spl
| greater_or_equal(cardinality_at_time(first_movers,start_time(sK0_skl(sK2_skl))),zero)
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f336,f46]) ).
fof(f374,definition,
( sQ50_spl
<=> greater_or_equal(cardinality_at_time(first_movers,start_time(sK0_skl(sK2_skl))),zero) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( ~ sQ44_spl
| sQ50_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f373,f103,f374,f335]) ).
fof(f378,plain,
! [X0] :
( ~ sQ41_spl
| greater(X0,start_time(sK0_skl(sK2_skl)))
| ~ greater(X0,end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f323,f56]) ).
fof(f386,plain,
! [X0,X1] :
( ~ sQ46_spl
| selection_favors(efficient_producers,X1,critical_point(sK0_skl(sK2_skl)))
| cardinality_at_time(X1,critical_point(sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X1,X0,critical_point(sK0_skl(sK2_skl)))
| ~ subpopulation(efficient_producers,X0,critical_point(sK0_skl(sK2_skl)))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[f348,f26]) ).
fof(f393,plain,
! [X0] :
( ~ sQ5_spl
| in_environment(sK0_skl(sK2_skl),X0)
| ~ greater_or_equal(X0,start_time(sK0_skl(sK2_skl)))
| greater(X0,end_time(sK0_skl(sK2_skl)))
| ~ greater(X0,start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f203,f126]) ).
fof(f394,plain,
! [X0] :
( ~ sQ5_spl
| end_time(sK0_skl(sK2_skl)) = X0
| greater(end_time(sK0_skl(sK2_skl)),X0)
| greater(X0,end_time(sK0_skl(sK2_skl)))
| ~ greater(X0,start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f203,f61]) ).
fof(f395,plain,
! [X0] :
( ~ sQ5_spl
| in_environment(sK0_skl(sK2_skl),X0)
| greater(X0,end_time(sK0_skl(sK2_skl)))
| ~ greater(X0,start_time(sK0_skl(sK2_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f62]) ).
fof(f413,definition,
( sQ54_spl
<=> greater(cardinality_at_time(efficient_producers,start_time(sK0_skl(sK2_skl))),zero) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f415,plain,
( sQ54_spl
| ~ greater(cardinality_at_time(efficient_producers,start_time(sK0_skl(sK2_skl))),zero) ),
inference(component_clause,[status(thm)],[f413]) ).
fof(f425,plain,
( ~ sQ5_spl
| greater(appear(efficient_producers,sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl)))
| ~ greater(appear(efficient_producers,sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))
| greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)
| ~ in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f276,f203]) ).
fof(f426,plain,
! [X0] :
( ~ sQ5_spl
| ~ greater(X0,appear(efficient_producers,sK0_skl(sK2_skl)))
| greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ in_environment(sK0_skl(sK2_skl),X0) ),
inference(resolution,[status(thm)],[f276,f62]) ).
fof(f427,plain,
( ~ sQ5_spl
| greater(cardinality_at_time(efficient_producers,appear(efficient_producers,sK0_skl(sK2_skl))),zero)
| ~ in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f276,f93]) ).
fof(f428,definition,
( sQ56_spl
<=> greater(appear(efficient_producers,sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( ~ sQ56_spl
| greater(appear(efficient_producers,sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f430,plain,
( sQ56_spl
| ~ greater(appear(efficient_producers,sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,definition,
( sQ57_spl
<=> greater(appear(efficient_producers,sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f432,plain,
( ~ sQ57_spl
| greater(appear(efficient_producers,sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f434,plain,
( ~ sQ5_spl
| sQ57_spl
| ~ sQ56_spl
| sQ31_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f425,f150,f249,f428,f431,f103]) ).
fof(f435,definition,
( sQ58_spl
<=> in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f437,plain,
( sQ58_spl
| ~ in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f435]) ).
fof(f438,definition,
( sQ59_spl
<=> greater(cardinality_at_time(efficient_producers,appear(efficient_producers,sK0_skl(sK2_skl))),zero) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( ~ sQ59_spl
| greater(cardinality_at_time(efficient_producers,appear(efficient_producers,sK0_skl(sK2_skl))),zero) ),
inference(component_clause,[status(thm)],[f438]) ).
fof(f441,plain,
( ~ sQ5_spl
| sQ59_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f427,f435,f438,f103]) ).
fof(f442,plain,
( ~ sQ5_spl
| greater(cardinality_at_time(efficient_producers,critical_point(sK0_skl(sK2_skl))),zero)
| ~ in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f110,f276]) ).
fof(f444,plain,
( ~ sQ5_spl
| sQ46_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f442,f344,f347,f103]) ).
fof(f451,plain,
! [X0] :
( ~ sQ9_spl
| greater(X0,appear(efficient_producers,sK0_skl(sK2_skl)))
| ~ greater(X0,critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f139,f56]) ).
fof(f453,plain,
! [X0] :
( ~ sQ25_spl
| greater(X0,critical_point(sK0_skl(sK2_skl)))
| ~ greater(X0,sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
inference(resolution,[status(thm)],[f214,f56]) ).
fof(f462,plain,
( ~ sQ5_spl
| ~ sQ16_spl
| end_time(sK0_skl(sK2_skl)) = sK1_skl(sK0_skl(sK2_skl),sK2_skl)
| greater(end_time(sK0_skl(sK2_skl)),sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
inference(resolution,[status(thm)],[f228,f61]) ).
fof(f467,definition,
( sQ63_spl
<=> greater(end_time(sK0_skl(sK2_skl)),sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( ~ sQ63_spl
| greater(end_time(sK0_skl(sK2_skl)),sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
inference(component_clause,[status(thm)],[f467]) ).
fof(f470,definition,
( sQ64_spl
<=> end_time(sK0_skl(sK2_skl)) = sK1_skl(sK0_skl(sK2_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( ~ sQ64_spl
| end_time(sK0_skl(sK2_skl)) = sK1_skl(sK0_skl(sK2_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,plain,
( ~ sQ5_spl
| ~ sQ16_spl
| sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f462,f467,f470,f168,f103]) ).
fof(f476,plain,
( ~ sQ16_spl
| ~ sQ64_spl
| in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
inference(backward_demodulation,[status(thm)],[f471,f169]) ).
fof(f479,definition,
( sQ65_spl
<=> greater_or_equal(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( sQ65_spl
| ~ greater_or_equal(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f479]) ).
fof(f484,plain,
( sQ65_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f481,f114]) ).
fof(f485,plain,
( sQ65_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f484]) ).
fof(f486,plain,
( ~ sQ5_spl
| ~ sQ45_spl
| greater_or_equal(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f345,f113]) ).
fof(f487,plain,
( ~ sQ45_spl
| greater_or_equal(cardinality_at_time(first_movers,critical_point(sK0_skl(sK2_skl))),zero)
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f345,f46]) ).
fof(f488,definition,
( sQ66_spl
<=> greater_or_equal(cardinality_at_time(first_movers,critical_point(sK0_skl(sK2_skl))),zero) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f491,plain,
( ~ sQ45_spl
| sQ66_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f487,f103,f488,f344]) ).
fof(f493,plain,
( ~ sQ5_spl
| ~ sQ45_spl
| end_time(sK0_skl(sK2_skl)) = critical_point(sK0_skl(sK2_skl))
| greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f486,f61]) ).
fof(f495,plain,
( ~ sQ5_spl
| ~ sQ45_spl
| sQ38_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f493,f292,f295,f344,f103]) ).
fof(f501,plain,
( ~ sQ46_spl
| ~ sQ38_spl
| greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero) ),
inference(backward_demodulation,[status(thm)],[f296,f348]) ).
fof(f508,plain,
( ~ sQ46_spl
| ~ sQ38_spl
| sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f501,f251]) ).
fof(f509,plain,
( ~ sQ46_spl
| ~ sQ38_spl
| sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f508]) ).
fof(f510,plain,
( ~ sQ16_spl
| ~ sQ64_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f476,f150,f470,f168]) ).
fof(f565,plain,
( ~ sQ5_spl
| ~ sQ44_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f372,f147,f335,f103]) ).
fof(f566,plain,
( ~ sQ7_spl
| ~ sQ5_spl
| in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl)))
| greater(critical_point(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f395,f118]) ).
fof(f567,plain,
( ~ sQ7_spl
| ~ sQ5_spl
| sQ45_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f566,f283,f344,f103,f117]) ).
fof(f582,plain,
! [X0,X1] :
( ~ sQ59_spl
| selection_favors(efficient_producers,X1,appear(efficient_producers,sK0_skl(sK2_skl)))
| cardinality_at_time(X1,appear(efficient_producers,sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X1,X0,appear(efficient_producers,sK0_skl(sK2_skl)))
| ~ subpopulation(efficient_producers,X0,appear(efficient_producers,sK0_skl(sK2_skl)))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[f439,f26]) ).
fof(f605,plain,
( ~ sQ5_spl
| ~ sQ41_spl
| end_time(sK0_skl(sK2_skl)) = end_time(sK0_skl(sK2_skl))
| greater(end_time(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl)))
| greater(end_time(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f323,f394]) ).
fof(f609,definition,
( sQ73_spl
<=> greater(end_time(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f612,definition,
( sQ74_spl
<=> end_time(sK0_skl(sK2_skl)) = end_time(sK0_skl(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f615,plain,
( ~ sQ5_spl
| ~ sQ41_spl
| sQ74_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f605,f609,f612,f322,f103]) ).
fof(f648,plain,
( ~ sQ25_spl
| ~ sQ7_spl
| greater(sK1_skl(sK0_skl(sK2_skl),sK2_skl),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f134,f214]) ).
fof(f649,plain,
( ~ sQ37_spl
| ~ sQ7_spl
| greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f134,f293]) ).
fof(f683,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ7_spl
| greater(X0,start_time(sK0_skl(sK2_skl)))
| ~ greater(X0,sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
inference(resolution,[status(thm)],[f648,f56]) ).
fof(f694,plain,
( ~ sQ25_spl
| ~ sQ64_spl
| greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
inference(backward_demodulation,[status(thm)],[f471,f214]) ).
fof(f699,plain,
( ~ sQ37_spl
| ~ sQ7_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f649,f322,f117,f292]) ).
fof(f700,plain,
( sQ11_spl
| ~ sQ8_spl
| ~ sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f223,f293]) ).
fof(f701,plain,
( sQ11_spl
| ~ sQ8_spl
| ~ sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f700]) ).
fof(f709,plain,
( sQ54_spl
| ~ sQ8_spl
| ~ greater(cardinality_at_time(efficient_producers,critical_point(sK0_skl(sK2_skl))),zero) ),
inference(backward_demodulation,[status(thm)],[f121,f415]) ).
fof(f713,plain,
( sQ54_spl
| ~ sQ8_spl
| ~ sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f709,f348]) ).
fof(f714,plain,
( sQ54_spl
| ~ sQ8_spl
| ~ sQ46_spl ),
inference(contradiction_clause,[status(thm)],[f713]) ).
fof(f724,plain,
( sQ36_spl
| ~ sQ5_spl
| ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f486]) ).
fof(f725,plain,
( sQ36_spl
| ~ sQ5_spl
| ~ sQ45_spl ),
inference(contradiction_clause,[status(thm)],[f724]) ).
fof(f727,definition,
( sQ84_spl
<=> greater_or_equal(end_time(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f729,plain,
( sQ84_spl
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f727]) ).
fof(f732,plain,
( ~ sQ44_spl
| ~ sQ8_spl
| in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl))) ),
inference(forward_demodulation,[status(thm)],[f121,f336]) ).
fof(f775,plain,
( ~ sQ44_spl
| ~ sQ8_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f732,f344,f120,f335]) ).
fof(f785,plain,
( ~ sQ25_spl
| ~ sQ64_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f694,f292,f470,f213]) ).
fof(f821,plain,
! [X0] :
( ~ sQ5_spl
| ~ greater(X0,start_time(sK0_skl(sK2_skl)))
| in_environment(sK0_skl(sK2_skl),X0)
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),X0) ),
inference(resolution,[status(thm)],[f126,f62]) ).
fof(f822,plain,
( ~ sQ5_spl
| in_environment(sK0_skl(sK2_skl),start_time(sK0_skl(sK2_skl)))
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f126,f93]) ).
fof(f823,plain,
( ~ sQ5_spl
| sQ44_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f822,f147,f335,f103]) ).
fof(f868,plain,
( ~ sQ5_spl
| ~ greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))
| in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f145,f114]) ).
fof(f871,plain,
( ~ sQ5_spl
| ~ greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))
| in_environment(sK0_skl(sK2_skl),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f145,f93]) ).
fof(f872,plain,
( ~ sQ5_spl
| ~ sQ37_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f868,f344,f292,f103]) ).
fof(f874,plain,
( ~ sQ5_spl
| ~ sQ41_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f871,f335,f322,f103]) ).
fof(f893,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f729,f93]) ).
fof(f894,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f893]) ).
fof(f895,plain,
( ~ sQ34_spl
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f264,f94]) ).
fof(f898,plain,
( ~ sQ34_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f895,f104]) ).
fof(f899,plain,
( ~ sQ34_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f898]) ).
fof(f900,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ9_spl
| greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ in_environment(sK0_skl(sK2_skl),X0)
| ~ greater(X0,critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f451,f426]) ).
fof(f901,plain,
! [X0,X1] :
( ~ sQ9_spl
| greater(X1,appear(efficient_producers,sK0_skl(sK2_skl)))
| ~ greater(X1,X0)
| ~ greater(X0,critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f451,f56]) ).
fof(f904,plain,
! [X0] :
( ~ sQ37_spl
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ subpopulations(first_movers,efficient_producers,sK0_skl(sK2_skl),X0)
| ~ environment(sK0_skl(sK2_skl))
| ~ greater(X0,end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f313,f95]) ).
fof(f906,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f904,f360,f103,f292]) ).
fof(f907,plain,
( ~ sQ63_spl
| ~ sQ25_spl
| greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f453,f468]) ).
fof(f908,plain,
( sQ56_spl
| ~ sQ41_spl
| ~ greater(appear(efficient_producers,sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f378,f430]) ).
fof(f913,plain,
( sQ56_spl
| ~ sQ41_spl
| ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f908,f432]) ).
fof(f914,plain,
( sQ56_spl
| ~ sQ41_spl
| ~ sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f913]) ).
fof(f917,plain,
! [X0,X1] :
( ~ sQ31_spl
| selection_favors(efficient_producers,X1,end_time(sK0_skl(sK2_skl)))
| cardinality_at_time(X1,end_time(sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X1,X0,end_time(sK0_skl(sK2_skl)))
| ~ subpopulation(efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[f250,f26]) ).
fof(f952,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ59_spl
| ~ in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))
| selection_favors(efficient_producers,X0,appear(efficient_producers,sK0_skl(sK2_skl)))
| cardinality_at_time(X0,appear(efficient_producers,sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X0,sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f582,f111]) ).
fof(f953,definition,
! [X0] :
( sQ89_spl
<=> ( selection_favors(efficient_producers,X0,appear(efficient_producers,sK0_skl(sK2_skl)))
| cardinality_at_time(X0,appear(efficient_producers,sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X0,sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f954,plain,
! [X0] :
( ~ sQ89_spl
| selection_favors(efficient_producers,X0,appear(efficient_producers,sK0_skl(sK2_skl)))
| cardinality_at_time(X0,appear(efficient_producers,sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X0,sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f953]) ).
fof(f956,plain,
( ~ sQ59_spl
| ~ sQ58_spl
| sQ89_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f952,f103,f953,f435,f438]) ).
fof(f959,plain,
( ~ sQ63_spl
| ~ sQ25_spl
| ~ sQ7_spl
| greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f683,f468]) ).
fof(f961,plain,
! [X0] :
( ~ sQ40_spl
| selection_favors(efficient_producers,first_movers,end_time(sK0_skl(sK2_skl)))
| ~ subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[f318,f23]) ).
fof(f963,definition,
! [X0] :
( sQ90_spl
<=> ( ~ subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| ~ environment(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f964,plain,
! [X0] :
( ~ sQ90_spl
| ~ subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| ~ environment(X0) ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f966,definition,
( sQ91_spl
<=> selection_favors(efficient_producers,first_movers,end_time(sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f967,plain,
( ~ sQ91_spl
| selection_favors(efficient_producers,first_movers,end_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f966]) ).
fof(f969,plain,
( ~ sQ40_spl
| sQ91_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f961,f963,f966,f317]) ).
fof(f970,plain,
( ~ sQ4_spl
| ~ sQ91_spl
| selection_favors(efficient_producers,first_movers,sK2_skl)
| ~ observational_period(sK2_skl) ),
inference(resolution,[status(thm)],[f967,f90]) ).
fof(f971,plain,
( ~ sQ4_spl
| ~ sQ91_spl
| sQ6_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f970,f162,f106,f966,f89]) ).
fof(f972,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ46_spl
| ~ in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl)))
| selection_favors(efficient_producers,X0,critical_point(sK0_skl(sK2_skl)))
| cardinality_at_time(X0,critical_point(sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X0,sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl)))
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f386,f111]) ).
fof(f973,definition,
! [X0] :
( sQ92_spl
<=> ( selection_favors(efficient_producers,X0,critical_point(sK0_skl(sK2_skl)))
| cardinality_at_time(X0,critical_point(sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X0,sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f976,plain,
( ~ sQ46_spl
| ~ sQ45_spl
| sQ92_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f972,f103,f973,f344,f347]) ).
fof(f990,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sQ9_spl
| greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ in_environment(sK0_skl(sK2_skl),X1)
| ~ greater(X1,X0)
| ~ greater(X0,critical_point(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f901,f426]) ).
fof(f1002,plain,
! [X0] :
( ~ sQ30_spl
| ~ sQ90_spl
| ~ in_environment(X0,end_time(sK0_skl(sK2_skl)))
| ~ environment(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f247,f964]) ).
fof(f1003,plain,
( ~ sQ12_spl
| ~ sQ30_spl
| ~ sQ90_spl
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f1002,f151]) ).
fof(f1004,plain,
( ~ sQ12_spl
| ~ sQ30_spl
| ~ sQ90_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1003,f104]) ).
fof(f1005,plain,
( ~ sQ12_spl
| ~ sQ30_spl
| ~ sQ90_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1004]) ).
fof(f1006,plain,
( ~ sQ63_spl
| ~ sQ25_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f907,f292,f213,f467]) ).
fof(f1200,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| ~ sQ9_spl
| greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)
| ~ in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f900,f293]) ).
fof(f1202,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| ~ sQ9_spl
| sQ31_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1200,f150,f249,f138,f103,f292]) ).
fof(f1207,plain,
( sQ58_spl
| ~ sQ10_spl
| ~ in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl))) ),
inference(backward_demodulation,[status(thm)],[f142,f437]) ).
fof(f1210,plain,
( sQ58_spl
| ~ sQ10_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f1207,f344,f141,f435]) ).
fof(f1234,plain,
( ~ sQ5_spl
| ~ sQ45_spl
| ~ sQ10_spl
| greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)
| ~ in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f277,f486]) ).
fof(f1237,plain,
( ~ sQ5_spl
| ~ sQ45_spl
| ~ sQ10_spl
| sQ31_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1234,f150,f249,f141,f344,f103]) ).
fof(f1239,plain,
( sQ41_spl
| ~ sQ8_spl
| ~ greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))) ),
inference(forward_demodulation,[status(thm)],[f121,f324]) ).
fof(f1240,plain,
( sQ41_spl
| ~ sQ8_spl
| ~ sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1239,f293]) ).
fof(f1241,plain,
( sQ41_spl
| ~ sQ8_spl
| ~ sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f1240]) ).
fof(f1253,plain,
! [X0] :
( ~ sQ5_spl
| ~ greater(X0,start_time(sK0_skl(sK2_skl)))
| in_environment(sK0_skl(sK2_skl),X0)
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),X0) ),
inference(resolution,[status(thm)],[f126,f62]) ).
fof(f1282,plain,
( ~ sQ63_spl
| ~ sQ25_spl
| ~ sQ7_spl
| ~ sQ5_spl
| in_environment(sK0_skl(sK2_skl),start_time(sK0_skl(sK2_skl)))
| ~ greater_or_equal(start_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f145,f959]) ).
fof(f1285,plain,
( ~ sQ63_spl
| ~ sQ25_spl
| ~ sQ7_spl
| ~ sQ5_spl
| sQ44_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1282,f332,f335,f103,f117,f213,f467]) ).
fof(f1304,plain,
( ~ sQ5_spl
| ~ sQ56_spl
| in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f429,f821]) ).
fof(f1307,definition,
( sQ96_spl
<=> greater_or_equal(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1310,plain,
( ~ sQ5_spl
| ~ sQ56_spl
| sQ58_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f1304,f1307,f435,f428,f103]) ).
fof(f1363,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ8_spl
| ~ greater(X0,critical_point(sK0_skl(sK2_skl)))
| in_environment(sK0_skl(sK2_skl),X0)
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),X0) ),
inference(forward_demodulation,[status(thm)],[f121,f1253]) ).
fof(f1365,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| ~ sQ8_spl
| in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))
| ~ greater_or_equal(end_time(sK0_skl(sK2_skl)),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f1363,f293]) ).
fof(f1367,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| ~ sQ8_spl
| sQ12_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f1365,f727,f150,f120,f103,f292]) ).
fof(f1409,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ5_spl
| ~ sQ9_spl
| greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ in_environment(sK0_skl(sK2_skl),X0)
| ~ greater(X0,sK1_skl(sK0_skl(sK2_skl),sK2_skl)) ),
inference(resolution,[status(thm)],[f990,f214]) ).
fof(f1416,plain,
( ~ sQ63_spl
| ~ sQ25_spl
| ~ sQ5_spl
| ~ sQ9_spl
| greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)
| ~ in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
inference(resolution,[status(thm)],[f1409,f468]) ).
fof(f1418,plain,
( ~ sQ63_spl
| ~ sQ25_spl
| ~ sQ5_spl
| ~ sQ9_spl
| sQ31_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1416,f150,f249,f138,f103,f213,f467]) ).
fof(f1419,plain,
( ~ sQ5_spl
| ~ sQ89_spl
| ~ in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))
| selection_favors(efficient_producers,first_movers,appear(efficient_producers,sK0_skl(sK2_skl)))
| cardinality_at_time(first_movers,appear(efficient_producers,sK0_skl(sK2_skl))) != zero ),
inference(resolution,[status(thm)],[f954,f112]) ).
fof(f1420,plain,
( ~ sQ5_spl
| ~ sQ89_spl
| ~ in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))
| selection_favors(efficient_producers,efficient_producers,appear(efficient_producers,sK0_skl(sK2_skl)))
| cardinality_at_time(efficient_producers,appear(efficient_producers,sK0_skl(sK2_skl))) != zero ),
inference(resolution,[status(thm)],[f954,f111]) ).
fof(f1421,definition,
( sQ97_spl
<=> cardinality_at_time(first_movers,appear(efficient_producers,sK0_skl(sK2_skl))) = zero ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1424,definition,
( sQ98_spl
<=> selection_favors(efficient_producers,first_movers,appear(efficient_producers,sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1427,plain,
( ~ sQ5_spl
| ~ sQ89_spl
| ~ sQ58_spl
| sQ98_spl
| ~ sQ97_spl ),
inference(split_clause,[status(thm)],[f1419,f1421,f1424,f435,f953,f103]) ).
fof(f1428,definition,
( sQ99_spl
<=> cardinality_at_time(efficient_producers,appear(efficient_producers,sK0_skl(sK2_skl))) = zero ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1431,definition,
( sQ100_spl
<=> selection_favors(efficient_producers,efficient_producers,appear(efficient_producers,sK0_skl(sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1434,plain,
( ~ sQ5_spl
| ~ sQ89_spl
| ~ sQ58_spl
| sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f1420,f1428,f1431,f435,f953,f103]) ).
fof(f1594,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ31_spl
| ~ in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))
| selection_favors(efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| cardinality_at_time(X0,end_time(sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X0,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f917,f111]) ).
fof(f1595,definition,
! [X0] :
( sQ113_spl
<=> ( selection_favors(efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| cardinality_at_time(X0,end_time(sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X0,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1596,plain,
! [X0] :
( ~ sQ113_spl
| selection_favors(efficient_producers,X0,end_time(sK0_skl(sK2_skl)))
| cardinality_at_time(X0,end_time(sK0_skl(sK2_skl))) != zero
| ~ subpopulation(X0,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))) ),
inference(component_clause,[status(thm)],[f1595]) ).
fof(f1598,plain,
( ~ sQ31_spl
| ~ sQ12_spl
| sQ113_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1594,f103,f1595,f150,f249]) ).
fof(f1614,plain,
( ~ sQ5_spl
| ~ sQ113_spl
| ~ in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))
| selection_favors(efficient_producers,first_movers,end_time(sK0_skl(sK2_skl)))
| cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))) != zero ),
inference(resolution,[status(thm)],[f1596,f112]) ).
fof(f1616,plain,
( ~ sQ5_spl
| ~ sQ113_spl
| ~ sQ12_spl
| sQ91_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f1614,f239,f966,f150,f1595,f103]) ).
fof(f1627,plain,
( ~ sQ12_spl
| ~ sQ30_spl
| subpopulations(first_movers,efficient_producers,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))
| ~ environment(sK0_skl(sK2_skl)) ),
inference(resolution,[status(thm)],[f247,f151]) ).
fof(f1629,plain,
( ~ sQ12_spl
| ~ sQ30_spl
| sQ39_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1627,f103,f314,f246,f150]) ).
fof(f1631,plain,
$false,
inference(sat_refutation,[status(thm)],[f84,f88,f92,f97,f99,f109,f123,f125,f144,f153,f159,f171,f209,f211,f216,f222,f233,f242,f270,f320,f328,f341,f359,f377,f434,f441,f444,f473,f485,f491,f495,f509,f510,f565,f567,f615,f699,f701,f714,f725,f775,f785,f823,f872,f874,f894,f899,f906,f914,f956,f969,f971,f976,f1005,f1006,f1202,f1210,f1237,f1241,f1285,f1310,f1367,f1418,f1427,f1434,f1598,f1616,f1629]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.96 % Computer : n012.cluster.edu
% 0.09/5.96 % Model : x86_64 x86_64
% 0.09/5.96 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.96 % Memory : 8046.5625MB
% 0.09/5.96 % OS : Linux 6.8.0-71-generic
% 0.09/5.96 % CPULimit : 300
% 0.09/5.96 % WCLimit : 300
% 0.09/5.96 % DateTime : Mon Sep 21 01:22:43 UTC 2026
% 0.09/5.97 % CPUTime :
% 0.09/5.98 % Drodi V4.1.1
% 0.21/6.10 % Refutation found
% 0.21/6.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/6.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/6.14 % Elapsed time: 0.165172 seconds
% 0.19/6.14 % CPU time: 0.791242 seconds
% 0.19/6.14 % Total memory used: 96.100 MB
% 0.19/6.14 % Net memory used: 94.950 MB
%------------------------------------------------------------------------------