(ignored inputs)COMMENT Rules of Fig. 3 and Fig. 4 of \cite{BK08} doi: http://dx.doi.org/10.1007/978-3-540-89439-1_34
Rewrite Rules:
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R,id) -> ?R,
     .(id,?R) -> ?R,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(and(?R,?T),w2) -> .(w2,?T),
     .(?R,c) -> .(c,and(?R,?R)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
Apply Direct Methods...
Inner CPs:
   [ .(?R,?R_1) = .(.(?R,?R_1),id),
     .(?R,?R_2) = .(.(?R,id),?R_2),
     .(?R,and(.(?R_3,?U_3),.(?T_3,?V_3))) = .(.(?R,and(?R_3,?T_3)),and(?U_3,?V_3)),
     .(?R,sub(.(?U_4,?R_4),.(?T_4,?V_4))) = .(.(?R,sub(?R_4,?T_4)),sub(?U_4,?V_4)),
     .(?R,.(w1,?R_5)) = .(.(?R,and(?R_5,?T_5)),w1),
     .(?R,.(w2,?T_6)) = .(.(?R,and(?R_6,?T_6)),w2),
     .(?R,.(c,and(?R_7,?R_7))) = .(.(?R,?R_7),c),
     .(?R,id) = .(.(?R,c),w1),
     .(?R,id) = .(.(?R,c),w2),
     .(?R,.(i,sub(id,and(?R_8,id)))) = .(.(?R,?R_8),i),
     .(?R,.(and(id,?T_9),?R_9)) = .(.(?R,and(.(i,sub(id,?R_9)),?T_9)),e),
     .(?R,.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10)))) = .(.(?R,.(?W_10,and(?R_10,?T_10))),and(?U_10,?V_10)),
     .(?R,.(?W_11,sub(.(?U_11,?R_11),.(?T_11,?V_11)))) = .(.(?R,.(?W_11,sub(?R_11,?T_11))),sub(?U_11,?V_11)),
     .(?R,.(.(?W_12,w1),?R_12)) = .(.(?R,.(?W_12,and(?R_12,?T_12))),w1),
     .(?R,.(.(?W_13,w2),?T_13)) = .(.(?R,.(?W_13,and(?R_13,?T_13))),w2),
     .(?R,and(id,?R_14)) = .(.(?R,and(i,?R_14)),e),
     .(?R,.(?W_15,and(id,?R_15))) = .(.(?R,.(?W_15,and(i,?R_15))),e),
     .(?R,.(.(?W_16,and(id,?T_16)),?R_16)) = .(.(?R,.(?W_16,and(.(i,sub(id,?R_16)),?T_16))),e),
     .(id,and(?U_3,?V_3)) = and(.(id,?U_3),.(id,?V_3)),
     .(and(?R_3,?T_3),id) = and(.(?R_3,id),.(?T_3,id)),
     .(id,sub(?U_4,?V_4)) = sub(.(?U_4,id),.(id,?V_4)),
     .(sub(?R_4,?T_4),id) = sub(.(id,?R_4),.(?T_4,id)),
     .(id,w1) = .(w1,id),
     .(id,w2) = .(w2,id),
     .(and(.(i,id),?T_9),e) = .(and(id,?T_9),id),
     .(and(?R_10,?T_10),and(?U_10,?V_10)) = .(id,and(.(?R_10,?U_10),.(?T_10,?V_10))),
     .(.(?W_10,id),and(?U_10,?V_10)) = .(?W_10,and(.(id,?U_10),.(id,?V_10))),
     .(.(?W_10,and(?R_10,?T_10)),id) = .(?W_10,and(.(?R_10,id),.(?T_10,id))),
     .(and(.(?R_3,?U_3),.(?T_3,?V_3)),and(?U_10,?V_10)) = .(and(?R_3,?T_3),and(.(?U_3,?U_10),.(?V_3,?V_10))),
     .(sub(?R_11,?T_11),sub(?U_11,?V_11)) = .(id,sub(.(?U_11,?R_11),.(?T_11,?V_11))),
     .(.(?W_11,id),sub(?U_11,?V_11)) = .(?W_11,sub(.(?U_11,id),.(id,?V_11))),
     .(.(?W_11,sub(?R_11,?T_11)),id) = .(?W_11,sub(.(id,?R_11),.(?T_11,id))),
     .(sub(.(?U_4,?R_4),.(?T_4,?V_4)),sub(?U_11,?V_11)) = .(sub(?R_4,?T_4),sub(.(?U_11,?U_4),.(?V_4,?V_11))),
     .(and(?R_12,?T_12),w1) = .(.(id,w1),?R_12),
     .(.(?W_12,id),w1) = .(.(?W_12,w1),id),
     .(and(.(?R_3,?U_3),.(?T_3,?V_3)),w1) = .(.(and(?R_3,?T_3),w1),?U_3),
     .(.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),w1) = .(.(.(?W_10,and(?R_10,?T_10)),w1),?U_10),
     .(and(?R_13,?T_13),w2) = .(.(id,w2),?T_13),
     .(.(?W_13,id),w2) = .(.(?W_13,w2),id),
     .(and(.(?R_3,?U_3),.(?T_3,?V_3)),w2) = .(.(and(?R_3,?T_3),w2),?V_3),
     .(.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),w2) = .(.(.(?W_10,and(?R_10,?T_10)),w2),?V_10),
     .(and(i,?R_15),e) = .(id,and(id,?R_15)),
     .(and(.(?R_3,i),.(?T_3,?V_3)),e) = .(and(?R_3,?T_3),and(id,?V_3)),
     .(.(?W_10,and(.(?R_10,i),.(?T_10,?V_10))),e) = .(.(?W_10,and(?R_10,?T_10)),and(id,?V_10)),
     .(and(.(i,sub(id,?R_16)),?T_16),e) = .(.(id,and(id,?T_16)),?R_16),
     .(.(?W_16,and(.(i,id),?T_16)),e) = .(.(?W_16,and(id,?T_16)),id),
     .(and(.(?R_3,.(i,sub(id,?R_16))),.(?T_3,?V_3)),e) = .(.(and(?R_3,?T_3),and(id,?V_3)),?R_16),
     .(.(?W_10,and(.(?R_10,.(i,sub(id,?R_16))),.(?T_10,?V_10))),e) = .(.(.(?W_10,and(?R_10,?T_10)),and(id,?V_10)),?R_16),
     .(?R_1,.(.(?R,?T),?U)) = .(.(?R_1,?R),.(?T,?U)),
     .(.(?W,and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)) = .(.(?W,and(?R,?T)),and(.(?U,?U_1),.(?V,?V_1))),
     .(.(?W,sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)) = .(.(?W,sub(?R,?T)),sub(.(?U_1,?U),.(?V,?V_1))) ]
