%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MGT035+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:02:37 PM UTC 2026
% Result : Theorem 2.25s 0.88s
% Output : Refutation 2.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 78
% Syntax : Number of formulae : 644 ( 48 unt; 60 def)
% Number of atoms : 1973 ( 84 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2349 (1020 ~;1149 |; 89 &)
% ( 64 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 73 ( 71 usr; 61 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-2 aty)
% Number of variables : 300 ( 0 sgn 288 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ( environment(X0)
& subpopulations(first_movers,efficient_producers,X0,X1) )
=> in_environment(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_time_point_in_environment) ).
fof(f2,axiom,
! [X0,X1] :
( ( environment(X0)
& subpopulations(first_movers,efficient_producers,X0,X1) )
=> greater(number_of_organizations(X0,X1),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_environment_not_empty) ).
fof(f3,axiom,
! [X0,X1,X2] :
( ( environment(X0)
& subpopulation(X1,X0,X2)
& ( greater(cardinality_at_time(X1,X2),zero)
=> ( X1 = efficient_producers
| X1 = first_movers ) ) )
=> number_of_organizations(X0,X2) = sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_only_members) ).
fof(f4,axiom,
! [X0,X1] :
( ( environment(X0)
& in_environment(X0,X1) )
=> ( subpopulation(first_movers,X0,X1)
& subpopulation(efficient_producers,X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_FM_and_EP_organisational) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( X0 = sum(X1,X2)
& constant(X0) )
=> ( ( constant(X1)
& constant(X2) )
| ( increases(X1)
& decreases(X2) )
| ( decreases(X1)
& increases(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_abc_sum_increase) ).
fof(f6,axiom,
! [X0,X1,X2] :
( ( environment(X1)
& in_environment(X1,X2)
& subpopulation(X0,X1,X2)
& greater(cardinality_at_time(X0,X2),zero) )
=> ( ( constant(cardinality_at_time(X0,X2))
=> growth_rate(X0,X2) = zero )
& ( increases(cardinality_at_time(X0,X2))
=> greater(growth_rate(X0,X2),zero) )
& ( decreases(cardinality_at_time(X0,X2))
=> greater(zero,growth_rate(X0,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_growth_rate) ).
fof(f7,axiom,
! [X0,X1] :
( ( environment(X0)
& subpopulations(first_movers,efficient_producers,X0,X1) )
=> ( greater(cardinality_at_time(first_movers,X1),zero)
& greater(cardinality_at_time(efficient_producers,X1),zero) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_positive_number_of_organizations) ).
fof(f8,axiom,
! [X0,X1] :
~ ( greater(X0,X1)
& X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp6_1) ).
fof(f9,axiom,
! [X0,X1] :
~ ( greater(X0,X1)
& greater(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp6_2) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( greater(X0,X1)
& greater(X1,X2) )
=> greater(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( 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) ).
fof(f12,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
<=> ( greater(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal) ).
fof(f14,axiom,
! [X0,X1,X2,X3] :
( ( environment(X0)
& subpopulations(X1,X2,X0,X3) )
=> ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
<=> outcompetes(X2,X1,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2) ).
fof(f15,axiom,
! [X0,X1] :
( ( environment(X0)
& in_environment(X0,X1)
& greater(number_of_organizations(X0,X1),zero) )
=> ( ( greater(equilibrium(X0),X1)
=> decreases(resources(X0,X1)) )
& ( ~ greater(equilibrium(X0),X1)
=> constant(resources(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
fof(f16,axiom,
! [X0] :
( ( environment(X0)
& stable(X0) )
=> ? [X1] :
( in_environment(X0,X1)
& greater_or_equal(X1,equilibrium(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5) ).
fof(f17,axiom,
! [X0,X1] :
( ( environment(X0)
& in_environment(X0,X1) )
=> ( ( decreases(resources(X0,X1))
=> ~ decreases(number_of_organizations(X0,X1)) )
& ( constant(resources(X0,X1))
=> constant(number_of_organizations(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a7) ).
fof(f19,axiom,
! [X0] :
( ( environment(X0)
& stable(X0) )
=> ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( ( subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) )
=> greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1) ).
fof(f20,conjecture,
! [X0] :
( ( environment(X0)
& stable(X0) )
=> ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( ( subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) )
=> outcompetes(efficient_producers,first_movers,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t4) ).
fof(f21,negated_conjecture,
~ ! [X0] :
( ( environment(X0)
& stable(X0) )
=> ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( ( subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) )
=> outcompetes(efficient_producers,first_movers,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f22,plain,
! [X0,X1] :
( in_environment(X0,X1)
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(ennf_transformation,[],[f1]) ).
fof(f23,plain,
! [X0,X1] :
( in_environment(X0,X1)
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(flattening,[],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( greater(number_of_organizations(X0,X1),zero)
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f25,plain,
! [X0,X1] :
( greater(number_of_organizations(X0,X1),zero)
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(flattening,[],[f24]) ).
fof(f26,plain,
! [X0,X1,X2] :
( number_of_organizations(X0,X2) = sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2))
| ~ environment(X0)
| ~ subpopulation(X1,X0,X2)
| ( efficient_producers != X1
& first_movers != X1
& greater(cardinality_at_time(X1,X2),zero) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f27,plain,
! [X0,X1,X2] :
( number_of_organizations(X0,X2) = sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2))
| ~ environment(X0)
| ~ subpopulation(X1,X0,X2)
| ( efficient_producers != X1
& first_movers != X1
& greater(cardinality_at_time(X1,X2),zero) ) ),
inference(flattening,[],[f26]) ).
fof(f28,plain,
! [X0,X1] :
( ( subpopulation(first_movers,X0,X1)
& subpopulation(efficient_producers,X0,X1) )
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(ennf_transformation,[],[f4]) ).
fof(f29,plain,
! [X0,X1] :
( ( subpopulation(first_movers,X0,X1)
& subpopulation(efficient_producers,X0,X1) )
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(flattening,[],[f28]) ).
fof(f30,plain,
! [X0,X1,X2] :
( ( constant(X1)
& constant(X2) )
| ( increases(X1)
& decreases(X2) )
| ( decreases(X1)
& increases(X2) )
| sum(X1,X2) != X0
| ~ constant(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ( constant(X1)
& constant(X2) )
| ( increases(X1)
& decreases(X2) )
| ( decreases(X1)
& increases(X2) )
| sum(X1,X2) != X0
| ~ constant(X0) ),
inference(flattening,[],[f30]) ).
fof(f32,plain,
! [X0,X1,X2] :
( ( ( growth_rate(X0,X2) = zero
| ~ constant(cardinality_at_time(X0,X2)) )
& ( greater(growth_rate(X0,X2),zero)
| ~ increases(cardinality_at_time(X0,X2)) )
& ( greater(zero,growth_rate(X0,X2))
| ~ decreases(cardinality_at_time(X0,X2)) ) )
| ~ environment(X1)
| ~ in_environment(X1,X2)
| ~ subpopulation(X0,X1,X2)
| ~ greater(cardinality_at_time(X0,X2),zero) ),
inference(ennf_transformation,[],[f6]) ).
fof(f33,plain,
! [X0,X1,X2] :
( ( ( growth_rate(X0,X2) = zero
| ~ constant(cardinality_at_time(X0,X2)) )
& ( greater(growth_rate(X0,X2),zero)
| ~ increases(cardinality_at_time(X0,X2)) )
& ( greater(zero,growth_rate(X0,X2))
| ~ decreases(cardinality_at_time(X0,X2)) ) )
| ~ environment(X1)
| ~ in_environment(X1,X2)
| ~ subpopulation(X0,X1,X2)
| ~ greater(cardinality_at_time(X0,X2),zero) ),
inference(flattening,[],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( ( greater(cardinality_at_time(first_movers,X1),zero)
& greater(cardinality_at_time(efficient_producers,X1),zero) )
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(ennf_transformation,[],[f7]) ).
fof(f35,plain,
! [X0,X1] :
( ( greater(cardinality_at_time(first_movers,X1),zero)
& greater(cardinality_at_time(efficient_producers,X1),zero) )
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(flattening,[],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| X0 != X1 ),
inference(ennf_transformation,[],[f8]) ).
fof(f37,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| ~ greater(X1,X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f38,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(ennf_transformation,[],[f10]) ).
fof(f39,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(flattening,[],[f38]) ).
fof(f40,plain,
! [X0,X1,X2] :
( greater(X2,X1)
| X2 = X1
| greater(X1,X2)
| ~ in_environment(X0,X1)
| ~ in_environment(X0,X2) ),
inference(ennf_transformation,[],[f11]) ).
fof(f41,plain,
! [X0,X1,X2] :
( greater(X2,X1)
| X2 = X1
| greater(X1,X2)
| ~ in_environment(X0,X1)
| ~ in_environment(X0,X2) ),
inference(flattening,[],[f40]) ).
fof(f44,plain,
! [X0,X1,X2,X3] :
( ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
<=> outcompetes(X2,X1,X3) )
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f45,plain,
! [X0,X1,X2,X3] :
( ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
<=> outcompetes(X2,X1,X3) )
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(flattening,[],[f44]) ).
fof(f46,plain,
! [X0,X1] :
( ( ( decreases(resources(X0,X1))
| ~ greater(equilibrium(X0),X1) )
& ( constant(resources(X0,X1))
| greater(equilibrium(X0),X1) ) )
| ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ greater(number_of_organizations(X0,X1),zero) ),
inference(ennf_transformation,[],[f15]) ).
fof(f47,plain,
! [X0,X1] :
( ( ( decreases(resources(X0,X1))
| ~ greater(equilibrium(X0),X1) )
& ( constant(resources(X0,X1))
| greater(equilibrium(X0),X1) ) )
| ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ greater(number_of_organizations(X0,X1),zero) ),
inference(flattening,[],[f46]) ).
fof(f48,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& greater_or_equal(X1,equilibrium(X0)) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f49,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& greater_or_equal(X1,equilibrium(X0)) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(flattening,[],[f48]) ).
fof(f50,plain,
! [X0,X1] :
( ( ( ~ decreases(number_of_organizations(X0,X1))
| ~ decreases(resources(X0,X1)) )
& ( constant(number_of_organizations(X0,X1))
| ~ constant(resources(X0,X1)) ) )
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f51,plain,
! [X0,X1] :
( ( ( ~ decreases(number_of_organizations(X0,X1))
| ~ decreases(resources(X0,X1)) )
& ( constant(number_of_organizations(X0,X1))
| ~ constant(resources(X0,X1)) ) )
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(flattening,[],[f50]) ).
fof(f54,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater_or_equal(X2,X1) ) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f55,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& ! [X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater_or_equal(X2,X1) ) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(flattening,[],[f54]) ).
fof(f56,plain,
? [X0] :
( ! [X1] :
( ~ in_environment(X0,X1)
| ? [X2] :
( ~ outcompetes(efficient_producers,first_movers,X2)
& subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) ) )
& environment(X0)
& stable(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f57,plain,
? [X0] :
( ! [X1] :
( ~ in_environment(X0,X1)
| ? [X2] :
( ~ outcompetes(efficient_producers,first_movers,X2)
& subpopulations(first_movers,efficient_producers,X0,X2)
& greater_or_equal(X2,X1) ) )
& environment(X0)
& stable(X0) ),
inference(flattening,[],[f56]) ).
fof(f58,plain,
! [X0,X1] :
( ( greater_or_equal(X0,X1)
| ( ~ greater(X0,X1)
& X0 != X1 ) )
& ( greater(X0,X1)
| X0 = X1
| ~ greater_or_equal(X0,X1) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f59,plain,
! [X0,X1] :
( ( greater_or_equal(X0,X1)
| ( ~ greater(X0,X1)
& X0 != X1 ) )
& ( greater(X0,X1)
| X0 = X1
| ~ greater_or_equal(X0,X1) ) ),
inference(flattening,[],[f58]) ).
fof(f60,plain,
! [X0,X1,X2,X3] :
( ( ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
| ~ outcompetes(X2,X1,X3) )
& ( outcompetes(X2,X1,X3)
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| ~ greater(zero,growth_rate(X1,X3)) ) )
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(nnf_transformation,[],[f45]) ).
fof(f61,plain,
! [X0,X1,X2,X3] :
( ( ( ( greater_or_equal(growth_rate(X2,X3),zero)
& greater(zero,growth_rate(X1,X3)) )
| ~ outcompetes(X2,X1,X3) )
& ( outcompetes(X2,X1,X3)
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| ~ greater(zero,growth_rate(X1,X3)) ) )
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0] :
( ( in_environment(X0,sK0(X0))
& greater_or_equal(sK0(X0),equilibrium(X0)) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f49]) ).
fof(f63,plain,
! [X0] :
( ( in_environment(X0,sK1(X0))
& ! [X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater_or_equal(X2,sK1(X0)) ) )
| ~ environment(X0)
| ~ stable(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X1,sK1(X0))],[f55]) ).
fof(f64,plain,
( ! [X1] :
( ~ in_environment(sK2,X1)
| ( ~ outcompetes(efficient_producers,first_movers,sK3(X1))
& subpopulations(first_movers,efficient_producers,sK2,sK3(X1))
& greater_or_equal(sK3(X1),X1) ) )
& environment(sK2)
& stable(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X0,sK2),skolemize(X2,sK3(X1))],[f57]) ).
fof(f65,plain,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| in_environment(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f66,plain,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(number_of_organizations(X0,X1),zero) ),
inference(cnf_transformation,[],[f25]) ).
fof(f69,plain,
! [X2,X0,X1] :
( number_of_organizations(X0,X2) = sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2))
| ~ environment(X0)
| ~ subpopulation(X1,X0,X2)
| efficient_producers != X1 ),
inference(cnf_transformation,[],[f27]) ).
fof(f70,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulation(efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f71,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulation(first_movers,X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f73,plain,
! [X2,X0,X1] :
( constant(X2)
| decreases(X2)
| decreases(X1)
| sum(X1,X2) != X0
| ~ constant(X0) ),
inference(cnf_transformation,[],[f31]) ).
fof(f74,plain,
! [X2,X0,X1] :
( constant(X2)
| increases(X1)
| increases(X2)
| sum(X1,X2) != X0
| ~ constant(X0) ),
inference(cnf_transformation,[],[f31]) ).
fof(f76,plain,
! [X2,X0,X1] :
( constant(X1)
| decreases(X2)
| increases(X2)
| sum(X1,X2) != X0
| ~ constant(X0) ),
inference(cnf_transformation,[],[f31]) ).
fof(f78,plain,
! [X2,X0,X1] :
( constant(X1)
| increases(X1)
| increases(X2)
| sum(X1,X2) != X0
| ~ constant(X0) ),
inference(cnf_transformation,[],[f31]) ).
fof(f80,plain,
! [X2,X0,X1] :
( ~ greater(cardinality_at_time(X0,X2),zero)
| ~ decreases(cardinality_at_time(X0,X2))
| ~ environment(X1)
| ~ in_environment(X1,X2)
| ~ subpopulation(X0,X1,X2)
| greater(zero,growth_rate(X0,X2)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f81,plain,
! [X2,X0,X1] :
( ~ greater(cardinality_at_time(X0,X2),zero)
| ~ increases(cardinality_at_time(X0,X2))
| ~ environment(X1)
| ~ in_environment(X1,X2)
| ~ subpopulation(X0,X1,X2)
| greater(growth_rate(X0,X2),zero) ),
inference(cnf_transformation,[],[f33]) ).
fof(f82,plain,
! [X2,X0,X1] :
( ~ greater(cardinality_at_time(X0,X2),zero)
| ~ constant(cardinality_at_time(X0,X2))
| ~ environment(X1)
| ~ in_environment(X1,X2)
| ~ subpopulation(X0,X1,X2)
| zero = growth_rate(X0,X2) ),
inference(cnf_transformation,[],[f33]) ).
fof(f83,plain,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(cardinality_at_time(efficient_producers,X1),zero) ),
inference(cnf_transformation,[],[f35]) ).
fof(f84,plain,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(cardinality_at_time(first_movers,X1),zero) ),
inference(cnf_transformation,[],[f35]) ).
fof(f85,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f36]) ).
fof(f86,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f87,plain,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f88,plain,
! [X2,X0,X1] :
( ~ in_environment(X0,X2)
| X1 = X2
| greater(X1,X2)
| ~ in_environment(X0,X1)
| greater(X2,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f89,plain,
! [X0,X1] :
( ~ greater_or_equal(X0,X1)
| X0 = X1
| greater(X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
fof(f91,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
fof(f93,plain,
! [X2,X3,X0,X1] :
( ~ greater_or_equal(growth_rate(X2,X3),zero)
| outcompetes(X2,X1,X3)
| ~ greater(zero,growth_rate(X1,X3))
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3) ),
inference(cnf_transformation,[],[f61]) ).
fof(f96,plain,
! [X0,X1] :
( ~ greater(number_of_organizations(X0,X1),zero)
| greater(equilibrium(X0),X1)
| ~ environment(X0)
| ~ in_environment(X0,X1)
| constant(resources(X0,X1)) ),
inference(cnf_transformation,[],[f47]) ).
fof(f98,plain,
! [X0] :
( greater_or_equal(sK0(X0),equilibrium(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f99,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sK0(X0)) ),
inference(cnf_transformation,[],[f62]) ).
fof(f100,plain,
! [X0,X1] :
( ~ constant(resources(X0,X1))
| constant(number_of_organizations(X0,X1))
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f51]) ).
fof(f103,plain,
! [X2,X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ greater_or_equal(X2,sK1(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f104,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sK1(X0)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f105,plain,
stable(sK2),
inference(cnf_transformation,[],[f64]) ).
fof(f106,plain,
environment(sK2),
inference(cnf_transformation,[],[f64]) ).
fof(f107,plain,
! [X1] :
( greater_or_equal(sK3(X1),X1)
| ~ in_environment(sK2,X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f108,plain,
! [X1] :
( subpopulations(first_movers,efficient_producers,sK2,sK3(X1))
| ~ in_environment(sK2,X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f109,plain,
! [X1] :
( ~ outcompetes(efficient_producers,first_movers,sK3(X1))
| ~ in_environment(sK2,X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f110,plain,
! [X2,X0] :
( ~ subpopulation(efficient_producers,X0,X2)
| ~ environment(X0)
| number_of_organizations(X0,X2) = sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2)) ),
inference(equality_resolution,[],[f69]) ).
fof(f113,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| increases(X1)
| increases(X2)
| constant(X1) ),
inference(equality_resolution,[],[f78]) ).
fof(f115,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| decreases(X2)
| increases(X2)
| constant(X1) ),
inference(equality_resolution,[],[f76]) ).
fof(f117,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| increases(X1)
| increases(X2)
| constant(X2) ),
inference(equality_resolution,[],[f74]) ).
fof(f118,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| decreases(X2)
| decreases(X1)
| constant(X2) ),
inference(equality_resolution,[],[f73]) ).
fof(f120,plain,
! [X1] : ~ greater(X1,X1),
inference(equality_resolution,[],[f85]) ).
fof(f122,plain,
( ~ environment(sK2)
| in_environment(sK2,sK0(sK2)) ),
inference(resolution,[],[f99,f105]) ).
fof(f123,plain,
in_environment(sK2,sK0(sK2)),
inference(forward_subsumption_resolution,[],[f122,f106]) ).
fof(f124,plain,
( ~ environment(sK2)
| in_environment(sK2,sK1(sK2)) ),
inference(resolution,[],[f104,f105]) ).
fof(f125,plain,
in_environment(sK2,sK1(sK2)),
inference(forward_subsumption_resolution,[],[f124,f106]) ).
fof(f134,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| greater(sK3(X0),X0)
| sK3(X0) = X0 ),
inference(resolution,[],[f89,f107]) ).
fof(f136,plain,
! [X0] :
( ~ stable(X0)
| greater(sK0(X0),equilibrium(X0))
| ~ environment(X0)
| equilibrium(X0) = sK0(X0) ),
inference(resolution,[],[f89,f98]) ).
fof(f137,plain,
! [X0] :
( ~ environment(sK2)
| in_environment(sK2,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f65,f108]) ).
fof(f138,plain,
! [X0] :
( in_environment(sK2,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f137,f106]) ).
fof(f144,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| ~ environment(sK2)
| subpopulation(efficient_producers,sK2,sK3(X0)) ),
inference(resolution,[],[f138,f70]) ).
fof(f145,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| subpopulation(efficient_producers,sK2,sK3(X0)) ),
inference(forward_subsumption_resolution,[],[f144,f106]) ).
fof(f147,plain,
subpopulation(efficient_producers,sK2,sK3(sK0(sK2))),
inference(resolution,[],[f145,f123]) ).
fof(f148,plain,
subpopulation(efficient_producers,sK2,sK3(sK1(sK2))),
inference(resolution,[],[f145,f125]) ).
fof(f156,plain,
! [X0] :
( ~ environment(sK2)
| greater(number_of_organizations(sK2,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f66,f108]) ).
fof(f157,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| greater(number_of_organizations(sK2,sK3(X0)),zero) ),
inference(forward_subsumption_resolution,[],[f156,f106]) ).
fof(f158,plain,
! [X0] :
( ~ environment(sK2)
| greater(cardinality_at_time(efficient_producers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f83,f108]) ).
fof(f159,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| greater(cardinality_at_time(efficient_producers,sK3(X0)),zero) ),
inference(forward_subsumption_resolution,[],[f158,f106]) ).
fof(f160,plain,
greater(number_of_organizations(sK2,sK3(sK0(sK2))),zero),
inference(resolution,[],[f157,f123]) ).
fof(f161,plain,
greater(number_of_organizations(sK2,sK3(sK1(sK2))),zero),
inference(resolution,[],[f157,f125]) ).
fof(f163,plain,
! [X0] :
( ~ environment(sK2)
| greater(cardinality_at_time(first_movers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f84,f108]) ).
fof(f164,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| greater(cardinality_at_time(first_movers,sK3(X0)),zero) ),
inference(forward_subsumption_resolution,[],[f163,f106]) ).
fof(f173,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| greater(X0,sK1(sK2))
| sK1(sK2) = X0
| greater(sK1(sK2),X0) ),
inference(resolution,[],[f88,f125]) ).
fof(f178,plain,
greater(cardinality_at_time(efficient_producers,sK3(sK0(sK2))),zero),
inference(resolution,[],[f159,f123]) ).
fof(f179,plain,
greater(cardinality_at_time(efficient_producers,sK3(sK1(sK2))),zero),
inference(resolution,[],[f159,f125]) ).
fof(f183,plain,
( ~ environment(sK2)
| number_of_organizations(sK2,sK3(sK0(sK2))) = sum(cardinality_at_time(first_movers,sK3(sK0(sK2))),cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
inference(resolution,[],[f110,f147]) ).
fof(f184,plain,
( ~ environment(sK2)
| number_of_organizations(sK2,sK3(sK1(sK2))) = sum(cardinality_at_time(first_movers,sK3(sK1(sK2))),cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
inference(resolution,[],[f110,f148]) ).
fof(f189,plain,
number_of_organizations(sK2,sK3(sK1(sK2))) = sum(cardinality_at_time(first_movers,sK3(sK1(sK2))),cardinality_at_time(efficient_producers,sK3(sK1(sK2)))),
inference(forward_subsumption_resolution,[],[f184,f106]) ).
fof(f190,plain,
number_of_organizations(sK2,sK3(sK0(sK2))) = sum(cardinality_at_time(first_movers,sK3(sK0(sK2))),cardinality_at_time(efficient_producers,sK3(sK0(sK2)))),
inference(forward_subsumption_resolution,[],[f183,f106]) ).
fof(f205,plain,
( greater(equilibrium(sK2),sK3(sK0(sK2)))
| ~ environment(sK2)
| ~ in_environment(sK2,sK3(sK0(sK2)))
| constant(resources(sK2,sK3(sK0(sK2)))) ),
inference(resolution,[],[f96,f160]) ).
fof(f206,plain,
( greater(equilibrium(sK2),sK3(sK1(sK2)))
| ~ environment(sK2)
| ~ in_environment(sK2,sK3(sK1(sK2)))
| constant(resources(sK2,sK3(sK1(sK2)))) ),
inference(resolution,[],[f96,f161]) ).
fof(f207,plain,
( greater(equilibrium(sK2),sK3(sK1(sK2)))
| ~ in_environment(sK2,sK3(sK1(sK2)))
| constant(resources(sK2,sK3(sK1(sK2)))) ),
inference(forward_subsumption_resolution,[],[f206,f106]) ).
fof(f208,plain,
( greater(equilibrium(sK2),sK3(sK0(sK2)))
| ~ in_environment(sK2,sK3(sK0(sK2)))
| constant(resources(sK2,sK3(sK0(sK2)))) ),
inference(forward_subsumption_resolution,[],[f205,f106]) ).
fof(f210,definition,
( spl4_1
<=> constant(resources(sK2,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f212,plain,
( constant(resources(sK2,sK3(sK1(sK2))))
| ~ spl4_1 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f214,definition,
( spl4_2
<=> in_environment(sK2,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f215,plain,
( in_environment(sK2,sK3(sK1(sK2)))
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f216,plain,
( ~ in_environment(sK2,sK3(sK1(sK2)))
| spl4_2 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f218,definition,
( spl4_3
<=> greater(equilibrium(sK2),sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f220,plain,
( greater(equilibrium(sK2),sK3(sK1(sK2)))
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f221,plain,
( spl4_1
| ~ spl4_2
| spl4_3 ),
inference(avatar_split_clause,[],[f207,f218,f214,f210]) ).
fof(f223,definition,
( spl4_4
<=> constant(resources(sK2,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f225,plain,
( constant(resources(sK2,sK3(sK0(sK2))))
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f227,definition,
( spl4_5
<=> in_environment(sK2,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f228,plain,
( in_environment(sK2,sK3(sK0(sK2)))
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f229,plain,
( ~ in_environment(sK2,sK3(sK0(sK2)))
| spl4_5 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f231,definition,
( spl4_6
<=> greater(equilibrium(sK2),sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f232,plain,
( ~ greater(equilibrium(sK2),sK3(sK0(sK2)))
| spl4_6 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f233,plain,
( greater(equilibrium(sK2),sK3(sK0(sK2)))
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f234,plain,
( spl4_4
| ~ spl4_5
| spl4_6 ),
inference(avatar_split_clause,[],[f208,f231,f227,f223]) ).
fof(f235,plain,
( ~ in_environment(sK2,sK1(sK2))
| spl4_2 ),
inference(resolution,[],[f216,f138]) ).
fof(f236,plain,
( $false
| spl4_2 ),
inference(forward_subsumption_resolution,[],[f235,f125]) ).
fof(f237,plain,
spl4_2,
inference(avatar_contradiction_clause,[],[f236]) ).
fof(f251,plain,
! [X0] :
( greater(growth_rate(efficient_producers,sK3(X0)),growth_rate(first_movers,sK3(X0)))
| ~ greater_or_equal(sK3(X0),sK1(sK2))
| ~ environment(sK2)
| ~ stable(sK2)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f103,f108]) ).
fof(f252,plain,
! [X0] :
( greater(growth_rate(efficient_producers,sK3(X0)),growth_rate(first_movers,sK3(X0)))
| ~ greater_or_equal(sK3(X0),sK1(sK2))
| ~ stable(sK2)
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f251,f106]) ).
fof(f253,plain,
! [X0] :
( ~ greater_or_equal(sK3(X0),sK1(sK2))
| greater(growth_rate(efficient_producers,sK3(X0)),growth_rate(first_movers,sK3(X0)))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f252,f105]) ).
fof(f254,plain,
( ~ in_environment(sK2,sK0(sK2))
| spl4_5 ),
inference(resolution,[],[f229,f138]) ).
fof(f255,plain,
( $false
| spl4_5 ),
inference(forward_subsumption_resolution,[],[f254,f123]) ).
fof(f256,plain,
spl4_5,
inference(avatar_contradiction_clause,[],[f255]) ).
fof(f269,plain,
( ! [X0] :
( ~ in_environment(sK2,X0)
| greater(X0,sK3(sK0(sK2)))
| sK3(sK0(sK2)) = X0
| greater(sK3(sK0(sK2)),X0) )
| ~ spl4_5 ),
inference(resolution,[],[f228,f88]) ).
fof(f285,plain,
! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| ~ subpopulation(efficient_producers,X0,sK3(sK0(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2)))) ),
inference(resolution,[],[f80,f178]) ).
fof(f286,plain,
! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| ~ subpopulation(efficient_producers,X0,sK3(sK1(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2)))) ),
inference(resolution,[],[f80,f179]) ).
fof(f287,plain,
! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2)))) ),
inference(forward_subsumption_resolution,[],[f286,f70]) ).
fof(f288,plain,
! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2)))) ),
inference(forward_subsumption_resolution,[],[f285,f70]) ).
fof(f290,definition,
( spl4_8
<=> greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f292,plain,
( greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f294,definition,
( spl4_9
<=> ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f295,plain,
( ! [X0] :
( ~ in_environment(X0,sK3(sK1(sK2)))
| ~ environment(X0) )
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f297,definition,
( spl4_10
<=> decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f299,plain,
( ~ decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| spl4_10 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f300,plain,
( spl4_8
| spl4_9
| ~ spl4_10 ),
inference(avatar_split_clause,[],[f287,f297,f294,f290]) ).
fof(f302,definition,
( spl4_11
<=> greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f304,plain,
( greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f306,definition,
( spl4_12
<=> ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f307,plain,
( ! [X0] :
( ~ in_environment(X0,sK3(sK0(sK2)))
| ~ environment(X0) )
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f309,definition,
( spl4_13
<=> decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f310,plain,
( decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_13 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f311,plain,
( ~ decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| spl4_13 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
( spl4_11
| spl4_12
| ~ spl4_13 ),
inference(avatar_split_clause,[],[f288,f309,f306,f302]) ).
fof(f313,plain,
( constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| ~ environment(sK2)
| ~ in_environment(sK2,sK3(sK0(sK2)))
| ~ spl4_4 ),
inference(resolution,[],[f225,f100]) ).
fof(f314,plain,
( constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| ~ in_environment(sK2,sK3(sK0(sK2)))
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f313,f106]) ).
fof(f315,plain,
( constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5 ),
inference(forward_subsumption_resolution,[],[f314,f228]) ).
fof(f316,plain,
! [X0] :
( ~ increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| ~ subpopulation(efficient_producers,X0,sK3(sK0(sK2)))
| greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero) ),
inference(resolution,[],[f81,f178]) ).
fof(f317,plain,
! [X0] :
( ~ increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| ~ subpopulation(efficient_producers,X0,sK3(sK1(sK2)))
| greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) ),
inference(resolution,[],[f81,f179]) ).
fof(f318,plain,
! [X0] :
( ~ increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) ),
inference(forward_subsumption_resolution,[],[f317,f70]) ).
fof(f319,plain,
! [X0] :
( ~ increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero) ),
inference(forward_subsumption_resolution,[],[f316,f70]) ).
fof(f321,definition,
( spl4_14
<=> greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f322,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| spl4_14 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f323,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f325,definition,
( spl4_15
<=> increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f327,plain,
( ~ increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| spl4_15 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f328,plain,
( spl4_14
| spl4_9
| ~ spl4_15 ),
inference(avatar_split_clause,[],[f318,f325,f294,f321]) ).
fof(f330,definition,
( spl4_16
<=> greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_16])],[avatar_definition]) ).
fof(f331,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| spl4_16 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f332,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ spl4_16 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f334,definition,
( spl4_17
<=> increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f336,plain,
( ~ increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| spl4_17 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f337,plain,
( spl4_16
| spl4_12
| ~ spl4_17 ),
inference(avatar_split_clause,[],[f319,f334,f306,f330]) ).
fof(f338,plain,
! [X0] :
( ~ constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| ~ subpopulation(efficient_producers,X0,sK3(sK0(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK0(sK2))) ),
inference(resolution,[],[f82,f178]) ).
fof(f339,plain,
! [X0] :
( ~ constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| ~ subpopulation(efficient_producers,X0,sK3(sK1(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK1(sK2))) ),
inference(resolution,[],[f82,f179]) ).
fof(f340,plain,
! [X0] :
( ~ constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK1(sK2))) ),
inference(forward_subsumption_resolution,[],[f339,f70]) ).
fof(f341,plain,
! [X0] :
( ~ constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK0(sK2))) ),
inference(forward_subsumption_resolution,[],[f338,f70]) ).
fof(f343,definition,
( spl4_18
<=> zero = growth_rate(efficient_producers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_18])],[avatar_definition]) ).
fof(f345,plain,
( zero = growth_rate(efficient_producers,sK3(sK1(sK2)))
| ~ spl4_18 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f347,definition,
( spl4_19
<=> constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_19])],[avatar_definition]) ).
fof(f349,plain,
( ~ constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| spl4_19 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f350,plain,
( spl4_18
| spl4_9
| ~ spl4_19 ),
inference(avatar_split_clause,[],[f340,f347,f294,f343]) ).
fof(f352,definition,
( spl4_20
<=> zero = growth_rate(efficient_producers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition]) ).
fof(f354,plain,
( zero = growth_rate(efficient_producers,sK3(sK0(sK2)))
| ~ spl4_20 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,definition,
( spl4_21
<=> constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f358,plain,
( ~ constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| spl4_21 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,plain,
( spl4_20
| spl4_12
| ~ spl4_21 ),
inference(avatar_split_clause,[],[f341,f356,f306,f352]) ).
fof(f363,plain,
greater(cardinality_at_time(first_movers,sK3(sK0(sK2))),zero),
inference(resolution,[],[f164,f123]) ).
fof(f364,plain,
greater(cardinality_at_time(first_movers,sK3(sK1(sK2))),zero),
inference(resolution,[],[f164,f125]) ).
fof(f368,plain,
( greater(sK3(sK0(sK2)),sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2)) ),
inference(resolution,[],[f134,f123]) ).
fof(f369,plain,
( greater(sK3(sK1(sK2)),sK1(sK2))
| sK1(sK2) = sK3(sK1(sK2)) ),
inference(resolution,[],[f134,f125]) ).
fof(f392,definition,
( spl4_26
<=> sK1(sK2) = sK3(sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f394,plain,
( sK1(sK2) = sK3(sK1(sK2))
| ~ spl4_26 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f396,definition,
( spl4_27
<=> greater(sK3(sK1(sK2)),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_27])],[avatar_definition]) ).
fof(f398,plain,
( greater(sK3(sK1(sK2)),sK1(sK2))
| ~ spl4_27 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f399,plain,
( spl4_26
| spl4_27 ),
inference(avatar_split_clause,[],[f369,f396,f392]) ).
fof(f401,definition,
( spl4_28
<=> sK0(sK2) = sK3(sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f403,plain,
( sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_28 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f405,definition,
( spl4_29
<=> greater(sK3(sK0(sK2)),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_29])],[avatar_definition]) ).
fof(f407,plain,
( greater(sK3(sK0(sK2)),sK0(sK2))
| ~ spl4_29 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f408,plain,
( spl4_28
| spl4_29 ),
inference(avatar_split_clause,[],[f368,f405,f401]) ).
fof(f426,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2))))
| ~ in_environment(sK2,sK1(sK2))
| ~ in_environment(sK2,sK1(sK2)) ),
inference(resolution,[],[f253,f107]) ).
fof(f428,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2))))
| ~ in_environment(sK2,sK1(sK2)) ),
inference(duplicate_literal_removal,[],[f426]) ).
fof(f430,plain,
greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2)))),
inference(forward_subsumption_resolution,[],[f428,f125]) ).
fof(f439,plain,
( greater(sK0(sK2),equilibrium(sK2))
| ~ environment(sK2)
| sK0(sK2) = equilibrium(sK2) ),
inference(resolution,[],[f136,f105]) ).
fof(f440,plain,
( greater(sK0(sK2),equilibrium(sK2))
| sK0(sK2) = equilibrium(sK2) ),
inference(forward_subsumption_resolution,[],[f439,f106]) ).
fof(f442,definition,
( spl4_30
<=> sK0(sK2) = equilibrium(sK2) ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f444,plain,
( sK0(sK2) = equilibrium(sK2)
| ~ spl4_30 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f446,definition,
( spl4_31
<=> greater(sK0(sK2),equilibrium(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_31])],[avatar_definition]) ).
fof(f448,plain,
( greater(sK0(sK2),equilibrium(sK2))
| ~ spl4_31 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f449,plain,
( spl4_30
| spl4_31 ),
inference(avatar_split_clause,[],[f440,f446,f442]) ).
fof(f450,plain,
( in_environment(sK2,equilibrium(sK2))
| ~ spl4_30 ),
inference(superposition,[],[f123,f444]) ).
fof(f506,plain,
! [X0] :
( ~ constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| ~ subpopulation(first_movers,X0,sK3(sK0(sK2)))
| zero = growth_rate(first_movers,sK3(sK0(sK2))) ),
inference(resolution,[],[f363,f82]) ).
fof(f507,plain,
! [X0] :
( ~ increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| ~ subpopulation(first_movers,X0,sK3(sK0(sK2)))
| greater(growth_rate(first_movers,sK3(sK0(sK2))),zero) ),
inference(resolution,[],[f363,f81]) ).
fof(f508,plain,
! [X0] :
( ~ decreases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| ~ subpopulation(first_movers,X0,sK3(sK0(sK2)))
| greater(zero,growth_rate(first_movers,sK3(sK0(sK2)))) ),
inference(resolution,[],[f363,f80]) ).
fof(f520,plain,
! [X0] :
( ~ decreases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(zero,growth_rate(first_movers,sK3(sK0(sK2)))) ),
inference(forward_subsumption_resolution,[],[f508,f71]) ).
fof(f521,plain,
! [X0] :
( ~ increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(growth_rate(first_movers,sK3(sK0(sK2))),zero) ),
inference(forward_subsumption_resolution,[],[f507,f71]) ).
fof(f522,plain,
! [X0] :
( ~ constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| zero = growth_rate(first_movers,sK3(sK0(sK2))) ),
inference(forward_subsumption_resolution,[],[f506,f71]) ).
fof(f577,plain,
! [X0] :
( ~ constant(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| ~ subpopulation(first_movers,X0,sK3(sK1(sK2)))
| zero = growth_rate(first_movers,sK3(sK1(sK2))) ),
inference(resolution,[],[f364,f82]) ).
fof(f578,plain,
! [X0] :
( ~ increases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| ~ subpopulation(first_movers,X0,sK3(sK1(sK2)))
| greater(growth_rate(first_movers,sK3(sK1(sK2))),zero) ),
inference(resolution,[],[f364,f81]) ).
fof(f579,plain,
! [X0] :
( ~ decreases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| ~ subpopulation(first_movers,X0,sK3(sK1(sK2)))
| greater(zero,growth_rate(first_movers,sK3(sK1(sK2)))) ),
inference(resolution,[],[f364,f80]) ).
fof(f588,plain,
! [X0] :
( ~ decreases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(zero,growth_rate(first_movers,sK3(sK1(sK2)))) ),
inference(forward_subsumption_resolution,[],[f579,f71]) ).
fof(f589,plain,
! [X0] :
( ~ increases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(growth_rate(first_movers,sK3(sK1(sK2))),zero) ),
inference(forward_subsumption_resolution,[],[f578,f71]) ).
fof(f590,plain,
! [X0] :
( ~ constant(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| zero = growth_rate(first_movers,sK3(sK1(sK2))) ),
inference(forward_subsumption_resolution,[],[f577,f71]) ).
fof(f681,plain,
( greater(sK0(sK2),sK1(sK2))
| sK0(sK2) = sK1(sK2)
| greater(sK1(sK2),sK0(sK2)) ),
inference(resolution,[],[f173,f123]) ).
fof(f683,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| sK3(X0) = sK1(sK2)
| greater(sK1(sK2),sK3(X0))
| greater(sK3(X0),sK1(sK2)) ),
inference(resolution,[],[f173,f138]) ).
fof(f857,plain,
( constant(number_of_organizations(sK2,sK3(equilibrium(sK2))))
| ~ spl4_4
| ~ spl4_5
| ~ spl4_30 ),
inference(superposition,[],[f315,f444]) ).
fof(f1092,plain,
( greater(sK3(equilibrium(sK2)),equilibrium(sK2))
| ~ spl4_29
| ~ spl4_30 ),
inference(forward_demodulation,[],[f407,f444]) ).
fof(f1098,definition,
( spl4_47
<=> greater(sK3(equilibrium(sK2)),equilibrium(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_47])],[avatar_definition]) ).
fof(f1100,plain,
( greater(sK3(equilibrium(sK2)),equilibrium(sK2))
| ~ spl4_47 ),
inference(avatar_component_clause,[],[f1098]) ).
fof(f1106,plain,
( ! [X0] :
( ~ increases(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(growth_rate(first_movers,sK3(sK0(sK2))),zero) )
| ~ spl4_30 ),
inference(forward_demodulation,[],[f521,f444]) ).
fof(f1107,plain,
( ! [X0] :
( ~ constant(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| zero = growth_rate(first_movers,sK3(sK0(sK2))) )
| ~ spl4_30 ),
inference(forward_demodulation,[],[f522,f444]) ).
fof(f1138,definition,
( spl4_54
<=> greater(sK3(equilibrium(sK2)),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_54])],[avatar_definition]) ).
fof(f1139,plain,
( ~ greater(sK3(equilibrium(sK2)),sK1(sK2))
| spl4_54 ),
inference(avatar_component_clause,[],[f1138]) ).
fof(f1140,plain,
( greater(sK3(equilibrium(sK2)),sK1(sK2))
| ~ spl4_54 ),
inference(avatar_component_clause,[],[f1138]) ).
fof(f1153,plain,
( spl4_47
| ~ spl4_29
| ~ spl4_30 ),
inference(avatar_split_clause,[],[f1092,f442,f405,f1098]) ).
fof(f1155,plain,
( ! [X0] :
( ~ in_environment(X0,sK3(equilibrium(sK2)))
| ~ increases(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| ~ environment(X0)
| greater(growth_rate(first_movers,sK3(sK0(sK2))),zero) )
| ~ spl4_30 ),
inference(forward_demodulation,[],[f1106,f444]) ).
fof(f1156,plain,
( ! [X0] :
( ~ in_environment(X0,sK3(equilibrium(sK2)))
| ~ constant(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| ~ environment(X0)
| zero = growth_rate(first_movers,sK3(sK0(sK2))) )
| ~ spl4_30 ),
inference(forward_demodulation,[],[f1107,f444]) ).
fof(f1170,plain,
( ! [X0] :
( greater(growth_rate(first_movers,sK3(equilibrium(sK2))),zero)
| ~ in_environment(X0,sK3(equilibrium(sK2)))
| ~ increases(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| ~ environment(X0) )
| ~ spl4_30 ),
inference(forward_demodulation,[],[f1155,f444]) ).
fof(f1171,plain,
( ! [X0] :
( zero = growth_rate(first_movers,sK3(equilibrium(sK2)))
| ~ in_environment(X0,sK3(equilibrium(sK2)))
| ~ constant(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| ~ environment(X0) )
| ~ spl4_30 ),
inference(forward_demodulation,[],[f1156,f444]) ).
fof(f1189,definition,
( spl4_56
<=> ! [X0] :
( ~ in_environment(X0,sK3(equilibrium(sK2)))
| ~ environment(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_56])],[avatar_definition]) ).
fof(f1190,plain,
( ! [X0] :
( ~ in_environment(X0,sK3(equilibrium(sK2)))
| ~ environment(X0) )
| ~ spl4_56 ),
inference(avatar_component_clause,[],[f1189]) ).
fof(f1197,definition,
( spl4_58
<=> increases(cardinality_at_time(first_movers,sK3(equilibrium(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_58])],[avatar_definition]) ).
fof(f1199,plain,
( ~ increases(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| spl4_58 ),
inference(avatar_component_clause,[],[f1197]) ).
fof(f1201,definition,
( spl4_59
<=> greater(growth_rate(first_movers,sK3(equilibrium(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_59])],[avatar_definition]) ).
fof(f1203,plain,
( greater(growth_rate(first_movers,sK3(equilibrium(sK2))),zero)
| ~ spl4_59 ),
inference(avatar_component_clause,[],[f1201]) ).
fof(f1204,plain,
( ~ spl4_58
| spl4_56
| spl4_59
| ~ spl4_30 ),
inference(avatar_split_clause,[],[f1170,f442,f1201,f1189,f1197]) ).
fof(f1206,definition,
( spl4_60
<=> constant(cardinality_at_time(first_movers,sK3(equilibrium(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f1210,definition,
( spl4_61
<=> zero = growth_rate(first_movers,sK3(equilibrium(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_61])],[avatar_definition]) ).
fof(f1212,plain,
( zero = growth_rate(first_movers,sK3(equilibrium(sK2)))
| ~ spl4_61 ),
inference(avatar_component_clause,[],[f1210]) ).
fof(f1213,plain,
( ~ spl4_60
| spl4_56
| spl4_61
| ~ spl4_30 ),
inference(avatar_split_clause,[],[f1171,f442,f1210,f1189,f1206]) ).
fof(f1258,definition,
( spl4_66
<=> greater(sK0(sK2),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_66])],[avatar_definition]) ).
fof(f1259,plain,
( ~ greater(sK0(sK2),sK1(sK2))
| spl4_66 ),
inference(avatar_component_clause,[],[f1258]) ).
fof(f1260,plain,
( greater(sK0(sK2),sK1(sK2))
| ~ spl4_66 ),
inference(avatar_component_clause,[],[f1258]) ).
fof(f1262,definition,
( spl4_67
<=> sK0(sK2) = sK1(sK2) ),
introduced(definition,[new_symbols(definition,[spl4_67])],[avatar_definition]) ).
fof(f1264,plain,
( sK0(sK2) = sK1(sK2)
| ~ spl4_67 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1266,definition,
( spl4_68
<=> greater(sK1(sK2),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_68])],[avatar_definition]) ).
fof(f1268,plain,
( greater(sK1(sK2),sK0(sK2))
| ~ spl4_68 ),
inference(avatar_component_clause,[],[f1266]) ).
fof(f1270,plain,
( spl4_68
| spl4_67
| spl4_66 ),
inference(avatar_split_clause,[],[f681,f1258,f1262,f1266]) ).
fof(f1308,definition,
( spl4_76
<=> greater(zero,growth_rate(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_76])],[avatar_definition]) ).
fof(f1310,plain,
( greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ spl4_76 ),
inference(avatar_component_clause,[],[f1308]) ).
fof(f1312,definition,
( spl4_77
<=> decreases(cardinality_at_time(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_77])],[avatar_definition]) ).
fof(f1314,plain,
( ~ decreases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| spl4_77 ),
inference(avatar_component_clause,[],[f1312]) ).
fof(f1315,plain,
( spl4_76
| spl4_12
| ~ spl4_77 ),
inference(avatar_split_clause,[],[f520,f1312,f306,f1308]) ).
fof(f1317,definition,
( spl4_78
<=> greater(growth_rate(first_movers,sK3(sK0(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_78])],[avatar_definition]) ).
fof(f1319,plain,
( greater(growth_rate(first_movers,sK3(sK0(sK2))),zero)
| ~ spl4_78 ),
inference(avatar_component_clause,[],[f1317]) ).
fof(f1321,definition,
( spl4_79
<=> increases(cardinality_at_time(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_79])],[avatar_definition]) ).
fof(f1323,plain,
( ~ increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| spl4_79 ),
inference(avatar_component_clause,[],[f1321]) ).
fof(f1324,plain,
( spl4_78
| spl4_12
| ~ spl4_79 ),
inference(avatar_split_clause,[],[f521,f1321,f306,f1317]) ).
fof(f1326,definition,
( spl4_80
<=> zero = growth_rate(first_movers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_80])],[avatar_definition]) ).
fof(f1328,plain,
( zero = growth_rate(first_movers,sK3(sK0(sK2)))
| ~ spl4_80 ),
inference(avatar_component_clause,[],[f1326]) ).
fof(f1330,definition,
( spl4_81
<=> constant(cardinality_at_time(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_81])],[avatar_definition]) ).
fof(f1333,plain,
( spl4_80
| spl4_12
| ~ spl4_81 ),
inference(avatar_split_clause,[],[f522,f1330,f306,f1326]) ).
fof(f1335,definition,
( spl4_82
<=> greater(sK1(sK2),sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_82])],[avatar_definition]) ).
fof(f1337,plain,
( greater(sK1(sK2),sK3(sK0(sK2)))
| ~ spl4_82 ),
inference(avatar_component_clause,[],[f1335]) ).
fof(f1339,definition,
( spl4_83
<=> sK1(sK2) = sK3(sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_83])],[avatar_definition]) ).
fof(f1340,plain,
( sK1(sK2) != sK3(sK0(sK2))
| spl4_83 ),
inference(avatar_component_clause,[],[f1339]) ).
fof(f1341,plain,
( sK1(sK2) = sK3(sK0(sK2))
| ~ spl4_83 ),
inference(avatar_component_clause,[],[f1339]) ).
fof(f1343,definition,
( spl4_84
<=> greater(sK3(sK0(sK2)),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_84])],[avatar_definition]) ).
fof(f1344,plain,
( ~ greater(sK3(sK0(sK2)),sK1(sK2))
| spl4_84 ),
inference(avatar_component_clause,[],[f1343]) ).
fof(f1345,plain,
( greater(sK3(sK0(sK2)),sK1(sK2))
| ~ spl4_84 ),
inference(avatar_component_clause,[],[f1343]) ).
fof(f1352,plain,
( ! [X0] :
( ~ greater(X0,sK0(sK2))
| greater(X0,equilibrium(sK2)) )
| ~ spl4_31 ),
inference(resolution,[],[f448,f87]) ).
fof(f1354,plain,
( ~ greater(equilibrium(sK2),sK0(sK2))
| ~ spl4_31 ),
inference(resolution,[],[f448,f86]) ).
fof(f1359,plain,
( ! [X0] :
( ~ greater(X0,sK3(sK0(sK2)))
| greater(X0,sK0(sK2)) )
| ~ spl4_29 ),
inference(resolution,[],[f407,f87]) ).
fof(f1371,plain,
( greater(sK3(sK0(sK2)),equilibrium(sK2))
| ~ spl4_29
| ~ spl4_31 ),
inference(resolution,[],[f1352,f407]) ).
fof(f1374,plain,
( ~ greater(equilibrium(sK2),sK3(sK0(sK2)))
| ~ spl4_29
| ~ spl4_31 ),
inference(resolution,[],[f1371,f86]) ).
fof(f1375,plain,
( greater(sK1(sK2),sK0(sK2))
| ~ spl4_29
| ~ spl4_82 ),
inference(resolution,[],[f1359,f1337]) ).
fof(f1385,plain,
( greater(equilibrium(sK2),sK0(sK2))
| ~ spl4_6
| ~ spl4_28 ),
inference(forward_demodulation,[],[f233,f403]) ).
fof(f1387,plain,
( $false
| ~ spl4_6
| ~ spl4_28
| ~ spl4_31 ),
inference(forward_subsumption_resolution,[],[f1385,f1354]) ).
fof(f1388,plain,
( ~ spl4_6
| ~ spl4_28
| ~ spl4_31 ),
inference(avatar_contradiction_clause,[],[f1387]) ).
fof(f1400,plain,
( greater(equilibrium(sK2),equilibrium(sK2))
| ~ spl4_6
| ~ spl4_28
| ~ spl4_30 ),
inference(forward_demodulation,[],[f1385,f444]) ).
fof(f1405,plain,
( $false
| ~ spl4_6
| ~ spl4_28
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f1400,f120]) ).
fof(f1406,plain,
( ~ spl4_6
| ~ spl4_28
| ~ spl4_30 ),
inference(avatar_contradiction_clause,[],[f1405]) ).
fof(f1412,plain,
( ~ spl4_6
| ~ spl4_29
| ~ spl4_31 ),
inference(avatar_split_clause,[],[f1374,f446,f405,f231]) ).
fof(f1413,plain,
( spl4_68
| ~ spl4_29
| ~ spl4_82 ),
inference(avatar_split_clause,[],[f1375,f1335,f405,f1266]) ).
fof(f1421,plain,
( greater(cardinality_at_time(efficient_producers,sK3(equilibrium(sK2))),zero)
| ~ spl4_30 ),
inference(resolution,[],[f450,f159]) ).
fof(f1479,plain,
( ~ greater(equilibrium(sK2),sK1(sK2))
| ~ spl4_30
| spl4_66 ),
inference(superposition,[],[f1259,f444]) ).
fof(f1483,definition,
( spl4_85
<=> greater(zero,growth_rate(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_85])],[avatar_definition]) ).
fof(f1484,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| spl4_85 ),
inference(avatar_component_clause,[],[f1483]) ).
fof(f1485,plain,
( greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ spl4_85 ),
inference(avatar_component_clause,[],[f1483]) ).
fof(f1487,definition,
( spl4_86
<=> decreases(cardinality_at_time(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_86])],[avatar_definition]) ).
fof(f1489,plain,
( ~ decreases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| spl4_86 ),
inference(avatar_component_clause,[],[f1487]) ).
fof(f1490,plain,
( spl4_85
| spl4_9
| ~ spl4_86 ),
inference(avatar_split_clause,[],[f588,f1487,f294,f1483]) ).
fof(f1492,definition,
( spl4_87
<=> greater(growth_rate(first_movers,sK3(sK1(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_87])],[avatar_definition]) ).
fof(f1496,definition,
( spl4_88
<=> increases(cardinality_at_time(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_88])],[avatar_definition]) ).
fof(f1498,plain,
( ~ increases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| spl4_88 ),
inference(avatar_component_clause,[],[f1496]) ).
fof(f1499,plain,
( spl4_87
| spl4_9
| ~ spl4_88 ),
inference(avatar_split_clause,[],[f589,f1496,f294,f1492]) ).
fof(f1501,definition,
( spl4_89
<=> zero = growth_rate(first_movers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_89])],[avatar_definition]) ).
fof(f1503,plain,
( zero = growth_rate(first_movers,sK3(sK1(sK2)))
| ~ spl4_89 ),
inference(avatar_component_clause,[],[f1501]) ).
fof(f1505,definition,
( spl4_90
<=> constant(cardinality_at_time(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_90])],[avatar_definition]) ).
fof(f1508,plain,
( spl4_89
| spl4_9
| ~ spl4_90 ),
inference(avatar_split_clause,[],[f590,f1505,f294,f1501]) ).
fof(f1512,definition,
( spl4_91
<=> greater(sK1(sK2),equilibrium(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_91])],[avatar_definition]) ).
fof(f1513,plain,
( ~ greater(sK1(sK2),equilibrium(sK2))
| spl4_91 ),
inference(avatar_component_clause,[],[f1512]) ).
fof(f1514,plain,
( greater(sK1(sK2),equilibrium(sK2))
| ~ spl4_91 ),
inference(avatar_component_clause,[],[f1512]) ).
fof(f1520,definition,
( spl4_93
<=> greater(equilibrium(sK2),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_93])],[avatar_definition]) ).
fof(f1521,plain,
( ~ greater(equilibrium(sK2),sK1(sK2))
| spl4_93 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1522,plain,
( greater(equilibrium(sK2),sK1(sK2))
| ~ spl4_93 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1524,plain,
( ~ spl4_93
| ~ spl4_30
| spl4_66 ),
inference(avatar_split_clause,[],[f1479,f1258,f442,f1520]) ).
fof(f1533,plain,
( greater(sK1(sK2),equilibrium(sK2))
| ~ spl4_30
| ~ spl4_68 ),
inference(superposition,[],[f1268,f444]) ).
fof(f1542,plain,
( ! [X0] :
( ~ greater(X0,sK3(sK1(sK2)))
| greater(X0,sK1(sK2)) )
| ~ spl4_27 ),
inference(resolution,[],[f398,f87]) ).
fof(f1567,plain,
! [X0] :
( ~ greater(X0,growth_rate(efficient_producers,sK3(sK1(sK2))))
| greater(X0,growth_rate(first_movers,sK3(sK1(sK2)))) ),
inference(resolution,[],[f430,f87]) ).
fof(f1575,plain,
( ~ greater(sK3(sK0(sK2)),equilibrium(sK2))
| ~ spl4_6 ),
inference(resolution,[],[f233,f86]) ).
fof(f1577,plain,
( ~ greater(sK3(equilibrium(sK2)),equilibrium(sK2))
| ~ spl4_6
| ~ spl4_30 ),
inference(forward_demodulation,[],[f1575,f444]) ).
fof(f1580,plain,
( $false
| ~ spl4_6
| ~ spl4_30
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f1577,f1100]) ).
fof(f1581,plain,
( ~ spl4_6
| ~ spl4_30
| ~ spl4_47 ),
inference(avatar_contradiction_clause,[],[f1580]) ).
fof(f1598,plain,
( ~ greater(equilibrium(sK2),sK1(sK2))
| ~ spl4_91 ),
inference(resolution,[],[f1514,f86]) ).
fof(f1606,plain,
( greater(equilibrium(sK2),sK1(sK2))
| ~ spl4_3
| ~ spl4_27 ),
inference(resolution,[],[f1542,f220]) ).
fof(f1639,plain,
( constant(number_of_organizations(sK2,sK3(sK1(sK2))))
| ~ environment(sK2)
| ~ in_environment(sK2,sK3(sK1(sK2)))
| ~ spl4_1 ),
inference(resolution,[],[f212,f100]) ).
fof(f1641,plain,
( constant(number_of_organizations(sK2,sK3(sK1(sK2))))
| ~ in_environment(sK2,sK3(sK1(sK2)))
| ~ spl4_1 ),
inference(forward_subsumption_resolution,[],[f1639,f106]) ).
fof(f1642,plain,
( constant(number_of_organizations(sK2,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2 ),
inference(forward_subsumption_resolution,[],[f1641,f215]) ).
fof(f1897,plain,
( sK1(sK2) = sK3(sK0(sK2))
| greater(sK1(sK2),sK3(sK0(sK2)))
| greater(sK3(sK0(sK2)),sK1(sK2)) ),
inference(resolution,[],[f683,f123]) ).
fof(f2024,plain,
( ! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK3(equilibrium(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(equilibrium(sK2)))
| ~ subpopulation(efficient_producers,X0,sK3(equilibrium(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2)))) )
| ~ spl4_30 ),
inference(resolution,[],[f1421,f80]) ).
fof(f2211,definition,
( spl4_101
<=> greater_or_equal(sK3(equilibrium(sK2)),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_101])],[avatar_definition]) ).
fof(f2212,plain,
( greater_or_equal(sK3(equilibrium(sK2)),sK1(sK2))
| ~ spl4_101 ),
inference(avatar_component_clause,[],[f2211]) ).
fof(f2213,plain,
( ~ greater_or_equal(sK3(equilibrium(sK2)),sK1(sK2))
| spl4_101 ),
inference(avatar_component_clause,[],[f2211]) ).
fof(f2215,definition,
( spl4_102
<=> greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),growth_rate(first_movers,sK3(equilibrium(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_102])],[avatar_definition]) ).
fof(f2217,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),growth_rate(first_movers,sK3(equilibrium(sK2))))
| ~ spl4_102 ),
inference(avatar_component_clause,[],[f2215]) ).
fof(f2766,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK1(sK2))))
| decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK1(sK2)))) ),
inference(superposition,[],[f115,f189]) ).
fof(f2768,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK1(sK2))))
| increases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
inference(superposition,[],[f117,f189]) ).
fof(f2769,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK1(sK2))))
| decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| decreases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
inference(superposition,[],[f118,f189]) ).
fof(f2813,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK0(sK2)))) ),
inference(superposition,[],[f113,f190]) ).
fof(f2815,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK0(sK2)))) ),
inference(superposition,[],[f115,f190]) ).
fof(f2817,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
inference(superposition,[],[f117,f190]) ).
fof(f2818,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| decreases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
inference(superposition,[],[f118,f190]) ).
fof(f2822,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| spl4_79 ),
inference(forward_subsumption_resolution,[],[f2817,f1323]) ).
fof(f2830,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| spl4_17
| spl4_79 ),
inference(forward_subsumption_resolution,[],[f2822,f336]) ).
fof(f2838,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| spl4_17
| spl4_21
| spl4_79 ),
inference(forward_subsumption_resolution,[],[f2830,f358]) ).
fof(f2869,plain,
( decreases(cardinality_at_time(efficient_producers,sK3(equilibrium(sK2))))
| ~ spl4_13
| ~ spl4_30 ),
inference(forward_demodulation,[],[f310,f444]) ).
fof(f2873,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| spl4_17 ),
inference(forward_subsumption_resolution,[],[f2813,f336]) ).
fof(f2875,plain,
( ! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK3(equilibrium(sK2))))
| ~ environment(X0)
| ~ in_environment(X0,sK3(equilibrium(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2)))) )
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f2024,f70]) ).
fof(f2887,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(equilibrium(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2)))) )
| ~ spl4_13
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f2875,f2869]) ).
fof(f2897,definition,
( spl4_126
<=> greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_126])],[avatar_definition]) ).
fof(f2899,plain,
( greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| ~ spl4_126 ),
inference(avatar_component_clause,[],[f2897]) ).
fof(f2900,plain,
( spl4_126
| spl4_56
| ~ spl4_13
| ~ spl4_30 ),
inference(avatar_split_clause,[],[f2887,f442,f309,f1189,f2897]) ).
fof(f2930,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,equilibrium(sK2))
| ~ spl4_56 ),
inference(resolution,[],[f1190,f138]) ).
fof(f2931,plain,
( ~ in_environment(sK2,equilibrium(sK2))
| ~ spl4_56 ),
inference(forward_subsumption_resolution,[],[f2930,f106]) ).
fof(f2934,plain,
( $false
| ~ spl4_30
| ~ spl4_56 ),
inference(forward_subsumption_resolution,[],[f2931,f450]) ).
fof(f2935,plain,
( ~ spl4_30
| ~ spl4_56 ),
inference(avatar_contradiction_clause,[],[f2934]) ).
fof(f2942,plain,
( ~ constant(number_of_organizations(sK2,sK3(equilibrium(sK2))))
| increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| spl4_17
| ~ spl4_30 ),
inference(forward_demodulation,[],[f2873,f444]) ).
fof(f2954,plain,
( increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5
| spl4_17
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f2942,f857]) ).
fof(f2962,plain,
( increases(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5
| spl4_17
| ~ spl4_30 ),
inference(forward_demodulation,[],[f2954,f444]) ).
fof(f2970,plain,
( constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5
| spl4_17
| ~ spl4_30
| spl4_58 ),
inference(forward_subsumption_resolution,[],[f2962,f1199]) ).
fof(f2978,plain,
( constant(cardinality_at_time(first_movers,sK3(equilibrium(sK2))))
| ~ spl4_4
| ~ spl4_5
| spl4_17
| ~ spl4_30
| spl4_58 ),
inference(forward_demodulation,[],[f2970,f444]) ).
fof(f3047,plain,
( greater(sK1(sK2),sK3(sK0(sK2)))
| sK1(sK2) = sK3(sK0(sK2))
| greater(sK3(sK0(sK2)),sK1(sK2))
| ~ spl4_5 ),
inference(resolution,[],[f269,f125]) ).
fof(f3636,plain,
( ~ greater(growth_rate(first_movers,sK3(equilibrium(sK2))),growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| ~ spl4_102 ),
inference(resolution,[],[f2217,f86]) ).
fof(f3657,plain,
( greater(sK3(equilibrium(sK2)),sK1(sK2))
| ~ spl4_30
| ~ spl4_84 ),
inference(forward_demodulation,[],[f1345,f444]) ).
fof(f3679,plain,
( greater_or_equal(sK3(equilibrium(sK2)),sK1(sK2))
| ~ spl4_54 ),
inference(resolution,[],[f1140,f91]) ).
fof(f3681,plain,
( $false
| ~ spl4_54
| spl4_101 ),
inference(forward_subsumption_resolution,[],[f3679,f2213]) ).
fof(f3682,plain,
( ~ spl4_54
| spl4_101 ),
inference(avatar_contradiction_clause,[],[f3681]) ).
fof(f3683,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),growth_rate(first_movers,sK3(equilibrium(sK2))))
| ~ in_environment(sK2,equilibrium(sK2))
| ~ spl4_101 ),
inference(resolution,[],[f2212,f253]) ).
fof(f3685,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),growth_rate(first_movers,sK3(equilibrium(sK2))))
| ~ spl4_30
| ~ spl4_101 ),
inference(forward_subsumption_resolution,[],[f3683,f450]) ).
fof(f3690,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ~ spl4_16
| ~ spl4_30 ),
inference(forward_demodulation,[],[f332,f444]) ).
fof(f3770,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| ~ spl4_61
| ~ spl4_102 ),
inference(forward_demodulation,[],[f3636,f1212]) ).
fof(f3776,plain,
( $false
| ~ spl4_61
| ~ spl4_102
| ~ spl4_126 ),
inference(forward_subsumption_resolution,[],[f3770,f2899]) ).
fof(f3777,plain,
( ~ spl4_61
| ~ spl4_102
| ~ spl4_126 ),
inference(avatar_contradiction_clause,[],[f3776]) ).
fof(f3789,plain,
( spl4_102
| ~ spl4_30
| ~ spl4_101 ),
inference(avatar_split_clause,[],[f3685,f2211,f442,f2215]) ).
fof(f3805,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK3(equilibrium(sK2))))
| ~ spl4_16
| ~ spl4_30 ),
inference(resolution,[],[f3690,f86]) ).
fof(f3806,plain,
( $false
| ~ spl4_16
| ~ spl4_30
| ~ spl4_126 ),
inference(forward_subsumption_resolution,[],[f3805,f2899]) ).
fof(f3807,plain,
( ~ spl4_16
| ~ spl4_30
| ~ spl4_126 ),
inference(avatar_contradiction_clause,[],[f3806]) ).
fof(f4381,plain,
( greater(equilibrium(sK2),sK1(sK2))
| ~ spl4_3
| ~ spl4_26 ),
inference(forward_demodulation,[],[f220,f394]) ).
fof(f4422,plain,
( $false
| ~ spl4_3
| ~ spl4_26
| spl4_93 ),
inference(forward_subsumption_resolution,[],[f4381,f1521]) ).
fof(f4423,plain,
( ~ spl4_3
| ~ spl4_26
| spl4_93 ),
inference(avatar_contradiction_clause,[],[f4422]) ).
fof(f4527,plain,
( ! [X0] :
( ~ greater(X0,equilibrium(sK2))
| greater(X0,sK1(sK2)) )
| ~ spl4_93 ),
inference(resolution,[],[f1522,f87]) ).
fof(f4531,plain,
( greater(sK3(equilibrium(sK2)),sK1(sK2))
| ~ spl4_47
| ~ spl4_93 ),
inference(resolution,[],[f4527,f1100]) ).
fof(f5130,plain,
( ~ greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| spl4_16
| ~ spl4_30 ),
inference(forward_demodulation,[],[f331,f444]) ).
fof(f5144,plain,
( ! [X0] :
( ~ greater(X0,growth_rate(first_movers,sK3(equilibrium(sK2))))
| greater(X0,zero) )
| ~ spl4_59 ),
inference(resolution,[],[f1203,f87]) ).
fof(f5153,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ~ spl4_59
| ~ spl4_102 ),
inference(resolution,[],[f5144,f2217]) ).
fof(f5154,plain,
( $false
| spl4_16
| ~ spl4_30
| ~ spl4_59
| ~ spl4_102 ),
inference(forward_subsumption_resolution,[],[f5153,f5130]) ).
fof(f5155,plain,
( spl4_16
| ~ spl4_30
| ~ spl4_59
| ~ spl4_102 ),
inference(avatar_contradiction_clause,[],[f5154]) ).
fof(f5162,plain,
( $false
| ~ spl4_30
| spl4_54
| ~ spl4_84 ),
inference(forward_subsumption_resolution,[],[f3657,f1139]) ).
fof(f5163,plain,
( ~ spl4_30
| spl4_54
| ~ spl4_84 ),
inference(avatar_contradiction_clause,[],[f5162]) ).
fof(f5165,plain,
( $false
| ~ spl4_47
| spl4_54
| ~ spl4_93 ),
inference(forward_subsumption_resolution,[],[f4531,f1139]) ).
fof(f5166,plain,
( ~ spl4_47
| spl4_54
| ~ spl4_93 ),
inference(avatar_contradiction_clause,[],[f5165]) ).
fof(f5200,plain,
( spl4_91
| ~ spl4_30
| ~ spl4_68 ),
inference(avatar_split_clause,[],[f1533,f1266,f442,f1512]) ).
fof(f5210,plain,
( ~ spl4_93
| ~ spl4_91 ),
inference(avatar_split_clause,[],[f1598,f1512,f1520]) ).
fof(f5349,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK1(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f2766,f299]) ).
fof(f5461,plain,
( increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f5349,f1642]) ).
fof(f5492,plain,
( constant(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2
| spl4_10
| spl4_15 ),
inference(forward_subsumption_resolution,[],[f5461,f327]) ).
fof(f5589,plain,
( greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ spl4_18 ),
inference(superposition,[],[f430,f345]) ).
fof(f5603,plain,
( ~ greater(growth_rate(first_movers,sK3(sK1(sK2))),zero)
| ~ spl4_85 ),
inference(resolution,[],[f1485,f86]) ).
fof(f5610,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ spl4_89 ),
inference(superposition,[],[f430,f1503]) ).
fof(f5613,plain,
( $false
| spl4_14
| ~ spl4_89 ),
inference(forward_subsumption_resolution,[],[f5610,f322]) ).
fof(f5614,plain,
( spl4_14
| ~ spl4_89 ),
inference(avatar_contradiction_clause,[],[f5613]) ).
fof(f5621,plain,
( greater(zero,zero)
| ~ spl4_8
| ~ spl4_18 ),
inference(forward_demodulation,[],[f292,f345]) ).
fof(f5647,plain,
( $false
| ~ spl4_8
| ~ spl4_18 ),
inference(forward_subsumption_resolution,[],[f5621,f120]) ).
fof(f5648,plain,
( ~ spl4_8
| ~ spl4_18 ),
inference(avatar_contradiction_clause,[],[f5647]) ).
fof(f5720,plain,
( greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ spl4_8 ),
inference(resolution,[],[f292,f1567]) ).
fof(f5725,plain,
( $false
| ~ spl4_8
| spl4_85 ),
inference(forward_subsumption_resolution,[],[f5720,f1484]) ).
fof(f5726,plain,
( ~ spl4_8
| spl4_85 ),
inference(avatar_contradiction_clause,[],[f5725]) ).
fof(f5727,plain,
( ~ spl4_87
| ~ spl4_85 ),
inference(avatar_split_clause,[],[f5603,f1483,f1492]) ).
fof(f5729,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK1(sK2))
| ~ spl4_9 ),
inference(resolution,[],[f295,f138]) ).
fof(f5730,plain,
( ~ in_environment(sK2,sK1(sK2))
| ~ spl4_9 ),
inference(forward_subsumption_resolution,[],[f5729,f106]) ).
fof(f5733,plain,
( $false
| ~ spl4_9 ),
inference(forward_subsumption_resolution,[],[f5730,f125]) ).
fof(f5734,plain,
~ spl4_9,
inference(avatar_contradiction_clause,[],[f5733]) ).
fof(f5736,plain,
( spl4_90
| ~ spl4_1
| ~ spl4_2
| spl4_10
| spl4_15 ),
inference(avatar_split_clause,[],[f5492,f325,f297,f214,f210,f1505]) ).
fof(f5748,plain,
( spl4_60
| ~ spl4_4
| ~ spl4_5
| spl4_17
| ~ spl4_30
| spl4_58 ),
inference(avatar_split_clause,[],[f2978,f1197,f442,f334,f227,f223,f1206]) ).
fof(f5763,plain,
( increases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2 ),
inference(forward_subsumption_resolution,[],[f2768,f1642]) ).
fof(f5778,plain,
( decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| decreases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2 ),
inference(forward_subsumption_resolution,[],[f2769,f1642]) ).
fof(f5785,plain,
( increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2
| spl4_88 ),
inference(forward_subsumption_resolution,[],[f5763,f1498]) ).
fof(f5800,plain,
( decreases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f5778,f299]) ).
fof(f5806,plain,
( constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2
| spl4_15
| spl4_88 ),
inference(forward_subsumption_resolution,[],[f5785,f327]) ).
fof(f5821,plain,
( constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_1
| ~ spl4_2
| spl4_10
| spl4_86 ),
inference(forward_subsumption_resolution,[],[f5800,f1489]) ).
fof(f5826,plain,
( $false
| ~ spl4_1
| ~ spl4_2
| spl4_15
| spl4_19
| spl4_88 ),
inference(forward_subsumption_resolution,[],[f5806,f349]) ).
fof(f5827,plain,
( ~ spl4_1
| ~ spl4_2
| spl4_15
| spl4_19
| spl4_88 ),
inference(avatar_contradiction_clause,[],[f5826]) ).
fof(f5844,plain,
( $false
| ~ spl4_1
| ~ spl4_2
| spl4_10
| spl4_19
| spl4_86 ),
inference(forward_subsumption_resolution,[],[f5821,f349]) ).
fof(f5845,plain,
( ~ spl4_1
| ~ spl4_2
| spl4_10
| spl4_19
| spl4_86 ),
inference(avatar_contradiction_clause,[],[f5844]) ).
fof(f5854,plain,
( $false
| ~ spl4_18
| spl4_85 ),
inference(forward_subsumption_resolution,[],[f5589,f1484]) ).
fof(f5855,plain,
( ~ spl4_18
| spl4_85 ),
inference(avatar_contradiction_clause,[],[f5854]) ).
fof(f5866,plain,
( greater_or_equal(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ spl4_14 ),
inference(resolution,[],[f323,f91]) ).
fof(f5887,plain,
( ! [X0,X1] :
( ~ greater(zero,growth_rate(X0,sK3(sK1(sK2))))
| outcompetes(efficient_producers,X0,sK3(sK1(sK2)))
| ~ environment(X1)
| ~ subpopulations(X0,efficient_producers,X1,sK3(sK1(sK2))) )
| ~ spl4_14 ),
inference(resolution,[],[f5866,f93]) ).
fof(f6023,plain,
( ! [X0] :
( outcompetes(efficient_producers,first_movers,sK3(sK1(sK2)))
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2))) )
| ~ spl4_14
| ~ spl4_85 ),
inference(resolution,[],[f5887,f1485]) ).
fof(f6372,definition,
( spl4_218
<=> ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_218])],[avatar_definition]) ).
fof(f6373,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2)))
| ~ environment(X0) )
| ~ spl4_218 ),
inference(avatar_component_clause,[],[f6372]) ).
fof(f6375,definition,
( spl4_219
<=> outcompetes(efficient_producers,first_movers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_219])],[avatar_definition]) ).
fof(f6377,plain,
( outcompetes(efficient_producers,first_movers,sK3(sK1(sK2)))
| ~ spl4_219 ),
inference(avatar_component_clause,[],[f6375]) ).
fof(f6378,plain,
( spl4_218
| spl4_219
| ~ spl4_14
| ~ spl4_85 ),
inference(avatar_split_clause,[],[f6023,f1483,f321,f6375,f6372]) ).
fof(f7106,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK1(sK2))
| ~ spl4_218 ),
inference(resolution,[],[f6373,f108]) ).
fof(f7107,plain,
( ~ in_environment(sK2,sK1(sK2))
| ~ spl4_218 ),
inference(forward_subsumption_resolution,[],[f7106,f106]) ).
fof(f7108,plain,
( $false
| ~ spl4_218 ),
inference(forward_subsumption_resolution,[],[f7107,f125]) ).
fof(f7109,plain,
~ spl4_218,
inference(avatar_contradiction_clause,[],[f7108]) ).
fof(f7111,plain,
( ~ in_environment(sK2,sK1(sK2))
| ~ spl4_219 ),
inference(resolution,[],[f6377,f109]) ).
fof(f7112,plain,
( $false
| ~ spl4_219 ),
inference(forward_subsumption_resolution,[],[f7111,f125]) ).
fof(f7113,plain,
~ spl4_219,
inference(avatar_contradiction_clause,[],[f7112]) ).
fof(f7117,plain,
( spl4_93
| ~ spl4_3
| ~ spl4_27 ),
inference(avatar_split_clause,[],[f1606,f396,f218,f1520]) ).
fof(f7367,plain,
( decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| decreases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5 ),
inference(forward_subsumption_resolution,[],[f2818,f315]) ).
fof(f7372,plain,
( decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5 ),
inference(forward_subsumption_resolution,[],[f2815,f315]) ).
fof(f7574,plain,
( ! [X0] :
( ~ greater(X0,sK0(sK2))
| greater(X0,equilibrium(sK2)) )
| ~ spl4_31 ),
inference(resolution,[],[f448,f87]) ).
fof(f7607,plain,
( greater_or_equal(sK3(sK0(sK2)),sK1(sK2))
| ~ spl4_84 ),
inference(resolution,[],[f1345,f91]) ).
fof(f7835,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_84 ),
inference(resolution,[],[f7607,f253]) ).
fof(f7837,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ~ spl4_84 ),
inference(forward_subsumption_resolution,[],[f7835,f123]) ).
fof(f7838,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ spl4_80
| ~ spl4_84 ),
inference(forward_demodulation,[],[f7837,f1328]) ).
fof(f7857,plain,
( ~ greater(equilibrium(sK2),sK1(sK2))
| spl4_6
| ~ spl4_83 ),
inference(superposition,[],[f232,f1341]) ).
fof(f7930,plain,
( $false
| spl4_6
| ~ spl4_83
| ~ spl4_93 ),
inference(forward_subsumption_resolution,[],[f7857,f1522]) ).
fof(f7931,plain,
( spl4_6
| ~ spl4_83
| ~ spl4_93 ),
inference(avatar_contradiction_clause,[],[f7930]) ).
fof(f7946,plain,
( increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5
| spl4_13 ),
inference(forward_subsumption_resolution,[],[f7372,f311]) ).
fof(f7950,plain,
( constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5
| spl4_13
| spl4_17 ),
inference(forward_subsumption_resolution,[],[f7946,f336]) ).
fof(f7961,plain,
( greater(sK1(sK2),equilibrium(sK2))
| ~ spl4_31
| ~ spl4_68 ),
inference(resolution,[],[f1268,f7574]) ).
fof(f7967,plain,
( $false
| ~ spl4_31
| ~ spl4_68
| spl4_91 ),
inference(forward_subsumption_resolution,[],[f7961,f1513]) ).
fof(f7968,plain,
( ~ spl4_31
| ~ spl4_68
| spl4_91 ),
inference(avatar_contradiction_clause,[],[f7967]) ).
fof(f7974,plain,
( greater(sK1(sK2),sK3(sK0(sK2)))
| greater(sK3(sK0(sK2)),sK1(sK2))
| spl4_83 ),
inference(forward_subsumption_resolution,[],[f1897,f1340]) ).
fof(f7975,plain,
( greater(sK1(sK2),sK3(sK0(sK2)))
| greater(sK3(sK0(sK2)),sK1(sK2))
| ~ spl4_5
| spl4_83 ),
inference(forward_subsumption_resolution,[],[f3047,f1340]) ).
fof(f8001,plain,
( greater(equilibrium(sK2),sK3(sK0(sK2)))
| ~ spl4_3
| ~ spl4_67 ),
inference(superposition,[],[f220,f1264]) ).
fof(f8197,plain,
( $false
| ~ spl4_3
| spl4_6
| ~ spl4_67 ),
inference(forward_subsumption_resolution,[],[f8001,f232]) ).
fof(f8198,plain,
( ~ spl4_3
| spl4_6
| ~ spl4_67 ),
inference(avatar_contradiction_clause,[],[f8197]) ).
fof(f8210,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_12 ),
inference(resolution,[],[f307,f138]) ).
fof(f8211,plain,
( ~ in_environment(sK2,sK0(sK2))
| ~ spl4_12 ),
inference(forward_subsumption_resolution,[],[f8210,f106]) ).
fof(f8214,plain,
( $false
| ~ spl4_12 ),
inference(forward_subsumption_resolution,[],[f8211,f123]) ).
fof(f8215,plain,
~ spl4_12,
inference(avatar_contradiction_clause,[],[f8214]) ).
fof(f8216,plain,
( greater(zero,zero)
| ~ spl4_11
| ~ spl4_20 ),
inference(forward_demodulation,[],[f304,f354]) ).
fof(f8217,plain,
( $false
| ~ spl4_11
| ~ spl4_20 ),
inference(forward_subsumption_resolution,[],[f8216,f120]) ).
fof(f8218,plain,
( ~ spl4_11
| ~ spl4_20 ),
inference(avatar_contradiction_clause,[],[f8217]) ).
fof(f8221,plain,
( spl4_81
| ~ spl4_4
| ~ spl4_5
| spl4_13
| spl4_17 ),
inference(avatar_split_clause,[],[f7950,f334,f309,f227,f223,f1330]) ).
fof(f8230,plain,
( ~ greater(sK0(sK2),sK1(sK2))
| ~ spl4_28
| spl4_84 ),
inference(forward_demodulation,[],[f1344,f403]) ).
fof(f8244,plain,
( $false
| ~ spl4_28
| ~ spl4_66
| spl4_84 ),
inference(forward_subsumption_resolution,[],[f8230,f1260]) ).
fof(f8245,plain,
( ~ spl4_28
| ~ spl4_66
| spl4_84 ),
inference(avatar_contradiction_clause,[],[f8244]) ).
fof(f8804,plain,
( $false
| ~ spl4_4
| ~ spl4_5
| spl4_17
| spl4_21
| spl4_79 ),
inference(forward_subsumption_resolution,[],[f2838,f315]) ).
fof(f8805,plain,
( ~ spl4_4
| ~ spl4_5
| spl4_17
| spl4_21
| spl4_79 ),
inference(avatar_contradiction_clause,[],[f8804]) ).
fof(f10209,plain,
( spl4_16
| ~ spl4_80
| ~ spl4_84 ),
inference(avatar_split_clause,[],[f7838,f1343,f1326,f330]) ).
fof(f10210,plain,
( spl4_84
| spl4_82
| spl4_83 ),
inference(avatar_split_clause,[],[f7974,f1339,f1335,f1343]) ).
fof(f10211,plain,
( spl4_84
| spl4_82
| ~ spl4_5
| spl4_83 ),
inference(avatar_split_clause,[],[f7975,f1339,f227,f1335,f1343]) ).
fof(f10240,plain,
( decreases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5
| spl4_13 ),
inference(forward_subsumption_resolution,[],[f7367,f311]) ).
fof(f10332,plain,
( constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_4
| ~ spl4_5
| spl4_13
| spl4_77 ),
inference(forward_subsumption_resolution,[],[f10240,f1314]) ).
fof(f10592,plain,
( ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ spl4_11 ),
inference(resolution,[],[f304,f86]) ).
fof(f10595,plain,
( spl4_21
| ~ spl4_4
| ~ spl4_5
| spl4_13
| spl4_77 ),
inference(avatar_split_clause,[],[f10332,f1312,f309,f227,f223,f356]) ).
fof(f10663,plain,
( greater_or_equal(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ spl4_16 ),
inference(resolution,[],[f332,f91]) ).
fof(f10674,plain,
( greater(zero,zero)
| ~ spl4_16
| ~ spl4_20 ),
inference(superposition,[],[f332,f354]) ).
fof(f10678,plain,
( $false
| ~ spl4_16
| ~ spl4_20 ),
inference(forward_subsumption_resolution,[],[f10674,f120]) ).
fof(f10679,plain,
( ~ spl4_16
| ~ spl4_20 ),
inference(avatar_contradiction_clause,[],[f10678]) ).
fof(f10745,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_84 ),
inference(resolution,[],[f7607,f253]) ).
fof(f10794,plain,
( ! [X0,X1] :
( ~ greater(zero,growth_rate(X0,sK3(sK0(sK2))))
| outcompetes(efficient_producers,X0,sK3(sK0(sK2)))
| ~ environment(X1)
| ~ subpopulations(X0,efficient_producers,X1,sK3(sK0(sK2))) )
| ~ spl4_16 ),
inference(resolution,[],[f10663,f93]) ).
fof(f11009,plain,
( ! [X0] :
( outcompetes(efficient_producers,first_movers,sK3(sK0(sK2)))
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2))) )
| ~ spl4_16
| ~ spl4_76 ),
inference(resolution,[],[f10794,f1310]) ).
fof(f11739,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ~ spl4_84 ),
inference(forward_subsumption_resolution,[],[f10745,f123]) ).
fof(f11743,definition,
( spl4_396
<=> ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_396])],[avatar_definition]) ).
fof(f11744,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2)))
| ~ environment(X0) )
| ~ spl4_396 ),
inference(avatar_component_clause,[],[f11743]) ).
fof(f11746,definition,
( spl4_397
<=> outcompetes(efficient_producers,first_movers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_397])],[avatar_definition]) ).
fof(f11748,plain,
( outcompetes(efficient_producers,first_movers,sK3(sK0(sK2)))
| ~ spl4_397 ),
inference(avatar_component_clause,[],[f11746]) ).
fof(f11749,plain,
( spl4_396
| spl4_397
| ~ spl4_16
| ~ spl4_76 ),
inference(avatar_split_clause,[],[f11009,f1308,f330,f11746,f11743]) ).
fof(f12002,plain,
( ~ in_environment(sK2,sK0(sK2))
| ~ spl4_397 ),
inference(resolution,[],[f11748,f109]) ).
fof(f12003,plain,
( $false
| ~ spl4_397 ),
inference(forward_subsumption_resolution,[],[f12002,f123]) ).
fof(f12004,plain,
~ spl4_397,
inference(avatar_contradiction_clause,[],[f12003]) ).
fof(f12187,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_396 ),
inference(resolution,[],[f11744,f108]) ).
fof(f12188,plain,
( ~ in_environment(sK2,sK0(sK2))
| ~ spl4_396 ),
inference(forward_subsumption_resolution,[],[f12187,f106]) ).
fof(f12189,plain,
( $false
| ~ spl4_396 ),
inference(forward_subsumption_resolution,[],[f12188,f123]) ).
fof(f12190,plain,
~ spl4_396,
inference(avatar_contradiction_clause,[],[f12189]) ).
fof(f12191,plain,
( ~ spl4_16
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f10592,f302,f330]) ).
fof(f12194,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sK3(sK0(sK2))))
| ~ greater(X0,zero) )
| ~ spl4_11 ),
inference(resolution,[],[f304,f87]) ).
fof(f12208,plain,
( ! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,zero)
| greater(X1,growth_rate(efficient_producers,sK3(sK0(sK2)))) )
| ~ spl4_11 ),
inference(resolution,[],[f12194,f87]) ).
fof(f16183,plain,
( ~ greater(growth_rate(first_movers,sK3(sK0(sK2))),zero)
| greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_11
| ~ spl4_84 ),
inference(resolution,[],[f11739,f12208]) ).
fof(f16191,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_11
| ~ spl4_78
| ~ spl4_84 ),
inference(forward_subsumption_resolution,[],[f16183,f1319]) ).
fof(f16196,plain,
( $false
| ~ spl4_11
| ~ spl4_78
| ~ spl4_84 ),
inference(forward_subsumption_resolution,[],[f16191,f120]) ).
fof(f16197,plain,
( ~ spl4_11
| ~ spl4_78
| ~ spl4_84 ),
inference(avatar_contradiction_clause,[],[f16196]) ).
cnf(s1,plain,
( spl4_1
| ~ spl4_2
| spl4_3 ),
inference(sat_conversion,[],[f221]) ).
cnf(s2,plain,
( spl4_4
| ~ spl4_5
| spl4_6 ),
inference(sat_conversion,[],[f234]) ).
cnf(s3,plain,
spl4_2,
inference(sat_conversion,[],[f237]) ).
cnf(s4,plain,
spl4_5,
inference(sat_conversion,[],[f256]) ).
cnf(s6,plain,
( spl4_8
| spl4_9
| ~ spl4_10 ),
inference(sat_conversion,[],[f300]) ).
cnf(s7,plain,
( spl4_11
| spl4_12
| ~ spl4_13 ),
inference(sat_conversion,[],[f312]) ).
cnf(s8,plain,
( spl4_9
| spl4_14
| ~ spl4_15 ),
inference(sat_conversion,[],[f328]) ).
cnf(s9,plain,
( spl4_12
| spl4_16
| ~ spl4_17 ),
inference(sat_conversion,[],[f337]) ).
cnf(s10,plain,
( spl4_9
| spl4_18
| ~ spl4_19 ),
inference(sat_conversion,[],[f350]) ).
cnf(s11,plain,
( spl4_12
| spl4_20
| ~ spl4_21 ),
inference(sat_conversion,[],[f359]) ).
cnf(s14,plain,
( spl4_26
| spl4_27 ),
inference(sat_conversion,[],[f399]) ).
cnf(s15,plain,
( spl4_28
| spl4_29 ),
inference(sat_conversion,[],[f408]) ).
cnf(s16,plain,
( spl4_30
| spl4_31 ),
inference(sat_conversion,[],[f449]) ).
cnf(s37,plain,
( ~ spl4_29
| ~ spl4_30
| spl4_47 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s39,plain,
( ~ spl4_30
| spl4_56
| ~ spl4_58
| spl4_59 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s40,plain,
( ~ spl4_30
| spl4_56
| ~ spl4_60
| spl4_61 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s53,plain,
( spl4_66
| spl4_67
| spl4_68 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s62,plain,
( spl4_12
| spl4_76
| ~ spl4_77 ),
inference(sat_conversion,[],[f1315]) ).
cnf(s63,plain,
( spl4_12
| spl4_78
| ~ spl4_79 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s64,plain,
( spl4_12
| spl4_80
| ~ spl4_81 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s74,plain,
( ~ spl4_6
| ~ spl4_28
| ~ spl4_31 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s81,plain,
( ~ spl4_6
| ~ spl4_28
| ~ spl4_30 ),
inference(sat_conversion,[],[f1406]) ).
cnf(s84,plain,
( ~ spl4_6
| ~ spl4_29
| ~ spl4_31 ),
inference(sat_conversion,[],[f1412]) ).
cnf(s85,plain,
( ~ spl4_29
| spl4_68
| ~ spl4_82 ),
inference(sat_conversion,[],[f1413]) ).
cnf(s89,plain,
( spl4_9
| spl4_85
| ~ spl4_86 ),
inference(sat_conversion,[],[f1490]) ).
cnf(s90,plain,
( spl4_9
| spl4_87
| ~ spl4_88 ),
inference(sat_conversion,[],[f1499]) ).
cnf(s91,plain,
( spl4_9
| spl4_89
| ~ spl4_90 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s93,plain,
( ~ spl4_30
| spl4_66
| ~ spl4_93 ),
inference(sat_conversion,[],[f1524]) ).
cnf(s96,plain,
( ~ spl4_6
| ~ spl4_30
| ~ spl4_47 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s167,plain,
( ~ spl4_13
| ~ spl4_30
| spl4_56
| spl4_126 ),
inference(sat_conversion,[],[f2900]) ).
cnf(s173,plain,
( ~ spl4_30
| ~ spl4_56 ),
inference(sat_conversion,[],[f2935]) ).
cnf(s205,plain,
( ~ spl4_54
| spl4_101 ),
inference(sat_conversion,[],[f3682]) ).
cnf(s215,plain,
( ~ spl4_61
| ~ spl4_102
| ~ spl4_126 ),
inference(sat_conversion,[],[f3777]) ).
cnf(s218,plain,
( ~ spl4_30
| ~ spl4_101
| spl4_102 ),
inference(sat_conversion,[],[f3789]) ).
cnf(s220,plain,
( ~ spl4_16
| ~ spl4_30
| ~ spl4_126 ),
inference(sat_conversion,[],[f3807]) ).
cnf(s240,plain,
( ~ spl4_3
| ~ spl4_26
| spl4_93 ),
inference(sat_conversion,[],[f4423]) ).
cnf(s302,plain,
( spl4_16
| ~ spl4_30
| ~ spl4_59
| ~ spl4_102 ),
inference(sat_conversion,[],[f5155]) ).
cnf(s307,plain,
( ~ spl4_30
| spl4_54
| ~ spl4_84 ),
inference(sat_conversion,[],[f5163]) ).
cnf(s308,plain,
( ~ spl4_47
| spl4_54
| ~ spl4_93 ),
inference(sat_conversion,[],[f5166]) ).
cnf(s324,plain,
( ~ spl4_30
| ~ spl4_68
| spl4_91 ),
inference(sat_conversion,[],[f5200]) ).
cnf(s325,plain,
( ~ spl4_91
| ~ spl4_93 ),
inference(sat_conversion,[],[f5210]) ).
cnf(s355,plain,
( spl4_14
| ~ spl4_89 ),
inference(sat_conversion,[],[f5614]) ).
cnf(s357,plain,
( ~ spl4_8
| ~ spl4_18 ),
inference(sat_conversion,[],[f5648]) ).
cnf(s370,plain,
( ~ spl4_8
| spl4_85 ),
inference(sat_conversion,[],[f5726]) ).
cnf(s371,plain,
( ~ spl4_85
| ~ spl4_87 ),
inference(sat_conversion,[],[f5727]) ).
cnf(s373,plain,
~ spl4_9,
inference(sat_conversion,[],[f5734]) ).
cnf(s375,plain,
( ~ spl4_1
| ~ spl4_2
| spl4_10
| spl4_15
| spl4_90 ),
inference(sat_conversion,[],[f5736]) ).
cnf(s382,plain,
( ~ spl4_4
| ~ spl4_5
| spl4_17
| ~ spl4_30
| spl4_58
| spl4_60 ),
inference(sat_conversion,[],[f5748]) ).
cnf(s387,plain,
( ~ spl4_1
| ~ spl4_2
| spl4_15
| spl4_19
| spl4_88 ),
inference(sat_conversion,[],[f5827]) ).
cnf(s390,plain,
( ~ spl4_1
| ~ spl4_2
| spl4_10
| spl4_19
| spl4_86 ),
inference(sat_conversion,[],[f5845]) ).
cnf(s395,plain,
( ~ spl4_18
| spl4_85 ),
inference(sat_conversion,[],[f5855]) ).
cnf(s432,plain,
( ~ spl4_14
| ~ spl4_85
| spl4_218
| spl4_219 ),
inference(sat_conversion,[],[f6378]) ).
cnf(s488,plain,
~ spl4_218,
inference(sat_conversion,[],[f7109]) ).
cnf(s489,plain,
~ spl4_219,
inference(sat_conversion,[],[f7113]) ).
cnf(s492,plain,
( ~ spl4_3
| ~ spl4_27
| spl4_93 ),
inference(sat_conversion,[],[f7117]) ).
cnf(s594,plain,
( spl4_6
| ~ spl4_83
| ~ spl4_93 ),
inference(sat_conversion,[],[f7931]) ).
cnf(s607,plain,
( ~ spl4_31
| ~ spl4_68
| spl4_91 ),
inference(sat_conversion,[],[f7968]) ).
cnf(s637,plain,
( ~ spl4_3
| spl4_6
| ~ spl4_67 ),
inference(sat_conversion,[],[f8198]) ).
cnf(s643,plain,
~ spl4_12,
inference(sat_conversion,[],[f8215]) ).
cnf(s644,plain,
( ~ spl4_11
| ~ spl4_20 ),
inference(sat_conversion,[],[f8218]) ).
cnf(s646,plain,
( ~ spl4_4
| ~ spl4_5
| spl4_13
| spl4_17
| spl4_81 ),
inference(sat_conversion,[],[f8221]) ).
cnf(s651,plain,
( ~ spl4_28
| ~ spl4_66
| spl4_84 ),
inference(sat_conversion,[],[f8245]) ).
cnf(s685,plain,
( ~ spl4_4
| ~ spl4_5
| spl4_17
| spl4_21
| spl4_79 ),
inference(sat_conversion,[],[f8805]) ).
cnf(s759,plain,
( spl4_16
| ~ spl4_80
| ~ spl4_84 ),
inference(sat_conversion,[],[f10209]) ).
cnf(s760,plain,
( spl4_82
| spl4_83
| spl4_84 ),
inference(sat_conversion,[],[f10210]) ).
cnf(s761,plain,
( ~ spl4_5
| spl4_82
| spl4_83
| spl4_84 ),
inference(sat_conversion,[],[f10211]) ).
cnf(s773,plain,
( ~ spl4_4
| ~ spl4_5
| spl4_13
| spl4_21
| spl4_77 ),
inference(sat_conversion,[],[f10595]) ).
cnf(s778,plain,
( ~ spl4_16
| ~ spl4_20 ),
inference(sat_conversion,[],[f10679]) ).
cnf(s832,plain,
( ~ spl4_16
| ~ spl4_76
| spl4_396
| spl4_397 ),
inference(sat_conversion,[],[f11749]) ).
cnf(s849,plain,
~ spl4_397,
inference(sat_conversion,[],[f12004]) ).
cnf(s853,plain,
~ spl4_396,
inference(sat_conversion,[],[f12190]) ).
cnf(s854,plain,
( ~ spl4_11
| ~ spl4_16 ),
inference(sat_conversion,[],[f12191]) ).
cnf(s1113,plain,
( ~ spl4_11
| ~ spl4_78
| ~ spl4_84 ),
inference(sat_conversion,[],[f16197]) ).
cnf(s1114,plain,
( ~ spl4_16
| ~ spl4_76 ),
inference(rat,[],[s832,s849,s853]) ).
cnf(s1115,plain,
( ~ spl4_14
| ~ spl4_85 ),
inference(rat,[],[s432,s489,s488]) ).
cnf(s1116,plain,
( spl4_89
| ~ spl4_90 ),
inference(rat,[],[s91,s373]) ).
cnf(s1117,plain,
( spl4_87
| ~ spl4_88 ),
inference(rat,[],[s90,s373]) ).
cnf(s1118,plain,
( spl4_85
| ~ spl4_86 ),
inference(rat,[],[s89,s373]) ).
cnf(s1119,plain,
( spl4_80
| ~ spl4_81 ),
inference(rat,[],[s64,s643]) ).
cnf(s1120,plain,
( spl4_78
| ~ spl4_79 ),
inference(rat,[],[s63,s643]) ).
cnf(s1121,plain,
( spl4_76
| ~ spl4_77 ),
inference(rat,[],[s62,s643]) ).
cnf(s1125,plain,
( spl4_20
| ~ spl4_21 ),
inference(rat,[],[s11,s643]) ).
cnf(s1126,plain,
( spl4_18
| ~ spl4_19 ),
inference(rat,[],[s10,s373]) ).
cnf(s1127,plain,
( spl4_16
| ~ spl4_17 ),
inference(rat,[],[s9,s643]) ).
cnf(s1128,plain,
( spl4_14
| ~ spl4_15 ),
inference(rat,[],[s8,s373]) ).
cnf(s1129,plain,
( spl4_11
| ~ spl4_13 ),
inference(rat,[],[s7,s643]) ).
cnf(s1130,plain,
( spl4_8
| ~ spl4_10 ),
inference(rat,[],[s6,s373]) ).
cnf(s1135,plain,
( spl4_4
| spl4_6 ),
inference(rat,[],[s2,s4]) ).
cnf(s1136,plain,
( spl4_1
| spl4_3 ),
inference(rat,[],[s1,s3]) ).
cnf(s1137,plain,
( ~ spl4_29
| ~ spl4_6 ),
inference(rat,[],[s37,s96,s16,s84]) ).
cnf(s1138,plain,
( ~ spl4_28
| ~ spl4_6 ),
inference(rat,[],[s16,s74,s81]) ).
cnf(s1139,plain,
~ spl4_6,
inference(rat,[],[s1138,s15,s1137]) ).
cnf(s1140,plain,
spl4_4,
inference(rat,[],[s1135,s1139]) ).
cnf(s1141,plain,
( spl4_93
| ~ spl4_3 ),
inference(rat,[],[s14,s240,s492]) ).
cnf(s1142,plain,
( spl4_16
| spl4_13
| ~ spl4_84 ),
inference(rat,[],[s1119,s646,s759,s1127,s4,s1140]) ).
cnf(s1143,plain,
( spl4_13
| ~ spl4_84 ),
inference(rat,[],[s773,s1125,s1121,s778,s1114,s1142,s1140,s4]) ).
cnf(s1144,plain,
( ~ spl4_29
| ~ spl4_30
| ~ spl4_93 ),
inference(rat,[],[s382,s39,s40,s302,s1127,s215,s220,s167,s1143,s218,s205,s761,s308,s85,s37,s594,s173,s324,s325,s4,s1140,s1139]) ).
cnf(s1145,plain,
( ~ spl4_30
| ~ spl4_93 ),
inference(rat,[],[s382,s39,s40,s302,s1127,s215,s220,s218,s167,s205,s1143,s307,s651,s15,s1144,s93,s173,s4,s1140]) ).
cnf(s1146,plain,
( ~ spl4_11
| ~ spl4_84 ),
inference(rat,[],[s685,s1125,s1127,s1120,s644,s854,s1113,s1140,s4]) ).
cnf(s1147,plain,
~ spl4_84,
inference(rat,[],[s1146,s1129,s1143]) ).
cnf(s1148,plain,
~ spl4_3,
inference(rat,[],[s85,s15,s760,s651,s53,s607,s16,s1145,s594,s325,s1141,s637,s1147,s1139]) ).
cnf(s1149,plain,
spl4_1,
inference(rat,[],[s1136,s1148]) ).
cnf(s1154,plain,
( spl4_14
| spl4_10 ),
inference(rat,[],[s375,s1116,s1128,s355,s3,s1149]) ).
cnf(s1155,plain,
spl4_10,
inference(rat,[],[s390,s1126,s1118,s395,s1115,s1154,s3,s1149]) ).
cnf(s1156,plain,
spl4_8,
inference(rat,[],[s1130,s1155]) ).
cnf(s1157,plain,
spl4_85,
inference(rat,[],[s370,s1156]) ).
cnf(s1158,plain,
~ spl4_18,
inference(rat,[],[s357,s1156]) ).
cnf(s1159,plain,
~ spl4_14,
inference(rat,[],[s1115,s1157]) ).
cnf(s1160,plain,
~ spl4_87,
inference(rat,[],[s371,s1157]) ).
cnf(s1162,plain,
~ spl4_19,
inference(rat,[],[s1126,s1158]) ).
cnf(s1163,plain,
~ spl4_15,
inference(rat,[],[s1128,s1159]) ).
cnf(s1164,plain,
~ spl4_88,
inference(rat,[],[s1117,s1160]) ).
cnf(s1166,plain,
$false,
inference(rat,[],[s387,s1163,s1149,s3,s1164,s1162]) ).
fof(f16198,plain,
$false,
inference(avatar_sat_refutation,[],[s1166]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.38 % Computer : n015.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 17:25:16 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.25/0.88 % (1882265)Will run a generic schedule for satisfiability detection.
% 2.25/0.88 % (1882276)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2287907932:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.25/0.88 % (1882271)% WARNING: option uhcvi not known.
% 2.25/0.88 % (1882274)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1881216777:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.25/0.88 % (1882270)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1846444996_2999 on theBenchmark for (2999ds/0Mi)
% 2.25/0.88 % (1882271)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=817096677:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.25/0.88 % (1882272)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4207338715:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.25/0.88 % (1882273)dis+10_1_sil=32000:sp=arity:random_seed=1204059323:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.25/0.88 % (1882275)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1066042752:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.25/0.88 % TRYING [1]
% 2.25/0.88 % TRYING [2]
% 2.25/0.88 % TRYING [3]
% 2.25/0.88 % TRYING [4]
% 2.25/0.88 % (1882276)Instruction limit reached!
% 2.25/0.88 % (1882276)------------------------------
% 2.25/0.88 % (1882276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.88 % (1882276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.88 % (1882276)CaDiCaL version: 2.1.3
% 2.25/0.88 % (1882276)Termination reason: Instruction limit
% 2.25/0.88 % (1882276)Termination phase: Saturation
% 2.25/0.88 % (1882276)Time elapsed: 0.039 s
% 2.25/0.88 % (1882276)Peak memory usage: 12 MB
% 2.25/0.88 % (1882276)Instructions burned: 161 (million)
% 2.25/0.88 % (1882284)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1262267284:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.25/0.88 % TRYING [1]
% 2.25/0.88 % TRYING [2]
% 2.25/0.88 % TRYING [3]
% 2.25/0.88 % (1882274)Instruction limit reached!
% 2.25/0.88 % (1882274)------------------------------
% 2.25/0.88 % (1882274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.88 % (1882274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.88 % (1882274)CaDiCaL version: 2.1.3
% 2.25/0.88 % (1882274)Termination reason: Instruction limit
% 2.25/0.88 % (1882274)Termination phase: Saturation
% 2.25/0.88 % (1882274)Time elapsed: 0.060 s
% 2.25/0.88 % (1882274)Peak memory usage: 12 MB
% 2.25/0.88 % (1882274)Instructions burned: 118 (million)
% 2.25/0.88 % (1882273)Instruction limit reached!
% 2.25/0.88 % (1882273)------------------------------
% 2.25/0.88 % (1882273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.88 % (1882273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.88 % (1882273)CaDiCaL version: 2.1.3
% 2.25/0.88 % (1882273)Termination reason: Instruction limit
% 2.25/0.88 % (1882273)Termination phase: Saturation
% 2.25/0.88 % (1882273)Time elapsed: 0.064 s
% 2.25/0.88 % (1882273)Peak memory usage: 12 MB
% 2.25/0.88 % (1882273)Instructions burned: 104 (million)
% 2.25/0.88 % (1882275)Instruction limit reached!
% 2.25/0.88 % (1882275)------------------------------
% 2.25/0.88 % (1882275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.88 % (1882275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.88 % (1882275)CaDiCaL version: 2.1.3
% 2.25/0.88 % (1882275)Termination reason: Instruction limit
% 2.25/0.88 % (1882275)Termination phase: Saturation
% 2.25/0.88 % (1882275)Time elapsed: 0.077 s
% 2.25/0.88 % (1882275)Peak memory usage: 12 MB
% 2.25/0.88 % (1882275)Instructions burned: 133 (million)
% 2.25/0.88 % (1882286)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2045438116:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.25/0.88 % (1882287)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3709243843:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.25/0.88 % (1882288)ott-21_1_sil=16000:fs=off:random_seed=42013168:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.25/0.88 % TRYING [4]
% 2.25/0.88 % TRYING [5]
% 2.25/0.88 % (1882286)Instruction limit reached!
% 2.25/0.88 % (1882286)------------------------------
% 2.25/0.88 % (1882286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.88 % (1882286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.88 % (1882286)CaDiCaL version: 2.1.3
% 2.25/0.88 % (1882286)Termination reason: Instruction limit
% 2.25/0.88 % (1882286)Termination phase: Saturation
% 2.25/0.88 % (1882286)Time elapsed: 0.077 s
% 2.25/0.88 % (1882286)Peak memory usage: 12 MB
% 2.25/0.88 % (1882286)Instructions burned: 132 (million)
% 2.25/0.88 % (1882292)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=655432348:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.25/0.88 % (1882288)Instruction limit reached!
% 2.25/0.88 % (1882288)------------------------------
% 2.25/0.88 % (1882288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.88 % (1882288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.88 % (1882288)CaDiCaL version: 2.1.3
% 2.25/0.88 % (1882288)Termination reason: Instruction limit
% 2.25/0.88 % (1882288)Termination phase: Saturation
% 2.25/0.88 % (1882288)Time elapsed: 0.092 s
% 2.25/0.88 % (1882288)Peak memory usage: 12 MB
% 2.25/0.88 % (1882288)Instructions burned: 180 (million)
% 2.25/0.88 % (1882294)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1466506039:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.25/0.88 % TRYING [1]
% 2.25/0.88 % TRYING [2]
% 2.25/0.88 % TRYING [3]
% 2.25/0.88 % TRYING [4]
% 2.25/0.88 % (1882284)Instruction limit reached!
% 2.25/0.88 % (1882284)------------------------------
% 2.25/0.88 % (1882284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.88 % (1882284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.88 % (1882284)CaDiCaL version: 2.1.3
% 2.25/0.88 % (1882284)Termination reason: Instruction limit
% 2.25/0.88 % (1882284)Termination phase: Finite model building SAT solving
% 2.25/0.88 % (1882284)Time elapsed: 0.213 s
% 2.25/0.88 % (1882284)Peak memory usage: 13 MB
% 2.25/0.88 % (1882284)Instructions burned: 716 (million)
% 2.25/0.88 % (1882296)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2395117414:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 2.25/0.88 % TRYING [5]
% 2.25/0.88 % (1882287)Instruction limit reached!
% 2.25/0.88 % (1882287)------------------------------
% 2.25/0.88 % (1882287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.88 % (1882287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.88 % (1882287)CaDiCaL version: 2.1.3
% 2.25/0.88 % (1882287)Termination reason: Instruction limit
% 2.25/0.88 % (1882287)Termination phase: Saturation
% 2.25/0.88 % (1882287)Time elapsed: 0.332 s
% 2.25/0.88 % (1882287)Peak memory usage: 21 MB
% 2.25/0.88 % (1882287)Instructions burned: 685 (million)
% 2.25/0.88 % (1882296) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1882265-1882296"...
% 2.25/0.88 % (1882296)...printing done.
% 2.25/0.88 % (1882296)Refutation found. Thanks to Tanya!
% 2.25/0.88 % SZS status Theorem for theBenchmark
% 2.25/0.88 % SZS output start Proof for theBenchmark
% See solution above
% 2.25/0.89 % (1882296)------------------------------
% 2.25/0.89 % (1882296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.89 % (1882296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.89 % (1882296)CaDiCaL version: 2.1.3
% 2.25/0.89 % (1882296)Termination reason: Refutation
% 2.25/0.89 % (1882296)Time elapsed: 0.155 s
% 2.25/0.89 % (1882296)Peak memory usage: 17 MB
% 2.25/0.89 % (1882296)Instructions burned: 504 (million)
% 2.25/0.89 % (1882265)Success in time 0.456 s
% 2.25/0.89 % Vampire exiting
%------------------------------------------------------------------------------