%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP128-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n003.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:46 AM UTC 2025 % Result : Satisfiable 3.03s 3.03s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP128-10 : TPTP v9.0.0. Released v7.3.0. % 0.06/0.12 % Command : run_Leo-III %s %d THM % 0.11/0.33 % Computer : n003.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Mon Jul 14 14:16:34 EDT 2025 % 0.11/0.33 % CPUTime : % 3.03/3.03 % SZS status Satisfiable % 3.03/3.03 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 3.03/3.03 1: actual_world(skc5) -> true % 3.03/3.03 2: hollywood_placename(skc5, skc9) -> true % 3.03/3.03 3: placename(skc5, skc9) -> true % 3.03/3.03 4: street(skc5, skc7) -> true % 3.03/3.03 5: lonely(skc5, skc7) -> true % 3.03/3.03 6: barrel(skc5, skc6) -> true % 3.03/3.03 7: present(skc5, skc6) -> true % 3.03/3.03 8: event(skc5, skc6) -> true % 3.03/3.03 9: old(skc5, skc8) -> true % 3.03/3.03 10: dirty(skc5, skc8) -> true % 3.03/3.03 11: white(skc5, skc8) -> true % 3.03/3.03 12: chevy(skc5, skc8) -> true % 3.03/3.03 13: city(skc5, skc8) -> true % 3.03/3.03 14: of(skc5, skc9, skc8) -> true % 3.03/3.03 15: down(skc5, skc6, skc7) -> true % 3.03/3.03 16: in(skc5, skc6, skc8) -> true % 3.03/3.03 17: agent(skc5, skc6, skc8) -> true % 3.03/3.03 18: ifeq2(X, X, Y, Z) -> Y % 3.03/3.03 19: ifeq3(X, X, Y, Z) -> Y % 3.03/3.03 20: ifeq(X, X, Y, Z) -> Y % 3.03/3.03 21: ifeq2(event(X, Y), true, eventuality(X, Y), true) -> true % 3.03/3.03 22: eventuality(skc5, skc6) -> true % 3.03/3.03 23: ifeq2(barrel(X, Y), true, event(X, Y), true) -> true % 3.03/3.03 24: ifeq2(eventuality(X, Y), true, thing(X, Y), true) -> true % 3.03/3.03 25: thing(skc5, skc6) -> true % 3.03/3.03 26: ifeq2(instrumentality(X, Y), true, artifact(X, Y), true) -> true % 3.03/3.03 27: ifeq2(abstraction(X, Y), true, general(X, Y), true) -> true % 3.03/3.03 28: ifeq2(abstraction(X, Y), true, thing(X, Y), true) -> true % 3.03/3.03 29: ifeq2(abstraction(X, Y), true, nonhuman(X, Y), true) -> true % 3.03/3.03 30: ifeq2(abstraction(X, Y), true, unisex(X, Y), true) -> true % 3.03/3.03 31: ifeq2(city(X, Y), true, location(X, Y), true) -> true % 3.03/3.03 32: location(skc5, skc8) -> true % 3.03/3.03 33: ifeq2(hollywood_placename(X, Y), true, placename(X, Y), true) -> true % 3.03/3.03 34: ifeq2(location(X, Y), true, object(X, Y), true) -> true % 3.03/3.03 35: object(skc5, skc8) -> true % 3.03/3.03 36: ifeq2(vehicle(X, Y), true, transport(X, Y), true) -> true % 3.03/3.03 37: ifeq2(car(X, Y), true, vehicle(X, Y), true) -> true % 3.03/3.03 38: ifeq2(transport(X, Y), true, instrumentality(X, Y), true) -> true % 3.03/3.03 39: ifeq2(relation(X, Y), true, abstraction(X, Y), true) -> true % 3.03/3.03 40: ifeq2(chevy(X, Y), true, car(X, Y), true) -> true % 3.03/3.03 41: car(skc5, skc8) -> true % 3.03/3.03 42: vehicle(skc5, skc8) -> true % 3.03/3.03 43: transport(skc5, skc8) -> true % 3.03/3.03 44: instrumentality(skc5, skc8) -> true % 3.03/3.03 45: artifact(skc5, skc8) -> true % 3.03/3.03 46: ifeq2(thing(X, Y), true, singleton(X, Y), true) -> true % 3.03/3.03 47: singleton(skc5, skc6) -> true % 3.03/3.03 48: ifeq2(street(X, Y), true, way(X, Y), true) -> true % 3.03/3.03 49: way(skc5, skc7) -> true % 3.03/3.03 50: ifeq2(eventuality(X, Y), true, nonexistent(X, Y), true) -> true % 3.03/3.03 51: nonexistent(skc5, skc6) -> true % 3.03/3.03 52: ifeq2(eventuality(X, Y), true, unisex(X, Y), true) -> true % 3.03/3.03 53: unisex(skc5, skc6) -> true % 3.03/3.03 54: ifeq2(eventuality(X, Y), true, specific(X, Y), true) -> true % 3.03/3.03 55: specific(skc5, skc6) -> true % 3.03/3.03 56: ifeq2(way(X, Y), true, artifact(X, Y), true) -> true % 3.03/3.03 57: artifact(skc5, skc7) -> true % 3.03/3.03 58: ifeq2(object(X, Y), true, entity(X, Y), true) -> true % 3.03/3.03 59: entity(skc5, skc8) -> true % 3.03/3.03 60: ifeq2(artifact(X, Y), true, object(X, Y), true) -> true % 3.03/3.03 61: object(skc5, skc7) -> true % 3.03/3.03 62: entity(skc5, skc7) -> true % 3.03/3.03 63: ifeq2(entity(X, Y), true, thing(X, Y), true) -> true % 3.03/3.03 64: thing(skc5, skc8) -> true % 3.03/3.03 65: singleton(skc5, skc8) -> true % 3.03/3.03 66: thing(skc5, skc7) -> true % 3.03/3.03 67: singleton(skc5, skc7) -> true % 3.03/3.03 68: ifeq2(object(X, Y), true, nonliving(X, Y), true) -> true % 3.03/3.03 69: nonliving(skc5, skc8) -> true % 3.03/3.03 70: nonliving(skc5, skc7) -> true % 3.03/3.03 71: ifeq2(entity(X, Y), true, existent(X, Y), true) -> true % 3.03/3.03 72: existent(skc5, skc8) -> true % 3.03/3.03 73: existent(skc5, skc7) -> true % 3.03/3.03 74: ifeq2(entity(X, Y), true, specific(X, Y), true) -> true % 3.03/3.03 75: specific(skc5, skc8) -> true % 3.03/3.03 76: specific(skc5, skc7) -> true % 3.03/3.03 77: ifeq2(object(X, Y), true, impartial(X, Y), true) -> true % 3.03/3.03 78: impartial(skc5, skc8) -> true % 3.03/3.03 79: impartial(skc5, skc7) -> true % 3.03/3.03 80: ifeq2(placename(X, Y), true, relname(X, Y), true) -> true % 3.03/3.03 81: relname(skc5, skc9) -> true % 3.03/3.03 82: ifeq2(object(X, Y), true, unisex(X, Y), true) -> true % 3.03/3.03 83: unisex(skc5, skc8) -> true % 3.03/3.03 84: unisex(skc5, skc7) -> true % 3.03/3.03 85: ifeq2(relname(X, Y), true, relation(X, Y), true) -> true % 3.03/3.03 86: relation(skc5, skc9) -> true % 3.03/3.03 87: abstraction(skc5, skc9) -> true % 3.03/3.03 88: unisex(skc5, skc9) -> true % 3.03/3.03 89: nonhuman(skc5, skc9) -> true % 3.03/3.03 90: thing(skc5, skc9) -> true % 3.03/3.03 91: general(skc5, skc9) -> true % 3.03/3.03 92: singleton(skc5, skc9) -> true % 3.03/3.03 93: ifeq2(object(skc5, skc6), true, true, true) -> true % 3.03/3.03 94: ifeq2(instrumentality(skc5, skc7), true, true, true) -> true % 3.03/3.03 95: ifeq2(abstraction(skc5, skc6), true, true, true) -> true % 3.03/3.03 96: ifeq2(entity(skc5, skc6), true, true, true) -> true % 3.03/3.03 97: ifeq2(location(skc5, skc7), true, true, true) -> true % 3.03/3.03 98: ifeq2(eventuality(skc5, skc8), true, true, true) -> true % 3.03/3.03 99: ifeq2(abstraction(skc5, skc8), true, true, true) -> true % 3.03/3.03 100: ifeq2(object(skc5, skc9), true, true, true) -> true % 3.03/3.03 101: ifeq2(entity(skc5, skc9), true, true, true) -> true % 3.03/3.03 102: ifeq2(eventuality(skc5, skc9), true, true, true) -> true % 3.03/3.03 103: ifeq2(eventuality(skc5, skc7), true, true, true) -> true % 3.03/3.03 104: ifeq2(abstraction(skc5, skc7), true, true, true) -> true % 3.03/3.03 105: ifeq2(way(skc5, skc8), true, true, true) -> true % 3.03/3.03 106: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(true, true), a, b) -> b % 3.03/3.03 107: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(true, true), a, b) -> b % 3.03/3.03 108: ifeq(tuple(true, existent(skc5, skc6)), tuple(true, true), a, b) -> b % 3.03/3.03 109: ifeq(tuple(true, general(skc5, skc6)), tuple(true, true), a, b) -> b % 3.03/3.03 110: ifeq(tuple(nonexistent(skc5, skc8), true), tuple(true, true), a, b) -> b % 3.03/3.03 111: ifeq(tuple(specific(skc5, skc9), true), tuple(true, true), a, b) -> b % 3.03/3.03 112: ifeq(tuple(true, general(skc5, skc8)), tuple(true, true), a, b) -> b % 3.03/3.03 113: ifeq(tuple(nonexistent(skc5, skc7), true), tuple(true, true), a, b) -> b % 3.03/3.03 114: ifeq(tuple(true, general(skc5, skc7)), tuple(true, true), a, b) -> b % 3.03/3.03 115: ifeq3(of(X, Y, Z), true, ifeq3(of(X, W, Z), true, ifeq3(placename(X, Y), true, ifeq3(placename(X, W), true, ifeq3(entity(X, Z), true, Y, W), W), W), W), W) -> W % 3.03/3.03 116: ifeq3(of(skc5, X, skc8), true, ifeq3(placename(skc5, X), true, skc9, X), X) -> X % 3.03/3.03 117: ifeq3(of(skc5, X, skc8), true, ifeq3(placename(skc5, X), true, X, skc9), skc9) -> skc9 % 3.03/3.03 118: ifeq3(of(skc5, skc9, X), true, ifeq3(of(skc5, Y, X), true, ifeq3(placename(skc5, Y), true, ifeq3(entity(skc5, X), true, skc9, Y), Y), Y), Y) -> Y % 3.03/3.03 119: ifeq3(of(skc5, skc9, X), true, ifeq3(of(skc5, skc9, X), true, ifeq3(entity(skc5, X), true, skc9, skc9), skc9), skc9) -> skc9 % 3.03/3.03 120: ifeq3(of(skc5, skc9, skc7), true, ifeq3(of(skc5, skc9, skc7), true, skc9, skc9), skc9) -> skc9 % 3.03/3.03 121: ifeq3(of(skc5, skc9, skc7), true, ifeq3(of(skc5, X, skc7), true, ifeq3(placename(skc5, X), true, skc9, X), X), X) -> X % 3.03/3.03 122: ifeq3(of(skc5, X, Y), true, ifeq3(of(skc5, skc9, Y), true, ifeq3(placename(skc5, X), true, ifeq3(entity(skc5, Y), true, X, skc9), skc9), skc9), skc9) -> skc9 % 3.03/3.03 123: ifeq3(of(skc5, X, skc7), true, ifeq3(of(skc5, skc9, skc7), true, ifeq3(placename(skc5, X), true, X, skc9), skc9), skc9) -> skc9 % 3.03/3.03 124: ifeq3(of(skc5, X, skc8), true, ifeq3(of(skc5, Y, skc8), true, ifeq3(placename(skc5, X), true, ifeq3(placename(skc5, Y), true, X, Y), Y), Y), Y) -> Y % 3.03/3.03 125: ifeq3(of(skc5, X, skc7), true, ifeq3(of(skc5, Y, skc7), true, ifeq3(placename(skc5, X), true, ifeq3(placename(skc5, Y), true, X, Y), Y), Y), Y) -> Y % 3.03/3.03 %------------------------------------------------------------------------------