set(auto).


formula_list(usable).
-((all x y (R(x,y) -> R(y,x)))& 
  (all x y (R(x,y)&R(y,x) -> x=y))& 
  (all x y (R(x,y) | R(y,x) | x=y)) -> 
  (exists x all y (x=y))).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] -R(x,y)|R(y,x).
0 [] -R(x1,x2)| -R(x2,x1)|x1=x2.
0 [] R(x3,x4)|R(x4,x3)|x3=x4.
0 [] x5!=$f1(x5).
end_of_list.

...

This ia a non-Horn set with equality.  The strategy 
will be Knuth-Bendix, ordered hyper_res, factoring, 
and unit deleteion, with positive clauses in sos 
and nonpositive clauses in usable.
---------------- PROOF ----------------

1 [] -R(x,y)|R(y,x).
2 [] -R(x,y)| -R(y,x)|x=y.
3 [] x!=$f1(x).
4 [copy,3,flip.1] $f1(x)!=x.
6 [] R(x,y)|R(y,x)|x=y.
8 [hyper,6,1,factor_simp] R(x,y)|y=x.
9 [hyper,6,1,factor_simp] R(x,y)|x=y.
13 [hyper,9,2,8,factor_simp,factor_simp] x=y.
14 [binary,13.1,4.1] $F.

------------ end of proof -------------

----------- times (seconds) -----------
user CPU time          0.37        (0 hr, 0 min, 0 sec)