%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MGT035+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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 : Tue Sep 29 12:02:36 PM UTC 2026
% Result : Theorem 0.42s 0.49s
% Output : Refutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 81
% Syntax : Number of formulae : 598 ( 46 unt; 73 def)
% Number of atoms : 1880 ( 90 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 2161 ( 879 ~;1140 |; 54 &)
% ( 77 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 82 ( 80 usr; 74 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 198 ( 0 sgn 186 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( ( greater(X0,X1)
& greater(X1,X2) )
=> greater(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_transitivity) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( in_environment(X0,X1)
& in_environment(X0,X2) )
=> ( greater(X2,X1)
| X2 = X1
| greater(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_times_in_environment) ).
fof(f3,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
<=> ( greater(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal) ).
fof(f4,axiom,
! [X0,X1,X2,X3] :
( ( environment(X0)
& subpopulations(X1,X2,X0,X3) )
=> ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
<=> outcompetes(X2,X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2) ).
fof(f5,axiom,
! [X0,X1] :
( ( environment(X0)
& subpopulations(first_movers,efficient_producers,X0,X1)
& greater_or_equal(X1,equilibrium(X0)) )
=> ( ( growth_rate(first_movers,X1) = zero
& growth_rate(efficient_producers,X1) = zero )
| ( greater(growth_rate(first_movers,X1),zero)
& greater(zero,growth_rate(efficient_producers,X1)) )
| ( greater(growth_rate(efficient_producers,X1),zero)
& greater(zero,growth_rate(first_movers,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6) ).
fof(f6,axiom,
! [X0] :
( ( environment(X0)
& stable(X0) )
=> ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( ( subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) )
=> greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1) ).
fof(f7,axiom,
! [X0] :
( ( environment(X0)
& stable(X0) )
=> ? [X1] :
( in_environment(X0,X1)
& greater_or_equal(X1,equilibrium(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4) ).
fof(f8,conjecture,
! [X0] :
( ( environment(X0)
& stable(X0) )
=> ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( ( subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) )
=> outcompetes(efficient_producers,first_movers,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4) ).
fof(f9,negated_conjecture,
~ ! [X0] :
( ( environment(X0)
& stable(X0) )
=> ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( ( subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) )
=> outcompetes(efficient_producers,first_movers,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f8]) ).
fof(f10,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(ennf_transformation,[],[f1]) ).
fof(f11,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(flattening,[],[f10]) ).
fof(f12,plain,
! [X0,X1,X2] :
( greater(X2,X1)
| X2 = X1
| greater(X1,X2)
| ~ in_environment(X0,X1)
| ~ in_environment(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f13,plain,
! [X0,X1,X2] :
( greater(X2,X1)
| X2 = X1
| greater(X1,X2)
| ~ in_environment(X0,X1)
| ~ in_environment(X0,X2) ),
inference(flattening,[],[f12]) ).
fof(f14,plain,
! [X0,X1,X2,X3] :
( ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
<=> outcompetes(X2,X1,X3) )
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(ennf_transformation,[],[f4]) ).
fof(f15,plain,
! [X0,X1,X2,X3] :
( ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
<=> outcompetes(X2,X1,X3) )
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(flattening,[],[f14]) ).
fof(f16,plain,
! [X0,X1] :
( ( growth_rate(first_movers,X1) = zero
& growth_rate(efficient_producers,X1) = zero )
| ( greater(growth_rate(first_movers,X1),zero)
& greater(zero,growth_rate(efficient_producers,X1)) )
| ( greater(growth_rate(efficient_producers,X1),zero)
& greater(zero,growth_rate(first_movers,X1)) )
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0)) ),
inference(ennf_transformation,[],[f5]) ).
fof(f17,plain,
! [X0,X1] :
( ( growth_rate(first_movers,X1) = zero
& growth_rate(efficient_producers,X1) = zero )
| ( greater(growth_rate(first_movers,X1),zero)
& greater(zero,growth_rate(efficient_producers,X1)) )
| ( greater(growth_rate(efficient_producers,X1),zero)
& greater(zero,growth_rate(first_movers,X1)) )
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0)) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater_or_equal(X2,X1) ) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f19,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater_or_equal(X2,X1) ) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(flattening,[],[f18]) ).
fof(f20,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& greater_or_equal(X1,equilibrium(X0)) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f21,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& greater_or_equal(X1,equilibrium(X0)) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(flattening,[],[f20]) ).
fof(f22,plain,
? [X0] :
( ! [X1] :
( ~ in_environment(X0,X1)
| ? [X2] :
( ~ outcompetes(efficient_producers,first_movers,X2)
& subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) ) )
& environment(X0)
& stable(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f23,plain,
? [X0] :
( ! [X1] :
( ~ in_environment(X0,X1)
| ? [X2] :
( ~ outcompetes(efficient_producers,first_movers,X2)
& subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) ) )
& environment(X0)
& stable(X0) ),
inference(flattening,[],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( ( greater_or_equal(X0,X1)
| ( ~ greater(X0,X1)
& X0 != X1 ) )
& ( greater(X0,X1)
| X0 = X1
| ~ greater_or_equal(X0,X1) ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f25,plain,
! [X0,X1] :
( ( greater_or_equal(X0,X1)
| ( ~ greater(X0,X1)
& X0 != X1 ) )
& ( greater(X0,X1)
| X0 = X1
| ~ greater_or_equal(X0,X1) ) ),
inference(flattening,[],[f24]) ).
fof(f26,plain,
! [X0,X1,X2,X3] :
( ( ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
| ~ outcompetes(X2,X1,X3) )
& ( outcompetes(X2,X1,X3)
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| ~ greater(zero,growth_rate(X1,X3)) ) )
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(nnf_transformation,[],[f15]) ).
fof(f27,plain,
! [X0,X1,X2,X3] :
( ( ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
| ~ outcompetes(X2,X1,X3) )
& ( outcompetes(X2,X1,X3)
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| ~ greater(zero,growth_rate(X1,X3)) ) )
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(flattening,[],[f26]) ).
fof(f28,plain,
! [X0] :
( ( in_environment(X0,sK0(X0))
& ! [X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater_or_equal(X2,sK0(X0)) ) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f19]) ).
fof(f29,plain,
! [X0] :
( ( in_environment(X0,sK1(X0))
& greater_or_equal(sK1(X0),equilibrium(X0)) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X1,sK1(X0))],[f21]) ).
fof(f30,plain,
( ! [X1] :
( ~ in_environment(sK2,X1)
| ( ~ outcompetes(efficient_producers,first_movers,sK3(X1))
& subpopulations(first_movers,efficient_producers,sK2,sK3(X1))
& greater_or_equal(sK3(X1),X1) ) )
& environment(sK2)
& stable(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X0,sK2),skolemize(X2,sK3(X1))],[f23]) ).
fof(f31,plain,
! [X2,X0,X1] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(cnf_transformation,[],[f11]) ).
fof(f32,plain,
! [X2,X0,X1] :
( greater(X2,X1)
| X1 = X2
| greater(X1,X2)
| ~ in_environment(X0,X1)
| ~ in_environment(X0,X2) ),
inference(cnf_transformation,[],[f13]) ).
fof(f33,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f34,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f25]) ).
fof(f35,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f36,plain,
! [X2,X3,X0,X1] :
( outcompetes(X2,X1,X3)
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| ~ greater(zero,growth_rate(X1,X3))
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(cnf_transformation,[],[f27]) ).
fof(f39,plain,
! [X0,X1] :
( zero = growth_rate(efficient_producers,X1)
| greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1))
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0)) ),
inference(cnf_transformation,[],[f17]) ).
fof(f42,plain,
! [X0,X1] :
( zero = growth_rate(efficient_producers,X1)
| greater(growth_rate(first_movers,X1),zero)
| greater(growth_rate(efficient_producers,X1),zero)
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0)) ),
inference(cnf_transformation,[],[f17]) ).
fof(f46,plain,
! [X0,X1] :
( zero = growth_rate(first_movers,X1)
| greater(growth_rate(first_movers,X1),zero)
| greater(growth_rate(efficient_producers,X1),zero)
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0)) ),
inference(cnf_transformation,[],[f17]) ).
fof(f47,plain,
! [X2,X0] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater_or_equal(X2,sK0(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(cnf_transformation,[],[f28]) ).
fof(f48,plain,
! [X0] :
( in_environment(X0,sK0(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(cnf_transformation,[],[f28]) ).
fof(f49,plain,
! [X0] :
( greater_or_equal(sK1(X0),equilibrium(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(cnf_transformation,[],[f29]) ).
fof(f50,plain,
! [X0] :
( in_environment(X0,sK1(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(cnf_transformation,[],[f29]) ).
fof(f51,plain,
stable(sK2),
inference(cnf_transformation,[],[f30]) ).
fof(f52,plain,
environment(sK2),
inference(cnf_transformation,[],[f30]) ).
fof(f53,plain,
! [X1] :
( ~ in_environment(sK2,X1)
| greater_or_equal(sK3(X1),X1) ),
inference(cnf_transformation,[],[f30]) ).
fof(f54,plain,
! [X1] :
( ~ in_environment(sK2,X1)
| subpopulations(first_movers,efficient_producers,sK2,sK3(X1)) ),
inference(cnf_transformation,[],[f30]) ).
fof(f55,plain,
! [X1] :
( ~ in_environment(sK2,X1)
| ~ outcompetes(efficient_producers,first_movers,sK3(X1)) ),
inference(cnf_transformation,[],[f30]) ).
fof(f56,plain,
! [X1] : greater_or_equal(X1,X1),
inference(equality_resolution,[],[f34]) ).
fof(f57,plain,
! [X2,X0,X1] :
( greater(X1,X2)
| greater(X0,X1)
| ~ greater(X0,X2) ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f58,plain,
! [X2,X0,X1] :
( in_environment(X0,X2)
| X1 = X2
| ~ greater(X1,X2)
| in_environment(X0,X1)
| ~ greater(X2,X1) ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f59,plain,
! [X0,X1] :
( ~ greater_or_equal(X0,X1)
| greater(X0,X1) ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f60,plain,
! [X1] : ~ greater_or_equal(X1,X1),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f61,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| X0 = X1
| ~ greater(X0,X1) ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f64,plain,
! [X2,X3,X0,X1] :
( greater_or_equal(growth_rate(X2,X3),zero)
| ~ outcompetes(X2,X1,X3)
| greater(zero,growth_rate(X1,X3))
| ~ environment(X0)
| subpopulations(X1,X2,X0,X3) ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f65,plain,
! [X0,X1] :
( greater_or_equal(X1,equilibrium(X0))
| ~ greater(growth_rate(first_movers,X1),zero)
| ~ greater(growth_rate(efficient_producers,X1),zero)
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,X1)
| zero = growth_rate(first_movers,X1) ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f69,plain,
! [X0,X1] :
( greater_or_equal(X1,equilibrium(X0))
| ~ greater(growth_rate(first_movers,X1),zero)
| ~ greater(growth_rate(efficient_producers,X1),zero)
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,X1)
| zero = growth_rate(efficient_producers,X1) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f72,plain,
! [X0,X1] :
( greater_or_equal(X1,equilibrium(X0))
| ~ greater(zero,growth_rate(efficient_producers,X1))
| ~ greater(zero,growth_rate(first_movers,X1))
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,X1)
| zero = growth_rate(efficient_producers,X1) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f73,plain,
! [X0] :
( stable(X0)
| ~ environment(X0)
| ~ in_environment(X0,sK0(X0)) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f74,plain,
! [X2,X0] :
( stable(X0)
| subpopulations(first_movers,efficient_producers,X0,X2)
| greater_or_equal(X2,sK0(X0))
| ~ environment(X0)
| ~ greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f75,plain,
! [X0] :
( stable(X0)
| ~ environment(X0)
| ~ in_environment(X0,sK1(X0)) ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f76,plain,
! [X0] :
( ~ greater_or_equal(sK1(X0),equilibrium(X0))
| ~ environment(X0)
| stable(X0) ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f77,plain,
! [X1] :
( outcompetes(efficient_producers,first_movers,sK3(X1))
| in_environment(sK2,X1) ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f78,plain,
! [X1] :
( ~ subpopulations(first_movers,efficient_producers,sK2,sK3(X1))
| in_environment(sK2,X1) ),
inference(consistent_polarity_flipping,[],[f54]) ).
fof(f79,plain,
! [X1] :
( ~ greater_or_equal(sK3(X1),X1)
| in_environment(sK2,X1) ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f80,plain,
~ stable(sK2),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f81,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK0(sK2)) ),
inference(resolution,[],[f73,f80]) ).
fof(f83,definition,
( spl4_1
<=> in_environment(sK2,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f85,plain,
( ~ in_environment(sK2,sK0(sK2))
| spl4_1 ),
inference(avatar_component_clause,[],[f83]) ).
fof(f87,definition,
( spl4_2
<=> environment(sK2) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f89,plain,
( ~ environment(sK2)
| spl4_2 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f90,plain,
( ~ spl4_1
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f81,f87,f83]) ).
fof(f91,plain,
( $false
| spl4_2 ),
inference(resolution,[],[f89,f52]) ).
fof(f92,plain,
spl4_2,
inference(avatar_contradiction_clause,[],[f91]) ).
fof(f93,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK1(sK2)) ),
inference(resolution,[],[f75,f80]) ).
fof(f95,definition,
( spl4_3
<=> in_environment(sK2,sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f97,plain,
( ~ in_environment(sK2,sK1(sK2))
| spl4_3 ),
inference(avatar_component_clause,[],[f95]) ).
fof(f98,plain,
( ~ spl4_3
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f93,f87,f95]) ).
fof(f99,plain,
! [X0] :
( in_environment(sK2,X0)
| ~ greater(sK3(X0),X0)
| sK3(X0) = X0 ),
inference(resolution,[],[f61,f79]) ).
fof(f102,plain,
! [X0] :
( ~ greater(sK1(X0),equilibrium(X0))
| equilibrium(X0) = sK1(X0)
| ~ environment(X0)
| stable(X0) ),
inference(resolution,[],[f61,f76]) ).
fof(f103,plain,
( ~ greater(sK3(sK0(sK2)),sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| spl4_1 ),
inference(resolution,[],[f99,f85]) ).
fof(f104,plain,
( ~ greater(sK3(sK1(sK2)),sK1(sK2))
| sK1(sK2) = sK3(sK1(sK2))
| spl4_3 ),
inference(resolution,[],[f99,f97]) ).
fof(f106,definition,
( spl4_4
<=> sK1(sK2) = sK3(sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f108,plain,
( sK1(sK2) = sK3(sK1(sK2))
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f110,definition,
( spl4_5
<=> greater(sK3(sK1(sK2)),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f112,plain,
( ~ greater(sK3(sK1(sK2)),sK1(sK2))
| spl4_5 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f113,plain,
( spl4_4
| ~ spl4_5
| spl4_3 ),
inference(avatar_split_clause,[],[f104,f95,f110,f106]) ).
fof(f115,definition,
( spl4_6
<=> sK0(sK2) = sK3(sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f117,plain,
( sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f119,definition,
( spl4_7
<=> greater(sK3(sK0(sK2)),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f121,plain,
( ~ greater(sK3(sK0(sK2)),sK0(sK2))
| spl4_7 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f122,plain,
( spl4_6
| ~ spl4_7
| spl4_1 ),
inference(avatar_split_clause,[],[f103,f83,f119,f115]) ).
fof(f124,plain,
( ! [X0] :
( in_environment(sK2,X0)
| ~ greater(X0,sK0(sK2))
| sK0(sK2) = X0
| ~ greater(sK0(sK2),X0) )
| spl4_1 ),
inference(resolution,[],[f58,f85]) ).
fof(f128,plain,
( ~ greater(sK1(sK2),sK0(sK2))
| sK0(sK2) = sK1(sK2)
| ~ greater(sK0(sK2),sK1(sK2))
| spl4_1
| spl4_3 ),
inference(resolution,[],[f124,f97]) ).
fof(f131,definition,
( spl4_8
<=> greater(sK0(sK2),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f133,plain,
( ~ greater(sK0(sK2),sK1(sK2))
| spl4_8 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f135,definition,
( spl4_9
<=> sK0(sK2) = sK1(sK2) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f137,plain,
( sK0(sK2) = sK1(sK2)
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f139,definition,
( spl4_10
<=> greater(sK1(sK2),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f141,plain,
( ~ greater(sK1(sK2),sK0(sK2))
| spl4_10 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,plain,
( ~ spl4_8
| spl4_9
| ~ spl4_10
| spl4_1
| spl4_3 ),
inference(avatar_split_clause,[],[f128,f95,f83,f139,f135,f131]) ).
fof(f143,plain,
( ! [X0] :
( greater(X0,sK0(sK2))
| ~ greater(X0,sK1(sK2)) )
| spl4_8 ),
inference(resolution,[],[f133,f57]) ).
fof(f144,plain,
( ! [X0] :
( greater(X0,sK1(sK2))
| ~ greater(X0,sK0(sK2)) )
| spl4_10 ),
inference(resolution,[],[f141,f57]) ).
fof(f145,plain,
( ~ greater(sK3(sK0(sK2)),sK1(sK2))
| spl4_7
| spl4_8 ),
inference(resolution,[],[f143,f121]) ).
fof(f149,plain,
( ~ greater(sK3(sK1(sK2)),sK0(sK2))
| spl4_5
| spl4_10 ),
inference(resolution,[],[f144,f112]) ).
fof(f160,plain,
! [X0,X1] :
( stable(X0)
| ~ environment(X0)
| equilibrium(X0) = sK1(X0)
| greater(X1,sK1(X0))
| ~ greater(X1,equilibrium(X0)) ),
inference(resolution,[],[f102,f57]) ).
fof(f161,plain,
! [X0] :
( ~ environment(sK2)
| sK1(sK2) = equilibrium(sK2)
| greater(X0,sK1(sK2))
| ~ greater(X0,equilibrium(sK2)) ),
inference(resolution,[],[f160,f80]) ).
fof(f163,definition,
( spl4_11
<=> ! [X0] :
( greater(X0,sK1(sK2))
| ~ greater(X0,equilibrium(sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f164,plain,
( ! [X0] :
( greater(X0,sK1(sK2))
| ~ greater(X0,equilibrium(sK2)) )
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f163]) ).
fof(f166,definition,
( spl4_12
<=> sK1(sK2) = equilibrium(sK2) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f168,plain,
( sK1(sK2) = equilibrium(sK2)
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,plain,
( spl4_11
| spl4_12
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f161,f87,f166,f163]) ).
fof(f170,plain,
( ~ greater(sK3(sK1(sK2)),equilibrium(sK2))
| spl4_5
| ~ spl4_11 ),
inference(resolution,[],[f164,f112]) ).
fof(f171,plain,
( ~ greater(sK3(sK0(sK2)),equilibrium(sK2))
| spl4_7
| spl4_8
| ~ spl4_11 ),
inference(resolution,[],[f164,f145]) ).
fof(f172,plain,
( ~ greater(sK0(sK2),equilibrium(sK2))
| spl4_8
| ~ spl4_11 ),
inference(resolution,[],[f164,f133]) ).
fof(f182,plain,
! [X0] :
( subpopulations(first_movers,efficient_producers,sK2,X0)
| greater_or_equal(X0,sK0(sK2))
| ~ environment(sK2)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(resolution,[],[f74,f80]) ).
fof(f184,definition,
( spl4_13
<=> ! [X0] :
( subpopulations(first_movers,efficient_producers,sK2,X0)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| greater_or_equal(X0,sK0(sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f185,plain,
( ! [X0] :
( subpopulations(first_movers,efficient_producers,sK2,X0)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| greater_or_equal(X0,sK0(sK2)) )
| ~ spl4_13 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f186,plain,
( ~ spl4_2
| spl4_13 ),
inference(avatar_split_clause,[],[f182,f184,f87]) ).
fof(f187,plain,
( ! [X0] :
( greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(X0)),growth_rate(first_movers,sK3(X0)))
| in_environment(sK2,X0) )
| ~ spl4_13 ),
inference(resolution,[],[f185,f78]) ).
fof(f188,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| in_environment(sK2,sK0(sK2))
| in_environment(sK2,sK0(sK2))
| ~ spl4_13 ),
inference(resolution,[],[f187,f79]) ).
fof(f189,plain,
( ! [X0] :
( greater(sK3(X0),sK0(sK2))
| in_environment(sK2,X0)
| ~ greater(growth_rate(efficient_producers,sK3(X0)),growth_rate(first_movers,sK3(X0))) )
| ~ spl4_13 ),
inference(resolution,[],[f187,f59]) ).
fof(f190,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| in_environment(sK2,sK0(sK2))
| ~ spl4_13 ),
inference(duplicate_literal_removal,[],[f188]) ).
fof(f192,definition,
( spl4_14
<=> greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f194,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| spl4_14 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,plain,
( spl4_1
| ~ spl4_14
| ~ spl4_13 ),
inference(avatar_split_clause,[],[f190,f184,f192,f83]) ).
fof(f196,plain,
! [X2,X3,X0,X1] :
( greater(zero,growth_rate(X1,X2))
| ~ outcompetes(X0,X1,X2)
| ~ environment(X3)
| subpopulations(X1,X0,X3,X2)
| greater(growth_rate(X0,X2),zero) ),
inference(resolution,[],[f64,f59]) ).
fof(f197,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sK3(sK0(sK2))))
| ~ greater(X0,growth_rate(first_movers,sK3(sK0(sK2)))) )
| spl4_14 ),
inference(resolution,[],[f194,f57]) ).
fof(f199,plain,
( in_environment(sK2,sK1(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2))))
| spl4_5
| spl4_10
| ~ spl4_13 ),
inference(resolution,[],[f189,f149]) ).
fof(f201,definition,
( spl4_15
<=> greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f202,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2))))
| ~ spl4_15 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f203,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2))))
| spl4_15 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f204,plain,
( ~ spl4_15
| spl4_3
| spl4_5
| spl4_10
| ~ spl4_13 ),
inference(avatar_split_clause,[],[f199,f184,f139,f110,f95,f201]) ).
fof(f205,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ~ greater(X0,growth_rate(first_movers,sK3(sK1(sK2)))) )
| spl4_15 ),
inference(resolution,[],[f203,f57]) ).
fof(f206,plain,
! [X0] :
( ~ greater(growth_rate(first_movers,sK1(X0)),zero)
| ~ greater(growth_rate(efficient_producers,sK1(X0)),zero)
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK1(X0))
| zero = growth_rate(first_movers,sK1(X0))
| ~ environment(X0)
| stable(X0) ),
inference(resolution,[],[f65,f76]) ).
fof(f209,plain,
! [X0,X1] :
( greater(X0,equilibrium(X1))
| ~ greater(growth_rate(efficient_producers,X0),zero)
| ~ environment(X1)
| subpopulations(first_movers,efficient_producers,X1,X0)
| zero = growth_rate(first_movers,X0)
| ~ greater(growth_rate(first_movers,X0),zero) ),
inference(resolution,[],[f65,f59]) ).
fof(f210,plain,
! [X0] :
( stable(X0)
| ~ greater(growth_rate(efficient_producers,sK1(X0)),zero)
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK1(X0))
| zero = growth_rate(first_movers,sK1(X0))
| ~ greater(growth_rate(first_movers,sK1(X0)),zero) ),
inference(duplicate_literal_removal,[],[f206]) ).
fof(f241,plain,
! [X0] :
( ~ greater(zero,growth_rate(efficient_producers,sK1(X0)))
| ~ greater(zero,growth_rate(first_movers,sK1(X0)))
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK1(X0))
| zero = growth_rate(efficient_producers,sK1(X0))
| ~ environment(X0)
| stable(X0) ),
inference(resolution,[],[f72,f76]) ).
fof(f242,plain,
! [X0] :
( in_environment(sK2,equilibrium(X0))
| ~ greater(zero,growth_rate(first_movers,sK3(equilibrium(X0))))
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK3(equilibrium(X0)))
| zero = growth_rate(efficient_producers,sK3(equilibrium(X0)))
| ~ greater(zero,growth_rate(efficient_producers,sK3(equilibrium(X0)))) ),
inference(resolution,[],[f72,f79]) ).
fof(f244,plain,
! [X0,X1] :
( greater(X0,equilibrium(X1))
| ~ greater(zero,growth_rate(first_movers,X0))
| ~ environment(X1)
| subpopulations(first_movers,efficient_producers,X1,X0)
| zero = growth_rate(efficient_producers,X0)
| ~ greater(zero,growth_rate(efficient_producers,X0)) ),
inference(resolution,[],[f72,f59]) ).
fof(f245,plain,
! [X0] :
( stable(X0)
| ~ greater(zero,growth_rate(first_movers,sK1(X0)))
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK1(X0))
| zero = growth_rate(efficient_producers,sK1(X0))
| ~ greater(zero,growth_rate(efficient_producers,sK1(X0))) ),
inference(duplicate_literal_removal,[],[f241]) ).
fof(f249,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(sK1(sK2)))
| zero = growth_rate(first_movers,sK3(sK1(sK2)))
| ~ greater(growth_rate(first_movers,sK3(sK1(sK2))),zero)
| spl4_5
| ~ spl4_11 ),
inference(resolution,[],[f209,f170]) ).
fof(f250,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(sK0(sK2)))
| zero = growth_rate(first_movers,sK3(sK0(sK2)))
| ~ greater(growth_rate(first_movers,sK3(sK0(sK2))),zero)
| spl4_7
| spl4_8
| ~ spl4_11 ),
inference(resolution,[],[f209,f171]) ).
fof(f253,definition,
( spl4_16
<=> greater(growth_rate(first_movers,sK3(sK0(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_16])],[avatar_definition]) ).
fof(f255,plain,
( ~ greater(growth_rate(first_movers,sK3(sK0(sK2))),zero)
| spl4_16 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f257,definition,
( spl4_17
<=> zero = growth_rate(first_movers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f258,plain,
( zero != growth_rate(first_movers,sK3(sK0(sK2)))
| spl4_17 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( zero = growth_rate(first_movers,sK3(sK0(sK2)))
| ~ spl4_17 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f261,definition,
( spl4_18
<=> subpopulations(first_movers,efficient_producers,sK2,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_18])],[avatar_definition]) ).
fof(f262,plain,
( ~ subpopulations(first_movers,efficient_producers,sK2,sK3(sK0(sK2)))
| spl4_18 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f263,plain,
( subpopulations(first_movers,efficient_producers,sK2,sK3(sK0(sK2)))
| ~ spl4_18 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f265,definition,
( spl4_19
<=> greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_19])],[avatar_definition]) ).
fof(f266,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ spl4_19 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f267,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| spl4_19 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,plain,
( ~ spl4_16
| spl4_17
| spl4_18
| ~ spl4_2
| ~ spl4_19
| spl4_7
| spl4_8
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f250,f163,f131,f119,f265,f87,f261,f257,f253]) ).
fof(f270,definition,
( spl4_20
<=> greater(growth_rate(first_movers,sK3(sK1(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition]) ).
fof(f271,plain,
( greater(growth_rate(first_movers,sK3(sK1(sK2))),zero)
| ~ spl4_20 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f272,plain,
( ~ greater(growth_rate(first_movers,sK3(sK1(sK2))),zero)
| spl4_20 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f274,definition,
( spl4_21
<=> zero = growth_rate(first_movers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f275,plain,
( zero != growth_rate(first_movers,sK3(sK1(sK2)))
| spl4_21 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f276,plain,
( zero = growth_rate(first_movers,sK3(sK1(sK2)))
| ~ spl4_21 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f278,definition,
( spl4_22
<=> subpopulations(first_movers,efficient_producers,sK2,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_22])],[avatar_definition]) ).
fof(f279,plain,
( ~ subpopulations(first_movers,efficient_producers,sK2,sK3(sK1(sK2)))
| spl4_22 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f280,plain,
( subpopulations(first_movers,efficient_producers,sK2,sK3(sK1(sK2)))
| ~ spl4_22 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f282,definition,
( spl4_23
<=> greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition]) ).
fof(f283,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ spl4_23 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f284,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| spl4_23 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f285,plain,
( ~ spl4_20
| spl4_21
| spl4_22
| ~ spl4_2
| ~ spl4_23
| spl4_5
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f249,f163,f110,f282,f87,f278,f274,f270]) ).
fof(f287,definition,
( spl4_24
<=> greater(growth_rate(first_movers,sK1(sK2)),zero) ),
introduced(definition,[new_symbols(definition,[spl4_24])],[avatar_definition]) ).
fof(f289,plain,
( ~ greater(growth_rate(first_movers,sK1(sK2)),zero)
| spl4_24 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f291,definition,
( spl4_25
<=> zero = growth_rate(first_movers,sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
fof(f293,plain,
( zero = growth_rate(first_movers,sK1(sK2))
| ~ spl4_25 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f295,definition,
( spl4_26
<=> subpopulations(first_movers,efficient_producers,sK2,sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f296,plain,
( ~ subpopulations(first_movers,efficient_producers,sK2,sK1(sK2))
| spl4_26 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f299,definition,
( spl4_27
<=> greater(growth_rate(efficient_producers,sK1(sK2)),zero) ),
introduced(definition,[new_symbols(definition,[spl4_27])],[avatar_definition]) ).
fof(f301,plain,
( ~ greater(growth_rate(efficient_producers,sK1(sK2)),zero)
| spl4_27 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f304,definition,
( spl4_28
<=> greater(growth_rate(first_movers,sK0(sK2)),zero) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f306,plain,
( ~ greater(growth_rate(first_movers,sK0(sK2)),zero)
| spl4_28 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f308,definition,
( spl4_29
<=> zero = growth_rate(first_movers,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_29])],[avatar_definition]) ).
fof(f312,definition,
( spl4_30
<=> subpopulations(first_movers,efficient_producers,sK2,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f313,plain,
( ~ subpopulations(first_movers,efficient_producers,sK2,sK0(sK2))
| spl4_30 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f316,definition,
( spl4_31
<=> greater(growth_rate(efficient_producers,sK0(sK2)),zero) ),
introduced(definition,[new_symbols(definition,[spl4_31])],[avatar_definition]) ).
fof(f318,plain,
( ~ greater(growth_rate(efficient_producers,sK0(sK2)),zero)
| spl4_31 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f320,plain,
( ! [X0] :
( greater(X0,growth_rate(first_movers,sK0(sK2)))
| ~ greater(X0,zero) )
| spl4_28 ),
inference(resolution,[],[f306,f57]) ).
fof(f323,definition,
( spl4_32
<=> greater_or_equal(sK0(sK2),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_32])],[avatar_definition]) ).
fof(f325,plain,
( greater_or_equal(sK0(sK2),sK0(sK2))
| ~ spl4_32 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f327,definition,
( spl4_33
<=> greater(growth_rate(efficient_producers,sK0(sK2)),growth_rate(first_movers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition]) ).
fof(f329,plain,
( ~ greater(growth_rate(efficient_producers,sK0(sK2)),growth_rate(first_movers,sK0(sK2)))
| spl4_33 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f332,plain,
( ! [X0] :
( greater(X0,growth_rate(first_movers,sK1(sK2)))
| ~ greater(X0,zero) )
| spl4_24 ),
inference(resolution,[],[f289,f57]) ).
fof(f335,definition,
( spl4_34
<=> greater_or_equal(sK1(sK2),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_34])],[avatar_definition]) ).
fof(f337,plain,
( greater_or_equal(sK1(sK2),sK0(sK2))
| ~ spl4_34 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f339,definition,
( spl4_35
<=> greater(growth_rate(efficient_producers,sK1(sK2)),growth_rate(first_movers,sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_35])],[avatar_definition]) ).
fof(f341,plain,
( ~ greater(growth_rate(efficient_producers,sK1(sK2)),growth_rate(first_movers,sK1(sK2)))
| spl4_35 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f345,plain,
( ! [X0] :
( greater(X0,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ greater(X0,zero) )
| spl4_20 ),
inference(resolution,[],[f272,f57]) ).
fof(f348,plain,
( ! [X0] :
( greater(X0,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ greater(X0,zero) )
| spl4_16 ),
inference(resolution,[],[f255,f57]) ).
fof(f351,plain,
( ~ greater(growth_rate(efficient_producers,sK0(sK2)),zero)
| spl4_28
| spl4_33 ),
inference(resolution,[],[f329,f320]) ).
fof(f352,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sK0(sK2)))
| ~ greater(X0,growth_rate(first_movers,sK0(sK2))) )
| spl4_33 ),
inference(resolution,[],[f329,f57]) ).
fof(f353,plain,
( ~ greater(growth_rate(efficient_producers,sK1(sK2)),zero)
| spl4_24
| spl4_35 ),
inference(resolution,[],[f341,f332]) ).
fof(f354,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sK1(sK2)))
| ~ greater(X0,growth_rate(first_movers,sK1(sK2))) )
| spl4_35 ),
inference(resolution,[],[f341,f57]) ).
fof(f355,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| spl4_15
| spl4_20 ),
inference(resolution,[],[f345,f203]) ).
fof(f362,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| spl4_14
| spl4_16 ),
inference(resolution,[],[f348,f194]) ).
fof(f376,definition,
( spl4_36
<=> greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_36])],[avatar_definition]) ).
fof(f378,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2))))
| spl4_36 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f380,definition,
( spl4_37
<=> greater(zero,growth_rate(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_37])],[avatar_definition]) ).
fof(f382,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| spl4_37 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f385,definition,
( spl4_38
<=> greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_38])],[avatar_definition]) ).
fof(f386,plain,
( greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_38 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f387,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| spl4_38 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f389,definition,
( spl4_39
<=> greater(zero,growth_rate(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_39])],[avatar_definition]) ).
fof(f390,plain,
( greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ spl4_39 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f391,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| spl4_39 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f394,definition,
( spl4_40
<=> greater(zero,growth_rate(efficient_producers,sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_40])],[avatar_definition]) ).
fof(f396,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK1(sK2)))
| spl4_40 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f398,definition,
( spl4_41
<=> greater(zero,growth_rate(first_movers,sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_41])],[avatar_definition]) ).
fof(f403,definition,
( spl4_42
<=> greater(zero,growth_rate(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_42])],[avatar_definition]) ).
fof(f405,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK0(sK2)))
| spl4_42 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f407,definition,
( spl4_43
<=> greater(zero,growth_rate(first_movers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_43])],[avatar_definition]) ).
fof(f409,plain,
( ~ greater(zero,growth_rate(first_movers,sK0(sK2)))
| spl4_43 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f412,plain,
( ~ greater(zero,growth_rate(first_movers,sK0(sK2)))
| spl4_33
| spl4_42 ),
inference(resolution,[],[f405,f352]) ).
fof(f416,plain,
( ! [X0,X1] :
( greater(growth_rate(X0,sK0(sK2)),zero)
| ~ environment(X1)
| subpopulations(first_movers,X0,X1,sK0(sK2))
| ~ outcompetes(X0,first_movers,sK0(sK2)) )
| spl4_43 ),
inference(resolution,[],[f409,f196]) ).
fof(f417,plain,
( ~ greater(zero,zero)
| spl4_28
| spl4_43 ),
inference(resolution,[],[f409,f320]) ).
fof(f420,plain,
( ~ greater(zero,growth_rate(first_movers,sK1(sK2)))
| spl4_35
| spl4_40 ),
inference(resolution,[],[f396,f354]) ).
fof(f428,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| spl4_15
| spl4_38 ),
inference(resolution,[],[f387,f205]) ).
fof(f430,plain,
( ! [X0,X1] :
( greater(growth_rate(X0,sK3(sK1(sK2))),zero)
| ~ environment(X1)
| subpopulations(first_movers,X0,X1,sK3(sK1(sK2)))
| ~ outcompetes(X0,first_movers,sK3(sK1(sK2))) )
| spl4_39 ),
inference(resolution,[],[f391,f196]) ).
fof(f435,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| spl4_14
| spl4_36 ),
inference(resolution,[],[f378,f197]) ).
fof(f437,plain,
( ! [X0,X1] :
( greater(growth_rate(X0,sK3(sK0(sK2))),zero)
| ~ environment(X1)
| subpopulations(first_movers,X0,X1,sK3(sK0(sK2)))
| ~ outcompetes(X0,first_movers,sK3(sK0(sK2))) )
| spl4_37 ),
inference(resolution,[],[f382,f196]) ).
fof(f1193,plain,
( ! [X0] :
( ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK0(sK2))
| ~ outcompetes(efficient_producers,first_movers,sK0(sK2)) )
| spl4_31
| spl4_43 ),
inference(resolution,[],[f416,f318]) ).
fof(f1195,definition,
( spl4_50
<=> outcompetes(efficient_producers,first_movers,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_50])],[avatar_definition]) ).
fof(f1199,definition,
( spl4_51
<=> ! [X0] :
( ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK0(sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl4_51])],[avatar_definition]) ).
fof(f1200,plain,
( ! [X0] :
( subpopulations(first_movers,efficient_producers,X0,sK0(sK2))
| ~ environment(X0) )
| ~ spl4_51 ),
inference(avatar_component_clause,[],[f1199]) ).
fof(f1201,plain,
( ~ spl4_50
| spl4_51
| spl4_31
| spl4_43 ),
inference(avatar_split_clause,[],[f1193,f407,f316,f1199,f1195]) ).
fof(f1212,plain,
( ~ greater(growth_rate(efficient_producers,sK1(sK2)),zero)
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK1(sK2))
| zero = growth_rate(first_movers,sK1(sK2))
| ~ greater(growth_rate(first_movers,sK1(sK2)),zero) ),
inference(resolution,[],[f210,f80]) ).
fof(f1254,definition,
( spl4_60
<=> outcompetes(efficient_producers,first_movers,sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f1255,plain,
( outcompetes(efficient_producers,first_movers,sK1(sK2))
| ~ spl4_60 ),
inference(avatar_component_clause,[],[f1254]) ).
fof(f1319,plain,
( ! [X0] :
( ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2)))
| ~ outcompetes(efficient_producers,first_movers,sK3(sK1(sK2))) )
| spl4_23
| spl4_39 ),
inference(resolution,[],[f430,f284]) ).
fof(f1321,definition,
( spl4_70
<=> outcompetes(efficient_producers,first_movers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_70])],[avatar_definition]) ).
fof(f1322,plain,
( outcompetes(efficient_producers,first_movers,sK3(sK1(sK2)))
| ~ spl4_70 ),
inference(avatar_component_clause,[],[f1321]) ).
fof(f1323,plain,
( ~ outcompetes(efficient_producers,first_movers,sK3(sK1(sK2)))
| spl4_70 ),
inference(avatar_component_clause,[],[f1321]) ).
fof(f1325,definition,
( spl4_71
<=> ! [X0] :
( ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_71])],[avatar_definition]) ).
fof(f1326,plain,
( ! [X0] :
( subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2)))
| ~ environment(X0) )
| ~ spl4_71 ),
inference(avatar_component_clause,[],[f1325]) ).
fof(f1327,plain,
( ~ spl4_70
| spl4_71
| spl4_23
| spl4_39 ),
inference(avatar_split_clause,[],[f1319,f389,f282,f1325,f1321]) ).
fof(f1336,plain,
( in_environment(sK2,sK1(sK2))
| spl4_70 ),
inference(resolution,[],[f1323,f77]) ).
fof(f1339,plain,
( spl4_3
| spl4_70 ),
inference(avatar_split_clause,[],[f1336,f1321,f95]) ).
fof(f1340,plain,
( ~ spl4_23
| spl4_15
| spl4_20 ),
inference(avatar_split_clause,[],[f355,f270,f201,f282]) ).
fof(f1342,definition,
( spl4_74
<=> zero = growth_rate(efficient_producers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_74])],[avatar_definition]) ).
fof(f1343,plain,
( zero != growth_rate(efficient_producers,sK3(sK1(sK2)))
| spl4_74 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1344,plain,
( zero = growth_rate(efficient_producers,sK3(sK1(sK2)))
| ~ spl4_74 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1346,plain,
( ~ spl4_39
| spl4_15
| spl4_38 ),
inference(avatar_split_clause,[],[f428,f385,f201,f389]) ).
fof(f1348,definition,
( spl4_75
<=> greater_or_equal(sK3(sK1(sK2)),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_75])],[avatar_definition]) ).
fof(f1349,plain,
( ~ greater_or_equal(sK3(sK1(sK2)),sK0(sK2))
| spl4_75 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1350,plain,
( greater_or_equal(sK3(sK1(sK2)),sK0(sK2))
| ~ spl4_75 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1353,plain,
( greater(sK1(sK2),sK0(sK2))
| ~ spl4_34 ),
inference(resolution,[],[f337,f59]) ).
fof(f1357,definition,
( spl4_76
<=> greater(sK3(sK1(sK2)),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_76])],[avatar_definition]) ).
fof(f1358,plain,
( greater(sK3(sK1(sK2)),sK0(sK2))
| ~ spl4_76 ),
inference(avatar_component_clause,[],[f1357]) ).
fof(f1359,plain,
( ~ greater(sK3(sK1(sK2)),sK0(sK2))
| spl4_76 ),
inference(avatar_component_clause,[],[f1357]) ).
fof(f1372,plain,
( in_environment(sK2,sK1(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2))))
| ~ spl4_13
| spl4_76 ),
inference(resolution,[],[f1359,f189]) ).
fof(f1384,definition,
( spl4_79
<=> greater(zero,zero) ),
introduced(definition,[new_symbols(definition,[spl4_79])],[avatar_definition]) ).
fof(f1398,plain,
( in_environment(sK2,sK1(sK2))
| ~ spl4_22 ),
inference(resolution,[],[f280,f78]) ).
fof(f1399,plain,
( spl4_3
| ~ spl4_22 ),
inference(avatar_split_clause,[],[f1398,f278,f95]) ).
fof(f1411,plain,
( ~ in_environment(sK2,equilibrium(sK2))
| spl4_3
| ~ spl4_12 ),
inference(superposition,[],[f97,f168]) ).
fof(f1413,plain,
( ~ greater(sK3(equilibrium(sK2)),equilibrium(sK2))
| spl4_5
| ~ spl4_12 ),
inference(superposition,[],[f112,f168]) ).
fof(f1415,plain,
( ~ greater(sK0(sK2),equilibrium(sK2))
| spl4_8
| ~ spl4_12 ),
inference(superposition,[],[f133,f168]) ).
fof(f1418,plain,
( ~ greater(sK3(sK0(sK2)),equilibrium(sK2))
| spl4_7
| spl4_8
| ~ spl4_12 ),
inference(superposition,[],[f145,f168]) ).
fof(f1420,plain,
( zero != growth_rate(first_movers,sK3(equilibrium(sK2)))
| ~ spl4_12
| spl4_21 ),
inference(superposition,[],[f275,f168]) ).
fof(f1421,plain,
( ~ subpopulations(first_movers,efficient_producers,sK2,sK3(equilibrium(sK2)))
| ~ spl4_12
| spl4_22 ),
inference(superposition,[],[f279,f168]) ).
fof(f1422,plain,
( ~ greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ~ spl4_12
| spl4_23 ),
inference(superposition,[],[f284,f168]) ).
fof(f1432,plain,
( greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| ~ spl4_12
| ~ spl4_38 ),
inference(superposition,[],[f386,f168]) ).
fof(f1475,plain,
( outcompetes(efficient_producers,first_movers,sK3(equilibrium(sK2)))
| ~ spl4_12
| ~ spl4_70 ),
inference(superposition,[],[f1322,f168]) ).
fof(f1477,plain,
( ~ greater(sK3(equilibrium(sK2)),sK0(sK2))
| ~ spl4_12
| spl4_76 ),
inference(superposition,[],[f1359,f168]) ).
fof(f1487,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(equilibrium(sK2))))
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(equilibrium(sK2)))
| zero = growth_rate(efficient_producers,sK3(equilibrium(sK2)))
| ~ greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| spl4_3
| ~ spl4_12 ),
inference(resolution,[],[f1411,f242]) ).
fof(f1493,definition,
( spl4_80
<=> greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_80])],[avatar_definition]) ).
fof(f1495,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| spl4_80 ),
inference(avatar_component_clause,[],[f1493]) ).
fof(f1497,definition,
( spl4_81
<=> zero = growth_rate(efficient_producers,sK3(equilibrium(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_81])],[avatar_definition]) ).
fof(f1501,definition,
( spl4_82
<=> subpopulations(first_movers,efficient_producers,sK2,sK3(equilibrium(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_82])],[avatar_definition]) ).
fof(f1505,definition,
( spl4_83
<=> greater(zero,growth_rate(first_movers,sK3(equilibrium(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_83])],[avatar_definition]) ).
fof(f1507,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(equilibrium(sK2))))
| spl4_83 ),
inference(avatar_component_clause,[],[f1505]) ).
fof(f1508,plain,
( ~ spl4_80
| spl4_81
| spl4_82
| ~ spl4_2
| ~ spl4_83
| spl4_3
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f1487,f166,f95,f1505,f87,f1501,f1497,f1493]) ).
fof(f1510,definition,
( spl4_84
<=> zero = growth_rate(first_movers,sK3(equilibrium(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_84])],[avatar_definition]) ).
fof(f1545,plain,
( ~ spl4_15
| spl4_3
| ~ spl4_13
| spl4_76 ),
inference(avatar_split_clause,[],[f1372,f1357,f184,f95,f201]) ).
fof(f1555,plain,
( greater(sK3(sK1(sK2)),sK0(sK2))
| ~ spl4_75 ),
inference(resolution,[],[f1350,f59]) ).
fof(f1577,definition,
( spl4_86
<=> greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),growth_rate(first_movers,sK3(equilibrium(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_86])],[avatar_definition]) ).
fof(f1579,plain,
( ~ greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),growth_rate(first_movers,sK3(equilibrium(sK2))))
| spl4_86 ),
inference(avatar_component_clause,[],[f1577]) ).
fof(f1584,definition,
( spl4_87
<=> greater(sK3(equilibrium(sK2)),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_87])],[avatar_definition]) ).
fof(f1586,plain,
( ~ greater(sK3(equilibrium(sK2)),sK0(sK2))
| spl4_87 ),
inference(avatar_component_clause,[],[f1584]) ).
fof(f1592,plain,
( in_environment(sK2,equilibrium(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),growth_rate(first_movers,sK3(equilibrium(sK2))))
| ~ spl4_13
| spl4_87 ),
inference(resolution,[],[f1586,f189]) ).
fof(f1596,plain,
( ! [X0,X1] :
( greater(growth_rate(X0,sK3(equilibrium(sK2))),zero)
| ~ environment(X1)
| subpopulations(first_movers,X0,X1,sK3(equilibrium(sK2)))
| ~ outcompetes(X0,first_movers,sK3(equilibrium(sK2))) )
| spl4_83 ),
inference(resolution,[],[f1507,f196]) ).
fof(f1628,definition,
( spl4_89
<=> greater(growth_rate(first_movers,sK3(equilibrium(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_89])],[avatar_definition]) ).
fof(f1632,definition,
( spl4_90
<=> greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_90])],[avatar_definition]) ).
fof(f1634,plain,
( ~ greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| spl4_90 ),
inference(avatar_component_clause,[],[f1632]) ).
fof(f1654,plain,
( ~ environment(sK2)
| in_environment(sK2,sK1(sK2))
| ~ spl4_71 ),
inference(resolution,[],[f1326,f78]) ).
fof(f1655,plain,
( spl4_3
| ~ spl4_2
| ~ spl4_71 ),
inference(avatar_split_clause,[],[f1654,f1325,f87,f95]) ).
fof(f1695,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| ~ greater(X0,growth_rate(first_movers,sK3(equilibrium(sK2)))) )
| spl4_86 ),
inference(resolution,[],[f1579,f57]) ).
fof(f1770,plain,
( ~ greater(zero,growth_rate(first_movers,sK1(sK2)))
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK1(sK2))
| zero = growth_rate(efficient_producers,sK1(sK2))
| ~ greater(zero,growth_rate(efficient_producers,sK1(sK2))) ),
inference(resolution,[],[f245,f80]) ).
fof(f1972,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(equilibrium(sK2))))
| spl4_80
| spl4_86 ),
inference(resolution,[],[f1695,f1495]) ).
fof(f2040,plain,
( ! [X0] :
( ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK3(equilibrium(sK2)))
| ~ outcompetes(efficient_producers,first_movers,sK3(equilibrium(sK2))) )
| spl4_83
| spl4_90 ),
inference(resolution,[],[f1596,f1634]) ).
fof(f2042,definition,
( spl4_97
<=> outcompetes(efficient_producers,first_movers,sK3(equilibrium(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_97])],[avatar_definition]) ).
fof(f2046,definition,
( spl4_98
<=> ! [X0] :
( ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK3(equilibrium(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_98])],[avatar_definition]) ).
fof(f2047,plain,
( ! [X0] :
( subpopulations(first_movers,efficient_producers,X0,sK3(equilibrium(sK2)))
| ~ environment(X0) )
| ~ spl4_98 ),
inference(avatar_component_clause,[],[f2046]) ).
fof(f2048,plain,
( ~ spl4_97
| spl4_98
| spl4_83
| spl4_90 ),
inference(avatar_split_clause,[],[f2040,f1632,f1505,f2046,f2042]) ).
fof(f2484,plain,
( ! [X0] :
( ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2)))
| ~ outcompetes(efficient_producers,first_movers,sK3(sK0(sK2))) )
| spl4_19
| spl4_37 ),
inference(resolution,[],[f437,f267]) ).
fof(f2486,definition,
( spl4_107
<=> outcompetes(efficient_producers,first_movers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_107])],[avatar_definition]) ).
fof(f2487,plain,
( outcompetes(efficient_producers,first_movers,sK3(sK0(sK2)))
| ~ spl4_107 ),
inference(avatar_component_clause,[],[f2486]) ).
fof(f2488,plain,
( ~ outcompetes(efficient_producers,first_movers,sK3(sK0(sK2)))
| spl4_107 ),
inference(avatar_component_clause,[],[f2486]) ).
fof(f2490,definition,
( spl4_108
<=> ! [X0] :
( ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_108])],[avatar_definition]) ).
fof(f2491,plain,
( ! [X0] :
( subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2)))
| ~ environment(X0) )
| ~ spl4_108 ),
inference(avatar_component_clause,[],[f2490]) ).
fof(f2492,plain,
( ~ spl4_107
| spl4_108
| spl4_19
| spl4_37 ),
inference(avatar_split_clause,[],[f2484,f380,f265,f2490,f2486]) ).
fof(f2501,plain,
( in_environment(sK2,sK0(sK2))
| spl4_107 ),
inference(resolution,[],[f2488,f77]) ).
fof(f2504,plain,
( spl4_1
| spl4_107 ),
inference(avatar_split_clause,[],[f2501,f2486,f83]) ).
fof(f2508,plain,
( ~ environment(sK2)
| in_environment(sK2,sK0(sK2))
| ~ spl4_108 ),
inference(resolution,[],[f2491,f78]) ).
fof(f2509,plain,
( spl4_1
| ~ spl4_2
| ~ spl4_108 ),
inference(avatar_split_clause,[],[f2508,f2490,f87,f83]) ).
fof(f2511,plain,
( ~ spl4_19
| spl4_14
| spl4_16 ),
inference(avatar_split_clause,[],[f362,f253,f192,f265]) ).
fof(f2514,definition,
( spl4_111
<=> zero = growth_rate(efficient_producers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_111])],[avatar_definition]) ).
fof(f2515,plain,
( zero != growth_rate(efficient_producers,sK3(sK0(sK2)))
| spl4_111 ),
inference(avatar_component_clause,[],[f2514]) ).
fof(f2516,plain,
( zero = growth_rate(efficient_producers,sK3(sK0(sK2)))
| ~ spl4_111 ),
inference(avatar_component_clause,[],[f2514]) ).
fof(f2518,plain,
( ~ spl4_37
| spl4_14
| spl4_36 ),
inference(avatar_split_clause,[],[f435,f376,f192,f380]) ).
fof(f2526,plain,
( ~ greater(sK3(sK0(sK2)),sK0(sK2))
| spl4_5
| ~ spl4_9 ),
inference(superposition,[],[f112,f137]) ).
fof(f2533,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ~ spl4_9
| ~ spl4_15 ),
inference(superposition,[],[f202,f137]) ).
fof(f2540,plain,
( ~ subpopulations(first_movers,efficient_producers,sK2,sK0(sK2))
| ~ spl4_9
| spl4_26 ),
inference(superposition,[],[f296,f137]) ).
fof(f2541,plain,
( ~ greater(growth_rate(efficient_producers,sK0(sK2)),zero)
| ~ spl4_9
| spl4_27 ),
inference(superposition,[],[f301,f137]) ).
fof(f2549,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK0(sK2)))
| ~ spl4_9
| spl4_40 ),
inference(superposition,[],[f396,f137]) ).
fof(f2586,plain,
( greater(sK3(sK0(sK2)),sK0(sK2))
| ~ spl4_9
| ~ spl4_76 ),
inference(superposition,[],[f1358,f137]) ).
fof(f2646,definition,
( spl4_113
<=> greater_or_equal(sK0(sK2),equilibrium(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_113])],[avatar_definition]) ).
fof(f2647,plain,
( greater_or_equal(sK0(sK2),equilibrium(sK2))
| ~ spl4_113 ),
inference(avatar_component_clause,[],[f2646]) ).
fof(f2648,plain,
( ~ greater_or_equal(sK0(sK2),equilibrium(sK2))
| spl4_113 ),
inference(avatar_component_clause,[],[f2646]) ).
fof(f2651,definition,
( spl4_114
<=> sK0(sK2) = equilibrium(sK2) ),
introduced(definition,[new_symbols(definition,[spl4_114])],[avatar_definition]) ).
fof(f2653,plain,
( sK0(sK2) = equilibrium(sK2)
| ~ spl4_114 ),
inference(avatar_component_clause,[],[f2651]) ).
fof(f2655,definition,
( spl4_115
<=> greater(sK0(sK2),equilibrium(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_115])],[avatar_definition]) ).
fof(f2659,plain,
( spl4_7
| ~ spl4_9
| ~ spl4_76 ),
inference(avatar_split_clause,[],[f2586,f1357,f135,f119]) ).
fof(f2668,plain,
( spl4_14
| ~ spl4_9
| ~ spl4_15 ),
inference(avatar_split_clause,[],[f2533,f201,f135,f192]) ).
fof(f2670,plain,
( spl4_10
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f1353,f335,f139]) ).
fof(f2672,plain,
( ~ greater(growth_rate(first_movers,sK0(sK2)),zero)
| ~ greater(growth_rate(efficient_producers,sK0(sK2)),zero)
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK0(sK2))
| zero = growth_rate(first_movers,sK0(sK2))
| spl4_113 ),
inference(resolution,[],[f2648,f65]) ).
fof(f2676,plain,
( ~ greater(growth_rate(first_movers,sK0(sK2)),zero)
| ~ greater(growth_rate(efficient_producers,sK0(sK2)),zero)
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK0(sK2))
| zero = growth_rate(efficient_producers,sK0(sK2))
| spl4_113 ),
inference(resolution,[],[f2648,f69]) ).
fof(f2694,plain,
( ~ subpopulations(first_movers,efficient_producers,sK2,sK1(sK2))
| ~ spl4_4
| spl4_22 ),
inference(superposition,[],[f279,f108]) ).
fof(f2697,plain,
( greater(zero,growth_rate(first_movers,sK1(sK2)))
| ~ spl4_4
| ~ spl4_39 ),
inference(superposition,[],[f390,f108]) ).
fof(f2703,plain,
( outcompetes(efficient_producers,first_movers,sK1(sK2))
| ~ spl4_4
| ~ spl4_70 ),
inference(superposition,[],[f1322,f108]) ).
fof(f2705,plain,
( zero != growth_rate(efficient_producers,sK1(sK2))
| ~ spl4_4
| spl4_74 ),
inference(superposition,[],[f1343,f108]) ).
fof(f2707,plain,
( greater(sK1(sK2),sK0(sK2))
| ~ spl4_4
| ~ spl4_76 ),
inference(superposition,[],[f1358,f108]) ).
fof(f2751,plain,
( spl4_10
| ~ spl4_4
| ~ spl4_76 ),
inference(avatar_split_clause,[],[f2707,f1357,f106,f139]) ).
fof(f2754,plain,
( spl4_60
| ~ spl4_4
| ~ spl4_70 ),
inference(avatar_split_clause,[],[f2703,f1321,f106,f1254]) ).
fof(f2757,plain,
( spl4_41
| ~ spl4_4
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f2697,f389,f106,f398]) ).
fof(f2775,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| spl4_14
| ~ spl4_17 ),
inference(superposition,[],[f194,f259]) ).
fof(f2785,plain,
( ~ spl4_19
| spl4_14
| ~ spl4_17 ),
inference(avatar_split_clause,[],[f2775,f257,f192,f265]) ).
fof(f2786,plain,
( in_environment(sK2,sK0(sK2))
| ~ spl4_18 ),
inference(resolution,[],[f263,f78]) ).
fof(f2787,plain,
( spl4_1
| ~ spl4_18 ),
inference(avatar_split_clause,[],[f2786,f261,f83]) ).
fof(f2788,plain,
( ~ greater(growth_rate(efficient_producers,sK0(sK2)),growth_rate(first_movers,sK0(sK2)))
| ~ spl4_6
| spl4_14 ),
inference(superposition,[],[f194,f117]) ).
fof(f2791,plain,
( zero != growth_rate(first_movers,sK0(sK2))
| ~ spl4_6
| spl4_17 ),
inference(superposition,[],[f258,f117]) ).
fof(f2795,plain,
( outcompetes(efficient_producers,first_movers,sK0(sK2))
| ~ spl4_6
| ~ spl4_107 ),
inference(superposition,[],[f2487,f117]) ).
fof(f2804,plain,
( spl4_50
| ~ spl4_6
| ~ spl4_107 ),
inference(avatar_split_clause,[],[f2795,f2486,f115,f1195]) ).
fof(f2812,plain,
( ~ spl4_29
| ~ spl4_6
| spl4_17 ),
inference(avatar_split_clause,[],[f2791,f257,f115,f308]) ).
fof(f2830,plain,
( ~ subpopulations(first_movers,efficient_producers,sK2,sK0(sK2))
| ~ spl4_6
| spl4_18 ),
inference(superposition,[],[f262,f117]) ).
fof(f2831,plain,
( greater(growth_rate(efficient_producers,sK0(sK2)),zero)
| ~ spl4_6
| ~ spl4_19 ),
inference(superposition,[],[f266,f117]) ).
fof(f2832,plain,
( spl4_31
| ~ spl4_6
| ~ spl4_19 ),
inference(avatar_split_clause,[],[f2831,f265,f115,f316]) ).
fof(f2835,plain,
( spl4_97
| ~ spl4_12
| ~ spl4_70 ),
inference(avatar_split_clause,[],[f1475,f1321,f166,f2042]) ).
fof(f2836,plain,
( ~ spl4_83
| spl4_80
| spl4_86 ),
inference(avatar_split_clause,[],[f1972,f1577,f1493,f1505]) ).
fof(f2839,plain,
( ~ spl4_82
| ~ spl4_12
| spl4_22 ),
inference(avatar_split_clause,[],[f1421,f278,f166,f1501]) ).
fof(f2842,plain,
( ~ spl4_90
| ~ spl4_12
| spl4_23 ),
inference(avatar_split_clause,[],[f1422,f282,f166,f1632]) ).
fof(f2844,definition,
( spl4_117
<=> in_environment(sK2,equilibrium(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_117])],[avatar_definition]) ).
fof(f2847,plain,
( ~ spl4_86
| spl4_117
| ~ spl4_13
| spl4_87 ),
inference(avatar_split_clause,[],[f1592,f1584,f184,f2844,f1577]) ).
fof(f2848,plain,
( ~ spl4_30
| ~ spl4_6
| spl4_18 ),
inference(avatar_split_clause,[],[f2830,f261,f115,f312]) ).
fof(f2850,definition,
( spl4_118
<=> zero = growth_rate(efficient_producers,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_118])],[avatar_definition]) ).
fof(f2915,plain,
( zero != growth_rate(efficient_producers,sK3(equilibrium(sK2)))
| ~ spl4_12
| spl4_74 ),
inference(superposition,[],[f1343,f168]) ).
fof(f2946,plain,
( ~ spl4_81
| ~ spl4_12
| spl4_74 ),
inference(avatar_split_clause,[],[f2915,f1342,f166,f1497]) ).
fof(f2964,plain,
( ~ greater(growth_rate(efficient_producers,sK0(sK2)),growth_rate(first_movers,sK0(sK2)))
| greater_or_equal(sK0(sK2),sK0(sK2))
| ~ spl4_13
| spl4_30 ),
inference(resolution,[],[f313,f185]) ).
fof(f2985,plain,
( ~ spl4_41
| spl4_35
| spl4_40 ),
inference(avatar_split_clause,[],[f420,f394,f339,f398]) ).
fof(f2988,plain,
( ~ spl4_27
| spl4_24
| spl4_35 ),
inference(avatar_split_clause,[],[f353,f339,f287,f299]) ).
fof(f2990,definition,
( spl4_120
<=> zero = growth_rate(efficient_producers,sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_120])],[avatar_definition]) ).
fof(f2995,plain,
( ~ spl4_24
| spl4_25
| spl4_26
| ~ spl4_2
| ~ spl4_27 ),
inference(avatar_split_clause,[],[f1212,f299,f87,f295,f291,f287]) ).
fof(f3068,plain,
( ~ greater(zero,growth_rate(first_movers,sK0(sK2)))
| ~ spl4_6
| spl4_37 ),
inference(superposition,[],[f382,f117]) ).
fof(f3121,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| spl4_14
| ~ spl4_111 ),
inference(superposition,[],[f194,f2516]) ).
fof(f3123,plain,
( greater(zero,zero)
| ~ spl4_19
| ~ spl4_111 ),
inference(superposition,[],[f266,f2516]) ).
fof(f3137,plain,
( spl4_79
| ~ spl4_19
| ~ spl4_111 ),
inference(avatar_split_clause,[],[f3123,f2514,f265,f1384]) ).
fof(f3139,plain,
( zero != growth_rate(efficient_producers,sK0(sK2))
| ~ spl4_6
| spl4_111 ),
inference(superposition,[],[f2515,f117]) ).
fof(f3145,plain,
( ~ environment(sK2)
| spl4_30
| ~ spl4_51 ),
inference(resolution,[],[f1200,f313]) ).
fof(f3146,plain,
( ~ spl4_2
| spl4_30
| ~ spl4_51 ),
inference(avatar_split_clause,[],[f3145,f1199,f312,f87]) ).
fof(f3149,plain,
( spl4_118
| spl4_30
| ~ spl4_2
| ~ spl4_31
| ~ spl4_28
| spl4_113 ),
inference(avatar_split_clause,[],[f2676,f2646,f304,f316,f87,f312,f2850]) ).
fof(f3150,plain,
( spl4_29
| spl4_30
| ~ spl4_2
| ~ spl4_31
| ~ spl4_28
| spl4_113 ),
inference(avatar_split_clause,[],[f2672,f2646,f304,f316,f87,f312,f308]) ).
fof(f3151,plain,
( ~ spl4_115
| spl4_8
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f1415,f166,f131,f2655]) ).
fof(f3158,plain,
( ~ spl4_7
| spl4_5
| ~ spl4_9 ),
inference(avatar_split_clause,[],[f2526,f135,f110,f119]) ).
fof(f3160,plain,
( ~ spl4_31
| ~ spl4_9
| spl4_27 ),
inference(avatar_split_clause,[],[f2541,f299,f135,f316]) ).
fof(f3169,plain,
( ~ spl4_76
| spl4_5
| spl4_10 ),
inference(avatar_split_clause,[],[f149,f139,f110,f1357]) ).
fof(f3170,plain,
( ~ spl4_26
| ~ spl4_4
| spl4_22 ),
inference(avatar_split_clause,[],[f2694,f278,f106,f295]) ).
fof(f3185,definition,
( spl4_125
<=> greater(sK3(equilibrium(sK2)),equilibrium(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_125])],[avatar_definition]) ).
fof(f3187,plain,
( ~ greater(sK3(equilibrium(sK2)),equilibrium(sK2))
| spl4_125 ),
inference(avatar_component_clause,[],[f3185]) ).
fof(f3190,plain,
( ~ spl4_120
| ~ spl4_4
| spl4_74 ),
inference(avatar_split_clause,[],[f2705,f1342,f106,f2990]) ).
fof(f3192,plain,
( ~ spl4_118
| ~ spl4_6
| spl4_111 ),
inference(avatar_split_clause,[],[f3139,f2514,f115,f2850]) ).
fof(f3199,plain,
( ~ spl4_43
| spl4_33
| spl4_42 ),
inference(avatar_split_clause,[],[f412,f403,f327,f407]) ).
fof(f3221,plain,
( greater(sK0(sK2),equilibrium(sK2))
| ~ spl4_113 ),
inference(resolution,[],[f2647,f59]) ).
fof(f3222,plain,
( spl4_115
| ~ spl4_113 ),
inference(avatar_split_clause,[],[f3221,f2646,f2655]) ).
fof(f3230,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK0(sK2)))
| ~ greater(zero,growth_rate(first_movers,sK0(sK2)))
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK0(sK2))
| zero = growth_rate(efficient_producers,sK0(sK2))
| spl4_113 ),
inference(resolution,[],[f2648,f72]) ).
fof(f3232,plain,
( spl4_118
| spl4_30
| ~ spl4_2
| ~ spl4_43
| ~ spl4_42
| spl4_113 ),
inference(avatar_split_clause,[],[f3230,f2646,f403,f407,f87,f312,f2850]) ).
fof(f3245,plain,
( $false
| ~ spl4_32 ),
inference(resolution,[],[f325,f60]) ).
fof(f3247,plain,
~ spl4_32,
inference(avatar_contradiction_clause,[],[f3245]) ).
fof(f3287,plain,
( ~ greater(growth_rate(efficient_producers,sK1(sK2)),growth_rate(first_movers,sK1(sK2)))
| greater_or_equal(sK1(sK2),sK0(sK2))
| ~ spl4_13
| spl4_26 ),
inference(resolution,[],[f296,f185]) ).
fof(f3381,plain,
( greater(growth_rate(first_movers,sK3(equilibrium(sK2))),zero)
| ~ spl4_12
| ~ spl4_20 ),
inference(superposition,[],[f271,f168]) ).
fof(f3384,plain,
( spl4_89
| ~ spl4_12
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f3381,f270,f166,f1628]) ).
fof(f3387,plain,
( spl4_80
| ~ spl4_12
| ~ spl4_38 ),
inference(avatar_split_clause,[],[f1432,f385,f166,f1493]) ).
fof(f3406,plain,
( ~ spl4_84
| ~ spl4_12
| spl4_21 ),
inference(avatar_split_clause,[],[f1420,f274,f166,f1510]) ).
fof(f3414,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ~ spl4_12
| ~ spl4_23 ),
inference(superposition,[],[f283,f168]) ).
fof(f3415,plain,
( greater(growth_rate(efficient_producers,sK1(sK2)),zero)
| ~ spl4_4
| ~ spl4_23 ),
inference(superposition,[],[f283,f108]) ).
fof(f3465,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(sK0(sK2)))
| zero = growth_rate(first_movers,sK3(sK0(sK2)))
| ~ greater(growth_rate(first_movers,sK3(sK0(sK2))),zero)
| spl4_7
| spl4_8
| ~ spl4_12 ),
inference(resolution,[],[f1418,f209]) ).
fof(f3475,plain,
( ~ spl4_16
| spl4_17
| spl4_18
| ~ spl4_2
| ~ spl4_19
| spl4_7
| spl4_8
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f3465,f166,f131,f119,f265,f87,f261,f257,f253]) ).
fof(f3477,plain,
( ~ spl4_42
| ~ spl4_9
| spl4_40 ),
inference(avatar_split_clause,[],[f2549,f394,f135,f403]) ).
fof(f3478,plain,
( ~ spl4_79
| spl4_28
| spl4_43 ),
inference(avatar_split_clause,[],[f417,f407,f304,f1384]) ).
fof(f3479,plain,
( spl4_76
| ~ spl4_75 ),
inference(avatar_split_clause,[],[f1555,f1348,f1357]) ).
fof(f3527,plain,
( outcompetes(efficient_producers,first_movers,sK0(sK2))
| ~ spl4_9
| ~ spl4_60 ),
inference(superposition,[],[f1255,f137]) ).
fof(f3541,plain,
( spl4_50
| ~ spl4_9
| ~ spl4_60 ),
inference(avatar_split_clause,[],[f3527,f1254,f135,f1195]) ).
fof(f3665,plain,
( spl4_27
| ~ spl4_4
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f3415,f282,f106,f299]) ).
fof(f3668,plain,
( ~ spl4_30
| ~ spl4_9
| spl4_26 ),
inference(avatar_split_clause,[],[f2540,f295,f135,f312]) ).
fof(f3669,plain,
( spl4_34
| ~ spl4_35
| ~ spl4_13
| spl4_26 ),
inference(avatar_split_clause,[],[f3287,f295,f184,f339,f335]) ).
fof(f3670,plain,
( ~ spl4_125
| spl4_5
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f1413,f166,f110,f3185]) ).
fof(f3671,plain,
( ~ spl4_117
| spl4_3
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f1411,f166,f95,f2844]) ).
fof(f3672,plain,
( ~ spl4_87
| ~ spl4_12
| spl4_76 ),
inference(avatar_split_clause,[],[f1477,f1357,f166,f1584]) ).
fof(f3680,plain,
( ~ spl4_31
| spl4_28
| spl4_33 ),
inference(avatar_split_clause,[],[f351,f327,f304,f316]) ).
fof(f3684,plain,
( spl4_90
| ~ spl4_12
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f3414,f282,f166,f1632]) ).
fof(f3701,plain,
( sK0(sK2) = equilibrium(sK2)
| ~ spl4_9
| ~ spl4_12 ),
inference(superposition,[],[f137,f168]) ).
fof(f3727,plain,
( spl4_114
| ~ spl4_9
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f3701,f166,f135,f2651]) ).
fof(f3756,plain,
( ~ greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| spl4_75
| ~ spl4_114 ),
inference(superposition,[],[f1349,f2653]) ).
fof(f3809,plain,
( ~ greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(equilibrium(sK2)))
| zero = growth_rate(first_movers,sK3(equilibrium(sK2)))
| ~ greater(growth_rate(first_movers,sK3(equilibrium(sK2))),zero)
| spl4_125 ),
inference(resolution,[],[f3187,f209]) ).
fof(f3816,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(equilibrium(sK2))))
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(equilibrium(sK2)))
| zero = growth_rate(efficient_producers,sK3(equilibrium(sK2)))
| ~ greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| spl4_125 ),
inference(resolution,[],[f3187,f244]) ).
fof(f3872,plain,
( ~ greater(growth_rate(first_movers,sK3(sK1(sK2))),zero)
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(sK1(sK2)))
| zero = growth_rate(first_movers,sK3(sK1(sK2)))
| spl4_75
| ~ spl4_114 ),
inference(resolution,[],[f3756,f65]) ).
fof(f3884,plain,
( spl4_21
| spl4_22
| ~ spl4_2
| ~ spl4_23
| ~ spl4_20
| spl4_75
| ~ spl4_114 ),
inference(avatar_split_clause,[],[f3872,f2651,f1348,f270,f282,f87,f278,f274]) ).
fof(f3916,plain,
( ~ environment(sK2)
| in_environment(sK2,equilibrium(sK2))
| ~ spl4_98 ),
inference(resolution,[],[f2047,f78]) ).
fof(f3917,plain,
( spl4_117
| ~ spl4_2
| ~ spl4_98 ),
inference(avatar_split_clause,[],[f3916,f2046,f87,f2844]) ).
fof(f3922,plain,
( ~ spl4_89
| spl4_84
| spl4_82
| ~ spl4_2
| ~ spl4_90
| spl4_125 ),
inference(avatar_split_clause,[],[f3809,f3185,f1632,f87,f1501,f1510,f1628]) ).
fof(f3975,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| spl4_15
| ~ spl4_74 ),
inference(superposition,[],[f203,f1344]) ).
fof(f3977,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| spl4_15
| ~ spl4_21 ),
inference(superposition,[],[f203,f276]) ).
fof(f3978,plain,
( ~ spl4_23
| spl4_15
| ~ spl4_21 ),
inference(avatar_split_clause,[],[f3977,f274,f201,f282]) ).
fof(f3979,plain,
( ~ spl4_39
| spl4_15
| ~ spl4_74 ),
inference(avatar_split_clause,[],[f3975,f1342,f201,f389]) ).
fof(f3980,plain,
( ~ spl4_33
| ~ spl4_6
| spl4_14 ),
inference(avatar_split_clause,[],[f2788,f192,f115,f327]) ).
fof(f3981,plain,
( ~ spl4_43
| ~ spl4_6
| spl4_37 ),
inference(avatar_split_clause,[],[f3068,f380,f115,f407]) ).
fof(f3983,plain,
( spl4_32
| ~ spl4_33
| ~ spl4_13
| spl4_30 ),
inference(avatar_split_clause,[],[f2964,f312,f184,f327,f323]) ).
fof(f3987,plain,
( ~ spl4_80
| spl4_81
| spl4_82
| ~ spl4_2
| ~ spl4_83
| spl4_125 ),
inference(avatar_split_clause,[],[f3816,f3185,f1505,f87,f1501,f1497,f1493]) ).
fof(f3992,plain,
( ~ spl4_40
| spl4_120
| spl4_26
| ~ spl4_2
| ~ spl4_41 ),
inference(avatar_split_clause,[],[f1770,f398,f87,f295,f2990,f394]) ).
fof(f4039,plain,
( ~ greater(growth_rate(efficient_producers,sK1(sK2)),zero)
| ~ spl4_25
| spl4_35 ),
inference(superposition,[],[f341,f293]) ).
fof(f4043,plain,
( ~ spl4_27
| ~ spl4_25
| spl4_35 ),
inference(avatar_split_clause,[],[f4039,f339,f291,f299]) ).
fof(f4088,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(sK1(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK1(sK2)))
| ~ greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| spl4_5
| ~ spl4_11 ),
inference(resolution,[],[f170,f244]) ).
fof(f4090,plain,
( ~ spl4_38
| spl4_74
| spl4_22
| ~ spl4_2
| ~ spl4_39
| spl4_5
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f4088,f163,f110,f389,f87,f278,f1342,f385]) ).
fof(f4096,plain,
( ~ spl4_115
| spl4_8
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f172,f163,f131,f2655]) ).
fof(f4113,plain,
( ~ greater(growth_rate(efficient_producers,sK1(sK2)),growth_rate(first_movers,sK1(sK2)))
| ~ spl4_4
| spl4_15 ),
inference(superposition,[],[f203,f108]) ).
fof(f4133,plain,
( ~ spl4_35
| ~ spl4_4
| spl4_15 ),
inference(avatar_split_clause,[],[f4113,f201,f106,f339]) ).
fof(f4246,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(sK0(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK0(sK2)))
| ~ greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2))))
| spl4_7
| spl4_8
| ~ spl4_11 ),
inference(resolution,[],[f171,f244]) ).
fof(f4248,plain,
( ~ spl4_36
| spl4_111
| spl4_18
| ~ spl4_2
| ~ spl4_37
| spl4_7
| spl4_8
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f4246,f163,f131,f119,f380,f87,f261,f2514,f376]) ).
fof(f4250,plain,
( ~ spl4_37
| spl4_14
| ~ spl4_111 ),
inference(avatar_split_clause,[],[f3121,f2514,f192,f380]) ).
fof(f4390,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ environment(sK2)
| subpopulations(first_movers,efficient_producers,sK2,sK3(sK0(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK0(sK2)))
| ~ greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2))))
| spl4_7
| spl4_8
| ~ spl4_12 ),
inference(resolution,[],[f1418,f244]) ).
fof(f4392,plain,
( ~ spl4_36
| spl4_111
| spl4_18
| ~ spl4_2
| ~ spl4_37
| spl4_7
| spl4_8
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f4390,f166,f131,f119,f380,f87,f261,f2514,f376]) ).
cnf(s1,plain,
( ~ spl4_1
| ~ spl4_2 ),
inference(sat_conversion,[],[f90]) ).
cnf(s2,plain,
spl4_2,
inference(sat_conversion,[],[f92]) ).
cnf(s3,plain,
( ~ spl4_2
| ~ spl4_3 ),
inference(sat_conversion,[],[f98]) ).
cnf(s4,plain,
( spl4_3
| spl4_4
| ~ spl4_5 ),
inference(sat_conversion,[],[f113]) ).
cnf(s5,plain,
( spl4_1
| spl4_6
| ~ spl4_7 ),
inference(sat_conversion,[],[f122]) ).
cnf(s6,plain,
( spl4_1
| spl4_3
| ~ spl4_8
| spl4_9
| ~ spl4_10 ),
inference(sat_conversion,[],[f142]) ).
cnf(s7,plain,
( ~ spl4_2
| spl4_11
| spl4_12 ),
inference(sat_conversion,[],[f169]) ).
cnf(s8,plain,
( ~ spl4_2
| spl4_13 ),
inference(sat_conversion,[],[f186]) ).
cnf(s9,plain,
( spl4_1
| ~ spl4_13
| ~ spl4_14 ),
inference(sat_conversion,[],[f195]) ).
cnf(s10,plain,
( spl4_3
| spl4_5
| spl4_10
| ~ spl4_13
| ~ spl4_15 ),
inference(sat_conversion,[],[f204]) ).
cnf(s11,plain,
( ~ spl4_2
| spl4_7
| spl4_8
| ~ spl4_11
| ~ spl4_16
| spl4_17
| spl4_18
| ~ spl4_19 ),
inference(sat_conversion,[],[f268]) ).
cnf(s12,plain,
( ~ spl4_2
| spl4_5
| ~ spl4_11
| ~ spl4_20
| spl4_21
| spl4_22
| ~ spl4_23 ),
inference(sat_conversion,[],[f285]) ).
cnf(s25,plain,
( spl4_31
| spl4_43
| ~ spl4_50
| spl4_51 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s37,plain,
( spl4_23
| spl4_39
| ~ spl4_70
| spl4_71 ),
inference(sat_conversion,[],[f1327]) ).
cnf(s39,plain,
( spl4_3
| spl4_70 ),
inference(sat_conversion,[],[f1339]) ).
cnf(s40,plain,
( spl4_15
| spl4_20
| ~ spl4_23 ),
inference(sat_conversion,[],[f1340]) ).
cnf(s42,plain,
( spl4_15
| spl4_38
| ~ spl4_39 ),
inference(sat_conversion,[],[f1346]) ).
cnf(s55,plain,
( spl4_3
| ~ spl4_22 ),
inference(sat_conversion,[],[f1399]) ).
cnf(s57,plain,
( ~ spl4_2
| spl4_3
| ~ spl4_12
| ~ spl4_80
| spl4_81
| spl4_82
| ~ spl4_83 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s60,plain,
( spl4_3
| ~ spl4_13
| ~ spl4_15
| spl4_76 ),
inference(sat_conversion,[],[f1545]) ).
cnf(s66,plain,
( ~ spl4_2
| spl4_3
| ~ spl4_71 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s72,plain,
( spl4_83
| spl4_90
| ~ spl4_97
| spl4_98 ),
inference(sat_conversion,[],[f2048]) ).
cnf(s78,plain,
( spl4_19
| spl4_37
| ~ spl4_107
| spl4_108 ),
inference(sat_conversion,[],[f2492]) ).
cnf(s80,plain,
( spl4_1
| spl4_107 ),
inference(sat_conversion,[],[f2504]) ).
cnf(s81,plain,
( spl4_1
| ~ spl4_2
| ~ spl4_108 ),
inference(sat_conversion,[],[f2509]) ).
cnf(s83,plain,
( spl4_14
| spl4_16
| ~ spl4_19 ),
inference(sat_conversion,[],[f2511]) ).
cnf(s86,plain,
( spl4_14
| spl4_36
| ~ spl4_37 ),
inference(sat_conversion,[],[f2518]) ).
cnf(s96,plain,
( spl4_7
| ~ spl4_9
| ~ spl4_76 ),
inference(sat_conversion,[],[f2659]) ).
cnf(s105,plain,
( ~ spl4_9
| spl4_14
| ~ spl4_15 ),
inference(sat_conversion,[],[f2668]) ).
cnf(s107,plain,
( spl4_10
| ~ spl4_34 ),
inference(sat_conversion,[],[f2670]) ).
cnf(s109,plain,
( ~ spl4_4
| spl4_10
| ~ spl4_76 ),
inference(sat_conversion,[],[f2751]) ).
cnf(s112,plain,
( ~ spl4_4
| spl4_60
| ~ spl4_70 ),
inference(sat_conversion,[],[f2754]) ).
cnf(s115,plain,
( ~ spl4_4
| ~ spl4_39
| spl4_41 ),
inference(sat_conversion,[],[f2757]) ).
cnf(s119,plain,
( spl4_14
| ~ spl4_17
| ~ spl4_19 ),
inference(sat_conversion,[],[f2785]) ).
cnf(s120,plain,
( spl4_1
| ~ spl4_18 ),
inference(sat_conversion,[],[f2787]) ).
cnf(s123,plain,
( ~ spl4_6
| spl4_50
| ~ spl4_107 ),
inference(sat_conversion,[],[f2804]) ).
cnf(s131,plain,
( ~ spl4_6
| spl4_17
| ~ spl4_29 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s135,plain,
( ~ spl4_6
| ~ spl4_19
| spl4_31 ),
inference(sat_conversion,[],[f2832]) ).
cnf(s139,plain,
( ~ spl4_12
| ~ spl4_70
| spl4_97 ),
inference(sat_conversion,[],[f2835]) ).
cnf(s140,plain,
( spl4_80
| ~ spl4_83
| spl4_86 ),
inference(sat_conversion,[],[f2836]) ).
cnf(s143,plain,
( ~ spl4_12
| spl4_22
| ~ spl4_82 ),
inference(sat_conversion,[],[f2839]) ).
cnf(s146,plain,
( ~ spl4_12
| spl4_23
| ~ spl4_90 ),
inference(sat_conversion,[],[f2842]) ).
cnf(s147,plain,
( ~ spl4_13
| ~ spl4_86
| spl4_87
| spl4_117 ),
inference(sat_conversion,[],[f2847]) ).
cnf(s149,plain,
( ~ spl4_6
| spl4_18
| ~ spl4_30 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s152,plain,
( ~ spl4_12
| spl4_74
| ~ spl4_81 ),
inference(sat_conversion,[],[f2946]) ).
cnf(s161,plain,
( spl4_35
| spl4_40
| ~ spl4_41 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s164,plain,
( spl4_24
| ~ spl4_27
| spl4_35 ),
inference(sat_conversion,[],[f2988]) ).
cnf(s167,plain,
( ~ spl4_2
| ~ spl4_24
| spl4_25
| spl4_26
| ~ spl4_27 ),
inference(sat_conversion,[],[f2995]) ).
cnf(s174,plain,
( ~ spl4_19
| spl4_79
| ~ spl4_111 ),
inference(sat_conversion,[],[f3137]) ).
cnf(s176,plain,
( ~ spl4_2
| spl4_30
| ~ spl4_51 ),
inference(sat_conversion,[],[f3146]) ).
cnf(s179,plain,
( ~ spl4_2
| ~ spl4_28
| spl4_30
| ~ spl4_31
| spl4_113
| spl4_118 ),
inference(sat_conversion,[],[f3149]) ).
cnf(s180,plain,
( ~ spl4_2
| ~ spl4_28
| spl4_29
| spl4_30
| ~ spl4_31
| spl4_113 ),
inference(sat_conversion,[],[f3150]) ).
cnf(s181,plain,
( spl4_8
| ~ spl4_12
| ~ spl4_115 ),
inference(sat_conversion,[],[f3151]) ).
cnf(s185,plain,
( spl4_5
| ~ spl4_7
| ~ spl4_9 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s187,plain,
( ~ spl4_9
| spl4_27
| ~ spl4_31 ),
inference(sat_conversion,[],[f3160]) ).
cnf(s199,plain,
( spl4_5
| spl4_10
| ~ spl4_76 ),
inference(sat_conversion,[],[f3169]) ).
cnf(s200,plain,
( ~ spl4_4
| spl4_22
| ~ spl4_26 ),
inference(sat_conversion,[],[f3170]) ).
cnf(s223,plain,
( ~ spl4_4
| spl4_74
| ~ spl4_120 ),
inference(sat_conversion,[],[f3190]) ).
cnf(s226,plain,
( ~ spl4_6
| spl4_111
| ~ spl4_118 ),
inference(sat_conversion,[],[f3192]) ).
cnf(s235,plain,
( spl4_33
| spl4_42
| ~ spl4_43 ),
inference(sat_conversion,[],[f3199]) ).
cnf(s239,plain,
( ~ spl4_113
| spl4_115 ),
inference(sat_conversion,[],[f3222]) ).
cnf(s240,plain,
( ~ spl4_2
| spl4_30
| ~ spl4_42
| ~ spl4_43
| spl4_113
| spl4_118 ),
inference(sat_conversion,[],[f3232]) ).
cnf(s244,plain,
~ spl4_32,
inference(sat_conversion,[],[f3247]) ).
cnf(s264,plain,
( ~ spl4_12
| ~ spl4_20
| spl4_89 ),
inference(sat_conversion,[],[f3384]) ).
cnf(s270,plain,
( ~ spl4_12
| ~ spl4_38
| spl4_80 ),
inference(sat_conversion,[],[f3387]) ).
cnf(s278,plain,
( ~ spl4_12
| spl4_21
| ~ spl4_84 ),
inference(sat_conversion,[],[f3406]) ).
cnf(s293,plain,
( ~ spl4_2
| spl4_7
| spl4_8
| ~ spl4_12
| ~ spl4_16
| spl4_17
| spl4_18
| ~ spl4_19 ),
inference(sat_conversion,[],[f3475]) ).
cnf(s296,plain,
( ~ spl4_9
| spl4_40
| ~ spl4_42 ),
inference(sat_conversion,[],[f3477]) ).
cnf(s300,plain,
( spl4_28
| spl4_43
| ~ spl4_79 ),
inference(sat_conversion,[],[f3478]) ).
cnf(s301,plain,
( ~ spl4_75
| spl4_76 ),
inference(sat_conversion,[],[f3479]) ).
cnf(s312,plain,
( ~ spl4_9
| spl4_50
| ~ spl4_60 ),
inference(sat_conversion,[],[f3541]) ).
cnf(s330,plain,
( ~ spl4_4
| ~ spl4_23
| spl4_27 ),
inference(sat_conversion,[],[f3665]) ).
cnf(s336,plain,
( ~ spl4_9
| spl4_26
| ~ spl4_30 ),
inference(sat_conversion,[],[f3668]) ).
cnf(s337,plain,
( ~ spl4_13
| spl4_26
| spl4_34
| ~ spl4_35 ),
inference(sat_conversion,[],[f3669]) ).
cnf(s339,plain,
( spl4_5
| ~ spl4_12
| ~ spl4_125 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s340,plain,
( spl4_3
| ~ spl4_12
| ~ spl4_117 ),
inference(sat_conversion,[],[f3671]) ).
cnf(s342,plain,
( ~ spl4_12
| spl4_76
| ~ spl4_87 ),
inference(sat_conversion,[],[f3672]) ).
cnf(s356,plain,
( spl4_28
| ~ spl4_31
| spl4_33 ),
inference(sat_conversion,[],[f3680]) ).
cnf(s362,plain,
( ~ spl4_12
| ~ spl4_23
| spl4_90 ),
inference(sat_conversion,[],[f3684]) ).
cnf(s368,plain,
( ~ spl4_9
| ~ spl4_12
| spl4_114 ),
inference(sat_conversion,[],[f3727]) ).
cnf(s376,plain,
( ~ spl4_2
| ~ spl4_20
| spl4_21
| spl4_22
| ~ spl4_23
| spl4_75
| ~ spl4_114 ),
inference(sat_conversion,[],[f3884]) ).
cnf(s384,plain,
( ~ spl4_2
| ~ spl4_98
| spl4_117 ),
inference(sat_conversion,[],[f3917]) ).
cnf(s389,plain,
( ~ spl4_2
| spl4_82
| spl4_84
| ~ spl4_89
| ~ spl4_90
| spl4_125 ),
inference(sat_conversion,[],[f3922]) ).
cnf(s406,plain,
( spl4_15
| ~ spl4_21
| ~ spl4_23 ),
inference(sat_conversion,[],[f3978]) ).
cnf(s407,plain,
( spl4_15
| ~ spl4_39
| ~ spl4_74 ),
inference(sat_conversion,[],[f3979]) ).
cnf(s412,plain,
( ~ spl4_6
| spl4_14
| ~ spl4_33 ),
inference(sat_conversion,[],[f3980]) ).
cnf(s417,plain,
( ~ spl4_6
| spl4_37
| ~ spl4_43 ),
inference(sat_conversion,[],[f3981]) ).
cnf(s419,plain,
( ~ spl4_13
| spl4_30
| spl4_32
| ~ spl4_33 ),
inference(sat_conversion,[],[f3983]) ).
cnf(s425,plain,
( ~ spl4_2
| ~ spl4_80
| spl4_81
| spl4_82
| ~ spl4_83
| spl4_125 ),
inference(sat_conversion,[],[f3987]) ).
cnf(s430,plain,
( ~ spl4_2
| spl4_26
| ~ spl4_40
| ~ spl4_41
| spl4_120 ),
inference(sat_conversion,[],[f3992]) ).
cnf(s433,plain,
( ~ spl4_25
| ~ spl4_27
| spl4_35 ),
inference(sat_conversion,[],[f4043]) ).
cnf(s448,plain,
( ~ spl4_2
| spl4_5
| ~ spl4_11
| spl4_22
| ~ spl4_38
| ~ spl4_39
| spl4_74 ),
inference(sat_conversion,[],[f4090]) ).
cnf(s460,plain,
( spl4_8
| ~ spl4_11
| ~ spl4_115 ),
inference(sat_conversion,[],[f4096]) ).
cnf(s476,plain,
( ~ spl4_4
| spl4_15
| ~ spl4_35 ),
inference(sat_conversion,[],[f4133]) ).
cnf(s488,plain,
( ~ spl4_2
| spl4_7
| spl4_8
| ~ spl4_11
| spl4_18
| ~ spl4_36
| ~ spl4_37
| spl4_111 ),
inference(sat_conversion,[],[f4248]) ).
cnf(s490,plain,
( spl4_14
| ~ spl4_37
| ~ spl4_111 ),
inference(sat_conversion,[],[f4250]) ).
cnf(s526,plain,
( ~ spl4_2
| spl4_7
| spl4_8
| ~ spl4_12
| spl4_18
| ~ spl4_36
| ~ spl4_37
| spl4_111 ),
inference(sat_conversion,[],[f4392]) ).
cnf(s537,plain,
spl4_13,
inference(rat,[],[s8,s2]) ).
cnf(s538,plain,
~ spl4_3,
inference(rat,[],[s3,s2]) ).
cnf(s539,plain,
~ spl4_71,
inference(rat,[],[s66,s2,s538]) ).
cnf(s540,plain,
~ spl4_22,
inference(rat,[],[s55,s538]) ).
cnf(s541,plain,
spl4_70,
inference(rat,[],[s39,s538]) ).
cnf(s542,plain,
~ spl4_1,
inference(rat,[],[s1,s2]) ).
cnf(s543,plain,
~ spl4_18,
inference(rat,[],[s120,s542]) ).
cnf(s544,plain,
~ spl4_108,
inference(rat,[],[s81,s2,s542]) ).
cnf(s545,plain,
spl4_107,
inference(rat,[],[s80,s542]) ).
cnf(s546,plain,
~ spl4_14,
inference(rat,[],[s9,s537,s542]) ).
cnf(s547,plain,
( ~ spl4_37
| ~ spl4_12
| spl4_8
| spl4_7 ),
inference(rat,[],[s526,s86,s490,s2,s543,s546]) ).
cnf(s548,plain,
( ~ spl4_12
| spl4_8
| spl4_7 ),
inference(rat,[],[s293,s83,s119,s78,s547,s544,s545,s546,s543,s2]) ).
cnf(s549,plain,
( ~ spl4_37
| spl4_8
| spl4_7 ),
inference(rat,[],[s488,s86,s490,s7,s548,s2,s543,s546]) ).
cnf(s550,plain,
( spl4_8
| spl4_7 ),
inference(rat,[],[s11,s83,s119,s78,s549,s7,s548,s544,s545,s546,s543,s2]) ).
cnf(s551,plain,
( spl4_23
| spl4_86
| spl4_15
| spl4_125
| ~ spl4_12 ),
inference(rat,[],[s425,s152,s140,s407,s72,s37,s146,s143,s139,s384,s340,s2,s541,s539,s538,s540]) ).
cnf(s552,plain,
( spl4_10
| ~ spl4_12
| spl4_5 ),
inference(rat,[],[s389,s264,s278,s40,s406,s362,s551,s147,s342,s10,s199,s340,s143,s339,s2,s537,s538,s540]) ).
cnf(s553,plain,
( ~ spl4_12
| spl4_7
| spl4_5 ),
inference(rat,[],[s406,s376,s40,s551,s147,s342,s301,s368,s96,s105,s6,s552,s339,s340,s550,s2,s540,s537,s546,s538,s542]) ).
cnf(s554,plain,
( ~ spl4_39
| spl4_15
| ~ spl4_11
| spl4_5 ),
inference(rat,[],[s448,s42,s407,s2,s540]) ).
cnf(s555,plain,
( spl4_15
| ~ spl4_11
| spl4_5 ),
inference(rat,[],[s12,s40,s406,s37,s554,s539,s541,s540,s2]) ).
cnf(s556,plain,
( spl4_7
| spl4_5 ),
inference(rat,[],[s6,s10,s105,s555,s7,s553,s550,s538,s542,s537,s546,s2]) ).
cnf(s557,plain,
( spl4_23
| spl4_15
| ~ spl4_12 ),
inference(rat,[],[s57,s270,s152,s42,s407,s72,s37,s146,s143,s139,s384,s340,s2,s538,s541,s539,s540]) ).
cnf(s559,plain,
( ~ spl4_43
| spl4_118
| spl4_113
| ~ spl4_6 ),
inference(rat,[],[s240,s235,s412,s149,s2,s543,s546]) ).
cnf(s560,plain,
( spl4_118
| spl4_113
| ~ spl4_6 ),
inference(rat,[],[s179,s356,s25,s559,s412,s123,s176,s149,s2,s543,s545,s546]) ).
cnf(s561,plain,
( spl4_113
| ~ spl4_6 ),
inference(rat,[],[s180,s131,s300,s174,s135,s119,s417,s78,s490,s226,s560,s149,s2,s546,s545,s544,s543]) ).
cnf(s562,plain,
( ~ spl4_12
| spl4_5 ),
inference(rat,[],[s6,s181,s552,s185,s239,s561,s5,s556,s538,s542]) ).
cnf(s563,plain,
spl4_5,
inference(rat,[],[s10,s6,s555,s460,s7,s562,s239,s561,s185,s5,s556,s538,s537,s542,s2]) ).
cnf(s564,plain,
spl4_4,
inference(rat,[],[s4,s538,s563]) ).
cnf(s565,plain,
~ spl4_26,
inference(rat,[],[s200,s540,s564]) ).
cnf(s566,plain,
spl4_60,
inference(rat,[],[s112,s541,s564]) ).
cnf(s567,plain,
( spl4_8
| ~ spl4_12 ),
inference(rat,[],[s561,s239,s5,s181,s550,s542]) ).
cnf(s568,plain,
( ~ spl4_27
| spl4_35 ),
inference(rat,[],[s167,s433,s164,s565,s2]) ).
cnf(s569,plain,
( spl4_10
| ~ spl4_12 ),
inference(rat,[],[s568,s330,s557,s337,s60,s107,s109,s564,s537,s565,s538]) ).
cnf(s570,plain,
( spl4_15
| ~ spl4_12 ),
inference(rat,[],[s568,s330,s476,s557,s564]) ).
cnf(s571,plain,
~ spl4_12,
inference(rat,[],[s570,s105,s6,s569,s567,s546,s538,s542]) ).
cnf(s573,plain,
spl4_11,
inference(rat,[],[s7,s2,s571]) ).
cnf(s574,plain,
spl4_8,
inference(rat,[],[s561,s239,s5,s460,s550,s542,s573]) ).
cnf(s575,plain,
spl4_10,
inference(rat,[],[s430,s223,s161,s407,s115,s37,s330,s568,s337,s60,s107,s109,s2,s565,s564,s541,s539,s537,s538]) ).
cnf(s577,plain,
spl4_9,
inference(rat,[],[s6,s574,s542,s538,s575]) ).
cnf(s579,plain,
~ spl4_15,
inference(rat,[],[s105,s546,s577]) ).
cnf(s584,plain,
~ spl4_30,
inference(rat,[],[s336,s565,s577]) ).
cnf(s585,plain,
spl4_50,
inference(rat,[],[s312,s566,s577]) ).
cnf(s588,plain,
~ spl4_35,
inference(rat,[],[s476,s564,s579]) ).
cnf(s592,plain,
~ spl4_33,
inference(rat,[],[s419,s537,s244,s584]) ).
cnf(s593,plain,
~ spl4_51,
inference(rat,[],[s176,s2,s584]) ).
cnf(s594,plain,
~ spl4_27,
inference(rat,[],[s568,s588]) ).
cnf(s596,plain,
~ spl4_31,
inference(rat,[],[s187,s577,s594]) ).
cnf(s597,plain,
~ spl4_23,
inference(rat,[],[s330,s564,s594]) ).
cnf(s600,plain,
spl4_43,
inference(rat,[],[s25,s593,s585,s596]) ).
cnf(s602,plain,
spl4_39,
inference(rat,[],[s37,s539,s541,s597]) ).
cnf(s605,plain,
spl4_42,
inference(rat,[],[s235,s592,s600]) ).
cnf(s607,plain,
spl4_41,
inference(rat,[],[s115,s564,s602]) ).
cnf(s608,plain,
~ spl4_74,
inference(rat,[],[s407,s579,s602]) ).
cnf(s611,plain,
spl4_40,
inference(rat,[],[s296,s577,s605]) ).
cnf(s614,plain,
~ spl4_120,
inference(rat,[],[s223,s564,s608]) ).
cnf(s618,plain,
$false,
inference(rat,[],[s430,s607,s565,s2,s614,s611]) ).
fof(f4394,plain,
$false,
inference(avatar_sat_refutation,[],[s618]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 17:23:41 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.39 Running first-order model finding
% 0.14/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.49 % (807063)Will run a generic schedule for satisfiability detection.
% 0.42/0.49 % (807074)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=355969668:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.42/0.49 % (807069)% WARNING: option uhcvi not known.
% 0.42/0.49 % (807068)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3465934133_2999 on theBenchmark for (2999ds/0Mi)
% 0.42/0.49 % (807070)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=799695402:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.42/0.49 % (807071)dis+10_1_sil=32000:sp=arity:random_seed=2563564066:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.42/0.49 % (807072)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2471113590:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.42/0.49 % (807073)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3600768239:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.42/0.49 % (807069)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=543940780:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.42/0.49 % TRYING [1]
% 0.42/0.49 % TRYING [2]
% 0.42/0.49 % TRYING [3]
% 0.42/0.49 % (807074) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-807063-807074"...
% 0.42/0.49 % (807073) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-807063-807073"...
% 0.42/0.49 % (807074)...printing done.
% 0.42/0.49 % (807074)Refutation found. Thanks to Tanya!
% 0.42/0.49 % SZS status Theorem for theBenchmark
% 0.42/0.49 % SZS output start Proof for theBenchmark
% See solution above
% 0.42/0.49 % (807074)------------------------------
% 0.42/0.49 % (807074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.49 % (807074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.49 % (807074)CaDiCaL version: 2.1.3
% 0.42/0.49 % (807074)Termination reason: Refutation
% 0.42/0.49 % (807074)Time elapsed: 0.056 s
% 0.42/0.49 % (807074)Peak memory usage: 13 MB
% 0.42/0.49 % (807074)Instructions burned: 162 (million)
% 0.42/0.49 % (807063)Success in time 0.086 s
% 0.42/0.49 % Vampire exiting
%------------------------------------------------------------------------------