%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MGT035-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:37 PM UTC 2026
% Result : Unsatisfiable 0.54s 0.57s
% Output : Refutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 85
% Syntax : Number of formulae : 533 ( 37 unt; 65 def)
% Number of atoms : 1671 ( 103 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1924 ( 786 ~;1073 |; 0 &)
% ( 65 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 74 ( 72 usr; 66 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 137 ( 0 sgn 137 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ greater(X0,X1)
| ~ greater(X1,X2)
| greater(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_transitivity_22) ).
fof(f2,axiom,
! [X2,X0,X1] :
( ~ 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_23) ).
fof(f3,plain,
! [X2,X0,X1] :
( ~ in_environment(X0,X1)
| ~ in_environment(X0,X2)
| greater(X2,X1)
| X1 = X2
| greater(X1,X2) ),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X0,X1] :
( ~ greater_or_equal(X0,X1)
| greater(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_24) ).
fof(f5,axiom,
! [X0,X1] :
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_25) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_26) ).
fof(f7,axiom,
! [X2,X3,X0,X1] :
( ~ 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_27) ).
fof(f10,axiom,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| growth_rate(first_movers,X1) = zero
| greater(growth_rate(first_movers,X1),zero)
| greater(growth_rate(efficient_producers,X1),zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_30) ).
fof(f11,plain,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(first_movers,X1)
| greater(growth_rate(first_movers,X1),zero)
| greater(growth_rate(efficient_producers,X1),zero) ),
inference(reorient_equations,[],[f10]) ).
fof(f12,axiom,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| growth_rate(first_movers,X1) = zero
| greater(growth_rate(first_movers,X1),zero)
| greater(zero,growth_rate(first_movers,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_31) ).
fof(f13,plain,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(first_movers,X1)
| greater(growth_rate(first_movers,X1),zero)
| greater(zero,growth_rate(first_movers,X1)) ),
inference(reorient_equations,[],[f12]) ).
fof(f16,axiom,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| growth_rate(first_movers,X1) = zero
| greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_33) ).
fof(f17,plain,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(first_movers,X1)
| greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1)) ),
inference(reorient_equations,[],[f16]) ).
fof(f20,axiom,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| growth_rate(efficient_producers,X1) = zero
| greater(growth_rate(first_movers,X1),zero)
| greater(zero,growth_rate(first_movers,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_35) ).
fof(f21,plain,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(efficient_producers,X1)
| greater(growth_rate(first_movers,X1),zero)
| greater(zero,growth_rate(first_movers,X1)) ),
inference(reorient_equations,[],[f20]) ).
fof(f24,axiom,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| growth_rate(efficient_producers,X1) = zero
| greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_37) ).
fof(f25,plain,
! [X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(efficient_producers,X1)
| greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1)) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,axiom,
! [X0] :
( ~ environment(X0)
| ~ stable(X0)
| in_environment(X0,sk1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_38) ).
fof(f27,axiom,
! [X0,X1] :
( ~ environment(X0)
| ~ stable(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,sk1(X0))
| greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_39) ).
fof(f28,axiom,
! [X0] :
( ~ environment(X0)
| ~ stable(X0)
| in_environment(X0,sk2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_40) ).
fof(f29,axiom,
! [X0] :
( ~ environment(X0)
| ~ stable(X0)
| greater_or_equal(sk2(X0),equilibrium(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_41) ).
fof(f30,negated_conjecture,
environment(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_42) ).
fof(f31,negated_conjecture,
stable(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_43) ).
fof(f32,negated_conjecture,
! [X0] :
( ~ in_environment(sk3,X0)
| subpopulations(first_movers,efficient_producers,sk3,sk4(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_44) ).
fof(f33,negated_conjecture,
! [X0] :
( ~ in_environment(sk3,X0)
| greater_or_equal(sk4(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_45) ).
fof(f34,negated_conjecture,
! [X0] :
( ~ in_environment(sk3,X0)
| ~ outcompetes(efficient_producers,first_movers,sk4(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_46) ).
fof(f35,plain,
! [X1] : greater_or_equal(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f36,plain,
! [X2,X0,X1] :
( greater(X1,X2)
| greater(X0,X1)
| ~ greater(X0,X2) ),
inference(consistent_polarity_flipping,[],[f1]) ).
fof(f37,plain,
! [X2,X0,X1] :
( in_environment(X0,X2)
| in_environment(X0,X1)
| ~ greater(X2,X1)
| X1 = X2
| ~ greater(X1,X2) ),
inference(consistent_polarity_flipping,[],[f3]) ).
fof(f38,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f4]) ).
fof(f39,plain,
! [X0,X1] :
( ~ greater_or_equal(X0,X1)
| greater(X0,X1) ),
inference(consistent_polarity_flipping,[],[f5]) ).
fof(f40,plain,
! [X1] : ~ greater_or_equal(X1,X1),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f41,plain,
! [X2,X3,X0,X1] :
( greater_or_equal(growth_rate(X2,X3),zero)
| ~ subpopulations(X1,X2,X0,X3)
| environment(X0)
| greater(zero,growth_rate(X1,X3))
| outcompetes(X2,X1,X3) ),
inference(consistent_polarity_flipping,[],[f7]) ).
fof(f44,plain,
! [X0,X1] :
( environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(first_movers,X1)
| ~ greater(growth_rate(first_movers,X1),zero)
| ~ greater(growth_rate(efficient_producers,X1),zero) ),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f45,plain,
! [X0,X1] :
( environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(first_movers,X1)
| ~ greater(growth_rate(first_movers,X1),zero)
| ~ greater(zero,growth_rate(first_movers,X1)) ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f47,plain,
! [X0,X1] :
( environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(first_movers,X1)
| ~ greater(zero,growth_rate(efficient_producers,X1))
| ~ greater(zero,growth_rate(first_movers,X1)) ),
inference(consistent_polarity_flipping,[],[f17]) ).
fof(f49,plain,
! [X0,X1] :
( environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(efficient_producers,X1)
| ~ greater(growth_rate(first_movers,X1),zero)
| ~ greater(zero,growth_rate(first_movers,X1)) ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f51,plain,
! [X0,X1] :
( environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| greater_or_equal(X1,equilibrium(X0))
| zero = growth_rate(efficient_producers,X1)
| ~ greater(zero,growth_rate(efficient_producers,X1))
| ~ greater(zero,growth_rate(first_movers,X1)) ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f52,plain,
! [X0] :
( environment(X0)
| ~ stable(X0)
| ~ in_environment(X0,sk1(X0)) ),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f53,plain,
! [X0,X1] :
( environment(X0)
| ~ stable(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| greater_or_equal(X1,sk1(X0))
| ~ greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)) ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f54,plain,
! [X0] :
( environment(X0)
| ~ stable(X0)
| ~ in_environment(X0,sk2(X0)) ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f55,plain,
! [X0] :
( ~ greater_or_equal(sk2(X0),equilibrium(X0))
| ~ stable(X0)
| environment(X0) ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f56,plain,
~ environment(sk3),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f57,plain,
! [X0] :
( subpopulations(first_movers,efficient_producers,sk3,sk4(X0))
| in_environment(sk3,X0) ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f58,plain,
! [X0] :
( ~ greater_or_equal(sk4(X0),X0)
| in_environment(sk3,X0) ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f59,plain,
! [X0] :
( ~ outcompetes(efficient_producers,first_movers,sk4(X0))
| in_environment(sk3,X0) ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f60,plain,
( ~ stable(sk3)
| ~ in_environment(sk3,sk1(sk3)) ),
inference(resolution,[],[f52,f56]) ).
fof(f62,definition,
( spl0_1
<=> in_environment(sk3,sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f64,plain,
( ~ in_environment(sk3,sk1(sk3))
| spl0_1 ),
inference(avatar_component_clause,[],[f62]) ).
fof(f66,definition,
( spl0_2
<=> stable(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f68,plain,
( ~ stable(sk3)
| spl0_2 ),
inference(avatar_component_clause,[],[f66]) ).
fof(f69,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f60,f66,f62]) ).
fof(f70,plain,
( $false
| spl0_2 ),
inference(resolution,[],[f68,f31]) ).
fof(f71,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f70]) ).
fof(f72,plain,
( ~ stable(sk3)
| ~ in_environment(sk3,sk2(sk3)) ),
inference(resolution,[],[f54,f56]) ).
fof(f74,definition,
( spl0_3
<=> in_environment(sk3,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f76,plain,
( ~ in_environment(sk3,sk2(sk3))
| spl0_3 ),
inference(avatar_component_clause,[],[f74]) ).
fof(f77,plain,
( ~ spl0_3
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f72,f66,f74]) ).
fof(f78,plain,
! [X0] :
( in_environment(sk3,X0)
| sk4(X0) = X0
| ~ greater(sk4(X0),X0) ),
inference(resolution,[],[f38,f58]) ).
fof(f81,plain,
! [X0] :
( ~ greater(sk2(X0),equilibrium(X0))
| equilibrium(X0) = sk2(X0)
| ~ stable(X0)
| environment(X0) ),
inference(resolution,[],[f38,f55]) ).
fof(f82,plain,
( sk1(sk3) = sk4(sk1(sk3))
| ~ greater(sk4(sk1(sk3)),sk1(sk3))
| spl0_1 ),
inference(resolution,[],[f78,f64]) ).
fof(f83,plain,
( sk2(sk3) = sk4(sk2(sk3))
| ~ greater(sk4(sk2(sk3)),sk2(sk3))
| spl0_3 ),
inference(resolution,[],[f78,f76]) ).
fof(f85,definition,
( spl0_4
<=> greater(sk4(sk2(sk3)),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f87,plain,
( ~ greater(sk4(sk2(sk3)),sk2(sk3))
| spl0_4 ),
inference(avatar_component_clause,[],[f85]) ).
fof(f89,definition,
( spl0_5
<=> sk2(sk3) = sk4(sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f91,plain,
( sk2(sk3) = sk4(sk2(sk3))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f92,plain,
( ~ spl0_4
| spl0_5
| spl0_3 ),
inference(avatar_split_clause,[],[f83,f74,f89,f85]) ).
fof(f94,definition,
( spl0_6
<=> greater(sk4(sk1(sk3)),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f96,plain,
( ~ greater(sk4(sk1(sk3)),sk1(sk3))
| spl0_6 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f98,definition,
( spl0_7
<=> sk1(sk3) = sk4(sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f100,plain,
( sk1(sk3) = sk4(sk1(sk3))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f98]) ).
fof(f101,plain,
( ~ spl0_6
| spl0_7
| spl0_1 ),
inference(avatar_split_clause,[],[f82,f62,f98,f94]) ).
fof(f103,plain,
( ! [X0] :
( in_environment(sk3,X0)
| ~ greater(sk1(sk3),X0)
| sk1(sk3) = X0
| ~ greater(X0,sk1(sk3)) )
| spl0_1 ),
inference(resolution,[],[f37,f64]) ).
fof(f107,plain,
( ~ greater(sk1(sk3),sk2(sk3))
| sk1(sk3) = sk2(sk3)
| ~ greater(sk2(sk3),sk1(sk3))
| spl0_1
| spl0_3 ),
inference(resolution,[],[f103,f76]) ).
fof(f110,definition,
( spl0_8
<=> greater(sk2(sk3),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f111,plain,
( greater(sk2(sk3),sk1(sk3))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f112,plain,
( ~ greater(sk2(sk3),sk1(sk3))
| spl0_8 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f114,definition,
( spl0_9
<=> sk1(sk3) = sk2(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f115,plain,
( sk1(sk3) != sk2(sk3)
| spl0_9 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f116,plain,
( sk1(sk3) = sk2(sk3)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f118,definition,
( spl0_10
<=> greater(sk1(sk3),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f120,plain,
( ~ greater(sk1(sk3),sk2(sk3))
| spl0_10 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f121,plain,
( ~ spl0_8
| spl0_9
| ~ spl0_10
| spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f107,f74,f62,f118,f114,f110]) ).
fof(f122,plain,
( ! [X0] :
( greater(X0,sk2(sk3))
| ~ greater(X0,sk1(sk3)) )
| spl0_8 ),
inference(resolution,[],[f112,f36]) ).
fof(f123,plain,
( ! [X0] :
( greater(X0,sk1(sk3))
| ~ greater(X0,sk2(sk3)) )
| spl0_10 ),
inference(resolution,[],[f120,f36]) ).
fof(f124,plain,
( ~ greater(sk4(sk2(sk3)),sk1(sk3))
| spl0_4
| spl0_8 ),
inference(resolution,[],[f122,f87]) ).
fof(f128,plain,
( ~ greater(sk4(sk1(sk3)),sk2(sk3))
| spl0_6
| spl0_10 ),
inference(resolution,[],[f123,f96]) ).
fof(f141,plain,
! [X0,X1] :
( environment(X0)
| ~ stable(X0)
| equilibrium(X0) = sk2(X0)
| greater(X1,sk2(X0))
| ~ greater(X1,equilibrium(X0)) ),
inference(resolution,[],[f81,f36]) ).
fof(f144,plain,
! [X0] :
( ~ stable(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(X0,sk2(sk3))
| ~ greater(X0,equilibrium(sk3)) ),
inference(resolution,[],[f141,f56]) ).
fof(f146,definition,
( spl0_11
<=> ! [X0] :
( greater(X0,sk2(sk3))
| ~ greater(X0,equilibrium(sk3)) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f147,plain,
( ! [X0] :
( greater(X0,sk2(sk3))
| ~ greater(X0,equilibrium(sk3)) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f149,definition,
( spl0_12
<=> sk2(sk3) = equilibrium(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f151,plain,
( sk2(sk3) = equilibrium(sk3)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f152,plain,
( spl0_11
| spl0_12
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f144,f66,f149,f146]) ).
fof(f153,plain,
( ~ greater(sk4(sk2(sk3)),equilibrium(sk3))
| spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f147,f87]) ).
fof(f154,plain,
( ~ greater(sk4(sk1(sk3)),equilibrium(sk3))
| spl0_6
| spl0_10
| ~ spl0_11 ),
inference(resolution,[],[f147,f128]) ).
fof(f156,plain,
( ~ greater(sk1(sk3),equilibrium(sk3))
| spl0_10
| ~ spl0_11 ),
inference(resolution,[],[f147,f120]) ).
fof(f165,plain,
! [X0] :
( ~ stable(sk3)
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| greater_or_equal(X0,sk1(sk3))
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(resolution,[],[f53,f56]) ).
fof(f167,definition,
( spl0_13
<=> ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| greater_or_equal(X0,sk1(sk3)) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f168,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| greater_or_equal(X0,sk1(sk3)) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f169,plain,
( spl0_13
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f165,f66,f167]) ).
fof(f170,plain,
! [X2,X3,X0,X1] :
( greater(zero,growth_rate(X0,X3))
| environment(X2)
| ~ subpopulations(X0,X1,X2,X3)
| outcompetes(X1,X0,X3)
| greater(growth_rate(X1,X3),zero) ),
inference(resolution,[],[f41,f39]) ).
fof(f171,plain,
( ! [X0] :
( greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater(growth_rate(efficient_producers,sk4(X0)),growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0) )
| ~ spl0_13 ),
inference(resolution,[],[f168,f57]) ).
fof(f172,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| in_environment(sk3,sk1(sk3))
| in_environment(sk3,sk1(sk3))
| ~ spl0_13 ),
inference(resolution,[],[f171,f58]) ).
fof(f173,plain,
( ! [X0] :
( greater(sk4(X0),sk1(sk3))
| in_environment(sk3,X0)
| ~ greater(growth_rate(efficient_producers,sk4(X0)),growth_rate(first_movers,sk4(X0))) )
| ~ spl0_13 ),
inference(resolution,[],[f171,f39]) ).
fof(f174,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| in_environment(sk3,sk1(sk3))
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f172]) ).
fof(f176,definition,
( spl0_14
<=> greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f178,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_14 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f179,plain,
( spl0_1
| ~ spl0_14
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f174,f167,f176,f62]) ).
fof(f180,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ greater(X0,growth_rate(first_movers,sk4(sk1(sk3)))) )
| spl0_14 ),
inference(resolution,[],[f178,f36]) ).
fof(f184,definition,
( spl0_15
<=> greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f186,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_15 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f188,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ greater(X0,growth_rate(first_movers,sk4(sk2(sk3)))) )
| spl0_15 ),
inference(resolution,[],[f186,f36]) ).
fof(f189,plain,
! [X0] :
( ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| greater_or_equal(X0,equilibrium(sk3))
| zero = growth_rate(first_movers,X0)
| ~ greater(growth_rate(first_movers,X0),zero)
| ~ greater(growth_rate(efficient_producers,X0),zero) ),
inference(resolution,[],[f44,f56]) ).
fof(f190,plain,
! [X0] :
( greater_or_equal(sk4(X0),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(X0))
| ~ greater(growth_rate(first_movers,sk4(X0)),zero)
| ~ greater(growth_rate(efficient_producers,sk4(X0)),zero)
| in_environment(sk3,X0) ),
inference(resolution,[],[f189,f57]) ).
fof(f191,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| in_environment(sk3,equilibrium(sk3))
| in_environment(sk3,equilibrium(sk3)) ),
inference(resolution,[],[f190,f58]) ).
fof(f192,plain,
! [X0] :
( greater(sk4(X0),equilibrium(sk3))
| ~ greater(growth_rate(first_movers,sk4(X0)),zero)
| ~ greater(growth_rate(efficient_producers,sk4(X0)),zero)
| in_environment(sk3,X0)
| zero = growth_rate(first_movers,sk4(X0)) ),
inference(resolution,[],[f190,f39]) ).
fof(f193,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| in_environment(sk3,equilibrium(sk3)) ),
inference(duplicate_literal_removal,[],[f191]) ).
fof(f195,definition,
( spl0_16
<=> in_environment(sk3,equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f196,plain,
( ~ in_environment(sk3,equilibrium(sk3))
| spl0_16 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f199,definition,
( spl0_17
<=> greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f203,definition,
( spl0_18
<=> greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f207,definition,
( spl0_19
<=> zero = growth_rate(first_movers,sk4(equilibrium(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f210,plain,
( spl0_16
| ~ spl0_17
| ~ spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f193,f207,f203,f199,f195]) ).
fof(f216,definition,
( spl0_20
<=> greater(sk4(equilibrium(sk3)),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f218,plain,
( ~ greater(sk4(equilibrium(sk3)),equilibrium(sk3))
| spl0_20 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f227,plain,
! [X0] :
( ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| greater_or_equal(X0,equilibrium(sk3))
| zero = growth_rate(first_movers,X0)
| ~ greater(growth_rate(first_movers,X0),zero)
| ~ greater(zero,growth_rate(first_movers,X0)) ),
inference(resolution,[],[f45,f56]) ).
fof(f232,plain,
! [X0] :
( greater_or_equal(sk4(X0),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(X0))
| ~ greater(growth_rate(first_movers,sk4(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0) ),
inference(resolution,[],[f227,f57]) ).
fof(f234,plain,
! [X0] :
( greater(sk4(X0),equilibrium(sk3))
| ~ greater(growth_rate(first_movers,sk4(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0)
| zero = growth_rate(first_movers,sk4(X0)) ),
inference(resolution,[],[f232,f39]) ).
fof(f236,plain,
( ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| in_environment(sk3,sk2(sk3))
| zero = growth_rate(first_movers,sk4(sk2(sk3)))
| spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f192,f153]) ).
fof(f237,plain,
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| in_environment(sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| spl0_6
| spl0_10
| ~ spl0_11 ),
inference(resolution,[],[f192,f154]) ).
fof(f240,definition,
( spl0_22
<=> zero = growth_rate(first_movers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f241,plain,
( zero != growth_rate(first_movers,sk4(sk1(sk3)))
| spl0_22 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f242,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f244,definition,
( spl0_23
<=> greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f245,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f246,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| spl0_23 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f248,definition,
( spl0_24
<=> greater(growth_rate(first_movers,sk4(sk1(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f249,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f250,plain,
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| spl0_24 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,plain,
( spl0_22
| spl0_1
| ~ spl0_23
| ~ spl0_24
| spl0_6
| spl0_10
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f237,f146,f118,f94,f248,f244,f62,f240]) ).
fof(f253,definition,
( spl0_25
<=> zero = growth_rate(first_movers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f254,plain,
( zero != growth_rate(first_movers,sk4(sk2(sk3)))
| spl0_25 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f255,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f257,definition,
( spl0_26
<=> greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f258,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| spl0_26 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f261,definition,
( spl0_27
<=> greater(growth_rate(first_movers,sk4(sk2(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f262,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f263,plain,
( ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| spl0_27 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f264,plain,
( spl0_25
| spl0_3
| ~ spl0_26
| ~ spl0_27
| spl0_4
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f236,f146,f85,f261,f257,f74,f253]) ).
fof(f265,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ greater(X0,zero) )
| spl0_26 ),
inference(resolution,[],[f259,f36]) ).
fof(f266,plain,
( ! [X0] :
( greater(X0,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater(X0,zero) )
| spl0_27 ),
inference(resolution,[],[f263,f36]) ).
fof(f268,plain,
( ! [X0] :
( greater(X0,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater(X0,zero) )
| spl0_24 ),
inference(resolution,[],[f250,f36]) ).
fof(f269,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| spl0_15
| spl0_27 ),
inference(resolution,[],[f266,f186]) ).
fof(f271,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| spl0_14
| spl0_24 ),
inference(resolution,[],[f268,f178]) ).
fof(f278,plain,
( ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| in_environment(sk3,equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| spl0_20 ),
inference(resolution,[],[f234,f218]) ).
fof(f282,plain,
! [X0] :
( ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| greater_or_equal(X0,equilibrium(sk3))
| zero = growth_rate(first_movers,X0)
| ~ greater(zero,growth_rate(efficient_producers,X0))
| ~ greater(zero,growth_rate(first_movers,X0)) ),
inference(resolution,[],[f47,f56]) ).
fof(f283,plain,
! [X0] :
( greater_or_equal(sk4(X0),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(X0))
| ~ greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0) ),
inference(resolution,[],[f282,f57]) ).
fof(f284,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| in_environment(sk3,equilibrium(sk3))
| in_environment(sk3,equilibrium(sk3)) ),
inference(resolution,[],[f283,f58]) ).
fof(f285,plain,
! [X0] :
( greater(sk4(X0),equilibrium(sk3))
| ~ greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0)
| zero = growth_rate(first_movers,sk4(X0)) ),
inference(resolution,[],[f283,f39]) ).
fof(f286,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| in_environment(sk3,equilibrium(sk3)) ),
inference(duplicate_literal_removal,[],[f284]) ).
fof(f288,definition,
( spl0_28
<=> greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f292,definition,
( spl0_29
<=> greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f295,plain,
( spl0_16
| ~ spl0_28
| ~ spl0_29
| spl0_19 ),
inference(avatar_split_clause,[],[f286,f207,f292,f288,f195]) ).
fof(f358,plain,
! [X0] :
( ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| greater_or_equal(X0,equilibrium(sk3))
| zero = growth_rate(efficient_producers,X0)
| ~ greater(growth_rate(first_movers,X0),zero)
| ~ greater(zero,growth_rate(first_movers,X0)) ),
inference(resolution,[],[f49,f56]) ).
fof(f380,plain,
! [X0] :
( greater_or_equal(sk4(X0),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk4(X0))
| ~ greater(growth_rate(first_movers,sk4(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0) ),
inference(resolution,[],[f358,f57]) ).
fof(f384,plain,
( zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| in_environment(sk3,equilibrium(sk3))
| in_environment(sk3,equilibrium(sk3)) ),
inference(resolution,[],[f380,f58]) ).
fof(f385,plain,
! [X0] :
( greater(sk4(X0),equilibrium(sk3))
| ~ greater(growth_rate(first_movers,sk4(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0)
| zero = growth_rate(efficient_producers,sk4(X0)) ),
inference(resolution,[],[f380,f39]) ).
fof(f386,plain,
( zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| in_environment(sk3,equilibrium(sk3)) ),
inference(duplicate_literal_removal,[],[f384]) ).
fof(f387,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| in_environment(sk3,sk2(sk3))
| zero = growth_rate(first_movers,sk4(sk2(sk3)))
| spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f285,f153]) ).
fof(f391,definition,
( spl0_34
<=> greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f392,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f393,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_34 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f395,definition,
( spl0_35
<=> greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f396,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f397,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| spl0_35 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f400,definition,
( spl0_36
<=> greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f401,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f402,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_36 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f404,definition,
( spl0_37
<=> greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f405,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f406,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| spl0_37 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f407,plain,
( spl0_25
| spl0_3
| ~ spl0_36
| ~ spl0_37
| spl0_4
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f387,f146,f85,f404,f400,f74,f253]) ).
fof(f409,plain,
( ! [X0,X1] :
( greater(growth_rate(X1,sk4(sk2(sk3))),zero)
| ~ subpopulations(first_movers,X1,X0,sk4(sk2(sk3)))
| outcompetes(X1,first_movers,sk4(sk2(sk3)))
| environment(X0) )
| spl0_36 ),
inference(resolution,[],[f402,f170]) ).
fof(f420,plain,
( ~ greater(zero,zero)
| spl0_26
| spl0_37 ),
inference(resolution,[],[f406,f265]) ).
fof(f421,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_15
| spl0_37 ),
inference(resolution,[],[f406,f188]) ).
fof(f423,plain,
( ! [X0,X1] :
( greater(growth_rate(X1,sk4(sk1(sk3))),zero)
| ~ subpopulations(first_movers,X1,X0,sk4(sk1(sk3)))
| outcompetes(X1,first_movers,sk4(sk1(sk3)))
| environment(X0) )
| spl0_34 ),
inference(resolution,[],[f393,f170]) ).
fof(f432,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_14
| spl0_35 ),
inference(resolution,[],[f397,f180]) ).
fof(f486,plain,
! [X0] :
( ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| greater_or_equal(X0,equilibrium(sk3))
| zero = growth_rate(efficient_producers,X0)
| ~ greater(zero,growth_rate(efficient_producers,X0))
| ~ greater(zero,growth_rate(first_movers,X0)) ),
inference(resolution,[],[f51,f56]) ).
fof(f570,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk2(sk3)))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| environment(X0) )
| spl0_26
| spl0_36 ),
inference(resolution,[],[f409,f259]) ).
fof(f581,definition,
( spl0_40
<=> outcompetes(efficient_producers,first_movers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f583,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f585,definition,
( spl0_41
<=> ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk2(sk3)))
| environment(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f586,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk2(sk3)))
| environment(X0) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f587,plain,
( spl0_40
| spl0_41
| spl0_26
| spl0_36 ),
inference(avatar_split_clause,[],[f570,f400,f257,f585,f581]) ).
fof(f606,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| in_environment(sk3,sk2(sk3))
| ~ spl0_5 ),
inference(superposition,[],[f57,f91]) ).
fof(f608,plain,
( ~ outcompetes(efficient_producers,first_movers,sk2(sk3))
| in_environment(sk3,sk2(sk3))
| ~ spl0_5 ),
inference(superposition,[],[f59,f91]) ).
fof(f610,plain,
( greater(sk2(sk3),sk1(sk3))
| in_environment(sk3,sk2(sk3))
| ~ greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ~ spl0_5
| ~ spl0_13 ),
inference(superposition,[],[f173,f91]) ).
fof(f622,definition,
( spl0_42
<=> greater(zero,growth_rate(first_movers,sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f624,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| spl0_42 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f626,definition,
( spl0_43
<=> greater(growth_rate(first_movers,sk2(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f627,plain,
( greater(growth_rate(first_movers,sk2(sk3)),zero)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f628,plain,
( ~ greater(growth_rate(first_movers,sk2(sk3)),zero)
| spl0_43 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f630,definition,
( spl0_44
<=> zero = growth_rate(efficient_producers,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f632,plain,
( zero = growth_rate(efficient_producers,sk2(sk3))
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f630]) ).
fof(f634,definition,
( spl0_45
<=> greater_or_equal(sk2(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f635,plain,
( ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| spl0_45 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f636,plain,
( greater_or_equal(sk2(sk3),equilibrium(sk3))
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f639,definition,
( spl0_46
<=> greater(growth_rate(efficient_producers,sk2(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f641,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| spl0_46 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f644,definition,
( spl0_47
<=> zero = growth_rate(first_movers,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f646,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f648,definition,
( spl0_48
<=> greater(zero,growth_rate(efficient_producers,sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f650,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| spl0_48 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f652,definition,
( spl0_49
<=> greater(sk2(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f653,plain,
( ~ greater(sk2(sk3),equilibrium(sk3))
| spl0_49 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f664,definition,
( spl0_50
<=> greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f666,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| spl0_50 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f667,plain,
( ~ spl0_50
| spl0_3
| spl0_8
| ~ spl0_5
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f610,f167,f89,f110,f74,f664]) ).
fof(f669,definition,
( spl0_51
<=> greater_or_equal(sk2(sk3),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f671,plain,
( greater_or_equal(sk2(sk3),sk1(sk3))
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f674,definition,
( spl0_52
<=> outcompetes(efficient_producers,first_movers,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f677,plain,
( spl0_3
| ~ spl0_52
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f608,f89,f674,f74]) ).
fof(f679,definition,
( spl0_53
<=> subpopulations(first_movers,efficient_producers,sk3,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f681,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f682,plain,
( spl0_3
| spl0_53
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f606,f89,f679,f74]) ).
fof(f692,plain,
( ! [X0,X1] :
( greater(growth_rate(X1,sk2(sk3)),zero)
| ~ subpopulations(first_movers,X1,X0,sk2(sk3))
| outcompetes(X1,first_movers,sk2(sk3))
| environment(X0) )
| spl0_42 ),
inference(resolution,[],[f624,f170]) ).
fof(f700,plain,
( ! [X0] :
( greater(X0,growth_rate(first_movers,sk2(sk3)))
| ~ greater(X0,zero) )
| spl0_43 ),
inference(resolution,[],[f628,f36]) ).
fof(f708,plain,
! [X0] :
( greater_or_equal(sk4(X0),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk4(X0))
| ~ greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0) ),
inference(resolution,[],[f486,f57]) ).
fof(f720,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| spl0_15
| ~ spl0_25 ),
inference(superposition,[],[f186,f255]) ).
fof(f736,definition,
( spl0_56
<=> greater(zero,zero) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f740,plain,
( ~ spl0_26
| spl0_15
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f720,f253,f184,f257]) ).
fof(f741,plain,
( ~ spl0_26
| spl0_15
| spl0_27 ),
inference(avatar_split_clause,[],[f269,f261,f184,f257]) ).
fof(f742,plain,
( ~ spl0_36
| spl0_15
| spl0_37 ),
inference(avatar_split_clause,[],[f421,f404,f184,f400]) ).
fof(f753,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_9
| spl0_37 ),
inference(superposition,[],[f406,f116]) ).
fof(f771,definition,
( spl0_57
<=> environment(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f773,plain,
( environment(sk3)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f781,plain,
( ~ greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_9
| spl0_49 ),
inference(superposition,[],[f653,f116]) ).
fof(f798,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sk2(sk3)))
| ~ greater(X0,growth_rate(first_movers,sk2(sk3))) )
| spl0_50 ),
inference(resolution,[],[f666,f36]) ).
fof(f805,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| spl0_43
| spl0_50 ),
inference(resolution,[],[f700,f666]) ).
fof(f824,plain,
! [X0] :
( greater(sk4(X0),equilibrium(sk3))
| ~ greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| in_environment(sk3,X0)
| zero = growth_rate(efficient_producers,sk4(X0)) ),
inference(resolution,[],[f708,f39]) ).
fof(f870,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| spl0_48
| spl0_50 ),
inference(resolution,[],[f798,f650]) ).
fof(f949,plain,
( ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| in_environment(sk3,equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| spl0_20 ),
inference(resolution,[],[f385,f218]) ).
fof(f983,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk2(sk3))
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| environment(X0) )
| spl0_42
| spl0_46 ),
inference(resolution,[],[f692,f641]) ).
fof(f985,definition,
( spl0_59
<=> ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk2(sk3))
| environment(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f986,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk2(sk3))
| environment(X0) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f987,plain,
( spl0_52
| spl0_59
| spl0_42
| spl0_46 ),
inference(avatar_split_clause,[],[f983,f639,f622,f985,f674]) ).
fof(f1026,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk1(sk3)))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| environment(X0) )
| spl0_23
| spl0_34 ),
inference(resolution,[],[f423,f246]) ).
fof(f1037,definition,
( spl0_70
<=> outcompetes(efficient_producers,first_movers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f1039,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1041,definition,
( spl0_71
<=> ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk1(sk3)))
| environment(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f1042,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk1(sk3)))
| environment(X0) )
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f1041]) ).
fof(f1043,plain,
( spl0_70
| spl0_71
| spl0_23
| spl0_34 ),
inference(avatar_split_clause,[],[f1026,f391,f244,f1041,f1037]) ).
fof(f1044,plain,
( in_environment(sk3,sk1(sk3))
| ~ spl0_70 ),
inference(resolution,[],[f1039,f59]) ).
fof(f1045,plain,
( spl0_1
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f1044,f1037,f62]) ).
fof(f1046,plain,
( environment(sk3)
| in_environment(sk3,sk1(sk3))
| ~ spl0_71 ),
inference(resolution,[],[f1042,f57]) ).
fof(f1047,plain,
( spl0_1
| spl0_57
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1046,f1041,f771,f62]) ).
fof(f1048,plain,
( ~ spl0_23
| spl0_14
| spl0_24 ),
inference(avatar_split_clause,[],[f271,f248,f176,f244]) ).
fof(f1049,plain,
( $false
| ~ spl0_57 ),
inference(resolution,[],[f773,f56]) ).
fof(f1050,plain,
~ spl0_57,
inference(avatar_contradiction_clause,[],[f1049]) ).
fof(f1051,plain,
( ~ spl0_34
| spl0_14
| spl0_35 ),
inference(avatar_split_clause,[],[f432,f395,f176,f391]) ).
fof(f1052,plain,
( ~ spl0_35
| ~ spl0_9
| spl0_37 ),
inference(avatar_split_clause,[],[f753,f404,f114,f395]) ).
fof(f1063,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| spl0_14
| ~ spl0_22 ),
inference(superposition,[],[f178,f242]) ).
fof(f1085,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| in_environment(sk3,sk2(sk3))
| zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f824,f153]) ).
fof(f1094,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| ~ spl0_7
| spl0_14 ),
inference(superposition,[],[f178,f100]) ).
fof(f1103,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_7
| ~ spl0_34 ),
inference(superposition,[],[f392,f100]) ).
fof(f1117,plain,
( greater(sk1(sk3),equilibrium(sk3))
| ~ greater(growth_rate(first_movers,sk1(sk3)),zero)
| ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| in_environment(sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| ~ spl0_7 ),
inference(superposition,[],[f192,f100]) ).
fof(f1131,plain,
( greater(sk1(sk3),equilibrium(sk3))
| ~ greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| in_environment(sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| ~ spl0_7 ),
inference(superposition,[],[f824,f100]) ).
fof(f1133,definition,
( spl0_74
<=> zero = growth_rate(efficient_producers,sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f1135,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1137,definition,
( spl0_75
<=> greater(zero,growth_rate(first_movers,sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f1141,definition,
( spl0_76
<=> greater(zero,growth_rate(efficient_producers,sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f1145,definition,
( spl0_77
<=> greater(sk1(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f1147,plain,
( greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f1145]) ).
fof(f1148,plain,
( spl0_74
| spl0_1
| ~ spl0_75
| ~ spl0_76
| spl0_77
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1131,f98,f1145,f1141,f1137,f62,f1133]) ).
fof(f1150,definition,
( spl0_78
<=> greater(growth_rate(efficient_producers,sk1(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f1157,definition,
( spl0_79
<=> greater(growth_rate(first_movers,sk1(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f1165,definition,
( spl0_80
<=> zero = growth_rate(first_movers,sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f1174,plain,
( spl0_80
| spl0_1
| ~ spl0_78
| ~ spl0_79
| spl0_77
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1117,f98,f1145,f1157,f1150,f62,f1165]) ).
fof(f1177,definition,
( spl0_81
<=> greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f1179,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| spl0_81 ),
inference(avatar_component_clause,[],[f1177]) ).
fof(f1186,definition,
( spl0_83
<=> greater_or_equal(sk1(sk3),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f1188,plain,
( greater_or_equal(sk1(sk3),sk1(sk3))
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f1186]) ).
fof(f1201,plain,
( spl0_75
| ~ spl0_7
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1103,f391,f98,f1137]) ).
fof(f1204,plain,
( ~ spl0_81
| ~ spl0_7
| spl0_14 ),
inference(avatar_split_clause,[],[f1094,f176,f98,f1177]) ).
fof(f1241,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| in_environment(sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| spl0_6
| spl0_10
| ~ spl0_11 ),
inference(resolution,[],[f154,f824]) ).
fof(f1244,definition,
( spl0_86
<=> zero = growth_rate(efficient_producers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f1246,plain,
( zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f1244]) ).
fof(f1247,plain,
( spl0_86
| spl0_1
| ~ spl0_34
| ~ spl0_35
| spl0_6
| spl0_10
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1241,f146,f118,f94,f395,f391,f62,f1244]) ).
fof(f1249,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_14
| ~ spl0_86 ),
inference(superposition,[],[f178,f1246]) ).
fof(f1260,plain,
( ~ spl0_34
| spl0_14
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f1249,f1244,f176,f391]) ).
fof(f1261,plain,
( ~ spl0_23
| spl0_14
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1063,f240,f176,f244]) ).
fof(f1265,plain,
( greater(growth_rate(first_movers,sk1(sk3)),zero)
| ~ spl0_7
| ~ spl0_24 ),
inference(superposition,[],[f249,f100]) ).
fof(f1266,plain,
( greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| ~ spl0_7
| ~ spl0_35 ),
inference(superposition,[],[f396,f100]) ).
fof(f1291,plain,
( spl0_76
| ~ spl0_7
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f1266,f395,f98,f1141]) ).
fof(f1292,plain,
( spl0_79
| ~ spl0_7
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f1265,f248,f98,f1157]) ).
fof(f1304,plain,
( zero != growth_rate(first_movers,sk1(sk3))
| ~ spl0_7
| spl0_22 ),
inference(superposition,[],[f241,f100]) ).
fof(f1306,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_7
| ~ spl0_23 ),
inference(superposition,[],[f245,f100]) ).
fof(f1307,plain,
( spl0_78
| ~ spl0_7
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f1306,f244,f98,f1150]) ).
fof(f1308,plain,
( ~ spl0_80
| ~ spl0_7
| spl0_22 ),
inference(avatar_split_clause,[],[f1304,f240,f98,f1165]) ).
fof(f1310,plain,
( $false
| spl0_10
| ~ spl0_11
| ~ spl0_77 ),
inference(resolution,[],[f1147,f156]) ).
fof(f1311,plain,
( spl0_10
| ~ spl0_11
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f1310]) ).
fof(f1315,definition,
( spl0_88
<=> zero = growth_rate(efficient_producers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f1316,plain,
( zero != growth_rate(efficient_producers,sk4(sk2(sk3)))
| spl0_88 ),
inference(avatar_component_clause,[],[f1315]) ).
fof(f1317,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f1315]) ).
fof(f1318,plain,
( spl0_88
| spl0_3
| ~ spl0_36
| ~ spl0_37
| spl0_4
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1085,f146,f85,f404,f400,f74,f1315]) ).
fof(f1325,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_74
| spl0_81 ),
inference(superposition,[],[f1179,f1135]) ).
fof(f1335,plain,
( ~ greater(zero,zero)
| ~ spl0_25
| spl0_27 ),
inference(superposition,[],[f263,f255]) ).
fof(f1336,plain,
( greater(zero,zero)
| ~ spl0_25
| ~ spl0_36 ),
inference(superposition,[],[f401,f255]) ).
fof(f1346,plain,
( ~ spl0_56
| ~ spl0_25
| spl0_27 ),
inference(avatar_split_clause,[],[f1335,f261,f253,f736]) ).
fof(f1354,plain,
( ~ greater(zero,zero)
| spl0_26
| ~ spl0_88 ),
inference(superposition,[],[f259,f1317]) ).
fof(f1361,plain,
( ~ spl0_56
| spl0_26
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f1354,f1315,f257,f736]) ).
fof(f1389,plain,
( greater_or_equal(sk2(sk3),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk2(sk3))
| ~ greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| in_environment(sk3,sk2(sk3))
| ~ spl0_5 ),
inference(superposition,[],[f708,f91]) ).
fof(f1398,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_44
| spl0_50 ),
inference(superposition,[],[f666,f632]) ).
fof(f1411,plain,
( ~ spl0_42
| ~ spl0_44
| spl0_50 ),
inference(avatar_split_clause,[],[f1398,f664,f630,f622]) ).
fof(f1414,plain,
( spl0_3
| ~ spl0_42
| ~ spl0_48
| spl0_44
| spl0_45
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1389,f89,f634,f630,f648,f622,f74]) ).
fof(f1416,plain,
( ~ stable(sk3)
| environment(sk3)
| ~ spl0_45 ),
inference(resolution,[],[f636,f55]) ).
fof(f1418,plain,
( spl0_57
| ~ spl0_2
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1416,f634,f66,f771]) ).
fof(f1419,plain,
( ~ spl0_46
| spl0_43
| spl0_50 ),
inference(avatar_split_clause,[],[f805,f664,f626,f639]) ).
fof(f1420,plain,
( ~ spl0_42
| spl0_48
| spl0_50 ),
inference(avatar_split_clause,[],[f870,f664,f648,f622]) ).
fof(f1423,plain,
( ~ spl0_75
| ~ spl0_74
| spl0_81 ),
inference(avatar_split_clause,[],[f1325,f1177,f1133,f1137]) ).
fof(f1426,plain,
( ~ greater(sk2(sk3),equilibrium(sk3))
| sk2(sk3) = equilibrium(sk3)
| spl0_45 ),
inference(resolution,[],[f635,f38]) ).
fof(f1427,plain,
( spl0_12
| ~ spl0_49
| spl0_45 ),
inference(avatar_split_clause,[],[f1426,f634,f652,f149]) ).
fof(f1437,plain,
( greater_or_equal(sk2(sk3),equilibrium(sk3))
| zero = growth_rate(first_movers,sk2(sk3))
| ~ greater(growth_rate(first_movers,sk2(sk3)),zero)
| ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_53 ),
inference(resolution,[],[f681,f189]) ).
fof(f1447,plain,
( environment(sk3)
| ~ spl0_53
| ~ spl0_59 ),
inference(resolution,[],[f681,f986]) ).
fof(f1448,plain,
( spl0_57
| ~ spl0_53
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f1447,f985,f679,f771]) ).
fof(f1465,plain,
( ~ spl0_56
| spl0_26
| spl0_37 ),
inference(avatar_split_clause,[],[f420,f404,f257,f736]) ).
fof(f1469,plain,
( greater(zero,zero)
| ~ spl0_43
| ~ spl0_47 ),
inference(superposition,[],[f627,f646]) ).
fof(f1470,plain,
( ~ greater(zero,zero)
| spl0_42
| ~ spl0_47 ),
inference(superposition,[],[f624,f646]) ).
fof(f1477,plain,
( ~ spl0_56
| spl0_42
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1470,f644,f622,f736]) ).
fof(f1478,plain,
( ~ spl0_46
| ~ spl0_43
| spl0_47
| spl0_45
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f1437,f679,f634,f644,f626,f639]) ).
fof(f1488,plain,
( ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| in_environment(sk3,sk2(sk3))
| zero = growth_rate(first_movers,sk4(sk2(sk3)))
| spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f153,f234]) ).
fof(f1516,plain,
( environment(sk3)
| in_environment(sk3,sk2(sk3))
| ~ spl0_41 ),
inference(resolution,[],[f586,f57]) ).
fof(f1517,plain,
( spl0_3
| spl0_57
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f1516,f585,f771,f74]) ).
fof(f1518,plain,
( in_environment(sk3,sk2(sk3))
| ~ spl0_40 ),
inference(resolution,[],[f583,f59]) ).
fof(f1519,plain,
( spl0_3
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1518,f581,f74]) ).
fof(f1521,plain,
( ~ spl0_77
| ~ spl0_9
| spl0_49 ),
inference(avatar_split_clause,[],[f781,f652,f114,f1145]) ).
fof(f1560,definition,
( spl0_94
<=> sk1(sk3) = equilibrium(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f1562,plain,
( sk1(sk3) = equilibrium(sk3)
| ~ spl0_94 ),
inference(avatar_component_clause,[],[f1560]) ).
fof(f1566,plain,
( ~ in_environment(sk3,equilibrium(sk3))
| spl0_3
| ~ spl0_12 ),
inference(superposition,[],[f76,f151]) ).
fof(f1567,plain,
( ~ greater(sk4(equilibrium(sk3)),equilibrium(sk3))
| spl0_4
| ~ spl0_12 ),
inference(superposition,[],[f87,f151]) ).
fof(f1569,plain,
( greater(equilibrium(sk3),sk1(sk3))
| ~ spl0_8
| ~ spl0_12 ),
inference(superposition,[],[f111,f151]) ).
fof(f1570,plain,
( sk1(sk3) = equilibrium(sk3)
| ~ spl0_9
| ~ spl0_12 ),
inference(superposition,[],[f116,f151]) ).
fof(f1574,plain,
( zero != growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ spl0_12
| spl0_25 ),
inference(superposition,[],[f254,f151]) ).
fof(f1588,plain,
( zero != growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| ~ spl0_12
| spl0_88 ),
inference(superposition,[],[f1316,f151]) ).
fof(f1592,plain,
( ~ spl0_16
| spl0_3
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1566,f149,f74,f195]) ).
fof(f1593,plain,
( ~ spl0_19
| ~ spl0_12
| spl0_25 ),
inference(avatar_split_clause,[],[f1574,f253,f149,f207]) ).
fof(f1595,definition,
( spl0_95
<=> zero = growth_rate(efficient_producers,sk4(equilibrium(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f1601,plain,
( spl0_19
| spl0_16
| ~ spl0_28
| ~ spl0_18
| spl0_20 ),
inference(avatar_split_clause,[],[f278,f216,f203,f288,f195,f207]) ).
fof(f1602,plain,
( spl0_16
| ~ spl0_28
| ~ spl0_18
| spl0_95 ),
inference(avatar_split_clause,[],[f386,f1595,f203,f288,f195]) ).
fof(f1603,plain,
( spl0_95
| spl0_16
| ~ spl0_28
| ~ spl0_18
| spl0_20 ),
inference(avatar_split_clause,[],[f949,f216,f203,f288,f195,f1595]) ).
fof(f1606,plain,
( ~ greater(sk1(sk3),equilibrium(sk3))
| sk1(sk3) = equilibrium(sk3)
| ~ greater(equilibrium(sk3),sk1(sk3))
| spl0_1
| spl0_16 ),
inference(resolution,[],[f196,f103]) ).
fof(f1621,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ spl0_24
| ~ spl0_94 ),
inference(superposition,[],[f249,f1562]) ).
fof(f1639,plain,
( spl0_18
| ~ spl0_24
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f1621,f1560,f248,f203]) ).
fof(f1679,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_12
| ~ spl0_26 ),
inference(superposition,[],[f258,f151]) ).
fof(f1680,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_9
| ~ spl0_26 ),
inference(superposition,[],[f258,f116]) ).
fof(f1681,plain,
( spl0_17
| ~ spl0_12
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1679,f257,f149,f199]) ).
fof(f1682,plain,
( spl0_94
| ~ spl0_9
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1570,f149,f114,f1560]) ).
fof(f1684,definition,
( spl0_98
<=> greater(equilibrium(sk3),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f1703,plain,
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| ~ spl0_9
| spl0_27 ),
inference(superposition,[],[f263,f116]) ).
fof(f1704,plain,
( ~ spl0_24
| ~ spl0_9
| spl0_27 ),
inference(avatar_split_clause,[],[f1703,f261,f114,f248]) ).
fof(f1708,plain,
( spl0_25
| spl0_3
| ~ spl0_36
| ~ spl0_27
| spl0_4
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1488,f146,f85,f261,f400,f74,f253]) ).
fof(f1709,plain,
( spl0_56
| ~ spl0_25
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f1336,f400,f253,f736]) ).
fof(f1710,plain,
( spl0_56
| ~ spl0_43
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1469,f644,f626,f736]) ).
fof(f1714,plain,
( greater_or_equal(sk1(sk3),sk1(sk3))
| ~ spl0_9
| ~ spl0_51 ),
inference(superposition,[],[f671,f116]) ).
fof(f1715,plain,
( spl0_83
| ~ spl0_9
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f1714,f669,f114,f1186]) ).
fof(f1716,plain,
( $false
| ~ spl0_83 ),
inference(resolution,[],[f1188,f40]) ).
fof(f1718,plain,
~ spl0_83,
inference(avatar_contradiction_clause,[],[f1716]) ).
fof(f1754,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| ~ spl0_9
| ~ spl0_25 ),
inference(superposition,[],[f255,f116]) ).
fof(f1757,plain,
( spl0_22
| ~ spl0_9
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1754,f253,f114,f240]) ).
fof(f1758,plain,
( spl0_23
| ~ spl0_9
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1680,f257,f114,f244]) ).
fof(f1759,plain,
( spl0_98
| ~ spl0_8
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1569,f149,f110,f1684]) ).
fof(f1843,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_12
| ~ spl0_36 ),
inference(superposition,[],[f401,f151]) ).
fof(f1845,plain,
( spl0_28
| ~ spl0_12
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f1843,f400,f149,f288]) ).
fof(f1846,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_12
| ~ spl0_37 ),
inference(superposition,[],[f405,f151]) ).
fof(f1848,plain,
( spl0_29
| ~ spl0_12
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f1846,f404,f149,f292]) ).
fof(f1856,plain,
( sk1(sk3) != equilibrium(sk3)
| spl0_9
| ~ spl0_12 ),
inference(superposition,[],[f115,f151]) ).
fof(f1861,plain,
( in_environment(sk3,sk2(sk3))
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_4
| spl0_8
| ~ spl0_13 ),
inference(resolution,[],[f124,f173]) ).
fof(f1865,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ spl0_12
| ~ spl0_27 ),
inference(superposition,[],[f262,f151]) ).
fof(f1866,plain,
( spl0_18
| ~ spl0_12
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1865,f261,f149,f203]) ).
fof(f1867,plain,
( ~ spl0_98
| spl0_94
| ~ spl0_77
| spl0_1
| spl0_16 ),
inference(avatar_split_clause,[],[f1606,f195,f62,f1145,f1560,f1684]) ).
fof(f1871,plain,
( ~ greater(sk1(sk3),equilibrium(sk3))
| spl0_10
| ~ spl0_12 ),
inference(superposition,[],[f120,f151]) ).
fof(f1911,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| greater_or_equal(sk2(sk3),sk1(sk3))
| ~ spl0_13
| ~ spl0_53 ),
inference(resolution,[],[f681,f168]) ).
fof(f1968,plain,
( ~ greater(sk4(sk1(sk3)),equilibrium(sk3))
| spl0_6
| spl0_10
| ~ spl0_12 ),
inference(superposition,[],[f128,f151]) ).
fof(f1994,plain,
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| in_environment(sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| spl0_6
| spl0_10
| ~ spl0_12 ),
inference(resolution,[],[f1968,f192]) ).
fof(f2001,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| in_environment(sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| spl0_6
| spl0_10
| ~ spl0_12 ),
inference(resolution,[],[f1968,f824]) ).
fof(f2004,plain,
( spl0_22
| spl0_1
| ~ spl0_23
| ~ spl0_24
| spl0_6
| spl0_10
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1994,f149,f118,f94,f248,f244,f62,f240]) ).
fof(f2005,plain,
( spl0_86
| spl0_1
| ~ spl0_34
| ~ spl0_35
| spl0_6
| spl0_10
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f2001,f149,f118,f94,f395,f391,f62,f1244]) ).
fof(f2009,plain,
( ~ spl0_94
| spl0_9
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1856,f149,f114,f1560]) ).
fof(f2010,plain,
( ~ spl0_77
| spl0_10
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1871,f149,f118,f1145]) ).
fof(f2014,plain,
( ~ spl0_20
| spl0_4
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1567,f149,f85,f216]) ).
fof(f2016,plain,
( ~ spl0_15
| spl0_3
| spl0_4
| spl0_8
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1861,f167,f110,f85,f74,f184]) ).
fof(f2024,plain,
( ~ spl0_95
| ~ spl0_12
| spl0_88 ),
inference(avatar_split_clause,[],[f1588,f1315,f149,f1595]) ).
fof(f2026,plain,
( spl0_51
| ~ spl0_50
| ~ spl0_13
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f1911,f679,f167,f664,f669]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f69]) ).
cnf(s2,plain,
spl0_2,
inference(sat_conversion,[],[f71]) ).
cnf(s3,plain,
( ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f77]) ).
cnf(s4,plain,
( spl0_3
| ~ spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f92]) ).
cnf(s5,plain,
( spl0_1
| ~ spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f101]) ).
cnf(s6,plain,
( spl0_1
| spl0_3
| ~ spl0_8
| spl0_9
| ~ spl0_10 ),
inference(sat_conversion,[],[f121]) ).
cnf(s7,plain,
( ~ spl0_2
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f152]) ).
cnf(s8,plain,
( ~ spl0_2
| spl0_13 ),
inference(sat_conversion,[],[f169]) ).
cnf(s9,plain,
( spl0_1
| ~ spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f179]) ).
cnf(s11,plain,
( spl0_16
| ~ spl0_17
| ~ spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f210]) ).
cnf(s13,plain,
( spl0_1
| spl0_6
| spl0_10
| ~ spl0_11
| spl0_22
| ~ spl0_23
| ~ spl0_24 ),
inference(sat_conversion,[],[f251]) ).
cnf(s14,plain,
( spl0_3
| spl0_4
| ~ spl0_11
| spl0_25
| ~ spl0_26
| ~ spl0_27 ),
inference(sat_conversion,[],[f264]) ).
cnf(s15,plain,
( spl0_16
| spl0_19
| ~ spl0_28
| ~ spl0_29 ),
inference(sat_conversion,[],[f295]) ).
cnf(s19,plain,
( spl0_3
| spl0_4
| ~ spl0_11
| spl0_25
| ~ spl0_36
| ~ spl0_37 ),
inference(sat_conversion,[],[f407]) ).
cnf(s21,plain,
( spl0_26
| spl0_36
| spl0_40
| spl0_41 ),
inference(sat_conversion,[],[f587]) ).
cnf(s32,plain,
( spl0_3
| ~ spl0_5
| spl0_8
| ~ spl0_13
| ~ spl0_50 ),
inference(sat_conversion,[],[f667]) ).
cnf(s34,plain,
( spl0_3
| ~ spl0_5
| ~ spl0_52 ),
inference(sat_conversion,[],[f677]) ).
cnf(s35,plain,
( spl0_3
| ~ spl0_5
| spl0_53 ),
inference(sat_conversion,[],[f682]) ).
cnf(s42,plain,
( spl0_15
| ~ spl0_25
| ~ spl0_26 ),
inference(sat_conversion,[],[f740]) ).
cnf(s43,plain,
( spl0_15
| ~ spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f741]) ).
cnf(s44,plain,
( spl0_15
| ~ spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f742]) ).
cnf(s49,plain,
( spl0_42
| spl0_46
| spl0_52
| spl0_59 ),
inference(sat_conversion,[],[f987]) ).
cnf(s55,plain,
( spl0_23
| spl0_34
| spl0_70
| spl0_71 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s56,plain,
( spl0_1
| ~ spl0_70 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s57,plain,
( spl0_1
| spl0_57
| ~ spl0_71 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s58,plain,
( spl0_14
| ~ spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s59,plain,
~ spl0_57,
inference(sat_conversion,[],[f1050]) ).
cnf(s60,plain,
( spl0_14
| ~ spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s61,plain,
( ~ spl0_9
| ~ spl0_35
| spl0_37 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s65,plain,
( spl0_1
| ~ spl0_7
| spl0_74
| ~ spl0_75
| ~ spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f1148]) ).
cnf(s79,plain,
( spl0_1
| ~ spl0_7
| spl0_77
| ~ spl0_78
| ~ spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f1174]) ).
cnf(s86,plain,
( ~ spl0_7
| ~ spl0_34
| spl0_75 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s89,plain,
( ~ spl0_7
| spl0_14
| ~ spl0_81 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s94,plain,
( spl0_1
| spl0_6
| spl0_10
| ~ spl0_11
| ~ spl0_34
| ~ spl0_35
| spl0_86 ),
inference(sat_conversion,[],[f1247]) ).
cnf(s98,plain,
( spl0_14
| ~ spl0_34
| ~ spl0_86 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s100,plain,
( spl0_14
| ~ spl0_22
| ~ spl0_23 ),
inference(sat_conversion,[],[f1261]) ).
cnf(s102,plain,
( ~ spl0_7
| ~ spl0_35
| spl0_76 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s103,plain,
( ~ spl0_7
| ~ spl0_24
| spl0_79 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s104,plain,
( ~ spl0_7
| ~ spl0_23
| spl0_78 ),
inference(sat_conversion,[],[f1307]) ).
cnf(s105,plain,
( ~ spl0_7
| spl0_22
| ~ spl0_80 ),
inference(sat_conversion,[],[f1308]) ).
cnf(s106,plain,
( spl0_10
| ~ spl0_11
| ~ spl0_77 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s111,plain,
( spl0_3
| spl0_4
| ~ spl0_11
| ~ spl0_36
| ~ spl0_37
| spl0_88 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s115,plain,
( ~ spl0_25
| spl0_27
| ~ spl0_56 ),
inference(sat_conversion,[],[f1346]) ).
cnf(s117,plain,
( spl0_26
| ~ spl0_56
| ~ spl0_88 ),
inference(sat_conversion,[],[f1361]) ).
cnf(s123,plain,
( ~ spl0_42
| ~ spl0_44
| spl0_50 ),
inference(sat_conversion,[],[f1411]) ).
cnf(s126,plain,
( spl0_3
| ~ spl0_5
| ~ spl0_42
| spl0_44
| spl0_45
| ~ spl0_48 ),
inference(sat_conversion,[],[f1414]) ).
cnf(s128,plain,
( ~ spl0_2
| ~ spl0_45
| spl0_57 ),
inference(sat_conversion,[],[f1418]) ).
cnf(s130,plain,
( spl0_43
| ~ spl0_46
| spl0_50 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s131,plain,
( ~ spl0_42
| spl0_48
| spl0_50 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s141,plain,
( ~ spl0_74
| ~ spl0_75
| spl0_81 ),
inference(sat_conversion,[],[f1423]) ).
cnf(s145,plain,
( spl0_12
| spl0_45
| ~ spl0_49 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s146,plain,
( ~ spl0_53
| spl0_57
| ~ spl0_59 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s159,plain,
( spl0_26
| spl0_37
| ~ spl0_56 ),
inference(sat_conversion,[],[f1465]) ).
cnf(s162,plain,
( spl0_42
| ~ spl0_47
| ~ spl0_56 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s163,plain,
( ~ spl0_43
| spl0_45
| ~ spl0_46
| spl0_47
| ~ spl0_53 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s165,plain,
( spl0_3
| ~ spl0_41
| spl0_57 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s166,plain,
( spl0_3
| ~ spl0_40 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s168,plain,
( ~ spl0_9
| spl0_49
| ~ spl0_77 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s185,plain,
( spl0_3
| ~ spl0_12
| ~ spl0_16 ),
inference(sat_conversion,[],[f1592]) ).
cnf(s186,plain,
( ~ spl0_12
| ~ spl0_19
| spl0_25 ),
inference(sat_conversion,[],[f1593]) ).
cnf(s190,plain,
( spl0_16
| ~ spl0_18
| spl0_19
| spl0_20
| ~ spl0_28 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s191,plain,
( spl0_16
| ~ spl0_18
| ~ spl0_28
| spl0_95 ),
inference(sat_conversion,[],[f1602]) ).
cnf(s192,plain,
( spl0_16
| ~ spl0_18
| spl0_20
| ~ spl0_28
| spl0_95 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s195,plain,
( spl0_18
| ~ spl0_24
| ~ spl0_94 ),
inference(sat_conversion,[],[f1639]) ).
cnf(s197,plain,
( ~ spl0_12
| spl0_17
| ~ spl0_26 ),
inference(sat_conversion,[],[f1681]) ).
cnf(s198,plain,
( ~ spl0_9
| ~ spl0_12
| spl0_94 ),
inference(sat_conversion,[],[f1682]) ).
cnf(s207,plain,
( ~ spl0_9
| ~ spl0_24
| spl0_27 ),
inference(sat_conversion,[],[f1704]) ).
cnf(s214,plain,
( spl0_3
| spl0_4
| ~ spl0_11
| spl0_25
| ~ spl0_27
| ~ spl0_36 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s217,plain,
( ~ spl0_25
| ~ spl0_36
| spl0_56 ),
inference(sat_conversion,[],[f1709]) ).
cnf(s222,plain,
( ~ spl0_43
| ~ spl0_47
| spl0_56 ),
inference(sat_conversion,[],[f1710]) ).
cnf(s225,plain,
( ~ spl0_9
| ~ spl0_51
| spl0_83 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s226,plain,
~ spl0_83,
inference(sat_conversion,[],[f1718]) ).
cnf(s229,plain,
( ~ spl0_9
| spl0_22
| ~ spl0_25 ),
inference(sat_conversion,[],[f1757]) ).
cnf(s232,plain,
( ~ spl0_9
| spl0_23
| ~ spl0_26 ),
inference(sat_conversion,[],[f1758]) ).
cnf(s234,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_98 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s247,plain,
( ~ spl0_12
| spl0_28
| ~ spl0_36 ),
inference(sat_conversion,[],[f1845]) ).
cnf(s248,plain,
( ~ spl0_12
| spl0_29
| ~ spl0_37 ),
inference(sat_conversion,[],[f1848]) ).
cnf(s255,plain,
( ~ spl0_12
| spl0_18
| ~ spl0_27 ),
inference(sat_conversion,[],[f1866]) ).
cnf(s258,plain,
( spl0_1
| spl0_16
| ~ spl0_77
| spl0_94
| ~ spl0_98 ),
inference(sat_conversion,[],[f1867]) ).
cnf(s265,plain,
( spl0_1
| spl0_6
| spl0_10
| ~ spl0_12
| spl0_22
| ~ spl0_23
| ~ spl0_24 ),
inference(sat_conversion,[],[f2004]) ).
cnf(s266,plain,
( spl0_1
| spl0_6
| spl0_10
| ~ spl0_12
| ~ spl0_34
| ~ spl0_35
| spl0_86 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s276,plain,
( spl0_9
| ~ spl0_12
| ~ spl0_94 ),
inference(sat_conversion,[],[f2009]) ).
cnf(s277,plain,
( spl0_10
| ~ spl0_12
| ~ spl0_77 ),
inference(sat_conversion,[],[f2010]) ).
cnf(s281,plain,
( spl0_4
| ~ spl0_12
| ~ spl0_20 ),
inference(sat_conversion,[],[f2014]) ).
cnf(s284,plain,
( spl0_3
| spl0_4
| spl0_8
| ~ spl0_13
| ~ spl0_15 ),
inference(sat_conversion,[],[f2016]) ).
cnf(s291,plain,
( ~ spl0_12
| spl0_88
| ~ spl0_95 ),
inference(sat_conversion,[],[f2024]) ).
cnf(s294,plain,
( ~ spl0_13
| ~ spl0_50
| spl0_51
| ~ spl0_53 ),
inference(sat_conversion,[],[f2026]) ).
cnf(s303,plain,
( ~ spl0_9
| ~ spl0_51 ),
inference(rat,[],[s225,s226]) ).
cnf(s307,plain,
( spl0_1
| ~ spl0_71 ),
inference(rat,[],[s57,s59]) ).
cnf(s310,plain,
~ spl0_45,
inference(rat,[],[s128,s59,s2]) ).
cnf(s311,plain,
spl0_13,
inference(rat,[],[s8,s2]) ).
cnf(s312,plain,
~ spl0_3,
inference(rat,[],[s3,s2]) ).
cnf(s313,plain,
~ spl0_40,
inference(rat,[],[s166,s312]) ).
cnf(s314,plain,
~ spl0_41,
inference(rat,[],[s165,s59,s312]) ).
cnf(s315,plain,
~ spl0_1,
inference(rat,[],[s1,s2]) ).
cnf(s316,plain,
~ spl0_71,
inference(rat,[],[s307,s315]) ).
cnf(s317,plain,
~ spl0_70,
inference(rat,[],[s56,s315]) ).
cnf(s318,plain,
~ spl0_14,
inference(rat,[],[s9,s311,s315]) ).
cnf(s319,plain,
( spl0_26
| ~ spl0_12
| spl0_15 ),
inference(rat,[],[s191,s291,s255,s117,s115,s217,s186,s15,s248,s247,s44,s21,s185,s313,s314,s312]) ).
cnf(s320,plain,
( ~ spl0_12
| spl0_15 ),
inference(rat,[],[s11,s186,s255,s197,s42,s43,s319,s185,s312]) ).
cnf(s321,plain,
( ~ spl0_25
| spl0_15
| spl0_4 ),
inference(rat,[],[s117,s111,s217,s44,s21,s42,s7,s320,s312,s313,s314,s2]) ).
cnf(s322,plain,
( ~ spl0_36
| spl0_15
| spl0_4 ),
inference(rat,[],[s19,s44,s7,s320,s321,s312,s2]) ).
cnf(s323,plain,
( spl0_15
| spl0_4 ),
inference(rat,[],[s14,s43,s21,s322,s321,s7,s320,s312,s313,s314,s2]) ).
cnf(s324,plain,
( spl0_26
| ~ spl0_25
| spl0_20
| ~ spl0_12 ),
inference(rat,[],[s192,s255,s291,s115,s117,s217,s247,s21,s185,s313,s314,s312]) ).
cnf(s326,plain,
( ~ spl0_24
| ~ spl0_23
| ~ spl0_12
| spl0_6
| spl0_10 ),
inference(rat,[],[s100,s265,s315,s318]) ).
cnf(s328,plain,
( ~ spl0_9
| ~ spl0_26
| ~ spl0_25 ),
inference(rat,[],[s100,s232,s229,s318]) ).
cnf(s329,plain,
( ~ spl0_34
| spl0_10
| ~ spl0_12
| spl0_6 ),
inference(rat,[],[s266,s60,s98,s315,s318]) ).
cnf(s330,plain,
( spl0_10
| ~ spl0_12
| spl0_6 ),
inference(rat,[],[s326,s58,s55,s329,s316,s317,s318]) ).
cnf(s331,plain,
( ~ spl0_25
| ~ spl0_9
| spl0_20
| ~ spl0_12 ),
inference(rat,[],[s328,s324]) ).
cnf(s332,plain,
( ~ spl0_26
| spl0_19
| ~ spl0_9
| ~ spl0_12 ),
inference(rat,[],[s195,s58,s11,s232,s197,s185,s198,s318,s312]) ).
cnf(s333,plain,
( ~ spl0_12
| spl0_6
| spl0_4 ),
inference(rat,[],[s55,s60,s58,s61,s195,s248,s190,s15,s247,s21,s332,s186,s331,s198,s6,s330,s185,s281,s284,s323,s317,s316,s318,s313,s314,s312,s315,s311]) ).
cnf(s334,plain,
( ~ spl0_34
| spl0_10
| ~ spl0_11
| spl0_6 ),
inference(rat,[],[s94,s60,s98,s315,s318]) ).
cnf(s335,plain,
( spl0_10
| spl0_6
| ~ spl0_11 ),
inference(rat,[],[s13,s100,s58,s55,s334,s316,s317,s318,s315]) ).
cnf(s336,plain,
( ~ spl0_25
| spl0_6
| spl0_4 ),
inference(rat,[],[s111,s159,s117,s217,s21,s328,s6,s335,s7,s333,s284,s323,s312,s313,s314,s311,s315,s2]) ).
cnf(s337,plain,
( ~ spl0_26
| spl0_6
| spl0_4 ),
inference(rat,[],[s58,s207,s232,s14,s6,s335,s7,s333,s284,s323,s336,s318,s312,s311,s315,s2]) ).
cnf(s338,plain,
( spl0_6
| spl0_4 ),
inference(rat,[],[s55,s58,s60,s207,s61,s214,s19,s21,s337,s336,s6,s335,s7,s333,s284,s323,s317,s316,s318,s312,s313,s314,s315,s2,s311]) ).
cnf(s339,plain,
( ~ spl0_34
| spl0_77
| ~ spl0_7 ),
inference(rat,[],[s65,s141,s102,s86,s60,s89,s315,s318]) ).
cnf(s340,plain,
( spl0_77
| ~ spl0_7 ),
inference(rat,[],[s79,s105,s103,s104,s100,s58,s55,s339,s316,s317,s318,s315]) ).
cnf(s341,plain,
( ~ spl0_12
| spl0_4 ),
inference(rat,[],[s55,s60,s58,s61,s195,s248,s190,s15,s247,s21,s332,s186,s331,s276,s258,s185,s234,s281,s284,s323,s340,s5,s338,s317,s316,s318,s313,s314,s315,s312,s311]) ).
cnf(s342,plain,
( ~ spl0_15
| spl0_4 ),
inference(rat,[],[s6,s106,s168,s7,s145,s341,s340,s5,s338,s284,s311,s310,s2,s315,s312]) ).
cnf(s343,plain,
spl0_4,
inference(rat,[],[s342,s323]) ).
cnf(s344,plain,
spl0_5,
inference(rat,[],[s4,s312,s343]) ).
cnf(s345,plain,
spl0_53,
inference(rat,[],[s35,s312,s344]) ).
cnf(s346,plain,
~ spl0_52,
inference(rat,[],[s34,s312,s344]) ).
cnf(s347,plain,
~ spl0_59,
inference(rat,[],[s146,s59,s345]) ).
cnf(s349,plain,
( ~ spl0_42
| spl0_50 ),
inference(rat,[],[s126,s123,s131,s310,s344,s312]) ).
cnf(s354,plain,
spl0_50,
inference(rat,[],[s222,s162,s163,s130,s49,s349,s310,s345,s346,s347]) ).
cnf(s355,plain,
spl0_51,
inference(rat,[],[s294,s345,s311,s354]) ).
cnf(s356,plain,
spl0_8,
inference(rat,[],[s32,s344,s311,s312,s354]) ).
cnf(s357,plain,
~ spl0_9,
inference(rat,[],[s303,s355]) ).
cnf(s358,plain,
~ spl0_10,
inference(rat,[],[s6,s356,s315,s312,s357]) ).
cnf(s359,plain,
~ spl0_12,
inference(rat,[],[s5,s340,s330,s277,s315,s358]) ).
cnf(s362,plain,
spl0_11,
inference(rat,[],[s7,s2,s359]) ).
cnf(s363,plain,
~ spl0_77,
inference(rat,[],[s106,s358,s362]) ).
cnf(s364,plain,
spl0_6,
inference(rat,[],[s335,s358,s362]) ).
cnf(s366,plain,
~ spl0_7,
inference(rat,[],[s340,s363]) ).
cnf(s367,plain,
$false,
inference(rat,[],[s5,s315,s366,s364]) ).
fof(f2059,plain,
$false,
inference(avatar_sat_refutation,[],[s367]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 17:22:50 UTC 2026
% 0.15/0.38 % CPUTime :
% 0.15/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.42 Running first-order model finding
% 0.15/0.42 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.54/0.57 % (3630233)Will run a generic schedule for satisfiability detection.
% 0.54/0.57 % (3630245)dis+10_1_sil=32000:sp=arity:random_seed=797078480:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.54/0.57 % (3630243)% WARNING: option uhcvi not known.
% 0.54/0.57 % (3630246)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3495509440:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.54/0.57 % (3630244)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3200530203:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.54/0.57 % (3630243)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3253319065:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.54/0.57 % (3630242)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2587020682_2999 on theBenchmark for (2999ds/0Mi)
% 0.54/0.57 % TRYING [1]
% 0.54/0.57 % TRYING [2]
% 0.54/0.57 % (3630248)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2276407931:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.54/0.57 % TRYING [3]
% 0.54/0.57 % (3630247)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1136078568:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.54/0.57 % (3630245)Instruction limit reached!
% 0.54/0.57 % (3630245)------------------------------
% 0.54/0.57 % (3630245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.57 % (3630245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.57 % (3630245)CaDiCaL version: 2.1.3
% 0.54/0.57 % (3630245)Termination reason: Instruction limit
% 0.54/0.57 % (3630245)Termination phase: Saturation
% 0.54/0.57 % (3630245)Time elapsed: 0.057 s
% 0.54/0.57 % (3630245)Peak memory usage: 12 MB
% 0.54/0.57 % (3630245)Instructions burned: 105 (million)
% 0.54/0.57 % (3630258)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3821909892:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.54/0.57 % TRYING [1]
% 0.54/0.57 % TRYING [2]
% 0.54/0.57 % TRYING [3]
% 0.54/0.57 % (3630248) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3630233-3630248"...
% 0.54/0.57 % (3630246)Instruction limit reached!
% 0.54/0.57 % (3630246)------------------------------
% 0.54/0.57 % (3630246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.57 % (3630246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.57 % (3630246)CaDiCaL version: 2.1.3
% 0.54/0.57 % (3630246)Termination reason: Instruction limit
% 0.54/0.57 % (3630246)Termination phase: Saturation
% 0.54/0.57 % (3630246)Time elapsed: 0.099 s
% 0.54/0.57 % (3630246)Peak memory usage: 12 MB
% 0.54/0.57 % (3630246)Instructions burned: 117 (million)
% 0.54/0.57 % (3630247) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3630233-3630247"...
% 0.54/0.57 % (3630248)...printing done.
% 0.54/0.57 % (3630248)Refutation found. Thanks to Tanya!
% 0.54/0.57 % SZS status Unsatisfiable for theBenchmark
% 0.54/0.57 % SZS output start Proof for theBenchmark
% See solution above
% 0.54/0.58 % (3630248)------------------------------
% 0.54/0.58 % (3630248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.58 % (3630248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.58 % (3630248)CaDiCaL version: 2.1.3
% 0.54/0.58 % (3630248)Termination reason: Refutation
% 0.54/0.58 % (3630248)Time elapsed: 0.090 s
% 0.54/0.58 % (3630248)Peak memory usage: 13 MB
% 0.54/0.58 % (3630248)Instructions burned: 88 (million)
% 0.54/0.58 % (3630233)Success in time 0.141 s
% 0.54/0.58 % Vampire exiting
%------------------------------------------------------------------------------