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 2)
0.001/0.001	(gt 1 2)
0.001/0.001	(if 1)
0.001/0.001	(minus 1 2)
0.001/0.001	(p 1)
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)) -> s(div(minus(X:S,Y:S),s(Y:S)))
0.001/0.001	gt(0,Y:S) -> false
0.001/0.001	gt(s(X:S),0) -> true
0.001/0.001	gt(s(X:S),s(Y:S)) -> gt(X:S,Y:S)
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(X:S,Y:S) -> if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S)
0.001/0.001	p(0) -> 0
0.001/0.001	p(s(X:S)) -> X: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 2)
0.001/0.001	(gt 1 2)
0.001/0.001	(if 1)
0.001/0.001	(minus 1 2)
0.001/0.001	(p 1)
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)) -> s(div(minus(X:S,Y:S),s(Y:S)))
0.001/0.001	gt(0,Y:S) -> false
0.001/0.001	gt(s(X:S),0) -> true
0.001/0.001	gt(s(X:S),s(Y:S)) -> gt(X:S,Y:S)
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(X:S,Y:S) -> if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S)
0.001/0.001	p(0) -> 0
0.001/0.001	p(s(X:S)) -> X: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 2)
0.001/0.001	(gt 1 2)
0.001/0.001	(if 1)
0.001/0.001	(minus 1 2)
0.001/0.001	(p 1)
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)) -> s(div(minus(X:S,Y:S),s(Y:S)))
0.001/0.001	gt(0,Y:S) -> false
0.001/0.001	gt(s(X:S),0) -> true
0.001/0.001	gt(s(X:S),s(Y:S)) -> gt(X:S,Y:S)
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(X:S,Y:S) -> if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S)
0.001/0.001	p(0) -> 0
0.001/0.001	p(s(X:S)) -> X: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) => minus(x14:S,x15:S) -> if(gt(x15:S,0),minus(p(x14:S),p(x15:S)),x14:S)
0.001/0.001	 Rule 8 (l' :-> r') => minus(X:S,Y:S) -> if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S)
0.001/0.001	 Var => x14:S
0.001/0.001	 Pos x14:S in l => [1]
0.001/0.001	 Sigma => {x14:S -> minus(X:S,Y:S)}
0.001/0.001	 s => if(gt(x15:S,0),minus(p(minus(X:S,Y:S)),p(x15:S)),minus(X:S,Y:S))
0.001/0.001	 t => minus(if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S),x15: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) => minus(x14:S,x15:S) -> if(gt(x15:S,0),minus(p(x14:S),p(x15:S)),x14:S)
0.001/0.001	 Rule 9 (l' :-> r') => p(0) -> 0
0.001/0.001	 Var => x14:S
0.001/0.001	 Pos x14:S in l => [1]
0.001/0.001	 Sigma => {x14:S -> p(0)}
0.001/0.001	 s => if(gt(x15:S,0),minus(p(p(0)),p(x15:S)),p(0))
0.001/0.001	 t => minus(0,x15: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) => minus(x14:S,x15:S) -> if(gt(x15:S,0),minus(p(x14:S),p(x15:S)),x14:S)
0.001/0.001	 Rule 10 (l' :-> r') => p(s(X:S)) -> X:S
0.001/0.001	 Var => x14:S
0.001/0.001	 Pos x14:S in l => [1]
0.001/0.001	 Sigma => {x14:S -> p(s(X:S))}
0.001/0.001	 s => if(gt(x15:S,0),minus(p(p(s(X:S))),p(x15:S)),p(s(X:S)))
0.001/0.001	 t => minus(X:S,x15: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 2)
0.001/0.001	(gt 1 2)
0.001/0.001	(if 1)
0.001/0.001	(minus 1 2)
0.001/0.001	(p 1)
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)) -> s(div(minus(X:S,Y:S),s(Y:S)))
0.001/0.001	gt(0,Y:S) -> false
0.001/0.001	gt(s(X:S),0) -> true
0.001/0.001	gt(s(X:S),s(Y:S)) -> gt(X:S,Y:S)
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(X:S,Y:S) -> if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S)
0.001/0.001	p(0) -> 0
0.001/0.001	p(s(X:S)) -> X:S
0.001/0.001	)
0.001/0.001	Critical Pairs:
0.001/0.001	<if(gt(x15:S,0),minus(p(minus(X:S,Y:S)),p(x15:S)),minus(X:S,Y:S)),minus(if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S),x15:S)>   =>  Not trivial, Not overlay, NW1, N1
0.001/0.001	<if(gt(x15:S,0),minus(p(p(0)),p(x15:S)),p(0)),minus(0,x15:S)>   =>  Not trivial, Not overlay, NW1, N2
0.001/0.001	<if(gt(x15:S,0),minus(p(p(s(X:S))),p(x15:S)),p(s(X:S))),minus(X:S,x15:S)>   =>  Not trivial, Not overlay, NW1, N3
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)) -> s(div(minus(X:S,Y:S),s(Y:S)))
0.001/0.001	 gt(0,Y:S) -> false
0.001/0.001	 gt(s(X:S),0) -> true
0.001/0.001	 gt(s(X:S),s(Y:S)) -> gt(X:S,Y:S)
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(X:S,Y:S) -> if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S)
0.001/0.001	 p(0) -> 0
0.001/0.001	 p(s(X:S)) -> X:S
0.001/0.001	-> Vars:
0.001/0.001	 Y, X, Y, Y, X, X, Y, X, Y, X, Y, X, Y, X
0.001/0.001	-> UVars:
0.001/0.001	 (UV-RuleId: 1, UV-LActive: [Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.001/0.001	 (UV-RuleId: 2, UV-LActive: [X, Y], UV-RActive: [X, Y], UV-LFrozen: [], UV-RFrozen: [])
0.001/0.001	 (UV-RuleId: 3, UV-LActive: [Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.001/0.001	 (UV-RuleId: 4, UV-LActive: [X], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.001/0.001	 (UV-RuleId: 5, UV-LActive: [X, Y], UV-RActive: [X, Y], UV-LFrozen: [], 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: [X, Y], UV-RActive: [Y], UV-LFrozen: [], UV-RFrozen: [X, Y])
0.001/0.001	 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.001/0.001	 (UV-RuleId: 10, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: [])
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, x9, x11, x13, x15], X: [x4, x7, x8, x10, x12, x14, x16]
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], s(x3:S)->[2])
0.001/0.001	 (rule: div(s(x4:S),s(x5:S)) -> s(div(minus(x4:S,x5:S),s(x5:S))), id: 2, possubterms: div(s(x4:S),s(x5:S))->[], s(x4:S)->[1], s(x5:S)->[2])
0.001/0.001	 (rule: gt(0,x6:S) -> false, id: 3, possubterms: gt(0,x6:S)->[], 0->[1])
0.001/0.001	 (rule: gt(s(x7:S),0) -> true, id: 4, possubterms: gt(s(x7:S),0)->[], s(x7:S)->[1], 0->[2])
0.001/0.001	 (rule: gt(s(x8:S),s(x9:S)) -> gt(x8:S,x9:S), id: 5, possubterms: gt(s(x8:S),s(x9:S))->[], s(x8:S)->[1], s(x9:S)->[2])
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(x14:S,x15:S) -> if(gt(x15:S,0),minus(p(x14:S),p(x15:S)),x14:S), id: 8, possubterms: minus(x14:S,x15:S)->[])
0.001/0.001	 (rule: p(0) -> 0, id: 9, possubterms: p(0)->[], 0->[1])
0.001/0.001	 (rule: p(s(x16:S)) -> x16:S, id: 10, possubterms: p(s(x16:S))->[], s(x16:S)->[1])
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	<if(gt(Y:S,0),minus(p(p(0)),p(Y:S)),p(0)),minus(0,Y:S)>   =>  Not trivial, Not overlay, NW1, N1
0.001/0.001	<if(gt(Y:S,0),minus(p(p(s(X:S))),p(Y:S)),p(s(X:S))),minus(X:S,Y:S)>   =>  Not trivial, Not overlay, NW1, N2
0.001/0.001	<if(gt(Y:S,0),minus(p(minus(X:S,Y:S)),p(Y:S)),minus(X:S,Y:S)),minus(if(gt(Y:S,0),minus(p(X:S),p(Y:S)),X:S),Y:S)>   =>  Not trivial, Not overlay, NW1, N3
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(gt(Y:S,0),minus(p(p(0)),p(Y:S)),p(0))
0.001/0.001	Nodes: [0]
0.001/0.001	Edges: []
0.001/0.001	ID: 0 => ('if(gt(Y:S,0),minus(p(p(0)),p(Y:S)),p(0))', D0)
0.001/0.001	t: minus(0,Y:S)
0.001/0.001	Nodes: [0,1]
0.001/0.001	Edges: [(0,1)]
0.001/0.001	ID: 0 => ('minus(0,Y:S)', D0)
0.001/0.001	ID: 1 => ('if(gt(Y:S,0),minus(p(0),p(Y:S)),0)', D1, R8, P[], S{x14:S -> 0, x15:S -> Y:S}), NR: 'if(gt(Y:S,0),minus(p(0),p(Y:S)),0)'
0.001/0.001	if(gt(Y:S,0),minus(p(p(0)),p(Y:S)),p(0)) ->* no union *<- minus(0,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 84%CPU (0avgtext+0avgdata 10364maxresident)k
0.001/0.001	0inputs+0outputs (0major+872minor)pagefaults 0swaps