The three substitution-of-equals axioms are proved from the four group axioms
and the definition of equality.

1)

===========================  ASSUMPTIONS =============================

R(e,x,x)					# label(unit).
R(i(x),x,e)					# label(inverse).
-R(x,y,u)|-R(y,z,v)|-R(u,z,w)|R(x,v,w)		# label(A1).
-R(x,y,u)|-R(y,z,v)|-R(x,v,w)|R(u,z,w)		# label(A2).
E(x,y) <-> (exists u exists v (R(u,v,x)&R(u,v,y))) # label(eq_def).

============================== GOALS =================================

(E(x,y) & R(x,u,v)) -> R(y,u,v) # label(eq_subst1).

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.03 (+ 0.03) seconds: eq_subst1.
% Length of proof is 15.
% Level of proof is 4.
% Maximum clause weight is 16.
% Given clauses 10.

1 E(x,y) <-> (exists z exists u (R(z,u,x) & R(z,u,y))) # label(eq_def) # label(non_clause).  [assumption].
2 E(x,y) & R(x,z,u) -> R(y,z,u) # label(eq_subst) # label(non_clause) # label(goal).  [goal].
4 -E(x,y) | R(f1(x,y),f2(x,y),x) # label(eq_def).  [clausify(1)].
5 -E(x,y) | R(f1(x,y),f2(x,y),y) # label(eq_def).  [clausify(1)].
6 E(c1,c2) # label(eq_subst).  [deny(2)].
7 R(e,x,x) # label(unit).  [assumption].
9 -R(x,y,z) | -R(y,u,w) | -R(z,u,v5) | R(x,w,v5) # label(A1).  [assumption].
10 -R(x,y,z) | -R(y,u,w) | -R(x,w,v5) | R(z,u,v5) # label(A2).  [assumption].
11 R(c1,c3,c4) # label(eq_subst).  [deny(2)].
12 -R(c2,c3,c4) # label(eq_subst) # answer(eq_subst).  [deny(2)].
15 R(f1(c1,c2),f2(c1,c2),c1).  [resolve(6,a,4,a)].
16 R(f1(c1,c2),f2(c1,c2),c2).  [resolve(6,a,5,a)].
22 -R(e,c1,c2) # answer(eq_subst).  [ur(10,b,11,a,c,7,a,d,12,a)].
31 R(e,c1,c2).  [ur(9,a,7,a,b,15,a,c,16,a)].
32 $F # answer(eq_subst).  [resolve(31,a,22,a)].

============================== end of proof ==========================



2)


===========================  ASSUMPTIONS =============================

R(e,x,x)					# label(unit).
R(i(x),x,e)					# label(inverse).
-R(x,y,u)|-R(y,z,v)|-R(u,z,w)|R(x,v,w)		# label(A1).
-R(x,y,u)|-R(y,z,v)|-R(x,v,w)|R(u,z,w)		# label(A2).
E(x,y) <-> (exists u exists v (R(u,v,x)&R(u,v,y))) # label(eq_def).

============================== GOALS =================================

(E(x,y) & R(u,x,v)) -> R(u,y,v) # label(eq_subst2).

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.06) seconds: eq_subst2.
% Length of proof is 18.
% Level of proof is 4.
% Maximum clause weight is 16.
% Given clauses 12.

1 E(x,y) <-> (exists z exists u (R(z,u,x) & R(z,u,y))) # label(eq_def) # label(non_clause).  [assumption].
2 E(x,y) & R(z,x,u) -> R(z,y,u) # label(eq_subst2) # label(non_clause) # label(goal).  [goal].
4 -E(x,y) | R(f1(x,y),f2(x,y),x) # label(eq_def).  [clausify(1)].
5 -E(x,y) | R(f1(x,y),f2(x,y),y) # label(eq_def).  [clausify(1)].
6 E(c1,c2) # label(eq_subst2).  [deny(2)].
7 R(e,x,x) # label(unit).  [assumption].
8 R(i(x),x,e) # label(inverse).  [assumption].
9 -R(x,y,z) | -R(y,u,w) | -R(z,u,v5) | R(x,w,v5) # label(A1).  [assumption].
10 -R(x,y,z) | -R(y,u,w) | -R(x,w,v5) | R(z,u,v5) # label(A2).  [assumption].
11 R(c3,c1,c4) # label(eq_subst2).  [deny(2)].
12 -R(c3,c2,c4) # label(eq_subst2) # answer(eq_subst2).  [deny(2)].
15 R(f1(c1,c2),f2(c1,c2),c1).  [resolve(6,a,4,a)].
16 R(f1(c1,c2),f2(c1,c2),c2).  [resolve(6,a,5,a)].
17 R(i(i(x)),e,x).  [ur(9,a,8,a,b,8,a,c,7,a)].
28 R(e,c1,c2).  [ur(9,a,7,a,b,15,a,c,16,a)].
41 -R(i(i(c3)),c2,c4) # answer(eq_subst2).  [ur(10,a,17,a,b,7,a,d,12,a)].
48 -R(e,c1,c2) # answer(eq_subst2).  [ur(9,a,17,a,c,11,a,d,41,a)].
49 $F # answer(eq_subst2).  [resolve(48,a,28,a)].

============================== end of proof ==========================


3)


===========================  ASSUMPTIONS =============================

R(e,x,x)					# label(unit).
R(i(x),x,e)					# label(inverse).
-R(x,y,u)|-R(y,z,v)|-R(u,z,w)|R(x,v,w)		# label(A1).
-R(x,y,u)|-R(y,z,v)|-R(x,v,w)|R(u,z,w)		# label(A2).
E(x,y) <-> (exists u exists v (R(u,v,x)&R(u,v,y))) # label(eq_def).

============================== GOALS =================================

(E(x,y) & R(u,v,x)) -> R(u,v,y) # label(eq_subst3).

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds: eq_subst3.
% Length of proof is 15.
% Level of proof is 4.
% Maximum clause weight is 16.
% Given clauses 10.

1 E(x,y) <-> (exists z exists u (R(z,u,x) & R(z,u,y))) # label(eq_def) # label(non_clause).  [assumption].
2 E(x,y) & R(z,u,x) -> R(z,u,y) # label(eq_subst3) # label(non_clause) # label(goal).  [goal].
4 -E(x,y) | R(f1(x,y),f2(x,y),x) # label(eq_def).  [clausify(1)].
5 -E(x,y) | R(f1(x,y),f2(x,y),y) # label(eq_def).  [clausify(1)].
6 E(c1,c2) # label(eq_subst3).  [deny(2)].
7 R(e,x,x) # label(unit).  [assumption].
9 -R(x,y,z) | -R(y,u,w) | -R(z,u,v5) | R(x,w,v5) # label(A1).  [assumption].
10 -R(x,y,z) | -R(y,u,w) | -R(x,w,v5) | R(z,u,v5) # label(A2).  [assumption].
11 R(c3,c4,c1) # label(eq_subst3).  [deny(2)].
12 -R(c3,c4,c2) # label(eq_subst3) # answer(eq_subst3).  [deny(2)].
15 R(f1(c1,c2),f2(c1,c2),c1).  [resolve(6,a,4,a)].
16 R(f1(c1,c2),f2(c1,c2),c2).  [resolve(6,a,5,a)].
22 -R(e,c1,c2) # answer(eq_subst3).  [ur(10,a,7,a,b,11,a,d,12,a)].
29 R(e,c1,c2).  [ur(9,a,7,a,b,15,a,c,16,a)].
30 $F # answer(eq_subst3).  [resolve(29,a,22,a)].

============================== end of proof ==========================