%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP226-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n009.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:58 AM UTC 2025 % Result : Satisfiable 28.47s 27.40s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : NLP226-10 : TPTP v9.0.0. Released v7.5.0. % 0.00/0.10 % Command : run_Leo-III %s %d THM % 0.09/0.30 % Computer : n009.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Mon Jul 14 14:21:19 EDT 2025 % 0.09/0.30 % CPUTime : % 28.47/27.40 % SZS status Satisfiable % 28.47/27.40 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 28.47/27.40 1: actual_world(skc8) -> true % 28.47/27.40 2: man(skc8, skc15) -> true % 28.47/27.40 3: forename(skc8, skc14) -> true % 28.47/27.40 4: vincent_forename(skc8, skc14) -> true % 28.47/27.40 5: event(skc8, skc13) -> true % 28.47/27.40 6: present(skc8, skc13) -> true % 28.47/27.40 7: think_believe_consider(skc8, skc13) -> true % 28.47/27.40 8: jules_forename(skc8, skc11) -> true % 28.47/27.40 9: forename(skc8, skc11) -> true % 28.47/27.40 10: man(skc8, skc10) -> true % 28.47/27.40 11: state(skc8, skc9) -> true % 28.47/27.40 12: accessible_world(skc8, skc12) -> true % 28.47/27.40 13: proposition(skc8, skc12) -> true % 28.47/27.40 14: of(skc8, skc14, skc15) -> true % 28.47/27.40 15: agent(skc8, skc13, skc15) -> true % 28.47/27.40 16: theme(skc8, skc13, skc12) -> true % 28.47/27.40 17: of(skc8, skc11, skc10) -> true % 28.47/27.40 18: ifeq3(X, X, Y, Z) -> Y % 28.47/27.40 19: ifeq(X, X, Y, Z) -> Y % 28.47/27.40 20: ifeq2(X, X, Y, Z) -> Y % 28.47/27.40 21: be(skc8, skc9, skc10, skc10) -> true % 28.47/27.40 22: ifeq3(be(X, Y, Z, W), true, Z, W) -> W % 28.47/27.40 23: ifeq2(abstraction(X, Y), true, thing(X, Y), true) -> true % 28.47/27.40 24: ifeq2(state(X, Y), true, event(X, Y), true) -> true % 28.47/27.40 25: event(skc8, skc9) -> true % 28.47/27.40 26: ifeq2(state(skc8, skc13), true, true, true) -> true % 28.47/27.40 27: ifeq2(eventuality(X, Y), true, unisex(X, Y), true) -> true % 28.47/27.40 28: ifeq2(abstraction(X, Y), true, unisex(X, Y), true) -> true % 28.47/27.40 29: ifeq2(abstraction(X, Y), true, general(X, Y), true) -> true % 28.47/27.40 30: ifeq2(abstraction(X, Y), true, nonhuman(X, Y), true) -> true % 28.47/27.40 31: ifeq2(jules_forename(X, Y), true, forename(X, Y), true) -> true % 28.47/27.40 32: ifeq2(jules_forename(skc8, skc14), true, true, true) -> true % 28.47/27.40 33: ifeq2(proposition(X, Y), true, relation(X, Y), true) -> true % 28.47/27.40 34: relation(skc8, skc12) -> true % 28.47/27.40 35: ifeq2(smoke(X, Y), true, event(X, Y), true) -> true % 28.47/27.40 36: ifeq2(smoke(skc8, skc13), true, true, true) -> true % 28.47/27.40 37: ifeq2(smoke(skc8, skc9), true, true, true) -> true % 28.47/27.40 38: ifeq2(vincent_forename(X, Y), true, forename(X, Y), true) -> true % 28.47/27.40 39: ifeq2(vincent_forename(skc8, skc11), true, true, true) -> true % 28.47/27.40 40: ifeq2(organism(X, Y), true, entity(X, Y), true) -> true % 28.47/27.40 41: ifeq2(man(X, Y), true, human_person(X, Y), true) -> true % 28.47/27.40 42: human_person(skc8, skc10) -> true % 28.47/27.40 43: human_person(skc8, skc15) -> true % 28.47/27.40 44: ifeq2(human_person(X, Y), true, organism(X, Y), true) -> true % 28.47/27.40 45: true -> organism(skc8, skc10) % 28.47/27.40 46: organism(skc8, skc10) -> organism(skc8, skc15) % 28.47/27.40 47: entity(skc8, skc10) -> organism(skc8, skc15) % 28.47/27.40 49: ifeq2(event(X, Y), organism(skc8, skc15), eventuality(X, Y), organism(skc8, skc15)) -> organism(skc8, skc15) % 28.47/27.40 50: eventuality(skc8, skc13) -> organism(skc8, skc15) % 28.47/27.40 51: unisex(skc8, skc13) -> organism(skc8, skc15) % 28.47/27.40 52: eventuality(skc8, skc9) -> organism(skc8, skc15) % 28.47/27.40 53: unisex(skc8, skc9) -> organism(skc8, skc15) % 28.47/27.40 55: ifeq2(entity(X, Y), organism(skc8, skc15), thing(X, Y), organism(skc8, skc15)) -> organism(skc8, skc15) % 28.47/27.40 56: thing(skc8, skc10) -> organism(skc8, skc15) % 28.47/27.40 58: ifeq2(entity(X, Y), organism(skc8, skc15), existent(X, Y), organism(skc8, skc15)) -> organism(skc8, skc15) % 28.47/27.40 59: existent(skc8, skc10) -> organism(skc8, skc15) % 28.47/27.40 61: ifeq2(entity(X, Y), organism(skc8, skc15), specific(X, Y), organism(skc8, skc15)) -> organism(skc8, skc15) % 28.47/27.40 62: specific(skc8, skc10) -> organism(skc8, skc15) % 28.47/27.40 64: ifeq2(organism(X, Y), organism(skc8, skc15), impartial(X, Y), organism(skc8, skc15)) -> organism(skc8, skc15) % 28.47/27.40 65: impartial(skc8, skc15) -> organism(skc8, skc15) % 28.47/27.40 66: impartial(skc8, skc10) -> organism(skc8, skc15) % 28.47/27.40 68: ifeq2(human_person(X, Y), organism(skc8, skc15), animate(X, Y), organism(skc8, skc15)) -> organism(skc8, skc15) % 28.47/27.40 69: animate(skc8, skc10) -> organism(skc8, skc15) % 28.47/27.40 70: organism(skc8, skc15) -> animate(skc8, skc15) % 28.47/27.40 71: entity(skc8, skc15) -> animate(skc8, skc15) % 28.47/27.40 72: specific(skc8, skc15) -> animate(skc8, skc15) % 28.47/27.40 73: existent(skc8, skc15) -> animate(skc8, skc15) % 28.47/27.40 74: thing(skc8, skc15) -> animate(skc8, skc15) % 28.47/27.40 76: ifeq2(organism(X, Y), animate(skc8, skc15), living(X, Y), animate(skc8, skc15)) -> animate(skc8, skc15) % 28.47/27.40 77: living(skc8, skc10) -> animate(skc8, skc15) % 28.47/27.40 78: living(skc8, skc15) -> animate(skc8, skc15) % 28.47/27.40 80: ifeq2(human_person(X, Y), animate(skc8, skc15), human(X, Y), animate(skc8, skc15)) -> animate(skc8, skc15) % 28.47/27.40 81: human(skc8, skc10) -> animate(skc8, skc15) % 28.47/27.40 82: human(skc8, skc15) -> animate(skc8, skc15) % 28.47/27.40 84: ifeq2(man(X, Y), animate(skc8, skc15), male(X, Y), animate(skc8, skc15)) -> animate(skc8, skc15) % 28.47/27.40 85: male(skc8, skc10) -> animate(skc8, skc15) % 28.47/27.40 86: male(skc8, skc15) -> animate(skc8, skc15) % 28.47/27.40 88: ifeq2(relname(X, Y), animate(skc8, skc15), relation(X, Y), animate(skc8, skc15)) -> animate(skc8, skc15) % 28.47/27.40 90: ifeq2(forename(X, Y), animate(skc8, skc15), relname(X, Y), animate(skc8, skc15)) -> animate(skc8, skc15) % 28.47/27.40 91: relname(skc8, skc11) -> animate(skc8, skc15) % 28.47/27.40 92: animate(skc8, skc15) -> relname(skc8, skc14) % 28.47/27.40 93: relation(skc8, skc11) -> relname(skc8, skc14) % 28.47/27.40 95: ifeq2(relation(X, Y), relname(skc8, skc14), abstraction(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 96: abstraction(skc8, skc12) -> relname(skc8, skc14) % 28.47/27.40 97: nonhuman(skc8, skc12) -> relname(skc8, skc14) % 28.47/27.40 98: general(skc8, skc12) -> relname(skc8, skc14) % 28.47/27.40 99: unisex(skc8, skc12) -> relname(skc8, skc14) % 28.47/27.40 100: thing(skc8, skc12) -> relname(skc8, skc14) % 28.47/27.40 101: abstraction(skc8, skc11) -> relname(skc8, skc14) % 28.47/27.40 102: nonhuman(skc8, skc11) -> relname(skc8, skc14) % 28.47/27.40 103: general(skc8, skc11) -> relname(skc8, skc14) % 28.47/27.40 104: unisex(skc8, skc11) -> relname(skc8, skc14) % 28.47/27.40 105: thing(skc8, skc11) -> relname(skc8, skc14) % 28.47/27.40 107: ifeq2(state(X, Y), relname(skc8, skc14), eventuality(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 109: ifeq2(eventuality(X, Y), relname(skc8, skc14), thing(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 110: thing(skc8, skc13) -> relname(skc8, skc14) % 28.47/27.40 111: thing(skc8, skc9) -> relname(skc8, skc14) % 28.47/27.40 113: ifeq2(eventuality(X, Y), relname(skc8, skc14), specific(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 114: specific(skc8, skc13) -> relname(skc8, skc14) % 28.47/27.40 115: specific(skc8, skc9) -> relname(skc8, skc14) % 28.47/27.40 117: ifeq2(thing(X, Y), relname(skc8, skc14), singleton(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 118: singleton(skc8, skc13) -> relname(skc8, skc14) % 28.47/27.40 119: singleton(skc8, skc12) -> relname(skc8, skc14) % 28.47/27.40 120: singleton(skc8, skc9) -> relname(skc8, skc14) % 28.47/27.40 121: singleton(skc8, skc10) -> relname(skc8, skc14) % 28.47/27.40 122: singleton(skc8, skc15) -> relname(skc8, skc14) % 28.47/27.40 123: singleton(skc8, skc11) -> relname(skc8, skc14) % 28.47/27.40 125: ifeq2(eventuality(X, Y), relname(skc8, skc14), nonexistent(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 126: nonexistent(skc8, skc13) -> relname(skc8, skc14) % 28.47/27.40 127: nonexistent(skc8, skc9) -> relname(skc8, skc14) % 28.47/27.40 129: ifeq2(man(skc12, X), relname(skc8, skc14), smoke(skc12, skf1(Y)), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 131: ifeq2(man(skc12, X), relname(skc8, skc14), present(skc12, skf1(Y)), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 133: ifeq2(man(skc12, X), relname(skc8, skc14), event(skc12, skf1(Y)), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 135: ifeq2(man(skc12, X), relname(skc8, skc14), agent(skc12, skf1(X), X), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 136: ifeq3(be(X, Y, Z, W), relname(skc8, skc14), Z, W) -> W % 28.47/27.40 138: ifeq(tuple(unisex(X, Y), male(X, Y)), tuple(relname(skc8, skc14), relname(skc8, skc14)), a, b) -> b % 28.47/27.40 140: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(relname(skc8, skc14), relname(skc8, skc14)), a, b) -> b % 28.47/27.40 142: ifeq(tuple(human(X, Y), nonhuman(X, Y)), tuple(relname(skc8, skc14), relname(skc8, skc14)), a, b) -> b % 28.47/27.40 144: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(relname(skc8, skc14), relname(skc8, skc14)), a, b) -> b % 28.47/27.40 145: ifeq2(organism(X, Y), relname(skc8, skc14), living(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 146: ifeq2(man(X, Y), relname(skc8, skc14), male(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 147: ifeq2(forename(X, Y), relname(skc8, skc14), relname(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 148: ifeq2(human_person(X, Y), relname(skc8, skc14), human(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 149: ifeq2(relname(X, Y), relname(skc8, skc14), relation(X, Y), relname(skc8, skc14)) -> relname(skc8, skc14) % 28.47/27.40 150: relname(skc8, skc14) -> relation(skc8, skc14) % 28.47/27.40 151: ifeq3(be(X, Y, Z, W), relation(skc8, skc14), Z, W) -> W % 28.47/27.40 152: ifeq2(forename(X, Y), relation(skc8, skc14), relname(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 153: ifeq2(relname(X, Y), relation(skc8, skc14), relation(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 155: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(organism(X, Z), relation(skc8, skc14), organism(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 156: ifeq2(organism(skc8, X), relation(skc8, skc14), organism(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 157: organism(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 158: organism(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 159: living(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 160: impartial(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 161: entity(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 162: living(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 163: impartial(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 164: entity(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 165: specific(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 166: existent(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 167: thing(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 168: specific(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 169: thing(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 170: existent(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 171: singleton(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 172: singleton(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 174: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(event(X, Z), relation(skc8, skc14), event(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 175: ifeq2(event(skc8, X), relation(skc8, skc14), event(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 176: event(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 177: event(skc12, skc9) -> relation(skc8, skc14) % 28.47/27.40 178: eventuality(skc12, skc9) -> relation(skc8, skc14) % 28.47/27.40 179: eventuality(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 180: nonexistent(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 181: specific(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 182: thing(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 183: unisex(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 184: thing(skc12, skc9) -> relation(skc8, skc14) % 28.47/27.40 185: nonexistent(skc12, skc9) -> relation(skc8, skc14) % 28.47/27.40 186: specific(skc12, skc9) -> relation(skc8, skc14) % 28.47/27.40 187: unisex(skc12, skc9) -> relation(skc8, skc14) % 28.47/27.40 188: singleton(skc12, skc9) -> relation(skc8, skc14) % 28.47/27.40 189: singleton(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 190: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), event(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 192: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(entity(X, Z), relation(skc8, skc14), entity(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 193: ifeq2(entity(skc8, X), relation(skc8, skc14), entity(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 195: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(man(X, Z), relation(skc8, skc14), man(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 196: ifeq2(man(skc8, X), relation(skc8, skc14), man(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 197: man(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 198: man(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 199: male(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 200: human_person(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 201: male(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 202: human_person(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 203: human(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 204: animate(skc12, skc10) -> relation(skc8, skc14) % 28.47/27.40 205: animate(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 206: human(skc12, skc15) -> relation(skc8, skc14) % 28.47/27.40 207: smoke(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 208: present(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 209: event(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 210: eventuality(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 211: nonexistent(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 212: unisex(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 213: specific(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 214: agent(skc12, skf1(skc15), skc15) -> relation(skc8, skc14) % 28.47/27.40 215: thing(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 216: agent(skc12, skf1(skc10), skc10) -> relation(skc8, skc14) % 28.47/27.40 217: singleton(skc12, skf1(X)) -> relation(skc8, skc14) % 28.47/27.40 218: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), man(X, skc10), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 219: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), man(X, skc15), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 221: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(human_person(X, Z), relation(skc8, skc14), human_person(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 222: ifeq2(human_person(skc8, X), relation(skc8, skc14), human_person(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 224: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(impartial(X, Z), relation(skc8, skc14), impartial(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 225: ifeq2(impartial(skc8, X), relation(skc8, skc14), impartial(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 227: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(existent(X, Z), relation(skc8, skc14), existent(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 228: ifeq2(existent(skc8, X), relation(skc8, skc14), existent(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 230: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(living(X, Z), relation(skc8, skc14), living(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 231: ifeq2(living(skc8, X), relation(skc8, skc14), living(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 233: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(male(X, Z), relation(skc8, skc14), male(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 234: ifeq2(male(skc8, X), relation(skc8, skc14), male(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 236: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(human(X, Z), relation(skc8, skc14), human(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 237: ifeq2(human(skc8, X), relation(skc8, skc14), human(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 239: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(forename(X, Z), relation(skc8, skc14), forename(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 240: ifeq2(forename(skc8, X), relation(skc8, skc14), forename(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 241: forename(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 242: forename(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 243: relname(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 244: relname(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 245: relation(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 246: relation(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 247: abstraction(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 248: abstraction(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 249: nonhuman(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 250: general(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 251: unisex(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 252: thing(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 253: unisex(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 254: nonhuman(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 255: general(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 256: thing(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 257: singleton(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 258: singleton(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 259: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), forename(X, skc11), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 260: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), forename(X, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 262: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(animate(X, Z), relation(skc8, skc14), animate(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 263: ifeq2(animate(skc8, X), relation(skc8, skc14), animate(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 265: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(relation(X, Z), relation(skc8, skc14), relation(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 266: ifeq2(relation(skc8, X), relation(skc8, skc14), relation(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 267: relation(skc12, skc12) -> relation(skc8, skc14) % 28.47/27.40 268: abstraction(skc12, skc12) -> relation(skc8, skc14) % 28.47/27.40 269: nonhuman(skc12, skc12) -> relation(skc8, skc14) % 28.47/27.40 270: general(skc12, skc12) -> relation(skc8, skc14) % 28.47/27.40 271: unisex(skc12, skc12) -> relation(skc8, skc14) % 28.47/27.40 272: thing(skc12, skc12) -> relation(skc8, skc14) % 28.47/27.40 273: singleton(skc12, skc12) -> relation(skc8, skc14) % 28.47/27.40 274: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), relation(X, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 276: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(relname(X, Z), relation(skc8, skc14), relname(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 277: ifeq2(relname(skc8, X), relation(skc8, skc14), relname(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 279: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(abstraction(X, Z), relation(skc8, skc14), abstraction(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 280: ifeq2(abstraction(skc8, X), relation(skc8, skc14), abstraction(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 282: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(nonhuman(X, Z), relation(skc8, skc14), nonhuman(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 283: ifeq2(nonhuman(skc8, X), relation(skc8, skc14), nonhuman(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 285: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(smoke(X, Z), relation(skc8, skc14), smoke(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 286: ifeq2(smoke(skc8, X), relation(skc8, skc14), smoke(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 288: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(jules_forename(X, Z), relation(skc8, skc14), jules_forename(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 289: ifeq2(jules_forename(skc8, X), relation(skc8, skc14), jules_forename(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 290: jules_forename(skc12, skc11) -> relation(skc8, skc14) % 28.47/27.40 291: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), jules_forename(X, skc11), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 293: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(general(X, Z), relation(skc8, skc14), general(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 294: ifeq2(general(skc8, X), relation(skc8, skc14), general(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 296: ifeq2(present(X, Y), relation(skc8, skc14), ifeq2(accessible_world(X, Z), relation(skc8, skc14), present(Z, Y), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 297: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), present(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 298: present(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 299: ifeq2(present(skc8, X), relation(skc8, skc14), present(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 301: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(proposition(X, Z), relation(skc8, skc14), proposition(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 302: ifeq2(proposition(skc8, X), relation(skc8, skc14), proposition(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 303: proposition(skc12, skc12) -> relation(skc8, skc14) % 28.47/27.40 304: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), proposition(X, skc12), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 306: ifeq2(think_believe_consider(X, Y), relation(skc8, skc14), ifeq2(accessible_world(X, Z), relation(skc8, skc14), think_believe_consider(Z, Y), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 307: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), think_believe_consider(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 308: think_believe_consider(skc12, skc13) -> relation(skc8, skc14) % 28.47/27.40 309: ifeq2(think_believe_consider(skc8, X), relation(skc8, skc14), think_believe_consider(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 311: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(vincent_forename(X, Z), relation(skc8, skc14), vincent_forename(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 312: ifeq2(vincent_forename(skc8, X), relation(skc8, skc14), vincent_forename(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 313: vincent_forename(skc12, skc14) -> relation(skc8, skc14) % 28.47/27.40 314: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), vincent_forename(X, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 316: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(eventuality(X, Z), relation(skc8, skc14), eventuality(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 317: ifeq2(eventuality(skc8, X), relation(skc8, skc14), eventuality(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 319: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(state(X, Z), relation(skc8, skc14), state(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 320: ifeq2(state(skc8, X), relation(skc8, skc14), state(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 321: state(skc12, skc9) -> relation(skc8, skc14) % 28.47/27.40 322: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), state(X, skc9), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 324: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(thing(X, Z), relation(skc8, skc14), thing(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 325: ifeq2(thing(skc8, X), relation(skc8, skc14), thing(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 327: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(specific(X, Z), relation(skc8, skc14), specific(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 328: ifeq2(specific(skc8, X), relation(skc8, skc14), specific(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 330: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(singleton(X, Z), relation(skc8, skc14), singleton(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 331: ifeq2(singleton(skc8, X), relation(skc8, skc14), singleton(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 333: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(nonexistent(X, Z), relation(skc8, skc14), nonexistent(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 334: ifeq2(nonexistent(skc8, X), relation(skc8, skc14), nonexistent(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 336: ifeq2(accessible_world(X, Y), relation(skc8, skc14), ifeq2(unisex(X, Z), relation(skc8, skc14), unisex(Y, Z), relation(skc8, skc14)), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 337: ifeq2(unisex(skc8, X), relation(skc8, skc14), unisex(skc12, X), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 338: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), eventuality(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 339: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), relname(X, skc11), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 340: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), relation(X, skc12), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 341: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), animate(X, skc15), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 342: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), event(X, skc9), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 343: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), male(X, skc15), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 344: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), male(X, skc10), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 345: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), impartial(X, skc15), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 346: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), human_person(X, skc15), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 347: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), human_person(X, skc10), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 348: ifeq2(relname(skc8, skc12), relation(skc8, skc14), relation(skc8, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 349: ifeq2(smoke(X, Y), relation(skc8, skc14), event(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 350: ifeq2(proposition(X, Y), relation(skc8, skc14), relation(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 351: ifeq2(jules_forename(X, Y), relation(skc8, skc14), forename(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 352: ifeq2(abstraction(X, Y), relation(skc8, skc14), nonhuman(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 353: ifeq2(human_person(X, Y), relation(skc8, skc14), organism(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 354: ifeq2(man(X, Y), relation(skc8, skc14), human_person(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 355: ifeq2(organism(X, Y), relation(skc8, skc14), entity(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 356: ifeq2(vincent_forename(X, Y), relation(skc8, skc14), forename(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 357: ifeq2(human_person(X, Y), relation(skc8, skc14), animate(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 358: ifeq2(organism(X, Y), relation(skc8, skc14), impartial(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 359: ifeq2(entity(X, Y), relation(skc8, skc14), specific(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 360: ifeq2(entity(X, Y), relation(skc8, skc14), existent(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 361: ifeq2(event(X, Y), relation(skc8, skc14), eventuality(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 362: ifeq2(entity(X, Y), relation(skc8, skc14), thing(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 363: ifeq2(state(X, Y), relation(skc8, skc14), event(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 364: ifeq2(abstraction(X, Y), relation(skc8, skc14), thing(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 365: ifeq2(abstraction(X, Y), relation(skc8, skc14), general(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 366: ifeq2(abstraction(X, Y), relation(skc8, skc14), unisex(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 367: ifeq2(eventuality(X, Y), relation(skc8, skc14), unisex(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 368: ifeq2(state(skc8, skc13), relation(skc8, skc14), relation(skc8, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 369: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), think_believe_consider(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 370: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), proposition(X, skc12), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 371: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), vincent_forename(X, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 372: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), specific(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 373: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), thing(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 374: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), man(X, skc10), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 375: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), man(X, skc15), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 376: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), forename(X, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 377: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), forename(X, skc11), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 378: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), jules_forename(X, skc11), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 379: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), present(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 380: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), human(X, skc10), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 381: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), human(X, skc15), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 382: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), event(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 383: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), event(X, skc9), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 384: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), animate(X, skc10), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 385: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), relation(X, skc11), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 386: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), relation(X, skc12), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 387: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), abstraction(X, skc12), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 388: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), unisex(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 389: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), eventuality(X, skc9), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 390: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), nonexistent(X, skc13), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 391: ifeq2(accessible_world(skc12, X), relation(skc8, skc14), state(X, skc9), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 392: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), organism(X, skc10), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 393: ifeq2(accessible_world(skc8, X), relation(skc8, skc14), organism(X, skc15), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 394: ifeq2(smoke(skc12, skc13), relation(skc8, skc14), relation(skc8, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 395: ifeq2(vincent_forename(skc12, skc11), relation(skc8, skc14), relation(skc8, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 396: ifeq2(smoke(skc12, skc9), relation(skc8, skc14), relation(skc8, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 397: ifeq2(entity(skc8, skc13), relation(skc8, skc14), relation(skc8, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 398: ifeq2(proposition(skc8, skc11), relation(skc8, skc14), relation(skc8, skc14), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 399: ifeq2(eventuality(X, Y), relation(skc8, skc14), nonexistent(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 400: ifeq2(state(X, Y), relation(skc8, skc14), eventuality(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 401: ifeq2(relation(X, Y), relation(skc8, skc14), abstraction(X, Y), relation(skc8, skc14)) -> relation(skc8, skc14) % 28.47/27.40 402: relation(skc8, skc14) -> abstraction(skc8, skc14) % 28.47/27.40 403: ifeq3(be(X, Y, Z, W), abstraction(skc8, skc14), Z, W) -> W % 28.47/27.40 404: ifeq2(relname(skc8, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 405: ifeq2(relation(X, Y), abstraction(skc8, skc14), abstraction(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 406: ifeq2(eventuality(X, Y), abstraction(skc8, skc14), specific(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 407: ifeq2(thing(X, Y), abstraction(skc8, skc14), singleton(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 408: ifeq2(eventuality(X, Y), abstraction(skc8, skc14), thing(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 409: ifeq2(state(X, Y), abstraction(skc8, skc14), eventuality(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 410: ifeq2(forename(X, Y), abstraction(skc8, skc14), relname(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 411: ifeq2(relname(X, Y), abstraction(skc8, skc14), relation(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 412: ifeq2(human_person(X, Y), abstraction(skc8, skc14), human(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 413: ifeq2(man(X, Y), abstraction(skc8, skc14), male(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 414: ifeq2(organism(X, Y), abstraction(skc8, skc14), living(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 415: ifeq2(jules_forename(skc12, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 416: ifeq2(jules_forename(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 417: ifeq2(smoke(skc8, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 418: ifeq2(smoke(skc8, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 419: ifeq2(state(skc12, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 420: ifeq2(relname(skc12, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 421: ifeq2(entity(skc8, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 422: ifeq2(abstraction(skc8, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 423: ifeq2(vincent_forename(skc8, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 424: ifeq2(state(skc8, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 425: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), singleton(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 426: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), entity(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 427: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), entity(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 428: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), living(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 429: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), male(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 430: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), thing(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 431: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), thing(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 432: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), specific(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 433: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), relname(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 434: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), organism(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 435: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), living(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 436: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), nonhuman(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 437: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), general(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 438: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), relname(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 439: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), relname(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 440: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), organism(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 441: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), unisex(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 442: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), unisex(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 443: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), eventuality(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 444: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), eventuality(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 445: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), abstraction(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 446: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), abstraction(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 447: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), human_person(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 448: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), human_person(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 449: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), nonexistent(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 450: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), impartial(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 451: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), male(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 452: ifeq2(man(skc12, X), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 453: ifeq2(smoke(skc12, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 454: ifeq2(smoke(skc12, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 455: ifeq2(proposition(skc8, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 456: ifeq2(accessible_world(skc12, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 457: ifeq2(accessible_world(skc12, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 458: ifeq2(entity(skc8, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 459: ifeq2(abstraction(skc8, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 460: ifeq2(eventuality(skc8, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 461: ifeq2(entity(skc8, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 462: ifeq2(vincent_forename(skc12, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 464: ifeq2(of(X, Y, Z), abstraction(skc8, skc14), ifeq2(accessible_world(X, W), abstraction(skc8, skc14), of(W, Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 465: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), of(X, skc11, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 466: of(skc12, skc11, skc10) -> abstraction(skc8, skc14) % 28.47/27.40 467: ifeq2(accessible_world(skc8, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 468: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), of(X, skc14, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 469: of(skc12, skc14, skc15) -> abstraction(skc8, skc14) % 28.47/27.40 470: ifeq2(of(skc8, X, Y), abstraction(skc8, skc14), of(skc12, X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 472: ifeq2(theme(X, Y, Z), abstraction(skc8, skc14), ifeq2(accessible_world(X, W), abstraction(skc8, skc14), theme(W, Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 473: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), theme(X, skc13, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 474: theme(skc12, skc13, skc12) -> abstraction(skc8, skc14) % 28.47/27.40 475: ifeq2(theme(skc8, X, Y), abstraction(skc8, skc14), theme(skc12, X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 477: ifeq2(agent(X, Y, Z), abstraction(skc8, skc14), ifeq2(accessible_world(X, W), abstraction(skc8, skc14), agent(W, Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 478: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), agent(X, skc13, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 479: agent(skc12, skc13, skc15) -> abstraction(skc8, skc14) % 28.47/27.40 480: ifeq2(agent(skc8, X, Y), abstraction(skc8, skc14), agent(skc12, X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 481: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), agent(X, skc13, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 482: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), theme(X, skc13, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 483: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), of(X, skc11, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 484: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), of(X, skc14, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 485: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), nonexistent(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 486: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), nonexistent(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 487: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), impartial(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 488: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), impartial(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 489: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), animate(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 490: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), animate(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 491: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), specific(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 492: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), specific(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 493: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), thing(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 494: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), thing(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 495: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), thing(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 496: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), existent(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 497: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), existent(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 498: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), relation(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 499: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), entity(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 500: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), entity(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 501: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), living(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 502: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), nonhuman(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 503: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), living(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 504: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), specific(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 505: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), specific(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 506: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), human(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 507: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), human(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 508: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), general(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 509: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), nonhuman(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 510: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), relation(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 511: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), unisex(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 512: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), unisex(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 513: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), unisex(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 514: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), unisex(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 515: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), singleton(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 516: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), singleton(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 517: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), thing(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 518: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), general(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 519: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), thing(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 520: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), thing(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 521: ifeq2(abstraction(skc8, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 522: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), present(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 523: ifeq2(proposition(skc12, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 524: ifeq2(proposition(skc12, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 525: ifeq2(entity(skc12, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 526: ifeq2(abstraction(skc12, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 527: ifeq2(entity(skc8, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 528: ifeq2(abstraction(skc8, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 529: ifeq2(eventuality(skc8, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 530: ifeq2(eventuality(skc8, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 531: ifeq2(eventuality(skc8, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 532: ifeq2(entity(X, Y), abstraction(skc8, skc14), existent(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 533: ifeq2(eventuality(X, Y), abstraction(skc8, skc14), nonexistent(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 534: ifeq2(entity(skc12, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 535: ifeq2(eventuality(skc12, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 536: ifeq2(entity(skc12, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 537: ifeq2(abstraction(skc12, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 538: ifeq2(abstraction(X, Y), abstraction(skc8, skc14), unisex(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 539: unisex(skc8, skc14) -> abstraction(skc8, skc14) % 28.47/27.40 540: ifeq2(eventuality(X, Y), abstraction(skc8, skc14), unisex(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 541: ifeq2(abstraction(X, Y), abstraction(skc8, skc14), general(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 542: general(skc8, skc14) -> abstraction(skc8, skc14) % 28.47/27.40 543: ifeq2(abstraction(X, Y), abstraction(skc8, skc14), thing(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 544: thing(skc8, skc14) -> abstraction(skc8, skc14) % 28.47/27.40 545: singleton(skc8, skc14) -> abstraction(skc8, skc14) % 28.47/27.40 546: ifeq2(entity(X, Y), abstraction(skc8, skc14), thing(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 547: ifeq2(state(X, Y), abstraction(skc8, skc14), event(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 548: ifeq2(event(X, Y), abstraction(skc8, skc14), eventuality(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 549: ifeq2(vincent_forename(X, Y), abstraction(skc8, skc14), forename(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 550: ifeq2(organism(X, Y), abstraction(skc8, skc14), impartial(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 551: ifeq2(human_person(X, Y), abstraction(skc8, skc14), animate(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 552: ifeq2(entity(X, Y), abstraction(skc8, skc14), specific(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 553: ifeq2(organism(X, Y), abstraction(skc8, skc14), entity(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 554: ifeq2(man(X, Y), abstraction(skc8, skc14), human_person(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 555: ifeq2(human_person(X, Y), abstraction(skc8, skc14), organism(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 556: ifeq2(abstraction(X, Y), abstraction(skc8, skc14), nonhuman(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 557: nonhuman(skc8, skc14) -> abstraction(skc8, skc14) % 28.47/27.40 558: ifeq2(jules_forename(X, Y), abstraction(skc8, skc14), forename(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 559: ifeq2(smoke(X, Y), abstraction(skc8, skc14), event(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 560: ifeq2(proposition(X, Y), abstraction(skc8, skc14), relation(X, Y), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 561: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), event(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 562: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), smoke(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 563: ifeq2(organism(skc8, X), abstraction(skc8, skc14), organism(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 564: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), relation(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 565: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), singleton(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 566: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), singleton(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 567: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), singleton(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 568: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), singleton(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 569: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), existent(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 570: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), existent(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 571: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), specific(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 572: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), thing(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 573: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), specific(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 574: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), thing(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 575: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), man(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 576: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), specific(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 577: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), vincent_forename(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 578: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), think_believe_consider(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 579: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), proposition(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 580: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), state(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 581: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), man(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 582: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), unisex(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 583: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), nonexistent(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 584: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), eventuality(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 585: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), abstraction(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 586: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), relation(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 587: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), relation(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 588: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), animate(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 589: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), event(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 590: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), human(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 591: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), event(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 592: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), human(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 593: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), present(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 594: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), forename(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 595: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), jules_forename(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 596: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), forename(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 597: ifeq2(smoke(skc8, X), abstraction(skc8, skc14), smoke(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 598: ifeq2(jules_forename(skc8, X), abstraction(skc8, skc14), jules_forename(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 599: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), jules_forename(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 600: ifeq2(nonhuman(skc8, X), abstraction(skc8, skc14), nonhuman(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 601: ifeq2(abstraction(skc8, X), abstraction(skc8, skc14), abstraction(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 602: ifeq2(relname(skc8, X), abstraction(skc8, skc14), relname(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 603: ifeq2(animate(skc8, X), abstraction(skc8, skc14), animate(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 604: ifeq2(relation(skc8, X), abstraction(skc8, skc14), relation(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 605: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), forename(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 606: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), forename(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 607: ifeq2(forename(skc8, X), abstraction(skc8, skc14), forename(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 608: ifeq2(human(skc8, X), abstraction(skc8, skc14), human(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 609: ifeq2(male(skc8, X), abstraction(skc8, skc14), male(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 610: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), singleton(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 611: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), thing(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 612: ifeq2(present(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 613: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), abstraction(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 614: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), abstraction(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 615: ifeq2(man(skc8, X), abstraction(skc8, skc14), man(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 616: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), singleton(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 617: ifeq2(entity(skc8, X), abstraction(skc8, skc14), entity(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 618: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), event(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 619: ifeq2(event(skc8, X), abstraction(skc8, skc14), event(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 620: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), organism(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 621: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), organism(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 622: ifeq2(living(skc8, X), abstraction(skc8, skc14), living(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 623: ifeq2(existent(skc8, X), abstraction(skc8, skc14), existent(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 624: ifeq2(impartial(skc8, X), abstraction(skc8, skc14), impartial(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 625: ifeq2(human_person(skc8, X), abstraction(skc8, skc14), human_person(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 626: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), man(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 627: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), man(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 628: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), animate(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 629: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), event(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 630: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), male(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 631: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), relation(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 632: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), relname(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 633: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), eventuality(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 634: ifeq2(unisex(skc8, X), abstraction(skc8, skc14), unisex(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 635: ifeq2(nonexistent(skc8, X), abstraction(skc8, skc14), nonexistent(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 636: ifeq2(singleton(skc8, X), abstraction(skc8, skc14), singleton(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 637: ifeq2(specific(skc8, X), abstraction(skc8, skc14), specific(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 638: ifeq2(thing(skc8, X), abstraction(skc8, skc14), thing(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 639: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), state(X, skc9), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 640: ifeq2(state(skc8, X), abstraction(skc8, skc14), state(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 641: ifeq2(eventuality(skc8, X), abstraction(skc8, skc14), eventuality(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 642: ifeq2(vincent_forename(skc8, X), abstraction(skc8, skc14), vincent_forename(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 643: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), vincent_forename(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 644: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), think_believe_consider(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 645: ifeq2(think_believe_consider(skc8, X), abstraction(skc8, skc14), think_believe_consider(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 646: ifeq2(proposition(skc8, X), abstraction(skc8, skc14), proposition(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 647: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), proposition(X, skc12), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 648: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), present(X, skc13), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 649: ifeq2(present(skc8, X), abstraction(skc8, skc14), present(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 650: ifeq2(general(skc8, X), abstraction(skc8, skc14), general(skc12, X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 651: ifeq2(state(skc12, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 652: ifeq2(smoke(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 653: ifeq2(event(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 654: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), human_person(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 655: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), human_person(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 656: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), impartial(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 657: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), male(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 658: ifeq2(abstraction(skc12, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 659: ifeq2(eventuality(skc12, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 660: ifeq2(abstraction(skc12, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 661: ifeq2(eventuality(skc12, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 662: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), eventuality(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 663: ifeq2(proposition(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 664: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), nonhuman(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 665: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), general(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 666: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), general(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 667: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), singleton(X, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 668: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), thing(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 669: ifeq2(eventuality(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 670: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), singleton(X, skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 671: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), thing(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 672: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), unisex(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 673: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), unisex(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 674: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), nonhuman(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 675: ifeq2(man(skc12, X), abstraction(skc8, skc14), agent(skc12, skf1(X), X), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 676: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), nonexistent(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 677: ifeq2(eventuality(skc12, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 678: ifeq2(eventuality(skc12, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 679: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), agent(X, skf1(skc15), skc15), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 680: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), agent(X, skf1(skc10), skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 681: ifeq2(entity(skc12, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 682: ifeq2(entity(skc12, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 683: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), thing(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 684: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), specific(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 685: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), unisex(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 687: ifeq2(be(X, Y, Z, W), abstraction(skc8, skc14), ifeq2(accessible_world(X, V), abstraction(skc8, skc14), be(V, Y, Z, W), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 688: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), be(X, skc9, skc10, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 689: be(skc12, skc9, skc10, skc10) -> abstraction(skc8, skc14) % 28.47/27.40 690: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), be(X, skc9, skc10, skc10), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 691: ifeq2(be(skc8, X, Y, Z), abstraction(skc8, skc14), be(skc12, X, Y, Z), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 692: ifeq2(agent(skc8, skf1(skc10), skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 693: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), singleton(X, skc11), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 694: ifeq2(abstraction(skc12, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 695: ifeq2(entity(skc12, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 696: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), nonhuman(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 697: ifeq2(unisex(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 698: ifeq2(specific(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 699: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), unisex(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 700: ifeq2(nonexistent(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 701: ifeq2(thing(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 702: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), singleton(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 703: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), thing(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 704: ifeq2(agent(skc8, skf1(skc15), skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 705: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), general(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 706: ifeq2(entity(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 707: ifeq2(eventuality(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 708: ifeq2(accessible_world(skc12, X), abstraction(skc8, skc14), singleton(X, skf1(Y)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 709: ifeq(tuple(unisex(skc8, skc15), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 710: ifeq(tuple(unisex(skc8, skc10), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 711: ifeq2(singleton(skc8, skf1(X)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 712: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), singleton(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 713: ifeq(tuple(human(X, Y), nonhuman(X, Y)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 714: ifeq(tuple(unisex(X, Y), male(X, Y)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 715: ifeq(tuple(abstraction(skc8, skc14), existent(skc8, skc13)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 716: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 717: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 718: ifeq(tuple(abstraction(skc8, skc14), general(skc8, skc13)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 719: ifeq(tuple(abstraction(skc8, skc14), nonhuman(skc8, skc15)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 720: ifeq(tuple(abstraction(skc8, skc14), nonhuman(skc8, skc10)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 721: ifeq(tuple(abstraction(skc8, skc14), male(skc8, skc13)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 722: ifeq(tuple(abstraction(skc8, skc14), male(skc8, skc12)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 723: ifeq(tuple(abstraction(skc8, skc14), male(skc8, skc9)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 724: ifeq(tuple(human(skc8, skc12), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 725: ifeq(tuple(specific(skc8, skc12), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 726: ifeq(tuple(abstraction(skc8, skc14), existent(skc8, skc9)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 727: ifeq(tuple(unisex(skc12, skc10), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 728: ifeq(tuple(abstraction(skc8, skc14), general(skc8, skc9)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 729: ifeq(tuple(unisex(skc12, skc15), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 730: ifeq(tuple(abstraction(skc8, skc14), existent(skc12, skc9)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 731: ifeq(tuple(nonexistent(skc8, skc10), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 732: ifeq(tuple(nonexistent(skc8, skc15), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 733: ifeq(tuple(abstraction(skc8, skc14), nonhuman(skc12, skc10)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 734: ifeq(tuple(abstraction(skc8, skc14), general(skc12, skc13)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 735: ifeq(tuple(abstraction(skc8, skc14), general(skc12, skc9)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 736: ifeq(tuple(human(skc8, skc11), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 737: ifeq(tuple(abstraction(skc8, skc14), nonhuman(skc12, skc15)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 738: ifeq(tuple(human(skc12, skc12), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 739: ifeq(tuple(abstraction(skc8, skc14), male(skc12, skc13)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 740: ifeq(tuple(abstraction(skc8, skc14), male(skc12, skc12)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 741: ifeq(tuple(abstraction(skc8, skc14), male(skc8, skc11)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 742: ifeq(tuple(abstraction(skc8, skc14), male(skc12, skc9)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 743: ifeq(tuple(abstraction(skc8, skc14), existent(skc12, skc13)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 744: ifeq(tuple(abstraction(skc8, skc14), general(skc8, skc15)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 745: ifeq(tuple(abstraction(skc8, skc14), general(skc8, skc10)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 746: ifeq(tuple(specific(skc12, skc12), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 747: ifeq(tuple(specific(skc8, skc11), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 748: ifeq(tuple(abstraction(skc8, skc14), general(skc12, skc15)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 749: ifeq(tuple(abstraction(skc8, skc14), general(skc12, skc10)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 750: ifeq(tuple(nonexistent(skc12, skc15), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 751: ifeq(tuple(nonexistent(skc12, skc10), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 752: ifeq(tuple(human(skc12, skc11), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 753: ifeq(tuple(abstraction(skc8, skc14), male(skc12, skc11)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 754: ifeq(tuple(abstraction(skc8, skc14), male(skc12, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 755: ifeq(tuple(human(skc12, skc14), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 756: ifeq(tuple(specific(skc12, skc11), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 757: ifeq(tuple(specific(skc12, skc14), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 758: ifeq(tuple(abstraction(skc8, skc14), male(skc12, skf1(X))), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 759: ifeq(tuple(abstraction(skc8, skc14), existent(skc12, skf1(X))), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 760: ifeq(tuple(abstraction(skc8, skc14), general(skc12, skf1(X))), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 761: ifeq(tuple(specific(skc8, skc14), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 762: ifeq(tuple(human(skc8, skc14), abstraction(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 763: ifeq(tuple(abstraction(skc8, skc14), male(skc8, skc14)), tuple(abstraction(skc8, skc14), abstraction(skc8, skc14)), a, b) -> b % 28.47/27.40 764: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(state(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 765: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(forename(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 766: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(forename(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 767: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(event(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 768: ifeq2(present(X, skc13), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 769: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(proposition(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 770: ifeq2(think_believe_consider(X, skc13), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 771: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(vincent_forename(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 772: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(man(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 773: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(man(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 774: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(jules_forename(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 775: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(relname(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 776: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(animate(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 777: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(event(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 778: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(male(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 779: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(male(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 780: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(eventuality(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 781: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(human_person(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 782: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(human_person(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 783: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(impartial(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 784: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(relation(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 785: ifeq2(theme(X, skc13, skc12), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 786: ifeq2(of(X, skc14, skc15), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 787: ifeq2(of(X, skc11, skc10), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 788: ifeq2(agent(X, skc13, skc15), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 789: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(nonexistent(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 790: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(man(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 791: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(organism(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 792: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(relation(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 793: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(abstraction(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 794: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(vincent_forename(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 795: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(animate(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 796: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(specific(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 797: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(jules_forename(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 798: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(unisex(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 799: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(organism(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 800: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(relation(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 801: ifeq2(present(X, skc13), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 802: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(human(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 803: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(proposition(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 804: ifeq2(think_believe_consider(X, skc13), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 805: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(human(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 806: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(state(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 807: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(man(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 808: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(eventuality(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 809: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(event(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 810: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(thing(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 811: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(event(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 812: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(forename(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 813: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(forename(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 814: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(eventuality(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 815: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(human_person(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 816: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(human_person(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 817: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(male(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 818: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(thing(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 819: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(nonhuman(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 820: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(general(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 821: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(abstraction(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 822: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(abstraction(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 823: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(living(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 824: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(living(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 825: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(organism(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 826: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(singleton(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 827: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(organism(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 828: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(nonexistent(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 829: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(unisex(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 830: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(relname(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 831: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(impartial(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 832: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(specific(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 833: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(thing(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 834: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(unisex(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 835: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(eventuality(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 836: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(entity(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 837: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(relname(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 838: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(entity(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 839: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(male(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 840: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(relname(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 841: ifeq2(be(X, skc9, skc10, skc10), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 842: ifeq2(theme(X, skc13, skc12), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 843: ifeq2(of(X, skc11, skc10), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 844: ifeq2(agent(X, skc13, skc15), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 845: ifeq2(of(X, skc14, skc15), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 846: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(specific(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 847: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(thing(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 848: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(thing(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 849: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(thing(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 850: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(general(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 851: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(entity(X, Z), abstraction(skc8, skc14), entity(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 852: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(man(X, Z), abstraction(skc8, skc14), man(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 853: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(nonexistent(X, Z), abstraction(skc8, skc14), nonexistent(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 854: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(specific(X, Z), abstraction(skc8, skc14), specific(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 855: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(smoke(X, Z), abstraction(skc8, skc14), smoke(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 856: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(organism(X, Z), abstraction(skc8, skc14), organism(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 857: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(impartial(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 858: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(singleton(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 859: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(animate(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 860: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(animate(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 861: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(specific(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 862: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(specific(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 863: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(specific(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 864: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(event(X, Z), abstraction(skc8, skc14), event(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 865: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(unisex(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 866: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(nonhuman(X, Z), abstraction(skc8, skc14), nonhuman(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 867: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(animate(X, Z), abstraction(skc8, skc14), animate(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 868: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(relation(X, Z), abstraction(skc8, skc14), relation(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 869: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(forename(X, Z), abstraction(skc8, skc14), forename(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 870: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(relname(X, Z), abstraction(skc8, skc14), relname(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 871: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(abstraction(X, Z), abstraction(skc8, skc14), abstraction(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 872: ifeq2(accessible_world(skc8, X), abstraction(skc8, skc14), abstraction(X, skc14), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 873: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(general(X, Z), abstraction(skc8, skc14), general(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 874: ifeq2(present(X, Y), abstraction(skc8, skc14), ifeq2(accessible_world(X, Z), abstraction(skc8, skc14), present(Z, Y), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 875: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(nonhuman(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 876: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(nonhuman(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 877: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(proposition(X, Z), abstraction(skc8, skc14), proposition(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 878: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(relation(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 879: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(living(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 880: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(male(X, Z), abstraction(skc8, skc14), male(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 881: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(unisex(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 882: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(human(X, Z), abstraction(skc8, skc14), human(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 883: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(jules_forename(X, Z), abstraction(skc8, skc14), jules_forename(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 884: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(nonexistent(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 885: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(singleton(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 886: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(unisex(X, Z), abstraction(skc8, skc14), unisex(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 887: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(relation(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 888: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(entity(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 889: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(entity(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 890: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(nonexistent(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 891: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(impartial(X, Z), abstraction(skc8, skc14), impartial(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 892: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(human_person(X, Z), abstraction(skc8, skc14), human_person(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 893: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(singleton(X, Z), abstraction(skc8, skc14), singleton(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 894: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(thing(X, Z), abstraction(skc8, skc14), thing(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 895: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(unisex(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 896: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(unisex(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 897: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(thing(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 898: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(existent(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 899: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(existent(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 900: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(impartial(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 901: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(eventuality(X, Z), abstraction(skc8, skc14), eventuality(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 902: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(state(X, Z), abstraction(skc8, skc14), state(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 903: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(living(X, Z), abstraction(skc8, skc14), living(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 904: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(vincent_forename(X, Z), abstraction(skc8, skc14), vincent_forename(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 905: ifeq2(think_believe_consider(X, Y), abstraction(skc8, skc14), ifeq2(accessible_world(X, Z), abstraction(skc8, skc14), think_believe_consider(Z, Y), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 906: ifeq2(accessible_world(X, Y), abstraction(skc8, skc14), ifeq2(existent(X, Z), abstraction(skc8, skc14), existent(Y, Z), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 907: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(general(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 908: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(thing(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 909: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(thing(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 910: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(human(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 911: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(human(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 912: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(living(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 913: ifeq2(present(X, skf1(Y)), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 914: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(smoke(X, skf1(Y)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 915: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(event(X, skf1(Y)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 916: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(relation(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 917: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(singleton(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 918: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(abstraction(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 919: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(abstraction(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 920: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(specific(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 921: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(specific(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 922: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(singleton(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 923: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(thing(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 924: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(existent(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 925: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(thing(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 926: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(singleton(X, skc9), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 927: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(singleton(X, skc13), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 928: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(singleton(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 929: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(singleton(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 930: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(existent(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 931: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(eventuality(X, skf1(Y)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 932: ifeq2(be(X, skc9, skc10, skc10), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 933: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(nonhuman(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 934: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(singleton(X, skc10), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 935: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(nonhuman(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 936: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(general(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 937: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(general(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 938: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(unisex(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 939: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(unisex(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 940: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(thing(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 941: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(thing(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 942: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(singleton(X, skc15), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 943: ifeq2(agent(X, skf1(skc10), skc10), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 944: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(nonexistent(X, skf1(Y)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 945: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(thing(X, skf1(Y)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 946: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(unisex(X, skf1(Y)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 947: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(specific(X, skf1(Y)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 948: ifeq2(agent(X, skf1(skc15), skc15), abstraction(skc8, skc14), ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 949: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(singleton(X, skc11), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 950: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(unisex(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 951: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(thing(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 952: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(nonhuman(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 953: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(singleton(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 954: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(general(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 955: ifeq2(accessible_world(X, skc12), abstraction(skc8, skc14), ifeq2(singleton(X, skf1(Y)), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 956: ifeq2(accessible_world(X, skc8), abstraction(skc8, skc14), ifeq2(singleton(X, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14), abstraction(skc8, skc14)), abstraction(skc8, skc14)) -> abstraction(skc8, skc14) % 28.47/27.40 958: ifeq3(of(X, Y, Z), abstraction(skc8, skc14), ifeq3(of(X, W, Z), abstraction(skc8, skc14), ifeq3(forename(X, Y), abstraction(skc8, skc14), ifeq3(forename(X, W), abstraction(skc8, skc14), ifeq3(entity(X, Z), abstraction(skc8, skc14), Y, W), W), W), W), W) -> W % 28.47/27.40 959: ifeq3(of(skc8, X, skc10), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), skc11, X), X) -> X % 28.47/27.40 960: ifeq3(of(skc8, skc14, skc10), abstraction(skc8, skc14), skc11, skc14) -> skc14 % 28.47/27.40 961: ifeq3(of(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), skc14, X), X) -> X % 28.47/27.40 962: ifeq3(of(skc8, skc11, skc15), abstraction(skc8, skc14), skc14, skc11) -> skc11 % 28.47/27.40 963: ifeq3(of(skc8, X, skc10), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), X, skc11), skc11) -> skc11 % 28.47/27.40 964: ifeq3(of(skc8, skc14, skc10), abstraction(skc8, skc14), skc14, skc11) -> skc11 % 28.47/27.40 965: ifeq3(of(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), X, skc14), skc14) -> skc14 % 28.47/27.40 966: ifeq3(of(skc8, skc11, skc15), abstraction(skc8, skc14), skc11, skc14) -> skc14 % 28.47/27.40 967: ifeq3(of(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), skc14, X), X) -> X % 28.47/27.40 968: ifeq3(of(skc12, skc11, skc15), abstraction(skc8, skc14), skc14, skc11) -> skc11 % 28.47/27.40 969: ifeq3(of(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), skc11, X), X) -> X % 28.47/27.40 970: ifeq3(of(skc12, skc14, skc10), abstraction(skc8, skc14), skc11, skc14) -> skc14 % 28.47/27.40 971: ifeq3(of(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), X, skc11), skc11) -> skc11 % 28.47/27.40 972: ifeq3(of(skc12, skc14, skc10), abstraction(skc8, skc14), skc14, skc11) -> skc11 % 28.47/27.40 973: ifeq3(of(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), X, skc14), skc14) -> skc14 % 28.47/27.40 974: ifeq3(of(skc12, skc11, skc15), abstraction(skc8, skc14), skc11, skc14) -> skc14 % 28.47/27.40 975: ifeq3(of(skc8, skc11, X), abstraction(skc8, skc14), ifeq3(of(skc8, Y, X), abstraction(skc8, skc14), ifeq3(forename(skc8, Y), abstraction(skc8, skc14), ifeq3(entity(skc8, X), abstraction(skc8, skc14), skc11, Y), Y), Y), Y) -> Y % 28.47/27.40 976: ifeq3(of(skc8, skc11, X), abstraction(skc8, skc14), ifeq3(of(skc8, skc11, X), abstraction(skc8, skc14), ifeq3(entity(skc8, X), abstraction(skc8, skc14), skc11, skc11), skc11), skc11) -> skc11 % 28.47/27.40 977: ifeq3(of(skc8, skc11, skc15), abstraction(skc8, skc14), ifeq3(of(skc8, skc11, skc15), abstraction(skc8, skc14), skc11, skc11), skc11) -> skc11 % 28.47/27.40 978: ifeq3(of(skc8, skc11, X), abstraction(skc8, skc14), ifeq3(of(skc8, skc14, X), abstraction(skc8, skc14), ifeq3(entity(skc8, X), abstraction(skc8, skc14), skc11, skc14), skc14), skc14) -> skc14 % 28.47/27.40 979: ifeq3(of(skc8, skc11, skc15), abstraction(skc8, skc14), ifeq3(of(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), skc11, X), X), X) -> X % 28.47/27.40 980: ifeq3(of(skc8, skc14, X), abstraction(skc8, skc14), ifeq3(of(skc8, Y, X), abstraction(skc8, skc14), ifeq3(forename(skc8, Y), abstraction(skc8, skc14), ifeq3(entity(skc8, X), abstraction(skc8, skc14), skc14, Y), Y), Y), Y) -> Y % 28.47/27.40 981: ifeq3(of(skc8, skc14, X), abstraction(skc8, skc14), ifeq3(of(skc8, skc11, X), abstraction(skc8, skc14), ifeq3(entity(skc8, X), abstraction(skc8, skc14), skc14, skc11), skc11), skc11) -> skc11 % 28.47/27.40 982: ifeq3(of(skc8, skc14, X), abstraction(skc8, skc14), ifeq3(of(skc8, skc14, X), abstraction(skc8, skc14), ifeq3(entity(skc8, X), abstraction(skc8, skc14), skc14, skc14), skc14), skc14) -> skc14 % 28.47/27.40 983: ifeq3(of(skc8, skc14, skc10), abstraction(skc8, skc14), ifeq3(of(skc8, skc14, skc10), abstraction(skc8, skc14), skc14, skc14), skc14) -> skc14 % 28.47/27.40 984: ifeq3(of(skc8, skc14, skc10), abstraction(skc8, skc14), ifeq3(of(skc8, X, skc10), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), skc14, X), X), X) -> X % 28.47/27.40 985: ifeq3(of(skc8, X, Y), abstraction(skc8, skc14), ifeq3(of(skc8, skc11, Y), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), ifeq3(entity(skc8, Y), abstraction(skc8, skc14), X, skc11), skc11), skc11), skc11) -> skc11 % 28.47/27.40 986: ifeq3(of(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(of(skc8, skc11, skc15), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), X, skc11), skc11), skc11) -> skc11 % 28.47/27.40 987: ifeq3(of(skc8, X, Y), abstraction(skc8, skc14), ifeq3(of(skc8, skc14, Y), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), ifeq3(entity(skc8, Y), abstraction(skc8, skc14), X, skc14), skc14), skc14), skc14) -> skc14 % 28.47/27.40 988: ifeq3(of(skc8, X, skc10), abstraction(skc8, skc14), ifeq3(of(skc8, skc14, skc10), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), X, skc14), skc14), skc14) -> skc14 % 28.47/27.40 989: ifeq3(of(skc12, skc14, X), abstraction(skc8, skc14), ifeq3(of(skc12, Y, X), abstraction(skc8, skc14), ifeq3(forename(skc12, Y), abstraction(skc8, skc14), ifeq3(entity(skc12, X), abstraction(skc8, skc14), skc14, Y), Y), Y), Y) -> Y % 28.47/27.40 990: ifeq3(of(skc12, skc14, X), abstraction(skc8, skc14), ifeq3(of(skc12, skc11, X), abstraction(skc8, skc14), ifeq3(entity(skc12, X), abstraction(skc8, skc14), skc14, skc11), skc11), skc11) -> skc11 % 28.47/27.40 991: ifeq3(of(skc12, skc14, X), abstraction(skc8, skc14), ifeq3(of(skc12, skc14, X), abstraction(skc8, skc14), ifeq3(entity(skc12, X), abstraction(skc8, skc14), skc14, skc14), skc14), skc14) -> skc14 % 28.47/27.40 992: ifeq3(of(skc12, skc14, skc10), abstraction(skc8, skc14), ifeq3(of(skc12, skc14, skc10), abstraction(skc8, skc14), skc14, skc14), skc14) -> skc14 % 28.47/27.40 993: ifeq3(of(skc12, skc14, skc10), abstraction(skc8, skc14), ifeq3(of(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), skc14, X), X), X) -> X % 28.47/27.40 994: ifeq3(of(skc12, skc11, X), abstraction(skc8, skc14), ifeq3(of(skc12, Y, X), abstraction(skc8, skc14), ifeq3(forename(skc12, Y), abstraction(skc8, skc14), ifeq3(entity(skc12, X), abstraction(skc8, skc14), skc11, Y), Y), Y), Y) -> Y % 28.47/27.40 995: ifeq3(of(skc12, skc11, X), abstraction(skc8, skc14), ifeq3(of(skc12, skc11, X), abstraction(skc8, skc14), ifeq3(entity(skc12, X), abstraction(skc8, skc14), skc11, skc11), skc11), skc11) -> skc11 % 28.47/27.40 996: ifeq3(of(skc12, skc11, skc15), abstraction(skc8, skc14), ifeq3(of(skc12, skc11, skc15), abstraction(skc8, skc14), skc11, skc11), skc11) -> skc11 % 28.47/27.40 997: ifeq3(of(skc12, skc11, X), abstraction(skc8, skc14), ifeq3(of(skc12, skc14, X), abstraction(skc8, skc14), ifeq3(entity(skc12, X), abstraction(skc8, skc14), skc11, skc14), skc14), skc14) -> skc14 % 28.47/27.40 998: ifeq3(of(skc12, skc11, skc15), abstraction(skc8, skc14), ifeq3(of(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), skc11, X), X), X) -> X % 28.47/27.40 999: ifeq3(of(skc12, X, Y), abstraction(skc8, skc14), ifeq3(of(skc12, skc11, Y), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), ifeq3(entity(skc12, Y), abstraction(skc8, skc14), X, skc11), skc11), skc11), skc11) -> skc11 % 28.47/27.40 1000: ifeq3(of(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(of(skc12, skc11, skc15), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), X, skc11), skc11), skc11) -> skc11 % 28.47/27.40 1001: ifeq3(of(skc12, X, Y), abstraction(skc8, skc14), ifeq3(of(skc12, skc14, Y), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), ifeq3(entity(skc12, Y), abstraction(skc8, skc14), X, skc14), skc14), skc14), skc14) -> skc14 % 28.47/27.40 1002: ifeq3(of(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(of(skc12, skc14, skc10), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), X, skc14), skc14), skc14) -> skc14 % 28.47/27.40 1003: ifeq3(of(skc8, X, skc10), abstraction(skc8, skc14), ifeq3(of(skc8, Y, skc10), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), ifeq3(forename(skc8, Y), abstraction(skc8, skc14), X, Y), Y), Y), Y) -> Y % 28.47/27.40 1004: ifeq3(of(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(of(skc8, Y, skc15), abstraction(skc8, skc14), ifeq3(forename(skc8, X), abstraction(skc8, skc14), ifeq3(forename(skc8, Y), abstraction(skc8, skc14), X, Y), Y), Y), Y) -> Y % 28.47/27.40 1005: ifeq3(of(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(of(skc12, Y, skc10), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), ifeq3(forename(skc12, Y), abstraction(skc8, skc14), X, Y), Y), Y), Y) -> Y % 28.47/27.40 1006: ifeq3(of(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(of(skc12, Y, skc15), abstraction(skc8, skc14), ifeq3(forename(skc12, X), abstraction(skc8, skc14), ifeq3(forename(skc12, Y), abstraction(skc8, skc14), X, Y), Y), Y), Y) -> Y % 28.47/27.40 1008: ifeq3(theme(X, Y, Z), abstraction(skc8, skc14), ifeq3(theme(X, W, V), abstraction(skc8, skc14), ifeq3(agent(X, Y, U), abstraction(skc8, skc14), ifeq3(agent(X, W, U), abstraction(skc8, skc14), ifeq3(think_believe_consider(X, Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(X, W), abstraction(skc8, skc14), ifeq3(proposition(X, Z), abstraction(skc8, skc14), ifeq3(proposition(X, V), abstraction(skc8, skc14), V, Z), Z), Z), Z), Z), Z), Z), Z) -> Z % 28.47/27.40 1009: ifeq3(theme(skc8, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, X, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), skc12, Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1010: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), skc12, X), X) -> X % 28.47/27.40 1011: ifeq3(agent(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, X), abstraction(skc8, skc14), skc12, skc12), skc12) -> skc12 % 28.47/27.40 1012: ifeq3(theme(skc8, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), skc12, Y), Y), Y), Y) -> Y % 28.47/27.40 1013: ifeq3(theme(skc8, X, skc12), abstraction(skc8, skc14), ifeq3(agent(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), skc12, skc12), skc12), skc12) -> skc12 % 28.47/27.40 1014: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), skc12, X), X), X), X) -> X % 28.47/27.40 1015: ifeq3(theme(skc8, X, skc12), abstraction(skc8, skc14), ifeq3(agent(skc8, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1016: ifeq3(theme(skc8, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, X, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1017: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), X, skc12), skc12) -> skc12 % 28.47/27.40 1018: ifeq3(theme(skc8, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1019: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), X, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1020: ifeq3(theme(skc8, X, skc12), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, X, Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1021: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), skc12, Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1022: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X) -> X % 28.47/27.40 1023: ifeq3(agent(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, X), abstraction(skc8, skc14), skc12, skc12), skc12) -> skc12 % 28.47/27.40 1024: ifeq3(theme(skc12, skf1(skc15), X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X) -> X % 28.47/27.40 1025: ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), skc12, skc12), skc12) -> skc12 % 28.47/27.40 1026: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), skc12, Y), Y), Y), Y) -> Y % 28.47/27.40 1027: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), skc12, skc12), skc12), skc12) -> skc12 % 28.47/27.40 1028: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X) -> X % 28.47/27.40 1029: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1030: ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), skc12, skc12), skc12), skc12) -> skc12 % 28.47/27.40 1031: ifeq3(theme(skc12, skf1(skc10), X), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X) -> X % 28.47/27.40 1032: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, X, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1033: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), X, skc12), skc12) -> skc12 % 28.47/27.40 1034: ifeq3(theme(skc12, skf1(skc15), X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), X, skc12), skc12), skc12) -> skc12 % 28.47/27.40 1035: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1036: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), X, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1037: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1038: ifeq3(theme(skc12, skf1(skc10), X), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), X, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1039: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc8, Y, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, Y, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Z), abstraction(skc8, skc14), Z, X), X), X), X), X), X) -> X % 28.47/27.40 1040: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), Y, X), X), X), X) -> X % 28.47/27.40 1041: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc8, Y, skc12), abstraction(skc8, skc14), ifeq3(agent(skc8, Y, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), skc12, X), X), X), X), X) -> X % 28.47/27.40 1042: ifeq3(theme(skc8, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc8, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, Z), abstraction(skc8, skc14), Z, Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1043: ifeq3(theme(skc8, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1044: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1045: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, X), X), X), X) -> X % 28.47/27.40 1046: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1047: ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), X, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1048: ifeq3(theme(skc12, skf1(skc15), X), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, X), X), X), X), X) -> X % 28.47/27.40 1049: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, X), X), X), X), X), X) -> X % 28.47/27.40 1050: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X), X) -> X % 28.47/27.40 1051: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X) -> X % 28.47/27.40 1052: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, X), X), X), X), X) -> X % 28.47/27.40 1053: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc8, Y, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, W), abstraction(skc8, skc14), ifeq3(agent(skc8, Y, W), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Z), abstraction(skc8, skc14), Z, X), X), X), X), X), X), X) -> X % 28.47/27.40 1054: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Z), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), Y, X), X), X), X), X), X) -> X % 28.47/27.40 1055: ifeq3(theme(skc8, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc8, Y, skc12), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, Y, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, X), abstraction(skc8, skc14), skc12, X), X), X), X), X), X) -> X % 28.47/27.40 1056: ifeq3(theme(skc8, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc8, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, X, W), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, W), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, Z), abstraction(skc8, skc14), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1057: ifeq3(theme(skc8, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc8, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc8, X, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, skc13, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1058: ifeq3(theme(skc8, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc8, Z, skc12), abstraction(skc8, skc14), ifeq3(agent(skc8, X, W), abstraction(skc8, skc14), ifeq3(agent(skc8, Z, W), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, Z), abstraction(skc8, skc14), ifeq3(proposition(skc8, Y), abstraction(skc8, skc14), skc12, Y), Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1059: ifeq3(theme(skc8, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc8, Y, skc12), abstraction(skc8, skc14), ifeq3(agent(skc8, X, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, Y, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, Y), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1060: ifeq3(theme(skc8, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc8, Y, Z), abstraction(skc8, skc14), ifeq3(agent(skc8, X, W), abstraction(skc8, skc14), ifeq3(agent(skc8, Y, W), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc8, Y), abstraction(skc8, skc14), ifeq3(proposition(skc8, Z), abstraction(skc8, skc14), Z, skc12), skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1061: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc12, Z, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, W), abstraction(skc8, skc14), ifeq3(agent(skc12, Z, W), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Z), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), skc12, Y), Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1062: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X), X), X) -> X % 28.47/27.40 1063: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X), X) -> X % 28.47/27.40 1064: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1065: ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1066: ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1067: ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1068: ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1069: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1070: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), skc12, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1071: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), skc12, Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1072: ifeq3(theme(skc12, skf1(skc10), X), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X), X) -> X % 28.47/27.40 1073: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), skc12, Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1074: ifeq3(theme(skc12, skf1(skc15), X), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X), X) -> X % 28.47/27.40 1075: ifeq3(theme(skc12, skf1(skc10), X), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X), X), X) -> X % 28.47/27.40 1076: ifeq3(theme(skc12, skf1(skc15), X), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, skc12), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), skc12, X), X), X), X), X), X) -> X % 28.47/27.40 1077: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, X, W), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, W), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1078: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Z), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, X), X), X), X), X), X) -> X % 28.47/27.40 1079: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, Z), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1080: ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), X, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1081: ifeq3(theme(skc12, skf1(skc10), X), abstraction(skc8, skc14), ifeq3(theme(skc12, skc13, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, X), X), X), X), X), X) -> X % 28.47/27.40 1082: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, W), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, W), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, X), X), X), X), X), X), X) -> X % 28.47/27.40 1083: ifeq3(theme(skc12, skc13, X), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), Y), abstraction(skc8, skc14), ifeq3(agent(skc12, skc13, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, X), X), X), X), X), X) -> X % 28.47/27.40 1084: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, X, W), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, W), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, skc12), skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1085: ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1086: ifeq3(theme(skc12, skf1(skc10), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), X, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1087: ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1088: ifeq3(theme(skc12, skf1(skc15), skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), X, skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1089: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1090: ifeq3(theme(skc12, X, skc12), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), Y), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, skc12), skc12), skc12), skc12), skc12), skc12) -> skc12 % 28.47/27.40 1091: ifeq3(theme(skc12, skf1(skc15), X), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, X), X), X), X), X), X), X) -> X % 28.47/27.40 1092: ifeq3(theme(skc12, skf1(skc15), X), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, X), X), X), X), X), X) -> X % 28.47/27.40 1093: ifeq3(theme(skc12, skf1(skc10), X), abstraction(skc8, skc14), ifeq3(theme(skc12, Y, Z), abstraction(skc8, skc14), ifeq3(agent(skc12, Y, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, X), X), X), X), X), X), X) -> X % 28.47/27.40 1094: ifeq3(theme(skc12, skf1(skc10), X), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), Y), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, X), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), Y, X), X), X), X), X), X) -> X % 28.47/27.40 1095: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc10), Z), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc10), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc10)), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 1096: ifeq3(theme(skc12, X, Y), abstraction(skc8, skc14), ifeq3(theme(skc12, skf1(skc15), Z), abstraction(skc8, skc14), ifeq3(agent(skc12, X, skc15), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, X), abstraction(skc8, skc14), ifeq3(think_believe_consider(skc12, skf1(skc15)), abstraction(skc8, skc14), ifeq3(proposition(skc12, Y), abstraction(skc8, skc14), ifeq3(proposition(skc12, Z), abstraction(skc8, skc14), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 28.47/27.40 %------------------------------------------------------------------------------