%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT020-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:04:29 AM UTC 2026
% Result : Unsatisfiable 0.24s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT020-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.33 % Computer : n026.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Mon Sep 7 12:04:27 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.12/0.45 start to proof:theBenchmark.p
% 0.24/0.53 % Version : CSI_E---1.1
% 0.24/0.53 % Problem : theBenchmark.p
% 0.24/0.53 % Proof found!
% 0.24/0.53 # SZS status Unsatisfiable
% 0.24/0.53 % SZS output start Proof
% 0.24/0.53 cnf(mp_times_in_order_28, axiom, (in_environment(X1,X2)|~environment(X1)|~greater_or_equal(X2,start_time(X1))|~greater(X3,X2)|~in_environment(X1,X3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_times_in_order_28)).
% 0.24/0.53 cnf(mp_initial_time_27, axiom, (greater_or_equal(initial_FM_EP(X1),start_time(X1))|~environment(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_initial_time_27)).
% 0.24/0.53 cnf(mp_greater_or_equal_30, axiom, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_greater_or_equal_30)).
% 0.24/0.53 cnf(mp_earliest_time_point_24, axiom, (greater_or_equal(X2,initial_FM_EP(X1))|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_earliest_time_point_24)).
% 0.24/0.53 cnf(mp_positive_function_difference_25, axiom, (decreases(difference(disbanding_rate(first_movers,X2),disbanding_rate(efficient_producers,X2)))|greater(disbanding_rate(first_movers,X4),disbanding_rate(efficient_producers,X4))|~environment(X1)|~greater_or_equal(X2,X3)|~greater_or_equal(X4,X2)|~subpopulations(first_movers,efficient_producers,X1,X4)|~greater(disbanding_rate(first_movers,X3),disbanding_rate(efficient_producers,X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_positive_function_difference_25)).
% 0.24/0.53 cnf(a8_31, hypothesis, (greater(disbanding_rate(first_movers,initial_FM_EP(X1)),disbanding_rate(efficient_producers,initial_FM_EP(X1)))|~environment(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', a8_31)).
% 0.24/0.53 cnf(mp_time_point_occurs_26, axiom, (in_environment(X1,X2)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_time_point_occurs_26)).
% 0.24/0.53 cnf(prove_l2_35, negated_conjecture, (~greater(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l2_35)).
% 0.24/0.53 cnf(prove_l2_34, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk1,sk2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l2_34)).
% 0.24/0.53 cnf(prove_l2_33, negated_conjecture, (environment(sk1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l2_33)).
% 0.24/0.53 cnf(l3_22, axiom, (~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~decreases(difference(disbanding_rate(first_movers,X2),disbanding_rate(efficient_producers,X2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l3_22)).
% 0.24/0.53 cnf(mp_earliest_time_point_23, axiom, (subpopulations(first_movers,efficient_producers,X1,initial_FM_EP(X1))|~environment(X1)|~in_environment(X1,initial_FM_EP(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_earliest_time_point_23)).
% 0.24/0.53 cnf(c_0_12, plain, (in_environment(X1,X2)|~environment(X1)|~greater_or_equal(X2,start_time(X1))|~greater(X3,X2)|~in_environment(X1,X3)), inference(fof_simplification,[status(thm)],[mp_times_in_order_28])).
% 0.24/0.53 cnf(c_0_13, plain, (greater_or_equal(initial_FM_EP(X1),start_time(X1))|~environment(X1)), inference(fof_simplification,[status(thm)],[mp_initial_time_27])).
% 0.24/0.53 cnf(c_0_14, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(fof_simplification,[status(thm)],[mp_greater_or_equal_30])).
% 0.24/0.53 cnf(c_0_15, plain, (greater_or_equal(X2,initial_FM_EP(X1))|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(fof_simplification,[status(thm)],[mp_earliest_time_point_24])).
% 0.24/0.53 cnf(c_0_16, plain, (decreases(difference(disbanding_rate(first_movers,X2),disbanding_rate(efficient_producers,X2)))|greater(disbanding_rate(first_movers,X4),disbanding_rate(efficient_producers,X4))|~environment(X1)|~greater_or_equal(X2,X3)|~greater_or_equal(X4,X2)|~subpopulations(first_movers,efficient_producers,X1,X4)|~greater(disbanding_rate(first_movers,X3),disbanding_rate(efficient_producers,X3))), inference(fof_simplification,[status(thm)],[mp_positive_function_difference_25])).
% 0.24/0.53 cnf(c_0_17, hypothesis, (greater(disbanding_rate(first_movers,initial_FM_EP(X1)),disbanding_rate(efficient_producers,initial_FM_EP(X1)))|~environment(X1)), inference(fof_simplification,[status(thm)],[a8_31])).
% 0.24/0.53 cnf(c_0_18, plain, (in_environment(X1,X2)|~environment(X1)|~greater_or_equal(X2,start_time(X1))|~greater(X3,X2)|~in_environment(X1,X3)), c_0_12).
% 0.24/0.53 cnf(c_0_19, plain, (greater_or_equal(initial_FM_EP(X1),start_time(X1))|~environment(X1)), c_0_13).
% 0.24/0.53 cnf(c_0_20, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), c_0_14).
% 0.24/0.53 cnf(c_0_21, plain, (greater_or_equal(X2,initial_FM_EP(X1))|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), c_0_15).
% 0.24/0.53 cnf(c_0_22, plain, (in_environment(X1,X2)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(fof_simplification,[status(thm)],[mp_time_point_occurs_26])).
% 0.24/0.53 cnf(c_0_23, plain, (decreases(difference(disbanding_rate(first_movers,X2),disbanding_rate(efficient_producers,X2)))|greater(disbanding_rate(first_movers,X4),disbanding_rate(efficient_producers,X4))|~environment(X1)|~greater_or_equal(X2,X3)|~greater_or_equal(X4,X2)|~subpopulations(first_movers,efficient_producers,X1,X4)|~greater(disbanding_rate(first_movers,X3),disbanding_rate(efficient_producers,X3))), c_0_16).
% 0.24/0.53 cnf(c_0_24, hypothesis, (greater(disbanding_rate(first_movers,initial_FM_EP(X1)),disbanding_rate(efficient_producers,initial_FM_EP(X1)))|~environment(X1)), c_0_17).
% 0.24/0.53 cnf(c_0_25, negated_conjecture, (~greater(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))), inference(fof_simplification,[status(thm)],[prove_l2_35])).
% 0.24/0.53 cnf(c_0_26, plain, (in_environment(X1,initial_FM_EP(X1))|~greater(X2,initial_FM_EP(X1))|~in_environment(X1,X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 0.24/0.53 cnf(c_0_27, plain, (X1=initial_FM_EP(X2)|greater(X1,initial_FM_EP(X2))|~subpopulations(first_movers,efficient_producers,X2,X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 0.24/0.53 cnf(c_0_28, plain, (in_environment(X1,X2)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), c_0_22).
% 0.24/0.53 cnf(c_0_29, hypothesis, (greater(disbanding_rate(first_movers,X1),disbanding_rate(efficient_producers,X1))|decreases(difference(disbanding_rate(first_movers,X2),disbanding_rate(efficient_producers,X2)))|~greater_or_equal(X2,initial_FM_EP(X3))|~greater_or_equal(X1,X2)|~subpopulations(first_movers,efficient_producers,X4,X1)|~environment(X4)|~environment(X3)), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 0.24/0.53 cnf(c_0_30, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk1,sk2)), prove_l2_34).
% 0.24/0.53 cnf(c_0_31, negated_conjecture, (environment(sk1)), prove_l2_33).
% 0.24/0.53 cnf(c_0_32, negated_conjecture, (~greater(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))), c_0_25).
% 0.24/0.53 cnf(c_0_33, plain, (~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~decreases(difference(disbanding_rate(first_movers,X2),disbanding_rate(efficient_producers,X2)))), inference(fof_simplification,[status(thm)],[l3_22])).
% 0.24/0.53 cnf(c_0_34, plain, (subpopulations(first_movers,efficient_producers,X1,initial_FM_EP(X1))|~environment(X1)|~in_environment(X1,initial_FM_EP(X1))), inference(fof_simplification,[status(thm)],[mp_earliest_time_point_23])).
% 0.24/0.53 cnf(c_0_35, plain, (X1=initial_FM_EP(X2)|in_environment(X2,initial_FM_EP(X2))|~subpopulations(first_movers,efficient_producers,X2,X1)|~environment(X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_27]), c_0_28])).
% 0.24/0.53 cnf(c_0_36, negated_conjecture, (decreases(difference(disbanding_rate(first_movers,X1),disbanding_rate(efficient_producers,X1)))|~greater_or_equal(X1,initial_FM_EP(X2))|~greater_or_equal(sk2,X1)|~environment(X2)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_31])]), c_0_32])).
% 0.24/0.53 cnf(c_0_37, plain, (~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~decreases(difference(disbanding_rate(first_movers,X2),disbanding_rate(efficient_producers,X2)))), c_0_33).
% 0.24/0.53 cnf(c_0_38, plain, (subpopulations(first_movers,efficient_producers,X1,initial_FM_EP(X1))|~environment(X1)|~in_environment(X1,initial_FM_EP(X1))), c_0_34).
% 0.24/0.53 cnf(c_0_39, negated_conjecture, (initial_FM_EP(sk1)=sk2|in_environment(sk1,initial_FM_EP(sk1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_30]), c_0_31])])).
% 0.24/0.53 cnf(c_0_40, negated_conjecture, (~greater_or_equal(sk2,X1)|~subpopulations(first_movers,efficient_producers,X2,X1)|~environment(X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_21]), c_0_37])).
% 0.24/0.53 cnf(c_0_41, negated_conjecture, (initial_FM_EP(sk1)=sk2|subpopulations(first_movers,efficient_producers,sk1,initial_FM_EP(sk1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_31])])).
% 0.24/0.53 cnf(c_0_42, negated_conjecture, (initial_FM_EP(sk1)=sk2|~greater_or_equal(sk2,initial_FM_EP(sk1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_31])])).
% 0.24/0.53 cnf(c_0_43, negated_conjecture, (initial_FM_EP(sk1)=sk2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_21]), c_0_30]), c_0_31])])).
% 0.24/0.53 cnf(c_0_44, hypothesis, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_43]), c_0_31])]), c_0_32]), ['proof']).
% 0.24/0.53 % SZS output end Proof
% 0.24/0.53 % User time : 0.008 s
% 0.24/0.53 % System time : 0.003 s
% 0.24/0.53 % Total time : 0.010 s
% 0.24/0.53 % User time : 0.030 s
% 0.24/0.53 % System time : 0.010 s
% 0.24/0.53 % Total time : 0.040 s
% 0.24/0.53
%------------------------------------------------------------------------------