%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP225-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jul 15 07:23:58 AM UTC 2025 % Result : Satisfiable 16.60s 15.78s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP225-10 : TPTP v9.0.0. Released v7.3.0. % 0.06/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.33 % Computer : n004.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Jul 14 14:21:04 EDT 2025 % 0.12/0.33 % CPUTime : % 16.60/15.78 % SZS status Satisfiable % 16.60/15.78 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 16.60/15.78 1: actual_world(skc8) -> true % 16.60/15.78 2: jules_forename(skc8, skc15) -> true % 16.60/15.78 3: forename(skc8, skc15) -> true % 16.60/15.78 4: man(skc8, skc14) -> true % 16.60/15.78 5: vincent_forename(skc8, skc13) -> true % 16.60/15.78 6: forename(skc8, skc13) -> true % 16.60/15.78 7: think_believe_consider(skc8, skc12) -> true % 16.60/15.78 8: present(skc8, skc12) -> true % 16.60/15.78 9: event(skc8, skc12) -> true % 16.60/15.78 10: proposition(skc8, skc11) -> true % 16.60/15.78 11: accessible_world(skc8, skc11) -> true % 16.60/15.78 12: man(skc8, skc10) -> true % 16.60/15.78 13: state(skc8, skc9) -> true % 16.60/15.78 14: of(skc8, skc15, skc14) -> true % 16.60/15.78 15: agent(skc8, skc12, skc14) -> true % 16.60/15.78 16: of(skc8, skc13, skc14) -> true % 16.60/15.78 17: theme(skc8, skc12, skc11) -> true % 16.60/15.78 18: ifeq3(X, X, Y, Z) -> Y % 16.60/15.78 19: ifeq(X, X, Y, Z) -> Y % 16.60/15.78 20: ifeq2(X, X, Y, Z) -> Y % 16.60/15.78 21: be(skc8, skc9, skc14, skc10) -> true % 16.60/15.78 22: ifeq3(be(X, Y, Z, W), true, Z, W) -> W % 16.60/15.78 23: skc10 -> skc14 % 16.60/15.78 24: be(skc8, skc9, skc14, skc14) -> true % 16.60/15.78 25: ifeq2(abstraction(X, Y), true, thing(X, Y), true) -> true % 16.60/15.78 26: ifeq2(state(X, Y), true, event(X, Y), true) -> true % 16.60/15.78 27: event(skc8, skc9) -> true % 16.60/15.78 28: ifeq2(state(skc8, skc12), true, true, true) -> true % 16.60/15.78 29: ifeq2(eventuality(X, Y), true, unisex(X, Y), true) -> true % 16.60/15.78 30: ifeq2(abstraction(X, Y), true, unisex(X, Y), true) -> true % 16.60/15.78 31: ifeq2(abstraction(X, Y), true, general(X, Y), true) -> true % 16.60/15.78 32: ifeq2(abstraction(X, Y), true, nonhuman(X, Y), true) -> true % 16.60/15.78 33: ifeq2(jules_forename(X, Y), true, forename(X, Y), true) -> true % 16.60/15.78 34: ifeq2(jules_forename(skc8, skc13), true, true, true) -> true % 16.60/15.78 35: ifeq2(proposition(X, Y), true, relation(X, Y), true) -> true % 16.60/15.78 36: true -> relation(skc8, skc11) % 16.60/15.78 38: ifeq2(smoke(X, Y), relation(skc8, skc11), event(X, Y), relation(skc8, skc11)) -> relation(skc8, skc11) % 16.60/15.78 40: ifeq2(vincent_forename(X, Y), relation(skc8, skc11), forename(X, Y), relation(skc8, skc11)) -> relation(skc8, skc11) % 16.60/15.78 42: ifeq2(organism(X, Y), relation(skc8, skc11), entity(X, Y), relation(skc8, skc11)) -> relation(skc8, skc11) % 16.60/15.78 44: ifeq2(event(X, Y), relation(skc8, skc11), eventuality(X, Y), relation(skc8, skc11)) -> relation(skc8, skc11) % 16.60/15.78 45: eventuality(skc8, skc12) -> relation(skc8, skc11) % 16.60/15.78 46: relation(skc8, skc11) -> unisex(skc8, skc12) % 16.60/15.78 47: eventuality(skc8, skc9) -> unisex(skc8, skc12) % 16.60/15.78 48: unisex(skc8, skc9) -> unisex(skc8, skc12) % 16.60/15.78 50: ifeq2(entity(X, Y), unisex(skc8, skc12), thing(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 52: ifeq2(man(X, Y), unisex(skc8, skc12), human_person(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 53: human_person(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 55: ifeq2(human_person(X, Y), unisex(skc8, skc12), organism(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 56: organism(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 57: entity(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 58: thing(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 60: ifeq2(entity(X, Y), unisex(skc8, skc12), existent(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 61: existent(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 63: ifeq2(entity(X, Y), unisex(skc8, skc12), specific(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 64: specific(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 66: ifeq2(organism(X, Y), unisex(skc8, skc12), impartial(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 67: impartial(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 69: ifeq2(human_person(X, Y), unisex(skc8, skc12), animate(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 70: animate(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 72: ifeq2(human_person(X, Y), unisex(skc8, skc12), human(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 73: human(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 75: ifeq2(organism(X, Y), unisex(skc8, skc12), living(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 76: living(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 78: ifeq2(man(X, Y), unisex(skc8, skc12), male(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 79: male(skc8, skc14) -> unisex(skc8, skc12) % 16.60/15.78 81: ifeq2(relname(X, Y), unisex(skc8, skc12), relation(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 83: ifeq2(forename(X, Y), unisex(skc8, skc12), relname(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 84: relname(skc8, skc13) -> unisex(skc8, skc12) % 16.60/15.78 85: relname(skc8, skc15) -> unisex(skc8, skc12) % 16.60/15.78 86: relation(skc8, skc15) -> unisex(skc8, skc12) % 16.60/15.78 87: relation(skc8, skc13) -> unisex(skc8, skc12) % 16.60/15.78 89: ifeq2(relation(X, Y), unisex(skc8, skc12), abstraction(X, Y), unisex(skc8, skc12)) -> unisex(skc8, skc12) % 16.60/15.78 90: abstraction(skc8, skc11) -> unisex(skc8, skc12) % 16.60/15.78 91: abstraction(skc8, skc13) -> unisex(skc8, skc12) % 16.60/15.78 92: abstraction(skc8, skc15) -> unisex(skc8, skc12) % 16.60/15.78 93: nonhuman(skc8, skc15) -> unisex(skc8, skc12) % 16.60/15.78 94: general(skc8, skc15) -> unisex(skc8, skc12) % 16.60/15.78 95: unisex(skc8, skc15) -> unisex(skc8, skc12) % 16.60/15.78 96: thing(skc8, skc15) -> unisex(skc8, skc12) % 16.60/15.78 97: nonhuman(skc8, skc13) -> unisex(skc8, skc12) % 16.60/15.78 98: general(skc8, skc13) -> unisex(skc8, skc12) % 16.60/15.78 99: thing(skc8, skc13) -> unisex(skc8, skc12) % 16.60/15.78 100: unisex(skc8, skc13) -> unisex(skc8, skc12) % 16.60/15.78 101: unisex(skc8, skc11) -> unisex(skc8, skc12) % 16.60/15.78 102: thing(skc8, skc11) -> unisex(skc8, skc12) % 16.60/15.78 103: unisex(skc8, skc12) -> nonhuman(skc8, skc11) % 16.60/15.78 104: general(skc8, skc11) -> nonhuman(skc8, skc11) % 16.60/15.78 106: ifeq2(state(X, Y), nonhuman(skc8, skc11), eventuality(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 108: ifeq2(eventuality(X, Y), nonhuman(skc8, skc11), thing(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 109: thing(skc8, skc12) -> nonhuman(skc8, skc11) % 16.60/15.78 110: thing(skc8, skc9) -> nonhuman(skc8, skc11) % 16.60/15.78 112: ifeq2(eventuality(X, Y), nonhuman(skc8, skc11), specific(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 113: specific(skc8, skc12) -> nonhuman(skc8, skc11) % 16.60/15.78 114: specific(skc8, skc9) -> nonhuman(skc8, skc11) % 16.60/15.78 116: ifeq2(thing(X, Y), nonhuman(skc8, skc11), singleton(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 117: singleton(skc8, skc12) -> nonhuman(skc8, skc11) % 16.60/15.78 118: singleton(skc8, skc9) -> nonhuman(skc8, skc11) % 16.60/15.78 119: singleton(skc8, skc11) -> nonhuman(skc8, skc11) % 16.60/15.78 120: singleton(skc8, skc13) -> nonhuman(skc8, skc11) % 16.60/15.78 121: singleton(skc8, skc15) -> nonhuman(skc8, skc11) % 16.60/15.78 122: singleton(skc8, skc14) -> nonhuman(skc8, skc11) % 16.60/15.78 124: ifeq2(eventuality(X, Y), nonhuman(skc8, skc11), nonexistent(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 125: nonexistent(skc8, skc12) -> nonhuman(skc8, skc11) % 16.60/15.78 126: nonexistent(skc8, skc9) -> nonhuman(skc8, skc11) % 16.60/15.78 128: ifeq2(man(skc11, X), nonhuman(skc8, skc11), smoke(skc11, skf1(Y)), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 130: ifeq2(man(skc11, X), nonhuman(skc8, skc11), present(skc11, skf1(Y)), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 132: ifeq2(man(skc11, X), nonhuman(skc8, skc11), event(skc11, skf1(Y)), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 134: ifeq2(man(skc11, X), nonhuman(skc8, skc11), agent(skc11, skf1(X), X), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 135: ifeq3(be(X, Y, Z, W), nonhuman(skc8, skc11), Z, W) -> W % 16.60/15.78 137: ifeq(tuple(unisex(X, Y), male(X, Y)), tuple(nonhuman(skc8, skc11), nonhuman(skc8, skc11)), a, b) -> b % 16.60/15.78 139: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(nonhuman(skc8, skc11), nonhuman(skc8, skc11)), a, b) -> b % 16.60/15.78 141: ifeq(tuple(human(X, Y), nonhuman(X, Y)), tuple(nonhuman(skc8, skc11), nonhuman(skc8, skc11)), a, b) -> b % 16.60/15.78 143: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(nonhuman(skc8, skc11), nonhuman(skc8, skc11)), a, b) -> b % 16.60/15.78 144: ifeq2(state(X, Y), nonhuman(skc8, skc11), event(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 145: ifeq2(abstraction(X, Y), nonhuman(skc8, skc11), thing(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 146: ifeq2(smoke(skc8, skc12), nonhuman(skc8, skc11), nonhuman(skc8, skc11), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 147: ifeq2(jules_forename(X, Y), nonhuman(skc8, skc11), forename(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 148: ifeq2(proposition(X, Y), nonhuman(skc8, skc11), relation(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 149: ifeq2(abstraction(X, Y), nonhuman(skc8, skc11), nonhuman(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 150: ifeq2(abstraction(X, Y), nonhuman(skc8, skc11), general(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 151: ifeq2(abstraction(X, Y), nonhuman(skc8, skc11), unisex(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 152: ifeq2(eventuality(X, Y), nonhuman(skc8, skc11), unisex(X, Y), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 153: ifeq2(vincent_forename(skc8, skc15), nonhuman(skc8, skc11), nonhuman(skc8, skc11), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 155: ifeq2(accessible_world(X, Y), nonhuman(skc8, skc11), ifeq2(eventuality(X, Z), nonhuman(skc8, skc11), eventuality(Y, Z), nonhuman(skc8, skc11)), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 156: ifeq2(eventuality(skc8, X), nonhuman(skc8, skc11), eventuality(skc11, X), nonhuman(skc8, skc11)) -> nonhuman(skc8, skc11) % 16.60/15.78 157: nonhuman(skc8, skc11) -> eventuality(skc11, skc12) % 16.60/15.78 158: eventuality(skc11, skc9) -> eventuality(skc11, skc12) % 16.60/15.78 159: unisex(skc11, skc9) -> eventuality(skc11, skc12) % 16.60/15.78 160: nonexistent(skc11, skc9) -> eventuality(skc11, skc12) % 16.60/15.78 161: specific(skc11, skc9) -> eventuality(skc11, skc12) % 16.60/15.78 162: thing(skc11, skc9) -> eventuality(skc11, skc12) % 16.60/15.78 163: singleton(skc11, skc9) -> eventuality(skc11, skc12) % 16.60/15.78 164: ifeq3(be(X, Y, Z, W), eventuality(skc11, skc12), Z, W) -> W % 16.60/15.78 166: ifeq2(accessible_world(X, Y), eventuality(skc11, skc12), ifeq2(state(X, Z), eventuality(skc11, skc12), state(Y, Z), eventuality(skc11, skc12)), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 167: ifeq2(state(skc8, X), eventuality(skc11, skc12), state(skc11, X), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 168: state(skc11, skc9) -> eventuality(skc11, skc12) % 16.60/15.78 169: event(skc11, skc9) -> eventuality(skc11, skc12) % 16.60/15.78 170: ifeq2(accessible_world(skc8, X), eventuality(skc11, skc12), state(X, skc9), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 172: ifeq2(accessible_world(X, Y), eventuality(skc11, skc12), ifeq2(thing(X, Z), eventuality(skc11, skc12), thing(Y, Z), eventuality(skc11, skc12)), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 173: ifeq2(thing(skc8, X), eventuality(skc11, skc12), thing(skc11, X), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 174: thing(skc11, skc12) -> eventuality(skc11, skc12) % 16.60/15.78 175: singleton(skc11, skc12) -> eventuality(skc11, skc12) % 16.60/15.78 176: thing(skc11, skc11) -> eventuality(skc11, skc12) % 16.60/15.78 177: thing(skc11, skc13) -> eventuality(skc11, skc12) % 16.60/15.78 178: thing(skc11, skc14) -> eventuality(skc11, skc12) % 16.60/15.78 179: thing(skc11, skc15) -> eventuality(skc11, skc12) % 16.60/15.78 180: singleton(skc11, skc15) -> eventuality(skc11, skc12) % 16.60/15.78 181: singleton(skc11, skc14) -> eventuality(skc11, skc12) % 16.60/15.78 182: singleton(skc11, skc13) -> eventuality(skc11, skc12) % 16.60/15.78 183: singleton(skc11, skc11) -> eventuality(skc11, skc12) % 16.60/15.78 185: ifeq2(accessible_world(X, Y), eventuality(skc11, skc12), ifeq2(specific(X, Z), eventuality(skc11, skc12), specific(Y, Z), eventuality(skc11, skc12)), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 186: ifeq2(specific(skc8, X), eventuality(skc11, skc12), specific(skc11, X), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 187: specific(skc11, skc12) -> eventuality(skc11, skc12) % 16.60/15.78 188: specific(skc11, skc14) -> eventuality(skc11, skc12) % 16.60/15.78 190: ifeq2(accessible_world(X, Y), eventuality(skc11, skc12), ifeq2(singleton(X, Z), eventuality(skc11, skc12), singleton(Y, Z), eventuality(skc11, skc12)), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 191: ifeq2(singleton(skc8, X), eventuality(skc11, skc12), singleton(skc11, X), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 193: ifeq2(accessible_world(X, Y), eventuality(skc11, skc12), ifeq2(nonexistent(X, Z), eventuality(skc11, skc12), nonexistent(Y, Z), eventuality(skc11, skc12)), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 194: ifeq2(nonexistent(skc8, X), eventuality(skc11, skc12), nonexistent(skc11, X), eventuality(skc11, skc12)) -> eventuality(skc11, skc12) % 16.60/15.78 195: eventuality(skc11, skc12) -> nonexistent(skc11, skc12) % 16.60/15.78 196: nonexistent(skc11, skc12) -> unisex(skc11, skc12) % 16.60/15.78 197: ifeq3(be(X, Y, Z, W), unisex(skc11, skc12), Z, W) -> W % 16.60/15.78 199: ifeq2(accessible_world(X, Y), unisex(skc11, skc12), ifeq2(unisex(X, Z), unisex(skc11, skc12), unisex(Y, Z), unisex(skc11, skc12)), unisex(skc11, skc12)) -> unisex(skc11, skc12) % 16.60/15.78 200: ifeq2(unisex(skc8, X), unisex(skc11, skc12), unisex(skc11, X), unisex(skc11, skc12)) -> unisex(skc11, skc12) % 16.60/15.78 201: unisex(skc11, skc11) -> unisex(skc11, skc12) % 16.60/15.78 202: unisex(skc11, skc13) -> unisex(skc11, skc12) % 16.60/15.78 203: unisex(skc11, skc15) -> unisex(skc11, skc12) % 16.60/15.78 204: ifeq2(accessible_world(skc11, X), unisex(skc11, skc12), unisex(X, skc12), unisex(skc11, skc12)) -> unisex(skc11, skc12) % 16.60/15.78 206: ifeq2(accessible_world(X, Y), unisex(skc11, skc12), ifeq2(nonhuman(X, Z), unisex(skc11, skc12), nonhuman(Y, Z), unisex(skc11, skc12)), unisex(skc11, skc12)) -> unisex(skc11, skc12) % 16.60/15.78 207: ifeq2(nonhuman(skc8, X), unisex(skc11, skc12), nonhuman(skc11, X), unisex(skc11, skc12)) -> unisex(skc11, skc12) % 16.60/15.78 208: unisex(skc11, skc12) -> nonhuman(skc11, skc11) % 16.60/15.78 209: nonhuman(skc11, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 210: nonhuman(skc11, skc15) -> nonhuman(skc11, skc11) % 16.60/15.78 211: ifeq3(be(X, Y, Z, W), nonhuman(skc11, skc11), Z, W) -> W % 16.60/15.78 213: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(smoke(X, Z), nonhuman(skc11, skc11), smoke(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 214: ifeq2(smoke(skc8, X), nonhuman(skc11, skc11), smoke(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 216: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(general(X, Z), nonhuman(skc11, skc11), general(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 217: ifeq2(general(skc8, X), nonhuman(skc11, skc11), general(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 218: general(skc11, skc11) -> nonhuman(skc11, skc11) % 16.60/15.78 219: general(skc11, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 220: general(skc11, skc15) -> nonhuman(skc11, skc11) % 16.60/15.78 222: ifeq2(present(X, Y), nonhuman(skc11, skc11), ifeq2(accessible_world(X, Z), nonhuman(skc11, skc11), present(Z, Y), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 223: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), present(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 224: present(skc11, skc12) -> nonhuman(skc11, skc11) % 16.60/15.78 225: ifeq2(present(skc8, X), nonhuman(skc11, skc11), present(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 227: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(jules_forename(X, Z), nonhuman(skc11, skc11), jules_forename(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 228: ifeq2(jules_forename(skc8, X), nonhuman(skc11, skc11), jules_forename(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 229: jules_forename(skc11, skc15) -> nonhuman(skc11, skc11) % 16.60/15.78 230: forename(skc11, skc15) -> nonhuman(skc11, skc11) % 16.60/15.78 231: relname(skc11, skc15) -> nonhuman(skc11, skc11) % 16.60/15.78 232: relation(skc11, skc15) -> nonhuman(skc11, skc11) % 16.60/15.78 233: abstraction(skc11, skc15) -> nonhuman(skc11, skc11) % 16.60/15.78 234: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), jules_forename(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 236: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(proposition(X, Z), nonhuman(skc11, skc11), proposition(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 237: ifeq2(proposition(skc8, X), nonhuman(skc11, skc11), proposition(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 238: proposition(skc11, skc11) -> nonhuman(skc11, skc11) % 16.60/15.78 239: relation(skc11, skc11) -> nonhuman(skc11, skc11) % 16.60/15.78 240: abstraction(skc11, skc11) -> nonhuman(skc11, skc11) % 16.60/15.78 241: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), proposition(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 243: ifeq2(think_believe_consider(X, Y), nonhuman(skc11, skc11), ifeq2(accessible_world(X, Z), nonhuman(skc11, skc11), think_believe_consider(Z, Y), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 244: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), think_believe_consider(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 245: think_believe_consider(skc11, skc12) -> nonhuman(skc11, skc11) % 16.60/15.78 246: ifeq2(think_believe_consider(skc8, X), nonhuman(skc11, skc11), think_believe_consider(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 248: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(vincent_forename(X, Z), nonhuman(skc11, skc11), vincent_forename(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 249: ifeq2(vincent_forename(skc8, X), nonhuman(skc11, skc11), vincent_forename(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 250: vincent_forename(skc11, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 251: forename(skc11, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 252: relname(skc11, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 253: relation(skc11, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 254: abstraction(skc11, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 255: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), vincent_forename(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 257: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(organism(X, Z), nonhuman(skc11, skc11), organism(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 258: ifeq2(organism(skc8, X), nonhuman(skc11, skc11), organism(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 259: organism(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 260: living(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 261: impartial(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 262: entity(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 263: existent(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 265: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(man(X, Z), nonhuman(skc11, skc11), man(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 266: ifeq2(man(skc8, X), nonhuman(skc11, skc11), man(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 267: man(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 268: human_person(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 269: male(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 270: human(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 271: animate(skc11, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 272: present(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 273: smoke(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 274: event(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 275: eventuality(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 276: thing(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 277: specific(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 278: nonexistent(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 279: unisex(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 280: agent(skc11, skf1(skc14), skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 281: singleton(skc11, skf1(X)) -> nonhuman(skc11, skc11) % 16.60/15.78 282: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), man(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 284: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(human_person(X, Z), nonhuman(skc11, skc11), human_person(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 285: ifeq2(human_person(skc8, X), nonhuman(skc11, skc11), human_person(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 287: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(event(X, Z), nonhuman(skc11, skc11), event(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 288: ifeq2(event(skc8, X), nonhuman(skc11, skc11), event(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 289: event(skc11, skc12) -> nonhuman(skc11, skc11) % 16.60/15.78 290: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), event(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 292: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(entity(X, Z), nonhuman(skc11, skc11), entity(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 293: ifeq2(entity(skc8, X), nonhuman(skc11, skc11), entity(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 295: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(impartial(X, Z), nonhuman(skc11, skc11), impartial(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 296: ifeq2(impartial(skc8, X), nonhuman(skc11, skc11), impartial(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 298: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(existent(X, Z), nonhuman(skc11, skc11), existent(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 299: ifeq2(existent(skc8, X), nonhuman(skc11, skc11), existent(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 301: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(living(X, Z), nonhuman(skc11, skc11), living(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 302: ifeq2(living(skc8, X), nonhuman(skc11, skc11), living(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 304: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(male(X, Z), nonhuman(skc11, skc11), male(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 305: ifeq2(male(skc8, X), nonhuman(skc11, skc11), male(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 307: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(human(X, Z), nonhuman(skc11, skc11), human(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 308: ifeq2(human(skc8, X), nonhuman(skc11, skc11), human(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 310: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(forename(X, Z), nonhuman(skc11, skc11), forename(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 311: ifeq2(forename(skc8, X), nonhuman(skc11, skc11), forename(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 312: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), forename(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 313: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), forename(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 315: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(animate(X, Z), nonhuman(skc11, skc11), animate(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 316: ifeq2(animate(skc8, X), nonhuman(skc11, skc11), animate(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 318: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(relation(X, Z), nonhuman(skc11, skc11), relation(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 319: ifeq2(relation(skc8, X), nonhuman(skc11, skc11), relation(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 321: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(relname(X, Z), nonhuman(skc11, skc11), relname(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 322: ifeq2(relname(skc8, X), nonhuman(skc11, skc11), relname(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 324: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(abstraction(X, Z), nonhuman(skc11, skc11), abstraction(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 325: ifeq2(abstraction(skc8, X), nonhuman(skc11, skc11), abstraction(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 326: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), relname(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 327: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), relname(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 328: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), male(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 329: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), human_person(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 330: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), event(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 331: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), eventuality(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 332: ifeq2(accessible_world(skc8, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 333: ifeq2(eventuality(X, Y), nonhuman(skc11, skc11), specific(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 334: ifeq2(state(X, Y), nonhuman(skc11, skc11), eventuality(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 335: ifeq2(abstraction(X, Y), nonhuman(skc11, skc11), general(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 336: ifeq2(abstraction(X, Y), nonhuman(skc11, skc11), unisex(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 337: ifeq2(abstraction(X, Y), nonhuman(skc11, skc11), nonhuman(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 338: ifeq2(proposition(X, Y), nonhuman(skc11, skc11), relation(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 339: ifeq2(jules_forename(X, Y), nonhuman(skc11, skc11), forename(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 340: ifeq2(abstraction(X, Y), nonhuman(skc11, skc11), thing(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 341: ifeq2(state(X, Y), nonhuman(skc11, skc11), event(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 342: ifeq2(eventuality(X, Y), nonhuman(skc11, skc11), unisex(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 343: ifeq2(state(skc8, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 344: ifeq2(jules_forename(skc8, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 345: ifeq2(smoke(skc8, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 346: ifeq2(vincent_forename(X, Y), nonhuman(skc11, skc11), forename(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 347: ifeq2(organism(X, Y), nonhuman(skc11, skc11), entity(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 348: ifeq2(event(X, Y), nonhuman(skc11, skc11), eventuality(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 349: ifeq2(smoke(X, Y), nonhuman(skc11, skc11), event(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 350: ifeq2(eventuality(X, Y), nonhuman(skc11, skc11), thing(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 351: ifeq2(eventuality(X, Y), nonhuman(skc11, skc11), nonexistent(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 352: ifeq2(thing(X, Y), nonhuman(skc11, skc11), singleton(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 353: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), organism(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 354: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), think_believe_consider(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 355: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), vincent_forename(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 356: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), human(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 357: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), animate(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 358: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), relation(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 359: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), relation(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 360: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), relation(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 361: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), man(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 362: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), thing(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 363: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), nonexistent(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 364: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), specific(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 365: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), event(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 366: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), state(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 367: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), eventuality(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 368: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), nonhuman(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 369: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), proposition(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 370: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), jules_forename(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 371: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), present(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 372: ifeq2(eventuality(skc8, X), nonhuman(skc11, skc11), eventuality(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 373: ifeq2(vincent_forename(skc8, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 374: ifeq2(entity(skc8, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 375: ifeq2(abstraction(skc8, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 376: ifeq2(state(skc11, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 377: ifeq2(smoke(skc11, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 378: ifeq2(proposition(skc8, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 379: ifeq2(proposition(skc8, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 380: ifeq2(relname(skc8, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 381: ifeq2(smoke(skc8, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 382: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), event(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 383: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), eventuality(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 384: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), relation(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 385: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), eventuality(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 386: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), state(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 387: ifeq2(state(skc8, X), nonhuman(skc11, skc11), state(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 388: ifeq2(nonexistent(skc8, X), nonhuman(skc11, skc11), nonexistent(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 389: ifeq2(specific(skc8, X), nonhuman(skc11, skc11), specific(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 390: ifeq2(singleton(skc8, X), nonhuman(skc11, skc11), singleton(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 391: ifeq2(thing(skc8, X), nonhuman(skc11, skc11), thing(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 392: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), nonexistent(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 393: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), thing(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 394: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), specific(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 395: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), specific(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 396: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), thing(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 397: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), human_person(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 398: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), unisex(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 399: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), male(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 400: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), entity(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 401: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), forename(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 402: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), unisex(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 403: ifeq2(unisex(skc8, X), nonhuman(skc11, skc11), unisex(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 404: ifeq2(nonhuman(skc8, X), nonhuman(skc11, skc11), nonhuman(skc11, X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 405: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), abstraction(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 406: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), abstraction(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 407: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), abstraction(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 408: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), living(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 409: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), impartial(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 410: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), forename(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 411: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), singleton(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 412: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), organism(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 413: ifeq2(man(skc11, X), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 414: ifeq2(accessible_world(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 415: ifeq2(jules_forename(skc11, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 416: ifeq2(abstraction(skc8, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 417: ifeq2(abstraction(skc11, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 418: ifeq2(entity(skc11, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 419: ifeq2(accessible_world(skc11, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 420: ifeq2(forename(X, Y), nonhuman(skc11, skc11), relname(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 421: ifeq2(relation(X, Y), nonhuman(skc11, skc11), abstraction(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 422: ifeq2(relname(X, Y), nonhuman(skc11, skc11), relation(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 423: ifeq2(man(X, Y), nonhuman(skc11, skc11), male(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 424: ifeq2(human_person(X, Y), nonhuman(skc11, skc11), human(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 425: ifeq2(organism(X, Y), nonhuman(skc11, skc11), living(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 426: ifeq2(human_person(X, Y), nonhuman(skc11, skc11), animate(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 427: ifeq2(organism(X, Y), nonhuman(skc11, skc11), impartial(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 428: ifeq2(entity(X, Y), nonhuman(skc11, skc11), existent(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 429: ifeq2(entity(X, Y), nonhuman(skc11, skc11), specific(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 430: ifeq2(human_person(X, Y), nonhuman(skc11, skc11), organism(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 431: ifeq2(man(X, Y), nonhuman(skc11, skc11), human_person(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 432: ifeq2(vincent_forename(skc11, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 433: ifeq2(relname(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 434: ifeq2(entity(X, Y), nonhuman(skc11, skc11), thing(X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 435: ifeq2(entity(skc8, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 436: ifeq2(smoke(skc11, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 438: ifeq2(of(X, Y, Z), nonhuman(skc11, skc11), ifeq2(accessible_world(X, W), nonhuman(skc11, skc11), of(W, Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 439: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), of(X, skc13, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 440: of(skc11, skc13, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 441: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), of(X, skc15, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 442: of(skc11, skc15, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 443: ifeq2(of(skc8, X, Y), nonhuman(skc11, skc11), of(skc11, X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 445: ifeq2(theme(X, Y, Z), nonhuman(skc11, skc11), ifeq2(accessible_world(X, W), nonhuman(skc11, skc11), theme(W, Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 446: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), theme(X, skc12, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 447: theme(skc11, skc12, skc11) -> nonhuman(skc11, skc11) % 16.60/15.78 448: ifeq2(theme(skc8, X, Y), nonhuman(skc11, skc11), theme(skc11, X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 450: ifeq2(agent(X, Y, Z), nonhuman(skc11, skc11), ifeq2(accessible_world(X, W), nonhuman(skc11, skc11), agent(W, Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 451: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), agent(X, skc12, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 452: agent(skc11, skc12, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 453: ifeq2(agent(skc8, X, Y), nonhuman(skc11, skc11), agent(skc11, X, Y), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 454: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), agent(X, skc12, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 455: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), theme(X, skc12, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 456: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), of(X, skc13, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 457: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), of(X, skc15, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 458: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), singleton(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 459: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), nonhuman(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 460: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), impartial(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 461: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), singleton(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 462: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), nonexistent(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 463: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), general(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 464: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), general(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 465: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), general(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 466: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), thing(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 467: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), thing(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 468: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), nonhuman(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 469: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), specific(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 470: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), animate(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 471: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), existent(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 472: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), entity(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 473: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), unisex(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 474: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), unisex(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 475: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), unisex(X, skc12), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 476: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), unisex(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 477: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), unisex(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 478: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), human(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 479: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), living(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 480: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), relname(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 481: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), relname(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 482: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), abstraction(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 483: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), specific(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 484: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), thing(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 485: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), thing(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 486: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), thing(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 487: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), nonexistent(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 488: ifeq2(abstraction(skc8, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 489: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), event(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 490: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), present(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 491: ifeq2(abstraction(skc11, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 492: ifeq2(entity(skc11, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 493: ifeq2(eventuality(skc8, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 494: ifeq2(eventuality(skc8, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 495: ifeq2(eventuality(skc8, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 496: ifeq2(eventuality(skc8, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 497: ifeq2(entity(skc8, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 498: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), smoke(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 499: ifeq2(entity(skc8, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 500: ifeq2(entity(skc8, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 501: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), relation(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 502: ifeq2(state(skc11, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 503: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), relation(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 504: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), general(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 505: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), general(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 506: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), general(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 507: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), singleton(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 508: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), singleton(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 509: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), singleton(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 510: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), singleton(X, skc9), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 511: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), singleton(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 512: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), existent(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 513: ifeq2(present(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 514: ifeq2(smoke(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 515: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), nonhuman(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 516: ifeq2(event(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 517: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), thing(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 518: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), thing(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 519: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), nonhuman(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 520: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), unisex(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 521: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), unisex(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 522: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), unisex(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 523: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), specific(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 524: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), thing(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 525: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), thing(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 526: ifeq2(man(skc11, X), nonhuman(skc11, skc11), agent(skc11, skf1(X), X), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 527: ifeq2(eventuality(skc11, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 528: ifeq2(proposition(skc11, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 529: ifeq2(abstraction(skc11, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 530: ifeq2(entity(skc11, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 531: ifeq2(entity(skc11, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 532: ifeq2(eventuality(skc11, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 533: ifeq2(eventuality(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 534: ifeq2(entity(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 535: ifeq2(eventuality(skc11, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 536: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), eventuality(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 537: ifeq2(proposition(skc11, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 538: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), singleton(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 539: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), singleton(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 540: ifeq2(eventuality(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 541: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), singleton(X, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 542: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), abstraction(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 543: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), abstraction(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 544: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), singleton(X, skc15), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 545: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), nonexistent(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 546: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), thing(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 547: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), specific(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 548: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), unisex(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 549: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), agent(X, skf1(skc14), skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 551: ifeq2(be(X, Y, Z, W), nonhuman(skc11, skc11), ifeq2(accessible_world(X, V), nonhuman(skc11, skc11), be(V, Y, Z, W), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 552: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), be(X, skc9, skc14, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 553: be(skc11, skc9, skc14, skc14) -> nonhuman(skc11, skc11) % 16.60/15.78 554: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), be(X, skc9, skc14, skc14), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 555: ifeq2(be(skc8, X, Y, Z), nonhuman(skc11, skc11), be(skc11, X, Y, Z), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 556: ifeq2(agent(skc8, skf1(skc14), skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 557: ifeq2(entity(skc11, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 558: ifeq2(abstraction(skc11, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 559: ifeq2(specific(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 560: ifeq2(unisex(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 561: ifeq2(thing(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 562: ifeq2(nonexistent(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 563: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), singleton(X, skf1(Y)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 564: ifeq(tuple(human(X, Y), nonhuman(X, Y)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 565: ifeq(tuple(nonexistent(X, Y), existent(X, Y)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 566: ifeq(tuple(specific(X, Y), general(X, Y)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 567: ifeq(tuple(unisex(X, Y), male(X, Y)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 568: ifeq(tuple(unisex(skc8, skc14), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 569: ifeq2(singleton(skc8, skf1(X)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 570: ifeq(tuple(nonhuman(skc11, skc11), existent(skc8, skc12)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 571: ifeq(tuple(human(skc8, skc11), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 572: ifeq(tuple(nonhuman(skc11, skc11), general(skc8, skc12)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 573: ifeq(tuple(nonhuman(skc11, skc11), nonhuman(skc8, skc14)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 574: ifeq(tuple(nonhuman(skc11, skc11), existent(skc8, skc9)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 575: ifeq(tuple(nonhuman(skc11, skc11), general(skc11, skc12)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 576: ifeq(tuple(nonhuman(skc11, skc11), general(skc8, skc9)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 577: ifeq(tuple(nonhuman(skc11, skc11), male(skc11, skc12)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 578: ifeq(tuple(nonhuman(skc11, skc11), male(skc8, skc9)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 579: ifeq(tuple(unisex(skc11, skc14), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 580: ifeq(tuple(nonhuman(skc11, skc11), general(skc8, skc14)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 581: ifeq(tuple(nonhuman(skc11, skc11), existent(skc11, skc9)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 582: ifeq(tuple(nonhuman(skc11, skc11), general(skc11, skc9)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 583: ifeq(tuple(human(skc8, skc13), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 584: ifeq(tuple(nonexistent(skc8, skc14), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 585: ifeq(tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc14)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 586: ifeq(tuple(specific(skc8, skc13), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 587: ifeq(tuple(specific(skc8, skc11), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 588: ifeq(tuple(specific(skc8, skc15), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 589: ifeq(tuple(human(skc8, skc15), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 590: ifeq(tuple(nonhuman(skc11, skc11), male(skc8, skc15)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 591: ifeq(tuple(nonhuman(skc11, skc11), male(skc8, skc13)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 592: ifeq(tuple(nonhuman(skc11, skc11), male(skc11, skc9)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 593: ifeq(tuple(nonhuman(skc11, skc11), male(skc8, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 594: ifeq(tuple(nonhuman(skc11, skc11), male(skc8, skc12)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 595: ifeq(tuple(nonhuman(skc11, skc11), existent(skc11, skc12)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 596: ifeq(tuple(specific(skc11, skc15), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 597: ifeq(tuple(human(skc11, skc13), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 598: ifeq(tuple(human(skc11, skc15), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 599: ifeq(tuple(nonhuman(skc11, skc11), male(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 600: ifeq(tuple(nonhuman(skc11, skc11), male(skc11, skc13)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 601: ifeq(tuple(specific(skc11, skc11), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 602: ifeq(tuple(specific(skc11, skc13), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 603: ifeq(tuple(nonexistent(skc11, skc14), nonhuman(skc11, skc11)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 604: ifeq(tuple(nonhuman(skc11, skc11), male(skc11, skc15)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 605: ifeq(tuple(nonhuman(skc11, skc11), general(skc11, skc14)), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 606: ifeq(tuple(nonhuman(skc11, skc11), general(skc11, skf1(X))), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 607: ifeq(tuple(nonhuman(skc11, skc11), male(skc11, skf1(X))), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 608: ifeq(tuple(nonhuman(skc11, skc11), existent(skc11, skf1(X))), tuple(nonhuman(skc11, skc11), nonhuman(skc11, skc11)), a, b) -> b % 16.60/15.78 609: ifeq2(present(X, skc12), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 610: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(man(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 611: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(vincent_forename(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 612: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(state(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 613: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(proposition(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 614: ifeq2(think_believe_consider(X, skc12), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 615: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(jules_forename(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 616: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(event(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 617: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(forename(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 618: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(forename(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 619: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(eventuality(X, Z), nonhuman(skc11, skc11), eventuality(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 620: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(eventuality(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 621: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(event(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 622: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(human_person(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 623: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(relname(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 624: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(relname(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 625: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(male(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 626: ifeq2(agent(X, skc12, skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 627: ifeq2(of(X, skc15, skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 628: ifeq2(theme(X, skc12, skc11), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 629: ifeq2(of(X, skc13, skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 630: ifeq2(present(X, skc12), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 631: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(state(X, Z), nonhuman(skc11, skc11), state(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 632: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(jules_forename(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 633: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(specific(X, Z), nonhuman(skc11, skc11), specific(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 634: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(unisex(X, Z), nonhuman(skc11, skc11), unisex(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 635: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(nonhuman(X, Z), nonhuman(skc11, skc11), nonhuman(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 636: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), nonhuman(X, skc11), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 637: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(man(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 638: ifeq2(think_believe_consider(X, skc12), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 639: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(nonexistent(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 640: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(thing(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 641: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(event(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 642: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(human(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 643: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(thing(X, Z), nonhuman(skc11, skc11), thing(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 644: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(nonexistent(X, Z), nonhuman(skc11, skc11), nonexistent(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 645: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(vincent_forename(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 646: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(proposition(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 647: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(specific(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 648: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(relation(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 649: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(relation(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 650: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(animate(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 651: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(relation(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 652: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(eventuality(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 653: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(organism(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 654: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(state(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 655: ifeq2(accessible_world(X, Y), nonhuman(skc11, skc11), ifeq2(singleton(X, Z), nonhuman(skc11, skc11), singleton(Y, Z), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 656: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(nonhuman(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 657: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(forename(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 658: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(eventuality(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 659: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(unisex(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 660: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(eventuality(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 661: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(forename(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 662: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(abstraction(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 663: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(abstraction(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 664: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(thing(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 665: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(specific(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 666: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(singleton(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 667: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(abstraction(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 668: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(organism(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 669: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(entity(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 670: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(human_person(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 671: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(male(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 672: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(living(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 673: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(impartial(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 674: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(relation(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 675: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(nonexistent(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 676: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(unisex(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 677: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(thing(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 678: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(event(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 679: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(specific(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 680: ifeq2(be(X, skc9, skc14, skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 681: ifeq2(agent(X, skc12, skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 682: ifeq2(of(X, skc13, skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 683: ifeq2(theme(X, skc12, skc11), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 684: ifeq2(of(X, skc15, skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 685: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(human(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 686: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(living(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 687: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(animate(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 688: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(singleton(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 689: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(specific(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 690: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(singleton(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 691: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(specific(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 692: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(general(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 693: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(general(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 694: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(nonexistent(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 695: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(nonexistent(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 696: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(general(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 697: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(nonhuman(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 698: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(unisex(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 699: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(thing(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 700: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(thing(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 701: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(thing(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 702: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(thing(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 703: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(thing(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 704: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(unisex(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 705: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(entity(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 706: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(abstraction(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 707: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(relname(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 708: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(existent(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 709: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(impartial(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 710: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(unisex(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 711: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(unisex(X, skc12), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 712: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(unisex(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 713: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(nonhuman(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 714: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(relname(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 715: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(smoke(X, skf1(Y)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 716: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(event(X, skf1(Y)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 717: ifeq2(present(X, skf1(Y)), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 718: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(general(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 719: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(general(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 720: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(specific(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 721: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(existent(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 722: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(thing(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 723: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(thing(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 724: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(unisex(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 725: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(unisex(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 726: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(nonhuman(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 727: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(nonhuman(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 728: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(unisex(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 729: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(thing(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 730: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(singleton(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 731: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(general(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 732: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(singleton(X, skc9), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 733: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(singleton(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 734: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(relation(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 735: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(relation(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 736: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(singleton(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 737: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(thing(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 738: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(singleton(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 739: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(eventuality(X, skf1(Y)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 740: ifeq2(be(X, skc9, skc14, skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 741: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(abstraction(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 742: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(abstraction(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 743: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(singleton(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 744: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(singleton(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 745: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(singleton(X, skc15), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 746: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(singleton(X, skc14), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 747: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(specific(X, skf1(Y)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 748: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(nonexistent(X, skf1(Y)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 749: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(thing(X, skf1(Y)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 750: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(unisex(X, skf1(Y)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 751: ifeq2(agent(X, skf1(skc14), skc14), nonhuman(skc11, skc11), ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 752: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(singleton(X, skf1(Y)), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 754: ifeq3(of(X, Y, Z), nonhuman(skc11, skc11), ifeq3(of(X, W, Z), nonhuman(skc11, skc11), ifeq3(forename(X, Y), nonhuman(skc11, skc11), ifeq3(forename(X, W), nonhuman(skc11, skc11), ifeq3(entity(X, Z), nonhuman(skc11, skc11), Y, W), W), W), W), W) -> W % 16.60/15.78 755: ifeq3(of(skc8, X, skc14), nonhuman(skc11, skc11), ifeq3(forename(skc8, X), nonhuman(skc11, skc11), skc13, X), X) -> X % 16.60/15.78 756: skc15 -> skc13 % 16.60/15.78 757: jules_forename(skc8, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 758: jules_forename(skc11, skc13) -> nonhuman(skc11, skc11) % 16.60/15.78 759: ifeq2(accessible_world(skc8, X), nonhuman(skc11, skc11), jules_forename(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 760: ifeq2(accessible_world(skc11, X), nonhuman(skc11, skc11), jules_forename(X, skc13), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 761: ifeq3(of(skc8, X, skc14), nonhuman(skc11, skc11), ifeq3(forename(skc8, X), nonhuman(skc11, skc11), X, skc13), skc13) -> skc13 % 16.60/15.78 762: ifeq3(of(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(forename(skc11, X), nonhuman(skc11, skc11), skc13, X), X) -> X % 16.60/15.78 763: ifeq3(of(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(forename(skc11, X), nonhuman(skc11, skc11), X, skc13), skc13) -> skc13 % 16.60/15.78 764: ifeq2(accessible_world(X, skc8), nonhuman(skc11, skc11), ifeq2(jules_forename(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 765: ifeq2(accessible_world(X, skc11), nonhuman(skc11, skc11), ifeq2(jules_forename(X, skc13), nonhuman(skc11, skc11), nonhuman(skc11, skc11), nonhuman(skc11, skc11)), nonhuman(skc11, skc11)) -> nonhuman(skc11, skc11) % 16.60/15.78 766: ifeq3(of(skc8, skc13, X), nonhuman(skc11, skc11), ifeq3(of(skc8, Y, X), nonhuman(skc11, skc11), ifeq3(forename(skc8, Y), nonhuman(skc11, skc11), ifeq3(entity(skc8, X), nonhuman(skc11, skc11), skc13, Y), Y), Y), Y) -> Y % 16.60/15.78 767: ifeq3(of(skc8, skc13, X), nonhuman(skc11, skc11), ifeq3(of(skc8, skc13, X), nonhuman(skc11, skc11), ifeq3(entity(skc8, X), nonhuman(skc11, skc11), skc13, skc13), skc13), skc13) -> skc13 % 16.60/15.78 768: ifeq3(of(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(of(skc8, skc13, Y), nonhuman(skc11, skc11), ifeq3(forename(skc8, X), nonhuman(skc11, skc11), ifeq3(entity(skc8, Y), nonhuman(skc11, skc11), X, skc13), skc13), skc13), skc13) -> skc13 % 16.60/15.78 769: ifeq3(of(skc8, X, skc14), nonhuman(skc11, skc11), ifeq3(of(skc8, Y, skc14), nonhuman(skc11, skc11), ifeq3(forename(skc8, X), nonhuman(skc11, skc11), ifeq3(forename(skc8, Y), nonhuman(skc11, skc11), X, Y), Y), Y), Y) -> Y % 16.60/15.78 770: ifeq3(of(skc11, skc13, X), nonhuman(skc11, skc11), ifeq3(of(skc11, Y, X), nonhuman(skc11, skc11), ifeq3(forename(skc11, Y), nonhuman(skc11, skc11), ifeq3(entity(skc11, X), nonhuman(skc11, skc11), skc13, Y), Y), Y), Y) -> Y % 16.60/15.78 771: ifeq3(of(skc11, skc13, X), nonhuman(skc11, skc11), ifeq3(of(skc11, skc13, X), nonhuman(skc11, skc11), ifeq3(entity(skc11, X), nonhuman(skc11, skc11), skc13, skc13), skc13), skc13) -> skc13 % 16.60/15.78 772: ifeq3(of(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(of(skc11, skc13, Y), nonhuman(skc11, skc11), ifeq3(forename(skc11, X), nonhuman(skc11, skc11), ifeq3(entity(skc11, Y), nonhuman(skc11, skc11), X, skc13), skc13), skc13), skc13) -> skc13 % 16.60/15.78 773: ifeq3(of(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(of(skc11, Y, skc14), nonhuman(skc11, skc11), ifeq3(forename(skc11, X), nonhuman(skc11, skc11), ifeq3(forename(skc11, Y), nonhuman(skc11, skc11), X, Y), Y), Y), Y) -> Y % 16.60/15.78 775: ifeq3(theme(X, Y, Z), nonhuman(skc11, skc11), ifeq3(theme(X, W, V), nonhuman(skc11, skc11), ifeq3(agent(X, Y, U), nonhuman(skc11, skc11), ifeq3(agent(X, W, U), nonhuman(skc11, skc11), ifeq3(think_believe_consider(X, Y), nonhuman(skc11, skc11), ifeq3(think_believe_consider(X, W), nonhuman(skc11, skc11), ifeq3(proposition(X, Z), nonhuman(skc11, skc11), ifeq3(proposition(X, V), nonhuman(skc11, skc11), V, Z), Z), Z), Z), Z), Z), Z), Z) -> Z % 16.60/15.78 776: ifeq3(theme(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), skc11, Y), Y), Y), Y), Y) -> Y % 16.60/15.78 777: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), skc11, X), X) -> X % 16.60/15.78 778: ifeq3(agent(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, X), nonhuman(skc11, skc11), skc11, skc11), skc11) -> skc11 % 16.60/15.78 779: ifeq3(theme(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), skc11, Y), Y), Y), Y) -> Y % 16.60/15.78 780: ifeq3(theme(skc8, X, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11) -> skc11 % 16.60/15.78 781: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), skc11, X), X), X), X) -> X % 16.60/15.78 782: ifeq3(theme(skc8, X, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 783: ifeq3(theme(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 784: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), X, skc11), skc11) -> skc11 % 16.60/15.78 785: ifeq3(theme(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 786: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), X, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 787: ifeq3(theme(skc8, X, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 788: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), skc11, Y), Y), Y), Y), Y) -> Y % 16.60/15.78 789: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), skc11, X), X) -> X % 16.60/15.78 790: ifeq3(agent(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, X), nonhuman(skc11, skc11), skc11, skc11), skc11) -> skc11 % 16.60/15.78 791: ifeq3(theme(skc11, skf1(skc14), X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), skc11, X), X), X) -> X % 16.60/15.78 792: ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), skc11, skc11), skc11) -> skc11 % 16.60/15.78 793: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), skc11, Y), Y), Y), Y) -> Y % 16.60/15.78 794: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11) -> skc11 % 16.60/15.78 795: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), skc11, X), X), X), X) -> X % 16.60/15.78 796: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 797: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 798: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), X, skc11), skc11) -> skc11 % 16.60/15.78 799: ifeq3(theme(skc11, skf1(skc14), X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), X, skc11), skc11), skc11) -> skc11 % 16.60/15.78 800: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 801: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), X, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 802: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 803: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc8, Y, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, Y, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Z), nonhuman(skc11, skc11), Z, X), X), X), X), X), X) -> X % 16.60/15.78 804: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), Y, X), X), X), X) -> X % 16.60/15.78 805: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc8, Y, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc8, Y, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), skc11, X), X), X), X), X) -> X % 16.60/15.78 806: ifeq3(theme(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(theme(skc8, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Z), nonhuman(skc11, skc11), Z, Y), Y), Y), Y), Y), Y) -> Y % 16.60/15.78 807: ifeq3(theme(skc8, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 808: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc11, Y, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, Y, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Z), nonhuman(skc11, skc11), Z, X), X), X), X), X), X) -> X % 16.60/15.78 809: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, X), X), X), X) -> X % 16.60/15.78 810: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc11, Y, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, Y, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), skc11, X), X), X), X), X) -> X % 16.60/15.78 811: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), skc11, X), X), X), X) -> X % 16.60/15.78 812: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), Y), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, X), X), X), X), X) -> X % 16.60/15.78 813: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(theme(skc11, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Z), nonhuman(skc11, skc11), Z, Y), Y), Y), Y), Y), Y) -> Y % 16.60/15.78 814: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 815: ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), X, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 816: ifeq3(theme(skc11, skf1(skc14), X), nonhuman(skc11, skc11), ifeq3(theme(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, X), X), X), X), X) -> X % 16.60/15.78 817: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc8, Y, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, W), nonhuman(skc11, skc11), ifeq3(agent(skc8, Y, W), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Z), nonhuman(skc11, skc11), Z, X), X), X), X), X), X), X) -> X % 16.60/15.78 818: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Z), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), Y, X), X), X), X), X), X) -> X % 16.60/15.78 819: ifeq3(theme(skc8, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc8, Y, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, Y, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, X), nonhuman(skc11, skc11), skc11, X), X), X), X), X), X) -> X % 16.60/15.78 820: ifeq3(theme(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(theme(skc8, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, W), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, W), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Z), nonhuman(skc11, skc11), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 16.60/15.78 821: ifeq3(theme(skc8, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc8, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, skc12, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 822: ifeq3(theme(skc8, X, Y), nonhuman(skc11, skc11), ifeq3(theme(skc8, Z, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, W), nonhuman(skc11, skc11), ifeq3(agent(skc8, Z, W), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, Z), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Y), nonhuman(skc11, skc11), skc11, Y), Y), Y), Y), Y), Y), Y) -> Y % 16.60/15.78 823: ifeq3(theme(skc8, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc8, Y, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, Y, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, Y), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 824: ifeq3(theme(skc8, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc8, Y, Z), nonhuman(skc11, skc11), ifeq3(agent(skc8, X, W), nonhuman(skc11, skc11), ifeq3(agent(skc8, Y, W), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc8, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc8, Z), nonhuman(skc11, skc11), Z, skc11), skc11), skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 825: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(theme(skc11, Z, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, W), nonhuman(skc11, skc11), ifeq3(agent(skc11, Z, W), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Z), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), skc11, Y), Y), Y), Y), Y), Y), Y) -> Y % 16.60/15.78 826: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc11, Y, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, Y, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), skc11, X), X), X), X), X), X) -> X % 16.60/15.78 827: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, Y, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, Y, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Y), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 828: ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 829: ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 830: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), skc11, skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 831: ifeq3(theme(skc11, skf1(skc14), X), nonhuman(skc11, skc11), ifeq3(theme(skc11, Y, skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, Y, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), skc11, X), X), X), X), X), X) -> X % 16.60/15.78 832: ifeq3(theme(skc11, skf1(skc14), X), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), skc11, X), X), X), X), X) -> X % 16.60/15.78 833: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), skc11, Y), Y), Y), Y), Y), Y) -> Y % 16.60/15.78 834: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(theme(skc11, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, W), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, W), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Z), nonhuman(skc11, skc11), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 16.60/15.78 835: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Z), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, X), X), X), X), X), X) -> X % 16.60/15.78 836: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, skc12, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, Z), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 837: ifeq3(theme(skc11, skc12, X), nonhuman(skc11, skc11), ifeq3(theme(skc11, Y, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, skc12, W), nonhuman(skc11, skc11), ifeq3(agent(skc11, Y, W), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Z), nonhuman(skc11, skc11), Z, X), X), X), X), X), X), X) -> X % 16.60/15.78 838: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, Y, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, W), nonhuman(skc11, skc11), ifeq3(agent(skc11, Y, W), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Z), nonhuman(skc11, skc11), Z, skc11), skc11), skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 839: ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 840: ifeq3(theme(skc11, skf1(skc14), skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), X, skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 841: ifeq3(theme(skc11, X, skc11), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), Y), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, skc11), skc11), skc11), skc11), skc11), skc11) -> skc11 % 16.60/15.78 842: ifeq3(theme(skc11, skf1(skc14), X), nonhuman(skc11, skc11), ifeq3(theme(skc11, Y, Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, Y, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Z), nonhuman(skc11, skc11), Z, X), X), X), X), X), X), X) -> X % 16.60/15.78 843: ifeq3(theme(skc11, skf1(skc14), X), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), Y), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, X), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), Y, X), X), X), X), X), X) -> X % 16.60/15.78 844: ifeq3(theme(skc11, X, Y), nonhuman(skc11, skc11), ifeq3(theme(skc11, skf1(skc14), Z), nonhuman(skc11, skc11), ifeq3(agent(skc11, X, skc14), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, X), nonhuman(skc11, skc11), ifeq3(think_believe_consider(skc11, skf1(skc14)), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Y), nonhuman(skc11, skc11), ifeq3(proposition(skc11, Z), nonhuman(skc11, skc11), Z, Y), Y), Y), Y), Y), Y), Y) -> Y % 16.60/15.78 %------------------------------------------------------------------------------