%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP111-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n015.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:44 AM UTC 2025 % Result : Satisfiable 4.42s 4.36s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NLP111-10 : TPTP v9.0.0. Released v7.5.0. % 0.03/0.11 % Command : run_Leo-III %s %d THM % 0.11/0.30 % Computer : n015.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Mon Jul 14 14:15:34 EDT 2025 % 0.11/0.31 % CPUTime : % 4.42/4.36 % SZS status Satisfiable % 4.42/4.36 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 4.42/4.36 1: actual_world(skc5) -> true % 4.42/4.36 2: restaurant(skc5, skc8) -> true % 4.42/4.36 3: human_person(skc5, skc7) -> true % 4.42/4.36 4: drink(skc5, skc6) -> true % 4.42/4.36 5: nonreflexive(skc5, skc6) -> true % 4.42/4.36 6: past(skc5, skc6) -> true % 4.42/4.36 7: event(skc5, skc6) -> true % 4.42/4.36 8: coffee(skc5, skc10) -> true % 4.42/4.36 9: patient(skc5, skc6, skc10) -> true % 4.42/4.36 10: agent(skc5, skc6, skc7) -> true % 4.42/4.36 11: ifeq2(X, X, Y, Z) -> Y % 4.42/4.36 12: ifeq3(X, X, Y, Z) -> Y % 4.42/4.36 13: ifeq(X, X, Y, Z) -> Y % 4.42/4.36 14: ifeq3(restaurant(X, Y), true, building(X, Y), true) -> true % 4.42/4.36 15: building(skc5, skc8) -> true % 4.42/4.36 16: ifeq3(customer(X, Y), true, human_person(X, Y), true) -> true % 4.42/4.36 17: ifeq3(customer(skc5, skc7), true, true, true) -> true % 4.42/4.36 18: ifeq3(building(X, Y), true, artifact(X, Y), true) -> true % 4.42/4.36 19: artifact(skc5, skc8) -> true % 4.42/4.36 20: ifeq3(human_person(X, Y), true, organism(X, Y), true) -> true % 4.42/4.36 21: organism(skc5, skc7) -> true % 4.42/4.36 22: ifeq3(object(X, Y), true, unisex(X, Y), true) -> true % 4.42/4.36 23: ifeq3(object(X, Y), true, impartial(X, Y), true) -> true % 4.42/4.36 24: ifeq3(organism(X, Y), true, entity(X, Y), true) -> true % 4.42/4.36 25: entity(skc5, skc7) -> true % 4.42/4.36 26: ifeq3(organism(X, Y), true, living(X, Y), true) -> true % 4.42/4.36 27: living(skc5, skc7) -> true % 4.42/4.36 28: ifeq3(organism(X, Y), true, impartial(X, Y), true) -> true % 4.42/4.36 29: impartial(skc5, skc7) -> true % 4.42/4.36 30: ifeq3(human_person(X, Y), true, human(X, Y), true) -> true % 4.42/4.36 31: human(skc5, skc7) -> true % 4.42/4.36 32: ifeq3(artifact(X, Y), true, object(X, Y), true) -> true % 4.42/4.36 33: object(skc5, skc8) -> true % 4.42/4.36 34: impartial(skc5, skc8) -> true % 4.42/4.36 35: unisex(skc5, skc8) -> true % 4.42/4.36 36: ifeq3(object(X, Y), true, nonliving(X, Y), true) -> true % 4.42/4.36 37: nonliving(skc5, skc8) -> true % 4.42/4.36 38: ifeq3(human_person(X, Y), true, animate(X, Y), true) -> true % 4.42/4.36 39: animate(skc5, skc7) -> true % 4.42/4.36 40: ifeq3(see(X, Y), true, event(X, Y), true) -> true % 4.42/4.36 41: ifeq3(see(skc5, skc6), true, true, true) -> true % 4.42/4.36 42: ifeq3(eventuality(X, Y), true, specific(X, Y), true) -> true % 4.42/4.36 43: ifeq3(event(X, Y), true, eventuality(X, Y), true) -> true % 4.42/4.36 44: eventuality(skc5, skc6) -> true % 4.42/4.36 45: specific(skc5, skc6) -> true % 4.42/4.36 46: ifeq3(thing(X, Y), true, singleton(X, Y), true) -> true % 4.42/4.36 47: ifeq3(eventuality(X, Y), true, thing(X, Y), true) -> true % 4.42/4.36 48: thing(skc5, skc6) -> true % 4.42/4.36 49: singleton(skc5, skc6) -> true % 4.42/4.36 50: ifeq3(eventuality(X, Y), true, nonexistent(X, Y), true) -> true % 4.42/4.36 51: nonexistent(skc5, skc6) -> true % 4.42/4.36 52: ifeq3(drink(X, Y), true, event(X, Y), true) -> true % 4.42/4.36 53: ifeq3(eventuality(X, Y), true, unisex(X, Y), true) -> true % 4.42/4.36 54: unisex(skc5, skc6) -> true % 4.42/4.36 55: ifeq3(coffee(X, Y), true, beverage(X, Y), true) -> true % 4.42/4.36 56: true -> beverage(skc5, skc10) % 4.42/4.36 58: ifeq3(substance_matter(X, Y), beverage(skc5, skc10), object(X, Y), beverage(skc5, skc10)) -> beverage(skc5, skc10) % 4.42/4.36 60: ifeq3(beverage(X, Y), beverage(skc5, skc10), food(X, Y), beverage(skc5, skc10)) -> beverage(skc5, skc10) % 4.42/4.36 61: food(skc5, skc10) -> beverage(skc5, skc10) % 4.42/4.36 63: ifeq3(food(X, Y), beverage(skc5, skc10), substance_matter(X, Y), beverage(skc5, skc10)) -> beverage(skc5, skc10) % 4.42/4.36 64: substance_matter(skc5, skc10) -> beverage(skc5, skc10) % 4.42/4.36 65: beverage(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 67: ifeq3(object(X, Y), object(skc5, skc10), entity(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 68: entity(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 69: entity(skc5, skc8) -> object(skc5, skc10) % 4.42/4.36 71: ifeq3(entity(X, Y), object(skc5, skc10), specific(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 72: specific(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 73: specific(skc5, skc7) -> object(skc5, skc10) % 4.42/4.36 74: specific(skc5, skc8) -> object(skc5, skc10) % 4.42/4.36 76: ifeq3(entity(X, Y), object(skc5, skc10), thing(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 77: thing(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 78: singleton(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 79: thing(skc5, skc7) -> object(skc5, skc10) % 4.42/4.36 80: singleton(skc5, skc7) -> object(skc5, skc10) % 4.42/4.36 81: thing(skc5, skc8) -> object(skc5, skc10) % 4.42/4.36 82: singleton(skc5, skc8) -> object(skc5, skc10) % 4.42/4.36 84: ifeq3(entity(X, Y), object(skc5, skc10), existent(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 85: existent(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 86: existent(skc5, skc7) -> object(skc5, skc10) % 4.42/4.36 87: existent(skc5, skc8) -> object(skc5, skc10) % 4.42/4.36 88: ifeq3(object(skc5, skc6), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 89: ifeq3(object(skc5, skc7), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 90: ifeq3(organism(skc5, skc8), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 91: ifeq3(eventuality(skc5, skc8), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 93: ifeq2(tuple2(nonliving(X, Y), living(X, Y)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 95: ifeq2(tuple2(nonexistent(X, Y), existent(X, Y)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 97: ifeq2(tuple2(nonliving(X, Y), animate(X, Y)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 98: ifeq3(building(X, Y), object(skc5, skc10), artifact(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 99: ifeq3(human_person(X, Y), object(skc5, skc10), organism(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 100: ifeq3(coffee(X, Y), object(skc5, skc10), beverage(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 101: ifeq3(eventuality(X, Y), object(skc5, skc10), unisex(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 102: ifeq3(drink(X, Y), object(skc5, skc10), event(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 103: ifeq3(object(X, Y), object(skc5, skc10), unisex(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 104: unisex(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 105: ifeq3(restaurant(X, Y), object(skc5, skc10), building(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 106: ifeq3(customer(X, Y), object(skc5, skc10), human_person(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 107: ifeq3(thing(X, Y), object(skc5, skc10), singleton(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 108: ifeq3(eventuality(X, Y), object(skc5, skc10), thing(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 109: ifeq3(eventuality(X, Y), object(skc5, skc10), nonexistent(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 110: ifeq3(event(X, Y), object(skc5, skc10), eventuality(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 111: ifeq3(eventuality(X, Y), object(skc5, skc10), specific(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 112: ifeq3(see(X, Y), object(skc5, skc10), event(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 113: ifeq3(human_person(X, Y), object(skc5, skc10), animate(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 114: ifeq3(artifact(X, Y), object(skc5, skc10), object(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 115: ifeq3(object(X, Y), object(skc5, skc10), nonliving(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 116: nonliving(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 117: ifeq3(human_person(X, Y), object(skc5, skc10), human(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 118: ifeq3(organism(X, Y), object(skc5, skc10), impartial(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 119: ifeq3(organism(X, Y), object(skc5, skc10), living(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 120: ifeq3(organism(X, Y), object(skc5, skc10), entity(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 121: ifeq3(object(X, Y), object(skc5, skc10), impartial(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 122: impartial(skc5, skc10) -> object(skc5, skc10) % 4.42/4.36 123: ifeq3(see(skc5, skc6), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 124: ifeq3(organism(skc5, skc10), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 125: ifeq3(customer(skc5, skc7), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 126: ifeq3(substance_matter(X, Y), object(skc5, skc10), object(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 127: ifeq3(beverage(X, Y), object(skc5, skc10), food(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 128: ifeq3(food(X, Y), object(skc5, skc10), substance_matter(X, Y), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 129: ifeq3(entity(skc5, skc6), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 130: ifeq3(eventuality(skc5, skc10), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 131: ifeq3(eventuality(skc5, skc7), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 132: ifeq3(substance_matter(skc5, skc8), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 134: ifeq3(in(skc5, X, skc8), object(skc5, skc10), ifeq3(customer(skc5, X), object(skc5, skc10), past(skc5, skf1(Y)), object(skc5, skc10)), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 136: ifeq3(in(skc5, X, skc8), object(skc5, skc10), ifeq3(customer(skc5, X), object(skc5, skc10), nonreflexive(skc5, skf1(Y)), object(skc5, skc10)), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 138: ifeq3(in(skc5, X, skc8), object(skc5, skc10), ifeq3(customer(skc5, X), object(skc5, skc10), event(skc5, skf1(Y)), object(skc5, skc10)), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 140: ifeq3(in(skc5, X, skc8), object(skc5, skc10), ifeq3(customer(skc5, X), object(skc5, skc10), see(skc5, skf1(Y)), object(skc5, skc10)), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 142: ifeq3(in(skc5, X, skc8), object(skc5, skc10), ifeq3(customer(skc5, X), object(skc5, skc10), agent(skc5, skf1(X), X), object(skc5, skc10)), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 144: ifeq3(in(skc5, X, skc8), object(skc5, skc10), ifeq3(customer(skc5, X), object(skc5, skc10), patient(skc5, skf1(Y), skc7), object(skc5, skc10)), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 146: ifeq(tuple(patient(X, Y, Z), nonreflexive(X, Y), agent(X, Y, Z)), tuple(object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 147: ifeq2(tuple2(nonliving(skc5, skc7), object(skc5, skc10)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 148: ifeq2(tuple2(object(skc5, skc10), existent(skc5, skc6)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 149: ifeq2(tuple2(nonexistent(skc5, skc10), object(skc5, skc10)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 150: ifeq2(tuple2(nonexistent(skc5, skc7), object(skc5, skc10)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 151: ifeq2(tuple2(object(skc5, skc10), animate(skc5, skc10)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 152: ifeq2(tuple2(object(skc5, skc10), living(skc5, skc10)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 153: ifeq2(tuple2(object(skc5, skc10), living(skc5, skc8)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 154: ifeq2(tuple2(object(skc5, skc10), animate(skc5, skc8)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 155: ifeq2(tuple2(nonexistent(skc5, skc8), object(skc5, skc10)), tuple2(object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 157: ifeq3(agent(X, Y, Z), object(skc5, skc10), ifeq3(patient(X, Y, W), object(skc5, skc10), ifeq3(drink(X, Y), object(skc5, skc10), beverage(X, W), object(skc5, skc10)), object(skc5, skc10)), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 158: ifeq3(patient(skc5, skc6, X), object(skc5, skc10), beverage(skc5, X), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 159: ifeq3(agent(skc5, skc6, X), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 160: ifeq(tuple(object(skc5, skc10), object(skc5, skc10), agent(skc5, skc6, skc10)), tuple(object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 161: ifeq(tuple(patient(skc5, skc6, skc7), object(skc5, skc10), object(skc5, skc10)), tuple(object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 162: ifeq(tuple(patient(skc5, skc6, X), object(skc5, skc10), agent(skc5, skc6, X)), tuple(object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)), a, b) -> b % 4.42/4.36 163: ifeq3(agent(skc5, X, Y), object(skc5, skc10), ifeq3(patient(skc5, X, skc10), object(skc5, skc10), ifeq3(drink(skc5, X), object(skc5, skc10), object(skc5, skc10), object(skc5, skc10)), object(skc5, skc10)), object(skc5, skc10)) -> object(skc5, skc10) % 4.42/4.36 %------------------------------------------------------------------------------