param (PROP pax/prop () "") var ( wff a b c d e f g h ) stmt (al-r () ((-> (/\ a b) c)) (-> (/\ b a) c)) stmt (ar-l () ((-> (/\ a b) c)) (-> (/\ b a) c)) stmt (all-l () ((-> (/\ (/\ a b) c) d)) (-> (/\ a (/\ b c)) d)) stmt (alr-l () ((-> (/\ (/\ a b) c) d)) (-> (/\ b (/\ a c)) d)) stmt (arl-l () ((-> (/\ a (/\ b c)) d)) (-> (/\ b (/\ a c)) d)) stmt (arr-l () ((-> (/\ a (/\ b c)) d)) (-> (/\ c (/\ a b)) d)) stmt (all-r () ((-> (/\ (/\ a b) c) d)) (-> (/\ (/\ b c) a) d)) stmt (alr-r () ((-> (/\ (/\ a b) c) d)) (-> (/\ (/\ a c) b) d)) stmt (arl-r () ((-> (/\ a (/\ b c)) d)) (-> (/\ (/\ a c) b) d)) stmt (arr-r () ((-> (/\ a (/\ b c)) d)) (-> (/\ (/\ a b) c) d)) stmt (al-ll () ((-> (/\ a (/\ b c)) d)) (-> (/\ (/\ a b) c) d)) stmt (al-lr () ((-> (/\ a (/\ b c)) d)) (-> (/\ (/\ b a) c) d)) stmt (al-rl () ((-> (/\ a (/\ b c)) d)) (-> (/\ b (/\ a c)) d)) stmt (al-rr () ((-> (/\ a (/\ b c)) d)) (-> (/\ b (/\ c a)) d)) stmt (alll-l () ((-> (/\ (/\ (/\ a b) c) d) e)) (-> (/\ a (/\ (/\ b c) d)) e)) stmt (allr-l () ((-> (/\ (/\ (/\ a b) c) d) e)) (-> (/\ b (/\ (/\ a c) d)) e)) stmt (alrl-l () ((-> (/\ (/\ a (/\ b c)) d) e)) (-> (/\ b (/\ (/\ a c) d)) e)) stmt (alrr-l () ((-> (/\ (/\ a (/\ b c)) d) e)) (-> (/\ c (/\ (/\ a b) d)) e)) stmt (arll-l () ((-> (/\ a (/\ (/\ b c) d)) e)) (-> (/\ b (/\ a (/\ c d))) e)) stmt (arlr-l () ((-> (/\ a (/\ (/\ b c) d)) e)) (-> (/\ c (/\ a (/\ b d))) e)) stmt (arrl-l () ((-> (/\ a (/\ b (/\ c d))) e)) (-> (/\ c (/\ a (/\ b d))) e)) stmt (arrr-l () ((-> (/\ a (/\ b (/\ c d))) e)) (-> (/\ d (/\ a (/\ b c))) e)) stmt (al-lll () ((-> (/\ a (/\ (/\ b c) d)) e)) (-> (/\ (/\ (/\ a b) c) d) e)) stmt (al-llr () ((-> (/\ a (/\ (/\ b c) d)) e)) (-> (/\ (/\ (/\ b a) c) d) e)) stmt (al-lrl () ((-> (/\ a (/\ (/\ b c) d)) e)) (-> (/\ (/\ b (/\ a c)) d) e)) stmt (al-lrr () ((-> (/\ a (/\ (/\ b c) d)) e)) (-> (/\ (/\ b (/\ c a)) d) e)) stmt (al-rll () ((-> (/\ a (/\ b (/\ c d))) e)) (-> (/\ b (/\ (/\ a c) d)) e)) stmt (al-rlr () ((-> (/\ a (/\ b (/\ c d))) e)) (-> (/\ b (/\ (/\ c a) d)) e)) stmt (al-rrl () ((-> (/\ a (/\ b (/\ c d))) e)) (-> (/\ b (/\ c (/\ a d))) e)) stmt (al-rrr () ((-> (/\ a (/\ b (/\ c d))) e)) (-> (/\ b (/\ c (/\ d a))) e)) stmt (allll-l () ((-> (/\ (/\ (/\ (/\ a b) c) d) e) f)) (-> (/\ a (/\ (/\ (/\ b c) d) e)) f)) stmt (alllr-l () ((-> (/\ (/\ (/\ (/\ a b) c) d) e) f)) (-> (/\ b (/\ (/\ (/\ a c) d) e)) f)) stmt (allrl-l () ((-> (/\ (/\ (/\ a (/\ b c)) d) e) f)) (-> (/\ b (/\ (/\ (/\ a c) d) e)) f)) stmt (allrr-l () ((-> (/\ (/\ (/\ a (/\ b c)) d) e) f)) (-> (/\ c (/\ (/\ (/\ a b) d) e)) f)) stmt (alrll-l () ((-> (/\ (/\ a (/\ (/\ b c) d)) e) f)) (-> (/\ b (/\ (/\ a (/\ c d)) e)) f)) stmt (alrlr-l () ((-> (/\ (/\ a (/\ (/\ b c) d)) e) f)) (-> (/\ c (/\ (/\ a (/\ b d)) e)) f)) stmt (alrrl-l () ((-> (/\ (/\ a (/\ b (/\ c d))) e) f)) (-> (/\ c (/\ (/\ a (/\ b d)) e)) f)) stmt (alrrr-l () ((-> (/\ (/\ a (/\ b (/\ c d))) e) f)) (-> (/\ d (/\ (/\ a (/\ b c)) e)) f)) stmt (arlll-l () ((-> (/\ a (/\ (/\ (/\ b c) d) e)) f)) (-> (/\ b (/\ a (/\ (/\ c d) e))) f)) stmt (arllr-l () ((-> (/\ a (/\ (/\ (/\ b c) d) e)) f)) (-> (/\ c (/\ a (/\ (/\ b d) e))) f)) stmt (arlrl-l () ((-> (/\ a (/\ (/\ b (/\ c d)) e)) f)) (-> (/\ c (/\ a (/\ (/\ b d) e))) f)) stmt (arlrr-l () ((-> (/\ a (/\ (/\ b (/\ c d)) e)) f)) (-> (/\ d (/\ a (/\ (/\ b c) e))) f)) stmt (arrll-l () ((-> (/\ a (/\ b (/\ (/\ c d) e))) f)) (-> (/\ c (/\ a (/\ b (/\ d e)))) f)) stmt (arrlr-l () ((-> (/\ a (/\ b (/\ (/\ c d) e))) f)) (-> (/\ d (/\ a (/\ b (/\ c e)))) f)) stmt (arrrl-l () ((-> (/\ a (/\ b (/\ c (/\ d e)))) f)) (-> (/\ d (/\ a (/\ b (/\ c e)))) f)) stmt (arrrr-l () ((-> (/\ a (/\ b (/\ c (/\ d e)))) f)) (-> (/\ e (/\ a (/\ b (/\ c d)))) f)) stmt (alllll-l () ((-> (/\ (/\ (/\ (/\ (/\ a b) c) d) e) f) g)) (-> (/\ a (/\ (/\ (/\ (/\ b c) d) e) f)) g)) stmt (allllll-l () ((-> (/\ (/\ (/\ (/\ (/\ (/\ a b) c) d) e) f) g) h)) (-> (/\ a (/\ (/\ (/\ (/\ (/\ b c) d) e) f) g)) h)) stmt (al-llll () ((-> (/\ a (/\ (/\ (/\ b c) d) e)) f)) (-> (/\ (/\ (/\ (/\ a b) c) d) e) f)) stmt (al-lllr () ((-> (/\ a (/\ (/\ (/\ b c) d) e)) f)) (-> (/\ (/\ (/\ (/\ b a) c) d) e) f)) stmt (al-llrl () ((-> (/\ a (/\ (/\ (/\ b c) d) e)) f)) (-> (/\ (/\ (/\ b (/\ a c)) d) e) f)) stmt (al-llrr () ((-> (/\ a (/\ (/\ (/\ b c) d) e)) f)) (-> (/\ (/\ (/\ b (/\ c a)) d) e) f)) stmt (al-lrll () ((-> (/\ a (/\ (/\ b (/\ c d)) e)) f)) (-> (/\ (/\ b (/\ (/\ a c) d)) e) f)) stmt (al-lrlr () ((-> (/\ a (/\ (/\ b (/\ c d)) e)) f)) (-> (/\ (/\ b (/\ (/\ c a) d)) e) f)) stmt (al-lrrl () ((-> (/\ a (/\ (/\ b (/\ c d)) e)) f)) (-> (/\ (/\ b (/\ c (/\ a d))) e) f)) stmt (al-lrrr () ((-> (/\ a (/\ (/\ b (/\ c d)) e)) f)) (-> (/\ (/\ b (/\ c (/\ d a))) e) f)) stmt (al-rlll () ((-> (/\ a (/\ b (/\ (/\ c d) e))) f)) (-> (/\ b (/\ (/\ (/\ a c) d) e)) f)) stmt (al-rllr () ((-> (/\ a (/\ b (/\ (/\ c d) e))) f)) (-> (/\ b (/\ (/\ (/\ c a) d) e)) f)) stmt (al-rlrl () ((-> (/\ a (/\ b (/\ (/\ c d) e))) f)) (-> (/\ b (/\ (/\ c (/\ a d)) e)) f)) stmt (al-rlrr () ((-> (/\ a (/\ b (/\ (/\ c d) e))) f)) (-> (/\ b (/\ (/\ c (/\ d a)) e)) f)) stmt (al-rrll () ((-> (/\ a (/\ b (/\ c (/\ d e)))) f)) (-> (/\ b (/\ c (/\ (/\ a d) e))) f)) stmt (al-rrlr () ((-> (/\ a (/\ b (/\ c (/\ d e)))) f)) (-> (/\ b (/\ c (/\ (/\ d a) e))) f)) stmt (al-rrrl () ((-> (/\ a (/\ b (/\ c (/\ d e)))) f)) (-> (/\ b (/\ c (/\ d (/\ a e)))) f)) stmt (al-rrrr () ((-> (/\ a (/\ b (/\ c (/\ d e)))) f)) (-> (/\ b (/\ c (/\ d (/\ e a)))) f)) stmt (alar () ((-> (/\ a a) b)) (-> a b)) stmt (allar () ((-> (/\ (/\ a b) a) c)) (-> (/\ a b) c)) stmt (alrar () ((-> (/\ (/\ a b) b) c)) (-> (/\ a b) c)) stmt (arall () ((-> (/\ (/\ a b) a) c)) (-> (/\ b a) c)) stmt (alarl () ((-> (/\ a (/\ a b)) c)) (-> (/\ a b) c)) stmt (arral () ((-> (/\ a (/\ b a)) c)) (-> (/\ b a) c)) stmt (allalr () ((-> (/\ (/\ a a) b) c)) (-> (/\ a b) c)) stmt (allarl () ((-> (/\ (/\ a b) (/\ a c)) d)) (-> (/\ (/\ a b) c) d)) stmt (alrarr () ((-> (/\ (/\ a b) (/\ c b)) d)) (-> (/\ (/\ a b) c) d)) stmt (syl-l () ((-> a b) (-> (/\ b c) d)) (-> (/\ a c) d)) stmt (syl-r () ((-> a b) (-> (/\ c b) d)) (-> (/\ c a) d)) stmt (syl-ll () ((-> a b) (-> (/\ (/\ b c) d) e)) (-> (/\ (/\ a c) d) e)) stmt (syl-lr () ((-> a b) (-> (/\ (/\ c b) d) e)) (-> (/\ (/\ c a) d) e)) stmt (syl-rl () ((-> a b) (-> (/\ c (/\ b d)) e)) (-> (/\ c (/\ a d)) e)) stmt (syl-rr () ((-> a b) (-> (/\ c (/\ d b)) e)) (-> (/\ c (/\ d a)) e))