0.00/0.21 MAYBE 0.00/0.21 (ignored inputs)COMMENT doi:10.1007/3-540-19242-5_3 [49] Example B as join CTRS; correction of Cops #273 submitted by: Thomas Sternagel 0.00/0.21 Conditional Rewrite Rules: 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x) -> g(?x) | h(f(?x)) == k(g(b)) ] 0.00/0.21 Check whether all rules are type 3 0.00/0.21 OK 0.00/0.21 Check whether the input is deterministic 0.00/0.21 OK 0.00/0.21 Result of unraveling: 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 U0(k(g(b)),?x) -> g(?x) ] 0.00/0.21 Check whether U(R) is terminating 0.00/0.21 failed to show termination 0.00/0.21 Check whether the input is weakly left-linear 0.00/0.21 OK 0.00/0.21 Conditional critical pairs (CCPs): 0.00/0.21 [ k(g(b)) = k(f(a)), 0.00/0.21 k(f(a)) = k(g(b)), 0.00/0.21 c = k(f(a)), 0.00/0.21 k(f(a)) = c, 0.00/0.21 h(f(b)) = c, 0.00/0.21 h(g(a)) = c | h(f(a)) == k(g(b)) ] 0.00/0.21 Check whether the input is almost orthogonale 0.00/0.21 not almost orthogonal 0.00/0.21 OK 0.00/0.21 Check U(R) is confluent 0.00/0.21 Rewrite Rules: 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 U0(k(g(b)),?x) -> g(?x) ] 0.00/0.21 Apply Direct Methods... 0.00/0.21 Inner CPs: 0.00/0.21 [ h(f(b)) = c, 0.00/0.21 h(U0(h(f(a)),a)) = c ] 0.00/0.21 Outer CPs: 0.00/0.21 [ k(f(a)) = k(g(b)), 0.00/0.21 k(f(a)) = c ] 0.00/0.21 not Overlay, check Termination... 0.00/0.21 unknown/not Terminating 0.00/0.21 unknown Knuth & Bendix 0.00/0.21 Left-Linear, not Right-Linear 0.00/0.21 unknown Development Closed 0.00/0.21 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow 0.00/0.21 unknown Upside-Parallel-Closed/Outside-Closed 0.00/0.21 (inner) Parallel CPs: (not computed) 0.00/0.21 unknown Toyama (Parallel CPs) 0.00/0.21 Simultaneous CPs: 0.00/0.21 [ k(g(b)) = k(f(a)), 0.00/0.21 k(f(a)) = k(g(b)), 0.00/0.21 c = k(f(a)), 0.00/0.21 k(U0(h(f(b)),b)) = c, 0.00/0.21 k(U0(h(f(a)),a)) = c, 0.00/0.21 k(f(b)) = c, 0.00/0.21 h(U0(h(f(b)),b)) = c, 0.00/0.21 k(f(a)) = c, 0.00/0.21 h(U0(h(f(a)),a)) = c, 0.00/0.21 h(f(b)) = c, 0.00/0.21 c = h(f(b)), 0.00/0.21 c = h(U0(h(f(a)),a)) ] 0.00/0.21 unknown Okui (Simultaneous CPs) 0.00/0.21 unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.21 unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.21 check Locally Decreasing Diagrams by Rule Labelling... 0.00/0.21 Critical Pair by Rules <4, 3> preceded by [(h,1),(f,1)] 0.00/0.21 joinable by a reduction of rules <[([],2)], [([],0),([(k,1),(f,1)],4)]> 0.00/0.21 Critical Pair by Rules <5, 3> preceded by [(h,1)] 0.00/0.21 joinable by a reduction of rules <[([],2)], [([],0),([(k,1)],5)]> 0.00/0.21 Critical Pair by Rules <1, 0> preceded by [] 0.00/0.21 joinable by a reduction of rules <[], [([(k,1)],5),([(k,1),(U0,2)],4),([(k,1),(U0,1)],3),([(k,1),(U0,1)],1),([(k,1)],6)]> 0.00/0.21 joinable by a reduction of rules <[], [([(k,1)],5),([(k,1),(U0,1)],3),([(k,1),(U0,2)],4),([(k,1),(U0,1)],1),([(k,1)],6)]> 0.00/0.21 joinable by a reduction of rules <[], [([(k,1)],5),([(k,1),(U0,1)],3),([(k,1),(U0,1)],1),([(k,1),(U0,2)],4),([(k,1)],6)]> 0.00/0.21 joinable by a reduction of rules <[], [([(k,1)],5),([(k,1),(U0,1)],3),([(k,1),(U0,1)],1),([(k,1)],6),([(k,1),(g,1)],4)]> 0.00/0.21 Critical Pair by Rules <3, 2> preceded by [] 0.00/0.21 joinable by a reduction of rules <[([],0)], []> 0.00/0.21 unknown Diagram Decreasing 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x_1) -> U0(h(f(?x_1)),?x_1), 0.00/0.21 U0(k(g(b)),?x_2) -> g(?x_2) ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>16 0.00/0.21 b : =>16 0.00/0.21 c : =>15 0.00/0.21 f : 16=>18 0.00/0.21 g : 16=>18 0.00/0.21 h : 18=>15 0.00/0.21 k : 18=>15 0.00/0.21 U0 : 15*16=>18 0.00/0.21 non-linear variables: {?x_1} 0.00/0.21 non-linear types: {16} 0.00/0.21 types leq non-linear types: {16} 0.00/0.21 rules applicable to terms of non-linear types: 0.00/0.21 [ a -> b ] 0.00/0.21 Rnl: 0.00/0.21 0: {} 0.00/0.21 1: {} 0.00/0.21 2: {} 0.00/0.21 3: {} 0.00/0.21 4: {} 0.00/0.21 5: {4} 0.00/0.21 6: {} 0.00/0.21 terms of non-linear types are innermost terminating 0.00/0.21 Critical Pair by Rules <4, 3> 0.00/0.21 convertible by a reduction of rules [->(2),(4)<-,(0)<-] 0.00/0.21 convertible by a reduction of rules [->(2),(4)<-,(2)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [->(5),(4)<-,(4)<-,(5)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [(4)<-,->(2),(0)<-] 0.00/0.21 Critical Pair by Rules <5, 3> 0.00/0.21 convertible by a reduction of rules [->(2),->(3),->(1),->(6),->(4),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(2),->(3),->(1),->(4),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(2),->(3),->(4),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(2),->(4),->(3),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(2),(5)<-,(0)<-] 0.00/0.21 convertible by a reduction of rules [->(2),(5)<-,(2)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(2),->(6),->(4),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(2),->(4),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(4),->(6),->(2),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(4),->(2),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(6),->(4),->(2),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(6),->(2),->(4),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(2),->(1),->(6),->(4),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(2),->(1),->(4),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(2),->(4),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(4),->(1),->(6),->(2),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(4),->(1),->(2),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(4),->(2),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(2),->(3),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(3),->(1),->(6),->(2),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(3),->(1),->(2),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(3),->(2),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(4),(5)<-,(4)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [(5)<-,->(2),(0)<-] 0.00/0.21 Critical Pair by Rules <1, 0> 0.00/0.21 convertible by a reduction of rules [(1)<-,(3)<-,->(2)] 0.00/0.21 convertible by a reduction of rules [(4)<-,(6)<-,(1)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(1)<-,(3)<-,(4)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(1)<-,(3)<-,->(4),(5)<-,(4)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(1)<-,(4)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(1)<-,(4)<-,->(0),(2)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(4)<-,(1)<-,(3)<-,(5)<-] 0.00/0.21 Critical Pair by Rules <3, 2> 0.00/0.21 convertible by a reduction of rules [->(0)] 0.00/0.21 convertible by a reduction of rules [->(1),(4)<-,(6)<-,(1)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [->(1),(6)<-,(1)<-,(4)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [->(1),(6)<-,(1)<-,(3)<-,(4)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [->(1),(6)<-,(4)<-,(1)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(3)<-,->(4),->(2),(4)<-] 0.00/0.21 convertible by a reduction of rules [(3)<-,->(5),->(2),(5)<-] 0.00/0.21 Not Satisfiable 0.00/0.21 unknown Quasi-Linear & Linearized-Decreasing 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x_1) -> U0(h(f(?x_1)),?x_1), 0.00/0.21 U0(k(g(b)),?x_2) -> g(?x_2) ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>16 0.00/0.21 b : =>16 0.00/0.21 c : =>15 0.00/0.21 f : 16=>18 0.00/0.21 g : 16=>18 0.00/0.21 h : 18=>15 0.00/0.21 k : 18=>15 0.00/0.21 U0 : 15*16=>18 0.00/0.21 non-linear variables: {?x_1} 0.00/0.21 non-linear types: {16} 0.00/0.21 types leq non-linear types: {16} 0.00/0.21 rules applicable to terms of non-linear types: 0.00/0.21 [ a -> b ] 0.00/0.21 terms of non-linear types are terminating 0.00/0.21 Check Joinablility of CP from NLR: 0.00/0.21 done. 0.00/0.21 Critical Pair by Rules <4, 3> 0.00/0.21 convertible by a reduction of rules [->(2),(4)<-,(0)<-] 0.00/0.21 convertible by a reduction of rules [->(2),(4)<-,(2)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [->(5),(4)<-,(4)<-,(5)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [(4)<-,->(2),(0)<-] 0.00/0.21 Critical Pair by Rules <5, 3> 0.00/0.21 convertible by a reduction of rules [->(2),->(3),->(1),->(6),->(4),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(2),->(3),->(1),->(4),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(2),->(3),->(4),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(2),->(4),->(3),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(2),(5)<-,(0)<-] 0.00/0.21 convertible by a reduction of rules [->(2),(5)<-,(2)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(2),->(6),->(4),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(2),->(4),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(4),->(6),->(2),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(4),->(2),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(6),->(4),->(2),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(1),->(6),->(2),->(4),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(2),->(1),->(6),->(4),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(2),->(1),->(4),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(2),->(4),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(4),->(1),->(6),->(2),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(4),->(1),->(2),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(3),->(4),->(2),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(2),->(3),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(3),->(1),->(6),->(2),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(3),->(1),->(2),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(3),->(2),->(1),->(6),(1)<-] 0.00/0.21 convertible by a reduction of rules [->(4),->(4),(5)<-,(4)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [(5)<-,->(2),(0)<-] 0.00/0.21 Critical Pair by Rules <1, 0> 0.00/0.21 convertible by a reduction of rules [(1)<-,(3)<-,->(2)] 0.00/0.21 convertible by a reduction of rules [(4)<-,(6)<-,(1)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(1)<-,(3)<-,(4)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(1)<-,(3)<-,->(4),(5)<-,(4)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(1)<-,(4)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(1)<-,(4)<-,->(0),(2)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(6)<-,(4)<-,(1)<-,(3)<-,(5)<-] 0.00/0.21 Critical Pair by Rules <3, 2> 0.00/0.21 convertible by a reduction of rules [->(0)] 0.00/0.21 convertible by a reduction of rules [->(1),(4)<-,(6)<-,(1)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [->(1),(6)<-,(1)<-,(4)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [->(1),(6)<-,(1)<-,(3)<-,(4)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [->(1),(6)<-,(4)<-,(1)<-,(3)<-,(5)<-] 0.00/0.21 convertible by a reduction of rules [(3)<-,->(4),->(2),(4)<-] 0.00/0.21 convertible by a reduction of rules [(3)<-,->(5),->(2),(5)<-] 0.00/0.21 Not Satisfiable 0.00/0.21 unknown Strongly Quasi-Linear & Hierarchically Decreasing 0.00/0.21 unknown Huet (modulo AC) 0.00/0.21 check by Reduction-Preserving Completion... 0.00/0.21 failure(empty P) 0.00/0.21 unknown Reduction-Preserving Completion 0.00/0.21 check by Ordered Rewriting... 0.00/0.21 remove redundants rules and split 0.00/0.21 R-part: 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 U0(k(g(b)),?x) -> g(?x) ] 0.00/0.21 E-part: 0.00/0.21 [ ] 0.00/0.21 ...failed to find a suitable LPO. 0.00/0.21 unknown Confluence by Ordered Rewriting 0.00/0.21 Direct Methods: Can't judge 0.00/0.21 0.00/0.21 Try Persistent Decomposition for... 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 U0(k(g(b)),?x) -> g(?x) ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>16 0.00/0.21 b : =>16 0.00/0.21 c : =>15 0.00/0.21 f : 16=>18 0.00/0.21 g : 16=>18 0.00/0.21 h : 18=>15 0.00/0.21 k : 18=>15 0.00/0.21 U0 : 15*16=>18 0.00/0.21 maximal types: {15,16,18} 0.00/0.21 Persistent Decomposition failed: Can't judge 0.00/0.21 0.00/0.21 Try Layer Preserving Decomposition for... 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 U0(k(g(b)),?x) -> g(?x) ] 0.00/0.21 Layer Preserving Decomposition failed: Can't judge 0.00/0.21 0.00/0.21 Try Commutative Decomposition for... 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)), 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b, 0.00/0.21 f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 U0(k(g(b)),?x) -> g(?x) ] 0.00/0.21 Outside Critical Pair: by Rules <1, 0> 0.00/0.21 develop reducts from lhs term... 0.00/0.21 <{}, k(g(b))> 0.00/0.21 develop reducts from rhs term... 0.00/0.21 <{4,5}, k(U0(h(f(b)),b))> 0.00/0.21 <{5}, k(U0(h(f(a)),a))> 0.00/0.21 <{4}, k(f(b))> 0.00/0.21 <{}, k(f(a))> 0.00/0.21 Outside Critical Pair: by Rules <3, 2> 0.00/0.21 develop reducts from lhs term... 0.00/0.21 <{1}, k(g(b))> 0.00/0.21 <{0}, k(f(a))> 0.00/0.21 <{}, c> 0.00/0.21 develop reducts from rhs term... 0.00/0.21 <{4,5}, k(U0(h(f(b)),b))> 0.00/0.21 <{5}, k(U0(h(f(a)),a))> 0.00/0.21 <{4}, k(f(b))> 0.00/0.21 <{}, k(f(a))> 0.00/0.21 Inside Critical Pair: by Rules <4, 3> 0.00/0.21 develop reducts from lhs term... 0.00/0.21 <{2,5}, k(U0(h(f(b)),b))> 0.00/0.21 <{2}, k(f(b))> 0.00/0.21 <{5}, h(U0(h(f(b)),b))> 0.00/0.21 <{}, h(f(b))> 0.00/0.21 develop reducts from rhs term... 0.00/0.21 <{1}, k(g(b))> 0.00/0.21 <{0}, k(f(a))> 0.00/0.21 <{}, c> 0.00/0.21 Inside Critical Pair: by Rules <5, 3> 0.00/0.21 develop reducts from lhs term... 0.00/0.21 <{2,3,4}, k(U0(c,b))> 0.00/0.21 <{2,3}, k(U0(c,a))> 0.00/0.21 <{2,4,5}, k(U0(k(U0(h(f(b)),b)),b))> 0.00/0.21 <{2,4,5}, k(U0(k(U0(h(f(b)),b)),a))> 0.00/0.21 <{2,4,5}, k(U0(k(U0(h(f(a)),a)),b))> 0.00/0.21 <{2,5}, k(U0(k(U0(h(f(a)),a)),a))> 0.00/0.21 <{2,4}, k(U0(k(f(b)),b))> 0.00/0.21 <{2,4}, k(U0(k(f(b)),a))> 0.00/0.21 <{2,4}, k(U0(k(f(a)),b))> 0.00/0.21 <{2}, k(U0(k(f(a)),a))> 0.00/0.21 <{2,4,5}, k(U0(h(U0(h(f(b)),b)),b))> 0.00/0.21 <{2,4,5}, k(U0(h(U0(h(f(b)),b)),a))> 0.00/0.21 <{2,4,5}, k(U0(h(U0(h(f(a)),a)),b))> 0.00/0.21 <{2,5}, k(U0(h(U0(h(f(a)),a)),a))> 0.00/0.21 <{2,4}, k(U0(h(f(b)),b))> 0.00/0.21 <{2,4}, k(U0(h(f(b)),a))> 0.00/0.21 <{2,4}, k(U0(h(f(a)),b))> 0.00/0.21 <{2}, k(U0(h(f(a)),a))> 0.00/0.21 <{3,4}, h(U0(c,b))> 0.00/0.21 <{3}, h(U0(c,a))> 0.00/0.21 <{2,4,5}, h(U0(k(U0(h(f(b)),b)),b))> 0.00/0.21 <{2,4,5}, h(U0(k(U0(h(f(b)),b)),a))> 0.00/0.21 <{2,4,5}, h(U0(k(U0(h(f(a)),a)),b))> 0.00/0.21 <{2,5}, h(U0(k(U0(h(f(a)),a)),a))> 0.00/0.21 <{2,4}, h(U0(k(f(b)),b))> 0.00/0.21 <{2,4}, h(U0(k(f(b)),a))> 0.00/0.21 <{2,4}, h(U0(k(f(a)),b))> 0.00/0.21 <{2}, h(U0(k(f(a)),a))> 0.00/0.21 <{4,5}, h(U0(h(U0(h(f(b)),b)),b))> 0.00/0.21 <{4,5}, h(U0(h(U0(h(f(b)),b)),a))> 0.00/0.21 <{4,5}, h(U0(h(U0(h(f(a)),a)),b))> 0.00/0.21 <{5}, h(U0(h(U0(h(f(a)),a)),a))> 0.00/0.21 <{4}, h(U0(h(f(b)),b))> 0.00/0.21 <{4}, h(U0(h(f(b)),a))> 0.00/0.21 <{4}, h(U0(h(f(a)),b))> 0.00/0.21 <{}, h(U0(h(f(a)),a))> 0.00/0.21 develop reducts from rhs term... 0.00/0.21 <{1}, k(g(b))> 0.00/0.21 <{0}, k(f(a))> 0.00/0.21 <{}, c> 0.00/0.21 Try A Minimal Decomposition {2,0,1}{5,3,4}{6} 0.00/0.21 {2,0,1} 0.00/0.21 (cm)Rewrite Rules: 0.00/0.21 [ h(?x) -> k(?x), 0.00/0.21 c -> k(f(a)), 0.00/0.21 c -> k(g(b)) ] 0.00/0.21 Apply Direct Methods... 0.00/0.21 Inner CPs: 0.00/0.21 [ ] 0.00/0.21 Outer CPs: 0.00/0.21 [ k(f(a)) = k(g(b)) ] 0.00/0.21 Overlay, check Innermost Termination... 0.00/0.21 Innermost Terminating (hence Terminating), not WCR 0.00/0.21 Knuth & Bendix 0.00/0.21 Direct Methods: not CR 0.00/0.21 {5,3,4} 0.00/0.21 (cm)Rewrite Rules: 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b ] 0.00/0.21 Apply Direct Methods... 0.00/0.21 Inner CPs: 0.00/0.21 [ h(U0(h(f(a)),a)) = c, 0.00/0.21 h(f(b)) = c ] 0.00/0.21 Outer CPs: 0.00/0.21 [ ] 0.00/0.21 not Overlay, check Termination... 0.00/0.21 unknown/not Terminating 0.00/0.21 unknown Knuth & Bendix 0.00/0.21 Left-Linear, not Right-Linear 0.00/0.21 unknown Development Closed 0.00/0.21 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow 0.00/0.21 inner CP cond (upside-parallel) 0.00/0.21 innter CP Cond (outside) 0.00/0.21 unknown Upside-Parallel-Closed/Outside-Closed 0.00/0.21 (inner) Parallel CPs: (not computed) 0.00/0.21 unknown Toyama (Parallel CPs) 0.00/0.21 Simultaneous CPs: 0.00/0.21 [ c = h(U0(h(f(a)),a)), 0.00/0.21 h(U0(h(f(b)),b)) = c, 0.00/0.21 h(U0(h(f(a)),a)) = c, 0.00/0.21 h(f(b)) = c, 0.00/0.21 c = h(f(b)) ] 0.00/0.21 unknown Okui (Simultaneous CPs) 0.00/0.21 unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.21 unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.21 check Locally Decreasing Diagrams by Rule Labelling... 0.00/0.21 Critical Pair by Rules <0, 1> preceded by [(h,1)] 0.00/0.21 unknown Diagram Decreasing 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>12 0.00/0.21 b : =>12 0.00/0.21 c : =>13 0.00/0.21 f : 12=>7 0.00/0.21 h : 7=>13 0.00/0.21 U0 : 13*12=>7 0.00/0.21 non-linear variables: {?x} 0.00/0.21 non-linear types: {12} 0.00/0.21 types leq non-linear types: {12} 0.00/0.21 rules applicable to terms of non-linear types: 0.00/0.21 [ a -> b ] 0.00/0.21 Rnl: 0.00/0.21 0: {2} 0.00/0.21 1: {} 0.00/0.21 2: {} 0.00/0.21 terms of non-linear types are innermost terminating 0.00/0.21 Critical Pair by Rules <0, 1> 0.00/0.21 convertible by a reduction of rules [->(2),->(2),(0)<-,(2)<-,->(1)] 0.00/0.21 Critical Pair by Rules <2, 1> 0.00/0.21 convertible by a reduction of rules [->(0),(2)<-,(2)<-,(0)<-,->(1)] 0.00/0.21 Not Satisfiable 0.00/0.21 unknown Quasi-Linear & Linearized-Decreasing 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>12 0.00/0.21 b : =>12 0.00/0.21 c : =>13 0.00/0.21 f : 12=>7 0.00/0.21 h : 7=>13 0.00/0.21 U0 : 13*12=>7 0.00/0.21 non-linear variables: {?x} 0.00/0.21 non-linear types: {12} 0.00/0.21 types leq non-linear types: {12} 0.00/0.21 rules applicable to terms of non-linear types: 0.00/0.21 [ a -> b ] 0.00/0.21 terms of non-linear types are terminating 0.00/0.21 Check Joinablility of CP from NLR: 0.00/0.21 done. 0.00/0.21 Critical Pair by Rules <2, 1> 0.00/0.21 convertible by a reduction of rules [->(0),(2)<-,(2)<-,(0)<-,->(1)] 0.00/0.21 Critical Pair by Rules <0, 1> 0.00/0.21 convertible by a reduction of rules [->(2),->(2),(0)<-,(2)<-,->(1)] 0.00/0.21 Not Satisfiable 0.00/0.21 unknown Strongly Quasi-Linear & Hierarchically Decreasing 0.00/0.21 unknown Huet (modulo AC) 0.00/0.21 check by Reduction-Preserving Completion... 0.00/0.21 failure(empty P) 0.00/0.21 unknown Reduction-Preserving Completion 0.00/0.21 check by Ordered Rewriting... 0.00/0.21 remove redundants rules and split 0.00/0.21 R-part: 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b ] 0.00/0.21 E-part: 0.00/0.21 [ ] 0.00/0.21 ...failed to find a suitable LPO. 0.00/0.21 unknown Confluence by Ordered Rewriting 0.00/0.21 Direct Methods: Can't judge 0.00/0.21 0.00/0.21 Try Persistent Decomposition for... 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>12 0.00/0.21 b : =>12 0.00/0.21 c : =>13 0.00/0.21 f : 12=>7 0.00/0.21 h : 7=>13 0.00/0.21 U0 : 13*12=>7 0.00/0.21 maximal types: {7,12,13} 0.00/0.21 Persistent Decomposition failed: Can't judge 0.00/0.21 0.00/0.21 Try Layer Preserving Decomposition for... 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 h(f(a)) -> c, 0.00/0.21 a -> b ] 0.00/0.21 Layer Preserving Decomposition failed: Can't judge 0.00/0.21 No further decomposition possible 0.00/0.21 0.00/0.21 {6} 0.00/0.21 (cm)Rewrite Rules: 0.00/0.21 [ U0(k(g(b)),?x) -> g(?x) ] 0.00/0.21 Apply Direct Methods... 0.00/0.21 Inner CPs: 0.00/0.21 [ ] 0.00/0.21 Outer CPs: 0.00/0.21 [ ] 0.00/0.21 Overlay, check Innermost Termination... 0.00/0.21 Innermost Terminating (hence Terminating), WCR 0.00/0.21 Knuth & Bendix 0.00/0.21 Direct Methods: CR 0.00/0.21 Try A Minimal Decomposition {0,1}{5,4,2,3}{6} 0.00/0.21 {0,1} 0.00/0.21 (cm)Rewrite Rules: 0.00/0.21 [ c -> k(f(a)), 0.00/0.21 c -> k(g(b)) ] 0.00/0.21 Apply Direct Methods... 0.00/0.21 Inner CPs: 0.00/0.21 [ ] 0.00/0.21 Outer CPs: 0.00/0.21 [ k(f(a)) = k(g(b)) ] 0.00/0.21 Overlay, check Innermost Termination... 0.00/0.21 Innermost Terminating (hence Terminating), not WCR 0.00/0.21 Knuth & Bendix 0.00/0.21 Direct Methods: not CR 0.00/0.21 {5,4,2,3} 0.00/0.21 (cm)Rewrite Rules: 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 a -> b, 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c ] 0.00/0.21 Apply Direct Methods... 0.00/0.21 Inner CPs: 0.00/0.21 [ h(U0(h(f(a)),a)) = c, 0.00/0.21 h(f(b)) = c ] 0.00/0.21 Outer CPs: 0.00/0.21 [ k(f(a)) = c ] 0.00/0.21 not Overlay, check Termination... 0.00/0.21 unknown/not Terminating 0.00/0.21 unknown Knuth & Bendix 0.00/0.21 Left-Linear, not Right-Linear 0.00/0.21 unknown Development Closed 0.00/0.21 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow 0.00/0.21 unknown Upside-Parallel-Closed/Outside-Closed 0.00/0.21 (inner) Parallel CPs: (not computed) 0.00/0.21 unknown Toyama (Parallel CPs) 0.00/0.21 Simultaneous CPs: 0.00/0.21 [ c = h(U0(h(f(a)),a)), 0.00/0.21 c = h(f(b)), 0.00/0.21 c = k(f(a)), 0.00/0.21 k(U0(h(f(b)),b)) = c, 0.00/0.21 k(U0(h(f(a)),a)) = c, 0.00/0.21 k(f(b)) = c, 0.00/0.21 h(U0(h(f(b)),b)) = c, 0.00/0.21 k(f(a)) = c, 0.00/0.21 h(U0(h(f(a)),a)) = c, 0.00/0.21 h(f(b)) = c ] 0.00/0.21 unknown Okui (Simultaneous CPs) 0.00/0.21 unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.21 unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.21 check Locally Decreasing Diagrams by Rule Labelling... 0.00/0.21 Critical Pair by Rules <0, 3> preceded by [(h,1)] 0.00/0.21 unknown Diagram Decreasing 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 a -> b, 0.00/0.21 h(?x_1) -> k(?x_1), 0.00/0.21 h(f(a)) -> c ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>13 0.00/0.21 b : =>13 0.00/0.21 c : =>15 0.00/0.21 f : 13=>10 0.00/0.21 h : 10=>15 0.00/0.21 k : 10=>15 0.00/0.21 U0 : 15*13=>10 0.00/0.21 non-linear variables: {?x} 0.00/0.21 non-linear types: {13} 0.00/0.21 types leq non-linear types: {13} 0.00/0.21 rules applicable to terms of non-linear types: 0.00/0.21 [ a -> b ] 0.00/0.21 Rnl: 0.00/0.21 0: {1} 0.00/0.21 1: {} 0.00/0.21 2: {} 0.00/0.21 3: {} 0.00/0.21 terms of non-linear types are innermost terminating 0.00/0.21 Critical Pair by Rules <0, 3> 0.00/0.21 convertible by a reduction of rules [->(1),->(1),(0)<-,(1)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [->(2),(0)<-,(2)<-,->(3)] 0.00/0.21 Critical Pair by Rules <1, 3> 0.00/0.21 convertible by a reduction of rules [->(0),(1)<-,(1)<-,(0)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [->(2),(1)<-,(2)<-,->(3)] 0.00/0.21 Critical Pair by Rules <3, 2> 0.00/0.21 convertible by a reduction of rules [(3)<-,->(0),->(2),(0)<-] 0.00/0.21 convertible by a reduction of rules [(3)<-,->(1),->(2),(1)<-] 0.00/0.21 Not Satisfiable 0.00/0.21 unknown Quasi-Linear & Linearized-Decreasing 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 a -> b, 0.00/0.21 h(?x_1) -> k(?x_1), 0.00/0.21 h(f(a)) -> c ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>13 0.00/0.21 b : =>13 0.00/0.21 c : =>15 0.00/0.21 f : 13=>10 0.00/0.21 h : 10=>15 0.00/0.21 k : 10=>15 0.00/0.21 U0 : 15*13=>10 0.00/0.21 non-linear variables: {?x} 0.00/0.21 non-linear types: {13} 0.00/0.21 types leq non-linear types: {13} 0.00/0.21 rules applicable to terms of non-linear types: 0.00/0.21 [ a -> b ] 0.00/0.21 terms of non-linear types are terminating 0.00/0.21 Check Joinablility of CP from NLR: 0.00/0.21 done. 0.00/0.21 Critical Pair by Rules <1, 3> 0.00/0.21 convertible by a reduction of rules [->(0),(1)<-,(1)<-,(0)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [->(2),(1)<-,(2)<-,->(3)] 0.00/0.21 Critical Pair by Rules <0, 3> 0.00/0.21 convertible by a reduction of rules [->(1),->(1),(0)<-,(1)<-,->(3)] 0.00/0.21 convertible by a reduction of rules [->(2),(0)<-,(2)<-,->(3)] 0.00/0.21 Critical Pair by Rules <3, 2> 0.00/0.21 convertible by a reduction of rules [(3)<-,->(0),->(2),(0)<-] 0.00/0.21 convertible by a reduction of rules [(3)<-,->(1),->(2),(1)<-] 0.00/0.21 Not Satisfiable 0.00/0.21 unknown Strongly Quasi-Linear & Hierarchically Decreasing 0.00/0.21 unknown Huet (modulo AC) 0.00/0.21 check by Reduction-Preserving Completion... 0.00/0.21 failure(empty P) 0.00/0.21 unknown Reduction-Preserving Completion 0.00/0.21 check by Ordered Rewriting... 0.00/0.21 remove redundants rules and split 0.00/0.21 R-part: 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 a -> b, 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c ] 0.00/0.21 E-part: 0.00/0.21 [ ] 0.00/0.21 ...failed to find a suitable LPO. 0.00/0.21 unknown Confluence by Ordered Rewriting 0.00/0.21 Direct Methods: Can't judge 0.00/0.21 0.00/0.21 Try Persistent Decomposition for... 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 a -> b, 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c ] 0.00/0.21 Sort Assignment: 0.00/0.21 a : =>13 0.00/0.21 b : =>13 0.00/0.21 c : =>15 0.00/0.21 f : 13=>10 0.00/0.21 h : 10=>15 0.00/0.21 k : 10=>15 0.00/0.21 U0 : 15*13=>10 0.00/0.21 maximal types: {10,13,15} 0.00/0.21 Persistent Decomposition failed: Can't judge 0.00/0.21 0.00/0.21 Try Layer Preserving Decomposition for... 0.00/0.21 [ f(?x) -> U0(h(f(?x)),?x), 0.00/0.21 a -> b, 0.00/0.21 h(?x) -> k(?x), 0.00/0.21 h(f(a)) -> c ] 0.00/0.21 Layer Preserving Decomposition failed: Can't judge 0.00/0.21 No further decomposition possible 0.00/0.21 0.00/0.21 {6} 0.00/0.21 (cm)Rewrite Rules: 0.00/0.21 [ U0(k(g(b)),?x) -> g(?x) ] 0.00/0.21 Apply Direct Methods... 0.00/0.21 Inner CPs: 0.00/0.21 [ ] 0.00/0.21 Outer CPs: 0.00/0.21 [ ] 0.00/0.21 Overlay, check Innermost Termination... 0.00/0.21 Innermost Terminating (hence Terminating), WCR 0.00/0.21 Knuth & Bendix 0.00/0.21 Direct Methods: CR 0.00/0.21 Commutative Decomposition failed: Can't judge 0.00/0.21 No further decomposition possible 0.00/0.21 0.00/0.21 0.00/0.21 Combined result: Can't judge 0.00/0.21 failed to show confluence of U(R) 0.00/0.21 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR) 0.00/0.21 (97 msec.) 0.00/0.21 EOF