%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MGT040-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 : n015.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 4.76s 2.75s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT040-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 : n015.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 13:02:00 UTC 2026 % 0.09/0.37 % CPUTime : % 4.76/2.75 % 4.76/2.75 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.76/2.75 % 4.76/2.75 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.76/2.76 %$ 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 % 4.76/2.76 % 4.76/2.76 %Foreground sorts: % 4.76/2.76 % 4.76/2.76 % 4.76/2.76 %Background operators: % 4.76/2.76 % 4.76/2.76 % 4.76/2.76 %Foreground operators: % 4.76/2.76 tff(greater, type, greater: ($i * $i) > $o). % 4.76/2.76 tff(sk1, type, sk1: $i > $i). % 4.76/2.76 tff(in_environment, type, in_environment: ($i * $i) > $o). % 4.76/2.76 tff(observational_period, type, observational_period: $i > $o). % 4.76/2.76 tff(rapid_change, type, rapid_change: $i > $o). % 4.76/2.76 tff(sk2, type, sk2: $i). % 4.76/2.76 tff(appear, type, appear: ($i * $i) > $i). % 4.76/2.76 tff(efficient_producers, type, efficient_producers: $i). % 4.76/2.76 tff(extreme, type, extreme: $i > $o). % 4.76/2.76 tff(critical_point, type, critical_point: $i > $i). % 4.76/2.76 tff(environment, type, environment: $i > $o). % 4.76/2.76 tff(empty, type, empty: $i > $o). % 4.76/2.76 tff(end_time, type, end_time: $i > $i). % 4.76/2.76 tff(first_movers, type, first_movers: $i). % 4.76/2.76 tff(an_organisation, type, an_organisation: $i). % 4.76/2.76 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o). % 4.76/2.76 tff(selection_favors, type, selection_favors: ($i * $i * $i) > $o). % 4.76/2.76 tff(propagation_strategy, type, propagation_strategy: $i > $o). % 4.76/2.76 % 4.76/2.76 %Saturated clause set: % 4.76/2.77 tff(c_243, plain, (![A_81, B_61]: (~rapid_change(sk1(A_81)) | ~observational_period(sk1(A_81)) | selection_favors(first_movers, efficient_producers, end_time(critical_point(sk1(A_81)))) | ~greater(critical_point(critical_point(sk1(A_81))), B_61) | ~environment(critical_point(sk1(A_81))) | greater(appear(efficient_producers, critical_point(sk1(A_81))), B_61) | ~in_environment(critical_point(sk1(A_81)), B_61) | extreme(A_81) | selection_favors(efficient_producers, first_movers, A_81) | ~observational_period(A_81) | empty(sk1(A_81)) | selection_favors(first_movers, efficient_producers, end_time(sk1(A_81))) | ~environment(sk1(A_81))))). % 4.76/2.77 tff(c_170, plain, (![A_18, B_64, B_19]: (~rapid_change(A_18) | ~observational_period(A_18) | selection_favors(first_movers, efficient_producers, end_time(critical_point(A_18))) | ~greater(critical_point(critical_point(A_18)), B_64) | ~environment(critical_point(A_18)) | greater(appear(efficient_producers, critical_point(A_18)), B_64) | ~in_environment(critical_point(A_18), B_64) | selection_favors(first_movers, efficient_producers, end_time(A_18)) | ~greater(critical_point(A_18), B_19) | ~environment(A_18) | greater(appear(efficient_producers, A_18), B_19) | ~in_environment(A_18, B_19)))). % 4.76/2.77 tff(c_222, plain, (![A_78]: (selection_favors(first_movers, efficient_producers, end_time(sk1(A_78))) | extreme(A_78) | selection_favors(efficient_producers, first_movers, A_78) | ~observational_period(A_78) | empty(sk1(A_78)) | ~environment(sk1(A_78)) | appear(efficient_producers, sk1(A_78))=end_time(sk1(A_78)) | greater(end_time(sk1(A_78)), appear(efficient_producers, sk1(A_78))) | ~in_environment(sk1(A_78), end_time(sk1(A_78)))))). % 4.76/2.77 tff(c_246, plain, (![A_81]: (~empty(critical_point(sk1(A_81))) | ~environment(critical_point(sk1(A_81))) | extreme(sk1(A_81)) | ~observational_period(sk1(A_81)) | extreme(A_81) | selection_favors(efficient_producers, first_movers, A_81) | ~observational_period(A_81) | empty(sk1(A_81)) | selection_favors(first_movers, efficient_producers, end_time(sk1(A_81))) | ~environment(sk1(A_81))))). % 4.76/2.77 tff(c_251, plain, (![A_2]: (~rapid_change(A_2) | extreme(A_2) | empty(sk1(A_2)) | selection_favors(first_movers, efficient_producers, end_time(sk1(A_2))) | ~environment(sk1(A_2)) | selection_favors(efficient_producers, first_movers, A_2) | ~observational_period(A_2)))). % 4.76/2.77 tff(c_245, plain, (![A_4, A_81]: (~in_environment(A_4, sk1(A_81)) | ~rapid_change(A_4) | ~observational_period(A_4) | extreme(A_81) | selection_favors(efficient_producers, first_movers, A_81) | ~observational_period(A_81) | empty(sk1(A_81)) | selection_favors(first_movers, efficient_producers, end_time(sk1(A_81))) | ~environment(sk1(A_81))))). % 4.76/2.77 tff(c_171, plain, (![A_10, B_64]: (~rapid_change(A_10) | ~observational_period(A_10) | selection_favors(first_movers, efficient_producers, end_time(appear(an_organisation, A_10))) | ~greater(critical_point(appear(an_organisation, A_10)), B_64) | ~environment(appear(an_organisation, A_10)) | greater(appear(efficient_producers, appear(an_organisation, A_10)), B_64) | ~in_environment(appear(an_organisation, A_10), B_64) | empty(A_10) | ~environment(A_10)))). % 4.76/2.77 tff(c_232, plain, (![A_80]: (extreme(A_80) | selection_favors(efficient_producers, first_movers, A_80) | ~observational_period(A_80) | empty(sk1(A_80)) | selection_favors(first_movers, efficient_producers, end_time(sk1(A_80))) | in_environment(sk1(A_80), critical_point(sk1(A_80))) | ~environment(sk1(A_80))))). % 4.76/2.77 tff(c_219, plain, (![A_78]: (extreme(A_78) | selection_favors(efficient_producers, first_movers, A_78) | ~observational_period(A_78) | empty(sk1(A_78)) | selection_favors(first_movers, efficient_producers, end_time(sk1(A_78))) | ~greater(critical_point(sk1(A_78)), end_time(sk1(A_78))) | ~environment(sk1(A_78)) | ~in_environment(sk1(A_78), end_time(sk1(A_78)))))). % 4.76/2.77 tff(c_199, plain, (![A_75]: (selection_favors(first_movers, efficient_producers, end_time(sk1(A_75))) | ~greater(appear(efficient_producers, sk1(A_75)), end_time(sk1(A_75))) | ~in_environment(sk1(A_75), end_time(sk1(A_75))) | extreme(A_75) | selection_favors(efficient_producers, first_movers, A_75) | ~observational_period(A_75) | empty(sk1(A_75)) | ~environment(sk1(A_75))))). % 4.76/2.77 tff(c_172, plain, (![A_2, B_64]: (~rapid_change(A_2) | selection_favors(first_movers, efficient_producers, end_time(sk1(A_2))) | ~greater(critical_point(sk1(A_2)), B_64) | ~environment(sk1(A_2)) | greater(appear(efficient_producers, sk1(A_2)), B_64) | ~in_environment(sk1(A_2), B_64) | selection_favors(efficient_producers, first_movers, A_2) | ~observational_period(A_2)))). % 4.76/2.77 tff(c_135, plain, (![B_21, A_53]: (selection_favors(first_movers, efficient_producers, B_21) | ~greater(appear(efficient_producers, sk1(A_53)), B_21) | ~greater_or_equal(B_21, appear(an_organisation, sk1(A_53))) | ~in_environment(sk1(A_53), B_21) | ~environment(sk1(A_53)) | extreme(A_53) | selection_favors(efficient_producers, first_movers, A_53) | ~observational_period(A_53)))). % 4.76/2.78 tff(c_173, plain, (![A_8, B_64]: (~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_64) | ~environment(end_time(A_8)) | greater(appear(efficient_producers, end_time(A_8)), B_64) | ~in_environment(end_time(A_8), B_64) | ~environment(A_8)))). % 4.76/2.78 tff(c_188, plain, (![B_19, A_60]: (selection_favors(first_movers, efficient_producers, B_19) | selection_favors(first_movers, efficient_producers, end_time(A_60)) | ~greater(critical_point(A_60), B_19) | ~environment(A_60) | ~in_environment(A_60, B_19) | greater(appear(efficient_producers, A_60), B_19)))). % 4.76/2.78 tff(c_160, plain, (![A_60, B_61]: (~empty(critical_point(A_60)) | ~environment(critical_point(A_60)) | extreme(A_60) | ~observational_period(A_60) | selection_favors(first_movers, efficient_producers, end_time(A_60)) | ~greater(critical_point(A_60), B_61) | ~environment(A_60) | greater(appear(efficient_producers, A_60), B_61) | ~in_environment(A_60, B_61)))). % 4.76/2.78 tff(c_159, plain, (![A_4, A_60, B_61]: (~in_environment(A_4, A_60) | ~rapid_change(A_4) | ~observational_period(A_4) | selection_favors(first_movers, efficient_producers, end_time(A_60)) | ~greater(critical_point(A_60), B_61) | ~environment(A_60) | greater(appear(efficient_producers, A_60), B_61) | ~in_environment(A_60, B_61)))). % 4.76/2.78 tff(c_148, plain, (![A_18, B_19]: (selection_favors(first_movers, efficient_producers, end_time(A_18)) | in_environment(A_18, critical_point(A_18)) | ~greater(critical_point(A_18), B_19) | ~environment(A_18) | greater(appear(efficient_producers, A_18), B_19) | ~in_environment(A_18, B_19)))). % 4.76/2.78 tff(c_144, plain, (![B_19, A_18]: (selection_favors(first_movers, efficient_producers, B_19) | ~greater(critical_point(A_18), B_19) | ~in_environment(A_18, critical_point(A_18)) | ~environment(A_18) | greater(appear(efficient_producers, A_18), B_19) | ~in_environment(A_18, B_19)))). % 4.76/2.78 tff(c_24, plain, (![A_12, B_13]: (selection_favors(first_movers, efficient_producers, end_time(A_12)) | in_environment(A_12, critical_point(A_12)) | ~greater(critical_point(A_12), B_13) | ~greater_or_equal(B_13, appear(efficient_producers, A_12)) | ~environment(A_12)))). % 4.76/2.78 tff(c_34, plain, (![B_23, A_22]: (selection_favors(first_movers, efficient_producers, B_23) | ~greater(critical_point(A_22), B_23) | ~greater_or_equal(B_23, appear(efficient_producers, A_22)) | ~in_environment(A_22, critical_point(A_22)) | ~environment(A_22)))). % 4.76/2.78 tff(c_128, plain, (![A_52]: (extreme(A_52) | appear(first_movers, sk1(A_52))=appear(an_organisation, sk1(A_52)) | selection_favors(efficient_producers, first_movers, A_52) | ~observational_period(A_52)))). % 4.76/2.78 tff(c_91, plain, (![A_1]: (appear(first_movers, sk1(A_1))=appear(an_organisation, sk1(A_1)) | empty(sk1(A_1)) | selection_favors(efficient_producers, first_movers, A_1) | ~observational_period(A_1)))). % 4.76/2.78 tff(c_97, plain, (![A_43, B_42]: (appear(efficient_producers, A_43)=B_42 | greater(B_42, appear(efficient_producers, A_43)) | greater(appear(efficient_producers, A_43), B_42) | ~in_environment(A_43, B_42)))). % 4.76/2.78 tff(c_32, plain, (![B_21, A_20]: (selection_favors(first_movers, efficient_producers, B_21) | ~greater(appear(efficient_producers, A_20), B_21) | ~greater_or_equal(B_21, appear(first_movers, A_20)) | ~in_environment(A_20, B_21) | ~environment(A_20)))). % 4.76/2.78 tff(c_86, plain, (![A_38]: (~empty(appear(an_organisation, A_38)) | ~environment(appear(an_organisation, A_38)) | extreme(A_38) | ~observational_period(A_38) | empty(A_38) | ~environment(A_38)))). % 4.76/2.78 tff(c_58, plain, (![A_29]: (appear(an_organisation, A_29)=end_time(A_29) | greater(end_time(A_29), appear(an_organisation, A_29)) | empty(A_29) | ~environment(A_29)))). % 4.76/2.78 tff(c_102, plain, (![A_1]: (~empty(sk1(A_1)) | extreme(A_1) | selection_favors(efficient_producers, first_movers, A_1) | ~observational_period(A_1)))). % 4.76/2.78 tff(c_30, plain, (![B_19, A_18]: (greater_or_equal(B_19, appear(efficient_producers, A_18)) | greater(appear(efficient_producers, A_18), B_19) | ~in_environment(A_18, B_19)))). % 4.76/2.78 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)))). % 4.76/2.78 tff(c_85, plain, (![A_38]: (appear(first_movers, A_38)=appear(an_organisation, A_38) | empty(A_38) | ~environment(A_38)))). % 4.76/2.78 tff(c_77, plain, (![A_10]: (in_environment(A_10, appear(an_organisation, A_10)) | empty(A_10) | ~environment(A_10)))). % 4.76/2.78 tff(c_22, plain, (![A_11]: (in_environment(A_11, appear(an_organisation, A_11)) | ~greater_or_equal(end_time(A_11), appear(an_organisation, A_11)) | ~environment(A_11)))). % 4.76/2.78 tff(c_36, plain, (![A_24]: (appear(first_movers, A_24)=appear(an_organisation, A_24) | ~in_environment(A_24, appear(an_organisation, A_24)) | ~environment(A_24)))). % 4.76/2.78 tff(c_68, plain, (![A_8]: (~empty(end_time(A_8)) | ~environment(end_time(A_8)) | extreme(A_8) | ~observational_period(A_8) | ~environment(A_8)))). % 4.76/2.78 tff(c_46, 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)))). % 4.76/2.78 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)))). % 4.76/2.79 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)))). % 4.76/2.79 tff(c_48, plain, (![A_2]: (selection_favors(efficient_producers, first_movers, A_2) | in_environment(A_2, sk1(A_2)) | ~observational_period(A_2)))). % 4.76/2.79 tff(c_20, plain, (![A_10]: (greater_or_equal(end_time(A_10), appear(an_organisation, A_10)) | empty(A_10) | ~environment(A_10)))). % 4.76/2.79 tff(c_50, plain, (![A_1]: (selection_favors(efficient_producers, first_movers, A_1) | environment(sk1(A_1)) | ~observational_period(A_1)))). % 4.76/2.79 tff(c_28, plain, (![B_17, A_16]: (B_17=A_16 | greater(A_16, B_17) | ~greater_or_equal(A_16, B_17)))). % 4.76/2.79 tff(c_16, plain, (![A_8]: (in_environment(A_8, end_time(A_8)) | ~environment(A_8)))). % 4.76/2.79 tff(c_44, plain, (~selection_favors(first_movers, efficient_producers, sk2))). % 4.76/2.79 tff(c_14, plain, (propagation_strategy(efficient_producers))). % 4.76/2.79 tff(c_40, plain, (rapid_change(sk2))). % 4.76/2.79 tff(c_12, plain, (propagation_strategy(first_movers))). % 4.76/2.79 tff(c_38, plain, (observational_period(sk2))). % 4.76/2.79 tff(c_42, plain, (~extreme(sk2))). % 4.76/2.79 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.76/2.79 %------------------------------------------------------------------------------