formula(n, 242072).
formula(dr(n, n), 169708).
formula(dr(np(nb), n), 97267).
formula('.', 57590).
formula(dr(dl(np, np), np), 49750).
formula(',', 48844).
formula(dr(dl(dl(np, s), dl(np, s)), np), 23549).
formula(dr(dl(np, s(dcl)), np), 23525).
formula(np, 21669).
formula(dr(pp, np), 20699).
formula(conj, 20660).
formula(dl(dl(np, s), dl(np, s)), 16326).
formula(dr(dl(np, s(b)), np), 14635).
formula(dr(dl(np, s(to)), dl(np, s(b))), 13356).
formula(dr(dl(np, s(dcl)), dl(np, s(b))), 10822).
formula(dl(np, dr(np(nb), n)), 9674).
formula(dl(np, s(adj)), 8674).
formula(n(num), 8547).
formula(dl(np, s(pss)), 7278).
formula(dr(n, n(num)), 6992).
formula(dr(s(wq), dl(np, s(dcl))), 6080).
formula(dr(dl(np, s), dl(np, s)), 6063).
formula(dr(dr(n, n), dr(n, n)), 6030).
formula(dr(dl(np, s(ng)), np), 5968).
formula(dl(np, s(dcl)), 5674).
formula(dr(dl(np, s(dcl)), s(dcl)), 5627).
formula(dr(dl(np, s(dcl)), dl(np, s(pt))), 5472).
formula(dr(dl(np, np), dl(np, s(dcl))), 5355).
formula(dr(s, s), 5292).
formula(dr(dl(np, s(dcl)), dl(np, s(pss))), 4987).
formula(dr(dr(s, s), np), 4826).
formula(dr(dl(np, s(dcl)), dl(np, s(adj))), 4684).
formula(dr(dl(np, s(pss)), pp), 4532).
formula(dr(s(em), s(dcl)), 4290).
formula(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), 3830).
formula(dr(dr(s(q), dl(np, s(b))), np), 3632).
formula(dr(dl(np, s(dcl)), dl(np, s(ng))), 3503).
formula(dr(s(wq), dr(s(q), np)), 3455).
formula(dr(dl(np, s(dcl)), pp), 3388).
formula(dr(dl(dl(np, s), dl(np, s)), s(dcl)), 3261).
formula(dr(dl(np, s(b)), pp), 3002).
formula(dl(np, s(b)), 2882).
formula(dr(dl(np, s(dcl)), dl(np, s(to))), 2753).
formula(dr(dl(np, s(pt)), np), 2540).
formula(dl(np, np), 2527).
formula(dr(dr(s(wq), dr(s(q), np)), n), 2411).
formula(dr(dl(np, s(adj)), dl(np, s(adj))), 2362).
formula(dr(dr(s(wq), dl(np, s(dcl))), n), 2353).
formula(dr(dr(s(q), np), np), 2341).
formula(dr(dl(np, s(dcl)), s(em)), 2303).
formula(dr(np, np), 2266).
formula(dr(s(wq), dr(s(q), pp)), 2180).
formula(dr(dr(s(q), dl(np, s(pss))), np), 2152).
formula(dr(dr(dl(np, s(b)), pp), np), 2054).
formula(dr(dr(s, s), s(dcl)), 1915).
formula(:, 1864).
formula(dr(dl(np, s(b)), dl(np, s(pss))), 1845).
formula(dl(np, dl(s(dcl), s(dcl))), 1816).
formula(dr(dl(np, s(adj)), pp), 1770).
formula(dr(dl(np, np), dl(np, np)), 1704).
formula(dr(dr(dl(np, s(dcl)), pp), np), 1698).
formula(dl(np, s(ng)), 1671).
formula(dr(dl(np, np), n), 1628).
formula(dr(dl(s(dcl), s(dcl)), np), 1546).
formula(dr(dl(dl(np, s), dl(np, s)), pp), 1460).
formula(rrb, 1433).
formula(dr(dl(np, s(b)), dl(np, s(adj))), 1379).
formula(dr(dr(s(q), pp), np), 1163).
formula(dl(n, n), 1148).
formula(dr(dl(np, s(ng)), pp), 1140).
formula(dr(dl(np, s(pss)), dl(np, s(to))), 1120).
formula(;, 1096).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s(ng))), 1017).
formula(dr(dl(np, s(pss)), np), 1005).
formula(dr(dr(n, n), n(num)), 927).
formula(dr(dl(np, np), s(dcl)), 910).
formula(dr(dl(np, s(adj)), dl(np, s(to))), 880).
formula(dr(pp, dl(np, s(ng))), 878).
formula(dr(dl(np, np), dl(np, s(ng))), 872).
formula(np(thr), 864).
formula(rqu, 850).
formula(lqu, 850).
formula(dr(dl(dl(np, s(adj)), dl(np, s(adj))), np), 849).
formula(dr(dl(n, n), np), 795).
formula(dr(dl(np, s(ng)), dl(np, s(to))), 775).
formula(dl(np, s(pt)), 771).
formula(dr(dr(s, s), dr(s, s)), 771).
formula(dr(dl(dl(np, s), dl(np, s)), n), 763).
formula(dr(dl(np, s(b)), dl(np, s(to))), 747).
formula(dr(dr(dl(np, s(ng)), pp), np), 705).
formula(dr(dl(np(thr), s(dcl)), np), 688).
formula(dr(dr(dl(np, s(dcl)), dl(np, s(to))), np), 686).
formula(dr(dl(np, s(pt)), dl(np, s(pss))), 668).
formula(np(expl), 601).
formula(dr(dr(s(wq), dr(s(q), pp)), n), 600).
formula(dr(s(qem), s(dcl)), 594).
formula(dr(dr(dl(np, s), dl(np, s)), np), 582).
formula(dr(n, s(em)), 562).
formula(lrb, 535).
formula(dr(dl(np, np), dr(s(dcl), np)), 534).
formula(dr(dl(np, s(adj)), np), 506).
formula(dr(pp, pp), 504).
formula(dr(dr(s(wq), dr(s(q), dl(np, s(adj)))), dl(np, s(adj))), 500).
formula(dr(dl(np, s(pt)), pp), 488).
formula(dr(dl(np, s(b)), dl(np, s(pt))), 463).
formula(dr(dr(s(q), dl(np, s(adj))), np), 457).
formula(dr(dl(np, s(b)), dl(np, s(ng))), 448).
formula(dr(dl(dl(np, s), dl(np, s)), n(num)), 430).
formula(dr(dr(dl(np, s(b)), dl(np, s(to))), np), 420).
formula(dr(dl(np, np), pp), 405).
formula(dr(dr(dl(np, s(dcl)), np), np), 393).
formula(dr(dr(dl(np, s(b)), np), np), 383).
formula(dr(dl(np, s(pt)), dl(np, s(ng))), 378).
formula(dr(np, n), 370).
formula(dr(dr(s, s), pp), 364).
formula(dr(dl(np, s(ng)), dl(np, s(pss))), 358).
formula(dr(dl(np, s(pt)), dl(np, s(adj))), 353).
formula(dl(np, dl(np, s(adj))), 340).
formula(dr(np, dr(s(dcl), np)), 339).
formula(dr(conj, conj), 332).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), np), 325).
formula(dr(dr(dl(np, s(pt)), pp), np), 322).
formula(dr(dl(s, s), s(dcl)), 320).
formula(dr(dl(np, s(pt)), dl(np, s(to))), 308).
formula(dl(np, s(asup)), 296).
formula(dl(dl(np, s(adj)), dr(dr(n, n), dr(n, n))), 296).
formula(dl(dr(dl(np, np), np), dr(dl(np, np), s(dcl))), 284).
formula(dr(dr(dl(np, s), dl(np, s)), dr(dl(np, s), dl(np, s))), 276).
formula(dr(dl(np, s(b)), s(em)), 273).
formula(dr(dl(np, s(b)), s(dcl)), 258).
formula(dr(s(wq), s(q)), 257).
formula(dr(dr(n, n), n), 254).
formula(dr(dl(np, s(ng)), s(em)), 252).
formula(dr(dl(np, s(pss)), dl(np, s(adj))), 245).
formula(dr(dl(np, s(b)), s(qem)), 243).
formula(dr(dr(dl(np, s(dcl)), dl(np, s(adj))), np), 240).
formula(dr(dr(dl(np, s(b)), dl(np, s(adj))), np), 237).
formula(dl(np, dl(dl(np, s), dl(np, s))), 235).
formula(dr(dl(np, s(ng)), dl(np, s(adj))), 232).
formula(dl(s, s), 222).
formula(dr(dr(dl(np, s(ng)), dl(np, s(to))), np), 212).
formula(dr(dl(n, n), n), 211).
formula(dr(dr(s(wq), dr(s(q), pp)), dr(s(wq), dr(s(q), np))), 210).
formula(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), 207).
formula(dl(dl(np, s(adj)), dl(np, s(adj))), 205).
formula(dr(dr(dr(s(wq), dr(s(q), np)), n), dr(np, n)), 200).
formula(dr(dr(s(for), dl(np, s(to))), np), 196).
formula(dr(dr(s, s), n), 196).
formula(dr(dr(s, s), dl(np, s(ng))), 196).
formula(dr(dr(dr(n, n), dr(n, n)), dr(dr(n, n), dr(n, n))), 183).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s(adj))), 182).
formula(dr(np, dl(np, s(dcl))), 177).
formula(dl(dl(np, s(adj)), dr(n, n)), 175).
formula(dr(dl(np, s(dcl)), s(qem)), 174).
formula(dl(dr(n, n), dr(n, n)), 173).
formula(dr(dr(dl(np, s(b)), dl(np, s(b))), np), 172).
formula(dr(dl(np, s(ng)), s(dcl)), 171).
formula(dr(dr(dl(np, np), dl(np, s(dcl))), n), 158).
formula(dl(np, dr(s, s)), 152).
formula(dr(dl(np, s(pt)), s(em)), 151).
formula(dr(dl(dl(np, np), dl(np, np)), np), 146).
formula(dr(dl(dr(n, n), dr(n, n)), np), 145).
formula(dr(pp, dl(np, s(adj))), 144).
formula(dr(dl(s, s), np), 144).
formula(dr(dl(np, s(b)), dl(np, s(b))), 142).
formula(dl(np, dl(np, np)), 137).
formula(dr(dr(dl(np, s(adj)), dl(np, s(adj))), dr(dl(np, s(adj)), dl(np, s(adj)))), 133).
formula(dr(dr(n, pp), dl(np, s(adj))), 132).
formula(dr(dr(dl(np(expl), s(dcl)), dl(np, s(to))), dl(np, s(adj))), 132).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s)))), 128).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), np), 127).
formula(dl(dl(np, np), dl(np, np)), 126).
formula(dr(dr(np, np), dr(np, np)), 126).
formula(dr(dl(np, np), n(num)), 125).
formula(dr(dr(dl(np, s(b)), pp), pp), 125).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s(dcl))), 124).
formula(dl(np, dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s)))), 122).
formula(dr(dl(np, s(pt)), s(dcl)), 120).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(np, s(ng))), np), 118).
formula(dr(dr(s(q), dl(np, s(pt))), np), 116).
formula(dr(dr(dr(n, n), dr(n, n)), dl(np, s(asup))), 116).
formula(dr(dr(dl(np, s(dcl)), dl(np, s(b))), np), 115).
formula(dr(dl(np, np), dl(np, s(adj))), 112).
formula(dr(dr(dl(np, s(dcl)), dl(np, s(ng))), np), 109).
formula(dr(dl(dr(n, n), dr(n, n)), dr(n, n)), 107).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), s(dcl)), 104).
formula(dr(dl(np, s(adj)), s(em)), 103).
formula(dr(dr(dl(np, s(pt)), dl(np, s(to))), np), 103).
formula(dr(dl(np, np), s(qem)), 102).
formula(dr(dr(dl(np, s(dcl)), s(em)), np), 102).
formula(dr(dl(dl(np, s(adj)), dl(np, s(adj))), s(dcl)), 102).
formula(dr(dr(dl(np, s(ng)), dl(np, s(adj))), np), 101).
formula(dr(dr(s(wq), dr(s(q), np)), np), 100).
formula(dl(dr(s(wq), dl(np, s(dcl))), dr(dr(s(wq), dl(np, s(dcl))), n)), 100).
formula(dr(dr(dr(dr(s(wq), pp), dr(dr(s(q), pp), np)), n), dr(np, n)), 100).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s(b))), 99).
formula(dr(dr(dl(np, s(ng)), np), np), 99).
formula(dr(s, s(dcl)), 94).
formula(dr(dr(dl(np, s(dcl)), np), dl(np, s(dcl))), 92).
formula(dr(dl(np, s(pss)), s(em)), 85).
formula(dr(pp, s(qem)), 83).
formula(dr(dl(np, s(adj)), s(dcl)), 82).
formula(dr(dl(s(wq), s(wq)), s(dcl)), 80).
formula(dr(dl(s(wq), s(wq)), np), 80).
formula(dr(dr(s, s), dl(np, s(adj))), 80).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), n), 79).
formula(dr(dl(np(thr), s(dcl)), dl(np, s(b))), 78).
formula(dr(dl(pp, pp), np), 77).
formula(dr(dl(np, np), dl(np, s(pss))), 77).
formula(dr(dr(dl(np, s(pss)), dl(np, s(to))), pp), 76).
formula(dr(s(qem), dl(np, s(to))), 75).
formula(dr(dr(dl(np(expl), s(dcl)), s(em)), dl(np, s(adj))), 75).
formula(dr(dr(dr(dl(np, s(b)), pp), pp), np), 74).
formula(dr(dl(dl(np, np), dl(np, np)), dl(dl(np, np), dl(np, np))), 73).
formula(dl(pp, pp), 71).
formula(dl(np, dl(pp, pp)), 71).
formula(dr(dl(dr(s(dcl), np), s(wq)), n), 70).
formula(dr(dr(dl(np, s(dcl)), pp), dl(np, s(adj))), 70).
formula(dr(dl(pp, s(dcl)), np), 68).
formula(dr(dr(dl(np, s(b)), dl(np, s(ng))), np), 68).
formula(dr(dl(np(expl), s(dcl)), dl(np, s(b))), 67).
formula(dr(dl(dl(np, s(adj)), s(dcl)), np), 65).
formula(dr(s(bem), s(b)), 62).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s(pss))), 62).
formula(dr(dr(dl(np, s(pss)), pp), pp), 62).
formula(dl(dr(np, np), dr(dl(np, np), dl(np, s(dcl)))), 62).
formula(dr(dl(np, s(adj)), dr(dl(np, s(to)), np)), 61).
formula(dr(dr(dl(np, s), dl(np, s)), n), 61).
formula(dr(np, pp), 60).
formula(dr(dr(dl(np, np), dl(np, np)), np), 60).
formula(dr(dl(dr(dl(np, np), dl(np, np)), dr(dl(np, np), dl(np, np))), dr(dl(np, np), dl(np, np))), 60).
formula(dr(dr(dl(dl(np, s), dl(np, s)), pp), np), 57).
formula(dr(dr(dl(np, s), dl(np, s)), s(dcl)), 56).
formula(dr(dr(dl(np, s(dcl)), s(dcl)), np), 56).
formula(dr(dr(dl(np, s(adj)), pp), np), 55).
formula(dr(dr(dl(np, np), pp), np), 55).
formula(dr(n, s(dcl)), 54).
formula(dr(s(poss), s(dcl)), 53).
formula(dr(dr(dl(np, s(pt)), np), np), 53).
formula(dr(dl(np, s(ng)), dl(np, s(pt))), 52).
formula(dr(dr(pp, pp), np), 52).
formula(dr(dr(dl(np, s), dl(np, s)), pp), 52).
formula(dr(dr(dl(np, s(adj)), s(em)), dl(np, s(adj))), 52).
formula(dr(s(inv), np), 50).
formula(dr(dl(np, s(ng)), s(qem)), 50).
formula(dr(dl(np(thr), s(dcl)), dl(np, s(pt))), 50).
formula(dr(dr(dr(s(wq), pp), dr(dr(s(q), pp), dl(np, s(adj)))), dl(np, s(adj))), 50).
formula(dr(dr(dr(s(q), pp), dl(np, s(adj))), np), 50).
formula(dr(dr(dl(np, s(dcl)), pp), pp), 50).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s)))), 49).
formula(dr(dr(dl(np, s(ng)), dl(np, s(b))), np), 48).
formula(dr(dr(s(qem), s(dcl)), dl(np, s(adj))), 47).
formula(dr(dl(np, s(dcl)), s(for)), 45).
formula(dr(dr(dr(s, s), dl(np, s(ng))), np), 45).
formula(dr(dr(dl(np, s(dcl)), np), pp), 44).
formula(dr(dl(np, pp), np), 43).
formula(dr(dl(np, np), dl(np, s(b))), 43).
formula(dr(dl(dl(np, s(adj)), dl(np, s(adj))), pp), 43).
formula(dr(dr(s, s), dl(np, s(pss))), 42).
formula(dr(dl(pp, pp), dl(pp, pp)), 42).
formula(dr(dr(dl(np, s(b)), np), dl(np, s(adj))), 42).
formula(dr(dr(s(dcl), s(dcl)), np), 41).
formula(dr(dl(np, dl(dl(np, s), dl(np, s))), np), 41).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(np, s(to))), n), 41).
formula(dr(s(dcl), np), 40).
formula(dr(dr(s(wq), dl(np, s(dcl))), np), 40).
formula(dr(dr(s(qem), dr(s(dcl), np)), n), 40).
formula(dr(dl(np, s(dcl)), dl(np, s(dcl))), 40).
formula(dr(dr(pp, dl(np, s(ng))), np), 40).
formula(dr(dr(dr(s(q), pp), np), np), 40).
formula(dl(conj, conj), 38).
formula(dr(dr(n, n), dl(np, s(asup))), 38).
formula(dr(n, pp), 37).
formula(dr(dl(dl(np, s), dl(np, s)), s(em)), 37).
formula(dr(dr(dl(np, np), dl(np, s(ng))), np), 37).
formula(dr(s(em), s(b)), 36).
formula(dr(dr(np, np), np), 35).
formula(dr(dr(dl(np, s(pt)), dl(np, s(adj))), np), 35).
formula(dr(dr(dl(np(expl), s(dcl)), dl(np, np)), np), 35).
formula(dr(dl(dl(np, s(adj)), dl(np, s(adj))), dl(np, s(adj))), 35).
formula(dr(dl(np, s(dcl)), s), 34).
formula(dr(s(qem), dl(np, s(dcl))), 33).
formula(dl(dr(s, s), dr(s, s)), 33).
formula(dr(dr(np, np), dl(np, s(asup))), 33).
formula(dr(dr(n, n), np), 33).
formula(dr(dl(dl(np, s), dl(np, s)), dl(np, s(to))), 33).
formula(dr(dr(dl(np, s(adj)), dl(np, s(to))), dl(np, s(adj))), 33).
formula(dr(dl(np, s(ng)), dl(np, s(ng))), 32).
formula(dr(dr(dl(np(expl), s(dcl)), s(qem)), dl(np, s(adj))), 32).
formula(dr(dl(dl(np, s(adj)), dl(np, s(adj))), dl(dl(np, s(adj)), dl(np, s(adj)))), 32).
formula(dr(dl(np, dl(dl(np, s), dl(np, s))), s(dcl)), 32).
formula(dr(dr(dr(dl(np, s(dcl)), pp), pp), np), 32).
formula(dr(dl(np, s(pss)), dr(pp, np)), 31).
formula(dr(dl(dl(np, s(ng)), s(dcl)), np), 31).
formula(dr(dl(dl(np, s), dl(np, s)), s(poss)), 31).
formula(dr(dl(dl(np, s), dl(np, s)), s), 31).
formula(dr(dr(dl(np, s(dcl)), np), dl(np, s(adj))), 31).
formula(dr(dr(dl(np, s(b)), np), pp), 31).
formula(dl(s(wq), s(wq)), 30).
formula(dr(dl(s, s), dl(s, s)), 30).
formula(dr(dr(dl(np(expl), s(dcl)), dl(np, s(to))), np), 30).
formula(dr(dr(dl(np, s(b)), pp), dl(np, s(adj))), 30).
formula(dl(dl(np, s(adj)), dr(dr(np, np), dr(np, np))), 30).
formula(s(intj), 29).
formula(dr(dr(s(qem), dr(s(dcl), dl(np, s(adj)))), dl(np, s(adj))), 29).
formula(dr(dr(s(q), dl(np, s(ng))), np), 29).
formula(dl(dl(np, s(adj)), dr(dl(np, s), dl(np, s))), 29).
formula(dr(dr(dl(np, s), dl(np, s)), dl(np, s(adj))), 29).
formula(dr(dl(dl(np, s(adj)), dl(np, s(adj))), dl(np, s(ng))), 29).
formula(dr(dl(np, s(adj)), dl(np, s(ng))), 28).
formula(dr(dr(dl(np, s), dl(np, s)), dl(np, s(ng))), 28).
formula(dl(np, s(to)), 26).
formula(dr(dr(s, s), dl(np, s(dcl))), 26).
formula(dr(dl(np, dl(s(dcl), s(dcl))), np), 26).
formula(dr(dr(dl(np, np), dl(np, s(to))), np), 26).
formula(dr(dr(n, n), dl(np, s(adj))), 25).
formula(dr(dl(dl(np, s), dl(np, s)), s(qem)), 25).
formula(dr(dl(dl(np, s), dl(np, s)), dr(s(dcl), np)), 25).
formula(dr(dl(dr(n, n), dr(n, n)), n), 25).
formula(dr(dl(np, s(dcl)), s(bem)), 24).
formula(dr(dr(dl(np, s(dcl)), dl(np, s(pss))), np), 24).
formula(dr(dr(dl(np, np), dl(np, np)), dr(dl(np, np), dl(np, np))), 24).
formula(dr(dl(np, s(adj)), s(for)), 23).
formula(dl(dl(np, s(adj)), dr(np, np)), 23).
formula(dr(dr(dl(np, s), dl(np, s)), dl(np, s(pss))), 23).
formula(dr(dr(dl(np, s(ng)), pp), pp), 23).
formula(dr(dr(dl(np, s(ng)), dl(np, s(ng))), np), 23).
formula(dr(dr(dl(np(expl), s(dcl)), s(for)), dl(np, s(adj))), 23).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dl(np, s(asup))), 23).
formula(dr(n, s(for)), 22).
formula(dr(dr(s(qem), dl(np, s(dcl))), n), 22).
formula(dr(dl(dl(np, s), dl(np, s)), s(inv)), 22).
formula(dr(dr(dl(np, s(dcl)), dl(np, s(to))), pp), 22).
formula(dr(dr(dl(np, s(adj)), pp), pp), 22).
formula(dr(dl(dr(s, s), dr(s, s)), s(dcl)), 22).
formula(dr(dl(dr(s, s), dr(s, s)), np), 22).
formula(s, 21).
formula(dr(dr(s(dcl), dl(np, s(b))), np), 21).
formula(dr(dr(dl(np, s(b)), dl(np, s(pss))), np), 21).
formula(dr(dr(dl(np, s(adj)), dl(np, s(adj))), n), 21).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(np, s(to))), np), 21).
formula(dl(dl(np, s(adj)), dr(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))))), 21).
formula(dl(dr(s(dcl), np), s(wq)), 20).
formula(dr(dl(s, s), pp), 20).
formula(dr(dl(dr(s(dcl), pp), s(wq)), dl(dr(s(dcl), np), s(wq))), 20).
formula(dr(dl(np, s(adj)), n(num)), 20).
formula(dr(dr(s, s), dl(np, s(asup))), 20).
formula(dr(dr(pp, pp), dr(pp, pp)), 20).
formula(dr(dr(dr(s(wq), pp), n), dr(np, n)), 20).
formula(dr(dl(dr(s(wq), dr(s(q), pp)), dr(s(wq), dr(s(q), pp))), np), 20).
formula(dr(dr(dr(s(wq), dl(np, s(dcl))), n), dr(np, n)), 20).
formula(dr(dr(dl(np, s(dcl)), dl(np, s(adj))), pp), 20).
formula(dr(dr(dl(np, s(b)), dl(np, s(to))), dl(np, s(adj))), 20).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(np, s(pt))), np), 20).
formula(dr(s(qem), dr(s(dcl), np)), 19).
formula(pp, 19).
formula(dr(dl(dl(np, s(pss)), s(dcl)), np), 19).
formula(dr(dr(dl(np, s(pt)), dl(np, s(b))), np), 19).
formula(dr(dl(np, dl(np, np)), np), 19).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), pp), 19).
formula(dr(dr(dr(dl(np, s(dcl)), dl(np, s(to))), dl(np, s(adj))), np(expl)), 19).
formula(dr(dl(np, s(pt)), dl(np, s(b))), 18).
formula(dr(dl(np, s(pss)), s(dcl)), 18).
formula(dr(dl(dl(np, s(b)), s(dcl)), np), 18).
formula(dr(dr(np, dr(s(dcl), np)), n), 18).
formula(dr(dr(dl(np, s(pt)), dl(np, s(ng))), np), 18).
formula(dr(dr(dl(np, s(b)), s(qem)), np), 18).
formula(dr(dr(dl(np, s(b)), s(em)), np), 18).
formula(dr(dl(dr(np(nb), n), dr(np(nb), n)), dr(np(nb), n)), 18).
formula(dr(pp, s(dcl)), 17).
formula(dl(np, dr(n, n)), 17).
formula(dr(dl(dl(np, np), dl(np, np)), s(dcl)), 17).
formula(dr(dl(dl(np, np), dl(np, np)), dl(np, s(dcl))), 17).
formula(dr(dl(dr(n, n), dr(n, n)), dl(np, s(adj))), 17).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dl(dl(np, s), dl(np, s))), 17).
formula(dr(dr(s(q), dl(np, s(dcl))), np), 16).
formula(dr(dl(np, s(pss)), s(qem)), 16).
formula(dr(dl(np, s(ng)), s(for)), 16).
formula(dr(dl(np, s(dcl)), s(wq)), 16).
formula(dr(dr(dl(np, s(dcl)), s(qem)), np), 16).
formula(dr(dr(dl(dl(np, s), dl(np, s)), dl(np, s(pss))), np), 16).
formula(dl(np, s), 15).
formula(dr(s(frg), np), 15).
formula(dr(dl(np, s(pss)), dl(np, s(ng))), 15).
formula(dr(dr(dl(np, s(ng)), pp), dl(np, s(adj))), 15).
formula(dr(dr(dl(np, s(b)), s(for)), dl(np, s(adj))), 15).
formula(dr(dr(dl(np, s(b)), dl(np, s(pt))), np), 15).
formula(dr(dr(dr(s, s), dl(np, s(pt))), np), 15).
formula(dr(dr(dr(s, s), dl(np, s(adj))), np), 15).
formula(dr(dl(s, s), s(q)), 14).
formula(dr(dl(np, s(pss)), dl(np, s(pss))), 14).
formula(dr(dl(np, np), s), 14).
formula(dr(dr(np, np), dl(np, s(adj))), 14).
formula(dr(dr(dl(np, s(b)), s(dcl)), np), 14).
formula(dr(dl(np, dl(np, s(adj))), pp), 14).
formula(dl(np, dl(dl(np, np), dl(np, np))), 14).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dl(np, s(adj))), 14).
formula(dr(dl(np, s(pt)), s(qem)), 13).
formula(dr(dl(np, s(ng)), dl(np, s(b))), 13).
formula(dr(dl(np(expl), s(dcl)), dl(np, s(pt))), 13).
formula(dr(dl(pp, pp), n), 13).
formula(dr(dl(dl(np, s), dl(np, s)), s(ng)), 13).
formula(dr(dr(dl(np, s(pss)), pp), np), 13).
formula(dr(dr(dl(np(expl), s(dcl)), s(em)), np), 13).
formula(dr(dr(dl(np, s(dcl)), dl(np, s(to))), dl(np, s(adj))), 13).
formula(dr(dl(np, dr(s, s)), np), 13).
formula(dr(dr(dr(s, s), dr(s, s)), np), 13).
formula(dr(s(dcl), s(inv)), 12).
formula(dr(np, dr(dl(np, s(to)), np)), 12).
formula(dr(dl(np, s(dcl)), s(b)), 12).
formula(dr(dr(s(dcl), np), np), 12).
formula(dr(dl(np, np), dl(np, s(to))), 12).
formula(dr(dr(np, dl(np, s(dcl))), n), 12).
formula(dl(dr(dl(np, s), dl(np, s)), dr(dl(np, s), dl(np, s))), 12).
formula(dr(dr(dr(s(qem), dl(np, s(dcl))), n), dl(np, s(adj))), 12).
formula(dr(dr(dl(np, s(ng)), np), pp), 12).
formula(dr(dr(dl(np, s(ng)), dl(np, s(pss))), np), 12).
formula(dr(dr(dl(np(expl), s(dcl)), s(em)), pp), 12).
formula(dr(dl(np, dl(np, s(dcl))), dl(np, s(b))), 12).
formula(dr(dl(np, dr(s, s)), s(dcl)), 12).
formula(dr(dr(dr(s, s), dl(np, s(b))), np), 12).
formula(dr(dr(dr(np(nb), n), pp), dl(np, s(adj))), 12).
formula(dr(dr(dr(dl(np, s(b)), s(for)), dl(np, s(adj))), np(expl)), 12).
formula(dr(dr(dr(dl(np, s(adj)), dl(np, s(adj))), dr(dl(np, s(adj)), dl(np, s(adj)))), dr(dr(dl(np, s(adj)), dl(np, s(adj))), dr(dl(np, s(adj)), dl(np, s(adj))))), 12).
formula(s(wq), 11).
formula(s(frg), 11).
formula(dr(s, dl(np, s(dcl))), 11).
formula(dr(dl(s, s), dl(np, s(ng))), 11).
formula(dr(dr(s(dcl), dl(np, s(pt))), np), 11).
formula(dr(dl(pp, pp), s(dcl)), 11).
formula(dl(np, dr(dl(np, s), dl(np, s))), 11).
formula(dr(dr(dl(np, s), dl(np, s)), dl(np, s(asup))), 11).
formula(dr(dr(dr(s(qem), dr(s(dcl), np)), n), dl(np, s(adj))), 11).
formula(dr(dr(dl(np, s(b)), dl(np, s(to))), pp), 11).
formula(dr(dl(dl(np, s(adj)), dl(np, s(adj))), dl(np, s(pss))), 11).
formula(dr(dr(dr(s, s), pp), np), 11).
formula(dr(dr(dl(dl(np, s), dl(np, s)), np), np), 11).
formula(dr(dl(dr(dl(np, s), dl(np, s)), dr(dl(np, s), dl(np, s))), np), 11).
formula(dr(dr(dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dr(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s)))), dl(np, s(asup))), 11).
formula(dr(np, s(dcl)), 10).
formula(dr(n, np), 10).
formula(dr(dl(s, s), n), 10).
formula(dr(dl(s, s), dl(np, s(dcl))), 10).
formula(dr(dl(s, s), dl(np, s(b))), 10).
formula(dr(dl(s(wq), s(wq)), dl(np, s(dcl))), 10).
formula(dr(dr(s(wq), dr(s(q), pp)), dr(s(wq), dr(s(q), dl(np, s(adj))))), 10).
formula(dr(dr(s(wq), dr(s(q), np)), dr(s(wq), dr(s(q), np))), 10).
formula(dr(dl(np, s(ng)), s(bem)), 10).
formula(dr(dl(s(wq), s(dcl)), np), 10).
formula(dr(dl(np(expl), s(dcl)), dl(np, s(pss))), 10).
formula(dl(np, dl(dl(np, s(b)), s(dcl))), 10).
formula(dr(dr(s, s), s(inv)), 10).
formula(dr(dl(np, np), s(inv)), 10).
formula(dr(dl(dr(s(wq), s(q)), dr(s(wq), s(q))), np), 10).
formula(dr(dr(dr(s(wq), dr(s(q), pp)), n), dr(np, n)), 10).
formula(dl(dr(s(wq), dr(s(q), np)), dr(dr(s(wq), dr(s(q), np)), n)), 10).
formula(dr(dr(dr(s(q), pp), pp), np), 10).
formula(dr(dr(dl(np, s(pss)), pp), dl(np, s(adj))), 10).
formula(dr(dr(dl(np, s(ng)), s(em)), np), 10).
formula(dr(dr(dl(np, s(ng)), np), dl(np, s(adj))), 10).
formula(dr(dr(dl(np, s(adj)), s(dcl)), dl(np, s(adj))), 10).
formula(dr(dr(dr(s, s), s(dcl)), dl(np, s(adj))), 10).
formula(dr(dr(dl(np, np), dl(np, s(pss))), np), 10).
formula(dr(dl(dl(dl(np, s), dl(np, s)), dl(dl(np, s), dl(np, s))), dl(np, s(pss))), 10).
formula(dr(dr(dr(dr(s(wq), np), dr(dr(s(q), np), np)), n), dr(np, n)), 10).
formula(dr(dr(dr(dr(s(wq), dl(np, s(pss))), dr(dr(s(q), dl(np, s(pss))), np)), n), dr(np, n)), 10).
formula(dr(dr(dr(dr(s(q), np), pp), dr(dr(dl(np, s(b)), pp), np)), np), 10).
formula(dr(dr(dr(dl(np, s(dcl)), s(em)), dl(np, s(adj))), np(expl)), 10).
