YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/imply.trs
Input rules:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y:Bool) -> true,
     or(?x:Bool,true) -> true,
     or(false,false) -> false,
     implies(true,?y:Bool) -> ?y:Bool,
     implies(false,?y:Bool) -> true,
     implies(?x:Bool,?y:Bool) -> or(not(?x:Bool),?y:Bool) ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y:Bool) -> true,
     or(?x:Bool,true) -> true,
     or(false,false) -> false,
     implies(true,?y:Bool) -> ?y:Bool,
     implies(false,?y:Bool) -> true,
     implies(?x:Bool,?y:Bool) -> or(not(?x:Bool),?y:Bool) ]
Constructor pattern: [true,false]
Defined pattern: [implies(?x_2,?x_3),or(?x_2,?x_3),not(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for implies(?x_2,?x_3):
   [ implies(?x,?y) -> or(not(?x),?y) ]
   [ implies(true,?y) -> ?y,
     implies(false,?y) -> true ]
candidate for or(?x_2,?x_3):
   [ or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false ]
candidate for not(?x_1):
   [ not(true) -> false,
     not(false) -> true ]
Find a quasi-ordering ...
order successfully found
Precedence:
 or : Mul;
 implies : Mul;
 false : Mul,  true : Mul;
 not : Mul;
Rules:
   [ implies(true,?y) -> ?y,
     implies(false,?y) -> true,
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     not(true) -> false,
     not(false) -> true ]
Conjectures:
   [ implies(?x,?y) = or(not(?x),?y),
     true = true ]
STEP 0
ES:
   [ implies(?x,?y) = or(not(?x),?y),
     true = true ]
HS:
   [ ]
ES0:
   [ implies(?x,?y) = or(not(?x),?y),
     true = true ]
HS0:
   [ ]
ES1:
   [ implies(?x,?y) = or(not(?x),?y) ]
HS1:
   [ ]
Expand or(not(?x),?y) = implies(?x,?y)
   [ or(false,?y) = implies(true,?y),
     or(true,?y) = implies(false,?y) ]
ES2:
   [ or(false,?y) = implies(true,?y),
     true = implies(false,?y) ]
HS2:
   [ or(not(?x),?y) -> implies(?x,?y) ]
STEP 1
ES:
   [ or(false,?y) = implies(true,?y),
     true = implies(false,?y) ]
HS:
   [ or(not(?x),?y) -> implies(?x,?y) ]
ES0:
   [ or(false,?y) = ?y,
     true = true ]
HS0:
   [ or(not(?x),?y) -> implies(?x,?y) ]
ES1:
   [ or(false,?y) = ?y ]
HS1:
   [ or(not(?x),?y) -> implies(?x,?y) ]
Expand or(false,?y) = ?y
   [ true = true,
     false = false ]
ES2:
   [ true = true,
     false = false ]
HS2:
   [ or(false,?y) -> ?y,
     or(not(?x),?y) -> implies(?x,?y) ]
STEP 2
ES:
   [ true = true,
     false = false ]
HS:
   [ or(false,?y) -> ?y,
     or(not(?x),?y) -> implies(?x,?y) ]
ES0:
   [ true = true,
     false = false ]
HS0:
   [ or(false,?y) -> ?y,
     or(not(?x),?y) -> implies(?x,?y) ]
ES1:
   [ ]
HS1:
   [ or(false,?y) -> ?y,
     or(not(?x),?y) -> implies(?x,?y) ]
: Success(GCR)
(14 msec.)