%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP021-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jul 15 07:23:32 AM UTC 2025 % Result : Satisfiable 5.24s 5.12s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : NLP021-10 : TPTP v9.0.0. Released v7.3.0. % 0.07/0.11 % Command : run_Leo-III %s %d THM % 0.12/0.32 % Computer : n011.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Mon Jul 14 14:10:19 EDT 2025 % 0.12/0.32 % CPUTime : % 5.24/5.12 % SZS status Satisfiable % 5.24/5.12 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 5.24/5.12 1: city(skc13) -> true % 5.24/5.12 2: hollywood(skc13) -> true % 5.24/5.12 3: event(skc12) -> true % 5.24/5.12 4: lonely(skc11) -> true % 5.24/5.12 5: way(skc11) -> true % 5.24/5.12 6: street(skc11) -> true % 5.24/5.12 7: seat(skc9) -> true % 5.24/5.12 8: furniture(skc9) -> true % 5.24/5.12 9: front(skc9) -> true % 5.24/5.12 10: young(skc8) -> true % 5.24/5.12 11: man(skc8) -> true % 5.24/5.12 12: fellow(skc8) -> true % 5.24/5.12 13: fellow(skc7) -> true % 5.24/5.12 14: man(skc7) -> true % 5.24/5.12 15: young(skc7) -> true % 5.24/5.12 16: chevy(skc10) -> true % 5.24/5.12 17: car(skc10) -> true % 5.24/5.12 18: white(skc10) -> true % 5.24/5.12 19: dirty(skc10) -> true % 5.24/5.12 20: old(skc10) -> true % 5.24/5.12 21: in(skc12, skc13) -> true % 5.24/5.12 22: barrel(skc12, skc10) -> true % 5.24/5.12 23: down(skc12, skc11) -> true % 5.24/5.12 24: in(skc8, skc9) -> true % 5.24/5.12 25: in(skc7, skc9) -> true % 5.24/5.12 26: event(skf1(X, Y)) -> true % 5.24/5.12 27: ifeq(X, X, Y, Z) -> Y % 5.24/5.12 28: ifeq3(X, X, Y, Z) -> Y % 5.24/5.12 29: ifeq4(X, X, Y, Z) -> Y % 5.24/5.12 30: ifeq2(X, X, Y, Z) -> Y % 5.24/5.12 31: ifeq4(skc8, skc7, a, b) -> b % 5.24/5.12 32: ifeq2(nonhuman(X), true, entity(X), true) -> true % 5.24/5.12 33: ifeq2(seat(X), true, furniture(X), true) -> true % 5.24/5.12 34: ifeq2(male(X), true, human(X), true) -> true % 5.24/5.12 35: ifeq2(city(X), true, location(X), true) -> true % 5.24/5.12 36: true -> location(skc13) % 5.24/5.12 38: ifeq2(object(X), location(skc13), entity(X), location(skc13)) -> location(skc13) % 5.24/5.12 40: ifeq2(location(X), location(skc13), object(X), location(skc13)) -> location(skc13) % 5.24/5.12 41: object(skc13) -> location(skc13) % 5.24/5.12 42: entity(skc13) -> location(skc13) % 5.24/5.12 44: ifeq2(man(X), location(skc13), male(X), location(skc13)) -> location(skc13) % 5.24/5.12 45: male(skc7) -> location(skc13) % 5.24/5.12 46: male(skc8) -> location(skc13) % 5.24/5.12 47: human(skc8) -> location(skc13) % 5.24/5.12 48: human(skc7) -> location(skc13) % 5.24/5.12 50: ifeq2(hollywood(X), location(skc13), city(X), location(skc13)) -> location(skc13) % 5.24/5.12 52: ifeq2(artifact(X), location(skc13), object(X), location(skc13)) -> location(skc13) % 5.24/5.12 54: ifeq2(event(X), location(skc13), eventuality(X), location(skc13)) -> location(skc13) % 5.24/5.12 55: eventuality(skc12) -> location(skc13) % 5.24/5.12 56: eventuality(skf1(X, Y)) -> location(skc13) % 5.24/5.12 58: ifeq2(instrumentality(X), location(skc13), artifact(X), location(skc13)) -> location(skc13) % 5.24/5.12 60: ifeq2(car(X), location(skc13), vehicle(X), location(skc13)) -> location(skc13) % 5.24/5.12 61: vehicle(skc10) -> location(skc13) % 5.24/5.12 63: ifeq2(transport(X), location(skc13), instrumentality(X), location(skc13)) -> location(skc13) % 5.24/5.12 65: ifeq2(vehicle(X), location(skc13), transport(X), location(skc13)) -> location(skc13) % 5.24/5.12 66: transport(skc10) -> location(skc13) % 5.24/5.12 67: instrumentality(skc10) -> location(skc13) % 5.24/5.12 68: artifact(skc10) -> location(skc13) % 5.24/5.12 69: object(skc10) -> location(skc13) % 5.24/5.12 70: entity(skc10) -> location(skc13) % 5.24/5.12 72: ifeq2(chevy(X), location(skc13), car(X), location(skc13)) -> location(skc13) % 5.24/5.12 74: ifeq2(street(X), location(skc13), way(X), location(skc13)) -> location(skc13) % 5.24/5.12 76: ifeq2(way(X), location(skc13), artifact(X), location(skc13)) -> location(skc13) % 5.24/5.12 77: artifact(skc11) -> location(skc13) % 5.24/5.12 78: object(skc11) -> location(skc13) % 5.24/5.12 79: entity(skc11) -> location(skc13) % 5.24/5.12 81: ifeq2(furniture(X), location(skc13), instrumentality(X), location(skc13)) -> location(skc13) % 5.24/5.12 82: location(skc13) -> instrumentality(skc9) % 5.24/5.12 84: ifeq2(drs(X), instrumentality(skc9), proposition(X), instrumentality(skc9)) -> instrumentality(skc9) % 5.24/5.12 86: ifeq2(woman(X), instrumentality(skc9), female(X), instrumentality(skc9)) -> instrumentality(skc9) % 5.24/5.12 88: ifeq2(proposition(X), instrumentality(skc9), drs(X), instrumentality(skc9)) -> instrumentality(skc9) % 5.24/5.12 90: ifeq2(female(X), instrumentality(skc9), human(X), instrumentality(skc9)) -> instrumentality(skc9) % 5.24/5.12 92: ifeq2(human(X), instrumentality(skc9), organism(X), instrumentality(skc9)) -> instrumentality(skc9) % 5.24/5.12 93: organism(skc7) -> instrumentality(skc9) % 5.24/5.12 94: organism(skc8) -> instrumentality(skc9) % 5.24/5.12 96: ifeq2(front(X), instrumentality(skc9), nonhuman(X), instrumentality(skc9)) -> instrumentality(skc9) % 5.24/5.12 97: instrumentality(skc9) -> nonhuman(skc9) % 5.24/5.12 98: artifact(skc9) -> nonhuman(skc9) % 5.24/5.12 99: object(skc9) -> nonhuman(skc9) % 5.24/5.12 100: entity(skc9) -> nonhuman(skc9) % 5.24/5.12 102: ifeq2(organism(X), nonhuman(skc9), entity(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 103: entity(skc7) -> nonhuman(skc9) % 5.24/5.12 104: entity(skc8) -> nonhuman(skc9) % 5.24/5.12 106: ifeq2(man(X), nonhuman(skc9), human(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 108: ifeq2(fellow(X), nonhuman(skc9), man(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 109: ifeq2(human(X), nonhuman(skc9), organism(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 110: ifeq2(front(X), nonhuman(skc9), nonhuman(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 111: ifeq2(female(X), nonhuman(skc9), human(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 112: ifeq2(proposition(X), nonhuman(skc9), drs(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 113: ifeq2(drs(X), nonhuman(skc9), proposition(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 114: ifeq2(woman(X), nonhuman(skc9), female(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 115: ifeq2(male(X), nonhuman(skc9), human(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 116: ifeq2(city(X), nonhuman(skc9), location(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 117: ifeq2(seat(X), nonhuman(skc9), furniture(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 118: ifeq2(nonhuman(X), nonhuman(skc9), entity(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 119: ifeq2(furniture(X), nonhuman(skc9), instrumentality(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 120: ifeq2(way(X), nonhuman(skc9), artifact(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 121: ifeq2(street(X), nonhuman(skc9), way(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 122: ifeq2(vehicle(X), nonhuman(skc9), transport(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 123: ifeq2(chevy(X), nonhuman(skc9), car(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 124: ifeq2(transport(X), nonhuman(skc9), instrumentality(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 125: ifeq2(car(X), nonhuman(skc9), vehicle(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 126: ifeq2(event(X), nonhuman(skc9), eventuality(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 127: ifeq2(instrumentality(X), nonhuman(skc9), artifact(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 128: ifeq2(artifact(X), nonhuman(skc9), object(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 129: ifeq2(hollywood(X), nonhuman(skc9), city(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 130: ifeq2(man(X), nonhuman(skc9), male(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 131: ifeq2(location(X), nonhuman(skc9), object(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 132: ifeq2(object(X), nonhuman(skc9), entity(X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 133: ifeq2(transport(skc9), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 134: ifeq2(instrumentality(skc11), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 135: ifeq2(artifact(skc13), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 137: ifeq(tuple(old(X), new(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 139: ifeq(tuple(entity(X), abstraction(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 141: ifeq(tuple(entity(X), eventuality(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 143: ifeq(tuple(location(X), artifact(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 145: ifeq(tuple(transport(X), furniture(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 147: ifeq(tuple(object(X), organism(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 149: ifeq(tuple(instrumentality(X), way(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 151: ifeq(tuple(nonhuman(X), human(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 153: ifeq(tuple(female(X), male(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 155: ifeq(tuple(woman(X), man(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 157: ifeq(tuple(eventuality(X), abstraction(X)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 158: ifeq2(location(skc11), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 159: ifeq2(organism(skc13), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 160: ifeq2(female(skc7), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 161: ifeq2(female(skc8), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 162: ifeq2(way(skc9), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 163: ifeq2(nonhuman(skc13), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 165: ifeq2(of(X, Y), nonhuman(skc9), have(skf1(X, Y), Y, X), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 166: ifeq2(furniture(skc10), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 167: ifeq2(nonhuman(skc11), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 168: ifeq2(location(skc9), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 169: ifeq2(organism(skc11), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 171: ifeq3(partof(X, Y), nonhuman(skc9), ifeq3(partof(X, Z), nonhuman(skc9), Y, Z), Z) -> Z % 5.24/5.12 172: ifeq2(nonhuman(skc8), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 173: ifeq2(way(skc10), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 174: ifeq2(nonhuman(skc7), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 175: ifeq2(object(skc8), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 176: ifeq2(object(skc7), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 177: ifeq2(organism(skc9), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 179: ifeq2(of(X, Y), nonhuman(skc9), ifeq2(owner(X), nonhuman(skc9), human(X), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 180: ifeq2(location(skc10), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 181: ifeq2(nonhuman(skc10), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 182: ifeq2(organism(skc10), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 184: ifeq2(have(X, Y, Z), nonhuman(skc9), ifeq2(human(Y), nonhuman(skc9), owner(Y), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 185: ifeq2(have(X, skc7, Y), nonhuman(skc9), owner(skc7), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 186: ifeq2(have(X, skc8, Y), nonhuman(skc9), owner(skc8), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 187: ifeq(tuple(transport(skc9), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 188: ifeq(tuple(nonhuman(skc9), new(skc10)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 189: ifeq(tuple(woman(skc7), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 190: ifeq(tuple(woman(skc8), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 191: ifeq(tuple(instrumentality(skc11), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 192: ifeq(tuple(nonhuman(skc9), way(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 193: ifeq(tuple(female(skc8), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 195: ifeq2(have(X, Y, Z), nonhuman(skc9), ifeq2(human(Y), nonhuman(skc9), of(Y, Z), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 196: ifeq2(have(X, skc7, Y), nonhuman(skc9), of(skc7, Y), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 197: ifeq2(have(X, skc8, Y), nonhuman(skc9), of(skc8, Y), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 198: ifeq(tuple(female(skc7), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 199: ifeq(tuple(nonhuman(skc9), organism(skc13)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 200: ifeq(tuple(nonhuman(skc9), abstraction(skc12)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 201: ifeq(tuple(entity(skc12), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 202: ifeq(tuple(nonhuman(skc9), artifact(skc13)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 203: ifeq(tuple(location(skc11), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 205: ifeq2(have(X, Y, Z), nonhuman(skc9), ifeq2(event(X), nonhuman(skc9), of(Y, Z), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 206: ifeq2(have(skc12, X, Y), nonhuman(skc9), of(X, Y), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 207: ifeq2(have(skf1(X, Y), Z, W), nonhuman(skc9), of(Z, W), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 209: ifeq2(of(X, Y), nonhuman(skc9), ifeq2(owner(X), nonhuman(skc9), have(Z, X, Y), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 210: ifeq3(partof(X, ifeq3(partof(X, Y), nonhuman(skc9), Y, Y)), nonhuman(skc9), Y, Y) -> Y % 5.24/5.12 211: ifeq(tuple(nonhuman(skc7), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 212: ifeq(tuple(location(skc9), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 213: ifeq(tuple(nonhuman(skc9), organism(skc11)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 214: ifeq(tuple(nonhuman(skc9), eventuality(skc13)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 215: ifeq(tuple(nonhuman(skc9), furniture(skc10)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 216: ifeq(tuple(nonhuman(skc9), abstraction(skc13)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 217: ifeq(tuple(nonhuman(skc8), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 218: ifeq(tuple(nonhuman(skc9), way(skc10)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 219: ifeq(tuple(object(skc8), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 220: ifeq(tuple(object(skc7), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 221: ifeq(tuple(nonhuman(skc9), abstraction(skc11)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 222: ifeq(tuple(nonhuman(skc9), organism(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 223: ifeq(tuple(nonhuman(skc9), eventuality(skc11)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 224: ifeq(tuple(nonhuman(skc9), abstraction(skf1(X, Y))), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 225: ifeq(tuple(location(skc10), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 226: ifeq(tuple(nonhuman(skc9), eventuality(skc8)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 227: ifeq(tuple(nonhuman(skc9), eventuality(skc7)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 228: ifeq(tuple(nonhuman(skc9), eventuality(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 229: ifeq(tuple(nonhuman(skc9), abstraction(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 230: ifeq(tuple(nonhuman(skc9), abstraction(skc7)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 231: ifeq(tuple(nonhuman(skc9), abstraction(skc8)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 232: ifeq(tuple(entity(skf1(X, Y)), nonhuman(skc9)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 233: ifeq(tuple(nonhuman(skc9), organism(skc10)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 234: ifeq(tuple(nonhuman(skc9), eventuality(skc10)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 235: ifeq(tuple(nonhuman(skc9), abstraction(skc10)), tuple(nonhuman(skc9), nonhuman(skc9)), a, b) -> b % 5.24/5.12 236: ifeq2(of(skc7, X), nonhuman(skc9), ifeq2(owner(skc7), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 237: ifeq2(of(skc8, X), nonhuman(skc9), ifeq2(owner(skc8), nonhuman(skc9), nonhuman(skc9), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 239: ifeq2(have(X, Y, Z), nonhuman(skc9), ifeq2(nonhuman(Y), nonhuman(skc9), ifeq2(nonhuman(Z), nonhuman(skc9), partof(Z, Y), nonhuman(skc9)), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 240: ifeq2(have(X, skc9, Y), nonhuman(skc9), ifeq2(nonhuman(Y), nonhuman(skc9), partof(Y, skc9), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 241: ifeq2(have(X, skc9, skc9), nonhuman(skc9), partof(skc9, skc9), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 242: ifeq2(have(X, Y, skc9), nonhuman(skc9), ifeq2(nonhuman(Y), nonhuman(skc9), partof(skc9, Y), nonhuman(skc9)), nonhuman(skc9)) -> nonhuman(skc9) % 5.24/5.12 %------------------------------------------------------------------------------