%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : MGT035+1 : 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 : n009.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:27 PM UTC 2026
% Result : Theorem 8.19s 1.72s
% Output : CNFRefutation 8.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 14
% Syntax : Number of formulae : 335 ( 26 unt; 0 def)
% Number of atoms : 1338 ( 372 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1717 ( 714 ~; 934 |; 54 &)
% ( 4 <=>; 11 =>; 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 : 388 ( 0 sgn 376 !; 12 ?; 266 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( ( greater(X1,X2)
& greater(X0,X1) )
=> greater(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( in_environment(X0,X2)
& in_environment(X0,X1) )
=> ( greater(X1,X2)
| X2 = X1
| greater(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_times_in_environment) ).
fof(f3,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(f4,axiom,
! [X0,X1,X2,X3] :
( ( subpopulations(X1,X2,X0,X3)
& environment(X0) )
=> ( ( greater(zero,growth_rate(X1,X3))
& greater_or_equal(growth_rate(X2,X3),zero) )
<=> outcompetes(X2,X1,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2) ).
fof(f5,axiom,
! [X0,X1] :
( ( greater_or_equal(X1,equilibrium(X0))
& subpopulations(first_movers,efficient_producers,X0,X1)
& environment(X0) )
=> ( ( greater(zero,growth_rate(first_movers,X1))
& greater(growth_rate(efficient_producers,X1),zero) )
| ( greater(zero,growth_rate(efficient_producers,X1))
& greater(growth_rate(first_movers,X1),zero) )
| ( growth_rate(efficient_producers,X1) = zero
& growth_rate(first_movers,X1) = zero ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l6) ).
fof(f6,axiom,
! [X0] :
( ( stable(X0)
& environment(X0) )
=> ? [X1] :
( ! [X2] :
( ( greater_or_equal(X2,X1)
& subpopulations(first_movers,efficient_producers,X0,X2) )
=> greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) )
& in_environment(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1) ).
fof(f7,axiom,
! [X0] :
( ( stable(X0)
& environment(X0) )
=> ? [X1] :
( greater_or_equal(X1,equilibrium(X0))
& in_environment(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
fof(f8,conjecture,
! [X0] :
( ( stable(X0)
& environment(X0) )
=> ? [X1] :
( ! [X2] :
( ( greater_or_equal(X2,X1)
& subpopulations(first_movers,efficient_producers,X0,X2) )
=> outcompetes(efficient_producers,first_movers,X2) )
& in_environment(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t4) ).
fof(f9,negated_conjecture,
~ ! [X0] :
( ( stable(X0)
& environment(X0) )
=> ? [X1] :
( ! [X2] :
( ( greater_or_equal(X2,X1)
& subpopulations(first_movers,efficient_producers,X0,X2) )
=> outcompetes(efficient_producers,first_movers,X2) )
& in_environment(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f8]) ).
fof(f10,plain,
! [X0,X1,X2] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(ennf_transformation,[],[f1]) ).
fof(f11,plain,
! [X0,X1,X2] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(flattening,[],[f10]) ).
fof(f12,plain,
! [X0,X1,X2] :
( ~ in_environment(X0,X2)
| ~ in_environment(X0,X1)
| greater(X1,X2)
| X2 = X1
| greater(X2,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f13,plain,
! [X0,X1,X2] :
( ~ in_environment(X0,X2)
| ~ in_environment(X0,X1)
| greater(X1,X2)
| X2 = X1
| greater(X2,X1) ),
inference(flattening,[],[f12]) ).
fof(f14,plain,
! [X0,X1,X2,X3] :
( ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| ( ( greater(zero,growth_rate(X1,X3))
& greater_or_equal(growth_rate(X2,X3),zero) )
<=> outcompetes(X2,X1,X3) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f15,plain,
! [X0,X1,X2,X3] :
( ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| ( ( greater(zero,growth_rate(X1,X3))
& greater_or_equal(growth_rate(X2,X3),zero) )
<=> outcompetes(X2,X1,X3) ) ),
inference(flattening,[],[f14]) ).
fof(f16,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ( greater(zero,growth_rate(first_movers,X1))
& greater(growth_rate(efficient_producers,X1),zero) )
| ( greater(zero,growth_rate(efficient_producers,X1))
& greater(growth_rate(first_movers,X1),zero) )
| ( growth_rate(efficient_producers,X1) = zero
& growth_rate(first_movers,X1) = zero ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f17,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ( greater(zero,growth_rate(first_movers,X1))
& greater(growth_rate(efficient_producers,X1),zero) )
| ( greater(zero,growth_rate(efficient_producers,X1))
& greater(growth_rate(first_movers,X1),zero) )
| ( growth_rate(efficient_producers,X1) = zero
& growth_rate(first_movers,X1) = zero ) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| ? [X1] :
( ! [X2] :
( ~ greater_or_equal(X2,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) )
& in_environment(X0,X1) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f19,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| ? [X1] :
( ! [X2] :
( ~ greater_or_equal(X2,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) )
& in_environment(X0,X1) ) ),
inference(flattening,[],[f18]) ).
fof(f20,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| ? [X1] :
( greater_or_equal(X1,equilibrium(X0))
& in_environment(X0,X1) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f21,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| ? [X1] :
( greater_or_equal(X1,equilibrium(X0))
& in_environment(X0,X1) ) ),
inference(flattening,[],[f20]) ).
fof(f22,plain,
? [X0] :
( stable(X0)
& environment(X0)
& ! [X1] :
( ? [X2] :
( greater_or_equal(X2,X1)
& subpopulations(first_movers,efficient_producers,X0,X2)
& ~ outcompetes(efficient_producers,first_movers,X2) )
| ~ in_environment(X0,X1) ) ),
inference(ennf_transformation,[],[f9]) ).
fof(f23,plain,
? [X0] :
( stable(X0)
& environment(X0)
& ! [X1] :
( ? [X2] :
( greater_or_equal(X2,X1)
& subpopulations(first_movers,efficient_producers,X0,X2)
& ~ outcompetes(efficient_producers,first_movers,X2) )
| ~ in_environment(X0,X1) ) ),
inference(flattening,[],[f22]) ).
fof(f24,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,[],[f3]) ).
fof(f25,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,[],[f24]) ).
fof(f26,plain,
! [X0,X1,X2,X3] :
( ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| ( ( ~ greater(zero,growth_rate(X1,X3))
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| outcompetes(X2,X1,X3) )
& ( ~ outcompetes(X2,X1,X3)
| ( greater(zero,growth_rate(X1,X3))
& greater_or_equal(growth_rate(X2,X3),zero) ) ) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f27,plain,
! [X0,X1,X2,X3] :
( ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| ( ( ~ greater(zero,growth_rate(X1,X3))
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| outcompetes(X2,X1,X3) )
& ( ~ outcompetes(X2,X1,X3)
| ( greater(zero,growth_rate(X1,X3))
& greater_or_equal(growth_rate(X2,X3),zero) ) ) ) ),
inference(flattening,[],[f26]) ).
fof(f28,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| ( ! [X2] :
( ~ greater_or_equal(X2,sK0(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) )
& in_environment(X0,sK0(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f19]) ).
fof(f29,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| ( greater_or_equal(sK1(X0),equilibrium(X0))
& in_environment(X0,sK1(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X1,sK1(X0))],[f21]) ).
fof(f30,plain,
( stable(sK2)
& environment(sK2)
& ! [X1] :
( ( greater_or_equal(sK3(X1),X1)
& subpopulations(first_movers,efficient_producers,sK2,sK3(X1))
& ~ outcompetes(efficient_producers,first_movers,sK3(X1)) )
| ~ in_environment(sK2,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X0,sK2),skolemize(X2,sK3(X1))],[f23]) ).
fof(f31,plain,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(cnf_transformation,[],[f11]) ).
fof(f32,plain,
! [X2,X0,X1] :
( ~ in_environment(X0,X2)
| ~ in_environment(X0,X1)
| greater(X1,X2)
| X1 = X2
| greater(X2,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f33,plain,
! [X0,X1] :
( ~ greater_or_equal(X0,X1)
| X0 = X1
| greater(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f34,plain,
! [X0,X1] :
( X0 != X1
| greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f35,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f36,plain,
! [X2,X3,X0,X1] :
( ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| ~ greater(zero,growth_rate(X1,X3))
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| outcompetes(X2,X1,X3) ),
inference(cnf_transformation,[],[f27]) ).
fof(f39,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(zero,growth_rate(first_movers,X1))
| greater(zero,growth_rate(efficient_producers,X1))
| zero = growth_rate(efficient_producers,X1) ),
inference(cnf_transformation,[],[f17]) ).
fof(f40,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(growth_rate(efficient_producers,X1),zero)
| greater(zero,growth_rate(efficient_producers,X1))
| zero = growth_rate(efficient_producers,X1) ),
inference(cnf_transformation,[],[f17]) ).
fof(f41,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| zero = growth_rate(efficient_producers,X1) ),
inference(cnf_transformation,[],[f17]) ).
fof(f42,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| zero = growth_rate(efficient_producers,X1) ),
inference(cnf_transformation,[],[f17]) ).
fof(f43,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(zero,growth_rate(first_movers,X1))
| greater(zero,growth_rate(efficient_producers,X1))
| zero = growth_rate(first_movers,X1) ),
inference(cnf_transformation,[],[f17]) ).
fof(f44,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(growth_rate(efficient_producers,X1),zero)
| greater(zero,growth_rate(efficient_producers,X1))
| zero = growth_rate(first_movers,X1) ),
inference(cnf_transformation,[],[f17]) ).
fof(f45,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(zero,growth_rate(first_movers,X1))
| greater(growth_rate(first_movers,X1),zero)
| zero = growth_rate(first_movers,X1) ),
inference(cnf_transformation,[],[f17]) ).
fof(f46,plain,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| zero = growth_rate(first_movers,X1) ),
inference(cnf_transformation,[],[f17]) ).
fof(f47,plain,
! [X2,X0] :
( ~ stable(X0)
| ~ environment(X0)
| ~ greater_or_equal(X2,sK0(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ),
inference(cnf_transformation,[],[f28]) ).
fof(f48,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sK0(X0)) ),
inference(cnf_transformation,[],[f28]) ).
fof(f49,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| greater_or_equal(sK1(X0),equilibrium(X0)) ),
inference(cnf_transformation,[],[f29]) ).
fof(f50,plain,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sK1(X0)) ),
inference(cnf_transformation,[],[f29]) ).
fof(f51,plain,
stable(sK2),
inference(cnf_transformation,[],[f30]) ).
fof(f52,plain,
environment(sK2),
inference(cnf_transformation,[],[f30]) ).
fof(f53,plain,
! [X1] :
( greater_or_equal(sK3(X1),X1)
| ~ in_environment(sK2,X1) ),
inference(cnf_transformation,[],[f30]) ).
fof(f54,plain,
! [X1] :
( subpopulations(first_movers,efficient_producers,sK2,sK3(X1))
| ~ in_environment(sK2,X1) ),
inference(cnf_transformation,[],[f30]) ).
fof(f55,plain,
! [X1] :
( ~ outcompetes(efficient_producers,first_movers,sK3(X1))
| ~ in_environment(sK2,X1) ),
inference(cnf_transformation,[],[f30]) ).
fof(f56,plain,
! [X1] : greater_or_equal(X1,X1),
inference(equality_resolution,[],[f34]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_50,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,[],[f32]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_52,plain,
! [X0: $i] : greater_or_equal(X0,X0),
inference(cnf_transformation,[],[f56]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( greater(X0,X1)
| ( X0 = X1 )
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_56,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,[],[f36]) ).
tcf(c_57,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,[],[f46]) ).
tcf(c_58,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,[],[f45]) ).
tcf(c_59,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,[],[f44]) ).
tcf(c_60,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,[],[f43]) ).
tcf(c_61,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,[],[f42]) ).
tcf(c_62,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,[],[f41]) ).
tcf(c_63,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,[],[f40]) ).
tcf(c_64,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,[],[f39]) ).
tcf(c_65,plain,
! [X0: $i] :
( in_environment(X0,sK0(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ stable(X0)
| ~ environment(X0)
| ~ greater_or_equal(X1,sK0(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_67,plain,
! [X0: $i] :
( in_environment(X0,sK1(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_68,plain,
! [X0: $i] :
( greater_or_equal(sK1(X0),equilibrium(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_69,negated_conjecture,
! [X0: $i] :
( ~ in_environment(sK2,X0)
| ~ outcompetes(efficient_producers,first_movers,sK3(X0)) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_70,negated_conjecture,
! [X0: $i] :
( subpopulations(first_movers,efficient_producers,sK2,sK3(X0))
| ~ in_environment(sK2,X0) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_71,negated_conjecture,
! [X0: $i] :
( greater_or_equal(sK3(X0),X0)
| ~ in_environment(sK2,X0) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_72,negated_conjecture,
environment(sK2),
inference(cnf_transformation,[],[f52]) ).
tcf(c_73,negated_conjecture,
stable(sK2),
inference(cnf_transformation,[],[f51]) ).
tcf(c_74,plain,
greater_or_equal(zero,zero),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_300,plain,
! [X0: $i] :
( greater_or_equal(sK1(X0),equilibrium(X0))
| ~ environment(X0)
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_68,c_73]) ).
tcf(c_301,plain,
( greater_or_equal(sK1(sK2),equilibrium(sK2))
| ~ environment(sK2) ),
inference(unflattening,[status(thm)],[c_300]) ).
tcf(c_302,plain,
greater_or_equal(sK1(sK2),equilibrium(sK2)),
inference(global_subsumption_just,[status(thm)],[c_301,c_72,c_301]) ).
tcf(c_307,plain,
! [X0: $i] :
( in_environment(X0,sK1(X0))
| ~ environment(X0)
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_67,c_73]) ).
tcf(c_308,plain,
( in_environment(sK2,sK1(sK2))
| ~ environment(sK2) ),
inference(unflattening,[status(thm)],[c_307]) ).
tcf(c_309,plain,
in_environment(sK2,sK1(sK2)),
inference(global_subsumption_just,[status(thm)],[c_308,c_72,c_308]) ).
tcf(c_314,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ environment(X0)
| ~ greater_or_equal(X1,sK0(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_66,c_73]) ).
tcf(c_315,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ environment(sK2)
| ~ greater_or_equal(X0,sK0(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_314]) ).
tcf(c_317,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0)
| ~ greater_or_equal(X0,sK0(sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_315,c_72,c_315]) ).
tcf(c_318,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ greater_or_equal(X0,sK0(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(renaming,[status(thm)],[c_317]) ).
tcf(c_329,plain,
! [X0: $i] :
( in_environment(X0,sK0(X0))
| ~ environment(X0)
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_65,c_73]) ).
tcf(c_330,plain,
( in_environment(sK2,sK0(sK2))
| ~ environment(sK2) ),
inference(unflattening,[status(thm)],[c_329]) ).
tcf(c_331,plain,
in_environment(sK2,sK0(sK2)),
inference(global_subsumption_just,[status(thm)],[c_330,c_72,c_330]) ).
tcf(c_346,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ environment(X4)
| ~ in_environment(sK2,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 )
| ( sK3(X2) != X3 ) ),
inference(resolution_lifted,[status(thm)],[c_56,c_69]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i] :
( ~ environment(X0)
| ~ in_environment(sK2,X1)
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(X1)),zero)
| ~ greater(zero,growth_rate(first_movers,sK3(X1)))
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(X1)) ),
inference(unflattening,[status(thm)],[c_346]) ).
tcf(c_369,plain,
! [X0: $i,X1: $i] :
( ~ in_environment(sK2,X1)
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(X1)),zero)
| ~ greater(zero,growth_rate(first_movers,sK3(X1)))
| ~ subpopulations(first_movers,efficient_producers,X0,sK3(X1))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_347,c_72]) ).
tcf(c_370,plain,
! [X0: $i] :
( ~ in_environment(sK2,X0)
| ~ subpopulations(first_movers,efficient_producers,sK2,sK3(X0))
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sK3(X0))) ),
inference(unflattening,[status(thm)],[c_369]) ).
tcf(c_372,plain,
! [X0: $i] :
( ~ in_environment(sK2,X0)
| ~ greater(zero,growth_rate(first_movers,sK3(X0)))
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_370,c_70,c_370]) ).
tcf(c_373,plain,
! [X0: $i] :
( ~ in_environment(sK2,X0)
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(X0)),zero)
| ~ greater(zero,growth_rate(first_movers,sK3(X0))) ),
inference(renaming,[status(thm)],[c_372]) ).
tcf(c_384,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 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_72]) ).
tcf(c_385,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(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_384]) ).
tcf(c_402,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 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_72]) ).
tcf(c_403,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(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_402]) ).
tcf(c_420,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 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_72]) ).
tcf(c_421,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(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_420]) ).
tcf(c_438,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 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_72]) ).
tcf(c_439,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(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_438]) ).
tcf(c_456,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 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_72]) ).
tcf(c_457,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(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_456]) ).
tcf(c_474,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 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_72]) ).
tcf(c_475,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(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_474]) ).
tcf(c_492,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 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_72]) ).
tcf(c_493,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(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_492]) ).
tcf(c_510,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 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_72]) ).
tcf(c_511,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(sK2))
| ~ subpopulations(first_movers,efficient_producers,sK2,X0) ),
inference(unflattening,[status(thm)],[c_510]) ).
tcf(c_571,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(sK2,X0)
| ~ greater_or_equal(X1,equilibrium(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_511]) ).
tcf(c_572,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sK3(X0)),zero)
| greater(growth_rate(first_movers,sK3(X0)),zero)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(unflattening,[status(thm)],[c_571]) ).
tcf(c_589,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(sK2,X0)
| ~ greater_or_equal(X1,equilibrium(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_493]) ).
tcf(c_590,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sK3(X0)))
| greater(growth_rate(first_movers,sK3(X0)),zero)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(unflattening,[status(thm)],[c_589]) ).
tcf(c_607,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(sK2,X0)
| ~ greater_or_equal(X1,equilibrium(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_475]) ).
tcf(c_608,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| greater(growth_rate(efficient_producers,sK3(X0)),zero)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(unflattening,[status(thm)],[c_607]) ).
tcf(c_625,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(sK2,X0)
| ~ greater_or_equal(X1,equilibrium(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_457]) ).
tcf(c_626,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| greater(zero,growth_rate(first_movers,sK3(X0)))
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(unflattening,[status(thm)],[c_625]) ).
tcf(c_643,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(sK2,X0)
| ~ greater_or_equal(X1,equilibrium(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_439]) ).
tcf(c_644,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sK3(X0)),zero)
| greater(growth_rate(first_movers,sK3(X0)),zero)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(unflattening,[status(thm)],[c_643]) ).
tcf(c_661,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(sK2,X0)
| ~ greater_or_equal(X1,equilibrium(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_421]) ).
tcf(c_662,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sK3(X0)))
| greater(growth_rate(first_movers,sK3(X0)),zero)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(unflattening,[status(thm)],[c_661]) ).
tcf(c_679,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(sK2,X0)
| ~ greater_or_equal(X1,equilibrium(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_403]) ).
tcf(c_680,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| greater(growth_rate(efficient_producers,sK3(X0)),zero)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(unflattening,[status(thm)],[c_679]) ).
tcf(c_697,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(sK2,X0)
| ~ greater_or_equal(X1,equilibrium(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_385]) ).
tcf(c_698,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| greater(zero,growth_rate(first_movers,sK3(X0)))
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(unflattening,[status(thm)],[c_697]) ).
tcf(c_715,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(X1,sK0(sK2))
| ( sK2 != sK2 )
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( sK3(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_318]) ).
tcf(c_716,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sK3(X0)),growth_rate(first_movers,sK3(X0)))
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2)) ),
inference(unflattening,[status(thm)],[c_715]) ).
tcf(c_794,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ in_environment(sK2,X0)
| ~ greater(X1,X2)
| ~ greater(zero,growth_rate(first_movers,sK3(X0)))
| ( X2 != zero )
| ( growth_rate(efficient_producers,sK3(X0)) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_51,c_373]) ).
tcf(c_795,plain,
! [X0: $i] :
( ~ in_environment(sK2,X0)
| ~ greater(zero,growth_rate(first_movers,sK3(X0)))
| ~ greater(growth_rate(efficient_producers,sK3(X0)),zero) ),
inference(unflattening,[status(thm)],[c_794]) ).
tcf(c_962,plain,
! [X0: $i,X1: $i] :
( ~ in_environment(sK2,X0)
| ~ greater(zero,growth_rate(first_movers,sK3(X0)))
| ( X1 != zero )
| ( growth_rate(efficient_producers,sK3(X0)) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_373]) ).
tcf(c_963,plain,
! [X0: $i] :
( ~ in_environment(sK2,X0)
| ~ greater(zero,growth_rate(first_movers,sK3(X0)))
| ( growth_rate(efficient_producers,sK3(X0)) != zero ) ),
inference(unflattening,[status(thm)],[c_962]) ).
tcf(c_1521,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(efficient_producers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_698,c_680,c_698,c_795]) ).
tcf(c_1522,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_1521]) ).
tcf(c_1524,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(efficient_producers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_680,c_680,c_698,c_795]) ).
tcf(c_1525,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_1524]) ).
tcf(c_1526,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| greater(growth_rate(first_movers,sK3(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_662,c_644,c_662,c_795]) ).
tcf(c_1527,plain,
! [X0: $i] :
( greater(growth_rate(first_movers,sK3(X0)),zero)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_1526]) ).
tcf(c_1529,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| greater(growth_rate(first_movers,sK3(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_644,c_1527]) ).
tcf(c_1530,plain,
! [X0: $i] :
( greater(growth_rate(first_movers,sK3(X0)),zero)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_1529]) ).
tcf(c_1531,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(first_movers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_626,c_626,c_963,c_1522]) ).
tcf(c_1532,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_1531]) ).
tcf(c_1534,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(first_movers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_608,c_1532]) ).
tcf(c_1535,plain,
! [X0: $i] :
( greater(zero,growth_rate(efficient_producers,sK3(X0)))
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_1534]) ).
tcf(c_1536,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| greater(growth_rate(first_movers,sK3(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_590,c_572,c_590,c_795]) ).
tcf(c_1537,plain,
! [X0: $i] :
( greater(growth_rate(first_movers,sK3(X0)),zero)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_1536]) ).
tcf(c_1539,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| greater(growth_rate(first_movers,sK3(X0)),zero) ),
inference(global_subsumption_just,[status(thm)],[c_572,c_1537]) ).
tcf(c_1540,plain,
! [X0: $i] :
( greater(growth_rate(first_movers,sK3(X0)),zero)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_1539]) ).
tcf(c_2661,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_2663,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2664,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( greater(X0,X2)
| ~ greater(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2665,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_2666,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_2669,plain,
! [X0: $i,X1: $i] :
( ( sK0(X0) = sK0(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2675,plain,
zero = zero,
inference(instantiation,[status(thm)],[c_2661]) ).
tcf(c_2946,plain,
( greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ( growth_rate(efficient_producers,sK3(sK1(sK2))) = zero )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2)) ),
inference(instantiation,[status(thm)],[c_1525]) ).
tcf(c_2947,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2))))
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),sK0(sK2)) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_2948,plain,
( ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ greater(zero,growth_rate(first_movers,sK3(sK1(sK2)))) ),
inference(instantiation,[status(thm)],[c_373]) ).
tcf(c_2956,plain,
( greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ~ in_environment(sK2,sK0(sK2))
| ~ greater_or_equal(sK3(sK0(sK2)),sK0(sK2)) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_2957,plain,
( ~ in_environment(sK2,sK0(sK2))
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ greater(zero,growth_rate(first_movers,sK3(sK0(sK2)))) ),
inference(instantiation,[status(thm)],[c_373]) ).
tcf(c_2958,plain,
( greater_or_equal(sK3(sK0(sK2)),sK0(sK2))
| ~ in_environment(sK2,sK0(sK2)) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_2982,plain,
( greater_or_equal(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_2983,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sK3(sK0(sK2)),equilibrium(sK2))
| ~ greater_or_equal(X0,X1)
| ( equilibrium(sK2) != X1 )
| ( sK3(sK0(sK2)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2666]) ).
tcf(c_2985,plain,
( greater_or_equal(sK3(sK0(sK2)),equilibrium(sK2))
| ~ greater(sK3(sK0(sK2)),equilibrium(sK2)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_2992,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ greater_or_equal(X0,X1)
| ( zero != X1 )
| ( growth_rate(efficient_producers,sK3(sK0(sK2))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2666]) ).
tcf(c_2993,plain,
( greater_or_equal(growth_rate(efficient_producers,sK3(sK0(sK2))),zero)
| ~ greater_or_equal(zero,zero)
| ( zero != zero )
| ( growth_rate(efficient_producers,sK3(sK0(sK2))) != zero ) ),
inference(instantiation,[status(thm)],[c_2992]) ).
tcf(c_2995,plain,
sK2 = sK2,
inference(instantiation,[status(thm)],[c_2661]) ).
tcf(c_3011,plain,
! [X0: $i] :
( greater_or_equal(growth_rate(efficient_producers,sK3(X0)),growth_rate(first_movers,sK3(X0)))
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_716,c_51]) ).
tcf(c_3015,plain,
! [X0: $i] :
( greater_or_equal(sK3(sK0(sK2)),equilibrium(sK2))
| ~ greater_or_equal(sK3(sK0(sK2)),X0)
| ( equilibrium(sK2) != X0 )
| ( sK3(sK0(sK2)) != sK3(sK0(sK2)) ) ),
inference(instantiation,[status(thm)],[c_2983]) ).
tcf(c_3025,plain,
! [X0: $i,X1: $i] :
( greater(zero,X1)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(X0)),X1) ),
inference(superposition,[status(thm)],[c_1525,c_49]) ).
tcf(c_3026,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,sK3(X0)),X1)
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater(growth_rate(first_movers,sK3(X0)),X1) ),
inference(superposition,[status(thm)],[c_716,c_49]) ).
tcf(c_3044,plain,
! [X0: $i] :
( greater(sK3(X0),X0)
| ( sK3(X0) = X0 )
| ~ in_environment(sK2,X0) ),
inference(superposition,[status(thm)],[c_71,c_53]) ).
tcf(c_3045,plain,
( greater(sK1(sK2),equilibrium(sK2))
| ( equilibrium(sK2) = sK1(sK2) ) ),
inference(superposition,[status(thm)],[c_302,c_53]) ).
tcf(c_3054,plain,
! [X0: $i] :
( greater(sK3(sK0(sK2)),equilibrium(sK2))
| ~ greater(X0,equilibrium(sK2))
| ~ greater(sK3(sK0(sK2)),X0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_3062,plain,
! [X0: $i,X1: $i] :
( greater(sK3(X0),X1)
| ( sK3(X0) = X0 )
| ~ in_environment(sK2,X0)
| ~ greater(X0,X1) ),
inference(superposition,[status(thm)],[c_3044,c_49]) ).
tcf(c_3072,plain,
! [X0: $i,X1: $i] :
( greater(zero,X1)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(X0)),X1) ),
inference(superposition,[status(thm)],[c_1535,c_49]) ).
tcf(c_3098,plain,
sK3(sK0(sK2)) = sK3(sK0(sK2)),
inference(instantiation,[status(thm)],[c_2661]) ).
tcf(c_3106,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(sK3(X0),X2)
| ( sK3(X0) = X0 )
| ~ in_environment(sK2,X0)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(superposition,[status(thm)],[c_3062,c_49]) ).
tcf(c_3107,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sK3(X0),X1)
| ( sK3(X0) = X0 )
| ~ in_environment(sK2,X0)
| ~ greater(X0,X1) ),
inference(superposition,[status(thm)],[c_3062,c_51]) ).
tcf(c_3128,plain,
( greater(sK1(sK2),equilibrium(sK2))
| ( equilibrium(sK2) = sK1(sK2) ) ),
inference(superposition,[status(thm)],[c_302,c_53]) ).
tcf(c_3162,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sK3(X0)),zero)
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_1540,c_3026]) ).
tcf(c_3163,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,sK3(X0)),zero)
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_1530,c_3026]) ).
tcf(c_3174,plain,
! [X0: $i] :
( greater(X0,sK1(sK2))
| greater(sK1(sK2),X0)
| ( sK1(sK2) = X0 )
| ~ in_environment(sK2,X0) ),
inference(superposition,[status(thm)],[c_309,c_50]) ).
tcf(c_3175,plain,
! [X0: $i] :
( greater(X0,sK0(sK2))
| greater(sK0(sK2),X0)
| ( sK0(sK2) = X0 )
| ~ in_environment(sK2,X0) ),
inference(superposition,[status(thm)],[c_331,c_50]) ).
tcf(c_3185,plain,
! [X0: $i,X1: $i] :
( greater(X1,X0)
| greater(sK1(sK2),X1)
| ( sK1(sK2) = X1 )
| ~ in_environment(sK2,X1)
| ~ greater(sK1(sK2),X0) ),
inference(superposition,[status(thm)],[c_3174,c_49]) ).
tcf(c_3198,plain,
! [X0: $i,X1: $i] :
( greater(X0,X1)
| ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ( X1 != growth_rate(first_movers,sK3(sK0(sK2))) )
| ( X0 != growth_rate(efficient_producers,sK3(sK0(sK2))) ) ),
inference(instantiation,[status(thm)],[c_2664]) ).
tcf(c_3207,plain,
! [X0: $i] :
( greater(sK3(sK0(sK2)),X0)
| ( sK3(sK0(sK2)) = X0 )
| ~ greater_or_equal(sK3(sK0(sK2)),X0) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_3212,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater_or_equal(sK3(sK0(sK2)),X1)
| ~ greater_or_equal(X0,X2)
| ( X1 != X2 )
| ( sK3(sK0(sK2)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2666]) ).
tcf(c_3217,plain,
( greater_or_equal(sK3(sK0(sK2)),equilibrium(sK2))
| ~ greater_or_equal(sK3(sK0(sK2)),sK0(sK2))
| ( equilibrium(sK2) != sK0(sK2) )
| ( sK3(sK0(sK2)) != sK3(sK0(sK2)) ) ),
inference(instantiation,[status(thm)],[c_3015]) ).
tcf(c_3225,plain,
! [X0: $i] :
( greater_or_equal(X0,sK0(sK2))
| greater(sK0(sK2),X0)
| ( sK0(sK2) = X0 )
| ~ in_environment(sK2,X0) ),
inference(superposition,[status(thm)],[c_3175,c_51]) ).
tcf(c_3229,plain,
! [X0: $i] :
( greater_or_equal(sK0(sK2),X0)
| greater(X0,sK0(sK2))
| ( sK0(sK2) = X0 )
| ~ in_environment(sK2,X0) ),
inference(superposition,[status(thm)],[c_3175,c_51]) ).
tcf(c_3370,plain,
! [X0: $i,X1: $i] :
( ( X1 = growth_rate(efficient_producers,sK3(sK1(sK2))) )
| ( X1 != X0 )
| ( growth_rate(efficient_producers,sK3(sK1(sK2))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2663]) ).
tcf(c_3371,plain,
( ( zero = growth_rate(efficient_producers,sK3(sK1(sK2))) )
| ( zero != zero )
| ( growth_rate(efficient_producers,sK3(sK1(sK2))) != zero ) ),
inference(instantiation,[status(thm)],[c_3370]) ).
tcf(c_3387,plain,
! [X0: $i] :
( greater(sK3(sK1(sK2)),X0)
| ( equilibrium(sK2) = sK1(sK2) )
| ( sK3(sK1(sK2)) = sK1(sK2) )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater(equilibrium(sK2),X0) ),
inference(superposition,[status(thm)],[c_3128,c_3106]) ).
tcf(c_3469,plain,
! [X0: $i] :
( greater(X0,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ( X0 != growth_rate(efficient_producers,sK3(sK0(sK2))) )
| ( growth_rate(first_movers,sK3(sK0(sK2))) != growth_rate(first_movers,sK3(sK0(sK2))) ) ),
inference(instantiation,[status(thm)],[c_3198]) ).
tcf(c_3470,plain,
( greater(zero,growth_rate(first_movers,sK3(sK0(sK2))))
| ~ greater(growth_rate(efficient_producers,sK3(sK0(sK2))),growth_rate(first_movers,sK3(sK0(sK2))))
| ( zero != growth_rate(efficient_producers,sK3(sK0(sK2))) )
| ( growth_rate(first_movers,sK3(sK0(sK2))) != growth_rate(first_movers,sK3(sK0(sK2))) ) ),
inference(instantiation,[status(thm)],[c_3469]) ).
tcf(c_3519,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sK3(sK0(sK2)),X0)
| ~ greater_or_equal(sK3(sK0(sK2)),X1)
| ( X0 != X1 )
| ( sK3(sK0(sK2)) != sK3(sK0(sK2)) ) ),
inference(instantiation,[status(thm)],[c_3212]) ).
tcf(c_3583,plain,
! [X0: $i] :
( ( sK0(X0) = sK0(sK2) )
| ( X0 != sK2 ) ),
inference(instantiation,[status(thm)],[c_2669]) ).
tcf(c_3851,plain,
! [X0: $i] :
( greater_or_equal(sK3(sK0(sK2)),X0)
| ~ greater_or_equal(sK3(sK0(sK2)),sK0(sK2))
| ( X0 != sK0(sK2) )
| ( sK3(sK0(sK2)) != sK3(sK0(sK2)) ) ),
inference(instantiation,[status(thm)],[c_3519]) ).
tcf(c_3983,plain,
( ( sK0(sK2) = sK0(sK2) )
| ( sK2 != sK2 ) ),
inference(instantiation,[status(thm)],[c_3583]) ).
tcf(c_3986,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sK3(X0)))
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_716,c_3025]) ).
tcf(c_4031,plain,
! [X0: $i] :
( greater(zero,growth_rate(first_movers,sK3(X0)))
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_716,c_3072]) ).
tcf(c_4389,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2664,c_2661]) ).
tcf(c_4444,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ( growth_rate(first_movers,sK3(sK1(sK2))) = zero )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),sK0(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2)) ),
inference(instantiation,[status(thm)],[c_3162]) ).
tcf(c_4449,plain,
! [X0: $i] :
( greater(zero,X0)
| ( growth_rate(first_movers,sK3(sK1(sK2))) = zero )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),X0) ),
inference(instantiation,[status(thm)],[c_3072]) ).
tcf(c_4452,plain,
! [X0: $i] :
( greater(zero,X0)
| ( growth_rate(efficient_producers,sK3(sK1(sK2))) = zero )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),X0) ),
inference(instantiation,[status(thm)],[c_3025]) ).
tcf(c_4469,plain,
! [X0: $i,X1: $i] :
( in_environment(X0,X1)
| ~ in_environment(sK2,sK1(sK2))
| ( X1 != sK1(sK2) )
| ( X0 != sK2 ) ),
inference(instantiation,[status(thm)],[c_2665]) ).
tcf(c_4515,plain,
! [X0: $i] :
( in_environment(sK2,X0)
| ~ in_environment(sK2,sK1(sK2))
| ( sK2 != sK2 )
| ( X0 != sK1(sK2) ) ),
inference(instantiation,[status(thm)],[c_4469]) ).
tcf(c_4531,plain,
( greater_or_equal(sK3(sK1(sK2)),sK0(sK2))
| ( sK3(sK1(sK2)) = sK1(sK2) )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater(sK1(sK2),sK0(sK2)) ),
inference(instantiation,[status(thm)],[c_3107]) ).
tcf(c_4540,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sK3(sK1(sK2)),sK0(sK2))
| ~ greater_or_equal(X0,X1)
| ( sK0(sK2) != X1 )
| ( sK3(sK1(sK2)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2666]) ).
tcf(c_4544,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| ~ greater_or_equal(X0,X1)
| ( equilibrium(sK2) != X1 )
| ( sK3(sK1(sK2)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2666]) ).
tcf(c_4634,plain,
! [X0: $i,X1: $i] :
( greater(X1,sK0(sK2))
| greater(sK0(sK2),X1)
| ( X1 = sK0(sK2) )
| ~ in_environment(X0,X1)
| ~ in_environment(X0,sK0(sK2)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_4652,plain,
! [X0: $i] :
( greater_or_equal(sK3(X0),sK0(sK2))
| ( sK3(X0) = X0 )
| ~ in_environment(sK2,X0)
| ~ greater(X0,sK0(sK2)) ),
inference(instantiation,[status(thm)],[c_3107]) ).
tcf(c_4706,plain,
! [X0: $i] :
( greater_or_equal(sK3(sK1(sK2)),sK0(sK2))
| ~ greater_or_equal(X0,sK0(sK2))
| ( sK0(sK2) != sK0(sK2) )
| ( sK3(sK1(sK2)) != X0 ) ),
inference(instantiation,[status(thm)],[c_4540]) ).
tcf(c_4713,plain,
! [X0: $i] :
( greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| ~ greater_or_equal(X0,equilibrium(sK2))
| ( equilibrium(sK2) != equilibrium(sK2) )
| ( sK3(sK1(sK2)) != X0 ) ),
inference(instantiation,[status(thm)],[c_4544]) ).
tcf(c_4715,plain,
! [X0: $i,X1: $i] :
( ( equilibrium(sK2) = X1 )
| ( X1 != X0 )
| ( equilibrium(sK2) != X0 ) ),
inference(instantiation,[status(thm)],[c_2663]) ).
tcf(c_4785,plain,
! [X0: $i,X1: $i] :
( greater(sK3(sK0(sK2)),equilibrium(sK2))
| ~ greater(X0,X1)
| ( equilibrium(sK2) != X1 )
| ( sK3(sK0(sK2)) != X0 ) ),
inference(instantiation,[status(thm)],[c_2664]) ).
tcf(c_4804,plain,
( greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ( growth_rate(efficient_producers,sK3(sK1(sK2))) = zero )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2)))) ),
inference(instantiation,[status(thm)],[c_4452]) ).
tcf(c_4805,plain,
( greater(zero,growth_rate(first_movers,sK3(sK1(sK2))))
| ( growth_rate(first_movers,sK3(sK1(sK2))) = zero )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),growth_rate(first_movers,sK3(sK1(sK2)))) ),
inference(instantiation,[status(thm)],[c_4449]) ).
tcf(c_4810,plain,
! [X0: $i] :
( greater_or_equal(sK3(sK1(sK2)),X0)
| ( sK3(sK1(sK2)) = sK1(sK2) )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater(sK1(sK2),X0) ),
inference(instantiation,[status(thm)],[c_3107]) ).
tcf(c_4897,plain,
! [X0: $i,X1: $i] :
( greater(sK0(sK2),X1)
| ~ greater(X0,X1)
| ~ greater(sK0(sK2),X0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_4914,plain,
! [X0: $i] :
( greater(X0,sK0(sK2))
| greater(sK0(sK2),X0)
| ( X0 = sK0(sK2) )
| ~ in_environment(sK2,X0)
| ~ in_environment(sK2,sK0(sK2)) ),
inference(instantiation,[status(thm)],[c_4634]) ).
tcf(c_5032,plain,
( greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| ~ greater_or_equal(sK1(sK2),equilibrium(sK2))
| ( equilibrium(sK2) != equilibrium(sK2) )
| ( sK3(sK1(sK2)) != sK1(sK2) ) ),
inference(instantiation,[status(thm)],[c_4713]) ).
tcf(c_5039,plain,
! [X0: $i] :
( ( equilibrium(sK2) = X0 )
| ( X0 != equilibrium(sK2) )
| ( equilibrium(sK2) != equilibrium(sK2) ) ),
inference(instantiation,[status(thm)],[c_4715]) ).
tcf(c_5049,plain,
! [X0: $i] :
( greater(sK3(sK1(sK2)),X0)
| ( equilibrium(sK2) = sK1(sK2) )
| ( sK3(sK1(sK2)) = sK1(sK2) )
| ~ greater(equilibrium(sK2),X0) ),
inference(global_subsumption_just,[status(thm)],[c_3387,c_72,c_308,c_3387]) ).
tcf(c_5056,plain,
! [X0: $i] :
( greater_or_equal(sK3(sK1(sK2)),X0)
| ( equilibrium(sK2) = sK1(sK2) )
| ( sK3(sK1(sK2)) = sK1(sK2) )
| ~ greater(equilibrium(sK2),X0) ),
inference(superposition,[status(thm)],[c_5049,c_51]) ).
tcf(c_5082,plain,
growth_rate(first_movers,sK3(sK0(sK2))) = growth_rate(first_movers,sK3(sK0(sK2))),
inference(instantiation,[status(thm)],[c_2661]) ).
tcf(c_5362,plain,
! [X0: $i] :
( greater(sK3(sK0(sK2)),equilibrium(sK2))
| ~ greater(X0,equilibrium(sK2))
| ( equilibrium(sK2) != equilibrium(sK2) )
| ( sK3(sK0(sK2)) != X0 ) ),
inference(instantiation,[status(thm)],[c_4785]) ).
tcf(c_5422,plain,
! [X0: $i] :
( greater(X0,sK1(sK2))
| greater(sK1(sK2),X0)
| ( X0 = sK1(sK2) )
| ~ in_environment(sK2,X0) ),
inference(resolution,[status(thm)],[c_50,c_309]) ).
tcf(c_5424,plain,
! [X0: $i] :
( greater(X0,sK0(sK2))
| greater(sK0(sK2),X0)
| ( X0 = sK0(sK2) )
| ~ in_environment(sK2,X0) ),
inference(resolution,[status(thm)],[c_50,c_331]) ).
tcf(c_5458,plain,
( greater_or_equal(sK3(sK1(sK2)),equilibrium(sK2))
| ( sK3(sK1(sK2)) = sK1(sK2) )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater(sK1(sK2),equilibrium(sK2)) ),
inference(instantiation,[status(thm)],[c_4810]) ).
tcf(c_5492,plain,
! [X0: $i,X1: $i] :
( greater(X1,X0)
| ~ greater(X1,sK1(sK2))
| ~ greater(sK1(sK2),X0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5568,plain,
! [X0: $i,X1: $i] :
( greater(X1,X0)
| ~ greater(X1,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),X0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5569,plain,
( greater(zero,zero)
| ~ greater(zero,growth_rate(efficient_producers,sK3(sK1(sK2))))
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) ),
inference(instantiation,[status(thm)],[c_5568]) ).
tcf(c_5570,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X0,X1)
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),X2)
| ( X1 != X2 )
| ( X0 != growth_rate(efficient_producers,sK3(sK1(sK2))) ) ),
inference(instantiation,[status(thm)],[c_2664]) ).
tcf(c_5571,plain,
( greater(zero,zero)
| ~ greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ( zero != zero )
| ( zero != growth_rate(efficient_producers,sK3(sK1(sK2))) ) ),
inference(instantiation,[status(thm)],[c_5570]) ).
tcf(c_5853,plain,
( greater_or_equal(sK3(equilibrium(sK2)),equilibrium(sK2))
| ~ in_environment(sK2,equilibrium(sK2)) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_5997,plain,
( greater_or_equal(equilibrium(sK2),sK0(sK2))
| greater(sK0(sK2),equilibrium(sK2))
| ( sK0(sK2) = equilibrium(sK2) )
| ~ in_environment(sK2,equilibrium(sK2)) ),
inference(instantiation,[status(thm)],[c_3225]) ).
tcf(c_6026,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(first_movers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3162,c_795,c_3162,c_4031]) ).
tcf(c_6027,plain,
! [X0: $i] :
( ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_6026]) ).
tcf(c_6185,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(efficient_producers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3163,c_795,c_3163,c_3986]) ).
tcf(c_6186,plain,
! [X0: $i] :
( ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_6185]) ).
tcf(c_6188,plain,
( ( growth_rate(efficient_producers,sK3(sK0(sK2))) = zero )
| ~ in_environment(sK2,sK0(sK2))
| ~ greater_or_equal(sK3(sK0(sK2)),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_71,c_6186]) ).
tcf(c_6270,plain,
( ( growth_rate(efficient_producers,sK3(sK0(sK2))) = zero )
| ~ greater_or_equal(sK3(sK0(sK2)),equilibrium(sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_6188,c_72,c_330,c_6188]) ).
tcf(c_6293,plain,
( greater(sK0(sK2),equilibrium(sK2))
| greater(equilibrium(sK2),sK0(sK2))
| ( equilibrium(sK2) = sK0(sK2) )
| ~ in_environment(sK2,sK0(sK2))
| ~ in_environment(sK2,equilibrium(sK2)) ),
inference(instantiation,[status(thm)],[c_4914]) ).
tcf(c_6531,plain,
( ( equilibrium(sK2) = sK0(sK2) )
| ( sK0(sK2) != equilibrium(sK2) )
| ( equilibrium(sK2) != equilibrium(sK2) ) ),
inference(instantiation,[status(thm)],[c_5039]) ).
tcf(c_6846,plain,
( greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2))
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater(equilibrium(sK2),sK0(sK2)) ),
inference(instantiation,[status(thm)],[c_4652]) ).
tcf(c_6873,plain,
! [X0: $i] :
( greater(sK3(X0),X0)
| ( sK3(X0) = X0 )
| ~ in_environment(sK2,X0) ),
inference(superposition,[status(thm)],[c_71,c_53]) ).
tcf(c_6878,plain,
! [X0: $i] :
( greater(X0,sK0(sK2))
| greater(sK0(sK2),X0)
| ( sK0(sK2) = X0 )
| ~ in_environment(sK2,X0) ),
inference(superposition,[status(thm)],[c_3229,c_53]) ).
tcf(c_6913,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(first_movers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3162,c_795,c_3162,c_4031]) ).
tcf(c_6914,plain,
! [X0: $i] :
( ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_6913]) ).
tcf(c_6916,plain,
! [X0: $i] :
( greater(sK0(sK2),sK3(X0))
| ( sK3(X0) = sK0(sK2) )
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ in_environment(sK2,sK3(X0))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_3225,c_6914]) ).
tcf(c_6917,plain,
! [X0: $i] :
( ( sK3(X0) = X0 )
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater(X0,sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_3107,c_6914]) ).
tcf(c_6961,plain,
( ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater(equilibrium(sK2),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_71,c_6917]) ).
tcf(c_6962,plain,
! [X0: $i] :
( ( sK3(X0) = X0 )
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater(X0,sK0(sK2))
| ~ greater(X0,equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_3107,c_6917]) ).
tcf(c_6972,plain,
( greater(sK0(sK2),sK3(equilibrium(sK2)))
| ( sK3(equilibrium(sK2)) = sK0(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ in_environment(sK2,sK3(equilibrium(sK2))) ),
inference(superposition,[status(thm)],[c_71,c_6916]) ).
tcf(c_6975,plain,
( greater(sK0(sK2),equilibrium(sK2))
| ( equilibrium(sK2) = sK0(sK2) )
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_6878,c_6961]) ).
tcf(c_6978,plain,
! [X0: $i] :
( greater(sK0(sK2),X0)
| ( sK3(equilibrium(sK2)) = sK0(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ in_environment(sK2,sK3(equilibrium(sK2)))
| ~ greater(sK3(equilibrium(sK2)),X0) ),
inference(superposition,[status(thm)],[c_6972,c_49]) ).
tcf(c_6982,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(efficient_producers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3163,c_795,c_3163,c_3986]) ).
tcf(c_6983,plain,
! [X0: $i] :
( ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_6982]) ).
tcf(c_6986,plain,
! [X0: $i] :
( ( sK3(X0) = X0 )
| ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater(X0,sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_3107,c_6983]) ).
tcf(c_7047,plain,
( ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(efficient_producers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater(equilibrium(sK2),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_71,c_6986]) ).
tcf(c_7067,plain,
( greater(sK0(sK2),equilibrium(sK2))
| ( equilibrium(sK2) = sK0(sK2) )
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(efficient_producers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_6878,c_7047]) ).
tcf(c_7153,plain,
( greater(sK0(sK2),equilibrium(sK2))
| ( sK3(equilibrium(sK2)) = sK0(sK2) )
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ in_environment(sK2,sK3(equilibrium(sK2))) ),
inference(superposition,[status(thm)],[c_6873,c_6978]) ).
tcf(c_7292,plain,
! [X0: $i,X1: $i] :
( ( X1 = growth_rate(efficient_producers,sK3(sK0(sK2))) )
| ( X1 != X0 )
| ( growth_rate(efficient_producers,sK3(sK0(sK2))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2663]) ).
tcf(c_7293,plain,
( ( zero = growth_rate(efficient_producers,sK3(sK0(sK2))) )
| ( zero != zero )
| ( growth_rate(efficient_producers,sK3(sK0(sK2))) != zero ) ),
inference(instantiation,[status(thm)],[c_7292]) ).
tcf(c_7540,plain,
( greater(sK0(sK2),equilibrium(sK2))
| ~ in_environment(sK2,equilibrium(sK2))
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_7153,c_72,c_74,c_330,c_2675,c_2958,c_2957,c_2956,c_2993,c_3098,c_3217,c_3470,c_5082,c_6270,c_6975,c_7293]) ).
tcf(c_7541,plain,
( greater(sK0(sK2),equilibrium(sK2))
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_7540]) ).
tcf(c_7895,plain,
( greater_or_equal(sK3(sK1(sK2)),sK0(sK2))
| ~ greater_or_equal(sK1(sK2),sK0(sK2))
| ( sK0(sK2) != sK0(sK2) )
| ( sK3(sK1(sK2)) != sK1(sK2) ) ),
inference(instantiation,[status(thm)],[c_4706]) ).
tcf(c_8289,plain,
( in_environment(sK2,equilibrium(sK2))
| ~ in_environment(sK2,sK1(sK2))
| ( sK2 != sK2 )
| ( equilibrium(sK2) != sK1(sK2) ) ),
inference(instantiation,[status(thm)],[c_4515]) ).
tcf(c_8555,plain,
! [X0: $i] :
( greater(sK0(sK2),equilibrium(sK2))
| ~ greater(X0,equilibrium(sK2))
| ~ greater(sK0(sK2),X0) ),
inference(instantiation,[status(thm)],[c_4897]) ).
tcf(c_9132,plain,
equilibrium(sK2) = equilibrium(sK2),
inference(instantiation,[status(thm)],[c_2661]) ).
tcf(c_11232,plain,
! [X0: $i,X1: $i] :
( greater(X1,X0)
| greater(X1,sK1(sK2))
| greater(sK1(sK2),X1)
| ~ in_environment(sK2,X1)
| ~ greater(sK1(sK2),X0) ),
inference(resolution,[status(thm)],[c_4389,c_5422]) ).
tcf(c_11309,plain,
( greater(sK3(sK0(sK2)),equilibrium(sK2))
| ~ greater(sK0(sK2),equilibrium(sK2))
| ( equilibrium(sK2) != equilibrium(sK2) )
| ( sK3(sK0(sK2)) != sK0(sK2) ) ),
inference(instantiation,[status(thm)],[c_5362]) ).
tcf(c_11553,plain,
( greater(sK1(sK2),equilibrium(sK2))
| ( equilibrium(sK2) = sK1(sK2) ) ),
inference(superposition,[status(thm)],[c_302,c_53]) ).
tcf(c_11593,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(first_movers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3162,c_6027]) ).
tcf(c_11594,plain,
! [X0: $i] :
( ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_11593]) ).
tcf(c_11595,plain,
( ( growth_rate(first_movers,sK3(sK0(sK2))) = zero )
| ~ in_environment(sK2,sK0(sK2))
| ~ greater_or_equal(sK3(sK0(sK2)),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_71,c_11594]) ).
tcf(c_11597,plain,
! [X0: $i] :
( ( sK3(X0) = X0 )
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater(X0,sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_3107,c_11594]) ).
tcf(c_11598,plain,
~ greater_or_equal(sK3(sK0(sK2)),equilibrium(sK2)),
inference(global_subsumption_just,[status(thm)],[c_11595,c_72,c_74,c_330,c_2675,c_2958,c_2957,c_2956,c_2993,c_3470,c_5082,c_6270,c_7293]) ).
tcf(c_11600,plain,
( ( sK3(sK0(sK2)) = sK0(sK2) )
| ~ in_environment(sK2,sK0(sK2))
| ~ greater(sK0(sK2),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_3107,c_11598]) ).
tcf(c_11601,plain,
~ greater(sK0(sK2),equilibrium(sK2)),
inference(global_subsumption_just,[status(thm)],[c_11600,c_72,c_330,c_2985,c_9132,c_11309,c_11598,c_11600]) ).
tcf(c_11649,plain,
! [X0: $i] :
( ~ greater_or_equal(sK3(X0),equilibrium(sK2))
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ in_environment(sK2,X0)
| ( growth_rate(efficient_producers,sK3(X0)) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_3163,c_795,c_3163,c_3986]) ).
tcf(c_11650,plain,
! [X0: $i] :
( ( growth_rate(efficient_producers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater_or_equal(sK3(X0),sK0(sK2))
| ~ greater_or_equal(sK3(X0),equilibrium(sK2)) ),
inference(renaming,[status(thm)],[c_11649]) ).
tcf(c_11669,plain,
! [X0: $i,X1: $i] :
( greater(X1,X0)
| greater(sK1(sK2),X1)
| ~ greater(sK1(sK2),X0)
| ~ in_environment(sK2,X1) ),
inference(global_subsumption_just,[status(thm)],[c_3185,c_5492,c_11232]) ).
tcf(c_11670,plain,
! [X0: $i,X1: $i] :
( greater(X1,X0)
| greater(sK1(sK2),X1)
| ~ in_environment(sK2,X1)
| ~ greater(sK1(sK2),X0) ),
inference(renaming,[status(thm)],[c_11669]) ).
tcf(c_11671,plain,
! [X0: $i] :
( greater(X0,equilibrium(sK2))
| greater(sK1(sK2),X0)
| ( equilibrium(sK2) = sK1(sK2) )
| ~ in_environment(sK2,X0) ),
inference(superposition,[status(thm)],[c_11553,c_11670]) ).
tcf(c_11895,plain,
( greater(sK1(sK2),sK0(sK2))
| ( equilibrium(sK2) = sK1(sK2) )
| ~ in_environment(sK2,sK0(sK2)) ),
inference(superposition,[status(thm)],[c_11671,c_11601]) ).
tcf(c_11913,plain,
( greater(sK1(sK2),sK0(sK2))
| ( equilibrium(sK2) = sK1(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_11895,c_72,c_330,c_11895]) ).
tcf(c_11919,plain,
( greater_or_equal(sK1(sK2),sK0(sK2))
| ( equilibrium(sK2) = sK1(sK2) ) ),
inference(superposition,[status(thm)],[c_11913,c_51]) ).
tcf(c_11955,plain,
( ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater(equilibrium(sK2),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_71,c_11597]) ).
tcf(c_11956,plain,
( ( equilibrium(sK2) = sK1(sK2) )
| ( sK3(sK1(sK2)) = sK1(sK2) )
| ( growth_rate(first_movers,sK3(sK1(sK2))) = zero )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater(sK1(sK2),sK0(sK2))
| ~ greater(equilibrium(sK2),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_5056,c_11597]) ).
tcf(c_11957,plain,
! [X0: $i] :
( ( sK3(X0) = X0 )
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater(X0,sK0(sK2))
| ~ greater(X0,equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_3107,c_11597]) ).
tcf(c_11978,plain,
! [X0: $i] :
( ( sK3(X0) = X0 )
| ( growth_rate(first_movers,sK3(X0)) = zero )
| ~ in_environment(sK2,X0)
| ~ greater(X0,equilibrium(sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_11957,c_72,c_74,c_330,c_2675,c_2958,c_2957,c_2956,c_2985,c_2993,c_3054,c_3098,c_3207,c_3470,c_3851,c_5082,c_5362,c_5424,c_6270,c_6962,c_7293,c_8555,c_9132,c_11309,c_11600]) ).
tcf(c_11983,plain,
( ( equilibrium(sK2) = sK1(sK2) )
| ( sK3(sK1(sK2)) = sK1(sK2) )
| ( growth_rate(first_movers,sK3(sK1(sK2))) = zero )
| ~ in_environment(sK2,sK1(sK2)) ),
inference(superposition,[status(thm)],[c_11553,c_11978]) ).
tcf(c_12004,plain,
( ( equilibrium(sK2) = sK1(sK2) )
| ( growth_rate(first_movers,sK3(sK1(sK2))) = zero ) ),
inference(global_subsumption_just,[status(thm)],[c_11956,c_72,c_301,c_308,c_330,c_2948,c_2947,c_2982,c_2995,c_3983,c_4444,c_4531,c_4805,c_5032,c_7895,c_9132,c_11895,c_11919,c_11983]) ).
tcf(c_12019,plain,
( greater_or_equal(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ( equilibrium(sK2) = sK1(sK2) )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_12004,c_3011]) ).
tcf(c_12022,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ( equilibrium(sK2) = sK1(sK2) )
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(sK3(sK1(sK2)),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_12004,c_716]) ).
tcf(c_12023,plain,
( ( equilibrium(sK2) = sK1(sK2) )
| ~ greater(zero,zero)
| ~ in_environment(sK2,sK1(sK2))
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(sK1(sK2))),zero) ),
inference(superposition,[status(thm)],[c_12004,c_373]) ).
tcf(c_12025,plain,
( ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_11955,c_72,c_74,c_330,c_2675,c_2958,c_2957,c_2956,c_2985,c_2993,c_3470,c_5082,c_6270,c_7293,c_7541,c_9132,c_11309,c_11600]) ).
tcf(c_12027,plain,
( ( equilibrium(sK2) = sK1(sK2) )
| ~ greater(zero,zero) ),
inference(global_subsumption_just,[status(thm)],[c_12023,c_72,c_308,c_330,c_2995,c_3983,c_4531,c_7895,c_11895,c_11919,c_12023,c_12019]) ).
tcf(c_12029,plain,
( greater(growth_rate(efficient_producers,sK3(sK1(sK2))),zero)
| ( equilibrium(sK2) = sK1(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_12022,c_72,c_301,c_308,c_330,c_2675,c_2948,c_2947,c_2995,c_3045,c_3371,c_3983,c_4531,c_4804,c_5032,c_5458,c_5571,c_7895,c_9132,c_11895,c_11919,c_12022,c_12019,c_12027]) ).
tcf(c_12031,plain,
equilibrium(sK2) = sK1(sK2),
inference(global_subsumption_just,[status(thm)],[c_12029,c_72,c_301,c_308,c_2675,c_2946,c_3045,c_3371,c_5032,c_5458,c_5569,c_5571,c_9132,c_12027,c_12029]) ).
tcf(c_12056,plain,
in_environment(sK2,equilibrium(sK2)),
inference(superposition,[status(thm)],[c_12031,c_309]) ).
tcf(c_12071,plain,
( ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero ) ),
inference(superposition,[status(thm)],[c_12056,c_12025]) ).
tcf(c_12089,plain,
( greater_or_equal(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_12071,c_3011]) ).
tcf(c_12091,plain,
( greater(zero,zero)
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(efficient_producers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_12071,c_1530]) ).
tcf(c_12092,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_12071,c_716]) ).
tcf(c_12093,plain,
( ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ~ greater(zero,zero)
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero) ),
inference(superposition,[status(thm)],[c_12071,c_373]) ).
tcf(c_12095,plain,
( ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ~ greater(zero,zero) ),
inference(global_subsumption_just,[status(thm)],[c_12093,c_72,c_74,c_301,c_308,c_330,c_2675,c_2948,c_2947,c_2958,c_2957,c_2956,c_2985,c_2993,c_2995,c_3045,c_3098,c_3217,c_3371,c_3470,c_3983,c_4531,c_4804,c_5032,c_5082,c_5458,c_5571,c_6270,c_6293,c_6846,c_7293,c_7895,c_8289,c_9132,c_11309,c_11600,c_11895,c_11919,c_12022,c_12019,c_12027,c_12093,c_12089]) ).
tcf(c_12097,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_12092,c_72,c_74,c_301,c_308,c_330,c_2675,c_2948,c_2947,c_2958,c_2957,c_2956,c_2985,c_2993,c_2995,c_3045,c_3098,c_3217,c_3371,c_3470,c_3983,c_4531,c_4804,c_5032,c_5082,c_5458,c_5571,c_6270,c_6293,c_6846,c_7293,c_7895,c_8289,c_9132,c_11309,c_11600,c_11895,c_11919,c_12022,c_12019,c_12027,c_12092]) ).
tcf(c_12177,plain,
( ( growth_rate(efficient_producers,sK3(equilibrium(sK2))) = zero )
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_12091,c_72,c_308,c_330,c_2958,c_2995,c_3098,c_3217,c_7067,c_8289,c_11598,c_11601,c_12031]) ).
tcf(c_12178,plain,
( ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ( growth_rate(efficient_producers,sK3(equilibrium(sK2))) = zero ) ),
inference(renaming,[status(thm)],[c_12177]) ).
tcf(c_12201,plain,
( greater(zero,growth_rate(first_movers,sK3(equilibrium(sK2))))
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_12178,c_716]) ).
tcf(c_12203,plain,
( greater(zero,zero)
| ( sK3(equilibrium(sK2)) = equilibrium(sK2) ) ),
inference(superposition,[status(thm)],[c_12178,c_12097]) ).
tcf(c_12205,plain,
sK3(equilibrium(sK2)) = equilibrium(sK2),
inference(global_subsumption_just,[status(thm)],[c_12201,c_12095,c_12203]) ).
tcf(c_12233,plain,
( ( growth_rate(efficient_producers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(equilibrium(sK2),sK0(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_12205,c_11650]) ).
tcf(c_12235,plain,
( ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(equilibrium(sK2),sK0(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_12205,c_11594]) ).
tcf(c_12249,plain,
( greater(growth_rate(first_movers,equilibrium(sK2)),zero)
| ( growth_rate(first_movers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_12205,c_1540]) ).
tcf(c_12278,plain,
growth_rate(first_movers,sK3(equilibrium(sK2))) = zero,
inference(global_subsumption_just,[status(thm)],[c_12249,c_72,c_74,c_301,c_308,c_330,c_2675,c_2948,c_2947,c_2958,c_2957,c_2956,c_2985,c_2993,c_2995,c_3045,c_3098,c_3217,c_3371,c_3470,c_3983,c_4531,c_4804,c_5032,c_5082,c_5458,c_5571,c_5853,c_5997,c_6270,c_6531,c_7293,c_7895,c_8289,c_9132,c_11309,c_11600,c_11895,c_11919,c_12022,c_12019,c_12027,c_12235]) ).
tcf(c_12296,plain,
( greater(zero,zero)
| ( growth_rate(efficient_producers,sK3(equilibrium(sK2))) = zero )
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),equilibrium(sK2)) ),
inference(superposition,[status(thm)],[c_12278,c_1530]) ).
tcf(c_12297,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_12278,c_716]) ).
tcf(c_12298,plain,
( ~ greater(zero,zero)
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero) ),
inference(superposition,[status(thm)],[c_12278,c_373]) ).
tcf(c_12300,plain,
( ~ greater(zero,zero)
| ~ greater_or_equal(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero) ),
inference(global_subsumption_just,[status(thm)],[c_12298,c_72,c_301,c_308,c_330,c_2675,c_2948,c_2947,c_2995,c_3045,c_3371,c_3983,c_4531,c_4804,c_5032,c_5458,c_5571,c_7895,c_8289,c_9132,c_11895,c_11919,c_12022,c_12019,c_12027,c_12298]) ).
tcf(c_12366,plain,
( greater(growth_rate(efficient_producers,sK3(equilibrium(sK2))),zero)
| ~ greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_12297,c_72,c_301,c_308,c_330,c_2675,c_2948,c_2947,c_2995,c_3045,c_3371,c_3983,c_4531,c_4804,c_5032,c_5458,c_5571,c_7895,c_8289,c_9132,c_11895,c_11919,c_12022,c_12019,c_12027,c_12297]) ).
tcf(c_12424,plain,
growth_rate(efficient_producers,sK3(equilibrium(sK2))) = zero,
inference(global_subsumption_just,[status(thm)],[c_12296,c_72,c_74,c_301,c_308,c_330,c_2675,c_2948,c_2947,c_2958,c_2957,c_2956,c_2985,c_2993,c_2995,c_3045,c_3098,c_3217,c_3371,c_3470,c_3983,c_4531,c_4804,c_5032,c_5082,c_5458,c_5571,c_5853,c_5997,c_6270,c_6531,c_7293,c_7895,c_8289,c_9132,c_11309,c_11600,c_11895,c_11919,c_12022,c_12019,c_12027,c_12233]) ).
tcf(c_12453,plain,
( greater(zero,growth_rate(first_movers,sK3(equilibrium(sK2))))
| ~ in_environment(sK2,equilibrium(sK2))
| ~ greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_12424,c_716]) ).
tcf(c_12454,plain,
( greater(zero,zero)
| ~ greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2)) ),
inference(superposition,[status(thm)],[c_12424,c_12366]) ).
tcf(c_12455,plain,
( ~ greater_or_equal(zero,zero)
| ~ greater(zero,zero) ),
inference(superposition,[status(thm)],[c_12424,c_12300]) ).
tcf(c_12589,plain,
~ greater_or_equal(sK3(equilibrium(sK2)),sK0(sK2)),
inference(global_subsumption_just,[status(thm)],[c_12453,c_74,c_12455,c_12454]) ).
tcf(c_12593,plain,
~ greater_or_equal(equilibrium(sK2),sK0(sK2)),
inference(superposition,[status(thm)],[c_12205,c_12589]) ).
tcf(c_12594,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_12593,c_12031,c_11601,c_11598,c_9132,c_8289,c_6531,c_5997,c_3217,c_3098,c_2995,c_2958,c_330,c_308,c_72]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT035+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.36 % Computer : n009.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Thu Sep 24 01:07:45 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 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.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 8.19/1.72 % SZS status Started for theBenchmark.p
% 8.19/1.72 % SZS status Theorem for theBenchmark.p
% 8.19/1.72
% 8.19/1.72 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.19/1.72
% 8.19/1.72 % ------ iProver source info
% 8.19/1.72
% 8.19/1.72 % git: date: 2026-07-19 20:42:38 +0200
% 8.19/1.72 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.19/1.72 % git: non_committed_changes: false
% 8.19/1.72
% 8.19/1.72 % ------ Parsing...
% 8.19/1.72 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.19/1.72
% 8.19/1.72 % ------ 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 %
% 8.19/1.72
% 8.19/1.72 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.19/1.72
% 8.19/1.72 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.19/1.72 % ------ Proving...
% 8.19/1.72 % ------ Problem Properties
% 8.19/1.72
% 8.19/1.72 %
% 8.19/1.72 % clauses 15
% 8.19/1.72 % conjectures 1
% 8.19/1.72 % EPR 5
% 8.19/1.72 % Horn 9
% 8.19/1.72 % unary 4
% 8.19/1.72 % binary 2
% 8.19/1.72 % lits 41
% 8.19/1.72 % lits eq 6
% 8.19/1.72 % fd_pure 0
% 8.19/1.72 % fd_pseudo 0
% 8.19/1.72 % fd_cond 0
% 8.19/1.72 % fd_pseudo_cond 2
% 8.19/1.72 % AC symbols 0
% 8.19/1.72
% 8.19/1.72 % ------ Input Options Time Limit: Unbounded
% 8.19/1.72
% 8.19/1.72
% 8.19/1.72 % ------
% 8.19/1.72 % Current options:
% 8.19/1.72 % ------
% 8.19/1.72
% 8.19/1.72
% 8.19/1.72 %
% 8.19/1.72
% 8.19/1.72 % ------ Proving...
% 8.19/1.72 %
% 8.19/1.72
% 8.19/1.72 % SZS status Theorem for theBenchmark.p
% 8.19/1.72
% 8.19/1.72 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.19/1.72
% 8.19/1.72
%------------------------------------------------------------------------------