% This input file causes Otter to find a noncommutative group
% of order 6.  We start with a ground system for a group of
% order 6 and state that two of the elements don't commute.
% We apply splitting, which terminates because a branch cannot
% be refuted.  That branch gives us a model, that is, a
% noncommutative group of order 6.
%
% This method of model search was developed as a possible
% alternative to MACE.

set(knuth_bendix).
set(split_when_given).

clear(print_kept).
clear(print_given).
clear(print_new_demod).
clear(print_back_demod).
clear(print_proofs).

assign(stats_level, 1).

list(usable).
x = x.  % Not necessary.  If omitted, we derive and keep 0=0,1=1,2=2,... .
end_of_list.

list(sos).

0 != 1.   % The six elements 0--5 are distinct.
0 != 2.
0 != 3.
0 != 4.
0 != 5.
1 != 2.
1 != 3.
1 != 4.
1 != 5.
2 != 3.
2 != 4.
2 != 5.
3 != 4.
3 != 5.
4 != 5.

e = 0.             % let 0 be the identity.

f(1,2) != f(2,1).  % 1 and 2 don't commute.

f(e,0)=0.   % instances of f(e,x) = x.
f(e,1)=1.
f(e,2)=2.
f(e,3)=3.
f(e,4)=4.
f(e,5)=5.

f(g(0),0)=e.   % instances of f(g(x),x) = e.
f(g(1),1)=e.
f(g(2),2)=e.
f(g(3),3)=e.
f(g(4),4)=e.
f(g(5),5)=e.

