%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MGT033-1 : 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/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 : n011.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:56 AM UTC 2026 % Result : Satisfiable 4.20s 2.60s % 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.4.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.09/0.36 % Computer : n011.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.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Mon Sep 7 12:24:45 UTC 2026 % 0.09/0.37 % CPUTime : % 4.20/2.60 % 4.20/2.60 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.20/2.60 % 4.20/2.60 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.20/2.61 %$ subpopulation > selection_favors > in_environment > greater_or_equal > greater > environment > sk1 > number_of_organizations > cardinality_at_time > appear > #nlpp > start_time > zero > t > sk3 > sk2 > first_movers > efficient_producers > an_organisation % 4.20/2.61 % 4.20/2.61 %Foreground sorts: % 4.20/2.61 % 4.20/2.61 % 4.20/2.61 %Background operators: % 4.20/2.61 % 4.20/2.61 % 4.20/2.61 %Foreground operators: % 4.20/2.61 tff(greater, type, greater: ($i * $i) > $o). % 4.20/2.61 tff(number_of_organizations, type, number_of_organizations: ($i * $i) > $i). % 4.20/2.61 tff(in_environment, type, in_environment: ($i * $i) > $o). % 4.20/2.61 tff(t, type, t: $i). % 4.20/2.61 tff(sk2, type, sk2: $i). % 4.20/2.61 tff(appear, type, appear: ($i * $i) > $i). % 4.20/2.61 tff(efficient_producers, type, efficient_producers: $i). % 4.20/2.61 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i). % 4.20/2.61 tff(environment, type, environment: $i > $o). % 4.20/2.61 tff(start_time, type, start_time: $i > $i). % 4.20/2.61 tff(first_movers, type, first_movers: $i). % 4.20/2.61 tff(sk3, type, sk3: $i). % 4.20/2.61 tff(an_organisation, type, an_organisation: $i). % 4.20/2.61 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o). % 4.20/2.61 tff(subpopulation, type, subpopulation: ($i * $i * $i) > $o). % 4.20/2.61 tff(selection_favors, type, selection_favors: ($i * $i * $i) > $o). % 4.20/2.61 tff(sk1, type, sk1: ($i * $i) > $i). % 4.20/2.61 tff(zero, type, zero: $i). % 4.20/2.61 % 4.20/2.61 %Saturated clause set: % 4.20/2.62 tff(c_241, plain, (![B_9, A_80, A_8]: (selection_favors(sk1(B_9, A_80), sk1(B_9, A_8), B_9) | cardinality_at_time(sk1(B_9, A_8), B_9)!=zero | ~subpopulation(sk1(B_9, A_80), A_8, B_9) | ~greater(number_of_organizations(A_80, B_9), zero) | ~environment(A_80) | ~greater(number_of_organizations(A_8, B_9), zero) | ~environment(A_8)))). % 4.20/2.62 tff(c_358, plain, (![B_9, A_8]: (selection_favors(sk1(B_9, A_8), first_movers, B_9) | cardinality_at_time(first_movers, B_9)!=zero | ~in_environment(A_8, B_9) | ~greater(number_of_organizations(A_8, B_9), zero) | ~environment(A_8)))). % 4.20/2.62 tff(c_243, plain, (![B_23, A_80, A_22]: (selection_favors(sk1(B_23, A_80), first_movers, B_23) | cardinality_at_time(first_movers, B_23)!=zero | ~subpopulation(sk1(B_23, A_80), A_22, B_23) | ~greater(number_of_organizations(A_80, B_23), zero) | ~environment(A_80) | ~in_environment(A_22, B_23) | ~environment(A_22)))). % 4.20/2.62 tff(c_342, plain, (![B_9, A_8]: (selection_favors(sk1(B_9, A_8), efficient_producers, B_9) | cardinality_at_time(efficient_producers, B_9)!=zero | ~in_environment(A_8, B_9) | ~greater(number_of_organizations(A_8, B_9), zero) | ~environment(A_8)))). % 4.20/2.62 tff(c_242, plain, (![B_25, A_80, A_24]: (selection_favors(sk1(B_25, A_80), efficient_producers, B_25) | cardinality_at_time(efficient_producers, B_25)!=zero | ~subpopulation(sk1(B_25, A_80), A_24, B_25) | ~greater(number_of_organizations(A_80, B_25), zero) | ~environment(A_80) | ~in_environment(A_24, B_25) | ~environment(A_24)))). % 4.20/2.62 tff(c_320, plain, (![A_8]: (selection_favors(efficient_producers, sk1(sk3, A_8), sk3) | cardinality_at_time(sk1(sk3, A_8), sk3)!=zero | ~subpopulation(efficient_producers, A_8, sk3) | ~greater(number_of_organizations(A_8, sk3), zero) | ~environment(A_8)))). % 4.20/2.62 tff(c_326, plain, (cardinality_at_time(first_movers, sk3)!=zero)). % 4.20/2.62 tff(c_304, plain, (![D_67, A_69]: (selection_favors(efficient_producers, D_67, sk3) | cardinality_at_time(D_67, sk3)!=zero | ~subpopulation(D_67, A_69, sk3) | ~subpopulation(efficient_producers, A_69, sk3) | ~environment(A_69)))). % 4.20/2.62 tff(c_299, plain, (selection_favors(efficient_producers, efficient_producers, sk3))). % 4.20/2.62 tff(c_240, plain, (![A_80]: (selection_favors(sk1(sk3, A_80), efficient_producers, sk3) | ~subpopulation(sk1(sk3, A_80), sk2, sk3) | ~greater(number_of_organizations(A_80, sk3), zero) | ~environment(A_80)))). % 4.20/2.62 tff(c_169, plain, (![A_59, C_62]: (in_environment(A_59, appear(an_organisation, sk2)) | ~greater_or_equal(C_62, appear(an_organisation, sk2)) | ~in_environment(A_59, C_62) | ~in_environment(A_59, start_time(sk2)) | ~environment(A_59)))). % 4.20/2.62 tff(c_187, plain, (![A_16, C_18]: (in_environment(A_16, sk3) | ~greater_or_equal(C_18, sk3) | ~in_environment(A_16, C_18) | ~in_environment(A_16, appear(an_organisation, sk2)) | ~environment(A_16)))). % 4.20/2.63 tff(c_151, plain, (![A_20]: (in_environment(A_20, sk3) | ~greater_or_equal(start_time(A_20), sk3) | ~in_environment(A_20, appear(an_organisation, sk2)) | ~environment(A_20)))). % 4.20/2.63 tff(c_150, plain, (![A_70]: (in_environment(A_70, appear(an_organisation, sk2)) | ~in_environment(A_70, sk3) | ~in_environment(A_70, start_time(sk2)) | ~environment(A_70)))). % 4.20/2.63 tff(c_171, plain, (![B_6]: (cardinality_at_time(first_movers, B_6)=zero | ~greater(appear(an_organisation, sk2), B_6) | ~in_environment(sk2, B_6)))). % 4.20/2.63 tff(c_101, plain, (![B_11, A_10, D_67, A_69]: (selection_favors(sk1(B_11, A_10), D_67, B_11) | cardinality_at_time(D_67, B_11)!=zero | ~subpopulation(D_67, A_69, B_11) | ~subpopulation(sk1(B_11, A_10), A_69, B_11) | ~environment(A_69) | ~greater(number_of_organizations(A_10, B_11), zero) | ~environment(A_10)))). % 4.20/2.63 tff(c_227, plain, (subpopulation(efficient_producers, sk2, sk3))). % 4.20/2.63 tff(c_225, plain, (greater(zero, zero))). % 4.20/2.63 tff(c_213, plain, (sk1(sk3, sk2)=efficient_producers)). % 4.20/2.63 tff(c_181, plain, (![B_9, A_8]: (sk1(B_9, A_8)=first_movers | sk1(B_9, A_8)=efficient_producers | ~greater(number_of_organizations(A_8, B_9), zero) | ~environment(A_8)))). % 4.20/2.63 tff(c_175, plain, (greater_or_equal(appear(an_organisation, sk2), start_time(sk2)))). % 4.20/2.63 tff(c_190, plain, (greater(number_of_organizations(sk2, sk3), zero))). % 4.20/2.63 tff(c_153, plain, (greater_or_equal(sk3, appear(an_organisation, sk2)))). % 4.20/2.63 tff(c_149, plain, (appear(first_movers, sk2)=appear(an_organisation, sk2))). % 4.20/2.63 tff(c_132, plain, (in_environment(sk2, appear(an_organisation, sk2)))). % 4.20/2.63 tff(c_133, plain, (in_environment(sk2, start_time(sk2)))). % 4.20/2.63 tff(c_84, plain, (![A_59, A_21, C_62]: (in_environment(A_59, appear(first_movers, A_21)) | ~greater_or_equal(C_62, appear(first_movers, A_21)) | ~in_environment(A_59, C_62) | ~in_environment(A_59, start_time(A_21)) | ~environment(A_59) | ~environment(A_21)))). % 4.20/2.63 tff(c_2, plain, (![B_2, D_4, C_3, A_1]: (selection_favors(B_2, D_4, C_3) | cardinality_at_time(D_4, C_3)!=zero | ~greater(cardinality_at_time(B_2, C_3), zero) | ~subpopulation(D_4, A_1, C_3) | ~subpopulation(B_2, A_1, C_3) | ~environment(A_1)))). % 4.20/2.63 tff(c_14, plain, (![A_16, D_19, B_17, C_18]: (in_environment(A_16, D_19) | ~greater_or_equal(D_19, B_17) | ~greater_or_equal(C_18, D_19) | ~in_environment(A_16, C_18) | ~in_environment(A_16, B_17) | ~environment(A_16)))). % 4.20/2.63 tff(c_26, plain, (![A_27, B_28]: (greater(number_of_organizations(A_27, B_28), zero) | ~greater_or_equal(B_28, appear(an_organisation, A_27)) | ~in_environment(A_27, B_28) | ~environment(A_27)))). % 4.20/2.63 tff(c_61, plain, (![B_50, A_51]: (cardinality_at_time(sk1(B_50, A_51), t)!=zero | ~greater(number_of_organizations(A_51, B_50), zero) | ~environment(A_51)))). % 4.20/2.63 tff(c_28, plain, (![B_30, C_31, A_29]: (first_movers=B_30 | efficient_producers=B_30 | ~greater(cardinality_at_time(B_30, C_31), zero) | ~subpopulation(B_30, A_29, C_31) | ~environment(A_29)))). % 4.20/2.63 tff(c_69, plain, (cardinality_at_time(efficient_producers, t)!=zero)). % 4.20/2.63 tff(c_56, plain, (cardinality_at_time(efficient_producers, sk3)=zero)). % 4.20/2.63 tff(c_8, plain, (![B_11, A_10]: (greater(cardinality_at_time(sk1(B_11, A_10), B_11), zero) | ~greater(number_of_organizations(A_10, B_11), zero) | ~environment(A_10)))). % 4.20/2.63 tff(c_4, plain, (![C_7, B_6, A_5]: (cardinality_at_time(C_7, B_6)=zero | ~greater(appear(C_7, A_5), B_6) | ~in_environment(A_5, B_6) | ~environment(A_5)))). % 4.20/2.63 tff(c_30, plain, (![A_32]: (appear(first_movers, A_32)=appear(an_organisation, A_32) | ~in_environment(A_32, appear(an_organisation, A_32)) | ~environment(A_32)))). % 4.20/2.63 tff(c_6, plain, (![B_9, A_8]: (subpopulation(sk1(B_9, A_8), A_8, B_9) | ~greater(number_of_organizations(A_8, B_9), zero) | ~environment(A_8)))). % 4.20/2.63 tff(c_24, plain, (![A_26]: (in_environment(A_26, appear(an_organisation, A_26)) | ~in_environment(A_26, appear(first_movers, A_26)) | ~environment(A_26)))). % 4.20/2.63 tff(c_12, plain, (![A_14, B_15]: (in_environment(A_14, B_15) | ~greater(number_of_organizations(A_14, B_15), zero) | ~environment(A_14)))). % 4.20/2.63 tff(c_10, plain, (![A_12, B_13]: (~greater(cardinality_at_time(A_12, B_13), zero) | cardinality_at_time(A_12, t)!=zero))). % 4.20/2.64 tff(c_22, plain, (![A_24, B_25]: (subpopulation(efficient_producers, A_24, B_25) | ~in_environment(A_24, B_25) | ~environment(A_24)))). % 4.20/2.64 tff(c_20, plain, (![A_22, B_23]: (subpopulation(first_movers, A_22, B_23) | ~in_environment(A_22, B_23) | ~environment(A_22)))). % 4.20/2.64 tff(c_18, plain, (![A_21]: (greater_or_equal(appear(first_movers, A_21), start_time(A_21)) | ~environment(A_21)))). % 4.20/2.64 tff(c_16, plain, (![A_20]: (in_environment(A_20, start_time(A_20)) | ~environment(A_20)))). % 4.20/2.64 tff(c_38, plain, (greater(appear(efficient_producers, sk2), sk3))). % 4.20/2.64 tff(c_40, plain, (~selection_favors(first_movers, efficient_producers, sk3))). % 4.20/2.64 tff(c_34, plain, (in_environment(sk2, sk3))). % 4.20/2.64 tff(c_32, plain, (environment(sk2))). % 4.20/2.64 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.20/2.64 %------------------------------------------------------------------------------