%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : NLP003-10 : TPTP v9.0.0. Released v7.3.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:29 AM UTC 2025 % Result : Satisfiable 3.28s 3.24s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.01/0.11 % Problem : NLP003-10 : TPTP v9.0.0. Released v7.3.0. % 0.01/0.11 % Command : run_Leo-III %s %d THM % 0.12/0.30 % Computer : n003.cluster.edu % 0.12/0.30 % Model : x86_64 x86_64 % 0.12/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.30 % Memory : 8042.1875MB % 0.12/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.30 % CPULimit : 300 % 0.12/0.30 % WCLimit : 300 % 0.12/0.30 % DateTime : Mon Jul 14 14:07:49 EDT 2025 % 0.12/0.30 % CPUTime : % 3.28/3.24 % SZS status Satisfiable % 3.28/3.24 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 3.28/3.24 1: hollywood(skc7) -> true % 3.28/3.24 2: city(skc7) -> true % 3.28/3.24 3: event(skc6) -> true % 3.28/3.24 4: chevy(skc5) -> true % 3.28/3.24 5: car(skc5) -> true % 3.28/3.24 6: white(skc5) -> true % 3.28/3.24 7: dirty(skc5) -> true % 3.28/3.24 8: old(skc5) -> true % 3.28/3.24 9: lonely(skc4) -> true % 3.28/3.24 10: way(skc4) -> true % 3.28/3.24 11: street(skc4) -> true % 3.28/3.24 12: in(skc6, skc7) -> true % 3.28/3.24 13: down(skc6, skc4) -> true % 3.28/3.24 14: barrel(skc6, skc5) -> true % 3.28/3.24 15: event(skf1(X, Y)) -> true % 3.28/3.24 16: ifeq(X, X, Y, Z) -> Y % 3.28/3.24 17: ifeq3(X, X, Y, Z) -> Y % 3.28/3.24 18: ifeq2(X, X, Y, Z) -> Y % 3.28/3.24 19: ifeq2(vehicle(X), true, transport(X), true) -> true % 3.28/3.24 20: ifeq2(transport(X), true, instrumentality(X), true) -> true % 3.28/3.24 21: ifeq2(instrumentality(X), true, artifact(X), true) -> true % 3.28/3.24 22: ifeq2(car(X), true, vehicle(X), true) -> true % 3.28/3.24 23: vehicle(skc5) -> true % 3.28/3.24 24: transport(skc5) -> true % 3.28/3.24 25: instrumentality(skc5) -> true % 3.28/3.24 26: artifact(skc5) -> true % 3.28/3.24 27: ifeq2(chevy(X), true, car(X), true) -> true % 3.28/3.24 28: ifeq2(street(X), true, way(X), true) -> true % 3.28/3.24 29: ifeq2(proposition(X), true, drs(X), true) -> true % 3.28/3.24 30: ifeq2(nonhuman(X), true, entity(X), true) -> true % 3.28/3.24 31: ifeq2(drs(X), true, proposition(X), true) -> true % 3.28/3.24 32: ifeq2(woman(X), true, female(X), true) -> true % 3.28/3.24 33: ifeq2(male(X), true, human(X), true) -> true % 3.28/3.24 34: ifeq2(female(X), true, human(X), true) -> true % 3.28/3.24 35: ifeq2(man(X), true, male(X), true) -> true % 3.28/3.24 36: ifeq2(city(X), true, location(X), true) -> true % 3.28/3.24 37: location(skc7) -> true % 3.28/3.24 38: ifeq2(object(X), true, entity(X), true) -> true % 3.28/3.24 39: ifeq2(location(X), true, object(X), true) -> true % 3.28/3.24 40: object(skc7) -> true % 3.28/3.24 41: entity(skc7) -> true % 3.28/3.24 42: ifeq2(hollywood(X), true, city(X), true) -> true % 3.28/3.24 43: ifeq2(artifact(X), true, object(X), true) -> true % 3.28/3.24 44: object(skc5) -> true % 3.28/3.24 45: entity(skc5) -> true % 3.28/3.24 46: ifeq2(event(X), true, eventuality(X), true) -> true % 3.28/3.24 47: eventuality(skc6) -> true % 3.28/3.24 48: eventuality(skf1(X, Y)) -> true % 3.28/3.24 49: ifeq2(way(X), true, artifact(X), true) -> true % 3.28/3.24 50: artifact(skc4) -> true % 3.28/3.24 51: object(skc4) -> true % 3.28/3.24 52: entity(skc4) -> true % 3.28/3.24 53: ifeq2(instrumentality(skc4), true, true, true) -> true % 3.28/3.24 54: ifeq2(location(skc4), true, true, true) -> true % 3.28/3.24 55: ifeq2(artifact(skc7), true, true, true) -> true % 3.28/3.24 56: ifeq2(nonhuman(skc4), true, true, true) -> true % 3.28/3.24 57: ifeq2(nonhuman(skc7), true, true, true) -> true % 3.28/3.24 58: ifeq2(way(skc5), true, true, true) -> true % 3.28/3.24 59: ifeq2(location(skc5), true, true, true) -> true % 3.28/3.24 60: ifeq2(nonhuman(skc5), true, true, true) -> true % 3.28/3.24 61: ifeq(tuple(nonhuman(X), human(X)), tuple(true, true), a, b) -> b % 3.28/3.24 62: ifeq(tuple(woman(X), man(X)), tuple(true, true), a, b) -> b % 3.28/3.24 63: ifeq(tuple(female(X), male(X)), tuple(true, true), a, b) -> b % 3.28/3.24 64: ifeq(tuple(eventuality(X), abstraction(X)), tuple(true, true), a, b) -> b % 3.28/3.24 65: ifeq(tuple(entity(X), abstraction(X)), tuple(true, true), a, b) -> b % 3.28/3.24 66: ifeq(tuple(entity(X), eventuality(X)), tuple(true, true), a, b) -> b % 3.28/3.24 67: ifeq(tuple(old(X), new(X)), tuple(true, true), a, b) -> b % 3.28/3.24 68: ifeq(tuple(true, new(skc5)), tuple(true, true), a, b) -> b % 3.28/3.24 69: ifeq(tuple(location(X), artifact(X)), tuple(true, true), a, b) -> b % 3.28/3.24 70: ifeq(tuple(way(X), instrumentality(X)), tuple(true, true), a, b) -> b % 3.28/3.24 71: ifeq(tuple(true, instrumentality(skc4)), tuple(true, true), a, b) -> b % 3.28/3.24 72: ifeq(tuple(location(skc4), true), tuple(true, true), a, b) -> b % 3.28/3.24 73: ifeq(tuple(true, artifact(skc7)), tuple(true, true), a, b) -> b % 3.28/3.24 74: ifeq(tuple(entity(skc6), true), tuple(true, true), a, b) -> b % 3.28/3.24 75: ifeq2(of(X, Y), true, have(skf1(X, Y), Y, X), true) -> true % 3.28/3.24 76: ifeq(tuple(true, abstraction(skc6)), tuple(true, true), a, b) -> b % 3.28/3.24 77: ifeq3(partof(X, Y), true, ifeq3(partof(X, Z), true, Y, Z), Z) -> Z % 3.28/3.24 78: ifeq(tuple(way(skc5), true), tuple(true, true), a, b) -> b % 3.28/3.24 79: ifeq(tuple(true, abstraction(skc7)), tuple(true, true), a, b) -> b % 3.28/3.24 80: ifeq(tuple(true, eventuality(skc7)), tuple(true, true), a, b) -> b % 3.28/3.24 81: ifeq(tuple(true, eventuality(skc4)), tuple(true, true), a, b) -> b % 3.28/3.24 82: ifeq(tuple(true, abstraction(skc4)), tuple(true, true), a, b) -> b % 3.28/3.24 83: ifeq2(of(X, Y), true, ifeq2(owner(X), true, human(X), true), true) -> true % 3.28/3.24 84: ifeq3(partof(X, ifeq3(partof(X, Y), true, Y, Y)), true, Y, Y) -> Y % 3.28/3.24 85: ifeq(tuple(location(skc5), true), tuple(true, true), a, b) -> b % 3.28/3.24 86: ifeq(tuple(true, abstraction(skf1(X, Y))), tuple(true, true), a, b) -> b % 3.28/3.24 87: ifeq(tuple(entity(skf1(X, Y)), true), tuple(true, true), a, b) -> b % 3.28/3.24 88: ifeq2(have(X, Y, Z), true, ifeq2(human(Y), true, owner(Y), true), true) -> true % 3.28/3.24 89: ifeq(tuple(true, abstraction(skc5)), tuple(true, true), a, b) -> b % 3.28/3.24 90: ifeq(tuple(true, eventuality(skc5)), tuple(true, true), a, b) -> b % 3.28/3.24 91: ifeq2(of(X, Y), true, ifeq2(owner(X), true, have(Z, X, Y), true), true) -> true % 3.28/3.24 92: ifeq2(have(X, Y, Z), true, ifeq2(event(X), true, of(Y, Z), true), true) -> true % 3.28/3.24 93: ifeq2(have(skc6, X, Y), true, of(X, Y), true) -> true % 3.28/3.24 94: ifeq2(have(skf1(X, Y), Z, W), true, of(Z, W), true) -> true % 3.28/3.24 95: ifeq2(have(X, Y, Z), true, ifeq2(human(Y), true, of(Y, Z), true), true) -> true % 3.28/3.24 96: ifeq2(have(X, Y, Z), true, ifeq2(nonhuman(Y), true, ifeq2(nonhuman(Z), true, partof(Z, Y), true), true), true) -> true % 3.28/3.24 %------------------------------------------------------------------------------