%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n002.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 : Fri Sep 25 02:12:32 PM UTC 2026
% Result : Theorem 2.24s 1.20s
% Output : CNFRefutation 2.24s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2,X3] :
( ( greater(growth_rate(X2,X3),growth_rate(X1,X3))
& subpopulations(X1,X2,X0,X3)
& environment(X0) )
=> selection_favors(X2,X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp1_high_growth_rates) ).
fof(f2,axiom,
! [X0,X1,X2,X3] :
( ( cardinality_at_time(X2,X3) = zero
& greater(cardinality_at_time(X1,X3),zero)
& subpopulation(X2,X0,X3)
& subpopulation(X1,X0,X3)
& environment(X0) )
=> selection_favors(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp2_favour_members) ).
fof(f3,axiom,
! [X0] :
( ( ! [X1] :
( ( in_environment(X0,X1)
& environment(X1) )
=> selection_favors(efficient_producers,first_movers,end_time(X1)) )
& propagation_strategy(efficient_producers)
& propagation_strategy(first_movers)
& observational_period(X0) )
=> selection_favors(efficient_producers,first_movers,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_favoured_trategy) ).
fof(f4,axiom,
! [X0] :
( ( slow_change(X0)
& observational_period(X0) )
=> ! [X1] :
( ( in_environment(X0,X1)
& environment(X1) )
=> ? [X2] :
( greater(X2,critical_point(X1))
& in_environment(X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp4_critical_point) ).
fof(f5,axiom,
propagation_strategy(first_movers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_organizational_sets1) ).
fof(f6,axiom,
propagation_strategy(efficient_producers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_organizational_sets2) ).
fof(f7,axiom,
! [X0,X1] :
( ( greater_or_equal(end_time(X0),X1)
& greater_or_equal(X1,start_time(X0))
& environment(X0) )
=> in_environment(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_time_in_environment) ).
fof(f8,axiom,
! [X0,X1] :
( ( in_environment(X0,X1)
& environment(X0) )
=> greater_or_equal(end_time(X0),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_environment_end_point) ).
fof(f9,axiom,
! [X0,X1] :
( ( greater(cardinality_at_time(efficient_producers,X1),zero)
& greater(cardinality_at_time(first_movers,X1),zero)
& in_environment(X0,X1)
& environment(X0) )
=> subpopulations(first_movers,efficient_producers,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_contains_FM_and_EP) ).
fof(f10,axiom,
! [X0,X1] :
( ( in_environment(X0,X1)
& environment(X0) )
=> greater_or_equal(cardinality_at_time(first_movers,X1),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_first_movers_exist) ).
fof(f11,axiom,
! [X0,X1] :
( ( in_environment(X0,X1)
& environment(X0) )
=> ( subpopulation(efficient_producers,X0,X1)
& subpopulation(first_movers,X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_subpopulations) ).
fof(f12,axiom,
! [X0] :
( environment(X0)
=> greater_or_equal(critical_point(X0),appear(efficient_producers,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_critical_point_after_EP) ).
fof(f13,axiom,
! [X0] :
( environment(X0)
=> greater_or_equal(critical_point(X0),start_time(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_time_of_critical_point) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( greater(X1,X2)
& greater(X0,X1) )
=> greater(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity) ).
fof(f16,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
<=> ( X0 = X1
| greater(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal) ).
fof(f17,axiom,
! [X0,X1] :
( ( X1 = critical_point(X0)
& environment(X0) )
=> ( ! [X2] :
( ( greater(X2,X1)
& subpopulations(first_movers,efficient_producers,X0,X2) )
=> greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) )
& ~ greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1) ).
fof(f18,axiom,
! [X0,X1] :
( ( greater_or_equal(X1,appear(efficient_producers,X0))
& in_environment(X0,X1)
& environment(X0) )
=> greater(cardinality_at_time(efficient_producers,X1),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6) ).
fof(f19,conjecture,
! [X0] :
( ( slow_change(X0)
& observational_period(X0) )
=> selection_favors(efficient_producers,first_movers,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t8) ).
fof(f20,negated_conjecture,
~ ! [X0] :
( ( slow_change(X0)
& observational_period(X0) )
=> selection_favors(efficient_producers,first_movers,X0) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [X0,X1,X2,X3] :
( ~ greater(growth_rate(X2,X3),growth_rate(X1,X3))
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| selection_favors(X2,X1,X3) ),
inference(ennf_transformation,[],[f1]) ).
fof(f22,plain,
! [X0,X1,X2,X3] :
( ~ greater(growth_rate(X2,X3),growth_rate(X1,X3))
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| selection_favors(X2,X1,X3) ),
inference(flattening,[],[f21]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( zero != cardinality_at_time(X2,X3)
| ~ greater(cardinality_at_time(X1,X3),zero)
| ~ subpopulation(X2,X0,X3)
| ~ subpopulation(X1,X0,X3)
| ~ environment(X0)
| selection_favors(X1,X2,X3) ),
inference(ennf_transformation,[],[f2]) ).
fof(f24,plain,
! [X0,X1,X2,X3] :
( zero != cardinality_at_time(X2,X3)
| ~ greater(cardinality_at_time(X1,X3),zero)
| ~ subpopulation(X2,X0,X3)
| ~ subpopulation(X1,X0,X3)
| ~ environment(X0)
| selection_favors(X1,X2,X3) ),
inference(flattening,[],[f23]) ).
fof(f25,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& environment(X1)
& ~ selection_favors(efficient_producers,first_movers,end_time(X1)) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0)
| selection_favors(efficient_producers,first_movers,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f26,plain,
! [X0] :
( ? [X1] :
( in_environment(X0,X1)
& environment(X1)
& ~ selection_favors(efficient_producers,first_movers,end_time(X1)) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0)
| selection_favors(efficient_producers,first_movers,X0) ),
inference(flattening,[],[f25]) ).
fof(f27,plain,
! [X0] :
( ~ slow_change(X0)
| ~ observational_period(X0)
| ! [X1] :
( ~ in_environment(X0,X1)
| ~ environment(X1)
| ? [X2] :
( greater(X2,critical_point(X1))
& in_environment(X1,X2) ) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f28,plain,
! [X0] :
( ~ slow_change(X0)
| ~ observational_period(X0)
| ! [X1] :
( ~ in_environment(X0,X1)
| ~ environment(X1)
| ? [X2] :
( greater(X2,critical_point(X1))
& in_environment(X1,X2) ) ) ),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( ~ greater_or_equal(end_time(X0),X1)
| ~ greater_or_equal(X1,start_time(X0))
| ~ environment(X0)
| in_environment(X0,X1) ),
inference(ennf_transformation,[],[f7]) ).
fof(f30,plain,
! [X0,X1] :
( ~ greater_or_equal(end_time(X0),X1)
| ~ greater_or_equal(X1,start_time(X0))
| ~ environment(X0)
| in_environment(X0,X1) ),
inference(flattening,[],[f29]) ).
fof(f31,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| greater_or_equal(end_time(X0),X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f32,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| greater_or_equal(end_time(X0),X1) ),
inference(flattening,[],[f31]) ).
fof(f33,plain,
! [X0,X1] :
( ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f34,plain,
! [X0,X1] :
( ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(flattening,[],[f33]) ).
fof(f35,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| greater_or_equal(cardinality_at_time(first_movers,X1),zero) ),
inference(ennf_transformation,[],[f10]) ).
fof(f36,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| greater_or_equal(cardinality_at_time(first_movers,X1),zero) ),
inference(flattening,[],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| ( subpopulation(efficient_producers,X0,X1)
& subpopulation(first_movers,X0,X1) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f38,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| ( subpopulation(efficient_producers,X0,X1)
& subpopulation(first_movers,X0,X1) ) ),
inference(flattening,[],[f37]) ).
fof(f39,plain,
! [X0] :
( ~ environment(X0)
| greater_or_equal(critical_point(X0),appear(efficient_producers,X0)) ),
inference(ennf_transformation,[],[f12]) ).
fof(f40,plain,
! [X0] :
( ~ environment(X0)
| greater_or_equal(critical_point(X0),start_time(X0)) ),
inference(ennf_transformation,[],[f13]) ).
fof(f41,plain,
! [X0,X1,X2] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(flattening,[],[f41]) ).
fof(f45,plain,
! [X0,X1] :
( critical_point(X0) != X1
| ~ environment(X0)
| ( ! [X2] :
( ~ greater(X2,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) )
& ~ greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f46,plain,
! [X0,X1] :
( critical_point(X0) != X1
| ~ environment(X0)
| ( ! [X2] :
( ~ greater(X2,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) )
& ~ greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)) ) ),
inference(flattening,[],[f45]) ).
fof(f47,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,appear(efficient_producers,X0))
| ~ in_environment(X0,X1)
| ~ environment(X0)
| greater(cardinality_at_time(efficient_producers,X1),zero) ),
inference(ennf_transformation,[],[f18]) ).
fof(f48,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,appear(efficient_producers,X0))
| ~ in_environment(X0,X1)
| ~ environment(X0)
| greater(cardinality_at_time(efficient_producers,X1),zero) ),
inference(flattening,[],[f47]) ).
fof(f49,plain,
? [X0] :
( slow_change(X0)
& observational_period(X0)
& ~ selection_favors(efficient_producers,first_movers,X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f50,plain,
? [X0] :
( slow_change(X0)
& observational_period(X0)
& ~ selection_favors(efficient_producers,first_movers,X0) ),
inference(flattening,[],[f49]) ).
fof(f51,plain,
! [X0] :
( ( in_environment(X0,sK0(X0))
& environment(sK0(X0))
& ~ selection_favors(efficient_producers,first_movers,end_time(sK0(X0))) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0)
| selection_favors(efficient_producers,first_movers,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f26]) ).
fof(f52,plain,
! [X0] :
( ~ slow_change(X0)
| ~ observational_period(X0)
| ! [X1] :
( ~ in_environment(X0,X1)
| ~ environment(X1)
| ( greater(sK1(X1),critical_point(X1))
& in_environment(X1,sK1(X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X1))],[f28]) ).
fof(f53,plain,
! [X0,X1] :
( ( ~ greater_or_equal(X0,X1)
| X0 = X1
| greater(X0,X1) )
& ( ( X0 != X1
& ~ greater(X0,X1) )
| greater_or_equal(X0,X1) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f54,plain,
! [X0,X1] :
( ( ~ greater_or_equal(X0,X1)
| X0 = X1
| greater(X0,X1) )
& ( ( X0 != X1
& ~ greater(X0,X1) )
| greater_or_equal(X0,X1) ) ),
inference(flattening,[],[f53]) ).
fof(f55,plain,
( slow_change(sK2)
& observational_period(sK2)
& ~ selection_favors(efficient_producers,first_movers,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f50]) ).
fof(f56,plain,
! [X2,X3,X0,X1] :
( ~ greater(growth_rate(X2,X3),growth_rate(X1,X3))
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| selection_favors(X2,X1,X3) ),
inference(cnf_transformation,[],[f22]) ).
fof(f57,plain,
! [X2,X3,X0,X1] :
( zero != cardinality_at_time(X2,X3)
| ~ greater(cardinality_at_time(X1,X3),zero)
| ~ subpopulation(X2,X0,X3)
| ~ subpopulation(X1,X0,X3)
| ~ environment(X0)
| selection_favors(X1,X2,X3) ),
inference(cnf_transformation,[],[f24]) ).
fof(f58,plain,
! [X0] :
( in_environment(X0,sK0(X0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0)
| selection_favors(efficient_producers,first_movers,X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f59,plain,
! [X0] :
( environment(sK0(X0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0)
| selection_favors(efficient_producers,first_movers,X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f60,plain,
! [X0] :
( ~ selection_favors(efficient_producers,first_movers,end_time(sK0(X0)))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0)
| selection_favors(efficient_producers,first_movers,X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f61,plain,
! [X0,X1] :
( ~ slow_change(X0)
| ~ observational_period(X0)
| ~ in_environment(X0,X1)
| ~ environment(X1)
| greater(sK1(X1),critical_point(X1)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f62,plain,
! [X0,X1] :
( ~ slow_change(X0)
| ~ observational_period(X0)
| ~ in_environment(X0,X1)
| ~ environment(X1)
| in_environment(X1,sK1(X1)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f63,plain,
propagation_strategy(first_movers),
inference(cnf_transformation,[],[f5]) ).
fof(f64,plain,
propagation_strategy(efficient_producers),
inference(cnf_transformation,[],[f6]) ).
fof(f65,plain,
! [X0,X1] :
( ~ greater_or_equal(end_time(X0),X1)
| ~ greater_or_equal(X1,start_time(X0))
| ~ environment(X0)
| in_environment(X0,X1) ),
inference(cnf_transformation,[],[f30]) ).
fof(f66,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| greater_or_equal(end_time(X0),X1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f67,plain,
! [X0,X1] :
( ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f68,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| greater_or_equal(cardinality_at_time(first_movers,X1),zero) ),
inference(cnf_transformation,[],[f36]) ).
fof(f69,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulation(efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
fof(f70,plain,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulation(first_movers,X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
fof(f71,plain,
! [X0] :
( ~ environment(X0)
| greater_or_equal(critical_point(X0),appear(efficient_producers,X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f72,plain,
! [X0] :
( ~ environment(X0)
| greater_or_equal(critical_point(X0),start_time(X0)) ),
inference(cnf_transformation,[],[f40]) ).
fof(f73,plain,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f75,plain,
! [X0,X1] :
( ~ greater_or_equal(X0,X1)
| X0 = X1
| greater(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f76,plain,
! [X0,X1] :
( X0 != X1
| greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f77,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f78,plain,
! [X2,X0,X1] :
( critical_point(X0) != X1
| ~ environment(X0)
| ~ greater(X2,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ),
inference(cnf_transformation,[],[f46]) ).
fof(f80,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,appear(efficient_producers,X0))
| ~ in_environment(X0,X1)
| ~ environment(X0)
| greater(cardinality_at_time(efficient_producers,X1),zero) ),
inference(cnf_transformation,[],[f48]) ).
fof(f81,plain,
slow_change(sK2),
inference(cnf_transformation,[],[f55]) ).
fof(f82,plain,
observational_period(sK2),
inference(cnf_transformation,[],[f55]) ).
fof(f83,plain,
~ selection_favors(efficient_producers,first_movers,sK2),
inference(cnf_transformation,[],[f55]) ).
fof(f84,plain,
! [X1] : greater_or_equal(X1,X1),
inference(equality_resolution,[],[f76]) ).
fof(f86,plain,
! [X2,X0] :
( ~ environment(X0)
| ~ greater(X2,critical_point(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ),
inference(equality_resolution,[],[f78]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( selection_favors(X0,X2,X1)
| ~ environment(X3)
| ~ subpopulations(X2,X0,X3,X1)
| ~ greater(growth_rate(X0,X1),growth_rate(X2,X1)) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( selection_favors(X2,X0,X1)
| ~ environment(X3)
| ~ subpopulation(X2,X3,X1)
| ~ subpopulation(X0,X3,X1)
| ~ greater(cardinality_at_time(X2,X1),zero)
| ( cardinality_at_time(X0,X1) != zero ) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_51,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(X0))) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_52,plain,
! [X0: $i] :
( environment(sK0(X0))
| selection_favors(efficient_producers,first_movers,X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(X0) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_53,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sK0(X0))
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ~ observational_period(X0) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( in_environment(X1,sK1(X1))
| ~ slow_change(X0)
| ~ observational_period(X0)
| ~ environment(X1)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( greater(sK1(X1),critical_point(X1))
| ~ slow_change(X0)
| ~ observational_period(X0)
| ~ environment(X1)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_56,plain,
propagation_strategy(first_movers),
inference(cnf_transformation,[],[f63]) ).
tcf(c_57,plain,
propagation_strategy(efficient_producers),
inference(cnf_transformation,[],[f64]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( in_environment(X0,X1)
| ~ environment(X0)
| ~ greater_or_equal(X1,start_time(X0))
| ~ greater_or_equal(end_time(X0),X1) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(end_time(X0),X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( subpopulations(first_movers,efficient_producers,X1,X0)
| ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( subpopulation(first_movers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( subpopulation(efficient_producers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_64,plain,
! [X0: $i] :
( greater_or_equal(critical_point(X0),appear(efficient_producers,X0))
| ~ environment(X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_65,plain,
! [X0: $i] :
( greater_or_equal(critical_point(X0),start_time(X0))
| ~ environment(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X2,X1)
| ~ greater(X2,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_69,plain,
! [X0: $i] : greater_or_equal(X0,X0),
inference(cnf_transformation,[],[f84]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] :
( greater(X0,X1)
| ( X0 = X1 )
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ environment(X0)
| ~ greater(X1,critical_point(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater_or_equal(X0,appear(efficient_producers,X1)) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_74,negated_conjecture,
~ selection_favors(efficient_producers,first_movers,sK2),
inference(cnf_transformation,[],[f83]) ).
tcf(c_75,negated_conjecture,
observational_period(sK2),
inference(cnf_transformation,[],[f82]) ).
tcf(c_76,negated_conjecture,
slow_change(sK2),
inference(cnf_transformation,[],[f81]) ).
tcf(c_98,plain,
! [X0: $i] :
( environment(sK0(X0))
| selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0) ),
inference(global_subsumption_just,[status(thm)],[c_52,c_57,c_56,c_52]) ).
tcf(c_101,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sK0(X0))
| ~ observational_period(X0) ),
inference(global_subsumption_just,[status(thm)],[c_53,c_57,c_56,c_53]) ).
tcf(c_104,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_51,c_57,c_56,c_51]) ).
tcf(c_438,plain,
! [X0: $i,X1: $i] :
( greater(sK1(X1),critical_point(X1))
| ~ observational_period(X0)
| ~ environment(X1)
| ~ in_environment(X0,X1)
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_76]) ).
tcf(c_439,plain,
! [X0: $i] :
( greater(sK1(X0),critical_point(X0))
| ~ observational_period(sK2)
| ~ environment(X0)
| ~ in_environment(sK2,X0) ),
inference(unflattening,[status(thm)],[c_438]) ).
tcf(c_441,plain,
! [X0: $i] :
( greater(sK1(X0),critical_point(X0))
| ~ in_environment(sK2,X0)
| ~ environment(X0) ),
inference(global_subsumption_just,[status(thm)],[c_439,c_75,c_439]) ).
tcf(c_442,plain,
! [X0: $i] :
( greater(sK1(X0),critical_point(X0))
| ~ environment(X0)
| ~ in_environment(sK2,X0) ),
inference(renaming,[status(thm)],[c_441]) ).
tcf(c_453,plain,
! [X0: $i,X1: $i] :
( in_environment(X1,sK1(X1))
| ~ observational_period(X0)
| ~ environment(X1)
| ~ in_environment(X0,X1)
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_76]) ).
tcf(c_454,plain,
! [X0: $i] :
( in_environment(X0,sK1(X0))
| ~ observational_period(sK2)
| ~ environment(X0)
| ~ in_environment(sK2,X0) ),
inference(unflattening,[status(thm)],[c_453]) ).
tcf(c_456,plain,
! [X0: $i] :
( in_environment(X0,sK1(X0))
| ~ in_environment(sK2,X0)
| ~ environment(X0) ),
inference(global_subsumption_just,[status(thm)],[c_454,c_75,c_454]) ).
tcf(c_457,plain,
! [X0: $i] :
( in_environment(X0,sK1(X0))
| ~ environment(X0)
| ~ in_environment(sK2,X0) ),
inference(renaming,[status(thm)],[c_456]) ).
tcf(c_474,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(X0)))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_104,c_75]) ).
tcf(c_475,plain,
( selection_favors(efficient_producers,first_movers,sK2)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))) ),
inference(unflattening,[status(thm)],[c_474]) ).
tcf(c_476,plain,
~ selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))),
inference(global_subsumption_just,[status(thm)],[c_475,c_74,c_475]) ).
tcf(c_481,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sK0(X0))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_101,c_75]) ).
tcf(c_482,plain,
( in_environment(sK2,sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(unflattening,[status(thm)],[c_481]) ).
tcf(c_488,plain,
! [X0: $i] :
( environment(sK0(X0))
| selection_favors(efficient_producers,first_movers,X0)
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_98,c_75]) ).
tcf(c_489,plain,
( environment(sK0(sK2))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(unflattening,[status(thm)],[c_488]) ).
tcf(c_490,plain,
environment(sK0(sK2)),
inference(global_subsumption_just,[status(thm)],[c_489,c_74,c_489]) ).
tcf(c_498,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( selection_favors(X0,X3,X1)
| ~ environment(X5)
| ~ environment(X4)
| ~ in_environment(X5,X2)
| ~ greater(cardinality_at_time(first_movers,X2),zero)
| ~ greater(cardinality_at_time(efficient_producers,X2),zero)
| ~ greater(growth_rate(X0,X1),growth_rate(X3,X1))
| ( X4 != X5 )
| ( X3 != first_movers )
| ( X1 != X2 )
| ( X0 != efficient_producers ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_60]) ).
tcf(c_499,plain,
! [X0: $i,X1: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(unflattening,[status(thm)],[c_498]) ).
tcf(c_519,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ environment(X3)
| ~ environment(X2)
| ~ in_environment(X2,X0)
| ~ greater(X1,critical_point(X3))
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ( first_movers != first_movers )
| ( efficient_producers != efficient_producers )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_72]) ).
tcf(c_520,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater(X0,critical_point(X1))
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero) ),
inference(unflattening,[status(thm)],[c_519]) ).
tcf(c_570,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ environment(X3)
| ~ subpopulation(X2,X3,X1)
| ~ subpopulation(X0,X3,X1)
| ~ greater(cardinality_at_time(X2,X1),zero)
| ( X2 != efficient_producers )
| ( X0 != first_movers )
| ( end_time(sK0(sK2)) != X1 )
| ( cardinality_at_time(X0,X1) != zero ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_476]) ).
tcf(c_571,plain,
! [X0: $i] :
( ~ environment(X0)
| ~ subpopulation(first_movers,X0,end_time(sK0(sK2)))
| ~ subpopulation(efficient_producers,X0,end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero ) ),
inference(unflattening,[status(thm)],[c_570]) ).
tcf(c_606,plain,
! [X0: $i,X1: $i] :
( ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ( first_movers != first_movers )
| ( efficient_producers != efficient_producers )
| ( end_time(sK0(sK2)) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_499,c_476]) ).
tcf(c_607,plain,
! [X0: $i] :
( ~ environment(X0)
| ~ in_environment(X0,end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(unflattening,[status(thm)],[c_606]) ).
tcf(c_644,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ in_environment(X0,X1)
| ~ greater(X1,critical_point(X0))
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_520,c_490]) ).
tcf(c_645,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ in_environment(sK0(sK2),X0)
| ~ greater(X0,critical_point(sK0(sK2)))
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero) ),
inference(unflattening,[status(thm)],[c_644]) ).
tcf(c_662,plain,
! [X0: $i,X1: $i] :
( greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ in_environment(X0,X1)
| ~ greater_or_equal(X1,appear(efficient_producers,X0))
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_73,c_490]) ).
tcf(c_663,plain,
! [X0: $i] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ in_environment(sK0(sK2),X0)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(sK2))) ),
inference(unflattening,[status(thm)],[c_662]) ).
tcf(c_686,plain,
! [X0: $i] :
( ~ in_environment(X0,end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_607,c_490]) ).
tcf(c_687,plain,
( ~ in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
inference(unflattening,[status(thm)],[c_686]) ).
tcf(c_714,plain,
! [X0: $i] :
( ~ subpopulation(first_movers,X0,end_time(sK0(sK2)))
| ~ subpopulation(efficient_producers,X0,end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ( sK0(sK2) != X0 )
| ( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero ) ),
inference(resolution_lifted,[status(thm)],[c_571,c_490]) ).
tcf(c_715,plain,
( ~ subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| ~ subpopulation(efficient_producers,sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ( cardinality_at_time(first_movers,end_time(sK0(sK2))) != zero ) ),
inference(unflattening,[status(thm)],[c_714]) ).
tcf(c_742,plain,
! [X0: $i] :
( in_environment(X0,sK1(X0))
| ~ in_environment(sK2,X0)
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_457,c_490]) ).
tcf(c_743,plain,
( in_environment(sK0(sK2),sK1(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(unflattening,[status(thm)],[c_742]) ).
tcf(c_744,plain,
in_environment(sK0(sK2),sK1(sK0(sK2))),
inference(global_subsumption_just,[status(thm)],[c_743,c_74,c_482,c_743]) ).
tcf(c_749,plain,
! [X0: $i] :
( greater(sK1(X0),critical_point(X0))
| ~ in_environment(sK2,X0)
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_442,c_490]) ).
tcf(c_750,plain,
( greater(sK1(sK0(sK2)),critical_point(sK0(sK2)))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(unflattening,[status(thm)],[c_749]) ).
tcf(c_751,plain,
greater(sK1(sK0(sK2)),critical_point(sK0(sK2))),
inference(global_subsumption_just,[status(thm)],[c_750,c_74,c_482,c_750]) ).
tcf(c_761,plain,
! [X0: $i] :
( greater_or_equal(critical_point(X0),start_time(X0))
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_65,c_490]) ).
tcf(c_762,plain,
greater_or_equal(critical_point(sK0(sK2)),start_time(sK0(sK2))),
inference(unflattening,[status(thm)],[c_761]) ).
tcf(c_766,plain,
! [X0: $i] :
( greater_or_equal(critical_point(X0),appear(efficient_producers,X0))
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_490]) ).
tcf(c_767,plain,
greater_or_equal(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2))),
inference(unflattening,[status(thm)],[c_766]) ).
tcf(c_771,plain,
! [X0: $i,X1: $i] :
( subpopulation(efficient_producers,X0,X1)
| ~ in_environment(X0,X1)
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_490]) ).
tcf(c_772,plain,
! [X0: $i] :
( subpopulation(efficient_producers,sK0(sK2),X0)
| ~ in_environment(sK0(sK2),X0) ),
inference(unflattening,[status(thm)],[c_771]) ).
tcf(c_780,plain,
! [X0: $i,X1: $i] :
( subpopulation(first_movers,X0,X1)
| ~ in_environment(X0,X1)
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_490]) ).
tcf(c_781,plain,
! [X0: $i] :
( subpopulation(first_movers,sK0(sK2),X0)
| ~ in_environment(sK0(sK2),X0) ),
inference(unflattening,[status(thm)],[c_780]) ).
tcf(c_789,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_490]) ).
tcf(c_790,plain,
! [X0: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X0),zero)
| ~ in_environment(sK0(sK2),X0) ),
inference(unflattening,[status(thm)],[c_789]) ).
tcf(c_798,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(end_time(X0),X1)
| ~ in_environment(X0,X1)
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_490]) ).
tcf(c_799,plain,
! [X0: $i] :
( greater_or_equal(end_time(sK0(sK2)),X0)
| ~ in_environment(sK0(sK2),X0) ),
inference(unflattening,[status(thm)],[c_798]) ).
tcf(c_807,plain,
! [X0: $i,X1: $i] :
( in_environment(X0,X1)
| ~ greater_or_equal(X1,start_time(X0))
| ~ greater_or_equal(end_time(X0),X1)
| ( sK0(sK2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_490]) ).
tcf(c_808,plain,
! [X0: $i] :
( in_environment(sK0(sK2),X0)
| ~ greater_or_equal(X0,start_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),X0) ),
inference(unflattening,[status(thm)],[c_807]) ).
tcf(c_1751,definition,
iPr_def_10 = sK0(sK2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_1752,definition,
iPr_def_11 = end_time(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_1753,definition,
iPr_def_12 = start_time(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_1754,definition,
iPr_def_13 = critical_point(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_1755,definition,
iPr_def_14 = appear(efficient_producers,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_1758,definition,
iPr_def_17 = sK1(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_1761,definition,
iPr_def_20 = cardinality_at_time(first_movers,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_1762,definition,
iPr_def_21 = cardinality_at_time(efficient_producers,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_1765,definition,
iPr_def_24 = growth_rate(efficient_producers,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_1766,definition,
iPr_def_25 = growth_rate(first_movers,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_1767,plain,
! [X0: $i] :
( in_environment(iPr_def_10,X0)
| ~ greater_or_equal(iPr_def_11,X0)
| ~ greater_or_equal(X0,iPr_def_12) ),
inference(demodulation,[status(thm)],[c_808,c_1753,c_1751,c_1752]) ).
tcf(c_1768,plain,
! [X0: $i] :
( greater_or_equal(iPr_def_11,X0)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_799]) ).
tcf(c_1769,plain,
! [X0: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X0),zero)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_790]) ).
tcf(c_1770,plain,
! [X0: $i] :
( subpopulation(first_movers,iPr_def_10,X0)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_781]) ).
tcf(c_1771,plain,
! [X0: $i] :
( subpopulation(efficient_producers,iPr_def_10,X0)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_772]) ).
tcf(c_1772,plain,
greater_or_equal(iPr_def_13,iPr_def_14),
inference(demodulation,[status(thm)],[c_767,c_1755,c_1754]) ).
tcf(c_1773,plain,
greater_or_equal(iPr_def_13,iPr_def_12),
inference(demodulation,[status(thm)],[c_762]) ).
tcf(c_1775,plain,
greater(iPr_def_17,iPr_def_13),
inference(demodulation,[status(thm)],[c_751,c_1758]) ).
tcf(c_1776,plain,
in_environment(iPr_def_10,iPr_def_17),
inference(demodulation,[status(thm)],[c_744]) ).
tcf(c_1778,plain,
( ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11)
| ( iPr_def_20 != zero ) ),
inference(demodulation,[status(thm)],[c_715,c_1762,c_1761]) ).
tcf(c_1780,plain,
( ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_20,zero) ),
inference(demodulation,[status(thm)],[c_687,c_1766,c_1765]) ).
tcf(c_1782,plain,
! [X0: $i] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,iPr_def_14)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_663]) ).
tcf(c_1783,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ in_environment(iPr_def_10,X0)
| ~ greater(X0,iPr_def_13)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero) ),
inference(demodulation,[status(thm)],[c_645]) ).
tcf(c_2258,plain,
greater_or_equal(iPr_def_11,iPr_def_17),
inference(superposition,[status(thm)],[c_1776,c_1768]) ).
tcf(c_2283,plain,
( in_environment(iPr_def_10,iPr_def_11)
| ~ greater_or_equal(iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_69,c_1767]) ).
tcf(c_2324,plain,
( greater_or_equal(iPr_def_20,zero)
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1761,c_1769]) ).
tcf(c_2327,plain,
( greater(iPr_def_21,zero)
| ~ greater_or_equal(iPr_def_11,iPr_def_14)
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1762,c_1782]) ).
tcf(c_2354,plain,
( greater(growth_rate(efficient_producers,iPr_def_11),iPr_def_25)
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_11,iPr_def_13)
| ~ greater(cardinality_at_time(first_movers,iPr_def_11),zero)
| ~ greater(cardinality_at_time(efficient_producers,iPr_def_11),zero) ),
inference(superposition,[status(thm)],[c_1766,c_1783]) ).
tcf(c_2355,plain,
( greater(iPr_def_24,iPr_def_25)
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_11,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_2354,c_1761,c_1762,c_1765]) ).
tcf(c_2429,plain,
! [X0: $i] :
( greater_or_equal(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,iPr_def_14)
| ~ in_environment(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_1782,c_68]) ).
tcf(c_2431,plain,
greater_or_equal(iPr_def_17,iPr_def_13),
inference(superposition,[status(thm)],[c_1775,c_68]) ).
tcf(c_2449,plain,
! [X0: $i,X1: $i] :
( greater(X0,growth_rate(first_movers,X1))
| ~ in_environment(iPr_def_10,X1)
| ~ greater(X1,iPr_def_13)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(X0,growth_rate(efficient_producers,X1)) ),
inference(superposition,[status(thm)],[c_1783,c_66]) ).
tcf(c_2450,plain,
! [X0: $i] :
( greater(X0,iPr_def_13)
| ~ greater(X0,iPr_def_17) ),
inference(superposition,[status(thm)],[c_1775,c_66]) ).
tcf(c_2473,plain,
! [X0: $i] :
( greater(cardinality_at_time(first_movers,X0),zero)
| ( cardinality_at_time(first_movers,X0) = zero )
| ~ in_environment(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_1769,c_70]) ).
tcf(c_2474,plain,
( greater(iPr_def_13,iPr_def_14)
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1772,c_70]) ).
tcf(c_2475,plain,
( greater(iPr_def_13,iPr_def_12)
| ( iPr_def_12 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_1773,c_70]) ).
tcf(c_2476,plain,
( greater(iPr_def_11,iPr_def_17)
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2258,c_70]) ).
tcf(c_2496,plain,
! [X0: $i] :
( greater(X0,iPr_def_14)
| ( iPr_def_13 = iPr_def_14 )
| ~ greater(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_2474,c_66]) ).
tcf(c_2506,plain,
! [X0: $i] :
( greater(X0,iPr_def_12)
| ( iPr_def_12 = iPr_def_13 )
| ~ greater(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_2475,c_66]) ).
tcf(c_2522,plain,
( greater(iPr_def_11,iPr_def_13)
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2476,c_2450]) ).
tcf(c_2559,plain,
( greater_or_equal(iPr_def_21,zero)
| ~ greater_or_equal(iPr_def_11,iPr_def_14)
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1762,c_2429]) ).
tcf(c_2585,plain,
( greater(iPr_def_20,zero)
| ( cardinality_at_time(first_movers,iPr_def_11) = zero )
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1761,c_2473]) ).
tcf(c_2589,plain,
( greater(iPr_def_20,zero)
| ( zero = iPr_def_20 )
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_2585,c_1761]) ).
tcf(c_2672,plain,
! [X0: $i,X1: $i] :
( greater(X0,growth_rate(first_movers,X1))
| ( cardinality_at_time(first_movers,X1) = zero )
| ~ in_environment(iPr_def_10,X1)
| ~ greater(X1,iPr_def_13)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(X0,growth_rate(efficient_producers,X1)) ),
inference(superposition,[status(thm)],[c_2473,c_2449]) ).
tcf(c_2699,plain,
( greater(iPr_def_17,iPr_def_14)
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1775,c_2496]) ).
tcf(c_2728,plain,
( greater_or_equal(iPr_def_11,iPr_def_13)
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2522,c_68]) ).
tcf(c_2729,plain,
( greater(iPr_def_11,iPr_def_12)
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2522,c_2506]) ).
tcf(c_2730,plain,
( greater(iPr_def_11,iPr_def_14)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2522,c_2496]) ).
tcf(c_2748,plain,
( greater_or_equal(iPr_def_17,iPr_def_14)
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2699,c_68]) ).
tcf(c_2922,plain,
( greater_or_equal(iPr_def_11,iPr_def_12)
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2729,c_68]) ).
tcf(c_2941,plain,
( greater_or_equal(iPr_def_11,iPr_def_14)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2730,c_68]) ).
tcf(c_2971,plain,
( in_environment(iPr_def_10,iPr_def_11)
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2922,c_2283]) ).
tcf(c_2986,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_2971,c_2589]) ).
tcf(c_2988,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2971,c_2327]) ).
tcf(c_3062,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_20 = zero )
| ~ greater_or_equal(iPr_def_20,zero) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_3075,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2941,c_2988]) ).
tcf(c_3184,plain,
( ~ greater(iPr_def_11,iPr_def_13)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_21,zero)
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_2355,c_1780,c_2355]) ).
tcf(c_3185,plain,
( ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_11,iPr_def_13) ),
inference(renaming,[status(thm)],[c_3184]) ).
tcf(c_3206,plain,
! [X0: $i,X1: $i] :
( greater(X0,growth_rate(first_movers,X1))
| ( cardinality_at_time(first_movers,X1) = zero )
| ~ greater_or_equal(X1,iPr_def_14)
| ~ in_environment(iPr_def_10,X1)
| ~ greater(X1,iPr_def_13)
| ~ greater(X0,growth_rate(efficient_producers,X1)) ),
inference(superposition,[status(thm)],[c_1782,c_2672]) ).
tcf(c_3208,plain,
! [X0: $i] :
( greater(X0,growth_rate(first_movers,iPr_def_11))
| ( cardinality_at_time(first_movers,iPr_def_11) = zero )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_11,iPr_def_13)
| ~ greater(X0,growth_rate(efficient_producers,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_1762,c_2672]) ).
tcf(c_3209,plain,
! [X0: $i] :
( greater(X0,iPr_def_25)
| ( zero = iPr_def_20 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_11,iPr_def_13)
| ~ greater(X0,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_3208,c_1761,c_1765,c_1766]) ).
tcf(c_3246,plain,
! [X0: $i] :
( greater(X0,growth_rate(first_movers,iPr_def_11))
| ( cardinality_at_time(first_movers,iPr_def_11) = zero )
| ~ greater_or_equal(iPr_def_11,iPr_def_14)
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_11,iPr_def_13)
| ~ greater(X0,iPr_def_24) ),
inference(superposition,[status(thm)],[c_1765,c_3206]) ).
tcf(c_3247,plain,
! [X0: $i] :
( greater(X0,iPr_def_25)
| ( zero = iPr_def_20 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14)
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_11,iPr_def_13)
| ~ greater(X0,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_3246,c_1761,c_1766]) ).
tcf(c_3279,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_3075,c_3185]) ).
tcf(c_3280,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_20,zero) ),
inference(superposition,[status(thm)],[c_3075,c_1780]) ).
tcf(c_3299,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ greater(iPr_def_20,zero) ),
inference(global_subsumption_just,[status(thm)],[c_3280,c_2522,c_2971,c_3279]) ).
tcf(c_3309,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_2986,c_3299]) ).
tcf(c_3347,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_3309,c_1778]) ).
tcf(c_3667,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_3347,c_3075,c_3347]) ).
tcf(c_3668,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(renaming,[status(thm)],[c_3667]) ).
tcf(c_3679,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1771,c_3668]) ).
tcf(c_3692,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_3679,c_2971,c_3679]) ).
tcf(c_3702,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1770,c_3692]) ).
tcf(c_3707,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_3702,c_2971,c_3702]) ).
tcf(c_3720,plain,
( greater_or_equal(iPr_def_11,iPr_def_14)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3707,c_2748]) ).
tcf(c_3727,plain,
( in_environment(iPr_def_10,iPr_def_11)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3707,c_1776]) ).
tcf(c_3728,plain,
( greater(iPr_def_11,iPr_def_13)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3707,c_1775]) ).
tcf(c_3809,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_3727,c_2589]) ).
tcf(c_3811,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_3727,c_2327]) ).
tcf(c_4034,plain,
( ~ greater(iPr_def_11,iPr_def_13)
| ~ greater(iPr_def_21,zero)
| ~ in_environment(iPr_def_10,iPr_def_11)
| ( zero = iPr_def_20 ) ),
inference(global_subsumption_just,[status(thm)],[c_3209,c_2589,c_3185]) ).
tcf(c_4035,plain,
( ( zero = iPr_def_20 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_11,iPr_def_13) ),
inference(renaming,[status(thm)],[c_4034]) ).
tcf(c_4075,plain,
( ~ greater(iPr_def_11,iPr_def_13)
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater_or_equal(iPr_def_11,iPr_def_14)
| ( zero = iPr_def_20 ) ),
inference(global_subsumption_just,[status(thm)],[c_3247,c_2327,c_4035]) ).
tcf(c_4076,plain,
( ( zero = iPr_def_20 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14)
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_11,iPr_def_13) ),
inference(renaming,[status(thm)],[c_4075]) ).
tcf(c_4085,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( zero = iPr_def_20 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_3720,c_4076]) ).
tcf(c_4127,plain,
( ( zero = iPr_def_20 )
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_3809,c_3728,c_3727,c_4085]) ).
tcf(c_4128,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ( zero = iPr_def_20 ) ),
inference(renaming,[status(thm)],[c_4127]) ).
tcf(c_4145,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_4128,c_1778]) ).
tcf(c_4406,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_4145,c_3720,c_3811,c_4145]) ).
tcf(c_4407,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(renaming,[status(thm)],[c_4406]) ).
tcf(c_4416,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1771,c_4407]) ).
tcf(c_4421,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_4416,c_3727,c_4416]) ).
tcf(c_4429,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1770,c_4421]) ).
tcf(c_4433,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_4429,c_3727,c_4429]) ).
tcf(c_4439,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( zero = iPr_def_20 )
| ~ greater_or_equal(iPr_def_11,iPr_def_13)
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_4433,c_4076]) ).
tcf(c_4444,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ greater_or_equal(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_4433,c_2988]) ).
tcf(c_4506,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_4444,c_2728,c_4444]) ).
tcf(c_4516,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_4506,c_3185]) ).
tcf(c_4517,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_20,zero) ),
inference(superposition,[status(thm)],[c_4506,c_1780]) ).
tcf(c_4533,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ greater(iPr_def_20,zero) ),
inference(global_subsumption_just,[status(thm)],[c_4517,c_2522,c_2971,c_4516]) ).
tcf(c_4541,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ( zero = iPr_def_20 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2986,c_4533]) ).
tcf(c_4562,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_4541,c_1778]) ).
tcf(c_4705,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_4562,c_2728,c_4444,c_4562]) ).
tcf(c_4706,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(renaming,[status(thm)],[c_4705]) ).
tcf(c_4715,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1771,c_4706]) ).
tcf(c_4720,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_4715,c_2971,c_4715]) ).
tcf(c_4728,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1770,c_4720]) ).
tcf(c_4732,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_4728,c_2971,c_4728]) ).
tcf(c_4749,plain,
( greater_or_equal(iPr_def_11,iPr_def_13)
| ( iPr_def_12 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_4732,c_2431]) ).
tcf(c_4751,plain,
( in_environment(iPr_def_10,iPr_def_11)
| ( iPr_def_12 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_4732,c_1776]) ).
tcf(c_4752,plain,
( greater(iPr_def_11,iPr_def_13)
| ( iPr_def_12 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_4732,c_1775]) ).
tcf(c_4783,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_12 = iPr_def_13 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_4751,c_2589]) ).
tcf(c_4901,plain,
( ( zero = iPr_def_20 )
| ( iPr_def_12 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_4783,c_4439,c_4752,c_4751,c_4749]) ).
tcf(c_4902,plain,
( ( iPr_def_12 = iPr_def_13 )
| ( zero = iPr_def_20 ) ),
inference(renaming,[status(thm)],[c_4901]) ).
tcf(c_4915,plain,
( ( iPr_def_12 = iPr_def_13 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_4902,c_1778]) ).
tcf(c_4919,plain,
! [X0: $i] :
( greater(cardinality_at_time(efficient_producers,X0),iPr_def_20)
| ( iPr_def_12 = iPr_def_13 )
| ~ greater_or_equal(X0,iPr_def_14)
| ~ in_environment(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_4902,c_1782]) ).
tcf(c_4920,plain,
! [X0: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X0),iPr_def_20)
| ( iPr_def_12 = iPr_def_13 )
| ~ in_environment(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_4902,c_1769]) ).
tcf(c_5008,plain,
! [X0: $i] :
( greater(cardinality_at_time(first_movers,X0),iPr_def_20)
| ( iPr_def_12 = iPr_def_13 )
| ( cardinality_at_time(first_movers,X0) = iPr_def_20 )
| ~ in_environment(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_4920,c_70]) ).
tcf(c_5026,plain,
( greater(iPr_def_21,iPr_def_20)
| ( iPr_def_12 = iPr_def_13 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14)
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1762,c_4919]) ).
tcf(c_5076,plain,
( ( iPr_def_12 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1771,c_4915]) ).
tcf(c_5081,plain,
( ( iPr_def_12 = iPr_def_13 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero) ),
inference(global_subsumption_just,[status(thm)],[c_5076,c_4751,c_5076]) ).
tcf(c_5082,plain,
( ( iPr_def_12 = iPr_def_13 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(renaming,[status(thm)],[c_5081]) ).
tcf(c_5089,plain,
( ( iPr_def_12 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero) ),
inference(superposition,[status(thm)],[c_1770,c_5082]) ).
tcf(c_5093,plain,
( ( iPr_def_12 = iPr_def_13 )
| ~ greater(iPr_def_21,zero) ),
inference(global_subsumption_just,[status(thm)],[c_5089,c_4751,c_5089]) ).
tcf(c_5157,plain,
( ~ greater_or_equal(iPr_def_11,iPr_def_14)
| ( iPr_def_12 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_5026,c_2327,c_4751,c_5093]) ).
tcf(c_5158,plain,
( ( iPr_def_12 = iPr_def_13 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14) ),
inference(renaming,[status(thm)],[c_5157]) ).
tcf(c_5164,plain,
( ( iPr_def_12 = iPr_def_13 )
| ~ greater_or_equal(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_4433,c_5158]) ).
tcf(c_5167,plain,
iPr_def_12 = iPr_def_13,
inference(global_subsumption_just,[status(thm)],[c_5008,c_4749,c_5164]) ).
tcf(c_5182,plain,
( ( zero = iPr_def_20 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_11,iPr_def_12) ),
inference(demodulation,[status(thm)],[c_4035,c_5167]) ).
tcf(c_5187,plain,
( ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_11,iPr_def_12) ),
inference(demodulation,[status(thm)],[c_3185,c_5167]) ).
tcf(c_5190,plain,
( greater_or_equal(iPr_def_11,iPr_def_14)
| ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_2941,c_5167]) ).
tcf(c_5197,plain,
( greater_or_equal(iPr_def_17,iPr_def_14)
| ( iPr_def_12 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_2748,c_5167]) ).
tcf(c_5199,plain,
( greater_or_equal(iPr_def_11,iPr_def_12)
| ( iPr_def_11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_2728,c_5167]) ).
tcf(c_5209,plain,
greater_or_equal(iPr_def_17,iPr_def_12),
inference(demodulation,[status(thm)],[c_2431,c_5167]) ).
tcf(c_5215,plain,
greater(iPr_def_17,iPr_def_12),
inference(demodulation,[status(thm)],[c_1775,c_5167]) ).
tcf(c_5393,plain,
( in_environment(iPr_def_10,iPr_def_11)
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_5199,c_2283]) ).
tcf(c_5418,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_11 = iPr_def_17 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_5393,c_2589]) ).
tcf(c_5419,plain,
( greater_or_equal(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_17 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_5393,c_2559]) ).
tcf(c_5420,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_17 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_5393,c_2327]) ).
tcf(c_5454,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_5190,c_5420]) ).
tcf(c_5534,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_20,zero) ),
inference(superposition,[status(thm)],[c_5454,c_1780]) ).
tcf(c_5545,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ~ greater(iPr_def_20,zero) ),
inference(global_subsumption_just,[status(thm)],[c_5534,c_2522,c_3185,c_5393,c_5454]) ).
tcf(c_5553,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_5418,c_5545]) ).
tcf(c_5570,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_5553,c_1778]) ).
tcf(c_5680,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_5570,c_5454,c_5570]) ).
tcf(c_5681,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(renaming,[status(thm)],[c_5680]) ).
tcf(c_5690,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1771,c_5681]) ).
tcf(c_5695,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_5690,c_5393,c_5690]) ).
tcf(c_5703,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1770,c_5695]) ).
tcf(c_5707,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_5703,c_5393,c_5703]) ).
tcf(c_5714,plain,
( greater_or_equal(iPr_def_11,iPr_def_14)
| ( iPr_def_12 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_5707,c_5197]) ).
tcf(c_5717,plain,
( greater(iPr_def_11,iPr_def_12)
| ( iPr_def_12 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_5707,c_5215]) ).
tcf(c_5721,plain,
( in_environment(iPr_def_10,iPr_def_11)
| ( iPr_def_12 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_5707,c_1776]) ).
tcf(c_5747,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_12 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_5721,c_2589]) ).
tcf(c_5749,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_14 )
| ~ greater_or_equal(iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_5721,c_2327]) ).
tcf(c_5911,plain,
( ( zero = iPr_def_20 )
| ( iPr_def_12 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_5747,c_5182,c_5721,c_5717,c_5714,c_5749]) ).
tcf(c_5912,plain,
( ( iPr_def_12 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(renaming,[status(thm)],[c_5911]) ).
tcf(c_5923,plain,
( ( iPr_def_12 = iPr_def_14 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_5912,c_1778]) ).
tcf(c_6080,plain,
( ( iPr_def_12 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_5923,c_5714,c_5749,c_5923]) ).
tcf(c_6081,plain,
( ( iPr_def_12 = iPr_def_14 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(renaming,[status(thm)],[c_6080]) ).
tcf(c_6088,plain,
( ( iPr_def_12 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1771,c_6081]) ).
tcf(c_6098,plain,
( ( iPr_def_12 = iPr_def_14 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_6088,c_5721,c_6088]) ).
tcf(c_6104,plain,
( ( iPr_def_12 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1770,c_6098]) ).
tcf(c_6137,plain,
iPr_def_12 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_6104,c_5721,c_6104]) ).
tcf(c_6147,plain,
( greater_or_equal(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_17 )
| ~ greater_or_equal(iPr_def_11,iPr_def_12) ),
inference(demodulation,[status(thm)],[c_5419,c_6137]) ).
tcf(c_6150,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_17 )
| ~ greater_or_equal(iPr_def_11,iPr_def_12) ),
inference(demodulation,[status(thm)],[c_5420,c_6137]) ).
tcf(c_6154,plain,
( greater_or_equal(iPr_def_21,zero)
| ~ greater_or_equal(iPr_def_11,iPr_def_12)
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(demodulation,[status(thm)],[c_2559,c_6137]) ).
tcf(c_6158,plain,
( greater(iPr_def_21,zero)
| ~ greater_or_equal(iPr_def_11,iPr_def_12)
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(demodulation,[status(thm)],[c_2327,c_6137]) ).
tcf(c_6227,plain,
( greater_or_equal(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_6147,c_5199,c_5393,c_6154]) ).
tcf(c_6233,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_17 )
| ( zero = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_6227,c_70]) ).
tcf(c_6237,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_6150,c_5199,c_6150]) ).
tcf(c_6245,plain,
( ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_20,zero) ),
inference(superposition,[status(thm)],[c_6237,c_1780]) ).
tcf(c_6254,plain,
( ( iPr_def_11 = iPr_def_17 )
| ~ greater(iPr_def_20,zero) ),
inference(global_subsumption_just,[status(thm)],[c_6245,c_2522,c_3185,c_5199,c_5393,c_6150]) ).
tcf(c_6260,plain,
( ( iPr_def_11 = iPr_def_17 )
| ( zero = iPr_def_20 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5418,c_6254]) ).
tcf(c_6276,plain,
( ( iPr_def_11 = iPr_def_17 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_6260,c_1778]) ).
tcf(c_6341,plain,
( ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_6276,c_5199,c_6150,c_6276]) ).
tcf(c_6342,plain,
( ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(renaming,[status(thm)],[c_6341]) ).
tcf(c_6349,plain,
( ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1771,c_6342]) ).
tcf(c_6353,plain,
( ( iPr_def_11 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_6349,c_5393,c_6349]) ).
tcf(c_6359,plain,
( ( iPr_def_11 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1770,c_6353]) ).
tcf(c_6362,plain,
iPr_def_11 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_6359,c_5393,c_6359]) ).
tcf(c_6370,plain,
greater(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_5215,c_6362]) ).
tcf(c_6371,plain,
greater_or_equal(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_5209,c_6362]) ).
tcf(c_6375,plain,
in_environment(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_1776,c_6362]) ).
tcf(c_6381,plain,
greater_or_equal(iPr_def_20,zero),
inference(backward_subsumption_resolution,[status(thm)],[c_2324,c_6375]) ).
tcf(c_6394,plain,
greater(iPr_def_21,zero),
inference(global_subsumption_just,[status(thm)],[c_6233,c_6158,c_6375,c_6371]) ).
tcf(c_6396,plain,
( ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11)
| ( zero != iPr_def_20 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1778,c_6394]) ).
tcf(c_6425,plain,
( ~ subpopulation(first_movers,iPr_def_10,iPr_def_11)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_11) ),
inference(global_subsumption_just,[status(thm)],[c_6396,c_1778,c_3062,c_5187,c_6158,c_6381,c_6375,c_6371,c_6370]) ).
tcf(c_6431,plain,
( ~ in_environment(iPr_def_10,iPr_def_11)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1771,c_6425]) ).
tcf(c_6432,plain,
~ subpopulation(first_movers,iPr_def_10,iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_6431,c_6375]) ).
tcf(c_6437,plain,
~ in_environment(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_1770,c_6432]) ).
tcf(c_6438,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_6437,c_6375]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 01:12:18 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 2.24/1.20 % SZS status Started for theBenchmark.p
% 2.24/1.20 % SZS status Theorem for theBenchmark.p
% 2.24/1.20
% 2.24/1.20 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.24/1.20
% 2.24/1.20 % ------ iProver source info
% 2.24/1.20
% 2.24/1.20 % git: date: 2026-07-19 20:42:38 +0200
% 2.24/1.20 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.24/1.20 % git: non_committed_changes: false
% 2.24/1.20
% 2.24/1.20 % ------ Parsing...
% 2.24/1.20 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.24/1.20
% 2.24/1.20 % ------ Preprocessing... sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 7 0s sf_e pe_s pe_e %
% 2.24/1.20
% 2.24/1.20 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.24/1.20
% 2.24/1.20 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.24/1.20 % ------ Proving...
% 2.24/1.20 % ------ Problem Properties
% 2.24/1.20
% 2.24/1.20 %
% 2.24/1.20 % clauses 38
% 2.24/1.20 % conjectures 0
% 2.24/1.20 % EPR 19
% 2.24/1.20 % Horn 36
% 2.24/1.20 % unary 23
% 2.24/1.20 % binary 5
% 2.24/1.20 % lits 69
% 2.24/1.20 % lits eq 19
% 2.24/1.20 % fd_pure 0
% 2.24/1.20 % fd_pseudo 0
% 2.24/1.20 % fd_cond 0
% 2.24/1.20 % fd_pseudo_cond 1
% 2.24/1.20 % AC symbols 0
% 2.24/1.20
% 2.24/1.20 % ------ Schedule dynamic 5 is on
% 2.24/1.20
% 2.24/1.20 % ------ no conjectures: strip conj schedule
% 2.24/1.20
% 2.24/1.20 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 2.24/1.20
% 2.24/1.20
% 2.24/1.20 % ------
% 2.24/1.20 % Current options:
% 2.24/1.20 % ------
% 2.24/1.20
% 2.24/1.20
% 2.24/1.20 %
% 2.24/1.20
% 2.24/1.20 % ------ Proving...
% 2.24/1.20 %
% 2.24/1.20
% 2.24/1.20 % SZS status Theorem for theBenchmark.p
% 2.24/1.20
% 2.24/1.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.24/1.21
% 2.24/1.21
%------------------------------------------------------------------------------