%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT024+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n017.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:04:30 AM UTC 2026
% Result : Theorem 0.25s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT024+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.35 % Computer : n017.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 7 12:03:24 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.25/0.47 start to proof:theBenchmark.p
% 0.25/0.55 % Version : CSI_E---1.1
% 0.25/0.55 % Problem : theBenchmark.p
% 0.25/0.55 % Proof found!
% 0.25/0.55 % SZS status Theorem for theBenchmark.p
% 0.25/0.55 % SZS output start Proof
% 0.25/0.55 fof(prove_l6, conjecture, ![X1, X2]:((((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X2))&greater_or_equal(X2,equilibrium(X1)))=>((growth_rate(first_movers,X2)=zero&growth_rate(efficient_producers,X2)=zero)|(greater(growth_rate(first_movers,X2),zero)&greater(zero,growth_rate(efficient_producers,X2)))|(greater(growth_rate(efficient_producers,X2),zero)&greater(zero,growth_rate(first_movers,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l6)).
% 0.25/0.55 fof(mp_equilibrium, axiom, ![X1, X2]:(((environment(X1)&greater_or_equal(X2,equilibrium(X1)))=>~(greater(equilibrium(X1),X2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_equilibrium)).
% 0.25/0.55 fof(a3, hypothesis, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&greater(number_of_organizations(X1,X2),zero))=>((greater(equilibrium(X1),X2)=>decreases(resources(X1,X2)))&(~(greater(equilibrium(X1),X2))=>constant(resources(X1,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a3)).
% 0.25/0.55 fof(mp_positive_number_of_organizations, axiom, ![X1, X2]:(((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X2))=>greater(number_of_organizations(X1,X2),zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_positive_number_of_organizations)).
% 0.25/0.55 fof(mp_time_point_occur, axiom, ![X1, X2]:(((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X2))=>in_environment(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_time_point_occur)).
% 0.25/0.55 fof(a6, hypothesis, ![X1, X2]:(((environment(X1)&in_environment(X1,X2))=>((decreases(resources(X1,X2))=>~(decreases(number_of_organizations(X1,X2))))&(constant(resources(X1,X2))=>constant(number_of_organizations(X1,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a6)).
% 0.25/0.55 fof(l7, hypothesis, ![X1, X2]:((((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X2))&constant(number_of_organizations(X1,X2)))=>((growth_rate(first_movers,X2)=zero&growth_rate(efficient_producers,X2)=zero)|(greater(growth_rate(first_movers,X2),zero)&greater(zero,growth_rate(efficient_producers,X2)))|(greater(growth_rate(efficient_producers,X2),zero)&greater(zero,growth_rate(first_movers,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l7)).
% 0.25/0.55 fof(c_0_7, negated_conjecture, ~(![X1, X2]:((((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X2))&greater_or_equal(X2,equilibrium(X1)))=>((growth_rate(first_movers,X2)=zero&growth_rate(efficient_producers,X2)=zero)|(greater(growth_rate(first_movers,X2),zero)&greater(zero,growth_rate(efficient_producers,X2)))|(greater(growth_rate(efficient_producers,X2),zero)&greater(zero,growth_rate(first_movers,X2))))))), inference(assume_negation,[status(cth)],[prove_l6])).
% 0.25/0.55 fof(c_0_8, plain, ![X1, X2]:(((environment(X1)&greater_or_equal(X2,equilibrium(X1)))=>~greater(equilibrium(X1),X2))), inference(fof_simplification,[status(thm)],[mp_equilibrium])).
% 0.25/0.55 fof(c_0_9, hypothesis, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&greater(number_of_organizations(X1,X2),zero))=>((greater(equilibrium(X1),X2)=>decreases(resources(X1,X2)))&(~greater(equilibrium(X1),X2)=>constant(resources(X1,X2)))))), inference(fof_simplification,[status(thm)],[a3])).
% 0.25/0.55 fof(c_0_10, plain, ![X11, X12]:((~environment(X11)|~subpopulations(first_movers,efficient_producers,X11,X12)|greater(number_of_organizations(X11,X12),zero))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_positive_number_of_organizations])])])).
% 0.25/0.55 fof(c_0_11, negated_conjecture, (((environment(esk1_0)&subpopulations(first_movers,efficient_producers,esk1_0,esk2_0))&greater_or_equal(esk2_0,equilibrium(esk1_0)))&(((growth_rate(first_movers,esk2_0)!=zero|growth_rate(efficient_producers,esk2_0)!=zero)&(~greater(growth_rate(first_movers,esk2_0),zero)|~greater(zero,growth_rate(efficient_producers,esk2_0))))&(~greater(growth_rate(efficient_producers,esk2_0),zero)|~greater(zero,growth_rate(first_movers,esk2_0))))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])).
% 0.25/0.55 fof(c_0_12, plain, ![X15, X16]:((~environment(X15)|~subpopulations(first_movers,efficient_producers,X15,X16)|in_environment(X15,X16))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_time_point_occur])])])).
% 0.25/0.55 fof(c_0_13, plain, ![X13, X14]:((~environment(X13)|~greater_or_equal(X14,equilibrium(X13))|~greater(equilibrium(X13),X14))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])).
% 0.25/0.55 fof(c_0_14, hypothesis, ![X1, X2]:(((environment(X1)&in_environment(X1,X2))=>((decreases(resources(X1,X2))=>~decreases(number_of_organizations(X1,X2)))&(constant(resources(X1,X2))=>constant(number_of_organizations(X1,X2)))))), inference(fof_simplification,[status(thm)],[a6])).
% 0.25/0.55 fof(c_0_15, hypothesis, ![X3, X4]:(((~greater(equilibrium(X3),X4)|decreases(resources(X3,X4))|(~environment(X3)|~in_environment(X3,X4)|~greater(number_of_organizations(X3,X4),zero)))&(greater(equilibrium(X3),X4)|constant(resources(X3,X4))|(~environment(X3)|~in_environment(X3,X4)|~greater(number_of_organizations(X3,X4),zero))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])])).
% 0.25/0.55 cnf(c_0_16, plain, (greater(number_of_organizations(X1,X2),zero)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.25/0.55 cnf(c_0_17, negated_conjecture, (subpopulations(first_movers,efficient_producers,esk1_0,esk2_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.25/0.55 cnf(c_0_18, negated_conjecture, (environment(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.25/0.55 cnf(c_0_19, plain, (in_environment(X1,X2)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.25/0.55 cnf(c_0_20, plain, (~environment(X1)|~greater_or_equal(X2,equilibrium(X1))|~greater(equilibrium(X1),X2)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.25/0.55 cnf(c_0_21, negated_conjecture, (greater_or_equal(esk2_0,equilibrium(esk1_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.25/0.55 fof(c_0_22, hypothesis, ![X5, X6]:(((~decreases(resources(X5,X6))|~decreases(number_of_organizations(X5,X6))|(~environment(X5)|~in_environment(X5,X6)))&(~constant(resources(X5,X6))|constant(number_of_organizations(X5,X6))|(~environment(X5)|~in_environment(X5,X6))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])])])).
% 0.25/0.55 cnf(c_0_23, hypothesis, (greater(equilibrium(X1),X2)|constant(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.25/0.55 cnf(c_0_24, negated_conjecture, (greater(number_of_organizations(esk1_0,esk2_0),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18])])).
% 0.25/0.55 cnf(c_0_25, negated_conjecture, (in_environment(esk1_0,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_17]), c_0_18])])).
% 0.25/0.55 cnf(c_0_26, negated_conjecture, (~greater(equilibrium(esk1_0),esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_18])])).
% 0.25/0.55 fof(c_0_27, hypothesis, ![X7, X8]:(((((greater(growth_rate(efficient_producers,X8),zero)|(greater(growth_rate(first_movers,X8),zero)|growth_rate(first_movers,X8)=zero)|(~environment(X7)|~subpopulations(first_movers,efficient_producers,X7,X8)|~constant(number_of_organizations(X7,X8))))&(greater(zero,growth_rate(first_movers,X8))|(greater(growth_rate(first_movers,X8),zero)|growth_rate(first_movers,X8)=zero)|(~environment(X7)|~subpopulations(first_movers,efficient_producers,X7,X8)|~constant(number_of_organizations(X7,X8)))))&((greater(growth_rate(efficient_producers,X8),zero)|(greater(zero,growth_rate(efficient_producers,X8))|growth_rate(first_movers,X8)=zero)|(~environment(X7)|~subpopulations(first_movers,efficient_producers,X7,X8)|~constant(number_of_organizations(X7,X8))))&(greater(zero,growth_rate(first_movers,X8))|(greater(zero,growth_rate(efficient_producers,X8))|growth_rate(first_movers,X8)=zero)|(~environment(X7)|~subpopulations(first_movers,efficient_producers,X7,X8)|~constant(number_of_organizations(X7,X8))))))&(((greater(growth_rate(efficient_producers,X8),zero)|(greater(growth_rate(first_movers,X8),zero)|growth_rate(efficient_producers,X8)=zero)|(~environment(X7)|~subpopulations(first_movers,efficient_producers,X7,X8)|~constant(number_of_organizations(X7,X8))))&(greater(zero,growth_rate(first_movers,X8))|(greater(growth_rate(first_movers,X8),zero)|growth_rate(efficient_producers,X8)=zero)|(~environment(X7)|~subpopulations(first_movers,efficient_producers,X7,X8)|~constant(number_of_organizations(X7,X8)))))&((greater(growth_rate(efficient_producers,X8),zero)|(greater(zero,growth_rate(efficient_producers,X8))|growth_rate(efficient_producers,X8)=zero)|(~environment(X7)|~subpopulations(first_movers,efficient_producers,X7,X8)|~constant(number_of_organizations(X7,X8))))&(greater(zero,growth_rate(first_movers,X8))|(greater(zero,growth_rate(efficient_producers,X8))|growth_rate(efficient_producers,X8)=zero)|(~environment(X7)|~subpopulations(first_movers,efficient_producers,X7,X8)|~constant(number_of_organizations(X7,X8)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[l7])])])])).
% 0.25/0.55 cnf(c_0_28, hypothesis, (constant(number_of_organizations(X1,X2))|~constant(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.25/0.55 cnf(c_0_29, hypothesis, (constant(resources(esk1_0,esk2_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_25]), c_0_18])]), c_0_26])).
% 0.25/0.55 cnf(c_0_30, hypothesis, (greater(zero,growth_rate(first_movers,X1))|greater(growth_rate(first_movers,X1),zero)|growth_rate(first_movers,X1)=zero|~environment(X2)|~subpopulations(first_movers,efficient_producers,X2,X1)|~constant(number_of_organizations(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.55 cnf(c_0_31, hypothesis, (constant(number_of_organizations(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_25]), c_0_18])])).
% 0.25/0.55 cnf(c_0_32, hypothesis, (greater(zero,growth_rate(first_movers,X1))|greater(zero,growth_rate(efficient_producers,X1))|growth_rate(first_movers,X1)=zero|~environment(X2)|~subpopulations(first_movers,efficient_producers,X2,X1)|~constant(number_of_organizations(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.55 cnf(c_0_33, hypothesis, (greater(growth_rate(efficient_producers,X1),zero)|greater(growth_rate(first_movers,X1),zero)|growth_rate(first_movers,X1)=zero|~environment(X2)|~subpopulations(first_movers,efficient_producers,X2,X1)|~constant(number_of_organizations(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.55 cnf(c_0_34, negated_conjecture, (~greater(growth_rate(first_movers,esk2_0),zero)|~greater(zero,growth_rate(efficient_producers,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.25/0.55 cnf(c_0_35, negated_conjecture, (growth_rate(first_movers,esk2_0)=zero|greater(growth_rate(first_movers,esk2_0),zero)|greater(zero,growth_rate(first_movers,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_17]), c_0_18])]), c_0_31])])).
% 0.25/0.55 cnf(c_0_36, negated_conjecture, (growth_rate(first_movers,esk2_0)=zero|greater(zero,growth_rate(efficient_producers,esk2_0))|greater(zero,growth_rate(first_movers,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_17]), c_0_18])]), c_0_31])])).
% 0.25/0.55 cnf(c_0_37, hypothesis, (greater(growth_rate(efficient_producers,X1),zero)|greater(zero,growth_rate(efficient_producers,X1))|growth_rate(first_movers,X1)=zero|~environment(X2)|~subpopulations(first_movers,efficient_producers,X2,X1)|~constant(number_of_organizations(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.55 cnf(c_0_38, hypothesis, (greater(zero,growth_rate(first_movers,X1))|greater(growth_rate(first_movers,X1),zero)|growth_rate(efficient_producers,X1)=zero|~environment(X2)|~subpopulations(first_movers,efficient_producers,X2,X1)|~constant(number_of_organizations(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.55 cnf(c_0_39, hypothesis, (greater(zero,growth_rate(first_movers,X1))|greater(zero,growth_rate(efficient_producers,X1))|growth_rate(efficient_producers,X1)=zero|~environment(X2)|~subpopulations(first_movers,efficient_producers,X2,X1)|~constant(number_of_organizations(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.55 cnf(c_0_40, negated_conjecture, (~greater(growth_rate(efficient_producers,esk2_0),zero)|~greater(zero,growth_rate(first_movers,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.25/0.55 cnf(c_0_41, negated_conjecture, (growth_rate(first_movers,esk2_0)=zero|greater(growth_rate(efficient_producers,esk2_0),zero)|greater(growth_rate(first_movers,esk2_0),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_17]), c_0_18])]), c_0_31])])).
% 0.25/0.55 cnf(c_0_42, negated_conjecture, (growth_rate(first_movers,esk2_0)=zero|greater(zero,growth_rate(first_movers,esk2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_36])).
% 0.25/0.55 cnf(c_0_43, negated_conjecture, (growth_rate(first_movers,esk2_0)=zero|greater(growth_rate(efficient_producers,esk2_0),zero)|greater(zero,growth_rate(efficient_producers,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_17]), c_0_18])]), c_0_31])])).
% 0.25/0.55 cnf(c_0_44, hypothesis, (greater(growth_rate(efficient_producers,X1),zero)|greater(zero,growth_rate(efficient_producers,X1))|growth_rate(efficient_producers,X1)=zero|~environment(X2)|~subpopulations(first_movers,efficient_producers,X2,X1)|~constant(number_of_organizations(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.55 cnf(c_0_45, negated_conjecture, (growth_rate(efficient_producers,esk2_0)=zero|greater(growth_rate(first_movers,esk2_0),zero)|greater(zero,growth_rate(first_movers,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_17]), c_0_18])]), c_0_31])])).
% 0.25/0.55 cnf(c_0_46, negated_conjecture, (growth_rate(efficient_producers,esk2_0)=zero|greater(zero,growth_rate(efficient_producers,esk2_0))|greater(zero,growth_rate(first_movers,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_17]), c_0_18])]), c_0_31])])).
% 0.25/0.55 cnf(c_0_47, negated_conjecture, (growth_rate(first_movers,esk2_0)=zero|greater(growth_rate(first_movers,esk2_0),zero)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_42])).
% 0.25/0.55 cnf(c_0_48, negated_conjecture, (growth_rate(first_movers,esk2_0)=zero|greater(zero,growth_rate(efficient_producers,esk2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_43]), c_0_42])).
% 0.25/0.55 cnf(c_0_49, negated_conjecture, (growth_rate(efficient_producers,esk2_0)=zero|greater(growth_rate(efficient_producers,esk2_0),zero)|greater(zero,growth_rate(efficient_producers,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_17]), c_0_18])]), c_0_31])])).
% 0.25/0.55 cnf(c_0_50, negated_conjecture, (growth_rate(efficient_producers,esk2_0)=zero|greater(zero,growth_rate(first_movers,esk2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_45]), c_0_46])).
% 0.25/0.55 cnf(c_0_51, negated_conjecture, (growth_rate(first_movers,esk2_0)!=zero|growth_rate(efficient_producers,esk2_0)!=zero), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.25/0.55 cnf(c_0_52, negated_conjecture, (growth_rate(first_movers,esk2_0)=zero), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_47]), c_0_48])).
% 0.25/0.55 cnf(c_0_53, negated_conjecture, (growth_rate(efficient_producers,esk2_0)=zero|greater(zero,growth_rate(efficient_producers,esk2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_49]), c_0_50])).
% 0.25/0.55 cnf(c_0_54, negated_conjecture, (growth_rate(efficient_producers,esk2_0)!=zero), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_52])])).
% 0.25/0.55 cnf(c_0_55, negated_conjecture, (greater(zero,growth_rate(efficient_producers,esk2_0))), inference(sr,[status(thm)],[c_0_53, c_0_54])).
% 0.25/0.55 cnf(c_0_56, negated_conjecture, (greater(zero,zero)), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_52]), c_0_54])).
% 0.25/0.55 cnf(c_0_57, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_52]), c_0_55]), c_0_56])]), ['proof']).
% 0.25/0.55 % SZS output end Proof
% 0.25/0.55 % User time : 0.010 s
% 0.25/0.55 % System time : 0.002 s
% 0.25/0.55 % Total time : 0.012 s
% 0.25/0.55 % User time : 0.011 s
% 0.25/0.55 % System time : 0.006 s
% 0.25/0.55 % Total time : 0.017 s
% 0.25/0.55
%------------------------------------------------------------------------------