Outer CPs:
   [ .(.(id,?T),?U) = .(?T,?U),
     id = id,
     c = .(c,and(id,id)),
     i = .(i,sub(id,and(id,id))) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
Left-Linear, not Right-Linear
unknown Development Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ .(.(?R_2,.(?W,and(.(i,sub(id,?R)),?T))),e) = .(?R_2,.(.(?W,and(id,?T)),?R)),
     .(.(?R_2,.(?W,and(.(i,id),?T))),e) = .(?R_2,.(.(?W,and(id,?T)),id)),
     .(.(?R_2,.(?W_14,and(.(?R_14,.(i,sub(id,?R))),.(?T_14,?T)))),e) = .(?R_2,.(.(.(?W_14,and(?R_14,?T_14)),and(id,?T)),?R)),
     .(.(?R_2,and(.(?R_7,.(i,sub(id,?R))),.(?T_7,?T))),e) = .(?R_2,.(.(and(?R_7,?T_7),and(id,?T)),?R)),
     .(.(?R_2,and(.(i,sub(id,?R)),?T)),e) = .(?R_2,.(.(id,and(id,?T)),?R)),
     .(.(?R_2,.(?W_14,and(.(?R_14,.(i,id)),.(?T_14,?T)))),e) = .(?R_2,.(.(.(?W_14,and(?R_14,?T_14)),and(id,?T)),id)),
     .(.(?R_2,and(.(?R_7,.(i,id)),.(?T_7,?T))),e) = .(?R_2,.(.(and(?R_7,?T_7),and(id,?T)),id)),
     .(.(?R_2,and(.(i,id),?T)),e) = .(?R_2,.(.(id,and(id,?T)),id)),
     .(.(?W,and(.(i,id),?T)),e) = .(.(?W,and(id,?T)),id),
     .(.(?W_12,and(.(?R_12,.(i,sub(id,?R))),.(?T_12,?T))),e) = .(.(.(?W_12,and(?R_12,?T_12)),and(id,?T)),?R),
     .(and(.(?R_5,.(i,sub(id,?R))),.(?T_5,?T)),e) = .(.(and(?R_5,?T_5),and(id,?T)),?R),
     .(and(.(i,sub(id,?R)),?T),e) = .(.(id,and(id,?T)),?R),
     .(.(?W_12,and(.(?R_12,.(i,id)),.(?T_12,?T))),e) = .(.(.(?W_12,and(?R_12,?T_12)),and(id,?T)),id),
     .(and(.(?R_5,.(i,id)),.(?T_5,?T)),e) = .(.(and(?R_5,?T_5),and(id,?T)),id),
     .(and(.(i,id),?T),e) = .(.(id,and(id,?T)),id),
     .(.(?R_2,.(?W,and(i,?R))),e) = .(?R_2,.(?W,and(id,?R))),
     .(.(?R_2,.(?W_14,and(.(?R_14,i),.(?T_14,?R)))),e) = .(?R_2,.(.(?W_14,and(?R_14,?T_14)),and(id,?R))),
     .(.(?R_2,and(.(?R_7,i),.(?T_7,?R))),e) = .(?R_2,.(and(?R_7,?T_7),and(id,?R))),
     .(.(?R_2,and(i,?R)),e) = .(?R_2,.(id,and(id,?R))),
     .(.(?W_12,and(.(?R_12,i),.(?T_12,?R))),e) = .(.(?W_12,and(?R_12,?T_12)),and(id,?R)),
     .(and(.(?R_5,i),.(?T_5,?R)),e) = .(and(?R_5,?T_5),and(id,?R)),
     .(and(i,?R),e) = .(id,and(id,?R)),
     .(.(?R_2,and(i,?R)),e) = .(?R_2,and(id,?R)),
     .(.(?R_2,.(?W,and(?R,?T))),w2) = .(?R_2,.(.(?W,w2),?T)),
     .(.(?R_2,.(?W,id)),w2) = .(?R_2,.(.(?W,w2),id)),
     .(.(?R_2,.(?W_14,and(.(?R_14,?R),.(?T_14,?T)))),w2) = .(?R_2,.(.(.(?W_14,and(?R_14,?T_14)),w2),?T)),
     .(.(?R_2,and(.(?R_7,?R),.(?T_7,?T))),w2) = .(?R_2,.(.(and(?R_7,?T_7),w2),?T)),
     .(.(?R_2,and(?R,?T)),w2) = .(?R_2,.(.(id,w2),?T)),
     .(.(?R_2,id),w2) = .(?R_2,.(.(id,w2),id)),
     .(.(?W,id),w2) = .(.(?W,w2),id),
     .(.(?W_12,and(.(?R_12,?R),.(?T_12,?T))),w2) = .(.(.(?W_12,and(?R_12,?T_12)),w2),?T),
     .(and(.(?R_5,?R),.(?T_5,?T)),w2) = .(.(and(?R_5,?T_5),w2),?T),
     .(and(?R,?T),w2) = .(.(id,w2),?T),
     .(id,w2) = .(.(id,w2),id),
     .(.(?R_2,.(?W,and(?R,?T))),w1) = .(?R_2,.(.(?W,w1),?R)),
     .(.(?R_2,.(?W,id)),w1) = .(?R_2,.(.(?W,w1),id)),
     .(.(?R_2,.(?W_14,and(.(?R_14,?R),.(?T_14,?T)))),w1) = .(?R_2,.(.(.(?W_14,and(?R_14,?T_14)),w1),?R)),
     .(.(?R_2,and(.(?R_7,?R),.(?T_7,?T))),w1) = .(?R_2,.(.(and(?R_7,?T_7),w1),?R)),
     .(.(?R_2,and(?R,?T)),w1) = .(?R_2,.(.(id,w1),?R)),
     .(.(?R_2,id),w1) = .(?R_2,.(.(id,w1),id)),
     .(.(?W,id),w1) = .(.(?W,w1),id),
     .(.(?W_12,and(.(?R_12,?R),.(?T_12,?T))),w1) = .(.(.(?W_12,and(?R_12,?T_12)),w1),?R),
     .(and(.(?R_5,?R),.(?T_5,?T)),w1) = .(.(and(?R_5,?T_5),w1),?R),
     .(and(?R,?T),w1) = .(.(id,w1),?R),
     .(id,w1) = .(.(id,w1),id),
     .(.(?R_2,.(?W,sub(?R,?T))),sub(?U,?V)) = .(?R_2,.(?W,sub(.(?U,?R),.(?T,?V)))),
     .(.(?W,sub(?R,?T)),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(?W,sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)),
     .(.(?R_2,.(?W,sub(?R,?T))),id) = .(?R_2,.(?W,sub(.(id,?R),.(?T,id)))),
     .(.(?R_2,.(?W,id)),sub(?U,?V)) = .(?R_2,.(?W,sub(.(?U,id),.(id,?V)))),
     .(.(?R_2,sub(.(?R,?R_8),.(?T_8,?T))),sub(?U,?V)) = .(?R_2,.(sub(?R_8,?T_8),sub(.(?U,?R),.(?T,?V)))),
     .(.(?R_2,sub(?R,?T)),sub(?U,?V)) = .(?R_2,.(id,sub(.(?U,?R),.(?T,?V)))),
     .(.(?R_2,.(?W_3,sub(.(?R,?R_3),.(?T_3,?T)))),sub(?U,?V)) = .(?R_2,.(.(?W_3,sub(?R_3,?T_3)),sub(.(?U,?R),.(?T,?V)))),
     .(.(?W,id),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(?W,sub(.(?U,id),.(id,?V))),sub(?U_1,?V_1)),
     .(sub(.(?R,?R_7),.(?T_7,?T)),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(sub(?R_7,?T_7),sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)),
     .(sub(?R,?T),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(id,sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)),
     .(.(?W_2,sub(.(?R,?R_2),.(?T_2,?T))),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(.(?W_2,sub(?R_2,?T_2)),sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)),
     .(.(?R_2,.(?W,id)),id) = .(?R_2,.(?W,sub(.(id,id),.(id,id)))),
     .(.(?R_2,sub(.(?R,?R_8),.(?T_8,?T))),id) = .(?R_2,.(sub(?R_8,?T_8),sub(.(id,?R),.(?T,id)))),
     .(.(?R_2,sub(?R,?T)),id) = .(?R_2,.(id,sub(.(id,?R),.(?T,id)))),
     .(.(?R_2,id),sub(?U,?V)) = .(?R_2,.(id,sub(.(?U,id),.(id,?V)))),
     .(.(?R_2,.(?W_3,sub(.(?R,?R_3),.(?T_3,?T)))),id) = .(?R_2,.(.(?W_3,sub(?R_3,?T_3)),sub(.(id,?R),.(?T,id)))),
     .(id,sub(.(?U_1,?U),.(?V,?V_1))) = .(.(id,sub(.(?U,id),.(id,?V))),sub(?U_1,?V_1)),
     .(.(?R_2,id),id) = .(?R_2,.(id,sub(.(id,id),.(id,id)))),
     .(sub(.(?R,?R_6),.(?T_6,?T)),sub(?U,?V)) = .(sub(?R_6,?T_6),sub(.(?U,?R),.(?T,?V))),
     .(sub(?R,?T),sub(?U,?V)) = .(id,sub(.(?U,?R),.(?T,?V))),
     .(.(?W_1,sub(.(?R,?R_1),.(?T_1,?T))),sub(?U,?V)) = .(.(?W_1,sub(?R_1,?T_1)),sub(.(?U,?R),.(?T,?V))),
     .(sub(.(?R,?R_6),.(?T_6,?T)),id) = .(sub(?R_6,?T_6),sub(.(id,?R),.(?T,id))),
     .(sub(?R,?T),id) = .(id,sub(.(id,?R),.(?T,id))),
     .(id,sub(?U,?V)) = .(id,sub(.(?U,id),.(id,?V))),
     .(.(?W_1,sub(.(?R,?R_1),.(?T_1,?T))),id) = .(.(?W_1,sub(?R_1,?T_1)),sub(.(id,?R),.(?T,id))),
     .(id,id) = .(id,sub(.(id,id),.(id,id))),
     .(.(.(?W,and(?R,?T)),and(id,?V)),?R_17) = .(.(?W,and(.(?R,.(i,sub(id,?R_17))),.(?T,?V))),e),
     .(.(?W,and(?R,?T)),and(id,?V)) = .(.(?W,and(.(?R,i),.(?T,?V))),e),
     .(.(.(?W,and(?R,?T)),w2),?V) = .(.(?W,and(.(?R,?U),.(?T,?V))),w2),
     .(.(.(?W,and(?R,?T)),w1),?U) = .(.(?W,and(.(?R,?U),.(?T,?V))),w1),
     .(.(?R_2,.(?W,and(?R,?T))),and(?U,?V)) = .(?R_2,.(?W,and(.(?R,?U),.(?T,?V)))),
     .(.(?W,and(?R,?T)),and(.(?U,?U_1),.(?V,?V_1))) = .(.(?W,and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)),
     .(.(.(?W,id),and(id,?V)),?R_17) = .(.(?W,and(.(id,.(i,sub(id,?R_17))),.(id,?V))),e),
     .(.(and(.(?R_22,?R),.(?T_22,?T)),and(id,?V)),?R_17) = .(.(and(?R_22,?T_22),and(.(?R,.(i,sub(id,?R_17))),.(?T,?V))),e),
     .(.(and(?R,?T),and(id,?V)),?R_17) = .(.(id,and(.(?R,.(i,sub(id,?R_17))),.(?T,?V))),e),
     .(.(.(?W_18,and(.(?R_18,?R),.(?T_18,?T))),and(id,?V)),?R_17) = .(.(.(?W_18,and(?R_18,?T_18)),and(.(?R,.(i,sub(id,?R_17))),.(?T,?V))),e),
     .(.(?W,id),and(id,?V)) = .(.(?W,and(.(id,i),.(id,?V))),e),
     .(and(.(?R_5,?R),.(?T_5,?T)),and(id,?V)) = .(.(and(?R_5,?T_5),and(.(?R,i),.(?T,?V))),e),
     .(and(?R,?T),and(id,?V)) = .(.(id,and(.(?R,i),.(?T,?V))),e),
     .(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),and(id,?V)) = .(.(.(?W_1,and(?R_1,?T_1)),and(.(?R,i),.(?T,?V))),e),
     .(.(.(?W,id),w2),?V) = .(.(?W,and(.(id,?U),.(id,?V))),w2),
     .(.(and(.(?R_5,?R),.(?T_5,?T)),w2),?V) = .(.(and(?R_5,?T_5),and(.(?R,?U),.(?T,?V))),w2),
     .(.(and(?R,?T),w2),?V) = .(.(id,and(.(?R,?U),.(?T,?V))),w2),
     .(.(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),w2),?V) = .(.(.(?W_1,and(?R_1,?T_1)),and(.(?R,?U),.(?T,?V))),w2),
     .(.(.(?W,id),w1),?U) = .(.(?W,and(.(id,?U),.(id,?V))),w1),
     .(.(and(.(?R_5,?R),.(?T_5,?T)),w1),?U) = .(.(and(?R_5,?T_5),and(.(?R,?U),.(?T,?V))),w1),
     .(.(and(?R,?T),w1),?U) = .(.(id,and(.(?R,?U),.(?T,?V))),w1),
     .(.(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),w1),?U) = .(.(.(?W_1,and(?R_1,?T_1)),and(.(?R,?U),.(?T,?V))),w1),
     .(.(?R_2,.(?W,and(?R,?T))),id) = .(?R_2,.(?W,and(.(?R,id),.(?T,id)))),
     .(.(?R_2,.(?W,id)),and(?U,?V)) = .(?R_2,.(?W,and(.(id,?U),.(id,?V)))),
     .(.(?R_2,and(.(?R_7,?R),.(?T_7,?T))),and(?U,?V)) = .(?R_2,.(and(?R_7,?T_7),and(.(?R,?U),.(?T,?V)))),
     .(.(?R_2,and(?R,?T)),and(?U,?V)) = .(?R_2,.(id,and(.(?R,?U),.(?T,?V)))),
     .(.(?R_2,.(?W_3,and(.(?R_3,?R),.(?T_3,?T)))),and(?U,?V)) = .(?R_2,.(.(?W_3,and(?R_3,?T_3)),and(.(?R,?U),.(?T,?V)))),
     .(.(?W,id),and(.(?U,?U_1),.(?V,?V_1))) = .(.(?W,and(.(id,?U),.(id,?V))),and(?U_1,?V_1)),
     .(and(.(?R_6,?R),.(?T_6,?T)),and(.(?U,?U_1),.(?V,?V_1))) = .(.(and(?R_6,?T_6),and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)),
     .(and(?R,?T),and(.(?U,?U_1),.(?V,?V_1))) = .(.(id,and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)),
     .(.(?W_2,and(.(?R_2,?R),.(?T_2,?T))),and(.(?U,?U_1),.(?V,?V_1))) = .(.(.(?W_2,and(?R_2,?T_2)),and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)),
     .(.(id,and(id,?V)),?R_17) = .(.(id,and(.(id,.(i,sub(id,?R_17))),.(id,?V))),e),
     .(id,and(id,?V)) = .(.(id,and(.(id,i),.(id,?V))),e),
     .(.(id,w2),?V) = .(.(id,and(.(id,?U),.(id,?V))),w2),
     .(.(id,w1),?U) = .(.(id,and(.(id,?U),.(id,?V))),w1),
     .(.(?R_2,.(?W,id)),id) = .(?R_2,.(?W,and(.(id,id),.(id,id)))),
     .(.(?R_2,and(.(?R_7,?R),.(?T_7,?T))),id) = .(?R_2,.(and(?R_7,?T_7),and(.(?R,id),.(?T,id)))),
     .(.(?R_2,and(?R,?T)),id) = .(?R_2,.(id,and(.(?R,id),.(?T,id)))),
     .(.(?R_2,id),and(?U,?V)) = .(?R_2,.(id,and(.(id,?U),.(id,?V)))),
     .(.(?R_2,.(?W_3,and(.(?R_3,?R),.(?T_3,?T)))),id) = .(?R_2,.(.(?W_3,and(?R_3,?T_3)),and(.(?R,id),.(?T,id)))),
     .(id,and(.(?U,?U_1),.(?V,?V_1))) = .(.(id,and(.(id,?U),.(id,?V))),and(?U_1,?V_1)),
     .(.(?R_2,id),id) = .(?R_2,.(id,and(.(id,id),.(id,id)))),
     .(and(.(?R_5,?R),.(?T_5,?T)),and(?U,?V)) = .(and(?R_5,?T_5),and(.(?R,?U),.(?T,?V))),
     .(and(?R,?T),and(?U,?V)) = .(id,and(.(?R,?U),.(?T,?V))),
     .(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),and(?U,?V)) = .(.(?W_1,and(?R_1,?T_1)),and(.(?R,?U),.(?T,?V))),
     .(and(.(?R_5,?R),.(?T_5,?T)),id) = .(and(?R_5,?T_5),and(.(?R,id),.(?T,id))),
     .(and(?R,?T),id) = .(id,and(.(?R,id),.(?T,id))),
     .(id,and(?U,?V)) = .(id,and(.(id,?U),.(id,?V))),
     .(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),id) = .(.(?W_1,and(?R_1,?T_1)),and(.(?R,id),.(?T,id))),
     .(id,id) = .(id,and(.(id,id),.(id,id))),
     .(.(?R_2,and(.(i,sub(id,?R)),?T)),e) = .(?R_2,.(and(id,?T),?R)),
     .(.(?R_2,and(.(i,id),?T)),e) = .(?R_2,.(and(id,?T),id)),
     .(and(.(i,id),?T),e) = .(and(id,?T),id),
     .(.(?R_2,?R),i) = .(?R_2,.(i,sub(id,and(?R,id)))),
     i = .(i,sub(id,and(id,id))),
     .(.(?R,c),w2) = .(?R,id),
     .(.(?R,c),w1) = .(?R,id),
     .(.(?R_2,?R),c) = .(?R_2,.(c,and(?R,?R))),
     c = .(c,and(id,id)),
     .(.(?R_2,and(?R,?T)),w2) = .(?R_2,.(w2,?T)),
     .(.(?R_2,id),w2) = .(?R_2,.(w2,id)),
     .(id,w2) = .(w2,id),
     .(.(?R_2,and(?R,?T)),w1) = .(?R_2,.(w1,?R)),
     .(.(?R_2,id),w1) = .(?R_2,.(w1,id)),
     .(id,w1) = .(w1,id),
     .(sub(?R,?T),sub(.(?U_12,?U),.(?V,?V_12))) = .(sub(.(?U,?R),.(?T,?V)),sub(?U_12,?V_12)),
     .(.(?R_2,sub(?R,?T)),sub(?U,?V)) = .(?R_2,sub(.(?U,?R),.(?T,?V))),
     .(id,sub(.(?U_12,?U),.(?V,?V_12))) = .(sub(.(?U,id),.(id,?V)),sub(?U_12,?V_12)),
     .(.(?R_2,sub(?R,?T)),id) = .(?R_2,sub(.(id,?R),.(?T,id))),
     .(.(?R_2,id),sub(?U,?V)) = .(?R_2,sub(.(?U,id),.(id,?V))),
     .(.(?R_2,id),id) = .(?R_2,sub(.(id,id),.(id,id))),
     .(sub(?R,?T),id) = sub(.(id,?R),.(?T,id)),
     .(id,sub(?U,?V)) = sub(.(?U,id),.(id,?V)),
     .(id,id) = sub(.(id,id),.(id,id)),
     .(.(and(?R,?T),and(id,?V)),?R_17) = .(and(.(?R,.(i,sub(id,?R_17))),.(?T,?V)),e),
     .(and(?R,?T),and(id,?V)) = .(and(.(?R,i),.(?T,?V)),e),
     .(.(and(?R,?T),w2),?V) = .(and(.(?R,?U),.(?T,?V)),w2),
     .(.(and(?R,?T),w1),?U) = .(and(.(?R,?U),.(?T,?V)),w1),
     .(and(?R,?T),and(.(?U,?U_11),.(?V,?V_11))) = .(and(.(?R,?U),.(?T,?V)),and(?U_11,?V_11)),
     .(.(?R_2,and(?R,?T)),and(?U,?V)) = .(?R_2,and(.(?R,?U),.(?T,?V))),
     .(.(id,and(id,?V)),?R_17) = .(and(.(id,.(i,sub(id,?R_17))),.(id,?V)),e),
     .(id,and(id,?V)) = .(and(.(id,i),.(id,?V)),e),
     .(.(id,w2),?V) = .(and(.(id,?U),.(id,?V)),w2),
     .(.(id,w1),?U) = .(and(.(id,?U),.(id,?V)),w1),
     .(id,and(.(?U,?U_11),.(?V,?V_11))) = .(and(.(id,?U),.(id,?V)),and(?U_11,?V_11)),
     .(.(?R_2,and(?R,?T)),id) = .(?R_2,and(.(?R,id),.(?T,id))),
     .(.(?R_2,id),and(?U,?V)) = .(?R_2,and(.(id,?U),.(id,?V))),
     .(.(?R_2,id),id) = .(?R_2,and(.(id,id),.(id,id))),
     .(and(?R,?T),id) = and(.(?R,id),.(?T,id)),
     .(id,and(?U,?V)) = and(.(id,?U),.(id,?V)),
     .(id,id) = and(.(id,id),.(id,id)),
     .(.(?W_16,and(id,?T_16)),id) = .(.(?W_16,and(.(i,id),?T_16)),e),
     .(?W_11,sub(.(id,?R_11),.(?T_11,id))) = .(.(?W_11,sub(?R_11,?T_11)),id),
     .(?W_11,sub(.(?U_11,id),.(id,?V_11))) = .(.(?W_11,id),sub(?U_11,?V_11)),
     .(and(id,?T_9),id) = .(and(.(i,id),?T_9),e),
     sub(.(id,?R_4),.(?T_4,id)) = .(sub(?R_4,?T_4),id),
     sub(.(?U_4,id),.(id,?V_4)) = .(id,sub(?U_4,?V_4)),
     .(.(?W_13,w2),id) = .(.(?W_13,id),w2),
     .(.(?W_12,w1),id) = .(.(?W_12,id),w1),
     .(?W_10,and(.(?R_10,id),.(?T_10,id))) = .(.(?W_10,and(?R_10,?T_10)),id),
     .(?W_10,and(.(id,?U_10),.(id,?V_10))) = .(.(?W_10,id),and(?U_10,?V_10)),
     .(w2,id) = .(id,w2),
     .(w1,id) = .(id,w1),
     and(.(?R_3,id),.(?T_3,id)) = .(and(?R_3,?T_3),id),
     and(.(id,?U_3),.(id,?V_3)) = .(id,and(?U_3,?V_3)),
     .(.(id,and(id,?T_17)),?R_17) = .(and(.(i,sub(id,?R_17)),?T_17),e),
     .(id,and(id,?R_16)) = .(and(i,?R_16),e),
     .(.(id,w2),?T_14) = .(and(?R_14,?T_14),w2),
     .(.(id,w1),?R_13) = .(and(?R_13,?T_13),w1),
     .(id,sub(.(?U_12,?R_12),.(?T_12,?V_12))) = .(sub(?R_12,?T_12),sub(?U_12,?V_12)),
     .(id,and(.(?R_11,?U_11),.(?T_11,?V_11))) = .(and(?R_11,?T_11),and(?U_11,?V_11)),
     .(.(?R_2,id),?R) = .(?R_2,?R),
     .(i,sub(id,and(id,id))) = i,
     .(c,and(id,id)) = c,
     .(.(id,?T_1),?U_1) = .(?T_1,?U_1),
     .(.(?R_2,?R),id) = .(?R_2,?R),
     id = id,
     .(.(?R_1,?R),.(?T,?U)) = .(?R_1,.(.(?R,?T),?U)),
     .(.(?R_1,?R),.(.(?W_18,and(id,?T_18)),?R_18)) = .(?R_1,.(.(?R,.(?W_18,and(.(i,sub(id,?R_18)),?T_18))),e)),
     .(.(?R_1,?R),.(?W_17,and(id,?R_17))) = .(?R_1,.(.(?R,.(?W_17,and(i,?R_17))),e)),
     .(.(?R_1,?R),and(id,?R_16)) = .(?R_1,.(.(?R,and(i,?R_16)),e)),
     .(.(?R_1,?R),.(.(?W_15,w2),?T_15)) = .(?R_1,.(.(?R,.(?W_15,and(?R_15,?T_15))),w2)),
     .(.(?R_1,?R),.(.(?W_14,w1),?R_14)) = .(?R_1,.(.(?R,.(?W_14,and(?R_14,?T_14))),w1)),
     .(.(?R_1,?R),.(?W_13,sub(.(?U_13,?R_13),.(?T_13,?V_13)))) = .(?R_1,.(.(?R,.(?W_13,sub(?R_13,?T_13))),sub(?U_13,?V_13))),
     .(.(?R_1,?R),.(?W_12,and(.(?R_12,?U_12),.(?T_12,?V_12)))) = .(?R_1,.(.(?R,.(?W_12,and(?R_12,?T_12))),and(?U_12,?V_12))),
     .(.(?R_1,?R),.(and(id,?T_11),?R_11)) = .(?R_1,.(.(?R,and(.(i,sub(id,?R_11)),?T_11)),e)),
     .(.(?R_1,?R),.(i,sub(id,and(?T,id)))) = .(?R_1,.(.(?R,?T),i)),
     .(.(?R_1,?R),id) = .(?R_1,.(.(?R,c),w2)),
     .(.(?R_1,?R),id) = .(?R_1,.(.(?R,c),w1)),
     .(.(?R_1,?R),.(c,and(?T,?T))) = .(?R_1,.(.(?R,?T),c)),
     .(.(?R_1,?R),.(w2,?T_8)) = .(?R_1,.(.(?R,and(?R_8,?T_8)),w2)),
     .(.(?R_1,?R),.(w1,?R_7)) = .(?R_1,.(.(?R,and(?R_7,?T_7)),w1)),
     .(.(?R_1,?R),sub(.(?U_6,?R_6),.(?T_6,?V_6))) = .(?R_1,.(.(?R,sub(?R_6,?T_6)),sub(?U_6,?V_6))),
     .(.(?R_1,?R),and(.(?R_5,?U_5),.(?T_5,?V_5))) = .(?R_1,.(.(?R,and(?R_5,?T_5)),and(?U_5,?V_5))),
     .(.(?R_1,?R),?U) = .(?R_1,.(.(?R,id),?U)),
     .(.(?R_1,?R),?T) = .(?R_1,.(.(?R,?T),id)),
     .(.(?R_1,?R),.(.(?T,?T_2),?U_2)) = .(?R_1,.(.(?R,?T),.(?T_2,?U_2))),
     .(?R,.(.(?W_17,and(id,?T_17)),?R_17)) = .(.(?R,.(?W_17,and(.(i,sub(id,?R_17)),?T_17))),e),
     .(?R,.(?W_16,and(id,?R_16))) = .(.(?R,.(?W_16,and(i,?R_16))),e),
     .(?R,and(id,?R_15)) = .(.(?R,and(i,?R_15)),e),
     .(?R,.(.(?W_14,w2),?T_14)) = .(.(?R,.(?W_14,and(?R_14,?T_14))),w2),
     .(?R,.(.(?W_13,w1),?R_13)) = .(.(?R,.(?W_13,and(?R_13,?T_13))),w1),
     .(?R,.(?W_12,sub(.(?U_12,?R_12),.(?T_12,?V_12)))) = .(.(?R,.(?W_12,sub(?R_12,?T_12))),sub(?U_12,?V_12)),
     .(?R,.(?W_11,and(.(?R_11,?U_11),.(?T_11,?V_11)))) = .(.(?R,.(?W_11,and(?R_11,?T_11))),and(?U_11,?V_11)),
     .(?R,.(and(id,?T_10),?R_10)) = .(.(?R,and(.(i,sub(id,?R_10)),?T_10)),e),
     .(?R,.(i,sub(id,and(?T,id)))) = .(.(?R,?T),i),
     .(?R,id) = .(.(?R,c),w2),
     .(?R,id) = .(.(?R,c),w1),
     .(?R,.(c,and(?T,?T))) = .(.(?R,?T),c),
     .(?R,.(w2,?T_7)) = .(.(?R,and(?R_7,?T_7)),w2),
     .(?R,.(w1,?R_6)) = .(.(?R,and(?R_6,?T_6)),w1),
     .(?R,sub(.(?U_5,?R_5),.(?T_5,?V_5))) = .(.(?R,sub(?R_5,?T_5)),sub(?U_5,?V_5)),
     .(?R,and(.(?R_4,?U_4),.(?T_4,?V_4))) = .(.(?R,and(?R_4,?T_4)),and(?U_4,?V_4)),
     .(?R,?U) = .(.(?R,id),?U),
     .(?R,?T) = .(.(?R,?T),id),
     .(?R,.(.(?T,?T_1),?U_1)) = .(.(?R,?T),.(?T_1,?U_1)),
     .(?T,?U) = .(.(id,?T),?U),
     .(.(?W_17,and(id,?T_17)),?R_17) = .(.(id,.(?W_17,and(.(i,sub(id,?R_17)),?T_17))),e),
     .(?W_16,and(id,?R_16)) = .(.(id,.(?W_16,and(i,?R_16))),e),
     and(id,?R_15) = .(.(id,and(i,?R_15)),e),
     .(.(?W_14,w2),?T_14) = .(.(id,.(?W_14,and(?R_14,?T_14))),w2),
     .(.(?W_13,w1),?R_13) = .(.(id,.(?W_13,and(?R_13,?T_13))),w1),
     .(?W_12,sub(.(?U_12,?R_12),.(?T_12,?V_12))) = .(.(id,.(?W_12,sub(?R_12,?T_12))),sub(?U_12,?V_12)),
     .(?W_11,and(.(?R_11,?U_11),.(?T_11,?V_11))) = .(.(id,.(?W_11,and(?R_11,?T_11))),and(?U_11,?V_11)),
     .(and(id,?T_10),?R_10) = .(.(id,and(.(i,sub(id,?R_10)),?T_10)),e),
     .(i,sub(id,and(?T,id))) = .(.(id,?T),i),
     id = .(.(id,c),w2),
     id = .(.(id,c),w1),
     .(c,and(?T,?T)) = .(.(id,?T),c),
     .(w2,?T_7) = .(.(id,and(?R_7,?T_7)),w2),
     .(w1,?R_6) = .(.(id,and(?R_6,?T_6)),w1),
     sub(.(?U_5,?R_5),.(?T_5,?V_5)) = .(.(id,sub(?R_5,?T_5)),sub(?U_5,?V_5)),
     and(.(?R_4,?U_4),.(?T_4,?V_4)) = .(.(id,and(?R_4,?T_4)),and(?U_4,?V_4)),
     ?U = .(.(id,id),?U),
     ?T = .(.(id,?T),id),
     .(.(?T,?T_1),?U_1) = .(.(id,?T),.(?T_1,?U_1)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <.(?R,?R_1), .(.(?R,?R_1),id)> by Rules <1, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[], [([],1)]>
Critical Pair <.(?R,?R_2), .(.(?R,id),?R_2)> by Rules <2, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[], [([(.,1)],1)]>
Critical Pair <.(?R,and(.(?R_3,?U_3),.(?T_3,?V_3))), .(.(?R,and(?R_3,?T_3)),and(?U_3,?V_3))> by Rules <5, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[], [([],14)]>
Critical Pair <.(?R,sub(.(?U_4,?R_4),.(?T_4,?V_4))), .(.(?R,sub(?R_4,?T_4)),sub(?U_4,?V_4))> by Rules <6, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[], [([],15)]>
Critical Pair <.(?R,.(w1,?R_5)), .(.(?R,and(?R_5,?T_5)),w1)> by Rules <7, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[([],0)], [([],16)]>
Critical Pair <.(?R,.(w2,?T_6)), .(.(?R,and(?R_6,?T_6)),w2)> by Rules <8, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[([],0)], [([],17)]>
Critical Pair <.(?R,.(c,and(?R_7,?R_7))), .(.(?R,?R_7),c)> by Rules <9, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[([],0),([(.,1)],9),([],14)], [([],9)]>
Critical Pair <.(?R,id), .(.(?R,c),w1)> by Rules <10, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[([],1)], [([(.,1)],9),([],16),([(.,1)],10),([],2)]>
Critical Pair <.(?R,id), .(.(?R,c),w2)> by Rules <11, 0> preceded by [(.,2)]
 joinable by a reduction of rules <[([],1)], [([(.,1)],9),([],17),([(.,1)],11),([],2)]>
Critical Pair <.(?R,.(i,sub(id,and(?R_8,id)))), .(.(?R,?R_8),i)> by Rules <12, 0> preceded by [(.,2)]
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ .(?R,id) -> ?R,
     .(id,?R) -> ?R,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(and(?R,?T),w2) -> .(w2,?T),
     .(?R,c) -> .(c,and(?R,?R)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
P:
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))) ]
P: not reversible
failure(Step 1)
STEP: 2 (linear)
S:
   [ .(?R,id) -> ?R,
     .(id,?R) -> ?R,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(and(?R,?T),w2) -> .(w2,?T),
     .(?R,c) -> .(c,and(?R,?R)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
P:
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))) ]
P: not reversible
failure(Step 2)
STEP: 3 (relative)
S:
   [ .(?R,id) -> ?R,
     .(id,?R) -> ?R,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(and(?R,?T),w2) -> .(w2,?T),
     .(?R,c) -> .(c,and(?R,?R)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
P:
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))) ]
P: not reversible
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
check Non-Confluence...Unknown
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R,id) -> ?R,
     .(id,?R) -> ?R,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(and(?R,?T),w2) -> .(w2,?T),
     .(?R,c) -> .(c,and(?R,?R)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
Sort Assignment:
 . : 59*59=>59
 c : =>59
 e : =>59
 i : =>59
 id : =>59
 w1 : =>59
 w2 : =>59
 and : 59*59=>59
 sub : 59*59=>59
maximal types: {59}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R,id) -> ?R,
     .(id,?R) -> ?R,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(and(?R,?T),w2) -> .(w2,?T),
     .(?R,c) -> .(c,and(?R,?R)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R,id) -> ?R,
     .(id,?R) -> ?R,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(and(?R,?T),w2) -> .(w2,?T),
     .(?R,c) -> .(c,and(?R,?R)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
Outside Critical Pair: <.(?T,?U), .(.(id,?T),?U)> by Rules <2, 0>
develop reducts from lhs term...
<{}, .(?T,?U)>
develop reducts from rhs term...
<{2}, .(?T,?U)>
<{}, .(.(id,?T),?U)>
Outside Critical Pair: <id, id> by Rules <2, 1>
develop reducts from lhs term...
<{}, id>
develop reducts from rhs term...
<{}, id>
Outside Critical Pair: <.(c,and(id,id)), c> by Rules <9, 2>
develop reducts from lhs term...
<{3}, .(c,id)>
<{}, .(c,and(id,id))>
develop reducts from rhs term...
<{}, c>
Outside Critical Pair: <.(i,sub(id,and(id,id))), i> by Rules <12, 2>
develop reducts from lhs term...
<{3}, .(i,sub(id,id))>
<{}, .(i,sub(id,and(id,id)))>
develop reducts from rhs term...
<{}, i>
Inside Critical Pair: <.(?R,?R_1), .(.(?R,?R_1),id)> by Rules <1, 0>
develop reducts from lhs term...
<{}, .(?R,?R_1)>
develop reducts from rhs term...
<{1}, .(?R,?R_1)>
<{}, .(.(?R,?R_1),id)>
Inside Critical Pair: <.(?R,?R_2), .(.(?R,id),?R_2)> by Rules <2, 0>
develop reducts from lhs term...
<{}, .(?R,?R_2)>
develop reducts from rhs term...
<{1}, .(?R,?R_2)>
<{}, .(.(?R,id),?R_2)>
Inside Critical Pair: <.(?R,and(.(?R_3,?U_3),.(?T_3,?V_3))), .(.(?R,and(?R_3,?T_3)),and(?U_3,?V_3))> by Rules <5, 0>
develop reducts from lhs term...
<{}, .(?R,and(.(?R_3,?U_3),.(?T_3,?V_3)))>
develop reducts from rhs term...
<{14}, .(?R,and(.(?R_3,?U_3),.(?T_3,?V_3)))>
<{}, .(.(?R,and(?R_3,?T_3)),and(?U_3,?V_3))>
Inside Critical Pair: <.(?R,sub(.(?U_4,?R_4),.(?T_4,?V_4))), .(.(?R,sub(?R_4,?T_4)),sub(?U_4,?V_4))> by Rules <6, 0>
develop reducts from lhs term...
<{}, .(?R,sub(.(?U_4,?R_4),.(?T_4,?V_4)))>
develop reducts from rhs term...
<{15}, .(?R,sub(.(?U_4,?R_4),.(?T_4,?V_4)))>
<{}, .(.(?R,sub(?R_4,?T_4)),sub(?U_4,?V_4))>
Inside Critical Pair: <.(?R,.(w1,?R_5)), .(.(?R,and(?R_5,?T_5)),w1)> by Rules <7, 0>
develop reducts from lhs term...
<{0}, .(.(?R,w1),?R_5)>
<{}, .(?R,.(w1,?R_5))>
develop reducts from rhs term...
<{16}, .(.(?R,w1),?R_5)>
<{}, .(.(?R,and(?R_5,?T_5)),w1)>
Inside Critical Pair: <.(?R,.(w2,?T_6)), .(.(?R,and(?R_6,?T_6)),w2)> by Rules <8, 0>
develop reducts from lhs term...
<{0}, .(.(?R,w2),?T_6)>
<{}, .(?R,.(w2,?T_6))>
develop reducts from rhs term...
<{17}, .(.(?R,w2),?T_6)>
<{}, .(.(?R,and(?R_6,?T_6)),w2)>
Inside Critical Pair: <.(?R,.(c,and(?R_7,?R_7))), .(.(?R,?R_7),c)> by Rules <9, 0>
develop reducts from lhs term...
<{0}, .(.(?R,c),and(?R_7,?R_7))>
<{}, .(?R,.(c,and(?R_7,?R_7)))>
develop reducts from rhs term...
<{9}, .(c,and(.(?R,?R_7),.(?R,?R_7)))>
<{}, .(.(?R,?R_7),c)>
Inside Critical Pair: <.(?R,id), .(.(?R,c),w1)> by Rules <10, 0>
develop reducts from lhs term...
<{1}, ?R>
<{}, .(?R,id)>
develop reducts from rhs term...
<{9}, .(.(c,and(?R,?R)),w1)>
<{}, .(.(?R,c),w1)>
Inside Critical Pair: <.(?R,id), .(.(?R,c),w2)> by Rules <11, 0>
develop reducts from lhs term...
<{1}, ?R>
<{}, .(?R,id)>
develop reducts from rhs term...
<{9}, .(.(c,and(?R,?R)),w2)>
<{}, .(.(?R,c),w2)>
Inside Critical Pair: <.(?R,.(i,sub(id,and(?R_8,id)))), .(.(?R,?R_8),i)> by Rules <12, 0>
develop reducts from lhs term...
<{0}, .(.(?R,i),sub(id,and(?R_8,id)))>
<{}, .(?R,.(i,sub(id,and(?R_8,id))))>
develop reducts from rhs term...
<{12}, .(i,sub(id,and(.(?R,?R_8),id)))>
<{}, .(.(?R,?R_8),i)>
Inside Critical Pair: <.(?R,.(and(id,?T_9),?R_9)), .(.(?R,and(.(i,sub(id,?R_9)),?T_9)),e)> by Rules <13, 0>
develop reducts from lhs term...
<{0}, .(.(?R,and(id,?T_9)),?R_9)>
<{}, .(?R,.(and(id,?T_9),?R_9))>
develop reducts from rhs term...
<{20}, .(.(?R,and(id,?T_9)),?R_9)>
<{}, .(.(?R,and(.(i,sub(id,?R_9)),?T_9)),e)>
Inside Critical Pair: <.(?R,.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10)))), .(.(?R,.(?W_10,and(?R_10,?T_10))),and(?U_10,?V_10))> by Rules <14, 0>
develop reducts from lhs term...
<{0}, .(.(?R,?W_10),and(.(?R_10,?U_10),.(?T_10,?V_10)))>
<{}, .(?R,.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))))>
develop reducts from rhs term...
<{0}, .(.(.(?R,?W_10),and(?R_10,?T_10)),and(?U_10,?V_10))>
<{}, .(.(?R,.(?W_10,and(?R_10,?T_10))),and(?U_10,?V_10))>
Inside Critical Pair: <.(?R,.(?W_11,sub(.(?U_11,?R_11),.(?T_11,?V_11)))), .(.(?R,.(?W_11,sub(?R_11,?T_11))),sub(?U_11,?V_11))> by Rules <15, 0>
develop reducts from lhs term...
<{0}, .(.(?R,?W_11),sub(.(?U_11,?R_11),.(?T_11,?V_11)))>
<{}, .(?R,.(?W_11,sub(.(?U_11,?R_11),.(?T_11,?V_11))))>
develop reducts from rhs term...
<{0}, .(.(.(?R,?W_11),sub(?R_11,?T_11)),sub(?U_11,?V_11))>
<{}, .(.(?R,.(?W_11,sub(?R_11,?T_11))),sub(?U_11,?V_11))>
Inside Critical Pair: <.(?R,.(.(?W_12,w1),?R_12)), .(.(?R,.(?W_12,and(?R_12,?T_12))),w1)> by Rules <16, 0>
develop reducts from lhs term...
<{0}, .(.(?R,.(?W_12,w1)),?R_12)>
<{}, .(?R,.(.(?W_12,w1),?R_12))>
develop reducts from rhs term...
<{0}, .(.(.(?R,?W_12),and(?R_12,?T_12)),w1)>
<{}, .(.(?R,.(?W_12,and(?R_12,?T_12))),w1)>
Inside Critical Pair: <.(?R,.(.(?W_13,w2),?T_13)), .(.(?R,.(?W_13,and(?R_13,?T_13))),w2)> by Rules <17, 0>
develop reducts from lhs term...
<{0}, .(.(?R,.(?W_13,w2)),?T_13)>
<{}, .(?R,.(.(?W_13,w2),?T_13))>
develop reducts from rhs term...
<{0}, .(.(.(?R,?W_13),and(?R_13,?T_13)),w2)>
<{}, .(.(?R,.(?W_13,and(?R_13,?T_13))),w2)>
Inside Critical Pair: <.(?R,and(id,?R_14)), .(.(?R,and(i,?R_14)),e)> by Rules <18, 0>
develop reducts from lhs term...
<{}, .(?R,and(id,?R_14))>
develop reducts from rhs term...
<{19}, .(?R,and(id,?R_14))>
<{}, .(.(?R,and(i,?R_14)),e)>
Inside Critical Pair: <.(?R,.(?W_15,and(id,?R_15))), .(.(?R,.(?W_15,and(i,?R_15))),e)> by Rules <19, 0>
develop reducts from lhs term...
<{0}, .(.(?R,?W_15),and(id,?R_15))>
<{}, .(?R,.(?W_15,and(id,?R_15)))>
develop reducts from rhs term...
<{0}, .(.(.(?R,?W_15),and(i,?R_15)),e)>
<{}, .(.(?R,.(?W_15,and(i,?R_15))),e)>
Inside Critical Pair: <.(?R,.(.(?W_16,and(id,?T_16)),?R_16)), .(.(?R,.(?W_16,and(.(i,sub(id,?R_16)),?T_16))),e)> by Rules <20, 0>
develop reducts from lhs term...
<{0}, .(.(?R,.(?W_16,and(id,?T_16))),?R_16)>
<{}, .(?R,.(.(?W_16,and(id,?T_16)),?R_16))>
develop reducts from rhs term...
<{0}, .(.(.(?R,?W_16),and(.(i,sub(id,?R_16)),?T_16)),e)>
<{}, .(.(?R,.(?W_16,and(.(i,sub(id,?R_16)),?T_16))),e)>
Inside Critical Pair: <.(id,and(?U_3,?V_3)), and(.(id,?U_3),.(id,?V_3))> by Rules <3, 5>
develop reducts from lhs term...
<{2}, and(?U_3,?V_3)>
<{}, .(id,and(?U_3,?V_3))>
develop reducts from rhs term...
<{2}, and(?U_3,?V_3)>
<{2}, and(?U_3,.(id,?V_3))>
<{2}, and(.(id,?U_3),?V_3)>
<{}, and(.(id,?U_3),.(id,?V_3))>
Inside Critical Pair: <.(and(?R_3,?T_3),id), and(.(?R_3,id),.(?T_3,id))> by Rules <3, 5>
develop reducts from lhs term...
<{1}, and(?R_3,?T_3)>
<{}, .(and(?R_3,?T_3),id)>
develop reducts from rhs term...
<{1}, and(?R_3,?T_3)>
<{1}, and(?R_3,.(?T_3,id))>
<{1}, and(.(?R_3,id),?T_3)>
<{}, and(.(?R_3,id),.(?T_3,id))>
Inside Critical Pair: <.(id,sub(?U_4,?V_4)), sub(.(?U_4,id),.(id,?V_4))> by Rules <4, 6>
develop reducts from lhs term...
<{2}, sub(?U_4,?V_4)>
<{}, .(id,sub(?U_4,?V_4))>
develop reducts from rhs term...
<{1,2}, sub(?U_4,?V_4)>
<{1}, sub(?U_4,.(id,?V_4))>
<{2}, sub(.(?U_4,id),?V_4)>
<{}, sub(.(?U_4,id),.(id,?V_4))>
Inside Critical Pair: <.(sub(?R_4,?T_4),id), sub(.(id,?R_4),.(?T_4,id))> by Rules <4, 6>
develop reducts from lhs term...
<{1}, sub(?R_4,?T_4)>
<{}, .(sub(?R_4,?T_4),id)>
develop reducts from rhs term...
<{1,2}, sub(?R_4,?T_4)>
<{2}, sub(?R_4,.(?T_4,id))>
<{1}, sub(.(id,?R_4),?T_4)>
<{}, sub(.(id,?R_4),.(?T_4,id))>
Inside Critical Pair: <.(id,w1), .(w1,id)> by Rules <3, 7>
develop reducts from lhs term...
<{2}, w1>
<{}, .(id,w1)>
develop reducts from rhs term...
<{1}, w1>
<{}, .(w1,id)>
Inside Critical Pair: <.(id,w2), .(w2,id)> by Rules <3, 8>
develop reducts from lhs term...
<{2}, w2>
<{}, .(id,w2)>
develop reducts from rhs term...
<{1}, w2>
<{}, .(w2,id)>
Inside Critical Pair: <.(and(.(i,id),?T_9),e), .(and(id,?T_9),id)> by Rules <4, 13>
develop reducts from lhs term...
<{1}, .(and(i,?T_9),e)>
<{}, .(and(.(i,id),?T_9),e)>
develop reducts from rhs term...
<{1}, and(id,?T_9)>
<{}, .(and(id,?T_9),id)>
Inside Critical Pair: <.(and(?R_10,?T_10),and(?U_10,?V_10)), .(id,and(.(?R_10,?U_10),.(?T_10,?V_10)))> by Rules <2, 14>
develop reducts from lhs term...
<{5}, and(.(?R_10,?U_10),.(?T_10,?V_10))>
<{}, .(and(?R_10,?T_10),and(?U_10,?V_10))>
develop reducts from rhs term...
<{2}, and(.(?R_10,?U_10),.(?T_10,?V_10))>
<{}, .(id,and(.(?R_10,?U_10),.(?T_10,?V_10)))>
Inside Critical Pair: <.(.(?W_10,id),and(?U_10,?V_10)), .(?W_10,and(.(id,?U_10),.(id,?V_10)))> by Rules <3, 14>
develop reducts from lhs term...
<{1}, .(?W_10,and(?U_10,?V_10))>
<{}, .(.(?W_10,id),and(?U_10,?V_10))>
develop reducts from rhs term...
<{2}, .(?W_10,and(?U_10,?V_10))>
<{2}, .(?W_10,and(?U_10,.(id,?V_10)))>
<{2}, .(?W_10,and(.(id,?U_10),?V_10))>
<{}, .(?W_10,and(.(id,?U_10),.(id,?V_10)))>
Inside Critical Pair: <.(.(?W_10,and(?R_10,?T_10)),id), .(?W_10,and(.(?R_10,id),.(?T_10,id)))> by Rules <3, 14>
develop reducts from lhs term...
<{1}, .(?W_10,and(?R_10,?T_10))>
<{}, .(.(?W_10,and(?R_10,?T_10)),id)>
develop reducts from rhs term...
<{1}, .(?W_10,and(?R_10,?T_10))>
<{1}, .(?W_10,and(?R_10,.(?T_10,id)))>
<{1}, .(?W_10,and(.(?R_10,id),?T_10))>
<{}, .(?W_10,and(.(?R_10,id),.(?T_10,id)))>
Inside Critical Pair: <.(and(.(?R_3,?U_3),.(?T_3,?V_3)),and(?U_10,?V_10)), .(and(?R_3,?T_3),and(.(?U_3,?U_10),.(?V_3,?V_10)))> by Rules <5, 14>
develop reducts from lhs term...
<{5}, and(.(.(?R_3,?U_3),?U_10),.(.(?T_3,?V_3),?V_10))>
<{}, .(and(.(?R_3,?U_3),.(?T_3,?V_3)),and(?U_10,?V_10))>
develop reducts from rhs term...
<{5}, and(.(?R_3,.(?U_3,?U_10)),.(?T_3,.(?V_3,?V_10)))>
<{}, .(and(?R_3,?T_3),and(.(?U_3,?U_10),.(?V_3,?V_10)))>
Inside Critical Pair: <.(sub(?R_11,?T_11),sub(?U_11,?V_11)), .(id,sub(.(?U_11,?R_11),.(?T_11,?V_11)))> by Rules <2, 15>
develop reducts from lhs term...
<{6}, sub(.(?U_11,?R_11),.(?T_11,?V_11))>
<{}, .(sub(?R_11,?T_11),sub(?U_11,?V_11))>
develop reducts from rhs term...
<{2}, sub(.(?U_11,?R_11),.(?T_11,?V_11))>
<{}, .(id,sub(.(?U_11,?R_11),.(?T_11,?V_11)))>
Inside Critical Pair: <.(.(?W_11,id),sub(?U_11,?V_11)), .(?W_11,sub(.(?U_11,id),.(id,?V_11)))> by Rules <4, 15>
develop reducts from lhs term...
<{1}, .(?W_11,sub(?U_11,?V_11))>
<{}, .(.(?W_11,id),sub(?U_11,?V_11))>
develop reducts from rhs term...
<{1,2}, .(?W_11,sub(?U_11,?V_11))>
<{1}, .(?W_11,sub(?U_11,.(id,?V_11)))>
<{2}, .(?W_11,sub(.(?U_11,id),?V_11))>
<{}, .(?W_11,sub(.(?U_11,id),.(id,?V_11)))>
Inside Critical Pair: <.(.(?W_11,sub(?R_11,?T_11)),id), .(?W_11,sub(.(id,?R_11),.(?T_11,id)))> by Rules <4, 15>
develop reducts from lhs term...
<{1}, .(?W_11,sub(?R_11,?T_11))>
<{}, .(.(?W_11,sub(?R_11,?T_11)),id)>
develop reducts from rhs term...
<{1,2}, .(?W_11,sub(?R_11,?T_11))>
<{2}, .(?W_11,sub(?R_11,.(?T_11,id)))>
<{1}, .(?W_11,sub(.(id,?R_11),?T_11))>
<{}, .(?W_11,sub(.(id,?R_11),.(?T_11,id)))>
Inside Critical Pair: <.(sub(.(?U_4,?R_4),.(?T_4,?V_4)),sub(?U_11,?V_11)), .(sub(?R_4,?T_4),sub(.(?U_11,?U_4),.(?V_4,?V_11)))> by Rules <6, 15>
develop reducts from lhs term...
<{6}, sub(.(?U_11,.(?U_4,?R_4)),.(.(?T_4,?V_4),?V_11))>
<{}, .(sub(.(?U_4,?R_4),.(?T_4,?V_4)),sub(?U_11,?V_11))>
develop reducts from rhs term...
<{6}, sub(.(.(?U_11,?U_4),?R_4),.(?T_4,.(?V_4,?V_11)))>
<{}, .(sub(?R_4,?T_4),sub(.(?U_11,?U_4),.(?V_4,?V_11)))>
Inside Critical Pair: <.(and(?R_12,?T_12),w1), .(.(id,w1),?R_12)> by Rules <2, 16>
develop reducts from lhs term...
<{7}, .(w1,?R_12)>
<{}, .(and(?R_12,?T_12),w1)>
develop reducts from rhs term...
<{2}, .(w1,?R_12)>
<{}, .(.(id,w1),?R_12)>
Inside Critical Pair: <.(.(?W_12,id),w1), .(.(?W_12,w1),id)> by Rules <3, 16>
develop reducts from lhs term...
<{1}, .(?W_12,w1)>
<{}, .(.(?W_12,id),w1)>
develop reducts from rhs term...
<{1}, .(?W_12,w1)>
<{}, .(.(?W_12,w1),id)>
Inside Critical Pair: <.(and(.(?R_3,?U_3),.(?T_3,?V_3)),w1), .(.(and(?R_3,?T_3),w1),?U_3)> by Rules <5, 16>
develop reducts from lhs term...
<{7}, .(w1,.(?R_3,?U_3))>
<{}, .(and(.(?R_3,?U_3),.(?T_3,?V_3)),w1)>
develop reducts from rhs term...
<{7}, .(.(w1,?R_3),?U_3)>
<{}, .(.(and(?R_3,?T_3),w1),?U_3)>
Inside Critical Pair: <.(.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),w1), .(.(.(?W_10,and(?R_10,?T_10)),w1),?U_10)> by Rules <14, 16>
develop reducts from lhs term...
<{16}, .(.(?W_10,w1),.(?R_10,?U_10))>
<{}, .(.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),w1)>
develop reducts from rhs term...
<{16}, .(.(.(?W_10,w1),?R_10),?U_10)>
<{}, .(.(.(?W_10,and(?R_10,?T_10)),w1),?U_10)>
Inside Critical Pair: <.(and(?R_13,?T_13),w2), .(.(id,w2),?T_13)> by Rules <2, 17>
develop reducts from lhs term...
<{8}, .(w2,?T_13)>
<{}, .(and(?R_13,?T_13),w2)>
develop reducts from rhs term...
<{2}, .(w2,?T_13)>
<{}, .(.(id,w2),?T_13)>
Inside Critical Pair: <.(.(?W_13,id),w2), .(.(?W_13,w2),id)> by Rules <3, 17>
develop reducts from lhs term...
<{1}, .(?W_13,w2)>
<{}, .(.(?W_13,id),w2)>
develop reducts from rhs term...
<{1}, .(?W_13,w2)>
<{}, .(.(?W_13,w2),id)>
Inside Critical Pair: <.(and(.(?R_3,?U_3),.(?T_3,?V_3)),w2), .(.(and(?R_3,?T_3),w2),?V_3)> by Rules <5, 17>
develop reducts from lhs term...
<{8}, .(w2,.(?T_3,?V_3))>
<{}, .(and(.(?R_3,?U_3),.(?T_3,?V_3)),w2)>
develop reducts from rhs term...
<{8}, .(.(w2,?T_3),?V_3)>
<{}, .(.(and(?R_3,?T_3),w2),?V_3)>
Inside Critical Pair: <.(.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),w2), .(.(.(?W_10,and(?R_10,?T_10)),w2),?V_10)> by Rules <14, 17>
develop reducts from lhs term...
<{17}, .(.(?W_10,w2),.(?T_10,?V_10))>
<{}, .(.(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),w2)>
develop reducts from rhs term...
<{17}, .(.(.(?W_10,w2),?T_10),?V_10)>
<{}, .(.(.(?W_10,and(?R_10,?T_10)),w2),?V_10)>
Inside Critical Pair: <.(and(i,?R_15),e), .(id,and(id,?R_15))> by Rules <2, 19>
develop reducts from lhs term...
<{18}, and(id,?R_15)>
<{}, .(and(i,?R_15),e)>
develop reducts from rhs term...
<{2}, and(id,?R_15)>
<{}, .(id,and(id,?R_15))>
Inside Critical Pair: <.(and(.(?R_3,i),.(?T_3,?V_3)),e), .(and(?R_3,?T_3),and(id,?V_3))> by Rules <5, 19>
develop reducts from lhs term...
<{12}, .(and(.(i,sub(id,and(?R_3,id))),.(?T_3,?V_3)),e)>
<{}, .(and(.(?R_3,i),.(?T_3,?V_3)),e)>
develop reducts from rhs term...
<{5}, and(.(?R_3,id),.(?T_3,?V_3))>
<{}, .(and(?R_3,?T_3),and(id,?V_3))>
Inside Critical Pair: <.(.(?W_10,and(.(?R_10,i),.(?T_10,?V_10))),e), .(.(?W_10,and(?R_10,?T_10)),and(id,?V_10))> by Rules <14, 19>
develop reducts from lhs term...
<{12}, .(.(?W_10,and(.(i,sub(id,and(?R_10,id))),.(?T_10,?V_10))),e)>
<{}, .(.(?W_10,and(.(?R_10,i),.(?T_10,?V_10))),e)>
develop reducts from rhs term...
<{14}, .(?W_10,and(.(?R_10,id),.(?T_10,?V_10)))>
<{}, .(.(?W_10,and(?R_10,?T_10)),and(id,?V_10))>
Inside Critical Pair: <.(and(.(i,sub(id,?R_16)),?T_16),e), .(.(id,and(id,?T_16)),?R_16)> by Rules <2, 20>
develop reducts from lhs term...
<{13}, .(and(id,?T_16),?R_16)>
<{}, .(and(.(i,sub(id,?R_16)),?T_16),e)>
develop reducts from rhs term...
<{2}, .(and(id,?T_16),?R_16)>
<{}, .(.(id,and(id,?T_16)),?R_16)>
Inside Critical Pair: <.(.(?W_16,and(.(i,id),?T_16)),e), .(.(?W_16,and(id,?T_16)),id)> by Rules <4, 20>
develop reducts from lhs term...
<{1}, .(.(?W_16,and(i,?T_16)),e)>
<{}, .(.(?W_16,and(.(i,id),?T_16)),e)>
develop reducts from rhs term...
<{1}, .(?W_16,and(id,?T_16))>
<{}, .(.(?W_16,and(id,?T_16)),id)>
Inside Critical Pair: <.(and(.(?R_3,.(i,sub(id,?R_16))),.(?T_3,?V_3)),e), .(.(and(?R_3,?T_3),and(id,?V_3)),?R_16)> by Rules <5, 20>
develop reducts from lhs term...
<{0}, .(and(.(.(?R_3,i),sub(id,?R_16)),.(?T_3,?V_3)),e)>
<{}, .(and(.(?R_3,.(i,sub(id,?R_16))),.(?T_3,?V_3)),e)>
develop reducts from rhs term...
<{5}, .(and(.(?R_3,id),.(?T_3,?V_3)),?R_16)>
<{}, .(.(and(?R_3,?T_3),and(id,?V_3)),?R_16)>
Inside Critical Pair: <.(.(?W_10,and(.(?R_10,.(i,sub(id,?R_16))),.(?T_10,?V_10))),e), .(.(.(?W_10,and(?R_10,?T_10)),and(id,?V_10)),?R_16)> by Rules <14, 20>
develop reducts from lhs term...
<{0}, .(.(?W_10,and(.(.(?R_10,i),sub(id,?R_16)),.(?T_10,?V_10))),e)>
<{}, .(.(?W_10,and(.(?R_10,.(i,sub(id,?R_16))),.(?T_10,?V_10))),e)>
develop reducts from rhs term...
<{14}, .(.(?W_10,and(.(?R_10,id),.(?T_10,?V_10))),?R_16)>
<{}, .(.(.(?W_10,and(?R_10,?T_10)),and(id,?V_10)),?R_16)>
Try A Minimal Decomposition {4,3,20,19,18,17,16,15,14,13,11,10,8,7,6,5,0,12,2,9}{1}
{4,3,20,19,18,17,16,15,14,13,11,10,8,7,6,5,0,12,2,9}
(cm)Rewrite Rules:
   [ sub(id,id) -> id,
     and(id,id) -> id,
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(c,w2) -> id,
     .(c,w1) -> id,
     .(and(?R,?T),w2) -> .(w2,?T),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(id,?R) -> ?R,
     .(?R,c) -> .(c,and(?R,?R)) ]
