%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP112-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n011.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.62s 4.51s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP112-10 : TPTP v9.0.0. Released v7.5.0. % 0.11/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.33 % Computer : n011.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:15:49 EDT 2025 % 0.12/0.33 % CPUTime : % 4.62/4.51 % SZS status Satisfiable % 4.62/4.51 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 4.62/4.51 1: actual_world(skc5) -> true % 4.62/4.51 2: coffee(skc5, skc10) -> true % 4.62/4.51 3: human_person(skc5, skc8) -> true % 4.62/4.51 4: event(skc5, skc7) -> true % 4.62/4.51 5: past(skc5, skc7) -> true % 4.62/4.51 6: nonreflexive(skc5, skc7) -> true % 4.62/4.51 7: drink(skc5, skc7) -> true % 4.62/4.51 8: restaurant(skc5, skc6) -> true % 4.62/4.51 9: agent(skc5, skc7, skc8) -> true % 4.62/4.51 10: patient(skc5, skc7, skc10) -> true % 4.62/4.51 11: ifeq2(X, X, Y, Z) -> Y % 4.62/4.51 12: ifeq3(X, X, Y, Z) -> Y % 4.62/4.51 13: ifeq(X, X, Y, Z) -> Y % 4.62/4.51 14: ifeq3(restaurant(X, Y), true, building(X, Y), true) -> true % 4.62/4.51 15: building(skc5, skc6) -> true % 4.62/4.51 16: ifeq3(customer(X, Y), true, human_person(X, Y), true) -> true % 4.62/4.51 17: ifeq3(customer(skc5, skc8), true, true, true) -> true % 4.62/4.51 18: ifeq3(building(X, Y), true, artifact(X, Y), true) -> true % 4.62/4.51 19: artifact(skc5, skc6) -> true % 4.62/4.51 20: ifeq3(human_person(X, Y), true, organism(X, Y), true) -> true % 4.62/4.51 21: organism(skc5, skc8) -> true % 4.62/4.51 22: ifeq3(object(X, Y), true, unisex(X, Y), true) -> true % 4.62/4.51 23: ifeq3(object(X, Y), true, impartial(X, Y), true) -> true % 4.62/4.51 24: ifeq3(organism(X, Y), true, entity(X, Y), true) -> true % 4.62/4.51 25: entity(skc5, skc8) -> true % 4.62/4.51 26: ifeq3(organism(X, Y), true, living(X, Y), true) -> true % 4.62/4.51 27: living(skc5, skc8) -> true % 4.62/4.51 28: ifeq3(organism(X, Y), true, impartial(X, Y), true) -> true % 4.62/4.51 29: impartial(skc5, skc8) -> true % 4.62/4.51 30: ifeq3(human_person(X, Y), true, human(X, Y), true) -> true % 4.62/4.51 31: human(skc5, skc8) -> true % 4.62/4.51 32: ifeq3(artifact(X, Y), true, object(X, Y), true) -> true % 4.62/4.51 33: object(skc5, skc6) -> true % 4.62/4.51 34: impartial(skc5, skc6) -> true % 4.62/4.51 35: unisex(skc5, skc6) -> true % 4.62/4.51 36: ifeq3(object(X, Y), true, nonliving(X, Y), true) -> true % 4.62/4.51 37: nonliving(skc5, skc6) -> true % 4.62/4.51 38: ifeq3(human_person(X, Y), true, animate(X, Y), true) -> true % 4.62/4.51 39: animate(skc5, skc8) -> true % 4.62/4.51 40: ifeq3(see(X, Y), true, event(X, Y), true) -> true % 4.62/4.51 41: ifeq3(see(skc5, skc7), true, true, true) -> true % 4.62/4.51 42: ifeq3(eventuality(X, Y), true, specific(X, Y), true) -> true % 4.62/4.51 43: ifeq3(event(X, Y), true, eventuality(X, Y), true) -> true % 4.62/4.51 44: eventuality(skc5, skc7) -> true % 4.62/4.51 45: specific(skc5, skc7) -> true % 4.62/4.51 46: ifeq3(thing(X, Y), true, singleton(X, Y), true) -> true % 4.62/4.51 47: ifeq3(eventuality(X, Y), true, thing(X, Y), true) -> true % 4.62/4.51 48: thing(skc5, skc7) -> true % 4.62/4.51 49: singleton(skc5, skc7) -> true % 4.62/4.51 50: ifeq3(eventuality(X, Y), true, nonexistent(X, Y), true) -> true % 4.62/4.51 51: nonexistent(skc5, skc7) -> true % 4.62/4.51 52: ifeq3(drink(X, Y), true, event(X, Y), true) -> true % 4.62/4.51 53: ifeq3(eventuality(X, Y), true, unisex(X, Y), true) -> true % 4.62/4.51 54: unisex(skc5, skc7) -> true % 4.62/4.51 55: ifeq3(coffee(X, Y), true, beverage(X, Y), true) -> true % 4.62/4.51 56: beverage(skc5, skc10) -> true % 4.62/4.51 57: ifeq3(substance_matter(X, Y), true, object(X, Y), true) -> true % 4.62/4.51 58: ifeq3(beverage(X, Y), true, food(X, Y), true) -> true % 4.62/4.51 59: food(skc5, skc10) -> true % 4.62/4.51 60: ifeq3(food(X, Y), true, substance_matter(X, Y), true) -> true % 4.62/4.51 61: substance_matter(skc5, skc10) -> true % 4.62/4.51 62: object(skc5, skc10) -> true % 4.62/4.51 63: nonliving(skc5, skc10) -> true % 4.62/4.51 64: impartial(skc5, skc10) -> true % 4.62/4.51 65: unisex(skc5, skc10) -> true % 4.62/4.51 66: ifeq3(object(X, Y), true, entity(X, Y), true) -> true % 4.62/4.51 67: entity(skc5, skc6) -> true % 4.62/4.51 68: entity(skc5, skc10) -> true % 4.62/4.51 69: ifeq3(entity(X, Y), true, specific(X, Y), true) -> true % 4.62/4.51 70: specific(skc5, skc8) -> true % 4.62/4.51 71: specific(skc5, skc6) -> true % 4.62/4.51 72: specific(skc5, skc10) -> true % 4.62/4.51 73: ifeq3(entity(X, Y), true, thing(X, Y), true) -> true % 4.62/4.51 74: thing(skc5, skc8) -> true % 4.62/4.51 75: singleton(skc5, skc8) -> true % 4.62/4.51 76: thing(skc5, skc6) -> true % 4.62/4.51 77: singleton(skc5, skc6) -> true % 4.62/4.51 78: thing(skc5, skc10) -> true % 4.62/4.51 79: singleton(skc5, skc10) -> true % 4.62/4.51 80: ifeq3(entity(X, Y), true, existent(X, Y), true) -> true % 4.62/4.51 81: existent(skc5, skc8) -> true % 4.62/4.51 82: existent(skc5, skc6) -> true % 4.62/4.51 83: existent(skc5, skc10) -> true % 4.62/4.51 84: ifeq3(entity(skc5, skc7), true, true, true) -> true % 4.62/4.51 85: ifeq3(object(skc5, skc8), true, true, true) -> true % 4.62/4.51 86: ifeq3(object(skc5, skc7), true, true, true) -> true % 4.62/4.51 87: ifeq3(substance_matter(skc5, skc6), true, true, true) -> true % 4.62/4.51 88: ifeq3(eventuality(skc5, skc8), true, true, true) -> true % 4.62/4.51 89: ifeq3(artifact(skc5, skc10), true, true, true) -> true % 4.62/4.51 90: ifeq3(eventuality(skc5, skc6), true, true, true) -> true % 4.62/4.51 91: ifeq3(organism(skc5, skc6), true, true, true) -> true % 4.62/4.51 92: ifeq3(eventuality(skc5, skc10), true, true, true) -> true % 4.62/4.51 93: ifeq3(organism(skc5, skc10), true, true, true) -> true % 4.62/4.51 94: ifeq2(tuple2(nonliving(X, Y), living(X, Y)), tuple2(true, true), a, b) -> b % 4.62/4.51 95: ifeq2(tuple2(nonexistent(X, Y), existent(X, Y)), tuple2(true, true), a, b) -> b % 4.62/4.51 96: ifeq2(tuple2(nonliving(X, Y), animate(X, Y)), tuple2(true, true), a, b) -> b % 4.62/4.51 97: ifeq2(tuple2(nonliving(skc5, skc8), true), tuple2(true, true), a, b) -> b % 4.62/4.51 98: ifeq2(tuple2(true, existent(skc5, skc7)), tuple2(true, true), a, b) -> b % 4.62/4.51 99: ifeq2(tuple2(nonexistent(skc5, skc8), true), tuple2(true, true), a, b) -> b % 4.62/4.51 100: ifeq2(tuple2(true, animate(skc5, skc6)), tuple2(true, true), a, b) -> b % 4.62/4.51 101: ifeq2(tuple2(true, living(skc5, skc6)), tuple2(true, true), a, b) -> b % 4.62/4.51 102: ifeq2(tuple2(true, animate(skc5, skc10)), tuple2(true, true), a, b) -> b % 4.62/4.51 103: ifeq2(tuple2(nonexistent(skc5, skc6), true), tuple2(true, true), a, b) -> b % 4.62/4.51 104: ifeq2(tuple2(true, living(skc5, skc10)), tuple2(true, true), a, b) -> b % 4.62/4.51 105: ifeq2(tuple2(nonexistent(skc5, skc10), true), tuple2(true, true), a, b) -> b % 4.62/4.51 106: ifeq3(in(skc5, X, skc6), true, ifeq3(customer(skc5, X), true, see(skc5, skf1(Y)), true), true) -> true % 4.62/4.51 107: ifeq3(in(skc5, X, skc6), true, ifeq3(customer(skc5, X), true, past(skc5, skf1(Y)), true), true) -> true % 4.62/4.51 108: ifeq3(in(skc5, X, skc6), true, ifeq3(customer(skc5, X), true, nonreflexive(skc5, skf1(Y)), true), true) -> true % 4.62/4.51 109: ifeq3(in(skc5, X, skc6), true, ifeq3(customer(skc5, X), true, event(skc5, skf1(Y)), true), true) -> true % 4.62/4.51 110: ifeq3(in(skc5, X, skc6), true, ifeq3(customer(skc5, X), true, agent(skc5, skf1(X), X), true), true) -> true % 4.62/4.51 111: ifeq3(in(skc5, X, skc6), true, ifeq3(customer(skc5, X), true, patient(skc5, skf1(Y), skc8), true), true) -> true % 4.62/4.51 112: ifeq(tuple(patient(X, Y, Z), nonreflexive(X, Y), agent(X, Y, Z)), tuple(true, true, true), a, b) -> b % 4.62/4.51 113: ifeq(tuple(true, true, agent(skc5, skc7, skc10)), tuple(true, true, true), a, b) -> b % 4.62/4.51 114: ifeq(tuple(patient(skc5, skc7, skc8), true, true), tuple(true, true, true), a, b) -> b % 4.62/4.51 115: ifeq(tuple(patient(skc5, skc7, X), true, agent(skc5, skc7, X)), tuple(true, true, true), a, b) -> b % 4.62/4.51 116: ifeq3(agent(X, Y, Z), true, ifeq3(patient(X, Y, W), true, ifeq3(drink(X, Y), true, beverage(X, W), true), true), true) -> true % 4.62/4.51 117: ifeq3(agent(skc5, skc7, X), true, true, true) -> true % 4.62/4.51 118: ifeq3(patient(skc5, skc7, X), true, beverage(skc5, X), true) -> true % 4.62/4.51 119: ifeq3(agent(skc5, X, Y), true, ifeq3(patient(skc5, X, skc10), true, ifeq3(drink(skc5, X), true, true, true), true), true) -> true % 4.62/4.51 %------------------------------------------------------------------------------