0.014/0.014 NO 0.014/0.014 0.014/0.014 Problem 1: 0.014/0.014 0.014/0.014 0.014/0.014 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.014/0.014 Confluence Problem: 0.014/0.014 (VAR vNonEmpty:S X:S Y:S) 0.014/0.014 (STRATEGY CONTEXTSENSITIVE 0.014/0.014 (diff 1 2) 0.014/0.014 (if 1) 0.014/0.014 (leq 1 2) 0.014/0.014 (p 1) 0.014/0.014 (0) 0.014/0.014 (fSNonEmpty) 0.014/0.014 (false) 0.014/0.014 (s 1) 0.014/0.014 (true) 0.014/0.014 ) 0.014/0.014 (RULES 0.014/0.014 diff(X:S,Y:S) -> if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S))) 0.014/0.014 if(false,X:S,Y:S) -> Y:S 0.014/0.014 if(true,X:S,Y:S) -> X:S 0.014/0.014 leq(0,Y:S) -> true 0.014/0.014 leq(s(X:S),0) -> false 0.014/0.014 leq(s(X:S),s(Y:S)) -> leq(X:S,Y:S) 0.014/0.014 p(0) -> 0 0.014/0.014 p(s(X:S)) -> X:S 0.014/0.014 ) 0.014/0.014 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.014/0.014 0.014/0.014 0.014/0.014 Problem 1: 0.014/0.014 0.014/0.014 CleanTRS Processor: 0.014/0.014 0.014/0.014 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.014/0.014 Confluence Problem: 0.014/0.014 (VAR vNonEmpty:S X:S Y:S) 0.014/0.014 (STRATEGY CONTEXTSENSITIVE 0.014/0.014 (diff 1 2) 0.014/0.014 (if 1) 0.014/0.014 (leq 1 2) 0.014/0.014 (p 1) 0.014/0.014 (0) 0.014/0.014 (fSNonEmpty) 0.014/0.014 (false) 0.014/0.014 (s 1) 0.014/0.014 (true) 0.014/0.014 ) 0.014/0.014 (RULES 0.014/0.014 diff(X:S,Y:S) -> if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S))) 0.014/0.014 if(false,X:S,Y:S) -> Y:S 0.014/0.014 if(true,X:S,Y:S) -> X:S 0.014/0.014 leq(0,Y:S) -> true 0.014/0.014 leq(s(X:S),0) -> false 0.014/0.014 leq(s(X:S),s(Y:S)) -> leq(X:S,Y:S) 0.014/0.014 p(0) -> 0 0.014/0.014 p(s(X:S)) -> X:S 0.014/0.014 ) 0.014/0.014 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.014/0.014 0.014/0.014 0.014/0.014 Problem 1: 0.014/0.014 0.014/0.014 Modular Confluence Combinations Decomposition Processor: 0.014/0.014 It is a CTRS -> No modular confluence 0.014/0.014 0.014/0.014 Problem 1: 0.014/0.014 CS-TRS Processor: 0.014/0.014 R is a CS-TRS 0.014/0.014 0.014/0.014 Problem 1: 0.014/0.014 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.014/0.014 Confluence Problem: 0.014/0.014 (VAR vNonEmpty:S X:S Y:S) 0.014/0.014 (STRATEGY CONTEXTSENSITIVE 0.014/0.014 (diff 1 2) 0.014/0.014 (if 1) 0.014/0.014 (leq 1 2) 0.014/0.014 (p 1) 0.014/0.014 (0) 0.014/0.014 (fSNonEmpty) 0.014/0.014 (false) 0.014/0.014 (s 1) 0.014/0.014 (true) 0.014/0.014 ) 0.014/0.014 (RULES 0.014/0.014 diff(X:S,Y:S) -> if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S))) 0.014/0.014 if(false,X:S,Y:S) -> Y:S 0.014/0.014 if(true,X:S,Y:S) -> X:S 0.014/0.014 leq(0,Y:S) -> true 0.014/0.014 leq(s(X:S),0) -> false 0.014/0.014 leq(s(X:S),s(Y:S)) -> leq(X:S,Y:S) 0.014/0.014 p(0) -> 0 0.014/0.014 p(s(X:S)) -> X:S 0.014/0.014 ) 0.014/0.014 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.014/0.014 0.014/0.014 Extended u-Critical Pairs NonLHRV Processor [JLAMP21]: 0.014/0.014 ->Extended u-Critical Pair: 0.014/0.014 Rule 1 (l :-> r) => diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))) 0.014/0.014 Rule 1 (l' :-> r') => diff(X:S,Y:S) -> if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S))) 0.014/0.014 Var => x3:S 0.014/0.014 Pos x3:S in l => [1] 0.014/0.014 Sigma => {x3:S -> diff(X:S,Y:S)} 0.014/0.014 s => if(leq(diff(X:S,Y:S),x4:S),0,s(diff(p(diff(X:S,Y:S)),x4:S))) 0.014/0.014 t => diff(if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S))),x4:S) 0.014/0.014 NW => 0 0.014/0.014 0.014/0.014 0.014/0.014 ->Extended u-Critical Pair: 0.014/0.014 Rule 1 (l :-> r) => diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))) 0.014/0.014 Rule 2 (l' :-> r') => if(false,X:S,Y:S) -> Y:S 0.014/0.014 Var => x3:S 0.014/0.014 Pos x3:S in l => [1] 0.014/0.014 Sigma => {x3:S -> if(false,X:S,Y:S)} 0.014/0.014 s => if(leq(if(false,X:S,Y:S),x4:S),0,s(diff(p(if(false,X:S,Y:S)),x4:S))) 0.014/0.014 t => diff(Y:S,x4:S) 0.014/0.014 NW => 0 0.014/0.014 0.014/0.014 0.014/0.014 ->Extended u-Critical Pair: 0.014/0.014 Rule 1 (l :-> r) => diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))) 0.014/0.014 Rule 3 (l' :-> r') => if(true,X:S,Y:S) -> X:S 0.014/0.014 Var => x3:S 0.014/0.014 Pos x3:S in l => [1] 0.014/0.014 Sigma => {x3:S -> if(true,X:S,Y:S)} 0.014/0.014 s => if(leq(if(true,X:S,Y:S),x4:S),0,s(diff(p(if(true,X:S,Y:S)),x4:S))) 0.014/0.014 t => diff(X:S,x4:S) 0.014/0.014 NW => 0 0.014/0.014 0.014/0.014 0.014/0.014 ->Extended u-Critical Pair: 0.014/0.014 Rule 1 (l :-> r) => diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))) 0.014/0.014 Rule 4 (l' :-> r') => leq(0,Y:S) -> true 0.014/0.014 Var => x3:S 0.014/0.014 Pos x3:S in l => [1] 0.014/0.014 Sigma => {x3:S -> leq(0,Y:S)} 0.014/0.014 s => if(leq(leq(0,Y:S),x4:S),0,s(diff(p(leq(0,Y:S)),x4:S))) 0.014/0.014 t => diff(true,x4:S) 0.014/0.014 NW => 0 0.014/0.014 0.014/0.014 0.014/0.014 ->Extended u-Critical Pair: 0.014/0.014 Rule 1 (l :-> r) => diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))) 0.014/0.014 Rule 5 (l' :-> r') => leq(s(X:S),0) -> false 0.014/0.014 Var => x3:S 0.014/0.014 Pos x3:S in l => [1] 0.014/0.014 Sigma => {x3:S -> leq(s(X:S),0)} 0.014/0.014 s => if(leq(leq(s(X:S),0),x4:S),0,s(diff(p(leq(s(X:S),0)),x4:S))) 0.014/0.014 t => diff(false,x4:S) 0.014/0.014 NW => 0 0.014/0.014 0.014/0.014 0.014/0.014 ->Extended u-Critical Pair: 0.014/0.014 Rule 1 (l :-> r) => diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))) 0.014/0.014 Rule 6 (l' :-> r') => leq(s(X:S),s(Y:S)) -> leq(X:S,Y:S) 0.014/0.014 Var => x3:S 0.014/0.014 Pos x3:S in l => [1] 0.014/0.014 Sigma => {x3:S -> leq(s(X:S),s(Y:S))} 0.014/0.014 s => if(leq(leq(s(X:S),s(Y:S)),x4:S),0,s(diff(p(leq(s(X:S),s(Y:S))),x4:S))) 0.014/0.014 t => diff(leq(X:S,Y:S),x4:S) 0.014/0.014 NW => 0 0.014/0.014 0.014/0.014 0.014/0.014 ->Extended u-Critical Pair: 0.014/0.014 Rule 1 (l :-> r) => diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))) 0.014/0.014 Rule 7 (l' :-> r') => p(0) -> 0 0.014/0.014 Var => x3:S 0.014/0.014 Pos x3:S in l => [1] 0.014/0.014 Sigma => {x3:S -> p(0)} 0.014/0.014 s => if(leq(p(0),x4:S),0,s(diff(p(p(0)),x4:S))) 0.014/0.014 t => diff(0,x4:S) 0.014/0.014 NW => 0 0.014/0.014 0.014/0.014 0.014/0.014 ->Extended u-Critical Pair: 0.014/0.014 Rule 1 (l :-> r) => diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))) 0.014/0.014 Rule 8 (l' :-> r') => p(s(X:S)) -> X:S 0.014/0.014 Var => x3:S 0.014/0.014 Pos x3:S in l => [1] 0.014/0.014 Sigma => {x3:S -> p(s(X:S))} 0.014/0.014 s => if(leq(p(s(X:S)),x4:S),0,s(diff(p(p(s(X:S))),x4:S))) 0.014/0.014 t => diff(X:S,x4:S) 0.014/0.014 NW => 0 0.014/0.014 0.014/0.014 0.014/0.014 Problem 1: 0.014/0.014 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.014/0.014 Confluence Problem: 0.014/0.014 (VAR vNonEmpty:S X:S Y:S) 0.014/0.014 (STRATEGY CONTEXTSENSITIVE 0.014/0.014 (diff 1 2) 0.014/0.014 (if 1) 0.014/0.014 (leq 1 2) 0.014/0.014 (p 1) 0.014/0.014 (0) 0.014/0.014 (fSNonEmpty) 0.014/0.014 (false) 0.014/0.014 (s 1) 0.014/0.014 (true) 0.014/0.014 ) 0.014/0.014 (RULES 0.014/0.014 diff(X:S,Y:S) -> if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S))) 0.014/0.014 if(false,X:S,Y:S) -> Y:S 0.014/0.014 if(true,X:S,Y:S) -> X:S 0.014/0.014 leq(0,Y:S) -> true 0.014/0.014 leq(s(X:S),0) -> false 0.014/0.014 leq(s(X:S),s(Y:S)) -> leq(X:S,Y:S) 0.014/0.014 p(0) -> 0 0.014/0.014 p(s(X:S)) -> X:S 0.014/0.014 ) 0.014/0.014 Critical Pairs: 0.014/0.014 => Not trivial, Not overlay, NW0, N1 0.014/0.014 => Not trivial, Not overlay, NW0, N2 0.014/0.014 => Not trivial, Not overlay, NW0, N3 0.014/0.014 => Not trivial, Not overlay, NW0, N4 0.014/0.014 => Not trivial, Not overlay, NW0, N5 0.014/0.014 => Not trivial, Not overlay, NW0, N6 0.014/0.014 => Not trivial, Not overlay, NW0, N7 0.014/0.014 => Not trivial, Not overlay, NW0, N8 0.014/0.014 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.014/0.014 0.014/0.014 Huet Levy Processor: 0.014/0.014 -> Rules: 0.014/0.014 diff(X:S,Y:S) -> if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S))) 0.014/0.014 if(false,X:S,Y:S) -> Y:S 0.014/0.014 if(true,X:S,Y:S) -> X:S 0.014/0.014 leq(0,Y:S) -> true 0.014/0.014 leq(s(X:S),0) -> false 0.014/0.014 leq(s(X:S),s(Y:S)) -> leq(X:S,Y:S) 0.014/0.014 p(0) -> 0 0.014/0.014 p(s(X:S)) -> X:S 0.014/0.014 -> Vars: 0.014/0.014 X, Y, X, Y, X, Y, Y, X, X, Y, X 0.014/0.014 -> UVars: 0.014/0.014 (UV-RuleId: 1, UV-LActive: [X, Y], UV-RActive: [X, Y], UV-LFrozen: [], UV-RFrozen: [X, Y]) 0.014/0.014 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [Y], UV-LFrozen: [X, Y], UV-RFrozen: []) 0.014/0.014 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X, Y], UV-RFrozen: []) 0.014/0.014 (UV-RuleId: 4, UV-LActive: [Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.014/0.014 (UV-RuleId: 5, UV-LActive: [X], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.014/0.014 (UV-RuleId: 6, UV-LActive: [X, Y], UV-RActive: [X, Y], UV-LFrozen: [], UV-RFrozen: []) 0.014/0.014 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.014/0.014 (UV-RuleId: 8, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: []) 0.014/0.014 -> FVars: 0.014/0.014 x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 0.014/0.014 -> PVars: 0.014/0.014 X: [x3, x5, x7, x10, x11, x13], Y: [x4, x6, x8, x9, x12] 0.014/0.014 0.014/0.014 -> Rlps: 0.014/0.014 (rule: diff(x3:S,x4:S) -> if(leq(x3:S,x4:S),0,s(diff(p(x3:S),x4:S))), id: 1, possubterms: diff(x3:S,x4:S)->[]) 0.014/0.014 (rule: if(false,x5:S,x6:S) -> x6:S, id: 2, possubterms: if(false,x5:S,x6:S)->[], false->[1]) 0.014/0.014 (rule: if(true,x7:S,x8:S) -> x7:S, id: 3, possubterms: if(true,x7:S,x8:S)->[], true->[1]) 0.014/0.014 (rule: leq(0,x9:S) -> true, id: 4, possubterms: leq(0,x9:S)->[], 0->[1]) 0.014/0.014 (rule: leq(s(x10:S),0) -> false, id: 5, possubterms: leq(s(x10:S),0)->[], s(x10:S)->[1], 0->[2]) 0.014/0.014 (rule: leq(s(x11:S),s(x12:S)) -> leq(x11:S,x12:S), id: 6, possubterms: leq(s(x11:S),s(x12:S))->[], s(x11:S)->[1], s(x12:S)->[2]) 0.014/0.014 (rule: p(0) -> 0, id: 7, possubterms: p(0)->[], 0->[1]) 0.014/0.014 (rule: p(s(x13:S)) -> x13:S, id: 8, possubterms: p(s(x13:S))->[], s(x13:S)->[1]) 0.014/0.014 0.014/0.014 -> Unifications: 0.014/0.014 0.014/0.014 0.014/0.014 -> Critical pairs info: 0.014/0.014 => Not trivial, Not overlay, NW0, N1 0.014/0.014 => Not trivial, Not overlay, NW0, N2 0.014/0.014 => Not trivial, Not overlay, NW0, N3 0.014/0.014 => Not trivial, Not overlay, NW0, N4 0.014/0.014 => Not trivial, Not overlay, NW0, N5 0.014/0.014 => Not trivial, Not overlay, NW0, N6 0.014/0.014 => Not trivial, Not overlay, NW0, N7 0.014/0.014 => Not trivial, Not overlay, NW0, N8 0.014/0.014 0.014/0.014 -> Problem conclusions: 0.014/0.014 Left linear, Not right linear, Not linear 0.014/0.014 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.014/0.014 Not Huet-Levy confluent, Not Newman confluent 0.014/0.014 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.014/0.014 0.014/0.014 0.014/0.014 Problem 1: 0.014/0.014 No Convergence Brute Force Processor: 0.014/0.014 -> Rewritings: 0.014/0.014 s: if(leq(if(true,X:S,Y:S),Y:S),0,s(diff(p(if(true,X:S,Y:S)),Y:S))) 0.014/0.014 Nodes: [0,1] 0.014/0.014 Edges: [(0,1)] 0.014/0.014 ID: 0 => ('if(leq(if(true,X:S,Y:S),Y:S),0,s(diff(p(if(true,X:S,Y:S)),Y:S)))', D0) 0.014/0.014 ID: 1 => ('if(leq(X:S,Y:S),0,s(diff(p(if(true,X:S,Y:S)),Y:S)))', D1, R3, P[1, 1], S{x7:S -> X:S, x8:S -> Y:S}), NR: 'X:S' 0.014/0.014 t: diff(X:S,Y:S) 0.014/0.014 Nodes: [0,1] 0.014/0.014 Edges: [(0,1)] 0.014/0.014 ID: 0 => ('diff(X:S,Y:S)', D0) 0.014/0.014 ID: 1 => ('if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S)))', D1, R1, P[], S{x3:S -> X:S, x4:S -> Y:S}), NR: 'if(leq(X:S,Y:S),0,s(diff(p(X:S),Y:S)))' 0.014/0.014 if(leq(if(true,X:S,Y:S),Y:S),0,s(diff(p(if(true,X:S,Y:S)),Y:S))) ->* no union *<- diff(X:S,Y:S) 0.014/0.014 "Not joinable" 0.014/0.014 0.014/0.014 The problem is not joinable. 0.014/0.014 0.20user 0.03system 0:00.14elapsed 169%CPU (0avgtext+0avgdata 15624maxresident)k 0.014/0.014 0inputs+0outputs (0major+16423minor)pagefaults 0swaps