%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : MGT035-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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:28 PM UTC 2026
% Result : Unsatisfiable 7.13s 6.77s
% Output : CNFRefutation 7.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 31
% Syntax : Number of formulae : 305 ( 24 unt; 0 def)
% Number of atoms : 1186 ( 395 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1558 ( 677 ~; 881 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 343 ( 0 sgn 343 !; 0 ?; 283 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_transitivity_22) ).
fof(f2,axiom,
! [X2,X0,X1] :
( greater(X1,X2)
| X2 = X1
| greater(X2,X1)
| ~ in_environment(X0,X2)
| ~ in_environment(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_times_in_environment_23) ).
fof(f3,plain,
! [X2,X0,X1] :
( greater(X1,X2)
| X1 = X2
| greater(X2,X1)
| ~ in_environment(X0,X2)
| ~ in_environment(X0,X1) ),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X0,X1] :
( X0 = X1
| greater(X0,X1)
| ~ greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_24) ).
fof(f5,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_25) ).
fof(f6,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
| X0 != X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_26) ).
fof(f7,axiom,
! [X2,X3,X0,X1] :
( outcompetes(X2,X1,X3)
| ~ greater(zero,growth_rate(X1,X3))
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_27) ).
fof(f10,axiom,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| growth_rate(first_movers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_30) ).
fof(f11,plain,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| zero = growth_rate(first_movers,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(reorient_equations,[],[f10]) ).
fof(f12,axiom,
! [X0,X1] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| growth_rate(first_movers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_31) ).
fof(f13,plain,
! [X0,X1] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| zero = growth_rate(first_movers,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(zero,growth_rate(efficient_producers,X1))
| growth_rate(first_movers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_32) ).
fof(f15,plain,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(zero,growth_rate(efficient_producers,X1))
| zero = growth_rate(first_movers,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(reorient_equations,[],[f14]) ).
fof(f16,axiom,
! [X0,X1] :
( greater(zero,growth_rate(first_movers,X1))
| greater(zero,growth_rate(efficient_producers,X1))
| growth_rate(first_movers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_33) ).
fof(f17,plain,
! [X0,X1] :
( greater(zero,growth_rate(first_movers,X1))
| greater(zero,growth_rate(efficient_producers,X1))
| zero = growth_rate(first_movers,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(reorient_equations,[],[f16]) ).
fof(f18,axiom,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| growth_rate(efficient_producers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_34) ).
fof(f19,plain,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| zero = growth_rate(efficient_producers,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,axiom,
! [X0,X1] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| growth_rate(efficient_producers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_35) ).
fof(f21,plain,
! [X0,X1] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| zero = growth_rate(efficient_producers,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,axiom,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(zero,growth_rate(efficient_producers,X1))
| growth_rate(efficient_producers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_36) ).
fof(f23,plain,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(zero,growth_rate(efficient_producers,X1))
| zero = growth_rate(efficient_producers,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,axiom,
! [X0,X1] :
( greater(zero,growth_rate(first_movers,X1))
| greater(zero,growth_rate(efficient_producers,X1))
| growth_rate(efficient_producers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_37) ).
fof(f25,plain,
! [X0,X1] :
( greater(zero,growth_rate(first_movers,X1))
| greater(zero,growth_rate(efficient_producers,X1))
| zero = growth_rate(efficient_producers,X1)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,axiom,
! [X0] :
( in_environment(X0,sk1(X0))
| ~ stable(X0)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_38) ).
fof(f27,axiom,
! [X0,X1] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ greater_or_equal(X1,sk1(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ stable(X0)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_39) ).
fof(f28,axiom,
! [X0] :
( in_environment(X0,sk2(X0))
| ~ stable(X0)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_40) ).
fof(f29,axiom,
! [X0] :
( greater_or_equal(sk2(X0),equilibrium(X0))
| ~ stable(X0)
| ~ environment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_41) ).
fof(f30,negated_conjecture,
environment(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_42) ).
fof(f31,negated_conjecture,
stable(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_43) ).
fof(f32,negated_conjecture,
! [X0] :
( subpopulations(first_movers,efficient_producers,sk3,sk4(X0))
| ~ in_environment(sk3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_44) ).
fof(f33,negated_conjecture,
! [X0] :
( greater_or_equal(sk4(X0),X0)
| ~ in_environment(sk3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_45) ).
fof(f34,negated_conjecture,
! [X0] :
( ~ outcompetes(efficient_producers,first_movers,sk4(X0))
| ~ in_environment(sk3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_46) ).
fof(f35,plain,
! [X1] : greater_or_equal(X1,X1),
inference(equality_resolution,[],[f6]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X2,X1)
| greater(X1,X2)
| ( X1 = X2 )
| ~ in_environment(X0,X2)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] :
( greater(X0,X1)
| ( X0 = X1 )
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_78,plain,
! [X0: $i] : greater_or_equal(X0,X0),
inference(cnf_transformation,[],[f35]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( outcompetes(X1,X0,X3)
| ~ environment(X2)
| ~ greater_or_equal(growth_rate(X1,X3),zero)
| ~ greater(zero,growth_rate(X0,X3))
| ~ subpopulations(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(growth_rate(efficient_producers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1))
| ( growth_rate(first_movers,X1) = zero )
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(growth_rate(efficient_producers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1))
| ( growth_rate(efficient_producers,X1) = zero )
| ~ environment(X0)
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_90,plain,
! [X0: $i] :
( in_environment(X0,sk1(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ stable(X0)
| ~ environment(X0)
| ~ greater_or_equal(X1,sk1(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_92,plain,
! [X0: $i] :
( in_environment(X0,sk2(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_93,plain,
! [X0: $i] :
( greater_or_equal(sk2(X0),equilibrium(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_94,negated_conjecture,
environment(sk3),
inference(cnf_transformation,[],[f30]) ).
tcf(c_95,negated_conjecture,
stable(sk3),
inference(cnf_transformation,[],[f31]) ).
tcf(c_96,negated_conjecture,
! [X0: $i] :
( subpopulations(first_movers,efficient_producers,sk3,sk4(X0))
| ~ in_environment(sk3,X0) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_97,negated_conjecture,
! [X0: $i] :
( greater_or_equal(sk4(X0),X0)
| ~ in_environment(sk3,X0) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_98,negated_conjecture,
! [X0: $i] :
( ~ in_environment(sk3,X0)
| ~ outcompetes(efficient_producers,first_movers,sk4(X0)) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_99,plain,
greater_or_equal(zero,zero),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_325,plain,
! [X0: $i] :
( greater_or_equal(sk2(X0),equilibrium(X0))
| ~ environment(X0)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_93,c_95]) ).
tcf(c_326,plain,
( greater_or_equal(sk2(sk3),equilibrium(sk3))
| ~ environment(sk3) ),
inference(unflattening,[status(thm)],[c_325]) ).
tcf(c_327,plain,
greater_or_equal(sk2(sk3),equilibrium(sk3)),
inference(global_subsumption_just,[status(thm)],[c_326,c_94,c_326]) ).
tcf(c_332,plain,
! [X0: $i] :
( in_environment(X0,sk2(X0))
| ~ environment(X0)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_92,c_95]) ).
tcf(c_333,plain,
( in_environment(sk3,sk2(sk3))
| ~ environment(sk3) ),
inference(unflattening,[status(thm)],[c_332]) ).
tcf(c_339,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ environment(X0)
| ~ greater_or_equal(X1,sk1(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_91,c_95]) ).
tcf(c_340,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ environment(sk3)
| ~ greater_or_equal(X0,sk1(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_339]) ).
tcf(c_342,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| ~ greater_or_equal(X0,sk1(sk3)) ),
inference(global_subsumption_just,[status(thm)],[c_340,c_94,c_340]) ).
tcf(c_343,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ greater_or_equal(X0,sk1(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(renaming,[status(thm)],[c_342]) ).
tcf(c_354,plain,
! [X0: $i] :
( in_environment(X0,sk1(X0))
| ~ environment(X0)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_90,c_95]) ).
tcf(c_355,plain,
( in_environment(sk3,sk1(sk3))
| ~ environment(sk3) ),
inference(unflattening,[status(thm)],[c_354]) ).
tcf(c_356,plain,
in_environment(sk3,sk1(sk3)),
inference(global_subsumption_just,[status(thm)],[c_355,c_94,c_355]) ).
tcf(c_371,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ environment(X4)
| ~ in_environment(sk3,X2)
| ~ greater_or_equal(growth_rate(X1,X3),zero)
| ~ greater(zero,growth_rate(X0,X3))
| ~ subpopulations(X0,X1,X4,X3)
| ( X1 != efficient_producers )
| ( X0 != first_movers )
| ( sk4(X2) != X3 ) ),
inference(resolution_lifted,[status(thm)],[c_79,c_98]) ).
tcf(c_372,plain,
! [X0: $i,X1: $i] :
( ~ environment(X0)
| ~ in_environment(sk3,X1)
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(X1)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X1)))
| ~ subpopulations(first_movers,efficient_producers,X0,sk4(X1)) ),
inference(unflattening,[status(thm)],[c_371]) ).
tcf(c_394,plain,
! [X0: $i,X1: $i] :
( ~ in_environment(sk3,X1)
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(X1)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X1)))
| ~ subpopulations(first_movers,efficient_producers,X0,sk4(X1))
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_372,c_94]) ).
tcf(c_395,plain,
! [X0: $i] :
( ~ in_environment(sk3,X0)
| ~ subpopulations(first_movers,efficient_producers,sk3,sk4(X0))
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X0))) ),
inference(unflattening,[status(thm)],[c_394]) ).
tcf(c_397,plain,
! [X0: $i] :
( ~ in_environment(sk3,X0)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_395,c_96,c_395]) ).
tcf(c_398,plain,
! [X0: $i] :
( ~ in_environment(sk3,X0)
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(X0))) ),
inference(renaming,[status(thm)],[c_397]) ).
tcf(c_409,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1))
| ( growth_rate(efficient_producers,X1) = zero )
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_89,c_94]) ).
tcf(c_410,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,X0))
| greater(zero,growth_rate(first_movers,X0))
| ( growth_rate(efficient_producers,X0) = zero )
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_409]) ).
tcf(c_427,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(growth_rate(efficient_producers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_88,c_94]) ).
tcf(c_428,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,X0))
| greater(growth_rate(efficient_producers,X0),zero)
| ( growth_rate(efficient_producers,X0) = zero )
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_427]) ).
tcf(c_445,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_87,c_94]) ).
tcf(c_446,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,X0))
| greater(growth_rate(first_movers,X0),zero)
| ( growth_rate(efficient_producers,X0) = zero )
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_445]) ).
tcf(c_463,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_86,c_94]) ).
tcf(c_464,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),zero)
| greater(growth_rate(first_movers,X0),zero)
| ( growth_rate(efficient_producers,X0) = zero )
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_463]) ).
tcf(c_481,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1))
| ( growth_rate(first_movers,X1) = zero )
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_85,c_94]) ).
tcf(c_482,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,X0))
| greater(zero,growth_rate(first_movers,X0))
| ( growth_rate(first_movers,X0) = zero )
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_481]) ).
tcf(c_499,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(growth_rate(efficient_producers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_84,c_94]) ).
tcf(c_500,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,X0))
| greater(growth_rate(efficient_producers,X0),zero)
| ( growth_rate(first_movers,X0) = zero )
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_499]) ).
tcf(c_517,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_83,c_94]) ).
tcf(c_518,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,X0))
| greater(growth_rate(first_movers,X0),zero)
| ( growth_rate(first_movers,X0) = zero )
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_517]) ).
tcf(c_535,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_82,c_94]) ).
tcf(c_536,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),zero)
| greater(growth_rate(first_movers,X0),zero)
| ( growth_rate(first_movers,X0) = zero )
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(unflattening,[status(thm)],[c_535]) ).
tcf(c_596,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,equilibrium(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_536]) ).
tcf(c_597,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sk4(X0)),zero)
| greater(growth_rate(first_movers,sk4(X0)),zero)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(unflattening,[status(thm)],[c_596]) ).
tcf(c_614,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,equilibrium(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_518]) ).
tcf(c_615,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sk4(X0)))
| greater(growth_rate(first_movers,sk4(X0)),zero)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(unflattening,[status(thm)],[c_614]) ).
tcf(c_632,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(growth_rate(efficient_producers,X1),zero)
| ( growth_rate(first_movers,X1) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,equilibrium(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_500]) ).
tcf(c_633,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| greater(growth_rate(efficient_producers,sk4(X0)),zero)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(unflattening,[status(thm)],[c_632]) ).
tcf(c_650,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1))
| ( growth_rate(first_movers,X1) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,equilibrium(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_482]) ).
tcf(c_651,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| greater(zero,growth_rate(first_movers,sk4(X0)))
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(unflattening,[status(thm)],[c_650]) ).
tcf(c_668,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,equilibrium(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_464]) ).
tcf(c_669,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sk4(X0)),zero)
| greater(growth_rate(first_movers,sk4(X0)),zero)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(unflattening,[status(thm)],[c_668]) ).
tcf(c_686,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,equilibrium(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_446]) ).
tcf(c_687,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sk4(X0)))
| greater(growth_rate(first_movers,sk4(X0)),zero)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(unflattening,[status(thm)],[c_686]) ).
tcf(c_704,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(growth_rate(efficient_producers,X1),zero)
| ( growth_rate(efficient_producers,X1) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,equilibrium(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_428]) ).
tcf(c_705,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| greater(growth_rate(efficient_producers,sk4(X0)),zero)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(unflattening,[status(thm)],[c_704]) ).
tcf(c_722,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(efficient_producers,X1))
| greater(zero,growth_rate(first_movers,X1))
| ( growth_rate(efficient_producers,X1) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,equilibrium(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_410]) ).
tcf(c_723,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| greater(zero,growth_rate(first_movers,sk4(X0)))
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(unflattening,[status(thm)],[c_722]) ).
tcf(c_740,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(X1,sk1(sk3))
| ( sk3 != sk3 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sk4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_343]) ).
tcf(c_741,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sk4(X0)),growth_rate(first_movers,sk4(X0)))
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3)) ),
inference(unflattening,[status(thm)],[c_740]) ).
tcf(c_819,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ in_environment(sk3,X0)
| ~ greater(X1,X2)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| ( X2 != zero )
| ( growth_rate(efficient_producers,sk4(X0)) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_77,c_398]) ).
tcf(c_820,plain,
! [X0: $i] :
( ~ in_environment(sk3,X0)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| ~ greater(growth_rate(efficient_producers,sk4(X0)),zero) ),
inference(unflattening,[status(thm)],[c_819]) ).
tcf(c_1185,plain,
! [X0: $i,X1: $i] :
( ~ in_environment(sk3,X0)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| ( X1 != zero )
| ( growth_rate(efficient_producers,sk4(X0)) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_78,c_398]) ).
tcf(c_1186,plain,
! [X0: $i] :
( ~ in_environment(sk3,X0)
| ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| ( growth_rate(efficient_producers,sk4(X0)) != zero ) ),
inference(unflattening,[status(thm)],[c_1185]) ).
tcf(c_1581,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(efficient_producers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_723,c_705,c_723,c_820]) ).
tcf(c_1582,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_1581]) ).
tcf(c_1584,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(efficient_producers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_705,c_705,c_723,c_820]) ).
tcf(c_1585,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_1584]) ).
tcf(c_1586,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| greater(growth_rate(first_movers,sk4(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_687,c_669,c_687,c_820]) ).
tcf(c_1587,plain,
! [X0: $i] :
( greater(growth_rate(first_movers,sk4(X0)),zero)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_1586]) ).
tcf(c_1589,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| greater(growth_rate(first_movers,sk4(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_669,c_1587]) ).
tcf(c_1590,plain,
! [X0: $i] :
( greater(growth_rate(first_movers,sk4(X0)),zero)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_1589]) ).
tcf(c_1591,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(first_movers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_651,c_651,c_1186,c_1582]) ).
tcf(c_1592,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_1591]) ).
tcf(c_1594,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(first_movers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_633,c_1592]) ).
tcf(c_1595,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sk4(X0)))
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_1594]) ).
tcf(c_1596,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| greater(growth_rate(first_movers,sk4(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_615,c_597,c_615,c_820]) ).
tcf(c_1597,plain,
! [X0: $i] :
( greater(growth_rate(first_movers,sk4(X0)),zero)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_1596]) ).
tcf(c_1599,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| greater(growth_rate(first_movers,sk4(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_597,c_1597]) ).
tcf(c_1600,plain,
! [X0: $i] :
( greater(growth_rate(first_movers,sk4(X0)),zero)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_1599]) ).
tcf(c_2721,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_2723,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2724,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( greater(X0,X2)
| ~ greater(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2725,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in_environment(X0,X2)
| ~ in_environment(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2726,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( greater_or_equal(X0,X2)
| ~ greater_or_equal(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2727,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( growth_rate(X0,X2) = growth_rate(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2729,plain,
! [X0: $i,X1: $i] :
( ( sk1(X0) = sk1(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2730,plain,
! [X0: $i,X1: $i] :
( ( sk2(X0) = sk2(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2735,plain,
zero = zero,
inference(instantiation,[status(thm)],[c_2721]) ).
tcf(c_3007,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ in_environment(sk3,sk2(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3)) ),
inference(instantiation,[status(thm)],[c_741]) ).
tcf(c_3008,plain,
( ~ in_environment(sk3,sk2(sk3))
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_3009,plain,
( greater_or_equal(sk4(sk2(sk3)),sk2(sk3))
| ~ in_environment(sk3,sk2(sk3)) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_3016,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ~ in_environment(sk3,sk1(sk3))
| ~ greater_or_equal(sk4(sk1(sk3)),sk1(sk3)) ),
inference(instantiation,[status(thm)],[c_741]) ).
tcf(c_3017,plain,
( ~ in_environment(sk3,sk1(sk3))
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_3018,plain,
( greater_or_equal(sk4(sk1(sk3)),sk1(sk3))
| ~ in_environment(sk3,sk1(sk3)) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_3029,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ greater_or_equal(X0,X1)
| ( equilibrium(sk3) != X1 )
| ( sk4(sk2(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_3038,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ greater_or_equal(X0,X1)
| ( sk1(sk3) != X1 )
| ( sk4(sk2(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_3040,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_3041,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ greater_or_equal(X0,X1)
| ( zero != X1 )
| ( growth_rate(efficient_producers,sk4(sk2(sk3))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_3042,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ greater_or_equal(zero,zero)
| ( zero != zero )
| ( growth_rate(efficient_producers,sk4(sk2(sk3))) != zero ) ),
inference(instantiation,[status(thm)],[c_3041]) ).
tcf(c_3043,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_3044,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater_or_equal(X0,X1)
| ( equilibrium(sk3) != X1 )
| ( sk4(sk1(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_3053,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ greater_or_equal(X0,X1)
| ( zero != X1 )
| ( growth_rate(efficient_producers,sk4(sk1(sk3))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_3055,plain,
sk3 = sk3,
inference(instantiation,[status(thm)],[c_2721]) ).
tcf(c_3059,plain,
! [X0: $i] :
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),X0)
| ( equilibrium(sk3) != X0 )
| ( sk4(sk2(sk3)) != sk4(sk2(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3029]) ).
tcf(c_3062,plain,
! [X0: $i] :
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),X0)
| ( sk1(sk3) != X0 )
| ( sk4(sk2(sk3)) != sk4(sk2(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3038]) ).
tcf(c_3075,plain,
! [X0: $i] :
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater_or_equal(sk4(sk1(sk3)),X0)
| ( equilibrium(sk3) != X0 )
| ( sk4(sk1(sk3)) != sk4(sk1(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3044]) ).
tcf(c_3078,plain,
! [X0: $i] :
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| ( zero != X0 )
| ( growth_rate(efficient_producers,sk4(sk1(sk3))) != growth_rate(efficient_producers,sk4(sk1(sk3))) ) ),
inference(instantiation,[status(thm)],[c_3053]) ).
tcf(c_3085,plain,
! [X0: $i,X1: $i] :
( greater(zero,X1)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ greater(growth_rate(efficient_producers,sk4(X0)),X1) ),
inference(superposition,[status(thm)],[c_1585,c_74]) ).
tcf(c_3086,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,sk4(X0)),X1)
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater(growth_rate(first_movers,sk4(X0)),X1) ),
inference(superposition,[status(thm)],[c_741,c_74]) ).
tcf(c_3103,plain,
! [X0: $i] :
( greater(sk4(X0),X0)
| ( sk4(X0) = X0 )
| ~ in_environment(sk3,X0) ),
inference(superposition,[status(thm)],[c_97,c_76]) ).
tcf(c_3105,plain,
( greater(sk2(sk3),equilibrium(sk3))
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(superposition,[status(thm)],[c_327,c_76]) ).
tcf(c_3114,plain,
! [X0: $i] :
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater(X0,equilibrium(sk3))
| ~ greater(sk4(sk1(sk3)),X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_3119,plain,
! [X0: $i] :
( greater(sk2(sk3),X0)
| ( equilibrium(sk3) = sk2(sk3) )
| ~ greater(equilibrium(sk3),X0) ),
inference(superposition,[status(thm)],[c_3105,c_74]) ).
tcf(c_3122,plain,
! [X0: $i,X1: $i] :
( greater(sk4(X0),X1)
| ( sk4(X0) = X0 )
| ~ in_environment(sk3,X0)
| ~ greater(X0,X1) ),
inference(superposition,[status(thm)],[c_3103,c_74]) ).
tcf(c_3132,plain,
! [X0: $i,X1: $i] :
( greater(zero,X1)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ greater(growth_rate(efficient_producers,sk4(X0)),X1) ),
inference(superposition,[status(thm)],[c_1595,c_74]) ).
tcf(c_3136,plain,
sk4(sk2(sk3)) = sk4(sk2(sk3)),
inference(instantiation,[status(thm)],[c_2721]) ).
tcf(c_3158,plain,
sk4(sk1(sk3)) = sk4(sk1(sk3)),
inference(instantiation,[status(thm)],[c_2721]) ).
tcf(c_3163,plain,
! [X0: $i] :
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_3166,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(sk4(X0),X2)
| ( sk4(X0) = X0 )
| ~ in_environment(sk3,X0)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(superposition,[status(thm)],[c_3122,c_74]) ).
tcf(c_3167,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sk4(X0),X1)
| ( sk4(X0) = X0 )
| ~ in_environment(sk3,X0)
| ~ greater(X0,X1) ),
inference(superposition,[status(thm)],[c_3122,c_77]) ).
tcf(c_3175,plain,
! [X0: $i,X1: $i] :
( ( growth_rate(efficient_producers,sk4(sk1(sk3))) = growth_rate(X1,X0) )
| ( efficient_producers != X1 )
| ( sk4(sk1(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2727]) ).
tcf(c_3188,plain,
( greater(sk2(sk3),equilibrium(sk3))
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(superposition,[status(thm)],[c_327,c_76]) ).
tcf(c_3222,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sk4(X0)),zero)
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_1600,c_3086]) ).
tcf(c_3223,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sk4(X0)),zero)
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_1590,c_3086]) ).
tcf(c_3235,plain,
! [X0: $i] :
( greater(X0,sk1(sk3))
| greater(sk1(sk3),X0)
| ( sk1(sk3) = X0 )
| ~ in_environment(sk3,X0) ),
inference(superposition,[status(thm)],[c_356,c_75]) ).
tcf(c_3243,plain,
! [X0: $i] :
( greater(X0,sk1(sk3))
| greater(sk1(sk3),X0)
| ( X0 = sk1(sk3) )
| ~ in_environment(sk3,X0)
| ~ in_environment(sk3,sk1(sk3)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_3258,plain,
! [X0: $i,X1: $i] :
( greater(X0,X1)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ( X1 != growth_rate(first_movers,sk4(sk1(sk3))) )
| ( X0 != growth_rate(efficient_producers,sk4(sk1(sk3))) ) ),
inference(instantiation,[status(thm)],[c_2724]) ).
tcf(c_3267,plain,
! [X0: $i] :
( greater(sk4(sk1(sk3)),X0)
| ( sk4(sk1(sk3)) = X0 )
| ~ greater_or_equal(sk4(sk1(sk3)),X0) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_3275,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater_or_equal(sk4(sk1(sk3)),X1)
| ~ greater_or_equal(X0,X2)
| ( X1 != X2 )
| ( sk4(sk1(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_3277,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater_or_equal(sk4(sk1(sk3)),sk1(sk3))
| ( equilibrium(sk3) != sk1(sk3) )
| ( sk4(sk1(sk3)) != sk4(sk1(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3075]) ).
tcf(c_3283,plain,
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),sk2(sk3))
| ( equilibrium(sk3) != sk2(sk3) )
| ( sk4(sk2(sk3)) != sk4(sk2(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3059]) ).
tcf(c_3287,plain,
( greater(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| ( equilibrium(sk3) = sk2(sk3) )
| ( equilibrium(sk3) = sk1(sk3) )
| ~ in_environment(sk3,equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_3235,c_3119]) ).
tcf(c_3288,plain,
! [X0: $i,X1: $i] :
( greater(X0,sk1(sk3))
| greater(sk1(sk3),X1)
| ( sk1(sk3) = X0 )
| ~ in_environment(sk3,X0)
| ~ greater(X0,X1) ),
inference(superposition,[status(thm)],[c_3235,c_74]) ).
tcf(c_3289,plain,
! [X0: $i] :
( greater_or_equal(sk1(sk3),X0)
| greater(X0,sk1(sk3))
| ( sk1(sk3) = X0 )
| ~ in_environment(sk3,X0) ),
inference(superposition,[status(thm)],[c_3235,c_77]) ).
tcf(c_3298,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),sk2(sk3))
| ( sk1(sk3) != sk2(sk3) )
| ( sk4(sk2(sk3)) != sk4(sk2(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3062]) ).
tcf(c_3430,plain,
! [X0: $i,X1: $i] :
( ( X1 = growth_rate(efficient_producers,sk4(sk2(sk3))) )
| ( X1 != X0 )
| ( growth_rate(efficient_producers,sk4(sk2(sk3))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2723]) ).
tcf(c_3431,plain,
( ( zero = growth_rate(efficient_producers,sk4(sk2(sk3))) )
| ( zero != zero )
| ( growth_rate(efficient_producers,sk4(sk2(sk3))) != zero ) ),
inference(instantiation,[status(thm)],[c_3430]) ).
tcf(c_3447,plain,
! [X0: $i] :
( greater(sk4(sk2(sk3)),X0)
| ( equilibrium(sk3) = sk2(sk3) )
| ( sk4(sk2(sk3)) = sk2(sk3) )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater(equilibrium(sk3),X0) ),
inference(superposition,[status(thm)],[c_3188,c_3166]) ).
tcf(c_3472,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(instantiation,[status(thm)],[c_3163]) ).
tcf(c_3487,plain,
! [X0: $i] :
( ( growth_rate(efficient_producers,sk4(sk1(sk3))) = growth_rate(efficient_producers,X0) )
| ( efficient_producers != efficient_producers )
| ( sk4(sk1(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_3175]) ).
tcf(c_3529,plain,
! [X0: $i] :
( greater(X0,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ( X0 != growth_rate(efficient_producers,sk4(sk1(sk3))) )
| ( growth_rate(first_movers,sk4(sk1(sk3))) != growth_rate(first_movers,sk4(sk1(sk3))) ) ),
inference(instantiation,[status(thm)],[c_3258]) ).
tcf(c_3530,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ( zero != growth_rate(efficient_producers,sk4(sk1(sk3))) )
| ( growth_rate(first_movers,sk4(sk1(sk3))) != growth_rate(first_movers,sk4(sk1(sk3))) ) ),
inference(instantiation,[status(thm)],[c_3529]) ).
tcf(c_3551,plain,
( greater(sk2(sk3),equilibrium(sk3))
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(superposition,[status(thm)],[c_327,c_76]) ).
tcf(c_3581,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sk4(sk1(sk3)),X0)
| ~ greater_or_equal(sk4(sk1(sk3)),X1)
| ( X0 != X1 )
| ( sk4(sk1(sk3)) != sk4(sk1(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3275]) ).
tcf(c_3632,plain,
! [X0: $i] :
( ( sk2(X0) = sk2(sk3) )
| ( X0 != sk3 ) ),
inference(instantiation,[status(thm)],[c_2730]) ).
tcf(c_3643,plain,
! [X0: $i] :
( ( sk1(X0) = sk1(sk3) )
| ( X0 != sk3 ) ),
inference(instantiation,[status(thm)],[c_2729]) ).
tcf(c_3826,plain,
( greater(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| ( sk1(sk3) = sk2(sk3) )
| ( equilibrium(sk3) = sk2(sk3) )
| ~ in_environment(sk3,sk2(sk3)) ),
inference(superposition,[status(thm)],[c_3551,c_3288]) ).
tcf(c_3843,plain,
efficient_producers = efficient_producers,
inference(instantiation,[status(thm)],[c_2721]) ).
tcf(c_3871,plain,
( ( growth_rate(efficient_producers,sk4(sk1(sk3))) = growth_rate(efficient_producers,sk4(sk1(sk3))) )
| ( efficient_producers != efficient_producers )
| ( sk4(sk1(sk3)) != sk4(sk1(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3487]) ).
tcf(c_3911,plain,
! [X0: $i] :
( greater_or_equal(sk4(sk1(sk3)),X0)
| ~ greater_or_equal(sk4(sk1(sk3)),sk1(sk3))
| ( X0 != sk1(sk3) )
| ( sk4(sk1(sk3)) != sk4(sk1(sk3)) ) ),
inference(instantiation,[status(thm)],[c_3581]) ).
tcf(c_3987,plain,
( ( sk2(sk3) = sk2(sk3) )
| ( sk3 != sk3 ) ),
inference(instantiation,[status(thm)],[c_3632]) ).
tcf(c_4000,plain,
! [X0: $i] :
( greater_or_equal(sk1(sk3),X0)
| ~ greater(sk1(sk3),X0) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_4043,plain,
( ( sk1(sk3) = sk1(sk3) )
| ( sk3 != sk3 ) ),
inference(instantiation,[status(thm)],[c_3643]) ).
tcf(c_4046,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sk4(X0)))
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_741,c_3085]) ).
tcf(c_4085,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ( zero != growth_rate(first_movers,sk4(sk1(sk3))) )
| ( growth_rate(efficient_producers,sk4(sk1(sk3))) != growth_rate(efficient_producers,sk4(sk1(sk3))) ) ),
inference(instantiation,[status(thm)],[c_3078]) ).
tcf(c_4091,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sk4(X0)))
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_741,c_3132]) ).
tcf(c_4120,plain,
greater_or_equal(sk1(sk3),sk1(sk3)),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_4488,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(instantiation,[status(thm)],[c_3223]) ).
tcf(c_4497,plain,
! [X0: $i] :
( greater(zero,X0)
| ( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0) ),
inference(instantiation,[status(thm)],[c_3085]) ).
tcf(c_4514,plain,
! [X0: $i,X1: $i] :
( in_environment(X0,X1)
| ~ in_environment(sk3,sk2(sk3))
| ( X1 != sk2(sk3) )
| ( X0 != sk3 ) ),
inference(instantiation,[status(thm)],[c_2725]) ).
tcf(c_4539,plain,
! [X0: $i] :
( greater(zero,X0)
| ( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero )
| ~ in_environment(sk3,sk1(sk3))
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0) ),
inference(instantiation,[status(thm)],[c_3085]) ).
tcf(c_4560,plain,
! [X0: $i] :
( in_environment(sk3,X0)
| ~ in_environment(sk3,sk2(sk3))
| ( sk3 != sk3 )
| ( X0 != sk2(sk3) ) ),
inference(instantiation,[status(thm)],[c_4514]) ).
tcf(c_4576,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ( sk4(sk2(sk3)) = sk2(sk3) )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater(sk2(sk3),sk1(sk3)) ),
inference(instantiation,[status(thm)],[c_3167]) ).
tcf(c_4586,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ greater_or_equal(X0,X1)
| ( sk1(sk3) != X1 )
| ( sk4(sk2(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_4590,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ greater_or_equal(X0,X1)
| ( equilibrium(sk3) != X1 )
| ( sk4(sk2(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_4632,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero )
| ~ in_environment(sk3,sk1(sk3))
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(instantiation,[status(thm)],[c_4539]) ).
tcf(c_4679,plain,
! [X0: $i,X1: $i] :
( greater(X1,sk1(sk3))
| greater(sk1(sk3),X1)
| ( X1 = sk1(sk3) )
| ~ in_environment(X0,X1)
| ~ in_environment(X0,sk1(sk3)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_4707,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X0,X2)
| ~ greater(X1,sk1(sk3))
| ( X2 != sk1(sk3) )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_2724]) ).
tcf(c_4751,plain,
! [X0: $i] :
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ greater_or_equal(X0,sk1(sk3))
| ( sk1(sk3) != sk1(sk3) )
| ( sk4(sk2(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_4586]) ).
tcf(c_4758,plain,
! [X0: $i] :
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ greater_or_equal(X0,equilibrium(sk3))
| ( equilibrium(sk3) != equilibrium(sk3) )
| ( sk4(sk2(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_4590]) ).
tcf(c_4775,plain,
! [X0: $i,X1: $i] :
( ( X1 = growth_rate(first_movers,sk4(sk1(sk3))) )
| ( X1 != X0 )
| ( growth_rate(first_movers,sk4(sk1(sk3))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2723]) ).
tcf(c_4776,plain,
( ( zero = growth_rate(first_movers,sk4(sk1(sk3))) )
| ( zero != zero )
| ( growth_rate(first_movers,sk4(sk1(sk3))) != zero ) ),
inference(instantiation,[status(thm)],[c_4775]) ).
tcf(c_4825,plain,
! [X0: $i,X1: $i] :
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater(X1,X0)
| ( zero != X1 )
| ( growth_rate(first_movers,sk4(sk2(sk3))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2724]) ).
tcf(c_4830,plain,
! [X0: $i,X1: $i] :
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater(X0,X1)
| ( equilibrium(sk3) != X1 )
| ( sk4(sk1(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2724]) ).
tcf(c_4849,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(instantiation,[status(thm)],[c_4497]) ).
tcf(c_4942,plain,
! [X0: $i,X1: $i] :
( greater(sk1(sk3),X1)
| ~ greater(X0,X1)
| ~ greater(sk1(sk3),X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_4950,plain,
! [X0: $i,X1: $i] :
( ( sk2(sk3) = X1 )
| ( X1 != X0 )
| ( sk2(sk3) != X0 ) ),
inference(instantiation,[status(thm)],[c_2723]) ).
tcf(c_4959,plain,
! [X0: $i] :
( greater(X0,sk1(sk3))
| greater(sk1(sk3),X0)
| ( X0 = sk1(sk3) )
| ~ in_environment(sk3,X0)
| ~ in_environment(sk3,sk1(sk3)) ),
inference(instantiation,[status(thm)],[c_4679]) ).
tcf(c_5016,plain,
! [X0: $i,X1: $i] :
( greater(X0,sk1(sk3))
| ~ greater(X1,sk1(sk3))
| ( X0 != X1 )
| ( sk1(sk3) != sk1(sk3) ) ),
inference(instantiation,[status(thm)],[c_4707]) ).
tcf(c_5052,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater_or_equal(sk1(sk3),X1)
| ~ greater_or_equal(X0,X2)
| ( X1 != X2 )
| ( sk1(sk3) != X0 ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_5074,plain,
! [X0: $i,X1: $i] :
( ( sk4(sk2(sk3)) = X1 )
| ( X1 != X0 )
| ( sk4(sk2(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2723]) ).
tcf(c_5077,plain,
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| ( equilibrium(sk3) != equilibrium(sk3) )
| ( sk4(sk2(sk3)) != sk2(sk3) ) ),
inference(instantiation,[status(thm)],[c_4758]) ).
tcf(c_5094,plain,
! [X0: $i] :
( greater(sk4(sk2(sk3)),X0)
| ( equilibrium(sk3) = sk2(sk3) )
| ( sk4(sk2(sk3)) = sk2(sk3) )
| ~ greater(equilibrium(sk3),X0) ),
inference(global_subsumption_just,[status(thm)],[c_3447,c_94,c_333,c_3447]) ).
tcf(c_5101,plain,
! [X0: $i] :
( greater_or_equal(sk4(sk2(sk3)),X0)
| ( equilibrium(sk3) = sk2(sk3) )
| ( sk4(sk2(sk3)) = sk2(sk3) )
| ~ greater(equilibrium(sk3),X0) ),
inference(superposition,[status(thm)],[c_5094,c_77]) ).
tcf(c_5127,plain,
growth_rate(first_movers,sk4(sk1(sk3))) = growth_rate(first_movers,sk4(sk1(sk3))),
inference(instantiation,[status(thm)],[c_2721]) ).
tcf(c_5376,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater(X0,growth_rate(first_movers,sk4(sk2(sk3))))
| ( zero != X0 )
| ( growth_rate(first_movers,sk4(sk2(sk3))) != growth_rate(first_movers,sk4(sk2(sk3))) ) ),
inference(instantiation,[status(thm)],[c_4825]) ).
tcf(c_5407,plain,
! [X0: $i] :
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater(X0,equilibrium(sk3))
| ( equilibrium(sk3) != equilibrium(sk3) )
| ( sk4(sk1(sk3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_4830]) ).
tcf(c_5474,plain,
! [X0: $i] :
( greater(X0,sk1(sk3))
| greater(sk1(sk3),X0)
| ( X0 = sk1(sk3) )
| ~ in_environment(sk3,X0) ),
inference(resolution,[status(thm)],[c_75,c_356]) ).
tcf(c_5514,plain,
( in_environment(sk3,equilibrium(sk3))
| ~ in_environment(sk3,sk2(sk3))
| ( sk3 != sk3 )
| ( equilibrium(sk3) != sk2(sk3) ) ),
inference(instantiation,[status(thm)],[c_4560]) ).
tcf(c_6049,plain,
! [X0: $i,X1: $i] :
( ( X1 = growth_rate(efficient_producers,sk4(sk1(sk3))) )
| ( X1 != X0 )
| ( growth_rate(efficient_producers,sk4(sk1(sk3))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2723]) ).
tcf(c_6050,plain,
( ( zero = growth_rate(efficient_producers,sk4(sk1(sk3))) )
| ( zero != zero )
| ( growth_rate(efficient_producers,sk4(sk1(sk3))) != zero ) ),
inference(instantiation,[status(thm)],[c_6049]) ).
tcf(c_6089,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(first_movers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3222,c_820,c_3222,c_4091]) ).
tcf(c_6090,plain,
! [X0: $i] :
( ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_6089]) ).
tcf(c_6092,plain,
( ( growth_rate(first_movers,sk4(sk1(sk3))) = zero )
| ~ in_environment(sk3,sk1(sk3))
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_97,c_6090]) ).
tcf(c_6121,plain,
~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)),
inference(global_subsumption_just,[status(thm)],[c_6092,c_94,c_355,c_2735,c_3018,c_3017,c_3016,c_3158,c_3472,c_3530,c_3843,c_3871,c_4085,c_4632,c_4776,c_5127,c_6050,c_6092]) ).
tcf(c_6123,plain,
( ( sk4(sk1(sk3)) = sk1(sk3) )
| ~ in_environment(sk3,sk1(sk3))
| ~ greater(sk1(sk3),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_3167,c_6121]) ).
tcf(c_6194,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(efficient_producers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3223,c_820,c_3223,c_4046]) ).
tcf(c_6195,plain,
! [X0: $i] :
( ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_6194]) ).
tcf(c_6371,plain,
! [X0: $i] :
( greater(sk1(sk3),equilibrium(sk3))
| ~ greater(X0,equilibrium(sk3))
| ~ greater(sk1(sk3),X0) ),
inference(instantiation,[status(thm)],[c_4942]) ).
tcf(c_6507,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(equilibrium(sk3),sk1(sk3))
| ( equilibrium(sk3) = sk1(sk3) )
| ~ in_environment(sk3,sk1(sk3))
| ~ in_environment(sk3,equilibrium(sk3)) ),
inference(instantiation,[status(thm)],[c_4959]) ).
tcf(c_6780,plain,
! [X0: $i] :
( ( sk4(sk2(sk3)) = X0 )
| ( X0 != sk2(sk3) )
| ( sk4(sk2(sk3)) != sk2(sk3) ) ),
inference(instantiation,[status(thm)],[c_5074]) ).
tcf(c_6820,plain,
equilibrium(sk3) = equilibrium(sk3),
inference(instantiation,[status(thm)],[c_2721]) ).
tcf(c_7053,plain,
! [X0: $i] :
( greater(sk2(sk3),sk1(sk3))
| ~ greater(X0,sk1(sk3))
| ( sk2(sk3) != X0 )
| ( sk1(sk3) != sk1(sk3) ) ),
inference(instantiation,[status(thm)],[c_5016]) ).
tcf(c_7260,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sk1(sk3),X0)
| ~ greater_or_equal(sk1(sk3),X1)
| ( X0 != X1 )
| ( sk1(sk3) != sk1(sk3) ) ),
inference(instantiation,[status(thm)],[c_5052]) ).
tcf(c_7279,plain,
! [X0: $i] :
( ( sk2(sk3) = X0 )
| ( X0 != sk2(sk3) )
| ( sk2(sk3) != sk2(sk3) ) ),
inference(instantiation,[status(thm)],[c_4950]) ).
tcf(c_7377,plain,
( greater(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| ( equilibrium(sk3) = sk2(sk3) )
| ~ in_environment(sk3,equilibrium(sk3)) ),
inference(global_subsumption_just,[status(thm)],[c_3287,c_94,c_355,c_2735,c_3018,c_3017,c_3016,c_3158,c_3277,c_3287,c_3472,c_3530,c_3843,c_3871,c_4085,c_4632,c_4776,c_5127,c_6050,c_6092]) ).
tcf(c_7380,plain,
( greater_or_equal(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| ( equilibrium(sk3) = sk2(sk3) )
| ~ in_environment(sk3,equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_7377,c_77]) ).
tcf(c_7488,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(efficient_producers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3223,c_820,c_3223,c_4046]) ).
tcf(c_7489,plain,
! [X0: $i] :
( ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_7488]) ).
tcf(c_7492,plain,
! [X0: $i] :
( ( sk4(X0) = X0 )
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater(X0,sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_3167,c_7489]) ).
tcf(c_7531,plain,
! [X0: $i] :
( ( sk4(X0) = X0 )
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater(X0,sk1(sk3))
| ~ greater(X0,equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_3167,c_7492]) ).
tcf(c_7603,plain,
( greater(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| ( sk1(sk3) = sk2(sk3) )
| ( equilibrium(sk3) = sk2(sk3) )
| ~ in_environment(sk3,equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_7380,c_76]) ).
tcf(c_8369,plain,
growth_rate(first_movers,sk4(sk2(sk3))) = growth_rate(first_movers,sk4(sk2(sk3))),
inference(instantiation,[status(thm)],[c_2721]) ).
tcf(c_8392,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ( zero != growth_rate(efficient_producers,sk4(sk2(sk3))) )
| ( growth_rate(first_movers,sk4(sk2(sk3))) != growth_rate(first_movers,sk4(sk2(sk3))) ) ),
inference(instantiation,[status(thm)],[c_5376]) ).
tcf(c_8519,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ greater_or_equal(sk2(sk3),sk1(sk3))
| ( sk1(sk3) != sk1(sk3) )
| ( sk4(sk2(sk3)) != sk2(sk3) ) ),
inference(instantiation,[status(thm)],[c_4751]) ).
tcf(c_8729,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ greater(sk1(sk3),equilibrium(sk3))
| ( equilibrium(sk3) != equilibrium(sk3) )
| ( sk4(sk1(sk3)) != sk1(sk3) ) ),
inference(instantiation,[status(thm)],[c_5407]) ).
tcf(c_9401,plain,
( greater(sk2(sk3),sk1(sk3))
| ( equilibrium(sk3) = sk2(sk3) )
| ( sk1(sk3) = sk2(sk3) ) ),
inference(global_subsumption_just,[status(thm)],[c_7603,c_94,c_333,c_355,c_2735,c_3018,c_3017,c_3016,c_3043,c_3158,c_3472,c_3530,c_3826,c_3843,c_3871,c_4085,c_4632,c_4776,c_5127,c_6050,c_6092,c_6123,c_6820,c_8729]) ).
tcf(c_9402,plain,
( greater(sk2(sk3),sk1(sk3))
| ( sk1(sk3) = sk2(sk3) )
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(renaming,[status(thm)],[c_9401]) ).
tcf(c_9407,plain,
( greater_or_equal(sk2(sk3),sk1(sk3))
| ( sk1(sk3) = sk2(sk3) )
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(superposition,[status(thm)],[c_9402,c_77]) ).
tcf(c_10966,plain,
! [X0: $i] :
( greater_or_equal(sk1(sk3),X0)
| ~ greater_or_equal(sk1(sk3),sk1(sk3))
| ( X0 != sk1(sk3) )
| ( sk1(sk3) != sk1(sk3) ) ),
inference(instantiation,[status(thm)],[c_7260]) ).
tcf(c_10991,plain,
( ( sk2(sk3) = equilibrium(sk3) )
| ( sk2(sk3) != sk2(sk3) )
| ( equilibrium(sk3) != sk2(sk3) ) ),
inference(instantiation,[status(thm)],[c_7279]) ).
tcf(c_11303,plain,
( greater(sk2(sk3),equilibrium(sk3))
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(superposition,[status(thm)],[c_327,c_76]) ).
tcf(c_11305,plain,
! [X0: $i] :
( greater_or_equal(sk1(sk3),X0)
| greater(X0,sk1(sk3))
| ~ in_environment(sk3,X0) ),
inference(global_subsumption_just,[status(thm)],[c_3289,c_94,c_355,c_3055,c_3243,c_4000,c_4043,c_4120,c_10966]) ).
tcf(c_11308,plain,
! [X0: $i] :
( greater(X0,sk1(sk3))
| greater(sk1(sk3),X0)
| ( sk1(sk3) = X0 )
| ~ in_environment(sk3,X0) ),
inference(superposition,[status(thm)],[c_11305,c_76]) ).
tcf(c_11341,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(first_movers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3222,c_6090]) ).
tcf(c_11342,plain,
! [X0: $i] :
( ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_11341]) ).
tcf(c_11343,plain,
( ( growth_rate(first_movers,sk4(sk1(sk3))) = zero )
| ~ in_environment(sk3,sk1(sk3))
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_97,c_11342]) ).
tcf(c_11345,plain,
! [X0: $i] :
( ( sk4(X0) = X0 )
| ( growth_rate(first_movers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater(X0,sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_3167,c_11342]) ).
tcf(c_11346,plain,
~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)),
inference(global_subsumption_just,[status(thm)],[c_11343,c_6121]) ).
tcf(c_11348,plain,
( ( sk4(sk1(sk3)) = sk1(sk3) )
| ~ in_environment(sk3,sk1(sk3))
| ~ greater(sk1(sk3),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_3167,c_11346]) ).
tcf(c_11349,plain,
~ greater(sk1(sk3),equilibrium(sk3)),
inference(global_subsumption_just,[status(thm)],[c_11348,c_94,c_355,c_3043,c_6121,c_6123,c_6820,c_8729]) ).
tcf(c_11369,plain,
( greater(equilibrium(sk3),sk1(sk3))
| ( equilibrium(sk3) = sk1(sk3) )
| ~ in_environment(sk3,equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_11308,c_11349]) ).
tcf(c_11394,plain,
! [X0: $i] :
( ~ greater_or_equal(sk4(X0),equilibrium(sk3))
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ in_environment(sk3,X0)
| ( growth_rate(efficient_producers,sk4(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3223,c_6195]) ).
tcf(c_11395,plain,
! [X0: $i] :
( ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater_or_equal(sk4(X0),sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(renaming,[status(thm)],[c_11394]) ).
tcf(c_11398,plain,
! [X0: $i] :
( ( sk4(X0) = X0 )
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater(X0,sk1(sk3))
| ~ greater_or_equal(sk4(X0),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_3167,c_11395]) ).
tcf(c_11619,plain,
( greater(equilibrium(sk3),sk1(sk3))
| ~ in_environment(sk3,equilibrium(sk3)) ),
inference(global_subsumption_just,[status(thm)],[c_11369,c_94,c_355,c_2735,c_3018,c_3017,c_3016,c_3043,c_3158,c_3277,c_3472,c_3530,c_3843,c_3871,c_4085,c_4632,c_4776,c_5127,c_6050,c_6092,c_6123,c_6507,c_6820,c_8729]) ).
tcf(c_11625,plain,
( greater_or_equal(equilibrium(sk3),sk1(sk3))
| ~ in_environment(sk3,equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_11619,c_77]) ).
tcf(c_11738,plain,
( ( equilibrium(sk3) = sk2(sk3) )
| ( sk4(sk2(sk3)) = sk2(sk3) )
| ( growth_rate(first_movers,sk4(sk2(sk3))) = zero )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater(sk2(sk3),sk1(sk3))
| ~ greater(equilibrium(sk3),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_5101,c_11345]) ).
tcf(c_11742,plain,
! [X0: $i] :
( ( sk4(X0) = X0 )
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater(X0,sk1(sk3))
| ~ greater(X0,equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_3167,c_11398]) ).
tcf(c_11789,plain,
! [X0: $i] :
( ( sk4(X0) = X0 )
| ( growth_rate(efficient_producers,sk4(X0)) = zero )
| ~ in_environment(sk3,X0)
| ~ greater(X0,equilibrium(sk3)) ),
inference(global_subsumption_just,[status(thm)],[c_11742,c_94,c_355,c_2735,c_3018,c_3017,c_3016,c_3043,c_3114,c_3158,c_3267,c_3472,c_3530,c_3843,c_3871,c_3911,c_4085,c_4632,c_4776,c_5127,c_5407,c_5474,c_6050,c_6092,c_6123,c_6371,c_6820,c_7531,c_8729]) ).
tcf(c_11794,plain,
( ( equilibrium(sk3) = sk2(sk3) )
| ( sk4(sk2(sk3)) = sk2(sk3) )
| ( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero )
| ~ in_environment(sk3,sk2(sk3)) ),
inference(superposition,[status(thm)],[c_11303,c_11789]) ).
tcf(c_11818,plain,
( ( equilibrium(sk3) = sk2(sk3) )
| ( sk4(sk2(sk3)) = sk2(sk3) ) ),
inference(global_subsumption_just,[status(thm)],[c_11738,c_94,c_99,c_333,c_2735,c_3009,c_3008,c_3007,c_3042,c_3136,c_3298,c_3431,c_3826,c_4576,c_8369,c_8392,c_11349,c_11794]) ).
tcf(c_11861,plain,
( greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| ( equilibrium(sk3) = sk2(sk3) )
| ( growth_rate(first_movers,sk4(sk2(sk3))) = zero )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[c_11818,c_1595]) ).
tcf(c_11865,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ( equilibrium(sk3) = sk2(sk3) )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3)) ),
inference(superposition,[status(thm)],[c_11818,c_741]) ).
tcf(c_11866,plain,
( ( equilibrium(sk3) = sk2(sk3) )
| ~ in_environment(sk3,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
inference(superposition,[status(thm)],[c_11818,c_398]) ).
tcf(c_11895,plain,
( ( equilibrium(sk3) = sk2(sk3) )
| ~ greater(zero,growth_rate(first_movers,sk2(sk3))) ),
inference(global_subsumption_just,[status(thm)],[c_11866,c_94,c_99,c_326,c_333,c_2735,c_3009,c_3008,c_3007,c_3040,c_3042,c_3055,c_3136,c_3298,c_3431,c_4043,c_4488,c_4849,c_5077,c_6820,c_8369,c_8392,c_8519,c_9407,c_11818]) ).
tcf(c_11897,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(global_subsumption_just,[status(thm)],[c_11865,c_94,c_99,c_326,c_333,c_2735,c_3009,c_3008,c_3007,c_3040,c_3042,c_3055,c_3136,c_3298,c_3431,c_4043,c_4488,c_4849,c_5077,c_6820,c_8369,c_8392,c_8519,c_9407,c_11818]) ).
tcf(c_11914,plain,
( greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(global_subsumption_just,[status(thm)],[c_11861,c_94,c_99,c_326,c_333,c_2735,c_3009,c_3008,c_3007,c_3040,c_3042,c_3055,c_3136,c_3298,c_3431,c_4043,c_4488,c_4849,c_5077,c_6820,c_8369,c_8392,c_8519,c_9407,c_11818]) ).
tcf(c_11919,plain,
! [X0: $i] :
( greater(zero,X0)
| ( equilibrium(sk3) = sk2(sk3) )
| ~ greater(growth_rate(efficient_producers,sk2(sk3)),X0) ),
inference(superposition,[status(thm)],[c_11914,c_74]) ).
tcf(c_11962,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| ( equilibrium(sk3) = sk2(sk3) ) ),
inference(superposition,[status(thm)],[c_11897,c_11919]) ).
tcf(c_11963,plain,
equilibrium(sk3) = sk2(sk3),
inference(global_subsumption_just,[status(thm)],[c_11962,c_11895,c_11962]) ).
tcf(c_13343,plain,
( ( sk4(sk2(sk3)) = equilibrium(sk3) )
| ( equilibrium(sk3) != sk2(sk3) )
| ( sk4(sk2(sk3)) != sk2(sk3) ) ),
inference(instantiation,[status(thm)],[c_6780]) ).
tcf(c_13701,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| ~ greater_or_equal(equilibrium(sk3),sk1(sk3))
| ( sk1(sk3) != sk1(sk3) )
| ( sk4(sk2(sk3)) != equilibrium(sk3) ) ),
inference(instantiation,[status(thm)],[c_4751]) ).
tcf(c_15031,plain,
( greater(sk2(sk3),sk1(sk3))
| ~ greater(equilibrium(sk3),sk1(sk3))
| ( sk2(sk3) != equilibrium(sk3) )
| ( sk1(sk3) != sk1(sk3) ) ),
inference(instantiation,[status(thm)],[c_7053]) ).
tcf(c_15040,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_15031,c_13701,c_13343,c_11963,c_11625,c_11349,c_10991,c_8392,c_8369,c_6507,c_6121,c_5514,c_4849,c_4576,c_4488,c_4043,c_3987,c_3431,c_3283,c_3277,c_3158,c_3136,c_3055,c_3042,c_3040,c_3018,c_3007,c_3008,c_3009,c_2735,c_355,c_333,c_99,c_94]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/5.39 % Computer : n006.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Thu Sep 24 01:07:22 UTC 2026
% 0.16/5.40 % CPUTime :
% 0.16/5.40 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.44 Running first-order theorem proving
% 0.16/5.44 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.45
% 0.16/5.45 % ======== iProver multi-core TPTP/SMT =========
% 0.16/5.45
% 0.16/5.45 % Detected problem language: tptp
% 0.16/5.46 % Proving...
% 7.13/6.77 % SZS status Started for theBenchmark.p
% 7.13/6.77 % SZS status Unsatisfiable for theBenchmark.p
% 7.13/6.77
% 7.13/6.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.13/6.77
% 7.13/6.77 % ------ iProver source info
% 7.13/6.77
% 7.13/6.77 % git: date: 2026-07-19 20:42:38 +0200
% 7.13/6.77 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.13/6.77 % git: non_committed_changes: false
% 7.13/6.77
% 7.13/6.77 % ------ Parsing...% successful
% 7.13/6.77
% 7.13/6.77
% 7.13/6.77 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 7.13/6.77
% 7.13/6.77 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 5 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 5 0s sf_e pe_s pe_e %
% 7.13/6.77
% 7.13/6.77 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 7.13/6.77
% 7.13/6.77 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 7.13/6.77 % ------ Proving...
% 7.13/6.77 % ------ Problem Properties
% 7.13/6.77
% 7.13/6.77 %
% 7.13/6.77 % clauses 15
% 7.13/6.77 % conjectures 1
% 7.13/6.77 % EPR 5
% 7.13/6.77 % Horn 9
% 7.13/6.77 % unary 4
% 7.13/6.77 % binary 2
% 7.13/6.77 % lits 41
% 7.13/6.77 % lits eq 6
% 7.13/6.77 % fd_pure 0
% 7.13/6.77 % fd_pseudo 0
% 7.13/6.77 % fd_cond 0
% 7.13/6.77 % fd_pseudo_cond 2
% 7.13/6.77 % AC symbols 0
% 7.13/6.77
% 7.13/6.77 % ------ Input Options Time Limit: Unbounded
% 7.13/6.77
% 7.13/6.77
% 7.13/6.77 % ------
% 7.13/6.77 % Current options:
% 7.13/6.77 % ------
% 7.13/6.77
% 7.13/6.77
% 7.13/6.77 %
% 7.13/6.77
% 7.13/6.77 % ------ Proving...
% 7.13/6.77 %
% 7.13/6.77
% 7.13/6.77 % SZS status Unsatisfiable for theBenchmark.p
% 7.13/6.77
% 7.13/6.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.13/6.78
% 7.13/6.78
%------------------------------------------------------------------------------