MAYBE
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/eq2.trs
Input rules:
   [ eq(?x:Nat,?x:Nat) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),0) -> false,
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ eq(?x:Nat,?x:Nat) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),0) -> false,
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
Constructor pattern: [true,false,s(?x_1),0]
Defined pattern: [not(?x_1),neq(?x_2,?x_3),eq(?x_2,?x_3)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for not(?x_1):
   [ not(true) -> false,
     not(false) -> true ]
candidate for neq(?x_2,?x_3):
   [ neq(?x,?y) -> not(eq(?x,?y)) ]
candidate for eq(?x_2,?x_3):
No canditates. Supplement rules, and retry...
patlist: 
{0,s(?y)}
{s(?x),0}
Required Patterns: {eq(s(?x_1),s(?y_2)),eq(0,0)}
Added rules:
   [ eq(0,0) -> true ]
candidate for eq(?x_2,?x_3):
No canditates. Supplement rules, and retry...
patlist: 
{0,s(?y)}
{s(?x),0}
{0,0}
Required Patterns: {eq(s(?x_1),s(?y_2))}
failed to construct defining rules
Retry with a different D/C-partition.
Constructor pattern: [true,false,s(?x_1),0,eq(?x_2,?x_3)]
Defined pattern: [not(?x_1),neq(?x_2,?x_3)]
Constructor subsystem:
   [ eq(?x,?x) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false ]
Modified Constructor subsystem:
   [ eq(?x,?x) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false ]
candidate for not(?x_1):
No canditates. Supplement rules, and retry...
patlist: 
{true}
{false}
{eq(0,s(?y))}
{eq(s(?x),0)}
Required Patterns: {not(eq(s(?x_1),s(?y_2))),not(eq(0,0))}
Added rules:
   [ not(eq(0,0)) -> false ]
candidate for not(?x_1):
No canditates. Supplement rules, and retry...
patlist: 
{true}
{false}
{eq(0,s(?y))}
{eq(s(?x),0)}
{eq(0,0)}
Required Patterns: {not(eq(s(?x_1),s(?y_2)))}
failed to construct defining rules
Retry with a different D/C-partition.
Constructor pattern: [true,false,s(?x_1),0,eq(?x_2,?x_3),not(?x_1)]
Defined pattern: [neq(?x_2,?x_3)]
Constructor subsystem:
   [ eq(?x,?x) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     not(true) -> false,
     not(false) -> true ]
Modified Constructor subsystem:
   [ eq(?x,?x) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     not(true) -> false,
     not(false) -> true ]
candidate for neq(?x_2,?x_3):
   [ neq(?x,?y) -> not(eq(?x,?y)) ]
Find a quasi-ordering ...
order successfully found
Precedence:
 neq : Mul;
 not : Mul;
 eq : Mul;
 s : Mul;
 true : Mul,  0 : Mul;
 false : Mul;
Rules:
   [ neq(?x,?y) -> not(eq(?x,?y)),
     eq(?x,?x) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     not(true) -> false,
     not(false) -> true ]
Check confluence of constructor subsystem...
Check Termination...
Terminating, WCR: CR
Conjectures:
   [ neq(?x,s(?x)) = true ]
STEP 0
ES:
   [ neq(?x,s(?x)) = true ]
HS:
   [ ]
ES0:
   [ not(eq(?x,s(?x))) = true ]
HS0:
   [ ]
ES1:
   [ not(eq(?x,s(?x))) = true ]
HS1:
   [ ]
No equation to expand
check Non-Ground-Confluence...
ground constructor terms for instantiation: {true,false,0,s(0)}
ground terms for instantiation: {true:Bool,false:Bool,0:Nat,s(0):Nat}
obtain 10 rules by 3 steps unfolding
obtain 4 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
: Failure(unknown)
(120 msec.)