Failures on Equality Theorems 6-10

Theorem EQ-6.

The fragment {B,W,M} of combinatory logic contains fixed point combinators. Otter found a proof, but the settings were different from those used in theorems EQ-1 through EQ-5. The important difference is that the initial set of support consists of the denial only (so that all generated clauses are negative), and paramodulation is allowed into both arguments of equality literals. The following input file causes Otter to find a proof of EQ-6 in about 27 seconds.

set(para_into).
clear(para_from_right).
set(order_eq).
assign(max_mem, 16000).
set(lex_rpo).
clear(print_kept).

lex([B,W,L,M,a(x,x),f(x)]).
lrpo_lr_status([a(x,x)]).

list(usable).
(x = x).
(a(a(a(B,x),y),z) = a(x,a(y,z))).
(a(a(W,x),y) = a(a(x,y),y)).
(a(M,x) = a(x,x)).
end_of_list.

list(sos).
(a(y,f(y)) != a(f(y),a(y,f(y)))) | $Ans(y).
end_of_list.

list(demodulators).
(a(a(a(B,x),y),z) = a(x,a(y,z))).
end_of_list.

Theorem EQ-7.

Rings in which x³=x are commutative. As far as we know, Otter has never found a proof of this theorem, except with highly specialized settings and weight templates. We suspect that with associative-commutative unification, Otter would be able to prove it.

Theorem EQ-8.

The fragment {B,W} of combinatory logic contains fixed point combinators. This theorem is much more difficult than EQ-6, and the strategy above that works for EQ-6 fails for EQ-8. The kernel method [7], which was developed for this type of problem, finds a proof of EQ-8 within a few seconds.

Theorems EQ-9 and EQ-10.

On Moufang identities in nonassociative rings (EQ-9), and on right alternative nonassociative rings (EQ-10). The complicated definitions in these theorems cause terms in the conclusion to be greatly expanded. Otter cannot cope with the complex conclusions, because it likes to focus on simple terms. We also believe that associative-commutative unification would be helpful for these theorems.