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