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