%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:02:08 PM UTC 2026
% Result : Theorem 5.69s 1.80s
% Output : Refutation 7.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 73
% Syntax : Number of formulae : 613 ( 26 unt; 54 def)
% Number of atoms : 2130 ( 136 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2690 (1173 ~;1341 |; 90 &)
% ( 58 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 67 ( 65 usr; 55 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-2 aty)
% Number of variables : 369 ( 0 sgn 357 !; 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(f13,axiom,
! [X0,X1] :
( ( environment(X0)
& greater_or_equal(X1,equilibrium(X0)) )
=> ~ greater(equilibrium(X0),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_equilibrium) ).
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(f42,plain,
! [X0,X1] :
( ~ greater(equilibrium(X0),X1)
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0)) ),
inference(ennf_transformation,[],[f13]) ).
fof(f43,plain,
! [X0,X1] :
( ~ greater(equilibrium(X0),X1)
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0)) ),
inference(flattening,[],[f42]) ).
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(f68,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)
| first_movers != X1 ),
inference(cnf_transformation,[],[f27]) ).
fof(f70,plain,
! [X0,X1] :
( subpopulation(efficient_producers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f71,plain,
! [X0,X1] :
( subpopulation(first_movers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f72,plain,
! [X2,X0,X1] :
( constant(X2)
| decreases(X2)
| increases(X2)
| sum(X1,X2) != X0
| ~ constant(X0) ),
inference(cnf_transformation,[],[f31]) ).
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(f75,plain,
! [X2,X0,X1] :
( constant(X2)
| increases(X1)
| decreases(X1)
| 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(f77,plain,
! [X2,X0,X1] :
( constant(X1)
| decreases(X2)
| decreases(X1)
| 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(f92,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ environment(X0)
| ~ greater(equilibrium(X0),X1) ),
inference(cnf_transformation,[],[f43]) ).
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] :
( in_environment(X0,sK0(X0))
| ~ environment(X0)
| ~ stable(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] :
( in_environment(X0,sK1(X0))
| ~ environment(X0)
| ~ stable(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(f111,plain,
! [X2,X0] :
( ~ subpopulation(first_movers,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,[],[f68]) ).
fof(f113,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| increases(X1)
| increases(X2)
| constant(X1) ),
inference(equality_resolution,[],[f78]) ).
fof(f114,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| decreases(X2)
| decreases(X1)
| constant(X1) ),
inference(equality_resolution,[],[f77]) ).
fof(f115,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| decreases(X2)
| increases(X2)
| constant(X1) ),
inference(equality_resolution,[],[f76]) ).
fof(f116,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| increases(X1)
| decreases(X1)
| constant(X2) ),
inference(equality_resolution,[],[f75]) ).
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(f119,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| decreases(X2)
| increases(X2)
| constant(X2) ),
inference(equality_resolution,[],[f72]) ).
fof(f120,plain,
! [X1] : ~ greater(X1,X1),
inference(equality_resolution,[],[f85]) ).
fof(f122,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(f123,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,[],[f122,f106]) ).
fof(f124,plain,
! [X0] :
( greater(growth_rate(efficient_producers,sK3(X0)),growth_rate(first_movers,sK3(X0)))
| ~ greater_or_equal(sK3(X0),sK1(sK2))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f123,f105]) ).
fof(f125,plain,
! [X0] :
( ~ environment(sK2)
| greater(number_of_organizations(sK2,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f66,f108]) ).
fof(f126,plain,
! [X0] :
( greater(number_of_organizations(sK2,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f125,f106]) ).
fof(f127,plain,
! [X0] :
( ~ environment(sK2)
| in_environment(sK2,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f65,f108]) ).
fof(f128,plain,
! [X0] :
( in_environment(sK2,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f127,f106]) ).
fof(f129,plain,
! [X0] :
( greater(sK3(X0),X0)
| sK3(X0) = X0
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f89,f107]) ).
fof(f130,plain,
! [X0] :
( greater(sK0(X0),equilibrium(X0))
| equilibrium(X0) = sK0(X0)
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[],[f89,f98]) ).
fof(f132,plain,
! [X0] :
( ~ environment(X0)
| ~ greater(equilibrium(X0),sK0(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[],[f92,f98]) ).
fof(f133,plain,
! [X0] :
( ~ greater(equilibrium(X0),sK0(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(duplicate_literal_removal,[],[f132]) ).
fof(f136,plain,
! [X0] :
( ~ environment(sK2)
| greater(cardinality_at_time(efficient_producers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f83,f108]) ).
fof(f137,plain,
! [X0] :
( greater(cardinality_at_time(efficient_producers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f136,f106]) ).
fof(f138,plain,
! [X0] :
( ~ environment(sK2)
| greater(cardinality_at_time(first_movers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f84,f108]) ).
fof(f139,plain,
! [X0] :
( greater(cardinality_at_time(first_movers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f138,f106]) ).
fof(f144,plain,
! [X0,X1] :
( ~ greater(X0,growth_rate(efficient_producers,sK3(X1)))
| greater(X0,growth_rate(first_movers,sK3(X1)))
| ~ greater_or_equal(sK3(X1),sK1(sK2))
| ~ in_environment(sK2,X1) ),
inference(resolution,[],[f87,f124]) ).
fof(f146,plain,
! [X0,X1] :
( ~ greater(X0,sK3(X1))
| greater(X0,X1)
| sK3(X1) = X1
| ~ in_environment(sK2,X1) ),
inference(resolution,[],[f87,f129]) ).
fof(f151,plain,
! [X0,X1] :
( ~ constant(cardinality_at_time(efficient_producers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| ~ subpopulation(efficient_producers,X1,sK3(X0))
| zero = growth_rate(efficient_producers,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f82,f137]) ).
fof(f152,plain,
! [X0,X1] :
( ~ constant(cardinality_at_time(first_movers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| ~ subpopulation(first_movers,X1,sK3(X0))
| zero = growth_rate(first_movers,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f82,f139]) ).
fof(f153,plain,
! [X0,X1] :
( ~ constant(cardinality_at_time(first_movers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| zero = growth_rate(first_movers,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f152,f71]) ).
fof(f154,plain,
! [X0,X1] :
( ~ constant(cardinality_at_time(efficient_producers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| zero = growth_rate(efficient_producers,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f151,f70]) ).
fof(f159,plain,
! [X0] :
( ~ greater(growth_rate(first_movers,sK3(X0)),growth_rate(efficient_producers,sK3(X0)))
| ~ greater_or_equal(sK3(X0),sK1(sK2))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f86,f124]) ).
fof(f161,plain,
! [X0,X1] :
( ~ decreases(cardinality_at_time(efficient_producers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| ~ subpopulation(efficient_producers,X1,sK3(X0))
| greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f80,f137]) ).
fof(f162,plain,
! [X0,X1] :
( ~ decreases(cardinality_at_time(first_movers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| ~ subpopulation(first_movers,X1,sK3(X0))
| greater(zero,growth_rate(first_movers,sK3(X0)))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f80,f139]) ).
fof(f163,plain,
! [X0,X1] :
( ~ decreases(cardinality_at_time(first_movers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| greater(zero,growth_rate(first_movers,sK3(X0)))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f162,f71]) ).
fof(f164,plain,
! [X0,X1] :
( ~ decreases(cardinality_at_time(efficient_producers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f161,f70]) ).
fof(f165,plain,
! [X0,X1] :
( ~ increases(cardinality_at_time(efficient_producers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| ~ subpopulation(efficient_producers,X1,sK3(X0))
| greater(growth_rate(efficient_producers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f81,f137]) ).
fof(f166,plain,
! [X0,X1] :
( ~ increases(cardinality_at_time(first_movers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| ~ subpopulation(first_movers,X1,sK3(X0))
| greater(growth_rate(first_movers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f81,f139]) ).
fof(f167,plain,
! [X0,X1] :
( ~ increases(cardinality_at_time(first_movers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| greater(growth_rate(first_movers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f166,f71]) ).
fof(f168,plain,
! [X0,X1] :
( ~ increases(cardinality_at_time(efficient_producers,sK3(X0)))
| ~ environment(X1)
| ~ in_environment(X1,sK3(X0))
| greater(growth_rate(efficient_producers,sK3(X0)),zero)
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f165,f70]) ).
fof(f169,plain,
! [X0] :
( greater(equilibrium(sK2),sK3(X0))
| ~ environment(sK2)
| ~ in_environment(sK2,sK3(X0))
| constant(resources(sK2,sK3(X0)))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f96,f126]) ).
fof(f170,plain,
! [X0] :
( greater(equilibrium(sK2),sK3(X0))
| ~ in_environment(sK2,sK3(X0))
| constant(resources(sK2,sK3(X0)))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f169,f106]) ).
fof(f171,plain,
! [X0] :
( constant(resources(sK2,sK3(X0)))
| greater(equilibrium(sK2),sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f170,f128]) ).
fof(f172,plain,
! [X0,X1] :
( ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ environment(X0)
| number_of_organizations(X0,X1) = sum(cardinality_at_time(first_movers,X1),cardinality_at_time(efficient_producers,X1)) ),
inference(resolution,[],[f71,f111]) ).
fof(f173,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| number_of_organizations(X0,X1) = sum(cardinality_at_time(first_movers,X1),cardinality_at_time(efficient_producers,X1)) ),
inference(duplicate_literal_removal,[],[f172]) ).
fof(f186,plain,
! [X0] :
( ~ environment(X0)
| number_of_organizations(X0,sK0(X0)) = sum(cardinality_at_time(first_movers,sK0(X0)),cardinality_at_time(efficient_producers,sK0(X0)))
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[],[f173,f99]) ).
fof(f187,plain,
! [X0] :
( ~ environment(sK2)
| number_of_organizations(sK2,sK3(X0)) = sum(cardinality_at_time(first_movers,sK3(X0)),cardinality_at_time(efficient_producers,sK3(X0)))
| ~ in_environment(sK2,X0) ),
inference(resolution,[],[f173,f128]) ).
fof(f188,plain,
! [X0] :
( ~ stable(X0)
| number_of_organizations(X0,sK0(X0)) = sum(cardinality_at_time(first_movers,sK0(X0)),cardinality_at_time(efficient_producers,sK0(X0)))
| ~ environment(X0) ),
inference(duplicate_literal_removal,[],[f186]) ).
fof(f190,plain,
! [X0] :
( ~ in_environment(sK2,X0)
| number_of_organizations(sK2,sK3(X0)) = sum(cardinality_at_time(first_movers,sK3(X0)),cardinality_at_time(efficient_producers,sK3(X0))) ),
inference(forward_subsumption_resolution,[],[f187,f106]) ).
fof(f193,plain,
( number_of_organizations(sK2,sK0(sK2)) = sum(cardinality_at_time(first_movers,sK0(sK2)),cardinality_at_time(efficient_producers,sK0(sK2)))
| ~ environment(sK2) ),
inference(resolution,[],[f188,f105]) ).
fof(f194,plain,
number_of_organizations(sK2,sK0(sK2)) = sum(cardinality_at_time(first_movers,sK0(sK2)),cardinality_at_time(efficient_producers,sK0(sK2))),
inference(forward_subsumption_resolution,[],[f193,f106]) ).
fof(f231,plain,
( ~ constant(number_of_organizations(sK2,sK0(sK2)))
| increases(cardinality_at_time(first_movers,sK0(sK2)))
| decreases(cardinality_at_time(first_movers,sK0(sK2)))
| constant(cardinality_at_time(efficient_producers,sK0(sK2))) ),
inference(superposition,[],[f116,f194]) ).
fof(f234,plain,
( ~ constant(number_of_organizations(sK2,sK0(sK2)))
| decreases(cardinality_at_time(efficient_producers,sK0(sK2)))
| decreases(cardinality_at_time(first_movers,sK0(sK2)))
| constant(cardinality_at_time(efficient_producers,sK0(sK2))) ),
inference(superposition,[],[f118,f194]) ).
fof(f236,definition,
( spl4_8
<=> constant(cardinality_at_time(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f237,plain,
( ~ constant(cardinality_at_time(efficient_producers,sK0(sK2)))
| spl4_8 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f240,definition,
( spl4_9
<=> decreases(cardinality_at_time(first_movers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f242,plain,
( decreases(cardinality_at_time(first_movers,sK0(sK2)))
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f244,definition,
( spl4_10
<=> decreases(cardinality_at_time(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f248,definition,
( spl4_11
<=> constant(number_of_organizations(sK2,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f250,plain,
( ~ constant(number_of_organizations(sK2,sK0(sK2)))
| spl4_11 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,plain,
( spl4_8
| spl4_9
| spl4_10
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f234,f248,f244,f240,f236]) ).
fof(f263,definition,
( spl4_14
<=> increases(cardinality_at_time(first_movers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f265,plain,
( increases(cardinality_at_time(first_movers,sK0(sK2)))
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f266,plain,
( spl4_8
| spl4_9
| spl4_14
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f231,f248,f263,f240,f236]) ).
fof(f275,plain,
! [X0] :
( greater(equilibrium(sK2),sK3(X0))
| ~ in_environment(sK2,X0)
| constant(number_of_organizations(sK2,sK3(X0)))
| ~ environment(sK2)
| ~ in_environment(sK2,sK3(X0)) ),
inference(resolution,[],[f171,f100]) ).
fof(f276,plain,
! [X0] :
( greater(equilibrium(sK2),sK3(X0))
| ~ in_environment(sK2,X0)
| constant(number_of_organizations(sK2,sK3(X0)))
| ~ in_environment(sK2,sK3(X0)) ),
inference(forward_subsumption_resolution,[],[f275,f106]) ).
fof(f277,plain,
! [X0] :
( constant(number_of_organizations(sK2,sK3(X0)))
| ~ in_environment(sK2,X0)
| greater(equilibrium(sK2),sK3(X0)) ),
inference(forward_subsumption_resolution,[],[f276,f128]) ).
fof(f278,plain,
! [X0,X1] :
( greater(sK1(X1),X0)
| greater(X0,sK1(X1))
| ~ in_environment(X1,X0)
| sK1(X1) = X0
| ~ environment(X1)
| ~ stable(X1) ),
inference(resolution,[],[f88,f104]) ).
fof(f280,plain,
! [X0,X1] :
( greater(sK3(X1),X0)
| greater(X0,sK3(X1))
| ~ in_environment(sK2,X0)
| sK3(X1) = X0
| ~ in_environment(sK2,X1) ),
inference(resolution,[],[f88,f128]) ).
fof(f284,plain,
! [X0,X1] :
( greater_or_equal(X0,sK1(X1))
| ~ in_environment(X1,X0)
| sK1(X1) = X0
| ~ environment(X1)
| ~ stable(X1)
| greater(sK1(X1),X0) ),
inference(resolution,[],[f278,f91]) ).
fof(f290,plain,
! [X0,X1] :
( ~ greater(X1,sK0(X0))
| ~ environment(X0)
| ~ stable(X0)
| equilibrium(X0) = sK0(X0)
| greater(X1,equilibrium(X0)) ),
inference(resolution,[],[f130,f87]) ).
fof(f320,plain,
! [X0,X1] :
( greater(X0,X1)
| sK3(X1) = X1
| ~ in_environment(sK2,X1)
| greater(sK3(X1),X0)
| ~ in_environment(sK2,X0)
| sK3(X1) = X0
| ~ in_environment(sK2,X1) ),
inference(resolution,[],[f146,f280]) ).
fof(f325,plain,
! [X0,X1] :
( greater(sK3(X1),X0)
| sK3(X1) = X1
| ~ in_environment(sK2,X1)
| greater(X0,X1)
| ~ in_environment(sK2,X0)
| sK3(X1) = X0 ),
inference(duplicate_literal_removal,[],[f320]) ).
fof(f337,plain,
! [X0,X1] :
( greater_or_equal(sK3(X0),X1)
| ~ in_environment(sK2,X0)
| greater(X1,X0)
| ~ in_environment(sK2,X1)
| sK3(X0) = X1
| sK3(X0) = X0 ),
inference(resolution,[],[f325,f91]) ).
fof(f389,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))))
| ~ environment(sK2)
| ~ stable(sK2) ),
inference(resolution,[],[f190,f104]) ).
fof(f390,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))))
| ~ environment(sK2)
| ~ stable(sK2) ),
inference(resolution,[],[f190,f99]) ).
fof(f391,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))))
| ~ stable(sK2) ),
inference(forward_subsumption_resolution,[],[f390,f106]) ).
fof(f392,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))))
| ~ stable(sK2) ),
inference(forward_subsumption_resolution,[],[f389,f106]) ).
fof(f393,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,[],[f391,f105]) ).
fof(f394,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,[],[f392,f105]) ).
fof(f396,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(first_movers,sK3(sK1(sK2)))) ),
inference(superposition,[],[f113,f394]) ).
fof(f397,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(first_movers,sK3(sK1(sK2)))) ),
inference(superposition,[],[f114,f394]) ).
fof(f398,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,f394]) ).
fof(f400,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,f394]) ).
fof(f401,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,f394]) ).
fof(f402,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(efficient_producers,sK3(sK1(sK2)))) ),
inference(superposition,[],[f119,f394]) ).
fof(f404,definition,
( spl4_15
<=> constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f406,plain,
( constant(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_15 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f408,definition,
( spl4_16
<=> increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_16])],[avatar_definition]) ).
fof(f410,plain,
( increases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_16 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f412,definition,
( spl4_17
<=> decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f414,plain,
( decreases(cardinality_at_time(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_17 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f416,definition,
( spl4_18
<=> constant(number_of_organizations(sK2,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_18])],[avatar_definition]) ).
fof(f418,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK1(sK2))))
| spl4_18 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f419,plain,
( spl4_15
| spl4_16
| spl4_17
| ~ spl4_18 ),
inference(avatar_split_clause,[],[f402,f416,f412,f408,f404]) ).
fof(f421,definition,
( spl4_19
<=> decreases(cardinality_at_time(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_19])],[avatar_definition]) ).
fof(f423,plain,
( decreases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ spl4_19 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f424,plain,
( spl4_15
| spl4_19
| spl4_17
| ~ spl4_18 ),
inference(avatar_split_clause,[],[f401,f416,f412,f421,f404]) ).
fof(f426,definition,
( spl4_20
<=> increases(cardinality_at_time(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition]) ).
fof(f428,plain,
( increases(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ spl4_20 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f429,plain,
( spl4_15
| spl4_16
| spl4_20
| ~ spl4_18 ),
inference(avatar_split_clause,[],[f400,f416,f426,f408,f404]) ).
fof(f432,definition,
( spl4_21
<=> constant(cardinality_at_time(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f434,plain,
( constant(cardinality_at_time(first_movers,sK3(sK1(sK2))))
| ~ spl4_21 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f435,plain,
( spl4_21
| spl4_16
| spl4_17
| ~ spl4_18 ),
inference(avatar_split_clause,[],[f398,f416,f412,f408,f432]) ).
fof(f436,plain,
( spl4_21
| spl4_19
| spl4_17
| ~ spl4_18 ),
inference(avatar_split_clause,[],[f397,f416,f412,f421,f432]) ).
fof(f437,plain,
( spl4_21
| spl4_16
| spl4_20
| ~ spl4_18 ),
inference(avatar_split_clause,[],[f396,f416,f426,f408,f432]) ).
fof(f439,plain,
( ~ in_environment(sK2,sK1(sK2))
| greater(equilibrium(sK2),sK3(sK1(sK2)))
| spl4_18 ),
inference(resolution,[],[f418,f277]) ).
fof(f441,definition,
( spl4_22
<=> greater(equilibrium(sK2),sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_22])],[avatar_definition]) ).
fof(f443,plain,
( greater(equilibrium(sK2),sK3(sK1(sK2)))
| ~ spl4_22 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f445,definition,
( spl4_23
<=> in_environment(sK2,sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition]) ).
fof(f446,plain,
( in_environment(sK2,sK1(sK2))
| ~ spl4_23 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f447,plain,
( ~ in_environment(sK2,sK1(sK2))
| spl4_23 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f448,plain,
( spl4_22
| ~ spl4_23
| spl4_18 ),
inference(avatar_split_clause,[],[f439,f416,f445,f441]) ).
fof(f449,plain,
( ~ environment(sK2)
| ~ stable(sK2)
| spl4_23 ),
inference(resolution,[],[f447,f104]) ).
fof(f450,plain,
( ~ stable(sK2)
| spl4_23 ),
inference(forward_subsumption_resolution,[],[f449,f106]) ).
fof(f451,plain,
( $false
| spl4_23 ),
inference(forward_subsumption_resolution,[],[f450,f105]) ).
fof(f452,plain,
spl4_23,
inference(avatar_contradiction_clause,[],[f451]) ).
fof(f456,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ in_environment(sK2,sK1(sK2)) )
| ~ spl4_19 ),
inference(resolution,[],[f423,f163]) ).
fof(f457,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(zero,growth_rate(first_movers,sK3(sK1(sK2)))) )
| ~ spl4_19
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f456,f446]) ).
fof(f459,definition,
( spl4_24
<=> greater(zero,growth_rate(first_movers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_24])],[avatar_definition]) ).
fof(f460,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| spl4_24 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ spl4_24 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f463,definition,
( spl4_25
<=> ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
fof(f464,plain,
( ! [X0] :
( ~ in_environment(X0,sK3(sK1(sK2)))
| ~ environment(X0) )
| ~ spl4_25 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f465,plain,
( spl4_24
| spl4_25
| ~ spl4_19
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f457,f445,f421,f463,f459]) ).
fof(f466,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ~ in_environment(sK2,sK1(sK2)) )
| ~ spl4_17 ),
inference(resolution,[],[f414,f164]) ).
fof(f467,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2)))) )
| ~ spl4_17
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f466,f446]) ).
fof(f469,definition,
( spl4_26
<=> greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f471,plain,
( greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_26 ),
inference(avatar_component_clause,[],[f469]) ).
fof(f472,plain,
( spl4_26
| spl4_25
| ~ spl4_17
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f467,f445,f412,f463,f469]) ).
fof(f473,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| zero = growth_rate(first_movers,sK3(sK1(sK2)))
| ~ in_environment(sK2,sK1(sK2)) )
| ~ spl4_21 ),
inference(resolution,[],[f434,f153]) ).
fof(f474,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| zero = growth_rate(first_movers,sK3(sK1(sK2))) )
| ~ spl4_21
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f473,f446]) ).
fof(f476,definition,
( spl4_27
<=> zero = growth_rate(first_movers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_27])],[avatar_definition]) ).
fof(f478,plain,
( zero = growth_rate(first_movers,sK3(sK1(sK2)))
| ~ spl4_27 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f479,plain,
( spl4_27
| spl4_25
| ~ spl4_21
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f474,f445,f432,f463,f476]) ).
fof(f481,plain,
( greater(equilibrium(sK2),sK1(sK2))
| sK1(sK2) = sK3(sK1(sK2))
| ~ in_environment(sK2,sK1(sK2))
| ~ spl4_22 ),
inference(resolution,[],[f443,f146]) ).
fof(f486,plain,
( greater(equilibrium(sK2),sK1(sK2))
| sK1(sK2) = sK3(sK1(sK2))
| ~ spl4_22
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f481,f446]) ).
fof(f489,definition,
( spl4_28
<=> sK1(sK2) = sK3(sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f491,plain,
( sK1(sK2) = sK3(sK1(sK2))
| ~ spl4_28 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f493,definition,
( spl4_29
<=> greater(equilibrium(sK2),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_29])],[avatar_definition]) ).
fof(f495,plain,
( greater(equilibrium(sK2),sK1(sK2))
| ~ spl4_29 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f496,plain,
( spl4_28
| spl4_29
| ~ spl4_22
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f486,f445,f441,f493,f489]) ).
fof(f499,plain,
( ~ greater(growth_rate(first_movers,sK3(sK1(sK2))),zero)
| ~ spl4_24 ),
inference(resolution,[],[f461,f86]) ).
fof(f503,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK1(sK2)))
| ~ in_environment(sK2,sK1(sK2)) )
| ~ spl4_15 ),
inference(resolution,[],[f406,f154]) ).
fof(f504,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK1(sK2))) )
| ~ spl4_15
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f503,f446]) ).
fof(f506,definition,
( spl4_30
<=> zero = growth_rate(efficient_producers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f508,plain,
( zero = growth_rate(efficient_producers,sK3(sK1(sK2)))
| ~ spl4_30 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f509,plain,
( spl4_30
| spl4_25
| ~ spl4_15
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f504,f445,f404,f463,f506]) ).
fof(f512,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(first_movers,sK3(sK0(sK2)))) ),
inference(superposition,[],[f114,f393]) ).
fof(f513,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,f393]) ).
fof(f515,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,f393]) ).
fof(f516,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,f393]) ).
fof(f517,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(efficient_producers,sK3(sK0(sK2)))) ),
inference(superposition,[],[f119,f393]) ).
fof(f519,definition,
( spl4_31
<=> constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_31])],[avatar_definition]) ).
fof(f521,plain,
( constant(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_31 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f523,definition,
( spl4_32
<=> increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_32])],[avatar_definition]) ).
fof(f525,plain,
( increases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_32 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl4_33
<=> decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition]) ).
fof(f529,plain,
( decreases(cardinality_at_time(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_33 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f531,definition,
( spl4_34
<=> constant(number_of_organizations(sK2,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_34])],[avatar_definition]) ).
fof(f533,plain,
( ~ constant(number_of_organizations(sK2,sK3(sK0(sK2))))
| spl4_34 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f534,plain,
( spl4_31
| spl4_32
| spl4_33
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f517,f531,f527,f523,f519]) ).
fof(f536,definition,
( spl4_35
<=> decreases(cardinality_at_time(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_35])],[avatar_definition]) ).
fof(f537,plain,
( ~ decreases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| spl4_35 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f538,plain,
( decreases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_35 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f539,plain,
( spl4_31
| spl4_35
| spl4_33
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f516,f531,f527,f536,f519]) ).
fof(f541,definition,
( spl4_36
<=> increases(cardinality_at_time(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_36])],[avatar_definition]) ).
fof(f543,plain,
( increases(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_36 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f544,plain,
( spl4_31
| spl4_32
| spl4_36
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f515,f531,f541,f523,f519]) ).
fof(f547,definition,
( spl4_37
<=> constant(cardinality_at_time(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_37])],[avatar_definition]) ).
fof(f549,plain,
( constant(cardinality_at_time(first_movers,sK3(sK0(sK2))))
| ~ spl4_37 ),
inference(avatar_component_clause,[],[f547]) ).
fof(f550,plain,
( spl4_37
| spl4_32
| spl4_33
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f513,f531,f527,f523,f547]) ).
fof(f551,plain,
( spl4_37
| spl4_35
| spl4_33
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f512,f531,f527,f536,f547]) ).
fof(f554,plain,
( ~ in_environment(sK2,sK0(sK2))
| greater(equilibrium(sK2),sK3(sK0(sK2)))
| spl4_34 ),
inference(resolution,[],[f533,f277]) ).
fof(f556,definition,
( spl4_38
<=> greater(equilibrium(sK2),sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_38])],[avatar_definition]) ).
fof(f557,plain,
( ~ greater(equilibrium(sK2),sK3(sK0(sK2)))
| spl4_38 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f558,plain,
( greater(equilibrium(sK2),sK3(sK0(sK2)))
| ~ spl4_38 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f560,definition,
( spl4_39
<=> in_environment(sK2,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_39])],[avatar_definition]) ).
fof(f561,plain,
( in_environment(sK2,sK0(sK2))
| ~ spl4_39 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f562,plain,
( ~ in_environment(sK2,sK0(sK2))
| spl4_39 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f563,plain,
( spl4_38
| ~ spl4_39
| spl4_34 ),
inference(avatar_split_clause,[],[f554,f531,f560,f556]) ).
fof(f564,plain,
( ~ environment(sK2)
| ~ stable(sK2)
| spl4_39 ),
inference(resolution,[],[f562,f99]) ).
fof(f565,plain,
( ~ stable(sK2)
| spl4_39 ),
inference(forward_subsumption_resolution,[],[f564,f106]) ).
fof(f566,plain,
( $false
| spl4_39 ),
inference(forward_subsumption_resolution,[],[f565,f105]) ).
fof(f567,plain,
spl4_39,
inference(avatar_contradiction_clause,[],[f566]) ).
fof(f571,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_35 ),
inference(resolution,[],[f538,f163]) ).
fof(f572,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(zero,growth_rate(first_movers,sK3(sK0(sK2)))) )
| ~ spl4_35
| ~ spl4_39 ),
inference(forward_subsumption_resolution,[],[f571,f561]) ).
fof(f574,definition,
( spl4_40
<=> greater(zero,growth_rate(first_movers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_40])],[avatar_definition]) ).
fof(f575,plain,
( ~ greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| spl4_40 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f576,plain,
( greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ spl4_40 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f578,definition,
( spl4_41
<=> ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_41])],[avatar_definition]) ).
fof(f579,plain,
( ! [X0] :
( ~ in_environment(X0,sK3(sK0(sK2)))
| ~ environment(X0) )
| ~ spl4_41 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f580,plain,
( spl4_40
| spl4_41
| ~ spl4_35
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f572,f560,f536,f578,f574]) ).
fof(f581,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2))))
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_33 ),
inference(resolution,[],[f529,f164]) ).
fof(f582,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2)))) )
| ~ spl4_33
| ~ spl4_39 ),
inference(forward_subsumption_resolution,[],[f581,f561]) ).
fof(f584,definition,
( spl4_42
<=> greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl4_42])],[avatar_definition]) ).
fof(f585,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2))))
| spl4_42 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f586,plain,
( greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_42 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f587,plain,
( spl4_42
| spl4_41
| ~ spl4_33
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f582,f560,f527,f578,f584]) ).
fof(f588,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| zero = growth_rate(first_movers,sK3(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_37 ),
inference(resolution,[],[f549,f153]) ).
fof(f589,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| zero = growth_rate(first_movers,sK3(sK0(sK2))) )
| ~ spl4_37
| ~ spl4_39 ),
inference(forward_subsumption_resolution,[],[f588,f561]) ).
fof(f591,definition,
( spl4_43
<=> zero = growth_rate(first_movers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_43])],[avatar_definition]) ).
fof(f593,plain,
( zero = growth_rate(first_movers,sK3(sK0(sK2)))
| ~ spl4_43 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f594,plain,
( spl4_43
| spl4_41
| ~ spl4_37
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f589,f560,f547,f578,f591]) ).
fof(f596,plain,
( greater(equilibrium(sK2),sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_38 ),
inference(resolution,[],[f558,f146]) ).
fof(f601,plain,
( greater(equilibrium(sK2),sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_38
| ~ spl4_39 ),
inference(forward_subsumption_resolution,[],[f596,f561]) ).
fof(f604,definition,
( spl4_44
<=> sK0(sK2) = sK3(sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_44])],[avatar_definition]) ).
fof(f605,plain,
( sK0(sK2) != sK3(sK0(sK2))
| spl4_44 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f606,plain,
( sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_44 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f608,definition,
( spl4_45
<=> greater(equilibrium(sK2),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_45])],[avatar_definition]) ).
fof(f609,plain,
( ~ greater(equilibrium(sK2),sK0(sK2))
| spl4_45 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f610,plain,
( greater(equilibrium(sK2),sK0(sK2))
| ~ spl4_45 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f611,plain,
( spl4_44
| spl4_45
| ~ spl4_38
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f601,f560,f556,f608,f604]) ).
fof(f614,plain,
( ~ greater(growth_rate(first_movers,sK3(sK0(sK2))),zero)
| ~ spl4_40 ),
inference(resolution,[],[f576,f86]) ).
fof(f618,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_31 ),
inference(resolution,[],[f521,f154]) ).
fof(f619,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| zero = growth_rate(efficient_producers,sK3(sK0(sK2))) )
| ~ spl4_31
| ~ spl4_39 ),
inference(forward_subsumption_resolution,[],[f618,f561]) ).
fof(f621,definition,
( spl4_46
<=> zero = growth_rate(efficient_producers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_46])],[avatar_definition]) ).
fof(f622,plain,
( zero != growth_rate(efficient_producers,sK3(sK0(sK2)))
| spl4_46 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f623,plain,
( zero = growth_rate(efficient_producers,sK3(sK0(sK2)))
| ~ spl4_46 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f624,plain,
( spl4_46
| spl4_41
| ~ spl4_31
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f619,f560,f519,f578,f621]) ).
fof(f625,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(growth_rate(first_movers,sK3(sK1(sK2))),zero)
| ~ in_environment(sK2,sK1(sK2)) )
| ~ spl4_20 ),
inference(resolution,[],[f428,f167]) ).
fof(f626,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| ~ in_environment(sK2,sK1(sK2)) )
| ~ spl4_20
| ~ spl4_24 ),
inference(forward_subsumption_resolution,[],[f625,f499]) ).
fof(f627,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2))) )
| ~ spl4_20
| ~ spl4_23
| ~ spl4_24 ),
inference(forward_subsumption_resolution,[],[f626,f446]) ).
fof(f628,plain,
( spl4_25
| ~ spl4_20
| ~ spl4_23
| ~ spl4_24 ),
inference(avatar_split_clause,[],[f627,f459,f445,f426,f463]) ).
fof(f629,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ in_environment(sK2,sK1(sK2)) )
| ~ spl4_16 ),
inference(resolution,[],[f410,f168]) ).
fof(f630,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK1(sK2)))
| greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) )
| ~ spl4_16
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f629,f446]) ).
fof(f632,definition,
( spl4_47
<=> greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_47])],[avatar_definition]) ).
fof(f634,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ spl4_47 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,plain,
( spl4_47
| spl4_25
| ~ spl4_16
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f630,f445,f408,f463,f632]) ).
fof(f636,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK1(sK2))
| ~ spl4_25 ),
inference(resolution,[],[f464,f128]) ).
fof(f637,plain,
( ~ in_environment(sK2,sK1(sK2))
| ~ spl4_25 ),
inference(forward_subsumption_resolution,[],[f636,f106]) ).
fof(f638,plain,
( $false
| ~ spl4_23
| ~ spl4_25 ),
inference(forward_subsumption_resolution,[],[f637,f446]) ).
fof(f639,plain,
( ~ spl4_23
| ~ spl4_25 ),
inference(avatar_contradiction_clause,[],[f638]) ).
fof(f644,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ greater_or_equal(sK3(sK1(sK2)),sK1(sK2))
| ~ in_environment(sK2,sK1(sK2))
| ~ spl4_27 ),
inference(superposition,[],[f124,f478]) ).
fof(f647,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ in_environment(sK2,sK1(sK2))
| ~ spl4_27 ),
inference(forward_subsumption_resolution,[],[f644,f107]) ).
fof(f652,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ spl4_23
| ~ spl4_27 ),
inference(forward_subsumption_resolution,[],[f647,f446]) ).
fof(f655,plain,
( greater(zero,zero)
| ~ spl4_23
| ~ spl4_27
| ~ spl4_30 ),
inference(forward_demodulation,[],[f652,f508]) ).
fof(f658,plain,
( $false
| ~ spl4_23
| ~ spl4_27
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f655,f120]) ).
fof(f659,plain,
( ~ spl4_23
| ~ spl4_27
| ~ spl4_30 ),
inference(avatar_contradiction_clause,[],[f658]) ).
fof(f676,plain,
( greater(equilibrium(sK2),sK1(sK2))
| ~ spl4_22
| ~ spl4_28 ),
inference(superposition,[],[f443,f491]) ).
fof(f733,plain,
( spl4_29
| ~ spl4_22
| ~ spl4_28 ),
inference(avatar_split_clause,[],[f676,f489,f441,f493]) ).
fof(f770,plain,
( ~ greater(sK1(sK2),equilibrium(sK2))
| ~ spl4_29 ),
inference(resolution,[],[f495,f86]) ).
fof(f812,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(growth_rate(first_movers,sK3(sK0(sK2))),zero)
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_36 ),
inference(resolution,[],[f543,f167]) ).
fof(f813,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_36
| ~ spl4_40 ),
inference(forward_subsumption_resolution,[],[f812,f614]) ).
fof(f814,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2))) )
| ~ spl4_36
| ~ spl4_39
| ~ spl4_40 ),
inference(forward_subsumption_resolution,[],[f813,f561]) ).
fof(f815,plain,
( spl4_41
| ~ spl4_36
| ~ spl4_39
| ~ spl4_40 ),
inference(avatar_split_clause,[],[f814,f574,f560,f541,f578]) ).
fof(f816,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_41 ),
inference(resolution,[],[f579,f128]) ).
fof(f817,plain,
( ~ in_environment(sK2,sK0(sK2))
| ~ spl4_41 ),
inference(forward_subsumption_resolution,[],[f816,f106]) ).
fof(f818,plain,
( $false
| ~ spl4_39
| ~ spl4_41 ),
inference(forward_subsumption_resolution,[],[f817,f561]) ).
fof(f819,plain,
( ~ spl4_39
| ~ spl4_41 ),
inference(avatar_contradiction_clause,[],[f818]) ).
fof(f821,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_32 ),
inference(resolution,[],[f525,f168]) ).
fof(f822,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK3(sK0(sK2)))
| greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero) )
| ~ spl4_32
| ~ spl4_39 ),
inference(forward_subsumption_resolution,[],[f821,f561]) ).
fof(f824,definition,
( spl4_51
<=> greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl4_51])],[avatar_definition]) ).
fof(f826,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ spl4_51 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f827,plain,
( spl4_51
| spl4_41
| ~ spl4_32
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f822,f560,f523,f578,f824]) ).
fof(f829,plain,
( greater_or_equal(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ spl4_51 ),
inference(resolution,[],[f826,f91]) ).
fof(f830,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK3(sK0(sK2))))
| ~ spl4_51 ),
inference(resolution,[],[f826,f86]) ).
fof(f832,plain,
( ~ spl4_42
| ~ spl4_51 ),
inference(avatar_split_clause,[],[f830,f824,f584]) ).
fof(f833,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_51 ),
inference(resolution,[],[f829,f93]) ).
fof(f865,plain,
( ! [X0] :
( outcompetes(efficient_producers,first_movers,sK3(sK0(sK2)))
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2))) )
| ~ spl4_40
| ~ spl4_51 ),
inference(resolution,[],[f833,f576]) ).
fof(f867,definition,
( spl4_52
<=> ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_52])],[avatar_definition]) ).
fof(f868,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK0(sK2)))
| ~ environment(X0) )
| ~ spl4_52 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f870,definition,
( spl4_53
<=> outcompetes(efficient_producers,first_movers,sK3(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_53])],[avatar_definition]) ).
fof(f872,plain,
( outcompetes(efficient_producers,first_movers,sK3(sK0(sK2)))
| ~ spl4_53 ),
inference(avatar_component_clause,[],[f870]) ).
fof(f873,plain,
( spl4_52
| spl4_53
| ~ spl4_40
| ~ spl4_51 ),
inference(avatar_split_clause,[],[f865,f824,f574,f870,f867]) ).
fof(f886,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_52 ),
inference(resolution,[],[f868,f108]) ).
fof(f887,plain,
( ~ in_environment(sK2,sK0(sK2))
| ~ spl4_52 ),
inference(forward_subsumption_resolution,[],[f886,f106]) ).
fof(f888,plain,
( $false
| ~ spl4_39
| ~ spl4_52 ),
inference(forward_subsumption_resolution,[],[f887,f561]) ).
fof(f889,plain,
( ~ spl4_39
| ~ spl4_52 ),
inference(avatar_contradiction_clause,[],[f888]) ).
fof(f890,plain,
( ~ in_environment(sK2,sK0(sK2))
| ~ spl4_53 ),
inference(resolution,[],[f872,f109]) ).
fof(f891,plain,
( $false
| ~ spl4_39
| ~ spl4_53 ),
inference(forward_subsumption_resolution,[],[f890,f561]) ).
fof(f892,plain,
( ~ spl4_39
| ~ spl4_53 ),
inference(avatar_contradiction_clause,[],[f891]) ).
fof(f911,plain,
( greater(equilibrium(sK2),sK0(sK2))
| ~ spl4_38
| ~ spl4_44 ),
inference(superposition,[],[f558,f606]) ).
fof(f913,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK0(sK2)))
| spl4_42
| ~ spl4_44 ),
inference(superposition,[],[f585,f606]) ).
fof(f919,plain,
( greater(growth_rate(efficient_producers,sK0(sK2)),growth_rate(first_movers,sK0(sK2)))
| ~ greater_or_equal(sK0(sK2),sK1(sK2))
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_44 ),
inference(superposition,[],[f124,f606]) ).
fof(f930,plain,
( ! [X0] :
( ~ constant(cardinality_at_time(efficient_producers,sK0(sK2)))
| ~ environment(X0)
| ~ in_environment(X0,sK0(sK2))
| zero = growth_rate(efficient_producers,sK0(sK2))
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_44 ),
inference(superposition,[],[f154,f606]) ).
fof(f934,plain,
( ~ greater(growth_rate(first_movers,sK0(sK2)),growth_rate(efficient_producers,sK0(sK2)))
| ~ greater_or_equal(sK0(sK2),sK1(sK2))
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_44 ),
inference(superposition,[],[f159,f606]) ).
fof(f936,plain,
( ! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK0(sK2)))
| ~ environment(X0)
| ~ in_environment(X0,sK0(sK2))
| greater(zero,growth_rate(efficient_producers,sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_44 ),
inference(superposition,[],[f164,f606]) ).
fof(f937,plain,
( ! [X0] :
( ~ increases(cardinality_at_time(first_movers,sK0(sK2)))
| ~ environment(X0)
| ~ in_environment(X0,sK0(sK2))
| greater(growth_rate(first_movers,sK0(sK2)),zero)
| ~ in_environment(sK2,sK0(sK2)) )
| ~ spl4_44 ),
inference(superposition,[],[f167,f606]) ).
fof(f943,plain,
( constant(number_of_organizations(sK2,sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2))
| greater(equilibrium(sK2),sK0(sK2))
| ~ spl4_44 ),
inference(superposition,[],[f277,f606]) ).
fof(f946,plain,
( ~ in_environment(sK2,sK0(sK2))
| greater(equilibrium(sK2),sK0(sK2))
| spl4_11
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f943,f250]) ).
fof(f952,plain,
( ! [X0] :
( ~ increases(cardinality_at_time(first_movers,sK0(sK2)))
| ~ environment(X0)
| ~ in_environment(X0,sK0(sK2))
| greater(growth_rate(first_movers,sK0(sK2)),zero) )
| ~ spl4_39
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f937,f561]) ).
fof(f953,plain,
( ! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK0(sK2)))
| ~ environment(X0)
| ~ in_environment(X0,sK0(sK2))
| greater(zero,growth_rate(efficient_producers,sK0(sK2))) )
| ~ spl4_39
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f936,f561]) ).
fof(f955,plain,
( ~ greater(growth_rate(first_movers,sK0(sK2)),growth_rate(efficient_producers,sK0(sK2)))
| ~ greater_or_equal(sK0(sK2),sK1(sK2))
| ~ spl4_39
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f934,f561]) ).
fof(f959,plain,
( ! [X0] :
( ~ constant(cardinality_at_time(efficient_producers,sK0(sK2)))
| ~ environment(X0)
| ~ in_environment(X0,sK0(sK2))
| zero = growth_rate(efficient_producers,sK0(sK2)) )
| ~ spl4_39
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f930,f561]) ).
fof(f969,plain,
( greater(growth_rate(efficient_producers,sK0(sK2)),growth_rate(first_movers,sK0(sK2)))
| ~ greater_or_equal(sK0(sK2),sK1(sK2))
| ~ spl4_39
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f919,f561]) ).
fof(f971,plain,
( spl4_45
| ~ spl4_38
| ~ spl4_44 ),
inference(avatar_split_clause,[],[f911,f604,f556,f608]) ).
fof(f977,plain,
( greater(equilibrium(sK2),sK0(sK2))
| spl4_11
| ~ spl4_39
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f946,f561]) ).
fof(f979,definition,
( spl4_54
<=> greater_or_equal(sK0(sK2),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_54])],[avatar_definition]) ).
fof(f981,plain,
( ~ greater_or_equal(sK0(sK2),sK1(sK2))
| spl4_54 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f994,plain,
( ! [X0] :
( ~ decreases(cardinality_at_time(efficient_producers,sK0(sK2)))
| ~ environment(X0)
| ~ in_environment(X0,sK0(sK2)) )
| ~ spl4_39
| spl4_42
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f953,f913]) ).
fof(f996,definition,
( spl4_57
<=> greater(growth_rate(first_movers,sK0(sK2)),growth_rate(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_57])],[avatar_definition]) ).
fof(f998,plain,
( ~ greater(growth_rate(first_movers,sK0(sK2)),growth_rate(efficient_producers,sK0(sK2)))
| spl4_57 ),
inference(avatar_component_clause,[],[f996]) ).
fof(f999,plain,
( ~ spl4_54
| ~ spl4_57
| ~ spl4_39
| ~ spl4_44 ),
inference(avatar_split_clause,[],[f955,f604,f560,f996,f979]) ).
fof(f1001,definition,
( spl4_58
<=> zero = growth_rate(efficient_producers,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_58])],[avatar_definition]) ).
fof(f1003,plain,
( zero = growth_rate(efficient_producers,sK0(sK2))
| ~ spl4_58 ),
inference(avatar_component_clause,[],[f1001]) ).
fof(f1005,definition,
( spl4_59
<=> ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK0(sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl4_59])],[avatar_definition]) ).
fof(f1006,plain,
( ! [X0] :
( ~ in_environment(X0,sK0(sK2))
| ~ environment(X0) )
| ~ spl4_59 ),
inference(avatar_component_clause,[],[f1005]) ).
fof(f1007,plain,
( spl4_58
| spl4_59
| ~ spl4_8
| ~ spl4_39
| ~ spl4_44 ),
inference(avatar_split_clause,[],[f959,f604,f560,f236,f1005,f1001]) ).
fof(f1009,definition,
( spl4_60
<=> zero = growth_rate(first_movers,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f1010,plain,
( zero != growth_rate(first_movers,sK0(sK2))
| spl4_60 ),
inference(avatar_component_clause,[],[f1009]) ).
fof(f1011,plain,
( zero = growth_rate(first_movers,sK0(sK2))
| ~ spl4_60 ),
inference(avatar_component_clause,[],[f1009]) ).
fof(f1023,definition,
( spl4_63
<=> greater(growth_rate(efficient_producers,sK0(sK2)),growth_rate(first_movers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_63])],[avatar_definition]) ).
fof(f1025,plain,
( greater(growth_rate(efficient_producers,sK0(sK2)),growth_rate(first_movers,sK0(sK2)))
| ~ spl4_63 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1026,plain,
( ~ spl4_54
| spl4_63
| ~ spl4_39
| ~ spl4_44 ),
inference(avatar_split_clause,[],[f969,f604,f560,f1023,f979]) ).
fof(f1027,plain,
( spl4_45
| spl4_11
| ~ spl4_39
| ~ spl4_44 ),
inference(avatar_split_clause,[],[f977,f604,f560,f248,f608]) ).
fof(f1030,plain,
( spl4_59
| ~ spl4_10
| ~ spl4_39
| spl4_42
| ~ spl4_44 ),
inference(avatar_split_clause,[],[f994,f604,f584,f560,f244,f1005]) ).
fof(f1031,plain,
( ~ environment(sK2)
| ~ stable(sK2)
| ~ spl4_45 ),
inference(resolution,[],[f610,f133]) ).
fof(f1038,plain,
( ~ stable(sK2)
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f1031,f106]) ).
fof(f1040,plain,
( $false
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f1038,f105]) ).
fof(f1041,plain,
~ spl4_45,
inference(avatar_contradiction_clause,[],[f1040]) ).
fof(f1043,plain,
( constant(cardinality_at_time(efficient_producers,sK0(sK2)))
| ~ spl4_31
| ~ spl4_44 ),
inference(forward_demodulation,[],[f521,f606]) ).
fof(f1047,plain,
( zero = growth_rate(first_movers,sK0(sK2))
| ~ spl4_43
| ~ spl4_44 ),
inference(forward_demodulation,[],[f593,f606]) ).
fof(f1051,plain,
( $false
| spl4_8
| ~ spl4_31
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f1043,f237]) ).
fof(f1052,plain,
( spl4_8
| ~ spl4_31
| ~ spl4_44 ),
inference(avatar_contradiction_clause,[],[f1051]) ).
fof(f1070,plain,
( ~ in_environment(sK2,sK0(sK2))
| sK1(sK2) = sK0(sK2)
| ~ environment(sK2)
| ~ stable(sK2)
| greater(sK1(sK2),sK0(sK2))
| spl4_54 ),
inference(resolution,[],[f981,f284]) ).
fof(f1071,plain,
( sK1(sK2) = sK0(sK2)
| ~ environment(sK2)
| ~ stable(sK2)
| greater(sK1(sK2),sK0(sK2))
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f1070,f99]) ).
fof(f1072,plain,
( sK1(sK2) = sK0(sK2)
| ~ stable(sK2)
| greater(sK1(sK2),sK0(sK2))
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f1071,f106]) ).
fof(f1073,plain,
( sK1(sK2) = sK0(sK2)
| greater(sK1(sK2),sK0(sK2))
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f1072,f105]) ).
fof(f1075,definition,
( spl4_64
<=> greater(sK1(sK2),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_64])],[avatar_definition]) ).
fof(f1076,plain,
( ~ greater(sK1(sK2),sK0(sK2))
| spl4_64 ),
inference(avatar_component_clause,[],[f1075]) ).
fof(f1077,plain,
( greater(sK1(sK2),sK0(sK2))
| ~ spl4_64 ),
inference(avatar_component_clause,[],[f1075]) ).
fof(f1079,definition,
( spl4_65
<=> sK1(sK2) = sK0(sK2) ),
introduced(definition,[new_symbols(definition,[spl4_65])],[avatar_definition]) ).
fof(f1081,plain,
( sK1(sK2) = sK0(sK2)
| ~ spl4_65 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1082,plain,
( spl4_64
| spl4_65
| spl4_54 ),
inference(avatar_split_clause,[],[f1073,f979,f1079,f1075]) ).
fof(f1083,plain,
( ~ environment(sK2)
| ~ stable(sK2)
| equilibrium(sK2) = sK0(sK2)
| greater(sK1(sK2),equilibrium(sK2))
| ~ spl4_64 ),
inference(resolution,[],[f1077,f290]) ).
fof(f1088,plain,
( ~ stable(sK2)
| equilibrium(sK2) = sK0(sK2)
| greater(sK1(sK2),equilibrium(sK2))
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f1083,f106]) ).
fof(f1089,plain,
( equilibrium(sK2) = sK0(sK2)
| greater(sK1(sK2),equilibrium(sK2))
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f1088,f105]) ).
fof(f1090,plain,
( equilibrium(sK2) = sK0(sK2)
| ~ spl4_29
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f1089,f770]) ).
fof(f1112,plain,
( greater(sK1(sK2),equilibrium(sK2))
| ~ spl4_29
| ~ spl4_64 ),
inference(superposition,[],[f1077,f1090]) ).
fof(f1121,plain,
( $false
| ~ spl4_29
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f1112,f770]) ).
fof(f1122,plain,
( ~ spl4_29
| ~ spl4_64 ),
inference(avatar_contradiction_clause,[],[f1121]) ).
fof(f1160,plain,
( greater(equilibrium(sK2),sK0(sK2))
| ~ spl4_29
| ~ spl4_65 ),
inference(superposition,[],[f495,f1081]) ).
fof(f1193,plain,
( $false
| ~ spl4_29
| spl4_45
| ~ spl4_65 ),
inference(forward_subsumption_resolution,[],[f1160,f609]) ).
fof(f1194,plain,
( ~ spl4_29
| spl4_45
| ~ spl4_65 ),
inference(avatar_contradiction_clause,[],[f1193]) ).
fof(f1225,plain,
( $false
| ~ spl4_43
| ~ spl4_44
| spl4_60 ),
inference(forward_subsumption_resolution,[],[f1047,f1010]) ).
fof(f1226,plain,
( ~ spl4_43
| ~ spl4_44
| spl4_60 ),
inference(avatar_contradiction_clause,[],[f1225]) ).
fof(f1228,plain,
( greater(zero,growth_rate(first_movers,sK0(sK2)))
| ~ spl4_58
| ~ spl4_63 ),
inference(forward_demodulation,[],[f1025,f1003]) ).
fof(f1229,plain,
( ~ decreases(cardinality_at_time(first_movers,sK0(sK2)))
| spl4_35
| ~ spl4_44 ),
inference(forward_demodulation,[],[f537,f606]) ).
fof(f1231,plain,
( greater(growth_rate(efficient_producers,sK0(sK2)),zero)
| ~ spl4_44
| ~ spl4_51 ),
inference(forward_demodulation,[],[f826,f606]) ).
fof(f1237,plain,
( greater(zero,zero)
| ~ spl4_58
| ~ spl4_60
| ~ spl4_63 ),
inference(forward_demodulation,[],[f1228,f1011]) ).
fof(f1238,plain,
( $false
| ~ spl4_9
| spl4_35
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f1229,f242]) ).
fof(f1239,plain,
( ~ spl4_9
| spl4_35
| ~ spl4_44 ),
inference(avatar_contradiction_clause,[],[f1238]) ).
fof(f1241,plain,
( greater(zero,zero)
| ~ spl4_44
| ~ spl4_51
| ~ spl4_58 ),
inference(forward_demodulation,[],[f1231,f1003]) ).
fof(f1245,plain,
( $false
| ~ spl4_58
| ~ spl4_60
| ~ spl4_63 ),
inference(forward_subsumption_resolution,[],[f1237,f120]) ).
fof(f1246,plain,
( ~ spl4_58
| ~ spl4_60
| ~ spl4_63 ),
inference(avatar_contradiction_clause,[],[f1245]) ).
fof(f1247,plain,
( $false
| ~ spl4_44
| ~ spl4_51
| ~ spl4_58 ),
inference(forward_subsumption_resolution,[],[f1241,f120]) ).
fof(f1248,plain,
( ~ spl4_44
| ~ spl4_51
| ~ spl4_58 ),
inference(avatar_contradiction_clause,[],[f1247]) ).
fof(f1253,plain,
( greater(zero,growth_rate(efficient_producers,sK0(sK2)))
| ~ spl4_42
| ~ spl4_44 ),
inference(forward_demodulation,[],[f586,f606]) ).
fof(f1255,plain,
( zero != growth_rate(efficient_producers,sK0(sK2))
| ~ spl4_44
| spl4_46 ),
inference(forward_demodulation,[],[f622,f606]) ).
fof(f1257,plain,
( ~ spl4_58
| ~ spl4_44
| spl4_46 ),
inference(avatar_split_clause,[],[f1255,f621,f604,f1001]) ).
fof(f1258,plain,
( ~ environment(sK2)
| ~ environment(sK2)
| ~ stable(sK2)
| ~ spl4_59 ),
inference(resolution,[],[f1006,f99]) ).
fof(f1260,plain,
( ~ environment(sK2)
| ~ stable(sK2)
| ~ spl4_59 ),
inference(duplicate_literal_removal,[],[f1258]) ).
fof(f1263,plain,
( ~ stable(sK2)
| ~ spl4_59 ),
inference(forward_subsumption_resolution,[],[f1260,f106]) ).
fof(f1264,plain,
( $false
| ~ spl4_59 ),
inference(forward_subsumption_resolution,[],[f1263,f105]) ).
fof(f1265,plain,
~ spl4_59,
inference(avatar_contradiction_clause,[],[f1264]) ).
fof(f1266,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,sK0(sK2))
| greater(growth_rate(first_movers,sK0(sK2)),zero) )
| ~ spl4_14
| ~ spl4_39
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f952,f265]) ).
fof(f1268,definition,
( spl4_66
<=> greater(growth_rate(first_movers,sK0(sK2)),zero) ),
introduced(definition,[new_symbols(definition,[spl4_66])],[avatar_definition]) ).
fof(f1270,plain,
( greater(growth_rate(first_movers,sK0(sK2)),zero)
| ~ spl4_66 ),
inference(avatar_component_clause,[],[f1268]) ).
fof(f1271,plain,
( spl4_66
| spl4_59
| ~ spl4_14
| ~ spl4_39
| ~ spl4_44 ),
inference(avatar_split_clause,[],[f1266,f604,f560,f263,f1005,f1268]) ).
fof(f1331,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sK0(sK2)))
| ~ greater(X0,zero) )
| ~ spl4_42
| ~ spl4_44 ),
inference(resolution,[],[f1253,f87]) ).
fof(f1781,plain,
( ~ greater(growth_rate(first_movers,sK0(sK2)),zero)
| ~ spl4_42
| ~ spl4_44
| spl4_57 ),
inference(resolution,[],[f998,f1331]) ).
fof(f1784,plain,
( $false
| ~ spl4_42
| ~ spl4_44
| spl4_57
| ~ spl4_66 ),
inference(forward_subsumption_resolution,[],[f1781,f1270]) ).
fof(f1785,plain,
( ~ spl4_42
| ~ spl4_44
| spl4_57
| ~ spl4_66 ),
inference(avatar_contradiction_clause,[],[f1784]) ).
fof(f2800,definition,
( spl4_188
<=> outcompetes(efficient_producers,first_movers,sK3(sK1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl4_188])],[avatar_definition]) ).
fof(f2801,plain,
( outcompetes(efficient_producers,first_movers,sK3(sK1(sK2)))
| ~ spl4_188 ),
inference(avatar_component_clause,[],[f2800]) ).
fof(f2817,plain,
( greater_or_equal(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ spl4_47 ),
inference(resolution,[],[f634,f91]) ).
fof(f2818,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ~ spl4_47 ),
inference(resolution,[],[f634,f86]) ).
fof(f2820,plain,
( ~ spl4_26
| ~ spl4_47 ),
inference(avatar_split_clause,[],[f2818,f632,f469]) ).
fof(f2846,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_47 ),
inference(resolution,[],[f2817,f93]) ).
fof(f2900,plain,
( ! [X0] :
( outcompetes(efficient_producers,first_movers,sK3(sK1(sK2)))
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2))) )
| ~ spl4_24
| ~ spl4_47 ),
inference(resolution,[],[f2846,f461]) ).
fof(f2902,definition,
( spl4_195
<=> ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl4_195])],[avatar_definition]) ).
fof(f2903,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sK3(sK1(sK2)))
| ~ environment(X0) )
| ~ spl4_195 ),
inference(avatar_component_clause,[],[f2902]) ).
fof(f2904,plain,
( spl4_195
| spl4_188
| ~ spl4_24
| ~ spl4_47 ),
inference(avatar_split_clause,[],[f2900,f632,f459,f2800,f2902]) ).
fof(f2905,plain,
( ~ in_environment(sK2,sK1(sK2))
| ~ spl4_188 ),
inference(resolution,[],[f2801,f109]) ).
fof(f2906,plain,
( $false
| ~ spl4_23
| ~ spl4_188 ),
inference(forward_subsumption_resolution,[],[f2905,f446]) ).
fof(f2907,plain,
( ~ spl4_23
| ~ spl4_188 ),
inference(avatar_contradiction_clause,[],[f2906]) ).
fof(f2908,plain,
( ~ environment(sK2)
| ~ in_environment(sK2,sK1(sK2))
| ~ spl4_195 ),
inference(resolution,[],[f2903,f108]) ).
fof(f2909,plain,
( ~ in_environment(sK2,sK1(sK2))
| ~ spl4_195 ),
inference(forward_subsumption_resolution,[],[f2908,f106]) ).
fof(f2910,plain,
( $false
| ~ spl4_23
| ~ spl4_195 ),
inference(forward_subsumption_resolution,[],[f2909,f446]) ).
fof(f2911,plain,
( ~ spl4_23
| ~ spl4_195 ),
inference(avatar_contradiction_clause,[],[f2910]) ).
fof(f2912,plain,
( greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ~ greater_or_equal(sK3(sK1(sK2)),sK1(sK2))
| ~ in_environment(sK2,sK1(sK2))
| ~ spl4_26 ),
inference(resolution,[],[f471,f144]) ).
fof(f2923,plain,
( ~ greater_or_equal(sK3(sK1(sK2)),sK1(sK2))
| ~ in_environment(sK2,sK1(sK2))
| spl4_24
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f2912,f460]) ).
fof(f2924,plain,
( ~ in_environment(sK2,sK1(sK2))
| spl4_24
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f2923,f107]) ).
fof(f2925,plain,
( $false
| ~ spl4_23
| spl4_24
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f2924,f446]) ).
fof(f2926,plain,
( ~ spl4_23
| spl4_24
| ~ spl4_26 ),
inference(avatar_contradiction_clause,[],[f2925]) ).
fof(f3009,plain,
( greater(zero,zero)
| ~ spl4_42
| ~ spl4_46 ),
inference(forward_demodulation,[],[f586,f623]) ).
fof(f3013,plain,
( $false
| ~ spl4_42
| ~ spl4_46 ),
inference(forward_subsumption_resolution,[],[f3009,f120]) ).
fof(f3014,plain,
( ~ spl4_42
| ~ spl4_46 ),
inference(avatar_contradiction_clause,[],[f3013]) ).
fof(f3050,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ greater_or_equal(sK3(sK0(sK2)),sK1(sK2))
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_43 ),
inference(superposition,[],[f124,f593]) ).
fof(f3053,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ greater_or_equal(sK3(sK0(sK2)),sK1(sK2))
| ~ spl4_39
| ~ spl4_43 ),
inference(forward_subsumption_resolution,[],[f3050,f561]) ).
fof(f3057,plain,
( greater(zero,zero)
| ~ greater_or_equal(sK3(sK0(sK2)),sK1(sK2))
| ~ spl4_39
| ~ spl4_43
| ~ spl4_46 ),
inference(forward_demodulation,[],[f3053,f623]) ).
fof(f3061,plain,
( ~ greater_or_equal(sK3(sK0(sK2)),sK1(sK2))
| ~ spl4_39
| ~ spl4_43
| ~ spl4_46 ),
inference(forward_subsumption_resolution,[],[f3057,f120]) ).
fof(f3096,plain,
( ~ in_environment(sK2,sK0(sK2))
| greater(sK1(sK2),sK0(sK2))
| ~ in_environment(sK2,sK1(sK2))
| sK1(sK2) = sK3(sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_39
| ~ spl4_43
| ~ spl4_46 ),
inference(resolution,[],[f3061,f337]) ).
fof(f3099,plain,
( greater(sK1(sK2),sK0(sK2))
| ~ in_environment(sK2,sK1(sK2))
| sK1(sK2) = sK3(sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_39
| ~ spl4_43
| ~ spl4_46 ),
inference(forward_subsumption_resolution,[],[f3096,f561]) ).
fof(f3102,plain,
( ~ in_environment(sK2,sK1(sK2))
| sK1(sK2) = sK3(sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_39
| ~ spl4_43
| ~ spl4_46
| spl4_64 ),
inference(forward_subsumption_resolution,[],[f3099,f1076]) ).
fof(f3109,definition,
( spl4_202
<=> sK1(sK2) = sK3(sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_202])],[avatar_definition]) ).
fof(f3110,plain,
( sK1(sK2) != sK3(sK0(sK2))
| spl4_202 ),
inference(avatar_component_clause,[],[f3109]) ).
fof(f3111,plain,
( sK1(sK2) = sK3(sK0(sK2))
| ~ spl4_202 ),
inference(avatar_component_clause,[],[f3109]) ).
fof(f3117,plain,
( sK1(sK2) = sK3(sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_23
| ~ spl4_39
| ~ spl4_43
| ~ spl4_46
| spl4_64 ),
inference(forward_subsumption_resolution,[],[f3102,f446]) ).
fof(f3119,plain,
( sK1(sK2) = sK3(sK0(sK2))
| ~ spl4_23
| ~ spl4_39
| ~ spl4_43
| spl4_44
| ~ spl4_46
| spl4_64 ),
inference(forward_subsumption_resolution,[],[f3117,f605]) ).
fof(f3120,plain,
( spl4_202
| ~ spl4_23
| ~ spl4_39
| ~ spl4_43
| spl4_44
| ~ spl4_46
| spl4_64 ),
inference(avatar_split_clause,[],[f3119,f1075,f621,f604,f591,f560,f445,f3109]) ).
fof(f3124,plain,
( ~ greater(equilibrium(sK2),sK1(sK2))
| spl4_38
| ~ spl4_202 ),
inference(superposition,[],[f557,f3111]) ).
fof(f3221,plain,
( $false
| ~ spl4_29
| spl4_38
| ~ spl4_202 ),
inference(forward_subsumption_resolution,[],[f3124,f495]) ).
fof(f3222,plain,
( ~ spl4_29
| spl4_38
| ~ spl4_202 ),
inference(avatar_contradiction_clause,[],[f3221]) ).
fof(f3275,definition,
( spl4_204
<=> greater_or_equal(sK3(sK0(sK2)),sK1(sK2)) ),
introduced(definition,[new_symbols(definition,[spl4_204])],[avatar_definition]) ).
fof(f3276,plain,
( greater_or_equal(sK3(sK0(sK2)),sK1(sK2))
| ~ spl4_204 ),
inference(avatar_component_clause,[],[f3275]) ).
fof(f3277,plain,
( ~ greater_or_equal(sK3(sK0(sK2)),sK1(sK2))
| spl4_204 ),
inference(avatar_component_clause,[],[f3275]) ).
fof(f3298,plain,
( greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ greater_or_equal(sK3(sK0(sK2)),sK1(sK2))
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_42 ),
inference(resolution,[],[f586,f144]) ).
fof(f3323,plain,
( ~ in_environment(sK2,sK0(sK2))
| greater(sK1(sK2),sK0(sK2))
| ~ in_environment(sK2,sK1(sK2))
| sK1(sK2) = sK3(sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| spl4_204 ),
inference(resolution,[],[f3277,f337]) ).
fof(f3326,plain,
( greater(sK1(sK2),sK0(sK2))
| ~ in_environment(sK2,sK1(sK2))
| sK1(sK2) = sK3(sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_39
| spl4_204 ),
inference(forward_subsumption_resolution,[],[f3323,f561]) ).
fof(f3329,plain,
( ~ in_environment(sK2,sK1(sK2))
| sK1(sK2) = sK3(sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_39
| spl4_64
| spl4_204 ),
inference(forward_subsumption_resolution,[],[f3326,f1076]) ).
fof(f3332,plain,
( sK1(sK2) = sK3(sK0(sK2))
| sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_23
| ~ spl4_39
| spl4_64
| spl4_204 ),
inference(forward_subsumption_resolution,[],[f3329,f446]) ).
fof(f3335,plain,
( sK0(sK2) = sK3(sK0(sK2))
| ~ spl4_23
| ~ spl4_39
| spl4_64
| spl4_202
| spl4_204 ),
inference(forward_subsumption_resolution,[],[f3332,f3110]) ).
fof(f3337,plain,
( $false
| ~ spl4_23
| ~ spl4_39
| spl4_44
| spl4_64
| spl4_202
| spl4_204 ),
inference(forward_subsumption_resolution,[],[f3335,f605]) ).
fof(f3338,plain,
( ~ spl4_23
| ~ spl4_39
| spl4_44
| spl4_64
| spl4_202
| spl4_204 ),
inference(avatar_contradiction_clause,[],[f3337]) ).
fof(f3339,plain,
( greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ in_environment(sK2,sK0(sK2))
| ~ spl4_42
| ~ spl4_204 ),
inference(forward_subsumption_resolution,[],[f3298,f3276]) ).
fof(f3340,plain,
( ~ in_environment(sK2,sK0(sK2))
| spl4_40
| ~ spl4_42
| ~ spl4_204 ),
inference(forward_subsumption_resolution,[],[f3339,f575]) ).
fof(f3341,plain,
( $false
| ~ spl4_39
| spl4_40
| ~ spl4_42
| ~ spl4_204 ),
inference(forward_subsumption_resolution,[],[f3340,f561]) ).
fof(f3342,plain,
( ~ spl4_39
| spl4_40
| ~ spl4_42
| ~ spl4_204 ),
inference(avatar_contradiction_clause,[],[f3341]) ).
cnf(s5,plain,
( spl4_8
| spl4_9
| spl4_10
| ~ spl4_11 ),
inference(sat_conversion,[],[f251]) ).
cnf(s8,plain,
( spl4_8
| spl4_9
| ~ spl4_11
| spl4_14 ),
inference(sat_conversion,[],[f266]) ).
cnf(s9,plain,
( spl4_15
| spl4_16
| spl4_17
| ~ spl4_18 ),
inference(sat_conversion,[],[f419]) ).
cnf(s10,plain,
( spl4_15
| spl4_17
| ~ spl4_18
| spl4_19 ),
inference(sat_conversion,[],[f424]) ).
cnf(s11,plain,
( spl4_15
| spl4_16
| ~ spl4_18
| spl4_20 ),
inference(sat_conversion,[],[f429]) ).
cnf(s13,plain,
( spl4_16
| spl4_17
| ~ spl4_18
| spl4_21 ),
inference(sat_conversion,[],[f435]) ).
cnf(s14,plain,
( spl4_17
| ~ spl4_18
| spl4_19
| spl4_21 ),
inference(sat_conversion,[],[f436]) ).
cnf(s15,plain,
( spl4_16
| ~ spl4_18
| spl4_20
| spl4_21 ),
inference(sat_conversion,[],[f437]) ).
cnf(s17,plain,
( spl4_18
| spl4_22
| ~ spl4_23 ),
inference(sat_conversion,[],[f448]) ).
cnf(s18,plain,
spl4_23,
inference(sat_conversion,[],[f452]) ).
cnf(s19,plain,
( ~ spl4_19
| ~ spl4_23
| spl4_24
| spl4_25 ),
inference(sat_conversion,[],[f465]) ).
cnf(s20,plain,
( ~ spl4_17
| ~ spl4_23
| spl4_25
| spl4_26 ),
inference(sat_conversion,[],[f472]) ).
cnf(s21,plain,
( ~ spl4_21
| ~ spl4_23
| spl4_25
| spl4_27 ),
inference(sat_conversion,[],[f479]) ).
cnf(s22,plain,
( ~ spl4_22
| ~ spl4_23
| spl4_28
| spl4_29 ),
inference(sat_conversion,[],[f496]) ).
cnf(s23,plain,
( ~ spl4_15
| ~ spl4_23
| spl4_25
| spl4_30 ),
inference(sat_conversion,[],[f509]) ).
cnf(s24,plain,
( spl4_31
| spl4_32
| spl4_33
| ~ spl4_34 ),
inference(sat_conversion,[],[f534]) ).
cnf(s25,plain,
( spl4_31
| spl4_33
| ~ spl4_34
| spl4_35 ),
inference(sat_conversion,[],[f539]) ).
cnf(s26,plain,
( spl4_31
| spl4_32
| ~ spl4_34
| spl4_36 ),
inference(sat_conversion,[],[f544]) ).
cnf(s28,plain,
( spl4_32
| spl4_33
| ~ spl4_34
| spl4_37 ),
inference(sat_conversion,[],[f550]) ).
cnf(s29,plain,
( spl4_33
| ~ spl4_34
| spl4_35
| spl4_37 ),
inference(sat_conversion,[],[f551]) ).
cnf(s32,plain,
( spl4_34
| spl4_38
| ~ spl4_39 ),
inference(sat_conversion,[],[f563]) ).
cnf(s33,plain,
spl4_39,
inference(sat_conversion,[],[f567]) ).
cnf(s34,plain,
( ~ spl4_35
| ~ spl4_39
| spl4_40
| spl4_41 ),
inference(sat_conversion,[],[f580]) ).
cnf(s35,plain,
( ~ spl4_33
| ~ spl4_39
| spl4_41
| spl4_42 ),
inference(sat_conversion,[],[f587]) ).
cnf(s36,plain,
( ~ spl4_37
| ~ spl4_39
| spl4_41
| spl4_43 ),
inference(sat_conversion,[],[f594]) ).
cnf(s37,plain,
( ~ spl4_38
| ~ spl4_39
| spl4_44
| spl4_45 ),
inference(sat_conversion,[],[f611]) ).
cnf(s38,plain,
( ~ spl4_31
| ~ spl4_39
| spl4_41
| spl4_46 ),
inference(sat_conversion,[],[f624]) ).
cnf(s39,plain,
( ~ spl4_20
| ~ spl4_23
| ~ spl4_24
| spl4_25 ),
inference(sat_conversion,[],[f628]) ).
cnf(s40,plain,
( ~ spl4_16
| ~ spl4_23
| spl4_25
| spl4_47 ),
inference(sat_conversion,[],[f635]) ).
cnf(s41,plain,
( ~ spl4_23
| ~ spl4_25 ),
inference(sat_conversion,[],[f639]) ).
cnf(s43,plain,
( ~ spl4_23
| ~ spl4_27
| ~ spl4_30 ),
inference(sat_conversion,[],[f659]) ).
cnf(s44,plain,
( ~ spl4_22
| ~ spl4_28
| spl4_29 ),
inference(sat_conversion,[],[f733]) ).
cnf(s54,plain,
( ~ spl4_36
| ~ spl4_39
| ~ spl4_40
| spl4_41 ),
inference(sat_conversion,[],[f815]) ).
cnf(s55,plain,
( ~ spl4_39
| ~ spl4_41 ),
inference(sat_conversion,[],[f819]) ).
cnf(s56,plain,
( ~ spl4_32
| ~ spl4_39
| spl4_41
| spl4_51 ),
inference(sat_conversion,[],[f827]) ).
cnf(s57,plain,
( ~ spl4_42
| ~ spl4_51 ),
inference(sat_conversion,[],[f832]) ).
cnf(s58,plain,
( ~ spl4_40
| ~ spl4_51
| spl4_52
| spl4_53 ),
inference(sat_conversion,[],[f873]) ).
cnf(s59,plain,
( ~ spl4_39
| ~ spl4_52 ),
inference(sat_conversion,[],[f889]) ).
cnf(s60,plain,
( ~ spl4_39
| ~ spl4_53 ),
inference(sat_conversion,[],[f892]) ).
cnf(s61,plain,
( ~ spl4_38
| ~ spl4_44
| spl4_45 ),
inference(sat_conversion,[],[f971]) ).
cnf(s69,plain,
( ~ spl4_39
| ~ spl4_44
| ~ spl4_54
| ~ spl4_57 ),
inference(sat_conversion,[],[f999]) ).
cnf(s70,plain,
( ~ spl4_8
| ~ spl4_39
| ~ spl4_44
| spl4_58
| spl4_59 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s74,plain,
( ~ spl4_39
| ~ spl4_44
| ~ spl4_54
| spl4_63 ),
inference(sat_conversion,[],[f1026]) ).
cnf(s75,plain,
( spl4_11
| ~ spl4_39
| ~ spl4_44
| spl4_45 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s78,plain,
( ~ spl4_10
| ~ spl4_39
| spl4_42
| ~ spl4_44
| spl4_59 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s79,plain,
~ spl4_45,
inference(sat_conversion,[],[f1041]) ).
cnf(s80,plain,
( spl4_8
| ~ spl4_31
| ~ spl4_44 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s84,plain,
( spl4_54
| spl4_64
| spl4_65 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s85,plain,
( ~ spl4_29
| ~ spl4_64 ),
inference(sat_conversion,[],[f1122]) ).
cnf(s91,plain,
( ~ spl4_29
| spl4_45
| ~ spl4_65 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s100,plain,
( ~ spl4_43
| ~ spl4_44
| spl4_60 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s101,plain,
( ~ spl4_9
| spl4_35
| ~ spl4_44 ),
inference(sat_conversion,[],[f1239]) ).
cnf(s103,plain,
( ~ spl4_58
| ~ spl4_60
| ~ spl4_63 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s104,plain,
( ~ spl4_44
| ~ spl4_51
| ~ spl4_58 ),
inference(sat_conversion,[],[f1248]) ).
cnf(s105,plain,
( ~ spl4_44
| spl4_46
| ~ spl4_58 ),
inference(sat_conversion,[],[f1257]) ).
cnf(s107,plain,
~ spl4_59,
inference(sat_conversion,[],[f1265]) ).
cnf(s108,plain,
( ~ spl4_14
| ~ spl4_39
| ~ spl4_44
| spl4_59
| spl4_66 ),
inference(sat_conversion,[],[f1271]) ).
cnf(s134,plain,
( ~ spl4_42
| ~ spl4_44
| spl4_57
| ~ spl4_66 ),
inference(sat_conversion,[],[f1785]) ).
cnf(s216,plain,
( ~ spl4_26
| ~ spl4_47 ),
inference(sat_conversion,[],[f2820]) ).
cnf(s220,plain,
( ~ spl4_24
| ~ spl4_47
| spl4_188
| spl4_195 ),
inference(sat_conversion,[],[f2904]) ).
cnf(s221,plain,
( ~ spl4_23
| ~ spl4_188 ),
inference(sat_conversion,[],[f2907]) ).
cnf(s222,plain,
( ~ spl4_23
| ~ spl4_195 ),
inference(sat_conversion,[],[f2911]) ).
cnf(s224,plain,
( ~ spl4_23
| spl4_24
| ~ spl4_26 ),
inference(sat_conversion,[],[f2926]) ).
cnf(s243,plain,
( ~ spl4_42
| ~ spl4_46 ),
inference(sat_conversion,[],[f3014]) ).
cnf(s247,plain,
( ~ spl4_23
| ~ spl4_39
| ~ spl4_43
| spl4_44
| ~ spl4_46
| spl4_64
| spl4_202 ),
inference(sat_conversion,[],[f3120]) ).
cnf(s249,plain,
( ~ spl4_29
| spl4_38
| ~ spl4_202 ),
inference(sat_conversion,[],[f3222]) ).
cnf(s264,plain,
( ~ spl4_23
| ~ spl4_39
| spl4_44
| spl4_64
| spl4_202
| spl4_204 ),
inference(sat_conversion,[],[f3338]) ).
cnf(s265,plain,
( ~ spl4_39
| spl4_40
| ~ spl4_42
| ~ spl4_204 ),
inference(sat_conversion,[],[f3342]) ).
cnf(s266,plain,
( ~ spl4_10
| ~ spl4_39
| spl4_42
| ~ spl4_44 ),
inference(rat,[],[s78,s107]) ).
cnf(s269,plain,
( spl4_11
| ~ spl4_39
| ~ spl4_44 ),
inference(rat,[],[s75,s79]) ).
cnf(s271,plain,
( ~ spl4_8
| ~ spl4_39
| ~ spl4_44
| spl4_58 ),
inference(rat,[],[s70,s107]) ).
cnf(s273,plain,
( ~ spl4_38
| ~ spl4_44 ),
inference(rat,[],[s61,s79]) ).
cnf(s278,plain,
( ~ spl4_38
| ~ spl4_39
| spl4_44 ),
inference(rat,[],[s37,s79]) ).
cnf(s279,plain,
~ spl4_53,
inference(rat,[],[s60,s33]) ).
cnf(s280,plain,
~ spl4_52,
inference(rat,[],[s59,s33]) ).
cnf(s281,plain,
~ spl4_41,
inference(rat,[],[s55,s33]) ).
cnf(s282,plain,
( spl4_34
| spl4_38 ),
inference(rat,[],[s32,s33]) ).
cnf(s283,plain,
~ spl4_195,
inference(rat,[],[s222,s18]) ).
cnf(s284,plain,
~ spl4_188,
inference(rat,[],[s221,s18]) ).
cnf(s286,plain,
~ spl4_25,
inference(rat,[],[s41,s18]) ).
cnf(s287,plain,
( spl4_18
| spl4_22 ),
inference(rat,[],[s17,s18]) ).
cnf(s288,plain,
( spl4_32
| spl4_31
| ~ spl4_204
| ~ spl4_34 ),
inference(rat,[],[s265,s54,s35,s26,s24,s33,s281]) ).
cnf(s289,plain,
( spl4_31
| ~ spl4_204
| ~ spl4_34 ),
inference(rat,[],[s25,s35,s34,s57,s58,s56,s288,s279,s280,s33,s281]) ).
cnf(s290,plain,
( spl4_37
| spl4_33
| ~ spl4_34 ),
inference(rat,[],[s58,s56,s34,s28,s29,s281,s33,s279,s280]) ).
cnf(s291,plain,
( ~ spl4_29
| spl4_44 ),
inference(rat,[],[s290,s36,s35,s247,s243,s38,s289,s264,s249,s85,s282,s278,s281,s33,s18]) ).
cnf(s292,plain,
( ~ spl4_18
| spl4_16
| spl4_15 ),
inference(rat,[],[s224,s20,s39,s9,s11,s286,s18]) ).
cnf(s293,plain,
( ~ spl4_18
| spl4_15 ),
inference(rat,[],[s10,s20,s19,s216,s220,s40,s292,s283,s284,s18,s286]) ).
cnf(s294,plain,
( spl4_16
| ~ spl4_18
| spl4_21 ),
inference(rat,[],[s224,s39,s20,s15,s13,s286,s18]) ).
cnf(s295,plain,
( ~ spl4_18
| spl4_21 ),
inference(rat,[],[s14,s20,s19,s216,s220,s40,s294,s283,s284,s18,s286]) ).
cnf(s296,plain,
~ spl4_18,
inference(rat,[],[s295,s21,s43,s23,s293,s286,s18]) ).
cnf(s297,plain,
spl4_22,
inference(rat,[],[s287,s296]) ).
cnf(s298,plain,
( ~ spl4_29
| spl4_9
| spl4_8 ),
inference(rat,[],[s134,s266,s108,s5,s8,s69,s269,s84,s291,s85,s91,s33,s107,s79]) ).
cnf(s300,plain,
( spl4_8
| ~ spl4_29 ),
inference(rat,[],[s26,s56,s54,s58,s34,s101,s80,s298,s282,s273,s291,s33,s281,s280,s279]) ).
cnf(s301,plain,
~ spl4_29,
inference(rat,[],[s28,s35,s36,s56,s243,s100,s104,s105,s103,s271,s300,s282,s74,s273,s84,s291,s85,s91,s281,s33,s79]) ).
cnf(s303,plain,
spl4_28,
inference(rat,[],[s22,s297,s18,s301]) ).
cnf(s304,plain,
$false,
inference(rat,[],[s44,s297,s301,s303]) ).
fof(f3343,plain,
$false,
inference(avatar_sat_refutation,[],[s304]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 17:22:49 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.69/1.79 % (3630115)Detected formulas, will run a generic FOF schedule.
% 5.69/1.79 % (3630217)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3052126868:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.69/1.79 % (3630220)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=389185965:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.69/1.79 % (3630221)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=911196928:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.69/1.79 % (3630218)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3505812550:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.69/1.79 % (3630219)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3178074889:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.69/1.79 % (3630222)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3622868740:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.69/1.79 % (3630223)dis-21_1_sil=8000:lcm=predicate:random_seed=210493388:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.69/1.79 % (3630220)Instruction limit reached!
% 5.69/1.79 % (3630220)------------------------------
% 5.69/1.79 % (3630220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.79 % (3630220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.79 % (3630220)CaDiCaL version: 2.1.3
% 5.69/1.79 % (3630220)Termination reason: Instruction limit
% 5.69/1.79 % (3630220)Termination phase: Saturation
% 5.69/1.79 % (3630220)Time elapsed: 0.090 s
% 5.69/1.79 % (3630220)Peak memory usage: 89 MB
% 5.69/1.79 % (3630220)Instructions burned: 109 (million)
% 5.69/1.79 % (3630221)Instruction limit reached!
% 5.69/1.79 % (3630221)------------------------------
% 5.69/1.79 % (3630221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.79 % (3630221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.79 % (3630221)CaDiCaL version: 2.1.3
% 5.69/1.79 % (3630221)Termination reason: Instruction limit
% 5.69/1.79 % (3630221)Termination phase: Saturation
% 5.69/1.79 % (3630221)Time elapsed: 0.100 s
% 5.69/1.79 % (3630221)Peak memory usage: 87 MB
% 5.69/1.79 % (3630221)Instructions burned: 119 (million)
% 5.69/1.79 % (3630223)Instruction limit reached!
% 5.69/1.79 % (3630223)------------------------------
% 5.69/1.79 % (3630223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.79 % (3630223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.79 % (3630223)CaDiCaL version: 2.1.3
% 5.69/1.79 % (3630223)Termination reason: Instruction limit
% 5.69/1.79 % (3630223)Termination phase: Saturation
% 5.69/1.79 % (3630223)Time elapsed: 0.088 s
% 5.69/1.79 % (3630223)Peak memory usage: 88 MB
% 5.69/1.79 % (3630223)Instructions burned: 130 (million)
% 5.69/1.79 % (3630222)Instruction limit reached!
% 5.69/1.79 % (3630222)------------------------------
% 5.69/1.79 % (3630222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.79 % (3630222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.79 % (3630222)CaDiCaL version: 2.1.3
% 5.69/1.79 % (3630222)Termination reason: Instruction limit
% 5.69/1.79 % (3630222)Termination phase: Saturation
% 5.69/1.79 % (3630222)Time elapsed: 0.133 s
% 5.69/1.79 % (3630222)Peak memory usage: 89 MB
% 5.69/1.79 % (3630222)Instructions burned: 140 (million)
% 5.69/1.79 % (3630261)lrs+10_1_sil=32000:urr=on:br=off:random_seed=668193008:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.69/1.79 % (3630260)lrs+10_1_sil=8000:sp=occurrence:random_seed=923521488:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.69/1.79 % (3630263)lrs+1011_1_sil=32000:sp=occurrence:random_seed=399771669:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.69/1.79 % (3630265)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=159343137:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 5.69/1.79 % (3630261)Instruction limit reached!
% 5.69/1.79 % (3630261)------------------------------
% 5.69/1.79 % (3630261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.79 % (3630261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.79 % (3630261)CaDiCaL version: 2.1.3
% 5.69/1.79 % (3630261)Termination reason: Instruction limit
% 5.69/1.79 % (3630261)Termination phase: Saturation
% 5.69/1.79 % (3630261)Time elapsed: 0.077 s
% 5.69/1.79 % (3630261)Peak memory usage: 89 MB
% 5.69/1.79 % (3630261)Instructions burned: 158 (million)
% 5.69/1.79 % (3630260)Instruction limit reached!
% 5.69/1.79 % (3630260)------------------------------
% 5.69/1.79 % (3630260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.79 % (3630260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.79 % (3630260)CaDiCaL version: 2.1.3
% 5.69/1.79 % (3630260)Termination reason: Instruction limit
% 5.69/1.79 % (3630260)Termination phase: Saturation
% 5.69/1.79 % (3630260)Time elapsed: 0.164 s
% 5.69/1.79 % (3630260)Peak memory usage: 91 MB
% 5.69/1.79 % (3630260)Instructions burned: 287 (million)
% 5.69/1.79 % (3630265)Instruction limit reached!
% 5.69/1.80 % (3630265)------------------------------
% 5.69/1.80 % (3630265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.80 % (3630265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.80 % (3630265)CaDiCaL version: 2.1.3
% 5.69/1.80 % (3630265)Termination reason: Instruction limit
% 5.69/1.80 % (3630265)Termination phase: Saturation
% 5.69/1.80 % (3630265)Time elapsed: 0.138 s
% 5.69/1.80 % (3630265)Peak memory usage: 90 MB
% 5.69/1.80 % (3630265)Instructions burned: 250 (million)
% 5.69/1.80 % (3630318)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=215802682:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.69/1.80 % (3630263)Instruction limit reached!
% 5.69/1.80 % (3630263)------------------------------
% 5.69/1.80 % (3630263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.80 % (3630263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.80 % (3630263)CaDiCaL version: 2.1.3
% 5.69/1.80 % (3630263)Termination reason: Instruction limit
% 5.69/1.80 % (3630263)Termination phase: Saturation
% 5.69/1.80 % (3630263)Time elapsed: 0.215 s
% 5.69/1.80 % (3630263)Peak memory usage: 91 MB
% 5.69/1.80 % (3630263)Instructions burned: 326 (million)
% 5.69/1.80 % (3630350)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4231047542:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.69/1.80 % (3630217)First to succeed.
% 5.69/1.80 % (3630217)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3630115"
% 5.69/1.80 % (3630365)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1888726403:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 5.69/1.80 % (3630371)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1626706502:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 5.69/1.80 % (3630318)Instruction limit reached!
% 5.69/1.80 % (3630318)------------------------------
% 5.69/1.80 % (3630318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.80 % (3630318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.80 % (3630318)CaDiCaL version: 2.1.3
% 5.69/1.80 % (3630318)Termination reason: Instruction limit
% 5.69/1.80 % (3630318)Termination phase: Saturation
% 5.69/1.80 % (3630318)Time elapsed: 0.147 s
% 5.69/1.80 % (3630318)Peak memory usage: 88 MB
% 5.69/1.80 % (3630318)Instructions burned: 295 (million)
% 5.69/1.80 % (3630365)Instruction limit reached!
% 5.69/1.80 % (3630365)------------------------------
% 5.69/1.80 % (3630365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.80 % (3630365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.80 % (3630365)CaDiCaL version: 2.1.3
% 5.69/1.80 % (3630365)Termination reason: Instruction limit
% 5.69/1.80 % (3630365)Termination phase: Saturation
% 5.69/1.80 % (3630365)Time elapsed: 0.078 s
% 5.69/1.80 % (3630365)Peak memory usage: 90 MB
% 5.69/1.80 % (3630365)Instructions burned: 114 (million)
% 5.69/1.80 % (3630371)Instruction limit reached!
% 5.69/1.80 % (3630371)------------------------------
% 5.69/1.80 % (3630371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.69/1.80 % (3630371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.80 % (3630371)CaDiCaL version: 2.1.3
% 5.69/1.80 % (3630371)Termination reason: Instruction limit
% 5.69/1.80 % (3630371)Termination phase: Saturation
% 5.69/1.80 % (3630371)Time elapsed: 0.066 s
% 5.69/1.80 % (3630371)Peak memory usage: 88 MB
% 5.69/1.80 % (3630371)Instructions burned: 128 (million)
% 5.69/1.80 % (3630217)Refutation found. Thanks to Tanya!
% 5.69/1.80 % SZS status Theorem for theBenchmark
% 5.69/1.80 % SZS output start Proof for theBenchmark
% See solution above
% 7.12/2.00 % (3630217)------------------------------
% 7.12/2.00 % (3630217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.00 % (3630217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.00 % (3630217)CaDiCaL version: 2.1.3
% 7.12/2.00 % (3630217)Termination reason: Refutation
% 7.12/2.00 % (3630217)Time elapsed: 0.636 s
% 7.12/2.00 % (3630217)Peak memory usage: 133 MB
% 7.12/2.00 % (3630217)Instructions burned: 1350 (million)
% 7.12/2.00 % (3630217)------------------------------
% 7.12/2.00 % (3630217)------------------------------
% 7.12/2.00 % (3630115)Success in time 0.932 s
% 7.12/2.00 % Vampire exiting
%------------------------------------------------------------------------------