%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n017.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:05 PM UTC 2026
% Result : Unsatisfiable 3.56s 1.41s
% Output : Refutation 4.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 57
% Syntax : Number of formulae : 561 ( 21 unt; 39 def)
% Number of atoms : 1821 ( 138 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 2169 ( 909 ~;1221 |; 0 &)
% ( 39 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 47 ( 45 usr; 40 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 51 ( 0 sgn 51 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| 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,X2)
| ~ in_environment(X0,X1)
| 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] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ~ 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(f10,axiom,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ~ 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(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] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ~ 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] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ~ 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] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ stable(X0)
| ~ environment(X0)
| ~ 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] :
( ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| ~ greater(growth_rate(efficient_producers,sk4(X0)),zero)
| ~ in_environment(sk3,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_40) ).
fof(f28,plain,
! [X1] : greater_or_equal(X1,X1),
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,
subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3))),
inference(resolution,[],[f30,f25]) ).
fof(f32,plain,
greater_or_equal(sk4(sk1(sk3)),sk1(sk3)),
inference(resolution,[],[f30,f26]) ).
fof(f33,plain,
( ~ environment(sk3)
| in_environment(sk3,sk2(sk3)) ),
inference(resolution,[],[f21,f24]) ).
fof(f34,plain,
in_environment(sk3,sk2(sk3)),
inference(forward_subsumption_resolution,[],[f33,f23]) ).
fof(f35,plain,
subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3))),
inference(resolution,[],[f34,f25]) ).
fof(f36,plain,
greater_or_equal(sk4(sk2(sk3)),sk2(sk3)),
inference(resolution,[],[f34,f26]) ).
fof(f37,plain,
( ~ environment(sk3)
| greater_or_equal(sk2(sk3),equilibrium(sk3)) ),
inference(resolution,[],[f22,f24]) ).
fof(f38,plain,
greater_or_equal(sk2(sk3),equilibrium(sk3)),
inference(forward_subsumption_resolution,[],[f37,f23]) ).
fof(f40,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| sk1(sk3) = sk4(sk1(sk3)) ),
inference(resolution,[],[f4,f32]) ).
fof(f41,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| sk2(sk3) = sk4(sk2(sk3)) ),
inference(resolution,[],[f4,f36]) ).
fof(f42,plain,
( greater(sk2(sk3),equilibrium(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[],[f4,f38]) ).
fof(f44,definition,
( spl0_1
<=> sk2(sk3) = equilibrium(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f46,plain,
( sk2(sk3) = equilibrium(sk3)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f44]) ).
fof(f48,definition,
( spl0_2
<=> greater(sk2(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f50,plain,
( greater(sk2(sk3),equilibrium(sk3))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f48]) ).
fof(f51,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f42,f48,f44]) ).
fof(f53,definition,
( spl0_3
<=> sk2(sk3) = sk4(sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f54,plain,
( sk2(sk3) != sk4(sk2(sk3))
| spl0_3 ),
inference(avatar_component_clause,[],[f53]) ).
fof(f55,plain,
( sk2(sk3) = sk4(sk2(sk3))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f53]) ).
fof(f57,definition,
( spl0_4
<=> greater(sk4(sk2(sk3)),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f59,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f57]) ).
fof(f60,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f41,f57,f53]) ).
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,[],[f40,f66,f62]) ).
fof(f70,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| ~ spl0_3 ),
inference(backward_demodulation,[],[f35,f55]) ).
fof(f72,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| ~ spl0_5 ),
inference(backward_demodulation,[],[f31,f64]) ).
fof(f74,plain,
( ! [X0] :
( ~ greater(X0,sk2(sk3))
| greater(X0,equilibrium(sk3)) )
| ~ spl0_2 ),
inference(resolution,[],[f50,f1]) ).
fof(f76,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ in_environment(sk3,sk2(sk3))
| ~ spl0_3 ),
inference(superposition,[],[f27,f55]) ).
fof(f77,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f76,f34]) ).
fof(f79,definition,
( spl0_7
<=> greater(growth_rate(efficient_producers,sk2(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f80,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f81,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| spl0_7 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f83,definition,
( spl0_8
<=> greater(zero,growth_rate(first_movers,sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f85,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| spl0_8 ),
inference(avatar_component_clause,[],[f83]) ).
fof(f86,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f77,f53,f83,f79]) ).
fof(f87,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ in_environment(sk3,sk1(sk3))
| ~ spl0_5 ),
inference(superposition,[],[f27,f64]) ).
fof(f88,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f87,f30]) ).
fof(f90,definition,
( spl0_9
<=> greater(growth_rate(efficient_producers,sk1(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f91,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f90]) ).
fof(f92,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| spl0_9 ),
inference(avatar_component_clause,[],[f90]) ).
fof(f94,definition,
( spl0_10
<=> greater(zero,growth_rate(first_movers,sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f96,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| spl0_10 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f97,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f88,f62,f94,f90]) ).
fof(f98,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| greater(sk1(sk3),X0)
| sk1(sk3) = X0
| greater(X0,sk1(sk3)) ),
inference(resolution,[],[f3,f30]) ).
fof(f101,plain,
( greater(sk1(sk3),sk2(sk3))
| sk1(sk3) = sk2(sk3)
| greater(sk2(sk3),sk1(sk3)) ),
inference(resolution,[],[f98,f34]) ).
fof(f104,definition,
( spl0_11
<=> greater(sk2(sk3),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f105,plain,
( ~ greater(sk2(sk3),sk1(sk3))
| spl0_11 ),
inference(avatar_component_clause,[],[f104]) ).
fof(f106,plain,
( greater(sk2(sk3),sk1(sk3))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f104]) ).
fof(f108,definition,
( spl0_12
<=> sk1(sk3) = sk2(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f110,plain,
( sk1(sk3) = sk2(sk3)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f112,definition,
( spl0_13
<=> greater(sk1(sk3),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f114,plain,
( greater(sk1(sk3),sk2(sk3))
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,plain,
( spl0_11
| spl0_12
| spl0_13 ),
inference(avatar_split_clause,[],[f101,f112,f108,f104]) ).
fof(f116,plain,
( ! [X0] :
( ~ greater(X0,sk2(sk3))
| greater(X0,sk1(sk3)) )
| ~ spl0_11 ),
inference(resolution,[],[f106,f1]) ).
fof(f117,plain,
( greater_or_equal(sk2(sk3),sk1(sk3))
| ~ spl0_11 ),
inference(resolution,[],[f106,f5]) ).
fof(f123,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ greater_or_equal(sk1(sk3),sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(resolution,[],[f20,f72]) ).
fof(f124,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk1(sk3),sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f123,f24]) ).
fof(f126,plain,
( ~ greater_or_equal(sk1(sk3),sk1(sk3))
| greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f124,f23]) ).
fof(f128,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f126,f28]) ).
fof(f130,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(efficient_producers,sk1(sk3)))
| greater(X0,growth_rate(first_movers,sk1(sk3))) )
| ~ spl0_5 ),
inference(resolution,[],[f128,f1]) ).
fof(f136,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| zero = growth_rate(first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_3 ),
inference(resolution,[],[f7,f70]) ).
fof(f137,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk1(sk3),equilibrium(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_5 ),
inference(resolution,[],[f7,f72]) ).
fof(f138,plain,
( ~ greater_or_equal(sk1(sk3),equilibrium(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_5 ),
inference(forward_subsumption_resolution,[],[f137,f23]) ).
fof(f139,plain,
( ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| zero = growth_rate(first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f136,f23]) ).
fof(f140,plain,
( ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| ~ spl0_5
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f138,f92]) ).
fof(f141,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_3 ),
inference(forward_subsumption_resolution,[],[f139,f38]) ).
fof(f143,definition,
( spl0_14
<=> greater(growth_rate(first_movers,sk1(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f145,plain,
( greater(growth_rate(first_movers,sk1(sk3)),zero)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f147,definition,
( spl0_15
<=> zero = growth_rate(first_movers,sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f149,plain,
( zero = growth_rate(first_movers,sk1(sk3))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f151,definition,
( spl0_16
<=> greater_or_equal(sk1(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f152,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f153,plain,
( ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| spl0_16 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,plain,
( spl0_14
| spl0_15
| ~ spl0_16
| ~ spl0_5
| spl0_9 ),
inference(avatar_split_clause,[],[f140,f90,f62,f151,f147,f143]) ).
fof(f155,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| ~ spl0_3
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f141,f81]) ).
fof(f157,definition,
( spl0_17
<=> greater(growth_rate(first_movers,sk2(sk3)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f161,definition,
( spl0_18
<=> zero = growth_rate(first_movers,sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f162,plain,
( zero != growth_rate(first_movers,sk2(sk3))
| spl0_18 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f163,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f164,plain,
( spl0_17
| spl0_18
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f155,f79,f53,f161,f157]) ).
fof(f175,plain,
( greater(sk4(sk2(sk3)),sk1(sk3))
| ~ spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f59,f116]) ).
fof(f176,plain,
( greater(sk4(sk2(sk3)),equilibrium(sk3))
| ~ spl0_2
| ~ spl0_4 ),
inference(resolution,[],[f59,f74]) ).
fof(f180,plain,
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ spl0_2
| ~ spl0_4 ),
inference(resolution,[],[f176,f5]) ).
fof(f182,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f175,f5]) ).
fof(f186,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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) ),
inference(resolution,[],[f35,f7]) ).
fof(f187,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(resolution,[],[f35,f20]) ).
fof(f188,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f187,f24]) ).
fof(f189,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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) ),
inference(forward_subsumption_resolution,[],[f186,f23]) ).
fof(f191,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f188,f23]) ).
fof(f192,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_2
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f189,f180]) ).
fof(f194,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f191,f182]) ).
fof(f196,definition,
( spl0_19
<=> greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f197,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| spl0_19 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f198,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f200,definition,
( spl0_20
<=> greater(growth_rate(first_movers,sk4(sk2(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f201,plain,
( ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| spl0_20 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f202,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f204,definition,
( spl0_21
<=> zero = growth_rate(first_movers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f205,plain,
( zero != growth_rate(first_movers,sk4(sk2(sk3)))
| spl0_21 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f206,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f207,plain,
( spl0_19
| spl0_20
| spl0_21
| ~ spl0_2
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f192,f57,f48,f204,f200,f196]) ).
fof(f209,definition,
( spl0_22
<=> greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f210,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_22 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f211,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f213,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(X0,zero) )
| ~ spl0_19 ),
inference(resolution,[],[f198,f1]) ).
fof(f215,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ in_environment(sk3,sk2(sk3))
| ~ spl0_22 ),
inference(resolution,[],[f211,f27]) ).
fof(f218,plain,
( ~ in_environment(sk3,sk2(sk3))
| ~ spl0_19
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f215,f198]) ).
fof(f219,plain,
( $false
| ~ spl0_19
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f218,f34]) ).
fof(f220,plain,
( ~ spl0_19
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f219]) ).
fof(f221,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(X0,zero) )
| ~ spl0_20 ),
inference(resolution,[],[f202,f1]) ).
fof(f227,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_4
| ~ spl0_11
| ~ spl0_20 ),
inference(resolution,[],[f194,f221]) ).
fof(f228,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(X0,growth_rate(first_movers,sk4(sk2(sk3)))) )
| ~ spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f194,f1]) ).
fof(f231,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk1(sk3),equilibrium(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_5 ),
inference(resolution,[],[f10,f72]) ).
fof(f232,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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)))) ),
inference(resolution,[],[f10,f35]) ).
fof(f233,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f232,f228]) ).
fof(f234,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f233,f23]) ).
fof(f235,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_2
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f234,f180]) ).
fof(f236,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| ~ spl0_2
| ~ spl0_4
| ~ spl0_11
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f235,f210]) ).
fof(f237,plain,
( spl0_21
| ~ spl0_2
| ~ spl0_4
| ~ spl0_11
| spl0_22 ),
inference(avatar_split_clause,[],[f236,f209,f104,f57,f48,f204]) ).
fof(f241,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| ~ spl0_12 ),
inference(backward_demodulation,[],[f38,f110]) ).
fof(f243,plain,
( sk1(sk3) != sk4(sk1(sk3))
| spl0_3
| ~ spl0_12 ),
inference(backward_demodulation,[],[f54,f110]) ).
fof(f263,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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)))) ),
inference(forward_subsumption_resolution,[],[f232,f23]) ).
fof(f279,plain,
( $false
| spl0_3
| ~ spl0_5
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f243,f64]) ).
fof(f280,plain,
( spl0_3
| ~ spl0_5
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f279]) ).
fof(f281,plain,
( $false
| ~ spl0_12
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f241,f153]) ).
fof(f282,plain,
( ~ spl0_12
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f281]) ).
fof(f302,definition,
( spl0_23
<=> greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f303,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_23 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f304,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f306,definition,
( spl0_24
<=> greater_or_equal(sk4(sk2(sk3)),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f307,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f313,definition,
( spl0_25
<=> greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f314,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| spl0_25 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f315,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f324,plain,
( ! [X0] :
( ~ greater(X0,sk1(sk3))
| greater(X0,sk2(sk3)) )
| ~ spl0_13 ),
inference(resolution,[],[f114,f1]) ).
fof(f336,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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)))) ),
inference(resolution,[],[f35,f10]) ).
fof(f339,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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) ),
inference(resolution,[],[f35,f7]) ).
fof(f340,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(resolution,[],[f35,f20]) ).
fof(f350,plain,
( greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_2
| ~ spl0_13 ),
inference(resolution,[],[f74,f114]) ).
fof(f353,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| ~ spl0_2
| ~ spl0_13 ),
inference(resolution,[],[f350,f5]) ).
fof(f357,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f231,f130]) ).
fof(f359,plain,
( ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| zero = growth_rate(first_movers,sk1(sk3))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f357,f23]) ).
fof(f361,plain,
( zero = growth_rate(first_movers,sk1(sk3))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f359,f152]) ).
fof(f363,plain,
( zero = growth_rate(first_movers,sk1(sk3))
| ~ spl0_5
| spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f361,f96]) ).
fof(f364,plain,
( spl0_15
| ~ spl0_5
| spl0_10
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f363,f151,f94,f62,f147]) ).
fof(f373,plain,
( ~ greater(zero,zero)
| spl0_10
| ~ spl0_15 ),
inference(backward_demodulation,[],[f96,f149]) ).
fof(f377,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| ~ spl0_5
| ~ spl0_15 ),
inference(backward_demodulation,[],[f128,f149]) ).
fof(f378,plain,
( spl0_9
| ~ spl0_5
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f377,f147,f62,f90]) ).
fof(f382,plain,
( greater(sk1(sk3),equilibrium(sk3))
| sk1(sk3) = equilibrium(sk3)
| ~ spl0_16 ),
inference(resolution,[],[f152,f4]) ).
fof(f386,plain,
( greater(zero,zero)
| ~ spl0_19
| ~ spl0_25 ),
inference(resolution,[],[f213,f315]) ).
fof(f399,plain,
( greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_1
| ~ spl0_13 ),
inference(backward_demodulation,[],[f114,f46]) ).
fof(f405,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_1
| spl0_22 ),
inference(backward_demodulation,[],[f210,f46]) ).
fof(f416,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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)))) ),
inference(forward_subsumption_resolution,[],[f336,f23]) ).
fof(f421,definition,
( spl0_27
<=> sk1(sk3) = equilibrium(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f423,plain,
( sk1(sk3) = equilibrium(sk3)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f425,definition,
( spl0_28
<=> greater(sk1(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f427,plain,
( greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f428,plain,
( spl0_27
| spl0_28
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f382,f151,f425,f421]) ).
fof(f430,plain,
( spl0_28
| ~ spl0_1
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f399,f112,f44,f425]) ).
fof(f465,plain,
( spl0_28
| ~ spl0_2
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f350,f112,f48,f425]) ).
fof(f479,plain,
( ~ greater(sk2(sk3),equilibrium(sk3))
| spl0_11
| ~ spl0_27 ),
inference(forward_demodulation,[],[f105,f423]) ).
fof(f487,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(first_movers,sk2(sk3)))
| greater(X0,zero) )
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f221,f55]) ).
fof(f492,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| ~ spl0_3
| spl0_25 ),
inference(forward_demodulation,[],[f314,f55]) ).
fof(f497,plain,
( ~ greater_or_equal(sk2(sk3),equilibrium(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_3 ),
inference(forward_demodulation,[],[f416,f55]) ).
fof(f499,plain,
( $false
| ~ spl0_2
| spl0_11
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f479,f50]) ).
fof(f500,plain,
( ~ spl0_2
| spl0_11
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f499]) ).
fof(f510,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_3 ),
inference(forward_subsumption_resolution,[],[f497,f38]) ).
fof(f520,plain,
( zero = growth_rate(first_movers,sk2(sk3))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f510,f55]) ).
fof(f526,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f520,f162]) ).
fof(f531,plain,
( greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| spl0_18 ),
inference(forward_demodulation,[],[f526,f55]) ).
fof(f534,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| spl0_18
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f531,f492]) ).
fof(f537,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_3
| spl0_18
| spl0_25 ),
inference(forward_demodulation,[],[f534,f55]) ).
fof(f540,plain,
( $false
| ~ spl0_3
| spl0_8
| spl0_18
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f537,f85]) ).
fof(f541,plain,
( ~ spl0_3
| spl0_8
| spl0_18
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f540]) ).
fof(f548,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_3
| spl0_19 ),
inference(forward_demodulation,[],[f197,f55]) ).
fof(f549,plain,
( greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| ~ spl0_3
| ~ spl0_25 ),
inference(forward_demodulation,[],[f315,f55]) ).
fof(f571,plain,
( ! [X0] :
( ~ greater(X0,sk2(sk3))
| greater(X0,equilibrium(sk3)) )
| ~ spl0_2 ),
inference(resolution,[],[f50,f1]) ).
fof(f577,plain,
( ! [X0] :
( ~ greater(X0,sk1(sk3))
| greater(X0,equilibrium(sk3)) )
| ~ spl0_28 ),
inference(resolution,[],[f427,f1]) ).
fof(f578,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| ~ spl0_28 ),
inference(resolution,[],[f427,f5]) ).
fof(f646,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(resolution,[],[f14,f72]) ).
fof(f647,plain,
( ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f646,f23]) ).
fof(f648,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f647,f152]) ).
fof(f649,plain,
( greater(zero,zero)
| zero = growth_rate(efficient_producers,sk1(sk3))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f648,f149]) ).
fof(f650,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ spl0_5
| spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f649,f373]) ).
fof(f651,plain,
( greater(zero,zero)
| zero = growth_rate(efficient_producers,sk1(sk3))
| ~ spl0_5
| spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f650,f149]) ).
fof(f652,plain,
( zero = growth_rate(efficient_producers,sk1(sk3))
| ~ spl0_5
| spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f651,f373]) ).
fof(f655,plain,
( greater(zero,zero)
| ~ spl0_5
| ~ spl0_9
| spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(backward_demodulation,[],[f91,f652]) ).
fof(f656,plain,
( $false
| ~ spl0_5
| ~ spl0_9
| spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f655,f373]) ).
fof(f657,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f656]) ).
fof(f659,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_6
| ~ spl0_28 ),
inference(resolution,[],[f68,f577]) ).
fof(f660,plain,
( greater(sk4(sk1(sk3)),sk2(sk3))
| ~ spl0_6
| ~ spl0_13 ),
inference(resolution,[],[f68,f324]) ).
fof(f683,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_6
| ~ spl0_28 ),
inference(resolution,[],[f659,f5]) ).
fof(f686,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(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) ),
inference(resolution,[],[f31,f7]) ).
fof(f689,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f31,f10]) ).
fof(f691,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f31,f14]) ).
fof(f692,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ greater_or_equal(sk4(sk1(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f31,f20]) ).
fof(f693,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk1(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(forward_subsumption_resolution,[],[f692,f24]) ).
fof(f694,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(forward_subsumption_resolution,[],[f691,f23]) ).
fof(f696,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(forward_subsumption_resolution,[],[f689,f23]) ).
fof(f699,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(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) ),
inference(forward_subsumption_resolution,[],[f686,f23]) ).
fof(f700,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(forward_subsumption_resolution,[],[f693,f23]) ).
fof(f706,plain,
( 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_28 ),
inference(forward_subsumption_resolution,[],[f699,f683]) ).
fof(f707,plain,
greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))),
inference(forward_subsumption_resolution,[],[f700,f32]) ).
fof(f709,definition,
( spl0_35
<=> greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f710,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_35 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f711,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f713,definition,
( spl0_36
<=> greater(growth_rate(first_movers,sk4(sk1(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f714,plain,
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| spl0_36 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f715,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f717,definition,
( spl0_37
<=> zero = growth_rate(efficient_producers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f718,plain,
( zero != growth_rate(efficient_producers,sk4(sk1(sk3)))
| spl0_37 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f719,plain,
( zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f722,definition,
( spl0_38
<=> greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f723,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| spl0_38 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f724,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f727,definition,
( spl0_39
<=> greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f728,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| spl0_39 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f729,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f731,definition,
( spl0_40
<=> zero = growth_rate(first_movers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f732,plain,
( zero != growth_rate(first_movers,sk4(sk1(sk3)))
| spl0_40 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f733,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f737,plain,
( spl0_38
| spl0_36
| spl0_40
| ~ spl0_6
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f706,f425,f66,f731,f713,f722]) ).
fof(f738,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ in_environment(sk3,sk1(sk3))
| ~ spl0_35 ),
inference(resolution,[],[f711,f27]) ).
fof(f742,plain,
( ~ in_environment(sk3,sk1(sk3))
| ~ spl0_35
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f738,f724]) ).
fof(f743,plain,
( $false
| ~ spl0_35
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f742,f30]) ).
fof(f744,plain,
( ~ spl0_35
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f743]) ).
fof(f745,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ~ spl0_3
| ~ spl0_23 ),
inference(forward_demodulation,[],[f304,f55]) ).
fof(f749,plain,
( greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3))
| ~ spl0_27 ),
inference(backward_demodulation,[],[f32,f423]) ).
fof(f767,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_27
| spl0_35 ),
inference(forward_demodulation,[],[f710,f423]) ).
fof(f768,plain,
( ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f694,f423]) ).
fof(f770,plain,
( ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f696,f423]) ).
fof(f774,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f340,f24]) ).
fof(f783,plain,
( zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f768,f749]) ).
fof(f785,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f770,f749]) ).
fof(f789,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f774,f23]) ).
fof(f793,plain,
( zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f783,f423]) ).
fof(f795,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f785,f423]) ).
fof(f802,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f793,f423]) ).
fof(f804,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f795,f423]) ).
fof(f811,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f802,f423]) ).
fof(f813,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f804,f423]) ).
fof(f820,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| ~ spl0_27
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f811,f767]) ).
fof(f821,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ spl0_27
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f813,f767]) ).
fof(f825,definition,
( spl0_41
<=> zero = growth_rate(efficient_producers,sk4(equilibrium(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f826,plain,
( zero != growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| spl0_41 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f827,plain,
( zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f829,definition,
( spl0_42
<=> greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f830,plain,
( ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| spl0_42 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f831,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f832,plain,
( spl0_41
| spl0_42
| ~ spl0_27
| spl0_35 ),
inference(avatar_split_clause,[],[f820,f709,f421,f829,f825]) ).
fof(f834,definition,
( spl0_43
<=> zero = growth_rate(first_movers,sk4(equilibrium(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f835,plain,
( zero != growth_rate(first_movers,sk4(equilibrium(sk3)))
| spl0_43 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f836,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f838,definition,
( spl0_44
<=> greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f840,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f838]) ).
fof(f841,plain,
( spl0_43
| spl0_44
| ~ spl0_27
| spl0_35 ),
inference(avatar_split_clause,[],[f821,f709,f421,f838,f834]) ).
fof(f851,plain,
( spl0_16
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f578,f425,f151]) ).
fof(f852,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f707,f733]) ).
fof(f853,plain,
( greater(zero,zero)
| ~ spl0_37
| ~ spl0_38 ),
inference(forward_demodulation,[],[f724,f719]) ).
fof(f854,plain,
( ~ greater(zero,zero)
| spl0_35
| ~ spl0_40 ),
inference(forward_demodulation,[],[f710,f733]) ).
fof(f855,plain,
( ~ greater_or_equal(sk2(sk3),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f789,f55]) ).
fof(f859,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f855,f117]) ).
fof(f862,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ~ spl0_3
| ~ spl0_11 ),
inference(forward_demodulation,[],[f859,f55]) ).
fof(f884,plain,
( ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_27
| spl0_38 ),
inference(forward_demodulation,[],[f723,f423]) ).
fof(f886,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_27 ),
inference(forward_demodulation,[],[f707,f423]) ).
fof(f899,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_27
| ~ spl0_43 ),
inference(forward_demodulation,[],[f886,f836]) ).
fof(f907,plain,
( $false
| ~ spl0_27
| spl0_38
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f899,f884]) ).
fof(f908,plain,
( ~ spl0_27
| spl0_38
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f907]) ).
fof(f915,plain,
( zero != growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| ~ spl0_27
| spl0_37 ),
inference(forward_demodulation,[],[f718,f423]) ).
fof(f952,plain,
( zero != growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ spl0_27
| spl0_40 ),
inference(forward_demodulation,[],[f732,f423]) ).
fof(f984,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_3
| ~ spl0_20
| ~ spl0_23 ),
inference(resolution,[],[f745,f487]) ).
fof(f991,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ~ spl0_3
| spl0_23 ),
inference(forward_demodulation,[],[f303,f55]) ).
fof(f994,plain,
( spl0_38
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f852,f731,f722]) ).
fof(f1000,plain,
( $false
| ~ spl0_3
| ~ spl0_11
| spl0_23 ),
inference(forward_subsumption_resolution,[],[f991,f862]) ).
fof(f1001,plain,
( ~ spl0_3
| ~ spl0_11
| spl0_23 ),
inference(avatar_contradiction_clause,[],[f1000]) ).
fof(f1104,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(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) ),
inference(resolution,[],[f31,f7]) ).
fof(f1112,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(X0,zero) )
| ~ spl0_36 ),
inference(resolution,[],[f715,f1]) ).
fof(f1122,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_2
| ~ spl0_6
| ~ spl0_13 ),
inference(resolution,[],[f571,f660]) ).
fof(f1137,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_36 ),
inference(resolution,[],[f707,f1112]) ).
fof(f1138,plain,
! [X0] :
( ~ greater(X0,growth_rate(efficient_producers,sk4(sk1(sk3))))
| greater(X0,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f707,f1]) ).
fof(f1146,plain,
( greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3))
| ~ spl0_27 ),
inference(backward_demodulation,[],[f32,f423]) ).
fof(f1172,plain,
( ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ spl0_27
| spl0_36 ),
inference(forward_demodulation,[],[f714,f423]) ).
fof(f1184,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(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) ),
inference(forward_subsumption_resolution,[],[f1104,f23]) ).
fof(f1192,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f548,f80]) ).
fof(f1193,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f1192]) ).
fof(f1206,plain,
( $false
| ~ spl0_27
| spl0_36
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f1172,f831]) ).
fof(f1207,plain,
( ~ spl0_27
| spl0_36
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f1206]) ).
fof(f1215,plain,
( ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(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_27 ),
inference(forward_demodulation,[],[f1184,f423]) ).
fof(f1230,plain,
( 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_27 ),
inference(forward_subsumption_resolution,[],[f1215,f1146]) ).
fof(f1241,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_27 ),
inference(forward_demodulation,[],[f1230,f423]) ).
fof(f1247,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_27
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1241,f835]) ).
fof(f1251,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_27
| spl0_43 ),
inference(forward_demodulation,[],[f1247,f423]) ).
fof(f1252,plain,
( ~ greater(growth_rate(first_movers,sk2(sk3)),zero)
| ~ spl0_3
| spl0_20 ),
inference(forward_demodulation,[],[f201,f55]) ).
fof(f1256,plain,
( ~ spl0_41
| ~ spl0_27
| spl0_37 ),
inference(avatar_split_clause,[],[f915,f717,f421,f825]) ).
fof(f1260,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_27
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1251,f830]) ).
fof(f1266,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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) ),
inference(forward_subsumption_resolution,[],[f339,f23]) ).
fof(f1273,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_27
| spl0_42
| spl0_43 ),
inference(forward_demodulation,[],[f1260,f423]) ).
fof(f1282,plain,
( $false
| ~ spl0_27
| spl0_38
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1273,f884]) ).
fof(f1283,plain,
( ~ spl0_27
| spl0_38
| spl0_42
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f1282]) ).
fof(f1312,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f855,f117]) ).
fof(f1326,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ~ spl0_3
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1312,f55]) ).
fof(f1335,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| ~ spl0_3
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1326,f163]) ).
fof(f1373,plain,
( greater_or_equal(sk4(equilibrium(sk3)),sk1(sk3))
| ~ spl0_1
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_demodulation,[],[f182,f46]) ).
fof(f1379,plain,
( greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f36,f46]) ).
fof(f1386,plain,
( ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_1
| spl0_19 ),
inference(forward_demodulation,[],[f197,f46]) ).
fof(f1390,plain,
( ~ greater_or_equal(sk4(equilibrium(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f789,f46]) ).
fof(f1393,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_demodulation,[],[f304,f46]) ).
fof(f1395,plain,
( ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| ~ spl0_1
| spl0_20 ),
inference(forward_demodulation,[],[f201,f46]) ).
fof(f1396,plain,
( ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(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_1 ),
inference(forward_demodulation,[],[f1266,f46]) ).
fof(f1406,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_1
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1390,f1373]) ).
fof(f1407,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_1 ),
inference(forward_subsumption_resolution,[],[f1396,f1379]) ).
fof(f1416,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_1
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1406,f46]) ).
fof(f1417,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1407,f46]) ).
fof(f1425,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_1
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1417,f835]) ).
fof(f1433,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_1
| spl0_43 ),
inference(forward_demodulation,[],[f1425,f46]) ).
fof(f1437,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_1
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1433,f830]) ).
fof(f1441,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_1
| spl0_42
| spl0_43 ),
inference(forward_demodulation,[],[f1437,f46]) ).
fof(f1447,plain,
( $false
| ~ spl0_1
| spl0_19
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1441,f1386]) ).
fof(f1448,plain,
( ~ spl0_1
| spl0_19
| spl0_42
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f1447]) ).
fof(f1481,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_1
| ~ spl0_4
| ~ spl0_11
| ~ spl0_43 ),
inference(forward_demodulation,[],[f1416,f836]) ).
fof(f1485,plain,
( $false
| ~ spl0_1
| ~ spl0_4
| ~ spl0_11
| spl0_19
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f1481,f1386]) ).
fof(f1486,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_11
| spl0_19
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f1485]) ).
fof(f1487,plain,
( spl0_24
| ~ spl0_4
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f182,f104,f57,f306]) ).
fof(f1488,plain,
( ~ greater(zero,zero)
| ~ spl0_21
| spl0_22 ),
inference(forward_demodulation,[],[f210,f206]) ).
fof(f1489,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ spl0_21 ),
inference(forward_demodulation,[],[f789,f206]) ).
fof(f1493,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| spl0_19
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1489,f197]) ).
fof(f1496,plain,
( $false
| spl0_19
| ~ spl0_21
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1493,f307]) ).
fof(f1497,plain,
( spl0_19
| ~ spl0_21
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1496]) ).
fof(f1531,plain,
( spl0_16
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f241,f108,f151]) ).
fof(f1562,plain,
( ~ spl0_43
| ~ spl0_27
| spl0_40 ),
inference(avatar_split_clause,[],[f952,f731,f421,f834]) ).
fof(f1569,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_27
| spl0_39 ),
inference(forward_demodulation,[],[f728,f423]) ).
fof(f1609,plain,
( $false
| ~ spl0_27
| spl0_39
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f1569,f840]) ).
fof(f1610,plain,
( ~ spl0_27
| spl0_39
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f1609]) ).
fof(f1685,plain,
( spl0_16
| ~ spl0_2
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f353,f112,f48,f151]) ).
fof(f1687,plain,
( spl0_38
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f1137,f713,f722]) ).
fof(f1737,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_2
| ~ spl0_6
| ~ spl0_13 ),
inference(resolution,[],[f1122,f5]) ).
fof(f1746,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(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)))) ),
inference(resolution,[],[f31,f18]) ).
fof(f1755,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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)))) ),
inference(resolution,[],[f35,f18]) ).
fof(f1756,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(resolution,[],[f35,f20]) ).
fof(f1885,definition,
( spl0_46
<=> greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f1886,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f1885]) ).
fof(f1887,plain,
( ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| spl0_46 ),
inference(avatar_component_clause,[],[f1885]) ).
fof(f2077,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_39 ),
inference(resolution,[],[f1138,f729]) ).
fof(f2078,plain,
( $false
| spl0_35
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f2077,f710]) ).
fof(f2079,plain,
( spl0_35
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f2078]) ).
fof(f2082,plain,
( greater(zero,zero)
| ~ spl0_36
| ~ spl0_40 ),
inference(backward_demodulation,[],[f715,f733]) ).
fof(f2105,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(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)))) ),
inference(forward_subsumption_resolution,[],[f1746,f23]) ).
fof(f2110,plain,
( $false
| spl0_35
| ~ spl0_36
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f2082,f854]) ).
fof(f2111,plain,
( spl0_35
| ~ spl0_36
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f2110]) ).
fof(f2121,plain,
( greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3))
| ~ spl0_1 ),
inference(backward_demodulation,[],[f36,f46]) ).
fof(f2163,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| ~ spl0_1
| ~ spl0_19 ),
inference(forward_demodulation,[],[f198,f46]) ).
fof(f2176,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| zero = growth_rate(first_movers,sk4(sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(forward_subsumption_resolution,[],[f696,f1138]) ).
fof(f2188,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(forward_subsumption_resolution,[],[f2105,f1138]) ).
fof(f2189,plain,
( ~ environment(sk3)
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f1756,f24]) ).
fof(f2190,plain,
( ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(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_1 ),
inference(forward_demodulation,[],[f263,f46]) ).
fof(f2207,plain,
( $false
| ~ spl0_1
| ~ spl0_19
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f2163,f1887]) ).
fof(f2208,plain,
( ~ spl0_1
| ~ spl0_19
| spl0_46 ),
inference(avatar_contradiction_clause,[],[f2207]) ).
fof(f2211,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f2176,f732]) ).
fof(f2221,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f2188,f718]) ).
fof(f2222,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f2189,f23]) ).
fof(f2223,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_1 ),
inference(forward_subsumption_resolution,[],[f2190,f2121]) ).
fof(f2230,definition,
( spl0_50
<=> greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f2232,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| spl0_50 ),
inference(avatar_component_clause,[],[f2230]) ).
fof(f2235,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| spl0_35
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f2211,f710]) ).
fof(f2242,plain,
( ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| spl0_35
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f2221,f710]) ).
fof(f2244,plain,
( zero = growth_rate(first_movers,sk4(equilibrium(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f2223,f46]) ).
fof(f2249,plain,
( ~ spl0_50
| spl0_35
| spl0_40 ),
inference(avatar_split_clause,[],[f2235,f731,f709,f2230]) ).
fof(f2253,plain,
( ~ spl0_50
| spl0_35
| spl0_37 ),
inference(avatar_split_clause,[],[f2242,f717,f709,f2230]) ).
fof(f2255,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_1
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f2244,f835]) ).
fof(f2261,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_1
| spl0_43 ),
inference(forward_demodulation,[],[f2255,f46]) ).
fof(f2266,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_1
| spl0_43 ),
inference(forward_demodulation,[],[f2261,f46]) ).
fof(f2280,plain,
( ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(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)))) ),
inference(forward_subsumption_resolution,[],[f1755,f23]) ).
fof(f2284,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_1
| spl0_22
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f2266,f405]) ).
fof(f2288,plain,
( ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(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_1 ),
inference(forward_demodulation,[],[f2280,f46]) ).
fof(f2292,plain,
( spl0_44
| ~ spl0_1
| spl0_22
| spl0_43 ),
inference(avatar_split_clause,[],[f2284,f834,f209,f44,f838]) ).
fof(f2295,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_1 ),
inference(forward_subsumption_resolution,[],[f2288,f2121]) ).
fof(f2301,plain,
( zero = growth_rate(efficient_producers,sk4(equilibrium(sk3)))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f2295,f46]) ).
fof(f2307,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_1
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f2301,f826]) ).
fof(f2313,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_1
| spl0_41 ),
inference(forward_demodulation,[],[f2307,f46]) ).
fof(f2317,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_1
| spl0_41 ),
inference(forward_demodulation,[],[f2313,f46]) ).
fof(f2321,plain,
( greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| ~ spl0_1
| spl0_22
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f2317,f405]) ).
fof(f2323,plain,
( spl0_44
| ~ spl0_1
| spl0_22
| spl0_41 ),
inference(avatar_split_clause,[],[f2321,f825,f209,f44,f838]) ).
fof(f2372,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| greater(X0,growth_rate(first_movers,sk4(equilibrium(sk3)))) )
| ~ spl0_1
| ~ spl0_23 ),
inference(resolution,[],[f1393,f1]) ).
fof(f2417,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ spl0_1
| ~ spl0_23
| ~ spl0_44 ),
inference(resolution,[],[f2372,f840]) ).
fof(f2418,plain,
( $false
| ~ spl0_1
| spl0_22
| ~ spl0_23
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f2417,f405]) ).
fof(f2419,plain,
( ~ spl0_1
| spl0_22
| ~ spl0_23
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f2418]) ).
fof(f2433,plain,
( spl0_19
| ~ spl0_4
| ~ spl0_11
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f227,f200,f104,f57,f196]) ).
fof(f2434,plain,
( ~ greater(zero,zero)
| ~ spl0_21
| spl0_22 ),
inference(forward_demodulation,[],[f210,f206]) ).
fof(f2439,plain,
( $false
| ~ spl0_19
| ~ spl0_21
| spl0_22
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2434,f386]) ).
fof(f2440,plain,
( ~ spl0_19
| ~ spl0_21
| spl0_22
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f2439]) ).
fof(f2462,plain,
( spl0_7
| ~ spl0_3
| ~ spl0_20
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f984,f302,f200,f53,f79]) ).
fof(f2465,plain,
( spl0_7
| ~ spl0_3
| ~ spl0_11
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f1335,f161,f104,f53,f79]) ).
fof(f2474,plain,
( zero != growth_rate(first_movers,sk2(sk3))
| ~ spl0_3
| spl0_21 ),
inference(forward_demodulation,[],[f205,f55]) ).
fof(f2500,plain,
( $false
| ~ spl0_3
| ~ spl0_18
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f2474,f163]) ).
fof(f2501,plain,
( ~ spl0_3
| ~ spl0_18
| spl0_21 ),
inference(avatar_contradiction_clause,[],[f2500]) ).
fof(f2589,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(efficient_producers,sk2(sk3)))
| greater(X0,growth_rate(first_movers,sk2(sk3))) )
| ~ spl0_3
| ~ spl0_23 ),
inference(resolution,[],[f745,f1]) ).
fof(f2624,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ spl0_3
| ~ spl0_23
| ~ spl0_25 ),
inference(resolution,[],[f2589,f549]) ).
fof(f2625,plain,
( $false
| ~ spl0_3
| spl0_8
| ~ spl0_23
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2624,f85]) ).
fof(f2626,plain,
( ~ spl0_3
| spl0_8
| ~ spl0_23
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f2625]) ).
fof(f2651,plain,
( ~ spl0_42
| ~ spl0_1
| spl0_20 ),
inference(avatar_split_clause,[],[f1395,f200,f44,f829]) ).
fof(f2661,plain,
( greater(zero,zero)
| ~ spl0_41
| ~ spl0_46 ),
inference(backward_demodulation,[],[f1886,f827]) ).
fof(f2690,plain,
( zero != growth_rate(first_movers,sk4(equilibrium(sk3)))
| ~ spl0_1
| spl0_21 ),
inference(forward_demodulation,[],[f205,f46]) ).
fof(f2737,plain,
( $false
| ~ spl0_1
| spl0_21
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f2690,f836]) ).
fof(f2738,plain,
( ~ spl0_1
| spl0_21
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f2737]) ).
fof(f2790,plain,
( $false
| ~ spl0_21
| spl0_22
| ~ spl0_41
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f2661,f1488]) ).
fof(f2791,plain,
( ~ spl0_21
| spl0_22
| ~ spl0_41
| ~ spl0_46 ),
inference(avatar_contradiction_clause,[],[f2790]) ).
fof(f2826,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_2
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2280,f180]) ).
fof(f2838,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_2
| ~ spl0_4
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f2826,f314]) ).
fof(f2840,plain,
( greater(zero,zero)
| zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| ~ spl0_2
| ~ spl0_4
| ~ spl0_21
| spl0_25 ),
inference(forward_demodulation,[],[f2838,f206]) ).
fof(f2842,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| ~ spl0_2
| ~ spl0_4
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f2840,f1488]) ).
fof(f2845,plain,
( greater(zero,zero)
| ~ spl0_2
| ~ spl0_4
| ~ spl0_19
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(backward_demodulation,[],[f198,f2842]) ).
fof(f2847,plain,
( $false
| ~ spl0_2
| ~ spl0_4
| ~ spl0_19
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f2845,f1488]) ).
fof(f2848,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_19
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f2847]) ).
fof(f2853,plain,
( ~ spl0_17
| ~ spl0_3
| spl0_20 ),
inference(avatar_split_clause,[],[f1252,f200,f53,f157]) ).
fof(f2869,plain,
( ~ greater_or_equal(sk2(sk3),equilibrium(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_3 ),
inference(forward_demodulation,[],[f2280,f55]) ).
fof(f2882,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_3 ),
inference(forward_subsumption_resolution,[],[f2869,f38]) ).
fof(f2892,plain,
( zero = growth_rate(efficient_producers,sk2(sk3))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f2882,f55]) ).
fof(f2895,plain,
( greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| zero = growth_rate(efficient_producers,sk2(sk3))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f2892,f55]) ).
fof(f2897,plain,
( zero = growth_rate(efficient_producers,sk2(sk3))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f2895,f492]) ).
fof(f2899,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| zero = growth_rate(efficient_producers,sk2(sk3))
| ~ spl0_3
| spl0_25 ),
inference(forward_demodulation,[],[f2897,f55]) ).
fof(f2901,plain,
( greater(zero,zero)
| zero = growth_rate(efficient_producers,sk2(sk3))
| ~ spl0_3
| ~ spl0_18
| spl0_25 ),
inference(forward_demodulation,[],[f2899,f163]) ).
fof(f2903,plain,
( zero = growth_rate(efficient_producers,sk2(sk3))
| ~ spl0_3
| ~ spl0_18
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f2901,f1488]) ).
fof(f2908,plain,
( greater(zero,zero)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_18
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(backward_demodulation,[],[f80,f2903]) ).
fof(f2909,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_18
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f2908,f1488]) ).
fof(f2910,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_18
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f2909]) ).
fof(f2915,plain,
( ~ greater(growth_rate(first_movers,sk1(sk3)),zero)
| ~ spl0_5
| spl0_36 ),
inference(backward_demodulation,[],[f714,f64]) ).
fof(f2924,plain,
( ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| ~ spl0_5
| spl0_50 ),
inference(backward_demodulation,[],[f2232,f64]) ).
fof(f2929,plain,
( spl0_23
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f2222,f306,f302]) ).
fof(f2934,plain,
( $false
| ~ spl0_5
| ~ spl0_16
| spl0_50 ),
inference(forward_subsumption_resolution,[],[f2924,f152]) ).
fof(f2935,plain,
( ~ spl0_5
| ~ spl0_16
| spl0_50 ),
inference(avatar_contradiction_clause,[],[f2934]) ).
fof(f2941,plain,
( $false
| ~ spl0_5
| ~ spl0_14
| spl0_36 ),
inference(forward_subsumption_resolution,[],[f2915,f145]) ).
fof(f2942,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_36 ),
inference(avatar_contradiction_clause,[],[f2941]) ).
fof(f2947,plain,
( spl0_50
| ~ spl0_2
| ~ spl0_6
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1737,f112,f66,f48,f2230]) ).
fof(f2948,plain,
( spl0_50
| ~ spl0_6
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f683,f425,f66,f2230]) ).
fof(f2958,plain,
( ~ greater(zero,zero)
| spl0_35
| ~ spl0_40 ),
inference(forward_demodulation,[],[f710,f733]) ).
fof(f3051,plain,
( $false
| spl0_35
| ~ spl0_37
| ~ spl0_38
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f2958,f853]) ).
fof(f3052,plain,
( spl0_35
| ~ spl0_37
| ~ spl0_38
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f3051]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f51]) ).
cnf(s2,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f60]) ).
cnf(s3,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f69]) ).
cnf(s4,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f86]) ).
cnf(s5,plain,
( ~ spl0_5
| ~ spl0_9
| ~ spl0_10 ),
inference(sat_conversion,[],[f97]) ).
cnf(s6,plain,
( spl0_11
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f115]) ).
cnf(s7,plain,
( ~ spl0_5
| spl0_9
| spl0_14
| spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f154]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_7
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f164]) ).
cnf(s10,plain,
( ~ spl0_2
| ~ spl0_4
| spl0_19
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f207]) ).
cnf(s12,plain,
( ~ spl0_19
| ~ spl0_22 ),
inference(sat_conversion,[],[f220]) ).
cnf(s13,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_11
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f237]) ).
cnf(s15,plain,
( spl0_3
| ~ spl0_5
| ~ spl0_12 ),
inference(sat_conversion,[],[f280]) ).
cnf(s16,plain,
( ~ spl0_12
| spl0_16 ),
inference(sat_conversion,[],[f282]) ).
cnf(s26,plain,
( ~ spl0_5
| spl0_10
| spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f364]) ).
cnf(s29,plain,
( ~ spl0_5
| spl0_9
| ~ spl0_15 ),
inference(sat_conversion,[],[f378]) ).
cnf(s32,plain,
( ~ spl0_16
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f428]) ).
cnf(s33,plain,
( ~ spl0_1
| ~ spl0_13
| spl0_28 ),
inference(sat_conversion,[],[f430]) ).
cnf(s36,plain,
( ~ spl0_2
| ~ spl0_13
| spl0_28 ),
inference(sat_conversion,[],[f465]) ).
cnf(s37,plain,
( ~ spl0_2
| spl0_11
| ~ spl0_27 ),
inference(sat_conversion,[],[f500]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_8
| spl0_18
| spl0_25 ),
inference(sat_conversion,[],[f541]) ).
cnf(s48,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_10
| ~ spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f657]) ).
cnf(s55,plain,
( ~ spl0_6
| ~ spl0_28
| spl0_36
| spl0_38
| spl0_40 ),
inference(sat_conversion,[],[f737]) ).
cnf(s56,plain,
( ~ spl0_35
| ~ spl0_38 ),
inference(sat_conversion,[],[f744]) ).
cnf(s57,plain,
( ~ spl0_27
| spl0_35
| spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f832]) ).
cnf(s58,plain,
( ~ spl0_27
| spl0_35
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f841]) ).
cnf(s62,plain,
( spl0_16
| ~ spl0_28 ),
inference(sat_conversion,[],[f851]) ).
cnf(s68,plain,
( ~ spl0_27
| spl0_38
| ~ spl0_43 ),
inference(sat_conversion,[],[f908]) ).
cnf(s74,plain,
( spl0_38
| ~ spl0_40 ),
inference(sat_conversion,[],[f994]) ).
cnf(s76,plain,
( ~ spl0_3
| ~ spl0_11
| spl0_23 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s90,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_19 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s91,plain,
( ~ spl0_27
| spl0_36
| ~ spl0_42 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s94,plain,
( ~ spl0_27
| spl0_37
| ~ spl0_41 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s97,plain,
( ~ spl0_27
| spl0_38
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s105,plain,
( ~ spl0_1
| spl0_19
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s111,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_11
| spl0_19
| ~ spl0_43 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s113,plain,
( ~ spl0_4
| ~ spl0_11
| spl0_24 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s115,plain,
( spl0_19
| ~ spl0_21
| ~ spl0_24 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s120,plain,
( ~ spl0_12
| spl0_16 ),
inference(sat_conversion,[],[f1531]) ).
cnf(s124,plain,
( ~ spl0_27
| spl0_40
| ~ spl0_43 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s132,plain,
( ~ spl0_27
| spl0_39
| ~ spl0_44 ),
inference(sat_conversion,[],[f1610]) ).
cnf(s135,plain,
( ~ spl0_2
| ~ spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f1685]) ).
cnf(s142,plain,
( ~ spl0_36
| spl0_38 ),
inference(sat_conversion,[],[f1687]) ).
cnf(s159,plain,
( spl0_35
| ~ spl0_39 ),
inference(sat_conversion,[],[f2079]) ).
cnf(s167,plain,
( spl0_35
| ~ spl0_36
| ~ spl0_40 ),
inference(sat_conversion,[],[f2111]) ).
cnf(s175,plain,
( ~ spl0_1
| ~ spl0_19
| spl0_46 ),
inference(sat_conversion,[],[f2208]) ).
cnf(s180,plain,
( spl0_35
| spl0_40
| ~ spl0_50 ),
inference(sat_conversion,[],[f2249]) ).
cnf(s184,plain,
( spl0_35
| spl0_37
| ~ spl0_50 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s192,plain,
( ~ spl0_1
| spl0_22
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f2292]) ).
cnf(s194,plain,
( ~ spl0_1
| spl0_22
| spl0_41
| spl0_44 ),
inference(sat_conversion,[],[f2323]) ).
cnf(s199,plain,
( ~ spl0_1
| spl0_22
| ~ spl0_23
| ~ spl0_44 ),
inference(sat_conversion,[],[f2419]) ).
cnf(s204,plain,
( ~ spl0_4
| ~ spl0_11
| spl0_19
| ~ spl0_20 ),
inference(sat_conversion,[],[f2433]) ).
cnf(s205,plain,
( ~ spl0_19
| ~ spl0_21
| spl0_22
| ~ spl0_25 ),
inference(sat_conversion,[],[f2440]) ).
cnf(s211,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_20
| ~ spl0_23 ),
inference(sat_conversion,[],[f2462]) ).
cnf(s213,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_11
| ~ spl0_18 ),
inference(sat_conversion,[],[f2465]) ).
cnf(s219,plain,
( ~ spl0_3
| ~ spl0_18
| spl0_21 ),
inference(sat_conversion,[],[f2501]) ).
cnf(s222,plain,
( ~ spl0_3
| spl0_8
| ~ spl0_23
| ~ spl0_25 ),
inference(sat_conversion,[],[f2626]) ).
cnf(s229,plain,
( ~ spl0_1
| spl0_20
| ~ spl0_42 ),
inference(sat_conversion,[],[f2651]) ).
cnf(s238,plain,
( ~ spl0_1
| spl0_21
| ~ spl0_43 ),
inference(sat_conversion,[],[f2738]) ).
cnf(s243,plain,
( ~ spl0_21
| spl0_22
| ~ spl0_41
| ~ spl0_46 ),
inference(sat_conversion,[],[f2791]) ).
cnf(s257,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_19
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s258,plain,
( ~ spl0_3
| ~ spl0_17
| spl0_20 ),
inference(sat_conversion,[],[f2853]) ).
cnf(s259,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_18
| ~ spl0_21
| spl0_22
| spl0_25 ),
inference(sat_conversion,[],[f2910]) ).
cnf(s265,plain,
( spl0_23
| ~ spl0_24 ),
inference(sat_conversion,[],[f2929]) ).
cnf(s266,plain,
( ~ spl0_5
| ~ spl0_16
| spl0_50 ),
inference(sat_conversion,[],[f2935]) ).
cnf(s269,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_36 ),
inference(sat_conversion,[],[f2942]) ).
cnf(s272,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_13
| spl0_50 ),
inference(sat_conversion,[],[f2947]) ).
cnf(s273,plain,
( ~ spl0_6
| ~ spl0_28
| spl0_50 ),
inference(sat_conversion,[],[f2948]) ).
cnf(s312,plain,
( spl0_35
| ~ spl0_37
| ~ spl0_38
| ~ spl0_40 ),
inference(sat_conversion,[],[f3052]) ).
cnf(s315,plain,
( ~ spl0_37
| ~ spl0_40
| spl0_35 ),
inference(rat,[],[s74,s312]) ).
cnf(s316,plain,
( spl0_35
| ~ spl0_50 ),
inference(rat,[],[s315,s180,s184]) ).
cnf(s317,plain,
( ~ spl0_13
| ~ spl0_6
| ~ spl0_2 ),
inference(rat,[],[s55,s74,s142,s56,s316,s272,s36]) ).
cnf(s318,plain,
( ~ spl0_28
| ~ spl0_6 ),
inference(rat,[],[s55,s74,s142,s56,s316,s273]) ).
cnf(s319,plain,
( spl0_11
| ~ spl0_6
| ~ spl0_2 ),
inference(rat,[],[s16,s32,s6,s37,s317,s318]) ).
cnf(s320,plain,
( ~ spl0_27
| ~ spl0_40
| spl0_35 ),
inference(rat,[],[s57,s91,s94,s315,s167]) ).
cnf(s321,plain,
( spl0_19
| ~ spl0_11
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s10,s115,s204,s113]) ).
cnf(s322,plain,
( ~ spl0_21
| ~ spl0_19
| ~ spl0_2
| ~ spl0_4
| spl0_22 ),
inference(rat,[],[s205,s257]) ).
cnf(s323,plain,
( ~ spl0_11
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s322,s13,s12,s321]) ).
cnf(s324,plain,
( spl0_9
| ~ spl0_16
| ~ spl0_5 ),
inference(rat,[],[s7,s29,s269,s142,s56,s316,s266]) ).
cnf(s325,plain,
( ~ spl0_9
| spl0_10
| ~ spl0_5
| ~ spl0_16 ),
inference(rat,[],[s26,s48]) ).
cnf(s326,plain,
( ~ spl0_16
| ~ spl0_5 ),
inference(rat,[],[s325,s5,s324]) ).
cnf(s327,plain,
( spl0_3
| ~ spl0_2 ),
inference(rat,[],[s326,s135,s6,s15,s3,s319,s323,s2]) ).
cnf(s328,plain,
( spl0_35
| ~ spl0_27 ),
inference(rat,[],[s58,s124,s132,s320,s159]) ).
cnf(s329,plain,
~ spl0_27,
inference(rat,[],[s97,s91,s68,s142,s56,s328]) ).
cnf(s330,plain,
( spl0_7
| ~ spl0_11
| ~ spl0_3 ),
inference(rat,[],[s258,s8,s211,s213,s76]) ).
cnf(s331,plain,
( ~ spl0_11
| ~ spl0_3 ),
inference(rat,[],[s259,s219,s41,s222,s12,s4,s90,s330,s76]) ).
cnf(s332,plain,
( spl0_11
| ~ spl0_2 ),
inference(rat,[],[s6,s135,s120,s326,s3,s319]) ).
cnf(s333,plain,
~ spl0_2,
inference(rat,[],[s332,s331,s327]) ).
cnf(s334,plain,
spl0_1,
inference(rat,[],[s1,s333]) ).
cnf(s335,plain,
( spl0_19
| ~ spl0_11
| ~ spl0_4 ),
inference(rat,[],[s229,s105,s204,s111,s334]) ).
cnf(s336,plain,
( ~ spl0_4
| ~ spl0_11 ),
inference(rat,[],[s243,s238,s194,s192,s199,s12,s175,s335,s265,s113,s334]) ).
cnf(s337,plain,
~ spl0_11,
inference(rat,[],[s336,s2,s331]) ).
cnf(s338,plain,
spl0_28,
inference(rat,[],[s6,s120,s33,s32,s337,s334,s329]) ).
cnf(s339,plain,
~ spl0_6,
inference(rat,[],[s318,s338]) ).
cnf(s340,plain,
spl0_16,
inference(rat,[],[s62,s338]) ).
cnf(s342,plain,
spl0_5,
inference(rat,[],[s3,s339]) ).
cnf(s344,plain,
$false,
inference(rat,[],[s326,s342,s340]) ).
fof(f3057,plain,
$false,
inference(avatar_sat_refutation,[],[s344]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % 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 THM
% 0.11/0.36 % Computer : n017.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 17:16:50 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.40 Running first-order theorem proving
% 0.15/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.56/1.41 % (2819096)Input is clausal, will run a generic CNF schedule.
% 3.56/1.41 % (2819105)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1523192402:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.56/1.41 % (2819103)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3554553405:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.56/1.41 % (2819107)dis-21_1_sil=8000:lcm=predicate:random_seed=151062967:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.56/1.41 % (2819104)lrs+10_1_sil=8000:sp=occurrence:random_seed=453405085:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.56/1.41 % (2819102)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=970366754:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.56/1.41 % (2819101)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=511515174:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.56/1.41 % (2819106)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2834393803:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.56/1.41 % (2819105)Instruction limit reached!
% 3.56/1.41 % (2819105)------------------------------
% 3.56/1.41 % (2819105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.41 % (2819105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.41 % (2819105)CaDiCaL version: 2.1.3
% 3.56/1.41 % (2819105)Termination reason: Instruction limit
% 3.56/1.41 % (2819105)Termination phase: Saturation
% 3.56/1.41 % (2819105)Time elapsed: 0.041 s
% 3.56/1.41 % (2819105)Peak memory usage: 89 MB
% 3.56/1.41 % (2819105)Instructions burned: 117 (million)
% 3.56/1.41 % (2819107)Instruction limit reached!
% 3.56/1.41 % (2819107)------------------------------
% 3.56/1.41 % (2819107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.41 % (2819107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.41 % (2819107)CaDiCaL version: 2.1.3
% 3.56/1.41 % (2819107)Termination reason: Instruction limit
% 3.56/1.41 % (2819107)Termination phase: Saturation
% 3.56/1.41 % (2819107)Time elapsed: 0.050 s
% 3.56/1.41 % (2819107)Peak memory usage: 88 MB
% 3.56/1.41 % (2819107)Instructions burned: 118 (million)
% 3.56/1.41 % (2819104)Instruction limit reached!
% 3.56/1.41 % (2819104)------------------------------
% 3.56/1.41 % (2819104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.41 % (2819104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.41 % (2819104)CaDiCaL version: 2.1.3
% 3.56/1.41 % (2819104)Termination reason: Instruction limit
% 3.56/1.41 % (2819104)Termination phase: Saturation
% 3.56/1.41 % (2819104)Time elapsed: 0.063 s
% 3.56/1.41 % (2819104)Peak memory usage: 89 MB
% 3.56/1.41 % (2819104)Instructions burned: 108 (million)
% 3.56/1.41 % (2819106)Instruction limit reached!
% 3.56/1.41 % (2819106)------------------------------
% 3.56/1.41 % (2819106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.41 % (2819106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.41 % (2819106)CaDiCaL version: 2.1.3
% 3.56/1.41 % (2819106)Termination reason: Instruction limit
% 3.56/1.41 % (2819106)Termination phase: Saturation
% 3.56/1.41 % (2819106)Time elapsed: 0.073 s
% 3.56/1.41 % (2819106)Peak memory usage: 90 MB
% 3.56/1.41 % (2819106)Instructions burned: 182 (million)
% 3.56/1.41 % (2819115)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=845903599:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.56/1.41 % (2819118)lrs+10_64_to=lpo:sil=8000:random_seed=1489285871:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 3.56/1.41 % (2819117)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=208199277:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.56/1.41 % (2819116)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4019741856:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.56/1.41 % (2819116)Refutation not found, incomplete strategy
% 3.56/1.41 % (2819116)------------------------------
% 3.56/1.41 % (2819116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.41 % (2819116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.41 % (2819116)CaDiCaL version: 2.1.3
% 3.56/1.41 % (2819116)Termination reason: Refutation not found, incomplete strategy
% 3.56/1.41 % (2819116)Time elapsed: 0.003 s
% 3.56/1.41 % (2819116)Peak memory usage: 88 MB
% 3.56/1.41 % (2819116)Instructions burned: 3 (million)
% 3.56/1.41 % (2819118)First to succeed.
% 3.56/1.41 % (2819118)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2819096"
% 3.56/1.41 % (2819115)Instruction limit reached!
% 3.56/1.41 % (2819115)------------------------------
% 3.56/1.41 % (2819115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.41 % (2819115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.41 % (2819115)CaDiCaL version: 2.1.3
% 3.56/1.41 % (2819115)Termination reason: Instruction limit
% 3.56/1.41 % (2819115)Termination phase: Saturation
% 3.56/1.41 % (2819115)Time elapsed: 0.120 s
% 3.56/1.41 % (2819115)Peak memory usage: 89 MB
% 3.56/1.41 % (2819115)Instructions burned: 144 (million)
% 3.56/1.41 % (2819117)Instruction limit reached!
% 3.56/1.41 % (2819117)------------------------------
% 3.56/1.41 % (2819117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.41 % (2819117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.41 % (2819117)CaDiCaL version: 2.1.3
% 3.56/1.41 % (2819117)Termination reason: Instruction limit
% 3.56/1.41 % (2819117)Termination phase: Saturation
% 3.56/1.41 % (2819117)Time elapsed: 0.128 s
% 3.56/1.41 % (2819117)Peak memory usage: 89 MB
% 3.56/1.41 % (2819117)Instructions burned: 219 (million)
% 3.56/1.41 % (2819118)Refutation found. Thanks to Tanya!
% 3.56/1.41 % SZS status Unsatisfiable for theBenchmark
% 3.56/1.41 % SZS output start Proof for theBenchmark
% See solution above
% 4.66/1.61 % (2819118)------------------------------
% 4.66/1.61 % (2819118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.66/1.61 % (2819118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.66/1.61 % (2819118)CaDiCaL version: 2.1.3
% 4.66/1.61 % (2819118)Termination reason: Refutation
% 4.66/1.61 % (2819118)Time elapsed: 0.042 s
% 4.66/1.61 % (2819118)Peak memory usage: 90 MB
% 4.66/1.61 % (2819118)Instructions burned: 134 (million)
% 4.66/1.61 % (2819118)------------------------------
% 4.66/1.61 % (2819118)------------------------------
% 4.66/1.61 % (2819096)Success in time 0.569 s
% 4.66/1.61 % Vampire exiting
%------------------------------------------------------------------------------