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