%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MGT040-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 : n002.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:58 AM UTC 2026 % Result : Satisfiable 3.28s 1.51s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT040-2 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.05 % 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.10/0.38 % Computer : n002.cluster.edu % 0.10/0.38 % Model : x86_64 x86_64 % 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.38 % Memory : 8046.5625MB % 0.10/0.38 % OS : Linux 6.8.0-71-generic % 0.10/0.38 % CPULimit : 300 % 0.10/0.38 % WCLimit : 300 % 0.10/0.38 % DateTime : Mon Sep 7 13:03:37 UTC 2026 % 0.10/0.38 % CPUTime : % 3.28/1.51 % 3.28/1.51 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.28/1.51 % 3.28/1.51 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.28/1.52 %$ selection_favors > in_environment > greater_or_equal > greater > rapid_change > propagation_strategy > observational_period > extreme > environment > empty > appear > #nlpp > sk1 > end_time > critical_point > sk2 > first_movers > efficient_producers > an_organisation % 3.28/1.52 % 3.28/1.52 %Foreground sorts: % 3.28/1.52 % 3.28/1.52 % 3.28/1.52 %Background operators: % 3.28/1.52 % 3.28/1.52 % 3.28/1.52 %Foreground operators: % 3.28/1.52 tff(greater, type, greater: ($i * $i) > $o). % 3.28/1.52 tff(sk1, type, sk1: $i > $i). % 3.28/1.52 tff(in_environment, type, in_environment: ($i * $i) > $o). % 3.28/1.52 tff(observational_period, type, observational_period: $i > $o). % 3.28/1.52 tff(rapid_change, type, rapid_change: $i > $o). % 3.28/1.52 tff(sk2, type, sk2: $i). % 3.28/1.52 tff(appear, type, appear: ($i * $i) > $i). % 3.28/1.52 tff(efficient_producers, type, efficient_producers: $i). % 3.28/1.52 tff(extreme, type, extreme: $i > $o). % 3.28/1.52 tff(critical_point, type, critical_point: $i > $i). % 3.28/1.52 tff(environment, type, environment: $i > $o). % 3.28/1.52 tff(empty, type, empty: $i > $o). % 3.28/1.52 tff(end_time, type, end_time: $i > $i). % 3.28/1.52 tff(first_movers, type, first_movers: $i). % 3.28/1.52 tff(an_organisation, type, an_organisation: $i). % 3.28/1.52 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o). % 3.28/1.52 tff(selection_favors, type, selection_favors: ($i * $i * $i) > $o). % 3.28/1.52 tff(propagation_strategy, type, propagation_strategy: $i > $o). % 3.28/1.52 % 3.28/1.52 %Saturated clause set: % 3.28/1.52 tff(c_126, plain, (![A_17, B_55, B_18]: (~rapid_change(A_17) | ~observational_period(A_17) | selection_favors(first_movers, efficient_producers, end_time(critical_point(A_17))) | ~greater(critical_point(critical_point(A_17)), B_55) | ~environment(critical_point(A_17)) | greater(appear(efficient_producers, critical_point(A_17)), B_55) | ~in_environment(critical_point(A_17), B_55) | selection_favors(first_movers, efficient_producers, end_time(A_17)) | ~greater(critical_point(A_17), B_18) | ~environment(A_17) | greater(appear(efficient_producers, A_17), B_18) | ~in_environment(A_17, B_18)))). % 3.28/1.52 tff(c_145, plain, (![B_18, A_51]: (selection_favors(first_movers, efficient_producers, B_18) | selection_favors(first_movers, efficient_producers, end_time(A_51)) | ~greater(critical_point(A_51), B_18) | ~environment(A_51) | ~in_environment(A_51, B_18) | greater(appear(efficient_producers, A_51), B_18)))). % 3.28/1.52 tff(c_127, plain, (![A_2, B_55]: (~rapid_change(A_2) | selection_favors(first_movers, efficient_producers, end_time(sk1(A_2))) | ~greater(critical_point(sk1(A_2)), B_55) | ~environment(sk1(A_2)) | greater(appear(efficient_producers, sk1(A_2)), B_55) | ~in_environment(sk1(A_2), B_55) | selection_favors(efficient_producers, first_movers, A_2) | ~observational_period(A_2)))). % 3.28/1.52 tff(c_128, plain, (![A_8, B_55]: (~rapid_change(A_8) | ~observational_period(A_8) | selection_favors(first_movers, efficient_producers, end_time(end_time(A_8))) | ~greater(critical_point(end_time(A_8)), B_55) | ~environment(end_time(A_8)) | greater(appear(efficient_producers, end_time(A_8)), B_55) | ~in_environment(end_time(A_8), B_55) | ~environment(A_8)))). % 3.28/1.52 tff(c_118, plain, (![A_51, B_52]: (~empty(critical_point(A_51)) | ~environment(critical_point(A_51)) | extreme(A_51) | ~observational_period(A_51) | selection_favors(first_movers, efficient_producers, end_time(A_51)) | ~greater(critical_point(A_51), B_52) | ~environment(A_51) | greater(appear(efficient_producers, A_51), B_52) | ~in_environment(A_51, B_52)))). % 3.28/1.52 tff(c_117, plain, (![A_4, A_51, B_52]: (~in_environment(A_4, A_51) | ~rapid_change(A_4) | ~observational_period(A_4) | selection_favors(first_movers, efficient_producers, end_time(A_51)) | ~greater(critical_point(A_51), B_52) | ~environment(A_51) | greater(appear(efficient_producers, A_51), B_52) | ~in_environment(A_51, B_52)))). % 3.28/1.52 tff(c_106, plain, (![A_17, B_18]: (selection_favors(first_movers, efficient_producers, end_time(A_17)) | in_environment(A_17, critical_point(A_17)) | ~greater(critical_point(A_17), B_18) | ~environment(A_17) | greater(appear(efficient_producers, A_17), B_18) | ~in_environment(A_17, B_18)))). % 3.28/1.52 tff(c_83, plain, (![B_18, A_17]: (selection_favors(first_movers, efficient_producers, B_18) | ~greater(critical_point(A_17), B_18) | ~in_environment(A_17, critical_point(A_17)) | ~environment(A_17) | greater(appear(efficient_producers, A_17), B_18) | ~in_environment(A_17, B_18)))). % 3.28/1.52 tff(c_22, plain, (![A_11, B_12]: (selection_favors(first_movers, efficient_producers, end_time(A_11)) | in_environment(A_11, critical_point(A_11)) | ~greater(critical_point(A_11), B_12) | ~greater_or_equal(B_12, appear(efficient_producers, A_11)) | ~environment(A_11)))). % 3.28/1.52 tff(c_30, plain, (![B_20, A_19]: (selection_favors(first_movers, efficient_producers, B_20) | ~greater(appear(efficient_producers, A_19), B_20) | ~greater_or_equal(B_20, appear(first_movers, A_19)) | ~in_environment(A_19, B_20) | ~environment(A_19)))). % 3.28/1.52 tff(c_72, plain, (![A_35, B_34]: (appear(efficient_producers, A_35)=B_34 | greater(B_34, appear(efficient_producers, A_35)) | greater(appear(efficient_producers, A_35), B_34) | ~in_environment(A_35, B_34)))). % 3.28/1.52 tff(c_54, plain, (![A_27]: (appear(an_organisation, A_27)=end_time(A_27) | greater(end_time(A_27), appear(an_organisation, A_27)) | empty(A_27) | ~environment(A_27)))). % 3.28/1.52 tff(c_32, plain, (![B_22, A_21]: (selection_favors(first_movers, efficient_producers, B_22) | ~greater(critical_point(A_21), B_22) | ~greater_or_equal(B_22, appear(efficient_producers, A_21)) | ~in_environment(A_21, critical_point(A_21)) | ~environment(A_21)))). % 3.28/1.52 tff(c_78, plain, (![A_1]: (~empty(sk1(A_1)) | extreme(A_1) | selection_favors(efficient_producers, first_movers, A_1) | ~observational_period(A_1)))). % 3.28/1.52 tff(c_8, plain, (![B_5, A_4]: (~in_environment(B_5, critical_point(B_5)) | ~in_environment(A_4, B_5) | ~environment(B_5) | ~rapid_change(A_4) | ~observational_period(A_4)))). % 3.28/1.52 tff(c_28, plain, (![B_18, A_17]: (greater_or_equal(B_18, appear(efficient_producers, A_17)) | greater(appear(efficient_producers, A_17), B_18) | ~in_environment(A_17, B_18)))). % 3.28/1.52 tff(c_65, plain, (![A_8]: (~empty(end_time(A_8)) | ~environment(end_time(A_8)) | extreme(A_8) | ~observational_period(A_8) | ~environment(A_8)))). % 3.28/1.52 tff(c_42, plain, (![A_3]: (selection_favors(efficient_producers, first_movers, A_3) | ~selection_favors(efficient_producers, first_movers, end_time(sk1(A_3))) | ~observational_period(A_3)))). % 3.28/1.52 tff(c_10, plain, (![B_7, A_6]: (~empty(B_7) | ~in_environment(A_6, B_7) | ~environment(B_7) | extreme(A_6) | ~observational_period(A_6)))). % 3.28/1.52 tff(c_18, plain, (![A_9]: (greater(critical_point(A_9), end_time(A_9)) | in_environment(A_9, critical_point(A_9)) | ~environment(A_9)))). % 3.28/1.52 tff(c_44, plain, (![A_2]: (selection_favors(efficient_producers, first_movers, A_2) | in_environment(A_2, sk1(A_2)) | ~observational_period(A_2)))). % 3.28/1.52 tff(c_20, plain, (![A_10]: (greater_or_equal(end_time(A_10), appear(an_organisation, A_10)) | empty(A_10) | ~environment(A_10)))). % 3.28/1.52 tff(c_46, plain, (![A_1]: (selection_favors(efficient_producers, first_movers, A_1) | environment(sk1(A_1)) | ~observational_period(A_1)))). % 3.28/1.52 tff(c_26, plain, (![B_16, A_15]: (B_16=A_15 | greater(A_15, B_16) | ~greater_or_equal(A_15, B_16)))). % 3.28/1.52 tff(c_16, plain, (![A_8]: (in_environment(A_8, end_time(A_8)) | ~environment(A_8)))). % 3.28/1.52 tff(c_40, plain, (~selection_favors(first_movers, efficient_producers, sk2))). % 3.28/1.52 tff(c_12, plain, (propagation_strategy(first_movers))). % 3.28/1.52 tff(c_14, plain, (propagation_strategy(efficient_producers))). % 3.28/1.52 tff(c_36, plain, (rapid_change(sk2))). % 3.28/1.52 tff(c_34, plain, (observational_period(sk2))). % 3.28/1.52 tff(c_38, plain, (~extreme(sk2))). % 3.28/1.52 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.28/1.52 %------------------------------------------------------------------------------