(ignored inputs)COMMENT Example 1 of \cite{Tiw02} Rewrite Rules: [ a -> f(a,b), f(a,b) -> f(b,a) ] Apply Direct Methods... Inner CPs: [ f(f(a,b),b) = f(b,a) ] Outer CPs: [ ] not Overlay, check Termination... unknown/not Terminating unknown Knuth&Bendix Linear unknown Development Closed unknown Strongly Closed inner CP cond (upside-parallel) innter CP Cond (outside) unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ f(f(a,b),b) = f(b,a), f(b,a) = f(f(a,b),b) ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <0, 1> preceded by [(f,1)] unknown Diagram Decreasing check by Reduction-Preserving Completion... STEP: 1 (parallel) S: [ a -> f(a,b) ] P: [ f(a,b) -> f(b,a) ] P: not reversible failure(Step 1) STEP: 2 (linear) S: [ a -> f(a,b) ] P: [ f(a,b) -> f(b,a) ] P: not reversible failure(Step 2) STEP: 3 (relative) S: [ a -> f(a,b) ] P: [ f(a,b) -> f(b,a) ] P: not reversible failure(Step 3) failure(no possibility remains) unknown Reduction-Preserving Completion check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ a -> f(a,b), f(a,b) -> f(b,a) ] Sort Assignment: a : =>6 b : =>6 f : 6*6=>6 maximal types: {6} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ a -> f(a,b), f(a,b) -> f(b,a) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ a -> f(a,b), f(a,b) -> f(b,a) ] Inside Critical Pair: by Rules <0, 1> develop reducts from lhs term... <{1}, f(f(b,a),b)> <{0}, f(f(f(a,b),b),b)> <{}, f(f(a,b),b)> develop reducts from rhs term... <{0}, f(b,f(a,b))> <{}, f(b,a)> Commutative Decomposition failed: Can't judge No further decomposition possible Final result: Can't judge /local-scratch/hzankl/2012/cops2012/80.trs: Failure(unknown) (3 msec.)