%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : MGT040-1 : TPTP v9.2.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n006.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:17 PM UTC 2026
% Result : Satisfiable 1.24s 1.71s
% Output : Saturation 1.24s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
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/sandbox2/benchmark/theBenchmark.p',mp3_favoured_trategy_25) ).
cnf(mp_organizational_sets1_28,axiom,
propagation_strategy(first_movers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_organizational_sets1_28) ).
cnf(mp_organizational_sets2_29,axiom,
propagation_strategy(efficient_producers),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',mp3_favoured_trategy_23) ).
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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',mp_endpoint_in_environment_30) ).
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/sandbox2/benchmark/theBenchmark.p',mp3_favoured_trategy_24) ).
cnf(mp_selection_favours_in_time_34,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/sandbox2/benchmark/theBenchmark.p',mp_selection_favours_in_time_34) ).
cnf(mp_greater_or_equal_36,axiom,
( greater(X1,X2)
| X1 = X2
| ~ greater_or_equal(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_36) ).
cnf(t3_39,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/sandbox2/benchmark/theBenchmark.p',t3_39) ).
cnf(t2_38,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/sandbox2/benchmark/theBenchmark.p',t2_38) ).
cnf(mp_appearance_of_EP_37,axiom,
( greater(appear(efficient_producers,X1),X2)
| greater_or_equal(X2,appear(efficient_producers,X1))
| ~ in_environment(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_appearance_of_EP_37) ).
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/sandbox2/benchmark/theBenchmark.p',mp_critical_point_not_before_opening_31) ).
cnf(mp_appearance_before_end_holds_33,axiom,
( in_environment(X1,appear(an_organisation,X1))
| ~ environment(X1)
| ~ greater_or_equal(end_time(X1),appear(an_organisation,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_appearance_before_end_holds_33) ).
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/sandbox2/benchmark/theBenchmark.p',mp_non_empty_means_organisations_32) ).
cnf(prove_t9_43,negated_conjecture,
~ extreme(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t9_43) ).
cnf(prove_t9_41,negated_conjecture,
observational_period(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t9_41) ).
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/sandbox2/benchmark/theBenchmark.p',mp5_rapid_change_is_non_critical_26) ).
cnf(l13_40,hypothesis,
( appear(an_organisation,X1) = appear(first_movers,X1)
| ~ environment(X1)
| ~ in_environment(X1,appear(an_organisation,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l13_40) ).
cnf(prove_t9_44,negated_conjecture,
~ selection_favors(first_movers,efficient_producers,sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t9_44) ).
cnf(prove_t9_42,negated_conjecture,
rapid_change(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t9_42) ).
cnf(c_0_21,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_22,axiom,
propagation_strategy(first_movers),
mp_organizational_sets1_28,
[final] ).
cnf(c_0_23,axiom,
propagation_strategy(efficient_producers),
mp_organizational_sets2_29,
[final] ).
cnf(c_0_24,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_25,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_26,axiom,
( in_environment(X1,end_time(X1))
| ~ environment(X1) ),
mp_endpoint_in_environment_30,
[final] ).
cnf(c_0_27,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_28,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_34,
[final] ).
cnf(c_0_29,axiom,
( greater(X1,X2)
| X1 = X2
| ~ greater_or_equal(X1,X2) ),
mp_greater_or_equal_36,
[final] ).
cnf(c_0_30,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_39,
[final] ).
cnf(c_0_31,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_38,
[final] ).
cnf(c_0_32,axiom,
( greater(appear(efficient_producers,X1),X2)
| greater_or_equal(X2,appear(efficient_producers,X1))
| ~ in_environment(X1,X2) ),
mp_appearance_of_EP_37,
[final] ).
cnf(c_0_33,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_34,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_21,c_0_22]),c_0_23])]),
[final] ).
cnf(c_0_35,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_24,c_0_22]),c_0_23])]),
[final] ).
cnf(c_0_36,axiom,
( in_environment(X1,appear(an_organisation,X1))
| ~ environment(X1)
| ~ greater_or_equal(end_time(X1),appear(an_organisation,X1)) ),
mp_appearance_before_end_holds_33,
[final] ).
cnf(c_0_37,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_38,negated_conjecture,
~ extreme(sk2),
prove_t9_43,
[final] ).
cnf(c_0_39,plain,
( extreme(X1)
| ~ empty(end_time(X1))
| ~ environment(end_time(X1))
| ~ environment(X1)
| ~ observational_period(X1) ),
inference(spm,[status(thm)],[c_0_25,c_0_26]),
[final] ).
cnf(c_0_40,negated_conjecture,
observational_period(sk2),
prove_t9_41,
[final] ).
cnf(c_0_41,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_27,c_0_22]),c_0_23])]),
[final] ).
cnf(c_0_42,plain,
( critical_point(X1) = X2
| in_environment(X1,critical_point(X1))
| selection_favors(first_movers,efficient_producers,end_time(X1))
| ~ greater_or_equal(X2,appear(efficient_producers,X1))
| ~ greater_or_equal(critical_point(X1),X2)
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_28,c_0_29]),
[final] ).
cnf(c_0_43,hypothesis,
( critical_point(X1) = X2
| selection_favors(first_movers,efficient_producers,X2)
| ~ greater_or_equal(X2,appear(efficient_producers,X1))
| ~ greater_or_equal(critical_point(X1),X2)
| ~ in_environment(X1,critical_point(X1))
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_30,c_0_29]),
[final] ).
cnf(c_0_44,hypothesis,
( appear(efficient_producers,X1) = X2
| selection_favors(first_movers,efficient_producers,X2)
| ~ greater_or_equal(X2,appear(first_movers,X1))
| ~ greater_or_equal(appear(efficient_producers,X1),X2)
| ~ in_environment(X1,X2)
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_31,c_0_29]),
[final] ).
cnf(c_0_45,hypothesis,
( greater_or_equal(X1,appear(efficient_producers,X2))
| selection_favors(first_movers,efficient_producers,X1)
| ~ greater_or_equal(X1,appear(first_movers,X2))
| ~ in_environment(X2,X1)
| ~ environment(X2) ),
inference(spm,[status(thm)],[c_0_31,c_0_32]),
[final] ).
cnf(c_0_46,plain,
( in_environment(X1,critical_point(X1))
| selection_favors(first_movers,efficient_producers,end_time(X1))
| ~ greater_or_equal(end_time(X1),appear(efficient_producers,X1))
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_28,c_0_33]),
[final] ).
cnf(c_0_47,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_34,c_0_35]),
[final] ).
cnf(c_0_48,plain,
( empty(X1)
| in_environment(X1,appear(an_organisation,X1))
| ~ environment(X1) ),
inference(spm,[status(thm)],[c_0_36,c_0_37]),
[final] ).
cnf(c_0_49,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_38,c_0_39]),c_0_40])]),
[final] ).
cnf(c_0_50,negated_conjecture,
( in_environment(sk2,sk1(sk2))
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(spm,[status(thm)],[c_0_41,c_0_40]),
[final] ).
cnf(c_0_51,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_52,hypothesis,
( appear(an_organisation,X1) = appear(first_movers,X1)
| ~ environment(X1)
| ~ in_environment(X1,appear(an_organisation,X1)) ),
l13_40,
[final] ).
cnf(c_0_53,negated_conjecture,
~ selection_favors(first_movers,efficient_producers,sk2),
prove_t9_44,
[final] ).
cnf(c_0_54,negated_conjecture,
rapid_change(sk2),
prove_t9_42,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : MGT040-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.32 % Computer : n006.cluster.edu
% 0.16/0.32 % Model : x86_64 x86_64
% 0.16/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.32 % Memory : 8042.1875MB
% 0.16/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.32 % CPULimit : 300
% 0.16/0.32 % WCLimit : 300
% 0.16/0.32 % DateTime : Mon May 4 23:29:31 EDT 2026
% 0.16/0.32 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 1.24/1.71 % Version : CSE_E---1.7
% 1.24/1.71 % Problem : theBenchmark.p
% 1.24/1.71 % SZS status Satisfiable for theBenchmark.p
% 1.24/1.71 % SZS output start Saturation
% See solution above
% 1.24/1.71 % Total time : 1.371s
%------------------------------------------------------------------------------