%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP020-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n003.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 4.78s 4.66s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP020-10 : TPTP v9.0.0. Released v7.5.0. % 0.00/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.31 % Computer : n003.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.31 % CPULimit : 300 % 0.12/0.31 % WCLimit : 300 % 0.12/0.31 % DateTime : Mon Jul 14 14:10:19 EDT 2025 % 0.12/0.31 % CPUTime : % 4.78/4.66 % SZS status Satisfiable % 4.78/4.66 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 4.78/4.66 1: city(skc11) -> true % 4.78/4.66 2: hollywood(skc11) -> true % 4.78/4.66 3: event(skc10) -> true % 4.78/4.66 4: lonely(skc9) -> true % 4.78/4.66 5: way(skc9) -> true % 4.78/4.66 6: street(skc9) -> true % 4.78/4.66 7: seat(skc7) -> true % 4.78/4.66 8: furniture(skc7) -> true % 4.78/4.66 9: front(skc7) -> true % 4.78/4.66 10: young(skc6) -> true % 4.78/4.66 11: man(skc6) -> true % 4.78/4.66 12: fellow(skc6) -> true % 4.78/4.66 13: chevy(skc8) -> true % 4.78/4.66 14: car(skc8) -> true % 4.78/4.66 15: white(skc8) -> true % 4.78/4.66 16: dirty(skc8) -> true % 4.78/4.66 17: old(skc8) -> true % 4.78/4.66 18: in(skc10, skc11) -> true % 4.78/4.66 19: barrel(skc10, skc8) -> true % 4.78/4.66 20: down(skc10, skc9) -> true % 4.78/4.66 21: in(skc6, skc7) -> true % 4.78/4.66 22: event(skf1(X, Y)) -> true % 4.78/4.66 23: ifeq(X, X, Y, Z) -> Y % 4.78/4.66 24: ifeq3(X, X, Y, Z) -> Y % 4.78/4.66 25: ifeq2(X, X, Y, Z) -> Y % 4.78/4.66 26: ifeq2(nonhuman(X), true, entity(X), true) -> true % 4.78/4.66 27: ifeq2(seat(X), true, furniture(X), true) -> true % 4.78/4.66 28: ifeq2(male(X), true, human(X), true) -> true % 4.78/4.66 29: ifeq2(city(X), true, location(X), true) -> true % 4.78/4.66 30: location(skc11) -> true % 4.78/4.66 31: ifeq2(object(X), true, entity(X), true) -> true % 4.78/4.66 32: ifeq2(location(X), true, object(X), true) -> true % 4.78/4.66 33: object(skc11) -> true % 4.78/4.66 34: entity(skc11) -> true % 4.78/4.66 35: ifeq2(man(X), true, male(X), true) -> true % 4.78/4.66 36: true -> male(skc6) % 4.78/4.66 38: ifeq2(hollywood(X), male(skc6), city(X), male(skc6)) -> male(skc6) % 4.78/4.66 40: ifeq2(artifact(X), male(skc6), object(X), male(skc6)) -> male(skc6) % 4.78/4.66 42: ifeq2(instrumentality(X), male(skc6), artifact(X), male(skc6)) -> male(skc6) % 4.78/4.66 44: ifeq2(event(X), male(skc6), eventuality(X), male(skc6)) -> male(skc6) % 4.78/4.66 45: eventuality(skc10) -> male(skc6) % 4.78/4.66 46: eventuality(skf1(X, Y)) -> male(skc6) % 4.78/4.66 48: ifeq2(car(X), male(skc6), vehicle(X), male(skc6)) -> male(skc6) % 4.78/4.66 49: vehicle(skc8) -> male(skc6) % 4.78/4.66 51: ifeq2(transport(X), male(skc6), instrumentality(X), male(skc6)) -> male(skc6) % 4.78/4.66 53: ifeq2(vehicle(X), male(skc6), transport(X), male(skc6)) -> male(skc6) % 4.78/4.66 54: transport(skc8) -> male(skc6) % 4.78/4.66 55: instrumentality(skc8) -> male(skc6) % 4.78/4.66 56: artifact(skc8) -> male(skc6) % 4.78/4.66 57: object(skc8) -> male(skc6) % 4.78/4.66 58: entity(skc8) -> male(skc6) % 4.78/4.66 60: ifeq2(chevy(X), male(skc6), car(X), male(skc6)) -> male(skc6) % 4.78/4.66 62: ifeq2(street(X), male(skc6), way(X), male(skc6)) -> male(skc6) % 4.78/4.66 64: ifeq2(way(X), male(skc6), artifact(X), male(skc6)) -> male(skc6) % 4.78/4.66 65: artifact(skc9) -> male(skc6) % 4.78/4.66 66: object(skc9) -> male(skc6) % 4.78/4.66 67: entity(skc9) -> male(skc6) % 4.78/4.66 69: ifeq2(furniture(X), male(skc6), instrumentality(X), male(skc6)) -> male(skc6) % 4.78/4.66 70: instrumentality(skc7) -> male(skc6) % 4.78/4.66 71: artifact(skc7) -> male(skc6) % 4.78/4.66 72: object(skc7) -> male(skc6) % 4.78/4.66 73: entity(skc7) -> male(skc6) % 4.78/4.66 75: ifeq2(drs(X), male(skc6), proposition(X), male(skc6)) -> male(skc6) % 4.78/4.66 77: ifeq2(woman(X), male(skc6), female(X), male(skc6)) -> male(skc6) % 4.78/4.66 79: ifeq2(proposition(X), male(skc6), drs(X), male(skc6)) -> male(skc6) % 4.78/4.66 81: ifeq2(female(X), male(skc6), human(X), male(skc6)) -> male(skc6) % 4.78/4.66 83: ifeq2(human(X), male(skc6), organism(X), male(skc6)) -> male(skc6) % 4.78/4.66 85: ifeq2(front(X), male(skc6), nonhuman(X), male(skc6)) -> male(skc6) % 4.78/4.66 86: nonhuman(skc7) -> male(skc6) % 4.78/4.66 88: ifeq2(organism(X), male(skc6), entity(X), male(skc6)) -> male(skc6) % 4.78/4.66 90: ifeq2(man(X), male(skc6), human(X), male(skc6)) -> male(skc6) % 4.78/4.66 91: human(skc6) -> male(skc6) % 4.78/4.66 92: organism(skc6) -> male(skc6) % 4.78/4.66 93: entity(skc6) -> male(skc6) % 4.78/4.66 95: ifeq2(fellow(X), male(skc6), man(X), male(skc6)) -> male(skc6) % 4.78/4.66 96: ifeq2(nonhuman(skc11), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 97: ifeq2(city(X), male(skc6), location(X), male(skc6)) -> male(skc6) % 4.78/4.66 98: ifeq2(male(X), male(skc6), human(X), male(skc6)) -> male(skc6) % 4.78/4.66 99: ifeq2(seat(X), male(skc6), furniture(X), male(skc6)) -> male(skc6) % 4.78/4.66 100: ifeq2(nonhuman(X), male(skc6), entity(X), male(skc6)) -> male(skc6) % 4.78/4.66 101: ifeq2(man(X), male(skc6), male(X), male(skc6)) -> male(skc6) % 4.78/4.66 102: ifeq2(location(X), male(skc6), object(X), male(skc6)) -> male(skc6) % 4.78/4.66 103: ifeq2(object(X), male(skc6), entity(X), male(skc6)) -> male(skc6) % 4.78/4.66 104: ifeq2(female(skc6), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 105: ifeq2(instrumentality(skc9), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 106: ifeq2(transport(skc7), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 108: ifeq(tuple(nonhuman(X), human(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 110: ifeq(tuple(woman(X), man(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 112: ifeq(tuple(female(X), male(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 114: ifeq(tuple(eventuality(X), abstraction(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 116: ifeq(tuple(entity(X), abstraction(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 118: ifeq(tuple(entity(X), eventuality(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 120: ifeq(tuple(old(X), new(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 122: ifeq(tuple(location(X), artifact(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 124: ifeq(tuple(instrumentality(X), way(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 126: ifeq(tuple(transport(X), furniture(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 128: ifeq(tuple(object(X), organism(X)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 129: ifeq2(way(skc7), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 130: ifeq2(location(skc9), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 131: ifeq2(artifact(skc11), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 133: ifeq2(of(X, Y), male(skc6), have(skf1(X, Y), Y, X), male(skc6)) -> male(skc6) % 4.78/4.66 134: ifeq2(organism(skc11), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 135: ifeq2(nonhuman(skc9), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 136: ifeq2(organism(skc9), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 137: ifeq2(furniture(skc8), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 138: ifeq2(object(skc6), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 139: ifeq2(location(skc7), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 140: ifeq2(nonhuman(skc6), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 142: ifeq3(partof(X, Y), male(skc6), ifeq3(partof(X, Z), male(skc6), Y, Z), Z) -> Z % 4.78/4.66 143: ifeq2(organism(skc7), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 144: ifeq2(way(skc8), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 146: ifeq2(of(X, Y), male(skc6), ifeq2(owner(X), male(skc6), human(X), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 147: ifeq2(location(skc8), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 148: ifeq2(nonhuman(skc8), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 149: ifeq2(organism(skc8), male(skc6), male(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 151: ifeq2(have(X, Y, Z), male(skc6), ifeq2(human(Y), male(skc6), owner(Y), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 152: ifeq2(have(X, skc6, Y), male(skc6), owner(skc6), male(skc6)) -> male(skc6) % 4.78/4.66 153: ifeq(tuple(instrumentality(skc9), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 154: ifeq(tuple(transport(skc7), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 155: ifeq(tuple(male(skc6), new(skc8)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 156: ifeq(tuple(woman(skc6), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 157: ifeq(tuple(male(skc6), way(skc7)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 158: ifeq(tuple(male(skc6), abstraction(skc10)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 159: ifeq(tuple(location(skc9), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 160: ifeq(tuple(male(skc6), artifact(skc11)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 162: ifeq2(of(X, Y), male(skc6), ifeq2(owner(X), male(skc6), have(Z, X, Y), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 163: ifeq(tuple(entity(skc10), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 164: ifeq(tuple(male(skc6), human(skc7)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 165: ifeq(tuple(nonhuman(skc6), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 167: ifeq2(have(X, Y, Z), male(skc6), ifeq2(human(Y), male(skc6), of(Y, Z), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 168: ifeq2(have(X, skc6, Y), male(skc6), of(skc6, Y), male(skc6)) -> male(skc6) % 4.78/4.66 170: ifeq2(have(X, Y, Z), male(skc6), ifeq2(event(X), male(skc6), of(Y, Z), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 171: ifeq2(have(skc10, X, Y), male(skc6), of(X, Y), male(skc6)) -> male(skc6) % 4.78/4.66 172: ifeq2(have(skf1(X, Y), Z, W), male(skc6), of(Z, W), male(skc6)) -> male(skc6) % 4.78/4.66 173: ifeq3(partof(X, ifeq3(partof(X, Y), male(skc6), Y, Y)), male(skc6), Y, Y) -> Y % 4.78/4.66 174: ifeq(tuple(object(skc6), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 175: ifeq(tuple(location(skc7), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 176: ifeq(tuple(male(skc6), organism(skc9)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 177: ifeq(tuple(male(skc6), furniture(skc8)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 178: ifeq(tuple(male(skc6), organism(skc11)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 179: ifeq(tuple(male(skc6), organism(skc7)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 180: ifeq(tuple(male(skc6), way(skc8)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 181: ifeq(tuple(male(skc6), abstraction(skc9)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 182: ifeq(tuple(male(skc6), abstraction(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 183: ifeq(tuple(male(skc6), abstraction(skc11)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 184: ifeq(tuple(male(skc6), eventuality(skc11)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 185: ifeq(tuple(male(skc6), eventuality(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 186: ifeq(tuple(male(skc6), eventuality(skc9)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 187: ifeq(tuple(male(skc6), eventuality(skc7)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 188: ifeq(tuple(location(skc8), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 189: ifeq(tuple(entity(skf1(X, Y)), male(skc6)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 190: ifeq(tuple(male(skc6), abstraction(skc7)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 191: ifeq(tuple(male(skc6), abstraction(skf1(X, Y))), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 192: ifeq(tuple(male(skc6), organism(skc8)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 193: ifeq(tuple(male(skc6), abstraction(skc8)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 194: ifeq(tuple(male(skc6), eventuality(skc8)), tuple(male(skc6), male(skc6)), a, b) -> b % 4.78/4.66 195: ifeq2(of(skc6, X), male(skc6), ifeq2(owner(skc6), male(skc6), male(skc6), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 197: ifeq2(have(X, Y, Z), male(skc6), ifeq2(nonhuman(Y), male(skc6), ifeq2(nonhuman(Z), male(skc6), partof(Z, Y), male(skc6)), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 198: ifeq2(have(X, skc7, Y), male(skc6), ifeq2(nonhuman(Y), male(skc6), partof(Y, skc7), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 199: ifeq2(have(X, skc7, skc7), male(skc6), partof(skc7, skc7), male(skc6)) -> male(skc6) % 4.78/4.66 200: ifeq2(have(X, Y, skc7), male(skc6), ifeq2(nonhuman(Y), male(skc6), partof(skc7, Y), male(skc6)), male(skc6)) -> male(skc6) % 4.78/4.66 %------------------------------------------------------------------------------