f(f(0,0),0)=f(0,f(0,0)).  % instances of associativity.
f(f(1,1),1)=f(1,f(1,1)).
f(f(1,0),1)=f(1,f(0,1)).
f(f(0,1),1)=f(0,f(1,1)).
f(f(0,0),1)=f(0,f(0,1)).
f(f(1,1),0)=f(1,f(1,0)).
f(f(0,1),0)=f(0,f(1,0)).
f(f(1,0),0)=f(1,f(0,0)).
f(f(2,2),2)=f(2,f(2,2)).
f(f(2,1),2)=f(2,f(1,2)).
f(f(2,0),2)=f(2,f(0,2)).
f(f(1,2),2)=f(1,f(2,2)).
f(f(1,1),2)=f(1,f(1,2)).
f(f(1,0),2)=f(1,f(0,2)).
f(f(0,2),2)=f(0,f(2,2)).
f(f(0,1),2)=f(0,f(1,2)).
f(f(0,0),2)=f(0,f(0,2)).
f(f(2,2),1)=f(2,f(2,1)).
f(f(2,2),0)=f(2,f(2,0)).
f(f(1,2),1)=f(1,f(2,1)).
f(f(1,2),0)=f(1,f(2,0)).
f(f(0,2),1)=f(0,f(2,1)).
f(f(0,2),0)=f(0,f(2,0)).
f(f(2,1),1)=f(2,f(1,1)).
f(f(2,1),0)=f(2,f(1,0)).
f(f(2,0),1)=f(2,f(0,1)).
f(f(2,0),0)=f(2,f(0,0)).
f(f(3,3),3)=f(3,f(3,3)).
f(f(3,2),3)=f(3,f(2,3)).
f(f(3,1),3)=f(3,f(1,3)).
f(f(3,0),3)=f(3,f(0,3)).
f(f(2,3),3)=f(2,f(3,3)).
f(f(2,2),3)=f(2,f(2,3)).
f(f(2,1),3)=f(2,f(1,3)).
f(f(2,0),3)=f(2,f(0,3)).
f(f(1,3),3)=f(1,f(3,3)).
f(f(1,2),3)=f(1,f(2,3)).
f(f(1,1),3)=f(1,f(1,3)).
f(f(1,0),3)=f(1,f(0,3)).
f(f(0,3),3)=f(0,f(3,3)).
f(f(0,2),3)=f(0,f(2,3)).
f(f(0,1),3)=f(0,f(1,3)).
f(f(0,0),3)=f(0,f(0,3)).
f(f(3,3),2)=f(3,f(3,2)).
f(f(3,3),1)=f(3,f(3,1)).
f(f(3,3),0)=f(3,f(3,0)).
f(f(2,3),2)=f(2,f(3,2)).
f(f(2,3),1)=f(2,f(3,1)).
f(f(2,3),0)=f(2,f(3,0)).
f(f(1,3),2)=f(1,f(3,2)).
f(f(1,3),1)=f(1,f(3,1)).
f(f(1,3),0)=f(1,f(3,0)).
f(f(0,3),2)=f(0,f(3,2)).
f(f(0,3),1)=f(0,f(3,1)).
f(f(0,3),0)=f(0,f(3,0)).
f(f(3,2),2)=f(3,f(2,2)).
f(f(3,2),1)=f(3,f(2,1)).
f(f(3,2),0)=f(3,f(2,0)).
f(f(3,1),2)=f(3,f(1,2)).
f(f(3,1),1)=f(3,f(1,1)).
f(f(3,1),0)=f(3,f(1,0)).
f(f(3,0),2)=f(3,f(0,2)).
f(f(3,0),1)=f(3,f(0,1)).
f(f(3,0),0)=f(3,f(0,0)).
f(f(4,4),4)=f(4,f(4,4)).
f(f(4,3),4)=f(4,f(3,4)).
f(f(4,2),4)=f(4,f(2,4)).
f(f(4,1),4)=f(4,f(1,4)).
f(f(4,0),4)=f(4,f(0,4)).
f(f(3,4),4)=f(3,f(4,4)).
f(f(3,3),4)=f(3,f(3,4)).
f(f(3,2),4)=f(3,f(2,4)).
f(f(3,1),4)=f(3,f(1,4)).
f(f(3,0),4)=f(3,f(0,4)).
f(f(2,4),4)=f(2,f(4,4)).
f(f(2,3),4)=f(2,f(3,4)).
f(f(2,2),4)=f(2,f(2,4)).
f(f(2,1),4)=f(2,f(1,4)).
f(f(2,0),4)=f(2,f(0,4)).
f(f(1,4),4)=f(1,f(4,4)).
f(f(1,3),4)=f(1,f(3,4)).
f(f(1,2),4)=f(1,f(2,4)).
f(f(1,1),4)=f(1,f(1,4)).
f(f(1,0),4)=f(1,f(0,4)).
f(f(0,4),4)=f(0,f(4,4)).
f(f(0,3),4)=f(0,f(3,4)).
f(f(0,2),4)=f(0,f(2,4)).
f(f(0,1),4)=f(0,f(1,4)).
f(f(0,0),4)=f(0,f(0,4)).
f(f(4,4),3)=f(4,f(4,3)).
f(f(4,4),2)=f(4,f(4,2)).
f(f(4,4),1)=f(4,f(4,1)).
f(f(4,4),0)=f(4,f(4,0)).
f(f(3,4),3)=f(3,f(4,3)).
f(f(3,4),2)=f(3,f(4,2)).
f(f(3,4),1)=f(3,f(4,1)).
f(f(3,4),0)=f(3,f(4,0)).
f(f(2,4),3)=f(2,f(4,3)).
f(f(2,4),2)=f(2,f(4,2)).
f(f(2,4),1)=f(2,f(4,1)).
f(f(2,4),0)=f(2,f(4,0)).
f(f(1,4),3)=f(1,f(4,3)).
f(f(1,4),2)=f(1,f(4,2)).
f(f(1,4),1)=f(1,f(4,1)).
f(f(1,4),0)=f(1,f(4,0)).
f(f(0,4),3)=f(0,f(4,3)).
f(f(0,4),2)=f(0,f(4,2)).
f(f(0,4),1)=f(0,f(4,1)).
f(f(0,4),0)=f(0,f(4,0)).
f(f(4,3),3)=f(4,f(3,3)).
f(f(4,3),2)=f(4,f(3,2)).
f(f(4,3),1)=f(4,f(3,1)).
f(f(4,3),0)=f(4,f(3,0)).
f(f(4,2),3)=f(4,f(2,3)).
f(f(4,2),2)=f(4,f(2,2)).
f(f(4,2),1)=f(4,f(2,1)).
f(f(4,2),0)=f(4,f(2,0)).
f(f(4,1),3)=f(4,f(1,3)).
f(f(4,1),2)=f(4,f(1,2)).
f(f(4,1),1)=f(4,f(1,1)).
f(f(4,1),0)=f(4,f(1,0)).
f(f(4,0),3)=f(4,f(0,3)).
f(f(4,0),2)=f(4,f(0,2)).
f(f(4,0),1)=f(4,f(0,1)).
f(f(4,0),0)=f(4,f(0,0)).
f(f(5,5),5)=f(5,f(5,5)).
f(f(5,4),5)=f(5,f(4,5)).
f(f(5,3),5)=f(5,f(3,5)).
f(f(5,2),5)=f(5,f(2,5)).
f(f(5,1),5)=f(5,f(1,5)).
f(f(5,0),5)=f(5,f(0,5)).
f(f(4,5),5)=f(4,f(5,5)).
f(f(4,4),5)=f(4,f(4,5)).
f(f(4,3),5)=f(4,f(3,5)).
f(f(4,2),5)=f(4,f(2,5)).
f(f(4,1),5)=f(4,f(1,5)).
f(f(4,0),5)=f(4,f(0,5)).
f(f(3,5),5)=f(3,f(5,5)).
f(f(3,4),5)=f(3,f(4,5)).
f(f(3,3),5)=f(3,f(3,5)).
f(f(3,2),5)=f(3,f(2,5)).
f(f(3,1),5)=f(3,f(1,5)).
f(f(3,0),5)=f(3,f(0,5)).
f(f(2,5),5)=f(2,f(5,5)).
f(f(2,4),5)=f(2,f(4,5)).
f(f(2,3),5)=f(2,f(3,5)).
f(f(2,2),5)=f(2,f(2,5)).
f(f(2,1),5)=f(2,f(1,5)).
f(f(2,0),5)=f(2,f(0,5)).
f(f(1,5),5)=f(1,f(5,5)).
f(f(1,4),5)=f(1,f(4,5)).
f(f(1,3),5)=f(1,f(3,5)).
f(f(1,2),5)=f(1,f(2,5)).
f(f(1,1),5)=f(1,f(1,5)).
f(f(1,0),5)=f(1,f(0,5)).
f(f(0,5),5)=f(0,f(5,5)).
f(f(0,4),5)=f(0,f(4,5)).
f(f(0,3),5)=f(0,f(3,5)).
f(f(0,2),5)=f(0,f(2,5)).
f(f(0,1),5)=f(0,f(1,5)).
f(f(0,0),5)=f(0,f(0,5)).
f(f(5,5),4)=f(5,f(5,4)).
f(f(5,5),3)=f(5,f(5,3)).
f(f(5,5),2)=f(5,f(5,2)).
f(f(5,5),1)=f(5,f(5,1)).
f(f(5,5),0)=f(5,f(5,0)).
f(f(4,5),4)=f(4,f(5,4)).
f(f(4,5),3)=f(4,f(5,3)).
f(f(4,5),2)=f(4,f(5,2)).
f(f(4,5),1)=f(4,f(5,1)).
f(f(4,5),0)=f(4,f(5,0)).
f(f(3,5),4)=f(3,f(5,4)).
f(f(3,5),3)=f(3,f(5,3)).
f(f(3,5),2)=f(3,f(5,2)).
f(f(3,5),1)=f(3,f(5,1)).
f(f(3,5),0)=f(3,f(5,0)).
f(f(2,5),4)=f(2,f(5,4)).
f(f(2,5),3)=f(2,f(5,3)).
f(f(2,5),2)=f(2,f(5,2)).
f(f(2,5),1)=f(2,f(5,1)).
f(f(2,5),0)=f(2,f(5,0)).
f(f(1,5),4)=f(1,f(5,4)).
f(f(1,5),3)=f(1,f(5,3)).
f(f(1,5),2)=f(1,f(5,2)).
f(f(1,5),1)=f(1,f(5,1)).
f(f(1,5),0)=f(1,f(5,0)).
f(f(0,5),4)=f(0,f(5,4)).
f(f(0,5),3)=f(0,f(5,3)).
f(f(0,5),2)=f(0,f(5,2)).
f(f(0,5),1)=f(0,f(5,1)).
f(f(0,5),0)=f(0,f(5,0)).
f(f(5,4),4)=f(5,f(4,4)).
f(f(5,4),3)=f(5,f(4,3)).
f(f(5,4),2)=f(5,f(4,2)).
f(f(5,4),1)=f(5,f(4,1)).
f(f(5,4),0)=f(5,f(4,0)).
f(f(5,3),4)=f(5,f(3,4)).
f(f(5,3),3)=f(5,f(3,3)).
f(f(5,3),2)=f(5,f(3,2)).
f(f(5,3),1)=f(5,f(3,1)).
f(f(5,3),0)=f(5,f(3,0)).
f(f(5,2),4)=f(5,f(2,4)).
f(f(5,2),3)=f(5,f(2,3)).
f(f(5,2),2)=f(5,f(2,2)).
f(f(5,2),1)=f(5,f(2,1)).
f(f(5,2),0)=f(5,f(2,0)).
f(f(5,1),4)=f(5,f(1,4)).
f(f(5,1),3)=f(5,f(1,3)).
f(f(5,1),2)=f(5,f(1,2)).
f(f(5,1),1)=f(5,f(1,1)).
f(f(5,1),0)=f(5,f(1,0)).
f(f(5,0),4)=f(5,f(0,4)).
f(f(5,0),3)=f(5,f(0,3)).
f(f(5,0),2)=f(5,f(0,2)).
f(f(5,0),1)=f(5,f(0,1)).
f(f(5,0),0)=f(5,f(0,0)).

