%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MGT038-10 : TPTP v9.3.0. Released v7.5.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 : n019.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 5.90s 3.10s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT038-10 : TPTP v9.3.0. Released v7.5.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.12/0.37 % Computer : n019.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Mon Sep 7 12:47:52 UTC 2026 % 0.12/0.38 % CPUTime : % 5.90/3.10 % 5.90/3.10 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.90/3.10 % 5.90/3.10 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.90/3.13 %$ ifeq2 > ifeq > tuple > sk1 > in_environment > greater > contracts_from > cardinality_at_time > appear > #nlpp > stable > sk2 > finite_set > environment > zero > true > to > t2 > sk3 > s > first_movers > efficient_producers > e % 5.90/3.13 % 5.90/3.13 %Foreground sorts: % 5.90/3.13 % 5.90/3.13 % 5.90/3.13 %Background operators: % 5.90/3.13 % 5.90/3.13 % 5.90/3.13 %Foreground operators: % 5.90/3.13 tff(tuple, type, tuple: ($i * $i * $i) > $i). % 5.90/3.13 tff(sk2, type, sk2: $i > $i). % 5.90/3.13 tff(in_environment, type, in_environment: ($i * $i) > $i). % 5.90/3.13 tff(appear, type, appear: ($i * $i) > $i). % 5.90/3.13 tff(efficient_producers, type, efficient_producers: $i). % 5.90/3.13 tff(s, type, s: $i). % 5.90/3.13 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i). % 5.90/3.13 tff(environment, type, environment: $i > $i). % 5.90/3.13 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 5.90/3.13 tff(stable, type, stable: $i > $i). % 5.90/3.13 tff(t2, type, t2: $i). % 5.90/3.13 tff(to, type, to: $i). % 5.90/3.13 tff(first_movers, type, first_movers: $i). % 5.90/3.13 tff(sk3, type, sk3: $i). % 5.90/3.13 tff(greater, type, greater: ($i * $i) > $i). % 5.90/3.13 tff(contracts_from, type, contracts_from: ($i * $i) > $i). % 5.90/3.13 tff(true, type, true: $i). % 5.90/3.13 tff(finite_set, type, finite_set: $i > $i). % 6.33/3.13 tff(e, type, e: $i). % 6.33/3.13 tff(sk1, type, sk1: ($i * $i) > $i). % 6.33/3.13 tff(zero, type, zero: $i). % 6.33/3.13 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 6.33/3.13 % 6.33/3.13 %Saturated clause set: % 6.33/3.13 tff(c_1117, plain, (![A_79]: (ifeq(in_environment(A_79, appear(efficient_producers, sk3)), true, ifeq(environment(A_79), true, ifeq(stable(A_79), true, in_environment(A_79, sk1(sk2(sk3), first_movers)), true), true), true)=true))). % 6.33/3.13 tff(c_1074, plain, (![A_77]: (ifeq(in_environment(A_77, sk2(sk3)), true, ifeq(environment(A_77), true, ifeq(stable(A_77), true, in_environment(A_77, sk1(sk2(sk3), first_movers)), true), true), true)=true))). % 6.33/3.13 tff(c_1015, plain, (![A_75]: (ifeq(in_environment(A_75, appear(first_movers, sk3)), true, ifeq(environment(A_75), true, ifeq(stable(A_75), true, in_environment(A_75, appear(efficient_producers, e)), true), true), true)=true))). % 6.33/3.13 tff(c_578, plain, (![B_15]: (ifeq(greater(B_15, appear(efficient_producers, sk3)), true, ifeq(greater(sk1(sk2(sk3), first_movers), B_15), true, true, true), true)=true))). % 6.33/3.13 tff(c_745, plain, (![A_64]: (ifeq(in_environment(A_64, appear(efficient_producers, sk3)), true, ifeq(environment(A_64), true, ifeq(stable(A_64), true, in_environment(A_64, sk2(sk3)), true), true), true)=true))). % 6.33/3.14 tff(c_943, plain, (ifeq(in_environment(sk3, appear(efficient_producers, sk3)), true, in_environment(sk3, sk1(sk2(sk3), first_movers)), true)=true)). % 6.33/3.14 tff(c_901, plain, (![A_71]: (ifeq(greater(A_71, sk1(sk2(sk3), first_movers)), true, greater(A_71, appear(efficient_producers, sk3)), true)=true))). % 6.33/3.14 tff(c_877, plain, (ifeq(in_environment(sk3, sk2(sk3)), true, in_environment(sk3, sk1(sk2(sk3), first_movers)), true)=true)). % 6.33/3.14 tff(c_237, plain, (![B_39]: (ifeq(greater(B_39, appear(first_movers, sk3)), true, ifeq(greater(appear(efficient_producers, e), B_39), true, true, true), true)=true))). % 6.33/3.14 tff(c_842, plain, (ifeq(greater(sk1(sk2(sk3), first_movers), sk1(sk2(sk3), first_movers)), true, true, true)=true)). % 6.33/3.14 tff(c_819, plain, (![A_68]: (ifeq(greater(A_68, sk1(sk2(sk3), first_movers)), true, greater(A_68, sk2(sk3)), true)=true))). % 6.33/3.14 tff(c_784, plain, (![A_66]: (ifeq(greater(A_66, appear(efficient_producers, e)), true, greater(A_66, appear(first_movers, sk3)), true)=true))). % 6.33/3.14 tff(c_281, plain, (![B_15]: (ifeq(greater(B_15, sk2(sk3)), true, ifeq(greater(sk1(sk2(sk3), first_movers), B_15), true, true, true), true)=true))). % 6.33/3.14 tff(c_722, plain, (ifeq(greater(sk2(sk3), sk1(sk2(sk3), first_movers)), true, true, true)=true)). % 6.33/3.14 tff(c_673, plain, (![A_62]: (ifeq(greater(A_62, sk2(sk3)), true, greater(A_62, appear(efficient_producers, sk3)), true)=true))). % 6.33/3.14 tff(c_649, plain, (ifeq(in_environment(sk3, appear(efficient_producers, sk3)), true, in_environment(sk3, sk2(sk3)), true)=true)). % 6.33/3.14 tff(c_460, plain, (![B_13]: (ifeq(greater(appear(efficient_producers, e), B_13), true, ifeq(in_environment(sk3, B_13), true, true, true), true)=true))). % 6.33/3.14 tff(c_617, plain, (ifeq(greater(appear(efficient_producers, sk3), sk2(sk3)), true, true, true)=true)). % 6.33/3.14 tff(c_582, plain, (![C_16]: (ifeq(greater(appear(efficient_producers, sk3), C_16), true, greater(sk1(sk2(sk3), first_movers), C_16), true)=true))). % 6.33/3.14 tff(c_373, plain, (![B_15]: (ifeq(greater(B_15, appear(efficient_producers, sk3)), true, ifeq(greater(sk2(sk3), B_15), true, true, true), true)=true))). % 6.33/3.14 tff(c_551, plain, (greater(sk1(sk2(sk3), first_movers), appear(efficient_producers, sk3))=true)). % 6.33/3.14 tff(c_540, plain, (ifeq(greater(appear(efficient_producers, sk3), appear(efficient_producers, sk3)), true, true, true)=true)). % 6.33/3.14 tff(c_377, plain, (![C_16]: (ifeq(greater(appear(efficient_producers, sk3), C_16), true, greater(sk2(sk3), C_16), true)=true))). % 6.33/3.14 tff(c_502, plain, (ifeq(greater(appear(efficient_producers, e), appear(efficient_producers, e)), true, true, true)=true)). % 6.33/3.14 tff(c_522, plain, (ifeq(greater(appear(first_movers, sk3), appear(efficient_producers, e)), true, true, true)=true)). % 6.33/3.14 tff(c_400, plain, (![A_7, B_50]: (ifeq(greater(appear(first_movers, A_7), B_50), true, ifeq(in_environment(A_7, B_50), true, true, true), true)=true))). % 6.33/3.14 tff(c_459, plain, (![C_12]: (ifeq(greater(C_12, appear(efficient_producers, e)), true, in_environment(sk3, C_12), true)=true))). % 6.33/3.14 tff(c_415, plain, (![C_49, B_50]: (ifeq(greater(C_49, B_50), true, ifeq(in_environment(sk3, B_50), true, in_environment(sk3, C_49), true), true)=true))). % 6.33/3.14 tff(c_441, plain, (tuple(cardinality_at_time(first_movers, to), true, true)!=tuple(zero, true, true))). % 6.33/3.14 tff(c_433, plain, (in_environment(sk3, appear(efficient_producers, e))=true)). % 6.33/3.14 tff(c_412, plain, (![C_49]: (ifeq(greater(C_49, appear(first_movers, sk3)), true, in_environment(sk3, C_49), true)=true))). % 6.33/3.14 tff(c_14, plain, (![C_12, B_13, A_14]: (ifeq(greater(C_12, B_13), true, ifeq(in_environment(A_14, B_13), true, ifeq(environment(A_14), true, ifeq(stable(A_14), true, in_environment(A_14, C_12), true), true), true), true)=true))). % 6.33/3.14 tff(c_356, plain, (greater(sk2(sk3), appear(efficient_producers, sk3))=true)). % 6.33/3.14 tff(c_18, plain, (![A_18]: (ifeq(environment(A_18), true, ifeq(stable(A_18), true, greater(sk2(A_18), appear(efficient_producers, A_18)), true), true)=true))). % 6.33/3.15 tff(c_306, plain, (![B_46]: (ifeq(contracts_from(B_46, first_movers), true, greater(sk1(B_46, first_movers), B_46), true)=true))). % 6.33/3.15 tff(c_294, plain, (ifeq(greater(sk2(sk3), sk2(sk3)), true, true, true)=true)). % 6.33/3.15 tff(c_285, plain, (![C_16]: (ifeq(greater(sk2(sk3), C_16), true, greater(sk1(sk2(sk3), first_movers), C_16), true)=true))). % 6.33/3.15 tff(c_268, plain, (greater(sk1(sk2(sk3), first_movers), sk2(sk3))=true)). % 6.33/3.15 tff(c_10, plain, (![A_8, B_9]: (ifeq(finite_set(A_8), true, ifeq(contracts_from(B_9, A_8), true, greater(sk1(B_9, A_8), B_9), true), true)=true))). % 6.33/3.15 tff(c_189, plain, (tuple(cardinality_at_time(first_movers, to), true, greater(appear(first_movers, sk3), appear(first_movers, sk3)))!=tuple(zero, true, true))). % 6.33/3.15 tff(c_248, plain, (ifeq(greater(appear(first_movers, sk3), appear(first_movers, sk3)), true, true, true)=true)). % 6.33/3.15 tff(c_240, plain, (![C_40]: (ifeq(greater(appear(first_movers, sk3), C_40), true, greater(appear(efficient_producers, e), C_40), true)=true))). % 6.33/3.15 tff(c_16, plain, (![B_15, C_16, A_17]: (ifeq(greater(B_15, C_16), true, ifeq(greater(A_17, B_15), true, greater(A_17, C_16), true), true)=true))). % 6.33/3.15 tff(c_172, plain, (![A_10, B_11]: (ifeq2(finite_set(A_10), true, ifeq2(contracts_from(B_11, A_10), true, zero, zero), zero)=zero))). % 6.33/3.15 tff(c_171, plain, (![B_31]: (ifeq2(contracts_from(B_31, first_movers), true, zero, zero)=zero))). % 6.33/3.15 tff(c_28, plain, (![A_21]: (tuple(cardinality_at_time(first_movers, to), in_environment(sk3, A_21), greater(A_21, appear(first_movers, sk3)))!=tuple(zero, true, true)))). % 6.33/3.15 tff(c_169, plain, (in_environment(sk3, appear(first_movers, sk3))=true)). % 6.33/3.15 tff(c_154, plain, (cardinality_at_time(s, t2)=zero)). % 6.33/3.15 tff(c_8, plain, (![A_7]: (ifeq(environment(A_7), true, ifeq(stable(A_7), true, in_environment(A_7, appear(first_movers, A_7)), true), true)=true))). % 6.33/3.15 tff(c_140, plain, (contracts_from(sk2(sk3), first_movers)=true)). % 6.33/3.15 tff(c_20, plain, (![A_19]: (ifeq(environment(A_19), true, ifeq(stable(A_19), true, contracts_from(sk2(A_19), first_movers), true), true)=true))). % 6.33/3.15 tff(c_72, plain, (greater(appear(efficient_producers, e), appear(first_movers, sk3))=true)). % 6.33/3.15 tff(c_22, plain, (![A_20]: (ifeq(environment(A_20), true, greater(appear(efficient_producers, e), appear(first_movers, A_20)), true)=true))). % 6.33/3.15 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq2(A_1, A_1, B_2, C_3)=B_2))). % 6.33/3.15 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq(A_4, A_4, B_5, C_6)=B_5))). % 6.33/3.15 tff(c_6, plain, (finite_set(first_movers)=true)). % 6.33/3.15 tff(c_24, plain, (environment(sk3)=true)). % 6.33/3.15 tff(c_26, plain, (stable(sk3)=true)). % 6.33/3.15 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.33/3.15 %------------------------------------------------------------------------------