%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT034+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Sun Sep 27 08:01:16 AM UTC 2026
% Result : Theorem 28.89s 19.26s
% Output : CNFRefutation 28.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 17
% Syntax : Number of formulae : 112 ( 14 unt; 0 def)
% Number of atoms : 414 ( 38 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 517 ( 215 ~; 251 |; 31 &)
% ( 3 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-2 aty)
% Number of variables : 115 ( 0 sgn 37 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mp1_high_growth_rates,axiom,
! [X0,X1,X2,X3] :
( ( greater('growth$urate'(X2,X3),'growth$urate'(X1,X3))
& subpopulations(X1,X2,X0,X3)
& environment(X0) )
=> 'selection$ufavors'(X2,X1,X3) ) ).
fof(l3,axiom,
! [X0,X1] :
( ( subpopulations('first$umovers','efficient$uproducers',X0,X1)
& environment(X0) )
=> ~ decreases(difference('disbanding$urate'('first$umovers',X1),'disbanding$urate'('efficient$uproducers',X1))) ) ).
fof(mp_critical_point_means_FM_and_EP,axiom,
! [X0] :
( ( 'in$uenvironment'(X0,'critical$upoint'(X0))
& environment(X0) )
=> subpopulations('first$umovers','efficient$uproducers',X0,'critical$upoint'(X0)) ) ).
fof(mp_FM_and_EP_when_EP_appears,axiom,
! [X0] :
( ( 'in$uenvironment'(X0,appear('efficient$uproducers',X0))
& environment(X0) )
=> subpopulations('first$umovers','efficient$uproducers',X0,appear('efficient$uproducers',X0)) ) ).
fof(mp_difference_between_founding_rates,axiom,
! [X0] :
( ( ~ decreases(difference('disbanding$urate'('first$umovers',X0),'disbanding$urate'('efficient$uproducers',X0)))
& decreases(difference('founding$urate'('first$umovers',X0),'founding$urate'('efficient$uproducers',X0))) )
=> decreases(difference('growth$urate'('first$umovers',X0),'growth$urate'('efficient$uproducers',X0))) ) ).
fof(mp_decreasing_function,axiom,
! [X0,X1,X2] :
( ( greater(X2,X1)
& 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
& 'greater$uor$uequal'(difference('growth$urate'('first$umovers',X2),'growth$urate'('efficient$uproducers',X2)),zero)
& 'in$uenvironment'(X0,X2)
& environment(X0) )
=> ( decreases(difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)))
=> greater(difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)),zero) ) ) ).
fof(mp_negative_growth_rate_difference,axiom,
! [X0] :
( greater(zero,difference('growth$urate'('first$umovers',X0),'growth$urate'('efficient$uproducers',X0)))
<=> greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) ) ).
fof(mp_positive_growth_rate_difference,axiom,
! [X0] :
( greater(difference('growth$urate'('first$umovers',X0),'growth$urate'('efficient$uproducers',X0)),zero)
<=> greater('growth$urate'('first$umovers',X0),'growth$urate'('efficient$uproducers',X0)) ) ).
fof(mp_critical_time_points,axiom,
! [X0,X1] :
( ( greater('critical$upoint'(X0),X1)
& 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
& 'in$uenvironment'(X0,'critical$upoint'(X0))
& environment(X0) )
=> 'in$uenvironment'(X0,X1) ) ).
fof(mp_symmetry_of_subpopulations,axiom,
! [X0,X1] :
( ( subpopulations('first$umovers','efficient$uproducers',X0,X1)
& environment(X0) )
=> subpopulations('efficient$uproducers','first$umovers',X0,X1) ) ).
fof(mp_FM_and_EP_members_EP_appeared,axiom,
! [X0,X1] :
( ( subpopulations('first$umovers','efficient$uproducers',X0,X1)
& environment(X0) )
=> 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0)) ) ).
fof(mp_greater_or_equal,axiom,
! [X0,X1] :
( 'greater$uor$uequal'(X0,X1)
<=> ( X0 = X1
| greater(X0,X1) ) ) ).
fof(mp_relationship_of_growth_rates,axiom,
! [X0,X1] :
( ( ~ greater(zero,difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)))
& subpopulations('first$umovers','efficient$uproducers',X0,X1)
& environment(X0) )
=> 'greater$uor$uequal'(difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)),zero) ) ).
fof(d1,hypothesis,
! [X0,X1] :
( ( X1 = 'critical$upoint'(X0)
& environment(X0) )
=> ( ! [X2] :
( ( greater(X2,X1)
& subpopulations('first$umovers','efficient$uproducers',X0,X2) )
=> greater('growth$urate'('efficient$uproducers',X2),'growth$urate'('first$umovers',X2)) )
& ~ greater('growth$urate'('efficient$uproducers',X1),'growth$urate'('first$umovers',X1)) ) ) ).
fof(a10,hypothesis,
! [X0,X1,X2,X3] :
( ( 'greater$uor$uequal'(X2,X3)
& 'greater$uor$uequal'(X3,X1)
& subpopulations('first$umovers','efficient$uproducers',X0,X2)
& subpopulations('first$umovers','efficient$uproducers',X0,X1)
& environment(X0) )
=> subpopulations('first$umovers','efficient$uproducers',X0,X3) ) ).
fof(a12,hypothesis,
! [X0,X1] :
( ( subpopulations('first$umovers','efficient$uproducers',X0,X1)
& environment(X0) )
=> decreases(difference('founding$urate'('first$umovers',X1),'founding$urate'('efficient$uproducers',X1))) ) ).
fof(prove_t3,conjecture,
! [X0,X1] :
( ( greater('critical$upoint'(X0),X1)
& 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
& 'in$uenvironment'(X0,'critical$upoint'(X0))
& environment(X0) )
=> 'selection$ufavors'('first$umovers','efficient$uproducers',X1) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0,X1] :
( ( greater('critical$upoint'(X0),X1)
& 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
& 'in$uenvironment'(X0,'critical$upoint'(X0))
& environment(X0) )
=> 'selection$ufavors'('first$umovers','efficient$uproducers',X1) ),
inference(negate_conjecture,[status(cth)],[prove_t3]) ).
cnf(c0,plain,
( 'selection$ufavors'(X2,X1,X3)
| ~ greater('growth$urate'(X2,X3),'growth$urate'(X1,X3))
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp1_high_growth_rates]) ).
cnf(c1,plain,
( ~ decreases(difference('disbanding$urate'('first$umovers',X1),'disbanding$urate'('efficient$uproducers',X1)))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[l3]) ).
cnf(c2,plain,
( subpopulations('first$umovers','efficient$uproducers',X0,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_critical_point_means_FM_and_EP]) ).
cnf(c3,plain,
( subpopulations('first$umovers','efficient$uproducers',X0,appear('efficient$uproducers',X0))
| ~ 'in$uenvironment'(X0,appear('efficient$uproducers',X0))
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_FM_and_EP_when_EP_appears]) ).
cnf(c4,plain,
( decreases(difference('growth$urate'('first$umovers',X0),'growth$urate'('efficient$uproducers',X0)))
| decreases(difference('disbanding$urate'('first$umovers',X0),'disbanding$urate'('efficient$uproducers',X0)))
| ~ decreases(difference('founding$urate'('first$umovers',X0),'founding$urate'('efficient$uproducers',X0))) ),
inference(clausification,[status(esa)],[mp_difference_between_founding_rates]) ).
cnf(c5,plain,
( ~ decreases(difference('growth$urate'('first$umovers',X2),'growth$urate'('efficient$uproducers',X2)))
| ~ 'in$uenvironment'(X0,X1)
| ~ 'greater$uor$uequal'(difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)),zero)
| greater(difference('growth$urate'('first$umovers',X2),'growth$urate'('efficient$uproducers',X2)),zero)
| ~ 'greater$uor$uequal'(X2,appear('efficient$uproducers',X0))
| ~ greater(X1,X2)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_decreasing_function]) ).
cnf(c6,plain,
( greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0))
| ~ greater(zero,difference('growth$urate'('first$umovers',X0),'growth$urate'('efficient$uproducers',X0))) ),
inference(clausification,[status(esa)],[mp_negative_growth_rate_difference]) ).
cnf(c8,plain,
( greater('growth$urate'('first$umovers',X0),'growth$urate'('efficient$uproducers',X0))
| ~ greater(difference('growth$urate'('first$umovers',X0),'growth$urate'('efficient$uproducers',X0)),zero) ),
inference(clausification,[status(esa)],[mp_positive_growth_rate_difference]) ).
cnf(c13,plain,
( ~ greater('critical$upoint'(X0),X1)
| ~ 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
| 'in$uenvironment'(X0,X1)
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_critical_time_points]) ).
cnf(c15,plain,
( subpopulations('efficient$uproducers','first$umovers',X0,X1)
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_symmetry_of_subpopulations]) ).
cnf(c16,plain,
( 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_FM_and_EP_members_EP_appeared]) ).
cnf(c17,plain,
( X0 = X1
| greater(X0,X1)
| ~ 'greater$uor$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_or_equal]) ).
cnf(c18,plain,
( ~ greater(X0,X1)
| 'greater$uor$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_or_equal]) ).
cnf(c19,plain,
( X0 != X1
| 'greater$uor$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_or_equal]) ).
cnf(c20,plain,
( 'greater$uor$uequal'(difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)),zero)
| greater(zero,difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_relationship_of_growth_rates]) ).
cnf(c21,plain,
( ~ greater('growth$urate'('efficient$uproducers',X1),'growth$urate'('first$umovers',X1))
| X1 != 'critical$upoint'(X0)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[d1]) ).
cnf(c23,plain,
( ~ environment(X2)
| subpopulations('first$umovers','efficient$uproducers',X2,X1)
| ~ subpopulations('first$umovers','efficient$uproducers',X2,X0)
| ~ 'greater$uor$uequal'(X1,X3)
| ~ subpopulations('first$umovers','efficient$uproducers',X2,X3)
| ~ 'greater$uor$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[a10]) ).
cnf(c24,plain,
( decreases(difference('founding$urate'('first$umovers',X1),'founding$urate'('efficient$uproducers',X1)))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[a12]) ).
cnf(c25,plain,
environment(sK41),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c26,plain,
'in$uenvironment'(sK41,'critical$upoint'(sK41)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c27,plain,
'greater$uor$uequal'(sK42,appear('efficient$uproducers',sK41)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c28,plain,
greater('critical$upoint'(sK41),sK42),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c29,plain,
~ 'selection$ufavors'('first$umovers','efficient$uproducers',sK42),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d_0,plain,
'greater$uor$uequal'('critical$upoint'(sK41),sK42),
inference(resolution,[status(thm)],[c18,c28]) ).
cnf(d_1,plain,
( ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| ~ 'greater$uor$uequal'(X2,X1)
| ~ 'greater$uor$uequal'(X1,'critical$upoint'(X0))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X2)
| subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ),
inference(resolution,[status(thm)],[c23,c2]) ).
cnf(d_2,plain,
( ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| ~ 'greater$uor$uequal'(X1,'critical$upoint'(X0))
| ~ 'greater$uor$uequal'('critical$upoint'(X0),X1)
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ),
inference(resolution,[status(thm)],[d_1,c2]) ).
cnf(d_3,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| ~ environment(sK41) ),
inference(resolution,[status(thm)],[d_2,d_0]) ).
cnf(d_4,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42) ),
inference(resolution,[status(thm)],[c25,d_3]) ).
cnf(d_5,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42) ),
inference(resolution,[status(thm)],[c26,d_4]) ).
cnf(d_6,plain,
( subpopulations('efficient$uproducers','first$umovers',sK41,sK42)
| ~ environment(sK41)
| ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41)) ),
inference(resolution,[status(thm)],[d_5,c15]) ).
cnf(d_7,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| subpopulations('efficient$uproducers','first$umovers',sK41,sK42) ),
inference(resolution,[status(thm)],[c25,d_6]) ).
cnf(d_8,plain,
( ~ 'in$uenvironment'(X0,appear('efficient$uproducers',X0))
| ~ environment(X0)
| ~ 'greater$uor$uequal'(X2,X1)
| ~ 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X2)
| subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ),
inference(resolution,[status(thm)],[c23,c3]) ).
cnf(d_9,plain,
( ~ 'greater$uor$uequal'(X0,sK42)
| ~ 'in$uenvironment'(sK41,appear('efficient$uproducers',sK41))
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| ~ subpopulations('first$umovers','efficient$uproducers',sK41,X0)
| ~ environment(sK41) ),
inference(resolution,[status(thm)],[d_8,c27]) ).
cnf(d_10,plain,
( ~ 'greater$uor$uequal'(X0,sK42)
| ~ 'in$uenvironment'(sK41,appear('efficient$uproducers',sK41))
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| ~ subpopulations('first$umovers','efficient$uproducers',sK41,X0) ),
inference(resolution,[status(thm)],[c25,d_9]) ).
cnf(d_11,plain,
'greater$uor$uequal'(X0,X0),
inference(equality_resolution,[status(thm)],[c19]) ).
cnf(d_12,plain,
( ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| 'in$uenvironment'(X0,appear('efficient$uproducers',X0))
| ~ environment(X0)
| ~ greater('critical$upoint'(X0),appear('efficient$uproducers',X0)) ),
inference(resolution,[status(thm)],[c13,d_11]) ).
cnf(d_13,plain,
( ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| 'greater$uor$uequal'('critical$upoint'(X0),appear('efficient$uproducers',X0))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[c16,c2]) ).
cnf(d_14,plain,
( greater('critical$upoint'(X0),appear('efficient$uproducers',X0))
| 'critical$upoint'(X0) = appear('efficient$uproducers',X0)
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[d_13,c17]) ).
cnf(d_15,plain,
( 'in$uenvironment'(X0,appear('efficient$uproducers',X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| 'critical$upoint'(X0) = appear('efficient$uproducers',X0) ),
inference(resolution,[status(thm)],[d_14,d_12]) ).
cnf(d_16,plain,
( ~ 'greater$uor$uequal'(X0,sK42)
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| ~ subpopulations('first$umovers','efficient$uproducers',sK41,X0)
| ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| ~ environment(sK41)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_15,d_10]) ).
cnf(d_17,plain,
( ~ 'greater$uor$uequal'(X0,sK42)
| ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| ~ subpopulations('first$umovers','efficient$uproducers',sK41,X0)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c25,d_16]) ).
cnf(d_18,plain,
( ~ 'greater$uor$uequal'(X0,sK42)
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| ~ subpopulations('first$umovers','efficient$uproducers',sK41,X0)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c26,d_17]) ).
cnf(d_19,plain,
( ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| ~ environment(sK41)
| ~ 'greater$uor$uequal'('critical$upoint'(sK41),sK42)
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_18,c2]) ).
cnf(d_20,plain,
( ~ 'greater$uor$uequal'('critical$upoint'(sK41),sK42)
| ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c25,d_19]) ).
cnf(d_21,plain,
( ~ 'greater$uor$uequal'('critical$upoint'(sK41),sK42)
| subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c26,d_20]) ).
cnf(d_22,plain,
( subpopulations('first$umovers','efficient$uproducers',sK41,sK42)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_0,d_21]) ).
cnf(d_23,plain,
( subpopulations('efficient$uproducers','first$umovers',sK41,sK42)
| ~ environment(sK41)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_22,c15]) ).
cnf(d_24,plain,
( subpopulations('efficient$uproducers','first$umovers',sK41,sK42)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c25,d_23]) ).
cnf(d_25,plain,
( ~ environment(X0)
| ~ greater('growth$urate'('efficient$uproducers','critical$upoint'(X0)),'growth$urate'('first$umovers','critical$upoint'(X0))) ),
inference(equality_resolution,[status(thm)],[c21]) ).
cnf(d_26,plain,
( ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| 'greater$uor$uequal'(difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0))),zero)
| ~ environment(X0)
| greater(zero,difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0)))) ),
inference(resolution,[status(thm)],[c20,c2]) ).
cnf(d_27,plain,
( ~ 'greater$uor$uequal'(X1,appear('efficient$uproducers',X2))
| ~ 'in$uenvironment'(X2,'critical$upoint'(X0))
| ~ decreases(difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)))
| ~ environment(X2)
| greater(difference('growth$urate'('first$umovers',X1),'growth$urate'('efficient$uproducers',X1)),zero)
| ~ greater('critical$upoint'(X0),X1)
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| greater(zero,difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0)))) ),
inference(resolution,[status(thm)],[d_26,c5]) ).
cnf(d_28,plain,
( decreases(difference('founding$urate'('first$umovers',sK42),'founding$urate'('efficient$uproducers',sK42)))
| ~ environment(sK41)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_22,c24]) ).
cnf(d_29,plain,
( decreases(difference('founding$urate'('first$umovers',sK42),'founding$urate'('efficient$uproducers',sK42)))
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c25,d_28]) ).
cnf(d_30,plain,
( decreases(difference('disbanding$urate'('first$umovers',sK42),'disbanding$urate'('efficient$uproducers',sK42)))
| decreases(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)))
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_29,c4]) ).
cnf(d_31,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',X0,sK42)
| ~ environment(X0)
| decreases(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)))
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_30,c1]) ).
cnf(d_32,plain,
( 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41)
| decreases(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)))
| ~ environment(sK41)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_31,d_22]) ).
cnf(d_33,plain,
( decreases(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)))
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c25,d_32]) ).
cnf(d_34,plain,
( ~ 'greater$uor$uequal'(sK42,appear('efficient$uproducers',X1))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X1,'critical$upoint'(X0))
| ~ environment(X0)
| ~ environment(X1)
| greater(zero,difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0))))
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_33,d_27]) ).
cnf(d_35,plain,
( ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ environment(X0)
| ~ environment(sK41)
| greater(zero,difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0))))
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_34,c27]) ).
cnf(d_36,plain,
( ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| greater(zero,difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0))))
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c25,d_35]) ).
cnf(d_37,plain,
( greater('growth$urate'('efficient$uproducers','critical$upoint'(X0)),'growth$urate'('first$umovers','critical$upoint'(X0)))
| ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_36,c6]) ).
cnf(d_38,plain,
( ~ environment(X0)
| ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_37,d_25]) ).
cnf(d_39,plain,
( ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| ~ environment(sK41)
| ~ greater('critical$upoint'(sK41),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_38,c26]) ).
cnf(d_40,plain,
( ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| ~ greater('critical$upoint'(sK41),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c25,d_39]) ).
cnf(d_41,plain,
( ~ greater('critical$upoint'(sK41),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c26,d_40]) ).
cnf(d_42,plain,
( greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c28,d_41]) ).
cnf(d_43,plain,
( greater('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42))
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_42,c8]) ).
cnf(d_44,plain,
( 'selection$ufavors'('first$umovers','efficient$uproducers',sK42)
| ~ subpopulations('efficient$uproducers','first$umovers',X0,sK42)
| ~ environment(X0)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_43,c0]) ).
cnf(d_45,plain,
( ~ subpopulations('efficient$uproducers','first$umovers',X0,sK42)
| ~ environment(X0)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[c29,d_44]) ).
cnf(d_46,plain,
( 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41)
| ~ environment(sK41)
| 'critical$upoint'(sK41) = appear('efficient$uproducers',sK41) ),
inference(resolution,[status(thm)],[d_45,d_24]) ).
cnf(d_47,plain,
'critical$upoint'(sK41) = appear('efficient$uproducers',sK41),
inference(resolution,[status(thm)],[c25,d_46]) ).
cnf(d_48,plain,
'greater$uor$uequal'(sK42,'critical$upoint'(sK41)),
inference(demodulation,[status(thm)],[c27,d_47]) ).
cnf(d_49,plain,
subpopulations('efficient$uproducers','first$umovers',sK41,sK42),
inference(resolution,[status(thm)],[d_48,d_7]) ).
cnf(d_50,plain,
( decreases(difference('founding$urate'('first$umovers',sK42),'founding$urate'('efficient$uproducers',sK42)))
| ~ environment(sK41)
| ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41)) ),
inference(resolution,[status(thm)],[d_5,c24]) ).
cnf(d_51,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| decreases(difference('founding$urate'('first$umovers',sK42),'founding$urate'('efficient$uproducers',sK42))) ),
inference(resolution,[status(thm)],[c25,d_50]) ).
cnf(d_52,plain,
( decreases(difference('disbanding$urate'('first$umovers',sK42),'disbanding$urate'('efficient$uproducers',sK42)))
| decreases(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)))
| ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41)) ),
inference(resolution,[status(thm)],[d_51,c4]) ).
cnf(d_53,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',X0,sK42)
| ~ environment(X0)
| ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| decreases(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42))) ),
inference(resolution,[status(thm)],[d_52,c1]) ).
cnf(d_54,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| decreases(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)))
| ~ environment(sK41) ),
inference(resolution,[status(thm)],[d_53,d_5]) ).
cnf(d_55,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| decreases(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42))) ),
inference(resolution,[status(thm)],[c25,d_54]) ).
cnf(d_56,plain,
( ~ 'greater$uor$uequal'(sK42,appear('efficient$uproducers',X1))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X1,'critical$upoint'(X0))
| ~ environment(X0)
| ~ environment(X1)
| greater(zero,difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0))))
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41)) ),
inference(resolution,[status(thm)],[d_55,d_27]) ).
cnf(d_57,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ environment(X0)
| ~ environment(sK41)
| greater(zero,difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0))))
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero) ),
inference(resolution,[status(thm)],[d_56,c27]) ).
cnf(d_58,plain,
( ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| greater(zero,difference('growth$urate'('first$umovers','critical$upoint'(X0)),'growth$urate'('efficient$uproducers','critical$upoint'(X0))))
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero) ),
inference(resolution,[status(thm)],[c25,d_57]) ).
cnf(d_59,plain,
( greater('growth$urate'('efficient$uproducers','critical$upoint'(X0)),'growth$urate'('first$umovers','critical$upoint'(X0)))
| ~ 'greater$uor$uequal'(sK42,'critical$upoint'(sK41))
| ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero) ),
inference(resolution,[status(thm)],[d_58,c6]) ).
cnf(d_60,plain,
( ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero)
| greater('growth$urate'('efficient$uproducers','critical$upoint'(X0)),'growth$urate'('first$umovers','critical$upoint'(X0))) ),
inference(resolution,[status(thm)],[d_48,d_59]) ).
cnf(d_61,plain,
( ~ environment(X0)
| ~ 'in$uenvironment'(sK41,'critical$upoint'(X0))
| ~ 'in$uenvironment'(X0,'critical$upoint'(X0))
| ~ environment(X0)
| ~ greater('critical$upoint'(X0),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero) ),
inference(resolution,[status(thm)],[d_60,d_25]) ).
cnf(d_62,plain,
( ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| ~ environment(sK41)
| ~ greater('critical$upoint'(sK41),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero) ),
inference(resolution,[status(thm)],[d_61,c26]) ).
cnf(d_63,plain,
( ~ 'in$uenvironment'(sK41,'critical$upoint'(sK41))
| ~ greater('critical$upoint'(sK41),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero) ),
inference(resolution,[status(thm)],[c25,d_62]) ).
cnf(d_64,plain,
( ~ greater('critical$upoint'(sK41),sK42)
| greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero) ),
inference(resolution,[status(thm)],[c26,d_63]) ).
cnf(d_65,plain,
greater(difference('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),zero),
inference(resolution,[status(thm)],[c28,d_64]) ).
cnf(d_66,plain,
greater('growth$urate'('first$umovers',sK42),'growth$urate'('efficient$uproducers',sK42)),
inference(resolution,[status(thm)],[d_65,c8]) ).
cnf(d_67,plain,
( 'selection$ufavors'('first$umovers','efficient$uproducers',sK42)
| ~ subpopulations('efficient$uproducers','first$umovers',X0,sK42)
| ~ environment(X0) ),
inference(resolution,[status(thm)],[d_66,c0]) ).
cnf(d_68,plain,
( ~ subpopulations('efficient$uproducers','first$umovers',X0,sK42)
| ~ environment(X0) ),
inference(resolution,[status(thm)],[c29,d_67]) ).
cnf(d_69,plain,
~ environment(sK41),
inference(resolution,[status(thm)],[d_68,d_49]) ).
cnf(d_70,plain,
$false,
inference(resolution,[status(thm)],[c25,d_69]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT034+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/15.46 % Computer : n026.cluster.edu
% 0.18/15.46 % Model : x86_64 x86_64
% 0.18/15.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/15.46 % Memory : 8046.5625MB
% 0.18/15.46 % OS : Linux 6.8.0-71-generic
% 0.18/15.46 % CPULimit : 300
% 0.18/15.46 % WCLimit : 300
% 0.18/15.46 % DateTime : Sat Sep 26 00:08:41 UTC 2026
% 0.18/15.46 % CPUTime :
% 0.18/15.46 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.89/19.26 % SZS status Theorem for theBenchmark.p
% 28.89/19.26 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------