Apply Direct Methods...
Inner CPs:
   [ .(.(?W,and(.(i,id),?T)),e) = .(.(?W,and(id,?T)),id),
     .(.(?W_6,and(.(?R_6,.(i,sub(id,?R))),.(?T_6,?V_6))),e) = .(.(.(?W_6,and(?R_6,?T_6)),and(id,?V_6)),?R),
     .(and(.(?R_11,.(i,sub(id,?R))),.(?T_11,?V_11)),e) = .(.(and(?R_11,?T_11),and(id,?V_11)),?R),
     .(and(.(i,sub(id,?R)),?T),e) = .(.(id,and(id,?T)),?R),
     .(.(?W_6,and(.(?R_6,i),.(?T_6,?V_6))),e) = .(.(?W_6,and(?R_6,?T_6)),and(id,?V_6)),
     .(and(.(?R_11,i),.(?T_11,?V_11)),e) = .(and(?R_11,?T_11),and(id,?V_11)),
     .(and(i,?R_1),e) = .(id,and(id,?R_1)),
     .(.(?W_3,id),w2) = .(.(?W_3,w2),id),
     .(.(?W_6,and(.(?R_6,?U_6),.(?T_6,?V_6))),w2) = .(.(.(?W_6,and(?R_6,?T_6)),w2),?V_6),
     .(and(.(?R_11,?U_11),.(?T_11,?V_11)),w2) = .(.(and(?R_11,?T_11),w2),?V_11),
     .(and(?R_3,?T_3),w2) = .(.(id,w2),?T_3),
     .(.(?W_4,id),w1) = .(.(?W_4,w1),id),
     .(.(?W_6,and(.(?R_6,?U_6),.(?T_6,?V_6))),w1) = .(.(.(?W_6,and(?R_6,?T_6)),w1),?U_6),
     .(and(.(?R_11,?U_11),.(?T_11,?V_11)),w1) = .(.(and(?R_11,?T_11),w1),?U_11),
     .(and(?R_4,?T_4),w1) = .(.(id,w1),?R_4),
     .(.(?W_5,id),sub(?U_5,?V_5)) = .(?W_5,sub(.(?U_5,id),.(id,?V_5))),
     .(.(?W_5,sub(?R_5,?T_5)),id) = .(?W_5,sub(.(id,?R_5),.(?T_5,id))),
     .(sub(.(?U_10,?R_10),.(?T_10,?V_10)),sub(?U_5,?V_5)) = .(sub(?R_10,?T_10),sub(.(?U_5,?U_10),.(?V_10,?V_5))),
     .(sub(?R_5,?T_5),sub(?U_5,?V_5)) = .(id,sub(.(?U_5,?R_5),.(?T_5,?V_5))),
     .(.(?W_6,id),and(?U_6,?V_6)) = .(?W_6,and(.(id,?U_6),.(id,?V_6))),
     .(.(?W_6,and(?R_6,?T_6)),id) = .(?W_6,and(.(?R_6,id),.(?T_6,id))),
     .(and(.(?R_11,?U_11),.(?T_11,?V_11)),and(?U_6,?V_6)) = .(and(?R_11,?T_11),and(.(?U_11,?U_6),.(?V_11,?V_6))),
     .(and(?R_6,?T_6),and(?U_6,?V_6)) = .(id,and(.(?R_6,?U_6),.(?T_6,?V_6))),
     .(and(.(i,id),?T_7),e) = .(and(id,?T_7),id),
     .(id,w2) = .(w2,id),
     .(id,w1) = .(w1,id),
     .(id,sub(?U_10,?V_10)) = sub(.(?U_10,id),.(id,?V_10)),
     .(sub(?R_10,?T_10),id) = sub(.(id,?R_10),.(?T_10,id)),
     .(id,and(?U_11,?V_11)) = and(.(id,?U_11),.(id,?V_11)),
     .(and(?R_11,?T_11),id) = and(.(?R_11,id),.(?T_11,id)),
     .(?R_12,.(.(?W,and(id,?T)),?R)) = .(.(?R_12,.(?W,and(.(i,sub(id,?R)),?T))),e),
     .(?R_12,.(?W_1,and(id,?R_1))) = .(.(?R_12,.(?W_1,and(i,?R_1))),e),
     .(?R_12,and(id,?R_2)) = .(.(?R_12,and(i,?R_2)),e),
     .(?R_12,.(.(?W_3,w2),?T_3)) = .(.(?R_12,.(?W_3,and(?R_3,?T_3))),w2),
     .(?R_12,.(.(?W_4,w1),?R_4)) = .(.(?R_12,.(?W_4,and(?R_4,?T_4))),w1),
     .(?R_12,.(?W_5,sub(.(?U_5,?R_5),.(?T_5,?V_5)))) = .(.(?R_12,.(?W_5,sub(?R_5,?T_5))),sub(?U_5,?V_5)),
     .(?R_12,.(?W_6,and(.(?R_6,?U_6),.(?T_6,?V_6)))) = .(.(?R_12,.(?W_6,and(?R_6,?T_6))),and(?U_6,?V_6)),
     .(?R_12,.(and(id,?T_7),?R_7)) = .(.(?R_12,and(.(i,sub(id,?R_7)),?T_7)),e),
     .(?R_12,id) = .(.(?R_12,c),w2),
     .(?R_12,id) = .(.(?R_12,c),w1),
     .(?R_12,.(w2,?T_8)) = .(.(?R_12,and(?R_8,?T_8)),w2),
     .(?R_12,.(w1,?R_9)) = .(.(?R_12,and(?R_9,?T_9)),w1),
     .(?R_12,sub(.(?U_10,?R_10),.(?T_10,?V_10))) = .(.(?R_12,sub(?R_10,?T_10)),sub(?U_10,?V_10)),
     .(?R_12,and(.(?R_11,?U_11),.(?T_11,?V_11))) = .(.(?R_12,and(?R_11,?T_11)),and(?U_11,?V_11)),
     .(?R_12,.(i,sub(id,and(?R_13,id)))) = .(.(?R_12,?R_13),i),
     .(?R_12,?R_14) = .(.(?R_12,id),?R_14),
     .(?R_12,.(c,and(?R_15,?R_15))) = .(.(?R_12,?R_15),c),
     .(.(?W,sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)) = .(.(?W,sub(?R,?T)),sub(.(?U_1,?U),.(?V,?V_1))),
     .(.(?W,and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)) = .(.(?W,and(?R,?T)),and(.(?U,?U_1),.(?V,?V_1))),
     .(?R_1,.(.(?R,?T),?U)) = .(.(?R_1,?R),.(?T,?U)) ]
