%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP127-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n014.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.12s 3.18s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NLP127-10 : TPTP v9.0.0. Released v7.5.0. % 0.08/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.34 % Computer : n014.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:34 EDT 2025 % 0.12/0.34 % CPUTime : % 3.12/3.18 % SZS status Satisfiable % 3.12/3.18 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 3.12/3.18 1: actual_world(skc6) -> true % 3.12/3.18 2: chevy(skc6, skc11) -> true % 3.12/3.18 3: city(skc6, skc10) -> true % 3.12/3.18 4: lonely(skc6, skc8) -> true % 3.12/3.18 5: street(skc6, skc8) -> true % 3.12/3.18 6: placename(skc6, skc9) -> true % 3.12/3.18 7: hollywood_placename(skc6, skc9) -> true % 3.12/3.18 8: event(skc6, skc7) -> true % 3.12/3.18 9: present(skc6, skc7) -> true % 3.12/3.18 10: barrel(skc6, skc7) -> true % 3.12/3.18 11: white(skc6, skc11) -> true % 3.12/3.18 12: dirty(skc6, skc11) -> true % 3.12/3.18 13: old(skc6, skc11) -> true % 3.12/3.18 14: of(skc6, skc9, skc10) -> true % 3.12/3.18 15: in(skc6, skc7, skc10) -> true % 3.12/3.18 16: down(skc6, skc7, skc8) -> true % 3.12/3.18 17: agent(skc6, skc7, skc11) -> true % 3.12/3.18 18: ifeq2(X, X, Y, Z) -> Y % 3.12/3.18 19: ifeq3(X, X, Y, Z) -> Y % 3.12/3.18 20: ifeq(X, X, Y, Z) -> Y % 3.12/3.18 21: ifeq2(event(X, Y), true, eventuality(X, Y), true) -> true % 3.12/3.18 22: eventuality(skc6, skc7) -> true % 3.12/3.18 23: ifeq2(barrel(X, Y), true, event(X, Y), true) -> true % 3.12/3.18 24: ifeq2(eventuality(X, Y), true, thing(X, Y), true) -> true % 3.12/3.18 25: thing(skc6, skc7) -> true % 3.12/3.18 26: ifeq2(instrumentality(X, Y), true, artifact(X, Y), true) -> true % 3.12/3.18 27: ifeq2(abstraction(X, Y), true, general(X, Y), true) -> true % 3.12/3.18 28: ifeq2(abstraction(X, Y), true, thing(X, Y), true) -> true % 3.12/3.18 29: ifeq2(abstraction(X, Y), true, nonhuman(X, Y), true) -> true % 3.12/3.18 30: ifeq2(abstraction(X, Y), true, unisex(X, Y), true) -> true % 3.12/3.18 31: ifeq2(city(X, Y), true, location(X, Y), true) -> true % 3.12/3.18 32: location(skc6, skc10) -> true % 3.12/3.18 33: ifeq2(hollywood_placename(X, Y), true, placename(X, Y), true) -> true % 3.12/3.18 34: ifeq2(location(X, Y), true, object(X, Y), true) -> true % 3.12/3.18 35: object(skc6, skc10) -> true % 3.12/3.18 36: ifeq2(vehicle(X, Y), true, transport(X, Y), true) -> true % 3.12/3.18 37: ifeq2(car(X, Y), true, vehicle(X, Y), true) -> true % 3.12/3.18 38: ifeq2(transport(X, Y), true, instrumentality(X, Y), true) -> true % 3.12/3.18 39: ifeq2(relation(X, Y), true, abstraction(X, Y), true) -> true % 3.12/3.18 40: ifeq2(chevy(X, Y), true, car(X, Y), true) -> true % 3.12/3.18 41: car(skc6, skc11) -> true % 3.12/3.18 42: vehicle(skc6, skc11) -> true % 3.12/3.18 43: transport(skc6, skc11) -> true % 3.12/3.18 44: instrumentality(skc6, skc11) -> true % 3.12/3.18 45: artifact(skc6, skc11) -> true % 3.12/3.18 46: ifeq2(thing(X, Y), true, singleton(X, Y), true) -> true % 3.12/3.18 47: singleton(skc6, skc7) -> true % 3.12/3.18 48: ifeq2(street(X, Y), true, way(X, Y), true) -> true % 3.12/3.18 49: way(skc6, skc8) -> true % 3.12/3.18 50: ifeq2(eventuality(X, Y), true, nonexistent(X, Y), true) -> true % 3.12/3.18 51: nonexistent(skc6, skc7) -> true % 3.12/3.18 52: ifeq2(eventuality(X, Y), true, unisex(X, Y), true) -> true % 3.12/3.18 53: unisex(skc6, skc7) -> true % 3.12/3.18 54: ifeq2(eventuality(X, Y), true, specific(X, Y), true) -> true % 3.12/3.18 55: specific(skc6, skc7) -> true % 3.12/3.18 56: ifeq2(way(X, Y), true, artifact(X, Y), true) -> true % 3.12/3.18 57: artifact(skc6, skc8) -> true % 3.12/3.18 58: ifeq2(object(X, Y), true, entity(X, Y), true) -> true % 3.12/3.18 59: entity(skc6, skc10) -> true % 3.12/3.18 60: ifeq2(artifact(X, Y), true, object(X, Y), true) -> true % 3.12/3.18 61: true -> object(skc6, skc8) % 3.12/3.18 62: object(skc6, skc11) -> object(skc6, skc8) % 3.12/3.18 63: entity(skc6, skc11) -> object(skc6, skc8) % 3.12/3.18 65: ifeq2(entity(X, Y), object(skc6, skc8), thing(X, Y), object(skc6, skc8)) -> object(skc6, skc8) % 3.12/3.18 66: thing(skc6, skc10) -> object(skc6, skc8) % 3.12/3.18 67: singleton(skc6, skc10) -> object(skc6, skc8) % 3.12/3.18 68: thing(skc6, skc11) -> object(skc6, skc8) % 3.12/3.18 70: ifeq2(object(X, Y), object(skc6, skc8), nonliving(X, Y), object(skc6, skc8)) -> object(skc6, skc8) % 3.12/3.18 71: nonliving(skc6, skc8) -> object(skc6, skc8) % 3.12/3.18 72: nonliving(skc6, skc10) -> object(skc6, skc8) % 3.12/3.18 73: nonliving(skc6, skc11) -> object(skc6, skc8) % 3.12/3.18 75: ifeq2(entity(X, Y), object(skc6, skc8), specific(X, Y), object(skc6, skc8)) -> object(skc6, skc8) % 3.12/3.18 76: specific(skc6, skc10) -> object(skc6, skc8) % 3.12/3.18 77: specific(skc6, skc11) -> object(skc6, skc8) % 3.12/3.18 79: ifeq2(object(X, Y), object(skc6, skc8), impartial(X, Y), object(skc6, skc8)) -> object(skc6, skc8) % 3.12/3.18 80: impartial(skc6, skc8) -> object(skc6, skc8) % 3.12/3.18 81: impartial(skc6, skc10) -> object(skc6, skc8) % 3.12/3.18 82: impartial(skc6, skc11) -> object(skc6, skc8) % 3.12/3.18 84: ifeq2(entity(X, Y), object(skc6, skc8), existent(X, Y), object(skc6, skc8)) -> object(skc6, skc8) % 3.12/3.18 85: existent(skc6, skc10) -> object(skc6, skc8) % 3.12/3.18 86: existent(skc6, skc11) -> object(skc6, skc8) % 3.12/3.18 88: ifeq2(placename(X, Y), object(skc6, skc8), relname(X, Y), object(skc6, skc8)) -> object(skc6, skc8) % 3.12/3.18 89: object(skc6, skc8) -> relname(skc6, skc9) % 3.12/3.18 90: entity(skc6, skc8) -> relname(skc6, skc9) % 3.12/3.18 91: existent(skc6, skc8) -> relname(skc6, skc9) % 3.12/3.18 92: specific(skc6, skc8) -> relname(skc6, skc9) % 3.12/3.18 93: thing(skc6, skc8) -> relname(skc6, skc9) % 3.12/3.18 94: singleton(skc6, skc8) -> relname(skc6, skc9) % 3.12/3.18 96: ifeq2(object(X, Y), relname(skc6, skc9), unisex(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 97: unisex(skc6, skc8) -> relname(skc6, skc9) % 3.12/3.18 98: unisex(skc6, skc10) -> relname(skc6, skc9) % 3.12/3.18 99: unisex(skc6, skc11) -> relname(skc6, skc9) % 3.12/3.18 101: ifeq2(relname(X, Y), relname(skc6, skc9), relation(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 102: relation(skc6, skc9) -> relname(skc6, skc9) % 3.12/3.18 103: abstraction(skc6, skc9) -> relname(skc6, skc9) % 3.12/3.18 104: unisex(skc6, skc9) -> relname(skc6, skc9) % 3.12/3.18 105: nonhuman(skc6, skc9) -> relname(skc6, skc9) % 3.12/3.18 106: thing(skc6, skc9) -> relname(skc6, skc9) % 3.12/3.18 107: general(skc6, skc9) -> relname(skc6, skc9) % 3.12/3.18 108: singleton(skc6, skc9) -> relname(skc6, skc9) % 3.12/3.18 109: singleton(skc6, skc11) -> relname(skc6, skc9) % 3.12/3.18 110: ifeq2(abstraction(skc6, skc7), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 111: ifeq2(artifact(skc6, skc10), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 112: ifeq2(instrumentality(skc6, skc8), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 113: ifeq2(way(skc6, skc11), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 115: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 117: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 118: ifeq2(placename(X, Y), relname(skc6, skc9), relname(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 119: ifeq2(entity(X, Y), relname(skc6, skc9), existent(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 120: ifeq2(object(X, Y), relname(skc6, skc9), impartial(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 121: ifeq2(object(X, Y), relname(skc6, skc9), nonliving(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 122: ifeq2(entity(X, Y), relname(skc6, skc9), specific(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 123: ifeq2(entity(X, Y), relname(skc6, skc9), thing(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 124: ifeq2(location(skc6, skc8), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 125: ifeq2(object(skc6, skc7), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 126: ifeq2(eventuality(skc6, skc8), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 127: ifeq2(entity(skc6, skc7), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 128: ifeq2(barrel(X, Y), relname(skc6, skc9), event(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 129: ifeq2(eventuality(X, Y), relname(skc6, skc9), thing(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 130: ifeq2(artifact(X, Y), relname(skc6, skc9), object(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 131: ifeq2(object(X, Y), relname(skc6, skc9), entity(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 132: ifeq2(abstraction(X, Y), relname(skc6, skc9), thing(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 133: ifeq2(abstraction(X, Y), relname(skc6, skc9), nonhuman(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 134: ifeq2(abstraction(X, Y), relname(skc6, skc9), general(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 135: ifeq2(instrumentality(X, Y), relname(skc6, skc9), artifact(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 136: ifeq2(abstraction(skc6, skc8), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 137: ifeq2(car(X, Y), relname(skc6, skc9), vehicle(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 138: ifeq2(relation(X, Y), relname(skc6, skc9), abstraction(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 139: ifeq2(transport(X, Y), relname(skc6, skc9), instrumentality(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 140: ifeq2(vehicle(X, Y), relname(skc6, skc9), transport(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 141: ifeq2(location(X, Y), relname(skc6, skc9), object(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 142: ifeq2(hollywood_placename(X, Y), relname(skc6, skc9), placename(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 143: ifeq2(city(X, Y), relname(skc6, skc9), location(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 144: ifeq2(abstraction(X, Y), relname(skc6, skc9), unisex(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 145: ifeq2(eventuality(X, Y), relname(skc6, skc9), specific(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 146: ifeq2(way(X, Y), relname(skc6, skc9), artifact(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 147: ifeq2(eventuality(X, Y), relname(skc6, skc9), unisex(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 148: ifeq2(eventuality(X, Y), relname(skc6, skc9), nonexistent(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 149: ifeq2(street(X, Y), relname(skc6, skc9), way(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 150: ifeq2(thing(X, Y), relname(skc6, skc9), singleton(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 151: ifeq2(chevy(X, Y), relname(skc6, skc9), car(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 152: ifeq2(event(X, Y), relname(skc6, skc9), eventuality(X, Y), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 153: ifeq2(object(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 154: ifeq2(eventuality(skc6, skc10), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 155: ifeq2(abstraction(skc6, skc10), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 156: ifeq2(entity(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 157: ifeq2(eventuality(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 158: ifeq2(location(skc6, skc11), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 159: ifeq2(abstraction(skc6, skc11), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 160: ifeq2(eventuality(skc6, skc11), relname(skc6, skc9), relname(skc6, skc9), relname(skc6, skc9)) -> relname(skc6, skc9) % 3.12/3.18 161: ifeq(tuple(relname(skc6, skc9), general(skc6, skc7)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 162: ifeq(tuple(relname(skc6, skc9), existent(skc6, skc7)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 163: ifeq(tuple(relname(skc6, skc9), general(skc6, skc8)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 164: ifeq(tuple(nonexistent(skc6, skc8), relname(skc6, skc9)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 165: ifeq(tuple(specific(skc6, skc9), relname(skc6, skc9)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 166: ifeq(tuple(relname(skc6, skc9), general(skc6, skc10)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 167: ifeq(tuple(nonexistent(skc6, skc10), relname(skc6, skc9)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 168: ifeq(tuple(nonexistent(skc6, skc11), relname(skc6, skc9)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 169: ifeq(tuple(relname(skc6, skc9), general(skc6, skc11)), tuple(relname(skc6, skc9), relname(skc6, skc9)), a, b) -> b % 3.12/3.18 171: ifeq3(of(X, Y, Z), relname(skc6, skc9), ifeq3(of(X, W, Z), relname(skc6, skc9), ifeq3(placename(X, Y), relname(skc6, skc9), ifeq3(placename(X, W), relname(skc6, skc9), ifeq3(entity(X, Z), relname(skc6, skc9), Y, W), W), W), W), W) -> W % 3.12/3.18 172: ifeq3(of(skc6, X, skc10), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), skc9, X), X) -> X % 3.12/3.18 173: ifeq3(of(skc6, X, skc10), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), X, skc9), skc9) -> skc9 % 3.12/3.18 174: ifeq3(of(skc6, skc9, X), relname(skc6, skc9), ifeq3(of(skc6, Y, X), relname(skc6, skc9), ifeq3(placename(skc6, Y), relname(skc6, skc9), ifeq3(entity(skc6, X), relname(skc6, skc9), skc9, Y), Y), Y), Y) -> Y % 3.12/3.18 175: ifeq3(of(skc6, skc9, X), relname(skc6, skc9), ifeq3(of(skc6, skc9, X), relname(skc6, skc9), ifeq3(entity(skc6, X), relname(skc6, skc9), skc9, skc9), skc9), skc9) -> skc9 % 3.12/3.18 176: ifeq3(of(skc6, skc9, skc8), relname(skc6, skc9), ifeq3(of(skc6, skc9, skc8), relname(skc6, skc9), skc9, skc9), skc9) -> skc9 % 3.12/3.18 177: ifeq3(of(skc6, skc9, skc11), relname(skc6, skc9), ifeq3(of(skc6, skc9, skc11), relname(skc6, skc9), skc9, skc9), skc9) -> skc9 % 3.12/3.18 178: ifeq3(of(skc6, skc9, skc8), relname(skc6, skc9), ifeq3(of(skc6, X, skc8), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), skc9, X), X), X) -> X % 3.12/3.18 179: ifeq3(of(skc6, skc9, skc11), relname(skc6, skc9), ifeq3(of(skc6, X, skc11), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), skc9, X), X), X) -> X % 3.12/3.18 180: ifeq3(of(skc6, X, Y), relname(skc6, skc9), ifeq3(of(skc6, skc9, Y), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), ifeq3(entity(skc6, Y), relname(skc6, skc9), X, skc9), skc9), skc9), skc9) -> skc9 % 3.12/3.18 181: ifeq3(of(skc6, X, skc8), relname(skc6, skc9), ifeq3(of(skc6, skc9, skc8), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), X, skc9), skc9), skc9) -> skc9 % 3.12/3.18 182: ifeq3(of(skc6, X, skc11), relname(skc6, skc9), ifeq3(of(skc6, skc9, skc11), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), X, skc9), skc9), skc9) -> skc9 % 3.12/3.18 183: ifeq3(of(skc6, X, skc8), relname(skc6, skc9), ifeq3(of(skc6, Y, skc8), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), ifeq3(placename(skc6, Y), relname(skc6, skc9), X, Y), Y), Y), Y) -> Y % 3.12/3.18 184: ifeq3(of(skc6, X, skc10), relname(skc6, skc9), ifeq3(of(skc6, Y, skc10), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), ifeq3(placename(skc6, Y), relname(skc6, skc9), X, Y), Y), Y), Y) -> Y % 3.12/3.18 185: ifeq3(of(skc6, X, skc11), relname(skc6, skc9), ifeq3(of(skc6, Y, skc11), relname(skc6, skc9), ifeq3(placename(skc6, X), relname(skc6, skc9), ifeq3(placename(skc6, Y), relname(skc6, skc9), X, Y), Y), Y), Y) -> Y % 3.12/3.18 %------------------------------------------------------------------------------