f(f(g(f(y,x)),x),g(f(g(f(y,f(x,z))),x))) = z. g(f(f(f(x,x),y),f(g(f(x,y)),g(f(z,x))))) = z. f(f(f(x,x),y),f(g(f(x,y)),g(f(g(z),x)))) = z. g(f(f(g(f(x,z)),y),f(x,f(g(f(y,x)),x)))) = z. f(f(g(f(x,g(z))),y),f(x,f(g(f(y,x)),x))) = z. f(g(f(x,y)),g(f(g(f(f(f(x,x),y),z)),x))) = z. f(f(g(y),x),f(g(f(f(x,g(f(y,z))),x)),x)) = z. f(f(g(y),x),g(f(f(z,g(f(y,f(z,z)))),x))) = z. g(f(f(y,x),g(f(f(z,f(y,f(g(z),z))),x)))) = z. f(f(g(y),x),g(f(x,f(g(f(f(y,z),x)),x)))) = z. f(f(y,x),f(x,g(f(f(g(f(g(y),z)),x),x)))) = z. f(g(f(x,y)),g(f(x,g(f(x,f(f(y,z),x)))))) = z. f(y,g(f(g(f(f(f(x,g(f(x,y))),x),z)),x))) = z. g(f(x,f(g(f(f(f(x,z),f(x,g(y))),y)),x))) = z. f(x,f(g(f(f(f(x,g(z)),f(x,g(y))),y)),x)) = z. f(x,g(f(f(g(f(g(y),f(f(y,x),z))),x),x))) = z. g(f(x,f(g(f(f(y,f(f(g(y),x),z)),x)),x))) = z. f(x,f(g(f(f(y,f(f(g(y),x),g(z))),x)),x)) = z. g(f(y,f(f(f(g(y),g(f(z,f(x,z)))),z),x))) = z. g(f(x,g(f(f(f(z,f(x,g(f(x,y)))),x),y)))) = z. f(x,g(f(f(f(g(z),f(x,g(f(x,y)))),x),y))) = z. f(x,f(f(g(f(g(f(z,x)),x)),g(f(y,x))),y)) = z. g(f(x,f(f(g(f(f(x,z),x)),f(x,g(y))),y))) = z. f(x,f(f(g(f(f(x,g(z)),x)),f(x,g(y))),y)) = z. f(x,g(f(f(f(g(f(x,z)),x),f(x,y)),g(y)))) = z. f(y,g(f(f(f(z,g(f(z,z))),f(y,g(x))),x))) = z. g(f(x,f(f(y,f(g(f(x,y)),g(f(x,z)))),x))) = z. f(x,f(f(y,f(g(f(x,y)),g(f(x,g(z))))),x)) = z. f(x,f(f(g(f(y,x)),x),g(f(g(f(y,z)),x)))) = z. g(f(x,g(f(f(z,g(f(y,x))),f(y,f(x,x)))))) = z. f(x,g(f(f(g(z),g(f(y,x))),f(y,f(x,x))))) = z. g(f(y,f(f(g(y),x),f(g(f(f(x,z),x)),x)))) = z. f(y,f(f(g(y),x),f(g(f(f(x,g(z)),x)),x))) = z. g(f(g(y),f(f(y,x),f(x,g(f(f(z,x),x)))))) = z. f(y,f(f(g(y),x),g(f(x,f(g(f(z,x)),x))))) = z. f(g(y),f(f(y,x),f(x,g(f(f(g(z),x),x))))) = z. g(f(x,g(f(f(z,y),f(x,f(g(f(y,x)),x)))))) = z. f(x,g(f(f(g(z),y),f(x,f(g(f(y,x)),x))))) = z. f(y,f(g(f(x,y)),g(f(x,g(f(x,f(z,x))))))) = z. f(x,g(f(x,f(g(f(f(z,f(x,g(y))),y)),x)))) = z. f(x,g(f(x,f(f(g(f(z,x)),f(x,g(y))),y)))) = z. g(f(x,f(x,g(f(f(f(z,x),f(x,y)),g(y)))))) = z. f(x,f(x,g(f(f(f(g(z),x),f(x,y)),g(y))))) = z. g(f(x,g(f(x,f(f(y,f(g(f(x,y)),z)),x))))) = z. f(x,g(f(x,f(f(y,f(g(f(x,y)),g(z))),x)))) = z. g(f(y,f(z,f(f(g(f(y,z)),x),g(f(z,x)))))) = z. f(y,f(z,f(f(g(f(y,z)),x),g(f(g(z),x))))) = z. g(f(y,f(x,f(f(g(f(y,x)),x),g(f(z,x)))))) = z. f(y,f(x,f(f(g(f(y,x)),x),g(f(g(z),x))))) = z. f(x,g(f(y,f(f(g(y),x),f(g(f(z,x)),x))))) = z. % idfilter /home/mccune/gtsax/programs/gt.demods : tested 1981980, passed 20568 in 230.05 seconds. % attack head.2-3 interps.2-3 (on gyro.thornwood): checked 20568, passed 3541, new_interps 25. % attack head.r9 interps.r9 (on gyro.thornwood): checked 3541, passed 896, new_interps 100. % attack head.r29 interps.r29 (on gyro.thornwood): checked 896, passed 132, new_interps 151. % attack head.da10 interps.da10 (on theorem.mcs.anl.gov): checked 132, passed 50, new_interps 1.