Outer CPs:
   [ .(.(id,?T_12),?U_12) = .(?T_12,?U_12),
     .(i,sub(id,and(id,id))) = i,
     c = .(c,and(id,id)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
Left-Linear, not Right-Linear
unknown Development Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ .(.(?R_14,?R),c) = .(?R_14,.(c,and(?R,?R))),
     c = .(c,and(id,id)),
     .(.(?R_14,id),?R) = .(?R_14,?R),
     .(id,and(.(?R_8,?U_8),.(?T_8,?V_8))) = .(and(?R_8,?T_8),and(?U_8,?V_8)),
     .(id,sub(.(?U_7,?R_7),.(?T_7,?V_7))) = .(sub(?R_7,?T_7),sub(?U_7,?V_7)),
     .(.(id,w1),?R_6) = .(and(?R_6,?T_6),w1),
     .(.(id,w2),?T_5) = .(and(?R_5,?T_5),w2),
     .(id,and(id,?R_3)) = .(and(i,?R_3),e),
     .(.(id,and(id,?T_2)),?R_2) = .(and(.(i,sub(id,?R_2)),?T_2),e),
     .(c,and(id,id)) = c,
     .(i,sub(id,and(id,id))) = i,
     .(.(id,?T_13),?U_13) = .(?T_13,?U_13),
     .(.(?R_14,?R),i) = .(?R_14,.(i,sub(id,and(?R,id)))),
     i = .(i,sub(id,and(id,id))),
     .(.(?R_1,?R),.(?T,?U)) = .(?R_1,.(.(?R,?T),?U)),
     .(.(?R_1,?R),.(c,and(?T,?T))) = .(?R_1,.(.(?R,?T),c)),
     .(.(?R_1,?R),?U) = .(?R_1,.(.(?R,id),?U)),
     .(.(?R_1,?R),.(i,sub(id,and(?T,id)))) = .(?R_1,.(.(?R,?T),i)),
     .(.(?R_1,?R),and(.(?R_14,?U_14),.(?T_14,?V_14))) = .(?R_1,.(.(?R,and(?R_14,?T_14)),and(?U_14,?V_14))),
     .(.(?R_1,?R),sub(.(?U_13,?R_13),.(?T_13,?V_13))) = .(?R_1,.(.(?R,sub(?R_13,?T_13)),sub(?U_13,?V_13))),
     .(.(?R_1,?R),.(w1,?R_12)) = .(?R_1,.(.(?R,and(?R_12,?T_12)),w1)),
     .(.(?R_1,?R),.(w2,?T_11)) = .(?R_1,.(.(?R,and(?R_11,?T_11)),w2)),
     .(.(?R_1,?R),id) = .(?R_1,.(.(?R,c),w1)),
     .(.(?R_1,?R),id) = .(?R_1,.(.(?R,c),w2)),
     .(.(?R_1,?R),.(and(id,?T_10),?R_10)) = .(?R_1,.(.(?R,and(.(i,sub(id,?R_10)),?T_10)),e)),
     .(.(?R_1,?R),.(?W_9,and(.(?R_9,?U_9),.(?T_9,?V_9)))) = .(?R_1,.(.(?R,.(?W_9,and(?R_9,?T_9))),and(?U_9,?V_9))),
     .(.(?R_1,?R),.(?W_8,sub(.(?U_8,?R_8),.(?T_8,?V_8)))) = .(?R_1,.(.(?R,.(?W_8,sub(?R_8,?T_8))),sub(?U_8,?V_8))),
     .(.(?R_1,?R),.(.(?W_7,w1),?R_7)) = .(?R_1,.(.(?R,.(?W_7,and(?R_7,?T_7))),w1)),
     .(.(?R_1,?R),.(.(?W_6,w2),?T_6)) = .(?R_1,.(.(?R,.(?W_6,and(?R_6,?T_6))),w2)),
     .(.(?R_1,?R),and(id,?R_5)) = .(?R_1,.(.(?R,and(i,?R_5)),e)),
     .(.(?R_1,?R),.(?W_4,and(id,?R_4))) = .(?R_1,.(.(?R,.(?W_4,and(i,?R_4))),e)),
     .(.(?R_1,?R),.(.(?W_3,and(id,?T_3)),?R_3)) = .(?R_1,.(.(?R,.(?W_3,and(.(i,sub(id,?R_3)),?T_3))),e)),
     .(.(?R_1,?R),.(.(?T,?T_2),?U_2)) = .(?R_1,.(.(?R,?T),.(?T_2,?U_2))),
     .(?R,.(c,and(?T,?T))) = .(.(?R,?T),c),
     .(?R,?U) = .(.(?R,id),?U),
     .(?R,.(i,sub(id,and(?T,id)))) = .(.(?R,?T),i),
     .(?R,and(.(?R_13,?U_13),.(?T_13,?V_13))) = .(.(?R,and(?R_13,?T_13)),and(?U_13,?V_13)),
     .(?R,sub(.(?U_12,?R_12),.(?T_12,?V_12))) = .(.(?R,sub(?R_12,?T_12)),sub(?U_12,?V_12)),
     .(?R,.(w1,?R_11)) = .(.(?R,and(?R_11,?T_11)),w1),
     .(?R,.(w2,?T_10)) = .(.(?R,and(?R_10,?T_10)),w2),
     .(?R,id) = .(.(?R,c),w1),
     .(?R,id) = .(.(?R,c),w2),
     .(?R,.(and(id,?T_9),?R_9)) = .(.(?R,and(.(i,sub(id,?R_9)),?T_9)),e),
     .(?R,.(?W_8,and(.(?R_8,?U_8),.(?T_8,?V_8)))) = .(.(?R,.(?W_8,and(?R_8,?T_8))),and(?U_8,?V_8)),
     .(?R,.(?W_7,sub(.(?U_7,?R_7),.(?T_7,?V_7)))) = .(.(?R,.(?W_7,sub(?R_7,?T_7))),sub(?U_7,?V_7)),
     .(?R,.(.(?W_6,w1),?R_6)) = .(.(?R,.(?W_6,and(?R_6,?T_6))),w1),
     .(?R,.(.(?W_5,w2),?T_5)) = .(.(?R,.(?W_5,and(?R_5,?T_5))),w2),
     .(?R,and(id,?R_4)) = .(.(?R,and(i,?R_4)),e),
     .(?R,.(?W_3,and(id,?R_3))) = .(.(?R,.(?W_3,and(i,?R_3))),e),
     .(?R,.(.(?W_2,and(id,?T_2)),?R_2)) = .(.(?R,.(?W_2,and(.(i,sub(id,?R_2)),?T_2))),e),
     .(?R,.(.(?T,?T_1),?U_1)) = .(.(?R,?T),.(?T_1,?U_1)),
     .(?T,?U) = .(.(id,?T),?U),
     .(c,and(?T,?T)) = .(.(id,?T),c),
     ?U = .(.(id,id),?U),
     .(i,sub(id,and(?T,id))) = .(.(id,?T),i),
     and(.(?R_13,?U_13),.(?T_13,?V_13)) = .(.(id,and(?R_13,?T_13)),and(?U_13,?V_13)),
     sub(.(?U_12,?R_12),.(?T_12,?V_12)) = .(.(id,sub(?R_12,?T_12)),sub(?U_12,?V_12)),
     .(w1,?R_11) = .(.(id,and(?R_11,?T_11)),w1),
     .(w2,?T_10) = .(.(id,and(?R_10,?T_10)),w2),
     id = .(.(id,c),w1),
     id = .(.(id,c),w2),
     .(and(id,?T_9),?R_9) = .(.(id,and(.(i,sub(id,?R_9)),?T_9)),e),
     .(?W_8,and(.(?R_8,?U_8),.(?T_8,?V_8))) = .(.(id,.(?W_8,and(?R_8,?T_8))),and(?U_8,?V_8)),
     .(?W_7,sub(.(?U_7,?R_7),.(?T_7,?V_7))) = .(.(id,.(?W_7,sub(?R_7,?T_7))),sub(?U_7,?V_7)),
     .(.(?W_6,w1),?R_6) = .(.(id,.(?W_6,and(?R_6,?T_6))),w1),
     .(.(?W_5,w2),?T_5) = .(.(id,.(?W_5,and(?R_5,?T_5))),w2),
     and(id,?R_4) = .(.(id,and(i,?R_4)),e),
     .(?W_3,and(id,?R_3)) = .(.(id,.(?W_3,and(i,?R_3))),e),
     .(.(?W_2,and(id,?T_2)),?R_2) = .(.(id,.(?W_2,and(.(i,sub(id,?R_2)),?T_2))),e),
     .(.(?T,?T_1),?U_1) = .(.(id,?T),.(?T_1,?U_1)),
     .(.(?R_13,and(?R,?T)),and(?U,?V)) = .(?R_13,and(.(?R,?U),.(?T,?V))),
     .(and(?R,?T),and(.(?U,?U_8),.(?V,?V_8))) = .(and(.(?R,?U),.(?T,?V)),and(?U_8,?V_8)),
     .(.(and(?R,?T),w1),?U) = .(and(.(?R,?U),.(?T,?V)),w1),
     .(.(and(?R,?T),w2),?V) = .(and(.(?R,?U),.(?T,?V)),w2),
     .(and(?R,?T),and(id,?V)) = .(and(.(?R,i),.(?T,?V)),e),
     .(.(and(?R,?T),and(id,?V)),?R_2) = .(and(.(?R,.(i,sub(id,?R_2))),.(?T,?V)),e),
     .(id,and(.(?U,?U_8),.(?V,?V_8))) = .(and(.(id,?U),.(id,?V)),and(?U_8,?V_8)),
     .(.(id,w1),?U) = .(and(.(id,?U),.(id,?V)),w1),
     .(.(id,w2),?V) = .(and(.(id,?U),.(id,?V)),w2),
     .(id,and(id,?V)) = .(and(.(id,i),.(id,?V)),e),
     .(.(id,and(id,?V)),?R_2) = .(and(.(id,.(i,sub(id,?R_2))),.(id,?V)),e),
     .(and(?R,?T),id) = and(.(?R,id),.(?T,id)),
     .(id,and(?U,?V)) = and(.(id,?U),.(id,?V)),
     .(id,id) = and(.(id,id),.(id,id)),
     .(.(?R_13,sub(?R,?T)),sub(?U,?V)) = .(?R_13,sub(.(?U,?R),.(?T,?V))),
     .(sub(?R,?T),sub(.(?U_7,?U),.(?V,?V_7))) = .(sub(.(?U,?R),.(?T,?V)),sub(?U_7,?V_7)),
     .(id,sub(.(?U_7,?U),.(?V,?V_7))) = .(sub(.(?U,id),.(id,?V)),sub(?U_7,?V_7)),
     .(sub(?R,?T),id) = sub(.(id,?R),.(?T,id)),
     .(id,sub(?U,?V)) = sub(.(?U,id),.(id,?V)),
     .(id,id) = sub(.(id,id),.(id,id)),
     .(.(?R_13,and(?R,?T)),w1) = .(?R_13,.(w1,?R)),
     .(.(?R_13,id),w1) = .(?R_13,.(w1,id)),
     .(id,w1) = .(w1,id),
     .(.(?R_13,and(?R,?T)),w2) = .(?R_13,.(w2,?T)),
     .(.(?R_13,id),w2) = .(?R_13,.(w2,id)),
     .(id,w2) = .(w2,id),
     .(.(?R_12,c),w1) = .(?R_12,id),
     .(.(?R_12,c),w2) = .(?R_12,id),
     .(.(?R_13,and(.(i,sub(id,?R)),?T)),e) = .(?R_13,.(and(id,?T),?R)),
     .(.(?R_13,and(.(i,id),?T)),e) = .(?R_13,.(and(id,?T),id)),
     .(and(.(i,id),?T),e) = .(and(id,?T),id),
     .(.(?R_13,.(?W,and(?R,?T))),and(?U,?V)) = .(?R_13,.(?W,and(.(?R,?U),.(?T,?V)))),
     .(.(.(?W,and(?R,?T)),w1),?U) = .(.(?W,and(.(?R,?U),.(?T,?V))),w1),
     .(.(.(?W,and(?R,?T)),w2),?V) = .(.(?W,and(.(?R,?U),.(?T,?V))),w2),
     .(.(?W,and(?R,?T)),and(id,?V)) = .(.(?W,and(.(?R,i),.(?T,?V))),e),
     .(.(.(?W,and(?R,?T)),and(id,?V)),?R_2) = .(.(?W,and(.(?R,.(i,sub(id,?R_2))),.(?T,?V))),e),
     .(.(?W,and(?R,?T)),and(.(?U,?U_1),.(?V,?V_1))) = .(.(?W,and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)),
     .(.(?R_13,.(?W,and(?R,?T))),id) = .(?R_13,.(?W,and(.(?R,id),.(?T,id)))),
     .(.(?R_13,.(?W,id)),and(?U,?V)) = .(?R_13,.(?W,and(.(id,?U),.(id,?V)))),
     .(.(?R_13,and(?R,?T)),and(?U,?V)) = .(?R_13,.(id,and(.(?R,?U),.(?T,?V)))),
     .(.(?R_13,and(.(?R_25,?R),.(?T_25,?T))),and(?U,?V)) = .(?R_13,.(and(?R_25,?T_25),and(.(?R,?U),.(?T,?V)))),
     .(.(?R_13,.(?W_14,and(.(?R_14,?R),.(?T_14,?T)))),and(?U,?V)) = .(?R_13,.(.(?W_14,and(?R_14,?T_14)),and(.(?R,?U),.(?T,?V)))),
     .(.(.(?W,id),w1),?U) = .(.(?W,and(.(id,?U),.(id,?V))),w1),
     .(.(and(?R,?T),w1),?U) = .(.(id,and(.(?R,?U),.(?T,?V))),w1),
     .(.(and(.(?R_12,?R),.(?T_12,?T)),w1),?U) = .(.(and(?R_12,?T_12),and(.(?R,?U),.(?T,?V))),w1),
     .(.(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),w1),?U) = .(.(.(?W_1,and(?R_1,?T_1)),and(.(?R,?U),.(?T,?V))),w1),
     .(.(.(?W,id),w2),?V) = .(.(?W,and(.(id,?U),.(id,?V))),w2),
     .(.(and(?R,?T),w2),?V) = .(.(id,and(.(?R,?U),.(?T,?V))),w2),
     .(.(and(.(?R_12,?R),.(?T_12,?T)),w2),?V) = .(.(and(?R_12,?T_12),and(.(?R,?U),.(?T,?V))),w2),
     .(.(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),w2),?V) = .(.(.(?W_1,and(?R_1,?T_1)),and(.(?R,?U),.(?T,?V))),w2),
     .(.(?W,id),and(id,?V)) = .(.(?W,and(.(id,i),.(id,?V))),e),
     .(and(?R,?T),and(id,?V)) = .(.(id,and(.(?R,i),.(?T,?V))),e),
     .(and(.(?R_12,?R),.(?T_12,?T)),and(id,?V)) = .(.(and(?R_12,?T_12),and(.(?R,i),.(?T,?V))),e),
     .(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),and(id,?V)) = .(.(.(?W_1,and(?R_1,?T_1)),and(.(?R,i),.(?T,?V))),e),
     .(.(.(?W,id),and(id,?V)),?R_2) = .(.(?W,and(.(id,.(i,sub(id,?R_2))),.(id,?V))),e),
     .(.(and(?R,?T),and(id,?V)),?R_2) = .(.(id,and(.(?R,.(i,sub(id,?R_2))),.(?T,?V))),e),
     .(.(and(.(?R_14,?R),.(?T_14,?T)),and(id,?V)),?R_2) = .(.(and(?R_14,?T_14),and(.(?R,.(i,sub(id,?R_2))),.(?T,?V))),e),
     .(.(.(?W_3,and(.(?R_3,?R),.(?T_3,?T))),and(id,?V)),?R_2) = .(.(.(?W_3,and(?R_3,?T_3)),and(.(?R,.(i,sub(id,?R_2))),.(?T,?V))),e),
     .(.(?W,id),and(.(?U,?U_1),.(?V,?V_1))) = .(.(?W,and(.(id,?U),.(id,?V))),and(?U_1,?V_1)),
     .(and(?R,?T),and(.(?U,?U_1),.(?V,?V_1))) = .(.(id,and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)),
     .(and(.(?R_13,?R),.(?T_13,?T)),and(.(?U,?U_1),.(?V,?V_1))) = .(.(and(?R_13,?T_13),and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)),
     .(.(?W_2,and(.(?R_2,?R),.(?T_2,?T))),and(.(?U,?U_1),.(?V,?V_1))) = .(.(.(?W_2,and(?R_2,?T_2)),and(.(?R,?U),.(?T,?V))),and(?U_1,?V_1)),
     .(.(?R_13,.(?W,id)),id) = .(?R_13,.(?W,and(.(id,id),.(id,id)))),
     .(.(?R_13,and(?R,?T)),id) = .(?R_13,.(id,and(.(?R,id),.(?T,id)))),
     .(.(?R_13,id),and(?U,?V)) = .(?R_13,.(id,and(.(id,?U),.(id,?V)))),
     .(.(?R_13,and(.(?R_25,?R),.(?T_25,?T))),id) = .(?R_13,.(and(?R_25,?T_25),and(.(?R,id),.(?T,id)))),
     .(.(?R_13,.(?W_14,and(.(?R_14,?R),.(?T_14,?T)))),id) = .(?R_13,.(.(?W_14,and(?R_14,?T_14)),and(.(?R,id),.(?T,id)))),
     .(.(id,w1),?U) = .(.(id,and(.(id,?U),.(id,?V))),w1),
     .(.(id,w2),?V) = .(.(id,and(.(id,?U),.(id,?V))),w2),
     .(id,and(id,?V)) = .(.(id,and(.(id,i),.(id,?V))),e),
     .(.(id,and(id,?V)),?R_2) = .(.(id,and(.(id,.(i,sub(id,?R_2))),.(id,?V))),e),
     .(id,and(.(?U,?U_1),.(?V,?V_1))) = .(.(id,and(.(id,?U),.(id,?V))),and(?U_1,?V_1)),
     .(.(?R_13,id),id) = .(?R_13,.(id,and(.(id,id),.(id,id)))),
     .(.(?W,and(?R,?T)),id) = .(?W,and(.(?R,id),.(?T,id))),
     .(.(?W,id),and(?U,?V)) = .(?W,and(.(id,?U),.(id,?V))),
     .(and(?R,?T),and(?U,?V)) = .(id,and(.(?R,?U),.(?T,?V))),
     .(and(.(?R_12,?R),.(?T_12,?T)),and(?U,?V)) = .(and(?R_12,?T_12),and(.(?R,?U),.(?T,?V))),
     .(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),and(?U,?V)) = .(.(?W_1,and(?R_1,?T_1)),and(.(?R,?U),.(?T,?V))),
     .(.(?W,id),id) = .(?W,and(.(id,id),.(id,id))),
     .(and(?R,?T),id) = .(id,and(.(?R,id),.(?T,id))),
     .(id,and(?U,?V)) = .(id,and(.(id,?U),.(id,?V))),
     .(and(.(?R_12,?R),.(?T_12,?T)),id) = .(and(?R_12,?T_12),and(.(?R,id),.(?T,id))),
     .(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),id) = .(.(?W_1,and(?R_1,?T_1)),and(.(?R,id),.(?T,id))),
     .(id,id) = .(id,and(.(id,id),.(id,id))),
     .(.(?R_13,.(?W,sub(?R,?T))),sub(?U,?V)) = .(?R_13,.(?W,sub(.(?U,?R),.(?T,?V)))),
     .(.(?W,sub(?R,?T)),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(?W,sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)),
     .(.(?R_13,.(?W,sub(?R,?T))),id) = .(?R_13,.(?W,sub(.(id,?R),.(?T,id)))),
     .(.(?R_13,.(?W,id)),sub(?U,?V)) = .(?R_13,.(?W,sub(.(?U,id),.(id,?V)))),
     .(.(?R_13,sub(?R,?T)),sub(?U,?V)) = .(?R_13,.(id,sub(.(?U,?R),.(?T,?V)))),
     .(.(?R_13,sub(.(?R,?R_24),.(?T_24,?T))),sub(?U,?V)) = .(?R_13,.(sub(?R_24,?T_24),sub(.(?U,?R),.(?T,?V)))),
     .(.(?R_13,.(?W_14,sub(.(?R,?R_14),.(?T_14,?T)))),sub(?U,?V)) = .(?R_13,.(.(?W_14,sub(?R_14,?T_14)),sub(.(?U,?R),.(?T,?V)))),
     .(.(?W,id),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(?W,sub(.(?U,id),.(id,?V))),sub(?U_1,?V_1)),
     .(sub(?R,?T),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(id,sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)),
     .(sub(.(?R,?R_12),.(?T_12,?T)),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(sub(?R_12,?T_12),sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)),
     .(.(?W_2,sub(.(?R,?R_2),.(?T_2,?T))),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(.(?W_2,sub(?R_2,?T_2)),sub(.(?U,?R),.(?T,?V))),sub(?U_1,?V_1)),
     .(.(?R_13,.(?W,id)),id) = .(?R_13,.(?W,sub(.(id,id),.(id,id)))),
     .(.(?R_13,sub(?R,?T)),id) = .(?R_13,.(id,sub(.(id,?R),.(?T,id)))),
     .(.(?R_13,id),sub(?U,?V)) = .(?R_13,.(id,sub(.(?U,id),.(id,?V)))),
     .(.(?R_13,sub(.(?R,?R_24),.(?T_24,?T))),id) = .(?R_13,.(sub(?R_24,?T_24),sub(.(id,?R),.(?T,id)))),
     .(.(?R_13,.(?W_14,sub(.(?R,?R_14),.(?T_14,?T)))),id) = .(?R_13,.(.(?W_14,sub(?R_14,?T_14)),sub(.(id,?R),.(?T,id)))),
     .(id,sub(.(?U_1,?U),.(?V,?V_1))) = .(.(id,sub(.(?U,id),.(id,?V))),sub(?U_1,?V_1)),
     .(.(?R_13,id),id) = .(?R_13,.(id,sub(.(id,id),.(id,id)))),
     .(.(?W,sub(?R,?T)),id) = .(?W,sub(.(id,?R),.(?T,id))),
     .(.(?W,id),sub(?U,?V)) = .(?W,sub(.(?U,id),.(id,?V))),
     .(sub(?R,?T),sub(?U,?V)) = .(id,sub(.(?U,?R),.(?T,?V))),
     .(sub(.(?R,?R_11),.(?T_11,?T)),sub(?U,?V)) = .(sub(?R_11,?T_11),sub(.(?U,?R),.(?T,?V))),
     .(.(?W_1,sub(.(?R,?R_1),.(?T_1,?T))),sub(?U,?V)) = .(.(?W_1,sub(?R_1,?T_1)),sub(.(?U,?R),.(?T,?V))),
     .(.(?W,id),id) = .(?W,sub(.(id,id),.(id,id))),
     .(sub(?R,?T),id) = .(id,sub(.(id,?R),.(?T,id))),
     .(id,sub(?U,?V)) = .(id,sub(.(?U,id),.(id,?V))),
     .(sub(.(?R,?R_11),.(?T_11,?T)),id) = .(sub(?R_11,?T_11),sub(.(id,?R),.(?T,id))),
     .(.(?W_1,sub(.(?R,?R_1),.(?T_1,?T))),id) = .(.(?W_1,sub(?R_1,?T_1)),sub(.(id,?R),.(?T,id))),
     .(id,id) = .(id,sub(.(id,id),.(id,id))),
     .(.(?R_13,.(?W,and(?R,?T))),w1) = .(?R_13,.(.(?W,w1),?R)),
     .(.(?R_13,.(?W,id)),w1) = .(?R_13,.(.(?W,w1),id)),
     .(.(?R_13,and(?R,?T)),w1) = .(?R_13,.(.(id,w1),?R)),
     .(.(?R_13,and(.(?R_25,?R),.(?T_25,?T))),w1) = .(?R_13,.(.(and(?R_25,?T_25),w1),?R)),
     .(.(?R_13,.(?W_20,and(.(?R_20,?R),.(?T_20,?T)))),w1) = .(?R_13,.(.(.(?W_20,and(?R_20,?T_20)),w1),?R)),
     .(.(?R_13,id),w1) = .(?R_13,.(.(id,w1),id)),
     .(.(?W,id),w1) = .(.(?W,w1),id),
     .(and(?R,?T),w1) = .(.(id,w1),?R),
     .(and(.(?R_12,?R),.(?T_12,?T)),w1) = .(.(and(?R_12,?T_12),w1),?R),
     .(.(?W_7,and(.(?R_7,?R),.(?T_7,?T))),w1) = .(.(.(?W_7,and(?R_7,?T_7)),w1),?R),
     .(id,w1) = .(.(id,w1),id),
     .(.(?R_13,.(?W,and(?R,?T))),w2) = .(?R_13,.(.(?W,w2),?T)),
     .(.(?R_13,.(?W,id)),w2) = .(?R_13,.(.(?W,w2),id)),
     .(.(?R_13,and(?R,?T)),w2) = .(?R_13,.(.(id,w2),?T)),
     .(.(?R_13,and(.(?R_25,?R),.(?T_25,?T))),w2) = .(?R_13,.(.(and(?R_25,?T_25),w2),?T)),
     .(.(?R_13,.(?W_20,and(.(?R_20,?R),.(?T_20,?T)))),w2) = .(?R_13,.(.(.(?W_20,and(?R_20,?T_20)),w2),?T)),
     .(.(?R_13,id),w2) = .(?R_13,.(.(id,w2),id)),
     .(.(?W,id),w2) = .(.(?W,w2),id),
     .(and(?R,?T),w2) = .(.(id,w2),?T),
     .(and(.(?R_12,?R),.(?T_12,?T)),w2) = .(.(and(?R_12,?T_12),w2),?T),
     .(.(?W_7,and(.(?R_7,?R),.(?T_7,?T))),w2) = .(.(.(?W_7,and(?R_7,?T_7)),w2),?T),
     .(id,w2) = .(.(id,w2),id),
     .(.(?R_13,and(i,?R)),e) = .(?R_13,and(id,?R)),
     .(.(?R_13,.(?W,and(i,?R))),e) = .(?R_13,.(?W,and(id,?R))),
     .(.(?R_13,and(i,?R)),e) = .(?R_13,.(id,and(id,?R))),
     .(.(?R_13,and(.(?R_25,i),.(?T_25,?R))),e) = .(?R_13,.(and(?R_25,?T_25),and(id,?R))),
     .(.(?R_13,.(?W_20,and(.(?R_20,i),.(?T_20,?R)))),e) = .(?R_13,.(.(?W_20,and(?R_20,?T_20)),and(id,?R))),
     .(and(i,?R),e) = .(id,and(id,?R)),
     .(and(.(?R_12,i),.(?T_12,?R)),e) = .(and(?R_12,?T_12),and(id,?R)),
     .(.(?W_7,and(.(?R_7,i),.(?T_7,?R))),e) = .(.(?W_7,and(?R_7,?T_7)),and(id,?R)),
     .(.(?R_13,.(?W,and(.(i,sub(id,?R)),?T))),e) = .(?R_13,.(.(?W,and(id,?T)),?R)),
     .(.(?R_13,.(?W,and(.(i,id),?T))),e) = .(?R_13,.(.(?W,and(id,?T)),id)),
     .(.(?R_13,and(.(i,sub(id,?R)),?T)),e) = .(?R_13,.(.(id,and(id,?T)),?R)),
     .(.(?R_13,and(.(?R_25,.(i,sub(id,?R))),.(?T_25,?T))),e) = .(?R_13,.(.(and(?R_25,?T_25),and(id,?T)),?R)),
     .(.(?R_13,.(?W_20,and(.(?R_20,.(i,sub(id,?R))),.(?T_20,?T)))),e) = .(?R_13,.(.(.(?W_20,and(?R_20,?T_20)),and(id,?T)),?R)),
     .(.(?R_13,and(.(i,id),?T)),e) = .(?R_13,.(.(id,and(id,?T)),id)),
     .(.(?R_13,and(.(?R_25,.(i,id)),.(?T_25,?T))),e) = .(?R_13,.(.(and(?R_25,?T_25),and(id,?T)),id)),
     .(.(?R_13,.(?W_20,and(.(?R_20,.(i,id)),.(?T_20,?T)))),e) = .(?R_13,.(.(.(?W_20,and(?R_20,?T_20)),and(id,?T)),id)),
     .(.(?W,and(.(i,id),?T)),e) = .(.(?W,and(id,?T)),id),
     .(and(.(i,sub(id,?R)),?T),e) = .(.(id,and(id,?T)),?R),
     .(and(.(?R_12,.(i,sub(id,?R))),.(?T_12,?T)),e) = .(.(and(?R_12,?T_12),and(id,?T)),?R),
     .(.(?W_7,and(.(?R_7,.(i,sub(id,?R))),.(?T_7,?T))),e) = .(.(.(?W_7,and(?R_7,?T_7)),and(id,?T)),?R),
     .(and(.(i,id),?T),e) = .(.(id,and(id,?T)),id),
     .(and(.(?R_12,.(i,id)),.(?T_12,?T)),e) = .(.(and(?R_12,?T_12),and(id,?T)),id),
     .(.(?W_7,and(.(?R_7,.(i,id)),.(?T_7,?T))),e) = .(.(.(?W_7,and(?R_7,?T_7)),and(id,?T)),id),
     and(.(?R_11,id),.(?T_11,id)) = .(and(?R_11,?T_11),id),
     and(.(id,?U_11),.(id,?V_11)) = .(id,and(?U_11,?V_11)),
     .(w1,id) = .(id,w1),
     .(w2,id) = .(id,w2),
     .(?W_6,and(.(?R_6,id),.(?T_6,id))) = .(.(?W_6,and(?R_6,?T_6)),id),
     .(?W_6,and(.(id,?U_6),.(id,?V_6))) = .(.(?W_6,id),and(?U_6,?V_6)),
     .(.(?W_4,w1),id) = .(.(?W_4,id),w1),
     .(.(?W_3,w2),id) = .(.(?W_3,id),w2),
     sub(.(id,?R_10),.(?T_10,id)) = .(sub(?R_10,?T_10),id),
     sub(.(?U_10,id),.(id,?V_10)) = .(id,sub(?U_10,?V_10)),
     .(and(id,?T_7),id) = .(and(.(i,id),?T_7),e),
     .(?W_5,sub(.(id,?R_5),.(?T_5,id))) = .(.(?W_5,sub(?R_5,?T_5)),id),
     .(?W_5,sub(.(?U_5,id),.(id,?V_5))) = .(.(?W_5,id),sub(?U_5,?V_5)),
     .(.(?W,and(id,?T)),id) = .(.(?W,and(.(i,id),?T)),e) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <.(.(?W,and(.(i,id),?T)),e), .(.(?W,and(id,?T)),id)> by Rules <0, 2> preceded by [(.,1),(.,2),(and,1),(.,2)]
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ sub(id,id) -> id,
     and(id,id) -> id,
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(c,w2) -> id,
     .(c,w1) -> id,
     .(and(?R,?T),w2) -> .(w2,?T),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(id,?R) -> ?R,
     .(?R,c) -> .(c,and(?R,?R)) ]
