diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 1126 |
1 files changed, 563 insertions, 563 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 9583d92d..d48ed6f3 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,14 +1,14 @@ -(142485 . 3409939483) -(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) #0#) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(142485 . 3410359543) +(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) #0#) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (((|#2| |#2|) . T)) ((((-522)) . T)) -((($ $) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((|#2| |#2|) . T) ((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522))))) +((($ $) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((|#2| |#2|) . T) ((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522))))) ((($) . T)) (((|#1|) . T)) ((($) . T) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#2|) . T)) -((($) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((|#2|) . T) (((-382 (-522))) |has| |#2| (-37 (-382 (-522))))) +((($) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((|#2|) . T) (((-382 (-522))) |has| |#2| (-37 (-382 (-522))))) (|has| |#1| (-838)) ((((-792)) . T)) ((((-792)) . T)) @@ -23,28 +23,28 @@ ((((-202)) . T) (((-792)) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-782))) -((($ $) . T) ((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1| |#1|) . T)) -(-3708 (|has| |#1| (-757)) (|has| |#1| (-784))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-782))) +((($ $) . T) ((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1| |#1|) . T)) +(-3844 (|has| |#1| (-757)) (|has| |#1| (-784))) ((((-382 (-522))) |has| |#1| (-962 (-382 (-522)))) (((-522)) |has| |#1| (-962 (-522))) ((|#1|) . T)) ((((-792)) . T)) ((((-792)) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (|has| |#1| (-782)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1| |#2| |#3|) . T)) (((|#4|) . T)) -((($) . T) (((-382 (-522))) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) +((($) . T) (((-382 (-522))) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) ((((-792)) . T)) ((((-792)) |has| |#1| (-1014))) (((|#1|) . T) ((|#2|) . T)) (((|#1|) . T) (((-522)) |has| |#1| (-962 (-522))) (((-382 (-522))) |has| |#1| (-962 (-382 (-522))))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) -(((|#2| (-455 (-3480 |#1|) (-708))) . T)) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(((|#2| (-455 (-3591 |#1|) (-708))) . T)) (((|#1| (-494 (-1085))) . T)) (((#0=(-799 |#1|) #0#) . T) ((#1=(-382 (-522)) #1#) . T) (($ $) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (|has| |#4| (-343)) (|has| |#3| (-343)) (((|#1|) . T)) @@ -54,10 +54,10 @@ (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-514)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) ((($) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) ((($) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T)) ((($) . T)) @@ -66,59 +66,59 @@ ((((-792)) . T)) ((((-792)) . T)) ((((-382 (-522))) . T) (($) . T)) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (((-1158 |#1| |#2| |#3|)) |has| |#1| (-338)) (($) . T) ((|#1|) . T)) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (((-1158 |#1| |#2| |#3|)) |has| |#1| (-338)) (($) . T) ((|#1|) . T)) ((((-792)) . T)) ((((-792)) . T)) ((((-792)) . T)) (((|#1|) . T)) -(((|#1|) . T) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) . T)) +(((|#1|) . T) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) . T)) (((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) (($) . T)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#1| |#2|) . T)) ((((-792)) . T)) (((|#1|) . T)) -(((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522)))) ((|#2| |#2|) . T) (($ $) -3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +(((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522)))) ((|#2| |#2|) . T) (($ $) -3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) (((|#1|) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) -((($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) -(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) +(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) ((($ $) . T)) (((|#2|) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T) (($) -3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T) (($) -3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) ((($) . T)) (|has| |#1| (-343)) (((|#1|) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) ((((-792)) . T)) ((((-792)) . T)) (((|#1| |#2|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) (((|#1| |#1|) . T)) (|has| |#1| (-514)) (((|#2| |#2|) -12 (|has| |#1| (-338)) (|has| |#2| (-285 |#2|))) (((-1085) |#2|) -12 (|has| |#1| (-338)) (|has| |#2| (-483 (-1085) |#2|)))) ((((-382 |#2|)) . T) (((-382 (-522))) . T) (($) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-782))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-782))) ((($ $) . T) ((#0=(-382 (-522)) #0#) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (|has| |#1| (-1014)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (|has| |#1| (-1014)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (|has| |#1| (-782)) ((($) . T) (((-382 (-522))) . T)) (((|#1|) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) -(-3708 (|has| |#4| (-730)) (|has| |#4| (-782))) -(-3708 (|has| |#4| (-730)) (|has| |#4| (-782))) -(-3708 (|has| |#3| (-730)) (|has| |#3| (-782))) -(-3708 (|has| |#3| (-730)) (|has| |#3| (-782))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#4| (-730)) (|has| |#4| (-782))) +(-3844 (|has| |#4| (-730)) (|has| |#4| (-782))) +(-3844 (|has| |#3| (-730)) (|has| |#3| (-782))) +(-3844 (|has| |#3| (-730)) (|has| |#3| (-782))) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-1014)) @@ -132,21 +132,21 @@ ((((-522)) . T)) ((((-522)) . T)) (((|#1|) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) (((|#1| (-708)) . T)) (|has| |#2| (-730)) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) (|has| |#2| (-782)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) ((((-1068) |#1|) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (((|#1|) . T)) (((|#3| (-708)) . T)) (|has| |#1| (-135)) (|has| |#1| (-133)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (|has| |#1| (-1014)) ((((-382 (-522))) . T) (((-522)) . T)) ((((-1085) |#2|) |has| |#2| (-483 (-1085) |#2|)) ((|#2| |#2|) |has| |#2| (-285 |#2|))) @@ -154,7 +154,7 @@ (((|#1|) . T) (($) . T)) ((((-522)) . T)) ((((-522)) . T)) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) |has| |#1| (-157))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) |has| |#1| (-157))) ((((-522)) . T)) ((((-522)) . T)) (((#0=(-637) (-1081 #0#)) . T)) @@ -173,12 +173,12 @@ ((((-792)) . T)) ((((-792)) . T)) (((|#1| |#1|) . T)) -(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) (((|#1|) . T)) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) -((($) -3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971)))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971)))) ((((-792)) . T)) ((((-792)) . T)) ((((-792)) . T)) @@ -189,25 +189,25 @@ ((((-154 (-202))) |has| |#1| (-947)) (((-154 (-354))) |has| |#1| (-947)) (((-498)) |has| |#1| (-563 (-498))) (((-1081 |#1|)) . T) (((-821 (-522))) |has| |#1| (-563 (-821 (-522)))) (((-821 (-354))) |has| |#1| (-563 (-821 (-354))))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-782))) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-782))) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#2|) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) -(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514)))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-782))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-782))) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#2|) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) +(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514)))) (|has| |#1| (-338)) (-12 (|has| |#4| (-210)) (|has| |#4| (-971))) (-12 (|has| |#3| (-210)) (|has| |#3| (-971))) -(-3708 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((((-792)) . T)) (((|#1|) . T)) ((((-382 (-522))) |has| |#1| (-962 (-382 (-522)))) (((-522)) |has| |#1| (-962 (-522))) ((|#1|) . T)) (((|#1|) . T) (((-522)) |has| |#1| (-584 (-522)))) -(((|#2|) . T) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) (|has| |#1| (-514)) (|has| |#1| (-514)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#1|) . T)) (|has| |#1| (-514)) (|has| |#1| (-514)) @@ -218,11 +218,11 @@ (((|#2|) . T) (($) . T) (((-382 (-522))) . T)) (-12 (|has| |#1| (-1014)) (|has| |#2| (-1014))) ((($) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T)) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (((-1083 |#1| |#2| |#3|)) |has| |#1| (-338)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) . T)) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (((-1083 |#1| |#2| |#3|)) |has| |#1| (-338)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) . T)) (((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) (($) . T)) -(((|#4| |#4|) -3708 (|has| |#4| (-157)) (|has| |#4| (-338)) (|has| |#4| (-971))) (($ $) |has| |#4| (-157))) -(((|#3| |#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971))) (($ $) |has| |#3| (-157))) +(((|#4| |#4|) -3844 (|has| |#4| (-157)) (|has| |#4| (-338)) (|has| |#4| (-971))) (($ $) |has| |#4| (-157))) +(((|#3| |#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971))) (($ $) |has| |#3| (-157))) (((|#1|) . T)) (((|#2|) . T)) ((((-498)) |has| |#2| (-563 (-498))) (((-821 (-354))) |has| |#2| (-563 (-821 (-354)))) (((-821 (-522))) |has| |#2| (-563 (-821 (-522))))) @@ -231,21 +231,21 @@ ((((-792)) . T)) ((((-498)) |has| |#1| (-563 (-498))) (((-821 (-354))) |has| |#1| (-563 (-821 (-354)))) (((-821 (-522))) |has| |#1| (-563 (-821 (-522))))) ((((-792)) . T)) -(((|#4|) -3708 (|has| |#4| (-157)) (|has| |#4| (-338)) (|has| |#4| (-971))) (($) |has| |#4| (-157))) -(((|#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971))) (($) |has| |#3| (-157))) +(((|#4|) -3844 (|has| |#4| (-157)) (|has| |#4| (-338)) (|has| |#4| (-971))) (($) |has| |#4| (-157))) +(((|#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971))) (($) |has| |#3| (-157))) ((((-792)) . T)) ((((-498)) . T) (((-522)) . T) (((-821 (-522))) . T) (((-354)) . T) (((-202)) . T)) (((|#1|) . T) (((-522)) |has| |#1| (-962 (-522))) (((-382 (-522))) |has| |#1| (-962 (-382 (-522))))) ((($) . T) (((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T)) ((((-382 $) (-382 $)) |has| |#2| (-514)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 (-51)))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 (-51)))) . T)) (((|#1|) . T)) (|has| |#2| (-838)) ((((-1068) (-51)) . T)) ((((-522)) |has| #0=(-382 |#2|) (-584 (-522))) ((#0#) . T)) ((((-498)) . T) (((-202)) . T) (((-354)) . T) (((-821 (-354))) . T)) ((((-792)) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) (((|#1|) |has| |#1| (-157))) (((|#1| $) |has| |#1| (-262 |#1| |#1|))) ((((-792)) . T)) @@ -256,13 +256,13 @@ (|has| |#1| (-784)) (|has| |#1| (-1014)) (((|#1|) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) -((($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (|has| |#1| (-210)) -((($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1| (-494 (-755 (-1085)))) . T)) (((|#1| (-898)) . T)) (((#0=(-799 |#1|) $) |has| #0# (-262 #0# #0#))) @@ -271,7 +271,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1061)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) (|has| (-1152 |#1| |#2| |#3| |#4|) (-133)) (|has| (-1152 |#1| |#2| |#3| |#4|) (-135)) (|has| |#1| (-133)) @@ -288,20 +288,20 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-971))) ((((-792)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) #0#) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) #0#) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (((|#1|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014))) ((#0=(-2 (|:| -2530 (-1068)) (|:| -3048 |#1|)) #0#) |has| (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|)) (-285 (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014))) ((#0=(-2 (|:| -2644 (-1068)) (|:| -3149 |#1|)) #0#) |has| (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|)) (-285 (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))))) ((((-522) |#1|) . T)) ((((-792)) . T)) ((((-498)) -12 (|has| |#1| (-563 (-498))) (|has| |#2| (-563 (-498)))) (((-821 (-354))) -12 (|has| |#1| (-563 (-821 (-354)))) (|has| |#2| (-563 (-821 (-354))))) (((-821 (-522))) -12 (|has| |#1| (-563 (-821 (-522)))) (|has| |#2| (-563 (-821 (-522)))))) ((((-792)) . T)) ((((-792)) . T)) ((($) . T)) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) ((($) . T)) ((($) . T)) ((($) . T)) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((((-792)) . T)) ((((-792)) . T)) (|has| (-1151 |#2| |#3| |#4|) (-135)) @@ -312,16 +312,16 @@ ((((-792)) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) (((|#1|) . T)) ((((-522) |#1|) . T)) (((|#2|) |has| |#2| (-157))) (((|#1|) |has| |#1| (-157))) (((|#1|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-782))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-782))) ((((-792)) |has| |#1| (-1014))) -(-3708 (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)) (|has| |#1| (-1026))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)) (|has| |#1| (-1026))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((((-839 |#1|)) . T)) ((((-382 |#2|) |#3|) . T)) (|has| |#1| (-15 * (|#1| (-522) |#1|))) @@ -333,7 +333,7 @@ (((|#1|) . T)) ((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) |has| |#1| (-514))) (|has| |#1| (-338)) -(-3708 (-12 (|has| (-1158 |#1| |#2| |#3|) (-210)) (|has| |#1| (-338))) (|has| |#1| (-15 * (|#1| (-522) |#1|)))) +(-3844 (-12 (|has| (-1158 |#1| |#2| |#3|) (-210)) (|has| |#1| (-338))) (|has| |#1| (-15 * (|#1| (-522) |#1|)))) (|has| |#1| (-15 * (|#1| (-382 (-522)) |#1|))) (|has| |#1| (-338)) ((((-522)) . T)) @@ -345,31 +345,31 @@ (((|#1|) . T)) ((((-522) |#1|) . T)) (((|#2|) . T)) -(-3708 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) (((|#1|) . T)) ((((-1085)) -12 (|has| |#3| (-829 (-1085))) (|has| |#3| (-971)))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (-12 (|has| |#1| (-338)) (|has| |#2| (-757))) -(-3708 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324)) (|has| |#1| (-514))) -(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-514)))) +(-3844 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324)) (|has| |#1| (-514))) +(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-514)))) ((($ $) |has| |#1| (-514))) (((#0=(-637) (-1081 #0#)) . T)) ((((-792)) . T)) ((((-792)) . T) (((-1166 |#4|)) . T)) ((((-792)) . T) (((-1166 |#3|)) . T)) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-514)))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-514)))) ((($) |has| |#1| (-514))) ((((-792)) . T)) ((($) . T)) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((#1=(-1158 |#1| |#2| |#3|) #1#) |has| |#1| (-338)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (((-1158 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) . T)) -(((|#1|) . T) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((#1=(-1158 |#1| |#2| |#3|) #1#) |has| |#1| (-338)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (((-1158 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) . T)) +(((|#1|) . T) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) (((|#3|) |has| |#3| (-971))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (|has| |#1| (-1014)) (((|#2| (-756 |#1|)) . T)) (((|#1|) . T)) @@ -381,37 +381,37 @@ ((((-132)) . T)) (((|#3|) |has| |#3| (-1014)) (((-522)) -12 (|has| |#3| (-962 (-522))) (|has| |#3| (-1014))) (((-382 (-522))) -12 (|has| |#3| (-962 (-382 (-522)))) (|has| |#3| (-1014)))) ((((-792)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1|) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) . T)) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) . T)) (|has| |#1| (-338)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-782))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-782))) ((((-1085) |#1|) |has| |#1| (-483 (-1085) |#1|)) ((|#1| |#1|) |has| |#1| (-285 |#1|))) (|has| |#2| (-757)) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-782)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) ((((-792)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-498)) |has| |#1| (-563 (-498)))) (((|#1| |#2|) . T)) ((((-1085)) -12 (|has| |#1| (-338)) (|has| |#1| (-829 (-1085))))) ((((-1068) |#1|) . T)) (((|#1| |#2| |#3| (-494 |#3|)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (|has| |#1| (-343)) (|has| |#1| (-343)) (|has| |#1| (-343)) ((((-792)) . T)) (((|#1|) . T)) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) (|has| |#1| (-343)) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((((-522)) . T)) ((((-522)) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((((-792)) . T)) ((((-792)) . T)) (-12 (|has| |#2| (-210)) (|has| |#2| (-971))) @@ -420,10 +420,10 @@ ((((-522) |#4|) . T)) ((((-522) |#3|) . T)) (((|#1|) . T) (((-522)) |has| |#1| (-584 (-522)))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((((-1152 |#1| |#2| |#3| |#4|)) . T)) ((((-382 (-522))) . T) (((-522)) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (((|#1| |#1|) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) @@ -452,37 +452,37 @@ ((($) . T)) ((($ $) . T) ((#0=(-1085) $) . T) ((#0# |#1|) . T)) (((|#2|) |has| |#2| (-157))) -((($) -3708 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((|#2|) |has| |#2| (-157)) (((-382 (-522))) |has| |#2| (-37 (-382 (-522))))) -(((|#2| |#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($ $) |has| |#2| (-157))) +((($) -3844 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((|#2|) |has| |#2| (-157)) (((-382 (-522))) |has| |#2| (-37 (-382 (-522))))) +(((|#2| |#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($ $) |has| |#2| (-157))) ((((-132)) . T)) (((|#1|) . T)) (-12 (|has| |#1| (-343)) (|has| |#2| (-343))) ((((-792)) . T)) -(((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($) |has| |#2| (-157))) +(((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($) |has| |#2| (-157))) (((|#1|) . T)) ((((-792)) . T)) (|has| |#1| (-1014)) (|has| $ (-135)) ((((-522) |#1|) . T)) -((($) -3708 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) +((($) -3844 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) ((((-1085)) -12 (|has| |#1| (-15 * (|#1| (-382 (-522)) |#1|))) (|has| |#1| (-829 (-1085))))) (|has| |#1| (-338)) -(-3708 (-12 (|has| (-1083 |#1| |#2| |#3|) (-210)) (|has| |#1| (-338))) (|has| |#1| (-15 * (|#1| (-522) |#1|)))) +(-3844 (-12 (|has| (-1083 |#1| |#2| |#3|) (-210)) (|has| |#1| (-338))) (|has| |#1| (-15 * (|#1| (-522) |#1|)))) (|has| |#1| (-15 * (|#1| (-382 (-522)) |#1|))) (|has| |#1| (-338)) (|has| |#1| (-15 * (|#1| (-708) |#1|))) (((|#1|) . T)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) ((((-792)) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) (((|#2| (-494 (-794 |#1|))) . T)) ((((-792)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1|) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((((-535 |#1|)) . T)) ((($) . T)) (((|#1|) . T) (($) . T)) @@ -499,28 +499,28 @@ ((((-792)) . T)) ((((-792)) . T)) (((|#1| |#2| |#3| |#4| |#5|) . T)) -(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-514)))) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((#1=(-1083 |#1| |#2| |#3|) #1#) |has| |#1| (-338)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-514)))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((#1=(-1083 |#1| |#2| |#3|) #1#) |has| |#1| (-338)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) (((|#2|) |has| |#2| (-971))) (|has| |#1| (-1014)) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-514)))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (((-1083 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) . T)) -(((|#1|) . T) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-514)))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (((-1083 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) . T)) +(((|#1|) . T) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1|) |has| |#1| (-157)) (($) . T)) (((|#1|) . T)) -(((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522)))) ((|#2| |#2|) . T) (($ $) -3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +(((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522)))) ((|#2| |#2|) . T) (($ $) -3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) ((((-792)) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) ((($ $) . T) ((|#2| $) . T) ((|#2| |#1|) . T)) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) (((#0=(-999) |#1|) . T) ((#0# $) . T) (($ $) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T) (($) -3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T) (($) -3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) ((($) . T)) (((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) (($) . T)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#2|) |has| |#1| (-338))) (((|#1|) . T)) (((|#2|) |has| |#2| (-1014)) (((-522)) -12 (|has| |#2| (-962 (-522))) (|has| |#2| (-1014))) (((-382 (-522))) -12 (|has| |#2| (-962 (-382 (-522)))) (|has| |#2| (-1014)))) @@ -534,8 +534,8 @@ (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-133)) (|has| |#1| (-135)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) -((($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((((-382 (-522))) . T) (($) . T)) ((((-382 (-522))) . T) (($) . T)) ((((-382 (-522))) . T) (($) . T)) @@ -546,12 +546,12 @@ (((|#1| (-708) (-999)) . T)) ((((-382 (-522))) |has| |#2| (-338)) (($) . T)) (((|#1| (-494 (-1004 (-1085))) (-1004 (-1085))) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (((|#1|) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) (|has| |#2| (-730)) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) (|has| |#1| (-343)) (|has| |#1| (-343)) (|has| |#1| (-343)) @@ -583,61 +583,61 @@ (((|#4| |#4|) -12 (|has| |#4| (-285 |#4|)) (|has| |#4| (-1014)))) (((|#2|) . T) (((-522)) |has| |#2| (-962 (-522))) (((-382 (-522))) |has| |#2| (-962 (-382 (-522))))) (((|#3| |#3|) -12 (|has| |#3| (-285 |#3|)) (|has| |#3| (-1014)))) -(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) ((($) . T)) (((|#2|) . T)) (((|#3|) . T)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) -(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (((|#2|) . T)) -((((-792)) -3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-562 (-792))) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((-1166 |#2|)) . T)) +((((-792)) -3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-562 (-792))) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((-1166 |#2|)) . T)) (((|#1|) |has| |#1| (-157))) ((((-522)) . T)) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((((-522) (-132)) . T)) -((($) -3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971)))) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) +((($) -3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971)))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) (((|#1|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) (((|#2|) |has| |#1| (-338))) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1| |#1|) . T) (($ $) . T)) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) |has| |#1| (-157))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) |has| |#1| (-157))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1| (-494 #0=(-1085)) #0#) . T)) (((|#1|) . T) (($) . T)) (|has| |#4| (-157)) (|has| |#3| (-157)) (((#0=(-382 (-881 |#1|)) #0#) . T)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (|has| |#1| (-1014)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (|has| |#1| (-1014)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#1| |#1|) |has| |#1| (-157))) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1|) . T)) ((((-382 (-881 |#1|))) . T)) (((|#1|) |has| |#1| (-157))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((((-792)) . T)) ((((-1152 |#1| |#2| |#3| |#4|)) . T)) (((|#1|) |has| |#1| (-971)) (((-522)) -12 (|has| |#1| (-584 (-522))) (|has| |#1| (-971)))) (((|#1| |#2|) . T)) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) (|has| |#3| (-730)) -(-3708 (|has| |#3| (-730)) (|has| |#3| (-782))) +(-3844 (|has| |#3| (-730)) (|has| |#3| (-782))) (|has| |#3| (-782)) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#2|) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) -(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514)))) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#2|) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) +(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514)))) (((|#2|) . T)) ((((-792)) . T)) ((((-792)) . T)) @@ -652,22 +652,22 @@ (|has| |#1| (-1014)) (((|#2|) . T)) ((((-498)) |has| |#2| (-563 (-498))) (((-821 (-354))) |has| |#2| (-563 (-821 (-354)))) (((-821 (-522))) |has| |#2| (-563 (-821 (-522))))) -(((|#4|) -3708 (|has| |#4| (-157)) (|has| |#4| (-338)))) -(((|#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)))) +(((|#4|) -3844 (|has| |#4| (-157)) (|has| |#4| (-338)))) +(((|#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)))) ((((-792)) . T)) (((|#1|) . T)) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-838))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-838))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-838))) ((($ $) . T) ((#0=(-1085) $) |has| |#1| (-210)) ((#0# |#1|) |has| |#1| (-210)) ((#1=(-755 (-1085)) |#1|) . T) ((#1# $) . T)) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-838))) ((((-522) |#2|) . T)) ((((-792)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) -((($) -3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((|#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971)))) +((($) -3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((|#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971)))) ((((-522) |#1|) . T)) (|has| (-382 |#2|) (-135)) (|has| (-382 |#2|) (-133)) @@ -680,21 +680,21 @@ (|has| |#1| (-514)) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-792)) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) (|has| |#1| (-37 (-382 (-522)))) -((((-363) (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +((((-363) (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) (|has| |#1| (-37 (-382 (-522)))) (|has| |#2| (-1061)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((|#1|) . T)) ((((-363) (-1068)) . T)) (|has| |#1| (-514)) ((((-112 |#1|)) . T)) ((((-522) |#1|) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (((|#2|) . T)) ((((-792)) . T)) ((((-756 |#1|)) . T)) @@ -707,7 +707,7 @@ (((|#1|) |has| |#1| (-157))) ((((-792)) . T)) ((((-498)) |has| |#1| (-563 (-498)))) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#2|) |has| |#2| (-285 |#2|))) (((#0=(-522) #0#) . T) ((#1=(-382 (-522)) #1#) . T) (($ $) . T)) (((|#1|) . T)) @@ -717,7 +717,7 @@ (((#0=(-522) #0#) . T) ((#1=(-382 (-522)) #1#) . T) (($ $) . T)) ((($) . T) (((-522)) . T) (((-382 (-522))) . T)) (|has| |#2| (-343)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) @@ -728,9 +728,9 @@ ((((-1083 |#1| |#2| |#3|) $) -12 (|has| (-1083 |#1| |#2| |#3|) (-262 (-1083 |#1| |#2| |#3|) (-1083 |#1| |#2| |#3|))) (|has| |#1| (-338))) (($ $) . T)) ((((-792)) . T)) ((((-792)) . T)) -((($) . T) (((-382 (-522))) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) +((($) . T) (((-382 (-522))) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) ((((-498)) |has| |#1| (-563 (-498)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) ((($ $) . T)) ((($ $) . T)) ((((-792)) . T)) @@ -740,12 +740,12 @@ (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -((($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((((-382 (-522))) . T) (((-522)) . T)) ((((-522) (-132)) . T)) ((((-132)) . T)) (((|#1|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) ((((-108)) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) ((((-108)) . T)) @@ -753,38 +753,38 @@ ((((-498)) |has| |#1| (-563 (-498))) (((-202)) . #0=(|has| |#1| (-947))) (((-354)) . #0#)) ((((-792)) . T)) (|has| |#1| (-757)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (|has| |#1| (-784)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-514))) (|has| |#1| (-514)) (|has| |#1| (-838)) (((|#1|) . T)) (|has| |#1| (-1014)) ((((-792)) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((((-792)) . T)) ((((-792)) . T)) ((((-792)) . T)) (((|#1| (-1166 |#1|) (-1166 |#1|)) . T)) ((((-522) (-132)) . T)) ((($) . T)) -(-3708 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((((-792)) . T)) (|has| |#1| (-1014)) (((|#1| (-898)) . T)) (((|#1| |#1|) . T)) ((($) . T)) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) (-12 (|has| |#1| (-447)) (|has| |#2| (-447))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) -(-3708 (-12 (|has| |#1| (-447)) (|has| |#2| (-447))) (-12 (|has| |#1| (-664)) (|has| |#2| (-664)))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (-12 (|has| |#1| (-447)) (|has| |#2| (-447))) (-12 (|has| |#1| (-664)) (|has| |#2| (-664)))) (((|#1|) . T)) (|has| |#2| (-730)) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) (((|#1| |#2|) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (|has| |#2| (-782)) @@ -799,7 +799,7 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-382 (-522))) . T) (($) . T)) -((($) . T) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) . T)) +((($) . T) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) . T)) (|has| |#1| (-765)) ((((-382 (-522))) |has| |#1| (-962 (-382 (-522)))) (((-522)) |has| |#1| (-962 (-522))) ((|#1|) . T)) (|has| |#1| (-1014)) @@ -810,8 +810,8 @@ (((|#3|) |has| |#3| (-1014))) (|has| |#3| (-343)) (((|#1|) . T) (((-792)) . T)) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-1158 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) -(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514)))) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-1158 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) +(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514)))) ((((-792)) . T)) ((($) |has| |#1| (-514)) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#2|) . T)) @@ -821,30 +821,30 @@ (((|#1|) . T)) (((|#1|) |has| |#1| (-157))) ((((-382 (-522))) . T) (((-522)) . T)) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) ((((-132)) . T)) (((|#1|) . T)) ((((-132)) . T)) -((($) -3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971)))) +((($) -3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971)))) ((((-132)) . T)) (((|#1| |#2| |#3|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) (|has| $ (-135)) (|has| $ (-135)) (|has| |#1| (-1014)) ((((-792)) . T)) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-447)) (|has| |#1| (-514)) (|has| |#1| (-971)) (|has| |#1| (-1026))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-447)) (|has| |#1| (-514)) (|has| |#1| (-971)) (|has| |#1| (-1026))) ((($ $) |has| |#1| (-262 $ $)) ((|#1| $) |has| |#1| (-262 |#1| |#1|))) (((|#1| (-382 (-522))) . T)) (((|#1|) . T)) ((((-1085)) . T)) (|has| |#1| (-514)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (|has| |#1| (-514)) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) @@ -855,7 +855,7 @@ (|has| |#1| (-135)) (|has| |#1| (-133)) (|has| |#4| (-782)) -(((|#2| (-217 (-3480 |#1|) (-708)) (-794 |#1|)) . T)) +(((|#2| (-217 (-3591 |#1|) (-708)) (-794 |#1|)) . T)) (|has| |#3| (-782)) (((|#1| (-494 |#3|) |#3|) . T)) (|has| |#1| (-135)) @@ -869,21 +869,21 @@ (|has| |#1| (-133)) ((((-382 (-522))) |has| |#2| (-338)) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) -(-3708 (|has| |#1| (-324)) (|has| |#1| (-343))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#1| (-324)) (|has| |#1| (-343))) ((((-1052 |#2| |#1|)) . T) ((|#1|) . T)) (|has| |#2| (-157)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-210)) (|has| |#2| (-971))) -(((|#2|) . T) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -(-3708 (|has| |#3| (-730)) (|has| |#3| (-782))) -(-3708 (|has| |#3| (-730)) (|has| |#3| (-782))) +(((|#2|) . T) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +(-3844 (|has| |#3| (-730)) (|has| |#3| (-782))) +(-3844 (|has| |#3| (-730)) (|has| |#3| (-782))) ((((-792)) . T)) (((|#1|) . T)) (((|#2|) . T) (($) . T)) (((|#1|) . T) (($) . T)) ((((-637)) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) (|has| |#1| (-514)) (((|#1|) . T)) (((|#1|) . T)) @@ -905,10 +905,10 @@ (((|#1| (-382 (-522))) . T)) (((|#3|) . T) (((-561 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((($ $) . T) ((|#2| $) . T)) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) (((#0=(-1083 |#1| |#2| |#3|) #0#) -12 (|has| (-1083 |#1| |#2| |#3|) (-285 (-1083 |#1| |#2| |#3|))) (|has| |#1| (-338))) (((-1085) #0#) -12 (|has| (-1083 |#1| |#2| |#3|) (-483 (-1085) (-1083 |#1| |#2| |#3|))) (|has| |#1| (-338)))) @@ -916,8 +916,8 @@ ((((-792)) . T)) ((((-792)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) -(((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014))) (((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) |has| (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|)) (-285 (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))))) +(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) +(((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014))) (((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) |has| (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|)) (-285 (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))))) ((((-792)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -928,10 +928,10 @@ ((($ $) . T) ((#0=(-794 |#1|) $) . T) ((#0# |#2|) . T)) (|has| |#1| (-765)) (|has| |#1| (-1014)) -(((|#2| |#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($ $) |has| |#2| (-157))) -(((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)))) -((((-522) (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T) ((|#1| |#2|) . T)) -(((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($) |has| |#2| (-157))) +(((|#2| |#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($ $) |has| |#2| (-157))) +(((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)))) +((((-522) (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T) ((|#1| |#2|) . T)) +(((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($) |has| |#2| (-157))) ((((-708)) . T)) ((((-522)) . T)) (|has| |#1| (-514)) @@ -944,29 +944,29 @@ ((((-112 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-135)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-514))) ((((-821 (-522))) . T) (((-821 (-354))) . T) (((-498)) . T) (((-1085)) . T)) ((((-792)) . T)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) ((($) . T)) ((((-792)) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) (((|#2|) |has| |#2| (-157))) -((($) -3708 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((|#2|) |has| |#2| (-157)) (((-382 (-522))) |has| |#2| (-37 (-382 (-522))))) +((($) -3844 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((|#2|) |has| |#2| (-157)) (((-382 (-522))) |has| |#2| (-37 (-382 (-522))))) ((((-799 |#1|)) . T)) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (-12 (|has| |#3| (-210)) (|has| |#3| (-971))) (|has| |#2| (-1061)) -(((#0=(-51)) . T) (((-2 (|:| -2530 (-1085)) (|:| -3048 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -2644 (-1085)) (|:| -3149 #0#))) . T)) (((|#1| |#2|) . T)) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) (((|#1| (-522) (-999)) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1| (-382 (-522)) (-999)) . T)) -((($) -3708 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) +((($) -3844 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) ((((-522) |#2|) . T)) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) @@ -974,37 +974,37 @@ (-12 (|has| |#1| (-343)) (|has| |#2| (-343))) ((((-792)) . T)) ((((-1085) |#1|) |has| |#1| (-483 (-1085) |#1|)) ((|#1| |#1|) |has| |#1| (-285 |#1|))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) (((|#1|) . T)) ((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) |has| |#1| (-514))) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-1083 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) -(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514)))) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-1083 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) +(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514)))) ((($) |has| |#1| (-514)) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((((-792)) . T)) (|has| |#1| (-324)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) #0#) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) #0#) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (|has| |#1| (-514)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) ((((-792)) . T)) (((|#1| |#2|) . T)) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-838))) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-838))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-838))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-838))) ((((-382 (-522))) . T) (((-522)) . T)) ((((-522)) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) ((($) . T)) ((((-792)) . T)) (((|#1|) . T)) ((((-799 |#1|)) . T) (($) . T) (((-382 (-522))) . T)) ((((-792)) . T)) -(((|#3| |#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971))) (($ $) |has| |#3| (-157))) +(((|#3| |#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971))) (($ $) |has| |#3| (-157))) (|has| |#1| (-947)) ((((-792)) . T)) -(((|#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971))) (($) |has| |#3| (-157))) +(((|#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971))) (($) |has| |#3| (-157))) ((((-522) (-108)) . T)) (((|#1|) |has| |#1| (-285 |#1|))) (|has| |#1| (-343)) @@ -1012,31 +1012,31 @@ (|has| |#1| (-343)) ((((-1085) $) |has| |#1| (-483 (-1085) $)) (($ $) |has| |#1| (-285 $)) ((|#1| |#1|) |has| |#1| (-285 |#1|)) (((-1085) |#1|) |has| |#1| (-483 (-1085) |#1|))) ((((-1085)) |has| |#1| (-829 (-1085)))) -(-3708 (-12 (|has| |#1| (-210)) (|has| |#1| (-338))) (|has| |#1| (-324))) +(-3844 (-12 (|has| |#1| (-210)) (|has| |#1| (-338))) (|has| |#1| (-324))) ((((-363) (-1032)) . T)) (((|#1| |#4|) . T)) (((|#1| |#3|) . T)) ((((-363) |#1|) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) (|has| |#1| (-1014)) ((((-792)) . T)) ((((-792)) . T)) ((((-839 |#1|)) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) (((|#1| |#2|) . T)) ((($) . T)) (((|#1| |#1|) . T)) (((#0=(-799 |#1|)) |has| #0# (-285 #0#))) (((|#1| |#2|) . T)) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) (-12 (|has| |#1| (-730)) (|has| |#2| (-730))) (((|#1|) . T)) (-12 (|has| |#1| (-730)) (|has| |#2| (-730))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (|has| |#1| (-1106)) (((#0=(-522) #0#) . T) ((#1=(-382 (-522)) #1#) . T) (($ $) . T)) ((((-382 (-522))) . T) (($) . T)) @@ -1047,8 +1047,8 @@ (((|#1| |#1|) . T) (($ $) . T) ((#0=(-382 (-522)) #0#) . T)) (|has| |#1| (-338)) ((((-522)) . T) (((-382 (-522))) . T) (($) . T)) -((($ $) . T) ((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1| |#1|) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((($ $) . T) ((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1| |#1|) . T)) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (((|#1|) . T) (($) . T) (((-382 (-522))) . T)) ((((-792)) . T)) ((((-792)) . T)) @@ -1063,14 +1063,14 @@ (((|#1| |#2|) . T)) (|has| |#1| (-782)) (|has| |#1| (-782)) -((($) . T) (((-382 (-522))) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-514))) -(((#0=(-2 (|:| -2530 (-1085)) (|:| -3048 (-51))) #0#) |has| (-2 (|:| -2530 (-1085)) (|:| -3048 (-51))) (-285 (-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))))) +((($) . T) (((-382 (-522))) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-514))) +(((#0=(-2 (|:| -2644 (-1085)) (|:| -3149 (-51))) #0#) |has| (-2 (|:| -2644 (-1085)) (|:| -3149 (-51))) (-285 (-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))))) ((($) . T)) (|has| |#2| (-784)) ((($) . T)) (((|#2|) |has| |#2| (-1014))) -((((-792)) -3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-562 (-792))) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((-1166 |#2|)) . T)) +((((-792)) -3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-562 (-792))) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((-1166 |#2|)) . T)) (|has| |#1| (-784)) (|has| |#1| (-784)) ((((-1068) (-51)) . T)) @@ -1078,10 +1078,10 @@ ((((-792)) . T)) ((((-522)) |has| #0=(-382 |#2|) (-584 (-522))) ((#0#) . T)) ((((-522) (-132)) . T)) -((((-522) (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T) ((|#1| |#2|) . T)) +((((-522) (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T) ((|#1| |#2|) . T)) ((((-382 (-522))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-792)) . T)) ((((-839 |#1|)) . T)) (|has| |#1| (-338)) @@ -1106,31 +1106,31 @@ ((($) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-157))) -((((-522) (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T) ((|#1| |#2|) . T)) +((((-522) (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) ((($) |has| |#1| (-514)) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#3|) . T)) (((|#1|) |has| |#1| (-157))) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838)))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1|) . T)) (((|#1|) . T)) ((((-498)) |has| |#1| (-563 (-498))) (((-821 (-354))) |has| |#1| (-563 (-821 (-354)))) (((-821 (-522))) |has| |#1| (-563 (-821 (-522))))) ((((-792)) . T)) -(((|#2|) . T) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (|has| |#2| (-782)) (-12 (|has| |#2| (-210)) (|has| |#2| (-971))) (|has| |#1| (-514)) (|has| |#1| (-1061)) ((((-1068) |#1|) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) -(((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#1| |#1|) . T)) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#1| |#1|) . T)) ((((-382 (-522))) |has| |#1| (-962 (-522))) (((-522)) |has| |#1| (-962 (-522))) (((-1085)) |has| |#1| (-962 (-1085))) ((|#1|) . T)) ((((-522) |#2|) . T)) ((((-382 (-522))) |has| |#1| (-962 (-382 (-522)))) (((-522)) |has| |#1| (-962 (-522))) ((|#1|) . T)) ((((-522)) |has| |#1| (-815 (-522))) (((-354)) |has| |#1| (-815 (-354)))) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#1|) . T)) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#1|) . T)) (((|#1|) . T)) ((((-588 |#4|)) . T) (((-792)) . T)) ((((-498)) |has| |#4| (-563 (-498)))) @@ -1143,17 +1143,17 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1085)) |has| (-382 |#2|) (-829 (-1085)))) -(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) #0#) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) #0#) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) -((((-792)) -3708 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-562 (-792))) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-343)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971)) (|has| |#3| (-1014))) (((-1166 |#3|)) . T)) +((((-792)) -3844 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-562 (-792))) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-343)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971)) (|has| |#3| (-1014))) (((-1166 |#3|)) . T)) ((((-522) |#2|) . T)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) -(((|#2| |#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($ $) |has| |#2| (-157))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(((|#2| |#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($ $) |has| |#2| (-157))) ((((-792)) . T)) ((((-792)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T) ((|#2|) . T)) ((((-792)) . T)) ((((-792)) . T)) ((((-1068) (-1085) (-522) (-202) (-792)) . T)) @@ -1188,8 +1188,8 @@ (|has| |#1| (-37 (-382 (-522)))) ((((-792)) . T)) ((((-498)) |has| |#1| (-563 (-498)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) -(((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($) |has| |#2| (-157))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +(((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-971))) (($) |has| |#2| (-157))) (|has| $ (-135)) ((((-382 |#2|)) . T)) ((((-382 (-522))) |has| #0=(-382 |#2|) (-962 (-382 (-522)))) (((-522)) |has| #0# (-962 (-522))) ((#0#) . T)) @@ -1200,11 +1200,11 @@ (((|#3|) |has| |#3| (-157))) (|has| |#1| (-135)) (|has| |#1| (-133)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) (|has| |#1| (-135)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) (|has| |#1| (-135)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) (|has| |#1| (-135)) (((|#1|) . T)) (((|#2|) . T)) @@ -1235,7 +1235,7 @@ ((((-925 |#1|)) . T) ((|#1|) . T)) ((((-792)) . T)) ((((-792)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-382 (-522))) . T) (((-382 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1081 |#1|)) . T)) ((((-522)) . T) (($) . T) (((-382 (-522))) . T)) @@ -1243,9 +1243,9 @@ (|has| |#1| (-784)) (((|#2|) . T)) ((((-522)) . T) (($) . T) (((-382 (-522))) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) ((((-522) |#2|) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (((|#2|) . T)) ((((-522) |#3|) . T)) (((|#2|) . T)) @@ -1260,7 +1260,7 @@ (((|#3|) -12 (|has| |#3| (-285 |#3|)) (|has| |#3| (-1014)))) (((|#2|) . T)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) #0#) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) #0#) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (((|#2| |#2|) . T)) (|has| |#2| (-338)) (((|#2|) . T) (((-522)) |has| |#2| (-962 (-522))) (((-382 (-522))) |has| |#2| (-962 (-382 (-522))))) @@ -1290,19 +1290,19 @@ (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1| |#2|) . T)) ((((-522) (-132)) . T)) -(((#0=(-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) #0#) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) -((($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +(((#0=(-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) #0#) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) +((($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (|has| |#1| (-784)) (((|#2| (-708) (-999)) . T)) (((|#1| |#2|) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-514))) (|has| |#1| (-728)) (((|#1|) |has| |#1| (-157))) (((|#4|) . T)) (((|#4|) . T)) (((|#1| |#2|) . T)) -(-3708 (|has| |#1| (-135)) (-12 (|has| |#1| (-338)) (|has| |#2| (-135)))) -(-3708 (|has| |#1| (-133)) (-12 (|has| |#1| (-338)) (|has| |#2| (-133)))) +(-3844 (|has| |#1| (-135)) (-12 (|has| |#1| (-338)) (|has| |#2| (-135)))) +(-3844 (|has| |#1| (-133)) (-12 (|has| |#1| (-338)) (|has| |#2| (-133)))) (((|#4|) . T)) (|has| |#1| (-133)) ((((-1068) |#1|) . T)) @@ -1315,10 +1315,10 @@ (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#3|) . T)) ((((-1158 |#1| |#2| |#3|)) |has| |#1| (-338))) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#1|) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014))) (((-886 |#1|)) . T)) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014))) (((-886 |#1|)) . T)) (|has| |#1| (-782)) (|has| |#1| (-782)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) @@ -1331,8 +1331,8 @@ ((($) . T)) ((((-363) (-1068)) . T)) ((($) |has| |#1| (-514)) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) -((((-792)) -3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-562 (-792))) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((-1166 |#2|)) . T)) -(((#0=(-51)) . T) (((-2 (|:| -2530 (-1068)) (|:| -3048 #0#))) . T)) +((((-792)) -3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-562 (-792))) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((-1166 |#2|)) . T)) +(((#0=(-51)) . T) (((-2 (|:| -2644 (-1068)) (|:| -3149 #0#))) . T)) (((|#1|) . T)) ((((-792)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) @@ -1340,7 +1340,7 @@ (|has| |#2| (-133)) (|has| |#2| (-135)) (|has| |#1| (-447)) -(-3708 (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) (|has| |#1| (-338)) ((((-792)) . T)) (|has| |#1| (-37 (-382 (-522)))) @@ -1349,8 +1349,8 @@ (|has| |#1| (-782)) (|has| |#1| (-782)) ((((-792)) . T)) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-1158 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) -(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514)))) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-1158 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) +(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514)))) ((($) |has| |#1| (-514)) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1| |#2|) . T)) ((((-1085)) |has| |#1| (-829 (-1085)))) @@ -1358,7 +1358,7 @@ ((((-792)) . T)) ((((-792)) . T)) (|has| |#1| (-1014)) -(((|#2| (-455 (-3480 |#1|) (-708)) (-794 |#1|)) . T)) +(((|#2| (-455 (-3591 |#1|) (-708)) (-794 |#1|)) . T)) ((((-382 (-522))) . #0=(|has| |#2| (-338))) (($) . #0#)) (((|#1| (-494 (-1085)) (-1085)) . T)) (((|#1|) . T)) @@ -1378,16 +1378,16 @@ (|has| |#1| (-135)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) . T)) +(((|#1|) . T) (((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) . T)) ((((-1083 |#1| |#2| |#3|)) |has| |#1| (-338))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-1085) (-51)) . T)) ((($ $) . T)) (((|#1| (-522)) . T)) ((((-839 |#1|)) . T)) -(((|#1|) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-971))) (($) -3708 (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)))) +(((|#1|) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-971))) (($) -3844 (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)))) (((|#1|) . T) (((-522)) |has| |#1| (-962 (-522))) (((-382 (-522))) |has| |#1| (-962 (-382 (-522))))) (|has| |#1| (-784)) (|has| |#1| (-784)) @@ -1402,13 +1402,13 @@ (((|#4| |#4|) -12 (|has| |#4| (-285 |#4|)) (|has| |#4| (-1014)))) (((|#1|) |has| |#1| (-157))) (((|#4| |#4|) -12 (|has| |#4| (-285 |#4|)) (|has| |#4| (-1014)))) -(((|#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)))) +(((|#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)))) (|has| |#2| (-784)) (|has| |#1| (-784)) -(-3708 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-838))) ((($ $) . T) ((#0=(-382 (-522)) #0#) . T)) ((((-522) |#2|) . T)) -(((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)))) +(((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)))) (|has| |#1| (-324)) (((|#3| |#3|) -12 (|has| |#3| (-285 |#3|)) (|has| |#3| (-1014)))) ((($) . T) (((-382 (-522))) . T)) @@ -1416,7 +1416,7 @@ (|has| |#1| (-757)) (|has| |#1| (-757)) (((|#1|) . T)) -(-3708 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324))) (|has| |#1| (-782)) (|has| |#1| (-782)) (|has| |#1| (-782)) @@ -1425,13 +1425,13 @@ ((((-522)) . T) (($) . T) (((-382 (-522))) . T)) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) (|has| |#1| (-37 (-382 (-522)))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-1085)) |has| |#1| (-829 (-1085))) (((-999)) . T)) (((|#1|) . T)) (|has| |#1| (-782)) -(((#0=(-2 (|:| -2530 (-1068)) (|:| -3048 (-51))) #0#) |has| (-2 (|:| -2530 (-1068)) (|:| -3048 (-51))) (-285 (-2 (|:| -2530 (-1068)) (|:| -3048 (-51)))))) +(((#0=(-2 (|:| -2644 (-1068)) (|:| -3149 (-51))) #0#) |has| (-2 (|:| -2644 (-1068)) (|:| -3149 (-51))) (-285 (-2 (|:| -2644 (-1068)) (|:| -3149 (-51)))))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (|has| |#1| (-1014)) (((|#1|) . T)) @@ -1449,7 +1449,7 @@ (((|#1|) . T)) ((((-132)) . T)) (((|#2|) |has| |#2| (-157))) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((|#1|) . T)) (|has| |#1| (-133)) (|has| |#1| (-135)) @@ -1471,32 +1471,32 @@ (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014))) ((#0=(-2 (|:| -2530 (-1068)) (|:| -3048 |#1|)) #0#) |has| (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|)) (-285 (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))))) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-838))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-838))) +(((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014))) ((#0=(-2 (|:| -2644 (-1068)) (|:| -3149 |#1|)) #0#) |has| (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|)) (-285 (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-838))) (((|#1|) . T) (($) . T)) (((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) (((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(((|#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)))) +(((|#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)))) (|has| |#1| (-784)) (|has| |#1| (-514)) ((((-535 |#1|)) . T)) ((($) . T)) (((|#2|) . T)) -(-3708 (-12 (|has| |#1| (-338)) (|has| |#2| (-757))) (-12 (|has| |#1| (-338)) (|has| |#2| (-784)))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (-12 (|has| |#1| (-338)) (|has| |#2| (-757))) (-12 (|has| |#1| (-338)) (|has| |#2| (-784)))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) ((((-839 |#1|)) . T)) (((|#1| (-466 |#1| |#3|) (-466 |#1| |#2|)) . T)) (((|#1| |#4| |#5|) . T)) (((|#1| (-708)) . T)) ((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) |has| |#1| (-157)) (($) |has| |#1| (-514))) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-1083 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) -(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514)))) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-1083 |#1| |#2| |#3|)) |has| |#1| (-338)) ((|#1|) |has| |#1| (-157))) +(((|#1|) |has| |#1| (-157)) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514)))) ((($) |has| |#1| (-514)) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) . T)) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) . T)) ((((-382 |#2|)) . T) (((-382 (-522))) . T) (($) . T)) ((((-613 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1504,17 +1504,17 @@ ((((-792)) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) ((((-792)) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) ((((-792)) . T)) ((((-792)) . T)) ((((-792)) . T)) (((|#2|) . T)) -(-3708 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-343)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971)) (|has| |#3| (-1014))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-343)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971)) (|has| |#3| (-1014))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((((-382 (-522))) |has| |#1| (-962 (-382 (-522)))) (((-522)) |has| |#1| (-962 (-522))) ((|#1|) . T)) (|has| |#1| (-1106)) (|has| |#1| (-1106)) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (|has| |#1| (-1106)) (|has| |#1| (-1106)) (((|#3| |#3|) . T)) @@ -1527,43 +1527,43 @@ (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) ((((-1068) (-51)) . T)) (|has| |#1| (-1014)) -(-3708 (|has| |#2| (-757)) (|has| |#2| (-784))) +(-3844 (|has| |#2| (-757)) (|has| |#2| (-784))) (((|#1|) . T)) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) (((-382 (-522))) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) (((-382 (-522))) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) (((|#1|) |has| |#1| (-157)) (($) . T)) ((($) . T)) ((((-1083 |#1| |#2| |#3|)) -12 (|has| (-1083 |#1| |#2| |#3|) (-285 (-1083 |#1| |#2| |#3|))) (|has| |#1| (-338)))) ((((-792)) . T)) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((($) . T)) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) ((((-792)) . T)) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-838))) (|has| |#2| (-838)) (|has| |#1| (-338)) (((|#2|) |has| |#2| (-1014))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((($) . T) ((|#2|) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-838))) (|has| |#1| (-838)) (|has| |#1| (-838)) ((((-498)) . T) (((-382 (-1081 (-522)))) . T) (((-202)) . T) (((-354)) . T)) ((((-354)) . T) (((-202)) . T) (((-792)) . T)) (|has| |#1| (-838)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) ((($ $) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((($ $) . T)) ((((-522) (-108)) . T)) ((($) . T)) (((|#1|) . T)) ((((-522)) . T)) ((((-108)) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (|has| |#1| (-37 (-382 (-522)))) (((|#1| (-522)) . T)) ((($) . T)) @@ -1585,7 +1585,7 @@ (((|#1| (-1130 |#1| |#2| |#3|)) . T)) (((|#1| (-708)) . T)) (((|#1|) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-792)) . T)) (|has| |#1| (-1014)) ((((-1068) |#1|) . T)) @@ -1605,18 +1605,18 @@ (((|#1|) . T)) ((((-522)) . T)) ((((-792)) . T)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-324))) ((((-792)) . T)) (|has| |#1| (-135)) (((|#3|) . T)) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((((-792)) . T)) ((((-1151 |#2| |#3| |#4|)) . T) (((-1152 |#1| |#2| |#3| |#4|)) . T)) ((((-792)) . T)) -((((-47)) -12 (|has| |#1| (-514)) (|has| |#1| (-962 (-522)))) (((-561 $)) . T) ((|#1|) . T) (((-522)) |has| |#1| (-962 (-522))) (((-382 (-522))) -3708 (-12 (|has| |#1| (-514)) (|has| |#1| (-962 (-522)))) (|has| |#1| (-962 (-382 (-522))))) (((-382 (-881 |#1|))) |has| |#1| (-514)) (((-881 |#1|)) |has| |#1| (-971)) (((-1085)) . T)) +((((-47)) -12 (|has| |#1| (-514)) (|has| |#1| (-962 (-522)))) (((-561 $)) . T) ((|#1|) . T) (((-522)) |has| |#1| (-962 (-522))) (((-382 (-522))) -3844 (-12 (|has| |#1| (-514)) (|has| |#1| (-962 (-522)))) (|has| |#1| (-962 (-382 (-522))))) (((-382 (-881 |#1|))) |has| |#1| (-514)) (((-881 |#1|)) |has| |#1| (-971)) (((-1085)) . T)) (((|#1|) . T) (($) . T)) (((|#1| (-708)) . T)) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) |has| |#1| (-157))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) |has| |#1| (-157))) (((|#1|) |has| |#1| (-285 |#1|))) ((((-1152 |#1| |#2| |#3| |#4|)) . T)) ((((-522)) |has| |#1| (-815 (-522))) (((-354)) |has| |#1| (-815 (-354)))) @@ -1624,14 +1624,14 @@ (|has| |#1| (-514)) (((|#1|) . T)) ((((-792)) . T)) -(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (((|#1|) |has| |#1| (-157))) ((($) |has| |#1| (-514)) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) (((|#1|) . T)) (((|#3|) |has| |#3| (-1014))) -(((|#2|) -3708 (|has| |#2| (-157)) (|has| |#2| (-338)))) +(((|#2|) -3844 (|has| |#2| (-157)) (|has| |#2| (-338)))) ((((-1151 |#2| |#3| |#4|)) . T)) ((((-108)) . T)) (|has| |#1| (-757)) @@ -1641,8 +1641,8 @@ (|has| |#1| (-782)) (|has| |#1| (-782)) (((|#1| (-522) (-999)) . T)) -(-3708 (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +(-3844 (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1| (-382 (-522)) (-999)) . T)) (((|#1| (-708) (-999)) . T)) (|has| |#1| (-784)) @@ -1658,28 +1658,28 @@ (((|#1|) . T)) (|has| |#1| (-1014)) ((((-522)) -12 (|has| |#1| (-338)) (|has| |#2| (-584 (-522)))) ((|#2|) |has| |#1| (-338))) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((|#2|) |has| |#2| (-157))) (((|#1|) |has| |#1| (-157))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) ((((-792)) . T)) (|has| |#3| (-782)) ((((-792)) . T)) ((((-1151 |#2| |#3| |#4|) (-294 |#2| |#3| |#4|)) . T)) ((((-792)) . T)) -(((|#1| |#1|) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-971)))) +(((|#1| |#1|) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-971)))) (((|#1|) . T)) ((((-522)) . T)) ((((-522)) . T)) -(((|#1|) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-971)))) +(((|#1|) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-971)))) (((|#2|) |has| |#2| (-338))) ((($) . T) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-338))) (|has| |#1| (-784)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) |has| (-2 (|:| -2530 (-1085)) (|:| -3048 (-51))) (-285 (-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-838))) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) |has| (-2 (|:| -2644 (-1085)) (|:| -3149 (-51))) (-285 (-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-838))) (((|#2|) . T) (((-522)) |has| |#2| (-584 (-522)))) ((((-792)) . T)) ((((-792)) . T)) @@ -1713,18 +1713,18 @@ (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) (((|#1|) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) (((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) . T) (($ $) . T)) ((((-792)) . T)) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) ((($) . T) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (|has| |#1| (-338)) (|has| |#1| (-338)) (|has| (-382 |#2|) (-210)) (|has| |#1| (-838)) (((|#2|) |has| |#2| (-971))) -(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (|has| |#1| (-338)) (((|#1|) |has| |#1| (-157))) (((|#1| |#1|) . T)) @@ -1749,7 +1749,7 @@ (((|#1| (-382 (-522)) (-999)) . T)) (((|#1| (-708) (-999)) . T)) (((#0=(-382 |#2|) #0#) . T) ((#1=(-382 (-522)) #1#) . T) (($ $) . T)) -(((|#1|) . T) (((-522)) -3708 (|has| (-382 (-522)) (-962 (-522))) (|has| |#1| (-962 (-522)))) (((-382 (-522))) . T)) +(((|#1|) . T) (((-522)) -3844 (|has| (-382 (-522)) (-962 (-522))) (|has| |#1| (-962 (-522)))) (((-382 (-522))) . T)) (((|#1| (-553 |#1| |#3|) (-553 |#1| |#2|)) . T)) (((|#1|) |has| |#1| (-157))) (((|#1|) . T)) @@ -1768,24 +1768,24 @@ ((((-637)) . T)) (((|#2|) |has| |#2| (-157))) (|has| |#2| (-782)) -((((-108)) |has| |#1| (-1014)) (((-792)) -3708 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)) (|has| |#1| (-1026)) (|has| |#1| (-1014)))) +((((-108)) |has| |#1| (-1014)) (((-792)) -3844 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)) (|has| |#1| (-1026)) (|has| |#1| (-1014)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 (-51)))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 (-51)))) . T)) ((((-792)) . T)) ((((-522) |#1|) . T)) ((((-637)) . T) (((-382 (-522))) . T) (((-522)) . T)) (((|#1| |#1|) |has| |#1| (-157))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) ((((-354)) . T)) ((((-637)) . T)) ((((-382 (-522))) . #0=(|has| |#2| (-338))) (($) . #0#)) (((|#1|) |has| |#1| (-157))) ((((-382 (-881 |#1|))) . T)) (((|#2| |#2|) . T)) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (((|#2|) . T)) (|has| |#2| (-784)) (((|#3|) |has| |#3| (-971))) @@ -1795,14 +1795,14 @@ (|has| |#1| (-784)) ((((-1085)) |has| |#2| (-829 (-1085)))) ((((-792)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-382 (-522))) . T) (($) . T)) (|has| |#1| (-447)) (|has| |#1| (-343)) (|has| |#1| (-343)) (|has| |#1| (-343)) (|has| |#1| (-338)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-447)) (|has| |#1| (-514)) (|has| |#1| (-971)) (|has| |#1| (-1026))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-447)) (|has| |#1| (-514)) (|has| |#1| (-971)) (|has| |#1| (-1026))) (|has| |#1| (-37 (-382 (-522)))) ((((-112 |#1|)) . T)) ((((-112 |#1|)) . T)) @@ -1823,11 +1823,11 @@ (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-784)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-135)) (|has| |#1| (-133)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)))) ((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)))) ((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) (((|#2|) . T)) (((|#3|) . T)) ((((-112 |#1|)) . T)) @@ -1845,11 +1845,11 @@ ((((-498)) |has| |#1| (-563 (-498))) (((-821 (-522))) |has| |#1| (-563 (-821 (-522)))) (((-821 (-354))) |has| |#1| (-563 (-821 (-354)))) (((-354)) . #0=(|has| |#1| (-947))) (((-202)) . #0#)) (((|#1|) |has| |#1| (-338))) ((((-792)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((($ $) . T) (((-561 $) $) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) ((($) . T) (((-1152 |#1| |#2| |#3| |#4|)) . T) (((-382 (-522))) . T)) -((($) -3708 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-514))) +((($) -3844 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-514))) (|has| |#1| (-338)) (|has| |#1| (-338)) (|has| |#1| (-338)) @@ -1860,11 +1860,11 @@ ((((-354)) . T)) (((|#3|) -12 (|has| |#3| (-285 |#3|)) (|has| |#3| (-1014)))) ((((-792)) . T)) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-838))) (((|#1|) . T)) (|has| |#1| (-784)) (|has| |#1| (-784)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) (((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) (|has| |#1| (-1014)) @@ -1873,13 +1873,13 @@ (|has| |#1| (-133)) (|has| |#1| (-135)) ((((-522)) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((#0=(-1151 |#2| |#3| |#4|)) . T) (((-382 (-522))) |has| #0# (-37 (-382 (-522)))) (($) . T)) ((((-522)) . T)) (|has| |#1| (-338)) -(-3708 (-12 (|has| (-1158 |#1| |#2| |#3|) (-135)) (|has| |#1| (-338))) (|has| |#1| (-135))) -(-3708 (-12 (|has| (-1158 |#1| |#2| |#3|) (-133)) (|has| |#1| (-338))) (|has| |#1| (-133))) +(-3844 (-12 (|has| (-1158 |#1| |#2| |#3|) (-135)) (|has| |#1| (-338))) (|has| |#1| (-135))) +(-3844 (-12 (|has| (-1158 |#1| |#2| |#3|) (-133)) (|has| |#1| (-338))) (|has| |#1| (-133))) (|has| |#1| (-338)) (|has| |#1| (-133)) (|has| |#1| (-135)) @@ -1896,18 +1896,18 @@ (((|#1| |#2|) . T)) (((|#1|) . T) (((-522)) |has| |#1| (-584 (-522)))) (((|#3|) |has| |#3| (-157))) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) ((((-522)) . T)) (((|#1| $) |has| |#1| (-262 |#1| |#1|))) ((((-382 (-522))) . T) (($) . T) (((-382 |#1|)) . T) ((|#1|) . T)) ((((-792)) . T)) (((|#3|) . T)) -(((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-266)) (|has| |#1| (-338))) ((#0=(-382 (-522)) #0#) |has| |#1| (-338))) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) . T)) +(((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-266)) (|has| |#1| (-338))) ((#0=(-382 (-522)) #0#) |has| |#1| (-338))) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) . T)) ((($) . T)) ((((-522) |#1|) . T)) ((((-1085)) |has| (-382 |#2|) (-829 (-1085)))) -(((|#1|) . T) (($) -3708 (|has| |#1| (-266)) (|has| |#1| (-338))) (((-382 (-522))) |has| |#1| (-338))) +(((|#1|) . T) (($) -3844 (|has| |#1| (-266)) (|has| |#1| (-338))) (((-382 (-522))) |has| |#1| (-338))) ((((-498)) |has| |#2| (-563 (-498)))) ((((-628 |#2|)) . T) (((-792)) . T)) (((|#1|) . T)) @@ -1915,8 +1915,8 @@ (((|#4|) -12 (|has| |#4| (-285 |#4|)) (|has| |#4| (-1014)))) ((((-799 |#1|)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) -(-3708 (|has| |#4| (-730)) (|has| |#4| (-782))) -(-3708 (|has| |#3| (-730)) (|has| |#3| (-782))) +(-3844 (|has| |#4| (-730)) (|has| |#4| (-782))) +(-3844 (|has| |#3| (-730)) (|has| |#3| (-782))) ((((-792)) . T)) ((((-792)) . T)) (((|#4|) -12 (|has| |#4| (-285 |#4|)) (|has| |#4| (-1014)))) @@ -1932,17 +1932,17 @@ ((((-382 (-522))) . T) (($) . T)) ((((-382 (-522))) . T) (($) . T)) ((((-382 (-522))) . T) (($) . T)) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-1124))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-1124))) ((($) . T)) ((((-382 (-522))) |has| #0=(-382 |#2|) (-962 (-382 (-522)))) (((-522)) |has| #0# (-962 (-522))) ((#0#) . T)) (((|#2|) . T) (((-522)) |has| |#2| (-584 (-522)))) (((|#1| (-708)) . T)) (|has| |#1| (-784)) (((|#1|) . T) (((-522)) |has| |#1| (-584 (-522)))) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) (((-382 (-522))) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) (((-382 (-522))) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) ((((-522)) . T)) (|has| |#1| (-37 (-382 (-522)))) -((((-2 (|:| -2530 (-1068)) (|:| -3048 (-51)))) |has| (-2 (|:| -2530 (-1068)) (|:| -3048 (-51))) (-285 (-2 (|:| -2530 (-1068)) (|:| -3048 (-51)))))) +((((-2 (|:| -2644 (-1068)) (|:| -3149 (-51)))) |has| (-2 (|:| -2644 (-1068)) (|:| -3149 (-51))) (-285 (-2 (|:| -2644 (-1068)) (|:| -3149 (-51)))))) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (|has| |#1| (-782)) (|has| |#1| (-37 (-382 (-522)))) @@ -1967,24 +1967,24 @@ (((|#1| |#2|) . T)) ((((-132)) . T)) ((((-717 |#1| (-794 |#2|))) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (|has| |#1| (-1106)) (((|#1|) . T)) -(-3708 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-343)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971)) (|has| |#3| (-1014))) +(-3844 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-343)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971)) (|has| |#3| (-1014))) ((((-1085) |#1|) |has| |#1| (-483 (-1085) |#1|))) (((|#2|) . T)) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((((-839 |#1|)) . T)) ((($) . T)) ((((-382 (-881 |#1|))) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) ((((-498)) |has| |#4| (-563 (-498)))) ((((-792)) . T) (((-588 |#4|)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-782)) -(((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014))) (((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) |has| (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|)) (-285 (-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))))) +(((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014))) (((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) |has| (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|)) (-285 (-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))))) (|has| |#1| (-1014)) (|has| |#1| (-338)) (|has| |#1| (-784)) @@ -1992,16 +1992,16 @@ (((|#1|) . T)) (((|#1|) . T)) ((($) . T) (((-382 (-522))) . T)) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) |has| |#1| (-157))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) |has| |#1| (-157))) (|has| |#1| (-133)) (|has| |#1| (-135)) -(-3708 (-12 (|has| (-1083 |#1| |#2| |#3|) (-135)) (|has| |#1| (-338))) (|has| |#1| (-135))) -(-3708 (-12 (|has| (-1083 |#1| |#2| |#3|) (-133)) (|has| |#1| (-338))) (|has| |#1| (-133))) +(-3844 (-12 (|has| (-1083 |#1| |#2| |#3|) (-135)) (|has| |#1| (-338))) (|has| |#1| (-135))) +(-3844 (-12 (|has| (-1083 |#1| |#2| |#3|) (-133)) (|has| |#1| (-338))) (|has| |#1| (-133))) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-135)) (|has| |#1| (-133)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) ((((-1158 |#1| |#2| |#3|)) |has| |#1| (-338))) (|has| |#1| (-782)) (((|#1| |#2|) . T)) @@ -2024,9 +2024,9 @@ ((((-792)) . T)) ((((-792)) . T)) ((((-498)) |has| |#1| (-563 (-498)))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-1085) |#1|) |has| |#1| (-483 (-1085) |#1|)) ((|#1| |#1|) |has| |#1| (-285 |#1|))) -(((|#1|) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)))) +(((|#1|) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)))) ((((-291 |#1|)) . T)) (((|#2|) |has| |#2| (-338))) (((|#2|) . T)) @@ -2047,14 +2047,14 @@ (|has| |#1| (-133)) (|has| |#1| (-135)) ((($ $) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)) (|has| |#1| (-1026)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)) (|has| |#1| (-1026)) (|has| |#1| (-1014))) (|has| |#1| (-514)) (((|#2|) . T)) ((((-522)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) ((((-535 |#1|)) . T)) ((($) . T)) (((|#1| (-57 |#1|) (-57 |#1|)) . T)) @@ -2079,12 +2079,12 @@ (((|#1| |#2|) . T)) ((((-1085) |#1|) . T)) (((|#4|) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((((-1085) (-51)) . T)) ((((-1151 |#2| |#3| |#4|) (-294 |#2| |#3| |#4|)) . T)) ((((-382 (-522))) |has| |#1| (-962 (-382 (-522)))) (((-522)) |has| |#1| (-962 (-522))) ((|#1|) . T)) ((((-792)) . T)) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-343)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971)) (|has| |#2| (-1014))) (((#0=(-1152 |#1| |#2| |#3| |#4|) #0#) . T) ((#1=(-382 (-522)) #1#) . T) (($ $) . T)) (((|#1| |#1|) |has| |#1| (-157)) ((#0=(-382 (-522)) #0#) |has| |#1| (-514)) (($ $) |has| |#1| (-514))) (((|#1|) . T) (($) . T) (((-382 (-522))) . T)) @@ -2103,14 +2103,14 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) (((|#2| |#3|) . T)) -(-3708 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-338)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) (((|#1| (-494 |#2|)) . T)) (((|#1| (-708)) . T)) (((|#1| (-494 (-1004 (-1085)))) . T)) (((|#1|) |has| |#1| (-157))) (((|#1|) . T)) (|has| |#2| (-838)) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) ((((-792)) . T)) ((($ $) . T) ((#0=(-1151 |#2| |#3| |#4|) #0#) . T) ((#1=(-382 (-522)) #1#) |has| #0# (-37 (-382 (-522))))) ((((-839 |#1|)) . T)) @@ -2119,13 +2119,13 @@ ((($) . T)) ((($) . T)) (|has| |#1| (-338)) -(-3708 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324)) (|has| |#1| (-514))) (|has| |#1| (-338)) ((($) . T) ((#0=(-1151 |#2| |#3| |#4|)) . T) (((-382 (-522))) |has| #0# (-37 (-382 (-522))))) (((|#1| |#2|) . T)) ((((-1083 |#1| |#2| |#3|)) |has| |#1| (-338))) -(-3708 (-12 (|has| |#1| (-283)) (|has| |#1| (-838))) (|has| |#1| (-338)) (|has| |#1| (-324))) -(-3708 (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) +(-3844 (-12 (|has| |#1| (-283)) (|has| |#1| (-838))) (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-829 (-1085))) (|has| |#1| (-971))) ((((-522)) |has| |#1| (-584 (-522))) ((|#1|) . T)) (((|#1| |#2|) . T)) ((((-792)) . T)) @@ -2157,27 +2157,27 @@ (((|#1|) |has| |#1| (-157))) ((((-792)) . T)) (((|#4| |#4|) -12 (|has| |#4| (-285 |#4|)) (|has| |#4| (-1014)))) -(((|#2|) -3708 (|has| |#2| (-6 (-4240 "*"))) (|has| |#2| (-157)))) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(((|#2|) -3844 (|has| |#2| (-6 (-4240 "*"))) (|has| |#2| (-157)))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (|has| |#2| (-784)) (|has| |#2| (-838)) (|has| |#1| (-838)) (((|#2|) |has| |#2| (-157))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-1158 |#1| |#2| |#3|)) |has| |#1| (-338))) ((((-792)) . T)) ((((-792)) . T)) ((((-498)) . T) (((-522)) . T) (((-821 (-522))) . T) (((-354)) . T) (((-202)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 (-51)))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 (-51)))) . T)) (((|#1|) . T)) ((((-792)) . T)) (((|#1| |#2|) . T)) (((|#1| (-382 (-522))) . T)) (((|#1|) . T)) -(-3708 (|has| |#1| (-266)) (|has| |#1| (-338))) +(-3844 (|has| |#1| (-266)) (|has| |#1| (-338))) ((((-132)) . T)) ((((-382 |#2|)) . T) (((-382 (-522))) . T) (($) . T)) (|has| |#1| (-782)) @@ -2192,7 +2192,7 @@ ((((-382 (-522))) . T) (($) . T)) ((((-792)) . T)) ((((-792)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-792)) . T)) ((((-792)) . T)) @@ -2203,7 +2203,7 @@ (((|#1|) . T)) ((((-588 (-132))) . T) (((-1068)) . T)) ((((-792)) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) ((((-1085) |#1|) |has| |#1| (-483 (-1085) |#1|)) ((|#1| |#1|) |has| |#1| (-285 |#1|))) (|has| |#1| (-784)) ((((-792)) . T)) @@ -2215,16 +2215,16 @@ ((((-792)) . T) (((-588 |#4|)) . T)) (((|#2|) . T)) ((((-839 |#1|)) . T) (((-382 (-522))) . T) (($) . T)) -(-3708 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((((-1085) (-51)) . T)) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-782)) (|has| |#2| (-971))) (|has| |#1| (-838)) (|has| |#1| (-838)) (((|#2|) . T)) @@ -2239,12 +2239,12 @@ (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (|has| |#1| (-757)) (((#0=(-839 |#1|) #0#) . T) (($ $) . T) ((#1=(-382 (-522)) #1#) . T)) ((((-382 |#2|)) . T)) (|has| |#1| (-782)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) . T) ((#1=(-522) #1#) . T) (($ $) . T)) ((((-839 |#1|)) . T) (($) . T) (((-382 (-522))) . T)) (((|#2|) |has| |#2| (-971)) (((-522)) -12 (|has| |#2| (-584 (-522))) (|has| |#2| (-971)))) @@ -2254,25 +2254,25 @@ (|has| |#1| (-133)) (((|#2|) . T)) ((((-792)) . T)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) . T)) -(((#0=(-51)) . T) (((-2 (|:| -2530 (-1085)) (|:| -3048 #0#))) . T)) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -2644 (-1085)) (|:| -3149 #0#))) . T)) (|has| |#1| (-324)) ((((-522)) . T)) ((((-792)) . T)) (((#0=(-1152 |#1| |#2| |#3| |#4|) $) |has| #0# (-262 #0# #0#))) (|has| |#1| (-338)) (((#0=(-999) |#1|) . T) ((#0# $) . T) (($ $) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) (((#0=(-382 (-522)) #0#) . T) ((#1=(-637) #1#) . T) (($ $) . T)) ((((-291 |#1|)) . T) (($) . T)) (((|#1|) . T) (((-382 (-522))) |has| |#1| (-338))) (|has| |#1| (-1014)) (((|#1|) . T)) -(((|#1|) -3708 (|has| |#2| (-342 |#1|)) (|has| |#2| (-392 |#1|)))) -(((|#1|) -3708 (|has| |#2| (-342 |#1|)) (|has| |#2| (-392 |#1|)))) +(((|#1|) -3844 (|has| |#2| (-342 |#1|)) (|has| |#2| (-392 |#1|)))) +(((|#1|) -3844 (|has| |#2| (-342 |#1|)) (|has| |#2| (-392 |#1|)))) (((|#2|) . T)) ((((-382 (-522))) . T) (((-637)) . T) (($) . T)) (((|#3| |#3|) . T)) @@ -2291,7 +2291,7 @@ (((|#2|) . T)) (((|#1|) . T)) ((((-522)) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (((|#2|) . T) (((-522)) |has| |#2| (-584 (-522)))) (((|#1| |#2|) . T)) ((($) . T)) @@ -2328,7 +2328,7 @@ (|has| |#2| (-947)) ((($) . T)) (|has| |#1| (-838)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2336,24 +2336,24 @@ ((($) . T)) (|has| |#1| (-338)) ((((-839 |#1|)) . T)) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((($ $) . T) ((#0=(-382 (-522)) #0#) . T)) -(-3708 (|has| |#1| (-343)) (|has| |#1| (-784))) +(-3844 (|has| |#1| (-343)) (|has| |#1| (-784))) (((|#1|) . T)) ((((-792)) . T)) ((((-1085)) -12 (|has| |#1| (-15 * (|#1| (-382 (-522)) |#1|))) (|has| |#1| (-829 (-1085))))) ((((-382 |#2|) |#3|) . T)) ((($) . T) (((-382 (-522))) . T)) ((((-708) |#1|) . T)) -(((|#2| (-217 (-3480 |#1|) (-708))) . T)) +(((|#2| (-217 (-3591 |#1|) (-708))) . T)) (((|#1| (-494 |#3|)) . T)) ((((-382 (-522))) . T)) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((((-792)) . T)) -(((#0=(-2 (|:| -2530 (-1085)) (|:| -3048 (-51))) #0#) |has| (-2 (|:| -2530 (-1085)) (|:| -3048 (-51))) (-285 (-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))))) +(((#0=(-2 (|:| -2644 (-1085)) (|:| -3149 (-51))) #0#) |has| (-2 (|:| -2644 (-1085)) (|:| -3149 (-51))) (-285 (-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))))) (|has| |#1| (-838)) (|has| |#2| (-338)) -(-3708 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((((-154 (-354))) . T) (((-202)) . T) (((-354)) . T)) ((((-792)) . T)) (((|#1|) . T)) @@ -2370,11 +2370,11 @@ (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) -(-3708 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324))) (|has| |#1| (-37 (-382 (-522)))) (-12 (|has| |#1| (-507)) (|has| |#1| (-765))) ((((-792)) . T)) -((((-1085)) -3708 (-12 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (|has| |#1| (-829 (-1085)))) (-12 (|has| |#1| (-338)) (|has| |#2| (-829 (-1085)))))) +((((-1085)) -3844 (-12 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (|has| |#1| (-829 (-1085)))) (-12 (|has| |#1| (-338)) (|has| |#2| (-829 (-1085)))))) (|has| |#1| (-338)) ((((-1085)) -12 (|has| |#1| (-15 * (|#1| (-382 (-522)) |#1|))) (|has| |#1| (-829 (-1085))))) (|has| |#1| (-338)) @@ -2384,7 +2384,7 @@ (((|#1|) . T)) (((|#2|) |has| |#1| (-338))) (((|#2|) |has| |#1| (-338))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-157))) (((|#1|) . T)) @@ -2407,31 +2407,31 @@ (((|#2|) |has| |#1| (-338))) ((((-354)) -12 (|has| |#1| (-338)) (|has| |#2| (-815 (-354)))) (((-522)) -12 (|has| |#1| (-338)) (|has| |#2| (-815 (-522))))) (|has| |#1| (-338)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (|has| |#1| (-338)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) (|has| |#1| (-338)) (|has| |#1| (-514)) (((|#4| |#4|) -12 (|has| |#4| (-285 |#4|)) (|has| |#4| (-1014)))) (((|#3|) . T)) (((|#1|) . T)) -(-3708 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) (((|#2|) . T)) (((|#2|) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (|has| |#1| (-37 (-382 (-522)))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-382 (-522)))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) (|has| |#1| (-135)) ((((-1068) |#1|) . T)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) (|has| |#1| (-135)) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-343))) (|has| |#1| (-135)) ((((-535 |#1|)) . T)) ((($) . T)) @@ -2439,7 +2439,7 @@ (|has| |#1| (-514)) (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-37 (-382 (-522)))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-324))) (|has| |#1| (-135)) ((((-792)) . T)) ((($) . T)) @@ -2464,7 +2464,7 @@ (|has| |#1| (-728)) (|has| |#1| (-728)) ((((-498)) |has| |#1| (-563 (-498)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-110)) . T) ((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2484,7 +2484,7 @@ ((((-522)) . T)) ((((-792)) . T)) ((((-522)) . T)) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) ((((-154 (-354))) . T) (((-202)) . T) (((-354)) . T)) ((((-792)) . T)) ((((-792)) . T)) @@ -2496,9 +2496,9 @@ (((|#1|) . T) (($) . T) (((-382 (-522))) . T)) (|has| |#1| (-338)) (|has| |#1| (-338)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)) (|has| |#1| (-1026)) (|has| |#1| (-1014))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-447)) (|has| |#1| (-664)) (|has| |#1| (-829 (-1085))) (|has| |#1| (-971)) (|has| |#1| (-1026)) (|has| |#1| (-1014))) (|has| |#1| (-1061)) ((((-522) |#1|) . T)) (((|#1|) . T)) @@ -2516,8 +2516,8 @@ (((|#1|) . T)) (|has| |#1| (-514)) ((((-382 |#2|)) . T) (((-382 (-522))) . T) (($) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) ((((-354)) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2526,7 +2526,7 @@ (|has| |#1| (-514)) (|has| |#1| (-1014)) ((((-717 |#1| (-794 |#2|))) |has| (-717 |#1| (-794 |#2|)) (-285 (-717 |#1| (-794 |#2|))))) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) (((|#1|) . T)) (((|#2| |#3|) . T)) (|has| |#2| (-838)) @@ -2536,12 +2536,12 @@ (|has| |#1| (-210)) (((|#1| (-494 (-1004 (-1085)))) . T)) (|has| |#2| (-338)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 (-51)))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 (-51)))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) ((((-792)) . T)) ((((-792)) . T)) -(-3708 (|has| |#3| (-730)) (|has| |#3| (-782))) +(-3844 (|has| |#3| (-730)) (|has| |#3| (-782))) ((((-792)) . T)) ((((-792)) . T)) (((|#1|) . T)) @@ -2550,8 +2550,8 @@ ((((-522)) . T)) (((|#3|) . T)) ((((-792)) . T)) -(-3708 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324))) -(-3708 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) +(-3844 (|has| |#1| (-283)) (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-157)) (|has| |#1| (-514)) (|has| |#1| (-971))) (((#0=(-535 |#1|) #0#) . T) (($ $) . T) ((#1=(-382 (-522)) #1#) . T)) ((($ $) . T) ((#0=(-382 (-522)) #0#) . T)) (((|#1|) |has| |#1| (-157))) @@ -2564,7 +2564,7 @@ (((|#1|) . T)) ((((-792)) |has| |#1| (-562 (-792)))) ((((-270 |#3|)) . T)) -(((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522)))) ((|#2| |#2|) . T) (($ $) -3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +(((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522)))) ((|#2| |#2|) . T) (($ $) -3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) (((|#2| |#2|) . T) ((|#6| |#6|) . T)) (((|#1|) . T)) ((($) . T) (((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T)) @@ -2572,20 +2572,20 @@ (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) (((|#1|) . T) (((-382 (-522))) . T) (($) . T)) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) (((|#2|) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T) (($) -3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T) (($) -3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) (((|#2|) . T) ((|#6|) . T)) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) ((((-792)) . T)) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (|has| |#2| (-838)) (|has| |#1| (-838)) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1|) . T)) -((((-2 (|:| -2530 (-1068)) (|:| -3048 |#1|))) . T)) +((((-2 (|:| -2644 (-1068)) (|:| -3149 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) . T)) @@ -2599,10 +2599,10 @@ (((|#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014)))) (((#0=(-382 (-522)) #0#) . T)) ((((-382 (-522))) . T)) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) (((|#1|) . T)) (((|#1|) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((((-498)) . T)) ((((-792)) . T)) ((((-1085)) |has| |#2| (-829 (-1085))) (((-999)) . T)) @@ -2616,12 +2616,12 @@ ((($ $) . T) ((#0=(-382 (-522)) #0#) . T)) ((((-1085)) |has| |#1| (-829 (-1085)))) ((((-839 |#1|)) . T) (((-382 (-522))) . T) (($) . T)) -((($) . T) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) . T)) -(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-514)))) +((($) . T) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#1|) . T)) +(((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522)))) ((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-514)))) ((($) . T) (((-382 (-522))) . T)) (((|#1|) . T) (((-382 (-522))) . T) (((-522)) . T) (($) . T)) (((|#2|) |has| |#2| (-971)) (((-522)) -12 (|has| |#2| (-584 (-522))) (|has| |#2| (-971)))) -((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-514)))) +((((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-514)))) (|has| |#1| (-514)) (((|#1|) |has| |#1| (-338))) ((((-522)) . T)) @@ -2640,8 +2640,8 @@ ((((-792)) . T)) (|has| |#2| (-757)) (|has| |#2| (-757)) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#2|) |has| |#1| (-338)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) . T)) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#2|) |has| |#1| (-338)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1|) . T) (((-522)) |has| |#1| (-962 (-522))) (((-382 (-522))) |has| |#1| (-962 (-382 (-522))))) ((((-522)) |has| |#1| (-815 (-522))) (((-354)) |has| |#1| (-815 (-354)))) @@ -2667,12 +2667,12 @@ (((|#2| (-708)) . T)) ((((-1085)) . T)) ((((-799 |#1|)) . T)) -(-3708 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971))) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((((-792)) . T)) (((|#1|) . T)) -(-3708 (|has| |#2| (-730)) (|has| |#2| (-782))) -(-3708 (-12 (|has| |#1| (-730)) (|has| |#2| (-730))) (-12 (|has| |#1| (-784)) (|has| |#2| (-784)))) +(-3844 (|has| |#2| (-730)) (|has| |#2| (-782))) +(-3844 (-12 (|has| |#1| (-730)) (|has| |#2| (-730))) (-12 (|has| |#1| (-784)) (|has| |#2| (-784)))) ((((-799 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-343)) @@ -2698,7 +2698,7 @@ (((|#1|) . T)) ((((-792)) . T)) (|has| |#2| (-838)) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) . T)) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) . T)) ((((-498)) |has| |#2| (-563 (-498))) (((-821 (-354))) |has| |#2| (-563 (-821 (-354)))) (((-821 (-522))) |has| |#2| (-563 (-821 (-522))))) ((((-792)) . T)) ((((-792)) . T)) @@ -2731,11 +2731,11 @@ ((((-382 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1014)) -(((|#2| (-455 (-3480 |#1|) (-708))) . T)) +(((|#2| (-455 (-3591 |#1|) (-708))) . T)) ((((-522) |#1|) . T)) (((|#2| |#2|) . T)) (((|#1| (-494 (-1085))) . T)) -(-3708 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((((-522)) . T)) (((|#2|) . T)) (((|#2|) . T)) @@ -2745,9 +2745,9 @@ ((($) . T) (((-382 (-522))) . T)) ((($) . T)) ((($) . T)) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) (((|#1|) . T)) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((((-792)) . T)) ((((-132)) . T)) (((|#1|) . T) (((-382 (-522))) . T)) @@ -2787,27 +2787,27 @@ (|has| |#1| (-210)) (((|#1| (-494 |#3|)) . T)) (|has| |#1| (-343)) -(((|#2| (-217 (-3480 |#1|) (-708))) . T)) +(((|#2| (-217 (-3591 |#1|) (-708))) . T)) (|has| |#1| (-343)) (|has| |#1| (-343)) (((|#1|) . T) (($) . T)) (((|#1| (-494 |#2|)) . T)) -(-3708 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) (((|#1| (-708)) . T)) (|has| |#1| (-514)) -(-3708 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-782)) (|has| |#2| (-971))) (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) ((((-792)) . T)) -(-3708 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-730)) (|has| |#2| (-730)))) -(-3708 (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971))) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-730)) (|has| |#2| (-730)))) +(-3844 (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) (((|#1|) |has| |#1| (-157))) (((|#4|) |has| |#4| (-971))) (((|#3|) |has| |#3| (-971))) (-12 (|has| |#1| (-338)) (|has| |#2| (-757))) (-12 (|has| |#1| (-338)) (|has| |#2| (-757))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) ((((-382 |#2|)) . T) (((-382 (-522))) . T) (($) . T)) ((($ $) . T) ((#0=(-382 (-522)) #0#) . T)) @@ -2820,14 +2820,14 @@ (((|#2|) |has| |#2| (-971)) (((-522)) -12 (|has| |#2| (-584 (-522))) (|has| |#2| (-971)))) (((|#1|) . T)) (|has| |#2| (-338)) -(((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522)))) ((|#2| |#2|) . T) (($ $) -3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) +(((#0=(-382 (-522)) #0#) |has| |#2| (-37 (-382 (-522)))) ((|#2| |#2|) . T) (($ $) -3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1| |#1|) . T) ((#0=(-382 (-522)) #0#) |has| |#1| (-37 (-382 (-522))))) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-382 (-522)) #0#) . T)) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-382 (-522)) #0#) . T)) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-382 (-522)) #0#) . T)) (((|#2| |#2|) . T)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T) (($) -3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T) (($) -3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#1|) . T) (($) . T) (((-382 (-522))) . T)) (((|#1|) . T) (($) . T) (((-382 (-522))) . T)) (((|#1|) . T) (($) . T) (((-382 (-522))) . T)) @@ -2846,25 +2846,25 @@ (((|#1|) |has| |#2| (-392 |#1|))) (((|#1|) |has| |#2| (-392 |#1|))) ((((-839 |#1|)) . T) (((-382 (-522))) . T) (($) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) ((((-792)) . T)) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) |has| (-2 (|:| -2530 (-1085)) (|:| -3048 (-51))) (-285 (-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))))) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) |has| (-2 (|:| -2644 (-1085)) (|:| -3149 (-51))) (-285 (-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) ((((-522) |#1|) . T)) ((((-522) |#1|) . T)) ((((-522) |#1|) . T)) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((((-522) |#1|) . T)) (((|#1|) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((((-1085)) |has| |#1| (-829 (-1085))) (((-755 (-1085))) . T)) -(-3708 (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#3| (-124)) (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-730)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((((-756 |#1|)) . T)) (((|#1| |#2|) . T)) ((((-792)) . T)) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-382 (-522)))) ((((-792)) . T)) @@ -2872,15 +2872,15 @@ (((|#1|) |has| |#1| (-157)) (($) |has| |#1| (-514)) (((-382 (-522))) |has| |#1| (-514))) (((|#2|) . T) (((-522)) |has| |#2| (-584 (-522)))) (|has| |#1| (-338)) -(-3708 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (-12 (|has| |#1| (-338)) (|has| |#2| (-210)))) +(-3844 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (-12 (|has| |#1| (-338)) (|has| |#2| (-210)))) (|has| |#1| (-15 * (|#1| (-382 (-522)) |#1|))) (|has| |#1| (-338)) (((|#1|) . T)) -(((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#1| |#1|) . T)) +(((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#1| |#1|) . T)) ((((-522) |#1|) . T)) ((((-291 |#1|)) . T)) (((#0=(-637) (-1081 #0#)) . T)) -((((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#1|) . T)) +((((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (|has| |#1| (-782)) ((($ $) . T) ((#0=(-794 |#1|) $) . T) ((#0# |#2|) . T)) @@ -2897,12 +2897,12 @@ (((#0=(-1152 |#1| |#2| |#3| |#4|)) |has| #0# (-285 #0#))) ((($) . T)) (((|#1|) . T)) -((($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#2| |#2|) |has| |#1| (-338)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) +((($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#2| |#2|) |has| |#1| (-338)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) ((#0=(-382 (-522)) #0#) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) (|has| |#2| (-210)) (|has| $ (-135)) ((((-792)) . T)) -((($) . T) (((-382 (-522))) -3708 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) +((($) . T) (((-382 (-522))) -3844 (|has| |#1| (-338)) (|has| |#1| (-324))) ((|#1|) . T)) ((((-792)) . T)) (|has| |#1| (-782)) ((((-1085)) -12 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (|has| |#1| (-829 (-1085))))) @@ -2914,23 +2914,23 @@ (((|#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#4|) . T)) (|has| |#1| (-514)) -((($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#2|) |has| |#1| (-338)) ((|#1|) . T)) -((((-1085)) -3708 (-12 (|has| (-1158 |#1| |#2| |#3|) (-829 (-1085))) (|has| |#1| (-338))) (-12 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (|has| |#1| (-829 (-1085)))))) -(((|#1|) . T) (($) -3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3708 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) +((($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338))) ((|#2|) |has| |#1| (-338)) ((|#1|) . T)) +((((-1085)) -3844 (-12 (|has| (-1158 |#1| |#2| |#3|) (-829 (-1085))) (|has| |#1| (-338))) (-12 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (|has| |#1| (-829 (-1085)))))) +(((|#1|) . T) (($) -3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-514))) (((-382 (-522))) -3844 (|has| |#1| (-37 (-382 (-522)))) (|has| |#1| (-338)))) ((((-1085)) -12 (|has| |#1| (-15 * (|#1| (-382 (-522)) |#1|))) (|has| |#1| (-829 (-1085))))) ((((-1085)) -12 (|has| |#1| (-15 * (|#1| (-708) |#1|))) (|has| |#1| (-829 (-1085))))) (((|#4|) -12 (|has| |#4| (-285 |#4|)) (|has| |#4| (-1014)))) ((((-522) |#1|) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) (((|#1|) . T)) (((|#1| (-494 (-755 (-1085)))) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (((|#1|) . T)) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) (((|#1|) . T)) -(-3708 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) -(-3708 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-730)) (|has| |#2| (-730)))) +(-3844 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-730)) (|has| |#2| (-730)))) ((((-1158 |#1| |#2| |#3|)) |has| |#1| (-338))) ((($) . T) (((-799 |#1|)) . T) (((-382 (-522))) . T)) ((((-1158 |#1| |#2| |#3|)) |has| |#1| (-338))) @@ -2939,15 +2939,15 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-382 |#2|)) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (((|#1|) . T)) (((|#2| |#2|) . T) ((#0=(-382 (-522)) #0#) . T) (($ $) . T)) ((((-522)) . T)) @@ -2976,32 +2976,32 @@ ((((-1158 |#1| |#2| |#3|)) |has| |#1| (-338))) ((((-1085)) . T) (((-792)) . T)) (|has| |#1| (-338)) -((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) +((((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) |has| |#2| (-157)) (($) -3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838)))) (((|#2|) . T) ((|#6|) . T)) ((($) . T) (((-382 (-522))) |has| |#2| (-37 (-382 (-522)))) ((|#2|) . T)) -((($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) -((($) -3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) ((((-1018)) . T)) ((((-792)) . T)) ((($) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522)))) ((|#1|) . T)) ((($) . T)) -((($) -3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) +((($) -3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((|#1|) |has| |#1| (-157)) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (|has| |#2| (-838)) (|has| |#1| (-838)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) |has| |#1| (-157))) ((((-637)) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (((|#1|) |has| |#1| (-157))) (((|#1|) |has| |#1| (-157))) ((((-382 (-522))) . T) (($) . T)) (((|#1| (-522)) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) (|has| |#1| (-338)) (|has| |#1| (-338)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) -(-3708 (|has| |#1| (-157)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-157)) (|has| |#1| (-514))) (((|#1| (-522)) . T)) (((|#1| (-382 (-522))) . T)) (((|#1| (-708)) . T)) @@ -3016,16 +3016,16 @@ ((((-821 (-354))) . T) (((-821 (-522))) . T) (((-1085)) . T) (((-498)) . T)) (((|#1|) . T)) ((((-792)) . T)) -(-3708 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) -(-3708 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-730)) (|has| |#2| (-730)))) +(-3844 (|has| |#2| (-124)) (|has| |#2| (-157)) (|has| |#2| (-338)) (|has| |#2| (-730)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-730)) (|has| |#2| (-730)))) ((((-522)) . T)) ((((-522)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) -(-3708 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) +(-3844 (|has| |#2| (-157)) (|has| |#2| (-782)) (|has| |#2| (-971))) ((((-1085)) -12 (|has| |#2| (-829 (-1085))) (|has| |#2| (-971)))) -(-3708 (-12 (|has| |#1| (-447)) (|has| |#2| (-447))) (-12 (|has| |#1| (-664)) (|has| |#2| (-664)))) +(-3844 (-12 (|has| |#1| (-447)) (|has| |#2| (-447))) (-12 (|has| |#1| (-664)) (|has| |#2| (-664)))) (|has| |#1| (-133)) (|has| |#1| (-135)) (|has| |#1| (-338)) @@ -3049,7 +3049,7 @@ ((((-1068) (-1085) (-522) (-202) (-792)) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) -(-3708 (|has| |#1| (-324)) (|has| |#1| (-343))) +(-3844 (|has| |#1| (-324)) (|has| |#1| (-343))) (((|#1| |#2|) . T)) ((($) . T) ((|#1|) . T)) ((((-792)) . T)) @@ -3057,7 +3057,7 @@ ((($) . T) ((|#1|) . T) (((-382 (-522))) |has| |#1| (-37 (-382 (-522))))) (((|#2|) |has| |#2| (-1014)) (((-522)) -12 (|has| |#2| (-962 (-522))) (|has| |#2| (-1014))) (((-382 (-522))) -12 (|has| |#2| (-962 (-382 (-522)))) (|has| |#2| (-1014)))) ((((-498)) |has| |#1| (-563 (-498)))) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-784)) (|has| |#1| (-1014)))) ((($) . T) (((-382 (-522))) . T)) (|has| |#1| (-838)) (|has| |#1| (-838)) @@ -3066,14 +3066,14 @@ ((((-792)) . T)) (((|#2| |#2|) . T)) (((|#1| |#1|) |has| |#1| (-157))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-514))) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-782))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-514))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-782))) (((|#2|) . T)) -(-3708 (|has| |#1| (-21)) (|has| |#1| (-782))) +(-3844 (|has| |#1| (-21)) (|has| |#1| (-782))) (((|#1|) |has| |#1| (-157))) (((|#1|) . T)) (((|#1|) . T)) -((((-792)) -3708 (-12 (|has| |#1| (-562 (-792))) (|has| |#2| (-562 (-792)))) (-12 (|has| |#1| (-1014)) (|has| |#2| (-1014))))) +((((-792)) -3844 (-12 (|has| |#1| (-562 (-792))) (|has| |#2| (-562 (-792)))) (-12 (|has| |#1| (-1014)) (|has| |#2| (-1014))))) ((((-382 |#2|) |#3|) . T)) ((((-382 (-522))) . T) (($) . T)) (|has| |#1| (-37 (-382 (-522)))) @@ -3085,17 +3085,17 @@ (((|#1|) . T) (((-382 (-522))) . T) (((-522)) . T) (($) . T)) (((#0=(-522) #0#) . T)) ((($) . T) (((-382 (-522))) . T)) -(-3708 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) -(-3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) +(-3844 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) +(-3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) (|has| |#4| (-730)) -(-3708 (|has| |#4| (-730)) (|has| |#4| (-782))) +(-3844 (|has| |#4| (-730)) (|has| |#4| (-782))) (|has| |#4| (-782)) (|has| |#3| (-730)) -(-3708 (|has| |#3| (-730)) (|has| |#3| (-782))) +(-3844 (|has| |#3| (-730)) (|has| |#3| (-782))) (|has| |#3| (-782)) ((((-522)) . T)) (((|#2|) . T)) -((((-1085)) -3708 (-12 (|has| (-1083 |#1| |#2| |#3|) (-829 (-1085))) (|has| |#1| (-338))) (-12 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (|has| |#1| (-829 (-1085)))))) +((((-1085)) -3844 (-12 (|has| (-1083 |#1| |#2| |#3|) (-829 (-1085))) (|has| |#1| (-338))) (-12 (|has| |#1| (-15 * (|#1| (-522) |#1|))) (|has| |#1| (-829 (-1085)))))) ((((-1085)) -12 (|has| |#1| (-15 * (|#1| (-382 (-522)) |#1|))) (|has| |#1| (-829 (-1085))))) ((((-1085)) -12 (|has| |#1| (-15 * (|#1| (-708) |#1|))) (|has| |#1| (-829 (-1085))))) (((|#1| |#1|) . T) (($ $) . T)) @@ -3110,11 +3110,11 @@ ((((-1083 |#1| |#2| |#3|)) |has| |#1| (-338))) ((((-1083 |#1| |#2| |#3|)) |has| |#1| (-338))) ((((-1050 |#1| |#2|)) . T)) -(((|#2|) . T) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) . T)) +(((|#2|) . T) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) . T)) ((($) . T)) (|has| |#1| (-947)) -(((|#2|) . T) (((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) ((((-792)) . T)) ((((-498)) |has| |#2| (-563 (-498))) (((-821 (-522))) |has| |#2| (-563 (-821 (-522)))) (((-821 (-354))) |has| |#2| (-563 (-821 (-354)))) (((-354)) . #0=(|has| |#2| (-947))) (((-202)) . #0#)) ((((-1085) (-51)) . T)) @@ -3126,15 +3126,15 @@ ((((-1083 |#1| |#2| |#3|)) . T)) ((((-1083 |#1| |#2| |#3|)) . T) (((-1076 |#1| |#2| |#3|)) . T)) ((((-792)) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) ((((-522) |#1|) . T)) ((((-1083 |#1| |#2| |#3|)) |has| |#1| (-338))) (((|#1| |#2| |#3| |#4|) . T)) (((|#1|) . T)) (((|#2|) . T)) (|has| |#2| (-338)) -(((|#3|) . T) ((|#2|) . T) (($) -3708 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) ((|#4|) -3708 (|has| |#4| (-157)) (|has| |#4| (-338)) (|has| |#4| (-971)))) -(((|#2|) . T) (($) -3708 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((|#3|) -3708 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971)))) +(((|#3|) . T) ((|#2|) . T) (($) -3844 (|has| |#4| (-157)) (|has| |#4| (-782)) (|has| |#4| (-971))) ((|#4|) -3844 (|has| |#4| (-157)) (|has| |#4| (-338)) (|has| |#4| (-971)))) +(((|#2|) . T) (($) -3844 (|has| |#3| (-157)) (|has| |#3| (-782)) (|has| |#3| (-971))) ((|#3|) -3844 (|has| |#3| (-157)) (|has| |#3| (-338)) (|has| |#3| (-971)))) (((|#1|) . T)) (((|#1|) . T)) (|has| |#1| (-338)) @@ -3146,37 +3146,37 @@ ((((-792)) . T)) ((((-792)) . T)) (((|#1|) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) ((((-522) |#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#2| $) -12 (|has| |#1| (-338)) (|has| |#2| (-262 |#2| |#2|))) (($ $) . T)) ((($ $) . T)) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-838))) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-426)) (|has| |#1| (-838))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) ((((-792)) . T)) ((((-792)) . T)) ((((-792)) . T)) (((|#1| (-494 |#2|)) . T)) -((((-2 (|:| -2530 (-1085)) (|:| -3048 (-51)))) . T)) +((((-2 (|:| -2644 (-1085)) (|:| -3149 (-51)))) . T)) (((|#1| (-522)) . T)) (((|#1| (-382 (-522))) . T)) (((|#1| (-708)) . T)) ((((-112 |#1|)) . T) (($) . T) (((-382 (-522))) . T)) -(-3708 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) -(-3708 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) +(-3844 (|has| |#2| (-426)) (|has| |#2| (-514)) (|has| |#2| (-838))) +(-3844 (|has| |#1| (-426)) (|has| |#1| (-514)) (|has| |#1| (-838))) ((($) . T)) (((|#2| (-494 (-794 |#1|))) . T)) ((((-522) |#1|) . T)) (((|#2|) . T)) (((|#2| (-708)) . T)) -((((-792)) -3708 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) +((((-792)) -3844 (|has| |#1| (-562 (-792))) (|has| |#1| (-1014)))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((((-1068) |#1|) . T)) ((((-382 |#2|)) . T)) -((((-2 (|:| -2530 |#1|) (|:| -3048 |#2|))) . T)) +((((-2 (|:| -2644 |#1|) (|:| -3149 |#2|))) . T)) (|has| |#1| (-514)) (|has| |#1| (-514)) ((($) . T) ((|#2|) . T)) @@ -3184,12 +3184,12 @@ (((|#1| |#2|) . T)) (((|#2| $) |has| |#2| (-262 |#2| |#2|))) (((|#1| (-588 |#1|)) |has| |#1| (-782))) -(-3708 (|has| |#1| (-210)) (|has| |#1| (-324))) -(-3708 (|has| |#1| (-338)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-210)) (|has| |#1| (-324))) +(-3844 (|has| |#1| (-338)) (|has| |#1| (-324))) (|has| |#1| (-1014)) (((|#1|) . T)) ((((-382 (-522))) . T) (($) . T)) -((((-925 |#1|)) . T) ((|#1|) . T) (((-522)) -3708 (|has| (-925 |#1|) (-962 (-522))) (|has| |#1| (-962 (-522)))) (((-382 (-522))) -3708 (|has| (-925 |#1|) (-962 (-382 (-522)))) (|has| |#1| (-962 (-382 (-522)))))) +((((-925 |#1|)) . T) ((|#1|) . T) (((-522)) -3844 (|has| (-925 |#1|) (-962 (-522))) (|has| |#1| (-962 (-522)))) (((-382 (-522))) -3844 (|has| (-925 |#1|) (-962 (-382 (-522)))) (|has| |#1| (-962 (-382 (-522)))))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) (((|#1| |#1|) -12 (|has| |#1| (-285 |#1|)) (|has| |#1| (-1014)))) @@ -3200,9 +3200,9 @@ (((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1050 |#1| |#2|) #0#) |has| (-1050 |#1| |#2|) (-285 (-1050 |#1| |#2|)))) -(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) #0#) |has| (-2 (|:| -2530 |#1|) (|:| -3048 |#2|)) (-285 (-2 (|:| -2530 |#1|) (|:| -3048 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-285 |#2|)) (|has| |#2| (-1014))) ((#0=(-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) #0#) |has| (-2 (|:| -2644 |#1|) (|:| -3149 |#2|)) (-285 (-2 (|:| -2644 |#1|) (|:| -3149 |#2|))))) (((#0=(-112 |#1|)) |has| #0# (-285 #0#))) -(-3708 (|has| |#1| (-784)) (|has| |#1| (-1014))) +(-3844 (|has| |#1| (-784)) (|has| |#1| (-1014))) ((($ $) . T)) ((($ $) . T) ((#0=(-794 |#1|) $) . T) ((#0# |#2|) . T)) ((($ $) . T) ((|#2| $) |has| |#1| (-210)) ((|#2| |#1|) |has| |#1| (-210)) ((|#3| |#1|) . T) ((|#3| $) . T)) |