% g is closed.

g(0)=0 | g(0)=1 | g(0)=2 | g(0)=3 | g(0)=4 | g(0)=5.
g(1)=0 | g(1)=1 | g(1)=2 | g(1)=3 | g(1)=4 | g(1)=5.
g(2)=0 | g(2)=1 | g(2)=2 | g(2)=3 | g(2)=4 | g(2)=5.
g(3)=0 | g(3)=1 | g(3)=2 | g(3)=3 | g(3)=4 | g(3)=5.
g(4)=0 | g(4)=1 | g(4)=2 | g(4)=3 | g(4)=4 | g(4)=5.
g(5)=0 | g(5)=1 | g(5)=2 | g(5)=3 | g(5)=4 | g(5)=5.

% f is closed.

f(0,0)=0 | f(0,0)=1 | f(0,0)=2 | f(0,0)=3 | f(0,0)=4 | f(0,0)=5.
f(1,1)=0 | f(1,1)=1 | f(1,1)=2 | f(1,1)=3 | f(1,1)=4 | f(1,1)=5.
f(0,1)=0 | f(0,1)=1 | f(0,1)=2 | f(0,1)=3 | f(0,1)=4 | f(0,1)=5.
f(1,0)=0 | f(1,0)=1 | f(1,0)=2 | f(1,0)=3 | f(1,0)=4 | f(1,0)=5.
f(2,2)=0 | f(2,2)=1 | f(2,2)=2 | f(2,2)=3 | f(2,2)=4 | f(2,2)=5.
f(1,2)=0 | f(1,2)=1 | f(1,2)=2 | f(1,2)=3 | f(1,2)=4 | f(1,2)=5.
f(0,2)=0 | f(0,2)=1 | f(0,2)=2 | f(0,2)=3 | f(0,2)=4 | f(0,2)=5.
f(2,1)=0 | f(2,1)=1 | f(2,1)=2 | f(2,1)=3 | f(2,1)=4 | f(2,1)=5.
f(2,0)=0 | f(2,0)=1 | f(2,0)=2 | f(2,0)=3 | f(2,0)=4 | f(2,0)=5.
f(3,3)=0 | f(3,3)=1 | f(3,3)=2 | f(3,3)=3 | f(3,3)=4 | f(3,3)=5.
f(2,3)=0 | f(2,3)=1 | f(2,3)=2 | f(2,3)=3 | f(2,3)=4 | f(2,3)=5.
f(1,3)=0 | f(1,3)=1 | f(1,3)=2 | f(1,3)=3 | f(1,3)=4 | f(1,3)=5.
f(0,3)=0 | f(0,3)=1 | f(0,3)=2 | f(0,3)=3 | f(0,3)=4 | f(0,3)=5.
f(3,2)=0 | f(3,2)=1 | f(3,2)=2 | f(3,2)=3 | f(3,2)=4 | f(3,2)=5.
f(3,1)=0 | f(3,1)=1 | f(3,1)=2 | f(3,1)=3 | f(3,1)=4 | f(3,1)=5.
f(3,0)=0 | f(3,0)=1 | f(3,0)=2 | f(3,0)=3 | f(3,0)=4 | f(3,0)=5.
f(4,4)=0 | f(4,4)=1 | f(4,4)=2 | f(4,4)=3 | f(4,4)=4 | f(4,4)=5.
f(3,4)=0 | f(3,4)=1 | f(3,4)=2 | f(3,4)=3 | f(3,4)=4 | f(3,4)=5.
f(2,4)=0 | f(2,4)=1 | f(2,4)=2 | f(2,4)=3 | f(2,4)=4 | f(2,4)=5.
f(1,4)=0 | f(1,4)=1 | f(1,4)=2 | f(1,4)=3 | f(1,4)=4 | f(1,4)=5.
f(0,4)=0 | f(0,4)=1 | f(0,4)=2 | f(0,4)=3 | f(0,4)=4 | f(0,4)=5.
f(4,3)=0 | f(4,3)=1 | f(4,3)=2 | f(4,3)=3 | f(4,3)=4 | f(4,3)=5.
f(4,2)=0 | f(4,2)=1 | f(4,2)=2 | f(4,2)=3 | f(4,2)=4 | f(4,2)=5.
f(4,1)=0 | f(4,1)=1 | f(4,1)=2 | f(4,1)=3 | f(4,1)=4 | f(4,1)=5.
f(4,0)=0 | f(4,0)=1 | f(4,0)=2 | f(4,0)=3 | f(4,0)=4 | f(4,0)=5.
f(5,5)=0 | f(5,5)=1 | f(5,5)=2 | f(5,5)=3 | f(5,5)=4 | f(5,5)=5.
f(4,5)=0 | f(4,5)=1 | f(4,5)=2 | f(4,5)=3 | f(4,5)=4 | f(4,5)=5.
f(3,5)=0 | f(3,5)=1 | f(3,5)=2 | f(3,5)=3 | f(3,5)=4 | f(3,5)=5.
f(2,5)=0 | f(2,5)=1 | f(2,5)=2 | f(2,5)=3 | f(2,5)=4 | f(2,5)=5.
f(1,5)=0 | f(1,5)=1 | f(1,5)=2 | f(1,5)=3 | f(1,5)=4 | f(1,5)=5.
f(0,5)=0 | f(0,5)=1 | f(0,5)=2 | f(0,5)=3 | f(0,5)=4 | f(0,5)=5.
f(5,4)=0 | f(5,4)=1 | f(5,4)=2 | f(5,4)=3 | f(5,4)=4 | f(5,4)=5.
f(5,3)=0 | f(5,3)=1 | f(5,3)=2 | f(5,3)=3 | f(5,3)=4 | f(5,3)=5.
f(5,2)=0 | f(5,2)=1 | f(5,2)=2 | f(5,2)=3 | f(5,2)=4 | f(5,2)=5.
f(5,1)=0 | f(5,1)=1 | f(5,1)=2 | f(5,1)=3 | f(5,1)=4 | f(5,1)=5.
f(5,0)=0 | f(5,0)=1 | f(5,0)=2 | f(5,0)=3 | f(5,0)=4 | f(5,0)=5.

end_of_list.