Here are some Prover9 proofs showing the triviality of finite models.  

The proofs are very easy.  The difficult part is to find non-trivial
(necessarily  infinite) models.

As I mentioned yesterday, all of them use only one simple idea:
one-to-one implies onto. The trick is to find a suitable binary  
operation that is  cancellative. For example, in the Austin identity

      (((y * y) * y) * x) * (y * z ) = x

the derived binary operation x+y = ((y*y)*y)*x is left cancellative :).
Once Skolemized, Prover9 will easily show the triviality.


****************
Austin Example 1
****************

%% K.A. Skornyakov algebra
%% also due to Bjarni Jonsson, Tarski and others
%% type (2,1,1)
f(x * y) = x.
g(x * y) = y.
%% to prove that the only finite models of these are trivial.
%% if a * b = a * c then g(a*b) = g(a*c) and hence b=c.
%% so the mapping y --> a*y is one-to-one and hence onto.
%% also the solution is unique: Skolemize a*(a/b) = b.
x * (x/y) = y.
%% Now ask prover9 to prove the triviality of the algebra
============================== PROOF =================================
1 x = y # label(non_clause) # label(goal).  [goal].
2 f(x * y) = x.  [assumption].
4 x * (x / y) = y.  [assumption].
5 c2 != c1.  [deny(1)].
6 f(x) = y.  [para(4(a,1),2(a,1,1))].
10 x = y.  [para(6(a,1),6(a,1))].
11 $F.  [resolve(10,a,5,a)].
============================== end of proof ==========================


****************
Austin Example 2
****************

%% Austin varieties with Prover9
%% shortest known Austin identity
%% due to A. KISIELEWICZ, Algebra Universalis 1997
%% to prove that the only finite models of this are trivial.
%% the idea is to find some cancellative binary operation in the clone of *.
%% observe that if ((a * a) * a) * b = ((a * a) * a) * c then b=c.
%% in fact, you can ask Prover9 to prove this.
%% so the mapping y --> ((a * a) * a) * y is one-to-one and hence onto.
%% also the solution is unique: now Skolemize ((x*x)*x)*(x/y) = y
(((y * y) * y) * x) * (y * z ) = x. % KISIELEWICZ's identity
((x * x) * x) * (x / y) = y. % quasigroup property of the derived  
operation ((x * x) * x) * y.
% now to prove the triviality of the model.
============================== PROOF =================================
1 x = y # label(non_clause) # label(goal).  [goal].
2 (((x * x) * x) * y) * (x * z) = y.  [assumption].
3 ((x * x) * x) * (x / y) = y.  [assumption].
4 c1 != c2.  [deny(1)].
5 c2 != c1.  [copy(4),flip(a)].
6 ((((((x * x) * x) * y) * (((x * x) * x) * y)) * (((x * x) * x) * y))  
* z) * y = z.  [para(2(a,1),2(a,1,2))].
7 x / y = y * (x * z).  [para(3(a,1),2(a,1,1)),flip(a)].
33 x / y = y * (z / x).  [para(7(a,2),7(a,2,2))].
40 x / ((y * y) * y) = x.  [para(33(a,2),3(a,1))].
50 x / y = y * z.  [para(33(a,2),6(a,1,1)),rewrite([40(12)]),flip(a)].
64 x = y.  [para(50(a,2),3(a,1)),rewrite([40(3)])].
65 $F.  [resolve(64,a,5,a)].
============================== end of proof ==========================


****************
Austin Example 3
****************

%% Austin varieties with Prover9
%% shortest known Austin identity
%% A. KISIELEWICZ, Algebra Universalis 1997
%% observe that if b * a = c * a then b=c.
%% in fact, you can ask Prover9 to prove this.
%% so the mapping y --> y * a is one-to-one and hence onto.
%% also the solution is unique: Skolemize f(a, b) * a = b in every  
finite model
%% Now ask prover9 to prove the triviality of the (finite) model
y * (y * (y * (x * (z * y)))) = x. % KISIELEWICZ's identity (1997, AU)
f(x, y) * x = y.
============================== PROOF =================================
1 x = y # label(non_clause) # label(goal).  [goal].
2 x * (x * (x * (y * (z * x)))) = y.  [assumption].
3 f(x,y) * x = y.  [assumption].
4 c1 != c2.  [deny(1)].
5 c2 != c1.  [copy(4),flip(a)].
8 x * (x * (x * (y * z))) = y.  [para(3(a,1),2(a,1,2,2,2,2))].
27 x * y = x.  [para(8(a,1),8(a,1,2))].
28 x = y.  [para(8(a,1),8(a,1,2,2,2)),rewrite([27(1),27(1),27(1)])].
29 $F.  [resolve(28,a,5,a)].
============================== end of proof ==========================