-N (((x y) (z. (y. (y. z)))) (z. y))\r
- (((x y) x) (y y))\r
-\r
-# p27\r
-N (((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))))\r
- ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))\r
- (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))\r
-\r
-# p28\r
-N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))\r
- (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))\r
-\r
-# p29\r
-N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))\r
- (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)\r
-\r
-# p30\r
-N ((b c) (b. (z a)))\r
- ((v (a. (z v))) ((y (b c)) ((z a) (v y))))\r
- ((v (v. c)) z)\r
- ((v y) (v (a. (z v))))\r
- ((y (b c)) ((z a) (v y)))\r
-\r
-# p31\r
-N (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))\r
- ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))\r
- (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))\r
- (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))\r
- ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))\r
-\r
-# p32\r
-N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))\r
- (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)\r
- (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))\r
- ((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))\r
- ((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))\r
-\r
-# p33\r
+N (((x y) (z. (y. (y. z)))) (z. y)) Z\r
+ (((x y) x) (y y)) Z\r
+\r
+$! p27\r
+N (((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))) Z\r
+ ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) Z\r
+ (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) Z\r
+\r
+$! p28\r
+N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x))))) Z\r
+ (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x))))) Z\r
+\r
+$! p29\r
+N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y)) Z\r
+ (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) Z\r
+\r
+$! p30\r
+N ((b c) (b. (z a))) Z\r
+ ((v (a. (z v))) ((y (b c)) ((z a) (v y)))) Z\r
+ ((v (v. c)) z) Z\r
+ ((v y) (v (a. (z v)))) Z\r
+ ((y (b c)) ((z a) (v y))) Z\r
+\r
+$! p31\r
+N (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c))) Z\r
+ ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) Z\r
+ (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) Z\r
+ (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) Z\r
+ ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) Z\r
+\r
+$? p32\r
+# should fail because the first and second terms are eta-eq\r
+N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) Z\r
+ (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) Z\r
+ (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) Z\r
+ ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) Z\r
+ ((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a))))))) Z\r
+\r
+$! p33\r