P:
   [ .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(?R,.(?T,?U)) -> .(.(?R,?T),?U) ]
P: not reversible
failure(Step 1)
STEP: 2 (linear)
S:
   [ sub(id,id) -> id,
     and(id,id) -> id,
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(c,w2) -> id,
     .(c,w1) -> id,
     .(and(?R,?T),w2) -> .(w2,?T),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(id,?R) -> ?R,
     .(?R,c) -> .(c,and(?R,?R)) ]
P:
   [ .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(?R,.(?T,?U)) -> .(.(?R,?T),?U) ]
P: not reversible
failure(Step 2)
STEP: 3 (relative)
S:
   [ sub(id,id) -> id,
     and(id,id) -> id,
     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R),
     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
     .(and(i,?R),e) -> and(id,?R),
     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
     .(c,w2) -> id,
     .(c,w1) -> id,
     .(and(?R,?T),w2) -> .(w2,?T),
     .(and(?R,?T),w1) -> .(w1,?R),
     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
     .(?R,i) -> .(i,sub(id,and(?R,id))),
     .(id,?R) -> ?R,
     .(?R,c) -> .(c,and(?R,?R)) ]
P:
   [ .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
     .(?R,.(?T,?U)) -> .(.(?R,?T),?U) ]
P: not reversible
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: <.(?R_12,?R_14), .(.(?R_12,id),?R_14)> from .(?R_12,.(id,?R_14))
Not Confluent
Direct Methods: not CR
{1}
(cm)Rewrite Rules:
   [ .(?R,id) -> ?R ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth&Bendix
Direct Methods: CR
Try to add other components to {4,3,20,19,18,17,16,15,14,13,11,10,8,7,6,5,0,12,2,9}
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
/local-scratch/hzankl/2012/cops2012/110.trs: Failure(unknown)
(2782 msec.)