NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y z) (REPLACEMENT-MAP (* 1, 2) (+ 1, 2) (0) (fSNonEmpty) (s 1) ) (RULES *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(0,y) -> 0 *(s(x),y) -> +(*(x,y),y) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,0) -> 0 *(x,s(y)) -> +(*(x,y),x) *(x,y) -> *(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(x,y) -> +(y,x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y z) (REPLACEMENT-MAP (* 1, 2) (+ 1, 2) (0) (fSNonEmpty) (s 1) ) (RULES *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(0,y) -> 0 *(s(x),y) -> +(*(x,y),y) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,0) -> 0 *(x,s(y)) -> +(*(x,y),x) *(x,y) -> *(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(x,y) -> +(y,x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(0,y) -> 0 *(s(x),y) -> +(*(x,y),y) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,0) -> 0 *(x,s(y)) -> +(*(x,y),x) *(x,y) -> *(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(x,y) -> +(y,x) -> Vars: x, y, z, x, y, z, y, x, y, x, y, z, x, x, y, x, y, x, y, z, y, x, y, x, x, y, x, y -> Rlps: (rule: *(*(x,y),z) -> *(x,*(y,z)), id: 1, possubterms: *(*(x,y),z)->[], *(x,y)->[1]) (rule: *(+(x,y),z) -> +(*(x,z),*(y,z)), id: 2, possubterms: *(+(x,y),z)->[], +(x,y)->[1]) (rule: *(0,y) -> 0, id: 3, possubterms: *(0,y)->[], 0->[1]) (rule: *(s(x),y) -> +(*(x,y),y), id: 4, possubterms: *(s(x),y)->[], s(x)->[1]) (rule: *(x,+(y,z)) -> +(*(x,y),*(x,z)), id: 5, possubterms: *(x,+(y,z))->[], +(y,z)->[2]) (rule: *(x,0) -> 0, id: 6, possubterms: *(x,0)->[], 0->[2]) (rule: *(x,s(y)) -> +(*(x,y),x), id: 7, possubterms: *(x,s(y))->[], s(y)->[2]) (rule: *(x,y) -> *(y,x), id: 8, possubterms: *(x,y)->[]) (rule: +(+(x,y),z) -> +(x,+(y,z)), id: 9, possubterms: +(+(x,y),z)->[], +(x,y)->[1]) (rule: +(0,y) -> y, id: 10, possubterms: +(0,y)->[], 0->[1]) (rule: +(s(x),y) -> s(+(x,y)), id: 11, possubterms: +(s(x),y)->[], s(x)->[1]) (rule: +(x,0) -> x, id: 12, possubterms: +(x,0)->[], 0->[2]) (rule: +(x,s(y)) -> s(+(x,y)), id: 13, possubterms: +(x,s(y))->[], s(y)->[2]) (rule: +(x,y) -> +(y,x), id: 14, possubterms: +(x,y)->[]) -> Unifications: (R1 unifies with R1 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> *(x',y'),y -> z'}, l': *(*(x',y'),z'), r: *(x,*(y,z)), r': *(x',*(y',z'))) (R1 unifies with R2 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> +(x',y'),y -> z'}, l': *(+(x',y'),z'), r: *(x,*(y,z)), r': +(*(x',z'),*(y',z'))) (R1 unifies with R3 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> 0,y -> y'}, l': *(0,y'), r: *(x,*(y,z)), r': 0) (R1 unifies with R4 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> s(x'),y -> y'}, l': *(s(x'),y'), r: *(x,*(y,z)), r': +(*(x',y'),y')) (R1 unifies with R5 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> x',y -> +(y',z')}, l': *(x',+(y',z')), r: *(x,*(y,z)), r': +(*(x',y'),*(x',z'))) (R1 unifies with R6 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> x',y -> 0}, l': *(x',0), r: *(x,*(y,z)), r': 0) (R1 unifies with R7 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> x',y -> s(y')}, l': *(x',s(y')), r: *(x,*(y,z)), r': +(*(x',y'),x')) (R1 unifies with R8 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> x',y -> y'}, l': *(x',y'), r: *(x,*(y,z)), r': *(y',x')) (R2 unifies with R9 at p: [1], l: *(+(x,y),z), lp: +(x,y), sig: {x -> +(x',y'),y -> z'}, l': +(+(x',y'),z'), r: +(*(x,z),*(y,z)), r': +(x',+(y',z'))) (R2 unifies with R10 at p: [1], l: *(+(x,y),z), lp: +(x,y), sig: {x -> 0,y -> y'}, l': +(0,y'), r: +(*(x,z),*(y,z)), r': y') (R2 unifies with R11 at p: [1], l: *(+(x,y),z), lp: +(x,y), sig: {x -> s(x'),y -> y'}, l': +(s(x'),y'), r: +(*(x,z),*(y,z)), r': s(+(x',y'))) (R2 unifies with R12 at p: [1], l: *(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> 0}, l': +(x',0), r: +(*(x,z),*(y,z)), r': x') (R2 unifies with R13 at p: [1], l: *(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> s(y')}, l': +(x',s(y')), r: +(*(x,z),*(y,z)), r': s(+(x',y'))) (R2 unifies with R14 at p: [1], l: *(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> y'}, l': +(x',y'), r: +(*(x,z),*(y,z)), r': +(y',x')) (R5 unifies with R1 at p: [], l: *(x,+(y,z)), lp: *(x,+(y,z)), sig: {x -> *(x',y'),z' -> +(y,z)}, l': *(*(x',y'),z'), r: +(*(x,y),*(x,z)), r': *(x',*(y',z'))) (R5 unifies with R2 at p: [], l: *(x,+(y,z)), lp: *(x,+(y,z)), sig: {x -> +(x',y'),z' -> +(y,z)}, l': *(+(x',y'),z'), r: +(*(x,y),*(x,z)), r': +(*(x',z'),*(y',z'))) (R5 unifies with R3 at p: [], l: *(x,+(y,z)), lp: *(x,+(y,z)), sig: {x -> 0,y' -> +(y,z)}, l': *(0,y'), r: +(*(x,y),*(x,z)), r': 0) (R5 unifies with R4 at p: [], l: *(x,+(y,z)), lp: *(x,+(y,z)), sig: {x -> s(x'),y' -> +(y,z)}, l': *(s(x'),y'), r: +(*(x,y),*(x,z)), r': +(*(x',y'),y')) (R5 unifies with R9 at p: [2], l: *(x,+(y,z)), lp: +(y,z), sig: {y -> +(x',y'),z -> z'}, l': +(+(x',y'),z'), r: +(*(x,y),*(x,z)), r': +(x',+(y',z'))) (R5 unifies with R10 at p: [2], l: *(x,+(y,z)), lp: +(y,z), sig: {y -> 0,z -> y'}, l': +(0,y'), r: +(*(x,y),*(x,z)), r': y') (R5 unifies with R11 at p: [2], l: *(x,+(y,z)), lp: +(y,z), sig: {y -> s(x'),z -> y'}, l': +(s(x'),y'), r: +(*(x,y),*(x,z)), r': s(+(x',y'))) (R5 unifies with R12 at p: [2], l: *(x,+(y,z)), lp: +(y,z), sig: {y -> x',z -> 0}, l': +(x',0), r: +(*(x,y),*(x,z)), r': x') (R5 unifies with R13 at p: [2], l: *(x,+(y,z)), lp: +(y,z), sig: {y -> x',z -> s(y')}, l': +(x',s(y')), r: +(*(x,y),*(x,z)), r': s(+(x',y'))) (R5 unifies with R14 at p: [2], l: *(x,+(y,z)), lp: +(y,z), sig: {y -> x',z -> y'}, l': +(x',y'), r: +(*(x,y),*(x,z)), r': +(y',x')) (R6 unifies with R1 at p: [], l: *(x,0), lp: *(x,0), sig: {x -> *(x',y),z -> 0}, l': *(*(x',y),z), r: 0, r': *(x',*(y,z))) (R6 unifies with R2 at p: [], l: *(x,0), lp: *(x,0), sig: {x -> +(x',y),z -> 0}, l': *(+(x',y),z), r: 0, r': +(*(x',z),*(y,z))) (R6 unifies with R3 at p: [], l: *(x,0), lp: *(x,0), sig: {x -> 0,y -> 0}, l': *(0,y), r: 0, r': 0) (R6 unifies with R4 at p: [], l: *(x,0), lp: *(x,0), sig: {x -> s(x'),y -> 0}, l': *(s(x'),y), r: 0, r': +(*(x',y),y)) (R7 unifies with R1 at p: [], l: *(x,s(y)), lp: *(x,s(y)), sig: {x -> *(x',y'),z -> s(y)}, l': *(*(x',y'),z), r: +(*(x,y),x), r': *(x',*(y',z))) (R7 unifies with R2 at p: [], l: *(x,s(y)), lp: *(x,s(y)), sig: {x -> +(x',y'),z -> s(y)}, l': *(+(x',y'),z), r: +(*(x,y),x), r': +(*(x',z),*(y',z))) (R7 unifies with R3 at p: [], l: *(x,s(y)), lp: *(x,s(y)), sig: {x -> 0,y' -> s(y)}, l': *(0,y'), r: +(*(x,y),x), r': 0) (R7 unifies with R4 at p: [], l: *(x,s(y)), lp: *(x,s(y)), sig: {x -> s(x'),y' -> s(y)}, l': *(s(x'),y'), r: +(*(x,y),x), r': +(*(x',y'),y')) (R8 unifies with R1 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> *(x',y'),y -> z}, l': *(*(x',y'),z), r: *(y,x), r': *(x',*(y',z))) (R8 unifies with R2 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> +(x',y'),y -> z}, l': *(+(x',y'),z), r: *(y,x), r': +(*(x',z),*(y',z))) (R8 unifies with R3 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> 0,y -> y'}, l': *(0,y'), r: *(y,x), r': 0) (R8 unifies with R4 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> s(x'),y -> y'}, l': *(s(x'),y'), r: *(y,x), r': +(*(x',y'),y')) (R8 unifies with R5 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> x',y -> +(y',z)}, l': *(x',+(y',z)), r: *(y,x), r': +(*(x',y'),*(x',z))) (R8 unifies with R6 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> x',y -> 0}, l': *(x',0), r: *(y,x), r': 0) (R8 unifies with R7 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> x',y -> s(y')}, l': *(x',s(y')), r: *(y,x), r': +(*(x',y'),x')) (R9 unifies with R9 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> +(x',y'),y -> z'}, l': +(+(x',y'),z'), r: +(x,+(y,z)), r': +(x',+(y',z'))) (R9 unifies with R10 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> 0,y -> y'}, l': +(0,y'), r: +(x,+(y,z)), r': y') (R9 unifies with R11 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> s(x'),y -> y'}, l': +(s(x'),y'), r: +(x,+(y,z)), r': s(+(x',y'))) (R9 unifies with R12 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> 0}, l': +(x',0), r: +(x,+(y,z)), r': x') (R9 unifies with R13 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> s(y')}, l': +(x',s(y')), r: +(x,+(y,z)), r': s(+(x',y'))) (R9 unifies with R14 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> y'}, l': +(x',y'), r: +(x,+(y,z)), r': +(y',x')) (R12 unifies with R9 at p: [], l: +(x,0), lp: +(x,0), sig: {x -> +(x',y),z -> 0}, l': +(+(x',y),z), r: x, r': +(x',+(y,z))) (R12 unifies with R10 at p: [], l: +(x,0), lp: +(x,0), sig: {x -> 0,y -> 0}, l': +(0,y), r: x, r': y) (R12 unifies with R11 at p: [], l: +(x,0), lp: +(x,0), sig: {x -> s(x'),y -> 0}, l': +(s(x'),y), r: x, r': s(+(x',y))) (R13 unifies with R9 at p: [], l: +(x,s(y)), lp: +(x,s(y)), sig: {x -> +(x',y'),z -> s(y)}, l': +(+(x',y'),z), r: s(+(x,y)), r': +(x',+(y',z))) (R13 unifies with R10 at p: [], l: +(x,s(y)), lp: +(x,s(y)), sig: {x -> 0,y' -> s(y)}, l': +(0,y'), r: s(+(x,y)), r': y') (R13 unifies with R11 at p: [], l: +(x,s(y)), lp: +(x,s(y)), sig: {x -> s(x'),y' -> s(y)}, l': +(s(x'),y'), r: s(+(x,y)), r': s(+(x',y'))) (R14 unifies with R9 at p: [], l: +(x,y), lp: +(x,y), sig: {x -> +(x',y'),y -> z}, l': +(+(x',y'),z), r: +(y,x), r': +(x',+(y',z))) (R14 unifies with R10 at p: [], l: +(x,y), lp: +(x,y), sig: {x -> 0,y -> y'}, l': +(0,y'), r: +(y,x), r': y') (R14 unifies with R11 at p: [], l: +(x,y), lp: +(x,y), sig: {x -> s(x'),y -> y'}, l': +(s(x'),y'), r: +(y,x), r': s(+(x',y'))) (R14 unifies with R12 at p: [], l: +(x,y), lp: +(x,y), sig: {x -> x',y -> 0}, l': +(x',0), r: +(y,x), r': x') (R14 unifies with R13 at p: [], l: +(x,y), lp: +(x,y), sig: {x -> x',y -> s(y')}, l': +(x',s(y')), r: +(y,x), r': s(+(x',y'))) -> Critical pairs info: <0,0> => Trivial, Overlay, Proper, NW0, N1 <0,0> => Trivial, Overlay, Proper, NW0, N2 => Not trivial, Overlay, Proper, NW0, N3 <0,*(0,x')> => Not trivial, Overlay, Proper, NW0, N4 => Not trivial, Overlay, Proper, NW0, N5 <0,*(y',0)> => Not trivial, Overlay, Proper, NW0, N6 <0,+(*(0,y),0)> => Not trivial, Overlay, Proper, NW0, N7 <*(x',*(y,0)),0> => Not trivial, Overlay, Proper, NW0, N8 <+(*(x',0),0),0> => Not trivial, Overlay, Proper, NW0, N9 <+(*(x',0),*(y,0)),0> => Not trivial, Overlay, Proper, NW0, N10 => Not trivial, Overlay, Proper, NW0, N11 <0,+(*(0,y),*(0,z))> => Not trivial, Overlay, Proper, NW0, N12 => Not trivial, Overlay, Proper, NW0, N13 <+(x',+(y,0)),+(x',y)> => Not trivial, Overlay, Proper, NW0, N14 <+(y',z),+(0,+(y',z))> => Not trivial, Not overlay, Proper, NW0, N15 <+(x',z),+(x',+(0,z))> => Not trivial, Not overlay, Proper, NW0, N16 <*(0,z),*(0,*(y',z))> => Not trivial, Not overlay, Proper, NW0, N17 <*(0,z),*(x',*(0,z))> => Not trivial, Not overlay, Proper, NW0, N18 <+(+(y',x'),z),+(x',+(y',z))> => Not trivial, Not overlay, Proper, NW0, N19 <*(x,y'),+(*(x,0),*(x,y'))> => Not trivial, Not overlay, Proper, NW0, N20 <*(*(y',x'),z),*(x',*(y',z))> => Not trivial, Not overlay, Proper, NW0, N21 <+(*(x',y'),x'),*(s(y'),x')> => Not trivial, Overlay, Proper, NW0, N22 <+(x',+(y',z)),+(z,+(x',y'))> => Not trivial, Overlay, Proper, NW0, N23 <*(x,x'),+(*(x,x'),*(x,0))> => Not trivial, Not overlay, Proper, NW0, N24 <*(y',z),+(*(0,z),*(y',z))> => Not trivial, Not overlay, Proper, NW0, N25 => Not trivial, Overlay, Proper, NW0, N26 => Not trivial, Overlay, Proper, NW0, N27 <*(x',z),+(*(x',z),*(0,z))> => Not trivial, Not overlay, Proper, NW0, N28 <*(x',*(y',z)),*(z,*(x',y'))> => Not trivial, Overlay, Proper, NW0, N29 <+(*(x',y'),y'),*(y',s(x'))> => Not trivial, Overlay, Proper, NW0, N30 => Not trivial, Overlay, Proper, NW0, N31 <*(+(*(x',y'),y'),z),*(s(x'),*(y',z))> => Not trivial, Not overlay, Proper, NW0, N32 <+(+(x',+(y',z')),z),+(+(x',y'),+(z',z))> => Not trivial, Not overlay, Proper, NW0, N33 <+(*(x',z),*(y',z)),*(z,+(x',y'))> => Not trivial, Overlay, Proper, NW0, N34 <+(*(x',y'),*(x',z)),*(+(y',z),x')> => Not trivial, Overlay, Proper, NW0, N35 <*(+(*(x',y'),x'),z),*(x',*(s(y'),z))> => Not trivial, Not overlay, Proper, NW0, N36 <*(+(y',x'),z),+(*(x',z),*(y',z))> => Not trivial, Not overlay, Proper, NW0, N37 <+(x',+(y',s(y))),s(+(+(x',y'),y))> => Not trivial, Overlay, Proper, NW0, N38 <+(*(x',s(y)),s(y)),+(*(s(x'),y),s(x'))> => Not trivial, Overlay, Proper, NW0, N39 <*(*(x',*(y',z')),z),*(*(x',y'),*(z',z))> => Not trivial, Not overlay, Proper, NW0, N40 <+(s(+(x',y')),z),+(x',+(s(y'),z))> => Not trivial, Not overlay, Proper, NW0, N41 <*(x,+(y',x')),+(*(x,x'),*(x,y'))> => Not trivial, Not overlay, Proper, NW0, N42 <*(x',*(y',s(y))),+(*(*(x',y'),y),*(x',y'))> => Not trivial, Overlay, Proper, NW0, N43 <+(s(+(x',y')),z),+(s(x'),+(y',z))> => Not trivial, Not overlay, Proper, NW0, N44 <+(*(x',+(y,z)),+(y,z)),+(*(s(x'),y),*(s(x'),z))> => Not trivial, Overlay, Proper, NW0, N45 <+(*(x',s(y)),*(y',s(y))),+(*(+(x',y'),y),+(x',y'))> => Not trivial, Overlay, Proper, NW0, N46 <*(s(+(x',y')),z),+(*(x',z),*(s(y'),z))> => Not trivial, Not overlay, Proper, NW0, N47 <*(+(*(x',z'),*(y',z')),z),*(+(x',y'),*(z',z))> => Not trivial, Not overlay, Proper, NW0, N48 <*(x,s(+(x',y'))),+(*(x,x'),*(x,s(y')))> => Not trivial, Not overlay, Proper, NW0, N49 <+(*(x',+(y,z)),*(y',+(y,z))),+(*(+(x',y'),y),*(+(x',y'),z))> => Not trivial, Overlay, Proper, NW0, N50 <*(x',*(y',+(y,z))),+(*(*(x',y'),y),*(*(x',y'),z))> => Not trivial, Overlay, Proper, NW0, N51 <*(s(+(x',y')),z),+(*(s(x'),z),*(y',z))> => Not trivial, Not overlay, Proper, NW0, N52 <*(+(x',+(y',z')),z),+(*(+(x',y'),z),*(z',z))> => Not trivial, Not overlay, Proper, NW0, N53 <*(+(*(x',y'),*(x',z')),z),*(x',*(+(y',z'),z))> => Not trivial, Not overlay, Proper, NW0, N54 <*(x,s(+(x',y'))),+(*(x,s(x')),*(x,y'))> => Not trivial, Not overlay, Proper, NW0, N55 <*(x,+(x',+(y',z'))),+(*(x,+(x',y')),*(x,z'))> => Not trivial, Not overlay, Proper, NW0, N56 -> 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 x y z x' y' z) (REPLACEMENT-MAP (* 1, 2) (+ 1, 2) (0) (fSNonEmpty) (s 1) ) (RULES *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(0,y) -> 0 *(s(x),y) -> +(*(x,y),y) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,0) -> 0 *(x,s(y)) -> +(*(x,y),x) *(x,y) -> *(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(x,y) -> +(y,x) ) Critical Pairs: <+(*(x',+(y,z)),+(y,z)),+(*(s(x'),y),*(s(x'),z))> => Not trivial, Overlay, Proper, NW0, N45 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: No Convergence InfChecker Procedure: Infeasible convergence? YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x y z x1 y1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (+ 1 2) (* 1 2) (0) (c_x1) (c_y) (c_z) (fSNonEmpty) (s 1) ) (RULES +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(x,y) -> +(y,x) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(*(x,y),z) -> *(x,*(y,z)) *(0,y) -> 0 *(s(x),y) -> +(*(x,y),y) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,0) -> 0 *(x,s(y)) -> +(*(x,y),x) *(x,y) -> *(y,x) )] Infeasibility Conditions: +(*(c_x1,+(c_y,c_z)),+(c_y,c_z)) ->* z0, +(*(s(c_x1),c_y),*(s(c_x1),c_z)) ->* z0 Problem 1: Obtaining a model using AGES: -> Theory (Usable Rules): +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(x,y) -> +(y,x) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(*(x,y),z) -> *(x,*(y,z)) *(0,y) -> 0 *(s(x),y) -> +(*(x,y),y) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,0) -> 0 *(x,s(y)) -> +(*(x,y),x) *(x,y) -> *(y,x) -> AGES Output: The problem is infeasible. The problem is not confluent.