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