(VAR x1 x2 x3 x4 ) (RULES trans(trans(x1,x2),x3) -> trans(x1,trans(x2,x3)) trans(refl,x1) -> x1 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 )