%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT030+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:02:55 AM UTC 2026
% Result : Theorem 7.34s 3.39s
% Output : CNFRefutation 7.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 3
% Syntax : Number of formulae : 148 ( 45 unt; 0 typ; 0 def)
% Number of atoms : 463 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 627 ( 312 ~; 295 |; 13 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 123 ( 119 !; 4 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ subpopulations > in_environment > greater_or_equal > greater > stable > environment > growth_rate > #nlpp > first_movers > efficient_producers > #skF_5 > #skF_2 > #skF_4 > #skF_3 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(subpopulations,type,
subpopulations: ( $i * $i * $i * $i ) > $o ).
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff(in_environment,type,
in_environment: ( $i * $i ) > $o ).
tff(efficient_producers,type,
efficient_producers: $i ).
tff(growth_rate,type,
growth_rate: ( $i * $i ) > $i ).
tff(environment,type,
environment: $i > $o ).
tff(first_movers,type,
first_movers: $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff(greater_or_equal,type,
greater_or_equal: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(stable,type,
stable: $i > $o ).
tff(f_91,negated_conjecture,
~ ! [E] :
( ( environment(E)
& stable(E) )
=> ? [To] :
( in_environment(E,To)
& ~ greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To))
& ! [T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& greater(T,To) )
=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l12) ).
tff(f_71,hypothesis,
! [E] :
( ( environment(E)
& stable(E) )
=> ? [To] :
( in_environment(E,To)
& ! [T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& greater_or_equal(T,To) )
=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1) ).
tff(f_55,axiom,
! [E] :
( ( environment(E)
& ? [To] :
( in_environment(E,To)
& ! [T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& greater_or_equal(T,To) )
=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) )
=> ? [To] :
( in_environment(E,To)
& ~ greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To))
& ! [T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& greater(T,To) )
=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds) ).
tff(c_26,plain,
environment('#skF_4'),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_24,plain,
stable('#skF_4'),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_22,plain,
! [E_12] :
( in_environment(E_12,'#skF_3'(E_12))
| ~ stable(E_12)
| ~ environment(E_12) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_18,plain,
! [E_1,To_8] :
( subpopulations(first_movers,efficient_producers,E_1,'#skF_1'(E_1,To_8))
| in_environment(E_1,'#skF_2'(E_1))
| ~ in_environment(E_1,To_8)
| ~ environment(E_1) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_16,plain,
! [E_1,To_8] :
( greater_or_equal('#skF_1'(E_1,To_8),To_8)
| in_environment(E_1,'#skF_2'(E_1))
| ~ in_environment(E_1,To_8)
| ~ environment(E_1) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_57,plain,
! [T_35,E_36] :
( greater(growth_rate(efficient_producers,T_35),growth_rate(first_movers,T_35))
| ~ greater_or_equal(T_35,'#skF_3'(E_36))
| ~ subpopulations(first_movers,efficient_producers,E_36,T_35)
| ~ stable(E_36)
| ~ environment(E_36) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_331,plain,
! [E_96,E_97] :
( greater(growth_rate(efficient_producers,'#skF_1'(E_96,'#skF_3'(E_97))),growth_rate(first_movers,'#skF_1'(E_96,'#skF_3'(E_97))))
| ~ subpopulations(first_movers,efficient_producers,E_97,'#skF_1'(E_96,'#skF_3'(E_97)))
| ~ stable(E_97)
| ~ environment(E_97)
| in_environment(E_96,'#skF_2'(E_96))
| ~ in_environment(E_96,'#skF_3'(E_97))
| ~ environment(E_96) ),
inference(resolution,[status(thm)],[c_16,c_57]) ).
tff(c_14,plain,
! [E_1,To_8] :
( ~ greater(growth_rate(efficient_producers,'#skF_1'(E_1,To_8)),growth_rate(first_movers,'#skF_1'(E_1,To_8)))
| in_environment(E_1,'#skF_2'(E_1))
| ~ in_environment(E_1,To_8)
| ~ environment(E_1) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_342,plain,
! [E_98,E_99] :
( ~ subpopulations(first_movers,efficient_producers,E_98,'#skF_1'(E_99,'#skF_3'(E_98)))
| ~ stable(E_98)
| ~ environment(E_98)
| in_environment(E_99,'#skF_2'(E_99))
| ~ in_environment(E_99,'#skF_3'(E_98))
| ~ environment(E_99) ),
inference(resolution,[status(thm)],[c_331,c_14]) ).
tff(c_358,plain,
! [E_1] :
( ~ stable(E_1)
| in_environment(E_1,'#skF_2'(E_1))
| ~ in_environment(E_1,'#skF_3'(E_1))
| ~ environment(E_1) ),
inference(resolution,[status(thm)],[c_18,c_342]) ).
tff(c_32,plain,
! [To_21] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'(To_21))
| greater(growth_rate(efficient_producers,To_21),growth_rate(first_movers,To_21))
| ~ in_environment('#skF_4',To_21) ),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_38,plain,
! [E_30,To_31] :
( greater_or_equal('#skF_1'(E_30,To_31),To_31)
| ~ greater(growth_rate(efficient_producers,'#skF_2'(E_30)),growth_rate(first_movers,'#skF_2'(E_30)))
| ~ in_environment(E_30,To_31)
| ~ environment(E_30) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_45,plain,
! [E_30,To_31] :
( greater_or_equal('#skF_1'(E_30,To_31),To_31)
| ~ in_environment(E_30,To_31)
| ~ environment(E_30)
| subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'(E_30)))
| ~ in_environment('#skF_4','#skF_2'(E_30)) ),
inference(resolution,[status(thm)],[c_32,c_38]) ).
tff(c_30,plain,
! [To_21] :
( greater('#skF_5'(To_21),To_21)
| greater(growth_rate(efficient_producers,To_21),growth_rate(first_movers,To_21))
| ~ in_environment('#skF_4',To_21) ),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_46,plain,
! [E_30,To_31] :
( greater_or_equal('#skF_1'(E_30,To_31),To_31)
| ~ in_environment(E_30,To_31)
| ~ environment(E_30)
| greater('#skF_5'('#skF_2'(E_30)),'#skF_2'(E_30))
| ~ in_environment('#skF_4','#skF_2'(E_30)) ),
inference(resolution,[status(thm)],[c_30,c_38]) ).
tff(c_124,plain,
! [E_55,To_56,T_57] :
( greater_or_equal('#skF_1'(E_55,To_56),To_56)
| greater(growth_rate(efficient_producers,T_57),growth_rate(first_movers,T_57))
| ~ greater(T_57,'#skF_2'(E_55))
| ~ subpopulations(first_movers,efficient_producers,E_55,T_57)
| ~ in_environment(E_55,To_56)
| ~ environment(E_55) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_130,plain,
! [E_30,To_56,To_31] :
( greater_or_equal('#skF_1'(E_30,To_56),To_56)
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'(E_30))),growth_rate(first_movers,'#skF_5'('#skF_2'(E_30))))
| ~ subpopulations(first_movers,efficient_producers,E_30,'#skF_5'('#skF_2'(E_30)))
| ~ in_environment(E_30,To_56)
| greater_or_equal('#skF_1'(E_30,To_31),To_31)
| ~ in_environment(E_30,To_31)
| ~ environment(E_30)
| ~ in_environment('#skF_4','#skF_2'(E_30)) ),
inference(resolution,[status(thm)],[c_46,c_124]) ).
tff(c_396,plain,
! [E_114,To_115] :
( greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'(E_114))),growth_rate(first_movers,'#skF_5'('#skF_2'(E_114))))
| ~ subpopulations(first_movers,efficient_producers,E_114,'#skF_5'('#skF_2'(E_114)))
| ~ in_environment(E_114,To_115)
| ~ environment(E_114)
| ~ in_environment('#skF_4','#skF_2'(E_114))
| greater_or_equal('#skF_1'(E_114,To_115),To_115) ),
inference(factorization,[status(thm),theory(equality)],[c_130]) ).
tff(c_28,plain,
! [To_21] :
( ~ greater(growth_rate(efficient_producers,'#skF_5'(To_21)),growth_rate(first_movers,'#skF_5'(To_21)))
| greater(growth_rate(efficient_producers,To_21),growth_rate(first_movers,To_21))
| ~ in_environment('#skF_4',To_21) ),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_421,plain,
! [E_119,To_120] :
( greater(growth_rate(efficient_producers,'#skF_2'(E_119)),growth_rate(first_movers,'#skF_2'(E_119)))
| ~ subpopulations(first_movers,efficient_producers,E_119,'#skF_5'('#skF_2'(E_119)))
| ~ in_environment(E_119,To_120)
| ~ environment(E_119)
| ~ in_environment('#skF_4','#skF_2'(E_119))
| greater_or_equal('#skF_1'(E_119,To_120),To_120) ),
inference(resolution,[status(thm)],[c_396,c_28]) ).
tff(c_10,plain,
! [E_1,To_8] :
( greater_or_equal('#skF_1'(E_1,To_8),To_8)
| ~ greater(growth_rate(efficient_producers,'#skF_2'(E_1)),growth_rate(first_movers,'#skF_2'(E_1)))
| ~ in_environment(E_1,To_8)
| ~ environment(E_1) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_441,plain,
! [E_121,To_122,To_123] :
( greater_or_equal('#skF_1'(E_121,To_122),To_122)
| ~ in_environment(E_121,To_122)
| ~ subpopulations(first_movers,efficient_producers,E_121,'#skF_5'('#skF_2'(E_121)))
| ~ in_environment(E_121,To_123)
| ~ environment(E_121)
| ~ in_environment('#skF_4','#skF_2'(E_121))
| greater_or_equal('#skF_1'(E_121,To_123),To_123) ),
inference(resolution,[status(thm)],[c_421,c_10]) ).
tff(c_450,plain,
! [To_122,To_123,To_31] :
( greater_or_equal('#skF_1'('#skF_4',To_122),To_122)
| ~ in_environment('#skF_4',To_122)
| ~ in_environment('#skF_4',To_123)
| greater_or_equal('#skF_1'('#skF_4',To_123),To_123)
| greater_or_equal('#skF_1'('#skF_4',To_31),To_31)
| ~ in_environment('#skF_4',To_31)
| ~ environment('#skF_4')
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_45,c_441]) ).
tff(c_459,plain,
! [To_122,To_123,To_31] :
( greater_or_equal('#skF_1'('#skF_4',To_122),To_122)
| ~ in_environment('#skF_4',To_122)
| ~ in_environment('#skF_4',To_123)
| greater_or_equal('#skF_1'('#skF_4',To_123),To_123)
| greater_or_equal('#skF_1'('#skF_4',To_31),To_31)
| ~ in_environment('#skF_4',To_31)
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_450]) ).
tff(c_460,plain,
~ in_environment('#skF_4','#skF_2'('#skF_4')),
inference(splitLeft,[status(thm)],[c_459]) ).
tff(c_464,plain,
( ~ stable('#skF_4')
| ~ in_environment('#skF_4','#skF_3'('#skF_4'))
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_358,c_460]) ).
tff(c_472,plain,
~ in_environment('#skF_4','#skF_3'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_464]) ).
tff(c_478,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_22,c_472]) ).
tff(c_482,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_478]) ).
tff(c_484,plain,
in_environment('#skF_4','#skF_2'('#skF_4')),
inference(splitRight,[status(thm)],[c_459]) ).
tff(c_483,plain,
! [To_31,To_123,To_122] :
( greater_or_equal('#skF_1'('#skF_4',To_31),To_31)
| ~ in_environment('#skF_4',To_31)
| ~ in_environment('#skF_4',To_123)
| greater_or_equal('#skF_1'('#skF_4',To_123),To_123)
| greater_or_equal('#skF_1'('#skF_4',To_122),To_122)
| ~ in_environment('#skF_4',To_122) ),
inference(splitRight,[status(thm)],[c_459]) ).
tff(c_486,plain,
! [To_124] :
( greater_or_equal('#skF_1'('#skF_4',To_124),To_124)
| ~ in_environment('#skF_4',To_124) ),
inference(splitLeft,[status(thm)],[c_483]) ).
tff(c_20,plain,
! [T_17,E_12] :
( greater(growth_rate(efficient_producers,T_17),growth_rate(first_movers,T_17))
| ~ greater_or_equal(T_17,'#skF_3'(E_12))
| ~ subpopulations(first_movers,efficient_producers,E_12,T_17)
| ~ stable(E_12)
| ~ environment(E_12) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_502,plain,
! [E_127] :
( greater(growth_rate(efficient_producers,'#skF_1'('#skF_4','#skF_3'(E_127))),growth_rate(first_movers,'#skF_1'('#skF_4','#skF_3'(E_127))))
| ~ subpopulations(first_movers,efficient_producers,E_127,'#skF_1'('#skF_4','#skF_3'(E_127)))
| ~ stable(E_127)
| ~ environment(E_127)
| ~ in_environment('#skF_4','#skF_3'(E_127)) ),
inference(resolution,[status(thm)],[c_486,c_20]) ).
tff(c_8,plain,
! [E_1,To_8] :
( ~ greater(growth_rate(efficient_producers,'#skF_1'(E_1,To_8)),growth_rate(first_movers,'#skF_1'(E_1,To_8)))
| ~ greater(growth_rate(efficient_producers,'#skF_2'(E_1)),growth_rate(first_movers,'#skF_2'(E_1)))
| ~ in_environment(E_1,To_8)
| ~ environment(E_1) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_506,plain,
! [E_127] :
( ~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ environment('#skF_4')
| ~ subpopulations(first_movers,efficient_producers,E_127,'#skF_1'('#skF_4','#skF_3'(E_127)))
| ~ stable(E_127)
| ~ environment(E_127)
| ~ in_environment('#skF_4','#skF_3'(E_127)) ),
inference(resolution,[status(thm)],[c_502,c_8]) ).
tff(c_515,plain,
! [E_127] :
( ~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ subpopulations(first_movers,efficient_producers,E_127,'#skF_1'('#skF_4','#skF_3'(E_127)))
| ~ stable(E_127)
| ~ environment(E_127)
| ~ in_environment('#skF_4','#skF_3'(E_127)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_506]) ).
tff(c_519,plain,
~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(splitLeft,[status(thm)],[c_515]) ).
tff(c_530,plain,
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_32,c_519]) ).
tff(c_542,plain,
subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_530]) ).
tff(c_533,plain,
( greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4'))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_30,c_519]) ).
tff(c_545,plain,
greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_533]) ).
tff(c_6,plain,
! [E_1,To_8,T_11] :
( subpopulations(first_movers,efficient_producers,E_1,'#skF_1'(E_1,To_8))
| greater(growth_rate(efficient_producers,T_11),growth_rate(first_movers,T_11))
| ~ greater(T_11,'#skF_2'(E_1))
| ~ subpopulations(first_movers,efficient_producers,E_1,T_11)
| ~ in_environment(E_1,To_8)
| ~ environment(E_1) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_553,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4',To_8)
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_545,c_6]) ).
tff(c_567,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_553]) ).
tff(c_578,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_542,c_567]) ).
tff(c_579,plain,
greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4')))),
inference(splitLeft,[status(thm)],[c_578]) ).
tff(c_582,plain,
( greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_579,c_28]) ).
tff(c_585,plain,
greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_582]) ).
tff(c_587,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_519,c_585]) ).
tff(c_588,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8) ),
inference(splitRight,[status(thm)],[c_578]) ).
tff(c_2,plain,
! [E_1,To_8,T_11] :
( ~ greater(growth_rate(efficient_producers,'#skF_1'(E_1,To_8)),growth_rate(first_movers,'#skF_1'(E_1,To_8)))
| greater(growth_rate(efficient_producers,T_11),growth_rate(first_movers,T_11))
| ~ greater(T_11,'#skF_2'(E_1))
| ~ subpopulations(first_movers,efficient_producers,E_1,T_11)
| ~ in_environment(E_1,To_8)
| ~ environment(E_1) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_504,plain,
! [T_11,E_127] :
( greater(growth_rate(efficient_producers,T_11),growth_rate(first_movers,T_11))
| ~ greater(T_11,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_11)
| ~ environment('#skF_4')
| ~ subpopulations(first_movers,efficient_producers,E_127,'#skF_1'('#skF_4','#skF_3'(E_127)))
| ~ stable(E_127)
| ~ environment(E_127)
| ~ in_environment('#skF_4','#skF_3'(E_127)) ),
inference(resolution,[status(thm)],[c_502,c_2]) ).
tff(c_512,plain,
! [T_11,E_127] :
( greater(growth_rate(efficient_producers,T_11),growth_rate(first_movers,T_11))
| ~ greater(T_11,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_11)
| ~ subpopulations(first_movers,efficient_producers,E_127,'#skF_1'('#skF_4','#skF_3'(E_127)))
| ~ stable(E_127)
| ~ environment(E_127)
| ~ in_environment('#skF_4','#skF_3'(E_127)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_504]) ).
tff(c_686,plain,
! [E_133] :
( ~ subpopulations(first_movers,efficient_producers,E_133,'#skF_1'('#skF_4','#skF_3'(E_133)))
| ~ stable(E_133)
| ~ environment(E_133)
| ~ in_environment('#skF_4','#skF_3'(E_133)) ),
inference(splitLeft,[status(thm)],[c_512]) ).
tff(c_690,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4')
| ~ in_environment('#skF_4','#skF_3'('#skF_4')) ),
inference(resolution,[status(thm)],[c_588,c_686]) ).
tff(c_705,plain,
~ in_environment('#skF_4','#skF_3'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_690]) ).
tff(c_722,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_22,c_705]) ).
tff(c_726,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_722]) ).
tff(c_728,plain,
! [T_136] :
( greater(growth_rate(efficient_producers,T_136),growth_rate(first_movers,T_136))
| ~ greater(T_136,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_136) ),
inference(splitRight,[status(thm)],[c_512]) ).
tff(c_589,plain,
~ greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4')))),
inference(splitRight,[status(thm)],[c_578]) ).
tff(c_731,plain,
( ~ greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4'))) ),
inference(resolution,[status(thm)],[c_728,c_589]) ).
tff(c_765,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_542,c_545,c_731]) ).
tff(c_767,plain,
greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(splitRight,[status(thm)],[c_515]) ).
tff(c_12,plain,
! [E_1,To_8] :
( subpopulations(first_movers,efficient_producers,E_1,'#skF_1'(E_1,To_8))
| ~ greater(growth_rate(efficient_producers,'#skF_2'(E_1)),growth_rate(first_movers,'#skF_2'(E_1)))
| ~ in_environment(E_1,To_8)
| ~ environment(E_1) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_775,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8)
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_767,c_12]) ).
tff(c_789,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_775]) ).
tff(c_800,plain,
! [E_138] :
( ~ subpopulations(first_movers,efficient_producers,E_138,'#skF_1'('#skF_4','#skF_3'(E_138)))
| ~ stable(E_138)
| ~ environment(E_138)
| ~ in_environment('#skF_4','#skF_3'(E_138)) ),
inference(splitRight,[status(thm)],[c_515]) ).
tff(c_804,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4')
| ~ in_environment('#skF_4','#skF_3'('#skF_4')) ),
inference(resolution,[status(thm)],[c_789,c_800]) ).
tff(c_819,plain,
~ in_environment('#skF_4','#skF_3'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_804]) ).
tff(c_825,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_22,c_819]) ).
tff(c_829,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_825]) ).
tff(c_830,plain,
! [To_123,To_31] :
( ~ in_environment('#skF_4',To_123)
| greater_or_equal('#skF_1'('#skF_4',To_123),To_123)
| greater_or_equal('#skF_1'('#skF_4',To_31),To_31)
| ~ in_environment('#skF_4',To_31) ),
inference(splitRight,[status(thm)],[c_483]) ).
tff(c_832,plain,
! [To_139] :
( greater_or_equal('#skF_1'('#skF_4',To_139),To_139)
| ~ in_environment('#skF_4',To_139) ),
inference(splitLeft,[status(thm)],[c_830]) ).
tff(c_848,plain,
! [E_142] :
( greater(growth_rate(efficient_producers,'#skF_1'('#skF_4','#skF_3'(E_142))),growth_rate(first_movers,'#skF_1'('#skF_4','#skF_3'(E_142))))
| ~ subpopulations(first_movers,efficient_producers,E_142,'#skF_1'('#skF_4','#skF_3'(E_142)))
| ~ stable(E_142)
| ~ environment(E_142)
| ~ in_environment('#skF_4','#skF_3'(E_142)) ),
inference(resolution,[status(thm)],[c_832,c_20]) ).
tff(c_852,plain,
! [E_142] :
( ~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ environment('#skF_4')
| ~ subpopulations(first_movers,efficient_producers,E_142,'#skF_1'('#skF_4','#skF_3'(E_142)))
| ~ stable(E_142)
| ~ environment(E_142)
| ~ in_environment('#skF_4','#skF_3'(E_142)) ),
inference(resolution,[status(thm)],[c_848,c_8]) ).
tff(c_861,plain,
! [E_142] :
( ~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ subpopulations(first_movers,efficient_producers,E_142,'#skF_1'('#skF_4','#skF_3'(E_142)))
| ~ stable(E_142)
| ~ environment(E_142)
| ~ in_environment('#skF_4','#skF_3'(E_142)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_852]) ).
tff(c_865,plain,
~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(splitLeft,[status(thm)],[c_861]) ).
tff(c_876,plain,
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_32,c_865]) ).
tff(c_888,plain,
subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_876]) ).
tff(c_879,plain,
( greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4'))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_30,c_865]) ).
tff(c_891,plain,
greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_879]) ).
tff(c_899,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4',To_8)
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_891,c_6]) ).
tff(c_913,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_899]) ).
tff(c_924,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_888,c_913]) ).
tff(c_925,plain,
greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4')))),
inference(splitLeft,[status(thm)],[c_924]) ).
tff(c_928,plain,
( greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_925,c_28]) ).
tff(c_931,plain,
greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_928]) ).
tff(c_933,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_865,c_931]) ).
tff(c_934,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8) ),
inference(splitRight,[status(thm)],[c_924]) ).
tff(c_850,plain,
! [T_11,E_142] :
( greater(growth_rate(efficient_producers,T_11),growth_rate(first_movers,T_11))
| ~ greater(T_11,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_11)
| ~ environment('#skF_4')
| ~ subpopulations(first_movers,efficient_producers,E_142,'#skF_1'('#skF_4','#skF_3'(E_142)))
| ~ stable(E_142)
| ~ environment(E_142)
| ~ in_environment('#skF_4','#skF_3'(E_142)) ),
inference(resolution,[status(thm)],[c_848,c_2]) ).
tff(c_858,plain,
! [T_11,E_142] :
( greater(growth_rate(efficient_producers,T_11),growth_rate(first_movers,T_11))
| ~ greater(T_11,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_11)
| ~ subpopulations(first_movers,efficient_producers,E_142,'#skF_1'('#skF_4','#skF_3'(E_142)))
| ~ stable(E_142)
| ~ environment(E_142)
| ~ in_environment('#skF_4','#skF_3'(E_142)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_850]) ).
tff(c_1032,plain,
! [E_148] :
( ~ subpopulations(first_movers,efficient_producers,E_148,'#skF_1'('#skF_4','#skF_3'(E_148)))
| ~ stable(E_148)
| ~ environment(E_148)
| ~ in_environment('#skF_4','#skF_3'(E_148)) ),
inference(splitLeft,[status(thm)],[c_858]) ).
tff(c_1036,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4')
| ~ in_environment('#skF_4','#skF_3'('#skF_4')) ),
inference(resolution,[status(thm)],[c_934,c_1032]) ).
tff(c_1051,plain,
~ in_environment('#skF_4','#skF_3'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_1036]) ).
tff(c_1068,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_22,c_1051]) ).
tff(c_1072,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_1068]) ).
tff(c_1074,plain,
! [T_151] :
( greater(growth_rate(efficient_producers,T_151),growth_rate(first_movers,T_151))
| ~ greater(T_151,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_151) ),
inference(splitRight,[status(thm)],[c_858]) ).
tff(c_935,plain,
~ greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4')))),
inference(splitRight,[status(thm)],[c_924]) ).
tff(c_1077,plain,
( ~ greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4'))) ),
inference(resolution,[status(thm)],[c_1074,c_935]) ).
tff(c_1111,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_888,c_891,c_1077]) ).
tff(c_1113,plain,
greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(splitRight,[status(thm)],[c_861]) ).
tff(c_1121,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8)
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_1113,c_12]) ).
tff(c_1135,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_1121]) ).
tff(c_1146,plain,
! [E_153] :
( ~ subpopulations(first_movers,efficient_producers,E_153,'#skF_1'('#skF_4','#skF_3'(E_153)))
| ~ stable(E_153)
| ~ environment(E_153)
| ~ in_environment('#skF_4','#skF_3'(E_153)) ),
inference(splitRight,[status(thm)],[c_861]) ).
tff(c_1150,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4')
| ~ in_environment('#skF_4','#skF_3'('#skF_4')) ),
inference(resolution,[status(thm)],[c_1135,c_1146]) ).
tff(c_1165,plain,
~ in_environment('#skF_4','#skF_3'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_1150]) ).
tff(c_1171,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_22,c_1165]) ).
tff(c_1175,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_1171]) ).
tff(c_1177,plain,
! [To_154] :
( ~ in_environment('#skF_4',To_154)
| greater_or_equal('#skF_1'('#skF_4',To_154),To_154) ),
inference(splitRight,[status(thm)],[c_830]) ).
tff(c_1182,plain,
! [E_155] :
( greater(growth_rate(efficient_producers,'#skF_1'('#skF_4','#skF_3'(E_155))),growth_rate(first_movers,'#skF_1'('#skF_4','#skF_3'(E_155))))
| ~ subpopulations(first_movers,efficient_producers,E_155,'#skF_1'('#skF_4','#skF_3'(E_155)))
| ~ stable(E_155)
| ~ environment(E_155)
| ~ in_environment('#skF_4','#skF_3'(E_155)) ),
inference(resolution,[status(thm)],[c_1177,c_20]) ).
tff(c_1186,plain,
! [E_155] :
( ~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ environment('#skF_4')
| ~ subpopulations(first_movers,efficient_producers,E_155,'#skF_1'('#skF_4','#skF_3'(E_155)))
| ~ stable(E_155)
| ~ environment(E_155)
| ~ in_environment('#skF_4','#skF_3'(E_155)) ),
inference(resolution,[status(thm)],[c_1182,c_8]) ).
tff(c_1195,plain,
! [E_155] :
( ~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ subpopulations(first_movers,efficient_producers,E_155,'#skF_1'('#skF_4','#skF_3'(E_155)))
| ~ stable(E_155)
| ~ environment(E_155)
| ~ in_environment('#skF_4','#skF_3'(E_155)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_1186]) ).
tff(c_1210,plain,
~ greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(splitLeft,[status(thm)],[c_1195]) ).
tff(c_1221,plain,
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_32,c_1210]) ).
tff(c_1233,plain,
subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_1221]) ).
tff(c_1224,plain,
( greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4'))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_30,c_1210]) ).
tff(c_1236,plain,
greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_1224]) ).
tff(c_1244,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4',To_8)
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_1236,c_6]) ).
tff(c_1258,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4')))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_1244]) ).
tff(c_1269,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4'))))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_1233,c_1258]) ).
tff(c_1270,plain,
greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4')))),
inference(splitLeft,[status(thm)],[c_1269]) ).
tff(c_1273,plain,
( greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4')))
| ~ in_environment('#skF_4','#skF_2'('#skF_4')) ),
inference(resolution,[status(thm)],[c_1270,c_28]) ).
tff(c_1276,plain,
greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_1273]) ).
tff(c_1278,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1210,c_1276]) ).
tff(c_1279,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8) ),
inference(splitRight,[status(thm)],[c_1269]) ).
tff(c_1184,plain,
! [T_11,E_155] :
( greater(growth_rate(efficient_producers,T_11),growth_rate(first_movers,T_11))
| ~ greater(T_11,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_11)
| ~ environment('#skF_4')
| ~ subpopulations(first_movers,efficient_producers,E_155,'#skF_1'('#skF_4','#skF_3'(E_155)))
| ~ stable(E_155)
| ~ environment(E_155)
| ~ in_environment('#skF_4','#skF_3'(E_155)) ),
inference(resolution,[status(thm)],[c_1182,c_2]) ).
tff(c_1192,plain,
! [T_11,E_155] :
( greater(growth_rate(efficient_producers,T_11),growth_rate(first_movers,T_11))
| ~ greater(T_11,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_11)
| ~ subpopulations(first_movers,efficient_producers,E_155,'#skF_1'('#skF_4','#skF_3'(E_155)))
| ~ stable(E_155)
| ~ environment(E_155)
| ~ in_environment('#skF_4','#skF_3'(E_155)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_1184]) ).
tff(c_1377,plain,
! [E_163] :
( ~ subpopulations(first_movers,efficient_producers,E_163,'#skF_1'('#skF_4','#skF_3'(E_163)))
| ~ stable(E_163)
| ~ environment(E_163)
| ~ in_environment('#skF_4','#skF_3'(E_163)) ),
inference(splitLeft,[status(thm)],[c_1192]) ).
tff(c_1381,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4')
| ~ in_environment('#skF_4','#skF_3'('#skF_4')) ),
inference(resolution,[status(thm)],[c_1279,c_1377]) ).
tff(c_1396,plain,
~ in_environment('#skF_4','#skF_3'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_1381]) ).
tff(c_1402,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_22,c_1396]) ).
tff(c_1406,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_1402]) ).
tff(c_1408,plain,
! [T_164] :
( greater(growth_rate(efficient_producers,T_164),growth_rate(first_movers,T_164))
| ~ greater(T_164,'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4',T_164) ),
inference(splitRight,[status(thm)],[c_1192]) ).
tff(c_1280,plain,
~ greater(growth_rate(efficient_producers,'#skF_5'('#skF_2'('#skF_4'))),growth_rate(first_movers,'#skF_5'('#skF_2'('#skF_4')))),
inference(splitRight,[status(thm)],[c_1269]) ).
tff(c_1411,plain,
( ~ greater('#skF_5'('#skF_2'('#skF_4')),'#skF_2'('#skF_4'))
| ~ subpopulations(first_movers,efficient_producers,'#skF_4','#skF_5'('#skF_2'('#skF_4'))) ),
inference(resolution,[status(thm)],[c_1408,c_1280]) ).
tff(c_1445,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1233,c_1236,c_1411]) ).
tff(c_1447,plain,
greater(growth_rate(efficient_producers,'#skF_2'('#skF_4')),growth_rate(first_movers,'#skF_2'('#skF_4'))),
inference(splitRight,[status(thm)],[c_1195]) ).
tff(c_1455,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8)
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_1447,c_12]) ).
tff(c_1469,plain,
! [To_8] :
( subpopulations(first_movers,efficient_producers,'#skF_4','#skF_1'('#skF_4',To_8))
| ~ in_environment('#skF_4',To_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_1455]) ).
tff(c_1480,plain,
! [E_166] :
( ~ subpopulations(first_movers,efficient_producers,E_166,'#skF_1'('#skF_4','#skF_3'(E_166)))
| ~ stable(E_166)
| ~ environment(E_166)
| ~ in_environment('#skF_4','#skF_3'(E_166)) ),
inference(splitRight,[status(thm)],[c_1195]) ).
tff(c_1484,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4')
| ~ in_environment('#skF_4','#skF_3'('#skF_4')) ),
inference(resolution,[status(thm)],[c_1469,c_1480]) ).
tff(c_1499,plain,
~ in_environment('#skF_4','#skF_3'('#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_1484]) ).
tff(c_1505,plain,
( ~ stable('#skF_4')
| ~ environment('#skF_4') ),
inference(resolution,[status(thm)],[c_22,c_1499]) ).
tff(c_1509,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_1505]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT030+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 12:21:42 UTC 2026
% 0.09/0.36 % CPUTime :
% 7.34/3.39 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.74/3.42
% 7.74/3.42 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------