(ignored inputs)COMMENT doi:10.1007/978-3-319-63046-5_24 [118] Example 4 submitted by: Aart Middeldorp
Rewrite Rules:
   [ +(a,b) -> b,
     +(c,a) -> a,
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ +(b,?z_1) = +(a,+(b,?z_1)),
     +(a,?z_1) = +(c,+(a,?z_1)),
     +(+(?y,?x),?z_1) = +(?x,+(?y,?z_1)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ b = +(b,a),
     a = +(a,c),
     +(?y,+(?x_1,?y_1)) = +(?x_1,+(?y_1,?y)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly 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:
   [ +(b,a) = b,
     +(a,+(b,?z_1)) = +(b,?z_1),
     +(a,c) = a,
     +(c,+(a,?z_1)) = +(a,?z_1),
     b = +(b,a),
     a = +(a,c),
     +(?x_1,+(?y_1,?y)) = +(?y,+(?x_1,?y_1)),
     +(?x,+(?y,?z_2)) = +(+(?y,?x),?z_2),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,b) = +(a,+(b,?z)),
     +(?z,a) = +(c,+(a,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(b,?z) = +(a,+(b,?z)),
     +(a,?z) = +(c,+(a,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(b,+(?z,?z_1)) = +(+(a,+(b,?z)),?z_1),
     +(a,+(?z,?z_1)) = +(+(c,+(a,?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1) ]
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 <+(b,?z_1), +(a,+(b,?z_1))> by Rules <0, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[([],2)], [([(+,2)],2),([],2),([],3),([(+,2)],2),([(+,2)],0)]>
 joinable by a reduction of rules <[([],2)], [([],2),([(+,1)],2),([],3),([(+,2)],2),([(+,2)],0)]>
 joinable by a reduction of rules <[([],2)], [([],2),([],3),([],2),([],3),([(+,2)],0)]>
Critical Pair <+(a,?z_1), +(c,+(a,?z_1))> by Rules <1, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[([],2)], [([(+,2)],2),([],2),([],3),([(+,2)],2),([(+,2)],1)]>
 joinable by a reduction of rules <[([],2)], [([],2),([(+,1)],2),([],3),([(+,2)],2),([(+,2)],1)]>
 joinable by a reduction of rules <[([],2)], [([],2),([],3),([],2),([],3),([(+,2)],1)]>
Critical Pair <+(+(?y,?x),?z_1), +(?x,+(?y,?z_1))> by Rules <2, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],2),([],3)], []>
 joinable by a reduction of rules <[([],3),([(+,2)],2)], [([],2),([],3)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <3, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[([],3),([(+,2)],3)], [([],3)]>
Critical Pair <+(b,a), b> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <+(a,c), a> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <+(?x_1,+(?y_1,?z_1)), +(?z_1,+(?x_1,?y_1))> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], [([],2),([],3)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 9 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
Check relative termination:
   [ +(a,b) -> b,
     +(c,a) -> a ]
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (2)+(1)*x1+(1)*x2
  a:= (7)
  b:= 0
  c:= 0
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(a,b) -> b,
     +(c,a) -> a ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<+(b,?z), +(a,+(b,?z))> --> <+(b,?z), +(a,+(b,?z))> => no
<b, +(b,a)> --> <b, +(b,a)> => no
<+(?x,b), +(+(?x,a),b)> --> <+(?x,b), +(+(?x,a),b)> => no
<+(a,?z), +(c,+(a,?z))> --> <+(a,?z), +(c,+(a,?z))> => no
<a, +(a,c)> --> <a, +(a,c)> => no
<+(?x,a), +(+(?x,c),a)> --> <+(?x,a), +(+(?x,c),a)> => no
check joinability condition:
check modulo reachablity from +(b,?z) to +(a,+(b,?z)): maybe not reachable
check modulo reachablity from b to +(b,a): maybe not reachable
check modulo reachablity from +(?x,b) to +(+(?x,a),b): maybe not reachable
check modulo reachablity from +(a,?z) to +(c,+(a,?z)): maybe not reachable
check modulo reachablity from a to +(a,c): maybe not reachable
check modulo reachablity from +(?x,a) to +(+(?x,c),a): maybe not reachable
failed
failure(Step 1)
   [ +(b,a) -> b,
     +(a,c) -> a ]
Added S-Rules:
   [ +(b,a) -> b,
     +(a,c) -> a ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ +(a,b) -> b,
     +(c,a) -> a ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<+(b,?z), +(a,+(b,?z))> --> <+(b,?z), +(a,+(b,?z))> => no
<b, +(b,a)> --> <b, +(b,a)> => no
<+(?x,b), +(+(?x,a),b)> --> <+(?x,b), +(+(?x,a),b)> => no
<+(a,?z), +(c,+(a,?z))> --> <+(a,?z), +(c,+(a,?z))> => no
<a, +(a,c)> --> <a, +(a,c)> => no
<+(?x,a), +(+(?x,c),a)> --> <+(?x,a), +(+(?x,c),a)> => no
check joinability condition:
check modulo reachablity from +(b,?z) to +(a,+(b,?z)): maybe not reachable
check modulo reachablity from b to +(b,a): maybe not reachable
check modulo reachablity from +(?x,b) to +(+(?x,a),b): maybe not reachable
check modulo reachablity from +(a,?z) to +(c,+(a,?z)): maybe not reachable
check modulo reachablity from a to +(a,c): maybe not reachable
check modulo reachablity from +(?x,a) to +(+(?x,c),a): maybe not reachable
failed
failure(Step 2)
   [ +(b,a) -> b,
     +(a,c) -> a ]
Added S-Rules:
   [ +(b,a) -> b,
     +(a,c) -> a ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ +(a,b) -> b,
     +(c,a) -> a ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Check relative termination:
   [ +(a,b) -> b,
     +(c,a) -> a ]
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (2)+(1)*x1+(1)*x2
  a:= (7)
  b:= 0
  c:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ +(a,b) -> b,
     +(c,a) -> a,
     +(b,a) -> b,
     +(a,c) -> a ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<+(b,?z), +(a,+(b,?z))> --> <+(b,?z), +(a,+(b,?z))> => no
<b, +(b,a)> --> <b, b> => yes
<+(?x,b), +(+(?x,a),b)> --> <+(?x,b), +(+(?x,a),b)> => no
<+(a,?z), +(c,+(a,?z))> --> <+(a,?z), +(c,+(a,?z))> => no
<a, +(a,c)> --> <a, a> => yes
<+(?x,a), +(+(?x,c),a)> --> <+(?x,a), +(+(?x,c),a)> => no
<+(b,?z), +(b,+(a,?z))> --> <+(b,?z), +(b,+(a,?z))> => no
<b, +(a,b)> --> <b, b> => yes
<+(?x,b), +(+(?x,b),a)> --> <+(?x,b), +(+(?x,b),a)> => no
<+(a,?z), +(a,+(c,?z))> --> <+(a,?z), +(a,+(c,?z))> => no
<a, +(c,a)> --> <a, a> => yes
<+(?x,a), +(+(?x,a),c)> --> <+(?x,a), +(+(?x,a),c)> => no
check joinability condition:
check modulo reachablity from +(b,?z) to +(a,+(b,?z)): maybe not reachable
check modulo reachablity from +(?x,b) to +(+(?x,a),b): maybe not reachable
check modulo reachablity from +(a,?z) to +(c,+(a,?z)): maybe not reachable
check modulo reachablity from +(?x,a) to +(+(?x,c),a): maybe not reachable
check modulo reachablity from +(b,?z) to +(b,+(a,?z)): maybe not reachable
check modulo reachablity from +(?x,b) to +(+(?x,b),a): maybe not reachable
check modulo reachablity from +(a,?z) to +(a,+(c,?z)): maybe not reachable
check modulo reachablity from +(?x,a) to +(+(?x,a),c): maybe not reachable
failed
failure(Step 4)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 5 (linear)
S:
   [ +(a,b) -> b,
     +(c,a) -> a,
     +(b,a) -> b,
     +(a,c) -> a ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<+(b,?z), +(a,+(b,?z))> --> <+(b,?z), +(a,+(b,?z))> => no
<b, +(b,a)> --> <b, b> => yes
<+(?x,b), +(+(?x,a),b)> --> <+(?x,b), +(+(?x,a),b)> => no
<+(a,?z), +(c,+(a,?z))> --> <+(a,?z), +(c,+(a,?z))> => no
<a, +(a,c)> --> <a, a> => yes
<+(?x,a), +(+(?x,c),a)> --> <+(?x,a), +(+(?x,c),a)> => no
<+(b,?z), +(b,+(a,?z))> --> <+(b,?z), +(b,+(a,?z))> => no
<b, +(a,b)> --> <b, b> => yes
<+(?x,b), +(+(?x,b),a)> --> <+(?x,b), +(+(?x,b),a)> => no
<+(a,?z), +(a,+(c,?z))> --> <+(a,?z), +(a,+(c,?z))> => no
<a, +(c,a)> --> <a, a> => yes
<+(?x,a), +(+(?x,a),c)> --> <+(?x,a), +(+(?x,a),c)> => no
check joinability condition:
check modulo reachablity from +(b,?z) to +(a,+(b,?z)): maybe not reachable
check modulo reachablity from +(?x,b) to +(+(?x,a),b): maybe not reachable
check modulo reachablity from +(a,?z) to +(c,+(a,?z)): maybe not reachable
check modulo reachablity from +(?x,a) to +(+(?x,c),a): maybe not reachable
check modulo reachablity from +(b,?z) to +(b,+(a,?z)): maybe not reachable
check modulo reachablity from +(?x,b) to +(+(?x,b),a): maybe not reachable
check modulo reachablity from +(a,?z) to +(a,+(c,?z)): maybe not reachable
check modulo reachablity from +(?x,a) to +(+(?x,a),c): maybe not reachable
failed
failure(Step 5)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 6 (relative)
S:
   [ +(a,b) -> b,
     +(c,a) -> a,
     +(b,a) -> b,
     +(a,c) -> a ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Check relative termination:
   [ +(a,b) -> b,
     +(c,a) -> a,
     +(b,a) -> b,
     +(a,c) -> a ]
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  a:= 0
  b:= 0
  c:= (5)
retract +(c,a) -> a
retract +(a,c) -> a
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  a:= (8)
  b:= 0
  c:= (9)
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ +(a,b) -> b,
     +(c,a) -> a,
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Sort Assignment:
 + : 12*12=>12
 a : =>12
 b : =>12
 c : =>12
maximal types: {12}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ +(a,b) -> b,
     +(c,a) -> a,
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ +(a,b) -> b,
     +(c,a) -> a,
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Outside Critical Pair: <+(b,a), b> by Rules <2, 0>
develop reducts from lhs term...
<{2}, +(a,b)>
<{}, +(b,a)>
develop reducts from rhs term...
<{}, b>
Outside Critical Pair: <+(a,c), a> by Rules <2, 1>
develop reducts from lhs term...
<{2}, +(c,a)>
<{}, +(a,c)>
develop reducts from rhs term...
<{}, a>
Outside Critical Pair: <+(?x_1,+(?y_1,?z_1)), +(?z_1,+(?x_1,?y_1))> by Rules <3, 2>
develop reducts from lhs term...
<{2}, +(+(?z_1,?y_1),?x_1)>
<{2}, +(+(?y_1,?z_1),?x_1)>
<{2}, +(?x_1,+(?z_1,?y_1))>
<{}, +(?x_1,+(?y_1,?z_1))>
develop reducts from rhs term...
<{2}, +(+(?y_1,?x_1),?z_1)>
<{2}, +(+(?x_1,?y_1),?z_1)>
<{2}, +(?z_1,+(?y_1,?x_1))>
<{}, +(?z_1,+(?x_1,?y_1))>
Inside Critical Pair: <+(b,?z_1), +(a,+(b,?z_1))> by Rules <0, 3>
develop reducts from lhs term...
<{2}, +(?z_1,b)>
<{}, +(b,?z_1)>
develop reducts from rhs term...
<{2}, +(+(?z_1,b),a)>
<{2}, +(+(b,?z_1),a)>
<{2}, +(a,+(?z_1,b))>
<{}, +(a,+(b,?z_1))>
Inside Critical Pair: <+(a,?z_1), +(c,+(a,?z_1))> by Rules <1, 3>
develop reducts from lhs term...
<{2}, +(?z_1,a)>
<{}, +(a,?z_1)>
develop reducts from rhs term...
<{2}, +(+(?z_1,a),c)>
<{2}, +(+(a,?z_1),c)>
<{2}, +(c,+(?z_1,a))>
<{}, +(c,+(a,?z_1))>
Inside Critical Pair: <+(+(?y,?x),?z_1), +(?x,+(?y,?z_1))> by Rules <2, 3>
develop reducts from lhs term...
<{3}, +(?y,+(?x,?z_1))>
<{2}, +(?z_1,+(?x,?y))>
<{2}, +(?z_1,+(?y,?x))>
<{2}, +(+(?x,?y),?z_1)>
<{}, +(+(?y,?x),?z_1)>
develop reducts from rhs term...
<{2}, +(+(?z_1,?y),?x)>
<{2}, +(+(?y,?z_1),?x)>
<{2}, +(?x,+(?z_1,?y))>
<{}, +(?x,+(?y,?z_1))>
Commutative Decomposition failed: Can't judge
No further decomposition possible


Combined result: Can't judge
541.trs: Failure(unknown CR)
MAYBE
(2645 msec.)