%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP023-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n010.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:32 AM UTC 2025 % Result : Satisfiable 10.69s 10.10s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP023-10 : TPTP v9.0.0. Released v7.3.0. % 0.07/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.33 % Computer : n010.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:10:34 EDT 2025 % 0.12/0.33 % CPUTime : % 10.69/10.10 % SZS status Satisfiable % 10.69/10.10 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 10.69/10.10 1: actual_world(skc6) -> true % 10.69/10.10 2: event(skc8, skc11) -> true % 10.69/10.10 3: woman(skc6, skc10) -> true % 10.69/10.10 4: present(skc8, skc11) -> true % 10.69/10.10 5: dance(skc8, skc11) -> true % 10.69/10.10 6: forename(skc6, skc9) -> true % 10.69/10.10 7: mia_forename(skc6, skc9) -> true % 10.69/10.10 8: proposition(skc6, skc8) -> true % 10.69/10.10 9: accessible_world(skc6, skc8) -> true % 10.69/10.10 10: desire_want(skc6, skc7) -> true % 10.69/10.10 11: present(skc6, skc7) -> true % 10.69/10.10 12: of(skc6, skc9, skc10) -> true % 10.69/10.10 13: agent(skc6, skc7, skc10) -> true % 10.69/10.10 14: agent(skc8, skc11, skc10) -> true % 10.69/10.10 15: theme(skc6, skc7, skc8) -> true % 10.69/10.10 16: ifeq(X, X, Y, Z) -> Y % 10.69/10.10 17: ifeq3(X, X, Y, Z) -> Y % 10.69/10.10 18: ifeq2(X, X, Y, Z) -> Y % 10.69/10.10 19: ifeq2(eventuality(X, Y), true, specific(X, Y), true) -> true % 10.69/10.10 20: ifeq2(thing(X, Y), true, singleton(X, Y), true) -> true % 10.69/10.10 21: ifeq2(dance(X, Y), true, event(X, Y), true) -> true % 10.69/10.10 22: ifeq2(eventuality(X, Y), true, thing(X, Y), true) -> true % 10.69/10.10 23: ifeq2(event(X, Y), true, eventuality(X, Y), true) -> true % 10.69/10.10 24: eventuality(skc8, skc11) -> true % 10.69/10.10 25: thing(skc8, skc11) -> true % 10.69/10.10 26: specific(skc8, skc11) -> true % 10.69/10.10 27: singleton(skc8, skc11) -> true % 10.69/10.10 28: ifeq2(eventuality(X, Y), true, nonexistent(X, Y), true) -> true % 10.69/10.10 29: nonexistent(skc8, skc11) -> true % 10.69/10.10 30: ifeq2(desire_want(X, Y), true, event(X, Y), true) -> true % 10.69/10.10 31: event(skc6, skc7) -> true % 10.69/10.10 32: eventuality(skc6, skc7) -> true % 10.69/10.10 33: true -> nonexistent(skc6, skc7) % 10.69/10.10 34: thing(skc6, skc7) -> nonexistent(skc6, skc7) % 10.69/10.10 35: specific(skc6, skc7) -> nonexistent(skc6, skc7) % 10.69/10.10 36: singleton(skc6, skc7) -> nonexistent(skc6, skc7) % 10.69/10.10 37: ifeq2(desire_want(skc8, skc11), nonexistent(skc6, skc7), nonexistent(skc6, skc7), nonexistent(skc6, skc7)) -> nonexistent(skc6, skc7) % 10.69/10.10 38: ifeq2(dance(skc6, skc7), nonexistent(skc6, skc7), nonexistent(skc6, skc7), nonexistent(skc6, skc7)) -> nonexistent(skc6, skc7) % 10.69/10.10 40: ifeq2(eventuality(X, Y), nonexistent(skc6, skc7), unisex(X, Y), nonexistent(skc6, skc7)) -> nonexistent(skc6, skc7) % 10.69/10.10 41: unisex(skc8, skc11) -> nonexistent(skc6, skc7) % 10.69/10.10 42: nonexistent(skc6, skc7) -> unisex(skc6, skc7) % 10.69/10.10 44: ifeq2(proposition(X, Y), unisex(skc6, skc7), relation(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 45: relation(skc6, skc8) -> unisex(skc6, skc7) % 10.69/10.10 47: ifeq2(abstraction(X, Y), unisex(skc6, skc7), nonhuman(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 49: ifeq2(relation(X, Y), unisex(skc6, skc7), abstraction(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 50: abstraction(skc6, skc8) -> unisex(skc6, skc7) % 10.69/10.10 51: nonhuman(skc6, skc8) -> unisex(skc6, skc7) % 10.69/10.10 53: ifeq2(abstraction(X, Y), unisex(skc6, skc7), thing(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 54: thing(skc6, skc8) -> unisex(skc6, skc7) % 10.69/10.10 55: singleton(skc6, skc8) -> unisex(skc6, skc7) % 10.69/10.10 57: ifeq2(abstraction(X, Y), unisex(skc6, skc7), general(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 58: general(skc6, skc8) -> unisex(skc6, skc7) % 10.69/10.10 60: ifeq2(forename(X, Y), unisex(skc6, skc7), relname(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 61: relname(skc6, skc9) -> unisex(skc6, skc7) % 10.69/10.10 63: ifeq2(abstraction(X, Y), unisex(skc6, skc7), unisex(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 64: unisex(skc6, skc8) -> unisex(skc6, skc7) % 10.69/10.10 66: ifeq2(relname(X, Y), unisex(skc6, skc7), relation(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 67: relation(skc6, skc9) -> unisex(skc6, skc7) % 10.69/10.10 68: abstraction(skc6, skc9) -> unisex(skc6, skc7) % 10.69/10.10 69: unisex(skc6, skc9) -> unisex(skc6, skc7) % 10.69/10.10 70: general(skc6, skc9) -> unisex(skc6, skc7) % 10.69/10.10 71: thing(skc6, skc9) -> unisex(skc6, skc7) % 10.69/10.10 72: nonhuman(skc6, skc9) -> unisex(skc6, skc7) % 10.69/10.10 73: singleton(skc6, skc9) -> unisex(skc6, skc7) % 10.69/10.10 75: ifeq2(organism(X, Y), unisex(skc6, skc7), entity(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 77: ifeq2(woman(X, Y), unisex(skc6, skc7), human_person(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 78: human_person(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 80: ifeq2(human_person(X, Y), unisex(skc6, skc7), organism(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 81: organism(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 82: entity(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 84: ifeq2(mia_forename(X, Y), unisex(skc6, skc7), forename(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 86: ifeq2(entity(X, Y), unisex(skc6, skc7), thing(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 87: thing(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 88: singleton(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 90: ifeq2(entity(X, Y), unisex(skc6, skc7), existent(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 91: existent(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 93: ifeq2(entity(X, Y), unisex(skc6, skc7), specific(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 94: specific(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 96: ifeq2(organism(X, Y), unisex(skc6, skc7), impartial(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 97: impartial(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 99: ifeq2(human_person(X, Y), unisex(skc6, skc7), animate(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 100: animate(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 102: ifeq2(human_person(X, Y), unisex(skc6, skc7), human(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 103: human(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 105: ifeq2(organism(X, Y), unisex(skc6, skc7), living(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 106: living(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 108: ifeq2(woman(X, Y), unisex(skc6, skc7), female(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 109: female(skc6, skc10) -> unisex(skc6, skc7) % 10.69/10.10 111: ifeq(tuple(unisex(X, Y), female(X, Y)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 113: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 115: ifeq(tuple(nonhuman(X, Y), human(X, Y)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 117: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 119: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(female(X, Z), unisex(skc6, skc7), female(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 120: ifeq2(female(skc6, X), unisex(skc6, skc7), female(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 121: female(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 123: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(existent(X, Z), unisex(skc6, skc7), existent(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 124: ifeq2(existent(skc6, X), unisex(skc6, skc7), existent(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 125: existent(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 127: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(organism(X, Z), unisex(skc6, skc7), organism(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 128: ifeq2(organism(skc6, X), unisex(skc6, skc7), organism(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 129: organism(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 130: living(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 131: impartial(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 132: entity(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 133: specific(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 134: thing(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 135: singleton(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 137: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(impartial(X, Z), unisex(skc6, skc7), impartial(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 138: ifeq2(impartial(skc6, X), unisex(skc6, skc7), impartial(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 140: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(entity(X, Z), unisex(skc6, skc7), entity(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 141: ifeq2(entity(skc6, X), unisex(skc6, skc7), entity(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 143: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(human(X, Z), unisex(skc6, skc7), human(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 144: ifeq2(human(skc6, X), unisex(skc6, skc7), human(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 145: human(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 147: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(living(X, Z), unisex(skc6, skc7), living(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 148: ifeq2(living(skc6, X), unisex(skc6, skc7), living(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 150: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(animate(X, Z), unisex(skc6, skc7), animate(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 151: ifeq2(animate(skc6, X), unisex(skc6, skc7), animate(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 152: animate(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 154: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(event(X, Z), unisex(skc6, skc7), event(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 155: ifeq2(event(skc6, X), unisex(skc6, skc7), event(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 156: event(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 157: eventuality(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 158: unisex(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 159: nonexistent(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 160: thing(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 161: specific(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 162: singleton(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 163: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), event(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 165: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(dance(X, Z), unisex(skc6, skc7), dance(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 166: ifeq2(dance(skc6, X), unisex(skc6, skc7), dance(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 167: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), dance(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 169: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(eventuality(X, Z), unisex(skc6, skc7), eventuality(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 170: ifeq2(eventuality(skc6, X), unisex(skc6, skc7), eventuality(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 172: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(unisex(X, Z), unisex(skc6, skc7), unisex(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 173: ifeq2(unisex(skc6, X), unisex(skc6, skc7), unisex(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 174: unisex(skc8, skc8) -> unisex(skc6, skc7) % 10.69/10.10 175: unisex(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 176: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), unisex(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 178: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(specific(X, Z), unisex(skc6, skc7), specific(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 179: ifeq2(specific(skc6, X), unisex(skc6, skc7), specific(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 181: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(nonexistent(X, Z), unisex(skc6, skc7), nonexistent(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 182: ifeq2(nonexistent(skc6, X), unisex(skc6, skc7), nonexistent(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 184: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(singleton(X, Z), unisex(skc6, skc7), singleton(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 185: ifeq2(singleton(skc6, X), unisex(skc6, skc7), singleton(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 186: singleton(skc8, skc8) -> unisex(skc6, skc7) % 10.69/10.10 187: singleton(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 189: ifeq2(present(X, Y), unisex(skc6, skc7), ifeq2(accessible_world(X, Z), unisex(skc6, skc7), present(Z, Y), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 190: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), present(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 191: present(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 192: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), present(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 193: ifeq2(present(skc6, X), unisex(skc6, skc7), present(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 195: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(proposition(X, Z), unisex(skc6, skc7), proposition(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 196: ifeq2(proposition(skc6, X), unisex(skc6, skc7), proposition(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 197: proposition(skc8, skc8) -> unisex(skc6, skc7) % 10.69/10.10 198: relation(skc8, skc8) -> unisex(skc6, skc7) % 10.69/10.10 199: abstraction(skc8, skc8) -> unisex(skc6, skc7) % 10.69/10.10 200: general(skc8, skc8) -> unisex(skc6, skc7) % 10.69/10.10 201: thing(skc8, skc8) -> unisex(skc6, skc7) % 10.69/10.10 202: nonhuman(skc8, skc8) -> unisex(skc6, skc7) % 10.69/10.10 203: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), proposition(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 205: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(relation(X, Z), unisex(skc6, skc7), relation(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 206: ifeq2(relation(skc6, X), unisex(skc6, skc7), relation(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 207: relation(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 208: abstraction(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 209: general(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 210: thing(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 211: nonhuman(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 213: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(desire_want(X, Z), unisex(skc6, skc7), desire_want(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 214: ifeq2(desire_want(skc6, X), unisex(skc6, skc7), desire_want(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 215: desire_want(skc8, skc7) -> unisex(skc6, skc7) % 10.69/10.10 216: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), desire_want(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 218: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(general(X, Z), unisex(skc6, skc7), general(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 219: ifeq2(general(skc6, X), unisex(skc6, skc7), general(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 221: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(abstraction(X, Z), unisex(skc6, skc7), abstraction(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 222: ifeq2(abstraction(skc6, X), unisex(skc6, skc7), abstraction(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 224: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(forename(X, Z), unisex(skc6, skc7), forename(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 225: ifeq2(forename(skc6, X), unisex(skc6, skc7), forename(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 226: forename(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 227: relname(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 228: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), forename(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 230: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(nonhuman(X, Z), unisex(skc6, skc7), nonhuman(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 231: ifeq2(nonhuman(skc6, X), unisex(skc6, skc7), nonhuman(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 233: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(mia_forename(X, Z), unisex(skc6, skc7), mia_forename(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 234: ifeq2(mia_forename(skc6, X), unisex(skc6, skc7), mia_forename(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 235: mia_forename(skc8, skc9) -> unisex(skc6, skc7) % 10.69/10.10 236: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), mia_forename(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 238: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(relname(X, Z), unisex(skc6, skc7), relname(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 239: ifeq2(relname(skc6, X), unisex(skc6, skc7), relname(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 241: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(woman(X, Z), unisex(skc6, skc7), woman(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 242: ifeq2(woman(skc6, X), unisex(skc6, skc7), woman(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 243: woman(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 244: human_person(skc8, skc10) -> unisex(skc6, skc7) % 10.69/10.10 245: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), woman(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 247: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(human_person(X, Z), unisex(skc6, skc7), human_person(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 248: ifeq2(human_person(skc6, X), unisex(skc6, skc7), human_person(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 250: ifeq2(accessible_world(X, Y), unisex(skc6, skc7), ifeq2(thing(X, Z), unisex(skc6, skc7), thing(Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 251: ifeq2(thing(skc6, X), unisex(skc6, skc7), thing(skc8, X), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 252: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), human_person(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 253: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), event(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 254: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), female(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 255: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), relation(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 256: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), relname(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 257: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), eventuality(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 258: ifeq2(eventuality(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 259: ifeq2(relname(skc6, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 260: ifeq2(accessible_world(skc8, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 261: ifeq2(event(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 262: ifeq2(present(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 263: ifeq2(dance(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 264: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), animate(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 265: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), present(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 266: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), thing(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 267: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), eventuality(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 268: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), specific(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 269: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), proposition(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 270: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), female(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 271: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), unisex(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 272: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), mia_forename(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 273: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), desire_want(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 274: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), nonexistent(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 275: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), forename(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 276: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), abstraction(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 277: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), relation(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 278: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), woman(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 279: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), event(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 280: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), human(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 281: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), organism(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 282: ifeq2(eventuality(X, Y), unisex(skc6, skc7), specific(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 283: ifeq2(thing(X, Y), unisex(skc6, skc7), singleton(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 284: ifeq2(dance(X, Y), unisex(skc6, skc7), event(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 285: ifeq2(desire_want(X, Y), unisex(skc6, skc7), event(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 286: ifeq2(eventuality(X, Y), unisex(skc6, skc7), nonexistent(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 287: ifeq2(event(X, Y), unisex(skc6, skc7), eventuality(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 288: ifeq2(eventuality(X, Y), unisex(skc6, skc7), thing(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 289: ifeq2(unisex(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 290: ifeq2(eventuality(X, Y), unisex(skc6, skc7), unisex(X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 291: ifeq2(abstraction(skc8, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 292: ifeq2(entity(skc8, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 293: ifeq2(dance(skc8, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 294: ifeq2(nonexistent(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 295: ifeq2(thing(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 296: ifeq2(specific(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 297: ifeq2(proposition(skc6, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 298: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), eventuality(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 299: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), living(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 300: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), thing(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 301: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), thing(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 302: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), specific(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 303: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), relation(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 304: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), entity(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 305: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), impartial(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 306: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), nonexistent(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 307: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), general(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 308: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), abstraction(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 309: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), nonhuman(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 310: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), relname(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 311: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), animate(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 312: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), singleton(X, skc11), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 313: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), human(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 314: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), organism(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 315: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), relation(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 316: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), human_person(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 317: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), unisex(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 318: ifeq2(accessible_world(skc8, skc6), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 319: ifeq2(desire_want(skc8, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 320: ifeq2(dance(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 321: ifeq2(entity(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 322: ifeq2(entity(skc6, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 323: ifeq2(singleton(skc6, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 324: ifeq2(eventuality(skc6, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 325: ifeq2(proposition(skc8, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 326: ifeq2(relname(skc8, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 328: ifeq2(theme(X, Y, Z), unisex(skc6, skc7), ifeq2(accessible_world(X, W), unisex(skc6, skc7), theme(W, Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 329: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), theme(X, skc7, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 330: theme(skc8, skc7, skc8) -> unisex(skc6, skc7) % 10.69/10.10 331: ifeq2(theme(skc6, X, Y), unisex(skc6, skc7), theme(skc8, X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 333: ifeq2(agent(X, Y, Z), unisex(skc6, skc7), ifeq2(accessible_world(X, W), unisex(skc6, skc7), agent(W, Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 334: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), agent(X, skc7, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 335: agent(skc8, skc7, skc10) -> unisex(skc6, skc7) % 10.69/10.10 336: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), agent(X, skc11, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 337: ifeq2(agent(skc6, X, Y), unisex(skc6, skc7), agent(skc8, X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 338: ifeq2(agent(skc6, skc11, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 340: ifeq2(of(X, Y, Z), unisex(skc6, skc7), ifeq2(accessible_world(X, W), unisex(skc6, skc7), of(W, Y, Z), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 341: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), of(X, skc9, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 342: of(skc8, skc9, skc10) -> unisex(skc6, skc7) % 10.69/10.10 343: ifeq2(of(skc6, X, Y), unisex(skc6, skc7), of(skc8, X, Y), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 344: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), agent(X, skc7, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 345: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), of(X, skc9, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 346: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), theme(X, skc7, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 347: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), thing(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 348: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), existent(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 349: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), specific(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 350: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), thing(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 351: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), general(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 352: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), impartial(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 353: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), entity(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 354: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), thing(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 355: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), unisex(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 356: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), unisex(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 357: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), nonhuman(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 358: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), abstraction(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 359: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), singleton(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 360: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), singleton(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 361: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), abstraction(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 362: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), nonexistent(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 363: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), unisex(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 364: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), specific(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 365: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), living(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 366: ifeq2(entity(skc8, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 367: ifeq2(eventuality(skc6, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 368: ifeq2(eventuality(skc8, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 369: ifeq2(abstraction(skc8, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 370: ifeq2(eventuality(skc6, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 371: ifeq2(abstraction(skc6, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 372: ifeq2(entity(skc6, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 373: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), specific(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 374: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), singleton(X, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 375: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), thing(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 376: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), thing(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 377: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), existent(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 378: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), thing(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 379: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), singleton(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 380: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), unisex(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 381: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), general(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 382: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), general(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 383: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), singleton(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 384: ifeq2(accessible_world(skc6, X), unisex(skc6, skc7), singleton(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 385: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), nonhuman(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 386: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), nonhuman(X, skc8), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 387: ifeq2(entity(skc8, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 388: ifeq2(eventuality(skc8, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 389: ifeq2(abstraction(skc8, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 390: ifeq2(eventuality(skc8, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 391: ifeq2(entity(skc8, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 392: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), singleton(X, skc9), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 393: ifeq2(accessible_world(skc8, X), unisex(skc6, skc7), singleton(X, skc10), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 394: ifeq(tuple(unisex(skc6, skc10), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 395: ifeq(tuple(nonhuman(skc6, skc10), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 396: ifeq(tuple(unisex(skc6, skc7), general(skc8, skc11)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 397: ifeq(tuple(unisex(skc6, skc7), existent(skc8, skc11)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 398: ifeq(tuple(unisex(skc6, skc7), female(skc8, skc11)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 399: ifeq(tuple(unisex(skc8, skc10), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 400: ifeq(tuple(unisex(skc6, skc7), existent(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 401: ifeq(tuple(unisex(skc6, skc7), general(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 402: ifeq(tuple(specific(skc6, skc8), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 403: ifeq(tuple(unisex(skc6, skc7), human(skc6, skc8)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 404: ifeq(tuple(nonhuman(skc8, skc10), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 405: ifeq(tuple(unisex(skc6, skc7), female(skc6, skc8)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 406: ifeq(tuple(unisex(skc6, skc7), female(skc6, skc9)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 407: ifeq(tuple(unisex(skc6, skc7), general(skc8, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 408: ifeq(tuple(unisex(skc6, skc7), general(skc6, skc10)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 409: ifeq(tuple(unisex(skc6, skc7), female(skc8, skc8)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 410: ifeq(tuple(nonexistent(skc6, skc10), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 411: ifeq(tuple(unisex(skc6, skc7), human(skc6, skc9)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 412: ifeq(tuple(specific(skc6, skc9), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 413: ifeq(tuple(unisex(skc6, skc7), existent(skc8, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 414: ifeq(tuple(unisex(skc6, skc7), female(skc8, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 415: ifeq(tuple(unisex(skc6, skc7), human(skc8, skc8)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 416: ifeq(tuple(specific(skc8, skc8), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 417: ifeq(tuple(unisex(skc6, skc7), female(skc8, skc9)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 418: ifeq(tuple(nonexistent(skc8, skc10), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 419: ifeq(tuple(unisex(skc6, skc7), human(skc8, skc9)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 420: ifeq(tuple(specific(skc8, skc9), unisex(skc6, skc7)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 421: ifeq(tuple(unisex(skc6, skc7), general(skc8, skc10)), tuple(unisex(skc6, skc7), unisex(skc6, skc7)), a, b) -> b % 10.69/10.10 422: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(forename(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 423: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(woman(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 424: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(proposition(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 425: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(event(X, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 426: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(mia_forename(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 427: ifeq2(present(X, skc11), unisex(skc6, skc7), ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 428: ifeq2(present(X, skc7), unisex(skc6, skc7), ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 429: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(desire_want(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 430: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(dance(X, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 431: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(human_person(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 432: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(relation(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 433: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(eventuality(X, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 434: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(female(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 435: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(event(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 436: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(relname(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 437: ifeq2(agent(X, skc11, skc10), unisex(skc6, skc7), ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 438: ifeq2(agent(X, skc7, skc10), unisex(skc6, skc7), ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 439: ifeq2(theme(X, skc7, skc8), unisex(skc6, skc7), ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 440: ifeq2(of(X, skc9, skc10), unisex(skc6, skc7), ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 441: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(female(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 442: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(proposition(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 443: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(abstraction(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 444: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(specific(X, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 445: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(forename(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 446: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(human(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 447: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(organism(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 448: ifeq2(present(X, skc7), unisex(skc6, skc7), ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 449: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(unisex(X, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 450: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(event(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 451: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(eventuality(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 452: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(mia_forename(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 453: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(animate(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 454: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(woman(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 455: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(desire_want(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 456: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(relation(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 457: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(nonexistent(X, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 458: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(thing(X, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 459: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(nonexistent(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 460: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(thing(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 461: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(thing(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 462: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(nonhuman(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 463: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(relation(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 464: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(unisex(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 465: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(human_person(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 466: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(eventuality(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 467: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(human(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 468: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(relation(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 469: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(relname(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 470: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(singleton(X, skc11), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 471: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(abstraction(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 472: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(animate(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 473: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(organism(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 474: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(general(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 475: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(entity(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 476: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(impartial(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 477: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(living(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 478: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(specific(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 479: ifeq2(theme(X, skc7, skc8), unisex(skc6, skc7), ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 480: ifeq2(of(X, skc9, skc10), unisex(skc6, skc7), ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 481: ifeq2(agent(X, skc7, skc10), unisex(skc6, skc7), ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 482: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(nonhuman(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 483: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(specific(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 484: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(unisex(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 485: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(abstraction(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 486: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(thing(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 487: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(existent(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 488: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(impartial(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 489: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(abstraction(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 490: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(general(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 491: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(thing(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 492: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(thing(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 493: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(unisex(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 494: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(living(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 495: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(specific(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 496: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(unisex(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 497: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(entity(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 498: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(nonexistent(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 499: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(singleton(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 500: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(singleton(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 501: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(singleton(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 502: ifeq2(accessible_world(X, skc6), unisex(skc6, skc7), ifeq2(singleton(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 503: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(singleton(X, skc7), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 504: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(nonhuman(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 505: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(nonhuman(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 506: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(thing(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 507: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(thing(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 508: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(specific(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 509: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(thing(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 510: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(unisex(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 511: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(general(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 512: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(general(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 513: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(existent(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 514: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(singleton(X, skc8), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 515: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(singleton(X, skc9), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 516: ifeq2(accessible_world(X, skc8), unisex(skc6, skc7), ifeq2(singleton(X, skc10), unisex(skc6, skc7), unisex(skc6, skc7), unisex(skc6, skc7)), unisex(skc6, skc7)) -> unisex(skc6, skc7) % 10.69/10.10 518: ifeq3(of(X, Y, Z), unisex(skc6, skc7), ifeq3(of(X, W, Z), unisex(skc6, skc7), ifeq3(entity(X, Z), unisex(skc6, skc7), ifeq3(forename(X, Y), unisex(skc6, skc7), ifeq3(forename(X, W), unisex(skc6, skc7), Y, W), W), W), W), W) -> W % 10.69/10.10 519: ifeq3(of(skc6, X, skc10), unisex(skc6, skc7), ifeq3(forename(skc6, X), unisex(skc6, skc7), skc9, X), X) -> X % 10.69/10.10 520: ifeq3(of(skc6, X, skc10), unisex(skc6, skc7), ifeq3(forename(skc6, X), unisex(skc6, skc7), X, skc9), skc9) -> skc9 % 10.69/10.10 521: ifeq3(of(skc8, X, skc10), unisex(skc6, skc7), ifeq3(forename(skc8, X), unisex(skc6, skc7), skc9, X), X) -> X % 10.69/10.10 522: ifeq3(of(skc8, X, skc10), unisex(skc6, skc7), ifeq3(forename(skc8, X), unisex(skc6, skc7), X, skc9), skc9) -> skc9 % 10.69/10.10 523: ifeq3(of(skc6, skc9, X), unisex(skc6, skc7), ifeq3(of(skc6, Y, X), unisex(skc6, skc7), ifeq3(entity(skc6, X), unisex(skc6, skc7), ifeq3(forename(skc6, Y), unisex(skc6, skc7), skc9, Y), Y), Y), Y) -> Y % 10.69/10.10 524: ifeq3(of(skc6, skc9, X), unisex(skc6, skc7), ifeq3(of(skc6, skc9, X), unisex(skc6, skc7), ifeq3(entity(skc6, X), unisex(skc6, skc7), skc9, skc9), skc9), skc9) -> skc9 % 10.69/10.10 525: ifeq3(of(skc6, X, Y), unisex(skc6, skc7), ifeq3(of(skc6, skc9, Y), unisex(skc6, skc7), ifeq3(entity(skc6, Y), unisex(skc6, skc7), ifeq3(forename(skc6, X), unisex(skc6, skc7), X, skc9), skc9), skc9), skc9) -> skc9 % 10.69/10.10 526: ifeq3(of(skc8, skc9, X), unisex(skc6, skc7), ifeq3(of(skc8, Y, X), unisex(skc6, skc7), ifeq3(entity(skc8, X), unisex(skc6, skc7), ifeq3(forename(skc8, Y), unisex(skc6, skc7), skc9, Y), Y), Y), Y) -> Y % 10.69/10.10 527: ifeq3(of(skc8, skc9, X), unisex(skc6, skc7), ifeq3(of(skc8, skc9, X), unisex(skc6, skc7), ifeq3(entity(skc8, X), unisex(skc6, skc7), skc9, skc9), skc9), skc9) -> skc9 % 10.69/10.10 528: ifeq3(of(skc8, X, Y), unisex(skc6, skc7), ifeq3(of(skc8, skc9, Y), unisex(skc6, skc7), ifeq3(entity(skc8, Y), unisex(skc6, skc7), ifeq3(forename(skc8, X), unisex(skc6, skc7), X, skc9), skc9), skc9), skc9) -> skc9 % 10.69/10.10 530: ifeq3(theme(X, Y, Z), unisex(skc6, skc7), ifeq3(theme(X, W, V), unisex(skc6, skc7), ifeq3(proposition(X, Z), unisex(skc6, skc7), ifeq3(proposition(X, V), unisex(skc6, skc7), ifeq3(desire_want(X, Y), unisex(skc6, skc7), ifeq3(desire_want(X, W), unisex(skc6, skc7), Z, V), V), V), V), V), V) -> V % 10.69/10.10 531: ifeq3(theme(skc6, X, Y), unisex(skc6, skc7), ifeq3(proposition(skc6, Y), unisex(skc6, skc7), ifeq3(desire_want(skc6, X), unisex(skc6, skc7), skc8, Y), Y), Y) -> Y % 10.69/10.10 532: ifeq3(theme(skc6, skc7, X), unisex(skc6, skc7), ifeq3(proposition(skc6, X), unisex(skc6, skc7), skc8, X), X) -> X % 10.69/10.10 533: ifeq3(theme(skc6, X, skc8), unisex(skc6, skc7), ifeq3(desire_want(skc6, X), unisex(skc6, skc7), skc8, skc8), skc8) -> skc8 % 10.69/10.10 534: ifeq3(theme(skc6, X, Y), unisex(skc6, skc7), ifeq3(proposition(skc6, Y), unisex(skc6, skc7), ifeq3(desire_want(skc6, X), unisex(skc6, skc7), Y, skc8), skc8), skc8) -> skc8 % 10.69/10.10 535: ifeq3(theme(skc6, skc7, X), unisex(skc6, skc7), ifeq3(proposition(skc6, X), unisex(skc6, skc7), X, skc8), skc8) -> skc8 % 10.69/10.10 536: ifeq3(theme(skc8, X, Y), unisex(skc6, skc7), ifeq3(proposition(skc8, Y), unisex(skc6, skc7), ifeq3(desire_want(skc8, X), unisex(skc6, skc7), skc8, Y), Y), Y) -> Y % 10.69/10.10 537: ifeq3(theme(skc8, skc7, X), unisex(skc6, skc7), ifeq3(proposition(skc8, X), unisex(skc6, skc7), skc8, X), X) -> X % 10.69/10.10 538: ifeq3(theme(skc8, X, skc8), unisex(skc6, skc7), ifeq3(desire_want(skc8, X), unisex(skc6, skc7), skc8, skc8), skc8) -> skc8 % 10.69/10.10 539: ifeq3(theme(skc8, X, Y), unisex(skc6, skc7), ifeq3(proposition(skc8, Y), unisex(skc6, skc7), ifeq3(desire_want(skc8, X), unisex(skc6, skc7), Y, skc8), skc8), skc8) -> skc8 % 10.69/10.10 540: ifeq3(theme(skc8, skc7, X), unisex(skc6, skc7), ifeq3(proposition(skc8, X), unisex(skc6, skc7), X, skc8), skc8) -> skc8 % 10.69/10.10 541: ifeq3(of(skc6, X, skc10), unisex(skc6, skc7), ifeq3(of(skc6, Y, skc10), unisex(skc6, skc7), ifeq3(forename(skc6, X), unisex(skc6, skc7), ifeq3(forename(skc6, Y), unisex(skc6, skc7), X, Y), Y), Y), Y) -> Y % 10.69/10.10 542: ifeq3(of(skc8, X, skc10), unisex(skc6, skc7), ifeq3(of(skc8, Y, skc10), unisex(skc6, skc7), ifeq3(forename(skc8, X), unisex(skc6, skc7), ifeq3(forename(skc8, Y), unisex(skc6, skc7), X, Y), Y), Y), Y) -> Y % 10.69/10.10 543: ifeq3(theme(skc6, X, Y), unisex(skc6, skc7), ifeq3(theme(skc6, skc7, Z), unisex(skc6, skc7), ifeq3(proposition(skc6, Y), unisex(skc6, skc7), ifeq3(proposition(skc6, Z), unisex(skc6, skc7), ifeq3(desire_want(skc6, X), unisex(skc6, skc7), Y, Z), Z), Z), Z), Z) -> Z % 10.69/10.10 544: ifeq3(theme(skc6, skc7, X), unisex(skc6, skc7), ifeq3(theme(skc6, skc7, Y), unisex(skc6, skc7), ifeq3(proposition(skc6, X), unisex(skc6, skc7), ifeq3(proposition(skc6, Y), unisex(skc6, skc7), X, Y), Y), Y), Y) -> Y % 10.69/10.10 545: ifeq3(theme(skc6, X, skc8), unisex(skc6, skc7), ifeq3(theme(skc6, skc7, Y), unisex(skc6, skc7), ifeq3(proposition(skc6, Y), unisex(skc6, skc7), ifeq3(desire_want(skc6, X), unisex(skc6, skc7), skc8, Y), Y), Y), Y) -> Y % 10.69/10.10 546: ifeq3(theme(skc6, skc7, X), unisex(skc6, skc7), ifeq3(theme(skc6, Y, Z), unisex(skc6, skc7), ifeq3(proposition(skc6, X), unisex(skc6, skc7), ifeq3(proposition(skc6, Z), unisex(skc6, skc7), ifeq3(desire_want(skc6, Y), unisex(skc6, skc7), X, Z), Z), Z), Z), Z) -> Z % 10.69/10.10 547: ifeq3(theme(skc6, skc7, X), unisex(skc6, skc7), ifeq3(theme(skc6, Y, skc8), unisex(skc6, skc7), ifeq3(proposition(skc6, X), unisex(skc6, skc7), ifeq3(desire_want(skc6, Y), unisex(skc6, skc7), X, skc8), skc8), skc8), skc8) -> skc8 % 10.69/10.10 548: ifeq3(theme(skc6, X, skc8), unisex(skc6, skc7), ifeq3(theme(skc6, Y, Z), unisex(skc6, skc7), ifeq3(proposition(skc6, Z), unisex(skc6, skc7), ifeq3(desire_want(skc6, X), unisex(skc6, skc7), ifeq3(desire_want(skc6, Y), unisex(skc6, skc7), skc8, Z), Z), Z), Z), Z) -> Z % 10.69/10.10 549: ifeq3(theme(skc6, X, skc8), unisex(skc6, skc7), ifeq3(theme(skc6, Y, skc8), unisex(skc6, skc7), ifeq3(desire_want(skc6, X), unisex(skc6, skc7), ifeq3(desire_want(skc6, Y), unisex(skc6, skc7), skc8, skc8), skc8), skc8), skc8) -> skc8 % 10.69/10.10 550: ifeq3(theme(skc6, X, Y), unisex(skc6, skc7), ifeq3(theme(skc6, Z, skc8), unisex(skc6, skc7), ifeq3(proposition(skc6, Y), unisex(skc6, skc7), ifeq3(desire_want(skc6, X), unisex(skc6, skc7), ifeq3(desire_want(skc6, Z), unisex(skc6, skc7), Y, skc8), skc8), skc8), skc8), skc8) -> skc8 % 10.69/10.10 551: ifeq3(theme(skc8, X, Y), unisex(skc6, skc7), ifeq3(theme(skc8, skc7, Z), unisex(skc6, skc7), ifeq3(proposition(skc8, Y), unisex(skc6, skc7), ifeq3(proposition(skc8, Z), unisex(skc6, skc7), ifeq3(desire_want(skc8, X), unisex(skc6, skc7), Y, Z), Z), Z), Z), Z) -> Z % 10.69/10.10 552: ifeq3(theme(skc8, skc7, X), unisex(skc6, skc7), ifeq3(theme(skc8, skc7, Y), unisex(skc6, skc7), ifeq3(proposition(skc8, X), unisex(skc6, skc7), ifeq3(proposition(skc8, Y), unisex(skc6, skc7), X, Y), Y), Y), Y) -> Y % 10.69/10.10 553: ifeq3(theme(skc8, X, skc8), unisex(skc6, skc7), ifeq3(theme(skc8, skc7, Y), unisex(skc6, skc7), ifeq3(proposition(skc8, Y), unisex(skc6, skc7), ifeq3(desire_want(skc8, X), unisex(skc6, skc7), skc8, Y), Y), Y), Y) -> Y % 10.69/10.10 554: ifeq3(theme(skc8, skc7, X), unisex(skc6, skc7), ifeq3(theme(skc8, Y, Z), unisex(skc6, skc7), ifeq3(proposition(skc8, X), unisex(skc6, skc7), ifeq3(proposition(skc8, Z), unisex(skc6, skc7), ifeq3(desire_want(skc8, Y), unisex(skc6, skc7), X, Z), Z), Z), Z), Z) -> Z % 10.69/10.10 555: ifeq3(theme(skc8, skc7, X), unisex(skc6, skc7), ifeq3(theme(skc8, Y, skc8), unisex(skc6, skc7), ifeq3(proposition(skc8, X), unisex(skc6, skc7), ifeq3(desire_want(skc8, Y), unisex(skc6, skc7), X, skc8), skc8), skc8), skc8) -> skc8 % 10.69/10.10 556: ifeq3(theme(skc8, X, skc8), unisex(skc6, skc7), ifeq3(theme(skc8, Y, Z), unisex(skc6, skc7), ifeq3(proposition(skc8, Z), unisex(skc6, skc7), ifeq3(desire_want(skc8, X), unisex(skc6, skc7), ifeq3(desire_want(skc8, Y), unisex(skc6, skc7), skc8, Z), Z), Z), Z), Z) -> Z % 10.69/10.10 557: ifeq3(theme(skc8, X, skc8), unisex(skc6, skc7), ifeq3(theme(skc8, Y, skc8), unisex(skc6, skc7), ifeq3(desire_want(skc8, X), unisex(skc6, skc7), ifeq3(desire_want(skc8, Y), unisex(skc6, skc7), skc8, skc8), skc8), skc8), skc8) -> skc8 % 10.69/10.10 558: ifeq3(theme(skc8, X, Y), unisex(skc6, skc7), ifeq3(theme(skc8, Z, skc8), unisex(skc6, skc7), ifeq3(proposition(skc8, Y), unisex(skc6, skc7), ifeq3(desire_want(skc8, X), unisex(skc6, skc7), ifeq3(desire_want(skc8, Z), unisex(skc6, skc7), Y, skc8), skc8), skc8), skc8), skc8) -> skc8 % 10.69/10.10 %------------------------------------------------------------------------------