%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT033+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/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 : n003.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.98s 1.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT033+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/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.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 12:25:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 3.98/1.76
% 3.98/1.77 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.98/1.77
% 3.98/1.77 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.98/1.78 %$ subpopulation > selection_favors > in_environment > greater_or_equal > greater > environment > number_of_organizations > cardinality_at_time > appear > #nlpp > start_time > zero > t > first_movers > efficient_producers > an_organisation > #skF_2 > #skF_3 > #skF_1
% 3.98/1.78
% 3.98/1.78 %Foreground sorts:
% 3.98/1.78
% 3.98/1.78
% 3.98/1.78 %Background operators:
% 3.98/1.78
% 3.98/1.78
% 3.98/1.78 %Foreground operators:
% 3.98/1.78 tff(greater, type, greater: ($i * $i) > $o).
% 3.98/1.78 tff(number_of_organizations, type, number_of_organizations: ($i * $i) > $i).
% 3.98/1.78 tff(in_environment, type, in_environment: ($i * $i) > $o).
% 3.98/1.78 tff(t, type, t: $i).
% 3.98/1.78 tff(appear, type, appear: ($i * $i) > $i).
% 3.98/1.78 tff(efficient_producers, type, efficient_producers: $i).
% 3.98/1.78 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i).
% 3.98/1.78 tff('#skF_2', type, '#skF_2': $i).
% 3.98/1.78 tff('#skF_3', type, '#skF_3': $i).
% 3.98/1.78 tff(environment, type, environment: $i > $o).
% 3.98/1.78 tff(start_time, type, start_time: $i > $i).
% 3.98/1.78 tff(first_movers, type, first_movers: $i).
% 3.98/1.78 tff(an_organisation, type, an_organisation: $i).
% 3.98/1.78 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o).
% 3.98/1.78 tff('#skF_1', type, '#skF_1': ($i * $i) > $i).
% 3.98/1.78 tff(subpopulation, type, subpopulation: ($i * $i * $i) > $o).
% 3.98/1.78 tff(selection_favors, type, selection_favors: ($i * $i * $i) > $o).
% 3.98/1.78 tff(zero, type, zero: $i).
% 3.98/1.78
% 3.98/1.78 %Saturated clause set:
% 3.98/1.78 tff(c_255, plain, (![E_79, T_9, E_8]: (selection_favors('#skF_1'(E_79, T_9), '#skF_1'(E_8, T_9), T_9) | cardinality_at_time('#skF_1'(E_8, T_9), T_9)!=zero | ~subpopulation('#skF_1'(E_79, T_9), E_8, T_9) | ~greater(number_of_organizations(E_79, T_9), zero) | ~environment(E_79) | ~greater(number_of_organizations(E_8, T_9), zero) | ~environment(E_8)))).
% 3.98/1.78 tff(c_360, plain, (![E_8, T_9]: (selection_favors('#skF_1'(E_8, T_9), first_movers, T_9) | cardinality_at_time(first_movers, T_9)!=zero | ~in_environment(E_8, T_9) | ~greater(number_of_organizations(E_8, T_9), zero) | ~environment(E_8)))).
% 3.98/1.78 tff(c_256, plain, (![E_79, T_22, E_21]: (selection_favors('#skF_1'(E_79, T_22), first_movers, T_22) | cardinality_at_time(first_movers, T_22)!=zero | ~subpopulation('#skF_1'(E_79, T_22), E_21, T_22) | ~greater(number_of_organizations(E_79, T_22), zero) | ~environment(E_79) | ~in_environment(E_21, T_22) | ~environment(E_21)))).
% 3.98/1.78 tff(c_344, plain, (![E_8, T_9]: (selection_favors('#skF_1'(E_8, T_9), efficient_producers, T_9) | cardinality_at_time(efficient_producers, T_9)!=zero | ~in_environment(E_8, T_9) | ~greater(number_of_organizations(E_8, T_9), zero) | ~environment(E_8)))).
% 3.98/1.79 tff(c_257, plain, (![E_79, T_22, E_21]: (selection_favors('#skF_1'(E_79, T_22), efficient_producers, T_22) | cardinality_at_time(efficient_producers, T_22)!=zero | ~subpopulation('#skF_1'(E_79, T_22), E_21, T_22) | ~greater(number_of_organizations(E_79, T_22), zero) | ~environment(E_79) | ~in_environment(E_21, T_22) | ~environment(E_21)))).
% 3.98/1.79 tff(c_320, plain, (![E_8]: (selection_favors(efficient_producers, '#skF_1'(E_8, '#skF_3'), '#skF_3') | cardinality_at_time('#skF_1'(E_8, '#skF_3'), '#skF_3')!=zero | ~subpopulation(efficient_producers, E_8, '#skF_3') | ~greater(number_of_organizations(E_8, '#skF_3'), zero) | ~environment(E_8)))).
% 3.98/1.79 tff(c_327, plain, (cardinality_at_time(first_movers, '#skF_3')!=zero)).
% 3.98/1.79 tff(c_319, plain, (selection_favors(efficient_producers, efficient_producers, '#skF_3'))).
% 3.98/1.79 tff(c_304, plain, (![S2_64, E_66]: (selection_favors(efficient_producers, S2_64, '#skF_3') | cardinality_at_time(S2_64, '#skF_3')!=zero | ~subpopulation(S2_64, E_66, '#skF_3') | ~subpopulation(efficient_producers, E_66, '#skF_3') | ~environment(E_66)))).
% 3.98/1.79 tff(c_285, plain, (![E_8]: (selection_favors('#skF_1'(E_8, '#skF_3'), efficient_producers, '#skF_3') | ~subpopulation('#skF_1'(E_8, '#skF_3'), '#skF_2', '#skF_3') | ~greater(number_of_organizations(E_8, '#skF_3'), zero) | ~environment(E_8)))).
% 3.98/1.79 tff(c_169, plain, (![E_56, T2_59]: (in_environment(E_56, appear(an_organisation, '#skF_2')) | ~greater_or_equal(T2_59, appear(an_organisation, '#skF_2')) | ~in_environment(E_56, T2_59) | ~in_environment(E_56, start_time('#skF_2')) | ~environment(E_56)))).
% 3.98/1.79 tff(c_279, plain, (subpopulation(efficient_producers, '#skF_2', '#skF_3'))).
% 3.98/1.79 tff(c_277, plain, (greater(zero, zero))).
% 3.98/1.79 tff(c_265, plain, ('#skF_1'('#skF_2', '#skF_3')=efficient_producers)).
% 3.98/1.79 tff(c_181, plain, (![E_8, T_9]: ('#skF_1'(E_8, T_9)=first_movers | '#skF_1'(E_8, T_9)=efficient_producers | ~greater(number_of_organizations(E_8, T_9), zero) | ~environment(E_8)))).
% 3.98/1.79 tff(c_101, plain, (![E_8, T_9, S2_64, E_66]: (selection_favors('#skF_1'(E_8, T_9), S2_64, T_9) | cardinality_at_time(S2_64, T_9)!=zero | ~subpopulation(S2_64, E_66, T_9) | ~subpopulation('#skF_1'(E_8, T_9), E_66, T_9) | ~environment(E_66) | ~greater(number_of_organizations(E_8, T_9), zero) | ~environment(E_8)))).
% 3.98/1.79 tff(c_150, plain, (![E_67]: (in_environment(E_67, appear(an_organisation, '#skF_2')) | ~in_environment(E_67, '#skF_3') | ~in_environment(E_67, start_time('#skF_2')) | ~environment(E_67)))).
% 3.98/1.79 tff(c_151, plain, (![E_19]: (in_environment(E_19, '#skF_3') | ~greater_or_equal(start_time(E_19), '#skF_3') | ~in_environment(E_19, appear(an_organisation, '#skF_2')) | ~environment(E_19)))).
% 3.98/1.79 tff(c_171, plain, (![T_7]: (cardinality_at_time(first_movers, T_7)=zero | ~greater(appear(an_organisation, '#skF_2'), T_7) | ~in_environment('#skF_2', T_7)))).
% 3.98/1.79 tff(c_152, plain, (![E_56, T2_59]: (in_environment(E_56, '#skF_3') | ~greater_or_equal(T2_59, '#skF_3') | ~in_environment(E_56, T2_59) | ~in_environment(E_56, appear(an_organisation, '#skF_2')) | ~environment(E_56)))).
% 3.98/1.79 tff(c_175, plain, (greater_or_equal(appear(an_organisation, '#skF_2'), start_time('#skF_2')))).
% 3.98/1.79 tff(c_190, plain, (greater(number_of_organizations('#skF_2', '#skF_3'), zero))).
% 3.98/1.79 tff(c_153, plain, (greater_or_equal('#skF_3', appear(an_organisation, '#skF_2')))).
% 3.98/1.79 tff(c_149, plain, (appear(first_movers, '#skF_2')=appear(an_organisation, '#skF_2'))).
% 3.98/1.79 tff(c_132, plain, (in_environment('#skF_2', appear(an_organisation, '#skF_2')))).
% 3.98/1.79 tff(c_133, plain, (in_environment('#skF_2', start_time('#skF_2')))).
% 3.98/1.79 tff(c_84, plain, (![E_56, E_20, T2_59]: (in_environment(E_56, appear(first_movers, E_20)) | ~greater_or_equal(T2_59, appear(first_movers, E_20)) | ~in_environment(E_56, T2_59) | ~in_environment(E_56, start_time(E_20)) | ~environment(E_56) | ~environment(E_20)))).
% 3.98/1.79 tff(c_2, plain, (![S1_2, S2_3, T_4, E_1]: (selection_favors(S1_2, S2_3, T_4) | cardinality_at_time(S2_3, T_4)!=zero | ~greater(cardinality_at_time(S1_2, T_4), zero) | ~subpopulation(S2_3, E_1, T_4) | ~subpopulation(S1_2, E_1, T_4) | ~environment(E_1)))).
% 3.98/1.79 tff(c_14, plain, (![E_15, T_18, T1_16, T2_17]: (in_environment(E_15, T_18) | ~greater_or_equal(T_18, T1_16) | ~greater_or_equal(T2_17, T_18) | ~in_environment(E_15, T2_17) | ~in_environment(E_15, T1_16) | ~environment(E_15)))).
% 3.98/1.80 tff(c_26, plain, (![E_24, T_25]: (greater(number_of_organizations(E_24, T_25), zero) | ~greater_or_equal(T_25, appear(an_organisation, E_24)) | ~in_environment(E_24, T_25) | ~environment(E_24)))).
% 3.98/1.80 tff(c_54, plain, (![E_44, T_45]: (cardinality_at_time('#skF_1'(E_44, T_45), t)!=zero | ~greater(number_of_organizations(E_44, T_45), zero) | ~environment(E_44)))).
% 3.98/1.80 tff(c_28, plain, (![X_27, T_28, E_26]: (first_movers=X_27 | efficient_producers=X_27 | ~greater(cardinality_at_time(X_27, T_28), zero) | ~subpopulation(X_27, E_26, T_28) | ~environment(E_26)))).
% 3.98/1.80 tff(c_69, plain, (cardinality_at_time(efficient_producers, t)!=zero)).
% 3.98/1.80 tff(c_61, plain, (cardinality_at_time(efficient_producers, '#skF_3')=zero)).
% 4.40/1.80 tff(c_4, plain, (![X_6, T_7, E_5]: (cardinality_at_time(X_6, T_7)=zero | ~greater(appear(X_6, E_5), T_7) | ~in_environment(E_5, T_7) | ~environment(E_5)))).
% 4.40/1.80 tff(c_6, plain, (![E_8, T_9]: (greater(cardinality_at_time('#skF_1'(E_8, T_9), T_9), zero) | ~greater(number_of_organizations(E_8, T_9), zero) | ~environment(E_8)))).
% 4.40/1.80 tff(c_30, plain, (![E_29]: (appear(first_movers, E_29)=appear(an_organisation, E_29) | ~in_environment(E_29, appear(an_organisation, E_29)) | ~environment(E_29)))).
% 4.40/1.80 tff(c_8, plain, (![E_8, T_9]: (subpopulation('#skF_1'(E_8, T_9), E_8, T_9) | ~greater(number_of_organizations(E_8, T_9), zero) | ~environment(E_8)))).
% 4.40/1.80 tff(c_24, plain, (![E_23]: (in_environment(E_23, appear(an_organisation, E_23)) | ~in_environment(E_23, appear(first_movers, E_23)) | ~environment(E_23)))).
% 4.40/1.80 tff(c_12, plain, (![E_13, T_14]: (in_environment(E_13, T_14) | ~greater(number_of_organizations(E_13, T_14), zero) | ~environment(E_13)))).
% 4.40/1.80 tff(c_10, plain, (![X_11, T_12]: (~greater(cardinality_at_time(X_11, T_12), zero) | cardinality_at_time(X_11, t)!=zero))).
% 4.40/1.80 tff(c_22, plain, (![E_21, T_22]: (subpopulation(first_movers, E_21, T_22) | ~in_environment(E_21, T_22) | ~environment(E_21)))).
% 4.40/1.80 tff(c_20, plain, (![E_21, T_22]: (subpopulation(efficient_producers, E_21, T_22) | ~in_environment(E_21, T_22) | ~environment(E_21)))).
% 4.40/1.80 tff(c_18, plain, (![E_20]: (greater_or_equal(appear(first_movers, E_20), start_time(E_20)) | ~environment(E_20)))).
% 4.40/1.80 tff(c_16, plain, (![E_19]: (in_environment(E_19, start_time(E_19)) | ~environment(E_19)))).
% 4.40/1.80 tff(c_34, plain, (greater(appear(efficient_producers, '#skF_2'), '#skF_3'))).
% 4.40/1.80 tff(c_32, plain, (~selection_favors(first_movers, efficient_producers, '#skF_3'))).
% 4.40/1.80 tff(c_38, plain, (in_environment('#skF_2', '#skF_3'))).
% 4.40/1.80 tff(c_40, plain, (environment('#skF_2'))).
% 4.40/1.80 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.40/1.80
%------------------------------------------------------------------------------