(VAR x1 x2 x3 x4 )
(THEORY (AC trans))
(RULES 
  trans(x1,refl)  ->  x1
 congror1(refl)  ->  refl
 congror2(refl)  ->  refl
 trans(congror1(x1),ortrue2)  ->  ortrue2
 trans(congror2(x1),ortrue1)  ->  ortrue1
 trans(orfalse1,x1)  ->  trans(congror2(x1),orfalse1)
 trans(orfalse2,x1)  ->  trans(congror1(x1),orfalse2)
 trans(trans(congror1(x1),congror2(x2)), trans(congror1(x3),congror2(x4)))  ->  trans(congror1(trans(x1,x3)), congror2(trans(x2,x4)))
 trans(ortrue1,x1)  ->  ortrue1
 trans(ortrue2,x1)  ->  ortrue2
)