%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP022-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jul 15 07:23:32 AM UTC 2025 % Result : Satisfiable 5.43s 5.31s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NLP022-10 : TPTP v9.0.0. Released v7.5.0. % 0.04/0.12 % Command : run_Leo-III %s %d THM % 0.12/0.33 % Computer : n006.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:10:49 EDT 2025 % 0.12/0.33 % CPUTime : % 5.43/5.31 % SZS status Satisfiable % 5.43/5.31 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 5.43/5.31 1: hollywood(skc13) -> true % 5.43/5.31 2: city(skc13) -> true % 5.43/5.31 3: event(skc12) -> true % 5.43/5.31 4: chevy(skc11) -> true % 5.43/5.31 5: car(skc11) -> true % 5.43/5.31 6: white(skc11) -> true % 5.43/5.31 7: dirty(skc11) -> true % 5.43/5.31 8: old(skc11) -> true % 5.43/5.31 9: seat(skc9) -> true % 5.43/5.31 10: furniture(skc9) -> true % 5.43/5.31 11: front(skc9) -> true % 5.43/5.31 12: young(skc8) -> true % 5.43/5.31 13: man(skc8) -> true % 5.43/5.31 14: fellow(skc8) -> true % 5.43/5.31 15: fellow(skc7) -> true % 5.43/5.31 16: man(skc7) -> true % 5.43/5.31 17: young(skc7) -> true % 5.43/5.31 18: lonely(skc10) -> true % 5.43/5.31 19: way(skc10) -> true % 5.43/5.31 20: street(skc10) -> true % 5.43/5.31 21: in(skc12, skc13) -> true % 5.43/5.31 22: down(skc12, skc10) -> true % 5.43/5.31 23: barrel(skc12, skc11) -> true % 5.43/5.31 24: in(skc8, skc9) -> true % 5.43/5.31 25: in(skc7, skc9) -> true % 5.43/5.31 26: event(skf1(X, Y)) -> true % 5.43/5.31 27: ifeq(X, X, Y, Z) -> Y % 5.43/5.31 28: ifeq3(X, X, Y, Z) -> Y % 5.43/5.31 29: ifeq4(X, X, Y, Z) -> Y % 5.43/5.31 30: ifeq2(X, X, Y, Z) -> Y % 5.43/5.31 31: ifeq4(skc8, skc7, a, b) -> b % 5.43/5.31 32: ifeq2(nonhuman(X), true, entity(X), true) -> true % 5.43/5.31 33: ifeq2(seat(X), true, furniture(X), true) -> true % 5.43/5.31 34: ifeq2(male(X), true, human(X), true) -> true % 5.43/5.31 35: ifeq2(city(X), true, location(X), true) -> true % 5.43/5.31 36: location(skc13) -> true % 5.43/5.31 37: ifeq2(object(X), true, entity(X), true) -> true % 5.43/5.31 38: ifeq2(location(X), true, object(X), true) -> true % 5.43/5.31 39: object(skc13) -> true % 5.43/5.31 40: entity(skc13) -> true % 5.43/5.31 41: ifeq2(man(X), true, male(X), true) -> true % 5.43/5.31 42: male(skc7) -> true % 5.43/5.31 43: male(skc8) -> true % 5.43/5.31 44: human(skc8) -> true % 5.43/5.31 45: human(skc7) -> true % 5.43/5.31 46: ifeq2(hollywood(X), true, city(X), true) -> true % 5.43/5.31 47: ifeq2(artifact(X), true, object(X), true) -> true % 5.43/5.31 48: ifeq2(event(X), true, eventuality(X), true) -> true % 5.43/5.31 49: eventuality(skc12) -> true % 5.43/5.31 50: eventuality(skf1(X, Y)) -> true % 5.43/5.31 51: ifeq2(instrumentality(X), true, artifact(X), true) -> true % 5.43/5.31 52: ifeq2(car(X), true, vehicle(X), true) -> true % 5.43/5.31 53: vehicle(skc11) -> true % 5.43/5.31 54: ifeq2(vehicle(X), true, transport(X), true) -> true % 5.43/5.31 55: transport(skc11) -> true % 5.43/5.31 56: ifeq2(transport(X), true, instrumentality(X), true) -> true % 5.43/5.31 57: instrumentality(skc11) -> true % 5.43/5.31 58: artifact(skc11) -> true % 5.43/5.31 59: object(skc11) -> true % 5.43/5.31 60: entity(skc11) -> true % 5.43/5.31 61: ifeq2(chevy(X), true, car(X), true) -> true % 5.43/5.31 62: ifeq2(street(X), true, way(X), true) -> true % 5.43/5.31 63: ifeq2(way(X), true, artifact(X), true) -> true % 5.43/5.31 64: artifact(skc10) -> true % 5.43/5.31 65: object(skc10) -> true % 5.43/5.31 66: entity(skc10) -> true % 5.43/5.31 67: ifeq2(furniture(X), true, instrumentality(X), true) -> true % 5.43/5.31 68: instrumentality(skc9) -> true % 5.43/5.31 69: artifact(skc9) -> true % 5.43/5.31 70: object(skc9) -> true % 5.43/5.31 71: entity(skc9) -> true % 5.43/5.31 72: ifeq2(drs(X), true, proposition(X), true) -> true % 5.43/5.31 73: ifeq2(woman(X), true, female(X), true) -> true % 5.43/5.31 74: ifeq2(proposition(X), true, drs(X), true) -> true % 5.43/5.31 75: ifeq2(female(X), true, human(X), true) -> true % 5.43/5.31 76: ifeq2(human(X), true, organism(X), true) -> true % 5.43/5.31 77: organism(skc7) -> true % 5.43/5.31 78: organism(skc8) -> true % 5.43/5.31 79: ifeq2(organism(X), true, entity(X), true) -> true % 5.43/5.31 80: entity(skc7) -> true % 5.43/5.31 81: entity(skc8) -> true % 5.43/5.31 82: ifeq2(front(X), true, nonhuman(X), true) -> true % 5.43/5.31 83: nonhuman(skc9) -> true % 5.43/5.31 84: ifeq2(man(X), true, human(X), true) -> true % 5.43/5.31 85: ifeq2(fellow(X), true, man(X), true) -> true % 5.43/5.31 86: ifeq2(transport(skc9), true, true, true) -> true % 5.43/5.31 87: ifeq2(instrumentality(skc10), true, true, true) -> true % 5.43/5.31 88: ifeq2(location(skc10), true, true, true) -> true % 5.43/5.31 89: ifeq2(way(skc9), true, true, true) -> true % 5.43/5.31 90: ifeq2(female(skc7), true, true, true) -> true % 5.43/5.31 91: ifeq2(female(skc8), true, true, true) -> true % 5.43/5.31 92: ifeq2(artifact(skc13), true, true, true) -> true % 5.43/5.31 93: ifeq2(organism(skc10), true, true, true) -> true % 5.43/5.31 94: ifeq2(nonhuman(skc13), true, true, true) -> true % 5.43/5.31 95: ifeq2(organism(skc13), true, true, true) -> true % 5.43/5.31 96: ifeq2(location(skc9), true, true, true) -> true % 5.43/5.31 97: ifeq2(furniture(skc11), true, true, true) -> true % 5.43/5.31 98: ifeq2(nonhuman(skc10), true, true, true) -> true % 5.43/5.31 99: ifeq2(object(skc7), true, true, true) -> true % 5.43/5.31 100: ifeq2(nonhuman(skc8), true, true, true) -> true % 5.43/5.31 101: ifeq2(nonhuman(skc7), true, true, true) -> true % 5.43/5.31 102: ifeq2(object(skc8), true, true, true) -> true % 5.43/5.31 103: ifeq2(organism(skc9), true, true, true) -> true % 5.43/5.31 104: ifeq2(way(skc11), true, true, true) -> true % 5.43/5.31 105: ifeq2(location(skc11), true, true, true) -> true % 5.43/5.31 106: ifeq2(nonhuman(skc11), true, true, true) -> true % 5.43/5.31 107: ifeq2(organism(skc11), true, true, true) -> true % 5.43/5.31 108: ifeq(tuple(old(X), new(X)), tuple(true, true), a, b) -> b % 5.43/5.31 109: ifeq(tuple(true, new(skc11)), tuple(true, true), a, b) -> b % 5.43/5.31 110: ifeq(tuple(entity(X), abstraction(X)), tuple(true, true), a, b) -> b % 5.43/5.31 111: ifeq(tuple(entity(X), eventuality(X)), tuple(true, true), a, b) -> b % 5.43/5.31 112: ifeq(tuple(location(X), artifact(X)), tuple(true, true), a, b) -> b % 5.43/5.31 113: ifeq(tuple(transport(X), furniture(X)), tuple(true, true), a, b) -> b % 5.43/5.31 114: ifeq(tuple(transport(skc9), true), tuple(true, true), a, b) -> b % 5.43/5.31 115: ifeq(tuple(object(X), organism(X)), tuple(true, true), a, b) -> b % 5.43/5.31 116: ifeq(tuple(instrumentality(X), way(X)), tuple(true, true), a, b) -> b % 5.43/5.31 117: ifeq(tuple(instrumentality(skc10), true), tuple(true, true), a, b) -> b % 5.43/5.31 118: ifeq(tuple(nonhuman(X), human(X)), tuple(true, true), a, b) -> b % 5.43/5.31 119: ifeq(tuple(female(X), male(X)), tuple(true, true), a, b) -> b % 5.43/5.31 120: ifeq(tuple(woman(X), man(X)), tuple(true, true), a, b) -> b % 5.43/5.31 121: ifeq(tuple(woman(skc7), true), tuple(true, true), a, b) -> b % 5.43/5.31 122: ifeq(tuple(woman(skc8), true), tuple(true, true), a, b) -> b % 5.43/5.31 123: ifeq(tuple(eventuality(X), abstraction(X)), tuple(true, true), a, b) -> b % 5.43/5.31 124: ifeq(tuple(true, abstraction(skc12)), tuple(true, true), a, b) -> b % 5.43/5.31 125: ifeq(tuple(true, way(skc9)), tuple(true, true), a, b) -> b % 5.43/5.31 126: ifeq(tuple(female(skc8), true), tuple(true, true), a, b) -> b % 5.43/5.31 127: ifeq(tuple(female(skc7), true), tuple(true, true), a, b) -> b % 5.43/5.31 128: ifeq(tuple(true, human(skc9)), tuple(true, true), a, b) -> b % 5.43/5.31 129: ifeq2(of(X, Y), true, have(skf1(X, Y), Y, X), true) -> true % 5.43/5.31 130: ifeq(tuple(entity(skc12), true), tuple(true, true), a, b) -> b % 5.43/5.31 131: ifeq(tuple(true, artifact(skc13)), tuple(true, true), a, b) -> b % 5.43/5.31 132: ifeq(tuple(location(skc10), true), tuple(true, true), a, b) -> b % 5.43/5.31 133: ifeq(tuple(location(skc9), true), tuple(true, true), a, b) -> b % 5.43/5.31 134: ifeq(tuple(true, furniture(skc11)), tuple(true, true), a, b) -> b % 5.43/5.31 135: ifeq(tuple(nonhuman(skc8), true), tuple(true, true), a, b) -> b % 5.43/5.31 136: ifeq(tuple(true, organism(skc13)), tuple(true, true), a, b) -> b % 5.43/5.31 137: ifeq(tuple(true, organism(skc10)), tuple(true, true), a, b) -> b % 5.43/5.31 138: ifeq(tuple(nonhuman(skc7), true), tuple(true, true), a, b) -> b % 5.43/5.31 139: ifeq3(partof(X, Y), true, ifeq3(partof(X, Z), true, Y, Z), Z) -> Z % 5.43/5.31 140: ifeq(tuple(object(skc7), true), tuple(true, true), a, b) -> b % 5.43/5.31 141: ifeq(tuple(true, organism(skc9)), tuple(true, true), a, b) -> b % 5.43/5.31 142: ifeq(tuple(object(skc8), true), tuple(true, true), a, b) -> b % 5.43/5.31 143: ifeq(tuple(true, way(skc11)), tuple(true, true), a, b) -> b % 5.43/5.31 144: ifeq(tuple(true, abstraction(skc10)), tuple(true, true), a, b) -> b % 5.43/5.31 145: ifeq(tuple(true, abstraction(skc13)), tuple(true, true), a, b) -> b % 5.43/5.31 146: ifeq(tuple(true, eventuality(skc10)), tuple(true, true), a, b) -> b % 5.43/5.31 147: ifeq(tuple(true, eventuality(skc13)), tuple(true, true), a, b) -> b % 5.43/5.31 148: ifeq2(of(X, Y), true, ifeq2(owner(X), true, human(X), true), true) -> true % 5.43/5.31 149: ifeq3(partof(X, ifeq3(partof(X, Y), true, Y, Y)), true, Y, Y) -> Y % 5.43/5.31 150: ifeq(tuple(true, abstraction(skf1(X, Y))), tuple(true, true), a, b) -> b % 5.43/5.31 151: ifeq(tuple(true, eventuality(skc7)), tuple(true, true), a, b) -> b % 5.43/5.31 152: ifeq(tuple(true, eventuality(skc9)), tuple(true, true), a, b) -> b % 5.43/5.31 153: ifeq(tuple(location(skc11), true), tuple(true, true), a, b) -> b % 5.43/5.31 154: ifeq(tuple(true, eventuality(skc8)), tuple(true, true), a, b) -> b % 5.43/5.31 155: ifeq(tuple(true, abstraction(skc7)), tuple(true, true), a, b) -> b % 5.43/5.31 156: ifeq(tuple(entity(skf1(X, Y)), true), tuple(true, true), a, b) -> b % 5.43/5.31 157: ifeq(tuple(true, abstraction(skc8)), tuple(true, true), a, b) -> b % 5.43/5.31 158: ifeq(tuple(true, abstraction(skc9)), tuple(true, true), a, b) -> b % 5.43/5.31 159: ifeq2(have(X, Y, Z), true, ifeq2(human(Y), true, owner(Y), true), true) -> true % 5.43/5.31 160: ifeq2(have(X, skc7, Y), true, owner(skc7), true) -> true % 5.43/5.31 161: ifeq2(have(X, skc8, Y), true, owner(skc8), true) -> true % 5.43/5.31 162: ifeq(tuple(true, organism(skc11)), tuple(true, true), a, b) -> b % 5.43/5.31 163: ifeq2(of(skc7, X), true, ifeq2(owner(skc7), true, true, true), true) -> true % 5.43/5.31 164: ifeq2(of(skc8, X), true, ifeq2(owner(skc8), true, true, true), true) -> true % 5.43/5.31 165: ifeq(tuple(true, abstraction(skc11)), tuple(true, true), a, b) -> b % 5.43/5.31 166: ifeq(tuple(true, eventuality(skc11)), tuple(true, true), a, b) -> b % 5.43/5.31 167: ifeq2(have(X, Y, Z), true, ifeq2(event(X), true, of(Y, Z), true), true) -> true % 5.43/5.31 168: ifeq2(have(skc12, X, Y), true, of(X, Y), true) -> true % 5.43/5.31 169: ifeq2(have(skf1(X, Y), Z, W), true, of(Z, W), true) -> true % 5.43/5.31 170: ifeq2(have(X, Y, Z), true, ifeq2(human(Y), true, of(Y, Z), true), true) -> true % 5.43/5.31 171: ifeq2(have(X, skc7, Y), true, of(skc7, Y), true) -> true % 5.43/5.31 172: ifeq2(have(X, skc8, Y), true, of(skc8, Y), true) -> true % 5.43/5.31 173: ifeq2(of(X, Y), true, ifeq2(owner(X), true, have(Z, X, Y), true), true) -> true % 5.43/5.31 174: ifeq2(have(X, Y, Z), true, ifeq2(nonhuman(Y), true, ifeq2(nonhuman(Z), true, partof(Z, Y), true), true), true) -> true % 5.43/5.31 175: ifeq2(have(X, skc9, Y), true, ifeq2(nonhuman(Y), true, partof(Y, skc9), true), true) -> true % 5.43/5.31 176: ifeq2(have(X, skc9, skc9), true, partof(skc9, skc9), true) -> true % 5.43/5.31 177: ifeq2(have(X, Y, skc9), true, ifeq2(nonhuman(Y), true, partof(skc9, Y), true), true) -> true % 5.43/5.31 %------------------------------------------------------------------------------