diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 1130 |
1 files changed, 565 insertions, 565 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 3afc9f26..b731f09c 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,14 +1,14 @@ -(143433 . 3429209011) -(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) #0#) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(143433 . 3429259033) +(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) #0#) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (((|#2| |#2|) . T)) ((((-530)) . T)) -((($ $) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((|#2| |#2|) . T) ((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530))))) +((($ $) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((|#2| |#2|) . T) ((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530))))) ((($) . T)) (((|#1|) . T)) ((($) . T) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#2|) . T)) -((($) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((|#2|) . T) (((-388 (-530))) |has| |#2| (-37 (-388 (-530))))) +((($) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((|#2|) . T) (((-388 (-530))) |has| |#2| (-37 (-388 (-530))))) (|has| |#1| (-850)) ((((-804)) . T)) ((((-804)) . T)) @@ -23,28 +23,28 @@ ((((-208)) . T) (((-804)) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-793))) -((($ $) . T) ((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1| |#1|) . T)) -(-1476 (|has| |#1| (-768)) (|has| |#1| (-795))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-793))) +((($ $) . T) ((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1| |#1|) . T)) +(-1461 (|has| |#1| (-768)) (|has| |#1| (-795))) ((((-388 (-530))) |has| |#1| (-975 (-388 (-530)))) (((-530)) |has| |#1| (-975 (-530))) ((|#1|) . T)) ((((-804)) . T)) ((((-804)) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (|has| |#1| (-793)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1| |#2| |#3|) . T)) (((|#4|) . T)) -((($) . T) (((-388 (-530))) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) +((($) . T) (((-388 (-530))) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) ((((-804)) . T)) ((((-804)) |has| |#1| (-1027))) (((|#1|) . T) ((|#2|) . T)) (((|#1|) . T) (((-530)) |has| |#1| (-975 (-530))) (((-388 (-530))) |has| |#1| (-975 (-388 (-530))))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) -(((|#2| (-461 (-2167 |#1|) (-719))) . T)) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(((|#2| (-461 (-2267 |#1|) (-719))) . T)) (((|#1| (-502 (-1099))) . T)) (((#0=(-811 |#1|) #0#) . T) ((#1=(-388 (-530)) #1#) . T) (($ $) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (|has| |#4| (-349)) (|has| |#3| (-349)) (((|#1|) . T)) @@ -54,10 +54,10 @@ (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-522)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) ((($) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) ((($) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T)) ((($) . T)) @@ -66,59 +66,59 @@ ((((-804)) . T)) ((((-804)) . T)) ((((-388 (-530))) . T) (($) . T)) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-344)) (($) . T) ((|#1|) . T)) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-344)) (($) . T) ((|#1|) . T)) ((((-804)) . T)) ((((-804)) . T)) (((|#1|) . T)) ((((-804)) . T)) -(((|#1|) . T) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) . T)) +(((|#1|) . T) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) . T)) (((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) (($) . T)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#1| |#2|) . T)) ((((-804)) . T)) (((|#1|) . T)) -(((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530)))) ((|#2| |#2|) . T) (($ $) -1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +(((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530)))) ((|#2| |#2|) . T) (($ $) -1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) (((|#1|) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) -((($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) -(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) +(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) ((($ $) . T)) (((|#2|) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T) (($) -1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T) (($) -1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) ((($) . T)) (|has| |#1| (-349)) (((|#1|) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) ((((-804)) . T)) ((((-804)) . T)) (((|#1| |#2|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) (((|#1| |#1|) . T)) (|has| |#1| (-522)) (((|#2| |#2|) -12 (|has| |#1| (-344)) (|has| |#2| (-291 |#2|))) (((-1099) |#2|) -12 (|has| |#1| (-344)) (|has| |#2| (-491 (-1099) |#2|)))) ((((-388 |#2|)) . T) (((-388 (-530))) . T) (($) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-793))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-793))) ((($ $) . T) ((#0=(-388 (-530)) #0#) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (|has| |#1| (-1027)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (|has| |#1| (-1027)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (|has| |#1| (-793)) ((($) . T) (((-388 (-530))) . T)) (((|#1|) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) -(-1476 (|has| |#4| (-741)) (|has| |#4| (-793))) -(-1476 (|has| |#4| (-741)) (|has| |#4| (-793))) -(-1476 (|has| |#3| (-741)) (|has| |#3| (-793))) -(-1476 (|has| |#3| (-741)) (|has| |#3| (-793))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#4| (-741)) (|has| |#4| (-793))) +(-1461 (|has| |#4| (-741)) (|has| |#4| (-793))) +(-1461 (|has| |#3| (-741)) (|has| |#3| (-793))) +(-1461 (|has| |#3| (-741)) (|has| |#3| (-793))) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-1027)) @@ -132,21 +132,21 @@ ((((-530)) . T)) ((((-530)) . T)) (((|#1|) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) (((|#1| (-719)) . T)) (|has| |#2| (-741)) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) (|has| |#2| (-793)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) ((((-1082) |#1|) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (((|#1|) . T)) (((|#3| (-719)) . T)) (|has| |#1| (-140)) (|has| |#1| (-138)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (|has| |#1| (-1027)) ((((-388 (-530))) . T) (((-530)) . T)) ((((-1099) |#2|) |has| |#2| (-491 (-1099) |#2|)) ((|#2| |#2|) |has| |#2| (-291 |#2|))) @@ -154,7 +154,7 @@ (((|#1|) . T) (($) . T)) ((((-530)) . T)) ((((-530)) . T)) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) |has| |#1| (-162))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) |has| |#1| (-162))) ((((-530)) . T)) ((((-530)) . T)) (((#0=(-647) (-1095 #0#)) . T)) @@ -173,12 +173,12 @@ ((((-804)) . T)) ((((-804)) . T)) (((|#1| |#1|) . T)) -(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) (((|#1|) . T)) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) -((($) -1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984)))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984)))) ((((-804)) . T)) ((((-804)) . T)) ((((-804)) . T)) @@ -189,25 +189,25 @@ ((((-804)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-793))) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-793))) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#2|) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) -(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522)))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-793))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-793))) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#2|) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) +(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522)))) (|has| |#1| (-344)) (-12 (|has| |#4| (-216)) (|has| |#4| (-984))) (-12 (|has| |#3| (-216)) (|has| |#3| (-984))) -(-1476 (|has| |#4| (-162)) (|has| |#4| (-793)) (|has| |#4| (-984))) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#4| (-162)) (|has| |#4| (-793)) (|has| |#4| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((((-804)) . T)) (((|#1|) . T)) ((((-388 (-530))) |has| |#1| (-975 (-388 (-530)))) (((-530)) |has| |#1| (-975 (-530))) ((|#1|) . T)) (((|#1|) . T) (((-530)) |has| |#1| (-593 (-530)))) -(((|#2|) . T) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) (|has| |#1| (-522)) (|has| |#1| (-522)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#1|) . T)) (|has| |#1| (-522)) (|has| |#1| (-522)) @@ -218,11 +218,11 @@ (((|#2|) . T) (($) . T) (((-388 (-530))) . T)) (-12 (|has| |#1| (-1027)) (|has| |#2| (-1027))) ((($) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T)) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (((-1097 |#1| |#2| |#3|)) |has| |#1| (-344)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) . T)) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (((-1097 |#1| |#2| |#3|)) |has| |#1| (-344)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) . T)) (((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) (($) . T)) -(((|#4| |#4|) -1476 (|has| |#4| (-162)) (|has| |#4| (-344)) (|has| |#4| (-984))) (($ $) |has| |#4| (-162))) -(((|#3| |#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984))) (($ $) |has| |#3| (-162))) +(((|#4| |#4|) -1461 (|has| |#4| (-162)) (|has| |#4| (-344)) (|has| |#4| (-984))) (($ $) |has| |#4| (-162))) +(((|#3| |#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984))) (($ $) |has| |#3| (-162))) (((|#1|) . T)) (((|#2|) . T)) ((((-506)) |has| |#2| (-572 (-506))) (((-833 (-360))) |has| |#2| (-572 (-833 (-360)))) (((-833 (-530))) |has| |#2| (-572 (-833 (-530))))) @@ -231,21 +231,21 @@ ((((-804)) . T)) ((((-506)) |has| |#1| (-572 (-506))) (((-833 (-360))) |has| |#1| (-572 (-833 (-360)))) (((-833 (-530))) |has| |#1| (-572 (-833 (-530))))) ((((-804)) . T)) -(((|#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984))) (($) |has| |#3| (-162))) -(((|#4|) -1476 (|has| |#4| (-162)) (|has| |#4| (-344)) (|has| |#4| (-984))) (($) |has| |#4| (-162))) +(((|#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984))) (($) |has| |#3| (-162))) +(((|#4|) -1461 (|has| |#4| (-162)) (|has| |#4| (-344)) (|has| |#4| (-984))) (($) |has| |#4| (-162))) ((((-804)) . T)) ((((-506)) . T) (((-530)) . T) (((-833 (-530))) . T) (((-360)) . T) (((-208)) . T)) (((|#1|) . T) (((-530)) |has| |#1| (-975 (-530))) (((-388 (-530))) |has| |#1| (-975 (-388 (-530))))) ((($) . T) (((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T)) ((((-388 $) (-388 $)) |has| |#2| (-522)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 (-51)))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 (-51)))) . T)) (((|#1|) . T)) (|has| |#2| (-850)) ((((-1082) (-51)) . T)) ((((-530)) |has| #0=(-388 |#2|) (-593 (-530))) ((#0#) . T)) ((((-506)) . T) (((-208)) . T) (((-360)) . T) (((-833 (-360))) . T)) ((((-804)) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) (((|#1|) |has| |#1| (-162))) (((|#1| $) |has| |#1| (-268 |#1| |#1|))) ((((-804)) . T)) @@ -256,15 +256,15 @@ (|has| |#1| (-795)) (|has| |#1| (-1027)) (((|#1|) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) ((((-127)) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) ((((-127)) . T)) -((($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (|has| |#1| (-216)) -((($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1| (-502 (-766 (-1099)))) . T)) (((|#1| (-911)) . T)) (((#0=(-811 |#1|) $) |has| #0# (-268 #0# #0#))) @@ -273,7 +273,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1075)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) (|has| (-1167 |#1| |#2| |#3| |#4|) (-138)) (|has| (-1167 |#1| |#2| |#3| |#4|) (-140)) (|has| |#1| (-138)) @@ -290,20 +290,20 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-984))) ((((-804)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) #0#) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) #0#) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (((|#1|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027))) ((#0=(-2 (|:| -2940 (-1082)) (|:| -1806 |#1|)) #0#) |has| (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|)) (-291 (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027))) ((#0=(-2 (|:| -3078 (-1082)) (|:| -1874 |#1|)) #0#) |has| (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|)) (-291 (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))))) ((((-530) |#1|) . T)) ((((-804)) . T)) ((((-506)) -12 (|has| |#1| (-572 (-506))) (|has| |#2| (-572 (-506)))) (((-833 (-360))) -12 (|has| |#1| (-572 (-833 (-360)))) (|has| |#2| (-572 (-833 (-360))))) (((-833 (-530))) -12 (|has| |#1| (-572 (-833 (-530)))) (|has| |#2| (-572 (-833 (-530)))))) ((((-804)) . T)) ((((-804)) . T)) ((($) . T)) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) ((($) . T)) ((($) . T)) ((($) . T)) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((((-804)) . T)) ((((-804)) . T)) (|has| (-1166 |#2| |#3| |#4|) (-140)) @@ -314,16 +314,16 @@ ((((-804)) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) (((|#1|) . T)) ((((-530) |#1|) . T)) (((|#2|) |has| |#2| (-162))) (((|#1|) |has| |#1| (-162))) (((|#1|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-793))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-793))) ((((-804)) |has| |#1| (-1027))) -(-1476 (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)) (|has| |#1| (-1039))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)) (|has| |#1| (-1039))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((((-851 |#1|)) . T)) ((((-388 |#2|) |#3|) . T)) (|has| |#1| (-15 * (|#1| (-530) |#1|))) @@ -335,7 +335,7 @@ (((|#1|) . T)) ((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) |has| |#1| (-522))) (|has| |#1| (-344)) -(-1476 (-12 (|has| (-1173 |#1| |#2| |#3|) (-216)) (|has| |#1| (-344))) (|has| |#1| (-15 * (|#1| (-530) |#1|)))) +(-1461 (-12 (|has| (-1173 |#1| |#2| |#3|) (-216)) (|has| |#1| (-344))) (|has| |#1| (-15 * (|#1| (-530) |#1|)))) (|has| |#1| (-15 * (|#1| (-388 (-530)) |#1|))) (|has| |#1| (-344)) ((((-530)) . T)) @@ -347,31 +347,31 @@ (((|#1|) . T)) ((((-530) |#1|) . T)) (((|#2|) . T)) -(-1476 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) (((|#1|) . T)) ((((-1099)) -12 (|has| |#3| (-841 (-1099))) (|has| |#3| (-984)))) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (-12 (|has| |#1| (-344)) (|has| |#2| (-768))) -(-1476 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330)) (|has| |#1| (-522))) -(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-522)))) +(-1461 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330)) (|has| |#1| (-522))) +(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-522)))) ((($ $) |has| |#1| (-522))) (((#0=(-647) (-1095 #0#)) . T)) ((((-804)) . T)) ((((-804)) . T) (((-1181 |#4|)) . T)) ((((-804)) . T) (((-1181 |#3|)) . T)) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-522)))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-522)))) ((($) |has| |#1| (-522))) ((((-804)) . T)) ((($) . T)) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((#1=(-1173 |#1| |#2| |#3|) #1#) |has| |#1| (-344)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) . T)) -(((|#1|) . T) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((#1=(-1173 |#1| |#2| |#3|) #1#) |has| |#1| (-344)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) . T)) +(((|#1|) . T) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) (((|#3|) |has| |#3| (-984))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (|has| |#1| (-1027)) (((|#2| (-767 |#1|)) . T)) (((|#1|) . T)) @@ -383,37 +383,37 @@ ((((-137)) . T)) (((|#3|) |has| |#3| (-1027)) (((-530)) -12 (|has| |#3| (-975 (-530))) (|has| |#3| (-1027))) (((-388 (-530))) -12 (|has| |#3| (-975 (-388 (-530)))) (|has| |#3| (-1027)))) ((((-804)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1|) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) . T)) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) . T)) (|has| |#1| (-344)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-793))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-793))) ((((-1099) |#1|) |has| |#1| (-491 (-1099) |#1|)) ((|#1| |#1|) |has| |#1| (-291 |#1|))) (|has| |#2| (-768)) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-793)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) ((((-804)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-506)) |has| |#1| (-572 (-506)))) (((|#1| |#2|) . T)) ((((-1099)) -12 (|has| |#1| (-344)) (|has| |#1| (-841 (-1099))))) ((((-1082) |#1|) . T)) (((|#1| |#2| |#3| (-502 |#3|)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (|has| |#1| (-349)) (|has| |#1| (-349)) (|has| |#1| (-349)) ((((-804)) . T)) (((|#1|) . T)) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) (|has| |#1| (-349)) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((((-530)) . T)) ((((-530)) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((((-804)) . T)) ((((-804)) . T)) (-12 (|has| |#2| (-216)) (|has| |#2| (-984))) @@ -422,10 +422,10 @@ ((((-530) |#4|) . T)) ((((-530) |#3|) . T)) (((|#1|) . T) (((-530)) |has| |#1| (-593 (-530)))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((((-1167 |#1| |#2| |#3| |#4|)) . T)) ((((-388 (-530))) . T) (((-530)) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (((|#1| |#1|) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) @@ -454,38 +454,38 @@ ((($) . T)) ((($ $) . T) ((#0=(-1099) $) . T) ((#0# |#1|) . T)) (((|#2|) |has| |#2| (-162))) -((($) -1476 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((|#2|) |has| |#2| (-162)) (((-388 (-530))) |has| |#2| (-37 (-388 (-530))))) -(((|#2| |#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($ $) |has| |#2| (-162))) +((($) -1461 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((|#2|) |has| |#2| (-162)) (((-388 (-530))) |has| |#2| (-37 (-388 (-530))))) +(((|#2| |#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($ $) |has| |#2| (-162))) ((((-137)) . T)) (((|#1|) . T)) (-12 (|has| |#1| (-349)) (|has| |#2| (-349))) ((((-804)) . T)) -(((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($) |has| |#2| (-162))) +(((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($) |has| |#2| (-162))) (((|#1|) . T)) ((((-804)) . T)) (|has| |#1| (-1027)) (|has| $ (-140)) ((((-530) |#1|) . T)) -((($) -1476 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) +((($) -1461 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) ((((-1099)) -12 (|has| |#1| (-15 * (|#1| (-388 (-530)) |#1|))) (|has| |#1| (-841 (-1099))))) (|has| |#1| (-344)) -(-1476 (-12 (|has| (-1097 |#1| |#2| |#3|) (-216)) (|has| |#1| (-344))) (|has| |#1| (-15 * (|#1| (-530) |#1|)))) +(-1461 (-12 (|has| (-1097 |#1| |#2| |#3|) (-216)) (|has| |#1| (-344))) (|has| |#1| (-15 * (|#1| (-530) |#1|)))) (|has| |#1| (-15 * (|#1| (-388 (-530)) |#1|))) (|has| |#1| (-344)) (|has| |#1| (-15 * (|#1| (-719) |#1|))) (((|#1|) . T)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) ((((-804)) . T)) ((((-530) (-127)) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) (((|#2| (-502 (-806 |#1|))) . T)) ((((-804)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1|) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((((-543 |#1|)) . T)) ((($) . T)) (((|#1|) . T) (($) . T)) @@ -502,28 +502,28 @@ ((((-804)) . T)) ((((-804)) . T)) (((|#1| |#2| |#3| |#4| |#5|) . T)) -(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-522)))) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((#1=(-1097 |#1| |#2| |#3|) #1#) |has| |#1| (-344)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-522)))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((#1=(-1097 |#1| |#2| |#3|) #1#) |has| |#1| (-344)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) (((|#2|) |has| |#2| (-984))) (|has| |#1| (-1027)) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-522)))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (((-1097 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) . T)) -(((|#1|) . T) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-522)))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (((-1097 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) . T)) +(((|#1|) . T) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1|) |has| |#1| (-162)) (($) . T)) (((|#1|) . T)) -(((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530)))) ((|#2| |#2|) . T) (($ $) -1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +(((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530)))) ((|#2| |#2|) . T) (($ $) -1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) ((((-804)) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) ((($ $) . T) ((|#2| $) . T) ((|#2| |#1|) . T)) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) (((#0=(-1012) |#1|) . T) ((#0# $) . T) (($ $) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T) (($) -1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T) (($) -1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) ((($) . T)) (((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) (($) . T)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#2|) |has| |#1| (-344))) (((|#1|) . T)) (((|#2|) |has| |#2| (-1027)) (((-530)) -12 (|has| |#2| (-975 (-530))) (|has| |#2| (-1027))) (((-388 (-530))) -12 (|has| |#2| (-975 (-388 (-530)))) (|has| |#2| (-1027)))) @@ -538,8 +538,8 @@ (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-138)) (|has| |#1| (-140)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) -((($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((((-388 (-530))) . T) (($) . T)) ((((-388 (-530))) . T) (($) . T)) ((((-388 (-530))) . T) (($) . T)) @@ -550,12 +550,12 @@ (((|#1| (-719) (-1012)) . T)) ((((-388 (-530))) |has| |#2| (-344)) (($) . T)) (((|#1| (-502 (-1017 (-1099))) (-1017 (-1099))) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (((|#1|) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) (|has| |#2| (-741)) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) (|has| |#1| (-349)) (|has| |#1| (-349)) (|has| |#1| (-349)) @@ -588,63 +588,63 @@ (((|#4| |#4|) -12 (|has| |#4| (-291 |#4|)) (|has| |#4| (-1027)))) (((|#2|) . T) (((-530)) |has| |#2| (-975 (-530))) (((-388 (-530))) |has| |#2| (-975 (-388 (-530))))) (((|#3| |#3|) -12 (|has| |#3| (-291 |#3|)) (|has| |#3| (-1027)))) -(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) ((($) . T)) (((|#2|) . T)) (((|#3|) . T)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) -(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (((|#2|) . T)) -((((-804)) -1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-571 (-804))) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((-1181 |#2|)) . T)) +((((-804)) -1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-571 (-804))) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((-1181 |#2|)) . T)) (((|#1|) |has| |#1| (-162))) ((((-530)) . T)) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((((-530) (-137)) . T)) -((($) -1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984)))) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) +((($) -1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984)))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) (((|#1|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) (((|#2|) |has| |#1| (-344))) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1| |#1|) . T) (($ $) . T)) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) |has| |#1| (-162))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) |has| |#1| (-162))) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1| (-502 #0=(-1099)) #0#) . T)) (((|#1|) . T) (($) . T)) (|has| |#4| (-162)) (|has| |#3| (-162)) (((#0=(-388 (-893 |#1|)) #0#) . T)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (|has| |#1| (-1027)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (|has| |#1| (-1027)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#1| |#1|) |has| |#1| (-162))) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1|) . T)) ((((-388 (-893 |#1|))) . T)) ((((-530) (-127)) . T)) (((|#1|) |has| |#1| (-162))) ((((-127)) . T)) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((((-804)) . T)) ((((-1167 |#1| |#2| |#3| |#4|)) . T)) (((|#1|) |has| |#1| (-984)) (((-530)) -12 (|has| |#1| (-593 (-530))) (|has| |#1| (-984)))) (((|#1| |#2|) . T)) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-675)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-675)) (|has| |#3| (-793)) (|has| |#3| (-984))) (|has| |#3| (-741)) -(-1476 (|has| |#3| (-741)) (|has| |#3| (-793))) +(-1461 (|has| |#3| (-741)) (|has| |#3| (-793))) (|has| |#3| (-793)) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#2|) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) -(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522)))) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#2|) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) +(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522)))) (((|#2|) . T)) ((((-530) (-127)) . T)) ((((-804)) . T)) @@ -660,22 +660,22 @@ (|has| |#1| (-1027)) (((|#2|) . T)) ((((-506)) |has| |#2| (-572 (-506))) (((-833 (-360))) |has| |#2| (-572 (-833 (-360)))) (((-833 (-530))) |has| |#2| (-572 (-833 (-530))))) -(((|#4|) -1476 (|has| |#4| (-162)) (|has| |#4| (-344)))) -(((|#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)))) +(((|#4|) -1461 (|has| |#4| (-162)) (|has| |#4| (-344)))) +(((|#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)))) ((((-804)) . T)) (((|#1|) . T)) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-850))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-850))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-850))) ((($ $) . T) ((#0=(-1099) $) |has| |#1| (-216)) ((#0# |#1|) |has| |#1| (-216)) ((#1=(-766 (-1099)) |#1|) . T) ((#1# $) . T)) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-850))) ((((-530) |#2|) . T)) ((((-804)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) -((($) -1476 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((|#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984)))) +((($) -1461 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((|#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984)))) ((((-530) |#1|) . T)) (|has| (-388 |#2|) (-140)) (|has| (-388 |#2|) (-138)) @@ -688,22 +688,22 @@ (|has| |#1| (-522)) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-804)) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) (|has| |#1| (-37 (-388 (-530)))) -((((-369) (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +((((-369) (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) (|has| |#1| (-37 (-388 (-530)))) (|has| |#2| (-1075)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((|#1|) . T)) ((((-369) (-1082)) . T)) (|has| |#1| (-522)) ((((-114 |#1|)) . T)) ((((-127)) . T)) ((((-530) |#1|) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (((|#2|) . T)) ((((-804)) . T)) ((((-767 |#1|)) . T)) @@ -716,7 +716,7 @@ (((|#1|) |has| |#1| (-162))) ((((-804)) . T)) ((((-506)) |has| |#1| (-572 (-506)))) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#2|) |has| |#2| (-291 |#2|))) (((#0=(-530) #0#) . T) ((#1=(-388 (-530)) #1#) . T) (($ $) . T)) (((|#1|) . T)) @@ -726,7 +726,7 @@ (((#0=(-530) #0#) . T) ((#1=(-388 (-530)) #1#) . T) (($ $) . T)) ((($) . T) (((-530)) . T) (((-388 (-530))) . T)) (|has| |#2| (-349)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) @@ -737,9 +737,9 @@ ((((-1097 |#1| |#2| |#3|) $) -12 (|has| (-1097 |#1| |#2| |#3|) (-268 (-1097 |#1| |#2| |#3|) (-1097 |#1| |#2| |#3|))) (|has| |#1| (-344))) (($ $) . T)) ((((-804)) . T)) ((((-804)) . T)) -((($) . T) (((-388 (-530))) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) +((($) . T) (((-388 (-530))) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) ((((-506)) |has| |#1| (-572 (-506)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) ((($ $) . T)) ((($ $) . T)) ((((-804)) . T)) @@ -749,12 +749,12 @@ (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -((($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((((-388 (-530))) . T) (((-530)) . T)) ((((-530) (-137)) . T)) ((((-137)) . T)) (((|#1|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) ((((-110)) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) ((((-110)) . T)) @@ -762,38 +762,38 @@ ((((-506)) |has| |#1| (-572 (-506))) (((-208)) . #0=(|has| |#1| (-960))) (((-360)) . #0#)) ((((-804)) . T)) (|has| |#1| (-768)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (|has| |#1| (-795)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-522))) (|has| |#1| (-522)) (|has| |#1| (-850)) (((|#1|) . T)) (|has| |#1| (-1027)) ((((-804)) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((((-804)) . T)) ((((-804)) . T)) ((((-804)) . T)) (((|#1| (-1181 |#1|) (-1181 |#1|)) . T)) ((((-530) (-137)) . T)) ((($) . T)) -(-1476 (|has| |#4| (-162)) (|has| |#4| (-793)) (|has| |#4| (-984))) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#4| (-162)) (|has| |#4| (-793)) (|has| |#4| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((((-804)) . T)) (|has| |#1| (-1027)) (((|#1| (-911)) . T)) (((|#1| |#1|) . T)) ((($) . T)) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) (-12 (|has| |#1| (-453)) (|has| |#2| (-453))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) -(-1476 (-12 (|has| |#1| (-453)) (|has| |#2| (-453))) (-12 (|has| |#1| (-675)) (|has| |#2| (-675)))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (-12 (|has| |#1| (-453)) (|has| |#2| (-453))) (-12 (|has| |#1| (-675)) (|has| |#2| (-675)))) (((|#1|) . T)) (|has| |#2| (-741)) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) (((|#1| |#2|) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (|has| |#2| (-793)) @@ -808,7 +808,7 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-388 (-530))) . T) (($) . T)) -((($) . T) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) . T)) +((($) . T) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) . T)) (|has| |#1| (-776)) ((((-388 (-530))) |has| |#1| (-975 (-388 (-530)))) (((-530)) |has| |#1| (-975 (-530))) ((|#1|) . T)) (|has| |#1| (-1027)) @@ -819,8 +819,8 @@ (((|#3|) |has| |#3| (-1027))) (|has| |#3| (-349)) (((|#1|) . T) (((-804)) . T)) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) -(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522)))) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) +(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522)))) ((((-804)) . T)) ((($) |has| |#1| (-522)) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#2|) . T)) @@ -830,30 +830,30 @@ (((|#1|) . T)) (((|#1|) |has| |#1| (-162))) ((((-388 (-530))) . T) (((-530)) . T)) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) ((((-137)) . T)) (((|#1|) . T)) ((((-137)) . T)) -((($) -1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984)))) +((($) -1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984)))) ((((-137)) . T)) (((|#1| |#2| |#3|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) (|has| $ (-140)) (|has| $ (-140)) (|has| |#1| (-1027)) ((((-804)) . T)) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-453)) (|has| |#1| (-522)) (|has| |#1| (-984)) (|has| |#1| (-1039))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-453)) (|has| |#1| (-522)) (|has| |#1| (-984)) (|has| |#1| (-1039))) ((($ $) |has| |#1| (-268 $ $)) ((|#1| $) |has| |#1| (-268 |#1| |#1|))) (((|#1| (-388 (-530))) . T)) (((|#1|) . T)) ((((-1099)) . T)) (|has| |#1| (-522)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (|has| |#1| (-522)) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) @@ -864,7 +864,7 @@ (|has| |#1| (-140)) (|has| |#1| (-138)) (|has| |#4| (-793)) -(((|#2| (-223 (-2167 |#1|) (-719)) (-806 |#1|)) . T)) +(((|#2| (-223 (-2267 |#1|) (-719)) (-806 |#1|)) . T)) (|has| |#3| (-793)) (((|#1| (-502 |#3|) |#3|) . T)) (|has| |#1| (-140)) @@ -878,21 +878,21 @@ (|has| |#1| (-138)) ((((-388 (-530))) |has| |#2| (-344)) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) -(-1476 (|has| |#1| (-330)) (|has| |#1| (-349))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#1| (-330)) (|has| |#1| (-349))) ((((-1066 |#2| |#1|)) . T) ((|#1|) . T)) (|has| |#2| (-162)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-216)) (|has| |#2| (-984))) -(((|#2|) . T) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -(-1476 (|has| |#3| (-741)) (|has| |#3| (-793))) -(-1476 (|has| |#3| (-741)) (|has| |#3| (-793))) +(((|#2|) . T) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +(-1461 (|has| |#3| (-741)) (|has| |#3| (-793))) +(-1461 (|has| |#3| (-741)) (|has| |#3| (-793))) ((((-804)) . T)) (((|#1|) . T)) (((|#2|) . T) (($) . T)) (((|#1|) . T) (($) . T)) ((((-647)) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) (|has| |#1| (-522)) (((|#1|) . T)) (((|#1|) . T)) @@ -914,10 +914,10 @@ (((|#1| (-388 (-530))) . T)) (((|#3|) . T) (((-570 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((($ $) . T) ((|#2| $) . T)) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) (((#0=(-1097 |#1| |#2| |#3|) #0#) -12 (|has| (-1097 |#1| |#2| |#3|) (-291 (-1097 |#1| |#2| |#3|))) (|has| |#1| (-344))) (((-1099) #0#) -12 (|has| (-1097 |#1| |#2| |#3|) (-491 (-1099) (-1097 |#1| |#2| |#3|))) (|has| |#1| (-344)))) @@ -925,8 +925,8 @@ ((((-804)) . T)) ((((-804)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) -(((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027))) (((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) |has| (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|)) (-291 (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))))) +(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) +(((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027))) (((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) |has| (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|)) (-291 (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))))) ((((-804)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -937,10 +937,10 @@ ((($ $) . T) ((#0=(-806 |#1|) $) . T) ((#0# |#2|) . T)) (|has| |#1| (-776)) (|has| |#1| (-1027)) -(((|#2| |#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($ $) |has| |#2| (-162))) -(((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)))) -((((-530) (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T) ((|#1| |#2|) . T)) -(((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($) |has| |#2| (-162))) +(((|#2| |#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($ $) |has| |#2| (-162))) +(((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)))) +((((-530) (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T) ((|#1| |#2|) . T)) +(((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($) |has| |#2| (-162))) ((((-719)) . T)) ((((-530)) . T)) (|has| |#1| (-522)) @@ -953,29 +953,29 @@ ((((-114 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-140)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-522))) ((((-833 (-530))) . T) (((-833 (-360))) . T) (((-506)) . T) (((-1099)) . T)) ((((-804)) . T)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) ((($) . T)) ((((-804)) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) (((|#2|) |has| |#2| (-162))) -((($) -1476 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((|#2|) |has| |#2| (-162)) (((-388 (-530))) |has| |#2| (-37 (-388 (-530))))) +((($) -1461 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((|#2|) |has| |#2| (-162)) (((-388 (-530))) |has| |#2| (-37 (-388 (-530))))) ((((-811 |#1|)) . T)) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (-12 (|has| |#3| (-216)) (|has| |#3| (-984))) (|has| |#2| (-1075)) -(((#0=(-51)) . T) (((-2 (|:| -2940 (-1099)) (|:| -1806 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3078 (-1099)) (|:| -1874 #0#))) . T)) (((|#1| |#2|) . T)) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) (((|#1| (-530) (-1012)) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1| (-388 (-530)) (-1012)) . T)) -((($) -1476 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) +((($) -1461 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) ((((-530) |#2|) . T)) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) @@ -983,37 +983,37 @@ (-12 (|has| |#1| (-349)) (|has| |#2| (-349))) ((((-804)) . T)) ((((-1099) |#1|) |has| |#1| (-491 (-1099) |#1|)) ((|#1| |#1|) |has| |#1| (-291 |#1|))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) (((|#1|) . T)) ((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) |has| |#1| (-522))) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-1097 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) -(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522)))) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-1097 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) +(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522)))) ((($) |has| |#1| (-522)) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((((-804)) . T)) (|has| |#1| (-330)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) #0#) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) #0#) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (|has| |#1| (-522)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) ((((-804)) . T)) (((|#1| |#2|) . T)) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-850))) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-850))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-850))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-850))) ((((-388 (-530))) . T) (((-530)) . T)) ((((-530)) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) ((($) . T)) ((((-804)) . T)) (((|#1|) . T)) ((((-811 |#1|)) . T) (($) . T) (((-388 (-530))) . T)) ((((-804)) . T)) -(((|#3| |#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984))) (($ $) |has| |#3| (-162))) +(((|#3| |#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984))) (($ $) |has| |#3| (-162))) (|has| |#1| (-960)) ((((-804)) . T)) -(((|#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984))) (($) |has| |#3| (-162))) +(((|#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984))) (($) |has| |#3| (-162))) ((((-530) (-110)) . T)) (((|#1|) |has| |#1| (-291 |#1|))) (|has| |#1| (-349)) @@ -1021,31 +1021,31 @@ (|has| |#1| (-349)) ((((-1099) $) |has| |#1| (-491 (-1099) $)) (($ $) |has| |#1| (-291 $)) ((|#1| |#1|) |has| |#1| (-291 |#1|)) (((-1099) |#1|) |has| |#1| (-491 (-1099) |#1|))) ((((-1099)) |has| |#1| (-841 (-1099)))) -(-1476 (-12 (|has| |#1| (-216)) (|has| |#1| (-344))) (|has| |#1| (-330))) +(-1461 (-12 (|has| |#1| (-216)) (|has| |#1| (-344))) (|has| |#1| (-330))) ((((-369) (-1046)) . T)) (((|#1| |#4|) . T)) (((|#1| |#3|) . T)) ((((-369) |#1|) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) (|has| |#1| (-1027)) ((((-804)) . T)) ((((-804)) . T)) ((((-851 |#1|)) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) (((|#1| |#2|) . T)) ((($) . T)) (((|#1| |#1|) . T)) (((#0=(-811 |#1|)) |has| #0# (-291 #0#))) (((|#1| |#2|) . T)) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) (-12 (|has| |#1| (-741)) (|has| |#2| (-741))) (((|#1|) . T)) (-12 (|has| |#1| (-741)) (|has| |#2| (-741))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (|has| |#1| (-1121)) (((#0=(-530) #0#) . T) ((#1=(-388 (-530)) #1#) . T) (($ $) . T)) ((((-388 (-530))) . T) (($) . T)) @@ -1056,8 +1056,8 @@ (((|#1| |#1|) . T) (($ $) . T) ((#0=(-388 (-530)) #0#) . T)) (|has| |#1| (-344)) ((((-530)) . T) (((-388 (-530))) . T) (($) . T)) -((($ $) . T) ((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1| |#1|) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((($ $) . T) ((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1| |#1|) . T)) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (((|#1|) . T) (($) . T) (((-388 (-530))) . T)) ((((-804)) . T)) ((((-804)) . T)) @@ -1072,14 +1072,14 @@ (((|#1| |#2|) . T)) (|has| |#1| (-793)) (|has| |#1| (-793)) -((($) . T) (((-388 (-530))) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-522))) -(((#0=(-2 (|:| -2940 (-1099)) (|:| -1806 (-51))) #0#) |has| (-2 (|:| -2940 (-1099)) (|:| -1806 (-51))) (-291 (-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))))) +((($) . T) (((-388 (-530))) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-522))) +(((#0=(-2 (|:| -3078 (-1099)) (|:| -1874 (-51))) #0#) |has| (-2 (|:| -3078 (-1099)) (|:| -1874 (-51))) (-291 (-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))))) ((($) . T)) (|has| |#2| (-795)) ((($) . T)) (((|#2|) |has| |#2| (-1027))) -((((-804)) -1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-571 (-804))) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((-1181 |#2|)) . T)) +((((-804)) -1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-571 (-804))) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((-1181 |#2|)) . T)) (|has| |#1| (-795)) (|has| |#1| (-795)) ((((-1082) (-51)) . T)) @@ -1087,10 +1087,10 @@ ((((-804)) . T)) ((((-530)) |has| #0=(-388 |#2|) (-593 (-530))) ((#0#) . T)) ((((-530) (-137)) . T)) -((((-530) (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T) ((|#1| |#2|) . T)) +((((-530) (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T) ((|#1| |#2|) . T)) ((((-388 (-530))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-804)) . T)) ((((-851 |#1|)) . T)) (|has| |#1| (-344)) @@ -1115,31 +1115,31 @@ ((($) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-162))) -((((-530) (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T) ((|#1| |#2|) . T)) +((((-530) (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) ((($) |has| |#1| (-522)) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#3|) . T)) (((|#1|) |has| |#1| (-162))) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850)))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1|) . T)) (((|#1|) . T)) ((((-506)) |has| |#1| (-572 (-506))) (((-833 (-360))) |has| |#1| (-572 (-833 (-360)))) (((-833 (-530))) |has| |#1| (-572 (-833 (-530))))) ((((-804)) . T)) -(((|#2|) . T) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (|has| |#2| (-793)) (-12 (|has| |#2| (-216)) (|has| |#2| (-984))) (|has| |#1| (-522)) (|has| |#1| (-1075)) ((((-1082) |#1|) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) -(((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#1| |#1|) . T)) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#1| |#1|) . T)) ((((-388 (-530))) |has| |#1| (-975 (-530))) (((-530)) |has| |#1| (-975 (-530))) (((-1099)) |has| |#1| (-975 (-1099))) ((|#1|) . T)) ((((-530) |#2|) . T)) ((((-388 (-530))) |has| |#1| (-975 (-388 (-530)))) (((-530)) |has| |#1| (-975 (-530))) ((|#1|) . T)) ((((-530)) |has| |#1| (-827 (-530))) (((-360)) |has| |#1| (-827 (-360)))) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#1|) . T)) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#1|) . T)) (((|#1|) . T)) ((((-597 |#4|)) . T) (((-804)) . T)) ((((-506)) |has| |#4| (-572 (-506)))) @@ -1152,17 +1152,17 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1099)) |has| (-388 |#2|) (-841 (-1099)))) -(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) #0#) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) #0#) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) -((((-804)) -1476 (|has| |#3| (-25)) (|has| |#3| (-128)) (|has| |#3| (-571 (-804))) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-349)) (|has| |#3| (-675)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984)) (|has| |#3| (-1027))) (((-1181 |#3|)) . T)) +((((-804)) -1461 (|has| |#3| (-25)) (|has| |#3| (-128)) (|has| |#3| (-571 (-804))) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-349)) (|has| |#3| (-675)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984)) (|has| |#3| (-1027))) (((-1181 |#3|)) . T)) ((((-530) |#2|) . T)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) -(((|#2| |#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($ $) |has| |#2| (-162))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(((|#2| |#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($ $) |has| |#2| (-162))) ((((-804)) . T)) ((((-804)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T) ((|#2|) . T)) ((((-804)) . T)) ((((-804)) . T)) ((((-1082) (-1099) (-530) (-208) (-804)) . T)) @@ -1197,8 +1197,8 @@ (|has| |#1| (-37 (-388 (-530)))) ((((-804)) . T)) ((((-506)) |has| |#1| (-572 (-506)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) -(((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($) |has| |#2| (-162))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +(((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-984))) (($) |has| |#2| (-162))) (|has| $ (-140)) ((((-388 |#2|)) . T)) ((((-388 (-530))) |has| #0=(-388 |#2|) (-975 (-388 (-530)))) (((-530)) |has| #0# (-975 (-530))) ((#0#) . T)) @@ -1209,11 +1209,11 @@ (((|#3|) |has| |#3| (-162))) (|has| |#1| (-140)) (|has| |#1| (-138)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) (|has| |#1| (-140)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) (|has| |#1| (-140)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) (|has| |#1| (-140)) (((|#1|) . T)) (((|#2|) . T)) @@ -1244,7 +1244,7 @@ ((((-938 |#1|)) . T) ((|#1|) . T)) ((((-804)) . T)) ((((-804)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-388 (-530))) . T) (((-388 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1095 |#1|)) . T)) ((((-530)) . T) (($) . T) (((-388 (-530))) . T)) @@ -1252,9 +1252,9 @@ (|has| |#1| (-795)) (((|#2|) . T)) ((((-530)) . T) (($) . T) (((-388 (-530))) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) ((((-530) |#2|) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (((|#2|) . T)) ((((-530) |#3|) . T)) (((|#2|) . T)) @@ -1269,7 +1269,7 @@ (((|#3|) -12 (|has| |#3| (-291 |#3|)) (|has| |#3| (-1027)))) (((|#2|) . T)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) #0#) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) #0#) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (((|#2| |#2|) . T)) (|has| |#2| (-344)) (((|#2|) . T) (((-530)) |has| |#2| (-975 (-530))) (((-388 (-530))) |has| |#2| (-975 (-388 (-530))))) @@ -1299,19 +1299,19 @@ (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1| |#2|) . T)) ((((-530) (-137)) . T)) -(((#0=(-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) #0#) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) -((($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +(((#0=(-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) #0#) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) +((($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (|has| |#1| (-795)) (((|#2| (-719) (-1012)) . T)) (((|#1| |#2|) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-522))) (|has| |#1| (-739)) (((|#1|) |has| |#1| (-162))) (((|#4|) . T)) (((|#4|) . T)) (((|#1| |#2|) . T)) -(-1476 (|has| |#1| (-140)) (-12 (|has| |#1| (-344)) (|has| |#2| (-140)))) -(-1476 (|has| |#1| (-138)) (-12 (|has| |#1| (-344)) (|has| |#2| (-138)))) +(-1461 (|has| |#1| (-140)) (-12 (|has| |#1| (-344)) (|has| |#2| (-140)))) +(-1461 (|has| |#1| (-138)) (-12 (|has| |#1| (-344)) (|has| |#2| (-138)))) (((|#4|) . T)) (|has| |#1| (-138)) ((((-1082) |#1|) . T)) @@ -1324,10 +1324,10 @@ (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#3|) . T)) ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-344))) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#1|) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027))) (((-899 |#1|)) . T)) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027))) (((-899 |#1|)) . T)) (|has| |#1| (-793)) (|has| |#1| (-793)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) @@ -1340,8 +1340,8 @@ ((($) . T)) ((((-369) (-1082)) . T)) ((($) |has| |#1| (-522)) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) -((((-804)) -1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-571 (-804))) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((-1181 |#2|)) . T)) -(((#0=(-51)) . T) (((-2 (|:| -2940 (-1082)) (|:| -1806 #0#))) . T)) +((((-804)) -1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-571 (-804))) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((-1181 |#2|)) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3078 (-1082)) (|:| -1874 #0#))) . T)) (((|#1|) . T)) ((((-804)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) @@ -1349,7 +1349,7 @@ (|has| |#2| (-138)) (|has| |#2| (-140)) (|has| |#1| (-453)) -(-1476 (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) (|has| |#1| (-344)) ((((-804)) . T)) (|has| |#1| (-37 (-388 (-530)))) @@ -1358,8 +1358,8 @@ (|has| |#1| (-793)) (|has| |#1| (-793)) ((((-804)) . T)) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) -(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522)))) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) +(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522)))) ((($) |has| |#1| (-522)) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1| |#2|) . T)) ((((-1099)) |has| |#1| (-841 (-1099)))) @@ -1367,7 +1367,7 @@ ((((-804)) . T)) ((((-804)) . T)) (|has| |#1| (-1027)) -(((|#2| (-461 (-2167 |#1|) (-719)) (-806 |#1|)) . T)) +(((|#2| (-461 (-2267 |#1|) (-719)) (-806 |#1|)) . T)) ((((-388 (-530))) . #0=(|has| |#2| (-344))) (($) . #0#)) (((|#1| (-502 (-1099)) (-1099)) . T)) (((|#1|) . T)) @@ -1387,16 +1387,16 @@ (|has| |#1| (-140)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) . T)) +(((|#1|) . T) (((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) . T)) ((((-1097 |#1| |#2| |#3|)) |has| |#1| (-344))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-1099) (-51)) . T)) ((($ $) . T)) (((|#1| (-530)) . T)) ((((-851 |#1|)) . T)) -(((|#1|) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-984))) (($) -1476 (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)))) +(((|#1|) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-984))) (($) -1461 (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)))) (((|#1|) . T) (((-530)) |has| |#1| (-975 (-530))) (((-388 (-530))) |has| |#1| (-975 (-388 (-530))))) (|has| |#1| (-795)) (|has| |#1| (-795)) @@ -1411,13 +1411,13 @@ (((|#4| |#4|) -12 (|has| |#4| (-291 |#4|)) (|has| |#4| (-1027)))) (((|#1|) |has| |#1| (-162))) (((|#4| |#4|) -12 (|has| |#4| (-291 |#4|)) (|has| |#4| (-1027)))) -(((|#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)))) +(((|#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)))) (|has| |#2| (-795)) (|has| |#1| (-795)) -(-1476 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-850))) ((($ $) . T) ((#0=(-388 (-530)) #0#) . T)) ((((-530) |#2|) . T)) -(((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)))) +(((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)))) (|has| |#1| (-330)) (((|#3| |#3|) -12 (|has| |#3| (-291 |#3|)) (|has| |#3| (-1027)))) ((($) . T) (((-388 (-530))) . T)) @@ -1425,7 +1425,7 @@ (|has| |#1| (-768)) (|has| |#1| (-768)) (((|#1|) . T)) -(-1476 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330))) (|has| |#1| (-793)) (|has| |#1| (-793)) (|has| |#1| (-793)) @@ -1434,13 +1434,13 @@ ((((-530)) . T) (($) . T) (((-388 (-530))) . T)) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) (|has| |#1| (-37 (-388 (-530)))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-1099)) |has| |#1| (-841 (-1099))) (((-1012)) . T)) (((|#1|) . T)) (|has| |#1| (-793)) -(((#0=(-2 (|:| -2940 (-1082)) (|:| -1806 (-51))) #0#) |has| (-2 (|:| -2940 (-1082)) (|:| -1806 (-51))) (-291 (-2 (|:| -2940 (-1082)) (|:| -1806 (-51)))))) +(((#0=(-2 (|:| -3078 (-1082)) (|:| -1874 (-51))) #0#) |has| (-2 (|:| -3078 (-1082)) (|:| -1874 (-51))) (-291 (-2 (|:| -3078 (-1082)) (|:| -1874 (-51)))))) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (|has| |#1| (-1027)) (((|#1|) . T)) @@ -1459,7 +1459,7 @@ (((|#1|) . T)) ((((-137)) . T)) (((|#2|) |has| |#2| (-162))) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((|#1|) . T)) (|has| |#1| (-138)) (|has| |#1| (-140)) @@ -1481,32 +1481,32 @@ (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027))) ((#0=(-2 (|:| -2940 (-1082)) (|:| -1806 |#1|)) #0#) |has| (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|)) (-291 (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))))) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-850))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-850))) +(((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027))) ((#0=(-2 (|:| -3078 (-1082)) (|:| -1874 |#1|)) #0#) |has| (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|)) (-291 (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-850))) (((|#1|) . T) (($) . T)) (((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) (((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(((|#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)))) +(((|#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)))) (|has| |#1| (-795)) (|has| |#1| (-522)) ((((-543 |#1|)) . T)) ((($) . T)) (((|#2|) . T)) -(-1476 (-12 (|has| |#1| (-344)) (|has| |#2| (-768))) (-12 (|has| |#1| (-344)) (|has| |#2| (-795)))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (-12 (|has| |#1| (-344)) (|has| |#2| (-768))) (-12 (|has| |#1| (-344)) (|has| |#2| (-795)))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) ((((-851 |#1|)) . T)) (((|#1| (-474 |#1| |#3|) (-474 |#1| |#2|)) . T)) (((|#1| |#4| |#5|) . T)) (((|#1| (-719)) . T)) ((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) |has| |#1| (-162)) (($) |has| |#1| (-522))) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-1097 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) -(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522)))) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-1097 |#1| |#2| |#3|)) |has| |#1| (-344)) ((|#1|) |has| |#1| (-162))) +(((|#1|) |has| |#1| (-162)) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522)))) ((($) |has| |#1| (-522)) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) . T)) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) . T)) ((((-388 |#2|)) . T) (((-388 (-530))) . T) (($) . T)) ((((-622 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1514,17 +1514,17 @@ ((((-804)) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) ((((-804)) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) ((((-804)) . T)) ((((-804)) . T)) ((((-804)) . T)) (((|#2|) . T)) -(-1476 (|has| |#3| (-25)) (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-349)) (|has| |#3| (-675)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984)) (|has| |#3| (-1027))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#3| (-25)) (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-349)) (|has| |#3| (-675)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984)) (|has| |#3| (-1027))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((((-388 (-530))) |has| |#1| (-975 (-388 (-530)))) (((-530)) |has| |#1| (-975 (-530))) ((|#1|) . T)) (|has| |#1| (-1121)) (|has| |#1| (-1121)) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (|has| |#1| (-1121)) (|has| |#1| (-1121)) (((|#3| |#3|) . T)) @@ -1537,43 +1537,43 @@ (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) ((((-1082) (-51)) . T)) (|has| |#1| (-1027)) -(-1476 (|has| |#2| (-768)) (|has| |#2| (-795))) +(-1461 (|has| |#2| (-768)) (|has| |#2| (-795))) (((|#1|) . T)) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) (((-388 (-530))) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) (((-388 (-530))) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) (((|#1|) |has| |#1| (-162)) (($) . T)) ((($) . T)) ((((-1097 |#1| |#2| |#3|)) -12 (|has| (-1097 |#1| |#2| |#3|) (-291 (-1097 |#1| |#2| |#3|))) (|has| |#1| (-344)))) ((((-804)) . T)) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((($) . T)) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) ((((-804)) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-850))) (|has| |#2| (-850)) (|has| |#1| (-344)) (((|#2|) |has| |#2| (-1027))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((($) . T) ((|#2|) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-850))) (|has| |#1| (-850)) ((((-506)) . T) (((-388 (-1095 (-530)))) . T) (((-208)) . T) (((-360)) . T)) ((((-360)) . T) (((-208)) . T) (((-804)) . T)) (|has| |#1| (-850)) (|has| |#1| (-850)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) ((($ $) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((($ $) . T)) ((((-530) (-110)) . T)) ((($) . T)) (((|#1|) . T)) ((((-530)) . T)) ((((-110)) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (|has| |#1| (-37 (-388 (-530)))) (((|#1| (-530)) . T)) ((($) . T)) @@ -1595,7 +1595,7 @@ (((|#1| (-1145 |#1| |#2| |#3|)) . T)) (((|#1| (-719)) . T)) (((|#1|) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-804)) . T)) (|has| |#1| (-1027)) ((((-1082) |#1|) . T)) @@ -1615,18 +1615,18 @@ (((|#1|) . T)) ((((-530)) . T)) ((((-804)) . T)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-330))) (|has| |#1| (-140)) ((((-804)) . T)) (((|#3|) . T)) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((((-804)) . T)) ((((-1166 |#2| |#3| |#4|)) . T) (((-1167 |#1| |#2| |#3| |#4|)) . T)) ((((-804)) . T)) -((((-47)) -12 (|has| |#1| (-522)) (|has| |#1| (-975 (-530)))) (((-570 $)) . T) ((|#1|) . T) (((-530)) |has| |#1| (-975 (-530))) (((-388 (-530))) -1476 (-12 (|has| |#1| (-522)) (|has| |#1| (-975 (-530)))) (|has| |#1| (-975 (-388 (-530))))) (((-388 (-893 |#1|))) |has| |#1| (-522)) (((-893 |#1|)) |has| |#1| (-984)) (((-1099)) . T)) +((((-47)) -12 (|has| |#1| (-522)) (|has| |#1| (-975 (-530)))) (((-570 $)) . T) ((|#1|) . T) (((-530)) |has| |#1| (-975 (-530))) (((-388 (-530))) -1461 (-12 (|has| |#1| (-522)) (|has| |#1| (-975 (-530)))) (|has| |#1| (-975 (-388 (-530))))) (((-388 (-893 |#1|))) |has| |#1| (-522)) (((-893 |#1|)) |has| |#1| (-984)) (((-1099)) . T)) (((|#1|) . T) (($) . T)) (((|#1| (-719)) . T)) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) |has| |#1| (-162))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) |has| |#1| (-162))) (((|#1|) |has| |#1| (-291 |#1|))) ((((-1167 |#1| |#2| |#3| |#4|)) . T)) ((((-530)) |has| |#1| (-827 (-530))) (((-360)) |has| |#1| (-827 (-360)))) @@ -1634,14 +1634,14 @@ (|has| |#1| (-522)) (((|#1|) . T)) ((((-804)) . T)) -(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (((|#1|) |has| |#1| (-162))) ((($) |has| |#1| (-522)) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) (((|#1|) . T)) (((|#3|) |has| |#3| (-1027))) -(((|#2|) -1476 (|has| |#2| (-162)) (|has| |#2| (-344)))) +(((|#2|) -1461 (|has| |#2| (-162)) (|has| |#2| (-344)))) ((((-1166 |#2| |#3| |#4|)) . T)) ((((-110)) . T)) (|has| |#1| (-768)) @@ -1651,8 +1651,8 @@ (|has| |#1| (-793)) (|has| |#1| (-793)) (((|#1| (-530) (-1012)) . T)) -(-1476 (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +(-1461 (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1| (-388 (-530)) (-1012)) . T)) (((|#1| (-719) (-1012)) . T)) (|has| |#1| (-795)) @@ -1668,28 +1668,28 @@ (((|#1|) . T)) (|has| |#1| (-1027)) ((((-530)) -12 (|has| |#1| (-344)) (|has| |#2| (-593 (-530)))) ((|#2|) |has| |#1| (-344))) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((|#2|) |has| |#2| (-162))) (((|#1|) |has| |#1| (-162))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) ((((-804)) . T)) (|has| |#3| (-793)) ((((-804)) . T)) ((((-1166 |#2| |#3| |#4|) (-300 |#2| |#3| |#4|)) . T)) ((((-804)) . T)) -(((|#1| |#1|) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-984)))) +(((|#1| |#1|) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-984)))) (((|#1|) . T)) ((((-530)) . T)) ((((-530)) . T)) -(((|#1|) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-984)))) +(((|#1|) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-984)))) (((|#2|) |has| |#2| (-344))) ((($) . T) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-344))) (|has| |#1| (-795)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) |has| (-2 (|:| -2940 (-1099)) (|:| -1806 (-51))) (-291 (-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-850))) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) |has| (-2 (|:| -3078 (-1099)) (|:| -1874 (-51))) (-291 (-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-850))) (((|#2|) . T) (((-530)) |has| |#2| (-593 (-530)))) ((((-804)) . T)) ((((-804)) . T)) @@ -1725,18 +1725,18 @@ (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) (((|#1|) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-793)) (|has| |#2| (-984))) (((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) . T) (($ $) . T)) ((((-804)) . T)) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) ((($) . T) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (|has| |#1| (-344)) (|has| |#1| (-344)) (|has| (-388 |#2|) (-216)) (|has| |#1| (-850)) (((|#2|) |has| |#2| (-984))) -(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (|has| |#1| (-344)) (((|#1|) |has| |#1| (-162))) (((|#1| |#1|) . T)) @@ -1761,7 +1761,7 @@ (((|#1| (-388 (-530)) (-1012)) . T)) (((|#1| (-719) (-1012)) . T)) (((#0=(-388 |#2|) #0#) . T) ((#1=(-388 (-530)) #1#) . T) (($ $) . T)) -(((|#1|) . T) (((-530)) -1476 (|has| (-388 (-530)) (-975 (-530))) (|has| |#1| (-975 (-530)))) (((-388 (-530))) . T)) +(((|#1|) . T) (((-530)) -1461 (|has| (-388 (-530)) (-975 (-530))) (|has| |#1| (-975 (-530)))) (((-388 (-530))) . T)) (((|#1| (-561 |#1| |#3|) (-561 |#1| |#2|)) . T)) (((|#1|) |has| |#1| (-162))) (((|#1|) . T)) @@ -1780,24 +1780,24 @@ ((((-647)) . T)) (((|#2|) |has| |#2| (-162))) (|has| |#2| (-793)) -((((-110)) |has| |#1| (-1027)) (((-804)) -1476 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)) (|has| |#1| (-1039)) (|has| |#1| (-1027)))) +((((-110)) |has| |#1| (-1027)) (((-804)) -1461 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)) (|has| |#1| (-1039)) (|has| |#1| (-1027)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 (-51)))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 (-51)))) . T)) ((((-804)) . T)) ((((-530) |#1|) . T)) ((((-647)) . T) (((-388 (-530))) . T) (((-530)) . T)) (((|#1| |#1|) |has| |#1| (-162))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) ((((-360)) . T)) ((((-647)) . T)) ((((-388 (-530))) . #0=(|has| |#2| (-344))) (($) . #0#)) (((|#1|) |has| |#1| (-162))) ((((-388 (-893 |#1|))) . T)) (((|#2| |#2|) . T)) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (((|#2|) . T)) (|has| |#2| (-795)) (((|#3|) |has| |#3| (-984))) @@ -1807,14 +1807,14 @@ (|has| |#1| (-795)) ((((-1099)) |has| |#2| (-841 (-1099)))) ((((-804)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-388 (-530))) . T) (($) . T)) (|has| |#1| (-453)) (|has| |#1| (-349)) (|has| |#1| (-349)) (|has| |#1| (-349)) (|has| |#1| (-344)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-453)) (|has| |#1| (-522)) (|has| |#1| (-984)) (|has| |#1| (-1039))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-453)) (|has| |#1| (-522)) (|has| |#1| (-984)) (|has| |#1| (-1039))) (|has| |#1| (-37 (-388 (-530)))) ((((-114 |#1|)) . T)) ((((-114 |#1|)) . T)) @@ -1835,11 +1835,11 @@ (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-795)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-140)) (|has| |#1| (-138)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)))) ((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)))) ((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) (((|#2|) . T)) (((|#3|) . T)) ((((-114 |#1|)) . T)) @@ -1857,11 +1857,11 @@ ((((-506)) |has| |#1| (-572 (-506))) (((-833 (-530))) |has| |#1| (-572 (-833 (-530)))) (((-833 (-360))) |has| |#1| (-572 (-833 (-360)))) (((-360)) . #0=(|has| |#1| (-960))) (((-208)) . #0#)) (((|#1|) |has| |#1| (-344))) ((((-804)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((($ $) . T) (((-570 $) $) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) ((($) . T) (((-1167 |#1| |#2| |#3| |#4|)) . T) (((-388 (-530))) . T)) -((($) -1476 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-522))) +((($) -1461 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-522))) (|has| |#1| (-344)) (|has| |#1| (-344)) (|has| |#1| (-344)) @@ -1872,11 +1872,11 @@ ((((-360)) . T)) (((|#3|) -12 (|has| |#3| (-291 |#3|)) (|has| |#3| (-1027)))) ((((-804)) . T)) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-850))) (((|#1|) . T)) (|has| |#1| (-795)) (|has| |#1| (-795)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) (((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) (|has| |#1| (-1027)) @@ -1885,13 +1885,13 @@ (|has| |#1| (-138)) (|has| |#1| (-140)) ((((-530)) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((#0=(-1166 |#2| |#3| |#4|)) . T) (((-388 (-530))) |has| #0# (-37 (-388 (-530)))) (($) . T)) ((((-530)) . T)) (|has| |#1| (-344)) -(-1476 (-12 (|has| (-1173 |#1| |#2| |#3|) (-140)) (|has| |#1| (-344))) (|has| |#1| (-140))) -(-1476 (-12 (|has| (-1173 |#1| |#2| |#3|) (-138)) (|has| |#1| (-344))) (|has| |#1| (-138))) +(-1461 (-12 (|has| (-1173 |#1| |#2| |#3|) (-140)) (|has| |#1| (-344))) (|has| |#1| (-140))) +(-1461 (-12 (|has| (-1173 |#1| |#2| |#3|) (-138)) (|has| |#1| (-344))) (|has| |#1| (-138))) (|has| |#1| (-344)) (|has| |#1| (-138)) (|has| |#1| (-140)) @@ -1908,18 +1908,18 @@ (((|#1| |#2|) . T)) (((|#1|) . T) (((-530)) |has| |#1| (-593 (-530)))) (((|#3|) |has| |#3| (-162))) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) ((((-530)) . T)) (((|#1| $) |has| |#1| (-268 |#1| |#1|))) ((((-388 (-530))) . T) (($) . T) (((-388 |#1|)) . T) ((|#1|) . T)) ((((-804)) . T)) (((|#3|) . T)) -(((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-272)) (|has| |#1| (-344))) ((#0=(-388 (-530)) #0#) |has| |#1| (-344))) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) . T)) +(((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-272)) (|has| |#1| (-344))) ((#0=(-388 (-530)) #0#) |has| |#1| (-344))) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) . T)) ((($) . T)) ((((-530) |#1|) . T)) ((((-1099)) |has| (-388 |#2|) (-841 (-1099)))) -(((|#1|) . T) (($) -1476 (|has| |#1| (-272)) (|has| |#1| (-344))) (((-388 (-530))) |has| |#1| (-344))) +(((|#1|) . T) (($) -1461 (|has| |#1| (-272)) (|has| |#1| (-344))) (((-388 (-530))) |has| |#1| (-344))) ((((-506)) |has| |#2| (-572 (-506)))) ((((-637 |#2|)) . T) (((-804)) . T)) (((|#1|) . T)) @@ -1927,8 +1927,8 @@ (((|#4|) -12 (|has| |#4| (-291 |#4|)) (|has| |#4| (-1027)))) ((((-811 |#1|)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) -(-1476 (|has| |#4| (-741)) (|has| |#4| (-793))) -(-1476 (|has| |#3| (-741)) (|has| |#3| (-793))) +(-1461 (|has| |#4| (-741)) (|has| |#4| (-793))) +(-1461 (|has| |#3| (-741)) (|has| |#3| (-793))) ((((-804)) . T)) ((((-804)) . T)) (((|#4|) -12 (|has| |#4| (-291 |#4|)) (|has| |#4| (-1027)))) @@ -1944,17 +1944,17 @@ ((((-388 (-530))) . T) (($) . T)) ((((-388 (-530))) . T) (($) . T)) ((((-388 (-530))) . T) (($) . T)) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-1139))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-1139))) ((($) . T)) ((((-388 (-530))) |has| #0=(-388 |#2|) (-975 (-388 (-530)))) (((-530)) |has| #0# (-975 (-530))) ((#0#) . T)) (((|#2|) . T) (((-530)) |has| |#2| (-593 (-530)))) (((|#1| (-719)) . T)) (|has| |#1| (-795)) (((|#1|) . T) (((-530)) |has| |#1| (-593 (-530)))) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) (((-388 (-530))) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) (((-388 (-530))) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) ((((-530)) . T)) (|has| |#1| (-37 (-388 (-530)))) -((((-2 (|:| -2940 (-1082)) (|:| -1806 (-51)))) |has| (-2 (|:| -2940 (-1082)) (|:| -1806 (-51))) (-291 (-2 (|:| -2940 (-1082)) (|:| -1806 (-51)))))) +((((-2 (|:| -3078 (-1082)) (|:| -1874 (-51)))) |has| (-2 (|:| -3078 (-1082)) (|:| -1874 (-51))) (-291 (-2 (|:| -3078 (-1082)) (|:| -1874 (-51)))))) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (|has| |#1| (-793)) (|has| |#1| (-37 (-388 (-530)))) @@ -1979,24 +1979,24 @@ (((|#1| |#2|) . T)) ((((-137)) . T)) ((((-728 |#1| (-806 |#2|))) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (|has| |#1| (-1121)) (((|#1|) . T)) -(-1476 (|has| |#3| (-25)) (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-349)) (|has| |#3| (-675)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984)) (|has| |#3| (-1027))) +(-1461 (|has| |#3| (-25)) (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-349)) (|has| |#3| (-675)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984)) (|has| |#3| (-1027))) ((((-1099) |#1|) |has| |#1| (-491 (-1099) |#1|))) (((|#2|) . T)) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((((-851 |#1|)) . T)) ((($) . T)) ((((-388 (-893 |#1|))) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) ((((-506)) |has| |#4| (-572 (-506)))) ((((-804)) . T) (((-597 |#4|)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-793)) -(((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027))) (((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) |has| (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|)) (-291 (-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))))) +(((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027))) (((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) |has| (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|)) (-291 (-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))))) (|has| |#1| (-1027)) (|has| |#1| (-344)) (|has| |#1| (-795)) @@ -2004,16 +2004,16 @@ (((|#1|) . T)) (((|#1|) . T)) ((($) . T) (((-388 (-530))) . T)) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) |has| |#1| (-162))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) |has| |#1| (-162))) (|has| |#1| (-138)) (|has| |#1| (-140)) -(-1476 (-12 (|has| (-1097 |#1| |#2| |#3|) (-140)) (|has| |#1| (-344))) (|has| |#1| (-140))) -(-1476 (-12 (|has| (-1097 |#1| |#2| |#3|) (-138)) (|has| |#1| (-344))) (|has| |#1| (-138))) +(-1461 (-12 (|has| (-1097 |#1| |#2| |#3|) (-140)) (|has| |#1| (-344))) (|has| |#1| (-140))) +(-1461 (-12 (|has| (-1097 |#1| |#2| |#3|) (-138)) (|has| |#1| (-344))) (|has| |#1| (-138))) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-140)) (|has| |#1| (-138)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-344))) (|has| |#1| (-793)) (((|#1| |#2|) . T)) @@ -2036,9 +2036,9 @@ ((((-804)) . T)) ((((-804)) . T)) ((((-506)) |has| |#1| (-572 (-506)))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-1099) |#1|) |has| |#1| (-491 (-1099) |#1|)) ((|#1| |#1|) |has| |#1| (-291 |#1|))) -(((|#1|) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)))) +(((|#1|) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)))) ((((-297 |#1|)) . T)) (((|#2|) |has| |#2| (-344))) (((|#2|) . T)) @@ -2059,13 +2059,13 @@ (|has| |#1| (-138)) (|has| |#1| (-140)) ((($ $) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)) (|has| |#1| (-1039)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)) (|has| |#1| (-1039)) (|has| |#1| (-1027))) (|has| |#1| (-522)) (((|#2|) . T)) ((((-530)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1|) . T)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) ((((-543 |#1|)) . T)) ((($) . T)) (((|#1| (-57 |#1|) (-57 |#1|)) . T)) @@ -2074,7 +2074,7 @@ ((($) . T)) (((|#1|) . T)) ((((-804)) . T)) -(((|#2|) |has| |#2| (-6 (-4272 "*")))) +(((|#2|) |has| |#2| (-6 (-4271 "*")))) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2091,12 +2091,12 @@ (((|#1| |#2|) . T)) ((((-1099) |#1|) . T)) (((|#4|) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((((-1099) (-51)) . T)) ((((-1166 |#2| |#3| |#4|) (-300 |#2| |#3| |#4|)) . T)) ((((-388 (-530))) |has| |#1| (-975 (-388 (-530)))) (((-530)) |has| |#1| (-975 (-530))) ((|#1|) . T)) ((((-804)) . T)) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-349)) (|has| |#2| (-675)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984)) (|has| |#2| (-1027))) (((#0=(-1167 |#1| |#2| |#3| |#4|) #0#) . T) ((#1=(-388 (-530)) #1#) . T) (($ $) . T)) (((|#1| |#1|) |has| |#1| (-162)) ((#0=(-388 (-530)) #0#) |has| |#1| (-522)) (($ $) |has| |#1| (-522))) (((|#1|) . T) (($) . T) (((-388 (-530))) . T)) @@ -2115,14 +2115,14 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) (((|#2| |#3|) . T)) -(-1476 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-344)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) (((|#1| (-502 |#2|)) . T)) (((|#1| (-719)) . T)) (((|#1| (-502 (-1017 (-1099)))) . T)) (((|#1|) |has| |#1| (-162))) (((|#1|) . T)) (|has| |#2| (-850)) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) ((((-804)) . T)) ((($ $) . T) ((#0=(-1166 |#2| |#3| |#4|) #0#) . T) ((#1=(-388 (-530)) #1#) |has| #0# (-37 (-388 (-530))))) ((((-851 |#1|)) . T)) @@ -2131,13 +2131,13 @@ ((($) . T)) ((($) . T)) (|has| |#1| (-344)) -(-1476 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330)) (|has| |#1| (-522))) (|has| |#1| (-344)) ((($) . T) ((#0=(-1166 |#2| |#3| |#4|)) . T) (((-388 (-530))) |has| #0# (-37 (-388 (-530))))) (((|#1| |#2|) . T)) ((((-1097 |#1| |#2| |#3|)) |has| |#1| (-344))) -(-1476 (-12 (|has| |#1| (-289)) (|has| |#1| (-850))) (|has| |#1| (-344)) (|has| |#1| (-330))) -(-1476 (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) +(-1461 (-12 (|has| |#1| (-289)) (|has| |#1| (-850))) (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-841 (-1099))) (|has| |#1| (-984))) ((((-530)) |has| |#1| (-593 (-530))) ((|#1|) . T)) (((|#1| |#2|) . T)) ((((-804)) . T)) @@ -2169,27 +2169,27 @@ (((|#1|) |has| |#1| (-162))) ((((-804)) . T)) (((|#4| |#4|) -12 (|has| |#4| (-291 |#4|)) (|has| |#4| (-1027)))) -(((|#2|) -1476 (|has| |#2| (-6 (-4272 "*"))) (|has| |#2| (-162)))) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(((|#2|) -1461 (|has| |#2| (-6 (-4271 "*"))) (|has| |#2| (-162)))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (|has| |#2| (-795)) (|has| |#2| (-850)) (|has| |#1| (-850)) (((|#2|) |has| |#2| (-162))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-344))) ((((-804)) . T)) ((((-804)) . T)) ((((-506)) . T) (((-530)) . T) (((-833 (-530))) . T) (((-360)) . T) (((-208)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 (-51)))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 (-51)))) . T)) (((|#1|) . T)) ((((-804)) . T)) (((|#1| |#2|) . T)) (((|#1| (-388 (-530))) . T)) (((|#1|) . T)) -(-1476 (|has| |#1| (-272)) (|has| |#1| (-344))) +(-1461 (|has| |#1| (-272)) (|has| |#1| (-344))) ((((-137)) . T)) ((((-388 |#2|)) . T) (((-388 (-530))) . T) (($) . T)) (|has| |#1| (-793)) @@ -2204,7 +2204,7 @@ ((((-388 (-530))) . T) (($) . T)) ((((-804)) . T)) ((((-804)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-804)) . T)) ((((-804)) . T)) @@ -2215,7 +2215,7 @@ (((|#1|) . T)) ((((-597 (-137))) . T) (((-1082)) . T)) ((((-804)) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) ((((-1099) |#1|) |has| |#1| (-491 (-1099) |#1|)) ((|#1| |#1|) |has| |#1| (-291 |#1|))) (|has| |#1| (-795)) ((((-804)) . T)) @@ -2227,16 +2227,16 @@ ((((-804)) . T) (((-597 |#4|)) . T)) (((|#2|) . T)) ((((-851 |#1|)) . T) (((-388 (-530))) . T) (($) . T)) -(-1476 (|has| |#4| (-162)) (|has| |#4| (-675)) (|has| |#4| (-793)) (|has| |#4| (-984))) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-675)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#4| (-162)) (|has| |#4| (-675)) (|has| |#4| (-793)) (|has| |#4| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-675)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((((-1099) (-51)) . T)) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-793)) (|has| |#2| (-984))) (|has| |#1| (-850)) (|has| |#1| (-850)) (((|#2|) . T)) @@ -2251,12 +2251,12 @@ (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (|has| |#1| (-768)) (((#0=(-851 |#1|) #0#) . T) (($ $) . T) ((#1=(-388 (-530)) #1#) . T)) ((((-388 |#2|)) . T)) (|has| |#1| (-793)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) . T) ((#1=(-530) #1#) . T) (($ $) . T)) ((((-851 |#1|)) . T) (($) . T) (((-388 (-530))) . T)) (((|#2|) |has| |#2| (-984)) (((-530)) -12 (|has| |#2| (-593 (-530))) (|has| |#2| (-984)))) @@ -2266,25 +2266,25 @@ (|has| |#1| (-138)) (((|#2|) . T)) ((((-804)) . T)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) . T)) -(((#0=(-51)) . T) (((-2 (|:| -2940 (-1099)) (|:| -1806 #0#))) . T)) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3078 (-1099)) (|:| -1874 #0#))) . T)) (|has| |#1| (-330)) ((((-530)) . T)) ((((-804)) . T)) (((#0=(-1167 |#1| |#2| |#3| |#4|) $) |has| #0# (-268 #0# #0#))) (|has| |#1| (-344)) (((#0=(-1012) |#1|) . T) ((#0# $) . T) (($ $) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) (((#0=(-388 (-530)) #0#) . T) ((#1=(-647) #1#) . T) (($ $) . T)) ((((-297 |#1|)) . T) (($) . T)) (((|#1|) . T) (((-388 (-530))) |has| |#1| (-344))) (|has| |#1| (-1027)) (((|#1|) . T)) -(((|#1|) -1476 (|has| |#2| (-348 |#1|)) (|has| |#2| (-398 |#1|)))) -(((|#1|) -1476 (|has| |#2| (-348 |#1|)) (|has| |#2| (-398 |#1|)))) +(((|#1|) -1461 (|has| |#2| (-348 |#1|)) (|has| |#2| (-398 |#1|)))) +(((|#1|) -1461 (|has| |#2| (-348 |#1|)) (|has| |#2| (-398 |#1|)))) (((|#2|) . T)) ((((-388 (-530))) . T) (((-647)) . T) (($) . T)) (((|#3| |#3|) . T)) @@ -2303,7 +2303,7 @@ (((|#2|) . T)) (((|#1|) . T)) ((((-530)) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (((|#2|) . T) (((-530)) |has| |#2| (-593 (-530)))) (((|#1| |#2|) . T)) ((($) . T)) @@ -2340,7 +2340,7 @@ (|has| |#2| (-960)) ((($) . T)) (|has| |#1| (-850)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2348,24 +2348,24 @@ ((($) . T)) (|has| |#1| (-344)) ((((-851 |#1|)) . T)) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((($ $) . T) ((#0=(-388 (-530)) #0#) . T)) -(-1476 (|has| |#1| (-349)) (|has| |#1| (-795))) +(-1461 (|has| |#1| (-349)) (|has| |#1| (-795))) (((|#1|) . T)) ((((-804)) . T)) ((((-1099)) -12 (|has| |#1| (-15 * (|#1| (-388 (-530)) |#1|))) (|has| |#1| (-841 (-1099))))) ((((-388 |#2|) |#3|) . T)) ((($) . T) (((-388 (-530))) . T)) ((((-719) |#1|) . T)) -(((|#2| (-223 (-2167 |#1|) (-719))) . T)) +(((|#2| (-223 (-2267 |#1|) (-719))) . T)) (((|#1| (-502 |#3|)) . T)) ((((-388 (-530))) . T)) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((((-804)) . T)) -(((#0=(-2 (|:| -2940 (-1099)) (|:| -1806 (-51))) #0#) |has| (-2 (|:| -2940 (-1099)) (|:| -1806 (-51))) (-291 (-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))))) +(((#0=(-2 (|:| -3078 (-1099)) (|:| -1874 (-51))) #0#) |has| (-2 (|:| -3078 (-1099)) (|:| -1874 (-51))) (-291 (-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))))) (|has| |#1| (-850)) (|has| |#2| (-344)) -(-1476 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((((-159 (-360))) . T) (((-208)) . T) (((-360)) . T)) ((((-804)) . T)) (((|#1|) . T)) @@ -2382,11 +2382,11 @@ (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) -(-1476 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330))) (|has| |#1| (-37 (-388 (-530)))) (-12 (|has| |#1| (-515)) (|has| |#1| (-776))) ((((-804)) . T)) -((((-1099)) -1476 (-12 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (|has| |#1| (-841 (-1099)))) (-12 (|has| |#1| (-344)) (|has| |#2| (-841 (-1099)))))) +((((-1099)) -1461 (-12 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (|has| |#1| (-841 (-1099)))) (-12 (|has| |#1| (-344)) (|has| |#2| (-841 (-1099)))))) (|has| |#1| (-344)) ((((-1099)) -12 (|has| |#1| (-15 * (|#1| (-388 (-530)) |#1|))) (|has| |#1| (-841 (-1099))))) (|has| |#1| (-344)) @@ -2396,7 +2396,7 @@ (((|#1|) . T)) (((|#2|) |has| |#1| (-344))) (((|#2|) |has| |#1| (-344))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-162))) (((|#1|) . T)) @@ -2421,30 +2421,30 @@ ((((-360)) -12 (|has| |#1| (-344)) (|has| |#2| (-827 (-360)))) (((-530)) -12 (|has| |#1| (-344)) (|has| |#2| (-827 (-530))))) (|has| |#1| (-344)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (|has| |#1| (-344)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) (|has| |#1| (-344)) (|has| |#1| (-522)) (((|#4| |#4|) -12 (|has| |#4| (-291 |#4|)) (|has| |#4| (-1027)))) (((|#3|) . T)) (((|#1|) . T)) -(-1476 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) (((|#2|) . T)) (((|#2|) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (|has| |#1| (-37 (-388 (-530)))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-388 (-530)))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) (|has| |#1| (-140)) ((((-1082) |#1|) . T)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) (|has| |#1| (-140)) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-349))) (|has| |#1| (-140)) ((((-543 |#1|)) . T)) ((($) . T)) @@ -2452,7 +2452,7 @@ (|has| |#1| (-522)) (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-37 (-388 (-530)))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-330))) (|has| |#1| (-140)) ((((-804)) . T)) ((($) . T)) @@ -2477,7 +2477,7 @@ (|has| |#1| (-739)) (|has| |#1| (-739)) ((((-506)) |has| |#1| (-572 (-506)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-112)) . T) ((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2498,7 +2498,7 @@ ((((-530)) . T)) ((((-804)) . T)) ((((-530)) . T)) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) ((((-159 (-360))) . T) (((-208)) . T) (((-360)) . T)) ((((-804)) . T)) ((((-804)) . T)) @@ -2510,9 +2510,9 @@ (((|#1|) . T) (($) . T) (((-388 (-530))) . T)) (|has| |#1| (-344)) (|has| |#1| (-344)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)) (|has| |#1| (-1039)) (|has| |#1| (-1027))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-453)) (|has| |#1| (-675)) (|has| |#1| (-841 (-1099))) (|has| |#1| (-984)) (|has| |#1| (-1039)) (|has| |#1| (-1027))) (|has| |#1| (-1075)) ((((-530) |#1|) . T)) (((|#1|) . T)) @@ -2530,8 +2530,8 @@ (((|#1|) . T)) (|has| |#1| (-522)) ((((-388 |#2|)) . T) (((-388 (-530))) . T) (($) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) ((((-360)) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2540,7 +2540,7 @@ (|has| |#1| (-522)) (|has| |#1| (-1027)) ((((-728 |#1| (-806 |#2|))) |has| (-728 |#1| (-806 |#2|)) (-291 (-728 |#1| (-806 |#2|))))) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) (((|#1|) . T)) (((|#2| |#3|) . T)) (|has| |#2| (-850)) @@ -2550,12 +2550,12 @@ (|has| |#1| (-216)) (((|#1| (-502 (-1017 (-1099)))) . T)) (|has| |#2| (-344)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 (-51)))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 (-51)))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) ((((-804)) . T)) ((((-804)) . T)) -(-1476 (|has| |#3| (-741)) (|has| |#3| (-793))) +(-1461 (|has| |#3| (-741)) (|has| |#3| (-793))) ((((-804)) . T)) ((((-1046)) . T) (((-804)) . T)) ((((-804)) . T)) @@ -2565,8 +2565,8 @@ ((((-530)) . T)) (((|#3|) . T)) ((((-804)) . T)) -(-1476 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330))) -(-1476 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) +(-1461 (|has| |#1| (-289)) (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-162)) (|has| |#1| (-522)) (|has| |#1| (-984))) (((#0=(-543 |#1|) #0#) . T) (($ $) . T) ((#1=(-388 (-530)) #1#) . T)) ((($ $) . T) ((#0=(-388 (-530)) #0#) . T)) (((|#1|) |has| |#1| (-162))) @@ -2574,12 +2574,12 @@ ((((-543 |#1|)) . T) (($) . T) (((-388 (-530))) . T)) ((($) . T) (((-388 (-530))) . T)) ((($) . T) (((-388 (-530))) . T)) -(((|#2|) |has| |#2| (-6 (-4272 "*")))) +(((|#2|) |has| |#2| (-6 (-4271 "*")))) (((|#1|) . T)) (((|#1|) . T)) ((((-804)) |has| |#1| (-571 (-804)))) ((((-276 |#3|)) . T)) -(((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530)))) ((|#2| |#2|) . T) (($ $) -1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +(((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530)))) ((|#2| |#2|) . T) (($ $) -1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) (((|#2| |#2|) . T) ((|#6| |#6|) . T)) (((|#1|) . T)) ((($) . T) (((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T)) @@ -2587,20 +2587,20 @@ (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) (((|#1|) . T) (((-388 (-530))) . T) (($) . T)) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) (((|#2|) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T) (($) -1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T) (($) -1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) (((|#2|) . T) ((|#6|) . T)) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) ((((-804)) . T)) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (|has| |#2| (-850)) (|has| |#1| (-850)) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1|) . T)) -((((-2 (|:| -2940 (-1082)) (|:| -1806 |#1|))) . T)) +((((-2 (|:| -3078 (-1082)) (|:| -1874 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) . T)) @@ -2614,10 +2614,10 @@ (((|#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027)))) (((#0=(-388 (-530)) #0#) . T)) ((((-388 (-530))) . T)) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) (((|#1|) . T)) (((|#1|) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((((-506)) . T)) ((((-804)) . T)) ((((-1099)) |has| |#2| (-841 (-1099))) (((-1012)) . T)) @@ -2632,12 +2632,12 @@ ((($ $) . T) ((#0=(-388 (-530)) #0#) . T)) ((((-1099)) |has| |#1| (-841 (-1099)))) ((((-851 |#1|)) . T) (((-388 (-530))) . T) (($) . T)) -((($) . T) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) . T)) -(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-522)))) +((($) . T) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#1|) . T)) +(((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530)))) ((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-522)))) ((($) . T) (((-388 (-530))) . T)) (((|#1|) . T) (((-388 (-530))) . T) (((-530)) . T) (($) . T)) (((|#2|) |has| |#2| (-984)) (((-530)) -12 (|has| |#2| (-593 (-530))) (|has| |#2| (-984)))) -((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-522)))) +((((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-522)))) (|has| |#1| (-522)) (((|#1|) |has| |#1| (-344))) ((((-530)) . T)) @@ -2656,8 +2656,8 @@ ((((-804)) . T)) (|has| |#2| (-768)) (|has| |#2| (-768)) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#2|) |has| |#1| (-344)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) . T)) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#2|) |has| |#1| (-344)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1|) . T) (((-530)) |has| |#1| (-975 (-530))) (((-388 (-530))) |has| |#1| (-975 (-388 (-530))))) ((((-530)) |has| |#1| (-827 (-530))) (((-360)) |has| |#1| (-827 (-360)))) @@ -2683,12 +2683,12 @@ (((|#2| (-719)) . T)) ((((-1099)) . T)) ((((-811 |#1|)) . T)) -(-1476 (|has| |#3| (-25)) (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984))) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#3| (-25)) (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((((-804)) . T)) (((|#1|) . T)) -(-1476 (|has| |#2| (-741)) (|has| |#2| (-793))) -(-1476 (-12 (|has| |#1| (-741)) (|has| |#2| (-741))) (-12 (|has| |#1| (-795)) (|has| |#2| (-795)))) +(-1461 (|has| |#2| (-741)) (|has| |#2| (-793))) +(-1461 (-12 (|has| |#1| (-741)) (|has| |#2| (-741))) (-12 (|has| |#1| (-795)) (|has| |#2| (-795)))) ((((-811 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-349)) @@ -2714,7 +2714,7 @@ (((|#1|) . T)) ((((-804)) . T)) (|has| |#2| (-850)) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) . T)) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) . T)) ((((-506)) |has| |#2| (-572 (-506))) (((-833 (-360))) |has| |#2| (-572 (-833 (-360)))) (((-833 (-530))) |has| |#2| (-572 (-833 (-530))))) ((((-804)) . T)) ((((-804)) . T)) @@ -2747,12 +2747,12 @@ ((((-388 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1027)) -(((|#2| (-461 (-2167 |#1|) (-719))) . T)) +(((|#2| (-461 (-2267 |#1|) (-719))) . T)) ((((-530) |#1|) . T)) ((((-1082)) . T) (((-804)) . T)) (((|#2| |#2|) . T)) (((|#1| (-502 (-1099))) . T)) -(-1476 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((((-530)) . T)) (((|#2|) . T)) (((|#2|) . T)) @@ -2762,9 +2762,9 @@ ((($) . T) (((-388 (-530))) . T)) ((($) . T)) ((($) . T)) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) (((|#1|) . T)) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((((-804)) . T)) ((((-137)) . T)) (((|#1|) . T) (((-388 (-530))) . T)) @@ -2804,27 +2804,27 @@ (|has| |#1| (-216)) (((|#1| (-502 |#3|)) . T)) (|has| |#1| (-349)) -(((|#2| (-223 (-2167 |#1|) (-719))) . T)) +(((|#2| (-223 (-2267 |#1|) (-719))) . T)) (|has| |#1| (-349)) (|has| |#1| (-349)) (((|#1|) . T) (($) . T)) (((|#1| (-502 |#2|)) . T)) -(-1476 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) (((|#1| (-719)) . T)) (|has| |#1| (-522)) -(-1476 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-25)) (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-793)) (|has| |#2| (-984))) (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) ((((-804)) . T)) -(-1476 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-128)) (|has| |#2| (-128))) (-12 (|has| |#1| (-741)) (|has| |#2| (-741)))) -(-1476 (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984))) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-128)) (|has| |#2| (-128))) (-12 (|has| |#1| (-741)) (|has| |#2| (-741)))) +(-1461 (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) (((|#1|) |has| |#1| (-162))) (((|#4|) |has| |#4| (-984))) (((|#3|) |has| |#3| (-984))) (-12 (|has| |#1| (-344)) (|has| |#2| (-768))) (-12 (|has| |#1| (-344)) (|has| |#2| (-768))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) ((((-388 |#2|)) . T) (((-388 (-530))) . T) (($) . T)) ((($ $) . T) ((#0=(-388 (-530)) #0#) . T)) @@ -2837,14 +2837,14 @@ (((|#2|) |has| |#2| (-984)) (((-530)) -12 (|has| |#2| (-593 (-530))) (|has| |#2| (-984)))) (((|#1|) . T)) (|has| |#2| (-344)) -(((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530)))) ((|#2| |#2|) . T) (($ $) -1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) +(((#0=(-388 (-530)) #0#) |has| |#2| (-37 (-388 (-530)))) ((|#2| |#2|) . T) (($ $) -1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1| |#1|) . T) ((#0=(-388 (-530)) #0#) |has| |#1| (-37 (-388 (-530))))) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-388 (-530)) #0#) . T)) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-388 (-530)) #0#) . T)) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-388 (-530)) #0#) . T)) (((|#2| |#2|) . T)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T) (($) -1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T) (($) -1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#1|) . T) (($) . T) (((-388 (-530))) . T)) (((|#1|) . T) (($) . T) (((-388 (-530))) . T)) (((|#1|) . T) (($) . T) (((-388 (-530))) . T)) @@ -2863,25 +2863,25 @@ (((|#1|) |has| |#2| (-398 |#1|))) (((|#1|) |has| |#2| (-398 |#1|))) ((((-851 |#1|)) . T) (((-388 (-530))) . T) (($) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) ((((-804)) . T)) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) |has| (-2 (|:| -2940 (-1099)) (|:| -1806 (-51))) (-291 (-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))))) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) |has| (-2 (|:| -3078 (-1099)) (|:| -1874 (-51))) (-291 (-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) ((((-530) |#1|) . T)) ((((-530) |#1|) . T)) ((((-530) |#1|) . T)) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((((-530) |#1|) . T)) (((|#1|) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((((-1099)) |has| |#1| (-841 (-1099))) (((-766 (-1099))) . T)) -(-1476 (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#3| (-128)) (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-741)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((((-767 |#1|)) . T)) (((|#1| |#2|) . T)) ((((-804)) . T)) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-675)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-675)) (|has| |#3| (-793)) (|has| |#3| (-984))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-388 (-530)))) ((((-804)) . T)) @@ -2889,15 +2889,15 @@ (((|#1|) |has| |#1| (-162)) (($) |has| |#1| (-522)) (((-388 (-530))) |has| |#1| (-522))) (((|#2|) . T) (((-530)) |has| |#2| (-593 (-530)))) (|has| |#1| (-344)) -(-1476 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (-12 (|has| |#1| (-344)) (|has| |#2| (-216)))) +(-1461 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (-12 (|has| |#1| (-344)) (|has| |#2| (-216)))) (|has| |#1| (-15 * (|#1| (-388 (-530)) |#1|))) (|has| |#1| (-344)) (((|#1|) . T)) -(((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#1| |#1|) . T)) +(((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#1| |#1|) . T)) ((((-530) |#1|) . T)) ((((-297 |#1|)) . T)) (((#0=(-647) (-1095 #0#)) . T)) -((((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#1|) . T)) +((((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (|has| |#1| (-793)) ((($ $) . T) ((#0=(-806 |#1|) $) . T) ((#0# |#2|) . T)) @@ -2914,12 +2914,12 @@ (((#0=(-1167 |#1| |#2| |#3| |#4|)) |has| #0# (-291 #0#))) ((($) . T)) (((|#1|) . T)) -((($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#2| |#2|) |has| |#1| (-344)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) +((($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#2| |#2|) |has| |#1| (-344)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) ((#0=(-388 (-530)) #0#) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) (|has| |#2| (-216)) (|has| $ (-140)) ((((-804)) . T)) -((($) . T) (((-388 (-530))) -1476 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) +((($) . T) (((-388 (-530))) -1461 (|has| |#1| (-344)) (|has| |#1| (-330))) ((|#1|) . T)) ((((-804)) . T)) (|has| |#1| (-793)) ((((-1099)) -12 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (|has| |#1| (-841 (-1099))))) @@ -2931,23 +2931,23 @@ (((|#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#4|) . T)) (|has| |#1| (-522)) -((($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#2|) |has| |#1| (-344)) ((|#1|) . T)) -((((-1099)) -1476 (-12 (|has| (-1173 |#1| |#2| |#3|) (-841 (-1099))) (|has| |#1| (-344))) (-12 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (|has| |#1| (-841 (-1099)))))) -(((|#1|) . T) (($) -1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1476 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) +((($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344))) ((|#2|) |has| |#1| (-344)) ((|#1|) . T)) +((((-1099)) -1461 (-12 (|has| (-1173 |#1| |#2| |#3|) (-841 (-1099))) (|has| |#1| (-344))) (-12 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (|has| |#1| (-841 (-1099)))))) +(((|#1|) . T) (($) -1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-522))) (((-388 (-530))) -1461 (|has| |#1| (-37 (-388 (-530)))) (|has| |#1| (-344)))) ((((-1099)) -12 (|has| |#1| (-15 * (|#1| (-388 (-530)) |#1|))) (|has| |#1| (-841 (-1099))))) ((((-1099)) -12 (|has| |#1| (-15 * (|#1| (-719) |#1|))) (|has| |#1| (-841 (-1099))))) (((|#4|) -12 (|has| |#4| (-291 |#4|)) (|has| |#4| (-1027)))) ((((-530) |#1|) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) (((|#1|) . T)) (((|#1| (-502 (-766 (-1099)))) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (((|#1|) . T)) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) (((|#1|) . T)) -(-1476 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) -(-1476 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-128)) (|has| |#2| (-128))) (-12 (|has| |#1| (-741)) (|has| |#2| (-741)))) +(-1461 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-128)) (|has| |#2| (-128))) (-12 (|has| |#1| (-741)) (|has| |#2| (-741)))) ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-344))) ((($) . T) (((-811 |#1|)) . T) (((-388 (-530))) . T)) ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-344))) @@ -2956,15 +2956,15 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-388 |#2|)) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (((|#1|) . T)) (((|#2| |#2|) . T) ((#0=(-388 (-530)) #0#) . T) (($ $) . T)) ((((-530)) . T)) @@ -2993,32 +2993,32 @@ ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-344))) ((((-1099)) . T) (((-804)) . T)) (|has| |#1| (-344)) -((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) +((((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) |has| |#2| (-162)) (($) -1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850)))) (((|#2|) . T) ((|#6|) . T)) ((($) . T) (((-388 (-530))) |has| |#2| (-37 (-388 (-530)))) ((|#2|) . T)) -((($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((((-1031)) . T)) ((((-804)) . T)) -((($) -1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) ((($) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530)))) ((|#1|) . T)) ((($) . T)) -((($) -1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) +((($) -1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((|#1|) |has| |#1| (-162)) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (|has| |#2| (-850)) (|has| |#1| (-850)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) |has| |#1| (-162))) ((((-647)) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (((|#1|) |has| |#1| (-162))) (((|#1|) |has| |#1| (-162))) ((((-388 (-530))) . T) (($) . T)) (((|#1| (-530)) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) (|has| |#1| (-344)) (|has| |#1| (-344)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) -(-1476 (|has| |#1| (-162)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-162)) (|has| |#1| (-522))) (((|#1| (-530)) . T)) (((|#1| (-388 (-530))) . T)) (((|#1| (-719)) . T)) @@ -3033,16 +3033,16 @@ ((((-833 (-360))) . T) (((-833 (-530))) . T) (((-1099)) . T) (((-506)) . T)) (((|#1|) . T)) ((((-804)) . T)) -(-1476 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) -(-1476 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-128)) (|has| |#2| (-128))) (-12 (|has| |#1| (-741)) (|has| |#2| (-741)))) +(-1461 (|has| |#2| (-128)) (|has| |#2| (-162)) (|has| |#2| (-344)) (|has| |#2| (-741)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-128)) (|has| |#2| (-128))) (-12 (|has| |#1| (-741)) (|has| |#2| (-741)))) ((((-530)) . T)) ((((-530)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) -(-1476 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) +(-1461 (|has| |#2| (-162)) (|has| |#2| (-675)) (|has| |#2| (-793)) (|has| |#2| (-984))) ((((-1099)) -12 (|has| |#2| (-841 (-1099))) (|has| |#2| (-984)))) -(-1476 (-12 (|has| |#1| (-453)) (|has| |#2| (-453))) (-12 (|has| |#1| (-675)) (|has| |#2| (-675)))) +(-1461 (-12 (|has| |#1| (-453)) (|has| |#2| (-453))) (-12 (|has| |#1| (-675)) (|has| |#2| (-675)))) (|has| |#1| (-138)) (|has| |#1| (-140)) (|has| |#1| (-344)) @@ -3066,7 +3066,7 @@ ((((-1082) (-1099) (-530) (-208) (-804)) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) -(-1476 (|has| |#1| (-330)) (|has| |#1| (-349))) +(-1461 (|has| |#1| (-330)) (|has| |#1| (-349))) (((|#1| |#2|) . T)) ((($) . T) ((|#1|) . T)) ((((-804)) . T)) @@ -3074,7 +3074,7 @@ ((($) . T) ((|#1|) . T) (((-388 (-530))) |has| |#1| (-37 (-388 (-530))))) (((|#2|) |has| |#2| (-1027)) (((-530)) -12 (|has| |#2| (-975 (-530))) (|has| |#2| (-1027))) (((-388 (-530))) -12 (|has| |#2| (-975 (-388 (-530)))) (|has| |#2| (-1027)))) ((((-506)) |has| |#1| (-572 (-506)))) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-795)) (|has| |#1| (-1027)))) ((($) . T) (((-388 (-530))) . T)) (|has| |#1| (-850)) (|has| |#1| (-850)) @@ -3083,14 +3083,14 @@ ((((-804)) . T)) (((|#2| |#2|) . T)) (((|#1| |#1|) |has| |#1| (-162))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-522))) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-793))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-522))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-793))) (((|#2|) . T)) -(-1476 (|has| |#1| (-21)) (|has| |#1| (-793))) +(-1461 (|has| |#1| (-21)) (|has| |#1| (-793))) (((|#1|) |has| |#1| (-162))) (((|#1|) . T)) (((|#1|) . T)) -((((-804)) -1476 (-12 (|has| |#1| (-571 (-804))) (|has| |#2| (-571 (-804)))) (-12 (|has| |#1| (-1027)) (|has| |#2| (-1027))))) +((((-804)) -1461 (-12 (|has| |#1| (-571 (-804))) (|has| |#2| (-571 (-804)))) (-12 (|has| |#1| (-1027)) (|has| |#2| (-1027))))) ((((-388 |#2|) |#3|) . T)) ((((-388 (-530))) . T) (($) . T)) (|has| |#1| (-37 (-388 (-530)))) @@ -3102,17 +3102,17 @@ (((|#1|) . T) (((-388 (-530))) . T) (((-530)) . T) (($) . T)) (((#0=(-530) #0#) . T)) ((($) . T) (((-388 (-530))) . T)) -(-1476 (|has| |#4| (-162)) (|has| |#4| (-675)) (|has| |#4| (-793)) (|has| |#4| (-984))) -(-1476 (|has| |#3| (-162)) (|has| |#3| (-675)) (|has| |#3| (-793)) (|has| |#3| (-984))) +(-1461 (|has| |#4| (-162)) (|has| |#4| (-675)) (|has| |#4| (-793)) (|has| |#4| (-984))) +(-1461 (|has| |#3| (-162)) (|has| |#3| (-675)) (|has| |#3| (-793)) (|has| |#3| (-984))) (|has| |#4| (-741)) -(-1476 (|has| |#4| (-741)) (|has| |#4| (-793))) +(-1461 (|has| |#4| (-741)) (|has| |#4| (-793))) (|has| |#4| (-793)) (|has| |#3| (-741)) -(-1476 (|has| |#3| (-741)) (|has| |#3| (-793))) +(-1461 (|has| |#3| (-741)) (|has| |#3| (-793))) (|has| |#3| (-793)) ((((-530)) . T)) (((|#2|) . T)) -((((-1099)) -1476 (-12 (|has| (-1097 |#1| |#2| |#3|) (-841 (-1099))) (|has| |#1| (-344))) (-12 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (|has| |#1| (-841 (-1099)))))) +((((-1099)) -1461 (-12 (|has| (-1097 |#1| |#2| |#3|) (-841 (-1099))) (|has| |#1| (-344))) (-12 (|has| |#1| (-15 * (|#1| (-530) |#1|))) (|has| |#1| (-841 (-1099)))))) ((((-1099)) -12 (|has| |#1| (-15 * (|#1| (-388 (-530)) |#1|))) (|has| |#1| (-841 (-1099))))) ((((-1099)) -12 (|has| |#1| (-15 * (|#1| (-719) |#1|))) (|has| |#1| (-841 (-1099))))) (((|#1| |#1|) . T) (($ $) . T)) @@ -3127,11 +3127,11 @@ ((((-1097 |#1| |#2| |#3|)) |has| |#1| (-344))) ((((-1064 |#1| |#2|)) . T)) ((((-1097 |#1| |#2| |#3|)) |has| |#1| (-344))) -(((|#2|) . T) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) . T)) +(((|#2|) . T) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) . T)) ((($) . T)) (|has| |#1| (-960)) -(((|#2|) . T) (((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) ((((-804)) . T)) ((((-506)) |has| |#2| (-572 (-506))) (((-833 (-530))) |has| |#2| (-572 (-833 (-530)))) (((-833 (-360))) |has| |#2| (-572 (-833 (-360)))) (((-360)) . #0=(|has| |#2| (-960))) (((-208)) . #0#)) ((((-1099) (-51)) . T)) @@ -3143,15 +3143,15 @@ ((((-1097 |#1| |#2| |#3|)) . T)) ((((-1097 |#1| |#2| |#3|)) . T) (((-1090 |#1| |#2| |#3|)) . T)) ((((-804)) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) ((((-530) |#1|) . T)) ((((-1097 |#1| |#2| |#3|)) |has| |#1| (-344))) (((|#1| |#2| |#3| |#4|) . T)) (((|#1|) . T)) (((|#2|) . T)) (|has| |#2| (-344)) -(((|#3|) . T) ((|#2|) . T) (($) -1476 (|has| |#4| (-162)) (|has| |#4| (-793)) (|has| |#4| (-984))) ((|#4|) -1476 (|has| |#4| (-162)) (|has| |#4| (-344)) (|has| |#4| (-984)))) -(((|#2|) . T) (($) -1476 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((|#3|) -1476 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984)))) +(((|#3|) . T) ((|#2|) . T) (($) -1461 (|has| |#4| (-162)) (|has| |#4| (-793)) (|has| |#4| (-984))) ((|#4|) -1461 (|has| |#4| (-162)) (|has| |#4| (-344)) (|has| |#4| (-984)))) +(((|#2|) . T) (($) -1461 (|has| |#3| (-162)) (|has| |#3| (-793)) (|has| |#3| (-984))) ((|#3|) -1461 (|has| |#3| (-162)) (|has| |#3| (-344)) (|has| |#3| (-984)))) (((|#1|) . T)) (((|#1|) . T)) (|has| |#1| (-344)) @@ -3163,7 +3163,7 @@ ((((-804)) . T)) ((((-804)) . T)) (((|#1|) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) ((((-127)) . T) (((-804)) . T)) ((((-530) |#1|) . T)) (((|#1|) . T)) @@ -3171,31 +3171,31 @@ (((|#1|) . T)) (((|#2| $) -12 (|has| |#1| (-344)) (|has| |#2| (-268 |#2| |#2|))) (($ $) . T)) ((($ $) . T)) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-850))) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-432)) (|has| |#1| (-850))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) ((((-804)) . T)) ((((-804)) . T)) ((((-804)) . T)) (((|#1| (-502 |#2|)) . T)) -((((-2 (|:| -2940 (-1099)) (|:| -1806 (-51)))) . T)) +((((-2 (|:| -3078 (-1099)) (|:| -1874 (-51)))) . T)) (((|#1| (-530)) . T)) (((|#1| (-388 (-530))) . T)) (((|#1| (-719)) . T)) ((((-1104)) . T) (((-804)) . T)) ((((-114 |#1|)) . T) (($) . T) (((-388 (-530))) . T)) -(-1476 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) -(-1476 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) +(-1461 (|has| |#2| (-432)) (|has| |#2| (-522)) (|has| |#2| (-850))) +(-1461 (|has| |#1| (-432)) (|has| |#1| (-522)) (|has| |#1| (-850))) ((($) . T)) (((|#2| (-502 (-806 |#1|))) . T)) ((((-530) |#1|) . T)) (((|#2|) . T)) (((|#2| (-719)) . T)) -((((-804)) -1476 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) +((((-804)) -1461 (|has| |#1| (-571 (-804))) (|has| |#1| (-1027)))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((((-1082) |#1|) . T)) ((((-388 |#2|)) . T)) -((((-2 (|:| -2940 |#1|) (|:| -1806 |#2|))) . T)) +((((-2 (|:| -3078 |#1|) (|:| -1874 |#2|))) . T)) (|has| |#1| (-522)) (|has| |#1| (-522)) ((($) . T) ((|#2|) . T)) @@ -3203,12 +3203,12 @@ (((|#1| |#2|) . T)) (((|#2| $) |has| |#2| (-268 |#2| |#2|))) (((|#1| (-597 |#1|)) |has| |#1| (-793))) -(-1476 (|has| |#1| (-216)) (|has| |#1| (-330))) -(-1476 (|has| |#1| (-344)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-216)) (|has| |#1| (-330))) +(-1461 (|has| |#1| (-344)) (|has| |#1| (-330))) (|has| |#1| (-1027)) (((|#1|) . T)) ((((-388 (-530))) . T) (($) . T)) -((((-938 |#1|)) . T) ((|#1|) . T) (((-530)) -1476 (|has| (-938 |#1|) (-975 (-530))) (|has| |#1| (-975 (-530)))) (((-388 (-530))) -1476 (|has| (-938 |#1|) (-975 (-388 (-530)))) (|has| |#1| (-975 (-388 (-530)))))) +((((-938 |#1|)) . T) ((|#1|) . T) (((-530)) -1461 (|has| (-938 |#1|) (-975 (-530))) (|has| |#1| (-975 (-530)))) (((-388 (-530))) -1461 (|has| (-938 |#1|) (-975 (-388 (-530)))) (|has| |#1| (-975 (-388 (-530)))))) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) (((|#1| |#1|) -12 (|has| |#1| (-291 |#1|)) (|has| |#1| (-1027)))) @@ -3219,9 +3219,9 @@ (((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1064 |#1| |#2|) #0#) |has| (-1064 |#1| |#2|) (-291 (-1064 |#1| |#2|)))) -(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) #0#) |has| (-2 (|:| -2940 |#1|) (|:| -1806 |#2|)) (-291 (-2 (|:| -2940 |#1|) (|:| -1806 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-291 |#2|)) (|has| |#2| (-1027))) ((#0=(-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) #0#) |has| (-2 (|:| -3078 |#1|) (|:| -1874 |#2|)) (-291 (-2 (|:| -3078 |#1|) (|:| -1874 |#2|))))) (((#0=(-114 |#1|)) |has| #0# (-291 #0#))) -(-1476 (|has| |#1| (-795)) (|has| |#1| (-1027))) +(-1461 (|has| |#1| (-795)) (|has| |#1| (-1027))) ((($ $) . T)) ((($ $) . T) ((#0=(-806 |#1|) $) . T) ((#0# |#2|) . T)) ((($ $) . T) ((|#2| $) |has| |#1| (-216)) ((|#2| |#1|) |has| |#1| (-216)) ((|#3| |#1|) . T) ((|#3| $) . T)) |