MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     eq(?x,?y) -> eq(?y,?x),
     not(true) -> false,
     not(false) -> true,
     neq(?x,?y) -> not(eq(?x,?y)),
     neq(?x,s(?x)) -> true ]
Constructors: {0,s,eq,true,false}
Defined function symbols: {neq,not}
Constructor subsystem:
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y) ]
no strongly quasi-reducible parts found
new/eq3.trs: Failure(unknown)
(2 msec.)