%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT025+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:04 AM UTC 2026
% Result : Theorem 12.79s 2.23s
% Output : CNFRefutation 12.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT025+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Sat Sep 26 00:04:06 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.79/2.23 % SZS status Theorem for theBenchmark.p
% 12.79/2.23 % SZS output start CNFRefutation for theBenchmark.p
% 12.79/2.23 fof(mp_only_members, axiom, ! [X0] : ! [X1] : ! [X2] : (((environment(X0) & (subpopulation(X1,X0,X2) & (greater('cardinality$uat$utime'(X1,X2),zero) => (X1 = 'efficient$uproducers' | X1 = 'first$umovers')))) => 'number$uof$uorganizations'(X0,X2) = sum('cardinality$uat$utime'('first$umovers',X2),'cardinality$uat$utime'('efficient$uproducers',X2))))).
% 12.79/2.23 fof(mp_subpopulations, axiom, ! [X0] : ! [X1] : (((environment(X0) & 'in$uenvironment'(X0,X1)) => (subpopulation('first$umovers',X0,X1) & subpopulation('efficient$uproducers',X0,X1))))).
% 12.79/2.23 fof(mp_abc_sum_increase, axiom, ! [X0] : ! [X1] : ! [X2] : (((X0 = sum(X1,X2) & constant(X0)) => ((constant(X1) & constant(X2)) | ((increases(X1) & decreases(X2)) | (decreases(X1) & increases(X2))))))).
% 12.79/2.23 fof(mp_growth_rate, axiom, ! [X0] : ! [X1] : ! [X2] : (((environment(X1) & ('in$uenvironment'(X1,X2) & (subpopulation(X0,X1,X2) & greater('cardinality$uat$utime'(X0,X2),zero)))) => ((constant('cardinality$uat$utime'(X0,X2)) => 'growth$urate'(X0,X2) = zero) & ((increases('cardinality$uat$utime'(X0,X2)) => greater('growth$urate'(X0,X2),zero)) & (decreases('cardinality$uat$utime'(X0,X2)) => greater(zero,'growth$urate'(X0,X2)))))))).
% 12.79/2.23 fof(mp_non_zero_producers, axiom, ! [X0] : ! [X1] : (((environment(X0) & subpopulations('first$umovers','efficient$uproducers',X0,X1)) => (greater('cardinality$uat$utime'('first$umovers',X1),zero) & greater('cardinality$uat$utime'('efficient$uproducers',X1),zero))))).
% 12.79/2.23 fof(mp_time_point_occur, axiom, ! [X0] : ! [X1] : (((environment(X0) & subpopulations('first$umovers','efficient$uproducers',X0,X1)) => 'in$uenvironment'(X0,X1)))).
% 12.79/2.23 fof(prove_l7, conjecture, ! [X0] : ! [X1] : (((environment(X0) & (subpopulations('first$umovers','efficient$uproducers',X0,X1) & constant('number$uof$uorganizations'(X0,X1)))) => (('growth$urate'('first$umovers',X1) = zero & 'growth$urate'('efficient$uproducers',X1) = zero) | ((greater('growth$urate'('first$umovers',X1),zero) & greater(zero,'growth$urate'('efficient$uproducers',X1))) | (greater('growth$urate'('efficient$uproducers',X1),zero) & greater(zero,'growth$urate'('first$umovers',X1)))))))).
% 12.79/2.23 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : (((environment(X0) & (subpopulations('first$umovers','efficient$uproducers',X0,X1) & constant('number$uof$uorganizations'(X0,X1)))) => (('growth$urate'('first$umovers',X1) = zero & 'growth$urate'('efficient$uproducers',X1) = zero) | ((greater('growth$urate'('first$umovers',X1),zero) & greater(zero,'growth$urate'('efficient$uproducers',X1))) | (greater('growth$urate'('efficient$uproducers',X1),zero) & greater(zero,'growth$urate'('first$umovers',X1))))))), inference(negate_conjecture, [status(cth)], [prove_l7])).
% 12.79/2.23 cnf(c1, plain, ~subpopulation(X0,X1,X2) | X0 != 'first$umovers' | ~environment(X1) | sum('cardinality$uat$utime'('first$umovers',X2),'cardinality$uat$utime'('efficient$uproducers',X2)) = 'number$uof$uorganizations'(X1,X2), inference(clausification, [status(esa)], [mp_only_members])).
% 12.79/2.23 cnf(c3, plain, ~'in$uenvironment'(X0,X1) | ~environment(X0) | subpopulation('first$umovers',X0,X1), inference(clausification, [status(esa)], [mp_subpopulations])).
% 12.79/2.23 cnf(c4, plain, ~'in$uenvironment'(X0,X1) | ~environment(X0) | subpopulation('efficient$uproducers',X0,X1), inference(clausification, [status(esa)], [mp_subpopulations])).
% 12.79/2.23 cnf(c5, plain, X0(X1,X2,X3) | constant(X2), inference(clausification, [status(esa)], [mp_abc_sum_increase])).
% 12.79/2.23 cnf(c6, plain, X0(X1,X2,X3) | constant(X3), inference(clausification, [status(esa)], [mp_abc_sum_increase])).
% 12.79/2.23 cnf(c7, plain, decreases(X0) | increases(X0) | ~X1(X2,X0,X3) | sum(X0,X3) != X2 | ~constant(X2), inference(clausification, [status(esa)], [mp_abc_sum_increase])).
% 12.79/2.23 cnf(c8, plain, increases(X0) | increases(X1) | ~X2(X3,X1,X0) | sum(X1,X0) != X3 | ~constant(X3), inference(clausification, [status(esa)], [mp_abc_sum_increase])).
% 12.79/2.23 cnf(c9, plain, decreases(X0) | ~X1(X2,X0,X3) | sum(X0,X3) != X2 | decreases(X3) | ~constant(X2), inference(clausification, [status(esa)], [mp_abc_sum_increase])).
% 12.79/2.23 cnf(c10, plain, increases(X0) | ~X1(X2,X3,X0) | sum(X3,X0) != X2 | decreases(X0) | ~constant(X2), inference(clausification, [status(esa)], [mp_abc_sum_increase])).
% 12.79/2.23 cnf(c11, plain, ~environment(X0) | ~'in$uenvironment'(X0,X1) | ~subpopulation(X2,X0,X1) | ~greater('cardinality$uat$utime'(X2,X1),zero) | 'growth$urate'(X2,X1) = zero | ~constant('cardinality$uat$utime'(X2,X1)), inference(clausification, [status(esa)], [mp_growth_rate])).
% 12.79/2.23 cnf(c12, plain, greater(zero,'growth$urate'(X0,X1)) | ~environment(X2) | ~'in$uenvironment'(X2,X1) | ~decreases('cardinality$uat$utime'(X0,X1)) | ~subpopulation(X0,X2,X1) | ~greater('cardinality$uat$utime'(X0,X1),zero), inference(clausification, [status(esa)], [mp_growth_rate])).
% 12.79/2.23 cnf(c13, plain, ~'in$uenvironment'(X0,X1) | ~subpopulation(X2,X0,X1) | ~greater('cardinality$uat$utime'(X2,X1),zero) | ~increases('cardinality$uat$utime'(X2,X1)) | ~environment(X0) | greater('growth$urate'(X2,X1),zero), inference(clausification, [status(esa)], [mp_growth_rate])).
% 12.79/2.23 cnf(c14, plain, ~subpopulations('first$umovers','efficient$uproducers',X0,X1) | ~environment(X0) | greater('cardinality$uat$utime'('first$umovers',X1),zero), inference(clausification, [status(esa)], [mp_non_zero_producers])).
% 12.79/2.23 cnf(c15, plain, ~subpopulations('first$umovers','efficient$uproducers',X0,X1) | ~environment(X0) | greater('cardinality$uat$utime'('efficient$uproducers',X1),zero), inference(clausification, [status(esa)], [mp_non_zero_producers])).
% 12.79/2.23 cnf(c16, plain, ~subpopulations('first$umovers','efficient$uproducers',X0,X1) | ~environment(X0) | 'in$uenvironment'(X0,X1), inference(clausification, [status(esa)], [mp_time_point_occur])).
% 12.79/2.23 cnf(c18, plain, subpopulations('first$umovers','efficient$uproducers',sK19,sK20), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.79/2.23 cnf(c19, plain, constant('number$uof$uorganizations'(sK19,sK20)), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.79/2.23 cnf(c20, plain, environment(sK19), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.79/2.23 cnf(c21, plain, ~greater('growth$urate'('first$umovers',sK20),zero) | ~greater(zero,'growth$urate'('efficient$uproducers',sK20)), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.79/2.23 cnf(c22, plain, ~greater('growth$urate'('efficient$uproducers',sK20),zero) | ~greater(zero,'growth$urate'('first$umovers',sK20)), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.79/2.23 cnf(c23, plain, 'growth$urate'('first$umovers',sK20) != zero | 'growth$urate'('efficient$uproducers',sK20) != zero, inference(clausification, [status(esa)], [negated_conjecture])).
% 12.79/2.23 cnf(d0, plain, ~environment(sK19) | 'in$uenvironment'(sK19,sK20), inference(resolution, [status(thm)], [c16,c18])).
% 12.79/2.23 cnf(d1, plain, 'in$uenvironment'(sK19,sK20), inference(resolution, [status(thm)], [c20,d0])).
% 12.79/2.23 cnf(d2, plain, ~environment(sK19) | greater('cardinality$uat$utime'('first$umovers',sK20),zero), inference(resolution, [status(thm)], [c14,c18])).
% 12.79/2.23 cnf(d3, plain, greater('cardinality$uat$utime'('first$umovers',sK20),zero), inference(resolution, [status(thm)], [c20,d2])).
% 12.79/2.23 cnf(d4, plain, 'growth$urate'('first$umovers',sK20) = zero | ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | ~'in$uenvironment'(X0,sK20) | ~constant('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c11,d3])).
% 12.79/2.23 cnf(d5, plain, ~environment(sK19) | greater('cardinality$uat$utime'('efficient$uproducers',sK20),zero), inference(resolution, [status(thm)], [c15,c18])).
% 12.79/2.23 cnf(d6, plain, greater('cardinality$uat$utime'('efficient$uproducers',sK20),zero), inference(resolution, [status(thm)], [c20,d5])).
% 12.79/2.23 cnf(d7, plain, 'growth$urate'('efficient$uproducers',sK20) = zero | ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | ~'in$uenvironment'(X0,sK20) | ~constant('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c11,d6])).
% 12.79/2.23 cnf(d8, plain, ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | greater(zero,'growth$urate'('first$umovers',sK20)) | ~'in$uenvironment'(X0,sK20) | ~decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c12,d3])).
% 12.79/2.23 cnf(d9, plain, ~constant(sum(X0,X1)) | ~'Ts5'(sum(X0,X1),X0,X1) | decreases(X1) | decreases(X0), inference(equality_resolution, [status(thm)], [c9])).
% 12.79/2.23 cnf(d10, plain, ~constant(sum(X0,X1)) | decreases(X1) | decreases(X0) | constant(X1), inference(resolution, [status(thm)], [d9,c6])).
% 12.79/2.23 cnf(d11, plain, sum('cardinality$uat$utime'('first$umovers',X0),'cardinality$uat$utime'('efficient$uproducers',X0)) = 'number$uof$uorganizations'(X1,X0) | ~environment(X1) | ~subpopulation('first$umovers',X1,X0), inference(equality_resolution, [status(thm)], [c1])).
% 12.79/2.23 cnf(d12, plain, sum('cardinality$uat$utime'('first$umovers',X0),'cardinality$uat$utime'('efficient$uproducers',X0)) = 'number$uof$uorganizations'(X1,X0) | ~environment(X1) | ~environment(X1) | ~'in$uenvironment'(X1,X0), inference(resolution, [status(thm)], [d11,c3])).
% 12.79/2.23 cnf(d13, plain, sum('cardinality$uat$utime'('first$umovers',sK20),'cardinality$uat$utime'('efficient$uproducers',sK20)) = 'number$uof$uorganizations'(sK19,sK20) | ~environment(sK19), inference(resolution, [status(thm)], [d12,d1])).
% 12.79/2.23 cnf(d14, plain, sum('cardinality$uat$utime'('first$umovers',sK20),'cardinality$uat$utime'('efficient$uproducers',sK20)) = 'number$uof$uorganizations'(sK19,sK20), inference(resolution, [status(thm)], [c20,d13])).
% 12.79/2.23 cnf(d15, plain, ~constant('number$uof$uorganizations'(sK19,sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(superposition, [status(thm)], [d14,d10])).
% 12.79/2.23 cnf(d16, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)) | decreases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c19,d15])).
% 12.79/2.23 cnf(d17, plain, ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | ~'in$uenvironment'(X0,sK20) | ~decreases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c12,d6])).
% 12.79/2.23 cnf(d18, plain, ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d17,d16])).
% 12.79/2.23 cnf(d19, plain, ~environment(X0) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d18,c4])).
% 12.79/2.23 cnf(d20, plain, ~environment(sK19) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d19,d1])).
% 12.79/2.23 cnf(d21, plain, greater(zero,'growth$urate'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c20,d20])).
% 12.79/2.23 cnf(d22, plain, ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | greater('growth$urate'('first$umovers',sK20),zero) | ~'in$uenvironment'(X0,sK20) | ~increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c13,d3])).
% 12.79/2.23 cnf(d23, plain, ~constant(sum(X0,X1)) | ~'Ts5'(sum(X0,X1),X0,X1) | increases(X0) | decreases(X0), inference(equality_resolution, [status(thm)], [c7])).
% 12.79/2.23 cnf(d24, plain, ~constant(sum(X0,X1)) | increases(X0) | decreases(X0) | constant(X1), inference(resolution, [status(thm)], [d23,c6])).
% 12.79/2.23 cnf(d25, plain, ~constant('number$uof$uorganizations'(sK19,sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(superposition, [status(thm)], [d14,d24])).
% 12.79/2.23 cnf(d26, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c19,d25])).
% 12.79/2.23 cnf(d27, plain, ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | greater(zero,'growth$urate'('first$umovers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d8,d26])).
% 12.79/2.23 cnf(d28, plain, ~environment(X0) | greater(zero,'growth$urate'('first$umovers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d27,c3])).
% 12.79/2.23 cnf(d29, plain, ~environment(sK19) | greater(zero,'growth$urate'('first$umovers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d28,d1])).
% 12.79/2.23 cnf(d30, plain, greater(zero,'growth$urate'('first$umovers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c20,d29])).
% 12.79/2.23 cnf(d31, plain, ~constant(sum(X0,X1)) | ~'Ts5'(sum(X0,X1),X0,X1) | increases(X1) | increases(X0), inference(equality_resolution, [status(thm)], [c8])).
% 12.79/2.23 cnf(d32, plain, ~constant(sum(X0,X1)) | increases(X1) | increases(X0) | constant(X1), inference(resolution, [status(thm)], [d31,c6])).
% 12.79/2.23 cnf(d33, plain, ~constant('number$uof$uorganizations'(sK19,sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(superposition, [status(thm)], [d14,d32])).
% 12.79/2.23 cnf(d34, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c19,d33])).
% 12.79/2.23 cnf(d35, plain, ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater('growth$urate'('efficient$uproducers',sK20),zero) | ~'in$uenvironment'(X0,sK20) | ~increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c13,d6])).
% 12.79/2.23 cnf(d36, plain, ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater('growth$urate'('efficient$uproducers',sK20),zero) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d35,d34])).
% 12.79/2.23 cnf(d37, plain, ~environment(X0) | greater('growth$urate'('efficient$uproducers',sK20),zero) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d36,c4])).
% 12.79/2.23 cnf(d38, plain, ~environment(sK19) | greater('growth$urate'('efficient$uproducers',sK20),zero) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d37,d1])).
% 12.79/2.23 cnf(d39, plain, greater('growth$urate'('efficient$uproducers',sK20),zero) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c20,d38])).
% 12.79/2.23 cnf(d40, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | ~greater(zero,'growth$urate'('first$umovers',sK20)), inference(resolution, [status(thm)], [d39,c22])).
% 12.79/2.23 cnf(d41, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d40,d30])).
% 12.79/2.23 cnf(d42, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | greater('growth$urate'('first$umovers',sK20),zero) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d41,d22])).
% 12.79/2.23 cnf(d43, plain, ~environment(X0) | greater('growth$urate'('first$umovers',sK20),zero) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d42,c3])).
% 12.79/2.23 cnf(d44, plain, ~environment(sK19) | greater('growth$urate'('first$umovers',sK20),zero) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d43,d1])).
% 12.79/2.23 cnf(d45, plain, greater('growth$urate'('first$umovers',sK20),zero) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c20,d44])).
% 12.79/2.23 cnf(d46, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~greater(zero,'growth$urate'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d45,c21])).
% 12.79/2.23 cnf(d47, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d46,d21])).
% 12.79/2.23 cnf(d48, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | greater(zero,'growth$urate'('first$umovers',sK20)) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d47,d8])).
% 12.79/2.23 cnf(d49, plain, ~environment(X0) | greater(zero,'growth$urate'('first$umovers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d48,c3])).
% 12.79/2.23 cnf(d50, plain, ~environment(sK19) | greater(zero,'growth$urate'('first$umovers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d49,d1])).
% 12.79/2.23 cnf(d51, plain, greater(zero,'growth$urate'('first$umovers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c20,d50])).
% 12.79/2.23 cnf(d52, plain, ~constant(sum(X0,X1)) | ~'Ts5'(sum(X0,X1),X0,X1) | increases(X1) | decreases(X1), inference(equality_resolution, [status(thm)], [c10])).
% 12.79/2.23 cnf(d53, plain, ~constant(sum(X0,X1)) | increases(X1) | decreases(X1) | constant(X1), inference(resolution, [status(thm)], [d52,c6])).
% 12.79/2.23 cnf(d54, plain, ~constant('number$uof$uorganizations'(sK19,sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(superposition, [status(thm)], [d14,d53])).
% 12.79/2.23 cnf(d55, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c19,d54])).
% 12.79/2.23 cnf(d56, plain, ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d17,d55])).
% 12.79/2.23 cnf(d57, plain, ~environment(X0) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d56,c4])).
% 12.79/2.23 cnf(d58, plain, ~environment(sK19) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d57,d1])).
% 12.79/2.23 cnf(d59, plain, greater(zero,'growth$urate'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c20,d58])).
% 12.79/2.23 cnf(d60, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d46,d59])).
% 12.79/2.23 cnf(d61, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater('growth$urate'('efficient$uproducers',sK20),zero) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d60,d35])).
% 12.79/2.23 cnf(d62, plain, ~environment(X0) | greater('growth$urate'('efficient$uproducers',sK20),zero) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d61,c4])).
% 12.79/2.23 cnf(d63, plain, ~environment(sK19) | greater('growth$urate'('efficient$uproducers',sK20),zero) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d62,d1])).
% 12.79/2.23 cnf(d64, plain, greater('growth$urate'('efficient$uproducers',sK20),zero) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c20,d63])).
% 12.79/2.23 cnf(d65, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~greater(zero,'growth$urate'('first$umovers',sK20)), inference(resolution, [status(thm)], [d64,c22])).
% 12.79/2.23 cnf(d66, plain, constant('cardinality$uat$utime'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d65,d51])).
% 12.79/2.23 cnf(d67, plain, 'growth$urate'('efficient$uproducers',sK20) = zero | ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d66,d7])).
% 12.79/2.23 cnf(d68, plain, 'growth$urate'('efficient$uproducers',sK20) = zero | ~environment(X0) | ~'in$uenvironment'(X0,sK20) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d67,c4])).
% 12.79/2.23 cnf(d69, plain, 'growth$urate'('efficient$uproducers',sK20) = zero | ~environment(sK19), inference(resolution, [status(thm)], [d68,d1])).
% 12.79/2.23 cnf(d70, plain, 'growth$urate'('efficient$uproducers',sK20) = zero, inference(resolution, [status(thm)], [c20,d69])).
% 12.79/2.23 cnf(d71, plain, 'growth$urate'('first$umovers',sK20) != zero, inference(resolution, [status(thm)], [d70,c23])).
% 12.79/2.23 cnf(d72, plain, ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | ~'in$uenvironment'(X0,sK20) | ~constant('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d71,d4])).
% 12.79/2.23 cnf(d73, plain, ~constant(sum(X0,X1)) | increases(X0) | decreases(X0) | constant(X0), inference(resolution, [status(thm)], [d23,c5])).
% 12.79/2.23 cnf(d74, plain, ~constant('number$uof$uorganizations'(sK19,sK20)) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(superposition, [status(thm)], [d14,d73])).
% 12.79/2.23 cnf(d75, plain, constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | decreases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c19,d74])).
% 12.79/2.23 cnf(d76, plain, ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | greater(zero,'growth$urate'('first$umovers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d8,d75])).
% 12.79/2.23 cnf(d77, plain, ~environment(X0) | greater(zero,'growth$urate'('first$umovers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d76,c3])).
% 12.79/2.23 cnf(d78, plain, ~environment(sK19) | greater(zero,'growth$urate'('first$umovers',sK20)) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d77,d1])).
% 12.79/2.23 cnf(d79, plain, greater(zero,'growth$urate'('first$umovers',sK20)) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c20,d78])).
% 12.79/2.23 cnf(d80, plain, ~greater(zero,'growth$urate'('first$umovers',sK20)) | ~greater(zero,zero), inference(demodulation, [status(thm)], [c22,d70])).
% 12.79/2.23 cnf(d81, plain, ~greater(zero,zero) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d80,d79])).
% 12.79/2.23 cnf(d82, plain, ~constant(sum(X0,X1)) | increases(X1) | decreases(X1) | constant(X0), inference(resolution, [status(thm)], [d52,c5])).
% 12.79/2.23 cnf(d83, plain, ~constant('number$uof$uorganizations'(sK19,sK20)) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(superposition, [status(thm)], [d14,d82])).
% 12.79/2.23 cnf(d84, plain, constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)) | decreases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c19,d83])).
% 12.79/2.23 cnf(d85, plain, ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d17,d84])).
% 12.79/2.23 cnf(d86, plain, ~environment(X0) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d85,c4])).
% 12.79/2.23 cnf(d87, plain, ~environment(sK19) | greater(zero,'growth$urate'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [d86,d1])).
% 12.79/2.23 cnf(d88, plain, greater(zero,'growth$urate'('efficient$uproducers',sK20)) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(resolution, [status(thm)], [c20,d87])).
% 12.79/2.23 cnf(d89, plain, greater(zero,zero) | constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(demodulation, [status(thm)], [d88,d70])).
% 12.79/2.23 cnf(d90, plain, ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater(zero,zero) | ~'in$uenvironment'(X0,sK20) | ~increases('cardinality$uat$utime'('efficient$uproducers',sK20)), inference(demodulation, [status(thm)], [d35,d70])).
% 12.79/2.23 cnf(d91, plain, ~environment(X0) | ~subpopulation('efficient$uproducers',X0,sK20) | greater(zero,zero) | ~'in$uenvironment'(X0,sK20) | greater(zero,zero) | constant('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d90,d89])).
% 12.79/2.23 cnf(d92, plain, ~environment(X0) | greater(zero,zero) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('first$umovers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d91,c4])).
% 12.79/2.23 cnf(d93, plain, ~environment(sK19) | greater(zero,zero) | constant('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d92,d1])).
% 12.79/2.23 cnf(d94, plain, greater(zero,zero) | constant('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c20,d93])).
% 12.79/2.23 cnf(d95, plain, greater(zero,zero) | ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d94,d72])).
% 12.79/2.23 cnf(d96, plain, ~environment(X0) | greater(zero,zero) | ~'in$uenvironment'(X0,sK20) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d95,c3])).
% 12.79/2.23 cnf(d97, plain, ~environment(sK19) | greater(zero,zero), inference(resolution, [status(thm)], [d96,d1])).
% 12.79/2.23 cnf(d98, plain, greater(zero,zero), inference(resolution, [status(thm)], [c20,d97])).
% 12.79/2.23 cnf(d99, plain, constant('cardinality$uat$utime'('first$umovers',sK20)) | increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d98,d81])).
% 12.79/2.23 cnf(d100, plain, ~greater(zero,zero) | ~greater('growth$urate'('first$umovers',sK20),zero), inference(demodulation, [status(thm)], [c21,d70])).
% 12.79/2.23 cnf(d101, plain, ~greater('growth$urate'('first$umovers',sK20),zero), inference(resolution, [status(thm)], [d98,d100])).
% 12.79/2.23 cnf(d102, plain, ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | ~'in$uenvironment'(X0,sK20) | ~increases('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d101,d22])).
% 12.79/2.23 cnf(d103, plain, ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d102,d99])).
% 12.79/2.23 cnf(d104, plain, ~environment(X0) | ~'in$uenvironment'(X0,sK20) | constant('cardinality$uat$utime'('first$umovers',sK20)) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d103,c3])).
% 12.79/2.23 cnf(d105, plain, ~environment(sK19) | constant('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [d104,d1])).
% 12.79/2.23 cnf(d106, plain, constant('cardinality$uat$utime'('first$umovers',sK20)), inference(resolution, [status(thm)], [c20,d105])).
% 12.79/2.23 cnf(d107, plain, ~environment(X0) | ~subpopulation('first$umovers',X0,sK20) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d106,d72])).
% 12.79/2.23 cnf(d108, plain, ~environment(X0) | ~'in$uenvironment'(X0,sK20) | ~environment(X0) | ~'in$uenvironment'(X0,sK20), inference(resolution, [status(thm)], [d107,c3])).
% 12.79/2.23 cnf(d109, plain, ~environment(sK19), inference(resolution, [status(thm)], [d108,d1])).
% 12.79/2.23 cnf(d110, plain, $false, inference(resolution, [status(thm)], [c20,d109])).
% 12.79/2.23 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------