%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MGT019-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/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:52 AM UTC 2026 % Result : Satisfiable 3.07s 2.19s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT019-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/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.35 % Computer : n011.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 11:59:30 UTC 2026 % 0.09/0.36 % CPUTime : % 3.07/2.18 % 3.07/2.19 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.07/2.19 % 3.07/2.19 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.21/2.20 %$ subpopulations > in_environment > greater_or_equal > greater > stable > environment > growth_rate > founding_rate > disbanding_rate > #nlpp > sk5 > sk3 > sk4 > sk2 > sk1 > first_movers > efficient_producers % 3.21/2.20 % 3.21/2.20 %Foreground sorts: % 3.21/2.20 % 3.21/2.20 % 3.21/2.20 %Background operators: % 3.21/2.20 % 3.21/2.20 % 3.21/2.20 %Foreground operators: % 3.21/2.20 tff(subpopulations, type, subpopulations: ($i * $i * $i * $i) > $o). % 3.21/2.20 tff(greater, type, greater: ($i * $i) > $o). % 3.21/2.20 tff(in_environment, type, in_environment: ($i * $i) > $o). % 3.21/2.20 tff(founding_rate, type, founding_rate: ($i * $i) > $i). % 3.21/2.20 tff(sk2, type, sk2: $i). % 3.21/2.20 tff(sk1, type, sk1: $i). % 3.21/2.20 tff(efficient_producers, type, efficient_producers: $i). % 3.21/2.20 tff(disbanding_rate, type, disbanding_rate: ($i * $i) > $i). % 3.21/2.20 tff(growth_rate, type, growth_rate: ($i * $i) > $i). % 3.21/2.20 tff(sk5, type, sk5: $i > $i). % 3.21/2.20 tff(environment, type, environment: $i > $o). % 3.21/2.20 tff(sk4, type, sk4: $i). % 3.21/2.20 tff(first_movers, type, first_movers: $i). % 3.21/2.20 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o). % 3.21/2.20 tff(sk3, type, sk3: $i > $i). % 3.21/2.20 tff(stable, type, stable: $i > $o). % 3.21/2.20 % 3.21/2.20 %Saturated clause set: % 3.21/2.20 tff(c_55, plain, (![A_22]: (~greater(disbanding_rate(first_movers, sk5(sk3(A_22))), disbanding_rate(efficient_producers, sk5(sk3(A_22)))) | ~subpopulations(first_movers, efficient_producers, A_22, sk5(sk3(A_22))) | ~stable(A_22) | ~environment(A_22) | ~in_environment(sk4, sk3(A_22))))). % 3.21/2.20 tff(c_49, plain, (![A_20]: (founding_rate(first_movers, sk5(sk3(A_20)))=founding_rate(efficient_producers, sk5(sk3(A_20))) | greater(founding_rate(efficient_producers, sk5(sk3(A_20))), founding_rate(first_movers, sk5(sk3(A_20)))) | ~subpopulations(first_movers, efficient_producers, A_20, sk5(sk3(A_20))) | ~stable(A_20) | ~environment(A_20) | ~in_environment(sk4, sk3(A_20))))). % 3.21/2.20 tff(c_39, plain, (![A_18]: (greater_or_equal(founding_rate(efficient_producers, sk5(sk3(A_18))), founding_rate(first_movers, sk5(sk3(A_18)))) | ~subpopulations(first_movers, efficient_producers, A_18, sk5(sk3(A_18))) | ~stable(A_18) | ~environment(A_18) | ~in_environment(sk4, sk3(A_18))))). % 3.21/2.20 tff(c_8, plain, (![A_1]: (greater(growth_rate(efficient_producers, A_1), growth_rate(first_movers, A_1)) | ~greater_or_equal(founding_rate(efficient_producers, A_1), founding_rate(first_movers, A_1)) | ~greater(disbanding_rate(first_movers, A_1), disbanding_rate(efficient_producers, A_1))))). % 3.21/2.20 tff(c_14, plain, (![B_6, A_5]: (greater_or_equal(founding_rate(efficient_producers, B_6), founding_rate(first_movers, B_6)) | ~greater_or_equal(B_6, sk3(A_5)) | ~subpopulations(first_movers, efficient_producers, A_5, B_6) | ~stable(A_5) | ~environment(A_5)))). % 3.21/2.20 tff(c_31, plain, (![A_8]: (sk5(A_8)=A_8 | greater(sk5(A_8), A_8) | ~in_environment(sk4, A_8)))). % 3.21/2.21 tff(c_24, plain, (![A_9]: (~greater(growth_rate(efficient_producers, sk5(A_9)), growth_rate(first_movers, sk5(A_9))) | ~in_environment(sk4, A_9)))). % 3.21/2.21 tff(c_20, plain, (![A_7]: (subpopulations(first_movers, efficient_producers, sk4, sk5(A_7)) | ~in_environment(sk4, A_7)))). % 3.21/2.21 tff(c_10, plain, (![B_3, A_2]: (B_3=A_2 | greater(A_2, B_3) | ~greater_or_equal(A_2, B_3)))). % 3.21/2.21 tff(c_12, plain, (![A_4]: (in_environment(A_4, sk3(A_4)) | ~stable(A_4) | ~environment(A_4)))). % 3.21/2.21 tff(c_22, plain, (![A_8]: (greater_or_equal(sk5(A_8), A_8) | ~in_environment(sk4, A_8)))). % 3.21/2.21 tff(c_6, plain, (~greater(disbanding_rate(first_movers, sk2), disbanding_rate(efficient_producers, sk2)))). % 3.21/2.21 tff(c_4, plain, (subpopulations(first_movers, efficient_producers, sk1, sk2))). % 3.21/2.21 tff(c_2, plain, (environment(sk1))). % 3.21/2.21 tff(c_16, plain, (environment(sk4))). % 3.21/2.21 tff(c_18, plain, (stable(sk4))). % 3.21/2.21 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.21/2.21 %------------------------------------------------------------------------------