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