%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 : Sun Sep 27 08:02:55 AM UTC 2026
% Result : Theorem 0.15s 5.58s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 152
% Number of leaves : 18
% Syntax : Number of formulae : 426 ( 26 unt; 0 def)
% Number of atoms : 1844 ( 740 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1930 ( 512 ~;1355 |; 43 &)
% ( 1 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-2 aty)
% Number of variables : 233 ( 0 sgn 49 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mp1_high_growth_rates,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('theBenchmark.p',mp1_high_growth_rates) ).
fof(mp2_favour_members,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('theBenchmark.p',mp2_favour_members) ).
fof(mp3_favoured_trategy,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('theBenchmark.p',mp3_favoured_trategy) ).
fof(mp4_critical_point,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('theBenchmark.p',mp4_critical_point) ).
fof(mp_time_in_environment,axiom,
! [E,T] :
( ( greater_or_equal(end_time(E),T)
& greater_or_equal(T,start_time(E))
& environment(E) )
=> in_environment(E,T) ),
file('theBenchmark.p',mp_time_in_environment) ).
fof(mp_environment_end_point,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> greater_or_equal(end_time(E),T) ),
file('theBenchmark.p',mp_environment_end_point) ).
fof(mp_contains_FM_and_EP,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('theBenchmark.p',mp_contains_FM_and_EP) ).
fof(mp_first_movers_exist,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> greater_or_equal(cardinality_at_time(first_movers,T),zero) ),
file('theBenchmark.p',mp_first_movers_exist) ).
fof(mp_subpopulations,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> ( subpopulation(efficient_producers,E,T)
& subpopulation(first_movers,E,T) ) ),
file('theBenchmark.p',mp_subpopulations) ).
fof(mp_critical_point_after_EP,axiom,
! [E] :
( environment(E)
=> greater_or_equal(critical_point(E),appear(efficient_producers,E)) ),
file('theBenchmark.p',mp_critical_point_after_EP) ).
fof(mp_time_of_critical_point,axiom,
! [E] :
( environment(E)
=> greater_or_equal(critical_point(E),start_time(E)) ),
file('theBenchmark.p',mp_time_of_critical_point) ).
fof(mp_greater_transitivity,axiom,
! [X,Y,Z] :
( ( greater(Y,Z)
& greater(X,Y) )
=> greater(X,Z) ),
file('theBenchmark.p',mp_greater_transitivity) ).
fof(mp_greater_or_equal,axiom,
! [X,Y] :
( greater_or_equal(X,Y)
<=> ( X = Y
| greater(X,Y) ) ),
file('theBenchmark.p',mp_greater_or_equal) ).
fof(d1,axiom,
! [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('theBenchmark.p',d1) ).
fof(t6,axiom,
! [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('theBenchmark.p',t6) ).
fof(prove_t8,conjecture,
! [P] :
( ( slow_change(P)
& observational_period(P) )
=> selection_favors(efficient_producers,first_movers,P) ),
file('theBenchmark.p',prove_t8) ).
fof(prove_t8_neg,negated_conjecture,
~ ! [P] :
( ( slow_change(P)
& observational_period(P) )
=> selection_favors(efficient_producers,first_movers,P) ),
inference(assume_negation,[status(cth)],[prove_t8]) ).
fof(nnf_3,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(fof_nnf,[status(thm)],[mp3_favoured_trategy]) ).
fof(sk_mp3_favoured_trategy_sk,plain,
! [P] :
( selection_favors(efficient_producers,first_movers,P)
| ( ~ selection_favors(efficient_producers,first_movers,end_time(sK0(P)))
& in_environment(P,sK0(P))
& environment(sK0(P)) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(E,sK0(P))],[nnf_3]) ).
fof(sk_mp3_favoured_trategy,plain,
( ! [VAR_0] :
( selection_favors(efficient_producers,first_movers,VAR_0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(VAR_0)))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(VAR_0) )
& ! [VAR_0] :
( selection_favors(efficient_producers,first_movers,VAR_0)
| in_environment(VAR_0,sK0(VAR_0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(VAR_0) )
& ! [VAR_0] :
( selection_favors(efficient_producers,first_movers,VAR_0)
| environment(sK0(VAR_0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mp3_favoured_trategy_sk]) ).
cnf(c_18,plain,
( selection_favors(efficient_producers,first_movers,A)
| environment(sK0(A))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A) ),
inference(split_conjunct,[status(thm)],[sk_mp3_favoured_trategy]) ).
cnf(c_19,plain,
( selection_favors(B,D,C)
| cardinality_at_time(D,C) != zero
| ~ greater(cardinality_at_time(B,C),zero)
| ~ subpopulation(D,A,C)
| ~ subpopulation(B,A,C)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp2_favour_members]) ).
cnf(c_20,plain,
( selection_favors(C,B,D)
| ~ greater(growth_rate(C,D),growth_rate(B,D))
| ~ subpopulations(B,C,A,D)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp1_high_growth_rates]) ).
fof(nnf_4,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(fof_nnf,[status(thm)],[mp4_critical_point]) ).
fof(sk_mp4_critical_point_sk,plain,
! [P] :
( ! [E] :
( ( greater(sK1(P,E),critical_point(E))
& in_environment(E,sK1(P,E)) )
| ~ in_environment(P,E)
| ~ environment(E) )
| ~ slow_change(P)
| ~ observational_period(P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(T,sK1(P,E))],[nnf_4]) ).
fof(sk_mp4_critical_point,plain,
( ! [VAR_0,VAR_1] :
( greater(sK1(VAR_0,VAR_1),critical_point(VAR_1))
| ~ in_environment(VAR_0,VAR_1)
| ~ environment(VAR_1)
| ~ slow_change(VAR_0)
| ~ observational_period(VAR_0) )
& ! [VAR_0,VAR_1] :
( in_environment(VAR_1,sK1(VAR_0,VAR_1))
| ~ in_environment(VAR_0,VAR_1)
| ~ environment(VAR_1)
| ~ slow_change(VAR_0)
| ~ observational_period(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mp4_critical_point_sk]) ).
cnf(c_21,plain,
( in_environment(B,sK1(A,B))
| ~ in_environment(A,B)
| ~ environment(B)
| ~ slow_change(A)
| ~ observational_period(A) ),
inference(split_conjunct,[status(thm)],[sk_mp4_critical_point]) ).
cnf(c_22,plain,
( greater(sK1(A,B),critical_point(B))
| ~ in_environment(A,B)
| ~ environment(B)
| ~ slow_change(A)
| ~ observational_period(A) ),
inference(split_conjunct,[status(thm)],[sk_mp4_critical_point]) ).
cnf(c_23,plain,
( in_environment(A,B)
| ~ greater_or_equal(end_time(A),B)
| ~ greater_or_equal(B,start_time(A))
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_time_in_environment]) ).
cnf(c_24,plain,
( greater_or_equal(end_time(A),B)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_environment_end_point]) ).
cnf(c_25,plain,
( subpopulations(first_movers,efficient_producers,A,B)
| ~ greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_contains_FM_and_EP]) ).
cnf(c_26,plain,
( greater_or_equal(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_first_movers_exist]) ).
cnf(c_27,plain,
( subpopulation(first_movers,A,B)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_subpopulations]) ).
cnf(c_28,plain,
( subpopulation(efficient_producers,A,B)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_subpopulations]) ).
cnf(c_29,plain,
( greater_or_equal(critical_point(A),appear(efficient_producers,A))
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_critical_point_after_EP]) ).
cnf(c_30,plain,
( greater_or_equal(critical_point(A),start_time(A))
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_time_of_critical_point]) ).
cnf(c_33,plain,
( greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C))
| ~ greater(C,B)
| ~ subpopulations(first_movers,efficient_producers,A,C)
| critical_point(A) != B
| ~ environment(A) ),
inference(clausify,[status(thm)],[d1]) ).
cnf(c_34,plain,
( greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater_or_equal(B,appear(efficient_producers,A))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[t6]) ).
fof(nnf_17,plain,
? [P] :
( ~ selection_favors(efficient_producers,first_movers,P)
& slow_change(P)
& observational_period(P) ),
inference(fof_nnf,[status(thm)],[prove_t8_neg]) ).
fof(sk_prove_t8_neg,plain,
( ~ selection_favors(efficient_producers,first_movers,sK2)
& slow_change(sK2)
& observational_period(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(P,sK2)],[nnf_17]) ).
cnf(c_35,negated_conjecture,
slow_change(sK2),
inference(split_conjunct,[status(thm)],[sk_prove_t8_neg]) ).
cnf(c_36,plain,
( selection_favors(efficient_producers,first_movers,B)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(B)
| in_environment(sK0(B),sK1(A,sK0(B)))
| ~ in_environment(A,sK0(B))
| ~ slow_change(A)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_21,c_18]) ).
cnf(c_37,plain,
( selection_favors(efficient_producers,first_movers,B)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(B)
| greater(sK1(A,sK0(B)),critical_point(sK0(B)))
| ~ in_environment(A,sK0(B))
| ~ slow_change(A)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_22,c_18]) ).
cnf(c_38,negated_conjecture,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| greater(sK1(sK2,sK0(A)),critical_point(sK0(A)))
| ~ in_environment(sK2,sK0(A))
| ~ observational_period(sK2) ),
inference(resolve,[status(thm)],[c_35,c_37]) ).
cnf(c_39,negated_conjecture,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| in_environment(sK0(A),sK1(sK2,sK0(A)))
| ~ in_environment(sK2,sK0(A))
| ~ observational_period(sK2) ),
inference(resolve,[status(thm)],[c_35,c_36]) ).
cnf(c_40,plain,
( selection_favors(efficient_producers,first_movers,A)
| in_environment(A,sK0(A))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A) ),
inference(split_conjunct,[status(thm)],[sk_mp3_favoured_trategy]) ).
cnf(c_41,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(A)))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A) ),
inference(split_conjunct,[status(thm)],[sk_mp3_favoured_trategy]) ).
fof(mp_organizational_sets1,axiom,
propagation_strategy(first_movers),
file('theBenchmark.p',mp_organizational_sets1) ).
cnf(c_42,plain,
propagation_strategy(first_movers),
inference(clausify,[status(thm)],[mp_organizational_sets1]) ).
fof(mp_organizational_sets2,axiom,
propagation_strategy(efficient_producers),
file('theBenchmark.p',mp_organizational_sets2) ).
cnf(c_43,plain,
propagation_strategy(efficient_producers),
inference(clausify,[status(thm)],[mp_organizational_sets2]) ).
cnf(c_44,plain,
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
inference(clausify,[status(thm)],[mp_greater_transitivity]) ).
cnf(c_45,plain,
( B = A
| greater(A,B)
| ~ greater_or_equal(A,B) ),
inference(clausify,[status(thm)],[mp_greater_or_equal]) ).
cnf(c_46,plain,
( ~ greater(A,B)
| greater_or_equal(A,B) ),
inference(clausify,[status(thm)],[mp_greater_or_equal]) ).
cnf(c_47,plain,
( B != A
| greater_or_equal(A,B) ),
inference(clausify,[status(thm)],[mp_greater_or_equal]) ).
cnf(c_48,negated_conjecture,
observational_period(sK2),
inference(split_conjunct,[status(thm)],[sk_prove_t8_neg]) ).
cnf(c_49,negated_conjecture,
~ selection_favors(efficient_producers,first_movers,sK2),
inference(split_conjunct,[status(thm)],[sk_prove_t8_neg]) ).
cnf(c_50,plain,
( selection_favors(B,D,C)
| cardinality_at_time(D,C) != zero
| ~ greater(cardinality_at_time(B,C),zero)
| ~ subpopulation(D,sK0(A),C)
| ~ subpopulation(B,sK0(A),C)
| selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_18,c_19]) ).
cnf(c_671,plain,
( selection_favors(B,D,C)
| cardinality_at_time(D,C) != zero
| ~ greater(cardinality_at_time(B,C),zero)
| ~ subpopulation(D,sK0(A),C)
| ~ subpopulation(B,sK0(A),C)
| selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_42,c_50]) ).
cnf(c_51,plain,
( selection_favors(B,D,C)
| cardinality_at_time(D,C) != zero
| ~ greater(cardinality_at_time(B,C),zero)
| ~ subpopulation(D,sK0(A),C)
| ~ subpopulation(B,sK0(A),C)
| selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_43,c_671]) ).
cnf(c_52,plain,
( selection_favors(C,B,D)
| ~ greater(growth_rate(C,D),growth_rate(B,D))
| ~ subpopulations(B,C,sK0(A),D)
| selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_18,c_20]) ).
cnf(c_672,plain,
( selection_favors(C,B,D)
| ~ greater(growth_rate(C,D),growth_rate(B,D))
| ~ subpopulations(B,C,sK0(A),D)
| selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_42,c_52]) ).
cnf(c_53,plain,
( selection_favors(C,B,D)
| ~ greater(growth_rate(C,D),growth_rate(B,D))
| ~ subpopulations(B,C,sK0(A),D)
| selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_43,c_672]) ).
cnf(c_54,plain,
( selection_favors(efficient_producers,first_movers,B)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(B)
| in_environment(sK0(B),A)
| ~ greater_or_equal(end_time(sK0(B)),A)
| ~ greater_or_equal(A,start_time(sK0(B))) ),
inference(resolve,[status(thm)],[c_23,c_18]) ).
cnf(c_673,plain,
( selection_favors(efficient_producers,first_movers,B)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(B)
| in_environment(sK0(B),A)
| ~ greater_or_equal(end_time(sK0(B)),A)
| ~ greater_or_equal(A,start_time(sK0(B))) ),
inference(resolve,[status(thm)],[c_42,c_54]) ).
cnf(c_55,plain,
( selection_favors(efficient_producers,first_movers,B)
| ~ observational_period(B)
| in_environment(sK0(B),A)
| ~ greater_or_equal(end_time(sK0(B)),A)
| ~ greater_or_equal(A,start_time(sK0(B))) ),
inference(resolve,[status(thm)],[c_43,c_673]) ).
cnf(c_56,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| greater_or_equal(end_time(sK0(A)),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_24,c_18]) ).
cnf(c_674,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| greater_or_equal(end_time(sK0(A)),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_42,c_56]) ).
cnf(c_57,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater_or_equal(end_time(sK0(A)),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_43,c_674]) ).
cnf(c_58,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| subpopulations(first_movers,efficient_producers,sK0(A),B)
| ~ greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_25,c_18]) ).
cnf(c_675,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| subpopulations(first_movers,efficient_producers,sK0(A),B)
| ~ greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_42,c_58]) ).
cnf(c_59,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| subpopulations(first_movers,efficient_producers,sK0(A),B)
| ~ greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_43,c_675]) ).
cnf(c_60,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| greater_or_equal(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_26,c_18]) ).
cnf(c_676,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| greater_or_equal(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_42,c_60]) ).
cnf(c_61,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater_or_equal(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_43,c_676]) ).
cnf(c_62,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| subpopulation(first_movers,sK0(A),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_27,c_18]) ).
cnf(c_677,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| subpopulation(first_movers,sK0(A),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_42,c_62]) ).
cnf(c_63,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| subpopulation(first_movers,sK0(A),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_43,c_677]) ).
cnf(c_64,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| subpopulation(efficient_producers,sK0(A),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_28,c_18]) ).
cnf(c_678,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| subpopulation(efficient_producers,sK0(A),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_42,c_64]) ).
cnf(c_65,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| subpopulation(efficient_producers,sK0(A),B)
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_43,c_678]) ).
cnf(c_66,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| greater_or_equal(critical_point(sK0(A)),appear(efficient_producers,sK0(A))) ),
inference(resolve,[status(thm)],[c_29,c_18]) ).
cnf(c_679,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| greater_or_equal(critical_point(sK0(A)),appear(efficient_producers,sK0(A))) ),
inference(resolve,[status(thm)],[c_42,c_66]) ).
cnf(c_67,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater_or_equal(critical_point(sK0(A)),appear(efficient_producers,sK0(A))) ),
inference(resolve,[status(thm)],[c_43,c_679]) ).
cnf(c_68,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| greater_or_equal(critical_point(sK0(A)),start_time(sK0(A))) ),
inference(resolve,[status(thm)],[c_30,c_18]) ).
cnf(c_680,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| greater_or_equal(critical_point(sK0(A)),start_time(sK0(A))) ),
inference(resolve,[status(thm)],[c_42,c_68]) ).
cnf(c_69,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater_or_equal(critical_point(sK0(A)),start_time(sK0(A))) ),
inference(resolve,[status(thm)],[c_43,c_680]) ).
cnf(c_74,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C))
| ~ greater(C,B)
| ~ subpopulations(first_movers,efficient_producers,sK0(A),C)
| critical_point(sK0(A)) != B ),
inference(resolve,[status(thm)],[c_33,c_18]) ).
cnf(c_681,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C))
| ~ greater(C,B)
| ~ subpopulations(first_movers,efficient_producers,sK0(A),C)
| critical_point(sK0(A)) != B ),
inference(resolve,[status(thm)],[c_42,c_74]) ).
cnf(c_75,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C))
| ~ greater(C,B)
| ~ subpopulations(first_movers,efficient_producers,sK0(A),C)
| critical_point(sK0(A)) != B ),
inference(resolve,[status(thm)],[c_43,c_681]) ).
cnf(c_76,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(A)
| greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater_or_equal(B,appear(efficient_producers,sK0(A)))
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_34,c_18]) ).
cnf(c_682,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A)
| greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater_or_equal(B,appear(efficient_producers,sK0(A)))
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_42,c_76]) ).
cnf(c_77,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater_or_equal(B,appear(efficient_producers,sK0(A)))
| ~ in_environment(sK0(A),B) ),
inference(resolve,[status(thm)],[c_43,c_682]) ).
cnf(c_683,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2))
| ~ observational_period(sK2) ),
inference(factor,[status(thm)],[c_38]) ).
cnf(c_684,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_683]) ).
cnf(c_685,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ propagation_strategy(efficient_producers)
| greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_42,c_684]) ).
cnf(c_686,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_43,c_685]) ).
cnf(c_78,negated_conjecture,
( greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_686]) ).
cnf(c_687,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| in_environment(sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2))
| ~ observational_period(sK2) ),
inference(factor,[status(thm)],[c_39]) ).
cnf(c_688,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| in_environment(sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_687]) ).
cnf(c_689,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ propagation_strategy(efficient_producers)
| in_environment(sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_42,c_688]) ).
cnf(c_690,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| in_environment(sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_43,c_689]) ).
cnf(c_79,negated_conjecture,
( in_environment(sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_690]) ).
cnf(c_691,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(A)))
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_42,c_41]) ).
cnf(c_80,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(A)))
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_43,c_691]) ).
cnf(c_692,plain,
( selection_favors(efficient_producers,first_movers,A)
| in_environment(A,sK0(A))
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_42,c_40]) ).
cnf(c_81,plain,
( selection_favors(efficient_producers,first_movers,A)
| in_environment(A,sK0(A))
| ~ observational_period(A) ),
inference(resolve,[status(thm)],[c_43,c_692]) ).
cnf(c_87,plain,
greater_or_equal(A,A),
inference(xxres,[status(thm)],[c_47]) ).
cnf(c_693,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater_or_equal(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_67,c_48]) ).
cnf(c_88,negated_conjecture,
greater_or_equal(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2))),
inference(resolve,[status(thm)],[c_49,c_693]) ).
cnf(c_694,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater_or_equal(critical_point(sK0(sK2)),start_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_69,c_48]) ).
cnf(c_89,negated_conjecture,
greater_or_equal(critical_point(sK0(sK2)),start_time(sK0(sK2))),
inference(resolve,[status(thm)],[c_49,c_694]) ).
cnf(c_695,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_80,c_48]) ).
cnf(c_91,negated_conjecture,
~ selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))),
inference(resolve,[status(thm)],[c_695,c_49]) ).
cnf(c_696,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| in_environment(sK2,sK0(sK2)) ),
inference(resolve,[status(thm)],[c_81,c_48]) ).
cnf(c_92,negated_conjecture,
in_environment(sK2,sK0(sK2)),
inference(resolve,[status(thm)],[c_49,c_696]) ).
cnf(c_93,negated_conjecture,
in_environment(sK0(sK2),sK1(sK2,sK0(sK2))),
inference(resolve,[status(thm)],[c_92,c_79]) ).
cnf(c_94,negated_conjecture,
greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2))),
inference(resolve,[status(thm)],[c_92,c_78]) ).
cnf(c_95,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| in_environment(sK0(A),end_time(sK0(A)))
| ~ greater_or_equal(end_time(sK0(A)),start_time(sK0(A))) ),
inference(resolve,[status(thm)],[c_87,c_55]) ).
cnf(c_98,plain,
( start_time(sK0(sK2)) = critical_point(sK0(sK2))
| greater(critical_point(sK0(sK2)),start_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_89,c_45]) ).
cnf(c_697,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ greater_or_equal(sK1(sK2,sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_93,c_77]) ).
cnf(c_698,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ greater_or_equal(sK1(sK2,sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_48,c_697]) ).
cnf(c_99,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ greater_or_equal(sK1(sK2,sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_698]) ).
cnf(c_699,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulation(efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_93,c_65]) ).
cnf(c_700,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulation(efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_48,c_699]) ).
cnf(c_100,negated_conjecture,
subpopulation(efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2))),
inference(resolve,[status(thm)],[c_49,c_700]) ).
cnf(c_701,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulation(first_movers,sK0(sK2),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_93,c_63]) ).
cnf(c_702,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulation(first_movers,sK0(sK2),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_48,c_701]) ).
cnf(c_101,negated_conjecture,
subpopulation(first_movers,sK0(sK2),sK1(sK2,sK0(sK2))),
inference(resolve,[status(thm)],[c_49,c_702]) ).
cnf(c_703,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater_or_equal(cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_93,c_61]) ).
cnf(c_704,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater_or_equal(cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_48,c_703]) ).
cnf(c_102,negated_conjecture,
greater_or_equal(cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))),zero),
inference(resolve,[status(thm)],[c_49,c_704]) ).
cnf(c_705,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_93,c_59]) ).
cnf(c_706,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_48,c_705]) ).
cnf(c_103,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_49,c_706]) ).
cnf(c_707,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater_or_equal(end_time(sK0(sK2)),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_93,c_57]) ).
cnf(c_708,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater_or_equal(end_time(sK0(sK2)),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_48,c_707]) ).
cnf(c_104,negated_conjecture,
greater_or_equal(end_time(sK0(sK2)),sK1(sK2,sK0(sK2))),
inference(resolve,[status(thm)],[c_49,c_708]) ).
cnf(c_105,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| greater(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_88,c_45]) ).
cnf(c_106,plain,
greater_or_equal(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2))),
inference(resolve,[status(thm)],[c_94,c_46]) ).
cnf(c_107,plain,
( greater(A,critical_point(sK0(sK2)))
| ~ greater(A,sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_94,c_44]) ).
cnf(c_108,plain,
( greater(sK1(sK2,sK0(sK2)),A)
| ~ greater(critical_point(sK0(sK2)),A) ),
inference(resolve,[status(thm)],[c_94,c_44]) ).
cnf(c_709,plain,
( selection_favors(efficient_producers,A,sK1(sK2,sK0(sK2)))
| cardinality_at_time(A,sK1(sK2,sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2) ),
inference(resolve,[status(thm)],[c_100,c_51]) ).
cnf(c_710,negated_conjecture,
( selection_favors(efficient_producers,A,sK1(sK2,sK0(sK2)))
| cardinality_at_time(A,sK1(sK2,sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_48,c_709]) ).
cnf(c_111,negated_conjecture,
( selection_favors(efficient_producers,A,sK1(sK2,sK0(sK2)))
| cardinality_at_time(A,sK1(sK2,sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_710]) ).
cnf(c_115,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(end_time(sK0(sK2)),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_104,c_45]) ).
cnf(c_711,plain,
( zero = cardinality_at_time(first_movers,sK1(sK2,sK0(sK2)))
| greater(cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_102,c_45]) ).
cnf(c_116,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| greater(cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))),zero) ),
inference(copy,[status(thm)],[c_711]) ).
cnf(c_117,plain,
( greater(sK1(sK2,sK0(sK2)),start_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_98,c_108]) ).
cnf(c_124,plain,
( greater(sK1(sK2,sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_105,c_108]) ).
cnf(c_127,plain,
( greater(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_115,c_107]) ).
cnf(c_712,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(end_time(sK0(sK2)),A)
| ~ greater(sK1(sK2,sK0(sK2)),A) ),
inference(resolve,[status(thm)],[c_44,c_115]) ).
cnf(c_130,plain,
( start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(end_time(sK0(sK2)),start_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_712,c_117]) ).
cnf(c_131,plain,
( greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_127,c_46]) ).
cnf(c_713,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(end_time(sK0(sK2)),A)
| ~ greater(critical_point(sK0(sK2)),A) ),
inference(resolve,[status(thm)],[c_44,c_127]) ).
cnf(c_134,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_713,c_105]) ).
cnf(c_147,plain,
( greater_or_equal(sK1(sK2,sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_124,c_46]) ).
cnf(c_150,plain,
( greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_147,c_99]) ).
cnf(c_156,plain,
( subpopulations(first_movers,efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero ),
inference(resolve,[status(thm)],[c_116,c_103]) ).
cnf(c_161,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_111,c_101]) ).
cnf(c_714,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_103,c_116]) ).
cnf(c_171,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_714,c_150]) ).
cnf(c_178,plain,
( greater_or_equal(end_time(sK0(sK2)),start_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_130,c_46]) ).
cnf(c_715,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| in_environment(sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_178,c_95]) ).
cnf(c_716,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| in_environment(sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_715]) ).
cnf(c_182,negated_conjecture,
( in_environment(sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_716]) ).
cnf(c_717,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_182,c_77]) ).
cnf(c_718,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_717]) ).
cnf(c_188,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_718]) ).
cnf(c_719,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulation(efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_182,c_65]) ).
cnf(c_720,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulation(efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_719]) ).
cnf(c_189,negated_conjecture,
( subpopulation(efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_720]) ).
cnf(c_721,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_182,c_63]) ).
cnf(c_722,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_721]) ).
cnf(c_190,negated_conjecture,
( subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_722]) ).
cnf(c_723,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater_or_equal(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_182,c_61]) ).
cnf(c_724,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater_or_equal(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_723]) ).
cnf(c_191,negated_conjecture,
( greater_or_equal(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_724]) ).
cnf(c_725,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_182,c_59]) ).
cnf(c_726,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_725]) ).
cnf(c_192,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_726]) ).
cnf(c_727,plain,
( selection_favors(efficient_producers,A,end_time(sK0(sK2)))
| cardinality_at_time(A,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_189,c_51]) ).
cnf(c_728,negated_conjecture,
( selection_favors(efficient_producers,A,end_time(sK0(sK2)))
| cardinality_at_time(A,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_727]) ).
cnf(c_201,negated_conjecture,
( selection_favors(efficient_producers,A,end_time(sK0(sK2)))
| cardinality_at_time(A,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_728]) ).
cnf(c_205,plain,
( greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_134,c_46]) ).
cnf(c_729,plain,
( start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_77,c_182]) ).
cnf(c_730,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_729,c_205]) ).
cnf(c_731,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_730,c_48]) ).
cnf(c_732,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(copy,[status(thm)],[c_731]) ).
cnf(c_209,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_49,c_732]) ).
cnf(c_733,plain,
( zero = cardinality_at_time(first_movers,end_time(sK0(sK2)))
| greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_191,c_45]) ).
cnf(c_220,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_733]) ).
cnf(c_228,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) != zero ),
inference(resolve,[status(thm)],[c_161,c_150]) ).
cnf(c_734,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater(B,critical_point(sK0(A)))
| ~ subpopulations(first_movers,efficient_producers,sK0(A),B) ),
inference(xxres,[status(thm)],[c_75]) ).
cnf(c_735,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2))))
| ~ greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_734,c_171]) ).
cnf(c_736,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_735,c_94]) ).
cnf(c_737,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_736,c_48]) ).
cnf(c_263,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_49,c_737]) ).
cnf(c_738,negated_conjecture,
( selection_favors(B,A,C)
| ~ greater(growth_rate(B,C),growth_rate(A,C))
| ~ subpopulations(A,B,sK0(sK2),C)
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_53,c_48]) ).
cnf(c_739,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_738,c_171]) ).
cnf(c_740,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_739,c_263]) ).
cnf(c_741,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_740]) ).
cnf(c_742,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_741]) ).
cnf(c_281,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_742]) ).
cnf(c_743,plain,
( start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_59,c_182]) ).
cnf(c_744,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_743,c_220]) ).
cnf(c_745,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_744,c_209]) ).
cnf(c_746,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_745,c_48]) ).
cnf(c_747,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(copy,[status(thm)],[c_746]) ).
cnf(c_748,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(copy,[status(thm)],[c_747]) ).
cnf(c_749,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(copy,[status(thm)],[c_748]) ).
cnf(c_750,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(copy,[status(thm)],[c_749]) ).
cnf(c_288,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_750]) ).
cnf(c_751,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_192,c_220]) ).
cnf(c_752,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_751]) ).
cnf(c_311,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_752]) ).
cnf(c_753,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_288,c_53]) ).
cnf(c_754,negated_conjecture,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2)
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_753]) ).
cnf(c_755,negated_conjecture,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_754]) ).
cnf(c_313,negated_conjecture,
( ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_755]) ).
cnf(c_756,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater(B,critical_point(sK0(A)))
| ~ subpopulations(first_movers,efficient_producers,sK0(A),B) ),
inference(xxres,[status(thm)],[c_75]) ).
cnf(c_757,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| ~ greater(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_756,c_288]) ).
cnf(c_758,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_757,c_127]) ).
cnf(c_759,negated_conjecture,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_758,c_48]) ).
cnf(c_760,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(copy,[status(thm)],[c_759]) ).
cnf(c_315,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_49,c_760]) ).
cnf(c_761,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_315,c_313]) ).
cnf(c_762,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_761]) ).
cnf(c_763,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_762]) ).
cnf(c_764,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_763]) ).
cnf(c_323,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_764]) ).
cnf(c_765,negated_conjecture,
( selection_favors(A,C,B)
| cardinality_at_time(C,B) != zero
| ~ greater(cardinality_at_time(A,B),zero)
| ~ subpopulation(C,sK0(sK2),B)
| ~ subpopulation(A,sK0(sK2),B)
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_51,c_48]) ).
cnf(c_766,negated_conjecture,
( start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,A,end_time(sK0(sK2)))
| cardinality_at_time(A,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_765,c_189]) ).
cnf(c_767,negated_conjecture,
( start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_766,c_190]) ).
cnf(c_768,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_767,c_209]) ).
cnf(c_769,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_768,c_323]) ).
cnf(c_770,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_769]) ).
cnf(c_771,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_770]) ).
cnf(c_772,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_771]) ).
cnf(c_773,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_772]) ).
cnf(c_774,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_773]) ).
cnf(c_775,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_774]) ).
cnf(c_776,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_775]) ).
cnf(c_777,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_776]) ).
cnf(c_326,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_777]) ).
cnf(c_778,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_326,c_281]) ).
cnf(c_779,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_778]) ).
cnf(c_359,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_779]) ).
cnf(c_780,plain,
( start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_201,c_190]) ).
cnf(c_781,plain,
( start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_780]) ).
cnf(c_782,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_781]) ).
cnf(c_396,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_782]) ).
cnf(c_783,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_359,c_228]) ).
cnf(c_406,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_783]) ).
cnf(c_784,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_326,c_406]) ).
cnf(c_785,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_784]) ).
cnf(c_786,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_785]) ).
cnf(c_412,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_786]) ).
cnf(c_787,plain,
( greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ greater_or_equal(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_412,c_99]) ).
cnf(c_415,plain,
( greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_106,c_787]) ).
cnf(c_788,plain,
( greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_412,c_188]) ).
cnf(c_417,plain,
( greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_788]) ).
cnf(c_420,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) != zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_415,c_161]) ).
cnf(c_421,plain,
( subpopulations(first_movers,efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2)))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_415,c_156]) ).
cnf(c_789,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater(B,critical_point(sK0(A)))
| ~ subpopulations(first_movers,efficient_producers,sK0(A),B) ),
inference(xxres,[status(thm)],[c_75]) ).
cnf(c_790,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2))))
| ~ greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_789,c_421]) ).
cnf(c_791,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_790,c_94]) ).
cnf(c_792,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_791,c_48]) ).
cnf(c_429,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_49,c_792]) ).
cnf(c_793,negated_conjecture,
( selection_favors(B,A,C)
| ~ greater(growth_rate(B,C),growth_rate(A,C))
| ~ subpopulations(A,B,sK0(sK2),C)
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_53,c_48]) ).
cnf(c_794,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_793,c_421]) ).
cnf(c_795,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_794,c_429]) ).
cnf(c_796,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_795]) ).
cnf(c_797,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_796]) ).
cnf(c_434,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_797]) ).
cnf(c_798,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_417,c_131]) ).
cnf(c_436,plain,
( greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_798]) ).
cnf(c_799,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_436,c_396]) ).
cnf(c_800,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_799]) ).
cnf(c_437,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_800]) ).
cnf(c_801,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_436,c_311]) ).
cnf(c_802,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_801]) ).
cnf(c_438,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_802]) ).
cnf(c_803,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_438,c_53]) ).
cnf(c_804,negated_conjecture,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2)
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_803]) ).
cnf(c_805,negated_conjecture,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_804]) ).
cnf(c_447,negated_conjecture,
( ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_805]) ).
cnf(c_806,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater(B,critical_point(sK0(A)))
| ~ subpopulations(first_movers,efficient_producers,sK0(A),B) ),
inference(xxres,[status(thm)],[c_75]) ).
cnf(c_807,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| ~ greater(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_806,c_438]) ).
cnf(c_808,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_807,c_127]) ).
cnf(c_809,negated_conjecture,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_808,c_48]) ).
cnf(c_810,negated_conjecture,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(copy,[status(thm)],[c_809]) ).
cnf(c_449,negated_conjecture,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_49,c_810]) ).
cnf(c_811,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_449,c_447]) ).
cnf(c_812,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_811]) ).
cnf(c_813,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_812]) ).
cnf(c_450,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_813]) ).
cnf(c_814,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_450,c_437]) ).
cnf(c_815,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_814]) ).
cnf(c_451,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_815]) ).
cnf(c_816,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_451,c_434]) ).
cnf(c_817,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_816]) ).
cnf(c_481,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_817]) ).
cnf(c_818,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_481,c_420]) ).
cnf(c_523,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_818]) ).
cnf(c_819,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_451,c_523]) ).
cnf(c_820,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| start_time(sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_819]) ).
cnf(c_529,plain,
start_time(sK0(sK2)) = critical_point(sK0(sK2)),
inference(resolve,[status(thm)],[c_91,c_820]) ).
cnf(c_821,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
inference(paramod,[status(thm)],[c_529,c_95]) ).
cnf(c_822,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_48,c_821]) ).
cnf(c_533,negated_conjecture,
( in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_822]) ).
cnf(c_534,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| in_environment(sK0(sK2),end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_533,c_131]) ).
cnf(c_823,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_534,c_77]) ).
cnf(c_824,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_823]) ).
cnf(c_535,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_824]) ).
cnf(c_825,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulation(efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_534,c_65]) ).
cnf(c_826,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulation(efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_825]) ).
cnf(c_536,negated_conjecture,
( subpopulation(efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_826]) ).
cnf(c_827,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_534,c_63]) ).
cnf(c_828,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_827]) ).
cnf(c_537,negated_conjecture,
( subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_828]) ).
cnf(c_829,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater_or_equal(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_534,c_61]) ).
cnf(c_830,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| greater_or_equal(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_829]) ).
cnf(c_538,negated_conjecture,
( greater_or_equal(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_830]) ).
cnf(c_831,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_534,c_59]) ).
cnf(c_832,negated_conjecture,
( selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_831]) ).
cnf(c_539,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_832]) ).
cnf(c_833,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_77,c_534]) ).
cnf(c_834,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_833,c_205]) ).
cnf(c_835,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_834,c_48]) ).
cnf(c_836,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(copy,[status(thm)],[c_835]) ).
cnf(c_540,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_49,c_836]) ).
cnf(c_837,plain,
( selection_favors(efficient_producers,A,end_time(sK0(sK2)))
| cardinality_at_time(A,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_536,c_51]) ).
cnf(c_838,negated_conjecture,
( selection_favors(efficient_producers,A,end_time(sK0(sK2)))
| cardinality_at_time(A,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_837]) ).
cnf(c_543,negated_conjecture,
( selection_favors(efficient_producers,A,end_time(sK0(sK2)))
| cardinality_at_time(A,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_838]) ).
cnf(c_839,plain,
( zero = cardinality_at_time(first_movers,end_time(sK0(sK2)))
| greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_538,c_45]) ).
cnf(c_547,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_839]) ).
cnf(c_840,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_59,c_534]) ).
cnf(c_841,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
inference(resolve,[status(thm)],[c_840,c_547]) ).
cnf(c_842,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_841,c_540]) ).
cnf(c_843,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_842,c_48]) ).
cnf(c_844,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(copy,[status(thm)],[c_843]) ).
cnf(c_845,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(copy,[status(thm)],[c_844]) ).
cnf(c_553,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_845]) ).
cnf(c_846,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_539,c_547]) ).
cnf(c_554,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_846]) ).
cnf(c_847,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_553,c_53]) ).
cnf(c_848,negated_conjecture,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2)
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_847]) ).
cnf(c_849,negated_conjecture,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_848]) ).
cnf(c_557,negated_conjecture,
( ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_849]) ).
cnf(c_850,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater(B,critical_point(sK0(A)))
| ~ subpopulations(first_movers,efficient_producers,sK0(A),B) ),
inference(xxres,[status(thm)],[c_75]) ).
cnf(c_851,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| ~ greater(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_850,c_553]) ).
cnf(c_852,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_851,c_127]) ).
cnf(c_853,negated_conjecture,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_852,c_48]) ).
cnf(c_854,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(copy,[status(thm)],[c_853]) ).
cnf(c_558,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_49,c_854]) ).
cnf(c_855,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_558,c_557]) ).
cnf(c_856,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_855]) ).
cnf(c_857,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_856]) ).
cnf(c_561,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_857]) ).
cnf(c_858,negated_conjecture,
( selection_favors(A,C,B)
| cardinality_at_time(C,B) != zero
| ~ greater(cardinality_at_time(A,B),zero)
| ~ subpopulation(C,sK0(sK2),B)
| ~ subpopulation(A,sK0(sK2),B)
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_51,c_48]) ).
cnf(c_859,negated_conjecture,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,A,end_time(sK0(sK2)))
| cardinality_at_time(A,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(A,sK0(sK2),end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_858,c_536]) ).
cnf(c_860,negated_conjecture,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_859,c_537]) ).
cnf(c_861,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_860,c_540]) ).
cnf(c_862,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_861,c_561]) ).
cnf(c_863,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_862]) ).
cnf(c_864,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_863]) ).
cnf(c_865,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_864]) ).
cnf(c_866,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_865]) ).
cnf(c_867,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_866]) ).
cnf(c_563,negated_conjecture,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_867]) ).
cnf(c_868,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_563,c_281]) ).
cnf(c_869,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_868]) ).
cnf(c_593,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_869]) ).
cnf(c_870,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_543,c_537]) ).
cnf(c_871,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_870]) ).
cnf(c_595,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_871]) ).
cnf(c_872,plain,
( appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_593,c_228]) ).
cnf(c_624,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_872]) ).
cnf(c_873,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_563,c_624]) ).
cnf(c_874,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)) ),
inference(copy,[status(thm)],[c_873]) ).
cnf(c_630,plain,
appear(efficient_producers,sK0(sK2)) = critical_point(sK0(sK2)),
inference(resolve,[status(thm)],[c_91,c_874]) ).
cnf(c_631,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(paramod,[status(thm)],[c_630,c_535]) ).
cnf(c_875,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero)
| ~ greater_or_equal(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2))) ),
inference(paramod,[status(thm)],[c_630,c_99]) ).
cnf(c_632,negated_conjecture,
greater(cardinality_at_time(efficient_producers,sK1(sK2,sK0(sK2))),zero),
inference(resolve,[status(thm)],[c_106,c_875]) ).
cnf(c_633,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) != zero ),
inference(resolve,[status(thm)],[c_632,c_161]) ).
cnf(c_634,plain,
( subpopulations(first_movers,efficient_producers,sK0(sK2),sK1(sK2,sK0(sK2)))
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero ),
inference(resolve,[status(thm)],[c_632,c_156]) ).
cnf(c_876,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater(B,critical_point(sK0(A)))
| ~ subpopulations(first_movers,efficient_producers,sK0(A),B) ),
inference(xxres,[status(thm)],[c_75]) ).
cnf(c_877,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2))))
| ~ greater(sK1(sK2,sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_876,c_634]) ).
cnf(c_878,plain,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_877,c_94]) ).
cnf(c_879,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_878,c_48]) ).
cnf(c_643,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_49,c_879]) ).
cnf(c_880,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_631,c_131]) ).
cnf(c_644,plain,
( greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_880]) ).
cnf(c_881,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_644,c_595]) ).
cnf(c_645,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_881]) ).
cnf(c_882,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_644,c_554]) ).
cnf(c_646,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| subpopulations(first_movers,efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_882]) ).
cnf(c_883,negated_conjecture,
( selection_favors(B,A,C)
| ~ greater(growth_rate(B,C),growth_rate(A,C))
| ~ subpopulations(A,B,sK0(sK2),C)
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_53,c_48]) ).
cnf(c_884,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,sK1(sK2,sK0(sK2))),growth_rate(first_movers,sK1(sK2,sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_883,c_634]) ).
cnf(c_885,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(resolve,[status(thm)],[c_884,c_643]) ).
cnf(c_886,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(copy,[status(thm)],[c_885]) ).
cnf(c_655,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2))) ),
inference(resolve,[status(thm)],[c_49,c_886]) ).
cnf(c_887,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_646,c_53]) ).
cnf(c_888,negated_conjecture,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| selection_favors(efficient_producers,first_movers,sK2)
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_48,c_887]) ).
cnf(c_889,negated_conjecture,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_49,c_888]) ).
cnf(c_658,negated_conjecture,
( ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_91,c_889]) ).
cnf(c_890,plain,
( selection_favors(efficient_producers,first_movers,A)
| ~ observational_period(A)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater(B,critical_point(sK0(A)))
| ~ subpopulations(first_movers,efficient_producers,sK0(A),B) ),
inference(xxres,[status(thm)],[c_75]) ).
cnf(c_891,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| ~ greater(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
inference(resolve,[status(thm)],[c_890,c_646]) ).
cnf(c_892,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| ~ observational_period(sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_891,c_127]) ).
cnf(c_893,negated_conjecture,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_892,c_48]) ).
cnf(c_894,negated_conjecture,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2)
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(copy,[status(thm)],[c_893]) ).
cnf(c_659,negated_conjecture,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(resolve,[status(thm)],[c_49,c_894]) ).
cnf(c_895,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_659,c_658]) ).
cnf(c_896,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_895]) ).
cnf(c_660,plain,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(copy,[status(thm)],[c_896]) ).
cnf(c_897,plain,
( sK1(sK2,sK0(sK2)) = end_time(sK0(sK2))
| sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)) ),
inference(resolve,[status(thm)],[c_660,c_645]) ).
cnf(c_661,plain,
sK1(sK2,sK0(sK2)) = end_time(sK0(sK2)),
inference(copy,[status(thm)],[c_897]) ).
cnf(c_898,negated_conjecture,
( cardinality_at_time(first_movers,sK1(sK2,sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))) ),
inference(paramod,[status(thm)],[c_661,c_655]) ).
cnf(c_899,negated_conjecture,
( cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))) ),
inference(paramod,[status(thm)],[c_661,c_898]) ).
cnf(c_663,negated_conjecture,
cardinality_at_time(first_movers,end_time(sK0(sK2))) = zero,
inference(resolve,[status(thm)],[c_91,c_899]) ).
cnf(c_900,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero ),
inference(paramod,[status(thm)],[c_661,c_633]) ).
cnf(c_901,plain,
( selection_favors(efficient_producers,first_movers,sK1(sK2,sK0(sK2)))
| zero != zero ),
inference(paramod,[status(thm)],[c_663,c_900]) ).
cnf(c_902,plain,
( selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| zero != zero ),
inference(paramod,[status(thm)],[c_661,c_901]) ).
cnf(c_903,plain,
selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))),
inference(copy,[status(thm)],[c_902]) ).
cnf(c_670,plain,
$false,
inference(resolve,[status(thm)],[c_91,c_903]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n009.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sat Sep 26 00:08:19 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.39 % Process 2892520 was started by sandbox on n009,
% 0.10/5.39 % Sat Sep 26 00:08:19 2026
% 0.10/5.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/5.39
% 0.10/5.39 % From the command line: assign(max_seconds, 300).
% 0.15/5.58
% 0.15/5.58 % SZS status Theorem for theBenchmark
% 0.15/5.58
% 0.15/5.58 % Proof 1 at 0.14 (+ 0.03) seconds.
% 0.15/5.58 % Length of proof is 182.
% 0.15/5.58 % Level of proof is 47.
% 0.15/5.58 % Maximum clause weight is 62.000.
% 0.15/5.58 % Given clauses 424.
% 0.15/5.58
% 0.15/5.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------