%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT040+2 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n001.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:02:58 AM UTC 2026
% Result : CounterSatisfiable 4.49s 2.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT040+2 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 13:05:07 UTC 2026
% 0.08/0.36 % CPUTime :
% 4.49/2.51
% 4.49/2.52 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.49/2.52
% 4.49/2.52 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.49/2.53 %$ selection_favors > in_environment > greater_or_equal > greater > rapid_change > propagation_strategy > observational_period > extreme > environment > empty > appear > #nlpp > end_time > critical_point > first_movers > efficient_producers > an_organisation > #skF_1 > #skF_2
% 4.49/2.53
% 4.49/2.53 %Foreground sorts:
% 4.49/2.53
% 4.49/2.53
% 4.49/2.53 %Background operators:
% 4.49/2.53
% 4.49/2.53
% 4.49/2.53 %Foreground operators:
% 4.49/2.53 tff(greater, type, greater: ($i * $i) > $o).
% 4.49/2.53 tff(in_environment, type, in_environment: ($i * $i) > $o).
% 4.49/2.53 tff(observational_period, type, observational_period: $i > $o).
% 4.49/2.53 tff(rapid_change, type, rapid_change: $i > $o).
% 4.49/2.53 tff('#skF_1', type, '#skF_1': $i > $i).
% 4.49/2.53 tff(appear, type, appear: ($i * $i) > $i).
% 4.49/2.53 tff(efficient_producers, type, efficient_producers: $i).
% 4.49/2.53 tff(extreme, type, extreme: $i > $o).
% 4.49/2.53 tff(critical_point, type, critical_point: $i > $i).
% 4.49/2.53 tff('#skF_2', type, '#skF_2': $i).
% 4.49/2.53 tff(environment, type, environment: $i > $o).
% 4.49/2.53 tff(empty, type, empty: $i > $o).
% 4.49/2.53 tff(end_time, type, end_time: $i > $i).
% 4.49/2.53 tff(first_movers, type, first_movers: $i).
% 4.49/2.53 tff(an_organisation, type, an_organisation: $i).
% 4.49/2.53 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o).
% 4.49/2.53 tff(selection_favors, type, selection_favors: ($i * $i * $i) > $o).
% 4.49/2.53 tff(propagation_strategy, type, propagation_strategy: $i > $o).
% 4.49/2.53
% 4.49/2.53 %Saturated clause set:
% 4.49/2.53 tff(c_126, plain, (![E_16, T_54, T_17]: (~rapid_change(E_16) | ~observational_period(E_16) | selection_favors(first_movers, efficient_producers, end_time(critical_point(E_16))) | ~greater(critical_point(critical_point(E_16)), T_54) | ~environment(critical_point(E_16)) | greater(appear(efficient_producers, critical_point(E_16)), T_54) | ~in_environment(critical_point(E_16), T_54) | selection_favors(first_movers, efficient_producers, end_time(E_16)) | ~greater(critical_point(E_16), T_17) | ~environment(E_16) | greater(appear(efficient_producers, E_16), T_17) | ~in_environment(E_16, T_17)))).
% 4.49/2.53 tff(c_145, plain, (![T_17, E_50]: (selection_favors(first_movers, efficient_producers, T_17) | selection_favors(first_movers, efficient_producers, end_time(E_50)) | ~greater(critical_point(E_50), T_17) | ~environment(E_50) | ~in_environment(E_50, T_17) | greater(appear(efficient_producers, E_50), T_17)))).
% 4.49/2.53 tff(c_127, plain, (![P_1, T_54]: (~rapid_change(P_1) | selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_1))) | ~greater(critical_point('#skF_1'(P_1)), T_54) | ~environment('#skF_1'(P_1)) | greater(appear(efficient_producers, '#skF_1'(P_1)), T_54) | ~in_environment('#skF_1'(P_1), T_54) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 4.49/2.53 tff(c_128, plain, (![E_9, T_54]: (~rapid_change(E_9) | ~observational_period(E_9) | selection_favors(first_movers, efficient_producers, end_time(end_time(E_9))) | ~greater(critical_point(end_time(E_9)), T_54) | ~environment(end_time(E_9)) | greater(appear(efficient_producers, end_time(E_9)), T_54) | ~in_environment(end_time(E_9), T_54) | ~environment(E_9)))).
% 4.49/2.53 tff(c_118, plain, (![E_50, T_51]: (~empty(critical_point(E_50)) | ~environment(critical_point(E_50)) | extreme(E_50) | ~observational_period(E_50) | selection_favors(first_movers, efficient_producers, end_time(E_50)) | ~greater(critical_point(E_50), T_51) | ~environment(E_50) | greater(appear(efficient_producers, E_50), T_51) | ~in_environment(E_50, T_51)))).
% 4.49/2.53 tff(c_117, plain, (![P_3, E_50, T_51]: (~in_environment(P_3, E_50) | ~rapid_change(P_3) | ~observational_period(P_3) | selection_favors(first_movers, efficient_producers, end_time(E_50)) | ~greater(critical_point(E_50), T_51) | ~environment(E_50) | greater(appear(efficient_producers, E_50), T_51) | ~in_environment(E_50, T_51)))).
% 4.49/2.54 tff(c_106, plain, (![E_16, T_17]: (selection_favors(first_movers, efficient_producers, end_time(E_16)) | in_environment(E_16, critical_point(E_16)) | ~greater(critical_point(E_16), T_17) | ~environment(E_16) | greater(appear(efficient_producers, E_16), T_17) | ~in_environment(E_16, T_17)))).
% 4.49/2.54 tff(c_83, plain, (![T_17, E_16]: (selection_favors(first_movers, efficient_producers, T_17) | ~greater(critical_point(E_16), T_17) | ~in_environment(E_16, critical_point(E_16)) | ~environment(E_16) | greater(appear(efficient_producers, E_16), T_17) | ~in_environment(E_16, T_17)))).
% 4.49/2.54 tff(c_24, plain, (![E_12, T_13]: (selection_favors(first_movers, efficient_producers, end_time(E_12)) | in_environment(E_12, critical_point(E_12)) | ~greater(critical_point(E_12), T_13) | ~greater_or_equal(T_13, appear(efficient_producers, E_12)) | ~environment(E_12)))).
% 4.49/2.54 tff(c_30, plain, (![T_19, E_18]: (selection_favors(first_movers, efficient_producers, T_19) | ~greater(appear(efficient_producers, E_18), T_19) | ~greater_or_equal(T_19, appear(first_movers, E_18)) | ~in_environment(E_18, T_19) | ~environment(E_18)))).
% 4.49/2.54 tff(c_72, plain, (![E_34, T_33]: (appear(efficient_producers, E_34)=T_33 | greater(T_33, appear(efficient_producers, E_34)) | greater(appear(efficient_producers, E_34), T_33) | ~in_environment(E_34, T_33)))).
% 4.49/2.54 tff(c_54, plain, (![E_26]: (appear(an_organisation, E_26)=end_time(E_26) | greater(end_time(E_26), appear(an_organisation, E_26)) | empty(E_26) | ~environment(E_26)))).
% 4.49/2.54 tff(c_32, plain, (![T_21, E_20]: (selection_favors(first_movers, efficient_producers, T_21) | ~greater(critical_point(E_20), T_21) | ~greater_or_equal(T_21, appear(efficient_producers, E_20)) | ~in_environment(E_20, critical_point(E_20)) | ~environment(E_20)))).
% 4.49/2.54 tff(c_78, plain, (![P_1]: (~empty('#skF_1'(P_1)) | extreme(P_1) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 4.49/2.54 tff(c_8, plain, (![E_5, P_3]: (~in_environment(E_5, critical_point(E_5)) | ~in_environment(P_3, E_5) | ~environment(E_5) | ~rapid_change(P_3) | ~observational_period(P_3)))).
% 4.49/2.54 tff(c_28, plain, (![T_17, E_16]: (greater_or_equal(T_17, appear(efficient_producers, E_16)) | greater(appear(efficient_producers, E_16), T_17) | ~in_environment(E_16, T_17)))).
% 4.49/2.54 tff(c_65, plain, (![E_9]: (~empty(end_time(E_9)) | ~environment(end_time(E_9)) | extreme(E_9) | ~observational_period(E_9) | ~environment(E_9)))).
% 4.49/2.54 tff(c_46, plain, (![P_1]: (~selection_favors(efficient_producers, first_movers, end_time('#skF_1'(P_1))) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 4.49/2.54 tff(c_10, plain, (![E_8, P_6]: (~empty(E_8) | ~in_environment(P_6, E_8) | ~environment(E_8) | extreme(P_6) | ~observational_period(P_6)))).
% 4.49/2.54 tff(c_18, plain, (![E_10]: (greater(critical_point(E_10), end_time(E_10)) | in_environment(E_10, critical_point(E_10)) | ~environment(E_10)))).
% 4.49/2.54 tff(c_44, plain, (![P_1]: (in_environment(P_1, '#skF_1'(P_1)) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 4.49/2.54 tff(c_20, plain, (![E_11]: (greater_or_equal(end_time(E_11), appear(an_organisation, E_11)) | empty(E_11) | ~environment(E_11)))).
% 4.49/2.54 tff(c_42, plain, (![P_1]: (environment('#skF_1'(P_1)) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 4.49/2.54 tff(c_26, plain, (![Y_15, X_14]: (Y_15=X_14 | greater(X_14, Y_15) | ~greater_or_equal(X_14, Y_15)))).
% 4.49/2.54 tff(c_16, plain, (![E_9]: (in_environment(E_9, end_time(E_9)) | ~environment(E_9)))).
% 4.49/2.54 tff(c_34, plain, (~selection_favors(first_movers, efficient_producers, '#skF_2'))).
% 4.49/2.54 tff(c_12, plain, (propagation_strategy(first_movers))).
% 4.49/2.54 tff(c_14, plain, (propagation_strategy(efficient_producers))).
% 4.49/2.54 tff(c_36, plain, (~extreme('#skF_2'))).
% 4.49/2.54 tff(c_38, plain, (rapid_change('#skF_2'))).
% 4.49/2.54 tff(c_40, plain, (observational_period('#skF_2'))).
% 4.49/2.54 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.49/2.54
%------------------------------------------------------------------------------