I ran Prover9 [1] with the following inputs:

1.

-P(i(x, y)) | -P(x) | P(y).
P(i(x,i(y,x))). %RVP
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). %SD

2.

-P(i(x, y)) | -P(x) | P(y).
-P(i(x, y)) | -P(i(y, z)) | P(i(x, z)).
P(i(x,i(y,x))). %RVP
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). %SD

-P(i(x, y)) | -P(i(y, z)) | P(i(x, z)) represents a derivable rule in the first system.  I had the formula P(i(i(x, y), i(i(y, z), i(i(z, u), i(x, u))))) as the goal.  The proof in the 1st system took 7.56 seconds, had 958 givens, generated 835656 formulas, and 23398 formulas kept.  The proof in the 2nd system took 25.72 seconds, had 1450 givens, generated 3835597 formulas, and kept 26067 formulas.  Both proofs took the same number of steps.  The maximum clause weight of the second proof was lower than that of the first proof.  As I understand things, this means that the longest formula of the second proof (excluding parentheses and predicate symbols) was shorter than that of the first proof.  Here's the first proof:

% -------- Comments from original proof --------
% Proof 1 at 7.56 (+ 0.41) seconds.
% Length of proof is 21.
% Level of proof is 10.
% Maximum clause weight is 24.
% Given clauses 958.

1 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))) # label(non_clause) # label(goal).  [goal].
2 -P(i(x,y)) | -P(x) | P(y).  [assumption].
3 P(i(x,i(y,x))).  [assumption].
4 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  [assumption].
5 -P(i(i(c1,c2),i(i(c2,c3),i(i(c3,c4),i(c1,c4))))).  [deny(1)].
6 P(i(x,i(y,i(z,y)))).  [hyper(2,a,3,a,b,3,a)].
7 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).  [hyper(2,a,4,a,b,4,a)].
8 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))).  [hyper(2,a,3,a,b,4,a)].
11 P(i(x,i(y,i(z,i(u,z))))).  [hyper(2,a,3,a,b,6,a)].
23 P(i(i(x,i(i(y,x),z)),i(x,z))).  [hyper(2,a,7,a,b,6,a)].
39 P(i(i(x,i(i(y,i(z,y)),u)),i(x,u))).  [hyper(2,a,7,a,b,11,a)].
43 P(i(i(i(x,i(y,z)),i(i(i(x,y),i(x,z)),u)),i(i(x,i(y,z)),u))).  [hyper(2,a,7,a,b,8,a)].
126 P(i(i(x,y),i(i(z,x),i(z,y)))).  [hyper(2,a,23,a,b,8,a)].
419 P(i(i(i(x,y),z),i(y,z))).  [hyper(2,a,39,a,b,126,a)].
441 P(i(x,i(i(i(y,z),u),i(z,u)))).  [hyper(2,a,3,a,b,419,a)].
876 P(i(i(x,i(y,z)),i(y,i(x,z)))).  [hyper(2,a,43,a,b,441,a)].
1406 P(i(i(x,y),i(i(y,z),i(x,z)))).  [hyper(2,a,876,a,b,126,a)].
2202 P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).  [hyper(2,a,1406,a,b,1406,a)].
2220 P(i(i(x,i(y,z)),i(x,i(i(z,u),i(y,u))))).  [hyper(2,a,126,a,b,1406,a)].
23399 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))).  [hyper(2,a,2202,a,b,2220,a)].
23400 $F.  [resolve(23399,a,5,a)].


Here's the second proof:

% -------- Comments from original proof --------
% Proof 1 at 25.72 (+ 1.89) seconds.
% Length of proof is 21.
% Level of proof is 10.
% Maximum clause weight is 16.
% Given clauses 1450.

1 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))) # label(non_clause) # label(goal).  [goal].
2 -P(i(x,y)) | -P(x) | P(y).  [assumption].
3 -P(i(x,y)) | -P(i(y,z)) | P(i(x,z)).  [assumption].
4 P(i(x,i(y,x))).  [assumption].
5 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  [assumption].
6 -P(i(i(c1,c2),i(i(c2,c3),i(i(c3,c4),i(c1,c4))))).  [deny(1)].
8 P(i(x,i(y,i(z,y)))).  [hyper(2,a,4,a,b,4,a)].
10 P(i(i(x,y),i(i(z,x),i(z,y)))).  [hyper(3,a,4,a,b,5,a)].
14 P(i(i(x,y),i(x,x))).  [hyper(2,a,5,a,b,4,a)].
31 P(i(x,x)).  [hyper(2,a,14,a,b,8,a)].
33 P(i(i(i(x,y),x),i(i(x,y),y))).  [hyper(2,a,5,a,b,31,a)].
146 P(i(x,i(i(x,y),y))).  [hyper(3,a,4,a,b,33,a)].
166 P(i(i(i(x,i(y,x)),z),z)).  [hyper(2,a,33,a,b,8,a)].
190 P(i(i(x,y),i(x,i(i(y,z),z)))).  [hyper(2,a,10,a,b,146,a)].
344 P(i(i(i(x,y),z),i(y,z))).  [hyper(3,a,10,a,b,166,a)].
601 P(i(i(x,i(y,z)),i(y,i(x,z)))).  [hyper(3,a,5,a,b,344,a)].
3542 P(i(i(x,y),i(i(y,z),i(x,z)))).  [hyper(3,a,190,a,b,601,a)].
5634 P(i(i(x,y),i(i(z,i(y,u)),i(z,i(x,u))))).  [hyper(3,a,3542,a,b,10,a)].
5639 P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).  [hyper(2,a,3542,a,b,3542,a)].
26068 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))).  [hyper(3,a,5634,a,b,5639,a)].
26069 $F.  [resolve(26068,a,6,a)].

