%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP220-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jul 15 07:23:57 AM UTC 2025 % Result : Satisfiable 15.87s 15.36s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : NLP220-10 : TPTP v9.0.0. Released v7.3.0. % 0.00/0.10 % Command : run_Leo-III %s %d THM % 0.10/0.30 % Computer : n006.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Mon Jul 14 14:21:34 EDT 2025 % 0.10/0.30 % CPUTime : % 15.87/15.36 % SZS status Satisfiable % 15.87/15.36 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 15.87/15.36 1: actual_world(skc5) -> true % 15.87/15.36 2: man(skc5, skc9) -> true % 15.87/15.36 3: forename(skc5, skc8) -> true % 15.87/15.36 4: vincent_forename(skc5, skc8) -> true % 15.87/15.36 5: event(skc5, skc7) -> true % 15.87/15.36 6: present(skc5, skc7) -> true % 15.87/15.36 7: think_believe_consider(skc5, skc7) -> true % 15.87/15.36 8: accessible_world(skc5, skc6) -> true % 15.87/15.36 9: proposition(skc5, skc6) -> true % 15.87/15.36 10: of(skc5, skc8, skc9) -> true % 15.87/15.36 11: agent(skc5, skc7, skc9) -> true % 15.87/15.36 12: theme(skc5, skc7, skc6) -> true % 15.87/15.36 13: ifeq2(X, X, Y, Z) -> Y % 15.87/15.36 14: ifeq3(X, X, Y, Z) -> Y % 15.87/15.36 15: ifeq(X, X, Y, Z) -> Y % 15.87/15.36 16: ifeq2(thing(X, Y), true, singleton(X, Y), true) -> true % 15.87/15.36 17: ifeq2(event(X, Y), true, eventuality(X, Y), true) -> true % 15.87/15.36 18: eventuality(skc5, skc7) -> true % 15.87/15.36 19: ifeq2(eventuality(X, Y), true, thing(X, Y), true) -> true % 15.87/15.36 20: thing(skc5, skc7) -> true % 15.87/15.36 21: singleton(skc5, skc7) -> true % 15.87/15.36 22: ifeq2(smoke(X, Y), true, event(X, Y), true) -> true % 15.87/15.36 23: ifeq2(smoke(skc5, skc7), true, true, true) -> true % 15.87/15.36 24: ifeq2(eventuality(X, Y), true, specific(X, Y), true) -> true % 15.87/15.36 25: specific(skc5, skc7) -> true % 15.87/15.36 26: ifeq2(eventuality(X, Y), true, unisex(X, Y), true) -> true % 15.87/15.36 27: unisex(skc5, skc7) -> true % 15.87/15.36 28: ifeq2(eventuality(X, Y), true, nonexistent(X, Y), true) -> true % 15.87/15.36 29: nonexistent(skc5, skc7) -> true % 15.87/15.36 30: ifeq2(man(X, Y), true, human_person(X, Y), true) -> true % 15.87/15.36 31: human_person(skc5, skc9) -> true % 15.87/15.36 32: ifeq2(entity(X, Y), true, thing(X, Y), true) -> true % 15.87/15.36 33: ifeq2(organism(X, Y), true, entity(X, Y), true) -> true % 15.87/15.36 34: ifeq2(human_person(X, Y), true, organism(X, Y), true) -> true % 15.87/15.36 35: organism(skc5, skc9) -> true % 15.87/15.36 36: entity(skc5, skc9) -> true % 15.87/15.36 37: thing(skc5, skc9) -> true % 15.87/15.36 38: singleton(skc5, skc9) -> true % 15.87/15.36 39: ifeq2(entity(X, Y), true, specific(X, Y), true) -> true % 15.87/15.36 40: specific(skc5, skc9) -> true % 15.87/15.36 41: ifeq2(organism(X, Y), true, impartial(X, Y), true) -> true % 15.87/15.36 42: impartial(skc5, skc9) -> true % 15.87/15.36 43: ifeq2(entity(X, Y), true, existent(X, Y), true) -> true % 15.87/15.36 44: existent(skc5, skc9) -> true % 15.87/15.36 45: ifeq2(organism(X, Y), true, living(X, Y), true) -> true % 15.87/15.36 46: living(skc5, skc9) -> true % 15.87/15.36 47: ifeq2(proposition(X, Y), true, relation(X, Y), true) -> true % 15.87/15.36 48: relation(skc5, skc6) -> true % 15.87/15.36 49: ifeq2(human_person(X, Y), true, animate(X, Y), true) -> true % 15.87/15.36 50: animate(skc5, skc9) -> true % 15.87/15.36 51: ifeq2(man(X, Y), true, male(X, Y), true) -> true % 15.87/15.36 52: male(skc5, skc9) -> true % 15.87/15.36 53: ifeq2(human_person(X, Y), true, human(X, Y), true) -> true % 15.87/15.36 54: human(skc5, skc9) -> true % 15.87/15.36 55: ifeq2(relation(X, Y), true, abstraction(X, Y), true) -> true % 15.87/15.36 56: abstraction(skc5, skc6) -> true % 15.87/15.36 57: ifeq2(abstraction(X, Y), true, nonhuman(X, Y), true) -> true % 15.87/15.36 58: nonhuman(skc5, skc6) -> true % 15.87/15.36 59: ifeq2(abstraction(X, Y), true, thing(X, Y), true) -> true % 15.87/15.36 60: thing(skc5, skc6) -> true % 15.87/15.36 61: singleton(skc5, skc6) -> true % 15.87/15.36 62: ifeq2(abstraction(X, Y), true, general(X, Y), true) -> true % 15.87/15.36 63: general(skc5, skc6) -> true % 15.87/15.36 64: ifeq2(relname(X, Y), true, relation(X, Y), true) -> true % 15.87/15.36 65: ifeq2(relname(skc5, skc6), true, true, true) -> true % 15.87/15.36 66: ifeq2(abstraction(X, Y), true, unisex(X, Y), true) -> true % 15.87/15.36 67: unisex(skc5, skc6) -> true % 15.87/15.36 68: ifeq2(forename(X, Y), true, relname(X, Y), true) -> true % 15.87/15.36 69: relname(skc5, skc8) -> true % 15.87/15.36 70: relation(skc5, skc8) -> true % 15.87/15.36 71: abstraction(skc5, skc8) -> true % 15.87/15.36 72: unisex(skc5, skc8) -> true % 15.87/15.36 73: general(skc5, skc8) -> true % 15.87/15.36 74: thing(skc5, skc8) -> true % 15.87/15.36 75: nonhuman(skc5, skc8) -> true % 15.87/15.36 76: singleton(skc5, skc8) -> true % 15.87/15.36 77: ifeq2(vincent_forename(X, Y), true, forename(X, Y), true) -> true % 15.87/15.36 78: ifeq2(proposition(skc5, skc8), true, true, true) -> true % 15.87/15.36 79: ifeq2(abstraction(skc5, skc7), true, true, true) -> true % 15.87/15.36 80: ifeq2(entity(skc5, skc7), true, true, true) -> true % 15.87/15.36 81: ifeq2(eventuality(skc5, skc6), true, true, true) -> true % 15.87/15.36 82: ifeq2(entity(skc5, skc6), true, true, true) -> true % 15.87/15.36 83: ifeq2(man(skc6, X), true, smoke(skc6, skf1(Y)), true) -> true % 15.87/15.36 84: ifeq2(man(skc6, X), true, present(skc6, skf1(Y)), true) -> true % 15.87/15.36 85: ifeq2(man(skc6, X), true, event(skc6, skf1(Y)), true) -> true % 15.87/15.36 86: ifeq2(eventuality(skc5, skc8), true, true, true) -> true % 15.87/15.36 87: ifeq2(eventuality(skc5, skc9), true, true, true) -> true % 15.87/15.36 88: ifeq2(entity(skc5, skc8), true, true, true) -> true % 15.87/15.36 89: ifeq2(abstraction(skc5, skc9), true, true, true) -> true % 15.87/15.36 90: ifeq2(man(skc6, X), true, agent(skc6, skf1(X), X), true) -> true % 15.87/15.36 91: ifeq(tuple(unisex(X, Y), male(X, Y)), tuple(true, true), a, b) -> b % 15.87/15.36 92: ifeq(tuple(unisex(skc5, skc9), true), tuple(true, true), a, b) -> b % 15.87/15.36 93: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(true, true), a, b) -> b % 15.87/15.36 94: ifeq(tuple(human(X, Y), nonhuman(X, Y)), tuple(true, true), a, b) -> b % 15.87/15.36 95: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(true, true), a, b) -> b % 15.87/15.36 96: ifeq(tuple(true, existent(skc5, skc7)), tuple(true, true), a, b) -> b % 15.87/15.36 97: ifeq(tuple(true, nonhuman(skc5, skc9)), tuple(true, true), a, b) -> b % 15.87/15.36 98: ifeq(tuple(true, general(skc5, skc7)), tuple(true, true), a, b) -> b % 15.87/15.36 99: ifeq(tuple(true, male(skc5, skc7)), tuple(true, true), a, b) -> b % 15.87/15.36 100: ifeq(tuple(true, male(skc5, skc6)), tuple(true, true), a, b) -> b % 15.87/15.36 101: ifeq(tuple(human(skc5, skc6), true), tuple(true, true), a, b) -> b % 15.87/15.36 102: ifeq(tuple(specific(skc5, skc6), true), tuple(true, true), a, b) -> b % 15.87/15.36 103: ifeq(tuple(specific(skc5, skc8), true), tuple(true, true), a, b) -> b % 15.87/15.36 104: ifeq(tuple(true, general(skc5, skc9)), tuple(true, true), a, b) -> b % 15.87/15.36 105: ifeq(tuple(nonexistent(skc5, skc9), true), tuple(true, true), a, b) -> b % 15.87/15.36 106: ifeq(tuple(human(skc5, skc8), true), tuple(true, true), a, b) -> b % 15.87/15.36 107: ifeq(tuple(true, male(skc5, skc8)), tuple(true, true), a, b) -> b % 15.87/15.36 108: ifeq2(accessible_world(X, Y), true, ifeq2(thing(X, Z), true, thing(Y, Z), true), true) -> true % 15.87/15.36 109: ifeq2(thing(skc5, X), true, thing(skc6, X), true) -> true % 15.87/15.36 110: true -> thing(skc6, skc7) % 15.87/15.36 111: thing(skc6, skc7) -> thing(skc6, skc6) % 15.87/15.36 112: thing(skc6, skc6) -> thing(skc6, skc8) % 15.87/15.36 113: thing(skc6, skc8) -> thing(skc6, skc9) % 15.87/15.36 114: singleton(skc6, skc7) -> thing(skc6, skc9) % 15.87/15.36 115: thing(skc6, skc9) -> singleton(skc6, skc8) % 15.87/15.36 116: singleton(skc6, skc6) -> singleton(skc6, skc8) % 15.87/15.36 117: singleton(skc6, skc8) -> singleton(skc6, skc9) % 15.87/15.36 118: ifeq2(accessible_world(skc5, X), singleton(skc6, skc9), thing(X, skc7), singleton(skc6, skc9)) -> singleton(skc6, skc9) % 15.87/15.36 119: ifeq2(accessible_world(skc5, X), singleton(skc6, skc9), thing(X, skc6), singleton(skc6, skc9)) -> singleton(skc6, skc9) % 15.87/15.36 120: ifeq2(accessible_world(skc5, X), singleton(skc6, skc9), thing(X, skc8), singleton(skc6, skc9)) -> singleton(skc6, skc9) % 15.87/15.36 121: ifeq2(accessible_world(skc5, X), singleton(skc6, skc9), thing(X, skc9), singleton(skc6, skc9)) -> singleton(skc6, skc9) % 15.87/15.36 123: ifeq2(accessible_world(X, Y), singleton(skc6, skc9), ifeq2(unisex(X, Z), singleton(skc6, skc9), unisex(Y, Z), singleton(skc6, skc9)), singleton(skc6, skc9)) -> singleton(skc6, skc9) % 15.87/15.36 124: ifeq2(unisex(skc5, X), singleton(skc6, skc9), unisex(skc6, X), singleton(skc6, skc9)) -> singleton(skc6, skc9) % 15.87/15.36 125: unisex(skc6, skc7) -> singleton(skc6, skc9) % 15.87/15.36 126: unisex(skc6, skc6) -> singleton(skc6, skc9) % 15.87/15.36 127: unisex(skc6, skc8) -> singleton(skc6, skc9) % 15.87/15.36 129: ifeq2(accessible_world(X, Y), singleton(skc6, skc9), ifeq2(specific(X, Z), singleton(skc6, skc9), specific(Y, Z), singleton(skc6, skc9)), singleton(skc6, skc9)) -> singleton(skc6, skc9) % 15.87/15.36 130: ifeq2(specific(skc5, X), singleton(skc6, skc9), specific(skc6, X), singleton(skc6, skc9)) -> singleton(skc6, skc9) % 15.87/15.36 131: specific(skc6, skc7) -> singleton(skc6, skc9) % 15.87/15.36 132: singleton(skc6, skc9) -> specific(skc6, skc9) % 15.87/15.36 134: ifeq2(accessible_world(X, Y), specific(skc6, skc9), ifeq2(singleton(X, Z), specific(skc6, skc9), singleton(Y, Z), specific(skc6, skc9)), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 135: ifeq2(singleton(skc5, X), specific(skc6, skc9), singleton(skc6, X), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 137: ifeq2(present(X, Y), specific(skc6, skc9), ifeq2(accessible_world(X, Z), specific(skc6, skc9), present(Z, Y), specific(skc6, skc9)), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 138: ifeq2(accessible_world(skc5, X), specific(skc6, skc9), present(X, skc7), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 139: present(skc6, skc7) -> specific(skc6, skc9) % 15.87/15.36 140: ifeq2(present(skc5, X), specific(skc6, skc9), present(skc6, X), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 142: ifeq2(accessible_world(X, Y), specific(skc6, skc9), ifeq2(nonexistent(X, Z), specific(skc6, skc9), nonexistent(Y, Z), specific(skc6, skc9)), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 143: ifeq2(nonexistent(skc5, X), specific(skc6, skc9), nonexistent(skc6, X), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 144: nonexistent(skc6, skc7) -> specific(skc6, skc9) % 15.87/15.36 146: ifeq2(accessible_world(X, Y), specific(skc6, skc9), ifeq2(human_person(X, Z), specific(skc6, skc9), human_person(Y, Z), specific(skc6, skc9)), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 147: ifeq2(human_person(skc5, X), specific(skc6, skc9), human_person(skc6, X), specific(skc6, skc9)) -> specific(skc6, skc9) % 15.87/15.36 148: specific(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 150: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(man(X, Z), human_person(skc6, skc9), man(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 151: ifeq2(man(skc5, X), human_person(skc6, skc9), man(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 152: man(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 153: male(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 154: present(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 155: smoke(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 156: event(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 157: eventuality(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 158: nonexistent(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 159: specific(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 160: unisex(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 161: thing(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 162: agent(skc6, skf1(skc9), skc9) -> human_person(skc6, skc9) % 15.87/15.36 163: singleton(skc6, skf1(X)) -> human_person(skc6, skc9) % 15.87/15.36 164: ifeq2(accessible_world(skc5, X), human_person(skc6, skc9), man(X, skc9), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 166: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(organism(X, Z), human_person(skc6, skc9), organism(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 167: ifeq2(organism(skc5, X), human_person(skc6, skc9), organism(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 168: organism(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 169: living(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 170: impartial(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 171: entity(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 172: existent(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 174: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(impartial(X, Z), human_person(skc6, skc9), impartial(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 175: ifeq2(impartial(skc5, X), human_person(skc6, skc9), impartial(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 177: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(existent(X, Z), human_person(skc6, skc9), existent(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 178: ifeq2(existent(skc5, X), human_person(skc6, skc9), existent(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 180: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(entity(X, Z), human_person(skc6, skc9), entity(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 181: ifeq2(entity(skc5, X), human_person(skc6, skc9), entity(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 183: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(living(X, Z), human_person(skc6, skc9), living(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 184: ifeq2(living(skc5, X), human_person(skc6, skc9), living(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 186: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(animate(X, Z), human_person(skc6, skc9), animate(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 187: ifeq2(animate(skc5, X), human_person(skc6, skc9), animate(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 188: animate(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 190: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(male(X, Z), human_person(skc6, skc9), male(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 191: ifeq2(male(skc5, X), human_person(skc6, skc9), male(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 193: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(human(X, Z), human_person(skc6, skc9), human(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 194: ifeq2(human(skc5, X), human_person(skc6, skc9), human(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 195: human(skc6, skc9) -> human_person(skc6, skc9) % 15.87/15.36 197: ifeq2(accessible_world(X, Y), human_person(skc6, skc9), ifeq2(vincent_forename(X, Z), human_person(skc6, skc9), vincent_forename(Y, Z), human_person(skc6, skc9)), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 198: ifeq2(vincent_forename(skc5, X), human_person(skc6, skc9), vincent_forename(skc6, X), human_person(skc6, skc9)) -> human_person(skc6, skc9) % 15.87/15.36 199: vincent_forename(skc6, skc8) -> human_person(skc6, skc9) % 15.87/15.36 200: forename(skc6, skc8) -> human_person(skc6, skc9) % 15.87/15.36 201: relname(skc6, skc8) -> human_person(skc6, skc9) % 15.87/15.36 202: human_person(skc6, skc9) -> relation(skc6, skc8) % 15.87/15.36 203: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), vincent_forename(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 205: ifeq2(think_believe_consider(X, Y), relation(skc6, skc8), ifeq2(accessible_world(X, Z), relation(skc6, skc8), think_believe_consider(Z, Y), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 206: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), think_believe_consider(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 207: think_believe_consider(skc6, skc7) -> relation(skc6, skc8) % 15.87/15.36 208: ifeq2(think_believe_consider(skc5, X), relation(skc6, skc8), think_believe_consider(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 210: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(event(X, Z), relation(skc6, skc8), event(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 211: ifeq2(event(skc5, X), relation(skc6, skc8), event(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 212: event(skc6, skc7) -> relation(skc6, skc8) % 15.87/15.36 213: eventuality(skc6, skc7) -> relation(skc6, skc8) % 15.87/15.36 214: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), event(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 216: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(smoke(X, Z), relation(skc6, skc8), smoke(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 217: ifeq2(smoke(skc5, X), relation(skc6, skc8), smoke(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 219: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(eventuality(X, Z), relation(skc6, skc8), eventuality(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 220: ifeq2(eventuality(skc5, X), relation(skc6, skc8), eventuality(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 222: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(abstraction(X, Z), relation(skc6, skc8), abstraction(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 223: ifeq2(abstraction(skc5, X), relation(skc6, skc8), abstraction(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 224: abstraction(skc6, skc6) -> relation(skc6, skc8) % 15.87/15.36 225: general(skc6, skc6) -> relation(skc6, skc8) % 15.87/15.36 226: nonhuman(skc6, skc6) -> relation(skc6, skc8) % 15.87/15.36 227: abstraction(skc6, skc8) -> relation(skc6, skc8) % 15.87/15.36 228: general(skc6, skc8) -> relation(skc6, skc8) % 15.87/15.36 229: nonhuman(skc6, skc8) -> relation(skc6, skc8) % 15.87/15.36 231: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(relation(X, Z), relation(skc6, skc8), relation(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 232: ifeq2(relation(skc5, X), relation(skc6, skc8), relation(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 233: relation(skc6, skc6) -> relation(skc6, skc8) % 15.87/15.36 234: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), relation(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 236: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(proposition(X, Z), relation(skc6, skc8), proposition(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 237: ifeq2(proposition(skc5, X), relation(skc6, skc8), proposition(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 238: proposition(skc6, skc6) -> relation(skc6, skc8) % 15.87/15.36 239: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), proposition(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 241: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(nonhuman(X, Z), relation(skc6, skc8), nonhuman(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 242: ifeq2(nonhuman(skc5, X), relation(skc6, skc8), nonhuman(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 244: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(forename(X, Z), relation(skc6, skc8), forename(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 245: ifeq2(forename(skc5, X), relation(skc6, skc8), forename(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 246: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), forename(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 248: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(general(X, Z), relation(skc6, skc8), general(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 249: ifeq2(general(skc5, X), relation(skc6, skc8), general(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 251: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(relname(X, Z), relation(skc6, skc8), relname(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 252: ifeq2(relname(skc5, X), relation(skc6, skc8), relname(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 253: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), relname(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 254: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), eventuality(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 255: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), relation(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 256: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), human_person(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 257: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), male(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 258: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(thing(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 259: ifeq2(accessible_world(skc5, skc5), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 260: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), proposition(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 261: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), event(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 262: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), think_believe_consider(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 263: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), nonexistent(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 264: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), present(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 265: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), abstraction(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 266: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), unisex(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 267: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), animate(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 268: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), vincent_forename(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 269: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), human(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 270: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), relation(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 271: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), relation(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 272: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), man(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 273: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), organism(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 274: ifeq2(singleton(skc5, X), relation(skc6, skc8), singleton(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 275: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), specific(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 276: ifeq2(nonexistent(skc5, X), relation(skc6, skc8), nonexistent(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 277: ifeq2(human_person(skc5, X), relation(skc6, skc8), human_person(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 278: ifeq2(present(skc5, X), relation(skc6, skc8), present(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 279: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), present(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 280: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), specific(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 281: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(thing(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 282: ifeq2(smoke(skc6, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 283: ifeq2(eventuality(skc6, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 284: ifeq2(accessible_world(skc6, skc5), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 285: ifeq2(relname(skc6, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 286: ifeq2(thing(X, Y), relation(skc6, skc8), singleton(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 287: ifeq2(eventuality(X, Y), relation(skc6, skc8), thing(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 288: ifeq2(eventuality(X, Y), relation(skc6, skc8), unisex(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 289: ifeq2(entity(X, Y), relation(skc6, skc8), existent(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 290: ifeq2(event(X, Y), relation(skc6, skc8), eventuality(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 291: ifeq2(eventuality(X, Y), relation(skc6, skc8), specific(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 292: ifeq2(smoke(X, Y), relation(skc6, skc8), event(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 293: ifeq2(entity(X, Y), relation(skc6, skc8), specific(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 294: ifeq2(organism(X, Y), relation(skc6, skc8), impartial(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 295: ifeq2(human_person(X, Y), relation(skc6, skc8), organism(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 296: ifeq2(organism(X, Y), relation(skc6, skc8), entity(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 297: ifeq2(man(X, Y), relation(skc6, skc8), human_person(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 298: ifeq2(entity(X, Y), relation(skc6, skc8), thing(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 299: ifeq2(eventuality(X, Y), relation(skc6, skc8), nonexistent(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 300: ifeq2(forename(X, Y), relation(skc6, skc8), relname(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 301: ifeq2(vincent_forename(X, Y), relation(skc6, skc8), forename(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 302: ifeq2(abstraction(X, Y), relation(skc6, skc8), unisex(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 303: ifeq2(relname(X, Y), relation(skc6, skc8), relation(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 304: ifeq2(abstraction(X, Y), relation(skc6, skc8), general(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 305: ifeq2(abstraction(X, Y), relation(skc6, skc8), thing(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 306: ifeq2(relation(X, Y), relation(skc6, skc8), abstraction(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 307: ifeq2(abstraction(X, Y), relation(skc6, skc8), nonhuman(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 308: ifeq2(human_person(X, Y), relation(skc6, skc8), human(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 309: ifeq2(man(X, Y), relation(skc6, skc8), male(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 310: ifeq2(proposition(X, Y), relation(skc6, skc8), relation(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 311: ifeq2(human_person(X, Y), relation(skc6, skc8), animate(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 312: ifeq2(organism(X, Y), relation(skc6, skc8), living(X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 313: ifeq2(thing(skc5, X), relation(skc6, skc8), thing(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 314: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), entity(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 315: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), animate(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 316: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), unisex(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 317: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), abstraction(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 318: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), eventuality(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 319: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), nonexistent(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 320: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), abstraction(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 321: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), nonhuman(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 322: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), general(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 323: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), forename(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 324: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), male(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 325: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), unisex(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 326: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), impartial(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 327: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), human(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 328: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), singleton(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 329: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), specific(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 330: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), organism(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 331: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), living(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 332: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(thing(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 333: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(thing(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 334: ifeq2(man(skc6, X), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 335: ifeq2(smoke(skc5, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 336: ifeq2(entity(skc5, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 337: ifeq2(abstraction(skc5, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 338: ifeq2(proposition(skc5, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 339: ifeq2(relname(skc5, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 340: ifeq2(abstraction(skc6, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 341: ifeq2(entity(skc6, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 343: ifeq2(theme(X, Y, Z), relation(skc6, skc8), ifeq2(accessible_world(X, W), relation(skc6, skc8), theme(W, Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 344: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), theme(X, skc7, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 345: theme(skc6, skc7, skc6) -> relation(skc6, skc8) % 15.87/15.36 346: ifeq2(theme(skc5, X, Y), relation(skc6, skc8), theme(skc6, X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 348: ifeq2(agent(X, Y, Z), relation(skc6, skc8), ifeq2(accessible_world(X, W), relation(skc6, skc8), agent(W, Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 349: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), agent(X, skc7, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 350: agent(skc6, skc7, skc9) -> relation(skc6, skc8) % 15.87/15.36 351: ifeq2(agent(skc5, X, Y), relation(skc6, skc8), agent(skc6, X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 353: ifeq2(of(X, Y, Z), relation(skc6, skc8), ifeq2(accessible_world(X, W), relation(skc6, skc8), of(W, Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 354: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), of(X, skc8, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 355: of(skc6, skc8, skc9) -> relation(skc6, skc8) % 15.87/15.36 356: ifeq2(of(skc5, X, Y), relation(skc6, skc8), of(skc6, X, Y), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 357: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), agent(X, skc7, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 358: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), of(X, skc8, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 359: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), theme(X, skc7, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 360: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), existent(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 361: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), entity(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 362: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), living(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 363: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), unisex(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 364: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), impartial(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 365: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), abstraction(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 366: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), unisex(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 367: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), singleton(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 368: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), specific(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 369: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), thing(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 370: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), relname(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 371: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), general(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 372: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), general(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 373: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), nonhuman(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 374: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), nonhuman(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 375: ifeq2(eventuality(skc6, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 376: ifeq2(eventuality(skc5, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 377: ifeq2(eventuality(skc5, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 378: ifeq2(abstraction(skc5, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 379: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), event(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 380: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), smoke(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 381: ifeq2(entity(skc5, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 382: ifeq2(eventuality(skc5, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 383: ifeq2(entity(skc5, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 384: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), present(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 385: ifeq2(present(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 386: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), human_person(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 387: ifeq2(event(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 388: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), existent(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 389: ifeq2(existent(skc5, X), relation(skc6, skc8), existent(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 390: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), singleton(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 391: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), singleton(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 392: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), singleton(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 393: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), thing(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 394: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), thing(X, skc7), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 395: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), singleton(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 396: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), thing(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 397: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), thing(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 398: ifeq2(smoke(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 399: ifeq2(man(skc5, X), relation(skc6, skc8), man(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 400: ifeq2(accessible_world(skc5, X), relation(skc6, skc8), man(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 401: ifeq2(vincent_forename(skc5, X), relation(skc6, skc8), vincent_forename(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 402: ifeq2(impartial(skc5, X), relation(skc6, skc8), impartial(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 403: ifeq2(organism(skc5, X), relation(skc6, skc8), organism(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 404: ifeq2(male(skc5, X), relation(skc6, skc8), male(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 405: ifeq2(human(skc5, X), relation(skc6, skc8), human(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 406: ifeq2(animate(skc5, X), relation(skc6, skc8), animate(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 407: ifeq2(living(skc5, X), relation(skc6, skc8), living(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 408: ifeq2(entity(skc5, X), relation(skc6, skc8), entity(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 409: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), thing(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 410: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), thing(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 411: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), nonhuman(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 412: ifeq2(specific(skc5, X), relation(skc6, skc8), specific(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 413: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), unisex(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 414: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), general(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 415: ifeq2(unisex(skc5, X), relation(skc6, skc8), unisex(skc6, X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 416: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), eventuality(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 417: ifeq2(eventuality(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 418: ifeq2(entity(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 419: ifeq2(entity(skc6, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 420: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), singleton(X, skc6), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 421: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), thing(X, skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 422: ifeq2(eventuality(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 423: ifeq2(man(skc6, X), relation(skc6, skc8), agent(skc6, skf1(X), X), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 424: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), agent(X, skf1(skc9), skc9), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 425: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), thing(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 426: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), unisex(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 427: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), nonexistent(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 428: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), specific(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 429: ifeq2(abstraction(skc6, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 430: ifeq2(specific(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 431: ifeq2(thing(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 432: ifeq2(agent(skc5, skf1(skc9), skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 433: ifeq2(unisex(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 434: ifeq2(abstraction(skc6, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 435: ifeq2(entity(skc6, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 436: ifeq2(nonexistent(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 437: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), singleton(X, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 438: ifeq2(accessible_world(skc6, X), relation(skc6, skc8), singleton(X, skf1(Y)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 439: ifeq2(singleton(skc5, skf1(X)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 440: ifeq(tuple(unisex(X, Y), male(X, Y)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 441: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 442: ifeq(tuple(human(X, Y), nonhuman(X, Y)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 443: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 444: ifeq(tuple(relation(skc6, skc8), general(skc6, skc9)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 445: ifeq(tuple(relation(skc6, skc8), male(skc6, skc7)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 446: ifeq(tuple(relation(skc6, skc8), male(skc5, skc7)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 447: ifeq(tuple(relation(skc6, skc8), general(skc5, skc7)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 448: ifeq(tuple(relation(skc6, skc8), nonhuman(skc5, skc9)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 449: ifeq(tuple(relation(skc6, skc8), existent(skc5, skc7)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 450: ifeq(tuple(relation(skc6, skc8), general(skc6, skc7)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 451: ifeq(tuple(unisex(skc6, skc9), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 452: ifeq(tuple(relation(skc6, skc8), nonhuman(skc6, skc9)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 453: ifeq(tuple(unisex(skc5, skc9), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 454: ifeq(tuple(relation(skc6, skc8), existent(skc6, skc7)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 455: ifeq(tuple(relation(skc6, skc8), male(skc6, skc6)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 456: ifeq(tuple(specific(skc5, skc6), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 457: ifeq(tuple(nonexistent(skc5, skc9), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 458: ifeq(tuple(human(skc5, skc6), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 459: ifeq(tuple(human(skc5, skc8), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 460: ifeq(tuple(human(skc6, skc6), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 461: ifeq(tuple(relation(skc6, skc8), male(skc5, skc6)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 462: ifeq(tuple(relation(skc6, skc8), male(skc5, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 463: ifeq(tuple(relation(skc6, skc8), general(skc5, skc9)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 464: ifeq(tuple(specific(skc5, skc8), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 465: ifeq(tuple(specific(skc6, skc6), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 466: ifeq(tuple(specific(skc6, skc8), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 467: ifeq(tuple(nonexistent(skc6, skc9), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 468: ifeq(tuple(human(skc6, skc8), relation(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 469: ifeq(tuple(relation(skc6, skc8), male(skc6, skc8)), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 470: ifeq(tuple(relation(skc6, skc8), male(skc6, skf1(X))), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 471: ifeq(tuple(relation(skc6, skc8), general(skc6, skf1(X))), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 472: ifeq(tuple(relation(skc6, skc8), existent(skc6, skf1(X))), tuple(relation(skc6, skc8), relation(skc6, skc8)), a, b) -> b % 15.87/15.36 473: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(proposition(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 474: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(forename(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 475: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(vincent_forename(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 476: ifeq2(think_believe_consider(X, skc7), relation(skc6, skc8), ifeq2(accessible_world(X, skc5), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 477: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(event(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 478: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(man(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 479: ifeq2(present(X, skc7), relation(skc6, skc8), ifeq2(accessible_world(X, skc5), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 480: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(male(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 481: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(singleton(X, Z), relation(skc6, skc8), singleton(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 482: ifeq2(present(X, Y), relation(skc6, skc8), ifeq2(accessible_world(X, Z), relation(skc6, skc8), present(Z, Y), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 483: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(nonexistent(X, Z), relation(skc6, skc8), nonexistent(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 484: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(relation(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 485: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(human_person(X, Z), relation(skc6, skc8), human_person(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 486: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(eventuality(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 487: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(relname(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 488: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(human_person(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 489: ifeq2(of(X, skc8, skc9), relation(skc6, skc8), ifeq2(accessible_world(X, skc5), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 490: ifeq2(theme(X, skc7, skc6), relation(skc6, skc8), ifeq2(accessible_world(X, skc5), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 491: ifeq2(agent(X, skc7, skc9), relation(skc6, skc8), ifeq2(accessible_world(X, skc5), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 492: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(unisex(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 493: ifeq2(think_believe_consider(X, skc7), relation(skc6, skc8), ifeq2(accessible_world(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 494: ifeq2(present(X, skc7), relation(skc6, skc8), ifeq2(accessible_world(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 495: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(vincent_forename(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 496: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(proposition(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 497: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(thing(X, Z), relation(skc6, skc8), thing(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 498: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(specific(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 499: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(animate(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 500: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(specific(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 501: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(relation(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 502: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(human(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 503: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(relation(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 504: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(nonexistent(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 505: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(abstraction(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 506: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(man(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 507: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(organism(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 508: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(event(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 509: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(impartial(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 510: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(abstraction(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 511: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(eventuality(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 512: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(organism(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 513: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(specific(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 514: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(abstraction(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 515: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(living(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 516: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(singleton(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 517: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(male(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 518: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(entity(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 519: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(unisex(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 520: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(animate(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 521: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(nonexistent(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 522: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(general(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 523: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(human(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 524: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(forename(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 525: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(nonhuman(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 526: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(unisex(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 527: ifeq2(theme(X, skc7, skc6), relation(skc6, skc8), ifeq2(accessible_world(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 528: ifeq2(of(X, skc8, skc9), relation(skc6, skc8), ifeq2(accessible_world(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 529: ifeq2(agent(X, skc7, skc9), relation(skc6, skc8), ifeq2(accessible_world(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 530: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(vincent_forename(X, Z), relation(skc6, skc8), vincent_forename(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 531: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(man(X, Z), relation(skc6, skc8), man(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 532: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(general(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 533: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(existent(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 534: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(singleton(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 535: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(unisex(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 536: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(thing(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 537: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(nonhuman(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 538: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(male(X, Z), relation(skc6, skc8), male(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 539: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(human(X, Z), relation(skc6, skc8), human(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 540: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(living(X, Z), relation(skc6, skc8), living(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 541: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(animate(X, Z), relation(skc6, skc8), animate(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 542: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(organism(X, Z), relation(skc6, skc8), organism(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 543: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(impartial(X, Z), relation(skc6, skc8), impartial(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 544: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(unisex(X, Z), relation(skc6, skc8), unisex(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 545: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(existent(X, Z), relation(skc6, skc8), existent(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 546: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(unisex(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 547: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(specific(X, Z), relation(skc6, skc8), specific(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 548: ifeq2(accessible_world(X, Y), relation(skc6, skc8), ifeq2(entity(X, Z), relation(skc6, skc8), entity(Y, Z), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 549: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(impartial(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 550: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(abstraction(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 551: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(relname(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 552: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(entity(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 553: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(nonhuman(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 554: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(general(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 555: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(living(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 556: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(specific(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 557: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(smoke(X, skf1(Y)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 558: ifeq2(present(X, skf1(Y)), relation(skc6, skc8), ifeq2(accessible_world(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 559: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(event(X, skf1(Y)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 560: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(thing(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 561: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(singleton(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 562: ifeq2(accessible_world(X, skc5), relation(skc6, skc8), ifeq2(singleton(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 563: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(singleton(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 564: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(singleton(X, skc7), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 565: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(thing(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 566: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(existent(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 567: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(human_person(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 568: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(unisex(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 569: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(general(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 570: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(nonhuman(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 571: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(eventuality(X, skf1(Y)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 572: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(thing(X, skc9), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 573: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(singleton(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 574: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(specific(X, skf1(Y)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 575: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(thing(X, skf1(Y)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 576: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(nonexistent(X, skf1(Y)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 577: ifeq2(agent(X, skf1(skc9), skc9), relation(skc6, skc8), ifeq2(accessible_world(X, skc6), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 578: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(unisex(X, skf1(Y)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 579: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(singleton(X, skc8), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 580: ifeq2(accessible_world(X, skc6), relation(skc6, skc8), ifeq2(singleton(X, skf1(Y)), relation(skc6, skc8), relation(skc6, skc8), relation(skc6, skc8)), relation(skc6, skc8)) -> relation(skc6, skc8) % 15.87/15.36 582: ifeq3(of(X, Y, Z), relation(skc6, skc8), ifeq3(of(X, W, Z), relation(skc6, skc8), ifeq3(forename(X, Y), relation(skc6, skc8), ifeq3(forename(X, W), relation(skc6, skc8), ifeq3(entity(X, Z), relation(skc6, skc8), Y, W), W), W), W), W) -> W % 15.87/15.36 583: ifeq3(of(skc5, X, skc9), relation(skc6, skc8), ifeq3(forename(skc5, X), relation(skc6, skc8), skc8, X), X) -> X % 15.87/15.36 584: ifeq3(of(skc5, X, skc9), relation(skc6, skc8), ifeq3(forename(skc5, X), relation(skc6, skc8), X, skc8), skc8) -> skc8 % 15.87/15.36 585: ifeq3(of(skc6, X, skc9), relation(skc6, skc8), ifeq3(forename(skc6, X), relation(skc6, skc8), skc8, X), X) -> X % 15.87/15.36 586: ifeq3(of(skc6, X, skc9), relation(skc6, skc8), ifeq3(forename(skc6, X), relation(skc6, skc8), X, skc8), skc8) -> skc8 % 15.87/15.36 587: ifeq3(of(skc5, skc8, X), relation(skc6, skc8), ifeq3(of(skc5, Y, X), relation(skc6, skc8), ifeq3(forename(skc5, Y), relation(skc6, skc8), ifeq3(entity(skc5, X), relation(skc6, skc8), skc8, Y), Y), Y), Y) -> Y % 15.87/15.36 588: ifeq3(of(skc5, skc8, X), relation(skc6, skc8), ifeq3(of(skc5, skc8, X), relation(skc6, skc8), ifeq3(entity(skc5, X), relation(skc6, skc8), skc8, skc8), skc8), skc8) -> skc8 % 15.87/15.36 589: ifeq3(of(skc5, X, Y), relation(skc6, skc8), ifeq3(of(skc5, skc8, Y), relation(skc6, skc8), ifeq3(forename(skc5, X), relation(skc6, skc8), ifeq3(entity(skc5, Y), relation(skc6, skc8), X, skc8), skc8), skc8), skc8) -> skc8 % 15.87/15.36 590: ifeq3(of(skc6, skc8, X), relation(skc6, skc8), ifeq3(of(skc6, Y, X), relation(skc6, skc8), ifeq3(forename(skc6, Y), relation(skc6, skc8), ifeq3(entity(skc6, X), relation(skc6, skc8), skc8, Y), Y), Y), Y) -> Y % 15.87/15.36 591: ifeq3(of(skc6, skc8, X), relation(skc6, skc8), ifeq3(of(skc6, skc8, X), relation(skc6, skc8), ifeq3(entity(skc6, X), relation(skc6, skc8), skc8, skc8), skc8), skc8) -> skc8 % 15.87/15.36 592: ifeq3(of(skc5, X, skc9), relation(skc6, skc8), ifeq3(of(skc5, Y, skc9), relation(skc6, skc8), ifeq3(forename(skc5, X), relation(skc6, skc8), ifeq3(forename(skc5, Y), relation(skc6, skc8), X, Y), Y), Y), Y) -> Y % 15.87/15.36 593: ifeq3(of(skc6, X, Y), relation(skc6, skc8), ifeq3(of(skc6, skc8, Y), relation(skc6, skc8), ifeq3(forename(skc6, X), relation(skc6, skc8), ifeq3(entity(skc6, Y), relation(skc6, skc8), X, skc8), skc8), skc8), skc8) -> skc8 % 15.87/15.36 594: ifeq3(of(skc6, X, skc9), relation(skc6, skc8), ifeq3(of(skc6, Y, skc9), relation(skc6, skc8), ifeq3(forename(skc6, X), relation(skc6, skc8), ifeq3(forename(skc6, Y), relation(skc6, skc8), X, Y), Y), Y), Y) -> Y % 15.87/15.36 596: ifeq3(theme(X, Y, Z), relation(skc6, skc8), ifeq3(theme(X, W, V), relation(skc6, skc8), ifeq3(agent(X, Y, U), relation(skc6, skc8), ifeq3(agent(X, W, U), relation(skc6, skc8), ifeq3(think_believe_consider(X, Y), relation(skc6, skc8), ifeq3(think_believe_consider(X, W), relation(skc6, skc8), ifeq3(proposition(X, Z), relation(skc6, skc8), ifeq3(proposition(X, V), relation(skc6, skc8), V, Z), Z), Z), Z), Z), Z), Z), Z) -> Z % 15.87/15.36 597: ifeq3(theme(skc5, X, Y), relation(skc6, skc8), ifeq3(agent(skc5, X, Z), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), skc6, Y), Y), Y), Y), Y) -> Y % 15.87/15.36 598: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), skc6, X), X) -> X % 15.87/15.36 599: ifeq3(agent(skc5, skc7, X), relation(skc6, skc8), ifeq3(agent(skc5, skc7, X), relation(skc6, skc8), skc6, skc6), skc6) -> skc6 % 15.87/15.36 600: ifeq3(theme(skc5, X, Y), relation(skc6, skc8), ifeq3(agent(skc5, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), skc6, Y), Y), Y), Y) -> Y % 15.87/15.36 601: ifeq3(theme(skc5, X, skc6), relation(skc6, skc8), ifeq3(agent(skc5, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), skc6, skc6), skc6), skc6) -> skc6 % 15.87/15.36 602: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Y), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), skc6, X), X), X), X) -> X % 15.87/15.36 603: ifeq3(theme(skc5, X, skc6), relation(skc6, skc8), ifeq3(agent(skc5, X, Y), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Y), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 604: ifeq3(theme(skc5, X, Y), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc5, X, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 605: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), X, skc6), skc6) -> skc6 % 15.87/15.36 606: ifeq3(theme(skc5, X, Y), relation(skc6, skc8), ifeq3(agent(skc5, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 607: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Y), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), X, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 608: ifeq3(theme(skc5, X, skc6), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc5, X, Y), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 609: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(agent(skc6, X, Z), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), skc6, Y), Y), Y), Y), Y) -> Y % 15.87/15.36 610: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), skc6, X), X) -> X % 15.87/15.36 611: ifeq3(agent(skc6, skc7, X), relation(skc6, skc8), ifeq3(agent(skc6, skc7, X), relation(skc6, skc8), skc6, skc6), skc6) -> skc6 % 15.87/15.36 612: ifeq3(theme(skc6, skf1(skc9), X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), skc6, X), X), X) -> X % 15.87/15.36 613: ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), skc6, skc6), skc6) -> skc6 % 15.87/15.36 614: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), skc6, Y), Y), Y), Y) -> Y % 15.87/15.36 615: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), skc6, skc6), skc6), skc6) -> skc6 % 15.87/15.36 616: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), skc6, X), X), X), X) -> X % 15.87/15.36 617: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(agent(skc6, X, Y), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Y), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 618: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc6, X, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 619: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), X, skc6), skc6) -> skc6 % 15.87/15.36 620: ifeq3(theme(skc6, skf1(skc9), X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), X, skc6), skc6), skc6) -> skc6 % 15.87/15.36 621: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 622: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), X, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 623: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc6, X, Y), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 624: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(theme(skc5, Y, Z), relation(skc6, skc8), ifeq3(agent(skc5, Y, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, Y), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Z), relation(skc6, skc8), Z, X), X), X), X), X), X) -> X % 15.87/15.36 625: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(theme(skc5, skc7, Y), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), Y, X), X), X), X) -> X % 15.87/15.36 626: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(theme(skc5, Y, skc6), relation(skc6, skc8), ifeq3(agent(skc5, Y, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, Y), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), skc6, X), X), X), X), X) -> X % 15.87/15.36 627: ifeq3(theme(skc5, X, Y), relation(skc6, skc8), ifeq3(theme(skc5, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc5, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), ifeq3(proposition(skc5, Z), relation(skc6, skc8), Z, Y), Y), Y), Y), Y), Y) -> Y % 15.87/15.36 628: ifeq3(theme(skc5, X, skc6), relation(skc6, skc8), ifeq3(theme(skc5, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc5, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 629: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(theme(skc6, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, Z), relation(skc6, skc8), Z, Y), Y), Y), Y), Y), Y) -> Y % 15.87/15.36 630: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(theme(skc6, skc7, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, X), X), X), X) -> X % 15.87/15.36 631: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(theme(skc6, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 632: ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), X, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 633: ifeq3(theme(skc6, skf1(skc9), X), relation(skc6, skc8), ifeq3(theme(skc6, skc7, Y), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, X), X), X), X), X) -> X % 15.87/15.36 634: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(theme(skc6, Y, Z), relation(skc6, skc8), ifeq3(agent(skc6, Y, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Z), relation(skc6, skc8), Z, X), X), X), X), X), X) -> X % 15.87/15.36 635: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(theme(skc6, Y, skc6), relation(skc6, skc8), ifeq3(agent(skc6, Y, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), skc6, X), X), X), X), X) -> X % 15.87/15.36 636: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), skc6, X), X), X), X) -> X % 15.87/15.36 637: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), Y), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, X), X), X), X), X) -> X % 15.87/15.36 638: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(theme(skc5, Y, Z), relation(skc6, skc8), ifeq3(agent(skc5, skc7, W), relation(skc6, skc8), ifeq3(agent(skc5, Y, W), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, Y), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Z), relation(skc6, skc8), Z, X), X), X), X), X), X), X) -> X % 15.87/15.36 639: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(theme(skc5, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Z), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), Y, X), X), X), X), X), X) -> X % 15.87/15.36 640: ifeq3(theme(skc5, skc7, X), relation(skc6, skc8), ifeq3(theme(skc5, Y, skc6), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc5, Y, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, Y), relation(skc6, skc8), ifeq3(proposition(skc5, X), relation(skc6, skc8), skc6, X), X), X), X), X), X) -> X % 15.87/15.36 641: ifeq3(theme(skc5, X, Y), relation(skc6, skc8), ifeq3(theme(skc5, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc5, X, W), relation(skc6, skc8), ifeq3(agent(skc5, skc7, W), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), ifeq3(proposition(skc5, Z), relation(skc6, skc8), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 15.87/15.36 642: ifeq3(theme(skc5, X, skc6), relation(skc6, skc8), ifeq3(theme(skc5, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc5, X, Z), relation(skc6, skc8), ifeq3(agent(skc5, skc7, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 643: ifeq3(theme(skc5, X, Y), relation(skc6, skc8), ifeq3(theme(skc5, Z, skc6), relation(skc6, skc8), ifeq3(agent(skc5, X, W), relation(skc6, skc8), ifeq3(agent(skc5, Z, W), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, Z), relation(skc6, skc8), ifeq3(proposition(skc5, Y), relation(skc6, skc8), skc6, Y), Y), Y), Y), Y), Y), Y) -> Y % 15.87/15.36 644: ifeq3(theme(skc5, X, skc6), relation(skc6, skc8), ifeq3(theme(skc5, Y, skc6), relation(skc6, skc8), ifeq3(agent(skc5, X, Z), relation(skc6, skc8), ifeq3(agent(skc5, Y, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, Y), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 645: ifeq3(theme(skc5, X, skc6), relation(skc6, skc8), ifeq3(theme(skc5, Y, Z), relation(skc6, skc8), ifeq3(agent(skc5, X, W), relation(skc6, skc8), ifeq3(agent(skc5, Y, W), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc5, Y), relation(skc6, skc8), ifeq3(proposition(skc5, Z), relation(skc6, skc8), Z, skc6), skc6), skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 646: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(theme(skc6, Z, skc6), relation(skc6, skc8), ifeq3(agent(skc6, X, W), relation(skc6, skc8), ifeq3(agent(skc6, Z, W), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Z), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), skc6, Y), Y), Y), Y), Y), Y), Y) -> Y % 15.87/15.36 647: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(theme(skc6, Y, skc6), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc6, Y, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), skc6, X), X), X), X), X), X) -> X % 15.87/15.36 648: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(theme(skc6, Y, skc6), relation(skc6, skc8), ifeq3(agent(skc6, X, Z), relation(skc6, skc8), ifeq3(agent(skc6, Y, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Y), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 649: ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 650: ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 651: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), skc6, skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 652: ifeq3(theme(skc6, skf1(skc9), X), relation(skc6, skc8), ifeq3(theme(skc6, Y, skc6), relation(skc6, skc8), ifeq3(agent(skc6, Y, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), skc6, X), X), X), X), X), X) -> X % 15.87/15.36 653: ifeq3(theme(skc6, skf1(skc9), X), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), skc6, X), X), X), X), X) -> X % 15.87/15.36 654: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), skc6, Y), Y), Y), Y), Y), Y) -> Y % 15.87/15.36 655: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(theme(skc6, Y, Z), relation(skc6, skc8), ifeq3(agent(skc6, skc7, W), relation(skc6, skc8), ifeq3(agent(skc6, Y, W), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Z), relation(skc6, skc8), Z, X), X), X), X), X), X), X) -> X % 15.87/15.36 656: ifeq3(theme(skc6, skc7, X), relation(skc6, skc8), ifeq3(theme(skc6, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Z), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, X), X), X), X), X), X) -> X % 15.87/15.36 657: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(theme(skc6, skc7, Z), relation(skc6, skc8), ifeq3(agent(skc6, X, W), relation(skc6, skc8), ifeq3(agent(skc6, skc7, W), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, Z), relation(skc6, skc8), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 15.87/15.36 658: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(theme(skc6, skc7, Y), relation(skc6, skc8), ifeq3(agent(skc6, X, Z), relation(skc6, skc8), ifeq3(agent(skc6, skc7, Z), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 659: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(theme(skc6, Y, Z), relation(skc6, skc8), ifeq3(agent(skc6, X, W), relation(skc6, skc8), ifeq3(agent(skc6, Y, W), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, Z), relation(skc6, skc8), Z, skc6), skc6), skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 660: ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 661: ifeq3(theme(skc6, skf1(skc9), skc6), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), X, skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 662: ifeq3(theme(skc6, X, skc6), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), Y), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, skc6), skc6), skc6), skc6), skc6), skc6) -> skc6 % 15.87/15.36 663: ifeq3(theme(skc6, skf1(skc9), X), relation(skc6, skc8), ifeq3(theme(skc6, Y, Z), relation(skc6, skc8), ifeq3(agent(skc6, Y, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Z), relation(skc6, skc8), Z, X), X), X), X), X), X), X) -> X % 15.87/15.36 664: ifeq3(theme(skc6, skf1(skc9), X), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), Y), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, X), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), Y, X), X), X), X), X), X) -> X % 15.87/15.36 665: ifeq3(theme(skc6, X, Y), relation(skc6, skc8), ifeq3(theme(skc6, skf1(skc9), Z), relation(skc6, skc8), ifeq3(agent(skc6, X, skc9), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, X), relation(skc6, skc8), ifeq3(think_believe_consider(skc6, skf1(skc9)), relation(skc6, skc8), ifeq3(proposition(skc6, Y), relation(skc6, skc8), ifeq3(proposition(skc6, Z), relation(skc6, skc8), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 15.87/15.36 %------------------------------------------------------------------------------