%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MGT037-2 : TPTP v9.3.0. Released v2.4.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 : n029.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 : Satisfiable 4.72s 2.72s % 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.4.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.11/0.38 % Computer : n029.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Mon Sep 7 12:47:11 UTC 2026 % 0.11/0.38 % CPUTime : % 4.72/2.72 % 4.72/2.72 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.72/2.72 % 4.72/2.72 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.72/2.73 %$ subpopulation > in_environment > greater_or_equal > greater > environment > decreases > constant > sk2 > sk1 > resources > number_of_organizations > growth_rate > cardinality_at_time > appear > #nlpp > resilience > equilibrium > zero > sk4 > sk3 > first_movers > efficient_producers > an_organisation % 4.72/2.73 % 4.72/2.73 %Foreground sorts: % 4.72/2.73 % 4.72/2.73 % 4.72/2.73 %Background operators: % 4.72/2.73 % 4.72/2.73 % 4.72/2.73 %Foreground operators: % 4.72/2.73 tff(greater, type, greater: ($i * $i) > $o). % 4.72/2.73 tff(sk2, type, sk2: ($i * $i) > $i). % 4.72/2.73 tff(number_of_organizations, type, number_of_organizations: ($i * $i) > $i). % 4.72/2.73 tff(in_environment, type, in_environment: ($i * $i) > $o). % 4.72/2.73 tff(constant, type, constant: $i > $o). % 4.72/2.73 tff(appear, type, appear: ($i * $i) > $i). % 4.72/2.73 tff(efficient_producers, type, efficient_producers: $i). % 4.72/2.73 tff(resilience, type, resilience: $i > $i). % 4.72/2.73 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i). % 4.72/2.73 tff(growth_rate, type, growth_rate: ($i * $i) > $i). % 4.72/2.73 tff(decreases, type, decreases: $i > $o). % 4.72/2.73 tff(environment, type, environment: $i > $o). % 4.72/2.73 tff(sk4, type, sk4: $i). % 4.72/2.73 tff(first_movers, type, first_movers: $i). % 4.72/2.73 tff(sk3, type, sk3: $i). % 4.72/2.73 tff(an_organisation, type, an_organisation: $i). % 4.72/2.73 tff(equilibrium, type, equilibrium: $i > $i). % 4.72/2.73 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o). % 4.72/2.73 tff(resources, type, resources: ($i * $i) > $i). % 4.72/2.73 tff(subpopulation, type, subpopulation: ($i * $i * $i) > $o). % 4.72/2.73 tff(sk1, type, sk1: ($i * $i) > $i). % 4.72/2.73 tff(zero, type, zero: $i). % 4.72/2.73 % 4.72/2.73 %Saturated clause set: % 4.72/2.74 tff(c_221, plain, (![C_46, B_131, A_132, A_44]: (~greater(resilience(first_movers), resilience(C_46)) | greater(zero, growth_rate(C_46, sk1(B_131, A_132))) | ~in_environment(A_44, sk1(B_131, A_132)) | ~environment(A_44) | cardinality_at_time(efficient_producers, B_131)!=zero | ~greater_or_equal(B_131, appear(efficient_producers, A_132)) | ~environment(A_132)))). % 4.72/2.74 tff(c_229, plain, (cardinality_at_time(first_movers, sk1(sk4, sk3))!=zero)). % 4.72/2.74 tff(c_222, plain, (![B_131, A_132]: (cardinality_at_time(first_movers, sk1(B_131, A_132))!=zero | cardinality_at_time(efficient_producers, B_131)!=zero | ~greater_or_equal(B_131, appear(efficient_producers, A_132)) | ~environment(A_132)))). % 4.72/2.74 tff(c_214, plain, (![B_4, A_3]: (greater(zero, growth_rate(first_movers, sk1(B_4, A_3))) | cardinality_at_time(efficient_producers, B_4)!=zero | ~greater_or_equal(B_4, appear(efficient_producers, A_3)) | ~environment(A_3)))). % 4.72/2.74 tff(c_149, plain, (![C_99, B_8, A_7, A_100]: (~greater(resilience(efficient_producers), resilience(C_99)) | greater(zero, growth_rate(C_99, sk1(B_8, A_7))) | ~in_environment(A_100, sk1(B_8, A_7)) | ~environment(A_100) | cardinality_at_time(efficient_producers, B_8)!=zero | ~greater_or_equal(B_8, appear(efficient_producers, A_7)) | ~environment(A_7)))). % 4.72/2.74 tff(c_205, plain, (![A_121, B_120]: (~constant(number_of_organizations(A_121, B_120)) | sk2(B_120, A_121)=first_movers | sk2(B_120, A_121)=efficient_producers | ~in_environment(A_121, B_120) | ~environment(A_121)))). % 4.72/2.74 tff(c_200, plain, (![B_12, A_11]: (sk2(B_12, A_11)=first_movers | sk2(B_12, A_11)=efficient_producers | decreases(number_of_organizations(A_11, B_12)) | ~in_environment(A_11, B_12) | ~environment(A_11)))). % 4.72/2.74 tff(c_94, plain, (![B_79, A_78]: (greater(cardinality_at_time(efficient_producers, sk1(B_79, A_78)), zero) | cardinality_at_time(efficient_producers, sk1(B_79, A_78))=zero | cardinality_at_time(efficient_producers, B_79)!=zero | ~greater_or_equal(B_79, appear(efficient_producers, A_78)) | ~environment(A_78)))). % 4.72/2.74 tff(c_116, plain, (![B_4, A_3]: (cardinality_at_time(efficient_producers, sk1(B_4, A_3))=zero | number_of_organizations(A_3, sk1(B_4, A_3))!=zero | cardinality_at_time(efficient_producers, B_4)!=zero | ~greater_or_equal(B_4, appear(efficient_producers, A_3)) | ~environment(A_3)))). % 4.72/2.74 tff(c_188, plain, (![A_109, B_110]: (~constant(number_of_organizations(A_109, B_110)) | number_of_organizations(A_109, B_110)!=zero | ~in_environment(A_109, B_110) | ~environment(A_109)))). % 4.72/2.74 tff(c_178, plain, (![A_102, B_101]: (number_of_organizations(A_102, B_101)!=zero | ~in_environment(A_102, B_101) | ~environment(A_102) | decreases(number_of_organizations(A_102, B_101))))). % 4.72/2.74 tff(c_127, plain, (![B_4, A_3]: (cardinality_at_time(first_movers, sk1(B_4, A_3))=zero | number_of_organizations(A_3, sk1(B_4, A_3))!=zero | cardinality_at_time(efficient_producers, B_4)!=zero | ~greater_or_equal(B_4, appear(efficient_producers, A_3)) | ~environment(A_3)))). % 4.72/2.74 tff(c_46, plain, (![D_47, B_45, C_46, A_44]: (~greater(zero, growth_rate(D_47, B_45)) | ~greater(resilience(D_47), resilience(C_46)) | greater(zero, growth_rate(C_46, B_45)) | ~in_environment(A_44, B_45) | ~environment(A_44)))). % 4.72/2.74 tff(c_145, plain, (cardinality_at_time(efficient_producers, sk1(sk4, sk3))!=zero)). % 4.72/2.74 tff(c_138, plain, (![B_93, A_94]: (cardinality_at_time(efficient_producers, sk1(B_93, A_94))!=zero | cardinality_at_time(efficient_producers, B_93)!=zero | ~greater_or_equal(B_93, appear(efficient_producers, A_94)) | ~environment(A_94)))). % 4.72/2.74 tff(c_8, plain, (![B_8, A_7]: (greater(zero, growth_rate(efficient_producers, sk1(B_8, A_7))) | cardinality_at_time(efficient_producers, B_8)!=zero | ~greater_or_equal(B_8, appear(efficient_producers, A_7)) | ~environment(A_7)))). % 4.72/2.74 tff(c_2, plain, (![B_2, A_1]: (greater(sk1(B_2, A_1), appear(efficient_producers, A_1)) | cardinality_at_time(efficient_producers, B_2)!=zero | ~greater_or_equal(B_2, appear(efficient_producers, A_1)) | ~environment(A_1)))). % 4.72/2.74 tff(c_131, plain, (number_of_organizations(sk3, sk4)!=zero)). % 4.72/2.74 tff(c_36, plain, (![A_33, B_34]: (decreases(resources(A_33, B_34)) | ~greater(equilibrium(A_33), B_34) | ~greater(number_of_organizations(A_33, B_34), zero) | ~in_environment(A_33, B_34) | ~environment(A_33)))). % 4.72/2.74 tff(c_107, plain, (![B_21, A_20]: (cardinality_at_time(first_movers, B_21)=zero | number_of_organizations(A_20, B_21)!=zero | ~in_environment(A_20, B_21) | ~environment(A_20)))). % 4.72/2.75 tff(c_106, plain, (![B_23, A_22]: (cardinality_at_time(efficient_producers, B_23)=zero | number_of_organizations(A_22, B_23)!=zero | ~in_environment(A_22, B_23) | ~environment(A_22)))). % 4.72/2.75 tff(c_38, plain, (![A_35, B_36]: (constant(resources(A_35, B_36)) | greater(equilibrium(A_35), B_36) | ~greater(number_of_organizations(A_35, B_36), zero) | ~in_environment(A_35, B_36) | ~environment(A_35)))). % 4.72/2.75 tff(c_18, plain, (![C_19, B_18, A_17]: (cardinality_at_time(C_19, B_18)=zero | ~subpopulation(C_19, A_17, B_18) | number_of_organizations(A_17, B_18)!=zero | ~in_environment(A_17, B_18) | ~environment(A_17)))). % 4.72/2.75 tff(c_4, plain, (![A_3, B_4]: (in_environment(A_3, sk1(B_4, A_3)) | cardinality_at_time(efficient_producers, B_4)!=zero | ~greater_or_equal(B_4, appear(efficient_producers, A_3)) | ~environment(A_3)))). % 4.72/2.75 tff(c_14, plain, (![B_14, A_13]: (greater(cardinality_at_time(sk2(B_14, A_13), B_14), zero) | decreases(number_of_organizations(A_13, B_14)) | ~in_environment(A_13, B_14) | ~environment(A_13)))). % 4.72/2.75 tff(c_86, plain, (greater(sk4, sk1(sk4, sk3)))). % 4.72/2.75 tff(c_6, plain, (![B_6, A_5]: (greater(B_6, sk1(B_6, A_5)) | cardinality_at_time(efficient_producers, B_6)!=zero | ~greater_or_equal(B_6, appear(efficient_producers, A_5)) | ~environment(A_5)))). % 4.72/2.75 tff(c_16, plain, (![B_16, A_15]: (~greater(zero, growth_rate(sk2(B_16, A_15), B_16)) | decreases(number_of_organizations(A_15, B_16)) | ~in_environment(A_15, B_16) | ~environment(A_15)))). % 4.72/2.75 tff(c_30, plain, (![A_29, B_30]: (greater(appear(an_organisation, A_29), B_30) | ~greater_or_equal(B_30, appear(an_organisation, A_29)) | ~in_environment(A_29, B_30) | ~environment(A_29)))). % 4.72/2.75 tff(c_32, plain, (![A_31, B_32]: (greater(number_of_organizations(A_31, B_32), zero) | ~greater_or_equal(B_32, appear(an_organisation, A_31)) | ~in_environment(A_31, B_32) | ~environment(A_31)))). % 4.72/2.75 tff(c_12, plain, (![B_12, A_11]: (subpopulation(sk2(B_12, A_11), A_11, B_12) | decreases(number_of_organizations(A_11, B_12)) | ~in_environment(A_11, B_12) | ~environment(A_11)))). % 4.72/2.75 tff(c_44, plain, (![B_42, C_43, A_41]: (first_movers=B_42 | efficient_producers=B_42 | ~greater(cardinality_at_time(B_42, C_43), zero) | ~subpopulation(B_42, A_41, C_43) | ~environment(A_41)))). % 4.72/2.75 tff(c_69, plain, (~greater(zero, zero))). % 4.72/2.75 tff(c_68, plain, (cardinality_at_time(efficient_producers, sk4)=zero)). % 4.72/2.75 tff(c_26, plain, (![B_27, A_26]: (greater(cardinality_at_time(efficient_producers, B_27), zero) | cardinality_at_time(efficient_producers, B_27)=zero | ~in_environment(A_26, B_27) | ~environment(A_26)))). % 4.72/2.75 tff(c_10, plain, (![A_9, B_10]: (number_of_organizations(A_9, B_10)=zero | ~greater(appear(an_organisation, A_9), B_10) | ~in_environment(A_9, B_10) | ~environment(A_9)))). % 4.72/2.75 tff(c_40, plain, (![A_37, B_38]: (~decreases(number_of_organizations(A_37, B_38)) | ~decreases(resources(A_37, B_38)) | ~in_environment(A_37, B_38) | ~environment(A_37)))). % 4.72/2.75 tff(c_42, plain, (![A_39, B_40]: (constant(number_of_organizations(A_39, B_40)) | ~constant(resources(A_39, B_40)) | ~in_environment(A_39, B_40) | ~environment(A_39)))). % 4.72/2.75 tff(c_24, plain, (![A_24, B_25]: (~greater(zero, growth_rate(A_24, B_25)) | cardinality_at_time(A_24, B_25)!=zero))). % 4.72/2.75 tff(c_22, plain, (![A_22, B_23]: (subpopulation(efficient_producers, A_22, B_23) | ~in_environment(A_22, B_23) | ~environment(A_22)))). % 4.72/2.75 tff(c_20, plain, (![A_20, B_21]: (subpopulation(first_movers, A_20, B_21) | ~in_environment(A_20, B_21) | ~environment(A_20)))). % 4.72/2.75 tff(c_34, plain, (greater(resilience(efficient_producers), resilience(first_movers)))). % 4.72/2.75 tff(c_52, plain, (greater_or_equal(sk4, appear(efficient_producers, sk3)))). % 4.72/2.75 tff(c_28, plain, (![A_28]: (~decreases(A_28) | ~constant(A_28)))). % 4.72/2.75 tff(c_50, plain, (in_environment(sk3, sk4))). % 4.72/2.75 tff(c_48, plain, (environment(sk3))). % 4.72/2.75 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.72/2.75 %------------------------------------------------------------------------------