%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : MGT038-10 : TPTP v9.3.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n004.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:20:40 AM UTC 2026 % Result : Satisfiable 0.45s 1.06s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT038-10 : TPTP v9.3.0. Released v7.5.0. % 0.00/0.02 % Command : run_Leo-III %s %d THM % 0.07/0.34 % Computer : n004.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Mon Sep 7 12:46:45 UTC 2026 % 0.07/0.34 % CPUTime : % 0.45/1.06 % SZS status Satisfiable % 0.45/1.06 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 0.45/1.06 1: finite_set(first_movers) -> true % 0.45/1.06 2: environment(sk3) -> true % 0.45/1.06 3: stable(sk3) -> true % 0.45/1.06 4: eq(X, X) -> true0 % 0.45/1.06 5: ifeq2(X, X, Y, Z) -> Y % 0.45/1.06 6: ifeq(X, X, Y, Z) -> Y % 0.45/1.06 7: ifeq(environment(X), true, greater(appear(efficient_producers, e), appear(first_movers, X)), true) -> true % 0.45/1.06 8: greater(appear(efficient_producers, e), appear(first_movers, sk3)) -> true % 0.45/1.06 9: ifeq(environment(X), true, ifeq(stable(X), true, contracts_from(sk2(X), first_movers), true), true) -> true % 0.45/1.06 10: true -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 12: ifeq2(finite_set(X), contracts_from(sk2(sk3), first_movers), ifeq2(contracts_from(Y, X), contracts_from(sk2(sk3), first_movers), cardinality_at_time(s, t2), zero), zero) -> zero % 0.45/1.06 13: zero -> cardinality_at_time(s, t2) % 0.45/1.06 14: ifeq2(contracts_from(X, first_movers), contracts_from(sk2(sk3), first_movers), cardinality_at_time(s, t2), cardinality_at_time(s, t2)) -> cardinality_at_time(s, t2) % 0.45/1.06 16: ifeq(greater(X, Y), contracts_from(sk2(sk3), first_movers), ifeq(greater(Z, X), contracts_from(sk2(sk3), first_movers), greater(Z, Y), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 18: ifeq(environment(X), contracts_from(sk2(sk3), first_movers), ifeq(stable(X), contracts_from(sk2(sk3), first_movers), in_environment(X, appear(first_movers, X)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 19: in_environment(sk3, appear(first_movers, sk3)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 21: ifeq(finite_set(X), contracts_from(sk2(sk3), first_movers), ifeq(contracts_from(Y, X), contracts_from(sk2(sk3), first_movers), greater(sk1(Y, X), Y), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 22: greater(sk1(sk2(sk3), first_movers), sk2(sk3)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 24: ifeq(environment(X), contracts_from(sk2(sk3), first_movers), ifeq(stable(X), contracts_from(sk2(sk3), first_movers), greater(sk2(X), appear(efficient_producers, X)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 25: greater(sk2(sk3), appear(efficient_producers, sk3)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 27: eq(tuple(cardinality_at_time(first_movers, to), in_environment(sk3, X), greater(X, appear(first_movers, sk3))), tuple(cardinality_at_time(s, t2), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers))) -> false % 0.45/1.06 28: ifeq(contracts_from(X, first_movers), contracts_from(sk2(sk3), first_movers), greater(sk1(X, first_movers), X), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 29: ifeq(environment(X), contracts_from(sk2(sk3), first_movers), greater(appear(efficient_producers, e), appear(first_movers, X)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 30: ifeq(greater(appear(efficient_producers, sk3), X), contracts_from(sk2(sk3), first_movers), greater(sk2(sk3), X), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 31: ifeq(greater(X, sk2(sk3)), contracts_from(sk2(sk3), first_movers), greater(X, appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 32: greater(sk1(sk2(sk3), first_movers), appear(efficient_producers, sk3)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 33: ifeq(greater(sk2(sk3), sk2(sk3)), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 34: ifeq(greater(X, appear(efficient_producers, e)), contracts_from(sk2(sk3), first_movers), greater(X, appear(first_movers, sk3)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 35: ifeq(greater(appear(first_movers, sk3), X), contracts_from(sk2(sk3), first_movers), greater(appear(efficient_producers, e), X), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 36: ifeq(greater(sk2(sk3), X), contracts_from(sk2(sk3), first_movers), greater(sk1(sk2(sk3), first_movers), X), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 37: ifeq(greater(X, sk1(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers), greater(X, sk2(sk3)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 38: ifeq(greater(appear(first_movers, sk3), appear(first_movers, sk3)), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 39: ifeq(greater(appear(efficient_producers, e), appear(efficient_producers, e)), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 40: ifeq(greater(appear(efficient_producers, sk3), appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 41: ifeq(greater(appear(efficient_producers, sk3), X), contracts_from(sk2(sk3), first_movers), greater(sk1(sk2(sk3), first_movers), X), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 42: ifeq(greater(appear(efficient_producers, sk3), sk2(sk3)), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 43: ifeq(greater(X, sk1(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers), greater(X, appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 44: ifeq(greater(sk2(sk3), sk1(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 46: ifeq(greater(X, Y), contracts_from(sk2(sk3), first_movers), ifeq(in_environment(Z, Y), contracts_from(sk2(sk3), first_movers), ifeq(environment(Z), contracts_from(sk2(sk3), first_movers), ifeq(stable(Z), contracts_from(sk2(sk3), first_movers), in_environment(Z, X), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 47: ifeq(greater(X, appear(first_movers, sk3)), contracts_from(sk2(sk3), first_movers), in_environment(sk3, X), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 48: in_environment(sk3, appear(efficient_producers, e)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 49: ifeq(greater(X, appear(efficient_producers, e)), contracts_from(sk2(sk3), first_movers), in_environment(sk3, X), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 50: ifeq(greater(appear(first_movers, sk3), appear(efficient_producers, e)), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 51: ifeq(greater(sk1(sk2(sk3), first_movers), sk1(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 52: ifeq2(finite_set(X), contracts_from(sk2(sk3), first_movers), ifeq2(contracts_from(Y, X), contracts_from(sk2(sk3), first_movers), cardinality_at_time(s, t2), cardinality_at_time(s, t2)), cardinality_at_time(s, t2)) -> cardinality_at_time(s, t2) % 0.45/1.06 53: eq(tuple(cardinality_at_time(first_movers, to), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)), tuple(cardinality_at_time(s, t2), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers))) -> false % 0.45/1.06 54: ifeq(environment(X), contracts_from(sk2(sk3), first_movers), ifeq(stable(X), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(X), first_movers), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 55: ifeq(greater(X, Y), contracts_from(sk2(sk3), first_movers), ifeq(in_environment(sk3, Y), contracts_from(sk2(sk3), first_movers), in_environment(sk3, X), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 56: ifeq(in_environment(sk3, appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers), in_environment(sk3, sk2(sk3)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 57: ifeq(in_environment(sk3, sk2(sk3)), contracts_from(sk2(sk3), first_movers), in_environment(sk3, sk1(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 58: ifeq(in_environment(sk3, appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers), in_environment(sk3, sk1(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 59: eq(tuple(cardinality_at_time(first_movers, to), contracts_from(sk2(sk3), first_movers), greater(appear(first_movers, sk3), appear(first_movers, sk3))), tuple(cardinality_at_time(s, t2), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers))) -> false % 0.45/1.06 60: ifeq(greater(appear(first_movers, X), Y), contracts_from(sk2(sk3), first_movers), ifeq(in_environment(X, Y), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 61: ifeq(greater(X, appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers), ifeq(greater(sk2(sk3), X), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 62: ifeq(greater(appear(efficient_producers, e), X), contracts_from(sk2(sk3), first_movers), ifeq(in_environment(sk3, X), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 63: ifeq(greater(X, sk2(sk3)), contracts_from(sk2(sk3), first_movers), ifeq(greater(sk1(sk2(sk3), first_movers), X), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 64: ifeq(greater(X, appear(first_movers, sk3)), contracts_from(sk2(sk3), first_movers), ifeq(greater(appear(efficient_producers, e), X), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 65: ifeq(greater(X, appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers), ifeq(greater(sk1(sk2(sk3), first_movers), X), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 66: ifeq(in_environment(X, appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers), ifeq(environment(X), contracts_from(sk2(sk3), first_movers), ifeq(stable(X), contracts_from(sk2(sk3), first_movers), in_environment(X, sk2(sk3)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 67: ifeq(in_environment(X, sk2(sk3)), contracts_from(sk2(sk3), first_movers), ifeq(environment(X), contracts_from(sk2(sk3), first_movers), ifeq(stable(X), contracts_from(sk2(sk3), first_movers), in_environment(X, sk1(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 68: ifeq(in_environment(X, appear(first_movers, sk3)), contracts_from(sk2(sk3), first_movers), ifeq(environment(X), contracts_from(sk2(sk3), first_movers), ifeq(stable(X), contracts_from(sk2(sk3), first_movers), in_environment(X, appear(efficient_producers, e)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 69: ifeq(in_environment(X, appear(efficient_producers, sk3)), contracts_from(sk2(sk3), first_movers), ifeq(environment(X), contracts_from(sk2(sk3), first_movers), ifeq(stable(X), contracts_from(sk2(sk3), first_movers), in_environment(X, sk1(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)), contracts_from(sk2(sk3), first_movers)) -> contracts_from(sk2(sk3), first_movers) % 0.45/1.06 %------------------------------------------------------------------------------