%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : PUZ054-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:39:21 AM UTC 2025 % Result : Satisfiable 60.00s 60.40s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : PUZ054-10 : TPTP v9.0.0. Released v7.5.0. % 0.03/0.11 % Command : run_Leo-III %s %d THM % 0.12/0.31 % Computer : n006.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 15:56:49 EDT 2025 % 0.12/0.31 % CPUTime : % 60.00/60.40 % SZS status Satisfiable % 60.00/60.40 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 60.00/60.40 1: ifeq(X, X, Y, Z) -> Y % 60.00/60.40 2: ifeq(p(s(s(X)), Y), true, p(X, s(Y)), true) -> true % 60.00/60.40 3: ifeq(p(X, s(s(Y))), true, p(X, s(Y)), true) -> true % 60.00/60.40 4: ifeq(p(s(X), s(Y)), true, p(s(X), Y), true) -> true % 60.00/60.40 5: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(s(s(s(n0)))))))))) -> true % 60.00/60.40 6: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(s(s(n0))))))))) -> true % 60.00/60.40 7: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(s(n0)))))))) -> true % 60.00/60.40 8: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(n0))))))) -> true % 60.00/60.40 9: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(n0)))))) -> true % 60.00/60.40 10: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(n0))))) -> true % 60.00/60.40 11: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(n0)))) -> true % 60.00/60.40 12: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(n0))) -> true % 60.00/60.40 13: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(n0)) -> true % 60.00/60.40 14: p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), n0) -> true % 60.00/60.40 15: p(s(s(s(s(s(s(s(s(n0)))))))), s(n0)) -> true % 60.00/60.40 16: p(s(s(s(s(s(s(s(s(n0)))))))), n0) -> true % 60.00/60.40 17: p(s(s(s(s(s(s(n0)))))), s(n0)) -> true % 60.00/60.40 18: p(s(s(s(s(s(s(n0)))))), n0) -> true % 60.00/60.40 19: p(s(s(s(s(n0)))), s(n0)) -> true % 60.00/60.40 20: p(s(s(s(s(n0)))), n0) -> true % 60.00/60.40 21: p(s(s(n0)), s(n0)) -> true % 60.00/60.40 22: p(s(s(n0)), n0) -> true % 60.00/60.40 23: p(n0, s(n0)) -> true % 60.00/60.40 24: p(n0, s(s(n0))) -> true % 60.00/60.40 25: p(s(s(n0)), s(s(n0))) -> true % 60.00/60.40 26: p(n0, s(s(s(n0)))) -> true % 60.00/60.40 27: p(s(s(s(s(n0)))), s(s(n0))) -> true % 60.00/60.40 28: p(s(s(n0)), s(s(s(n0)))) -> true % 60.00/60.40 29: p(n0, s(s(s(s(n0))))) -> true % 60.00/60.40 30: p(s(s(s(s(s(s(n0)))))), s(s(n0))) -> true % 60.00/60.40 31: p(s(s(s(s(n0)))), s(s(s(n0)))) -> true % 60.00/60.40 32: p(s(s(n0)), s(s(s(s(n0))))) -> true % 60.00/60.40 33: p(n0, s(s(s(s(s(n0)))))) -> true % 60.00/60.40 34: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(n0))) -> true % 60.00/60.40 35: p(s(s(s(s(s(s(n0)))))), s(s(s(n0)))) -> true % 60.00/60.40 36: p(s(s(s(s(n0)))), s(s(s(s(n0))))) -> true % 60.00/60.40 37: p(s(s(n0)), s(s(s(s(s(n0)))))) -> true % 60.00/60.40 38: p(n0, s(s(s(s(s(s(n0))))))) -> true % 60.00/60.40 39: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(n0)))) -> true % 60.00/60.40 40: p(s(s(s(s(s(s(n0)))))), s(s(s(s(n0))))) -> true % 60.00/60.40 41: p(s(s(s(s(n0)))), s(s(s(s(s(n0)))))) -> true % 60.00/60.40 42: p(s(s(n0)), s(s(s(s(s(s(n0))))))) -> true % 60.00/60.40 43: p(n0, s(s(s(s(s(s(s(n0)))))))) -> true % 60.00/60.40 44: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(n0))))) -> true % 60.00/60.40 45: p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(n0)))))) -> true % 60.00/60.40 46: p(s(s(s(s(n0)))), s(s(s(s(s(s(n0))))))) -> true % 60.00/60.40 47: p(s(s(n0)), s(s(s(s(s(s(s(n0)))))))) -> true % 60.00/60.40 48: p(n0, s(s(s(s(s(s(s(s(n0))))))))) -> true % 60.00/60.40 49: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(n0)))))) -> true % 60.00/60.40 50: p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(n0))))))) -> true % 60.00/60.40 51: p(s(s(s(s(n0)))), s(s(s(s(s(s(s(n0)))))))) -> true % 60.00/60.40 52: p(s(s(n0)), s(s(s(s(s(s(s(s(n0))))))))) -> true % 60.00/60.40 53: p(n0, s(s(s(s(s(s(s(s(s(n0)))))))))) -> true % 60.00/60.40 54: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(n0))))))) -> true % 60.00/60.40 55: p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(n0)))))))) -> true % 60.00/60.40 56: p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(n0))))))))) -> true % 60.00/60.40 57: p(s(s(n0)), s(s(s(s(s(s(s(s(s(n0)))))))))) -> true % 60.00/60.40 58: p(n0, s(s(s(s(s(s(s(s(s(s(n0))))))))))) -> true % 60.00/60.40 59: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(n0)))))))) -> true % 60.00/60.40 60: p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(n0))))))))) -> true % 60.00/60.40 61: p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(n0)))))))))) -> true % 60.00/60.40 62: p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(n0))))))))))) -> true % 60.00/60.40 63: p(n0, s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) -> true % 60.00/60.40 64: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(s(n0))))))))) -> true % 60.00/60.40 65: p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(s(n0)))))))))) -> true % 60.00/60.40 66: p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(s(n0))))))))))) -> true % 60.00/60.40 67: p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) -> true % 60.00/60.40 68: p(n0, s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) -> true % 60.00/60.40 69: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(s(s(n0)))))))))) -> true % 60.00/60.40 70: p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(s(s(n0))))))))))) -> true % 60.00/60.40 71: p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) -> true % 60.00/60.40 72: p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) -> true % 60.00/60.40 73: p(n0, s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) -> true % 60.00/60.40 74: p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(s(s(s(n0))))))))))) -> true % 60.00/60.40 75: p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) -> true % 60.00/60.40 76: p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) -> true % 60.00/60.40 77: p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) -> true % 60.00/60.40 78: p(n0, s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))) -> true % 60.00/60.40 79: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), n0), true, true, true) -> true % 60.00/60.40 80: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(n0)), true, true, true) -> true % 60.00/60.40 81: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(n0))), true, true, true) -> true % 60.00/60.40 82: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(n0)))), true, true, true) -> true % 60.00/60.40 83: ifeq(p(n0, s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))), true, true, true) -> true % 60.00/60.40 84: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(n0))))), true, true, true) -> true % 60.00/60.40 85: ifeq(p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))), true, true, true) -> true % 60.00/60.40 86: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(s(n0)))))), true, true, true) -> true % 60.00/60.40 87: ifeq(p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))), true, true, true) -> true % 60.00/60.40 88: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(s(s(n0))))))), true, true, true) -> true % 60.00/60.40 89: ifeq(p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))), true, true, true) -> true % 60.00/60.40 90: ifeq(p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), true, true, true) -> true % 60.00/60.40 91: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(s(s(s(n0)))))))), true, true, true) -> true % 60.00/60.40 92: ifeq(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(s(s(s(s(n0))))))))))), true, true, true) -> true % 60.00/60.40 93: ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(s(s(s(s(n0))))))))), true, true, true) -> true % 60.00/60.40 %------------------------------------------------------------------------------