%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT031+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 : n004.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:55 AM UTC 2026
% Result : CounterSatisfiable 3.67s 2.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT031+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % 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.35 % Computer : n004.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 12:20:30 UTC 2026
% 0.08/0.35 % CPUTime :
% 3.67/2.05
% 3.67/2.05 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.67/2.05
% 3.67/2.05 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.67/2.05 %$ subpopulation > in_environment > greater_or_equal > greater > environment > number_of_organizations > cardinality_at_time > appear > #nlpp > zero > first_movers > efficient_producers > e > an_organisation > #skF_2 > #skF_1
% 3.67/2.05
% 3.67/2.05 %Foreground sorts:
% 3.67/2.05
% 3.67/2.05
% 3.67/2.05 %Background operators:
% 3.67/2.05
% 3.67/2.05
% 3.67/2.05 %Foreground operators:
% 3.67/2.05 tff(greater, type, greater: ($i * $i) > $o).
% 3.67/2.05 tff(number_of_organizations, type, number_of_organizations: ($i * $i) > $i).
% 3.67/2.05 tff(in_environment, type, in_environment: ($i * $i) > $o).
% 3.67/2.05 tff(appear, type, appear: ($i * $i) > $i).
% 3.67/2.05 tff(efficient_producers, type, efficient_producers: $i).
% 3.67/2.05 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i).
% 3.67/2.05 tff('#skF_2', type, '#skF_2': $i).
% 3.67/2.05 tff(environment, type, environment: $i > $o).
% 3.67/2.05 tff(first_movers, type, first_movers: $i).
% 3.67/2.05 tff(an_organisation, type, an_organisation: $i).
% 3.67/2.05 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o).
% 3.67/2.05 tff(e, type, e: $i).
% 3.67/2.05 tff('#skF_1', type, '#skF_1': ($i * $i) > $i).
% 3.67/2.05 tff(subpopulation, type, subpopulation: ($i * $i * $i) > $o).
% 3.67/2.05 tff(zero, type, zero: $i).
% 3.67/2.05
% 3.67/2.05 %Saturated clause set:
% 3.67/2.06 tff(c_150, plain, (![X_10, E_68, E_67]: (greater(X_10, appear(an_organisation, E_68)) | ~greater(X_10, appear(first_movers, E_67)) | appear(first_movers, E_68)=appear(an_organisation, E_68) | ~greater(appear(an_organisation, E_67), appear(efficient_producers, e)) | ~environment(E_68) | appear(first_movers, E_67)=appear(an_organisation, E_67) | ~environment(E_67)))).
% 3.67/2.06 tff(c_131, plain, (![E_62, E_63]: (greater(appear(first_movers, E_62), appear(an_organisation, E_63)) | appear(first_movers, E_63)=appear(an_organisation, E_63) | ~greater(appear(an_organisation, E_62), appear(efficient_producers, e)) | ~environment(E_63) | appear(first_movers, E_62)=appear(an_organisation, E_62) | ~environment(E_62)))).
% 3.67/2.06 tff(c_133, plain, (![X_10, E_63, E_62]: (greater(X_10, appear(first_movers, E_63)) | ~greater(X_10, appear(first_movers, E_62)) | ~greater(appear(an_organisation, E_62), appear(efficient_producers, e)) | ~environment(E_63) | appear(first_movers, E_62)=appear(an_organisation, E_62) | ~environment(E_62)))).
% 3.67/2.06 tff(c_88, plain, (![E_29, E_47]: (greater(appear(first_movers, E_29), appear(first_movers, E_47)) | ~greater(appear(an_organisation, E_29), appear(efficient_producers, e)) | ~environment(E_47) | appear(first_movers, E_29)=appear(an_organisation, E_29) | ~environment(E_29)))).
% 3.67/2.06 tff(c_122, plain, (~environment(e))).
% 3.67/2.06 tff(c_116, plain, (![E_2, T_3]: ('#skF_1'(E_2, T_3)=first_movers | '#skF_1'(E_2, T_3)=efficient_producers | ~greater(number_of_organizations(E_2, T_3), zero) | ~environment(E_2)))).
% 3.67/2.06 tff(c_111, plain, (~greater(zero, appear(efficient_producers, e)))).
% 3.67/2.06 tff(c_101, plain, (![X_10, E_27]: (greater(X_10, appear(an_organisation, E_27)) | appear(first_movers, E_27)=appear(an_organisation, E_27) | ~greater(X_10, appear(efficient_producers, e)) | ~environment(E_27)))).
% 3.67/2.06 tff(c_102, plain, (![E_18]: (greater(appear(efficient_producers, e), appear(an_organisation, E_18)) | appear(first_movers, E_18)=appear(an_organisation, E_18) | ~environment(E_18)))).
% 3.67/2.06 tff(c_76, plain, (![X_10, E_45]: (greater(X_10, appear(an_organisation, E_45)) | ~greater(X_10, appear(first_movers, E_45)) | appear(first_movers, E_45)=appear(an_organisation, E_45) | ~environment(E_45)))).
% 3.67/2.06 tff(c_66, plain, (![X_10, E_36, T_37]: (greater(X_10, zero) | ~greater(X_10, cardinality_at_time('#skF_1'(E_36, T_37), T_37)) | ~greater(number_of_organizations(E_36, T_37), zero) | ~environment(E_36)))).
% 3.67/2.06 tff(c_61, plain, (![X_10, E_33, X_32]: (greater(X_10, appear(first_movers, E_33)) | ~greater(X_10, X_32) | ~greater(X_32, appear(efficient_producers, e)) | ~environment(E_33)))).
% 3.67/2.06 tff(c_56, plain, (![E_29]: (appear(first_movers, E_29)=appear(an_organisation, E_29) | greater(appear(first_movers, E_29), appear(an_organisation, E_29)) | ~environment(E_29)))).
% 3.67/2.06 tff(c_10, plain, (![T_8, E_7]: (~greater(cardinality_at_time(first_movers, T_8), zero) | ~greater(appear(first_movers, E_7), T_8) | ~in_environment(E_7, T_8) | ~environment(E_7)))).
% 3.67/2.06 tff(c_8, plain, (![T_6, E_5]: (~greater(cardinality_at_time(efficient_producers, T_6), zero) | ~greater(appear(efficient_producers, E_5), T_6) | ~in_environment(E_5, T_6) | ~environment(E_5)))).
% 3.67/2.06 tff(c_22, plain, (![X_16, T_17, E_15]: (first_movers=X_16 | efficient_producers=X_16 | ~greater(cardinality_at_time(X_16, T_17), zero) | ~subpopulation(X_16, E_15, T_17) | ~environment(E_15)))).
% 3.67/2.06 tff(c_4, plain, (![E_2, T_3]: (greater(cardinality_at_time('#skF_1'(E_2, T_3), T_3), zero) | ~greater(number_of_organizations(E_2, T_3), zero) | ~environment(E_2)))).
% 3.67/2.06 tff(c_6, plain, (![E_2, T_3]: (subpopulation('#skF_1'(E_2, T_3), E_2, T_3) | ~greater(number_of_organizations(E_2, T_3), zero) | ~environment(E_2)))).
% 3.67/2.06 tff(c_47, plain, (![X_10, E_27]: (greater(X_10, appear(first_movers, E_27)) | ~greater(X_10, appear(efficient_producers, e)) | ~environment(E_27)))).
% 3.67/2.06 tff(c_51, plain, (![X_10, E_28]: (greater(X_10, zero) | ~greater(X_10, number_of_organizations(e, appear(an_organisation, E_28))) | ~environment(E_28)))).
% 3.67/2.06 tff(c_12, plain, (![E_9]: (greater_or_equal(appear(first_movers, E_9), appear(an_organisation, E_9)) | ~environment(E_9)))).
% 3.67/2.06 tff(c_2, plain, (![E_1]: (greater(number_of_organizations(e, appear(an_organisation, E_1)), zero) | ~environment(E_1)))).
% 3.67/2.06 tff(c_24, plain, (![E_18]: (greater(appear(efficient_producers, e), appear(first_movers, E_18)) | ~environment(E_18)))).
% 3.67/2.06 tff(c_14, plain, (![X_10, Z_12, Y_11]: (greater(X_10, Z_12) | ~greater(Y_11, Z_12) | ~greater(X_10, Y_11)))).
% 3.67/2.06 tff(c_16, plain, (![Y_14, X_13]: (Y_14=X_13 | greater(X_13, Y_14) | ~greater_or_equal(X_13, Y_14)))).
% 3.67/2.06 tff(c_26, plain, (appear(first_movers, '#skF_2')!=appear(an_organisation, '#skF_2'))).
% 3.67/2.06 tff(c_20, plain, (![X_13, Y_14]: (~greater(X_13, Y_14) | greater_or_equal(X_13, Y_14)))).
% 3.67/2.06 tff(c_28, plain, (in_environment('#skF_2', appear(an_organisation, '#skF_2')))).
% 3.67/2.06 tff(c_18, plain, (![Y_14]: (greater_or_equal(Y_14, Y_14)))).
% 3.67/2.06 tff(c_30, plain, (environment('#skF_2'))).
% 3.67/2.06 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.67/2.06
%------------------------------------------------------------------------------