%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MGT029-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:34 PM UTC 2026
% Result : Unsatisfiable 0.44s 0.48s
% Output : Refutation 0.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 68
% Syntax : Number of formulae : 613 ( 41 unt; 48 def)
% Number of atoms : 2079 ( 139 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 2507 (1041 ~;1418 |; 0 &)
% ( 48 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 56 ( 54 usr; 49 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 63 ( 0 sgn 63 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ greater(X0,X1)
| ~ greater(X1,X2)
| greater(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity_19) ).
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/sandbox/benchmark/theBenchmark.p',mp_times_in_environment_20) ).
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/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_21) ).
fof(f5,axiom,
! [X0,X1] :
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_22) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_23) ).
fof(f7,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/sandbox/benchmark/theBenchmark.p',l6_24) ).
fof(f8,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/sandbox/benchmark/theBenchmark.p',l6_25) ).
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(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l6_27) ).
fof(f11,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(growth_rate(efficient_producers,X1),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l6_28) ).
fof(f12,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(growth_rate(efficient_producers,X1),zero) ),
inference(reorient_equations,[],[f11]) ).
fof(f13,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/sandbox/benchmark/theBenchmark.p',l6_29) ).
fof(f14,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,[],[f13]) ).
fof(f17,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/sandbox/benchmark/theBenchmark.p',l6_31) ).
fof(f18,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,[],[f17]) ).
fof(f19,axiom,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sk1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_32) ).
fof(f20,axiom,
! [X0,X1] :
( ~ stable(X0)
| ~ environment(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/sandbox/benchmark/theBenchmark.p',l1_33) ).
fof(f21,axiom,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sk2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4_34) ).
fof(f22,axiom,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| greater_or_equal(sk2(X0),equilibrium(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4_35) ).
fof(f23,negated_conjecture,
environment(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_36) ).
fof(f24,negated_conjecture,
stable(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_37) ).
fof(f25,negated_conjecture,
! [X0] :
( ~ in_environment(sk3,X0)
| subpopulations(first_movers,efficient_producers,sk3,sk4(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_38) ).
fof(f26,negated_conjecture,
! [X0] :
( ~ in_environment(sk3,X0)
| greater_or_equal(sk4(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_39) ).
fof(f27,negated_conjecture,
! [X0] :
( ~ in_environment(sk3,X0)
| ~ greater(growth_rate(efficient_producers,sk4(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_40) ).
fof(f28,plain,
! [X0] : greater_or_equal(X0,X0),
inference(equality_resolution,[],[f6]) ).
fof(f29,plain,
( ~ environment(sk3)
| in_environment(sk3,sk1(sk3)) ),
inference(resolution,[],[f19,f24]) ).
fof(f30,plain,
in_environment(sk3,sk1(sk3)),
inference(forward_subsumption_resolution,[],[f29,f23]) ).
fof(f31,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f30,f27]) ).
fof(f32,plain,
subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3))),
inference(resolution,[],[f30,f25]) ).
fof(f33,plain,
greater_or_equal(sk4(sk1(sk3)),sk1(sk3)),
inference(resolution,[],[f30,f26]) ).
fof(f35,definition,
( spl0_1
<=> greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f37,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_1 ),
inference(avatar_component_clause,[],[f35]) ).
fof(f39,definition,
( spl0_2
<=> greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f40,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f39]) ).
fof(f41,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| spl0_2 ),
inference(avatar_component_clause,[],[f39]) ).
fof(f42,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f31,f39,f35]) ).
fof(f43,plain,
( ~ environment(sk3)
| in_environment(sk3,sk2(sk3)) ),
inference(resolution,[],[f21,f24]) ).
fof(f44,plain,
in_environment(sk3,sk2(sk3)),
inference(forward_subsumption_resolution,[],[f43,f23]) ).
fof(f45,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(resolution,[],[f44,f27]) ).
fof(f46,plain,
subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3))),
inference(resolution,[],[f44,f25]) ).
fof(f47,plain,
greater_or_equal(sk4(sk2(sk3)),sk2(sk3)),
inference(resolution,[],[f44,f26]) ).
fof(f49,definition,
( spl0_3
<=> greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f51,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_3 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f53,definition,
( spl0_4
<=> greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f54,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f53]) ).
fof(f55,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| spl0_4 ),
inference(avatar_component_clause,[],[f53]) ).
fof(f56,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f45,f53,f49]) ).
fof(f57,plain,
( ~ environment(sk3)
| greater_or_equal(sk2(sk3),equilibrium(sk3)) ),
inference(resolution,[],[f22,f24]) ).
fof(f58,plain,
greater_or_equal(sk2(sk3),equilibrium(sk3)),
inference(forward_subsumption_resolution,[],[f57,f23]) ).
fof(f59,plain,
( greater(sk2(sk3),equilibrium(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[],[f4,f58]) ).
fof(f60,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| sk1(sk3) = sk4(sk1(sk3)) ),
inference(resolution,[],[f4,f33]) ).
fof(f62,definition,
( spl0_5
<=> sk1(sk3) = sk4(sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f64,plain,
( sk1(sk3) = sk4(sk1(sk3))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f62]) ).
fof(f66,definition,
( spl0_6
<=> greater(sk4(sk1(sk3)),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f68,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f66]) ).
fof(f69,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f60,f66,f62]) ).
fof(f71,definition,
( spl0_7
<=> sk2(sk3) = equilibrium(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f73,plain,
( sk2(sk3) = equilibrium(sk3)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f75,definition,
( spl0_8
<=> greater(sk2(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f77,plain,
( greater(sk2(sk3),equilibrium(sk3))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f78,plain,
( spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f59,f75,f71]) ).
fof(f80,plain,
( in_environment(sk3,equilibrium(sk3))
| ~ spl0_7 ),
inference(superposition,[],[f44,f73]) ).
fof(f81,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| greater(X0,sk1(sk3))
| sk1(sk3) = X0
| greater(sk1(sk3),X0) ),
inference(resolution,[],[f3,f30]) ).
fof(f91,definition,
( spl0_9
<=> greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f93,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| spl0_9 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f95,definition,
( spl0_10
<=> greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f99,plain,
! [X0] :
( ~ environment(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,[],[f20,f24]) ).
fof(f100,plain,
! [X0] :
( ~ greater_or_equal(X0,sk1(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(forward_subsumption_resolution,[],[f99,f23]) ).
fof(f101,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| sk2(sk3) = sk4(sk2(sk3)) ),
inference(resolution,[],[f47,f4]) ).
fof(f103,plain,
( greater(sk4(equilibrium(sk3)),equilibrium(sk3))
| sk2(sk3) = sk4(sk2(sk3))
| ~ spl0_7 ),
inference(forward_demodulation,[],[f101,f73]) ).
fof(f104,plain,
( equilibrium(sk3) = sk4(equilibrium(sk3))
| greater(sk4(equilibrium(sk3)),equilibrium(sk3))
| ~ spl0_7 ),
inference(forward_demodulation,[],[f103,f73]) ).
fof(f106,definition,
( spl0_11
<=> greater(sk4(equilibrium(sk3)),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f107,plain,
( ~ greater(sk4(equilibrium(sk3)),equilibrium(sk3))
| spl0_11 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f108,plain,
( greater(sk4(equilibrium(sk3)),equilibrium(sk3))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f110,definition,
( spl0_12
<=> equilibrium(sk3) = sk4(equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f112,plain,
( equilibrium(sk3) = sk4(equilibrium(sk3))
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f113,plain,
( spl0_11
| spl0_12
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f104,f71,f110,f106]) ).
fof(f115,definition,
( spl0_13
<=> sk2(sk3) = sk4(sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f117,plain,
( sk2(sk3) = sk4(sk2(sk3))
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f119,definition,
( spl0_14
<=> greater(sk4(sk2(sk3)),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f121,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f122,plain,
( spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f101,f119,f115]) ).
fof(f123,plain,
! [X0] :
( ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| zero = growth_rate(first_movers,X0)
| greater(growth_rate(first_movers,X0),zero)
| greater(growth_rate(efficient_producers,X0),zero) ),
inference(resolution,[],[f7,f23]) ).
fof(f124,plain,
! [X0] :
( ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| zero = growth_rate(first_movers,X0)
| greater(growth_rate(first_movers,X0),zero)
| greater(zero,growth_rate(first_movers,X0)) ),
inference(resolution,[],[f8,f23]) ).
fof(f129,plain,
! [X0] :
( ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| zero = growth_rate(first_movers,X0)
| greater(zero,growth_rate(efficient_producers,X0))
| greater(zero,growth_rate(first_movers,X0)) ),
inference(resolution,[],[f10,f23]) ).
fof(f131,plain,
! [X0] :
( ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| zero = growth_rate(efficient_producers,X0)
| greater(growth_rate(first_movers,X0),zero)
| greater(growth_rate(efficient_producers,X0),zero) ),
inference(resolution,[],[f12,f23]) ).
fof(f132,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| ~ spl0_5 ),
inference(superposition,[],[f32,f64]) ).
fof(f133,plain,
! [X0] :
( ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| zero = growth_rate(efficient_producers,X0)
| greater(growth_rate(first_movers,X0),zero)
| greater(zero,growth_rate(first_movers,X0)) ),
inference(resolution,[],[f14,f23]) ).
fof(f135,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| spl0_1
| ~ spl0_5 ),
inference(superposition,[],[f37,f64]) ).
fof(f136,plain,
! [X0] :
( ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| zero = growth_rate(efficient_producers,X0)
| greater(zero,growth_rate(efficient_producers,X0))
| greater(zero,growth_rate(first_movers,X0)) ),
inference(resolution,[],[f18,f23]) ).
fof(f137,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f100,f33]) ).
fof(f138,plain,
greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))),
inference(forward_subsumption_resolution,[],[f137,f32]) ).
fof(f139,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f138,f64]) ).
fof(f140,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| ~ spl0_13 ),
inference(superposition,[],[f46,f117]) ).
fof(f141,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| zero = growth_rate(first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero) ),
inference(resolution,[],[f123,f58]) ).
fof(f142,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f141,f140]) ).
fof(f144,definition,
( spl0_15
<=> greater(growth_rate(efficient_producers,sk2(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f145,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| spl0_15 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f146,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f148,definition,
( spl0_16
<=> greater(growth_rate(first_movers,sk2(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f150,plain,
( greater(growth_rate(first_movers,sk2(sk3)),zero)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f152,definition,
( spl0_17
<=> zero = growth_rate(first_movers,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f153,plain,
( zero != growth_rate(first_movers,sk2(sk3))
| spl0_17 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f154,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f155,plain,
( spl0_15
| spl0_16
| spl0_17
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f142,f115,f152,f148,f144]) ).
fof(f157,definition,
( spl0_18
<=> subpopulations(first_movers,efficient_producers,sk3,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f158,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f160,plain,
( spl0_15
| spl0_16
| spl0_17
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f141,f157,f152,f148,f144]) ).
fof(f161,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| zero = growth_rate(first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(zero,growth_rate(first_movers,sk2(sk3))) ),
inference(resolution,[],[f124,f58]) ).
fof(f163,plain,
( ! [X0] :
( ~ greater(sk2(sk3),X0)
| greater(sk4(sk2(sk3)),X0) )
| ~ spl0_14 ),
inference(resolution,[],[f121,f1]) ).
fof(f165,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| zero = growth_rate(first_movers,sk2(sk3))
| greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk2(sk3))) ),
inference(resolution,[],[f129,f58]) ).
fof(f167,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| zero = growth_rate(efficient_producers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(zero,growth_rate(first_movers,sk2(sk3))) ),
inference(resolution,[],[f133,f58]) ).
fof(f169,plain,
( ! [X0] :
( ~ greater(growth_rate(first_movers,sk1(sk3)),X0)
| greater(growth_rate(efficient_producers,sk1(sk3)),X0) )
| ~ spl0_5 ),
inference(resolution,[],[f139,f1]) ).
fof(f171,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| zero = growth_rate(efficient_producers,sk2(sk3))
| greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk2(sk3))) ),
inference(resolution,[],[f136,f58]) ).
fof(f172,plain,
( greater(sk4(sk2(sk3)),equilibrium(sk3))
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f163,f77]) ).
fof(f174,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3))) ),
inference(resolution,[],[f28,f100]) ).
fof(f206,definition,
( spl0_24
<=> greater(growth_rate(first_movers,equilibrium(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f208,plain,
( greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f220,plain,
( greater(sk2(sk3),sk1(sk3))
| sk1(sk3) = sk2(sk3)
| greater(sk1(sk3),sk2(sk3)) ),
inference(resolution,[],[f81,f44]) ).
fof(f223,definition,
( spl0_26
<=> greater(sk1(sk3),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f224,plain,
( ~ greater(sk1(sk3),sk2(sk3))
| spl0_26 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f225,plain,
( greater(sk1(sk3),sk2(sk3))
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f227,definition,
( spl0_27
<=> sk1(sk3) = sk2(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f229,plain,
( sk1(sk3) = sk2(sk3)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f231,definition,
( spl0_28
<=> greater(sk2(sk3),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f232,plain,
( ~ greater(sk2(sk3),sk1(sk3))
| spl0_28 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f233,plain,
( greater(sk2(sk3),sk1(sk3))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f234,plain,
( spl0_26
| spl0_27
| spl0_28 ),
inference(avatar_split_clause,[],[f220,f231,f227,f223]) ).
fof(f235,plain,
( ! [X0] :
( ~ greater(sk2(sk3),X0)
| greater(sk1(sk3),X0) )
| ~ spl0_26 ),
inference(resolution,[],[f225,f1]) ).
fof(f236,plain,
( greater_or_equal(sk1(sk3),sk2(sk3))
| ~ spl0_26 ),
inference(resolution,[],[f225,f5]) ).
fof(f241,plain,
( greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_8
| ~ spl0_26 ),
inference(resolution,[],[f235,f77]) ).
fof(f243,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| ~ spl0_8
| ~ spl0_26 ),
inference(resolution,[],[f241,f5]) ).
fof(f245,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_8
| ~ spl0_26 ),
inference(resolution,[],[f243,f123]) ).
fof(f252,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_8
| ~ spl0_26 ),
inference(resolution,[],[f243,f136]) ).
fof(f254,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f252,f132]) ).
fof(f261,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f245,f169]) ).
fof(f262,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| spl0_1
| ~ spl0_5
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f254,f135]) ).
fof(f264,definition,
( spl0_29
<=> greater(growth_rate(efficient_producers,sk1(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f265,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| spl0_29 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f268,definition,
( spl0_30
<=> greater(zero,growth_rate(efficient_producers,sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f269,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| spl0_30 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f270,plain,
( greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f272,definition,
( spl0_31
<=> zero = growth_rate(efficient_producers,sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f273,plain,
( zero != growth_rate(efficient_producers,sk1(sk3))
| spl0_31 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f274,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f280,definition,
( spl0_32
<=> zero = growth_rate(first_movers,sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f281,plain,
( zero != growth_rate(first_movers,sk1(sk3))
| spl0_32 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f285,plain,
( zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f261,f132]) ).
fof(f286,plain,
( spl0_30
| spl0_31
| spl0_1
| ~ spl0_5
| ~ spl0_8
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f262,f223,f75,f62,f35,f272,f268]) ).
fof(f295,plain,
( spl0_29
| spl0_32
| ~ spl0_5
| ~ spl0_8
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f285,f223,f75,f62,f280,f264]) ).
fof(f300,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| spl0_3
| ~ spl0_7 ),
inference(superposition,[],[f51,f73]) ).
fof(f308,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| ~ spl0_7
| ~ spl0_26 ),
inference(superposition,[],[f236,f73]) ).
fof(f319,plain,
( greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3))
| ~ spl0_11 ),
inference(resolution,[],[f108,f5]) ).
fof(f320,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_7
| ~ spl0_26 ),
inference(resolution,[],[f308,f123]) ).
fof(f327,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_7
| ~ spl0_26 ),
inference(resolution,[],[f308,f136]) ).
fof(f329,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f327,f132]) ).
fof(f336,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f320,f169]) ).
fof(f337,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| spl0_1
| ~ spl0_5
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f329,f135]) ).
fof(f344,plain,
( zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f336,f132]) ).
fof(f345,plain,
( spl0_30
| spl0_31
| spl0_1
| ~ spl0_5
| ~ spl0_7
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f337,f223,f71,f62,f35,f272,f268]) ).
fof(f350,plain,
( spl0_29
| spl0_32
| ~ spl0_5
| ~ spl0_7
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f344,f223,f71,f62,f280,f264]) ).
fof(f352,definition,
( spl0_34
<=> greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f354,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,definition,
( spl0_35
<=> subpopulations(first_movers,efficient_producers,sk3,sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f357,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f358,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| spl0_35 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,plain,
( spl0_34
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f174,f356,f352]) ).
fof(f375,plain,
( ! [X0] :
( ~ greater(sk1(sk3),X0)
| greater(sk4(sk1(sk3)),X0) )
| ~ spl0_6 ),
inference(resolution,[],[f68,f1]) ).
fof(f377,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| 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)
| ~ spl0_11 ),
inference(resolution,[],[f319,f123]) ).
fof(f378,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_11 ),
inference(resolution,[],[f319,f124]) ).
fof(f380,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| 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))))
| ~ spl0_11 ),
inference(resolution,[],[f319,f129]) ).
fof(f381,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_11 ),
inference(resolution,[],[f319,f131]) ).
fof(f384,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_11 ),
inference(resolution,[],[f319,f136]) ).
fof(f386,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f384,f93]) ).
fof(f388,definition,
( spl0_36
<=> greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f390,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f392,definition,
( spl0_37
<=> zero = growth_rate(efficient_producers,sk4(equilibrium(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f396,definition,
( spl0_38
<=> subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f398,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| spl0_38 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f402,definition,
( spl0_39
<=> greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f404,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f405,plain,
( spl0_10
| spl0_39
| spl0_37
| ~ spl0_38
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f381,f106,f396,f392,f402,f95]) ).
fof(f406,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f380,f93]) ).
fof(f408,definition,
( spl0_40
<=> zero = growth_rate(first_movers,sk4(equilibrium(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f412,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f378,f93]) ).
fof(f413,plain,
( spl0_10
| spl0_39
| spl0_40
| ~ spl0_38
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f377,f106,f396,f408,f402,f95]) ).
fof(f414,plain,
( spl0_36
| spl0_37
| ~ spl0_38
| spl0_9
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f386,f106,f91,f396,f392,f388]) ).
fof(f416,plain,
( spl0_36
| spl0_40
| ~ spl0_38
| spl0_9
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f406,f106,f91,f396,f408,f388]) ).
fof(f417,plain,
( spl0_39
| spl0_40
| ~ spl0_38
| spl0_9
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f412,f106,f91,f396,f408,f402]) ).
fof(f419,plain,
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f172,f5]) ).
fof(f420,plain,
! [X0] :
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),X0)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0) ),
inference(resolution,[],[f138,f1]) ).
fof(f422,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))
| zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f419,f123]) ).
fof(f423,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))
| zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f419,f124]) ).
fof(f425,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))
| zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f419,f129]) ).
fof(f426,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))
| zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f419,f131]) ).
fof(f427,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))
| zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f419,f133]) ).
fof(f429,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))
| zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f419,f136]) ).
fof(f431,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f429,f46]) ).
fof(f433,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f427,f46]) ).
fof(f434,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f426,f46]) ).
fof(f435,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f425,f46]) ).
fof(f437,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f423,f46]) ).
fof(f438,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f422,f46]) ).
fof(f439,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| spl0_3
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f431,f51]) ).
fof(f441,definition,
( spl0_41
<=> greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f442,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| spl0_41 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f443,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f445,definition,
( spl0_42
<=> zero = growth_rate(efficient_producers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f446,plain,
( zero != growth_rate(efficient_producers,sk4(sk2(sk3)))
| spl0_42 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f447,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f451,definition,
( spl0_43
<=> greater(growth_rate(first_movers,sk4(sk2(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f452,plain,
( ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| spl0_43 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f453,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f454,plain,
( spl0_4
| spl0_43
| spl0_42
| ~ spl0_8
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f434,f119,f75,f445,f451,f53]) ).
fof(f455,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| spl0_3
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f435,f51]) ).
fof(f457,definition,
( spl0_44
<=> zero = growth_rate(first_movers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f458,plain,
( zero != growth_rate(first_movers,sk4(sk2(sk3)))
| spl0_44 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f459,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f461,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| spl0_3
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f437,f51]) ).
fof(f462,plain,
( spl0_4
| spl0_43
| spl0_44
| ~ spl0_8
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f438,f119,f75,f457,f451,f53]) ).
fof(f463,plain,
( spl0_41
| spl0_42
| spl0_3
| ~ spl0_8
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f439,f119,f75,f49,f445,f441]) ).
fof(f465,plain,
( spl0_41
| spl0_44
| spl0_3
| ~ spl0_8
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f455,f119,f75,f49,f457,f441]) ).
fof(f466,plain,
( spl0_43
| spl0_44
| spl0_3
| ~ spl0_8
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f461,f119,f75,f49,f457,f451]) ).
fof(f467,plain,
( greater(sk4(sk1(sk3)),sk2(sk3))
| ~ spl0_6
| ~ spl0_26 ),
inference(resolution,[],[f375,f225]) ).
fof(f468,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(resolution,[],[f375,f241]) ).
fof(f470,plain,
( greater_or_equal(sk4(sk1(sk3)),sk2(sk3))
| ~ spl0_6
| ~ spl0_26 ),
inference(resolution,[],[f467,f5]) ).
fof(f473,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(resolution,[],[f468,f5]) ).
fof(f475,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(resolution,[],[f473,f123]) ).
fof(f482,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(resolution,[],[f473,f136]) ).
fof(f484,plain,
( zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f482,f32]) ).
fof(f491,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f475,f420]) ).
fof(f492,plain,
( zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| spl0_1
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f484,f37]) ).
fof(f494,definition,
( spl0_45
<=> greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f495,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| spl0_45 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f496,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f498,definition,
( spl0_46
<=> zero = growth_rate(efficient_producers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f499,plain,
( zero != growth_rate(efficient_producers,sk4(sk1(sk3)))
| spl0_46 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f500,plain,
( zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f506,definition,
( spl0_47
<=> zero = growth_rate(first_movers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f507,plain,
( zero != growth_rate(first_movers,sk4(sk1(sk3)))
| spl0_47 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f508,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f511,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f491,f32]) ).
fof(f512,plain,
( spl0_45
| spl0_46
| spl0_1
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f492,f223,f75,f66,f35,f498,f494]) ).
fof(f514,definition,
( spl0_48
<=> greater(growth_rate(first_movers,sk4(sk1(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f515,plain,
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| spl0_48 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f516,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f521,plain,
( spl0_2
| spl0_47
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f511,f223,f75,f66,f506,f39]) ).
fof(f523,plain,
( ~ greater(zero,zero)
| spl0_3
| ~ spl0_44 ),
inference(superposition,[],[f51,f459]) ).
fof(f525,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_46 ),
inference(superposition,[],[f138,f500]) ).
fof(f526,plain,
( $false
| spl0_1
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f525,f37]) ).
fof(f527,plain,
( spl0_1
| ~ spl0_46 ),
inference(avatar_contradiction_clause,[],[f526]) ).
fof(f537,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f433,f446]) ).
fof(f538,plain,
( greater(zero,zero)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_8
| ~ spl0_14
| spl0_42
| ~ spl0_44 ),
inference(forward_demodulation,[],[f537,f459]) ).
fof(f544,plain,
( ! [X0] :
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0)
| greater(zero,X0) )
| ~ spl0_41 ),
inference(resolution,[],[f443,f1]) ).
fof(f553,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_47 ),
inference(superposition,[],[f138,f508]) ).
fof(f554,plain,
( ~ greater(zero,zero)
| spl0_1
| ~ spl0_47 ),
inference(superposition,[],[f37,f508]) ).
fof(f560,plain,
( $false
| spl0_2
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f553,f41]) ).
fof(f561,plain,
( spl0_2
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f560]) ).
fof(f564,plain,
( $false
| ~ spl0_5
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f132,f358]) ).
fof(f565,plain,
( ~ spl0_5
| spl0_35 ),
inference(avatar_contradiction_clause,[],[f564]) ).
fof(f567,plain,
( zero != growth_rate(first_movers,sk1(sk3))
| ~ spl0_5
| spl0_47 ),
inference(forward_demodulation,[],[f507,f64]) ).
fof(f572,plain,
( ~ spl0_32
| ~ spl0_5
| spl0_47 ),
inference(avatar_split_clause,[],[f567,f506,f62,f280]) ).
fof(f588,plain,
( zero != growth_rate(efficient_producers,sk1(sk3))
| ~ spl0_5
| spl0_46 ),
inference(forward_demodulation,[],[f499,f64]) ).
fof(f589,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| ~ spl0_5
| spl0_45 ),
inference(forward_demodulation,[],[f495,f64]) ).
fof(f590,plain,
( ~ spl0_31
| ~ spl0_5
| spl0_46 ),
inference(avatar_split_clause,[],[f588,f498,f62,f272]) ).
fof(f591,plain,
( ~ spl0_30
| ~ spl0_5
| spl0_45 ),
inference(avatar_split_clause,[],[f589,f494,f62,f268]) ).
fof(f592,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| spl0_2
| ~ spl0_5 ),
inference(superposition,[],[f41,f64]) ).
fof(f600,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| spl0_4
| ~ spl0_27 ),
inference(superposition,[],[f55,f229]) ).
fof(f601,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| ~ spl0_27 ),
inference(superposition,[],[f58,f229]) ).
fof(f610,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_27
| ~ spl0_41 ),
inference(superposition,[],[f443,f229]) ).
fof(f612,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| ~ spl0_27
| ~ spl0_44 ),
inference(superposition,[],[f459,f229]) ).
fof(f613,plain,
( $false
| ~ spl0_27
| ~ spl0_44
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f612,f507]) ).
fof(f614,plain,
( ~ spl0_27
| ~ spl0_44
| spl0_47 ),
inference(avatar_contradiction_clause,[],[f613]) ).
fof(f619,plain,
( ! [X0] :
( ~ greater(growth_rate(first_movers,sk1(sk3)),X0)
| greater(growth_rate(efficient_producers,sk1(sk3)),X0) )
| ~ spl0_34 ),
inference(resolution,[],[f354,f1]) ).
fof(f621,plain,
( greater(sk4(sk2(sk3)),sk1(sk3))
| ~ spl0_14
| ~ spl0_28 ),
inference(resolution,[],[f233,f163]) ).
fof(f623,plain,
( greater_or_equal(sk2(sk3),sk1(sk3))
| ~ spl0_28 ),
inference(resolution,[],[f233,f5]) ).
fof(f624,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ~ spl0_28 ),
inference(resolution,[],[f623,f100]) ).
fof(f630,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ spl0_14
| ~ spl0_28 ),
inference(resolution,[],[f621,f5]) ).
fof(f632,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_14
| ~ spl0_28 ),
inference(resolution,[],[f630,f100]) ).
fof(f634,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_14
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f632,f46]) ).
fof(f635,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_14
| ~ spl0_28
| ~ spl0_44 ),
inference(forward_demodulation,[],[f634,f459]) ).
fof(f636,plain,
( $false
| spl0_4
| ~ spl0_14
| ~ spl0_28
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f635,f55]) ).
fof(f637,plain,
( spl0_4
| ~ spl0_14
| ~ spl0_28
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f636]) ).
fof(f639,plain,
( ~ spl0_29
| spl0_2
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f592,f62,f39,f264]) ).
fof(f642,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_3
| ~ spl0_8
| ~ spl0_14
| spl0_42
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f538,f523]) ).
fof(f643,plain,
( greater(zero,zero)
| spl0_3
| ~ spl0_8
| ~ spl0_14
| spl0_42
| ~ spl0_44 ),
inference(forward_demodulation,[],[f642,f459]) ).
fof(f644,plain,
( $false
| spl0_3
| ~ spl0_8
| ~ spl0_14
| spl0_42
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f643,f523]) ).
fof(f645,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_14
| spl0_42
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f644]) ).
fof(f650,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f161,f158]) ).
fof(f651,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f165,f158]) ).
fof(f653,plain,
( zero = growth_rate(efficient_producers,sk2(sk3))
| greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f171,f158]) ).
fof(f654,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ~ spl0_18
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f624,f158]) ).
fof(f656,definition,
( spl0_49
<=> greater(zero,growth_rate(first_movers,sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f657,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| spl0_49 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f659,plain,
( spl0_49
| spl0_16
| spl0_17
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f650,f157,f152,f148,f656]) ).
fof(f661,definition,
( spl0_50
<=> greater(zero,growth_rate(efficient_producers,sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f663,plain,
( greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f664,plain,
( spl0_49
| spl0_50
| spl0_17
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f651,f157,f152,f661,f656]) ).
fof(f666,definition,
( spl0_51
<=> zero = growth_rate(efficient_producers,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f667,plain,
( zero != growth_rate(efficient_producers,sk2(sk3))
| spl0_51 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f670,plain,
( spl0_49
| spl0_50
| spl0_51
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f653,f157,f666,f661,f656]) ).
fof(f679,plain,
( ! [X0] :
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),X0)
| greater(zero,X0) )
| ~ spl0_50 ),
inference(resolution,[],[f663,f1]) ).
fof(f691,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| spl0_4
| ~ spl0_13 ),
inference(superposition,[],[f55,f117]) ).
fof(f693,plain,
( zero != growth_rate(efficient_producers,sk2(sk3))
| ~ spl0_13
| spl0_42 ),
inference(superposition,[],[f446,f117]) ).
fof(f694,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| ~ spl0_13
| ~ spl0_44 ),
inference(superposition,[],[f459,f117]) ).
fof(f695,plain,
( spl0_17
| ~ spl0_13
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f694,f457,f115,f152]) ).
fof(f696,plain,
( ~ spl0_51
| ~ spl0_13
| spl0_42 ),
inference(avatar_split_clause,[],[f693,f445,f115,f666]) ).
fof(f697,plain,
( $false
| spl0_4
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f691,f146]) ).
fof(f698,plain,
( spl0_4
| ~ spl0_13
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f697]) ).
fof(f723,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_18
| ~ spl0_28
| ~ spl0_50 ),
inference(resolution,[],[f654,f679]) ).
fof(f724,plain,
( ! [X0] :
( ~ greater(growth_rate(first_movers,sk2(sk3)),X0)
| greater(growth_rate(efficient_producers,sk2(sk3)),X0) )
| ~ spl0_18
| ~ spl0_28 ),
inference(resolution,[],[f654,f1]) ).
fof(f726,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_17
| ~ spl0_18
| ~ spl0_28 ),
inference(superposition,[],[f654,f154]) ).
fof(f727,plain,
( $false
| spl0_15
| ~ spl0_17
| ~ spl0_18
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f726,f145]) ).
fof(f728,plain,
( spl0_15
| ~ spl0_17
| ~ spl0_18
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f727]) ).
fof(f735,plain,
( spl0_49
| ~ spl0_18
| ~ spl0_28
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f723,f661,f231,f157,f656]) ).
fof(f764,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_16
| ~ spl0_18
| ~ spl0_28 ),
inference(resolution,[],[f724,f150]) ).
fof(f768,plain,
( $false
| spl0_15
| ~ spl0_16
| ~ spl0_18
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f764,f145]) ).
fof(f769,plain,
( spl0_15
| ~ spl0_16
| ~ spl0_18
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f768]) ).
fof(f790,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_14
| ~ spl0_28 ),
inference(resolution,[],[f630,f100]) ).
fof(f792,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_14
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f790,f46]) ).
fof(f798,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_14
| ~ spl0_28
| ~ spl0_41 ),
inference(resolution,[],[f792,f544]) ).
fof(f799,plain,
( ! [X0] :
( ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),X0)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0) )
| ~ spl0_14
| ~ spl0_28 ),
inference(resolution,[],[f792,f1]) ).
fof(f819,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_14
| ~ spl0_28
| ~ spl0_43 ),
inference(resolution,[],[f799,f453]) ).
fof(f820,plain,
( $false
| spl0_4
| ~ spl0_14
| ~ spl0_28
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f819,f55]) ).
fof(f821,plain,
( spl0_4
| ~ spl0_14
| ~ spl0_28
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f820]) ).
fof(f822,plain,
( $false
| spl0_3
| ~ spl0_14
| ~ spl0_28
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f798,f51]) ).
fof(f823,plain,
( spl0_3
| ~ spl0_14
| ~ spl0_28
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f828,plain,
( greater(zero,zero)
| ~ spl0_4
| ~ spl0_42 ),
inference(superposition,[],[f54,f447]) ).
fof(f830,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_14
| ~ spl0_28
| ~ spl0_42 ),
inference(superposition,[],[f792,f447]) ).
fof(f833,plain,
( $false
| spl0_3
| ~ spl0_14
| ~ spl0_28
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f830,f51]) ).
fof(f834,plain,
( spl0_3
| ~ spl0_14
| ~ spl0_28
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f833]) ).
fof(f835,plain,
( $false
| spl0_3
| ~ spl0_4
| ~ spl0_42
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f828,f523]) ).
fof(f836,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_42
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f835]) ).
fof(f837,plain,
( spl0_18
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f140,f115,f157]) ).
fof(f853,plain,
( zero != growth_rate(first_movers,sk2(sk3))
| ~ spl0_13
| spl0_44 ),
inference(forward_demodulation,[],[f458,f117]) ).
fof(f856,plain,
( $false
| ~ spl0_13
| ~ spl0_17
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f853,f154]) ).
fof(f857,plain,
( ~ spl0_13
| ~ spl0_17
| spl0_44 ),
inference(avatar_contradiction_clause,[],[f856]) ).
fof(f860,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| spl0_3
| ~ spl0_13 ),
inference(superposition,[],[f51,f117]) ).
fof(f862,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| ~ spl0_13
| spl0_41 ),
inference(superposition,[],[f442,f117]) ).
fof(f867,plain,
( greater(sk4(equilibrium(sk3)),equilibrium(sk3))
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f121,f73]) ).
fof(f870,plain,
( zero != growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| ~ spl0_7
| spl0_42 ),
inference(forward_demodulation,[],[f446,f73]) ).
fof(f874,plain,
( zero != growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ spl0_7
| spl0_44 ),
inference(forward_demodulation,[],[f458,f73]) ).
fof(f875,plain,
( ~ spl0_37
| ~ spl0_7
| spl0_42 ),
inference(avatar_split_clause,[],[f870,f445,f71,f392]) ).
fof(f876,plain,
( ~ spl0_40
| ~ spl0_7
| spl0_44 ),
inference(avatar_split_clause,[],[f874,f457,f71,f408]) ).
fof(f878,plain,
( greater(equilibrium(sk3),sk1(sk3))
| sk1(sk3) = equilibrium(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_7 ),
inference(resolution,[],[f80,f81]) ).
fof(f880,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3)))
| ~ spl0_7 ),
inference(resolution,[],[f80,f25]) ).
fof(f883,plain,
( $false
| ~ spl0_7
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f880,f398]) ).
fof(f884,plain,
( ~ spl0_7
| spl0_38 ),
inference(avatar_contradiction_clause,[],[f883]) ).
fof(f886,definition,
( spl0_52
<=> greater(sk1(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f890,definition,
( spl0_53
<=> sk1(sk3) = equilibrium(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f892,plain,
( sk1(sk3) = equilibrium(sk3)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f894,definition,
( spl0_54
<=> greater(equilibrium(sk3),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f896,plain,
( greater(equilibrium(sk3),sk1(sk3))
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f894]) ).
fof(f897,plain,
( spl0_52
| spl0_53
| spl0_54
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f878,f71,f894,f890,f886]) ).
fof(f907,plain,
( ~ greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_7
| spl0_26 ),
inference(superposition,[],[f224,f73]) ).
fof(f910,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_7
| spl0_41 ),
inference(superposition,[],[f442,f73]) ).
fof(f918,plain,
( $false
| ~ spl0_7
| ~ spl0_36
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f910,f390]) ).
fof(f919,plain,
( ~ spl0_7
| ~ spl0_36
| spl0_41 ),
inference(avatar_contradiction_clause,[],[f918]) ).
fof(f921,plain,
( ~ spl0_52
| ~ spl0_7
| spl0_26 ),
inference(avatar_split_clause,[],[f907,f223,f71,f886]) ).
fof(f929,plain,
( ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f55,f73]) ).
fof(f935,plain,
( ~ spl0_10
| spl0_4
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f929,f71,f53,f95]) ).
fof(f985,plain,
( ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ spl0_7
| spl0_43 ),
inference(superposition,[],[f452,f73]) ).
fof(f986,plain,
( $false
| ~ spl0_7
| ~ spl0_39
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f985,f404]) ).
fof(f987,plain,
( ~ spl0_7
| ~ spl0_39
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f986]) ).
fof(f989,plain,
( ~ spl0_9
| spl0_3
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f300,f71,f49,f91]) ).
fof(f997,plain,
( ~ greater(equilibrium(sk3),sk1(sk3))
| ~ spl0_7
| spl0_28 ),
inference(forward_demodulation,[],[f232,f73]) ).
fof(f1007,plain,
( $false
| ~ spl0_7
| spl0_28
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f997,f896]) ).
fof(f1008,plain,
( ~ spl0_7
| spl0_28
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f1007]) ).
fof(f1014,plain,
( ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| spl0_48
| ~ spl0_53 ),
inference(forward_demodulation,[],[f515,f892]) ).
fof(f1019,plain,
( $false
| ~ spl0_39
| spl0_48
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f1014,f404]) ).
fof(f1020,plain,
( ~ spl0_39
| spl0_48
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f1019]) ).
fof(f1022,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_27 ),
inference(resolution,[],[f601,f123]) ).
fof(f1026,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_27 ),
inference(resolution,[],[f601,f131]) ).
fof(f1032,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_27
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1026,f619]) ).
fof(f1034,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_27
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1022,f619]) ).
fof(f1036,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_27
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1032,f357]) ).
fof(f1038,plain,
( zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_27
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1034,f357]) ).
fof(f1040,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_27
| spl0_31
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1036,f273]) ).
fof(f1042,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_27
| spl0_32
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1038,f281]) ).
fof(f1107,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_demodulation,[],[f470,f73]) ).
fof(f1119,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_7
| ~ spl0_26 ),
inference(resolution,[],[f308,f131]) ).
fof(f1129,definition,
( spl0_55
<=> greater(zero,growth_rate(first_movers,sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f1130,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| spl0_55 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f1131,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f1141,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26 ),
inference(resolution,[],[f1107,f123]) ).
fof(f1148,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26 ),
inference(resolution,[],[f1107,f136]) ).
fof(f1152,plain,
( ! [X0] :
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),X0)
| greater(zero,X0) )
| ~ spl0_30 ),
inference(resolution,[],[f270,f1]) ).
fof(f1162,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_31
| ~ spl0_34 ),
inference(superposition,[],[f354,f274]) ).
fof(f1170,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_7
| ~ spl0_26
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1119,f619]) ).
fof(f1172,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_7
| ~ spl0_26
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1170,f357]) ).
fof(f1174,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_7
| ~ spl0_26
| spl0_31
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1172,f273]) ).
fof(f1176,plain,
( $false
| ~ spl0_7
| ~ spl0_26
| spl0_29
| spl0_31
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1174,f265]) ).
fof(f1177,plain,
( ~ spl0_7
| ~ spl0_26
| spl0_29
| spl0_31
| ~ spl0_34
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f1176]) ).
fof(f1195,plain,
( ! [X0] :
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| greater(zero,X0) )
| ~ spl0_45 ),
inference(resolution,[],[f496,f1]) ).
fof(f1198,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_48 ),
inference(resolution,[],[f516,f420]) ).
fof(f1201,plain,
( $false
| spl0_2
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f1198,f41]) ).
fof(f1202,plain,
( spl0_2
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f1201]) ).
fof(f1204,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1141,f420]) ).
fof(f1206,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1204,f32]) ).
fof(f1208,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f1206,f507]) ).
fof(f1211,plain,
( $false
| spl0_2
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f1208,f41]) ).
fof(f1212,plain,
( spl0_2
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_47 ),
inference(avatar_contradiction_clause,[],[f1211]) ).
fof(f1258,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_30
| ~ spl0_34 ),
inference(resolution,[],[f1152,f354]) ).
fof(f1259,plain,
( spl0_55
| ~ spl0_30
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1258,f352,f268,f1129]) ).
fof(f1317,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_45 ),
inference(resolution,[],[f1195,f138]) ).
fof(f1323,plain,
( $false
| spl0_1
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f1317,f37]) ).
fof(f1324,plain,
( spl0_1
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f1323]) ).
fof(f1325,plain,
( zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1148,f32]) ).
fof(f1327,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f1325,f499]) ).
fof(f1329,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_45
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f1327,f495]) ).
fof(f1331,plain,
( $false
| spl0_1
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_45
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f1329,f37]) ).
fof(f1332,plain,
( spl0_1
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_45
| spl0_46 ),
inference(avatar_contradiction_clause,[],[f1331]) ).
fof(f1339,plain,
( greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f150,f73]) ).
fof(f1344,plain,
( spl0_29
| ~ spl0_27
| spl0_31
| ~ spl0_34
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f1040,f356,f352,f272,f227,f264]) ).
fof(f1345,plain,
( spl0_29
| ~ spl0_27
| spl0_32
| ~ spl0_34
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f1042,f356,f352,f280,f227,f264]) ).
fof(f1353,plain,
( zero = growth_rate(efficient_producers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f167,f158]) ).
fof(f1359,plain,
( $false
| ~ spl0_7
| spl0_11
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f867,f107]) ).
fof(f1360,plain,
( ~ spl0_7
| spl0_11
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1359]) ).
fof(f1367,plain,
( spl0_24
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1339,f148,f71,f206]) ).
fof(f1375,plain,
( greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_18
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f1353,f667]) ).
fof(f1393,plain,
( $false
| ~ spl0_2
| spl0_4
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f600,f40]) ).
fof(f1394,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1393]) ).
fof(f1456,plain,
( ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| spl0_48
| ~ spl0_53 ),
inference(forward_demodulation,[],[f515,f892]) ).
fof(f1474,plain,
( ~ greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| ~ spl0_12
| spl0_48
| ~ spl0_53 ),
inference(forward_demodulation,[],[f1456,f112]) ).
fof(f1478,plain,
( $false
| ~ spl0_12
| ~ spl0_24
| spl0_48
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f1474,f208]) ).
fof(f1479,plain,
( ~ spl0_12
| ~ spl0_24
| spl0_48
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f1478]) ).
fof(f1483,plain,
( ~ spl0_49
| spl0_3
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f860,f115,f49,f656]) ).
fof(f1489,plain,
( ~ spl0_50
| ~ spl0_13
| spl0_41 ),
inference(avatar_split_clause,[],[f862,f441,f115,f661]) ).
fof(f1502,plain,
( greater(zero,zero)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_17
| ~ spl0_18
| spl0_51 ),
inference(forward_demodulation,[],[f1375,f154]) ).
fof(f1522,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| spl0_1
| ~ spl0_17
| ~ spl0_18
| ~ spl0_47
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f1502,f554]) ).
fof(f1532,plain,
( greater(zero,zero)
| spl0_1
| ~ spl0_17
| ~ spl0_18
| ~ spl0_47
| spl0_51 ),
inference(forward_demodulation,[],[f1522,f154]) ).
fof(f1536,plain,
( $false
| spl0_1
| ~ spl0_17
| ~ spl0_18
| ~ spl0_47
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f1532,f554]) ).
fof(f1537,plain,
( spl0_1
| ~ spl0_17
| ~ spl0_18
| ~ spl0_47
| spl0_51 ),
inference(avatar_contradiction_clause,[],[f1536]) ).
fof(f1541,plain,
( spl0_45
| ~ spl0_27
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f610,f441,f227,f494]) ).
fof(f1546,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_27
| spl0_49 ),
inference(forward_demodulation,[],[f657,f229]) ).
fof(f1552,plain,
( $false
| ~ spl0_27
| spl0_49
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f1546,f1131]) ).
fof(f1553,plain,
( ~ spl0_27
| spl0_49
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f1552]) ).
fof(f1561,plain,
( spl0_55
| ~ spl0_31
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1162,f352,f272,f1129]) ).
fof(f1579,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| ~ spl0_18
| ~ spl0_27 ),
inference(superposition,[],[f158,f229]) ).
fof(f1581,plain,
( $false
| ~ spl0_18
| ~ spl0_27
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1579,f358]) ).
fof(f1582,plain,
( ~ spl0_18
| ~ spl0_27
| spl0_35 ),
inference(avatar_contradiction_clause,[],[f1581]) ).
fof(f1590,plain,
( zero != growth_rate(first_movers,sk1(sk3))
| spl0_17
| ~ spl0_27 ),
inference(superposition,[],[f153,f229]) ).
fof(f1598,plain,
( ~ subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_27 ),
inference(resolution,[],[f601,f129]) ).
fof(f1605,plain,
( zero = growth_rate(first_movers,sk1(sk3))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_27
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1598,f357]) ).
fof(f1607,plain,
( greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_27
| spl0_32
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1605,f281]) ).
fof(f1609,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_27
| spl0_30
| spl0_32
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1607,f269]) ).
fof(f1612,plain,
( $false
| ~ spl0_27
| spl0_30
| spl0_32
| ~ spl0_35
| spl0_55 ),
inference(forward_subsumption_resolution,[],[f1609,f1130]) ).
fof(f1613,plain,
( ~ spl0_27
| spl0_30
| spl0_32
| ~ spl0_35
| spl0_55 ),
inference(avatar_contradiction_clause,[],[f1612]) ).
fof(f1617,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| spl0_4
| ~ spl0_13 ),
inference(forward_demodulation,[],[f55,f117]) ).
fof(f1619,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| spl0_15
| ~ spl0_27 ),
inference(forward_demodulation,[],[f145,f229]) ).
fof(f1628,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| spl0_4
| ~ spl0_13
| ~ spl0_27 ),
inference(forward_demodulation,[],[f1617,f229]) ).
fof(f1631,plain,
( $false
| spl0_15
| ~ spl0_27
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1619,f266]) ).
fof(f1632,plain,
( spl0_15
| ~ spl0_27
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1631]) ).
fof(f1634,plain,
( $false
| spl0_4
| ~ spl0_13
| ~ spl0_27
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1628,f266]) ).
fof(f1635,plain,
( spl0_4
| ~ spl0_13
| ~ spl0_27
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1634]) ).
fof(f1648,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| ~ spl0_27
| ~ spl0_43 ),
inference(forward_demodulation,[],[f453,f229]) ).
fof(f1650,plain,
( ~ spl0_32
| spl0_17
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1590,f227,f152,f280]) ).
fof(f1658,plain,
( $false
| ~ spl0_27
| ~ spl0_43
| spl0_48 ),
inference(forward_subsumption_resolution,[],[f1648,f515]) ).
fof(f1659,plain,
( ~ spl0_27
| ~ spl0_43
| spl0_48 ),
inference(avatar_contradiction_clause,[],[f1658]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f42]) ).
cnf(s2,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f56]) ).
cnf(s3,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f69]) ).
cnf(s4,plain,
( spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f78]) ).
cnf(s6,plain,
( ~ spl0_7
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f113]) ).
cnf(s7,plain,
( spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f122]) ).
cnf(s8,plain,
( ~ spl0_13
| spl0_15
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f155]) ).
cnf(s9,plain,
( spl0_15
| spl0_16
| spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f160]) ).
cnf(s18,plain,
( spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f234]) ).
cnf(s21,plain,
( spl0_1
| ~ spl0_5
| ~ spl0_8
| ~ spl0_26
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f286]) ).
cnf(s26,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_26
| spl0_29
| spl0_32 ),
inference(sat_conversion,[],[f295]) ).
cnf(s30,plain,
( spl0_1
| ~ spl0_5
| ~ spl0_7
| ~ spl0_26
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f345]) ).
cnf(s35,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_26
| spl0_29
| spl0_32 ),
inference(sat_conversion,[],[f350]) ).
cnf(s36,plain,
( spl0_34
| ~ spl0_35 ),
inference(sat_conversion,[],[f359]) ).
cnf(s38,plain,
( spl0_10
| ~ spl0_11
| spl0_37
| ~ spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f405]) ).
cnf(s40,plain,
( spl0_10
| ~ spl0_11
| ~ spl0_38
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f413]) ).
cnf(s41,plain,
( spl0_9
| ~ spl0_11
| spl0_36
| spl0_37
| ~ spl0_38 ),
inference(sat_conversion,[],[f414]) ).
cnf(s43,plain,
( spl0_9
| ~ spl0_11
| spl0_36
| ~ spl0_38
| spl0_40 ),
inference(sat_conversion,[],[f416]) ).
cnf(s44,plain,
( spl0_9
| ~ spl0_11
| ~ spl0_38
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f417]) ).
cnf(s46,plain,
( spl0_4
| ~ spl0_8
| ~ spl0_14
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f454]) ).
cnf(s48,plain,
( spl0_4
| ~ spl0_8
| ~ spl0_14
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f462]) ).
cnf(s49,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_14
| spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f463]) ).
cnf(s51,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_14
| spl0_41
| spl0_44 ),
inference(sat_conversion,[],[f465]) ).
cnf(s52,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_14
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f466]) ).
cnf(s55,plain,
( spl0_1
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26
| spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f512]) ).
cnf(s60,plain,
( spl0_2
| ~ spl0_6
| ~ spl0_8
| ~ spl0_26
| spl0_47 ),
inference(sat_conversion,[],[f521]) ).
cnf(s61,plain,
( spl0_1
| ~ spl0_46 ),
inference(sat_conversion,[],[f527]) ).
cnf(s65,plain,
( spl0_2
| ~ spl0_47 ),
inference(sat_conversion,[],[f561]) ).
cnf(s66,plain,
( ~ spl0_5
| spl0_35 ),
inference(sat_conversion,[],[f565]) ).
cnf(s67,plain,
( ~ spl0_5
| ~ spl0_32
| spl0_47 ),
inference(sat_conversion,[],[f572]) ).
cnf(s71,plain,
( ~ spl0_5
| ~ spl0_31
| spl0_46 ),
inference(sat_conversion,[],[f590]) ).
cnf(s72,plain,
( ~ spl0_5
| ~ spl0_30
| spl0_45 ),
inference(sat_conversion,[],[f591]) ).
cnf(s74,plain,
( ~ spl0_27
| ~ spl0_44
| spl0_47 ),
inference(sat_conversion,[],[f614]) ).
cnf(s77,plain,
( spl0_4
| ~ spl0_14
| ~ spl0_28
| ~ spl0_44 ),
inference(sat_conversion,[],[f637]) ).
cnf(s78,plain,
( spl0_2
| ~ spl0_5
| ~ spl0_29 ),
inference(sat_conversion,[],[f639]) ).
cnf(s80,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_14
| spl0_42
| ~ spl0_44 ),
inference(sat_conversion,[],[f645]) ).
cnf(s82,plain,
( spl0_16
| spl0_17
| ~ spl0_18
| spl0_49 ),
inference(sat_conversion,[],[f659]) ).
cnf(s83,plain,
( spl0_17
| ~ spl0_18
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f664]) ).
cnf(s85,plain,
( ~ spl0_18
| spl0_49
| spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f670]) ).
cnf(s86,plain,
( ~ spl0_13
| spl0_17
| ~ spl0_44 ),
inference(sat_conversion,[],[f695]) ).
cnf(s87,plain,
( ~ spl0_13
| spl0_42
| ~ spl0_51 ),
inference(sat_conversion,[],[f696]) ).
cnf(s88,plain,
( spl0_4
| ~ spl0_13
| ~ spl0_15 ),
inference(sat_conversion,[],[f698]) ).
cnf(s90,plain,
( spl0_15
| ~ spl0_17
| ~ spl0_18
| ~ spl0_28 ),
inference(sat_conversion,[],[f728]) ).
cnf(s91,plain,
( ~ spl0_18
| ~ spl0_28
| spl0_49
| ~ spl0_50 ),
inference(sat_conversion,[],[f735]) ).
cnf(s93,plain,
( spl0_15
| ~ spl0_16
| ~ spl0_18
| ~ spl0_28 ),
inference(sat_conversion,[],[f769]) ).
cnf(s94,plain,
( spl0_4
| ~ spl0_14
| ~ spl0_28
| ~ spl0_43 ),
inference(sat_conversion,[],[f821]) ).
cnf(s95,plain,
( spl0_3
| ~ spl0_14
| ~ spl0_28
| ~ spl0_41 ),
inference(sat_conversion,[],[f823]) ).
cnf(s96,plain,
( spl0_3
| ~ spl0_14
| ~ spl0_28
| ~ spl0_42 ),
inference(sat_conversion,[],[f834]) ).
cnf(s97,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_42
| ~ spl0_44 ),
inference(sat_conversion,[],[f836]) ).
cnf(s98,plain,
( ~ spl0_13
| spl0_18 ),
inference(sat_conversion,[],[f837]) ).
cnf(s104,plain,
( ~ spl0_13
| ~ spl0_17
| spl0_44 ),
inference(sat_conversion,[],[f857]) ).
cnf(s106,plain,
( ~ spl0_7
| ~ spl0_37
| spl0_42 ),
inference(sat_conversion,[],[f875]) ).
cnf(s107,plain,
( ~ spl0_7
| ~ spl0_40
| spl0_44 ),
inference(sat_conversion,[],[f876]) ).
cnf(s108,plain,
( ~ spl0_7
| spl0_38 ),
inference(sat_conversion,[],[f884]) ).
cnf(s109,plain,
( ~ spl0_7
| spl0_52
| spl0_53
| spl0_54 ),
inference(sat_conversion,[],[f897]) ).
cnf(s112,plain,
( ~ spl0_7
| ~ spl0_36
| spl0_41 ),
inference(sat_conversion,[],[f919]) ).
cnf(s114,plain,
( ~ spl0_7
| spl0_26
| ~ spl0_52 ),
inference(sat_conversion,[],[f921]) ).
cnf(s120,plain,
( spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(sat_conversion,[],[f935]) ).
cnf(s122,plain,
( ~ spl0_7
| ~ spl0_39
| spl0_43 ),
inference(sat_conversion,[],[f987]) ).
cnf(s123,plain,
( spl0_3
| ~ spl0_7
| ~ spl0_9 ),
inference(sat_conversion,[],[f989]) ).
cnf(s129,plain,
( ~ spl0_7
| spl0_28
| ~ spl0_54 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s130,plain,
( ~ spl0_39
| spl0_48
| ~ spl0_53 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s146,plain,
( ~ spl0_7
| ~ spl0_26
| spl0_29
| spl0_31
| ~ spl0_34
| ~ spl0_35 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s148,plain,
( spl0_2
| ~ spl0_48 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s150,plain,
( spl0_2
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_47 ),
inference(sat_conversion,[],[f1212]) ).
cnf(s153,plain,
( ~ spl0_30
| ~ spl0_34
| spl0_55 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s154,plain,
( spl0_1
| ~ spl0_45 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s155,plain,
( spl0_1
| ~ spl0_6
| ~ spl0_7
| ~ spl0_26
| spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f1332]) ).
cnf(s159,plain,
( ~ spl0_27
| spl0_29
| spl0_31
| ~ spl0_34
| ~ spl0_35 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s160,plain,
( ~ spl0_27
| spl0_29
| spl0_32
| ~ spl0_34
| ~ spl0_35 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s162,plain,
( ~ spl0_7
| spl0_11
| ~ spl0_14 ),
inference(sat_conversion,[],[f1360]) ).
cnf(s166,plain,
( ~ spl0_7
| ~ spl0_16
| spl0_24 ),
inference(sat_conversion,[],[f1367]) ).
cnf(s172,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_27 ),
inference(sat_conversion,[],[f1394]) ).
cnf(s182,plain,
( ~ spl0_12
| ~ spl0_24
| spl0_48
| ~ spl0_53 ),
inference(sat_conversion,[],[f1479]) ).
cnf(s183,plain,
( spl0_3
| ~ spl0_13
| ~ spl0_49 ),
inference(sat_conversion,[],[f1483]) ).
cnf(s187,plain,
( ~ spl0_13
| spl0_41
| ~ spl0_50 ),
inference(sat_conversion,[],[f1489]) ).
cnf(s196,plain,
( spl0_1
| ~ spl0_17
| ~ spl0_18
| ~ spl0_47
| spl0_51 ),
inference(sat_conversion,[],[f1537]) ).
cnf(s197,plain,
( ~ spl0_27
| ~ spl0_41
| spl0_45 ),
inference(sat_conversion,[],[f1541]) ).
cnf(s198,plain,
( ~ spl0_27
| spl0_49
| ~ spl0_55 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s201,plain,
( ~ spl0_31
| ~ spl0_34
| spl0_55 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s202,plain,
( ~ spl0_18
| ~ spl0_27
| spl0_35 ),
inference(sat_conversion,[],[f1582]) ).
cnf(s204,plain,
( ~ spl0_27
| spl0_30
| spl0_32
| ~ spl0_35
| spl0_55 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s207,plain,
( spl0_15
| ~ spl0_27
| ~ spl0_29 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s208,plain,
( spl0_4
| ~ spl0_13
| ~ spl0_27
| ~ spl0_29 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s209,plain,
( spl0_17
| ~ spl0_27
| ~ spl0_32 ),
inference(sat_conversion,[],[f1650]) ).
cnf(s210,plain,
( ~ spl0_27
| ~ spl0_43
| spl0_48 ),
inference(sat_conversion,[],[f1659]) ).
cnf(s211,plain,
( ~ spl0_28
| ~ spl0_14
| ~ spl0_8
| spl0_4
| spl0_3 ),
inference(rat,[],[s46,s94,s96]) ).
cnf(s212,plain,
( ~ spl0_14
| spl0_26
| ~ spl0_8
| spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s48,s74,s210,s18,s211,s148,s65]) ).
cnf(s213,plain,
( ~ spl0_28
| spl0_15
| ~ spl0_18
| spl0_49 ),
inference(rat,[],[s83,s90,s91]) ).
cnf(s214,plain,
( spl0_26
| ~ spl0_8
| spl0_2
| spl0_4
| spl0_3 ),
inference(rat,[],[s159,s201,s36,s198,s202,s207,s18,s213,s88,s98,s183,s7,s212]) ).
cnf(s215,plain,
( ~ spl0_8
| ~ spl0_6
| spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s214,s60,s65]) ).
cnf(s216,plain,
( ~ spl0_28
| ~ spl0_14
| ~ spl0_7
| spl0_4
| spl0_3 ),
inference(rat,[],[s38,s122,s106,s94,s96,s108,s120,s162]) ).
cnf(s217,plain,
( ~ spl0_14
| ~ spl0_6
| spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s44,s107,s130,s74,s109,s18,s129,s216,s162,s148,s108,s123,s114,s150,s65,s4,s215]) ).
cnf(s218,plain,
( ~ spl0_6
| spl0_4
| spl0_3
| spl0_2
| spl0_45 ),
inference(rat,[],[s83,s104,s187,s74,s197,s18,s213,s88,s98,s183,s7,s217,s150,s4,s215,s65]) ).
cnf(s219,plain,
( ~ spl0_28
| ~ spl0_7
| spl0_3
| spl0_4 ),
inference(rat,[],[s213,s88,s98,s183,s7,s216]) ).
cnf(s220,plain,
( spl0_26
| spl0_27
| spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s219,s4,s18,s214]) ).
cnf(s221,plain,
( spl0_4
| spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s4,s26,s146,s220,s160,s36,s71,s66,s67,s78,s3,s218,s154,s61,s65]) ).
cnf(s222,plain,
( ~ spl0_14
| ~ spl0_28
| ~ spl0_8
| spl0_3 ),
inference(rat,[],[s49,s95,s96]) ).
cnf(s223,plain,
( ~ spl0_28
| ~ spl0_8
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s97,s104,s87,s83,s85,s91,s98,s183,s7,s222]) ).
cnf(s224,plain,
( ~ spl0_8
| spl0_26
| ~ spl0_4
| spl0_3
| spl0_2
| spl0_45 ),
inference(rat,[],[s83,s104,s187,s98,s183,s7,s52,s74,s197,s210,s18,s223,s148,s65]) ).
cnf(s225,plain,
( ~ spl0_14
| ~ spl0_28
| ~ spl0_7
| spl0_3 ),
inference(rat,[],[s41,s112,s106,s95,s96,s162,s108,s123]) ).
cnf(s226,plain,
( ~ spl0_28
| ~ spl0_7
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s97,s104,s87,s83,s85,s91,s98,s183,s7,s225]) ).
cnf(s227,plain,
( spl0_26
| ~ spl0_4
| spl0_3
| spl0_2
| spl0_45 ),
inference(rat,[],[s83,s104,s187,s98,s183,s7,s162,s44,s107,s130,s74,s197,s109,s18,s129,s226,s114,s123,s108,s4,s224,s148,s65]) ).
cnf(s228,plain,
( ~ spl0_8
| ~ spl0_26
| spl0_2
| spl0_47 ),
inference(rat,[],[s26,s67,s78,s3,s60]) ).
cnf(s229,plain,
( ~ spl0_7
| ~ spl0_26
| spl0_2
| spl0_47 ),
inference(rat,[],[s35,s67,s78,s3,s150]) ).
cnf(s230,plain,
( ~ spl0_26
| spl0_47
| spl0_2 ),
inference(rat,[],[s229,s4,s228]) ).
cnf(s231,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s227,s221,s154,s230,s65]) ).
cnf(s232,plain,
( ~ spl0_14
| ~ spl0_28
| ~ spl0_8
| spl0_4 ),
inference(rat,[],[s48,s94,s77]) ).
cnf(s233,plain,
( ~ spl0_28
| ~ spl0_8
| spl0_4 ),
inference(rat,[],[s8,s90,s93,s88,s98,s7,s232]) ).
cnf(s234,plain,
( ~ spl0_8
| spl0_4
| spl0_26
| spl0_47
| spl0_48 ),
inference(rat,[],[s160,s36,s209,s202,s104,s208,s98,s7,s48,s74,s210,s18,s233]) ).
cnf(s235,plain,
( ~ spl0_14
| ~ spl0_28
| ~ spl0_7
| spl0_4 ),
inference(rat,[],[s40,s122,s107,s94,s77,s162,s108,s120]) ).
cnf(s236,plain,
( ~ spl0_28
| spl0_4
| ~ spl0_7 ),
inference(rat,[],[s8,s90,s93,s88,s98,s7,s235]) ).
cnf(s237,plain,
( spl0_4
| spl0_48
| spl0_26
| spl0_47 ),
inference(rat,[],[s9,s166,s104,s88,s98,s182,s7,s6,s162,s40,s107,s130,s74,s109,s18,s129,s236,s114,s120,s108,s4,s234]) ).
cnf(s238,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s237,s2,s231,s230,s65,s148]) ).
cnf(s239,plain,
( ~ spl0_28
| spl0_4 ),
inference(rat,[],[s4,s236,s233]) ).
cnf(s240,plain,
( spl0_4
| spl0_26
| ~ spl0_2 ),
inference(rat,[],[s239,s18,s172]) ).
cnf(s241,plain,
( spl0_44
| spl0_41
| spl0_3
| ~ spl0_8 ),
inference(rat,[],[s83,s104,s187,s98,s183,s7,s51]) ).
cnf(s242,plain,
( ~ spl0_8
| spl0_26
| spl0_1 ),
inference(rat,[],[s196,s87,s86,s98,s7,s80,s97,s74,s241,s197,s18,s223,s154,s2,s240,s238]) ).
cnf(s243,plain,
( ~ spl0_11
| spl0_36
| ~ spl0_7
| ~ spl0_4 ),
inference(rat,[],[s97,s106,s107,s41,s43,s108,s123,s2]) ).
cnf(s244,plain,
( spl0_26
| spl0_1 ),
inference(rat,[],[s97,s104,s87,s83,s85,s187,s98,s183,s7,s162,s243,s112,s197,s18,s226,s4,s242,s2,s240,s154,s238]) ).
cnf(s245,plain,
( ~ spl0_8
| spl0_46
| spl0_1
| ~ spl0_26
| spl0_45 ),
inference(rat,[],[s21,s71,s72,s3,s55]) ).
cnf(s246,plain,
( ~ spl0_7
| spl0_46
| spl0_1
| ~ spl0_26
| spl0_45 ),
inference(rat,[],[s30,s71,s72,s3,s155]) ).
cnf(s247,plain,
( spl0_46
| spl0_45
| spl0_1
| ~ spl0_26 ),
inference(rat,[],[s246,s4,s245]) ).
cnf(s248,plain,
spl0_1,
inference(rat,[],[s247,s244,s61,s154]) ).
cnf(s249,plain,
~ spl0_2,
inference(rat,[],[s1,s248]) ).
cnf(s250,plain,
~ spl0_48,
inference(rat,[],[s148,s249]) ).
cnf(s251,plain,
~ spl0_47,
inference(rat,[],[s65,s249]) ).
cnf(s252,plain,
~ spl0_26,
inference(rat,[],[s230,s249,s251]) ).
cnf(s253,plain,
spl0_4,
inference(rat,[],[s237,s250,s252,s251]) ).
cnf(s254,plain,
~ spl0_3,
inference(rat,[],[s2,s253]) ).
cnf(s256,plain,
~ spl0_8,
inference(rat,[],[s153,s204,s36,s209,s202,s198,s104,s98,s183,s7,s52,s74,s210,s18,s223,s254,s251,s250,s252,s253]) ).
cnf(s257,plain,
spl0_7,
inference(rat,[],[s4,s256]) ).
cnf(s258,plain,
spl0_38,
inference(rat,[],[s108,s257]) ).
cnf(s259,plain,
~ spl0_52,
inference(rat,[],[s114,s252,s257]) ).
cnf(s261,plain,
~ spl0_28,
inference(rat,[],[s226,s254,s253,s257]) ).
cnf(s262,plain,
~ spl0_54,
inference(rat,[],[s129,s261,s257]) ).
cnf(s263,plain,
~ spl0_9,
inference(rat,[],[s123,s254,s257]) ).
cnf(s264,plain,
spl0_27,
inference(rat,[],[s18,s252,s261]) ).
cnf(s265,plain,
spl0_53,
inference(rat,[],[s109,s257,s259,s262]) ).
cnf(s267,plain,
~ spl0_44,
inference(rat,[],[s74,s251,s264]) ).
cnf(s268,plain,
~ spl0_39,
inference(rat,[],[s130,s250,s265]) ).
cnf(s269,plain,
~ spl0_40,
inference(rat,[],[s107,s257,s267]) ).
cnf(s270,plain,
~ spl0_11,
inference(rat,[],[s44,s263,s268,s258,s269]) ).
cnf(s271,plain,
~ spl0_14,
inference(rat,[],[s162,s257,s270]) ).
cnf(s272,plain,
spl0_12,
inference(rat,[],[s6,s257,s270]) ).
cnf(s273,plain,
spl0_13,
inference(rat,[],[s7,s271]) ).
cnf(s274,plain,
~ spl0_24,
inference(rat,[],[s182,s265,s250,s272]) ).
cnf(s276,plain,
~ spl0_49,
inference(rat,[],[s183,s254,s273]) ).
cnf(s277,plain,
spl0_18,
inference(rat,[],[s98,s273]) ).
cnf(s279,plain,
~ spl0_17,
inference(rat,[],[s104,s267,s273]) ).
cnf(s280,plain,
~ spl0_16,
inference(rat,[],[s166,s257,s274]) ).
cnf(s286,plain,
$false,
inference(rat,[],[s82,s276,s277,s280,s279]) ).
fof(f1660,plain,
$false,
inference(avatar_sat_refutation,[],[s286]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT029-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.05/0.36 % Computer : n001.cluster.edu
% 0.05/0.36 % Model : x86_64 x86_64
% 0.05/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.36 % Memory : 8046.5625MB
% 0.05/0.36 % OS : Linux 6.8.0-71-generic
% 0.05/0.36 % CPULimit : 300
% 0.05/0.36 % WCLimit : 300
% 0.05/0.36 % DateTime : Sun Sep 27 17:27:16 UTC 2026
% 0.05/0.36 % CPUTime :
% 0.05/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.05/0.40 Running first-order model finding
% 0.05/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.44/0.48 % (3823789)Will run a generic schedule for satisfiability detection.
% 0.44/0.48 % (3823794)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=562965825_2999 on theBenchmark for (2999ds/0Mi)
% 0.44/0.48 % TRYING [1]
% 0.44/0.48 % TRYING [2]
% 0.44/0.48 % (3823795)% WARNING: option uhcvi not known.
% 0.44/0.48 % TRYING [3]
% 0.44/0.48 % (3823796)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1945265492:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.44/0.48 % (3823797)dis+10_1_sil=32000:sp=arity:random_seed=1544560865:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.44/0.48 % (3823798)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3634870641:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.44/0.48 % (3823799)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2728433251:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.44/0.48 % (3823800)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2611892277:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.44/0.48 % (3823795)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3804133680:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.44/0.48 % TRYING [4]
% 0.44/0.48 % (3823799) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3823789-3823799"...
% 0.44/0.48 % (3823800) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3823789-3823800"...
% 0.44/0.48 % (3823799)...printing done.
% 0.44/0.48 % (3823799)Refutation found. Thanks to Tanya!
% 0.44/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.44/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.44/0.49 % (3823799)------------------------------
% 0.44/0.49 % (3823799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.49 % (3823799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.49 % (3823799)CaDiCaL version: 2.1.3
% 0.44/0.49 % (3823799)Termination reason: Refutation
% 0.44/0.49 % (3823799)Time elapsed: 0.043 s
% 0.44/0.49 % (3823799)Peak memory usage: 12 MB
% 0.44/0.49 % (3823799)Instructions burned: 65 (million)
% 0.44/0.49 % (3823789)Success in time 0.077 s
% 0.44/0.49 % Vampire exiting
%------------------------------------------------------------------------------