The above may make it look like derived rules aren't of use.  But I ran another trial looking for proofs of  P(i(i(x, i(y, z)), i(y, i(x, z)))).  For the first system I got the following proof:

% Proof 1 at 0.05 (+ 0.03) seconds.
% Length of proof is 17.
% Level of proof is 7.
% Maximum clause weight is 24.
% Given clauses 75.

1 P(i(i(x,i(y,z)),i(y,i(x,z)))) # label(non_clause) # label(goal).  [goal].
2 -P(i(x,y)) | -P(x) | P(y).  [assumption].
3 P(i(x,i(y,x))).  [assumption].
4 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  [assumption].
5 -P(i(i(c1,i(c2,c3)),i(c2,i(c1,c3)))).  [deny(1)].
6 P(i(x,i(y,i(z,y)))).  [hyper(2,a,3,a,b,3,a)].
7 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).  [hyper(2,a,4,a,b,4,a)].
8 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))).  [hyper(2,a,3,a,b,4,a)].
11 P(i(x,i(y,i(z,i(u,z))))).  [hyper(2,a,3,a,b,6,a)].
23 P(i(i(x,i(i(y,x),z)),i(x,z))).  [hyper(2,a,7,a,b,6,a)].
39 P(i(i(x,i(i(y,i(z,y)),u)),i(x,u))).  [hyper(2,a,7,a,b,11,a)].
43 P(i(i(i(x,i(y,z)),i(i(i(x,y),i(x,z)),u)),i(i(x,i(y,z)),u))).  [hyper(2,a,7,a,b,8,a)].
126 P(i(i(x,y),i(i(z,x),i(z,y)))).  [hyper(2,a,23,a,b,8,a)].
419 P(i(i(i(x,y),z),i(y,z))).  [hyper(2,a,39,a,b,126,a)].
441 P(i(x,i(i(i(y,z),u),i(z,u)))).  [hyper(2,a,3,a,b,419,a)].
876 P(i(i(x,i(y,z)),i(y,i(x,z)))).  [hyper(2,a,43,a,b,441,a)].
877 $F.  [resolve(876,a,5,a)].

For the second system I got the following proof:

% -------- Comments from original proof --------
% Proof 1 at 0.03 (+ 0.01) seconds.
% Length of proof is 15.
% Level of proof is 7.
% Maximum clause weight is 14.
% Given clauses 38.

1 P(i(i(x,i(y,z)),i(y,i(x,z)))) # label(non_clause) # label(goal).  [goal].
2 -P(i(x,y)) | -P(x) | P(y).  [assumption].
3 -P(i(x,y)) | -P(i(y,z)) | P(i(x,z)).  [assumption].
4 P(i(x,i(y,x))).  [assumption].
5 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  [assumption].
6 -P(i(i(c1,i(c2,c3)),i(c2,i(c1,c3)))).  [deny(1)].
8 P(i(x,i(y,i(z,y)))).  [hyper(2,a,4,a,b,4,a)].
10 P(i(i(x,y),i(i(z,x),i(z,y)))).  [hyper(3,a,4,a,b,5,a)].
14 P(i(i(x,y),i(x,x))).  [hyper(2,a,5,a,b,4,a)].
31 P(i(x,x)).  [hyper(2,a,14,a,b,8,a)].
33 P(i(i(i(x,y),x),i(i(x,y),y))).  [hyper(2,a,5,a,b,31,a)].
166 P(i(i(i(x,i(y,x)),z),z)).  [hyper(2,a,33,a,b,8,a)].
344 P(i(i(i(x,y),z),i(y,z))).  [hyper(3,a,10,a,b,166,a)].
601 P(i(i(x,i(y,z)),i(y,i(x,z)))).  [hyper(3,a,5,a,b,344,a)].
602 $F.  [resolve(601,a,6,a)].

Since the second proof here took some 602 formulas in comparison to 877 formulas of the first proof, the second proof has length of 15 in comparison to length 17 of the first proof, the clause weight is 14 in comparison to 24, the given clauses is 38 in comparison to 75, and it took slightly less time this suggest that *sometimes* using derived rules might make it easier for Prover9 to find a proof.

[1] W. McCune, "Prover9 and Mace4", http://www.cs.unm.edu/~mccune/Prover9, 2005-2010.