1. trans=( r)(y)(Va((r(, y)A R(y, a)),R(a, a)) 2. sym=(Va)(Vy(R(a, y)+R(y, r)) 3. ref=(V)R(, a) 4. nontriv=(V)(u)R(a, y) Then Itrans, sym, nontriuFref Proof. We now prove that T,S,NI RWe have the following tableaux as Figure??. It is a FVrR( x R(, y) 3yR(e, yI TR(C, d), new d vvy(R(x,y)→R(y,x)) Tvy(R(c,y)→R(y,c) [(R(cd)→Rac y(R(xy)∧R(2)→R(x2 vy2(Rc)AR(2)→R(2 vz(R(cd)∧R(d,2)→RC2) R(cd)∧R(,c)→Rc FR(C d)AR(, a] TR(C,c) FR(c, d) FR(d, el T(R(cd)→R(a.c) Red[⑦R(d Figure 1: The tableau proof tableau proof. It is proved1. trans = (∀x)(∀y)(∀z)((R(x, y) ∧ R(y, z)) → R(x, z)), 2. sym = (∀x)(∀y)(R(x, y) → R(y, x)), 3. ref = (∀x)R(x, x), 4. nontriv = (∀x)(∃y)R(x, y). Then {trans, sym, nontriv} |= ref. Proof. We now prove that {T, S, N} |= R.We have the following tableaux as Figure ??. It is a F∀xR(x, x) F R(c, c), new c T∀x∃yR(x, y) T∃yR(c, y) T R(c, d), new d T∀x∀y(R(x, y) → R(y, x)) T∀y(R(c, y) → R(y, c)) T(R(c, d) → R(d, c)) T∀x∀y∀z(R(x, y) ∧ R(y, z) → R(x, z)) T∀y∀z(R(c, y) ∧ R(y, z) → R(c, z)) T∀z(R(c, d) ∧ R(d, z) → R(c, z)) T R(c, d) ∧ R(d, c) → R(c, c) F R(c, d) ∧ R(d, c) F R(c, d) × F R(d, c) T(R(c, d) → R(d, c)) F R(c, d) × T R(d, c) × T R(c, c) × Figure 1: The tableau proof tableau proof. It is proved. 2