%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP110-10 : TPTP v9.0.0. Released v7.3.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:43 AM UTC 2025 % Result : Satisfiable 4.49s 4.37s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP110-10 : TPTP v9.0.0. Released v7.3.0. % 0.03/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.34 % Computer : n001.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Mon Jul 14 14:15:34 EDT 2025 % 0.12/0.34 % CPUTime : % 4.49/4.37 % SZS status Satisfiable % 4.49/4.37 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 4.49/4.37 1: actual_world(skc4) -> true % 4.49/4.37 2: coffee(skc4, skc8) -> true % 4.49/4.37 3: human_person(skc4, skc6) -> true % 4.49/4.37 4: event(skc4, skc5) -> true % 4.49/4.37 5: past(skc4, skc5) -> true % 4.49/4.37 6: nonreflexive(skc4, skc5) -> true % 4.49/4.37 7: drink(skc4, skc5) -> true % 4.49/4.37 8: agent(skc4, skc5, skc6) -> true % 4.49/4.37 9: patient(skc4, skc5, skc8) -> true % 4.49/4.37 10: ifeq2(X, X, Y, Z) -> Y % 4.49/4.37 11: ifeq3(X, X, Y, Z) -> Y % 4.49/4.37 12: ifeq(X, X, Y, Z) -> Y % 4.49/4.37 13: ifeq3(artifact(X, Y), true, object(X, Y), true) -> true % 4.49/4.37 14: ifeq3(restaurant(X, Y), true, building(X, Y), true) -> true % 4.49/4.37 15: ifeq3(customer(X, Y), true, human_person(X, Y), true) -> true % 4.49/4.37 16: ifeq3(customer(skc4, skc6), true, true, true) -> true % 4.49/4.37 17: ifeq3(building(X, Y), true, artifact(X, Y), true) -> true % 4.49/4.37 18: ifeq3(human_person(X, Y), true, organism(X, Y), true) -> true % 4.49/4.37 19: true -> organism(skc4, skc6) % 4.49/4.37 21: ifeq3(object(X, Y), organism(skc4, skc6), impartial(X, Y), organism(skc4, skc6)) -> organism(skc4, skc6) % 4.49/4.37 23: ifeq3(object(X, Y), organism(skc4, skc6), unisex(X, Y), organism(skc4, skc6)) -> organism(skc4, skc6) % 4.49/4.37 25: ifeq3(organism(X, Y), organism(skc4, skc6), entity(X, Y), organism(skc4, skc6)) -> organism(skc4, skc6) % 4.49/4.37 26: organism(skc4, skc6) -> entity(skc4, skc6) % 4.49/4.37 28: ifeq3(organism(X, Y), entity(skc4, skc6), living(X, Y), entity(skc4, skc6)) -> entity(skc4, skc6) % 4.49/4.37 29: entity(skc4, skc6) -> living(skc4, skc6) % 4.49/4.37 31: ifeq3(organism(X, Y), living(skc4, skc6), impartial(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 32: impartial(skc4, skc6) -> living(skc4, skc6) % 4.49/4.37 34: ifeq3(human_person(X, Y), living(skc4, skc6), human(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 35: human(skc4, skc6) -> living(skc4, skc6) % 4.49/4.37 37: ifeq3(object(X, Y), living(skc4, skc6), nonliving(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 39: ifeq3(human_person(X, Y), living(skc4, skc6), animate(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 40: animate(skc4, skc6) -> living(skc4, skc6) % 4.49/4.37 42: ifeq3(see(X, Y), living(skc4, skc6), event(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 44: ifeq3(eventuality(X, Y), living(skc4, skc6), specific(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 46: ifeq3(thing(X, Y), living(skc4, skc6), singleton(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 48: ifeq3(event(X, Y), living(skc4, skc6), eventuality(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 49: eventuality(skc4, skc5) -> living(skc4, skc6) % 4.49/4.37 50: specific(skc4, skc5) -> living(skc4, skc6) % 4.49/4.37 52: ifeq3(eventuality(X, Y), living(skc4, skc6), thing(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 53: thing(skc4, skc5) -> living(skc4, skc6) % 4.49/4.37 54: singleton(skc4, skc5) -> living(skc4, skc6) % 4.49/4.37 56: ifeq3(eventuality(X, Y), living(skc4, skc6), nonexistent(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 57: nonexistent(skc4, skc5) -> living(skc4, skc6) % 4.49/4.37 59: ifeq3(drink(X, Y), living(skc4, skc6), event(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 61: ifeq3(eventuality(X, Y), living(skc4, skc6), unisex(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 62: unisex(skc4, skc5) -> living(skc4, skc6) % 4.49/4.37 64: ifeq3(coffee(X, Y), living(skc4, skc6), beverage(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 65: beverage(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 67: ifeq3(substance_matter(X, Y), living(skc4, skc6), object(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 69: ifeq3(beverage(X, Y), living(skc4, skc6), food(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 70: food(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 72: ifeq3(food(X, Y), living(skc4, skc6), substance_matter(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 73: substance_matter(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 74: object(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 75: nonliving(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 76: unisex(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 77: impartial(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 79: ifeq3(object(X, Y), living(skc4, skc6), entity(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 80: entity(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 82: ifeq3(entity(X, Y), living(skc4, skc6), specific(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 83: specific(skc4, skc6) -> living(skc4, skc6) % 4.49/4.37 84: specific(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 86: ifeq3(entity(X, Y), living(skc4, skc6), thing(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 87: thing(skc4, skc6) -> living(skc4, skc6) % 4.49/4.37 88: singleton(skc4, skc6) -> living(skc4, skc6) % 4.49/4.37 89: thing(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 90: singleton(skc4, skc8) -> living(skc4, skc6) % 4.49/4.37 92: ifeq3(entity(X, Y), living(skc4, skc6), existent(X, Y), living(skc4, skc6)) -> living(skc4, skc6) % 4.49/4.37 93: living(skc4, skc6) -> existent(skc4, skc6) % 4.49/4.37 94: existent(skc4, skc8) -> existent(skc4, skc6) % 4.49/4.37 96: ifeq2(tuple2(nonliving(X, Y), living(X, Y)), tuple2(existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 98: ifeq2(tuple2(nonexistent(X, Y), existent(X, Y)), tuple2(existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 100: ifeq2(tuple2(nonliving(X, Y), animate(X, Y)), tuple2(existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 101: ifeq3(see(skc4, skc5), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 102: ifeq3(human_person(X, Y), existent(skc4, skc6), organism(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 103: ifeq3(building(X, Y), existent(skc4, skc6), artifact(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 104: ifeq3(customer(X, Y), existent(skc4, skc6), human_person(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 105: ifeq3(restaurant(X, Y), existent(skc4, skc6), building(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 106: ifeq3(artifact(X, Y), existent(skc4, skc6), object(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 107: ifeq3(object(X, Y), existent(skc4, skc6), unisex(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 108: ifeq3(organism(X, Y), existent(skc4, skc6), entity(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 109: ifeq3(object(X, Y), existent(skc4, skc6), impartial(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 110: ifeq3(organism(X, Y), existent(skc4, skc6), living(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 111: ifeq3(customer(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 112: ifeq3(object(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 113: ifeq3(object(skc4, skc5), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 114: ifeq3(entity(skc4, skc5), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 115: ifeq3(eventuality(X, Y), existent(skc4, skc6), specific(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 116: ifeq3(thing(X, Y), existent(skc4, skc6), singleton(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 117: ifeq3(see(X, Y), existent(skc4, skc6), event(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 118: ifeq3(human_person(X, Y), existent(skc4, skc6), animate(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 119: ifeq3(entity(X, Y), existent(skc4, skc6), specific(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 120: ifeq3(entity(X, Y), existent(skc4, skc6), thing(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 121: ifeq3(object(X, Y), existent(skc4, skc6), entity(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 122: ifeq3(food(X, Y), existent(skc4, skc6), substance_matter(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 123: ifeq3(coffee(X, Y), existent(skc4, skc6), beverage(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 124: ifeq3(substance_matter(X, Y), existent(skc4, skc6), object(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 125: ifeq3(beverage(X, Y), existent(skc4, skc6), food(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 126: ifeq3(eventuality(X, Y), existent(skc4, skc6), unisex(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 127: ifeq3(drink(X, Y), existent(skc4, skc6), event(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 128: ifeq3(eventuality(X, Y), existent(skc4, skc6), nonexistent(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 129: ifeq3(eventuality(X, Y), existent(skc4, skc6), thing(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 130: ifeq3(event(X, Y), existent(skc4, skc6), eventuality(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 131: ifeq3(organism(X, Y), existent(skc4, skc6), impartial(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 132: ifeq3(object(X, Y), existent(skc4, skc6), nonliving(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 133: ifeq3(human_person(X, Y), existent(skc4, skc6), human(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 134: ifeq3(entity(X, Y), existent(skc4, skc6), existent(X, Y), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 135: ifeq3(eventuality(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 136: ifeq3(artifact(skc4, skc8), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 137: ifeq3(eventuality(skc4, skc8), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 138: ifeq3(organism(skc4, skc8), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 140: ifeq(tuple(patient(X, Y, Z), nonreflexive(X, Y), agent(X, Y, Z)), tuple(existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 141: ifeq2(tuple2(nonliving(skc4, skc6), existent(skc4, skc6)), tuple2(existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 142: ifeq2(tuple2(existent(skc4, skc6), existent(skc4, skc5)), tuple2(existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 143: ifeq2(tuple2(existent(skc4, skc6), living(skc4, skc8)), tuple2(existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 144: ifeq2(tuple2(existent(skc4, skc6), animate(skc4, skc8)), tuple2(existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 145: ifeq2(tuple2(nonexistent(skc4, skc8), existent(skc4, skc6)), tuple2(existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 147: ifeq3(agent(X, Y, Z), existent(skc4, skc6), ifeq3(patient(X, Y, W), existent(skc4, skc6), ifeq3(drink(X, Y), existent(skc4, skc6), beverage(X, W), existent(skc4, skc6)), existent(skc4, skc6)), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 148: ifeq3(patient(skc4, skc5, X), existent(skc4, skc6), beverage(skc4, X), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 149: ifeq3(agent(skc4, skc5, X), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 151: ifeq3(in(skc4, X, Y), existent(skc4, skc6), ifeq3(restaurant(skc4, Y), existent(skc4, skc6), ifeq3(customer(skc4, X), existent(skc4, skc6), event(skc4, skf1(Z)), existent(skc4, skc6)), existent(skc4, skc6)), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 153: ifeq3(in(skc4, X, Y), existent(skc4, skc6), ifeq3(restaurant(skc4, Y), existent(skc4, skc6), ifeq3(customer(skc4, X), existent(skc4, skc6), nonreflexive(skc4, skf1(Z)), existent(skc4, skc6)), existent(skc4, skc6)), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 155: ifeq3(in(skc4, X, Y), existent(skc4, skc6), ifeq3(restaurant(skc4, Y), existent(skc4, skc6), ifeq3(customer(skc4, X), existent(skc4, skc6), past(skc4, skf1(Z)), existent(skc4, skc6)), existent(skc4, skc6)), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 157: ifeq3(in(skc4, X, Y), existent(skc4, skc6), ifeq3(restaurant(skc4, Y), existent(skc4, skc6), ifeq3(customer(skc4, X), existent(skc4, skc6), see(skc4, skf1(Z)), existent(skc4, skc6)), existent(skc4, skc6)), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 159: ifeq3(in(skc4, X, Y), existent(skc4, skc6), ifeq3(restaurant(skc4, Y), existent(skc4, skc6), ifeq3(customer(skc4, X), existent(skc4, skc6), agent(skc4, skf1(X), X), existent(skc4, skc6)), existent(skc4, skc6)), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 161: ifeq3(in(skc4, X, Y), existent(skc4, skc6), ifeq3(restaurant(skc4, Y), existent(skc4, skc6), ifeq3(customer(skc4, X), existent(skc4, skc6), patient(skc4, skf1(Z), skc6), existent(skc4, skc6)), existent(skc4, skc6)), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 162: ifeq(tuple(existent(skc4, skc6), existent(skc4, skc6), agent(skc4, skc5, skc8)), tuple(existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 163: ifeq(tuple(patient(skc4, skc5, skc6), existent(skc4, skc6), existent(skc4, skc6)), tuple(existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 164: ifeq(tuple(patient(skc4, skc5, X), existent(skc4, skc6), agent(skc4, skc5, X)), tuple(existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)), a, b) -> b % 4.49/4.37 165: ifeq3(agent(skc4, X, Y), existent(skc4, skc6), ifeq3(patient(skc4, X, skc8), existent(skc4, skc6), ifeq3(drink(skc4, X), existent(skc4, skc6), existent(skc4, skc6), existent(skc4, skc6)), existent(skc4, skc6)), existent(skc4, skc6)) -> existent(skc4, skc6) % 4.49/4.37 %------------------------------------------------------------------------------