%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : SYO640-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n005.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 08:40:41 AM UTC 2025 % Result : Satisfiable 0.15s 0.45s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : SYO640-10 : TPTP v9.0.0. Released v7.3.0. % 0.02/0.09 % Command : run_Leo-III %s %d THM % 0.09/0.29 % Computer : n005.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Mon Jul 14 23:02:34 EDT 2025 % 0.09/0.30 % CPUTime : % 0.15/0.45 % SZS status Satisfiable % 0.15/0.45 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 0.15/0.45 1: f(sK2_itmul0_Y2, sK3_itmul0_Y1, sK4_itmul0_Y4) -> true % 0.15/0.45 2: f(sK3_itmul0_Y1, sK2_itmul0_Y2, sK4_itmul0_Y4) -> true % 0.15/0.45 3: ifeq(X, X, Y, Z) -> Y % 0.15/0.45 4: ifeq(f(sK3_itmul0_Y1, sK1_itmul0_Y3, X), true, f(sK3_itmul0_Y1, sK3_itmul0_Y1, X), true) -> true % 0.15/0.45 5: ifeq(f(X, Y, Z), true, ifeq(f(W, X, Z), true, f(W, Y, Z), true), true) -> true % 0.15/0.45 6: ifeq(f(sK1_itmul0_Y3, sK3_itmul0_Y1, X), true, true, true) -> true % 0.15/0.45 7: ifeq(f(X, sK3_itmul0_Y1, sK4_itmul0_Y4), true, f(X, sK2_itmul0_Y2, sK4_itmul0_Y4), true) -> true % 0.15/0.45 8: f(sK2_itmul0_Y2, sK2_itmul0_Y2, sK4_itmul0_Y4) -> true % 0.15/0.45 9: ifeq(f(sK3_itmul0_Y1, sK3_itmul0_Y1, sK4_itmul0_Y4), true, true, true) -> true % 0.15/0.45 10: ifeq(f(X, sK2_itmul0_Y2, sK4_itmul0_Y4), true, f(X, sK3_itmul0_Y1, sK4_itmul0_Y4), true) -> true % 0.15/0.45 11: f(sK3_itmul0_Y1, sK3_itmul0_Y1, sK4_itmul0_Y4) -> true % 0.15/0.45 12: ifeq(f(sK3_itmul0_Y1, sK1_itmul0_Y3, sK4_itmul0_Y4), true, true, true) -> true % 0.15/0.45 13: ifeq(f(sK3_itmul0_Y1, X, sK4_itmul0_Y4), true, f(sK2_itmul0_Y2, X, sK4_itmul0_Y4), true) -> true % 0.15/0.45 14: ifeq(f(sK2_itmul0_Y2, X, sK4_itmul0_Y4), true, f(sK3_itmul0_Y1, X, sK4_itmul0_Y4), true) -> true % 0.15/0.45 15: ifeq(f(sK2_itmul0_Y2, X, sK4_itmul0_Y4), true, f(sK2_itmul0_Y2, X, sK4_itmul0_Y4), true) -> true % 0.15/0.45 16: ifeq(f(X, X, sK4_itmul0_Y4), true, true, true) -> true % 0.15/0.45 17: ifeq(f(X, sK2_itmul0_Y2, sK4_itmul0_Y4), true, f(X, sK2_itmul0_Y2, sK4_itmul0_Y4), true) -> true % 0.15/0.45 18: ifeq(f(sK3_itmul0_Y1, X, sK4_itmul0_Y4), true, f(sK3_itmul0_Y1, X, sK4_itmul0_Y4), true) -> true % 0.15/0.45 19: ifeq(f(X, sK3_itmul0_Y1, sK4_itmul0_Y4), true, f(X, sK3_itmul0_Y1, sK4_itmul0_Y4), true) -> true % 0.15/0.45 20: ifeq(f(X, sK3_itmul0_Y1, sK4_itmul0_Y4), true, ifeq(f(sK2_itmul0_Y2, X, sK4_itmul0_Y4), true, true, true), true) -> true % 0.15/0.45 21: ifeq(f(X, sK2_itmul0_Y2, sK4_itmul0_Y4), true, ifeq(f(sK3_itmul0_Y1, X, sK4_itmul0_Y4), true, true, true), true) -> true % 0.15/0.45 22: ifeq(f(sK1_itmul0_Y3, sK2_itmul0_Y2, sK4_itmul0_Y4), true, true, true) -> true % 0.15/0.45 23: ifeq(f(X, sK3_itmul0_Y1, sK4_itmul0_Y4), true, ifeq(f(sK3_itmul0_Y1, X, sK4_itmul0_Y4), true, true, true), true) -> true % 0.15/0.45 24: ifeq(f(X, sK2_itmul0_Y2, sK4_itmul0_Y4), true, ifeq(f(sK2_itmul0_Y2, X, sK4_itmul0_Y4), true, true, true), true) -> true % 0.15/0.45 %------------------------------------------------------------------------------