### In Search for The Irreducible Lambda-Expressions.

 ; In last post, I wrote the program that generates random lambda ; expressions, 500 of these. This is the program that generates ; roughly 3500000 random lambda expressions, then attempts to ; reduce these, and makes list of lambda-expressions such that ; reduction to normal form failed. There are two different kinds of ; lambda-expressions on that list: ; ;  (i)  the program proves that reductions fail to terminate, i.e. ;       lambda-expression is reduced to the form that is further ;       reduced to itself. ; ;  (ii) the program doesn't prove that reductions fail to terminate ;       generally, but it shows that after n (in our case 25) ;       reductions the lambda expression is still not in normal ;       form. ; ; The lambda expressions on the list are normalized, i.e. two lambda ; expressions are considered to be equivalent if there is ; alpha-conversion that transform one expression in the other. ; For example, there is alpha-conversion from (^ x . x) to (^ y . y). ; ; The results are at the bottom of the post. If you decide to try ; the program, be patient, it might need one hour of time. If ; you want it to run faster, change the constant in line ; ;              (dotimes(dummy 200000) ... (setf [println.supressed] true [print.supressed] true) (load "http://www.instprog.com/Instprog.default-library.lsp") (setf [println.supressed] nil [print.supressed] nil) ;--------------------------------------------------------------- ; is-variable, is-function and is-application are predicated ; that return true or false (set 'is-variable (lambda(x)(symbol? x))) (set 'is-function (lambda(L)(and (list? L)                                  (= (first L) '^)                                  (= (nth 2 L) '.))))                                   (set 'is-application (lambda(L)(and (list? L)                                     (= (length L) 2)))) ;--------------------------------------------------------------- ; function-variable and function-body return parts of the ; lambda-expression. For example ; ;       (function-variable '(^ x . (x x))) returns x ;       (function-body '(^ x . (x x))) returns (x x) (set 'function-variable (lambda(f)(nth 1 f))) (set 'function-body (lambda(f)(last f))) ;--------------------------------------------------------------- ; ; (substitute-free-occurences V E F) ; ; Substitutes free occurences of variable V in expression E with F. ; Don't change bounded occurences of the variable. (set 'substitute-free-occurences ; of variable V in E with F      (lambda(V E F)        (cond ((is-variable E) (if (= E V) F E))                      ((is-function E)                   (if (= (function-variable E) V)                                              E ; V is bounded in E - no substitution                                              (list '^                             (function-variable E)                             '.                             (substitute-free-occurences V                                    (function-body E)                                    F))))                                        ((is-application E)                (list (substitute-free-occurences V (first E) F)                      (substitute-free-occurences V (last E) F)))))) ;--------------------------------------------------------------- ; ;                      (reduce-once E) ; ; performs beta-reduction on lambda-expression E. It returns pair ; ;                      (success result) ; where ; ;     success = true or nil, dependently if E is reduced ;     result  = reduced E if reduction is possible ;               original E if reduction is not possible (set 'reduce-once      (lambda(E)               (cond ((is-variable E) (list 'nil E))                        ((is-function E)                (let((rfb (reduce-once (function-body E))))                  (if (first rfb) ; success                      (list 'true (append (chop E)                                          (list (last rfb))))                                             (list 'nil E))))                                                         ((is-application E)                 (let ((F (first E))                       (G (last E)))                                    (if (is-function F)                                          ;E=((^V._) G) ==> E10[V:=E2]                                              (list 'true (substitute-free-occurences (function-variable F)                                                               (function-body F)                                                               G))                        ;E=(F G) ==>                        (let ((rF (reduce-once F)))                              (cond ((= (first rF) true)                                     (list 'true (list (last rF) G)))                                    ((= (first rF) nil)                                     (let ((rG (reduce-once G)))                                          (cond ((= (first rG) true)                                                 (list 'true (list F (last rG))))                                                ((= (first rG) nil)                                                 (list 'nil (list F G)))))))))))))) ; (println= (reduce-once 'a)) ; (println= (reduce-once '(a b))) ; (println= (reduce-once '(^ x . x))) ; (println= (reduce-once '((^ x . x) y))) ; (println= (reduce-once '((^ x . y) y))) ; (set 'pretty-form    (lambda(t)       (replace " . " (replace "^ " (replace ") (" (string t) ")(") "^") "."))) ;--------------------------------------------------------------- ;                     (bounded-var i) ; ; returns i-th of variables A0, B0, C0, ... A1, B1, C1 ... (set 'bounded-var      (lambda(i)(sym (append (char (+ 64 (% i 25)))                             (string (/ i 25)))))) ;--------------------------------------------------------------- ; alpha-convert converts expressions, so beta-reduction can be ; performed on the way it is defined. (set 'init-and-alpha-convert      (lambda(E)         (setf bounded-vars-counter 0)         (alpha-convert E))) (set 'alpha-convert      (lambda(E)         (cond ((is-variable E) E)               ((is-function E)                (begin (inc bounded-vars-counter)                       (let (new-E-1 (bounded-var bounded-vars-counter))                            (list '^                                  new-E-1                                  '.                                  (expand (alpha-convert (E 3))                                          (list (list (E 1) new-E-1)))))))               ((is-application E)                (list (alpha-convert (E 0))                      (alpha-convert (E 1))))))) ;--------------------------------------------------------------- ; ;      (reduce new-expression reduce-max to-print) ; ; reduces new-expression in at most reduce-max steps, producing ; output if to-print is set to true. ; ; It returs list ; ;            (terminating result result-counter) ; ; where ; ;       terminating = true if further reductions are impossible ;                   = nil  if cyclical reduction is discovered ;                   = undefined if reduction is quited because of ;                     lack of computing resources ; ;       result = last lambda-expression in process ;       result-counter = numbers of derived lambda-expression ;                        before further derivation is canceled ;                        independently of a reason (set 'reduce   (lambda(new-expr reduce-max to-print)     (when to-print           (println "\n--------------\n\n " (pretty-form new-expr)))          (let ((reduce-counter 0)             (terminating 'undefined)           (result 'undefined)           (reduce-end nil))         (setf new-expr (init-and-alpha-convert new-expr))         (when to-print (println " ==[alpha]==> "                                 (pretty-form new-expr)))         (until reduce-end           ;(println "unless loop")           (letn ((old-expr new-expr)                  (r (reduce-once old-expr))                  (reduce-once-succeeded (first r)))                        (cond ((not reduce-once-succeeded)                                 (begin (setf reduce-end true)                           (setf terminating true)                           (setf result old-expr)                                                      (when to-print                                 (println "\n There are no further reductions"))))                   (reduce-once-succeeded                    (begin (inc reduce-counter)                           (setf new-expr (last r))                           (when to-print                                 (println " ==[beta " reduce-counter                                          ".]==> " (pretty-form new-expr)))                           (setf new-expr (init-and-alpha-convert new-expr))                           (when to-print                                (println " ==[alpha]==> " (pretty-form new-expr)))                           (cond ((= old-expr new-expr)                                 (begin (setf reduce-end true)                                        (setf terminating nil)                                        (setf result old-expr)                                                                                (when to-print                                          (println "\n Self-evaluating expression."))))                                ((>= reduce-counter reduce-max)                                    (begin (setf reduce-end true)                                           (setf terminating 'undefined)                                           (setf result new-expr)                                           (when to-print                                             (println "\n Maximal number of the reductions reached."))))))))))           ;(println= "unless loop ended." old-expr new-expr reduce-end)                                           (list terminating result reduce-counter))))            ;--------------------------------------------------------------- ; ;                  EXAMPLE OF REDUCTION                                 (reduce '((^ c . (c c)) (^ c . (c (c (^ c . c))))) 15 true) ; -------------- ; ;  ((^A0.(A0 A0))(^B0.(B0 (B0 (^C0.C0))))) ;  ==[alpha]==> ((^A0.(A0 A0))(^B0.(B0 (B0 (^C0.C0))))) ;  ==[beta 1.]==> ((^B0.(B0 (B0 (^C0.C0))))(^B0.(B0 (B0 (^C0.C0))))) ;  ==[alpha]==> ((^A0.(A0 (A0 (^A0.A0))))(^C0.(C0 (C0 (^D0.D0))))) ;  ==[beta 2.]==> ((^C0.(C0 (C0 (^D0.D0))))((^C0.(C0 (C0 (^D0.D0))))(^A0.A0))) ;  ==[alpha]==> ((^A0.(A0 (A0 (^B0.B0))))((^C0.(C0 (C0 (^D0.D0))))(^E0.E0))) ;  ==[beta 3.]==> (((^C0.(C0 (C0 (^D0.D0))))(^E0.E0))(((^C0.(C0 (C0 (^D0.D0))))(^E0.E0))(^B0.B0))) ;  ==[alpha]==> (((^A0.(A0 (A0 (^B0.B0))))(^C0.C0))(((^D0.(D0 (D0 (^E0.E0))))(^F0.F0))(^G0.G0))) ;  ==[beta 4.]==> (((^C0.C0)((^C0.C0)(^B0.B0)))(((^D0.(D0 (D0 (^E0.E0))))(^F0.F0))(^G0.G0))) ;  ==[alpha]==> (((^A0.A0)((^B0.B0)(^C0.C0)))(((^D0.(D0 (D0 (^E0.E0))))(^F0.F0))(^G0.G0))) ;  ==[beta 5.]==> (((^B0.B0)(^C0.C0))(((^D0.(D0 (D0 (^E0.E0))))(^F0.F0))(^G0.G0))) ;  ==[alpha]==> (((^A0.A0)(^B0.B0))(((^C0.(C0 (C0 (^C0.C0))))(^E0.E0))(^F0.F0))) ;  ==[beta 6.]==> ((^B0.B0)(((^C0.(C0 (C0 (^C0.C0))))(^E0.E0))(^F0.F0))) ;  ==[alpha]==> ((^A0.A0)(((^B0.(B0 (B0 (^B0.B0))))(^D0.D0))(^E0.E0))) ;  ==[beta 7.]==> (((^B0.(B0 (B0 (^B0.B0))))(^D0.D0))(^E0.E0)) ;  ==[alpha]==> (((^A0.(A0 (A0 (^A0.A0))))(^C0.C0))(^D0.D0)) ;  ==[beta 8.]==> (((^C0.C0)((^C0.C0)(^A0.A0)))(^D0.D0)) ;  ==[alpha]==> (((^A0.A0)((^B0.B0)(^C0.C0)))(^D0.D0)) ;  ==[beta 9.]==> (((^B0.B0)(^C0.C0))(^D0.D0)) ;  ==[alpha]==> (((^A0.A0)(^B0.B0))(^C0.C0)) ;  ==[beta 10.]==> ((^B0.B0)(^C0.C0)) ;  ==[alpha]==> ((^A0.A0)(^B0.B0)) ;  ==[beta 11.]==> (^B0.B0) ;  ==[alpha]==> (^A0.A0) ; ;  There are no further reductions ; ;--------------------------------------------------------------- ; ;                    (random-var nvars) ; ; return random of the first nvars variables of ; a0, b0, c0, ..., a1, b1, c1 ... ; (set 'random-var      (lambda(nvars)        (let((r (rand nvars)))            (sym (append (char (+ 97 (% r 25)))                         (string (/ r 25)))))))                          ;--------------------------------------------------------------- ;               ;               (random-^-expr nvars number-of-occurences) ; ; returns random lambda-expression with at most nvars variables ; in total of exactly number-of-occurences occurences (set 'random-^-expr    (lambda(nvars number-of-occurences)       (cond ((= number-of-occurences 1) (random-var nvars))             ((> number-of-occurences 1)              (amb (let ((r (+ (rand (- number-of-occurences 1)) 1)))                        (list (random-^-expr nvars r)                              (random-^-expr nvars (- number-of-occurences r))))                   (list '^                         (random-var nvars)                         '.                         (random-^-expr nvars (- number-of-occurences 1)))))))) ;--------------------------------------------------------------- ; ;                         (normalized E) ; ; returns normalized expression E, i.e. variables sorted by some ; natural and unique order. It is important only for order of ; free variables. The order of bounded variables is sorted on ; natural and unique way using function init-and-alpha-convert. (set 'normalized   (lambda(E)     (let((varcounter 0)          (F (flat E)))       (dolist(i F)                 (when (and (!= i '^)                    (!= i '.)                    (= (string i)                       (lower-case (string i))))           (inc varcounter)           (setf E              (expand E ;((i _i))                 (list (list i                         (sym (append "_"                                 (lower-case (string (bounded-var varcounter)))))))))))                                                             (eval-string (append "'" (replace "_" (string E) ""))))))                                                           ; (println= (normalized '(b0 (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0))))   ;--------------------------------------------------------------- ; The program will generate large number of lambda-expressions, ; and attempt to reduce these. The lambda-expressions not reduced in ; 20 steps or more are good candidates for unreducible lambda-expressions.      (for(number-of-occurences 6 8 1)   (setf successes 0         failures 0         attempts 0         total-number-of-steps 0         max-number-of-steps-if-reduction-succeeded 0)            (setf max-number-of-reductions 25)   (setf unreduced '())      (println= "\n\n----------------" number-of-occurences)   (for(nvars 1 (- number-of-occurences 1) 1)     (dotimes(dummy 200000)       (letn((F (random-^-expr nvars number-of-occurences))             (G (init-and-alpha-convert F)))            (inc attempts)                        (letn((H (reduce G                             max-number-of-reductions                             nil)))                             (cond ((= (H 0) true) ; reduction succeeded                         (inc total-number-of-steps (H 2))                         (inc successes)                         (when (> (H 2) max-number-of-steps-if-reduction-succeeded)                               (setf max-number-of-steps-if-reduction-succeeded (H 2))                               (setf longest-reduction G)))                                               ((= (H 0) nil) ; reduction failed                                               (begin (inc failures)                               ;(print "!")                               (if (= (% failures 80) 0) (println))                                                              (push (append (string (normalized G)) "  failed.")                                     unreduced                                     -1)))                                                      ((= (H 0) 'undefined) ; reduction canceled                        (begin (inc failures)                               ;(print "?")                               (if (= (% failures 80) 0) (println))                                                              (push (append (string (normalized G))                                             "  didn't succeeded in "                                             (string max-number-of-reductions)                                             " steps.")                                     unreduced                                     -1))))))))                       (println= "\n\n" attempts "\n" successes "\n" failures              "\n" max-number-of-reductions "\n" total-number-of-steps              "\n" max-number-of-steps-if-reduction-succeeded              "\n" longest-reduction)                (println "\nUnreduced (without duplicates):\n")    (dolist(s (unique (sort unreduced)))      (println (+ \$idx 1) ".  " s)))      (exit) Output: (!'s and ?'s are printed during execution of the program) ----------------number-of-occurences=6; attempts=1000000; successes=998677; failures=1323; max-number-of-reductions=25; total-number-of-steps=596444; max-number-of-steps-if-reduction-succeeded=3; longest-reduction=(((^ A0 . (A0 A0)) (^ B0 . B0)) a0); Unreduced (without duplicates): 1. ((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) failed. ----------------number-of-occurences=7; attempts=1200000; successes=1197916; failures=2084; max-number-of-reductions=25; total-number-of-steps=908464; max-number-of-steps-if-reduction-succeeded=5; longest-reduction=((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 b0)))); Unreduced (without duplicates): 1. (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0) failed. 2. ((^ A0 . ((A0 A0) A0)) (^ B0 . (B0 B0))) failed. 3. ((^ A0 . ((A0 A0) a0)) (^ B0 . (B0 B0))) failed. 4. ((^ A0 . (A0 (A0 A0))) (^ B0 . (B0 B0))) failed. 5. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) B0))) didn't succeeded in 25 steps. 6. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) a0))) didn't succeeded in 25 steps. 7. ((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 8. ((^ A0 . (A0 A0)) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 9. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (C0 C0))) failed. 10. ((^ A0 . (a0 (A0 A0))) (^ B0 . (B0 B0))) failed. 11. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (C0 C0)))) failed. 12. (a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) failed. ----------------number-of-occurences=8; attempts=1400000; successes=1396693; failures=3307; max-number-of-reductions=25; total-number-of-steps=1278600; max-number-of-steps-if-reduction-succeeded=15; longest-reduction=((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 (B0 c0))))); Unreduced (without duplicates): 1. ((((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0) a0) failed. 2. ((((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0) b0) failed. 3. (((^ A0 . ((A0 A0) A0)) (^ B0 . (B0 B0))) a0) failed. 4. (((^ A0 . ((A0 A0) a0)) (^ B0 . (B0 B0))) b0) failed. 5. (((^ A0 . (A0 (A0 A0))) (^ B0 . (B0 B0))) a0) failed. 6. (((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) B0))) a0) didn't succeeded in 25 steps. 7. (((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) a0))) a0) didn't succeeded in 25 steps. 8. (((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 B0)))) a0) didn't succeeded in 25 steps. 9. (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) (^ C0 . C0)) failed. 10. (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) (^ C0 . a0)) failed. 11. (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) (a0 a0)) failed. 12. (((^ A0 . (A0 A0)) (^ B0 . (a0 (B0 B0)))) b0) didn't succeeded in 25 steps. 13. (((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (C0 C0))) a0) failed. 14. (((^ A0 . (^ B0 . (B0 B0))) a0) (^ C0 . (C0 C0))) failed. 15. (((^ A0 . (a0 (A0 A0))) (^ B0 . (B0 B0))) a0) failed. 16. (((^ A0 . A0) (^ B0 . (B0 B0))) (^ C0 . (C0 C0))) failed. 17. ((^ A0 . (((A0 A0) A0) A0)) (^ B0 . (B0 B0))) failed. 18. ((^ A0 . (((A0 A0) A0) a0)) (^ B0 . (B0 B0))) failed. 19. ((^ A0 . (((A0 A0) a0) A0)) (^ B0 . (B0 B0))) failed. 20. ((^ A0 . (((^ B0 . A0) A0) A0)) (^ C0 . (C0 C0))) failed. 21. ((^ A0 . (((^ B0 . A0) a0) A0)) (^ C0 . (C0 C0))) failed. 22. ((^ A0 . (((^ B0 . B0) A0) A0)) (^ C0 . (C0 C0))) failed. 23. ((^ A0 . ((A0 (A0 A0)) A0)) (^ B0 . (B0 B0))) failed. 24. ((^ A0 . ((A0 (A0 A0)) a0)) (^ B0 . (B0 B0))) failed. 25. ((^ A0 . ((A0 A0) (A0 A0))) (^ B0 . (B0 B0))) failed. 26. ((^ A0 . ((A0 A0) (^ B0 . A0))) (^ C0 . (C0 C0))) failed. 27. ((^ A0 . ((A0 A0) (^ B0 . B0))) (^ C0 . (C0 C0))) failed. 28. ((^ A0 . ((A0 A0) (^ B0 . a0))) (^ C0 . (C0 C0))) failed. 29. ((^ A0 . ((A0 A0) (a0 A0))) (^ B0 . (B0 B0))) failed. 30. ((^ A0 . ((A0 A0) (a0 a0))) (^ B0 . (B0 B0))) failed. 31. ((^ A0 . ((A0 A0) A0)) (^ B0 . ((B0 B0) B0))) didn't succeeded in 25 steps. 32. ((^ A0 . ((A0 A0) A0)) (^ B0 . ((B0 B0) a0))) didn't succeeded in 25 steps. 33. ((^ A0 . ((A0 A0) A0)) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 34. ((^ A0 . ((A0 A0) A0)) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 35. ((^ A0 . ((A0 A0) a0)) (^ B0 . ((B0 B0) a0))) didn't succeeded in 25 steps. 36. ((^ A0 . ((A0 A0) a0)) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 37. ((^ A0 . ((A0 A0) a0)) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 38. ((^ A0 . ((A0 a0) (A0 A0))) (^ B0 . (B0 B0))) failed. 39. ((^ A0 . ((^ B0 . (A0 A0)) A0)) (^ C0 . (C0 C0))) failed. 40. ((^ A0 . ((^ B0 . (A0 A0)) a0)) (^ C0 . (C0 C0))) failed. 41. ((^ A0 . ((^ B0 . (A0 B0)) A0)) (^ C0 . (C0 C0))) failed. 42. ((^ A0 . ((^ B0 . (B0 A0)) A0)) (^ C0 . (C0 C0))) failed. 43. ((^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (C0 C0)))) a0) failed. 44. ((^ A0 . ((^ B0 . (B0 B0)) A0)) (^ C0 . (C0 C0))) failed. 45. ((^ A0 . ((^ B0 . B0) (A0 A0))) (^ C0 . (C0 C0))) failed. 46. ((^ A0 . ((a0 (A0 A0)) A0)) (^ B0 . (B0 B0))) failed. 47. ((^ A0 . ((a0 (A0 A0)) a0)) (^ B0 . (B0 B0))) failed. 48. ((^ A0 . ((a0 A0) (A0 A0))) (^ B0 . (B0 B0))) failed. 49. ((^ A0 . (A0 ((A0 A0) A0))) (^ B0 . (B0 B0))) failed. 50. ((^ A0 . (A0 ((A0 A0) a0))) (^ B0 . (B0 B0))) failed. 51. ((^ A0 . (A0 ((^ B0 . A0) a0))) (^ C0 . (C0 C0))) didn't succeeded in 25 steps. 52. ((^ A0 . (A0 ((^ B0 . B0) A0))) (^ C0 . (C0 C0))) didn't succeeded in 25 steps. 53. ((^ A0 . (A0 (A0 (A0 A0)))) (^ B0 . (B0 B0))) failed. 54. ((^ A0 . (A0 (A0 (^ B0 . A0)))) (^ C0 . (C0 C0))) didn't succeeded in 25 steps. 55. ((^ A0 . (A0 (A0 A0))) (^ B0 . ((B0 B0) B0))) didn't succeeded in 25 steps. 56. ((^ A0 . (A0 (A0 A0))) (^ B0 . ((B0 B0) a0))) didn't succeeded in 25 steps. 57. ((^ A0 . (A0 (A0 A0))) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 58. ((^ A0 . (A0 (A0 A0))) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 59. ((^ A0 . (A0 (^ B0 . (A0 B0)))) (^ C0 . (C0 C0))) didn't succeeded in 25 steps. 60. ((^ A0 . (A0 (^ B0 . (B0 B0)))) (^ C0 . (C0 C0))) failed. 61. ((^ A0 . (A0 (^ B0 . A0))) (^ C0 . ((C0 a0) C0))) didn't succeeded in 25 steps. 62. ((^ A0 . (A0 (a0 (A0 A0)))) (^ B0 . (B0 B0))) failed. 63. ((^ A0 . (A0 A0)) ((^ B0 . (^ C0 . (B0 B0))) a0)) didn't succeeded in 25 steps. 64. ((^ A0 . (A0 A0)) ((^ B0 . (^ C0 . (B0 C0))) a0)) didn't succeeded in 25 steps. 65. ((^ A0 . (A0 A0)) ((^ B0 . (^ C0 . (C0 B0))) a0)) didn't succeeded in 25 steps. 66. ((^ A0 . (A0 A0)) ((^ B0 . (^ C0 . (C0 C0))) a0)) didn't succeeded in 25 steps. 67. ((^ A0 . (A0 A0)) ((^ B0 . B0) (^ C0 . (C0 C0)))) didn't succeeded in 25 steps. 68. ((^ A0 . (A0 A0)) (^ B0 . (((B0 B0) B0) B0))) didn't succeeded in 25 steps. 69. ((^ A0 . (A0 A0)) (^ B0 . (((B0 B0) a0) B0))) didn't succeeded in 25 steps. 70. ((^ A0 . (A0 A0)) (^ B0 . (((B0 B0) a0) a0))) didn't succeeded in 25 steps. 71. ((^ A0 . (A0 A0)) (^ B0 . (((B0 B0) a0) b0))) didn't succeeded in 25 steps. 72. ((^ A0 . (A0 A0)) (^ B0 . (((^ C0 . B0) B0) B0))) didn't succeeded in 25 steps. 73. ((^ A0 . (A0 A0)) (^ B0 . (((^ C0 . C0) B0) B0))) didn't succeeded in 25 steps. 74. ((^ A0 . (A0 A0)) (^ B0 . ((B0 (B0 B0)) B0))) didn't succeeded in 25 steps. 75. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (B0 B0)))) didn't succeeded in 25 steps. 76. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (B0 a0)))) didn't succeeded in 25 steps. 77. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (^ C0 . B0)))) didn't succeeded in 25 steps. 78. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (^ C0 . C0)))) didn't succeeded in 25 steps. 79. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (^ C0 . a0)))) didn't succeeded in 25 steps. 80. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (a0 B0)))) didn't succeeded in 25 steps. 81. ((^ A0 . (A0 A0)) (^ B0 . ((B0 a0) (B0 B0)))) didn't succeeded in 25 steps. 82. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . (B0 C0)) B0))) didn't succeeded in 25 steps. 83. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . (C0 B0)) B0))) didn't succeeded in 25 steps. 84. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . (C0 C0)) B0))) didn't succeeded in 25 steps. 85. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . B0) (B0 B0)))) didn't succeeded in 25 steps. 86. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . C0) (B0 B0)))) didn't succeeded in 25 steps. 87. ((^ A0 . (A0 A0)) (^ B0 . ((a0 a0) (B0 B0)))) didn't succeeded in 25 steps. 88. ((^ A0 . (A0 A0)) (^ B0 . (B0 ((B0 B0) B0)))) didn't succeeded in 25 steps. 89. ((^ A0 . (A0 A0)) (^ B0 . (B0 ((^ C0 . B0) B0)))) didn't succeeded in 25 steps. 90. ((^ A0 . (A0 A0)) (^ B0 . (B0 ((^ C0 . C0) B0)))) didn't succeeded in 25 steps. 91. ((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 (B0 B0))))) didn't succeeded in 25 steps. 92. ((^ A0 . (A0 A0)) (^ B0 . (B0 (^ C0 . (B0 B0))))) failed. 93. ((^ A0 . (A0 A0)) (^ B0 . (B0 (^ C0 . (B0 C0))))) didn't succeeded in 25 steps. 94. ((^ A0 . (A0 A0)) (^ B0 . (B0 (^ C0 . (C0 B0))))) failed. 95. ((^ A0 . (A0 A0)) (^ B0 . (B0 (^ C0 . (C0 C0))))) failed. 96. ((^ A0 . (A0 A0)) (^ B0 . (B0 (a0 (B0 B0))))) didn't succeeded in 25 steps. 97. ((^ A0 . (A0 A0)) (^ B0 . (a0 (B0 (B0 B0))))) didn't succeeded in 25 steps. 98. ((^ A0 . (A0 A0)) (^ B0 . (a0 (a0 (B0 B0))))) didn't succeeded in 25 steps. 99. ((^ A0 . (^ B0 . ((A0 A0) A0))) (^ C0 . (C0 C0))) failed. 100. ((^ A0 . (^ B0 . ((A0 A0) B0))) (^ C0 . (C0 C0))) failed. 101. ((^ A0 . (^ B0 . ((A0 A0) a0))) (^ C0 . (C0 C0))) failed. 102. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . ((C0 C0) C0))) didn't succeeded in 25 steps. 103. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . ((C0 C0) a0))) didn't succeeded in 25 steps. 104. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (C0 (C0 C0)))) didn't succeeded in 25 steps. 105. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (a0 (C0 C0)))) didn't succeeded in 25 steps. 106. ((^ A0 . (^ B0 . (B0 (A0 A0)))) (^ C0 . (C0 C0))) failed. 107. ((^ A0 . (^ B0 . (^ C0 . (A0 A0)))) (^ D0 . (D0 D0))) failed. 108. ((^ A0 . (^ B0 . (a0 (A0 A0)))) (^ C0 . (C0 C0))) failed. 109. ((^ A0 . (a0 ((A0 A0) a0))) (^ B0 . (B0 B0))) failed. 110. ((^ A0 . (a0 (A0 (A0 A0)))) (^ B0 . (B0 B0))) failed. 111. ((^ A0 . (a0 (A0 A0))) (^ B0 . ((B0 B0) B0))) didn't succeeded in 25 steps. 112. ((^ A0 . (a0 (A0 A0))) (^ B0 . ((B0 B0) b0))) didn't succeeded in 25 steps. 113. ((^ A0 . (a0 (A0 A0))) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 114. ((^ A0 . (a0 (A0 A0))) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 115. ((^ A0 . (a0 (A0 A0))) (^ B0 . (b0 (B0 B0)))) didn't succeeded in 25 steps. 116. ((^ A0 . (a0 (^ B0 . (A0 A0)))) (^ C0 . (C0 C0))) failed. 117. ((^ A0 . (a0 (b0 (A0 A0)))) (^ B0 . (B0 B0))) failed. 118. ((^ A0 . A0) ((^ B0 . (B0 B0)) (^ C0 . (C0 C0)))) failed. 119. ((a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) a0) failed. 120. ((a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) b0) failed. 121. ((a0 a0) ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) failed. 122. ((a0 b0) ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) failed. 123. (^ A0 . (((^ B0 . (B0 B0)) (^ C0 . (C0 C0))) A0)) failed. 124. (^ A0 . (((^ B0 . (B0 B0)) (^ C0 . (C0 C0))) a0)) failed. 125. (^ A0 . ((^ B0 . ((B0 B0) A0)) (^ C0 . (C0 C0)))) failed. 126. (^ A0 . ((^ B0 . ((B0 B0) B0)) (^ C0 . (C0 C0)))) failed. 127. (^ A0 . ((^ B0 . ((B0 B0) a0)) (^ C0 . (C0 C0)))) failed. 128. (^ A0 . ((^ B0 . (A0 (B0 B0))) (^ C0 . (C0 C0)))) failed. 129. (^ A0 . ((^ B0 . (B0 (B0 B0))) (^ C0 . (C0 C0)))) failed. 130. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . ((C0 C0) A0)))) didn't succeeded in 25 steps. 131. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . ((C0 C0) C0)))) didn't succeeded in 25 steps. 132. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . ((C0 C0) a0)))) didn't succeeded in 25 steps. 133. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (A0 (C0 C0))))) didn't succeeded in 25 steps. 134. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (C0 (C0 C0))))) didn't succeeded in 25 steps. 135. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (a0 (C0 C0))))) didn't succeeded in 25 steps. 136. (^ A0 . ((^ B0 . (^ C0 . (B0 B0))) (^ D0 . (D0 D0)))) failed. 137. (^ A0 . ((^ B0 . (a0 (B0 B0))) (^ C0 . (C0 C0)))) failed. 138. (^ A0 . (A0 ((^ B0 . (B0 B0)) (^ C0 . (C0 C0))))) failed. 139. (^ A0 . (^ B0 . ((^ C0 . (C0 C0)) (^ D0 . (D0 D0))))) failed. 140. (^ A0 . (a0 ((^ B0 . (B0 B0)) (^ C0 . (C0 C0))))) failed. 141. (a0 (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0)) failed. 142. (a0 (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) b0)) failed. 143. (a0 ((^ A0 . ((A0 A0) A0)) (^ B0 . (B0 B0)))) failed. 144. (a0 ((^ A0 . ((A0 A0) a0)) (^ B0 . (B0 B0)))) failed. 145. (a0 ((^ A0 . (A0 (A0 A0))) (^ B0 . (B0 B0)))) failed. 146. (a0 ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) B0)))) didn't succeeded in 25 steps. 147. (a0 ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) b0)))) didn't succeeded in 25 steps. 148. (a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 B0))))) didn't succeeded in 25 steps. 149. (a0 ((^ A0 . (A0 A0)) (^ B0 . (b0 (B0 B0))))) didn't succeeded in 25 steps. 150. (a0 ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (C0 C0)))) failed. 151. (a0 ((^ A0 . (a0 (A0 A0))) (^ B0 . (B0 B0)))) failed. 152. (a0 (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (C0 C0))))) failed. 153. (a0 (a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 B0))))) failed.