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