%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT025-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n006.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 : Unsatisfiable 0.25s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT025-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.06/0.33 % Computer : n006.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.33 % WCLimit : 300
% 0.06/0.33 % DateTime : Mon Sep 7 12:11:01 UTC 2026
% 0.06/0.33 % CPUTime :
% 0.12/0.45 start to proof:theBenchmark.p
% 0.25/0.53 % Version : CSI_E---1.1
% 0.25/0.53 % Problem : theBenchmark.p
% 0.25/0.53 % Proof found!
% 0.25/0.53 # SZS status Unsatisfiable
% 0.25/0.53 % SZS output start Proof
% 0.25/0.53 cnf(mp_time_point_occur_45, axiom, (in_environment(X1,X2)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_time_point_occur_45)).
% 0.25/0.53 cnf(mp_subpopulations_30, axiom, (subpopulation(first_movers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_subpopulations_30)).
% 0.25/0.53 cnf(prove_l7_48, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk1,sk2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l7_48)).
% 0.25/0.53 cnf(prove_l7_47, negated_conjecture, (environment(sk1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l7_47)).
% 0.25/0.53 cnf(mp_non_zero_producers_43, axiom, (greater(cardinality_at_time(first_movers,X2),zero)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_non_zero_producers_43)).
% 0.25/0.53 cnf(mp_subpopulations_31, axiom, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_subpopulations_31)).
% 0.25/0.53 cnf(mp_non_zero_producers_44, axiom, (greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_non_zero_producers_44)).
% 0.25/0.53 cnf(mp_growth_rate_41, axiom, (greater(growth_rate(X3,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~increases(cardinality_at_time(X3,X2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_growth_rate_41)).
% 0.25/0.53 cnf(mp_abc_sum_increase_39, axiom, (constant(X3)|decreases(X3)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_abc_sum_increase_39)).
% 0.25/0.53 cnf(mp_only_members_29, axiom, (number_of_organizations(X1,X3)=sum(cardinality_at_time(first_movers,X3),cardinality_at_time(efficient_producers,X3))|~environment(X1)|~subpopulation(X2,X1,X3)|X2!=first_movers), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_only_members_29)).
% 0.25/0.53 cnf(prove_l7_51, negated_conjecture, (~greater(growth_rate(first_movers,sk2),zero)|~greater(zero,growth_rate(efficient_producers,sk2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l7_51)).
% 0.25/0.53 cnf(mp_growth_rate_42, axiom, (greater(zero,growth_rate(X3,X2))|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~decreases(cardinality_at_time(X3,X2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_growth_rate_42)).
% 0.25/0.53 cnf(mp_growth_rate_40, axiom, (growth_rate(X3,X2)=zero|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~constant(cardinality_at_time(X3,X2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_growth_rate_40)).
% 0.25/0.53 cnf(mp_abc_sum_increase_35, axiom, (constant(X2)|decreases(X3)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_abc_sum_increase_35)).
% 0.25/0.53 cnf(prove_l7_52, negated_conjecture, (~greater(growth_rate(efficient_producers,sk2),zero)|~greater(zero,growth_rate(first_movers,sk2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l7_52)).
% 0.25/0.53 cnf(prove_l7_50, negated_conjecture, (growth_rate(first_movers,sk2)!=zero|growth_rate(efficient_producers,sk2)!=zero), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l7_50)).
% 0.25/0.53 cnf(prove_l7_49, negated_conjecture, (constant(number_of_organizations(sk1,sk2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l7_49)).
% 0.25/0.53 cnf(mp_abc_sum_increase_37, axiom, (constant(X3)|increases(X2)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_abc_sum_increase_37)).
% 0.25/0.53 cnf(mp_abc_sum_increase_36, axiom, (constant(X3)|increases(X2)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_abc_sum_increase_36)).
% 0.25/0.53 cnf(mp_abc_sum_increase_32, axiom, (constant(X2)|increases(X2)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_abc_sum_increase_32)).
% 0.25/0.53 cnf(mp_abc_sum_increase_38, axiom, (constant(X3)|decreases(X3)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_abc_sum_increase_38)).
% 0.25/0.53 cnf(c_0_21, plain, (in_environment(X1,X2)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(fof_simplification,[status(thm)],[mp_time_point_occur_45])).
% 0.25/0.53 cnf(c_0_22, plain, (subpopulation(first_movers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_subpopulations_30])).
% 0.25/0.53 cnf(c_0_23, plain, (in_environment(X1,X2)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), c_0_21).
% 0.25/0.53 cnf(c_0_24, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk1,sk2)), prove_l7_48).
% 0.25/0.53 cnf(c_0_25, negated_conjecture, (environment(sk1)), prove_l7_47).
% 0.25/0.53 cnf(c_0_26, plain, (greater(cardinality_at_time(first_movers,X2),zero)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(fof_simplification,[status(thm)],[mp_non_zero_producers_43])).
% 0.25/0.53 cnf(c_0_27, plain, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_subpopulations_31])).
% 0.25/0.53 cnf(c_0_28, plain, (greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(fof_simplification,[status(thm)],[mp_non_zero_producers_44])).
% 0.25/0.53 cnf(c_0_29, plain, (greater(growth_rate(X3,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~increases(cardinality_at_time(X3,X2))), inference(fof_simplification,[status(thm)],[mp_growth_rate_41])).
% 0.25/0.53 cnf(c_0_30, plain, (subpopulation(first_movers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), c_0_22).
% 0.25/0.53 cnf(c_0_31, negated_conjecture, (in_environment(sk1,sk2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_25])])).
% 0.25/0.53 cnf(c_0_32, plain, (greater(cardinality_at_time(first_movers,X2),zero)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), c_0_26).
% 0.25/0.53 cnf(c_0_33, plain, (constant(X3)|decreases(X3)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), inference(fof_simplification,[status(thm)],[mp_abc_sum_increase_39])).
% 0.25/0.53 cnf(c_0_34, plain, (number_of_organizations(X1,X3)=sum(cardinality_at_time(first_movers,X3),cardinality_at_time(efficient_producers,X3))|~environment(X1)|~subpopulation(X2,X1,X3)|X2!=first_movers), inference(fof_simplification,[status(thm)],[mp_only_members_29])).
% 0.25/0.53 cnf(c_0_35, plain, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), c_0_27).
% 0.25/0.53 cnf(c_0_36, plain, (greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), c_0_28).
% 0.25/0.53 cnf(c_0_37, negated_conjecture, (~greater(growth_rate(first_movers,sk2),zero)|~greater(zero,growth_rate(efficient_producers,sk2))), inference(fof_simplification,[status(thm)],[prove_l7_51])).
% 0.25/0.53 cnf(c_0_38, plain, (greater(growth_rate(X3,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~increases(cardinality_at_time(X3,X2))), c_0_29).
% 0.25/0.53 cnf(c_0_39, negated_conjecture, (subpopulation(first_movers,sk1,sk2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_25])])).
% 0.25/0.53 cnf(c_0_40, negated_conjecture, (greater(cardinality_at_time(first_movers,sk2),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_24]), c_0_25])])).
% 0.25/0.53 cnf(c_0_41, plain, (greater(zero,growth_rate(X3,X2))|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~decreases(cardinality_at_time(X3,X2))), inference(fof_simplification,[status(thm)],[mp_growth_rate_42])).
% 0.25/0.53 cnf(c_0_42, plain, (constant(X3)|decreases(X3)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), c_0_33).
% 0.25/0.53 cnf(c_0_43, plain, (number_of_organizations(X1,X3)=sum(cardinality_at_time(first_movers,X3),cardinality_at_time(efficient_producers,X3))|~environment(X1)|~subpopulation(X2,X1,X3)|X2!=first_movers), c_0_34).
% 0.25/0.53 cnf(c_0_44, plain, (growth_rate(X3,X2)=zero|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~constant(cardinality_at_time(X3,X2))), inference(fof_simplification,[status(thm)],[mp_growth_rate_40])).
% 0.25/0.53 cnf(c_0_45, plain, (constant(X2)|decreases(X3)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), inference(fof_simplification,[status(thm)],[mp_abc_sum_increase_35])).
% 0.25/0.53 cnf(c_0_46, negated_conjecture, (~greater(growth_rate(efficient_producers,sk2),zero)|~greater(zero,growth_rate(first_movers,sk2))), inference(fof_simplification,[status(thm)],[prove_l7_52])).
% 0.25/0.53 cnf(c_0_47, negated_conjecture, (subpopulation(efficient_producers,sk1,sk2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_31]), c_0_25])])).
% 0.25/0.53 cnf(c_0_48, negated_conjecture, (greater(cardinality_at_time(efficient_producers,sk2),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_24]), c_0_25])])).
% 0.25/0.53 cnf(c_0_49, negated_conjecture, (~greater(growth_rate(first_movers,sk2),zero)|~greater(zero,growth_rate(efficient_producers,sk2))), c_0_37).
% 0.25/0.53 cnf(c_0_50, negated_conjecture, (greater(growth_rate(first_movers,sk2),zero)|~increases(cardinality_at_time(first_movers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_31]), c_0_40]), c_0_25])])).
% 0.25/0.53 cnf(c_0_51, plain, (greater(zero,growth_rate(X3,X2))|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~decreases(cardinality_at_time(X3,X2))), c_0_41).
% 0.25/0.53 cnf(c_0_52, plain, (decreases(X1)|increases(X1)|constant(X1)|~constant(sum(X2,X1))), inference(er,[status(thm)],[c_0_42])).
% 0.25/0.53 cnf(c_0_53, plain, (number_of_organizations(X1,X2)=sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2))|~subpopulation(first_movers,X1,X2)|~environment(X1)), inference(er,[status(thm)],[c_0_43])).
% 0.25/0.53 cnf(c_0_54, negated_conjecture, (growth_rate(first_movers,sk2)!=zero|growth_rate(efficient_producers,sk2)!=zero), inference(fof_simplification,[status(thm)],[prove_l7_50])).
% 0.25/0.53 cnf(c_0_55, plain, (growth_rate(X3,X2)=zero|~environment(X1)|~in_environment(X1,X2)|~subpopulation(X3,X1,X2)|~greater(cardinality_at_time(X3,X2),zero)|~constant(cardinality_at_time(X3,X2))), c_0_44).
% 0.25/0.53 cnf(c_0_56, plain, (constant(X2)|decreases(X3)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), c_0_45).
% 0.25/0.53 cnf(c_0_57, negated_conjecture, (~greater(growth_rate(efficient_producers,sk2),zero)|~greater(zero,growth_rate(first_movers,sk2))), c_0_46).
% 0.25/0.53 cnf(c_0_58, negated_conjecture, (greater(growth_rate(efficient_producers,sk2),zero)|~increases(cardinality_at_time(efficient_producers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_47]), c_0_31]), c_0_48]), c_0_25])])).
% 0.25/0.53 cnf(c_0_59, negated_conjecture, (~increases(cardinality_at_time(first_movers,sk2))|~greater(zero,growth_rate(efficient_producers,sk2))), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 0.25/0.53 cnf(c_0_60, negated_conjecture, (greater(zero,growth_rate(efficient_producers,sk2))|~decreases(cardinality_at_time(efficient_producers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_47]), c_0_31]), c_0_48]), c_0_25])])).
% 0.25/0.53 cnf(c_0_61, plain, (decreases(cardinality_at_time(efficient_producers,X1))|increases(cardinality_at_time(efficient_producers,X1))|constant(cardinality_at_time(efficient_producers,X1))|~constant(number_of_organizations(X2,X1))|~subpopulation(first_movers,X2,X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_52, c_0_53])).
% 0.25/0.53 cnf(c_0_62, negated_conjecture, (constant(number_of_organizations(sk1,sk2))), prove_l7_49).
% 0.25/0.53 cnf(c_0_63, negated_conjecture, (growth_rate(first_movers,sk2)!=zero|growth_rate(efficient_producers,sk2)!=zero), c_0_54).
% 0.25/0.53 cnf(c_0_64, negated_conjecture, (growth_rate(efficient_producers,sk2)=zero|~constant(cardinality_at_time(efficient_producers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_47]), c_0_31]), c_0_48]), c_0_25])])).
% 0.25/0.53 cnf(c_0_65, plain, (number_of_organizations(X1,X2)=number_of_organizations(X3,X2)|~subpopulation(first_movers,X1,X2)|~subpopulation(first_movers,X3,X2)|~environment(X1)|~environment(X3)), inference(spm,[status(thm)],[c_0_53, c_0_53])).
% 0.25/0.53 cnf(c_0_66, plain, (constant(X3)|increases(X2)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), inference(fof_simplification,[status(thm)],[mp_abc_sum_increase_37])).
% 0.25/0.53 cnf(c_0_67, plain, (decreases(X1)|increases(X1)|constant(X2)|~constant(sum(X2,X1))), inference(er,[status(thm)],[c_0_56])).
% 0.25/0.53 cnf(c_0_68, negated_conjecture, (~increases(cardinality_at_time(efficient_producers,sk2))|~greater(zero,growth_rate(first_movers,sk2))), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 0.25/0.53 cnf(c_0_69, negated_conjecture, (growth_rate(first_movers,sk2)=zero|~constant(cardinality_at_time(first_movers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_39]), c_0_31]), c_0_40]), c_0_25])])).
% 0.25/0.53 cnf(c_0_70, negated_conjecture, (~decreases(cardinality_at_time(efficient_producers,sk2))|~increases(cardinality_at_time(first_movers,sk2))), inference(spm,[status(thm)],[c_0_59, c_0_60])).
% 0.25/0.53 cnf(c_0_71, negated_conjecture, (decreases(cardinality_at_time(efficient_producers,sk2))|increases(cardinality_at_time(efficient_producers,sk2))|constant(cardinality_at_time(efficient_producers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_39]), c_0_25])])).
% 0.25/0.53 cnf(c_0_72, negated_conjecture, (growth_rate(first_movers,sk2)!=zero|~constant(cardinality_at_time(efficient_producers,sk2))), inference(spm,[status(thm)],[c_0_63, c_0_64])).
% 0.25/0.53 cnf(c_0_73, plain, (constant(X3)|increases(X2)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), inference(fof_simplification,[status(thm)],[mp_abc_sum_increase_36])).
% 0.25/0.53 cnf(c_0_74, negated_conjecture, (constant(number_of_organizations(X1,sk2))|~subpopulation(first_movers,X1,sk2)|~environment(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_65]), c_0_39]), c_0_25])])).
% 0.25/0.53 cnf(c_0_75, plain, (constant(X3)|increases(X2)|increases(X3)|X1!=sum(X2,X3)|~constant(X1)), c_0_66).
% 0.25/0.53 cnf(c_0_76, plain, (decreases(cardinality_at_time(efficient_producers,X1))|increases(cardinality_at_time(efficient_producers,X1))|constant(cardinality_at_time(first_movers,X1))|~constant(number_of_organizations(X2,X1))|~subpopulation(first_movers,X2,X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_67, c_0_53])).
% 0.25/0.53 cnf(c_0_77, negated_conjecture, (~increases(cardinality_at_time(efficient_producers,sk2))|~constant(cardinality_at_time(first_movers,sk2))|~greater(zero,zero)), inference(spm,[status(thm)],[c_0_68, c_0_69])).
% 0.25/0.53 cnf(c_0_78, negated_conjecture, (increases(cardinality_at_time(efficient_producers,sk2))|constant(cardinality_at_time(efficient_producers,sk2))|~increases(cardinality_at_time(first_movers,sk2))), inference(spm,[status(thm)],[c_0_70, c_0_71])).
% 0.25/0.53 cnf(c_0_79, negated_conjecture, (greater(zero,zero)|~increases(cardinality_at_time(first_movers,sk2))|~constant(cardinality_at_time(first_movers,sk2))), inference(spm,[status(thm)],[c_0_50, c_0_69])).
% 0.25/0.53 cnf(c_0_80, negated_conjecture, (~constant(cardinality_at_time(efficient_producers,sk2))|~constant(cardinality_at_time(first_movers,sk2))), inference(spm,[status(thm)],[c_0_72, c_0_69])).
% 0.25/0.53 cnf(c_0_81, plain, (constant(X3)|increases(X2)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), c_0_73).
% 0.25/0.53 cnf(c_0_82, negated_conjecture, (constant(sum(cardinality_at_time(first_movers,sk2),cardinality_at_time(efficient_producers,sk2)))|~subpopulation(first_movers,X1,sk2)|~environment(X1)), inference(spm,[status(thm)],[c_0_74, c_0_53])).
% 0.25/0.53 cnf(c_0_83, plain, (increases(X1)|increases(X2)|constant(X1)|~constant(sum(X2,X1))), inference(er,[status(thm)],[c_0_75])).
% 0.25/0.53 cnf(c_0_84, negated_conjecture, (decreases(cardinality_at_time(efficient_producers,sk2))|increases(cardinality_at_time(efficient_producers,sk2))|constant(cardinality_at_time(first_movers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_62]), c_0_39]), c_0_25])])).
% 0.25/0.53 cnf(c_0_85, negated_conjecture, (~increases(cardinality_at_time(first_movers,sk2))|~constant(cardinality_at_time(first_movers,sk2))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_78]), c_0_79]), c_0_80])).
% 0.25/0.53 cnf(c_0_86, negated_conjecture, (greater(zero,growth_rate(first_movers,sk2))|~decreases(cardinality_at_time(first_movers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_39]), c_0_31]), c_0_40]), c_0_25])])).
% 0.25/0.53 cnf(c_0_87, plain, (decreases(X1)|increases(X1)|constant(X2)|~constant(sum(X1,X2))), inference(er,[status(thm)],[c_0_81])).
% 0.25/0.53 cnf(c_0_88, negated_conjecture, (constant(sum(cardinality_at_time(first_movers,sk2),cardinality_at_time(efficient_producers,sk2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_39]), c_0_25])])).
% 0.25/0.53 cnf(c_0_89, plain, (increases(cardinality_at_time(efficient_producers,X1))|increases(cardinality_at_time(first_movers,X1))|constant(cardinality_at_time(efficient_producers,X1))|~constant(number_of_organizations(X2,X1))|~subpopulation(first_movers,X2,X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_83, c_0_53])).
% 0.25/0.53 cnf(c_0_90, negated_conjecture, (increases(cardinality_at_time(efficient_producers,sk2))|~increases(cardinality_at_time(first_movers,sk2))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_84]), c_0_85])).
% 0.25/0.53 cnf(c_0_91, plain, (constant(X2)|increases(X2)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), inference(fof_simplification,[status(thm)],[mp_abc_sum_increase_32])).
% 0.25/0.53 cnf(c_0_92, negated_conjecture, (~decreases(cardinality_at_time(first_movers,sk2))|~increases(cardinality_at_time(efficient_producers,sk2))), inference(spm,[status(thm)],[c_0_68, c_0_86])).
% 0.25/0.53 cnf(c_0_93, negated_conjecture, (decreases(cardinality_at_time(first_movers,sk2))|increases(cardinality_at_time(first_movers,sk2))|constant(cardinality_at_time(efficient_producers,sk2))), inference(spm,[status(thm)],[c_0_87, c_0_88])).
% 0.25/0.53 cnf(c_0_94, negated_conjecture, (increases(cardinality_at_time(efficient_producers,sk2))|constant(cardinality_at_time(efficient_producers,sk2))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_62]), c_0_39]), c_0_25])]), c_0_90])).
% 0.25/0.53 cnf(c_0_95, plain, (constant(X2)|increases(X2)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), c_0_91).
% 0.25/0.53 cnf(c_0_96, negated_conjecture, (increases(cardinality_at_time(first_movers,sk2))|constant(cardinality_at_time(efficient_producers,sk2))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_93]), c_0_94])).
% 0.25/0.53 cnf(c_0_97, negated_conjecture, (~constant(cardinality_at_time(efficient_producers,sk2))|~greater(zero,growth_rate(first_movers,sk2))|~greater(zero,zero)), inference(spm,[status(thm)],[c_0_57, c_0_64])).
% 0.25/0.53 cnf(c_0_98, plain, (decreases(X1)|increases(X1)|constant(X1)|~constant(sum(X1,X2))), inference(er,[status(thm)],[c_0_95])).
% 0.25/0.53 cnf(c_0_99, negated_conjecture, (~constant(cardinality_at_time(first_movers,sk2))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_96]), c_0_80])).
% 0.25/0.53 cnf(c_0_100, negated_conjecture, (greater(zero,zero)|~decreases(cardinality_at_time(efficient_producers,sk2))|~constant(cardinality_at_time(efficient_producers,sk2))), inference(spm,[status(thm)],[c_0_60, c_0_64])).
% 0.25/0.53 cnf(c_0_101, negated_conjecture, (greater(zero,zero)|~increases(cardinality_at_time(efficient_producers,sk2))|~constant(cardinality_at_time(efficient_producers,sk2))), inference(spm,[status(thm)],[c_0_58, c_0_64])).
% 0.25/0.53 cnf(c_0_102, negated_conjecture, (~decreases(cardinality_at_time(first_movers,sk2))|~constant(cardinality_at_time(efficient_producers,sk2))|~greater(zero,zero)), inference(spm,[status(thm)],[c_0_97, c_0_86])).
% 0.25/0.53 cnf(c_0_103, negated_conjecture, (decreases(cardinality_at_time(first_movers,sk2))|increases(cardinality_at_time(first_movers,sk2))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_88]), c_0_99])).
% 0.25/0.53 cnf(c_0_104, negated_conjecture, (greater(zero,zero)|~constant(cardinality_at_time(efficient_producers,sk2))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_84]), c_0_80]), c_0_101])).
% 0.25/0.53 cnf(c_0_105, plain, (constant(X3)|decreases(X3)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), inference(fof_simplification,[status(thm)],[mp_abc_sum_increase_38])).
% 0.25/0.53 cnf(c_0_106, negated_conjecture, (increases(cardinality_at_time(first_movers,sk2))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_103]), c_0_104]), c_0_96])).
% 0.25/0.53 cnf(c_0_107, plain, (constant(X3)|decreases(X3)|decreases(X2)|X1!=sum(X2,X3)|~constant(X1)), c_0_105).
% 0.25/0.53 cnf(c_0_108, negated_conjecture, (increases(cardinality_at_time(efficient_producers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_90, c_0_106])])).
% 0.25/0.53 cnf(c_0_109, negated_conjecture, (~increases(cardinality_at_time(first_movers,sk2))|~constant(cardinality_at_time(efficient_producers,sk2))|~greater(zero,zero)), inference(spm,[status(thm)],[c_0_59, c_0_64])).
% 0.25/0.53 cnf(c_0_110, plain, (decreases(X1)|decreases(X2)|constant(X1)|~constant(sum(X2,X1))), inference(er,[status(thm)],[c_0_107])).
% 0.25/0.53 cnf(c_0_111, negated_conjecture, (~decreases(cardinality_at_time(first_movers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_92, c_0_108])])).
% 0.25/0.53 cnf(c_0_112, negated_conjecture, (~decreases(cardinality_at_time(efficient_producers,sk2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_70, c_0_106])])).
% 0.25/0.53 cnf(c_0_113, negated_conjecture, (~constant(cardinality_at_time(efficient_producers,sk2))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_109, c_0_106])]), c_0_104])).
% 0.25/0.53 cnf(c_0_114, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_110, c_0_88]), c_0_111]), c_0_112]), c_0_113]), ['proof']).
% 0.25/0.53 % SZS output end Proof
% 0.25/0.53 % User time : 0.007 s
% 0.25/0.53 % System time : 0.004 s
% 0.25/0.53 % Total time : 0.011 s
% 0.25/0.53 % User time : 0.034 s
% 0.25/0.53 % System time : 0.009 s
% 0.25/0.53 % Total time : 0.044 s
% 0.25/0.53
%------------------------------------------------------------------------------