NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty R T U V W) (REPLACEMENT-MAP (. 1, 2) (and 1, 2) (sub 1, 2) (c) (e) (fSNonEmpty) (i) (id) (w1) (w2) ) (RULES .(.(W,and(.(i,sub(id,R)),T)),e) -> .(.(W,and(id,T)),R) .(.(W,and(i,R)),e) -> .(W,and(id,R)) .(.(W,and(R,T)),and(U,V)) -> .(W,and(.(R,U),.(T,V))) .(.(W,and(R,T)),w1) -> .(.(W,w1),R) .(.(W,and(R,T)),w2) -> .(.(W,w2),T) .(.(W,sub(R,T)),sub(U,V)) -> .(W,sub(.(U,R),.(T,V))) .(and(.(i,sub(id,R)),T),e) -> .(and(id,T),R) .(and(i,R),e) -> and(id,R) .(and(R,T),and(U,V)) -> and(.(R,U),.(T,V)) .(and(R,T),w1) -> .(w1,R) .(and(R,T),w2) -> .(w2,T) .(sub(R,T),sub(U,V)) -> sub(.(U,R),.(T,V)) .(c,w1) -> id .(c,w2) -> id .(id,R) -> R .(R,.(T,U)) -> .(.(R,T),U) .(R,c) -> .(c,and(R,R)) .(R,i) -> .(i,sub(id,and(R,id))) .(R,id) -> R and(id,id) -> id sub(id,id) -> id ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty R T U V W) (REPLACEMENT-MAP (. 1, 2) (and 1, 2) (sub 1, 2) (c) (e) (fSNonEmpty) (i) (id) (w1) (w2) ) (RULES .(.(W,and(.(i,sub(id,R)),T)),e) -> .(.(W,and(id,T)),R) .(.(W,and(i,R)),e) -> .(W,and(id,R)) .(.(W,and(R,T)),and(U,V)) -> .(W,and(.(R,U),.(T,V))) .(.(W,and(R,T)),w1) -> .(.(W,w1),R) .(.(W,and(R,T)),w2) -> .(.(W,w2),T) .(.(W,sub(R,T)),sub(U,V)) -> .(W,sub(.(U,R),.(T,V))) .(and(.(i,sub(id,R)),T),e) -> .(and(id,T),R) .(and(i,R),e) -> and(id,R) .(and(R,T),and(U,V)) -> and(.(R,U),.(T,V)) .(and(R,T),w1) -> .(w1,R) .(and(R,T),w2) -> .(w2,T) .(sub(R,T),sub(U,V)) -> sub(.(U,R),.(T,V)) .(c,w1) -> id .(c,w2) -> id .(id,R) -> R .(R,.(T,U)) -> .(.(R,T),U) .(R,c) -> .(c,and(R,R)) .(R,i) -> .(i,sub(id,and(R,id))) .(R,id) -> R and(id,id) -> id sub(id,id) -> id ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: .(.(W,and(.(i,sub(id,R)),T)),e) -> .(.(W,and(id,T)),R) .(.(W,and(i,R)),e) -> .(W,and(id,R)) .(.(W,and(R,T)),and(U,V)) -> .(W,and(.(R,U),.(T,V))) .(.(W,and(R,T)),w1) -> .(.(W,w1),R) .(.(W,and(R,T)),w2) -> .(.(W,w2),T) .(.(W,sub(R,T)),sub(U,V)) -> .(W,sub(.(U,R),.(T,V))) .(and(.(i,sub(id,R)),T),e) -> .(and(id,T),R) .(and(i,R),e) -> and(id,R) .(and(R,T),and(U,V)) -> and(.(R,U),.(T,V)) .(and(R,T),w1) -> .(w1,R) .(and(R,T),w2) -> .(w2,T) .(sub(R,T),sub(U,V)) -> sub(.(U,R),.(T,V)) .(c,w1) -> id .(c,w2) -> id .(id,R) -> R .(R,.(T,U)) -> .(.(R,T),U) .(R,c) -> .(c,and(R,R)) .(R,i) -> .(i,sub(id,and(R,id))) .(R,id) -> R and(id,id) -> id sub(id,id) -> id -> Vars: R, T, W, R, W, R, T, U, V, W, R, T, W, R, T, W, R, T, U, V, W, R, T, R, R, T, U, V, R, T, R, T, R, T, U, V, R, R, T, U, R, R, R -> Rlps: (rule: .(.(W,and(.(i,sub(id,R)),T)),e) -> .(.(W,and(id,T)),R), id: 1, possubterms: .(.(W,and(.(i,sub(id,R)),T)),e)->[], .(W,and(.(i,sub(id,R)),T))->[1], and(.(i,sub(id,R)),T)->[1, 2], .(i,sub(id,R))->[1, 2, 1], i->[1, 2, 1, 1], sub(id,R)->[1, 2, 1, 2], id->[1, 2, 1, 2, 1], e->[2]) (rule: .(.(W,and(i,R)),e) -> .(W,and(id,R)), id: 2, possubterms: .(.(W,and(i,R)),e)->[], .(W,and(i,R))->[1], and(i,R)->[1, 2], i->[1, 2, 1], e->[2]) (rule: .(.(W,and(R,T)),and(U,V)) -> .(W,and(.(R,U),.(T,V))), id: 3, possubterms: .(.(W,and(R,T)),and(U,V))->[], .(W,and(R,T))->[1], and(R,T)->[1, 2], and(U,V)->[2]) (rule: .(.(W,and(R,T)),w1) -> .(.(W,w1),R), id: 4, possubterms: .(.(W,and(R,T)),w1)->[], .(W,and(R,T))->[1], and(R,T)->[1, 2], w1->[2]) (rule: .(.(W,and(R,T)),w2) -> .(.(W,w2),T), id: 5, possubterms: .(.(W,and(R,T)),w2)->[], .(W,and(R,T))->[1], and(R,T)->[1, 2], w2->[2]) (rule: .(.(W,sub(R,T)),sub(U,V)) -> .(W,sub(.(U,R),.(T,V))), id: 6, possubterms: .(.(W,sub(R,T)),sub(U,V))->[], .(W,sub(R,T))->[1], sub(R,T)->[1, 2], sub(U,V)->[2]) (rule: .(and(.(i,sub(id,R)),T),e) -> .(and(id,T),R), id: 7, possubterms: .(and(.(i,sub(id,R)),T),e)->[], and(.(i,sub(id,R)),T)->[1], .(i,sub(id,R))->[1, 1], i->[1, 1, 1], sub(id,R)->[1, 1, 2], id->[1, 1, 2, 1], e->[2]) (rule: .(and(i,R),e) -> and(id,R), id: 8, possubterms: .(and(i,R),e)->[], and(i,R)->[1], i->[1, 1], e->[2]) (rule: .(and(R,T),and(U,V)) -> and(.(R,U),.(T,V)), id: 9, possubterms: .(and(R,T),and(U,V))->[], and(R,T)->[1], and(U,V)->[2]) (rule: .(and(R,T),w1) -> .(w1,R), id: 10, possubterms: .(and(R,T),w1)->[], and(R,T)->[1], w1->[2]) (rule: .(and(R,T),w2) -> .(w2,T), id: 11, possubterms: .(and(R,T),w2)->[], and(R,T)->[1], w2->[2]) (rule: .(sub(R,T),sub(U,V)) -> sub(.(U,R),.(T,V)), id: 12, possubterms: .(sub(R,T),sub(U,V))->[], sub(R,T)->[1], sub(U,V)->[2]) (rule: .(c,w1) -> id, id: 13, possubterms: .(c,w1)->[], c->[1], w1->[2]) (rule: .(c,w2) -> id, id: 14, possubterms: .(c,w2)->[], c->[1], w2->[2]) (rule: .(id,R) -> R, id: 15, possubterms: .(id,R)->[], id->[1]) (rule: .(R,.(T,U)) -> .(.(R,T),U), id: 16, possubterms: .(R,.(T,U))->[], .(T,U)->[2]) (rule: .(R,c) -> .(c,and(R,R)), id: 17, possubterms: .(R,c)->[], c->[2]) (rule: .(R,i) -> .(i,sub(id,and(R,id))), id: 18, possubterms: .(R,i)->[], i->[2]) (rule: .(R,id) -> R, id: 19, possubterms: .(R,id)->[], id->[2]) (rule: and(id,id) -> id, id: 20, possubterms: and(id,id)->[], id->[1], id->[2]) (rule: sub(id,id) -> id, id: 21, possubterms: sub(id,id)->[], id->[1], id->[2]) -> Unifications: (R1 unifies with R3 at p: [1], l: .(.(W,and(.(i,sub(id,R)),T)),e), lp: .(W,and(.(i,sub(id,R)),T)), sig: {T -> V,W -> .(W',and(R',T')),U -> .(i,sub(id,R))}, l': .(.(W',and(R',T')),and(U,V)), r: .(.(W,and(id,T)),R), r': .(W',and(.(R',U),.(T',V)))) (R1 unifies with R9 at p: [1], l: .(.(W,and(.(i,sub(id,R)),T)),e), lp: .(W,and(.(i,sub(id,R)),T)), sig: {T -> V,W -> and(R',T'),U -> .(i,sub(id,R))}, l': .(and(R',T'),and(U,V)), r: .(.(W,and(id,T)),R), r': and(.(R',U),.(T',V))) (R1 unifies with R15 at p: [1], l: .(.(W,and(.(i,sub(id,R)),T)),e), lp: .(W,and(.(i,sub(id,R)),T)), sig: {W -> id,R' -> and(.(i,sub(id,R)),T)}, l': .(id,R'), r: .(.(W,and(id,T)),R), r': R') (R1 unifies with R21 at p: [1,2,1,2], l: .(.(W,and(.(i,sub(id,R)),T)),e), lp: sub(id,R), sig: {R -> id}, l': sub(id,id), r: .(.(W,and(id,T)),R), r': id) (R2 unifies with R3 at p: [1], l: .(.(W,and(i,R)),e), lp: .(W,and(i,R)), sig: {R -> V,W -> .(W',and(R',T)),U -> i}, l': .(.(W',and(R',T)),and(U,V)), r: .(W,and(id,R)), r': .(W',and(.(R',U),.(T,V)))) (R2 unifies with R9 at p: [1], l: .(.(W,and(i,R)),e), lp: .(W,and(i,R)), sig: {R -> V,W -> and(R',T),U -> i}, l': .(and(R',T),and(U,V)), r: .(W,and(id,R)), r': and(.(R',U),.(T,V))) (R2 unifies with R15 at p: [1], l: .(.(W,and(i,R)),e), lp: .(W,and(i,R)), sig: {W -> id,R' -> and(i,R)}, l': .(id,R'), r: .(W,and(id,R)), r': R') (R3 unifies with R3 at p: [1], l: .(.(W,and(R,T)),and(U,V)), lp: .(W,and(R,T)), sig: {R -> U',T -> V',W -> .(W',and(R',T'))}, l': .(.(W',and(R',T')),and(U',V')), r: .(W,and(.(R,U),.(T,V))), r': .(W',and(.(R',U'),.(T',V')))) (R3 unifies with R9 at p: [1], l: .(.(W,and(R,T)),and(U,V)), lp: .(W,and(R,T)), sig: {R -> U',T -> V',W -> and(R',T')}, l': .(and(R',T'),and(U',V')), r: .(W,and(.(R,U),.(T,V))), r': and(.(R',U'),.(T',V'))) (R3 unifies with R15 at p: [1], l: .(.(W,and(R,T)),and(U,V)), lp: .(W,and(R,T)), sig: {W -> id,R' -> and(R,T)}, l': .(id,R'), r: .(W,and(.(R,U),.(T,V))), r': R') (R3 unifies with R20 at p: [1,2], l: .(.(W,and(R,T)),and(U,V)), lp: and(R,T), sig: {R -> id,T -> id}, l': and(id,id), r: .(W,and(.(R,U),.(T,V))), r': id) (R3 unifies with R20 at p: [2], l: .(.(W,and(R,T)),and(U,V)), lp: and(U,V), sig: {U -> id,V -> id}, l': and(id,id), r: .(W,and(.(R,U),.(T,V))), r': id) (R4 unifies with R3 at p: [1], l: .(.(W,and(R,T)),w1), lp: .(W,and(R,T)), sig: {R -> U,T -> V,W -> .(W',and(R',T'))}, l': .(.(W',and(R',T')),and(U,V)), r: .(.(W,w1),R), r': .(W',and(.(R',U),.(T',V)))) (R4 unifies with R9 at p: [1], l: .(.(W,and(R,T)),w1), lp: .(W,and(R,T)), sig: {R -> U,T -> V,W -> and(R',T')}, l': .(and(R',T'),and(U,V)), r: .(.(W,w1),R), r': and(.(R',U),.(T',V))) (R4 unifies with R15 at p: [1], l: .(.(W,and(R,T)),w1), lp: .(W,and(R,T)), sig: {W -> id,R' -> and(R,T)}, l': .(id,R'), r: .(.(W,w1),R), r': R') (R4 unifies with R20 at p: [1,2], l: .(.(W,and(R,T)),w1), lp: and(R,T), sig: {R -> id,T -> id}, l': and(id,id), r: .(.(W,w1),R), r': id) (R5 unifies with R3 at p: [1], l: .(.(W,and(R,T)),w2), lp: .(W,and(R,T)), sig: {R -> U,T -> V,W -> .(W',and(R',T'))}, l': .(.(W',and(R',T')),and(U,V)), r: .(.(W,w2),T), r': .(W',and(.(R',U),.(T',V)))) (R5 unifies with R9 at p: [1], l: .(.(W,and(R,T)),w2), lp: .(W,and(R,T)), sig: {R -> U,T -> V,W -> and(R',T')}, l': .(and(R',T'),and(U,V)), r: .(.(W,w2),T), r': and(.(R',U),.(T',V))) (R5 unifies with R15 at p: [1], l: .(.(W,and(R,T)),w2), lp: .(W,and(R,T)), sig: {W -> id,R' -> and(R,T)}, l': .(id,R'), r: .(.(W,w2),T), r': R') (R5 unifies with R20 at p: [1,2], l: .(.(W,and(R,T)),w2), lp: and(R,T), sig: {R -> id,T -> id}, l': and(id,id), r: .(.(W,w2),T), r': id) (R6 unifies with R6 at p: [1], l: .(.(W,sub(R,T)),sub(U,V)), lp: .(W,sub(R,T)), sig: {R -> U',T -> V',W -> .(W',sub(R',T'))}, l': .(.(W',sub(R',T')),sub(U',V')), r: .(W,sub(.(U,R),.(T,V))), r': .(W',sub(.(U',R'),.(T',V')))) (R6 unifies with R12 at p: [1], l: .(.(W,sub(R,T)),sub(U,V)), lp: .(W,sub(R,T)), sig: {R -> U',T -> V',W -> sub(R',T')}, l': .(sub(R',T'),sub(U',V')), r: .(W,sub(.(U,R),.(T,V))), r': sub(.(U',R'),.(T',V'))) (R6 unifies with R15 at p: [1], l: .(.(W,sub(R,T)),sub(U,V)), lp: .(W,sub(R,T)), sig: {W -> id,R' -> sub(R,T)}, l': .(id,R'), r: .(W,sub(.(U,R),.(T,V))), r': R') (R6 unifies with R21 at p: [1,2], l: .(.(W,sub(R,T)),sub(U,V)), lp: sub(R,T), sig: {R -> id,T -> id}, l': sub(id,id), r: .(W,sub(.(U,R),.(T,V))), r': id) (R6 unifies with R21 at p: [2], l: .(.(W,sub(R,T)),sub(U,V)), lp: sub(U,V), sig: {U -> id,V -> id}, l': sub(id,id), r: .(W,sub(.(U,R),.(T,V))), r': id) (R7 unifies with R21 at p: [1,1,2], l: .(and(.(i,sub(id,R)),T),e), lp: sub(id,R), sig: {R -> id}, l': sub(id,id), r: .(and(id,T),R), r': id) (R9 unifies with R20 at p: [1], l: .(and(R,T),and(U,V)), lp: and(R,T), sig: {R -> id,T -> id}, l': and(id,id), r: and(.(R,U),.(T,V)), r': id) (R9 unifies with R20 at p: [2], l: .(and(R,T),and(U,V)), lp: and(U,V), sig: {U -> id,V -> id}, l': and(id,id), r: and(.(R,U),.(T,V)), r': id) (R10 unifies with R20 at p: [1], l: .(and(R,T),w1), lp: and(R,T), sig: {R -> id,T -> id}, l': and(id,id), r: .(w1,R), r': id) (R11 unifies with R20 at p: [1], l: .(and(R,T),w2), lp: and(R,T), sig: {R -> id,T -> id}, l': and(id,id), r: .(w2,T), r': id) (R12 unifies with R21 at p: [1], l: .(sub(R,T),sub(U,V)), lp: sub(R,T), sig: {R -> id,T -> id}, l': sub(id,id), r: sub(.(U,R),.(T,V)), r': id) (R12 unifies with R21 at p: [2], l: .(sub(R,T),sub(U,V)), lp: sub(U,V), sig: {U -> id,V -> id}, l': sub(id,id), r: sub(.(U,R),.(T,V)), r': id) (R16 unifies with R15 at p: [], l: .(R,.(T,U)), lp: .(R,.(T,U)), sig: {R -> id,R' -> .(T,U)}, l': .(id,R'), r: .(.(R,T),U), r': R') (R16 unifies with R1 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> .(W,and(.(i,sub(id,R')),T')),U -> e}, l': .(.(W,and(.(i,sub(id,R')),T')),e), r: .(.(R,T),U), r': .(.(W,and(id,T')),R')) (R16 unifies with R2 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> .(W,and(i,R')),U -> e}, l': .(.(W,and(i,R')),e), r: .(.(R,T),U), r': .(W,and(id,R'))) (R16 unifies with R3 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> .(W,and(R',T')),U -> and(U',V)}, l': .(.(W,and(R',T')),and(U',V)), r: .(.(R,T),U), r': .(W,and(.(R',U'),.(T',V)))) (R16 unifies with R4 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> .(W,and(R',T')),U -> w1}, l': .(.(W,and(R',T')),w1), r: .(.(R,T),U), r': .(.(W,w1),R')) (R16 unifies with R5 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> .(W,and(R',T')),U -> w2}, l': .(.(W,and(R',T')),w2), r: .(.(R,T),U), r': .(.(W,w2),T')) (R16 unifies with R6 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> .(W,sub(R',T')),U -> sub(U',V)}, l': .(.(W,sub(R',T')),sub(U',V)), r: .(.(R,T),U), r': .(W,sub(.(U',R'),.(T',V)))) (R16 unifies with R7 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> and(.(i,sub(id,R')),T'),U -> e}, l': .(and(.(i,sub(id,R')),T'),e), r: .(.(R,T),U), r': .(and(id,T'),R')) (R16 unifies with R8 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> and(i,R'),U -> e}, l': .(and(i,R'),e), r: .(.(R,T),U), r': and(id,R')) (R16 unifies with R9 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> and(R',T'),U -> and(U',V)}, l': .(and(R',T'),and(U',V)), r: .(.(R,T),U), r': and(.(R',U'),.(T',V))) (R16 unifies with R10 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> and(R',T'),U -> w1}, l': .(and(R',T'),w1), r: .(.(R,T),U), r': .(w1,R')) (R16 unifies with R11 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> and(R',T'),U -> w2}, l': .(and(R',T'),w2), r: .(.(R,T),U), r': .(w2,T')) (R16 unifies with R12 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> sub(R',T'),U -> sub(U',V)}, l': .(sub(R',T'),sub(U',V)), r: .(.(R,T),U), r': sub(.(U',R'),.(T',V))) (R16 unifies with R13 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> c,U -> w1}, l': .(c,w1), r: .(.(R,T),U), r': id) (R16 unifies with R14 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> c,U -> w2}, l': .(c,w2), r: .(.(R,T),U), r': id) (R16 unifies with R15 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> id,U -> R'}, l': .(id,R'), r: .(.(R,T),U), r': R') (R16 unifies with R16 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> R',U -> .(T',U')}, l': .(R',.(T',U')), r: .(.(R,T),U), r': .(.(R',T'),U')) (R16 unifies with R17 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> R',U -> c}, l': .(R',c), r: .(.(R,T),U), r': .(c,and(R',R'))) (R16 unifies with R18 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> R',U -> i}, l': .(R',i), r: .(.(R,T),U), r': .(i,sub(id,and(R',id)))) (R16 unifies with R19 at p: [2], l: .(R,.(T,U)), lp: .(T,U), sig: {T -> R',U -> id}, l': .(R',id), r: .(.(R,T),U), r': R') (R17 unifies with R15 at p: [], l: .(R,c), lp: .(R,c), sig: {R -> id,R' -> c}, l': .(id,R'), r: .(c,and(R,R)), r': R') (R18 unifies with R15 at p: [], l: .(R,i), lp: .(R,i), sig: {R -> id,R' -> i}, l': .(id,R'), r: .(i,sub(id,and(R,id))), r': R') (R19 unifies with R15 at p: [], l: .(R,id), lp: .(R,id), sig: {R -> id,R' -> id}, l': .(id,R'), r: R, r': R') -> Critical pairs info: => Trivial, Overlay, Proper, NW0, N1 => Not trivial, Overlay, Proper, NW0, N2 <.(id,w1),.(w1,id)> => Not trivial, Not overlay, Proper, NW0, N3 => Not trivial, Overlay, Proper, NW0, N4 <.(id,w2),.(w2,id)> => Not trivial, Not overlay, Proper, NW0, N5 <.(R,id),.(.(R,c),w2)> => Not trivial, Not overlay, Proper, NW0, N6 <.(R,id),.(.(R,c),w1)> => Not trivial, Not overlay, Proper, NW0, N7 <.(R,R'),.(.(R,id),R')> => Not trivial, Not overlay, Proper, NW0, N8 <.(T,U),.(.(id,T),U)> => Not trivial, Overlay, Proper, NW0, N9 <.(R,R'),.(.(R,R'),id)> => Not trivial, Not overlay, Proper, NW0, N10 <.(.(W,id),w2),.(.(W,w2),id)> => Not trivial, Not overlay, Proper, NW0, N11 <.(.(W,id),w1),.(.(W,w1),id)> => Not trivial, Not overlay, Proper, NW0, N12 <.(and(R,T),w2),.(.(id,w2),T)> => Not trivial, Not overlay, Proper, NW0, N13 <.(and(i,R),e),.(id,and(id,R))> => Not trivial, Not overlay, Proper, NW0, N14 <.(R,.(c,and(R',R'))),.(.(R,R'),c)> => Not trivial, Not overlay, Proper, NW0, N15 <.(and(R,T),w1),.(.(id,w1),R)> => Not trivial, Not overlay, Proper, NW0, N16 <.(and(R,T),id),and(.(R,id),.(T,id))> => Not trivial, Not overlay, Proper, NW0, N17 <.(R,.(w1,R')),.(.(R,and(R',T')),w1)> => Not trivial, Not overlay, Proper, NW0, N18 <.(and(.(i,id),T),e),.(and(id,T),id)> => Not trivial, Not overlay, Proper, NW0, N19 <.(R,.(.(R',T'),U')),.(.(R,R'),.(T',U'))> => Not trivial, Not overlay, Proper, NW0, N20 <.(sub(R,T),id),sub(.(id,R),.(T,id))> => Not trivial, Not overlay, Proper, NW0, N21 <.(R,.(w2,T')),.(.(R,and(R',T')),w2)> => Not trivial, Not overlay, Proper, NW0, N22 <.(id,sub(U,V)),sub(.(U,id),.(id,V))> => Not trivial, Not overlay, Proper, NW0, N23 <.(id,and(U,V)),and(.(id,U),.(id,V))> => Not trivial, Not overlay, Proper, NW0, N24 <.(R,.(i,sub(id,and(R',id)))),.(.(R,R'),i)> => Not trivial, Not overlay, Proper, NW0, N25 <.(R,and(id,R')),.(.(R,and(i,R')),e)> => Not trivial, Not overlay, Proper, NW0, N26 <.(.(W,and(.(i,id),T)),e),.(.(W,and(id,T)),id)> => Not trivial, Not overlay, Proper, NW0, N27 <.(.(W,sub(R,T)),id),.(W,sub(.(id,R),.(T,id)))> => Not trivial, Not overlay, Proper, NW0, N28 <.(R,.(.(W,w2),T')),.(.(R,.(W,and(R',T'))),w2)> => Not trivial, Not overlay, Proper, NW0, N29 <.(R,.(.(W,w1),R')),.(.(R,.(W,and(R',T'))),w1)> => Not trivial, Not overlay, Proper, NW0, N30 <.(.(W,id),sub(U,V)),.(W,sub(.(U,id),.(id,V)))> => Not trivial, Not overlay, Proper, NW0, N31 <.(.(W,id),and(U,V)),.(W,and(.(id,U),.(id,V)))> => Not trivial, Not overlay, Proper, NW0, N32 <.(.(W,and(R,T)),id),.(W,and(.(R,id),.(T,id)))> => Not trivial, Not overlay, Proper, NW0, N33 <.(and(R,T),and(U,V)),.(id,and(.(R,U),.(T,V)))> => Not trivial, Not overlay, Proper, NW0, N34 <.(and(.(i,sub(id,R)),T),e),.(.(id,and(id,T)),R)> => Not trivial, Not overlay, Proper, NW0, N35 <.(sub(R,T),sub(U,V)),.(id,sub(.(U,R),.(T,V)))> => Not trivial, Not overlay, Proper, NW0, N36 <.(and(.(R',U),.(T',V)),w2),.(.(and(R',T'),w2),V)> => Not trivial, Not overlay, Proper, NW0, N37 <.(and(.(R',U),.(T',V)),w1),.(.(and(R',T'),w1),U)> => Not trivial, Not overlay, Proper, NW0, N38 <.(and(.(R',i),.(T,V)),e),.(and(R',T),and(id,V))> => Not trivial, Not overlay, Proper, NW0, N39 <.(R,.(W,and(id,R'))),.(.(R,.(W,and(i,R'))),e)> => Not trivial, Not overlay, Proper, NW0, N40 <.(R,and(.(R',U'),.(T',V))),.(.(R,and(R',T')),and(U',V))> => Not trivial, Not overlay, Proper, NW0, N41 <.(R,sub(.(U',R'),.(T',V))),.(.(R,sub(R',T')),sub(U',V))> => Not trivial, Not overlay, Proper, NW0, N42 <.(.(W',and(.(R',U),.(T',V))),w1),.(.(.(W',and(R',T')),w1),U)> => Not trivial, Not overlay, Proper, NW0, N43 <.(R,.(and(id,T'),R')),.(.(R,and(.(i,sub(id,R')),T')),e)> => Not trivial, Not overlay, Proper, NW0, N44 <.(.(W',and(.(R',i),.(T,V))),e),.(.(W',and(R',T)),and(id,V))> => Not trivial, Not overlay, Proper, NW0, N45 <.(.(W',and(.(R',U),.(T',V))),w2),.(.(.(W',and(R',T')),w2),V)> => Not trivial, Not overlay, Proper, NW0, N46 <.(sub(.(U',R'),.(T',V')),sub(U,V)),.(sub(R',T'),sub(.(U,U'),.(V',V)))> => Not trivial, Not overlay, Proper, NW0, N47 <.(R,.(W,sub(.(U',R'),.(T',V)))),.(.(R,.(W,sub(R',T'))),sub(U',V))> => Not trivial, Not overlay, Proper, NW0, N48 <.(and(.(R',U'),.(T',V')),and(U,V)),.(and(R',T'),and(.(U',U),.(V',V)))> => Not trivial, Not overlay, Proper, NW0, N49 <.(R,.(W,and(.(R',U'),.(T',V)))),.(.(R,.(W,and(R',T'))),and(U',V))> => Not trivial, Not overlay, Proper, NW0, N50 <.(R,.(.(W,and(id,T')),R')),.(.(R,.(W,and(.(i,sub(id,R')),T'))),e)> => Not trivial, Not overlay, Proper, NW0, N51 <.(and(.(R',.(i,sub(id,R))),.(T',V)),e),.(.(and(R',T'),and(id,V)),R)> => Not trivial, Not overlay, Proper, NW0, N52 <.(.(W',and(.(R',U'),.(T',V'))),and(U,V)),.(.(W',and(R',T')),and(.(U',U),.(V',V)))> => Not trivial, Not overlay, Proper, NW0, N53 <.(.(W',sub(.(U',R'),.(T',V'))),sub(U,V)),.(.(W',sub(R',T')),sub(.(U,U'),.(V',V)))> => Not trivial, Not overlay, Proper, NW0, N54 <.(.(W',and(.(R',.(i,sub(id,R))),.(T',V))),e),.(.(.(W',and(R',T')),and(id,V)),R)> => Not trivial, Not overlay, Proper, NW0, N55 -> Problem conclusions: Left linear, Not right linear, Not linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR R T U V W R' T' U' V W) (REPLACEMENT-MAP (. 1, 2) (and 1, 2) (sub 1, 2) (c) (e) (fSNonEmpty) (i) (id) (w1) (w2) ) (RULES .(.(W,and(.(i,sub(id,R)),T)),e) -> .(.(W,and(id,T)),R) .(.(W,and(i,R)),e) -> .(W,and(id,R)) .(.(W,and(R,T)),and(U,V)) -> .(W,and(.(R,U),.(T,V))) .(.(W,and(R,T)),w1) -> .(.(W,w1),R) .(.(W,and(R,T)),w2) -> .(.(W,w2),T) .(.(W,sub(R,T)),sub(U,V)) -> .(W,sub(.(U,R),.(T,V))) .(and(.(i,sub(id,R)),T),e) -> .(and(id,T),R) .(and(i,R),e) -> and(id,R) .(and(R,T),and(U,V)) -> and(.(R,U),.(T,V)) .(and(R,T),w1) -> .(w1,R) .(and(R,T),w2) -> .(w2,T) .(sub(R,T),sub(U,V)) -> sub(.(U,R),.(T,V)) .(c,w1) -> id .(c,w2) -> id .(id,R) -> R .(R,.(T,U)) -> .(.(R,T),U) .(R,c) -> .(c,and(R,R)) .(R,i) -> .(i,sub(id,and(R,id))) .(R,id) -> R and(id,id) -> id sub(id,id) -> id ) Critical Pairs: <.(R,.(i,sub(id,and(R',id)))),.(.(R,R'),i)> => Not trivial, Not overlay, Proper, NW0, N25 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: No Convergence InfChecker Procedure: Infeasible convergence? YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty xR xT xU xV xW xR1 xT1 xU1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (. 1 2) (and 1 2) (sub 1 2) (c) (c_xR) (c_xR1) (cw1) (cw2) (e) (fSNonEmpty) (i) (id) ) (RULES .(.(xW,and(.(i,sub(id,xR)),xT)),e) -> .(.(xW,and(id,xT)),xR) .(.(xW,and(i,xR)),e) -> .(xW,and(id,xR)) .(.(xW,and(xR,xT)),and(xU,xV)) -> .(xW,and(.(xR,xU),.(xT,xV))) .(.(xW,and(xR,xT)),cw1) -> .(.(xW,cw1),xR) .(.(xW,and(xR,xT)),cw2) -> .(.(xW,cw2),xT) .(.(xW,sub(xR,xT)),sub(xU,xV)) -> .(xW,sub(.(xU,xR),.(xT,xV))) .(and(.(i,sub(id,xR)),xT),e) -> .(and(id,xT),xR) .(and(i,xR),e) -> and(id,xR) .(and(xR,xT),and(xU,xV)) -> and(.(xR,xU),.(xT,xV)) .(and(xR,xT),cw1) -> .(cw1,xR) .(and(xR,xT),cw2) -> .(cw2,xT) .(sub(xR,xT),sub(xU,xV)) -> sub(.(xU,xR),.(xT,xV)) .(c,cw1) -> id .(c,cw2) -> id .(id,xR) -> xR .(xR,.(xT,xU)) -> .(.(xR,xT),xU) .(xR,c) -> .(c,and(xR,xR)) .(xR,i) -> .(i,sub(id,and(xR,id))) .(xR,id) -> xR and(id,id) -> id sub(id,id) -> id )] Infeasibility Conditions: .(c_xR,.(i,sub(id,and(c_xR1,id)))) ->* z0, .(.(c_xR,c_xR1),i) ->* z0 Problem 1: Obtaining a model using AGES: -> Theory (Usable Rules): .(.(xW,and(.(i,sub(id,xR)),xT)),e) -> .(.(xW,and(id,xT)),xR) .(.(xW,and(i,xR)),e) -> .(xW,and(id,xR)) .(.(xW,and(xR,xT)),and(xU,xV)) -> .(xW,and(.(xR,xU),.(xT,xV))) .(.(xW,and(xR,xT)),cw1) -> .(.(xW,cw1),xR) .(.(xW,and(xR,xT)),cw2) -> .(.(xW,cw2),xT) .(.(xW,sub(xR,xT)),sub(xU,xV)) -> .(xW,sub(.(xU,xR),.(xT,xV))) .(and(.(i,sub(id,xR)),xT),e) -> .(and(id,xT),xR) .(and(i,xR),e) -> and(id,xR) .(and(xR,xT),and(xU,xV)) -> and(.(xR,xU),.(xT,xV)) .(and(xR,xT),cw1) -> .(cw1,xR) .(and(xR,xT),cw2) -> .(cw2,xT) .(sub(xR,xT),sub(xU,xV)) -> sub(.(xU,xR),.(xT,xV)) .(c,cw1) -> id .(c,cw2) -> id .(id,xR) -> xR .(xR,.(xT,xU)) -> .(.(xR,xT),xU) .(xR,c) -> .(c,and(xR,xR)) .(xR,i) -> .(i,sub(id,and(xR,id))) .(xR,id) -> xR and(id,id) -> id sub(id,id) -> id -> AGES Output: The problem is infeasible. The problem is not confluent.