%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : MGT040-2 : TPTP v9.2.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:48:18 PM UTC 2026
% Result : Satisfiable 1.27s 1.73s
% Output : Saturation 1.27s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(mp_selection_favours_in_time_33,axiom,
( in_environment(X1,critical_point(X1))
| selection_favors(first_movers,efficient_producers,end_time(X1))
| ~ environment(X1)
| ~ greater_or_equal(X2,appear(efficient_producers,X1))
| ~ greater(critical_point(X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_selection_favours_in_time_33) ).
cnf(mp_appearance_of_EP_36,axiom,
( greater(appear(efficient_producers,X1),X2)
| greater_or_equal(X2,appear(efficient_producers,X1))
| ~ in_environment(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_appearance_of_EP_36) ).
cnf(mp_greater_or_equal_35,axiom,
( greater(X1,X2)
| X1 = X2
| ~ greater_or_equal(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_35) ).
cnf(mp6_not_extreme_change_means_not_empty_27,axiom,
( extreme(X1)
| ~ observational_period(X1)
| ~ environment(X2)
| ~ in_environment(X1,X2)
| ~ empty(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp6_not_extreme_change_means_not_empty_27) ).
cnf(mp_endpoint_in_environment_30,axiom,
( in_environment(X1,end_time(X1))
| ~ environment(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_endpoint_in_environment_30) ).
cnf(mp3_favoured_trategy_25,axiom,
( selection_favors(efficient_producers,first_movers,X1)
| ~ observational_period(X1)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_favoured_trategy_25) ).
cnf(mp_organizational_sets1_28,axiom,
propagation_strategy(first_movers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_organizational_sets1_28) ).
cnf(mp_organizational_sets2_29,axiom,
propagation_strategy(efficient_producers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_organizational_sets2_29) ).
cnf(mp3_favoured_trategy_23,axiom,
( environment(sk1(X1))
| selection_favors(efficient_producers,first_movers,X1)
| ~ observational_period(X1)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_favoured_trategy_23) ).
cnf(mp3_favoured_trategy_24,axiom,
( in_environment(X1,sk1(X1))
| selection_favors(efficient_producers,first_movers,X1)
| ~ observational_period(X1)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_favoured_trategy_24) ).
cnf(mp_critical_point_not_before_opening_31,axiom,
( in_environment(X1,critical_point(X1))
| greater(critical_point(X1),end_time(X1))
| ~ environment(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_critical_point_not_before_opening_31) ).
cnf(t3_38,hypothesis,
( selection_favors(first_movers,efficient_producers,X2)
| ~ environment(X1)
| ~ in_environment(X1,critical_point(X1))
| ~ greater_or_equal(X2,appear(efficient_producers,X1))
| ~ greater(critical_point(X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_38) ).
cnf(mp_non_empty_means_organisations_32,axiom,
( empty(X1)
| greater_or_equal(end_time(X1),appear(an_organisation,X1))
| ~ environment(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_non_empty_means_organisations_32) ).
cnf(prove_t9_41,negated_conjecture,
~ extreme(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t9_41) ).
cnf(prove_t9_39,negated_conjecture,
observational_period(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t9_39) ).
cnf(mp5_rapid_change_is_non_critical_26,axiom,
( ~ observational_period(X1)
| ~ rapid_change(X1)
| ~ environment(X2)
| ~ in_environment(X1,X2)
| ~ in_environment(X2,critical_point(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp5_rapid_change_is_non_critical_26) ).
cnf(t2_37,hypothesis,
( selection_favors(first_movers,efficient_producers,X2)
| ~ environment(X1)
| ~ in_environment(X1,X2)
| ~ greater_or_equal(X2,appear(first_movers,X1))
| ~ greater(appear(efficient_producers,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_37) ).
cnf(prove_t9_42,negated_conjecture,
~ selection_favors(first_movers,efficient_producers,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t9_42) ).
cnf(prove_t9_40,negated_conjecture,
rapid_change(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t9_40) ).
cnf(c_0_19,axiom,
( in_environment(X1,critical_point(X1))
| selection_favors(first_movers,efficient_producers,end_time(X1))
| ~ environment(X1)
| ~ greater_or_equal(X2,appear(efficient_producers,X1))
| ~ greater(critical_point(X1),X2) ),
mp_selection_favours_in_time_33,
[final] ).
cnf(c_0_20,axiom,
( greater(appear(efficient_producers,X1),X2)
| greater_or_equal(X2,appear(efficient_producers,X1))
| ~ in_environment(X1,X2) ),
mp_appearance_of_EP_36,
[final] ).
cnf(c_0_21,axiom,
( greater(X1,X2)
| X1 = X2
| ~ greater_or_equal(X1,X2) ),
mp_greater_or_equal_35,
[final] ).
cnf(c_0_22,axiom,
( extreme(X1)
| ~ observational_period(X1)
| ~ environment(X2)
| ~ in_environment(X1,X2)
| ~ empty(X2) ),
mp6_not_extreme_change_means_not_empty_27,
[final] ).
cnf(c_0_23,axiom,
( in_environment(X1,end_time(X1))
| ~ environment(X1) ),
mp_endpoint_in_environment_30,
[final] ).
cnf(c_0_24,axiom,
( selection_favors(efficient_producers,first_movers,X1)
| ~ observational_period(X1)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(X1))) ),
mp3_favoured_trategy_25 ).
cnf(c_0_25,axiom,
propagation_strategy(first_movers),
mp_organizational_sets1_28,
[final] ).
cnf(c_0_26,axiom,
propagation_strategy(efficient_producers),
mp_organizational_sets2_29,
[final] ).
cnf(c_0_27,axiom,
( environment(sk1(X1))
| selection_favors(efficient_producers,first_movers,X1)
| ~ observational_period(X1)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers) ),
mp3_favoured_trategy_23 ).
cnf(c_0_28,axiom,
( in_environment(X1,sk1(X1))
| selection_favors(efficient_producers,first_movers,X1)
| ~ observational_period(X1)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers) ),
mp3_favoured_trategy_24 ).
cnf(c_0_29,plain,
( greater(appear(efficient_producers,X1),X2)
| in_environment(X1,critical_point(X1))
| selection_favors(first_movers,efficient_producers,end_time(X1))
| ~ greater(critical_point(X1),X2)
| ~ in_environment(X1,X2)
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_19,c_0_20]),
[final] ).
cnf(c_0_30,axiom,
( in_environment(X1,critical_point(X1))
| greater(critical_point(X1),end_time(X1))
| ~ environment(X1) ),
mp_critical_point_not_before_opening_31,
[final] ).
cnf(c_0_31,hypothesis,
( selection_favors(first_movers,efficient_producers,X2)
| ~ environment(X1)
| ~ in_environment(X1,critical_point(X1))
| ~ greater_or_equal(X2,appear(efficient_producers,X1))
| ~ greater(critical_point(X1),X2) ),
t3_38,
[final] ).
cnf(c_0_32,plain,
( X1 = appear(efficient_producers,X2)
| greater(appear(efficient_producers,X2),X1)
| greater(X1,appear(efficient_producers,X2))
| ~ in_environment(X2,X1) ),
inference(spm,[status(thm)],[c_0_21,c_0_20]),
[final] ).
cnf(c_0_33,axiom,
( empty(X1)
| greater_or_equal(end_time(X1),appear(an_organisation,X1))
| ~ environment(X1) ),
mp_non_empty_means_organisations_32,
[final] ).
cnf(c_0_34,negated_conjecture,
~ extreme(sk2),
prove_t9_41,
[final] ).
cnf(c_0_35,plain,
( extreme(X1)
| ~ empty(end_time(X1))
| ~ environment(end_time(X1))
| ~ environment(X1)
| ~ observational_period(X1) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]),
[final] ).
cnf(c_0_36,negated_conjecture,
observational_period(sk2),
prove_t9_39,
[final] ).
cnf(c_0_37,plain,
( selection_favors(efficient_producers,first_movers,X1)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(X1)))
| ~ observational_period(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_24,c_0_25]),c_0_26])]),
[final] ).
cnf(c_0_38,plain,
( selection_favors(efficient_producers,first_movers,X1)
| environment(sk1(X1))
| ~ observational_period(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_25]),c_0_26])]),
[final] ).
cnf(c_0_39,plain,
( in_environment(X1,sk1(X1))
| selection_favors(efficient_producers,first_movers,X1)
| ~ observational_period(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_28,c_0_25]),c_0_26])]),
[final] ).
cnf(c_0_40,plain,
( greater(appear(efficient_producers,X1),end_time(X1))
| in_environment(X1,critical_point(X1))
| selection_favors(first_movers,efficient_producers,end_time(X1))
| ~ environment(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_23]),
[final] ).
cnf(c_0_41,hypothesis,
( greater(appear(efficient_producers,X1),X2)
| selection_favors(first_movers,efficient_producers,X2)
| ~ greater(critical_point(X1),X2)
| ~ in_environment(X1,critical_point(X1))
| ~ in_environment(X1,X2)
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_31,c_0_20]),
[final] ).
cnf(c_0_42,plain,
( end_time(X1) = appear(efficient_producers,X1)
| greater(end_time(X1),appear(efficient_producers,X1))
| greater(appear(efficient_producers,X1),end_time(X1))
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_32,c_0_23]),
[final] ).
cnf(c_0_43,plain,
( end_time(X1) = appear(an_organisation,X1)
| greater(end_time(X1),appear(an_organisation,X1))
| empty(X1)
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_21,c_0_33]),
[final] ).
cnf(c_0_44,negated_conjecture,
( ~ empty(end_time(sk2))
| ~ environment(end_time(sk2))
| ~ environment(sk2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_35]),c_0_36])]),
[final] ).
cnf(c_0_45,plain,
( selection_favors(efficient_producers,first_movers,X1)
| environment(sk1(end_time(sk1(X1))))
| ~ observational_period(end_time(sk1(X1)))
| ~ observational_period(X1) ),
inference(spm,[status(thm)],[c_0_37,c_0_38]),
[final] ).
cnf(c_0_46,negated_conjecture,
( in_environment(sk2,sk1(sk2))
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(spm,[status(thm)],[c_0_39,c_0_36]),
[final] ).
cnf(c_0_47,axiom,
( ~ observational_period(X1)
| ~ rapid_change(X1)
| ~ environment(X2)
| ~ in_environment(X1,X2)
| ~ in_environment(X2,critical_point(X2)) ),
mp5_rapid_change_is_non_critical_26,
[final] ).
cnf(c_0_48,hypothesis,
( selection_favors(first_movers,efficient_producers,X2)
| ~ environment(X1)
| ~ in_environment(X1,X2)
| ~ greater_or_equal(X2,appear(first_movers,X1))
| ~ greater(appear(efficient_producers,X1),X2) ),
t2_37,
[final] ).
cnf(c_0_49,negated_conjecture,
~ selection_favors(first_movers,efficient_producers,sk2),
prove_t9_42,
[final] ).
cnf(c_0_50,negated_conjecture,
rapid_change(sk2),
prove_t9_40,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : MGT040-2 : TPTP v9.2.1. Released v2.4.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.17/0.34 % Computer : n023.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Mon May 4 23:30:08 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.35 % start to proof: theBenchmark
% 1.27/1.73 % Version : CSE_E---1.7
% 1.27/1.73 % Problem : theBenchmark.p
% 1.27/1.73 % SZS status Satisfiable for theBenchmark.p
% 1.27/1.73 % SZS output start Saturation
% See solution above
% 1.27/1.73 % Total time : 1.375s
%------------------------------------------------------------------------------