%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MGT031-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/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 : n026.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:55 AM UTC 2026 % Result : Satisfiable 3.62s 2.49s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT031-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/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.10/0.37 % Computer : n026.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Mon Sep 7 12:24:12 UTC 2026 % 0.10/0.37 % CPUTime : % 3.62/2.49 % 3.62/2.49 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.62/2.50 % 3.62/2.50 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.87/2.51 %$ subpopulation > in_environment > greater_or_equal > greater > environment > sk1 > number_of_organizations > cardinality_at_time > appear > #nlpp > zero > sk2 > first_movers > efficient_producers > e > an_organisation % 3.87/2.51 % 3.87/2.51 %Foreground sorts: % 3.87/2.51 % 3.87/2.51 % 3.87/2.51 %Background operators: % 3.87/2.51 % 3.87/2.51 % 3.87/2.51 %Foreground operators: % 3.87/2.51 tff(greater, type, greater: ($i * $i) > $o). % 3.87/2.51 tff(number_of_organizations, type, number_of_organizations: ($i * $i) > $i). % 3.87/2.51 tff(in_environment, type, in_environment: ($i * $i) > $o). % 3.87/2.51 tff(sk2, type, sk2: $i). % 3.87/2.51 tff(appear, type, appear: ($i * $i) > $i). % 3.87/2.51 tff(efficient_producers, type, efficient_producers: $i). % 3.87/2.51 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i). % 3.87/2.51 tff(environment, type, environment: $i > $o). % 3.87/2.51 tff(first_movers, type, first_movers: $i). % 3.87/2.51 tff(an_organisation, type, an_organisation: $i). % 3.87/2.51 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o). % 3.87/2.51 tff(e, type, e: $i). % 3.87/2.51 tff(subpopulation, type, subpopulation: ($i * $i * $i) > $o). % 3.87/2.51 tff(sk1, type, sk1: ($i * $i) > $i). % 3.87/2.51 tff(zero, type, zero: $i). % 3.87/2.51 % 3.87/2.51 %Saturated clause set: % 3.87/2.51 tff(c_150, plain, (![A_11, A_73, A_72]: (greater(A_11, appear(an_organisation, A_73)) | ~greater(A_11, appear(first_movers, A_72)) | appear(first_movers, A_73)=appear(an_organisation, A_73) | ~greater(appear(an_organisation, A_72), appear(efficient_producers, e)) | ~environment(A_73) | appear(first_movers, A_72)=appear(an_organisation, A_72) | ~environment(A_72)))). % 3.87/2.51 tff(c_131, plain, (![A_67, A_68]: (greater(appear(first_movers, A_67), appear(an_organisation, A_68)) | appear(first_movers, A_68)=appear(an_organisation, A_68) | ~greater(appear(an_organisation, A_67), appear(efficient_producers, e)) | ~environment(A_68) | appear(first_movers, A_67)=appear(an_organisation, A_67) | ~environment(A_67)))). % 3.87/2.51 tff(c_133, plain, (![A_11, A_68, A_67]: (greater(A_11, appear(first_movers, A_68)) | ~greater(A_11, appear(first_movers, A_67)) | ~greater(appear(an_organisation, A_67), appear(efficient_producers, e)) | ~environment(A_68) | appear(first_movers, A_67)=appear(an_organisation, A_67) | ~environment(A_67)))). % 3.87/2.51 tff(c_88, plain, (![A_34, A_52]: (greater(appear(first_movers, A_34), appear(first_movers, A_52)) | ~greater(appear(an_organisation, A_34), appear(efficient_producers, e)) | ~environment(A_52) | appear(first_movers, A_34)=appear(an_organisation, A_34) | ~environment(A_34)))). % 3.87/2.51 tff(c_122, plain, (~environment(e))). % 3.87/2.51 tff(c_116, plain, (![B_3, A_2]: (sk1(B_3, A_2)=first_movers | sk1(B_3, A_2)=efficient_producers | ~greater(number_of_organizations(A_2, B_3), zero) | ~environment(A_2)))). % 3.87/2.51 tff(c_111, plain, (~greater(zero, appear(efficient_producers, e)))). % 3.87/2.52 tff(c_101, plain, (![A_11, A_32]: (greater(A_11, appear(an_organisation, A_32)) | appear(first_movers, A_32)=appear(an_organisation, A_32) | ~greater(A_11, appear(efficient_producers, e)) | ~environment(A_32)))). % 3.87/2.52 tff(c_102, plain, (![A_23]: (greater(appear(efficient_producers, e), appear(an_organisation, A_23)) | appear(first_movers, A_23)=appear(an_organisation, A_23) | ~environment(A_23)))). % 3.87/2.52 tff(c_76, plain, (![A_11, A_50]: (greater(A_11, appear(an_organisation, A_50)) | ~greater(A_11, appear(first_movers, A_50)) | appear(first_movers, A_50)=appear(an_organisation, A_50) | ~environment(A_50)))). % 3.87/2.52 tff(c_66, plain, (![A_11, B_41, A_42]: (greater(A_11, zero) | ~greater(A_11, cardinality_at_time(sk1(B_41, A_42), B_41)) | ~greater(number_of_organizations(A_42, B_41), zero) | ~environment(A_42)))). % 3.87/2.52 tff(c_61, plain, (![A_11, A_38, A_37]: (greater(A_11, appear(first_movers, A_38)) | ~greater(A_11, A_37) | ~greater(A_37, appear(efficient_producers, e)) | ~environment(A_38)))). % 3.87/2.52 tff(c_56, plain, (![A_34]: (appear(first_movers, A_34)=appear(an_organisation, A_34) | greater(appear(first_movers, A_34), appear(an_organisation, A_34)) | ~environment(A_34)))). % 3.87/2.52 tff(c_10, plain, (![B_9, A_8]: (~greater(cardinality_at_time(first_movers, B_9), zero) | ~greater(appear(first_movers, A_8), B_9) | ~in_environment(A_8, B_9) | ~environment(A_8)))). % 3.87/2.52 tff(c_8, plain, (![B_7, A_6]: (~greater(cardinality_at_time(efficient_producers, B_7), zero) | ~greater(appear(efficient_producers, A_6), B_7) | ~in_environment(A_6, B_7) | ~environment(A_6)))). % 3.87/2.52 tff(c_22, plain, (![B_21, C_22, A_20]: (first_movers=B_21 | efficient_producers=B_21 | ~greater(cardinality_at_time(B_21, C_22), zero) | ~subpopulation(B_21, A_20, C_22) | ~environment(A_20)))). % 3.87/2.52 tff(c_6, plain, (![B_5, A_4]: (greater(cardinality_at_time(sk1(B_5, A_4), B_5), zero) | ~greater(number_of_organizations(A_4, B_5), zero) | ~environment(A_4)))). % 3.87/2.52 tff(c_4, plain, (![B_3, A_2]: (subpopulation(sk1(B_3, A_2), A_2, B_3) | ~greater(number_of_organizations(A_2, B_3), zero) | ~environment(A_2)))). % 3.87/2.52 tff(c_47, plain, (![A_11, A_32]: (greater(A_11, appear(first_movers, A_32)) | ~greater(A_11, appear(efficient_producers, e)) | ~environment(A_32)))). % 3.87/2.52 tff(c_51, plain, (![A_11, A_33]: (greater(A_11, zero) | ~greater(A_11, number_of_organizations(e, appear(an_organisation, A_33))) | ~environment(A_33)))). % 3.87/2.52 tff(c_12, plain, (![A_10]: (greater_or_equal(appear(first_movers, A_10), appear(an_organisation, A_10)) | ~environment(A_10)))). % 3.87/2.52 tff(c_2, plain, (![A_1]: (greater(number_of_organizations(e, appear(an_organisation, A_1)), zero) | ~environment(A_1)))). % 3.87/2.52 tff(c_24, plain, (![A_23]: (greater(appear(efficient_producers, e), appear(first_movers, A_23)) | ~environment(A_23)))). % 3.87/2.52 tff(c_14, plain, (![A_11, C_13, B_12]: (greater(A_11, C_13) | ~greater(B_12, C_13) | ~greater(A_11, B_12)))). % 3.87/2.52 tff(c_16, plain, (![B_15, A_14]: (B_15=A_14 | greater(A_14, B_15) | ~greater_or_equal(A_14, B_15)))). % 3.87/2.52 tff(c_18, plain, (![A_16, B_17]: (greater_or_equal(A_16, B_17) | ~greater(A_16, B_17)))). % 3.87/2.52 tff(c_30, plain, (appear(first_movers, sk2)!=appear(an_organisation, sk2))). % 3.87/2.52 tff(c_28, plain, (in_environment(sk2, appear(an_organisation, sk2)))). % 3.87/2.52 tff(c_20, plain, (![B_19]: (greater_or_equal(B_19, B_19)))). % 3.87/2.52 tff(c_26, plain, (environment(sk2))). % 3.87/2.52 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.87/2.52 %------------------------------------------------------------------------------