%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP124-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n011.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:45 AM UTC 2025 % Result : Satisfiable 3.27s 3.31s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NLP124-10 : TPTP v9.0.0. Released v7.3.0. % 0.03/0.11 % Command : run_Leo-III %s %d THM % 0.11/0.32 % Computer : n011.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Mon Jul 14 14:16:19 EDT 2025 % 0.11/0.32 % CPUTime : % 3.27/3.31 % SZS status Satisfiable % 3.27/3.31 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 3.27/3.31 1: actual_world(skc6) -> true % 3.27/3.31 2: street(skc6, skc11) -> true % 3.27/3.31 3: city(skc6, skc10) -> true % 3.27/3.31 4: old(skc6, skc8) -> true % 3.27/3.31 5: dirty(skc6, skc8) -> true % 3.27/3.31 6: white(skc6, skc8) -> true % 3.27/3.31 7: chevy(skc6, skc8) -> true % 3.27/3.31 8: placename(skc6, skc9) -> true % 3.27/3.31 9: hollywood_placename(skc6, skc9) -> true % 3.27/3.31 10: event(skc6, skc7) -> true % 3.27/3.31 11: present(skc6, skc7) -> true % 3.27/3.31 12: barrel(skc6, skc7) -> true % 3.27/3.31 13: lonely(skc6, skc11) -> true % 3.27/3.31 14: of(skc6, skc9, skc10) -> true % 3.27/3.31 15: in(skc6, skc7, skc10) -> true % 3.27/3.31 16: agent(skc6, skc7, skc8) -> true % 3.27/3.31 17: down(skc6, skc7, skc11) -> true % 3.27/3.31 18: ifeq2(X, X, Y, Z) -> Y % 3.27/3.31 19: ifeq3(X, X, Y, Z) -> Y % 3.27/3.31 20: ifeq(X, X, Y, Z) -> Y % 3.27/3.31 21: ifeq2(event(X, Y), true, eventuality(X, Y), true) -> true % 3.27/3.31 22: true -> eventuality(skc6, skc7) % 3.27/3.31 24: ifeq2(barrel(X, Y), eventuality(skc6, skc7), event(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 26: ifeq2(eventuality(X, Y), eventuality(skc6, skc7), thing(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 27: thing(skc6, skc7) -> eventuality(skc6, skc7) % 3.27/3.31 29: ifeq2(instrumentality(X, Y), eventuality(skc6, skc7), artifact(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 31: ifeq2(abstraction(X, Y), eventuality(skc6, skc7), general(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 33: ifeq2(abstraction(X, Y), eventuality(skc6, skc7), thing(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 35: ifeq2(abstraction(X, Y), eventuality(skc6, skc7), nonhuman(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 37: ifeq2(abstraction(X, Y), eventuality(skc6, skc7), unisex(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 39: ifeq2(city(X, Y), eventuality(skc6, skc7), location(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 40: location(skc6, skc10) -> eventuality(skc6, skc7) % 3.27/3.31 42: ifeq2(hollywood_placename(X, Y), eventuality(skc6, skc7), placename(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 44: ifeq2(location(X, Y), eventuality(skc6, skc7), object(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 45: object(skc6, skc10) -> eventuality(skc6, skc7) % 3.27/3.31 47: ifeq2(vehicle(X, Y), eventuality(skc6, skc7), transport(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 49: ifeq2(car(X, Y), eventuality(skc6, skc7), vehicle(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 51: ifeq2(transport(X, Y), eventuality(skc6, skc7), instrumentality(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 53: ifeq2(relation(X, Y), eventuality(skc6, skc7), abstraction(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 55: ifeq2(chevy(X, Y), eventuality(skc6, skc7), car(X, Y), eventuality(skc6, skc7)) -> eventuality(skc6, skc7) % 3.27/3.31 56: eventuality(skc6, skc7) -> car(skc6, skc8) % 3.27/3.31 58: ifeq2(thing(X, Y), car(skc6, skc8), singleton(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 59: singleton(skc6, skc7) -> car(skc6, skc8) % 3.27/3.31 61: ifeq2(street(X, Y), car(skc6, skc8), way(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 62: way(skc6, skc11) -> car(skc6, skc8) % 3.27/3.31 64: ifeq2(eventuality(X, Y), car(skc6, skc8), unisex(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 65: unisex(skc6, skc7) -> car(skc6, skc8) % 3.27/3.31 67: ifeq2(way(X, Y), car(skc6, skc8), artifact(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 68: artifact(skc6, skc11) -> car(skc6, skc8) % 3.27/3.31 70: ifeq2(eventuality(X, Y), car(skc6, skc8), nonexistent(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 71: nonexistent(skc6, skc7) -> car(skc6, skc8) % 3.27/3.31 73: ifeq2(eventuality(X, Y), car(skc6, skc8), specific(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 74: specific(skc6, skc7) -> car(skc6, skc8) % 3.27/3.31 76: ifeq2(object(X, Y), car(skc6, skc8), entity(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 77: entity(skc6, skc10) -> car(skc6, skc8) % 3.27/3.31 79: ifeq2(artifact(X, Y), car(skc6, skc8), object(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 80: object(skc6, skc11) -> car(skc6, skc8) % 3.27/3.31 81: entity(skc6, skc11) -> car(skc6, skc8) % 3.27/3.31 83: ifeq2(entity(X, Y), car(skc6, skc8), thing(X, Y), car(skc6, skc8)) -> car(skc6, skc8) % 3.27/3.31 84: thing(skc6, skc10) -> car(skc6, skc8) % 3.27/3.31 85: singleton(skc6, skc10) -> car(skc6, skc8) % 3.27/3.31 86: thing(skc6, skc11) -> car(skc6, skc8) % 3.27/3.31 87: car(skc6, skc8) -> singleton(skc6, skc11) % 3.27/3.31 88: vehicle(skc6, skc8) -> singleton(skc6, skc11) % 3.27/3.31 89: transport(skc6, skc8) -> singleton(skc6, skc11) % 3.27/3.31 91: ifeq2(object(X, Y), singleton(skc6, skc11), nonliving(X, Y), singleton(skc6, skc11)) -> singleton(skc6, skc11) % 3.27/3.31 92: nonliving(skc6, skc10) -> singleton(skc6, skc11) % 3.27/3.31 93: nonliving(skc6, skc11) -> singleton(skc6, skc11) % 3.27/3.31 95: ifeq2(entity(X, Y), singleton(skc6, skc11), existent(X, Y), singleton(skc6, skc11)) -> singleton(skc6, skc11) % 3.27/3.31 96: existent(skc6, skc10) -> singleton(skc6, skc11) % 3.27/3.31 97: existent(skc6, skc11) -> singleton(skc6, skc11) % 3.27/3.31 99: ifeq2(entity(X, Y), singleton(skc6, skc11), specific(X, Y), singleton(skc6, skc11)) -> singleton(skc6, skc11) % 3.27/3.31 100: specific(skc6, skc10) -> singleton(skc6, skc11) % 3.27/3.31 101: specific(skc6, skc11) -> singleton(skc6, skc11) % 3.27/3.31 103: ifeq2(object(X, Y), singleton(skc6, skc11), impartial(X, Y), singleton(skc6, skc11)) -> singleton(skc6, skc11) % 3.27/3.31 104: impartial(skc6, skc10) -> singleton(skc6, skc11) % 3.27/3.31 105: impartial(skc6, skc11) -> singleton(skc6, skc11) % 3.27/3.31 107: ifeq2(placename(X, Y), singleton(skc6, skc11), relname(X, Y), singleton(skc6, skc11)) -> singleton(skc6, skc11) % 3.27/3.31 108: relname(skc6, skc9) -> singleton(skc6, skc11) % 3.27/3.31 110: ifeq2(object(X, Y), singleton(skc6, skc11), unisex(X, Y), singleton(skc6, skc11)) -> singleton(skc6, skc11) % 3.27/3.31 111: unisex(skc6, skc10) -> singleton(skc6, skc11) % 3.27/3.31 112: unisex(skc6, skc11) -> singleton(skc6, skc11) % 3.27/3.31 114: ifeq2(relname(X, Y), singleton(skc6, skc11), relation(X, Y), singleton(skc6, skc11)) -> singleton(skc6, skc11) % 3.27/3.31 115: relation(skc6, skc9) -> singleton(skc6, skc11) % 3.27/3.31 116: abstraction(skc6, skc9) -> singleton(skc6, skc11) % 3.27/3.31 117: unisex(skc6, skc9) -> singleton(skc6, skc11) % 3.27/3.31 118: nonhuman(skc6, skc9) -> singleton(skc6, skc11) % 3.27/3.31 119: thing(skc6, skc9) -> singleton(skc6, skc11) % 3.27/3.31 120: general(skc6, skc9) -> singleton(skc6, skc11) % 3.27/3.31 121: singleton(skc6, skc11) -> singleton(skc6, skc9) % 3.27/3.31 122: instrumentality(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 123: artifact(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 124: object(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 125: unisex(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 126: impartial(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 127: nonliving(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 128: entity(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 129: specific(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 130: existent(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 131: thing(skc6, skc8) -> singleton(skc6, skc9) % 3.27/3.31 132: singleton(skc6, skc9) -> singleton(skc6, skc8) % 3.27/3.31 134: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 136: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 137: ifeq2(event(X, Y), singleton(skc6, skc8), eventuality(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 138: ifeq2(eventuality(X, Y), singleton(skc6, skc8), thing(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 139: ifeq2(instrumentality(X, Y), singleton(skc6, skc8), artifact(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 140: ifeq2(barrel(X, Y), singleton(skc6, skc8), event(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 141: ifeq2(abstraction(X, Y), singleton(skc6, skc8), general(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 142: ifeq2(location(X, Y), singleton(skc6, skc8), object(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 143: ifeq2(vehicle(X, Y), singleton(skc6, skc8), transport(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 144: ifeq2(car(X, Y), singleton(skc6, skc8), vehicle(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 145: ifeq2(hollywood_placename(X, Y), singleton(skc6, skc8), placename(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 146: ifeq2(city(X, Y), singleton(skc6, skc8), location(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 147: ifeq2(abstraction(X, Y), singleton(skc6, skc8), unisex(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 148: ifeq2(abstraction(X, Y), singleton(skc6, skc8), nonhuman(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 149: ifeq2(abstraction(X, Y), singleton(skc6, skc8), thing(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 150: ifeq2(relation(X, Y), singleton(skc6, skc8), abstraction(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 151: ifeq2(chevy(X, Y), singleton(skc6, skc8), car(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 152: ifeq2(transport(X, Y), singleton(skc6, skc8), instrumentality(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 153: ifeq2(entity(skc6, skc7), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 154: ifeq2(abstraction(skc6, skc7), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 155: ifeq2(artifact(skc6, skc10), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 156: ifeq2(instrumentality(skc6, skc11), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 157: ifeq2(object(skc6, skc7), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 158: ifeq2(eventuality(skc6, skc10), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 159: ifeq2(abstraction(skc6, skc10), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 160: ifeq2(location(skc6, skc11), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 161: ifeq2(object(skc6, skc9), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 162: ifeq2(abstraction(skc6, skc11), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 163: ifeq2(entity(X, Y), singleton(skc6, skc8), existent(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 164: ifeq2(object(X, Y), singleton(skc6, skc8), nonliving(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 165: ifeq2(entity(X, Y), singleton(skc6, skc8), specific(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 166: ifeq2(relname(X, Y), singleton(skc6, skc8), relation(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 167: ifeq2(placename(X, Y), singleton(skc6, skc8), relname(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 168: ifeq2(object(X, Y), singleton(skc6, skc8), unisex(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 169: ifeq2(object(X, Y), singleton(skc6, skc8), impartial(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 170: ifeq2(eventuality(skc6, skc11), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 171: ifeq2(eventuality(skc6, skc9), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 172: ifeq2(entity(skc6, skc9), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 173: ifeq2(street(X, Y), singleton(skc6, skc8), way(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 174: ifeq2(eventuality(X, Y), singleton(skc6, skc8), unisex(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 175: ifeq2(artifact(X, Y), singleton(skc6, skc8), object(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 176: ifeq2(entity(X, Y), singleton(skc6, skc8), thing(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 177: ifeq2(eventuality(X, Y), singleton(skc6, skc8), specific(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 178: ifeq2(object(X, Y), singleton(skc6, skc8), entity(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 179: ifeq2(eventuality(X, Y), singleton(skc6, skc8), nonexistent(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 180: ifeq2(way(X, Y), singleton(skc6, skc8), artifact(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 181: ifeq2(thing(X, Y), singleton(skc6, skc8), singleton(X, Y), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 182: ifeq(tuple(singleton(skc6, skc8), existent(skc6, skc7)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 183: ifeq(tuple(singleton(skc6, skc8), general(skc6, skc7)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 184: ifeq2(way(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 185: ifeq(tuple(specific(skc6, skc9), singleton(skc6, skc8)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 186: ifeq(tuple(nonexistent(skc6, skc10), singleton(skc6, skc8)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 187: ifeq(tuple(singleton(skc6, skc8), general(skc6, skc10)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 188: ifeq2(location(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 189: ifeq(tuple(nonexistent(skc6, skc11), singleton(skc6, skc8)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 190: ifeq(tuple(singleton(skc6, skc8), general(skc6, skc11)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 191: ifeq2(eventuality(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 192: ifeq2(abstraction(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8), singleton(skc6, skc8)) -> singleton(skc6, skc8) % 3.27/3.31 193: ifeq(tuple(singleton(skc6, skc8), general(skc6, skc8)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 194: ifeq(tuple(nonexistent(skc6, skc8), singleton(skc6, skc8)), tuple(singleton(skc6, skc8), singleton(skc6, skc8)), a, b) -> b % 3.27/3.31 196: ifeq3(of(X, Y, Z), singleton(skc6, skc8), ifeq3(of(X, W, Z), singleton(skc6, skc8), ifeq3(placename(X, Y), singleton(skc6, skc8), ifeq3(placename(X, W), singleton(skc6, skc8), ifeq3(entity(X, Z), singleton(skc6, skc8), Y, W), W), W), W), W) -> W % 3.27/3.31 197: ifeq3(of(skc6, X, skc10), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), skc9, X), X) -> X % 3.27/3.31 198: ifeq3(of(skc6, X, skc10), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), X, skc9), skc9) -> skc9 % 3.27/3.31 199: ifeq3(of(skc6, skc9, X), singleton(skc6, skc8), ifeq3(of(skc6, Y, X), singleton(skc6, skc8), ifeq3(placename(skc6, Y), singleton(skc6, skc8), ifeq3(entity(skc6, X), singleton(skc6, skc8), skc9, Y), Y), Y), Y) -> Y % 3.27/3.31 200: ifeq3(of(skc6, skc9, X), singleton(skc6, skc8), ifeq3(of(skc6, skc9, X), singleton(skc6, skc8), ifeq3(entity(skc6, X), singleton(skc6, skc8), skc9, skc9), skc9), skc9) -> skc9 % 3.27/3.31 201: ifeq3(of(skc6, skc9, skc11), singleton(skc6, skc8), ifeq3(of(skc6, skc9, skc11), singleton(skc6, skc8), skc9, skc9), skc9) -> skc9 % 3.27/3.31 202: ifeq3(of(skc6, skc9, skc8), singleton(skc6, skc8), ifeq3(of(skc6, skc9, skc8), singleton(skc6, skc8), skc9, skc9), skc9) -> skc9 % 3.27/3.31 203: ifeq3(of(skc6, skc9, skc11), singleton(skc6, skc8), ifeq3(of(skc6, X, skc11), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), skc9, X), X), X) -> X % 3.27/3.31 204: ifeq3(of(skc6, skc9, skc8), singleton(skc6, skc8), ifeq3(of(skc6, X, skc8), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), skc9, X), X), X) -> X % 3.27/3.31 205: ifeq3(of(skc6, X, Y), singleton(skc6, skc8), ifeq3(of(skc6, skc9, Y), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), ifeq3(entity(skc6, Y), singleton(skc6, skc8), X, skc9), skc9), skc9), skc9) -> skc9 % 3.27/3.31 206: ifeq3(of(skc6, X, skc11), singleton(skc6, skc8), ifeq3(of(skc6, skc9, skc11), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), X, skc9), skc9), skc9) -> skc9 % 3.27/3.31 207: ifeq3(of(skc6, X, skc8), singleton(skc6, skc8), ifeq3(of(skc6, skc9, skc8), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), X, skc9), skc9), skc9) -> skc9 % 3.27/3.31 208: ifeq3(of(skc6, X, skc10), singleton(skc6, skc8), ifeq3(of(skc6, Y, skc10), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), ifeq3(placename(skc6, Y), singleton(skc6, skc8), X, Y), Y), Y), Y) -> Y % 3.27/3.31 209: ifeq3(of(skc6, X, skc11), singleton(skc6, skc8), ifeq3(of(skc6, Y, skc11), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), ifeq3(placename(skc6, Y), singleton(skc6, skc8), X, Y), Y), Y), Y) -> Y % 3.27/3.31 210: ifeq3(of(skc6, X, skc8), singleton(skc6, skc8), ifeq3(of(skc6, Y, skc8), singleton(skc6, skc8), ifeq3(placename(skc6, X), singleton(skc6, skc8), ifeq3(placename(skc6, Y), singleton(skc6, skc8), X, Y), Y), Y), Y) -> Y % 3.27/3.31 %------------------------------------------------------------------------------