%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP002-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jul 15 07:23:28 AM UTC 2025 % Result : Satisfiable 3.36s 3.35s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP002-10 : TPTP v9.0.0. Released v7.5.0. % 0.07/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.33 % Computer : n001.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Jul 14 14:07:34 EDT 2025 % 0.12/0.33 % CPUTime : % 3.36/3.35 % SZS status Satisfiable % 3.36/3.35 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 3.36/3.35 1: hollywood(skc7) -> true % 3.36/3.35 2: city(skc7) -> true % 3.36/3.35 3: event(skc6) -> true % 3.36/3.35 4: street(skc5) -> true % 3.36/3.35 5: way(skc5) -> true % 3.36/3.35 6: lonely(skc5) -> true % 3.36/3.35 7: old(skc4) -> true % 3.36/3.35 8: dirty(skc4) -> true % 3.36/3.35 9: white(skc4) -> true % 3.36/3.35 10: car(skc4) -> true % 3.36/3.35 11: chevy(skc4) -> true % 3.36/3.35 12: in(skc6, skc7) -> true % 3.36/3.35 13: down(skc6, skc5) -> true % 3.36/3.35 14: barrel(skc6, skc4) -> true % 3.36/3.35 15: event(skf1(X, Y)) -> true % 3.36/3.35 16: ifeq(X, X, Y, Z) -> Y % 3.36/3.35 17: ifeq3(X, X, Y, Z) -> Y % 3.36/3.35 18: ifeq2(X, X, Y, Z) -> Y % 3.36/3.35 19: ifeq2(vehicle(X), true, transport(X), true) -> true % 3.36/3.35 20: ifeq2(transport(X), true, instrumentality(X), true) -> true % 3.36/3.35 21: ifeq2(instrumentality(X), true, artifact(X), true) -> true % 3.36/3.35 22: ifeq2(car(X), true, vehicle(X), true) -> true % 3.36/3.35 23: vehicle(skc4) -> true % 3.36/3.35 24: transport(skc4) -> true % 3.36/3.35 25: instrumentality(skc4) -> true % 3.36/3.35 26: artifact(skc4) -> true % 3.36/3.35 27: ifeq2(chevy(X), true, car(X), true) -> true % 3.36/3.35 28: ifeq2(street(X), true, way(X), true) -> true % 3.36/3.35 29: ifeq2(proposition(X), true, drs(X), true) -> true % 3.36/3.35 30: ifeq2(nonhuman(X), true, entity(X), true) -> true % 3.36/3.35 31: ifeq2(drs(X), true, proposition(X), true) -> true % 3.36/3.35 32: ifeq2(woman(X), true, female(X), true) -> true % 3.36/3.35 33: ifeq2(male(X), true, human(X), true) -> true % 3.36/3.35 34: ifeq2(female(X), true, human(X), true) -> true % 3.36/3.35 35: ifeq2(man(X), true, male(X), true) -> true % 3.36/3.35 36: ifeq2(city(X), true, location(X), true) -> true % 3.36/3.35 37: true -> location(skc7) % 3.36/3.35 39: ifeq2(object(X), location(skc7), entity(X), location(skc7)) -> location(skc7) % 3.36/3.35 41: ifeq2(location(X), location(skc7), object(X), location(skc7)) -> location(skc7) % 3.36/3.35 42: object(skc7) -> location(skc7) % 3.36/3.35 43: entity(skc7) -> location(skc7) % 3.36/3.35 45: ifeq2(hollywood(X), location(skc7), city(X), location(skc7)) -> location(skc7) % 3.36/3.35 47: ifeq2(artifact(X), location(skc7), object(X), location(skc7)) -> location(skc7) % 3.36/3.35 48: object(skc4) -> location(skc7) % 3.36/3.35 49: entity(skc4) -> location(skc7) % 3.36/3.35 51: ifeq2(event(X), location(skc7), eventuality(X), location(skc7)) -> location(skc7) % 3.36/3.35 52: eventuality(skc6) -> location(skc7) % 3.36/3.35 53: eventuality(skf1(X, Y)) -> location(skc7) % 3.36/3.35 55: ifeq2(way(X), location(skc7), artifact(X), location(skc7)) -> location(skc7) % 3.36/3.35 56: artifact(skc5) -> location(skc7) % 3.36/3.35 57: object(skc5) -> location(skc7) % 3.36/3.35 58: entity(skc5) -> location(skc7) % 3.36/3.35 59: ifeq2(man(X), location(skc7), male(X), location(skc7)) -> location(skc7) % 3.36/3.35 60: ifeq2(city(X), location(skc7), location(X), location(skc7)) -> location(skc7) % 3.36/3.35 61: ifeq2(instrumentality(X), location(skc7), artifact(X), location(skc7)) -> location(skc7) % 3.36/3.35 62: ifeq2(car(X), location(skc7), vehicle(X), location(skc7)) -> location(skc7) % 3.36/3.35 63: ifeq2(transport(X), location(skc7), instrumentality(X), location(skc7)) -> location(skc7) % 3.36/3.35 64: ifeq2(vehicle(X), location(skc7), transport(X), location(skc7)) -> location(skc7) % 3.36/3.35 65: ifeq2(chevy(X), location(skc7), car(X), location(skc7)) -> location(skc7) % 3.36/3.35 66: ifeq2(male(X), location(skc7), human(X), location(skc7)) -> location(skc7) % 3.36/3.35 67: ifeq2(female(X), location(skc7), human(X), location(skc7)) -> location(skc7) % 3.36/3.35 68: ifeq2(woman(X), location(skc7), female(X), location(skc7)) -> location(skc7) % 3.36/3.35 69: ifeq2(drs(X), location(skc7), proposition(X), location(skc7)) -> location(skc7) % 3.36/3.35 70: ifeq2(proposition(X), location(skc7), drs(X), location(skc7)) -> location(skc7) % 3.36/3.35 71: ifeq2(nonhuman(X), location(skc7), entity(X), location(skc7)) -> location(skc7) % 3.36/3.35 72: ifeq2(street(X), location(skc7), way(X), location(skc7)) -> location(skc7) % 3.36/3.35 73: ifeq2(instrumentality(skc5), location(skc7), location(skc7), location(skc7)) -> location(skc7) % 3.36/3.35 74: ifeq2(artifact(skc7), location(skc7), location(skc7), location(skc7)) -> location(skc7) % 3.36/3.35 76: ifeq(tuple(nonhuman(X), human(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 78: ifeq(tuple(woman(X), man(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 80: ifeq(tuple(female(X), male(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 82: ifeq(tuple(eventuality(X), abstraction(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 84: ifeq(tuple(entity(X), abstraction(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 86: ifeq(tuple(entity(X), eventuality(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 88: ifeq(tuple(old(X), new(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 90: ifeq(tuple(location(X), artifact(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 92: ifeq(tuple(way(X), instrumentality(X)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 93: ifeq2(location(skc5), location(skc7), location(skc7), location(skc7)) -> location(skc7) % 3.36/3.35 94: ifeq2(nonhuman(skc7), location(skc7), location(skc7), location(skc7)) -> location(skc7) % 3.36/3.35 96: ifeq2(of(X, Y), location(skc7), have(skf1(X, Y), Y, X), location(skc7)) -> location(skc7) % 3.36/3.35 97: ifeq2(nonhuman(skc5), location(skc7), location(skc7), location(skc7)) -> location(skc7) % 3.36/3.35 99: ifeq3(partof(X, Y), location(skc7), ifeq3(partof(X, Z), location(skc7), Y, Z), Z) -> Z % 3.36/3.35 100: ifeq2(way(skc4), location(skc7), location(skc7), location(skc7)) -> location(skc7) % 3.36/3.35 102: ifeq2(of(X, Y), location(skc7), ifeq2(owner(X), location(skc7), human(X), location(skc7)), location(skc7)) -> location(skc7) % 3.36/3.35 103: ifeq2(location(skc4), location(skc7), location(skc7), location(skc7)) -> location(skc7) % 3.36/3.35 104: ifeq2(nonhuman(skc4), location(skc7), location(skc7), location(skc7)) -> location(skc7) % 3.36/3.35 106: ifeq2(have(X, Y, Z), location(skc7), ifeq2(human(Y), location(skc7), owner(Y), location(skc7)), location(skc7)) -> location(skc7) % 3.36/3.35 107: ifeq(tuple(location(skc7), new(skc4)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 108: ifeq(tuple(location(skc7), instrumentality(skc5)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 109: ifeq(tuple(location(skc5), location(skc7)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 111: ifeq2(of(X, Y), location(skc7), ifeq2(owner(X), location(skc7), have(Z, X, Y), location(skc7)), location(skc7)) -> location(skc7) % 3.36/3.35 112: ifeq(tuple(location(skc7), abstraction(skc6)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 113: ifeq(tuple(entity(skc6), location(skc7)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 115: ifeq2(have(X, Y, Z), location(skc7), ifeq2(human(Y), location(skc7), of(Y, Z), location(skc7)), location(skc7)) -> location(skc7) % 3.36/3.35 117: ifeq2(have(X, Y, Z), location(skc7), ifeq2(event(X), location(skc7), of(Y, Z), location(skc7)), location(skc7)) -> location(skc7) % 3.36/3.35 118: ifeq2(have(skc6, X, Y), location(skc7), of(X, Y), location(skc7)) -> location(skc7) % 3.36/3.35 119: ifeq2(have(skf1(X, Y), Z, W), location(skc7), of(Z, W), location(skc7)) -> location(skc7) % 3.36/3.35 120: ifeq3(partof(X, ifeq3(partof(X, Y), location(skc7), Y, Y)), location(skc7), Y, Y) -> Y % 3.36/3.35 121: ifeq(tuple(location(skc7), abstraction(skc7)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 122: ifeq(tuple(location(skc7), eventuality(skc7)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 123: ifeq(tuple(location(skc7), eventuality(skc5)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 124: ifeq(tuple(way(skc4), location(skc7)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 125: ifeq(tuple(location(skc7), abstraction(skc5)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 126: ifeq(tuple(location(skc7), abstraction(skf1(X, Y))), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 127: ifeq(tuple(location(skc4), location(skc7)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 128: ifeq(tuple(entity(skf1(X, Y)), location(skc7)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 129: ifeq(tuple(location(skc7), eventuality(skc4)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 130: ifeq(tuple(location(skc7), abstraction(skc4)), tuple(location(skc7), location(skc7)), a, b) -> b % 3.36/3.35 132: ifeq2(have(X, Y, Z), location(skc7), ifeq2(nonhuman(Y), location(skc7), ifeq2(nonhuman(Z), location(skc7), partof(Z, Y), location(skc7)), location(skc7)), location(skc7)) -> location(skc7) % 3.36/3.35 %------------------------------------------------------------------------------