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