formula(n, 121627).
formula(dr(np, n), 76363).
formula(let, 37678).
formula(dl(n, n), 30899).
formula(dr(dl(n, n), n), 28693).
formula(np, 27896).
formula(dr(dl(n, n), np), 20425).
formula(dl(s, txt), 19394).
formula(dr(n, n), 11783).
formula(dr(dl(np, s), np), 9301).
formula(dr(dl(np, np), np), 8748).
formula(dr(dl(s, s), np), 8034).
formula(dr(np, np), 6296).
formula(dl(s, s), 6204).
formula(dr(dl(np, s), dl(np, s_ppart)), 5671).
formula(dr(dl(np, s), dl(np, s)), 5611).
formula(dr(dl(np, s_inf), np), 5350).
formula(dr(dl(s, s), n), 4936).
formula(cl_r, 4559).
formula(dr(dl(n, n), dl(n, n)), 4202).
formula(dr(dl(np, s_inf), dl(np, s_inf)), 4079).
formula(dr(dl(np, s), dl(np, s_inf)), 3951).
formula(dr(dl(s, s), s), 3800).
formula(dr(pp_a, np), 3683).
formula(dr(dl(dl(n, n), dl(n, n)), dl(n, n)), 3677).
formula(dr(pp_de, np), 3577).
formula(dr(dl(n, n), dl(np, s)), 3250).
formula(dr(s_q, s), 3045).
formula(dr(dr(s, s), np), 2989).
formula(dr(pp, np), 2915).
formula(dr(pp_de, n), 2701).
formula(dr(dl(np, s_ppart), np), 2586).
formula(dr(s, s), 2559).
formula(dr(pp_a, n), 2305).
formula(dr(dl(np, np), n), 2216).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s)), 2204).
formula(dr(pp_par, np), 2176).
formula(dr(dl(np, s), dl(n, n)), 2008).
formula(dr(dr(s, s), n), 1898).
formula(dr(dl(n, n), dl(np, s_inf)), 1610).
formula(dr(dl(np, s), dr(dl(np, s), np)), 1577).
formula(dr(dl(np, s), dl(np, s_pass)), 1570).
formula(dl(np, s), 1551).
formula(dl(np, s_pass), 1393).
formula(dr(dl(s, s), dl(s, s)), 1294).
formula(dr(dl(np, s), pp), 1280).
formula(dl(np, s_inf), 1229).
formula(dr(dl(np, s), dr(dl(np, s), pp_a)), 1078).
formula(dr(dl(s, s), dl(np, s_inf)), 1045).
formula(dr(dl(n, n), pp), 1045).
formula(dl(cl_r, dl(np, s)), 1004).
formula(dr(dl(n, n), pp_par), 977).
formula(dr(dl(n, n), pp_de), 922).
formula(dr(dl(n, n), s), 920).
formula(dr(dl(dl(n, n), dl(n, n)), np), 895).
formula(dr(dl(n, n), pp_a), 890).
formula(dr(pp, n), 875).
formula(dr(dl(n, n), dr(s, np)), 846).
formula(dr(np, pp_de), 839).
formula(dr(dl(pp, pp), pp), 830).
formula(dr(dl(np, s), s_q), 773).
formula(dr(dl(np, s_ppart), dl(np, s_pass)), 718).
formula(dr(dl(np, s_ppres), np), 706).
formula(dr(dl(np, np), dl(n, n)), 688).
formula(dl(np, txt), 687).
formula(dr(dl(np, s), pp_a), 672).
formula(dr(dl(cl_r, dl(np, s)), dl(cl_r, dl(np, s_ppart))), 664).
formula(dr(dl(np, s_ppart), dl(np, s_inf)), 661).
formula(dr(dl(np, s_pass), pp_par), 625).
formula(dr(dl(dl(n, n), dl(n, n)), n), 604).
formula(dr(dl(np, np), dl(np, s)), 593).
formula(dl(np, np), 573).
formula(dr(dr(s, s), s), 570).
formula(dl(np, s_ppart), 569).
formula(dr(dr(dl(np, s), pp_a), np), 562).
formula(dr(dl(np, s), pp_de), 558).
formula(dr(dl(s, s), s), 532).
formula(dr(dl(s, s), s_q), 518).
formula(dr(s, np), 472).
formula(dr(dl(cl_r, dl(np, s)), pp), 468).
formula(dr(n, pp_de), 467).
formula(cl_y, 463).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s_ppres)), 426).
formula(dr(s_q, np), 417).
formula(dr(dl(dl(s, s), dl(s, s)), dl(s, s)), 409).
formula(dr(dl(np, s_inf), pp), 398).
formula(dl(cl_r, dl(np, s_inf)), 395).
formula(dr(dl(np, s_inf), pp_a), 393).
formula(dr(dr(dl(n, n), dl(np, s)), np), 385).
formula(dr(dl(np, s_inf), dl(np, s_pass)), 383).
formula(dr(dl(dl(np, s), np), np), 358).
formula(dr(dr(n, n), dr(n, n)), 356).
formula(dr(dl(np, s_inf), pp_de), 346).
formula(dr(pp, pp), 343).
formula(dr(dl(s, s), np), 343).
formula(dr(dl(np, s_pass), pp_a), 334).
formula(dl(n, txt), 332).
formula(dr(dr(s, s), dr(s, s)), 327).
formula(dr(dr(dl(n, n), s_q), dl(n, n)), 326).
formula(dr(dr(dl(np, s_inf), pp_a), np), 318).
formula(dr(dl(np, s_ppart), pp), 312).
formula(dr(dr(s, np), np), 311).
formula(dl(cl_r, dl(np, s_ppart)), 311).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s_inf)), 304).
formula(dr(dl(s, s), pp_de), 303).
formula(dr(dl(np, s_pass), pp), 290).
formula(dr(dl(cl_r, dl(np, s)), pp_a), 277).
formula(dr(dl(np, s_inf), dl(np, s_ppart)), 276).
formula(dr(dr(s, s), dl(np, s_inf)), 274).
formula(dr(dl(np, s_ppart), pp_de), 261).
formula(dr(dl(cl_r, dl(np, s)), pp_de), 259).
formula(dr(dl(cl_y, dl(np, s)), np), 253).
formula(dr(dl(np, np), dr(s, np)), 246).
formula(dr(dl(np, s_inf), s_q), 242).
formula(dr(dl(np, s_ppart), s_q), 240).
formula(dr(dl(dr(np, n), dr(np, n)), dr(np, n)), 231).
formula(dr(dl(np, s_pass), pp_de), 225).
formula(dr(dr(np, np), n), 224).
formula(dr(dl(s, s), pp), 223).
formula(dr(dl(np, s_ppart), pp_a), 217).
formula(dr(dl(dr(pp, np), dl(n, n)), s), 210).
formula(dl(dl(n, n), dl(n, n)), 207).
formula(dr(dr(dl(n, n), dl(n, n)), n), 201).
formula(dr(s_whq, s), 199).
formula(dr(dr(dl(np, s_ppart), pp_a), np), 197).
formula(dr(dl(np, s), s), 197).
formula(dl(dr(s, s), txt), 195).
formula(dr(dr(s, np), dl(np, s_ppart)), 193).
formula(dr(dl(np, np), s), 189).
formula(dr(dl(np, s_ppart), dl(n, n)), 182).
formula(dr(dl(np, s), dr(dl(np, s), pp_de)), 177).
formula(dr(dr(dl(np, s), pp_de), np), 176).
formula(dr(s_q, pp), 171).
formula(dr(dl(cl_r, dl(np, s)), dl(np, s_inf)), 167).
formula(dl(s, dl(np, s_ppart)), 167).
formula(dr(dl(dr(n, n), dr(n, n)), dr(n, n)), 165).
formula(dr(dr(dl(np, s_inf), pp), np), 162).
formula(dr(dl(cl_r, dl(np, s)), dl(cl_r, dl(np, s))), 162).
formula(dr(dr(s, s), pp_a), 157).
formula(dr(dr(dl(np, s), dl(np, s_inf)), np), 157).
formula(dr(np, dl(n, n)), 156).
formula(dr(dr(s, s), s_q), 150).
formula(dr(dl(np, s_inf), dl(n, n)), 149).
formula(dr(n, pp_a), 144).
formula(dr(dl(cl_r, dl(np, s_inf)), pp_a), 143).
formula(dr(dl(cl_r, dl(np, s_inf)), pp), 141).
formula(dr(dl(n, s), s), 140).
formula(dr(dr(dl(np, s), dl(np, s_inf)), pp_a), 126).
formula(dr(dr(dl(s, s), dl(s, s)), n), 120).
formula(dr(dl(np, s_pass), dl(np, s_inf)), 119).
formula(dr(dr(dl(np, s), np), pp_a), 116).
formula(dr(dl(s, s), pp_a), 116).
formula(dr(dl(n, n), s_q), 116).
formula(dr(dl(cl_r, dl(np, s)), dl(n, n)), 113).
formula(dr(dl(dr(s, s), dr(s, s)), dr(s, s)), 108).
formula(s, 103).
formula(dr(dr(dl(np, s), pp), np), 102).
formula(dr(dr(dl(np, s_inf), pp_de), np), 101).
formula(dr(dr(dl(np, s_ppart), dl(np, s_inf)), np), 100).
formula(dr(dr(s, s), pp_de), 99).
formula(dr(dl(pp_de, pp_a), np), 98).
formula(dr(dl(np, s_ppres), dl(np, s_inf)), 98).
formula(dr(dl(n, n), dr(s, pp_de)), 98).
formula(dr(dl(cl_r, dl(np, s)), np), 96).
formula(dr(dl(cl_r, dl(np, s)), dr(dl(cl_r, dl(np, s)), pp_de)), 95).
formula(dr(dr(dl(np, s_inf), np), pp), 94).
formula(dr(s, dr(s, np)), 93).
formula(dr(dr(dl(np, s), np), pp), 93).
formula(dl(np, s_ppres), 92).
formula(dr(dr(dl(np, s_inf), np), dl(np, s_inf)), 91).
formula(dr(dr(np, np), np), 89).
formula(dr(dr(s, dl(np, s_inf)), np), 88).
formula(dr(dr(dl(np, s_inf), dl(np, s_inf)), np), 88).
formula(dr(dr(dl(np, s), s_q), dl(n, n)), 87).
formula(dr(dl(cl_r, dl(np, s_inf)), pp_de), 86).
formula(dr(dl(np, s_ppres), s_q), 85).
formula(dr(dl(np, np), dl(np, s_inf)), 85).
formula(dr(dr(dl(np, s), s_q), pp), 84).
formula(dr(dl(n, n), dr(s, pp_a)), 84).
formula(dr(dr(n, s_q), n), 83).
formula(dr(dl(dl(n, n), np), np), 82).
formula(dr(dl(cl_r, dl(np, s_ppart)), pp), 81).
formula(dr(np, s_q), 79).
formula(dr(dl(cl_r, dl(np, s_ppart)), pp_a), 77).
formula(dr(dl(np, s_ppres), pp), 76).
formula(dr(dl(cl_r, s), np), 76).
formula(dr(dr(dl(np, s), dl(np, s_inf)), dl(n, n)), 74).
formula(dr(dl(np, s_ppres), dl(np, s_ppart)), 74).
formula(dr(dl(cl_r, dl(np, s)), dr(dl(cl_r, dl(np, s)), pp_a)), 74).
formula(dr(dr(dr(s, dl(np, s)), np), dl(np, s_inf)), 73).
formula(dr(dr(dr(s, s), dr(s, s)), n), 72).
formula(dr(pp_a, pp_de), 71).
formula(dr(dl(cl_r, dl(np, s_inf)), np), 71).
formula(dr(dr(dl(np, s_inf), np), pp_a), 70).
formula(dr(s_q, dl(n, n)), 69).
formula(dr(dl(dr(pp, np), dl(n, n)), dr(s, pp)), 69).
formula(dr(dr(dl(np, s_ppres), pp_a), np), 67).
formula(dr(dl(np, s_ppres), pp_de), 67).
formula(dr(dr(dl(np, s_ppart), pp_de), np), 63).
formula(dr(dr(dl(n, n), pp_de), dl(n, n)), 63).
formula(dr(s_whq, dr(s, np)), 62).
formula(dr(dl(np, s_pass), dl(n, n)), 60).
formula(dr(dr(s, dl(np, s_ppart)), np), 59).
formula(dr(dr(dr(s, dl(np, s)), np), dl(np, s_ppres)), 59).
formula(dr(dl(pp_de, dl(n, n)), dl(n, n)), 59).
formula(dr(dl(np, np), s_q), 59).
formula(dr(dl(dr(dl(np, s), np), dr(dl(np, s), np)), dr(dl(np, s), np)), 59).
formula(dr(dl(cl_r, dl(np, s_ppart)), pp_de), 59).
formula(dl(dl(np, s), txt), 59).
formula(dr(dr(dl(s, s), s_q), dl(s, s)), 58).
formula(dr(dl(cl_r, dl(np, s_ppres)), pp_a), 58).
formula(dr(dr(s, s), pp), 57).
formula(dr(dl(np, s_ppres), pp_a), 56).
formula(dr(dl(np, s), s_whq), 56).
formula(dr(dl(cl_y, dl(np, dl(s, s))), np), 56).
formula(dr(dl(cl_r, dl(np, s_ppres)), pp_de), 56).
formula(dr(dl(s, s), n), 55).
formula(dr(dl(cl_r, dl(np, s_ppart)), dl(np, s_inf)), 55).
formula(dr(dr(s, s), dl(np, s_ppres)), 54).
formula(dl(np, dl(s, s)), 54).
formula(dr(dr(s, np), dl(np, s_inf)), 53).
formula(dr(dr(dl(np, s_ppart), pp), np), 52).
formula(dr(dl(s, s), dl(s, s)), 52).
formula(dr(dr(s, dl(n, n)), np), 50).
formula(dr(dr(dl(np, s), np), dl(np, s_inf)), 50).
formula(dr(s_whq, dl(np, s_inf)), 49).
formula(dr(dr(s, np), dl(np, s_pass)), 49).
formula(dr(dr(dl(n, n), dl(n, n)), np), 49).
formula(dr(s_q, dl(np, s)), 48).
formula(dr(dr(dl(np, s), dl(n, n)), np), 48).
formula(dr(dl(np, s_inf), s_whq), 48).
formula(dr(dr(dl(np, s_ppart), dl(np, s_inf)), pp_a), 46).
formula(dr(dr(dl(np, s), np), dl(n, n)), 46).
formula(dr(s, s_q), 44).
formula(dr(dr(dl(np, s_inf), dl(np, s_inf)), pp_a), 44).
formula(dr(dr(s, pp), np), 43).
formula(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), 43).
formula(dr(dl(dl(np, np), dl(np, np)), dl(n, n)), 43).
formula(dr(dr(np, np), dr(np, np)), 42).
formula(dr(dl(np, s), dr(dl(np, s), np)), 42).
formula(dr(dl(np, np), pp), 42).
formula(dr(n, s_q), 41).
formula(dr(dr(dl(np, s), s_q), pp_a), 41).
formula(dr(dl(np, s_ppres), dl(np, s_pass)), 39).
formula(dl(dl(n, n), txt), 39).
formula(dr(dr(dl(np, s_ppart), np), dl(np, s_inf)), 36).
formula(dl(cl_r, dl(np, s_ppres)), 36).
formula(dr(dl(s, s), dl(np, s)), 35).
formula(dr(dl(np, s_pass), np), 35).
formula(dr(pp, pp_de), 34).
formula(dr(dr(s, pp_de), np), 34).
formula(dr(dr(dl(n, n), dl(np, s_inf)), dl(n, n)), 34).
formula(dr(dl(np, s_ppres), dl(n, n)), 34).
formula(dr(dl(dl(n, n), s), np), 34).
formula(dr(dl(cl_y, dl(np, dl(dl(n, n), dl(n, n)))), np), 34).
formula(dr(dr(dl(s, s), np), n), 33).
formula(dr(dr(dl(np, s_ppart), np), pp), 33).
formula(dr(dr(dl(np, s), pp_a), dl(np, s_inf)), 33).
formula(dr(dl(dl(n, n), dl(n, n)), dl(np, s_inf)), 33).
formula(dr(dl(cl_r, dl(np, s_ppart)), dl(n, n)), 33).
formula(dr(s_q, dl(s, s)), 32).
formula(dr(dr(dl(np, s_inf), dl(n, n)), np), 32).
formula(dr(dl(dl(n, n), dl(n, n)), pp_de), 32).
formula(dr(dr(dl(np, s_inf), np), pp_de), 31).
formula(dr(dl(cl_r, dl(np, s)), pp_par), 31).
formula(dr(dr(pp, pp), n), 30).
formula(dr(dr(dl(np, s_ppart), np), pp_a), 30).
formula(dr(dl(dr(pp, np), s_whq), dr(s, pp)), 30).
formula(dr(dl(cl_r, dl(np, s_inf)), dl(np, s_inf)), 30).
formula(dr(dr(dl(np, s), np), pp_de), 29).
formula(dr(dr(dl(np, s), dl(np, s)), n), 27).
formula(dr(dl(s, s), dl(n, n)), 27).
formula(dr(dl(dr(s, dr(dl(np, s), pp)), dr(s, dr(dl(np, s), pp))), dr(s, dr(dl(np, s), pp))), 27).
formula(dr(dl(cl_r, dl(np, s_ppart)), np), 27).
formula(dr(s, dr(s, pp_a)), 26).
formula(dr(dl(s, s), dl(n, n)), 26).
formula(dr(dl(pp_de, dl(s, s)), dl(s, s)), 26).
formula(dr(dl(np, dl(np, np)), np), 26).
formula(dr(dl(n, dl(s, s)), n), 26).
formula(dr(dl(dr(pp, np), dl(n, n)), np), 26).
formula(dr(dl(cl_y, dl(np, dr(s, s))), np), 26).
formula(dr(pp_par, n), 25).
formula(dr(dr(s, s_q), np), 25).
formula(dr(s, dl(np, s_inf)), 24).
formula(dr(n, dl(np, s_inf)), 24).
formula(dr(dr(dl(np, s), pp_a), dl(n, n)), 24).
formula(dr(dl(dl(n, n), dl(n, n)), s_q), 24).
formula(dr(dl(pp_de, dl(s, s)), np), 24).
formula(dr(dl(dr(s, dr(dl(np, s), np)), dr(s, dr(dl(np, s), np))), dr(s, dr(dl(np, s), np))), 24).
formula(dr(s_whq, dl(np, s)), 23).
formula(dr(dr(dl(np, s), s_q), np), 23).
formula(dr(dl(dl(np, s_inf), s), np), 23).
formula(dr(dl(cl_y, dl(np, s_ppart)), np), 23).
formula(dr(dl(cl_y, dl(np, s)), dl(cl_y, dl(np, s_ppart))), 23).
formula(dl(cl_r, dl(s, dr(s, np))), 23).
formula(dr(dl(cl_y, dl(np, s)), dl(cl_y, dl(np, s))), 22).
formula(dr(dr(dl(np, s_ppres), pp), np), 21).
formula(dr(dr(dl(cl_r, s), pp_a), np), 21).
formula(dr(dl(dl(n, n), dl(n, n)), s), 21).
formula(dr(dl(s, s), dl(np, s)), 21).
formula(dr(dl(cl_r, dl(np, s)), s_q), 21).
formula(dr(dr(dl(np, s), np), np), 20).
formula(dr(dr(dl(np, s), dl(np, s)), dr(dl(np, s), dl(np, s))), 20).
formula(dr(dr(dl(np, s), dl(np, s)), dl(np, s_ppres)), 20).
formula(dr(dl(dr(dl(n, n), dl(n, n)), dr(dl(n, n), dl(n, n))), dr(dl(n, n), dl(n, n))), 20).
formula(dr(dl(cl_r, dl(np, s_ppart)), pp_par), 20).
formula(dr(dr(np, s_q), np), 19).
formula(dr(dr(dl(np, s), s_q), dl(np, s)), 19).
formula(dr(dl(n, n), dl(np, s_ppart)), 19).
formula(dr(dl(dl(dl(n, n), dl(n, n)), dl(dl(n, n), dl(n, n))), dl(dl(n, n), dl(n, n))), 19).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dl(dl(np, s), dl(np, s))), 19).
formula(dr(dl(cl_r, dl(np, s_inf)), dl(cl_r, dl(np, s_ppart))), 19).
formula(dr(np, pp), 18).
formula(dr(dr(dl(s, s), dl(s, s)), np), 18).
formula(dr(dr(dl(np, s), dl(np, s_inf)), pp), 18).
formula(dr(dl(s, s), dl(np, s_ppres)), 18).
formula(dr(dl(dl(n, n), dl(n, n)), pp), 18).
formula(dr(dl(np, dl(s, s)), pp_de), 18).
formula(dr(dr(s, dr(s, pp_a)), np), 17).
formula(dr(dr(dl(np, s_ppres), pp_de), np), 17).
formula(dr(dr(dl(np, s_ppres), dl(np, s_inf)), np), 17).
formula(dr(dr(dl(np, s_ppart), dl(n, n)), np), 17).
formula(dr(dr(dl(np, s_inf), np), dl(n, n)), 17).
formula(dr(dr(dl(dr(pp, np), s_whq), s), n), 17).
formula(dr(dl(np, s), pp_par), 17).
formula(dr(dl(np, dl(dr(s, np), s)), dl(np, s_ppres)), 17).
formula(dr(dl(n, n), dl(np, s_ppres)), 17).
formula(dr(dl(dr(np, n), dl(dr(pp_de, np), dr(pp_a, n))), dr(np, n)), 17).
formula(dr(dl(cl_r, dl(np, s_inf)), dl(n, n)), 17).
formula(dr(dl(cl_r, dl(np, s)), dr(dl(np, s_inf), np)), 17).
formula(dr(dr(dl(np, s_inf), s_q), pp_a), 16).
formula(dr(dl(dr(pp, np), np), dl(np, s_inf)), 16).
formula(dr(dl(cl_r, dl(np, s_inf)), dr(dl(np, s_inf), np)), 16).
formula(dr(s_q, n), 15).
formula(dr(s, dr(s, pp_de)), 15).
formula(dr(dr(dl(np, s_ppres), dl(np, s_inf)), pp_a), 15).
formula(dr(dr(dl(np, s_ppart), np), pp_de), 15).
formula(dr(dr(dl(n, n), pp_a), np), 15).
formula(dr(dl(dr(s, dr(dl(np, s), dl(n, n))), dr(s, dr(dl(np, s), dl(n, n)))), dr(s, dr(dl(np, s), dl(n, n)))), 15).
formula(dr(dl(dr(dl(np, s), np), dr(dl(np, s), np)), dr(dl(np, s), np)), 15).
formula(dr(dl(dl(np, s), s), s), 15).
formula(dl(s, dr(s, np)), 15).
formula(dr(dr(pp, pp), np), 14).
formula(dr(dr(np, s_q), pp_de), 14).
formula(dr(dr(dl(np, s_ppart), s_q), pp_a), 14).
formula(dr(dr(dl(np, s_pass), pp_par), dl(n, n)), 14).
formula(dr(dr(dl(n, n), pp_par), pp), 14).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s_inf)), 14).
formula(dr(dl(dl(np, np), dl(np, np)), np), 14).
formula(dr(dl(dl(n, n), dl(n, n)), dl(dl(n, n), dl(n, n))), 14).
formula(dr(dl(cl_r, dr(s, np)), dl(cl_r, dl(np, s_ppart))), 14).
formula(dr(dl(cl_r, dl(np, s_ppart)), dr(dl(np, s_inf), np)), 14).
formula(pp, 13).
formula(dr(dr(dl(np, s_ppres), np), pp), 13).
formula(dr(dr(dl(np, s_ppres), np), dl(np, s_inf)), 13).
formula(dr(dr(dl(np, s_pass), pp_par), pp_a), 13).
formula(dr(dr(dl(np, s_pass), pp_par), pp), 13).
formula(dr(dr(dl(np, s), dl(np, s)), dl(np, s_inf)), 13).
formula(dr(dl(dl(np, s), dl(np, s)), np), 13).
formula(dl(dl(s, s), dl(s, s)), 13).
formula(dr(dr(s, pp_a), np), 12).
formula(dr(dl(np, s_ppres), pp_par), 12).
formula(dr(dl(np, s_inf), pp_par), 12).
formula(dr(dl(np, dl(s, s)), np), 12).
formula(dr(pp_de, dl(n, n)), 11).
formula(dr(dr(pp, s_q), pp), 11).
formula(dr(dr(dl(n, n), pp_par), pp_a), 11).
formula(dr(dl(np, np), pp_de), 11).
formula(dr(dl(np, dl(s, s)), s), 11).
formula(dr(dl(dl(np, s_inf), s), dl(np, s_inf)), 11).
formula(dr(dr(dl(np, s), pp_par), np), 10).
formula(dr(dr(dl(np, s), dl(np, s)), np), 10).
formula(dr(dr(dl(n, n), pp_par), dl(n, n)), 10).
formula(dr(dr(dl(n, n), dl(n, n)), dr(dl(n, n), dl(n, n))), 10).
formula(dr(dl(dl(np, np), dl(np, np)), n), 10).
formula(dr(dl(dl(n, n), dl(n, n)), pp_a), 10).
formula(dr(dl(p(np, pp), p(np, pp)), p(np, pp)), 10).
formula(dr(dl(n, n), dr(s, pp)), 10).
formula(dr(dl(dr(s, dr(dl(np, s), dl(np, s))), dr(s, dr(dl(np, s), dl(np, s)))), dr(s, dr(dl(np, s), dl(np, s)))), 10).
formula(dr(dl(cl_y, dl(s, s)), dl(s, s)), 10).
formula(dl(dl(np, s), dl(np, s)), 10).
formula(dr(s_whq, dr(s, dl(n, n))), 9).
formula(dr(s_whq, dr(dl(np, s), np)), 9).
formula(dr(dr(dr(s, s), s_q), dr(s, s)), 9).
formula(dr(dr(dl(np, s_pass), pp_par), pp_de), 9).
formula(dr(dr(dl(np, s_inf), pp_par), np), 9).
formula(dr(dr(dl(np, s), s_q), dl(s, s)), 9).
formula(dr(dr(dl(n, n), pp_a), pp_par), 9).
formula(dr(dr(dl(n, n), dl(np, s_inf)), pp_a), 9).
formula(dr(dr(dl(cl_r, s), np), np), 9).
formula(dr(dl(pp, pp), s_q), 9).
formula(dr(dl(dr(dl(np, s), pp), dr(dl(np, s), pp)), dr(dl(np, s), pp)), 9).
formula(dr(dl(dl(n, n), s), s), 9).
formula(dr(dl(cl_y, dl(np, np)), np), 9).
formula(dr(dl(cl_y, dl(np, dl(n, n))), np), 9).
formula(dr(dl(cl_r, dl(np, s_ppres)), pp), 9).
formula(dl(s, dl(np, s_inf)), 9).
formula(dr(dr(s, dr(s, pp_a)), n), 8).
formula(dr(dr(dl(np, s_inf), pp_a), dl(np, s_inf)), 8).
formula(dr(dr(dl(np, s), s_q), pp_de), 8).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s_ppres)), 8).
formula(dr(dl(np, s_pass), s_q), 8).
formula(dr(dl(np, np), pp_par), 8).
formula(dr(dl(np, dr(s, s)), pp_de), 8).
formula(dr(dl(dl(np, s), s), dl(dl(np, s), s)), 8).
formula(dr(dl(dl(n, n), dr(s, s)), dr(s, dl(n, n))), 8).
formula(dr(dl(dl(n, n), dl(n, n)), dl(n, n)), 8).
formula(dr(s, pp), 7).
formula(dr(pp_a, dl(n, n)), 7).
formula(dr(np, s), 7).
formula(dr(np, dl(np, s)), 7).
formula(dr(dr(dl(np, s_ppres), np), pp_de), 7).
formula(dr(dr(dl(np, s_ppres), dl(n, n)), np), 7).
formula(dr(dr(dl(n, n), np), pp), 7).
formula(dr(dl(dl(n, n), dl(n, n)), dl(np, s_ppres)), 7).
formula(dr(dl(p(dl(s, s), np), p(dl(s, s), np)), p(dl(s, s), np)), 7).
formula(dr(dl(np, np), pp_a), 7).
formula(dr(dl(dr(np, n), dl(dr(pp_de, np), dr(np, n))), dr(np, n)), 7).
formula(dr(dl(dl(np, s_inf), s), dl(n, n)), 7).
formula(dr(dl(cl_y, dl(np, pp)), np), 7).
formula(dr(dl(cl_r, dl(np, s_ppres)), dl(np, s_inf)), 7).
formula(dr(dl(cl_r, dl(np, s_inf)), s_whq), 7).
formula(dr(dl(cl_r, dl(np, s_inf)), s_q), 7).
formula(dr(dl(cl_r, dl(n, n)), pp_a), 7).
formula(dl(dr(s, s), dr(s, s)), 7).
formula(dr(s_whq, dr(s, pp)), 6).
formula(dr(pp_de, pp), 6).
formula(dr(dr(s, s), dl(n, n)), 6).
formula(dr(dr(s, pp), cl_r), 6).
formula(dr(dr(s, np), pp), 6).
formula(dr(dr(pp, pp), dr(pp, pp)), 6).
formula(dr(dr(np, np), dl(np, s_inf)), 6).
formula(dr(dr(dr(s, s), np), n), 6).
formula(dr(dr(dr(dl(np, s), dl(np, s_inf)), pp_a), dl(n, n)), 6).
formula(dr(dr(dl(np, s_ppres), np), dl(n, n)), 6).
formula(dr(dr(dl(np, s_inf), s_q), pp_de), 6).
formula(dr(dr(dl(n, n), pp_de), np), 6).
formula(dr(dl(s, dl(np, s_ppart)), pp_a), 6).
formula(dr(dl(pp_de, pp_a), n), 6).
formula(dr(dl(pp_de, dl(s, s)), n), 6).
formula(dr(dl(pp, dl(n, n)), s), 6).
formula(dr(dl(np, s_ppart), s_whq), 6).
formula(dr(dl(np, np), dr(s, pp_de)), 6).
formula(dr(dl(dr(dl(np, s), dl(np, s)), dr(dl(np, s), dl(np, s))), dr(dl(np, s), dl(np, s))), 6).
formula(dr(dl(dr(dl(n, n), n), dr(dl(n, n), n)), dr(dl(n, n), n)), 6).
formula(dr(dl(cl_r, dl(np, s_ppart)), dr(dl(np, s_inf), pp_a)), 6).
formula(dr(dl(cl_r, dl(np, s)), s_whq), 6).
formula(dr(dr(s_whq, dl(np, s)), pp_de), 5).
formula(dr(dr(dr(s, pp_a), np), np), 5).
formula(dr(dr(dr(s, np), pp_a), np), 5).
formula(dr(dr(dr(s, dl(np, s_inf)), dl(n, n)), np), 5).
formula(dr(dr(dr(dr(s, dl(np, s)), np), dr(dr(s, dl(np, s)), np)), n), 5).
formula(dr(dr(dl(np, s_pass), dl(np, s_inf)), pp_par), 5).
formula(dr(dr(dl(np, s_inf), np), np), 5).
formula(dr(dr(dl(cl_r, s), pp), np), 5).
formula(dr(dl(dl(np, s), dl(np, s)), np), 5).
formula(dr(dl(pp_de, np), np), 5).
formula(dr(dl(pp_de, dl(n, n)), np), 5).
formula(dr(dl(np, np), dl(np, np)), 5).
formula(dr(dl(np, dl(dl(n, n), dl(n, n))), dl(n, n)), 5).
formula(dr(dl(n, n), dr(dl(n, n), pp_a)), 5).
formula(dr(dl(dr(pp, np), s_whq), s), 5).
formula(dr(dl(dr(pp, np), dl(np, np)), dr(s, pp)), 5).
formula(dr(dl(dr(pp, n), dl(n, n)), s), 5).
formula(dr(dl(dr(np, n), dr(np, n)), dr(np, n)), 5).
formula(dr(dl(dr(dl(s, s), n), dr(dl(s, s), n)), dr(dl(s, s), n)), 5).
formula(dr(dl(dr(dl(n, n), np), dr(dl(n, n), np)), dr(dl(n, n), np)), 5).
formula(dr(dl(dl(n, n), dl(n, n)), np), 5).
formula(dr(dl(dl(cl_r, dl(np, s)), dl(cl_r, dl(np, s))), dl(cl_r, dl(np, s))), 5).
formula(dr(dl(cl_y, dl(n, n)), dl(n, n)), 5).
formula(dl(np, dr(s, s)), 5).
formula(s_whq, 4).
formula(dr(s_whq, np), 4).
formula(dr(dr(s, s), dl(np, s_ppart)), 4).
formula(dr(dr(n, n), n), 4).
formula(dr(dr(dr(s, pp_de), np), np), 4).
formula(dr(dr(dl(s, s), pp_a), np), 4).
formula(dr(dr(dl(np, s_ppart), s_q), np), 4).
formula(dr(dr(dl(np, s_pass), pp_a), np), 4).
formula(dr(dr(dl(np, s_inf), s_q), np), 4).
formula(dr(dr(dl(n, n), pp), dl(n, n)), 4).
formula(dr(dl(pp_de, dr(s, s)), np), 4).
formula(dr(dl(pp, s_q), dr(s, pp)), 4).
formula(dr(dl(np, dl(pp, pp)), pp), 4).
formula(dr(dl(np, dl(n, n)), dl(n, n)), 4).
formula(dr(dl(np, dl(dl(s, s), dl(s, s))), dl(s, s)), 4).
formula(dr(dl(np, dl(dl(np, s), dl(np, s))), dl(np, s)), 4).
formula(dr(dl(n, n), dr(dl(n, n), np)), 4).
formula(dr(dl(n, n), dl(np, s_pass)), 4).
formula(dr(dl(dr(pp, np), s_whq), n), 4).
formula(dr(dl(dr(pp, np), dl(np, np)), s), 4).
formula(dr(dl(dr(dl(n, n), n), dr(dl(n, n), n)), dr(dl(n, n), n)), 4).
formula(dr(dl(dl(n, n), dl(s, s)), dr(s, dl(n, n))), 4).
formula(dr(dl(cl_y, dl(s, s)), np), 4).
formula(dr(dl(cl_r, s), dr(dl(cl_r, s), pp_a)), 4).
formula(dr(dl(cl_r, dl(np, s_ppres)), dl(n, n)), 4).
formula(dr(dl(cl_r, dl(np, s_ppart)), s_q), 4).
formula(dr(dl(cl_r, dl(np, s_inf)), pp_par), 4).
formula(pp_a, 3).
formula(dr(s, s_whq), 3).
formula(dr(s, cl_r), 3).
formula(dr(pp_a, dl(np, s_inf)), 3).
formula(dr(dr(s, np), pp_a), 3).
formula(dr(dr(s, np), dl(n, n)), 3).
formula(dr(dr(s, dr(s, pp_de)), np), 3).
formula(dr(dr(s, dl(np, s_pass)), np), 3).
formula(dr(dr(dr(s, s), dr(s, s)), pp_de), 3).
formula(dr(dr(dl(s, s), dl(s, s)), dl(n, n)), 3).
formula(dr(dr(dl(dl(n, n), dl(n, n)), dl(dl(n, n), dl(n, n))), n), 3).
formula(dr(dr(dl(np, s_ppart), pp_par), np), 3).
formula(dr(dr(dl(np, s_ppart), np), dl(n, n)), 3).
formula(dr(dr(dl(np, s_ppart), dl(np, s_inf)), pp), 3).
formula(dr(dr(dl(np, s_pass), pp_a), pp_par), 3).
formula(dr(dr(dl(np, s_pass), dl(n, n)), pp_par), 3).
formula(dr(dr(dl(np, s_inf), np), pp_par), 3).
formula(dr(dr(dl(np, s_inf), dl(np, s_inf)), dl(n, n)), 3).
formula(dr(dr(dl(np, s), s_q), dl(np, s_inf)), 3).
formula(dr(dr(dl(np, s), dl(np, s_ppart)), np), 3).
formula(dr(dr(dl(n, n), np), pp_a), 3).
formula(dr(dr(dl(n, n), np), n), 3).
formula(dr(dr(dl(n, n), dl(np, s_inf)), np), 3).
formula(dr(dr(dl(n, n), dl(n, n)), pp), 3).
formula(dr(dr(dl(dr(pp, np), s_whq), dr(s, pp)), n), 3).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), n), 3).
formula(dr(dl(s, s), dr(dl(s, s), pp_a)), 3).
formula(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), 3).
formula(dr(dl(pp_de, pp), pp), 3).
formula(dr(dl(p(pp, np), p(pp, np)), p(pp, np)), 3).
formula(dr(dl(p(np, dl(np, s)), p(np, dl(np, s))), p(np, dl(np, s))), 3).
formula(dr(dl(np, np), dr(s, s)), 3).
formula(dr(dl(np, np), dr(s, pp_a)), 3).
formula(dr(dl(np, dl(n, n)), pp_de), 3).
formula(dr(dl(dr(s, np), dr(s, np)), dl(np, s_ppres)), 3).
formula(dr(dl(dr(s, np), dr(s, np)), dr(s, np)), 3).
formula(dr(dl(dr(np, np), dr(np, np)), dr(np, np)), 3).
formula(dr(dl(dr(dr(s, dl(np, s)), np), dr(dr(s, dl(np, s)), np)), dr(dr(s, dl(np, s)), np)), 3).
formula(dr(dl(dr(dr(dr(s, s), s_q), dr(s, s)), dr(dr(dr(s, s), s_q), dr(s, s))), dr(dr(dr(s, s), s_q), dr(s, s))), 3).
formula(dr(dl(dr(dr(dl(n, n), dl(n, n)), n), dr(dr(dl(n, n), dl(n, n)), n)), dr(dr(dl(n, n), dl(n, n)), n)), 3).
formula(dr(dl(dr(dl(n, n), pp), dr(dl(n, n), pp)), dr(dl(n, n), pp)), 3).
formula(dr(dl(dl(n, n), n), n), 3).
formula(dr(dl(dl(n, n), dl(n, n)), dr(s, dl(n, n))), 3).
formula(dr(dl(cl_y, dl(np, s_inf)), np), 3).
formula(dr(dl(cl_y, dl(np, s)), pp), 3).
formula(dr(dl(cl_y, dl(np, s)), dl(np, s_inf)), 3).
formula(dr(dl(cl_r, dl(np, s)), dr(dl(cl_r, dl(np, s)), np)), 3).
formula(dl(np, dl(dl(n, n), dl(n, n))), 3).
formula(dr(s_whq, pp_de), 2).
formula(dr(s_whq, n), 2).
formula(dr(s, pp_a), 2).
formula(dr(s, dl(n, n)), 2).
formula(dr(pp, s_q), 2).
formula(dr(pp, pp_a), 2).
formula(dr(dr(s_whq, dr(s, np)), pp_de), 2).
formula(dr(dr(s_whq, dr(s, np)), n), 2).
formula(dr(dr(s_whq, dl(np, s)), n), 2).
formula(dr(dr(s, s), dl(np, s)), 2).
formula(dr(dr(s, np), s), 2).
formula(dr(dr(s, dr(s, pp_de)), n), 2).
formula(dr(dr(s, dl(np, s_inf)), pp_a), 2).
formula(dr(dr(np, np), s), 2).
formula(dr(dr(n, n), np), 2).
formula(dr(dr(dr(s, s_q), pp), np), 2).
formula(dr(dr(dr(s, s), np), pp), 2).
formula(dr(dr(dr(s, s), dr(s, s)), np), 2).
formula(dr(dr(dr(s, np), np), dl(np, s_inf)), 2).
formula(dr(dr(dr(dl(np, s), dl(np, s_inf)), pp_a), np), 2).
formula(dr(dr(dr(dl(np, s), dl(np, s)), dr(dl(np, s), dl(np, s))), n), 2).
formula(dr(dr(dl(s, s), np), pp), 2).
formula(dr(dr(dl(s, s), dl(s, s)), pp_de), 2).
formula(dr(dr(dl(np, s_ppart), s_q), pp_de), 2).
formula(dr(dr(dl(np, s_ppart), pp_a), dl(n, n)), 2).
formula(dr(dr(dl(np, s_ppart), dl(np, s_inf)), dl(n, n)), 2).
formula(dr(dr(dl(np, s_pass), pp_par), np), 2).
formula(dr(dr(dl(np, s_pass), dl(np, s_inf)), pp_a), 2).
formula(dr(dr(dl(np, s_inf), s_whq), pp_a), 2).
formula(dr(dr(dl(np, s_inf), s_q), pp), 2).
formula(dr(dr(dl(np, s), s_whq), pp_a), 2).
formula(dr(dr(dl(np, s), s), s), 2).
formula(dr(dr(dl(np, s), pp_de), pp_a), 2).
formula(dr(dr(dl(np, s), pp_a), pp_de), 2).
formula(dr(dr(dl(np, s), pp_a), pp_a), 2).
formula(dr(dr(dl(np, np), s_q), dl(n, n)), 2).
formula(dr(dr(dl(n, s), s), n), 2).
formula(dr(dr(dl(n, n), pp_par), np), 2).
formula(dr(dr(dl(n, n), pp), pp_par), 2).
formula(dr(dr(dl(n, n), dl(np, s_inf)), pp_par), 2).
formula(dr(dr(dl(n, n), dl(np, s)), dr(dl(n, n), dl(np, s))), 2).
formula(dr(dr(dl(n, n), dl(n, n)), s), 2).
formula(dr(dr(dl(cl_y, s), np), np), 2).
formula(dr(dr(dl(cl_y, dl(np, s)), s_q), np), 2).
formula(dr(dr(dl(cl_y, dl(np, s)), dl(np, s_inf)), np), 2).
formula(dr(dr(dl(cl_r, s), dl(np, s_inf)), np), 2).
formula(dr(dr(dl(cl_r, dl(np, s_ppart)), s_q), np), 2).
formula(dr(dr(dl(cl_r, dl(np, s_ppart)), pp_a), np), 2).
formula(dr(dr(dl(cl_r, dl(np, s_inf)), pp_de), np), 2).
formula(dr(dr(dl(cl_r, dl(np, s)), s_q), dl(cl_r, dl(np, s))), 2).
formula(dr(dr(dl(cl_r, dl(np, s)), pp_de), np), 2).
formula(dr(dl(np, np), np), 2).
formula(dr(dl(pp_de, dl(n, n)), n), 2).
formula(dr(dl(pp, dl(n, n)), np), 2).
formula(dr(dl(pp, dl(n, n)), dr(s, pp)), 2).
formula(dr(dl(p(pp, dl(s, s)), p(pp, dl(s, s))), p(pp, dl(s, s))), 2).
formula(dr(dl(p(np, dl(n, n)), p(np, dl(n, n))), p(np, dl(n, n))), 2).
formula(dr(dl(p(dl(s, s), pp), p(dl(s, s), pp)), p(dl(s, s), pp)), 2).
formula(dr(dl(p(dl(n, n), pp), p(dl(n, n), pp)), p(dl(n, n), pp)), 2).
formula(dr(dl(np, s_ppart), pp_par), 2).
formula(dr(dl(np, dl(dl(n, n), dl(n, n))), np), 2).
formula(dr(dl(np, dl(n, n)), np), 2).
formula(dr(dl(np, dl(dr(s, np), s)), dl(np, dl(dr(s, np), s))), 2).
formula(dr(dl(n, n), dr(s_q, pp)), 2).
formula(dr(dl(dr(s, s_q), dr(s, s_q)), dr(s, s_q)), 2).
formula(dr(dl(dr(s, s), dr(s, s)), dr(s, s)), 2).
formula(dr(dl(dr(s, dl(np, s)), dr(s, dl(np, s))), dr(s, dl(np, s))), 2).
formula(dr(dl(dr(np, pp), dr(np, pp)), dr(np, pp)), 2).
formula(dr(dl(dr(np, n), dl(dr(pp_de, np), dr(dl(s, s), n))), dr(np, n)), 2).
formula(dr(dl(dr(n, n), dr(n, n)), dr(n, n)), 2).
formula(dr(dl(dr(dr(s, s), np), dr(dr(s, s), np)), dr(dr(s, s), np)), 2).
formula(dr(dl(dr(dl(s, s), n), dr(dl(s, s), n)), dr(dl(s, s), n)), 2).
formula(dr(dl(dr(dl(s, s), dl(s, s)), dr(dl(s, s), dl(s, s))), dr(dl(s, s), dl(s, s))), 2).
formula(dr(dl(dr(dl(np, s), s_q), dr(dl(np, s), s_q)), dr(dl(np, s), s_q)), 2).
formula(dr(dl(dr(dl(np, s), pp), dr(dl(np, s), pp)), dr(dl(np, s), pp)), 2).
formula(dr(dl(dr(dl(np, s), dl(np, s)), dr(dl(np, s), dl(np, s))), dr(dl(np, s), dl(np, s))), 2).
formula(dr(dl(dr(dl(n, n), s_q), dr(dl(n, n), s_q)), dr(dl(n, n), s_q)), 2).
formula(dr(dl(dr(dl(n, n), pp), dr(dl(n, n), pp)), dr(dl(n, n), pp)), 2).
formula(dr(dl(dr(dl(n, n), dl(np, s)), dr(dl(n, n), dl(np, s))), dr(dl(n, n), dl(np, s))), 2).
formula(dr(dl(dl(s, s), dl(s, s)), s_q), 2).
formula(dr(dl(dl(s, s), dl(s, s)), s), 2).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dl(dl(np, s), dl(np, s))), 2).
formula(dr(dl(dl(np, s_inf), s), pp_a), 2).
formula(dr(dl(dl(np, s), dl(s, s)), dl(np, s)), 2).
formula(dr(dl(dl(np, s), dl(np, s)), s), 2).
formula(dr(dl(dl(n, n), s), dr(s, dl(n, n))), 2).
formula(dr(dl(cl_y, dl(np, s)), dr(dl(cl_y, dl(np, s)), np)), 2).
formula(dr(dl(cl_r, dr(s, np)), dl(np, s_inf)), 2).
formula(dr(dl(cl_r, dl(s, s)), np), 2).
formula(dr(dl(cl_r, dl(np, s_ppres)), pp_par), 2).
formula(dr(dl(cl_r, dl(np, s_ppres)), dl(cl_r, dl(np, s_ppart))), 2).
formula(dr(dl(cl_r, dl(np, s_inf)), dr(dl(np, s_inf), pp_a)), 2).
formula(dr(dl(cl_r, dl(np, s)), dl(s, s)), 2).
formula(dr(dl(cl_r, dl(n, n)), pp), 2).
formula(dl(s, dl(cl_r, dl(np, s_ppart))), 2).
formula(dl(n, dl(s, s)), 2).
formula(dl(dr(s, s), s), 2).
formula(dl(dl(n, n), dl(np, s_inf)), 2).
formula(dl(dl(n, n), dl(n, n)), 2).
formula(dl(cl_r, dl(n, n)), 2).
formula(pp_de, 1).
formula(dr(s, pp_de), 1).
formula(dr(s, n), 1).
formula(dr(s, dl(np, s_ppart)), 1).
formula(dr(pp, dr(s, pp)), 1).
formula(dr(pp, dl(np, s)), 1).
formula(dr(pp, dl(n, n)), 1).
formula(dr(np, pp_a), 1).
formula(dr(np, dr(n, n)), 1).
formula(dr(n, dl(n, n)), 1).
formula(dr(dr(s_whq, dr(s, pp_a)), pp_de), 1).
formula(dr(dr(s_whq, dl(np, s_inf)), n), 1).
formula(dr(dr(s_ppres, dl(np, s_inf)), np), 1).
formula(dr(dr(s, s_whq), np), 1).
formula(dr(dr(s, s), pp_par), 1).
formula(dr(dr(s, pp), clr), 1).
formula(dr(dr(s, dr(s, pp)), np), 1).
formula(dr(dr(s, dl(s, s)), np), 1).
formula(dr(dr(s, dl(np, s_inf)), dl(np, s_ppart)), 1).
formula(dr(dr(s, dl(np, s_inf)), cl_r), 1).
formula(dr(dr(pp_a, np), n), 1).
formula(dr(dr(pp, pp), dl(s, s)), 1).
formula(dr(dr(p(dl(n, n), np), s_q), p(dl(n, n), np)), 1).
formula(dr(dr(np, s_q), pp), 1).
formula(dr(dr(np, s_q), n), 1).
formula(dr(dr(np, np), pp_de), 1).
formula(dr(dr(np, np), pp), 1).
formula(dr(dr(np, np), dl(s, s)), 1).
formula(dr(dr(np, np), dl(np, s_ppres)), 1).
formula(dr(dr(np, n), np), 1).
formula(dr(dr(np, n), dr(np, n)), 1).
formula(dr(dr(n, s_q), pp), 1).
formula(dr(dr(dr(s, s_q), s), n), 1).
formula(dr(dr(dr(s, s_q), dl(np, s_inf)), np), 1).
formula(dr(dr(dr(s, s_q), dl(n, n)), np), 1).
formula(dr(dr(dr(s, s), pp_par), np), 1).
formula(dr(dr(dr(s, pp_a), dl(np, s_inf)), pp_a), 1).
formula(dr(dr(dr(s, dl(np, s)), np), np), 1).
formula(dr(dr(dr(s, dl(np, s)), np), dr(dr(s, dl(np, s)), np)), 1).
formula(dr(dr(dr(np, s_q), np), dl(s, s)), 1).
formula(dr(dr(dr(n, n), dr(n, n)), n), 1).
formula(dr(dr(dr(dl(np, s_ppres), dl(np, s_inf)), pp_a), np), 1).
formula(dr(dr(dr(dl(np, s_ppart), np), pp_a), dl(np, s_inf)), 1).
formula(dr(dr(dr(dl(np, s_ppart), dl(np, s_inf)), pp_a), dl(n, n)), 1).
formula(dr(dr(dr(dl(np, s_inf), pp_par), pp_de), np), 1).
formula(dr(dr(dr(dl(np, s_inf), pp_a), np), pp), 1).
formula(dr(dr(dr(dl(np, s_inf), pp_a), dl(n, n)), np), 1).
formula(dr(dr(dr(dl(np, s_inf), dl(np, s_inf)), pp_par), np), 1).
formula(dr(dr(dr(dl(np, s), s_q), pp_a), np), 1).
formula(dr(dr(dr(dl(np, s), pp), s_q), dr(dl(np, s), pp)), 1).
formula(dr(dr(dl(s, s), dl(s, s)), s_q), 1).
formula(dr(dr(dl(s, s), dl(s, s)), s), 1).
formula(dr(dr(dl(s, s), dl(s, s)), dr(dl(s, s), dl(s, s))), 1).
formula(dr(dr(dl(s, s), dl(s, s)), dl(np, s_inf)), 1).
formula(dr(dr(dl(dl(n, n), dl(n, n)), dl(n, n)), np), 1).
formula(dr(dr(dl(np, s_ppres), pp_a), dl(np, s_inf)), 1).
formula(dr(dr(dl(np, s_ppres), pp_a), dl(n, n)), 1).
formula(dr(dr(dl(np, s_ppres), np), pp_a), 1).
formula(dr(dr(dl(np, s_ppres), np), np), 1).
formula(dr(dr(dl(np, s_ppres), dl(np, s_ppart)), np), 1).
formula(dr(dr(dl(np, s_ppart), s_whq), pp_a), 1).
formula(dr(dr(dl(np, s_ppart), pp_par), dl(n, n)), 1).
formula(dr(dr(dl(np, s_ppart), pp_a), pp_de), 1).
formula(dr(dr(dl(np, s_ppart), pp_a), dl(np, s_inf)), 1).
formula(dr(dr(dl(np, s_ppart), pp), pp_de), 1).
formula(dr(dr(dl(np, s_ppart), np), pp_par), 1).
formula(dr(dr(dl(np, s_ppart), dl(np, s_inf)), pp_de), 1).
formula(dr(dr(dl(np, s_pass), pp_de), pp_par), 1).
formula(dr(dr(dl(np, s_pass), np), pp_par), 1).
formula(dr(dr(dl(np, s_inf), pp_de), pp_a), 1).
formula(dr(dr(dl(np, s_inf), pp_a), pp_de), 1).
formula(dr(dr(dl(np, s_inf), pp_a), pp), 1).
formula(dr(dr(dl(np, s_inf), pp_a), dl(n, n)), 1).
formula(dr(dr(dl(np, s_inf), pp), pp), 1).
formula(dr(dr(dl(np, s_inf), dl(np, s_inf)), pp), 1).
formula(dr(dr(dl(np, s), pp_par), pp_de), 1).
formula(dr(dr(dl(np, s), pp_de), dl(n, n)), 1).
formula(dr(dr(dl(np, s), pp_a), s_q), 1).
formula(dr(dr(dl(np, s), dl(np, s_inf)), dl(np, s)), 1).
formula(dr(dr(dl(np, s), dl(n, n)), pp_a), 1).
formula(dr(dr(dl(np, np), pp_par), np), 1).
formula(dr(dr(dl(np, np), dl(np, s)), np), 1).
formula(dr(dr(dl(np, np), dl(np, np)), n), 1).
formula(dr(dr(dl(np, dr(s, s)), pp_a), pp_par), 1).
formula(dr(dr(dl(n, n), s_q), pp_de), 1).
formula(dr(dr(dl(n, n), s_q), pp_a), 1).
formula(dr(dr(dl(n, n), s_q), np), 1).
formula(dr(dr(dl(n, n), pp), np), 1).
formula(dr(dr(dl(n, n), np), dl(np, s_inf)), 1).
formula(dr(dr(dl(n, n), dl(n, n)), pp_par), 1).
formula(dr(dr(dl(n, n), dl(n, n)), pp_de), 1).
formula(dr(dr(dl(n, n), dl(n, n)), dl(np, s_inf)), 1).
formula(dr(dr(dl(n, n), dl(n, n)), dl(n, n)), 1).
formula(dr(dr(dl(dr(pp, n), s_whq), s), n), 1).
formula(dr(dr(dl(dl(np, s_inf), s), pp_a), np), 1).
formula(dr(dr(dl(dl(np, s_inf), s), pp_a), dl(n, n)), 1).
formula(dr(dr(dl(cl_y, dl(np, s)), dl(np, s_inf)), dl(n, n)), 1).
formula(dr(dr(dl(cl_r, s), pp_de), np), 1).
formula(dr(dr(dl(cl_r, s), pp_a), s_q), 1).
formula(dr(dr(dl(cl_r, s), dl(cl_r, dl(np, s_ppart))), np), 1).
formula(dr(dr(dl(cl_r, dl(np, s_ppres)), s_q), np), 1).
formula(dr(dr(dl(cl_r, dl(np, s_ppart)), pp_par), dl(np, s_inf)), 1).
formula(dr(dr(dl(cl_r, dl(np, s_ppart)), pp_de), np), 1).
formula(dr(dr(dl(cl_r, dl(np, s_inf)), s_q), np), 1).
formula(dr(dr(dl(cl_r, dl(np, s)), dl(np, s_inf)), np), 1).
formula(dr(dr(dl(cl_r, dl(np, s)), dl(cl_r, dl(np, s))), n), 1).
formula(dr(dl(s, s), dr(n, n)), 1).
formula(dr(dl(s, s), dl(np, s_ppart)), 1).
formula(dr(dl(dl(np, s), dl(np, s)), pp_a), 1).
formula(dr(dl(dl(np, s), dl(np, s)), n), 1).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s)), 1).
formula(dr(dl(dl(np, np), dl(np, np)), dl(np, s_inf)), 1).
formula(dr(dl(dl(n, n), dl(n, n)), dl(np, s_pass)), 1).
formula(dr(dl(dl(n, n), dl(n, n)), dl(n, n)), 1).
formula(dr(dl(s, s), pp), 1).
formula(dr(dl(pp_de, dr(s, s)), n), 1).
formula(dr(dl(pp, dr(s, dr(s, pp))), pp), 1).
formula(dr(dl(pp, dl(s, s)), pp), 1).
formula(dr(dl(pp, dl(s, s)), dr(s, pp)), 1).
formula(dr(dl(p(pp, dl(dl(n, n), dl(n, n))), p(pp, dl(dl(n, n), dl(n, n)))), p(pp, dl(dl(n, n), dl(n, n)))), 1).
formula(dr(dl(p(p(pp, np), dl(s, s)), p(p(pp, np), dl(s, s))), p(pp, dl(s, s))), 1).
formula(dr(dl(p(n, pp), p(n, pp)), p(n, pp)), 1).
formula(dr(dl(p(dl(np, s), np), p(dl(np, s), np)), p(dl(np, s), np)), 1).
formula(dr(dl(np, pp_de), np), 1).
formula(dr(dl(np, dr(s, s)), dl(np, dr(s, s))), 1).
formula(dr(dl(np, dl(s, s)), dl(np, dl(s, s))), 1).
formula(dr(dl(np, dl(s, s)), dl(n, n)), 1).
formula(dr(dl(np, dl(np, np)), pp), 1).
formula(dr(dl(np, dl(np, np)), dl(np, s)), 1).
formula(dr(dl(np, dl(n, n)), pp), 1).
formula(dr(dl(np, dl(n, n)), dl(np, dl(n, n))), 1).
formula(dr(dl(np, dl(dr(s, s), dr(s, s))), dr(s, s)), 1).
formula(dr(dl(n, pp_a), n), 1).
formula(dr(dl(n, n), dr(s, s)), 1).
formula(dr(dl(n, n), dl(s, s)), 1).
formula(dr(dl(n, dr(s, s)), n), 1).
formula(dr(dl(n, dl(n, n)), n), 1).
formula(dr(dl(dr(s, s), np), np), 1).
formula(dr(dl(dr(s, s), dr(s, s)), s), 1).
formula(dr(dl(dr(s, s), dr(s, s)), dr(dr(s, dl(np, s)), np)), 1).
formula(dr(dl(dr(s, np), dr(s, np)), dl(np, s_inf)), 1).
formula(dr(dl(dr(s, dr(s, pp_a)), dr(s, dr(s, pp_a))), dr(s, dr(s, pp_a))), 1).
formula(dr(dl(dr(s, dl(np, s)), dr(s, dl(np, s))), dr(s, dl(np, s))), 1).
formula(dr(dl(dr(s, dr(s, np)), dr(s, dr(s, np))), dr(s, dr(s, np))), 1).
formula(dr(dl(dr(s, dl(np, s)), dr(s, dl(np, s))), dr(s, dl(np, s))), 1).
formula(dr(dl(dr(s, np), np), n), 1).
formula(dr(dl(dr(pp, pp_de), dl(n, n)), s), 1).
formula(dr(dl(dr(pp, pp_de), dl(n, n)), dr(s, pp)), 1).
formula(dr(dl(dr(pp, np), s_whq), pp_de), 1).
formula(dr(dl(dr(pp, np), s_whq), dl(np, s_inf)), 1).
formula(dr(dl(dr(pp, np), dr(pp, np)), dr(pp, np)), 1).
formula(dr(dl(dr(pp, np), dl(s, s)), dl(s, s)), 1).
formula(dr(dl(dr(pp, np), dl(np, np)), np), 1).
formula(dr(dl(dr(pp, n), s_whq), s), 1).
formula(dr(dl(dr(pp, n), s), s), 1).
formula(dr(dl(dr(pp, n), dr(pp, n)), dr(pp, n)), 1).
formula(dr(dl(dr(n, n), n), n), 1).
formula(dr(dl(dr(dr(np, np), n), dr(dr(np, np), n)), dr(dr(np, np), n)), 1).
formula(dr(dl(dr(dr(dr(s, s), dr(s, s)), n), dr(dr(dr(s, s), dr(s, s)), n)), dr(dr(dr(s, s), dr(s, s)), n)), 1).
formula(dr(dl(dr(dr(dl(s, s), s_q), dl(s, s)), dr(dr(dl(s, s), s_q), dl(s, s))), dr(dr(dl(s, s), s_q), dl(s, s))), 1).
formula(dr(dl(dr(dr(dl(np, s), dl(np, s)), np), dr(dr(dl(np, s), dl(np, s)), np)), dr(dr(dl(np, s), dl(np, s)), np)), 1).
formula(dr(dl(dr(dl(s, s), s_q), dr(dl(s, s), s_q)), dr(dl(s, s), s_q)), 1).
formula(dr(dl(dr(dl(s, s), np), dr(dl(s, s), np)), dr(dl(s, s), np)), 1).
formula(dr(dl(dr(dl(s, s), np), dr(dl(s, s), np)), dr(dl(s, s), np)), 1).
formula(dr(dl(dr(dl(s, s), n), dl(n, n)), s), 1).
formula(dr(dl(dr(dl(n, n), dl(np, s)), dr(dl(n, n), dl(np, s))), dr(dl(n, n), dl(np, s))), 1).
formula(dr(dl(dr(dl(n, n), np), dr(dl(n, n), np)), dr(dl(n, n), np)), 1).
formula(dr(dl(dr(dl(dl(s, s), dl(s, s)), dl(s, s)), dr(dl(dl(s, s), dl(s, s)), dl(s, s))), dr(dl(dl(s, s), dl(s, s)), dl(s, s))), 1).
formula(dr(dl(dl(s, s), dl(s, s)), np), 1).
formula(dr(dl(dl(s, s), dl(s, s)), n), 1).
formula(dr(dl(dl(s, s), dl(s, s)), dl(np, s)), 1).
formula(dr(dl(dl(s, s), dl(s, s)), dl(dl(np, s), dl(np, s))), 1).
formula(dr(dl(dl(np, s_inf), s), pp_de), 1).
formula(dr(dl(dl(np, s_inf), s), dl(np, s_ppart)), 1).
formula(dr(dl(dl(np, s), s), dr(dl(dl(np, s), s), pp_a)), 1).
formula(dr(dl(dl(np, s), np), n), 1).
formula(dr(dl(dl(np, s), dl(np, s)), dl(n, n)), 1).
formula(dr(dl(dl(n, n), s_q), dr(s, dl(n, n))), 1).
formula(dr(dl(dl(n, n), dl(np, np)), dr(s, pp)), 1).
formula(dr(dl(dl(n, n), dl(np, np)), dr(s, dl(n, n))), 1).
formula(dr(dl(dl(n, n), dl(n, n)), s), 1).
formula(dr(dl(dl(n, n), dl(n, n)), n), 1).
formula(dr(dl(dl(n, n), dl(n, n)), dl(np, s)), 1).
formula(dr(dl(dl(dl(np, s), s), dl(dl(np, s), s)), dl(dl(np, s), s)), 1).
formula(dr(dl(dl(n, n), np), np), 1).
formula(dr(dl(cl_y, s), dr(s, s)), 1).
formula(dr(dl(cl_y, dl(np, s)), dl(n, n)), 1).
formula(dr(dl(cl_y, dl(np, dl(dl(np, np), dl(np, np)))), np), 1).
formula(dr(dl(cl_y, dl(n, n)), np), 1).
formula(dr(dl(cl_r, s), dr(dl(cl_r, s), pp_de)), 1).
formula(dr(dl(cl_r, s), dl(cl_r, s)), 1).
formula(dr(dl(cl_r, s), dl(cl_r, dl(np, s_ppart))), 1).
formula(dr(dl(cl_r, dr(s, s)), pp_de), 1).
formula(dr(dl(cl_r, dl(np, s_ppres)), s_q), 1).
formula(dr(dl(cl_r, dl(np, s_ppres)), np), 1).
formula(dr(dl(cl_r, dl(np, s_inf)), dr(dl(np, s_inf), pp_de)), 1).
formula(dr(dl(cl_r, dl(np, s)), s), 1).
formula(dr(dl(cl_r, dl(np, s)), dl(cl_r, dl(np, s_inf))), 1).
formula(dr(dl(cl_r, dl(n, n)), pp_de), 1).
formula(dr(dl(cl_r, dl(dl(np, s_inf), s)), dl(np, s_inf)), 1).
formula(dr(dl(cl_r, dl(dl(n, n), dl(n, n))), pp_de), 1).
formula(dl(np, dl(np, s_inf)), 1).
formula(dl(np, dl(np, s)), 1).
formula(dl(np, dl(np, np)), 1).
formula(dl(dr(pp, np), s_whq), 1).
formula(dl(dr(pp, np), np), 1).
formula(dl(dr(pp, n), s_whq), 1).
formula(dl(dr(n, n), dr(n, n)), 1).
formula(dl(dr(dl(np, s), np), s_whq), 1).
formula(dl(dl(np, s_inf), s), 1).
formula(dl(dl(np, s), np), 1).
formula(dl(dl(np, s), dl(s, s)), 1).
formula(dl(cl_r, dl(s, s)), 1).
formula(dl(cl_r, dl(np, dr(n, n))), 1).