%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT037-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:04:32 AM UTC 2026
% Result : Unsatisfiable 0.70s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT037-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.05 % Command : java -jar mcs_scs.jar %d %s
% 0.17/0.42 % Computer : n008.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 7 12:44:23 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.27/0.59 start to proof:theBenchmark.p
% 0.70/0.70 % Version : CSI_E---1.1
% 0.70/0.70 % Problem : theBenchmark.p
% 0.70/0.70 % Proof found!
% 0.70/0.70 # SZS status Unsatisfiable
% 0.70/0.70 % SZS output start Proof
% 0.70/0.70 cnf(mp_efficient_producers_exist_40, axiom, (cardinality_at_time(efficient_producers,X2)=zero|greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_efficient_producers_exist_40)).
% 0.70/0.70 cnf(prove_t6_54, negated_conjecture, (~greater(cardinality_at_time(efficient_producers,sk4),zero)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t6_54)).
% 0.70/0.70 cnf(mp_previous_negative_growth_29, axiom, (in_environment(X1,sk1(X2,X1))|~environment(X1)|~greater_or_equal(X2,appear(efficient_producers,X1))|cardinality_at_time(efficient_producers,X2)!=zero), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_previous_negative_growth_29)).
% 0.70/0.70 cnf(prove_t6_52, negated_conjecture, (in_environment(sk3,sk4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t6_52)).
% 0.70/0.70 cnf(prove_t6_51, negated_conjecture, (environment(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t6_51)).
% 0.70/0.70 cnf(mp_previous_negative_growth_31, axiom, (greater(zero,growth_rate(efficient_producers,sk1(X2,X1)))|~environment(X1)|~greater_or_equal(X2,appear(efficient_producers,X1))|cardinality_at_time(efficient_producers,X2)!=zero), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_previous_negative_growth_31)).
% 0.70/0.70 cnf(a9_50, hypothesis, (X2=efficient_producers|X2=first_movers|~environment(X1)|~subpopulation(X2,X1,X3)|~greater(cardinality_at_time(X2,X3),zero)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a9_50)).
% 0.70/0.70 cnf(mp_non_decreasing_34, axiom, (decreases(number_of_organizations(X1,X2))|greater(cardinality_at_time(sk2(X2,X1),X2),zero)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_non_decreasing_34)).
% 0.70/0.70 cnf(mp_non_decreasing_33, axiom, (decreases(number_of_organizations(X1,X2))|subpopulation(sk2(X2,X1),X1,X2)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_non_decreasing_33)).
% 0.70/0.71 cnf(prove_t6_53, negated_conjecture, (greater_or_equal(sk4,appear(efficient_producers,sk3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t6_53)).
% 0.70/0.71 cnf(a12_48, hypothesis, (greater(zero,growth_rate(X3,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(resilience(X4),resilience(X3))|~greater(zero,growth_rate(X4,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a12_48)).
% 0.70/0.71 cnf(mp_non_decreasing_35, axiom, (decreases(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(sk2(X2,X1),X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_non_decreasing_35)).
% 0.70/0.71 cnf(a6_46, hypothesis, (~environment(X1)|~in_environment(X1,X2)|~decreases(resources(X1,X2))|~decreases(number_of_organizations(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a6_46)).
% 0.70/0.71 cnf(a2_49, hypothesis, (greater(resilience(efficient_producers),resilience(first_movers))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a2_49)).
% 0.70/0.71 cnf(a1_45, hypothesis, (greater(number_of_organizations(X1,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(an_organisation,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a1_45)).
% 0.70/0.71 cnf(mp_environment_inequality_42, axiom, (greater_or_equal(X2,appear(an_organisation,X1))|greater(appear(an_organisation,X1),X2)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_environment_inequality_42)).
% 0.70/0.71 cnf(mp_subpopulations_38, axiom, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_subpopulations_38)).
% 0.70/0.71 cnf(a3_43, hypothesis, (decreases(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)|~greater(equilibrium(X1),X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a3_43)).
% 0.70/0.71 cnf(mp_no_members_36, axiom, (cardinality_at_time(X3,X2)=zero|~environment(X1)|~in_environment(X1,X2)|number_of_organizations(X1,X2)!=zero|~subpopulation(X3,X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_no_members_36)).
% 0.70/0.71 cnf(mp_empty_not_decreasing_39, axiom, (cardinality_at_time(X1,X2)!=zero|~greater(zero,growth_rate(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_empty_not_decreasing_39)).
% 0.70/0.71 cnf(a3_44, hypothesis, (greater(equilibrium(X1),X2)|constant(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a3_44)).
% 0.70/0.71 cnf(mp_start_of_organizations_32, axiom, (number_of_organizations(X1,X2)=zero|~environment(X1)|~in_environment(X1,X2)|~greater(appear(an_organisation,X1),X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_start_of_organizations_32)).
% 0.70/0.71 cnf(a6_47, hypothesis, (constant(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~constant(resources(X1,X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a6_47)).
% 0.70/0.71 cnf(mp_constant_not_decrease_41, axiom, (~constant(X1)|~decreases(X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_constant_not_decrease_41)).
% 0.70/0.71 cnf(c_0_24, plain, (cardinality_at_time(efficient_producers,X2)=zero|greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_efficient_producers_exist_40])).
% 0.70/0.71 cnf(c_0_25, negated_conjecture, (~greater(cardinality_at_time(efficient_producers,sk4),zero)), inference(fof_simplification,[status(thm)],[prove_t6_54])).
% 0.70/0.71 cnf(c_0_26, plain, (in_environment(X1,sk1(X2,X1))|~environment(X1)|~greater_or_equal(X2,appear(efficient_producers,X1))|cardinality_at_time(efficient_producers,X2)!=zero), inference(fof_simplification,[status(thm)],[mp_previous_negative_growth_29])).
% 0.70/0.71 cnf(c_0_27, plain, (cardinality_at_time(efficient_producers,X2)=zero|greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)), c_0_24).
% 0.70/0.71 cnf(c_0_28, negated_conjecture, (in_environment(sk3,sk4)), prove_t6_52).
% 0.70/0.71 cnf(c_0_29, negated_conjecture, (environment(sk3)), prove_t6_51).
% 0.70/0.71 cnf(c_0_30, negated_conjecture, (~greater(cardinality_at_time(efficient_producers,sk4),zero)), c_0_25).
% 0.70/0.71 cnf(c_0_31, plain, (greater(zero,growth_rate(efficient_producers,sk1(X2,X1)))|~environment(X1)|~greater_or_equal(X2,appear(efficient_producers,X1))|cardinality_at_time(efficient_producers,X2)!=zero), inference(fof_simplification,[status(thm)],[mp_previous_negative_growth_31])).
% 0.70/0.71 cnf(c_0_32, hypothesis, (X2=efficient_producers|X2=first_movers|~environment(X1)|~subpopulation(X2,X1,X3)|~greater(cardinality_at_time(X2,X3),zero)), inference(fof_simplification,[status(thm)],[a9_50])).
% 0.70/0.71 cnf(c_0_33, plain, (decreases(number_of_organizations(X1,X2))|greater(cardinality_at_time(sk2(X2,X1),X2),zero)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_non_decreasing_34])).
% 0.70/0.71 cnf(c_0_34, plain, (decreases(number_of_organizations(X1,X2))|subpopulation(sk2(X2,X1),X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_non_decreasing_33])).
% 0.70/0.71 cnf(c_0_35, plain, (in_environment(X1,sk1(X2,X1))|~environment(X1)|~greater_or_equal(X2,appear(efficient_producers,X1))|cardinality_at_time(efficient_producers,X2)!=zero), c_0_26).
% 0.70/0.71 cnf(c_0_36, negated_conjecture, (greater_or_equal(sk4,appear(efficient_producers,sk3))), prove_t6_53).
% 0.70/0.71 cnf(c_0_37, negated_conjecture, (cardinality_at_time(efficient_producers,sk4)=zero), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_28]), c_0_29])]), c_0_30])).
% 0.70/0.71 cnf(c_0_38, hypothesis, (greater(zero,growth_rate(X3,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(resilience(X4),resilience(X3))|~greater(zero,growth_rate(X4,X2))), inference(fof_simplification,[status(thm)],[a12_48])).
% 0.70/0.71 cnf(c_0_39, plain, (greater(zero,growth_rate(efficient_producers,sk1(X2,X1)))|~environment(X1)|~greater_or_equal(X2,appear(efficient_producers,X1))|cardinality_at_time(efficient_producers,X2)!=zero), c_0_31).
% 0.70/0.71 cnf(c_0_40, plain, (decreases(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(sk2(X2,X1),X2))), inference(fof_simplification,[status(thm)],[mp_non_decreasing_35])).
% 0.70/0.71 cnf(c_0_41, hypothesis, (X2=efficient_producers|X2=first_movers|~environment(X1)|~subpopulation(X2,X1,X3)|~greater(cardinality_at_time(X2,X3),zero)), c_0_32).
% 0.70/0.71 cnf(c_0_42, plain, (decreases(number_of_organizations(X1,X2))|greater(cardinality_at_time(sk2(X2,X1),X2),zero)|~environment(X1)|~in_environment(X1,X2)), c_0_33).
% 0.70/0.71 cnf(c_0_43, plain, (decreases(number_of_organizations(X1,X2))|subpopulation(sk2(X2,X1),X1,X2)|~environment(X1)|~in_environment(X1,X2)), c_0_34).
% 0.70/0.71 cnf(c_0_44, negated_conjecture, (in_environment(sk3,sk1(sk4,sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_29])]), c_0_37])])).
% 0.70/0.71 cnf(c_0_45, hypothesis, (greater(zero,growth_rate(X3,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(resilience(X4),resilience(X3))|~greater(zero,growth_rate(X4,X2))), c_0_38).
% 0.70/0.71 cnf(c_0_46, negated_conjecture, (greater(zero,growth_rate(efficient_producers,sk1(sk4,sk3)))), 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_36]), c_0_29])]), c_0_37])])).
% 0.70/0.71 cnf(c_0_47, plain, (decreases(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(sk2(X2,X1),X2))), c_0_40).
% 0.70/0.71 cnf(c_0_48, hypothesis, (sk2(X1,X2)=first_movers|sk2(X1,X2)=efficient_producers|decreases(number_of_organizations(X2,X1))|~subpopulation(sk2(X1,X2),X3,X1)|~in_environment(X2,X1)|~environment(X3)|~environment(X2)), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 0.70/0.71 cnf(c_0_49, negated_conjecture, (subpopulation(sk2(sk1(sk4,sk3),sk3),sk3,sk1(sk4,sk3))|decreases(number_of_organizations(sk3,sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_50, hypothesis, (greater(zero,growth_rate(X1,sk1(sk4,sk3)))|~in_environment(X2,sk1(sk4,sk3))|~greater(resilience(efficient_producers),resilience(X1))|~environment(X2)), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 0.70/0.71 cnf(c_0_51, hypothesis, (~environment(X1)|~in_environment(X1,X2)|~decreases(resources(X1,X2))|~decreases(number_of_organizations(X1,X2))), inference(fof_simplification,[status(thm)],[a6_46])).
% 0.70/0.71 cnf(c_0_52, negated_conjecture, (decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|~greater(zero,growth_rate(sk2(sk1(sk4,sk3),sk3),sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_53, hypothesis, (sk2(sk1(sk4,sk3),sk3)=efficient_producers|sk2(sk1(sk4,sk3),sk3)=first_movers|decreases(number_of_organizations(sk3,sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_49]), c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_54, negated_conjecture, (greater(zero,growth_rate(X1,sk1(sk4,sk3)))|~greater(resilience(efficient_producers),resilience(X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_55, hypothesis, (greater(resilience(efficient_producers),resilience(first_movers))), a2_49).
% 0.70/0.71 cnf(c_0_56, hypothesis, (~environment(X1)|~in_environment(X1,X2)|~decreases(resources(X1,X2))|~decreases(number_of_organizations(X1,X2))), c_0_51).
% 0.70/0.71 cnf(c_0_57, negated_conjecture, (sk2(sk1(sk4,sk3),sk3)=first_movers|decreases(number_of_organizations(sk3,sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_53]), c_0_46])])).
% 0.70/0.71 cnf(c_0_58, hypothesis, (greater(zero,growth_rate(first_movers,sk1(sk4,sk3)))), inference(spm,[status(thm)],[c_0_54, c_0_55])).
% 0.70/0.71 cnf(c_0_59, hypothesis, (greater(number_of_organizations(X1,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(an_organisation,X1))), inference(fof_simplification,[status(thm)],[a1_45])).
% 0.70/0.71 cnf(c_0_60, plain, (greater_or_equal(X2,appear(an_organisation,X1))|greater(appear(an_organisation,X1),X2)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_environment_inequality_42])).
% 0.70/0.71 cnf(c_0_61, plain, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_subpopulations_38])).
% 0.70/0.71 cnf(c_0_62, hypothesis, (decreases(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)|~greater(equilibrium(X1),X2)), inference(fof_simplification,[status(thm)],[a3_43])).
% 0.70/0.71 cnf(c_0_63, hypothesis, (~decreases(number_of_organizations(sk3,sk1(sk4,sk3)))|~decreases(resources(sk3,sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_64, negated_conjecture, (decreases(number_of_organizations(sk3,sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_57]), c_0_58])])).
% 0.70/0.71 cnf(c_0_65, hypothesis, (greater(number_of_organizations(X1,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(an_organisation,X1))), c_0_59).
% 0.70/0.71 cnf(c_0_66, plain, (greater_or_equal(X2,appear(an_organisation,X1))|greater(appear(an_organisation,X1),X2)|~environment(X1)|~in_environment(X1,X2)), c_0_60).
% 0.70/0.71 cnf(c_0_67, plain, (cardinality_at_time(X3,X2)=zero|~environment(X1)|~in_environment(X1,X2)|number_of_organizations(X1,X2)!=zero|~subpopulation(X3,X1,X2)), inference(fof_simplification,[status(thm)],[mp_no_members_36])).
% 0.70/0.71 cnf(c_0_68, plain, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), c_0_61).
% 0.70/0.71 cnf(c_0_69, hypothesis, (decreases(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)|~greater(equilibrium(X1),X2)), c_0_62).
% 0.70/0.71 cnf(c_0_70, hypothesis, (~decreases(resources(sk3,sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 0.70/0.71 cnf(c_0_71, hypothesis, (greater(appear(an_organisation,X1),X2)|greater(number_of_organizations(X1,X2),zero)|~in_environment(X1,X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 0.70/0.71 cnf(c_0_72, plain, (cardinality_at_time(X1,X2)!=zero|~greater(zero,growth_rate(X1,X2))), inference(fof_simplification,[status(thm)],[mp_empty_not_decreasing_39])).
% 0.70/0.71 cnf(c_0_73, plain, (cardinality_at_time(X3,X2)=zero|~environment(X1)|~in_environment(X1,X2)|number_of_organizations(X1,X2)!=zero|~subpopulation(X3,X1,X2)), c_0_67).
% 0.70/0.71 cnf(c_0_74, negated_conjecture, (subpopulation(efficient_producers,sk3,sk1(sk4,sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_75, hypothesis, (greater(equilibrium(X1),X2)|constant(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)), inference(fof_simplification,[status(thm)],[a3_44])).
% 0.70/0.71 cnf(c_0_76, plain, (number_of_organizations(X1,X2)=zero|~environment(X1)|~in_environment(X1,X2)|~greater(appear(an_organisation,X1),X2)), inference(fof_simplification,[status(thm)],[mp_start_of_organizations_32])).
% 0.70/0.71 cnf(c_0_77, hypothesis, (~greater(number_of_organizations(sk3,sk1(sk4,sk3)),zero)|~greater(equilibrium(sk3),sk1(sk4,sk3))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_44]), c_0_29])]), c_0_70])).
% 0.70/0.71 cnf(c_0_78, negated_conjecture, (greater(number_of_organizations(sk3,sk1(sk4,sk3)),zero)|greater(appear(an_organisation,sk3),sk1(sk4,sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_79, plain, (cardinality_at_time(X1,X2)!=zero|~greater(zero,growth_rate(X1,X2))), c_0_72).
% 0.70/0.71 cnf(c_0_80, negated_conjecture, (cardinality_at_time(efficient_producers,sk1(sk4,sk3))=zero|number_of_organizations(sk3,sk1(sk4,sk3))!=zero), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_74]), c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_81, hypothesis, (greater(equilibrium(X1),X2)|constant(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)), c_0_75).
% 0.70/0.71 cnf(c_0_82, plain, (number_of_organizations(X1,X2)=zero|~environment(X1)|~in_environment(X1,X2)|~greater(appear(an_organisation,X1),X2)), c_0_76).
% 0.70/0.71 cnf(c_0_83, negated_conjecture, (greater(appear(an_organisation,sk3),sk1(sk4,sk3))|~greater(equilibrium(sk3),sk1(sk4,sk3))), inference(spm,[status(thm)],[c_0_77, c_0_78])).
% 0.70/0.71 cnf(c_0_84, negated_conjecture, (number_of_organizations(sk3,sk1(sk4,sk3))!=zero), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_80]), c_0_46])])).
% 0.70/0.71 cnf(c_0_85, hypothesis, (constant(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~constant(resources(X1,X2))), inference(fof_simplification,[status(thm)],[a6_47])).
% 0.70/0.71 cnf(c_0_86, hypothesis, (constant(resources(sk3,sk1(sk4,sk3)))|greater(equilibrium(sk3),sk1(sk4,sk3))|~greater(number_of_organizations(sk3,sk1(sk4,sk3)),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_87, negated_conjecture, (~greater(equilibrium(sk3),sk1(sk4,sk3))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_83]), c_0_44]), c_0_29])]), c_0_84])).
% 0.70/0.71 cnf(c_0_88, hypothesis, (constant(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~constant(resources(X1,X2))), c_0_85).
% 0.70/0.71 cnf(c_0_89, negated_conjecture, (constant(resources(sk3,sk1(sk4,sk3)))|greater(appear(an_organisation,sk3),sk1(sk4,sk3))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_78]), c_0_87])).
% 0.70/0.71 cnf(c_0_90, plain, (~constant(X1)|~decreases(X1)), inference(fof_simplification,[status(thm)],[mp_constant_not_decrease_41])).
% 0.70/0.71 cnf(c_0_91, hypothesis, (constant(number_of_organizations(sk3,sk1(sk4,sk3)))|~constant(resources(sk3,sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_44]), c_0_29])])).
% 0.70/0.71 cnf(c_0_92, negated_conjecture, (constant(resources(sk3,sk1(sk4,sk3)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_89]), c_0_44]), c_0_29])]), c_0_84])).
% 0.70/0.71 cnf(c_0_93, plain, (~constant(X1)|~decreases(X1)), c_0_90).
% 0.70/0.71 cnf(c_0_94, hypothesis, (constant(number_of_organizations(sk3,sk1(sk4,sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_91, c_0_92])])).
% 0.70/0.71 cnf(c_0_95, hypothesis, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_94]), c_0_64])]), ['proof']).
% 0.70/0.71 % SZS output end Proof
% 0.70/0.71 % User time : 0.010 s
% 0.70/0.71 % System time : 0.003 s
% 0.70/0.71 % Total time : 0.013 s
% 0.70/0.71 % User time : 0.012 s
% 0.70/0.71 % System time : 0.008 s
% 0.70/0.71 % Total time : 0.020 s
% 0.70/0.71
%------------------------------------------------------------------------------