%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : MGT030+1 : TPTP v3.4.2. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1003MB
% OS : Linux 2.6.17-1.2142_FC4
% CPULimit : 600s
% DateTime : Wed May 6 14:01:41 EDT 2009
% Result : Theorem 0.4s
% Output : Refutation 0.4s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 3
% Syntax : Number of formulae : 49 ( 14 unt; 0 def)
% Number of atoms : 304 ( 0 equ)
% Maximal formula atoms : 135 ( 6 avg)
% Number of connectives : 381 ( 126 ~; 202 |; 53 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 46 ( 1 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(prove_l12,plain,
! [B] :
( ( environment(e)
| environment(e)
| environment(e) )
& ( stable(e)
| environment(e)
| environment(e) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| environment(e)
| environment(e) )
& ( greater(t(B),B)
| environment(e)
| environment(e) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| environment(e)
| environment(e) )
& ( environment(e)
| stable(e)
| environment(e) )
& ( stable(e)
| stable(e)
| environment(e) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| stable(e)
| environment(e) )
& ( greater(t(B),B)
| stable(e)
| environment(e) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| stable(e)
| environment(e) )
& ( environment(e)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| environment(e) )
& ( stable(e)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| environment(e) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| environment(e) )
& ( greater(t(B),B)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| environment(e) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| environment(e) )
& ( environment(e)
| environment(e)
| stable(e) )
& ( stable(e)
| environment(e)
| stable(e) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| environment(e)
| stable(e) )
& ( greater(t(B),B)
| environment(e)
| stable(e) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| environment(e)
| stable(e) )
& ( environment(e)
| stable(e)
| stable(e) )
& ( stable(e)
| stable(e)
| stable(e) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| stable(e)
| stable(e) )
& ( greater(t(B),B)
| stable(e)
| stable(e) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| stable(e)
| stable(e) )
& ( environment(e)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| stable(e) )
& ( stable(e)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| stable(e) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| stable(e) )
& ( greater(t(B),B)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| stable(e) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| stable(e) )
& ( environment(e)
| environment(e)
| ~ in_environment(e,B) )
& ( stable(e)
| environment(e)
| ~ in_environment(e,B) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| environment(e)
| ~ in_environment(e,B) )
& ( greater(t(B),B)
| environment(e)
| ~ in_environment(e,B) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| environment(e)
| ~ in_environment(e,B) )
& ( environment(e)
| stable(e)
| ~ in_environment(e,B) )
& ( stable(e)
| stable(e)
| ~ in_environment(e,B) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| stable(e)
| ~ in_environment(e,B) )
& ( greater(t(B),B)
| stable(e)
| ~ in_environment(e,B) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| stable(e)
| ~ in_environment(e,B) )
& ( environment(e)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ in_environment(e,B) )
& ( stable(e)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ in_environment(e,B) )
& ( subpopulations(first_movers,efficient_producers,e,t(B))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ in_environment(e,B) )
& ( greater(t(B),B)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ in_environment(e,B) )
& ( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ in_environment(e,B) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT030+1.tptp',unknown),
[] ).
cnf(162541728,plain,
( environment(e)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)) ),
inference(rewrite,[status(thm)],[prove_l12]),
[] ).
cnf(162513656,plain,
( stable(e)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)) ),
inference(rewrite,[status(thm)],[prove_l12]),
[] ).
cnf(162546072,plain,
environment(e),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[prove_l12,162541728]),
[] ).
fof(mp_earliest_time_growth_rate_exceeds,plain,
! [A,B,E] :
( ( ~ greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))
| ~ in_environment(A,B)
| ~ environment(A)
| ~ greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))) )
& ( subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))
| ~ in_environment(A,B)
| ~ environment(A)
| ~ greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))) )
& ( greater_or_equal(t_nn_2(A,B),B)
| ~ in_environment(A,B)
| ~ environment(A)
| ~ greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))) )
& ( ~ greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))
| ~ in_environment(A,B)
| ~ environment(A)
| ~ subpopulations(first_movers,efficient_producers,A,E)
| ~ greater(E,to(A,B))
| greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)) )
& ( subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))
| ~ in_environment(A,B)
| ~ environment(A)
| ~ subpopulations(first_movers,efficient_producers,A,E)
| ~ greater(E,to(A,B))
| greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)) )
& ( greater_or_equal(t_nn_2(A,B),B)
| ~ in_environment(A,B)
| ~ environment(A)
| ~ subpopulations(first_movers,efficient_producers,A,E)
| ~ greater(E,to(A,B))
| greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)) )
& ( ~ greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))
| ~ in_environment(A,B)
| ~ environment(A)
| in_environment(A,to(A,B)) )
& ( subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))
| ~ in_environment(A,B)
| ~ environment(A)
| in_environment(A,to(A,B)) )
& ( greater_or_equal(t_nn_2(A,B),B)
| ~ in_environment(A,B)
| ~ environment(A)
| in_environment(A,to(A,B)) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT030+1.tptp',unknown),
[] ).
cnf(161787424,plain,
( greater_or_equal(t_nn_2(A,B),B)
| ~ in_environment(A,B)
| ~ environment(A)
| in_environment(A,to(A,B)) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
fof(l1,plain,
! [A,C] :
( ( ~ subpopulations(first_movers,efficient_producers,A,C)
| ~ greater_or_equal(C,to(A))
| greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C))
| ~ environment(A)
| ~ stable(A) )
& ( in_environment(A,to(A))
| ~ environment(A)
| ~ stable(A) ) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT030+1.tptp',unknown),
[] ).
cnf(161913480,plain,
( in_environment(A,to(A))
| ~ environment(A)
| ~ stable(A) ),
inference(rewrite,[status(thm)],[l1]),
[] ).
cnf(162517904,plain,
stable(e),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[prove_l12,162513656]),
[] ).
cnf(228591736,plain,
in_environment(e,to(e)),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162546072,161913480,162517904]),
[] ).
cnf(228812032,plain,
( greater_or_equal(t_nn_2(e,to(e)),to(e))
| in_environment(e,to(e,to(e))) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162546072,161787424,228591736]),
[] ).
cnf(161797848,plain,
( subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))
| ~ in_environment(A,B)
| ~ environment(A)
| in_environment(A,to(A,B)) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
cnf(228860568,plain,
( subpopulations(first_movers,efficient_producers,e,t_nn_2(e,to(e)))
| in_environment(e,to(e,to(e))) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162546072,161797848,228591736]),
[] ).
cnf(161812096,plain,
( ~ greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))
| ~ in_environment(A,B)
| ~ environment(A)
| in_environment(A,to(A,B)) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
cnf(228897488,plain,
( ~ greater(growth_rate(efficient_producers,t_nn_2(e,to(e))),growth_rate(first_movers,t_nn_2(e,to(e))))
| in_environment(e,to(e,to(e))) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162546072,161812096,228591736]),
[] ).
cnf(161941824,plain,
( ~ subpopulations(first_movers,efficient_producers,A,C)
| ~ greater_or_equal(C,to(A))
| greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C))
| ~ environment(A)
| ~ stable(A) ),
inference(rewrite,[status(thm)],[l1]),
[] ).
cnf(228617464,plain,
( ~ subpopulations(first_movers,efficient_producers,e,B)
| ~ greater_or_equal(B,to(e))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162541728,161941824,162517904]),
[] ).
cnf(231071928,plain,
in_environment(e,to(e,to(e))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[228812032,228860568,228897488,228617464]),
[] ).
cnf(162396776,plain,
( greater(t(B),B)
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ in_environment(e,B) ),
inference(rewrite,[status(thm)],[prove_l12]),
[] ).
cnf(161896168,plain,
( subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))
| ~ in_environment(A,B)
| ~ environment(A)
| ~ greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
cnf(228727392,plain,
( subpopulations(first_movers,efficient_producers,e,t_nn_2(e,A))
| ~ in_environment(e,A)
| ~ greater(growth_rate(efficient_producers,to(e,A)),growth_rate(first_movers,to(e,A))) ),
inference(resolution,[status(thm)],[161896168,162546072]),
[] ).
cnf(161890896,plain,
( greater_or_equal(t_nn_2(A,B),B)
| ~ in_environment(A,B)
| ~ environment(A)
| ~ greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
cnf(228719576,plain,
( greater_or_equal(t_nn_2(e,A),A)
| ~ in_environment(e,A)
| ~ greater(growth_rate(efficient_producers,to(e,A)),growth_rate(first_movers,to(e,A))) ),
inference(resolution,[status(thm)],[161890896,162546072]),
[] ).
cnf(231510912,plain,
( ~ greater(growth_rate(efficient_producers,to(e,to(e))),growth_rate(first_movers,to(e,to(e))))
| greater(growth_rate(efficient_producers,t_nn_2(e,to(e))),growth_rate(first_movers,t_nn_2(e,to(e)))) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[228727392,228591736,228719576,228617464]),
[] ).
cnf(162464400,plain,
( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| environment(e)
| ~ in_environment(e,B) ),
inference(rewrite,[status(thm)],[prove_l12]),
[] ).
cnf(231044968,plain,
environment(e),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162541728,228897488,162464400]),
[] ).
cnf(161901344,plain,
( ~ greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))
| ~ in_environment(A,B)
| ~ environment(A)
| ~ greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
cnf(228757640,plain,
( ~ greater(growth_rate(efficient_producers,t_nn_2(e,A)),growth_rate(first_movers,t_nn_2(e,A)))
| ~ in_environment(e,A)
| ~ greater(growth_rate(efficient_producers,to(e,A)),growth_rate(first_movers,to(e,A))) ),
inference(resolution,[status(thm)],[161901344,162546072]),
[] ).
cnf(234964216,plain,
~ greater(growth_rate(efficient_producers,to(e,to(e))),growth_rate(first_movers,to(e,to(e)))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[231510912,231044968,162517904,228757640,161913480]),
[] ).
cnf(235071000,plain,
greater(t(to(e,to(e))),to(e,to(e))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[231071928,162396776,234964216]),
[] ).
cnf(162490336,plain,
( environment(e)
| ~ in_environment(e,B) ),
inference(rewrite,[status(thm)],[prove_l12]),
[] ).
cnf(162378232,plain,
( ~ greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ in_environment(e,B) ),
inference(rewrite,[status(thm)],[prove_l12]),
[] ).
cnf(235089880,plain,
~ greater(growth_rate(efficient_producers,t(to(e,to(e)))),growth_rate(first_movers,t(to(e,to(e))))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[231071928,162378232,234964216]),
[] ).
cnf(161873232,plain,
( subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))
| ~ in_environment(A,B)
| ~ environment(A)
| ~ subpopulations(first_movers,efficient_producers,A,E)
| ~ greater(E,to(A,B))
| greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
cnf(162408344,plain,
( subpopulations(first_movers,efficient_producers,e,t(B))
| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ in_environment(e,B) ),
inference(rewrite,[status(thm)],[prove_l12]),
[] ).
cnf(235083000,plain,
subpopulations(first_movers,efficient_producers,e,t(to(e,to(e)))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[231071928,162408344,234964216]),
[] ).
cnf(235340224,plain,
( subpopulations(first_movers,efficient_producers,e,t_nn_2(e,A))
| ~ in_environment(e,A)
| ~ greater(t(to(e,to(e))),to(e,A)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162490336,235089880,161873232,235083000]),
[] ).
cnf(235344408,plain,
subpopulations(first_movers,efficient_producers,e,t_nn_2(e,to(e))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[235071000,235340224,228591736]),
[] ).
cnf(228647792,plain,
( greater_or_equal(t_nn_2(e,A),A)
| ~ in_environment(e,A)
| in_environment(e,to(e,A)) ),
inference(resolution,[status(thm)],[161787424,162546072]),
[] ).
cnf(231488936,plain,
( greater_or_equal(t_nn_2(e,A),A)
| ~ in_environment(e,A)
| greater(t(to(e,A)),to(e,A)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[228647792,228719576,162396776]),
[] ).
cnf(231619432,plain,
( greater_or_equal(t_nn_2(e,to(e)),to(e))
| greater(t(to(e,to(e))),to(e,to(e))) ),
inference(resolution,[status(thm)],[231488936,228591736]),
[] ).
cnf(161860168,plain,
( greater_or_equal(t_nn_2(A,B),B)
| ~ in_environment(A,B)
| ~ environment(A)
| ~ subpopulations(first_movers,efficient_producers,A,E)
| ~ greater(E,to(A,B))
| greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
cnf(235310648,plain,
( greater_or_equal(t_nn_2(e,A),A)
| ~ in_environment(e,A)
| ~ greater(t(to(e,to(e))),to(e,A)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162490336,235089880,161860168,235083000]),
[] ).
cnf(235315152,plain,
greater_or_equal(t_nn_2(e,to(e)),to(e)),
inference(forward_subsumption_resolution__resolution,[status(thm)],[231619432,235310648,228591736]),
[] ).
cnf(235396904,plain,
greater(growth_rate(efficient_producers,t_nn_2(e,to(e))),growth_rate(first_movers,t_nn_2(e,to(e)))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162541728,162513656,235344408,161941824,235315152]),
[] ).
cnf(161881816,plain,
( ~ greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))
| ~ in_environment(A,B)
| ~ environment(A)
| ~ subpopulations(first_movers,efficient_producers,A,E)
| ~ greater(E,to(A,B))
| greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)) ),
inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),
[] ).
cnf(235359480,plain,
( ~ greater(growth_rate(efficient_producers,t_nn_2(e,A)),growth_rate(first_movers,t_nn_2(e,A)))
| ~ in_environment(e,A)
| ~ greater(t(to(e,to(e))),to(e,A)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[162490336,235089880,161881816,235083000]),
[] ).
cnf(235365976,plain,
~ greater(growth_rate(efficient_producers,t_nn_2(e,to(e))),growth_rate(first_movers,t_nn_2(e,to(e)))),
inference(forward_subsumption_resolution__resolution,[status(thm)],[235071000,235359480,228591736]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[235396904,235365976]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 1 seconds
% START OF PROOF SEQUENCE
% fof(prove_l12,plain,(((environment(e)|environment(e)|environment(e))&(stable(e)|environment(e)|environment(e))&(subpopulations(first_movers,efficient_producers,e,t(B))|environment(e)|environment(e))&(greater(t(B),B)|environment(e)|environment(e))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|environment(e)|environment(e))&(environment(e)|stable(e)|environment(e))&(stable(e)|stable(e)|environment(e))&(subpopulations(first_movers,efficient_producers,e,t(B))|stable(e)|environment(e))&(greater(t(B),B)|stable(e)|environment(e))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|stable(e)|environment(e))&(environment(e)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|environment(e))&(stable(e)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|environment(e))&(subpopulations(first_movers,efficient_producers,e,t(B))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|environment(e))&(greater(t(B),B)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|environment(e))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|environment(e))&(environment(e)|environment(e)|stable(e))&(stable(e)|environment(e)|stable(e))&(subpopulations(first_movers,efficient_producers,e,t(B))|environment(e)|stable(e))&(greater(t(B),B)|environment(e)|stable(e))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|environment(e)|stable(e))&(environment(e)|stable(e)|stable(e))&(stable(e)|stable(e)|stable(e))&(subpopulations(first_movers,efficient_producers,e,t(B))|stable(e)|stable(e))&(greater(t(B),B)|stable(e)|stable(e))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|stable(e)|stable(e))&(environment(e)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|stable(e))&(stable(e)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|stable(e))&(subpopulations(first_movers,efficient_producers,e,t(B))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|stable(e))&(greater(t(B),B)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|stable(e))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|stable(e))&(environment(e)|environment(e)|~in_environment(e,B))&(stable(e)|environment(e)|~in_environment(e,B))&(subpopulations(first_movers,efficient_producers,e,t(B))|environment(e)|~in_environment(e,B))&(greater(t(B),B)|environment(e)|~in_environment(e,B))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|environment(e)|~in_environment(e,B))&(environment(e)|stable(e)|~in_environment(e,B))&(stable(e)|stable(e)|~in_environment(e,B))&(subpopulations(first_movers,efficient_producers,e,t(B))|stable(e)|~in_environment(e,B))&(greater(t(B),B)|stable(e)|~in_environment(e,B))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|stable(e)|~in_environment(e,B))&(environment(e)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|~in_environment(e,B))&(stable(e)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|~in_environment(e,B))&(subpopulations(first_movers,efficient_producers,e,t(B))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|~in_environment(e,B))&(greater(t(B),B)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|~in_environment(e,B))&(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|~in_environment(e,B)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT030+1.tptp',unknown),[]).
%
% cnf(162541728,plain,(environment(e)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))),inference(rewrite,[status(thm)],[prove_l12]),[]).
%
% cnf(162513656,plain,(stable(e)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))),inference(rewrite,[status(thm)],[prove_l12]),[]).
%
% cnf(162546072,plain,(environment(e)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[prove_l12,162541728]),[]).
%
% fof(mp_earliest_time_growth_rate_exceeds,plain,(((~greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))|~in_environment(A,B)|~environment(A)|~greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))))&(subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))|~in_environment(A,B)|~environment(A)|~greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))))&(greater_or_equal(t_nn_2(A,B),B)|~in_environment(A,B)|~environment(A)|~greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B))))&(~greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))|~in_environment(A,B)|~environment(A)|~subpopulations(first_movers,efficient_producers,A,E)|~greater(E,to(A,B))|greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)))&(subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))|~in_environment(A,B)|~environment(A)|~subpopulations(first_movers,efficient_producers,A,E)|~greater(E,to(A,B))|greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)))&(greater_or_equal(t_nn_2(A,B),B)|~in_environment(A,B)|~environment(A)|~subpopulations(first_movers,efficient_producers,A,E)|~greater(E,to(A,B))|greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E)))&(~greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))|~in_environment(A,B)|~environment(A)|in_environment(A,to(A,B)))&(subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))|~in_environment(A,B)|~environment(A)|in_environment(A,to(A,B)))&(greater_or_equal(t_nn_2(A,B),B)|~in_environment(A,B)|~environment(A)|in_environment(A,to(A,B))))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT030+1.tptp',unknown),[]).
%
% cnf(161787424,plain,(greater_or_equal(t_nn_2(A,B),B)|~in_environment(A,B)|~environment(A)|in_environment(A,to(A,B))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% fof(l1,plain,(((~subpopulations(first_movers,efficient_producers,A,C)|~greater_or_equal(C,to(A))|greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C))|~environment(A)|~stable(A))&(in_environment(A,to(A))|~environment(A)|~stable(A)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT030+1.tptp',unknown),[]).
%
% cnf(161913480,plain,(in_environment(A,to(A))|~environment(A)|~stable(A)),inference(rewrite,[status(thm)],[l1]),[]).
%
% cnf(162517904,plain,(stable(e)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[prove_l12,162513656]),[]).
%
% cnf(228591736,plain,(in_environment(e,to(e))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162546072,161913480,162517904]),[]).
%
% cnf(228812032,plain,(greater_or_equal(t_nn_2(e,to(e)),to(e))|in_environment(e,to(e,to(e)))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162546072,161787424,228591736]),[]).
%
% cnf(161797848,plain,(subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))|~in_environment(A,B)|~environment(A)|in_environment(A,to(A,B))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% cnf(228860568,plain,(subpopulations(first_movers,efficient_producers,e,t_nn_2(e,to(e)))|in_environment(e,to(e,to(e)))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162546072,161797848,228591736]),[]).
%
% cnf(161812096,plain,(~greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))|~in_environment(A,B)|~environment(A)|in_environment(A,to(A,B))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% cnf(228897488,plain,(~greater(growth_rate(efficient_producers,t_nn_2(e,to(e))),growth_rate(first_movers,t_nn_2(e,to(e))))|in_environment(e,to(e,to(e)))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162546072,161812096,228591736]),[]).
%
% cnf(161941824,plain,(~subpopulations(first_movers,efficient_producers,A,C)|~greater_or_equal(C,to(A))|greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C))|~environment(A)|~stable(A)),inference(rewrite,[status(thm)],[l1]),[]).
%
% cnf(228617464,plain,(~subpopulations(first_movers,efficient_producers,e,B)|~greater_or_equal(B,to(e))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162541728,161941824,162517904]),[]).
%
% cnf(231071928,plain,(in_environment(e,to(e,to(e)))),inference(forward_subsumption_resolution__resolution,[status(thm)],[228812032,228860568,228897488,228617464]),[]).
%
% cnf(162396776,plain,(greater(t(B),B)|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|~in_environment(e,B)),inference(rewrite,[status(thm)],[prove_l12]),[]).
%
% cnf(161896168,plain,(subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))|~in_environment(A,B)|~environment(A)|~greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B)))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% cnf(228727392,plain,(subpopulations(first_movers,efficient_producers,e,t_nn_2(e,A))|~in_environment(e,A)|~greater(growth_rate(efficient_producers,to(e,A)),growth_rate(first_movers,to(e,A)))),inference(resolution,[status(thm)],[161896168,162546072]),[]).
%
% cnf(161890896,plain,(greater_or_equal(t_nn_2(A,B),B)|~in_environment(A,B)|~environment(A)|~greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B)))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% cnf(228719576,plain,(greater_or_equal(t_nn_2(e,A),A)|~in_environment(e,A)|~greater(growth_rate(efficient_producers,to(e,A)),growth_rate(first_movers,to(e,A)))),inference(resolution,[status(thm)],[161890896,162546072]),[]).
%
% cnf(231510912,plain,(~greater(growth_rate(efficient_producers,to(e,to(e))),growth_rate(first_movers,to(e,to(e))))|greater(growth_rate(efficient_producers,t_nn_2(e,to(e))),growth_rate(first_movers,t_nn_2(e,to(e))))),inference(forward_subsumption_resolution__resolution,[status(thm)],[228727392,228591736,228719576,228617464]),[]).
%
% cnf(162464400,plain,(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|environment(e)|~in_environment(e,B)),inference(rewrite,[status(thm)],[prove_l12]),[]).
%
% cnf(231044968,plain,(environment(e)),inference(forward_subsumption_resolution__resolution,[status(thm)],[162541728,228897488,162464400]),[]).
%
% cnf(161901344,plain,(~greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))|~in_environment(A,B)|~environment(A)|~greater(growth_rate(efficient_producers,to(A,B)),growth_rate(first_movers,to(A,B)))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% cnf(228757640,plain,(~greater(growth_rate(efficient_producers,t_nn_2(e,A)),growth_rate(first_movers,t_nn_2(e,A)))|~in_environment(e,A)|~greater(growth_rate(efficient_producers,to(e,A)),growth_rate(first_movers,to(e,A)))),inference(resolution,[status(thm)],[161901344,162546072]),[]).
%
% cnf(234964216,plain,(~greater(growth_rate(efficient_producers,to(e,to(e))),growth_rate(first_movers,to(e,to(e))))),inference(forward_subsumption_resolution__resolution,[status(thm)],[231510912,231044968,162517904,228757640,161913480]),[]).
%
% cnf(235071000,plain,(greater(t(to(e,to(e))),to(e,to(e)))),inference(forward_subsumption_resolution__resolution,[status(thm)],[231071928,162396776,234964216]),[]).
%
% cnf(162490336,plain,(environment(e)|~in_environment(e,B)),inference(rewrite,[status(thm)],[prove_l12]),[]).
%
% cnf(162378232,plain,(~greater(growth_rate(efficient_producers,t(B)),growth_rate(first_movers,t(B)))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|~in_environment(e,B)),inference(rewrite,[status(thm)],[prove_l12]),[]).
%
% cnf(235089880,plain,(~greater(growth_rate(efficient_producers,t(to(e,to(e)))),growth_rate(first_movers,t(to(e,to(e)))))),inference(forward_subsumption_resolution__resolution,[status(thm)],[231071928,162378232,234964216]),[]).
%
% cnf(161873232,plain,(subpopulations(first_movers,efficient_producers,A,t_nn_2(A,B))|~in_environment(A,B)|~environment(A)|~subpopulations(first_movers,efficient_producers,A,E)|~greater(E,to(A,B))|greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% cnf(162408344,plain,(subpopulations(first_movers,efficient_producers,e,t(B))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))|~in_environment(e,B)),inference(rewrite,[status(thm)],[prove_l12]),[]).
%
% cnf(235083000,plain,(subpopulations(first_movers,efficient_producers,e,t(to(e,to(e))))),inference(forward_subsumption_resolution__resolution,[status(thm)],[231071928,162408344,234964216]),[]).
%
% cnf(235340224,plain,(subpopulations(first_movers,efficient_producers,e,t_nn_2(e,A))|~in_environment(e,A)|~greater(t(to(e,to(e))),to(e,A))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162490336,235089880,161873232,235083000]),[]).
%
% cnf(235344408,plain,(subpopulations(first_movers,efficient_producers,e,t_nn_2(e,to(e)))),inference(forward_subsumption_resolution__resolution,[status(thm)],[235071000,235340224,228591736]),[]).
%
% cnf(228647792,plain,(greater_or_equal(t_nn_2(e,A),A)|~in_environment(e,A)|in_environment(e,to(e,A))),inference(resolution,[status(thm)],[161787424,162546072]),[]).
%
% cnf(231488936,plain,(greater_or_equal(t_nn_2(e,A),A)|~in_environment(e,A)|greater(t(to(e,A)),to(e,A))),inference(forward_subsumption_resolution__resolution,[status(thm)],[228647792,228719576,162396776]),[]).
%
% cnf(231619432,plain,(greater_or_equal(t_nn_2(e,to(e)),to(e))|greater(t(to(e,to(e))),to(e,to(e)))),inference(resolution,[status(thm)],[231488936,228591736]),[]).
%
% cnf(161860168,plain,(greater_or_equal(t_nn_2(A,B),B)|~in_environment(A,B)|~environment(A)|~subpopulations(first_movers,efficient_producers,A,E)|~greater(E,to(A,B))|greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% cnf(235310648,plain,(greater_or_equal(t_nn_2(e,A),A)|~in_environment(e,A)|~greater(t(to(e,to(e))),to(e,A))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162490336,235089880,161860168,235083000]),[]).
%
% cnf(235315152,plain,(greater_or_equal(t_nn_2(e,to(e)),to(e))),inference(forward_subsumption_resolution__resolution,[status(thm)],[231619432,235310648,228591736]),[]).
%
% cnf(235396904,plain,(greater(growth_rate(efficient_producers,t_nn_2(e,to(e))),growth_rate(first_movers,t_nn_2(e,to(e))))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162541728,162513656,235344408,161941824,235315152]),[]).
%
% cnf(161881816,plain,(~greater(growth_rate(efficient_producers,t_nn_2(A,B)),growth_rate(first_movers,t_nn_2(A,B)))|~in_environment(A,B)|~environment(A)|~subpopulations(first_movers,efficient_producers,A,E)|~greater(E,to(A,B))|greater(growth_rate(efficient_producers,E),growth_rate(first_movers,E))),inference(rewrite,[status(thm)],[mp_earliest_time_growth_rate_exceeds]),[]).
%
% cnf(235359480,plain,(~greater(growth_rate(efficient_producers,t_nn_2(e,A)),growth_rate(first_movers,t_nn_2(e,A)))|~in_environment(e,A)|~greater(t(to(e,to(e))),to(e,A))),inference(forward_subsumption_resolution__resolution,[status(thm)],[162490336,235089880,161881816,235083000]),[]).
%
% cnf(235365976,plain,(~greater(growth_rate(efficient_producers,t_nn_2(e,to(e))),growth_rate(first_movers,t_nn_2(e,to(e))))),inference(forward_subsumption_resolution__resolution,[status(thm)],[235071000,235359480,228591736]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[235396904,235365976]),[]).
%
% END OF PROOF SEQUENCE
% faust: ../JJParser/Signature.c:39: void FreeSignatureList(SymbolNodeType**): Assertion `(*Symbols)->NumberOfUses == 0' failed.
%
%------------------------------------------------------------------------------