%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : MGT039-2 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n008.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:42 PM UTC 2026
% Result : Unsatisfiable 3.51s 1.72s
% Output : CNFRefutation 3.51s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] :
( selection_favors(X2,X1,X3)
| ~ greater(growth_rate(X2,X3),growth_rate(X1,X3))
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp1_high_growth_rates_33) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( selection_favors(X1,X3,X2)
| cardinality_at_time(X3,X2) != zero
| ~ greater(cardinality_at_time(X1,X2),zero)
| ~ subpopulation(X3,X0,X2)
| ~ subpopulation(X1,X0,X2)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp2_favour_members_34) ).
fof(f3,plain,
! [X2,X3,X0,X1] :
( selection_favors(X1,X3,X2)
| zero != cardinality_at_time(X3,X2)
| ~ greater(cardinality_at_time(X1,X2),zero)
| ~ subpopulation(X3,X0,X2)
| ~ subpopulation(X1,X0,X2)
| ~ environment(X0) ),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| environment(sk1(X0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_favoured_trategy_35) ).
fof(f5,axiom,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sk1(X0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_favoured_trategy_36) ).
fof(f6,axiom,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(X0)))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_favoured_trategy_37) ).
fof(f7,axiom,
! [X0,X1] :
( in_environment(X1,sk2(X1,X0))
| ~ in_environment(X0,X1)
| ~ environment(X1)
| ~ slow_change(X0)
| ~ observational_period(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp4_critical_point_38) ).
fof(f8,axiom,
! [X0,X1] :
( greater(sk2(X1,X0),critical_point(X1))
| ~ in_environment(X0,X1)
| ~ environment(X1)
| ~ slow_change(X0)
| ~ observational_period(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp4_critical_point_39) ).
fof(f9,axiom,
propagation_strategy(first_movers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_organizational_sets1_40) ).
fof(f10,axiom,
propagation_strategy(efficient_producers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_organizational_sets2_41) ).
fof(f11,axiom,
! [X0,X1] :
( in_environment(X0,X1)
| ~ greater_or_equal(end_time(X0),X1)
| ~ greater_or_equal(X1,start_time(X0))
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_time_in_environment_42) ).
fof(f12,axiom,
! [X0,X1] :
( greater_or_equal(end_time(X0),X1)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_environment_end_point_43) ).
fof(f13,axiom,
! [X0,X1] :
( subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_contains_FM_and_EP_44) ).
fof(f14,axiom,
! [X0,X1] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_first_movers_exist_45) ).
fof(f15,axiom,
! [X0,X1] :
( subpopulation(first_movers,X0,X1)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_subpopulations_46) ).
fof(f16,axiom,
! [X0,X1] :
( subpopulation(efficient_producers,X0,X1)
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_subpopulations_47) ).
fof(f17,axiom,
! [X0] :
( greater_or_equal(critical_point(X0),appear(efficient_producers,X0))
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_critical_point_after_EP_48) ).
fof(f18,axiom,
! [X0] :
( greater_or_equal(critical_point(X0),start_time(X0))
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_time_of_critical_point_49) ).
fof(f19,axiom,
! [X2,X0,X1] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity_50) ).
fof(f21,axiom,
! [X0,X1] :
( X0 = X1
| greater(X0,X1)
| ~ greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_52) ).
fof(f22,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_53) ).
fof(f23,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
| X0 != X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_54) ).
fof(f26,axiom,
! [X2,X0,X1] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ greater(X2,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| X1 != critical_point(X0)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_56) ).
fof(f27,plain,
! [X2,X0,X1] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ greater(X2,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| critical_point(X0) != X1
| ~ environment(X0) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,axiom,
! [X0,X1] :
( greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater_or_equal(X1,appear(efficient_producers,X0))
| ~ in_environment(X0,X1)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_57) ).
fof(f29,negated_conjecture,
observational_period(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t8_58) ).
fof(f30,negated_conjecture,
slow_change(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t8_59) ).
fof(f31,negated_conjecture,
~ selection_favors(efficient_producers,first_movers,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t8_60) ).
fof(f32,plain,
! [X1] : greater_or_equal(X1,X1),
inference(equality_resolution,[],[f23]) ).
fof(f34,plain,
! [X2,X0] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ greater(X2,critical_point(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ environment(X0) ),
inference(equality_resolution,[],[f27]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( selection_favors(X0,X2,X1)
| ~ environment(X3)
| ~ subpopulations(X2,X0,X3,X1)
| ~ greater(growth_rate(X0,X1),growth_rate(X2,X1)) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( selection_favors(X2,X0,X1)
| ~ environment(X3)
| ~ subpopulation(X2,X3,X1)
| ~ subpopulation(X0,X3,X1)
| ~ greater(cardinality_at_time(X2,X1),zero)
| ( cardinality_at_time(X0,X1) != zero ) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_79,plain,
! [X0: $i] :
( environment(sk1(X0))
| selection_favors(efficient_producers,first_movers,X0)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_80,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sk1(X0))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_81,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(X0))) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i] :
( in_environment(X1,sk2(X1,X0))
| ~ slow_change(X0)
| ~ observational_period(X0)
| ~ environment(X1)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i] :
( greater(sk2(X1,X0),critical_point(X1))
| ~ slow_change(X0)
| ~ observational_period(X0)
| ~ environment(X1)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_84,plain,
propagation_strategy(first_movers),
inference(cnf_transformation,[],[f9]) ).
tcf(c_85,plain,
propagation_strategy(efficient_producers),
inference(cnf_transformation,[],[f10]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i] :
( in_environment(X0,X1)
| ~ environment(X0)
| ~ greater_or_equal(X1,start_time(X0))
| ~ greater_or_equal(end_time(X0),X1) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(end_time(X0),X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( subpopulations(first_movers,efficient_producers,X1,X0)
| ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i] :
( subpopulation(first_movers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] :
( subpopulation(efficient_producers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_92,plain,
! [X0: $i] :
( greater_or_equal(critical_point(X0),appear(efficient_producers,X0))
| ~ environment(X0) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_93,plain,
! [X0: $i] :
( greater_or_equal(critical_point(X0),start_time(X0))
| ~ environment(X0) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i] :
( greater(X0,X1)
| ( X0 = X1 )
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_98,plain,
! [X0: $i] : greater_or_equal(X0,X0),
inference(cnf_transformation,[],[f32]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ environment(X0)
| ~ greater(X1,critical_point(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater_or_equal(X0,appear(efficient_producers,X1)) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_102,negated_conjecture,
observational_period(sk3),
inference(cnf_transformation,[],[f29]) ).
tcf(c_103,negated_conjecture,
slow_change(sk3),
inference(cnf_transformation,[],[f30]) ).
tcf(c_104,negated_conjecture,
~ selection_favors(efficient_producers,first_movers,sk3),
inference(cnf_transformation,[],[f31]) ).
tcf(c_126,plain,
! [X0: $i] :
( environment(sk1(X0))
| selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0) ),
inference(global_subsumption_just,[status(thm)],[c_79,c_85,c_84,c_79]) ).
tcf(c_129,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sk1(X0))
| ~ observational_period(X0) ),
inference(global_subsumption_just,[status(thm)],[c_80,c_85,c_84,c_80]) ).
tcf(c_132,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_81,c_85,c_84,c_81]) ).
tcf(c_466,plain,
! [X0: $i,X1: $i] :
( greater(sk2(X1,X0),critical_point(X1))
| ~ observational_period(X0)
| ~ environment(X1)
| ~ in_environment(X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_83,c_103]) ).
tcf(c_467,plain,
! [X0: $i] :
( greater(sk2(X0,sk3),critical_point(X0))
| ~ observational_period(sk3)
| ~ environment(X0)
| ~ in_environment(sk3,X0) ),
inference(unflattening,[status(thm)],[c_466]) ).
tcf(c_469,plain,
! [X0: $i] :
( greater(sk2(X0,sk3),critical_point(X0))
| ~ in_environment(sk3,X0)
| ~ environment(X0) ),
inference(global_subsumption_just,[status(thm)],[c_467,c_102,c_467]) ).
tcf(c_470,plain,
! [X0: $i] :
( greater(sk2(X0,sk3),critical_point(X0))
| ~ environment(X0)
| ~ in_environment(sk3,X0) ),
inference(renaming,[status(thm)],[c_469]) ).
tcf(c_481,plain,
! [X0: $i,X1: $i] :
( in_environment(X1,sk2(X1,X0))
| ~ observational_period(X0)
| ~ environment(X1)
| ~ in_environment(X0,X1)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_82,c_103]) ).
tcf(c_482,plain,
! [X0: $i] :
( in_environment(X0,sk2(X0,sk3))
| ~ observational_period(sk3)
| ~ environment(X0)
| ~ in_environment(sk3,X0) ),
inference(unflattening,[status(thm)],[c_481]) ).
tcf(c_484,plain,
! [X0: $i] :
( in_environment(X0,sk2(X0,sk3))
| ~ in_environment(sk3,X0)
| ~ environment(X0) ),
inference(global_subsumption_just,[status(thm)],[c_482,c_102,c_482]) ).
tcf(c_485,plain,
! [X0: $i] :
( in_environment(X0,sk2(X0,sk3))
| ~ environment(X0)
| ~ in_environment(sk3,X0) ),
inference(renaming,[status(thm)],[c_484]) ).
tcf(c_502,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(X0)))
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_132,c_102]) ).
tcf(c_503,plain,
( selection_favors(efficient_producers,first_movers,sk3)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(sk3))) ),
inference(unflattening,[status(thm)],[c_502]) ).
tcf(c_504,plain,
~ selection_favors(efficient_producers,first_movers,end_time(sk1(sk3))),
inference(global_subsumption_just,[status(thm)],[c_503,c_104,c_503]) ).
tcf(c_509,plain,
! [X0: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| in_environment(X0,sk1(X0))
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_129,c_102]) ).
tcf(c_510,plain,
( in_environment(sk3,sk1(sk3))
| selection_favors(efficient_producers,first_movers,sk3) ),
inference(unflattening,[status(thm)],[c_509]) ).
tcf(c_516,plain,
! [X0: $i] :
( environment(sk1(X0))
| selection_favors(efficient_producers,first_movers,X0)
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_126,c_102]) ).
tcf(c_517,plain,
( environment(sk1(sk3))
| selection_favors(efficient_producers,first_movers,sk3) ),
inference(unflattening,[status(thm)],[c_516]) ).
tcf(c_518,plain,
environment(sk1(sk3)),
inference(global_subsumption_just,[status(thm)],[c_517,c_104,c_517]) ).
tcf(c_526,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( selection_favors(X0,X3,X1)
| ~ environment(X5)
| ~ environment(X4)
| ~ in_environment(X5,X2)
| ~ greater(cardinality_at_time(efficient_producers,X2),zero)
| ~ greater(cardinality_at_time(first_movers,X2),zero)
| ~ greater(growth_rate(X0,X1),growth_rate(X3,X1))
| ( X4 != X5 )
| ( X3 != first_movers )
| ( X1 != X2 )
| ( X0 != efficient_producers ) ),
inference(resolution_lifted,[status(thm)],[c_77,c_88]) ).
tcf(c_527,plain,
! [X0: $i,X1: $i] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(unflattening,[status(thm)],[c_526]) ).
tcf(c_547,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ environment(X1)
| ~ environment(X0)
| ~ in_environment(X1,X3)
| ~ greater(X2,critical_point(X0))
| ~ greater(cardinality_at_time(efficient_producers,X3),zero)
| ~ greater(cardinality_at_time(first_movers,X3),zero)
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_100,c_88]) ).
tcf(c_548,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater(X0,critical_point(X1))
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero) ),
inference(unflattening,[status(thm)],[c_547]) ).
tcf(c_598,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ environment(X3)
| ~ subpopulation(X2,X3,X1)
| ~ subpopulation(X0,X3,X1)
| ~ greater(cardinality_at_time(X2,X1),zero)
| ( X2 != efficient_producers )
| ( X0 != first_movers )
| ( end_time(sk1(sk3)) != X1 )
| ( cardinality_at_time(X0,X1) != zero ) ),
inference(resolution_lifted,[status(thm)],[c_78,c_504]) ).
tcf(c_599,plain,
! [X0: $i] :
( ~ environment(X0)
| ~ subpopulation(efficient_producers,X0,end_time(sk1(sk3)))
| ~ subpopulation(first_movers,X0,end_time(sk1(sk3)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)
| ( cardinality_at_time(first_movers,end_time(sk1(sk3))) != zero ) ),
inference(unflattening,[status(thm)],[c_598]) ).
tcf(c_634,plain,
! [X0: $i,X1: $i] :
( ~ environment(X1)
| ~ in_environment(X1,X0)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ( efficient_producers != efficient_producers )
| ( first_movers != first_movers )
| ( end_time(sk1(sk3)) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_527,c_504]) ).
tcf(c_635,plain,
! [X0: $i] :
( ~ environment(X0)
| ~ in_environment(X0,end_time(sk1(sk3)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))) ),
inference(unflattening,[status(thm)],[c_634]) ).
tcf(c_672,plain,
! [X0: $i] :
( ~ in_environment(X0,end_time(sk1(sk3)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_635,c_518]) ).
tcf(c_673,plain,
( ~ in_environment(sk1(sk3),end_time(sk1(sk3)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)
| ~ greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)
| ~ greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))) ),
inference(unflattening,[status(thm)],[c_672]) ).
tcf(c_700,plain,
! [X0: $i] :
( ~ subpopulation(efficient_producers,X0,end_time(sk1(sk3)))
| ~ subpopulation(first_movers,X0,end_time(sk1(sk3)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)
| ( sk1(sk3) != X0 )
| ( cardinality_at_time(first_movers,end_time(sk1(sk3))) != zero ) ),
inference(resolution_lifted,[status(thm)],[c_599,c_518]) ).
tcf(c_701,plain,
( ~ subpopulation(efficient_producers,sk1(sk3),end_time(sk1(sk3)))
| ~ subpopulation(first_movers,sk1(sk3),end_time(sk1(sk3)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)
| ( cardinality_at_time(first_movers,end_time(sk1(sk3))) != zero ) ),
inference(unflattening,[status(thm)],[c_700]) ).
tcf(c_728,plain,
! [X0: $i] :
( in_environment(X0,sk2(X0,sk3))
| ~ in_environment(sk3,X0)
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_485,c_518]) ).
tcf(c_729,plain,
( in_environment(sk1(sk3),sk2(sk1(sk3),sk3))
| ~ in_environment(sk3,sk1(sk3)) ),
inference(unflattening,[status(thm)],[c_728]) ).
tcf(c_730,plain,
in_environment(sk1(sk3),sk2(sk1(sk3),sk3)),
inference(global_subsumption_just,[status(thm)],[c_729,c_104,c_510,c_729]) ).
tcf(c_735,plain,
! [X0: $i] :
( greater(sk2(X0,sk3),critical_point(X0))
| ~ in_environment(sk3,X0)
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_470,c_518]) ).
tcf(c_736,plain,
( greater(sk2(sk1(sk3),sk3),critical_point(sk1(sk3)))
| ~ in_environment(sk3,sk1(sk3)) ),
inference(unflattening,[status(thm)],[c_735]) ).
tcf(c_737,plain,
greater(sk2(sk1(sk3),sk3),critical_point(sk1(sk3))),
inference(global_subsumption_just,[status(thm)],[c_736,c_104,c_510,c_736]) ).
tcf(c_747,plain,
! [X0: $i] :
( greater_or_equal(critical_point(X0),start_time(X0))
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_93,c_518]) ).
tcf(c_748,plain,
greater_or_equal(critical_point(sk1(sk3)),start_time(sk1(sk3))),
inference(unflattening,[status(thm)],[c_747]) ).
tcf(c_752,plain,
! [X0: $i] :
( greater_or_equal(critical_point(X0),appear(efficient_producers,X0))
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_92,c_518]) ).
tcf(c_753,plain,
greater_or_equal(critical_point(sk1(sk3)),appear(efficient_producers,sk1(sk3))),
inference(unflattening,[status(thm)],[c_752]) ).
tcf(c_757,plain,
! [X0: $i,X1: $i] :
( subpopulation(efficient_producers,X0,X1)
| ~ in_environment(X0,X1)
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_91,c_518]) ).
tcf(c_758,plain,
! [X0: $i] :
( subpopulation(efficient_producers,sk1(sk3),X0)
| ~ in_environment(sk1(sk3),X0) ),
inference(unflattening,[status(thm)],[c_757]) ).
tcf(c_766,plain,
! [X0: $i,X1: $i] :
( subpopulation(first_movers,X0,X1)
| ~ in_environment(X0,X1)
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_90,c_518]) ).
tcf(c_767,plain,
! [X0: $i] :
( subpopulation(first_movers,sk1(sk3),X0)
| ~ in_environment(sk1(sk3),X0) ),
inference(unflattening,[status(thm)],[c_766]) ).
tcf(c_775,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_89,c_518]) ).
tcf(c_776,plain,
! [X0: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X0),zero)
| ~ in_environment(sk1(sk3),X0) ),
inference(unflattening,[status(thm)],[c_775]) ).
tcf(c_784,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(end_time(X0),X1)
| ~ in_environment(X0,X1)
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_87,c_518]) ).
tcf(c_785,plain,
! [X0: $i] :
( greater_or_equal(end_time(sk1(sk3)),X0)
| ~ in_environment(sk1(sk3),X0) ),
inference(unflattening,[status(thm)],[c_784]) ).
tcf(c_793,plain,
! [X0: $i,X1: $i] :
( in_environment(X0,X1)
| ~ greater_or_equal(X1,start_time(X0))
| ~ greater_or_equal(end_time(X0),X1)
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_86,c_518]) ).
tcf(c_794,plain,
! [X0: $i] :
( in_environment(sk1(sk3),X0)
| ~ greater_or_equal(X0,start_time(sk1(sk3)))
| ~ greater_or_equal(end_time(sk1(sk3)),X0) ),
inference(unflattening,[status(thm)],[c_793]) ).
tcf(c_805,plain,
! [X0: $i,X1: $i] :
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ in_environment(X0,X1)
| ~ greater(X1,critical_point(X0))
| ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_548,c_518]) ).
tcf(c_806,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ in_environment(sk1(sk3),X0)
| ~ greater(X0,critical_point(sk1(sk3)))
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero) ),
inference(unflattening,[status(thm)],[c_805]) ).
tcf(c_823,plain,
! [X0: $i,X1: $i] :
( greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ in_environment(X0,X1)
| ~ greater_or_equal(X1,appear(efficient_producers,X0))
| ( sk1(sk3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_101,c_518]) ).
tcf(c_824,plain,
! [X0: $i] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ in_environment(sk1(sk3),X0)
| ~ greater_or_equal(X0,appear(efficient_producers,sk1(sk3))) ),
inference(unflattening,[status(thm)],[c_823]) ).
tcf(c_1782,definition,
iPr_def_13 = appear(efficient_producers,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_1783,definition,
iPr_def_14 = critical_point(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_1786,definition,
iPr_def_17 = sk2(iPr_def_10,sk3),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_1789,definition,
iPr_def_20 = cardinality_at_time(first_movers,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_1790,definition,
iPr_def_21 = cardinality_at_time(efficient_producers,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_1793,definition,
iPr_def_24 = growth_rate(efficient_producers,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_1794,definition,
iPr_def_25 = growth_rate(first_movers,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_1796,plain,
! [X0: $i] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,iPr_def_13)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_824,c_1782]) ).
tcf(c_1797,plain,
! [X0: $i] :
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ in_environment(iPr_def_10,X0)
| ~ greater(X0,iPr_def_14)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero) ),
inference(demodulation,[status(thm)],[c_806,c_1783]) ).
tcf(c_1798,plain,
! [X0: $i] :
( in_environment(iPr_def_10,X0)
| ~ greater_or_equal(iPr_def_12,X0)
| ~ greater_or_equal(X0,iPr_def_11) ),
inference(demodulation,[status(thm)],[c_794]) ).
tcf(c_1799,plain,
! [X0: $i] :
( greater_or_equal(iPr_def_12,X0)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_785]) ).
tcf(c_1800,plain,
! [X0: $i] :
( greater_or_equal(cardinality_at_time(first_movers,X0),zero)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_776]) ).
tcf(c_1801,plain,
! [X0: $i] :
( subpopulation(first_movers,iPr_def_10,X0)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_767]) ).
tcf(c_1802,plain,
! [X0: $i] :
( subpopulation(efficient_producers,iPr_def_10,X0)
| ~ in_environment(iPr_def_10,X0) ),
inference(demodulation,[status(thm)],[c_758]) ).
tcf(c_1803,plain,
greater_or_equal(iPr_def_14,iPr_def_13),
inference(demodulation,[status(thm)],[c_753]) ).
tcf(c_1804,plain,
greater_or_equal(iPr_def_14,iPr_def_11),
inference(demodulation,[status(thm)],[c_748]) ).
tcf(c_1806,plain,
greater(iPr_def_17,iPr_def_14),
inference(demodulation,[status(thm)],[c_737,c_1786]) ).
tcf(c_1807,plain,
in_environment(iPr_def_10,iPr_def_17),
inference(demodulation,[status(thm)],[c_730]) ).
tcf(c_1809,plain,
( ~ greater(iPr_def_21,zero)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ( iPr_def_20 != zero ) ),
inference(demodulation,[status(thm)],[c_701,c_1790,c_1789]) ).
tcf(c_1811,plain,
( ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_20,zero) ),
inference(demodulation,[status(thm)],[c_673,c_1794,c_1793]) ).
tcf(c_2290,plain,
greater_or_equal(iPr_def_12,iPr_def_17),
inference(superposition,[status(thm)],[c_1807,c_1799]) ).
tcf(c_2315,plain,
( in_environment(iPr_def_10,iPr_def_12)
| ~ greater_or_equal(iPr_def_12,iPr_def_11) ),
inference(superposition,[status(thm)],[c_98,c_1798]) ).
tcf(c_2356,plain,
( greater_or_equal(iPr_def_20,zero)
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1789,c_1800]) ).
tcf(c_2359,plain,
( greater(iPr_def_21,zero)
| ~ greater_or_equal(iPr_def_12,iPr_def_13)
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1790,c_1796]) ).
tcf(c_2386,plain,
( greater(growth_rate(efficient_producers,iPr_def_12),iPr_def_25)
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_12,iPr_def_14)
| ~ greater(cardinality_at_time(efficient_producers,iPr_def_12),zero)
| ~ greater(cardinality_at_time(first_movers,iPr_def_12),zero) ),
inference(superposition,[status(thm)],[c_1794,c_1797]) ).
tcf(c_2387,plain,
( greater(iPr_def_24,iPr_def_25)
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_12,iPr_def_14) ),
inference(light_normalisation,[status(thm)],[c_2386,c_1789,c_1790,c_1793]) ).
tcf(c_2453,plain,
! [X0: $i] :
( greater_or_equal(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,iPr_def_13)
| ~ in_environment(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_1796,c_97]) ).
tcf(c_2455,plain,
greater_or_equal(iPr_def_17,iPr_def_14),
inference(superposition,[status(thm)],[c_1806,c_97]) ).
tcf(c_2474,plain,
! [X0: $i] :
( greater(iPr_def_17,X0)
| ~ greater(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1806,c_94]) ).
tcf(c_2497,plain,
! [X0: $i] :
( greater(cardinality_at_time(first_movers,X0),zero)
| ( cardinality_at_time(first_movers,X0) = zero )
| ~ in_environment(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_1800,c_96]) ).
tcf(c_2498,plain,
( greater(iPr_def_14,iPr_def_13)
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1803,c_96]) ).
tcf(c_2499,plain,
( greater(iPr_def_14,iPr_def_11)
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1804,c_96]) ).
tcf(c_2500,plain,
( greater(iPr_def_12,iPr_def_17)
| ( iPr_def_12 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2290,c_96]) ).
tcf(c_2522,plain,
( greater(iPr_def_17,iPr_def_13)
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2498,c_2474]) ).
tcf(c_2536,plain,
( greater(iPr_def_17,iPr_def_11)
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2499,c_2474]) ).
tcf(c_2550,plain,
! [X0: $i] :
( greater(iPr_def_12,X0)
| ( iPr_def_12 = iPr_def_17 )
| ~ greater(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_2500,c_94]) ).
tcf(c_2586,plain,
( greater_or_equal(iPr_def_21,zero)
| ~ greater_or_equal(iPr_def_12,iPr_def_13)
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1790,c_2453]) ).
tcf(c_2606,plain,
( greater(iPr_def_20,zero)
| ( cardinality_at_time(first_movers,iPr_def_12) = zero )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1789,c_2497]) ).
tcf(c_2610,plain,
( greater(iPr_def_20,zero)
| ( zero = iPr_def_20 )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_2606,c_1789]) ).
tcf(c_2819,plain,
( greater(iPr_def_12,iPr_def_14)
| ( iPr_def_12 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_1806,c_2550]) ).
tcf(c_2834,plain,
( greater_or_equal(iPr_def_17,iPr_def_13)
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2522,c_97]) ).
tcf(c_2835,plain,
( greater(iPr_def_12,iPr_def_13)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2522,c_2550]) ).
tcf(c_2853,plain,
( greater(iPr_def_12,iPr_def_11)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2536,c_2550]) ).
tcf(c_2870,plain,
( greater_or_equal(iPr_def_12,iPr_def_14)
| ( iPr_def_12 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2819,c_97]) ).
tcf(c_3026,plain,
( greater_or_equal(iPr_def_12,iPr_def_13)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2835,c_97]) ).
tcf(c_3048,plain,
( greater_or_equal(iPr_def_12,iPr_def_11)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2853,c_97]) ).
tcf(c_3074,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_20 = zero )
| ~ greater_or_equal(iPr_def_20,zero) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_3108,plain,
( ~ greater(iPr_def_12,iPr_def_14)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_21,zero)
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_2387,c_1811,c_2387]) ).
tcf(c_3109,plain,
( ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_12,iPr_def_14) ),
inference(renaming,[status(thm)],[c_3108]) ).
tcf(c_3466,plain,
( in_environment(iPr_def_10,iPr_def_12)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_3048,c_2315]) ).
tcf(c_3491,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_3466,c_2610]) ).
tcf(c_3492,plain,
( greater_or_equal(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ greater_or_equal(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_3466,c_2586]) ).
tcf(c_3493,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ greater_or_equal(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_3466,c_2359]) ).
tcf(c_3743,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_3026,c_3493]) ).
tcf(c_3947,plain,
( greater_or_equal(iPr_def_21,zero)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_3026,c_3492]) ).
tcf(c_4521,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_12,iPr_def_14) ),
inference(superposition,[status(thm)],[c_3743,c_3109]) ).
tcf(c_4522,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_20,zero) ),
inference(superposition,[status(thm)],[c_3743,c_1811]) ).
tcf(c_4613,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ greater(iPr_def_20,zero) ),
inference(global_subsumption_just,[status(thm)],[c_4522,c_2819,c_3466,c_4521]) ).
tcf(c_4623,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_3491,c_4613]) ).
tcf(c_4734,plain,
( greater_or_equal(iPr_def_21,iPr_def_20)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_4623,c_3947]) ).
tcf(c_4744,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_4623,c_1809]) ).
tcf(c_4986,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_4744,c_3743,c_4744]) ).
tcf(c_4987,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(renaming,[status(thm)],[c_4986]) ).
tcf(c_4998,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1801,c_4987]) ).
tcf(c_5013,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_4998,c_3466,c_4998]) ).
tcf(c_5023,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1802,c_5013]) ).
tcf(c_5106,plain,
( ( iPr_def_11 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_4734,c_3466,c_5023]) ).
tcf(c_5107,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(renaming,[status(thm)],[c_5106]) ).
tcf(c_5117,plain,
( greater_or_equal(iPr_def_12,iPr_def_13)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_5107,c_2834]) ).
tcf(c_5124,plain,
( in_environment(iPr_def_10,iPr_def_12)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_5107,c_1807]) ).
tcf(c_5125,plain,
( greater(iPr_def_12,iPr_def_14)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_5107,c_1806]) ).
tcf(c_5256,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_5124,c_2610]) ).
tcf(c_5258,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ~ greater_or_equal(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_5124,c_2359]) ).
tcf(c_5568,plain,
( ( zero = iPr_def_20 )
| ( iPr_def_11 = iPr_def_14 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_5256,c_2610,c_3109,c_5125,c_5124,c_5117,c_5258]) ).
tcf(c_5569,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(renaming,[status(thm)],[c_5568]) ).
tcf(c_5585,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5569,c_1809]) ).
tcf(c_5766,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_5585,c_5117,c_5258,c_5585]) ).
tcf(c_5767,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(renaming,[status(thm)],[c_5766]) ).
tcf(c_5776,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1801,c_5767]) ).
tcf(c_5821,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_5776,c_5124,c_5776]) ).
tcf(c_5829,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1802,c_5821]) ).
tcf(c_5833,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_5829,c_5124,c_5829]) ).
tcf(c_5849,plain,
( greater_or_equal(iPr_def_12,iPr_def_13)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_5833,c_2870]) ).
tcf(c_5856,plain,
( greater_or_equal(iPr_def_17,iPr_def_13)
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_5833,c_2455]) ).
tcf(c_6495,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3493,c_5849]) ).
tcf(c_6782,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_12,iPr_def_14) ),
inference(superposition,[status(thm)],[c_6495,c_3109]) ).
tcf(c_6783,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_20,zero) ),
inference(superposition,[status(thm)],[c_6495,c_1811]) ).
tcf(c_6809,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ greater(iPr_def_20,zero) ),
inference(global_subsumption_just,[status(thm)],[c_6783,c_2819,c_3466,c_6782]) ).
tcf(c_6817,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3491,c_6809]) ).
tcf(c_6841,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_6817,c_1809]) ).
tcf(c_7088,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_6841,c_6495,c_6841]) ).
tcf(c_7089,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(renaming,[status(thm)],[c_7088]) ).
tcf(c_7098,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1801,c_7089]) ).
tcf(c_7103,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7098,c_3466,c_7098]) ).
tcf(c_7111,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1802,c_7103]) ).
tcf(c_7115,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_7111,c_3466,c_7111]) ).
tcf(c_7123,plain,
( greater_or_equal(iPr_def_12,iPr_def_13)
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_7115,c_5856]) ).
tcf(c_7135,plain,
( in_environment(iPr_def_10,iPr_def_12)
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_7115,c_1807]) ).
tcf(c_7136,plain,
( greater(iPr_def_12,iPr_def_14)
| ( iPr_def_11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_7115,c_1806]) ).
tcf(c_7172,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_11 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_7135,c_2610]) ).
tcf(c_7174,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_14 )
| ~ greater_or_equal(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_7135,c_2359]) ).
tcf(c_7666,plain,
( ( zero = iPr_def_20 )
| ( iPr_def_11 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_7172,c_2610,c_3109,c_7136,c_7135,c_7123,c_7174]) ).
tcf(c_7667,plain,
( ( iPr_def_11 = iPr_def_14 )
| ( zero = iPr_def_20 ) ),
inference(renaming,[status(thm)],[c_7666]) ).
tcf(c_7680,plain,
( ( iPr_def_11 = iPr_def_14 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7667,c_1809]) ).
tcf(c_7827,plain,
( ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7680,c_7123,c_7174,c_7680]) ).
tcf(c_7828,plain,
( ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(renaming,[status(thm)],[c_7827]) ).
tcf(c_7835,plain,
( ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1801,c_7828]) ).
tcf(c_7843,plain,
( ( iPr_def_11 = iPr_def_14 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7835,c_7135,c_7835]) ).
tcf(c_7849,plain,
( ( iPr_def_11 = iPr_def_14 )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1802,c_7843]) ).
tcf(c_7852,plain,
iPr_def_11 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_7849,c_7135,c_7849]) ).
tcf(c_7885,plain,
( greater_or_equal(iPr_def_12,iPr_def_13)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_3026,c_7852]) ).
tcf(c_7887,plain,
( ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_21,zero)
| ~ greater(iPr_def_20,zero)
| ~ greater(iPr_def_12,iPr_def_11) ),
inference(demodulation,[status(thm)],[c_3109,c_7852]) ).
tcf(c_7893,plain,
( greater_or_equal(iPr_def_12,iPr_def_11)
| ( iPr_def_12 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_2870,c_7852]) ).
tcf(c_7894,plain,
( greater_or_equal(iPr_def_17,iPr_def_13)
| ( iPr_def_11 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_2834,c_7852]) ).
tcf(c_7903,plain,
greater_or_equal(iPr_def_17,iPr_def_11),
inference(demodulation,[status(thm)],[c_2455,c_7852]) ).
tcf(c_7910,plain,
greater(iPr_def_17,iPr_def_11),
inference(demodulation,[status(thm)],[c_1806,c_7852]) ).
tcf(c_8169,plain,
( in_environment(iPr_def_10,iPr_def_12)
| ( iPr_def_12 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_7893,c_2315]) ).
tcf(c_8254,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_12 = iPr_def_17 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_8169,c_2610]) ).
tcf(c_8256,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_17 )
| ~ greater_or_equal(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_8169,c_2359]) ).
tcf(c_8488,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_7885,c_8256]) ).
tcf(c_8624,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_20,zero) ),
inference(superposition,[status(thm)],[c_8488,c_1811]) ).
tcf(c_8648,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ~ greater(iPr_def_20,zero) ),
inference(global_subsumption_just,[status(thm)],[c_8624,c_2819,c_3109,c_8169,c_8488]) ).
tcf(c_8656,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_8254,c_8648]) ).
tcf(c_8673,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_8656,c_1809]) ).
tcf(c_8801,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_8673,c_8488,c_8673]) ).
tcf(c_8802,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(renaming,[status(thm)],[c_8801]) ).
tcf(c_8811,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1801,c_8802]) ).
tcf(c_8816,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_8811,c_8169,c_8811]) ).
tcf(c_8824,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1802,c_8816]) ).
tcf(c_8828,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( iPr_def_11 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_8824,c_8169,c_8824]) ).
tcf(c_8835,plain,
( greater_or_equal(iPr_def_12,iPr_def_13)
| ( iPr_def_11 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_8828,c_7894]) ).
tcf(c_8837,plain,
( greater(iPr_def_12,iPr_def_11)
| ( iPr_def_11 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_8828,c_7910]) ).
tcf(c_8841,plain,
( in_environment(iPr_def_10,iPr_def_12)
| ( iPr_def_11 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_8828,c_1807]) ).
tcf(c_8869,plain,
( greater(iPr_def_20,zero)
| ( iPr_def_11 = iPr_def_13 )
| ( zero = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_8841,c_2610]) ).
tcf(c_8871,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_11 = iPr_def_13 )
| ~ greater_or_equal(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_8841,c_2359]) ).
tcf(c_9350,plain,
( ( zero = iPr_def_20 )
| ( iPr_def_11 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_8869,c_2610,c_7887,c_8841,c_8837,c_8835,c_8871]) ).
tcf(c_9351,plain,
( ( iPr_def_11 = iPr_def_13 )
| ( zero = iPr_def_20 ) ),
inference(renaming,[status(thm)],[c_9350]) ).
tcf(c_9361,plain,
( ( iPr_def_11 = iPr_def_13 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9351,c_1809]) ).
tcf(c_9589,plain,
( ( iPr_def_11 = iPr_def_13 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_9361,c_8835,c_8871,c_9361]) ).
tcf(c_9590,plain,
( ( iPr_def_11 = iPr_def_13 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(renaming,[status(thm)],[c_9589]) ).
tcf(c_9597,plain,
( ( iPr_def_11 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1801,c_9590]) ).
tcf(c_9601,plain,
( ( iPr_def_11 = iPr_def_13 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_9597,c_8841,c_9597]) ).
tcf(c_9607,plain,
( ( iPr_def_11 = iPr_def_13 )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1802,c_9601]) ).
tcf(c_9610,plain,
iPr_def_11 = iPr_def_13,
inference(global_subsumption_just,[status(thm)],[c_9607,c_8841,c_9607]) ).
tcf(c_9623,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_17 )
| ~ greater_or_equal(iPr_def_12,iPr_def_11) ),
inference(demodulation,[status(thm)],[c_8256,c_9610]) ).
tcf(c_9645,plain,
( greater(iPr_def_21,zero)
| ~ greater_or_equal(iPr_def_12,iPr_def_11)
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(demodulation,[status(thm)],[c_2359,c_9610]) ).
tcf(c_9790,plain,
( greater(iPr_def_21,zero)
| ( iPr_def_12 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_9623,c_7893,c_9623]) ).
tcf(c_9799,plain,
( ( iPr_def_12 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ greater(iPr_def_24,iPr_def_25)
| ~ greater(iPr_def_20,zero) ),
inference(superposition,[status(thm)],[c_9790,c_1811]) ).
tcf(c_9823,plain,
( ( iPr_def_12 = iPr_def_17 )
| ~ greater(iPr_def_20,zero) ),
inference(global_subsumption_just,[status(thm)],[c_9799,c_2819,c_3109,c_7893,c_8169,c_9623]) ).
tcf(c_9829,plain,
( ( iPr_def_12 = iPr_def_17 )
| ( zero = iPr_def_20 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8254,c_9823]) ).
tcf(c_9842,plain,
( ( iPr_def_12 = iPr_def_17 )
| ~ greater(iPr_def_21,zero)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9829,c_1809]) ).
tcf(c_9903,plain,
( ( iPr_def_12 = iPr_def_17 )
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_9842,c_9790,c_9842]) ).
tcf(c_9904,plain,
( ( iPr_def_12 = iPr_def_17 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(renaming,[status(thm)],[c_9903]) ).
tcf(c_9911,plain,
( ( iPr_def_12 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1801,c_9904]) ).
tcf(c_9915,plain,
( ( iPr_def_12 = iPr_def_17 )
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_9911,c_8169,c_9911]) ).
tcf(c_9921,plain,
( ( iPr_def_12 = iPr_def_17 )
| ~ in_environment(iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1802,c_9915]) ).
tcf(c_9924,plain,
iPr_def_12 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_9921,c_8169,c_9921]) ).
tcf(c_9933,plain,
greater_or_equal(iPr_def_12,iPr_def_11),
inference(demodulation,[status(thm)],[c_7903,c_9924]) ).
tcf(c_9934,plain,
greater(iPr_def_12,iPr_def_11),
inference(demodulation,[status(thm)],[c_7910,c_9924]) ).
tcf(c_9938,plain,
in_environment(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_1807,c_9924]) ).
tcf(c_9945,plain,
( greater(iPr_def_20,zero)
| ( zero = iPr_def_20 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2610,c_9938]) ).
tcf(c_9946,plain,
greater_or_equal(iPr_def_20,zero),
inference(backward_subsumption_resolution,[status(thm)],[c_2356,c_9938]) ).
tcf(c_10035,plain,
zero = iPr_def_20,
inference(global_subsumption_just,[status(thm)],[c_9945,c_2610,c_7887,c_9645,c_9938,c_9934,c_9933]) ).
tcf(c_10054,plain,
( ~ greater(iPr_def_21,iPr_def_20)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ( iPr_def_20 != iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_1809,c_10035]) ).
tcf(c_10097,plain,
( ~ greater(iPr_def_21,iPr_def_20)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(equality_resolution_simp,[status(thm)],[c_10054]) ).
tcf(c_10287,plain,
( ~ subpopulation(first_movers,iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_10097,c_1809,c_3074,c_7887,c_9645,c_9946,c_9938,c_9934,c_9933]) ).
tcf(c_10288,plain,
( ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12)
| ~ subpopulation(first_movers,iPr_def_10,iPr_def_12) ),
inference(renaming,[status(thm)],[c_10287]) ).
tcf(c_10293,plain,
( ~ in_environment(iPr_def_10,iPr_def_12)
| ~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1801,c_10288]) ).
tcf(c_10294,plain,
~ subpopulation(efficient_producers,iPr_def_10,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_10293,c_9938]) ).
tcf(c_10295,plain,
~ in_environment(iPr_def_10,iPr_def_12),
inference(superposition,[status(thm)],[c_1802,c_10294]) ).
tcf(c_10296,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_10295,c_9938]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT039-2 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 01:10:24 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 3.51/1.72 % SZS status Started for theBenchmark.p
% 3.51/1.72 % SZS status Unsatisfiable for theBenchmark.p
% 3.51/1.72
% 3.51/1.72 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.51/1.72
% 3.51/1.72 % ------ iProver source info
% 3.51/1.72
% 3.51/1.72 % git: date: 2026-07-19 20:42:38 +0200
% 3.51/1.72 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.51/1.72 % git: non_committed_changes: false
% 3.51/1.72
% 3.51/1.72 % ------ Parsing...% successful
% 3.51/1.72
% 3.51/1.72
% 3.51/1.72 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.51/1.72
% 3.51/1.72 % ------ Preprocessing... sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 7 0s sf_e pe_s pe_e %
% 3.51/1.72
% 3.51/1.72 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.51/1.72
% 3.51/1.72 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.51/1.72 % ------ Proving...
% 3.51/1.72 % ------ Problem Properties
% 3.51/1.72
% 3.51/1.72 %
% 3.51/1.72 % clauses 38
% 3.51/1.72 % conjectures 0
% 3.51/1.72 % EPR 19
% 3.51/1.72 % Horn 36
% 3.51/1.72 % unary 23
% 3.51/1.72 % binary 5
% 3.51/1.72 % lits 69
% 3.51/1.72 % lits eq 19
% 3.51/1.72 % fd_pure 0
% 3.51/1.72 % fd_pseudo 0
% 3.51/1.72 % fd_cond 0
% 3.51/1.72 % fd_pseudo_cond 1
% 3.51/1.72 % AC symbols 0
% 3.51/1.72
% 3.51/1.72 % ------ Schedule dynamic 5 is on
% 3.51/1.72
% 3.51/1.72 % ------ no conjectures: strip conj schedule
% 3.51/1.72
% 3.51/1.72 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 3.51/1.72
% 3.51/1.72
% 3.51/1.72 % ------
% 3.51/1.72 % Current options:
% 3.51/1.72 % ------
% 3.51/1.72
% 3.51/1.72
% 3.51/1.72 %
% 3.51/1.72
% 3.51/1.72 % ------ Proving...
% 3.51/1.72 %
% 3.51/1.72
% 3.51/1.72 % SZS status Unsatisfiable for theBenchmark.p
% 3.51/1.72
% 3.51/1.72 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.51/1.72
% 3.51/1.72
%------------------------------------------------------------------------------