%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT037+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 : n026.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:57 AM UTC 2026
% Result : CounterSatisfiable 4.28s 2.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT037+2 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.05 % 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.11/0.36 % Computer : n026.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 7 12:47:27 UTC 2026
% 0.11/0.36 % CPUTime :
% 4.28/2.18
% 4.28/2.18 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.28/2.18
% 4.28/2.18 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.28/2.19 %$ subpopulation > in_environment > greater_or_equal > greater > environment > decreases > constant > resources > number_of_organizations > growth_rate > cardinality_at_time > appear > #nlpp > resilience > equilibrium > zero > first_movers > efficient_producers > an_organisation > #skF_3 > #skF_4 > #skF_2 > #skF_1
% 4.28/2.19
% 4.28/2.19 %Foreground sorts:
% 4.28/2.19
% 4.28/2.19
% 4.28/2.19 %Background operators:
% 4.28/2.19
% 4.28/2.19
% 4.28/2.19 %Foreground operators:
% 4.28/2.19 tff(greater, type, greater: ($i * $i) > $o).
% 4.28/2.19 tff(number_of_organizations, type, number_of_organizations: ($i * $i) > $i).
% 4.28/2.19 tff(in_environment, type, in_environment: ($i * $i) > $o).
% 4.28/2.19 tff(constant, type, constant: $i > $o).
% 4.28/2.19 tff(appear, type, appear: ($i * $i) > $i).
% 4.28/2.19 tff(efficient_producers, type, efficient_producers: $i).
% 4.28/2.19 tff(resilience, type, resilience: $i > $i).
% 4.28/2.19 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i).
% 4.28/2.19 tff(growth_rate, type, growth_rate: ($i * $i) > $i).
% 4.28/2.19 tff(decreases, type, decreases: $i > $o).
% 4.28/2.19 tff('#skF_3', type, '#skF_3': $i).
% 4.28/2.19 tff(environment, type, environment: $i > $o).
% 4.28/2.19 tff(first_movers, type, first_movers: $i).
% 4.28/2.19 tff(an_organisation, type, an_organisation: $i).
% 4.28/2.19 tff('#skF_4', type, '#skF_4': $i).
% 4.28/2.19 tff(equilibrium, type, equilibrium: $i > $i).
% 4.28/2.19 tff('#skF_2', type, '#skF_2': ($i * $i) > $i).
% 4.28/2.19 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o).
% 4.28/2.19 tff(resources, type, resources: ($i * $i) > $i).
% 4.28/2.19 tff('#skF_1', type, '#skF_1': ($i * $i) > $i).
% 4.28/2.19 tff(subpopulation, type, subpopulation: ($i * $i * $i) > $o).
% 4.28/2.19 tff(zero, type, zero: $i).
% 4.28/2.19
% 4.28/2.19 %Saturated clause set:
% 4.28/2.19 tff(c_221, plain, (![S1_31, E_117, T_118, E_30]: (~greater(resilience(first_movers), resilience(S1_31)) | greater(zero, growth_rate(S1_31, '#skF_1'(E_117, T_118))) | ~in_environment(E_30, '#skF_1'(E_117, T_118)) | ~environment(E_30) | cardinality_at_time(efficient_producers, T_118)!=zero | ~greater_or_equal(T_118, appear(efficient_producers, E_117)) | ~environment(E_117)))).
% 4.28/2.19 tff(c_229, plain, (cardinality_at_time(first_movers, '#skF_1'('#skF_3', '#skF_4'))!=zero)).
% 4.28/2.19 tff(c_222, plain, (![E_117, T_118]: (cardinality_at_time(first_movers, '#skF_1'(E_117, T_118))!=zero | cardinality_at_time(efficient_producers, T_118)!=zero | ~greater_or_equal(T_118, appear(efficient_producers, E_117)) | ~environment(E_117)))).
% 4.28/2.19 tff(c_214, plain, (![E_1, T_2]: (greater(zero, growth_rate(first_movers, '#skF_1'(E_1, T_2))) | cardinality_at_time(efficient_producers, T_2)!=zero | ~greater_or_equal(T_2, appear(efficient_producers, E_1)) | ~environment(E_1)))).
% 4.28/2.19 tff(c_149, plain, (![S1_85, E_1, T_2, E_86]: (~greater(resilience(efficient_producers), resilience(S1_85)) | greater(zero, growth_rate(S1_85, '#skF_1'(E_1, T_2))) | ~in_environment(E_86, '#skF_1'(E_1, T_2)) | ~environment(E_86) | cardinality_at_time(efficient_producers, T_2)!=zero | ~greater_or_equal(T_2, appear(efficient_producers, E_1)) | ~environment(E_1)))).
% 4.28/2.19 tff(c_205, plain, (![E_106, T_107]: (~constant(number_of_organizations(E_106, T_107)) | '#skF_2'(E_106, T_107)=first_movers | '#skF_2'(E_106, T_107)=efficient_producers | ~in_environment(E_106, T_107) | ~environment(E_106)))).
% 4.28/2.19 tff(c_200, plain, (![E_6, T_7]: ('#skF_2'(E_6, T_7)=first_movers | '#skF_2'(E_6, T_7)=efficient_producers | decreases(number_of_organizations(E_6, T_7)) | ~in_environment(E_6, T_7) | ~environment(E_6)))).
% 4.28/2.19 tff(c_83, plain, (![E_58, T_59]: (greater(cardinality_at_time(efficient_producers, '#skF_1'(E_58, T_59)), zero) | cardinality_at_time(efficient_producers, '#skF_1'(E_58, T_59))=zero | cardinality_at_time(efficient_producers, T_59)!=zero | ~greater_or_equal(T_59, appear(efficient_producers, E_58)) | ~environment(E_58)))).
% 4.28/2.19 tff(c_133, plain, (![E_1, T_2]: (cardinality_at_time(efficient_producers, '#skF_1'(E_1, T_2))=zero | number_of_organizations(E_1, '#skF_1'(E_1, T_2))!=zero | cardinality_at_time(efficient_producers, T_2)!=zero | ~greater_or_equal(T_2, appear(efficient_producers, E_1)) | ~environment(E_1)))).
% 4.28/2.19 tff(c_116, plain, (![E_1, T_2]: (cardinality_at_time(first_movers, '#skF_1'(E_1, T_2))=zero | number_of_organizations(E_1, '#skF_1'(E_1, T_2))!=zero | cardinality_at_time(efficient_producers, T_2)!=zero | ~greater_or_equal(T_2, appear(efficient_producers, E_1)) | ~environment(E_1)))).
% 4.28/2.19 tff(c_187, plain, (![E_93, T_94]: (~constant(number_of_organizations(E_93, T_94)) | number_of_organizations(E_93, T_94)!=zero | ~in_environment(E_93, T_94) | ~environment(E_93)))).
% 4.28/2.19 tff(c_178, plain, (![E_87, T_88]: (number_of_organizations(E_87, T_88)!=zero | ~in_environment(E_87, T_88) | ~environment(E_87) | decreases(number_of_organizations(E_87, T_88))))).
% 4.28/2.19 tff(c_46, plain, (![S2_32, T_33, S1_31, E_30]: (~greater(zero, growth_rate(S2_32, T_33)) | ~greater(resilience(S2_32), resilience(S1_31)) | greater(zero, growth_rate(S1_31, T_33)) | ~in_environment(E_30, T_33) | ~environment(E_30)))).
% 4.28/2.20 tff(c_8, plain, (![E_1, T_2]: (greater('#skF_1'(E_1, T_2), appear(efficient_producers, E_1)) | cardinality_at_time(efficient_producers, T_2)!=zero | ~greater_or_equal(T_2, appear(efficient_producers, E_1)) | ~environment(E_1)))).
% 4.28/2.20 tff(c_36, plain, (![E_23, T_24]: (constant(resources(E_23, T_24)) | greater(equilibrium(E_23), T_24) | ~greater(number_of_organizations(E_23, T_24), zero) | ~in_environment(E_23, T_24) | ~environment(E_23)))).
% 4.28/2.20 tff(c_143, plain, (cardinality_at_time(efficient_producers, '#skF_1'('#skF_3', '#skF_4'))!=zero)).
% 4.28/2.20 tff(c_125, plain, (![E_73, T_74]: (cardinality_at_time(efficient_producers, '#skF_1'(E_73, T_74))!=zero | cardinality_at_time(efficient_producers, T_74)!=zero | ~greater_or_equal(T_74, appear(efficient_producers, E_73)) | ~environment(E_73)))).
% 4.28/2.20 tff(c_107, plain, (![T_13, E_12]: (cardinality_at_time(efficient_producers, T_13)=zero | number_of_organizations(E_12, T_13)!=zero | ~in_environment(E_12, T_13) | ~environment(E_12)))).
% 4.28/2.20 tff(c_2, plain, (![E_1, T_2]: (greater(zero, growth_rate(efficient_producers, '#skF_1'(E_1, T_2))) | cardinality_at_time(efficient_producers, T_2)!=zero | ~greater_or_equal(T_2, appear(efficient_producers, E_1)) | ~environment(E_1)))).
% 4.28/2.20 tff(c_120, plain, (number_of_organizations('#skF_3', '#skF_4')!=zero)).
% 4.59/2.20 tff(c_106, plain, (![T_13, E_12]: (cardinality_at_time(first_movers, T_13)=zero | number_of_organizations(E_12, T_13)!=zero | ~in_environment(E_12, T_13) | ~environment(E_12)))).
% 4.59/2.20 tff(c_38, plain, (![E_23, T_24]: (decreases(resources(E_23, T_24)) | ~greater(equilibrium(E_23), T_24) | ~greater(number_of_organizations(E_23, T_24), zero) | ~in_environment(E_23, T_24) | ~environment(E_23)))).
% 4.59/2.20 tff(c_18, plain, (![X_11, T_10, E_9]: (cardinality_at_time(X_11, T_10)=zero | ~subpopulation(X_11, E_9, T_10) | number_of_organizations(E_9, T_10)!=zero | ~in_environment(E_9, T_10) | ~environment(E_9)))).
% 4.59/2.20 tff(c_94, plain, (greater('#skF_4', '#skF_1'('#skF_3', '#skF_4')))).
% 4.59/2.20 tff(c_4, plain, (![T_2, E_1]: (greater(T_2, '#skF_1'(E_1, T_2)) | cardinality_at_time(efficient_producers, T_2)!=zero | ~greater_or_equal(T_2, appear(efficient_producers, E_1)) | ~environment(E_1)))).
% 4.59/2.20 tff(c_14, plain, (![E_6, T_7]: (greater(cardinality_at_time('#skF_2'(E_6, T_7), T_7), zero) | decreases(number_of_organizations(E_6, T_7)) | ~in_environment(E_6, T_7) | ~environment(E_6)))).
% 4.59/2.20 tff(c_12, plain, (![E_6, T_7]: (~greater(zero, growth_rate('#skF_2'(E_6, T_7), T_7)) | decreases(number_of_organizations(E_6, T_7)) | ~in_environment(E_6, T_7) | ~environment(E_6)))).
% 4.59/2.20 tff(c_6, plain, (![E_1, T_2]: (in_environment(E_1, '#skF_1'(E_1, T_2)) | cardinality_at_time(efficient_producers, T_2)!=zero | ~greater_or_equal(T_2, appear(efficient_producers, E_1)) | ~environment(E_1)))).
% 4.59/2.20 tff(c_30, plain, (![E_19, T_20]: (greater(appear(an_organisation, E_19), T_20) | ~greater_or_equal(T_20, appear(an_organisation, E_19)) | ~in_environment(E_19, T_20) | ~environment(E_19)))).
% 4.59/2.20 tff(c_32, plain, (![E_21, T_22]: (greater(number_of_organizations(E_21, T_22), zero) | ~greater_or_equal(T_22, appear(an_organisation, E_21)) | ~in_environment(E_21, T_22) | ~environment(E_21)))).
% 4.59/2.20 tff(c_16, plain, (![E_6, T_7]: (subpopulation('#skF_2'(E_6, T_7), E_6, T_7) | decreases(number_of_organizations(E_6, T_7)) | ~in_environment(E_6, T_7) | ~environment(E_6)))).
% 4.59/2.20 tff(c_44, plain, (![X_28, T_29, E_27]: (first_movers=X_28 | efficient_producers=X_28 | ~greater(cardinality_at_time(X_28, T_29), zero) | ~subpopulation(X_28, E_27, T_29) | ~environment(E_27)))).
% 4.59/2.20 tff(c_69, plain, (~greater(zero, zero))).
% 4.59/2.20 tff(c_68, plain, (cardinality_at_time(efficient_producers, '#skF_4')=zero)).
% 4.59/2.20 tff(c_26, plain, (![T_17, E_16]: (greater(cardinality_at_time(efficient_producers, T_17), zero) | cardinality_at_time(efficient_producers, T_17)=zero | ~in_environment(E_16, T_17) | ~environment(E_16)))).
% 4.59/2.20 tff(c_10, plain, (![E_4, T_5]: (number_of_organizations(E_4, T_5)=zero | ~greater(appear(an_organisation, E_4), T_5) | ~in_environment(E_4, T_5) | ~environment(E_4)))).
% 4.59/2.20 tff(c_40, plain, (![E_25, T_26]: (constant(number_of_organizations(E_25, T_26)) | ~constant(resources(E_25, T_26)) | ~in_environment(E_25, T_26) | ~environment(E_25)))).
% 4.59/2.20 tff(c_42, plain, (![E_25, T_26]: (~decreases(number_of_organizations(E_25, T_26)) | ~decreases(resources(E_25, T_26)) | ~in_environment(E_25, T_26) | ~environment(E_25)))).
% 4.59/2.20 tff(c_24, plain, (![S_14, T_15]: (~greater(zero, growth_rate(S_14, T_15)) | cardinality_at_time(S_14, T_15)!=zero))).
% 4.59/2.20 tff(c_22, plain, (![E_12, T_13]: (subpopulation(first_movers, E_12, T_13) | ~in_environment(E_12, T_13) | ~environment(E_12)))).
% 4.59/2.20 tff(c_20, plain, (![E_12, T_13]: (subpopulation(efficient_producers, E_12, T_13) | ~in_environment(E_12, T_13) | ~environment(E_12)))).
% 4.59/2.20 tff(c_50, plain, (greater_or_equal('#skF_4', appear(efficient_producers, '#skF_3')))).
% 4.59/2.20 tff(c_34, plain, (greater(resilience(efficient_producers), resilience(first_movers)))).
% 4.59/2.20 tff(c_28, plain, (![X_18]: (~decreases(X_18) | ~constant(X_18)))).
% 4.59/2.20 tff(c_52, plain, (in_environment('#skF_3', '#skF_4'))).
% 4.59/2.20 tff(c_54, plain, (environment('#skF_3'))).
% 4.59/2.20 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.59/2.20
%------------------------------------------------------------------------------