MAYBE
(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 Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ .(.(?T,?T_1),?U_1) = .(.(id,?T),.(?T_1,?U_1)),
     ?T = .(.(id,?T),id),
     ?U = .(.(id,id),?U),
     and(.(?R_4,?U_4),.(?T_4,?V_4)) = .(.(id,and(?R_4,?T_4)),and(?U_4,?V_4)),
     sub(.(?U_5,?R_5),.(?T_5,?V_5)) = .(.(id,sub(?R_5,?T_5)),sub(?U_5,?V_5)),
     .(w1,?R_6) = .(.(id,and(?R_6,?T_6)),w1),
     .(w2,?T_7) = .(.(id,and(?R_7,?T_7)),w2),
     .(c,and(?T,?T)) = .(.(id,?T),c),
     id = .(.(id,c),w1),
     id = .(.(id,c),w2),
     .(i,sub(id,and(?T,id))) = .(.(id,?T),i),
     .(and(id,?T_10),?R_10) = .(.(id,and(.(i,sub(id,?R_10)),?T_10)),e),
     .(?W_11,and(.(?R_11,?U_11),.(?T_11,?V_11))) = .(.(id,.(?W_11,and(?R_11,?T_11))),and(?U_11,?V_11)),
     .(?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_13,w1),?R_13) = .(.(id,.(?W_13,and(?R_13,?T_13))),w1),
     .(.(?W_14,w2),?T_14) = .(.(id,.(?W_14,and(?R_14,?T_14))),w2),
     and(id,?R_15) = .(.(id,and(i,?R_15)),e),
     .(?W_16,and(id,?R_16)) = .(.(id,.(?W_16,and(i,?R_16))),e),
     .(.(?W_17,and(id,?T_17)),?R_17) = .(.(id,.(?W_17,and(.(i,sub(id,?R_17)),?T_17))),e),
     .(?T,?U) = .(.(id,?T),?U),
     .(?R,.(.(?T,?T_1),?U_1)) = .(.(?R,?T),.(?T_1,?U_1)),
     .(?R,?T) = .(.(?R,?T),id),
     .(?R,?U) = .(.(?R,id),?U),
     .(?R,and(.(?R_4,?U_4),.(?T_4,?V_4))) = .(.(?R,and(?R_4,?T_4)),and(?U_4,?V_4)),
     .(?R,sub(.(?U_5,?R_5),.(?T_5,?V_5))) = .(.(?R,sub(?R_5,?T_5)),sub(?U_5,?V_5)),
     .(?R,.(w1,?R_6)) = .(.(?R,and(?R_6,?T_6)),w1),
     .(?R,.(w2,?T_7)) = .(.(?R,and(?R_7,?T_7)),w2),
     .(?R,.(c,and(?T,?T))) = .(.(?R,?T),c),
     .(?R,id) = .(.(?R,c),w1),
     .(?R,id) = .(.(?R,c),w2),
     .(?R,.(i,sub(id,and(?T,id)))) = .(.(?R,?T),i),
     .(?R,.(and(id,?T_10),?R_10)) = .(.(?R,and(.(i,sub(id,?R_10)),?T_10)),e),
     .(?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,.(?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_13,w1),?R_13)) = .(.(?R,.(?W_13,and(?R_13,?T_13))),w1),
     .(?R,.(.(?W_14,w2),?T_14)) = .(.(?R,.(?W_14,and(?R_14,?T_14))),w2),
     .(?R,and(id,?R_15)) = .(.(?R,and(i,?R_15)),e),
     .(?R,.(?W_16,and(id,?R_16))) = .(.(?R,.(?W_16,and(i,?R_16))),e),
     .(?R,.(.(?W_17,and(id,?T_17)),?R_17)) = .(.(?R,.(?W_17,and(.(i,sub(id,?R_17)),?T_17))),e),
     .(.(?R_1,?R),.(.(?T,?T_2),?U_2)) = .(?R_1,.(.(?R,?T),.(?T_2,?U_2))),
     .(.(?R_1,?R),?T) = .(?R_1,.(.(?R,?T),id)),
     .(.(?R_1,?R),?U) = .(?R_1,.(.(?R,id),?U)),
     .(.(?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),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),.(w1,?R_7)) = .(?R_1,.(.(?R,and(?R_7,?T_7)),w1)),
     .(.(?R_1,?R),.(w2,?T_8)) = .(?R_1,.(.(?R,and(?R_8,?T_8)),w2)),
     .(.(?R_1,?R),.(c,and(?T,?T))) = .(?R_1,.(.(?R,?T),c)),
     .(.(?R_1,?R),id) = .(?R_1,.(.(?R,c),w1)),
     .(.(?R_1,?R),id) = .(?R_1,.(.(?R,c),w2)),
     .(.(?R_1,?R),.(i,sub(id,and(?T,id)))) = .(?R_1,.(.(?R,?T),i)),
     .(.(?R_1,?R),.(and(id,?T_11),?R_11)) = .(?R_1,.(.(?R,and(.(i,sub(id,?R_11)),?T_11)),e)),
     .(.(?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),.(?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_14,w1),?R_14)) = .(?R_1,.(.(?R,.(?W_14,and(?R_14,?T_14))),w1)),
     .(.(?R_1,?R),.(.(?W_15,w2),?T_15)) = .(?R_1,.(.(?R,.(?W_15,and(?R_15,?T_15))),w2)),
     .(.(?R_1,?R),and(id,?R_16)) = .(?R_1,.(.(?R,and(i,?R_16)),e)),
     .(.(?R_1,?R),.(?W_17,and(id,?R_17))) = .(?R_1,.(.(?R,.(?W_17,and(i,?R_17))),e)),
     .(.(?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),.(?T,?U)) = .(?R_1,.(.(?R,?T),?U)),
     id = id,
     .(.(?R_2,?R),id) = .(?R_2,?R),
     .(.(id,?T_1),?U_1) = .(?T_1,?U_1),
     .(c,and(id,id)) = c,
     .(i,sub(id,and(id,id))) = i,
     .(.(?R_2,id),?R) = .(?R_2,?R),
     .(id,and(.(?R_11,?U_11),.(?T_11,?V_11))) = .(and(?R_11,?T_11),and(?U_11,?V_11)),
     .(id,sub(.(?U_12,?R_12),.(?T_12,?V_12))) = .(sub(?R_12,?T_12),sub(?U_12,?V_12)),
     .(.(id,w1),?R_13) = .(and(?R_13,?T_13),w1),
     .(.(id,w2),?T_14) = .(and(?R_14,?T_14),w2),
     .(id,and(id,?R_16)) = .(and(i,?R_16),e),
     .(.(id,and(id,?T_17)),?R_17) = .(and(.(i,sub(id,?R_17)),?T_17),e),
     and(.(id,?U_3),.(id,?V_3)) = .(id,and(?U_3,?V_3)),
     and(.(?R_3,id),.(?T_3,id)) = .(and(?R_3,?T_3),id),
     .(w1,id) = .(id,w1),
     .(w2,id) = .(id,w2),
     .(?W_10,and(.(id,?U_10),.(id,?V_10))) = .(.(?W_10,id),and(?U_10,?V_10)),
     .(?W_10,and(.(?R_10,id),.(?T_10,id))) = .(.(?W_10,and(?R_10,?T_10)),id),
     .(.(?W_12,w1),id) = .(.(?W_12,id),w1),
     .(.(?W_13,w2),id) = .(.(?W_13,id),w2),
     sub(.(?U_4,id),.(id,?V_4)) = .(id,sub(?U_4,?V_4)),
     sub(.(id,?R_4),.(?T_4,id)) = .(sub(?R_4,?T_4),id),
     .(and(id,?T_9),id) = .(and(.(i,id),?T_9),e),
     .(?W_11,sub(.(?U_11,id),.(id,?V_11))) = .(.(?W_11,id),sub(?U_11,?V_11)),
     .(?W_11,sub(.(id,?R_11),.(?T_11,id))) = .(.(?W_11,sub(?R_11,?T_11)),id),
     .(.(?W_16,and(id,?T_16)),id) = .(.(?W_16,and(.(i,id),?T_16)),e),
     .(id,id) = and(.(id,id),.(id,id)),
     .(id,and(?U,?V)) = and(.(id,?U),.(id,?V)),
     .(and(?R,?T),id) = and(.(?R,id),.(?T,id)),
     .(.(?R_2,id),id) = .(?R_2,and(.(id,id),.(id,id))),
     .(.(?R_2,id),and(?U,?V)) = .(?R_2,and(.(id,?U),.(id,?V))),
     .(.(?R_2,and(?R,?T)),id) = .(?R_2,and(.(?R,id),.(?T,id))),
     .(id,and(.(?U,?U_11),.(?V,?V_11))) = .(and(.(id,?U),.(id,?V)),and(?U_11,?V_11)),
     .(.(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_17) = .(and(.(id,.(i,sub(id,?R_17))),.(id,?V)),e),
     .(.(?R_2,and(?R,?T)),and(?U,?V)) = .(?R_2,and(.(?R,?U),.(?T,?V))),
     .(and(?R,?T),and(.(?U,?U_11),.(?V,?V_11))) = .(and(.(?R,?U),.(?T,?V)),and(?U_11,?V_11)),
     .(.(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_17) = .(and(.(?R,.(i,sub(id,?R_17))),.(?T,?V)),e),
     .(id,id) = sub(.(id,id),.(id,id)),
     .(id,sub(?U,?V)) = sub(.(?U,id),.(id,?V)),
     .(sub(?R,?T),id) = sub(.(id,?R),.(?T,id)),
     .(.(?R_2,id),id) = .(?R_2,sub(.(id,id),.(id,id))),
     .(.(?R_2,id),sub(?U,?V)) = .(?R_2,sub(.(?U,id),.(id,?V))),
     .(.(?R_2,sub(?R,?T)),id) = .(?R_2,sub(.(id,?R),.(?T,id))),
     .(id,sub(.(?U_12,?U),.(?V,?V_12))) = .(sub(.(?U,id),.(id,?V)),sub(?U_12,?V_12)),
     .(.(?R_2,sub(?R,?T)),sub(?U,?V)) = .(?R_2,sub(.(?U,?R),.(?T,?V))),
     .(sub(?R,?T),sub(.(?U_12,?U),.(?V,?V_12))) = .(sub(.(?U,?R),.(?T,?V)),sub(?U_12,?V_12)),
     .(id,w1) = .(w1,id),
     .(.(?R_2,id),w1) = .(?R_2,.(w1,id)),
     .(.(?R_2,and(?R,?T)),w1) = .(?R_2,.(w1,?R)),
     .(id,w2) = .(w2,id),
     .(.(?R_2,id),w2) = .(?R_2,.(w2,id)),
     .(.(?R_2,and(?R,?T)),w2) = .(?R_2,.(w2,?T)),
     c = .(c,and(id,id)),
     .(.(?R_2,?R),c) = .(?R_2,.(c,and(?R,?R))),
     .(.(?R,c),w1) = .(?R,id),
     .(.(?R,c),w2) = .(?R,id),
     i = .(i,sub(id,and(id,id))),
     .(.(?R_2,?R),i) = .(?R_2,.(i,sub(id,and(?R,id)))),
     .(and(.(i,id),?T),e) = .(and(id,?T),id),
     .(.(?R_2,and(.(i,id),?T)),e) = .(?R_2,.(and(id,?T),id)),
     .(.(?R_2,and(.(i,sub(id,?R)),?T)),e) = .(?R_2,.(and(id,?T),?R)),
     .(id,id) = .(id,and(.(id,id),.(id,id))),
     .(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),id) = .(.(?W_1,and(?R_1,?T_1)),and(.(?R,id),.(?T,id))),
     .(id,and(?U,?V)) = .(id,and(.(id,?U),.(id,?V))),
     .(and(?R,?T),id) = .(id,and(.(?R,id),.(?T,id))),
     .(and(.(?R_5,?R),.(?T_5,?T)),id) = .(and(?R_5,?T_5),and(.(?R,id),.(?T,id))),
     .(.(?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,?T),and(?U,?V)) = .(id,and(.(?R,?U),.(?T,?V))),
     .(and(.(?R_5,?R),.(?T_5,?T)),and(?U,?V)) = .(and(?R_5,?T_5),and(.(?R,?U),.(?T,?V))),
     .(.(?R_2,id),id) = .(?R_2,.(id,and(.(id,id),.(id,id)))),
     .(id,and(.(?U,?U_1),.(?V,?V_1))) = .(.(id,and(.(id,?U),.(id,?V))),and(?U_1,?V_1)),
     .(.(?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)))),
     .(.(?R_2,id),and(?U,?V)) = .(?R_2,.(id,and(.(id,?U),.(id,?V)))),
     .(.(?R_2,and(?R,?T)),id) = .(?R_2,.(id,and(.(?R,id),.(?T,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,.(?W,id)),id) = .(?R_2,.(?W,and(.(id,id),.(id,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_17) = .(.(id,and(.(id,.(i,sub(id,?R_17))),.(id,?V))),e),
     .(.(?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)),
     .(and(?R,?T),and(.(?U,?U_1),.(?V,?V_1))) = .(.(id,and(.(?R,?U),.(?T,?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)),
     .(.(?W,id),and(.(?U,?U_1),.(?V,?V_1))) = .(.(?W,and(.(id,?U),.(id,?V))),and(?U_1,?V_1)),
     .(.(?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)))),
     .(.(?R_2,and(?R,?T)),and(?U,?V)) = .(?R_2,.(id,and(.(?R,?U),.(?T,?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,.(?W,id)),and(?U,?V)) = .(?R_2,.(?W,and(.(id,?U),.(id,?V)))),
     .(.(?R_2,.(?W,and(?R,?T))),id) = .(?R_2,.(?W,and(.(?R,id),.(?T,id)))),
     .(.(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),w1),?U) = .(.(.(?W_1,and(?R_1,?T_1)),and(.(?R,?U),.(?T,?V))),w1),
     .(.(and(?R,?T),w1),?U) = .(.(id,and(.(?R,?U),.(?T,?V))),w1),
     .(.(and(.(?R_5,?R),.(?T_5,?T)),w1),?U) = .(.(and(?R_5,?T_5),and(.(?R,?U),.(?T,?V))),w1),
     .(.(.(?W,id),w1),?U) = .(.(?W,and(.(id,?U),.(id,?V))),w1),
     .(.(.(?W_1,and(.(?R_1,?R),.(?T_1,?T))),w2),?V) = .(.(.(?W_1,and(?R_1,?T_1)),and(.(?R,?U),.(?T,?V))),w2),
     .(.(and(?R,?T),w2),?V) = .(.(id,and(.(?R,?U),.(?T,?V))),w2),
     .(.(and(.(?R_5,?R),.(?T_5,?T)),w2),?V) = .(.(and(?R_5,?T_5),and(.(?R,?U),.(?T,?V))),w2),
     .(.(.(?W,id),w2),?V) = .(.(?W,and(.(id,?U),.(id,?V))),w2),
     .(.(?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),
     .(and(?R,?T),and(id,?V)) = .(.(id,and(.(?R,i),.(?T,?V))),e),
     .(and(.(?R_5,?R),.(?T_5,?T)),and(id,?V)) = .(.(and(?R_5,?T_5),and(.(?R,i),.(?T,?V))),e),
     .(.(?W,id),and(id,?V)) = .(.(?W,and(.(id,i),.(id,?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),
     .(.(and(?R,?T),and(id,?V)),?R_17) = .(.(id,and(.(?R,.(i,sub(id,?R_17))),.(?T,?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),
     .(.(.(?W,id),and(id,?V)),?R_17) = .(.(?W,and(.(id,.(i,sub(id,?R_17))),.(id,?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_2,.(?W,and(?R,?T))),and(?U,?V)) = .(?R_2,.(?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_17) = .(.(?W,and(.(?R,.(i,sub(id,?R_17))),.(?T,?V))),e),
     .(id,id) = .(id,sub(.(id,id),.(id,id))),
     .(.(?W_1,sub(.(?R,?R_1),.(?T_1,?T))),id) = .(.(?W_1,sub(?R_1,?T_1)),sub(.(id,?R),.(?T,id))),
     .(id,sub(?U,?V)) = .(id,sub(.(?U,id),.(id,?V))),
     .(sub(?R,?T),id) = .(id,sub(.(id,?R),.(?T,id))),
     .(sub(.(?R,?R_6),.(?T_6,?T)),id) = .(sub(?R_6,?T_6),sub(.(id,?R),.(?T,id))),
     .(.(?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,?T),sub(?U,?V)) = .(id,sub(.(?U,?R),.(?T,?V))),
     .(sub(.(?R,?R_6),.(?T_6,?T)),sub(?U,?V)) = .(sub(?R_6,?T_6),sub(.(?U,?R),.(?T,?V))),
     .(.(?R_2,id),id) = .(?R_2,.(id,sub(.(id,id),.(id,id)))),
     .(id,sub(.(?U_1,?U),.(?V,?V_1))) = .(.(id,sub(.(?U,id),.(id,?V))),sub(?U_1,?V_1)),
     .(.(?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)))),
     .(.(?R_2,id),sub(?U,?V)) = .(?R_2,.(id,sub(.(?U,id),.(id,?V)))),
     .(.(?R_2,sub(?R,?T)),id) = .(?R_2,.(id,sub(.(id,?R),.(?T,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,.(?W,id)),id) = .(?R_2,.(?W,sub(.(id,id),.(id,id)))),
     .(.(?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)),
     .(sub(?R,?T),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(id,sub(.(?U,?R),.(?T,?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)),
     .(.(?W,id),sub(.(?U_1,?U),.(?V,?V_1))) = .(.(?W,sub(.(?U,id),.(id,?V))),sub(?U_1,?V_1)),
     .(.(?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)))),
     .(.(?R_2,sub(?R,?T)),sub(?U,?V)) = .(?R_2,.(id,sub(.(?U,?R),.(?T,?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,.(?W,id)),sub(?U,?V)) = .(?R_2,.(?W,sub(.(?U,id),.(id,?V)))),
     .(.(?R_2,.(?W,sub(?R,?T))),id) = .(?R_2,.(?W,sub(.(id,?R),.(?T,id)))),
     .(.(?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))),sub(?U,?V)) = .(?R_2,.(?W,sub(.(?U,?R),.(?T,?V)))),
     .(id,w1) = .(.(id,w1),id),
     .(and(?R,?T),w1) = .(.(id,w1),?R),
     .(and(.(?R_5,?R),.(?T_5,?T)),w1) = .(.(and(?R_5,?T_5),w1),?R),
     .(.(?W_12,and(.(?R_12,?R),.(?T_12,?T))),w1) = .(.(.(?W_12,and(?R_12,?T_12)),w1),?R),
     .(.(?W,id),w1) = .(.(?W,w1),id),
     .(.(?R_2,id),w1) = .(?R_2,.(.(id,w1),id)),
     .(.(?R_2,and(?R,?T)),w1) = .(?R_2,.(.(id,w1),?R)),
     .(.(?R_2,and(.(?R_7,?R),.(?T_7,?T))),w1) = .(?R_2,.(.(and(?R_7,?T_7),w1),?R)),
     .(.(?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,.(?W,id)),w1) = .(?R_2,.(.(?W,w1),id)),
     .(.(?R_2,.(?W,and(?R,?T))),w1) = .(?R_2,.(.(?W,w1),?R)),
     .(id,w2) = .(.(id,w2),id),
     .(and(?R,?T),w2) = .(.(id,w2),?T),
     .(and(.(?R_5,?R),.(?T_5,?T)),w2) = .(.(and(?R_5,?T_5),w2),?T),
     .(.(?W_12,and(.(?R_12,?R),.(?T_12,?T))),w2) = .(.(.(?W_12,and(?R_12,?T_12)),w2),?T),
     .(.(?W,id),w2) = .(.(?W,w2),id),
     .(.(?R_2,id),w2) = .(?R_2,.(.(id,w2),id)),
     .(.(?R_2,and(?R,?T)),w2) = .(?R_2,.(.(id,w2),?T)),
     .(.(?R_2,and(.(?R_7,?R),.(?T_7,?T))),w2) = .(?R_2,.(.(and(?R_7,?T_7),w2),?T)),
     .(.(?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,.(?W,id)),w2) = .(?R_2,.(.(?W,w2),id)),
     .(.(?R_2,.(?W,and(?R,?T))),w2) = .(?R_2,.(.(?W,w2),?T)),
     .(.(?R_2,and(i,?R)),e) = .(?R_2,and(id,?R)),
     .(and(i,?R),e) = .(id,and(id,?R)),
     .(and(.(?R_5,i),.(?T_5,?R)),e) = .(and(?R_5,?T_5),and(id,?R)),
     .(.(?W_12,and(.(?R_12,i),.(?T_12,?R))),e) = .(.(?W_12,and(?R_12,?T_12)),and(id,?R)),
     .(.(?R_2,and(i,?R)),e) = .(?R_2,.(id,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,.(?W_14,and(.(?R_14,i),.(?T_14,?R)))),e) = .(?R_2,.(.(?W_14,and(?R_14,?T_14)),and(id,?R))),
     .(.(?R_2,.(?W,and(i,?R))),e) = .(?R_2,.(?W,and(id,?R))),
     .(and(.(i,id),?T),e) = .(.(id,and(id,?T)),id),
     .(and(.(?R_5,.(i,id)),.(?T_5,?T)),e) = .(.(and(?R_5,?T_5),and(id,?T)),id),
     .(.(?W_12,and(.(?R_12,.(i,id)),.(?T_12,?T))),e) = .(.(.(?W_12,and(?R_12,?T_12)),and(id,?T)),id),
     .(and(.(i,sub(id,?R)),?T),e) = .(.(id,and(id,?T)),?R),
     .(and(.(?R_5,.(i,sub(id,?R))),.(?T_5,?T)),e) = .(.(and(?R_5,?T_5),and(id,?T)),?R),
     .(.(?W_12,and(.(?R_12,.(i,sub(id,?R))),.(?T_12,?T))),e) = .(.(.(?W_12,and(?R_12,?T_12)),and(id,?T)),?R),
     .(.(?W,and(.(i,id),?T)),e) = .(.(?W,and(id,?T)),id),
     .(.(?R_2,and(.(i,id),?T)),e) = .(?R_2,.(.(id,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,.(?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(.(i,sub(id,?R)),?T)),e) = .(?R_2,.(.(id,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,.(?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,.(?W,and(.(i,id),?T))),e) = .(?R_2,.(.(?W,and(id,?T)),id)),
     .(.(?R_2,.(?W,and(.(i,sub(id,?R)),?T))),e) = .(?R_2,.(.(?W,and(id,?T)),?R)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/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
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R_1,id) -> ?R_1,
     .(id,?R_2) -> ?R_2,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R_3,?T_3),and(?U_3,?V_3)) -> and(.(?R_3,?U_3),.(?T_3,?V_3)),
     .(sub(?R_4,?T_4),sub(?U_4,?V_4)) -> sub(.(?U_4,?R_4),.(?T_4,?V_4)),
     .(and(?R_5,?T_5),w1) -> .(w1,?R_5),
     .(and(?R_6,?T_6),w2) -> .(w2,?T_6),
     .(?R_7,c) -> .(c,and(?R_7,?R_7)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R_8,i) -> .(i,sub(id,and(?R_8,id))),
     .(and(.(i,sub(id,?R_9)),?T_9),e) -> .(and(id,?T_9),?R_9),
     .(.(?W_10,and(?R_10,?T_10)),and(?U_10,?V_10)) -> .(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),
     .(.(?W_11,sub(?R_11,?T_11)),sub(?U_11,?V_11)) -> .(?W_11,sub(.(?U_11,?R_11),.(?T_11,?V_11))),
     .(.(?W_12,and(?R_12,?T_12)),w1) -> .(.(?W_12,w1),?R_12),
     .(.(?W_13,and(?R_13,?T_13)),w2) -> .(.(?W_13,w2),?T_13),
     .(and(i,?R_14),e) -> and(id,?R_14),
     .(.(?W_15,and(i,?R_15)),e) -> .(?W_15,and(id,?R_15)),
     .(.(?W_16,and(.(i,sub(id,?R_16)),?T_16)),e) -> .(.(?W_16,and(id,?T_16)),?R_16) ]
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
non-linear variables: {?R_7}
non-linear types: {59}
types leq non-linear types: {59}
rules applicable to terms of non-linear types:
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R_1,id) -> ?R_1,
     .(id,?R_2) -> ?R_2,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R_3,?T_3),and(?U_3,?V_3)) -> and(.(?R_3,?U_3),.(?T_3,?V_3)),
     .(sub(?R_4,?T_4),sub(?U_4,?V_4)) -> sub(.(?U_4,?R_4),.(?T_4,?V_4)),
     .(and(?R_5,?T_5),w1) -> .(w1,?R_5),
     .(and(?R_6,?T_6),w2) -> .(w2,?T_6),
     .(?R_7,c) -> .(c,and(?R_7,?R_7)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R_8,i) -> .(i,sub(id,and(?R_8,id))),
     .(and(.(i,sub(id,?R_9)),?T_9),e) -> .(and(id,?T_9),?R_9),
     .(.(?W_10,and(?R_10,?T_10)),and(?U_10,?V_10)) -> .(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),
     .(.(?W_11,sub(?R_11,?T_11)),sub(?U_11,?V_11)) -> .(?W_11,sub(.(?U_11,?R_11),.(?T_11,?V_11))),
     .(.(?W_12,and(?R_12,?T_12)),w1) -> .(.(?W_12,w1),?R_12),
     .(.(?W_13,and(?R_13,?T_13)),w2) -> .(.(?W_13,w2),?T_13),
     .(and(i,?R_14),e) -> and(id,?R_14),
     .(.(?W_15,and(i,?R_15)),e) -> .(?W_15,and(id,?R_15)),
     .(.(?W_16,and(.(i,sub(id,?R_16)),?T_16)),e) -> .(.(?W_16,and(id,?T_16)),?R_16) ]
NLR:
0: {}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {}
8: {}
9: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20}
10: {}
11: {}
12: {}
13: {}
14: {}
15: {}
16: {}
17: {}
18: {}
19: {}
20: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R_1,id) -> ?R_1,
     .(id,?R_2) -> ?R_2,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R_3,?T_3),and(?U_3,?V_3)) -> and(.(?R_3,?U_3),.(?T_3,?V_3)),
     .(sub(?R_4,?T_4),sub(?U_4,?V_4)) -> sub(.(?U_4,?R_4),.(?T_4,?V_4)),
     .(and(?R_5,?T_5),w1) -> .(w1,?R_5),
     .(and(?R_6,?T_6),w2) -> .(w2,?T_6),
     .(?R_7,c) -> .(c,and(?R_7,?R_7)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R_8,i) -> .(i,sub(id,and(?R_8,id))),
     .(and(.(i,sub(id,?R_9)),?T_9),e) -> .(and(id,?T_9),?R_9),
     .(.(?W_10,and(?R_10,?T_10)),and(?U_10,?V_10)) -> .(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),
     .(.(?W_11,sub(?R_11,?T_11)),sub(?U_11,?V_11)) -> .(?W_11,sub(.(?U_11,?R_11),.(?T_11,?V_11))),
     .(.(?W_12,and(?R_12,?T_12)),w1) -> .(.(?W_12,w1),?R_12),
     .(.(?W_13,and(?R_13,?T_13)),w2) -> .(.(?W_13,w2),?T_13),
     .(and(i,?R_14),e) -> and(id,?R_14),
     .(.(?W_15,and(i,?R_15)),e) -> .(?W_15,and(id,?R_15)),
     .(.(?W_16,and(.(i,sub(id,?R_16)),?T_16)),e) -> .(.(?W_16,and(id,?T_16)),?R_16) ]
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
non-linear variables: {?R_7}
non-linear types: {59}
types leq non-linear types: {59}
rules applicable to terms of non-linear types:
   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
     .(?R_1,id) -> ?R_1,
     .(id,?R_2) -> ?R_2,
     and(id,id) -> id,
     sub(id,id) -> id,
     .(and(?R_3,?T_3),and(?U_3,?V_3)) -> and(.(?R_3,?U_3),.(?T_3,?V_3)),
     .(sub(?R_4,?T_4),sub(?U_4,?V_4)) -> sub(.(?U_4,?R_4),.(?T_4,?V_4)),
     .(and(?R_5,?T_5),w1) -> .(w1,?R_5),
     .(and(?R_6,?T_6),w2) -> .(w2,?T_6),
     .(?R_7,c) -> .(c,and(?R_7,?R_7)),
     .(c,w1) -> id,
     .(c,w2) -> id,
     .(?R_8,i) -> .(i,sub(id,and(?R_8,id))),
     .(and(.(i,sub(id,?R_9)),?T_9),e) -> .(and(id,?T_9),?R_9),
     .(.(?W_10,and(?R_10,?T_10)),and(?U_10,?V_10)) -> .(?W_10,and(.(?R_10,?U_10),.(?T_10,?V_10))),
     .(.(?W_11,sub(?R_11,?T_11)),sub(?U_11,?V_11)) -> .(?W_11,sub(.(?U_11,?R_11),.(?T_11,?V_11))),
     .(.(?W_12,and(?R_12,?T_12)),w1) -> .(.(?W_12,w1),?R_12),
     .(.(?W_13,and(?R_13,?T_13)),w2) -> .(.(?W_13,w2),?T_13),
     .(and(i,?R_14),e) -> and(id,?R_14),
     .(.(?W_15,and(i,?R_15)),e) -> .(?W_15,and(id,?R_15)),
     .(.(?W_16,and(.(i,sub(id,?R_16)),?T_16)),e) -> .(.(?W_16,and(id,?T_16)),?R_16) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 31 rules by 3 steps unfolding
strenghten .(?R_19,id) and ?R_19
strenghten .(c,id) and c
strenghten .(c,w1) and id
strenghten .(c,w2) and id
strenghten .(w1,id) and .(id,w1)
strenghten .(w2,id) and .(id,w2)
strenghten .(.(?R_19,c),w1) and ?R_19
strenghten .(.(?R_20,c),w2) and ?R_20
strenghten .(c,and(id,id)) and c
strenghten .(.(?R,?R_1),id) and .(?R,?R_1)
strenghten .(.(?R,c),w1) and .(?R,id)
strenghten .(.(?R,c),w2) and .(?R,id)
strenghten .(.(?R,id),?R_2) and .(?R,?R_2)
strenghten .(.(?R,id),c) and .(?R,c)
strenghten .(.(id,?T),?U) and .(?T,?U)
strenghten .(c,and(id,id)) and .(c,id)
strenghten .(i,sub(id,and(id,id))) and i
strenghten .(.(?R,id),c) and .(?R,.(c,id))
strenghten .(.(?W_12,w1),id) and .(.(?W_12,id),w1)
strenghten .(.(?W_13,w2),id) and .(.(?W_13,id),w2)
strenghten .(.(id,w1),?R_12) and .(and(?R_12,?T_12),w1)
strenghten .(.(id,w2),?T_13) and .(and(?R_13,?T_13),w2)
strenghten .(id,and(id,?R_15)) and .(and(i,?R_15),e)
strenghten .(.(?R,?R_19),.(c,w1)) and .(?R,?R_19)
strenghten .(.(?R,?R_20),.(c,w2)) and .(?R,?R_20)
strenghten .(?R,.(c,and(?R_7,?R_7))) and .(.(?R,?R_7),c)
strenghten .(.(?R,and(?R_5,?T_5)),w1) and .(?R,.(w1,?R_5))
strenghten .(.(?R,and(?R_6,?T_6)),w2) and .(?R,.(w2,?T_6))
strenghten .(.(?R,and(i,?R_14)),e) and .(?R,and(id,?R_14))
strenghten .(and(.(i,id),?T_9),e) and .(and(id,?T_9),id)
strenghten and(.(?R_3,id),.(?T_3,id)) and .(and(?R_3,?T_3),id)
strenghten and(.(id,?U_3),.(id,?V_3)) and .(id,and(?U_3,?V_3))
strenghten sub(.(?U_4,id),.(id,?V_4)) and .(id,sub(?U_4,?V_4))
strenghten sub(.(id,?R_4),.(?T_4,id)) and .(sub(?R_4,?T_4),id)
strenghten .(.(?R_1,?R),.(?T,?U)) and .(?R_1,.(.(?R,?T),?U))
strenghten .(?R,.(i,sub(id,and(?R_8,id)))) and .(.(?R,?R_8),i)
strenghten .(?W_10,and(.(?R_10,id),.(?T_10,id))) and .(.(?W_10,and(?R_10,?T_10)),id)
strenghten .(?W_10,and(.(id,?U_10),.(id,?V_10))) and .(.(?W_10,id),and(?U_10,?V_10))
strenghten .(?W_11,sub(.(?U_11,id),.(id,?V_11))) and .(.(?W_11,id),sub(?U_11,?V_11))
strenghten .(?W_11,sub(.(id,?R_11),.(?T_11,id))) and .(.(?W_11,sub(?R_11,?T_11)),id)
strenghten .(.(?R,.(?W_12,and(?R_12,?T_12))),w1) and .(?R,.(.(?W_12,w1),?R_12))
strenghten .(.(?R,.(?W_13,and(?R_13,?T_13))),w2) and .(?R,.(.(?W_13,w2),?T_13))
strenghten .(.(?R,.(?W_15,and(i,?R_15))),e) and .(?R,.(?W_15,and(id,?R_15)))
strenghten .(.(?W_16,and(.(i,id),?T_16)),e) and .(.(?W_16,and(id,?T_16)),id)
strenghten .(id,and(.(?R_10,?U_10),.(?T_10,?V_10))) and .(and(?R_10,?T_10),and(?U_10,?V_10))
strenghten .(id,sub(.(?U_11,?R_11),.(?T_11,?V_11))) and .(sub(?R_11,?T_11),sub(?U_11,?V_11))
strenghten .(and(.(?R_3,?U_3),.(?T_3,?V_3)),w1) and .(.(and(?R_3,?T_3),w1),?U_3)
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation110.trs: Failure(timeout)
(64195 msec.)