NO
af/ONE-SORTED/741.trs
Input rules:
   [ if(true,a,?x:o) -> a,
     if(true,b,?x:o) -> b,
     if(true,g(a),?x:o) -> g(a),
     if(true,g(b),?x:o) -> g(b),
     if(false,?x:o,a) -> a,
     if(false,?x:o,b) -> b,
     if(false,?x:o,g(a)) -> g(a),
     if(false,?x:o,g(b)) -> g(b),
     g(a) -> g(g(a)),
     g(b) -> a,
     f(a,b) -> b,
     f(g(g(a)),?x:o) -> b ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ if(true,a,?x:o) -> a,
     if(true,b,?x:o) -> b,
     if(true,g(a),?x:o) -> g(a),
     if(true,g(b),?x:o) -> g(b),
     if(false,?x:o,a) -> a,
     if(false,?x:o,b) -> b,
     if(false,?x:o,g(a)) -> g(a),
     if(false,?x:o,g(b)) -> g(b),
     g(a) -> g(g(a)),
     g(b) -> a,
     f(a,b) -> b,
     f(g(g(a)),?x:o) -> b ]
Constructor pattern: [if(?x_1,?x_2,?x_3),true,a,b,g(?x_1),false,f(?x_1,?x_2)]
Defined pattern: []
Constructor subsystem:
   [ if(true,a,?x) -> a,
     if(true,b,?x) -> b,
     if(true,g(a),?x) -> g(a),
     if(true,g(b),?x) -> g(b),
     if(false,?x,a) -> a,
     if(false,?x,b) -> b,
     if(false,?x,g(a)) -> g(a),
     if(false,?x,g(b)) -> g(b),
     g(a) -> g(g(a)),
     g(b) -> a,
     f(a,b) -> b,
     f(g(g(a)),?x) -> b ]
Modified Constructor subsystem:
   [ if(true,a,?x) -> a,
     if(true,b,?x) -> b,
     if(true,g(a),?x) -> g(a),
     if(true,g(b),?x) -> g(b),
     if(false,?x,a) -> a,
     if(false,?x,b) -> b,
     if(false,?x,g(a)) -> g(a),
     if(false,?x,g(b)) -> g(b),
     g(a) -> g(g(a)),
     g(b) -> a,
     f(a,b) -> b,
     f(g(g(a)),?x) -> b ]
Find a quasi-ordering ...
order successfully found
Precedence:
 g : Mul;
 f : Mul;
 b : Mul;
 false : Mul,  true : Mul,  a : Mul;
 if : Mul;
Rules:
   [ if(true,a,?x) -> a,
     if(true,b,?x) -> b,
     if(true,g(a),?x) -> g(a),
     if(true,g(b),?x) -> g(b),
     if(false,?x,a) -> a,
     if(false,?x,b) -> b,
     if(false,?x,g(a)) -> g(a),
     if(false,?x,g(b)) -> g(b),
     g(b) -> a,
     f(a,b) -> b,
     f(g(g(a)),?x) -> b ]
Check confluence of constructor subsystem...
Check Termination...
Terminating, WCR: CR
Conjectures:
   [ g(a) = g(g(a)) ]
STEP 0
ES:
   [ g(a) = g(g(a)) ]
HS:
   [ ]
ES0:
   [ g(a) = g(g(a)) ]
HS0:
   [ ]
ES1:
   [ g(a) = g(g(a)) ]
HS1:
   [ ]
