(ignored inputs)COMMENT Example 3.3.1 of \cite{Gra96thesis}
Rewrite Rules:
   [ b -> a,
     b -> c,
     c -> b,
     c -> d ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ a = c,
     b = d ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ b = d,
     d = b,
     a = c,
     c = a ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <c, a> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <d, b> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], [([],1),([],3)]>
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ b -> a,
     c -> d ]
P:
   [ b -> c,
     c -> b ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<a, c> --> <a, d> => no
<d, b> --> <d, a> => no
check joinability condition:
check modulo joinability of a and d: maybe not joinable
check modulo joinability of d and a: maybe not joinable
failed
failure(Step 1)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ b -> a,
     c -> d ]
P:
   [ b -> c,
     c -> b ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<a, c> --> <a, d> => no
<d, b> --> <d, a> => no
check joinability condition:
check modulo joinability of a and d: maybe not joinable
check modulo joinability of d and a: maybe not joinable
failed
failure(Step 2)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ b -> a,
     c -> d ]
P:
   [ b -> c,
     c -> b ]
Check relative termination:
   [ b -> a,
     c -> d ]
   [ b -> c,
     c -> b ]
Polynomial Interpretation:
  a:= 0
  b:= (1)
  c:= (1)
  d:= (1)
retract b -> a
Polynomial Interpretation:
  a:= 0
  b:= (1)
  c:= (1)
  d:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: <a, d> from c
Not Confluent
Direct Methods: not CR

Final result: not CR
/local-scratch/hzankl/2012/cops2012/38.trs: Success(not CR)
(16 msec.)