%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT040+1 : 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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/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 5.06s 1.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT040+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.08/0.33 % Computer : n001.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 13:02:52 UTC 2026
% 0.08/0.33 % CPUTime :
% 5.06/1.97
% 5.06/1.97 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.06/1.98
% 5.06/1.98 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.06/1.99 %$ 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
% 5.06/1.99
% 5.06/1.99 %Foreground sorts:
% 5.06/1.99
% 5.06/1.99
% 5.06/1.99 %Background operators:
% 5.06/1.99
% 5.06/1.99
% 5.06/1.99 %Foreground operators:
% 5.06/1.99 tff(greater, type, greater: ($i * $i) > $o).
% 5.06/1.99 tff(in_environment, type, in_environment: ($i * $i) > $o).
% 5.06/1.99 tff(observational_period, type, observational_period: $i > $o).
% 5.06/1.99 tff(rapid_change, type, rapid_change: $i > $o).
% 5.06/1.99 tff('#skF_1', type, '#skF_1': $i > $i).
% 5.06/1.99 tff(appear, type, appear: ($i * $i) > $i).
% 5.06/1.99 tff(efficient_producers, type, efficient_producers: $i).
% 5.06/1.99 tff(extreme, type, extreme: $i > $o).
% 5.06/1.99 tff(critical_point, type, critical_point: $i > $i).
% 5.06/1.99 tff('#skF_2', type, '#skF_2': $i).
% 5.06/1.99 tff(environment, type, environment: $i > $o).
% 5.06/1.99 tff(empty, type, empty: $i > $o).
% 5.06/1.99 tff(end_time, type, end_time: $i > $i).
% 5.06/1.99 tff(first_movers, type, first_movers: $i).
% 5.06/1.99 tff(an_organisation, type, an_organisation: $i).
% 5.06/1.99 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o).
% 5.06/1.99 tff(selection_favors, type, selection_favors: ($i * $i * $i) > $o).
% 5.06/1.99 tff(propagation_strategy, type, propagation_strategy: $i > $o).
% 5.06/1.99
% 5.06/1.99 %Saturated clause set:
% 5.06/1.99 tff(c_243, plain, (![P_80, T_60]: (~rapid_change('#skF_1'(P_80)) | ~observational_period('#skF_1'(P_80)) | selection_favors(first_movers, efficient_producers, end_time(critical_point('#skF_1'(P_80)))) | ~greater(critical_point(critical_point('#skF_1'(P_80))), T_60) | ~environment(critical_point('#skF_1'(P_80))) | greater(appear(efficient_producers, critical_point('#skF_1'(P_80))), T_60) | ~in_environment(critical_point('#skF_1'(P_80)), T_60) | extreme(P_80) | selection_favors(efficient_producers, first_movers, P_80) | ~observational_period(P_80) | empty('#skF_1'(P_80)) | selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_80))) | ~environment('#skF_1'(P_80))))).
% 5.06/1.99 tff(c_170, plain, (![E_17, T_63, T_18]: (~rapid_change(E_17) | ~observational_period(E_17) | selection_favors(first_movers, efficient_producers, end_time(critical_point(E_17))) | ~greater(critical_point(critical_point(E_17)), T_63) | ~environment(critical_point(E_17)) | greater(appear(efficient_producers, critical_point(E_17)), T_63) | ~in_environment(critical_point(E_17), T_63) | selection_favors(first_movers, efficient_producers, end_time(E_17)) | ~greater(critical_point(E_17), T_18) | ~environment(E_17) | greater(appear(efficient_producers, E_17), T_18) | ~in_environment(E_17, T_18)))).
% 5.06/1.99 tff(c_222, plain, (![P_77]: (selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_77))) | extreme(P_77) | selection_favors(efficient_producers, first_movers, P_77) | ~observational_period(P_77) | empty('#skF_1'(P_77)) | ~environment('#skF_1'(P_77)) | appear(efficient_producers, '#skF_1'(P_77))=end_time('#skF_1'(P_77)) | greater(end_time('#skF_1'(P_77)), appear(efficient_producers, '#skF_1'(P_77))) | ~in_environment('#skF_1'(P_77), end_time('#skF_1'(P_77)))))).
% 5.06/1.99 tff(c_246, plain, (![P_80]: (~empty(critical_point('#skF_1'(P_80))) | ~environment(critical_point('#skF_1'(P_80))) | extreme('#skF_1'(P_80)) | ~observational_period('#skF_1'(P_80)) | extreme(P_80) | selection_favors(efficient_producers, first_movers, P_80) | ~observational_period(P_80) | empty('#skF_1'(P_80)) | selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_80))) | ~environment('#skF_1'(P_80))))).
% 5.06/1.99 tff(c_251, plain, (![P_1]: (~rapid_change(P_1) | extreme(P_1) | empty('#skF_1'(P_1)) | selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_1))) | ~environment('#skF_1'(P_1)) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 5.06/1.99 tff(c_245, plain, (![P_3, P_80]: (~in_environment(P_3, '#skF_1'(P_80)) | ~rapid_change(P_3) | ~observational_period(P_3) | extreme(P_80) | selection_favors(efficient_producers, first_movers, P_80) | ~observational_period(P_80) | empty('#skF_1'(P_80)) | selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_80))) | ~environment('#skF_1'(P_80))))).
% 5.06/1.99 tff(c_171, plain, (![E_11, T_63]: (~rapid_change(E_11) | ~observational_period(E_11) | selection_favors(first_movers, efficient_producers, end_time(appear(an_organisation, E_11))) | ~greater(critical_point(appear(an_organisation, E_11)), T_63) | ~environment(appear(an_organisation, E_11)) | greater(appear(efficient_producers, appear(an_organisation, E_11)), T_63) | ~in_environment(appear(an_organisation, E_11), T_63) | empty(E_11) | ~environment(E_11)))).
% 5.06/1.99 tff(c_232, plain, (![P_79]: (extreme(P_79) | selection_favors(efficient_producers, first_movers, P_79) | ~observational_period(P_79) | empty('#skF_1'(P_79)) | selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_79))) | in_environment('#skF_1'(P_79), critical_point('#skF_1'(P_79))) | ~environment('#skF_1'(P_79))))).
% 5.06/2.00 tff(c_219, plain, (![P_77]: (extreme(P_77) | selection_favors(efficient_producers, first_movers, P_77) | ~observational_period(P_77) | empty('#skF_1'(P_77)) | selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_77))) | ~greater(critical_point('#skF_1'(P_77)), end_time('#skF_1'(P_77))) | ~environment('#skF_1'(P_77)) | ~in_environment('#skF_1'(P_77), end_time('#skF_1'(P_77)))))).
% 5.06/2.00 tff(c_199, plain, (![P_74]: (selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_74))) | ~greater(appear(efficient_producers, '#skF_1'(P_74)), end_time('#skF_1'(P_74))) | ~in_environment('#skF_1'(P_74), end_time('#skF_1'(P_74))) | extreme(P_74) | selection_favors(efficient_producers, first_movers, P_74) | ~observational_period(P_74) | empty('#skF_1'(P_74)) | ~environment('#skF_1'(P_74))))).
% 5.06/2.00 tff(c_172, plain, (![P_1, T_63]: (~rapid_change(P_1) | selection_favors(first_movers, efficient_producers, end_time('#skF_1'(P_1))) | ~greater(critical_point('#skF_1'(P_1)), T_63) | ~environment('#skF_1'(P_1)) | greater(appear(efficient_producers, '#skF_1'(P_1)), T_63) | ~in_environment('#skF_1'(P_1), T_63) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 5.06/2.00 tff(c_144, plain, (![T_53, P_51]: (selection_favors(first_movers, efficient_producers, T_53) | ~greater(appear(efficient_producers, '#skF_1'(P_51)), T_53) | ~greater_or_equal(T_53, appear(an_organisation, '#skF_1'(P_51))) | ~in_environment('#skF_1'(P_51), T_53) | ~environment('#skF_1'(P_51)) | extreme(P_51) | selection_favors(efficient_producers, first_movers, P_51) | ~observational_period(P_51)))).
% 5.06/2.00 tff(c_173, plain, (![E_9, T_63]: (~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_63) | ~environment(end_time(E_9)) | greater(appear(efficient_producers, end_time(E_9)), T_63) | ~in_environment(end_time(E_9), T_63) | ~environment(E_9)))).
% 5.06/2.00 tff(c_188, plain, (![T_18, E_59]: (selection_favors(first_movers, efficient_producers, T_18) | selection_favors(first_movers, efficient_producers, end_time(E_59)) | ~greater(critical_point(E_59), T_18) | ~environment(E_59) | ~in_environment(E_59, T_18) | greater(appear(efficient_producers, E_59), T_18)))).
% 5.06/2.00 tff(c_160, plain, (![E_59, T_60]: (~empty(critical_point(E_59)) | ~environment(critical_point(E_59)) | extreme(E_59) | ~observational_period(E_59) | selection_favors(first_movers, efficient_producers, end_time(E_59)) | ~greater(critical_point(E_59), T_60) | ~environment(E_59) | greater(appear(efficient_producers, E_59), T_60) | ~in_environment(E_59, T_60)))).
% 5.06/2.00 tff(c_159, plain, (![P_3, E_59, T_60]: (~in_environment(P_3, E_59) | ~rapid_change(P_3) | ~observational_period(P_3) | selection_favors(first_movers, efficient_producers, end_time(E_59)) | ~greater(critical_point(E_59), T_60) | ~environment(E_59) | greater(appear(efficient_producers, E_59), T_60) | ~in_environment(E_59, T_60)))).
% 5.06/2.00 tff(c_148, plain, (![E_17, T_18]: (selection_favors(first_movers, efficient_producers, end_time(E_17)) | in_environment(E_17, critical_point(E_17)) | ~greater(critical_point(E_17), T_18) | ~environment(E_17) | greater(appear(efficient_producers, E_17), T_18) | ~in_environment(E_17, T_18)))).
% 5.06/2.00 tff(c_109, plain, (![T_18, E_17]: (selection_favors(first_movers, efficient_producers, T_18) | ~greater(critical_point(E_17), T_18) | ~in_environment(E_17, critical_point(E_17)) | ~environment(E_17) | greater(appear(efficient_producers, E_17), T_18) | ~in_environment(E_17, T_18)))).
% 5.06/2.00 tff(c_26, plain, (![E_13, T_14]: (selection_favors(first_movers, efficient_producers, end_time(E_13)) | in_environment(E_13, critical_point(E_13)) | ~greater(critical_point(E_13), T_14) | ~greater_or_equal(T_14, appear(efficient_producers, E_13)) | ~environment(E_13)))).
% 5.06/2.00 tff(c_32, plain, (![T_20, E_19]: (selection_favors(first_movers, efficient_producers, T_20) | ~greater(appear(efficient_producers, E_19), T_20) | ~greater_or_equal(T_20, appear(first_movers, E_19)) | ~in_environment(E_19, T_20) | ~environment(E_19)))).
% 5.06/2.00 tff(c_131, plain, (![P_51]: (extreme(P_51) | appear(first_movers, '#skF_1'(P_51))=appear(an_organisation, '#skF_1'(P_51)) | selection_favors(efficient_producers, first_movers, P_51) | ~observational_period(P_51)))).
% 5.06/2.00 tff(c_97, plain, (![P_1]: (appear(first_movers, '#skF_1'(P_1))=appear(an_organisation, '#skF_1'(P_1)) | empty('#skF_1'(P_1)) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 5.06/2.00 tff(c_76, plain, (![E_36, T_35]: (appear(efficient_producers, E_36)=T_35 | greater(T_35, appear(efficient_producers, E_36)) | greater(appear(efficient_producers, E_36), T_35) | ~in_environment(E_36, T_35)))).
% 5.06/2.00 tff(c_34, plain, (![T_22, E_21]: (selection_favors(first_movers, efficient_producers, T_22) | ~greater(critical_point(E_21), T_22) | ~greater_or_equal(T_22, appear(efficient_producers, E_21)) | ~in_environment(E_21, critical_point(E_21)) | ~environment(E_21)))).
% 5.06/2.00 tff(c_86, plain, (![E_38]: (~empty(appear(an_organisation, E_38)) | ~environment(appear(an_organisation, E_38)) | extreme(E_38) | ~observational_period(E_38) | empty(E_38) | ~environment(E_38)))).
% 5.06/2.00 tff(c_58, plain, (![E_28]: (appear(an_organisation, E_28)=end_time(E_28) | greater(end_time(E_28), appear(an_organisation, E_28)) | empty(E_28) | ~environment(E_28)))).
% 5.06/2.00 tff(c_102, plain, (![P_1]: (~empty('#skF_1'(P_1)) | extreme(P_1) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 5.06/2.00 tff(c_92, plain, (![E_11]: (appear(first_movers, E_11)=appear(an_organisation, E_11) | empty(E_11) | ~environment(E_11)))).
% 5.06/2.01 tff(c_36, plain, (![E_23]: (appear(first_movers, E_23)=appear(an_organisation, E_23) | ~in_environment(E_23, appear(an_organisation, E_23)) | ~environment(E_23)))).
% 5.06/2.01 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)))).
% 5.06/2.01 tff(c_81, plain, (![E_11]: (in_environment(E_11, appear(an_organisation, E_11)) | empty(E_11) | ~environment(E_11)))).
% 5.06/2.01 tff(c_22, plain, (![E_12]: (in_environment(E_12, appear(an_organisation, E_12)) | ~greater_or_equal(end_time(E_12), appear(an_organisation, E_12)) | ~environment(E_12)))).
% 5.06/2.01 tff(c_30, plain, (![T_18, E_17]: (greater_or_equal(T_18, appear(efficient_producers, E_17)) | greater(appear(efficient_producers, E_17), T_18) | ~in_environment(E_17, T_18)))).
% 5.06/2.01 tff(c_68, plain, (![E_9]: (~empty(end_time(E_9)) | ~environment(end_time(E_9)) | extreme(E_9) | ~observational_period(E_9) | ~environment(E_9)))).
% 5.06/2.01 tff(c_50, 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)))).
% 5.06/2.01 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)))).
% 5.06/2.01 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)))).
% 5.06/2.01 tff(c_48, plain, (![P_1]: (in_environment(P_1, '#skF_1'(P_1)) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 5.06/2.01 tff(c_20, plain, (![E_11]: (greater_or_equal(end_time(E_11), appear(an_organisation, E_11)) | empty(E_11) | ~environment(E_11)))).
% 5.06/2.01 tff(c_46, plain, (![P_1]: (environment('#skF_1'(P_1)) | selection_favors(efficient_producers, first_movers, P_1) | ~observational_period(P_1)))).
% 5.06/2.01 tff(c_28, plain, (![Y_16, X_15]: (Y_16=X_15 | greater(X_15, Y_16) | ~greater_or_equal(X_15, Y_16)))).
% 5.06/2.01 tff(c_16, plain, (![E_9]: (in_environment(E_9, end_time(E_9)) | ~environment(E_9)))).
% 5.06/2.01 tff(c_38, plain, (~selection_favors(first_movers, efficient_producers, '#skF_2'))).
% 5.06/2.01 tff(c_14, plain, (propagation_strategy(efficient_producers))).
% 5.06/2.01 tff(c_40, plain, (~extreme('#skF_2'))).
% 5.06/2.01 tff(c_12, plain, (propagation_strategy(first_movers))).
% 5.06/2.01 tff(c_42, plain, (rapid_change('#skF_2'))).
% 5.06/2.01 tff(c_44, plain, (observational_period('#skF_2'))).
% 5.06/2.01 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.06/2.01
%------------------------------------------------------------------------------