No equation to expand
check Non-Ground-Confluence...
ground constructor terms for instantiation: {true,a,b,false,if(true,true,true),if(true,true,a),if(true,true,b),if(true,true,false),if(true,a,true),if(true,a,a),if(true,a,b),if(true,a,false),if(true,b,true),if(true,b,a),if(true,b,b),if(true,b,false),if(true,false,true),if(true,false,a),if(true,false,b),if(true,false,false),if(a,true,true),if(a,true,a),if(a,true,b),if(a,true,false),if(a,a,true),if(a,a,a),if(a,a,b),if(a,a,false),if(a,b,true),if(a,b,a),if(a,b,b),if(a,b,false),if(a,false,true),if(a,false,a),if(a,false,b),if(a,false,false),if(b,true,true),if(b,true,a),if(b,true,b),if(b,true,false),if(b,a,true),if(b,a,a),if(b,a,b),if(b,a,false),if(b,b,true),if(b,b,a),if(b,b,b),if(b,b,false),if(b,false,true),if(b,false,a),if(b,false,b),if(b,false,false),if(false,true,true),if(false,true,a),if(false,true,b),if(false,true,false),if(false,a,true),if(false,a,a),if(false,a,b),if(false,a,false),if(false,b,true),if(false,b,a),if(false,b,b),if(false,b,false),if(false,false,true),if(false,false,a),if(false,false,b),if(false,false,false),g(true),g(a),g(b),g(false),f(true,true),f(true,a),f(true,b),f(true,false),f(a,true),f(a,a),f(a,b),f(a,false),f(b,true),f(b,a),f(b,b),f(b,false),f(false,true),f(false,a),f(false,b),f(false,false)}
ground terms for instantiation: {true:o,a:o,b:o,false:o,if(true,true,true):o,if(true,true,a):o,if(true,true,b):o,if(true,true,false):o,if(true,a,true):o,if(true,a,a):o,if(true,a,b):o,if(true,a,false):o,if(true,b,true):o,if(true,b,a):o,if(true,b,b):o,if(true,b,false):o,if(true,false,true):o,if(true,false,a):o,if(true,false,b):o,if(true,false,false):o,if(a,true,true):o,if(a,true,a):o,if(a,true,b):o,if(a,true,false):o,if(a,a,true):o,if(a,a,a):o,if(a,a,b):o,if(a,a,false):o,if(a,b,true):o,if(a,b,a):o,if(a,b,b):o,if(a,b,false):o,if(a,false,true):o,if(a,false,a):o,if(a,false,b):o,if(a,false,false):o,if(b,true,true):o,if(b,true,a):o,if(b,true,b):o,if(b,true,false):o,if(b,a,true):o,if(b,a,a):o,if(b,a,b):o,if(b,a,false):o,if(b,b,true):o,if(b,b,a):o,if(b,b,b):o,if(b,b,false):o,if(b,false,true):o,if(b,false,a):o,if(b,false,b):o,if(b,false,false):o,if(false,true,true):o,if(false,true,a):o,if(false,true,b):o,if(false,true,false):o,if(false,a,true):o,if(false,a,a):o,if(false,a,b):o,if(false,a,false):o,if(false,b,true):o,if(false,b,a):o,if(false,b,b):o,if(false,b,false):o,if(false,false,true):o,if(false,false,a):o,if(false,false,b):o,if(false,false,false):o,g(true):o,g(a):o,g(b):o,g(false):o,f(true,true):o,f(true,a):o,f(true,b):o,f(true,false):o,f(a,true):o,f(a,a):o,f(a,b):o,f(a,false):o,f(b,true):o,f(b,a):o,f(b,b):o,f(b,false):o,f(false,true):o,f(false,a):o,f(false,b):o,f(false,false):o}
obtain 15 rules by 3 steps unfolding
obtain 43 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
<F,Q,Q_f,Delta> where
   F = {(a,0),(b,0),(f,2),(g,1),(if,3),(true,0),(false,0)}
   Q = {q_0,q_1,q_{g(g(a))},q_{a},q_{g(a)},q_{true},q_{g(g(g(a)))}}
   Qf = {q_0,q_1}
   Delta = 
   [ a -> q_{a},
     b -> q_1,
     f(q_{g(g(g(a)))},q_{true}) -> q_0,
     g(q_{g(g(a))}) -> q_{g(g(g(a)))},
     g(q_{a}) -> q_{g(a)},
     g(q_{g(a)}) -> q_{g(g(a))},
     g(q_{g(a)}) -> q_{g(a)},
     true -> q_{true} ]
Witness for Non-Confluence: <f(g(g(g(a))),true), b>
: Success(not GCR)
(54 msec.)
0.09