%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP042-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n004.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:35 AM UTC 2025 % Result : Satisfiable 3.76s 3.71s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NLP042-10 : TPTP v9.0.0. Released v7.3.0. % 0.08/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.32 % Computer : n004.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % 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:12:04 EDT 2025 % 0.12/0.33 % CPUTime : % 3.76/3.71 % SZS status Satisfiable % 3.76/3.71 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 3.76/3.71 1: actual_world(skc5) -> true % 3.76/3.71 2: woman(skc5, skc9) -> true % 3.76/3.71 3: shake_beverage(skc5, skc7) -> true % 3.76/3.71 4: order(skc5, skc6) -> true % 3.76/3.71 5: nonreflexive(skc5, skc6) -> true % 3.76/3.71 6: past(skc5, skc6) -> true % 3.76/3.71 7: event(skc5, skc6) -> true % 3.76/3.71 8: forename(skc5, skc8) -> true % 3.76/3.71 9: mia_forename(skc5, skc8) -> true % 3.76/3.71 10: of(skc5, skc8, skc9) -> true % 3.76/3.71 11: agent(skc5, skc6, skc9) -> true % 3.76/3.71 12: patient(skc5, skc6, skc7) -> true % 3.76/3.71 13: ifeq4(X, X, Y, Z) -> Y % 3.76/3.71 14: ifeq2(X, X, Y, Z) -> Y % 3.76/3.71 15: ifeq3(X, X, Y, Z) -> Y % 3.76/3.71 16: ifeq(X, X, Y, Z) -> Y % 3.76/3.71 17: ifeq3(human_person(X, Y), true, human(X, Y), true) -> true % 3.76/3.71 18: ifeq3(organism(X, Y), true, living(X, Y), true) -> true % 3.76/3.71 19: ifeq3(human_person(X, Y), true, animate(X, Y), true) -> true % 3.76/3.71 20: ifeq3(organism(X, Y), true, impartial(X, Y), true) -> true % 3.76/3.71 21: ifeq3(abstraction(X, Y), true, thing(X, Y), true) -> true % 3.76/3.71 22: ifeq3(woman(X, Y), true, female(X, Y), true) -> true % 3.76/3.71 23: female(skc5, skc9) -> true % 3.76/3.71 24: ifeq3(eventuality(X, Y), true, unisex(X, Y), true) -> true % 3.76/3.71 25: ifeq3(abstraction(X, Y), true, unisex(X, Y), true) -> true % 3.76/3.71 26: ifeq3(abstraction(X, Y), true, nonhuman(X, Y), true) -> true % 3.76/3.71 27: ifeq3(abstraction(X, Y), true, general(X, Y), true) -> true % 3.76/3.71 28: ifeq3(mia_forename(X, Y), true, forename(X, Y), true) -> true % 3.76/3.71 29: ifeq3(human_person(X, Y), true, organism(X, Y), true) -> true % 3.76/3.71 30: ifeq3(woman(X, Y), true, human_person(X, Y), true) -> true % 3.76/3.71 31: human_person(skc5, skc9) -> true % 3.76/3.71 32: organism(skc5, skc9) -> true % 3.76/3.71 33: animate(skc5, skc9) -> true % 3.76/3.71 34: human(skc5, skc9) -> true % 3.76/3.71 35: impartial(skc5, skc9) -> true % 3.76/3.71 36: living(skc5, skc9) -> true % 3.76/3.71 37: ifeq3(organism(X, Y), true, entity(X, Y), true) -> true % 3.76/3.71 38: entity(skc5, skc9) -> true % 3.76/3.71 39: ifeq3(event(X, Y), true, eventuality(X, Y), true) -> true % 3.76/3.71 40: true -> eventuality(skc5, skc6) % 3.76/3.71 42: ifeq3(order(X, Y), eventuality(skc5, skc6), act(X, Y), eventuality(skc5, skc6)) -> eventuality(skc5, skc6) % 3.76/3.71 43: eventuality(skc5, skc6) -> act(skc5, skc6) % 3.76/3.71 44: unisex(skc5, skc6) -> act(skc5, skc6) % 3.76/3.71 46: ifeq3(act(X, Y), act(skc5, skc6), event(X, Y), act(skc5, skc6)) -> act(skc5, skc6) % 3.76/3.71 48: ifeq3(eventuality(X, Y), act(skc5, skc6), thing(X, Y), act(skc5, skc6)) -> act(skc5, skc6) % 3.76/3.71 49: thing(skc5, skc6) -> act(skc5, skc6) % 3.76/3.71 51: ifeq3(eventuality(X, Y), act(skc5, skc6), specific(X, Y), act(skc5, skc6)) -> act(skc5, skc6) % 3.76/3.71 52: specific(skc5, skc6) -> act(skc5, skc6) % 3.76/3.71 54: ifeq3(thing(X, Y), act(skc5, skc6), singleton(X, Y), act(skc5, skc6)) -> act(skc5, skc6) % 3.76/3.71 55: singleton(skc5, skc6) -> act(skc5, skc6) % 3.76/3.71 57: ifeq3(eventuality(X, Y), act(skc5, skc6), nonexistent(X, Y), act(skc5, skc6)) -> act(skc5, skc6) % 3.76/3.71 58: act(skc5, skc6) -> nonexistent(skc5, skc6) % 3.76/3.71 60: ifeq3(food(X, Y), nonexistent(skc5, skc6), substance_matter(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 62: ifeq3(shake_beverage(X, Y), nonexistent(skc5, skc6), beverage(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 63: beverage(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 65: ifeq3(order(X, Y), nonexistent(skc5, skc6), event(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 67: ifeq3(beverage(X, Y), nonexistent(skc5, skc6), food(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 68: food(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 69: substance_matter(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 71: ifeq3(substance_matter(X, Y), nonexistent(skc5, skc6), object(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 72: object(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 74: ifeq3(entity(X, Y), nonexistent(skc5, skc6), thing(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 75: thing(skc5, skc9) -> nonexistent(skc5, skc6) % 3.76/3.71 76: singleton(skc5, skc9) -> nonexistent(skc5, skc6) % 3.76/3.71 78: ifeq3(object(X, Y), nonexistent(skc5, skc6), entity(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 79: entity(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 80: thing(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 81: singleton(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 83: ifeq3(entity(X, Y), nonexistent(skc5, skc6), specific(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 84: specific(skc5, skc9) -> nonexistent(skc5, skc6) % 3.76/3.71 85: specific(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 87: ifeq3(object(X, Y), nonexistent(skc5, skc6), impartial(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 88: impartial(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 90: ifeq3(entity(X, Y), nonexistent(skc5, skc6), existent(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 91: existent(skc5, skc9) -> nonexistent(skc5, skc6) % 3.76/3.71 92: existent(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 94: ifeq3(object(X, Y), nonexistent(skc5, skc6), nonliving(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 95: nonliving(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 97: ifeq3(object(X, Y), nonexistent(skc5, skc6), unisex(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 98: unisex(skc5, skc7) -> nonexistent(skc5, skc6) % 3.76/3.71 100: ifeq3(relname(X, Y), nonexistent(skc5, skc6), relation(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 102: ifeq3(forename(X, Y), nonexistent(skc5, skc6), relname(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 103: relname(skc5, skc8) -> nonexistent(skc5, skc6) % 3.76/3.71 104: relation(skc5, skc8) -> nonexistent(skc5, skc6) % 3.76/3.71 106: ifeq3(relation(X, Y), nonexistent(skc5, skc6), abstraction(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 107: abstraction(skc5, skc8) -> nonexistent(skc5, skc6) % 3.76/3.71 108: general(skc5, skc8) -> nonexistent(skc5, skc6) % 3.76/3.71 109: nonhuman(skc5, skc8) -> nonexistent(skc5, skc6) % 3.76/3.71 110: unisex(skc5, skc8) -> nonexistent(skc5, skc6) % 3.76/3.71 111: thing(skc5, skc8) -> nonexistent(skc5, skc6) % 3.76/3.71 112: singleton(skc5, skc8) -> nonexistent(skc5, skc6) % 3.76/3.71 114: ifeq2(tuple2(unisex(X, Y), female(X, Y)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 116: ifeq2(tuple2(specific(X, Y), general(X, Y)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 118: ifeq2(tuple2(nonliving(X, Y), living(X, Y)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 120: ifeq2(tuple2(nonhuman(X, Y), human(X, Y)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 122: ifeq2(tuple2(nonexistent(X, Y), existent(X, Y)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 124: ifeq2(tuple2(nonliving(X, Y), animate(X, Y)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 125: ifeq3(human_person(X, Y), nonexistent(skc5, skc6), animate(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 126: ifeq3(woman(X, Y), nonexistent(skc5, skc6), human_person(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 127: ifeq3(organism(X, Y), nonexistent(skc5, skc6), entity(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 128: ifeq3(human_person(X, Y), nonexistent(skc5, skc6), organism(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 129: ifeq3(mia_forename(X, Y), nonexistent(skc5, skc6), forename(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 130: ifeq3(order(X, Y), nonexistent(skc5, skc6), act(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 131: ifeq3(organism(X, Y), nonexistent(skc5, skc6), living(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 132: ifeq3(human_person(X, Y), nonexistent(skc5, skc6), human(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 133: ifeq3(event(X, Y), nonexistent(skc5, skc6), eventuality(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 134: ifeq3(abstraction(X, Y), nonexistent(skc5, skc6), nonhuman(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 135: ifeq3(abstraction(X, Y), nonexistent(skc5, skc6), general(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 136: ifeq3(abstraction(X, Y), nonexistent(skc5, skc6), unisex(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 137: ifeq3(eventuality(X, Y), nonexistent(skc5, skc6), unisex(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 138: ifeq3(woman(X, Y), nonexistent(skc5, skc6), female(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 139: ifeq3(abstraction(X, Y), nonexistent(skc5, skc6), thing(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 140: ifeq3(organism(X, Y), nonexistent(skc5, skc6), impartial(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 141: ifeq3(act(X, Y), nonexistent(skc5, skc6), event(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 142: ifeq3(eventuality(X, Y), nonexistent(skc5, skc6), thing(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 143: ifeq3(eventuality(X, Y), nonexistent(skc5, skc6), nonexistent(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 144: ifeq3(thing(X, Y), nonexistent(skc5, skc6), singleton(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 145: ifeq3(eventuality(X, Y), nonexistent(skc5, skc6), specific(X, Y), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 146: ifeq3(abstraction(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 147: ifeq3(entity(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 148: ifeq3(object(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 149: ifeq3(object(skc5, skc9), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 150: ifeq3(eventuality(skc5, skc9), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 151: ifeq3(abstraction(skc5, skc9), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 152: ifeq3(eventuality(skc5, skc8), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 153: ifeq3(object(skc5, skc8), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 154: ifeq3(entity(skc5, skc8), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 155: ifeq3(eventuality(skc5, skc7), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 156: ifeq3(organism(skc5, skc7), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 157: ifeq3(abstraction(skc5, skc7), nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)) -> nonexistent(skc5, skc6) % 3.76/3.71 159: ifeq(tuple(patient(X, Y, Z), nonreflexive(X, Y), agent(X, Y, Z)), tuple(nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 160: ifeq2(tuple2(unisex(skc5, skc9), nonexistent(skc5, skc6)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 161: ifeq2(tuple2(nonexistent(skc5, skc6), female(skc5, skc6)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 162: ifeq2(tuple2(nonhuman(skc5, skc9), nonexistent(skc5, skc6)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 163: ifeq2(tuple2(nonexistent(skc5, skc6), general(skc5, skc6)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 164: ifeq2(tuple2(nonliving(skc5, skc9), nonexistent(skc5, skc6)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 165: ifeq2(tuple2(specific(skc5, skc8), nonexistent(skc5, skc6)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 166: ifeq2(tuple2(nonexistent(skc5, skc6), general(skc5, skc9)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 167: ifeq2(tuple2(nonexistent(skc5, skc9), nonexistent(skc5, skc6)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 168: ifeq2(tuple2(nonexistent(skc5, skc6), female(skc5, skc8)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 169: ifeq2(tuple2(nonexistent(skc5, skc6), human(skc5, skc8)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 170: ifeq2(tuple2(nonexistent(skc5, skc6), female(skc5, skc7)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 171: ifeq2(tuple2(nonexistent(skc5, skc6), animate(skc5, skc7)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 172: ifeq2(tuple2(nonexistent(skc5, skc6), living(skc5, skc7)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 173: ifeq2(tuple2(nonexistent(skc5, skc6), general(skc5, skc7)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 174: ifeq2(tuple2(nonexistent(skc5, skc7), nonexistent(skc5, skc6)), tuple2(nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 175: ifeq(tuple(patient(skc5, skc6, skc9), nonexistent(skc5, skc6), nonexistent(skc5, skc6)), tuple(nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 176: ifeq(tuple(nonexistent(skc5, skc6), nonexistent(skc5, skc6), agent(skc5, skc6, skc7)), tuple(nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 177: ifeq(tuple(patient(skc5, skc6, X), nonexistent(skc5, skc6), agent(skc5, skc6, X)), tuple(nonexistent(skc5, skc6), nonexistent(skc5, skc6), nonexistent(skc5, skc6)), a, b) -> b % 3.76/3.71 179: ifeq4(of(X, Y, Z), nonexistent(skc5, skc6), ifeq4(of(X, W, Z), nonexistent(skc5, skc6), ifeq4(forename(X, Y), nonexistent(skc5, skc6), ifeq4(forename(X, W), nonexistent(skc5, skc6), ifeq4(entity(X, Z), nonexistent(skc5, skc6), Y, W), W), W), W), W) -> W % 3.76/3.71 180: ifeq4(of(skc5, X, skc9), nonexistent(skc5, skc6), ifeq4(forename(skc5, X), nonexistent(skc5, skc6), skc8, X), X) -> X % 3.76/3.71 181: ifeq4(of(skc5, X, skc9), nonexistent(skc5, skc6), ifeq4(forename(skc5, X), nonexistent(skc5, skc6), X, skc8), skc8) -> skc8 % 3.76/3.71 182: ifeq4(of(skc5, skc8, X), nonexistent(skc5, skc6), ifeq4(of(skc5, Y, X), nonexistent(skc5, skc6), ifeq4(forename(skc5, Y), nonexistent(skc5, skc6), ifeq4(entity(skc5, X), nonexistent(skc5, skc6), skc8, Y), Y), Y), Y) -> Y % 3.76/3.71 183: ifeq4(of(skc5, skc8, X), nonexistent(skc5, skc6), ifeq4(of(skc5, skc8, X), nonexistent(skc5, skc6), ifeq4(entity(skc5, X), nonexistent(skc5, skc6), skc8, skc8), skc8), skc8) -> skc8 % 3.76/3.71 184: ifeq4(of(skc5, skc8, skc7), nonexistent(skc5, skc6), ifeq4(of(skc5, skc8, skc7), nonexistent(skc5, skc6), skc8, skc8), skc8) -> skc8 % 3.76/3.71 185: ifeq4(of(skc5, skc8, skc7), nonexistent(skc5, skc6), ifeq4(of(skc5, X, skc7), nonexistent(skc5, skc6), ifeq4(forename(skc5, X), nonexistent(skc5, skc6), skc8, X), X), X) -> X % 3.76/3.71 186: ifeq4(of(skc5, X, Y), nonexistent(skc5, skc6), ifeq4(of(skc5, skc8, Y), nonexistent(skc5, skc6), ifeq4(forename(skc5, X), nonexistent(skc5, skc6), ifeq4(entity(skc5, Y), nonexistent(skc5, skc6), X, skc8), skc8), skc8), skc8) -> skc8 % 3.76/3.71 187: ifeq4(of(skc5, X, skc7), nonexistent(skc5, skc6), ifeq4(of(skc5, skc8, skc7), nonexistent(skc5, skc6), ifeq4(forename(skc5, X), nonexistent(skc5, skc6), X, skc8), skc8), skc8) -> skc8 % 3.76/3.71 188: ifeq4(of(skc5, X, skc9), nonexistent(skc5, skc6), ifeq4(of(skc5, Y, skc9), nonexistent(skc5, skc6), ifeq4(forename(skc5, X), nonexistent(skc5, skc6), ifeq4(forename(skc5, Y), nonexistent(skc5, skc6), X, Y), Y), Y), Y) -> Y % 3.76/3.71 189: ifeq4(of(skc5, X, skc7), nonexistent(skc5, skc6), ifeq4(of(skc5, Y, skc7), nonexistent(skc5, skc6), ifeq4(forename(skc5, X), nonexistent(skc5, skc6), ifeq4(forename(skc5, Y), nonexistent(skc5, skc6), X, Y), Y), Y), Y) -> Y % 3.76/3.71 %------------------------------------------------------------------------------