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