NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (B 1) (C 1) (b 1) (c 1) (fSNonEmpty) ) (RULES B(B(x)) -> b(x) B(b(x)) -> x C(c(x)) -> x C(x) -> c(x) b(B(x)) -> x b(b(x)) -> B(x) c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x))))))) c(C(x)) -> x c(c(x)) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (B 1) (C 1) (b 1) (c 1) (fSNonEmpty) ) (RULES B(B(x)) -> b(x) B(b(x)) -> x C(c(x)) -> x C(x) -> c(x) b(B(x)) -> x b(b(x)) -> B(x) c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x))))))) c(C(x)) -> x c(c(x)) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: B(B(x)) -> b(x) B(b(x)) -> x C(c(x)) -> x C(x) -> c(x) b(B(x)) -> x b(b(x)) -> B(x) c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x))))))) c(C(x)) -> x c(c(x)) -> x -> Vars: x, x, x, x, x, x, x, x, x -> Rlps: (rule: B(B(x)) -> b(x), id: 1, possubterms: B(B(x))->[], B(x)->[1]) (rule: B(b(x)) -> x, id: 2, possubterms: B(b(x))->[], b(x)->[1]) (rule: C(c(x)) -> x, id: 3, possubterms: C(c(x))->[], c(x)->[1]) (rule: C(x) -> c(x), id: 4, possubterms: C(x)->[]) (rule: b(B(x)) -> x, id: 5, possubterms: b(B(x))->[], B(x)->[1]) (rule: b(b(x)) -> B(x), id: 6, possubterms: b(b(x))->[], b(x)->[1]) (rule: c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x))))))), id: 7, possubterms: c(B(c(b(c(x)))))->[], B(c(b(c(x))))->[1], c(b(c(x)))->[1, 1], b(c(x))->[1, 1, 1], c(x)->[1, 1, 1, 1]) (rule: c(C(x)) -> x, id: 8, possubterms: c(C(x))->[], C(x)->[1]) (rule: c(c(x)) -> x, id: 9, possubterms: c(c(x))->[], c(x)->[1]) -> Unifications: (R1 unifies with R1 at p: [1], l: B(B(x)), lp: B(x), sig: {x -> B(x')}, l': B(B(x')), r: b(x), r': b(x')) (R1 unifies with R2 at p: [1], l: B(B(x)), lp: B(x), sig: {x -> b(x')}, l': B(b(x')), r: b(x), r': x') (R2 unifies with R5 at p: [1], l: B(b(x)), lp: b(x), sig: {x -> B(x')}, l': b(B(x')), r: x, r': x') (R2 unifies with R6 at p: [1], l: B(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: x, r': B(x')) (R3 unifies with R7 at p: [1], l: C(c(x)), lp: c(x), sig: {x -> B(c(b(c(x'))))}, l': c(B(c(b(c(x'))))), r: x, r': B(c(b(c(B(c(b(x')))))))) (R3 unifies with R8 at p: [1], l: C(c(x)), lp: c(x), sig: {x -> C(x')}, l': c(C(x')), r: x, r': x') (R3 unifies with R9 at p: [1], l: C(c(x)), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: x, r': x') (R4 unifies with R3 at p: [], l: C(x), lp: C(x), sig: {x -> c(x')}, l': C(c(x')), r: c(x), r': x') (R5 unifies with R1 at p: [1], l: b(B(x)), lp: B(x), sig: {x -> B(x')}, l': B(B(x')), r: x, r': b(x')) (R5 unifies with R2 at p: [1], l: b(B(x)), lp: B(x), sig: {x -> b(x')}, l': B(b(x')), r: x, r': x') (R6 unifies with R5 at p: [1], l: b(b(x)), lp: b(x), sig: {x -> B(x')}, l': b(B(x')), r: B(x), r': x') (R6 unifies with R6 at p: [1], l: b(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: B(x), r': B(x')) (R7 unifies with R7 at p: [1,1,1,1], l: c(B(c(b(c(x))))), lp: c(x), sig: {x -> B(c(b(c(x'))))}, l': c(B(c(b(c(x'))))), r: B(c(b(c(B(c(b(x))))))), r': B(c(b(c(B(c(b(x')))))))) (R7 unifies with R8 at p: [1,1,1,1], l: c(B(c(b(c(x))))), lp: c(x), sig: {x -> C(x')}, l': c(C(x')), r: B(c(b(c(B(c(b(x))))))), r': x') (R7 unifies with R9 at p: [1,1,1,1], l: c(B(c(b(c(x))))), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: B(c(b(c(B(c(b(x))))))), r': x') (R8 unifies with R3 at p: [1], l: c(C(x)), lp: C(x), sig: {x -> c(x')}, l': C(c(x')), r: x, r': x') (R8 unifies with R4 at p: [1], l: c(C(x)), lp: C(x), sig: {x -> x'}, l': C(x'), r: x, r': c(x')) (R9 unifies with R7 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> B(c(b(c(x'))))}, l': c(B(c(b(c(x'))))), r: x, r': B(c(b(c(B(c(b(x')))))))) (R9 unifies with R8 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> C(x')}, l': c(C(x')), r: x, r': x') (R9 unifies with R9 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: x, r': x') -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Trivial, Not overlay, Proper, NW0, N3 => Trivial, Not overlay, Proper, NW0, N4 => Not trivial, Not overlay, Proper, NW0, N5 => Not trivial, Not overlay, Proper, NW0, N6 => Trivial, Not overlay, Proper, NW0, N7 => Trivial, Not overlay, Proper, NW0, N8 => Not trivial, Not overlay, Proper, NW0, N9 => Trivial, Not overlay, Proper, NW0, N10 => Not trivial, Not overlay, Proper, NW0, N11 => Not trivial, Not overlay, Proper, NW0, N12 => Not trivial, Not overlay, Proper, NW0, N13 => Not trivial, Not overlay, Proper, NW0, N14 => Not trivial, Not overlay, Proper, NW0, N15 => Not trivial, Not overlay, Proper, NW0, N16 => Not trivial, Not overlay, Proper, NW0, N17 => Not trivial, Not overlay, Proper, NW0, N18 => Not trivial, Not overlay, Proper, NW0, N19 => Not trivial, Not overlay, Proper, NW0, N20 -> Problem conclusions: Left linear, Right linear, 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 x x') (REPLACEMENT-MAP (B 1) (C 1) (b 1) (c 1) (fSNonEmpty) ) (RULES B(B(x)) -> b(x) B(b(x)) -> x C(c(x)) -> x C(x) -> c(x) b(B(x)) -> x b(b(x)) -> B(x) c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x))))))) c(C(x)) -> x c(c(x)) -> x ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N16 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: No Convergence InfChecker Procedure: Infeasible convergence? YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x x1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (B 1) (C 1) (b 1) (c 1) (c_x1) (fSNonEmpty) ) (RULES B(B(x)) -> b(x) B(b(x)) -> x C(c(x)) -> x C(x) -> c(x) b(B(x)) -> x b(b(x)) -> B(x) c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x))))))) c(C(x)) -> x c(c(x)) -> x )] Infeasibility Conditions: c(B(c(b(c(B(c(b(c_x1)))))))) ->* z0, B(c(b(c(c_x1)))) ->* z0 Problem 1: Obtaining a model using AGES: -> Theory (Usable Rules): B(B(x)) -> b(x) B(b(x)) -> x b(B(x)) -> x b(b(x)) -> B(x) c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x))))))) c(C(x)) -> x c(c(x)) -> x -> AGES Output: The problem is infeasible. The problem is not confluent.