diff options
Diffstat (limited to 'src/share/algebra/operation.daase')
| -rw-r--r-- | src/share/algebra/operation.daase | 268 |
1 files changed, 134 insertions, 134 deletions
diff --git a/src/share/algebra/operation.daase b/src/share/algebra/operation.daase index e103cd51..b9a4bbbd 100644 --- a/src/share/algebra/operation.daase +++ b/src/share/algebra/operation.daase @@ -1,5 +1,5 @@ -(631058 . 3577300070) +(631058 . 3577302778) (((*1 *2 *3 *4) (|partial| -12 (-5 *3 (-1178 *4)) (-4 *4 (-13 (-961) (-580 (-483)))) (-5 *2 (-1178 (-348 (-483)))) (-5 *1 (-1207 *4))))) @@ -257,7 +257,7 @@ ((*1 *1 *1 *2) (-12 (-4 *1 (-408 *2 *3)) (-4 *2 (-146)) (-4 *3 (-23)))) ((*1 *1 *2 *1) (-12 (-4 *1 (-408 *2 *3)) (-4 *2 (-146)) (-4 *3 (-23)))) ((*1 *1 *1 *1) - (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-441 *2 *3 *4 *5)) + (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-442 *2 *3 *4 *5)) (-4 *5 (-861 *2 *3 *4)))) ((*1 *2 *2 *2) (-12 (-5 *2 (-1178 *3)) (-4 *3 (-299)) (-5 *1 (-465 *3)))) ((*1 *1 *1 *1) (-5 *1 (-472))) @@ -325,7 +325,7 @@ (-2 (|:| -2400 *4) (|:| -2401 *5)))) (-5 *1 (-399 *2 *3 *4 *5 *6 *7)) (-4 *4 (-756)) (-4 *7 (-861 *3 *5 (-773 *2))))) - ((*1 *1 *1) (-12 (-4 *1 (-447 *2 *3)) (-4 *2 (-72)) (-4 *3 (-759)))) + ((*1 *1 *1) (-12 (-4 *1 (-448 *2 *3)) (-4 *2 (-72)) (-4 *3 (-759)))) ((*1 *1 *1) (-12 (-4 *2 (-494)) (-5 *1 (-562 *2 *3)) (-4 *3 (-1154 *2)))) ((*1 *1 *1) (-12 (-4 *1 (-645 *2)) (-4 *2 (-961)))) ((*1 *1 *1) @@ -419,7 +419,7 @@ (-5 *1 (-368 *5 *4 *6 *2)) (-4 *4 (-367 *5)))) ((*1 *1 *2 *1) (-12 (-5 *2 (-1 *3 *3)) (-4 *1 (-427 *3)) (-4 *3 (-1128)))) ((*1 *1 *2 *1) - (-12 (-5 *2 (-1 *3 *3)) (-4 *1 (-447 *3 *4)) (-4 *3 (-72)) (-4 *4 (-759)))) + (-12 (-5 *2 (-1 *3 *3)) (-4 *1 (-448 *3 *4)) (-4 *3 (-72)) (-4 *4 (-759)))) ((*1 *2 *3 *4) (-12 (-5 *3 (-1 *6 *5)) (-5 *4 (-518 *5)) (-4 *5 (-312)) (-4 *6 (-312)) (-5 *2 (-518 *6)) (-5 *1 (-519 *5 *6)))) @@ -838,7 +838,7 @@ (-4 *3 (-961)) (-14 *5 *3))) ((*1 *1 *2) (-12 (-5 *2 (-583 *6)) (-4 *6 (-861 *3 *4 *5)) (-4 *3 (-312)) (-4 *4 (-717)) - (-4 *5 (-756)) (-5 *1 (-441 *3 *4 *5 *6)))) + (-4 *5 (-756)) (-5 *1 (-442 *3 *4 *5 *6)))) ((*1 *1 *2) (-12 (-5 *2 (-583 (-1129))) (-5 *1 (-461)))) ((*1 *1 *2) (-12 (-5 *2 (-583 (-1129))) (-5 *1 (-539)))) ((*1 *1 *2) (-12 (-4 *3 (-146)) (-5 *1 (-540 *3 *2)) (-4 *2 (-683 *3)))) @@ -914,7 +914,7 @@ (-5 *1 (-1088 *3 *4 *5)))) ((*1 *2 *1) (-12 (-5 *2 (-1101 (-1089) (-377))) (-5 *1 (-1093)))) ((*1 *2 *1) (-12 (-5 *2 (-1072)) (-5 *1 (-1094)))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-1094)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-1094)))) ((*1 *2 *1) (-12 (-5 *2 (-179)) (-5 *1 (-1094)))) ((*1 *2 *1) (-12 (-5 *2 (-483)) (-5 *1 (-1094)))) ((*1 *2 *1) (-12 (-5 *2 (-772)) (-5 *1 (-1102 *3)) (-4 *3 (-1013)))) @@ -1127,7 +1127,7 @@ (-12 (-5 *3 (-694)) (-4 *4 (-961)) (-4 *5 (-756)) (-4 *6 (-717)) (-14 *8 (-583 *5)) (-5 *2 (-1184)) (-5 *1 (-1191 *4 *5 *6 *7 *8 *9 *10)) (-4 *7 (-861 *4 *6 *5)) (-14 *9 (-583 *3)) (-14 *10 *3)))) -(((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-456)))) +(((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-457)))) ((*1 *2 *1) (-12 (-4 *2 (-13 (-1013) (-34))) (-5 *1 (-1053 *3 *2)) (-4 *3 (-13 (-1013) (-34))))) @@ -1208,10 +1208,10 @@ (-4 *5 (-146)))) ((*1 *2 *1) (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *2 (-483)) - (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) + (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) ((*1 *2 *1 *3) (-12 (-5 *3 (-583 *6)) (-4 *6 (-756)) (-4 *4 (-312)) (-4 *5 (-717)) - (-5 *2 (-483)) (-5 *1 (-441 *4 *5 *6 *7)) (-4 *7 (-861 *4 *5 *6)))) + (-5 *2 (-483)) (-5 *1 (-442 *4 *5 *6 *7)) (-4 *7 (-861 *4 *5 *6)))) ((*1 *2 *1) (-12 (-4 *1 (-893 *3)) (-4 *3 (-961)) (-5 *2 (-830)))) ((*1 *2) (-12 (-4 *1 (-1186 *3)) (-4 *3 (-312)) (-5 *2 (-107))))) (((*1 *1) (-5 *1 (-1184)))) @@ -1535,7 +1535,7 @@ (-12 (-4 *3 (-13 (-312) (-120))) (-5 *1 (-340 *3 *2)) (-4 *2 (-1154 *3)))) ((*1 *1 *1 *1) (-12 (-4 *1 (-408 *2 *3)) (-4 *2 (-146)) (-4 *3 (-23)))) ((*1 *1 *1 *1) - (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-441 *2 *3 *4 *5)) + (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-442 *2 *3 *4 *5)) (-4 *5 (-861 *2 *3 *4)))) ((*1 *1 *1 *1) (-5 *1 (-472))) ((*1 *1 *1 *1) @@ -1753,7 +1753,7 @@ ((*1 *1 *1 *2) (-12 (-4 *1 (-411)) (-5 *2 (-483)))) ((*1 *1 *1 *2) (-12 (-5 *2 (-694)) (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) - (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) + (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) ((*1 *2 *2 *3) (-12 (-5 *2 (-1178 *4)) (-5 *3 (-483)) (-4 *4 (-299)) (-5 *1 (-465 *4)))) ((*1 *1 *1 *2) (-12 (-5 *2 (-483)) (-5 *1 (-472)))) @@ -2021,7 +2021,7 @@ ((*1 *2 *1 *2 *2) (-12 (-4 *1 (-291 *2 *3 *4)) (-4 *2 (-1133)) (-4 *3 (-1154 *2)) (-4 *4 (-1154 (-348 *3))))) - ((*1 *2 *1 *3) (-12 (-5 *3 (-1089)) (-5 *2 (-1072)) (-5 *1 (-439)))) + ((*1 *2 *1 *3) (-12 (-5 *3 (-1089)) (-5 *2 (-1072)) (-5 *1 (-440)))) ((*1 *1 *1 *2 *2) (-12 (-5 *2 (-583 (-483))) (-4 *1 (-627 *3 *4 *5)) (-4 *3 (-961)) (-4 *4 (-322 *3)) (-4 *5 (-322 *3)))) @@ -2235,8 +2235,8 @@ (-12 (-4 *1 (-274 *3 *4)) (-4 *3 (-1013)) (-4 *4 (-104)) (-5 *2 (-583 (-2 (|:| |gen| *3) (|:| -3942 *4)))))) ((*1 *2 *1) - (-12 (-4 *1 (-447 *3 *4)) (-4 *3 (-72)) (-4 *4 (-759)) - (-5 *2 (-583 (-451 *3 *4))))) + (-12 (-4 *1 (-448 *3 *4)) (-4 *3 (-72)) (-4 *4 (-759)) + (-5 *2 (-583 (-452 *3 *4))))) ((*1 *2 *1) (-12 (-5 *2 (-583 (-2 (|:| -3953 *3) (|:| -3937 *4)))) (-5 *1 (-674 *3 *4)) (-4 *3 (-961)) (-4 *4 (-663)))) @@ -2390,9 +2390,9 @@ ((*1 *1 *1 *2) (-12 (-5 *2 (-1089)) (-4 *1 (-362 *3)) (-4 *3 (-1013)) (-4 *3 (-553 (-472))))) - ((*1 *1 *1 *2 *3) (-12 (-4 *1 (-453 *2 *3)) (-4 *2 (-1013)) (-4 *3 (-1128)))) + ((*1 *1 *1 *2 *3) (-12 (-4 *1 (-454 *2 *3)) (-4 *2 (-1013)) (-4 *3 (-1128)))) ((*1 *1 *1 *2 *3) - (-12 (-5 *2 (-583 *4)) (-5 *3 (-583 *5)) (-4 *1 (-453 *4 *5)) (-4 *4 (-1013)) + (-12 (-5 *2 (-583 *4)) (-5 *3 (-583 *5)) (-4 *1 (-454 *4 *5)) (-4 *4 (-1013)) (-4 *5 (-1128)))) ((*1 *2 *1 *2) (-12 (-5 *2 (-743 *3)) (-4 *3 (-312)) (-5 *1 (-655 *3)))) ((*1 *2 *1 *2) (-12 (-5 *1 (-655 *2)) (-4 *2 (-312)))) @@ -2534,7 +2534,7 @@ (-4 *3 (-322 *5)))) ((*1 *2 *3) (-12 (-4 *4 (-494)) (-4 *5 (-904 *4)) - (-5 *2 (-2 (|:| |num| *6) (|:| |den| *4))) (-5 *1 (-440 *4 *5 *6 *3)) + (-5 *2 (-2 (|:| |num| *6) (|:| |den| *4))) (-5 *1 (-441 *4 *5 *6 *3)) (-4 *6 (-322 *4)) (-4 *3 (-322 *5)))) ((*1 *2 *3) (-12 (-5 *3 (-630 *5)) (-4 *5 (-904 *4)) (-4 *4 (-494)) @@ -2553,7 +2553,7 @@ (-4 *2 (-322 *4)))) ((*1 *2 *3) (-12 (-4 *4 (-494)) (-4 *5 (-904 *4)) (-4 *2 (-322 *4)) - (-5 *1 (-440 *4 *5 *2 *3)) (-4 *3 (-322 *5)))) + (-5 *1 (-441 *4 *5 *2 *3)) (-4 *3 (-322 *5)))) ((*1 *2 *3) (-12 (-5 *3 (-630 *5)) (-4 *5 (-904 *4)) (-4 *4 (-494)) (-5 *2 (-630 *4)) (-5 *1 (-633 *4 *5)))) @@ -2564,7 +2564,7 @@ (-12 (-4 *4 (-904 *2)) (-4 *2 (-494)) (-5 *1 (-115 *2 *4 *3)) (-4 *3 (-322 *4)))) ((*1 *2 *3) - (-12 (-4 *4 (-904 *2)) (-4 *2 (-494)) (-5 *1 (-440 *2 *4 *5 *3)) + (-12 (-4 *4 (-904 *2)) (-4 *2 (-494)) (-5 *1 (-441 *2 *4 *5 *3)) (-4 *5 (-322 *2)) (-4 *3 (-322 *4)))) ((*1 *2 *3) (-12 (-5 *3 (-630 *4)) (-4 *4 (-904 *2)) (-4 *2 (-494)) @@ -2823,8 +2823,8 @@ ((*1 *2 *3) (-12 (-5 *3 - (-441 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483))))) - (-14 *4 (-583 (-1089))) (-14 *5 (-694)) (-5 *2 (-85)) (-5 *1 (-442 *4 *5)))) + (-442 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483))))) + (-14 *4 (-583 (-1089))) (-14 *5 (-694)) (-5 *2 (-85)) (-5 *1 (-443 *4 *5)))) ((*1 *2 *3) (-12 (-5 *2 (-85)) (-5 *1 (-873 *3)) (-4 *3 (-482)))) ((*1 *2 *1) (-12 (-4 *1 (-1133)) (-5 *2 (-85))))) (((*1 *2) (-12 (-5 *2 (-1184)) (-5 *1 (-1131))))) @@ -3086,7 +3086,7 @@ (-14 *4 (-583 (-1089))))) ((*1 *2 *3 *1) (-12 (-4 *1 (-274 *3 *2)) (-4 *3 (-1013)) (-4 *2 (-104)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-333 *2 *3)) (-4 *3 (-1013)) (-4 *2 (-961)))) - ((*1 *2 *1) (-12 (-4 *2 (-72)) (-5 *1 (-451 *2 *3)) (-4 *3 (-759)))) + ((*1 *2 *1) (-12 (-4 *2 (-72)) (-5 *1 (-452 *2 *3)) (-4 *3 (-759)))) ((*1 *2 *1 *3) (-12 (-5 *3 (-483)) (-4 *2 (-494)) (-5 *1 (-562 *2 *4)) (-4 *4 (-1154 *2)))) ((*1 *2 *1 *3) (-12 (-5 *3 (-694)) (-4 *1 (-645 *2)) (-4 *2 (-961)))) @@ -3382,7 +3382,7 @@ (-13 (-756) (-10 -8 (-15 -3799 ((-1072) $ (-1089))) (-15 -3616 (*2 $)) (-15 -1963 (*2 $))))))) - ((*1 *2 *1) (-12 (-5 *2 (-1184)) (-5 *1 (-439)))) + ((*1 *2 *1) (-12 (-5 *2 (-1184)) (-5 *1 (-440)))) ((*1 *2 *3) (-12 (-5 *3 (-1072)) (-5 *2 (-1184)) (-5 *1 (-647)))) ((*1 *2 *1) (-12 (-5 *2 (-1184)) (-5 *1 (-1108)))) ((*1 *2 *1 *3) (-12 (-5 *3 (-483)) (-5 *2 (-1184)) (-5 *1 (-1108))))) @@ -3716,10 +3716,10 @@ (-5 *3 (-249 (-348 (-857 *4))))))) (((*1 *2 *1) (-12 (-5 *1 (-632 *2)) (-4 *2 (-552 (-772))))) ((*1 *2 *1) (-12 (-5 *2 (-1072)) (-5 *1 (-785)))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-785)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-785)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-483)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-1072)))) - ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-444)))) + ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-445)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-527)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-416)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-110)))) @@ -3739,7 +3739,7 @@ ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-462)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-1190)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-978)))) - ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-456)))) + ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-457)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-622)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-67)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-1029)))) @@ -3751,15 +3751,15 @@ ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-172)))) ((*1 *2 *1) (-12 (-4 *1 (-1050)) (-5 *2 (-461)))) ((*1 *2 *1) (-12 (-5 *2 (-1072)) (-5 *1 (-1094)))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-1094)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-1094)))) ((*1 *2 *1) (-12 (-5 *2 (-179)) (-5 *1 (-1094)))) ((*1 *2 *1) (-12 (-5 *2 (-483)) (-5 *1 (-1094))))) (((*1 *1 *1 *2) (-12 (-5 *2 (-583 (-1094))) (-5 *1 (-1094)))) - ((*1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-583 (-1094))) (-5 *1 (-1094))))) + ((*1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-583 (-1094))) (-5 *1 (-1094))))) (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-1094))))) -(((*1 *2 *1) (|partial| -12 (-5 *2 (-444)) (-5 *1 (-234)))) +(((*1 *2 *1) (|partial| -12 (-5 *2 (-445)) (-5 *1 (-234)))) ((*1 *2 *1) - (-12 (-5 *2 (-3 (-483) (-179) (-444) (-1072) (-1094))) (-5 *1 (-1094))))) + (-12 (-5 *2 (-3 (-483) (-179) (-445) (-1072) (-1094))) (-5 *1 (-1094))))) (((*1 *2 *1) (|partial| -12 (-5 *2 (-583 (-234))) (-5 *1 (-234)))) ((*1 *2 *1) (-12 (-5 *2 (-583 (-1094))) (-5 *1 (-1094))))) (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-1094))))) @@ -3773,10 +3773,10 @@ (-12 (-5 *3 (|[\|\|]| *4)) (-4 *4 (-552 (-772))) (-5 *2 (-85)) (-5 *1 (-632 *4)))) ((*1 *2 *1 *3) (-12 (-5 *3 (|[\|\|]| (-1072))) (-5 *2 (-85)) (-5 *1 (-785)))) - ((*1 *2 *1 *3) (-12 (-5 *3 (|[\|\|]| (-444))) (-5 *2 (-85)) (-5 *1 (-785)))) + ((*1 *2 *1 *3) (-12 (-5 *3 (|[\|\|]| (-445))) (-5 *2 (-85)) (-5 *1 (-785)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-483))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-1072))) (-5 *2 (-85)))) - ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-444))) (-5 *2 (-85)))) + ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-445))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-527))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-416))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-110))) (-5 *2 (-85)))) @@ -3796,7 +3796,7 @@ ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-462))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-1190))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-978))) (-5 *2 (-85)))) - ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-456))) (-5 *2 (-85)))) + ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-457))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-622))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-67))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-1029))) (-5 *2 (-85)))) @@ -3808,7 +3808,7 @@ ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-172))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-4 *1 (-1050)) (-5 *3 (|[\|\|]| (-461))) (-5 *2 (-85)))) ((*1 *2 *1 *3) (-12 (-5 *3 (|[\|\|]| (-1072))) (-5 *2 (-85)) (-5 *1 (-1094)))) - ((*1 *2 *1 *3) (-12 (-5 *3 (|[\|\|]| (-444))) (-5 *2 (-85)) (-5 *1 (-1094)))) + ((*1 *2 *1 *3) (-12 (-5 *3 (|[\|\|]| (-445))) (-5 *2 (-85)) (-5 *1 (-1094)))) ((*1 *2 *1 *3) (-12 (-5 *3 (|[\|\|]| (-179))) (-5 *2 (-85)) (-5 *1 (-1094)))) ((*1 *2 *1 *3) (-12 (-5 *3 (|[\|\|]| (-483))) (-5 *2 (-85)) (-5 *1 (-1094))))) (((*1 *1) (-4 *1 (-34))) ((*1 *1) (-5 *1 (-247))) ((*1 *1) (-5 *1 (-772))) @@ -3885,16 +3885,16 @@ (-12 (-5 *4 (-830)) (-5 *2 (-1178 *3)) (-5 *1 (-1090 *3)) (-4 *3 (-961))))) (((*1 *2) (-12 (-5 *2 (-1184)) (-5 *1 (-1089))))) (((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-67)))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-78)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-78)))) ((*1 *2 *1) (-12 (-4 *1 (-314 *2 *3)) (-4 *3 (-1013)) (-4 *2 (-1013)))) ((*1 *2 *1) (-12 (-4 *1 (-337)) (-5 *2 (-1072)))) ((*1 *2 *1) (-12 (-5 *2 (-1089)) (-5 *1 (-378 *3)) (-14 *3 *2))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-421)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-421)))) ((*1 *2 *1) (-12 (-4 *1 (-747 *2)) (-4 *2 (-1013)))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-774)))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-876)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-774)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-876)))) ((*1 *2 *1) (-12 (-5 *2 (-1089)) (-5 *1 (-988 *3)) (-14 *3 *2))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-1029)))) ((*1 *1 *1) (-5 *1 (-1089)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-1029)))) ((*1 *1 *1) (-5 *1 (-1089)))) (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-1089))))) (((*1 *1 *1 *2) (-12 (-5 *2 (-583 (-772))) (-5 *1 (-772)))) ((*1 *2 *1) @@ -3919,7 +3919,7 @@ ((*1 *2 *1) (-12 (-4 *1 (-1016 *2 *3 *4 *5 *6)) (-4 *3 (-1013)) (-4 *4 (-1013)) (-4 *5 (-1013)) (-4 *6 (-1013)) (-4 *2 (-1013)))) - ((*1 *1 *2) (-12 (-5 *2 (-444)) (-5 *1 (-1072)))) + ((*1 *1 *2) (-12 (-5 *2 (-445)) (-5 *1 (-1072)))) ((*1 *1 *2) (-12 (-5 *2 (-179)) (-5 *1 (-1072)))) ((*1 *1 *2) (-12 (-5 *2 (-483)) (-5 *1 (-1072)))) ((*1 *2 *1) (-12 (-5 *2 (-1072)) (-5 *1 (-1089))))) @@ -3993,7 +3993,7 @@ (-14 *4 (-1 (-85) (-2 (|:| -2400 *2) (|:| -2401 *3)) (-2 (|:| -2400 *2) (|:| -2401 *3)))))) - ((*1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-1028)) (-5 *1 (-749)))) + ((*1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-1028)) (-5 *1 (-749)))) ((*1 *1 *2 *3) (-12 (-5 *1 (-782 *2 *3)) (-4 *2 (-1128)) (-4 *3 (-1128)))) ((*1 *1 *2) (-12 (-5 *2 (-583 (-2 (|:| -3859 (-1089)) (|:| |entry| *4)))) (-4 *4 (-1013)) @@ -4541,8 +4541,8 @@ (-4 *2 (-1171 *3)))) ((*1 *2 *2) (-12 (-5 *2 (-1068 *3)) (-4 *3 (-13 (-494) (-120))) (-5 *1 (-1067 *3))))) -(((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-462)))) - ((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-1066))))) +(((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-462)))) + ((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-1066))))) (((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-1066))))) (((*1 *2 *1) (-12 (-5 *2 (-632 (-1048))) (-5 *1 (-1066))))) (((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-1066))))) @@ -5231,7 +5231,7 @@ (((*1 *2 *3) (-12 (-5 *3 (-630 *2)) (-4 *4 (-1154 *2)) (-4 *2 (-13 (-258) (-10 -8 (-15 -3970 ((-346 $) $))))) - (-5 *1 (-436 *2 *4 *5)) (-4 *5 (-351 *2 *4)))) + (-5 *1 (-437 *2 *4 *5)) (-4 *5 (-351 *2 *4)))) ((*1 *2 *1) (-12 (-4 *1 (-1036 *3 *2 *4 *5)) (-4 *4 (-196 *3 *2)) (-4 *5 (-196 *3 *2)) (-4 *2 (-961))))) @@ -5263,7 +5263,7 @@ ((*1 *2 *1) (-12 (-4 *1 (-1034 *3)) (-4 *3 (-1128)) (-5 *2 (-694))))) (((*1 *1 *1 *1) (-5 *1 (-85))) ((*1 *1 *1 *1) (-4 *1 (-96))) ((*1 *1 *1 *1) (-5 *1 (-1033)))) -(((*1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-1028)) (-5 *1 (-1029))))) +(((*1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-1028)) (-5 *1 (-1029))))) (((*1 *2 *1) (-12 (-5 *2 (-1028)) (-5 *1 (-172)))) ((*1 *2 *1) (-12 (-5 *2 (-1028)) (-5 *1 (-379)))) ((*1 *2 *1) (-12 (-5 *2 (-1028)) (-5 *1 (-749)))) @@ -5627,10 +5627,10 @@ (((*1 *1 *2) (-12 (-5 *2 (-583 *3)) (-4 *3 (-1013)) (-4 *1 (-1011 *3)))) ((*1 *1) (-12 (-4 *1 (-1011 *2)) (-4 *2 (-1013))))) (((*1 *1 *2) - (-12 (-5 *2 (-583 (-441 *3 *4 *5 *6))) (-4 *3 (-312)) (-4 *4 (-717)) - (-4 *5 (-756)) (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) + (-12 (-5 *2 (-583 (-442 *3 *4 *5 *6))) (-4 *3 (-312)) (-4 *4 (-717)) + (-4 *5 (-756)) (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) ((*1 *1 *1 *1) - (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-441 *2 *3 *4 *5)) + (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-442 *2 *3 *4 *5)) (-4 *5 (-861 *2 *3 *4)))) ((*1 *2 *3 *2) (-12 (-5 *2 (-583 *1)) (-4 *1 (-983 *4 *5 *6 *3)) (-4 *4 (-390)) @@ -5731,8 +5731,8 @@ (-12 (-5 *3 (-583 (-630 *4))) (-4 *4 (-312)) (-5 *2 (-1178 (-630 *4))) (-5 *1 (-998 *4))))) (((*1 *2 *1) (-12 (-5 *2 (-583 (-149))) (-5 *1 (-997))))) -(((*1 *2 *3 *1) (-12 (-5 *3 (-444)) (-5 *2 (-632 (-78))) (-5 *1 (-149)))) - ((*1 *2 *3 *1) (-12 (-5 *3 (-444)) (-5 *2 (-632 (-78))) (-5 *1 (-997))))) +(((*1 *2 *3 *1) (-12 (-5 *3 (-445)) (-5 *2 (-632 (-78))) (-5 *1 (-149)))) + ((*1 *2 *3 *1) (-12 (-5 *3 (-445)) (-5 *2 (-632 (-78))) (-5 *1 (-997))))) (((*1 *1 *2 *1) (-12 (-5 *2 (-78)) (-5 *1 (-997))))) (((*1 *1) (-5 *1 (-997)))) (((*1 *1) (-5 *1 (-997)))) @@ -5904,7 +5904,7 @@ ((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-55)))) ((*1 *2 *1) (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *2 (-85)) - (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) + (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) ((*1 *2 *3 *1) (-12 (-4 *1 (-980 *4 *3)) (-4 *4 (-13 (-755) (-312))) (-4 *3 (-1154 *4)) (-5 *2 (-85))))) @@ -6000,7 +6000,7 @@ (-2 (|:| -2400 *4) (|:| -2401 *5)))) (-4 *2 (-146)) (-5 *1 (-399 *3 *2 *4 *5 *6 *7)) (-4 *4 (-756)) (-4 *7 (-861 *2 *5 (-773 *3))))) - ((*1 *2 *1) (-12 (-4 *1 (-447 *2 *3)) (-4 *3 (-759)) (-4 *2 (-72)))) + ((*1 *2 *1) (-12 (-4 *1 (-448 *2 *3)) (-4 *3 (-759)) (-4 *2 (-72)))) ((*1 *2 *1) (-12 (-4 *2 (-494)) (-5 *1 (-562 *2 *3)) (-4 *3 (-1154 *2)))) ((*1 *2 *1) (-12 (-4 *1 (-645 *2)) (-4 *2 (-961)))) ((*1 *2 *1) @@ -7393,7 +7393,7 @@ (-2 (|:| -2400 *5) (|:| -2401 *6)))) (-14 *4 (-583 (-1089))) (-4 *2 (-146)) (-5 *1 (-399 *4 *2 *5 *6 *7 *8)) (-4 *8 (-861 *2 *6 (-773 *4))))) - ((*1 *1 *2 *3) (-12 (-4 *1 (-447 *2 *3)) (-4 *2 (-72)) (-4 *3 (-759)))) + ((*1 *1 *2 *3) (-12 (-4 *1 (-448 *2 *3)) (-4 *2 (-72)) (-4 *3 (-759)))) ((*1 *1 *2 *3) (-12 (-5 *3 (-483)) (-4 *2 (-494)) (-5 *1 (-562 *2 *4)) (-4 *4 (-1154 *2)))) ((*1 *1 *2 *3) (-12 (-5 *3 (-694)) (-4 *1 (-645 *2)) (-4 *2 (-961)))) @@ -7569,9 +7569,9 @@ (-4 *3 (-1013))))) (((*1 *1 *1 *1) (-12 (-5 *1 (-877 *2)) (-4 *2 (-1013))))) (((*1 *1 *1 *1) (-12 (-5 *1 (-877 *2)) (-4 *2 (-1013))))) -(((*1 *2 *1 *3) (-12 (-5 *3 (-444)) (-5 *2 (-632 (-696))) (-5 *1 (-86)))) +(((*1 *2 *1 *3) (-12 (-5 *3 (-445)) (-5 *2 (-632 (-696))) (-5 *1 (-86)))) ((*1 *2 *1 *3) (|partial| -12 (-5 *3 (-1072)) (-5 *2 (-696)) (-5 *1 (-86)))) - ((*1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-1015)) (-5 *1 (-876))))) + ((*1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-1015)) (-5 *1 (-876))))) (((*1 *1 *2 *3) (-12 (-5 *1 (-875 *2 *3)) (-4 *2 (-1013)) (-4 *3 (-1013))))) (((*1 *2 *1) (-12 (-4 *2 (-1013)) (-5 *1 (-875 *2 *3)) (-4 *3 (-1013))))) (((*1 *2 *1) (-12 (-4 *2 (-1013)) (-5 *1 (-875 *3 *2)) (-4 *3 (-1013))))) @@ -7860,11 +7860,11 @@ ((*1 *2 *2) (-12 (-4 *3 (-1013)) (-5 *1 (-841 *3 *2)) (-4 *2 (-362 *3))))) (((*1 *2 *3) (-12 (-5 *3 (-1089)) (-5 *2 (-265 (-483))) (-5 *1 (-840)))) ((*1 *2 *2) (-12 (-4 *3 (-1013)) (-5 *1 (-841 *3 *2)) (-4 *2 (-362 *3))))) -(((*1 *1 *1 *2) (-12 (-5 *2 (-444)) (-5 *1 (-86)))) +(((*1 *1 *1 *2) (-12 (-5 *2 (-445)) (-5 *1 (-86)))) ((*1 *2 *3 *4) - (-12 (-5 *3 (-1089)) (-5 *4 (-444)) (-5 *2 (-265 (-483))) (-5 *1 (-840)))) + (-12 (-5 *3 (-1089)) (-5 *4 (-445)) (-5 *2 (-265 (-483))) (-5 *1 (-840)))) ((*1 *2 *2 *3) - (-12 (-5 *3 (-444)) (-4 *4 (-1013)) (-5 *1 (-841 *4 *2)) (-4 *2 (-362 *4))))) + (-12 (-5 *3 (-445)) (-4 *4 (-1013)) (-5 *1 (-841 *4 *2)) (-4 *2 (-362 *4))))) (((*1 *2 *3) (-12 (-5 *3 (-583 (-583 (-854 (-179))))) (-5 *2 (-583 (-1001 (-179)))) (-5 *1 (-839))))) @@ -8391,7 +8391,7 @@ (-5 *1 (-818 *5 *6 *4 *7))))) (((*1 *2 *1) (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *2 (-583 *6)) - (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) + (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) ((*1 *2 *1) (-12 (-5 *2 (-583 (-813 *3))) (-5 *1 (-816 *3)) (-4 *3 (-1013))))) (((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-31)))) ((*1 *2) (-12 (-4 *1 (-345)) (-5 *2 (-830)))) ((*1 *1) (-4 *1 (-482))) @@ -8851,7 +8851,7 @@ (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-743 *3)) (-4 *3 (-1013)))) ((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-750 *3)) (-4 *3 (-1013))))) (((*1 *2 *1) (-12 (-5 *2 (-1033)) (-5 *1 (-750 *3)) (-4 *3 (-1013))))) -(((*1 *2 *3) (-12 (-5 *3 (-1072)) (-5 *2 (-167 (-439))) (-5 *1 (-748))))) +(((*1 *2 *3) (-12 (-5 *3 (-1072)) (-5 *2 (-167 (-440))) (-5 *1 (-748))))) (((*1 *2 *1) (-12 (-4 *1 (-747 *3)) (-4 *3 (-1013)) (-5 *2 (-55))))) (((*1 *1 *1) (-12 (-4 *1 (-600 *2)) (-4 *2 (-961)))) ((*1 *2 *3) @@ -9524,7 +9524,7 @@ (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-55)))) ((*1 *2 *1) (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *2 (-85)) - (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) + (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) ((*1 *2 *1) (-12 (-4 *1 (-659)) (-5 *2 (-85)))) ((*1 *2 *1) (-12 (-4 *1 (-663)) (-5 *2 (-85))))) (((*1 *1 *2) @@ -9577,7 +9577,7 @@ (-1 (-85) (-2 (|:| -2400 *3) (|:| -2401 *2)) (-2 (|:| -2400 *3) (|:| -2401 *2))))))) (((*1 *1 *2) (-12 (-5 *2 (-830)) (-4 *1 (-318)))) - ((*1 *2 *1) (-12 (-4 *2 (-759)) (-5 *1 (-451 *3 *2)) (-4 *3 (-72)))) + ((*1 *2 *1) (-12 (-4 *2 (-759)) (-5 *1 (-452 *3 *2)) (-4 *3 (-72)))) ((*1 *2 *3 *3) (-12 (-5 *3 (-830)) (-5 *2 (-1178 *4)) (-5 *1 (-465 *4)) (-4 *4 (-299)))) ((*1 *2 *1) @@ -10101,7 +10101,7 @@ (-12 (-5 *2 (-583 *7)) (-5 *3 (-1072)) (-4 *7 (-861 *4 *5 *6)) (-4 *4 (-390)) (-4 *5 (-717)) (-4 *6 (-756)) (-5 *1 (-385 *4 *5 *6 *7)))) ((*1 *1 *1) - (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-441 *2 *3 *4 *5)) + (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-442 *2 *3 *4 *5)) (-4 *5 (-861 *2 *3 *4)))) ((*1 *2 *2) (-12 (-5 *2 (-583 (-703 *3 (-773 *4)))) (-4 *3 (-390)) @@ -10366,9 +10366,9 @@ (-4 *3 (-482))))) (((*1 *2 *3 *4) (-12 (-5 *4 (-694)) (-5 *2 (-85)) (-5 *1 (-522 *3)) (-4 *3 (-482))))) -(((*1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-531)) (-5 *1 (-521))))) -(((*1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-531)) (-5 *1 (-521))))) -(((*1 *1 *2 *3 *1) (-12 (-5 *2 (-444)) (-5 *3 (-531)) (-5 *1 (-521))))) +(((*1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-531)) (-5 *1 (-521))))) +(((*1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-531)) (-5 *1 (-521))))) +(((*1 *1 *2 *3 *1) (-12 (-5 *2 (-445)) (-5 *3 (-531)) (-5 *1 (-521))))) (((*1 *1 *2 *3 *4) (-12 (-5 *3 @@ -10627,7 +10627,7 @@ (-5 *5 (-694)) (-4 *8 (-1154 *7)) (-4 *7 (-1154 *6)) (-4 *6 (-299)) (-5 *2 (-2 (|:| -2012 (-630 *7)) (|:| |basisDen| *7) (|:| |basisInv| (-630 *7)))) - (-5 *1 (-435 *6 *7 *8)))) + (-5 *1 (-436 *6 *7 *8)))) ((*1 *2 *2 *2 *2 *2) (-12 (-5 *2 (-483)) (-5 *1 (-498))))) (((*1 *2 *3 *4 *5 *5 *4 *6) (-12 (-5 *5 (-550 *4)) (-5 *6 (-1084 *4)) @@ -10899,26 +10899,26 @@ (((*1 *2 *2) (-12 (-4 *3 (-312)) (-4 *4 (-322 *3)) (-4 *5 (-322 *3)) (-5 *1 (-459 *3 *4 *5 *2)) (-4 *2 (-627 *3 *4 *5))))) -(((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-456))))) -(((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-456))))) +(((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-457))))) +(((*1 *2 *1) (-12 (-5 *2 (-1048)) (-5 *1 (-457))))) (((*1 *1 *2) (-12 (-5 *2 (-583 *3)) (-4 *3 (-1128)) (-5 *1 (-278 *3)))) ((*1 *1 *2) - (-12 (-5 *2 (-583 *3)) (-4 *3 (-1128)) (-5 *1 (-455 *3 *4)) (-14 *4 (-483))))) + (-12 (-5 *2 (-583 *3)) (-4 *3 (-1128)) (-5 *1 (-456 *3 *4)) (-14 *4 (-483))))) (((*1 *2 *1) (-12 (-5 *2 (-694)) (-5 *1 (-278 *3)) (-4 *3 (-1128)))) ((*1 *2 *1) - (-12 (-5 *2 (-694)) (-5 *1 (-455 *3 *4)) (-4 *3 (-1128)) (-14 *4 (-483))))) + (-12 (-5 *2 (-694)) (-5 *1 (-456 *3 *4)) (-4 *3 (-1128)) (-14 *4 (-483))))) (((*1 *1 *1 *2) (-12 (-5 *2 (-483)) (-5 *1 (-278 *3)) (-4 *3 (-1128)))) ((*1 *1 *1 *2) - (-12 (-5 *2 (-483)) (-5 *1 (-455 *3 *4)) (-4 *3 (-1128)) (-14 *4 *2)))) + (-12 (-5 *2 (-483)) (-5 *1 (-456 *3 *4)) (-4 *3 (-1128)) (-14 *4 *2)))) (((*1 *2 *2) (-12 (-5 *2 (-85)) (-5 *1 (-278 *3)) (-4 *3 (-1128)))) ((*1 *2 *2) - (-12 (-5 *2 (-85)) (-5 *1 (-455 *3 *4)) (-4 *3 (-1128)) (-14 *4 (-483))))) -(((*1 *1 *2 *3) (-12 (-5 *1 (-451 *3 *2)) (-4 *3 (-72)) (-4 *2 (-759))))) + (-12 (-5 *2 (-85)) (-5 *1 (-456 *3 *4)) (-4 *3 (-1128)) (-14 *4 (-483))))) +(((*1 *1 *2 *3) (-12 (-5 *1 (-452 *3 *2)) (-4 *3 (-72)) (-4 *2 (-759))))) (((*1 *1 *1 *1 *2 *3) (-12 (-5 *2 (-1 *4 *4 *4)) (-5 *3 (-1 (-85) *4 *4)) (-4 *4 (-72)) - (-5 *1 (-448 *4 *5)) (-4 *5 (-759))))) -(((*1 *2 *1) (-12 (-4 *1 (-447 *3 *2)) (-4 *3 (-72)) (-4 *2 (-759))))) -(((*1 *1) (-5 *1 (-444)))) + (-5 *1 (-449 *4 *5)) (-4 *5 (-759))))) +(((*1 *2 *1) (-12 (-4 *1 (-448 *3 *2)) (-4 *3 (-72)) (-4 *2 (-759))))) +(((*1 *1) (-5 *1 (-445)))) (((*1 *1 *1 *2 *2) (-12 (-5 *2 (-483)) (-5 *1 (-108 *3 *4 *5)) (-14 *3 *2) (-14 *4 (-694)) (-4 *5 (-146)))) @@ -10928,68 +10928,68 @@ ((*1 *2 *2 *3) (-12 (-5 *2 - (-441 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483))))) + (-442 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483))))) (-5 *3 (-583 (-773 *4))) (-14 *4 (-583 (-1089))) (-14 *5 (-694)) - (-5 *1 (-442 *4 *5))))) + (-5 *1 (-443 *4 *5))))) (((*1 *2 *3) (-12 (-14 *4 (-583 (-1089))) (-14 *5 (-694)) (-5 *2 (-583 - (-441 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483)))))) - (-5 *1 (-442 *4 *5)) + (-442 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483)))))) + (-5 *1 (-443 *4 *5)) (-5 *3 - (-441 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483)))))))) + (-442 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483)))))))) (((*1 *2 *2) (-12 (-5 *2 - (-441 (-348 (-483)) (-197 *4 (-694)) (-773 *3) (-206 *3 (-348 (-483))))) - (-14 *3 (-583 (-1089))) (-14 *4 (-694)) (-5 *1 (-442 *3 *4))))) + (-442 (-348 (-483)) (-197 *4 (-694)) (-773 *3) (-206 *3 (-348 (-483))))) + (-14 *3 (-583 (-1089))) (-14 *4 (-694)) (-5 *1 (-443 *3 *4))))) (((*1 *2 *3) (-12 (-5 *3 - (-441 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483))))) - (-14 *4 (-583 (-1089))) (-14 *5 (-694)) (-5 *2 (-85)) (-5 *1 (-442 *4 *5))))) + (-442 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483))))) + (-14 *4 (-583 (-1089))) (-14 *5 (-694)) (-5 *2 (-85)) (-5 *1 (-443 *4 *5))))) (((*1 *2 *3) (-12 (-5 *3 - (-441 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483))))) - (-14 *4 (-583 (-1089))) (-14 *5 (-694)) (-5 *2 (-85)) (-5 *1 (-442 *4 *5))))) + (-442 (-348 (-483)) (-197 *5 (-694)) (-773 *4) (-206 *4 (-348 (-483))))) + (-14 *4 (-583 (-1089))) (-14 *5 (-694)) (-5 *2 (-85)) (-5 *1 (-443 *4 *5))))) (((*1 *2 *3 *1) (-12 (-4 *4 (-312)) (-4 *5 (-717)) (-4 *6 (-756)) (-5 *2 (-85)) - (-5 *1 (-441 *4 *5 *6 *3)) (-4 *3 (-861 *4 *5 *6))))) + (-5 *1 (-442 *4 *5 *6 *3)) (-4 *3 (-861 *4 *5 *6))))) (((*1 *2 *1 *1) (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *2 (-85)) - (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5))))) + (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5))))) (((*1 *2 *3 *1) (-12 (-4 *4 (-312)) (-4 *5 (-717)) (-4 *6 (-756)) (-5 *2 (-85)) - (-5 *1 (-441 *4 *5 *6 *3)) (-4 *3 (-861 *4 *5 *6))))) + (-5 *1 (-442 *4 *5 *6 *3)) (-4 *3 (-861 *4 *5 *6))))) (((*1 *2 *1) (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *2 (-85)) - (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) + (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5)))) ((*1 *2 *1 *3) (-12 (-5 *3 (-583 *6)) (-4 *6 (-756)) (-4 *4 (-312)) (-4 *5 (-717)) - (-5 *2 (-85)) (-5 *1 (-441 *4 *5 *6 *7)) (-4 *7 (-861 *4 *5 *6))))) + (-5 *2 (-85)) (-5 *1 (-442 *4 *5 *6 *7)) (-4 *7 (-861 *4 *5 *6))))) (((*1 *1 *1 *2) - (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *1 (-441 *3 *4 *5 *2)) + (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *1 (-442 *3 *4 *5 *2)) (-4 *2 (-861 *3 *4 *5)))) ((*1 *1 *1 *1) - (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-441 *2 *3 *4 *5)) + (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-442 *2 *3 *4 *5)) (-4 *5 (-861 *2 *3 *4))))) (((*1 *2 *1 *3) (-12 (-5 *3 (-583 *6)) (-4 *6 (-756)) (-4 *4 (-312)) (-4 *5 (-717)) (-5 *2 (-2 (|:| |mval| (-630 *4)) (|:| |invmval| (-630 *4)) - (|:| |genIdeal| (-441 *4 *5 *6 *7)))) - (-5 *1 (-441 *4 *5 *6 *7)) (-4 *7 (-861 *4 *5 *6))))) + (|:| |genIdeal| (-442 *4 *5 *6 *7)))) + (-5 *1 (-442 *4 *5 *6 *7)) (-4 *7 (-861 *4 *5 *6))))) (((*1 *1 *2) (-12 (-5 *2 (-2 (|:| |mval| (-630 *3)) (|:| |invmval| (-630 *3)) - (|:| |genIdeal| (-441 *3 *4 *5 *6)))) - (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *1 (-441 *3 *4 *5 *6)) + (|:| |genIdeal| (-442 *3 *4 *5 *6)))) + (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5))))) (((*1 *1 *1) - (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-441 *2 *3 *4 *5)) + (-12 (-4 *2 (-312)) (-4 *3 (-717)) (-4 *4 (-756)) (-5 *1 (-442 *2 *3 *4 *5)) (-4 *5 (-861 *2 *3 *4))))) (((*1 *2 *1) (-12 (-4 *1 (-286 *3 *4 *5 *6)) (-4 *3 (-312)) (-4 *4 (-1154 *3)) @@ -11001,24 +11001,24 @@ (-5 *1 (-354 *3 *4 *5 *6)))) ((*1 *1 *2) (-12 (-5 *2 (-583 *6)) (-4 *6 (-861 *3 *4 *5)) (-4 *3 (-312)) (-4 *4 (-717)) - (-4 *5 (-756)) (-5 *1 (-441 *3 *4 *5 *6))))) + (-4 *5 (-756)) (-5 *1 (-442 *3 *4 *5 *6))))) (((*1 *1 *2) (-12 (-5 *2 (-583 *6)) (-4 *6 (-861 *3 *4 *5)) (-4 *3 (-312)) (-4 *4 (-717)) - (-4 *5 (-756)) (-5 *1 (-441 *3 *4 *5 *6))))) + (-4 *5 (-756)) (-5 *1 (-442 *3 *4 *5 *6))))) (((*1 *2 *1) (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *2 (-85)) - (-5 *1 (-441 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5))))) + (-5 *1 (-442 *3 *4 *5 *6)) (-4 *6 (-861 *3 *4 *5))))) (((*1 *1 *1 *2 *3) (-12 (-5 *3 (-583 *6)) (-4 *6 (-756)) (-4 *4 (-312)) (-4 *5 (-717)) - (-5 *1 (-441 *4 *5 *6 *2)) (-4 *2 (-861 *4 *5 *6)))) + (-5 *1 (-442 *4 *5 *6 *2)) (-4 *2 (-861 *4 *5 *6)))) ((*1 *1 *1 *2) - (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *1 (-441 *3 *4 *5 *2)) + (-12 (-4 *3 (-312)) (-4 *4 (-717)) (-4 *5 (-756)) (-5 *1 (-442 *3 *4 *5 *2)) (-4 *2 (-861 *3 *4 *5))))) (((*1 *2 *3) (-12 (-5 *3 (-583 *7)) (-4 *7 (-861 *4 *5 *6)) (-4 *6 (-553 (-1089))) (-4 *4 (-312)) (-4 *5 (-717)) (-4 *6 (-756)) (-5 *2 (-1079 (-583 (-857 *4)) (-583 (-249 (-857 *4))))) - (-5 *1 (-441 *4 *5 *6 *7))))) + (-5 *1 (-442 *4 *5 *6 *7))))) (((*1 *2 *1 *3 *3) (-12 (-5 *3 (-830)) (-5 *2 (-1184)) (-5 *1 (-167 *4)) (-4 *4 @@ -11031,57 +11031,57 @@ (-13 (-756) (-10 -8 (-15 -3799 ((-1072) $ (-1089))) (-15 -3616 (*2 $)) (-15 -1963 (*2 $))))))) - ((*1 *2 *1) (-12 (-5 *2 (-1184)) (-5 *1 (-439))))) + ((*1 *2 *1) (-12 (-5 *2 (-1184)) (-5 *1 (-440))))) (((*1 *2 *3 *4) (-12 (-5 *3 (-1 *7 *5)) (-4 *5 (-961)) (-4 *7 (-961)) (-4 *6 (-1154 *5)) - (-5 *2 (-1084 (-1084 *7))) (-5 *1 (-438 *5 *6 *4 *7)) (-4 *4 (-1154 *6))))) + (-5 *2 (-1084 (-1084 *7))) (-5 *1 (-439 *5 *6 *4 *7)) (-4 *4 (-1154 *6))))) (((*1 *2 *3 *4) (|partial| -12 (-5 *3 (-1 (-3 *5 "failed") *8)) (-5 *4 (-630 (-1084 *8))) (-4 *5 (-961)) (-4 *8 (-961)) (-4 *6 (-1154 *5)) (-5 *2 (-630 *6)) - (-5 *1 (-438 *5 *6 *7 *8)) (-4 *7 (-1154 *6))))) + (-5 *1 (-439 *5 *6 *7 *8)) (-4 *7 (-1154 *6))))) (((*1 *2 *3 *4) (|partial| -12 (-5 *3 (-1 (-3 *5 "failed") *7)) (-5 *4 (-1084 *7)) - (-4 *5 (-961)) (-4 *7 (-961)) (-4 *2 (-1154 *5)) (-5 *1 (-438 *5 *2 *6 *7)) + (-4 *5 (-961)) (-4 *7 (-961)) (-4 *2 (-1154 *5)) (-5 *1 (-439 *5 *2 *6 *7)) (-4 *6 (-1154 *2))))) (((*1 *2 *3 *4) (-12 (-5 *3 (-1 *5 *7)) (-5 *4 (-1084 *7)) (-4 *5 (-961)) (-4 *7 (-961)) - (-4 *2 (-1154 *5)) (-5 *1 (-438 *5 *2 *6 *7)) (-4 *6 (-1154 *2)))) + (-4 *2 (-1154 *5)) (-5 *1 (-439 *5 *2 *6 *7)) (-4 *6 (-1154 *2)))) ((*1 *2 *3 *4) (-12 (-5 *3 (-1 *7 *5)) (-4 *5 (-961)) (-4 *7 (-961)) (-4 *4 (-1154 *5)) - (-5 *2 (-1084 *7)) (-5 *1 (-438 *5 *4 *6 *7)) (-4 *6 (-1154 *4))))) + (-5 *2 (-1084 *7)) (-5 *1 (-439 *5 *4 *6 *7)) (-4 *6 (-1154 *4))))) (((*1 *2 *2 *2) (-12 (-5 *2 (-2 (|:| -2012 (-630 *3)) (|:| |basisDen| *3) (|:| |basisInv| (-630 *3)))) (-4 *3 (-13 (-258) (-10 -8 (-15 -3970 ((-346 $) $))))) (-4 *4 (-1154 *3)) - (-5 *1 (-436 *3 *4 *5)) (-4 *5 (-351 *3 *4))))) + (-5 *1 (-437 *3 *4 *5)) (-4 *5 (-351 *3 *4))))) (((*1 *2 *2 *2) (-12 (-5 *2 (-630 *3)) (-4 *3 (-13 (-258) (-10 -8 (-15 -3970 ((-346 $) $))))) - (-4 *4 (-1154 *3)) (-5 *1 (-436 *3 *4 *5)) (-4 *5 (-351 *3 *4))))) + (-4 *4 (-1154 *3)) (-5 *1 (-437 *3 *4 *5)) (-4 *5 (-351 *3 *4))))) (((*1 *2 *2 *2) (-12 (-5 *2 (-630 *3)) (-4 *3 (-13 (-258) (-10 -8 (-15 -3970 ((-346 $) $))))) - (-4 *4 (-1154 *3)) (-5 *1 (-436 *3 *4 *5)) (-4 *5 (-351 *3 *4)))) + (-4 *4 (-1154 *3)) (-5 *1 (-437 *3 *4 *5)) (-4 *5 (-351 *3 *4)))) ((*1 *2 *2 *2 *3) (-12 (-5 *2 (-630 *3)) (-4 *3 (-13 (-258) (-10 -8 (-15 -3970 ((-346 $) $))))) - (-4 *4 (-1154 *3)) (-5 *1 (-436 *3 *4 *5)) (-4 *5 (-351 *3 *4))))) + (-4 *4 (-1154 *3)) (-5 *1 (-437 *3 *4 *5)) (-4 *5 (-351 *3 *4))))) (((*1 *2 *2 *2) (-12 (-5 *2 (-694)) (-4 *3 (-13 (-258) (-10 -8 (-15 -3970 ((-346 $) $))))) - (-4 *4 (-1154 *3)) (-5 *1 (-436 *3 *4 *5)) (-4 *5 (-351 *3 *4))))) + (-4 *4 (-1154 *3)) (-5 *1 (-437 *3 *4 *5)) (-4 *5 (-351 *3 *4))))) (((*1 *2 *3 *3 *2 *4) (-12 (-5 *3 (-630 *2)) (-5 *4 (-483)) (-4 *2 (-13 (-258) (-10 -8 (-15 -3970 ((-346 $) $))))) (-4 *5 (-1154 *2)) - (-5 *1 (-436 *2 *5 *6)) (-4 *6 (-351 *2 *5))))) + (-5 *1 (-437 *2 *5 *6)) (-4 *6 (-351 *2 *5))))) (((*1 *2 *3 *2 *4) (-12 (-5 *3 (-630 *2)) (-5 *4 (-694)) (-4 *2 (-13 (-258) (-10 -8 (-15 -3970 ((-346 $) $))))) (-4 *5 (-1154 *2)) - (-5 *1 (-436 *2 *5 *6)) (-4 *6 (-351 *2 *5))))) + (-5 *1 (-437 *2 *5 *6)) (-4 *6 (-351 *2 *5))))) (((*1 *2 *3 *4 *4) (-12 (-5 *4 (-694)) (-4 *5 (-299)) (-4 *6 (-1154 *5)) (-5 *2 (-583 (-2 (|:| -2012 (-630 *6)) (|:| |basisDen| *6) (|:| |basisInv| (-630 *6))))) - (-5 *1 (-435 *5 *6 *7)) + (-5 *1 (-436 *5 *6 *7)) (-5 *3 (-2 (|:| -2012 (-630 *6)) (|:| |basisDen| *6) (|:| |basisInv| (-630 *6)))) (-4 *7 (-1154 *6))))) @@ -11094,7 +11094,7 @@ (-5 *1 (-346 *3)) (-4 *3 (-494)))) ((*1 *2 *3 *4 *4 *4) (-12 (-5 *4 (-694)) (-4 *3 (-299)) (-4 *5 (-1154 *3)) - (-5 *2 (-583 (-1084 *3))) (-5 *1 (-435 *3 *5 *6)) (-4 *6 (-1154 *5))))) + (-5 *2 (-583 (-1084 *3))) (-5 *1 (-436 *3 *5 *6)) (-4 *6 (-1154 *5))))) (((*1 *2 *1 *1) (-12 (-5 *2 (-85)) (-5 *1 (-433))))) (((*1 *1 *2) (-12 (-5 *2 (-1072)) (-5 *1 (-429))))) (((*1 *1 *2 *1) @@ -11123,8 +11123,8 @@ (((*1 *2 *2) (-12 (-5 *2 (-583 *3)) (-4 *3 (-1154 (-483))) (-5 *1 (-424 *3))))) (((*1 *2 *3) (-12 (-5 *3 (-583 *2)) (-5 *1 (-424 *2)) (-4 *2 (-1154 (-483)))))) (((*1 *1 *2) (-12 (-5 *2 (-583 *3)) (-4 *3 (-756)) (-5 *1 (-422 *3))))) -(((*1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-583 (-785))) (-5 *1 (-421))))) -(((*1 *2 *1) (-12 (-5 *2 (-583 (-444))) (-5 *1 (-49)))) +(((*1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-583 (-785))) (-5 *1 (-421))))) +(((*1 *2 *1) (-12 (-5 *2 (-583 (-445))) (-5 *1 (-49)))) ((*1 *2 *1) (-12 (-5 *2 (-583 (-785))) (-5 *1 (-421))))) (((*1 *1 *1 *2) (-12 (-5 *2 (-583 (-483))) (-5 *1 (-206 *3 *4)) (-14 *3 (-583 (-1089))) @@ -12270,7 +12270,7 @@ (((*1 *2 *1) (-12 (-5 *2 (-209)) (-5 *1 (-282))))) (((*1 *2 *1) (-12 (-5 *2 (-583 (-782 (-1094) (-694)))) (-5 *1 (-282))))) (((*1 *2 *1) (-12 (-5 *2 (-869 (-694))) (-5 *1 (-282))))) -(((*1 *2 *1) (-12 (-5 *2 (-444)) (-5 *1 (-282))))) +(((*1 *2 *1) (-12 (-5 *2 (-445)) (-5 *1 (-282))))) (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-281 *3)) (-4 *3 (-756))))) (((*1 *1) (-12 (-4 *1 (-280 *2)) (-4 *2 (-318)) (-4 *2 (-312))))) (((*1 *1 *1 *2) @@ -12441,10 +12441,10 @@ (-5 *2 (-583 (-3 (-348 (-857 *4)) (-1079 (-1089) (-857 *4))))) (-5 *1 (-248 *4))))) (((*1 *2 *1) (-12 (-5 *2 (-583 (-997))) (-5 *1 (-247))))) -(((*1 *2 *3 *3 *1) (-12 (-5 *3 (-444)) (-5 *2 (-632 (-1015))) (-5 *1 (-247))))) -(((*1 *1 *2 *2 *3 *1) (-12 (-5 *2 (-444)) (-5 *3 (-1015)) (-5 *1 (-247))))) -(((*1 *2 *3 *1) (-12 (-5 *3 (-444)) (-5 *2 (-583 (-876))) (-5 *1 (-247))))) -(((*1 *1 *2 *3 *1) (-12 (-5 *2 (-444)) (-5 *3 (-583 (-876))) (-5 *1 (-247))))) +(((*1 *2 *3 *3 *1) (-12 (-5 *3 (-445)) (-5 *2 (-632 (-1015))) (-5 *1 (-247))))) +(((*1 *1 *2 *2 *3 *1) (-12 (-5 *2 (-445)) (-5 *3 (-1015)) (-5 *1 (-247))))) +(((*1 *2 *3 *1) (-12 (-5 *3 (-445)) (-5 *2 (-583 (-876))) (-5 *1 (-247))))) +(((*1 *1 *2 *3 *1) (-12 (-5 *2 (-445)) (-5 *3 (-583 (-876))) (-5 *1 (-247))))) (((*1 *1) (-5 *1 (-247)))) (((*1 *1) (-5 *1 (-247)))) (((*1 *1) (-5 *1 (-247)))) @@ -12474,7 +12474,7 @@ (((*1 *2 *1) (-12 (-5 *2 (-1094)) (-5 *1 (-234))))) (((*1 *2 *1) (|partial| -12 (-5 *2 (-1015)) (-5 *1 (-234))))) (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-234))))) -(((*1 *2 *1) (|partial| -12 (-5 *2 (-444)) (-5 *1 (-234))))) +(((*1 *2 *1) (|partial| -12 (-5 *2 (-445)) (-5 *1 (-234))))) (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-234))))) (((*1 *2 *3 *2) (-12 (-5 *3 (-348 (-483))) (-4 *4 (-13 (-494) (-950 (-483)) (-580 (-483)))) @@ -12947,7 +12947,7 @@ (((*1 *2 *1) (-12 (-4 *1 (-160)) (-5 *2 (-583 (-85)))))) (((*1 *2 *1) (-12 (-4 *1 (-160)) (-5 *2 (-583 (-774)))))) (((*1 *2 *1) (-12 (-5 *2 (-583 (-1094))) (-5 *1 (-158 *3)) (-4 *3 (-160))))) -(((*1 *2 *3) (-12 (-5 *3 (-444)) (-5 *2 (-632 (-157))) (-5 *1 (-157))))) +(((*1 *2 *3) (-12 (-5 *3 (-445)) (-5 *2 (-632 (-157))) (-5 *1 (-157))))) (((*1 *2 *2 *2) (-12 (-4 *3 (-1128)) (-5 *1 (-156 *3 *2)) (-4 *2 (-616 *3))))) (((*1 *2 *3) (-12 (-4 *4 (-1128)) (-5 *2 (-694)) (-5 *1 (-156 *4 *3)) (-4 *3 (-616 *4))))) @@ -13242,14 +13242,14 @@ (((*1 *2 *1) (-12 (-5 *2 (-85)) (-5 *1 (-86))))) (((*1 *1 *1 *2) (-12 (-5 *2 (-1 (-85) (-86) (-86))) (-5 *1 (-86))))) (((*1 *1 *1 *2) (-12 (-5 *2 (-1 (-85) (-86) (-86))) (-5 *1 (-86))))) -(((*1 *2 *1 *3) (-12 (-5 *3 (-444)) (-5 *2 (-85)) (-5 *1 (-86))))) -(((*1 *1 *1 *2) (-12 (-5 *2 (-444)) (-5 *1 (-86)))) +(((*1 *2 *1 *3) (-12 (-5 *3 (-445)) (-5 *2 (-85)) (-5 *1 (-86))))) +(((*1 *1 *1 *2) (-12 (-5 *2 (-445)) (-5 *1 (-86)))) ((*1 *1 *1 *2) (-12 (-5 *2 (-1072)) (-5 *1 (-86))))) -(((*1 *1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-696)) (-5 *1 (-86)))) +(((*1 *1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-696)) (-5 *1 (-86)))) ((*1 *1 *1 *2 *3) (-12 (-5 *2 (-1072)) (-5 *3 (-696)) (-5 *1 (-86))))) (((*1 *1 *1 *2) (-12 (-5 *2 (-45 (-1072) (-696))) (-5 *1 (-86))))) (((*1 *1 *2) (-12 (-5 *2 (-1 *3 *3 *3)) (-4 *3 (-1128)) (-5 *1 (-79 *3))))) -(((*1 *1 *2 *3) (-12 (-5 *2 (-444)) (-5 *3 (-583 (-876))) (-5 *1 (-78))))) +(((*1 *1 *2 *3) (-12 (-5 *2 (-445)) (-5 *3 (-583 (-876))) (-5 *1 (-78))))) (((*1 *1 *2) (-12 (-5 *2 (-583 *3)) (-4 *3 (-1128)) (-4 *1 (-76 *3))))) (((*1 *2 *1) (-12 (-4 *1 (-76 *2)) (-4 *2 (-1128))))) (((*1 *2 *1) (-12 (-4 *1 (-76 *2)) (-4 *2 (-1128))))) |